From 266df0e4912fcb26240690cc658bac226bb5371c Mon Sep 17 00:00:00 2001 From: jeanmon Date: Thu, 11 Apr 2024 12:44:51 +0000 Subject: [PATCH] 5641: Enable range check on the ALU registers --- barretenberg/cpp/pil/avm/avm_alu.pil | 45 +-- barretenberg/cpp/pil/avm/avm_main.pil | 2 + .../relations/generated/avm/avm_alu.hpp | 343 ++++++++++-------- .../relations/generated/avm/declare_views.hpp | 10 +- .../vm/avm_trace/avm_alu_trace.cpp | 120 +++--- .../vm/avm_trace/avm_alu_trace.hpp | 9 +- .../barretenberg/vm/avm_trace/avm_trace.cpp | 16 +- .../barretenberg/vm/avm_trace/avm_trace.hpp | 2 - .../vm/generated/avm_circuit_builder.hpp | 22 +- .../barretenberg/vm/generated/avm_flavor.hpp | 92 +++-- .../barretenberg/vm/generated/avm_prover.cpp | 2 - .../vm/generated/avm_verifier.cpp | 1 - .../vm/tests/avm_arithmetic.test.cpp | 40 +- .../vm/tests/avm_comparison.test.cpp | 1 + .../vm/tests/avm_inter_table.test.cpp | 1 + 15 files changed, 391 insertions(+), 315 deletions(-) diff --git a/barretenberg/cpp/pil/avm/avm_alu.pil b/barretenberg/cpp/pil/avm/avm_alu.pil index 224c8f3d6f36..8e2a578c5df3 100644 --- a/barretenberg/cpp/pil/avm/avm_alu.pil +++ b/barretenberg/cpp/pil/avm/avm_alu.pil @@ -55,9 +55,6 @@ namespace avm_alu(256); pol commit u16_r13; pol commit u16_r14; - // 64-bit slice register - pol commit u64_r0; - // Carry flag pol commit cf; @@ -67,13 +64,13 @@ namespace avm_alu(256); // ========= Type Constraints ============================================= // TODO: Range constraints - // - for slice registers // - intermediate registers ia and ib (inputs) depending on flag (or inherited from previous ops?) // - intermediate register ic (in some operations it might be inherited based on ia and ib ranges. To be checked.) - // Carry flag: We will have to constraint to ensure that the - // arithmetic expressions are not overflowing finite field size // Remark: Operation selectors are constrained in the main trace. + // cf is boolean + cf * (1 - cf) = 0; + // Boolean flattened instructions tags ff_tag * (1 - ff_tag) = 0; u8_tag * (1 - u8_tag) = 0; @@ -89,8 +86,8 @@ namespace avm_alu(256); in_tag = u8_tag + 2 * u16_tag + 3 * u32_tag + 4 * u64_tag + 5 * u128_tag + 6 * ff_tag; // Operation selectors are copied from main table and do not need to be constrained here. - // TODO: Ensure mutual exclusion of op_add and op_sub as some relations below - // requires it. + // Mutual exclusion of op_add and op_sub are derived from their mutual exclusion in the + // main trace which is ensured by the operation decomposition. // ========= ARITHMETIC OPERATION - EXPLANATIONS ================================================= // Main trick for arithmetic operations modulo 2^k is to perform the operation @@ -134,8 +131,6 @@ namespace avm_alu(256); pol SUM_96 = SUM_64 + u16_r3 * 2**64 + u16_r4 * 2**80; pol SUM_128 = SUM_96 + u16_r5 * 2**96 + u16_r6 * 2**112; - - // ========= ADDITION/SUBTRACTION Operation Constraints =============================== // // Addition and subtraction relations are very similar and will be consolidated. @@ -170,7 +165,6 @@ namespace avm_alu(256); #[ALU_MULTIPLICATION_FF] ff_tag * op_mul * (ia * ib - ic) = 0; - // We need 2k bits to express the product (a*b) over the integer, i.e., for type uk // we express the product as sum_k (u8 is an exception as we need 8-bit registers) @@ -191,34 +185,34 @@ namespace avm_alu(256); // b = b_l + b_h * 2^64 // We show that c satisfies: a_l * b_l + (a_h * b_l + a_l * b_h) * 2^64 = R * 2^128 + c // for a R < 2^65. Equivalently: - // a * b_l + a_l * b_h * 2^64 = (CF * 2^64 + R') * 2^128 + c - // for a bit carry flag CF and R' range constrained to 64 bits. + // a * b_l + a_l * b_h * 2^64 = (CF * 2^64 + R_64) * 2^128 + c + // for a bit carry flag CF and R_64 range constrained to 64 bits. // We use two lines in the execution trace. First line represents a // as decomposed over 16-bit registers. Second line represents b. // Selector flag is only toggled in the first line and we access b through // shifted polynomials. - // R' is stored in u64_r0 - - // 64-bit lower limb - pol SUM_LOW_64 = u16_r0 + u16_r1 * 2**16 + u16_r2 * 2**32 + u16_r3 * 2**48; + // R_64 is stored in u16_r7, u16_r8, u16_r9, u_16_r10 // 64-bit higher limb - pol SUM_HIGH_64 = u16_r4 + u16_r5 * 2**16 + u16_r6 * 2**32 + u16_r7 * 2**48; + pol SUM_HIGH_64 = u16_r3 + u16_r4 * 2**16 + u16_r5 * 2**32 + u16_r6 * 2**48; // 64-bit lower limb for next row - pol SUM_LOW_SHIFTED_64 = u16_r0' + u16_r1' * 2**16 + u16_r2' * 2**32 + u16_r3' * 2**48; + pol SUM_LOW_SHIFTED_64 = u8_r0' + u8_r1' * 2**8 + u16_r0' * 2**16 + u16_r1' * 2**32 + u16_r2' * 2**48; // 64-bit higher limb for next row - pol SUM_HIGH_SHIFTED_64 = u16_r4' + u16_r5' * 2**16 + u16_r6' * 2**32 + u16_r7' * 2**48; + pol SUM_HIGH_SHIFTED_64 = u16_r3' + u16_r4' * 2**16 + u16_r5' * 2**32 + u16_r6' * 2**48; + + // R_64 decomposition + pol R_64 = u16_r7 + u16_r8 * 2**16 + u16_r9 * 2**32 + u16_r10 * 2**48; // Arithmetic relations - u128_tag * op_mul * (SUM_LOW_64 + SUM_HIGH_64 * 2**64 - ia) = 0; + u128_tag * op_mul * (SUM_64 + SUM_HIGH_64 * 2**64 - ia) = 0; u128_tag * op_mul * (SUM_LOW_SHIFTED_64 + SUM_HIGH_SHIFTED_64 * 2**64 - ib) = 0; #[ALU_MULTIPLICATION_OUT_U128] u128_tag * op_mul * ( ia * SUM_LOW_SHIFTED_64 - + SUM_LOW_64 * SUM_HIGH_SHIFTED_64 * 2**64 - - (cf * 2**64 + u64_r0) * 2**128 + + SUM_64 * SUM_HIGH_SHIFTED_64 * 2**64 + - (cf * 2**64 + R_64) * 2**128 - ic ) = 0; @@ -431,7 +425,7 @@ namespace avm_alu(256); rng_chk_sel * (1 - rng_chk_sel) = 0; // If we have remaining range checks, we cannot have cmp_sel set. This prevents malicious truncating of the range // checks by adding a new LT/LTE operation before all the range checks from the previous computation are complete. - rng_chk_sel * cmp_sel = 0; + rng_chk_sel * cmp_sel = 0; // rng_chk_sel = 1 when cmp_rng_ctr != 0 and rng_chk_sel = 0 when cmp_rng_ctr = 0; #[CTR_NON_ZERO_REL] @@ -442,13 +436,12 @@ namespace avm_alu(256); pol commit rng_chk_lookup_selector; #[RNG_CHK_LOOKUP_SELECTOR] - rng_chk_lookup_selector = cmp_sel + rng_chk_sel; + rng_chk_lookup_selector' = cmp_sel' + rng_chk_sel' + op_add' + op_sub' + op_mul' + op_mul * u128_tag; // Perform 128-bit range check on lo part #[LOWER_CMP_RNG_CHK] a_lo = SUM_128 * RNG_CHK_OP; - // Perform 128-bit range check on hi part #[UPPER_CMP_RNG_CHK] a_hi = (u16_r7 + u16_r8 * 2**16 + diff --git a/barretenberg/cpp/pil/avm/avm_main.pil b/barretenberg/cpp/pil/avm/avm_main.pil index d491662c0fb2..ecc18fe6d83d 100644 --- a/barretenberg/cpp/pil/avm/avm_main.pil +++ b/barretenberg/cpp/pil/avm/avm_main.pil @@ -364,6 +364,8 @@ namespace avm_main(256); //====== Inter-table Constraints (Range Checks) ============================================ // TODO: Investigate optimising these range checks. Handling non-FF elements should require less range checks. + // One can increase the granularity based on the operation and tag. In the most extreme case, + // a specific selector per register might be introduced. #[LOOKUP_U8_0] avm_alu.rng_chk_lookup_selector { avm_alu.u8_r0 } in sel_rng_8 { clk }; diff --git a/barretenberg/cpp/src/barretenberg/relations/generated/avm/avm_alu.hpp b/barretenberg/cpp/src/barretenberg/relations/generated/avm/avm_alu.hpp index fc4fcff7998e..8682c27d4cfc 100644 --- a/barretenberg/cpp/src/barretenberg/relations/generated/avm/avm_alu.hpp +++ b/barretenberg/cpp/src/barretenberg/relations/generated/avm/avm_alu.hpp @@ -21,19 +21,23 @@ template struct Avm_aluRow { FF avm_alu_cmp_rng_ctr{}; FF avm_alu_cmp_rng_ctr_shift{}; FF avm_alu_cmp_sel{}; + FF avm_alu_cmp_sel_shift{}; FF avm_alu_ff_tag{}; FF avm_alu_ia{}; FF avm_alu_ib{}; FF avm_alu_ic{}; FF avm_alu_in_tag{}; FF avm_alu_op_add{}; + FF avm_alu_op_add_shift{}; FF avm_alu_op_eq{}; FF avm_alu_op_eq_diff_inv{}; FF avm_alu_op_lt{}; FF avm_alu_op_lte{}; FF avm_alu_op_mul{}; + FF avm_alu_op_mul_shift{}; FF avm_alu_op_not{}; FF avm_alu_op_sub{}; + FF avm_alu_op_sub_shift{}; FF avm_alu_p_a_borrow{}; FF avm_alu_p_b_borrow{}; FF avm_alu_p_sub_a_hi{}; @@ -46,7 +50,7 @@ template struct Avm_aluRow { FF avm_alu_p_sub_b_lo_shift{}; FF avm_alu_res_hi{}; FF avm_alu_res_lo{}; - FF avm_alu_rng_chk_lookup_selector{}; + FF avm_alu_rng_chk_lookup_selector_shift{}; FF avm_alu_rng_chk_sel{}; FF avm_alu_rng_chk_sel_shift{}; FF avm_alu_u128_tag{}; @@ -70,103 +74,103 @@ template struct Avm_aluRow { FF avm_alu_u16_r6{}; FF avm_alu_u16_r6_shift{}; FF avm_alu_u16_r7{}; - FF avm_alu_u16_r7_shift{}; FF avm_alu_u16_r8{}; FF avm_alu_u16_r9{}; FF avm_alu_u16_tag{}; FF avm_alu_u32_tag{}; - FF avm_alu_u64_r0{}; FF avm_alu_u64_tag{}; FF avm_alu_u8_r0{}; + FF avm_alu_u8_r0_shift{}; FF avm_alu_u8_r1{}; + FF avm_alu_u8_r1_shift{}; FF avm_alu_u8_tag{}; }; inline std::string get_relation_label_avm_alu(int index) { switch (index) { - case 10: + case 11: return "ALU_ADD_SUB_1"; - case 11: + case 12: return "ALU_ADD_SUB_2"; - case 12: + case 13: return "ALU_MULTIPLICATION_FF"; - case 13: + case 14: return "ALU_MUL_COMMON_1"; - case 14: + case 15: return "ALU_MUL_COMMON_2"; - case 17: + case 18: return "ALU_MULTIPLICATION_OUT_U128"; - case 18: + case 19: return "ALU_FF_NOT_XOR"; - case 19: + case 20: return "ALU_OP_NOT"; - case 20: + case 21: return "ALU_RES_IS_BOOL"; - case 21: + case 22: return "ALU_OP_EQ"; - case 22: + case 23: return "INPUT_DECOMP_1"; - case 23: + case 24: return "INPUT_DECOMP_2"; - case 25: + case 26: return "SUB_LO_1"; - case 26: + case 27: return "SUB_HI_1"; - case 28: + case 29: return "SUB_LO_2"; - case 29: + case 30: return "SUB_HI_2"; - case 30: + case 31: return "RES_LO"; - case 31: + case 32: return "RES_HI"; - case 32: + case 33: return "CMP_CTR_REL_1"; - case 33: + case 34: return "CMP_CTR_REL_2"; - case 36: + case 37: return "CTR_NON_ZERO_REL"; - case 37: + case 38: return "RNG_CHK_LOOKUP_SELECTOR"; - case 38: + case 39: return "LOWER_CMP_RNG_CHK"; - case 39: + case 40: return "UPPER_CMP_RNG_CHK"; - case 40: + case 41: return "SHIFT_RELS_0"; - case 42: + case 43: return "SHIFT_RELS_1"; - case 44: + case 45: return "SHIFT_RELS_2"; - case 46: + case 47: return "SHIFT_RELS_3"; } return std::to_string(index); @@ -176,9 +180,9 @@ template class avm_aluImpl { public: using FF = FF_; - static constexpr std::array SUBRELATION_PARTIAL_LENGTHS{ - 2, 2, 3, 3, 3, 3, 3, 3, 3, 3, 4, 5, 5, 5, 5, 6, 6, 8, 3, 4, 4, 5, 4, 4, - 3, 4, 3, 3, 4, 3, 6, 5, 3, 3, 3, 3, 4, 2, 4, 4, 3, 3, 3, 3, 3, 3, 3, 3, + static constexpr std::array SUBRELATION_PARTIAL_LENGTHS{ + 2, 2, 3, 3, 3, 3, 3, 3, 3, 3, 3, 4, 5, 5, 5, 5, 6, 6, 8, 3, 4, 4, 5, 4, 4, + 3, 4, 3, 3, 4, 3, 6, 5, 3, 3, 3, 3, 4, 3, 4, 4, 3, 3, 3, 3, 3, 3, 3, 3, }; template @@ -211,7 +215,7 @@ template class avm_aluImpl { { Avm_DECLARE_VIEWS(2); - auto tmp = (avm_alu_ff_tag * (-avm_alu_ff_tag + FF(1))); + auto tmp = (avm_alu_cf * (-avm_alu_cf + FF(1))); tmp *= scaling_factor; std::get<2>(evals) += tmp; } @@ -219,7 +223,7 @@ template class avm_aluImpl { { Avm_DECLARE_VIEWS(3); - auto tmp = (avm_alu_u8_tag * (-avm_alu_u8_tag + FF(1))); + auto tmp = (avm_alu_ff_tag * (-avm_alu_ff_tag + FF(1))); tmp *= scaling_factor; std::get<3>(evals) += tmp; } @@ -227,7 +231,7 @@ template class avm_aluImpl { { Avm_DECLARE_VIEWS(4); - auto tmp = (avm_alu_u16_tag * (-avm_alu_u16_tag + FF(1))); + auto tmp = (avm_alu_u8_tag * (-avm_alu_u8_tag + FF(1))); tmp *= scaling_factor; std::get<4>(evals) += tmp; } @@ -235,7 +239,7 @@ template class avm_aluImpl { { Avm_DECLARE_VIEWS(5); - auto tmp = (avm_alu_u32_tag * (-avm_alu_u32_tag + FF(1))); + auto tmp = (avm_alu_u16_tag * (-avm_alu_u16_tag + FF(1))); tmp *= scaling_factor; std::get<5>(evals) += tmp; } @@ -243,7 +247,7 @@ template class avm_aluImpl { { Avm_DECLARE_VIEWS(6); - auto tmp = (avm_alu_u64_tag * (-avm_alu_u64_tag + FF(1))); + auto tmp = (avm_alu_u32_tag * (-avm_alu_u32_tag + FF(1))); tmp *= scaling_factor; std::get<6>(evals) += tmp; } @@ -251,7 +255,7 @@ template class avm_aluImpl { { Avm_DECLARE_VIEWS(7); - auto tmp = (avm_alu_u128_tag * (-avm_alu_u128_tag + FF(1))); + auto tmp = (avm_alu_u64_tag * (-avm_alu_u64_tag + FF(1))); tmp *= scaling_factor; std::get<7>(evals) += tmp; } @@ -259,28 +263,36 @@ template class avm_aluImpl { { Avm_DECLARE_VIEWS(8); + auto tmp = (avm_alu_u128_tag * (-avm_alu_u128_tag + FF(1))); + tmp *= scaling_factor; + std::get<8>(evals) += tmp; + } + // Contribution 9 + { + Avm_DECLARE_VIEWS(9); + auto tmp = (avm_alu_alu_sel * ((((((avm_alu_ff_tag + avm_alu_u8_tag) + avm_alu_u16_tag) + avm_alu_u32_tag) + avm_alu_u64_tag) + avm_alu_u128_tag) - FF(1))); tmp *= scaling_factor; - std::get<8>(evals) += tmp; + std::get<9>(evals) += tmp; } - // Contribution 9 + // Contribution 10 { - Avm_DECLARE_VIEWS(9); + Avm_DECLARE_VIEWS(10); auto tmp = (avm_alu_in_tag - (((((avm_alu_u8_tag + (avm_alu_u16_tag * FF(2))) + (avm_alu_u32_tag * FF(3))) + (avm_alu_u64_tag * FF(4))) + (avm_alu_u128_tag * FF(5))) + (avm_alu_ff_tag * FF(6)))); tmp *= scaling_factor; - std::get<9>(evals) += tmp; + std::get<10>(evals) += tmp; } - // Contribution 10 + // Contribution 11 { - Avm_DECLARE_VIEWS(10); + Avm_DECLARE_VIEWS(11); auto tmp = (((avm_alu_op_add + avm_alu_op_sub) * ((((((((((avm_alu_u8_r0 + (avm_alu_u8_r1 * FF(256))) + (avm_alu_u16_r0 * FF(65536))) + @@ -295,11 +307,11 @@ template class avm_aluImpl { ((avm_alu_op_add - avm_alu_op_sub) * ((avm_alu_cf * FF(uint256_t{ 0UL, 0UL, 1UL, 0UL })) - avm_alu_ib))); tmp *= scaling_factor; - std::get<10>(evals) += tmp; + std::get<11>(evals) += tmp; } - // Contribution 11 + // Contribution 12 { - Avm_DECLARE_VIEWS(11); + Avm_DECLARE_VIEWS(12); auto tmp = (((avm_alu_op_add + avm_alu_op_sub) * (((((((avm_alu_u8_tag * avm_alu_u8_r0) + @@ -322,19 +334,19 @@ template class avm_aluImpl { avm_alu_ic)) + ((avm_alu_ff_tag * (avm_alu_op_add - avm_alu_op_sub)) * avm_alu_ib)); tmp *= scaling_factor; - std::get<11>(evals) += tmp; + std::get<12>(evals) += tmp; } - // Contribution 12 + // Contribution 13 { - Avm_DECLARE_VIEWS(12); + Avm_DECLARE_VIEWS(13); auto tmp = ((avm_alu_ff_tag * avm_alu_op_mul) * ((avm_alu_ia * avm_alu_ib) - avm_alu_ic)); tmp *= scaling_factor; - std::get<12>(evals) += tmp; + std::get<13>(evals) += tmp; } - // Contribution 13 + // Contribution 14 { - Avm_DECLARE_VIEWS(13); + Avm_DECLARE_VIEWS(14); auto tmp = ((((-avm_alu_ff_tag + FF(1)) - avm_alu_u128_tag) * avm_alu_op_mul) * (((((((((avm_alu_u8_r0 + (avm_alu_u8_r1 * FF(256))) + (avm_alu_u16_r0 * FF(65536))) + @@ -346,11 +358,11 @@ template class avm_aluImpl { (avm_alu_u16_r6 * FF(uint256_t{ 0UL, 281474976710656UL, 0UL, 0UL }))) - (avm_alu_ia * avm_alu_ib))); tmp *= scaling_factor; - std::get<13>(evals) += tmp; + std::get<14>(evals) += tmp; } - // Contribution 14 + // Contribution 15 { - Avm_DECLARE_VIEWS(14); + Avm_DECLARE_VIEWS(15); auto tmp = (avm_alu_op_mul * @@ -362,20 +374,6 @@ template class avm_aluImpl { (avm_alu_u16_r2 * FF(281474976710656UL))))) - (((-avm_alu_ff_tag + FF(1)) - avm_alu_u128_tag) * avm_alu_ic))); tmp *= scaling_factor; - std::get<14>(evals) += tmp; - } - // Contribution 15 - { - Avm_DECLARE_VIEWS(15); - - auto tmp = ((avm_alu_u128_tag * avm_alu_op_mul) * - (((((avm_alu_u16_r0 + (avm_alu_u16_r1 * FF(65536))) + (avm_alu_u16_r2 * FF(4294967296UL))) + - (avm_alu_u16_r3 * FF(281474976710656UL))) + - ((((avm_alu_u16_r4 + (avm_alu_u16_r5 * FF(65536))) + (avm_alu_u16_r6 * FF(4294967296UL))) + - (avm_alu_u16_r7 * FF(281474976710656UL))) * - FF(uint256_t{ 0UL, 1UL, 0UL, 0UL }))) - - avm_alu_ia)); - tmp *= scaling_factor; std::get<15>(evals) += tmp; } // Contribution 16 @@ -383,14 +381,13 @@ template class avm_aluImpl { Avm_DECLARE_VIEWS(16); auto tmp = ((avm_alu_u128_tag * avm_alu_op_mul) * - (((((avm_alu_u16_r0_shift + (avm_alu_u16_r1_shift * FF(65536))) + - (avm_alu_u16_r2_shift * FF(4294967296UL))) + - (avm_alu_u16_r3_shift * FF(281474976710656UL))) + - ((((avm_alu_u16_r4_shift + (avm_alu_u16_r5_shift * FF(65536))) + - (avm_alu_u16_r6_shift * FF(4294967296UL))) + - (avm_alu_u16_r7_shift * FF(281474976710656UL))) * + ((((((avm_alu_u8_r0 + (avm_alu_u8_r1 * FF(256))) + (avm_alu_u16_r0 * FF(65536))) + + (avm_alu_u16_r1 * FF(4294967296UL))) + + (avm_alu_u16_r2 * FF(281474976710656UL))) + + ((((avm_alu_u16_r3 + (avm_alu_u16_r4 * FF(65536))) + (avm_alu_u16_r5 * FF(4294967296UL))) + + (avm_alu_u16_r6 * FF(281474976710656UL))) * FF(uint256_t{ 0UL, 1UL, 0UL, 0UL }))) - - avm_alu_ib)); + avm_alu_ia)); tmp *= scaling_factor; std::get<16>(evals) += tmp; } @@ -398,19 +395,16 @@ template class avm_aluImpl { { Avm_DECLARE_VIEWS(17); - auto tmp = ((avm_alu_u128_tag * avm_alu_op_mul) * - ((((avm_alu_ia * (((avm_alu_u16_r0_shift + (avm_alu_u16_r1_shift * FF(65536))) + - (avm_alu_u16_r2_shift * FF(4294967296UL))) + - (avm_alu_u16_r3_shift * FF(281474976710656UL)))) + - (((((avm_alu_u16_r0 + (avm_alu_u16_r1 * FF(65536))) + (avm_alu_u16_r2 * FF(4294967296UL))) + - (avm_alu_u16_r3 * FF(281474976710656UL))) * - (((avm_alu_u16_r4_shift + (avm_alu_u16_r5_shift * FF(65536))) + - (avm_alu_u16_r6_shift * FF(4294967296UL))) + - (avm_alu_u16_r7_shift * FF(281474976710656UL)))) * - FF(uint256_t{ 0UL, 1UL, 0UL, 0UL }))) - - (((avm_alu_cf * FF(uint256_t{ 0UL, 1UL, 0UL, 0UL })) + avm_alu_u64_r0) * - FF(uint256_t{ 0UL, 0UL, 1UL, 0UL }))) - - avm_alu_ic)); + auto tmp = + ((avm_alu_u128_tag * avm_alu_op_mul) * + ((((((avm_alu_u8_r0_shift + (avm_alu_u8_r1_shift * FF(256))) + (avm_alu_u16_r0_shift * FF(65536))) + + (avm_alu_u16_r1_shift * FF(4294967296UL))) + + (avm_alu_u16_r2_shift * FF(281474976710656UL))) + + ((((avm_alu_u16_r3_shift + (avm_alu_u16_r4_shift * FF(65536))) + + (avm_alu_u16_r5_shift * FF(4294967296UL))) + + (avm_alu_u16_r6_shift * FF(281474976710656UL))) * + FF(uint256_t{ 0UL, 1UL, 0UL, 0UL }))) - + avm_alu_ib)); tmp *= scaling_factor; std::get<17>(evals) += tmp; } @@ -418,7 +412,24 @@ template class avm_aluImpl { { Avm_DECLARE_VIEWS(18); - auto tmp = (avm_alu_op_not * avm_alu_ff_tag); + auto tmp = + ((avm_alu_u128_tag * avm_alu_op_mul) * + ((((avm_alu_ia * + ((((avm_alu_u8_r0_shift + (avm_alu_u8_r1_shift * FF(256))) + (avm_alu_u16_r0_shift * FF(65536))) + + (avm_alu_u16_r1_shift * FF(4294967296UL))) + + (avm_alu_u16_r2_shift * FF(281474976710656UL)))) + + ((((((avm_alu_u8_r0 + (avm_alu_u8_r1 * FF(256))) + (avm_alu_u16_r0 * FF(65536))) + + (avm_alu_u16_r1 * FF(4294967296UL))) + + (avm_alu_u16_r2 * FF(281474976710656UL))) * + (((avm_alu_u16_r3_shift + (avm_alu_u16_r4_shift * FF(65536))) + + (avm_alu_u16_r5_shift * FF(4294967296UL))) + + (avm_alu_u16_r6_shift * FF(281474976710656UL)))) * + FF(uint256_t{ 0UL, 1UL, 0UL, 0UL }))) - + (((avm_alu_cf * FF(uint256_t{ 0UL, 1UL, 0UL, 0UL })) + + (((avm_alu_u16_r7 + (avm_alu_u16_r8 * FF(65536))) + (avm_alu_u16_r9 * FF(4294967296UL))) + + (avm_alu_u16_r10 * FF(281474976710656UL)))) * + FF(uint256_t{ 0UL, 0UL, 1UL, 0UL }))) - + avm_alu_ic)); tmp *= scaling_factor; std::get<18>(evals) += tmp; } @@ -426,12 +437,7 @@ template class avm_aluImpl { { Avm_DECLARE_VIEWS(19); - auto tmp = (avm_alu_op_not * - ((avm_alu_ia + avm_alu_ic) - ((((((avm_alu_u8_tag * FF(256)) + (avm_alu_u16_tag * FF(65536))) + - (avm_alu_u32_tag * FF(4294967296UL))) + - (avm_alu_u64_tag * FF(uint256_t{ 0UL, 1UL, 0UL, 0UL }))) + - (avm_alu_u128_tag * FF(uint256_t{ 0UL, 0UL, 1UL, 0UL }))) - - FF(1)))); + auto tmp = (avm_alu_op_not * avm_alu_ff_tag); tmp *= scaling_factor; std::get<19>(evals) += tmp; } @@ -439,7 +445,12 @@ template class avm_aluImpl { { Avm_DECLARE_VIEWS(20); - auto tmp = ((avm_alu_cmp_sel + avm_alu_op_eq) * (avm_alu_ic * (-avm_alu_ic + FF(1)))); + auto tmp = (avm_alu_op_not * + ((avm_alu_ia + avm_alu_ic) - ((((((avm_alu_u8_tag * FF(256)) + (avm_alu_u16_tag * FF(65536))) + + (avm_alu_u32_tag * FF(4294967296UL))) + + (avm_alu_u64_tag * FF(uint256_t{ 0UL, 1UL, 0UL, 0UL }))) + + (avm_alu_u128_tag * FF(uint256_t{ 0UL, 0UL, 1UL, 0UL }))) - + FF(1)))); tmp *= scaling_factor; std::get<20>(evals) += tmp; } @@ -447,11 +458,7 @@ template class avm_aluImpl { { Avm_DECLARE_VIEWS(21); - auto tmp = - (avm_alu_op_eq * ((((avm_alu_ia - avm_alu_ib) * - ((avm_alu_ic * (-avm_alu_op_eq_diff_inv + FF(1))) + avm_alu_op_eq_diff_inv)) - - FF(1)) + - avm_alu_ic)); + auto tmp = ((avm_alu_cmp_sel + avm_alu_op_eq) * (avm_alu_ic * (-avm_alu_ic + FF(1)))); tmp *= scaling_factor; std::get<21>(evals) += tmp; } @@ -459,8 +466,11 @@ template class avm_aluImpl { { Avm_DECLARE_VIEWS(22); - auto tmp = (((avm_alu_op_lt * avm_alu_ib) + (avm_alu_op_lte * avm_alu_ia)) - - ((avm_alu_a_lo + (avm_alu_a_hi * FF(uint256_t{ 0UL, 0UL, 1UL, 0UL }))) * avm_alu_cmp_sel)); + auto tmp = + (avm_alu_op_eq * ((((avm_alu_ia - avm_alu_ib) * + ((avm_alu_ic * (-avm_alu_op_eq_diff_inv + FF(1))) + avm_alu_op_eq_diff_inv)) - + FF(1)) + + avm_alu_ic)); tmp *= scaling_factor; std::get<22>(evals) += tmp; } @@ -468,8 +478,8 @@ template class avm_aluImpl { { Avm_DECLARE_VIEWS(23); - auto tmp = (((avm_alu_op_lt * avm_alu_ia) + (avm_alu_op_lte * avm_alu_ib)) - - ((avm_alu_b_lo + (avm_alu_b_hi * FF(uint256_t{ 0UL, 0UL, 1UL, 0UL }))) * avm_alu_cmp_sel)); + auto tmp = (((avm_alu_op_lt * avm_alu_ib) + (avm_alu_op_lte * avm_alu_ia)) - + ((avm_alu_a_lo + (avm_alu_a_hi * FF(uint256_t{ 0UL, 0UL, 1UL, 0UL }))) * avm_alu_cmp_sel)); tmp *= scaling_factor; std::get<23>(evals) += tmp; } @@ -477,7 +487,8 @@ template class avm_aluImpl { { Avm_DECLARE_VIEWS(24); - auto tmp = (avm_alu_p_a_borrow * (-avm_alu_p_a_borrow + FF(1))); + auto tmp = (((avm_alu_op_lt * avm_alu_ia) + (avm_alu_op_lte * avm_alu_ib)) - + ((avm_alu_b_lo + (avm_alu_b_hi * FF(uint256_t{ 0UL, 0UL, 1UL, 0UL }))) * avm_alu_cmp_sel)); tmp *= scaling_factor; std::get<24>(evals) += tmp; } @@ -485,10 +496,7 @@ template class avm_aluImpl { { Avm_DECLARE_VIEWS(25); - auto tmp = ((avm_alu_p_sub_a_lo - - ((-avm_alu_a_lo + FF(uint256_t{ 4891460686036598784UL, 2896914383306846353UL, 0UL, 0UL })) + - (avm_alu_p_a_borrow * FF(uint256_t{ 0UL, 0UL, 1UL, 0UL })))) * - avm_alu_cmp_sel); + auto tmp = (avm_alu_p_a_borrow * (-avm_alu_p_a_borrow + FF(1))); tmp *= scaling_factor; std::get<25>(evals) += tmp; } @@ -496,9 +504,9 @@ template class avm_aluImpl { { Avm_DECLARE_VIEWS(26); - auto tmp = ((avm_alu_p_sub_a_hi - - ((-avm_alu_a_hi + FF(uint256_t{ 13281191951274694749UL, 3486998266802970665UL, 0UL, 0UL })) - - avm_alu_p_a_borrow)) * + auto tmp = ((avm_alu_p_sub_a_lo - + ((-avm_alu_a_lo + FF(uint256_t{ 4891460686036598784UL, 2896914383306846353UL, 0UL, 0UL })) + + (avm_alu_p_a_borrow * FF(uint256_t{ 0UL, 0UL, 1UL, 0UL })))) * avm_alu_cmp_sel); tmp *= scaling_factor; std::get<26>(evals) += tmp; @@ -507,7 +515,10 @@ template class avm_aluImpl { { Avm_DECLARE_VIEWS(27); - auto tmp = (avm_alu_p_b_borrow * (-avm_alu_p_b_borrow + FF(1))); + auto tmp = ((avm_alu_p_sub_a_hi - + ((-avm_alu_a_hi + FF(uint256_t{ 13281191951274694749UL, 3486998266802970665UL, 0UL, 0UL })) - + avm_alu_p_a_borrow)) * + avm_alu_cmp_sel); tmp *= scaling_factor; std::get<27>(evals) += tmp; } @@ -515,27 +526,35 @@ template class avm_aluImpl { { Avm_DECLARE_VIEWS(28); + auto tmp = (avm_alu_p_b_borrow * (-avm_alu_p_b_borrow + FF(1))); + tmp *= scaling_factor; + std::get<28>(evals) += tmp; + } + // Contribution 29 + { + Avm_DECLARE_VIEWS(29); + auto tmp = ((avm_alu_p_sub_b_lo - ((-avm_alu_b_lo + FF(uint256_t{ 4891460686036598784UL, 2896914383306846353UL, 0UL, 0UL })) + (avm_alu_p_b_borrow * FF(uint256_t{ 0UL, 0UL, 1UL, 0UL })))) * avm_alu_cmp_sel); tmp *= scaling_factor; - std::get<28>(evals) += tmp; + std::get<29>(evals) += tmp; } - // Contribution 29 + // Contribution 30 { - Avm_DECLARE_VIEWS(29); + Avm_DECLARE_VIEWS(30); auto tmp = ((avm_alu_p_sub_b_hi - ((-avm_alu_b_hi + FF(uint256_t{ 13281191951274694749UL, 3486998266802970665UL, 0UL, 0UL })) - avm_alu_p_b_borrow)) * avm_alu_cmp_sel); tmp *= scaling_factor; - std::get<29>(evals) += tmp; + std::get<30>(evals) += tmp; } - // Contribution 30 + // Contribution 31 { - Avm_DECLARE_VIEWS(30); + Avm_DECLARE_VIEWS(31); auto tmp = ((avm_alu_res_lo - @@ -545,11 +564,11 @@ template class avm_aluImpl { (-((avm_alu_op_lt * avm_alu_ic) + ((-avm_alu_ic + FF(1)) * avm_alu_op_lte)) + FF(1))))) * avm_alu_cmp_sel); tmp *= scaling_factor; - std::get<30>(evals) += tmp; + std::get<31>(evals) += tmp; } - // Contribution 31 + // Contribution 32 { - Avm_DECLARE_VIEWS(31); + Avm_DECLARE_VIEWS(32); auto tmp = ((avm_alu_res_hi - ((((avm_alu_a_hi - avm_alu_b_hi) - avm_alu_borrow) * @@ -558,21 +577,13 @@ template class avm_aluImpl { (-((avm_alu_op_lt * avm_alu_ic) + ((-avm_alu_ic + FF(1)) * avm_alu_op_lte)) + FF(1))))) * avm_alu_cmp_sel); tmp *= scaling_factor; - std::get<31>(evals) += tmp; - } - // Contribution 32 - { - Avm_DECLARE_VIEWS(32); - - auto tmp = (((avm_alu_cmp_rng_ctr_shift - avm_alu_cmp_rng_ctr) + FF(1)) * avm_alu_cmp_rng_ctr); - tmp *= scaling_factor; std::get<32>(evals) += tmp; } // Contribution 33 { Avm_DECLARE_VIEWS(33); - auto tmp = ((avm_alu_cmp_rng_ctr_shift - FF(4)) * avm_alu_cmp_sel); + auto tmp = (((avm_alu_cmp_rng_ctr_shift - avm_alu_cmp_rng_ctr) + FF(1)) * avm_alu_cmp_rng_ctr); tmp *= scaling_factor; std::get<33>(evals) += tmp; } @@ -580,7 +591,7 @@ template class avm_aluImpl { { Avm_DECLARE_VIEWS(34); - auto tmp = (avm_alu_rng_chk_sel * (-avm_alu_rng_chk_sel + FF(1))); + auto tmp = ((avm_alu_cmp_rng_ctr_shift - FF(4)) * avm_alu_cmp_sel); tmp *= scaling_factor; std::get<34>(evals) += tmp; } @@ -588,7 +599,7 @@ template class avm_aluImpl { { Avm_DECLARE_VIEWS(35); - auto tmp = (avm_alu_rng_chk_sel * avm_alu_cmp_sel); + auto tmp = (avm_alu_rng_chk_sel * (-avm_alu_rng_chk_sel + FF(1))); tmp *= scaling_factor; std::get<35>(evals) += tmp; } @@ -596,9 +607,7 @@ template class avm_aluImpl { { Avm_DECLARE_VIEWS(36); - auto tmp = ((avm_alu_cmp_rng_ctr * (((-avm_alu_rng_chk_sel + FF(1)) * (-avm_alu_op_eq_diff_inv + FF(1))) + - avm_alu_op_eq_diff_inv)) - - avm_alu_rng_chk_sel); + auto tmp = (avm_alu_rng_chk_sel * avm_alu_cmp_sel); tmp *= scaling_factor; std::get<36>(evals) += tmp; } @@ -606,7 +615,9 @@ template class avm_aluImpl { { Avm_DECLARE_VIEWS(37); - auto tmp = (avm_alu_rng_chk_lookup_selector - (avm_alu_cmp_sel + avm_alu_rng_chk_sel)); + auto tmp = ((avm_alu_cmp_rng_ctr * (((-avm_alu_rng_chk_sel + FF(1)) * (-avm_alu_op_eq_diff_inv + FF(1))) + + avm_alu_op_eq_diff_inv)) - + avm_alu_rng_chk_sel); tmp *= scaling_factor; std::get<37>(evals) += tmp; } @@ -614,6 +625,18 @@ template class avm_aluImpl { { Avm_DECLARE_VIEWS(38); + auto tmp = (avm_alu_rng_chk_lookup_selector_shift - + (((((avm_alu_cmp_sel_shift + avm_alu_rng_chk_sel_shift) + avm_alu_op_add_shift) + + avm_alu_op_sub_shift) + + avm_alu_op_mul_shift) + + (avm_alu_op_mul * avm_alu_u128_tag))); + tmp *= scaling_factor; + std::get<38>(evals) += tmp; + } + // Contribution 39 + { + Avm_DECLARE_VIEWS(39); + auto tmp = (avm_alu_a_lo - (((((((((avm_alu_u8_r0 + (avm_alu_u8_r1 * FF(256))) + (avm_alu_u16_r0 * FF(65536))) + (avm_alu_u16_r1 * FF(4294967296UL))) + @@ -624,11 +647,11 @@ template class avm_aluImpl { (avm_alu_u16_r6 * FF(uint256_t{ 0UL, 281474976710656UL, 0UL, 0UL }))) * (avm_alu_rng_chk_sel + avm_alu_cmp_sel))); tmp *= scaling_factor; - std::get<38>(evals) += tmp; + std::get<39>(evals) += tmp; } - // Contribution 39 + // Contribution 40 { - Avm_DECLARE_VIEWS(39); + Avm_DECLARE_VIEWS(40); auto tmp = (avm_alu_a_hi - ((((((((avm_alu_u16_r7 + (avm_alu_u16_r8 * FF(65536))) + (avm_alu_u16_r9 * FF(4294967296UL))) + @@ -639,21 +662,13 @@ template class avm_aluImpl { (avm_alu_u16_r14 * FF(uint256_t{ 0UL, 281474976710656UL, 0UL, 0UL }))) * (avm_alu_rng_chk_sel + avm_alu_cmp_sel))); tmp *= scaling_factor; - std::get<39>(evals) += tmp; - } - // Contribution 40 - { - Avm_DECLARE_VIEWS(40); - - auto tmp = ((avm_alu_a_lo_shift - avm_alu_b_lo) * avm_alu_rng_chk_sel_shift); - tmp *= scaling_factor; std::get<40>(evals) += tmp; } // Contribution 41 { Avm_DECLARE_VIEWS(41); - auto tmp = ((avm_alu_a_hi_shift - avm_alu_b_hi) * avm_alu_rng_chk_sel_shift); + auto tmp = ((avm_alu_a_lo_shift - avm_alu_b_lo) * avm_alu_rng_chk_sel_shift); tmp *= scaling_factor; std::get<41>(evals) += tmp; } @@ -661,7 +676,7 @@ template class avm_aluImpl { { Avm_DECLARE_VIEWS(42); - auto tmp = ((avm_alu_b_lo_shift - avm_alu_p_sub_a_lo) * avm_alu_rng_chk_sel_shift); + auto tmp = ((avm_alu_a_hi_shift - avm_alu_b_hi) * avm_alu_rng_chk_sel_shift); tmp *= scaling_factor; std::get<42>(evals) += tmp; } @@ -669,7 +684,7 @@ template class avm_aluImpl { { Avm_DECLARE_VIEWS(43); - auto tmp = ((avm_alu_b_hi_shift - avm_alu_p_sub_a_hi) * avm_alu_rng_chk_sel_shift); + auto tmp = ((avm_alu_b_lo_shift - avm_alu_p_sub_a_lo) * avm_alu_rng_chk_sel_shift); tmp *= scaling_factor; std::get<43>(evals) += tmp; } @@ -677,7 +692,7 @@ template class avm_aluImpl { { Avm_DECLARE_VIEWS(44); - auto tmp = ((avm_alu_p_sub_a_lo_shift - avm_alu_p_sub_b_lo) * avm_alu_rng_chk_sel_shift); + auto tmp = ((avm_alu_b_hi_shift - avm_alu_p_sub_a_hi) * avm_alu_rng_chk_sel_shift); tmp *= scaling_factor; std::get<44>(evals) += tmp; } @@ -685,7 +700,7 @@ template class avm_aluImpl { { Avm_DECLARE_VIEWS(45); - auto tmp = ((avm_alu_p_sub_a_hi_shift - avm_alu_p_sub_b_hi) * avm_alu_rng_chk_sel_shift); + auto tmp = ((avm_alu_p_sub_a_lo_shift - avm_alu_p_sub_b_lo) * avm_alu_rng_chk_sel_shift); tmp *= scaling_factor; std::get<45>(evals) += tmp; } @@ -693,7 +708,7 @@ template class avm_aluImpl { { Avm_DECLARE_VIEWS(46); - auto tmp = ((avm_alu_p_sub_b_lo_shift - avm_alu_res_lo) * avm_alu_rng_chk_sel_shift); + auto tmp = ((avm_alu_p_sub_a_hi_shift - avm_alu_p_sub_b_hi) * avm_alu_rng_chk_sel_shift); tmp *= scaling_factor; std::get<46>(evals) += tmp; } @@ -701,10 +716,18 @@ template class avm_aluImpl { { Avm_DECLARE_VIEWS(47); - auto tmp = ((avm_alu_p_sub_b_hi_shift - avm_alu_res_hi) * avm_alu_rng_chk_sel_shift); + auto tmp = ((avm_alu_p_sub_b_lo_shift - avm_alu_res_lo) * avm_alu_rng_chk_sel_shift); tmp *= scaling_factor; std::get<47>(evals) += tmp; } + // Contribution 48 + { + Avm_DECLARE_VIEWS(48); + + auto tmp = ((avm_alu_p_sub_b_hi_shift - avm_alu_res_hi) * avm_alu_rng_chk_sel_shift); + tmp *= scaling_factor; + std::get<48>(evals) += tmp; + } } }; diff --git a/barretenberg/cpp/src/barretenberg/relations/generated/avm/declare_views.hpp b/barretenberg/cpp/src/barretenberg/relations/generated/avm/declare_views.hpp index 168d0b96d077..05c47520ab45 100644 --- a/barretenberg/cpp/src/barretenberg/relations/generated/avm/declare_views.hpp +++ b/barretenberg/cpp/src/barretenberg/relations/generated/avm/declare_views.hpp @@ -56,7 +56,6 @@ [[maybe_unused]] auto avm_alu_u16_r9 = View(new_term.avm_alu_u16_r9); \ [[maybe_unused]] auto avm_alu_u16_tag = View(new_term.avm_alu_u16_tag); \ [[maybe_unused]] auto avm_alu_u32_tag = View(new_term.avm_alu_u32_tag); \ - [[maybe_unused]] auto avm_alu_u64_r0 = View(new_term.avm_alu_u64_r0); \ [[maybe_unused]] auto avm_alu_u64_tag = View(new_term.avm_alu_u64_tag); \ [[maybe_unused]] auto avm_alu_u8_r0 = View(new_term.avm_alu_u8_r0); \ [[maybe_unused]] auto avm_alu_u8_r1 = View(new_term.avm_alu_u8_r1); \ @@ -219,10 +218,16 @@ [[maybe_unused]] auto avm_alu_b_hi_shift = View(new_term.avm_alu_b_hi_shift); \ [[maybe_unused]] auto avm_alu_b_lo_shift = View(new_term.avm_alu_b_lo_shift); \ [[maybe_unused]] auto avm_alu_cmp_rng_ctr_shift = View(new_term.avm_alu_cmp_rng_ctr_shift); \ + [[maybe_unused]] auto avm_alu_cmp_sel_shift = View(new_term.avm_alu_cmp_sel_shift); \ + [[maybe_unused]] auto avm_alu_op_add_shift = View(new_term.avm_alu_op_add_shift); \ + [[maybe_unused]] auto avm_alu_op_mul_shift = View(new_term.avm_alu_op_mul_shift); \ + [[maybe_unused]] auto avm_alu_op_sub_shift = View(new_term.avm_alu_op_sub_shift); \ [[maybe_unused]] auto avm_alu_p_sub_a_hi_shift = View(new_term.avm_alu_p_sub_a_hi_shift); \ [[maybe_unused]] auto avm_alu_p_sub_a_lo_shift = View(new_term.avm_alu_p_sub_a_lo_shift); \ [[maybe_unused]] auto avm_alu_p_sub_b_hi_shift = View(new_term.avm_alu_p_sub_b_hi_shift); \ [[maybe_unused]] auto avm_alu_p_sub_b_lo_shift = View(new_term.avm_alu_p_sub_b_lo_shift); \ + [[maybe_unused]] auto avm_alu_rng_chk_lookup_selector_shift = \ + View(new_term.avm_alu_rng_chk_lookup_selector_shift); \ [[maybe_unused]] auto avm_alu_rng_chk_sel_shift = View(new_term.avm_alu_rng_chk_sel_shift); \ [[maybe_unused]] auto avm_alu_u16_r0_shift = View(new_term.avm_alu_u16_r0_shift); \ [[maybe_unused]] auto avm_alu_u16_r1_shift = View(new_term.avm_alu_u16_r1_shift); \ @@ -231,7 +236,8 @@ [[maybe_unused]] auto avm_alu_u16_r4_shift = View(new_term.avm_alu_u16_r4_shift); \ [[maybe_unused]] auto avm_alu_u16_r5_shift = View(new_term.avm_alu_u16_r5_shift); \ [[maybe_unused]] auto avm_alu_u16_r6_shift = View(new_term.avm_alu_u16_r6_shift); \ - [[maybe_unused]] auto avm_alu_u16_r7_shift = View(new_term.avm_alu_u16_r7_shift); \ + [[maybe_unused]] auto avm_alu_u8_r0_shift = View(new_term.avm_alu_u8_r0_shift); \ + [[maybe_unused]] auto avm_alu_u8_r1_shift = View(new_term.avm_alu_u8_r1_shift); \ [[maybe_unused]] auto avm_binary_acc_ia_shift = View(new_term.avm_binary_acc_ia_shift); \ [[maybe_unused]] auto avm_binary_acc_ib_shift = View(new_term.avm_binary_acc_ib_shift); \ [[maybe_unused]] auto avm_binary_acc_ic_shift = View(new_term.avm_binary_acc_ic_shift); \ diff --git a/barretenberg/cpp/src/barretenberg/vm/avm_trace/avm_alu_trace.cpp b/barretenberg/cpp/src/barretenberg/vm/avm_trace/avm_alu_trace.cpp index 8414c411c3cb..f92dcb2668d5 100644 --- a/barretenberg/cpp/src/barretenberg/vm/avm_trace/avm_alu_trace.cpp +++ b/barretenberg/cpp/src/barretenberg/vm/avm_trace/avm_alu_trace.cpp @@ -26,6 +26,7 @@ AvmAluTraceBuilder::AvmAluTraceBuilder() void AvmAluTraceBuilder::reset() { alu_trace.clear(); + range_checked_required = false; } /** @@ -38,6 +39,16 @@ std::vector AvmAluTraceBuilder::finalize() return std::move(alu_trace); } +/** + * @brief Helper routine telling whether range check is required. + * + * @return A boolean telling whether range check is required. + */ +bool AvmAluTraceBuilder::is_range_check_required() const +{ + return range_checked_required; +} + /** * @brief Build Alu trace and compute the result of an addition of type defined by in_tag. * Besides the addition calculation, for the types u8, u16, u32, u64, and u128, we @@ -93,19 +104,15 @@ FF AvmAluTraceBuilder::op_add(FF const& a, FF const& b, AvmMemoryTag in_tag, uin if (c_u128 < a_u128) { carry = true; } - - uint128_t c_trunc_128 = c_u128; - alu_u8_r0 = static_cast(c_trunc_128); - c_trunc_128 >>= 8; - alu_u8_r1 = static_cast(c_trunc_128); - c_trunc_128 >>= 8; - - for (size_t i = 0; i < 7; i++) { - alu_u16_reg.at(i) = static_cast(c_trunc_128); - c_trunc_128 >>= 16; - } } + // The range checks are activated for all tags and therefore we need to call the slice register + // routines also for tag FF with input 0. + auto [u8_r0, u8_r1, u16_reg] = to_alu_slice_registers(in_tag == AvmMemoryTag::FF ? 0 : c_u128); + alu_u8_r0 = u8_r0; + alu_u8_r1 = u8_r1; + alu_u16_reg = u16_reg; + alu_trace.push_back(AvmAluTraceBuilder::AluTraceEntry{ .alu_clk = clk, .alu_op_add = true, @@ -181,19 +188,15 @@ FF AvmAluTraceBuilder::op_sub(FF const& a, FF const& b, AvmMemoryTag in_tag, uin if (a_u128 < b_u128) { carry = true; } - - uint128_t c_trunc_128 = c_u128; - alu_u8_r0 = static_cast(c_trunc_128); - c_trunc_128 >>= 8; - alu_u8_r1 = static_cast(c_trunc_128); - c_trunc_128 >>= 8; - - for (size_t i = 0; i < 7; i++) { - alu_u16_reg.at(i) = static_cast(c_trunc_128); - c_trunc_128 >>= 16; - } } + // The range checks are activated for all tags and therefore we need to call the slice register + // routines also for tag FF with input 0. + auto [u8_r0, u8_r1, u16_reg] = to_alu_slice_registers(in_tag == AvmMemoryTag::FF ? 0 : c_u128); + alu_u8_r0 = u8_r0; + alu_u8_r1 = u8_r1; + alu_u16_reg = u16_reg; + alu_trace.push_back(AvmAluTraceBuilder::AluTraceEntry{ .alu_clk = clk, .alu_op_sub = true, @@ -265,31 +268,32 @@ FF AvmAluTraceBuilder::op_mul(FF const& a, FF const& b, AvmMemoryTag in_tag, uin uint128_t c_u128 = a_u128 * b_u128; - // Decompose a_u128 and b_u128 over 8 16-bit registers. - std::array alu_u16_reg_a; // Will be initialized in for loop below. - std::array alu_u16_reg_b; // Will be initialized in for loop below. - uint128_t a_trunc_128 = a_u128; - uint128_t b_trunc_128 = b_u128; - - for (size_t i = 0; i < 8; i++) { - alu_u16_reg_a.at(i) = static_cast(a_trunc_128); - alu_u16_reg_b.at(i) = static_cast(b_trunc_128); - a_trunc_128 >>= 16; - b_trunc_128 >>= 16; - } + // Decompose a_u128 and b_u128 over 8/16-bit registers. + auto [a_u8_r0, a_u8_r1, a_u16_reg] = to_alu_slice_registers(a_u128); + auto [b_u8_r0, b_u8_r1, b_u16_reg] = to_alu_slice_registers(b_u128); // Represent a, b with 64-bit limbs: a = a_l + 2^64 * a_h, b = b_l + 2^64 * b_h, // c_high := 2^128 * a_h * b_h uint256_t c_high = ((a_u256 >> 64) * (b_u256 >> 64)) << 128; - // From PIL relation in avm_alu.pil, we need to determine the bit CF and 64-bit value R' in - // a * b_l + a_l * b_h * 2^64 = (CF * 2^64 + R') * 2^128 + c + // From PIL relation in avm_alu.pil, we need to determine the bit CF and 64-bit value R_64 in + // a * b_l + a_l * b_h * 2^64 = (CF * 2^64 + R_64) * 2^128 + c // LHS is c_u256 - c_high // CF bit carry = ((c_u256 - c_high) >> 192) > 0; - // R' value - uint64_t alu_u64_r0 = static_cast(((c_u256 - c_high) >> 128) & uint256_t(UINT64_MAX)); + // R_64 value + uint64_t r_64 = static_cast(((c_u256 - c_high) >> 128) & uint256_t(UINT64_MAX)); + + // Decompose R_64 over 16-bit registers u16_r7, u16_r8, u16_r9, u_16_r10 + for (size_t i = 0; i < 4; i++) { + auto const slice = static_cast(r_64); + assert(a_u16_reg.at(7 + i) == 0); + u16_range_chk_counters[7 + i][0]--; + a_u16_reg.at(7 + i) = slice; + u16_range_chk_counters[7 + i][slice]++; + r_64 >>= 16; + } c = FF{ uint256_t::from_uint128(c_u128) }; @@ -301,12 +305,15 @@ FF AvmAluTraceBuilder::op_mul(FF const& a, FF const& b, AvmMemoryTag in_tag, uin .alu_ib = b, .alu_ic = c, .alu_cf = carry, - .alu_u16_reg = alu_u16_reg_a, - .alu_u64_r0 = alu_u64_r0, + .alu_u8_r0 = a_u8_r0, + .alu_u8_r1 = a_u8_r1, + .alu_u16_reg = a_u16_reg, }); alu_trace.push_back(AvmAluTraceBuilder::AluTraceEntry{ - .alu_u16_reg = alu_u16_reg_b, + .alu_u8_r0 = b_u8_r0, + .alu_u8_r1 = b_u8_r1, + .alu_u16_reg = b_u16_reg, }); return c; @@ -315,21 +322,13 @@ FF AvmAluTraceBuilder::op_mul(FF const& a, FF const& b, AvmMemoryTag in_tag, uin return FF{ 0 }; } - // Following code executed for: u8, u16, u32, u64 (u128 returned handled specifically) - if (in_tag != AvmMemoryTag::FF) { - // Decomposition of c_u128 into 8-bit and 16-bit registers as follows: - // alu_u8_r0 + alu_u8_r1 * 2^8 + alu_u16_r0 * 2^16 ... + alu_u16_r6 * 2^112 - uint128_t c_trunc_128 = c_u128; - alu_u8_r0 = static_cast(c_trunc_128); - c_trunc_128 >>= 8; - alu_u8_r1 = static_cast(c_trunc_128); - c_trunc_128 >>= 8; - - for (size_t i = 0; i < 7; i++) { - alu_u16_reg.at(i) = static_cast(c_trunc_128); - c_trunc_128 >>= 16; - } - } + // Following code executed for: u8, u16, u32, u64 (u128 returned handled specifically). + // The range checks are activated for all tags and therefore we need to call the slice register + // routines also for tag FF with input 0. + auto [u8_r0, u8_r1, u16_reg] = to_alu_slice_registers(in_tag == AvmMemoryTag::FF ? 0 : c_u128); + alu_u8_r0 = u8_r0; + alu_u8_r1 = u8_r1; + alu_u16_reg = u16_reg; // Following code executed for: ff, u8, u16, u32, u64 (u128 returned handled specifically) alu_trace.push_back(AvmAluTraceBuilder::AluTraceEntry{ @@ -445,17 +444,18 @@ FF AvmAluTraceBuilder::op_eq(FF const& a, FF const& b, AvmMemoryTag in_tag, uint * @return A triplet of */ template -std::tuple> AvmAluTraceBuilder::to_alu_slice_registers(T a) +std::tuple> AvmAluTraceBuilder::to_alu_slice_registers(T a) { + range_checked_required = true; auto alu_u8_r0 = static_cast(a); a >>= 8; auto alu_u8_r1 = static_cast(a); a >>= 8; - std::vector alu_u16_reg{}; + std::array alu_u16_reg; for (size_t i = 0; i < 15; i++) { auto alu_u16 = static_cast(a); u16_range_chk_counters[i][alu_u16]++; - alu_u16_reg.push_back(alu_u16); + alu_u16_reg.at(i) = alu_u16; a >>= 16; } u8_range_chk_counters[0][alu_u8_r0]++; @@ -493,7 +493,7 @@ std::vector AvmAluTraceBuilder::cmp_range_che auto [alu_u8_r0, alu_u8_r1, alu_u16_reg] = AvmAluTraceBuilder::to_alu_slice_registers(limb); r.alu_u8_r0 = alu_u8_r0; r.alu_u8_r1 = alu_u8_r1; - std::copy(alu_u16_reg.begin(), alu_u16_reg.end(), r.alu_u16_reg.begin()); + r.alu_u16_reg = alu_u16_reg; r.cmp_rng_ctr = j > 0 ? static_cast(num_rows - j) : 0; r.rng_chk_sel = j > 0; diff --git a/barretenberg/cpp/src/barretenberg/vm/avm_trace/avm_alu_trace.hpp b/barretenberg/cpp/src/barretenberg/vm/avm_trace/avm_alu_trace.hpp index 7d15c2f70df9..cb12ab925ed6 100644 --- a/barretenberg/cpp/src/barretenberg/vm/avm_trace/avm_alu_trace.hpp +++ b/barretenberg/cpp/src/barretenberg/vm/avm_trace/avm_alu_trace.hpp @@ -40,8 +40,6 @@ class AvmAluTraceBuilder { std::array alu_u16_reg{}; - uint64_t alu_u64_r0{}; - FF alu_op_eq_diff_inv{}; // Comparison Operation @@ -69,10 +67,13 @@ class AvmAluTraceBuilder { FF op_lt(FF const& a, FF const& b, AvmMemoryTag in_tag, uint32_t clk); FF op_lte(FF const& a, FF const& b, AvmMemoryTag in_tag, uint32_t clk); + bool is_range_check_required() const; + private: std::vector alu_trace; - template std::tuple> to_alu_slice_registers(T a); + bool range_checked_required = false; + + template std::tuple> to_alu_slice_registers(T a); std::vector cmp_range_check_helper(AluTraceEntry row, std::vector hi_lo_limbs); - void count_range_checks(AluTraceEntry const& entry); }; } // namespace bb::avm_trace diff --git a/barretenberg/cpp/src/barretenberg/vm/avm_trace/avm_trace.cpp b/barretenberg/cpp/src/barretenberg/vm/avm_trace/avm_trace.cpp index 5c4a20515ad5..a9e27af41274 100644 --- a/barretenberg/cpp/src/barretenberg/vm/avm_trace/avm_trace.cpp +++ b/barretenberg/cpp/src/barretenberg/vm/avm_trace/avm_trace.cpp @@ -648,7 +648,6 @@ void AvmTraceBuilder::op_lt( FF c = tag_match ? alu_trace_builder.op_lt(a, b, in_tag, clk) : FF(0); - range_checked_required = true; // Write into memory value c from intermediate register ic. mem_trace_builder.write_into_memory(clk, IntermRegister::IC, res.direct_c_offset, c, in_tag, AvmMemoryTag::U8); @@ -699,7 +698,6 @@ void AvmTraceBuilder::op_lte( FF c = tag_match ? alu_trace_builder.op_lte(a, b, in_tag, clk) : FF(0); - range_checked_required = true; // Write into memory value c from intermediate register ic. mem_trace_builder.write_into_memory(clk, IntermRegister::IC, res.direct_c_offset, c, in_tag, AvmMemoryTag::U8); @@ -1330,6 +1328,8 @@ void AvmTraceBuilder::finalise_mem_trace_lookup_counts() */ std::vector AvmTraceBuilder::finalize() { + bool const range_check_required = alu_trace_builder.is_range_check_required(); + auto mem_trace = mem_trace_builder.finalize(); auto alu_trace = alu_trace_builder.finalize(); auto bin_trace = bin_trace_builder.finalize(); @@ -1345,7 +1345,7 @@ std::vector AvmTraceBuilder::finalize() // If the bin_trace_size has entries, we need the main_trace to be as big as our byte lookup table (3 * 2**16 // long) size_t const lookup_table_size = bin_trace_size > 0 ? 3 * (1 << 16) : 0; - size_t const range_check_size = range_checked_required ? UINT16_MAX + 1 : 0; + size_t const range_check_size = range_check_required ? UINT16_MAX + 1 : 0; std::vector trace_sizes = { mem_trace_size, main_trace_size, alu_trace_size, lookup_table_size, range_check_size }; @@ -1480,7 +1480,6 @@ std::vector AvmTraceBuilder::finalize() dest.avm_alu_u16_r13 = FF(src.alu_u16_reg.at(13)); dest.avm_alu_u16_r14 = FF(src.alu_u16_reg.at(14)); - dest.avm_alu_u64_r0 = FF(src.alu_u64_r0); dest.avm_alu_op_eq_diff_inv = FF(src.alu_op_eq_diff_inv); // Not all rows in ALU are enabled with a selector. For instance, @@ -1508,6 +1507,15 @@ std::vector AvmTraceBuilder::finalize() dest.avm_alu_cmp_rng_ctr = FF(static_cast(src.cmp_rng_ctr)); dest.avm_alu_rng_chk_lookup_selector = FF(1); } + + if (dest.avm_alu_op_add == FF(1) || dest.avm_alu_op_sub == FF(1) || dest.avm_alu_op_mul == FF(1)) { + dest.avm_alu_rng_chk_lookup_selector = FF(1); + } + + // Multiplication over u128 expands over two rows. + if (dest.avm_alu_op_mul == FF(1) && dest.avm_alu_u128_tag) { + main_trace.at(i + 1).avm_alu_rng_chk_lookup_selector = FF(1); + } } for (size_t i = 0; i < main_trace_size; i++) { diff --git a/barretenberg/cpp/src/barretenberg/vm/avm_trace/avm_trace.hpp b/barretenberg/cpp/src/barretenberg/vm/avm_trace/avm_trace.hpp index c4e72a0c3ffc..9918144f5f32 100644 --- a/barretenberg/cpp/src/barretenberg/vm/avm_trace/avm_trace.hpp +++ b/barretenberg/cpp/src/barretenberg/vm/avm_trace/avm_trace.hpp @@ -117,8 +117,6 @@ class AvmTraceBuilder { AvmAluTraceBuilder alu_trace_builder; AvmBinaryTraceBuilder bin_trace_builder; - bool range_checked_required = false; - void finalise_mem_trace_lookup_counts(); IndirectThreeResolution resolve_ind_three( diff --git a/barretenberg/cpp/src/barretenberg/vm/generated/avm_circuit_builder.hpp b/barretenberg/cpp/src/barretenberg/vm/generated/avm_circuit_builder.hpp index fe2b81f0e340..4a163364de3e 100644 --- a/barretenberg/cpp/src/barretenberg/vm/generated/avm_circuit_builder.hpp +++ b/barretenberg/cpp/src/barretenberg/vm/generated/avm_circuit_builder.hpp @@ -105,7 +105,6 @@ template struct AvmFullRow { FF avm_alu_u16_r9{}; FF avm_alu_u16_tag{}; FF avm_alu_u32_tag{}; - FF avm_alu_u64_r0{}; FF avm_alu_u64_tag{}; FF avm_alu_u8_r0{}; FF avm_alu_u8_r1{}; @@ -268,10 +267,15 @@ template struct AvmFullRow { FF avm_alu_b_hi_shift{}; FF avm_alu_b_lo_shift{}; FF avm_alu_cmp_rng_ctr_shift{}; + FF avm_alu_cmp_sel_shift{}; + FF avm_alu_op_add_shift{}; + FF avm_alu_op_mul_shift{}; + FF avm_alu_op_sub_shift{}; FF avm_alu_p_sub_a_hi_shift{}; FF avm_alu_p_sub_a_lo_shift{}; FF avm_alu_p_sub_b_hi_shift{}; FF avm_alu_p_sub_b_lo_shift{}; + FF avm_alu_rng_chk_lookup_selector_shift{}; FF avm_alu_rng_chk_sel_shift{}; FF avm_alu_u16_r0_shift{}; FF avm_alu_u16_r1_shift{}; @@ -280,7 +284,8 @@ template struct AvmFullRow { FF avm_alu_u16_r4_shift{}; FF avm_alu_u16_r5_shift{}; FF avm_alu_u16_r6_shift{}; - FF avm_alu_u16_r7_shift{}; + FF avm_alu_u8_r0_shift{}; + FF avm_alu_u8_r1_shift{}; FF avm_binary_acc_ia_shift{}; FF avm_binary_acc_ib_shift{}; FF avm_binary_acc_ic_shift{}; @@ -304,8 +309,8 @@ class AvmCircuitBuilder { using Polynomial = Flavor::Polynomial; using ProverPolynomials = Flavor::ProverPolynomials; - static constexpr size_t num_fixed_columns = 241; - static constexpr size_t num_polys = 212; + static constexpr size_t num_fixed_columns = 246; + static constexpr size_t num_polys = 211; std::vector rows; void set_trace(std::vector&& trace) { rows = std::move(trace); } @@ -375,7 +380,6 @@ class AvmCircuitBuilder { polys.avm_alu_u16_r9[i] = rows[i].avm_alu_u16_r9; polys.avm_alu_u16_tag[i] = rows[i].avm_alu_u16_tag; polys.avm_alu_u32_tag[i] = rows[i].avm_alu_u32_tag; - polys.avm_alu_u64_r0[i] = rows[i].avm_alu_u64_r0; polys.avm_alu_u64_tag[i] = rows[i].avm_alu_u64_tag; polys.avm_alu_u8_r0[i] = rows[i].avm_alu_u8_r0; polys.avm_alu_u8_r1[i] = rows[i].avm_alu_u8_r1; @@ -509,10 +513,15 @@ class AvmCircuitBuilder { polys.avm_alu_b_hi_shift = Polynomial(polys.avm_alu_b_hi.shifted()); polys.avm_alu_b_lo_shift = Polynomial(polys.avm_alu_b_lo.shifted()); polys.avm_alu_cmp_rng_ctr_shift = Polynomial(polys.avm_alu_cmp_rng_ctr.shifted()); + polys.avm_alu_cmp_sel_shift = Polynomial(polys.avm_alu_cmp_sel.shifted()); + polys.avm_alu_op_add_shift = Polynomial(polys.avm_alu_op_add.shifted()); + polys.avm_alu_op_mul_shift = Polynomial(polys.avm_alu_op_mul.shifted()); + polys.avm_alu_op_sub_shift = Polynomial(polys.avm_alu_op_sub.shifted()); polys.avm_alu_p_sub_a_hi_shift = Polynomial(polys.avm_alu_p_sub_a_hi.shifted()); polys.avm_alu_p_sub_a_lo_shift = Polynomial(polys.avm_alu_p_sub_a_lo.shifted()); polys.avm_alu_p_sub_b_hi_shift = Polynomial(polys.avm_alu_p_sub_b_hi.shifted()); polys.avm_alu_p_sub_b_lo_shift = Polynomial(polys.avm_alu_p_sub_b_lo.shifted()); + polys.avm_alu_rng_chk_lookup_selector_shift = Polynomial(polys.avm_alu_rng_chk_lookup_selector.shifted()); polys.avm_alu_rng_chk_sel_shift = Polynomial(polys.avm_alu_rng_chk_sel.shifted()); polys.avm_alu_u16_r0_shift = Polynomial(polys.avm_alu_u16_r0.shifted()); polys.avm_alu_u16_r1_shift = Polynomial(polys.avm_alu_u16_r1.shifted()); @@ -521,7 +530,8 @@ class AvmCircuitBuilder { polys.avm_alu_u16_r4_shift = Polynomial(polys.avm_alu_u16_r4.shifted()); polys.avm_alu_u16_r5_shift = Polynomial(polys.avm_alu_u16_r5.shifted()); polys.avm_alu_u16_r6_shift = Polynomial(polys.avm_alu_u16_r6.shifted()); - polys.avm_alu_u16_r7_shift = Polynomial(polys.avm_alu_u16_r7.shifted()); + polys.avm_alu_u8_r0_shift = Polynomial(polys.avm_alu_u8_r0.shifted()); + polys.avm_alu_u8_r1_shift = Polynomial(polys.avm_alu_u8_r1.shifted()); polys.avm_binary_acc_ia_shift = Polynomial(polys.avm_binary_acc_ia.shifted()); polys.avm_binary_acc_ib_shift = Polynomial(polys.avm_binary_acc_ib.shifted()); polys.avm_binary_acc_ic_shift = Polynomial(polys.avm_binary_acc_ic.shifted()); diff --git a/barretenberg/cpp/src/barretenberg/vm/generated/avm_flavor.hpp b/barretenberg/cpp/src/barretenberg/vm/generated/avm_flavor.hpp index 0964aa336324..4bb786ea4cb5 100644 --- a/barretenberg/cpp/src/barretenberg/vm/generated/avm_flavor.hpp +++ b/barretenberg/cpp/src/barretenberg/vm/generated/avm_flavor.hpp @@ -69,11 +69,11 @@ class AvmFlavor { using RelationSeparator = FF; static constexpr size_t NUM_PRECOMPUTED_ENTITIES = 2; - static constexpr size_t NUM_WITNESS_ENTITIES = 210; + static constexpr size_t NUM_WITNESS_ENTITIES = 209; static constexpr size_t NUM_WIRES = NUM_WITNESS_ENTITIES + NUM_PRECOMPUTED_ENTITIES; // We have two copies of the witness entities, so we subtract the number of fixed ones (they have no shift), one for // the unshifted and one for the shifted - static constexpr size_t NUM_ALL_ENTITIES = 241; + static constexpr size_t NUM_ALL_ENTITIES = 246; using GrandProductRelations = std::tuple, perm_main_bin_relation, @@ -227,7 +227,6 @@ class AvmFlavor { avm_alu_u16_r9, avm_alu_u16_tag, avm_alu_u32_tag, - avm_alu_u64_r0, avm_alu_u64_tag, avm_alu_u8_r0, avm_alu_u8_r1, @@ -440,7 +439,6 @@ class AvmFlavor { avm_alu_u16_r9, avm_alu_u16_tag, avm_alu_u32_tag, - avm_alu_u64_r0, avm_alu_u64_tag, avm_alu_u8_r0, avm_alu_u8_r1, @@ -658,7 +656,6 @@ class AvmFlavor { avm_alu_u16_r9, avm_alu_u16_tag, avm_alu_u32_tag, - avm_alu_u64_r0, avm_alu_u64_tag, avm_alu_u8_r0, avm_alu_u8_r1, @@ -821,10 +818,15 @@ class AvmFlavor { avm_alu_b_hi_shift, avm_alu_b_lo_shift, avm_alu_cmp_rng_ctr_shift, + avm_alu_cmp_sel_shift, + avm_alu_op_add_shift, + avm_alu_op_mul_shift, + avm_alu_op_sub_shift, avm_alu_p_sub_a_hi_shift, avm_alu_p_sub_a_lo_shift, avm_alu_p_sub_b_hi_shift, avm_alu_p_sub_b_lo_shift, + avm_alu_rng_chk_lookup_selector_shift, avm_alu_rng_chk_sel_shift, avm_alu_u16_r0_shift, avm_alu_u16_r1_shift, @@ -833,7 +835,8 @@ class AvmFlavor { avm_alu_u16_r4_shift, avm_alu_u16_r5_shift, avm_alu_u16_r6_shift, - avm_alu_u16_r7_shift, + avm_alu_u8_r0_shift, + avm_alu_u8_r1_shift, avm_binary_acc_ia_shift, avm_binary_acc_ib_shift, avm_binary_acc_ic_shift, @@ -902,7 +905,6 @@ class AvmFlavor { avm_alu_u16_r9, avm_alu_u16_tag, avm_alu_u32_tag, - avm_alu_u64_r0, avm_alu_u64_tag, avm_alu_u8_r0, avm_alu_u8_r1, @@ -1065,10 +1067,15 @@ class AvmFlavor { avm_alu_b_hi_shift, avm_alu_b_lo_shift, avm_alu_cmp_rng_ctr_shift, + avm_alu_cmp_sel_shift, + avm_alu_op_add_shift, + avm_alu_op_mul_shift, + avm_alu_op_sub_shift, avm_alu_p_sub_a_hi_shift, avm_alu_p_sub_a_lo_shift, avm_alu_p_sub_b_hi_shift, avm_alu_p_sub_b_lo_shift, + avm_alu_rng_chk_lookup_selector_shift, avm_alu_rng_chk_sel_shift, avm_alu_u16_r0_shift, avm_alu_u16_r1_shift, @@ -1077,7 +1084,8 @@ class AvmFlavor { avm_alu_u16_r4_shift, avm_alu_u16_r5_shift, avm_alu_u16_r6_shift, - avm_alu_u16_r7_shift, + avm_alu_u8_r0_shift, + avm_alu_u8_r1_shift, avm_binary_acc_ia_shift, avm_binary_acc_ib_shift, avm_binary_acc_ic_shift, @@ -1146,7 +1154,6 @@ class AvmFlavor { avm_alu_u16_r9, avm_alu_u16_tag, avm_alu_u32_tag, - avm_alu_u64_r0, avm_alu_u64_tag, avm_alu_u8_r0, avm_alu_u8_r1, @@ -1307,26 +1314,39 @@ class AvmFlavor { }; RefVector get_to_be_shifted() { - return { avm_alu_a_hi, avm_alu_a_lo, avm_alu_b_hi, avm_alu_b_lo, - avm_alu_cmp_rng_ctr, avm_alu_p_sub_a_hi, avm_alu_p_sub_a_lo, avm_alu_p_sub_b_hi, - avm_alu_p_sub_b_lo, avm_alu_rng_chk_sel, avm_alu_u16_r0, avm_alu_u16_r1, - avm_alu_u16_r2, avm_alu_u16_r3, avm_alu_u16_r4, avm_alu_u16_r5, - avm_alu_u16_r6, avm_alu_u16_r7, avm_binary_acc_ia, avm_binary_acc_ib, - avm_binary_acc_ic, avm_binary_mem_tag_ctr, avm_binary_op_id, avm_main_internal_return_ptr, - avm_main_pc, avm_mem_addr, avm_mem_rw, avm_mem_tag, + return { avm_alu_a_hi, avm_alu_a_lo, + avm_alu_b_hi, avm_alu_b_lo, + avm_alu_cmp_rng_ctr, avm_alu_cmp_sel, + avm_alu_op_add, avm_alu_op_mul, + avm_alu_op_sub, avm_alu_p_sub_a_hi, + avm_alu_p_sub_a_lo, avm_alu_p_sub_b_hi, + avm_alu_p_sub_b_lo, avm_alu_rng_chk_lookup_selector, + avm_alu_rng_chk_sel, avm_alu_u16_r0, + avm_alu_u16_r1, avm_alu_u16_r2, + avm_alu_u16_r3, avm_alu_u16_r4, + avm_alu_u16_r5, avm_alu_u16_r6, + avm_alu_u8_r0, avm_alu_u8_r1, + avm_binary_acc_ia, avm_binary_acc_ib, + avm_binary_acc_ic, avm_binary_mem_tag_ctr, + avm_binary_op_id, avm_main_internal_return_ptr, + avm_main_pc, avm_mem_addr, + avm_mem_rw, avm_mem_tag, avm_mem_val }; }; RefVector get_shifted() { return { avm_alu_a_hi_shift, avm_alu_a_lo_shift, avm_alu_b_hi_shift, avm_alu_b_lo_shift, - avm_alu_cmp_rng_ctr_shift, avm_alu_p_sub_a_hi_shift, + avm_alu_cmp_rng_ctr_shift, avm_alu_cmp_sel_shift, + avm_alu_op_add_shift, avm_alu_op_mul_shift, + avm_alu_op_sub_shift, avm_alu_p_sub_a_hi_shift, avm_alu_p_sub_a_lo_shift, avm_alu_p_sub_b_hi_shift, - avm_alu_p_sub_b_lo_shift, avm_alu_rng_chk_sel_shift, - avm_alu_u16_r0_shift, avm_alu_u16_r1_shift, - avm_alu_u16_r2_shift, avm_alu_u16_r3_shift, - avm_alu_u16_r4_shift, avm_alu_u16_r5_shift, - avm_alu_u16_r6_shift, avm_alu_u16_r7_shift, + avm_alu_p_sub_b_lo_shift, avm_alu_rng_chk_lookup_selector_shift, + avm_alu_rng_chk_sel_shift, avm_alu_u16_r0_shift, + avm_alu_u16_r1_shift, avm_alu_u16_r2_shift, + avm_alu_u16_r3_shift, avm_alu_u16_r4_shift, + avm_alu_u16_r5_shift, avm_alu_u16_r6_shift, + avm_alu_u8_r0_shift, avm_alu_u8_r1_shift, avm_binary_acc_ia_shift, avm_binary_acc_ib_shift, avm_binary_acc_ic_shift, avm_binary_mem_tag_ctr_shift, avm_binary_op_id_shift, avm_main_internal_return_ptr_shift, @@ -1345,13 +1365,23 @@ class AvmFlavor { RefVector get_to_be_shifted() { - return { avm_alu_a_hi, avm_alu_a_lo, avm_alu_b_hi, avm_alu_b_lo, - avm_alu_cmp_rng_ctr, avm_alu_p_sub_a_hi, avm_alu_p_sub_a_lo, avm_alu_p_sub_b_hi, - avm_alu_p_sub_b_lo, avm_alu_rng_chk_sel, avm_alu_u16_r0, avm_alu_u16_r1, - avm_alu_u16_r2, avm_alu_u16_r3, avm_alu_u16_r4, avm_alu_u16_r5, - avm_alu_u16_r6, avm_alu_u16_r7, avm_binary_acc_ia, avm_binary_acc_ib, - avm_binary_acc_ic, avm_binary_mem_tag_ctr, avm_binary_op_id, avm_main_internal_return_ptr, - avm_main_pc, avm_mem_addr, avm_mem_rw, avm_mem_tag, + return { avm_alu_a_hi, avm_alu_a_lo, + avm_alu_b_hi, avm_alu_b_lo, + avm_alu_cmp_rng_ctr, avm_alu_cmp_sel, + avm_alu_op_add, avm_alu_op_mul, + avm_alu_op_sub, avm_alu_p_sub_a_hi, + avm_alu_p_sub_a_lo, avm_alu_p_sub_b_hi, + avm_alu_p_sub_b_lo, avm_alu_rng_chk_lookup_selector, + avm_alu_rng_chk_sel, avm_alu_u16_r0, + avm_alu_u16_r1, avm_alu_u16_r2, + avm_alu_u16_r3, avm_alu_u16_r4, + avm_alu_u16_r5, avm_alu_u16_r6, + avm_alu_u8_r0, avm_alu_u8_r1, + avm_binary_acc_ia, avm_binary_acc_ib, + avm_binary_acc_ic, avm_binary_mem_tag_ctr, + avm_binary_op_id, avm_main_internal_return_ptr, + avm_main_pc, avm_mem_addr, + avm_mem_rw, avm_mem_tag, avm_mem_val }; }; @@ -1567,7 +1597,6 @@ class AvmFlavor { Base::avm_alu_u16_r9 = "AVM_ALU_U16_R9"; Base::avm_alu_u16_tag = "AVM_ALU_U16_TAG"; Base::avm_alu_u32_tag = "AVM_ALU_U32_TAG"; - Base::avm_alu_u64_r0 = "AVM_ALU_U64_R0"; Base::avm_alu_u64_tag = "AVM_ALU_U64_TAG"; Base::avm_alu_u8_r0 = "AVM_ALU_U8_R0"; Base::avm_alu_u8_r1 = "AVM_ALU_U8_R1"; @@ -1796,7 +1825,6 @@ class AvmFlavor { Commitment avm_alu_u16_r9; Commitment avm_alu_u16_tag; Commitment avm_alu_u32_tag; - Commitment avm_alu_u64_r0; Commitment avm_alu_u64_tag; Commitment avm_alu_u8_r0; Commitment avm_alu_u8_r1; @@ -2025,7 +2053,6 @@ class AvmFlavor { avm_alu_u16_r9 = deserialize_from_buffer(Transcript::proof_data, num_frs_read); avm_alu_u16_tag = deserialize_from_buffer(Transcript::proof_data, num_frs_read); avm_alu_u32_tag = deserialize_from_buffer(Transcript::proof_data, num_frs_read); - avm_alu_u64_r0 = deserialize_from_buffer(Transcript::proof_data, num_frs_read); avm_alu_u64_tag = deserialize_from_buffer(Transcript::proof_data, num_frs_read); avm_alu_u8_r0 = deserialize_from_buffer(Transcript::proof_data, num_frs_read); avm_alu_u8_r1 = deserialize_from_buffer(Transcript::proof_data, num_frs_read); @@ -2259,7 +2286,6 @@ class AvmFlavor { serialize_to_buffer(avm_alu_u16_r9, Transcript::proof_data); serialize_to_buffer(avm_alu_u16_tag, Transcript::proof_data); serialize_to_buffer(avm_alu_u32_tag, Transcript::proof_data); - serialize_to_buffer(avm_alu_u64_r0, Transcript::proof_data); serialize_to_buffer(avm_alu_u64_tag, Transcript::proof_data); serialize_to_buffer(avm_alu_u8_r0, Transcript::proof_data); serialize_to_buffer(avm_alu_u8_r1, Transcript::proof_data); diff --git a/barretenberg/cpp/src/barretenberg/vm/generated/avm_prover.cpp b/barretenberg/cpp/src/barretenberg/vm/generated/avm_prover.cpp index f204511330f3..5c1cde785673 100644 --- a/barretenberg/cpp/src/barretenberg/vm/generated/avm_prover.cpp +++ b/barretenberg/cpp/src/barretenberg/vm/generated/avm_prover.cpp @@ -111,7 +111,6 @@ void AvmProver::execute_wire_commitments_round() witness_commitments.avm_alu_u16_r9 = commitment_key->commit(key->avm_alu_u16_r9); witness_commitments.avm_alu_u16_tag = commitment_key->commit(key->avm_alu_u16_tag); witness_commitments.avm_alu_u32_tag = commitment_key->commit(key->avm_alu_u32_tag); - witness_commitments.avm_alu_u64_r0 = commitment_key->commit(key->avm_alu_u64_r0); witness_commitments.avm_alu_u64_tag = commitment_key->commit(key->avm_alu_u64_tag); witness_commitments.avm_alu_u8_r0 = commitment_key->commit(key->avm_alu_u8_r0); witness_commitments.avm_alu_u8_r1 = commitment_key->commit(key->avm_alu_u8_r1); @@ -294,7 +293,6 @@ void AvmProver::execute_wire_commitments_round() transcript->send_to_verifier(commitment_labels.avm_alu_u16_r9, witness_commitments.avm_alu_u16_r9); transcript->send_to_verifier(commitment_labels.avm_alu_u16_tag, witness_commitments.avm_alu_u16_tag); transcript->send_to_verifier(commitment_labels.avm_alu_u32_tag, witness_commitments.avm_alu_u32_tag); - transcript->send_to_verifier(commitment_labels.avm_alu_u64_r0, witness_commitments.avm_alu_u64_r0); transcript->send_to_verifier(commitment_labels.avm_alu_u64_tag, witness_commitments.avm_alu_u64_tag); transcript->send_to_verifier(commitment_labels.avm_alu_u8_r0, witness_commitments.avm_alu_u8_r0); transcript->send_to_verifier(commitment_labels.avm_alu_u8_r1, witness_commitments.avm_alu_u8_r1); diff --git a/barretenberg/cpp/src/barretenberg/vm/generated/avm_verifier.cpp b/barretenberg/cpp/src/barretenberg/vm/generated/avm_verifier.cpp index e195267791bc..f1b9bb2e4cd2 100644 --- a/barretenberg/cpp/src/barretenberg/vm/generated/avm_verifier.cpp +++ b/barretenberg/cpp/src/barretenberg/vm/generated/avm_verifier.cpp @@ -123,7 +123,6 @@ bool AvmVerifier::verify_proof(const HonkProof& proof) transcript->template receive_from_prover(commitment_labels.avm_alu_u16_tag); commitments.avm_alu_u32_tag = transcript->template receive_from_prover(commitment_labels.avm_alu_u32_tag); - commitments.avm_alu_u64_r0 = transcript->template receive_from_prover(commitment_labels.avm_alu_u64_r0); commitments.avm_alu_u64_tag = transcript->template receive_from_prover(commitment_labels.avm_alu_u64_tag); commitments.avm_alu_u8_r0 = transcript->template receive_from_prover(commitment_labels.avm_alu_u8_r0); diff --git a/barretenberg/cpp/src/barretenberg/vm/tests/avm_arithmetic.test.cpp b/barretenberg/cpp/src/barretenberg/vm/tests/avm_arithmetic.test.cpp index d0dceddcb1ad..68fb123ad3c8 100644 --- a/barretenberg/cpp/src/barretenberg/vm/tests/avm_arithmetic.test.cpp +++ b/barretenberg/cpp/src/barretenberg/vm/tests/avm_arithmetic.test.cpp @@ -1495,17 +1495,19 @@ TEST_F(AvmArithmeticTestsU128, multiplication) EXPECT_EQ(alu_row_first.avm_alu_u128_tag, FF(1)); // Decomposition of the first operand in 16-bit registers - EXPECT_EQ(alu_row_first.avm_alu_u16_r0, FF(0x5FFB)); - EXPECT_EQ(alu_row_first.avm_alu_u16_r1, FF(0xBF68)); - EXPECT_EQ(alu_row_first.avm_alu_u16_r2, FF(0x8D64)); - EXPECT_EQ(alu_row_first.avm_alu_u16_r3, FF(0x3)); + EXPECT_EQ(alu_row_first.avm_alu_u8_r0, FF(0xFB)); + EXPECT_EQ(alu_row_first.avm_alu_u8_r1, FF(0x5F)); + EXPECT_EQ(alu_row_first.avm_alu_u16_r0, FF(0xBF68)); + EXPECT_EQ(alu_row_first.avm_alu_u16_r1, FF(0x8D64)); + EXPECT_EQ(alu_row_first.avm_alu_u16_r2, FF(0x3)); // Decomposition of the second operand in 16-bit registers auto alu_row_second = trace.at(alu_row_index + 1); - EXPECT_EQ(alu_row_second.avm_alu_u16_r0, FF(0x98DF)); - EXPECT_EQ(alu_row_second.avm_alu_u16_r1, FF(0x762C)); - EXPECT_EQ(alu_row_second.avm_alu_u16_r2, FF(0xF92C)); - EXPECT_EQ(alu_row_second.avm_alu_u16_r3, FF(0x1)); + EXPECT_EQ(alu_row_second.avm_alu_u8_r0, FF(0xDF)); + EXPECT_EQ(alu_row_second.avm_alu_u8_r1, FF(0x98)); + EXPECT_EQ(alu_row_second.avm_alu_u16_r0, FF(0x762C)); + EXPECT_EQ(alu_row_second.avm_alu_u16_r1, FF(0xF92C)); + EXPECT_EQ(alu_row_second.avm_alu_u16_r2, FF(0x1)); validate_trace(std::move(trace)); } @@ -1538,32 +1540,40 @@ TEST_F(AvmArithmeticTestsU128, multiplicationOverflow) EXPECT_EQ(alu_row_first.avm_alu_u128_tag, FF(1)); // Decomposition of the first operand in 16-bit registers - EXPECT_EQ(alu_row_first.avm_alu_u16_r0, FF(0xFFFE)); + EXPECT_EQ(alu_row_first.avm_alu_u8_r0, FF(0xFE)); + EXPECT_EQ(alu_row_first.avm_alu_u8_r1, FF(0xFF)); + EXPECT_EQ(alu_row_first.avm_alu_u16_r0, FF(UINT16_MAX)); EXPECT_EQ(alu_row_first.avm_alu_u16_r1, FF(UINT16_MAX)); EXPECT_EQ(alu_row_first.avm_alu_u16_r2, FF(UINT16_MAX)); EXPECT_EQ(alu_row_first.avm_alu_u16_r3, FF(UINT16_MAX)); EXPECT_EQ(alu_row_first.avm_alu_u16_r4, FF(UINT16_MAX)); EXPECT_EQ(alu_row_first.avm_alu_u16_r5, FF(UINT16_MAX)); EXPECT_EQ(alu_row_first.avm_alu_u16_r6, FF(UINT16_MAX)); - EXPECT_EQ(alu_row_first.avm_alu_u16_r7, FF(UINT16_MAX)); // Decomposition of the second operand in 16-bit registers auto alu_row_second = trace.at(alu_row_index + 1); - EXPECT_EQ(alu_row_second.avm_alu_u16_r0, FF(0xFFFC)); + EXPECT_EQ(alu_row_second.avm_alu_u8_r0, FF(0xFC)); + EXPECT_EQ(alu_row_second.avm_alu_u8_r1, FF(0xFF)); + EXPECT_EQ(alu_row_second.avm_alu_u16_r0, FF(UINT16_MAX)); EXPECT_EQ(alu_row_second.avm_alu_u16_r1, FF(UINT16_MAX)); EXPECT_EQ(alu_row_second.avm_alu_u16_r2, FF(UINT16_MAX)); EXPECT_EQ(alu_row_second.avm_alu_u16_r3, FF(UINT16_MAX)); EXPECT_EQ(alu_row_second.avm_alu_u16_r4, FF(UINT16_MAX)); EXPECT_EQ(alu_row_second.avm_alu_u16_r5, FF(UINT16_MAX)); EXPECT_EQ(alu_row_second.avm_alu_u16_r6, FF(UINT16_MAX)); - EXPECT_EQ(alu_row_second.avm_alu_u16_r7, FF(UINT16_MAX)); // Other registers involved in the relevant relations - // PIL relation (avm_alu.pil): a * b_l + a_l * b_h * 2^64 = (CF * 2^64 + R') * 2^128 + c + // PIL relation (avm_alu.pil): a * b_l + a_l * b_h * 2^64 = (CF * 2^64 + R_64) * 2^128 + c // (2^128 - 2) * (2^64 - 4) + (2^64 - 2) * (2^64 - 1) * 2^64 = // 2 * 2^192 + (- 4 - 2 - 1) * 2^128 + (-2 + 2) * 2^64 + 8 = (2^65 - 7) * 2^128 + 8 - // Therefore, CF = 1 and R' = 2^64 - 7 - EXPECT_EQ(alu_row_first.avm_alu_u64_r0, FF{ UINT64_MAX - 6 }); // 2^64 - 7 + // Therefore, CF = 1 and R_64 = 2^64 - 7 + + // R_64 is decomposed over the 4 following 16-bit registers + EXPECT_EQ(alu_row_first.avm_alu_u16_r7, FF(UINT16_MAX - 6)); + EXPECT_EQ(alu_row_first.avm_alu_u16_r8, FF(UINT16_MAX)); + EXPECT_EQ(alu_row_first.avm_alu_u16_r9, FF(UINT16_MAX)); + EXPECT_EQ(alu_row_first.avm_alu_u16_r10, FF(UINT16_MAX)); + // CF EXPECT_EQ(alu_row_first.avm_alu_cf, FF(1)); validate_trace(std::move(trace)); diff --git a/barretenberg/cpp/src/barretenberg/vm/tests/avm_comparison.test.cpp b/barretenberg/cpp/src/barretenberg/vm/tests/avm_comparison.test.cpp index 3ba7361e7d9c..16ea72cbcaf6 100644 --- a/barretenberg/cpp/src/barretenberg/vm/tests/avm_comparison.test.cpp +++ b/barretenberg/cpp/src/barretenberg/vm/tests/avm_comparison.test.cpp @@ -226,6 +226,7 @@ std::vector gen_mutated_trace_cmp( break; case CounterNonZeroCheckFailed: range_check_row->avm_alu_rng_chk_sel = FF(0); + range_check_row->avm_alu_rng_chk_lookup_selector = FF(0); break; case ShiftRelationFailed: range_check_row->avm_alu_a_lo = range_check_row->avm_alu_res_lo; diff --git a/barretenberg/cpp/src/barretenberg/vm/tests/avm_inter_table.test.cpp b/barretenberg/cpp/src/barretenberg/vm/tests/avm_inter_table.test.cpp index 3e4e6a1a69cf..caf1b1855346 100644 --- a/barretenberg/cpp/src/barretenberg/vm/tests/avm_inter_table.test.cpp +++ b/barretenberg/cpp/src/barretenberg/vm/tests/avm_inter_table.test.cpp @@ -167,6 +167,7 @@ TEST_F(AvmPermMainAluNegativeTests, removeAluSelector) { trace.at(alu_idx).avm_alu_alu_sel = 0; trace.at(alu_idx).avm_alu_op_mul = 0; + trace.at(alu_idx).avm_alu_rng_chk_lookup_selector = 0; EXPECT_THROW_WITH_MESSAGE(validate_trace_check_circuit(std::move(trace)), "PERM_MAIN_ALU"); }