Skip to content

refactor(avm): kernel trace and finalization #8049

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

Merged
fcarreiro merged 1 commit into from
Aug 19, 2024
Merged

refactor(avm): kernel trace and finalization #8049

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
3 changes: 2 additions & 1 deletion barretenberg/cpp/pil/avm/gas.pil
View file
Open in desktop
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
Open in desktop
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
Open in desktop
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