Merge pull request #3874 from AztecProtocol/md/avm-main-sync

chore: merge avm main

barretenberg/.gitignore

@@ -5,4 +5,5 @@ node_modules
 ts/dest
 .tsbuildinfo
 .idea
-cmake-build-debug
+cmake-build-debug
+*_opt.pil

barretenberg/cpp/pil/avm/avm_mini.pil

@@ -7,13 +7,44 @@ namespace avmMini(256);
     pol constant clk(i) { i };
     pol constant first = [1] + [0]*; // Used mostly to toggle off the first row consisting
                                      // only in first element of shifted polynomials.
+
+    //===== CONTROL FLOW ==========================================================
+    // Program counter
+    pol commit pc; 
+    // Return Pointer
+    pol commit internal_return_ptr;
 
-    //===== TABLE SUBOP-TR ========================================================
-    // Enum over sub operations
-    // 0: VOID
-    // 1: ADD
-    pol commit subop;
+    pol commit sel_internal_call;
+    pol commit sel_internal_return;
+    pol commit sel_jump;
+
+    // Halt program execution
+    pol commit sel_halt;
 
+    //===== TABLE SUBOP-TR ========================================================
+    // Boolean selectors for (sub-)operations. Only one operation is activated at
+    // a time.
+
+    // ADD
+    pol commit sel_op_add;
+    // SUB
+    pol commit sel_op_sub;
+    // MUL
+    pol commit sel_op_mul;
+    // DIV
+    pol commit sel_op_div;
+
+    // Instruction memory tag (0: uninitialized, 1: u8, 2: u16, 3: u32, 4: u64, 5: u128, 6:field)
+    pol commit in_tag;
+
+    // Errors
+    pol commit op_err; // Boolean flag pertaining to an operation error
+    pol commit tag_err; // Boolean flag (foreign key to memTrace.m_tag_err)
+
+    // A helper witness being the inverse of some value
+    // to show a non-zero equality
+    pol commit inv;
+
     // Intermediate register values
     pol commit ia;
     pol commit ib;
@@ -35,22 +66,137 @@ namespace avmMini(256);
     pol commit mem_idx_a;
     pol commit mem_idx_b;
     pol commit mem_idx_c;
-    
-    
+
+
     // Track the last line of the execution trace. It does NOT correspond to the last row of the whole table
     // of size N. As this depends on the supplied bytecode, this polynomial cannot be constant.
     pol commit last;
 
     // Relations on type constraints
-    subop * (1 - subop) = 0;
+
+    sel_op_add * (1 - sel_op_add) = 0;
+    sel_op_sub * (1 - sel_op_sub) = 0;
+    sel_op_mul * (1 - sel_op_mul) = 0;
+    sel_op_div * (1 - sel_op_div) = 0;
+
+    sel_internal_call * (1 - sel_internal_call) = 0;
+    sel_internal_return * (1 - sel_internal_return) = 0;
+    sel_jump * (1 - sel_jump) = 0;
+    sel_halt * (1 - sel_halt) = 0;
+
+    op_err * (1 - op_err) = 0;
+    tag_err * (1 - tag_err) = 0; // Potential optimization (boolean constraint derivation from equivalence check to memTrace)?
+
     mem_op_a * (1 - mem_op_a) = 0;
     mem_op_b * (1 - mem_op_b) = 0;
     mem_op_c * (1 - mem_op_c) = 0;
+
     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
+
+    // Set intermediate registers to 0 whenever tag_err occurs
+    tag_err * ia = 0;
+    tag_err * ib = 0;
+    tag_err * ic = 0;
+
     // Relation for addition over the finite field
