Merge pull request #1534 from o1-labs/fix/lookup-gate-range-check

Bump bindings and Mina repo for lookup gate fix

CHANGELOG.md

@@ -52,6 +52,7 @@ This project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0.htm
 - Rename `Bool.Unsafe.ofField()` to `Bool.Unsafe.fromField()` https://github.com/o1-labs/o1js/pull/1485
 - Replace the namespaced type exports `Gadgets.Field3` and `Gadgets.ForeignField.Sum` with `Field3` and `ForeignFieldSum`
   - Unfortunately, the namespace didn't play well with auto-imports in TypeScript
+- Add `Gadgets.rangeCheck3x12()` and fix proof system bug that prevented it from working https://github.com/o1-labs/o1js/pull/1534
 
 ### Added
 

src/lib/provable/gadgets/gadgets.ts

@@ -29,6 +29,7 @@ import {
 } from './foreign-field.js';
 import { divMod32, addMod32 } from './arithmetic.js';
 import { SHA256 } from './sha256.js';
+import { rangeCheck3x12 } from './lookup.js';
 
 export { Gadgets, Field3, ForeignFieldSum };
 
@@ -490,6 +491,39 @@ const Gadgets = {
     return compactMultiRangeCheck(xy, z);
   },
 
+  /**
+   * Checks that three {@link Field} elements are in the range [0, 2^12) (using only one row).
+   *
+   * Internally, this gadget relies on the 12-bit [range check table](https://github.com/o1-labs/proof-systems/blob/master/kimchi/src/circuits/lookup/tables/mod.rs).
+   * All three inputs are checked to be included in that table.
+   *
+   * It's possible to use this as a range check for bit lengths n < 12, by passing in _two values_.
+   * - the value to be checked, `x`, to prove that x in [0, 2^12)
+   * - x scaled by 2^(12 - n), to prove that either x in [0, 2^n) or `x * 2^(12 - n)` overflows the field size (which is excluded by the first check)
+   *
+   * Note that both of these checks are necessary to prove x in [0, 2^n).
+   *
+   * You can find more details about lookups in the [Mina book](https://o1-labs.github.io/proof-systems/specs/kimchi.html?highlight=lookup%20gate#lookup)
+   *
+   * @param v0 - The first {@link Field} element to be checked.
+   * @param v1 - The second {@link Field} element to be checked.
+   * @param v2 - The third {@link Field} element to be checked.
+   *
+   * @throws Throws an error if one of the input values exceeds 2^12.
+   *
+   * @example
+   * ```typescript
+   * let a = Field(4000);
+   * rangeCheck3x12(a, Field(0), Field(0)); // works, since `a` is less than 12 bits
+   *
+   * let aScaled = a.mul(1 << 4); // scale `a`, to assert that it's less than 8 bits
+   * rangeCheck3x12(a, aScaled, Field(0)); // throws an error, since  `a` is greater than 8 bits (and so `aScaled` is greater than 12 bits)
+   * ```
+   */
+  rangeCheck3x12(v0: Field, v1: Field, v2: Field) {
+    return rangeCheck3x12(v0, v1, v2);
+  },
+
   /**
    * Gadgets for foreign field operations.
    *

src/lib/provable/gadgets/lookup.ts

@@ -0,0 +1,20 @@
+import { Field } from '../field.js';
+import { Gates } from '../gates.js';
+
+export { rangeCheck3x12 };
+
+function rangeCheck3x12(v0: Field, v1: Field, v2: Field) {
+  // Checks that all three input values exist in the RANGE_CHECK_TABLE (tableId: 1)
+  // v0, v1, v2 are used as the table keys
+  // The table "values" (inputs no 3, 5, 7) are 0 because the table only has one column
+  Gates.lookup(
+    // table id
+    Field.from(1),
+    v0,
+    Field.from(0),
+    v1,
+    Field.from(0),
+    v2,
+    Field.from(0)
+  );
+}

src/lib/provable/gates.ts

@@ -13,6 +13,7 @@ export {
   zero,
   rotate,
   generic,
+  lookup,
   foreignFieldAdd,
   foreignFieldMul,
   KimchiGateType,
@@ -27,6 +28,7 @@ const Gates = {
   zero,
   rotate,
   generic,
+  lookup,
   foreignFieldAdd,
   foreignFieldMul,
   raw,
@@ -158,6 +160,41 @@ function generic(
   );
 }
 
+/**
+ * **[lookup constraint](https://o1-labs.github.io/proof-systems/specs/kimchi.html?highlight=lookup%20gate#lookup)**
+ *
+ * Lookups allow you to check if a single value, or a series of values, are part of a table. The first case is useful to check for checking if a value belongs to a range (from 0 to 1,000, for example), whereas the second case is useful to check truth tables (for example, checking that three values can be found in the rows of an XOR table) or write and read from a memory vector (where one column is an index, and the other is the value stored at that index).
+ *
+ * @param tableId the [id](https://github.com/o1-labs/proof-systems/blob/master/kimchi/src/circuits/lookup/tables/mod.rs) of the lookup table.
+ * @param index0 the index of the first value to lookup.
+ * @param value0 the first value to lookup.
+ * @param index1 the index of the second value to lookup.
+ * @param value1 the second value to lookup.
+ * @param index2 the index of the third value to lookup.
+ * @param value2 the third value to lookup.
+ *
+ */
+function lookup(
+  tableId: Field,
+  index0: Field,
+  value0: Field,
+  index1: Field,
+  value1: Field,
+  index2: Field,
+  value2: Field
+) {
+  Snarky.gates.lookup([
+    0,
+    tableId.value,
+    index0.value,
+    value0.value,
+    index1.value,
+    value1.value,
+    index2.value,
+    value2.value,
+  ]);
+}
+
 function zero(a: Field, b: Field, c: Field) {
   raw(KimchiGateType.Zero, [a, b, c], []);
 }

