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
41 changes: 38 additions & 3 deletions barretenberg/cpp/pil/avm/avm_main.pil
Original file line number Diff line number Diff line change
Expand Up @@ -61,7 +61,7 @@ namespace avm_main(256);
pol commit ib;
pol commit ic;

// Memory operation per intermediate register
// Memory operation selector per intermediate register
pol commit mem_op_a;
pol commit mem_op_b;
pol commit mem_op_c;
Expand All @@ -71,6 +71,17 @@ namespace avm_main(256);
pol commit rwb;
pol commit rwc;

// Indirect register values
pol commit ind_a;
pol commit ind_b;
pol commit ind_c;

// Indirect memory operation selector per indirect register
pol commit ind_op_a;
pol commit ind_op_b;
pol commit ind_op_c;


// Memory index involved into a memory operation per pertaining intermediate register
// We should range constrain it to 32 bits ultimately. For first version of the AVM,
// we will assume that these columns are of the right type.
Expand Down Expand Up @@ -103,6 +114,7 @@ namespace avm_main(256);
op_err * (1 - op_err) = 0;
tag_err * (1 - tag_err) = 0; // Potential optimization (boolean constraint derivation from equivalence check to avm_mem)?

// Might be removed if derived from opcode based on a lookup of constants
mem_op_a * (1 - mem_op_a) = 0;
mem_op_b * (1 - mem_op_b) = 0;
mem_op_c * (1 - mem_op_c) = 0;
Expand All @@ -111,7 +123,15 @@ namespace avm_main(256);
rwb * (1 - rwb) = 0;
rwc * (1 - rwc) = 0;

// TODO: Constrain rwa, rwb, rwc to u32 type and 0 <= in_tag <= 6
// Might be removed if derived from opcode based on a lookup of constants
ind_op_a * (1 - ind_op_a) = 0;
ind_op_b * (1 - ind_op_b) = 0;
ind_op_c * (1 - ind_op_c) = 0;

// TODO - Constraints:
// - mem_idx_a, mem_idx_b, mem_idx_c to u32 type
// - ind_a, ind_b, ind_c to u32 type
// - 0 <= in_tag <= 6

// Relation for division over the finite field
// If tag_err == 1 in a division, then ib == 0 and op_err == 1.
Expand Down Expand Up @@ -232,4 +252,19 @@ namespace avm_main(256);
#[PERM_MAIN_MEM_C]
mem_op_c {clk, mem_idx_c, ic, rwc, in_tag}
is
avm_mem.m_op_c {avm_mem.m_clk, avm_mem.m_addr, avm_mem.m_val, avm_mem.m_rw, avm_mem.m_in_tag};
avm_mem.m_op_c {avm_mem.m_clk, avm_mem.m_addr, avm_mem.m_val, avm_mem.m_rw, avm_mem.m_in_tag};

#[PERM_MAIN_MEM_IND_A]
ind_op_a {clk, ind_a, mem_idx_a}
is
avm_mem.m_ind_op_a {avm_mem.m_clk, avm_mem.m_addr, avm_mem.m_val};

#[PERM_MAIN_MEM_IND_B]
ind_op_b {clk, ind_b, mem_idx_b}
is
avm_mem.m_ind_op_b {avm_mem.m_clk, avm_mem.m_addr, avm_mem.m_val};

#[PERM_MAIN_MEM_IND_C]
ind_op_c {clk, ind_c, mem_idx_c}
is
avm_mem.m_ind_op_c {avm_mem.m_clk, avm_mem.m_addr, avm_mem.m_val};
31 changes: 26 additions & 5 deletions barretenberg/cpp/pil/avm/avm_mem.pil
Original file line number Diff line number Diff line change
Expand Up @@ -20,6 +20,11 @@ namespace avm_mem(256);
pol commit m_op_b;
pol commit m_op_c;

// Indicator of the indirect register pertaining to the memory operation (foreign key to avm_main.ind_op_XXX)
pol commit m_ind_op_a;
pol commit m_ind_op_b;
pol commit m_ind_op_c;

// Selector for MOV opcode (copied from main trace for loading operation on intermediated register ia)
// Boolean constraint is performed in main trace.
pol commit m_sel_mov;
Expand All @@ -38,16 +43,21 @@ namespace avm_mem(256);
m_op_a * (1 - m_op_a) = 0;
m_op_b * (1 - m_op_b) = 0;
m_op_c * (1 - m_op_c) = 0;
m_ind_op_a * (1 - m_ind_op_a) = 0;
m_ind_op_b * (1 - m_ind_op_b) = 0;
m_ind_op_c * (1 - m_ind_op_c) = 0;

// TODO: m_addr is u32 and 0 <= m_tag <= 6
// (m_in_tag will be constrained through inclusion check to main trace)

// sub_clk derivation
m_sub_clk = 3 * m_rw + m_op_b + 2 * m_op_c;

// Maximum one memory operation enabled per row
pol M_OP_SUM = m_op_a + m_op_b + m_op_c;
M_OP_SUM * (M_OP_SUM - 1) = 0;
pol MEM_SEL = m_op_a + m_op_b + m_op_c + m_ind_op_a + m_ind_op_b + m_ind_op_c;
MEM_SEL * (MEM_SEL - 1) = 0;

// sub_clk derivation
pol IND_OP = m_ind_op_a + m_ind_op_b + m_ind_op_c;
m_sub_clk = MEM_SEL * (m_ind_op_b + m_op_b + 2 * (m_ind_op_c + m_op_c) + 3 * (1 - IND_OP + m_rw));
// We need the MEM_SEL factor as the right factor is not zero when all columns are zero.

// Remark: m_lastAccess == 1 on first row and therefore any relation with the
// multiplicative term (1 - m_lastAccess) implicitly includes (1 - avm_main.first)
Expand Down Expand Up @@ -117,6 +127,17 @@ namespace avm_mem(256);
// 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

//====== Indirect Memory Constraints =====================================
// Enforce m_in_tag == 3, i.e., in_tag must be U32
m_ind_op_a * (m_in_tag - 3) = 0;
m_ind_op_b * (m_in_tag - 3) = 0;
m_ind_op_c * (m_in_tag - 3) = 0;

// Indirect operation is always a load
m_ind_op_a * m_rw = 0;
m_ind_op_b * m_rw = 0;
m_ind_op_c * m_rw = 0;

//====== MOV Opcode in_tag Constraint =====================================
// The following constraint ensures that the m_in_tag is set to m_tag for
// the load operation pertaining to Ia.
Expand Down
Loading