feat(batch kernel): wire up INPUT_NOTES_COMMITMENT & note erasure

CHANGELOG.md

@@ -4,6 +4,8 @@
 
 ### Features
 
+- [BREAKING] Implemented partial batch kernel verification to check the transaction list against `BATCH_ID` and compute `INPUT_NOTES_COMMITMENT`; `BatchExecutor::execute` now additionally takes caller `AdviceInputs` ([#2905](https://github.com/0xMiden/protocol/pull/2905)).
+
 ### Changes
 
 - [BREAKING] Moved the internal shared helpers of `miden::protocol::input_note`, `miden::protocol::active_note`, and the note memory-write helpers into private `input_note_internal` and `note_internal` modules ([#3501](https://github.com/0xMiden/protocol/pull/3501)).

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

@@ -0,0 +1,184 @@
+use miden::core::crypto::hashes::poseidon2
+
+use miden::batch_kernel::memory
+use {
+    INPUT_NOTE_CONSUMPTION_OFFSET,
+    NOTE_ENTRY_FELT_LEN,
+    OUTPUT_NOTE_IS_CREATED_OFFSET,
+} from miden::batch_kernel::memory
+use {ERR_BATCH_NOTE_CONSUMED_BEFORE_CREATED} from miden::batch_kernel::errors
+
+# ERRORS
+# =================================================================================================
+
+const ERR_BATCH_INPUT_NOTE_NOT_CONSUMED =
+    "an input-note list entry was not consumed by any transaction"
+
+const ERR_BATCH_OUTPUT_NOTE_NOT_CREATED =
+    "an output-note list entry was not created by any transaction"
+
+# ASSERTIONS
+# =================================================================================================
+
+#! Asserts every output-note list entry was created by exactly one transaction (with the per-tx
+#! binding, this proves the list is exactly the union of the per-transaction output notes, so a host
+#! cannot fabricate an erasure with a note no transaction creates).
+#!
+#! The matching input-note checks (every entry consumed exactly once, none left pending-erasure) are
+#! folded into the single pass in [`compute_input_notes_commitment`].
+#!
+#! Inputs:  []
+#! Outputs: []
+proc assert_all_output_notes_created
+    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]
+    while.true
+        dup exec.memory::output_note_flags_ptr add.OUTPUT_NOTE_IS_CREATED_OFFSET mem_load
+        # => [is_created, idx, num_output_notes]
+        assert.err=ERR_BATCH_OUTPUT_NOTE_NOT_CREATED
+        # => [idx, num_output_notes]
+        add.1
+        # => [idx+1, num_output_notes]
+        dup.1 dup.1 neq
+        # => [should_loop, idx+1, num_output_notes]
+    end
+    drop drop
+end
+
+# INPUT NOTES COMMITMENT
+# =================================================================================================
+
+#! 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
+    # => [entry_ptr]
+    dup add.NOTE_ENTRY_FELT_LEN swap
+    # => [entry_ptr, end_ptr]
+    exec.memory::load_batch_hasher_state
+    # => [RATE0, RATE1, CAPACITY, entry_ptr, end_ptr]
+    exec.poseidon2::absorb_double_words_from_memory
+    # => [RATE0', RATE1', CAPACITY', end_ptr, end_ptr]
+    exec.memory::save_batch_hasher_state
+    # => [end_ptr, end_ptr]
+    drop drop
+end
+
+#! Processes one input-note list entry: asserts the entry was consumed exactly once and is not
+#! left expected-to-be-erased, then absorbs it into the batch hasher unless it was erased.
+#!
+#! The absorbed_count is only incremented by 1 if the entry was not erased (erasure != 2).
+#!
+#! Inputs:  [idx, absorbed_count, num]
+#! Outputs: [idx + 1, absorbed_count, num]
+proc process_input_entry
+    # Assert this entry was consumed exactly once and is not left expected-to-be-erased.
+    dup exec.memory::input_note_flags_ptr
+    # => [flags_ptr, idx, absorbed_count, num]
+    dup add.INPUT_NOTE_CONSUMPTION_OFFSET mem_load
+    # => [consumption, flags_ptr, idx, absorbed_count, num]
+    assert.err=ERR_BATCH_INPUT_NOTE_NOT_CONSUMED
+    # => [flags_ptr, idx, absorbed_count, num]
+    mem_load
+    # => [erasure, idx, absorbed_count, num]
+    dup neq.1 assert.err=ERR_BATCH_NOTE_CONSUMED_BEFORE_CREATED
+    # => [erasure, idx, absorbed_count, num]
+
+    # Absorb the entry unless it was erased (created-and-consumed in this batch).
+    neq.2
+    # => [not_erased, idx, absorbed_count, num]
+    if.true
+        dup exec.absorb_input_entry
+        swap add.1 swap
+        # => [idx, absorbed_count+1, num]
+    end
+    add.1
+end
+
+#! Computes INPUT_NOTES_COMMITMENT as the sequential poseidon2 hash of the non-erased
+#! `(NULLIFIER, NOTE_ID_OR_EMPTY)` entries of the nullifier-sorted input-note list (entries with
+#! erasure flag == 2 are skipped).
+#!
+#! The single pass over the input entries also enforces the epilogue invariants on each entry: it
+#! was consumed exactly once (consumption == 1) and is not left expected-to-be-erased (erasure != 1,
+#! i.e. any created-and-consumed note had its creator processed).
+#!
+#! Inputs:  []
+#! Outputs: [INPUT_NOTES_COMMITMENT]
+proc compute_input_notes_commitment
+    # Initialize the batch hasher state in memory.
+    exec.poseidon2::init_no_padding
+    exec.memory::save_batch_hasher_state
+
+    exec.memory::get_num_input_notes
+    push.0 push.0
+    # => [idx, absorbed_count, num]
+    dup dup.3 neq
+    # => [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)
+        dup dup.3 neq
+        # => [should_loop, idx+1, absorbed_count, num]
+    end
+    # => [idx, absorbed_count, num]
+    drop swap drop
+    # => [absorbed_count]
+
+    # 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
+end
+
+# OUTPUT NOTES COMMITMENT
+# =================================================================================================
+
+#! Computes the batch's output-notes commitment (the batch note tree root).
+#!
+#! Placeholder: returns the empty word until the batch note tree is wired up.
+#!
+#! Inputs:  []
+#! Outputs: [OUTPUT_NOTES_COMMITMENT]
+#!
+#! TODO: hash the batch's output notes into the batch note tree (SMT) root.
+proc compute_output_notes_commitment
+    padw
+end
+
+# EPILOGUE
+# =================================================================================================
+
+#! Verifies the note-tracking results and computes the batch's note commitments.
+#!
+#! Asserts every output-note list entry was created, then computes the input- and output-notes
+#! commitments. The per-input-entry invariants (consumed exactly once, no pending erasure) are
+#! enforced inside the input-commitment pass.
+#!
+#! Inputs:  []
+#! Outputs: [INPUT_NOTES_COMMITMENT, OUTPUT_NOTES_COMMITMENT]
+#!
+#! TODO: authenticate unauthenticated, non-erased input notes against BLOCK_COMMITMENT's chain MMR.
+pub proc finalize
+    exec.assert_all_output_notes_created
+    exec.compute_output_notes_commitment
+    # => [OUTPUT_NOTES_COMMITMENT]
+    exec.compute_input_notes_commitment
+    # => [INPUT_NOTES_COMMITMENT, OUTPUT_NOTES_COMMITMENT]
+end

crates/miden-protocol/asm/kernels/batch/lib/errors.masm

@@ -0,0 +1,7 @@
+# Error constants shared by batch kernel modules.
+
+# ERRORS
+# =================================================================================================
+
+pub const ERR_BATCH_NOTE_CONSUMED_BEFORE_CREATED =
+    "an erased input note was consumed before the transaction that created it"