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): gas remaining range check and handling of out of gas #6944

Merged
merged 4 commits into from
Jun 11, 2024
Merged

feat(avm): gas remaining range check and handling of out of gas #6944

Show file tree
Hide file tree
Changes from 3 commits
Commits
Show all changes
4 commits
Select commit Hold shift + click to select a range
3ee191c
6902: PIL relations for gas remaining checks
jeanmon Jun 5, 2024
9849928
6902: handle out of gas range check and error boolean in witness gene…
jeanmon Jun 6, 2024
441e68b
6902: rebase on top of master and resolve conflicts
jeanmon Jun 9, 2024
3403012
Update avm_arithmetic.test.cpp
jeanmon Jun 10, 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
40 changes: 36 additions & 4 deletions barretenberg/cpp/pil/avm/avm_main.pil
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -75,10 +75,19 @@ namespace avm_main(256);
pol commit l2_gas_op;
pol commit da_gas_op;

#[LOOKUP_OPCODE_GAS]
gas_cost_active {opcode_val, l2_gas_op, da_gas_op}
in
avm_gas.gas_cost_sel {clk, avm_gas.l2_gas_fixed_table, avm_gas.da_gas_fixed_table};
// Boolean indicating whether the current opcode gas consumption is higher than remaining gas
pol commit l2_out_of_gas;
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;

// Boolean constraints
l2_out_of_gas * (1 - l2_out_of_gas) = 0;
da_out_of_gas * (1 - da_out_of_gas) = 0;

// Constrain that the gas decrements correctly per instruction
#[L2_GAS_REMAINING_DECREMENT]
Expand All @@ -95,6 +104,29 @@ namespace avm_main(256);
// TODO: constrain that it stays the same if an opcode selector is not active -> TODO: will this break when the opcode takes multiple rows
// So we also need to constrain that it is the first line of the opcodes execution

// Prove that l2_out_of_gas == 0 <==> l2_gas_remaining' >= 0
// Same for da gas
// TODO: Ensure that remaining gas values are initialized as u32 and that gas l2_gas_op/da_gas_op are u32.
gas_cost_active * ((1 - 2 * l2_out_of_gas) * l2_gas_remaining' - 2**16 * abs_l2_rem_gas_hi - abs_l2_rem_gas_lo) = 0;
gas_cost_active * ((1 - 2 * da_out_of_gas) * da_gas_remaining' - 2**16 * abs_da_rem_gas_hi - abs_da_rem_gas_lo) = 0;

#[LOOKUP_OPCODE_GAS]
gas_cost_active {opcode_val, l2_gas_op, da_gas_op}
in
avm_gas.gas_cost_sel {clk, avm_gas.l2_gas_fixed_table, avm_gas.da_gas_fixed_table};

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

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

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

#[RANGE_CHECK_DA_GAS_LO]
gas_cost_active {abs_da_rem_gas_lo} in sel_rng_16 {clk};

//===== Gadget Selectors ======================================================
pol commit sel_op_radix_le;
pol commit sel_op_sha256;
Expand Down
Loading
Loading