Expose lookup constraint and implement three12Bit gadget for Keccak #1284

jackryanservia · 2023-12-01T14:53:01Z

Implementation of three12Bit for #1146.

jackryanservia · 2023-12-01T15:01:22Z

src/lib/gadgets/lookup.ts

Does it make sense for me to add another function threeHoweverManyBits(bits0, value0, ...) that also handles the scaling here, or does that just clutter things up?

just note that you need to use two lookup slots per input for a different number of checked bits. assuming three inputs at a time is still a good API in that case because 3*2 exactly fit in 2 lookup gates!

jackryanservia · 2023-12-01T15:12:50Z

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

+let Lookup = ZkProgram({
+  name: 'lookup',
+  methods: {
+    three12Bit: {
+      privateInputs: [Field, Field, Field],
+      method(v0: Field, v1: Field, v2: Field) {
+        // Dummy range check to make sure the lookup table is initialized
+        // It should never fail because 64 > 12
+        Gadgets.rangeCheck64(v0);
+        Gadgets.three12Bit(v0, v1, v2);
+      },
+    },
+  },
+});


I wasn't able to get the ZkProgram to compile unless I included rangeCheck64. Without it the process would just hang and not use any CPU time. I spent an hour or so trying to figure out why before I added rangeCheck64. Is this because of the dummy gate thing?

Oh I see, so it was not fixed eventually? I would have sweared that it was addressed at some point in the summer... Well, yes, a few months ago, it wouldn't work unless your circuit had a previous gate which was already using the range check table, even if it is just a dummy zero value. But you needed to include that row... Seems like it is still the case 😞

nice @jackryanservia - I guess you found out why #1253 wasn't working, so we can land that PR as well

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

querolita

Looks good to me, but I wonder if this is a functionality that should be provided to zkapp developers or if it should remain as an internal feature inside o1js.

src/lib/gadgets/gadgets.ts

querolita · 2023-12-01T15:35:42Z

src/lib/gadgets/gadgets.ts

+   * let a = Field(4000);
+   * let b = a.mul(2 ** 4); // scale `a` so we can check if it's less than 8 bits
+   * three12Bit(a, a, a); // works
+   * three12Bit(a, a, b); // throws an error since b is greater than 12 bits (and `a` is greater than 8 bits)


Take into account that in order to check that $x < 2^8$ both checks need to happen: both $x < 2^{12}$ and $x * 2^4 < 2^{12}$, meaning that both terms (x and scaled_x) need to be passed as params of the three12Bit function (maybe with a zero in v2). I am pointing this out because from the way it is expressed in the comment, the exact behavior is not super clear.

