diff --git a/barretenberg/cpp/pil/avm/avm_main.pil b/barretenberg/cpp/pil/avm/avm_main.pil index 37a32778bdb..ba2ce3d94d7 100644 --- a/barretenberg/cpp/pil/avm/avm_main.pil +++ b/barretenberg/cpp/pil/avm/avm_main.pil @@ -21,6 +21,9 @@ namespace avm_main(256); // Halt program execution pol commit sel_halt; + + //===== MEMORY OPCODES ========================================================== + pol commit sel_mov; //===== TABLE SUBOP-TR ======================================================== // Boolean selectors for (sub-)operations. Only one operation is activated at @@ -94,6 +97,9 @@ namespace avm_main(256); sel_jump * (1 - sel_jump) = 0; sel_halt * (1 - sel_halt) = 0; + // Might be removed if derived from opcode based on a lookup of constants + sel_mov * ( 1 - sel_mov) = 0; + op_err * (1 - op_err) = 0; tag_err * (1 - tag_err) = 0; // Potential optimization (boolean constraint derivation from equivalence check to avm_mem)? @@ -188,11 +194,17 @@ namespace avm_main(256); // TODO: we want to set an initial number for the reserved memory of the jump pointer - // Inter-table Constraints + //====== MEMORY OPCODES CONSTRAINTS ========================================= + #[MOV_SAME_VALUE] + sel_mov * (ia - ic) = 0; // Ensure that the correct value is moved/copied. + //====== Inter-table Constraints ============================================ #[INCL_MAIN_TAG_ERR] avm_mem.m_tag_err {avm_mem.m_clk} in tag_err {clk}; + #[INCL_MEM_TAG_ERR] + tag_err {clk} in avm_mem.m_tag_err {avm_mem.m_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: @@ -208,9 +220,9 @@ namespace avm_main(256); avm_alu.alu_op_not, avm_alu.alu_in_tag}; #[PERM_MAIN_MEM_A] - mem_op_a {clk, mem_idx_a, ia, rwa, in_tag} + mem_op_a {clk, mem_idx_a, ia, rwa, in_tag, sel_mov} is - avm_mem.m_op_a {avm_mem.m_clk, avm_mem.m_addr, avm_mem.m_val, avm_mem.m_rw, avm_mem.m_in_tag}; + avm_mem.m_op_a {avm_mem.m_clk, avm_mem.m_addr, avm_mem.m_val, avm_mem.m_rw, avm_mem.m_in_tag, avm_mem.m_sel_mov}; #[PERM_MAIN_MEM_B] mem_op_b {clk, mem_idx_b, ib, rwb, in_tag} diff --git a/barretenberg/cpp/pil/avm/avm_mem.pil b/barretenberg/cpp/pil/avm/avm_mem.pil index 356b05ee0ce..df862019cb6 100644 --- a/barretenberg/cpp/pil/avm/avm_mem.pil +++ b/barretenberg/cpp/pil/avm/avm_mem.pil @@ -20,6 +20,10 @@ namespace avm_mem(256); pol commit m_op_b; pol commit m_op_c; + // Selector for MOV opcode (copied from main trace for loading operation on intermediated register ia) + // Boolean constraint is performed in main trace. + pol commit m_sel_mov; + // Error columns pol commit m_tag_err; // Boolean (1 if m_in_tag != m_tag is detected) @@ -111,4 +115,15 @@ namespace avm_mem(256); // Correctness of two above checks MEM_IN_TAG_CONSISTENCY_1/2: // m_in_tag == m_tag ==> m_tag_err == 0 (first relation) - // m_tag_err == 0 ==> m_one_min_inv == 0 by second relation. First relation ==> m_in_tag - m_tag == 0 \ No newline at end of file + // m_tag_err == 0 ==> m_one_min_inv == 0 by second relation. First relation ==> m_in_tag - m_tag == 0 + + //====== MOV Opcode in_tag Constraint ===================================== + // The following constraint ensures that the m_in_tag is set to m_tag for + // the load operation pertaining to Ia. + // The permutation check #[PERM_MAIN_MEM_A] guarantees that the m_in_tag + // value load operation for Ia is copied back in the main trace. Then, + // #[PERM_MAIN_MEM_C] copies back m_in_tag for store operation from Ic. + // Finally, the following constraint guarantees that m_tag is correct for + // the output. + #[MOV_SAME_TAG] + m_sel_mov * m_tag_err = 0; // Equivalent to m_sel_mov * (m_in_tag - m_tag) = 0 \ No newline at end of file diff --git a/barretenberg/cpp/src/barretenberg/flavor/generated/avm_flavor.hpp b/barretenberg/cpp/src/barretenberg/flavor/generated/avm_flavor.hpp index 88ca63d463d..ea107e4c0e4 100644 --- a/barretenberg/cpp/src/barretenberg/flavor/generated/avm_flavor.hpp +++ b/barretenberg/cpp/src/barretenberg/flavor/generated/avm_flavor.hpp @@ -41,14 +41,14 @@ class AvmFlavor { using RelationSeparator = FF; static constexpr size_t NUM_PRECOMPUTED_ENTITIES = 2; - static constexpr size_t NUM_WITNESS_ENTITIES = 81; + static constexpr size_t NUM_WITNESS_ENTITIES = 85; 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 = 97; + static constexpr size_t NUM_ALL_ENTITIES = 101; - using Relations = std::tuple, - Avm_vm::avm_alu, + using Relations = std::tuple, + Avm_vm::avm_mem, Avm_vm::avm_main, perm_main_alu_relation, perm_main_mem_a_relation, @@ -99,6 +99,7 @@ class AvmFlavor { avm_mem_m_op_a, avm_mem_m_op_b, avm_mem_m_op_c, + avm_mem_m_sel_mov, avm_mem_m_tag_err, avm_mem_m_one_min_inv, avm_alu_alu_clk, @@ -138,6 +139,7 @@ class AvmFlavor { avm_main_sel_internal_return, avm_main_sel_jump, avm_main_sel_halt, + avm_main_sel_mov, avm_main_sel_op_add, avm_main_sel_op_sub, avm_main_sel_op_mul, @@ -167,7 +169,9 @@ class AvmFlavor { perm_main_mem_b, perm_main_mem_c, incl_main_tag_err, - incl_main_tag_err_counts) + incl_mem_tag_err, + incl_main_tag_err_counts, + incl_mem_tag_err_counts) RefVector get_wires() { @@ -183,6 +187,7 @@ class AvmFlavor { avm_mem_m_op_a, avm_mem_m_op_b, avm_mem_m_op_c, + avm_mem_m_sel_mov, avm_mem_m_tag_err, avm_mem_m_one_min_inv, avm_alu_alu_clk, @@ -222,6 +227,7 @@ class AvmFlavor { avm_main_sel_internal_return, avm_main_sel_jump, avm_main_sel_halt, + avm_main_sel_mov, avm_main_sel_op_add, avm_main_sel_op_sub, avm_main_sel_op_mul, @@ -251,7 +257,9 @@ class AvmFlavor { perm_main_mem_b, perm_main_mem_c, incl_main_tag_err, - incl_main_tag_err_counts }; + incl_mem_tag_err, + incl_main_tag_err_counts, + incl_mem_tag_err_counts }; }; RefVector get_sorted_polynomials() { return {}; }; }; @@ -273,6 +281,7 @@ class AvmFlavor { avm_mem_m_op_a, avm_mem_m_op_b, avm_mem_m_op_c, + avm_mem_m_sel_mov, avm_mem_m_tag_err, avm_mem_m_one_min_inv, avm_alu_alu_clk, @@ -312,6 +321,7 @@ class AvmFlavor { avm_main_sel_internal_return, avm_main_sel_jump, avm_main_sel_halt, + avm_main_sel_mov, avm_main_sel_op_add, avm_main_sel_op_sub, avm_main_sel_op_mul, @@ -341,21 +351,23 @@ class AvmFlavor { perm_main_mem_b, perm_main_mem_c, incl_main_tag_err, + incl_mem_tag_err, incl_main_tag_err_counts, - avm_mem_m_tag_shift, - avm_mem_m_val_shift, - avm_mem_m_rw_shift, - avm_mem_m_addr_shift, + incl_mem_tag_err_counts, avm_alu_alu_u16_r5_shift, + avm_alu_alu_u16_r6_shift, avm_alu_alu_u16_r3_shift, - avm_alu_alu_u16_r4_shift, avm_alu_alu_u16_r7_shift, - avm_alu_alu_u16_r1_shift, avm_alu_alu_u16_r0_shift, - avm_alu_alu_u16_r6_shift, avm_alu_alu_u16_r2_shift, - avm_main_pc_shift, - avm_main_internal_return_ptr_shift) + avm_alu_alu_u16_r1_shift, + avm_alu_alu_u16_r4_shift, + avm_mem_m_tag_shift, + avm_mem_m_addr_shift, + avm_mem_m_val_shift, + avm_mem_m_rw_shift, + avm_main_internal_return_ptr_shift, + avm_main_pc_shift) RefVector get_wires() { @@ -373,6 +385,7 @@ class AvmFlavor { avm_mem_m_op_a, avm_mem_m_op_b, avm_mem_m_op_c, + avm_mem_m_sel_mov, avm_mem_m_tag_err, avm_mem_m_one_min_inv, avm_alu_alu_clk, @@ -412,6 +425,7 @@ class AvmFlavor { avm_main_sel_internal_return, avm_main_sel_jump, avm_main_sel_halt, + avm_main_sel_mov, avm_main_sel_op_add, avm_main_sel_op_sub, avm_main_sel_op_mul, @@ -441,21 +455,23 @@ class AvmFlavor { perm_main_mem_b, perm_main_mem_c, incl_main_tag_err, + incl_mem_tag_err, incl_main_tag_err_counts, - avm_mem_m_tag_shift, - avm_mem_m_val_shift, - avm_mem_m_rw_shift, - avm_mem_m_addr_shift, + incl_mem_tag_err_counts, avm_alu_alu_u16_r5_shift, + avm_alu_alu_u16_r6_shift, avm_alu_alu_u16_r3_shift, - avm_alu_alu_u16_r4_shift, avm_alu_alu_u16_r7_shift, - avm_alu_alu_u16_r1_shift, avm_alu_alu_u16_r0_shift, - avm_alu_alu_u16_r6_shift, avm_alu_alu_u16_r2_shift, - avm_main_pc_shift, - avm_main_internal_return_ptr_shift }; + avm_alu_alu_u16_r1_shift, + avm_alu_alu_u16_r4_shift, + avm_mem_m_tag_shift, + avm_mem_m_addr_shift, + avm_mem_m_val_shift, + avm_mem_m_rw_shift, + avm_main_internal_return_ptr_shift, + avm_main_pc_shift }; }; RefVector get_unshifted() { @@ -473,6 +489,7 @@ class AvmFlavor { avm_mem_m_op_a, avm_mem_m_op_b, avm_mem_m_op_c, + avm_mem_m_sel_mov, avm_mem_m_tag_err, avm_mem_m_one_min_inv, avm_alu_alu_clk, @@ -512,6 +529,7 @@ class AvmFlavor { avm_main_sel_internal_return, avm_main_sel_jump, avm_main_sel_halt, + avm_main_sel_mov, avm_main_sel_op_add, avm_main_sel_op_sub, avm_main_sel_op_mul, @@ -541,27 +559,43 @@ class AvmFlavor { perm_main_mem_b, perm_main_mem_c, incl_main_tag_err, - incl_main_tag_err_counts }; + incl_mem_tag_err, + incl_main_tag_err_counts, + incl_mem_tag_err_counts }; }; RefVector get_to_be_shifted() { - return { avm_mem_m_tag, avm_mem_m_val, - avm_mem_m_rw, avm_mem_m_addr, - avm_alu_alu_u16_r5, avm_alu_alu_u16_r3, - avm_alu_alu_u16_r4, avm_alu_alu_u16_r7, - avm_alu_alu_u16_r1, avm_alu_alu_u16_r0, - avm_alu_alu_u16_r6, avm_alu_alu_u16_r2, - avm_main_pc, avm_main_internal_return_ptr }; + return { avm_alu_alu_u16_r5, + avm_alu_alu_u16_r6, + avm_alu_alu_u16_r3, + avm_alu_alu_u16_r7, + avm_alu_alu_u16_r0, + avm_alu_alu_u16_r2, + avm_alu_alu_u16_r1, + avm_alu_alu_u16_r4, + avm_mem_m_tag, + avm_mem_m_addr, + avm_mem_m_val, + avm_mem_m_rw, + avm_main_internal_return_ptr, + avm_main_pc }; }; RefVector get_shifted() { - return { avm_mem_m_tag_shift, avm_mem_m_val_shift, - avm_mem_m_rw_shift, avm_mem_m_addr_shift, - avm_alu_alu_u16_r5_shift, avm_alu_alu_u16_r3_shift, - avm_alu_alu_u16_r4_shift, avm_alu_alu_u16_r7_shift, - avm_alu_alu_u16_r1_shift, avm_alu_alu_u16_r0_shift, - avm_alu_alu_u16_r6_shift, avm_alu_alu_u16_r2_shift, - avm_main_pc_shift, avm_main_internal_return_ptr_shift }; + return { avm_alu_alu_u16_r5_shift, + avm_alu_alu_u16_r6_shift, + avm_alu_alu_u16_r3_shift, + avm_alu_alu_u16_r7_shift, + avm_alu_alu_u16_r0_shift, + avm_alu_alu_u16_r2_shift, + avm_alu_alu_u16_r1_shift, + avm_alu_alu_u16_r4_shift, + avm_mem_m_tag_shift, + avm_mem_m_addr_shift, + avm_mem_m_val_shift, + avm_mem_m_rw_shift, + avm_main_internal_return_ptr_shift, + avm_main_pc_shift }; }; }; @@ -574,13 +608,20 @@ class AvmFlavor { RefVector get_to_be_shifted() { - return { avm_mem_m_tag, avm_mem_m_val, - avm_mem_m_rw, avm_mem_m_addr, - avm_alu_alu_u16_r5, avm_alu_alu_u16_r3, - avm_alu_alu_u16_r4, avm_alu_alu_u16_r7, - avm_alu_alu_u16_r1, avm_alu_alu_u16_r0, - avm_alu_alu_u16_r6, avm_alu_alu_u16_r2, - avm_main_pc, avm_main_internal_return_ptr }; + return { avm_alu_alu_u16_r5, + avm_alu_alu_u16_r6, + avm_alu_alu_u16_r3, + avm_alu_alu_u16_r7, + avm_alu_alu_u16_r0, + avm_alu_alu_u16_r2, + avm_alu_alu_u16_r1, + avm_alu_alu_u16_r4, + avm_mem_m_tag, + avm_mem_m_addr, + avm_mem_m_val, + avm_mem_m_rw, + avm_main_internal_return_ptr, + avm_main_pc }; }; // The plookup wires that store plookup read data. @@ -671,6 +712,7 @@ class AvmFlavor { Base::avm_mem_m_op_a = "AVM_MEM_M_OP_A"; Base::avm_mem_m_op_b = "AVM_MEM_M_OP_B"; Base::avm_mem_m_op_c = "AVM_MEM_M_OP_C"; + Base::avm_mem_m_sel_mov = "AVM_MEM_M_SEL_MOV"; Base::avm_mem_m_tag_err = "AVM_MEM_M_TAG_ERR"; Base::avm_mem_m_one_min_inv = "AVM_MEM_M_ONE_MIN_INV"; Base::avm_alu_alu_clk = "AVM_ALU_ALU_CLK"; @@ -710,6 +752,7 @@ class AvmFlavor { Base::avm_main_sel_internal_return = "AVM_MAIN_SEL_INTERNAL_RETURN"; Base::avm_main_sel_jump = "AVM_MAIN_SEL_JUMP"; Base::avm_main_sel_halt = "AVM_MAIN_SEL_HALT"; + Base::avm_main_sel_mov = "AVM_MAIN_SEL_MOV"; Base::avm_main_sel_op_add = "AVM_MAIN_SEL_OP_ADD"; Base::avm_main_sel_op_sub = "AVM_MAIN_SEL_OP_SUB"; Base::avm_main_sel_op_mul = "AVM_MAIN_SEL_OP_MUL"; @@ -739,7 +782,9 @@ class AvmFlavor { Base::perm_main_mem_b = "PERM_MAIN_MEM_B"; Base::perm_main_mem_c = "PERM_MAIN_MEM_C"; Base::incl_main_tag_err = "INCL_MAIN_TAG_ERR"; + Base::incl_mem_tag_err = "INCL_MEM_TAG_ERR"; Base::incl_main_tag_err_counts = "INCL_MAIN_TAG_ERR_COUNTS"; + Base::incl_mem_tag_err_counts = "INCL_MEM_TAG_ERR_COUNTS"; }; }; @@ -771,6 +816,7 @@ class AvmFlavor { Commitment avm_mem_m_op_a; Commitment avm_mem_m_op_b; Commitment avm_mem_m_op_c; + Commitment avm_mem_m_sel_mov; Commitment avm_mem_m_tag_err; Commitment avm_mem_m_one_min_inv; Commitment avm_alu_alu_clk; @@ -810,6 +856,7 @@ class AvmFlavor { Commitment avm_main_sel_internal_return; Commitment avm_main_sel_jump; Commitment avm_main_sel_halt; + Commitment avm_main_sel_mov; Commitment avm_main_sel_op_add; Commitment avm_main_sel_op_sub; Commitment avm_main_sel_op_mul; @@ -839,7 +886,9 @@ class AvmFlavor { Commitment perm_main_mem_b; Commitment perm_main_mem_c; Commitment incl_main_tag_err; + Commitment incl_mem_tag_err; Commitment incl_main_tag_err_counts; + Commitment incl_mem_tag_err_counts; std::vector> sumcheck_univariates; std::array sumcheck_evaluations; @@ -871,6 +920,7 @@ class AvmFlavor { avm_mem_m_op_a = deserialize_from_buffer(Transcript::proof_data, num_frs_read); avm_mem_m_op_b = deserialize_from_buffer(Transcript::proof_data, num_frs_read); avm_mem_m_op_c = deserialize_from_buffer(Transcript::proof_data, num_frs_read); + avm_mem_m_sel_mov = deserialize_from_buffer(Transcript::proof_data, num_frs_read); avm_mem_m_tag_err = deserialize_from_buffer(Transcript::proof_data, num_frs_read); avm_mem_m_one_min_inv = deserialize_from_buffer(Transcript::proof_data, num_frs_read); avm_alu_alu_clk = deserialize_from_buffer(Transcript::proof_data, num_frs_read); @@ -910,6 +960,7 @@ class AvmFlavor { avm_main_sel_internal_return = deserialize_from_buffer(Transcript::proof_data, num_frs_read); avm_main_sel_jump = deserialize_from_buffer(Transcript::proof_data, num_frs_read); avm_main_sel_halt = deserialize_from_buffer(Transcript::proof_data, num_frs_read); + avm_main_sel_mov = 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_sub = deserialize_from_buffer(Transcript::proof_data, num_frs_read); avm_main_sel_op_mul = deserialize_from_buffer(Transcript::proof_data, num_frs_read); @@ -939,7 +990,9 @@ class AvmFlavor { perm_main_mem_b = deserialize_from_buffer(Transcript::proof_data, num_frs_read); perm_main_mem_c = deserialize_from_buffer(Transcript::proof_data, num_frs_read); incl_main_tag_err = deserialize_from_buffer(Transcript::proof_data, num_frs_read); + incl_mem_tag_err = deserialize_from_buffer(Transcript::proof_data, num_frs_read); incl_main_tag_err_counts = deserialize_from_buffer(Transcript::proof_data, num_frs_read); + incl_mem_tag_err_counts = deserialize_from_buffer(Transcript::proof_data, num_frs_read); for (size_t i = 0; i < log_n; ++i) { sumcheck_univariates.emplace_back( @@ -975,6 +1028,7 @@ class AvmFlavor { serialize_to_buffer(avm_mem_m_op_a, Transcript::proof_data); serialize_to_buffer(avm_mem_m_op_b, Transcript::proof_data); serialize_to_buffer(avm_mem_m_op_c, Transcript::proof_data); + serialize_to_buffer(avm_mem_m_sel_mov, Transcript::proof_data); serialize_to_buffer(avm_mem_m_tag_err, Transcript::proof_data); serialize_to_buffer(avm_mem_m_one_min_inv, Transcript::proof_data); serialize_to_buffer(avm_alu_alu_clk, Transcript::proof_data); @@ -1014,6 +1068,7 @@ class AvmFlavor { serialize_to_buffer(avm_main_sel_internal_return, Transcript::proof_data); serialize_to_buffer(avm_main_sel_jump, Transcript::proof_data); serialize_to_buffer(avm_main_sel_halt, Transcript::proof_data); + serialize_to_buffer(avm_main_sel_mov, Transcript::proof_data); serialize_to_buffer(avm_main_sel_op_add, Transcript::proof_data); serialize_to_buffer(avm_main_sel_op_sub, Transcript::proof_data); serialize_to_buffer(avm_main_sel_op_mul, Transcript::proof_data); @@ -1043,7 +1098,9 @@ class AvmFlavor { serialize_to_buffer(perm_main_mem_b, Transcript::proof_data); serialize_to_buffer(perm_main_mem_c, Transcript::proof_data); serialize_to_buffer(incl_main_tag_err, Transcript::proof_data); + serialize_to_buffer(incl_mem_tag_err, Transcript::proof_data); serialize_to_buffer(incl_main_tag_err_counts, Transcript::proof_data); + serialize_to_buffer(incl_mem_tag_err_counts, Transcript::proof_data); for (size_t i = 0; i < log_n; ++i) { serialize_to_buffer(sumcheck_univariates[i], Transcript::proof_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 7090216f452..0b9db3b8be7 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 @@ -16,6 +16,7 @@ #include "barretenberg/relations/generated/avm/avm_main.hpp" #include "barretenberg/relations/generated/avm/avm_mem.hpp" #include "barretenberg/relations/generated/avm/incl_main_tag_err.hpp" +#include "barretenberg/relations/generated/avm/incl_mem_tag_err.hpp" #include "barretenberg/relations/generated/avm/perm_main_alu.hpp" #include "barretenberg/relations/generated/avm/perm_main_mem_a.hpp" #include "barretenberg/relations/generated/avm/perm_main_mem_b.hpp" @@ -38,6 +39,7 @@ template struct AvmFullRow { FF avm_mem_m_op_a{}; FF avm_mem_m_op_b{}; FF avm_mem_m_op_c{}; + FF avm_mem_m_sel_mov{}; FF avm_mem_m_tag_err{}; FF avm_mem_m_one_min_inv{}; FF avm_alu_alu_clk{}; @@ -77,6 +79,7 @@ template struct AvmFullRow { FF avm_main_sel_internal_return{}; FF avm_main_sel_jump{}; FF avm_main_sel_halt{}; + FF avm_main_sel_mov{}; FF avm_main_sel_op_add{}; FF avm_main_sel_op_sub{}; FF avm_main_sel_op_mul{}; @@ -106,21 +109,23 @@ template struct AvmFullRow { FF perm_main_mem_b{}; FF perm_main_mem_c{}; FF incl_main_tag_err{}; + FF incl_mem_tag_err{}; FF incl_main_tag_err_counts{}; - FF avm_mem_m_tag_shift{}; - FF avm_mem_m_val_shift{}; - FF avm_mem_m_rw_shift{}; - FF avm_mem_m_addr_shift{}; + FF incl_mem_tag_err_counts{}; FF avm_alu_alu_u16_r5_shift{}; + FF avm_alu_alu_u16_r6_shift{}; FF avm_alu_alu_u16_r3_shift{}; - FF avm_alu_alu_u16_r4_shift{}; FF avm_alu_alu_u16_r7_shift{}; - FF avm_alu_alu_u16_r1_shift{}; FF avm_alu_alu_u16_r0_shift{}; - FF avm_alu_alu_u16_r6_shift{}; FF avm_alu_alu_u16_r2_shift{}; - FF avm_main_pc_shift{}; + FF avm_alu_alu_u16_r1_shift{}; + FF avm_alu_alu_u16_r4_shift{}; + FF avm_mem_m_tag_shift{}; + FF avm_mem_m_addr_shift{}; + FF avm_mem_m_val_shift{}; + FF avm_mem_m_rw_shift{}; FF avm_main_internal_return_ptr_shift{}; + FF avm_main_pc_shift{}; }; class AvmCircuitBuilder { @@ -133,8 +138,8 @@ class AvmCircuitBuilder { using Polynomial = Flavor::Polynomial; using ProverPolynomials = Flavor::ProverPolynomials; - static constexpr size_t num_fixed_columns = 97; - static constexpr size_t num_polys = 83; + static constexpr size_t num_fixed_columns = 101; + static constexpr size_t num_polys = 87; std::vector rows; void set_trace(std::vector&& trace) { rows = std::move(trace); } @@ -164,6 +169,7 @@ class AvmCircuitBuilder { polys.avm_mem_m_op_a[i] = rows[i].avm_mem_m_op_a; polys.avm_mem_m_op_b[i] = rows[i].avm_mem_m_op_b; polys.avm_mem_m_op_c[i] = rows[i].avm_mem_m_op_c; + polys.avm_mem_m_sel_mov[i] = rows[i].avm_mem_m_sel_mov; polys.avm_mem_m_tag_err[i] = rows[i].avm_mem_m_tag_err; polys.avm_mem_m_one_min_inv[i] = rows[i].avm_mem_m_one_min_inv; polys.avm_alu_alu_clk[i] = rows[i].avm_alu_alu_clk; @@ -203,6 +209,7 @@ class AvmCircuitBuilder { polys.avm_main_sel_internal_return[i] = rows[i].avm_main_sel_internal_return; polys.avm_main_sel_jump[i] = rows[i].avm_main_sel_jump; polys.avm_main_sel_halt[i] = rows[i].avm_main_sel_halt; + polys.avm_main_sel_mov[i] = rows[i].avm_main_sel_mov; polys.avm_main_sel_op_add[i] = rows[i].avm_main_sel_op_add; polys.avm_main_sel_op_sub[i] = rows[i].avm_main_sel_op_sub; polys.avm_main_sel_op_mul[i] = rows[i].avm_main_sel_op_mul; @@ -232,23 +239,25 @@ class AvmCircuitBuilder { polys.perm_main_mem_b[i] = rows[i].perm_main_mem_b; polys.perm_main_mem_c[i] = rows[i].perm_main_mem_c; polys.incl_main_tag_err[i] = rows[i].incl_main_tag_err; + polys.incl_mem_tag_err[i] = rows[i].incl_mem_tag_err; polys.incl_main_tag_err_counts[i] = rows[i].incl_main_tag_err_counts; + polys.incl_mem_tag_err_counts[i] = rows[i].incl_mem_tag_err_counts; } - polys.avm_mem_m_tag_shift = Polynomial(polys.avm_mem_m_tag.shifted()); - polys.avm_mem_m_val_shift = Polynomial(polys.avm_mem_m_val.shifted()); - polys.avm_mem_m_rw_shift = Polynomial(polys.avm_mem_m_rw.shifted()); - polys.avm_mem_m_addr_shift = Polynomial(polys.avm_mem_m_addr.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_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_r7_shift = Polynomial(polys.avm_alu_alu_u16_r7.shifted()); - polys.avm_alu_alu_u16_r1_shift = Polynomial(polys.avm_alu_alu_u16_r1.shifted()); polys.avm_alu_alu_u16_r0_shift = Polynomial(polys.avm_alu_alu_u16_r0.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_main_pc_shift = Polynomial(polys.avm_main_pc.shifted()); + polys.avm_alu_alu_u16_r1_shift = Polynomial(polys.avm_alu_alu_u16_r1.shifted()); + polys.avm_alu_alu_u16_r4_shift = Polynomial(polys.avm_alu_alu_u16_r4.shifted()); + polys.avm_mem_m_tag_shift = Polynomial(polys.avm_mem_m_tag.shifted()); + polys.avm_mem_m_addr_shift = Polynomial(polys.avm_mem_m_addr.shifted()); + polys.avm_mem_m_val_shift = Polynomial(polys.avm_mem_m_val.shifted()); + polys.avm_mem_m_rw_shift = Polynomial(polys.avm_mem_m_rw.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; } @@ -320,14 +329,14 @@ class AvmCircuitBuilder { return true; }; - if (!evaluate_relation.template operator()>("avm_mem", - Avm_vm::get_relation_label_avm_mem)) { - return false; - } if (!evaluate_relation.template operator()>("avm_alu", Avm_vm::get_relation_label_avm_alu)) { return false; } + if (!evaluate_relation.template operator()>("avm_mem", + Avm_vm::get_relation_label_avm_mem)) { + return false; + } if (!evaluate_relation.template operator()>("avm_main", Avm_vm::get_relation_label_avm_main)) { return false; @@ -348,6 +357,9 @@ class AvmCircuitBuilder { if (!evaluate_logderivative.template operator()>("INCL_MAIN_TAG_ERR")) { return false; } + if (!evaluate_logderivative.template operator()>("INCL_MEM_TAG_ERR")) { + return false; + } return true; } 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 3357e7144e5..98388dfb311 100644 --- a/barretenberg/cpp/src/barretenberg/relations/generated/avm/avm_alu.hpp +++ b/barretenberg/cpp/src/barretenberg/relations/generated/avm/avm_alu.hpp @@ -7,43 +7,43 @@ namespace bb::Avm_vm { template struct Avm_aluRow { - FF avm_alu_alu_op_eq{}; + FF avm_alu_alu_op_add{}; FF avm_alu_alu_u16_r5{}; + FF avm_alu_alu_u16_r2{}; + FF avm_alu_alu_cf{}; + FF avm_alu_alu_op_mul{}; + FF avm_alu_alu_u8_r1{}; + FF avm_alu_alu_op_not{}; FF avm_alu_alu_op_sub{}; FF avm_alu_alu_u16_r5_shift{}; - FF avm_alu_alu_u16_r4{}; + FF avm_alu_alu_u16_r6{}; FF avm_alu_alu_u16_r7{}; - FF avm_alu_alu_u8_tag{}; - FF avm_alu_alu_u16_r3_shift{}; FF avm_alu_alu_u64_r0{}; FF avm_alu_alu_ia{}; - FF avm_alu_alu_u32_tag{}; + FF avm_alu_alu_u16_r6_shift{}; FF avm_alu_alu_in_tag{}; - FF avm_alu_alu_u16_r2{}; - FF avm_alu_alu_u128_tag{}; - FF avm_alu_alu_u16_r0{}; FF avm_alu_alu_sel{}; - FF avm_alu_alu_ff_tag{}; + FF avm_alu_alu_u16_r3_shift{}; + FF avm_alu_alu_u16_r7_shift{}; FF avm_alu_alu_op_eq_diff_inv{}; - FF avm_alu_alu_ic{}; - FF avm_alu_alu_op_mul{}; - FF avm_alu_alu_cf{}; + FF avm_alu_alu_u64_tag{}; + FF avm_alu_alu_u16_r0_shift{}; + FF avm_alu_alu_u16_r2_shift{}; + FF avm_alu_alu_u32_tag{}; + FF avm_alu_alu_u16_r1_shift{}; + FF avm_alu_alu_op_eq{}; + FF avm_alu_alu_u16_r1{}; FF avm_alu_alu_u16_r4_shift{}; - FF avm_alu_alu_u16_r6{}; + FF avm_alu_alu_ff_tag{}; + FF avm_alu_alu_u16_r0{}; FF avm_alu_alu_ib{}; - FF avm_alu_alu_u16_r7_shift{}; - FF avm_alu_alu_op_add{}; - FF avm_alu_alu_u16_r1_shift{}; - FF avm_alu_alu_u8_r0{}; - FF avm_alu_alu_op_not{}; FF avm_alu_alu_u16_tag{}; - FF avm_alu_alu_u16_r1{}; - FF avm_alu_alu_u16_r0_shift{}; - FF avm_alu_alu_u16_r6_shift{}; - FF avm_alu_alu_u64_tag{}; - FF avm_alu_alu_u8_r1{}; FF avm_alu_alu_u16_r3{}; - FF avm_alu_alu_u16_r2_shift{}; + FF avm_alu_alu_u128_tag{}; + FF avm_alu_alu_u8_r0{}; + FF avm_alu_alu_ic{}; + FF avm_alu_alu_u8_tag{}; + FF avm_alu_alu_u16_r4{}; }; inline std::string get_relation_label_avm_alu(int index) @@ -52,32 +52,32 @@ inline std::string get_relation_label_avm_alu(int index) case 18: return "ALU_OP_NOT"; - case 19: - return "ALU_RES_IS_BOOL"; + case 16: + return "ALU_MULTIPLICATION_OUT_U128"; + + case 10: + return "ALU_ADD_SUB_2"; case 9: return "ALU_ADD_SUB_1"; - case 10: - return "ALU_ADD_SUB_2"; + case 11: + return "ALU_MULTIPLICATION_FF"; case 13: return "ALU_MUL_COMMON_2"; - case 20: - return "ALU_OP_EQ"; - case 17: return "ALU_FF_NOT_XOR"; - case 11: - return "ALU_MULTIPLICATION_FF"; + case 20: + return "ALU_OP_EQ"; + + case 19: + return "ALU_RES_IS_BOOL"; case 12: return "ALU_MUL_COMMON_1"; - - case 16: - return "ALU_MULTIPLICATION_OUT_U128"; } return std::to_string(index); } @@ -369,4 +369,4 @@ template class avm_aluImpl { template using avm_alu = Relation>; -} // namespace bb::Avm_vm +} // namespace bb::Avm_vm \ No newline at end of file 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 b48711ef2c7..fd48e15c47c 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,68 @@ namespace bb::Avm_vm { template struct Avm_mainRow { - FF avm_main_mem_idx_b{}; - FF avm_main_rwc{}; - FF avm_main_first{}; - FF avm_main_sel_jump{}; FF avm_main_tag_err{}; - FF avm_main_mem_op_c{}; + FF avm_main_rwb{}; FF avm_main_mem_op_b{}; + FF avm_main_ic{}; + FF avm_main_sel_internal_return{}; + FF avm_main_internal_return_ptr{}; + FF avm_main_alu_sel{}; + FF avm_main_sel_halt{}; + FF avm_main_internal_return_ptr_shift{}; + FF avm_main_mem_idx_a{}; + FF avm_main_mem_idx_b{}; + FF avm_main_rwa{}; FF avm_main_mem_op_a{}; + FF avm_main_sel_mov{}; + FF avm_main_mem_op_c{}; FF avm_main_sel_op_not{}; - FF avm_main_pc{}; - FF avm_main_sel_op_add{}; - FF avm_main_sel_internal_return{}; + FF avm_main_sel_internal_call{}; FF avm_main_pc_shift{}; - FF avm_main_ic{}; - FF avm_main_internal_return_ptr_shift{}; FF avm_main_inv{}; - FF avm_main_sel_internal_call{}; - FF avm_main_rwa{}; - FF avm_main_sel_halt{}; + FF avm_main_sel_op_add{}; + FF avm_main_rwc{}; + FF avm_main_sel_op_eq{}; + FF avm_main_ia{}; FF avm_main_sel_op_mul{}; - FF avm_main_sel_op_div{}; - FF avm_main_sel_op_sub{}; - FF avm_main_mem_idx_a{}; - FF avm_main_rwb{}; FF avm_main_op_err{}; - FF avm_main_ia{}; - FF avm_main_internal_return_ptr{}; - FF avm_main_alu_sel{}; - FF avm_main_sel_op_eq{}; + FF avm_main_first{}; FF avm_main_ib{}; + FF avm_main_sel_op_sub{}; + FF avm_main_sel_op_div{}; + FF avm_main_pc{}; + FF avm_main_sel_jump{}; }; inline std::string get_relation_label_avm_main(int index) { switch (index) { - case 34: + case 21: + return "SUBOP_DIVISION_ZERO_ERR2"; + + case 19: + return "SUBOP_DIVISION_FF"; + + case 35: return "PC_INCREMENT"; - case 23: - return "RETURN_POINTER_INCREMENT"; + case 20: + return "SUBOP_DIVISION_ZERO_ERR1"; - case 29: + case 30: return "RETURN_POINTER_DECREMENT"; - case 18: - return "SUBOP_DIVISION_FF"; + case 36: + return "INTERNAL_RETURN_POINTER_CONSISTENCY"; - case 21: + case 22: return "SUBOP_ERROR_RELEVANT_OP"; - case 35: - return "INTERNAL_RETURN_POINTER_CONSISTENCY"; + case 37: + return "MOV_SAME_VALUE"; - case 20: - return "SUBOP_DIVISION_ZERO_ERR2"; - - case 19: - return "SUBOP_DIVISION_ZERO_ERR1"; + case 24: + return "RETURN_POINTER_INCREMENT"; } return std::to_string(index); } @@ -73,8 +77,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, 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, 3, 5, + 4, 4, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 5, 3, 3, 3, }; template @@ -168,7 +173,7 @@ template class avm_mainImpl { { Avm_DECLARE_VIEWS(10); - auto tmp = (avm_main_op_err * (-avm_main_op_err + FF(1))); + auto tmp = (avm_main_sel_mov * (-avm_main_sel_mov + FF(1))); tmp *= scaling_factor; std::get<10>(evals) += tmp; } @@ -176,7 +181,7 @@ template class avm_mainImpl { { Avm_DECLARE_VIEWS(11); - auto tmp = (avm_main_tag_err * (-avm_main_tag_err + FF(1))); + auto tmp = (avm_main_op_err * (-avm_main_op_err + FF(1))); tmp *= scaling_factor; std::get<11>(evals) += tmp; } @@ -184,7 +189,7 @@ template class avm_mainImpl { { Avm_DECLARE_VIEWS(12); - auto tmp = (avm_main_mem_op_a * (-avm_main_mem_op_a + FF(1))); + auto tmp = (avm_main_tag_err * (-avm_main_tag_err + FF(1))); tmp *= scaling_factor; std::get<12>(evals) += tmp; } @@ -192,7 +197,7 @@ template class avm_mainImpl { { Avm_DECLARE_VIEWS(13); - auto tmp = (avm_main_mem_op_b * (-avm_main_mem_op_b + FF(1))); + auto tmp = (avm_main_mem_op_a * (-avm_main_mem_op_a + FF(1))); tmp *= scaling_factor; std::get<13>(evals) += tmp; } @@ -200,7 +205,7 @@ template class avm_mainImpl { { Avm_DECLARE_VIEWS(14); - auto tmp = (avm_main_mem_op_c * (-avm_main_mem_op_c + FF(1))); + auto tmp = (avm_main_mem_op_b * (-avm_main_mem_op_b + FF(1))); tmp *= scaling_factor; std::get<14>(evals) += tmp; } @@ -208,7 +213,7 @@ template class avm_mainImpl { { Avm_DECLARE_VIEWS(15); - auto tmp = (avm_main_rwa * (-avm_main_rwa + FF(1))); + auto tmp = (avm_main_mem_op_c * (-avm_main_mem_op_c + FF(1))); tmp *= scaling_factor; std::get<15>(evals) += tmp; } @@ -216,7 +221,7 @@ template class avm_mainImpl { { Avm_DECLARE_VIEWS(16); - auto tmp = (avm_main_rwb * (-avm_main_rwb + FF(1))); + auto tmp = (avm_main_rwa * (-avm_main_rwa + FF(1))); tmp *= scaling_factor; std::get<16>(evals) += tmp; } @@ -224,7 +229,7 @@ template class avm_mainImpl { { Avm_DECLARE_VIEWS(17); - auto tmp = (avm_main_rwc * (-avm_main_rwc + FF(1))); + auto tmp = (avm_main_rwb * (-avm_main_rwb + FF(1))); tmp *= scaling_factor; std::get<17>(evals) += tmp; } @@ -232,8 +237,7 @@ template class avm_mainImpl { { Avm_DECLARE_VIEWS(18); - 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_rwc * (-avm_main_rwc + FF(1))); tmp *= scaling_factor; std::get<18>(evals) += tmp; } @@ -241,7 +245,8 @@ template class avm_mainImpl { { Avm_DECLARE_VIEWS(19); - auto tmp = (avm_main_sel_op_div * (((avm_main_ib * avm_main_inv) - FF(1)) + avm_main_op_err)); + 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<19>(evals) += tmp; } @@ -249,7 +254,7 @@ template class avm_mainImpl { { Avm_DECLARE_VIEWS(20); - auto tmp = ((avm_main_sel_op_div * avm_main_op_err) * (-avm_main_inv + 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<20>(evals) += tmp; } @@ -257,7 +262,7 @@ template class avm_mainImpl { { Avm_DECLARE_VIEWS(21); - auto tmp = (avm_main_op_err * (avm_main_sel_op_div - FF(1))); + auto tmp = ((avm_main_sel_op_div * avm_main_op_err) * (-avm_main_inv + FF(1))); tmp *= scaling_factor; std::get<21>(evals) += tmp; } @@ -265,7 +270,7 @@ template class avm_mainImpl { { Avm_DECLARE_VIEWS(22); - auto tmp = (avm_main_sel_jump * (avm_main_pc_shift - avm_main_ia)); + auto tmp = (avm_main_op_err * (avm_main_sel_op_div - FF(1))); tmp *= scaling_factor; std::get<22>(evals) += tmp; } @@ -273,8 +278,7 @@ template class avm_mainImpl { { Avm_DECLARE_VIEWS(23); - 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_jump * (avm_main_pc_shift - avm_main_ia)); tmp *= scaling_factor; std::get<23>(evals) += tmp; } @@ -282,7 +286,8 @@ template class avm_mainImpl { { Avm_DECLARE_VIEWS(24); - 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_internal_return_ptr_shift - (avm_main_internal_return_ptr + FF(1)))); tmp *= scaling_factor; std::get<24>(evals) += tmp; } @@ -290,7 +295,7 @@ template class avm_mainImpl { { Avm_DECLARE_VIEWS(25); - auto tmp = (avm_main_sel_internal_call * (avm_main_pc_shift - avm_main_ia)); + auto tmp = (avm_main_sel_internal_call * (avm_main_internal_return_ptr - avm_main_mem_idx_b)); tmp *= scaling_factor; std::get<25>(evals) += tmp; } @@ -298,7 +303,7 @@ template class avm_mainImpl { { Avm_DECLARE_VIEWS(26); - auto tmp = (avm_main_sel_internal_call * ((avm_main_pc + FF(1)) - avm_main_ib)); + auto tmp = (avm_main_sel_internal_call * (avm_main_pc_shift - avm_main_ia)); tmp *= scaling_factor; std::get<26>(evals) += tmp; } @@ -306,7 +311,7 @@ template class avm_mainImpl { { Avm_DECLARE_VIEWS(27); - auto tmp = (avm_main_sel_internal_call * (avm_main_rwb - FF(1))); + auto tmp = (avm_main_sel_internal_call * ((avm_main_pc + FF(1)) - avm_main_ib)); tmp *= scaling_factor; std::get<27>(evals) += tmp; } @@ -314,7 +319,7 @@ template class avm_mainImpl { { Avm_DECLARE_VIEWS(28); - auto tmp = (avm_main_sel_internal_call * (avm_main_mem_op_b - FF(1))); + auto tmp = (avm_main_sel_internal_call * (avm_main_rwb - FF(1))); tmp *= scaling_factor; std::get<28>(evals) += tmp; } @@ -322,8 +327,7 @@ template class avm_mainImpl { { Avm_DECLARE_VIEWS(29); - 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_call * (avm_main_mem_op_b - FF(1))); tmp *= scaling_factor; std::get<29>(evals) += tmp; } @@ -331,7 +335,8 @@ template class avm_mainImpl { { Avm_DECLARE_VIEWS(30); - 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_internal_return_ptr_shift - (avm_main_internal_return_ptr - FF(1)))); tmp *= scaling_factor; std::get<30>(evals) += tmp; } @@ -339,7 +344,7 @@ template class avm_mainImpl { { Avm_DECLARE_VIEWS(31); - auto tmp = (avm_main_sel_internal_return * (avm_main_pc_shift - avm_main_ia)); + auto tmp = (avm_main_sel_internal_return * ((avm_main_internal_return_ptr - FF(1)) - avm_main_mem_idx_a)); tmp *= scaling_factor; std::get<31>(evals) += tmp; } @@ -347,7 +352,7 @@ template class avm_mainImpl { { Avm_DECLARE_VIEWS(32); - auto tmp = (avm_main_sel_internal_return * avm_main_rwa); + auto tmp = (avm_main_sel_internal_return * (avm_main_pc_shift - avm_main_ia)); tmp *= scaling_factor; std::get<32>(evals) += tmp; } @@ -355,7 +360,7 @@ template class avm_mainImpl { { Avm_DECLARE_VIEWS(33); - auto tmp = (avm_main_sel_internal_return * (avm_main_mem_op_a - FF(1))); + auto tmp = (avm_main_sel_internal_return * avm_main_rwa); tmp *= scaling_factor; std::get<33>(evals) += tmp; } @@ -363,35 +368,51 @@ template class avm_mainImpl { { Avm_DECLARE_VIEWS(34); + auto tmp = (avm_main_sel_internal_return * (avm_main_mem_op_a - FF(1))); + tmp *= scaling_factor; + std::get<34>(evals) += tmp; + } + // Contribution 35 + { + Avm_DECLARE_VIEWS(35); + 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<34>(evals) += tmp; + std::get<35>(evals) += tmp; } - // Contribution 35 + // Contribution 36 { - Avm_DECLARE_VIEWS(35); + Avm_DECLARE_VIEWS(36); 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<35>(evals) += tmp; + std::get<36>(evals) += tmp; } - // Contribution 36 + // Contribution 37 { - Avm_DECLARE_VIEWS(36); + Avm_DECLARE_VIEWS(37); + + auto tmp = (avm_main_sel_mov * (avm_main_ia - avm_main_ic)); + tmp *= scaling_factor; + std::get<37>(evals) += tmp; + } + // Contribution 38 + { + Avm_DECLARE_VIEWS(38); 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<36>(evals) += tmp; + std::get<38>(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 dafa996d6fa..caacb2ec45d 100644 --- a/barretenberg/cpp/src/barretenberg/relations/generated/avm/avm_mem.hpp +++ b/barretenberg/cpp/src/barretenberg/relations/generated/avm/avm_mem.hpp @@ -7,31 +7,29 @@ namespace bb::Avm_vm { template struct Avm_memRow { - FF avm_mem_m_tag_shift{}; - FF avm_mem_m_val_shift{}; FF avm_mem_m_op_a{}; + FF avm_mem_m_tag_err{}; + FF avm_mem_m_last{}; FF avm_mem_m_addr{}; - FF avm_mem_m_lastAccess{}; - FF avm_mem_m_tag{}; - FF avm_mem_m_rw_shift{}; + FF avm_mem_m_val{}; FF avm_mem_m_in_tag{}; - FF avm_mem_m_last{}; - FF avm_mem_m_tag_err{}; + FF avm_mem_m_tag_shift{}; + FF avm_mem_m_sub_clk{}; FF avm_mem_m_addr_shift{}; - FF avm_mem_m_val{}; - FF avm_mem_m_one_min_inv{}; + FF avm_mem_m_sel_mov{}; + FF avm_mem_m_rw{}; FF avm_mem_m_op_b{}; - FF avm_mem_m_sub_clk{}; + FF avm_mem_m_val_shift{}; + FF avm_mem_m_tag{}; FF avm_mem_m_op_c{}; - FF avm_mem_m_rw{}; + FF avm_mem_m_rw_shift{}; + FF avm_mem_m_one_min_inv{}; + FF avm_mem_m_lastAccess{}; }; inline std::string get_relation_label_avm_mem(int index) { switch (index) { - case 13: - return "MEM_IN_TAG_CONSISTENCY_1"; - case 10: return "MEM_READ_WRITE_VAL_CONSISTENCY"; @@ -41,11 +39,17 @@ inline std::string get_relation_label_avm_mem(int index) case 9: return "MEM_LAST_ACCESS_DELIMITER"; + case 13: + return "MEM_IN_TAG_CONSISTENCY_1"; + case 12: return "MEM_ZERO_INIT"; case 14: return "MEM_IN_TAG_CONSISTENCY_2"; + + case 15: + return "MOV_SAME_TAG"; } return std::to_string(index); } @@ -54,8 +58,8 @@ template class avm_memImpl { public: using FF = FF_; - static constexpr std::array SUBRELATION_PARTIAL_LENGTHS{ - 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 4, 4, 4, 3, 3, + static constexpr std::array SUBRELATION_PARTIAL_LENGTHS{ + 3, 3, 3, 3, 3, 3, 3, 3, 3, 3, 4, 4, 4, 3, 3, 3, }; template @@ -188,6 +192,14 @@ template class avm_memImpl { tmp *= scaling_factor; std::get<14>(evals) += tmp; } + // Contribution 15 + { + Avm_DECLARE_VIEWS(15); + + auto tmp = (avm_mem_m_sel_mov * avm_mem_m_tag_err); + tmp *= scaling_factor; + std::get<15>(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 3cfe1455ce2..9d9ee4459e5 100644 --- a/barretenberg/cpp/src/barretenberg/relations/generated/avm/declare_views.hpp +++ b/barretenberg/cpp/src/barretenberg/relations/generated/avm/declare_views.hpp @@ -16,6 +16,7 @@ [[maybe_unused]] auto avm_mem_m_op_a = View(new_term.avm_mem_m_op_a); \ [[maybe_unused]] auto avm_mem_m_op_b = View(new_term.avm_mem_m_op_b); \ [[maybe_unused]] auto avm_mem_m_op_c = View(new_term.avm_mem_m_op_c); \ + [[maybe_unused]] auto avm_mem_m_sel_mov = View(new_term.avm_mem_m_sel_mov); \ [[maybe_unused]] auto avm_mem_m_tag_err = View(new_term.avm_mem_m_tag_err); \ [[maybe_unused]] auto avm_mem_m_one_min_inv = View(new_term.avm_mem_m_one_min_inv); \ [[maybe_unused]] auto avm_alu_alu_clk = View(new_term.avm_alu_alu_clk); \ @@ -55,6 +56,7 @@ [[maybe_unused]] auto avm_main_sel_internal_return = View(new_term.avm_main_sel_internal_return); \ [[maybe_unused]] auto avm_main_sel_jump = View(new_term.avm_main_sel_jump); \ [[maybe_unused]] auto avm_main_sel_halt = View(new_term.avm_main_sel_halt); \ + [[maybe_unused]] auto avm_main_sel_mov = View(new_term.avm_main_sel_mov); \ [[maybe_unused]] auto avm_main_sel_op_add = View(new_term.avm_main_sel_op_add); \ [[maybe_unused]] auto avm_main_sel_op_sub = View(new_term.avm_main_sel_op_sub); \ [[maybe_unused]] auto avm_main_sel_op_mul = View(new_term.avm_main_sel_op_mul); \ @@ -84,18 +86,20 @@ [[maybe_unused]] auto perm_main_mem_b = View(new_term.perm_main_mem_b); \ [[maybe_unused]] auto perm_main_mem_c = View(new_term.perm_main_mem_c); \ [[maybe_unused]] auto incl_main_tag_err = View(new_term.incl_main_tag_err); \ + [[maybe_unused]] auto incl_mem_tag_err = View(new_term.incl_mem_tag_err); \ [[maybe_unused]] auto incl_main_tag_err_counts = View(new_term.incl_main_tag_err_counts); \ - [[maybe_unused]] auto avm_mem_m_tag_shift = View(new_term.avm_mem_m_tag_shift); \ - [[maybe_unused]] auto avm_mem_m_val_shift = View(new_term.avm_mem_m_val_shift); \ - [[maybe_unused]] auto avm_mem_m_rw_shift = View(new_term.avm_mem_m_rw_shift); \ - [[maybe_unused]] auto avm_mem_m_addr_shift = View(new_term.avm_mem_m_addr_shift); \ + [[maybe_unused]] auto incl_mem_tag_err_counts = View(new_term.incl_mem_tag_err_counts); \ [[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_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_r7_shift = View(new_term.avm_alu_alu_u16_r7_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_r0_shift = View(new_term.avm_alu_alu_u16_r0_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_main_pc_shift = View(new_term.avm_main_pc_shift); \ - [[maybe_unused]] auto avm_main_internal_return_ptr_shift = View(new_term.avm_main_internal_return_ptr_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_r4_shift = View(new_term.avm_alu_alu_u16_r4_shift); \ + [[maybe_unused]] auto avm_mem_m_tag_shift = View(new_term.avm_mem_m_tag_shift); \ + [[maybe_unused]] auto avm_mem_m_addr_shift = View(new_term.avm_mem_m_addr_shift); \ + [[maybe_unused]] auto avm_mem_m_val_shift = View(new_term.avm_mem_m_val_shift); \ + [[maybe_unused]] auto avm_mem_m_rw_shift = View(new_term.avm_mem_m_rw_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); diff --git a/barretenberg/cpp/src/barretenberg/relations/generated/avm/incl_mem_tag_err.hpp b/barretenberg/cpp/src/barretenberg/relations/generated/avm/incl_mem_tag_err.hpp new file mode 100644 index 00000000000..8c7535bc1c4 --- /dev/null +++ b/barretenberg/cpp/src/barretenberg/relations/generated/avm/incl_mem_tag_err.hpp @@ -0,0 +1,166 @@ + + +#pragma once + +#include "barretenberg/relations/generic_lookup/generic_lookup_relation.hpp" + +#include +#include + +namespace bb { + +/** + * @brief This class contains an example of how to set LookupSettings classes used by the + * GenericLookupRelationImpl class to specify a scaled lookup + * + * @details To create your own lookup: + * 1) Create a copy of this class and rename it + * 2) Update all the values with the ones needed for your lookup + * 3) Update "DECLARE_LOOKUP_IMPLEMENTATIONS_FOR_ALL_SETTINGS" and "DEFINE_LOOKUP_IMPLEMENTATIONS_FOR_ALL_SETTINGS" to + * include the new settings + * 4) Add the relation with the chosen settings to Relations in the flavor (for example,"` + * using Relations = std::tuple>;)` + * + */ +class incl_mem_tag_err_lookup_settings { + public: + /** + * @brief The number of read terms (how many lookups we perform) in each row + * + */ + static constexpr size_t READ_TERMS = 1; + /** + * @brief The number of write terms (how many additions to the lookup table we make) in each row + * + */ + static constexpr size_t WRITE_TERMS = 1; + + /** + * @brief The type of READ_TERM used for each read index (basic and scaled) + * + */ + static constexpr size_t READ_TERM_TYPES[READ_TERMS] = { 0 }; + + /** + * @brief They type of WRITE_TERM used for each write index + * + */ + static constexpr size_t WRITE_TERM_TYPES[WRITE_TERMS] = { 0 }; + + /** + * @brief How many values represent a single lookup object. This value is used by the automatic read term + * implementation in the relation in case the lookup is a basic or scaled tuple and in the write term if it's a + * basic tuple + * + */ + static constexpr size_t LOOKUP_TUPLE_SIZE = 1; + + /** + * @brief The polynomial degree of the relation telling us if the inverse polynomial value needs to be computed + * + */ + static constexpr size_t INVERSE_EXISTS_POLYNOMIAL_DEGREE = 2; + + /** + * @brief The degree of the read term if implemented arbitrarily. This value is not used by basic and scaled read + * terms, but will cause compilation error if not defined + * + */ + static constexpr size_t READ_TERM_DEGREE = 0; + + /** + * @brief The degree of the write term if implemented arbitrarily. This value is not used by the basic write + * term, but will cause compilation error if not defined + * + */ + + static constexpr size_t WRITE_TERM_DEGREE = 0; + + /** + * @brief If this method returns true on a row of values, then the inverse polynomial exists at this index. + * Otherwise the value needs to be set to zero. + * + * @details If this is true then the lookup takes place in this row + * + */ + + template static inline auto inverse_polynomial_is_computed_at_row(const AllEntities& in) + { + return (in.avm_main_tag_err == 1 || in.avm_mem_m_tag_err == 1); + } + + /** + * @brief Subprocedure for computing the value deciding if the inverse polynomial value needs to be checked in this + * row + * + * @tparam Accumulator Type specified by the lookup relation + * @tparam AllEntities Values/Univariates of all entities row + * @param in Value/Univariate of all entities at row/edge + * @return Accumulator + */ + + template + static inline auto compute_inverse_exists(const AllEntities& in) + { + using View = typename Accumulator::View; + const auto is_operation = View(in.avm_main_tag_err); + const auto is_table_entry = View(in.avm_mem_m_tag_err); + return (is_operation + is_table_entry - is_operation * is_table_entry); + } + + /** + * @brief Get all the entities for the lookup when need to update them + * + * @details The generic structure of this tuple is described in ./generic_lookup_relation.hpp . The following is + description for the current case: + The entities are returned as a tuple of references in the following order (this is for ): + * - The entity/polynomial used to store the product of the inverse values + * - The entity/polynomial that specifies how many times the lookup table entry at this row has been looked up + * - READ_TERMS entities/polynomials that enable individual lookup operations + * - The entity/polynomial that enables adding an entry to the lookup table in this row + * - LOOKUP_TUPLE_SIZE entities/polynomials representing the basic tuple being looked up as the first read term + * - LOOKUP_TUPLE_SIZE entities/polynomials representing the previous accumulators in the second read term + (scaled tuple) + * - LOOKUP_TUPLE_SIZE entities/polynomials representing the shifts in the second read term (scaled tuple) + * - LOOKUP_TUPLE_SIZE entities/polynomials representing the current accumulators in the second read term + (scaled tuple) + * - LOOKUP_TUPLE_SIZE entities/polynomials representing basic tuples added to the table + * + * @return All the entities needed for the lookup + */ + + template static inline auto get_const_entities(const AllEntities& in) + { + + return std::forward_as_tuple(in.incl_mem_tag_err, + in.incl_mem_tag_err_counts, + in.avm_main_tag_err, + in.avm_mem_m_tag_err, + in.avm_main_clk, + in.avm_mem_m_clk); + } + + /** + * @brief Get all the entities for the lookup when we only need to read them + * @details Same as in get_const_entities, but nonconst + * + * @return All the entities needed for the lookup + */ + + template static inline auto get_nonconst_entities(AllEntities& in) + { + + return std::forward_as_tuple(in.incl_mem_tag_err, + in.incl_mem_tag_err_counts, + in.avm_main_tag_err, + in.avm_mem_m_tag_err, + in.avm_main_clk, + in.avm_mem_m_clk); + } +}; + +template using incl_mem_tag_err_relation = GenericLookupRelation; +template using incl_mem_tag_err = GenericLookup; + +} // namespace bb diff --git a/barretenberg/cpp/src/barretenberg/relations/generated/avm/perm_main_mem_a.hpp b/barretenberg/cpp/src/barretenberg/relations/generated/avm/perm_main_mem_a.hpp index 5d52373810e..d7115275c10 100644 --- a/barretenberg/cpp/src/barretenberg/relations/generated/avm/perm_main_mem_a.hpp +++ b/barretenberg/cpp/src/barretenberg/relations/generated/avm/perm_main_mem_a.hpp @@ -12,7 +12,7 @@ namespace bb { class perm_main_mem_a_permutation_settings { public: // This constant defines how many columns are bundled together to form each set. - constexpr static size_t COLUMNS_PER_SET = 5; + constexpr static size_t COLUMNS_PER_SET = 6; /** * @brief If this method returns true on a row of values, then the inverse polynomial at this index. Otherwise the @@ -55,11 +55,13 @@ class perm_main_mem_a_permutation_settings { in.avm_main_ia, in.avm_main_rwa, in.avm_main_in_tag, + in.avm_main_sel_mov, in.avm_mem_m_clk, in.avm_mem_m_addr, in.avm_mem_m_val, in.avm_mem_m_rw, - in.avm_mem_m_in_tag); + in.avm_mem_m_in_tag, + in.avm_mem_m_sel_mov); } /** @@ -91,11 +93,13 @@ class perm_main_mem_a_permutation_settings { in.avm_main_ia, in.avm_main_rwa, in.avm_main_in_tag, + in.avm_main_sel_mov, in.avm_mem_m_clk, in.avm_mem_m_addr, in.avm_mem_m_val, in.avm_mem_m_rw, - in.avm_mem_m_in_tag); + in.avm_mem_m_in_tag, + in.avm_mem_m_sel_mov); } }; 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 00efac80474..657ae07ebfb 100644 --- a/barretenberg/cpp/src/barretenberg/vm/avm_trace/avm_deserialization.cpp +++ b/barretenberg/cpp/src/barretenberg/vm/avm_trace/avm_deserialization.cpp @@ -38,6 +38,7 @@ const std::unordered_map> OPCODE_WIRE_FORMAT = { OpCode::INTERNALRETURN, {} }, // Machine State - Memory // OpCode::SET is handled differently + { OpCode::MOV, { OperandType::INDIRECT, OperandType::UINT32, OperandType::UINT32 } }, // Control Flow - Contract Calls { OpCode::RETURN, { OperandType::INDIRECT, OperandType::UINT32, OperandType::UINT32 } }, }; 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 a16c7a6dc15..96ac76fc5e5 100644 --- a/barretenberg/cpp/src/barretenberg/vm/avm_trace/avm_execution.cpp +++ b/barretenberg/cpp/src/barretenberg/vm/avm_trace/avm_execution.cpp @@ -178,6 +178,9 @@ std::vector Execution::gen_trace(std::vector const& instructio trace_builder.set(val, dst_offset, in_tag); break; } + case OpCode::MOV: + trace_builder.op_mov(std::get(inst.operands.at(1)), std::get(inst.operands.at(2))); + break; // Control Flow - Contract Calls case OpCode::RETURN: // Skip indirect at index 0 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 d680159aef1..22de65efaef 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 @@ -86,7 +86,14 @@ void AvmMemTraceBuilder::load_mismatch_tag_in_mem_trace(uint32_t const m_clk, { FF one_min_inv = FF(1) - (FF(static_cast(m_in_tag)) - FF(static_cast(m_tag))).invert(); - // Lookup counter hint, used for #[equiv_tag_err] lookup (joined on clk) + // Relevant for inclusion (lookup) check #[INCL_MEM_TAG_ERR]. We need to + // flag the first memory entry per clk key. The number of memory entries + // with m_tag_err enabled can be higher than one for a given clk value. + // The repetition of the same clk in the lookup table side (right hand + // side, here, memory table) should be accounted for ONLY ONCE. + bool tag_err_count_relevant = !m_tag_err_lookup_counts.contains(m_clk); + + // Lookup counter hint, used for #[INCL_MAIN_TAG_ERR] lookup (joined on clk) m_tag_err_lookup_counts[m_clk]++; mem_trace.emplace_back(MemoryTraceEntry{ .m_clk = m_clk, @@ -96,7 +103,8 @@ void AvmMemTraceBuilder::load_mismatch_tag_in_mem_trace(uint32_t const m_clk, .m_tag = m_tag, .m_in_tag = m_in_tag, .m_tag_err = true, - .m_one_min_inv = one_min_inv }); + .m_one_min_inv = one_min_inv, + .m_tag_err_count_relevant = tag_err_count_relevant }); } /** @@ -168,6 +176,37 @@ void AvmMemTraceBuilder::store_in_mem_trace( insert_in_mem_trace(clk, sub_clk, addr, val, m_in_tag, true); } +/** + * @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. In addition, the specific selector + * for MOV opcode is enabled. + * + * @param clk Main clock + * @param addr Memory address of the source offset + * + * @return Result of the read operation containing the value and the tag of the memory cell + * at the supplied address. + */ +std::pair AvmMemTraceBuilder::read_and_load_mov_opcode(uint32_t const clk, uint32_t const addr) +{ + FF const& val = memory.at(addr); + AvmMemoryTag m_tag = memory_tag.at(addr); + + mem_trace.emplace_back(MemoryTraceEntry{ + .m_clk = clk, + .m_sub_clk = SUB_CLK_LOAD_A, + .m_addr = addr, + .m_val = val, + .m_tag = m_tag, + .m_in_tag = m_tag, + .m_sel_mov = true, + }); + + return std::make_pair(val, m_tag); +} + /** * @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 f6bd30c0937..e7246f14d03 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 @@ -1,6 +1,7 @@ #pragma once #include "avm_common.hpp" +#include namespace bb::avm_trace { @@ -29,6 +30,8 @@ class AvmMemTraceBuilder { bool m_rw = false; bool m_tag_err = false; FF m_one_min_inv{}; + bool m_sel_mov = false; + bool m_tag_err_count_relevant = false; /** * @brief A comparator on MemoryTraceEntry to be used by sorting algorithm. We sort first by @@ -70,6 +73,7 @@ class AvmMemTraceBuilder { std::vector finalize(); + std::pair read_and_load_mov_opcode(uint32_t clk, uint32_t addr); MemRead read_and_load_from_memory(uint32_t clk, IntermRegister interm_reg, uint32_t addr, AvmMemoryTag m_in_tag); void write_into_memory( uint32_t clk, IntermRegister interm_reg, uint32_t addr, FF const& val, AvmMemoryTag m_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 d4ec8c3ace1..c02f8b8f3c6 100644 --- a/barretenberg/cpp/src/barretenberg/vm/avm_trace/avm_trace.cpp +++ b/barretenberg/cpp/src/barretenberg/vm/avm_trace/avm_trace.cpp @@ -361,6 +361,39 @@ void AvmTraceBuilder::set(uint128_t val, uint32_t dst_offset, AvmMemoryTag in_ta }); } +/** + * @brief Copy value and tag from a memory cell at position src_offset to the + * memory cell at position dst_offset + * + * @param src_offset Offset of source memory cell + * @param dst_offset Offset of destination memory cell + */ +void AvmTraceBuilder::op_mov(uint32_t const src_offset, uint32_t const dst_offset) +{ + auto const clk = static_cast(main_trace.size()); + + // Reading from memory and loading into ia without tag check. + auto const [val, tag] = mem_trace_builder.read_and_load_mov_opcode(clk, src_offset); + + // Write into memory value c from intermediate register ic. + mem_trace_builder.write_into_memory(clk, IntermRegister::IC, dst_offset, val, tag); + + main_trace.push_back(Row{ + .avm_main_clk = clk, + .avm_main_pc = FF(pc++), + .avm_main_internal_return_ptr = FF(internal_return_ptr), + .avm_main_sel_mov = FF(1), + .avm_main_in_tag = FF(static_cast(tag)), + .avm_main_ia = val, + .avm_main_ic = val, + .avm_main_mem_op_a = FF(1), + .avm_main_mem_op_c = FF(1), + .avm_main_rwc = FF(1), + .avm_main_mem_idx_a = FF(src_offset), + .avm_main_mem_idx_c = FF(dst_offset), + }); +} + /** * @brief CALLDATACOPY opcode with direct memory access, i.e., * M[dst_offset:dst_offset+copy_size] = calldata[cd_offset:cd_offset+copy_size] @@ -695,9 +728,9 @@ void AvmTraceBuilder::internal_return() // counts column here // // NOTE: its coupled to pil - this is not the final iteration -void AvmTraceBuilder::finalise_mem_trace_lookup_counts(std::map const& tag_err_lookup_counts) +void AvmTraceBuilder::finalise_mem_trace_lookup_counts() { - for (auto const& [clk, count] : tag_err_lookup_counts) { + for (auto const& [clk, count] : mem_trace_builder.m_tag_err_lookup_counts) { main_trace.at(clk).incl_main_tag_err_counts = count; } } @@ -719,7 +752,7 @@ std::vector AvmTraceBuilder::finalize() size_t alu_trace_size = alu_trace.size(); // Get tag_err counts from the mem_trace_builder - this->finalise_mem_trace_lookup_counts(mem_trace_builder.m_tag_err_lookup_counts); + finalise_mem_trace_lookup_counts(); // TODO: We will have to handle this through error handling and not an assertion // Smaller than N because we have to add an extra initial row to support shifted @@ -750,6 +783,9 @@ std::vector AvmTraceBuilder::finalize() dest.avm_mem_m_tag = FF(static_cast(src.m_tag)); dest.avm_mem_m_tag_err = FF(static_cast(src.m_tag_err)); dest.avm_mem_m_one_min_inv = src.m_one_min_inv; + dest.avm_mem_m_sel_mov = FF(static_cast(src.m_sel_mov)); + + dest.incl_mem_tag_err_counts = FF(static_cast(src.m_tag_err_count_relevant)); if (src.m_sub_clk == AvmMemTraceBuilder::SUB_CLK_LOAD_A || src.m_sub_clk == AvmMemTraceBuilder::SUB_CLK_STORE_A) { 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 19971def2e4..8731f4515fd 100644 --- a/barretenberg/cpp/src/barretenberg/vm/avm_trace/avm_trace.hpp +++ b/barretenberg/cpp/src/barretenberg/vm/avm_trace/avm_trace.hpp @@ -49,6 +49,9 @@ class AvmTraceBuilder { // Set a constant from bytecode with direct memory access. void set(uint128_t val, uint32_t dst_offset, AvmMemoryTag in_tag); + // Move (copy) the value and tag of a memory cell to another one. + void op_mov(uint32_t src_offset, uint32_t dst_offset); + // Jump to a given program counter. void jump(uint32_t jmp_dest); @@ -78,7 +81,7 @@ class AvmTraceBuilder { AvmMemTraceBuilder mem_trace_builder; AvmAluTraceBuilder alu_trace_builder; - void finalise_mem_trace_lookup_counts(std::map const& tag_err_lookup_counts); + void finalise_mem_trace_lookup_counts(); uint32_t pc = 0; uint32_t internal_return_ptr = CALLSTACK_OFFSET; diff --git a/barretenberg/cpp/src/barretenberg/vm/generated/avm_verifier.cpp b/barretenberg/cpp/src/barretenberg/vm/generated/avm_verifier.cpp index 0ee66fee2ad..c457ce090a2 100644 --- a/barretenberg/cpp/src/barretenberg/vm/generated/avm_verifier.cpp +++ b/barretenberg/cpp/src/barretenberg/vm/generated/avm_verifier.cpp @@ -66,6 +66,8 @@ bool AvmVerifier::verify_proof(const HonkProof& proof) commitments.avm_mem_m_op_a = transcript->template receive_from_prover(commitment_labels.avm_mem_m_op_a); commitments.avm_mem_m_op_b = transcript->template receive_from_prover(commitment_labels.avm_mem_m_op_b); commitments.avm_mem_m_op_c = transcript->template receive_from_prover(commitment_labels.avm_mem_m_op_c); + commitments.avm_mem_m_sel_mov = + transcript->template receive_from_prover(commitment_labels.avm_mem_m_sel_mov); commitments.avm_mem_m_tag_err = transcript->template receive_from_prover(commitment_labels.avm_mem_m_tag_err); commitments.avm_mem_m_one_min_inv = @@ -139,6 +141,8 @@ bool AvmVerifier::verify_proof(const HonkProof& proof) transcript->template receive_from_prover(commitment_labels.avm_main_sel_jump); commitments.avm_main_sel_halt = transcript->template receive_from_prover(commitment_labels.avm_main_sel_halt); + commitments.avm_main_sel_mov = + transcript->template receive_from_prover(commitment_labels.avm_main_sel_mov); commitments.avm_main_sel_op_add = transcript->template receive_from_prover(commitment_labels.avm_main_sel_op_add); commitments.avm_main_sel_op_sub = @@ -188,8 +192,12 @@ bool AvmVerifier::verify_proof(const HonkProof& proof) transcript->template receive_from_prover(commitment_labels.perm_main_mem_c); commitments.incl_main_tag_err = transcript->template receive_from_prover(commitment_labels.incl_main_tag_err); + commitments.incl_mem_tag_err = + transcript->template receive_from_prover(commitment_labels.incl_mem_tag_err); commitments.incl_main_tag_err_counts = transcript->template receive_from_prover(commitment_labels.incl_main_tag_err_counts); + commitments.incl_mem_tag_err_counts = + transcript->template receive_from_prover(commitment_labels.incl_mem_tag_err_counts); // Execute Sumcheck Verifier const size_t log_circuit_size = numeric::get_msb(circuit_size); 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 e00cbd27a4f..b018610c5ef 100644 --- a/barretenberg/cpp/src/barretenberg/vm/tests/avm_execution.test.cpp +++ b/barretenberg/cpp/src/barretenberg/vm/tests/avm_execution.test.cpp @@ -455,6 +455,54 @@ TEST_F(AvmExecutionTests, jumpAndCalldatacopy) gen_proof_and_validate(bytecode, std::move(trace), std::vector{ 13, 156 }); } +// Positive test with MOV. +TEST_F(AvmExecutionTests, movOpcode) +{ + std::string bytecode_hex = to_hex(OpCode::SET) + // opcode SET + "00" // Indirect flag + "01" // U8 + "13" // val 19 + "000000AB" // dst_offset 171 + + to_hex(OpCode::MOV) + // opcode MOV + "00" // Indirect flag + "000000AB" // src_offset 171 + "00000021" // dst_offset 33 + + 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)); + + // SET + EXPECT_THAT(instructions.at(0), + AllOf(Field(&Instruction::op_code, OpCode::SET), + Field(&Instruction::operands, + ElementsAre(VariantWith(0), + VariantWith(AvmMemoryTag::U8), + VariantWith(19), + VariantWith(171))))); + + // MOV + EXPECT_THAT( + instructions.at(1), + AllOf(Field(&Instruction::op_code, OpCode::MOV), + Field(&Instruction::operands, + ElementsAre(VariantWith(0), VariantWith(171), VariantWith(33))))); + + auto trace = Execution::gen_trace(instructions); + + // Find the first row enabling the MOV selector + auto row = std::ranges::find_if(trace.begin(), trace.end(), [](Row r) { return r.avm_main_sel_mov == 1; }); + EXPECT_EQ(row->avm_main_ia, 19); + EXPECT_EQ(row->avm_main_ic, 19); + + gen_proof_and_validate(bytecode, std::move(trace), {}); +} + // Negative test detecting an invalid opcode byte. TEST_F(AvmExecutionTests, invalidOpcode) { diff --git a/barretenberg/cpp/src/barretenberg/vm/tests/avm_mem_opcodes.test.cpp b/barretenberg/cpp/src/barretenberg/vm/tests/avm_mem_opcodes.test.cpp new file mode 100644 index 00000000000..04b43ea9a5a --- /dev/null +++ b/barretenberg/cpp/src/barretenberg/vm/tests/avm_mem_opcodes.test.cpp @@ -0,0 +1,185 @@ +#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; + +class AvmMemOpcodeTests : public ::testing::Test { + public: + AvmTraceBuilder trace_builder; + + protected: + std::vector trace; + size_t main_idx; + size_t mem_a_idx; + size_t mem_c_idx; + + // 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 buildTrace(uint128_t const val, uint32_t const src_offset, uint32_t const dst_offset, AvmMemoryTag const tag) + { + trace_builder.set(val, src_offset, tag); + trace_builder.op_mov(src_offset, dst_offset); + trace_builder.return_op(0, 0); + trace = trace_builder.finalize(); + + // Find the first row enabling the MOV selector + auto row = std::ranges::find_if(trace.begin(), trace.end(), [](Row r) { return r.avm_main_sel_mov == FF(1); }); + ASSERT_TRUE(row != trace.end()); + main_idx = static_cast(row - trace.begin()); + + 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; + }); + ASSERT_TRUE(row != trace.end()); + mem_a_idx = static_cast(row - trace.begin()); + + // Find the memory trace position corresponding to the write sub-operation of register ic. + 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_STORE_C; + }); + ASSERT_TRUE(row != trace.end()); + mem_c_idx = static_cast(row - trace.begin()); + } + + void validate_trace(uint128_t const val, + uint32_t const src_offset, + uint32_t const dst_offset, + AvmMemoryTag const tag) + { + FF const val_ff = uint256_t::from_uint128(val); + auto const& main_row = trace.at(main_idx); + + EXPECT_EQ(main_row.avm_main_ia, val_ff); + EXPECT_EQ(main_row.avm_main_ib, FF(0)); + EXPECT_EQ(main_row.avm_main_ic, val_ff); + EXPECT_EQ(main_row.avm_main_in_tag, FF(static_cast(tag))); + + auto const& mem_a_row = trace.at(mem_a_idx); + + EXPECT_EQ(mem_a_row.avm_mem_m_tag_err, FF(0)); + EXPECT_EQ(mem_a_row.avm_mem_m_in_tag, FF(static_cast(tag))); + EXPECT_EQ(mem_a_row.avm_mem_m_tag, FF(static_cast(tag))); + EXPECT_EQ(mem_a_row.avm_mem_m_sel_mov, FF(1)); + EXPECT_EQ(mem_a_row.avm_mem_m_addr, FF(src_offset)); + EXPECT_EQ(mem_a_row.avm_mem_m_val, val_ff); + EXPECT_EQ(mem_a_row.avm_mem_m_op_a, FF(1)); + + auto const& mem_c_row = trace.at(mem_c_idx); + + EXPECT_EQ(mem_c_row.avm_mem_m_tag_err, FF(0)); + EXPECT_EQ(mem_c_row.avm_mem_m_in_tag, FF(static_cast(tag))); + EXPECT_EQ(mem_c_row.avm_mem_m_tag, FF(static_cast(tag))); + EXPECT_EQ(mem_c_row.avm_mem_m_addr, FF(dst_offset)); + EXPECT_EQ(mem_c_row.avm_mem_m_val, val_ff); + EXPECT_EQ(mem_c_row.avm_mem_m_op_c, FF(1)); + + validate_trace_proof(std::move(trace)); + } +}; + +class AvmMemOpcodeNegativeTests : public AvmMemOpcodeTests {}; + +/****************************************************************************** + * + * MEMORY OPCODE TESTS + * + ******************************************************************************/ + +TEST_F(AvmMemOpcodeTests, basicMov) +{ + buildTrace(42, 9, 13, AvmMemoryTag::U64); + validate_trace(42, 9, 13, AvmMemoryTag::U64); +} + +TEST_F(AvmMemOpcodeTests, sameAddressMov) +{ + + buildTrace(11, 356, 356, AvmMemoryTag::U16); + + validate_trace(11, 356, 356, AvmMemoryTag::U16); +} + +TEST_F(AvmMemOpcodeNegativeTests, wrongOutputErrorTag) +{ + buildTrace(234, 0, 1, AvmMemoryTag::U8); + trace.at(main_idx).avm_main_tag_err = 1; + + EXPECT_THROW_WITH_MESSAGE(validate_trace_proof(std::move(trace)), "INCL_MEM_TAG_ERR"); +} + +TEST_F(AvmMemOpcodeNegativeTests, wrongOutputValue) +{ + buildTrace(234, 0, 1, AvmMemoryTag::U8); + trace.at(main_idx).avm_main_ic = 233; + + EXPECT_THROW_WITH_MESSAGE(validate_trace_proof(std::move(trace)), "MOV_SAME_VALUE"); +} + +// We want to test that the output tag cannot be changed. +// In this test, we modify the m_in_tag for load operation to Ia. +// Then, we propagate the error tag and the copy of m_in_tag to the +// main trace and the memory entry related to stor operation from Ic. +TEST_F(AvmMemOpcodeNegativeTests, wrongOutputTagLoadIa) +{ + FF const tag_u64 = FF(static_cast(AvmMemoryTag::U64)); + FF const tag_u8 = FF(static_cast(AvmMemoryTag::U8)); + FF const one_min_inverse_diff = FF(1) - (tag_u64 - tag_u8).invert(); + + buildTrace(234, 0, 1, AvmMemoryTag::U8); + + trace.at(mem_a_idx).avm_mem_m_in_tag = tag_u64; + trace.at(mem_a_idx).avm_mem_m_tag_err = 1; + trace.at(mem_a_idx).avm_mem_m_one_min_inv = one_min_inverse_diff; + trace.at(mem_c_idx).avm_mem_m_tag = tag_u64; + trace.at(mem_c_idx).avm_mem_m_in_tag = tag_u64; + trace.at(main_idx).avm_main_in_tag = tag_u64; + trace.at(main_idx).avm_main_tag_err = 1; + + EXPECT_THROW_WITH_MESSAGE(validate_trace_proof(std::move(trace)), "MOV_SAME_TAG"); +} + +// Same as above but one tries to disable the selector of MOV opcode in +// the load operation. +TEST_F(AvmMemOpcodeNegativeTests, wrongOutputTagDisabledSelector) +{ + FF const tag_u64 = FF(static_cast(AvmMemoryTag::U64)); + FF const tag_u8 = FF(static_cast(AvmMemoryTag::U8)); + FF const one_min_inverse_diff = FF(1) - (tag_u64 - tag_u8).invert(); + + buildTrace(234, 0, 1, AvmMemoryTag::U8); + + trace.at(mem_a_idx).avm_mem_m_in_tag = tag_u64; + trace.at(mem_a_idx).avm_mem_m_tag_err = 1; + trace.at(mem_a_idx).avm_mem_m_one_min_inv = one_min_inverse_diff; + trace.at(mem_a_idx).avm_mem_m_sel_mov = 0; + trace.at(mem_c_idx).avm_mem_m_tag = tag_u64; + trace.at(mem_c_idx).avm_mem_m_in_tag = tag_u64; + trace.at(main_idx).avm_main_in_tag = tag_u64; + trace.at(main_idx).avm_main_tag_err = 1; + + EXPECT_THROW_WITH_MESSAGE(validate_trace_proof(std::move(trace)), "PERM_MAIN_MEM_A"); +} + +// The manipulation of the tag occurs in the main trace and then we +// propagate this change to the store memory operation of Ic. +TEST_F(AvmMemOpcodeNegativeTests, wrongOutputTagMainTrace) +{ + FF const tag_u64 = FF(static_cast(AvmMemoryTag::U64)); + + buildTrace(234, 0, 1, AvmMemoryTag::U8); + trace.at(main_idx).avm_main_in_tag = tag_u64; + + trace.at(mem_c_idx).avm_mem_m_tag = tag_u64; + trace.at(mem_c_idx).avm_mem_m_in_tag = tag_u64; + + EXPECT_THROW_WITH_MESSAGE(validate_trace_proof(std::move(trace)), "PERM_MAIN_MEM_A"); +} + +} // namespace tests_avm 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 d93dc15bddf..ac73aa1e55d 100644 --- a/barretenberg/cpp/src/barretenberg/vm/tests/avm_memory.test.cpp +++ b/barretenberg/cpp/src/barretenberg/vm/tests/avm_memory.test.cpp @@ -41,7 +41,6 @@ TEST_F(AvmMemoryTests, mismatchedTagAddOperation) EXPECT_TRUE(row != trace.end()); - // All intermediate registers should be set to zero. EXPECT_EQ(row->avm_main_ia, FF(98)); EXPECT_EQ(row->avm_main_ib, FF(12)); EXPECT_EQ(row->avm_main_ic, FF(0));