diff --git a/CHANGELOG.md b/CHANGELOG.md index aef584236b..271e4910b2 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -38,6 +38,7 @@ - [BREAKING] Changed note metadata version 1 to encode as `1`, leaving encoded version `0` invalid. - Documented the `miden::protocol::account_id` module in the protocol library docs ([#2607](https://github.com/0xMiden/protocol/issues/2607)). - Added a skeleton batch kernel program with the public input/output contract from issue [#1122](https://github.com/0xMiden/protocol/issues/1122), wired through `LocalBatchProver::prove` and attached to `ProvenBatch` as an `ExecutionProof`. The kernel does not yet perform any verification; the verification chain that fills in the real outputs will land in a follow-up PR. +- Added the batch kernel's verification chain: each transaction is reconstructed from the advice provider, anchored in `TRANSACTIONS_COMMITMENT`, and the per-tx note commitments are absorbed into the batch's `INPUT_NOTES_COMMITMENT` / `OUTPUT_NOTES_COMMITMENT` outputs. `LocalBatchProver::prove` now also cross-checks the kernel's `batch_expiration_block_num` against the proposed batch. ### Fixes diff --git a/crates/miden-protocol/asm/kernels/batch/lib/memory.masm b/crates/miden-protocol/asm/kernels/batch/lib/memory.masm new file mode 100644 index 0000000000..6c68c1d3b7 --- /dev/null +++ b/crates/miden-protocol/asm/kernels/batch/lib/memory.masm @@ -0,0 +1,233 @@ +# MEMORY LAYOUT +# ================================================================================================= +# +# Below is the memory layout used by the batch kernel: +# +# +-------------------+-------------------------+----------------------------------+ +# | Address range | Constant | Contents | +# +-------------------+-------------------------+----------------------------------+ +# | 0 | NUM_TRANSACTIONS_PTR | num_transactions (1 felt). | +# | 1 | BATCH_EXPIRATION_PTR | batch_expiration_block_num. | +# | 4..8 | BATCH_HASHER_RATE0_PTR | RATE0 of the batch-level | +# | | | poseidon2 hasher state. | +# | 8..12 | BATCH_HASHER_RATE1_PTR | RATE1 of the batch-level hasher. | +# | 12..16 | BATCH_HASHER_CAP_PTR | CAPACITY of the batch-level | +# | | | hasher. | +# | 16 | SCRATCH_WORDS_COUNT_PTR | num_words piped into | +# | | | TX_NOTES_SCRATCH_PTR for the | +# | | | current transaction. | +# | 17 | SCRATCH_WORD_INDEX_PTR | current iteration cursor for the | +# | | | scratch absorption loop. | +# | 20..8212 | TX_TUPLES_PTR | Layer 1 piped data: per | +# | | | transaction `[tx_id[4], | +# | | | account_id_prefix, | +# | | | account_id_suffix, 0, 0]` | +# | | | (8 felts each, sized for up to | +# | | | 1024 transactions). | +# | 8212..32788 | TX_HEADERS_PTR | Layer 2 piped data: per | +# | | | transaction the felt sequence | +# | | | TransactionId::new hashes | +# | | | (24 felts each, sized for up to | +# | | | 1024 transactions). | +# | 32788..40980 | TX_NOTES_SCRATCH_PTR | Per-transaction scratch space | +# | | | for Layer 3 / Layer 3' note | +# | | | data (overwritten each tx). | +# +-------------------+-------------------------+----------------------------------+ + +# BOOK KEEPING +# ================================================================================================= + +#! Single-felt slot holding `num_transactions` after Layer 1 verification. +const NUM_TRANSACTIONS_PTR=0 + +#! Single-felt slot holding the running min of all transactions' +#! `expiration_block_num`, initialised to `u32::MAX`. +const BATCH_EXPIRATION_PTR=1 + +# BATCH HASHER STATE +# ================================================================================================= + +#! Word holding the RATE0 portion of the batch-level poseidon2 hasher state. +const BATCH_HASHER_RATE0_PTR=4 + +#! Word holding the RATE1 portion of the batch-level poseidon2 hasher state. +const BATCH_HASHER_RATE1_PTR=8 + +#! Word holding the CAPACITY portion of the batch-level poseidon2 hasher state. +const BATCH_HASHER_CAP_PTR=12 + +# SCRATCH BOOKKEEPING +# ================================================================================================= + +#! Number of words piped into TX_NOTES_SCRATCH_PTR for the transaction whose Layer 3 / 3' is +#! being absorbed. +const SCRATCH_WORDS_COUNT_PTR=16 + +#! Iteration cursor (index in words) into TX_NOTES_SCRATCH_PTR for the absorption loop. +const SCRATCH_WORD_INDEX_PTR=17 + +# PIPED DATA REGIONS +# ================================================================================================= + +#! Base of the Layer 1 piped data region. Per transaction, 8 felts: +#! `[tx_id[4], account_id_prefix, account_id_suffix, 0, 0]`. +const TX_TUPLES_PTR=20 + +#! Number of felts each transaction occupies in TX_TUPLES_PTR. +const TX_TUPLE_FELT_LEN=8 + +#! Base of the Layer 2 piped data region. Per transaction, 24 felts: +#! `[INIT[4], FINAL[4], INPUT_NOTES_COMMITMENT[4], OUTPUT_NOTES_COMMITMENT[4], FEE_ASSET[8]]`. +#! This must match the felt-sequence layout of `TransactionId::new`. +const TX_HEADERS_PTR=8212 + +#! Number of felts each transaction occupies in TX_HEADERS_PTR. +const TX_HEADER_FELT_LEN=24 + +#! Felt offset within a transaction header where INPUT_NOTES_COMMITMENT starts. +const TX_HEADER_INPUT_NOTES_OFFSET=8 + +#! Felt offset within a transaction header where OUTPUT_NOTES_COMMITMENT starts. +const TX_HEADER_OUTPUT_NOTES_OFFSET=12 + +#! Per-transaction scratch space for Layer 3 / 3' note data, overwritten between iterations. +const TX_NOTES_SCRATCH_PTR=32788 + +# NUM TRANSACTIONS +# ================================================================================================= + +#! Stores `num_transactions`. +#! +#! Inputs: [num_transactions] +#! Outputs: [] +pub proc set_num_transactions + mem_store.NUM_TRANSACTIONS_PTR +end + +#! Returns `num_transactions`. +#! +#! Inputs: [] +#! Outputs: [num_transactions] +pub proc get_num_transactions + mem_load.NUM_TRANSACTIONS_PTR +end + +# BATCH EXPIRATION BLOCK NUM +# ================================================================================================= + +#! Stores `batch_expiration_block_num`. +#! +#! Inputs: [batch_expiration_block_num] +#! Outputs: [] +pub proc set_batch_expiration_block_num + mem_store.BATCH_EXPIRATION_PTR +end + +#! Returns `batch_expiration_block_num`. +#! +#! Inputs: [] +#! Outputs: [batch_expiration_block_num] +pub proc get_batch_expiration_block_num + mem_load.BATCH_EXPIRATION_PTR +end + +# BATCH HASHER STATE +# ================================================================================================= + +#! Persists the batch hasher state from the operand stack into memory. +#! +#! Inputs: [RATE0, RATE1, CAPACITY] +#! Outputs: [] +pub proc save_batch_hasher_state + mem_storew_le.BATCH_HASHER_RATE0_PTR dropw + mem_storew_le.BATCH_HASHER_RATE1_PTR dropw + mem_storew_le.BATCH_HASHER_CAP_PTR dropw +end + +#! Loads the batch hasher state from memory onto the operand stack. +#! +#! Inputs: [] +#! Outputs: [RATE0, RATE1, CAPACITY] +pub proc load_batch_hasher_state + padw mem_loadw_le.BATCH_HASHER_CAP_PTR + padw mem_loadw_le.BATCH_HASHER_RATE1_PTR + padw mem_loadw_le.BATCH_HASHER_RATE0_PTR +end + +# SCRATCH BOOKKEEPING +# ================================================================================================= + +#! Stores the count (in words) of data piped into the per-transaction scratch. +#! +#! Inputs: [num_words] +#! Outputs: [] +pub proc set_scratch_words_count + mem_store.SCRATCH_WORDS_COUNT_PTR +end + +#! Returns the count (in words) of data piped into the per-transaction scratch. +#! +#! Inputs: [] +#! Outputs: [num_words] +pub proc get_scratch_words_count + mem_load.SCRATCH_WORDS_COUNT_PTR +end + +#! Stores the absorption iteration cursor (index in words). +#! +#! Inputs: [word_index] +#! Outputs: [] +pub proc set_scratch_word_index + mem_store.SCRATCH_WORD_INDEX_PTR +end + +#! Returns the absorption iteration cursor (index in words). +#! +#! Inputs: [] +#! Outputs: [word_index] +pub proc get_scratch_word_index + mem_load.SCRATCH_WORD_INDEX_PTR +end + +# TRANSACTION TUPLE / HEADER ACCESSORS +# ================================================================================================= + +#! Returns a pointer to transaction `tx_index`'s entry in TX_TUPLES_PTR. +#! +#! Inputs: [tx_index] +#! Outputs: [tx_tuple_ptr] +pub proc tx_tuple_ptr + mul.TX_TUPLE_FELT_LEN add.TX_TUPLES_PTR +end + +#! Returns the verified `tx_id` for transaction `tx_index` (loaded from TX_TUPLES_PTR). +#! +#! Inputs: [tx_index] +#! Outputs: [TX_ID] +pub proc get_tx_id + exec.tx_tuple_ptr padw movup.4 mem_loadw_le +end + +#! Returns a pointer to transaction `tx_index`'s entry in TX_HEADERS_PTR. +#! +#! Inputs: [tx_index] +#! Outputs: [tx_header_ptr] +pub proc tx_header_ptr + mul.TX_HEADER_FELT_LEN add.TX_HEADERS_PTR +end + +#! Returns the verified per-transaction INPUT_NOTES_COMMITMENT for transaction `tx_index`. +#! +#! Inputs: [tx_index] +#! Outputs: [INPUT_NOTES_COMMITMENT_i] +pub proc get_tx_input_notes_commitment + exec.tx_header_ptr add.TX_HEADER_INPUT_NOTES_OFFSET padw movup.4 mem_loadw_le +end + +#! Returns the verified per-transaction OUTPUT_NOTES_COMMITMENT for transaction `tx_index`. +#! +#! Inputs: [tx_index] +#! Outputs: [OUTPUT_NOTES_COMMITMENT_i] +pub proc get_tx_output_notes_commitment + exec.tx_header_ptr add.TX_HEADER_OUTPUT_NOTES_OFFSET padw movup.4 mem_loadw_le +end diff --git a/crates/miden-protocol/asm/kernels/batch/lib/note_tracker.masm b/crates/miden-protocol/asm/kernels/batch/lib/note_tracker.masm new file mode 100644 index 0000000000..4e6ca8b86b --- /dev/null +++ b/crates/miden-protocol/asm/kernels/batch/lib/note_tracker.masm @@ -0,0 +1,244 @@ +use miden::core::mem +use miden::core::crypto::hashes::poseidon2 +use miden::core::word + +use miden::batch_kernel::memory +use miden::batch_kernel::memory::TX_NOTES_SCRATCH_PTR + +# ERRORS +# ================================================================================================= + +const ERR_BATCH_INPUT_NOTES_MISMATCH="per-transaction input notes data piped from the advice map does not match its INPUT_NOTES_COMMITMENT" + +const ERR_BATCH_OUTPUT_NOTES_MISMATCH="per-transaction output notes data piped from the advice map does not match its OUTPUT_NOTES_COMMITMENT" + +# ABSORPTION HELPER +# ================================================================================================= + +#! Absorbs the contents of [`memory::TX_NOTES_SCRATCH_PTR`] into the batch hasher state held in +#! [`memory::BATCH_HASHER_*_PTR`] memory slots. +#! +#! The scratch region is read as `(NULL_OR_NOTE_ID, COMMIT_OR_METADATA)` 8-felt tuples, in the +#! order they were piped (which matches `build_input_note_commitment` / +#! `OutputNotes::compute_commitment` in Rust). +#! +#! The number of words to absorb is read from [`memory::SCRATCH_WORDS_COUNT_PTR`]. +#! +#! Inputs: [] +#! Outputs: [] +proc absorb_scratch_into_batch_hasher + push.0 exec.memory::set_scratch_word_index + + exec.memory::load_batch_hasher_state + # Stack: [RATE0, RATE1, CAPACITY] + + exec.memory::get_scratch_word_index + exec.memory::get_scratch_words_count + u32lt + # Stack: [should_loop, RATE0, RATE1, CAPACITY] + + while.true + exec.memory::get_scratch_word_index + mul.4 add.TX_NOTES_SCRATCH_PTR + # Stack: [scratch_ptr, RATE0, RATE1, CAPACITY] + + padw dup.4 mem_loadw_le + # Stack: [DATA1, scratch_ptr, RATE0, RATE1, CAPACITY] + + padw dup.8 add.4 mem_loadw_le + # Stack: [DATA2, DATA1, scratch_ptr, RATE0, RATE1, CAPACITY] + + movup.8 drop + # Stack: [DATA2, DATA1, RATE0, RATE1, CAPACITY] + + # Replace RATE0 + RATE1 with DATA1 + DATA2 (DATA1 first, DATA2 second), then permute. + swapdw + dropw dropw + swapw + exec.poseidon2::permute + # Stack: [RATE0', RATE1', CAPACITY'] + + exec.memory::get_scratch_word_index add.2 exec.memory::set_scratch_word_index + exec.memory::get_scratch_word_index + exec.memory::get_scratch_words_count + u32lt + # Stack: [should_loop, RATE0, RATE1, CAPACITY] + end + + exec.memory::save_batch_hasher_state +end + +# COMMON SHAPE +# ================================================================================================= +# +# Both `compute_input_notes_commitment` and `compute_output_notes_commitment` follow the same +# four-step pattern, parametrised by which per-tx commitment the caller fetches from +# `TX_HEADERS_PTR`: +# +# 1. Init the batch hasher state in memory. +# 2. For each transaction: +# - Read the per-tx commitment from the verified TX_HEADERS region. +# - If it is `Word::empty()`, skip (the per-tx note list is empty). +# - Otherwise, pipe the advice-map value keyed by that commitment into TX_NOTES_SCRATCH_PTR +# and `assert_eqw` against the commitment. +# - Absorb the verified scratch contents into the batch hasher state. +# 3. Squeeze the final digest out of the batch hasher state. +# 4. Return the digest on the operand stack. + +# INPUT NOTES COMMITMENT +# ================================================================================================= + +#! Computes the batch's INPUT_NOTES_COMMITMENT. +#! +#! For each transaction in transaction order, verifies the per-transaction +#! `INPUT_NOTES_COMMITMENT_i` against its advice-map value (the `(NULLIFIER, EMPTY_OR_COMMITMENT)` +#! tuple list), then absorbs that verified data into the batch-level sequential hasher. +#! +#! Inputs: [] +#! Outputs: [INPUT_NOTES_COMMITMENT] +#! +#! Errors: +#! - ERR_BATCH_INPUT_NOTES_MISMATCH: a transaction's `(NULLIFIER, EMPTY_OR_COMMITMENT)` tuple +#! list piped from the advice map does not hash to its verified per-tx +#! `INPUT_NOTES_COMMITMENT_i`. +#! +#! TODO: erase intra-batch unauthenticated notes from the absorbed sequence (see +#! `InputOutputNoteTracker::from_transactions`). +#! TODO: re-sort + dedupe by nullifier so the result equals +#! `proposed_batch.input_notes().commitment()`. +#! TODO: authenticate unauthenticated input notes against `BLOCK_HASH`'s chain MMR. +#! TODO: enforce `MAX_INPUT_NOTES_PER_BATCH`. +pub proc compute_input_notes_commitment + exec.poseidon2::init_no_padding + exec.memory::save_batch_hasher_state + + exec.memory::get_num_transactions + push.0 + # Stack: [tx_index, num_transactions] + + dup.1 dup.1 neq + # Stack: [should_loop, tx_index, num_transactions] + + while.true + dup exec.memory::get_tx_input_notes_commitment + # Stack: [INPUT_NOTES_COMMITMENT_i, tx_index, num_transactions] + + dupw exec.word::eqz + # Stack: [is_empty, INPUT_NOTES_COMMITMENT_i, tx_index, num_transactions] + + if.true + dropw + else + push.TX_NOTES_SCRATCH_PTR movdn.4 + # Stack: [INPUT_NOTES_COMMITMENT_i, TX_NOTES_SCRATCH_PTR, tx_index, num_transactions] + + adv.push_mapvaln + adv_push.1 div.4 + # Stack: [num_words, INPUT_NOTES_COMMITMENT_i, TX_NOTES_SCRATCH_PTR, tx_index, num_transactions] + + dup exec.memory::set_scratch_words_count + + movup.5 swap + # Stack: [num_words, TX_NOTES_SCRATCH_PTR, INPUT_NOTES_COMMITMENT_i, tx_index, num_transactions] + + exec.mem::pipe_words_to_memory + exec.poseidon2::squeeze_digest + movup.4 drop + # Stack: [DIGEST, INPUT_NOTES_COMMITMENT_i, tx_index, num_transactions] + + assert_eqw.err=ERR_BATCH_INPUT_NOTES_MISMATCH + + exec.absorb_scratch_into_batch_hasher + end + # Stack: [tx_index, num_transactions] + + add.1 + dup.1 dup.1 neq + # Stack: [should_loop, tx_index, num_transactions] + end + + drop drop + + exec.memory::load_batch_hasher_state + exec.poseidon2::squeeze_digest + # Stack: [INPUT_NOTES_COMMITMENT] +end + +# OUTPUT NOTES COMMITMENT +# ================================================================================================= + +#! Computes the batch's OUTPUT_NOTES_COMMITMENT. +#! +#! For each transaction in transaction order, verifies the per-transaction +#! `OUTPUT_NOTES_COMMITMENT_i` against its advice-map value (the `(NOTE_ID, METADATA_COMMITMENT)` +#! tuple list), then absorbs that verified data into the batch-level sequential hasher. +#! +#! Inputs: [] +#! Outputs: [OUTPUT_NOTES_COMMITMENT] +#! +#! Errors: +#! - ERR_BATCH_OUTPUT_NOTES_MISMATCH: a transaction's `(NOTE_ID, METADATA_COMMITMENT)` tuple +#! list piped from the advice map does not hash to its verified per-tx +#! `OUTPUT_NOTES_COMMITMENT_i`. +#! +#! TODO: erase intra-batch unauthenticated notes from the absorbed sequence. +#! TODO: switch the output to `BatchNoteTree::root` (an SMT root rather than this sequential +#! hash). +#! TODO: enforce `MAX_OUTPUT_NOTES_PER_BATCH`. +pub proc compute_output_notes_commitment + # Stack: [] + + exec.poseidon2::init_no_padding + exec.memory::save_batch_hasher_state + + exec.memory::get_num_transactions + push.0 + # Stack: [tx_index, num_transactions] + + dup.1 dup.1 neq + # Stack: [should_loop, tx_index, num_transactions] + + while.true + dup exec.memory::get_tx_output_notes_commitment + # Stack: [OUTPUT_NOTES_COMMITMENT_i, tx_index, num_transactions] + + dupw exec.word::eqz + # Stack: [is_empty, OUTPUT_NOTES_COMMITMENT_i, tx_index, num_transactions] + + if.true + dropw + else + push.TX_NOTES_SCRATCH_PTR movdn.4 + # Stack: [OUTPUT_NOTES_COMMITMENT_i, TX_NOTES_SCRATCH_PTR, tx_index, num_transactions] + + adv.push_mapvaln + adv_push.1 div.4 + # Stack: [num_words, OUTPUT_NOTES_COMMITMENT_i, TX_NOTES_SCRATCH_PTR, tx_index, num_transactions] + + dup exec.memory::set_scratch_words_count + + movup.5 swap + # Stack: [num_words, TX_NOTES_SCRATCH_PTR, OUTPUT_NOTES_COMMITMENT_i, tx_index, num_transactions] + + exec.mem::pipe_words_to_memory + exec.poseidon2::squeeze_digest + movup.4 drop + # Stack: [DIGEST, OUTPUT_NOTES_COMMITMENT_i, tx_index, num_transactions] + + assert_eqw.err=ERR_BATCH_OUTPUT_NOTES_MISMATCH + # Stack: [tx_index, num_transactions] + + exec.absorb_scratch_into_batch_hasher + end + + add.1 + dup.1 dup.1 neq + # Stack: [should_loop, tx_index, num_transactions] + end + + drop drop + + exec.memory::load_batch_hasher_state + exec.poseidon2::squeeze_digest + # Stack: [OUTPUT_NOTES_COMMITMENT] +end diff --git a/crates/miden-protocol/asm/kernels/batch/lib/prologue.masm b/crates/miden-protocol/asm/kernels/batch/lib/prologue.masm new file mode 100644 index 0000000000..af1f330146 --- /dev/null +++ b/crates/miden-protocol/asm/kernels/batch/lib/prologue.masm @@ -0,0 +1,149 @@ +use miden::core::mem +use miden::core::crypto::hashes::poseidon2 + +use miden::batch_kernel::memory +use miden::batch_kernel::memory::TX_TUPLES_PTR + +# CONSTS +# ================================================================================================= + +#! Maximum value of `batch_expiration_block_num`, used as the running-min initialiser. +const MAX_BLOCK_NUM=0xFFFFFFFF + +# ERRORS +# ================================================================================================= + +const ERR_BATCH_TRANSACTIONS_COMMITMENT_MISMATCH="batch transactions commitment piped from the advice map does not match the public input" + +const ERR_BATCH_TRANSACTION_HEADER_MISMATCH="transaction header data piped from the advice map does not match its tx_id" + +# PROLOGUE +# ================================================================================================= + +#! Loads and verifies the batch's structural commitments and tracks the smallest +#! `expiration_block_num` across all transactions in [`memory::BATCH_EXPIRATION_PTR`]. +#! +#! Performs three steps: +#! - Layer 1: pipes the `(tx_id, account_id)` tuples from the advice map keyed by +#! `TRANSACTIONS_COMMITMENT` into [`memory::TX_TUPLES_PTR`], asserting that the sequential hash of +#! the piped data matches `TRANSACTIONS_COMMITMENT`. The number of transactions is derived from +#! the piped length and stored in [`memory::NUM_TRANSACTIONS_PTR`]. +#! - Layer 2: for each transaction, pipes the felt sequence hashed by `TransactionId::new` from the +#! advice map keyed by the verified `tx_id`, asserting that the sequential hash matches the +#! `tx_id`. Each transaction's data is written into [`memory::TX_HEADERS_PTR`] at the appropriate +#! per-tx offset. +#! - For each transaction, pops the `expiration_block_num` from the advice stack and updates the +#! running minimum in [`memory::BATCH_EXPIRATION_PTR`]. +#! +#! Inputs: +#! Operand stack: [TRANSACTIONS_COMMITMENT] +#! Advice map: +#! TRANSACTIONS_COMMITMENT |-> [(tx_id_0, account_id_0_pair), (tx_id_1, account_id_1_pair), ...] +#! For each verified tx_id_i: +#! tx_id_i |-> [INIT_i, FINAL_i, INPUT_NOTES_COMMITMENT_i, OUTPUT_NOTES_COMMITMENT_i, +#! FEE_ASSET_i] +#! Advice stack: [expiration_block_num_0, expiration_block_num_1, ...] +#! +#! Outputs: +#! Operand stack: [] +#! +#! Errors: +#! - ERR_BATCH_TRANSACTIONS_COMMITMENT_MISMATCH: the `(tx_id, account_id)` tuple list piped from +#! the advice map does not hash to `TRANSACTIONS_COMMITMENT`. +#! - ERR_BATCH_TRANSACTION_HEADER_MISMATCH: a transaction's +#! `(INIT, FINAL, INPUT_NOTES_COMMITMENT, OUTPUT_NOTES_COMMITMENT, FEE_ASSET)` data piped from +#! the advice map does not hash to its `tx_id`. +#! +#! TODO: verify that each transaction's reference block is contained in the chain MMR rooted at +#! BLOCK_HASH. +#! TODO: verify that the partial-blockchain peaks hash matches the block header's chain commitment. +#! TODO: assert each `expiration_block_num_i > reference_block_num`. +#! TODO: verify each `expiration_block_num_i` is part of tx_i's verified ExecutionProof public +#! outputs. +pub proc prepare_batch + # Layer 1: pipe TRANSACTIONS_COMMITMENT's mapped value to TX_TUPLES_PTR + verify. + # --------------------------------------------------------------------------------------------- + + # Stack: [TRANSACTIONS_COMMITMENT] + push.TX_TUPLES_PTR movdn.4 + # Stack: [TRANSACTIONS_COMMITMENT, TX_TUPLES_PTR] + + adv.push_mapvaln + # AS: [len_felts, data...] + + adv_push.1 div.4 + # Stack: [num_words, TRANSACTIONS_COMMITMENT, TX_TUPLES_PTR] + + # num_transactions = num_words / 2 (each tx contributes 2 words: tx_id + account_id_pair). + dup div.2 exec.memory::set_num_transactions + + movup.5 swap + # Stack: [num_words, TX_TUPLES_PTR, TRANSACTIONS_COMMITMENT] + + exec.mem::pipe_words_to_memory + # Stack: [C, B, A, end_ptr, TRANSACTIONS_COMMITMENT] + + exec.poseidon2::squeeze_digest + movup.4 drop + # Stack: [DIGEST, TRANSACTIONS_COMMITMENT] + + assert_eqw.err=ERR_BATCH_TRANSACTIONS_COMMITMENT_MISMATCH + + # Initialise batch_expiration_block_num to u32::MAX. + # --------------------------------------------------------------------------------------------- + + push.MAX_BLOCK_NUM exec.memory::set_batch_expiration_block_num + + # Layer 2: for each transaction, pipe + verify its header, accumulate expiration min. + # --------------------------------------------------------------------------------------------- + + exec.memory::get_num_transactions + push.0 + # Stack: [tx_index, num_transactions] + + dup.1 dup.1 neq + # Stack: [should_loop, tx_index, num_transactions] + + while.true + dup exec.memory::get_tx_id + # Stack: [TX_ID, tx_index, num_transactions] + + dup.4 exec.memory::tx_header_ptr movdn.4 + # Stack: [TX_ID, tx_header_ptr, tx_index, num_transactions] + + adv.push_mapvaln + adv_push.1 div.4 + # Stack: [num_words, TX_ID, tx_header_ptr, tx_index, num_transactions] + + movup.5 swap + # Stack: [num_words, tx_header_ptr, TX_ID, tx_index, num_transactions] + + exec.mem::pipe_words_to_memory + exec.poseidon2::squeeze_digest + movup.4 drop + # Stack: [DIGEST, TX_ID, tx_index, num_transactions] + + assert_eqw.err=ERR_BATCH_TRANSACTION_HEADER_MISMATCH + + adv_push.1 + # Stack: [expiration, tx_index, num_transactions] + + dup exec.memory::get_batch_expiration_block_num + # Stack: [current_min, expiration, expiration, tx_index, num_transactions] + + u32lt + + if.true + exec.memory::set_batch_expiration_block_num + else + drop + end + # Stack: [tx_index, num_transactions] + + add.1 + dup.1 dup.1 neq + # Stack: [should_loop, tx_index, num_transactions] + end + + drop drop +end diff --git a/crates/miden-protocol/asm/kernels/batch/main.masm b/crates/miden-protocol/asm/kernels/batch/main.masm index 89e70417be..70bcb7e5df 100644 --- a/crates/miden-protocol/asm/kernels/batch/main.masm +++ b/crates/miden-protocol/asm/kernels/batch/main.masm @@ -1,18 +1,34 @@ +use miden::batch_kernel::memory +use miden::batch_kernel::note_tracker +use miden::batch_kernel::prologue + # MAIN # ================================================================================================= -#! Batch kernel program (skeleton). +#! Batch kernel program. #! #! A transaction batch groups a set of independently-proven transactions so they can later be -#! aggregated into a block by the block kernel. This program defines the public input/output -#! contract that the batch kernel will eventually verify, but does not yet perform any -#! verification: it drops its inputs and exits, leaving the all-zero word output region as the -#! stack's initial padding zeros. +#! aggregated into a block by the block kernel. This program: +#! +#! 1. Reconstructs the per-transaction data (account state transitions, input/output notes, fee, +#! expiration) from the advice provider, anchoring the entire reconstruction in the public +#! `TRANSACTIONS_COMMITMENT`. +#! 2. Aggregates the per-transaction data into batch-wide commitments — one over the consumed +#! input notes, one over the produced output notes, plus the batch's effective expiration +#! block number — that the block kernel will later consume. +#! +#! Reconstruction is a recursive unhashing chain. Each layer of advice data is keyed by a hash +#! that the previous layer's verification produced, so once `TRANSACTIONS_COMMITMENT` is anchored +#! to the public input, every byte that feeds the batch outputs is transitively committed-to: #! -#! Splitting the kernel into "shape only" and "verification" lets downstream Rust tooling -#! (`BatchKernel`'s input/advice/output builders, `LocalBatchProver::prove`, the `ProvenBatch` -#! proof field) be built and reviewed against a stable interface before the verification logic -#! lands. The verification chain that fills in the real outputs is added in a follow-up PR. +#! `TRANSACTIONS_COMMITMENT` (public input) -> `(tx_id, account_id)` tuple list +#! each `tx_id` -> per-tx +#! `(INIT, FINAL, INPUT_NOTES_COMMITMENT_i, OUTPUT_NOTES_COMMITMENT_i, FEE_ASSET)` +#! each `INPUT_NOTES_COMMITMENT_i` -> `(NULLIFIER, EMPTY_OR_COMMITMENT)` tuples +#! each `OUTPUT_NOTES_COMMITMENT_i` -> `(NOTE_ID, METADATA_COMMITMENT)` tuples +#! +#! Each layer is loaded via `adv.push_mapvaln` keyed by the previously-verified hash and asserted +#! against that hash via `assert_eqw`. Only verified data feeds into the batch outputs. #! #! Inputs: [ #! TRANSACTIONS_COMMITMENT, @@ -28,24 +44,54 @@ #! ] #! #! Where: -#! - TRANSACTIONS_COMMITMENT is the sequential hash of the `(tx_id, account_id)` tuples -#! committing to the transactions in the batch (i.e. the `BatchId` value). +#! - TRANSACTIONS_COMMITMENT is the sequential hash of the `(tx_id, account_id)` tuples committing +#! to the transactions in the batch (i.e. the `BatchId` value). #! - BLOCK_HASH is the commitment of the batch's reference block. -#! - INPUT_NOTES_COMMITMENT will be the sequential hash over every transaction's input note -#! commitments. In this skeleton it is the empty word. -#! - OUTPUT_NOTES_COMMITMENT will be the sequential hash over every transaction's output note -#! commitments. In this skeleton it is the empty word. -#! - batch_expiration_block_num will be the minimum of every transaction's -#! `expiration_block_num`. In this skeleton it is zero. -#! -#! TODO: replace this skeleton with the verification chain that reconstructs every transaction -#! from the advice provider, anchors the reconstruction in `TRANSACTIONS_COMMITMENT`, and -#! emits the real batch commitments and expiration. +#! - INPUT_NOTES_COMMITMENT is the sequential hash over every transaction's verified +#! `(NULLIFIER, EMPTY_OR_COMMITMENT)` tuples in transaction order. +#! - OUTPUT_NOTES_COMMITMENT is the sequential hash over every transaction's verified +#! `(NOTE_ID, METADATA_COMMITMENT)` tuples in transaction order. +#! - batch_expiration_block_num is the minimum of every transaction's `expiration_block_num`. +#! +#! TODO: verify BLOCK_HASH against block header data via the same pipe-and-verify pattern. +#! TODO: authenticate unauthenticated input notes against BLOCK_HASH's chain MMR. +#! TODO: verify each transaction's reference block is contained in the chain MMR rooted at +#! BLOCK_HASH. +#! TODO: aggregate per-account updates and emit a separate ACCOUNT_UPDATES_COMMITMENT output. +#! TODO: erase intra-batch unauthenticated notes from INPUT_NOTES_COMMITMENT and the output set. +#! TODO: recursively verify each transaction's `ExecutionProof`. +#! TODO: switch OUTPUT_NOTES_COMMITMENT to the `BatchNoteTree` SMT root. +#! TODO: assert `batch_expiration_block_num > reference_block_num`. +#! TODO: enforce `MAX_INPUT_NOTES_PER_BATCH`, `MAX_OUTPUT_NOTES_PER_BATCH`, +#! `MAX_ACCOUNTS_PER_BATCH`. +#! TODO: derive `batch_expiration_block_num` from data committed-to in the verified chain rather +#! than from the unverified advice stack. proc main - # Drop TRANSACTIONS_COMMITMENT and BLOCK_HASH. The VM keeps the stack at depth >= 16, so the - # remaining 8 felts (the explicit `pad(8)` inputs) plus 8 zeros auto-filled below them form - # the all-zero 16-felt output region. - dropw dropw + # TODO: verify BLOCK_HASH against block header data via the pipe-and-verify pattern. + swapw dropw + # Stack: [TRANSACTIONS_COMMITMENT] + + exec.prologue::prepare_batch + # Stack: [] + + exec.note_tracker::compute_input_notes_commitment + # Stack: [INPUT_NOTES_COMMITMENT] + + exec.note_tracker::compute_output_notes_commitment + # Stack: [OUTPUT_NOTES_COMMITMENT, INPUT_NOTES_COMMITMENT] + + exec.memory::get_batch_expiration_block_num + # Stack: [batch_expiration_block_num, OUTPUT_NOTES_COMMITMENT, INPUT_NOTES_COMMITMENT] + + # Push the expiration felt past both commitment words so the words land word-aligned. + movdn.8 + swapw + # Stack: [INPUT_NOTES_COMMITMENT, OUTPUT_NOTES_COMMITMENT, batch_expiration_block_num] + + # Drop the leftover words below the output region. The kernel's earlier `consume`-only + # operations don't reduce stack depth below the 16-felt floor, so by this point the depth + # has grown above 16 and we need to bring it back down. + repeat.3 movupw.3 dropw end end begin diff --git a/crates/miden-protocol/build.rs b/crates/miden-protocol/build.rs index 6d45f6cdec..642504d6e6 100644 --- a/crates/miden-protocol/build.rs +++ b/crates/miden-protocol/build.rs @@ -23,6 +23,7 @@ const ASM_TX_KERNEL_DIR: &str = "kernels/transaction"; const ASM_BATCH_KERNEL_DIR: &str = "kernels/batch"; const PROTOCOL_LIB_NAMESPACE: &str = "miden::protocol"; +const BATCH_KERNEL_NAMESPACE: &str = "miden::batch_kernel"; const KERNEL_PROCEDURES_RS_FILE: &str = "procedures.rs"; const TX_KERNEL_ERRORS_RS_FILE: &str = "tx_kernel_errors.rs"; @@ -105,12 +106,16 @@ fn main() -> Result<()> { /// /// Unlike the transaction kernel, the batch kernel does not expose syscalls, so there is no /// `KernelLibrary` to build — only a single executable program assembled from -/// `kernels/batch/main.masm`. +/// `kernels/batch/main.masm` with the modules under `kernels/batch/lib/` statically linked +/// under the `miden::batch_kernel` namespace. fn compile_batch_kernel(source_dir: &Path, target_dir: &Path) -> Result<()> { let batch_kernel_dir = source_dir.join(ASM_BATCH_KERNEL_DIR); + let lib_dir = batch_kernel_dir.join("lib"); let main_file_path = batch_kernel_dir.join("main.masm"); - let assembler = build_assembler(None)?; + let mut assembler = build_assembler(None)?; + assembler.compile_and_statically_link_from_dir(&lib_dir, BATCH_KERNEL_NAMESPACE)?; + let batch_main = assembler.assemble_program(main_file_path)?; let masb_file_path = target_dir.join("batch_kernel.masb"); diff --git a/crates/miden-protocol/src/batch/batch_id.rs b/crates/miden-protocol/src/batch/batch_id.rs index 39cfe42255..4c4f78839f 100644 --- a/crates/miden-protocol/src/batch/batch_id.rs +++ b/crates/miden-protocol/src/batch/batch_id.rs @@ -37,14 +37,26 @@ impl BatchId { /// Calculates a batch ID from the given transaction ID and account ID tuple. pub fn from_ids(iter: impl IntoIterator) -> Self { + Self(Hasher::hash_elements(&Self::hash_input_elements(iter))) + } + + /// Returns the felt sequence that [`Self::from_ids`] hashes to produce a [`BatchId`]. + /// + /// The layout is, for each `(transaction_id, account_id)` pair in iteration order: + /// `[transaction_id[4], account_id_prefix, account_id_suffix, 0, 0]` + /// + /// The batch kernel pipes this same felt sequence from the advice provider to memory and + /// asserts the resulting hash matches the public input `TRANSACTIONS_COMMITMENT`. + pub(crate) fn hash_input_elements( + iter: impl IntoIterator, + ) -> Vec { let mut elements: Vec = Vec::new(); for (tx_id, account_id) in iter { elements.extend_from_slice(tx_id.as_elements()); let [account_id_prefix, account_id_suffix] = <[Felt; 2]>::from(account_id); elements.extend_from_slice(&[account_id_prefix, account_id_suffix, ZERO, ZERO]); } - - Self(Hasher::hash_elements(&elements)) + elements } } diff --git a/crates/miden-protocol/src/batch/kernel.rs b/crates/miden-protocol/src/batch/kernel.rs index 29c5ad4fa8..0f73a49121 100644 --- a/crates/miden-protocol/src/batch/kernel.rs +++ b/crates/miden-protocol/src/batch/kernel.rs @@ -2,9 +2,10 @@ use alloc::vec::Vec; use miden_core::program::Kernel; -use crate::batch::ProposedBatch; +use crate::batch::{BatchId, ProposedBatch}; use crate::block::BlockNumber; use crate::errors::BatchOutputError; +use crate::transaction::{ToInputNoteCommitments, TransactionId}; use crate::utils::serde::Deserializable; use crate::utils::sync::LazyLock; use crate::vm::{AdviceInputs, Program, ProgramInfo, StackInputs, StackOutputs}; @@ -18,7 +19,7 @@ static KERNEL_MAIN: LazyLock = LazyLock::new(|| { Program::read_from_bytes(bytes).expect("failed to deserialize batch kernel runtime") }); -// Output stack indices, kept in sync with the layout at the end of `main.masm::main`. These are +// Output stack indices, kept in sync with the lay-out at the end of `main.masm::main`. These are // felt offsets, not word indices: `get_word(N)` returns the four felts at positions `N..N+4`. const INPUT_NOTES_COMMITMENT_WORD_IDX: usize = 0; const OUTPUT_NOTES_COMMITMENT_WORD_IDX: usize = 4; @@ -34,10 +35,10 @@ const TRAILING_PAD_WORD_FELT_IDX: usize = 12; /// The batch kernel program: an executable Miden program that proves a batch of transactions. /// -/// The kernel takes `[TRANSACTIONS_COMMITMENT, BLOCK_HASH]` as public inputs and emits +/// The kernel takes `[BLOCK_HASH, TRANSACTIONS_COMMITMENT]` as public inputs and emits /// `[INPUT_NOTES_COMMITMENT, OUTPUT_NOTES_COMMITMENT, batch_expiration_block_num]`. See -/// `asm/kernels/batch/main.masm` for the input/output contract and the `TODO` listing checks -/// the kernel does not yet enforce. +/// `asm/kernels/batch/main.masm` for the verification chain and the `TODO` markers listing +/// checks that the kernel does not yet enforce. pub struct BatchKernel; impl BatchKernel { @@ -80,9 +81,9 @@ impl BatchKernel { /// ``` /// /// Where: - /// - `TRANSACTIONS_COMMITMENT` is the value [`BatchId`](crate::batch::BatchId) computes — a - /// sequential hash of `(transaction_id || account_id_prefix || account_id_suffix || 0 || 0)` - /// over all transactions in the batch. + /// - `TRANSACTIONS_COMMITMENT` is the value [`BatchId`] computes — a sequential hash of + /// `(transaction_id || account_id_prefix || account_id_suffix || 0 || 0)` over all + /// transactions in the batch. /// - `BLOCK_HASH` is the commitment of the batch's reference block. pub fn build_input_stack(block_hash: Word, transactions_commitment: Word) -> StackInputs { let mut inputs: Vec = Vec::with_capacity(8); @@ -167,11 +168,59 @@ impl BatchKernel { /// Builds the advice inputs (map + stack) consumed by the batch kernel. /// - /// The skeleton kernel ignores its advice inputs, so this returns the default empty value. - /// The follow-up PR that adds the verification chain will populate the advice map with the - /// `(tx_id, account_id)` tuple list keyed by `TRANSACTIONS_COMMITMENT` and the per-tx headers - /// and note tuples. - fn build_advice_inputs(_proposed_batch: &ProposedBatch) -> AdviceInputs { - AdviceInputs::default() + /// See `asm/kernels/batch/main.masm` for the layered map structure. + fn build_advice_inputs(proposed_batch: &ProposedBatch) -> AdviceInputs { + let mut advice_inputs = AdviceInputs::default(); + + // Layer 1: TRANSACTIONS_COMMITMENT |-> [(tx_id, account_id_pair) tuples]. + let layer1_data = BatchId::hash_input_elements( + proposed_batch.transactions().iter().map(|tx| (tx.id(), tx.account_id())), + ); + advice_inputs.map.extend([(proposed_batch.id().as_word(), layer1_data)]); + + for tx in proposed_batch.transactions().iter() { + // Layer 2: tx_id |-> [INIT, FINAL, INPUT_NOTES_COMMITMENT, OUTPUT_NOTES_COMMITMENT, + // FEE_ASSET]. + let header_data = TransactionId::input_elements( + tx.account_update().initial_state_commitment(), + tx.account_update().final_state_commitment(), + tx.input_notes().commitment(), + tx.output_notes().commitment(), + tx.fee(), + ); + advice_inputs.map.extend([(tx.id().as_word(), header_data.to_vec())]); + + // Layer 3: per-tx INPUT_NOTES_COMMITMENT |-> [(NULLIFIER, EMPTY_OR_COMMITMENT) tuples]. + let input_notes_commitment = tx.input_notes().commitment(); + if input_notes_commitment != Word::empty() { + let mut data: Vec = + Vec::with_capacity(usize::from(tx.input_notes().num_notes()) * 8); + for note_commit in tx.input_notes().iter() { + data.extend_from_slice(note_commit.nullifier().as_word().as_elements()); + let commit_or_zero = note_commit.note_commitment().unwrap_or(Word::empty()); + data.extend_from_slice(commit_or_zero.as_elements()); + } + advice_inputs.map.extend([(input_notes_commitment, data)]); + } + + // Layer 3': per-tx OUTPUT_NOTES_COMMITMENT |-> [(NOTE_ID, METADATA_COMMITMENT) tuples]. + let output_notes_commitment = tx.output_notes().commitment(); + if output_notes_commitment != Word::empty() { + let mut data: Vec = Vec::with_capacity(tx.output_notes().num_notes() * 8); + for note in tx.output_notes().iter() { + data.extend_from_slice(note.id().as_word().as_elements()); + data.extend_from_slice(note.metadata().to_commitment().as_elements()); + } + advice_inputs.map.extend([(output_notes_commitment, data)]); + } + } + + // Advice stack: per-tx expiration_block_num in transaction order. + // The advice stack is FIFO from the prover's perspective — first pushed = first popped. + for tx in proposed_batch.transactions().iter() { + advice_inputs.stack.push(Felt::from(tx.expiration_block_num())); + } + + advice_inputs } } diff --git a/crates/miden-protocol/src/transaction/transaction_id.rs b/crates/miden-protocol/src/transaction/transaction_id.rs index 4313e6c465..14b5f538ee 100644 --- a/crates/miden-protocol/src/transaction/transaction_id.rs +++ b/crates/miden-protocol/src/transaction/transaction_id.rs @@ -35,6 +35,9 @@ use crate::utils::serde::{ pub struct TransactionId(Word); impl TransactionId { + /// Length of the felt sequence hashed by [`Self::new`] / [`Self::input_elements`]. + pub(crate) const INPUT_ELEMENTS_LEN: usize = 6 * WORD_SIZE; + /// Returns a new [TransactionId] instantiated from the provided transaction components. pub fn new( init_account_commitment: Word, @@ -43,13 +46,36 @@ impl TransactionId { output_notes_commitment: Word, fee_asset: FungibleAsset, ) -> Self { - let mut elements = [ZERO; 6 * WORD_SIZE]; + Self(Hasher::hash_elements(&Self::input_elements( + init_account_commitment, + final_account_commitment, + input_notes_commitment, + output_notes_commitment, + fee_asset, + ))) + } + + /// Returns the felt sequence that [`Self::new`] hashes to produce a [`TransactionId`]. + /// + /// The layout is: + /// `[INIT[4], FINAL[4], INPUT_NOTES_COMMITMENT[4], OUTPUT_NOTES_COMMITMENT[4], FEE_ASSET[8]]` + /// + /// The batch kernel pipes this same felt sequence from the advice provider to memory and + /// asserts the resulting hash matches a previously-verified `tx_id`. + pub(crate) fn input_elements( + init_account_commitment: Word, + final_account_commitment: Word, + input_notes_commitment: Word, + output_notes_commitment: Word, + fee_asset: FungibleAsset, + ) -> [Felt; Self::INPUT_ELEMENTS_LEN] { + let mut elements = [ZERO; Self::INPUT_ELEMENTS_LEN]; elements[..4].copy_from_slice(init_account_commitment.as_elements()); elements[4..8].copy_from_slice(final_account_commitment.as_elements()); elements[8..12].copy_from_slice(input_notes_commitment.as_elements()); elements[12..16].copy_from_slice(output_notes_commitment.as_elements()); elements[16..].copy_from_slice(&Asset::from(fee_asset).as_elements()); - Self(Hasher::hash_elements(&elements)) + elements } } diff --git a/crates/miden-testing/src/kernel_tests/batch/batch_kernel.rs b/crates/miden-testing/src/kernel_tests/batch/batch_kernel.rs index 6964990410..9c3e34f6a6 100644 --- a/crates/miden-testing/src/kernel_tests/batch/batch_kernel.rs +++ b/crates/miden-testing/src/kernel_tests/batch/batch_kernel.rs @@ -1,15 +1,18 @@ +use alloc::string::ToString; use alloc::sync::Arc; +use alloc::vec::Vec; use std::collections::BTreeMap; use anyhow::Context; use miden_core_lib::CoreLibrary; use miden_processor::{DefaultHost, ExecutionOptions, FastProcessor}; -use miden_protocol::Word; use miden_protocol::account::{Account, AccountStorageMode}; use miden_protocol::batch::{BatchKernel, ProposedBatch}; use miden_protocol::block::BlockNumber; use miden_protocol::note::{Note, NoteType}; -use miden_protocol::vm::{AdviceInputs, Program, StackInputs, StackOutputs}; +use miden_protocol::transaction::ToInputNoteCommitments; +use miden_protocol::vm::{AdviceInputs, StackInputs, StackOutputs}; +use miden_protocol::{Felt, Hasher, Word}; use miden_standards::testing::account_component::MockAccountComponent; use rand::Rng; @@ -48,9 +51,11 @@ fn generate_account(chain: &mut MockChainBuilder) -> Account { .expect("failed to add pending account from builder") } -/// Builds a two-transaction batch with realistic inputs and outputs. The skeleton kernel does not -/// inspect any of this data, but the batch is built end-to-end so the smoke test exercises the -/// real `prepare_inputs` path that the verification PR will eventually consume. +/// Builds a two-transaction batch: +/// - tx1 (account1): consumes one authenticated input note, produces one output note, expiration = +/// 1234. +/// - tx2 (account2): consumes one unauthenticated input note, produces two output notes, expiration +/// = 800. fn two_tx_batch(setup: &mut TestSetup) -> anyhow::Result { let block1 = setup.chain.block_header(1); let block2 = setup.chain.prove_next_block()?; @@ -86,8 +91,48 @@ fn two_tx_batch(setup: &mut TestSetup) -> anyhow::Result { )?) } +// EXPECTED-VALUE HELPERS +// ================================================================================================ + +/// Sequential hash over `(NULLIFIER, EMPTY_OR_NOTE_COMMITMENT)` tuples for every input note in +/// every transaction in iteration order. Mirrors the kernel's per-tx absorption (no erasure). +fn expected_input_notes_commitment(batch: &ProposedBatch) -> Word { + let mut elements: Vec = Vec::new(); + for tx in batch.transactions() { + for commit in tx.input_notes().iter() { + elements.extend_from_slice(commit.nullifier().as_word().as_elements()); + let note_or_zero = commit.note_commitment().unwrap_or(Word::empty()); + elements.extend_from_slice(note_or_zero.as_elements()); + } + } + if elements.is_empty() { + Word::empty() + } else { + Hasher::hash_elements(&elements) + } +} + +/// Sequential hash over `(NOTE_ID, METADATA_COMMITMENT)` tuples for every output note in every +/// transaction in iteration order. +fn expected_output_notes_commitment(batch: &ProposedBatch) -> Word { + let mut elements: Vec = Vec::new(); + for tx in batch.transactions() { + for note in tx.output_notes().iter() { + elements.extend_from_slice(note.id().as_word().as_elements()); + elements.extend_from_slice(note.metadata().to_commitment().as_elements()); + } + } + if elements.is_empty() { + Word::empty() + } else { + Hasher::hash_elements(&elements) + } +} + +// EXECUTION HELPERS +// ================================================================================================ + fn run_kernel( - program: &Program, stack_inputs: StackInputs, advice_inputs: AdviceInputs, ) -> Result { @@ -98,32 +143,121 @@ fn run_kernel( let processor = FastProcessor::new_with_options(stack_inputs, advice_inputs, ExecutionOptions::default()) .with_debugging(true); - let output = processor.execute_sync(program, &mut host)?; + let output = processor.execute_sync(&BatchKernel::main(), &mut host)?; Ok(output.stack) } -// SMOKE TEST +// HAPPY PATH // ================================================================================================ -/// The skeleton batch kernel drops its public inputs and exits, leaving the all-zero word output -/// region. This test exercises the full plumbing path (build a realistic `ProposedBatch`, derive -/// stack and advice inputs via `BatchKernel::prepare_inputs`, run the kernel, parse the outputs) -/// and asserts that the contract holds: the kernel runs to completion and emits the empty word -/// shape. #[test] -fn batch_kernel_skeleton_emits_empty_outputs() -> anyhow::Result<()> { +fn batch_kernel_happy_path() -> anyhow::Result<()> { let mut setup = setup(); let batch = two_tx_batch(&mut setup)?; let (stack_inputs, advice_inputs) = BatchKernel::prepare_inputs(&batch); - let stack_outputs = run_kernel(&BatchKernel::main(), stack_inputs, advice_inputs) - .context("kernel execution failed")?; + let stack_outputs = + run_kernel(stack_inputs, advice_inputs).context("kernel execution failed")?; let (input_notes_commitment, output_notes_commitment, expiration) = BatchKernel::parse_output_stack(&stack_outputs).context("parse output stack failed")?; - assert_eq!(input_notes_commitment, Word::empty()); - assert_eq!(output_notes_commitment, Word::empty()); - assert_eq!(expiration, BlockNumber::from(0u32)); + assert_eq!(input_notes_commitment, expected_input_notes_commitment(&batch)); + assert_eq!(output_notes_commitment, expected_output_notes_commitment(&batch)); + assert_eq!(expiration, batch.batch_expiration_block_num()); + assert_eq!(expiration, BlockNumber::from(800u32)); + + Ok(()) +} + +// NEGATIVE TESTS +// ================================================================================================ + +/// Corrupting `TRANSACTIONS_COMMITMENT` on the input stack makes Layer 1 unloadable from the +/// advice map, so the kernel must abort. +#[test] +fn batch_kernel_rejects_wrong_transactions_commitment() -> anyhow::Result<()> { + let mut setup = setup(); + let batch = two_tx_batch(&mut setup)?; + + let block_hash = batch.reference_block_header().commitment(); + let bogus_commitment = Word::from([12345u32; 4]); + let stack_inputs = BatchKernel::build_input_stack(block_hash, bogus_commitment); + let (_, advice_inputs) = BatchKernel::prepare_inputs(&batch); + + let err = run_kernel(stack_inputs, advice_inputs).expect_err("kernel must abort"); + let msg = err.to_string(); + assert!( + msg.contains("advice map") || msg.contains("not found") || msg.contains("missing"), + "unexpected error: {msg}", + ); + Ok(()) +} + +/// Tampering a verified `tx_id`'s Layer 2 advice-map entry breaks the per-tx hash check. +#[test] +fn batch_kernel_rejects_tampered_layer_2() -> anyhow::Result<()> { + let mut setup = setup(); + let batch = two_tx_batch(&mut setup)?; + + let (stack_inputs, mut advice_inputs) = BatchKernel::prepare_inputs(&batch); + + let tx0_id = batch.transactions()[0].id().as_word(); + let entry = advice_inputs.map.get(&tx0_id).expect("tx0 layer 2 entry"); + let mut tampered: Vec = entry.iter().copied().collect(); + tampered[0] += Felt::new(1); + advice_inputs.map.extend([(tx0_id, tampered)]); + + let err = run_kernel(stack_inputs, advice_inputs).expect_err("kernel must abort"); + let msg = err.to_string(); + assert!( + msg.contains("transaction header data piped from the advice map"), + "unexpected error: {msg}", + ); + Ok(()) +} + +/// Tampering the per-tx input-notes Layer 3 entry breaks the input-note hash check. +#[test] +fn batch_kernel_rejects_tampered_input_notes() -> anyhow::Result<()> { + let mut setup = setup(); + let batch = two_tx_batch(&mut setup)?; + + let (stack_inputs, mut advice_inputs) = BatchKernel::prepare_inputs(&batch); + + let key = batch.transactions()[0].input_notes().commitment(); + let entry = advice_inputs.map.get(&key).expect("layer 3 entry"); + let mut tampered: Vec = entry.iter().copied().collect(); + tampered[0] += Felt::new(1); + advice_inputs.map.extend([(key, tampered)]); + + let err = run_kernel(stack_inputs, advice_inputs).expect_err("kernel must abort"); + let msg = err.to_string(); + assert!( + msg.contains("per-transaction input notes data piped"), + "unexpected error: {msg}", + ); + Ok(()) +} + +/// Tampering the per-tx output-notes Layer 3' entry breaks the output-note hash check. +#[test] +fn batch_kernel_rejects_tampered_output_notes() -> anyhow::Result<()> { + let mut setup = setup(); + let batch = two_tx_batch(&mut setup)?; + + let (stack_inputs, mut advice_inputs) = BatchKernel::prepare_inputs(&batch); + + let key = batch.transactions()[0].output_notes().commitment(); + let entry = advice_inputs.map.get(&key).expect("layer 3' entry"); + let mut tampered: Vec = entry.iter().copied().collect(); + tampered[0] += Felt::new(1); + advice_inputs.map.extend([(key, tampered)]); + let err = run_kernel(stack_inputs, advice_inputs).expect_err("kernel must abort"); + let msg = err.to_string(); + assert!( + msg.contains("per-transaction output notes data piped"), + "unexpected error: {msg}", + ); Ok(()) } diff --git a/crates/miden-tx-batch-prover/src/local_batch_prover.rs b/crates/miden-tx-batch-prover/src/local_batch_prover.rs index fdd70bf6cb..f06756ba41 100644 --- a/crates/miden-tx-batch-prover/src/local_batch_prover.rs +++ b/crates/miden-tx-batch-prover/src/local_batch_prover.rs @@ -1,4 +1,5 @@ use alloc::boxed::Box; +use alloc::format; use alloc::string::ToString; use miden_processor::DefaultHost; @@ -39,16 +40,22 @@ impl LocalBatchProver { /// /// Verifies each transaction's `ExecutionProof` natively first, then runs the batch kernel /// via `miden_prover::prove` and attaches the resulting proof to the returned - /// [`ProvenBatch`]. The kernel's public outputs are not yet cross-checked against the - /// proposed batch's expected values; that check is added together with the kernel's - /// verification logic in a follow-up PR. + /// [`ProvenBatch`]. + /// + /// After proof generation, the kernel's parsed `batch_expiration_block_num` output is + /// checked against `proposed_batch.batch_expiration_block_num()`. The two batch note + /// commitments produced by the kernel are *not* checked here because the kernel computes a + /// raw sequential hash that does not match `proposed_batch.input_notes().commitment()` for + /// batches with intra-batch unauthenticated-note erasure. /// /// # Errors /// /// Returns an error if: /// - any transaction's proof in the batch fails to verify; /// - the batch kernel program fails to execute or produce a proof; - /// - the kernel output stack fails to parse. + /// - the kernel output stack fails to parse; + /// - the kernel's `batch_expiration_block_num` does not match + /// `proposed_batch.batch_expiration_block_num()`. pub async fn prove( &self, proposed_batch: ProposedBatch, @@ -64,6 +71,7 @@ impl LocalBatchProver { })?; } + let expected_expiration = proposed_batch.batch_expiration_block_num(); let (stack_inputs, advice_inputs) = BatchKernel::prepare_inputs(&proposed_batch); let mut host = DefaultHost::default(); @@ -77,11 +85,15 @@ impl LocalBatchProver { .await .map_err(|err| ProvenBatchError::BatchKernelExecutionFailed(err.to_string()))?; - // Validate the output stack shape (padding cells are zero and the expiration fits in - // u32); the actual output values themselves are not checked until the kernel verifies - // them. - BatchKernel::parse_output_stack(&stack_outputs) - .map_err(|err| ProvenBatchError::BatchKernelExecutionFailed(err.to_string()))?; + let (_input_notes_commitment, _output_notes_commitment, kernel_expiration) = + BatchKernel::parse_output_stack(&stack_outputs) + .map_err(|err| ProvenBatchError::BatchKernelExecutionFailed(err.to_string()))?; + + if kernel_expiration != expected_expiration { + return Err(ProvenBatchError::BatchKernelExecutionFailed(format!( + "kernel batch_expiration_block_num {kernel_expiration} does not match the proposed batch's {expected_expiration}", + ))); + } Self::build_proven_batch(proposed_batch, proof) }