Hints for arithmetic machine #1005

georgwiese · 2024-02-01T17:10:44Z

Adds hints to the arithmetic machine, which fixes witness generation. I also converted Polygon's test cases.

std/arith.asm

georgwiese · 2024-02-14T16:36:23Z

std/arith.asm

+        (|x1, y1, x2, s|
+            (|x3|
+                compute_q2(x1, y1, x3, compute_y3_int(x1, y1, x3, s), s, limb_index)
+            )(compute_x3_int(x1, x2, s))
+        )(x1_int(i), y1_int(i), x2_int(i), s_int(i))


This used to be:
compute_q2(x1_int(i), y1_int(i), compute_x3_int(x1_int(i), x2_int(i), s_int(i)), compute_y3_int(x1_int(i), y1_int(i), compute_x3_int(x1_int(i), x2_int(i), s_int(i)), s_int(i)), s_int(i), limb_index)

This get's rid of duplicate calls to various functions. If we had let statements, the equivalent code would be:

let x1 = x1_int(i); let y1 = y1_int(i); let x2 = x2_int(i); let s = s_int(i); let x3 = compute_x3_int(x1, x2, s); let y3 = compute_y3_int(x1, y1, x3, s); compute_q2(x1, y1, x3, y3,, s, limb_index)

georgwiese · 2024-02-14T16:43:20Z

test_data/std/arith_test.asm

