Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

refactor(avm): replace range and cmp with gadgets #8164

Merged
merged 1 commit into from
Aug 29, 2024
Merged

refactor(avm): replace range and cmp with gadgets #8164

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
32 changes: 31 additions & 1 deletion barretenberg/cpp/pil/avm/gadgets/range_check.pil
View file
Open in desktop
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}
IlyasRidhuan marked this conversation as resolved.
Show resolved Hide resolved
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
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -44,10 +44,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 @@ -68,22 +66,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};
9 changes: 0 additions & 9 deletions barretenberg/cpp/pil/avm/main.pil
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -619,12 +619,3 @@ namespace main(256);
sel_resolve_ind_addr_d {clk, space_id, ind_addr_d, mem_addr_d}
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_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};
10 changes: 3 additions & 7 deletions barretenberg/cpp/pil/avm/mem.pil
View file
Open in desktop
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,12 @@ 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;

// lastAccess == 0 && rw' == 0 ==> val == val'
// This condition does not apply on the last row.
Expand Down
20 changes: 6 additions & 14 deletions barretenberg/cpp/src/barretenberg/vm/avm/generated/circuit_builder.cpp
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -151,10 +151,8 @@ AvmCircuitBuilder::ProverPolynomials AvmCircuitBuilder::compute_polynomials() co
polys.keccakf1600_input[i] = rows[i].keccakf1600_input;
polys.keccakf1600_output[i] = rows[i].keccakf1600_output;
polys.keccakf1600_sel_keccakf1600[i] = rows[i].keccakf1600_sel_keccakf1600;
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 @@ -697,19 +696,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.kernel_output_lookup_counts[i] = rows[i].kernel_output_lookup_counts;
polys.lookup_into_kernel_counts[i] = rows[i].lookup_into_kernel_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.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;
}

for (auto [shifted, to_be_shifted] : zip_view(polys.get_shifted(), polys.get_to_be_shifted())) {
Expand Down
Loading
Loading