Merge pull request #1735 from o1-labs/audit/is-positive

Refactor Int64: Introduce canonical zero representation and consistent positivity checks

CHANGELOG.md

@@ -32,6 +32,8 @@ This project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0.htm
 - A warning about the current reducer API limitations, as well as a mention of active work to mitigate them was added to doc comments and examples https://github.com/o1-labs/o1js/pull/1728
 - `ForeignField`-based representation of scalars via `ScalarField` https://github.com/o1-labs/o1js/pull/1705
 - Introduced new V2 methods for nullifier operations: `isUnusedV2()`, `assertUnusedV2()`, and `setUsedV2()` https://github.com/o1-labs/o1js/pull/1715
+- `Int64.create()` method for safe instance creation with canonical zero representation https://github.com/o1-labs/o1js/pull/1735
+- New V2 methods for `Int64` operations: `fromObjectV2`, `divV2()` https://github.com/o1-labs/o1js/pull/1735
 - `Experimental.BatchReducer` to reduce actions in batches https://github.com/o1-labs/o1js/pull/1676
   - Avoids the account update limit
   - Handles arbitrary numbers of pending actions thanks to recursive validation of the next batch
@@ -54,6 +56,8 @@ This project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0.htm
 
 - Deprecated `Nullifier.isUnused()`, `Nullifier.assertUnused()`, and `Nullifier.setUsed()` methods https://github.com/o1-labs/o1js/pull/1715
 - `createEcdsa`, `createForeignCurve`, `ForeignCurve` and `EcdsaSignature` deprecated in favor of `V2` versions due to a security vulnerability found in the current implementation https://github.com/o1-labs/o1js/pull/1703
+- `Int64` constructor, recommending `Int64.create()` instead https://github.com/o1-labs/o1js/pull/1735
+- Original `div()` and `fromObject`, methods in favor of V2 versions https://github.com/o1-labs/o1js/pull/1735
 - Deprecate `AccountUpdate.defaultAccountUpdate()` in favor of `AccountUpdate.default()` https://github.com/o1-labs/o1js/pull/1676
 
 ### Fixed

src/lib/mina/account-update.ts

@@ -730,11 +730,11 @@ class AccountUpdate implements Types.AccountUpdate {
     }
 
     // Sub the amount from the sender's account
-    this.body.balanceChange = Int64.fromObject(this.body.balanceChange).sub(
-      amount
-    );
+    this.body.balanceChange = Int64.Unsafe.fromObject(
+      this.body.balanceChange
+    ).sub(amount);
     // Add the amount to the receiver's account
