Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

feat(avm): Mov opcode with direct memory #5204

Merged
merged 4 commits into from
Mar 15, 2024
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
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
Loading