@@ -103,7 +103,7 @@ machine Main{
        assert_eq t_0_0, t_0_1, t_0_2, t_0_3, t_0_4, t_0_5, t_0_6, t_0_7, 0x9be02469, 0xf258bf25, 0x38e38e38, 0xe6f8091a, 0x740da740, 0x579be024, 0x091a2b3c, 0x00000000;
        assert_eq t_1_0, t_1_1, t_1_2, t_1_3, t_1_4, t_1_5, t_1_6, t_1_7, 0x33333333, 0xa1907f6e, 0xca8641fd, 0x369d0369, 0x907f6e5d, 0x60b60b60, 0x0da740da, 0x1fdb9753;

-        // Test vectors from: https://github.com/0xPolygonHermez/zkevm-proverjs/blob/main/test/sm/sm_arith.js
+        // Test vectors from: https://github.com/0xPolygonHermez/zkevm-proverjs/blob/a4006af3d7fe4a57a85500c01dc791fb5013cef0/test/sm/sm_arith.js


In the meantime, Polygon has a new test file, because they also added additional equation to the arithmetic machine.

georgwiese · 2024-02-14T16:44:06Z

test_data/std/arith_test.asm

+        assert_eq t_1_0, t_1_1, t_1_2, t_1_3, t_1_4, t_1_5, t_1_6, t_1_7, 0x6a255906, 0xb1976404, 0x3c3747d4, 0xebd4f608, 0x6bd3bbf, 0x40d90c4b, 0x23adb6fd, 0xb5196132;
+
+        // Left out these test cases, because the format is different...
+        // https://github.com/0xPolygonHermez/zkevm-proverjs/blob/a4006af3d7fe4a57a85500c01dc791fb5013cef0/test/sm/sm_arith.js#L1196-L1211


Not sure if these are important; they might have just wanted to test their addPoint() JS function?

georgwiese · 2024-02-14T17:10:17Z

pipeline/tests/powdr_std.rs

@@ -44,7 +44,8 @@ fn split_gl_test() {
 fn arith_test() {
    let f = "std/arith_test.asm";
    verify_test_file::<GoldilocksField>(f, Default::default(), vec![]);
-    gen_estark_proof(f, Default::default());
+    // Otherwise, we get: thread 'arith_test' has overflowed its stack
+    // gen_estark_proof(f, Default::default());


😢 I wonder why this happens. This line works just fine:
cargo run --features halo2 -r pil test_data/std/arith_test.asm -o output -f --prove-with estark

Also, I didn't add any columns or constraints in this PR (except maybe the main machine in arith_test.asm), so I don't see how it would make a difference for eStark?

Maybe we should investigate this a bit. Is it only a problem for us?

So what's strange is that that's only in the test, I can generate an eStark proof for this in the command line (but maybe it's just below the limit). We also have this in several other tests, so it's not a problem unique to the arithmetic machine.

Looks like this problem just disappeared.

Tests run in threads with limited memory iirc

chriseth · 2024-02-15T13:07:19Z

std/arith.asm

+    let s_for_eq2 = |x1, y1, limb_index| (div(mul(3, mul(x1, x1)), mul(2, y1)) >> (limb_index * 16)) & 0xffff;
+
+    let compute_x3_int = |x1, x2, s| (s * s - x1 - x2 + 2 * secp_modulus) % secp_modulus;
+    let compute_y3_int = |x1, y1, x3, s| (s * (((x1 - x3) + secp_modulus) % secp_modulus) - y1 + secp_modulus) % secp_modulus;


Why the intermediate % secp_modulus?

Also + secp_modulus) % secp_modulus?

Why the intermediate % secp_modulus?

True, I can remove that. I it reduces the size of the big int before doing the addition, but probably not worth it.

Also + secp_modulus) % secp_modulus?

That's needed because % behaves weird on negative numbers, e.g. -1 % 5 = -1. Adding the modulus ensures % is only applied to positive numbers. I'll add a comment.

chriseth · 2024-02-15T13:19:01Z

std/arith.asm

+    let compute_y3_int = |x1, y1, x3, s| (s * (((x1 - x3) + secp_modulus) % secp_modulus) - y1 + secp_modulus) % secp_modulus;
+
+    // Note that the most significant limb is 32-Bit instead of 16
+    let compute_q0_for_eq1 = |x1, y1, x2, y2, s, limb_index| ((-(s * x2 - s * x1 - y2 + y1) / secp_modulus + (1 << 258)) >> (limb_index * 16)) & if limb_index < 15 { 0xffff } else { 0xffffffff };


Can you split those up a bit? I cannot really parse it.

Yeah, good call! I made a select_limb(x, limb_index) function, and actually pulled it out all the way to the actual hint. This has the extra benefit that the evaluation cache will be much more efficient, because e.g. compute_q0_for_eq1 won't have a limb_index argument anymore!

chriseth · 2024-02-15T13:20:01Z

std/arith.asm

+    let compute_q1 = |x1, x2, x3, s, limb_index| ((-(s * s - x1 - x2 - x3) / secp_modulus + (1 << 258)) >> (limb_index * 16)) & if limb_index < 15 { 0xffff } else { 0xffffffff };
+    let compute_q2 = |x1, y1, x3, y3, s, limb_index| ((-(s * x1 - s * x3 - y1 - y3) / secp_modulus + (1 << 258)) >> (limb_index * 16)) & if limb_index < 15 { 0xffff } else { 0xffffffff };
+
+    let limbs_to_int = |limbs, row| array::sum(array::new(array::len(limbs), |i| int(limbs[i](row)) << (i * 16)));


We could add a map_enumerated function to array.

chriseth · 2024-02-15T13:22:30Z

std/arith.asm

+    let x3_int: int -> int = |row| limbs_to_int(x3, row);
+    let s_int: int -> int = |row| limbs_to_int(s, row);
+
+    let s_hint = |i, limb_index| if selEq[1](i) == fe(1) {


Ok, here we really need to evaluate a witness column. So for this I need to add a builtin eval function, but I think this should be doable.

std/arith.asm

chriseth · 2024-03-13T16:15:06Z

std/arith.asm

+
+    let limbs_to_int: expr[] -> int = |limbs| array::sum(array::map_enumerated(limbs, |i, limb| int(eval(limb)) << (i * 16)));
+
+    let x1_int: -> int = || limbs_to_int(x1);


Ok this is a bit weird because in a pure functional sense, this should be a constant. Maybe we can at some point also mark functions that need to be evaluated in a query context.

What is also not very clear to me is that the way this ends up being used is:

col witness s_0(i) query ("hint", fe(select_limb(s_hint(), 0)));

So the call to s_hint() is evaluated at witgen time (because otherwise it would hit eval(), which would fail?). Maybe it would be good to make that explicit somehow, e.g.:

col witness s_0: witness = |i| ("hint", fe(select_limb(s_hint(), 0)));

Then witness and fixed columns would be specified the same, but depending on the type the callback gets executed in different phases? I think that would also give us arrays of witness columns with hints, just like we already have arrays of fixed column?

chriseth · 2024-03-13T16:16:27Z

std/arith.asm

+    let x3_int: -> int = || limbs_to_int(x3);
+    let s_int: -> int = || limbs_to_int(s);
+
+    let s_hint: -> int = || if eval(selEq[1]) == 1 {


maybe have a helper function eq1_active()?

chriseth · 2024-03-13T16:17:31Z

std/arith.asm

+    };
+
+    let q0_hint: -> int = || if eval(selEq[1]) == 1 {
+        compute_q0_for_eq1(x1_int(), y1_int(), x2_int(), y2_int(), s_int())


Does it make sense to pass the x1_int etc functions if the are always the same? I think this has a too big danger for mixing up the different arguments.

I started doing that but we'll still want to do the (|x1, y1, ...| ...)(x1_int(), y2_int()) trick so we don't have to re-compute the integers if they are used multiple times. So I don't really see an improvement, maybe when we have let statements that changes.

chriseth · 2024-03-13T16:18:32Z

test_data/std/arith_test.asm

+        assert_eq t_1_0, t_1_1, t_1_2, t_1_3, t_1_4, t_1_5, t_1_6, t_1_7, 0x762cef4, 0xbbc02738, 0xc062b742, 0xbe040a8, 0x40e28465, 0xf6f29283, 0x68008032, 0x912770e0;
+
+        t_0_0, t_0_1, t_0_2, t_0_3, t_0_4, t_0_5, t_0_6, t_0_7, t_1_0, t_1_1, t_1_2, t_1_3, t_1_4, t_1_5, t_1_6, t_1_7 <== ec_double(
+            0x33ce1752, 0xc7b750f7, 0xd7cd204e, 0xe783c797, 0xd99c9aea, 0x812ddf64, 0xd01dc635, 0xd7a0da58,


You can use proper integers now.

What do you mean?

Oh I thought these are split into limbs because the parser cannot parse large numbers, but it's because of the registers.

georgwiese · 2024-03-14T14:57:32Z

std/arith.asm

+        12 => "ec_double",
+        _ => panic("Unknown operation")
+    };
+    let is_ec_operation: -> int = || match get_operation() {


This should return a bool, but I couldn't make it work:

Returning true and false didn't work (can't find the symbol). Are these literals not available?

Returning get_operation() != "affine_256" didn't work (string doesn't implement equality).

You can add the boolean constants as let true = (1 == 1) or something.

Ah probably 1 > 0, otherwise the type is not uniquely defined.

Hmm, I tried:

let true = 1 >= 1; let false = 1 > 1;

But this gives me:

Error during type inference: Error specializing generic references in main_arith.true: Unable to derive concrete type for literal 1. Error specializing generic references in main_arith.true: Unable to derive concrete type for literal 1. Error specializing generic references in main_arith.false: Unable to derive concrete type for literal 1. Error specializing generic references in main_arith.false: Unable to derive concrete type for literal 1.

georgwiese · 2024-03-14T14:58:23Z

std/arith.asm

+        1 => "affine_256",
+        10 => "ec_add",
+        12 => "ec_double",


I think soon we'll be able to use enums? :)

chriseth · 2024-03-15T10:21:01Z

std/arith.asm

+    let compute_x3_int = |x1, x2, s| (s * s - x1 - x2 + 2 * secp_modulus) % secp_modulus;
+    let compute_y3_int = |x1, y1, x3, s| (s * ((x1 - x3) + secp_modulus) - y1 + secp_modulus) % secp_modulus;
+
+    // Compute quotients for the various equation.


Suggested change

// Compute quotients for the various equation.

// Compute quotients for the various equations.

chriseth · 2024-03-15T10:27:54Z

std/arith.asm

+    // Note that the most significant limb can be up to 32 bits; all others are 16 bits.
+    let select_limb = |x, i| fe((x >> (i * 16)) & if i < 15 { 0xffff } else { 0xffffffff });
+
+    let s_for_eq1 = |x1, y1, x2, y2| div(sub(y2, y1), sub(x2, x1));


Should we not make this

Suggested change

let s_for_eq1 = |x1, y1, x2, y2| div(sub(y2, y1), sub(x2, x1));

let s_for_eq1 = || div(sub(y2_int(), y1_int()), sub(x2_int(), x1_int()));

Hmm, sure, but for other functions like s_for_eq2, this would mean computing the same number twice. And doing it only for s_for_eq1 is inconsistent. So I'd leave it like this for now and revisit once we have let statements.

chriseth · 2024-03-15T10:29:09Z

std/arith.asm

+    };
+
+    let q1_hint: -> int = || if is_ec_operation() == 1 {
+        // TODO: Make this more readable once we have let statements


Is this for performance reasons?

Yes! So we don't compute x1 and x2 twice.

chriseth · 2024-03-15T10:30:51Z

std/arith.asm

-        0xffff, 0xffff, 0xffff, 0xffff, 0xffff, 0xffff, 0xffff, 0xffff
-    ]);
+    let p: int -> expr = |i| if i >= 0 && i < 16 {
+        expr((secp_modulus >> (i * 16)) & 0xffff)


We could use a byte_slice function here (and also use that for select_limb?)

You mean a function that can select arbitrary bit ranges? Seems a bit overkill, no?

I just tried having a select_limb: int, int -> int function and using it here. I'm getting a stack overflow! I'll look into why, hopefully it's something we can fix.

I just tried the same thing again and it worked 😮 Maybe I did something wrong the other day.

The main problem I have with this is matching i * 16 with & 0xffff, but it's fine.

chriseth · 2024-03-15T10:31:06Z

std/arith.asm


-    let eq1 = (|| |nr| product(sf, x2f)(nr) - product(sf, x1f)(nr) - y2f(nr) + y1f(nr) + product_with_p(q0f)(nr))();
+    let eq1: int -> expr = |nr| product(sf, x2f)(nr) - product(sf, x1f)(nr) - y2f(nr) + y1f(nr) + product_with_p(q0f)(nr);


Do you really need the explicit type?

Looks like I don't! Also many other type declarations.

georgwiese force-pushed the arith-hints branch from 62326e4 to 3a0e339 Compare February 2, 2024 10:32

georgwiese force-pushed the ec-add branch 2 times, most recently from ac33b86 to fc52613 Compare February 6, 2024 16:04

georgwiese force-pushed the arith-hints branch 3 times, most recently from cf20314 to b9826bd Compare February 7, 2024 16:26

georgwiese force-pushed the ec-add branch from fc52613 to 2dbee80 Compare February 7, 2024 17:26

georgwiese force-pushed the arith-hints branch from b9826bd to d6564fe Compare February 7, 2024 17:28

georgwiese force-pushed the ec-add branch from 2dbee80 to f2a2a03 Compare February 7, 2024 21:27

georgwiese force-pushed the arith-hints branch from d6564fe to d38f3d4 Compare February 7, 2024 21:29

georgwiese force-pushed the ec-add branch from f2a2a03 to 40fe394 Compare February 8, 2024 10:42

georgwiese force-pushed the arith-hints branch from d38f3d4 to d712628 Compare February 8, 2024 11:04

Base automatically changed from ec-add to main February 8, 2024 12:56

georgwiese force-pushed the arith-hints branch from d712628 to bf44677 Compare February 14, 2024 11:44

georgwiese mentioned this pull request Feb 14, 2024

Improve error message in std::math::ff:inverse #1056

Merged

georgwiese force-pushed the arith-hints branch 2 times, most recently from 0e9df15 to e9d7805 Compare February 14, 2024 15:51

georgwiese commented Feb 14, 2024

View reviewed changes

std/arith.asm Outdated Show resolved Hide resolved

georgwiese commented Feb 14, 2024

View reviewed changes

std/arith.asm Outdated Show resolved Hide resolved

georgwiese force-pushed the arith-hints branch from 4b4ebc3 to 79dc4f3 Compare February 14, 2024 16:17

georgwiese commented Feb 14, 2024

View reviewed changes

georgwiese changed the title ~~[WIP] Hints for arithmetic machine~~ Hints for arithmetic machine Feb 14, 2024

georgwiese commented Feb 14, 2024

View reviewed changes

georgwiese mentioned this pull request Feb 14, 2024

Secp256k1 stuff #993

Closed

chriseth reviewed Feb 15, 2024

View reviewed changes

georgwiese force-pushed the arith-hints branch from 9059347 to 5d0826f Compare February 19, 2024 11:30

georgwiese force-pushed the arith-hints branch from 5d0826f to 0798895 Compare March 13, 2024 13:59

chriseth reviewed Mar 13, 2024

View reviewed changes

std/arith.asm Outdated Show resolved Hide resolved

chriseth reviewed Mar 13, 2024

View reviewed changes

std/arith.asm Outdated Show resolved Hide resolved

chriseth reviewed Mar 13, 2024

View reviewed changes

georgwiese force-pushed the arith-hints branch from 8128106 to c543f16 Compare March 14, 2024 14:54

georgwiese commented Mar 14, 2024

View reviewed changes

georgwiese marked this pull request as ready for review March 14, 2024 15:08

chriseth reviewed Mar 15, 2024

View reviewed changes

chriseth approved these changes Mar 18, 2024

View reviewed changes

Hints for arithmetic machine

f87a760

georgwiese force-pushed the arith-hints branch from 3d7c17d to f87a760 Compare March 18, 2024 10:58

georgwiese enabled auto-merge March 18, 2024 11:00

georgwiese added this pull request to the merge queue Mar 18, 2024

Merged via the queue into main with commit d08fa24 Mar 18, 2024
5 checks passed

georgwiese deleted the arith-hints branch March 18, 2024 11:24


		let limbs_to_int: expr[] -> int = \|limbs\| array::sum(array::map_enumerated(limbs, \|i, limb\| int(eval(limb)) << (i * 16)));

		let x1_int: -> int = \|\| limbs_to_int(x1);

	// Compute quotients for the various equation.
	// Compute quotients for the various equations.

	let s_for_eq1 = \|x1, y1, x2, y2\| div(sub(y2, y1), sub(x2, x1));
	let s_for_eq1 = \|\| div(sub(y2_int(), y1_int()), sub(x2_int(), x1_int()));


		let eq1 = (\|\| \|nr\| product(sf, x2f)(nr) - product(sf, x1f)(nr) - y2f(nr) + y1f(nr) + product_with_p(q0f)(nr))();
		let eq1: int -> expr = \|nr\| product(sf, x2f)(nr) - product(sf, x1f)(nr) - y2f(nr) + y1f(nr) + product_with_p(q0f)(nr);

Hints for arithmetic machine #1005

Hints for arithmetic machine #1005

Conversation

georgwiese commented Feb 1, 2024 • edited Loading

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

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

Choose a reason for hiding this comment

Choose a reason for hiding this comment

georgwiese commented Feb 1, 2024 •

edited

Loading