Skip to content

Commit

Permalink
refactor(avm): replace range and cmp with gadgets (#8164)
Browse files Browse the repository at this point in the history
Please read [contributing guidelines](CONTRIBUTING.md) and remove this line.
  • Loading branch information
IlyasRidhuan authored and codygunton committed Aug 30, 2024
1 parent 2689086 commit 855bc2b
Show file tree
Hide file tree
Showing 13 changed files with 891 additions and 795 deletions.
32 changes: 31 additions & 1 deletion barretenberg/cpp/pil/avm/gadgets/range_check.pil
Original file line number Diff line number Diff line change
@@ -1,7 +1,10 @@
include "../main.pil";
include "../mem.pil";
include "../fixed/powers.pil";

namespace range_check(256);
// TODO: We should look to rename this to something like rng_idx
// Increasingly this is less likely to be associated directly with a subtrace's clk
pol commit clk;

// Range check selector
Expand All @@ -11,7 +14,7 @@ namespace range_check(256);
// Witnesses
// Value to range check
pol commit value;
// Number of bits to check against
// Number of bits to check against (this number must be <=128)
pol commit rng_chk_bits;

// Bit Size Columns
Expand Down Expand Up @@ -188,3 +191,30 @@ namespace range_check(256);
#[LOOKUP_RNG_CHK_7]
sel_rng_chk { u16_r7 } in main.sel_rng_16 { main.clk };

// ===== MEM TRACE RANGE CHECKS =====
pol commit mem_rng_chk;
// We range check 40 bits in the mem trace
mem_rng_chk * (rng_chk_bits - 40) = 0;

#[PERM_RNG_MEM]
mem_rng_chk {clk, value}
is
mem.sel_rng_chk {mem.tsp, mem.diff};

// ===== GAS TRACE RANGE CHECKS =====
pol commit gas_l2_rng_chk;
pol commit gas_da_rng_chk;
// We range check 32 bits in the gas trace
gas_l2_rng_chk * (rng_chk_bits - 32) = 0;
gas_da_rng_chk * (rng_chk_bits - 32) = 0;

#[PERM_RNG_GAS_L2]
gas_l2_rng_chk {clk, value}
is
main.sel_execution_row {main.clk, main.abs_l2_rem_gas };

#[PERM_RNG_GAS_DA]
gas_da_rng_chk {clk, value}
is
main.sel_execution_row {main.clk, main.abs_da_rem_gas };

13 changes: 0 additions & 13 deletions barretenberg/cpp/pil/avm/gas.pil
Original file line number Diff line number Diff line change
Expand Up @@ -74,16 +74,3 @@ namespace main(256);
sel_execution_row {opcode_val, base_l2_gas_op_cost, base_da_gas_op_cost, dyn_l2_gas_op_cost, dyn_da_gas_op_cost}
in
gas.sel_gas_cost {clk, gas.base_l2_gas_fixed_table, gas.base_da_gas_fixed_table, gas.dyn_l2_gas_fixed_table, gas.dyn_da_gas_fixed_table};

// ========= Initialize Range Check Gadget ===============================
// We range check that the absolute value of the differences between each row of l2 and da gas are 32 bits.
#[PERM_RNG_GAS_L2]
range_check.gas_l2_rng_chk {range_check.clk, range_check.value}
is
main.sel_execution_row {main.clk, main.abs_l2_rem_gas };

#[PERM_RNG_GAS_DA]
range_check.gas_da_rng_chk {range_check.clk, range_check.value}
is
main.sel_execution_row {main.clk, main.abs_da_rem_gas };

1 change: 1 addition & 0 deletions barretenberg/cpp/pil/avm/mem.pil
Original file line number Diff line number Diff line change
Expand Up @@ -66,6 +66,7 @@ namespace mem(256);

// Helper columns
pol commit one_min_inv; // Extra value to prove r_in_tag != tag with error handling
// pol DIFF:
pol commit diff; // 40-bit difference between two consecutive timestamps or two consecutive addresses

// Type constraints
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -600,6 +600,8 @@ AvmCircuitBuilder::ProverPolynomials AvmCircuitBuilder::compute_polynomials() co
polys.range_check_dyn_diff[i] = rows[i].range_check_dyn_diff;
polys.range_check_dyn_rng_chk_bits[i] = rows[i].range_check_dyn_rng_chk_bits;
polys.range_check_dyn_rng_chk_pow_2[i] = rows[i].range_check_dyn_rng_chk_pow_2;
polys.range_check_gas_da_rng_chk[i] = rows[i].range_check_gas_da_rng_chk;
polys.range_check_gas_l2_rng_chk[i] = rows[i].range_check_gas_l2_rng_chk;
polys.range_check_is_lte_u112[i] = rows[i].range_check_is_lte_u112;
polys.range_check_is_lte_u128[i] = rows[i].range_check_is_lte_u128;
polys.range_check_is_lte_u16[i] = rows[i].range_check_is_lte_u16;
Expand All @@ -608,6 +610,7 @@ AvmCircuitBuilder::ProverPolynomials AvmCircuitBuilder::compute_polynomials() co
polys.range_check_is_lte_u64[i] = rows[i].range_check_is_lte_u64;
polys.range_check_is_lte_u80[i] = rows[i].range_check_is_lte_u80;
polys.range_check_is_lte_u96[i] = rows[i].range_check_is_lte_u96;
polys.range_check_mem_rng_chk[i] = rows[i].range_check_mem_rng_chk;
polys.range_check_rng_chk_bits[i] = rows[i].range_check_rng_chk_bits;
polys.range_check_sel_lookup_0[i] = rows[i].range_check_sel_lookup_0;
polys.range_check_sel_lookup_1[i] = rows[i].range_check_sel_lookup_1;
Expand Down
Loading

0 comments on commit 855bc2b

Please sign in to comment.