-    subop * (ia + ib - ic) = 0;
+    #[SUBOP_ADDITION_FF]
+    sel_op_add * (ia + ib - ic) = 0;
+
+    // Relation for subtraction over the finite field
+    #[SUBOP_SUBTRACTION_FF]
+    sel_op_sub * (ia - ib - ic) = 0;
+
+    // Relation for multiplication over the finite field
+    #[SUBOP_MULTIPLICATION_FF]
+    sel_op_mul * (ia * ib - 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]
+    sel_op_div * (1 - op_err) * (ic * ib - ia) = 0;
+
+    // When sel_op_div == 1, we want ib == 0 <==> op_err == 1
+    // This can be achieved with the 2 following relations.
+    // inv is an extra witness to show that we can invert ib, i.e., inv = ib^(-1)
+    // If ib == 0, we have to set inv = 1 to satisfy the second relation,
+    // because op_err == 1 from the first relation.
+    #[SUBOP_DIVISION_ZERO_ERR1]
+    sel_op_div * (ib * inv - 1 + op_err) = 0;
+    #[SUBOP_DIVISION_ZERO_ERR2]
+    sel_op_div * op_err * (1 - inv) = 0;
+
+    // op_err cannot be maliciously activated for a non-relevant
+    // operation selector, i.e., op_err == 1 ==> sel_op_div || sel_op_XXX || ...
+    // op_err * (sel_op_div + sel_op_XXX + ... - 1) == 0
+    // Note that the above is even a stronger constraint, as it shows
+    // that exactly one sel_op_XXX must be true.
+    // At this time, we have only division producing an error.
+    #[SUBOP_ERROR_RELEVANT_OP]
+    op_err * (sel_op_div - 1) = 0;
+
+    // TODO: constraint that we stop execution at the first error (tag_err or op_err)
+    // An error can only happen at the last sub-operation row.
+
+    // OPEN/POTENTIAL OPTIMIZATION: Dedicated error per relevant operation?
+    // For the division, we could lower the degree from 4 to 3
+    // (sel_op_div - op_div_err) * (ic * ib - ia) = 0;
+    // Same for the relations related to the error activation:
+    // (ib * inv - 1 + op_div_err) = 0 && op_err * (1 - inv) = 0 
+    // This works in combination with op_div_err * (sel_op_div - 1) = 0;
+    // Drawback is the need to paralllelize the latter.
+
+    //===== CONTROL FLOW =======================================================
+    //===== JUMP ===============================================================
+    sel_jump * (pc' - ia) = 0;
+
+    //===== INTERNAL_CALL ======================================================
+    // - The program counter in the next row should be equal to the value loaded from the ia register
+    // - We then write the return location (pc + 1) into the call stack (in memory)
+
+    #[RETURN_POINTER_INCREMENT]
+    sel_internal_call * (internal_return_ptr' - (internal_return_ptr + 1)) = 0;
+    sel_internal_call * (internal_return_ptr - mem_idx_b) = 0;
+    sel_internal_call * (pc' - ia) = 0;
+    sel_internal_call * ((pc + 1) - ib) = 0;
+
+    // TODO(md): Below relations may be removed through sub-op table lookup
+    sel_internal_call * (rwb - 1) = 0;
+    sel_internal_call * (mem_op_b  - 1) = 0;
+
+    //===== INTERNAL_RETURN ===================================================
+    // - We load the memory pointer to be the internal_return_ptr 
+    // - Constrain then next program counter to be the loaded value
+    // - decrement the internal_return_ptr
+
+    #[RETURN_POINTER_DECREMENT]
+    sel_internal_return * (internal_return_ptr' - (internal_return_ptr - 1)) = 0;
+    sel_internal_return * ((internal_return_ptr - 1) - mem_idx_a) = 0;
+    sel_internal_return * (pc' - ia) = 0;
+
+    // TODO(md): Below relations may be removed through sub-op table lookup
+    sel_internal_return * rwa = 0;
+    sel_internal_return * (mem_op_a - 1) = 0;
+
+    //===== CONTROL_FLOW_CONSISTENCY ============================================
+    pol INTERNAL_CALL_STACK_SELECTORS = (first + sel_internal_call + sel_internal_return + sel_halt);
+    pol OPCODE_SELECTORS = (sel_op_add + sel_op_sub + sel_op_div + sel_op_mul);
+
+    // Program counter must increment if not jumping or returning
+    #[PC_INCREMENT]
+    (1 - first) * (1 - sel_halt) * OPCODE_SELECTORS * (pc' - (pc + 1)) = 0;
+
+    // first == 0 && sel_internal_call == 0 && sel_internal_return == 0 && sel_halt == 0 ==> internal_return_ptr == internal_return_ptr'
+    #[INTERNAL_RETURN_POINTER_CONSISTENCY]
+    (1 - INTERNAL_CALL_STACK_SELECTORS) * (internal_return_ptr' - internal_return_ptr) = 0; 
+
+    // TODO: we want to set an initial number for the reserved memory of the jump pointer
+
+    // Inter-table Constraints
 
-
+    // TODO: tag_err {clk} IS memTrace.m_tag_err {memTrace.m_clk}
+    // 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}

barretenberg/cpp/pil/avm/mem_trace.pil

@@ -7,29 +7,50 @@ namespace memTrace(256);
     pol commit m_clk;
     pol commit m_sub_clk;
     pol commit m_addr;
+    pol commit m_tag; // Memory tag (0: uninitialized, 1: u8, 2: u16, 3: u32, 4: u64, 5: u128, 6:field)
     pol commit m_val;
     pol commit m_lastAccess; // Boolean (1 when this row is the last of a given address)
+    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 avmMini.in_tag)
+
+    // Error columns
+    pol commit m_tag_err; // Boolean (1 if m_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
+
     // Type constraints
     m_lastAccess * (1 - m_lastAccess) = 0;
+    m_last * (1 - m_last) = 0;
     m_rw * (1 - m_rw) = 0;
-
+    m_tag_err * (1 - m_tag_err) = 0;
+
+    // TODO: m_addr is u32 and 0 <= m_tag <= 6
+    //       (m_in_tag will be constrained through inclusion check to main trace)
+
+    // Remark: m_lastAccess == 1 on first row and therefore any relation with the
+    //         multiplicative term (1 - m_lastAccess) implicitly includes (1 - avmMini.first)
+    //         Similarly, this includes (1 - m_last) as well.
+
     // m_lastAccess == 0 ==> m_addr' == m_addr
-    (1 -  avmMini.first) * (1 - m_lastAccess) * (m_addr' - m_addr) = 0;
+    // Optimization: We removed the term (1 - avmMini.first)
+    #[MEM_LAST_ACCESS_DELIMITER]
+    (1 - m_lastAccess) * (m_addr' - m_addr) = 0;
 
     // We need: m_lastAccess == 1 ==> m_addr' > m_addr
     // The above implies: m_addr' == m_addr ==> m_lastAccess == 0
     // This condition does not apply on the last row.
     // clk + 1 used as an expression for positive integers
     // TODO: Uncomment when lookups are supported
-    // (1 - first) * (1 - last) * m_lastAccess { (m_addr' - m_addr) } in clk + 1; // Gated inclusion check. Is it supported?
+    // (1 - first) * (1 - m_last) * m_lastAccess { (m_addr' - m_addr) } in clk + 1; // Gated inclusion check. Is it supported?
 
     // TODO: following constraint
     // m_addr' == m_addr && m_clk == m_clk' ==> m_sub_clk' - m_sub_clk > 0
-    // Can be enforced with (1 - first) * (1 - last) * (1 - m_lastAccess) { 6 * (m_clk' - m_clk) + m_sub_clk' - m_sub_clk } in clk + 1
+    // Can be enforced with (1 - first) * (1 - m_lastAccess) { 6 * (m_clk' - m_clk) + m_sub_clk' - m_sub_clk } in clk + 1
 
-    // Alternatively to the above, one could require 
+    // Alternatively to the above, one could require
     // that m_addr' - m_addr is 0 or 1 (needs to add placeholders m_addr values):
     // (m_addr' - m_addr) * (m_addr' - m_addr) - (m_addr' - m_addr) = 0;
     // if m_addr' - m_addr is 0 or 1, the following is equiv. to m_lastAccess
@@ -40,8 +61,46 @@ namespace memTrace(256);
     // Note: in barretenberg, a shifted polynomial will be 0 on the last row (shift is not cyclic)
     // Note2: in barretenberg, if a poynomial is shifted, its non-shifted equivalent must be 0 on the first row
 
-    (1 -  avmMini.first) * (1 -  avmMini.last) * (1 - m_lastAccess) * (1 - m_rw') * (m_val' - m_val) = 0;
+    // Optimization: We removed the term (1 - avmMini.first) and (1 - m_last)
+    #[MEM_READ_WRITE_VAL_CONSISTENCY]
+    (1 - m_lastAccess) * (1 - m_rw') * (m_val' - m_val) = 0;
 
-    // TODO: Constraint the first load from a given adress has value 0. (Consistency of memory initialization.)
+    // m_lastAccess == 0 && m_rw' == 0 ==> m_tag == m_tag'
+    // Optimization: We removed the term (1 - avmMini.first) and (1 - m_last)
+    #[MEM_READ_WRITE_TAG_CONSISTENCY]
+    (1 - m_lastAccess) * (1 - m_rw') * (m_tag' - m_tag) = 0;
+
+    // Constrain that the first load from a given address has value 0. (Consistency of memory initialization.)
+    // We do not constrain that the m_tag == 0 as the 0 value is compatible with any memory type.
+    // If we set m_lastAccess = 1 on the first row, we can enforce this (should be ok as long as we do not shift m_lastAccess):
+    #[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
+    // 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).
+    // 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
+    // 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
+    // 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;
+    #[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
+
     // TODO: when introducing load/store as sub-operations, we will have to add consistency of intermediate
-    // register values ia, ib, ic
+    // register values ia, ib, ic
+
+    // Inter-table Constraints
+
+    // TODO: {m_clk, m_in_tag} IN {avmMini.clk, avmMini.in_tag}

barretenberg/cpp/pil/avm/toy_avm.pil

@@ -0,0 +1,20 @@
+namespace toy(256);
+    pol commit q_tuple_set;
+
+    // Set 1
+    pol commit set_1_column_1;
+    pol commit set_1_column_2;
+    // Set 2
+    pol commit set_2_column_1;
+    pol commit set_2_column_2;
+
+    // This is a column based tuple lookup
+    #[two_column_perm] // the name of the inverse
+    q_tuple_set { set_1_column_1, set_1_column_2 } is { set_2_column_1, set_2_column_2 };
+
+    // Relation not used -> we currently require a single relation for codegen
+    pol commit x;
+    x' - x = 0;
+
+    // Also needs a fixed relation 
+    pol fixed first = [1] + [0]*;