Merge pull request #1181 from o1-labs/feature/refactor-equivalence-tests

Expose and test rangeCheck64 gadget

CHANGELOG.md

@@ -29,6 +29,8 @@ This project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0.htm
 
 - Internal support for several custom gates (range check, bitwise operations, foreign field operations) and lookup tables https://github.com/o1-labs/o1js/pull/1176
 
+- `Gadgets.rangeCheck64()`, new provable method to do efficient 64-bit range checks using lookup tables https://github.com/o1-labs/o1js/pull/1181
+
 ## [0.13.1](https://github.com/o1-labs/o1js/compare/c2f392fe5...045faa7)
 
 ### Breaking changes
@@ -41,6 +43,7 @@ This project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0.htm
 
 - Improve prover performance by ~25% https://github.com/o1-labs/o1js/pull/1092
   - Change internal representation of field elements to be JS bigint instead of Uint8Array
+- Consolidate internal framework for testing equivalence of two implementations
 
 ## [0.13.0](https://github.com/o1-labs/o1js/compare/fbd4b2717...c2f392fe5)
 

src/examples/ex02_root.ts

@@ -1,4 +1,4 @@
-import { Field, Circuit, circuitMain, public_, UInt64 } from 'o1js';
+import { Field, Circuit, circuitMain, public_, UInt64, Gadgets } from 'o1js';
 
 /* Exercise 2:
 
@@ -10,6 +10,7 @@ Prove:
 class Main extends Circuit {
   @circuitMain
   static main(@public_ y: Field, x: UInt64) {
+    Gadgets.rangeCheck64(x.value);
     let y3 = y.square().mul(y);
     y3.assertEquals(x.value);
   }

src/examples/ex02_root_program.ts

@@ -1,11 +1,4 @@
-import {
-  Field,
-  Circuit,
-  circuitMain,
-  public_,
-  UInt64,
-  Experimental,
-} from 'o1js';
+import { Field, UInt64, Experimental, Gadgets } from 'o1js';
 
 let { ZkProgram } = Experimental;
 
@@ -15,6 +8,7 @@ const Main = ZkProgram({
     main: {
       privateInputs: [UInt64],
       method(y: Field, x: UInt64) {
+        Gadgets.rangeCheck64(x.value);
         let y3 = y.square().mul(y);
         y3.assertEquals(x.value);
       },

src/index.ts

@@ -21,6 +21,7 @@ export {
 export { Provable } from './lib/provable.js';
 export { Circuit, Keypair, public_, circuitMain } from './lib/circuit.js';
 export { UInt32, UInt64, Int64, Sign } from './lib/int.js';
+export { Gadgets } from './lib/gadgets/gadgets.js';
 export { Types } from './bindings/mina-transaction/types.js';
 
 export * as Mina from './lib/mina.js';

src/lib/field.unit-test.ts

@@ -7,7 +7,16 @@ import { Provable } from './provable.js';
 import { Binable } from '../bindings/lib/binable.js';
 import { ProvableExtended } from './circuit_value.js';
 import { FieldType } from './field.js';
-import { createEquivalenceTesters, throwError } from './testing/equivalent.js';
+import {
+  equivalentProvable as equivalent,
+  oneOf,
+  field,
+  bigintField,
+  throwError,
+  unit,
+  bool,
+  Spec,
+} from './testing/equivalent.js';
 
 // types
 Field satisfies Provable<Field>;
@@ -56,73 +65,75 @@ test(Random.field, Random.int(-5, 5), (x, k) => {
   deepEqual(Field(x + BigInt(k) * Field.ORDER), Field(x));
 });
 
+// Field | bigint parameter
+let fieldOrBigint = oneOf(field, bigintField);
+
 // special generator
 let SmallField = Random.reject(
   Random.field,
   (x) => x.toString(2).length > Fp.sizeInBits - 2
 );
-
-let { equivalent1, equivalent2, equivalentVoid1, equivalentVoid2 } =
-  createEquivalenceTesters(Field, Field);
+let smallField: Spec<bigint, Field> = { ...field, rng: SmallField };
+let smallBigint: Spec<bigint, bigint> = { ...bigintField, rng: SmallField };
+let smallFieldOrBigint = oneOf(smallField, smallBigint);
 
 // arithmetic, both in- and outside provable code
-equivalent2((x, y) => x.add(y), Fp.add);
-equivalent1((x) => x.neg(), Fp.negate);
-equivalent2((x, y) => x.sub(y), Fp.sub);
-equivalent2((x, y) => x.mul(y), Fp.mul);
+let equivalent1 = equivalent({ from: [field], to: field });
+let equivalent2 = equivalent({ from: [field, fieldOrBigint], to: field });
+
+equivalent2(Fp.add, (x, y) => x.add(y));
+equivalent1(Fp.negate, (x) => x.neg());
+equivalent2(Fp.sub, (x, y) => x.sub(y));
+equivalent2(Fp.mul, (x, y) => x.mul(y));
 equivalent1(
-  (x) => x.inv(),
-  (x) => Fp.inverse(x) ?? throwError('division by 0')
+  (x) => Fp.inverse(x) ?? throwError('division by 0'),
+  (x) => x.inv()
 );
 equivalent2(
-  (x, y) => x.div(y),
-  (x, y) => Fp.div(x, y) ?? throwError('division by 0')
+  (x, y) => Fp.div(x, y) ?? throwError('division by 0'),
+  (x, y) => x.div(y)
 );
-equivalent1((x) => x.square(), Fp.square);
+equivalent1(Fp.square, (x) => x.square());
 equivalent1(
-  (x) => x.sqrt(),
-  (x) => Fp.sqrt(x) ?? throwError('no sqrt')
+  (x) => Fp.sqrt(x) ?? throwError('no sqrt'),
+  (x) => x.sqrt()
 );
-equivalent2(
-  (x, y) => x.equals(y).toField(),
-  (x, y) => BigInt(x === y)
+equivalent({ from: [field, fieldOrBigint], to: bool })(
+  (x, y) => x === y,
+  (x, y) => x.equals(y)
 );
-equivalent2(
-  (x, y) => x.lessThan(y).toField(),
-  (x, y) => BigInt(x < y),
-  SmallField
+
+equivalent({ from: [smallField, smallFieldOrBigint], to: bool })(
+  (x, y) => x < y,
+  (x, y) => x.lessThan(y)
 );
-equivalent2(
-  (x, y) => x.lessThanOrEqual(y).toField(),
-  (x, y) => BigInt(x <= y),
-  SmallField
+equivalent({ from: [smallField, smallFieldOrBigint], to: bool })(
+  (x, y) => x <= y,
+  (x, y) => x.lessThanOrEqual(y)
 );
-equivalentVoid2(
-  (x, y) => x.assertEquals(y),
-  (x, y) => x === y || throwError('not equal')
+equivalent({ from: [field, fieldOrBigint], to: unit })(
+  (x, y) => x === y || throwError('not equal'),
+  (x, y) => x.assertEquals(y)
 );
-equivalentVoid2(
-  (x, y) => x.assertNotEquals(y),
-  (x, y) => x !== y || throwError('equal')
+equivalent({ from: [field, fieldOrBigint], to: unit })(
+  (x, y) => x !== y || throwError('equal'),
+  (x, y) => x.assertNotEquals(y)
 );
-equivalentVoid2(
-  (x, y) => x.assertLessThan(y),
+equivalent({ from: [smallField, smallFieldOrBigint], to: unit })(
   (x, y) => x < y || throwError('not less than'),
-  SmallField
+  (x, y) => x.assertLessThan(y)
 );
-equivalentVoid2(
-  (x, y) => x.assertLessThanOrEqual(y),
+equivalent({ from: [smallField, smallFieldOrBigint], to: unit })(
   (x, y) => x <= y || throwError('not less than or equal'),
-  SmallField
+  (x, y) => x.assertLessThanOrEqual(y)
 );
-equivalentVoid1(
-  (x) => x.assertBool(),
-  (x) => x === 0n || x === 1n || throwError('not boolean')
+equivalent({ from: [field], to: unit })(
+  (x) => x === 0n || x === 1n || throwError('not boolean'),
+  (x) => x.assertBool()
 );
-equivalent1(
-  (x) => x.isEven().toField(),
-  (x) => BigInt((x & 1n) === 0n),
-  SmallField
+equivalent({ from: [smallField], to: bool })(
+  (x) => (x & 1n) === 0n,
+  (x) => x.isEven()
 );
 
 // non-constant field vars

src/lib/gadgets/gadgets.ts

@@ -0,0 +1,36 @@
+/**
+ * Wrapper file for various gadgets, with a namespace and doccomments.
+ */
+import { rangeCheck64 } from './range-check.js';
+import { Field } from '../core.js';
+
+export { Gadgets };
+
+const Gadgets = {
+  /**
+   * Asserts that the input value is in the range [0, 2^64).
+   *
+   * This function proves that the provided field element can be represented with 64 bits.
+   * If the field element exceeds 64 bits, an error is thrown.
+   *
+   * @param x - The value to be range-checked.
+   *
+   * @throws Throws an error if the input value exceeds 64 bits.
+   *
+   * @example
+   * ```ts
+   * const x = Provable.witness(Field, () => Field(12345678n));
+   * rangeCheck64(x); // successfully proves 64-bit range
+   *
+   * const xLarge = Provable.witness(Field, () => Field(12345678901234567890123456789012345678n));
+   * rangeCheck64(xLarge); // throws an error since input exceeds 64 bits
+   * ```
+   *
+   * **Note**: Small "negative" field element inputs are interpreted as large integers close to the field size,
+   * and don't pass the 64-bit check. If you want to prove that a value lies in the int64 range [-2^63, 2^63),
+   * you could use `rangeCheck64(x.add(1n << 63n))`.
+   */
+  rangeCheck64(x: Field) {
+    return rangeCheck64(x);
+  },
+};

