Skip to content

Commit

Permalink
feat(avm): Mov opcode with direct memory (#5204)
Browse files Browse the repository at this point in the history
Resolves #5159
  • Loading branch information
jeanmon authored Mar 15, 2024
1 parent 2e63479 commit 08f9038
Show file tree
Hide file tree
Showing 20 changed files with 844 additions and 215 deletions.
18 changes: 15 additions & 3 deletions barretenberg/cpp/pil/avm/avm_main.pil
Original file line number Diff line number Diff line change
Expand Up @@ -21,6 +21,9 @@ namespace avm_main(256);

// Halt program execution
pol commit sel_halt;

//===== MEMORY OPCODES ==========================================================
pol commit sel_mov;

//===== TABLE SUBOP-TR ========================================================
// Boolean selectors for (sub-)operations. Only one operation is activated at
Expand Down Expand Up @@ -94,6 +97,9 @@ namespace avm_main(256);
sel_jump * (1 - sel_jump) = 0;
sel_halt * (1 - sel_halt) = 0;

// Might be removed if derived from opcode based on a lookup of constants
sel_mov * ( 1 - sel_mov) = 0;

op_err * (1 - op_err) = 0;
tag_err * (1 - tag_err) = 0; // Potential optimization (boolean constraint derivation from equivalence check to avm_mem)?

Expand Down Expand Up @@ -188,11 +194,17 @@ namespace avm_main(256);

// TODO: we want to set an initial number for the reserved memory of the jump pointer

// Inter-table Constraints
//====== MEMORY OPCODES CONSTRAINTS =========================================
#[MOV_SAME_VALUE]
sel_mov * (ia - ic) = 0; // Ensure that the correct value is moved/copied.

//====== Inter-table Constraints ============================================
#[INCL_MAIN_TAG_ERR]
avm_mem.m_tag_err {avm_mem.m_clk} in tag_err {clk};

#[INCL_MEM_TAG_ERR]
tag_err {clk} in avm_mem.m_tag_err {avm_mem.m_clk};

// Predicate to activate the copy of intermediate registers to ALU table. If tag_err == 1,
// the operation is not copied to the ALU table.
// TODO: when division is moved to the alu, we will need to add the selector in the list below:
Expand All @@ -208,9 +220,9 @@ namespace avm_main(256);
avm_alu.alu_op_not, avm_alu.alu_in_tag};

#[PERM_MAIN_MEM_A]
mem_op_a {clk, mem_idx_a, ia, rwa, in_tag}
mem_op_a {clk, mem_idx_a, ia, rwa, in_tag, sel_mov}
is
avm_mem.m_op_a {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_a {avm_mem.m_clk, avm_mem.m_addr, avm_mem.m_val, avm_mem.m_rw, avm_mem.m_in_tag, avm_mem.m_sel_mov};

#[PERM_MAIN_MEM_B]
mem_op_b {clk, mem_idx_b, ib, rwb, in_tag}
Expand Down
17 changes: 16 additions & 1 deletion barretenberg/cpp/pil/avm/avm_mem.pil
Original file line number Diff line number Diff line change
Expand Up @@ -20,6 +20,10 @@ namespace avm_mem(256);
pol commit m_op_b;
pol commit m_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;

// Error columns
pol commit m_tag_err; // Boolean (1 if m_in_tag != m_tag is detected)

Expand Down Expand Up @@ -111,4 +115,15 @@ namespace avm_mem(256);

// 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
// m_tag_err == 0 ==> m_one_min_inv == 0 by second relation. First relation ==> m_in_tag - m_tag == 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.
// The permutation check #[PERM_MAIN_MEM_A] guarantees that the m_in_tag
// value load operation for Ia is copied back in the main trace. Then,
// #[PERM_MAIN_MEM_C] copies back m_in_tag for store operation from Ic.
// Finally, the following constraint guarantees that m_tag is correct for
// the output.
#[MOV_SAME_TAG]
m_sel_mov * m_tag_err = 0; // Equivalent to m_sel_mov * (m_in_tag - m_tag) = 0
Loading

0 comments on commit 08f9038

Please sign in to comment.