Meaning, for this to be sound (to make sure you're really proving $x < 2^8$ and not something else) it is not sufficient to pass the scaled x. That's because it can be the case that $x * 2^4 < 2^12$ because the multiplication "wraps around$, but $x > 2^12$. Both checks are needed, and for that reason I believe that exposing a less error prone interface with the exact number of bits that you want to be checked, and the value, is preferable. Even if that other interface used three12Bit under the hood.

Maybe you need this function to be exposed in any case for you to be able to use it in the code? Otherwise, I would only expose a more high level interface for final users.

querolita · 2023-12-01T15:36:32Z

src/lib/gadgets/lookup.ts

+export { three12Bit };
+
+function three12Bit(v0: Field, v1: Field, v2: Field) {
+  // Checks that all three input values exist in the RANGE_CHECK_TABLE (tableId: 1) and are equal to 0.


and are equal to 0.

I don't get this part

Ahhh, yes, this isn't worded very well. I was trying to express that the hard-coded zeros are the values in the table at the index we are looking up, but I don't think it needs to be explained. I will just abstract over this as you suggested.

querolita · 2023-12-01T15:37:18Z

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

+      method(v0: Field, v1: Field, v2: Field) {
+        // Dummy range check to make sure the lookup table is initialized
+        // It should never fail because 64 > 12
+        Gadgets.rangeCheck64(v0);


I wonder if having this dummy range check is still needed

querolita · 2023-12-01T15:38:26Z

src/lib/gates.ts

+ * @param value2 the third value to lookup.
+ *
+ */
+function lookup(


Maybe don't expose this to the very end user? It is a bit low level.

gates are not currently exported from o1js! but I think they will eventually, having both low- and high-level APIs makes sense IMO

mitschabaude

Good stuff!

Feedback:

can you add a changelog item about the gadget?
maybe we can come up with a better name than three12bit?
the three12bit doccomment must not trick users into only range-checking $x2^{12-n}$, because we're in a finite field and all values, including $2^{12-n}$, have inverses, so you can trivially pick an $x$ which violates the supposed range check

mitschabaude · 2023-12-01T21:41:37Z

src/lib/gadgets/gadgets.ts

+   * Checks that three {@link Field} elements are less than 2^12 (using only one row) by verifying that they exist in the [RANGE_CHECK_TABLE](https://github.com/o1-labs/proof-systems/blob/master/kimchi/src/circuits/lookup/tables/mod.rs).
+   *
+   * It's possible to use this to check that a value is less than x bits by scaling the value by 2^(12 - x) before passing it in (with x < 12).


as Anais said below, this has to make clearer that for checking fewer bits you have to check both $z$ and $z 2^{12-x}$.

also, nit: x is not the best variable to use for an exponent here because we use it everywhere for field elements (usually in mathematics you try to pick different symbols for different kinds of value). exponent could be $i$ or $n$ or $e$ for example

mitschabaude · 2023-12-01T21:44:47Z

src/lib/gadgets/lookup.ts

just note that you need to use two lookup slots per input for a different number of checked bits. assuming three inputs at a time is still a good API in that case because 3*2 exactly fit in 2 lookup gates!

mitschabaude · 2023-12-01T21:47:11Z

src/lib/gadgets/gadgets.ts

+   * three12Bit(a, a, b); // throws an error since b is greater than 12 bits (and `a` is greater than 8 bits)
+   * ```
+   */
+  three12Bit(v0: Field, v1: Field, v2: Field) {


can we name this function more similarly to other range check gadgets? we have rangeCheck64 and rangeCheck32, as well as multiRangeCheck for the 3x88 bit check. this one could be rangeCheck12x3 maybe? at least it should say "range check"

mitschabaude · 2023-12-01T21:49:51Z

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

+let Lookup = ZkProgram({
+  name: 'lookup',
+  methods: {
+    three12Bit: {
+      privateInputs: [Field, Field, Field],
+      method(v0: Field, v1: Field, v2: Field) {
+        // Dummy range check to make sure the lookup table is initialized
+        // It should never fail because 64 > 12
+        Gadgets.rangeCheck64(v0);
+        Gadgets.three12Bit(v0, v1, v2);
+      },
+    },
+  },
+});


nice @jackryanservia - I guess you found out why #1253 wasn't working, so we can land that PR as well

mitschabaude · 2023-12-01T21:53:02Z

src/lib/gates.ts

+ * @param value2 the third value to lookup.
+ *
+ */
+function lookup(


gates are not currently exported from o1js! but I think they will eventually, having both low- and high-level APIs makes sense IMO

mitschabaude · 2023-12-01T22:00:09Z

oh - the lookup unit test fails, during proving the zkprogram. I wonder why it worked on your machine 🤔

EDIT: doesn't work for me either

jackryanservia added 2 commits December 1, 2023 14:48

Expose lookup constraint

9db5cd6

three12Bit gadget

4b3d672

jackryanservia requested review from a team and mitschabaude as code owners December 1, 2023 14:53

Fixed maybeUint values in lookup test

d667484

jackryanservia commented Dec 1, 2023

View reviewed changes

querolita approved these changes Dec 1, 2023

View reviewed changes

Fix doccomment for three12bit

a3db2b0

mitschabaude reviewed Dec 1, 2023

View reviewed changes

make lookup unit test only use the happy path for now

e165852

mitschabaude mentioned this pull request Dec 4, 2023

Range check 8 #1288

Merged

Add comment to make piRoh more clear (hopefully)

a03c437

Base automatically changed from feature/keccak-block-transformation to main December 4, 2023 13:43

dannywillems mentioned this pull request Dec 5, 2023

[o1js-main] Add missing runtime table commits in wrap verifier. MinaProtocol/mina#14662

Closed

7 tasks

mitschabaude mentioned this pull request Jan 16, 2024

Bug: Cannot use lookup gate with range check table #1374

Closed

mitschabaude mentioned this pull request Apr 4, 2024

Bump bindings and Mina repo for lookup gate fix #1534

Merged

mitschabaude merged commit 3ce785c into main Apr 5, 2024

mitschabaude deleted the feature/keccak-lookup branch April 5, 2024 10:24

Expose lookup constraint and implement three12Bit gadget for Keccak #1284

Expose lookup constraint and implement three12Bit gadget for Keccak #1284

Uh oh!

Conversation

jackryanservia commented Dec 1, 2023

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Uh oh!

querolita left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

mitschabaude left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

mitschabaude commented Dec 1, 2023 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

mitschabaude commented Dec 1, 2023 •

edited

Loading