PVM MASM verifier

.github/workflows/test.yml

@@ -133,7 +133,7 @@ jobs:
         run: make check-constraints
 
   check-pvm-registry:
-    name: check PVM ACE registry constants
+    name: check PVM registry and MASM artifacts
     runs-on: warp-ubuntu-latest-x64-8x
     timeout-minutes: 15
     steps:
@@ -147,7 +147,7 @@ jobs:
           save-if: ${{ github.event_name == 'push' && github.ref == 'refs/heads/next' }}
       - name: Install rust
         run: rustup update --no-self-update
-      - name: Check PVM registry constants for drift (full 10! recompute)
+      - name: Check PVM registry and MASM artifacts for drift (full 10! recompute)
         run: make check-pvm-registry
 
   run-examples:

CHANGELOG.md

@@ -3,6 +3,8 @@
 
 #### Changes
 
+- [BREAKING] Added `miden::core::sys::pvm::verify_proof`, a MASM recursive verifier for the precompile VM, and generalized the shared MASM STARK verifier ([#3467](https://github.com/0xMiden/miden-vm/pull/3467)).
+- [BREAKING] `DeferredProof::Stark` now carries a `DeferredClaim` in place of the raw deferred root (`{ proof, claim }`); the wire encoding is unchanged, and `miden_precompiles_prover::verify_deferred` returns the claim ([#3467](https://github.com/0xMiden/miden-vm/pull/3467)).
 - [BREAKING] Factored recursive ACE circuits into per-order and shared sections, generalized the registry infrastructure to arbitrary AIR sets, and added the ten-AIR precompile VM registry. This changes the Miden VM and precompile VM ACE roots, relation digests, circuit shapes, and recursive-proof transcripts ([#3465](https://github.com/0xMiden/miden-vm/pull/3465)).
 - [BREAKING] Reduced the precompile STARK relation from 12 AIRs to 10 by merging the chunk/node/sponge and EC point/group stores ([#3464](https://github.com/0xMiden/miden-vm/pull/3464)).
 

Makefile

@@ -21,9 +21,9 @@ help:
 	@printf "  make test-core-lib               # Test core-lib crate\n"
 	@printf "  make test-verifier               # Test verifier crate\n"
 	@printf "  make check-constraints           # Check core-lib constraint artifacts\n"
-	@printf "  make check-pvm-registry          # Check PVM ACE registry constants\n"
+	@printf "  make check-pvm-registry          # Check PVM registry and MASM artifacts\n"
 	@printf "  make regenerate-constraints      # Regenerate core-lib constraint artifacts\n"
-	@printf "  make regenerate-pvm-registry     # Regenerate PVM ACE registry constants\n"
+	@printf "  make regenerate-pvm-registry     # Regenerate PVM registry and MASM artifacts\n"
 	@printf "\nExamples:\n"
 	@printf "  make test-air test=\"some_test\" # Test specific function\n"
 	@printf "  make test-fast                   # Fast tests (no proptests/CLI)\n"
@@ -293,11 +293,11 @@ regenerate-constraints: ## Regenerate the checked-in constraint artifacts (MASM
 	cargo run --package miden-core-lib --features constraints-tools --bin regenerate-evaluator -- --write
 
 .PHONY: regenerate-pvm-registry
-regenerate-pvm-registry: ## Regenerate the PVM ACE registry constants (~2 min; protocol break)
+regenerate-pvm-registry: ## Regenerate PVM registry and MASM artifacts (~2 min; protocol break)
 	cargo run --release --package miden-precompiles-prover --features registry-tools --bin pvm-registry-regen -- --write
 
 .PHONY: check-pvm-registry
-check-pvm-registry: ## Check the PVM ACE registry constants for drift (full recompute)
+check-pvm-registry: ## Check PVM registry and MASM artifacts for drift (full recompute)
 	cargo run --release --package miden-precompiles-prover --features registry-tools --bin pvm-registry-regen -- --check
 
 .PHONY: check-constraints

air/src/ace/recursive.rs

@@ -3,18 +3,35 @@ use alloc::vec::Vec;
 use miden_ace_codegen::{
     AceConfig, AceError, FactoredCircuitFactory, LayoutKind, ShuffleEncodeBuffer,
 };
-use miden_core::{Felt, Word, crypto::hash::Poseidon2};
+use miden_core::{Felt, Word, crypto::hash::Poseidon2, field::QuadFelt};
 use miden_crypto::merkle::MerklePath;
 
 use super::multi_air::build_factored_multi_air_ace_circuit;
-use crate::{MIDEN_AIR_COUNT, ProofOrder};
+use crate::{AIRS, MIDEN_AIR_COUNT, ProofOrder};
+
+/// Number of quotient chunks the recursive verifier and its ACE circuit consume.
+///
+/// This is the same symbolic derivation the lifted-STARK prover and verifier use. Keeping it
+/// executable matters even though the Miden relation currently derives eight chunks: the MASM
+/// quotient-recomposition inputs are functions of this value, not of the coincidentally equal
+/// blowup factor.
+fn recursive_verifier_num_quotient_chunks() -> usize {
+    let max_log_quotient_degree = AIRS
+        .iter()
+        .map(miden_crypto::stark::log_quotient_degree::<Felt, QuadFelt, _>)
+        .max()
+        .expect("the Miden AIR set is non-empty");
+    1usize << max_log_quotient_degree
+}
 
 /// ACE codegen settings used by the recursive verifier's MASM evaluator.
-const RECURSIVE_VERIFIER_ACE_CONFIG: AceConfig = AceConfig {
-    num_quotient_chunks: 8,
-    layout: LayoutKind::Masm,
-    num_airs: MIDEN_AIR_COUNT,
-};
+fn recursive_verifier_ace_config() -> AceConfig {
+    AceConfig {
+        num_quotient_chunks: recursive_verifier_num_quotient_chunks(),
+        layout: LayoutKind::Masm,
+        num_airs: MIDEN_AIR_COUNT,
+    }
+}
 
 /// Encoded recursive-verifier ACE circuit and the metadata consumed by MASM.
 ///
@@ -57,7 +74,7 @@ pub struct RecursiveAceCircuitFactory {
     /// The generic factory owns all order-invariant caching (post-constants sponge
     /// state, common-section digest) and the construction cross-checks; this type only
     /// maps [`ProofOrder`]s onto instance-index permutations.
-    inner: FactoredCircuitFactory<miden_core::field::QuadFelt>,
+    inner: FactoredCircuitFactory<QuadFelt>,
 }
 
 impl RecursiveAceCircuitFactory {
@@ -68,7 +85,7 @@ impl RecursiveAceCircuitFactory {
     /// encode-only shuffle bytes against the assembled stream, and the resumed prefix
     /// hash against hashing the full prefix.
     pub fn new() -> Result<Self, AceError> {
-        let factored = build_factored_multi_air_ace_circuit(RECURSIVE_VERIFIER_ACE_CONFIG)?;
+        let factored = build_factored_multi_air_ace_circuit(recursive_verifier_ace_config())?;
         let inner = FactoredCircuitFactory::new(factored.into_inner())?;
         Ok(Self { inner })
     }
@@ -78,6 +95,11 @@ impl RecursiveAceCircuitFactory {
         order.airs().iter().map(|air| air.instance_index()).collect()
     }
 
+    /// Quotient chunk count recorded in the factored circuit's actual READ layout.
+    pub fn num_quotient_chunks(&self) -> usize {
+        self.inner.factored().layout().counts.num_quotient_chunks
+    }
+
     /// Compute the registry leaf for one proof order without assembling its circuit.
     ///
     /// Encodes only the shuffle section into `buffer` and resumes the cached
@@ -192,7 +214,7 @@ pub fn recursive_registry_entry(order: &ProofOrder) -> Result<RecursiveRegistryE
 pub fn build_recursive_verifier_ace_circuit(
     order: &ProofOrder,
 ) -> Result<RecursiveAceCircuit, AceError> {
-    let factored = build_factored_multi_air_ace_circuit(RECURSIVE_VERIFIER_ACE_CONFIG)?;
+    let factored = build_factored_multi_air_ace_circuit(recursive_verifier_ace_config())?;
     let circuit = factored.circuit_for_order(order)?;
     let encoded = circuit.to_ace()?;
     let instructions = encoded.instructions();

air/src/config.rs

@@ -75,7 +75,7 @@ const QUERY_POW_BITS: usize = 17;
 /// 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`
+/// ~2.9508 bits per query. Must match the constant in `crates/lib/core/asm/stark/utils.masm`
 /// (enforced by cross-tests).
 pub const CONJECTURED_BITS_PER_QUERY_FP: u64 = 193_382;
 
@@ -87,7 +87,7 @@ pub const MAX_SECURITY_LEVEL: u32 = 128;
 /// 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)` —
+/// 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`.

benches/synthetic-bench/.gitignore

@@ -0,0 +1 @@
+/target/

benches/synthetic-bench/Cargo.toml

@@ -13,7 +13,7 @@ workspace = true
 
 [dependencies]
 miden-processor = { workspace = true, features = ["concurrent"] }
-miden-vm        = { path = "../../miden-vm", features = ["concurrent"] }
+miden-vm        = { path = "../../miden-vm", features = ["concurrent", "internal"] }
 serde           = { workspace = true, features = ["std"] }
 serde_json      = { workspace = true, features = ["std"] }
 thiserror       = { workspace = true, features = ["std"] }
@@ -23,6 +23,7 @@ codspeed-criterion-compat = { workspace = true }
 miden-assembly = { workspace = true, features = ["std"] }
 miden-core = { workspace = true, features = ["std"] }
 miden-core-lib = { workspace = true, features = ["std"] }
+miden-precompiles-prover = { workspace = true, features = ["concurrent"] }
 miden-prover = { workspace = true, features = ["concurrent"] }
 miden-verifier = { workspace = true, features = ["std"] }
 

benches/synthetic-bench/README.md

@@ -238,6 +238,51 @@ Env vars:
 The `prove` and `verify` axes use `HashFunction::Poseidon2` for STARK
 proof generation (see the `BENCH_HASH` constant in `benches/synthetic_bench.rs`).
 
+## Recursive-verification benchmarks
+
+The `recursive_verify` benchmark measures recursive verification of synthetic transaction proofs.
+First emit the `consume-single-p2id-note` transaction fixture:
+
+```sh
+SYNTH_SCENARIO="consume single P2ID note" \
+SYNTH_BENCH_AXES=exec \
+SYNTH_MASM_WRITE=1 \
+cargo bench -p miden-vm-synthetic-bench --bench synthetic_bench --profile optimized
+```
+
+Then pass the generated MASM program to the recursive benchmark. By default it measures two
+through eight MVM proofs:
+
+```sh
+RECURSION_BENCH_MASM="benches/synthetic-bench/target/synthetic_bench_bench-tx__consume-single-p2id-note.masm" \
+cargo bench -p miden-vm-synthetic-bench --bench recursive_verify --profile optimized
+```
+
+Set `RECURSION_BENCH_TX_PROOF_CACHE_DIR` to reuse the generated transaction proofs across runs.
+Relative cache paths are resolved from the workspace root.
+
+### PVM comparison
+
+The focused comparison places mixed cases containing one proof of the canonical
+100-Keccak/4-ECDSA deferred workload beside pure-MVM baselines:
+
+```sh
+RECURSION_BENCH_MASM="benches/synthetic-bench/target/synthetic_bench_bench-tx__consume-single-p2id-note.masm" \
+RECURSION_PVM_COMPARISON=1 \
+RECURSION_BENCH_TX_PROOF_CACHE_DIR="${PWD}/target/recursive-bench-cache/tx" \
+RECURSION_BENCH_PVM_PROOF_CACHE_DIR="${PWD}/target/recursive-bench-cache/pvm" \
+RECURSION_PROFILE_PROVE=1 \
+RECURSION_PROFILE_PROVE_REPEATS=10 \
+RECURSION_PROFILE_PROVE_WARMUPS=1 \
+cargo bench -p miden-vm-synthetic-bench --bench recursive_verify --profile optimized
+```
+
+The four cases are `4 MVM + 1 PVM`, `7 MVM`, `5 MVM + 1 PVM`, and `8 MVM`, in that order. Eight
+distinct proofs of the same synthetic transaction program and the single PVM proof are loaded or
+generated before any timed section. Set `RECURSION_PROFILE_ONLY=1` to print trace shapes without
+Criterion timing, or `RECURSION_PROFILE_PROVE=1` to record repeated outer-proof measurements. The
+profile mode rotates the starting case in each round to limit cache and thermal ordering bias.
+
 ## License
 
 This project is dual-licensed under the [MIT](http://opensource.org/licenses/MIT) and [Apache 2.0](https://opensource.org/license/apache-2-0) licenses.