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

feat(avm): Skip gas accounting for fake rows #8944

Merged
merged 2 commits into from
Oct 3, 2024
Merged

feat(avm): Skip gas accounting for fake rows #8944

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
e1b87c0
8903: Skip gas accounting for fake rows
jeanmon Oct 1, 2024
32cfa24
8903: remove discrepancies between simulator and circuit
jeanmon Oct 3, 2024
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
31 changes: 24 additions & 7 deletions barretenberg/cpp/pil/avm/gas.pil
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -48,15 +48,32 @@ namespace main(256);
pol commit abs_l2_rem_gas;
pol commit abs_da_rem_gas;

// TODO(8945): Temporary workaround until we remove fake rows
// A boolean to toggle "fake" rows in main trace. It serves to remove them from gas accounting.
// The values in l2/da_gas_remaining will not change on such rows.
// Once all fake rows are removed, we can replace is_gas_accounted by sel_execution_row in all relations below.
pol commit is_fake_row;
pol commit is_gas_accounted;
#[IS_GAS_ACCOUNTED]
is_gas_accounted = (1 - is_fake_row) * sel_execution_row;

// Boolean constraints
l2_out_of_gas * (1 - l2_out_of_gas) = 0;
da_out_of_gas * (1 - da_out_of_gas) = 0;
// TODO(8945): clean up fake row related code
is_fake_row * (1 - is_fake_row) = 0; // Temporary

//TODO(8945): clean up fake row related code
#[L2_GAS_NO_DECREMENT_FAKE_ROW]
is_fake_row * (l2_gas_remaining - l2_gas_remaining') = 0;
#[DA_GAS_NO_DECREMENT_FAKE_ROW]
is_fake_row * (da_gas_remaining - da_gas_remaining') = 0;

// Constrain that the gas decrements correctly per instruction
#[L2_GAS_REMAINING_DECREMENT_NOT_CALL]
sel_execution_row * (1 - sel_op_external_call - sel_op_static_call) * (l2_gas_remaining' - l2_gas_remaining + base_l2_gas_op_cost + (dyn_l2_gas_op_cost * dyn_gas_multiplier)) = 0;
is_gas_accounted * (1 - sel_op_external_call - sel_op_static_call) * (l2_gas_remaining' - l2_gas_remaining + base_l2_gas_op_cost + (dyn_l2_gas_op_cost * dyn_gas_multiplier)) = 0;
#[DA_GAS_REMAINING_DECREMENT_NOT_CALL]
sel_execution_row * (1 - sel_op_external_call - sel_op_static_call) * (da_gas_remaining' - da_gas_remaining + base_da_gas_op_cost + (dyn_da_gas_op_cost * dyn_gas_multiplier)) = 0;
is_gas_accounted * (1 - sel_op_external_call - sel_op_static_call) * (da_gas_remaining' - da_gas_remaining + base_da_gas_op_cost + (dyn_da_gas_op_cost * dyn_gas_multiplier)) = 0;
// We need to special-case external calls since the gas cost format is
// base_l2 + nested_call_cost + dyn_gas_cost * dyn_gas_multiplier.
// TODO: Unconstrained until CALL is properly implemented.
Expand All @@ -67,11 +84,11 @@ 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' - abs_l2_rem_gas) = 0;
sel_execution_row * ((1 - 2 * da_out_of_gas) * da_gas_remaining' - abs_da_rem_gas) = 0;
is_gas_accounted * ((1 - 2 * l2_out_of_gas) * l2_gas_remaining' - abs_l2_rem_gas) = 0;
is_gas_accounted * ((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}
is_gas_accounted {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};

Expand All @@ -80,10 +97,10 @@ namespace main(256);
#[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 };
is_gas_accounted {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 };
is_gas_accounted {main.clk, main.abs_da_rem_gas };

2 changes: 2 additions & 0 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 @@ -193,6 +193,8 @@ AvmCircuitBuilder::ProverPolynomials AvmCircuitBuilder::compute_polynomials() co
polys.main_ind_addr_d.set_if_valid_index(i, rows[i].main_ind_addr_d);
polys.main_internal_return_ptr.set_if_valid_index(i, rows[i].main_internal_return_ptr);
polys.main_inv.set_if_valid_index(i, rows[i].main_inv);
polys.main_is_fake_row.set_if_valid_index(i, rows[i].main_is_fake_row);
polys.main_is_gas_accounted.set_if_valid_index(i, rows[i].main_is_gas_accounted);
polys.main_kernel_in_offset.set_if_valid_index(i, rows[i].main_kernel_in_offset);
polys.main_kernel_out_offset.set_if_valid_index(i, rows[i].main_kernel_out_offset);
polys.main_l1_to_l2_msg_exists_write_offset.set_if_valid_index(
Expand Down
Loading
Loading