feat(avm): back in avm context with macro - refactor context (#4438)

Fixes: AztecProtocol/aztec-packages#4313

cpp/pil/avm/avm.pil

@@ -0,0 +1,191 @@
+
+include "mem_trace.pil";
+include "alu_chip.pil";
+
+namespace avmMini(256);
+
+    //===== CONSTANT POLYNOMIALS ==================================================
+    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;
+
+    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;
+    pol commit ic;
+
+    // Memory operation per intermediate register
+    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;
+    pol commit rwc;
+
+    // Memory index involved into a memory operation per pertaining intermediate register
+    // We should range constrain it to 32 bits ultimately. For first mini-AVM,
+    // we will assume that these columns are of the right type.
+    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
+
+    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 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}