Foreign fields 1: Multi-range-check gadgets

CHANGELOG.md

@@ -23,6 +23,7 @@ This project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0.htm
 
 - `Gadgets.leftShift() / Gadgets.rightShift()`, new provable method to support bitwise shifting for native field elements. https://github.com/o1-labs/o1js/pull/1194
 - `Gadgets.and()`, new provable method to support bitwise and for native field elements. https://github.com/o1-labs/o1js/pull/1193
+- `Gadgets.multiRangeCheck()` and `Gadgets.compactMultiRangeCheck()`, two building blocks for non-native arithmetic with bigints of size up to 264 bits. https://github.com/o1-labs/o1js/pull/1216
 
 ## [0.14.0](https://github.com/o1-labs/o1js/compare/045faa7...e8e7510e1)
 

src/lib/gadgets/gadgets.ts

@@ -1,7 +1,11 @@
 /**
  * Wrapper file for various gadgets, with a namespace and doccomments.
  */
-import { rangeCheck64 } from './range-check.js';
+import {
+  compactMultiRangeCheck,
+  multiRangeCheck,
+  rangeCheck64,
+} from './range-check.js';
 import { rotate, xor, and, leftShift, rightShift } from './bitwise.js';
 import { Field } from '../core.js';
 
@@ -206,4 +210,50 @@ const Gadgets = {
   and(a: Field, b: Field, length: number) {
     return and(a, b, length);
   },
+
+  /**
+   * Multi-range check.
+   *
+   * Proves that x, y, z are all in the range [0, 2^88).
+   *
+   * This takes 4 rows, so it checks 88*3/4 = 66 bits per row. This is slightly more efficient
+   * than 64-bit range checks, which can do 64 bits in 1 row.
+   *
+   * In particular, the 3x88-bit range check supports bigints up to 264 bits, which in turn is enough
+   * to support foreign field multiplication with moduli up to 2^259.
+   *
+   * @example
+   * ```ts
+   * Gadgets.multiRangeCheck([x, y, z]);
+   * ```
+   *
+   * @throws Throws an error if one of the input values exceeds 88 bits.
+   */
+  multiRangeCheck(limbs: [Field, Field, Field]) {
+    multiRangeCheck(limbs);
+  },
+
+  /**
+   * Compact multi-range check
+   *
+   * This is a variant of {@link multiRangeCheck} where the first two variables are passed in
+   * combined form xy = x + 2^88*y.
+   *
+   * The gadget
+   * - splits up xy into x and y
+   * - proves that xy = x + 2^88*y
+   * - proves that x, y, z are all in the range [0, 2^88).
+   *
+   * The split form [x, y, z] is returned.
+   *
+   * @example
+   * ```ts
+   * let [x, y] = Gadgets.compactMultiRangeCheck([xy, z]);
+   * ```
+   *
+   * @throws Throws an error if `xy` exceeds 2*88 = 176 bits, or if z exceeds 88 bits.
+   */
+  compactMultiRangeCheck(xy: Field, z: Field) {
+    return compactMultiRangeCheck(xy, z);
+  },
 };

src/lib/gadgets/range-check.ts

@@ -2,10 +2,10 @@ import { Field } from '../field.js';
 import * as Gates from '../gates.js';
 import { bitSlice, exists } from './common.js';
 
