Foreign fields 2: Test DSL to detect broken gate chains #1241

mitschabaude · 2023-11-13T14:00:19Z

Adds a new DSL for testing constraint system layouts -- see testing/constraint-system.ts
Uncovers and fixes broken gate chains in multi-range check and rotation/shift gadgets
Remove unnecessary avoidance of constant input to xor gate

This is how a test in the DSL looks like. It asserts properties about the constraint system generated by Gadgets.multiRangeCheck(). Namely, it checks that the CS contains the sequence 'RangeCheck0', 'RangeCheck0', 'RangeCheck1', 'Zero' (except if all inputs are constant; in this case, it asserts that the CS is empty).

constraintSystem(
  'multi-range check',
  { from: [Field, Field, Field] },
  (x, y, z) => Gadgets.multiRangeCheck([x, y, z]),
  ifNotAllConstant(
    contains(['RangeCheck0', 'RangeCheck0', 'RangeCheck1', 'Zero'])
  )
);

Below is test output for the original, broken version of multi-range check. To help with debugging these tests, we try to pretty-print the CS in a way that is compact but not leaves out important details.

In this example, the CS contains a generic gate (at index 2) that breaks the expected chain of multi-range check gates, which makes it invalid. This is exactly the kind of bug that the DSL is designed to catch.

mitschabaude

some comments to help with reviewing

mitschabaude · 2023-11-13T16:48:05Z

src/lib/gadgets/bitwise.ts

-  let allOnesF = new Field(2n ** BigInt(length) - 1n);
-
-  let allOnes = Provable.witness(Field, () => {
-    return allOnesF;
-  });
-
-  allOnesF.assertEquals(allOnes);
+  let allOnes = new Field(2n ** BigInt(length) - 1n);


defensive logic like this is no longer necessary - we can easily check that the resulting gate layout is correct

mitschabaude · 2023-11-13T16:48:42Z

src/lib/gadgets/bitwise.ts

+  // flush zero var to prevent broken gate chain (zero is used in rangeCheck64)
+  // TODO this is an abstraction leak, but not clear to me how to improve
+  toVar(0n);


the kind of thing that is impossible to catch without tests

In OCaml we had a PR where whenever you add a gate it adds a "shadow row" that specifies what the next row should be with Some or None (for anything), per cell in the next row.

I guess this PR is about something similar.

We also had some tests which added an even/odd number of generic operations before calling the actual gadget so that in case the gadget was creating some "orphan" generic which was coincidentally correctly pushed to the end of the chain, we could catch it and fix the gadget accordingly. Do you think this could make sense in your tests?

@querolita I think my tests already exhibit that case, because I am creating random linear combinations of variables as inputs, something like x + 20y + 3z + 17, and this will generate an even or odd number of generic gates when passed to a gate, depending on the length of the linear combination. Since we test many random inputs, I'm pretty sure all cases are covered

In OCaml we had a PR where whenever you add a gate it adds a "shadow row" that specifies what the next row should be with Some or None (for anything), per cell in the next row.

That sounds interesting! Do you know where that PR is?

mitschabaude · 2023-11-13T16:49:52Z

src/lib/gadgets/range-check.ts

+  // ensure we are using pure variables
+  [x, y, z] = toVars([x, y, z]);
+  let zero = toVar(0n);


this is what fixed the multi-range check gadget

mitschabaude · 2023-11-13T16:50:14Z

src/lib/gadgets/range-check.ts

+  // ensure we are using pure variables
+  [xy, z] = toVars([xy, z]);


fix for the compact range check gadget

mitschabaude · 2023-11-13T16:51:24Z

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

+constraintSystem(
+  'compact multi-range check',
+  { from: [Field, Field] },
+  Gadgets.compactMultiRangeCheck,
+  ifNotAllConstant(
+    contains(['RangeCheck0', 'RangeCheck0', 'RangeCheck1', 'Zero'])
+  )
+);


removing ad-hoc tests which didn't catch the bugs in favor of comprehensive tests using the DSL

mitschabaude · 2023-11-13T16:54:03Z

src/lib/proof_system.ts

+      rawMethods: Object.fromEntries(
+        Object.entries(methods).map(([k, v]) => [k, v.method])
+      ) as any,


you can now access the original zkprogram methods (not wrapped to return proofs) on program.rawMethods. this was asked for by community members as well and it helped me reuse the methods for tests in this PR

mitschabaude · 2023-11-13T16:54:56Z

src/lib/testing/constraint-system.ts

This is the new code! I think it's pretty well-documented with comments

MartinMinkov

This is fantastic! Bonus points for your DSL design, seems straightforward to extend it! But you added a pretty extensive suite for our Gadgets already! 🎉

ymekuria

This is great @mitschabaude! I just had a question.

ymekuria · 2023-11-13T20:10:09Z

