Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
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