feat(avm): ALU <--> MAIN inter table relation on intermediate registe…

…rs copy (#4945)

Resolves #4613

cpp/pil/avm/avm_alu.pil

@@ -17,6 +17,10 @@ namespace avm_alu(256);
     pol commit alu_op_div;
     pol commit alu_op_not;
     pol commit alu_op_eq;
+    pol commit alu_sel; // Predicate to activate the copy of intermediate registers to ALU table.
+
+    // Instruction tag (1: u8, 2: u16, 3: u32, 4: u64, 5: u128, 6: field) copied from Main table
+    pol commit alu_in_tag;
 
     // Flattened boolean instruction tags
     pol commit alu_ff_tag;
@@ -46,6 +50,9 @@ namespace avm_alu(256);
     // Carry flag
     pol commit alu_cf;
 
+    // Compute predicate telling whether there is a row entry in the ALU table.
+    alu_sel = alu_op_add + alu_op_sub + alu_op_mul + alu_op_not + alu_op_eq;
+
     // ========= Type Constraints =============================================
     // TODO: Range constraints
     //       - for slice registers
@@ -54,7 +61,6 @@ namespace avm_alu(256);
     //       Carry flag: We will have to constraint to ensure that the 
     //                   arithmetic expressions are not overflowing finite field size
     // Remark: Operation selectors are constrained in the main trace.
-    //         TODO: Enforce the equivalence check for the selectors between both tables.
 
     // Boolean flattened instructions tags
     alu_ff_tag * (1 - alu_ff_tag) = 0;
@@ -64,17 +70,17 @@ namespace avm_alu(256);
     alu_u64_tag * (1 - alu_u64_tag) = 0;
     alu_u128_tag * (1 - alu_u128_tag) = 0;
 
+    // Mutual exclusion of the flattened instruction tag.
+    alu_sel * (alu_ff_tag + alu_u8_tag + alu_u16_tag + alu_u32_tag + alu_u64_tag + alu_u128_tag - 1) = 0;
+
+    // Correct flattening of the instruction tag.
+    alu_in_tag = alu_u8_tag + 2 * alu_u16_tag + 3 * alu_u32_tag + 4 * alu_u64_tag + 5 * alu_u128_tag + 6 * alu_ff_tag;
+
     // Operation selectors are copied from main table and do not need to be constrained here.
     // TODO: Ensure mutual exclusion of alu_op_add and alu_op_sub as some relations below
     //       requires it.
-    // TODO: Similarly, ensure the mutual exclusion of instruction tags
-
-    // ========= Inter-table Constraints ======================================
-    // TODO: Equivalence between intermediate registers, clk, type flag, operation
-    //       An ALU chiplet flag will be introduced in main trace to select relevant rows.
-
 
-    // ========= EXPLANATIONS =================================================
+    // ========= ARITHMETIC OPERATION - EXPLANATIONS =================================================
     // Main trick for arithmetic operations modulo 2^k is to perform the operation
     // over the integers and expressing the result as low + high * 2^k with low
     // smaller than 2^k. low is used as the output. This works as long this does

cpp/pil/avm/avm_main.pil

@@ -39,7 +39,10 @@ namespace avm_main(256);
     // EQ
     pol commit sel_op_eq;
 
-    // Instruction memory tag (0: uninitialized, 1: u8, 2: u16, 3: u32, 4: u64, 5: u128, 6:field)
+    // Helper selector to characterize an ALU chiplet selector
+    pol commit alu_sel;
+
+    // Instruction memory tag (1: u8, 2: u16, 3: u32, 4: u64, 5: u128, 6: field)
     pol commit in_tag;
 
     // Errors
@@ -104,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]
@@ -195,5 +193,19 @@ namespace avm_main(256);
     #[equiv_tag_err]
     avm_mem.m_tag_err {avm_mem.m_clk} in tag_err {clk};
 
+    // Predicate to activate the copy of intermediate registers to ALU table. If tag_err == 1,
+    // the operation is not copied to the ALU table.
+    // TODO: when division is moved to the alu, we will need to add the selector in the list below:
+    alu_sel = (sel_op_add + sel_op_sub + sel_op_mul + sel_op_not + sel_op_eq) * (1 - tag_err);
+
+    #[equiv_inter_reg_alu]
+    alu_sel {clk, ia, ib, ic,
+             sel_op_add, sel_op_sub, sel_op_mul, sel_op_eq,
+             sel_op_not, 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,
+                     avm_alu.alu_op_not, avm_alu.alu_in_tag};
+
     // TODO: Map memory trace with intermediate register values whenever there is no tag error, sthg like:
     // mem_op_a * (1 - tag_err) {mem_idx_a, clk, ia, rwa} IS m_sub_clk == 0 && 1 - m_tag_err {m_addr, m_clk, m_val, m_rw}