src/lib/gadgets/bitwise.ts


  if (checked) {
    return xor(a, allOnes, length);
  } else {
-    return allOnes.sub(a);
+    return allOnes.sub(a).seal();


What does .seal() do here?

It makes sure that the constraint created by the subtraction is added at this point. In my tests I found that the constraint system created by unchecked not() is empty (I would have expected a generic gate, for the subtraction).

It was empty because additions and subtractions are treated as a form of lazy constraint / AST, which are only turned into an actual constraint once the result is included in some multiplication or assertion or custom gate.

seal() triggers that concretizing of the AST, by creating a new variable that is asserted equal with the old variable, so with seal() this gadget immediately leads to a generic gate in the CS. I thought this was the better behavior for a gadget, as it's normalized and not dependent on the remaining circuit where this subtraction will end up in the CS.

So seal() is for making sure snarky doesn't add generic gates where they are not desired (e.g. in the middle of a chained gate)?

The snarky version of seal() could be used for that! The o1js version not because it doesn't "seal" constants. The o1js version was intended more to prevent unnecessary large numbers of constraints when the same long AST is flushed to generic gates again and again. The function added in this PR that does what you descirbe @jspada is called toVar()

jspada

I think this code is great. Approved with some minor suggestions and reminders.

jspada · 2023-11-14T15:32:31Z

src/lib/field.ts

-  // TODO: handle (special) constants
-  scale(c: FieldConst, x: FieldVar): FieldVar {
-    return [FieldType.Scale, c, x];
+  scale(c: bigint | FieldConst, x: FieldVar): FieldVar {


Just a note from our discussion of this code.

Remember to do the "collapsing" of scale that the OCaml code does, i.e. Scale a (Scale b x) becomes Scale a*b x

jspada · 2023-11-14T15:34:02Z

src/lib/field.ts

  add(x: FieldVar, y: FieldVar): FieldVar {
+    if (FieldVar.isConstant(x) && x[1][1] === 0n) return y;


If you do these types of checks often, perhaps you want to create a FieldVar.isZeroConst(x) helper for brevity.

jspada · 2023-11-14T16:02:05Z

src/lib/gadgets/bitwise.ts


  if (checked) {
    return xor(a, allOnes, length);
  } else {
-    return allOnes.sub(a);
+    return allOnes.sub(a).seal();


So seal() is for making sure snarky doesn't add generic gates where they are not desired (e.g. in the middle of a chained gate)?

jspada · 2023-11-14T16:05:11Z

src/lib/gadgets/bitwise.ts

+  // flush zero var to prevent broken gate chain (zero is used in rangeCheck64)
+  // TODO this is an abstraction leak, but not clear to me how to improve
+  toVar(0n);


In OCaml we had a PR where whenever you add a gate it adds a "shadow row" that specifies what the next row should be with Some or None (for anything), per cell in the next row.

I guess this PR is about something similar.

jspada · 2023-11-14T17:14:31Z

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

+// check that gate chains stay intact
+
+function xorChain(bits: number) {
+  return repeat(Math.ceil(bits / 16), 'Xor16').concat('Zero');


jspada · 2023-11-15T07:15:51Z

src/lib/gadgets/common.ts

+ * Given a Field, collapse its AST to a pure Var. See {@link FieldVar}.
+ *
+ * This is useful to prevent rogue Generic gates added in the middle of gate chains,
+ * which are caused by snarky auto-resolving constants, adds and scales to vars.


This is really awesome

jspada · 2023-11-15T07:20:01Z

src/lib/gadgets/common.ts

+ *
+ * Same as `Field.seal()` with the difference that `seal()` leaves constants as is.
+ */
+function toVar(x: Field | bigint) {


Maybe this is better called ConstrainConstantHere or something like that?

it's not just for constants though!

jspada · 2023-11-15T07:20:40Z

src/lib/gadgets/common.ts

+/**
+ * Apply {@link toVar} to each element of a tuple.
+ */
+function toVars<T extends Tuple<Field | bigint>>(


ConstrainConstantsHere?

querolita

Very useful for debugging, congrats!

querolita · 2023-11-15T12:44:47Z

src/lib/gadgets/bitwise.ts

+  // flush zero var to prevent broken gate chain (zero is used in rangeCheck64)
+  // TODO this is an abstraction leak, but not clear to me how to improve
+  toVar(0n);


We also had some tests which added an even/odd number of generic operations before calling the actual gadget so that in case the gadget was creating some "orphan" generic which was coincidentally correctly pushed to the end of the chain, we could catch it and fix the gadget accordingly. Do you think this could make sense in your tests?

querolita · 2023-11-15T12:46:38Z

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

+  'and',
+  { from: [Field, Field] },
+  Bitwise.rawMethods.and,
+  ifNotAllConstant(contains(xorChain(64)))


Are you only supporting And64 then?

no, this tests a specific example circuit -- the and() method on the Bitwise zkprogram, which happens to use 64-bit and. but we support all bit lengths

querolita · 2023-11-15T12:47:31Z

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

+  ifNotAllConstant(contains(xorChain(64)))
+);
+
+let rotChain: GateType[] = ['Rot64', 'RangeCheck0', 'RangeCheck0'];


Nice, but remember to have copy constraints to the RangeCheck0's to constant zero for the two most significant sublimbs to make it 64-bit instead of 88-bit.

mitschabaude added 9 commits November 13, 2023 11:24

first version of constraint system test dsl

d98e3a2

properly implement fieldvar combinators

1e5919b

pass inputs to cs tests, and make them combinable

4605ad2

more cs tests and combinators

4f68250

replace existing test with new dsl test, which passes

c6c4f97

usability tweaks

d17d47f

tweak error output

ff73b23

replace other test and expose bug where generic gate disrupts mrc chain

657d28f

print constraint system

1e4a1a0

mitschabaude changed the title ~~Test DSL to detect broken gate chains~~ Add test DSL to detect broken gate chains Nov 13, 2023

mitschabaude added 11 commits November 13, 2023 15:31

add utils to flush generic gates early

dfffeda

fix range check gadgets

2604f54

fix equals, usability tweaks

fb5ad69

expose raw methods from zkprogram

ad137ed

test bitwise cs, fix rot, clean up not

f4a0bfe

bindings

9759938

more verbose but clearer type name

82e5d28

document test runner

3e0fabb

changelog

015d29f

dump vks

5883f5e

tweak comments

bd35877

mitschabaude marked this pull request as ready for review November 13, 2023 16:28

mitschabaude requested a review from a team as a code owner November 13, 2023 16:28

more changelog

2a95ca8

mitschabaude commented Nov 13, 2023

View reviewed changes

mitschabaude changed the title ~~Add test DSL to detect broken gate chains~~ Foreign fields 2: Test DSL to detect broken gate chains Nov 13, 2023

MartinMinkov approved these changes Nov 13, 2023

View reviewed changes

ymekuria approved these changes Nov 14, 2023

View reviewed changes

mitschabaude mentioned this pull request Nov 14, 2023

Foreign fields 3: Addition #1220

Merged

jspada approved these changes Nov 15, 2023

View reviewed changes

querolita approved these changes Nov 15, 2023

View reviewed changes

Merge branch 'main' into feature/cs-test

4b400e4

mitschabaude merged commit aec1e89 into main Nov 16, 2023
13 checks passed

mitschabaude deleted the feature/cs-test branch November 16, 2023 15:15

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Foreign fields 2: Test DSL to detect broken gate chains #1241

Foreign fields 2: Test DSL to detect broken gate chains #1241

mitschabaude commented Nov 13, 2023 •

edited

Loading

mitschabaude left a comment

mitschabaude Nov 13, 2023

mitschabaude Nov 13, 2023

jspada Nov 14, 2023

querolita Nov 15, 2023

mitschabaude Nov 16, 2023

mitschabaude Nov 16, 2023

mitschabaude Nov 13, 2023

mitschabaude Nov 13, 2023

mitschabaude Nov 13, 2023

mitschabaude Nov 13, 2023

mitschabaude Nov 13, 2023

MartinMinkov left a comment

ymekuria left a comment

ymekuria Nov 13, 2023

mitschabaude Nov 14, 2023 •

edited

Loading

jspada Nov 14, 2023

mitschabaude Nov 16, 2023

jspada left a comment

jspada Nov 14, 2023

jspada Nov 14, 2023

jspada Nov 14, 2023

jspada Nov 14, 2023

jspada Nov 14, 2023

jspada Nov 15, 2023

jspada Nov 15, 2023

mitschabaude Nov 16, 2023

jspada Nov 15, 2023

querolita left a comment

querolita Nov 15, 2023

querolita Nov 15, 2023

mitschabaude Nov 16, 2023

querolita Nov 15, 2023

		// ensure we are using pure variables
		[xy, z] = toVars([xy, z]);

		add(x: FieldVar, y: FieldVar): FieldVar {
		if (FieldVar.isConstant(x) && x[1][1] === 0n) return y;

Foreign fields 2: Test DSL to detect broken gate chains #1241

Foreign fields 2: Test DSL to detect broken gate chains #1241

Conversation

mitschabaude commented Nov 13, 2023 • edited Loading

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

MartinMinkov left a comment

Choose a reason for hiding this comment

ymekuria left a comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

mitschabaude Nov 14, 2023 • edited Loading

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

jspada 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

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

mitschabaude commented Nov 13, 2023 •

edited

Loading

mitschabaude Nov 14, 2023 •

edited

Loading