src/lib/gadgets/gadgets.unit-test.ts

@@ -0,0 +1,47 @@
+import { mod } from '../../bindings/crypto/finite_field.js';
+import { Field } from '../field.js';
+import { ZkProgram } from '../proof_system.js';
+import {
+  Spec,
+  boolean,
+  equivalentAsync,
+  field,
+} from '../testing/equivalent.js';
+import { Random } from '../testing/random.js';
+import { Gadgets } from './gadgets.js';
+
+// TODO: make a ZkFunction or something that doesn't go through Pickles
+
+let RangeCheck64 = ZkProgram({
+  methods: {
+    run: {
+      privateInputs: [Field],
+      method(x) {
+        Gadgets.rangeCheck64(x);
+      },
+    },
+  },
+});
+
+await RangeCheck64.compile();
+
+let maybeUint64: Spec<bigint, Field> = {
+  ...field,
+  rng: Random.map(Random.oneOf(Random.uint64, Random.uint64.invalid), (x) =>
+    mod(x, Field.ORDER)
+  ),
+};
+
+// do a couple of proofs
+// TODO: we use this as a test because there's no way to check custom gates quickly :(
+
+equivalentAsync({ from: [maybeUint64], to: boolean }, { runs: 3 })(
+  (x) => {
+    if (x >= 1n << 64n) throw Error('expected 64 bits');
+    return true;
+  },
+  async (x) => {
+    let proof = await RangeCheck64.run(x);
+    return await RangeCheck64.verify(proof);
+  }
+);

src/lib/gadgets/range-check.ts

@@ -3,6 +3,9 @@ import * as Gates from '../gates.js';
 
 export { rangeCheck64 };
 
+/**
+ * Asserts that x is in the range [0, 2^64), handles constant case
+ */
 function rangeCheck64(x: Field) {
   if (x.isConstant()) {
     if (x.toBigInt() >= 1n << 64n) {