4955: Equivalence check between Main trace and Mem trace

barretenberg/cpp/pil/avm/avm_main.pil

@@ -62,7 +62,7 @@ namespace avm_main(256);
     pol commit mem_op_a;
     pol commit mem_op_b;
     pol commit mem_op_c;
-    
+
     // Read-write flag per intermediate register: Read = 0, Write = 1
     pol commit rwa;
     pol commit rwb;
@@ -104,7 +104,7 @@ namespace avm_main(256);
     rwa * (1 - rwa) = 0;
     rwb * (1 - rwb) = 0;
     rwc * (1 - rwc) = 0;
-    
+
     // TODO: Constrain rwa, rwb, rwc to u32 type and 0 <= in_tag <= 6
 
     // Relation for division over the finite field
@@ -189,7 +189,7 @@ namespace avm_main(256);
     // TODO: we want to set an initial number for the reserved memory of the jump pointer
 
     // Inter-table Constraints
-    
+
     #[equiv_tag_err]
     avm_mem.m_tag_err {avm_mem.m_clk} in tag_err {clk};
 
@@ -207,5 +207,17 @@ namespace avm_main(256);
                      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}
+    #[equiv_main_mem_a]
+    mem_op_a {clk, mem_idx_a, ia, rwa, in_tag}
+    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};
+
+    #[equiv_main_mem_b]
+    mem_op_b {clk, mem_idx_b, ib, rwb, 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};
+
+    #[equiv_main_mem_c]
+    mem_op_c {clk, mem_idx_c, ic, rwc, 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};

barretenberg/cpp/pil/avm/avm_mem.pil

@@ -15,6 +15,11 @@ namespace avm_mem(256);
 
     pol commit m_in_tag; // Instruction memory tag ("foreign key" pointing to avm_main.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;
+    pol commit m_op_b;
+    pol commit m_op_c;
+
     // Error columns
     pol commit m_tag_err; // Boolean (1 if m_in_tag != m_tag is detected)
 
@@ -26,10 +31,20 @@ namespace avm_mem(256);
     m_last * (1 - m_last) = 0;
     m_rw * (1 - m_rw) = 0;
     m_tag_err * (1 - m_tag_err) = 0;
+    m_op_a * (1 - m_op_a) = 0;
+    m_op_b * (1 - m_op_b) = 0;
+    m_op_c * (1 - m_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)
 
+    // sub_clk derivation
+    m_sub_clk = 3 * m_rw + m_op_b + 2 * m_op_c;
+
+    // Maximum one memory operation enabled per row
+    pol M_OP_SUM = m_op_a + m_op_b + m_op_c;
+    M_OP_SUM * (M_OP_SUM - 1) = 0;
+
     // Remark: m_lastAccess == 1 on first row and therefore any relation with the
     //         multiplicative term (1 - m_lastAccess) implicitly includes (1 - avm_main.first)
     //         Similarly, this includes (1 - m_last) as well.
@@ -96,11 +111,4 @@ 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
-
-    // TODO: when introducing load/store as sub-operations, we will have to add consistency of intermediate
-    // register values ia, ib, ic
-
-    // Inter-table Constraints
-
-    // TODO: {m_clk, m_in_tag} IN {avm_main.clk, avm_main.in_tag}
+    // m_tag_err == 0 ==> m_one_min_inv == 0 by second relation. First relation ==> m_in_tag - m_tag == 0