Recursive verifier API

CHANGELOG.md

@@ -3,6 +3,7 @@
 ## v0.28.0 (unreleased)
 
 #### Changes
+- [BREAKING] Reworked recursive verification around canonical execution claims: `ExecutionClaim` carries a domain-tagged commitment bound into the Fiat-Shamir statement; native verification becomes `Verifier::verify`/`verify_partial(proof, claim)` returning the deferred obligation as a `#[must_use]` token; the canonical MASM entrypoint becomes `exec.vm::verify_vm_proof [CLAIM_COMMITMENT] -> [D]`, with the claim, kernel witness, and proof delivered content-addressed through the advice map over the stream-level `exec.vm::verify_vm_proof_from_claim`; `miden_verifier::recursive` builds the advice ([#3422](https://github.com/0xMiden/miden-vm/pull/3422)).
 - `FastProcessor` `restore_call_state()` and `restore_context()` now return `OperationError::Internal` instead of panicking on empty stacks ([#3371](https://github.com/0xMiden/miden-vm/pull/3371), fixes [#3296](https://github.com/0xMiden/miden-vm/issues/3296)).
 
 - [BREAKING] Renamed module and kernel metadata APIs from `ModuleInfo`/`Kernel` to `ModuleDescriptor`/`KernelDescriptor`, including matching module descriptor method names ([#3356](https://github.com/0xMiden/miden-vm/pull/3356)).

air/src/config.rs

@@ -63,8 +63,39 @@ pub const FOLDING_POW_BITS: usize = 4;
 pub const DEEP_POW_BITS: usize = 12;
 /// Number of FRI query repetitions.
 const NUM_QUERIES: usize = 27;
-/// Proof-of-work bits for query phase.
-const QUERY_POW_BITS: usize = 16;
+/// Proof-of-work bits for query phase, calibrated so that with 27 queries
+/// `conjectured_security_level(27, 17) == 96` — exactly the recursion wrapper's acceptance
+/// target (`CONJECTURED_SECURITY_TARGET` in `sys/vm/mod.masm`), with no margin: lowering this
+/// or the per-query rate would drop the preset below the target and reject every proof.
+const QUERY_POW_BITS: usize = 17;
+
+// CONJECTURED SECURITY LEVEL
+// ================================================================================================
+
+/// Fixed-point (16 fractional bits) conjectured security bits contributed per FRI query, for
+/// this configuration's blowup (8) and challenge field (~128 bits):
+/// `floor(-log2(rho + eta) * 2^16)` with `rho = 1/8` and the random-words cutoff
+/// `eta = log2(e/rho) * rho / 128` (<https://eprint.iacr.org/2025/2010>, section 1.5), i.e.
+/// ~2.9508 bits per query. Must match the constant in `crates/lib/core/asm/sys/vm/mod.masm`
+/// (enforced by cross-tests).
+pub const CONJECTURED_BITS_PER_QUERY_FP: u64 = 193_382;
+
+/// Cap on any reported security level: the minimum of the challenge-field size and the
+/// commitment hash's collision resistance (both ~128 bits here).
+pub const MAX_SECURITY_LEVEL: u32 = 128;
+
+/// Returns the conjectured security level (in bits) attained by a proof with the given FRI
+/// query count and query-phase grinding bits, under this configuration's fixed blowup and
+/// challenge field.
+///
+/// The computation is integer fixed-point — `min((num_queries * C) >> 16 + query_pow, 128)` —
+/// so the MASM mirror can match it bit-for-bit; the constant is floored, so the result never
+/// exceeds the real-valued formula (conservative by at most one bit). `num_queries` is a FRI
+/// query count (the verifier bounds it to `<= 150`), so the product fits comfortably in a `u32`.
+pub fn conjectured_security_level(num_queries: u32, query_pow_bits: u32) -> u32 {
+    let fri_bits = ((num_queries as u64 * CONJECTURED_BITS_PER_QUERY_FP) >> 16) as u32;
+    (fri_bits + query_pow_bits).min(MAX_SECURITY_LEVEL)
+}
 
 /// Default PCS parameters shared by all hash function configurations.
 pub fn pcs_params() -> PcsParams {
@@ -452,4 +483,104 @@ mod tests {
             "RELATION_DIGEST in config.rs is stale. Regenerate with: {REGEN_HINT}"
         );
     }
+
+    /// The integer fixed-point conjectured-security computation must reproduce the
+    /// reference values of the random-words formula (2025/2010, section 1.5), precomputed
+    /// externally; in particular the calibration points (27, 16) -> 95 and (27, 17) -> 96.
+    #[test]
+    fn conjectured_security_level_matches_reference_vectors() {
+        static VECTORS: &[(u32, u32, u32)] = &[
+            (1, 0, 2),
+            (1, 4, 6),
+            (1, 16, 18),
+            (1, 17, 19),
+            (1, 24, 26),
+            (1, 30, 32),
+            (1, 100, 102),
+            (5, 0, 14),
+            (5, 4, 18),
+            (5, 16, 30),
+            (5, 17, 31),
+            (5, 24, 38),
+            (5, 30, 44),
+            (5, 100, 114),
+            (22, 0, 64),
+            (22, 4, 68),
+            (22, 16, 80),
+            (22, 17, 81),
+            (22, 24, 88),
+            (22, 30, 94),
+            (22, 100, 128),
+            (27, 0, 79),
+            (27, 4, 83),
+            (27, 16, 95),
+            (27, 17, 96),
+            (27, 24, 103),
+            (27, 30, 109),
+            (27, 100, 128),
+            (28, 0, 82),
+            (28, 4, 86),
+            (28, 16, 98),
+            (28, 17, 99),
+            (28, 24, 106),
+            (28, 30, 112),
+            (28, 100, 128),
+            (43, 0, 126),
+            (43, 4, 128),
+            (43, 16, 128),
+            (43, 17, 128),
+            (43, 24, 128),
+            (43, 30, 128),
+            (43, 100, 128),
+            (64, 0, 128),
+            (64, 16, 128),
+            (100, 0, 128),
+            (128, 24, 128),
+            (150, 0, 128),
+            (150, 100, 128),
+            (255, 0, 128),
+        ];
+        for &(q, pow, expected) in VECTORS {
+            assert_eq!(
+                super::conjectured_security_level(q, pow),
+                expected,
+                "conjectured_security_level({q}, {pow})"
+            );
+        }
+    }
+
+    /// The fixed-point estimator must never overstate security relative to the true random-words
+    /// f64 formula, and must track it within one bit. This guards the conservative direction (the
+    /// dangerous one) against any future recalibration of `CONJECTURED_BITS_PER_QUERY_FP`.
+    #[test]
+    fn conjectured_security_level_never_overstates_true_formula() {
+        // The true per-query rate `b = -log2(rho + eta)` with `rho = 1/8` (blowup 8) and the
+        // random-words cutoff `eta = log2(e/rho) * rho / 128` (2025/2010, section 1.5).
+        let rho = 0.125_f64;
+        let eta = (core::f64::consts::LOG2_E + 3.0) * rho / 128.0;
+        let bits_per_query = -(rho + eta).log2();
+
+        // The compiled constant is exactly that rate in 16-fractional-bit fixed point.
+        assert_eq!(
+            super::CONJECTURED_BITS_PER_QUERY_FP,
+            (bits_per_query * 65536.0).floor() as u64,
+            "CONJECTURED_BITS_PER_QUERY_FP is stale relative to the random-words rate"
+        );
+
+        // Over the whole verifier domain (num_queries a u8, query_pow_bits < 32) the fixed-point
+        // level never exceeds the f64 formula and trails it by at most one bit.
+        for nq in 0u32..256 {
+            for pow in 0u32..32 {
+                let float_fri = (f64::from(nq) * bits_per_query) as u32;
+                let float_level = (float_fri + pow).min(super::MAX_SECURITY_LEVEL);
+                let fixed_level = super::conjectured_security_level(nq, pow);
+                let delta = i64::from(float_level) - i64::from(fixed_level);
+                assert!(
+                    (0..=1).contains(&delta),
+                    "num_queries={nq}, query_pow_bits={pow}: float={float_level}, \
+                     fixed={fixed_level} (delta={delta})"
+                );
+            }
+        }
+    }
 }

air/src/lib.rs

@@ -13,7 +13,10 @@ use miden_core::{
     WORD_SIZE, Word,
     deferred::DeferredRoot,
     field::ExtensionField,
-    program::{KernelDescriptor, MIN_STACK_DEPTH, ProgramInfo, StackInputs, StackOutputs},
+    program::{
+        KernelDescriptor, MIN_STACK_DEPTH, NUM_CLAIM_ELEMENTS, ProgramInfo, StackInputs,
+        StackOutputs,
+    },
 };
 use miden_crypto::stark::{
     air::{ReductionError, WindowAccess},
@@ -802,18 +805,15 @@ impl<EF: ExtensionField<Felt>> MultiAir<Felt, EF> for MidenMultiAir {
 
     /// Absorb statement-owned public inputs into the Fiat-Shamir challenger.
     ///
-    /// Uses a rate-aligned schedule: six 8-felt blocks, 48 felts total.
-    ///
-    /// ```text
-    /// [ kernel_H (4) | program_hash (4) ]
-    /// [ deferred_root (4) | 0,0,0,0 ]         trailing pad keeps the schedule rate-aligned
-    /// [ stack_inputs (16) ]                   two blocks
-    /// [ stack_outputs (16) ]                  two blocks
-    /// ```
+    /// One rate-aligned block: `[CLAIM_HASH (4) | deferred_root (4)]`, where `CLAIM_HASH` is the
+    /// canonical execution-claim commitment (see `miden_core::program::ExecutionClaim`) over
+    /// `program_hash ‖ kernel_H ‖ stack_inputs ‖ stack_outputs`. With the relation digest
+    /// pre-loaded in the challenger (see `config`), the transcript state after this block
+    /// realizes the factored statement binding `H(RELATION_DIGEST ‖ CLAIM_HASH ‖ D)`.
     ///
-    /// The kernel digests enter the transcript only through `kernel_H`
-    /// (see [`hash_kernel_digests`]), committing to the kernel with a fixed-size value instead
-    /// of the unbounded digest list.
+    /// The kernel digests enter the transcript only through `kernel_H` (see
+    /// [`hash_kernel_digests`]); the raw stack I/O and digest list remain public values for
+    /// constraint evaluation and are not separately absorbed.
     fn observe<C: CanObserve<Felt>>(
         &self,
         challenger: &mut C,
@@ -830,19 +830,16 @@ impl<EF: ExtensionField<Felt>> MultiAir<Felt, EF> for MidenMultiAir {
         let kernel_h = hash_kernel_digests(&aux_inputs[AUX_KERNEL_DIGESTS..]);
         let program_hash = &aux_inputs[AUX_PROGRAM_HASH..AUX_PROGRAM_HASH + WORD_SIZE];
         let deferred_root = &aux_inputs[AUX_DEFERRED_ROOT..AUX_DEFERRED_ROOT + WORD_SIZE];
-        let stack_io = air_inputs;
 
-        // Block 1: kernel_H | program_hash. Block 2: deferred_root | zero pad.
-        for &v in kernel_h.iter().chain(program_hash) {
-            challenger.observe(v);
-        }
-        for &v in deferred_root {
-            challenger.observe(v);
-        }
-        for _ in 0..WORD_SIZE {
-            challenger.observe(Felt::ZERO);
-        }
-        for &v in stack_io {
+        // Canonical claim encoding P ‖ K ‖ I ‖ O; the offset layout of
+        // `ExecutionClaim::to_elements`, pinned by `observe_matches_execution_claim_commitment`.
+        let mut claim = [Felt::ZERO; NUM_CLAIM_ELEMENTS];
+        claim[0..WORD_SIZE].copy_from_slice(program_hash);
+        claim[WORD_SIZE..2 * WORD_SIZE].copy_from_slice(&kernel_h);
+        claim[2 * WORD_SIZE..].copy_from_slice(air_inputs);
+        let claim_hash = miden_core::program::claim_commitment(&claim);
+
+        for &v in claim_hash.as_elements().iter().chain(deferred_root) {
             challenger.observe(v);
         }
     }
@@ -938,8 +935,9 @@ impl<EF: ExtensionField<Felt>> MultiAir<Felt, EF> for MidenMultiAir {
 /// Computes `kernel_H`, the fixed-size commitment to the kernel-procedure digests.
 ///
 /// This is the canonical [`KernelDescriptor::commitment`] value expressed over the flattened digest
-/// felts: the linear hash (`hash_elements`) of `kernel_felts`. The empty digest list yields
-/// `hash_elements(&[])`.
+/// felts: the domain-tagged linear hash (`hash_elements_in_domain` with
+/// [`miden_core::program::KERNEL_DOMAIN_TAG`]) of `kernel_felts`. The empty digest list yields
+/// the canonical empty-input value under the same domain.
 ///
 /// `kernel_H` is absorbed into the Fiat-Shamir transcript in place of the unbounded kernel
 /// digest list, committing to the kernel with a fixed-size value.
@@ -957,7 +955,11 @@ pub fn hash_kernel_digests(kernel_felts: &[Felt]) -> [Felt; WORD_SIZE] {
 }
 
 fn hash_kernel_input_felts(kernel_felts: &[Felt]) -> [Felt; WORD_SIZE] {
-    miden_core::chiplets::hasher::hash_elements(kernel_felts).into()
+    miden_core::chiplets::hasher::hash_elements_in_domain(
+        kernel_felts,
+        miden_core::program::KERNEL_DOMAIN_TAG,
+    )
+    .into()
 }
 
 // REDUCED-AUX BOUNDARY BUILDER
@@ -1082,6 +1084,27 @@ mod tests {
         )));
     }
 
+    #[test]
+    fn hash_kernel_digests_matches_kernel_descriptor_commitment() {
+        // The transcript-side helper and `KernelDescriptor::commitment` are two computations of
+        // the same normative value; this pins them together (including the empty kernel).
+        use miden_core::Word;
+
+        let word = |a: u64| -> Word {
+            [Felt::new_unchecked(a), Felt::new_unchecked(a + 1), Felt::ZERO, Felt::ONE].into()
+        };
+        for procs in [vec![], vec![word(10)], vec![word(10), word(20), word(30)]] {
+            let descriptor = KernelDescriptor::from_hashes(procs).unwrap();
+            let flattened: Vec<Felt> =
+                descriptor.proc_hashes().iter().flat_map(|w| w.as_elements().to_vec()).collect();
+            assert_eq!(
+                Word::new(hash_kernel_digests(&flattened)),
+                descriptor.commitment(),
+                "hash_kernel_digests diverged from KernelDescriptor::commitment"
+            );
+        }
+    }
+
     #[test]
     #[should_panic(expected = "kernel digest felts exceed KernelDescriptor::MAX_NUM_PROCEDURES")]
     fn hash_kernel_digests_rejects_too_many_digest_felts() {
@@ -1090,6 +1113,68 @@ mod tests {
         let _ = hash_kernel_digests(&kernel_felts);
     }
 
+    #[test]
+    fn observe_matches_execution_claim_commitment() {
+        // The transcript's statement block must open with exactly
+        // `ExecutionClaim::commitment()` for the same statement, followed by the deferred
+        // root — pinning `observe`'s inline claim encoding to the canonical one.
+        use miden_core::{field::QuadFelt, program::ExecutionClaim};
+
+        #[derive(Default)]
+        struct FeltSink {
+            observed: Vec<Felt>,
+        }
+        impl CanObserve<Felt> for FeltSink {
+            fn observe(&mut self, value: Felt) {
+                self.observed.push(value);
+            }
+        }
+
+        let word = |a: u64| -> Word {
+            [
+                Felt::new_unchecked(a),
+                Felt::new_unchecked(a + 1),
+                Felt::new_unchecked(a + 2),
+                Felt::new_unchecked(a + 3),
+            ]
+            .into()
+        };
+        let kernel = KernelDescriptor::from_hashes(vec![word(50), word(60)]).unwrap();
+        let program_hash = word(1);
+        let stack_inputs =
+            StackInputs::new(&[Felt::new_unchecked(5), Felt::new_unchecked(6)]).unwrap();
+        let stack_outputs = StackOutputs::new(&[Felt::new_unchecked(7)]).unwrap();
+        let deferred_root = word(90);
+
+        let claim = ExecutionClaim::from_program_info(
+            ProgramInfo::new(program_hash, kernel.clone()),
+            stack_inputs,
+            stack_outputs,
+        );
+
+        // air_inputs = I ‖ O; aux_inputs = P ‖ D ‖ kernel digest felts.
+        let mut air_inputs = [Felt::ZERO; NUM_PUBLIC_VALUES];
+        air_inputs[0..MIN_STACK_DEPTH].copy_from_slice(&stack_inputs[..]);
+        air_inputs[MIN_STACK_DEPTH..].copy_from_slice(&stack_outputs[..]);
+        let mut aux_inputs: Vec<Felt> = Vec::new();
+        aux_inputs.extend(program_hash.as_elements());
+        aux_inputs.extend(deferred_root.as_elements());
+        aux_inputs.extend(Word::words_as_elements(kernel.proc_hashes()));
+
+        let mut sink = FeltSink::default();
+        <MidenMultiAir as MultiAir<Felt, QuadFelt>>::observe(
+            &MidenMultiAir::new(),
+            &mut sink,
+            &air_inputs,
+            &aux_inputs,
+            &[10, 10, 10],
+        );
+
+        let mut expected: Vec<Felt> = claim.commitment().as_elements().to_vec();
+        expected.extend(deferred_root.as_elements());
+        assert_eq!(sink.observed, expected, "observe must emit [CLAIM_HASH | D]");
+    }
+
     #[test]
     #[should_panic(
         expected = "aux inputs shorter than the fixed program-hash + deferred-root prefix"

benches/blake3-bench/src/lib.rs

@@ -159,8 +159,13 @@ pub fn prove_and_verify_once(fixture: &Blake3Fixture) {
     let stack_inputs = fixture.stack_inputs;
     let trace_inputs = execute_trace_inputs(fixture);
     let (stack_outputs, proof) = prove_trace_outputs(trace_inputs);
+    let claim = miden_vm::ExecutionClaim::from_program_info(
+        fixture.program.to_info(),
+        stack_inputs,
+        stack_outputs,
+    );
     Verifier::new()
-        .verify(fixture.program.to_info(), stack_inputs, stack_outputs, proof)
+        .verify(proof, claim)
         .expect("failed to verify Blake3 benchmark proof");
 }