Skip to content

Commit

Permalink
refactor(avm): extract rng chk from gas and mem
Browse files Browse the repository at this point in the history
  • Loading branch information
IlyasRidhuan committed Aug 19, 2024
1 parent 7322530 commit 93b1914
Show file tree
Hide file tree
Showing 28 changed files with 1,125 additions and 1,461 deletions.
30 changes: 29 additions & 1 deletion barretenberg/cpp/pil/avm/gadgets/range_check.pil
Original file line number Diff line number Diff line change
@@ -1,4 +1,5 @@
include "../main.pil";
include "../mem.pil";
include "../fixed/powers.pil";

namespace range_check(256);
Expand All @@ -11,7 +12,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 @@ -186,3 +187,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 };

22 changes: 4 additions & 18 deletions barretenberg/cpp/pil/avm/gas.pil
Original file line number Diff line number Diff line change
Expand Up @@ -43,10 +43,8 @@ namespace main(256);
pol commit da_out_of_gas;

// Absolute gas remaining value after the operation in 16-bit high and low limbs
pol commit abs_l2_rem_gas_hi;
pol commit abs_l2_rem_gas_lo;
pol commit abs_da_rem_gas_hi;
pol commit abs_da_rem_gas_lo;
pol commit abs_l2_rem_gas;
pol commit abs_da_rem_gas;

// Boolean constraints
l2_out_of_gas * (1 - l2_out_of_gas) = 0;
Expand All @@ -67,22 +65,10 @@ namespace main(256);

