Skip to content

Commit

Permalink
refactor(avm)!: remove CMOV opcode (#9030)
Browse files Browse the repository at this point in the history
It's not emitted by Noir, and it needs special casing in the AVM
circuit. We discussed with Alvaro that we'd remove it.
  • Loading branch information
fcarreiro authored Oct 4, 2024
1 parent 4873c7b commit ec9dfdf
Show file tree
Hide file tree
Showing 36 changed files with 711 additions and 1,520 deletions.
2 changes: 0 additions & 2 deletions avm-transpiler/src/opcodes.rs
Original file line number Diff line number Diff line change
Expand Up @@ -51,7 +51,6 @@ pub enum AvmOpcode {
SET_FF,
MOV_8,
MOV_16,
CMOV,
// World state
SLOAD,
SSTORE,
Expand Down Expand Up @@ -144,7 +143,6 @@ impl AvmOpcode {
AvmOpcode::SET_FF => "SET_FF",
AvmOpcode::MOV_8 => "MOV_8",
AvmOpcode::MOV_16 => "MOV_16",
AvmOpcode::CMOV => "CMOV",

// World State
AvmOpcode::SLOAD => "SLOAD", // Public Storage
Expand Down
13 changes: 0 additions & 13 deletions avm-transpiler/src/transpile.rs
Original file line number Diff line number Diff line change
Expand Up @@ -249,19 +249,6 @@ pub fn brillig_to_avm(
destination.to_usize() as u32,
));
}
BrilligOpcode::ConditionalMov { source_a, source_b, condition, destination } => {
avm_instrs.push(AvmInstruction {
opcode: AvmOpcode::CMOV,
indirect: Some(AvmOperand::U8 { value: ALL_DIRECT }),
operands: vec![
AvmOperand::U32 { value: source_a.to_usize() as u32 },
AvmOperand::U32 { value: source_b.to_usize() as u32 },
AvmOperand::U32 { value: condition.to_usize() as u32 },
AvmOperand::U32 { value: destination.to_usize() as u32 },
],
..Default::default()
});
}
BrilligOpcode::Load { destination, source_pointer } => {
avm_instrs.push(generate_mov_instruction(
Some(AvmOperand::U8 { value: ZEROTH_OPERAND_INDIRECT }),
Expand Down
37 changes: 16 additions & 21 deletions barretenberg/cpp/pil/avm/main.pil
Original file line number Diff line number Diff line change
Expand Up @@ -120,7 +120,6 @@ namespace main(256);
//===== MEMORY OPCODES ==========================================================
pol commit sel_op_set;
pol commit sel_op_mov;
pol commit sel_op_cmov;

//===== TABLE SUBOP-TR ========================================================
// Boolean selectors for (sub-)operations. Only one operation is activated at
Expand Down Expand Up @@ -160,7 +159,7 @@ namespace 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)
pol commit id_zero; // Boolean telling whether id is zero (jmp opcode)

//===== MEMORY MODEL ========================================================
// ind_addr_a -> (gets resolved to)
Expand Down Expand Up @@ -285,7 +284,6 @@ namespace main(256);
// Might be removed if derived from opcode based on a lookup of constants
sel_op_set * (1 - sel_op_set) = 0;
sel_op_mov * (1 - sel_op_mov) = 0;
sel_op_cmov * (1 - sel_op_cmov) = 0;

op_err * (1 - op_err) = 0;
tag_err * (1 - tag_err) = 0; // Potential optimization (boolean constraint derivation from equivalence check to mem)?
Expand Down Expand Up @@ -424,7 +422,7 @@ namespace main(256);
pol SEL_ALL_BINARY = sel_op_and + sel_op_or + sel_op_xor;
pol SEL_ALL_GADGET = sel_op_radix_le + sel_op_sha256 + sel_op_poseidon2 + sel_op_keccak + sel_op_pedersen
+ sel_op_ecadd + sel_op_pedersen_commit + sel_op_msm;
pol SEL_ALL_MEMORY = sel_op_cmov + sel_op_mov + sel_op_set;
pol SEL_ALL_MEMORY = sel_op_mov + sel_op_set;
pol OPCODE_SELECTORS = sel_op_fdiv + sel_op_calldata_copy + sel_op_get_contract_instance
+ SEL_ALL_ALU + SEL_ALL_BINARY + SEL_ALL_MEMORY + SEL_ALL_GADGET
+ KERNEL_INPUT_SELECTORS + KERNEL_OUTPUT_SELECTORS + SEL_ALL_LEFTGAS
Expand Down Expand Up @@ -457,35 +455,32 @@ namespace main(256);
//====== MEMORY OPCODES CONSTRAINTS =========================================

// TODO: consolidate with zero division error handling
// TODO: Ensure that operation decompostion will ensure mutual exclusivity of sel_op_cmov and sel_op_jumpi

// When sel_op_cmov or sel_op_jumpi == 1, we need id == 0 <==> id_zero == 0
// When sel_op_jumpi == 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_op_cmov + sel_op_jumpi) * (id * inv - 1 + id_zero) = 0;
#[CMOV_CONDITION_RES_2]
(sel_op_cmov + sel_op_jumpi) * id_zero * (1 - inv) = 0;
#[JMP_CONDITION_RES_1]
sel_op_jumpi * (id * inv - 1 + id_zero) = 0;
#[JMP_CONDITION_RES_2]
sel_op_jumpi * 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_op_mov, sel_op_cmov, and id_zero.
// respective definitions based on sel_op_mov, and id_zero.
pol commit sel_mov_ia_to_ic;
pol commit sel_mov_ib_to_ic;

// 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_ia_to_ic = sel_op_mov + sel_op_cmov * (1 - id_zero);
sel_mov_ib_to_ic = sel_op_cmov * id_zero;
sel_mov_ia_to_ic = sel_op_mov * (1 - id_zero);

#[MOV_SAME_VALUE_A]
sel_mov_ia_to_ic * (ia - ic) = 0; // Ensure that the correct value is moved/copied.
#[MOV_SAME_VALUE_B]
sel_mov_ib_to_ic * (ib - ic) = 0; // Ensure that the correct value is moved/copied.
#[MOV_MAIN_SAME_TAG]
(sel_op_mov + sel_op_cmov) * (r_in_tag - w_in_tag) = 0;
sel_op_mov * (r_in_tag - w_in_tag) = 0;

// Predicate to activate the copy of intermediate registers to ALU table. If tag_err == 1,
// the operation is not copied to the ALU table.
Expand Down Expand Up @@ -580,27 +575,27 @@ namespace main(256);
slice.sel_start {slice.clk, slice.space_id, slice.col_offset, slice.cnt, slice.addr, slice.sel_cd_cpy, slice.sel_return};

#[PERM_MAIN_MEM_A]
sel_mem_op_a {clk, space_id, mem_addr_a, ia, rwa, r_in_tag, w_in_tag, sel_mov_ia_to_ic, sel_op_cmov}
sel_mem_op_a {clk, space_id, mem_addr_a, ia, rwa, r_in_tag, w_in_tag, sel_mov_ia_to_ic}
is
mem.sel_op_a {mem.clk, mem.space_id, mem.addr, mem.val, mem.rw
, mem.r_in_tag, mem.w_in_tag, mem.sel_mov_ia_to_ic, mem.sel_op_cmov};
, mem.r_in_tag, mem.w_in_tag, mem.sel_mov_ia_to_ic};

#[PERM_MAIN_MEM_B]
sel_mem_op_b {clk, space_id, mem_addr_b, ib, rwb, r_in_tag, w_in_tag, sel_mov_ib_to_ic, sel_op_cmov}
sel_mem_op_b {clk, space_id, mem_addr_b, ib, rwb, r_in_tag, w_in_tag, sel_mov_ib_to_ic}
is
mem.sel_op_b {mem.clk, mem.space_id, mem.addr, mem.val, mem.rw
, mem.r_in_tag, mem.w_in_tag, mem.sel_mov_ib_to_ic, mem.sel_op_cmov};
, mem.r_in_tag, mem.w_in_tag, mem.sel_mov_ib_to_ic};

#[PERM_MAIN_MEM_C]
sel_mem_op_c {clk, space_id, mem_addr_c, ic, rwc, r_in_tag, w_in_tag}
is
mem.sel_op_c {mem.clk, mem.space_id, mem.addr, mem.val, mem.rw, mem.r_in_tag, mem.w_in_tag};

#[PERM_MAIN_MEM_D]
sel_mem_op_d {clk, space_id, mem_addr_d, id, rwd, r_in_tag, w_in_tag, sel_op_cmov}
sel_mem_op_d {clk, space_id, mem_addr_d, id, rwd, r_in_tag, w_in_tag}
is
mem.sel_op_d {mem.clk, mem.space_id, mem.addr, mem.val, mem.rw
, mem.r_in_tag, mem.w_in_tag, mem.sel_op_cmov};
, mem.r_in_tag, mem.w_in_tag};

