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, and native verification takes `(proof, claim)` with `Verifier::verify_partial` returning the deferred obligation as a `#[must_use]` `Unsettled` token. The MASM entrypoint becomes `exec.vm::verify_vm_proof [claim_ptr] -> [D, num_queries, query_pow_bits, deep_pow_bits, folding_pow_bits]`: it verifies the caller-staged claim and returns the deferred root with the proof's transcript-bound security parameters. `miden_verifier::recursive` builds the advice ([#3422](https://github.com/0xMiden/miden-vm/pull/3422)).
 - [BREAKING] Normalized each AIR's committed LogUp sum by its trace length and changed the running-sum constraint to close cyclically, removing the requirement that lookup activity be absent from the last row ([#3412](https://github.com/0xMiden/miden-vm/pull/3412)).
 - Replaced panics in `OverflowTable::restore_context()`, `get_current_overflow_stack()`, and `get_current_overflow_stack_mut()` with proper `OperationError` returns ([#3370](https://github.com/0xMiden/miden-vm/pull/3370)).
 - `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)).

air/src/config.rs

@@ -63,8 +63,38 @@ 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`, with no margin: lowering this or the per-query
+/// rate drops the preset below 96 conjectured bits.
+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 {
@@ -184,16 +214,16 @@ pub fn ace_circuit_registry_tree() -> MerkleTree {
 /// Call on a challenger obtained from `config.challenger()` to complete the
 /// domain-separated transcript initialization. The config factories bind the
 /// caller-supplied relation digest into the prototype challenger; this function
-/// adds the remaining protocol parameters.
-pub fn observe_protocol_params(challenger: &mut impl CanObserve<Felt>) {
+/// adds the actual PCS parameters used by that config.
+pub fn observe_protocol_params(params: &PcsParams, challenger: &mut impl CanObserve<Felt>) {
     // Batch 1: PCS parameters, zero-padded to SPONGE_RATE.
-    challenger.observe(Felt::new_unchecked(NUM_QUERIES as u64));
-    challenger.observe(Felt::new_unchecked(QUERY_POW_BITS as u64));
-    challenger.observe(Felt::new_unchecked(DEEP_POW_BITS as u64));
-    challenger.observe(Felt::new_unchecked(FOLDING_POW_BITS as u64));
-    challenger.observe(Felt::new_unchecked(LOG_BLOWUP as u64));
-    challenger.observe(Felt::new_unchecked(LOG_FINAL_DEGREE as u64));
-    challenger.observe(Felt::new_unchecked(1_u64 << LOG_FOLDING_ARITY));
+    challenger.observe(Felt::new_unchecked(params.num_queries() as u64));
+    challenger.observe(Felt::new_unchecked(params.query_pow_bits() as u64));
+    challenger.observe(Felt::new_unchecked(params.deep_pow_bits() as u64));
+    challenger.observe(Felt::new_unchecked(params.folding_pow_bits() as u64));
+    challenger.observe(Felt::new_unchecked(params.log_blowup() as u64));
+    challenger.observe(Felt::new_unchecked(params.log_final_degree() as u64));
+    challenger.observe(Felt::new_unchecked(1_u64 << params.log_folding_arity()));
     challenger.observe(Felt::ZERO);
 }
 
@@ -358,14 +388,41 @@ mod tests {
     use alloc::vec::Vec;
 
     use miden_core::{Felt, Word, crypto::hash::Poseidon2};
-    use miden_crypto::merkle::MerkleTree;
+    use miden_crypto::{
+        merkle::MerkleTree,
+        stark::{challenger::CanObserve, pcs::PcsParams},
+    };
 
     use crate::{ProofOrder, ace};
 
     const PROTOCOL_ID: u64 = 1;
     const ACE_REGISTRY_PADDING_DOMAIN: u64 = 0xace;
     const REGEN_HINT: &str = "cargo run -p miden-core-lib --features constraints-tools --bin regenerate-constraints -- --write";
 
+    #[derive(Default)]
+    struct RecordingChallenger(Vec<Felt>);
+
+    impl CanObserve<Felt> for RecordingChallenger {
+        fn observe(&mut self, value: Felt) {
+            self.0.push(value);
+        }
+    }
+
+    /// Transcript domain separation must bind the parameters actually supplied to the config,
+    /// not the Miden VM's current compile-time defaults.
+    #[test]
+    fn protocol_observation_uses_the_supplied_pcs_params() {
+        let params = PcsParams::new(4, 3, 6, 5, 11, 19, 13).expect("valid distinct PCS params");
+        let mut challenger = RecordingChallenger::default();
+        super::observe_protocol_params(&params, &mut challenger);
+        assert_eq!(
+            challenger.0,
+            [19, 13, 11, 5, 4, 6, 8, 0].map(Felt::new_unchecked),
+            "the transcript must encode [queries, query PoW, DEEP PoW, folding PoW, blowup log, \
+             final-degree log, folding arity, padding]",
+        );
+    }
+
     fn padding_leaf(index: usize) -> Word {
         Poseidon2::hash_elements(&[
             Felt::new_unchecked(ACE_REGISTRY_PADDING_DOMAIN),
@@ -452,4 +509,120 @@ mod tests {
             "RELATION_DIGEST in config.rs is stale. Regenerate with: {REGEN_HINT}"
         );
     }
+
+    /// The deployed PCS preset attains exactly the conjectured target (96 bits) at its actual
+    /// query count and query-PoW constants. Unlike the reference-vector test below (which pins the
+    /// formula against hard-coded inputs), this pins the live `NUM_QUERIES` / `QUERY_POW_BITS`
+    /// preset, so a query-count or query-PoW downgrade is caught here rather than only indirectly.
+    #[test]
+    fn deployed_preset_attains_conjectured_target() {
+        assert_eq!(
+            super::conjectured_security_level(
+                super::NUM_QUERIES as u32,
+                super::QUERY_POW_BITS as u32
+            ),
+            96,
+            "deployed preset no longer attains 96 conjectured bits",
+        );
+    }
+
+    /// 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})"
+                );
+            }
+        }
+    }
 }