Merge pull request #1193 from o1-labs/feature/AND-gadget

Implements AND gadget

src/examples/gadgets.ts

@@ -14,10 +14,10 @@ let cs = Provable.constraintSystem(() => {
 });
 console.log('constraint system: ', cs);
 
-const ROT = ZkProgram({
-  name: 'rot-example',
+const BitwiseProver = ZkProgram({
+  name: 'bitwise',
   methods: {
-    baseCase: {
+    rot: {
       privateInputs: [],
       method: () => {
         let a = Provable.witness(Field, () => Field(48));
@@ -31,13 +31,7 @@ const ROT = ZkProgram({
         actualRight.assertEquals(expectedRight);
       },
     },
-  },
-});
-
-const XOR = ZkProgram({
-  name: 'xor-example',
-  methods: {
-    baseCase: {
+    xor: {
       privateInputs: [],
       method: () => {
         let a = Provable.witness(Field, () => Field(5));
@@ -47,24 +41,38 @@ const XOR = ZkProgram({
         actual.assertEquals(expected);
       },
     },
+    and: {
+      privateInputs: [],
+      method: () => {
+        let a = Provable.witness(Field, () => Field(3));
+        let b = Provable.witness(Field, () => Field(5));
+        let actual = Gadgets.and(a, b, 4);
+        let expected = Field(1);
+        actual.assertEquals(expected);
+      },
+    },
   },
 });
 
 console.log('compiling..');
 
 console.time('compile');
-await ROT.compile();
-await XOR.compile();
+await BitwiseProver.compile();
 console.timeEnd('compile');
 
 console.log('proving..');
 
 console.time('rotation prove');
-let rotProof = await ROT.baseCase();
+let rotProof = await BitwiseProver.rot();
 console.timeEnd('rotation prove');
-if (!(await ROT.verify(rotProof))) throw Error('rotate: Invalid proof');
+if (!(await BitwiseProver.verify(rotProof))) throw Error('rot: Invalid proof');
 
 console.time('xor prove');
-let proof = await XOR.baseCase();
+let xorProof = await BitwiseProver.xor();
 console.timeEnd('xor prove');
-if (!(await XOR.verify(proof))) throw Error('Invalid proof');
+if (!(await BitwiseProver.verify(xorProof))) throw Error('xor: Invalid proof');
+
+console.time('and prove');
+let andProof = await BitwiseProver.and();
+console.timeEnd('and prove');
+if (!(await BitwiseProver.verify(andProof))) throw Error('and: Invalid proof');

src/examples/primitive_constraint_system.ts

@@ -79,6 +79,14 @@ const BitwiseMock = {
     Gadgets.xor(a, b, 48);
     Gadgets.xor(a, b, 64);
   },
+  and() {
+    let a = Provable.witness(Field, () => new Field(5n));
+    let b = Provable.witness(Field, () => new Field(5n));
+    Gadgets.and(a, b, 16);
+    Gadgets.and(a, b, 32);
+    Gadgets.and(a, b, 48);
+    Gadgets.and(a, b, 64);
+  },
 };
 
 export const GroupCS = mock(GroupMock, 'Group Primitive');

src/examples/regression_test.json

@@ -175,6 +175,10 @@
       "xor": {
         "rows": 15,
         "digest": "b3595a9cc9562d4f4a3a397b6de44971"
+      },
+      "and": {
+        "rows": 19,
+        "digest": "647e6fd1852873d1c326ba1cd269cff2"
       }
     },
     "verificationKey": {

src/lib/gadgets/bitwise.ts

@@ -10,7 +10,7 @@ import {
   divideWithRemainder,
 } from './common.js';
 
-export { xor, rotate };
+export { xor, and, rotate };
 
 function xor(a: Field, b: Field, length: number) {
   // check that both input lengths are positive
@@ -39,13 +39,13 @@ function xor(a: Field, b: Field, length: number) {
       `${b.toBigInt()} does not fit into ${padLength} bits`
     );
 
-    return new Field(Fp.xor(a.toBigInt(), b.toBigInt()));
+    return new Field(a.toBigInt() ^ b.toBigInt());
   }
 
   // calculate expected xor output
   let outputXor = Provable.witness(
     Field,
-    () => new Field(Fp.xor(a.toBigInt(), b.toBigInt()))
+    () => new Field(a.toBigInt() ^ b.toBigInt())
   );
 
   // builds the xor gadget chain
@@ -118,6 +118,52 @@ function buildXor(
   zero.assertEquals(expectedOutput);
 }
 
+function and(a: Field, b: Field, length: number) {
+  // check that both input lengths are positive
+  assert(length > 0, `Input lengths need to be positive values.`);
+
+  // check that length does not exceed maximum field size in bits
+  assert(
+    length <= Field.sizeInBits(),
+    `Length ${length} exceeds maximum of ${Field.sizeInBits()} bits.`
+  );
+
+  // obtain pad length until the length is a multiple of 16 for n-bit length lookup table
+  let padLength = Math.ceil(length / 16) * 16;
+
+  // handle constant case
+  if (a.isConstant() && b.isConstant()) {
+    let max = 1n << BigInt(padLength);
+
+    assert(
+      a.toBigInt() < max,
+      `${a.toBigInt()} does not fit into ${padLength} bits`
+    );
+
+    assert(
+      b.toBigInt() < max,
+      `${b.toBigInt()} does not fit into ${padLength} bits`
+    );
+
+    return new Field(a.toBigInt() & b.toBigInt());
+  }
+
+  // calculate expect and output
+  let outputAnd = Provable.witness(
+    Field,
+    () => new Field(a.toBigInt() & b.toBigInt())
+  );
+
+  // compute values for gate
+  // explanation: https://o1-labs.github.io/proof-systems/specs/kimchi.html?highlight=gates#and
+  let sum = a.add(b);
+  let xorOutput = xor(a, b, length);
+  outputAnd.mul(2).add(xorOutput).assertEquals(sum);
+
+  // return the result of the and operation
+  return outputAnd;
+}
+
 function rotate(
   field: Field,
   bits: number,

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

@@ -22,6 +22,12 @@ let Bitwise = ZkProgram({
         return Gadgets.xor(a, b, 64);
       },
     },
+    and: {
+      privateInputs: [Field, Field],
+      method(a: Field, b: Field) {
+        return Gadgets.and(a, b, 64);
+      },
+    },
     rot: {
       privateInputs: [Field],
       method(a: Field) {
@@ -37,9 +43,13 @@ let uint = (length: number) => fieldWithRng(Random.biguint(length));
 
 [2, 4, 8, 16, 32, 64, 128].forEach((length) => {
   equivalent({ from: [uint(length), uint(length)], to: field })(
-    Fp.xor,
+    (x, y) => x ^ y,
     (x, y) => Gadgets.xor(x, y, length)
   );
+  equivalent({ from: [uint(length), uint(length)], to: field })(
+    (x, y) => x & y,
+    (x, y) => Gadgets.and(x, y, length)
+  );
 });
 
 test(
@@ -71,14 +81,29 @@ await equivalentAsync(
   (x, y) => {
     if (x >= 2n ** 64n || y >= 2n ** 64n)
       throw Error('Does not fit into 64 bits');
-    return Fp.xor(x, y);
+    return x ^ y;
   },
   async (x, y) => {
     let proof = await Bitwise.xor(x, y);
     return proof.publicOutput;
   }
 );
 
+await equivalentAsync(
+  { from: [maybeUint64, maybeUint64], to: field },
+  { runs: 3 }
+)(
+  (x, y) => {
+    if (x >= 2n ** 64n || y >= 2n ** 64n)
+      throw Error('Does not fit into 64 bits');
+    return x & y;
+  },
+  async (x, y) => {
+    let proof = await Bitwise.and(x, y);
+    return proof.publicOutput;
+  }
+);
+
 await equivalentAsync({ from: [field], to: field }, { runs: 3 })(
   (x) => {
     if (x >= 2n ** 64n) throw Error('Does not fit into 64 bits');

src/lib/gadgets/gadgets.ts

@@ -2,7 +2,7 @@
  * Wrapper file for various gadgets, with a namespace and doccomments.
  */
 import { rangeCheck64 } from './range-check.js';
-import { xor, rotate } from './bitwise.js';
+import { rotate, xor, and } from './bitwise.js';
 import { Field } from '../core.js';
 
 export { Gadgets };
@@ -34,7 +34,6 @@ const Gadgets = {
   rangeCheck64(x: Field) {
     return rangeCheck64(x);
   },
-
   /**
    * A (left and right) rotation operates similarly to the shift operation (`<<` for left and `>>` for right) in JavaScript,
    * with the distinction that the bits are circulated to the opposite end of a 64-bit representation rather than being discarded.
@@ -72,7 +71,6 @@ const Gadgets = {
   rotate(field: Field, bits: number, direction: 'left' | 'right' = 'left') {
     return rotate(field, bits, direction);
   },
-
   /**
    * Bitwise XOR gadget on {@link Field} elements. Equivalent to the [bitwise XOR `^` operator in JavaScript](https://developer.mozilla.org/en-US/docs/Web/JavaScript/Reference/Operators/Bitwise_XOR).
    * A XOR gate works by comparing two bits and returning `1` if two bits differ, and `0` if two bits are equal.
@@ -108,4 +106,37 @@ const Gadgets = {
   xor(a: Field, b: Field, length: number) {
     return xor(a, b, length);
   },
+  /**
+   * Bitwise AND gadget on {@link Field} elements. Equivalent to the [bitwise AND `&` operator in JavaScript](https://developer.mozilla.org/en-US/docs/Web/JavaScript/Reference/Operators/Bitwise_AND).
+   * The AND gate works by comparing two bits and returning `1` if both bits are `1`, and `0` otherwise.
+   *
+   * It can be checked by a double generic gate that verifies the following relationship between the values below (in the process it also invokes the {@link Gadgets.xor} gadget which will create additional constraints depending on `length`).
+   *
+   * The generic gate verifies:\
+   * `a + b = sum` and the conjunction equation `2 * and = sum - xor`\
+   * Where:\
+   * `a + b = sum`\
+   * `a ^ b = xor`\
+   * `a & b = and`
+   *
+   * You can find more details about the implementation in the [Mina book](https://o1-labs.github.io/proof-systems/specs/kimchi.html?highlight=gates#and)
+   *
+   * The `length` parameter lets you define how many bits should be compared. `length` is rounded to the nearest multiple of 16, `paddedLength = ceil(length / 16) * 16`, and both input values are constrained to fit into `paddedLength` bits. The output is guaranteed to have at most `paddedLength` bits as well.
+   *
+   * **Note:** Specifying a larger `length` parameter adds additional constraints.
+   *
+   * **Note:** Both {@link Field} elements need to fit into `2^paddedLength - 1`. Otherwise, an error is thrown and no proof can be generated.
+   * For example, with `length = 2` (`paddedLength = 16`), `and()` will fail for any input that is larger than `2**16`.
+   *
+   * ```typescript
+   * let a = Field(3);    // ... 000011
+   * let b = Field(5);    // ... 000101
+   *
+   * let c = and(a, b, 2);    // ... 000001
+   * c.assertEquals(1);
+   * ```
+   */
+  and(a: Field, b: Field, length: number) {
+    return and(a, b, length);
+  },
 };

src/lib/gates.ts

@@ -2,7 +2,7 @@ import { Snarky } from '../snarky.js';
 import { FieldVar, FieldConst, type Field } from './field.js';
 import { MlArray } from './ml/base.js';
 
-export { rangeCheck64, xor, zero, rotate };
+export { rangeCheck64, xor, zero, rotate, generic };
 
 /**
  * Asserts that x is at most 64 bits
@@ -100,6 +100,39 @@ function xor(
   );
 }
 
+/**
+ * [Generic gate](https://o1-labs.github.io/proof-systems/specs/kimchi.html?highlight=foreignfield#double-generic-gate)
+ * The vanilla PLONK gate that allows us to do operations like:
+ * * addition of two registers (into an output register)
+ * * multiplication of two registers
+ * * equality of a register with a constant
+ *
+ * More generally, the generic gate controls the coefficients (denoted `c_`) in the equation:
+ *
+ * `c_l*l + c_r*r + c_o*o + c_m*l*r + c_c === 0`
+ */
+function generic(
+  coefficients: {
+    left: bigint;
+    right: bigint;
+    out: bigint;
+    mul: bigint;
+    const: bigint;
+  },
+  inputs: { left: Field; right: Field; out: Field }
+) {
+  Snarky.gates.generic(
+    FieldConst.fromBigint(coefficients.left),
+    inputs.left.value,
+    FieldConst.fromBigint(coefficients.right),
+    inputs.right.value,
+    FieldConst.fromBigint(coefficients.out),
+    inputs.out.value,
+    FieldConst.fromBigint(coefficients.mul),
+    FieldConst.fromBigint(coefficients.const)
+  );
+}
+
 function zero(a: Field, b: Field, c: Field) {
   Snarky.gates.zero(a.value, b.value, c.value);
 }

src/snarky.d.ts

@@ -348,6 +348,17 @@ declare const Snarky: {
     ): void;
 
     zero(in1: FieldVar, in2: FieldVar, out: FieldVar): void;
+
+    generic(
+      sl: FieldConst,
+      l: FieldVar,
+      sr: FieldConst,
+      r: FieldVar,
+      so: FieldConst,
+      o: FieldVar,
+      sm: FieldConst,
+      sc: FieldConst
+    ): void;
   };
 
   bool: {