diff --git a/barretenberg/cpp/pil/avm/avm_main.pil b/barretenberg/cpp/pil/avm/avm_main.pil index efbbeeed2dcc..59264c8ddd6b 100644 --- a/barretenberg/cpp/pil/avm/avm_main.pil +++ b/barretenberg/cpp/pil/avm/avm_main.pil @@ -107,11 +107,6 @@ namespace avm_main(256); // TODO: Constrain rwa, rwb, rwc to u32 type and 0 <= in_tag <= 6 - // Set intermediate registers to 0 whenever tag_err occurs - tag_err * ia = 0; - tag_err * ib = 0; - tag_err * ic = 0; - // Relation for division over the finite field // If tag_err == 1 in a division, then ib == 0 and op_err == 1. #[SUBOP_DIVISION_FF] diff --git a/barretenberg/cpp/src/barretenberg/flavor/generated/avm_flavor.hpp b/barretenberg/cpp/src/barretenberg/flavor/generated/avm_flavor.hpp index c07e3bbe98df..6122675cb609 100644 --- a/barretenberg/cpp/src/barretenberg/flavor/generated/avm_flavor.hpp +++ b/barretenberg/cpp/src/barretenberg/flavor/generated/avm_flavor.hpp @@ -45,7 +45,7 @@ class AvmFlavor { static constexpr size_t NUM_ALL_ENTITIES = 90; using Relations = - std::tuple, Avm_vm::avm_alu, Avm_vm::avm_main, equiv_inter_reg_alu_relation>; + std::tuple, Avm_vm::avm_alu, Avm_vm::avm_mem, equiv_inter_reg_alu_relation>; static constexpr size_t MAX_PARTIAL_RELATION_LENGTH = compute_max_partial_relation_length(); @@ -313,20 +313,20 @@ class AvmFlavor { equiv_inter_reg_alu, equiv_tag_err, equiv_tag_err_counts, - avm_mem_m_addr_shift, - avm_mem_m_rw_shift, - avm_mem_m_val_shift, - avm_mem_m_tag_shift, + avm_main_internal_return_ptr_shift, + avm_main_pc_shift, + avm_alu_alu_u16_r7_shift, + avm_alu_alu_u16_r3_shift, + avm_alu_alu_u16_r0_shift, + avm_alu_alu_u16_r2_shift, avm_alu_alu_u16_r1_shift, avm_alu_alu_u16_r5_shift, - avm_alu_alu_u16_r6_shift, - avm_alu_alu_u16_r2_shift, - avm_alu_alu_u16_r3_shift, avm_alu_alu_u16_r4_shift, - avm_alu_alu_u16_r0_shift, - avm_alu_alu_u16_r7_shift, - avm_main_internal_return_ptr_shift, - avm_main_pc_shift) + avm_alu_alu_u16_r6_shift, + avm_mem_m_addr_shift, + avm_mem_m_rw_shift, + avm_mem_m_val_shift, + avm_mem_m_tag_shift) RefVector get_wires() { @@ -406,20 +406,20 @@ class AvmFlavor { equiv_inter_reg_alu, equiv_tag_err, equiv_tag_err_counts, - avm_mem_m_addr_shift, - avm_mem_m_rw_shift, - avm_mem_m_val_shift, - avm_mem_m_tag_shift, + avm_main_internal_return_ptr_shift, + avm_main_pc_shift, + avm_alu_alu_u16_r7_shift, + avm_alu_alu_u16_r3_shift, + avm_alu_alu_u16_r0_shift, + avm_alu_alu_u16_r2_shift, avm_alu_alu_u16_r1_shift, avm_alu_alu_u16_r5_shift, - avm_alu_alu_u16_r6_shift, - avm_alu_alu_u16_r2_shift, - avm_alu_alu_u16_r3_shift, avm_alu_alu_u16_r4_shift, - avm_alu_alu_u16_r0_shift, - avm_alu_alu_u16_r7_shift, - avm_main_internal_return_ptr_shift, - avm_main_pc_shift }; + avm_alu_alu_u16_r6_shift, + avm_mem_m_addr_shift, + avm_mem_m_rw_shift, + avm_mem_m_val_shift, + avm_mem_m_tag_shift }; }; RefVector get_unshifted() { @@ -502,37 +502,37 @@ class AvmFlavor { }; RefVector get_to_be_shifted() { - return { avm_mem_m_addr, - avm_mem_m_rw, - avm_mem_m_val, - avm_mem_m_tag, + return { avm_main_internal_return_ptr, + avm_main_pc, + avm_alu_alu_u16_r7, + avm_alu_alu_u16_r3, + avm_alu_alu_u16_r0, + avm_alu_alu_u16_r2, avm_alu_alu_u16_r1, avm_alu_alu_u16_r5, - avm_alu_alu_u16_r6, - avm_alu_alu_u16_r2, - avm_alu_alu_u16_r3, avm_alu_alu_u16_r4, - avm_alu_alu_u16_r0, - avm_alu_alu_u16_r7, - avm_main_internal_return_ptr, - avm_main_pc }; + avm_alu_alu_u16_r6, + avm_mem_m_addr, + avm_mem_m_rw, + avm_mem_m_val, + avm_mem_m_tag }; }; RefVector get_shifted() { - return { avm_mem_m_addr_shift, - avm_mem_m_rw_shift, - avm_mem_m_val_shift, - avm_mem_m_tag_shift, + return { avm_main_internal_return_ptr_shift, + avm_main_pc_shift, + avm_alu_alu_u16_r7_shift, + avm_alu_alu_u16_r3_shift, + avm_alu_alu_u16_r0_shift, + avm_alu_alu_u16_r2_shift, avm_alu_alu_u16_r1_shift, avm_alu_alu_u16_r5_shift, - avm_alu_alu_u16_r6_shift, - avm_alu_alu_u16_r2_shift, - avm_alu_alu_u16_r3_shift, avm_alu_alu_u16_r4_shift, - avm_alu_alu_u16_r0_shift, - avm_alu_alu_u16_r7_shift, - avm_main_internal_return_ptr_shift, - avm_main_pc_shift }; + avm_alu_alu_u16_r6_shift, + avm_mem_m_addr_shift, + avm_mem_m_rw_shift, + avm_mem_m_val_shift, + avm_mem_m_tag_shift }; }; }; @@ -545,20 +545,20 @@ class AvmFlavor { RefVector get_to_be_shifted() { - return { avm_mem_m_addr, - avm_mem_m_rw, - avm_mem_m_val, - avm_mem_m_tag, + return { avm_main_internal_return_ptr, + avm_main_pc, + avm_alu_alu_u16_r7, + avm_alu_alu_u16_r3, + avm_alu_alu_u16_r0, + avm_alu_alu_u16_r2, avm_alu_alu_u16_r1, avm_alu_alu_u16_r5, - avm_alu_alu_u16_r6, - avm_alu_alu_u16_r2, - avm_alu_alu_u16_r3, avm_alu_alu_u16_r4, - avm_alu_alu_u16_r0, - avm_alu_alu_u16_r7, - avm_main_internal_return_ptr, - avm_main_pc }; + avm_alu_alu_u16_r6, + avm_mem_m_addr, + avm_mem_m_rw, + avm_mem_m_val, + avm_mem_m_tag }; }; // The plookup wires that store plookup read data. diff --git a/barretenberg/cpp/src/barretenberg/proof_system/circuit_builder/generated/avm_circuit_builder.hpp b/barretenberg/cpp/src/barretenberg/proof_system/circuit_builder/generated/avm_circuit_builder.hpp index e2a52570b6a5..e727494f6df5 100644 --- a/barretenberg/cpp/src/barretenberg/proof_system/circuit_builder/generated/avm_circuit_builder.hpp +++ b/barretenberg/cpp/src/barretenberg/proof_system/circuit_builder/generated/avm_circuit_builder.hpp @@ -97,20 +97,20 @@ template struct AvmFullRow { FF equiv_inter_reg_alu{}; FF equiv_tag_err{}; FF equiv_tag_err_counts{}; + FF avm_main_internal_return_ptr_shift{}; + FF avm_main_pc_shift{}; + FF avm_alu_alu_u16_r7_shift{}; + FF avm_alu_alu_u16_r3_shift{}; + FF avm_alu_alu_u16_r0_shift{}; + FF avm_alu_alu_u16_r2_shift{}; + FF avm_alu_alu_u16_r1_shift{}; + FF avm_alu_alu_u16_r5_shift{}; + FF avm_alu_alu_u16_r4_shift{}; + FF avm_alu_alu_u16_r6_shift{}; FF avm_mem_m_addr_shift{}; FF avm_mem_m_rw_shift{}; FF avm_mem_m_val_shift{}; FF avm_mem_m_tag_shift{}; - FF avm_alu_alu_u16_r1_shift{}; - FF avm_alu_alu_u16_r5_shift{}; - FF avm_alu_alu_u16_r6_shift{}; - FF avm_alu_alu_u16_r2_shift{}; - FF avm_alu_alu_u16_r3_shift{}; - FF avm_alu_alu_u16_r4_shift{}; - FF avm_alu_alu_u16_r0_shift{}; - FF avm_alu_alu_u16_r7_shift{}; - FF avm_main_internal_return_ptr_shift{}; - FF avm_main_pc_shift{}; }; class AvmCircuitBuilder { @@ -218,20 +218,20 @@ class AvmCircuitBuilder { polys.equiv_tag_err_counts[i] = rows[i].equiv_tag_err_counts; } + polys.avm_main_internal_return_ptr_shift = Polynomial(polys.avm_main_internal_return_ptr.shifted()); + polys.avm_main_pc_shift = Polynomial(polys.avm_main_pc.shifted()); + polys.avm_alu_alu_u16_r7_shift = Polynomial(polys.avm_alu_alu_u16_r7.shifted()); + polys.avm_alu_alu_u16_r3_shift = Polynomial(polys.avm_alu_alu_u16_r3.shifted()); + polys.avm_alu_alu_u16_r0_shift = Polynomial(polys.avm_alu_alu_u16_r0.shifted()); + polys.avm_alu_alu_u16_r2_shift = Polynomial(polys.avm_alu_alu_u16_r2.shifted()); + polys.avm_alu_alu_u16_r1_shift = Polynomial(polys.avm_alu_alu_u16_r1.shifted()); + polys.avm_alu_alu_u16_r5_shift = Polynomial(polys.avm_alu_alu_u16_r5.shifted()); + polys.avm_alu_alu_u16_r4_shift = Polynomial(polys.avm_alu_alu_u16_r4.shifted()); + polys.avm_alu_alu_u16_r6_shift = Polynomial(polys.avm_alu_alu_u16_r6.shifted()); polys.avm_mem_m_addr_shift = Polynomial(polys.avm_mem_m_addr.shifted()); polys.avm_mem_m_rw_shift = Polynomial(polys.avm_mem_m_rw.shifted()); polys.avm_mem_m_val_shift = Polynomial(polys.avm_mem_m_val.shifted()); polys.avm_mem_m_tag_shift = Polynomial(polys.avm_mem_m_tag.shifted()); - polys.avm_alu_alu_u16_r1_shift = Polynomial(polys.avm_alu_alu_u16_r1.shifted()); - polys.avm_alu_alu_u16_r5_shift = Polynomial(polys.avm_alu_alu_u16_r5.shifted()); - polys.avm_alu_alu_u16_r6_shift = Polynomial(polys.avm_alu_alu_u16_r6.shifted()); - polys.avm_alu_alu_u16_r2_shift = Polynomial(polys.avm_alu_alu_u16_r2.shifted()); - polys.avm_alu_alu_u16_r3_shift = Polynomial(polys.avm_alu_alu_u16_r3.shifted()); - polys.avm_alu_alu_u16_r4_shift = Polynomial(polys.avm_alu_alu_u16_r4.shifted()); - polys.avm_alu_alu_u16_r0_shift = Polynomial(polys.avm_alu_alu_u16_r0.shifted()); - polys.avm_alu_alu_u16_r7_shift = Polynomial(polys.avm_alu_alu_u16_r7.shifted()); - polys.avm_main_internal_return_ptr_shift = Polynomial(polys.avm_main_internal_return_ptr.shifted()); - polys.avm_main_pc_shift = Polynomial(polys.avm_main_pc.shifted()); return polys; } @@ -303,16 +303,16 @@ class AvmCircuitBuilder { return true; }; - if (!evaluate_relation.template operator()>("avm_mem", - Avm_vm::get_relation_label_avm_mem)) { + if (!evaluate_relation.template operator()>("avm_main", + Avm_vm::get_relation_label_avm_main)) { return false; } if (!evaluate_relation.template operator()>("avm_alu", Avm_vm::get_relation_label_avm_alu)) { return false; } - if (!evaluate_relation.template operator()>("avm_main", - Avm_vm::get_relation_label_avm_main)) { + if (!evaluate_relation.template operator()>("avm_mem", + Avm_vm::get_relation_label_avm_mem)) { return false; } 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 0015b3e9927e..b4562949aca8 100644 --- a/barretenberg/cpp/src/barretenberg/relations/generated/avm/avm_alu.hpp +++ b/barretenberg/cpp/src/barretenberg/relations/generated/avm/avm_alu.hpp @@ -7,42 +7,42 @@ namespace bb::Avm_vm { template struct Avm_aluRow { - FF avm_alu_alu_u16_r6{}; + FF avm_alu_alu_op_mul{}; FF avm_alu_alu_u16_r3{}; - FF avm_alu_alu_op_add{}; - FF avm_alu_alu_u16_r5{}; - FF avm_alu_alu_u8_r0{}; - FF avm_alu_alu_u16_r4{}; + FF avm_alu_alu_ib{}; FF avm_alu_alu_op_sub{}; - FF avm_alu_alu_op_mul{}; - FF avm_alu_alu_u16_r7{}; - FF avm_alu_alu_u16_r1_shift{}; - FF avm_alu_alu_sel{}; - FF avm_alu_alu_u16_r5_shift{}; - FF avm_alu_alu_op_eq{}; - FF avm_alu_alu_u128_tag{}; - FF avm_alu_alu_op_eq_diff_inv{}; - FF avm_alu_alu_u16_r6_shift{}; - FF avm_alu_alu_u64_tag{}; - FF avm_alu_alu_u16_r2_shift{}; + FF avm_alu_alu_u64_r0{}; FF avm_alu_alu_u16_r1{}; - FF avm_alu_alu_ic{}; - FF avm_alu_alu_u8_tag{}; - FF avm_alu_alu_u32_tag{}; - FF avm_alu_alu_u8_r1{}; - FF avm_alu_alu_ib{}; - FF avm_alu_alu_u16_tag{}; FF avm_alu_alu_u16_r2{}; - FF avm_alu_alu_ia{}; - FF avm_alu_alu_u16_r3_shift{}; - FF avm_alu_alu_u64_r0{}; FF avm_alu_alu_ff_tag{}; - FF avm_alu_alu_u16_r0{}; - FF avm_alu_alu_u16_r4_shift{}; + FF avm_alu_alu_u128_tag{}; + FF avm_alu_alu_u16_tag{}; + FF avm_alu_alu_sel{}; + FF avm_alu_alu_u8_r0{}; + FF avm_alu_alu_u16_r7_shift{}; + FF avm_alu_alu_u16_r3_shift{}; FF avm_alu_alu_u16_r0_shift{}; + FF avm_alu_alu_u16_r2_shift{}; + FF avm_alu_alu_u16_r5{}; + FF avm_alu_alu_u8_tag{}; + FF avm_alu_alu_u16_r1_shift{}; + FF avm_alu_alu_op_eq{}; + FF avm_alu_alu_u16_r5_shift{}; + FF avm_alu_alu_ic{}; + FF avm_alu_alu_u16_r6{}; + FF avm_alu_alu_u16_r4_shift{}; + FF avm_alu_alu_u8_r1{}; + FF avm_alu_alu_u16_r6_shift{}; + FF avm_alu_alu_u16_r7{}; FF avm_alu_alu_cf{}; - FF avm_alu_alu_u16_r7_shift{}; FF avm_alu_alu_op_not{}; + FF avm_alu_alu_op_add{}; + FF avm_alu_alu_ia{}; + FF avm_alu_alu_u16_r4{}; + FF avm_alu_alu_u64_tag{}; + FF avm_alu_alu_u16_r0{}; + FF avm_alu_alu_op_eq_diff_inv{}; + FF avm_alu_alu_u32_tag{}; }; inline std::string get_relation_label_avm_alu(int index) @@ -54,29 +54,29 @@ inline std::string get_relation_label_avm_alu(int index) case 11: return "ALU_MUL_COMMON_2"; - case 16: - return "ALU_OP_NOT"; + case 14: + return "ALU_MULTIPLICATION_OUT_U128"; case 10: return "ALU_MUL_COMMON_1"; - case 9: - return "ALU_MULTIPLICATION_FF"; - - case 17: - return "ALU_RES_IS_BOOL"; - case 18: return "ALU_OP_EQ"; + case 8: + return "ALU_ADD_SUB_2"; + case 15: return "ALU_FF_NOT_XOR"; - case 8: - return "ALU_ADD_SUB_2"; + case 17: + return "ALU_RES_IS_BOOL"; - case 14: - return "ALU_MULTIPLICATION_OUT_U128"; + case 9: + return "ALU_MULTIPLICATION_FF"; + + case 16: + return "ALU_OP_NOT"; } return std::to_string(index); } 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 1663eb501b25..392409d249aa 100644 --- a/barretenberg/cpp/src/barretenberg/relations/generated/avm/avm_main.hpp +++ b/barretenberg/cpp/src/barretenberg/relations/generated/avm/avm_main.hpp @@ -7,64 +7,64 @@ namespace bb::Avm_vm { template struct Avm_mainRow { - FF avm_main_mem_op_a{}; - FF avm_main_mem_idx_b{}; - FF avm_main_sel_op_not{}; - FF avm_main_op_err{}; - FF avm_main_rwa{}; + FF avm_main_mem_idx_a{}; + FF avm_main_sel_op_eq{}; + FF avm_main_rwc{}; + FF avm_main_mem_op_c{}; FF avm_main_internal_return_ptr_shift{}; - FF avm_main_sel_op_mul{}; - FF avm_main_alu_sel{}; - FF avm_main_sel_op_add{}; - FF avm_main_pc_shift{}; - FF avm_main_sel_jump{}; - FF avm_main_sel_internal_call{}; + FF avm_main_pc{}; + FF avm_main_internal_return_ptr{}; + FF avm_main_ia{}; + FF avm_main_mem_idx_b{}; FF avm_main_ic{}; FF avm_main_sel_internal_return{}; - FF avm_main_sel_op_sub{}; - FF avm_main_sel_op_eq{}; - FF avm_main_inv{}; + FF avm_main_sel_op_mul{}; + FF avm_main_mem_op_a{}; FF avm_main_mem_op_b{}; - FF avm_main_internal_return_ptr{}; + FF avm_main_rwa{}; FF avm_main_tag_err{}; - FF avm_main_mem_op_c{}; - FF avm_main_mem_idx_a{}; - FF avm_main_rwc{}; - FF avm_main_pc{}; - FF avm_main_first{}; + FF avm_main_sel_op_sub{}; FF avm_main_ib{}; - FF avm_main_ia{}; - FF avm_main_rwb{}; + FF avm_main_sel_op_not{}; FF avm_main_sel_halt{}; + FF avm_main_rwb{}; + FF avm_main_first{}; + FF avm_main_sel_op_add{}; + FF avm_main_pc_shift{}; + FF avm_main_alu_sel{}; FF avm_main_sel_op_div{}; + FF avm_main_sel_internal_call{}; + FF avm_main_sel_jump{}; + FF avm_main_inv{}; + FF avm_main_op_err{}; }; inline std::string get_relation_label_avm_main(int index) { switch (index) { - case 32: - return "RETURN_POINTER_DECREMENT"; - - case 23: + case 20: return "SUBOP_DIVISION_ZERO_ERR2"; - case 21: + case 18: return "SUBOP_DIVISION_FF"; - case 22: - return "SUBOP_DIVISION_ZERO_ERR1"; + case 23: + return "RETURN_POINTER_INCREMENT"; + + case 29: + return "RETURN_POINTER_DECREMENT"; - case 37: + case 34: return "PC_INCREMENT"; - case 38: - return "INTERNAL_RETURN_POINTER_CONSISTENCY"; + case 19: + return "SUBOP_DIVISION_ZERO_ERR1"; - case 24: + case 21: return "SUBOP_ERROR_RELEVANT_OP"; - case 26: - return "RETURN_POINTER_INCREMENT"; + case 35: + return "INTERNAL_RETURN_POINTER_CONSISTENCY"; } return std::to_string(index); } @@ -73,9 +73,8 @@ 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, 5, 4, 4, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 5, 3, 3, + 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, 5, 4, 4, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 5, 3, 3, }; template @@ -233,7 +232,8 @@ template class avm_mainImpl { { Avm_DECLARE_VIEWS(18); - auto tmp = (avm_main_tag_err * avm_main_ia); + 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<18>(evals) += tmp; } @@ -241,7 +241,7 @@ template class avm_mainImpl { { Avm_DECLARE_VIEWS(19); - auto tmp = (avm_main_tag_err * avm_main_ib); + auto tmp = (avm_main_sel_op_div * (((avm_main_ib * avm_main_inv) - FF(1)) + avm_main_op_err)); tmp *= scaling_factor; std::get<19>(evals) += tmp; } @@ -249,7 +249,7 @@ template class avm_mainImpl { { Avm_DECLARE_VIEWS(20); - auto tmp = (avm_main_tag_err * avm_main_ic); + auto tmp = ((avm_main_sel_op_div * avm_main_op_err) * (-avm_main_inv + FF(1))); tmp *= scaling_factor; std::get<20>(evals) += tmp; } @@ -257,8 +257,7 @@ template class avm_mainImpl { { Avm_DECLARE_VIEWS(21); - 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_op_err * (avm_main_sel_op_div - FF(1))); tmp *= scaling_factor; std::get<21>(evals) += tmp; } @@ -266,7 +265,7 @@ template class avm_mainImpl { { Avm_DECLARE_VIEWS(22); - auto tmp = (avm_main_sel_op_div * (((avm_main_ib * avm_main_inv) - FF(1)) + avm_main_op_err)); + auto tmp = (avm_main_sel_jump * (avm_main_pc_shift - avm_main_ia)); tmp *= scaling_factor; std::get<22>(evals) += tmp; } @@ -274,7 +273,8 @@ template class avm_mainImpl { { Avm_DECLARE_VIEWS(23); - 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_internal_return_ptr_shift - (avm_main_internal_return_ptr + FF(1)))); tmp *= scaling_factor; std::get<23>(evals) += tmp; } @@ -282,7 +282,7 @@ template class avm_mainImpl { { Avm_DECLARE_VIEWS(24); - auto tmp = (avm_main_op_err * (avm_main_sel_op_div - FF(1))); + auto tmp = (avm_main_sel_internal_call * (avm_main_internal_return_ptr - avm_main_mem_idx_b)); tmp *= scaling_factor; std::get<24>(evals) += tmp; } @@ -290,7 +290,7 @@ template class avm_mainImpl { { Avm_DECLARE_VIEWS(25); - auto tmp = (avm_main_sel_jump * (avm_main_pc_shift - avm_main_ia)); + auto tmp = (avm_main_sel_internal_call * (avm_main_pc_shift - avm_main_ia)); tmp *= scaling_factor; std::get<25>(evals) += tmp; } @@ -298,8 +298,7 @@ template class avm_mainImpl { { Avm_DECLARE_VIEWS(26); - 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_call * ((avm_main_pc + FF(1)) - avm_main_ib)); tmp *= scaling_factor; std::get<26>(evals) += tmp; } @@ -307,7 +306,7 @@ template class avm_mainImpl { { Avm_DECLARE_VIEWS(27); - auto tmp = (avm_main_sel_internal_call * (avm_main_internal_return_ptr - avm_main_mem_idx_b)); + auto tmp = (avm_main_sel_internal_call * (avm_main_rwb - FF(1))); tmp *= scaling_factor; std::get<27>(evals) += tmp; } @@ -315,7 +314,7 @@ template class avm_mainImpl { { Avm_DECLARE_VIEWS(28); - auto tmp = (avm_main_sel_internal_call * (avm_main_pc_shift - avm_main_ia)); + auto tmp = (avm_main_sel_internal_call * (avm_main_mem_op_b - FF(1))); tmp *= scaling_factor; std::get<28>(evals) += tmp; } @@ -323,7 +322,8 @@ template class avm_mainImpl { { Avm_DECLARE_VIEWS(29); - auto tmp = (avm_main_sel_internal_call * ((avm_main_pc + FF(1)) - avm_main_ib)); + 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<29>(evals) += tmp; } @@ -331,7 +331,7 @@ template class avm_mainImpl { { Avm_DECLARE_VIEWS(30); - auto tmp = (avm_main_sel_internal_call * (avm_main_rwb - 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<30>(evals) += tmp; } @@ -339,7 +339,7 @@ template class avm_mainImpl { { Avm_DECLARE_VIEWS(31); - auto tmp = (avm_main_sel_internal_call * (avm_main_mem_op_b - FF(1))); + auto tmp = (avm_main_sel_internal_return * (avm_main_pc_shift - avm_main_ia)); tmp *= scaling_factor; std::get<31>(evals) += tmp; } @@ -347,8 +347,7 @@ template class avm_mainImpl { { Avm_DECLARE_VIEWS(32); - 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_internal_return * avm_main_rwa); tmp *= scaling_factor; std::get<32>(evals) += tmp; } @@ -356,7 +355,7 @@ template class avm_mainImpl { { Avm_DECLARE_VIEWS(33); - auto tmp = (avm_main_sel_internal_return * ((avm_main_internal_return_ptr - FF(1)) - avm_main_mem_idx_a)); + auto tmp = (avm_main_sel_internal_return * (avm_main_mem_op_a - FF(1))); tmp *= scaling_factor; std::get<33>(evals) += tmp; } @@ -364,59 +363,35 @@ template class avm_mainImpl { { Avm_DECLARE_VIEWS(34); - auto tmp = (avm_main_sel_internal_return * (avm_main_pc_shift - avm_main_ia)); - tmp *= scaling_factor; - std::get<34>(evals) += tmp; - } - // Contribution 35 - { - Avm_DECLARE_VIEWS(35); - - auto tmp = (avm_main_sel_internal_return * avm_main_rwa); - tmp *= scaling_factor; - std::get<35>(evals) += tmp; - } - // Contribution 36 - { - Avm_DECLARE_VIEWS(36); - - auto tmp = (avm_main_sel_internal_return * (avm_main_mem_op_a - FF(1))); - tmp *= scaling_factor; - std::get<36>(evals) += tmp; - } - // Contribution 37 - { - Avm_DECLARE_VIEWS(37); - 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_pc_shift - (avm_main_pc + FF(1)))); tmp *= scaling_factor; - std::get<37>(evals) += tmp; + std::get<34>(evals) += tmp; } - // Contribution 38 + // Contribution 35 { - Avm_DECLARE_VIEWS(38); + Avm_DECLARE_VIEWS(35); 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<38>(evals) += tmp; + std::get<35>(evals) += tmp; } - // Contribution 39 + // Contribution 36 { - Avm_DECLARE_VIEWS(39); + Avm_DECLARE_VIEWS(36); 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<39>(evals) += tmp; + std::get<36>(evals) += tmp; } } }; diff --git a/barretenberg/cpp/src/barretenberg/relations/generated/avm/avm_mem.hpp b/barretenberg/cpp/src/barretenberg/relations/generated/avm/avm_mem.hpp index 182e0425c6ea..815692aa2d28 100644 --- a/barretenberg/cpp/src/barretenberg/relations/generated/avm/avm_mem.hpp +++ b/barretenberg/cpp/src/barretenberg/relations/generated/avm/avm_mem.hpp @@ -7,39 +7,39 @@ namespace bb::Avm_vm { template struct Avm_memRow { - FF avm_mem_m_addr{}; - FF avm_mem_m_in_tag{}; FF avm_mem_m_rw{}; - FF avm_mem_m_lastAccess{}; - FF avm_mem_m_last{}; + FF avm_mem_m_tag{}; FF avm_mem_m_addr_shift{}; FF avm_mem_m_rw_shift{}; + FF avm_mem_m_lastAccess{}; FF avm_mem_m_val_shift{}; - FF avm_mem_m_tag_err{}; - FF avm_mem_m_val{}; - FF avm_mem_m_tag{}; - FF avm_mem_m_one_min_inv{}; FF avm_mem_m_tag_shift{}; + FF avm_mem_m_addr{}; + FF avm_mem_m_one_min_inv{}; + FF avm_mem_m_last{}; + FF avm_mem_m_val{}; + FF avm_mem_m_in_tag{}; + FF avm_mem_m_tag_err{}; }; inline std::string get_relation_label_avm_mem(int index) { switch (index) { + case 4: + return "MEM_LAST_ACCESS_DELIMITER"; + case 7: return "MEM_ZERO_INIT"; + case 5: + return "MEM_READ_WRITE_VAL_CONSISTENCY"; + case 9: return "MEM_IN_TAG_CONSISTENCY_2"; - case 4: - return "MEM_LAST_ACCESS_DELIMITER"; - case 8: return "MEM_IN_TAG_CONSISTENCY_1"; - case 5: - return "MEM_READ_WRITE_VAL_CONSISTENCY"; - case 6: return "MEM_READ_WRITE_TAG_CONSISTENCY"; } 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 a42cd4de7a9f..1364f230845d 100644 --- a/barretenberg/cpp/src/barretenberg/relations/generated/avm/declare_views.hpp +++ b/barretenberg/cpp/src/barretenberg/relations/generated/avm/declare_views.hpp @@ -78,17 +78,17 @@ [[maybe_unused]] auto equiv_inter_reg_alu = View(new_term.equiv_inter_reg_alu); \ [[maybe_unused]] auto equiv_tag_err = View(new_term.equiv_tag_err); \ [[maybe_unused]] auto equiv_tag_err_counts = View(new_term.equiv_tag_err_counts); \ - [[maybe_unused]] auto avm_mem_m_addr_shift = View(new_term.avm_mem_m_addr_shift); \ - [[maybe_unused]] auto avm_mem_m_rw_shift = View(new_term.avm_mem_m_rw_shift); \ - [[maybe_unused]] auto avm_mem_m_val_shift = View(new_term.avm_mem_m_val_shift); \ - [[maybe_unused]] auto avm_mem_m_tag_shift = View(new_term.avm_mem_m_tag_shift); \ + [[maybe_unused]] auto avm_main_internal_return_ptr_shift = View(new_term.avm_main_internal_return_ptr_shift); \ + [[maybe_unused]] auto avm_main_pc_shift = View(new_term.avm_main_pc_shift); \ + [[maybe_unused]] auto avm_alu_alu_u16_r7_shift = View(new_term.avm_alu_alu_u16_r7_shift); \ + [[maybe_unused]] auto avm_alu_alu_u16_r3_shift = View(new_term.avm_alu_alu_u16_r3_shift); \ + [[maybe_unused]] auto avm_alu_alu_u16_r0_shift = View(new_term.avm_alu_alu_u16_r0_shift); \ + [[maybe_unused]] auto avm_alu_alu_u16_r2_shift = View(new_term.avm_alu_alu_u16_r2_shift); \ [[maybe_unused]] auto avm_alu_alu_u16_r1_shift = View(new_term.avm_alu_alu_u16_r1_shift); \ [[maybe_unused]] auto avm_alu_alu_u16_r5_shift = View(new_term.avm_alu_alu_u16_r5_shift); \ - [[maybe_unused]] auto avm_alu_alu_u16_r6_shift = View(new_term.avm_alu_alu_u16_r6_shift); \ - [[maybe_unused]] auto avm_alu_alu_u16_r2_shift = View(new_term.avm_alu_alu_u16_r2_shift); \ - [[maybe_unused]] auto avm_alu_alu_u16_r3_shift = View(new_term.avm_alu_alu_u16_r3_shift); \ [[maybe_unused]] auto avm_alu_alu_u16_r4_shift = View(new_term.avm_alu_alu_u16_r4_shift); \ - [[maybe_unused]] auto avm_alu_alu_u16_r0_shift = View(new_term.avm_alu_alu_u16_r0_shift); \ - [[maybe_unused]] auto avm_alu_alu_u16_r7_shift = View(new_term.avm_alu_alu_u16_r7_shift); \ - [[maybe_unused]] auto avm_main_internal_return_ptr_shift = View(new_term.avm_main_internal_return_ptr_shift); \ - [[maybe_unused]] auto avm_main_pc_shift = View(new_term.avm_main_pc_shift); + [[maybe_unused]] auto avm_alu_alu_u16_r6_shift = View(new_term.avm_alu_alu_u16_r6_shift); \ + [[maybe_unused]] auto avm_mem_m_addr_shift = View(new_term.avm_mem_m_addr_shift); \ + [[maybe_unused]] auto avm_mem_m_rw_shift = View(new_term.avm_mem_m_rw_shift); \ + [[maybe_unused]] auto avm_mem_m_val_shift = View(new_term.avm_mem_m_val_shift); \ + [[maybe_unused]] auto avm_mem_m_tag_shift = View(new_term.avm_mem_m_tag_shift); 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 b911fbf09cb0..c483da0f73f1 100644 --- a/barretenberg/cpp/src/barretenberg/vm/avm_trace/avm_trace.cpp +++ b/barretenberg/cpp/src/barretenberg/vm/avm_trace/avm_trace.cpp @@ -52,6 +52,8 @@ void AvmTraceBuilder::op_add(uint32_t a_offset, uint32_t b_offset, uint32_t dst_ // a + b = c FF a = tag_match ? read_a.val : FF(0); FF b = tag_match ? read_b.val : FF(0); + + // In case of a memory tag error, we must not generate an entry in the ALU table. FF c = tag_match ? alu_trace_builder.op_add(a, b, in_tag, clk) : FF(0); // Write into memory value c from intermediate register ic. @@ -97,6 +99,8 @@ void AvmTraceBuilder::op_sub(uint32_t a_offset, uint32_t b_offset, uint32_t dst_ // a - b = c FF a = tag_match ? read_a.val : FF(0); FF b = tag_match ? read_b.val : FF(0); + + // In case of a memory tag error, we must not generate an entry in the ALU table. FF c = tag_match ? alu_trace_builder.op_sub(a, b, in_tag, clk) : FF(0); // Write into memory value c from intermediate register ic. @@ -142,6 +146,8 @@ void AvmTraceBuilder::op_mul(uint32_t a_offset, uint32_t b_offset, uint32_t dst_ // a * b = c FF a = tag_match ? read_a.val : FF(0); FF b = tag_match ? read_b.val : FF(0); + + // In case of a memory tag error, we must not generate an entry in the ALU table. FF c = tag_match ? alu_trace_builder.op_mul(a, b, in_tag, clk) : FF(0); // Write into memory value c from intermediate register ic. @@ -243,11 +249,9 @@ void AvmTraceBuilder::op_not(uint32_t a_offset, uint32_t dst_offset, AvmMemoryTa // ~a = c FF a = read_a.tag_match ? read_a.val : FF(0); - // TODO(4613): If tag_match == false, then the value of c - // will not be zero which would not satisfy the constraint that - // ic == 0 whenever tag_err == 1. This constraint might be removed - // as part of #4613. - FF c = alu_trace_builder.op_not(a, in_tag, clk); + + // In case of a memory tag error, we must not generate an entry in the ALU table. + FF c = read_a.tag_match ? alu_trace_builder.op_not(a, in_tag, clk) : FF(0); // Write into memory value c from intermediate register ic. mem_trace_builder.write_into_memory(clk, IntermRegister::IC, dst_offset, c, in_tag); @@ -290,11 +294,8 @@ void AvmTraceBuilder::op_eq(uint32_t a_offset, uint32_t b_offset, uint32_t dst_o FF a = tag_match ? read_a.val : FF(0); FF b = tag_match ? read_b.val : FF(0); - // TODO(4613): If tag_match == false, then the value of c - // will not be zero which would not satisfy the constraint that - // ic == 0 whenever tag_err == 1. This constraint might be removed - // as part of #4613. - FF c = alu_trace_builder.op_eq(a, b, in_tag, clk); + // In case of a memory tag error, we must not generate an entry in the ALU table. + FF c = tag_match ? alu_trace_builder.op_eq(a, b, in_tag, clk) : FF(0); // Write into memory value c from intermediate register ic. mem_trace_builder.write_into_memory(clk, IntermRegister::IC, dst_offset, c, in_tag); diff --git a/barretenberg/cpp/src/barretenberg/vm/tests/avm_memory.test.cpp b/barretenberg/cpp/src/barretenberg/vm/tests/avm_memory.test.cpp index 815bf34d8b02..677770a1222e 100644 --- a/barretenberg/cpp/src/barretenberg/vm/tests/avm_memory.test.cpp +++ b/barretenberg/cpp/src/barretenberg/vm/tests/avm_memory.test.cpp @@ -1,4 +1,5 @@ #include "avm_common.test.hpp" +#include "barretenberg/vm/avm_trace/avm_common.hpp" using namespace bb; @@ -27,9 +28,9 @@ class AvmMemoryTests : public ::testing::Test { * trace is the focus. ******************************************************************************/ -// Testing an operation with a mismatched memory tag. +// Testing an addition operation with a mismatched memory tag. // The proof must pass and we check that the AVM error is raised. -TEST_F(AvmMemoryTests, mismatchedTag) +TEST_F(AvmMemoryTests, mismatchedTagAddOperation) { trace_builder.calldata_copy(0, 2, 0, std::vector{ 98, 12 }); @@ -49,7 +50,7 @@ TEST_F(AvmMemoryTests, mismatchedTag) auto clk = row->avm_main_clk; - // Find the memory trace position corresponding to the add sub-operation of register ia. + // Find the memory trace position corresponding to the load sub-operation of register ia. row = std::ranges::find_if(trace.begin(), trace.end(), [clk](Row r) { return r.avm_mem_m_clk == clk && r.avm_mem_m_sub_clk == AvmMemTraceBuilder::SUB_CLK_LOAD_A; }); @@ -74,6 +75,49 @@ TEST_F(AvmMemoryTests, mismatchedTag) validate_trace_proof(std::move(trace)); } +// Testing an equality operation with a mismatched memory tag. +// The proof must pass and we check that the AVM error is raised. +TEST_F(AvmMemoryTests, mismatchedTagEqOperation) +{ + trace_builder.set(3, 0, AvmMemoryTag::U32); + trace_builder.set(5, 1, AvmMemoryTag::U16); + + trace_builder.op_eq(0, 1, 2, AvmMemoryTag::U32); + trace_builder.halt(); + auto trace = trace_builder.finalize(); + + // Find the first row enabling the equality selector + auto row = std::ranges::find_if(trace.begin(), trace.end(), [](Row r) { return r.avm_main_sel_op_eq == FF(1); }); + + EXPECT_TRUE(row != trace.end()); + + auto clk = row->avm_main_clk; + + // Find the memory trace position corresponding to the load sub-operation of register ia. + row = std::ranges::find_if(trace.begin(), trace.end(), [clk](Row r) { + return r.avm_mem_m_clk == clk && r.avm_mem_m_sub_clk == AvmMemTraceBuilder::SUB_CLK_LOAD_A; + }); + + EXPECT_TRUE(row != trace.end()); + + EXPECT_EQ(row->avm_mem_m_tag_err, FF(0)); // Error is NOT raised + EXPECT_EQ(row->avm_mem_m_in_tag, FF(static_cast(AvmMemoryTag::U32))); + EXPECT_EQ(row->avm_mem_m_tag, FF(static_cast(AvmMemoryTag::U32))); + + // Find the memory trace position corresponding to the load sub-operation of register ib. + row = std::ranges::find_if(trace.begin(), trace.end(), [clk](Row r) { + return r.avm_mem_m_clk == clk && r.avm_mem_m_sub_clk == AvmMemTraceBuilder::SUB_CLK_LOAD_B; + }); + + EXPECT_TRUE(row != trace.end()); + + EXPECT_EQ(row->avm_mem_m_tag_err, FF(1)); // Error is raised + EXPECT_EQ(row->avm_mem_m_in_tag, FF(static_cast(AvmMemoryTag::U32))); + EXPECT_EQ(row->avm_mem_m_tag, FF(static_cast(AvmMemoryTag::U16))); + + validate_trace_proof(std::move(trace)); +} + // Testing violation that m_lastAccess is a delimiter for two different addresses // in the memory trace TEST_F(AvmMemoryTests, mLastAccessViolation)