Recursive verifier API by Al-Kindi-0 · Pull Request #3422 · 0xMiden/miden-vm

Al-Kindi-0 · 2026-07-24T13:54:01Z

Reworks recursive verification around a canonical execution claim. Resolves #3250 (and #2045).

The statement a proof attests is now an ExecutionClaim — (program_root, kernel_commitment, stack_inputs, stack_outputs) — with a domain-tagged commitment bound into the Fiat-Shamir transcript, so a proof is bound to exactly its claim. The deferred obligation D is returned by verification, never accepted from callers.

The API changes are for:

Native — Verifier::verify(proof, claim) and verify_partial(proof, claim); verify_partial returns the deferred obligation as a #[must_use] Unsettled token that the caller settles or re-exposes.

MASM — exec.vm::verify_vm_proof [claim_ptr] -> [D, num_queries, query_pow_bits, deep_pow_bits, folding_pow_bits]. The caller stages the 40-felt claim in memory; the kernel-digest witness is fetched from the advice map under the claim's kernel commitment and bound-checked before use; the proof is consumed from the advice stack (or fetched by request_key). The verifier returns the deferred root together with the proof's transcript-bound security parameters and applies no acceptance policy of its own — callers grade the parameters (e.g. sys::vm::conjectured_security_level + a >= 96 threshold; shown in the e2e tests). miden_verifier::recursive builds the advice.

