Skip to content

Commit

Permalink
feat(avm): constrain start and end l2/da gas (#9031)
Browse files Browse the repository at this point in the history 
Resolves #9001
  • Loading branch information
@jeanmon
jeanmon authored Oct 8, 2024
1 parent e3b467f commit 308c03b
Show file tree
Hide file tree
Showing 32 changed files with 1,608 additions and 1,237 deletions.
31 changes: 16 additions & 15 deletions barretenberg/cpp/pil/avm/constants_gen.pil
View file
Original file line number Diff line number Diff line change
Expand Up @@ -18,21 +18,22 @@ namespace constants(256);
pol MEM_TAG_U64 = 5;
pol MEM_TAG_U128 = 6;
pol MEM_TAG_FF = 7;
pol SENDER_SELECTOR = 0;
pol ADDRESS_SELECTOR = 1;
pol STORAGE_ADDRESS_SELECTOR = 1;
pol FUNCTION_SELECTOR_SELECTOR = 2;
pol IS_STATIC_CALL_SELECTOR = 4;
pol START_GLOBAL_VARIABLES = 29;
pol CHAIN_ID_SELECTOR = 29;
pol VERSION_SELECTOR = 30;
pol BLOCK_NUMBER_SELECTOR = 31;
pol TIMESTAMP_SELECTOR = 33;
pol FEE_PER_DA_GAS_SELECTOR = 36;
pol FEE_PER_L2_GAS_SELECTOR = 37;
pol END_GLOBAL_VARIABLES = 38;
pol START_SIDE_EFFECT_COUNTER = 38;
pol TRANSACTION_FEE_SELECTOR = 41;
pol SENDER_KERNEL_INPUTS_COL_OFFSET = 0;
pol ADDRESS_KERNEL_INPUTS_COL_OFFSET = 1;
pol STORAGE_ADDRESS_KERNEL_INPUTS_COL_OFFSET = 1;
pol FUNCTION_SELECTOR_KERNEL_INPUTS_COL_OFFSET = 2;
pol IS_STATIC_CALL_KERNEL_INPUTS_COL_OFFSET = 3;
pol CHAIN_ID_KERNEL_INPUTS_COL_OFFSET = 4;
pol VERSION_KERNEL_INPUTS_COL_OFFSET = 5;
pol BLOCK_NUMBER_KERNEL_INPUTS_COL_OFFSET = 6;
pol TIMESTAMP_KERNEL_INPUTS_COL_OFFSET = 7;
pol FEE_PER_DA_GAS_KERNEL_INPUTS_COL_OFFSET = 8;
pol FEE_PER_L2_GAS_KERNEL_INPUTS_COL_OFFSET = 9;
pol DA_START_GAS_KERNEL_INPUTS_COL_OFFSET = 10;
pol L2_START_GAS_KERNEL_INPUTS_COL_OFFSET = 11;
pol DA_END_GAS_KERNEL_INPUTS_COL_OFFSET = 12;
pol L2_END_GAS_KERNEL_INPUTS_COL_OFFSET = 13;
pol TRANSACTION_FEE_KERNEL_INPUTS_COL_OFFSET = 14;
pol START_NOTE_HASH_EXISTS_WRITE_OFFSET = 0;
pol START_NULLIFIER_EXISTS_OFFSET = 16;
pol START_NULLIFIER_NON_EXISTS_OFFSET = 32;
Expand Down
49 changes: 36 additions & 13 deletions barretenberg/cpp/pil/avm/kernel.pil
View file
Original file line number Diff line number Diff line change
Expand Up @@ -21,6 +21,12 @@ namespace main(256);
pol commit sel_kernel_inputs;
pol commit sel_kernel_out;

// Selectors toggling a fixed specific offset in kernel input column
pol constant sel_l2_start_gas_kernel_input;
pol constant sel_da_start_gas_kernel_input;
pol constant sel_l2_end_gas_kernel_input;
pol constant sel_da_end_gas_kernel_input;

// Kernel Outputs
//
// The current implementation of kernel outputs is described within https://hackmd.io/zP1oMXF6Rf-L-ZZLXWmfHg
Expand Down Expand Up @@ -84,42 +90,42 @@ namespace main(256);
// TODO: I think we can replace all these (IN) with a single lookup.
// CONTEXT - ENVIRONMENT
#[ADDRESS_KERNEL]
sel_op_address * (kernel_in_offset - constants.ADDRESS_SELECTOR) = 0;
sel_op_address * (kernel_in_offset - constants.ADDRESS_KERNEL_INPUTS_COL_OFFSET) = 0;

#[STORAGE_ADDRESS_KERNEL]
sel_op_storage_address * (kernel_in_offset - constants.STORAGE_ADDRESS_SELECTOR) = 0;
sel_op_storage_address * (kernel_in_offset - constants.STORAGE_ADDRESS_KERNEL_INPUTS_COL_OFFSET) = 0;

#[SENDER_KERNEL]
sel_op_sender * (kernel_in_offset - constants.SENDER_SELECTOR) = 0;
sel_op_sender * (kernel_in_offset - constants.SENDER_KERNEL_INPUTS_COL_OFFSET) = 0;

#[FUNCTION_SELECTOR_KERNEL]
sel_op_function_selector * (kernel_in_offset - constants.FUNCTION_SELECTOR_SELECTOR) = 0;
sel_op_function_selector * (kernel_in_offset - constants.FUNCTION_SELECTOR_KERNEL_INPUTS_COL_OFFSET) = 0;

#[FEE_TRANSACTION_FEE_KERNEL]
sel_op_transaction_fee * (kernel_in_offset - constants.TRANSACTION_FEE_SELECTOR) = 0;
sel_op_transaction_fee * (kernel_in_offset - constants.TRANSACTION_FEE_KERNEL_INPUTS_COL_OFFSET) = 0;

#[IS_STATIC_CALL_KERNEL]
sel_op_is_static_call * (kernel_in_offset - constants.IS_STATIC_CALL_SELECTOR) = 0;
sel_op_is_static_call * (kernel_in_offset - constants.IS_STATIC_CALL_KERNEL_INPUTS_COL_OFFSET) = 0;

// CONTEXT - ENVIRONMENT - GLOBALS
#[CHAIN_ID_KERNEL]
sel_op_chain_id * (kernel_in_offset - constants.CHAIN_ID_SELECTOR) = 0;
sel_op_chain_id * (kernel_in_offset - constants.CHAIN_ID_KERNEL_INPUTS_COL_OFFSET) = 0;

#[VERSION_KERNEL]
sel_op_version * (kernel_in_offset - constants.VERSION_SELECTOR) = 0;
sel_op_version * (kernel_in_offset - constants.VERSION_KERNEL_INPUTS_COL_OFFSET) = 0;

#[BLOCK_NUMBER_KERNEL]
sel_op_block_number * (kernel_in_offset - constants.BLOCK_NUMBER_SELECTOR) = 0;
sel_op_block_number * (kernel_in_offset - constants.BLOCK_NUMBER_KERNEL_INPUTS_COL_OFFSET) = 0;

#[TIMESTAMP_KERNEL]
sel_op_timestamp * (kernel_in_offset - constants.TIMESTAMP_SELECTOR) = 0;
sel_op_timestamp * (kernel_in_offset - constants.TIMESTAMP_KERNEL_INPUTS_COL_OFFSET) = 0;

// CONTEXT - ENVIRONMENT - GLOBALS - FEES
#[FEE_DA_GAS_KERNEL]
sel_op_fee_per_da_gas * (kernel_in_offset - constants.FEE_PER_DA_GAS_SELECTOR) = 0;
sel_op_fee_per_da_gas * (kernel_in_offset - constants.FEE_PER_DA_GAS_KERNEL_INPUTS_COL_OFFSET) = 0;

#[FEE_L2_GAS_KERNEL]
sel_op_fee_per_l2_gas * (kernel_in_offset - constants.FEE_PER_L2_GAS_SELECTOR) = 0;
sel_op_fee_per_l2_gas * (kernel_in_offset - constants.FEE_PER_L2_GAS_KERNEL_INPUTS_COL_OFFSET) = 0;

// OUTPUTS LOOKUPS
// Constrain the value of kernel_out_offset to be the correct offset for the operation being performed
Expand Down Expand Up @@ -187,4 +193,21 @@ namespace main(256);
sel_q_kernel_output_lookup {kernel_out_offset, /*ia,*/ /*side_effect_counter,*/ ib } in sel_kernel_out {clk, /*kernel_value_out,*/ /*kernel_side_effect_out,*/ kernel_metadata_out};

#[LOOKUP_INTO_KERNEL]
sel_q_kernel_lookup { main.ia, kernel_in_offset } in sel_kernel_inputs { kernel_inputs, clk };
sel_q_kernel_lookup { ia, kernel_in_offset } in sel_kernel_inputs { kernel_inputs, clk };

// Start/End Gas related permutations
// A lookup of the form "{CONST, gas_remaining} in {clk, kernel_in}" was considered but cannot
// be performed as long as we are not supporting constants or expressions in a tuple involved
// in a lookup/permutation.

#[PERM_L2_START_GAS]
sel_start_exec { l2_gas_remaining } is sel_l2_start_gas_kernel_input { kernel_inputs };

#[PERM_DA_START_GAS]
sel_start_exec { da_gas_remaining } is sel_da_start_gas_kernel_input { kernel_inputs };

#[PERM_L2_END_GAS]
sel_execution_end { l2_gas_remaining } is sel_l2_end_gas_kernel_input { kernel_inputs };

#[PERM_DA_END_GAS]
sel_execution_end { da_gas_remaining } is sel_da_end_gas_kernel_input { kernel_inputs };
11 changes: 6 additions & 5 deletions barretenberg/cpp/pil/avm/main.pil
View file
Original file line number Diff line number Diff line change
Expand Up @@ -19,7 +19,7 @@ namespace main(256);
pol constant sel_first = [1] + [0]*; // Used mostly to toggle off the first row consisting
// only in first element of shifted polynomials.
pol constant zeroes = [0]*; // Helper for if we need to use a constant zero column

pol constant sel_start_exec; // Toggle row which starts main execution trace (clk == 1).
//===== HELPER POLYNOMIALS ==================================================
// This column signals active rows in the main trace table, which should
// be every row except the first, and the padding rows at the end.
Expand All @@ -30,6 +30,11 @@ namespace main(256);
sel_execution_row * (1 - sel_execution_row) = 0;
// TODO: constrain that the right rows are marked with sel_execution_row

pol commit sel_execution_end; // Toggle next row of last execution trace row.
// Used as a LHS selector of the lookup to enforce final gas values which correspond to
// l2_gas_remaining and da_gas_remaining values located at the row after last execution row.
sel_execution_end' = sel_execution_row * (1 - sel_execution_row') * (1 - sel_first);