// Prove that XX_out_of_gas == 0 <==> XX_gas_remaining' >= 0
// TODO: Ensure that remaining gas values are initialized as u32 and that gas l2_gas_op_cost/da_gas_op_cost are u32.
sel_execution_row * ((1 - 2 * l2_out_of_gas) * l2_gas_remaining' - 2**16 * abs_l2_rem_gas_hi - abs_l2_rem_gas_lo) = 0;
sel_execution_row * ((1 - 2 * da_out_of_gas) * da_gas_remaining' - 2**16 * abs_da_rem_gas_hi - abs_da_rem_gas_lo) = 0;
sel_execution_row * ((1 - 2 * l2_out_of_gas) * l2_gas_remaining' - abs_l2_rem_gas) = 0;
sel_execution_row * ((1 - 2 * da_out_of_gas) * da_gas_remaining' - abs_da_rem_gas) = 0;

#[LOOKUP_OPCODE_GAS]
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};

#[RANGE_CHECK_L2_GAS_HI]
sel_execution_row {abs_l2_rem_gas_hi} in sel_rng_16 {clk};

#[RANGE_CHECK_L2_GAS_LO]
sel_execution_row {abs_l2_rem_gas_lo} in sel_rng_16 {clk};

#[RANGE_CHECK_DA_GAS_HI]
sel_execution_row {abs_da_rem_gas_hi} in sel_rng_16 {clk};

#[RANGE_CHECK_DA_GAS_LO]
sel_execution_row {abs_da_rem_gas_lo} in sel_rng_16 {clk};
12 changes: 6 additions & 6 deletions barretenberg/cpp/pil/avm/main.pil
Original file line number Diff line number Diff line change
Expand Up @@ -732,14 +732,14 @@ namespace main(256);
is
mem.sel_resolve_ind_addr_d {mem.clk, mem.space_id, mem.addr, mem.val};

#[LOOKUP_MEM_RNG_CHK_LO]
mem.sel_rng_chk {mem.diff_lo} in sel_rng_16 {clk};
// #[LOOKUP_MEM_RNG_CHK_LO]
// mem.sel_rng_chk {mem.diff_lo} in sel_rng_16 {clk};

#[LOOKUP_MEM_RNG_CHK_MID]
mem.sel_rng_chk {mem.diff_mid} in sel_rng_16 {clk};
// #[LOOKUP_MEM_RNG_CHK_MID]
// mem.sel_rng_chk {mem.diff_mid} in sel_rng_16 {clk};

#[LOOKUP_MEM_RNG_CHK_HI]
mem.sel_rng_chk {mem.diff_hi} in sel_rng_8 {clk};
//#[LOOKUP_MEM_RNG_CHK_HI]
//mem.sel_rng_chk {mem.diff_hi} in sel_rng_8 {clk};

//====== Inter-table Shift Constraints (Lookups) ============================================
// Currently only used for shift operations but can be generalised for other uses.
Expand Down
12 changes: 5 additions & 7 deletions barretenberg/cpp/pil/avm/mem.pil
Original file line number Diff line number Diff line change
Expand Up @@ -65,10 +65,8 @@ namespace mem(256);

// Helper columns
pol commit one_min_inv; // Extra value to prove r_in_tag != tag with error handling
// pol DIFF: 40-bit difference between two consecutive timestamps or two consecutive addresses
pol commit diff_hi; // Higher 8-bit limb of diff.
pol commit diff_mid; // Middle 16-bit limb of diff.
pol commit diff_lo; // Lower 16-bit limb of diff.
// pol DIFF:
pol commit diff; // 40-bit difference between two consecutive timestamps or two consecutive addresses

// Type constraints
lastAccess * (1 - lastAccess) = 0;
Expand Down Expand Up @@ -156,14 +154,14 @@ namespace mem(256);
// i.e., when sel_rng_chk == 1, we compute the difference:
// 1) glob_addr' - glob_addr if lastAccess == 1
// 2) tsp' - tsp if lastAccess == 0 (i.e., whenever glob_addr' == glob_addr)
pol DIFF = lastAccess * (glob_addr' - glob_addr) + (1 - lastAccess) * (tsp' - tsp);
sel_rng_chk * (diff - (lastAccess * (glob_addr' - glob_addr) + (1 - lastAccess) * (tsp' - tsp))) = 0;

// We perform a 40-bit range check of DIFF which proves that glob_addr' > glob_addr if lastAccess == 1
// and tsp' > tsp whenever glob_addr' == glob_addr
// Therefore, we ensure proper grouping of each global address and each memory access pertaining to a given
// global address is sorted according the arrow of time.
#[DIFF_RNG_CHK_DEC]
sel_rng_chk * (DIFF - diff_hi * 2**32 - diff_mid * 2**16 - diff_lo) = 0;
// #[DIFF_RNG_CHK_DEC]
// sel_rng_chk * (DIFF - diff_hi * 2**32 - diff_mid * 2**16 - diff_lo) = 0;

// lastAccess == 0 && rw' == 0 ==> val == val'
// This condition does not apply on the last row.
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -166,10 +166,8 @@ AvmCircuitBuilder::ProverPolynomials AvmCircuitBuilder::compute_polynomials() co
polys.kernel_side_effect_counter[i] = rows[i].kernel_side_effect_counter;
polys.kernel_sload_write_offset[i] = rows[i].kernel_sload_write_offset;
polys.kernel_sstore_write_offset[i] = rows[i].kernel_sstore_write_offset;
polys.main_abs_da_rem_gas_hi[i] = rows[i].main_abs_da_rem_gas_hi;
polys.main_abs_da_rem_gas_lo[i] = rows[i].main_abs_da_rem_gas_lo;
polys.main_abs_l2_rem_gas_hi[i] = rows[i].main_abs_l2_rem_gas_hi;
polys.main_abs_l2_rem_gas_lo[i] = rows[i].main_abs_l2_rem_gas_lo;
polys.main_abs_da_rem_gas[i] = rows[i].main_abs_da_rem_gas;
polys.main_abs_l2_rem_gas[i] = rows[i].main_abs_l2_rem_gas;
polys.main_alu_in_tag[i] = rows[i].main_alu_in_tag;
polys.main_base_da_gas_op_cost[i] = rows[i].main_base_da_gas_op_cost;
polys.main_base_l2_gas_op_cost[i] = rows[i].main_base_l2_gas_op_cost;
Expand Down Expand Up @@ -289,9 +287,7 @@ AvmCircuitBuilder::ProverPolynomials AvmCircuitBuilder::compute_polynomials() co
polys.main_w_in_tag[i] = rows[i].main_w_in_tag;
polys.mem_addr[i] = rows[i].mem_addr;
polys.mem_clk[i] = rows[i].mem_clk;
polys.mem_diff_hi[i] = rows[i].mem_diff_hi;
polys.mem_diff_lo[i] = rows[i].mem_diff_lo;
polys.mem_diff_mid[i] = rows[i].mem_diff_mid;
polys.mem_diff[i] = rows[i].mem_diff;
polys.mem_glob_addr[i] = rows[i].mem_glob_addr;
polys.mem_last[i] = rows[i].mem_last;
polys.mem_lastAccess[i] = rows[i].mem_lastAccess;
Expand Down Expand Up @@ -615,6 +611,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 @@ -623,6 +621,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 Expand Up @@ -670,19 +669,12 @@ AvmCircuitBuilder::ProverPolynomials AvmCircuitBuilder::compute_polynomials() co
polys.lookup_byte_lengths_counts[i] = rows[i].lookup_byte_lengths_counts;
polys.lookup_byte_operations_counts[i] = rows[i].lookup_byte_operations_counts;
polys.lookup_opcode_gas_counts[i] = rows[i].lookup_opcode_gas_counts;
polys.range_check_l2_gas_hi_counts[i] = rows[i].range_check_l2_gas_hi_counts;
polys.range_check_l2_gas_lo_counts[i] = rows[i].range_check_l2_gas_lo_counts;
polys.range_check_da_gas_hi_counts[i] = rows[i].range_check_da_gas_hi_counts;
polys.range_check_da_gas_lo_counts[i] = rows[i].range_check_da_gas_lo_counts;
polys.lookup_cd_value_counts[i] = rows[i].lookup_cd_value_counts;
polys.lookup_ret_value_counts[i] = rows[i].lookup_ret_value_counts;
polys.kernel_output_lookup_counts[i] = rows[i].kernel_output_lookup_counts;
polys.lookup_into_kernel_counts[i] = rows[i].lookup_into_kernel_counts;
polys.incl_main_tag_err_counts[i] = rows[i].incl_main_tag_err_counts;
polys.incl_mem_tag_err_counts[i] = rows[i].incl_mem_tag_err_counts;
polys.lookup_mem_rng_chk_lo_counts[i] = rows[i].lookup_mem_rng_chk_lo_counts;
polys.lookup_mem_rng_chk_mid_counts[i] = rows[i].lookup_mem_rng_chk_mid_counts;
polys.lookup_mem_rng_chk_hi_counts[i] = rows[i].lookup_mem_rng_chk_hi_counts;
polys.lookup_pow_2_0_counts[i] = rows[i].lookup_pow_2_0_counts;
polys.lookup_pow_2_1_counts[i] = rows[i].lookup_pow_2_1_counts;
polys.lookup_u8_0_counts[i] = rows[i].lookup_u8_0_counts;
Expand Down
Loading

0 comments on commit 93b1914

Please sign in to comment.