Skip to content

Commit

Permalink
feat(avm): CMOV opcode (#5575)
Browse files Browse the repository at this point in the history 
Resolves #5557
  • Loading branch information
@jeanmon
jeanmon authored Apr 11, 2024
1 parent 0b6b6f6 commit 19dbe46
Show file tree
Hide file tree
Showing 22 changed files with 1,563 additions and 235 deletions.
73 changes: 62 additions & 11 deletions barretenberg/cpp/pil/avm/avm_main.pil
View file
Original file line number Diff line number Diff line change
Expand Up @@ -30,6 +30,7 @@ namespace avm_main(256);

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

//===== TABLE SUBOP-TR ========================================================
// Boolean selectors for (sub-)operations. Only one operation is activated at
Expand Down Expand Up @@ -75,40 +76,45 @@ namespace avm_main(256);
// A helper witness being the inverse of some value
// to show a non-zero equality
pol commit inv;
pol commit id_zero; // Boolean telling whether id is zero (cmov opcode)

// Intermediate register values
pol commit ia;
pol commit ib;
pol commit ic;
pol commit id;

// Memory operation selector per intermediate register
pol commit mem_op_a;
pol commit mem_op_b;
pol commit mem_op_c;
pol commit mem_op_d;

// Read-write flag per intermediate register: Read = 0, Write = 1
pol commit rwa;
pol commit rwb;
pol commit rwc;
pol commit rwd;

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

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

pol commit ind_op_d;

// 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.
pol commit mem_idx_a;
pol commit mem_idx_b;
pol commit mem_idx_c;

pol commit mem_idx_d;

// 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.
Expand All @@ -135,27 +141,32 @@ namespace avm_main(256);

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

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

// 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;
mem_op_d * (1 - mem_op_d) = 0;

rwa * (1 - rwa) = 0;
rwb * (1 - rwb) = 0;
rwc * (1 - rwc) = 0;
rwd * (1 - rwd) = 0;

// 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;
ind_op_d * (1 - ind_op_d) = 0;

// TODO - Constraints:
// - mem_idx_a, mem_idx_b, mem_idx_c to u32 type
// - ind_a, ind_b, ind_c to u32 type
// - mem_idx_a, mem_idx_b, mem_idx_c, mem_idx_d to u32 type
// - ind_a, ind_b, ind_c, ind_d to u32 type
// - 0 <= r_in_tag, w_in_tag <= 6 // Maybe not needed as probably derived by the operation decomposition.

//====== COMPARATOR OPCODES CONSTRAINTS =====================================
Expand Down Expand Up @@ -245,10 +256,36 @@ namespace avm_main(256);
// TODO: we want to set an initial number for the reserved memory of the jump pointer

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

// TODO: consolidate with zero division error handling

// When sel_cmov == 1, we need id == 0 <==> id_zero == 0
// This can be achieved with the 2 following relations.
// inv is an extra witness to show that we can invert id, i.e., inv = id^(-1)
// If id == 0, we have to set inv = 1 to satisfy the second relation,
// because id_zero == 1 from the first relation.
#[CMOV_CONDITION_RES_1]
sel_cmov * (id * inv - 1 + id_zero) = 0;
#[CMOV_CONDITION_RES_2]
sel_cmov * id_zero * (1 - inv) = 0;

// Boolean selectors telling whether we move ia to ic or ib to ic.
// Boolean constraints and mutual exclusivity are derived from their
// respective definitions based on sel_mov, sel_cmov, and id_zero.
pol commit sel_mov_a;
pol commit sel_mov_b;

// For MOV, we copy ia to ic.
// For CMOV, we copy ia to ic if id is NOT zero, otherwise we copy ib to ic.
sel_mov_a = sel_mov + sel_cmov * (1 - id_zero);
sel_mov_b = sel_cmov * id_zero;

#[MOV_SAME_VALUE_A]
sel_mov_a * (ia - ic) = 0; // Ensure that the correct value is moved/copied.
#[MOV_SAME_VALUE_B]
sel_mov_b * (ib - ic) = 0; // Ensure that the correct value is moved/copied.
#[MOV_MAIN_SAME_TAG]
sel_mov * (r_in_tag - w_in_tag) = 0;
(sel_mov + sel_cmov) * (r_in_tag - w_in_tag) = 0;

//====== Inter-table Constraints ============================================
#[INCL_MAIN_TAG_ERR]
Expand Down Expand Up @@ -288,20 +325,31 @@ namespace avm_main(256);
avm_binary.start {avm_binary.clk, avm_binary.acc_ia, avm_binary.acc_ib, avm_binary.acc_ic, avm_binary.op_id, avm_binary.in_tag};

#[PERM_MAIN_MEM_A]
mem_op_a {clk, mem_idx_a, ia, rwa, r_in_tag, w_in_tag, sel_mov}
mem_op_a {clk, mem_idx_a, ia, rwa
, r_in_tag, w_in_tag, sel_mov_a, sel_cmov}
is
avm_mem.op_a {avm_mem.clk, avm_mem.addr, avm_mem.val, avm_mem.rw, avm_mem.r_in_tag, avm_mem.w_in_tag, avm_mem.sel_mov};
avm_mem.op_a {avm_mem.clk, avm_mem.addr, avm_mem.val, avm_mem.rw
, avm_mem.r_in_tag, avm_mem.w_in_tag, avm_mem.sel_mov_a, avm_mem.sel_cmov};

#[PERM_MAIN_MEM_B]
mem_op_b {clk, mem_idx_b, ib, rwb, r_in_tag, w_in_tag}
mem_op_b {clk, mem_idx_b, ib, rwb
, r_in_tag, w_in_tag, sel_mov_b, sel_cmov}
is
avm_mem.op_b {avm_mem.clk, avm_mem.addr, avm_mem.val, avm_mem.rw, avm_mem.r_in_tag, avm_mem.w_in_tag};
avm_mem.op_b {avm_mem.clk, avm_mem.addr, avm_mem.val, avm_mem.rw
, avm_mem.r_in_tag, avm_mem.w_in_tag, avm_mem.sel_mov_b, avm_mem.sel_cmov};

#[PERM_MAIN_MEM_C]
mem_op_c {clk, mem_idx_c, ic, rwc, r_in_tag, w_in_tag}
is
avm_mem.op_c {avm_mem.clk, avm_mem.addr, avm_mem.val, avm_mem.rw, avm_mem.r_in_tag, avm_mem.w_in_tag};

#[PERM_MAIN_MEM_D]
mem_op_d {clk, mem_idx_d, id, rwd
, r_in_tag, w_in_tag, sel_cmov}
is
avm_mem.op_d {avm_mem.clk, avm_mem.addr, avm_mem.val, avm_mem.rw
, avm_mem.r_in_tag, avm_mem.w_in_tag, avm_mem.sel_cmov};

#[PERM_MAIN_MEM_IND_A]
ind_op_a {clk, ind_a, mem_idx_a} is avm_mem.ind_op_a {avm_mem.clk, avm_mem.addr, avm_mem.val};

Expand All @@ -311,6 +359,9 @@ namespace avm_main(256);
#[PERM_MAIN_MEM_IND_C]
ind_op_c {clk, ind_c, mem_idx_c} is avm_mem.ind_op_c {avm_mem.clk, avm_mem.addr, avm_mem.val};

#[PERM_MAIN_MEM_IND_D]
ind_op_d {clk, ind_d, mem_idx_d} is avm_mem.ind_op_d {avm_mem.clk, avm_mem.addr, avm_mem.val};

//====== Inter-table Constraints (Range Checks) ============================================
// TODO: Investigate optimising these range checks. Handling non-FF elements should require less range checks.
#[LOOKUP_U8_0]
Expand Down
39 changes: 28 additions & 11 deletions barretenberg/cpp/pil/avm/avm_mem.pil
View file
Original file line number Diff line number Diff line change
Expand Up @@ -15,20 +15,26 @@ namespace avm_mem(256);

pol commit r_in_tag; // Instruction memory tag ("foreign key" pointing to avm_main.r_in_tag)
pol commit w_in_tag; // Instruction memory tag ("foreign key" pointing to avm_main.w_in_tag)
pol commit skip_check_tag; // A boolean value which relaxes the consistency check in memory
// trace between tag and r_in_tag. Required for CMOV opcode.

// Indicator of the intermediate register pertaining to the memory operation (foreign key to avm_main.mem_op_XXX)
pol commit op_a;
pol commit op_b;
pol commit op_c;
pol commit op_d;

// Indicator of the indirect register pertaining to the memory operation (foreign key to avm_main.ind_op_XXX)
pol commit ind_op_a;
pol commit ind_op_b;
pol commit ind_op_c;
pol commit ind_op_d;

// Selector for MOV opcode (copied from main trace for loading operation on intermediated register ia)
// Selectors related to MOV/CMOV opcodes (copied from main trace for loading operation on intermediated register ia/ib)
// Boolean constraint is performed in main trace.
pol commit sel_mov;
pol commit sel_mov_a;
pol commit sel_mov_b;
pol commit sel_cmov;

// Error columns
pol commit tag_err; // Boolean (1 if r_in_tag != tag is detected)
Expand All @@ -44,20 +50,22 @@ namespace avm_mem(256);
op_a * (1 - op_a) = 0;
op_b * (1 - op_b) = 0;
op_c * (1 - op_c) = 0;
op_d * (1 - op_d) = 0;
ind_op_a * (1 - ind_op_a) = 0;
ind_op_b * (1 - ind_op_b) = 0;
ind_op_c * (1 - ind_op_c) = 0;
ind_op_d * (1 - ind_op_d) = 0;

// TODO: addr is u32 and 0 <= tag <= 6
// (r_in_tag, w_in_tag will be constrained through inclusion check to main trace)

// Maximum one memory operation enabled per row
pol MEM_SEL = op_a + op_b + op_c + ind_op_a + ind_op_b + ind_op_c;
pol MEM_SEL = op_a + op_b + op_c + op_d + ind_op_a + ind_op_b + ind_op_c + ind_op_d;
MEM_SEL * (MEM_SEL - 1) = 0;

// sub_clk derivation
pol IND_OP = ind_op_a + ind_op_b + ind_op_c;
sub_clk = MEM_SEL * (ind_op_b + op_b + 2 * (ind_op_c + op_c) + 3 * (1 - IND_OP + rw));
pol IND_OP = ind_op_a + ind_op_b + ind_op_c + ind_op_d;
sub_clk = MEM_SEL * (ind_op_b + op_b + 2 * (ind_op_c + op_c) + 3 * (ind_op_d + op_d) + 4 * (1 - IND_OP + rw));
// We need the MEM_SEL factor as the right factor is not zero when all columns are zero.

// Remark: lastAccess == 1 on first row and therefore any relation with the
Expand Down Expand Up @@ -106,6 +114,10 @@ namespace avm_mem(256);
#[MEM_ZERO_INIT]
lastAccess * (1 - rw') * val' = 0;

// Skip check tag
#[SKIP_CHECK_TAG]
skip_check_tag = sel_cmov * (op_d + op_a * (1-sel_mov_a) + op_b * (1-sel_mov_b));

// Memory tag consistency check for load operations, i.e., rw == 0.
// We want to prove that r_in_tag == tag <==> tag_err == 0
// We want to show that we can invert (r_in_tag - tag) when tag_err == 1,
Expand All @@ -120,10 +132,13 @@ namespace avm_mem(256);
// The new column one_min_inv is set to 1 - (r_in_tag - tag)^(-1) when tag_err == 1
// but must be set to 0 when tags are matching and tag_err = 0
#[MEM_IN_TAG_CONSISTENCY_1]
(1 - rw) * ((r_in_tag - tag) * (1 - one_min_inv) - tag_err) = 0;
(1 - skip_check_tag) * (1 - rw) * ((r_in_tag - tag) * (1 - one_min_inv) - tag_err) = 0;
#[MEM_IN_TAG_CONSISTENCY_2]
(1 - tag_err) * one_min_inv = 0;

#[NO_TAG_ERR_WRITE_OR_SKIP]
(skip_check_tag + rw) * tag_err = 0;

// Correctness of two above checks MEM_IN_TAG_CONSISTENCY_1/2 (assuming rw == 0):
// r_in_tag == tag ==> tag_err == 0 (first relation)
// tag_err == 0 ==> one_min_inv == 0 by second relation. First relation ==> r_in_tag - tag == 0
Expand All @@ -140,18 +155,20 @@ namespace avm_mem(256);
ind_op_a * (r_in_tag - 3) = 0;
ind_op_b * (r_in_tag - 3) = 0;
ind_op_c * (r_in_tag - 3) = 0;
ind_op_d * (r_in_tag - 3) = 0;

// Indirect operation is always a load
ind_op_a * rw = 0;
ind_op_b * rw = 0;
ind_op_c * rw = 0;
ind_op_d * rw = 0;

//====== MOV Opcode Tag Constraint =====================================
//====== MOV/CMOV Opcode Tag Constraint =====================================
// The following constraint ensures that the r_in_tag is set to tag for
// the load operation pertaining to Ia.
// The permutation check #[PERM_MAIN_MEM_A] guarantees that the r_in_tag
// value load operation for Ia is copied back in the main trace.
// the load operation pertaining to Ia resp. Ib.
// The permutation check #[PERM_MAIN_MEM_A/B] guarantees that the r_in_tag
// value load operation for Ia/Ib is copied back in the main trace.
// Constraint #[MOV_MAIN_SAME_TAG] copies r_in_tag to w_in_tag in the main
// trace. Then, #[PERM_MAIN_MEM_C] copies w_in_tag for store operation from Ic.
#[MOV_SAME_TAG]
sel_mov * tag_err = 0; // Equivalent to sel_mov * (r_in_tag - tag) = 0
(sel_mov_a + sel_mov_b) * tag_err = 0; // Equivalent to (sel_mov_a + sel_mov_b) * (r_in_tag - tag) = 0
Loading

0 comments on commit 19dbe46

Please sign in to comment.