//===== PUBLIC COLUMNS=========================================================
pol public calldata;
pol commit sel_calldata; // Selector used for lookup in calldata. TODO: Might be removed or made constant.
Expand Down Expand Up @@ -209,10 +214,6 @@ namespace main(256);
pol commit sel_resolve_ind_addr_c;
pol commit sel_resolve_ind_addr_d;

// Track the last line of the execution trace. It does NOT correspond to the last row of the whole table
// of size N. As this depends on the supplied bytecode, this polynomial cannot be constant.
pol commit sel_last;

// Relations on type constraints
// TODO: Very likely, we can remove these constraints as the selectors should be derived during
// opcode decomposition.
Expand Down
9 changes: 8 additions & 1 deletion barretenberg/cpp/src/barretenberg/dsl/acir_format/avm_recursion_constraint.test.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -42,7 +42,8 @@ class AcirAvmRecursionConstraint : public ::testing::Test {

static void SetUpTestSuite() { bb::srs::init_crs_factory("../srs_db/ignition"); }

static InnerBuilder create_inner_circuit(const std::vector<FF>& kernel_public_inputs_vec)
// mutate the input kernel_public_inputs_vec to add end gas values
static InnerBuilder create_inner_circuit(std::vector<FF>& kernel_public_inputs_vec)
{
auto public_inputs = convert_public_inputs(kernel_public_inputs_vec);
AvmTraceBuilder trace_builder(public_inputs);
Expand All @@ -56,6 +57,12 @@ class AcirAvmRecursionConstraint : public ::testing::Test {
trace_builder.op_return(0, 0, 0);
auto trace = trace_builder.finalize(); // Passing true enables a longer trace with lookups

avm_trace::inject_end_gas_values(public_inputs, trace);
kernel_public_inputs_vec.at(DA_END_GAS_LEFT_PCPI_OFFSET) =
std::get<KERNEL_INPUTS>(public_inputs).at(DA_END_GAS_KERNEL_INPUTS_COL_OFFSET);
kernel_public_inputs_vec.at(L2_END_GAS_LEFT_PCPI_OFFSET) =
std::get<KERNEL_INPUTS>(public_inputs).at(L2_END_GAS_KERNEL_INPUTS_COL_OFFSET);

builder.set_trace(std::move(trace));
builder.check_circuit();
return builder;
Expand Down
9 changes: 8 additions & 1 deletion barretenberg/cpp/src/barretenberg/vm/avm/generated/circuit_builder.cpp
View file
Original file line number Diff line number Diff line change
Expand Up @@ -59,7 +59,14 @@ AvmCircuitBuilder::ProverPolynomials AvmCircuitBuilder::compute_polynomials() co
polys.gas_dyn_l2_gas_fixed_table.set_if_valid_index(i, rows[i].gas_dyn_l2_gas_fixed_table);
polys.gas_sel_gas_cost.set_if_valid_index(i, rows[i].gas_sel_gas_cost);
polys.main_clk.set_if_valid_index(i, rows[i].main_clk);
polys.main_sel_da_end_gas_kernel_input.set_if_valid_index(i, rows[i].main_sel_da_end_gas_kernel_input);
polys.main_sel_da_start_gas_kernel_input.set_if_valid_index(i,
rows[i].main_sel_da_start_gas_kernel_input);
polys.main_sel_first.set_if_valid_index(i, rows[i].main_sel_first);
polys.main_sel_l2_end_gas_kernel_input.set_if_valid_index(i, rows[i].main_sel_l2_end_gas_kernel_input);
polys.main_sel_l2_start_gas_kernel_input.set_if_valid_index(i,
rows[i].main_sel_l2_start_gas_kernel_input);
polys.main_sel_start_exec.set_if_valid_index(i, rows[i].main_sel_start_exec);
polys.main_zeroes.set_if_valid_index(i, rows[i].main_zeroes);
polys.powers_power_of_2.set_if_valid_index(i, rows[i].powers_power_of_2);
polys.main_kernel_inputs.set_if_valid_index(i, rows[i].main_kernel_inputs);
Expand Down Expand Up @@ -222,10 +229,10 @@ AvmCircuitBuilder::ProverPolynomials AvmCircuitBuilder::compute_polynomials() co
polys.main_sel_alu.set_if_valid_index(i, rows[i].main_sel_alu);
polys.main_sel_bin.set_if_valid_index(i, rows[i].main_sel_bin);
polys.main_sel_calldata.set_if_valid_index(i, rows[i].main_sel_calldata);
polys.main_sel_execution_end.set_if_valid_index(i, rows[i].main_sel_execution_end);
polys.main_sel_execution_row.set_if_valid_index(i, rows[i].main_sel_execution_row);
polys.main_sel_kernel_inputs.set_if_valid_index(i, rows[i].main_sel_kernel_inputs);
polys.main_sel_kernel_out.set_if_valid_index(i, rows[i].main_sel_kernel_out);
polys.main_sel_last.set_if_valid_index(i, rows[i].main_sel_last);
polys.main_sel_mem_op_a.set_if_valid_index(i, rows[i].main_sel_mem_op_a);
polys.main_sel_mem_op_b.set_if_valid_index(i, rows[i].main_sel_mem_op_b);
polys.main_sel_mem_op_c.set_if_valid_index(i, rows[i].main_sel_mem_op_c);
Expand Down
Loading

0 comments on commit 308c03b

Please sign in to comment.