-export { rangeCheck64 };
+export { rangeCheck64, multiRangeCheck, compactMultiRangeCheck, L };
 
 /**
- * Asserts that x is in the range [0, 2^64), handles constant case
+ * Asserts that x is in the range [0, 2^64)
  */
 function rangeCheck64(x: Field) {
   if (x.isConstant()) {
@@ -48,3 +48,154 @@ function rangeCheck64(x: Field) {
     false // not using compact mode
   );
 }
+
+// default bigint limb size
+const L = 88n;
+const twoL = 2n * L;
+const lMask = (1n << L) - 1n;
+
+/**
+ * Asserts that x, y, z \in [0, 2^88)
+ */
+function multiRangeCheck([x, y, z]: [Field, Field, Field]) {
+  if (x.isConstant() && y.isConstant() && z.isConstant()) {
+    if (x.toBigInt() >> L || y.toBigInt() >> L || z.toBigInt() >> L) {
+      throw Error(`Expected fields to fit in ${L} bits, got ${x}, ${y}, ${z}`);
+    }
+    return;
+  }
+
+  let [x64, x76] = rangeCheck0Helper(x);
+  let [y64, y76] = rangeCheck0Helper(y);
+  rangeCheck1Helper({ x64, x76, y64, y76, z, yz: new Field(0) });
+}
+
+/**
+ * Compact multi-range-check - checks
+ * - xy = x + 2^88*y
+ * - x, y, z \in [0, 2^88)
+ *
+ * Returns the full limbs x, y, z
+ */
+function compactMultiRangeCheck(xy: Field, z: Field): [Field, Field, Field] {
+  // constant case
+  if (xy.isConstant() && z.isConstant()) {
+    if (xy.toBigInt() >> twoL || z.toBigInt() >> L) {
+      throw Error(
+        `Expected fields to fit in ${twoL} and ${L} bits respectively, got ${xy}, ${z}`
+      );
+    }
+    let [x, y] = splitCompactLimb(xy.toBigInt());
+    return [new Field(x), new Field(y), z];
+  }
+
+  let [x, y] = exists(2, () => splitCompactLimb(xy.toBigInt()));
+
+  let [z64, z76] = rangeCheck0Helper(z, false);
+  let [x64, x76] = rangeCheck0Helper(x, true);
+  rangeCheck1Helper({ x64: z64, x76: z76, y64: x64, y76: x76, z: y, yz: xy });
+
+  return [x, y, z];
+}
+
+function splitCompactLimb(x01: bigint): [bigint, bigint] {
+  return [x01 & lMask, x01 >> L];
+}
+
+function rangeCheck0Helper(x: Field, isCompact = false): [Field, Field] {
+  // crumbs (2-bit limbs)
+  let [x0, x2, x4, x6, x8, x10, x12, x14] = exists(8, () => {
+    let xx = x.toBigInt();
+    return [
+      bitSlice(xx, 0, 2),
+      bitSlice(xx, 2, 2),
+      bitSlice(xx, 4, 2),
+      bitSlice(xx, 6, 2),
+      bitSlice(xx, 8, 2),
+      bitSlice(xx, 10, 2),
+      bitSlice(xx, 12, 2),
+      bitSlice(xx, 14, 2),
+    ];
+  });
+
+  // 12-bit limbs
+  let [x16, x28, x40, x52, x64, x76] = exists(6, () => {
+    let xx = x.toBigInt();
+    return [
+      bitSlice(xx, 16, 12),
+      bitSlice(xx, 28, 12),
+      bitSlice(xx, 40, 12),
+      bitSlice(xx, 52, 12),
+      bitSlice(xx, 64, 12),
+      bitSlice(xx, 76, 12),
+    ];
+  });
+
+  Gates.rangeCheck0(
+    x,
+    [x76, x64, x52, x40, x28, x16],
+    [x14, x12, x10, x8, x6, x4, x2, x0],
+    isCompact
+  );
+
+  // the two highest 12-bit limbs are returned because another gate
+  // is needed to add lookups for them
+  return [x64, x76];
+}
+
+function rangeCheck1Helper(inputs: {
+  x64: Field;
+  x76: Field;
+  y64: Field;
+  y76: Field;
+  z: Field;
+  yz: Field;
+}) {
+  let { x64, x76, y64, y76, z, yz } = inputs;
+
+  // create limbs for current row
+  let [z22, z24, z26, z28, z30, z32, z34, z36, z38, z50, z62, z74, z86] =
+    exists(13, () => {
+      let zz = z.toBigInt();
+      return [
+        bitSlice(zz, 22, 2),
+        bitSlice(zz, 24, 2),
+        bitSlice(zz, 26, 2),
+        bitSlice(zz, 28, 2),
+        bitSlice(zz, 30, 2),
+        bitSlice(zz, 32, 2),
+        bitSlice(zz, 34, 2),
+        bitSlice(zz, 36, 2),
+        bitSlice(zz, 38, 12),
+        bitSlice(zz, 50, 12),
+        bitSlice(zz, 62, 12),
+        bitSlice(zz, 74, 12),
+        bitSlice(zz, 86, 2),
+      ];
+    });
+
+  // create limbs for next row
+  let [z0, z2, z4, z6, z8, z10, z12, z14, z16, z18, z20] = exists(11, () => {
+    let zz = z.toBigInt();
+    return [
+      bitSlice(zz, 0, 2),
+      bitSlice(zz, 2, 2),
+      bitSlice(zz, 4, 2),
+      bitSlice(zz, 6, 2),
+      bitSlice(zz, 8, 2),
+      bitSlice(zz, 10, 2),
+      bitSlice(zz, 12, 2),
+      bitSlice(zz, 14, 2),
+      bitSlice(zz, 16, 2),
+      bitSlice(zz, 18, 2),
+      bitSlice(zz, 20, 2),
+    ];
+  });
+
+  Gates.rangeCheck1(
+    z,
+    yz,
+    [z86, z74, z62, z50, z38, z36, z34, z32, z30, z28, z26, z24, z22],
+    [z20, z18, z16, x76, x64, y76, y64, z14, z12, z10, z8, z6, z4, z2, z0]
+  );
+}

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

@@ -1,49 +1,127 @@
+import type { Gate } from '../../snarky.js';
 import { mod } from '../../bindings/crypto/finite_field.js';
 import { Field } from '../../lib/core.js';
 import { ZkProgram } from '../proof_system.js';
+import { Provable } from '../provable.js';
 import {
   Spec,
   boolean,
   equivalentAsync,
-  field,
+  fieldWithRng,
 } from '../testing/equivalent.js';
 import { Random } from '../testing/property.js';
+import { assert, exists } from './common.js';
 import { Gadgets } from './gadgets.js';
+import { L } from './range-check.js';
+import { expect } from 'expect';
 
-let maybeUint64: Spec<bigint, Field> = {
-  ...field,
-  rng: Random.map(Random.oneOf(Random.uint64, Random.uint64.invalid), (x) =>
-    mod(x, Field.ORDER)
-  ),
+let uint = (n: number | bigint): Spec<bigint, Field> => {
+  let uint = Random.bignat((1n << BigInt(n)) - 1n);
+  return fieldWithRng(uint);
 };
 
+let maybeUint = (n: number | bigint): Spec<bigint, Field> => {
+  let uint = Random.bignat((1n << BigInt(n)) - 1n);
+  return fieldWithRng(
+    Random.map(Random.oneOf(uint, uint.invalid), (x) => mod(x, Field.ORDER))
+  );
+};
+
+// constraint system sanity check
+
+function csWithoutGenerics(gates: Gate[]) {
+  return gates.map((g) => g.type).filter((type) => type !== 'Generic');
+}
+
+let check64 = Provable.constraintSystem(() => {
+  let [x] = exists(1, () => [0n]);
+  Gadgets.rangeCheck64(x);
+});
+let multi = Provable.constraintSystem(() => {
+  let x = exists(3, () => [0n, 0n, 0n]);
+  Gadgets.multiRangeCheck(x);
+});
+let compact = Provable.constraintSystem(() => {
+  let [xy, z] = exists(2, () => [0n, 0n]);
+  Gadgets.compactMultiRangeCheck(xy, z);
+});
+
+let expectedLayout64 = ['RangeCheck0'];
+let expectedLayoutMulti = ['RangeCheck0', 'RangeCheck0', 'RangeCheck1', 'Zero'];
+
+expect(csWithoutGenerics(check64.gates)).toEqual(expectedLayout64);
+expect(csWithoutGenerics(multi.gates)).toEqual(expectedLayoutMulti);
+expect(csWithoutGenerics(compact.gates)).toEqual(expectedLayoutMulti);
+
 // TODO: make a ZkFunction or something that doesn't go through Pickles
 // --------------------------
 // RangeCheck64 Gate
 // --------------------------
 
-let RangeCheck64 = ZkProgram({
-  name: 'range-check-64',
+let RangeCheck = ZkProgram({
+  name: 'range-check',
   methods: {
-    run: {
+    check64: {
       privateInputs: [Field],
       method(x) {
         Gadgets.rangeCheck64(x);
       },
     },
+    checkMulti: {
+      privateInputs: [Field, Field, Field],
+      method(x, y, z) {
+        Gadgets.multiRangeCheck([x, y, z]);
+      },
+    },
+    checkCompact: {
+      privateInputs: [Field, Field],
+      method(xy, z) {
+        let [x, y] = Gadgets.compactMultiRangeCheck(xy, z);
+        x.add(y.mul(1n << L)).assertEquals(xy);
+      },
+    },
   },
 });
 
-await RangeCheck64.compile();
+await RangeCheck.compile();
 
 // TODO: we use this as a test because there's no way to check custom gates quickly :(
-await equivalentAsync({ from: [maybeUint64], to: boolean }, { runs: 3 })(
+
+await equivalentAsync({ from: [maybeUint(64)], to: boolean }, { runs: 3 })(
   (x) => {
-    if (x >= 1n << 64n) throw Error('expected 64 bits');
+    assert(x < 1n << 64n);
     return true;
   },
   async (x) => {
-    let proof = await RangeCheck64.run(x);
-    return await RangeCheck64.verify(proof);
+    let proof = await RangeCheck.check64(x);
+    return await RangeCheck.verify(proof);
+  }
+);
+
+await equivalentAsync(
+  { from: [maybeUint(L), uint(L), uint(L)], to: boolean },
+  { runs: 3 }
+)(
+  (x, y, z) => {
+    assert(!(x >> L) && !(y >> L) && !(z >> L), 'multi: not out of range');
+    return true;
+  },
+  async (x, y, z) => {
+    let proof = await RangeCheck.checkMulti(x, y, z);
+    return await RangeCheck.verify(proof);
+  }
+);
+
+await equivalentAsync(
+  { from: [maybeUint(2n * L), uint(L)], to: boolean },
+  { runs: 3 }
+)(
+  (xy, z) => {
+    assert(!(xy >> (2n * L)) && !(z >> L), 'compact: not out of range');
+    return true;
+  },
+  async (xy, z) => {
+    let proof = await RangeCheck.checkCompact(xy, z);
+    return await RangeCheck.verify(proof);
   }
 );