Skip to content

Commit

Permalink
refactor(avm): kernel trace and finalization (#8049)
Browse files Browse the repository at this point in the history 
The original objective of this PR was to just remove kernel `finalize()`
from `trace.cpp`. Other things were done on top but I do not claim to
have solved or constrained everything.

Something that I realized while working on this: right now gas is broken
for SLOAD/SSTORE/UNENCRYPTEDLOG because they still either use SET or
take multiple lines (or should). However, if they take multiple lines,
we have to move them to their own gadget, and if we do so, then their
kernel accesses (1 per item) will make the kernel trace not be 1-1
anymore. So, we might need to rethink this whole trace.

-----

PIL
* Made kernel trace officially virtual
* Moved most constraints, lookups, etc from main to kernel
* Changed a few constraints; now we will constrain all rows of the
execution trace (this bleeds to "last + 1" using the shifts, on purpose)
* Changed some names and added some comments to make it more
understandable, but still needs love

CPP
* Encapsulated kernel finalization in its own finalize
* Changed `sel_last` to actually be the last row of the execution trace,
as PIL says. (in any case, it's not used now)
* Other misc changes:
* error reporting in check circuit now only reports first failure for
each subrelation (otherwise rows were spammed, but it didn't mean that
the actual row didn't satisfy it, just that the accumulator was already
"dirty")
  * Moved execution hints to their own hpp
  • Loading branch information
@fcarreiro
fcarreiro authored Aug 19, 2024
1 parent cee4eba commit d7edd24
Show file tree
Hide file tree
Showing 27 changed files with 1,731 additions and 1,564 deletions.
3 changes: 2 additions & 1 deletion barretenberg/cpp/pil/avm/gas.pil
View file
Original file line number Diff line number Diff line change
@@ -1,6 +1,7 @@
include "fixed/gas.pil";

// Gas is a "virtual" trace. Things are only in a separate file for modularity.
// This is a "virtual" trace. Things are only in a separate file for modularity.
// That is, this trace is expected to be in 1-1 relation with the main trace.
// However, the columns and relations are set on the "main" namespace.
namespace main(256);
//===== GAS ACCOUNTING ========================================================
Expand Down
167 changes: 144 additions & 23 deletions barretenberg/cpp/pil/avm/kernel.pil
View file
Original file line number Diff line number Diff line change
@@ -1,9 +1,14 @@
include "main.pil";
include "constants_gen.pil";

namespace kernel(256);
pol public kernel_inputs;
// The kernel trace is divided into two parts:
// - A 1-1 virtual trace
// - The public inputs which are looked up from the virtual trace

// This is a "virtual" trace. Things are only in a separate file for modularity.
// That is, this trace is expected to be in 1-1 relation with the main trace.
// However, the columns and relations are set on the "main" namespace.
namespace main(256);
pol public kernel_inputs;
pol public kernel_value_out;
pol public kernel_side_effect_out;
pol public kernel_metadata_out;
Expand All @@ -12,10 +17,9 @@ namespace kernel(256);
pol commit kernel_in_offset;
pol commit kernel_out_offset;

// Note: in the future, with some codegen adjustments, this column will not be needed
// as we can just add every entry in the public kernel_inputs to the lookup table
pol commit q_public_input_kernel_add_to_table;
pol commit q_public_input_kernel_out_add_to_table;
// These are selectors for the lookups on the public inputs.
pol commit sel_kernel_inputs;
pol commit sel_kernel_out;

// Kernel Outputs
//
Expand All @@ -24,7 +28,8 @@ namespace kernel(256);
// Global side effect counter; incremented after each side effect is produced.
pol commit side_effect_counter;

// TODO(https://github.com/AztecProtocol/aztec-packages/issues/6465): Must constrain write_offset counters to be less than side effect MAX
// TODO(https://github.com/AztecProtocol/aztec-packages/issues/6465): Must constrain write_offset
// counters to be less than side effect MAX
// Current write offsets for each opcode
pol commit note_hash_exist_write_offset;
pol commit nullifier_exists_write_offset;
Expand All @@ -39,30 +44,146 @@ namespace kernel(256);
pol commit emit_unencrypted_log_write_offset;
pol commit emit_l2_to_l1_msg_write_offset;


pol NOT_LAST = (1 - main.sel_last);

// Constraints to increase the offsets when the opcodes are found
#[NOTE_HASH_EXISTS_INC_CONSISTENCY_CHECK]
NOT_LAST * (note_hash_exist_write_offset' - (note_hash_exist_write_offset + main.sel_op_note_hash_exists)) = 0;
sel_execution_row * (note_hash_exist_write_offset' - (note_hash_exist_write_offset + sel_op_note_hash_exists)) = 0;
#[EMIT_NOTE_HASH_INC_CONSISTENCY_CHECK]
NOT_LAST * (emit_note_hash_write_offset' - (emit_note_hash_write_offset + main.sel_op_emit_note_hash)) = 0;
// if main.ib is set on op_nullifier_exists, then the nullifier_exists_write_offset will be incremented by 1, otherwise non_exists will be incremented
sel_execution_row * (emit_note_hash_write_offset' - (emit_note_hash_write_offset + sel_op_emit_note_hash)) = 0;

// if ib is set on op_nullifier_exists, then the nullifier_exists_write_offset
// will be incremented by 1, otherwise non_exists will be incremented.
#[NULLIFIER_EXISTS_INC_CONSISTENCY_CHECK]
NOT_LAST * (nullifier_exists_write_offset' - (nullifier_exists_write_offset + (main.sel_op_nullifier_exists * main.ib))) = 0;
sel_execution_row * (nullifier_exists_write_offset' - (nullifier_exists_write_offset + (sel_op_nullifier_exists * ib))) = 0;
#[NULLIFIER_NON_EXISTS_INC_CONSISTENCY_CHECK]
NOT_LAST * (nullifier_non_exists_write_offset' - (nullifier_non_exists_write_offset + (main.sel_op_nullifier_exists * (1 - main.ib)))) = 0;
sel_execution_row * (nullifier_non_exists_write_offset' - (nullifier_non_exists_write_offset + (sel_op_nullifier_exists * (1 - ib)))) = 0;

#[EMIT_NULLIFIER_INC_CONSISTENCY_CHECK]
NOT_LAST * (emit_nullifier_write_offset' - (emit_nullifier_write_offset + main.sel_op_emit_nullifier)) = 0;
sel_execution_row * (emit_nullifier_write_offset' - (emit_nullifier_write_offset + sel_op_emit_nullifier)) = 0;

#[L1_TO_L2_MSG_EXISTS_INC_CONSISTENCY_CHECK]
NOT_LAST * (l1_to_l2_msg_exists_write_offset' - (l1_to_l2_msg_exists_write_offset + main.sel_op_l1_to_l2_msg_exists)) = 0;
sel_execution_row * (l1_to_l2_msg_exists_write_offset' - (l1_to_l2_msg_exists_write_offset + sel_op_l1_to_l2_msg_exists)) = 0;

#[EMIT_UNENCRYPTED_LOG_INC_CONSISTENCY_CHECK]
NOT_LAST * (emit_unencrypted_log_write_offset' - (emit_unencrypted_log_write_offset + main.sel_op_emit_unencrypted_log)) = 0;
#[EMIT_L2_TO_L1_MSG_INC_CONSISTENCY_CHECK]
NOT_LAST * (emit_l2_to_l1_msg_write_offset' - (emit_l2_to_l1_msg_write_offset + main.sel_op_emit_l2_to_l1_msg)) = 0;
sel_execution_row * (emit_unencrypted_log_write_offset' - (emit_unencrypted_log_write_offset + sel_op_emit_unencrypted_log)) = 0;

#[EMIT_L2_TO_L1_MSG_INC_CONSISTENCY_CHECK]
sel_execution_row * (emit_l2_to_l1_msg_write_offset' - (emit_l2_to_l1_msg_write_offset + sel_op_emit_l2_to_l1_msg)) = 0;

#[SLOAD_INC_CONSISTENCY_CHECK]
NOT_LAST * (sload_write_offset' - (sload_write_offset + main.sel_op_sload)) = 0;
sel_execution_row * (sload_write_offset' - (sload_write_offset + sel_op_sload)) = 0;

#[SSTORE_INC_CONSISTENCY_CHECK]
NOT_LAST * (sstore_write_offset' - (sstore_write_offset + main.sel_op_sstore)) = 0;
sel_execution_row * (sstore_write_offset' - (sstore_write_offset + sel_op_sstore)) = 0;

//===== KERNEL INPUTS CONSTRAINTS ===========================================
// The general pattern for environment lookups is as follows:
// Each kernel opcode related to some fixed positions in the `public kernel_inputs` polynomial
// We can lookup into a fixed index of this polynomial by including constraints that force the value
// of kernel_in_offset to the value relevant to the given opcode that is active

// 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;

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

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

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

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

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

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

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

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

#[COINBASE_KERNEL]
sel_op_coinbase * (kernel_in_offset - constants.COINBASE_SELECTOR) = 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;

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

// OUTPUTS LOOKUPS
// Constrain the value of kernel_out_offset to be the correct offset for the operation being performed
#[NOTE_HASH_KERNEL_OUTPUT]
sel_op_note_hash_exists * (kernel_out_offset - (constants.START_NOTE_HASH_EXISTS_WRITE_OFFSET + note_hash_exist_write_offset)) = 0;
sel_first * note_hash_exist_write_offset = 0;

#[EMIT_NOTE_HASH_KERNEL_OUTPUT]
sel_op_emit_note_hash * (kernel_out_offset - (constants.START_EMIT_NOTE_HASH_WRITE_OFFSET + emit_note_hash_write_offset)) = 0;
sel_first * emit_note_hash_write_offset = 0;

#[NULLIFIER_EXISTS_KERNEL_OUTPUT]
sel_op_nullifier_exists * (kernel_out_offset - ((ib * (constants.START_NULLIFIER_EXISTS_OFFSET + nullifier_exists_write_offset)) + ((1 - ib) * (constants.START_NULLIFIER_NON_EXISTS_OFFSET + nullifier_non_exists_write_offset)))) = 0;
sel_first * nullifier_exists_write_offset = 0;
sel_first * nullifier_non_exists_write_offset = 0;

#[EMIT_NULLIFIER_KERNEL_OUTPUT]
sel_op_emit_nullifier * (kernel_out_offset - (constants.START_EMIT_NULLIFIER_WRITE_OFFSET + emit_nullifier_write_offset)) = 0;
sel_first * emit_nullifier_write_offset = 0;

#[L1_TO_L2_MSG_EXISTS_KERNEL_OUTPUT]
sel_op_l1_to_l2_msg_exists * (kernel_out_offset - (constants.START_L1_TO_L2_MSG_EXISTS_WRITE_OFFSET + l1_to_l2_msg_exists_write_offset)) = 0;
sel_first * l1_to_l2_msg_exists_write_offset = 0;

#[EMIT_UNENCRYPTED_LOG_KERNEL_OUTPUT]
sel_op_emit_unencrypted_log * (kernel_out_offset - (constants.START_EMIT_UNENCRYPTED_LOG_WRITE_OFFSET + emit_unencrypted_log_write_offset)) = 0;
sel_first * emit_unencrypted_log_write_offset = 0;

// TODO: Add the equivalent for GETCONTRACTINSTANCE?

#[EMIT_L2_TO_L1_MSGS_KERNEL_OUTPUT]
sel_op_emit_l2_to_l1_msg * (kernel_out_offset - (constants.START_EMIT_L2_TO_L1_MSG_WRITE_OFFSET + emit_l2_to_l1_msg_write_offset)) = 0;
sel_first * emit_l2_to_l1_msg_write_offset = 0;

#[SLOAD_KERNEL_OUTPUT]
sel_op_sload * (kernel_out_offset - (constants.START_SLOAD_WRITE_OFFSET + sload_write_offset)) = 0;
sel_first * sload_write_offset = 0;

#[SSTORE_KERNEL_OUTPUT]
sel_op_sstore * (kernel_out_offset - (constants.START_SSTORE_WRITE_OFFSET + sstore_write_offset)) = 0;
sel_first * sstore_write_offset = 0;

// When we encounter a state writing opcode
// We increment the side effect counter by 1
#[SIDE_EFFECT_COUNTER_INCREMENT]
KERNEL_OUTPUT_SELECTORS * (side_effect_counter' - (side_effect_counter + 1)) = 0;

//===== LOOKUPS INTO THE PUBLIC INPUTS ===========================================
pol KERNEL_INPUT_SELECTORS = sel_op_address + sel_op_storage_address + sel_op_sender
+ sel_op_function_selector + sel_op_transaction_fee + sel_op_chain_id
+ sel_op_version + sel_op_block_number + sel_op_coinbase + sel_op_timestamp
+ sel_op_fee_per_l2_gas + sel_op_fee_per_da_gas;
// Ensure that only one kernel lookup is active when the kernel_in_offset is active
#[KERNEL_INPUT_ACTIVE_CHECK]
KERNEL_INPUT_SELECTORS * (1 - sel_q_kernel_lookup) = 0;

pol KERNEL_OUTPUT_SELECTORS = sel_op_note_hash_exists + sel_op_emit_note_hash + sel_op_nullifier_exists
+ sel_op_emit_nullifier + sel_op_l1_to_l2_msg_exists + sel_op_emit_unencrypted_log
+ sel_op_emit_l2_to_l1_msg + sel_op_sload + sel_op_sstore;
#[KERNEL_OUTPUT_ACTIVE_CHECK]
KERNEL_OUTPUT_SELECTORS * (1 - sel_q_kernel_output_lookup) = 0;

#[KERNEL_OUTPUT_LOOKUP]
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 };
112 changes: 0 additions & 112 deletions barretenberg/cpp/pil/avm/main.pil
View file
Original file line number Diff line number Diff line change
Expand Up @@ -370,21 +370,6 @@ namespace main(256);
// This works in combination with op_fdiv_err * (sel_op_fdiv - 1) = 0;
// Drawback is the need to paralllelize the latter.

//===== KERNEL LOOKUPS =======================================================
pol KERNEL_INPUT_SELECTORS = sel_op_address + sel_op_storage_address + sel_op_sender
+ sel_op_function_selector + sel_op_transaction_fee + sel_op_chain_id
+ sel_op_version + sel_op_block_number + sel_op_coinbase + sel_op_timestamp
+ sel_op_fee_per_l2_gas + sel_op_fee_per_da_gas;
// Ensure that only one kernel lookup is active when the kernel_in_offset is active
#[KERNEL_INPUT_ACTIVE_CHECK]
KERNEL_INPUT_SELECTORS * (1 - sel_q_kernel_lookup) = 0;

pol KERNEL_OUTPUT_SELECTORS = sel_op_note_hash_exists + sel_op_emit_note_hash + sel_op_nullifier_exists
+ sel_op_emit_nullifier + sel_op_l1_to_l2_msg_exists + sel_op_emit_unencrypted_log
+ sel_op_emit_l2_to_l1_msg + sel_op_sload + sel_op_sstore;
#[KERNEL_OUTPUT_ACTIVE_CHECK]
KERNEL_OUTPUT_SELECTORS * (1 - sel_q_kernel_output_lookup) = 0;

//===== CONTROL FLOW =======================================================
// pol commit sel_halted;
// sel_halted * (1 - sel_halted) = 0;
Expand Down Expand Up @@ -517,97 +502,6 @@ namespace main(256);
#[DAGASLEFT]
sel_op_dagasleft * (ia - da_gas_remaining') = 0;

//===== KERNEL INPUTS CONSTRAINTS ===========================================
// The general pattern for environment lookups is as follows:
// Each kernel opcode related to some fixed positions in the `public kernel_inputs` polynomial
// We can lookup into a fixed index of this polynomial by including constraints that force the value
// of kernel_in_offset to the value relevant to the given opcode that is active

// CONTEXT - ENVIRONMENT
#[ADDRESS_KERNEL]
sel_op_address * (kernel.kernel_in_offset - constants.ADDRESS_SELECTOR) = 0;

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

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

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

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

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

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

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

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

#[COINBASE_KERNEL]
sel_op_coinbase * (kernel.kernel_in_offset - constants.COINBASE_SELECTOR) = 0;

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

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

// OUTPUTS LOOKUPS
// Constrain the value of kernel_out_offset to be the correct offset for the operation being performed
#[NOTE_HASH_KERNEL_OUTPUT]
sel_op_note_hash_exists * (kernel.kernel_out_offset - (constants.START_NOTE_HASH_EXISTS_WRITE_OFFSET + kernel.note_hash_exist_write_offset)) = 0;
sel_first * kernel.note_hash_exist_write_offset = 0;


#[EMIT_NOTE_HASH_KERNEL_OUTPUT]
sel_op_emit_note_hash * (kernel.kernel_out_offset - (constants.START_EMIT_NOTE_HASH_WRITE_OFFSET + kernel.emit_note_hash_write_offset)) = 0;
sel_first * kernel.emit_note_hash_write_offset = 0;

#[NULLIFIER_EXISTS_KERNEL_OUTPUT]
sel_op_nullifier_exists * (kernel.kernel_out_offset - ((ib * (constants.START_NULLIFIER_EXISTS_OFFSET + kernel.nullifier_exists_write_offset)) + ((1 - ib) * (constants.START_NULLIFIER_NON_EXISTS_OFFSET + kernel.nullifier_non_exists_write_offset)))) = 0;
sel_first * kernel.nullifier_exists_write_offset = 0;
sel_first * kernel.nullifier_non_exists_write_offset = 0;

#[EMIT_NULLIFIER_KERNEL_OUTPUT]
sel_op_emit_nullifier * (kernel.kernel_out_offset - (constants.START_EMIT_NULLIFIER_WRITE_OFFSET + kernel.emit_nullifier_write_offset)) = 0;
sel_first * kernel.emit_nullifier_write_offset = 0;

#[L1_TO_L2_MSG_EXISTS_KERNEL_OUTPUT]
sel_op_l1_to_l2_msg_exists * (kernel.kernel_out_offset - (constants.START_L1_TO_L2_MSG_EXISTS_WRITE_OFFSET + kernel.l1_to_l2_msg_exists_write_offset)) = 0;
sel_first * kernel.l1_to_l2_msg_exists_write_offset = 0;

#[EMIT_UNENCRYPTED_LOG_KERNEL_OUTPUT]
sel_op_emit_unencrypted_log * (kernel.kernel_out_offset - (constants.START_EMIT_UNENCRYPTED_LOG_WRITE_OFFSET + kernel.emit_unencrypted_log_write_offset)) = 0;
sel_first * kernel.emit_unencrypted_log_write_offset = 0;

// TODO: Add the equivalent for GETCONTRACTINSTANCE?

#[EMIT_L2_TO_L1_MSGS_KERNEL_OUTPUT]
sel_op_emit_l2_to_l1_msg * (kernel.kernel_out_offset - (constants.START_EMIT_L2_TO_L1_MSG_WRITE_OFFSET + kernel.emit_l2_to_l1_msg_write_offset)) = 0;
sel_first * kernel.emit_l2_to_l1_msg_write_offset = 0;

#[SLOAD_KERNEL_OUTPUT]
sel_op_sload * (kernel.kernel_out_offset - (constants.START_SLOAD_WRITE_OFFSET + kernel.sload_write_offset)) = 0;
sel_first * kernel.sload_write_offset = 0;

#[SSTORE_KERNEL_OUTPUT]
sel_op_sstore * (kernel.kernel_out_offset - (constants.START_SSTORE_WRITE_OFFSET + kernel.sstore_write_offset)) = 0;
sel_first * kernel.sstore_write_offset = 0;

// When we encounter a state writing opcode
// We increment the side effect counter by 1
KERNEL_OUTPUT_SELECTORS * (kernel.side_effect_counter' - (kernel.side_effect_counter + 1)) = 0;

//===== Memory Slice Constraints ============================================
pol commit sel_slice_gadget; // Selector to activate a slice gadget operation in the gadget (#[PERM_MAIN_SLICE]).

Expand All @@ -616,12 +510,6 @@ namespace main(256);

//====== Inter-table Constraints ============================================

#[KERNEL_OUTPUT_LOOKUP]
sel_q_kernel_output_lookup {kernel.kernel_out_offset, ia, kernel.side_effect_counter, ib} in kernel.q_public_input_kernel_out_add_to_table {clk, kernel.kernel_value_out, kernel.kernel_side_effect_out, kernel.kernel_metadata_out};

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

#[INCL_MAIN_TAG_ERR]
mem.tag_err {mem.clk} in tag_err {clk};

Expand Down
Loading

0 comments on commit d7edd24

Please sign in to comment.