Skip to content

Commit

Permalink
chore(avm): renamings and comments (#7128)
Browse files Browse the repository at this point in the history
Painful.

Also cleaned up the generated files. Some hadn't been deleted when the
renaming took place.
  • Loading branch information
fcarreiro authored Jun 20, 2024
1 parent 0770011 commit ed2f98e
Show file tree
Hide file tree
Showing 118 changed files with 3,611 additions and 3,954 deletions.
90 changes: 44 additions & 46 deletions barretenberg/cpp/pil/avm/alu.pil
Original file line number Diff line number Diff line change
@@ -1,5 +1,3 @@
include "main.pil";

namespace alu(256);

// ========= Table ALU-TR =================================================
Expand All @@ -19,14 +17,14 @@ namespace alu(256);
pol commit op_eq;
pol commit op_cast;
pol commit op_cast_prev; // Predicate on whether op_cast is enabled at previous row
pol commit alu_sel; // Predicate to activate the copy of intermediate registers to ALU table.
pol commit sel_alu; // Predicate to activate the copy of intermediate registers to ALU table.
pol commit op_lt;
pol commit op_lte;
pol commit cmp_sel; // Predicate if LT or LTE is set
pol commit rng_chk_sel; // Predicate representing a range check row.
pol commit sel_cmp; // Predicate if LT or LTE is set
pol commit sel_rng_chk; // Predicate representing a range check row.
pol commit op_shl;
pol commit op_shr;
pol commit shift_sel; // Predicate if SHR or SHR is set
pol commit sel_shift_which; // Predicate if SHR or SHR is set

// Instruction tag (1: u8, 2: u16, 3: u32, 4: u64, 5: u128, 6: field) copied from Main table
pol commit in_tag;
Expand Down Expand Up @@ -64,9 +62,9 @@ namespace alu(256);
pol commit cf;

// Compute predicate telling whether there is a row entry in the ALU table.
alu_sel = op_add + op_sub + op_mul + op_not + op_eq + op_cast + op_lt + op_lte + op_shr + op_shl + op_div;
cmp_sel = op_lt + op_lte;
shift_sel = op_shl + op_shr;
sel_alu = op_add + op_sub + op_mul + op_not + op_eq + op_cast + op_lt + op_lte + op_shr + op_shl + op_div;
sel_cmp = op_lt + op_lte;
sel_shift_which = op_shl + op_shr;

// ========= Type Constraints =============================================
// TODO: Range constraints
Expand All @@ -86,7 +84,7 @@ namespace alu(256);
u128_tag * (1 - u128_tag) = 0;

// Mutual exclusion of the flattened instruction tag.
alu_sel * (ff_tag + u8_tag + u16_tag + u32_tag + u64_tag + u128_tag - 1) = 0;
sel_alu * (ff_tag + u8_tag + u16_tag + u32_tag + u64_tag + u128_tag - 1) = 0;

// Correct flattening of the instruction tag.
in_tag = u8_tag + 2 * u16_tag + 3 * u32_tag + 4 * u64_tag + 5 * u128_tag + 6 * ff_tag;
Expand Down Expand Up @@ -227,9 +225,9 @@ namespace alu(256);
// TODO decide if it is done here or in another trace

// Do not allow ff_tag to be set if we are doing bitwise
pol BITWISE_SEL = op_not; // Add more bitwise operations
pol SEL_BITWISE = op_not; // Add more bitwise operations
#[ALU_FF_NOT_XOR]
BITWISE_SEL * ff_tag = 0;
SEL_BITWISE * ff_tag = 0;

// The value 2^k - 1
pol UINT_MAX = u8_tag * 2**8 +
Expand Down Expand Up @@ -264,9 +262,9 @@ namespace alu(256);
// Need an additional helper that holds the inverse of the difference;
pol commit op_eq_diff_inv;

// If EQ or CMP_SEL selector is set, ic needs to be boolean
// If EQ or sel_cmp selector is set, ic needs to be boolean
#[ALU_RES_IS_BOOL]
(cmp_sel + op_eq) * (ic * (1 - ic)) = 0;
(sel_cmp + op_eq) * (ic * (1 - ic)) = 0;

#[ALU_OP_EQ]
op_eq * (DIFF * (ic * (1 - op_eq_diff_inv) + op_eq_diff_inv) - 1 + ic) = 0;
Expand Down Expand Up @@ -296,13 +294,13 @@ namespace alu(256);
pol commit a_hi;
// Check INPUT_IA is well formed from its lo and hi limbs
#[INPUT_DECOMP_1]
INPUT_IA = (a_lo + 2 ** 128 * a_hi) * (cmp_sel + op_cast);
INPUT_IA = (a_lo + 2 ** 128 * a_hi) * (sel_cmp + op_cast);

pol commit b_lo;
pol commit b_hi;
// Check INPUT_IB is well formed from its lo and hi limbs
#[INPUT_DECOMP_2]
INPUT_IB = (b_lo + 2 ** 128 * b_hi) * cmp_sel;
INPUT_IB = (b_lo + 2 ** 128 * b_hi) * sel_cmp;

pol commit p_sub_a_lo; // p_lo - a_lo
pol commit p_sub_a_hi; // p_hi - a_hi
Expand All @@ -317,9 +315,9 @@ namespace alu(256);
// First condition is if borrow = 0, second condition is if borrow = 1
// This underflow check is done by the 128-bit check that is performed on each of these lo and hi limbs.
#[SUB_LO_1]
(p_sub_a_lo - (53438638232309528389504892708671455232 - a_lo + p_a_borrow * 2 ** 128)) * (cmp_sel + op_cast + op_div_std) = 0;
(p_sub_a_lo - (53438638232309528389504892708671455232 - a_lo + p_a_borrow * 2 ** 128)) * (sel_cmp + op_cast + op_div_std) = 0;
#[SUB_HI_1]
(p_sub_a_hi - (64323764613183177041862057485226039389 - a_hi - p_a_borrow)) * (cmp_sel + op_cast + op_div_std) = 0;
(p_sub_a_hi - (64323764613183177041862057485226039389 - a_hi - p_a_borrow)) * (sel_cmp + op_cast + op_div_std) = 0;

pol commit p_sub_b_lo;
pol commit p_sub_b_hi;
Expand All @@ -330,9 +328,9 @@ namespace alu(256);
// This is achieved by checking (p_lo > b_lo && p_hi >= bhi) || (p_lo <= b_lo && p_hi > b_hi)
// First condition is if borrow = 0, second condition is if borrow = 1;
#[SUB_LO_2]
(p_sub_b_lo - (53438638232309528389504892708671455232 - b_lo + p_b_borrow * 2 ** 128)) * cmp_sel = 0;
(p_sub_b_lo - (53438638232309528389504892708671455232 - b_lo + p_b_borrow * 2 ** 128)) * sel_cmp = 0;
#[SUB_HI_2]
(p_sub_b_hi - (64323764613183177041862057485226039389 - b_hi - p_b_borrow)) * cmp_sel = 0;
(p_sub_b_hi - (64323764613183177041862057485226039389 - b_hi - p_b_borrow)) * sel_cmp = 0;

// Calculate the combined relation: (a - b - 1) * q + (b -a ) * (1-q)
// Check that (a > b) by checking (a_lo > b_lo && a_hi >= bhi) || (alo <= b_lo && a_hi > b_hi)
Expand Down Expand Up @@ -410,9 +408,9 @@ namespace alu(256);
pol commit res_lo;
pol commit res_hi;
#[RES_LO]
(res_lo - (A_SUB_B_LO * IS_GT + B_SUB_A_LO * (1 - IS_GT))) * cmp_sel = 0;
(res_lo - (A_SUB_B_LO * IS_GT + B_SUB_A_LO * (1 - IS_GT))) * sel_cmp = 0;
#[RES_HI]
(res_hi - (A_SUB_B_HI * IS_GT + B_SUB_A_HI * (1 - IS_GT))) * cmp_sel = 0;
(res_hi - (A_SUB_B_HI * IS_GT + B_SUB_A_HI * (1 - IS_GT))) * sel_cmp = 0;

// ========= RANGE OPERATIONS ===============================

Expand All @@ -426,25 +424,25 @@ namespace alu(256);
// if this row is a comparison operation, the next range_check_remaining value is set to 4
// it is not set to 5 since we do 1 as part of the comparison.
#[CMP_CTR_REL_2]
(cmp_rng_ctr' - 4) * cmp_sel = 0;
(cmp_rng_ctr' - 4) * sel_cmp = 0;

rng_chk_sel * (1 - rng_chk_sel) = 0;
// If we have remaining range checks, we cannot have cmp_sel set. This prevents malicious truncating of the range
sel_rng_chk * (1 - sel_rng_chk) = 0;
// If we have remaining range checks, we cannot have sel_cmp set. This prevents malicious truncating of the range
// checks by adding a new LT/LTE operation before all the range checks from the previous computation are complete.
rng_chk_sel * cmp_sel = 0;
sel_rng_chk * sel_cmp = 0;

// rng_chk_sel = 1 when cmp_rng_ctr != 0 and rng_chk_sel = 0 when cmp_rng_ctr = 0;
// sel_rng_chk = 1 when cmp_rng_ctr != 0 and sel_rng_chk = 0 when cmp_rng_ctr = 0;
#[CTR_NON_ZERO_REL]
cmp_rng_ctr * ((1 - rng_chk_sel) * (1 - op_eq_diff_inv) + op_eq_diff_inv) - rng_chk_sel = 0;
cmp_rng_ctr * ((1 - sel_rng_chk) * (1 - op_eq_diff_inv) + op_eq_diff_inv) - sel_rng_chk = 0;

// We perform a range check if we have some range checks remaining or we are performing a comparison op
pol RNG_CHK_OP = rng_chk_sel + cmp_sel + op_cast + op_cast_prev + shift_lt_bit_len + op_div;
pol RNG_CHK_OP = sel_rng_chk + sel_cmp + op_cast + op_cast_prev + shift_lt_bit_len + op_div;

pol commit rng_chk_lookup_selector;
pol commit sel_rng_chk_lookup;
// TODO: Possible optimisation here if we swap the op_shl and op_shr with shift_lt_bit_len.
// Shift_lt_bit_len is a more restrictive form therefore we can avoid performing redundant range checks when we know the result == 0.
#[RNG_CHK_LOOKUP_SELECTOR]
rng_chk_lookup_selector' = cmp_sel' + rng_chk_sel' + op_add' + op_sub' + op_mul' + op_mul * u128_tag + op_cast' + op_cast_prev' + op_shl' + op_shr' + op_div';
sel_rng_chk_lookup' = sel_cmp' + sel_rng_chk' + op_add' + op_sub' + op_mul' + op_mul * u128_tag + op_cast' + op_cast_prev' + op_shl' + op_shr' + op_div';

// Perform 128-bit range check on lo part
#[LOWER_CMP_RNG_CHK]
Expand All @@ -463,17 +461,17 @@ namespace alu(256);
// Briefly: given a > b and p > a and p > a - b - 1, it is sufficient confirm that p > b without a range check
// To accomplish this we would likely change the order of the range_check so we can skip p_sub_b
#[SHIFT_RELS_0]
(a_lo' - b_lo) * rng_chk_sel' = 0;
(a_hi' - b_hi) * rng_chk_sel' = 0;
(a_lo' - b_lo) * sel_rng_chk' = 0;
(a_hi' - b_hi) * sel_rng_chk' = 0;
#[SHIFT_RELS_1]
(b_lo' - p_sub_a_lo) * rng_chk_sel' = 0;
(b_hi' - p_sub_a_hi) * rng_chk_sel' = 0;
(b_lo' - p_sub_a_lo) * sel_rng_chk' = 0;
(b_hi' - p_sub_a_hi) * sel_rng_chk' = 0;
#[SHIFT_RELS_2]
(p_sub_a_lo' - p_sub_b_lo) * rng_chk_sel'= 0;
(p_sub_a_hi' - p_sub_b_hi) * rng_chk_sel'= 0;
(p_sub_a_lo' - p_sub_b_lo) * sel_rng_chk'= 0;
(p_sub_a_hi' - p_sub_b_hi) * sel_rng_chk'= 0;
#[SHIFT_RELS_3]
(p_sub_b_lo' - res_lo) * rng_chk_sel'= 0;
(p_sub_b_hi' - res_hi) * rng_chk_sel'= 0;
(p_sub_b_lo' - res_lo) * sel_rng_chk'= 0;
(p_sub_b_hi' - res_hi) * sel_rng_chk'= 0;

// ========= CAST Operation Constraints ===============================
// We handle the input ia independently of its tag, i.e., we suppose it can take
Expand Down Expand Up @@ -514,7 +512,7 @@ namespace alu(256);
// 128-bit multiplication and CAST need two rows in ALU trace. We need to ensure
// that another ALU operation does not start in the second row.
#[TWO_LINE_OP_NO_OVERLAP]
(op_mul * u128_tag + op_cast) * alu_sel' = 0;
(op_mul * u128_tag + op_cast) * sel_alu' = 0;

// ========= SHIFT LEFT/RIGHT OPERATIONS ===============================
// Given (1) an input b, within the range [0, 2**128-1],
Expand Down Expand Up @@ -600,7 +598,7 @@ namespace alu(256);
// There is no chance of an underflow involving ib to result in a t_sub_b_bits < 2**8 ib is range checked to be < 2**8
// The range checking of t_sub_b_bits in the range [0, 2**8) is done by the lookup for 2**t_sub_s_bits
#[SHIFT_LT_BIT_LEN]
t_sub_s_bits = shift_sel * (shift_lt_bit_len * (MAX_BITS - ib) + (1 - shift_lt_bit_len) * (ib - MAX_BITS));
t_sub_s_bits = sel_shift_which * (shift_lt_bit_len * (MAX_BITS - ib) + (1 - shift_lt_bit_len) * (ib - MAX_BITS));

// ========= SHIFT RIGHT OPERATIONS ===============================
// a_hi * 2**s + a_lo = a
Expand Down Expand Up @@ -699,7 +697,7 @@ namespace alu(256);
(cmp_rng_ctr' - 2) * op_div_std = 0;

// If we have more range checks left we cannot do more divisions operations that might truncate the steps
rng_chk_sel * op_div_std = 0;
sel_rng_chk * op_div_std = 0;

// Check PRODUCT = ia - remainder
#[DIVISION_RELATION]
Expand All @@ -710,10 +708,10 @@ namespace alu(256);
// TODO: We need extra slice registers because we are performing an additional 64-bit range check in the same row, look into re-using old columns or refactoring
// range checks to be more modular.
// boolean to account for the division-specific 64-bit range checks.
pol commit div_rng_chk_selector;
div_rng_chk_selector * (1 - div_rng_chk_selector) = 0;
// div_rng_chk_selector && div_rng_chk_selector' = 1 if op_div_std = 1
div_rng_chk_selector * div_rng_chk_selector' = op_div_std;
pol commit sel_div_rng_chk;
sel_div_rng_chk * (1 - sel_div_rng_chk) = 0;
// sel_div_rng_chk && sel_div_rng_chk' = 1 if op_div_std = 1
sel_div_rng_chk * sel_div_rng_chk' = op_div_std;

pol commit div_u16_r0;
pol commit div_u16_r1;
Expand Down
26 changes: 13 additions & 13 deletions barretenberg/cpp/pil/avm/binary.pil
Original file line number Diff line number Diff line change
Expand Up @@ -7,8 +7,8 @@ namespace binary(256);
pol commit clk;

// Selector for Binary Operation
pol commit bin_sel;
bin_sel * (1 - bin_sel) = 0;
pol commit sel_bin;
sel_bin * (1 - sel_bin) = 0;

// Byte recomposition column, the value in these columns are part of the equivalence
// check to main wherever Start is set to 1.
Expand Down Expand Up @@ -46,31 +46,31 @@ namespace binary(256);
#[MEM_TAG_REL]
(mem_tag_ctr' - mem_tag_ctr + 1) * mem_tag_ctr = 0;

// Bin_sel is a boolean that is set to 1 if mem_tag_ctr != 0.
// sel_bin is a boolean that is set to 1 if mem_tag_ctr != 0.
// This is checked by two relation conditions and utilising mem_tag_ctr_inv
pol commit mem_tag_ctr_inv;

// bin_sel is set to 1 when mem_tag_ctr != 0, and 0 otherwise.
// we constrain it such that bin_sel = mem_tag_ctr * mem_tag_ctr_inv unless mem_tag_ctr = 0 the bin_sel = 0
// sel_bin is set to 1 when mem_tag_ctr != 0, and 0 otherwise.
// we constrain it such that sel_bin = mem_tag_ctr * mem_tag_ctr_inv unless mem_tag_ctr = 0 the sel_bin = 0
// In here we use the consolidated equality relation because it doesnt require us to enforce
// this additional relation: mem_tag_ctr_inv = 1 when mem_tag_ctr = 0. (allows default zero value in trace)
#[BIN_SEL_CTR_REL]
mem_tag_ctr * ((1 - bin_sel) * (1 - mem_tag_ctr_inv) + mem_tag_ctr_inv) - bin_sel = 0;
#[SEL_BIN_CTR_REL]
mem_tag_ctr * ((1 - sel_bin) * (1 - mem_tag_ctr_inv) + mem_tag_ctr_inv) - sel_bin = 0;

// Forces accumulator to start at zero when mem_tag_ctr == 0
(1 - bin_sel) * acc_ia = 0;
(1 - bin_sel) * acc_ib = 0;
(1 - bin_sel) * acc_ic = 0;
(1 - sel_bin) * acc_ia = 0;
(1 - sel_bin) * acc_ib = 0;
(1 - sel_bin) * acc_ic = 0;

#[LOOKUP_BYTE_LENGTHS]
start {in_tag, mem_tag_ctr}
in
byte_lookup.bin_sel {byte_lookup.table_in_tags, byte_lookup.table_byte_lengths};
byte_lookup.sel_bin {byte_lookup.table_in_tags, byte_lookup.table_byte_lengths};

#[LOOKUP_BYTE_OPERATIONS]
bin_sel {op_id, ia_bytes, ib_bytes, ic_bytes}
sel_bin {op_id, ia_bytes, ib_bytes, ic_bytes}
in
byte_lookup.bin_sel {byte_lookup.table_op_id, byte_lookup.table_input_a, byte_lookup.table_input_b, byte_lookup.table_output};
byte_lookup.sel_bin {byte_lookup.table_op_id, byte_lookup.table_input_a, byte_lookup.table_input_b, byte_lookup.table_output};

#[ACC_REL_A]
(acc_ia - ia_bytes - 256 * acc_ia') * mem_tag_ctr = 0;
Expand Down
2 changes: 1 addition & 1 deletion barretenberg/cpp/pil/avm/byte_lookup.pil
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,7 @@ namespace byte_lookup(256);
pol commit table_output; // output = a AND/OR/XOR b
// Selector to indicate when to utilise the lookup table
// TODO: Support for 1-sided lookups may make this redundant.
pol commit bin_sel;
pol commit sel_bin;

// These two columns are a mapping between instruction tags and their byte lengths
// {U8: 1, U16: 2, ... , U128: 16}
Expand Down
6 changes: 2 additions & 4 deletions barretenberg/cpp/pil/avm/gadgets/conversion.pil
Original file line number Diff line number Diff line change
@@ -1,12 +1,10 @@
include "../main.pil";

namespace conversion(256);

pol commit clk;

// Selector for Radix Operation
pol commit to_radix_le_sel;
to_radix_le_sel * (1 - to_radix_le_sel) = 0;
pol commit sel_to_radix_le;
sel_to_radix_le * (1 - sel_to_radix_le) = 0;

// ===== DRAFT: Planned Constraints for To Radix LE
// Similar to the binary trace; multi-row decomposition of the input using the number of limbs specified as the row count.
Expand Down
6 changes: 2 additions & 4 deletions barretenberg/cpp/pil/avm/gadgets/keccakf1600.pil
Original file line number Diff line number Diff line change
@@ -1,12 +1,10 @@
include "../main.pil";

namespace keccakf1600(256);

pol commit clk;

// Selector for Keccak Permutation Operation
pol commit keccakf1600_sel;
keccakf1600_sel * (1 - keccakf1600_sel) = 0;
pol commit sel_keccakf1600;
sel_keccakf1600 * (1 - sel_keccakf1600) = 0;

// These will all be arrays, but we just store the first element for permutation to the main trace for now
pol commit input;
Expand Down
7 changes: 2 additions & 5 deletions barretenberg/cpp/pil/avm/gadgets/pedersen.pil
Original file line number Diff line number Diff line change
@@ -1,13 +1,10 @@

include "../main.pil";

namespace pedersen(256);

pol commit clk;

// Selector for Pedersen Hash Operation
pol commit pedersen_sel;
pedersen_sel * (1 - pedersen_sel) = 0;
pol commit sel_pedersen;
sel_pedersen * (1 - sel_pedersen) = 0;

// These will all be arrays, but we just store the first element for permutation to the main trace for now
pol commit input;
Expand Down
6 changes: 2 additions & 4 deletions barretenberg/cpp/pil/avm/gadgets/poseidon2.pil
Original file line number Diff line number Diff line change
@@ -1,12 +1,10 @@
include "../main.pil";

namespace poseidon2(256);

pol commit clk;

// Selector for Radix Operation
pol commit poseidon_perm_sel;
poseidon_perm_sel * (1 - poseidon_perm_sel) = 0;
pol commit sel_poseidon_perm;
sel_poseidon_perm * (1 - sel_poseidon_perm) = 0;

// These will all be arrays, but we just store the first element for permutation to the main trace for now
pol commit input;
Expand Down
6 changes: 2 additions & 4 deletions barretenberg/cpp/pil/avm/gadgets/sha256.pil
Original file line number Diff line number Diff line change
@@ -1,12 +1,10 @@
include "../main.pil";

namespace sha256(256);

pol commit clk;

// Selector for Radix Operation
pol commit sha256_compression_sel;
sha256_compression_sel * (1 - sha256_compression_sel) = 0;
pol commit sel_sha256_compression;
sel_sha256_compression * (1 - sel_sha256_compression) = 0;

// These will all be arrays, but we just store the first element for permutation to the main trace for now
pol commit state;
Expand Down
3 changes: 1 addition & 2 deletions barretenberg/cpp/pil/avm/gas.pil
Original file line number Diff line number Diff line change
@@ -1,8 +1,7 @@

namespace gas(256);
// TODO: WILL BE FIXED - we should be able to have this be a fixed column / the lookup tables are fixed so require no selectors
// TODO: All the columns here will have to be constant (when supported by our powdr fork and proving system)
pol commit gas_cost_sel;
pol commit sel_gas_cost;

// TODO(ISSUE_NUMBER): Constrain variable gas costs
pol commit l2_gas_fixed_table;
Expand Down
2 changes: 1 addition & 1 deletion barretenberg/cpp/pil/avm/kernel.pil
Original file line number Diff line number Diff line change
Expand Up @@ -58,7 +58,7 @@ namespace kernel(256);
pol commit emit_l2_to_l1_msg_write_offset;


pol NOT_LAST = (1 - main.last);
pol NOT_LAST = (1 - main.sel_last);

// Constraints to increase the offsets when the opcodes are found
#[NOTE_HASH_EXISTS_INC_CONSISTENCY_CHECK]
Expand Down
Loading

0 comments on commit ed2f98e

Please sign in to comment.