Skip to content

Commit

Permalink
feat(avm): back in avm context with macro - refactor context (AztecPr…
Browse files Browse the repository at this point in the history
  • Loading branch information
Maddiaa0 authored Feb 6, 2024
1 parent 9f2a6eb commit ccf9b17
Show file tree
Hide file tree
Showing 7 changed files with 933 additions and 618 deletions.
191 changes: 191 additions & 0 deletions barretenberg/cpp/pil/avm/avm.pil
Original file line number Diff line number Diff line change
@@ -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}
33 changes: 33 additions & 0 deletions noir/aztec_macros/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -645,6 +645,10 @@ fn transform_vm_function(
func: &mut NoirFunction,
_storage_defined: bool,
) -> Result<(), AztecMacroError> {
// Push Avm context creation to the beginning of the function
let create_context = create_avm_context()?;
func.def.body.0.insert(0, create_context);

// We want the function to be seen as a public function
func.def.is_open = true;

Expand Down Expand Up @@ -1158,6 +1162,35 @@ fn create_context(ty: &str, params: &[Param]) -> Result<Vec<Statement>, AztecMac
Ok(injected_expressions)
}

/// Creates an mutable avm context
///
/// ```noir
/// /// Before
/// #[aztec(public-vm)]
/// fn foo() -> Field {
/// let mut context = aztec::context::AVMContext::new();
/// let timestamp = context.timestamp();
/// // ...
/// }
///
/// /// After
/// #[aztec(private)]
/// fn foo() -> Field {
/// let mut timestamp = context.timestamp();
/// // ...
/// }
fn create_avm_context() -> Result<Statement, AztecMacroError> {
let let_context = mutable_assignment(
"context", // Assigned to
call(
variable_path(chained_path!("aztec", "context", "AVMContext", "new")), // Path
vec![], // args
),
);

Ok(let_context)
}

/// Abstract Return Type
///
/// This function intercepts the function's current return type and replaces it with pushes
Expand Down
Loading

0 comments on commit ccf9b17

Please sign in to comment.