Skip to content

Commit

Permalink
feat(avm): VM circuit handles tagged memory (#3725)
Browse files Browse the repository at this point in the history 
Resolves #3644
  • Loading branch information
@jeanmon
jeanmon committed Dec 19, 2023
1 parent 78cf525 commit 739fe90
Show file tree
Hide file tree
Showing 16 changed files with 1,109 additions and 403 deletions.
41 changes: 34 additions & 7 deletions barretenberg/cpp/pil/avm/avm_mini.pil
View file
Original file line number Diff line number Diff line change
Expand Up @@ -21,8 +21,12 @@ namespace avmMini(256);
// DIV
pol commit sel_op_div;

// Error boolean flag pertaining to an operation
pol commit op_err;
// 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
Expand All @@ -49,8 +53,8 @@ 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;
Expand All @@ -63,6 +67,7 @@ namespace avmMini(256);
sel_op_div * (1 - sel_op_div) = 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;
Expand All @@ -72,23 +77,38 @@ namespace avmMini(256);
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_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.
// 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
Expand All @@ -97,9 +117,10 @@ namespace avmMini(256);
// 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
// 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?
Expand All @@ -108,4 +129,10 @@ namespace avmMini(256);
// 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.
// Drawback is the need to paralllelize the latter.

// 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}
21 changes: 19 additions & 2 deletions barretenberg/cpp/pil/avm/avm_mini_opt.pil
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,21 +2,34 @@ namespace memTrace(256);
col witness m_clk;
col witness m_sub_clk;
col witness m_addr;
col witness m_tag;
col witness m_val;
col witness m_lastAccess;
col witness m_last;
col witness m_rw;
col witness m_in_tag;
col witness m_tag_err;
col witness m_one_min_inv;
(memTrace.m_lastAccess * (1 - memTrace.m_lastAccess)) = 0;
(memTrace.m_last * (1 - memTrace.m_last)) = 0;
(memTrace.m_rw * (1 - memTrace.m_rw)) = 0;
(((1 - avmMini.first) * (1 - memTrace.m_lastAccess)) * (memTrace.m_addr' - memTrace.m_addr)) = 0;
(((((1 - avmMini.first) * (1 - avmMini.last)) * (1 - memTrace.m_lastAccess)) * (1 - memTrace.m_rw')) * (memTrace.m_val' - memTrace.m_val)) = 0;
(memTrace.m_tag_err * (1 - memTrace.m_tag_err)) = 0;
((1 - memTrace.m_lastAccess) * (memTrace.m_addr' - memTrace.m_addr)) = 0;
(((1 - memTrace.m_lastAccess) * (1 - memTrace.m_rw')) * (memTrace.m_val' - memTrace.m_val)) = 0;
(((1 - memTrace.m_lastAccess) * (1 - memTrace.m_rw')) * (memTrace.m_tag' - memTrace.m_tag)) = 0;
((memTrace.m_lastAccess * (1 - memTrace.m_rw')) * memTrace.m_val') = 0;
((memTrace.m_in_tag - memTrace.m_tag) * (1 - memTrace.m_one_min_inv)) = memTrace.m_tag_err;
((1 - memTrace.m_tag_err) * memTrace.m_one_min_inv) = 0;
namespace avmMini(256);
col fixed clk(i) { i };
col fixed first = [1] + [0]*;
col witness sel_op_add;
col witness sel_op_sub;
col witness sel_op_mul;
col witness sel_op_div;
col witness in_tag;
col witness op_err;
col witness tag_err;
col witness inv;
col witness ia;
col witness ib;
Expand All @@ -36,12 +49,16 @@ namespace avmMini(256);
(avmMini.sel_op_mul * (1 - avmMini.sel_op_mul)) = 0;
(avmMini.sel_op_div * (1 - avmMini.sel_op_div)) = 0;
(avmMini.op_err * (1 - avmMini.op_err)) = 0;
(avmMini.tag_err * (1 - avmMini.tag_err)) = 0;
(avmMini.mem_op_a * (1 - avmMini.mem_op_a)) = 0;
(avmMini.mem_op_b * (1 - avmMini.mem_op_b)) = 0;
(avmMini.mem_op_c * (1 - avmMini.mem_op_c)) = 0;
(avmMini.rwa * (1 - avmMini.rwa)) = 0;
(avmMini.rwb * (1 - avmMini.rwb)) = 0;
(avmMini.rwc * (1 - avmMini.rwc)) = 0;
(avmMini.tag_err * avmMini.ia) = 0;
(avmMini.tag_err * avmMini.ib) = 0;
(avmMini.tag_err * avmMini.ic) = 0;
(avmMini.sel_op_add * ((avmMini.ia + avmMini.ib) - avmMini.ic)) = 0;
(avmMini.sel_op_sub * ((avmMini.ia - avmMini.ib) - avmMini.ic)) = 0;
(avmMini.sel_op_mul * ((avmMini.ia * avmMini.ib) - avmMini.ic)) = 0;
Expand Down
77 changes: 68 additions & 9 deletions barretenberg/cpp/pil/avm/mem_trace.pil
View file
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand All @@ -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}

0 comments on commit 739fe90

Please sign in to comment.