feat(batch kernel): wire up `INPUT_NOTES_COMMITMENT` & note erasure by mmagician · Pull Request #2905 · 0xMiden/protocol

mmagician · 2026-05-12T08:25:29Z

Builds on the batch kernel skeleton (#2904) to fill in the first part of the verification chain. The kernel recomputes the batch INPUT_NOTES_COMMITMENT as the nullifier-sorted, post-erasure commitment matching ProposedBatch::input_notes().commitment(). Output notes are processed only to track erasure; computing BATCH_NOTE_TREE_ROOT and the expiration_block_num running-minimum are deferred to follow-up PRs.

What this does

Prologue

Verification of data layers

The kernel takes [BLOCK_COMMITMENT, BATCH_ID, pad(8)] and walks a layered advice map, each layer keyed by a hash the previous layer verified. It then writes all this data to memory. The advice map is structured as:

Layer 1 - BATCH_ID -> the (tx_id, account_id) tuple list
Layer 2 - each tx_id_i -> the transaction header preimage, i.e. [INIT_ACCOUNT_COMMITMENT_i, FINAL_ACCOUNT_COMMITMENT_i, INPUT_NOTES_COMMITMENT_i, OUTPUT_NOTES_COMMITMENT_i, FEE_ASSET_i]. For the scope of this PR, we only care about the input & output notes commitments.
Layer 3a - each INPUT_NOTES_COMMITMENT_i -> (NULLIFIER, EMPTY_OR_COMMITMENT) tuples
Layer 3b - each OUTPUT_NOTES_COMMITMENT_i -> (NOTE_DETAILS_COMMITMENT, METADATA_COMMITMENT) tuples

The prologue only verifies Layers 1 and 2: it writes the tuple list and the per-transaction headers (which include each INPUT_NOTES_COMMITMENT_i / OUTPUT_NOTES_COMMITMENT_i) to memory, in tx_id order. The Layer 3 note pre-images are not loaded here — they are streamed in per transaction later (see Note matching).

Loading "global" notes

So at this point we have, in tx_id order, each transaction's verified input/output notes commitments — but our goal is to compute INPUT_NOTES_COMMITMENT over the notes sorted by their nullifier, and post-erasure.
To do this, we load two more lists into memory, supplied by the host and unverified (for now):

input note list, sorted by their nullifier, via prepare_input_note_list
output note list, sorted by their note id, via prepare_output_note_list

So at the end of the prologue's prepare_batch, for both input and output notes we have a verified tx_id-ordered view (the per-transaction commitments) and an untrusted nullifier/note-id-sorted list.

The next step is to match them.

Note tracker

Note erasure

A note is erased when it is created and consumed within the same batch. Only an unauthenticated input note (one carrying a note id) can be erased, so for each such entry in the input list we look up its note id in the output list. If it is found, the note is created somewhere in the batch and is a candidate for erasure: we flag the input entry expected-to-be-erased and link it to the matching output entry.

This is a static, order-independent pass over the (untrusted) sorted lists. Whether the erasure is actually valid — the creating transaction runs before the consuming one — is enforced during matching.

Note matching

So far we've determined erasure, but the nullifier/note-id-sorted lists are still untrusted.

We now process one transaction at a time. Its note tuples are piped from the advice provider into a small scratch buffer — re-used for each transaction, so only one transaction's notes are written to scratch memory at a time — and verified by asserting their hash equals that transaction's INPUT_NOTES_COMMITMENT_i / OUTPUT_NOTES_COMMITMENT_i. Then, for each note, we look it up in the untrusted list — input notes by nullifier, output notes by note id — assert the looked-up entry matches, and mark it {consumed for inputs, created for outputs}.

Because every verified per-transaction note must be found, each entry may be marked at most once, and the lists are strictly sorted (no duplicates), this proves the untrusted lists are exactly the per-transaction note sets: the host cannot inject, omit, or duplicate notes.

Epilogue

Once every note is matched, we:

assert every input entry was consumed, every output entry was created, and no erasure is left pending — so the host could not tamper with the list;
compute INPUT_NOTES_COMMITMENT as the sequential hash over the non-erased input entries in nullifier order, reproducing build_input_note_commitment

Fill in the batch kernel to verify the batch's transaction list against its BATCH_ID (Layer 1), verify each transaction header (Layer 2), and recompute the batch INPUT_NOTES_COMMITMENT from the verified per-tx input notes (Layer 3). Output-notes (BATCH_NOTE_TREE_ROOT) and the expiration running-min stay as zero placeholders, wired up in follow-up PRs.

… injection Add BatchExecutor::extend_advice_inputs (mirroring TransactionContextBuilder) so the kernel's rejection paths can be exercised through the normal executor with tampered advice, and drop the low-level run_kernel test helper. The three negative tests now corrupt the Layer 1/2/3 advice-map entries via the executor.

Match the operand-stack (# =>) and advice-stack (# AS =>) comment style used throughout the rest of the protocol assembly.

Reconstruct the batch's input notes from a host-provided global list sorted by nullifier, bind every per-transaction input note to that list (lookup via sorted_array::find_key_value, with consumption + note-id checks so the host cannot omit, inject, duplicate, or alter notes), and hash the list to emit INPUT_NOTES_COMMITMENT == ProposedBatch::input_notes().commitment() for batches without intra-batch note erasure. BatchExecutor loads the CoreLibrary itself so the sorted_array event handlers are registered, and BatchVerifier now verifies against the real input-notes commitment. Intra-batch note erasure is a follow-up; the output-note advice (sorted list + per-tx output tuples) and the output memory regions are provided here as scaffolding for it.

…ut notes Add the output-note half of the note tracker: load the host-provided note-id-sorted output list, bind every per-transaction output note to it (deriving each NoteId via poseidon2::merge of its details/metadata commitments), and cross-reference the two lists to mark notes that are both created and consumed within the batch. Processing transactions in batch order (outputs before inputs) with a 1->2 erasure gate rejects consuming such a note before its creator runs (circular/incorrectly-ordered dependencies), and the epilogue hashes only the surviving input notes. INPUT_NOTES_COMMITMENT now matches ProposedBatch::input_notes().commitment() for batches with intra-batch erasure.

…gate Process each transaction's input notes before its output notes. With outputs-first, a note created and consumed by the same transaction had its erasure flag advanced to 2 before the consume check, so it was erased instead of rejected. Inputs-first means the consume sees the flag still at 1 (the creating output has not been processed yet), tripping the consume-before-create gate, matching the Rust note tracker's rejection. Cross-transaction erasure is unaffected (an earlier transaction's outputs are still processed before any later transaction's inputs). Adds a test that drives the gate by claiming a consumed note is created in-batch without any transaction creating it.

…tives Extract the batch kernel's MASM error constants (build.rs + the errors::batch_kernel module, mirroring tx_kernel/protocol) and assert the exact ERR_BATCH_* raised by each global-list binding and erasure negative test (via matches_execution_error), instead of just checking is_err. The three layer-tamper tests still assert only failure, since their hash check uses pipe_preimage_to_memory's bare assertion, which carries no named error code.

Rewrite comments that referenced the PR's development history ("currently", "still all-zero placeholders", "not yet", "wired up in follow-up PRs") so they describe what the code does. Tighten the CHANGELOG entry to match the surrounding single-sentence style.

Address review feedback on PR #2905: - Add bounds asserts so the kernel rejects oversized inputs before they overflow the fixed-size memory regions: the per-batch transaction count, the two global note-list lengths, and each transaction's note-set length are checked against MAX_TRANSACTIONS_PER_BATCH / MAX_NOTES_PER_BATCH. The global-list check is the load-bearing one, since those lists are not bound by a commitment hash. - Make note_tracker.masm the single source of truth for the advice-map sentinel keys: build.rs generates the matching Rust constants, and both the kernel and the tests derive them, removing the duplicated literals. - Add epilogue negative tests (unconsumed input note, uncreated output note) and an oversized-list bound test.

Address pre-push review findings on the batch verifier and output stack: - BatchVerifier::verify now returns the verified proof's security level instead of discarding it, so the acceptance test pins the proof's actual level (via a zero-minimum verify) rather than assuming the hardcoded MIN_PROOF_SECURITY_LEVEL constant equals it. - Rename the verifier's stored minimum to min_proof_security_level to distinguish it from the actual verified level. - Add a BatchOutputs::into_stack_outputs round-trip unit test covering distinct, non-zero fields.

The BATCH_ID and reference block commitment come from the ProvenBatch's own fields and are not recomputed from its transactions, so a successful verification binds nothing the batch's constructor could not forge. State this in the warning and restate the trust-boundary caveat on verify().

- note_tracker.masm: lowercase pointer names in stack-state comments. - kernel.rs: rename generated module to generated_constants; rename the per-tx note Vec to preimage_data. - test_batch_kernel.rs: introduce FELTS_PER_NOTE_ENTRY and use MAX_INPUT_NOTES_PER_BATCH instead of magic 8/1024; parametrize the three tampered-advice tests with rstest; drop the thin note-list-key wrappers in favor of BatchKernel::{input,output}_note_list_key. - build.rs / batch_executor.rs: trim verbose doc comments.

huitseeker · 2026-07-02T23:35:24Z

+                for note_commit in tx.input_notes().iter() {
+                    let nullifier = note_commit.nullifier();
+                    let note_id_or_empty =
+                        note_commit.header().map_or(Word::empty(), |header| header.id().as_word());


I think this should be an explicit unsupported-batch case for now.

I’d prefer to reject at the batch execution/proving boundary rather than in ProposedBatch::new, because the batch itself is still a valid protocol object. The current limitation is specifically that this batch kernel cannot yet prove the note-authentication transition from (NULLIFIER, NOTE_ID) to (NULLIFIER, EMPTY) without the MMR authentication step.

So the temporary shape I’d expect is:

detect when a tx consumes an unauthenticated note, but the batch-level input note set contains the authenticated/nullifier-only form for the same nullifier;

return a clear ProvenBatchError before executing the kernel;

add a regression test for that case;

leave the real fix tied to the existing in-kernel note-authentication TODO.

That keeps the liveness failure explicit, without weakening the binding check.

Port the Miden protocol batch kernel (0xMiden/protocol#2905, plus the expiration running-minimum of 0xMiden/protocol#3019) to Rust compiled with the Miden compiler, to exercise the compiler on a realistic kernel-sized program. The fixture at tests/fixtures/batch-kernel mirrors the MASM kernel module-for-module: the prologue unhashes the layered advice data anchored at the public BATCH_ID, the note tracker determines intra-batch erasure and binds the host-provided sorted note lists to the verified per-transaction notes, and the epilogue enforces the tracking invariants and computes INPUT_NOTES_COMMITMENT. The smoke test plays the protocol's BatchKernel::prepare_inputs role: it derives batch ids, transaction ids and note commitments for mock transactions with the host hasher, feeds the layered advice map and the expiration advice stack, and checks the kernel outputs across four scenarios (a plain two-transaction batch, intra-batch note erasure, a tampered BATCH_ID pre-image, and a consume-before-create rejection). Note-flag state is felt-typed and the sorted-list lookup uses a hand-rolled word comparison: integer discriminant matches currently lower to a br_table whose checked I32->U32 selector cast rejects legitimately wrapped selectors ("value does not fit in i32"), so the fixture stays in the felt domain where comparisons lower to opaque intrinsics.

…h-kernel-logic # Conflicts: # crates/miden-protocol/src/batch/batch_id.rs # crates/miden-protocol/src/batch/kernel.rs # crates/miden-tx-batch/src/verifier.rs

zeapoz

Looks pretty good! Didn't review all of the MASM or tests in detail but left some initial comments and optional nits. I'll touch on this again after getting more familiar with the mechanisms.

Co-authored-by: zeapoz <zeapo@pm.me>

Apply the constant/error formatting used across the migrated kernel MASM: spaces around =, plain # doc comments on constants, and wrapping definitions that exceed 100 columns onto an indented string line.

- drop the stale block of duplicated v0.16 entries (including the duplicated AccountStoragePatch line flagged in review) that earlier next-merges left in an already-released section - move the #2905 entry to the unreleased v0.17.0 section, mark it BREAKING, and call out that BatchExecutor::execute now takes caller AdviceInputs

BatchExecutor::execute now compares the parsed kernel outputs against the outputs expected for the proposed batch (its input notes commitment, with the note tree root and expiration pinned to the kernel's placeholder values, mirroring BatchVerifier) and fails with ProvenBatchError::BatchKernelOutputMismatch instead of deferring the mismatch to eventual proof verification.

PhilippGackstatter

Left a few comments. I think the PR would be a quite a bit easier to parse if it matched the regular code style of MASM, in particular newlines after stack comments, constants over magic numbers and precise labels.

Happy to address these in a "review comments" PR, if you'd like, just let me know.

PhilippGackstatter · 2026-08-19T11:36:11Z

+# +-------------------+-------------------------+----------------------------------+
+# | Address range     | Constant                | Contents                         |
+# +-------------------+-------------------------+----------------------------------+
+# | 0                 | NUM_TRANSACTIONS_PTR    | num_transactions (1 felt).       |
+# | 4..8              | BATCH_HASHER_RATE0_PTR  | RATE0 of the batch-level         |


nit: This is great!

It would be a bit more readable if we allowed it to be at least 100 characters wide. I would prioritize readability over the 100 char rule even, like we do in memory.rs.

PhilippGackstatter · 2026-08-19T11:42:16Z

+    # adv_push reads the value's felt length; div.4 converts felts -> words (4 felts per word).
+    adv_push div.4
+    # => [num_words, BATCH_ID, tx_tuples_ptr]
+
+    # num_transactions = num_words / 2 (each tx contributes 2 words: tx_id + account_id_pair).
+    dup div.2


nit: could we introduce constants here, e.g. WORD_NUM_ELEMENTS and TX_COMMITMENT_NUM_WORDS?

PhilippGackstatter · 2026-08-19T11:43:31Z

+    # adv_push reads the value's felt length; div.4 converts felts -> words (4 felts per word).
+    adv_push div.4
+    # => [num_words, BATCH_ID, tx_tuples_ptr]
+
+    # num_transactions = num_words / 2 (each tx contributes 2 words: tx_id + account_id_pair).
+    dup div.2
+    # => [num_transactions, num_words, BATCH_ID, tx_tuples_ptr]
+    dup u32lte.MAX_TRANSACTIONS_PER_BATCH assert.err=ERR_BATCH_TOO_MANY_TRANSACTIONS
+    exec.memory::set_num_transactions


u32 operation on unverified input. Use u32assert or u32assert2 first.

PhilippGackstatter · 2026-08-19T11:46:41Z

+    # num_transactions = num_words / 2 (each tx contributes 2 words: tx_id + account_id_pair).
+    dup div.2
+    # => [num_transactions, num_words, BATCH_ID, tx_tuples_ptr]
+    dup u32lte.MAX_TRANSACTIONS_PER_BATCH assert.err=ERR_BATCH_TOO_MANY_TRANSACTIONS
+    exec.memory::set_num_transactions
+


nit: could we apply the standard formatting here, e.g. add a newline after stack state comments (line 190) and add stack state comments after instruction groups (line 192)?

PhilippGackstatter · 2026-08-19T11:47:40Z

+    movup.5 swap
+    # => [num_words, tx_tuples_ptr, BATCH_ID]


nit: We could push tx tuples ptr here instead of earlier as we don't use it before.

PhilippGackstatter · 2026-08-19T13:27:25Z

+        # Pipe this transaction's input-note tuples into the scratch region, asserting their
+        # sequential hash equals INPUT_NOTES_COMMITMENT_idx (so the tuples are exactly the committed
+        # ones).
+        push.TX_NOTES_SCRATCH_PTR movdn.4


I would use local memory here so the global memory region doesn't get polluted by a scratch space.

PhilippGackstatter · 2026-08-19T13:29:38Z

+        adv_push div.4
+        # => [num_words, INPUT_NOTES_COMMITMENT_idx, scratch_ptr, tx_index]
+        dup div.2 u32lte.MAX_NOTES_PER_BATCH assert.err=ERR_BATCH_TX_TOO_MANY_NOTES


u32 operation on unverified input. Use u32assert or u32assert2 first.

PhilippGackstatter · 2026-08-19T13:31:52Z

+    # => [i, num_notes]
+    dup.1 dup.1 neq
+    while.true


nit: consider iterating high to low.

PhilippGackstatter · 2026-08-19T13:38:35Z

+    # => [is_found, key_ptr, start_ptr, end_ptr, scratch_entry_ptr]
+    assert.err=ERR_BATCH_INPUT_NOTE_NOT_IN_LIST
+    swap drop swap drop
+    # => [key_ptr, scratch_entry_ptr]


It would be helpful to name these something like claimed_input_note_ptr and verified_input_note_ptr or something that resembles the semantics.

PhilippGackstatter · 2026-08-19T13:40:24Z

+    # consumed.
+    swap drop
+    # => [key_ptr]
+    exec.memory::input_entry_index_from_key_ptr


nit: naming, key_ptr can refer to many things

partylikeits1983

Overall, the direction looks good. I left a few comments about input validation and the public API. I also think procedure doc comments should define their input and output stack signatures more explicitly, and consistent MASM formatting, stack state comments, and named constants would make the code easier to review and maintain.

partylikeits1983 · 2026-08-19T13:50:09Z

+    exec.memory::get_num_output_notes
+    # => [num_output_notes]
+    push.0
+    # => [idx, num_output_notes]
+    dup.1 dup.1 neq
+    # => [should_loop, idx, num_output_notes]


Adding empty lines after stack comments would make this easier to read. This applies to masm throughout this PR.

partylikeits1983 · 2026-08-19T13:57:26Z

+#! Absorbs input-note list entry `idx`'s 8-felt `(NULLIFIER, NOTE_ID_OR_EMPTY)` tuple into the batch
+#! hasher state held in memory (overwrite-mode poseidon2, matching `Hasher::hash_elements`).
+#!
+#! Inputs:  [idx]
+#! Outputs: []
+proc absorb_input_entry
+    # The entry occupies one double word [entry_ptr, entry_ptr + NOTE_ENTRY_FELT_LEN).
+    exec.memory::input_note_entry_ptr


In this procedure doc comment, I'd make it more obvious that NULLIFIER, NOTE_ID_OR_EMPTY is part of the type signature of this procedure, but passed in via memory.

Also applies to the the output, which is the hash in memory.

partylikeits1983 · 2026-08-19T13:59:23Z

+    add.1
+end


Suggested change

add.1

end

add.1

# => [idx + 1, absorbed_count, num]

end

partylikeits1983 · 2026-08-19T14:00:26Z

+#! Inputs:  [KEY, write_ptr]
+#! Outputs: [num_notes]
+proc load_note_list
+    adv.push_mapvaln


I'd outline in the procedure doc comment the expected state of the advice map when calling this procedure.

partylikeits1983 · 2026-08-19T19:23:10Z

+    ///   The kernel stores the pre-erasure lists in fixed-size regions, so it rejects such batches
+    ///   even when valid post-erasure. Tracked in
+    ///   <https://github.com/0xMiden/protocol/issues/3184>.
+    pub fn ensure_supported(proposed_batch: &ProposedBatch) -> Result<(), ProvenBatchError> {


The batch kernel supports at most 1024 transactions, but that limit is not checked here. We should reject batches with more than 1024 transactions in ensure_supported() and return a specific error.

partylikeits1983 · 2026-08-19T19:51:44Z

+        advice_inputs: AdviceInputs,
    ) -> Result<ExecutedBatch, ProvenBatchError> {
-        let (stack_inputs, advice_inputs) = BatchKernel::prepare_inputs(&proposed_batch);
+        BatchKernel::ensure_supported(&proposed_batch)?;
+
+        let (stack_inputs, mut batch_advice_inputs) = BatchKernel::prepare_inputs(&proposed_batch);


the execute() function now accepts and overwrites advice with caller provided advice inputs, is this intentional?

Because AdviceInputs::extend() replaces advice map entries with matching keys, callers can override the generated map returned by BatchKernel::prepare_inputs(). Current usage seems limited to negative tests. Is this intended to support additional nondeterministic inputs? If not, we should move this override mechanism to a test only helper.

Fumuran

Looks good, thank you! It's a partial review, for now I looked through only the masm code. One general comments is that we should standardize the format: add empty lines after stack comments, add inline comments, add advice stack inlines in addition to the operand stack.

Fumuran · 2026-08-19T07:14:30Z

+#! returns the number of entries. The list is not hashed against a commitment; its integrity is
+#! established later by binding every entry to a verified per-transaction note.
+#!
+#! Inputs:  [KEY, write_ptr]


nit: in case we use data from advice map, we should include it into the inputs

Suggested change

#! Inputs: [KEY, write_ptr]

#! Inputs:

#! Operand stack: [KEY, write_ptr]

#! Advice map: {

#! INPUT_NOTES_COMMITMENT_i: [(NULLIFIER, EMPTY_OR_COMMITMENT)]

#! }

Fumuran · 2026-08-19T07:18:26Z

+    adv.push_mapvaln
+    # AS: [len_felts, data...]
+    adv_push
+    # => [len_felts, KEY, write_ptr]


nit: here and in other places I would use our standard format (=> arrow after AS, include operand stack in addition to advice stack, empty line after stack state block)

Suggested change

adv.push_mapvaln

# AS: [len_felts, data...]

adv_push

# => [len_felts, KEY, write_ptr]

adv.push_mapvaln

# OS => [KEY, write_ptr]

# AS => [len_felts, [(NULLIFIER, EMPTY_OR_COMMITMENT)]]

adv_push

# OS => [len_felts, KEY, write_ptr]

# AS => [[(NULLIFIER, EMPTY_OR_COMMITMENT)]]

Fumuran · 2026-08-19T15:33:51Z

+    # A length that is not a multiple of 8 felts wraps `num_notes` (field `div`) to a non-u32
+    # felt, which the range check below rejects.


question: I'm not deeply understand how the field element inversion is computed, so I'm not sure: is it correct that we can guarantee that the result of the filed division will result in non-u32 value because num_notes is guaranteed to be a u32 value? So, in general, how can we guarantee that the result will be an non-u32 value?

Fumuran · 2026-08-19T15:43:27Z

+#! Inputs:  [KEY, write_ptr]
+#! Outputs: [num_notes]
+proc load_note_list
+    adv.push_mapvaln


nit: it seems like we don't use KEY after this line, so I would drop it here to simplify the stack management

Fumuran · 2026-08-19T20:04:48Z

+#
+# Below is the memory layout used by the batch kernel:
+#
+# +-------------------+-------------------------+----------------------------------+


Really nice table!

Fumuran · 2026-08-19T20:56:11Z

+# PER-TRANSACTION OUTPUT NOTES
+# =================================================================================================
+
+#! Marks output-note list entry `j` as created, asserting it was not already created.


nit: I would probably use something more meaningful than j

PhilippGackstatter

I think the MASM code looks good correctness-wise 👍.

I think the main work left is making it more human-readable and -maintainable.

PhilippGackstatter · 2026-08-20T12:39:24Z

+        push.OUTPUT_NOTES_PTR movdn.4
+        exec.memory::get_output_notes_end_ptr movdn.5
+        # => [NOTE_ID, output_notes_ptr, output_end_ptr, idx]
+        exec.sorted_array::find_key_value


Consider pulling this logic out into a helper find_output_note. Same for find_input_note that we search for elsewhere.

PhilippGackstatter · 2026-08-20T13:19:52Z

+#! Asserts input-note list entry `idx` is not expected-to-be-erased (erasure flag != 1) at the
+#! point it is consumed: if it is created in this batch, its creator has already been
+#! processed. Rejects consume-before-create / circular dependencies.
+#!
+#! Inputs:  [idx]
+#! Outputs: []
+proc assert_input_not_consumed_before_created
+    exec.memory::input_note_flags_ptr mem_load
+    # => [erasure]
+    neq.1 assert.err=ERR_BATCH_NOTE_CONSUMED_BEFORE_CREATED
+end


The input note flag is not a boolean or a bit flag, it is an enumeration as it has three states 0, 1, 2. So I'd avoid calling it a flag and add something like this enum:

enum InputNoteErasureState: u8 { UNERASED = 0, ERASURE_EXPECTED = 1, ERASED = 2, }

The doc comment could be:

Suggested change

#! Asserts input-note list entry `idx` is not expected-to-be-erased (erasure flag != 1) at the

#! point it is consumed: if it is created in this batch, its creator has already been

#! processed. Rejects consume-before-create / circular dependencies.

#!

#! Inputs: [idx]

#! Outputs: []

proc assert_input_not_consumed_before_created

exec.memory::input_note_flags_ptr mem_load

# => [erasure]

neq.1 assert.err=ERR_BATCH_NOTE_CONSUMED_BEFORE_CREATED

end

#! Asserts the state of the input note `input_note_idx` is not `ERASURE_EXPECTED`.

#!

#! If it is, it means the output note that erases it is created by a later transaction or by the

#! currently processed transaction.

#!

#! If it isn't erased at all, its state is `UNERASED`. If it is legitimately created by some

#! transaction _ordered before the current one_, its processing has marked the note as `ERASED`.

#!

#! This rejects consume-before-create / circular dependencies.

In general, I think it would be good to use the enum type for all enumerations in the batch as this makes things easier to understand and directly gives us types. This is something we should do in the tx kernel eventually, I think.

I think it would also be helpful to use is_consumed rather than consumption to make it clear that it's a boolean.

Just sharing the example I used to think about this. Take a batch with two txs as inputs but in the wrong order, i.e. X is consumed before it is created:

TX 1: Inputs [X] -> Outputs [] TX 2: Inputs [] -> Outputs [X]

After cross-referencing the state is:
Input X: erasure = 1, consumption = 1
Output X: will_be_erased = 0, erased_by = 0

During binding, we process tx1's input note X and find that ERASURE_EXPECTED. This means the output note that erases it has not yet marked it as ERASED, and this indicates the consumed-before-created state.

Had it been the opposite order, the state would've been ERASED and the assertion would have passed. Similarly, if it isn't erased at all, the state is UNERASED and neq.ERASURE_EXPECTED assert would also pass.

PhilippGackstatter · 2026-08-20T13:24:28Z

+    swapw
+    # => [DETAILS, METADATA, scratch_entry_ptr]
+    exec.poseidon2::merge
+    # => [NOTE_ID, scratch_entry_ptr]   (NoteId = merge(details, metadata))


Not necssarily for this PR, but it would be great to move this to a helper compute_note_id so we can eventually deduplicate these kinds of things with the tx kernel. I would even vote for doing this sooner than later, before we run into code duplications. This is a tiny example, but I'm sure larger code duplications will come otherwise.

PhilippGackstatter · 2026-08-20T13:45:42Z

+    # If this output note erases an input note (cross-referenced earlier), advance that input note's
+    # erasure flag from 1 (expected) to 2 (creator processed).
+    dup exec.memory::output_note_flags_ptr mem_load
+    # => [will_be_erased, j]
+    if.true
+        exec.memory::output_note_flags_ptr add.OUTPUT_NOTE_LINKED_INPUT_OFFSET mem_load
+        # => [linked_input_index]
+        exec.flip_input_erasure_created
+    else


Consider introducing helpers for reading and writing these flags or states so that these kinds of invocations become just get_output_note_erasure or set_input_note_erasure_expected, etc.

The linked_input_index is also only valid if will_be_erased = 1, so I would make it only accessible behind the same procedure, hence the suggestion for get_output_note_erasure to get both.

I think it would be even nicer if we could have just one value and have 0 indicate "not erased". One way to do this is to store the ptr to the input note that erases it.

PhilippGackstatter · 2026-08-20T13:49:37Z

+#!
+#! Inputs:  [idx]
+#! Outputs: []
+proc flip_input_erasure_created


Suggested change

proc flip_input_erasure_created

proc mark_input_note_erased

PhilippGackstatter · 2026-08-20T14:00:00Z

+    # => [flags_ptr, idx, absorbed_count, num]
+    mem_load
+    # => [erasure, idx, absorbed_count, num]
+    dup neq.1 assert.err=ERR_BATCH_NOTE_CONSUMED_BEFORE_CREATED


Can we ever actually run into this assertion? Wouldn't all of these be caught by assert_input_not_consumed_before_created already?

PhilippGackstatter · 2026-08-20T14:00:54Z

+    neq.2
+    # => [not_erased, idx, absorbed_count, num]
+    if.true


nit: I think eq.0 (or eq.UNERASED) would avoid the negation and be clearer.

PhilippGackstatter · 2026-08-20T14:03:30Z

+    # => [should_loop, idx, absorbed_count, num]
+    while.true
+        exec.process_input_entry
+        # => [idx+1, absorbed_count, num] (absorbed_count + 1 if entry was not erased)


Suggested change

# => [idx+1, absorbed_count, num] (absorbed_count + 1 if entry was not erased)

# => [idx+1, absorbed_count, num]

nit: that's the concern of process_input_entry

PhilippGackstatter · 2026-08-20T14:10:42Z

+    # With no non-erased entries the commitment is the empty word, matching the early return in
+    # `build_input_note_commitment` (this is not the hash of zero elements). Otherwise squeeze the
+    # accumulated state.
+    eq.0
+    if.true
+        padw
+        # => [EMPTY_WORD]
+    else
+        exec.memory::load_batch_hasher_state
+        exec.poseidon2::squeeze_digest
+        # => [INPUT_NOTES_COMMITMENT]
+    end


We don't need this, it's sufficient to

exec.memory::load_batch_hasher_state exec.poseidon2::squeeze_digest

I think this means also that we can remove absorbed_count completely.

PhilippGackstatter · 2026-08-20T14:14:39Z

+#!
+#! Inputs:  [tx_index]
+#! Outputs: [tx_tuple_ptr]
+pub proc tx_tuple_ptr


nit: I would use get and set prefixes for all procedures here that fit this description. For consistency with the tx kernel.

- document advice-map inputs in proc doc comments and use the standard OS/AS stack-comment format around advice interactions, with blank lines between instruction groups - widen the memory layout table beyond 100 columns for readability - name the felts-per-word and words-per-entry literals (WORD_NUM_ELEMENTS, TX_TUPLE_NUM_WORDS, NOTE_ENTRY_NUM_WORDS, shared via the memory module) - u32assert unverified advice-derived counts before their u32 range checks - assert the batch contains at least one transaction in Layer 1 (ERR_BATCH_NO_TRANSACTIONS, mirroring ProposedBatch's EmptyTransactionBatch check), letting the Layer 2 loop be entered unconditionally and iterate high-to-low - push write pointers only when needed, removing stack juggling

mmagician changed the title ~~feat: batch kernel verification chain + tests~~ feat: minimal batch kernel May 12, 2026

mmagician mentioned this pull request May 12, 2026

feat: minimal batch kernel #2884

Closed

mmagician commented May 15, 2026

View reviewed changes

Comment thread crates/miden-protocol/asm/kernels/batch/lib/prologue.masm Outdated

Comment thread crates/miden-protocol/asm/kernels/batch/lib/prologue.masm Outdated

mmagician force-pushed the mmagician-claude/batch-kernel-logic branch from 9b2a31a to 7e97e87 Compare June 1, 2026 10:11

mmagician changed the title ~~feat: minimal batch kernel~~ feat: verify batch tx list, tx headers, and input-notes commitment Jun 1, 2026

This was referenced Jun 1, 2026

feat(batch kernel): emit batch_expiration_block_num as the running-min over transactions #3019

Draft

Wire BatchNoteTree into batch & block construction #3020

Open

mmagician force-pushed the mmagician-claude/batch-kernel-logic branch 2 times, most recently from 7dbd6b7 to 5bccee1 Compare June 1, 2026 11:25

mmagician changed the title ~~feat: verify batch tx list, tx headers, and input-notes commitment~~ feat(batch kernel): verify INPUT_NOTES_COMMITMENT Jun 1, 2026

mmagician force-pushed the mmagician-claude/batch-kernel-logic branch from 5bccee1 to 133f9bb Compare June 1, 2026 11:38

mmagician commented Jun 1, 2026

View reviewed changes

mmagician force-pushed the mmagician-claude/batch-kernel-logic branch from 133f9bb to 59c2efb Compare June 1, 2026 13:51

mmagician mentioned this pull request Jun 3, 2026

feat: batch kernel skeleton #2904

Merged

Base automatically changed from mmagician-claude/batch-kernel-skeleton to next June 3, 2026 07:39

claude added 4 commits June 3, 2026 09:43

style: use the '# =>' stack-comment convention in the batch kernel masm

feeb1cc

Match the operand-stack (# =>) and advice-stack (# AS =>) comment style used throughout the rest of the protocol assembly.

mmagician force-pushed the mmagician-claude/batch-kernel-logic branch from 093ac8e to 622bee3 Compare June 3, 2026 12:32

claude added 7 commits June 3, 2026 12:47

mmagician commented Jun 4, 2026

View reviewed changes

huitseeker reviewed Jul 2, 2026

View reviewed changes

greenhat mentioned this pull request Jul 5, 2026

test: implement the protocol batch kernel in Rust 0xMiden/compiler#1242

Merged

greenhat mentioned this pull request Jul 10, 2026

Implement batch kernel in Rust 0xMiden/compiler#1158

Closed

Merge remote-tracking branch 'origin/next' into mmagician-claude/batc…

dc7558f

…h-kernel-logic # Conflicts: # crates/miden-protocol/src/batch/batch_id.rs # crates/miden-protocol/src/batch/kernel.rs # crates/miden-tx-batch/src/verifier.rs

mmagician requested a review from zeapoz August 11, 2026 07:13

zeapoz reviewed Aug 11, 2026

View reviewed changes

zeapoz mentioned this pull request Aug 17, 2026

chore: address batch kernel review comments #3615

Merged

zeapoz and others added 8 commits August 17, 2026 15:05

chore: address review comments (#3615)

d7973e8

Update crates/miden-protocol/asm/kernels/batch/lib/epilogue.masm

43ffbc1

Co-authored-by: zeapoz <zeapo@pm.me>

pull out shared errors into errors.masm

0914d80

style(batch-kernel): format constants to match repo conventions

f94484c

Apply the constant/error formatting used across the migrated kernel MASM: spaces around =, plain # doc comments on constants, and wrapping definitions that exceed 100 columns onto an indented string line.

style(batch-kernel): wrap comment lines exceeding 100 columns

150bc93

Merge branch 'next' into mmagician-claude/batch-kernel-logic

b9194f6

mmagician requested review from Fumuran, PhilippGackstatter, huitseeker, partylikeits1983 and zeapoz August 18, 2026 11:10

mmagician mentioned this pull request Aug 18, 2026

feat(batch): construct BatchNoteTree during batch construction #3022

Draft

PhilippGackstatter reviewed Aug 19, 2026

View reviewed changes

partylikeits1983 reviewed Aug 19, 2026

View reviewed changes

Fumuran reviewed Aug 19, 2026

View reviewed changes

PhilippGackstatter reviewed Aug 20, 2026

View reviewed changes

-    add.1
-end
+    add.1
+    # => [idx + 1, absorbed_count, num]
+end

-#! Inputs:  [KEY, write_ptr]
+#! Inputs:
+#!   Operand stack: [KEY, write_ptr]
+#!   Advice map: {
+#!     INPUT_NOTES_COMMITMENT_i: [(NULLIFIER, EMPTY_OR_COMMITMENT)]
+#!   }

		# A length that is not a multiple of 8 felts wraps `num_notes` (field `div`) to a non-u32
		# felt, which the range check below rejects.

	# => [idx+1, absorbed_count, num] (absorbed_count + 1 if entry was not erased)
	# => [idx+1, absorbed_count, num]

Uh oh!

Conversation

mmagician commented May 12, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

What this does

Prologue

Verification of data layers

Loading "global" notes

Note tracker

Note erasure

Note matching

Epilogue

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Choose a reason for hiding this comment

Uh oh!

zeapoz left a comment

Choose a reason for hiding this comment

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

Uh oh!

PhilippGackstatter left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

mmagician commented May 12, 2026 •

edited

Loading