#[PERM_MAIN_MEM_IND_ADDR_A]
sel_resolve_ind_addr_a {clk, space_id, ind_addr_a, mem_addr_a}
Expand Down
23 changes: 11 additions & 12 deletions barretenberg/cpp/pil/avm/mem.pil
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,7 @@ namespace mem(256);
pol commit r_in_tag; // Instruction memory tag ("foreign key" pointing to main.r_in_tag)
pol commit w_in_tag; // Instruction memory tag ("foreign key" pointing to 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.
// trace between tag and r_in_tag. Required for JMPI opcode.

// Indicator of the intermediate register pertaining to the memory operation (foreign key to main.sel_mem_op_XXX)
pol commit sel_op_a;
Expand Down Expand Up @@ -56,11 +56,10 @@ namespace mem(256);
// Selector for calldata_copy/return memory operations triggered from memory slice gadget.
pol commit sel_op_slice;

// Selectors related to MOV/CMOV opcodes (copied from main trace for loading operation on intermediated register ia/ib)
// Selectors related to MOV opcodes (copied from main trace for loading operation on intermediated register ia/ib)
// Boolean constraint is performed in main trace.
pol commit sel_mov_ia_to_ic;
pol commit sel_mov_ib_to_ic;
pol commit sel_op_cmov;

