From 959cac27f70140c444431b4dc2e93933f4f22ca9 Mon Sep 17 00:00:00 2001
From: Gregor Mitscha-Baude <gregor.mitscha-baude@gmx.at>
Date: Thu, 2 Nov 2023 22:43:04 +0100
Subject: [PATCH 01/34] ffmul gate wrapper

---
 src/lib/gates.ts | 46 ++++++++++++++++++++++++++++++++++++++++++++++
 1 file changed, 46 insertions(+)

diff --git a/src/lib/gates.ts b/src/lib/gates.ts
index d0be6abf1..e18ad6e2d 100644
--- a/src/lib/gates.ts
+++ b/src/lib/gates.ts
@@ -12,6 +12,7 @@ export {
   rotate,
   generic,
   foreignFieldAdd,
+  foreignFieldMul,
 };
 
 const Gates = {
@@ -184,3 +185,48 @@ function foreignFieldAdd({
     FieldConst.fromBigint(sign)
   );
 }
+
+/**
+ * Foreign field multiplication
+ */
+function foreignFieldMul(inputs: {
+  left: TupleN<Field, 3>;
+  right: TupleN<Field, 3>;
+  remainder: TupleN<Field, 2>;
+  quotient: TupleN<Field, 3>;
+  quotientHiBound: Field;
+  product1: TupleN<Field, 3>;
+  carry0: Field;
+  carry1p: TupleN<Field, 7>;
+  carry1c: TupleN<Field, 4>;
+  foreignFieldModulus2: bigint;
+  negForeignFieldModulus: TupleN<bigint, 3>;
+}) {
+  let {
+    left,
+    right,
+    remainder,
+    quotient,
+    quotientHiBound,
+    product1,
+    carry0,
+    carry1p,
+    carry1c,
+    foreignFieldModulus2,
+    negForeignFieldModulus,
+  } = inputs;
+
+  Snarky.gates.foreignFieldMul(
+    MlTuple.mapTo(left, (x) => x.value),
+    MlTuple.mapTo(right, (x) => x.value),
+    MlTuple.mapTo(remainder, (x) => x.value),
+    MlTuple.mapTo(quotient, (x) => x.value),
+    quotientHiBound.value,
+    MlTuple.mapTo(product1, (x) => x.value),
+    carry0.value,
+    MlTuple.mapTo(carry1p, (x) => x.value),
+    MlTuple.mapTo(carry1c, (x) => x.value),
+    FieldConst.fromBigint(foreignFieldModulus2),
+    MlTuple.mapTo(negForeignFieldModulus, FieldConst.fromBigint)
+  );
+}

From 7dab788ab5926275178b8d2b7955fbfd10d5c608 Mon Sep 17 00:00:00 2001
From: Gregor Mitscha-Baude <gregor.mitscha-baude@gmx.at>
Date: Thu, 2 Nov 2023 23:51:19 +0100
Subject: [PATCH 02/34] ffmul witnesses

---
 src/lib/gadgets/foreign-field.ts | 78 +++++++++++++++++++++++++++++---
 src/lib/gadgets/range-check.ts   | 20 +++-----
 2 files changed, 79 insertions(+), 19 deletions(-)

diff --git a/src/lib/gadgets/foreign-field.ts b/src/lib/gadgets/foreign-field.ts
index e2dfd5cd1..0dfe5966c 100644
--- a/src/lib/gadgets/foreign-field.ts
+++ b/src/lib/gadgets/foreign-field.ts
@@ -2,8 +2,8 @@ import { mod } from '../../bindings/crypto/finite_field.js';
 import { Field } from '../field.js';
 import { Gates, foreignFieldAdd } from '../gates.js';
 import { Tuple } from '../util/types.js';
-import { assert, exists } from './common.js';
-import { L, lMask, multiRangeCheck, twoL, twoLMask } from './range-check.js';
+import { assert, bitSlice, exists } from './common.js';
+import { L, lMask, multiRangeCheck, L2, l2Mask, L3 } from './range-check.js';
 
 export { ForeignField, Field3, Sign };
 
@@ -84,8 +84,8 @@ function singleAdd(x: Field3, y: Field3, sign: Sign, f: bigint) {
     // do the add with carry
     // note: this "just works" with negative r01
     let r01 = collapse2(x_) + sign * collapse2(y_) - overflow * collapse2(f_);
-    let carry = r01 >> twoL;
-    r01 &= twoLMask;
+    let carry = r01 >> L2;
+    r01 &= l2Mask;
     let [r0, r1] = split2(r01);
     let r2 = x_[2] + sign * y_[2] - overflow * f_[2] + carry;
 
@@ -97,6 +97,72 @@ function singleAdd(x: Field3, y: Field3, sign: Sign, f: bigint) {
   return { result: [r0, r1, r2] satisfies Field3, overflow };
 }
 
+function multiply(aF: Field3, bF: Field3, f: bigint) {
+  // notation follows https://github.com/o1-labs/rfcs/blob/main/0006-ffmul-revised.md
+  let f_ = (1n << L3) - f;
+  let [f_0, f_1, f_2] = split(f_);
+
+  let witnesses = exists(27, () => {
+    // split inputs into 3 limbs
+    let [a0, a1, a2] = bigint3(aF);
+    let [b0, b1, b2] = bigint3(bF);
+    let a = collapse([a0, a1, a2]);
+    let b = collapse([b0, b1, b2]);
+
+    // compute q and r such that a*b = q*f + r
+    let ab = a * b;
+    let q = ab / f;
+    let r = ab - q * f;
+
+    let [q0, q1, q2] = split(q);
+    let [r0, r1, r2] = split(r);
+    let r01 = collapse2([r0, r1]);
+
+    // compute product terms
+    let p0 = a0 * b0 + q0 * f_0;
+    let p1 = a0 * b1 + a1 * b0 + q0 * f_1 + q1 * f_0;
+    let p2 = a0 * b2 + a1 * b1 + a2 * b0 + q0 * f_2 + q1 * f_1 + q2 * f_0;
+
+    let [p10, p110, p111] = split(p1);
+    let p11 = collapse2([p110, p111]);
+
+    // carry bottom limbs
+    let c0 = (p0 + (p10 << L) - r01) >> L2;
+
+    // carry top limb
+    let c1 = (p2 - r2 + p11 + c0) >> L;
+
+    // split high carry
+    let c1_00 = bitSlice(c1, 0, 12);
+    let c1_12 = bitSlice(c1, 12, 12);
+    let c1_24 = bitSlice(c1, 24, 12);
+    let c1_36 = bitSlice(c1, 36, 12);
+    let c1_48 = bitSlice(c1, 48, 12);
+    let c1_60 = bitSlice(c1, 60, 12);
+    let c1_72 = bitSlice(c1, 72, 12);
+    let c1_84 = bitSlice(c1, 84, 2);
+    let c1_86 = bitSlice(c1, 86, 2);
+    let c1_88 = bitSlice(c1, 88, 2);
+    let c1_90 = bitSlice(c1, 90, 1);
+
+    // quotient high bound
+    let q2Bound = q2 + (1n << L) - (f >> L2) - 1n;
+
+    // prettier-ignore
+    return [
+      a0, a1, a2,
+      b0, b1, b2,
+      r01, r2,
+      q0, q1, q2,
+      q2Bound,
+      p10, p110, p111,
+      c0,
+      c1_00, c1_12, c1_24, c1_36, c1_48, c1_60, c1_72,
+      c1_84, c1_86, c1_88, c1_90,
+    ];
+  });
+}
+
 function Field3(x: bigint3): Field3 {
   return Tuple.map(x, (x) => new Field(x));
 }
@@ -105,10 +171,10 @@ function bigint3(x: Field3): bigint3 {
 }
 
 function collapse([x0, x1, x2]: bigint3) {
-  return x0 + (x1 << L) + (x2 << twoL);
+  return x0 + (x1 << L) + (x2 << L2);
 }
 function split(x: bigint): bigint3 {
-  return [x & lMask, (x >> L) & lMask, (x >> twoL) & lMask];
+  return [x & lMask, (x >> L) & lMask, (x >> L2) & lMask];
 }
 
 function collapse2([x0, x1]: bigint3 | [bigint, bigint]) {
diff --git a/src/lib/gadgets/range-check.ts b/src/lib/gadgets/range-check.ts
index 756388d24..8e57bde4b 100644
--- a/src/lib/gadgets/range-check.ts
+++ b/src/lib/gadgets/range-check.ts
@@ -2,15 +2,8 @@ import { Field } from '../field.js';
 import { Gates } from '../gates.js';
 import { bitSlice, exists } from './common.js';
 
-export {
-  rangeCheck64,
-  multiRangeCheck,
-  compactMultiRangeCheck,
-  L,
-  twoL,
-  lMask,
-  twoLMask,
-};
+export { rangeCheck64, multiRangeCheck, compactMultiRangeCheck };
+export { L, L2, L3, lMask, l2Mask };
 
 /**
  * Asserts that x is in the range [0, 2^64)
@@ -59,9 +52,10 @@ function rangeCheck64(x: Field) {
 
 // default bigint limb size
 const L = 88n;
-const twoL = 2n * L;
+const L2 = 2n * L;
+const L3 = 3n * L;
 const lMask = (1n << L) - 1n;
-const twoLMask = (1n << twoL) - 1n;
+const l2Mask = (1n << L2) - 1n;
 
 /**
  * Asserts that x, y, z \in [0, 2^88)
@@ -89,9 +83,9 @@ function multiRangeCheck(x: Field, y: Field, z: Field) {
 function compactMultiRangeCheck(xy: Field, z: Field): [Field, Field, Field] {
   // constant case
   if (xy.isConstant() && z.isConstant()) {
-    if (xy.toBigInt() >> twoL || z.toBigInt() >> L) {
+    if (xy.toBigInt() >> L2 || z.toBigInt() >> L) {
       throw Error(
-        `Expected fields to fit in ${twoL} and ${L} bits respectively, got ${xy}, ${z}`
+        `Expected fields to fit in ${L2} and ${L} bits respectively, got ${xy}, ${z}`
       );
     }
     let [x, y] = splitCompactLimb(xy.toBigInt());

From 99628cb01d0515805943ad71aacfbec4f117bc10 Mon Sep 17 00:00:00 2001
From: Gregor Mitscha-Baude <gregor.mitscha-baude@gmx.at>
Date: Fri, 3 Nov 2023 00:29:10 +0100
Subject: [PATCH 03/34] raw gate wrapper

---
 src/lib/gates.ts | 12 +++++++++++-
 src/snarky.d.ts  |  1 +
 2 files changed, 12 insertions(+), 1 deletion(-)

diff --git a/src/lib/gates.ts b/src/lib/gates.ts
index e18ad6e2d..5d620066c 100644
--- a/src/lib/gates.ts
+++ b/src/lib/gates.ts
@@ -1,4 +1,4 @@
-import { Snarky } from '../snarky.js';
+import { KimchiGateType, Snarky } from '../snarky.js';
 import { FieldConst, type Field } from './field.js';
 import { MlArray, MlTuple } from './ml/base.js';
 import { TupleN } from './util/types.js';
@@ -23,6 +23,8 @@ const Gates = {
   rotate,
   generic,
   foreignFieldAdd,
+  foreignFieldMul,
+  raw,
 };
 
 function rangeCheck0(
@@ -230,3 +232,11 @@ function foreignFieldMul(inputs: {
     MlTuple.mapTo(negForeignFieldModulus, FieldConst.fromBigint)
   );
 }
+
+function raw(kind: KimchiGateType, values: Field[], coefficients: bigint[]) {
+  Snarky.gates.raw(
+    kind,
+    MlArray.to(values.map((x) => x.value)),
+    MlArray.to(coefficients.map(FieldConst.fromBigint))
+  );
+}
diff --git a/src/snarky.d.ts b/src/snarky.d.ts
index 0408c637d..69fe3bcb3 100644
--- a/src/snarky.d.ts
+++ b/src/snarky.d.ts
@@ -33,6 +33,7 @@ export {
   Snarky,
   Test,
   JsonGate,
+  KimchiGateType,
   MlPublicKey,
   MlPublicKeyVar,
   FeatureFlags,

From 409c73ab64d4f76f9ffca2a23ab5ac20a5471ce8 Mon Sep 17 00:00:00 2001
From: Gregor Mitscha-Baude <gregor.mitscha-baude@gmx.at>
Date: Fri, 3 Nov 2023 00:29:51 +0100
Subject: [PATCH 04/34] ffmul constraints

---
 src/lib/gadgets/foreign-field.ts | 76 +++++++++++++++++++++++++++-----
 1 file changed, 65 insertions(+), 11 deletions(-)

diff --git a/src/lib/gadgets/foreign-field.ts b/src/lib/gadgets/foreign-field.ts
index 0dfe5966c..00b3cd594 100644
--- a/src/lib/gadgets/foreign-field.ts
+++ b/src/lib/gadgets/foreign-field.ts
@@ -3,7 +3,15 @@ import { Field } from '../field.js';
 import { Gates, foreignFieldAdd } from '../gates.js';
 import { Tuple } from '../util/types.js';
 import { assert, bitSlice, exists } from './common.js';
-import { L, lMask, multiRangeCheck, L2, l2Mask, L3 } from './range-check.js';
+import {
+  L,
+  lMask,
+  multiRangeCheck,
+  L2,
+  l2Mask,
+  L3,
+  compactMultiRangeCheck,
+} from './range-check.js';
 
 export { ForeignField, Field3, Sign };
 
@@ -21,6 +29,10 @@ const ForeignField = {
   },
   sumChain,
 
+  mul(x: Field3, y: Field3, f: bigint) {
+    return multiply(x, y, f);
+  },
+
   // helper methods
   from(x: bigint): Field3 {
     return Field3(split(x));
@@ -97,20 +109,21 @@ function singleAdd(x: Field3, y: Field3, sign: Sign, f: bigint) {
   return { result: [r0, r1, r2] satisfies Field3, overflow };
 }
 
-function multiply(aF: Field3, bF: Field3, f: bigint) {
+function multiply(a: Field3, b: Field3, f: bigint) {
   // notation follows https://github.com/o1-labs/rfcs/blob/main/0006-ffmul-revised.md
+  assert(f < 1n << 259n, 'Foreign modulus fits in 259 bits');
   let f_ = (1n << L3) - f;
   let [f_0, f_1, f_2] = split(f_);
+  let f2 = f >> L2;
+  let f2Bound = (1n << L) - f2 - 1n;
 
-  let witnesses = exists(27, () => {
+  let witnesses = exists(21, () => {
     // split inputs into 3 limbs
-    let [a0, a1, a2] = bigint3(aF);
-    let [b0, b1, b2] = bigint3(bF);
-    let a = collapse([a0, a1, a2]);
-    let b = collapse([b0, b1, b2]);
+    let [a0, a1, a2] = bigint3(a);
+    let [b0, b1, b2] = bigint3(b);
 
     // compute q and r such that a*b = q*f + r
-    let ab = a * b;
+    let ab = collapse([a0, a1, a2]) * collapse([b0, b1, b2]);
     let q = ab / f;
     let r = ab - q * f;
 
@@ -146,12 +159,10 @@ function multiply(aF: Field3, bF: Field3, f: bigint) {
     let c1_90 = bitSlice(c1, 90, 1);
 
     // quotient high bound
-    let q2Bound = q2 + (1n << L) - (f >> L2) - 1n;
+    let q2Bound = q2 + f2Bound;
 
     // prettier-ignore
     return [
-      a0, a1, a2,
-      b0, b1, b2,
       r01, r2,
       q0, q1, q2,
       q2Bound,
@@ -161,6 +172,49 @@ function multiply(aF: Field3, bF: Field3, f: bigint) {
       c1_84, c1_86, c1_88, c1_90,
     ];
   });
+
+  // prettier-ignore
+  let [
+    r01, r2,
+    q0, q1, q2,
+    q2Bound,
+    p10, p110, p111,
+    c0,
+    c1_00, c1_12, c1_24, c1_36, c1_48, c1_60, c1_72,
+    c1_84, c1_86, c1_88, c1_90,
+  ] = witnesses;
+
+  let q: Field3 = [q0, q1, q2];
+
+  // ffmul gate. this already adds the following zero row.
+  Gates.foreignFieldMul({
+    left: a,
+    right: b,
+    remainder: [r01, r2],
+    quotient: q,
+    quotientHiBound: q2Bound,
+    product1: [p10, p110, p111],
+    carry0: c0,
+    carry1p: [c1_00, c1_12, c1_24, c1_36, c1_48, c1_60, c1_72],
+    carry1c: [c1_84, c1_86, c1_88, c1_90],
+    foreignFieldModulus2: f2,
+    negForeignFieldModulus: [f_0, f_1, f_2],
+  });
+
+  // limb range checks on quotient and remainder
+  multiRangeCheck(...q);
+  let r = compactMultiRangeCheck(r01, r2);
+
+  // range check on q and r bounds
+  // TODO: this uses one RC too many.. need global RC stack
+  let [r2Bound, zero] = exists(2, () => [r2.toBigInt() + f2Bound, 0n]);
+  multiRangeCheck(q2Bound, r2Bound, zero);
+
+  // constrain r2 bound, zero
+  r2.add(f2Bound).assertEquals(r2Bound);
+  zero.assertEquals(0);
+
+  return [r, q] satisfies [Field3, Field3];
 }
 
 function Field3(x: bigint3): Field3 {

From 8f585772c0ee59698698e6368253e7aa8ac2fab4 Mon Sep 17 00:00:00 2001
From: Gregor Mitscha-Baude <gregor.mitscha-baude@gmx.at>
Date: Fri, 3 Nov 2023 00:39:26 +0100
Subject: [PATCH 05/34] constant case

---
 src/lib/gadgets/foreign-field.ts | 12 ++++++++++--
 1 file changed, 10 insertions(+), 2 deletions(-)

diff --git a/src/lib/gadgets/foreign-field.ts b/src/lib/gadgets/foreign-field.ts
index 00b3cd594..d9052def2 100644
--- a/src/lib/gadgets/foreign-field.ts
+++ b/src/lib/gadgets/foreign-field.ts
@@ -109,7 +109,7 @@ function singleAdd(x: Field3, y: Field3, sign: Sign, f: bigint) {
   return { result: [r0, r1, r2] satisfies Field3, overflow };
 }
 
-function multiply(a: Field3, b: Field3, f: bigint) {
+function multiply(a: Field3, b: Field3, f: bigint): [Field3, Field3] {
   // notation follows https://github.com/o1-labs/rfcs/blob/main/0006-ffmul-revised.md
   assert(f < 1n << 259n, 'Foreign modulus fits in 259 bits');
   let f_ = (1n << L3) - f;
@@ -117,6 +117,14 @@ function multiply(a: Field3, b: Field3, f: bigint) {
   let f2 = f >> L2;
   let f2Bound = (1n << L) - f2 - 1n;
 
+  // constant case
+  if (a.every((x) => x.isConstant()) && b.every((x) => x.isConstant())) {
+    let ab = ForeignField.toBigint(a) * ForeignField.toBigint(b);
+    let q = ab / f;
+    let r = ab - q * f;
+    return [ForeignField.from(r), ForeignField.from(q)];
+  }
+
   let witnesses = exists(21, () => {
     // split inputs into 3 limbs
     let [a0, a1, a2] = bigint3(a);
@@ -214,7 +222,7 @@ function multiply(a: Field3, b: Field3, f: bigint) {
   r2.add(f2Bound).assertEquals(r2Bound);
   zero.assertEquals(0);
 
-  return [r, q] satisfies [Field3, Field3];
+  return [r, q];
 }
 
 function Field3(x: bigint3): Field3 {

From 283fbd6c86178511e99c1c80dd2fc339380b63a0 Mon Sep 17 00:00:00 2001
From: Gregor Mitscha-Baude <gregor.mitscha-baude@gmx.at>
Date: Fri, 3 Nov 2023 00:39:38 +0100
Subject: [PATCH 06/34] start testing

---
 src/lib/gadgets/foreign-field.unit-test.ts | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/lib/gadgets/foreign-field.unit-test.ts b/src/lib/gadgets/foreign-field.unit-test.ts
index 0c173c835..baac7ca8e 100644
--- a/src/lib/gadgets/foreign-field.unit-test.ts
+++ b/src/lib/gadgets/foreign-field.unit-test.ts
@@ -50,6 +50,7 @@ for (let F of fields) {
 
   eq2(F.add, (x, y) => ForeignField.add(x, y, F.modulus), 'add');
   eq2(F.sub, (x, y) => ForeignField.sub(x, y, F.modulus), 'sub');
+  eq2(F.mul, (x, y) => ForeignField.mul(x, y, F.modulus)[0], 'mul');
 
   // sumchain of 5
   equivalentProvable({ from: [array(f, 5), array(sign, 4)], to: f })(

From fb28f8801cc080d435c2b077eb02dc63141cd73f Mon Sep 17 00:00:00 2001
From: Gregor <gregor.mitscha-baude@gmx.at>
Date: Fri, 3 Nov 2023 08:55:23 +0100
Subject: [PATCH 07/34] another small witness test

---
 src/lib/gadgets/foreign-field.unit-test.ts | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

diff --git a/src/lib/gadgets/foreign-field.unit-test.ts b/src/lib/gadgets/foreign-field.unit-test.ts
index baac7ca8e..13b548ad0 100644
--- a/src/lib/gadgets/foreign-field.unit-test.ts
+++ b/src/lib/gadgets/foreign-field.unit-test.ts
@@ -51,6 +51,11 @@ for (let F of fields) {
   eq2(F.add, (x, y) => ForeignField.add(x, y, F.modulus), 'add');
   eq2(F.sub, (x, y) => ForeignField.sub(x, y, F.modulus), 'sub');
   eq2(F.mul, (x, y) => ForeignField.mul(x, y, F.modulus)[0], 'mul');
+  eq2(
+    (x, y) => (x * y) / F.modulus,
+    (x, y) => ForeignField.mul(x, y, F.modulus)[1],
+    'mul quotient'
+  );
 
   // sumchain of 5
   equivalentProvable({ from: [array(f, 5), array(sign, 4)], to: f })(
@@ -99,7 +104,7 @@ let ffProgram = ZkProgram({
 
 await ffProgram.compile();
 
-await equivalentAsync({ from: [array(f, chainLength)], to: f }, { runs: 5 })(
+await equivalentAsync({ from: [array(f, chainLength)], to: f }, { runs: 0 })(
   (xs) => sumchain(xs, signs, F),
   async (xs) => {
     let proof = await ffProgram.sumchain(xs);

From ee17ca3acebc0a1cc044afd7cb3e7a741589f8a0 Mon Sep 17 00:00:00 2001
From: Gregor <gregor.mitscha-baude@gmx.at>
Date: Fri, 3 Nov 2023 09:58:48 +0100
Subject: [PATCH 08/34] add proof mul test which doesn't work

---
 src/lib/gadgets/foreign-field.unit-test.ts | 24 +++++++++++++++++++++-
 1 file changed, 23 insertions(+), 1 deletion(-)

diff --git a/src/lib/gadgets/foreign-field.unit-test.ts b/src/lib/gadgets/foreign-field.unit-test.ts
index 13b548ad0..69cce1418 100644
--- a/src/lib/gadgets/foreign-field.unit-test.ts
+++ b/src/lib/gadgets/foreign-field.unit-test.ts
@@ -99,12 +99,24 @@ let ffProgram = ZkProgram({
         return ForeignField.sumChain(xs, signs, F.modulus);
       },
     },
+
+    mul: {
+      privateInputs: [Field3_, Field3_],
+      method(x, y) {
+        let [r, _q] = ForeignField.mul(x, y, F.modulus);
+        return r;
+      },
+    },
   },
 });
 
 await ffProgram.compile();
 
-await equivalentAsync({ from: [array(f, chainLength)], to: f }, { runs: 0 })(
+await equivalentAsync(
+  { from: [array(f, chainLength)], to: f },
+  // TODO revert to 3 runs
+  { runs: 0 }
+)(
   (xs) => sumchain(xs, signs, F),
   async (xs) => {
     let proof = await ffProgram.sumchain(xs);
@@ -114,6 +126,16 @@ await equivalentAsync({ from: [array(f, chainLength)], to: f }, { runs: 0 })(
   'prove chain'
 );
 
+await equivalentAsync({ from: [f, f], to: f }, { runs: 10 })(
+  F.mul,
+  async (x, y) => {
+    let proof = await ffProgram.mul(x, y);
+    assert(await ffProgram.verify(proof), 'verifies');
+    return proof.publicOutput;
+  },
+  'prove mul'
+);
+
 // helper
 
 function sumchain(xs: bigint[], signs: (1n | -1n)[], F: FiniteField) {

From cff7732ff93d72ac05fa7926274ae4959b546d98 Mon Sep 17 00:00:00 2001
From: Gregor <gregor.mitscha-baude@gmx.at>
Date: Fri, 3 Nov 2023 15:40:05 +0100
Subject: [PATCH 09/34] revert test to normal

---
 src/lib/gadgets/foreign-field.unit-test.ts | 8 ++------
 1 file changed, 2 insertions(+), 6 deletions(-)

diff --git a/src/lib/gadgets/foreign-field.unit-test.ts b/src/lib/gadgets/foreign-field.unit-test.ts
index 69cce1418..d62235d41 100644
--- a/src/lib/gadgets/foreign-field.unit-test.ts
+++ b/src/lib/gadgets/foreign-field.unit-test.ts
@@ -112,11 +112,7 @@ let ffProgram = ZkProgram({
 
 await ffProgram.compile();
 
-await equivalentAsync(
-  { from: [array(f, chainLength)], to: f },
-  // TODO revert to 3 runs
-  { runs: 0 }
-)(
+await equivalentAsync({ from: [array(f, chainLength)], to: f }, { runs: 3 })(
   (xs) => sumchain(xs, signs, F),
   async (xs) => {
     let proof = await ffProgram.sumchain(xs);
@@ -126,7 +122,7 @@ await equivalentAsync(
   'prove chain'
 );
 
-await equivalentAsync({ from: [f, f], to: f }, { runs: 10 })(
+await equivalentAsync({ from: [f, f], to: f }, { runs: 3 })(
   F.mul,
   async (x, y) => {
     let proof = await ffProgram.mul(x, y);

From b6bdf13b6df93c89d5d7cadd1623a191bb95d9a7 Mon Sep 17 00:00:00 2001
From: Gregor Mitscha-Baude <gregor.mitscha-baude@gmx.at>
Date: Fri, 10 Nov 2023 01:34:49 +0100
Subject: [PATCH 10/34] refactor  common mul logic into function

---
 src/lib/gadgets/foreign-field.ts | 57 ++++++++++++++++++++------------
 1 file changed, 36 insertions(+), 21 deletions(-)

diff --git a/src/lib/gadgets/foreign-field.ts b/src/lib/gadgets/foreign-field.ts
index d9052def2..e3b15a6bc 100644
--- a/src/lib/gadgets/foreign-field.ts
+++ b/src/lib/gadgets/foreign-field.ts
@@ -13,7 +13,7 @@ import {
   compactMultiRangeCheck,
 } from './range-check.js';
 
-export { ForeignField, Field3, Sign };
+export { ForeignField, Field3, bigint3, Sign };
 
 type Field3 = [Field, Field, Field];
 type bigint3 = [bigint, bigint, bigint];
@@ -110,12 +110,7 @@ function singleAdd(x: Field3, y: Field3, sign: Sign, f: bigint) {
 }
 
 function multiply(a: Field3, b: Field3, f: bigint): [Field3, Field3] {
-  // notation follows https://github.com/o1-labs/rfcs/blob/main/0006-ffmul-revised.md
   assert(f < 1n << 259n, 'Foreign modulus fits in 259 bits');
-  let f_ = (1n << L3) - f;
-  let [f_0, f_1, f_2] = split(f_);
-  let f2 = f >> L2;
-  let f2Bound = (1n << L) - f2 - 1n;
 
   // constant case
   if (a.every((x) => x.isConstant()) && b.every((x) => x.isConstant())) {
@@ -125,6 +120,38 @@ function multiply(a: Field3, b: Field3, f: bigint): [Field3, Field3] {
     return [ForeignField.from(r), ForeignField.from(q)];
   }
 
+  // provable case
+  let {
+    r: [r01, r2],
+    q,
+    q2Bound,
+  } = multiplyNoRangeCheck(a, b, f);
+
+  // limb range checks on quotient and remainder
+  multiRangeCheck(...q);
+  let r = compactMultiRangeCheck(r01, r2);
+
+  // range check on q and r bounds
+  // TODO: this uses one RC too many.. need global RC stack
+  let f2 = f >> L2;
+  let f2Bound = (1n << L) - f2 - 1n;
+  let [r2Bound, zero] = exists(2, () => [r2.toBigInt() + f2Bound, 0n]);
+  multiRangeCheck(q2Bound, r2Bound, zero);
+
+  // constrain r2 bound, zero
+  r2.add(f2Bound).assertEquals(r2Bound);
+  zero.assertEquals(0);
+
+  return [r, q];
+}
+
+function multiplyNoRangeCheck(a: Field3, b: Field3, f: bigint) {
+  // notation follows https://github.com/o1-labs/rfcs/blob/main/0006-ffmul-revised.md
+  let f_ = (1n << L3) - f;
+  let [f_0, f_1, f_2] = split(f_);
+  let f2 = f >> L2;
+  let f2Bound = (1n << L) - f2 - 1n;
+
   let witnesses = exists(21, () => {
     // split inputs into 3 limbs
     let [a0, a1, a2] = bigint3(a);
@@ -193,12 +220,13 @@ function multiply(a: Field3, b: Field3, f: bigint): [Field3, Field3] {
   ] = witnesses;
 
   let q: Field3 = [q0, q1, q2];
+  let r: [Field, Field] = [r01, r2];
 
   // ffmul gate. this already adds the following zero row.
   Gates.foreignFieldMul({
     left: a,
     right: b,
-    remainder: [r01, r2],
+    remainder: r,
     quotient: q,
     quotientHiBound: q2Bound,
     product1: [p10, p110, p111],
@@ -209,20 +237,7 @@ function multiply(a: Field3, b: Field3, f: bigint): [Field3, Field3] {
     negForeignFieldModulus: [f_0, f_1, f_2],
   });
 
-  // limb range checks on quotient and remainder
-  multiRangeCheck(...q);
-  let r = compactMultiRangeCheck(r01, r2);
-
-  // range check on q and r bounds
-  // TODO: this uses one RC too many.. need global RC stack
-  let [r2Bound, zero] = exists(2, () => [r2.toBigInt() + f2Bound, 0n]);
-  multiRangeCheck(q2Bound, r2Bound, zero);
-
-  // constrain r2 bound, zero
-  r2.add(f2Bound).assertEquals(r2Bound);
-  zero.assertEquals(0);
-
-  return [r, q];
+  return { r, q, q2Bound };
 }
 
 function Field3(x: bigint3): Field3 {

From d0f592d863c29c4f566a164758c7c768fe13ca07 Mon Sep 17 00:00:00 2001
From: Gregor Mitscha-Baude <gregor.mitscha-baude@gmx.at>
Date: Fri, 10 Nov 2023 13:04:22 +0100
Subject: [PATCH 11/34] ff inverse

---
 src/lib/gadgets/common.ts        |  2 +-
 src/lib/gadgets/foreign-field.ts | 50 +++++++++++++++++++++++++-------
 2 files changed, 41 insertions(+), 11 deletions(-)

diff --git a/src/lib/gadgets/common.ts b/src/lib/gadgets/common.ts
index 6b97c6016..680d87b19 100644
--- a/src/lib/gadgets/common.ts
+++ b/src/lib/gadgets/common.ts
@@ -27,7 +27,7 @@ function exists<N extends number, C extends () => TupleN<bigint, N>>(
   return TupleN.fromArray(n, vars);
 }
 
-function assert(stmt: boolean, message?: string) {
+function assert(stmt: boolean, message?: string): asserts stmt {
   if (!stmt) {
     throw Error(message ?? 'Assertion failed');
   }
diff --git a/src/lib/gadgets/foreign-field.ts b/src/lib/gadgets/foreign-field.ts
index e3b15a6bc..a2b297268 100644
--- a/src/lib/gadgets/foreign-field.ts
+++ b/src/lib/gadgets/foreign-field.ts
@@ -1,4 +1,7 @@
-import { mod } from '../../bindings/crypto/finite_field.js';
+import {
+  inverse as modInverse,
+  mod,
+} from '../../bindings/crypto/finite_field.js';
 import { Field } from '../field.js';
 import { Gates, foreignFieldAdd } from '../gates.js';
 import { Tuple } from '../util/types.js';
@@ -32,6 +35,9 @@ const ForeignField = {
   mul(x: Field3, y: Field3, f: bigint) {
     return multiply(x, y, f);
   },
+  inv(x: Field3, f: bigint) {
+    return inverse(x, f);
+  },
 
   // helper methods
   from(x: bigint): Field3 {
@@ -121,11 +127,7 @@ function multiply(a: Field3, b: Field3, f: bigint): [Field3, Field3] {
   }
 
   // provable case
-  let {
-    r: [r01, r2],
-    q,
-    q2Bound,
-  } = multiplyNoRangeCheck(a, b, f);
+  let { r01, r2, q, q2Bound } = multiplyNoRangeCheck(a, b, f);
 
   // limb range checks on quotient and remainder
   multiRangeCheck(...q);
@@ -140,11 +142,40 @@ function multiply(a: Field3, b: Field3, f: bigint): [Field3, Field3] {
 
   // constrain r2 bound, zero
   r2.add(f2Bound).assertEquals(r2Bound);
-  zero.assertEquals(0);
+  zero.assertEquals(0n);
 
   return [r, q];
 }
 
+function inverse(x: Field3, f: bigint): Field3 {
+  // constant case
+  if (x.every((x) => x.isConstant())) {
+    let xInv = modInverse(ForeignField.toBigint(x), f);
+    assert(xInv !== undefined, 'inverse exists');
+    return ForeignField.from(xInv);
+  }
+
+  // provable case
+  let xInv = exists(3, () => {
+    let xInv = modInverse(ForeignField.toBigint(x), f);
+    return xInv === undefined ? [0n, 0n, 0n] : split(xInv);
+  });
+  let { r01, r2, q, q2Bound } = multiplyNoRangeCheck(x, xInv, f);
+
+  // range checks on quotient
+  multiRangeCheck(...q);
+  // TODO: this uses one RC too many.. need global RC stack
+  let [zero] = exists(1, () => [0n]);
+  multiRangeCheck(q2Bound, zero, zero);
+  zero.assertEquals(0n);
+
+  // assert r === 1
+  r01.assertEquals(1n);
+  r2.assertEquals(0n);
+
+  return xInv;
+}
+
 function multiplyNoRangeCheck(a: Field3, b: Field3, f: bigint) {
   // notation follows https://github.com/o1-labs/rfcs/blob/main/0006-ffmul-revised.md
   let f_ = (1n << L3) - f;
@@ -220,13 +251,12 @@ function multiplyNoRangeCheck(a: Field3, b: Field3, f: bigint) {
   ] = witnesses;
 
   let q: Field3 = [q0, q1, q2];
-  let r: [Field, Field] = [r01, r2];
 
   // ffmul gate. this already adds the following zero row.
   Gates.foreignFieldMul({
     left: a,
     right: b,
-    remainder: r,
+    remainder: [r01, r2],
     quotient: q,
     quotientHiBound: q2Bound,
     product1: [p10, p110, p111],
@@ -237,7 +267,7 @@ function multiplyNoRangeCheck(a: Field3, b: Field3, f: bigint) {
     negForeignFieldModulus: [f_0, f_1, f_2],
   });
 
-  return { r, q, q2Bound };
+  return { r01, r2, q, q2Bound };
 }
 
 function Field3(x: bigint3): Field3 {

From b403745b6381f0a772bb3711627527d484c2b23d Mon Sep 17 00:00:00 2001
From: Gregor Mitscha-Baude <gregor.mitscha-baude@gmx.at>
Date: Fri, 10 Nov 2023 14:13:25 +0100
Subject: [PATCH 12/34] fix inverse

---
 src/lib/gadgets/foreign-field.ts | 10 +++++++---
 1 file changed, 7 insertions(+), 3 deletions(-)

diff --git a/src/lib/gadgets/foreign-field.ts b/src/lib/gadgets/foreign-field.ts
index a2b297268..a85df1a33 100644
--- a/src/lib/gadgets/foreign-field.ts
+++ b/src/lib/gadgets/foreign-field.ts
@@ -162,11 +162,15 @@ function inverse(x: Field3, f: bigint): Field3 {
   });
   let { r01, r2, q, q2Bound } = multiplyNoRangeCheck(x, xInv, f);
 
-  // range checks on quotient
+  // limb range checks on quotient and inverse
   multiRangeCheck(...q);
+  multiRangeCheck(...xInv);
+  // range check on q and xInv bounds
   // TODO: this uses one RC too many.. need global RC stack
-  let [zero] = exists(1, () => [0n]);
-  multiRangeCheck(q2Bound, zero, zero);
+  let f2 = f >> L2;
+  let f2Bound = (1n << L) - f2 - 1n;
+  let [xInv2Bound, zero] = exists(2, () => [xInv[2].toBigInt() + f2Bound, 0n]);
+  multiRangeCheck(q2Bound, xInv2Bound, zero);
   zero.assertEquals(0n);
 
   // assert r === 1

From f7e2fe404272ddd547d45bfcb5f4ab6633c4ee9c Mon Sep 17 00:00:00 2001
From: Gregor Mitscha-Baude <gregor.mitscha-baude@gmx.at>
Date: Fri, 10 Nov 2023 15:32:02 +0100
Subject: [PATCH 13/34] division

---
 src/lib/gadgets/common.ts        | 26 +++++++++-
 src/lib/gadgets/foreign-field.ts | 85 +++++++++++++++++++++++++-------
 src/lib/gadgets/range-check.ts   |  6 ++-
 3 files changed, 95 insertions(+), 22 deletions(-)

diff --git a/src/lib/gadgets/common.ts b/src/lib/gadgets/common.ts
index 680d87b19..b497ef88d 100644
--- a/src/lib/gadgets/common.ts
+++ b/src/lib/gadgets/common.ts
@@ -1,6 +1,6 @@
 import { Provable } from '../provable.js';
-import { Field, FieldConst } from '../field.js';
-import { TupleN } from '../util/types.js';
+import { Field, FieldConst, FieldType } from '../field.js';
+import { Tuple, TupleN } from '../util/types.js';
 import { Snarky } from '../../snarky.js';
 import { MlArray } from '../ml/base.js';
 
@@ -9,6 +9,9 @@ const MAX_BITS = 64 as const;
 export {
   MAX_BITS,
   exists,
+  toVars,
+  existsOne,
+  toVar,
   assert,
   bitSlice,
   witnessSlice,
@@ -27,6 +30,25 @@ function exists<N extends number, C extends () => TupleN<bigint, N>>(
   return TupleN.fromArray(n, vars);
 }
 
+function toVars<T extends Tuple<Field | bigint>>(
+  fields: T
+): { [k in keyof T]: Field } {
+  return Tuple.map(fields, toVar);
+}
+
+function existsOne(compute: () => bigint) {
+  let varMl = Snarky.existsVar(() => FieldConst.fromBigint(compute()));
+  return new Field(varMl);
+}
+
+function toVar(x: Field | bigint) {
+  // don't change existing vars
+  if (x instanceof Field && x.value[1] === FieldType.Var) return x;
+  let xVar = existsOne(() => Field.from(x).toBigInt());
+  xVar.assertEquals(x);
+  return xVar;
+}
+
 function assert(stmt: boolean, message?: string): asserts stmt {
   if (!stmt) {
     throw Error(message ?? 'Assertion failed');
diff --git a/src/lib/gadgets/foreign-field.ts b/src/lib/gadgets/foreign-field.ts
index a85df1a33..bc9212c0c 100644
--- a/src/lib/gadgets/foreign-field.ts
+++ b/src/lib/gadgets/foreign-field.ts
@@ -4,8 +4,9 @@ import {
 } from '../../bindings/crypto/finite_field.js';
 import { Field } from '../field.js';
 import { Gates, foreignFieldAdd } from '../gates.js';
+import { Provable } from '../provable.js';
 import { Tuple } from '../util/types.js';
-import { assert, bitSlice, exists } from './common.js';
+import { assert, bitSlice, exists, existsOne, toVar } from './common.js';
 import {
   L,
   lMask,
@@ -38,6 +39,9 @@ const ForeignField = {
   inv(x: Field3, f: bigint) {
     return inverse(x, f);
   },
+  div(x: Field3, y: Field3, f: bigint, { allowZeroOverZero = false } = {}) {
+    return divide(x, y, f, allowZeroOverZero);
+  },
 
   // helper methods
   from(x: bigint): Field3 {
@@ -115,15 +119,13 @@ function singleAdd(x: Field3, y: Field3, sign: Sign, f: bigint) {
   return { result: [r0, r1, r2] satisfies Field3, overflow };
 }
 
-function multiply(a: Field3, b: Field3, f: bigint): [Field3, Field3] {
+function multiply(a: Field3, b: Field3, f: bigint): Field3 {
   assert(f < 1n << 259n, 'Foreign modulus fits in 259 bits');
 
   // constant case
   if (a.every((x) => x.isConstant()) && b.every((x) => x.isConstant())) {
     let ab = ForeignField.toBigint(a) * ForeignField.toBigint(b);
-    let q = ab / f;
-    let r = ab - q * f;
-    return [ForeignField.from(r), ForeignField.from(q)];
+    return ForeignField.from(mod(ab, f));
   }
 
   // provable case
@@ -135,19 +137,15 @@ function multiply(a: Field3, b: Field3, f: bigint): [Field3, Field3] {
 
   // range check on q and r bounds
   // TODO: this uses one RC too many.. need global RC stack
-  let f2 = f >> L2;
-  let f2Bound = (1n << L) - f2 - 1n;
-  let [r2Bound, zero] = exists(2, () => [r2.toBigInt() + f2Bound, 0n]);
-  multiRangeCheck(q2Bound, r2Bound, zero);
-
-  // constrain r2 bound, zero
-  r2.add(f2Bound).assertEquals(r2Bound);
-  zero.assertEquals(0n);
+  let r2Bound = weakBound(r2, f);
+  multiRangeCheck(q2Bound, r2Bound, toVar(0n));
 
-  return [r, q];
+  return r;
 }
 
 function inverse(x: Field3, f: bigint): Field3 {
+  assert(f < 1n << 259n, 'Foreign modulus fits in 259 bits');
+
   // constant case
   if (x.every((x) => x.isConstant())) {
     let xInv = modInverse(ForeignField.toBigint(x), f);
@@ -167,11 +165,9 @@ function inverse(x: Field3, f: bigint): Field3 {
   multiRangeCheck(...xInv);
   // range check on q and xInv bounds
   // TODO: this uses one RC too many.. need global RC stack
-  let f2 = f >> L2;
-  let f2Bound = (1n << L) - f2 - 1n;
-  let [xInv2Bound, zero] = exists(2, () => [xInv[2].toBigInt() + f2Bound, 0n]);
-  multiRangeCheck(q2Bound, xInv2Bound, zero);
-  zero.assertEquals(0n);
+  // TODO: make sure that we can just pass non-vars to multiRangeCheck() to get rid of this
+  let xInv2Bound = weakBound(xInv[2], f);
+  multiRangeCheck(q2Bound, xInv2Bound, new Field(0n));
 
   // assert r === 1
   r01.assertEquals(1n);
@@ -180,6 +176,51 @@ function inverse(x: Field3, f: bigint): Field3 {
   return xInv;
 }
 
+function divide(x: Field3, y: Field3, f: bigint, allowZeroOverZero = false) {
+  assert(f < 1n << 259n, 'Foreign modulus fits in 259 bits');
+
+  // constant case
+  if (x.every((x) => x.isConstant()) && y.every((x) => x.isConstant())) {
+    let yInv = modInverse(ForeignField.toBigint(y), f);
+    assert(yInv !== undefined, 'inverse exists');
+    return ForeignField.from(mod(ForeignField.toBigint(x) * yInv, f));
+  }
+
+  // provable case
+  // to show that z = x/y, we prove that z*y = x and y != 0 (the latter avoids the unconstrained 0/0 case)
+  let z = exists(3, () => {
+    let yInv = modInverse(ForeignField.toBigint(y), f);
+    if (yInv === undefined) return [0n, 0n, 0n];
+    return split(mod(ForeignField.toBigint(x) * yInv, f));
+  });
+  let { r01, r2, q, q2Bound } = multiplyNoRangeCheck(z, y, f);
+
+  // limb range checks on quotient and result
+  multiRangeCheck(...q);
+  multiRangeCheck(...z);
+  // range check on q and result bounds
+  let z2Bound = weakBound(z[2], f);
+  multiRangeCheck(q2Bound, z2Bound, new Field(0n));
+
+  // check that r === y
+  // this means we don't have to range check r
+  let y01 = y[0].add(y[1].mul(1n << L));
+  r01.assertEquals(y01);
+  r2.assertEquals(y[2]);
+
+  if (!allowZeroOverZero) {
+    // assert that y != 0 mod f by checking that it doesn't equal 0 or f
+    // this works because we assume y[2] <= f2
+    // TODO is this the most efficient way?
+    y01.equals(0n).and(y[2].equals(0n)).assertFalse();
+    let [f0, f1, f2] = split(f);
+    let f01 = collapse2([f0, f1]);
+    y01.equals(f01).and(y[2].equals(f2)).assertFalse();
+  }
+
+  return z;
+}
+
 function multiplyNoRangeCheck(a: Field3, b: Field3, f: bigint) {
   // notation follows https://github.com/o1-labs/rfcs/blob/main/0006-ffmul-revised.md
   let f_ = (1n << L3) - f;
@@ -274,6 +315,12 @@ function multiplyNoRangeCheck(a: Field3, b: Field3, f: bigint) {
   return { r01, r2, q, q2Bound };
 }
 
+function weakBound(x: Field, f: bigint) {
+  let f2 = f >> L2;
+  let f2Bound = (1n << L) - f2 - 1n;
+  return x.add(f2Bound);
+}
+
 function Field3(x: bigint3): Field3 {
   return Tuple.map(x, (x) => new Field(x));
 }
diff --git a/src/lib/gadgets/range-check.ts b/src/lib/gadgets/range-check.ts
index 8e57bde4b..bdb485afd 100644
--- a/src/lib/gadgets/range-check.ts
+++ b/src/lib/gadgets/range-check.ts
@@ -1,6 +1,6 @@
 import { Field } from '../field.js';
 import { Gates } from '../gates.js';
-import { bitSlice, exists } from './common.js';
+import { bitSlice, exists, toVars } from './common.js';
 
 export { rangeCheck64, multiRangeCheck, compactMultiRangeCheck };
 export { L, L2, L3, lMask, l2Mask };
@@ -67,6 +67,8 @@ function multiRangeCheck(x: Field, y: Field, z: Field) {
     }
     return;
   }
+  // ensure we are using pure variables
+  [x, y, z] = toVars([x, y, z]);
 
   let [x64, x76] = rangeCheck0Helper(x);
   let [y64, y76] = rangeCheck0Helper(y);
@@ -91,6 +93,8 @@ function compactMultiRangeCheck(xy: Field, z: Field): [Field, Field, Field] {
     let [x, y] = splitCompactLimb(xy.toBigInt());
     return [new Field(x), new Field(y), z];
   }
+  // ensure we are using pure variables
+  [xy, z] = toVars([xy, z]);
 
   let [x, y] = exists(2, () => splitCompactLimb(xy.toBigInt()));
 

From 4d8c4e10e5545dd94358ad630bbd43e72441450e Mon Sep 17 00:00:00 2001
From: Gregor Mitscha-Baude <gregor.mitscha-baude@gmx.at>
Date: Fri, 10 Nov 2023 16:41:48 +0100
Subject: [PATCH 14/34] improve zkprogram analyzemethods return

---
 src/lib/proof_system.ts           | 19 ++++++++++++++-----
 src/lib/proof_system.unit-test.ts | 16 +++++++---------
 2 files changed, 21 insertions(+), 14 deletions(-)

diff --git a/src/lib/proof_system.ts b/src/lib/proof_system.ts
index 377daf1a8..390f07337 100644
--- a/src/lib/proof_system.ts
+++ b/src/lib/proof_system.ts
@@ -268,7 +268,9 @@ function ZkProgram<
     >
   ) => Promise<boolean>;
   digest: () => string;
-  analyzeMethods: () => ReturnType<typeof analyzeMethod>[];
+  analyzeMethods: () => {
+    [I in keyof Types]: ReturnType<typeof analyzeMethod>;
+  };
   publicInputType: ProvableOrUndefined<Get<StatementType, 'publicInput'>>;
   publicOutputType: ProvableOrVoid<Get<StatementType, 'publicOutput'>>;
 } & {
@@ -302,9 +304,14 @@ function ZkProgram<
   let maxProofsVerified = getMaxProofsVerified(methodIntfs);
 
   function analyzeMethods() {
-    return methodIntfs.map((methodEntry, i) =>
-      analyzeMethod(publicInputType, methodEntry, methodFunctions[i])
-    );
+    return Object.fromEntries(
+      methodIntfs.map((methodEntry, i) => [
+        methodEntry.methodName,
+        analyzeMethod(publicInputType, methodEntry, methodFunctions[i]),
+      ])
+    ) as any as {
+      [I in keyof Types]: ReturnType<typeof analyzeMethod>;
+    };
   }
 
   let compileOutput:
@@ -318,7 +325,9 @@ function ZkProgram<
     | undefined;
 
   async function compile({ cache = Cache.FileSystemDefault } = {}) {
-    let methodsMeta = analyzeMethods();
+    let methodsMeta = methodIntfs.map((methodEntry, i) =>
+      analyzeMethod(publicInputType, methodEntry, methodFunctions[i])
+    );
     let gates = methodsMeta.map((m) => m.gates);
     let { provers, verify, verificationKey } = await compileProgram({
       publicInputType,
diff --git a/src/lib/proof_system.unit-test.ts b/src/lib/proof_system.unit-test.ts
index 477d35411..b89f1f3dd 100644
--- a/src/lib/proof_system.unit-test.ts
+++ b/src/lib/proof_system.unit-test.ts
@@ -16,14 +16,12 @@ const EmptyProgram = ZkProgram({
 });
 
 const emptyMethodsMetadata = EmptyProgram.analyzeMethods();
-emptyMethodsMetadata.forEach((methodMetadata) => {
-  expect(methodMetadata).toEqual({
-    rows: 0,
-    digest: '4f5ddea76d29cfcfd8c595f14e31f21b',
-    result: undefined,
-    gates: [],
-    publicInputSize: 0,
-  });
+expect(emptyMethodsMetadata.run).toEqual({
+  rows: 0,
+  digest: '4f5ddea76d29cfcfd8c595f14e31f21b',
+  result: undefined,
+  gates: [],
+  publicInputSize: 0,
 });
 
 class CounterPublicInput extends Struct({
@@ -47,5 +45,5 @@ const CounterProgram = ZkProgram({
   },
 });
 
-const incrementMethodMetadata = CounterProgram.analyzeMethods()[0];
+const incrementMethodMetadata = CounterProgram.analyzeMethods().increment;
 expect(incrementMethodMetadata).toEqual(expect.objectContaining({ rows: 18 }));

From ca0f39aa4fe027bd78b763b663512eb6b42d7514 Mon Sep 17 00:00:00 2001
From: Gregor Mitscha-Baude <gregor.mitscha-baude@gmx.at>
Date: Fri, 10 Nov 2023 16:58:41 +0100
Subject: [PATCH 15/34] fix division

---
 src/lib/gadgets/foreign-field.ts | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

diff --git a/src/lib/gadgets/foreign-field.ts b/src/lib/gadgets/foreign-field.ts
index bc9212c0c..8eb5ff437 100644
--- a/src/lib/gadgets/foreign-field.ts
+++ b/src/lib/gadgets/foreign-field.ts
@@ -202,16 +202,17 @@ function divide(x: Field3, y: Field3, f: bigint, allowZeroOverZero = false) {
   let z2Bound = weakBound(z[2], f);
   multiRangeCheck(q2Bound, z2Bound, new Field(0n));
 
-  // check that r === y
+  // check that r === x
   // this means we don't have to range check r
-  let y01 = y[0].add(y[1].mul(1n << L));
-  r01.assertEquals(y01);
-  r2.assertEquals(y[2]);
+  let x01 = x[0].add(x[1].mul(1n << L));
+  r01.assertEquals(x01);
+  r2.assertEquals(x[2]);
 
   if (!allowZeroOverZero) {
     // assert that y != 0 mod f by checking that it doesn't equal 0 or f
     // this works because we assume y[2] <= f2
     // TODO is this the most efficient way?
+    let y01 = y[0].add(y[1].mul(1n << L));
     y01.equals(0n).and(y[2].equals(0n)).assertFalse();
     let [f0, f1, f2] = split(f);
     let f01 = collapse2([f0, f1]);

From 16d8dc4b71ef85c511cbbec169fc26800b3458e8 Mon Sep 17 00:00:00 2001
From: Gregor Mitscha-Baude <gregor.mitscha-baude@gmx.at>
Date: Fri, 10 Nov 2023 16:59:59 +0100
Subject: [PATCH 16/34] test inv and div

---
 src/lib/gadgets/foreign-field.unit-test.ts | 45 +++++++++++++++++++---
 1 file changed, 39 insertions(+), 6 deletions(-)

diff --git a/src/lib/gadgets/foreign-field.unit-test.ts b/src/lib/gadgets/foreign-field.unit-test.ts
index d62235d41..627c7deec 100644
--- a/src/lib/gadgets/foreign-field.unit-test.ts
+++ b/src/lib/gadgets/foreign-field.unit-test.ts
@@ -50,11 +50,15 @@ for (let F of fields) {
 
   eq2(F.add, (x, y) => ForeignField.add(x, y, F.modulus), 'add');
   eq2(F.sub, (x, y) => ForeignField.sub(x, y, F.modulus), 'sub');
-  eq2(F.mul, (x, y) => ForeignField.mul(x, y, F.modulus)[0], 'mul');
+  eq2(F.mul, (x, y) => ForeignField.mul(x, y, F.modulus), 'mul');
+  equivalentProvable({ from: [f], to: f })(
+    (x) => F.inverse(x) ?? throwError('no inverse'),
+    (x) => ForeignField.inv(x, F.modulus)
+  );
   eq2(
-    (x, y) => (x * y) / F.modulus,
-    (x, y) => ForeignField.mul(x, y, F.modulus)[1],
-    'mul quotient'
+    (x, y) => F.div(x, y) ?? throwError('no inverse'),
+    (x, y) => ForeignField.div(x, y, F.modulus),
+    'div'
   );
 
   // sumchain of 5
@@ -103,13 +107,28 @@ let ffProgram = ZkProgram({
     mul: {
       privateInputs: [Field3_, Field3_],
       method(x, y) {
-        let [r, _q] = ForeignField.mul(x, y, F.modulus);
-        return r;
+        return ForeignField.mul(x, y, F.modulus);
+      },
+    },
+
+    inv: {
+      privateInputs: [Field3_],
+      method(x) {
+        return ForeignField.inv(x, F.modulus);
+      },
+    },
+
+    div: {
+      privateInputs: [Field3_, Field3_],
+      method(x, y) {
+        return ForeignField.div(x, y, F.modulus);
       },
     },
   },
 });
 
+// console.log(ffProgram.analyzeMethods());
+
 await ffProgram.compile();
 
 await equivalentAsync({ from: [array(f, chainLength)], to: f }, { runs: 3 })(
@@ -132,6 +151,16 @@ await equivalentAsync({ from: [f, f], to: f }, { runs: 3 })(
   'prove mul'
 );
 
+await equivalentAsync({ from: [f, f], to: f }, { runs: 3 })(
+  (x, y) => F.div(x, y) ?? throwError('no inverse'),
+  async (x, y) => {
+    let proof = await ffProgram.div(x, y);
+    assert(await ffProgram.verify(proof), 'verifies');
+    return proof.publicOutput;
+  },
+  'prove div'
+);
+
 // helper
 
 function sumchain(xs: bigint[], signs: (1n | -1n)[], F: FiniteField) {
@@ -141,3 +170,7 @@ function sumchain(xs: bigint[], signs: (1n | -1n)[], F: FiniteField) {
   }
   return sum;
 }
+
+function throwError<T>(message: string): T {
+  throw Error(message);
+}

From aa8c8f45342cedbbaa6a54e5d029cabf5e1c98bd Mon Sep 17 00:00:00 2001
From: Gregor <gregor.mitscha-baude@gmx.at>
Date: Tue, 14 Nov 2023 16:09:59 +0100
Subject: [PATCH 17/34] minor

---
 src/lib/gadgets/foreign-field.ts | 9 ++++-----
 1 file changed, 4 insertions(+), 5 deletions(-)

diff --git a/src/lib/gadgets/foreign-field.ts b/src/lib/gadgets/foreign-field.ts
index 4a299d3f3..088a38aff 100644
--- a/src/lib/gadgets/foreign-field.ts
+++ b/src/lib/gadgets/foreign-field.ts
@@ -131,9 +131,9 @@ function multiply(a: Field3, b: Field3, f: bigint): Field3 {
   let r = compactMultiRangeCheck(r01, r2);
 
   // range check on q and r bounds
-  // TODO: this uses one RC too many.. need global RC stack
+  // TODO: this uses one RC too many.. need global RC stack, or get rid of bounds checks
   let r2Bound = weakBound(r2, f);
-  multiRangeCheck([q2Bound, r2Bound, toVar(0n)]);
+  multiRangeCheck([q2Bound, r2Bound, Field.from(0n)]);
 
   return r;
 }
@@ -160,9 +160,8 @@ function inverse(x: Field3, f: bigint): Field3 {
   multiRangeCheck(xInv);
   // range check on q and xInv bounds
   // TODO: this uses one RC too many.. need global RC stack
-  // TODO: make sure that we can just pass non-vars to multiRangeCheck() to get rid of this
   let xInv2Bound = weakBound(xInv[2], f);
-  multiRangeCheck([q2Bound, xInv2Bound, new Field(0n)]);
+  multiRangeCheck([q2Bound, xInv2Bound, Field.from(0n)]);
 
   // assert r === 1
   r01.assertEquals(1n);
@@ -195,7 +194,7 @@ function divide(x: Field3, y: Field3, f: bigint, allowZeroOverZero = false) {
   multiRangeCheck(z);
   // range check on q and result bounds
   let z2Bound = weakBound(z[2], f);
-  multiRangeCheck([q2Bound, z2Bound, new Field(0n)]);
+  multiRangeCheck([q2Bound, z2Bound, Field.from(0n)]);
 
   // check that r === x
   // this means we don't have to range check r

From 96f52da15da59586502ffbb0fba2a0ddbde9dad9 Mon Sep 17 00:00:00 2001
From: Gregor <gregor.mitscha-baude@gmx.at>
Date: Tue, 14 Nov 2023 16:11:21 +0100
Subject: [PATCH 18/34] add cs tests for mul

---
 src/lib/gadgets/foreign-field.unit-test.ts | 12 ++++++++++++
 1 file changed, 12 insertions(+)

diff --git a/src/lib/gadgets/foreign-field.unit-test.ts b/src/lib/gadgets/foreign-field.unit-test.ts
index f38167ddb..99529cdbf 100644
--- a/src/lib/gadgets/foreign-field.unit-test.ts
+++ b/src/lib/gadgets/foreign-field.unit-test.ts
@@ -149,6 +149,18 @@ constraintSystem.fromZkProgram(
   )
 );
 
+let mulChain: GateType[] = ['ForeignFieldMul', 'Zero'];
+let mulLayout = ifNotAllConstant(
+  and(
+    contains([mulChain, mrc, mrc, mrc]),
+    withoutGenerics(equals([...mulChain, ...repeat(3, mrc)]))
+  )
+);
+
+constraintSystem.fromZkProgram(ffProgram, 'mul', mulLayout);
+constraintSystem.fromZkProgram(ffProgram, 'inv', mulLayout);
+constraintSystem.fromZkProgram(ffProgram, 'div', mulLayout);
+
 // tests with proving
 
 await ffProgram.compile();

From 3bfdc09880d4917b5cbde90a8c3602b4f619909c Mon Sep 17 00:00:00 2001
From: Gregor Mitscha-Baude <gregor.mitscha-baude@gmx.at>
Date: Wed, 15 Nov 2023 06:26:20 +0100
Subject: [PATCH 19/34] fix: add missing mrc

---
 src/lib/gadgets/foreign-field.ts | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/src/lib/gadgets/foreign-field.ts b/src/lib/gadgets/foreign-field.ts
index 4a299d3f3..d8e6fb770 100644
--- a/src/lib/gadgets/foreign-field.ts
+++ b/src/lib/gadgets/foreign-field.ts
@@ -308,6 +308,9 @@ function multiplyNoRangeCheck(a: Field3, b: Field3, f: bigint) {
     negForeignFieldModulus: [f_0, f_1, f_2],
   });
 
+  // multi-range check on intermediate values
+  multiRangeCheck([c0, p10, p110]);
+
   return { r01, r2, q, q2Bound };
 }
 

From 67d706e16a7095d25e78b5eda17519a8a5040591 Mon Sep 17 00:00:00 2001
From: Gregor Mitscha-Baude <gregor.mitscha-baude@gmx.at>
Date: Wed, 15 Nov 2023 09:34:48 +0100
Subject: [PATCH 20/34] introduce assertmul and use it for inv and div

---
 src/lib/gadgets/foreign-field.ts | 75 ++++++++++++++++++++++----------
 1 file changed, 52 insertions(+), 23 deletions(-)

diff --git a/src/lib/gadgets/foreign-field.ts b/src/lib/gadgets/foreign-field.ts
index d8e6fb770..72b5b724e 100644
--- a/src/lib/gadgets/foreign-field.ts
+++ b/src/lib/gadgets/foreign-field.ts
@@ -153,20 +153,15 @@ function inverse(x: Field3, f: bigint): Field3 {
     let xInv = modInverse(Field3.toBigint(x), f);
     return xInv === undefined ? [0n, 0n, 0n] : split(xInv);
   });
-  let { r01, r2, q, q2Bound } = multiplyNoRangeCheck(x, xInv, f);
-
-  // limb range checks on quotient and inverse
-  multiRangeCheck(q);
   multiRangeCheck(xInv);
-  // range check on q and xInv bounds
-  // TODO: this uses one RC too many.. need global RC stack
-  // TODO: make sure that we can just pass non-vars to multiRangeCheck() to get rid of this
   let xInv2Bound = weakBound(xInv[2], f);
-  multiRangeCheck([q2Bound, xInv2Bound, new Field(0n)]);
 
-  // assert r === 1
-  r01.assertEquals(1n);
-  r2.assertEquals(0n);
+  let one: [Field, Field] = [Field.from(1n), Field.from(0n)];
+  let q2Bound = assertMul(x, xInv, one, f);
+
+  // range check on q and result bounds
+  // TODO: this uses one RC too many.. need global RC stack
+  multiRangeCheck([q2Bound, xInv2Bound, Field.from(0n)]);
 
   return xInv;
 }
@@ -188,20 +183,12 @@ function divide(x: Field3, y: Field3, f: bigint, allowZeroOverZero = false) {
     if (yInv === undefined) return [0n, 0n, 0n];
     return split(mod(Field3.toBigint(x) * yInv, f));
   });
-  let { r01, r2, q, q2Bound } = multiplyNoRangeCheck(z, y, f);
-
-  // limb range checks on quotient and result
-  multiRangeCheck(q);
   multiRangeCheck(z);
-  // range check on q and result bounds
   let z2Bound = weakBound(z[2], f);
-  multiRangeCheck([q2Bound, z2Bound, new Field(0n)]);
+  let q2Bound = assertMul(z, y, x, f);
 
-  // check that r === x
-  // this means we don't have to range check r
-  let x01 = x[0].add(x[1].mul(1n << L));
-  r01.assertEquals(x01);
-  r2.assertEquals(x[2]);
+  // range check on q and result bounds
+  multiRangeCheck([q2Bound, z2Bound, new Field(0n)]);
 
   if (!allowZeroOverZero) {
     // assert that y != 0 mod f by checking that it doesn't equal 0 or f
@@ -217,6 +204,48 @@ function divide(x: Field3, y: Field3, f: bigint, allowZeroOverZero = false) {
   return z;
 }
 
+function assertMul(
+  x: Field3,
+  y: Field3,
+  xy: Field3 | [Field, Field],
+  f: bigint
+) {
+  assert(f < 1n << 259n, 'Foreign modulus fits in 259 bits');
+
+  // constant case
+  if (
+    x.every((x) => x.isConstant()) &&
+    y.every((x) => x.isConstant()) &&
+    xy.every((x) => x.isConstant())
+  ) {
+    let xyExpected = mod(Field3.toBigint(x) * Field3.toBigint(y), f);
+    let xyActual =
+      xy.length === 2
+        ? collapse2(Tuple.map(xy, (x) => x.toBigInt()))
+        : Field3.toBigint(xy);
+    assert(xyExpected === xyActual, 'Expected xy to be x*y mod f');
+    return Field.from(0n);
+  }
+
+  // provable case
+  let { r01, r2, q, q2Bound } = multiplyNoRangeCheck(x, y, f);
+
+  // range check on quotient
+  multiRangeCheck(q);
+
+  // bind remainder to input xy
+  if (xy.length === 2) {
+    let [xy01, xy2] = xy;
+    r01.assertEquals(xy01);
+    r2.assertEquals(xy2);
+  } else {
+    let xy01 = xy[0].add(xy[1].mul(1n << L));
+    r01.assertEquals(xy01);
+    r2.assertEquals(xy[2]);
+  }
+  return q2Bound;
+}
+
 function multiplyNoRangeCheck(a: Field3, b: Field3, f: bigint) {
   // notation follows https://github.com/o1-labs/rfcs/blob/main/0006-ffmul-revised.md
   let f_ = (1n << L3) - f;
@@ -316,7 +345,7 @@ function multiplyNoRangeCheck(a: Field3, b: Field3, f: bigint) {
 
 function weakBound(x: Field, f: bigint) {
   let f2 = f >> L2;
-  let f2Bound = (1n << L) - f2 - 1n;
+  let f2Bound = lMask - f2;
   return x.add(f2Bound);
 }
 

From e1009230315e462bcf4ade2cff72e988a555338d Mon Sep 17 00:00:00 2001
From: Gregor <gregor.mitscha-baude@gmx.at>
Date: Wed, 15 Nov 2023 10:21:24 +0100
Subject: [PATCH 21/34] add ff tests with unreduced inputs

---
 src/lib/gadgets/foreign-field.unit-test.ts | 54 +++++++++++++++++++++-
 1 file changed, 52 insertions(+), 2 deletions(-)

diff --git a/src/lib/gadgets/foreign-field.unit-test.ts b/src/lib/gadgets/foreign-field.unit-test.ts
index 99529cdbf..298e0b4ff 100644
--- a/src/lib/gadgets/foreign-field.unit-test.ts
+++ b/src/lib/gadgets/foreign-field.unit-test.ts
@@ -28,14 +28,32 @@ import { ForeignField as ForeignField_ } from './foreign-field.js';
 const { ForeignField, Field3 } = Gadgets;
 
 function foreignField(F: FiniteField): ProvableSpec<bigint, Gadgets.Field3> {
-  let rng = Random.otherField(F);
   return {
-    rng,
+    rng: Random.otherField(F),
     there: Field3.from,
     back: Field3.toBigint,
     provable: Field3.provable,
   };
 }
+
+// for testing with inputs > f
+function unreducedForeignField(
+  maxBits: number,
+  F: FiniteField
+): ProvableSpec<bigint, Gadgets.Field3> {
+  return {
+    rng: Random.bignat(1n << BigInt(maxBits)),
+    there: Field3.from,
+    back: Field3.toBigint,
+    provable: Field3.provable,
+    assertEqual(x, y, message) {
+      // need weak equality here because, while ffadd works on bigints larger than the modulus,
+      // it can't fully reduce them
+      assert(F.equal(x, y), message);
+    },
+  };
+}
+
 let sign = fromRandom(Random.oneOf(1n as const, -1n as const));
 
 let fields = [
@@ -68,6 +86,38 @@ for (let F of fields) {
     'div'
   );
 
+  // tests with inputs that aren't reduced mod f
+  let big264 = unreducedForeignField(264, F); // this is the max size supported by our range checks / ffadd
+  let big258 = unreducedForeignField(258, F); // rough max size supported by ffmul
+
+  equivalentProvable({ from: [big264, big264], to: big264 })(
+    F.add,
+    (x, y) => ForeignField.add(x, y, F.modulus),
+    'add'
+  );
+  // subtraction doesn't work with unreduced y because the range check on the result prevents x-y < -f
+  equivalentProvable({ from: [big264, f], to: big264 })(
+    F.sub,
+    (x, y) => ForeignField.sub(x, y, F.modulus),
+    'sub'
+  );
+  equivalentProvable({ from: [big258, big258], to: f })(
+    F.mul,
+    (x, y) => ForeignField_.mul(x, y, F.modulus),
+    'mul'
+  );
+  equivalentProvable({ from: [big258], to: f })(
+    (x) => F.inverse(x) ?? throwError('no inverse'),
+    (x) => ForeignField_.inv(x, F.modulus)
+  );
+  // the div() gadget doesn't work with unreduced x because the backwards check (x/y)*y === x fails
+  // and it's not valid with unreduced y because we only assert y != 0, y != f but it can be 2f, 3f, etc.
+  // the combination of inv() and mul() is more flexible (but much more expensive, ~40 vs ~30 constraints)
+  equivalentProvable({ from: [big258, big258], to: f })(
+    (x, y) => F.div(x, y) ?? throwError('no inverse'),
+    (x, y) => ForeignField_.mul(x, ForeignField_.inv(y, F.modulus), F.modulus)
+  );
+
   // sumchain of 5
   equivalentProvable({ from: [array(f, 5), array(sign, 4)], to: f })(
     (xs, signs) => sum(xs, signs, F),

From f40104c8abd478964ac9fe837bc5674ab6350c67 Mon Sep 17 00:00:00 2001
From: Gregor <gregor.mitscha-baude@gmx.at>
Date: Wed, 15 Nov 2023 10:36:12 +0100
Subject: [PATCH 22/34] a bit of clean up

---
 src/lib/gadgets/foreign-field.ts | 29 ++++++++++++-----------------
 1 file changed, 12 insertions(+), 17 deletions(-)

diff --git a/src/lib/gadgets/foreign-field.ts b/src/lib/gadgets/foreign-field.ts
index a12b6ef46..26f6ee868 100644
--- a/src/lib/gadgets/foreign-field.ts
+++ b/src/lib/gadgets/foreign-field.ts
@@ -5,9 +5,8 @@ import {
 import { provableTuple } from '../../bindings/lib/provable-snarky.js';
 import { Field } from '../field.js';
 import { Gates, foreignFieldAdd } from '../gates.js';
-import { Provable } from '../provable.js';
 import { Tuple } from '../util/types.js';
-import { assert, bitSlice, exists, toVars, toVar } from './common.js';
+import { assert, bitSlice, exists, toVars } from './common.js';
 import {
   L,
   lMask,
@@ -156,7 +155,7 @@ function inverse(x: Field3, f: bigint): Field3 {
   multiRangeCheck(xInv);
   let xInv2Bound = weakBound(xInv[2], f);
 
-  let one: [Field, Field] = [Field.from(1n), Field.from(0n)];
+  let one: Field2 = [Field.from(1n), Field.from(0n)];
   let q2Bound = assertMul(x, xInv, one, f);
 
   // range check on q and result bounds
@@ -204,12 +203,7 @@ function divide(x: Field3, y: Field3, f: bigint, allowZeroOverZero = false) {
   return z;
 }
 
-function assertMul(
-  x: Field3,
-  y: Field3,
-  xy: Field3 | [Field, Field],
-  f: bigint
-) {
+function assertMul(x: Field3, y: Field3, xy: Field3 | Field2, f: bigint) {
   assert(f < 1n << 259n, 'Foreign modulus fits in 259 bits');
 
   // constant case
@@ -219,10 +213,7 @@ function assertMul(
     xy.every((x) => x.isConstant())
   ) {
     let xyExpected = mod(Field3.toBigint(x) * Field3.toBigint(y), f);
-    let xyActual =
-      xy.length === 2
-        ? collapse2(Tuple.map(xy, (x) => x.toBigInt()))
-        : Field3.toBigint(xy);
+    let xyActual = xy.length === 2 ? Field2.toBigint(xy) : Field3.toBigint(xy);
     assert(xyExpected === xyActual, 'Expected xy to be x*y mod f');
     return Field.from(0n);
   }
@@ -354,7 +345,7 @@ const Field3 = {
    * Turn a bigint into a 3-tuple of Fields
    */
   from(x: bigint): Field3 {
-    return toField3(split(x));
+    return Tuple.map(split(x), Field.from);
   },
 
   /**
@@ -373,9 +364,13 @@ const Field3 = {
   provable: provableTuple([Field, Field, Field]),
 };
 
-function toField3(x: bigint3): Field3 {
-  return Tuple.map(x, (x) => new Field(x));
-}
+type Field2 = [Field, Field];
+const Field2 = {
+  toBigint(x: Field2): bigint {
+    return collapse2(Tuple.map(x, (x) => x.toBigInt()));
+  },
+};
+
 function bigint3(x: Field3): bigint3 {
   return Tuple.map(x, (x) => x.toBigInt());
 }

From 4f1b21fc01abbfa65f10e212e6f406ec72442436 Mon Sep 17 00:00:00 2001
From: Gregor <gregor.mitscha-baude@gmx.at>
Date: Wed, 15 Nov 2023 10:58:26 +0100
Subject: [PATCH 23/34] remove unused logic

---
 src/lib/gadgets/foreign-field.ts | 15 ---------------
 1 file changed, 15 deletions(-)

diff --git a/src/lib/gadgets/foreign-field.ts b/src/lib/gadgets/foreign-field.ts
index 26f6ee868..5fbade75e 100644
--- a/src/lib/gadgets/foreign-field.ts
+++ b/src/lib/gadgets/foreign-field.ts
@@ -204,21 +204,6 @@ function divide(x: Field3, y: Field3, f: bigint, allowZeroOverZero = false) {
 }
 
 function assertMul(x: Field3, y: Field3, xy: Field3 | Field2, f: bigint) {
-  assert(f < 1n << 259n, 'Foreign modulus fits in 259 bits');
-
-  // constant case
-  if (
-    x.every((x) => x.isConstant()) &&
-    y.every((x) => x.isConstant()) &&
-    xy.every((x) => x.isConstant())
-  ) {
-    let xyExpected = mod(Field3.toBigint(x) * Field3.toBigint(y), f);
-    let xyActual = xy.length === 2 ? Field2.toBigint(xy) : Field3.toBigint(xy);
-    assert(xyExpected === xyActual, 'Expected xy to be x*y mod f');
-    return Field.from(0n);
-  }
-
-  // provable case
   let { r01, r2, q, q2Bound } = multiplyNoRangeCheck(x, y, f);
 
   // range check on quotient

From 4532a2175814941c5c14ca25f7eef4b210c1410a Mon Sep 17 00:00:00 2001
From: Gregor <gregor.mitscha-baude@gmx.at>
Date: Wed, 15 Nov 2023 11:46:15 +0100
Subject: [PATCH 24/34] add to gadgets namespace, mul doccomment

---
 src/lib/gadgets/gadgets.ts | 54 +++++++++++++++++++++++++++++++++++++-
 1 file changed, 53 insertions(+), 1 deletion(-)

diff --git a/src/lib/gadgets/gadgets.ts b/src/lib/gadgets/gadgets.ts
index c7e1208a7..79b1e39e0 100644
--- a/src/lib/gadgets/gadgets.ts
+++ b/src/lib/gadgets/gadgets.ts
@@ -320,7 +320,7 @@ const Gadgets = {
    * A _foreign field_ is a finite field different from the native field of the proof system.
    *
    * The `ForeignField` namespace exposes operations like modular addition and multiplication,
-   * which work for any finite field of size less than 2^256.
+   * which work for any finite field of size less than 2^259.
    *
    * Foreign field elements are represented as 3 limbs of native field elements.
    * Each limb holds 88 bits of the total, in little-endian order.
@@ -412,6 +412,58 @@ const Gadgets = {
     sum(xs: Field3[], signs: (1n | -1n)[], f: bigint) {
       return ForeignField.sum(xs, signs, f);
     },
+
+    /**
+     * Foreign field multiplication: `x * y mod f`
+     *
+     * The modulus `f` does not need to be prime, but has to be smaller than 2^259.
+     *
+     * **Assumptions**: In addition to the assumption that inputs are in the range [0, 2^88), as in all foreign field gadgets,
+     * this assumes an additional bound on the inputs: `x * y < 2^264 * p`, where p is the native modulus.
+     * We usually assert this bound by proving that `x[2] < f[2] + 1`, where `x[2]` is the most significant limb of x.
+     * To do this, use an 88-bit range check on `2^88 - x[2] - (f[2] + 1)`, and same for y.
+     * The implication is that x and y are _almost_ reduced modulo f.
+     *
+     * @example
+     * ```ts
+     * // example modulus: secp256k1 prime
+     * let f = (1n << 256n) - (1n << 32n) - 0b1111010001n;
+     *
+     * let x = Provable.witness(Field3.provable, () => Field3.from(f - 1n));
+     * let y = Provable.witness(Field3.provable, () => Field3.from(f - 2n));
+     *
+     * // range check x, y
+     * Gadgets.multiRangeCheck(x);
+     * Gadgets.multiRangeCheck(y);
+     *
+     * // prove additional bounds
+     * let x2Bound = x[2].add((1n << 88n) - 1n - (f >> 176n));
+     * let y2Bound = y[2].add((1n << 88n) - 1n - (f >> 176n));
+     * Gadgets.multiRangeCheck([x2Bound, y2Bound, Field(0n)]);
+     *
+     * // compute x * y mod f
+     * let z = ForeignField.mul(x, y, f);
+     *
+     * Provable.log(z); // ['2', '0', '0'] = limb representation of 2 = (-1)*(-2) mod f
+     * ```
+     */
+    mul(x: Field3, y: Field3, f: bigint) {
+      return ForeignField.mul(x, y, f);
+    },
+
+    /**
+     * TODO
+     */
+    inv(x: Field3, f: bigint) {
+      return ForeignField.inv(x, f);
+    },
+
+    /**
+     * TODO
+     */
+    div(x: Field3, y: Field3, f: bigint) {
+      return ForeignField.div(x, y, f);
+    },
   },
 
   /**

From 8358f5713db78bdfa4a0f0f6a9d5dfdb4fda04d6 Mon Sep 17 00:00:00 2001
From: Gregor <gregor.mitscha-baude@gmx.at>
Date: Wed, 15 Nov 2023 11:51:10 +0100
Subject: [PATCH 25/34] fix unit tests and code tweak

---
 src/lib/gadgets/foreign-field.ts           | 19 ++++++-------
 src/lib/gadgets/foreign-field.unit-test.ts | 33 +++++++++++++---------
 2 files changed, 28 insertions(+), 24 deletions(-)

diff --git a/src/lib/gadgets/foreign-field.ts b/src/lib/gadgets/foreign-field.ts
index 5fbade75e..30e02e5e0 100644
--- a/src/lib/gadgets/foreign-field.ts
+++ b/src/lib/gadgets/foreign-field.ts
@@ -35,15 +35,9 @@ const ForeignField = {
   },
   sum,
 
-  mul(x: Field3, y: Field3, f: bigint) {
-    return multiply(x, y, f);
-  },
-  inv(x: Field3, f: bigint) {
-    return inverse(x, f);
-  },
-  div(x: Field3, y: Field3, f: bigint, { allowZeroOverZero = false } = {}) {
-    return divide(x, y, f, allowZeroOverZero);
-  },
+  mul: multiply,
+  inv: inverse,
+  div: divide,
 };
 
 /**
@@ -165,7 +159,12 @@ function inverse(x: Field3, f: bigint): Field3 {
   return xInv;
 }
 
-function divide(x: Field3, y: Field3, f: bigint, allowZeroOverZero = false) {
+function divide(
+  x: Field3,
+  y: Field3,
+  f: bigint,
+  { allowZeroOverZero = false } = {}
+) {
   assert(f < 1n << 259n, 'Foreign modulus fits in 259 bits');
 
   // constant case
diff --git a/src/lib/gadgets/foreign-field.unit-test.ts b/src/lib/gadgets/foreign-field.unit-test.ts
index 298e0b4ff..459ee7cde 100644
--- a/src/lib/gadgets/foreign-field.unit-test.ts
+++ b/src/lib/gadgets/foreign-field.unit-test.ts
@@ -23,7 +23,6 @@ import {
   withoutGenerics,
 } from '../testing/constraint-system.js';
 import { GateType } from '../../snarky.js';
-import { ForeignField as ForeignField_ } from './foreign-field.js';
 
 const { ForeignField, Field3 } = Gadgets;
 
@@ -75,14 +74,14 @@ for (let F of fields) {
 
   eq2(F.add, (x, y) => ForeignField.add(x, y, F.modulus), 'add');
   eq2(F.sub, (x, y) => ForeignField.sub(x, y, F.modulus), 'sub');
-  eq2(F.mul, (x, y) => ForeignField_.mul(x, y, F.modulus), 'mul');
+  eq2(F.mul, (x, y) => ForeignField.mul(x, y, F.modulus), 'mul');
   equivalentProvable({ from: [f], to: f })(
     (x) => F.inverse(x) ?? throwError('no inverse'),
-    (x) => ForeignField_.inv(x, F.modulus)
+    (x) => ForeignField.inv(x, F.modulus)
   );
   eq2(
     (x, y) => F.div(x, y) ?? throwError('no inverse'),
-    (x, y) => ForeignField_.div(x, y, F.modulus),
+    (x, y) => ForeignField.div(x, y, F.modulus),
     'div'
   );
 
@@ -103,19 +102,19 @@ for (let F of fields) {
   );
   equivalentProvable({ from: [big258, big258], to: f })(
     F.mul,
-    (x, y) => ForeignField_.mul(x, y, F.modulus),
+    (x, y) => ForeignField.mul(x, y, F.modulus),
     'mul'
   );
   equivalentProvable({ from: [big258], to: f })(
     (x) => F.inverse(x) ?? throwError('no inverse'),
-    (x) => ForeignField_.inv(x, F.modulus)
+    (x) => ForeignField.inv(x, F.modulus)
   );
   // the div() gadget doesn't work with unreduced x because the backwards check (x/y)*y === x fails
   // and it's not valid with unreduced y because we only assert y != 0, y != f but it can be 2f, 3f, etc.
   // the combination of inv() and mul() is more flexible (but much more expensive, ~40 vs ~30 constraints)
   equivalentProvable({ from: [big258, big258], to: f })(
     (x, y) => F.div(x, y) ?? throwError('no inverse'),
-    (x, y) => ForeignField_.mul(x, ForeignField_.inv(y, F.modulus), F.modulus)
+    (x, y) => ForeignField.mul(x, ForeignField.inv(y, F.modulus), F.modulus)
   );
 
   // sumchain of 5
@@ -163,21 +162,21 @@ let ffProgram = ZkProgram({
     mul: {
       privateInputs: [Field3.provable, Field3.provable],
       method(x, y) {
-        return ForeignField_.mul(x, y, F.modulus);
+        return ForeignField.mul(x, y, F.modulus);
       },
     },
 
     inv: {
       privateInputs: [Field3.provable],
       method(x) {
-        return ForeignField_.inv(x, F.modulus);
+        return ForeignField.inv(x, F.modulus);
       },
     },
 
     div: {
       privateInputs: [Field3.provable, Field3.provable],
       method(x, y) {
-        return ForeignField_.div(x, y, F.modulus);
+        return ForeignField.div(x, y, F.modulus);
       },
     },
   },
@@ -202,14 +201,20 @@ constraintSystem.fromZkProgram(
 let mulChain: GateType[] = ['ForeignFieldMul', 'Zero'];
 let mulLayout = ifNotAllConstant(
   and(
-    contains([mulChain, mrc, mrc, mrc]),
-    withoutGenerics(equals([...mulChain, ...repeat(3, mrc)]))
+    contains([mulChain, mrc, mrc, mrc, mrc]),
+    withoutGenerics(equals([...mulChain, ...repeat(4, mrc)]))
+  )
+);
+let invLayout = ifNotAllConstant(
+  and(
+    contains([mrc, mulChain, mrc, mrc, mrc]),
+    withoutGenerics(equals([...mrc, ...mulChain, ...repeat(3, mrc)]))
   )
 );
 
 constraintSystem.fromZkProgram(ffProgram, 'mul', mulLayout);
-constraintSystem.fromZkProgram(ffProgram, 'inv', mulLayout);
-constraintSystem.fromZkProgram(ffProgram, 'div', mulLayout);
+constraintSystem.fromZkProgram(ffProgram, 'inv', invLayout);
+constraintSystem.fromZkProgram(ffProgram, 'div', invLayout);
 
 // tests with proving
 

From 21b9e8b82834d61290aa112e8cc0f23f223e81b0 Mon Sep 17 00:00:00 2001
From: Gregor <gregor.mitscha-baude@gmx.at>
Date: Wed, 15 Nov 2023 11:54:17 +0100
Subject: [PATCH 26/34] document inv and div

---
 src/lib/gadgets/gadgets.ts | 13 ++++++-------
 1 file changed, 6 insertions(+), 7 deletions(-)

diff --git a/src/lib/gadgets/gadgets.ts b/src/lib/gadgets/gadgets.ts
index 79b1e39e0..50ac237ea 100644
--- a/src/lib/gadgets/gadgets.ts
+++ b/src/lib/gadgets/gadgets.ts
@@ -370,11 +370,6 @@ const Gadgets = {
      * Foreign field subtraction: `x - y mod f`
      *
      * See {@link ForeignField.add} for assumptions and usage examples.
-     *
-     * @param x left summand
-     * @param y right summand
-     * @param f modulus
-     * @returns x - y mod f
      */
     sub(x: Field3, y: Field3, f: bigint) {
       return ForeignField.sub(x, y, f);
@@ -452,14 +447,18 @@ const Gadgets = {
     },
 
     /**
-     * TODO
+     * Foreign field inverse: `x^(-1) mod f`
+     *
+     * See {@link ForeignField.mul} for assumptions on inputs and usage examples.
      */
     inv(x: Field3, f: bigint) {
       return ForeignField.inv(x, f);
     },
 
     /**
-     * TODO
+     * Foreign field division: `x * y^(-1) mod f`
+     *
+     * See {@link ForeignField.mul} for assumptions on inputs and usage examples.
      */
     div(x: Field3, y: Field3, f: bigint) {
       return ForeignField.div(x, y, f);

From e46432d2c7b317d5b69e6fa49def6d21a701dfb5 Mon Sep 17 00:00:00 2001
From: Gregor <gregor.mitscha-baude@gmx.at>
Date: Wed, 15 Nov 2023 12:01:01 +0100
Subject: [PATCH 27/34] bindings

---
 src/bindings | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/bindings b/src/bindings
index cea062267..c8f8c631f 160000
--- a/src/bindings
+++ b/src/bindings
@@ -1 +1 @@
-Subproject commit cea062267c2cf81edf50fee8ca9578824c056731
+Subproject commit c8f8c631f28b84c3d3859378a2fe857091207755

From df2ea58bdbcea31171e348f28cb7242d4e33a5c2 Mon Sep 17 00:00:00 2001
From: Gregor <gregor.mitscha-baude@gmx.at>
Date: Wed, 15 Nov 2023 12:13:05 +0100
Subject: [PATCH 28/34] minor

---
 src/lib/gadgets/foreign-field.ts | 6 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

diff --git a/src/lib/gadgets/foreign-field.ts b/src/lib/gadgets/foreign-field.ts
index 30e02e5e0..ddac02dc4 100644
--- a/src/lib/gadgets/foreign-field.ts
+++ b/src/lib/gadgets/foreign-field.ts
@@ -186,7 +186,7 @@ function divide(
   let q2Bound = assertMul(z, y, x, f);
 
   // range check on q and result bounds
-  multiRangeCheck([q2Bound, z2Bound, new Field(0n)]);
+  multiRangeCheck([q2Bound, z2Bound, Field.from(0n)]);
 
   if (!allowZeroOverZero) {
     // assert that y != 0 mod f by checking that it doesn't equal 0 or f
@@ -319,9 +319,7 @@ function multiplyNoRangeCheck(a: Field3, b: Field3, f: bigint) {
 }
 
 function weakBound(x: Field, f: bigint) {
-  let f2 = f >> L2;
-  let f2Bound = lMask - f2;
-  return x.add(f2Bound);
+  return x.add(lMask - (f >> L2));
 }
 
 const Field3 = {

From 9d6bb6d1069a9a0ce353d8e96b8363569e810fee Mon Sep 17 00:00:00 2001
From: Gregor <gregor.mitscha-baude@gmx.at>
Date: Wed, 15 Nov 2023 12:33:28 +0100
Subject: [PATCH 29/34] minor tweaks + changelog

---
 CHANGELOG.md                               |  5 +++++
 src/lib/gadgets/foreign-field.ts           |  5 ++++-
 src/lib/gadgets/foreign-field.unit-test.ts | 23 +++++++++++-----------
 3 files changed, 21 insertions(+), 12 deletions(-)

diff --git a/CHANGELOG.md b/CHANGELOG.md
index 0888d6204..9440ac0ac 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -19,10 +19,15 @@ This project adheres to [Semantic Versioning](https://semver.org/spec/v2.0.0.htm
 
 ## [Unreleased](https://github.com/o1-labs/o1js/compare/26363465d...HEAD)
 
+### Breaking changes
+
+- Change return signature of `ZkProgram.analyzeMethods()` to be a keyed object https://github.com/o1-labs/o1js/pull/1223
+
 ### Added
 
 - Provable non-native field arithmetic:
   - `Gadgets.ForeignField.{add, sub, sumchain}()` for addition and subtraction https://github.com/o1-labs/o1js/pull/1220
+  - `Gadgets.ForeignField.{mul, inv, div}()` for multiplication and division https://github.com/o1-labs/o1js/pull/1223
 - Comprehensive internal testing of constraint system layouts generated by new gadgets https://github.com/o1-labs/o1js/pull/1241 https://github.com/o1-labs/o1js/pull/1220
 
 ### Changed
diff --git a/src/lib/gadgets/foreign-field.ts b/src/lib/gadgets/foreign-field.ts
index ddac02dc4..c8415be2d 100644
--- a/src/lib/gadgets/foreign-field.ts
+++ b/src/lib/gadgets/foreign-field.ts
@@ -17,7 +17,7 @@ import {
   compactMultiRangeCheck,
 } from './range-check.js';
 
-export { ForeignField, Field3, bigint3, Sign };
+export { ForeignField, Field3, Sign };
 
 /**
  * A 3-tuple of Fields, representing a 3-limb bigint.
@@ -202,6 +202,9 @@ function divide(
   return z;
 }
 
+/**
+ * Common logic for gadgets that expect a certain multiplication result instead of just using the remainder.
+ */
 function assertMul(x: Field3, y: Field3, xy: Field3 | Field2, f: bigint) {
   let { r01, r2, q, q2Bound } = multiplyNoRangeCheck(x, y, f);
 
diff --git a/src/lib/gadgets/foreign-field.unit-test.ts b/src/lib/gadgets/foreign-field.unit-test.ts
index 459ee7cde..eca513d84 100644
--- a/src/lib/gadgets/foreign-field.unit-test.ts
+++ b/src/lib/gadgets/foreign-field.unit-test.ts
@@ -77,7 +77,8 @@ for (let F of fields) {
   eq2(F.mul, (x, y) => ForeignField.mul(x, y, F.modulus), 'mul');
   equivalentProvable({ from: [f], to: f })(
     (x) => F.inverse(x) ?? throwError('no inverse'),
-    (x) => ForeignField.inv(x, F.modulus)
+    (x) => ForeignField.inv(x, F.modulus),
+    'inv'
   );
   eq2(
     (x, y) => F.div(x, y) ?? throwError('no inverse'),
@@ -92,35 +93,38 @@ for (let F of fields) {
   equivalentProvable({ from: [big264, big264], to: big264 })(
     F.add,
     (x, y) => ForeignField.add(x, y, F.modulus),
-    'add'
+    'add unreduced'
   );
   // subtraction doesn't work with unreduced y because the range check on the result prevents x-y < -f
   equivalentProvable({ from: [big264, f], to: big264 })(
     F.sub,
     (x, y) => ForeignField.sub(x, y, F.modulus),
-    'sub'
+    'sub unreduced'
   );
   equivalentProvable({ from: [big258, big258], to: f })(
     F.mul,
     (x, y) => ForeignField.mul(x, y, F.modulus),
-    'mul'
+    'mul unreduced'
   );
   equivalentProvable({ from: [big258], to: f })(
     (x) => F.inverse(x) ?? throwError('no inverse'),
-    (x) => ForeignField.inv(x, F.modulus)
+    (x) => ForeignField.inv(x, F.modulus),
+    'inv unreduced'
   );
   // the div() gadget doesn't work with unreduced x because the backwards check (x/y)*y === x fails
   // and it's not valid with unreduced y because we only assert y != 0, y != f but it can be 2f, 3f, etc.
   // the combination of inv() and mul() is more flexible (but much more expensive, ~40 vs ~30 constraints)
   equivalentProvable({ from: [big258, big258], to: f })(
     (x, y) => F.div(x, y) ?? throwError('no inverse'),
-    (x, y) => ForeignField.mul(x, ForeignField.inv(y, F.modulus), F.modulus)
+    (x, y) => ForeignField.mul(x, ForeignField.inv(y, F.modulus), F.modulus),
+    'div unreduced'
   );
 
   // sumchain of 5
   equivalentProvable({ from: [array(f, 5), array(sign, 4)], to: f })(
     (xs, signs) => sum(xs, signs, F),
-    (xs, signs) => ForeignField.sum(xs, signs, F.modulus)
+    (xs, signs) => ForeignField.sum(xs, signs, F.modulus),
+    'sumchain 5'
   );
 
   // sumchain up to 100
@@ -137,7 +141,7 @@ for (let F of fields) {
       let signs = ts.map((t) => t.sign);
       return ForeignField.sum(xs, signs, F.modulus);
     },
-    'sumchain'
+    'sumchain long'
   );
 }
 
@@ -158,21 +162,18 @@ let ffProgram = ZkProgram({
         return ForeignField.sum(xs, signs, F.modulus);
       },
     },
-
     mul: {
       privateInputs: [Field3.provable, Field3.provable],
       method(x, y) {
         return ForeignField.mul(x, y, F.modulus);
       },
     },
-
     inv: {
       privateInputs: [Field3.provable],
       method(x) {
         return ForeignField.inv(x, F.modulus);
       },
     },
-
     div: {
       privateInputs: [Field3.provable, Field3.provable],
       method(x, y) {

From 0ccea11d1bbc83f138a661d828b07572befa5b33 Mon Sep 17 00:00:00 2001
From: Gregor <gregor.mitscha-baude@gmx.at>
Date: Fri, 17 Nov 2023 10:25:32 +0100
Subject: [PATCH 30/34] fix: don't range-check 2-bit carry

---
 src/lib/gadgets/foreign-field.ts | 40 ++++++++++++++++++--------------
 1 file changed, 23 insertions(+), 17 deletions(-)

diff --git a/src/lib/gadgets/foreign-field.ts b/src/lib/gadgets/foreign-field.ts
index c8415be2d..8d5d2edbe 100644
--- a/src/lib/gadgets/foreign-field.ts
+++ b/src/lib/gadgets/foreign-field.ts
@@ -117,16 +117,16 @@ function multiply(a: Field3, b: Field3, f: bigint): Field3 {
   }
 
   // provable case
-  let { r01, r2, q, q2Bound } = multiplyNoRangeCheck(a, b, f);
+  let { r01, r2, q } = multiplyNoRangeCheck(a, b, f);
 
   // limb range checks on quotient and remainder
   multiRangeCheck(q);
   let r = compactMultiRangeCheck(r01, r2);
 
-  // range check on q and r bounds
-  // TODO: this uses one RC too many.. need global RC stack, or get rid of bounds checks
+  // range check on r bound
+  // TODO: this uses two RCs too many.. need global RC stack, or get rid of bounds checks
   let r2Bound = weakBound(r2, f);
-  multiRangeCheck([q2Bound, r2Bound, Field.from(0n)]);
+  multiRangeCheck([r2Bound, Field.from(0n), Field.from(0n)]);
 
   return r;
 }
@@ -150,11 +150,11 @@ function inverse(x: Field3, f: bigint): Field3 {
   let xInv2Bound = weakBound(xInv[2], f);
 
   let one: Field2 = [Field.from(1n), Field.from(0n)];
-  let q2Bound = assertMul(x, xInv, one, f);
+  assertMul(x, xInv, one, f);
 
-  // range check on q and result bounds
-  // TODO: this uses one RC too many.. need global RC stack
-  multiRangeCheck([q2Bound, xInv2Bound, Field.from(0n)]);
+  // range check on result bound
+  // TODO: this uses two RCs too many.. need global RC stack
+  multiRangeCheck([xInv2Bound, Field.from(0n), Field.from(0n)]);
 
   return xInv;
 }
@@ -183,10 +183,10 @@ function divide(
   });
   multiRangeCheck(z);
   let z2Bound = weakBound(z[2], f);
-  let q2Bound = assertMul(z, y, x, f);
+  assertMul(z, y, x, f);
 
-  // range check on q and result bounds
-  multiRangeCheck([q2Bound, z2Bound, Field.from(0n)]);
+  // range check on result bound
+  multiRangeCheck([z2Bound, Field.from(0n), Field.from(0n)]);
 
   if (!allowZeroOverZero) {
     // assert that y != 0 mod f by checking that it doesn't equal 0 or f
@@ -203,10 +203,10 @@ function divide(
 }
 
 /**
- * Common logic for gadgets that expect a certain multiplication result instead of just using the remainder.
+ * Common logic for gadgets that expect a certain multiplication result a priori, instead of just using the remainder.
  */
 function assertMul(x: Field3, y: Field3, xy: Field3 | Field2, f: bigint) {
-  let { r01, r2, q, q2Bound } = multiplyNoRangeCheck(x, y, f);
+  let { r01, r2, q } = multiplyNoRangeCheck(x, y, f);
 
   // range check on quotient
   multiRangeCheck(q);
@@ -221,9 +221,11 @@ function assertMul(x: Field3, y: Field3, xy: Field3 | Field2, f: bigint) {
     r01.assertEquals(xy01);
     r2.assertEquals(xy[2]);
   }
-  return q2Bound;
 }
 
+/**
+ * Core building block for all gadgets using foreign field multiplication.
+ */
 function multiplyNoRangeCheck(a: Field3, b: Field3, f: bigint) {
   // notation follows https://github.com/o1-labs/rfcs/blob/main/0006-ffmul-revised.md
   let f_ = (1n << L3) - f;
@@ -315,10 +317,14 @@ function multiplyNoRangeCheck(a: Field3, b: Field3, f: bigint) {
     negForeignFieldModulus: [f_0, f_1, f_2],
   });
 
-  // multi-range check on intermediate values
-  multiRangeCheck([c0, p10, p110]);
+  // multi-range check on internal values
+  multiRangeCheck([p10, p110, q2Bound]);
 
-  return { r01, r2, q, q2Bound };
+  // note: this function is supposed to be the most flexible interface to the ffmul gate.
+  // that's why we don't add range checks on q and r here, because there are valid use cases
+  // for not range-checking either of them -- for example, they could be wired to other
+  // variables that are already range-checked, or to constants / public inputs.
+  return { r01, r2, q };
 }
 
 function weakBound(x: Field, f: bigint) {

From 571866b35488fd0fc85077bd7f986556e7761a11 Mon Sep 17 00:00:00 2001
From: Gregor <gregor.mitscha-baude@gmx.at>
Date: Fri, 17 Nov 2023 10:29:39 +0100
Subject: [PATCH 31/34] consistent lower-casing of limb size constant

---
 src/lib/gadgets/foreign-field.ts         | 32 ++++++++++++------------
 src/lib/gadgets/range-check.ts           | 22 ++++++++--------
 src/lib/gadgets/range-check.unit-test.ts | 12 ++++-----
 3 files changed, 33 insertions(+), 33 deletions(-)

diff --git a/src/lib/gadgets/foreign-field.ts b/src/lib/gadgets/foreign-field.ts
index 8d5d2edbe..177b16c5c 100644
--- a/src/lib/gadgets/foreign-field.ts
+++ b/src/lib/gadgets/foreign-field.ts
@@ -8,12 +8,12 @@ import { Gates, foreignFieldAdd } from '../gates.js';
 import { Tuple } from '../util/types.js';
 import { assert, bitSlice, exists, toVars } from './common.js';
 import {
-  L,
+  l,
   lMask,
   multiRangeCheck,
-  L2,
+  l2,
   l2Mask,
-  L3,
+  l3,
   compactMultiRangeCheck,
 } from './range-check.js';
 
@@ -94,7 +94,7 @@ function singleAdd(x: Field3, y: Field3, sign: Sign, f: bigint) {
     // do the add with carry
     // note: this "just works" with negative r01
     let r01 = collapse2(x_) + sign * collapse2(y_) - overflow * collapse2(f_);
-    let carry = r01 >> L2;
+    let carry = r01 >> l2;
     r01 &= l2Mask;
     let [r0, r1] = split2(r01);
     let r2 = x_[2] + sign * y_[2] - overflow * f_[2] + carry;
@@ -192,7 +192,7 @@ function divide(
     // assert that y != 0 mod f by checking that it doesn't equal 0 or f
     // this works because we assume y[2] <= f2
     // TODO is this the most efficient way?
-    let y01 = y[0].add(y[1].mul(1n << L));
+    let y01 = y[0].add(y[1].mul(1n << l));
     y01.equals(0n).and(y[2].equals(0n)).assertFalse();
     let [f0, f1, f2] = split(f);
     let f01 = collapse2([f0, f1]);
@@ -217,7 +217,7 @@ function assertMul(x: Field3, y: Field3, xy: Field3 | Field2, f: bigint) {
     r01.assertEquals(xy01);
     r2.assertEquals(xy2);
   } else {
-    let xy01 = xy[0].add(xy[1].mul(1n << L));
+    let xy01 = xy[0].add(xy[1].mul(1n << l));
     r01.assertEquals(xy01);
     r2.assertEquals(xy[2]);
   }
@@ -228,10 +228,10 @@ function assertMul(x: Field3, y: Field3, xy: Field3 | Field2, f: bigint) {
  */
 function multiplyNoRangeCheck(a: Field3, b: Field3, f: bigint) {
   // notation follows https://github.com/o1-labs/rfcs/blob/main/0006-ffmul-revised.md
-  let f_ = (1n << L3) - f;
+  let f_ = (1n << l3) - f;
   let [f_0, f_1, f_2] = split(f_);
-  let f2 = f >> L2;
-  let f2Bound = (1n << L) - f2 - 1n;
+  let f2 = f >> l2;
+  let f2Bound = (1n << l) - f2 - 1n;
 
   let witnesses = exists(21, () => {
     // split inputs into 3 limbs
@@ -256,10 +256,10 @@ function multiplyNoRangeCheck(a: Field3, b: Field3, f: bigint) {
     let p11 = collapse2([p110, p111]);
 
     // carry bottom limbs
-    let c0 = (p0 + (p10 << L) - r01) >> L2;
+    let c0 = (p0 + (p10 << l) - r01) >> l2;
 
     // carry top limb
-    let c1 = (p2 - r2 + p11 + c0) >> L;
+    let c1 = (p2 - r2 + p11 + c0) >> l;
 
     // split high carry
     let c1_00 = bitSlice(c1, 0, 12);
@@ -328,7 +328,7 @@ function multiplyNoRangeCheck(a: Field3, b: Field3, f: bigint) {
 }
 
 function weakBound(x: Field, f: bigint) {
-  return x.add(lMask - (f >> L2));
+  return x.add(lMask - (f >> l2));
 }
 
 const Field3 = {
@@ -367,15 +367,15 @@ function bigint3(x: Field3): bigint3 {
 }
 
 function collapse([x0, x1, x2]: bigint3) {
-  return x0 + (x1 << L) + (x2 << L2);
+  return x0 + (x1 << l) + (x2 << l2);
 }
 function split(x: bigint): bigint3 {
-  return [x & lMask, (x >> L) & lMask, (x >> L2) & lMask];
+  return [x & lMask, (x >> l) & lMask, (x >> l2) & lMask];
 }
 
 function collapse2([x0, x1]: bigint3 | [bigint, bigint]) {
-  return x0 + (x1 << L);
+  return x0 + (x1 << l);
 }
 function split2(x: bigint): [bigint, bigint] {
-  return [x & lMask, (x >> L) & lMask];
+  return [x & lMask, (x >> l) & lMask];
 }
diff --git a/src/lib/gadgets/range-check.ts b/src/lib/gadgets/range-check.ts
index 7abfe0739..1e44afdaf 100644
--- a/src/lib/gadgets/range-check.ts
+++ b/src/lib/gadgets/range-check.ts
@@ -3,7 +3,7 @@ import { Gates } from '../gates.js';
 import { bitSlice, exists, toVar, toVars } from './common.js';
 
 export { rangeCheck64, multiRangeCheck, compactMultiRangeCheck };
-export { L, L2, L3, lMask, l2Mask };
+export { l, l2, l3, lMask, l2Mask };
 
 /**
  * Asserts that x is in the range [0, 2^64)
@@ -51,19 +51,19 @@ function rangeCheck64(x: Field) {
 }
 
 // default bigint limb size
-const L = 88n;
-const L2 = 2n * L;
-const L3 = 3n * L;
-const lMask = (1n << L) - 1n;
-const l2Mask = (1n << L2) - 1n;
+const l = 88n;
+const l2 = 2n * l;
+const l3 = 3n * l;
+const lMask = (1n << l) - 1n;
+const l2Mask = (1n << l2) - 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}`);
+    if (x.toBigInt() >> l || y.toBigInt() >> l || z.toBigInt() >> l) {
+      throw Error(`Expected fields to fit in ${l} bits, got ${x}, ${y}, ${z}`);
     }
     return;
   }
@@ -86,9 +86,9 @@ function multiRangeCheck([x, y, z]: [Field, Field, Field]) {
 function compactMultiRangeCheck(xy: Field, z: Field): [Field, Field, Field] {
   // constant case
   if (xy.isConstant() && z.isConstant()) {
-    if (xy.toBigInt() >> L2 || z.toBigInt() >> L) {
+    if (xy.toBigInt() >> l2 || z.toBigInt() >> l) {
       throw Error(
-        `Expected fields to fit in ${L2} and ${L} bits respectively, got ${xy}, ${z}`
+        `Expected fields to fit in ${l2} and ${l} bits respectively, got ${xy}, ${z}`
       );
     }
     let [x, y] = splitCompactLimb(xy.toBigInt());
@@ -107,7 +107,7 @@ function compactMultiRangeCheck(xy: Field, z: Field): [Field, Field, Field] {
 }
 
 function splitCompactLimb(x01: bigint): [bigint, bigint] {
-  return [x01 & lMask, x01 >> L];
+  return [x01 & lMask, x01 >> l];
 }
 
 function rangeCheck0Helper(x: Field, isCompact = false): [Field, Field] {
diff --git a/src/lib/gadgets/range-check.unit-test.ts b/src/lib/gadgets/range-check.unit-test.ts
index b5d511080..47aafbf59 100644
--- a/src/lib/gadgets/range-check.unit-test.ts
+++ b/src/lib/gadgets/range-check.unit-test.ts
@@ -10,7 +10,7 @@ import {
 import { Random } from '../testing/property.js';
 import { assert } from './common.js';
 import { Gadgets } from './gadgets.js';
-import { L } from './range-check.js';
+import { l } from './range-check.js';
 import {
   constraintSystem,
   contains,
@@ -82,7 +82,7 @@ let RangeCheck = ZkProgram({
       privateInputs: [Field, Field],
       method(xy, z) {
         let [x, y] = Gadgets.compactMultiRangeCheck(xy, z);
-        x.add(y.mul(1n << L)).assertEquals(xy);
+        x.add(y.mul(1n << l)).assertEquals(xy);
       },
     },
   },
@@ -104,11 +104,11 @@ await equivalentAsync({ from: [maybeUint(64)], to: boolean }, { runs: 3 })(
 );
 
 await equivalentAsync(
-  { from: [maybeUint(L), uint(L), uint(L)], to: boolean },
+  { 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');
+    assert(!(x >> l) && !(y >> l) && !(z >> l), 'multi: not out of range');
     return true;
   },
   async (x, y, z) => {
@@ -118,11 +118,11 @@ await equivalentAsync(
 );
 
 await equivalentAsync(
-  { from: [maybeUint(2n * L), uint(L)], to: boolean },
+  { from: [maybeUint(2n * l), uint(l)], to: boolean },
   { runs: 3 }
 )(
   (xy, z) => {
-    assert(!(xy >> (2n * L)) && !(z >> L), 'compact: not out of range');
+    assert(!(xy >> (2n * l)) && !(z >> l), 'compact: not out of range');
     return true;
   },
   async (xy, z) => {

From 91fef7697d668854551f9ade4731ddb2a3c8e246 Mon Sep 17 00:00:00 2001
From: Gregor <gregor.mitscha-baude@gmx.at>
Date: Fri, 17 Nov 2023 10:57:40 +0100
Subject: [PATCH 32/34] remove remainder bounds check in mul() gadget

---
 src/lib/gadgets/foreign-field.ts | 6 ------
 src/lib/gadgets/gadgets.ts       | 9 ++++++++-
 2 files changed, 8 insertions(+), 7 deletions(-)

diff --git a/src/lib/gadgets/foreign-field.ts b/src/lib/gadgets/foreign-field.ts
index 177b16c5c..ca99fcc2b 100644
--- a/src/lib/gadgets/foreign-field.ts
+++ b/src/lib/gadgets/foreign-field.ts
@@ -122,12 +122,6 @@ function multiply(a: Field3, b: Field3, f: bigint): Field3 {
   // limb range checks on quotient and remainder
   multiRangeCheck(q);
   let r = compactMultiRangeCheck(r01, r2);
-
-  // range check on r bound
-  // TODO: this uses two RCs too many.. need global RC stack, or get rid of bounds checks
-  let r2Bound = weakBound(r2, f);
-  multiRangeCheck([r2Bound, Field.from(0n), Field.from(0n)]);
-
   return r;
 }
 
diff --git a/src/lib/gadgets/gadgets.ts b/src/lib/gadgets/gadgets.ts
index 50ac237ea..dc4569369 100644
--- a/src/lib/gadgets/gadgets.ts
+++ b/src/lib/gadgets/gadgets.ts
@@ -413,12 +413,15 @@ const Gadgets = {
      *
      * The modulus `f` does not need to be prime, but has to be smaller than 2^259.
      *
-     * **Assumptions**: In addition to the assumption that inputs are in the range [0, 2^88), as in all foreign field gadgets,
+     * **Assumptions**: In addition to the assumption that input limbs are in the range [0, 2^88), as in all foreign field gadgets,
      * this assumes an additional bound on the inputs: `x * y < 2^264 * p`, where p is the native modulus.
      * We usually assert this bound by proving that `x[2] < f[2] + 1`, where `x[2]` is the most significant limb of x.
      * To do this, use an 88-bit range check on `2^88 - x[2] - (f[2] + 1)`, and same for y.
      * The implication is that x and y are _almost_ reduced modulo f.
      *
+     * **Warning**: This gadget does not add the extra bound check on the result.
+     * So, to use the result in another foreign field multiplication, you have to add the bound check on it yourself, again.
+     *
      * @example
      * ```ts
      * // example modulus: secp256k1 prime
@@ -450,6 +453,8 @@ const Gadgets = {
      * Foreign field inverse: `x^(-1) mod f`
      *
      * See {@link ForeignField.mul} for assumptions on inputs and usage examples.
+     *
+     * This gadget adds an extra bound check on the result, so it can be used directly in another foreign field multiplication.
      */
     inv(x: Field3, f: bigint) {
       return ForeignField.inv(x, f);
@@ -459,6 +464,8 @@ const Gadgets = {
      * Foreign field division: `x * y^(-1) mod f`
      *
      * See {@link ForeignField.mul} for assumptions on inputs and usage examples.
+     *
+     * This gadget adds an extra bound check on the result, so it can be used directly in another foreign field multiplication.
      */
     div(x: Field3, y: Field3, f: bigint) {
       return ForeignField.div(x, y, f);

From ccb55c77f80ed8c2fb8563ef699cc48884e10b74 Mon Sep 17 00:00:00 2001
From: Gregor <gregor.mitscha-baude@gmx.at>
Date: Fri, 17 Nov 2023 12:23:35 +0100
Subject: [PATCH 33/34] fixup unit test

---
 src/lib/gadgets/foreign-field.unit-test.ts | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/lib/gadgets/foreign-field.unit-test.ts b/src/lib/gadgets/foreign-field.unit-test.ts
index eca513d84..4cb0d2d97 100644
--- a/src/lib/gadgets/foreign-field.unit-test.ts
+++ b/src/lib/gadgets/foreign-field.unit-test.ts
@@ -202,8 +202,8 @@ constraintSystem.fromZkProgram(
 let mulChain: GateType[] = ['ForeignFieldMul', 'Zero'];
 let mulLayout = ifNotAllConstant(
   and(
-    contains([mulChain, mrc, mrc, mrc, mrc]),
-    withoutGenerics(equals([...mulChain, ...repeat(4, mrc)]))
+    contains([mulChain, mrc, mrc, mrc]),
+    withoutGenerics(equals([...mulChain, ...repeat(3, mrc)]))
   )
 );
 let invLayout = ifNotAllConstant(

From 021b00144ccd80a353227d4763399920e20d00a9 Mon Sep 17 00:00:00 2001
From: Gregor <gregor.mitscha-baude@gmx.at>
Date: Tue, 21 Nov 2023 16:47:50 +0100
Subject: [PATCH 34/34] address feedback

---
 src/lib/gadgets/foreign-field.ts | 21 +++++++++++----------
 src/lib/gadgets/gadgets.ts       |  4 ++++
 2 files changed, 15 insertions(+), 10 deletions(-)

diff --git a/src/lib/gadgets/foreign-field.ts b/src/lib/gadgets/foreign-field.ts
index fc30ef0a4..75f41a7f8 100644
--- a/src/lib/gadgets/foreign-field.ts
+++ b/src/lib/gadgets/foreign-field.ts
@@ -85,7 +85,7 @@ function singleAdd(x: Field3, y: Field3, sign: Sign, f: bigint) {
     let y_ = toBigint3(y);
 
     // figure out if there's overflow
-    let r = collapse(x_) + sign * collapse(y_);
+    let r = combine(x_) + sign * combine(y_);
     let overflow = 0n;
     if (sign === 1n && r >= f) overflow = 1n;
     if (sign === -1n && r < 0n) overflow = -1n;
@@ -93,7 +93,7 @@ function singleAdd(x: Field3, y: Field3, sign: Sign, f: bigint) {
 
     // do the add with carry
     // note: this "just works" with negative r01
-    let r01 = collapse2(x_) + sign * collapse2(y_) - overflow * collapse2(f_);
+    let r01 = combine2(x_) + sign * combine2(y_) - overflow * combine2(f_);
     let carry = r01 >> l2;
     r01 &= l2Mask;
     let [r0, r1] = split2(r01);
@@ -141,6 +141,7 @@ function inverse(x: Field3, f: bigint): Field3 {
     return xInv === undefined ? [0n, 0n, 0n] : split(xInv);
   });
   multiRangeCheck(xInv);
+  // we need to bound xInv because it's a multiplication input
   let xInv2Bound = weakBound(xInv[2], f);
 
   let one: Field2 = [Field.from(1n), Field.from(0n)];
@@ -189,7 +190,7 @@ function divide(
     let y01 = y[0].add(y[1].mul(1n << l));
     y01.equals(0n).and(y[2].equals(0n)).assertFalse();
     let [f0, f1, f2] = split(f);
-    let f01 = collapse2([f0, f1]);
+    let f01 = combine2([f0, f1]);
     y01.equals(f01).and(y[2].equals(f2)).assertFalse();
   }
 
@@ -233,13 +234,13 @@ function multiplyNoRangeCheck(a: Field3, b: Field3, f: bigint) {
     let [b0, b1, b2] = toBigint3(b);
 
     // compute q and r such that a*b = q*f + r
-    let ab = collapse([a0, a1, a2]) * collapse([b0, b1, b2]);
+    let ab = combine([a0, a1, a2]) * combine([b0, b1, b2]);
     let q = ab / f;
     let r = ab - q * f;
 
     let [q0, q1, q2] = split(q);
     let [r0, r1, r2] = split(r);
-    let r01 = collapse2([r0, r1]);
+    let r01 = combine2([r0, r1]);
 
     // compute product terms
     let p0 = a0 * b0 + q0 * f_0;
@@ -247,7 +248,7 @@ function multiplyNoRangeCheck(a: Field3, b: Field3, f: bigint) {
     let p2 = a0 * b2 + a1 * b1 + a2 * b0 + q0 * f_2 + q1 * f_1 + q2 * f_0;
 
     let [p10, p110, p111] = split(p1);
-    let p11 = collapse2([p110, p111]);
+    let p11 = combine2([p110, p111]);
 
     // carry bottom limbs
     let c0 = (p0 + (p10 << l) - r01) >> l2;
@@ -337,7 +338,7 @@ const Field3 = {
    * Turn a 3-tuple of Fields into a bigint
    */
   toBigint(x: Field3): bigint {
-    return collapse(toBigint3(x));
+    return combine(toBigint3(x));
   },
 
   /**
@@ -352,7 +353,7 @@ const Field3 = {
 type Field2 = [Field, Field];
 const Field2 = {
   toBigint(x: Field2): bigint {
-    return collapse2(Tuple.map(x, (x) => x.toBigInt()));
+    return combine2(Tuple.map(x, (x) => x.toBigInt()));
   },
 };
 
@@ -360,14 +361,14 @@ function toBigint3(x: Field3): bigint3 {
   return Tuple.map(x, (x) => x.toBigInt());
 }
 
-function collapse([x0, x1, x2]: bigint3) {
+function combine([x0, x1, x2]: bigint3) {
   return x0 + (x1 << l) + (x2 << l2);
 }
 function split(x: bigint): bigint3 {
   return [x & lMask, (x >> l) & lMask, (x >> l2) & lMask];
 }
 
-function collapse2([x0, x1]: bigint3 | [bigint, bigint]) {
+function combine2([x0, x1]: bigint3 | [bigint, bigint]) {
   return x0 + (x1 << l);
 }
 function split2(x: bigint): [bigint, bigint] {
diff --git a/src/lib/gadgets/gadgets.ts b/src/lib/gadgets/gadgets.ts
index dc4569369..b67ef58fd 100644
--- a/src/lib/gadgets/gadgets.ts
+++ b/src/lib/gadgets/gadgets.ts
@@ -370,6 +370,8 @@ const Gadgets = {
      * Foreign field subtraction: `x - y mod f`
      *
      * See {@link ForeignField.add} for assumptions and usage examples.
+     *
+     * @throws fails if `x - y < -f`, where the result cannot be brought back to a positive number by adding `f` once.
      */
     sub(x: Field3, y: Field3, f: bigint) {
       return ForeignField.sub(x, y, f);
@@ -466,6 +468,8 @@ const Gadgets = {
      * See {@link ForeignField.mul} for assumptions on inputs and usage examples.
      *
      * This gadget adds an extra bound check on the result, so it can be used directly in another foreign field multiplication.
+     *
+     * @throws Different than {@link ForeignField.mul}, this fails on unreduced input `x`, because it checks that `x === (x/y)*y` and the right side will be reduced.
      */
     div(x: Field3, y: Field3, f: bigint) {
       return ForeignField.div(x, y, f);