From 9ea67369cedfb6dce19e71418480b97eeefcde7c Mon Sep 17 00:00:00 2001 From: Georg Wiese Date: Tue, 30 Jan 2024 16:23:01 +0100 Subject: [PATCH] Arithmetic machine: Add equation selectors --- std/arith.asm | 70 ++++++++++++++++++++++++++++++------ test_data/std/arith_test.asm | 30 ++++++++++------ 2 files changed, 79 insertions(+), 21 deletions(-) diff --git a/std/arith.asm b/std/arith.asm index 8104f68b0..4fc80e147 100644 --- a/std/arith.asm +++ b/std/arith.asm @@ -1,17 +1,34 @@ use std::array; use std::utils::unchanged_until; +use std::utils::force_bool; use std::utils::sum; // Arithmetic machine, ported mainly from Polygon: https://github.com/0xPolygonHermez/zkevm-proverjs/blob/main/pil/arith.pil // Currently only supports "Equation 0", i.e., 256-Bit addition and multiplication. machine Arith(CLK32_31, operation_id){ - operation eq0<0> x1_0, x1_1, x1_2, x1_3, x1_4, x1_5, x1_6, x1_7, y1_0, y1_1, y1_2, y1_3, y1_4, y1_5, y1_6, y1_7, x2_0, x2_1, x2_2, x2_3, x2_4, x2_5, x2_6, x2_7 -> y2_0, y2_1, y2_2, y2_3, y2_4, y2_5, y2_6, y2_7, y3_0, y3_1, y3_2, y3_3, y3_4, y3_5, y3_6, y3_7; + + // The operation ID will be bit-decomosed to yield selEq[], controlling which equations are activated. col witness operation_id; + // Computes x1 * y1 + x2, where all inputs / outputs are 256-bit words (represented as 32-Bit limbs in little-endian order). + // More precisely, affine_256(x1, y1, x2) = (y2, y3), where x1 * y1 + x2 = 2**256 * y2 + y3 + // Operation ID is 1 = 0b0001, i.e., we activate equation 0. + operation affine_256<1> x1_0, x1_1, x1_2, x1_3, x1_4, x1_5, x1_6, x1_7, y1_0, y1_1, y1_2, y1_3, y1_4, y1_5, y1_6, y1_7, x2_0, x2_1, x2_2, x2_3, x2_4, x2_5, x2_6, x2_7 -> y2_0, y2_1, y2_2, y2_3, y2_4, y2_5, y2_6, y2_7, y3_0, y3_1, y3_2, y3_3, y3_4, y3_5, y3_6, y3_7; + + // Performs elliptic curve addition of points (x1, y2) and (x2, y2). + // Operation ID is 10 = 0b1010, i.e., we activate equations 1, 3, and 4. + // TODO: Implement these equations + operation ec_add<10> x1_0, x1_1, x1_2, x1_3, x1_4, x1_5, x1_6, x1_7, y1_0, y1_1, y1_2, y1_3, y1_4, y1_5, y1_6, y1_7, x2_0, x2_1, x2_2, x2_3, x2_4, x2_5, x2_6, x2_7, y2_0, y2_1, y2_2, y2_3, y2_4, y2_5, y2_6, y2_7 -> x3_0, x3_1, x3_2, x3_3, x3_4, x3_5, x3_6, x3_7, y3_0, y3_1, y3_2, y3_3, y3_4, y3_5, y3_6, y3_7; + + // Performs elliptic curve doubling of point (x1, y2). + // Operation ID is 12 = 0b1100, i.e., we activate equations 2, 3, and 4. + // TODO: Implement these equations + operation ec_double<12> x1_0, x1_1, x1_2, x1_3, x1_4, x1_5, x1_6, x1_7, y1_0, y1_1, y1_2, y1_3, y1_4, y1_5, y1_6, y1_7 -> x3_0, x3_1, x3_2, x3_3, x3_4, x3_5, x3_6, x3_7, y3_0, y3_1, y3_2, y3_3, y3_4, y3_5, y3_6, y3_7; + let BYTE = |i| i & 0xff; let BYTE2 = |i| i & 0xffff; - pol commit x1[16], y1[16], x2[16], y2[16], y3[16]; + pol commit x1[16], y1[16], x2[16], y2[16], x3[16], y3[16]; // Intermediate polynomials, 32-Bit each pol x1_0 = x1[1] * 2**16 + x1[0]; @@ -50,6 +67,15 @@ machine Arith(CLK32_31, operation_id){ pol y2_6 = y2[13] * 2**16 + y2[12]; pol y2_7 = y2[15] * 2**16 + y2[14]; + pol x3_0 = x3[1] * 2**16 + x3[0]; + pol x3_1 = x3[3] * 2**16 + x3[2]; + pol x3_2 = x3[5] * 2**16 + x3[4]; + pol x3_3 = x3[7] * 2**16 + x3[6]; + pol x3_4 = x3[9] * 2**16 + x3[8]; + pol x3_5 = x3[11] * 2**16 + x3[10]; + pol x3_6 = x3[13] * 2**16 + x3[12]; + pol x3_7 = x3[15] * 2**16 + x3[14]; + pol y3_0 = y3[1] * 2**16 + y3[0]; pol y3_1 = y3[3] * 2**16 + y3[2]; pol y3_2 = y3[5] * 2**16 + y3[4]; @@ -112,6 +138,7 @@ machine Arith(CLK32_31, operation_id){ array::map(y1, |e| unchanged_until(e, CLK32[31])); array::map(x2, |e| unchanged_until(e, CLK32[31])); array::map(y2, |e| unchanged_until(e, CLK32[31])); + array::map(x3, |e| unchanged_until(e, CLK32[31])); array::map(y3, |e| unchanged_until(e, CLK32[31])); /**** @@ -121,8 +148,8 @@ machine Arith(CLK32_31, operation_id){ *****/ sum(16, |i| x1[i] * CLK32[i]) + sum(16, |i| y1[i] * CLK32[16 + i]) in BYTE2; - sum(16, |i| x2[i] * CLK32[i]) in BYTE2; - sum(16, |i| y3[i] * CLK32[i]) + sum(16, |i| y2[i] * CLK32[16 + i]) in BYTE2; + sum(16, |i| x2[i] * CLK32[i]) + sum(16, |i| y2[i] * CLK32[16 + i]) in BYTE2; + sum(16, |i| x3[i] * CLK32[i]) + sum(16, |i| y3[i] * CLK32[16 + i]) in BYTE2; /******* @@ -156,18 +183,39 @@ machine Arith(CLK32_31, operation_id){ + x2f(nr) - shift_right(y2f, 16)(nr) - y3f(nr); + + // Binary selectors for the equations that are activated. Determined from the operation ID via bit-decomposition. + // Note that there are only 4 selectors because equation 4 is activated iff. equation 3 is activated, so we can + // re-use the same selector. + pol commit selEq[4]; + // Note that this is not necessary, because the operation ID is already constant within the block + // array::map(selEq, |e| unchanged_until(e, CLK32[31])); + array::map(selEq, |c| force_bool(c)); + sum(4, |i| 2 ** i * selEq[i]) = operation_id; // Note that Polygon uses a single 22-Bit column. However, this approach allows for a lower degree (2**16) // while still preventing overflows: The 32-bit carry gets added to 32 16-Bit values, which can't overflow // the Goldilocks field. - pol witness carry_low, carry_high; - { carry_high } in { BYTE2 }; - { carry_low } in { BYTE2 }; + pol witness carry_low[3], carry_high[3]; + { carry_low[0] } in { BYTE2 }; + { carry_low[1] } in { BYTE2 }; + { carry_low[2] } in { BYTE2 }; + { carry_high[0] } in { BYTE2 }; + { carry_high[1] } in { BYTE2 }; + { carry_high[2] } in { BYTE2 }; - pol carry = carry_high * 2**16 + carry_low; + // Carries can be any integer in the range [-2**31, 2**31 - 1) + pol carry0 = carry_high[0] * 2**16 + carry_low[0] - 2 ** 31; + pol carry1 = carry_high[1] * 2**16 + carry_low[1] - 2 ** 31; + pol carry2 = carry_high[2] * 2**16 + carry_low[2] - 2 ** 31; + let carry = [carry0, carry1, carry2]; - carry * CLK32[0] = 0; + array::map(carry, |c| c * CLK32[0] == 0); - let eq0_sum = sum(32, |i| eq0(i) * CLK32[i]); - carry + eq0_sum = carry' * 2**16; + // TODO: Somehow witgen fails if a carry is unconstrained + selEq[0] * carry[1] = 0; + selEq[0] * carry[2] = 0; + + col eq0_sum = sum(32, |i| eq0(i) * CLK32[i]); + selEq[0] * (eq0_sum + carry[0]) = selEq[0] * carry[0]' * 2**16; } \ No newline at end of file diff --git a/test_data/std/arith_test.asm b/test_data/std/arith_test.asm index 24737d6b5..ab9aff8b0 100644 --- a/test_data/std/arith_test.asm +++ b/test_data/std/arith_test.asm @@ -44,6 +44,14 @@ machine Main{ reg E5[<=]; reg E6[<=]; reg E7[<=]; + reg F0[<=]; + reg F1[<=]; + reg F2[<=]; + reg F3[<=]; + reg F4[<=]; + reg F5[<=]; + reg F6[<=]; + reg F7[<=]; reg t_0_0; reg t_0_1; @@ -64,7 +72,9 @@ machine Main{ Arith arith; - instr eq0 A0, A1, A2, A3, A4, A5, A6, A7, B0, B1, B2, B3, B4, B5, B6, B7, C0, C1, C2, C3, C4, C5, C6, C7 -> D0, D1, D2, D3, D4, D5, D6, D7, E0, E1, E2, E3, E4, E5, E6, E7 = arith.eq0; + instr affine_256 A0, A1, A2, A3, A4, A5, A6, A7, B0, B1, B2, B3, B4, B5, B6, B7, C0, C1, C2, C3, C4, C5, C6, C7 -> D0, D1, D2, D3, D4, D5, D6, D7, E0, E1, E2, E3, E4, E5, E6, E7 = arith.affine_256; + instr ec_add A0, A1, A2, A3, A4, A5, A6, A7, B0, B1, B2, B3, B4, B5, B6, B7, C0, C1, C2, C3, C4, C5, C6, C7, D0, D1, D2, D3, D4, D5, D6, D7 -> E0, E1, E2, E3, E4, E5, E6, E7, F0, F1, F2, F3, F4, F5, F6, F7 = arith.ec_add; + instr ec_double A0, A1, A2, A3, A4, A5, A6, A7, B0, B1, B2, B3, B4, B5, B6, B7 -> E0, E1, E2, E3, E4, E5, E6, E7, F0, F1, F2, F3, F4, F5, F6, F7 = arith.ec_double; instr assert_eq A0, A1, A2, A3, A4, A5, A6, A7, B0, B1, B2, B3, B4, B5, B6, B7 { A0 = B0, @@ -85,7 +95,7 @@ machine Main{ // == 0x91a2b3c579be024740da740e6f8091a38e38e38f258bf259be024691fdb97530da740da60b60b60907f6e5d369d0369ca8641fda1907f6e33333333 // == 0x00000000_091a2b3c_579be024_740da740_e6f8091a_38e38e38_f258bf25_9be02469 * 2**256 + 0x1fdb9753_0da740da_60b60b60_907f6e5d_369d0369_ca8641fd_a1907f6e_33333333 - 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 <== eq0( + 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 <== affine_256( 0x77777777, 0x66666666, 0x55555555, 0x44444444, 0x33333333, 0x22222222, 0x11111111, 0x00000000, 0xffffffff, 0xeeeeeeee, 0xdddddddd, 0xcccccccc, 0xbbbbbbbb, 0xaaaaaaaa, 0x99999999, 0x88888888, 0xaaaaaaaa, 0xbbbbbbbb, 0xbbbbbbbb, 0xaaaaaaaa, 0xaaaaaaaa, 0xbbbbbbbb, 0xbbbbbbbb, 0xaaaaaaaa); @@ -96,7 +106,7 @@ machine Main{ // Test vectors from: https://github.com/0xPolygonHermez/zkevm-proverjs/blob/main/test/sm/sm_arith.js // 2 * 3 + 5 = 11 - 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 <== eq0( + 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 <== affine_256( 2, 0, 0, 0, 0, 0, 0, 0, 3, 0, 0, 0, 0, 0, 0, 0, 5, 0, 0, 0, 0, 0, 0, 0); @@ -104,7 +114,7 @@ machine Main{ 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, 11, 0, 0, 0, 0, 0, 0, 0; // 256 * 256 + 1 = 65537 - 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 <== eq0( + 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 <== affine_256( 256, 0, 0, 0, 0, 0, 0, 0, 256, 0, 0, 0, 0, 0, 0, 0, 1, 0, 0, 0, 0, 0, 0, 0); @@ -112,7 +122,7 @@ machine Main{ 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, 65537, 0, 0, 0, 0, 0, 0, 0; // 3000 * 2000 + 5000 = 6005000 - 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 <== eq0( + 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 <== affine_256( 3000, 0, 0, 0, 0, 0, 0, 0, 2000, 0, 0, 0, 0, 0, 0, 0, 5000, 0, 0, 0, 0, 0, 0, 0); @@ -120,7 +130,7 @@ machine Main{ 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, 6005000, 0, 0, 0, 0, 0, 0, 0; // 3000000 * 2000000 + 5000000 = 6000005000000 - 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 <== eq0( + 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 <== affine_256( 3000000, 0, 0, 0, 0, 0, 0, 0, 2000000, 0, 0, 0, 0, 0, 0, 0, 5000000, 0, 0, 0, 0, 0, 0, 0); @@ -128,7 +138,7 @@ machine Main{ 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, 0xfc2aab40, 0x574, 0, 0, 0, 0, 0, 0; // 3000 * 0 + 5000 = 5000 - 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 <== eq0( + 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 <== affine_256( 3000, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 5000, 0, 0, 0, 0, 0, 0, 0); @@ -136,7 +146,7 @@ machine Main{ 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, 5000, 0, 0, 0, 0, 0, 0, 0; // 2**255 * 2 + 0 = 2 ** 256 - 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 <== eq0( + 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 <== affine_256( 0, 0, 0, 0, 0, 0, 0, 0x80000000, 2, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0, 0); @@ -145,7 +155,7 @@ machine Main{ // (2**256 - 1) * (2**256 - 1) + (2**256 - 1) = 2 ** 256 * 115792089237316195423570985008687907853269984665640564039457584007913129639935 // = 2 ** 256 * 0xffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff - 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 <== eq0( + 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 <== affine_256( 0xffffffff, 0xffffffff, 0xffffffff, 0xffffffff, 0xffffffff, 0xffffffff, 0xffffffff, 0xffffffff, 0xffffffff, 0xffffffff, 0xffffffff, 0xffffffff, 0xffffffff, 0xffffffff, 0xffffffff, 0xffffffff, 0xffffffff, 0xffffffff, 0xffffffff, 0xffffffff, 0xffffffff, 0xffffffff, 0xffffffff, 0xffffffff); @@ -154,7 +164,7 @@ machine Main{ // (2**256 - 1) * 1 + (2**256 - 1) = 2 ** 256 + 115792089237316195423570985008687907853269984665640564039457584007913129639934 // = 2 ** 256 + 0xfffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffe - 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 <== eq0( + 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 <== affine_256( 0xffffffff, 0xffffffff, 0xffffffff, 0xffffffff, 0xffffffff, 0xffffffff, 0xffffffff, 0xffffffff, 1, 0, 0, 0, 0, 0, 0, 0, 0xffffffff, 0xffffffff, 0xffffffff, 0xffffffff, 0xffffffff, 0xffffffff, 0xffffffff, 0xffffffff);