// Error columns
pol commit tag_err; // Boolean (1 if r_in_tag != tag is detected)
Expand Down Expand Up @@ -91,7 +90,7 @@ namespace mem(256);
sel_mem = SEL_DIRECT_MEM_OP_A + SEL_DIRECT_MEM_OP_B + SEL_DIRECT_MEM_OP_C + SEL_DIRECT_MEM_OP_D +
sel_resolve_ind_addr_a + sel_resolve_ind_addr_b + sel_resolve_ind_addr_c + sel_resolve_ind_addr_d
+ sel_op_slice;

// Maximum one memory operation enabled per row
sel_mem * (sel_mem - 1) = 0; // TODO: might be infered by the main trace

Expand Down Expand Up @@ -145,11 +144,11 @@ namespace mem(256);
// Optimization: We removed the term (1 - main.sel_first)
#[MEM_LAST_ACCESS_DELIMITER]
(1 - lastAccess) * (glob_addr' - glob_addr) = 0;

// We need: lastAccess == 1 ==> glob_addr' > glob_addr
// The above implies: glob_addr' == glob_addr ==> lastAccess == 0
// This condition does not apply on the last row.

// In addition, we need glob_addr' == glob_addr ==> tsp' > tsp
// For all rows pertaining to the memory trace (sel_mem == 1) except the last one,
// i.e., when sel_rng_chk == 1, we compute the difference:
Expand All @@ -166,11 +165,11 @@ namespace mem(256);
// This condition does not apply on the last row.
// 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

// Optimization: We removed the term (1 - main.sel_first) and (1 - last)
#[MEM_READ_WRITE_VAL_CONSISTENCY]
(1 - lastAccess) * (1 - rw') * (val' - val) = 0;

// lastAccess == 0 && rw' == 0 ==> tag == tag'
// Optimization: We removed the term (1 - main.sel_first) and (1 - last)
#[MEM_READ_WRITE_TAG_CONSISTENCY]
Expand All @@ -183,9 +182,9 @@ namespace mem(256);
lastAccess * (1 - rw') * val' = 0;

// TODO: Verfiy that skip_check_tag cannot be enabled maliciously by the prover.
// Skip check tag enabled for some MOV/CMOV opcodes and RETURN opcode (sel_op_slice)
// Skip check tag enabled for some MOV opcodes and RETURN opcode (sel_op_slice)
#[SKIP_CHECK_TAG]
skip_check_tag = sel_op_cmov * (sel_op_d + sel_op_a * (1-sel_mov_ia_to_ic) + sel_op_b * (1-sel_mov_ib_to_ic)) + sel_op_slice;
skip_check_tag = sel_op_slice;

// Memory tag consistency check for load operations, i.e., rw == 0.
// We want to prove that r_in_tag == tag <==> tag_err == 0
Expand All @@ -200,7 +199,7 @@ namespace mem(256);
// instead of (r_in_tag - tag)^(-1) as this allows to store zero by default (i.e., when tag_err == 0).
// 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
// Relaxation: This relation is relaxed when skip_check_tag is enabled or for
// Relaxation: This relation is relaxed when skip_check_tag is enabled or for
// uninitialized memory, i.e. tag == 0.
#[MEM_IN_TAG_CONSISTENCY_1]
tag * (1 - skip_check_tag) * (1 - rw) * ((r_in_tag - tag) * (1 - one_min_inv) - tag_err) = 0;
Expand Down Expand Up @@ -251,7 +250,7 @@ namespace mem(256);
sel_op_poseidon_write_c * (r_in_tag - constants.MEM_TAG_FF) = 0; // Only write elements of type FF
sel_op_poseidon_write_d * (r_in_tag - constants.MEM_TAG_FF) = 0; // Only write elements of type FF

//====== MOV/CMOV Opcode Tag Constraint =====================================
//====== MOV Opcode Tag Constraint =====================================
// The following constraint ensures that the r_in_tag is set to tag for
// the load operation pertaining to Ia resp. Ib.
// The permutation check #[PERM_MAIN_MEM_A/B] guarantees that the r_in_tag
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -239,7 +239,6 @@ AvmCircuitBuilder::ProverPolynomials AvmCircuitBuilder::compute_polynomials() co
polys.main_sel_op_calldata_copy.set_if_valid_index(i, rows[i].main_sel_op_calldata_copy);
polys.main_sel_op_cast.set_if_valid_index(i, rows[i].main_sel_op_cast);
polys.main_sel_op_chain_id.set_if_valid_index(i, rows[i].main_sel_op_chain_id);
polys.main_sel_op_cmov.set_if_valid_index(i, rows[i].main_sel_op_cmov);
polys.main_sel_op_dagasleft.set_if_valid_index(i, rows[i].main_sel_op_dagasleft);
polys.main_sel_op_div.set_if_valid_index(i, rows[i].main_sel_op_div);
polys.main_sel_op_ecadd.set_if_valid_index(i, rows[i].main_sel_op_ecadd);
Expand Down Expand Up @@ -323,7 +322,6 @@ AvmCircuitBuilder::ProverPolynomials AvmCircuitBuilder::compute_polynomials() co
polys.mem_sel_op_a.set_if_valid_index(i, rows[i].mem_sel_op_a);
polys.mem_sel_op_b.set_if_valid_index(i, rows[i].mem_sel_op_b);
polys.mem_sel_op_c.set_if_valid_index(i, rows[i].mem_sel_op_c);
polys.mem_sel_op_cmov.set_if_valid_index(i, rows[i].mem_sel_op_cmov);
polys.mem_sel_op_d.set_if_valid_index(i, rows[i].mem_sel_op_d);
polys.mem_sel_op_poseidon_read_a.set_if_valid_index(i, rows[i].mem_sel_op_poseidon_read_a);
polys.mem_sel_op_poseidon_read_b.set_if_valid_index(i, rows[i].mem_sel_op_poseidon_read_b);
Expand Down
Loading

0 comments on commit ec9dfdf

Please sign in to comment.