src/lib/provable/test/lookup.unit-test.ts

@@ -0,0 +1,61 @@
+import { mod } from '../../../bindings/crypto/finite-field.js';
+import { Field } from '../field.js';
+import { ZkProgram } from '../../proof-system/zkprogram.js';
+import {
+  Spec,
+  boolean,
+  equivalentAsync,
+  fieldWithRng,
+} from '../../testing/equivalent.js';
+import { Random } from '../../testing/property.js';
+import { assert } from '../gadgets/common.js';
+import { Gadgets } from '../gadgets/gadgets.js';
+import { constraintSystem, contains } from '../../testing/constraint-system.js';
+
+let uint = (n: number | bigint): Spec<bigint, Field> => {
+  return fieldWithRng(Random.bignat((1n << BigInt(n)) - 1n));
+};
+
+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))
+  );
+};
+
+let Lookup = ZkProgram({
+  name: 'lookup',
+  methods: {
+    three12Bit: {
+      privateInputs: [Field, Field, Field],
+      async method(v0: Field, v1: Field, v2: Field) {
+        // Dummy range check to make sure the lookup table is initialized
+        // It should never fail because 64 > 12
+        Gadgets.rangeCheck64(v0);
+        Gadgets.rangeCheck3x12(v0, v1, v2);
+      },
+    },
+  },
+});
+
+// constraint system sanity check
+
+constraintSystem.fromZkProgram(Lookup, 'three12Bit', contains(['Lookup']));
+
+await Lookup.compile();
+
+await equivalentAsync(
+  { from: [uint(12), uint(12), maybeUint(12)], to: boolean },
+  { runs: 3 }
+)(
+  (x, y, z) => {
+    assert(x < 1n << 12n);
+    assert(y < 1n << 12n);
+    assert(z < 1n << 12n);
+    return true;
+  },
+  async (x, y, z) => {
+    let proof = await Lookup.three12Bit(x, y, z);
+    return await Lookup.verify(proof);
+  }
+);