From fc941818f6d28443f83792ef9f60808bad8a5530 Mon Sep 17 00:00:00 2001 From: jeanmon Date: Wed, 27 Mar 2024 10:23:23 +0000 Subject: [PATCH 1/8] 5466 - introduce in_tag dispatching to the ALU --- barretenberg/cpp/pil/avm/avm_main.pil | 32 ++- .../relations/generated/avm/avm_main.hpp | 261 ++++++------------ .../relations/generated/avm/declare_views.hpp | 2 + .../relations/generated/avm/perm_main_alu.hpp | 8 + .../barretenberg/vm/avm_trace/avm_trace.cpp | 5 + .../vm/generated/avm_circuit_builder.hpp | 9 + .../barretenberg/vm/generated/avm_flavor.hpp | 26 ++ .../vm/generated/avm_verifier.cpp | 4 + 8 files changed, 154 insertions(+), 193 deletions(-) diff --git a/barretenberg/cpp/pil/avm/avm_main.pil b/barretenberg/cpp/pil/avm/avm_main.pil index ecc18fe6d83..8e32589b75e 100644 --- a/barretenberg/cpp/pil/avm/avm_main.pil +++ b/barretenberg/cpp/pil/avm/avm_main.pil @@ -54,6 +54,8 @@ namespace avm_main(256); pol commit sel_op_or; // XOR pol commit sel_op_xor; + // CAST + pol commit sel_op_cast; // LT pol commit sel_op_lt; // LTE @@ -68,6 +70,7 @@ namespace avm_main(256); // Instruction memory tags read/write (1: u8, 2: u16, 3: u32, 4: u64, 5: u128, 6: field) pol commit r_in_tag; pol commit w_in_tag; + pol commit alu_in_tag; // Copy of r_in_tag or w_in_tag depending of the operation. It is sent to ALU trace. // Errors pol commit op_err; // Boolean flag pertaining to an operation error @@ -121,7 +124,8 @@ namespace avm_main(256); pol commit last; // Relations on type constraints - + // TODO: Very likely, we can remove these constraints as the selectors should be derived during + // opcode decomposition. sel_op_add * (1 - sel_op_add) = 0; sel_op_sub * (1 - sel_op_sub) = 0; sel_op_mul * (1 - sel_op_mul) = 0; @@ -131,6 +135,7 @@ namespace avm_main(256); sel_op_and * (1 - sel_op_and) = 0; sel_op_or * (1 - sel_op_or) = 0; sel_op_xor * (1 - sel_op_xor) = 0; + sel_op_cast * (1 - sel_op_cast) = 0; sel_op_lt * (1 - sel_op_lt) = 0; sel_op_lte * (1 - sel_op_lte) = 0; @@ -243,7 +248,8 @@ namespace avm_main(256); //===== CONTROL_FLOW_CONSISTENCY ============================================ pol INTERNAL_CALL_STACK_SELECTORS = (first + sel_internal_call + sel_internal_return + sel_halt); - pol OPCODE_SELECTORS = (sel_op_add + sel_op_sub + sel_op_div + sel_op_mul + sel_op_not + sel_op_eq + sel_op_and + sel_op_or + sel_op_xor); + pol OPCODE_SELECTORS = (sel_op_add + sel_op_sub + sel_op_div + sel_op_mul + sel_op_not + + sel_op_eq + sel_op_and + sel_op_or + sel_op_xor + sel_op_cast); // Program counter must increment if not jumping or returning #[PC_INCREMENT] @@ -287,6 +293,20 @@ namespace avm_main(256); #[MOV_MAIN_SAME_TAG] (sel_mov + sel_cmov) * (r_in_tag - w_in_tag) = 0; + //===== ALU CONSTRAINTS ===================================================== + // TODO: when division is moved to the alu, we will need to add the selector in the list below. + pol ALU_R_TAG_SEL = sel_op_add + sel_op_sub + sel_op_mul + sel_op_not + sel_op_eq + sel_op_lt + sel_op_lte; + pol ALU_W_TAG_SEL = sel_op_cast; + pol ALU_ALL_SEL = ALU_R_TAG_SEL + ALU_W_TAG_SEL; + + // Predicate to activate the copy of intermediate registers to ALU table. If tag_err == 1, + // the operation is not copied to the ALU table. + alu_sel = ALU_ALL_SEL * (1 - tag_err); + + // Dispatch the correct in_tag for alu + ALU_R_TAG_SEL * (alu_in_tag - r_in_tag) = 0; + ALU_W_TAG_SEL * (alu_in_tag - w_in_tag) = 0; + //====== Inter-table Constraints ============================================ #[INCL_MAIN_TAG_ERR] avm_mem.tag_err {avm_mem.clk} in tag_err {clk}; @@ -294,18 +314,12 @@ namespace avm_main(256); #[INCL_MEM_TAG_ERR] tag_err {clk} in avm_mem.tag_err {avm_mem.clk}; - // Predicate to activate the copy of intermediate registers to ALU table. If tag_err == 1, - // the operation is not copied to the ALU table. - // TODO: when division is moved to the alu, we will need to add the selector in the list below: - alu_sel = (sel_op_add + sel_op_sub + sel_op_mul + sel_op_not + sel_op_eq + sel_op_lt + sel_op_lte) * (1 - tag_err); - #[PERM_MAIN_ALU] alu_sel {clk, ia, ib, ic, sel_op_add, sel_op_sub, - sel_op_mul, sel_op_eq, sel_op_not, sel_op_lt, sel_op_lte, r_in_tag} + sel_op_mul, sel_op_eq, sel_op_not, sel_op_lt, sel_op_lte, alu_in_tag} is avm_alu.alu_sel {avm_alu.clk, avm_alu.ia, avm_alu.ib, avm_alu.ic, avm_alu.op_add, avm_alu.op_sub, avm_alu.op_mul, avm_alu.op_eq, avm_alu.op_not, avm_alu.op_lt, avm_alu.op_lte, avm_alu.in_tag}; - // Based on the boolean selectors, we derive the binary op id to lookup in the table; // TODO: Check if having 4 columns (op_id + 3 boolean selectors) is more optimal that just using the op_id // but with a higher degree constraint: op_id * (op_id - 1) * (op_id - 2) diff --git a/barretenberg/cpp/src/barretenberg/relations/generated/avm/avm_main.hpp b/barretenberg/cpp/src/barretenberg/relations/generated/avm/avm_main.hpp index 74e611ac699..8c88b757773 100644 --- a/barretenberg/cpp/src/barretenberg/relations/generated/avm/avm_main.hpp +++ b/barretenberg/cpp/src/barretenberg/relations/generated/avm/avm_main.hpp @@ -7,6 +7,7 @@ namespace bb::Avm_vm { template struct Avm_mainRow { + FF avm_main_alu_in_tag{}; FF avm_main_alu_sel{}; FF avm_main_bin_op_id{}; FF avm_main_bin_sel{}; @@ -47,6 +48,7 @@ template struct Avm_mainRow { FF avm_main_sel_mov_b{}; FF avm_main_sel_op_add{}; FF avm_main_sel_op_and{}; + FF avm_main_sel_op_cast{}; FF avm_main_sel_op_div{}; FF avm_main_sel_op_eq{}; FF avm_main_sel_op_lt{}; @@ -63,52 +65,43 @@ template struct Avm_mainRow { inline std::string get_relation_label_avm_main(int index) { switch (index) { - case 32: - return "OUTPUT_U8"; + case 25: + return "EQ_OUTPUT_U8"; - case 33: + case 26: return "SUBOP_DIVISION_FF"; - case 34: + case 27: return "SUBOP_DIVISION_ZERO_ERR1"; - case 35: + case 28: return "SUBOP_DIVISION_ZERO_ERR2"; - case 36: + case 29: return "SUBOP_ERROR_RELEVANT_OP"; - case 38: + case 31: return "RETURN_POINTER_INCREMENT"; - case 44: + case 37: return "RETURN_POINTER_DECREMENT"; - case 49: + case 42: return "PC_INCREMENT"; - case 50: + case 43: return "INTERNAL_RETURN_POINTER_CONSISTENCY"; - case 51: - return "CMOV_CONDITION_RES_1"; - - case 52: - return "CMOV_CONDITION_RES_2"; - - case 55: - return "MOV_SAME_VALUE_A"; - - case 56: - return "MOV_SAME_VALUE_B"; + case 44: + return "MOV_SAME_VALUE"; - case 57: + case 45: return "MOV_MAIN_SAME_TAG"; - case 59: + case 47: return "BIN_SEL_1"; - case 60: + case 48: return "BIN_SEL_2"; } return std::to_string(index); @@ -118,9 +111,9 @@ template class avm_mainImpl { public: using FF = FF_; - static constexpr std::array SUBRELATION_PARTIAL_LENGTHS{ - 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, - 3, 3, 5, 4, 4, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 5, 3, 4, 4, 3, 3, 3, 3, 3, 3, 3, 2, + static constexpr std::array SUBRELATION_PARTIAL_LENGTHS{ + 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, + 3, 5, 4, 4, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 5, 3, 3, 3, 3, 3, 2, }; template @@ -206,7 +199,7 @@ template class avm_mainImpl { { Avm_DECLARE_VIEWS(9); - auto tmp = (avm_main_sel_op_lt * (-avm_main_sel_op_lt + FF(1))); + auto tmp = (avm_main_sel_internal_call * (-avm_main_sel_internal_call + FF(1))); tmp *= scaling_factor; std::get<9>(evals) += tmp; } @@ -214,7 +207,7 @@ template class avm_mainImpl { { Avm_DECLARE_VIEWS(10); - auto tmp = (avm_main_sel_op_lte * (-avm_main_sel_op_lte + FF(1))); + auto tmp = (avm_main_sel_internal_return * (-avm_main_sel_internal_return + FF(1))); tmp *= scaling_factor; std::get<10>(evals) += tmp; } @@ -222,7 +215,7 @@ template class avm_mainImpl { { Avm_DECLARE_VIEWS(11); - auto tmp = (avm_main_sel_internal_call * (-avm_main_sel_internal_call + FF(1))); + auto tmp = (avm_main_sel_jump * (-avm_main_sel_jump + FF(1))); tmp *= scaling_factor; std::get<11>(evals) += tmp; } @@ -230,7 +223,7 @@ template class avm_mainImpl { { Avm_DECLARE_VIEWS(12); - auto tmp = (avm_main_sel_internal_return * (-avm_main_sel_internal_return + FF(1))); + auto tmp = (avm_main_sel_halt * (-avm_main_sel_halt + FF(1))); tmp *= scaling_factor; std::get<12>(evals) += tmp; } @@ -238,7 +231,7 @@ template class avm_mainImpl { { Avm_DECLARE_VIEWS(13); - auto tmp = (avm_main_sel_jump * (-avm_main_sel_jump + FF(1))); + auto tmp = (avm_main_sel_mov * (-avm_main_sel_mov + FF(1))); tmp *= scaling_factor; std::get<13>(evals) += tmp; } @@ -246,7 +239,7 @@ template class avm_mainImpl { { Avm_DECLARE_VIEWS(14); - auto tmp = (avm_main_sel_halt * (-avm_main_sel_halt + FF(1))); + auto tmp = (avm_main_op_err * (-avm_main_op_err + FF(1))); tmp *= scaling_factor; std::get<14>(evals) += tmp; } @@ -254,7 +247,7 @@ template class avm_mainImpl { { Avm_DECLARE_VIEWS(15); - auto tmp = (avm_main_sel_mov * (-avm_main_sel_mov + FF(1))); + auto tmp = (avm_main_tag_err * (-avm_main_tag_err + FF(1))); tmp *= scaling_factor; std::get<15>(evals) += tmp; } @@ -262,7 +255,7 @@ template class avm_mainImpl { { Avm_DECLARE_VIEWS(16); - auto tmp = (avm_main_sel_cmov * (-avm_main_sel_cmov + FF(1))); + auto tmp = (avm_main_mem_op_a * (-avm_main_mem_op_a + FF(1))); tmp *= scaling_factor; std::get<16>(evals) += tmp; } @@ -270,7 +263,7 @@ template class avm_mainImpl { { Avm_DECLARE_VIEWS(17); - auto tmp = (avm_main_op_err * (-avm_main_op_err + FF(1))); + auto tmp = (avm_main_mem_op_b * (-avm_main_mem_op_b + FF(1))); tmp *= scaling_factor; std::get<17>(evals) += tmp; } @@ -278,7 +271,7 @@ template class avm_mainImpl { { Avm_DECLARE_VIEWS(18); - auto tmp = (avm_main_tag_err * (-avm_main_tag_err + FF(1))); + auto tmp = (avm_main_mem_op_c * (-avm_main_mem_op_c + FF(1))); tmp *= scaling_factor; std::get<18>(evals) += tmp; } @@ -286,7 +279,7 @@ template class avm_mainImpl { { Avm_DECLARE_VIEWS(19); - auto tmp = (avm_main_id_zero * (-avm_main_id_zero + FF(1))); + auto tmp = (avm_main_rwa * (-avm_main_rwa + FF(1))); tmp *= scaling_factor; std::get<19>(evals) += tmp; } @@ -294,7 +287,7 @@ template class avm_mainImpl { { Avm_DECLARE_VIEWS(20); - auto tmp = (avm_main_mem_op_a * (-avm_main_mem_op_a + FF(1))); + auto tmp = (avm_main_rwb * (-avm_main_rwb + FF(1))); tmp *= scaling_factor; std::get<20>(evals) += tmp; } @@ -302,7 +295,7 @@ template class avm_mainImpl { { Avm_DECLARE_VIEWS(21); - auto tmp = (avm_main_mem_op_b * (-avm_main_mem_op_b + FF(1))); + auto tmp = (avm_main_rwc * (-avm_main_rwc + FF(1))); tmp *= scaling_factor; std::get<21>(evals) += tmp; } @@ -310,7 +303,7 @@ template class avm_mainImpl { { Avm_DECLARE_VIEWS(22); - auto tmp = (avm_main_mem_op_c * (-avm_main_mem_op_c + FF(1))); + auto tmp = (avm_main_ind_op_a * (-avm_main_ind_op_a + FF(1))); tmp *= scaling_factor; std::get<22>(evals) += tmp; } @@ -318,7 +311,7 @@ template class avm_mainImpl { { Avm_DECLARE_VIEWS(23); - auto tmp = (avm_main_mem_op_d * (-avm_main_mem_op_d + FF(1))); + auto tmp = (avm_main_ind_op_b * (-avm_main_ind_op_b + FF(1))); tmp *= scaling_factor; std::get<23>(evals) += tmp; } @@ -326,7 +319,7 @@ template class avm_mainImpl { { Avm_DECLARE_VIEWS(24); - auto tmp = (avm_main_rwa * (-avm_main_rwa + FF(1))); + auto tmp = (avm_main_ind_op_c * (-avm_main_ind_op_c + FF(1))); tmp *= scaling_factor; std::get<24>(evals) += tmp; } @@ -334,7 +327,7 @@ template class avm_mainImpl { { Avm_DECLARE_VIEWS(25); - auto tmp = (avm_main_rwb * (-avm_main_rwb + FF(1))); + auto tmp = (avm_main_sel_op_eq * (avm_main_w_in_tag - FF(1))); tmp *= scaling_factor; std::get<25>(evals) += tmp; } @@ -342,7 +335,8 @@ template class avm_mainImpl { { Avm_DECLARE_VIEWS(26); - auto tmp = (avm_main_rwc * (-avm_main_rwc + FF(1))); + auto tmp = + ((avm_main_sel_op_div * (-avm_main_op_err + FF(1))) * ((avm_main_ic * avm_main_ib) - avm_main_ia)); tmp *= scaling_factor; std::get<26>(evals) += tmp; } @@ -350,7 +344,7 @@ template class avm_mainImpl { { Avm_DECLARE_VIEWS(27); - auto tmp = (avm_main_rwd * (-avm_main_rwd + FF(1))); + auto tmp = (avm_main_sel_op_div * (((avm_main_ib * avm_main_inv) - FF(1)) + avm_main_op_err)); tmp *= scaling_factor; std::get<27>(evals) += tmp; } @@ -358,7 +352,7 @@ template class avm_mainImpl { { Avm_DECLARE_VIEWS(28); - auto tmp = (avm_main_ind_op_a * (-avm_main_ind_op_a + FF(1))); + auto tmp = ((avm_main_sel_op_div * avm_main_op_err) * (-avm_main_inv + FF(1))); tmp *= scaling_factor; std::get<28>(evals) += tmp; } @@ -366,7 +360,7 @@ template class avm_mainImpl { { Avm_DECLARE_VIEWS(29); - auto tmp = (avm_main_ind_op_b * (-avm_main_ind_op_b + FF(1))); + auto tmp = (avm_main_op_err * (avm_main_sel_op_div - FF(1))); tmp *= scaling_factor; std::get<29>(evals) += tmp; } @@ -374,7 +368,7 @@ template class avm_mainImpl { { Avm_DECLARE_VIEWS(30); - auto tmp = (avm_main_ind_op_c * (-avm_main_ind_op_c + FF(1))); + auto tmp = (avm_main_sel_jump * (avm_main_pc_shift - avm_main_ia)); tmp *= scaling_factor; std::get<30>(evals) += tmp; } @@ -382,7 +376,8 @@ template class avm_mainImpl { { Avm_DECLARE_VIEWS(31); - auto tmp = (avm_main_ind_op_d * (-avm_main_ind_op_d + FF(1))); + auto tmp = (avm_main_sel_internal_call * + (avm_main_internal_return_ptr_shift - (avm_main_internal_return_ptr + FF(1)))); tmp *= scaling_factor; std::get<31>(evals) += tmp; } @@ -390,8 +385,7 @@ template class avm_mainImpl { { Avm_DECLARE_VIEWS(32); - auto tmp = - (((avm_main_sel_op_eq + avm_main_sel_op_lte) + avm_main_sel_op_lt) * (avm_main_w_in_tag - FF(1))); + auto tmp = (avm_main_sel_internal_call * (avm_main_internal_return_ptr - avm_main_mem_idx_b)); tmp *= scaling_factor; std::get<32>(evals) += tmp; } @@ -399,8 +393,7 @@ template class avm_mainImpl { { Avm_DECLARE_VIEWS(33); - auto tmp = - ((avm_main_sel_op_div * (-avm_main_op_err + FF(1))) * ((avm_main_ic * avm_main_ib) - avm_main_ia)); + auto tmp = (avm_main_sel_internal_call * (avm_main_pc_shift - avm_main_ia)); tmp *= scaling_factor; std::get<33>(evals) += tmp; } @@ -408,7 +401,7 @@ template class avm_mainImpl { { Avm_DECLARE_VIEWS(34); - auto tmp = (avm_main_sel_op_div * (((avm_main_ib * avm_main_inv) - FF(1)) + avm_main_op_err)); + auto tmp = (avm_main_sel_internal_call * ((avm_main_pc + FF(1)) - avm_main_ib)); tmp *= scaling_factor; std::get<34>(evals) += tmp; } @@ -416,7 +409,7 @@ template class avm_mainImpl { { Avm_DECLARE_VIEWS(35); - auto tmp = ((avm_main_sel_op_div * avm_main_op_err) * (-avm_main_inv + FF(1))); + auto tmp = (avm_main_sel_internal_call * (avm_main_rwb - FF(1))); tmp *= scaling_factor; std::get<35>(evals) += tmp; } @@ -424,7 +417,7 @@ template class avm_mainImpl { { Avm_DECLARE_VIEWS(36); - auto tmp = (avm_main_op_err * (avm_main_sel_op_div - FF(1))); + auto tmp = (avm_main_sel_internal_call * (avm_main_mem_op_b - FF(1))); tmp *= scaling_factor; std::get<36>(evals) += tmp; } @@ -432,7 +425,8 @@ template class avm_mainImpl { { Avm_DECLARE_VIEWS(37); - auto tmp = (avm_main_sel_jump * (avm_main_pc_shift - avm_main_ia)); + auto tmp = (avm_main_sel_internal_return * + (avm_main_internal_return_ptr_shift - (avm_main_internal_return_ptr - FF(1)))); tmp *= scaling_factor; std::get<37>(evals) += tmp; } @@ -440,8 +434,7 @@ template class avm_mainImpl { { Avm_DECLARE_VIEWS(38); - auto tmp = (avm_main_sel_internal_call * - (avm_main_internal_return_ptr_shift - (avm_main_internal_return_ptr + FF(1)))); + auto tmp = (avm_main_sel_internal_return * ((avm_main_internal_return_ptr - FF(1)) - avm_main_mem_idx_a)); tmp *= scaling_factor; std::get<38>(evals) += tmp; } @@ -449,7 +442,7 @@ template class avm_mainImpl { { Avm_DECLARE_VIEWS(39); - auto tmp = (avm_main_sel_internal_call * (avm_main_internal_return_ptr - avm_main_mem_idx_b)); + auto tmp = (avm_main_sel_internal_return * (avm_main_pc_shift - avm_main_ia)); tmp *= scaling_factor; std::get<39>(evals) += tmp; } @@ -457,7 +450,7 @@ template class avm_mainImpl { { Avm_DECLARE_VIEWS(40); - auto tmp = (avm_main_sel_internal_call * (avm_main_pc_shift - avm_main_ia)); + auto tmp = (avm_main_sel_internal_return * avm_main_rwa); tmp *= scaling_factor; std::get<40>(evals) += tmp; } @@ -465,7 +458,7 @@ template class avm_mainImpl { { Avm_DECLARE_VIEWS(41); - auto tmp = (avm_main_sel_internal_call * ((avm_main_pc + FF(1)) - avm_main_ib)); + auto tmp = (avm_main_sel_internal_return * (avm_main_mem_op_a - FF(1))); tmp *= scaling_factor; std::get<41>(evals) += tmp; } @@ -473,7 +466,15 @@ template class avm_mainImpl { { Avm_DECLARE_VIEWS(42); - auto tmp = (avm_main_sel_internal_call * (avm_main_rwb - FF(1))); + auto tmp = + ((((-avm_main_first + FF(1)) * (-avm_main_sel_halt + FF(1))) * + ((((((((avm_main_sel_op_add + avm_main_sel_op_sub) + avm_main_sel_op_div) + avm_main_sel_op_mul) + + avm_main_sel_op_not) + + avm_main_sel_op_eq) + + avm_main_sel_op_and) + + avm_main_sel_op_or) + + avm_main_sel_op_xor)) * + (avm_main_pc_shift - (avm_main_pc + FF(1)))); tmp *= scaling_factor; std::get<42>(evals) += tmp; } @@ -481,7 +482,10 @@ template class avm_mainImpl { { Avm_DECLARE_VIEWS(43); - auto tmp = (avm_main_sel_internal_call * (avm_main_mem_op_b - FF(1))); + auto tmp = ((-(((avm_main_first + avm_main_sel_internal_call) + avm_main_sel_internal_return) + + avm_main_sel_halt) + + FF(1)) * + (avm_main_internal_return_ptr_shift - avm_main_internal_return_ptr)); tmp *= scaling_factor; std::get<43>(evals) += tmp; } @@ -489,8 +493,7 @@ template class avm_mainImpl { { Avm_DECLARE_VIEWS(44); - auto tmp = (avm_main_sel_internal_return * - (avm_main_internal_return_ptr_shift - (avm_main_internal_return_ptr - FF(1)))); + auto tmp = (avm_main_sel_mov * (avm_main_ia - avm_main_ic)); tmp *= scaling_factor; std::get<44>(evals) += tmp; } @@ -498,7 +501,7 @@ template class avm_mainImpl { { Avm_DECLARE_VIEWS(45); - auto tmp = (avm_main_sel_internal_return * ((avm_main_internal_return_ptr - FF(1)) - avm_main_mem_idx_a)); + auto tmp = (avm_main_sel_mov * (avm_main_r_in_tag - avm_main_w_in_tag)); tmp *= scaling_factor; std::get<45>(evals) += tmp; } @@ -506,7 +509,10 @@ template class avm_mainImpl { { Avm_DECLARE_VIEWS(46); - auto tmp = (avm_main_sel_internal_return * (avm_main_pc_shift - avm_main_ia)); + auto tmp = (avm_main_alu_sel - + (((((avm_main_sel_op_add + avm_main_sel_op_sub) + avm_main_sel_op_mul) + avm_main_sel_op_not) + + avm_main_sel_op_eq) * + (-avm_main_tag_err + FF(1)))); tmp *= scaling_factor; std::get<46>(evals) += tmp; } @@ -514,7 +520,7 @@ template class avm_mainImpl { { Avm_DECLARE_VIEWS(47); - auto tmp = (avm_main_sel_internal_return * avm_main_rwa); + auto tmp = (avm_main_bin_op_id - (avm_main_sel_op_or + (avm_main_sel_op_xor * FF(2)))); tmp *= scaling_factor; std::get<47>(evals) += tmp; } @@ -522,122 +528,9 @@ template class avm_mainImpl { { Avm_DECLARE_VIEWS(48); - auto tmp = (avm_main_sel_internal_return * (avm_main_mem_op_a - FF(1))); - tmp *= scaling_factor; - std::get<48>(evals) += tmp; - } - // Contribution 49 - { - Avm_DECLARE_VIEWS(49); - - auto tmp = - ((((-avm_main_first + FF(1)) * (-avm_main_sel_halt + FF(1))) * - ((((((((avm_main_sel_op_add + avm_main_sel_op_sub) + avm_main_sel_op_div) + avm_main_sel_op_mul) + - avm_main_sel_op_not) + - avm_main_sel_op_eq) + - avm_main_sel_op_and) + - avm_main_sel_op_or) + - avm_main_sel_op_xor)) * - (avm_main_pc_shift - (avm_main_pc + FF(1)))); - tmp *= scaling_factor; - std::get<49>(evals) += tmp; - } - // Contribution 50 - { - Avm_DECLARE_VIEWS(50); - - auto tmp = ((-(((avm_main_first + avm_main_sel_internal_call) + avm_main_sel_internal_return) + - avm_main_sel_halt) + - FF(1)) * - (avm_main_internal_return_ptr_shift - avm_main_internal_return_ptr)); - tmp *= scaling_factor; - std::get<50>(evals) += tmp; - } - // Contribution 51 - { - Avm_DECLARE_VIEWS(51); - - auto tmp = (avm_main_sel_cmov * (((avm_main_id * avm_main_inv) - FF(1)) + avm_main_id_zero)); - tmp *= scaling_factor; - std::get<51>(evals) += tmp; - } - // Contribution 52 - { - Avm_DECLARE_VIEWS(52); - - auto tmp = ((avm_main_sel_cmov * avm_main_id_zero) * (-avm_main_inv + FF(1))); - tmp *= scaling_factor; - std::get<52>(evals) += tmp; - } - // Contribution 53 - { - Avm_DECLARE_VIEWS(53); - - auto tmp = (avm_main_sel_mov_a - (avm_main_sel_mov + (avm_main_sel_cmov * (-avm_main_id_zero + FF(1))))); - tmp *= scaling_factor; - std::get<53>(evals) += tmp; - } - // Contribution 54 - { - Avm_DECLARE_VIEWS(54); - - auto tmp = (avm_main_sel_mov_b - (avm_main_sel_cmov * avm_main_id_zero)); - tmp *= scaling_factor; - std::get<54>(evals) += tmp; - } - // Contribution 55 - { - Avm_DECLARE_VIEWS(55); - - auto tmp = (avm_main_sel_mov_a * (avm_main_ia - avm_main_ic)); - tmp *= scaling_factor; - std::get<55>(evals) += tmp; - } - // Contribution 56 - { - Avm_DECLARE_VIEWS(56); - - auto tmp = (avm_main_sel_mov_b * (avm_main_ib - avm_main_ic)); - tmp *= scaling_factor; - std::get<56>(evals) += tmp; - } - // Contribution 57 - { - Avm_DECLARE_VIEWS(57); - - auto tmp = ((avm_main_sel_mov + avm_main_sel_cmov) * (avm_main_r_in_tag - avm_main_w_in_tag)); - tmp *= scaling_factor; - std::get<57>(evals) += tmp; - } - // Contribution 58 - { - Avm_DECLARE_VIEWS(58); - - auto tmp = - (avm_main_alu_sel - - (((((((avm_main_sel_op_add + avm_main_sel_op_sub) + avm_main_sel_op_mul) + avm_main_sel_op_not) + - avm_main_sel_op_eq) + - avm_main_sel_op_lt) + - avm_main_sel_op_lte) * - (-avm_main_tag_err + FF(1)))); - tmp *= scaling_factor; - std::get<58>(evals) += tmp; - } - // Contribution 59 - { - Avm_DECLARE_VIEWS(59); - - auto tmp = (avm_main_bin_op_id - (avm_main_sel_op_or + (avm_main_sel_op_xor * FF(2)))); - tmp *= scaling_factor; - std::get<59>(evals) += tmp; - } - // Contribution 60 - { - Avm_DECLARE_VIEWS(60); - auto tmp = (avm_main_bin_sel - ((avm_main_sel_op_and + avm_main_sel_op_or) + avm_main_sel_op_xor)); tmp *= scaling_factor; - std::get<60>(evals) += tmp; + 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 05c47520ab4..8e10193b537 100644 --- a/barretenberg/cpp/src/barretenberg/relations/generated/avm/declare_views.hpp +++ b/barretenberg/cpp/src/barretenberg/relations/generated/avm/declare_views.hpp @@ -80,6 +80,7 @@ [[maybe_unused]] auto avm_byte_lookup_table_input_b = View(new_term.avm_byte_lookup_table_input_b); \ [[maybe_unused]] auto avm_byte_lookup_table_op_id = View(new_term.avm_byte_lookup_table_op_id); \ [[maybe_unused]] auto avm_byte_lookup_table_output = View(new_term.avm_byte_lookup_table_output); \ + [[maybe_unused]] auto avm_main_alu_in_tag = View(new_term.avm_main_alu_in_tag); \ [[maybe_unused]] auto avm_main_alu_sel = View(new_term.avm_main_alu_sel); \ [[maybe_unused]] auto avm_main_bin_op_id = View(new_term.avm_main_bin_op_id); \ [[maybe_unused]] auto avm_main_bin_sel = View(new_term.avm_main_bin_sel); \ @@ -124,6 +125,7 @@ [[maybe_unused]] auto avm_main_sel_mov_b = View(new_term.avm_main_sel_mov_b); \ [[maybe_unused]] auto avm_main_sel_op_add = View(new_term.avm_main_sel_op_add); \ [[maybe_unused]] auto avm_main_sel_op_and = View(new_term.avm_main_sel_op_and); \ + [[maybe_unused]] auto avm_main_sel_op_cast = View(new_term.avm_main_sel_op_cast); \ [[maybe_unused]] auto avm_main_sel_op_div = View(new_term.avm_main_sel_op_div); \ [[maybe_unused]] auto avm_main_sel_op_eq = View(new_term.avm_main_sel_op_eq); \ [[maybe_unused]] auto avm_main_sel_op_lt = View(new_term.avm_main_sel_op_lt); \ diff --git a/barretenberg/cpp/src/barretenberg/relations/generated/avm/perm_main_alu.hpp b/barretenberg/cpp/src/barretenberg/relations/generated/avm/perm_main_alu.hpp index 0a45bb920d5..742265fea43 100644 --- a/barretenberg/cpp/src/barretenberg/relations/generated/avm/perm_main_alu.hpp +++ b/barretenberg/cpp/src/barretenberg/relations/generated/avm/perm_main_alu.hpp @@ -59,9 +59,13 @@ class perm_main_alu_permutation_settings { in.avm_main_sel_op_mul, in.avm_main_sel_op_eq, in.avm_main_sel_op_not, +<<<<<<< HEAD in.avm_main_sel_op_lt, in.avm_main_sel_op_lte, in.avm_main_r_in_tag, +======= + in.avm_main_alu_in_tag, +>>>>>>> a83ef175e (5466 - introduce in_tag dispatching to the ALU) in.avm_alu_clk, in.avm_alu_ia, in.avm_alu_ib, @@ -109,9 +113,13 @@ class perm_main_alu_permutation_settings { in.avm_main_sel_op_mul, in.avm_main_sel_op_eq, in.avm_main_sel_op_not, +<<<<<<< HEAD in.avm_main_sel_op_lt, in.avm_main_sel_op_lte, in.avm_main_r_in_tag, +======= + in.avm_main_alu_in_tag, +>>>>>>> a83ef175e (5466 - introduce in_tag dispatching to the ALU) in.avm_alu_clk, in.avm_alu_ia, in.avm_alu_ib, 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 a9e27af4127..9eeb7d0bc22 100644 --- a/barretenberg/cpp/src/barretenberg/vm/avm_trace/avm_trace.cpp +++ b/barretenberg/cpp/src/barretenberg/vm/avm_trace/avm_trace.cpp @@ -118,6 +118,7 @@ void AvmTraceBuilder::op_add( main_trace.push_back(Row{ .avm_main_clk = clk, + .avm_main_alu_in_tag = FF(static_cast(in_tag)), .avm_main_ia = a, .avm_main_ib = b, .avm_main_ic = c, @@ -181,6 +182,7 @@ void AvmTraceBuilder::op_sub( main_trace.push_back(Row{ .avm_main_clk = clk, + .avm_main_alu_in_tag = FF(static_cast(in_tag)), .avm_main_ia = a, .avm_main_ib = b, .avm_main_ic = c, @@ -244,6 +246,7 @@ void AvmTraceBuilder::op_mul( main_trace.push_back(Row{ .avm_main_clk = clk, + .avm_main_alu_in_tag = FF(static_cast(in_tag)), .avm_main_ia = a, .avm_main_ib = b, .avm_main_ic = c, @@ -390,6 +393,7 @@ void AvmTraceBuilder::op_not(uint8_t indirect, uint32_t a_offset, uint32_t dst_o main_trace.push_back(Row{ .avm_main_clk = clk, + .avm_main_alu_in_tag = FF(static_cast(in_tag)), .avm_main_ia = a, .avm_main_ic = c, .avm_main_ind_a = indirect_a_flag ? FF(a_offset) : FF(0), @@ -447,6 +451,7 @@ void AvmTraceBuilder::op_eq( main_trace.push_back(Row{ .avm_main_clk = clk, + .avm_main_alu_in_tag = FF(static_cast(in_tag)), .avm_main_ia = a, .avm_main_ib = b, .avm_main_ic = c, 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 4a163364de3..5ffe3d319db 100644 --- a/barretenberg/cpp/src/barretenberg/vm/generated/avm_circuit_builder.hpp +++ b/barretenberg/cpp/src/barretenberg/vm/generated/avm_circuit_builder.hpp @@ -129,6 +129,7 @@ template struct AvmFullRow { FF avm_byte_lookup_table_input_b{}; FF avm_byte_lookup_table_op_id{}; FF avm_byte_lookup_table_output{}; + FF avm_main_alu_in_tag{}; FF avm_main_alu_sel{}; FF avm_main_bin_op_id{}; FF avm_main_bin_sel{}; @@ -173,6 +174,7 @@ template struct AvmFullRow { FF avm_main_sel_mov_b{}; FF avm_main_sel_op_add{}; FF avm_main_sel_op_and{}; + FF avm_main_sel_op_cast{}; FF avm_main_sel_op_div{}; FF avm_main_sel_op_eq{}; FF avm_main_sel_op_lt{}; @@ -309,8 +311,13 @@ class AvmCircuitBuilder { using Polynomial = Flavor::Polynomial; using ProverPolynomials = Flavor::ProverPolynomials; +<<<<<<< HEAD static constexpr size_t num_fixed_columns = 246; static constexpr size_t num_polys = 211; +======= + static constexpr size_t num_fixed_columns = 152; + static constexpr size_t num_polys = 133; +>>>>>>> a83ef175e (5466 - introduce in_tag dispatching to the ALU) std::vector rows; void set_trace(std::vector&& trace) { rows = std::move(trace); } @@ -404,6 +411,7 @@ class AvmCircuitBuilder { polys.avm_byte_lookup_table_input_b[i] = rows[i].avm_byte_lookup_table_input_b; polys.avm_byte_lookup_table_op_id[i] = rows[i].avm_byte_lookup_table_op_id; polys.avm_byte_lookup_table_output[i] = rows[i].avm_byte_lookup_table_output; + polys.avm_main_alu_in_tag[i] = rows[i].avm_main_alu_in_tag; polys.avm_main_alu_sel[i] = rows[i].avm_main_alu_sel; polys.avm_main_bin_op_id[i] = rows[i].avm_main_bin_op_id; polys.avm_main_bin_sel[i] = rows[i].avm_main_bin_sel; @@ -448,6 +456,7 @@ class AvmCircuitBuilder { polys.avm_main_sel_mov_b[i] = rows[i].avm_main_sel_mov_b; polys.avm_main_sel_op_add[i] = rows[i].avm_main_sel_op_add; polys.avm_main_sel_op_and[i] = rows[i].avm_main_sel_op_and; + polys.avm_main_sel_op_cast[i] = rows[i].avm_main_sel_op_cast; polys.avm_main_sel_op_div[i] = rows[i].avm_main_sel_op_div; polys.avm_main_sel_op_eq[i] = rows[i].avm_main_sel_op_eq; polys.avm_main_sel_op_lt[i] = rows[i].avm_main_sel_op_lt; diff --git a/barretenberg/cpp/src/barretenberg/vm/generated/avm_flavor.hpp b/barretenberg/cpp/src/barretenberg/vm/generated/avm_flavor.hpp index 4bb786ea4cb..673d0e59f37 100644 --- a/barretenberg/cpp/src/barretenberg/vm/generated/avm_flavor.hpp +++ b/barretenberg/cpp/src/barretenberg/vm/generated/avm_flavor.hpp @@ -69,6 +69,7 @@ class AvmFlavor { using RelationSeparator = FF; static constexpr size_t NUM_PRECOMPUTED_ENTITIES = 2; +<<<<<<< HEAD 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 @@ -106,6 +107,13 @@ class AvmFlavor { lookup_u16_12_relation, lookup_u16_13_relation, lookup_u16_14_relation>; +======= + static constexpr size_t NUM_WITNESS_ENTITIES = 131; + 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 = 152; +>>>>>>> a83ef175e (5466 - introduce in_tag dispatching to the ALU) using Relations = std::tuple, Avm_vm::avm_binary, @@ -251,6 +259,7 @@ class AvmFlavor { avm_byte_lookup_table_input_b, avm_byte_lookup_table_op_id, avm_byte_lookup_table_output, + avm_main_alu_in_tag, avm_main_alu_sel, avm_main_bin_op_id, avm_main_bin_sel, @@ -295,6 +304,7 @@ class AvmFlavor { avm_main_sel_mov_b, avm_main_sel_op_add, avm_main_sel_op_and, + avm_main_sel_op_cast, avm_main_sel_op_div, avm_main_sel_op_eq, avm_main_sel_op_lt, @@ -463,6 +473,7 @@ class AvmFlavor { avm_byte_lookup_table_input_b, avm_byte_lookup_table_op_id, avm_byte_lookup_table_output, + avm_main_alu_in_tag, avm_main_alu_sel, avm_main_bin_op_id, avm_main_bin_sel, @@ -507,6 +518,7 @@ class AvmFlavor { avm_main_sel_mov_b, avm_main_sel_op_add, avm_main_sel_op_and, + avm_main_sel_op_cast, avm_main_sel_op_div, avm_main_sel_op_eq, avm_main_sel_op_lt, @@ -680,6 +692,7 @@ class AvmFlavor { avm_byte_lookup_table_input_b, avm_byte_lookup_table_op_id, avm_byte_lookup_table_output, + avm_main_alu_in_tag, avm_main_alu_sel, avm_main_bin_op_id, avm_main_bin_sel, @@ -724,6 +737,7 @@ class AvmFlavor { avm_main_sel_mov_b, avm_main_sel_op_add, avm_main_sel_op_and, + avm_main_sel_op_cast, avm_main_sel_op_div, avm_main_sel_op_eq, avm_main_sel_op_lt, @@ -929,6 +943,7 @@ class AvmFlavor { avm_byte_lookup_table_input_b, avm_byte_lookup_table_op_id, avm_byte_lookup_table_output, + avm_main_alu_in_tag, avm_main_alu_sel, avm_main_bin_op_id, avm_main_bin_sel, @@ -973,6 +988,7 @@ class AvmFlavor { avm_main_sel_mov_b, avm_main_sel_op_add, avm_main_sel_op_and, + avm_main_sel_op_cast, avm_main_sel_op_div, avm_main_sel_op_eq, avm_main_sel_op_lt, @@ -1178,6 +1194,7 @@ class AvmFlavor { avm_byte_lookup_table_input_b, avm_byte_lookup_table_op_id, avm_byte_lookup_table_output, + avm_main_alu_in_tag, avm_main_alu_sel, avm_main_bin_op_id, avm_main_bin_sel, @@ -1222,6 +1239,7 @@ class AvmFlavor { avm_main_sel_mov_b, avm_main_sel_op_add, avm_main_sel_op_and, + avm_main_sel_op_cast, avm_main_sel_op_div, avm_main_sel_op_eq, avm_main_sel_op_lt, @@ -1621,6 +1639,7 @@ class AvmFlavor { Base::avm_byte_lookup_table_input_b = "AVM_BYTE_LOOKUP_TABLE_INPUT_B"; Base::avm_byte_lookup_table_op_id = "AVM_BYTE_LOOKUP_TABLE_OP_ID"; Base::avm_byte_lookup_table_output = "AVM_BYTE_LOOKUP_TABLE_OUTPUT"; + Base::avm_main_alu_in_tag = "AVM_MAIN_ALU_IN_TAG"; Base::avm_main_alu_sel = "AVM_MAIN_ALU_SEL"; Base::avm_main_bin_op_id = "AVM_MAIN_BIN_OP_ID"; Base::avm_main_bin_sel = "AVM_MAIN_BIN_SEL"; @@ -1665,6 +1684,7 @@ class AvmFlavor { Base::avm_main_sel_mov_b = "AVM_MAIN_SEL_MOV_B"; Base::avm_main_sel_op_add = "AVM_MAIN_SEL_OP_ADD"; Base::avm_main_sel_op_and = "AVM_MAIN_SEL_OP_AND"; + Base::avm_main_sel_op_cast = "AVM_MAIN_SEL_OP_CAST"; Base::avm_main_sel_op_div = "AVM_MAIN_SEL_OP_DIV"; Base::avm_main_sel_op_eq = "AVM_MAIN_SEL_OP_EQ"; Base::avm_main_sel_op_lt = "AVM_MAIN_SEL_OP_LT"; @@ -1849,6 +1869,7 @@ class AvmFlavor { Commitment avm_byte_lookup_table_input_b; Commitment avm_byte_lookup_table_op_id; Commitment avm_byte_lookup_table_output; + Commitment avm_main_alu_in_tag; Commitment avm_main_alu_sel; Commitment avm_main_bin_op_id; Commitment avm_main_bin_sel; @@ -1893,6 +1914,7 @@ class AvmFlavor { Commitment avm_main_sel_mov_b; Commitment avm_main_sel_op_add; Commitment avm_main_sel_op_and; + Commitment avm_main_sel_op_cast; Commitment avm_main_sel_op_div; Commitment avm_main_sel_op_eq; Commitment avm_main_sel_op_lt; @@ -2078,6 +2100,7 @@ class AvmFlavor { avm_byte_lookup_table_input_b = deserialize_from_buffer(Transcript::proof_data, num_frs_read); avm_byte_lookup_table_op_id = deserialize_from_buffer(Transcript::proof_data, num_frs_read); avm_byte_lookup_table_output = deserialize_from_buffer(Transcript::proof_data, num_frs_read); + avm_main_alu_in_tag = deserialize_from_buffer(Transcript::proof_data, num_frs_read); avm_main_alu_sel = deserialize_from_buffer(Transcript::proof_data, num_frs_read); avm_main_bin_op_id = deserialize_from_buffer(Transcript::proof_data, num_frs_read); avm_main_bin_sel = deserialize_from_buffer(Transcript::proof_data, num_frs_read); @@ -2122,6 +2145,7 @@ class AvmFlavor { avm_main_sel_mov_b = deserialize_from_buffer(Transcript::proof_data, num_frs_read); avm_main_sel_op_add = deserialize_from_buffer(Transcript::proof_data, num_frs_read); avm_main_sel_op_and = deserialize_from_buffer(Transcript::proof_data, num_frs_read); + avm_main_sel_op_cast = deserialize_from_buffer(Transcript::proof_data, num_frs_read); avm_main_sel_op_div = deserialize_from_buffer(Transcript::proof_data, num_frs_read); avm_main_sel_op_eq = deserialize_from_buffer(Transcript::proof_data, num_frs_read); avm_main_sel_op_lt = deserialize_from_buffer(Transcript::proof_data, num_frs_read); @@ -2310,6 +2334,7 @@ class AvmFlavor { serialize_to_buffer(avm_byte_lookup_table_input_b, Transcript::proof_data); serialize_to_buffer(avm_byte_lookup_table_op_id, Transcript::proof_data); serialize_to_buffer(avm_byte_lookup_table_output, Transcript::proof_data); + serialize_to_buffer(avm_main_alu_in_tag, Transcript::proof_data); serialize_to_buffer(avm_main_alu_sel, Transcript::proof_data); serialize_to_buffer(avm_main_bin_op_id, Transcript::proof_data); serialize_to_buffer(avm_main_bin_sel, Transcript::proof_data); @@ -2354,6 +2379,7 @@ class AvmFlavor { serialize_to_buffer(avm_main_sel_mov_b, Transcript::proof_data); serialize_to_buffer(avm_main_sel_op_add, Transcript::proof_data); serialize_to_buffer(avm_main_sel_op_and, Transcript::proof_data); + serialize_to_buffer(avm_main_sel_op_cast, Transcript::proof_data); serialize_to_buffer(avm_main_sel_op_div, Transcript::proof_data); serialize_to_buffer(avm_main_sel_op_eq, Transcript::proof_data); serialize_to_buffer(avm_main_sel_op_lt, Transcript::proof_data); diff --git a/barretenberg/cpp/src/barretenberg/vm/generated/avm_verifier.cpp b/barretenberg/cpp/src/barretenberg/vm/generated/avm_verifier.cpp index f1b9bb2e4cd..116deb5058c 100644 --- a/barretenberg/cpp/src/barretenberg/vm/generated/avm_verifier.cpp +++ b/barretenberg/cpp/src/barretenberg/vm/generated/avm_verifier.cpp @@ -167,6 +167,8 @@ bool AvmVerifier::verify_proof(const HonkProof& proof) transcript->template receive_from_prover(commitment_labels.avm_byte_lookup_table_op_id); commitments.avm_byte_lookup_table_output = transcript->template receive_from_prover(commitment_labels.avm_byte_lookup_table_output); + commitments.avm_main_alu_in_tag = + transcript->template receive_from_prover(commitment_labels.avm_main_alu_in_tag); commitments.avm_main_alu_sel = transcript->template receive_from_prover(commitment_labels.avm_main_alu_sel); commitments.avm_main_bin_op_id = @@ -240,6 +242,8 @@ bool AvmVerifier::verify_proof(const HonkProof& proof) transcript->template receive_from_prover(commitment_labels.avm_main_sel_op_add); commitments.avm_main_sel_op_and = transcript->template receive_from_prover(commitment_labels.avm_main_sel_op_and); + commitments.avm_main_sel_op_cast = + transcript->template receive_from_prover(commitment_labels.avm_main_sel_op_cast); commitments.avm_main_sel_op_div = transcript->template receive_from_prover(commitment_labels.avm_main_sel_op_div); commitments.avm_main_sel_op_eq = From ae92c2ea7070cc2316b9f8454e422404baf225b5 Mon Sep 17 00:00:00 2001 From: jeanmon Date: Thu, 28 Mar 2024 10:03:55 +0000 Subject: [PATCH 2/8] 5466: PIL relations for CAST opcode + rebase on master conflicts resolution --- barretenberg/cpp/pil/avm/avm_alu.pil | 29 +- barretenberg/cpp/pil/avm/avm_main.pil | 7 +- .../relations/generated/avm/avm_alu.hpp | 198 +++++++----- .../relations/generated/avm/avm_main.hpp | 289 +++++++++++++----- .../relations/generated/avm/declare_views.hpp | 2 + .../relations/generated/avm/perm_main_alu.hpp | 14 +- .../barretenberg/vm/avm_trace/avm_trace.cpp | 2 + .../vm/generated/avm_circuit_builder.hpp | 13 +- .../barretenberg/vm/generated/avm_flavor.hpp | 179 +++++++---- .../barretenberg/vm/generated/avm_prover.cpp | 6 + .../vm/generated/avm_verifier.cpp | 2 + 11 files changed, 498 insertions(+), 243 deletions(-) diff --git a/barretenberg/cpp/pil/avm/avm_alu.pil b/barretenberg/cpp/pil/avm/avm_alu.pil index 8e2a578c5df..96a00f74cb3 100644 --- a/barretenberg/cpp/pil/avm/avm_alu.pil +++ b/barretenberg/cpp/pil/avm/avm_alu.pil @@ -17,6 +17,7 @@ namespace avm_alu(256); pol commit op_div; pol commit op_not; pol commit op_eq; + pol commit op_cast; pol commit alu_sel; // Predicate to activate the copy of intermediate registers to ALU table. pol commit op_lt; pol commit op_lte; @@ -59,7 +60,7 @@ namespace avm_alu(256); pol commit cf; // Compute predicate telling whether there is a row entry in the ALU table. - alu_sel = op_add + op_sub + op_mul + op_not + op_eq + op_lt + op_lte; + alu_sel = op_add + op_sub + op_mul + op_not + op_eq + op_cast + op_lt + op_lte; cmp_sel = op_lt + op_lte; // ========= Type Constraints ============================================= @@ -265,6 +266,20 @@ namespace avm_alu(256); #[ALU_OP_EQ] op_eq * (DIFF * (ic * (1 - op_eq_diff_inv) + op_eq_diff_inv) - 1 + ic) = 0; + // ========= CAST Operation Constraints =============================== + // We handle the input ia independently of its tag, i.e., we suppose it can take + // any value between 0 and p-1. + // We decompose the input ia in 8-bit/16-bit limbs and prove that the decomposition + // sums up to ia over the integers (i.e., no modulo p wrapping). To prove this, + // we perform a "school subtraction" (borrowing) over 128-bit limbs. + // The input I is written I = I_l + I_h * 2^128 and the field order P = P_l + P_h * 2^128. + // The school subtraction result is D = D_l + D_h * 2^128 and we prove the correctness + // through: P_l - I_l - CF * 2^128 == D_l AND P_h - I_h + CF == D_h + // where CF is a carry/borrowing bit. CF == 1 <==> P_l < I_l. + + #[ALU_OP_CAST] + op_cast * (SUM_TAG + ff_tag * ia - ic) = 0; + // ========= LT/LTE Operation Constraints =============================== // There are two routines that we utilise as part of this LT/LTE check // (1) Decomposition into two 128-bit limbs, lo and hi respectively and a borrow (1 or 0); @@ -282,7 +297,7 @@ namespace avm_alu(256); // (x - y - 1) * q + (y - x) (1 - q) = result // If LT, then swap ia and ib else keep the same - pol INPUT_IA = op_lt * ib + op_lte * ia; + pol INPUT_IA = op_lt * ib + (op_lte + op_cast) * ia; pol INPUT_IB = op_lt * ia + op_lte * ib; pol commit borrow; @@ -290,7 +305,7 @@ namespace avm_alu(256); pol commit a_hi; // Check INPUT_IA is well formed from its lo and hi limbs #[INPUT_DECOMP_1] - INPUT_IA = (a_lo + 2 ** 128 * a_hi) * cmp_sel; + INPUT_IA = (a_lo + 2 ** 128 * a_hi) * (cmp_sel + op_cast); pol commit b_lo; pol commit b_hi; @@ -311,9 +326,9 @@ namespace avm_alu(256); // First condition is if borrow = 0, second condition is if borrow = 1 // This underflow check is done by the 128-bit check that is performed on each of these lo and hi limbs. #[SUB_LO_1] - (p_sub_a_lo - (53438638232309528389504892708671455232 - a_lo + p_a_borrow * 2 ** 128)) * cmp_sel = 0; + (p_sub_a_lo - (53438638232309528389504892708671455232 - a_lo + p_a_borrow * 2 ** 128)) * (cmp_sel + op_cast) = 0; #[SUB_HI_1] - (p_sub_a_hi - (64323764613183177041862057485226039389 - a_hi - p_a_borrow)) * cmp_sel = 0; + (p_sub_a_hi - (64323764613183177041862057485226039389 - a_hi - p_a_borrow)) * (cmp_sel + op_cast) = 0; pol commit p_sub_b_lo; pol commit p_sub_b_hi; @@ -436,11 +451,11 @@ namespace avm_alu(256); pol commit rng_chk_lookup_selector; #[RNG_CHK_LOOKUP_SELECTOR] - rng_chk_lookup_selector' = cmp_sel' + rng_chk_sel' + op_add' + op_sub' + op_mul' + op_mul * u128_tag; + rng_chk_lookup_selector' = cmp_sel' + rng_chk_sel' + op_add' + op_sub' + op_mul' + op_mul * u128_tag + op_cast'; // Perform 128-bit range check on lo part #[LOWER_CMP_RNG_CHK] - a_lo = SUM_128 * RNG_CHK_OP; + a_lo = SUM_128 * (RNG_CHK_OP + op_cast); // Perform 128-bit range check on hi part #[UPPER_CMP_RNG_CHK] diff --git a/barretenberg/cpp/pil/avm/avm_main.pil b/barretenberg/cpp/pil/avm/avm_main.pil index 8e32589b75e..f4ce7214edb 100644 --- a/barretenberg/cpp/pil/avm/avm_main.pil +++ b/barretenberg/cpp/pil/avm/avm_main.pil @@ -316,10 +316,13 @@ namespace avm_main(256); #[PERM_MAIN_ALU] alu_sel {clk, ia, ib, ic, sel_op_add, sel_op_sub, - sel_op_mul, sel_op_eq, sel_op_not, sel_op_lt, sel_op_lte, alu_in_tag} + sel_op_mul, sel_op_eq, sel_op_not, sel_op_cast, + sel_op_lt, sel_op_lte, alu_in_tag} is avm_alu.alu_sel {avm_alu.clk, avm_alu.ia, avm_alu.ib, avm_alu.ic, avm_alu.op_add, avm_alu.op_sub, - avm_alu.op_mul, avm_alu.op_eq, avm_alu.op_not, avm_alu.op_lt, avm_alu.op_lte, avm_alu.in_tag}; + avm_alu.op_mul, avm_alu.op_eq, avm_alu.op_not, avm_alu.op_cast, + avm_alu.op_lt, avm_alu.op_lte, avm_alu.in_tag}; + // Based on the boolean selectors, we derive the binary op id to lookup in the table; // TODO: Check if having 4 columns (op_id + 3 boolean selectors) is more optimal that just using the op_id // but with a higher degree constraint: op_id * (op_id - 1) * (op_id - 2) 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 8682c27d4cf..2ba5ef845e7 100644 --- a/barretenberg/cpp/src/barretenberg/relations/generated/avm/avm_alu.hpp +++ b/barretenberg/cpp/src/barretenberg/relations/generated/avm/avm_alu.hpp @@ -29,6 +29,8 @@ template struct Avm_aluRow { FF avm_alu_in_tag{}; FF avm_alu_op_add{}; FF avm_alu_op_add_shift{}; + FF avm_alu_op_cast{}; + FF avm_alu_op_cast_shift{}; FF avm_alu_op_eq{}; FF avm_alu_op_eq_diff_inv{}; FF avm_alu_op_lt{}; @@ -120,57 +122,60 @@ inline std::string get_relation_label_avm_alu(int index) return "ALU_OP_EQ"; case 23: - return "INPUT_DECOMP_1"; + return "ALU_OP_CAST"; case 24: + return "INPUT_DECOMP_1"; + + case 25: return "INPUT_DECOMP_2"; - case 26: + case 27: return "SUB_LO_1"; - case 27: + case 28: return "SUB_HI_1"; - case 29: + case 30: return "SUB_LO_2"; - case 30: + case 31: return "SUB_HI_2"; - case 31: + case 32: return "RES_LO"; - case 32: + case 33: return "RES_HI"; - case 33: + case 34: return "CMP_CTR_REL_1"; - case 34: + case 35: return "CMP_CTR_REL_2"; - case 37: + case 38: return "CTR_NON_ZERO_REL"; - case 38: + case 39: return "RNG_CHK_LOOKUP_SELECTOR"; - case 39: + case 40: return "LOWER_CMP_RNG_CHK"; - case 40: + case 41: return "UPPER_CMP_RNG_CHK"; - case 41: + case 42: return "SHIFT_RELS_0"; - case 43: + case 44: return "SHIFT_RELS_1"; - case 45: + case 46: return "SHIFT_RELS_2"; - case 47: + case 48: return "SHIFT_RELS_3"; } return std::to_string(index); @@ -180,9 +185,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, 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, + 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, 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 @@ -197,7 +202,8 @@ template class avm_aluImpl { Avm_DECLARE_VIEWS(0); auto tmp = (avm_alu_alu_sel - - ((((((avm_alu_op_add + avm_alu_op_sub) + avm_alu_op_mul) + avm_alu_op_not) + avm_alu_op_eq) + + (((((((avm_alu_op_add + avm_alu_op_sub) + avm_alu_op_mul) + avm_alu_op_not) + avm_alu_op_eq) + + avm_alu_op_cast) + avm_alu_op_lt) + avm_alu_op_lte)); tmp *= scaling_factor; @@ -478,8 +484,25 @@ template class avm_aluImpl { { Avm_DECLARE_VIEWS(23); - 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_cast * + (((((((avm_alu_u8_tag * avm_alu_u8_r0) + + (avm_alu_u16_tag * (avm_alu_u8_r0 + (avm_alu_u8_r1 * FF(256))))) + + (avm_alu_u32_tag * + ((avm_alu_u8_r0 + (avm_alu_u8_r1 * FF(256))) + (avm_alu_u16_r0 * FF(65536))))) + + (avm_alu_u64_tag * ((((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_u128_tag * + ((((((((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 * FF(uint256_t{ 0UL, 1UL, 0UL, 0UL }))) + + (avm_alu_u16_r4 * FF(uint256_t{ 0UL, 65536UL, 0UL, 0UL }))) + + (avm_alu_u16_r5 * FF(uint256_t{ 0UL, 4294967296UL, 0UL, 0UL }))) + + (avm_alu_u16_r6 * FF(uint256_t{ 0UL, 281474976710656UL, 0UL, 0UL }))))) + + (avm_alu_ff_tag * avm_alu_ia)) - + avm_alu_ic)); tmp *= scaling_factor; std::get<23>(evals) += tmp; } @@ -487,8 +510,9 @@ template class avm_aluImpl { { Avm_DECLARE_VIEWS(24); - 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_op_cast) * avm_alu_ia)) - + ((avm_alu_a_lo + (avm_alu_a_hi * FF(uint256_t{ 0UL, 0UL, 1UL, 0UL }))) * + (avm_alu_cmp_sel + avm_alu_op_cast))); tmp *= scaling_factor; std::get<24>(evals) += tmp; } @@ -496,7 +520,8 @@ template class avm_aluImpl { { Avm_DECLARE_VIEWS(25); - 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<25>(evals) += tmp; } @@ -504,10 +529,7 @@ template class avm_aluImpl { { Avm_DECLARE_VIEWS(26); - 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<26>(evals) += tmp; } @@ -515,10 +537,10 @@ template class avm_aluImpl { { Avm_DECLARE_VIEWS(27); - 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); + 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 + avm_alu_op_cast)); tmp *= scaling_factor; std::get<27>(evals) += tmp; } @@ -526,7 +548,10 @@ template class avm_aluImpl { { Avm_DECLARE_VIEWS(28); - 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 + avm_alu_op_cast)); tmp *= scaling_factor; std::get<28>(evals) += tmp; } @@ -534,27 +559,35 @@ template class avm_aluImpl { { Avm_DECLARE_VIEWS(29); + auto tmp = (avm_alu_p_b_borrow * (-avm_alu_p_b_borrow + FF(1))); + tmp *= scaling_factor; + std::get<29>(evals) += tmp; + } + // Contribution 30 + { + Avm_DECLARE_VIEWS(30); + 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<29>(evals) += tmp; + std::get<30>(evals) += tmp; } - // Contribution 30 + // Contribution 31 { - Avm_DECLARE_VIEWS(30); + Avm_DECLARE_VIEWS(31); 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<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_lo - @@ -564,11 +597,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<31>(evals) += tmp; + std::get<32>(evals) += tmp; } - // Contribution 32 + // Contribution 33 { - Avm_DECLARE_VIEWS(32); + Avm_DECLARE_VIEWS(33); auto tmp = ((avm_alu_res_hi - ((((avm_alu_a_hi - avm_alu_b_hi) - avm_alu_borrow) * @@ -577,21 +610,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<32>(evals) += tmp; - } - // Contribution 33 - { - Avm_DECLARE_VIEWS(33); - - 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; } // Contribution 34 { Avm_DECLARE_VIEWS(34); - 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<34>(evals) += tmp; } @@ -599,7 +624,7 @@ template class avm_aluImpl { { Avm_DECLARE_VIEWS(35); - 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<35>(evals) += tmp; } @@ -607,7 +632,7 @@ template class avm_aluImpl { { Avm_DECLARE_VIEWS(36); - 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<36>(evals) += tmp; } @@ -615,9 +640,7 @@ template class avm_aluImpl { { Avm_DECLARE_VIEWS(37); - 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<37>(evals) += tmp; } @@ -625,11 +648,9 @@ 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))); + 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<38>(evals) += tmp; } @@ -637,6 +658,19 @@ template class avm_aluImpl { { Avm_DECLARE_VIEWS(39); + 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)) + + avm_alu_op_cast_shift)); + tmp *= scaling_factor; + std::get<39>(evals) += tmp; + } + // Contribution 40 + { + Avm_DECLARE_VIEWS(40); + 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))) + @@ -645,13 +679,13 @@ template class avm_aluImpl { (avm_alu_u16_r4 * FF(uint256_t{ 0UL, 65536UL, 0UL, 0UL }))) + (avm_alu_u16_r5 * FF(uint256_t{ 0UL, 4294967296UL, 0UL, 0UL }))) + (avm_alu_u16_r6 * FF(uint256_t{ 0UL, 281474976710656UL, 0UL, 0UL }))) * - (avm_alu_rng_chk_sel + avm_alu_cmp_sel))); + ((avm_alu_rng_chk_sel + avm_alu_cmp_sel) + avm_alu_op_cast))); tmp *= scaling_factor; - std::get<39>(evals) += tmp; + std::get<40>(evals) += tmp; } - // Contribution 40 + // Contribution 41 { - Avm_DECLARE_VIEWS(40); + Avm_DECLARE_VIEWS(41); auto tmp = (avm_alu_a_hi - ((((((((avm_alu_u16_r7 + (avm_alu_u16_r8 * FF(65536))) + (avm_alu_u16_r9 * FF(4294967296UL))) + @@ -662,21 +696,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<40>(evals) += tmp; - } - // Contribution 41 - { - Avm_DECLARE_VIEWS(41); - - 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; } // Contribution 42 { Avm_DECLARE_VIEWS(42); - 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<42>(evals) += tmp; } @@ -684,7 +710,7 @@ template class avm_aluImpl { { Avm_DECLARE_VIEWS(43); - 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<43>(evals) += tmp; } @@ -692,7 +718,7 @@ template class avm_aluImpl { { Avm_DECLARE_VIEWS(44); - 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<44>(evals) += tmp; } @@ -700,7 +726,7 @@ template class avm_aluImpl { { Avm_DECLARE_VIEWS(45); - 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<45>(evals) += tmp; } @@ -708,7 +734,7 @@ template class avm_aluImpl { { Avm_DECLARE_VIEWS(46); - 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<46>(evals) += tmp; } @@ -716,7 +742,7 @@ template class avm_aluImpl { { Avm_DECLARE_VIEWS(47); - 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<47>(evals) += tmp; } @@ -724,10 +750,18 @@ template class avm_aluImpl { { Avm_DECLARE_VIEWS(48); - 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<48>(evals) += tmp; } + // Contribution 49 + { + Avm_DECLARE_VIEWS(49); + + auto tmp = ((avm_alu_p_sub_b_hi_shift - avm_alu_res_hi) * avm_alu_rng_chk_sel_shift); + tmp *= scaling_factor; + std::get<49>(evals) += tmp; + } } }; diff --git a/barretenberg/cpp/src/barretenberg/relations/generated/avm/avm_main.hpp b/barretenberg/cpp/src/barretenberg/relations/generated/avm/avm_main.hpp index 8c88b757773..b9c4dfd14df 100644 --- a/barretenberg/cpp/src/barretenberg/relations/generated/avm/avm_main.hpp +++ b/barretenberg/cpp/src/barretenberg/relations/generated/avm/avm_main.hpp @@ -65,43 +65,52 @@ template struct Avm_mainRow { inline std::string get_relation_label_avm_main(int index) { switch (index) { - case 25: - return "EQ_OUTPUT_U8"; + case 33: + return "OUTPUT_U8"; - case 26: + case 34: return "SUBOP_DIVISION_FF"; - case 27: + case 35: return "SUBOP_DIVISION_ZERO_ERR1"; - case 28: + case 36: return "SUBOP_DIVISION_ZERO_ERR2"; - case 29: + case 37: return "SUBOP_ERROR_RELEVANT_OP"; - case 31: + case 39: return "RETURN_POINTER_INCREMENT"; - case 37: + case 45: return "RETURN_POINTER_DECREMENT"; - case 42: + case 50: return "PC_INCREMENT"; - case 43: + case 51: return "INTERNAL_RETURN_POINTER_CONSISTENCY"; - case 44: - return "MOV_SAME_VALUE"; + case 52: + return "CMOV_CONDITION_RES_1"; - case 45: + case 53: + return "CMOV_CONDITION_RES_2"; + + case 56: + return "MOV_SAME_VALUE_A"; + + case 57: + return "MOV_SAME_VALUE_B"; + + case 58: return "MOV_MAIN_SAME_TAG"; - case 47: + case 62: return "BIN_SEL_1"; - case 48: + case 63: return "BIN_SEL_2"; } return std::to_string(index); @@ -111,9 +120,9 @@ template class avm_mainImpl { public: using FF = FF_; - static constexpr std::array SUBRELATION_PARTIAL_LENGTHS{ - 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, - 3, 5, 4, 4, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 5, 3, 3, 3, 3, 3, 2, + static constexpr std::array SUBRELATION_PARTIAL_LENGTHS{ + 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, + 3, 3, 5, 4, 4, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 5, 3, 4, 4, 3, 3, 3, 3, 3, 3, 3, 3, 3, 2, }; template @@ -199,7 +208,7 @@ template class avm_mainImpl { { Avm_DECLARE_VIEWS(9); - auto tmp = (avm_main_sel_internal_call * (-avm_main_sel_internal_call + FF(1))); + auto tmp = (avm_main_sel_op_cast * (-avm_main_sel_op_cast + FF(1))); tmp *= scaling_factor; std::get<9>(evals) += tmp; } @@ -207,7 +216,7 @@ template class avm_mainImpl { { Avm_DECLARE_VIEWS(10); - auto tmp = (avm_main_sel_internal_return * (-avm_main_sel_internal_return + FF(1))); + auto tmp = (avm_main_sel_op_lt * (-avm_main_sel_op_lt + FF(1))); tmp *= scaling_factor; std::get<10>(evals) += tmp; } @@ -215,7 +224,7 @@ template class avm_mainImpl { { Avm_DECLARE_VIEWS(11); - auto tmp = (avm_main_sel_jump * (-avm_main_sel_jump + FF(1))); + auto tmp = (avm_main_sel_op_lte * (-avm_main_sel_op_lte + FF(1))); tmp *= scaling_factor; std::get<11>(evals) += tmp; } @@ -223,7 +232,7 @@ template class avm_mainImpl { { Avm_DECLARE_VIEWS(12); - auto tmp = (avm_main_sel_halt * (-avm_main_sel_halt + FF(1))); + auto tmp = (avm_main_sel_internal_call * (-avm_main_sel_internal_call + FF(1))); tmp *= scaling_factor; std::get<12>(evals) += tmp; } @@ -231,7 +240,7 @@ template class avm_mainImpl { { Avm_DECLARE_VIEWS(13); - auto tmp = (avm_main_sel_mov * (-avm_main_sel_mov + FF(1))); + auto tmp = (avm_main_sel_internal_return * (-avm_main_sel_internal_return + FF(1))); tmp *= scaling_factor; std::get<13>(evals) += tmp; } @@ -239,7 +248,7 @@ template class avm_mainImpl { { Avm_DECLARE_VIEWS(14); - auto tmp = (avm_main_op_err * (-avm_main_op_err + FF(1))); + auto tmp = (avm_main_sel_jump * (-avm_main_sel_jump + FF(1))); tmp *= scaling_factor; std::get<14>(evals) += tmp; } @@ -247,7 +256,7 @@ template class avm_mainImpl { { Avm_DECLARE_VIEWS(15); - auto tmp = (avm_main_tag_err * (-avm_main_tag_err + FF(1))); + auto tmp = (avm_main_sel_halt * (-avm_main_sel_halt + FF(1))); tmp *= scaling_factor; std::get<15>(evals) += tmp; } @@ -255,7 +264,7 @@ template class avm_mainImpl { { Avm_DECLARE_VIEWS(16); - auto tmp = (avm_main_mem_op_a * (-avm_main_mem_op_a + FF(1))); + auto tmp = (avm_main_sel_mov * (-avm_main_sel_mov + FF(1))); tmp *= scaling_factor; std::get<16>(evals) += tmp; } @@ -263,7 +272,7 @@ template class avm_mainImpl { { Avm_DECLARE_VIEWS(17); - auto tmp = (avm_main_mem_op_b * (-avm_main_mem_op_b + FF(1))); + auto tmp = (avm_main_sel_cmov * (-avm_main_sel_cmov + FF(1))); tmp *= scaling_factor; std::get<17>(evals) += tmp; } @@ -271,7 +280,7 @@ template class avm_mainImpl { { Avm_DECLARE_VIEWS(18); - auto tmp = (avm_main_mem_op_c * (-avm_main_mem_op_c + FF(1))); + auto tmp = (avm_main_op_err * (-avm_main_op_err + FF(1))); tmp *= scaling_factor; std::get<18>(evals) += tmp; } @@ -279,7 +288,7 @@ template class avm_mainImpl { { Avm_DECLARE_VIEWS(19); - auto tmp = (avm_main_rwa * (-avm_main_rwa + FF(1))); + auto tmp = (avm_main_tag_err * (-avm_main_tag_err + FF(1))); tmp *= scaling_factor; std::get<19>(evals) += tmp; } @@ -287,7 +296,7 @@ template class avm_mainImpl { { Avm_DECLARE_VIEWS(20); - auto tmp = (avm_main_rwb * (-avm_main_rwb + FF(1))); + auto tmp = (avm_main_id_zero * (-avm_main_id_zero + FF(1))); tmp *= scaling_factor; std::get<20>(evals) += tmp; } @@ -295,7 +304,7 @@ template class avm_mainImpl { { Avm_DECLARE_VIEWS(21); - auto tmp = (avm_main_rwc * (-avm_main_rwc + FF(1))); + auto tmp = (avm_main_mem_op_a * (-avm_main_mem_op_a + FF(1))); tmp *= scaling_factor; std::get<21>(evals) += tmp; } @@ -303,7 +312,7 @@ template class avm_mainImpl { { Avm_DECLARE_VIEWS(22); - auto tmp = (avm_main_ind_op_a * (-avm_main_ind_op_a + FF(1))); + auto tmp = (avm_main_mem_op_b * (-avm_main_mem_op_b + FF(1))); tmp *= scaling_factor; std::get<22>(evals) += tmp; } @@ -311,7 +320,7 @@ template class avm_mainImpl { { Avm_DECLARE_VIEWS(23); - auto tmp = (avm_main_ind_op_b * (-avm_main_ind_op_b + FF(1))); + auto tmp = (avm_main_mem_op_c * (-avm_main_mem_op_c + FF(1))); tmp *= scaling_factor; std::get<23>(evals) += tmp; } @@ -319,7 +328,7 @@ template class avm_mainImpl { { Avm_DECLARE_VIEWS(24); - auto tmp = (avm_main_ind_op_c * (-avm_main_ind_op_c + FF(1))); + auto tmp = (avm_main_mem_op_d * (-avm_main_mem_op_d + FF(1))); tmp *= scaling_factor; std::get<24>(evals) += tmp; } @@ -327,7 +336,7 @@ template class avm_mainImpl { { Avm_DECLARE_VIEWS(25); - auto tmp = (avm_main_sel_op_eq * (avm_main_w_in_tag - FF(1))); + auto tmp = (avm_main_rwa * (-avm_main_rwa + FF(1))); tmp *= scaling_factor; std::get<25>(evals) += tmp; } @@ -335,8 +344,7 @@ template class avm_mainImpl { { Avm_DECLARE_VIEWS(26); - auto tmp = - ((avm_main_sel_op_div * (-avm_main_op_err + FF(1))) * ((avm_main_ic * avm_main_ib) - avm_main_ia)); + auto tmp = (avm_main_rwb * (-avm_main_rwb + FF(1))); tmp *= scaling_factor; std::get<26>(evals) += tmp; } @@ -344,7 +352,7 @@ template class avm_mainImpl { { Avm_DECLARE_VIEWS(27); - auto tmp = (avm_main_sel_op_div * (((avm_main_ib * avm_main_inv) - FF(1)) + avm_main_op_err)); + auto tmp = (avm_main_rwc * (-avm_main_rwc + FF(1))); tmp *= scaling_factor; std::get<27>(evals) += tmp; } @@ -352,7 +360,7 @@ template class avm_mainImpl { { Avm_DECLARE_VIEWS(28); - auto tmp = ((avm_main_sel_op_div * avm_main_op_err) * (-avm_main_inv + FF(1))); + auto tmp = (avm_main_rwd * (-avm_main_rwd + FF(1))); tmp *= scaling_factor; std::get<28>(evals) += tmp; } @@ -360,7 +368,7 @@ template class avm_mainImpl { { Avm_DECLARE_VIEWS(29); - auto tmp = (avm_main_op_err * (avm_main_sel_op_div - FF(1))); + auto tmp = (avm_main_ind_op_a * (-avm_main_ind_op_a + FF(1))); tmp *= scaling_factor; std::get<29>(evals) += tmp; } @@ -368,7 +376,7 @@ template class avm_mainImpl { { Avm_DECLARE_VIEWS(30); - auto tmp = (avm_main_sel_jump * (avm_main_pc_shift - avm_main_ia)); + auto tmp = (avm_main_ind_op_b * (-avm_main_ind_op_b + FF(1))); tmp *= scaling_factor; std::get<30>(evals) += tmp; } @@ -376,8 +384,7 @@ template class avm_mainImpl { { Avm_DECLARE_VIEWS(31); - auto tmp = (avm_main_sel_internal_call * - (avm_main_internal_return_ptr_shift - (avm_main_internal_return_ptr + FF(1)))); + auto tmp = (avm_main_ind_op_c * (-avm_main_ind_op_c + FF(1))); tmp *= scaling_factor; std::get<31>(evals) += tmp; } @@ -385,7 +392,7 @@ template class avm_mainImpl { { Avm_DECLARE_VIEWS(32); - auto tmp = (avm_main_sel_internal_call * (avm_main_internal_return_ptr - avm_main_mem_idx_b)); + auto tmp = (avm_main_ind_op_d * (-avm_main_ind_op_d + FF(1))); tmp *= scaling_factor; std::get<32>(evals) += tmp; } @@ -393,7 +400,8 @@ template class avm_mainImpl { { Avm_DECLARE_VIEWS(33); - auto tmp = (avm_main_sel_internal_call * (avm_main_pc_shift - avm_main_ia)); + auto tmp = + (((avm_main_sel_op_eq + avm_main_sel_op_lte) + avm_main_sel_op_lt) * (avm_main_w_in_tag - FF(1))); tmp *= scaling_factor; std::get<33>(evals) += tmp; } @@ -401,7 +409,8 @@ template class avm_mainImpl { { Avm_DECLARE_VIEWS(34); - auto tmp = (avm_main_sel_internal_call * ((avm_main_pc + FF(1)) - avm_main_ib)); + auto tmp = + ((avm_main_sel_op_div * (-avm_main_op_err + FF(1))) * ((avm_main_ic * avm_main_ib) - avm_main_ia)); tmp *= scaling_factor; std::get<34>(evals) += tmp; } @@ -409,7 +418,7 @@ template class avm_mainImpl { { Avm_DECLARE_VIEWS(35); - auto tmp = (avm_main_sel_internal_call * (avm_main_rwb - FF(1))); + auto tmp = (avm_main_sel_op_div * (((avm_main_ib * avm_main_inv) - FF(1)) + avm_main_op_err)); tmp *= scaling_factor; std::get<35>(evals) += tmp; } @@ -417,7 +426,7 @@ template class avm_mainImpl { { Avm_DECLARE_VIEWS(36); - auto tmp = (avm_main_sel_internal_call * (avm_main_mem_op_b - FF(1))); + auto tmp = ((avm_main_sel_op_div * avm_main_op_err) * (-avm_main_inv + FF(1))); tmp *= scaling_factor; std::get<36>(evals) += tmp; } @@ -425,8 +434,7 @@ template class avm_mainImpl { { Avm_DECLARE_VIEWS(37); - auto tmp = (avm_main_sel_internal_return * - (avm_main_internal_return_ptr_shift - (avm_main_internal_return_ptr - FF(1)))); + auto tmp = (avm_main_op_err * (avm_main_sel_op_div - FF(1))); tmp *= scaling_factor; std::get<37>(evals) += tmp; } @@ -434,7 +442,7 @@ template class avm_mainImpl { { Avm_DECLARE_VIEWS(38); - auto tmp = (avm_main_sel_internal_return * ((avm_main_internal_return_ptr - FF(1)) - avm_main_mem_idx_a)); + auto tmp = (avm_main_sel_jump * (avm_main_pc_shift - avm_main_ia)); tmp *= scaling_factor; std::get<38>(evals) += tmp; } @@ -442,7 +450,8 @@ template class avm_mainImpl { { Avm_DECLARE_VIEWS(39); - auto tmp = (avm_main_sel_internal_return * (avm_main_pc_shift - avm_main_ia)); + auto tmp = (avm_main_sel_internal_call * + (avm_main_internal_return_ptr_shift - (avm_main_internal_return_ptr + FF(1)))); tmp *= scaling_factor; std::get<39>(evals) += tmp; } @@ -450,7 +459,7 @@ template class avm_mainImpl { { Avm_DECLARE_VIEWS(40); - auto tmp = (avm_main_sel_internal_return * avm_main_rwa); + auto tmp = (avm_main_sel_internal_call * (avm_main_internal_return_ptr - avm_main_mem_idx_b)); tmp *= scaling_factor; std::get<40>(evals) += tmp; } @@ -458,7 +467,7 @@ template class avm_mainImpl { { Avm_DECLARE_VIEWS(41); - auto tmp = (avm_main_sel_internal_return * (avm_main_mem_op_a - FF(1))); + auto tmp = (avm_main_sel_internal_call * (avm_main_pc_shift - avm_main_ia)); tmp *= scaling_factor; std::get<41>(evals) += tmp; } @@ -466,15 +475,7 @@ template class avm_mainImpl { { Avm_DECLARE_VIEWS(42); - auto tmp = - ((((-avm_main_first + FF(1)) * (-avm_main_sel_halt + FF(1))) * - ((((((((avm_main_sel_op_add + avm_main_sel_op_sub) + avm_main_sel_op_div) + avm_main_sel_op_mul) + - avm_main_sel_op_not) + - avm_main_sel_op_eq) + - avm_main_sel_op_and) + - avm_main_sel_op_or) + - avm_main_sel_op_xor)) * - (avm_main_pc_shift - (avm_main_pc + FF(1)))); + auto tmp = (avm_main_sel_internal_call * ((avm_main_pc + FF(1)) - avm_main_ib)); tmp *= scaling_factor; std::get<42>(evals) += tmp; } @@ -482,10 +483,7 @@ template class avm_mainImpl { { Avm_DECLARE_VIEWS(43); - auto tmp = ((-(((avm_main_first + avm_main_sel_internal_call) + avm_main_sel_internal_return) + - avm_main_sel_halt) + - FF(1)) * - (avm_main_internal_return_ptr_shift - avm_main_internal_return_ptr)); + auto tmp = (avm_main_sel_internal_call * (avm_main_rwb - FF(1))); tmp *= scaling_factor; std::get<43>(evals) += tmp; } @@ -493,7 +491,7 @@ template class avm_mainImpl { { Avm_DECLARE_VIEWS(44); - auto tmp = (avm_main_sel_mov * (avm_main_ia - avm_main_ic)); + auto tmp = (avm_main_sel_internal_call * (avm_main_mem_op_b - FF(1))); tmp *= scaling_factor; std::get<44>(evals) += tmp; } @@ -501,7 +499,8 @@ template class avm_mainImpl { { Avm_DECLARE_VIEWS(45); - auto tmp = (avm_main_sel_mov * (avm_main_r_in_tag - avm_main_w_in_tag)); + auto tmp = (avm_main_sel_internal_return * + (avm_main_internal_return_ptr_shift - (avm_main_internal_return_ptr - FF(1)))); tmp *= scaling_factor; std::get<45>(evals) += tmp; } @@ -509,10 +508,7 @@ template class avm_mainImpl { { Avm_DECLARE_VIEWS(46); - auto tmp = (avm_main_alu_sel - - (((((avm_main_sel_op_add + avm_main_sel_op_sub) + avm_main_sel_op_mul) + avm_main_sel_op_not) + - avm_main_sel_op_eq) * - (-avm_main_tag_err + FF(1)))); + auto tmp = (avm_main_sel_internal_return * ((avm_main_internal_return_ptr - FF(1)) - avm_main_mem_idx_a)); tmp *= scaling_factor; std::get<46>(evals) += tmp; } @@ -520,7 +516,7 @@ template class avm_mainImpl { { Avm_DECLARE_VIEWS(47); - auto tmp = (avm_main_bin_op_id - (avm_main_sel_op_or + (avm_main_sel_op_xor * FF(2)))); + auto tmp = (avm_main_sel_internal_return * (avm_main_pc_shift - avm_main_ia)); tmp *= scaling_factor; std::get<47>(evals) += tmp; } @@ -528,10 +524,153 @@ template class avm_mainImpl { { Avm_DECLARE_VIEWS(48); - auto tmp = (avm_main_bin_sel - ((avm_main_sel_op_and + avm_main_sel_op_or) + avm_main_sel_op_xor)); + auto tmp = (avm_main_sel_internal_return * avm_main_rwa); tmp *= scaling_factor; std::get<48>(evals) += tmp; } + // Contribution 49 + { + Avm_DECLARE_VIEWS(49); + + auto tmp = (avm_main_sel_internal_return * (avm_main_mem_op_a - FF(1))); + tmp *= scaling_factor; + std::get<49>(evals) += tmp; + } + // Contribution 50 + { + Avm_DECLARE_VIEWS(50); + + auto tmp = + ((((-avm_main_first + FF(1)) * (-avm_main_sel_halt + FF(1))) * + (((((((((avm_main_sel_op_add + avm_main_sel_op_sub) + avm_main_sel_op_div) + avm_main_sel_op_mul) + + avm_main_sel_op_not) + + avm_main_sel_op_eq) + + avm_main_sel_op_and) + + avm_main_sel_op_or) + + avm_main_sel_op_xor) + + avm_main_sel_op_cast)) * + (avm_main_pc_shift - (avm_main_pc + FF(1)))); + tmp *= scaling_factor; + std::get<50>(evals) += tmp; + } + // Contribution 51 + { + Avm_DECLARE_VIEWS(51); + + auto tmp = ((-(((avm_main_first + avm_main_sel_internal_call) + avm_main_sel_internal_return) + + avm_main_sel_halt) + + FF(1)) * + (avm_main_internal_return_ptr_shift - avm_main_internal_return_ptr)); + tmp *= scaling_factor; + std::get<51>(evals) += tmp; + } + // Contribution 52 + { + Avm_DECLARE_VIEWS(52); + + auto tmp = (avm_main_sel_cmov * (((avm_main_id * avm_main_inv) - FF(1)) + avm_main_id_zero)); + tmp *= scaling_factor; + std::get<52>(evals) += tmp; + } + // Contribution 53 + { + Avm_DECLARE_VIEWS(53); + + auto tmp = ((avm_main_sel_cmov * avm_main_id_zero) * (-avm_main_inv + FF(1))); + tmp *= scaling_factor; + std::get<53>(evals) += tmp; + } + // Contribution 54 + { + Avm_DECLARE_VIEWS(54); + + auto tmp = (avm_main_sel_mov_a - (avm_main_sel_mov + (avm_main_sel_cmov * (-avm_main_id_zero + FF(1))))); + tmp *= scaling_factor; + std::get<54>(evals) += tmp; + } + // Contribution 55 + { + Avm_DECLARE_VIEWS(55); + + auto tmp = (avm_main_sel_mov_b - (avm_main_sel_cmov * avm_main_id_zero)); + tmp *= scaling_factor; + std::get<55>(evals) += tmp; + } + // Contribution 56 + { + Avm_DECLARE_VIEWS(56); + + auto tmp = (avm_main_sel_mov_a * (avm_main_ia - avm_main_ic)); + tmp *= scaling_factor; + std::get<56>(evals) += tmp; + } + // Contribution 57 + { + Avm_DECLARE_VIEWS(57); + + auto tmp = (avm_main_sel_mov_b * (avm_main_ib - avm_main_ic)); + tmp *= scaling_factor; + std::get<57>(evals) += tmp; + } + // Contribution 58 + { + Avm_DECLARE_VIEWS(58); + + auto tmp = ((avm_main_sel_mov + avm_main_sel_cmov) * (avm_main_r_in_tag - avm_main_w_in_tag)); + tmp *= scaling_factor; + std::get<58>(evals) += tmp; + } + // Contribution 59 + { + Avm_DECLARE_VIEWS(59); + + auto tmp = + (avm_main_alu_sel - + ((((((((avm_main_sel_op_add + avm_main_sel_op_sub) + avm_main_sel_op_mul) + avm_main_sel_op_not) + + avm_main_sel_op_eq) + + avm_main_sel_op_lt) + + avm_main_sel_op_lte) + + avm_main_sel_op_cast) * + (-avm_main_tag_err + FF(1)))); + tmp *= scaling_factor; + std::get<59>(evals) += tmp; + } + // Contribution 60 + { + Avm_DECLARE_VIEWS(60); + + auto tmp = (((((((avm_main_sel_op_add + avm_main_sel_op_sub) + avm_main_sel_op_mul) + avm_main_sel_op_not) + + avm_main_sel_op_eq) + + avm_main_sel_op_lt) + + avm_main_sel_op_lte) * + (avm_main_alu_in_tag - avm_main_r_in_tag)); + tmp *= scaling_factor; + std::get<60>(evals) += tmp; + } + // Contribution 61 + { + Avm_DECLARE_VIEWS(61); + + auto tmp = (avm_main_sel_op_cast * (avm_main_alu_in_tag - avm_main_w_in_tag)); + tmp *= scaling_factor; + std::get<61>(evals) += tmp; + } + // Contribution 62 + { + Avm_DECLARE_VIEWS(62); + + auto tmp = (avm_main_bin_op_id - (avm_main_sel_op_or + (avm_main_sel_op_xor * FF(2)))); + tmp *= scaling_factor; + std::get<62>(evals) += tmp; + } + // Contribution 63 + { + Avm_DECLARE_VIEWS(63); + + auto tmp = (avm_main_bin_sel - ((avm_main_sel_op_and + avm_main_sel_op_or) + avm_main_sel_op_xor)); + tmp *= scaling_factor; + std::get<63>(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 8e10193b537..398fbe9840d 100644 --- a/barretenberg/cpp/src/barretenberg/relations/generated/avm/declare_views.hpp +++ b/barretenberg/cpp/src/barretenberg/relations/generated/avm/declare_views.hpp @@ -20,6 +20,7 @@ [[maybe_unused]] auto avm_alu_ic = View(new_term.avm_alu_ic); \ [[maybe_unused]] auto avm_alu_in_tag = View(new_term.avm_alu_in_tag); \ [[maybe_unused]] auto avm_alu_op_add = View(new_term.avm_alu_op_add); \ + [[maybe_unused]] auto avm_alu_op_cast = View(new_term.avm_alu_op_cast); \ [[maybe_unused]] auto avm_alu_op_div = View(new_term.avm_alu_op_div); \ [[maybe_unused]] auto avm_alu_op_eq = View(new_term.avm_alu_op_eq); \ [[maybe_unused]] auto avm_alu_op_eq_diff_inv = View(new_term.avm_alu_op_eq_diff_inv); \ @@ -222,6 +223,7 @@ [[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_cast_shift = View(new_term.avm_alu_op_cast_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); \ diff --git a/barretenberg/cpp/src/barretenberg/relations/generated/avm/perm_main_alu.hpp b/barretenberg/cpp/src/barretenberg/relations/generated/avm/perm_main_alu.hpp index 742265fea43..d79a11acf7c 100644 --- a/barretenberg/cpp/src/barretenberg/relations/generated/avm/perm_main_alu.hpp +++ b/barretenberg/cpp/src/barretenberg/relations/generated/avm/perm_main_alu.hpp @@ -12,7 +12,7 @@ namespace bb { class perm_main_alu_permutation_settings { public: // This constant defines how many columns are bundled together to form each set. - constexpr static size_t COLUMNS_PER_SET = 12; + constexpr static size_t COLUMNS_PER_SET = 13; /** * @brief If this method returns true on a row of values, then the inverse polynomial at this index. Otherwise the @@ -59,13 +59,10 @@ class perm_main_alu_permutation_settings { in.avm_main_sel_op_mul, in.avm_main_sel_op_eq, in.avm_main_sel_op_not, -<<<<<<< HEAD + in.avm_main_sel_op_cast, in.avm_main_sel_op_lt, in.avm_main_sel_op_lte, - in.avm_main_r_in_tag, -======= in.avm_main_alu_in_tag, ->>>>>>> a83ef175e (5466 - introduce in_tag dispatching to the ALU) in.avm_alu_clk, in.avm_alu_ia, in.avm_alu_ib, @@ -75,6 +72,7 @@ class perm_main_alu_permutation_settings { in.avm_alu_op_mul, in.avm_alu_op_eq, in.avm_alu_op_not, + in.avm_alu_op_cast, in.avm_alu_op_lt, in.avm_alu_op_lte, in.avm_alu_in_tag); @@ -113,13 +111,10 @@ class perm_main_alu_permutation_settings { in.avm_main_sel_op_mul, in.avm_main_sel_op_eq, in.avm_main_sel_op_not, -<<<<<<< HEAD + in.avm_main_sel_op_cast, in.avm_main_sel_op_lt, in.avm_main_sel_op_lte, - in.avm_main_r_in_tag, -======= in.avm_main_alu_in_tag, ->>>>>>> a83ef175e (5466 - introduce in_tag dispatching to the ALU) in.avm_alu_clk, in.avm_alu_ia, in.avm_alu_ib, @@ -129,6 +124,7 @@ class perm_main_alu_permutation_settings { in.avm_alu_op_mul, in.avm_alu_op_eq, in.avm_alu_op_not, + in.avm_alu_op_cast, in.avm_alu_op_lt, in.avm_alu_op_lte, in.avm_alu_in_tag); 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 9eeb7d0bc22..1523e0615f2 100644 --- a/barretenberg/cpp/src/barretenberg/vm/avm_trace/avm_trace.cpp +++ b/barretenberg/cpp/src/barretenberg/vm/avm_trace/avm_trace.cpp @@ -658,6 +658,7 @@ void AvmTraceBuilder::op_lt( main_trace.push_back(Row{ .avm_main_clk = clk, + .avm_main_alu_in_tag = FF(static_cast(in_tag)), .avm_main_ia = a, .avm_main_ib = b, .avm_main_ic = c, @@ -708,6 +709,7 @@ void AvmTraceBuilder::op_lte( main_trace.push_back(Row{ .avm_main_clk = clk, + .avm_main_alu_in_tag = FF(static_cast(in_tag)), .avm_main_ia = a, .avm_main_ib = b, .avm_main_ic = c, 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 5ffe3d319db..15cfb288a31 100644 --- a/barretenberg/cpp/src/barretenberg/vm/generated/avm_circuit_builder.hpp +++ b/barretenberg/cpp/src/barretenberg/vm/generated/avm_circuit_builder.hpp @@ -69,6 +69,7 @@ template struct AvmFullRow { FF avm_alu_ic{}; FF avm_alu_in_tag{}; FF avm_alu_op_add{}; + FF avm_alu_op_cast{}; FF avm_alu_op_div{}; FF avm_alu_op_eq{}; FF avm_alu_op_eq_diff_inv{}; @@ -271,6 +272,7 @@ template struct AvmFullRow { FF avm_alu_cmp_rng_ctr_shift{}; FF avm_alu_cmp_sel_shift{}; FF avm_alu_op_add_shift{}; + FF avm_alu_op_cast_shift{}; FF avm_alu_op_mul_shift{}; FF avm_alu_op_sub_shift{}; FF avm_alu_p_sub_a_hi_shift{}; @@ -311,13 +313,8 @@ class AvmCircuitBuilder { using Polynomial = Flavor::Polynomial; using ProverPolynomials = Flavor::ProverPolynomials; -<<<<<<< HEAD - static constexpr size_t num_fixed_columns = 246; - static constexpr size_t num_polys = 211; -======= - static constexpr size_t num_fixed_columns = 152; - static constexpr size_t num_polys = 133; ->>>>>>> a83ef175e (5466 - introduce in_tag dispatching to the ALU) + static constexpr size_t num_fixed_columns = 250; + static constexpr size_t num_polys = 214; std::vector rows; void set_trace(std::vector&& trace) { rows = std::move(trace); } @@ -351,6 +348,7 @@ class AvmCircuitBuilder { polys.avm_alu_ic[i] = rows[i].avm_alu_ic; polys.avm_alu_in_tag[i] = rows[i].avm_alu_in_tag; polys.avm_alu_op_add[i] = rows[i].avm_alu_op_add; + polys.avm_alu_op_cast[i] = rows[i].avm_alu_op_cast; polys.avm_alu_op_div[i] = rows[i].avm_alu_op_div; polys.avm_alu_op_eq[i] = rows[i].avm_alu_op_eq; polys.avm_alu_op_eq_diff_inv[i] = rows[i].avm_alu_op_eq_diff_inv; @@ -524,6 +522,7 @@ class AvmCircuitBuilder { 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_cast_shift = Polynomial(polys.avm_alu_op_cast.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()); diff --git a/barretenberg/cpp/src/barretenberg/vm/generated/avm_flavor.hpp b/barretenberg/cpp/src/barretenberg/vm/generated/avm_flavor.hpp index 673d0e59f37..a03e9a31976 100644 --- a/barretenberg/cpp/src/barretenberg/vm/generated/avm_flavor.hpp +++ b/barretenberg/cpp/src/barretenberg/vm/generated/avm_flavor.hpp @@ -69,12 +69,11 @@ class AvmFlavor { using RelationSeparator = FF; static constexpr size_t NUM_PRECOMPUTED_ENTITIES = 2; -<<<<<<< HEAD - static constexpr size_t NUM_WITNESS_ENTITIES = 209; + static constexpr size_t NUM_WITNESS_ENTITIES = 212; 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 = 246; + static constexpr size_t NUM_ALL_ENTITIES = 250; using GrandProductRelations = std::tuple, perm_main_bin_relation, @@ -107,13 +106,6 @@ class AvmFlavor { lookup_u16_12_relation, lookup_u16_13_relation, lookup_u16_14_relation>; -======= - static constexpr size_t NUM_WITNESS_ENTITIES = 131; - 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 = 152; ->>>>>>> a83ef175e (5466 - introduce in_tag dispatching to the ALU) using Relations = std::tuple, Avm_vm::avm_binary, @@ -199,6 +191,7 @@ class AvmFlavor { avm_alu_ic, avm_alu_in_tag, avm_alu_op_add, + avm_alu_op_cast, avm_alu_op_div, avm_alu_op_eq, avm_alu_op_eq_diff_inv, @@ -413,6 +406,7 @@ class AvmFlavor { avm_alu_ic, avm_alu_in_tag, avm_alu_op_add, + avm_alu_op_cast, avm_alu_op_div, avm_alu_op_eq, avm_alu_op_eq_diff_inv, @@ -632,6 +626,7 @@ class AvmFlavor { avm_alu_ic, avm_alu_in_tag, avm_alu_op_add, + avm_alu_op_cast, avm_alu_op_div, avm_alu_op_eq, avm_alu_op_eq_diff_inv, @@ -834,6 +829,7 @@ class AvmFlavor { avm_alu_cmp_rng_ctr_shift, avm_alu_cmp_sel_shift, avm_alu_op_add_shift, + avm_alu_op_cast_shift, avm_alu_op_mul_shift, avm_alu_op_sub_shift, avm_alu_p_sub_a_hi_shift, @@ -883,6 +879,7 @@ class AvmFlavor { avm_alu_ic, avm_alu_in_tag, avm_alu_op_add, + avm_alu_op_cast, avm_alu_op_div, avm_alu_op_eq, avm_alu_op_eq_diff_inv, @@ -1085,6 +1082,7 @@ class AvmFlavor { avm_alu_cmp_rng_ctr_shift, avm_alu_cmp_sel_shift, avm_alu_op_add_shift, + avm_alu_op_cast_shift, avm_alu_op_mul_shift, avm_alu_op_sub_shift, avm_alu_p_sub_a_hi_shift, @@ -1134,6 +1132,7 @@ class AvmFlavor { avm_alu_ic, avm_alu_in_tag, avm_alu_op_add, + avm_alu_op_cast, avm_alu_op_div, avm_alu_op_eq, avm_alu_op_eq_diff_inv, @@ -1332,44 +1331,80 @@ 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_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, + 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_cast, + 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_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, 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, - avm_main_pc_shift, avm_mem_addr_shift, - avm_mem_rw_shift, avm_mem_tag_shift, + 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_cmp_sel_shift, + avm_alu_op_add_shift, + avm_alu_op_cast_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, + 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, + avm_main_pc_shift, + avm_mem_addr_shift, + avm_mem_rw_shift, + avm_mem_tag_shift, avm_mem_val_shift }; }; }; @@ -1383,23 +1418,41 @@ 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_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, + 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_cast, + 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 }; }; @@ -1579,6 +1632,7 @@ class AvmFlavor { Base::avm_alu_ic = "AVM_ALU_IC"; Base::avm_alu_in_tag = "AVM_ALU_IN_TAG"; Base::avm_alu_op_add = "AVM_ALU_OP_ADD"; + Base::avm_alu_op_cast = "AVM_ALU_OP_CAST"; Base::avm_alu_op_div = "AVM_ALU_OP_DIV"; Base::avm_alu_op_eq = "AVM_ALU_OP_EQ"; Base::avm_alu_op_eq_diff_inv = "AVM_ALU_OP_EQ_DIFF_INV"; @@ -1809,6 +1863,7 @@ class AvmFlavor { Commitment avm_alu_ic; Commitment avm_alu_in_tag; Commitment avm_alu_op_add; + Commitment avm_alu_op_cast; Commitment avm_alu_op_div; Commitment avm_alu_op_eq; Commitment avm_alu_op_eq_diff_inv; @@ -2039,6 +2094,7 @@ class AvmFlavor { avm_alu_ic = deserialize_from_buffer(Transcript::proof_data, num_frs_read); avm_alu_in_tag = deserialize_from_buffer(Transcript::proof_data, num_frs_read); avm_alu_op_add = deserialize_from_buffer(Transcript::proof_data, num_frs_read); + avm_alu_op_cast = deserialize_from_buffer(Transcript::proof_data, num_frs_read); avm_alu_op_div = deserialize_from_buffer(Transcript::proof_data, num_frs_read); avm_alu_op_eq = deserialize_from_buffer(Transcript::proof_data, num_frs_read); avm_alu_op_eq_diff_inv = deserialize_from_buffer(Transcript::proof_data, num_frs_read); @@ -2274,6 +2330,7 @@ class AvmFlavor { serialize_to_buffer(avm_alu_ic, Transcript::proof_data); serialize_to_buffer(avm_alu_in_tag, Transcript::proof_data); serialize_to_buffer(avm_alu_op_add, Transcript::proof_data); + serialize_to_buffer(avm_alu_op_cast, Transcript::proof_data); serialize_to_buffer(avm_alu_op_div, Transcript::proof_data); serialize_to_buffer(avm_alu_op_eq, Transcript::proof_data); serialize_to_buffer(avm_alu_op_eq_diff_inv, 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 5c1cde78567..d8d367bbc65 100644 --- a/barretenberg/cpp/src/barretenberg/vm/generated/avm_prover.cpp +++ b/barretenberg/cpp/src/barretenberg/vm/generated/avm_prover.cpp @@ -75,6 +75,7 @@ void AvmProver::execute_wire_commitments_round() witness_commitments.avm_alu_ic = commitment_key->commit(key->avm_alu_ic); witness_commitments.avm_alu_in_tag = commitment_key->commit(key->avm_alu_in_tag); witness_commitments.avm_alu_op_add = commitment_key->commit(key->avm_alu_op_add); + witness_commitments.avm_alu_op_cast = commitment_key->commit(key->avm_alu_op_cast); witness_commitments.avm_alu_op_div = commitment_key->commit(key->avm_alu_op_div); witness_commitments.avm_alu_op_eq = commitment_key->commit(key->avm_alu_op_eq); witness_commitments.avm_alu_op_eq_diff_inv = commitment_key->commit(key->avm_alu_op_eq_diff_inv); @@ -136,6 +137,7 @@ void AvmProver::execute_wire_commitments_round() witness_commitments.avm_byte_lookup_table_input_b = commitment_key->commit(key->avm_byte_lookup_table_input_b); witness_commitments.avm_byte_lookup_table_op_id = commitment_key->commit(key->avm_byte_lookup_table_op_id); witness_commitments.avm_byte_lookup_table_output = commitment_key->commit(key->avm_byte_lookup_table_output); + witness_commitments.avm_main_alu_in_tag = commitment_key->commit(key->avm_main_alu_in_tag); witness_commitments.avm_main_alu_sel = commitment_key->commit(key->avm_main_alu_sel); witness_commitments.avm_main_bin_op_id = commitment_key->commit(key->avm_main_bin_op_id); witness_commitments.avm_main_bin_sel = commitment_key->commit(key->avm_main_bin_sel); @@ -180,6 +182,7 @@ void AvmProver::execute_wire_commitments_round() witness_commitments.avm_main_sel_mov_b = commitment_key->commit(key->avm_main_sel_mov_b); witness_commitments.avm_main_sel_op_add = commitment_key->commit(key->avm_main_sel_op_add); witness_commitments.avm_main_sel_op_and = commitment_key->commit(key->avm_main_sel_op_and); + witness_commitments.avm_main_sel_op_cast = commitment_key->commit(key->avm_main_sel_op_cast); witness_commitments.avm_main_sel_op_div = commitment_key->commit(key->avm_main_sel_op_div); witness_commitments.avm_main_sel_op_eq = commitment_key->commit(key->avm_main_sel_op_eq); witness_commitments.avm_main_sel_op_lt = commitment_key->commit(key->avm_main_sel_op_lt); @@ -256,6 +259,7 @@ void AvmProver::execute_wire_commitments_round() transcript->send_to_verifier(commitment_labels.avm_alu_ic, witness_commitments.avm_alu_ic); transcript->send_to_verifier(commitment_labels.avm_alu_in_tag, witness_commitments.avm_alu_in_tag); transcript->send_to_verifier(commitment_labels.avm_alu_op_add, witness_commitments.avm_alu_op_add); + transcript->send_to_verifier(commitment_labels.avm_alu_op_cast, witness_commitments.avm_alu_op_cast); transcript->send_to_verifier(commitment_labels.avm_alu_op_div, witness_commitments.avm_alu_op_div); transcript->send_to_verifier(commitment_labels.avm_alu_op_eq, witness_commitments.avm_alu_op_eq); transcript->send_to_verifier(commitment_labels.avm_alu_op_eq_diff_inv, witness_commitments.avm_alu_op_eq_diff_inv); @@ -325,6 +329,7 @@ void AvmProver::execute_wire_commitments_round() witness_commitments.avm_byte_lookup_table_op_id); transcript->send_to_verifier(commitment_labels.avm_byte_lookup_table_output, witness_commitments.avm_byte_lookup_table_output); + transcript->send_to_verifier(commitment_labels.avm_main_alu_in_tag, witness_commitments.avm_main_alu_in_tag); transcript->send_to_verifier(commitment_labels.avm_main_alu_sel, witness_commitments.avm_main_alu_sel); transcript->send_to_verifier(commitment_labels.avm_main_bin_op_id, witness_commitments.avm_main_bin_op_id); transcript->send_to_verifier(commitment_labels.avm_main_bin_sel, witness_commitments.avm_main_bin_sel); @@ -372,6 +377,7 @@ void AvmProver::execute_wire_commitments_round() transcript->send_to_verifier(commitment_labels.avm_main_sel_mov_b, witness_commitments.avm_main_sel_mov_b); transcript->send_to_verifier(commitment_labels.avm_main_sel_op_add, witness_commitments.avm_main_sel_op_add); transcript->send_to_verifier(commitment_labels.avm_main_sel_op_and, witness_commitments.avm_main_sel_op_and); + transcript->send_to_verifier(commitment_labels.avm_main_sel_op_cast, witness_commitments.avm_main_sel_op_cast); transcript->send_to_verifier(commitment_labels.avm_main_sel_op_div, witness_commitments.avm_main_sel_op_div); transcript->send_to_verifier(commitment_labels.avm_main_sel_op_eq, witness_commitments.avm_main_sel_op_eq); transcript->send_to_verifier(commitment_labels.avm_main_sel_op_lt, witness_commitments.avm_main_sel_op_lt); diff --git a/barretenberg/cpp/src/barretenberg/vm/generated/avm_verifier.cpp b/barretenberg/cpp/src/barretenberg/vm/generated/avm_verifier.cpp index 116deb5058c..435e6c7ae9f 100644 --- a/barretenberg/cpp/src/barretenberg/vm/generated/avm_verifier.cpp +++ b/barretenberg/cpp/src/barretenberg/vm/generated/avm_verifier.cpp @@ -70,6 +70,8 @@ bool AvmVerifier::verify_proof(const HonkProof& proof) commitments.avm_alu_ic = transcript->template receive_from_prover(commitment_labels.avm_alu_ic); commitments.avm_alu_in_tag = transcript->template receive_from_prover(commitment_labels.avm_alu_in_tag); commitments.avm_alu_op_add = transcript->template receive_from_prover(commitment_labels.avm_alu_op_add); + commitments.avm_alu_op_cast = + transcript->template receive_from_prover(commitment_labels.avm_alu_op_cast); commitments.avm_alu_op_div = transcript->template receive_from_prover(commitment_labels.avm_alu_op_div); commitments.avm_alu_op_eq = transcript->template receive_from_prover(commitment_labels.avm_alu_op_eq); commitments.avm_alu_op_eq_diff_inv = From b41dc1a7bf9256d823f17cf5965a151ee7c1c1fd Mon Sep 17 00:00:00 2001 From: jeanmon Date: Wed, 17 Apr 2024 09:28:07 +0000 Subject: [PATCH 3/8] 5466: witness generation and PIL modifications --- barretenberg/cpp/pil/avm/avm_alu.pil | 64 +++-- .../ecc/fields/field_declarations.hpp | 12 + .../relations/generated/avm/avm_alu.hpp | 257 +++++++++++------- .../relations/generated/avm/declare_views.hpp | 2 + .../vm/avm_trace/avm_alu_trace.cpp | 88 +++++- .../vm/avm_trace/avm_alu_trace.hpp | 7 +- .../vm/avm_trace/avm_mem_trace.cpp | 10 +- .../vm/avm_trace/avm_mem_trace.hpp | 2 +- .../barretenberg/vm/avm_trace/avm_trace.cpp | 88 +++++- .../barretenberg/vm/avm_trace/avm_trace.hpp | 4 + .../vm/generated/avm_circuit_builder.hpp | 8 +- .../barretenberg/vm/generated/avm_flavor.hpp | 156 ++++------- .../barretenberg/vm/generated/avm_prover.cpp | 2 + .../vm/generated/avm_verifier.cpp | 2 + 14 files changed, 449 insertions(+), 253 deletions(-) diff --git a/barretenberg/cpp/pil/avm/avm_alu.pil b/barretenberg/cpp/pil/avm/avm_alu.pil index 96a00f74cb3..2150542e686 100644 --- a/barretenberg/cpp/pil/avm/avm_alu.pil +++ b/barretenberg/cpp/pil/avm/avm_alu.pil @@ -18,11 +18,12 @@ namespace avm_alu(256); pol commit op_not; pol commit op_eq; pol commit op_cast; + pol commit op_cast_prev; // Predicate on whether op_cast is enabled at previous row pol commit alu_sel; // Predicate to activate the copy of intermediate registers to ALU table. pol commit op_lt; pol commit op_lte; pol commit cmp_sel; // Predicate if LT or LTE is set - pol commit rng_chk_sel; // Predicate representing a range check row. + pol commit rng_chk_sel; // Predicate representing a range check row used in LT/LTE. // Instruction tag (1: u8, 2: u16, 3: u32, 4: u64, 5: u128, 6: field) copied from Main table pol commit in_tag; @@ -266,20 +267,6 @@ namespace avm_alu(256); #[ALU_OP_EQ] op_eq * (DIFF * (ic * (1 - op_eq_diff_inv) + op_eq_diff_inv) - 1 + ic) = 0; - // ========= CAST Operation Constraints =============================== - // We handle the input ia independently of its tag, i.e., we suppose it can take - // any value between 0 and p-1. - // We decompose the input ia in 8-bit/16-bit limbs and prove that the decomposition - // sums up to ia over the integers (i.e., no modulo p wrapping). To prove this, - // we perform a "school subtraction" (borrowing) over 128-bit limbs. - // The input I is written I = I_l + I_h * 2^128 and the field order P = P_l + P_h * 2^128. - // The school subtraction result is D = D_l + D_h * 2^128 and we prove the correctness - // through: P_l - I_l - CF * 2^128 == D_l AND P_h - I_h + CF == D_h - // where CF is a carry/borrowing bit. CF == 1 <==> P_l < I_l. - - #[ALU_OP_CAST] - op_cast * (SUM_TAG + ff_tag * ia - ic) = 0; - // ========= LT/LTE Operation Constraints =============================== // There are two routines that we utilise as part of this LT/LTE check // (1) Decomposition into two 128-bit limbs, lo and hi respectively and a borrow (1 or 0); @@ -447,15 +434,15 @@ namespace avm_alu(256); cmp_rng_ctr * ((1 - rng_chk_sel) * (1 - op_eq_diff_inv) + op_eq_diff_inv) - rng_chk_sel = 0; // We perform a range check if we have some range checks remaining or we are performing a comparison op - pol RNG_CHK_OP = rng_chk_sel + cmp_sel; + pol RNG_CHK_OP = rng_chk_sel + cmp_sel + op_cast + op_cast_prev; pol commit rng_chk_lookup_selector; #[RNG_CHK_LOOKUP_SELECTOR] - rng_chk_lookup_selector' = cmp_sel' + rng_chk_sel' + op_add' + op_sub' + op_mul' + op_mul * u128_tag + op_cast'; + rng_chk_lookup_selector' = cmp_sel' + rng_chk_sel' + op_add' + op_sub' + op_mul' + op_mul * u128_tag + op_cast' + op_cast_prev'; // Perform 128-bit range check on lo part #[LOWER_CMP_RNG_CHK] - a_lo = SUM_128 * (RNG_CHK_OP + op_cast); + a_lo = SUM_128 * RNG_CHK_OP; // Perform 128-bit range check on hi part #[UPPER_CMP_RNG_CHK] @@ -482,3 +469,44 @@ namespace avm_alu(256); (p_sub_b_lo' - res_lo) * rng_chk_sel'= 0; (p_sub_b_hi' - res_hi) * rng_chk_sel'= 0; + + // ========= CAST Operation Constraints =============================== + // We handle the input ia independently of its tag, i.e., we suppose it can take + // any value between 0 and p-1. + // We decompose the input ia in 8-bit/16-bit limbs and prove that the decomposition + // sums up to ia over the integers (i.e., no modulo p wrapping). To prove this, we + // re-use techniques above from LT/LTE opcode. The following relations are toggled for CAST: + // - #[INPUT_DECOMP_1] shows a = a_lo + 2 ** 128 * a_hi + // - #[SUB_LO_1] and #[SUB_LO_1] shows that the above does not overflow modulo p. + // - We toggle RNG_CHK_OP with op_cast to show that a_lo, a_hi are correctly decomposed + // over the 8/16-bit ALU registers in #[LOWER_CMP_RNG_CHK] and #[UPPER_CMP_RNG_CHK]. + // - The 128-bit range checks for a_lo, a_hi are activated in #[RNG_CHK_LOOKUP_SELECTOR]. + // - We copy p_sub_a_lo resp. p_sub_a_hi into next row in columns a_lo resp. a_hi so + // that decomposition into the 8/16-bit ALU registers and range checks are performed. + // Copy is done in #[OP_CAST_RNG_CHECK_P_SUB_A_LOW/HIGH] below. + // Activation of decomposition and range check is achieved by adding op_cast_prev in + // #[LOWER_CMP_RNG_CHK], #[UPPER_CMP_RNG_CHK] and #[RNG_CHK_LOOKUP_SELECTOR]. + // - Finally, the truncated result SUM_TAG is copied in ic as part of #[ALU_OP_CAST] below. + // - Note that the tag of return value must be constrained to be in_tag and is enforced in + // the main and memory traces. + // + // TODO: Potential optimization is to un-toggle all CAST relevant operations when ff_tag is + // enabled. In this case, ic = ia trivially. + // Another one is to activate range checks in a more granular way depending on the tag. + + #[OP_CAST_PREV_LINE] + op_cast_prev' = op_cast; + + // TODO: If a lookup selector with value > 1 is enabled, then we do not need this constraint. + // Otherwise, melding two op_cast with a common row might lead to disabling + #[OP_CAST_PREV_MUT_EXCL] + op_cast_prev * op_cast = 0; + + #[ALU_OP_CAST] + op_cast * (SUM_TAG + ff_tag * ia - ic) = 0; + + #[OP_CAST_RNG_CHECK_P_SUB_A_LOW] + op_cast * (a_lo' - p_sub_a_lo) = 0; + + #[OP_CAST_RNG_CHECK_P_SUB_A_HIGH] + op_cast * (a_hi' - p_sub_a_hi) = 0; \ No newline at end of file diff --git a/barretenberg/cpp/src/barretenberg/ecc/fields/field_declarations.hpp b/barretenberg/cpp/src/barretenberg/ecc/fields/field_declarations.hpp index 87a10938677..35805403cde 100644 --- a/barretenberg/cpp/src/barretenberg/ecc/fields/field_declarations.hpp +++ b/barretenberg/cpp/src/barretenberg/ecc/fields/field_declarations.hpp @@ -119,6 +119,18 @@ template struct alignas(32) field { return static_cast(out.data[0]); } + constexpr explicit operator uint8_t() const + { + field out = from_montgomery_form(); + return static_cast(out.data[0]); + } + + constexpr explicit operator uint16_t() const + { + field out = from_montgomery_form(); + return static_cast(out.data[0]); + } + constexpr explicit operator uint32_t() const { field out = from_montgomery_form(); 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 2ba5ef845e7..ea21fba5789 100644 --- a/barretenberg/cpp/src/barretenberg/relations/generated/avm/avm_alu.hpp +++ b/barretenberg/cpp/src/barretenberg/relations/generated/avm/avm_alu.hpp @@ -30,6 +30,8 @@ template struct Avm_aluRow { FF avm_alu_op_add{}; FF avm_alu_op_add_shift{}; FF avm_alu_op_cast{}; + FF avm_alu_op_cast_prev{}; + FF avm_alu_op_cast_prev_shift{}; FF avm_alu_op_cast_shift{}; FF avm_alu_op_eq{}; FF avm_alu_op_eq_diff_inv{}; @@ -122,61 +124,73 @@ inline std::string get_relation_label_avm_alu(int index) return "ALU_OP_EQ"; case 23: - return "ALU_OP_CAST"; - - case 24: return "INPUT_DECOMP_1"; - case 25: + case 24: return "INPUT_DECOMP_2"; - case 27: + case 26: return "SUB_LO_1"; - case 28: + case 27: return "SUB_HI_1"; - case 30: + case 29: return "SUB_LO_2"; - case 31: + case 30: return "SUB_HI_2"; - case 32: + case 31: return "RES_LO"; - case 33: + case 32: return "RES_HI"; - case 34: + case 33: return "CMP_CTR_REL_1"; - case 35: + case 34: return "CMP_CTR_REL_2"; - case 38: + case 37: return "CTR_NON_ZERO_REL"; - case 39: + case 38: return "RNG_CHK_LOOKUP_SELECTOR"; - case 40: + case 39: return "LOWER_CMP_RNG_CHK"; - case 41: + case 40: return "UPPER_CMP_RNG_CHK"; - case 42: + case 41: return "SHIFT_RELS_0"; - case 44: + case 43: return "SHIFT_RELS_1"; - case 46: + case 45: return "SHIFT_RELS_2"; - case 48: + case 47: return "SHIFT_RELS_3"; + + case 49: + return "OP_CAST_PREV_LINE"; + + case 50: + return "OP_CAST_PREV_MUT_EXCL"; + + case 51: + return "ALU_OP_CAST"; + + case 52: + return "OP_CAST_RNG_CHECK_P_SUB_A_LOW"; + + case 53: + return "OP_CAST_RNG_CHECK_P_SUB_A_HIGH"; } return std::to_string(index); } @@ -185,9 +199,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, 3, 4, 5, 5, 5, 5, 6, 6, 8, 3, 4, 4, 5, 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, + 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, 2, 3, 5, 3, 3, }; template @@ -484,25 +498,9 @@ template class avm_aluImpl { { Avm_DECLARE_VIEWS(23); - auto tmp = - (avm_alu_op_cast * - (((((((avm_alu_u8_tag * avm_alu_u8_r0) + - (avm_alu_u16_tag * (avm_alu_u8_r0 + (avm_alu_u8_r1 * FF(256))))) + - (avm_alu_u32_tag * - ((avm_alu_u8_r0 + (avm_alu_u8_r1 * FF(256))) + (avm_alu_u16_r0 * FF(65536))))) + - (avm_alu_u64_tag * ((((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_u128_tag * - ((((((((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 * FF(uint256_t{ 0UL, 1UL, 0UL, 0UL }))) + - (avm_alu_u16_r4 * FF(uint256_t{ 0UL, 65536UL, 0UL, 0UL }))) + - (avm_alu_u16_r5 * FF(uint256_t{ 0UL, 4294967296UL, 0UL, 0UL }))) + - (avm_alu_u16_r6 * FF(uint256_t{ 0UL, 281474976710656UL, 0UL, 0UL }))))) + - (avm_alu_ff_tag * avm_alu_ia)) - - avm_alu_ic)); + auto tmp = (((avm_alu_op_lt * avm_alu_ib) + ((avm_alu_op_lte + avm_alu_op_cast) * avm_alu_ia)) - + ((avm_alu_a_lo + (avm_alu_a_hi * FF(uint256_t{ 0UL, 0UL, 1UL, 0UL }))) * + (avm_alu_cmp_sel + avm_alu_op_cast))); tmp *= scaling_factor; std::get<23>(evals) += tmp; } @@ -510,9 +508,8 @@ template class avm_aluImpl { { Avm_DECLARE_VIEWS(24); - auto tmp = (((avm_alu_op_lt * avm_alu_ib) + ((avm_alu_op_lte + avm_alu_op_cast) * avm_alu_ia)) - - ((avm_alu_a_lo + (avm_alu_a_hi * FF(uint256_t{ 0UL, 0UL, 1UL, 0UL }))) * - (avm_alu_cmp_sel + avm_alu_op_cast))); + 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; } @@ -520,8 +517,7 @@ template class avm_aluImpl { { Avm_DECLARE_VIEWS(25); - 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_p_a_borrow * (-avm_alu_p_a_borrow + FF(1))); tmp *= scaling_factor; std::get<25>(evals) += tmp; } @@ -529,7 +525,10 @@ template class avm_aluImpl { { Avm_DECLARE_VIEWS(26); - auto tmp = (avm_alu_p_a_borrow * (-avm_alu_p_a_borrow + FF(1))); + 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 + avm_alu_op_cast)); tmp *= scaling_factor; std::get<26>(evals) += tmp; } @@ -537,9 +536,9 @@ template class avm_aluImpl { { Avm_DECLARE_VIEWS(27); - 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 })))) * + 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 + avm_alu_op_cast)); tmp *= scaling_factor; std::get<27>(evals) += tmp; @@ -548,10 +547,7 @@ template class avm_aluImpl { { Avm_DECLARE_VIEWS(28); - 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 + avm_alu_op_cast)); + auto tmp = (avm_alu_p_b_borrow * (-avm_alu_p_b_borrow + FF(1))); tmp *= scaling_factor; std::get<28>(evals) += tmp; } @@ -559,35 +555,27 @@ template class avm_aluImpl { { Avm_DECLARE_VIEWS(29); - auto tmp = (avm_alu_p_b_borrow * (-avm_alu_p_b_borrow + FF(1))); - tmp *= scaling_factor; - std::get<29>(evals) += tmp; - } - // Contribution 30 - { - Avm_DECLARE_VIEWS(30); - 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<30>(evals) += tmp; + std::get<29>(evals) += tmp; } - // Contribution 31 + // Contribution 30 { - Avm_DECLARE_VIEWS(31); + 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<31>(evals) += tmp; + std::get<30>(evals) += tmp; } - // Contribution 32 + // Contribution 31 { - Avm_DECLARE_VIEWS(32); + Avm_DECLARE_VIEWS(31); auto tmp = ((avm_alu_res_lo - @@ -597,11 +585,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<32>(evals) += tmp; + std::get<31>(evals) += tmp; } - // Contribution 33 + // Contribution 32 { - Avm_DECLARE_VIEWS(33); + Avm_DECLARE_VIEWS(32); auto tmp = ((avm_alu_res_hi - ((((avm_alu_a_hi - avm_alu_b_hi) - avm_alu_borrow) * @@ -610,13 +598,21 @@ 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<32>(evals) += tmp; + } + // Contribution 33 + { + Avm_DECLARE_VIEWS(33); + + 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; } // Contribution 34 { Avm_DECLARE_VIEWS(34); - auto tmp = (((avm_alu_cmp_rng_ctr_shift - avm_alu_cmp_rng_ctr) + FF(1)) * avm_alu_cmp_rng_ctr); + auto tmp = ((avm_alu_cmp_rng_ctr_shift - FF(4)) * avm_alu_cmp_sel); tmp *= scaling_factor; std::get<34>(evals) += tmp; } @@ -624,7 +620,7 @@ template class avm_aluImpl { { Avm_DECLARE_VIEWS(35); - auto tmp = ((avm_alu_cmp_rng_ctr_shift - FF(4)) * 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; } @@ -632,7 +628,7 @@ template class avm_aluImpl { { Avm_DECLARE_VIEWS(36); - auto tmp = (avm_alu_rng_chk_sel * (-avm_alu_rng_chk_sel + FF(1))); + auto tmp = (avm_alu_rng_chk_sel * avm_alu_cmp_sel); tmp *= scaling_factor; std::get<36>(evals) += tmp; } @@ -640,7 +636,9 @@ template class avm_aluImpl { { Avm_DECLARE_VIEWS(37); - auto tmp = (avm_alu_rng_chk_sel * avm_alu_cmp_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; } @@ -648,9 +646,13 @@ template class avm_aluImpl { { Avm_DECLARE_VIEWS(38); - 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_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)) + + avm_alu_op_cast_shift) + + avm_alu_op_cast_prev_shift)); tmp *= scaling_factor; std::get<38>(evals) += tmp; } @@ -658,19 +660,6 @@ template class avm_aluImpl { { Avm_DECLARE_VIEWS(39); - 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)) + - avm_alu_op_cast_shift)); - tmp *= scaling_factor; - std::get<39>(evals) += tmp; - } - // Contribution 40 - { - Avm_DECLARE_VIEWS(40); - 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))) + @@ -679,13 +668,13 @@ template class avm_aluImpl { (avm_alu_u16_r4 * FF(uint256_t{ 0UL, 65536UL, 0UL, 0UL }))) + (avm_alu_u16_r5 * FF(uint256_t{ 0UL, 4294967296UL, 0UL, 0UL }))) + (avm_alu_u16_r6 * FF(uint256_t{ 0UL, 281474976710656UL, 0UL, 0UL }))) * - ((avm_alu_rng_chk_sel + avm_alu_cmp_sel) + avm_alu_op_cast))); + (((avm_alu_rng_chk_sel + avm_alu_cmp_sel) + avm_alu_op_cast) + avm_alu_op_cast_prev))); tmp *= scaling_factor; - std::get<40>(evals) += tmp; + std::get<39>(evals) += tmp; } - // Contribution 41 + // Contribution 40 { - Avm_DECLARE_VIEWS(41); + 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))) + @@ -694,7 +683,15 @@ template class avm_aluImpl { (avm_alu_u16_r12 * FF(uint256_t{ 0UL, 65536UL, 0UL, 0UL }))) + (avm_alu_u16_r13 * FF(uint256_t{ 0UL, 4294967296UL, 0UL, 0UL }))) + (avm_alu_u16_r14 * FF(uint256_t{ 0UL, 281474976710656UL, 0UL, 0UL }))) * - (avm_alu_rng_chk_sel + avm_alu_cmp_sel))); + (((avm_alu_rng_chk_sel + avm_alu_cmp_sel) + avm_alu_op_cast) + avm_alu_op_cast_prev))); + tmp *= scaling_factor; + std::get<40>(evals) += tmp; + } + // Contribution 41 + { + Avm_DECLARE_VIEWS(41); + + 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; } @@ -702,7 +699,7 @@ template class avm_aluImpl { { Avm_DECLARE_VIEWS(42); - auto tmp = ((avm_alu_a_lo_shift - avm_alu_b_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; } @@ -710,7 +707,7 @@ template class avm_aluImpl { { Avm_DECLARE_VIEWS(43); - auto tmp = ((avm_alu_a_hi_shift - avm_alu_b_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; } @@ -718,7 +715,7 @@ template class avm_aluImpl { { Avm_DECLARE_VIEWS(44); - auto tmp = ((avm_alu_b_lo_shift - avm_alu_p_sub_a_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; } @@ -726,7 +723,7 @@ template class avm_aluImpl { { Avm_DECLARE_VIEWS(45); - auto tmp = ((avm_alu_b_hi_shift - avm_alu_p_sub_a_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; } @@ -734,7 +731,7 @@ template class avm_aluImpl { { Avm_DECLARE_VIEWS(46); - 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_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; } @@ -742,7 +739,7 @@ template class avm_aluImpl { { Avm_DECLARE_VIEWS(47); - 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_b_lo_shift - avm_alu_res_lo) * avm_alu_rng_chk_sel_shift); tmp *= scaling_factor; std::get<47>(evals) += tmp; } @@ -750,7 +747,7 @@ template class avm_aluImpl { { Avm_DECLARE_VIEWS(48); - 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_b_hi_shift - avm_alu_res_hi) * avm_alu_rng_chk_sel_shift); tmp *= scaling_factor; std::get<48>(evals) += tmp; } @@ -758,10 +755,60 @@ template class avm_aluImpl { { Avm_DECLARE_VIEWS(49); - auto tmp = ((avm_alu_p_sub_b_hi_shift - avm_alu_res_hi) * avm_alu_rng_chk_sel_shift); + auto tmp = (avm_alu_op_cast_prev_shift - avm_alu_op_cast); tmp *= scaling_factor; std::get<49>(evals) += tmp; } + // Contribution 50 + { + Avm_DECLARE_VIEWS(50); + + auto tmp = (avm_alu_op_cast_prev * avm_alu_op_cast); + tmp *= scaling_factor; + std::get<50>(evals) += tmp; + } + // Contribution 51 + { + Avm_DECLARE_VIEWS(51); + + auto tmp = + (avm_alu_op_cast * + (((((((avm_alu_u8_tag * avm_alu_u8_r0) + + (avm_alu_u16_tag * (avm_alu_u8_r0 + (avm_alu_u8_r1 * FF(256))))) + + (avm_alu_u32_tag * + ((avm_alu_u8_r0 + (avm_alu_u8_r1 * FF(256))) + (avm_alu_u16_r0 * FF(65536))))) + + (avm_alu_u64_tag * ((((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_u128_tag * + ((((((((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 * FF(uint256_t{ 0UL, 1UL, 0UL, 0UL }))) + + (avm_alu_u16_r4 * FF(uint256_t{ 0UL, 65536UL, 0UL, 0UL }))) + + (avm_alu_u16_r5 * FF(uint256_t{ 0UL, 4294967296UL, 0UL, 0UL }))) + + (avm_alu_u16_r6 * FF(uint256_t{ 0UL, 281474976710656UL, 0UL, 0UL }))))) + + (avm_alu_ff_tag * avm_alu_ia)) - + avm_alu_ic)); + tmp *= scaling_factor; + std::get<51>(evals) += tmp; + } + // Contribution 52 + { + Avm_DECLARE_VIEWS(52); + + auto tmp = (avm_alu_op_cast * (avm_alu_a_lo_shift - avm_alu_p_sub_a_lo)); + tmp *= scaling_factor; + std::get<52>(evals) += tmp; + } + // Contribution 53 + { + Avm_DECLARE_VIEWS(53); + + auto tmp = (avm_alu_op_cast * (avm_alu_a_hi_shift - avm_alu_p_sub_a_hi)); + tmp *= scaling_factor; + std::get<53>(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 398fbe9840d..5531e8131b0 100644 --- a/barretenberg/cpp/src/barretenberg/relations/generated/avm/declare_views.hpp +++ b/barretenberg/cpp/src/barretenberg/relations/generated/avm/declare_views.hpp @@ -21,6 +21,7 @@ [[maybe_unused]] auto avm_alu_in_tag = View(new_term.avm_alu_in_tag); \ [[maybe_unused]] auto avm_alu_op_add = View(new_term.avm_alu_op_add); \ [[maybe_unused]] auto avm_alu_op_cast = View(new_term.avm_alu_op_cast); \ + [[maybe_unused]] auto avm_alu_op_cast_prev = View(new_term.avm_alu_op_cast_prev); \ [[maybe_unused]] auto avm_alu_op_div = View(new_term.avm_alu_op_div); \ [[maybe_unused]] auto avm_alu_op_eq = View(new_term.avm_alu_op_eq); \ [[maybe_unused]] auto avm_alu_op_eq_diff_inv = View(new_term.avm_alu_op_eq_diff_inv); \ @@ -223,6 +224,7 @@ [[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_cast_prev_shift = View(new_term.avm_alu_op_cast_prev_shift); \ [[maybe_unused]] auto avm_alu_op_cast_shift = View(new_term.avm_alu_op_cast_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); \ 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 f92dcb2668d..aceae2e2072 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 @@ -1,12 +1,4 @@ #include "avm_alu_trace.hpp" -#include "barretenberg/common/serialize.hpp" -#include "barretenberg/numeric/uint128/uint128.hpp" -#include "barretenberg/numeric/uint256/uint256.hpp" -#include "barretenberg/relations/generated/avm/avm_alu.hpp" -#include -#include -#include -#include namespace bb::avm_trace { @@ -608,7 +600,7 @@ FF AvmAluTraceBuilder::op_lt(FF const& a, FF const& b, AvmMemoryTag in_tag, uint std::vector rows = cmp_range_check_helper(row, hi_lo_limbs); // Append the rows to the alu_trace alu_trace.insert(alu_trace.end(), rows.begin(), rows.end()); - return { static_cast(c) }; + return FF{ static_cast(c) }; } /** @@ -662,6 +654,82 @@ FF AvmAluTraceBuilder::op_lte(FF const& a, FF const& b, AvmMemoryTag in_tag, uin // Update the row and add new rows with the correct hi_lo limbs std::vector rows = cmp_range_check_helper(row, hi_lo_limbs); alu_trace.insert(alu_trace.end(), rows.begin(), rows.end()); - return { static_cast(c) }; + return FF{ static_cast(c) }; } + +/** + * @brief Build ALU trace for the CAST opcode. + * + * @param a Input value to be casted. Tag of the input is not taken into account. + * @param in_tag Tag specifying the type for the input to be casted into. + * @param clk Clock referring to the operation in the main trace. + * @return The casted value as a finite field element. + */ +FF AvmAluTraceBuilder::op_cast(FF const& a, AvmMemoryTag in_tag, uint32_t clk) +{ + uint256_t a_256{ a }; + // Get the decomposition of a + auto [a_lo, a_hi] = decompose(a_256); + // Decomposition of p-a + auto [p_sub_a_lo, p_sub_a_hi, p_a_borrow] = gt_witness(FF::modulus, a_256); + auto [u8_r0, u8_r1, u16_reg] = to_alu_slice_registers(a_256); + + alu_trace.push_back(AvmAluTraceBuilder::AluTraceEntry{ + .alu_clk = clk, + .alu_op_cast = true, + .alu_ff_tag = in_tag == AvmMemoryTag::FF, + .alu_u8_tag = in_tag == AvmMemoryTag::U8, + .alu_u16_tag = in_tag == AvmMemoryTag::U16, + .alu_u32_tag = in_tag == AvmMemoryTag::U32, + .alu_u64_tag = in_tag == AvmMemoryTag::U64, + .alu_u128_tag = in_tag == AvmMemoryTag::U128, + .alu_ia = a, + .alu_ic = 0, + .alu_u8_r0 = u8_r0, + .alu_u8_r1 = u8_r1, + .alu_u16_reg = u16_reg, + .hi_lo_limbs = { a_lo, a_hi, p_sub_a_lo, p_sub_a_hi }, + .p_a_borrow = p_a_borrow, + }); + + uint256_t sub = (p_sub_a_hi << 128) + p_sub_a_lo; + auto [sub_u8_r0, sub_u8_r1, sub_u16_reg] = to_alu_slice_registers(sub); + + alu_trace.push_back(AvmAluTraceBuilder::AluTraceEntry{ + .alu_op_cast_prev = true, + .alu_u8_r0 = sub_u8_r0, + .alu_u8_r1 = sub_u8_r1, + .alu_u16_reg = sub_u16_reg, + .hi_lo_limbs = { p_sub_a_lo, p_sub_a_hi }, + }); + + FF c; + + switch (in_tag) { + case AvmMemoryTag::U8: + c = FF(uint8_t(a)); + break; + case AvmMemoryTag::U16: + c = FF(uint16_t(a)); + break; + case AvmMemoryTag::U32: + c = FF(uint32_t(a)); + break; + case AvmMemoryTag::U64: + c = FF(uint64_t(a)); + break; + case AvmMemoryTag::U128: + c = FF(uint256_t::from_uint128(uint128_t(a))); + break; + case AvmMemoryTag::FF: + c = a; + break; + default: + c = 0; + break; + } + + return c; +} + } // namespace bb::avm_trace 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 cb12ab925ed..7920aabd28e 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 @@ -1,10 +1,6 @@ #pragma once #include "avm_common.hpp" -#include "barretenberg/numeric/uint128/uint128.hpp" -#include "barretenberg/numeric/uint256/uint256.hpp" -#include -#include namespace bb::avm_trace { @@ -21,6 +17,8 @@ class AvmAluTraceBuilder { bool alu_op_eq = false; bool alu_op_lt = false; bool alu_op_lte = false; + bool alu_op_cast = false; + bool alu_op_cast_prev = false; bool alu_ff_tag = false; bool alu_u8_tag = false; @@ -66,6 +64,7 @@ class AvmAluTraceBuilder { FF op_eq(FF const& a, FF const& b, AvmMemoryTag in_tag, uint32_t clk); 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); + FF op_cast(FF const& a, AvmMemoryTag in_tag, uint32_t clk); bool is_range_check_required() const; diff --git a/barretenberg/cpp/src/barretenberg/vm/avm_trace/avm_mem_trace.cpp b/barretenberg/cpp/src/barretenberg/vm/avm_trace/avm_mem_trace.cpp index 00b7b0bc1a6..28806c4421c 100644 --- a/barretenberg/cpp/src/barretenberg/vm/avm_trace/avm_mem_trace.cpp +++ b/barretenberg/cpp/src/barretenberg/vm/avm_trace/avm_mem_trace.cpp @@ -179,10 +179,10 @@ void AvmMemTraceBuilder::store_in_mem_trace( } /** - * @brief Handle a read memory operation specific to MOV opcode. Load the corresponding + * @brief Handle a read memory operation without any tag check. Load the corresponding * value to the intermediate register ia. A memory trace entry for the load * operation is added. It is permissive in the sense that we do not enforce tag - * matching with against any instruction tag. In addition, the specific selector + * matching with against any instruction tag. Optionally, a specific selector * for MOV opcode is enabled. * * @param clk Main clock @@ -191,7 +191,9 @@ void AvmMemTraceBuilder::store_in_mem_trace( * @return Result of the read operation containing the value and the tag of the memory cell * at the supplied address. */ -AvmMemTraceBuilder::MemEntry AvmMemTraceBuilder::read_and_load_mov_opcode(uint32_t const clk, uint32_t const addr) +AvmMemTraceBuilder::MemEntry AvmMemTraceBuilder::read_and_load_no_tag_check(uint32_t const clk, + uint32_t const addr, + bool is_mov) { MemEntry mem_entry = memory.contains(addr) ? memory.at(addr) : MemEntry{}; @@ -203,7 +205,7 @@ AvmMemTraceBuilder::MemEntry AvmMemTraceBuilder::read_and_load_mov_opcode(uint32 .m_tag = mem_entry.tag, .r_in_tag = mem_entry.tag, .w_in_tag = mem_entry.tag, - .m_sel_mov_a = true, + .m_sel_mov_a = is_mov, }); return mem_entry; diff --git a/barretenberg/cpp/src/barretenberg/vm/avm_trace/avm_mem_trace.hpp b/barretenberg/cpp/src/barretenberg/vm/avm_trace/avm_mem_trace.hpp index 31bc2e4b915..24d39f3b218 100644 --- a/barretenberg/cpp/src/barretenberg/vm/avm_trace/avm_mem_trace.hpp +++ b/barretenberg/cpp/src/barretenberg/vm/avm_trace/avm_mem_trace.hpp @@ -87,7 +87,7 @@ class AvmMemTraceBuilder { std::vector finalize(); - MemEntry read_and_load_mov_opcode(uint32_t clk, uint32_t addr); + MemEntry read_and_load_no_tag_check(uint32_t clk, uint32_t addr, bool is_mov); std::array read_and_load_cmov_opcode(uint32_t clk, uint32_t a_addr, uint32_t b_addr, 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 1523e0615f2..c6f1b2bf88f 100644 --- a/barretenberg/cpp/src/barretenberg/vm/avm_trace/avm_trace.cpp +++ b/barretenberg/cpp/src/barretenberg/vm/avm_trace/avm_trace.cpp @@ -814,7 +814,7 @@ void AvmTraceBuilder::op_mov(uint8_t indirect, uint32_t src_offset, uint32_t dst } // Reading from memory and loading into ia without tag check. - auto const [val, tag] = mem_trace_builder.read_and_load_mov_opcode(clk, direct_src_offset); + auto const [val, tag] = mem_trace_builder.read_and_load_no_tag_check(clk, direct_src_offset, true); // Write into memory from intermediate register ic. mem_trace_builder.write_into_memory(clk, IntermRegister::IC, direct_dst_offset, val, tag, tag); @@ -949,6 +949,73 @@ void AvmTraceBuilder::op_cmov( }); } +/** + * @brief Cast an element pointed by the address a_offset into type specified by dst_tag and + store the result in address given by dst_offset. + * + * @param indirect A byte encoding information about indirect/direct memory access. + * @param a_offset Offset of source memory cell. + * @param dst_offset Offset of destination memory cell. + * @param dst_tag Destination tag specifying the type the source value must be casted to. + */ +void AvmTraceBuilder::op_cast(uint8_t indirect, uint32_t a_offset, uint32_t dst_offset, AvmMemoryTag dst_tag) +{ + auto const clk = static_cast(main_trace.size()); + bool tag_match = true; + uint32_t direct_a_offset = a_offset; + uint32_t direct_dst_offset = dst_offset; + + bool indirect_a_flag = is_operand_indirect(indirect, 0); + bool indirect_dst_flag = is_operand_indirect(indirect, 1); + + if (indirect_a_flag) { + auto read_ind_a = mem_trace_builder.indirect_read_and_load_from_memory(clk, IndirectRegister::IND_A, a_offset); + direct_a_offset = uint32_t(read_ind_a.val); + tag_match = tag_match && read_ind_a.tag_match; + } + + if (indirect_dst_flag) { + auto read_ind_c = + mem_trace_builder.indirect_read_and_load_from_memory(clk, IndirectRegister::IND_C, dst_offset); + direct_dst_offset = uint32_t(read_ind_c.val); + tag_match = tag_match && read_ind_c.tag_match; + } + + // Reading from memory and loading into ia + auto memEntry = mem_trace_builder.read_and_load_no_tag_check(clk, direct_a_offset, false); + FF a = memEntry.val; + + // In case of a memory tag error, we do not perform the computation. + // Therefore, we do not create any entry in ALU table and store the value 0 as + // output (c) in memory. + FF c = tag_match ? alu_trace_builder.op_cast(a, dst_tag, clk) : FF(0); + + // Write into memory value c from intermediate register ic. + mem_trace_builder.write_into_memory(clk, IntermRegister::IC, direct_dst_offset, c, memEntry.tag, dst_tag); + + main_trace.push_back(Row{ + .avm_main_clk = clk, + .avm_main_alu_in_tag = FF(static_cast(dst_tag)), + .avm_main_ia = a, + .avm_main_ic = c, + .avm_main_ind_a = indirect_a_flag ? FF(a_offset) : FF(0), + .avm_main_ind_c = indirect_dst_flag ? FF(dst_offset) : FF(0), + .avm_main_ind_op_a = FF(static_cast(indirect_a_flag)), + .avm_main_ind_op_c = FF(static_cast(indirect_dst_flag)), + .avm_main_internal_return_ptr = FF(internal_return_ptr), + .avm_main_mem_idx_a = FF(direct_a_offset), + .avm_main_mem_idx_c = FF(direct_dst_offset), + .avm_main_mem_op_a = FF(1), + .avm_main_mem_op_c = FF(1), + .avm_main_pc = FF(pc++), + .avm_main_r_in_tag = FF(static_cast(memEntry.tag)), + .avm_main_rwc = FF(1), + .avm_main_sel_op_cast = FF(1), + .avm_main_tag_err = FF(static_cast(!tag_match)), + .avm_main_w_in_tag = FF(static_cast(dst_tag)), + }); +} + /** * @brief CALLDATACOPY opcode with direct or indirect memory access, i.e., * direct: M[dst_offset:dst_offset+copy_size] = calldata[cd_offset:cd_offset+copy_size] @@ -1448,6 +1515,8 @@ std::vector AvmTraceBuilder::finalize() dest.avm_alu_op_eq = FF(static_cast(src.alu_op_eq)); dest.avm_alu_op_lt = FF(static_cast(src.alu_op_lt)); dest.avm_alu_op_lte = FF(static_cast(src.alu_op_lte)); + dest.avm_alu_op_cast = FF(static_cast(src.alu_op_cast)); + dest.avm_alu_op_cast_prev = FF(static_cast(src.alu_op_cast_prev)); dest.avm_alu_cmp_sel = FF(static_cast(src.alu_op_lt) + static_cast(src.alu_op_lte)); dest.avm_alu_rng_chk_sel = FF(static_cast(src.rng_chk_sel)); @@ -1493,9 +1562,10 @@ std::vector AvmTraceBuilder::finalize() // multiplication over u128 is taking two lines. 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_op_eq == FF(1) || dest.avm_alu_op_not == FF(1) || dest.avm_alu_op_lt == FF(1) || - dest.avm_alu_op_lte == FF(1)) { + dest.avm_alu_op_lte == FF(1) || dest.avm_alu_op_cast == FF(1)) { dest.avm_alu_alu_sel = FF(1); } + if (dest.avm_alu_cmp_sel == FF(1) || dest.avm_alu_rng_chk_sel == FF(1)) { dest.avm_alu_a_lo = FF(src.hi_lo_limbs.at(0)); dest.avm_alu_a_hi = FF(src.hi_lo_limbs.at(1)); @@ -1519,6 +1589,20 @@ std::vector AvmTraceBuilder::finalize() dest.avm_alu_rng_chk_lookup_selector = FF(1); } + if (dest.avm_alu_op_cast == FF(1)) { + dest.avm_alu_a_lo = FF(src.hi_lo_limbs.at(0)); + dest.avm_alu_a_hi = FF(src.hi_lo_limbs.at(1)); + dest.avm_alu_p_sub_a_lo = FF(src.hi_lo_limbs.at(2)); + dest.avm_alu_p_sub_a_hi = FF(src.hi_lo_limbs.at(3)); + dest.avm_alu_rng_chk_lookup_selector = FF(1); + } + + if (dest.avm_alu_op_cast_prev == FF(1)) { + dest.avm_alu_a_lo = FF(src.hi_lo_limbs.at(0)); + dest.avm_alu_a_hi = FF(src.hi_lo_limbs.at(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); 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 9918144f5f3..71b1aabe368 100644 --- a/barretenberg/cpp/src/barretenberg/vm/avm_trace/avm_trace.hpp +++ b/barretenberg/cpp/src/barretenberg/vm/avm_trace/avm_trace.hpp @@ -72,6 +72,10 @@ class AvmTraceBuilder { // is determined conditionally based on a conditional value determined by cond_offset. void op_cmov(uint8_t indirect, uint32_t a_offset, uint32_t b_offset, uint32_t cond_offset, uint32_t dst_offset); + // Cast an element pointed by the address a_offset into type specified by dst_tag and + // store the result in address given by dst_offset. + void op_cast(uint8_t indirect, uint32_t a_offset, uint32_t dst_offset, AvmMemoryTag dst_tag); + // Jump to a given program counter. void jump(uint32_t jmp_dest); 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 15cfb288a31..221702456b1 100644 --- a/barretenberg/cpp/src/barretenberg/vm/generated/avm_circuit_builder.hpp +++ b/barretenberg/cpp/src/barretenberg/vm/generated/avm_circuit_builder.hpp @@ -70,6 +70,7 @@ template struct AvmFullRow { FF avm_alu_in_tag{}; FF avm_alu_op_add{}; FF avm_alu_op_cast{}; + FF avm_alu_op_cast_prev{}; FF avm_alu_op_div{}; FF avm_alu_op_eq{}; FF avm_alu_op_eq_diff_inv{}; @@ -272,6 +273,7 @@ template struct AvmFullRow { FF avm_alu_cmp_rng_ctr_shift{}; FF avm_alu_cmp_sel_shift{}; FF avm_alu_op_add_shift{}; + FF avm_alu_op_cast_prev_shift{}; FF avm_alu_op_cast_shift{}; FF avm_alu_op_mul_shift{}; FF avm_alu_op_sub_shift{}; @@ -313,8 +315,8 @@ class AvmCircuitBuilder { using Polynomial = Flavor::Polynomial; using ProverPolynomials = Flavor::ProverPolynomials; - static constexpr size_t num_fixed_columns = 250; - static constexpr size_t num_polys = 214; + static constexpr size_t num_fixed_columns = 252; + static constexpr size_t num_polys = 215; std::vector rows; void set_trace(std::vector&& trace) { rows = std::move(trace); } @@ -349,6 +351,7 @@ class AvmCircuitBuilder { polys.avm_alu_in_tag[i] = rows[i].avm_alu_in_tag; polys.avm_alu_op_add[i] = rows[i].avm_alu_op_add; polys.avm_alu_op_cast[i] = rows[i].avm_alu_op_cast; + polys.avm_alu_op_cast_prev[i] = rows[i].avm_alu_op_cast_prev; polys.avm_alu_op_div[i] = rows[i].avm_alu_op_div; polys.avm_alu_op_eq[i] = rows[i].avm_alu_op_eq; polys.avm_alu_op_eq_diff_inv[i] = rows[i].avm_alu_op_eq_diff_inv; @@ -522,6 +525,7 @@ class AvmCircuitBuilder { 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_cast_prev_shift = Polynomial(polys.avm_alu_op_cast_prev.shifted()); polys.avm_alu_op_cast_shift = Polynomial(polys.avm_alu_op_cast.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()); diff --git a/barretenberg/cpp/src/barretenberg/vm/generated/avm_flavor.hpp b/barretenberg/cpp/src/barretenberg/vm/generated/avm_flavor.hpp index a03e9a31976..fbd3f58d4c8 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 = 212; + static constexpr size_t NUM_WITNESS_ENTITIES = 213; 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 = 250; + static constexpr size_t NUM_ALL_ENTITIES = 252; using GrandProductRelations = std::tuple, perm_main_bin_relation, @@ -192,6 +192,7 @@ class AvmFlavor { avm_alu_in_tag, avm_alu_op_add, avm_alu_op_cast, + avm_alu_op_cast_prev, avm_alu_op_div, avm_alu_op_eq, avm_alu_op_eq_diff_inv, @@ -407,6 +408,7 @@ class AvmFlavor { avm_alu_in_tag, avm_alu_op_add, avm_alu_op_cast, + avm_alu_op_cast_prev, avm_alu_op_div, avm_alu_op_eq, avm_alu_op_eq_diff_inv, @@ -627,6 +629,7 @@ class AvmFlavor { avm_alu_in_tag, avm_alu_op_add, avm_alu_op_cast, + avm_alu_op_cast_prev, avm_alu_op_div, avm_alu_op_eq, avm_alu_op_eq_diff_inv, @@ -829,6 +832,7 @@ class AvmFlavor { avm_alu_cmp_rng_ctr_shift, avm_alu_cmp_sel_shift, avm_alu_op_add_shift, + avm_alu_op_cast_prev_shift, avm_alu_op_cast_shift, avm_alu_op_mul_shift, avm_alu_op_sub_shift, @@ -880,6 +884,7 @@ class AvmFlavor { avm_alu_in_tag, avm_alu_op_add, avm_alu_op_cast, + avm_alu_op_cast_prev, avm_alu_op_div, avm_alu_op_eq, avm_alu_op_eq_diff_inv, @@ -1082,6 +1087,7 @@ class AvmFlavor { avm_alu_cmp_rng_ctr_shift, avm_alu_cmp_sel_shift, avm_alu_op_add_shift, + avm_alu_op_cast_prev_shift, avm_alu_op_cast_shift, avm_alu_op_mul_shift, avm_alu_op_sub_shift, @@ -1133,6 +1139,7 @@ class AvmFlavor { avm_alu_in_tag, avm_alu_op_add, avm_alu_op_cast, + avm_alu_op_cast_prev, avm_alu_op_div, avm_alu_op_eq, avm_alu_op_eq_diff_inv, @@ -1331,80 +1338,37 @@ 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_cmp_sel, - avm_alu_op_add, - avm_alu_op_cast, - 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, + 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_cast_prev, + avm_alu_op_cast, 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_cmp_sel_shift, - avm_alu_op_add_shift, - avm_alu_op_cast_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, - 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, - avm_main_pc_shift, - avm_mem_addr_shift, - avm_mem_rw_shift, - avm_mem_tag_shift, + 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_cmp_sel_shift, + avm_alu_op_add_shift, avm_alu_op_cast_prev_shift, + avm_alu_op_cast_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, 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, + avm_main_pc_shift, avm_mem_addr_shift, + avm_mem_rw_shift, avm_mem_tag_shift, avm_mem_val_shift }; }; }; @@ -1418,41 +1382,15 @@ 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_cmp_sel, - avm_alu_op_add, - avm_alu_op_cast, - 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, + 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_cast_prev, + avm_alu_op_cast, 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 }; }; @@ -1633,6 +1571,7 @@ class AvmFlavor { Base::avm_alu_in_tag = "AVM_ALU_IN_TAG"; Base::avm_alu_op_add = "AVM_ALU_OP_ADD"; Base::avm_alu_op_cast = "AVM_ALU_OP_CAST"; + Base::avm_alu_op_cast_prev = "AVM_ALU_OP_CAST_PREV"; Base::avm_alu_op_div = "AVM_ALU_OP_DIV"; Base::avm_alu_op_eq = "AVM_ALU_OP_EQ"; Base::avm_alu_op_eq_diff_inv = "AVM_ALU_OP_EQ_DIFF_INV"; @@ -1864,6 +1803,7 @@ class AvmFlavor { Commitment avm_alu_in_tag; Commitment avm_alu_op_add; Commitment avm_alu_op_cast; + Commitment avm_alu_op_cast_prev; Commitment avm_alu_op_div; Commitment avm_alu_op_eq; Commitment avm_alu_op_eq_diff_inv; @@ -2095,6 +2035,7 @@ class AvmFlavor { avm_alu_in_tag = deserialize_from_buffer(Transcript::proof_data, num_frs_read); avm_alu_op_add = deserialize_from_buffer(Transcript::proof_data, num_frs_read); avm_alu_op_cast = deserialize_from_buffer(Transcript::proof_data, num_frs_read); + avm_alu_op_cast_prev = deserialize_from_buffer(Transcript::proof_data, num_frs_read); avm_alu_op_div = deserialize_from_buffer(Transcript::proof_data, num_frs_read); avm_alu_op_eq = deserialize_from_buffer(Transcript::proof_data, num_frs_read); avm_alu_op_eq_diff_inv = deserialize_from_buffer(Transcript::proof_data, num_frs_read); @@ -2331,6 +2272,7 @@ class AvmFlavor { serialize_to_buffer(avm_alu_in_tag, Transcript::proof_data); serialize_to_buffer(avm_alu_op_add, Transcript::proof_data); serialize_to_buffer(avm_alu_op_cast, Transcript::proof_data); + serialize_to_buffer(avm_alu_op_cast_prev, Transcript::proof_data); serialize_to_buffer(avm_alu_op_div, Transcript::proof_data); serialize_to_buffer(avm_alu_op_eq, Transcript::proof_data); serialize_to_buffer(avm_alu_op_eq_diff_inv, 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 d8d367bbc65..d5b48dee516 100644 --- a/barretenberg/cpp/src/barretenberg/vm/generated/avm_prover.cpp +++ b/barretenberg/cpp/src/barretenberg/vm/generated/avm_prover.cpp @@ -76,6 +76,7 @@ void AvmProver::execute_wire_commitments_round() witness_commitments.avm_alu_in_tag = commitment_key->commit(key->avm_alu_in_tag); witness_commitments.avm_alu_op_add = commitment_key->commit(key->avm_alu_op_add); witness_commitments.avm_alu_op_cast = commitment_key->commit(key->avm_alu_op_cast); + witness_commitments.avm_alu_op_cast_prev = commitment_key->commit(key->avm_alu_op_cast_prev); witness_commitments.avm_alu_op_div = commitment_key->commit(key->avm_alu_op_div); witness_commitments.avm_alu_op_eq = commitment_key->commit(key->avm_alu_op_eq); witness_commitments.avm_alu_op_eq_diff_inv = commitment_key->commit(key->avm_alu_op_eq_diff_inv); @@ -260,6 +261,7 @@ void AvmProver::execute_wire_commitments_round() transcript->send_to_verifier(commitment_labels.avm_alu_in_tag, witness_commitments.avm_alu_in_tag); transcript->send_to_verifier(commitment_labels.avm_alu_op_add, witness_commitments.avm_alu_op_add); transcript->send_to_verifier(commitment_labels.avm_alu_op_cast, witness_commitments.avm_alu_op_cast); + transcript->send_to_verifier(commitment_labels.avm_alu_op_cast_prev, witness_commitments.avm_alu_op_cast_prev); transcript->send_to_verifier(commitment_labels.avm_alu_op_div, witness_commitments.avm_alu_op_div); transcript->send_to_verifier(commitment_labels.avm_alu_op_eq, witness_commitments.avm_alu_op_eq); transcript->send_to_verifier(commitment_labels.avm_alu_op_eq_diff_inv, witness_commitments.avm_alu_op_eq_diff_inv); diff --git a/barretenberg/cpp/src/barretenberg/vm/generated/avm_verifier.cpp b/barretenberg/cpp/src/barretenberg/vm/generated/avm_verifier.cpp index 435e6c7ae9f..a7b418bab60 100644 --- a/barretenberg/cpp/src/barretenberg/vm/generated/avm_verifier.cpp +++ b/barretenberg/cpp/src/barretenberg/vm/generated/avm_verifier.cpp @@ -72,6 +72,8 @@ bool AvmVerifier::verify_proof(const HonkProof& proof) commitments.avm_alu_op_add = transcript->template receive_from_prover(commitment_labels.avm_alu_op_add); commitments.avm_alu_op_cast = transcript->template receive_from_prover(commitment_labels.avm_alu_op_cast); + commitments.avm_alu_op_cast_prev = + transcript->template receive_from_prover(commitment_labels.avm_alu_op_cast_prev); commitments.avm_alu_op_div = transcript->template receive_from_prover(commitment_labels.avm_alu_op_div); commitments.avm_alu_op_eq = transcript->template receive_from_prover(commitment_labels.avm_alu_op_eq); commitments.avm_alu_op_eq_diff_inv = From 780ab06d2f480d6d9dbf95fea741601d548785c3 Mon Sep 17 00:00:00 2001 From: jeanmon Date: Wed, 17 Apr 2024 14:32:46 +0000 Subject: [PATCH 4/8] 5466: cleaning up some obsolete AVM opcode --- .../barretenberg/vm/avm_trace/avm_opcode.cpp | 145 +----------------- .../barretenberg/vm/avm_trace/avm_opcode.hpp | 2 - 2 files changed, 1 insertion(+), 146 deletions(-) diff --git a/barretenberg/cpp/src/barretenberg/vm/avm_trace/avm_opcode.cpp b/barretenberg/cpp/src/barretenberg/vm/avm_trace/avm_opcode.cpp index 05caf1ace28..df85cc684fa 100644 --- a/barretenberg/cpp/src/barretenberg/vm/avm_trace/avm_opcode.cpp +++ b/barretenberg/cpp/src/barretenberg/vm/avm_trace/avm_opcode.cpp @@ -6,95 +6,8 @@ namespace bb::avm_trace { -const std::unordered_map Bytecode::OPERANDS_NUM = { - // Compute - // Compute - Arithmetic - { OpCode::ADD, 3 }, - { OpCode::SUB, 3 }, - { OpCode::MUL, 3 }, - { OpCode::DIV, 3 }, - { OpCode::FDIV, 3 }, - //// Compute - Comparators - //{OpCode::EQ, }, - //{OpCode::LT, }, - //{OpCode::LTE, }, - //// Compute - Bitwise - //{OpCode::AND, }, - //{OpCode::OR, }, - //{OpCode::XOR, }, - // { OpCode::NOT, 2 }, - //{OpCode::SHL, }, - //{OpCode::SHR, }, - //// Compute - Type Conversions - //{OpCode::CAST, }, - - //// Execution Environment - //{OpCode::ADDRESS, }, - //{OpCode::STORAGEADDRESS, }, - //{OpCode::SENDER, }, - //{OpCode::PORTAL, }, - //{OpCode::FEEPERL1GAS, }, - //{OpCode::FEEPERL2GAS, }, - //{OpCode::FEEPERDAGAS, }, - //{OpCode::CONTRACTCALLDEPTH, }, - //// Execution Environment - Globals - //{OpCode::CHAINID, }, - //{OpCode::VERSION, }, - //{OpCode::BLOCKNUMBER, }, - //{OpCode::TIMESTAMP, }, - //{OpCode::COINBASE, }, - //{OpCode::BLOCKL1GASLIMIT, }, - //{OpCode::BLOCKL2GASLIMIT, }, - //{OpCode::BLOCKDAGASLIMIT, }, - // Execution Environment - Calldata - { OpCode::CALLDATACOPY, 3 }, - - //// Machine State - // Machine State - Gas - //{ OpCode::L1GASLEFT, }, - //{ OpCode::L2GASLEFT, }, - //{ OpCode::DAGASLEFT, }, - //// Machine State - Internal Control Flow - { OpCode::JUMP, 1 }, - { OpCode::JUMPI, 1 }, - { OpCode::INTERNALCALL, 1 }, - { OpCode::INTERNALRETURN, 0 }, - - //// Machine State - Memory - { OpCode::SET, 5 }, - //{ OpCode::MOV, }, - //{ OpCode::CMOV, }, - - //// World State - //{ OpCode::SLOAD, }, // Public Storage - //{ OpCode::SSTORE, }, // Public Storage - //{ OpCode::NOTEHASHEXISTS, }, // Notes & Nullifiers - //{ OpCode::EMITNOTEHASH, }, // Notes & Nullifiers - //{ OpCode::NULLIFIEREXISTS, }, // Notes & Nullifiers - //{ OpCode::EMITNULLIFIER, }, // Notes & Nullifiers - //{ OpCode::L1TOL2MSGEXISTS, }, // Messages - //{ OpCode::HEADERMEMBER, }, - - //// Accrued Substate - //{ OpCode::EMITUNENCRYPTEDLOG, }, - //{ OpCode::SENDL2TOL1MSG, }, - - //// Control Flow - Contract Calls - //{ OpCode::CALL, }, - //{ OpCode::STATICCALL, }, - //{ OpCode::DELEGATECALL, }, - { OpCode::RETURN, 2 }, - // { OpCode::REVERT, }, - - //// Gadgets - //{ OpCode::KECCAK, }, - //{ OpCode::POSEIDON2, }, - //{ OpCode::SHA256, }, - //{ OpCode::PEDERSEN, }, -}; - /** - * @brief Test whether a given byte reprents a valid opcode. + * @brief Test whether a given byte represents a valid opcode. * * @param byte The input byte. * @return A boolean telling whether a corresponding opcode does match the input byte. @@ -104,62 +17,6 @@ bool Bytecode::is_valid(const uint8_t byte) return byte < static_cast(OpCode::LAST_OPCODE_SENTINEL); } -/** - * @brief A function returning whether a supplied opcode has an instruction tag as argument. - * - * @param op_code The opcode - * @return A boolean set to true if the corresponding instruction needs a tag as argument. - */ -bool Bytecode::has_in_tag(OpCode const op_code) -{ - switch (op_code) { - case OpCode::ADDRESS: - case OpCode::STORAGEADDRESS: - case OpCode::SENDER: - case OpCode::PORTAL: - case OpCode::FEEPERL1GAS: - case OpCode::FEEPERL2GAS: - case OpCode::FEEPERDAGAS: - case OpCode::CONTRACTCALLDEPTH: - case OpCode::CHAINID: - case OpCode::VERSION: - case OpCode::BLOCKNUMBER: - case OpCode::TIMESTAMP: - case OpCode::COINBASE: - case OpCode::BLOCKL1GASLIMIT: - case OpCode::BLOCKL2GASLIMIT: - case OpCode::BLOCKDAGASLIMIT: - case OpCode::CALLDATACOPY: - case OpCode::L1GASLEFT: - case OpCode::L2GASLEFT: - case OpCode::DAGASLEFT: - case OpCode::JUMP: - case OpCode::JUMPI: - case OpCode::INTERNALCALL: - case OpCode::INTERNALRETURN: - case OpCode::MOV: - case OpCode::CMOV: - case OpCode::SLOAD: - case OpCode::SSTORE: - case OpCode::NOTEHASHEXISTS: - case OpCode::EMITNOTEHASH: - case OpCode::NULLIFIEREXISTS: - case OpCode::EMITNULLIFIER: - case OpCode::L1TOL2MSGEXISTS: - case OpCode::HEADERMEMBER: - case OpCode::EMITUNENCRYPTEDLOG: - case OpCode::SENDL2TOL1MSG: - case OpCode::CALL: - case OpCode::STATICCALL: - case OpCode::RETURN: - case OpCode::REVERT: - case OpCode::FDIV: - return false; - default: - return true; - } -} - std::string to_hex(OpCode opcode) { std::ostringstream stream; diff --git a/barretenberg/cpp/src/barretenberg/vm/avm_trace/avm_opcode.hpp b/barretenberg/cpp/src/barretenberg/vm/avm_trace/avm_opcode.hpp index 98adf14ab29..147cbbc36f1 100644 --- a/barretenberg/cpp/src/barretenberg/vm/avm_trace/avm_opcode.hpp +++ b/barretenberg/cpp/src/barretenberg/vm/avm_trace/avm_opcode.hpp @@ -106,8 +106,6 @@ enum class OpCode : uint8_t { class Bytecode { public: static bool is_valid(uint8_t byte); - static bool has_in_tag(OpCode); - static const std::unordered_map OPERANDS_NUM; }; std::string to_hex(OpCode opcode); From 86155a77e4e51ab31d93aebedcd73ffca9733a7e Mon Sep 17 00:00:00 2001 From: jeanmon Date: Wed, 17 Apr 2024 15:40:41 +0000 Subject: [PATCH 5/8] 5466: First unit test and various bugs fixing and improvements --- .../vm/avm_trace/avm_alu_trace.cpp | 61 +++++++++---------- .../barretenberg/vm/avm_trace/avm_common.hpp | 1 - .../vm/avm_trace/avm_mem_trace.cpp | 58 ++++++++++++++++-- .../vm/avm_trace/avm_mem_trace.hpp | 3 +- .../barretenberg/vm/avm_trace/avm_trace.cpp | 6 +- .../barretenberg/vm/tests/avm_cast.test.cpp | 32 ++++++++++ 6 files changed, 119 insertions(+), 42 deletions(-) create mode 100644 barretenberg/cpp/src/barretenberg/vm/tests/avm_cast.test.cpp 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 aceae2e2072..9935a74b840 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 @@ -667,12 +667,37 @@ FF AvmAluTraceBuilder::op_lte(FF const& a, FF const& b, AvmMemoryTag in_tag, uin */ FF AvmAluTraceBuilder::op_cast(FF const& a, AvmMemoryTag in_tag, uint32_t clk) { - uint256_t a_256{ a }; + FF c; + + switch (in_tag) { + case AvmMemoryTag::U8: + c = FF(uint8_t(a)); + break; + case AvmMemoryTag::U16: + c = FF(uint16_t(a)); + break; + case AvmMemoryTag::U32: + c = FF(uint32_t(a)); + break; + case AvmMemoryTag::U64: + c = FF(uint64_t(a)); + break; + case AvmMemoryTag::U128: + c = FF(uint256_t::from_uint128(uint128_t(a))); + break; + case AvmMemoryTag::FF: + c = a; + break; + default: + c = 0; + break; + } + // Get the decomposition of a - auto [a_lo, a_hi] = decompose(a_256); + auto [a_lo, a_hi] = decompose(uint256_t(a)); // Decomposition of p-a - auto [p_sub_a_lo, p_sub_a_hi, p_a_borrow] = gt_witness(FF::modulus, a_256); - auto [u8_r0, u8_r1, u16_reg] = to_alu_slice_registers(a_256); + auto [p_sub_a_lo, p_sub_a_hi, p_a_borrow] = gt_witness(FF::modulus, uint256_t(a)); + auto [u8_r0, u8_r1, u16_reg] = to_alu_slice_registers(uint256_t(a)); alu_trace.push_back(AvmAluTraceBuilder::AluTraceEntry{ .alu_clk = clk, @@ -684,7 +709,7 @@ FF AvmAluTraceBuilder::op_cast(FF const& a, AvmMemoryTag in_tag, uint32_t clk) .alu_u64_tag = in_tag == AvmMemoryTag::U64, .alu_u128_tag = in_tag == AvmMemoryTag::U128, .alu_ia = a, - .alu_ic = 0, + .alu_ic = c, .alu_u8_r0 = u8_r0, .alu_u8_r1 = u8_r1, .alu_u16_reg = u16_reg, @@ -703,32 +728,6 @@ FF AvmAluTraceBuilder::op_cast(FF const& a, AvmMemoryTag in_tag, uint32_t clk) .hi_lo_limbs = { p_sub_a_lo, p_sub_a_hi }, }); - FF c; - - switch (in_tag) { - case AvmMemoryTag::U8: - c = FF(uint8_t(a)); - break; - case AvmMemoryTag::U16: - c = FF(uint16_t(a)); - break; - case AvmMemoryTag::U32: - c = FF(uint32_t(a)); - break; - case AvmMemoryTag::U64: - c = FF(uint64_t(a)); - break; - case AvmMemoryTag::U128: - c = FF(uint256_t::from_uint128(uint128_t(a))); - break; - case AvmMemoryTag::FF: - c = a; - break; - default: - c = 0; - break; - } - return c; } diff --git a/barretenberg/cpp/src/barretenberg/vm/avm_trace/avm_common.hpp b/barretenberg/cpp/src/barretenberg/vm/avm_trace/avm_common.hpp index a0261419281..e3c4e90d01b 100644 --- a/barretenberg/cpp/src/barretenberg/vm/avm_trace/avm_common.hpp +++ b/barretenberg/cpp/src/barretenberg/vm/avm_trace/avm_common.hpp @@ -1,6 +1,5 @@ #pragma once -#include "barretenberg/relations/generated/avm/avm_binary.hpp" #include "barretenberg/stdlib_circuit_builders/circuit_builder_base.hpp" #include "barretenberg/vm/generated/avm_circuit_builder.hpp" #include diff --git a/barretenberg/cpp/src/barretenberg/vm/avm_trace/avm_mem_trace.cpp b/barretenberg/cpp/src/barretenberg/vm/avm_trace/avm_mem_trace.cpp index 28806c4421c..af36d8df5da 100644 --- a/barretenberg/cpp/src/barretenberg/vm/avm_trace/avm_mem_trace.cpp +++ b/barretenberg/cpp/src/barretenberg/vm/avm_trace/avm_mem_trace.cpp @@ -179,10 +179,10 @@ void AvmMemTraceBuilder::store_in_mem_trace( } /** - * @brief Handle a read memory operation without any tag check. Load the corresponding + * @brief Handle a read memory operation specific to MOV opcode. Load the corresponding * value to the intermediate register ia. A memory trace entry for the load * operation is added. It is permissive in the sense that we do not enforce tag - * matching with against any instruction tag. Optionally, a specific selector + * matching against any instruction tag. In addition, the specific selector * for MOV opcode is enabled. * * @param clk Main clock @@ -191,9 +191,7 @@ void AvmMemTraceBuilder::store_in_mem_trace( * @return Result of the read operation containing the value and the tag of the memory cell * at the supplied address. */ -AvmMemTraceBuilder::MemEntry AvmMemTraceBuilder::read_and_load_no_tag_check(uint32_t const clk, - uint32_t const addr, - bool is_mov) +AvmMemTraceBuilder::MemEntry AvmMemTraceBuilder::read_and_load_mov_opcode(uint32_t const clk, uint32_t const addr) { MemEntry mem_entry = memory.contains(addr) ? memory.at(addr) : MemEntry{}; @@ -205,12 +203,27 @@ AvmMemTraceBuilder::MemEntry AvmMemTraceBuilder::read_and_load_no_tag_check(uint .m_tag = mem_entry.tag, .r_in_tag = mem_entry.tag, .w_in_tag = mem_entry.tag, - .m_sel_mov_a = is_mov, + .m_sel_mov_a = true, }); return mem_entry; } +/** + * @brief Handle a read memory operation specific to CMOV opcode. Load the corresponding + * values to the intermediate register ia, ib, id. Three memory trace entries for + * these load operations are added. They are permissive in the sense that we do not + * enforce tag matching against any instruction tag. In addition, the specific selector + * for CMOV opcode is enabled. + * + * @param clk Main clock + * @param a_addr Memory address of the first value candidate a. + * @param b_addr Memory address of the second value candidate b. + * @param cond_addr Memory address of the conditional value. + * + * @return Result of the read operation containing the value and the tag of the memory cell + * at the supplied address. + */ std::array AvmMemTraceBuilder::read_and_load_cmov_opcode(uint32_t clk, uint32_t a_addr, uint32_t b_addr, @@ -262,6 +275,39 @@ std::array AvmMemTraceBuilder::read_and_load_cm return { a_mem_entry, b_mem_entry, cond_mem_entry }; } +/** + * @brief Handle a read memory operation specific to CAST opcode. Load the corresponding + * value to the intermediate register ia. A memory trace entry for the load + * operation is added. It is permissive in the sense that we do not enforce tag + * matching against any instruction tag. The write instruction tag w_in_tag + * is passed and added in the memory trace entry. + * + * @param clk Main clock + * @param addr Memory address of the source offset + * @param w_in_tag Write instruction instruction tag (tag the value is casted to) + * + * @return Result of the read operation containing the value and the tag of the memory cell + * at the supplied address. + */ +AvmMemTraceBuilder::MemEntry AvmMemTraceBuilder::read_and_load_cast_opcode(uint32_t clk, + uint32_t addr, + AvmMemoryTag w_in_tag) +{ + MemEntry mem_entry = memory.contains(addr) ? memory.at(addr) : MemEntry{}; + + mem_trace.emplace_back(MemoryTraceEntry{ + .m_clk = clk, + .m_sub_clk = SUB_CLK_LOAD_A, + .m_addr = addr, + .m_val = mem_entry.val, + .m_tag = mem_entry.tag, + .r_in_tag = mem_entry.tag, + .w_in_tag = w_in_tag, + }); + + return mem_entry; +} + /** * @brief Handle a read memory operation and load the corresponding value to the * supplied intermediate register. A memory trace entry for the load operation diff --git a/barretenberg/cpp/src/barretenberg/vm/avm_trace/avm_mem_trace.hpp b/barretenberg/cpp/src/barretenberg/vm/avm_trace/avm_mem_trace.hpp index 24d39f3b218..f71de0c4136 100644 --- a/barretenberg/cpp/src/barretenberg/vm/avm_trace/avm_mem_trace.hpp +++ b/barretenberg/cpp/src/barretenberg/vm/avm_trace/avm_mem_trace.hpp @@ -87,11 +87,12 @@ class AvmMemTraceBuilder { std::vector finalize(); - MemEntry read_and_load_no_tag_check(uint32_t clk, uint32_t addr, bool is_mov); + MemEntry read_and_load_mov_opcode(uint32_t clk, uint32_t addr); std::array read_and_load_cmov_opcode(uint32_t clk, uint32_t a_addr, uint32_t b_addr, uint32_t cond_addr); + MemEntry read_and_load_cast_opcode(uint32_t clk, uint32_t addr, AvmMemoryTag w_in_tag); MemRead read_and_load_from_memory( uint32_t clk, IntermRegister interm_reg, uint32_t addr, AvmMemoryTag r_in_tag, AvmMemoryTag w_in_tag); MemRead indirect_read_and_load_from_memory(uint32_t clk, IndirectRegister ind_reg, uint32_t addr); 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 c6f1b2bf88f..9a449eb43e8 100644 --- a/barretenberg/cpp/src/barretenberg/vm/avm_trace/avm_trace.cpp +++ b/barretenberg/cpp/src/barretenberg/vm/avm_trace/avm_trace.cpp @@ -814,7 +814,7 @@ void AvmTraceBuilder::op_mov(uint8_t indirect, uint32_t src_offset, uint32_t dst } // Reading from memory and loading into ia without tag check. - auto const [val, tag] = mem_trace_builder.read_and_load_no_tag_check(clk, direct_src_offset, true); + auto const [val, tag] = mem_trace_builder.read_and_load_mov_opcode(clk, direct_src_offset); // Write into memory from intermediate register ic. mem_trace_builder.write_into_memory(clk, IntermRegister::IC, direct_dst_offset, val, tag, tag); @@ -982,7 +982,7 @@ void AvmTraceBuilder::op_cast(uint8_t indirect, uint32_t a_offset, uint32_t dst_ } // Reading from memory and loading into ia - auto memEntry = mem_trace_builder.read_and_load_no_tag_check(clk, direct_a_offset, false); + auto memEntry = mem_trace_builder.read_and_load_cast_opcode(clk, direct_a_offset, dst_tag); FF a = memEntry.val; // In case of a memory tag error, we do not perform the computation. @@ -1614,7 +1614,7 @@ std::vector AvmTraceBuilder::finalize() if ((r.avm_main_sel_op_add == FF(1) || r.avm_main_sel_op_sub == FF(1) || r.avm_main_sel_op_mul == FF(1) || r.avm_main_sel_op_eq == FF(1) || r.avm_main_sel_op_not == FF(1) || r.avm_main_sel_op_lt || - r.avm_main_sel_op_lte) && + r.avm_main_sel_op_lte || r.avm_main_sel_op_cast == FF(1)) && r.avm_main_tag_err == FF(0)) { r.avm_main_alu_sel = FF(1); } diff --git a/barretenberg/cpp/src/barretenberg/vm/tests/avm_cast.test.cpp b/barretenberg/cpp/src/barretenberg/vm/tests/avm_cast.test.cpp new file mode 100644 index 00000000000..896043257be --- /dev/null +++ b/barretenberg/cpp/src/barretenberg/vm/tests/avm_cast.test.cpp @@ -0,0 +1,32 @@ +#include "avm_common.test.hpp" +#include "barretenberg/vm/avm_trace/avm_common.hpp" +#include "barretenberg/vm/tests/helpers.test.hpp" +#include +#include + +namespace tests_avm { +using namespace bb::avm_trace; +using namespace testing; + +class AvmCastTests : public ::testing::Test { + public: + AvmTraceBuilder trace_builder; + + protected: + std::vector trace; + + // TODO(640): The Standard Honk on Grumpkin test suite fails unless the SRS is initialised for every test. + void SetUp() override { srs::init_crs_factory("../srs_db/ignition"); }; +}; + +TEST_F(AvmCastTests, basicU8ToU16) +{ + trace_builder.op_set(0, 237, 0, AvmMemoryTag::U8); + trace_builder.op_cast(0, 0, 1, AvmMemoryTag::U16); + trace_builder.return_op(0, 0, 0); + auto trace = trace_builder.finalize(); + + validate_trace_check_circuit(std::move(trace)); +} + +} // namespace tests_avm From f0e34bbc05c4cdaeda27ef210cc888b28dd51582 Mon Sep 17 00:00:00 2001 From: jeanmon Date: Thu, 18 Apr 2024 11:23:46 +0000 Subject: [PATCH 6/8] 5466: positive unit tests for CAST --- .../barretenberg/vm/tests/avm_cast.test.cpp | 182 +++++++++++++++++- 1 file changed, 179 insertions(+), 3 deletions(-) diff --git a/barretenberg/cpp/src/barretenberg/vm/tests/avm_cast.test.cpp b/barretenberg/cpp/src/barretenberg/vm/tests/avm_cast.test.cpp index 896043257be..fbb35c11b5e 100644 --- a/barretenberg/cpp/src/barretenberg/vm/tests/avm_cast.test.cpp +++ b/barretenberg/cpp/src/barretenberg/vm/tests/avm_cast.test.cpp @@ -17,16 +17,192 @@ class AvmCastTests : public ::testing::Test { // TODO(640): The Standard Honk on Grumpkin test suite fails unless the SRS is initialised for every test. void SetUp() override { srs::init_crs_factory("../srs_db/ignition"); }; + + void gen_trace( + uint128_t const& a, uint32_t src_address, uint32_t dst_address, AvmMemoryTag src_tag, AvmMemoryTag dst_tag) + { + trace_builder.op_set(0, a, src_address, src_tag); + trace_builder.op_cast(0, src_address, dst_address, dst_tag); + trace_builder.return_op(0, 0, 0); + trace = trace_builder.finalize(); + } + + void validate_cast_trace(FF const& a, + FF const& cast_val, + uint32_t src_address, + uint32_t dst_address, + AvmMemoryTag src_tag, + AvmMemoryTag dst_tag + + ) + { + auto row = + std::ranges::find_if(trace.begin(), trace.end(), [](Row r) { return r.avm_main_sel_op_cast == FF(1); }); + ASSERT_TRUE(row != trace.end()); + + EXPECT_THAT(*row, + AllOf(Field("sel_op_cast", &Row::avm_main_sel_op_cast, 1), + Field("ia", &Row::avm_main_ia, a), + Field("ib", &Row::avm_main_ib, 0), + Field("ic", &Row::avm_main_ic, cast_val), + Field("r_in_tag", &Row::avm_main_r_in_tag, static_cast(src_tag)), + Field("w_in_tag", &Row::avm_main_w_in_tag, static_cast(dst_tag)), + Field("alu_in_tag", &Row::avm_main_alu_in_tag, static_cast(dst_tag)), + Field("op_a", &Row::avm_main_mem_op_a, 1), + Field("op_c", &Row::avm_main_mem_op_c, 1), + Field("rwa", &Row::avm_main_rwa, 0), + Field("rwc", &Row::avm_main_rwc, 1), + Field("mem_idx_a", &Row::avm_main_mem_idx_a, src_address), + Field("mem_idx_c", &Row::avm_main_mem_idx_c, dst_address), + Field("tag_err", &Row::avm_main_tag_err, 0), + Field("alu_sel", &Row::avm_main_alu_sel, 1), + Field("sel_rng_8", &Row::avm_main_sel_rng_8, 1), + Field("sel_rng_16", &Row::avm_main_sel_rng_16, 1))); + + // Find the corresponding Alu trace row + auto clk = row->avm_main_clk; + auto alu_row = std::ranges::find_if(trace.begin(), trace.end(), [clk](Row r) { return r.avm_alu_clk == clk; }); + ASSERT_TRUE(alu_row != trace.end()); + + EXPECT_THAT(*alu_row, + AllOf(Field("op_cast", &Row::avm_alu_op_cast, 1), + Field("alu_ia", &Row::avm_alu_ia, a), + Field("alu_ib", &Row::avm_alu_ib, 0), + Field("alu_ic", &Row::avm_alu_ic, cast_val), + Field("u8_tag", &Row::avm_alu_u8_tag, dst_tag == AvmMemoryTag::U8), + Field("u16_tag", &Row::avm_alu_u16_tag, dst_tag == AvmMemoryTag::U16), + Field("u32_tag", &Row::avm_alu_u32_tag, dst_tag == AvmMemoryTag::U32), + Field("u64_tag", &Row::avm_alu_u64_tag, dst_tag == AvmMemoryTag::U64), + Field("u128_tag", &Row::avm_alu_u128_tag, dst_tag == AvmMemoryTag::U128), + Field("ff_tag", &Row::avm_alu_ff_tag, dst_tag == AvmMemoryTag::FF), + Field("in_tag", &Row::avm_alu_in_tag, static_cast(dst_tag)), + Field("op_cast_prev", &Row::avm_alu_op_cast_prev, 0), + Field("lookup_selector", &Row::avm_alu_rng_chk_lookup_selector, 1), + Field("alu_sel", &Row::avm_alu_alu_sel, 1))); + + // Check that there is a second ALU row + auto alu_row_next = alu_row + 1; + EXPECT_THAT( + *alu_row_next, + AllOf(Field("op_cast", &Row::avm_alu_op_cast, 0), Field("op_cast_prev", &Row::avm_alu_op_cast_prev, 1))); + + validate_trace(std::move(trace)); + } }; TEST_F(AvmCastTests, basicU8ToU16) { - trace_builder.op_set(0, 237, 0, AvmMemoryTag::U8); + gen_trace(237, 0, 1, AvmMemoryTag::U8, AvmMemoryTag::U16); + validate_cast_trace(237, 237, 0, 1, AvmMemoryTag::U8, AvmMemoryTag::U16); +} + +TEST_F(AvmCastTests, truncationU32ToU8) +{ + gen_trace(876123, 0, 1, AvmMemoryTag::U32, AvmMemoryTag::U8); + validate_cast_trace(876123, 91, 0, 1, AvmMemoryTag::U32, AvmMemoryTag::U8); +} + +TEST_F(AvmCastTests, sameAddressU16ToU8) +{ + gen_trace(1049, 23, 23, AvmMemoryTag::U16, AvmMemoryTag::U8); // M[23] = 1049 + validate_cast_trace(1049, 25, 23, 23, AvmMemoryTag::U16, AvmMemoryTag::U8); +} + +TEST_F(AvmCastTests, basicU64ToFF) +{ + gen_trace(987234987324233324UL, 0, 1, AvmMemoryTag::U64, AvmMemoryTag::FF); + validate_cast_trace(987234987324233324UL, 987234987324233324UL, 0, 1, AvmMemoryTag::U64, AvmMemoryTag::FF); +} + +TEST_F(AvmCastTests, sameTagU128) +{ + uint128_t a = 312; + a = a << 99; + gen_trace(a, 0, 1, AvmMemoryTag::U128, AvmMemoryTag::U128); + validate_cast_trace( + uint256_t::from_uint128(a), FF(uint256_t::from_uint128(a)), 0, 1, AvmMemoryTag::U128, AvmMemoryTag::U128); +} + +TEST_F(AvmCastTests, noTruncationFFToU32) +{ + gen_trace(UINT32_MAX, 4, 9, AvmMemoryTag::FF, AvmMemoryTag::U32); + validate_cast_trace(UINT32_MAX, UINT32_MAX, 4, 9, AvmMemoryTag::FF, AvmMemoryTag::U32); +} + +TEST_F(AvmCastTests, truncationFFToU16ModMinus1) +{ + trace_builder.calldata_copy(0, 0, 1, 0, { FF(FF::modulus - 1) }); + trace_builder.op_cast(0, 0, 1, AvmMemoryTag::U16); + trace_builder.return_op(0, 0, 0); + trace = trace_builder.finalize(); + + validate_cast_trace(FF::modulus - 1, 0, 0, 1, AvmMemoryTag::FF, AvmMemoryTag::U16); +} + +TEST_F(AvmCastTests, truncationFFToU16ModMinus2) +{ + trace_builder.calldata_copy(0, 0, 1, 0, { FF(FF::modulus_minus_two) }); trace_builder.op_cast(0, 0, 1, AvmMemoryTag::U16); trace_builder.return_op(0, 0, 0); - auto trace = trace_builder.finalize(); + trace = trace_builder.finalize(); + + validate_cast_trace(FF::modulus_minus_two, UINT16_MAX, 0, 1, AvmMemoryTag::FF, AvmMemoryTag::U16); +} + +TEST_F(AvmCastTests, truncationU32ToU16) +{ + // 998877665 = OX3B89A9E1 + // Truncated to 16 bits: 0XA9E1 = 43489 + gen_trace(998877665UL, 0, 1, AvmMemoryTag::U32, AvmMemoryTag::U16); + validate_cast_trace(998877665UL, 43489, 0, 1, AvmMemoryTag::U32, AvmMemoryTag::U16); +} + +TEST_F(AvmCastTests, indirectAddrTruncationU64ToU8) +{ + // Indirect addresses. src:0 dst:1 + // Direct addresses. src:10 dst:11 + // Source value: 256'000'000'203 --> truncated to 203 + trace_builder.op_set(0, 10, 0, AvmMemoryTag::U32); + trace_builder.op_set(0, 11, 1, AvmMemoryTag::U32); + trace_builder.op_set(0, 256'000'000'203UL, 10, AvmMemoryTag::U64); + trace_builder.op_cast(3, 0, 1, AvmMemoryTag::U8); + trace_builder.return_op(0, 0, 0); + trace = trace_builder.finalize(); + + validate_cast_trace(256'000'000'203UL, 203, 10, 11, AvmMemoryTag::U64, AvmMemoryTag::U8); +} + +TEST_F(AvmCastTests, indirectAddrWrongResolutionU64ToU8) +{ + // Indirect addresses. src:5 dst:6 + // Direct addresses. src:10 dst:11 + trace_builder.op_set(0, 10, 5, AvmMemoryTag::U8); // Not an address type + trace_builder.op_set(0, 11, 6, AvmMemoryTag::U32); + trace_builder.op_set(0, 4234, 10, AvmMemoryTag::U64); + trace_builder.op_cast(3, 5, 6, AvmMemoryTag::U8); + trace_builder.return_op(0, 0, 0); + trace = trace_builder.finalize(); + + auto row = std::ranges::find_if(trace.begin(), trace.end(), [](Row r) { return r.avm_main_sel_op_cast == FF(1); }); + ASSERT_TRUE(row != trace.end()); + + EXPECT_THAT(*row, + AllOf(Field("sel_op_cast", &Row::avm_main_sel_op_cast, 1), + Field("r_in_tag", &Row::avm_main_r_in_tag, static_cast(AvmMemoryTag::U64)), + Field("w_in_tag", &Row::avm_main_w_in_tag, static_cast(AvmMemoryTag::U8)), + Field("alu_in_tag", &Row::avm_main_alu_in_tag, static_cast(AvmMemoryTag::U8)), + Field("op_a", &Row::avm_main_mem_op_a, 1), + Field("op_c", &Row::avm_main_mem_op_c, 1), + Field("ind_op_a", &Row::avm_main_ind_op_a, 1), + Field("ind_op_c", &Row::avm_main_ind_op_c, 1), + Field("ind_a", &Row::avm_main_ind_a, 5), + Field("ind_c", &Row::avm_main_ind_c, 6), + Field("rwa", &Row::avm_main_rwa, 0), + Field("rwc", &Row::avm_main_rwc, 1), + Field("alu_sel", &Row::avm_main_alu_sel, 0), // ALU trace not activated + Field("tag_err", &Row::avm_main_tag_err, 1))); // Error activated - validate_trace_check_circuit(std::move(trace)); + validate_trace(std::move(trace)); } } // namespace tests_avm From d1400acb764dafcb4999733a352b2af246ec6fc7 Mon Sep 17 00:00:00 2001 From: jeanmon Date: Thu, 18 Apr 2024 11:41:00 +0000 Subject: [PATCH 7/8] 5466: deserialization and execution support for CAST --- .../vm/avm_trace/avm_deserialization.cpp | 2 + .../vm/avm_trace/avm_execution.cpp | 7 ++++ .../vm/tests/avm_execution.test.cpp | 41 +++++++++++++++++++ 3 files changed, 50 insertions(+) diff --git a/barretenberg/cpp/src/barretenberg/vm/avm_trace/avm_deserialization.cpp b/barretenberg/cpp/src/barretenberg/vm/avm_trace/avm_deserialization.cpp index 2590e5e298a..9b9c4bd7b3e 100644 --- a/barretenberg/cpp/src/barretenberg/vm/avm_trace/avm_deserialization.cpp +++ b/barretenberg/cpp/src/barretenberg/vm/avm_trace/avm_deserialization.cpp @@ -35,6 +35,8 @@ const std::unordered_map> OPCODE_WIRE_FORMAT = { OpCode::AND, three_operand_format }, { OpCode::OR, three_operand_format }, { OpCode::XOR, three_operand_format }, + // Compute - Type Conversions + { OpCode::CAST, { OperandType::INDIRECT, OperandType::TAG, OperandType::UINT32, OperandType::UINT32 } }, // Execution Environment - Calldata { OpCode::CALLDATACOPY, { OperandType::INDIRECT, OperandType::UINT32, OperandType::UINT32, OperandType::UINT32 } }, // Machine State - Internal Control Flow diff --git a/barretenberg/cpp/src/barretenberg/vm/avm_trace/avm_execution.cpp b/barretenberg/cpp/src/barretenberg/vm/avm_trace/avm_execution.cpp index 1e018d647d6..e25d9ad1807 100644 --- a/barretenberg/cpp/src/barretenberg/vm/avm_trace/avm_execution.cpp +++ b/barretenberg/cpp/src/barretenberg/vm/avm_trace/avm_execution.cpp @@ -180,6 +180,13 @@ std::vector Execution::gen_trace(std::vector const& instructio std::get(inst.operands.at(4)), std::get(inst.operands.at(1))); break; + // Compute - Type Conversions + case OpCode::CAST: + trace_builder.op_cast(std::get(inst.operands.at(0)), + std::get(inst.operands.at(2)), + std::get(inst.operands.at(3)), + std::get(inst.operands.at(1))); + break; // Execution Environment - Calldata case OpCode::CALLDATACOPY: trace_builder.calldata_copy(std::get(inst.operands.at(0)), diff --git a/barretenberg/cpp/src/barretenberg/vm/tests/avm_execution.test.cpp b/barretenberg/cpp/src/barretenberg/vm/tests/avm_execution.test.cpp index f505eb16ce5..2639e9fb979 100644 --- a/barretenberg/cpp/src/barretenberg/vm/tests/avm_execution.test.cpp +++ b/barretenberg/cpp/src/barretenberg/vm/tests/avm_execution.test.cpp @@ -607,6 +607,47 @@ TEST_F(AvmExecutionTests, indMovOpcode) gen_proof_and_validate(bytecode, std::move(trace), {}); } +// Positive test for SET and CAST opcodes +TEST_F(AvmExecutionTests, setAndCastOpcodes) +{ + std::string bytecode_hex = to_hex(OpCode::SET) + // opcode SET + "00" // Indirect flag + "02" // U16 + "B813" // val 47123 + "00000011" // dst_offset 17 + + to_hex(OpCode::CAST) + // opcode CAST + "00" // Indirect flag + "01" // U8 + "00000011" // addr a + "00000012" // addr casted a + + to_hex(OpCode::RETURN) + // opcode RETURN + "00" // Indirect flag + "00000000" // ret offset 0 + "00000000"; // ret size 0 + + auto bytecode = hex_to_bytes(bytecode_hex); + auto instructions = Deserialization::parse(bytecode); + + ASSERT_THAT(instructions, SizeIs(3)); + + // SUB + EXPECT_THAT(instructions.at(1), + AllOf(Field(&Instruction::op_code, OpCode::CAST), + Field(&Instruction::operands, + ElementsAre(VariantWith(0), + VariantWith(AvmMemoryTag::U8), + VariantWith(17), + VariantWith(18))))); + + auto trace = Execution::gen_trace(instructions); + + // Find the first row enabling the cast selector + auto row = std::ranges::find_if(trace.begin(), trace.end(), [](Row r) { return r.avm_main_sel_op_cast == 1; }); + EXPECT_EQ(row->avm_main_ic, 19); // 0XB813 --> 0X13 = 19 + + gen_proof_and_validate(bytecode, std::move(trace), {}); +} + // Negative test detecting an invalid opcode byte. TEST_F(AvmExecutionTests, invalidOpcode) { From 8843cec04bed45ee071046d8c67d090e000635fc Mon Sep 17 00:00:00 2001 From: jeanmon Date: Thu, 18 Apr 2024 12:12:35 +0000 Subject: [PATCH 8/8] 5466: Add PIL relation to prevent overlap in second row of CAST and 128-bit multiplication in ALU trace --- barretenberg/cpp/pil/avm/avm_alu.pil | 12 +- .../relations/generated/avm/avm_alu.hpp | 31 ++-- .../relations/generated/avm/declare_views.hpp | 1 + .../vm/generated/avm_circuit_builder.hpp | 4 +- .../barretenberg/vm/generated/avm_flavor.hpp | 151 +++++++++++++----- 5 files changed, 140 insertions(+), 59 deletions(-) diff --git a/barretenberg/cpp/pil/avm/avm_alu.pil b/barretenberg/cpp/pil/avm/avm_alu.pil index 2150542e686..cc39ef9ca7e 100644 --- a/barretenberg/cpp/pil/avm/avm_alu.pil +++ b/barretenberg/cpp/pil/avm/avm_alu.pil @@ -497,11 +497,6 @@ namespace avm_alu(256); #[OP_CAST_PREV_LINE] op_cast_prev' = op_cast; - // TODO: If a lookup selector with value > 1 is enabled, then we do not need this constraint. - // Otherwise, melding two op_cast with a common row might lead to disabling - #[OP_CAST_PREV_MUT_EXCL] - op_cast_prev * op_cast = 0; - #[ALU_OP_CAST] op_cast * (SUM_TAG + ff_tag * ia - ic) = 0; @@ -509,4 +504,9 @@ namespace avm_alu(256); op_cast * (a_lo' - p_sub_a_lo) = 0; #[OP_CAST_RNG_CHECK_P_SUB_A_HIGH] - op_cast * (a_hi' - p_sub_a_hi) = 0; \ No newline at end of file + op_cast * (a_hi' - p_sub_a_hi) = 0; + + // 128-bit multiplication and CAST need two rows in ALU trace. We need to ensure + // that another ALU operation does not start in the second row. + #[TWO_LINE_OP_NO_OVERLAP] + (op_mul * ff_tag + op_cast) * alu_sel' = 0; \ No newline at end of file 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 ea21fba5789..ac09315024a 100644 --- a/barretenberg/cpp/src/barretenberg/relations/generated/avm/avm_alu.hpp +++ b/barretenberg/cpp/src/barretenberg/relations/generated/avm/avm_alu.hpp @@ -12,6 +12,7 @@ template struct Avm_aluRow { FF avm_alu_a_lo{}; FF avm_alu_a_lo_shift{}; FF avm_alu_alu_sel{}; + FF avm_alu_alu_sel_shift{}; FF avm_alu_b_hi{}; FF avm_alu_b_hi_shift{}; FF avm_alu_b_lo{}; @@ -181,16 +182,16 @@ inline std::string get_relation_label_avm_alu(int index) return "OP_CAST_PREV_LINE"; case 50: - return "OP_CAST_PREV_MUT_EXCL"; + return "ALU_OP_CAST"; case 51: - return "ALU_OP_CAST"; + return "OP_CAST_RNG_CHECK_P_SUB_A_LOW"; case 52: - return "OP_CAST_RNG_CHECK_P_SUB_A_LOW"; + return "OP_CAST_RNG_CHECK_P_SUB_A_HIGH"; case 53: - return "OP_CAST_RNG_CHECK_P_SUB_A_HIGH"; + return "TWO_LINE_OP_NO_OVERLAP"; } return std::to_string(index); } @@ -201,7 +202,7 @@ template class avm_aluImpl { 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, 2, 3, 5, 3, 3, + 3, 3, 4, 3, 6, 5, 3, 3, 3, 3, 4, 3, 4, 4, 3, 3, 3, 3, 3, 3, 3, 3, 2, 5, 3, 3, 4, }; template @@ -763,14 +764,6 @@ template class avm_aluImpl { { Avm_DECLARE_VIEWS(50); - auto tmp = (avm_alu_op_cast_prev * avm_alu_op_cast); - tmp *= scaling_factor; - std::get<50>(evals) += tmp; - } - // Contribution 51 - { - Avm_DECLARE_VIEWS(51); - auto tmp = (avm_alu_op_cast * (((((((avm_alu_u8_tag * avm_alu_u8_r0) + @@ -791,13 +784,21 @@ template class avm_aluImpl { (avm_alu_ff_tag * avm_alu_ia)) - avm_alu_ic)); tmp *= scaling_factor; + std::get<50>(evals) += tmp; + } + // Contribution 51 + { + Avm_DECLARE_VIEWS(51); + + auto tmp = (avm_alu_op_cast * (avm_alu_a_lo_shift - avm_alu_p_sub_a_lo)); + tmp *= scaling_factor; std::get<51>(evals) += tmp; } // Contribution 52 { Avm_DECLARE_VIEWS(52); - auto tmp = (avm_alu_op_cast * (avm_alu_a_lo_shift - avm_alu_p_sub_a_lo)); + auto tmp = (avm_alu_op_cast * (avm_alu_a_hi_shift - avm_alu_p_sub_a_hi)); tmp *= scaling_factor; std::get<52>(evals) += tmp; } @@ -805,7 +806,7 @@ template class avm_aluImpl { { Avm_DECLARE_VIEWS(53); - auto tmp = (avm_alu_op_cast * (avm_alu_a_hi_shift - avm_alu_p_sub_a_hi)); + auto tmp = (((avm_alu_op_mul * avm_alu_ff_tag) + avm_alu_op_cast) * avm_alu_alu_sel_shift); tmp *= scaling_factor; std::get<53>(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 5531e8131b0..e427a1bf7be 100644 --- a/barretenberg/cpp/src/barretenberg/relations/generated/avm/declare_views.hpp +++ b/barretenberg/cpp/src/barretenberg/relations/generated/avm/declare_views.hpp @@ -219,6 +219,7 @@ [[maybe_unused]] auto lookup_u16_14_counts = View(new_term.lookup_u16_14_counts); \ [[maybe_unused]] auto avm_alu_a_hi_shift = View(new_term.avm_alu_a_hi_shift); \ [[maybe_unused]] auto avm_alu_a_lo_shift = View(new_term.avm_alu_a_lo_shift); \ + [[maybe_unused]] auto avm_alu_alu_sel_shift = View(new_term.avm_alu_alu_sel_shift); \ [[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); \ 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 221702456b1..4bfaa9fa499 100644 --- a/barretenberg/cpp/src/barretenberg/vm/generated/avm_circuit_builder.hpp +++ b/barretenberg/cpp/src/barretenberg/vm/generated/avm_circuit_builder.hpp @@ -268,6 +268,7 @@ template struct AvmFullRow { FF lookup_u16_14_counts{}; FF avm_alu_a_hi_shift{}; FF avm_alu_a_lo_shift{}; + FF avm_alu_alu_sel_shift{}; FF avm_alu_b_hi_shift{}; FF avm_alu_b_lo_shift{}; FF avm_alu_cmp_rng_ctr_shift{}; @@ -315,7 +316,7 @@ class AvmCircuitBuilder { using Polynomial = Flavor::Polynomial; using ProverPolynomials = Flavor::ProverPolynomials; - static constexpr size_t num_fixed_columns = 252; + static constexpr size_t num_fixed_columns = 253; static constexpr size_t num_polys = 215; std::vector rows; @@ -520,6 +521,7 @@ class AvmCircuitBuilder { polys.avm_alu_a_hi_shift = Polynomial(polys.avm_alu_a_hi.shifted()); polys.avm_alu_a_lo_shift = Polynomial(polys.avm_alu_a_lo.shifted()); + polys.avm_alu_alu_sel_shift = Polynomial(polys.avm_alu_alu_sel.shifted()); 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()); diff --git a/barretenberg/cpp/src/barretenberg/vm/generated/avm_flavor.hpp b/barretenberg/cpp/src/barretenberg/vm/generated/avm_flavor.hpp index fbd3f58d4c8..bcdaabdbd6c 100644 --- a/barretenberg/cpp/src/barretenberg/vm/generated/avm_flavor.hpp +++ b/barretenberg/cpp/src/barretenberg/vm/generated/avm_flavor.hpp @@ -73,7 +73,7 @@ class AvmFlavor { 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 = 252; + static constexpr size_t NUM_ALL_ENTITIES = 253; using GrandProductRelations = std::tuple, perm_main_bin_relation, @@ -827,6 +827,7 @@ class AvmFlavor { lookup_u16_14_counts, avm_alu_a_hi_shift, avm_alu_a_lo_shift, + avm_alu_alu_sel_shift, avm_alu_b_hi_shift, avm_alu_b_lo_shift, avm_alu_cmp_rng_ctr_shift, @@ -1082,6 +1083,7 @@ class AvmFlavor { lookup_u16_14_counts, avm_alu_a_hi_shift, avm_alu_a_lo_shift, + avm_alu_alu_sel_shift, avm_alu_b_hi_shift, avm_alu_b_lo_shift, avm_alu_cmp_rng_ctr_shift, @@ -1338,37 +1340,84 @@ 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_cmp_sel, avm_alu_op_add, avm_alu_op_cast_prev, - avm_alu_op_cast, 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, + return { avm_alu_a_hi, + avm_alu_a_lo, + avm_alu_alu_sel, + avm_alu_b_hi, + avm_alu_b_lo, + avm_alu_cmp_rng_ctr, + avm_alu_cmp_sel, + avm_alu_op_add, + avm_alu_op_cast_prev, + avm_alu_op_cast, + 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_cmp_sel_shift, - avm_alu_op_add_shift, avm_alu_op_cast_prev_shift, - avm_alu_op_cast_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, 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, - avm_main_pc_shift, avm_mem_addr_shift, - avm_mem_rw_shift, avm_mem_tag_shift, + return { avm_alu_a_hi_shift, + avm_alu_a_lo_shift, + avm_alu_alu_sel_shift, + 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_cast_prev_shift, + avm_alu_op_cast_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, + 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, + avm_main_pc_shift, + avm_mem_addr_shift, + avm_mem_rw_shift, + avm_mem_tag_shift, avm_mem_val_shift }; }; }; @@ -1382,15 +1431,43 @@ 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_cmp_sel, avm_alu_op_add, avm_alu_op_cast_prev, - avm_alu_op_cast, 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, + return { avm_alu_a_hi, + avm_alu_a_lo, + avm_alu_alu_sel, + avm_alu_b_hi, + avm_alu_b_lo, + avm_alu_cmp_rng_ctr, + avm_alu_cmp_sel, + avm_alu_op_add, + avm_alu_op_cast_prev, + avm_alu_op_cast, + 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 }; };