Foreign fields 3: Addition #1220

mitschabaude · 2023-11-02T16:39:45Z

adds a ForeignField gadget namespace with methods for addition, subtraction and general sums using non-native modular arithmetic.
enhances the constraintSystem() test runner introduced in Foreign fields 2: Test DSL to detect broken gate chains #1241 so that it becomes very easy to check methods of a zkprogram

closes #1152
closes #1180

depends on bindings PRs o1-labs/o1js-bindings#203 and o1-labs/o1js-bindings#205

Proof that we can save range checks in `sum()`

An optimization used here is to not range-check intermediate results in addition chains of length > 2, i.e. what is exposed as sum(). The reasoning why this is sound is as follows:

Assume we are doing an addition chain over summands $a_0,\ldots,a_n$. Let's denote the lower input limbs by $a_i^{(01)}$ and the high limb by $a_i^{(2)}$. Each FFadd gate individually proves that

$$ a_i^{(01)} + a_{i+1}^{(01)} - o_i f^{(01)} - c_i 2^{2\ell} = r_i^{(01)} \mod{n} $$

$$ a_i^{(2)} + a_{i+1}^{(2)} - o_i f^{(2)} + c_i = r_i^{(2)} \mod{n} $$

where $o_i$ and $c_i$ are overflow and carry, and $n$ is the native modulus. Since addition modulo $n$ is associative, a full chain of ffadd gates proves the following equations about the final output $r$:

$$ a_0^{(01)} + \ldots + a_{n}^{(01)} - (o_1 + \ldots + o_n) f^{(01)} - (c_1 + \ldots + c_n) 2^{2\ell} = r^{(01)} \mod{n} $$

$$ a_0^{(2)} + \ldots + a_{n}^{(2)} - (o_1 + \ldots + o_n) f^{(2)} + (c_1 + \ldots + c_n) = r^{(2)} \mod{n} $$

Since we assume the inputs $a_i$ to be range-checked, and both $o_i$ and $c_i$ are 0 or 1 or -1, and the final output $r$ is range-checked as well, the difference of left and right hand side is too small to overflow the native field:

$$ |LHS - RHS| < n $$

This is enough to conclude that $LHS = RHS$ over the integers. Which in this case just means that we are doing correct addition or subtraction modulo the foreign field.

rbonichon · 2023-11-14T08:55:46Z

src/lib/testing/equivalent.ts

+function array<T, S>(
+  spec: ProvableSpec<T, S>,
+  n: number
+): ProvableSpec<T[], S[]>;
+function array<T, S>(
+  spec: Spec<T, S>,
+  n: Random<number> | number
+): Spec<T[], S[]>;


