feat(avm): EQ opcode output u8 and execution (#5402)

Resolves #5290

barretenberg/cpp/pil/avm/avm_main.pil

@@ -55,8 +55,9 @@ namespace avm_main(256);
     // Helper selector to characterize a Binary chiplet selector
     pol commit bin_sel;
 
-    // Instruction memory tag (1: u8, 2: u16, 3: u32, 4: u64, 5: u128, 6: field)
-    pol commit in_tag;
+    // Instruction memory tags read/write (1: u8, 2: u16, 3: u32, 4: u64, 5: u128, 6: field)
+    pol commit r_in_tag;
+    pol commit w_in_tag;
 
     // Errors
     pol commit op_err; // Boolean flag pertaining to an operation error
@@ -144,7 +145,12 @@ namespace avm_main(256);
     // TODO - Constraints:
     // - mem_idx_a, mem_idx_b, mem_idx_c to u32 type
     // - ind_a, ind_b, ind_c to u32 type
-    // - 0 <= in_tag <= 6
+    // - 0 <= r_in_tag, w_in_tag <= 6 // Maybe not needed as probably derived by the operation decomposition.
+
+    //====== COMPARATOR OPCODES CONSTRAINTS =====================================
+    // Enforce that the tag for the ouput of EQ opcode is u8 (i.e. equal to 1).
+    #[EQ_OUTPUT_U8]
+    sel_op_eq * (w_in_tag - 1) = 0;
 
     // Relation for division over the finite field
     // If tag_err == 1 in a division, then ib == 0 and op_err == 1.
@@ -230,6 +236,8 @@ namespace avm_main(256);
     //====== MEMORY OPCODES CONSTRAINTS =========================================
     #[MOV_SAME_VALUE]
     sel_mov * (ia - ic) = 0; // Ensure that the correct value is moved/copied.
+    #[MOV_MAIN_SAME_TAG]
+    sel_mov * (r_in_tag - w_in_tag) = 0;
 
     //====== Inter-table Constraints ============================================
     #[INCL_MAIN_TAG_ERR]
@@ -246,7 +254,7 @@ namespace avm_main(256);
     #[PERM_MAIN_ALU]
     alu_sel {clk, ia, ib, ic,
              sel_op_add, sel_op_sub, sel_op_mul, sel_op_eq,
-             sel_op_not, in_tag}
+             sel_op_not, r_in_tag}
     is
     avm_alu.alu_sel {avm_alu.alu_clk, avm_alu.alu_ia, avm_alu.alu_ib, avm_alu.alu_ic,
                      avm_alu.alu_op_add, avm_alu.alu_op_sub, avm_alu.alu_op_mul, avm_alu.alu_op_eq,
@@ -267,25 +275,28 @@ namespace avm_main(256);
     bin_sel = sel_op_and + sel_op_or + sel_op_xor;
 
     #[PERM_MAIN_BIN]
-    bin_sel {ia, ib, ic, bin_op_id, in_tag}
+    bin_sel {ia, ib, ic, bin_op_id, r_in_tag}
     is
     avm_binary.start {avm_binary.acc_ia, avm_binary.acc_ib, avm_binary.acc_ic,
                       avm_binary.op_id, avm_binary.in_tag};
 
     #[PERM_MAIN_MEM_A]
-    mem_op_a {clk, mem_idx_a, ia, rwa, in_tag, sel_mov}
+    mem_op_a {clk, mem_idx_a, ia, rwa, r_in_tag, w_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_sel_mov};
+    avm_mem.m_op_a {avm_mem.m_clk, avm_mem.m_addr, avm_mem.m_val, avm_mem.m_rw,
+                    avm_mem.r_in_tag, avm_mem.w_in_tag, avm_mem.m_sel_mov};
 
     #[PERM_MAIN_MEM_B]
-    mem_op_b {clk, mem_idx_b, ib, rwb, in_tag}
+    mem_op_b {clk, mem_idx_b, ib, rwb, r_in_tag, w_in_tag}
     is
-    avm_mem.m_op_b {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_b {avm_mem.m_clk, avm_mem.m_addr, avm_mem.m_val, avm_mem.m_rw,
+                    avm_mem.r_in_tag, avm_mem.w_in_tag};
 
     #[PERM_MAIN_MEM_C]
-    mem_op_c {clk, mem_idx_c, ic, rwc, in_tag}
+    mem_op_c {clk, mem_idx_c, ic, rwc, r_in_tag, w_in_tag}
     is
-    avm_mem.m_op_c {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_c {avm_mem.m_clk, avm_mem.m_addr, avm_mem.m_val, avm_mem.m_rw,
+                    avm_mem.r_in_tag, avm_mem.w_in_tag};
 
     #[PERM_MAIN_MEM_IND_A]
     ind_op_a {clk, ind_a, mem_idx_a}

barretenberg/cpp/pil/avm/avm_mem.pil

@@ -13,7 +13,8 @@ namespace avm_mem(256);
     pol commit m_last; // Boolean indicating the last row of the memory trace (not execution trace)
     pol commit m_rw; // Enum: 0 (read), 1 (write)
 
-    pol commit m_in_tag; // Instruction memory tag ("foreign key" pointing to avm_main.in_tag)
+    pol commit r_in_tag; // Instruction memory tag ("foreign key" pointing to avm_main.r_in_tag)
+    pol commit w_in_tag; // Instruction memory tag ("foreign key" pointing to avm_main.w_in_tag)
 
     // Indicator of the intermediate register pertaining to the memory operation (foreign key to avm_main.mem_op_XXX)
     pol commit m_op_a;
@@ -30,10 +31,10 @@ namespace avm_mem(256);
     pol commit m_sel_mov;
 
     // Error columns
-    pol commit m_tag_err; // Boolean (1 if m_in_tag != m_tag is detected)
+    pol commit m_tag_err; // Boolean (1 if r_in_tag != m_tag is detected)
 
     // Helper columns
-    pol commit m_one_min_inv; // Extra value to prove m_in_tag != m_tag with error handling
+    pol commit m_one_min_inv; // Extra value to prove r_in_tag != m_tag with error handling
 
     // Type constraints
     m_lastAccess * (1 - m_lastAccess) = 0;
@@ -48,7 +49,7 @@ namespace avm_mem(256);
     m_ind_op_c * (1 - m_ind_op_c) = 0;
 
     // TODO: m_addr is u32 and 0 <= m_tag <= 6
-    //       (m_in_tag will be constrained through inclusion check to main trace)
+    //       (r_in_tag, w_in_tag will be constrained through inclusion check to main trace)
 
     // Maximum one memory operation enabled per row
     pol MEM_SEL = m_op_a + m_op_b + m_op_c + m_ind_op_a + m_ind_op_b + m_ind_op_c;
@@ -105,46 +106,52 @@ namespace avm_mem(256);
     #[MEM_ZERO_INIT]
     m_lastAccess * (1 - m_rw') * m_val' = 0;
 
-    // Memory tag consistency check
-    // We want to prove that m_in_tag == m_tag <==> m_tag_err == 0
-    // We want to show that we can invert (m_in_tag - m_tag) when m_tag_err == 1,
-    // i.e., m_tag_err == 1 ==> m_in_tag != m_tag
+    // Memory tag consistency check for load operations, i.e., m_rw == 0.
+    // We want to prove that r_in_tag == m_tag <==> m_tag_err == 0
+    // We want to show that we can invert (r_in_tag - m_tag) when m_tag_err == 1,
+    // i.e., m_tag_err == 1 ==> r_in_tag != m_tag
     // For this purpose, we need an extra column to store a witness
-    // which can be used to show that (m_in_tag - m_tag) is invertible (non-zero).
+    // which can be used to show that (r_in_tag - m_tag) is invertible (non-zero).
     // We re-use the same zero (non)-equality technique as in SUBOP_DIVISION_ZERO_ERR1/2 applied
-    // to (m_in_tag - m_tag) by replacing m_tag_err by 1 - m_tag_err because here
+    // to (r_in_tag - m_tag) by replacing m_tag_err by 1 - m_tag_err because here
     // the equality to zero is not an error. Another modification
-    // consists in storing 1 - (m_in_tag - m_tag)^(-1) in the extra witness column
-    // instead of (m_in_tag - m_tag)^(-1) as this allows to store zero by default (i.e., when m_tag_err == 0).
-    // The new column m_one_min_inv is set to 1 - (m_in_tag - m_tag)^(-1) when m_tag_err == 1
+    // consists in storing 1 - (r_in_tag - m_tag)^(-1) in the extra witness column
+    // instead of (r_in_tag - m_tag)^(-1) as this allows to store zero by default (i.e., when m_tag_err == 0).
+    // The new column m_one_min_inv is set to 1 - (r_in_tag - m_tag)^(-1) when m_tag_err == 1
     // but must be set to 0 when tags are matching and m_tag_err = 0
     #[MEM_IN_TAG_CONSISTENCY_1]
-    (m_in_tag - m_tag) * (1 - m_one_min_inv) - m_tag_err = 0;
+    (1 - m_rw) * ((r_in_tag - m_tag) * (1 - m_one_min_inv) - m_tag_err) = 0;
     #[MEM_IN_TAG_CONSISTENCY_2]
     (1 - m_tag_err) * m_one_min_inv = 0;
 
-    // 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
+    // Correctness of two above checks MEM_IN_TAG_CONSISTENCY_1/2 (assuming m_rw == 0):
+    // r_in_tag == m_tag ==> m_tag_err == 0 (first relation)
+    // m_tag_err == 0 ==> m_one_min_inv == 0 by second relation. First relation ==> r_in_tag - m_tag == 0
+
+    // Enforce that a write instruction tag is equal to m_tag for a write operation
+    m_rw * (w_in_tag - m_tag) = 0;
+
+    // Enforce that a write instruction never leads to a tag error
+    #[NO_TAG_ERR_WRITE]
+    m_rw * m_tag_err = 0;
 
     //====== Indirect Memory Constraints =====================================
-    // Enforce m_in_tag == 3, i.e., in_tag must be U32
-    m_ind_op_a * (m_in_tag - 3) = 0;
-    m_ind_op_b * (m_in_tag - 3) = 0;
-    m_ind_op_c * (m_in_tag - 3) = 0;
+    // Enforce r_in_tag == 3, i.e., r_in_tag must be U32
+    m_ind_op_a * (r_in_tag - 3) = 0;
+    m_ind_op_b * (r_in_tag - 3) = 0;
+    m_ind_op_c * (r_in_tag - 3) = 0;
 
     // Indirect operation is always a load
     m_ind_op_a * m_rw = 0;
     m_ind_op_b * m_rw = 0;
     m_ind_op_c * m_rw = 0;
 
-    //====== MOV Opcode in_tag Constraint =====================================
-    // The following constraint ensures that the m_in_tag is set to m_tag for
+    //====== MOV Opcode Tag Constraint =====================================
+    // The following constraint ensures that the r_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.
+    // The permutation check #[PERM_MAIN_MEM_A] guarantees that the r_in_tag
+    // value load operation for Ia is copied back in the main trace.
+    // Constraint #[MOV_MAIN_SAME_TAG] copies r_in_tag to w_in_tag in the main
+    // trace. Then, #[PERM_MAIN_MEM_C] copies w_in_tag for store operation from Ic.
     #[MOV_SAME_TAG]
-    m_sel_mov * m_tag_err = 0; // Equivalent to m_sel_mov * (m_in_tag - m_tag) = 0
+    m_sel_mov * m_tag_err = 0; // Equivalent to m_sel_mov * (r_in_tag - m_tag) = 0

barretenberg/cpp/src/barretenberg/relations/generated/avm/avm_alu.hpp

@@ -7,77 +7,77 @@
 namespace bb::Avm_vm {
 
 template <typename FF> struct Avm_aluRow {
-    FF avm_alu_alu_u8_r0{};
-    FF avm_alu_alu_op_eq_diff_inv{};
-    FF avm_alu_alu_op_eq{};
-    FF avm_alu_alu_u16_r3{};
-    FF avm_alu_alu_u64_r0{};
-    FF avm_alu_alu_u16_r4{};
-    FF avm_alu_alu_u16_r3_shift{};
-    FF avm_alu_alu_u16_r6_shift{};
-    FF avm_alu_alu_u16_r0_shift{};
-    FF avm_alu_alu_u16_r1_shift{};
-    FF avm_alu_alu_u16_r1{};
     FF avm_alu_alu_in_tag{};
-    FF avm_alu_alu_cf{};
-    FF avm_alu_alu_op_not{};
-    FF avm_alu_alu_u16_r6{};
-    FF avm_alu_alu_ib{};
-    FF avm_alu_alu_op_add{};
-    FF avm_alu_alu_u128_tag{};
     FF avm_alu_alu_u16_r2_shift{};
-    FF avm_alu_alu_sel{};
-    FF avm_alu_alu_u16_r7_shift{};
-    FF avm_alu_alu_u16_r7{};
+    FF avm_alu_alu_u8_tag{};
+    FF avm_alu_alu_u16_r0_shift{};
+    FF avm_alu_alu_u16_r3_shift{};
     FF avm_alu_alu_u16_r0{};
+    FF avm_alu_alu_cf{};
+    FF avm_alu_alu_op_mul{};
     FF avm_alu_alu_u32_tag{};
+    FF avm_alu_alu_u64_tag{};
+    FF avm_alu_alu_u16_r1{};
+    FF avm_alu_alu_u16_r1_shift{};
+    FF avm_alu_alu_u16_r4_shift{};
+    FF avm_alu_alu_u64_r0{};
+    FF avm_alu_alu_u16_r7{};
+    FF avm_alu_alu_ib{};
+    FF avm_alu_alu_u16_r7_shift{};
     FF avm_alu_alu_ia{};
-    FF avm_alu_alu_ic{};
-    FF avm_alu_alu_u8_tag{};
+    FF avm_alu_alu_op_sub{};
+    FF avm_alu_alu_u8_r0{};
+    FF avm_alu_alu_op_not{};
+    FF avm_alu_alu_ff_tag{};
+    FF avm_alu_alu_u16_r2{};
+    FF avm_alu_alu_u16_r4{};
     FF avm_alu_alu_u8_r1{};
-    FF avm_alu_alu_u16_r4_shift{};
+    FF avm_alu_alu_u16_r6_shift{};
+    FF avm_alu_alu_op_eq{};
+    FF avm_alu_alu_op_add{};
+    FF avm_alu_alu_op_eq_diff_inv{};
     FF avm_alu_alu_u16_r5_shift{};
-    FF avm_alu_alu_u16_r2{};
-    FF avm_alu_alu_op_mul{};
-    FF avm_alu_alu_ff_tag{};
-    FF avm_alu_alu_u64_tag{};
-    FF avm_alu_alu_op_sub{};
     FF avm_alu_alu_u16_tag{};
+    FF avm_alu_alu_u128_tag{};
+    FF avm_alu_alu_u16_r6{};
+    FF avm_alu_alu_u16_r3{};
     FF avm_alu_alu_u16_r5{};
+    FF avm_alu_alu_ic{};
+    FF avm_alu_alu_sel{};
 };
 
 inline std::string get_relation_label_avm_alu(int index)
 {
     switch (index) {
-    case 20:
-        return "ALU_OP_EQ";
-
     case 13:
         return "ALU_MUL_COMMON_2";
 
-    case 16:
-        return "ALU_MULTIPLICATION_OUT_U128";
+    case 20:
+        return "ALU_OP_EQ";
 
-    case 18:
-        return "ALU_OP_NOT";
+    case 11:
+        return "ALU_MULTIPLICATION_FF";
 
     case 19:
         return "ALU_RES_IS_BOOL";
 
-    case 11:
-        return "ALU_MULTIPLICATION_FF";
+    case 9:
+        return "ALU_ADD_SUB_1";
+
+    case 16:
+        return "ALU_MULTIPLICATION_OUT_U128";
 
     case 12:
         return "ALU_MUL_COMMON_1";
 
-    case 9:
-        return "ALU_ADD_SUB_1";
+    case 10:
+        return "ALU_ADD_SUB_2";
 
     case 17:
         return "ALU_FF_NOT_XOR";
 
-    case 10:
-        return "ALU_ADD_SUB_2";
+    case 18:
+        return "ALU_OP_NOT";
     }
     return std::to_string(index);
 }

barretenberg/cpp/src/barretenberg/relations/generated/avm/avm_binary.hpp

@@ -7,43 +7,43 @@
 namespace bb::Avm_vm {
 
 template <typename FF> struct Avm_binaryRow {
-    FF avm_binary_bin_sel{};
-    FF avm_binary_acc_ib{};
-    FF avm_binary_mem_tag_ctr{};
+    FF avm_binary_mem_tag_ctr_inv{};
     FF avm_binary_bin_ic_bytes{};
-    FF avm_binary_acc_ic_shift{};
     FF avm_binary_acc_ia{};
-    FF avm_binary_op_id_shift{};
+    FF avm_binary_acc_ib{};
+    FF avm_binary_acc_ic{};
+    FF avm_binary_mem_tag_ctr_shift{};
     FF avm_binary_acc_ia_shift{};
+    FF avm_binary_op_id_shift{};
+    FF avm_binary_bin_sel{};
+    FF avm_binary_bin_ib_bytes{};
     FF avm_binary_op_id{};
-    FF avm_binary_mem_tag_ctr_shift{};
-    FF avm_binary_acc_ic{};
     FF avm_binary_bin_ia_bytes{};
-    FF avm_binary_bin_ib_bytes{};
-    FF avm_binary_mem_tag_ctr_inv{};
     FF avm_binary_acc_ib_shift{};
+    FF avm_binary_mem_tag_ctr{};
+    FF avm_binary_acc_ic_shift{};
 };
 
 inline std::string get_relation_label_avm_binary(int index)
 {
     switch (index) {
-    case 1:
-        return "OP_ID_REL";
+    case 9:
+        return "ACC_REL_C";
 
     case 7:
         return "ACC_REL_A";
 
+    case 1:
+        return "OP_ID_REL";
+
+    case 2:
+        return "MEM_TAG_REL";
+
     case 8:
         return "ACC_REL_B";
 
-    case 9:
-        return "ACC_REL_C";
-
     case 3:
         return "BIN_SEL_CTR_REL";
-
-    case 2:
-        return "MEM_TAG_REL";
     }
     return std::to_string(index);
 }