Skip to content

Commit

Permalink
refactor(avm)!: wire changes
Browse files Browse the repository at this point in the history
  • Loading branch information
fcarreiro committed Oct 4, 2024
1 parent f2ea42c commit 0364b50
Show file tree
Hide file tree
Showing 34 changed files with 711 additions and 1,483 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 0364b50

Please sign in to comment.