-    receiver.body.balanceChange = Int64.fromObject(
+    receiver.body.balanceChange = Int64.Unsafe.fromObject(
       receiver.body.balanceChange
     ).add(amount);
     return receiver;
@@ -778,7 +778,7 @@ class AccountUpdate implements Types.AccountUpdate {
   }
 
   get balanceChange() {
-    return Int64.fromObject(this.body.balanceChange);
+    return Int64.Unsafe.fromObject(this.body.balanceChange);
   }
   set balanceChange(x: Int64) {
     this.body.balanceChange = x;

src/lib/mina/errors.ts

@@ -15,7 +15,9 @@ const ErrorHandlers = {
 
     let balances = accountUpdates.map(({ body }) => {
       if (body.tokenId.equals(TokenId.default).toBoolean()) {
-        return Number(Int64.fromObject(body.balanceChange).toString()) * 1e-9;
+        return (
+          Number(Int64.Unsafe.fromObject(body.balanceChange).toString()) * 1e-9
+        );
       }
     });
     let sum = balances.reduce((a = 0, b = 0) => a + b) ?? 0;

src/lib/provable/int.ts

@@ -1048,10 +1048,48 @@ class Int64 extends CircuitValue implements BalanceChange {
   // The second point is one of the main things an Int64 is used for, and was the original motivation to use 2 fields.
   // Overall, I think the existing implementation is the optimal one.
 
+  /**
+   * @deprecated Use {@link Int64.create} for safe creation.
+   *
+   * WARNING: This constructor allows for ambiguous representation of zero (both +0 and -0).
+   * This can lead to unexpected behavior in operations like {@link isPositive()} and {@link mod()}.
+   *
+   * Security Implications:
+   * 1. A malicious prover could choose either positive or negative zero.
+   * 2. Arithmetic operations that result in 0 may allow an attacker to arbitrarily choose the sign.
+   * 3. This ambiguity could be exploited in protocols using Int64s for calculations like PNL tracking.
+   *
+   * Recommended Fix:
+   * Use Int64.create() which enforces a canonical representation of zero, or
+   * explicitly handle the zero case in operations like mod().
+   *
+   * @param magnitude - The magnitude of the integer as a UInt64.
+   * @param [sgn=Sign.one] - The sign of the integer. Default is positive (Sign.one).
+   */
   constructor(magnitude: UInt64, sgn = Sign.one) {
     super(magnitude, sgn);
   }
 
+  /**
+   * Safely creates a new Int64 instance, enforcing canonical representation of zero.
+   * This is the recommended way to create Int64 instances.
+   *
+   * @param magnitude - The magnitude of the integer as a UInt64
+   * @param sgn - The sign of the integer.
+   * @returns A new Int64 instance with a canonical representation.
+   *
+   * @example
+   * ```ts
+   * const x = Int64.create(0); // canonical representation of zero
+   * ```
+   */
+  static create(magnitude: UInt64, sign: Sign = Sign.one): Int64 {
+    const mag = UInt64.from(magnitude);
+    const isZero = mag.equals(UInt64.zero);
+    const canonicalSign = Provable.if(isZero, Sign.one, sign);
+    return new Int64(mag, canonicalSign);
+  }
+
   /**
    * Creates a new {@link Int64} from a {@link Field}.
    *
@@ -1092,6 +1130,23 @@ class Int64 extends CircuitValue implements BalanceChange {
     }
     return Int64.fromFieldUnchecked(Field(x));
   }
+
+  static Unsafe = {
+    /**
+     * @deprecated Use {@link Int64.fromObjectV2} instead.
+     */
+    fromObject(obj: { magnitude: UInt64; sgn: Sign }): Int64 {
+      return CircuitValue.fromObject.call(Int64, obj);
+    },
+  };
+
+  fromObjectV2(obj: {
+    magnitude: UInt64 | number | string | bigint;
+    sgn: Sign | bigint;
+  }) {
+    return Int64.create(UInt64.from(obj.magnitude), Sign.fromValue(obj.sgn));
+  }
+
   /**
    * Turns the {@link Int64} into a string.
    */
@@ -1155,9 +1210,22 @@ class Int64 extends CircuitValue implements BalanceChange {
   }
 
   /**
-   * Negates the value.
+   * Negates the current Int64 value.
+   *
+   * This method returns a new Int64 instance with the opposite sign of the current value.
+   * If the current value is zero, it returns zero.
    *
-   * `Int64.from(5).neg()` will turn into `Int64.from(-5)`
+   * @returns A new Int64 instance with the negated value.
+   *
+   * @example
+   * ```ts
+   * Int64.from(5).negV2();
+   * ```
+   *
+   * @see {@link Int64#from} for creating Int64 instances
+   * @see {@link Int64#zero} for the zero constant
+   *
+   * @throws {Error} Implicitly, if the internal Provable.if condition fails
    */
   negV2() {
     return Provable.if(
@@ -1202,6 +1270,31 @@ class Int64 extends CircuitValue implements BalanceChange {
     return new Int64(quotient, sign);
   }
 
+  /**
+   * Integer division with canonical zero representation.
+   *
+   * @param y - The divisor. Can be an Int64, number, string, bigint, UInt64, or UInt32.
+   * @returns A new Int64 representing the quotient, with canonical zero representation.
+   *
+   * @remarks
+   * This method performs the same division operation as {@link div},
+   * but ensures that the result always has a canonical representation,
+   * particularly for zero results.
+   *
+   * `x.divV2(y)` returns the floor of `x / y`, that is, the greatest
+   * *`z`* such that *`z * y <= x`.
+   * On negative numbers, this rounds towards zero.
+   *
+   * This method guarantees that all results, including zero, have a consistent
+   * representation, eliminating potential ambiguities in zero handling.
+   */
+  divV2(y: Int64 | number | string | bigint | UInt64 | UInt32) {
+    let y_ = Int64.from(y);
+    let { quotient } = this.magnitude.divMod(y_.magnitude);
+    let sign = this.sgn.mul(y_.sgn);
+    return Int64.create(quotient, sign);
+  }
+
   /**
    * @deprecated Use {@link modV2()} instead.
    * This implementation is vulnerable whenever `this` is zero.
@@ -1215,10 +1308,25 @@ class Int64 extends CircuitValue implements BalanceChange {
   }
 
   /**
-   * Integer remainder.
+   * Calculates the integer remainder of this Int64 divided by the given value.
    *
-   * `x.mod(y)` returns the value `z` such that `0 <= z < y` and
-   * `x - z` is divisible by `y`.
+   * The result `z` satisfies the following conditions:
+   * 1. 0 <= z < |y|
+   * 2. x - z is divisible by y
+   *
+   * Note: This method follows the "truncate toward zero" convention for negative numbers.
+   *
+   * @param y - The divisor. Will be converted to UInt64 if not already.
+   * @returns A new Int64 instance representing the remainder.
+   *
+   * @example
+   * ```ts
+   * const x1 = Int64.from(17);
+   * const y1 = UInt64.from(5);
+   * console.log(x1.modV2(y1).toString()); // Output: 2
+   * ```
+   *
+   * @throws {Error} Implicitly, if y is zero or negative.
    */
   modV2(y: UInt64 | number | string | bigint | UInt32) {
     let y_ = UInt64.from(y);
@@ -1256,7 +1364,14 @@ class Int64 extends CircuitValue implements BalanceChange {
   }
 
   /**
-   * Checks if the value is positive (x > 0).
+   * Checks if the value is strictly positive (x > 0).
+   *
+   * @returns True if the value is greater than zero, false otherwise.
+   *
+   * @remarks
+   * This method considers zero as non-positive. It ensures consistency
+   * with the mathematical definition of "positive" as strictly greater than zero.
+   * This differs from some other methods which may treat zero as non-negative.
    */
   isPositiveV2() {
     return this.magnitude.equals(UInt64.zero).not().and(this.sgn.isPositive());