Are these function declarations?
Why is the second declaration needed (it's the same type as the implementation right below)?

This is how you declare if there are two different function signatures. The third one is not exposed, it's the "internal" signature used in writing the function. So if I remove the second one, consumers only see the first one

mitschabaude

some notes for reviewers!

mitschabaude · 2023-11-14T12:17:26Z

src/lib/gadgets/foreign-field.ts

the code for the new gadgets! please review carefully

mitschabaude · 2023-11-14T12:21:20Z

src/lib/gadgets/gadgets.ts

+  /**
+   * Helper methods to interact with 3-limb vectors of Fields.
+   *
+   * **Note:** This interface does not contain any provable methods.
+   */
+  Field3,


I'm a bit conflicted about this. I sometimes got the feedback that it's confusing how o1js APIs are a mix of provable and non-provable methods. I'm not sure if putting them on a separate sub-namespace of Gadgets is enough separation. In any case, these helper methods are essential to reduce boiler-plate of interacting with all foreign field and foreign curve gadgets, and I also didn't feel good about another top-level export for them.

mitschabaude · 2023-11-14T12:23:45Z

src/lib/gadgets/gadgets.ts

+export namespace Gadgets {
+  /**
+   * A 3-tuple of Fields, representing a 3-limb bigint.
+   */
+  export type Field3 = [Field, Field, Field];
+}


note: this is how to get a type namespace alongside a value namespace. It's possible to use the same name if the type namespace is only types. We could've also put everything in a single namespace, but I prefer the syntax for writing JS objects over the clunky namespace syntax which isn't even real JS (just a TS addition to the language).

mitschabaude · 2023-11-14T12:26:44Z

src/lib/testing/constraint-system.ts

+/**
+ * Convenience function to run {@link constraintSystem} on the method of a {@link ZkProgram}.
+ *
+ * @example
+ * ```ts
+ * const program = ZkProgram({ methods: { myMethod: ... }, ... });
+ *
+ * constraintSystem.fromZkProgram(program, 'myMethod', contains('Rot64'));
+ * ```
+ */
+constraintSystem.fromZkProgram = function fromZkProgram<


This is a continuation of #1241. I figured I could make writing constraint system tests for zkprogram methods even easier by reading the input types off the zkprogram.

mitschabaude · 2023-11-14T12:27:24Z

src/lib/proof_system.ts

changes in this file are in support of the new constraintSystem.fromZkProgram()

mitschabaude · 2023-11-14T12:28:07Z

src/lib/proof_system.ts

      publicInputType: publicInputType as ProvableOrUndefined<
        Get<StatementType, 'publicInput'>
      >,
      publicOutputType: publicOutputType as ProvableOrVoid<
        Get<StatementType, 'publicOutput'>
      >,
-      analyzeMethods,
+      privateInputTypes: Object.fromEntries(


exposing the private input types on zkprogram seems consistent, since we already expose the public input types and the methods

What is this exactly for?

It's in support of a testing utility I added: #1220 (comment)
You can ignore it, it's not related to the circuit gadgets added here :D

mitschabaude · 2023-11-14T12:28:57Z

src/lib/proof_system.ts

@@ -925,6 +945,7 @@ ZkProgram.Proof = function <
    static tag = () => program;
  };
 };
+ExperimentalZkProgram.Proof = ZkProgram.Proof;


this was a bug which accidentally broke Experimental.ZkProgram, fixed it while I was here

mitschabaude · 2023-11-14T12:29:35Z

src/lib/testing/equivalent.ts

additions here are in support of the foreign field unit tests

mitschabaude · 2023-11-14T12:29:57Z

src/lib/testing/random.ts