…ectors - ExecutionClaim (P, K, I, O) with a normative 40-felt encoding and a domain-tagged commitment (CLAIM_HASH), mirrored in MASM by sys::vm::claim::claim_hash - domain tags are registered numeric selectors per the domain-separation RFC (0xMiden/crypto#1026); first provisional registry entries live in miden_core::program::domain - [BREAKING] kernel commitments are now domain-tagged; the three computation sites (KernelDescriptor::commitment, air::hash_kernel_digests, MASM kernel_H) are unified and pinned together by tests - add hash_elements_in_domain to the Poseidon2 MASM module, including the empty-input padding-marker rule, with Rust<->MASM cross-tests

- MidenMultiAir::observe now absorbs a single block [CLAIM_HASH | deferred_root]; with RELATION_DIGEST pre-loaded in the challenger capacity, the transcript realizes H(RELATION_DIGEST || CLAIM_HASH || D) - MASM: the six-block statement absorption (kernel_H|P, D|pad, four blocks of stack I/O) becomes compute_claim_hash + one absorbed block [CLAIM_HASH | D]; the stack I/O is still copied into the ACE READ region and the kernel digests still feed the LogUp boundary fold

…bligations - verify(proof, claim) verifies fully settled packages; verify_unsettled returns the deferred obligation as a #[must_use] Unsettled token consumable only by settle(pending, evidence, budget) - ExecutionProof now carries the statement-bound deferred_root plus optional settlement evidence; the old verify / verify_with_max_deferred_elements entrypoints are removed and all callers construct ExecutionClaim

…claim region - exec.vm::verify_proof becomes exec.vm::verify_vm_proof with inputs [claim_ptr, kernel_ptr, num_kernel_digests] and output [D], returning the deferred obligation instead of dropping it - the verifier computes the kernel commitment into the claim region via the new sys::vm::claim::kernel_commitment export and binds the transcript with sys::vm::claim::claim_commitment

- core::program::request_key(verifier_root, claim_commitment) and its MASM mirror sys::vm::claim::request_key derive the advice-map key H(claim_commitment ‖ verifier_root) under registered request domain id 34 - register_proof_package (test-utils) keys a package's advice-stack stream by request_key

…ed proof delivery The producer side (miden_verifier::recursive) builds the advice the MASM verifier consumes and registers proof packages in the advice map under H(verifier_root, claim_commitment); the consumer side gains sys::vm::verify_vm_proof_from_claim, which derives the claim commitment from the caller-staged claim, fetches its proof by content, and verifies it. CoreLibrary::recursive_verifier_root exposes the root packages are keyed by.

Replace the exact-parameter policy in the recursive verifier with a graded one. sys::vm::verify_vm_proof_from_claim now computes the attained conjectured security level from the transcript-bound parameters and returns it with the deferred root ([security_level, D]); the canonical verify_vm_proof wrapper thresholds it (>= 96) and returns [D]. Any parameter set reaching the target now verifies under one unchanged inner root, with the threshold as wrapper policy.

huitseeker · 2026-07-28T19:10:06Z

-    push.ACCEPTABLE_FOLDING_POW_BITS assert_eq.err="folding_pow_bits does not match acceptable security policy"
+    push.CONJECTURED_BITS_PER_QUERY_FP mul
+    u32shr.16
+    exec.constants::get_query_pow_bits add


The old wrapper required deep_pow_bits = 12 and folding_pow_bits = 4, but this grade only reads the query count and query PoW. The generic verifier only checks that the other two values are below 32, so a proof built with both set to zero still gets 96 for (27, 17).

That removes both intermediate grinding steps while reporting the same security level which sounds suboptimal.

Should we keep minimum checks for these fields?

Note that we have removed the wrapper and the core MASM verifier now returns the proof parameters, including the pow_bits.
It is correct that for conjectured security only the query phase pow matters. So the current conjectured security estimator only takes into account the query phase pow.
An upcoming proven security estimator will take all of the pow into account.

A question then is what security notion should we go with for mainnet. If we go with conjectured, then we can set deep_pow_bits and folding_pow_bits to zero and gain a few ms in proving times.

huitseeker · 2026-07-28T19:10:10Z

-    // Mirrors `ExecutionProof::security_level` until the STARK security estimator is available.
+    // TODO: placeholder for the precompile-VM proof's security level. Blocked on the
+    // precompile-VM security estimator (does not exist yet); wire together with the VM-side
+    // native level via `miden_air::config`. `verify` returns `min(vm_level, this)`, so this must


precompile_pcs_params() still uses (num_queries, query_pow_bits) = (27, 16), which the estimator added here rates at 95 bits.

huitseeker · 2026-07-28T19:10:13Z

+use crate::Felt;
+
+/// Registered domain id for the kernel commitment.
+pub const KERNEL_COMMITMENT_DOMAIN_ID: u32 = 32;


Nit: the (draft!) registry in 0xMiden/crypto#1026 reserved 0x010000..0x01ffff for miden-vm; IDs below 0x010000 belong to miden-crypto.

Using 32 here puts these consensus tags in crypto's range and would allows a future crypto entry to reuse them. If we keep the allocated ranges, wouldn't we need to allocate these three IDs from the VM range?

Good catch, and fixed it now though these are likely to change when we land the domain separation work

huitseeker · 2026-07-28T19:10:16Z

 | ----------- | ------------- |
 | load_air_context | Loads the VM-specific AIR context used by the generic STARK verifier.<br /><br />Advice supplies log heights in fixed instance order:<br />[log_core, log_chiplets, log_poseidon2_permutation]<br /><br />Writes per-AIR log heights, the maximum log height, ORDER_TAG, RELATION_DIGEST, and<br />ACE_REGISTRY_ROOT to memory.<br /> |
-| verify_proof | Verifies a STARK proof attesting to the correct execution of a program in the Miden VM.<br /><br />Security parameters (num_queries, query_pow_bits, deep_pow_bits, folding_pow_bits) are<br />loaded from the advice stack, validated against the acceptable security policy, and<br />stored in memory for use by the generic verifier.<br /><br />- Public inputs contain fixed-size input/output stacks, the program digest, and kernel procedure<br />digests.<br />- The wrapper records the AIR context before calling the generic STARK verifier.<br />- The constraints evaluator authenticates the ACE program selected by the derived proof order.<br /><br />The kernel-procedure digests and the stack i/o are read from caller memory at the<br />supplied `kernel_ptr` and `stack_io_ptr`; the program digest is supplied as an operand word; the<br />final deferred root is loaded from the advice stack. `verify_proof` stages the reduced-inputs<br />block (kernel_H \| program_digest \| deferred_root \| pad) before the transcript starts.<br /><br />Inputs:  [kernel_ptr, num_kernel_digests, stack_io_ptr, PROG0, PROG1, PROG2, PROG3]<br />Outputs: []<br /> |
+| verify_vm_proof_from_claim | Verifies a proof of the caller-staged execution claim, fetched from the advice map by<br />content.<br /><br />The caller populates the claim region with its own trusted P, I, O (K's slot may be left<br />unset) and supplies the kernel digest witness. This procedure materializes K from the<br />witness, derives the claim commitment from the completed region, fetches the registered<br />proof from the advice map under `request_key(verifier_root, claim_commitment)` (the verifier<br />root via `procref` of `verify_vm_proof` itself), and verifies it. The derived commitment is<br />both the fetch address and what verification binds, so consistency needs no check: a wrong<br />or substituted package fails verification against the caller's claim.<br /><br />Inputs:  [claim_ptr, kernel_ptr, num_kernel_digests, ...]<br />Outputs: [D, ...]<br /><br />Where:<br />- claim_ptr is the word-aligned address of the caller's claim region (40 felts), with P at +0,<br />I at +8, and O at +24 already populated from the caller's own inputs; K (+4) is written<br />here (and rederived by the verifier from the same witness).<br />- kernel_ptr / num_kernel_digests locate the kernel digest witness.<br />- D is the deferred root bound by the verified statement.<br /> |


These generated rows describe the entrypoints backwards. verify_vm_proof is now the commitment-first advice-map wrapper, while verify_vm_proof_from_claim takes only claim_ptr, consumes the proof stream, and returns [security_level, D] .. and neither accepts the kernel pointer and count shown here.

Does this need re-generation? It should also fix the stale stage_boundary_inputs row.

Regenerated and should be good now

verify_vm_proof [claim_ptr] -> [D, num_queries, query_pow_bits, deep_pow_bits, folding_pow_bits] verifies the caller-staged claim and returns the deferred obligation and the proof's security parameters. The parameters are bound into the Fiat-Shamir transcript by the generic verifier, so a proof cannot claim parameters it was not produced with; returning them lets each consumer grade and threshold under its own policy. An estimate or policy change therefore never moves the verifier's root - request keys and registered proof packages stay valid across such changes. conjectured_security_level becomes a pure estimator over the returned parameters ([num_queries, query_pow_bits] -> [level]).

query_pow_bits 16 -> 17 in precompile_pcs_params, matching miden_air::config::pcs_params again: the recalibration that moved the core preset to a 96-bit conjectured level had missed this mirror, leaving the precompile stack graded at 95.

The draft registry (0xMiden/crypto#1026) assigns 0x010000..0x01ffff to miden-vm; the provisional ids 32/33/34 sat in miden-crypto's range. Kernel / claim / request are now 0x010000 / 0x010001 / 0x010002 (selectors 0x01000001 / 0x01000101 / 0x01000201), and the domain module doc cites the range allocation. Every claim commitment, kernel commitment, and request key changes value.

regression tests for the kernel-witness-to-K binding (mutation-tested), the top-level oversized-witness bound, the returned security-parameter tuple across every e2e config, downward-forge transcript rejection, and the preset's 96-bit calibration

huitseeker

This overall looks good, though there are some check and test gaps in the PR, see inline.

huitseeker · 2026-07-31T15:31:52Z

+/// [`MAX_STARK_PROOF_BYTES`].
+fn deserialize_proof(proof_bytes: &[u8]) -> Result<P2ProofData, RecursiveAdviceError> {
+    let encoding_config = wincode::config::Configuration::default()
+        .with_preallocation_size_limit::<MAX_STARK_PROOF_BYTES>();


ExecutionProof::from_parts can hold more than 64 MiB. This setting caps each sequence allocation, not the total input, and ordinary wincode decoding accepts trailing bytes.

A valid proof prefix with a large suffix can reach advice_inputs, while verify_stark_proof rejects it at verifier/src/lib.rs:302.

It would be good to match the native proof-size check, and to use exact decoding here.

huitseeker · 2026-07-31T15:31:55Z

+        StarkProof::new(stark.bytes().to_vec(), stark.hash_fn()),
+        DeferredProof::empty(),
+    );
+    assert!(verify(tampered, claim).is_err());


Hmm, could we also verify the untampered proof before replacing its deferred material?

This removed the only positive top-level test for a valid DeferredProof::Stark; the current assertion still passes if final composed verification is broken, because it checks only the tampered package.

The inner deferred-proof tests do not exercise the outer VM proof against the returned root.

huitseeker · 2026-07-31T17:41:32Z

+    // (one per FRI round).
+    for batch_proof in pcs.deep_witnesses.iter().chain(pcs.fri_witnesses.iter()) {
+        let (tree, entries) = batch_proof_to_merkle(lmcs, batch_proof)?;
+        partial_trees.push(tree);


Could we create store before this loop and extend it from tree.inner_nodes() here? partial_trees is only retained for the loop below, so inserting each tree immediately removes the intermediate Vec and keeps the ownership flow local.

huitseeker

Some nits inline, but overall LGTM

huitseeker · 2026-07-31T20:02:52Z

+
+    let encoding_config = wincode::config::Configuration::default()
+        .with_preallocation_size_limit::<MAX_STARK_PROOF_BYTES>();
+    deserialize_serde_exact::<P2ProofData, _>(proof_bytes, encoding_config)


So, recursive advice rejects proof bytes that native verify still accepts.

Appending trailing bytes to a valid inner STARK proof returns Ok(96) natively but reaches TrailingBytes here; the precompile verifier uses the same permissive decode as the native path.

Could we use exact decoding in all three places (ideally a strict one) so they agree on which encodings are valid?

huitseeker · 2026-07-31T20:02:59Z

-    Verifier::new().verify(program_info, stack_inputs, stack_outputs, proof)
+/// Wire-backed deferred proofs are partial/delegable proof material and are rejected here; use
+/// [`Verifier::verify_partial`] to verify and hydrate wire-backed partial proofs.
+pub fn verify(proof: ExecutionProof, claim: ExecutionClaim) -> Result<u32, VerificationError> {


Nit: this changes the public call to (proof, ExecutionClaim), but miden-vm/README.md:143-175 still lists four arguments and calls Verifier::new().verify(ProgramInfo::from(program), StackInputs::default(), expected_outputs, proof).

bobbinth

Looks good! Thank you! Not a very deep review, but I left some comments inline. Some bigger API refactoring should probably be addressed as a part of #3437, but others should be addressed in a follow-up PR.

bobbinth · 2026-08-02T00:03:06Z

+fn deserialize_serde_exact<'de, T, C>(mut bytes: &'de [u8], _: C) -> wincode::ReadResult<T>
+where
+    C: wincode::config::Config,
+    SerdeCompat<T>: wincode::SchemaRead<'de, C, Dst = T>,
+{
+    let value = <SerdeCompat<T> as wincode::SchemaRead<'de, C>>::get(bytes.by_ref())?;
+    if bytes.is_empty() {
+        Ok(value)
+    } else {
+        Err(wincode::error::trailing_bytes())
+    }
+}


This function feels out of place here. It also looks like a duplicate of a function with the similar name in the preocmpiles-prover crate. Should we move it to some "utils" module and de-duplicate?

Agreed, moved this to miden-serde-utils

bobbinth · 2026-08-02T00:08:46Z

    pub fn verify(
        &self,
-        program_info: ProgramInfo,
-        stack_inputs: StackInputs,
-        stack_outputs: StackOutputs,
        proof: ExecutionProof,
+        claim: ExecutionClaim,
    ) -> Result<u32, VerificationError> {


Not related to this PR, but I think we should change the API in a couple of ways to align it more with the MASM API:

We shouldn't return the security level as it requires making some opinionated assumptions. Instead we could return the proof parameters (number of queries, grinding factors etc.).

verify() should return something like Option<DeferredState> in case the proof contains unverified deferred state.

Agreed, we can do it in the other PR #3437 as it makes more sense there

bobbinth · 2026-08-02T00:16:12Z

+#[derive(Debug, Clone, Eq, PartialEq)]
+pub struct RecursiveVerifierInputs {
+    /// The advice-stack stream, in the order `verify_vm_proof` (with the standard
+    /// staging prologue) consumes it.
+    pub advice_stack: Vec<Felt>,
+    /// Merkle store backing the query openings (`mtree_get` authentication paths).
+    pub store: MerkleStore,
+    /// Content-addressed advice-map entries: query rows (`leaf_hash -> leaf_data`), the ACE
+    /// circuit, and the kernel digest witness under K.
+    pub advice_map: Vec<(Word, Vec<Felt>)>,
+    /// Commitment to the execution claim: the content address (paired with a verifier root) the
+    /// proof stream is registered under.
+    pub claim_commitment: Word,
+}


Do we really need this type? AFAICT, this is basically AdviceInputs and claim_commitment. If we do want to keep it, it should probably look more like:

pub struct RecursiveVerifierInputs { advice: AdviceInputs, claim_commitment: Word, }

bobbinth · 2026-08-02T00:20:24Z

+pub fn advice_inputs(
+    proof: &ExecutionProof,
+    claim: &ExecutionClaim,
+) -> Result<RecursiveVerifierInputs, RecursiveAdviceError> {


If we do keep the RecursiveVerifierInputs struct, I'd convert this function into the constructor of this struct - something like:

impl RecursiveVerifierInputs { pub fn new( proof: &ExecutionProof, claim: &ExecutionClaim, ) -> Result<Self, RecursiveVerifierInputsError> { ... } }

bobbinth · 2026-08-02T00:22:42Z

+    pub fn into_request_package(mut self, verifier_root: Word) -> Self {
+        let key = request_key(verifier_root, self.claim_commitment);
+        let proof_stream = core::mem::take(&mut self.advice_stack);
+        self.advice_map.push((key, proof_stream));
+        self
+    }


Question: why do we want to provide the verifier root separately from struct construction? Building on the previous comment, why not make the constructor look like this:

impl RecursiveVerifierInputs { pub fn new( verifier_root: Word, proof: &ExecutionProof, claim: &ExecutionClaim, ) -> Result<Self, RecursiveVerifierInputsError> { ... } }

Added for_request(verifier_root, proof, claim) for request packages. I kept new(proof, claim) for direct verifier invocation and made the packaging step private.

bobbinth · 2026-08-02T01:10:10Z

+#! of the flattened digests, length-bound by the sponge's padding rule, in the descriptor's
+#! canonical order.
+#!
+#! Inputs:  [kernel_ptr, num_kernel_digests, ...]


nit: I'd probably rename num_kernel_digests into num_kernel_procedures as it makes the variable content a bit more self-evident.

bobbinth · 2026-08-02T01:12:58Z

+#!
+#! Inputs:  [num_queries, query_pow_bits, ...]
+#! Outputs: [level, ...]
+pub proc conjectured_security_level


nit: I'd rename this into something like compute_conjectured_security_level to have the procedure name start with an action verb.

bobbinth · 2026-08-02T01:15:27Z

+#! Inputs:  [claim_ptr, ...]
+#! Outputs: [D, num_queries, query_pow_bits, deep_pow_bits, folding_pow_bits, ...]


Question: why not pass CLAIM_COMMITMENT instead of claim_ptr? We should be able to write the pre-image of the claim commitment into the local procedure memory pretty easily.

bobbinth · 2026-08-02T01:16:05Z

+#! Where:
+#! - claim_ptr is word-aligned; its 40-felt region ends at or before
+#!   `constants::verifier_memory_start`.
+#! - D is the deferred root bound by the verified statement.


I would mention here explicitly that if D == EMPTY_WORD then the were not deferred computations.

bobbinth · 2026-08-02T01:16:30Z

+#! - D is the deferred root bound by the verified statement.
+#! - num_queries, query_pow_bits, deep_pow_bits, folding_pow_bits are the proof's
+#!   transcript-bound security parameters.
+pub proc verify_vm_proof


It would be good to start adding signatures to procedures.

Al-Kindi-0 · 2026-08-02T10:37:25Z

@bobbinth , will open a small followup PR to address your feedback

Al-Kindi-0 mentioned this pull request Jul 24, 2026

Define the recursive verifier API for structured Miden VM proof verification #3250

Closed

Al-Kindi-0 added 7 commits July 24, 2026 18:20

refactor: rename the reduced-inputs window to boundary inputs

3e4fd43

Al-Kindi-0 force-pushed the al/verifier-api branch from 4e65860 to 6fa963f Compare July 24, 2026 18:51

Al-Kindi-0 added 4 commits July 24, 2026 23:40

chore: fix CI

346c525

refactor: flatten ExecutionClaim and rename program_hash to program_root

2013d9a

feat: make verify_vm_proof commitment-first

9d14b7f

huitseeker reviewed Jul 28, 2026

View reviewed changes

Al-Kindi-0 added 8 commits July 30, 2026 13:27

Merge remote-tracking branch 'origin/next' into al/verifier-api

d42dbbb

chore: changelog

9af0e44

chore: misc. comment fixes

08c4cae

Merge branch 'next' into al/verifier-api

7b006c6

Al-Kindi-0 marked this pull request as ready for review July 31, 2026 10:05

Al-Kindi-0 added 3 commits July 31, 2026 15:39

refactor: drop the unused claim-encoding advice-map entry

dd3e526

fix: correct recursive verifier memory boundaries

a48c620

fix: bind STARK transcripts to supplied PCS parameters

bb6cc65

huitseeker reviewed Jul 31, 2026

View reviewed changes

chore: address feedback

28dfe43

huitseeker approved these changes Jul 31, 2026

View reviewed changes

chore: address feedback 2

d0448ce

Al-Kindi-0 added 3 commits August 1, 2026 02:23

Merge branch 'next' into al/verifier-api

9909b50

Merge branch 'next' into al/verifier-api

8dc08fc

Merge branch 'next' into al/verifier-api

3d5c46a

Al-Kindi-0 merged commit 752e8de into next Aug 1, 2026
30 checks passed

Al-Kindi-0 deleted the al/verifier-api branch August 1, 2026 09:20

bobbinth reviewed Aug 2, 2026

View reviewed changes

Al-Kindi-0 mentioned this pull request Aug 2, 2026

Recursive verifier review followups #3447

Merged

adr1anh mentioned this pull request Aug 3, 2026

feat(prover): add composable prover interface #3437

Open

7 tasks

Al-Kindi-0 mentioned this pull request Aug 4, 2026

Add proof security parameters to the block header 0xMiden/protocol#3467

Open

		#! Inputs: [claim_ptr, ...]
		#! Outputs: [D, num_queries, query_pow_bits, deep_pow_bits, folding_pow_bits, ...]

Uh oh!

Conversation

Al-Kindi-0 commented Jul 24, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

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!

Choose a reason for hiding this comment

Uh oh!

huitseeker 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!

huitseeker 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!

Uh oh!

bobbinth 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!

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

Al-Kindi-0 commented Jul 24, 2026 •

edited

Loading