@@ -307,6 +308,7 @@ const Random = Object.assign(Random_, {
  reject,
  dice: Object.assign(dice, { ofSize: diceOfSize() }),
  field,
+  otherField: fieldWithInvalid,


random generator for foreign fields, for tests

querolita

Approving with minor comments

querolita · 2023-11-16T15:34:45Z

src/lib/gadgets/foreign-field.ts

+export { ForeignField, Field3, Sign };
+
+/**
+ * A 3-tuple of Fields, representing a 3-limb bigint.


Maybe clarify here what's the highest and lowest limbs?

querolita · 2023-11-16T15:35:26Z

src/lib/gadgets/foreign-field.ts

+ *
+ * assumes that inputs are range checked, does range check on the result.
+ */
+function sum(x: Field3[], sign: Sign[], f: bigint) {


Is sum being exposed or just add, sub and sumchain?

sum() is exposed! it is actually the same as sumchain in OCaml, I renamed it because I think the "chain" aspect is more about the internal implementation and less important for users

querolita · 2023-11-16T15:36:14Z

src/lib/gadgets/foreign-field.ts

+  assert(x.length === sign.length + 1, 'inputs and operators match');
+
+  // constant case
+  if (x.every((x) => x.every((x) => x.isConstant()))) {


what's the meaning of this notation =>?

this is an inline function, called arrow function in JS. in Rust you'd call it a closure

querolita · 2023-11-16T15:37:59Z

src/lib/gadgets/foreign-field.ts

+    ({ result } = singleAdd(result, x[i + 1], sign[i], f));
+  }
+  // final zero row to hold result
+  Gates.zero(...result);


But maybe the last gate could be a FFMul0 for example, in case someone wanted to use that output for the left input of a multiplication, no?

I guess we had to provide some kind of tradeoff between ease-of-use and functionality 💭

I completely agree, this isn't yet the best version of the sumchain gadget. Wait for the ECDSA PR, there I needed chaining into ffmul and I came up with an API which is both easy to use and flexible

querolita · 2023-11-16T15:39:56Z

src/lib/gadgets/foreign-field.ts

+ * **warning**: this just adds the `foreignFieldAdd` row;
+ * it _must_ be chained with a second row that holds the result in its first 3 cells.
+ *
+ * the second row could, for example, be `zero`, `foreignFieldMul`, or another `foreignFieldAdd`.


Oh I see, so you still provide "fine grain" access to this in case the user wants to create a more efficient circuit.

querolita · 2023-11-16T15:57:30Z

src/lib/gadgets/foreign-field.ts

+    let overflow = 0n;
+    if (sign === 1n && r >= f) overflow = 1n;
+    if (sign === -1n && r < 0n) overflow = -1n;
+    if (f === 0n) overflow = 0n; // special case where overflow doesn't change anything


Why would we like to support foreign field zero? Is that even a thing?

yes I think it could be useful if you want to do plain bigint addition (not modulo a field)

querolita · 2023-11-16T15:59:17Z

src/lib/gadgets/foreign-field.ts

+    // note: this "just works" with negative r01
+    let r01 = collapse2(x_) + sign * collapse2(y_) - overflow * collapse2(f_);
+    let carry = r01 >> twoL;
+    r01 &= twoLMask;


what's twoLMask?

Oh this is 2^176 - 1 perhaps?

querolita · 2023-11-16T16:15:38Z

src/lib/gadgets/range-check.ts

@@ -53,6 +61,7 @@ function rangeCheck64(x: Field) {
 const L = 88n;
 const twoL = 2n * L;
 const lMask = (1n << L) - 1n;
+const twoLMask = (1n << twoL) - 1n;


Oh it is indeed 😄

querolita · 2023-11-16T16:23:09Z

src/lib/proof_system.ts

      publicInputType: publicInputType as ProvableOrUndefined<
        Get<StatementType, 'publicInput'>
      >,
      publicOutputType: publicOutputType as ProvableOrVoid<
        Get<StatementType, 'publicOutput'>
      >,
-      analyzeMethods,
+      privateInputTypes: Object.fromEntries(


What is this exactly for?

querolita · 2023-11-16T16:29:13Z

src/lib/testing/random.ts

-  let specialField = oneOf(0n, 1n, F(-1));
-  let field = oneOf<bigint[]>(randomField, randomField, uint64, specialField);
+  let specialField = oneOf(0n, 1n, F.negate(1n));
+  let roughLogSize = 1 << Math.ceil(Math.log2(F.sizeInBits) - 1);


Why are you using this size?

because the biguint random generator I'm passing it in needs the bit size to be a power of 2 (for efficiency)

Trivo25 · 2023-11-17T11:12:44Z

src/lib/gadgets/foreign-field.ts

+function toField3(x: bigint3): Field3 {
+  return Tuple.map(x, (x) => new Field(x));
+}
+function bigint3(x: Field3): bigint3 {


I would prefer if we could name this toBigint3, similar to toField3 for consistency

mitschabaude added 21 commits November 2, 2023 00:15

ffadd gate wrapper

b441e34

write logic for single ffadd

b07b047

write sumchain gadget

9ac67bf

add another comment

d316ab2

simplify gates imports

c277e35

add and sub

8529dcf

add helpers, return result 0.O

cc7d401

sophisticated random generator for any field

98666ab

handle constant case

1508440

add unit test for add and sub

1ef7165

more example fields

b5cb55c

add a few specs

4def5e5

expose sign

13c0e55

add sumchain tests and with zkprogram

b9c1a00

dang

7e93bf1

automatically reduce inputs to exists for easier use

6adf304

add proof works

ac77339

actually it's easier this way

1b135aa

sub proving works

68ff7da

sumchain works (signs are constants, d'oh)

d4db523

bindings

de3a15c

This was linked to issues Nov 2, 2023

Port FFSum_check gadget to TypeScript #1152

Closed

Port FFadd and FFsub gadget to TypeScript #1180

Closed

Base automatically changed from feature/multi-range-check to main November 3, 2023 16:18

Merge branch 'main' into feature/ffadd

240bc4b

mitschabaude changed the title ~~Foreign field addition~~ Foreign fields 2: addition Nov 13, 2023

mitschabaude changed the title ~~Foreign fields 2: addition~~ Foreign fields 2: Addition Nov 13, 2023

mitschabaude added 3 commits November 13, 2023 08:18

bindings with not operation

b53c875

fixup type

7df0a78

cleanup test

9a83e3c

mitschabaude mentioned this pull request Nov 13, 2023

Foreign field backend o1-labs/o1js-bindings#203

Merged

mitschabaude added 4 commits November 13, 2023 23:13

Merge branch 'feature/cs-test' into feature/ffadd

f43bbd2

make array spec support provable

a250c1c

add failing cs test

bcdbebd

fix test

64dc87a

mitschabaude changed the base branch from main to feature/cs-test November 13, 2023 22:46

mitschabaude marked this pull request as ready for review November 13, 2023 22:50

mitschabaude requested a review from a team as a code owner November 13, 2023 22:50

mitschabaude added 4 commits November 14, 2023 09:39

expose private input types from zkprogram & fix missing Proof

7f5e54f

make it easy to do cs tests on zkprograms

4335d9c

simplify bitwise cs tests

92d0ba5

changelog

54bcbd8

rbonichon reviewed Nov 14, 2023

View reviewed changes

mitschabaude added 7 commits November 14, 2023 11:00

more docs on foreign field namespace

2e5ace3

put provable on Field3

337c696

add doccomments for addition

ff98763

rename sumchain to sum and add docs

df5f7df

move non-provable helpers off of foreignfield namespace

255ad10

adapt unit test

6010ff1

refine docs

fcbeb60

mitschabaude mentioned this pull request Nov 14, 2023

Easier provable tuple types o1-labs/o1js-bindings#205

Merged

mitschabaude commented Nov 14, 2023

View reviewed changes

Base automatically changed from feature/cs-test to main November 16, 2023 15:15

querolita approved these changes Nov 16, 2023

View reviewed changes

Trivo25 approved these changes Nov 17, 2023

View reviewed changes

mitschabaude added 2 commits November 17, 2023 16:00

Merge branch 'main' into feature/ffadd

a433280

better function name

ee766ad

mitschabaude merged commit 21d774f into main Nov 17, 2023
13 checks passed

mitschabaude deleted the feature/ffadd branch November 17, 2023 16:33

mitschabaude mentioned this pull request Nov 22, 2023

Foreign fields 5: Optimized multiplication of sums #1262

Merged

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Foreign fields 3: Addition #1220

Foreign fields 3: Addition #1220

mitschabaude commented Nov 2, 2023 •

edited

Loading

rbonichon Nov 14, 2023

mitschabaude Nov 14, 2023

mitschabaude left a comment

mitschabaude Nov 14, 2023

mitschabaude Nov 14, 2023

mitschabaude Nov 14, 2023

mitschabaude Nov 14, 2023

mitschabaude Nov 14, 2023

mitschabaude Nov 14, 2023

querolita Nov 16, 2023

mitschabaude Nov 16, 2023

mitschabaude Nov 14, 2023

mitschabaude Nov 14, 2023

mitschabaude Nov 14, 2023

querolita left a comment

querolita Nov 16, 2023

querolita Nov 16, 2023

mitschabaude Nov 16, 2023

querolita Nov 16, 2023

mitschabaude Nov 16, 2023

querolita Nov 16, 2023

querolita Nov 16, 2023

mitschabaude Nov 16, 2023

querolita Nov 16, 2023

querolita Nov 16, 2023

mitschabaude Nov 16, 2023

querolita Nov 16, 2023

querolita Nov 16, 2023

querolita Nov 16, 2023

querolita Nov 16, 2023

querolita Nov 16, 2023

mitschabaude Nov 16, 2023

Trivo25 Nov 17, 2023

Foreign fields 3: Addition #1220

Foreign fields 3: Addition #1220

Conversation

mitschabaude commented Nov 2, 2023 • edited Loading

Proof that we can save range checks in sum()

Choose a reason for hiding this comment

Choose a reason for hiding this comment

mitschabaude left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

querolita left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

mitschabaude commented Nov 2, 2023 •

edited

Loading

Proof that we can save range checks in `sum()`