diff --git a/CHANGELOG.md b/CHANGELOG.md index f53bc9ee78..c00ea3796f 100644 --- a/CHANGELOG.md +++ b/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)). diff --git a/Cargo.lock b/Cargo.lock index 646c8a2c21..6fec14d69f 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -2658,9 +2658,7 @@ dependencies = [ "miden-verifier", "pretty_assertions", "proptest", - "serde-wincode", "test-case", - "thiserror", ] [[package]] @@ -2729,7 +2727,6 @@ dependencies = [ "miden-core", "miden-core-lib", "miden-mast-package", - "miden-precompiles", "miden-processor", "miden-prover", "miden-test-serde-macros", diff --git a/air/src/config.rs b/air/src/config.rs index 823ede68c5..682c1ab992 100644 --- a/air/src/config.rs +++ b/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` (, 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) { +/// adds the actual PCS parameters used by that config. +pub fn observe_protocol_params(params: &PcsParams, challenger: &mut impl CanObserve) { // 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,7 +388,10 @@ 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}; @@ -366,6 +399,30 @@ mod tests { 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); + + impl CanObserve 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(¶ms, &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})" + ); + } + } + } } diff --git a/air/src/lib.rs b/air/src/lib.rs index 9670783798..1700c7b402 100644 --- a/air/src/lib.rs +++ b/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}, @@ -877,18 +880,15 @@ impl> MultiAir 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>( &self, challenger: &mut C, @@ -905,19 +905,16 @@ impl> MultiAir 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); } } @@ -1024,8 +1021,9 @@ impl> MultiAir 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. @@ -1043,7 +1041,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 @@ -1213,6 +1215,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 = + 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() { @@ -1221,6 +1244,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, + } + impl CanObserve 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 = 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(); + >::observe( + &MidenMultiAir::new(), + &mut sink, + &air_inputs, + &aux_inputs, + &[10, 10, 10], + ); + + let mut expected: Vec = 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" diff --git a/benches/blake3-bench/src/lib.rs b/benches/blake3-bench/src/lib.rs index 50d0167afb..56919a90f2 100644 --- a/benches/blake3-bench/src/lib.rs +++ b/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"); } diff --git a/benches/synthetic-bench/benches/recursive_verify.rs b/benches/synthetic-bench/benches/recursive_verify.rs index fb72ea9b6b..0852efe549 100644 --- a/benches/synthetic-bench/benches/recursive_verify.rs +++ b/benches/synthetic-bench/benches/recursive_verify.rs @@ -2,7 +2,7 @@ //! //! This benchmark separates the transaction proof from the recursive verifier cost: //! transaction proofs are generated before timing, then the timed program verifies -//! the configured number of proofs via `exec.vm::verify_proof`. +//! the configured number of proofs via `exec.vm::verify_vm_proof`. //! //! For each requested proof count, the setup builds one recursive-verifier program and one advice //! provider. The program contains one verifier call per inner proof. The advice stack segments for @@ -44,8 +44,8 @@ use miden_assembly::Linkage; use miden_core::{ Felt, crypto::hash::Blake3_256, - deferred::TRUE_DIGEST, field::QuotientMap, + program::ExecutionClaim, serde::{Deserializable, Serializable}, utils::to_hex, }; @@ -55,7 +55,7 @@ use miden_processor::{ advice::{AdviceInputs, AdviceStack}, trace::TraceLenSummary, }; -use miden_prover::{PublicInputs, prove_sync}; +use miden_prover::prove_sync; use miden_utils_testing::recursive_verifier::generate_advice_inputs; use miden_vm::{ Assembler, ExecutionProof, HashFunction, Program, ProgramInfo, ProvingOptions, StackInputs, @@ -63,9 +63,7 @@ use miden_vm::{ }; const DEFAULT_PROOF_COUNTS: [usize; 7] = [2, 3, 4, 5, 6, 7, 8]; -const KERNEL_DIGEST_PTR: u64 = 0; -const STACK_IO_PTR: u64 = 4096; -const STACK_IO_VALUE_COUNT: u64 = 32; +const CLAIM_PTR: u64 = 4096; const TX_PROOF_CACHE_KEY_VERSION: &[u8] = b"miden-synthetic-recursive-tx-proof-cache-v1"; struct TxProofFixture { @@ -472,8 +470,6 @@ fn load_tx_fixtures(config: &BenchConfig, proof_count: usize) -> Vec Vec Vec String { let mut source = String::new(); - // `initial_stack[0]` must be on top when `verify_proof` starts. + // `initial_stack[0]` must be on top when `verify_vm_proof` starts. for value in initial_stack.iter().rev() { writeln!(source, "push.{value}").expect("write recursive verifier call source"); } writeln!( source, " - # Copy 4 * num_kernel_digests felts from advice into the kernel region. - dup.1 mul.4 push.{KERNEL_DIGEST_PTR} + # Copy the claim encoding P | K | I | O (40 felts) into the claim region; the kernel + # digest witness travels in the advice map. + push.40 push.{CLAIM_PTR} exec.copy_advice_to_mem - # Copy stack inputs and outputs into the stack i/o region. - push.{STACK_IO_VALUE_COUNT} push.{STACK_IO_PTR} - exec.copy_advice_to_mem - - exec.vm::verify_proof - " + exec.vm::verify_vm_proof + # => [D, num_queries, query_pow_bits, deep_pow_bits, folding_pow_bits] + dropw dropw + ", ) .expect("write recursive verifier call source"); source @@ -539,7 +534,8 @@ fn verify_proof_call_masm(initial_stack: &[u64]) -> String { /// Full MASM program used by the benchmark. /// -/// `verify_calls` is a sequence of `exec.vm::verify_proof` calls, one per inner proof. +/// `verify_calls` is a sequence of `exec.vm::verify_vm_proof` calls, one per inner +/// proof. fn recursive_verifier_program_masm(verify_calls: &str) -> String { format!( " @@ -597,19 +593,17 @@ fn dump_recursive_program_source(proof_count: usize, source: &str) { /// Build the advice provider consumed by one recursive verifier call. /// /// `generate_advice_inputs` parses the inner STARK proof and returns the exact advice stack, -/// Merkle store, and advice-map entries expected by `exec.vm::verify_proof`. +/// Merkle store, and advice-map entries expected by `exec.vm::verify_vm_proof`. /// The stack is ordered so its first element is the next value consumed by the VM. fn recursive_proof_advice(fixture: &TxProofFixture) -> RecursiveProofAdvice { - let pub_inputs = PublicInputs::new( + let claim = ExecutionClaim::from_program_info( fixture.program_info.clone(), fixture.stack_inputs, fixture.stack_outputs, - TRUE_DIGEST, ); - let verifier_inputs = generate_advice_inputs(fixture.proof.miden_proof().bytes(), pub_inputs) - .expect("recursive advice"); + let verifier_inputs = generate_advice_inputs(&fixture.proof, &claim).expect("recursive advice"); - let advice_stack = AdviceStack::try_from_values(verifier_inputs.advice_stack) + let advice_stack = AdviceStack::try_from_values(verifier_inputs.advice_stack()) .expect("recursive advice stack values must be canonical"); let advice_inputs = AdviceInputs::default() .with_advice_stack(advice_stack) diff --git a/benches/synthetic-bench/benches/synthetic_bench.rs b/benches/synthetic-bench/benches/synthetic_bench.rs index e008702648..06602c20d4 100644 --- a/benches/synthetic-bench/benches/synthetic_bench.rs +++ b/benches/synthetic-bench/benches/synthetic_bench.rs @@ -32,8 +32,8 @@ use miden_processor::{ DefaultHost, ExecutionOptions, FastProcessor, StackInputs, advice::AdviceInputs, }; use miden_vm::{ - Assembler, ExecutionProof, HashFunction, Program, ProgramInfo, ProvingOptions, StackOutputs, - Verifier, prove_sync, + Assembler, ExecutionClaim, ExecutionProof, HashFunction, Program, ProgramInfo, ProvingOptions, + StackOutputs, Verifier, prove_sync, }; use miden_vm_synthetic_bench::{ calibrator::{Calibration, calibrate, measure_program}, @@ -369,11 +369,12 @@ fn bench_one_scenario( b.iter_batched( || (program_info.clone(), StackInputs::default(), stack_outputs, proof.clone()), |(program_info, stack_inputs, stack_outputs, proof)| { - black_box( - Verifier::new() - .verify(program_info, stack_inputs, stack_outputs, proof) - .expect("verify"), + let claim = ExecutionClaim::from_program_info( + program_info, + stack_inputs, + stack_outputs, ); + black_box(Verifier::new().verify(proof, claim).expect("verify")); }, BatchSize::SmallInput, ); diff --git a/core/src/chiplets/hasher.rs b/core/src/chiplets/hasher.rs index 15bf5b4510..77b20e6dc3 100644 --- a/core/src/chiplets/hasher.rs +++ b/core/src/chiplets/hasher.rs @@ -60,6 +60,13 @@ pub fn hash_elements(elements: &[Felt]) -> Digest { Hasher::hash_elements(elements) } +/// Returns a hash of the provided list of field elements with the specified domain in the +/// second capacity element (the first carries the padding rule). +#[inline(always)] +pub fn hash_elements_in_domain(elements: &[Felt], domain: Felt) -> Digest { + Hasher::hash_elements_in_domain(elements, domain) +} + /// Applies a single Poseidon2 "step" to the provided state. /// /// The step number must be specified via `round` parameter, which must be between 0 and 30 diff --git a/core/src/program/claim.rs b/core/src/program/claim.rs new file mode 100644 index 0000000000..1aae385d76 --- /dev/null +++ b/core/src/program/claim.rs @@ -0,0 +1,256 @@ +//! The execution claim: the statement a Miden VM proof attests, and its canonical commitment. +//! +//! An execution claim binds four fields: the program digest `P`, the kernel commitment `K`, the +//! stack inputs `I`, and the stack outputs `O`. The deferred root `D` produced by execution is +//! *not* part of the claim: it is the obligation a verified claim hands back, bound separately +//! into the transcript seed. +//! +//! # Canonical encoding +//! +//! The claim encodes as exactly [`NUM_CLAIM_ELEMENTS`] = 40 field elements: +//! +//! ```text +//! offset 0..8 P ‖ K (program digest, kernel commitment) +//! offset 8..24 I StackInputs, 16 felts (canonical zero-padded, native order) +//! offset 24..40 O StackOutputs, 16 felts (canonical zero-padded, native order) +//! ``` +//! +//! The code context comes first so that callsites that pin `(P, K)` can resume the claim hash +//! from a precomputed sponge state; 40 elements is exactly five Poseidon2 rate blocks, so no +//! padding block is absorbed and both read points (the `(P, K)` prefix state and the claim +//! commitment) fall on permutation boundaries. +//! +//! # Claim commitment +//! +//! `CLAIM_HASH = Poseidon2::hash_elements_in_domain(P ‖ K ‖ I ‖ O, CLAIM_DOMAIN_TAG)`, i.e. the +//! domain tag rides in the second capacity element while the first carries the Sponge2 padding +//! rule of (here `40 % 8 = 0`). + +use super::{ + KernelDescriptor, ProgramInfo, StackInputs, StackOutputs, + domain::{EXECUTION_CLAIM_DOMAIN_ID, PROOF_REQUEST_DOMAIN_ID, domain_selector}, +}; +use crate::{Felt, Word, ZERO, chiplets::hasher}; + +// CONSTANTS +// ================================================================================================ + +/// Number of field elements in the canonical claim encoding: `P ‖ K ‖ I ‖ O`. +pub const NUM_CLAIM_ELEMENTS: usize = 40; + +/// Domain tag for the claim commitment: the registered selector +/// `(EXECUTION_CLAIM_DOMAIN_ID << 8) | 1` (see the [`domain`](super::domain) module). +pub const CLAIM_DOMAIN_TAG: Felt = domain_selector(EXECUTION_CLAIM_DOMAIN_ID, 1); + +/// Domain tag for the proof-request key: the registered selector +/// `(PROOF_REQUEST_DOMAIN_ID << 8) | 1` (see the [`domain`](super::domain) module). +pub const REQUEST_DOMAIN_TAG: Felt = domain_selector(PROOF_REQUEST_DOMAIN_ID, 1); + +// EXECUTION CLAIM +// ================================================================================================ + +/// The external statement a Miden VM proof attests: the program root and kernel identify the +/// executed code and its syscall authorization set; the stack inputs and outputs are the +/// execution's public I/O. +/// +/// Stack inputs and stack outputs are both stored top-of-stack first: the first value in each +/// slice is the top of the operand stack. The claim stores both in their canonical zero-padded +/// 16-element form. +/// +/// The deferred root is deliberately absent: verification returns it as an obligation. +#[derive(Debug, Clone, PartialEq, Eq)] +pub struct ExecutionClaim { + program_root: Word, + kernel: KernelDescriptor, + stack_inputs: StackInputs, + stack_outputs: StackOutputs, +} + +impl ExecutionClaim { + /// Creates a new execution claim from the program root, kernel, and stack I/O. + pub const fn new( + program_root: Word, + kernel: KernelDescriptor, + stack_inputs: StackInputs, + stack_outputs: StackOutputs, + ) -> Self { + Self { + program_root, + kernel, + stack_inputs, + stack_outputs, + } + } + + /// Creates a new execution claim from the program info and the stack I/O. + pub fn from_program_info( + program_info: ProgramInfo, + stack_inputs: StackInputs, + stack_outputs: StackOutputs, + ) -> Self { + let (program_root, kernel) = program_info.into_parts(); + Self::new(program_root, kernel, stack_inputs, stack_outputs) + } + + /// Returns the MAST root of the executed program. + pub const fn program_root(&self) -> Word { + self.program_root + } + + /// Returns the kernel descriptor of this claim. + pub const fn kernel(&self) -> &KernelDescriptor { + &self.kernel + } + + /// Returns the program info (program root + kernel) of this claim. + /// + /// This constructs a new [`ProgramInfo`], cloning the kernel descriptor. + pub fn to_program_info(&self) -> ProgramInfo { + ProgramInfo::new(self.program_root, self.kernel.clone()) + } + + /// Returns the stack inputs of this claim. + pub const fn stack_inputs(&self) -> &StackInputs { + &self.stack_inputs + } + + /// Returns the stack outputs of this claim. + pub const fn stack_outputs(&self) -> &StackOutputs { + &self.stack_outputs + } + + /// Splits this claim into its program root, kernel, and stack I/O. + pub fn into_parts(self) -> (Word, KernelDescriptor, StackInputs, StackOutputs) { + (self.program_root, self.kernel, self.stack_inputs, self.stack_outputs) + } + + /// Returns the canonical 40-element encoding `P ‖ K ‖ I ‖ O` of this claim. + pub fn to_elements(&self) -> [Felt; NUM_CLAIM_ELEMENTS] { + let mut elements = [ZERO; NUM_CLAIM_ELEMENTS]; + elements[0..4].copy_from_slice(self.program_root.as_elements()); + elements[4..8].copy_from_slice(self.kernel.commitment().as_elements()); + elements[8..24].copy_from_slice(&self.stack_inputs[..]); + elements[24..40].copy_from_slice(&self.stack_outputs[..]); + elements + } + + /// Returns the canonical commitment to this claim (`CLAIM_HASH`). + /// + /// This is the verifier-independent name of the claim: the value used to request proof + /// packages and to bind verified claims into a consumer's own statement. + pub fn commitment(&self) -> Word { + claim_commitment(&self.to_elements()) + } +} + +/// Returns the canonical claim commitment over an already-encoded claim. +/// +/// This is the single implementation of `CLAIM_HASH`; every native computation of the claim +/// commitment (including the transcript observation in `miden-air`) must go through it. +pub fn claim_commitment(elements: &[Felt; NUM_CLAIM_ELEMENTS]) -> Word { + hasher::hash_elements_in_domain(elements, CLAIM_DOMAIN_TAG) +} + +/// Returns the advice-map key addressing a proof package for `claim_commitment` under the +/// verifier identified by `verifier_root`. +/// +/// The key is `H_tag(claim_commitment ‖ verifier_root)` (one rate block, domain-separated). It +/// is a lookup address, not a trust anchor: the verifier re-checks the retrieved package against +/// the claim, so a wrong package fails verification. Both inputs are values the requester owns +/// (the verifier's MAST root; the claim commitment it computed or holds from its own inputs) — +/// neither is taken from advice. +pub fn request_key(verifier_root: Word, claim_commitment: Word) -> Word { + // Absorb claim_commitment first so the MASM mirror needs a single word-swap to place the + // rate; the order is otherwise arbitrary (a domain-separated hash of the two words). + let mut preimage = [ZERO; 2 * 4]; + preimage[0..4].copy_from_slice(claim_commitment.as_elements()); + preimage[4..8].copy_from_slice(verifier_root.as_elements()); + hasher::hash_elements_in_domain(&preimage, REQUEST_DOMAIN_TAG) +} + +// TESTS +// ================================================================================================ + +#[cfg(test)] +mod tests { + use super::{ + super::{KERNEL_DOMAIN_TAG, KernelDescriptor}, + *, + }; + + fn test_claim() -> ExecutionClaim { + 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(100)]).unwrap(); + let program_info = ProgramInfo::new(word(1), kernel); + let inputs = StackInputs::new(&[Felt::new_unchecked(5), Felt::new_unchecked(6)]).unwrap(); + let outputs = StackOutputs::new(&[Felt::new_unchecked(7)]).unwrap(); + ExecutionClaim::from_program_info(program_info, inputs, outputs) + } + + /// The commitment must bind every field and the I/O order, be domain-separated, and use + /// the registered selector. + #[test] + fn commitment_binds_fields_order_and_domain() { + let base = test_claim(); + let base_commitment = base.commitment(); + let base_elements = base.to_elements(); + + // mutate P + let mut mutated = base.clone(); + mutated.program_root = [Felt::new_unchecked(999), ZERO, ZERO, ZERO].into(); + assert_ne!(mutated.commitment(), base_commitment, "P not bound"); + + // mutate K (different kernel) + let mut mutated = base.clone(); + mutated.kernel = KernelDescriptor::from_hashes(vec![ + [Felt::new_unchecked(200), ZERO, ZERO, ZERO].into(), + ]) + .unwrap(); + assert_ne!(mutated.commitment(), base_commitment, "K not bound"); + + // mutate one element of I + let mut mutated = base.clone(); + mutated.stack_inputs = + StackInputs::new(&[Felt::new_unchecked(5), Felt::new_unchecked(60)]).unwrap(); + assert_ne!(mutated.commitment(), base_commitment, "I not bound"); + + // mutate one element of O + let mut mutated = base.clone(); + mutated.stack_outputs = StackOutputs::new(&[Felt::new_unchecked(70)]).unwrap(); + assert_ne!(mutated.commitment(), base_commitment, "O not bound"); + + // swap I and O (order binding): same multiset of felts, different positions + let mut mutated = base; + mutated.stack_inputs = StackInputs::new(&[Felt::new_unchecked(7)]).unwrap(); + mutated.stack_outputs = + StackOutputs::new(&[Felt::new_unchecked(5), Felt::new_unchecked(6)]).unwrap(); + assert_ne!(mutated.commitment(), base_commitment, "I/O order not bound"); + + // domain separation: differs from the untagged hash and from another registered tag + let elements = base_elements; + assert_ne!( + base_commitment, + hasher::hash_elements(&elements), + "claim commitment must differ from the untagged hash" + ); + assert_ne!( + base_commitment, + hasher::hash_elements_in_domain(&elements, KERNEL_DOMAIN_TAG), + "claim commitment must differ from a kernel-tagged hash of the same data" + ); + + // the tag is the registered selector + assert_eq!( + CLAIM_DOMAIN_TAG.as_canonical_u64(), + (u64::from(EXECUTION_CLAIM_DOMAIN_ID) << 8) | 1 + ); + } +} diff --git a/core/src/program/domain.rs b/core/src/program/domain.rs new file mode 100644 index 0000000000..dc9bf14706 --- /dev/null +++ b/core/src/program/domain.rs @@ -0,0 +1,85 @@ +//! Registered domain selectors for protocol-visible hash commitments. +//! +//! This module follows the Miden domain-separation RFC +//! (): consensus-critical domains use **registered +//! numeric identifiers** rather than hashed strings, packed as +//! +//! ```text +//! selector = (domain_id << 8) | version +//! ``` +//! +//! with `domain_id` a registered 24-bit integer (`>= 1`) and `version` an 8-bit per-domain +//! version (`>= 1`). The selector rides in the second capacity element of the Poseidon2 sponge +//! (`hash_elements_in_domain`); the first capacity element is hash-owned and carries the padding +//! rule, mirroring the RFC's frame/selector lane split. Unused parameter lanes are zero. +//! +//! # Provisional registry entries +//! +//! The RFC's draft registry allocates `0x010000..0x01ffff` to miden-vm, with concrete entries +//! delegated to this repository. These are the range's first entries, to be migrated into the +//! machine-readable registry when it lands: +//! +//! | domain_id | version | domain | +//! |------------|---------|-------------------------------------------| +//! | `0x010000` | 1 | kernel commitment ([`KERNEL_DOMAIN_TAG`](super::KERNEL_DOMAIN_TAG)) | +//! | `0x010001` | 1 | execution claim ([`CLAIM_DOMAIN_TAG`](super::CLAIM_DOMAIN_TAG)) | +//! | `0x010002` | 1 | proof request key ([`REQUEST_DOMAIN_TAG`](super::REQUEST_DOMAIN_TAG)) | +//! +//! Selectors share one capacity namespace with the `merge_in_domain` values used for MAST +//! control-block hashing. Those are opcode-sized (`< 256`) while every registered selector is +//! `>= 257` (`domain_id >= 1`), so those two ranges cannot collide. Distinctness among registered +//! selectors is the registry's responsibility: each `domain_id` is allocated once within its +//! maintainer's range, and the three defined here are pinned distinct by +//! `registry_entries_are_valid_and_distinct_selectors`. + +use crate::Felt; + +/// Registered domain id for the kernel commitment. +pub const KERNEL_COMMITMENT_DOMAIN_ID: u32 = 0x010000; + +/// Registered domain id for the execution-claim commitment. +pub const EXECUTION_CLAIM_DOMAIN_ID: u32 = 0x010001; + +/// Registered domain id for the proof-request key. +pub const PROOF_REQUEST_DOMAIN_ID: u32 = 0x010002; + +/// Packs a registered domain id and per-domain version into a domain selector. +/// +/// The result is a small integer (`domain_id << 8 | version`), used as the domain element of +/// `hash_elements_in_domain`. +pub const fn domain_selector(domain_id: u32, version: u8) -> Felt { + assert!( + domain_id >= 1 && domain_id < (1 << 24), + "domain_id must be a registered 24-bit id" + ); + assert!(version >= 1, "per-domain versions start at 1"); + Felt::new_unchecked(((domain_id as u64) << 8) | version as u64) +} + +#[cfg(test)] +mod tests { + use super::*; + + #[test] + fn registry_entries_are_valid_and_distinct_selectors() { + use crate::program::{CLAIM_DOMAIN_TAG, KERNEL_DOMAIN_TAG, REQUEST_DOMAIN_TAG}; + + let entries = [ + (KERNEL_COMMITMENT_DOMAIN_ID, KERNEL_DOMAIN_TAG), + (EXECUTION_CLAIM_DOMAIN_ID, CLAIM_DOMAIN_TAG), + (PROOF_REQUEST_DOMAIN_ID, REQUEST_DOMAIN_TAG), + ]; + for (i, (id, tag)) in entries.iter().enumerate() { + assert!(*id >= 1 && *id < (1 << 24), "domain id out of the registered range"); + assert_eq!( + tag.as_canonical_u64(), + (u64::from(*id) << 8) | 1, + "tag is not the packed selector" + ); + for (other_id, other_tag) in entries.iter().skip(i + 1) { + assert_ne!(id, other_id, "registered domain ids must be unique"); + assert_ne!(tag, other_tag, "registered tags must be unique"); + } + } + } +} diff --git a/core/src/program/kernel.rs b/core/src/program/kernel.rs index 405be6205d..38e2b15bf5 100644 --- a/core/src/program/kernel.rs +++ b/core/src/program/kernel.rs @@ -9,6 +9,14 @@ use crate::{ serde::{ByteReader, ByteWriter, Deserializable, DeserializationError, Serializable}, }; +// CONSTANTS +// ================================================================================================ + +/// Domain tag for the kernel commitment: the registered selector +/// `(KERNEL_COMMITMENT_DOMAIN_ID << 8) | 1` (see the [`domain`](super::domain) module). +pub const KERNEL_DOMAIN_TAG: crate::Felt = + super::domain::domain_selector(super::domain::KERNEL_COMMITMENT_DOMAIN_ID, 1); + // KERNEL // ================================================================================================ @@ -93,13 +101,18 @@ impl KernelDescriptor { &self.0 } - /// Returns the canonical commitment to this kernel: `hash_elements` over the flattened - /// procedure digests. + /// Returns the canonical commitment to this kernel: the domain-tagged sequential hash of the + /// flattened procedure digests, `hash_elements_in_domain(flatten(procs), KERNEL_DOMAIN_TAG)`. /// - /// This matches the kernel commitment computed by the protocol and is the fixed-size - /// identifier observed by the recursive verifier in place of the raw digest list. + /// This is the fixed-size identifier observed by the recursive verifier in place of the raw + /// digest list. The encoding is normative: + /// - element order is this descriptor's canonical procedure order (fixed at construction); + /// - length binding comes from the Sponge2 padding rule (: + /// the first capacity element carries `len % rate` and inputs are zero-padded to a rate + /// multiple), so digest lists of different lengths cannot collide; + /// - the empty kernel hashes to the rule's canonical empty-input value. pub fn commitment(&self) -> Word { - hasher::hash_elements(Word::words_as_elements(&self.0)) + hasher::hash_elements_in_domain(Word::words_as_elements(&self.0), KERNEL_DOMAIN_TAG) } } @@ -154,10 +167,14 @@ mod tests { #[test] fn empty_kernel_commitment_matches_hash_of_no_elements() { - // The empty kernel is the common case; its commitment must equal the canonical hash of - // zero elements, which the recursive verifier mirrors via `hash_elements(ptr, 0)`. + // The empty kernel's commitment must equal the canonical domain-tagged hash of zero + // elements, which the recursive verifier mirrors via + // `hash_elements_in_domain(ptr, 0, KERNEL_DOMAIN_TAG)`. let empty = KernelDescriptor::default(); - assert_eq!(empty.commitment(), crate::chiplets::hasher::hash_elements(&[])); + assert_eq!( + empty.commitment(), + crate::chiplets::hasher::hash_elements_in_domain(&[], super::KERNEL_DOMAIN_TAG) + ); } #[test] diff --git a/core/src/program/mod.rs b/core/src/program/mod.rs index fa9d14ca84..b43fbb8925 100644 --- a/core/src/program/mod.rs +++ b/core/src/program/mod.rs @@ -12,8 +12,16 @@ use crate::{ utils::ToElements, }; +mod claim; +pub use claim::{ + CLAIM_DOMAIN_TAG, ExecutionClaim, NUM_CLAIM_ELEMENTS, REQUEST_DOMAIN_TAG, claim_commitment, + request_key, +}; + +pub mod domain; + mod kernel; -pub use kernel::{KernelDescriptor, KernelError}; +pub use kernel::{KERNEL_DOMAIN_TAG, KernelDescriptor, KernelError}; mod stack; pub use stack::{InputError, MIN_STACK_DEPTH, OutputError, StackInputs, StackOutputs}; @@ -249,6 +257,11 @@ impl ProgramInfo { pub fn kernel_commitment(&self) -> Word { self.kernel.commitment() } + + /// Splits this program info into its program hash and kernel descriptor. + pub fn into_parts(self) -> (Word, KernelDescriptor) { + (self.program_hash, self.kernel) + } } impl From for ProgramInfo { diff --git a/core/src/proof.rs b/core/src/proof.rs index d69256a48a..401fe8a85d 100644 --- a/core/src/proof.rs +++ b/core/src/proof.rs @@ -185,11 +185,12 @@ impl ExecutionProof { /// Returns conjectured security level of this proof in bits. /// - /// Currently returns a hardcoded 96 bits. Once the security estimator is implemented - /// in Plonky3, this should calculate the actual conjectured security level based on: - /// - Proof parameters (FRI folding factor, number of queries, etc.) - /// - Hash function collision resistance - /// - Field size and extension degree + /// TODO: this is a placeholder returning a hardcoded 96 (honest only for the current + /// parameter preset). The conjectured estimator now exists as + /// `miden_air::config::conjectured_security_level`, but this method cannot call it — + /// `miden-air` depends on `miden-core`, not the reverse. The intended fix is to stop having + /// the proof self-report a security level and instead grade it in the verifier (which does + /// depend on `miden-air`). pub fn security_level(&self) -> u32 { 96 } diff --git a/crates/lib/core/asm/crypto/hashes/poseidon2.masm b/crates/lib/core/asm/crypto/hashes/poseidon2.masm index 69a313ec56..6afb0208f2 100644 --- a/crates/lib/core/asm/crypto/hashes/poseidon2.masm +++ b/crates/lib/core/asm/crypto/hashes/poseidon2.masm @@ -449,6 +449,62 @@ pub proc hash_elements # => [HASH] end +#! Computes the domain-tagged hash of Felt values starting at the specified memory address. +#! +#! Mirrors `Poseidon2::hash_elements_in_domain` on the Rust side: the first capacity element +#! carries the padding rule (`num_elements % 8`), the second carries the domain tag, and the +#! input is zero-padded to a rate multiple. +#! +#! Inputs: [ptr, num_elements, domain] +#! Outputs: [HASH] +#! +#! Where: +#! - ptr is the memory address of the first element to be hashed; must be word-aligned. +#! - num_elements is the number of elements to be hashed. +#! - domain is the domain-separation tag placed in the second capacity element. +pub proc hash_elements_in_domain + # => [ptr, num_elements, domain] + swap u32divmod.8 swap + # => [num_elements/8, num_elements%8, ptr, domain] + + # end address for the double-word absorption loop + mul.8 dup.2 add movup.2 + # => [ptr, end_pairs_addr, num_elements%8, domain] + + # capacity word = [num_elements%8, domain, 0, 0] + push.0.0 movup.5 dup.5 + # => [num_elements%8, domain, 0, 0, ptr, end_pairs_addr, num_elements%8] + + padw padw + # => [R0, R1, C, ptr, end_pairs_addr, num_elements%8] + + # Empty input with a nonzero domain absorbs a ONE padding marker into the first rate slot + # before permuting, mirroring the native rule (without it, the empty hash would collide with + # the hash of eight zeros under the same domain). Empty means ptr == end_pairs_addr and + # num_elements%8 == 0. + dup.14 eq.0 + # => [rem_is_zero, R0, R1, C, ptr, end_pairs_addr, num_elements%8] + dup.13 dup.15 eq + # => [ptr_eq_end, rem_is_zero, R0, R1, C, ptr, end_pairs_addr, num_elements%8] + and + # => [input_is_empty, R0, R1, C, ptr, end_pairs_addr, num_elements%8] + dup.10 eq.0 not and + # => [empty_and_domain_nonzero, R0, R1, C, ptr, end_pairs_addr, num_elements%8] + if.true + # set rate[0] = 1, apply one permutation, and squeeze + drop push.1 + # => [R0 = (1, 0, 0, 0), R1, C, ptr, end_pairs_addr, num_elements%8] + hperm + # => [R0', R1', C', ptr, end_pairs_addr, num_elements%8] + exec.squeeze_digest + swapw drop drop drop movdn.4 + # => [HASH] + else + exec.hash_elements_with_state + # => [HASH] + end +end + #! Computes hash of Felt values starting at the specified memory address. #! #! Notice that this procedure essentially pads the elements to be hashed to the next multiple of 8 diff --git a/crates/lib/core/asm/stark/constants.masm b/crates/lib/core/asm/stark/constants.masm index 5d08fae73f..3bdf730046 100644 --- a/crates/lib/core/asm/stark/constants.masm +++ b/crates/lib/core/asm/stark/constants.masm @@ -95,22 +95,22 @@ const OOD_FIXED_TERM_HORNER_EVALS_PTR = 3223322664 ### Address storing trace domain generator const TRACE_DOMAIN_GENERATOR_PTR = 3223322669 -### Address storing a pointer to the reduced-inputs block -### [kernel_H | program_digest | deferred_root | zero_pad] (16 felts). The block lives at the -### fixed standalone address REDUCED_INPUTS_PTR; this cell holds that pointer for the readers. -const REDUCED_INPUTS_ADDRESS_PTR = 3223322670 +### Pointer to the boundary data at BOUNDARY_INPUTS_PTR. +const BOUNDARY_INPUTS_ADDRESS_PTR = 3223322670 ### Address storing a pointer to the public inputs const PUBLIC_INPUTS_ADDRESS_PTR = 3223322671 -### Caller-supplied base address of the kernel-procedure digests (N word-aligned digests). Persisted -### by `verify_proof` from its operand so the step-II boundary fold can re-read the same region the -### kernel commitment hashes. +### Base address of the kernel-procedure digests (N word-aligned digests): the verifier-owned +### witness region (`KERNEL_WITNESS_PTR`) that `verify_vm_proof` fetches into from the advice map. +### Persisted by `stage_boundary_inputs` from its operand so the step-II boundary fold can re-read +### the same region the kernel commitment hashes. const KERNEL_DIGESTS_ADDRESS_PTR = 3223322706 -### Caller-supplied base address of the fixed-length public inputs (stack i/o, 32 base felts). -### Persisted by `verify_proof` from its operand so `load_public_inputs` can EF-expand them. -const STACK_IO_ADDRESS_PTR = 3223322707 +### Caller-supplied base address of the claim region (40 base felts: P | K | I | O). +### Persisted by `stage_boundary_inputs`; `load_public_inputs` EF-expands the I/O section (+8) +### and `claim_commitment` commits the whole region. +const CLAIM_ADDRESS_PTR = 3223322707 ### Scratch word used by the FRI verifier to persist loop state between queries. ### Stores [query_ptr, layer_ptr, rem_ptr, g]. @@ -139,7 +139,7 @@ const BUS_GAMMA_PTR = 3223322700 const C_TOTAL_PTR = 3223322704 ### Address of the cell holding the number of kernel-procedure digests `N`, persisted by -### `verify_proof` for the outer-LogUp boundary fold computed in step II. +### `verify_vm_proof` for the outer-LogUp boundary fold computed in step II. const NUM_KERNEL_DIGESTS_PTR = 3223322712 ### Address of the composition challenges [alpha0, alpha1, beta0, beta1]. @@ -182,11 +182,15 @@ const ORDER_TAG_PTR = 3223322764 const RELATION_DIGEST_PTR = 3223322768 const ACE_REGISTRY_ROOT_PTR = 3223322772 -### Fixed standalone reduced-inputs block (16 felts): -### [kernel_H (4) | program_digest (4) | deferred_root (4) | zero_pad (4)]. The verifier writes -### it and absorbs it into Fiat-Shamir; the ACE circuit never reads it, so it lives in the fixed -### verifier region rather than the OOD-derived ACE READ region. -const REDUCED_INPUTS_PTR = 3223322836 +### Boundary data: [kernel_H | program_digest | deferred_root | reserved]. +### Each entry is one word; the trailing word is unused. +const BOUNDARY_INPUTS_PTR = 3223322836 + +### Kernel digest witness region (up to 255 digests = 1020 felts, bounded by +### KernelDescriptor::MAX_NUM_PROCEDURES). `verify_vm_proof` fetches the digest +### list from the advice map under the claim's K, stages it here, and asserts it hashes to K; +### the step-II boundary fold reads it via KERNEL_DIGESTS_ADDRESS_PTR. +const KERNEL_WITNESS_PTR = 3223322852 ## ACE related ## Starts at address 3225419776 = 2**31 + 2**30 + 2**22 and the memory region grows backward @@ -211,16 +215,12 @@ const REDUCED_INPUTS_PTR = 3223322836 ## [ constants ] ACE_CIRCUIT_STREAM_PTR ## ... EVAL section follows ... ## -## The reduced-inputs block (kernel_H | program_digest | deferred_root | zero pad) is NOT part -## of the ACE READ section: the circuit references only the stack-i/o public values. It lives at -## the fixed standalone `REDUCED_INPUTS_PTR` above, staged by `verify_proof` and absorbed into -## Fiat-Shamir; it is not carved out of this region. +## Boundary data is stored separately at `BOUNDARY_INPUTS_PTR`. ACE reads stack inputs and outputs +## from `pi_ptr`; it does not read the boundary data. `CLAIM_HASH` binds kernel_H and program_digest; +## deferred_root is absorbed separately into Fiat-Shamir. ## -## After `verify_proof` returns, the 16 felts at `REDUCED_INPUTS_PTR` together with the FLPI -## window at `pi_ptr` (read base felts at `pi_ptr + 2*i`) constitute the verified public-input -## commitment the caller can bind against. The FLPI pointer is dynamic (stored at -## PUBLIC_INPUTS_ADDRESS_PTR); the reduced-inputs pointer cell (REDUCED_INPUTS_ADDRESS_PTR) holds -## the fixed `REDUCED_INPUTS_PTR`. All other pointers are fixed constants. +## `PUBLIC_INPUTS_ADDRESS_PTR` stores `pi_ptr`; read stack values at `pi_ptr + 2*i`. +## `BOUNDARY_INPUTS_ADDRESS_PTR` stores the fixed `BOUNDARY_INPUTS_PTR`. ### We use 2 extension field elements for a total of 4 base field elements. const AUX_RAND_ELEM_PTR = 3225419776 @@ -255,7 +255,7 @@ const AUXILIARY_ACE_INPUTS_PTR = 3225420336 # AUX_BUS_BOUNDARY_PTR + 8 const ACE_CIRCUIT_STREAM_PTR = 3225420376 # AUXILIARY_ACE_INPUTS_PTR + 40 ### Address at the start of the evaluation-gates portion of the arithmetic circuit (EVAL section). -const ACE_CIRCUIT_PTR = 3225420972 # ACE_CIRCUIT_STREAM_PTR + num_const_felts (596 for multi-AIR) +const ACE_CIRCUIT_PTR = 3225420960 # ACE_CIRCUIT_STREAM_PTR + num_const_felts (584 for multi-AIR) ## FRI ## @@ -352,6 +352,11 @@ pub proc get_fri_fold_arity push.FRI_FOLD_ARITY end +#! Returns the first verifier-owned memory address. +pub proc verifier_memory_start + push.LDE_DOMAIN_INFO_PTR +end + #! Store details about the LDE domain. #! #! The info stored is `[lde_size, log(lde_size), lde_g, 0]`. @@ -530,8 +535,8 @@ pub proc get_trace_domain_generator push.TRACE_DOMAIN_GENERATOR_PTR mem_load end -pub proc reduced_inputs_address_ptr - push.REDUCED_INPUTS_ADDRESS_PTR +pub proc boundary_inputs_address_ptr + push.BOUNDARY_INPUTS_ADDRESS_PTR end pub proc public_inputs_address_ptr @@ -610,16 +615,20 @@ pub proc c_total_ptr push.C_TOTAL_PTR end -pub proc reduced_inputs_ptr - push.REDUCED_INPUTS_PTR +pub proc boundary_inputs_ptr + push.BOUNDARY_INPUTS_PTR end pub proc kernel_digests_address_ptr push.KERNEL_DIGESTS_ADDRESS_PTR end -pub proc stack_io_address_ptr - push.STACK_IO_ADDRESS_PTR +pub proc kernel_witness_ptr + push.KERNEL_WITNESS_PTR +end + +pub proc claim_address_ptr + push.CLAIM_ADDRESS_PTR end pub proc fri_verify_state_ptr diff --git a/crates/lib/core/asm/stark/random_coin.masm b/crates/lib/core/asm/stark/random_coin.masm index 0bb2af445d..dd484ce2c1 100644 --- a/crates/lib/core/asm/stark/random_coin.masm +++ b/crates/lib/core/asm/stark/random_coin.masm @@ -829,8 +829,13 @@ pub proc generate_list_indices exec.constants::get_lde_domain_depth #=> [depth, query_ptr, num_queries, ...] - # Pre-compute mask = 2^depth - 1. - dup pow2 u32assert u32overflowing_sub.1 assertz + # mask = 2^depth - 1. Depth is at most 32; use the u32 all-ones mask at that boundary. + dup eq.32 + if.true + push.0xffffffff + else + dup pow2 u32assert u32overflowing_sub.1 assertz + end #=> [mask, depth, query_ptr, num_queries, ...] # Rearrange to loop layout: [query_ptr, num_queries, mask, depth, ...] diff --git a/crates/lib/core/asm/sys/vm/claim.masm b/crates/lib/core/asm/sys/vm/claim.masm new file mode 100644 index 0000000000..f7241e3453 --- /dev/null +++ b/crates/lib/core/asm/sys/vm/claim.masm @@ -0,0 +1,105 @@ +use miden::core::crypto::hashes::poseidon2 + +# EXECUTION CLAIM +# ================================================================================================= +# +# The execution claim is the statement a Miden VM proof attests, encoded as a canonical 40-felt +# memory region: +# +# claim_ptr + 0 P program_digest (1 word) +# claim_ptr + 4 K kernel_commitment (1 word) +# claim_ptr + 8 I stack_inputs (16 felts, canonical zero-padded) +# claim_ptr + 24 O stack_outputs (16 felts, canonical zero-padded) +# +# The deferred root D is not part of the claim: it is the obligation a verified claim hands back. +# +# The claim commitment is the domain-tagged sequential hash of the region. 40 felts is exactly +# five rate blocks, so no padding block is absorbed and the (P, K) prefix state after block 1 is +# resumable by callsites that pin those fields. Mirrors +# miden_core::program::ExecutionClaim::commitment (enforced by cross-tests). + +# Domain tag for the claim commitment: the registered selector +# (EXECUTION_CLAIM_DOMAIN_ID << 8) | version = (0x010001 << 8) | 1, per the Miden +# domain-separation RFC (https://github.com/0xMiden/crypto/pull/1026). +# Must match miden_core::program::CLAIM_DOMAIN_TAG (enforced by cross-tests). +const CLAIM_DOMAIN_TAG = 0x01000101 + +# Domain tag for the kernel commitment: the registered selector +# (KERNEL_COMMITMENT_DOMAIN_ID << 8) | version = (0x010000 << 8) | 1, per the Miden +# domain-separation RFC (https://github.com/0xMiden/crypto/pull/1026). +# Must match miden_core::program::KERNEL_DOMAIN_TAG (enforced by cross-tests). +const KERNEL_DOMAIN_TAG = 0x01000001 + +# Number of field elements in the canonical claim encoding. +const NUM_CLAIM_ELEMENTS = 40 + +#! Computes the canonical claim commitment (CLAIM_HASH) over a claim region. +#! +#! The region must hold the fully populated 40-felt claim encoding P ‖ K ‖ I ‖ O. The commitment +#! names the claim: it forms proof-request keys and binds verified claims into a consumer's own +#! statement. The procedure verifies nothing. +#! +#! Inputs: [claim_ptr, ...] +#! Outputs: [CLAIM_HASH, ...] +#! +#! Where: +#! - claim_ptr is the word-aligned address of the claim region. +#! - CLAIM_HASH is the domain-tagged Poseidon2 hash of the 40-element encoding. +pub proc claim_commitment + push.CLAIM_DOMAIN_TAG push.NUM_CLAIM_ELEMENTS movup.2 + # => [claim_ptr, NUM_CLAIM_ELEMENTS, CLAIM_DOMAIN_TAG, ...] + exec.poseidon2::hash_elements_in_domain + # => [CLAIM_HASH, ...] +end + +#! Computes the canonical kernel commitment over a raw kernel-procedure digest list. +#! +#! Mirrors miden_core::program::KernelDescriptor::commitment: the domain-tagged sequential hash +#! of the flattened digests, length-bound by the sponge's padding rule, in the descriptor's +#! canonical order. +#! +#! Inputs: [kernel_ptr, num_kernel_digests, ...] +#! Outputs: [K, ...] +#! +#! Where: +#! - kernel_ptr is the word-aligned address of the digest list. +#! - num_kernel_digests is the number of digests (words) in the list. +#! - K is the kernel commitment. +pub proc kernel_commitment + swap mul.4 swap + # => [kernel_ptr, num_elements, ...] + push.KERNEL_DOMAIN_TAG movdn.2 + # => [kernel_ptr, num_elements, KERNEL_DOMAIN_TAG, ...] + exec.poseidon2::hash_elements_in_domain + # => [K, ...] +end + +# Domain tag for the proof-request key: the registered selector +# (PROOF_REQUEST_DOMAIN_ID << 8) | version = (0x010002 << 8) | 1, per the Miden +# domain-separation RFC (https://github.com/0xMiden/crypto/pull/1026). +# Must match miden_core::program::REQUEST_DOMAIN_TAG (enforced by cross-tests). +const REQUEST_DOMAIN_TAG = 0x01000201 + +#! Computes the advice-map key addressing a proof package for a claim under a verifier. +#! +#! The key is the domain-tagged hash of `claim_commitment ‖ verifier_root` (exactly one rate +#! block, so a single permutation with no memory). It is a lookup address, not a trust anchor: +#! the verifier re-checks the retrieved package, so a wrong package fails verification. Both +#! inputs are program-owned (the verifier's MAST root via `procref`; the claim commitment via +#! `claim_commitment` or the program's own inputs) — neither comes from advice. Mirrors +#! miden_core::program::request_key. +#! +#! Inputs: [VERIFIER_ROOT, CLAIM_COMMITMENT, ...] +#! Outputs: [REQUEST_KEY, ...] +pub proc request_key + # Capacity word [0, REQUEST_DOMAIN_TAG, 0, 0]: first element 8 % 8 = 0, domain in the + # second. Pushed on top, then swapped to the capacity position (state word 2) so the two + # input words become the rate; absorbing claim ‖ verifier keeps this to a single swap. + push.0.0.REQUEST_DOMAIN_TAG.0 + # => [CAP, VERIFIER_ROOT, CLAIM_COMMITMENT, ...] + swapw.2 + # => [CLAIM_COMMITMENT, VERIFIER_ROOT, CAP, ...] = [R0, R1, C]; rate = claim ‖ verifier + hperm + exec.poseidon2::squeeze_digest + # => [REQUEST_KEY, ...] +end diff --git a/crates/lib/core/asm/sys/vm/mod.masm b/crates/lib/core/asm/sys/vm/mod.masm index be0fb96084..a2d4eb9539 100644 --- a/crates/lib/core/asm/sys/vm/mod.masm +++ b/crates/lib/core/asm/sys/vm/mod.masm @@ -1,20 +1,23 @@ pub mod aux_trace +pub mod claim pub mod constraints_eval pub mod constraints_eval_inputs pub mod deep_queries pub mod ood_frames pub mod public_inputs +use miden::core::mem use miden::core::stark::verifier use miden::core::stark::constants -# Acceptable security parameters for Miden VM proof verification. -# These define the security policy enforced by `assert_acceptable_options`. -# If the protocol security level changes, update these constants accordingly. -const ACCEPTABLE_NUM_QUERIES = 27 -const ACCEPTABLE_QUERY_POW_BITS = 16 -const ACCEPTABLE_DEEP_POW_BITS = 12 -const ACCEPTABLE_FOLDING_POW_BITS = 4 +# Fixed-point (16 fractional bits) conjectured security bits per FRI query for this +# configuration's blowup (8) and ~128-bit challenge field, per the random-words formula +# (https://eprint.iacr.org/2025/2010, section 1.5). Must match +# miden_air::config::CONJECTURED_BITS_PER_QUERY_FP (enforced by cross-tests). +const CONJECTURED_BITS_PER_QUERY_FP = 193382 + +# Cap on any reported security level: min(challenge-field bits, hash collision resistance). +const MAX_SECURITY_LEVEL = 128 # RELATION_DIGEST = hash(PROTOCOL_ID, ACE_REGISTRY_ROOT). const RELATION_DIGEST_0 = 6228634522968454696 @@ -45,22 +48,38 @@ proc load_security_params adv_push exec.constants::set_folding_pow_bits end -#! Asserts that the security parameters in memory meet the Miden VM security policy. +#! Checks that the 40-felt claim region is word-aligned and below verifier-owned memory. +#! Must run before the verifier writes to memory. #! -#! Input: [...] -#! Output: [...] -proc assert_acceptable_options - exec.constants::get_number_queries - push.ACCEPTABLE_NUM_QUERIES assert_eq.err="num_queries does not match acceptable security policy" +#! Input: [claim_ptr, ...] +#! Output: [claim_ptr, ...] +proc assert_valid_claim_region + # u32mod also validates that claim_ptr is a u32. + dup u32mod.4 assertz.err="claim_ptr must be word-aligned" - exec.constants::get_query_pow_bits - push.ACCEPTABLE_QUERY_POW_BITS assert_eq.err="query_pow_bits does not match acceptable security policy" - - exec.constants::get_deep_pow_bits - push.ACCEPTABLE_DEEP_POW_BITS assert_eq.err="deep_pow_bits does not match acceptable security policy" + # Require [claim_ptr, claim_ptr + 40) to end before verifier memory. + dup add.40 exec.constants::verifier_memory_start + u32lte assert.err="claim memory region overlaps verifier-owned memory" +end - exec.constants::get_folding_pow_bits - push.ACCEPTABLE_FOLDING_POW_BITS assert_eq.err="folding_pow_bits does not match acceptable security policy" +#! Computes the conjectured security level (in bits) attained by the given proof parameters. +#! +#! Evaluates the integer fixed-point formula `min((num_queries * C) >> 16 + query_pow_bits, 128)`. +#! Must match miden_air::config::conjectured_security_level bit-for-bit (enforced by +#! cross-tests). Holds no policy: the caller applies its own acceptance threshold to the result. +#! +#! PRECONDITION: `num_queries <= 150`, so `num_queries * C` fits in a u32 (the `u32shr` below +#! requires that). Parameters returned by `verify_vm_proof` satisfy this bound: the generic +#! verifier enforces it. +#! +#! Inputs: [num_queries, query_pow_bits, ...] +#! Outputs: [level, ...] +pub proc conjectured_security_level + push.CONJECTURED_BITS_PER_QUERY_FP mul + u32shr.16 + add + push.MAX_SECURITY_LEVEL u32min + # => [level, ...] end #! Loads the VM-specific AIR context used by the generic STARK verifier. @@ -172,34 +191,88 @@ proc store_ace_registry_root dropw dropw end -#! Verifies a STARK proof attesting to the correct execution of a program in the Miden VM. +#! Verifies a STARK proof of the caller-staged execution claim and returns the deferred +#! obligation the proof binds and the proof's transcript-bound security parameters. +#! +#! The proof is consumed from the advice stack; request keys name this procedure's MAST root +#! (`CoreLibrary::recursive_verifier_root` on the operator side). A consumer that fetches the +#! proof by content derives the identical root in-VM via `procref` of this procedure, computes +#! `request_key(verifier_root, claim_commitment)` with `claim::request_key`, and moves the +#! registered proof package onto the advice stack before calling it. +#! +#! Security parameters (num_queries, query_pow_bits, deep_pow_bits, folding_pow_bits) are loaded +#! from the advice stack and stored in memory for the generic verifier, which enforces their +#! structural bounds and binds them into the Fiat-Shamir transcript - so a proof cannot claim +#! parameters it was not produced with. This procedure holds no security-estimate formula and +#! no acceptance policy: it returns the transcript-bound parameters for the caller to grade +#! (e.g. with `conjectured_security_level`) under its own policy. An estimate or policy change +#! therefore never moves this procedure's root - request keys and registered proof packages +#! stay valid across such changes. #! -#! Security parameters (num_queries, query_pow_bits, deep_pow_bits, folding_pow_bits) are -#! loaded from the advice stack, validated against the acceptable security policy, and -#! stored in memory for use by the generic verifier. +#! The caller stores the claim as `P (+0) | K (+4) | I (+8) | O (+24)`. The complete 40-felt +#! region must be below `constants::verifier_memory_start`. #! -#! - Public inputs contain fixed-size input/output stacks, the program digest, and kernel procedure -#! digests. -#! - The wrapper records the AIR context before calling the generic STARK verifier. -#! - The constraints evaluator authenticates the ACE program selected by the derived proof order. +#! The verifier fetches the kernel digest list from the advice map under K, copies it to +#! `constants::kernel_witness_ptr`, and checks that it hashes to K. It binds the transcript to the +#! claim commitment and checks the kernel-ROM boundary against this list. #! -#! The kernel-procedure digests and the stack i/o are read from caller memory at the -#! supplied `kernel_ptr` and `stack_io_ptr`; the program digest is supplied as an operand word; the -#! final deferred root is loaded from the advice stack. `verify_proof` stages the reduced-inputs -#! block (kernel_H | program_digest | deferred_root | pad) before the transcript starts. +#! The returned deferred root is bound by the verified statement. The caller must settle it or +#! include it in its own statement. #! -#! Inputs: [kernel_ptr, num_kernel_digests, stack_io_ptr, PROG0, PROG1, PROG2, PROG3] -#! Outputs: [] -pub proc verify_proof - # --- Load and validate security parameters from advice stack --- +#! Inputs: [claim_ptr, ...] +#! Outputs: [D, num_queries, query_pow_bits, deep_pow_bits, folding_pow_bits, ...] +#! +#! 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. +#! - num_queries, query_pow_bits, deep_pow_bits, folding_pow_bits are the proof's +#! transcript-bound security parameters. +pub proc verify_vm_proof + # Validate before load_security_params writes verifier memory. + exec.assert_valid_claim_region + + # --- Load security parameters from advice stack --- exec.load_security_params - exec.assert_acceptable_options - # => [kernel_ptr, num_kernel_digests, stack_io_ptr, PROG0, PROG1, PROG2, PROG3] + # => [claim_ptr, ...] + + # --- Materialize the kernel digest witness from the advice map, keyed by the claim's K --- + + padw dup.4 add.4 mem_loadw_le + # => [K, claim_ptr, ...] + adv.push_mapval + adv_push + # => [num_kernel_digests, K, claim_ptr, ...] advice: [digest_0, .., digest_{n-1}] + + # The count must be bounded before the copy: it comes from advice and is only bound to K + # by the hash check, which runs after the writes. + u32assert.err="number of kernel procedure digests must fit in a u32" + dup u32lt.256 assert.err="number of kernel procedure digests exceeds KernelDescriptor::MAX_NUM_PROCEDURES" + + dup exec.constants::kernel_witness_ptr swap + # => [num_words = num_kernel_digests, write_ptr, num_kernel_digests, K, claim_ptr, ...] + exec.mem::pipe_words_to_memory + # The pipe's untagged hash state is unused: the binding check is the domain-tagged kernel + # commitment below. + # => [R0, R1, C, write_ptr', num_kernel_digests, K, claim_ptr, ...] + dropw dropw dropw drop + # => [num_kernel_digests, K, claim_ptr, ...] - # --- Stage the reduced-inputs block from the caller-supplied operands and advice --- + dup exec.constants::kernel_witness_ptr + # => [kernel_ptr, num_kernel_digests, num_kernel_digests, K, claim_ptr, ...] + exec.claim::kernel_commitment + # => [K', num_kernel_digests, K, claim_ptr, ...] + movup.4 movdn.8 + # => [K', K, num_kernel_digests, claim_ptr, ...] + assert_eqw.err="fetched kernel digests do not hash to the claim's kernel commitment" + # => [num_kernel_digests, claim_ptr, ...] - exec.public_inputs::stage_reduced_inputs + # --- Stage the boundary-inputs block from the claim region and advice --- + + exec.constants::kernel_witness_ptr movup.2 + # => [claim_ptr, kernel_ptr, num_kernel_digests, ...] + exec.public_inputs::stage_boundary_inputs # => [...] exec.load_air_context @@ -218,4 +291,14 @@ pub proc verify_proof exec.verifier::verify # => [...] + + # --- Return the deferred obligation and the transcript-bound security parameters --- + + exec.constants::get_folding_pow_bits + exec.constants::get_deep_pow_bits + exec.constants::get_query_pow_bits + exec.constants::get_number_queries + # => [num_queries, query_pow_bits, deep_pow_bits, folding_pow_bits, ...] + exec.public_inputs::load_deferred_root + # => [D, num_queries, query_pow_bits, deep_pow_bits, folding_pow_bits, ...] end diff --git a/crates/lib/core/asm/sys/vm/public_inputs.masm b/crates/lib/core/asm/sys/vm/public_inputs.masm index acff56eb73..a102968fde 100644 --- a/crates/lib/core/asm/sys/vm/public_inputs.masm +++ b/crates/lib/core/asm/sys/vm/public_inputs.masm @@ -2,33 +2,28 @@ use miden::core::stark::constants use miden::core::stark::public_inputs use miden::core::stark::random_coin use miden::core::crypto::hashes::poseidon2 +use miden::core::sys::vm::claim # PUBLIC INPUTS PROCESSING FOR MIDEN VM RECURSIVE VERIFIER # ================================================================================================= # -# This module handles the Miden VM-specific public input processing for the recursive verifier. -# It (a) computes `kernel_H`, the Poseidon2 hash (`hash_elements`) of all kernel-procedure -# digests, (b) materializes the kernel digests and populates the caller-facing reduced-inputs -# block and the FLPI section of the ACE READ region, and (c) absorbs every public input into the -# Fiat-Shamir transcript in a rate-aligned schedule mirroring `MidenMultiAir::observe` on the Rust -# side. The outer-LogUp boundary correction `c_total` is computed later, in step II -# (`observe_aux_trace`), once the aux randomness has been sampled from the transcript. +# This module stages the VM statement and absorbs `[CLAIM_HASH | deferred_root]` into Fiat-Shamir, +# matching `MidenMultiAir::observe`. CLAIM_HASH binds the program digest, kernel commitment, and +# stack I/O. The outer-LogUp correction `c_total` is computed in step II after sampling aux +# randomness. # # Memory layout populated (low -> high addresses): # -# reduced_inputs_ptr --> [ kernel_H (4 felts) ] caller-facing reduced-inputs -# [ program_digest (4 felts) ] block (16 felts). The trailing -# [ deferred_root (4 felts) ] pad keeps the FS observation -# [ zero pad (4 felts) ] rate-aligned (two 8-felt chunks). +# boundary_inputs_ptr --> [ kernel_H (4 felts) ] +# [ program_digest (4 felts) ] +# [ deferred_root (4 felts) ] +# [ reserved (4 felts) ] # # pi_ptr --> [ FLPI: 32 base felts as 32 EF slots ] stack i/o # # anchor --> [ aux_rand: beta0,beta1,alpha0,alpha1 ] AUX_RAND_ELEM_PTR (sampled # from the transcript in step II) # -# The trailing pad slot is written to zero before the reduced-inputs window is absorbed, so the FS -# observation does not depend on the scratch region being zero-initialized. -# # The outer-LogUp boundary correction accumulated at `C_TOTAL_PTR` is the signed sum of one # inverted bus term per boundary interaction: # @@ -46,30 +41,29 @@ use miden::core::crypto::hashes::poseidon2 # Requests (multiplicity +1) are added and the single response (−1) is subtracted, so `c_total` # is accumulated as `requests − response`. # -# Fiat-Shamir absorption order (`MidenMultiAir::observe`): -# 1. kernel_H + program_digest (4 + 4 = 8 felts) -# 2. deferred_root + zero pad (4 + 4 = 8 felts) -# 3. stack_inputs[0..8] (8 felts) -# 4. stack_inputs[8..16] (8 felts) -# 5. stack_outputs[0..8] (8 felts) -# 6. stack_outputs[8..16] (8 felts) +# Fiat-Shamir absorption order (`MidenMultiAir::observe`): one statement block +# 1. CLAIM_HASH + deferred_root (4 + 4 = 8 felts) +# where CLAIM_HASH is the canonical execution-claim commitment over +# `program_digest ‖ kernel_H ‖ stack_inputs ‖ stack_outputs` (computed over the caller's claim +# region by `claim::claim_commitment`). With RELATION_DIGEST pre-loaded in the transcript +# capacity by `init_seed`, the state after this block realizes `H(RELATION_DIGEST ‖ CLAIM_HASH ‖ D)`. +# The raw stack i/o and kernel digests remain public values for the constraint checks and the +# LogUp boundary without being separately absorbed. # # Data sources: -# - kernel digests: caller memory at `kernel_ptr` (operand), N word-aligned digests; hashed for -# kernel_H and re-read for the step-II boundary fold. -# - program_digest: operand word. -# - deferred_root: advice (4 canonical felts), loaded by `verify_proof`. -# - stack i/o (FLPI): caller memory at `stack_io_ptr` (operand), 32 base felts. -# -# `verify_proof` stages kernel_H, program_digest and deferred_root into the reduced-inputs -# block before the transcript starts; `process_public_inputs` then only absorbs into FS. +# - claim region: caller memory at `claim_ptr` (operand), 40 base felts `P | K | I | O`, +# fully populated by the caller from its own trusted data. +# - kernel digests: verifier memory at `kernel_ptr` (operand), N word-aligned digests. +# `verify_vm_proof` fetches them from the advice map and asserts they hash to +# the claim's K before calling into this module; the step-II boundary fold reads them +# from the same region. +# - deferred_root: advice (4 canonical felts), loaded by `stage_boundary_inputs`. # # CONSTANTS # ================================================================================================= -# Number of fixed length public inputs (in field elements): stack inputs (16) + stack -# outputs (16). These are the only public values referenced by the ACE circuit; the program -# digest and deferred root live in the caller-facing reduced-inputs block instead. +# ACE public inputs: 16 stack inputs + 16 stack outputs. + const NUM_FIXED_LEN_PUBLIC_INPUTS = 32 # Number of AIR instances in the Miden VM statement. @@ -80,10 +74,10 @@ const BUS_ID_KERNEL_ROM_INIT_PLUS_ONE = 1 # KernelRomInit (0) + 1 const BUS_ID_BLOCK_HASH_TABLE_PLUS_ONE = 2 # BlockHashTable (1) + 1 const BUS_ID_LOG_DEFERRED_ROOT_PLUS_ONE = 3 # LogDeferredRoot (2) + 1 -# Word offsets into the 16-felt reduced-inputs block at `reduced_inputs_ptr`: -# [ kernel_H (+0) | program_digest (+4) | deferred_root (+8) | zero pad (+12) ]. -const REDUCED_INPUTS_PROGRAM_OFFSET = 4 -const REDUCED_INPUTS_DEFERRED_OFFSET = 8 +# Word offsets into the 16-felt boundary-inputs block at `boundary_inputs_ptr`: +# [ kernel_H (+0) | program_digest (+4) | deferred_root (+8) | reserved (+12) ]. +const BOUNDARY_INPUTS_PROGRAM_OFFSET = 4 +const BOUNDARY_INPUTS_DEFERRED_OFFSET = 8 # CONSTANTS GETTERS @@ -113,17 +107,20 @@ pub proc process_public_inputs exec.constants::random_coin_input_len_ptr mem_load assertz.err="process_public_inputs: input buffer must be empty" - # 1) Compute and store `pi_ptr`; publish the fixed reduced-inputs block address separately. + # 1) Store the ACE and boundary-data pointers. exec.get_num_fixed_len_public_inputs exec.public_inputs::compute_and_store_public_inputs_address - exec.store_reduced_inputs_address + exec.store_boundary_inputs_address # => [...] - # 2) Observe the 16-felt reduced-inputs window into FS as two rate-aligned chunks. - exec.absorb_reduced_inputs_window_into_fs + # 2) Absorb [CLAIM_HASH | D]. + exec.constants::claim_address_ptr mem_load + exec.claim::claim_commitment + # => [CLAIM_HASH, ...] + exec.absorb_claim_and_deferred_into_fs # => [...] - # 3) Load FLPI (stack i/o) from caller memory into the FLPI region and absorb into FS. + # 3) Copy stack I/O into ACE READ. CLAIM_HASH already binds these values. exec.load_public_inputs # => [...] @@ -132,60 +129,69 @@ pub proc process_public_inputs # => [...] end -#! Publishes the fixed reduced-inputs block address for caller-facing output readers. +#! Publishes the fixed boundary-inputs block address for caller-facing output readers. #! #! Input: [...] #! Output: [...] -proc store_reduced_inputs_address - exec.constants::reduced_inputs_ptr - exec.constants::reduced_inputs_address_ptr mem_store +proc store_boundary_inputs_address + exec.constants::boundary_inputs_ptr + exec.constants::boundary_inputs_address_ptr mem_store end -#! Stages the reduced-inputs block at the fixed standalone `REDUCED_INPUTS_PTR` before the -#! transcript starts (called by `verify_proof`). +#! Stages VM boundary data before the transcript starts. #! -#! Writes, in order: -#! reduced_inputs+0 : kernel_H = hash_elements(kernel_ptr, 4·N), the kernel commitment over the -#! caller-owned digest region. -#! reduced_inputs+4 : program_digest, taken from the operand word. -#! reduced_inputs+8 : deferred_root, loaded from advice. +#! Precondition: the claim region is fully populated, and the digest witness at `kernel_ptr` +#! hashes to its K field (`verify_vm_proof` asserts this before calling). #! -#! Also persists the caller pointers `kernel_ptr` and `stack_io_ptr` and the digest count `N` into -#! their fixed cells so the step-I FLPI load and the step-II boundary fold can re-read the same -#! caller-owned regions. The trailing pad word is zeroed when the window is absorbed in step I. +#! Writes: +#! - +0: K from the claim +#! - +4: program_digest from the claim +#! - +8: deferred_root from advice +#! - +12: reserved and unchanged #! -#! Input: [kernel_ptr, N, stack_io_ptr, PROG0, PROG1, PROG2, PROG3, ...] +#! Also stores `claim_ptr`, `kernel_ptr`, and N for later steps. +#! +#! Input: [claim_ptr, kernel_ptr, N, ...] #! Output: [...] -pub proc stage_reduced_inputs - # Persist N (bounded by KernelDescriptor::MAX_NUM_PROCEDURES) and `kernel_ptr` for the step-II fold. - dup.1 +pub proc stage_boundary_inputs + # Persist N (bounded by KernelDescriptor::MAX_NUM_PROCEDURES) and the region pointers. + dup.2 u32assert.err="number of kernel procedure digests must fit in a u32" dup u32lt.256 assert.err="number of kernel procedure digests exceeds KernelDescriptor::MAX_NUM_PROCEDURES" exec.constants::num_kernel_digests_ptr mem_store - # => [kernel_ptr, N, stack_io_ptr, PROG..., ...] - dup exec.constants::kernel_digests_address_ptr mem_store - # => [kernel_ptr, N, stack_io_ptr, PROG..., ...] - - # kernel_H = hash_elements(kernel_ptr, 4·N) -> reduced_inputs+0. - swap mul.4 swap - # => [kernel_ptr, 4·N, stack_io_ptr, PROG..., ...] - exec.poseidon2::hash_elements - # => [kH0, kH1, kH2, kH3, stack_io_ptr, PROG..., ...] - exec.constants::reduced_inputs_ptr mem_storew_le dropw - # => [stack_io_ptr, PROG0, PROG1, PROG2, PROG3, ...] - - # Persist `stack_io_ptr` for the step-I FLPI load. - exec.constants::stack_io_address_ptr mem_store - # => [PROG0, PROG1, PROG2, PROG3, ...] - - # program_digest (operand) -> reduced_inputs + REDUCED_INPUTS_PROGRAM_OFFSET. - exec.constants::reduced_inputs_ptr add.REDUCED_INPUTS_PROGRAM_OFFSET mem_storew_le dropw + # => [claim_ptr, kernel_ptr, N, ...] + dup.1 exec.constants::kernel_digests_address_ptr mem_store + dup exec.constants::claim_address_ptr mem_store + # => [claim_ptr, kernel_ptr, N, ...] + movdn.2 drop drop + # => [claim_ptr, ...] + + # K: claim region (+4) -> the window (+0). + padw dup.4 add.4 mem_loadw_le + # => [K, claim_ptr, ...] + exec.constants::boundary_inputs_ptr mem_storew_le + # => [K, claim_ptr, ...] + + # program_digest: claim region (+0) -> boundary_inputs + BOUNDARY_INPUTS_PROGRAM_OFFSET. + # The dead K word is the load target (mem_loadw_le overwrites the top word). + movup.4 mem_loadw_le + # => [P, ...] + exec.constants::boundary_inputs_ptr add.BOUNDARY_INPUTS_PROGRAM_OFFSET mem_storew_le + # => [P, ...] + + # deferred_root from advice -> boundary_inputs + BOUNDARY_INPUTS_DEFERRED_OFFSET, loaded + # over the dead P word. + adv_loadw + exec.constants::boundary_inputs_ptr add.BOUNDARY_INPUTS_DEFERRED_OFFSET mem_storew_le dropw # => [...] +end - # deferred_root from advice -> reduced_inputs + REDUCED_INPUTS_DEFERRED_OFFSET. - padw adv_loadw - exec.constants::reduced_inputs_ptr add.REDUCED_INPUTS_DEFERRED_OFFSET mem_storew_le dropw - # => [...] +#! Loads the final deferred root from the boundary-inputs window. +#! +#! Input: [...] +#! Output: [D, ...] +pub proc load_deferred_root + padw exec.constants::boundary_inputs_ptr add.BOUNDARY_INPUTS_DEFERRED_OFFSET mem_loadw_le end # HELPER PROCEDURES @@ -291,7 +297,7 @@ proc fold_kernel_digests_into_acc # => [acc0, acc1, ...] end -#! Reads the canonical word `[d0, d1, d2, d3]` at `reduced_inputs_ptr + offset` (written in step I) +#! Reads the canonical word `[d0, d1, d2, d3]` at `boundary_inputs_ptr + offset` (written in step I) #! and computes the inverted bus term #! inv_term = 1 / ((α + i·γ) + msg(d)) #! where `i = bus_id_plus_one` and `msg(d) = Σ_{j<4} d_j·β^j`. The caller adds (request) or @@ -299,10 +305,10 @@ end #! #! Input: [bus_id_plus_one, offset, ...] #! Output: [inv_term0, inv_term1, ...] -proc fold_reduced_word_inv_term +proc fold_boundary_word_inv_term padw # => [0, 0, 0, 0, bus_id, offset, ...] - exec.constants::reduced_inputs_address_ptr mem_load + exec.constants::boundary_inputs_address_ptr mem_load dup.6 add # => [target, 0, 0, 0, 0, bus_id, offset, ...] mem_loadw_le @@ -326,9 +332,9 @@ end #! (step II). Requires the aux randomness to have been sampled into `AUX_RAND_ELEM_PTR` by #! `generate_aux_randomness` first. #! -#! Derives `γ = β^16`, then folds the request/response terms over the caller-owned kernel digests +#! Derives `γ = β^16`, then folds the request/response terms over the verifier-owned kernel digests #! at `KERNEL_DIGESTS_ADDRESS_PTR` (count at `NUM_KERNEL_DIGESTS_PTR`) and the program digest / -#! deferred root in the reduced-inputs block, all staged in `verify_proof`. Mirrors the module +#! deferred root in the boundary-inputs block, all staged in `stage_boundary_inputs`. Mirrors the module #! banner's `c_total` definition and `MidenMultiAir::eval_external`. #! #! Input: [...] @@ -348,9 +354,9 @@ pub proc compute_outer_logup_correction exec.fold_kernel_digests_into_acc # => [acc0, acc1, ...] - # Request b) program digest: + 1 / ((α + 2γ) + msg(program)) from reduced_inputs+4. - push.REDUCED_INPUTS_PROGRAM_OFFSET push.BUS_ID_BLOCK_HASH_TABLE_PLUS_ONE - exec.fold_reduced_word_inv_term + # Request b) program digest: + 1 / ((α + 2γ) + msg(program)) from boundary_inputs+4. + push.BOUNDARY_INPUTS_PROGRAM_OFFSET push.BUS_ID_BLOCK_HASH_TABLE_PLUS_ONE + exec.fold_boundary_word_inv_term ext2add # => [acc0, acc1, ...] @@ -361,9 +367,9 @@ pub proc compute_outer_logup_correction ext2add # => [acc0, acc1, ...] - # Response) deferred root: − 1 / ((α + 3γ) + msg(deferred_root)) from reduced_inputs+8. - push.REDUCED_INPUTS_DEFERRED_OFFSET push.BUS_ID_LOG_DEFERRED_ROOT_PLUS_ONE - exec.fold_reduced_word_inv_term + # Response) deferred root: − 1 / ((α + 3γ) + msg(deferred_root)) from boundary_inputs+8. + push.BOUNDARY_INPUTS_DEFERRED_OFFSET push.BUS_ID_LOG_DEFERRED_ROOT_PLUS_ONE + exec.fold_boundary_word_inv_term neg swap neg swap ext2add # => [acc0, acc1, ...] (acc = requests − response) @@ -374,79 +380,63 @@ pub proc compute_outer_logup_correction # => [...] end -#! Observes the 16-felt reduced-inputs window at `reduced_inputs_ptr + 0..+15` into the FS -#! transcript as two rate-aligned 8-felt chunks via `mem_stream + permute`: -#! Chunk 1: `[kernel_H | program_digest]` at reduced_inputs+0..+7. -#! Chunk 2: `[deferred_root | zero_pad]` at reduced_inputs+8..+15. -#! The trailing pad word is written to zero here so the absorption does not depend on the scratch -#! region being zero-initialized. +#! Absorbs the single statement block `[CLAIM_HASH | D]` into the FS transcript, mirroring +#! `MidenMultiAir::observe`. With RELATION_DIGEST pre-loaded in the transcript capacity +#! (`init_seed`), the resulting state realizes the factored statement binding +#! `H(RELATION_DIGEST ‖ CLAIM_HASH ‖ D)`. `D` is read from the boundary-inputs window. #! #! POSTCONDITION: random coin input_len=0, output_len=8 on return. #! -#! Input: [...] +#! Input: [CLAIM_HASH, ...] #! Output: [...] -proc absorb_reduced_inputs_window_into_fs - # Explicitly zero the trailing pad word at reduced_inputs+12 before absorbing the window. - padw exec.constants::reduced_inputs_address_ptr mem_load add.12 mem_storew_le dropw +proc absorb_claim_and_deferred_into_fs + # D from the boundary-inputs window + padw exec.constants::boundary_inputs_address_ptr mem_load add.BOUNDARY_INPUTS_DEFERRED_OFFSET mem_loadw_le + # => [D, CLAIM_HASH, ...] push.0 exec.constants::random_coin_output_len_ptr mem_store - exec.random_coin::load_random_coin_state - # => [R1, R2, C, ...] - - # `mem_stream` consumes its pointer from stack[12]. - exec.constants::reduced_inputs_address_ptr mem_load - movdn.12 - # => [R1, R2, C, base, ...] - - repeat.2 - mem_stream - # Bind the absorbed length (8) into the capacity before each absorb permutation. - movup.8 add.8 movdn.8 - exec.poseidon2::permute - end - # => [R1', R2', C', base+16, ...] + # Duplex overwrite mode: the stale rate words are never read, so load only the capacity + # and build the rate from [CLAIM_HASH | D] already on the stack. + exec.random_coin::get_capacity + # => [C, D, CLAIM_HASH, ...] + swapw.2 + # => [CLAIM_HASH, D, C, ...] + + # Bind the absorbed length (8) into the capacity before the absorb permutation. + movup.8 add.8 movdn.8 + exec.poseidon2::permute + # => [R1', R2', C', ...] exec.random_coin::store_random_coin_state push.8 exec.constants::random_coin_output_len_ptr mem_store - # => [base+16, ...] - - drop + # => [...] end -#! Loads stack i/o from caller memory at `STACK_IO_ADDRESS_PTR`, stores it at `pi_ptr` as extension -#! field elements (each base felt at offset `2*i`, zero in the high coordinate), and absorbs it -#! into the FS transcript. Each `load_base_store_extension_double_word_from_mem + permute` -#! iteration absorbs 8 base felts via direct sponge permutation. +#! Loads the claim region's stack i/o (at `claim_address_ptr + 8`) and stores it at `pi_ptr` as +#! extension field elements (each base felt at offset `2*i`, zero in the high coordinate). #! -#! POSTCONDITION: random coin input_len=0, output_len=8 on return. +#! The values are public inputs for the constraint checks only; they are NOT absorbed into the +#! FS transcript (the transcript binds them via CLAIM_HASH). #! #! Input: [...] #! Output: [...] proc load_public_inputs - push.0 exec.constants::random_coin_output_len_ptr mem_store - exec.random_coin::load_random_coin_state - # => [R1, R2, C, ...] - - exec.constants::stack_io_address_ptr mem_load + padw padw padw + # => [SCRATCH(12), ...] + exec.constants::claim_address_ptr mem_load add.8 movdn.12 exec.constants::public_inputs_address_ptr mem_load movdn.12 - # => [R1, R2, C, pi_ptr, stack_io_ptr, ...] + # => [SCRATCH(12), pi_ptr, claim_io_ptr, ...] - # 4 iterations × 8 = 32 = NUM_FIXED_LEN_PUBLIC_INPUTS. + # 4 iterations x 8 = 32 = NUM_FIXED_LEN_PUBLIC_INPUTS. repeat.4 exec.public_inputs::load_base_store_extension_double_word_from_mem - # Bind the absorbed length (8) into the capacity before each absorb permutation. - movup.8 add.8 movdn.8 - exec.poseidon2::permute end - # => [R1', R2', C', pi_ptr + 64, stack_io_ptr + 32, ...] + # => [SCRATCH'(12), pi_ptr + 64, claim_io_ptr + 32, ...] - exec.random_coin::store_random_coin_state - push.8 exec.constants::random_coin_output_len_ptr mem_store - # => [pi_ptr + 64, stack_io_ptr + 32, ...] - - drop drop + dropw dropw dropw drop drop + # => [...] end #! Observe the Miden AIR shape into the Fiat-Shamir transcript. diff --git a/crates/lib/core/docs/crypto/hashes/poseidon2.md b/crates/lib/core/docs/crypto/hashes/poseidon2.md index 84d41f5910..5e708b3425 100644 --- a/crates/lib/core/docs/crypto/hashes/poseidon2.md +++ b/crates/lib/core/docs/crypto/hashes/poseidon2.md @@ -13,6 +13,7 @@ | prepare_hasher_state | Initializes the hasher state required for the `hash_elements_with_state` procedure.

Depending on the provided pad_inputs_flag, this procedure initializes the hasher state using
different values for capacity element:
- If pad_inputs_flag = 1 the capacity element is set to 0. This will essentially "pad" the
hashed values with zeroes to the next multiple of 8.
- If pad_inputs_flag = 0 the capacity element is set to the remainder of the division of
number of hashed elements by 8 (num_elements%8).

Inputs: [ptr, num_elements, pad_inputs_flag]
Outputs: [R0, R1, C, ptr, end_pairs_addr, num_elements%8]

Where:
- ptr is the memory address of the first element to be hashed. This address must be
word-aligned - i.e., divisible by 4.
- num_elements is the number of elements to be hashed.
- pad_inputs_flag is the flag which indicates whether the values which will be hashed should be
padded with zeros to the next multiple of 8.
- R0, R1, C are three words representing the hasher state (R0 on top).
- end_pairs_addr is the memory address at which the pairs of words end.
- num_elements%8 is the number of elements which didn't fit to the word pairs and should be
hashed separately.
| | hash_elements_with_state | Computes hash of Felt values starting at the specified memory address using the provided hasher
state.

This procedure divides the hashing process into two parts: hashing pairs of words using
`absorb_double_words_from_memory` procedure and hashing the remaining values using the `permute`
procedure.

Inputs: [R0, R1, C, ptr, end_pairs_addr, num_elements%8]
Outputs: [HASH]

Where:
- ptr is the memory address of the first element to be hashed. This address must be
word-aligned - i.e., divisible by 4.
- R0, R1, C are three words representing the hasher state (R0 on top).
- end_pairs_addr is the memory address at which the pairs of words end.
- num_elements%8 is the number of elements which didn't fit to the word pairs and should be
hashed separately.
- HASH is the resulting hash of the provided memory values.
| | hash_elements | Computes hash of Felt values starting at the specified memory address.

This procedure divides the hashing process into two parts: hashing pairs of words using
`absorb_double_words_from_memory` procedure and hashing the remaining values using the `permute`
procedure.

Inputs: [ptr, num_elements]
Outputs: [HASH]

Where:
- ptr is the memory address of the first element to be hashed. This address must be
word-aligned - i.e., divisible by 4.
- num_elements is the number of elements to be hashed.
- HASH is the resulting hash of the provided memory values.

Cycles:
- If number of elements divides by 8: 52 cycles + 3 * words
- Else: 185 cycles + 3 * words
where `words` is the number of quads of input values.
| +| hash_elements_in_domain | Computes the domain-tagged hash of Felt values starting at the specified memory address.

Mirrors `Poseidon2::hash_elements_in_domain` on the Rust side: the first capacity element
carries the padding rule (`num_elements % 8`), the second carries the domain tag, and the
input is zero-padded to a rate multiple.

Inputs: [ptr, num_elements, domain]
Outputs: [HASH]

Where:
- ptr is the memory address of the first element to be hashed; must be word-aligned.
- num_elements is the number of elements to be hashed.
- domain is the domain-separation tag placed in the second capacity element.
| | pad_and_hash_elements | Computes hash of Felt values starting at the specified memory address.

Notice that this procedure essentially pads the elements to be hashed to the next multiple of 8
by setting the capacity element to 0.

This procedure divides the hashing process into two parts: hashing pairs of words using
`absorb_double_words_from_memory` procedure and hashing the remaining values using the `permute`
procedure.

Inputs: [ptr, num_elements]
Outputs: [HASH]

Where:
- ptr is the memory address of the first element to be hashed. This address must be
word-aligned - i.e., divisible by 4.
- num_elements is the number of elements to be hashed.
- HASH is the resulting hash of the provided memory values.

Cycles:
- If number of elements divides by 8: 52 cycles + 3 * words
- Else: 185 cycles + 3 * words
where `words` is the number of quads of input values.
| | hash | Computes Poseidon2 hash of a single word (256-bit input).

Inputs: [A]
Outputs: [B]

Where:
- A is the word to be hashed.
- B is the resulting hash, computed as `Poseidon2(A)`.

Cycles: 19
| | merge | Merges two words (256-bit digests) via Poseidon2 hash.

Inputs: [A, B]
Outputs: [C]

Where:
- A and B are the words to be merged.
- C is the resulting hash, computed as `Poseidon2(A \|\| B)`.

Cycles: 16
| diff --git a/crates/lib/core/docs/stark/constants.md b/crates/lib/core/docs/stark/constants.md index ca886ed480..a7a6564148 100644 --- a/crates/lib/core/docs/stark/constants.md +++ b/crates/lib/core/docs/stark/constants.md @@ -2,6 +2,7 @@ ## miden::core::stark::constants | Procedure | Description | | ----------- | ------------- | +| verifier_memory_start | Returns the first verifier-owned memory address.
| | set_lde_domain_info_word | Store details about the LDE domain.

The info stored is `[lde_size, log(lde_size), lde_g, 0]`.
| | get_lde_domain_info_word | Load details about the LDE domain.

The info stored is `[lde_size, log(lde_size), lde_g, 0]`.
| | get_lde_domain_depth | Returns log(lde_size), i.e., the depth of the LDE domain Merkle tree.
| diff --git a/crates/lib/core/docs/sys/vm.md b/crates/lib/core/docs/sys/vm.md index 32b2567a1a..5298fc20c5 100644 --- a/crates/lib/core/docs/sys/vm.md +++ b/crates/lib/core/docs/sys/vm.md @@ -2,5 +2,6 @@ ## miden::core::sys::vm | Procedure | Description | | ----------- | ------------- | +| conjectured_security_level | Computes the conjectured security level (in bits) attained by the given proof parameters.

Evaluates the integer fixed-point formula `min((num_queries * C) >> 16 + query_pow_bits, 128)`.
Must match miden_air::config::conjectured_security_level bit-for-bit (enforced by
cross-tests). Holds no policy: the caller applies its own acceptance threshold to the result.

PRECONDITION: `num_queries <= 150`, so `num_queries * C` fits in a u32 (the `u32shr` below
requires that). Parameters returned by `verify_vm_proof` satisfy this bound: the generic
verifier enforces it.

Inputs: [num_queries, query_pow_bits, ...]
Outputs: [level, ...]
| | load_air_context | Loads the VM-specific AIR context used by the generic STARK verifier.

Advice supplies log heights in fixed instance order:
[log_core, log_chiplets, log_poseidon2_permutation]

Writes per-AIR log heights, the maximum log height, ORDER_TAG, RELATION_DIGEST, and
ACE_REGISTRY_ROOT to memory.
| -| verify_proof | Verifies a STARK proof attesting to the correct execution of a program in the Miden VM.

Security parameters (num_queries, query_pow_bits, deep_pow_bits, folding_pow_bits) are
loaded from the advice stack, validated against the acceptable security policy, and
stored in memory for use by the generic verifier.

- Public inputs contain fixed-size input/output stacks, the program digest, and kernel procedure
digests.
- The wrapper records the AIR context before calling the generic STARK verifier.
- The constraints evaluator authenticates the ACE program selected by the derived proof order.

The kernel-procedure digests and the stack i/o are read from caller memory at the
supplied `kernel_ptr` and `stack_io_ptr`; the program digest is supplied as an operand word; the
final deferred root is loaded from the advice stack. `verify_proof` stages the reduced-inputs
block (kernel_H \| program_digest \| deferred_root \| pad) before the transcript starts.

Inputs: [kernel_ptr, num_kernel_digests, stack_io_ptr, PROG0, PROG1, PROG2, PROG3]
Outputs: []
| +| verify_vm_proof | Verifies a STARK proof of the caller-staged execution claim and returns the deferred
obligation the proof binds and the proof's transcript-bound security parameters.

The proof is consumed from the advice stack; request keys name this procedure's MAST root
(`CoreLibrary::recursive_verifier_root` on the operator side). A consumer that fetches the
proof by content derives the identical root in-VM via `procref` of this procedure, computes
`request_key(verifier_root, claim_commitment)` with `claim::request_key`, and moves the
registered proof package onto the advice stack before calling it.

Security parameters (num_queries, query_pow_bits, deep_pow_bits, folding_pow_bits) are loaded
from the advice stack and stored in memory for the generic verifier, which enforces their
structural bounds and binds them into the Fiat-Shamir transcript - so a proof cannot claim
parameters it was not produced with. This procedure holds no security-estimate formula and
no acceptance policy: it returns the transcript-bound parameters for the caller to grade
(e.g. with `conjectured_security_level`) under its own policy. An estimate or policy change
therefore never moves this procedure's root - request keys and registered proof packages
stay valid across such changes.

The caller stores the claim as `P (+0) \| K (+4) \| I (+8) \| O (+24)`. The complete 40-felt
region must be below `constants::verifier_memory_start`.

The verifier fetches the kernel digest list from the advice map under K, copies it to
`constants::kernel_witness_ptr`, and checks that it hashes to K. It binds the transcript to the
claim commitment and checks the kernel-ROM boundary against this list.

The returned deferred root is bound by the verified statement. The caller must settle it or
include it in its own statement.

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

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.
- num_queries, query_pow_bits, deep_pow_bits, folding_pow_bits are the proof's
transcript-bound security parameters.
| diff --git a/crates/lib/core/docs/sys/vm/claim.md b/crates/lib/core/docs/sys/vm/claim.md new file mode 100644 index 0000000000..22e25a3de3 --- /dev/null +++ b/crates/lib/core/docs/sys/vm/claim.md @@ -0,0 +1,7 @@ + +## miden::core::sys::vm::claim +| Procedure | Description | +| ----------- | ------------- | +| claim_commitment | Computes the canonical claim commitment (CLAIM_HASH) over a claim region.

The region must hold the fully populated 40-felt claim encoding P ‖ K ‖ I ‖ O. The commitment
names the claim: it forms proof-request keys and binds verified claims into a consumer's own
statement. The procedure verifies nothing.

Inputs: [claim_ptr, ...]
Outputs: [CLAIM_HASH, ...]

Where:
- claim_ptr is the word-aligned address of the claim region.
- CLAIM_HASH is the domain-tagged Poseidon2 hash of the 40-element encoding.
| +| kernel_commitment | Computes the canonical kernel commitment over a raw kernel-procedure digest list.

Mirrors miden_core::program::KernelDescriptor::commitment: the domain-tagged sequential hash
of the flattened digests, length-bound by the sponge's padding rule, in the descriptor's
canonical order.

Inputs: [kernel_ptr, num_kernel_digests, ...]
Outputs: [K, ...]

Where:
- kernel_ptr is the word-aligned address of the digest list.
- num_kernel_digests is the number of digests (words) in the list.
- K is the kernel commitment.
| +| request_key | Computes the advice-map key addressing a proof package for a claim under a verifier.

The key is the domain-tagged hash of `claim_commitment ‖ verifier_root` (exactly one rate
block, so a single permutation with no memory). It is a lookup address, not a trust anchor:
the verifier re-checks the retrieved package, so a wrong package fails verification. Both
inputs are program-owned (the verifier's MAST root via `procref`; the claim commitment via
`claim_commitment` or the program's own inputs) — neither comes from advice. Mirrors
miden_core::program::request_key.

Inputs: [VERIFIER_ROOT, CLAIM_COMMITMENT, ...]
Outputs: [REQUEST_KEY, ...]
| diff --git a/crates/lib/core/docs/sys/vm/public_inputs.md b/crates/lib/core/docs/sys/vm/public_inputs.md index 453cdf3cd1..326f5fc40a 100644 --- a/crates/lib/core/docs/sys/vm/public_inputs.md +++ b/crates/lib/core/docs/sys/vm/public_inputs.md @@ -3,5 +3,6 @@ | Procedure | Description | | ----------- | ------------- | | process_public_inputs | Processes the public inputs (step I of the verifier).

See module banner for the memory layout, the canonical FS schedule and the advice tape
order.

Precondition: random coin input_len=0 (guaranteed by `init_seed`, which absorbs the
protocol parameters as one full rate block).
Postcondition: the transcript input buffer holds the AIR-shape values. The generic verifier
observes the main-trace commitment next and flushes before sampling.

Input: [...]
Output: [...]
| -| stage_reduced_inputs | Stages the reduced-inputs block at the fixed standalone `REDUCED_INPUTS_PTR` before the
transcript starts (called by `verify_proof`).

Writes, in order:
reduced_inputs+0 : kernel_H = hash_elements(kernel_ptr, 4·N), the kernel commitment over the
caller-owned digest region.
reduced_inputs+4 : program_digest, taken from the operand word.
reduced_inputs+8 : deferred_root, loaded from advice.

Also persists the caller pointers `kernel_ptr` and `stack_io_ptr` and the digest count `N` into
their fixed cells so the step-I FLPI load and the step-II boundary fold can re-read the same
caller-owned regions. The trailing pad word is zeroed when the window is absorbed in step I.

Input: [kernel_ptr, N, stack_io_ptr, PROG0, PROG1, PROG2, PROG3, ...]
Output: [...]
| -| compute_outer_logup_correction | Computes the outer-LogUp boundary correction `c_total` and stores it at `C_TOTAL_PTR`
(step II). Requires the aux randomness to have been sampled into `AUX_RAND_ELEM_PTR` by
`generate_aux_randomness` first.

Derives `γ = β^16`, then folds the request/response terms over the caller-owned kernel digests
at `KERNEL_DIGESTS_ADDRESS_PTR` (count at `NUM_KERNEL_DIGESTS_PTR`) and the program digest /
deferred root in the reduced-inputs block, all staged in `verify_proof`. Mirrors the module
banner's `c_total` definition and `MidenMultiAir::eval_external`.

Input: [...]
Output: [...]
| +| stage_boundary_inputs | Stages VM boundary data before the transcript starts.

Precondition: the claim region is fully populated, and the digest witness at `kernel_ptr`
hashes to its K field (`verify_vm_proof` asserts this before calling).

Writes:
- +0: K from the claim
- +4: program_digest from the claim
- +8: deferred_root from advice
- +12: reserved and unchanged

Also stores `claim_ptr`, `kernel_ptr`, and N for later steps.

Input: [claim_ptr, kernel_ptr, N, ...]
Output: [...]
| +| load_deferred_root | Loads the final deferred root from the boundary-inputs window.

Input: [...]
Output: [D, ...]
| +| compute_outer_logup_correction | Computes the outer-LogUp boundary correction `c_total` and stores it at `C_TOTAL_PTR`
(step II). Requires the aux randomness to have been sampled into `AUX_RAND_ELEM_PTR` by
`generate_aux_randomness` first.

Derives `γ = β^16`, then folds the request/response terms over the verifier-owned kernel digests
at `KERNEL_DIGESTS_ADDRESS_PTR` (count at `NUM_KERNEL_DIGESTS_PTR`) and the program digest /
deferred root in the boundary-inputs block, all staged in `stage_boundary_inputs`. Mirrors the module
banner's `c_total` definition and `MidenMultiAir::eval_external`.

Input: [...]
Output: [...]
| diff --git a/crates/lib/core/src/lib.rs b/crates/lib/core/src/lib.rs index f1dcd22c08..35c12176e7 100644 --- a/crates/lib/core/src/lib.rs +++ b/crates/lib/core/src/lib.rs @@ -14,7 +14,7 @@ extern crate alloc; use alloc::{sync::Arc, vec, vec::Vec}; -use miden_core::{events::EventName, mast::MastForest}; +use miden_core::{Word, events::EventName, mast::MastForest}; use miden_mast_package::Package; use miden_processor::{HostLibrary, event::EventHandler}; use miden_utils_sync::LazyLock; @@ -124,6 +124,19 @@ impl CoreLibrary { self.0.clone() } + /// Returns the MAST root of `sys::vm::verify_vm_proof` — the verifier identity under + /// which recursive proofs are content-addressed. + /// + /// Operators pass this root when registering a proof package in the advice map + /// (`RecursiveVerifierInputs::into_request_package`). A consumer derives the identical value + /// in-VM with `procref` — a procedure's root is intrinsic to its own MAST — so the two sides + /// agree without a shared constant; consumers key their proof fetches by this root. + pub fn recursive_verifier_root(&self) -> Word { + self.0 + .get_procedure_root_by_path("::miden::core::sys::vm::verify_vm_proof") + .expect("verify_vm_proof is exported from the core library") + } + /// Returns the default event handlers required by the core library. /// /// Stack and memory print-style debug handlers write to stdout by default. These handlers can diff --git a/crates/lib/core/tests/stark/ace_read_check.rs b/crates/lib/core/tests/stark/ace_read_check.rs index 7a23179b6c..59f0bdcab1 100644 --- a/crates/lib/core/tests/stark/ace_read_check.rs +++ b/crates/lib/core/tests/stark/ace_read_check.rs @@ -22,23 +22,18 @@ const OOD_EVALUATIONS_PTR: u32 = 3225419784; const AUX_BUS_BOUNDARY_PTR: u32 = 3225420328; const AUXILIARY_ACE_INPUTS_PTR: u32 = 3225420336; const ACE_CIRCUIT_STREAM_PTR: u32 = 3225420376; +const ACE_CIRCUIT_PTR: u32 = 3225420960; -fn recursive_verifier_layout() -> InputLayout { +#[test] +fn ace_read_pointers_match_masm_layout() { let config = AceConfig { num_quotient_chunks: 8, layout: LayoutKind::Masm, num_airs: MIDEN_AIR_COUNT, }; - - build_multi_air_ace_circuit_for_order(config, &ProofOrder::instance_order()) - .expect("multi-AIR ace circuit") - .layout() - .clone() -} - -#[test] -fn ace_read_pointers_match_masm_layout() { - let layout = recursive_verifier_layout(); + let circuit = build_multi_air_ace_circuit_for_order(config, &ProofOrder::instance_order()) + .expect("multi-AIR ACE circuit"); + let layout = circuit.layout(); let beta = layout.index(InputKey::AuxRandBeta).expect("aux randomness beta"); let alpha = layout.index(InputKey::AuxRandAlpha).expect("aux randomness alpha"); @@ -57,6 +52,13 @@ fn ace_read_pointers_match_masm_layout() { ACE_CIRCUIT_STREAM_PTR - AUXILIARY_ACE_INPUTS_PTR, 2 * (layout.total_inputs - stark_vars) as u32 ); + + let encoded = circuit.to_ace().expect("encode multi-AIR ACE circuit"); + assert_eq!( + ACE_CIRCUIT_PTR, + ACE_CIRCUIT_STREAM_PTR + 2 * encoded.num_constants() as u32, + "ACE EVAL pointer must follow the encoded constant section" + ); } // EXTRACTION diff --git a/crates/lib/core/tests/stark/batch_query_gen.rs b/crates/lib/core/tests/stark/batch_query_gen.rs index d5f22055cf..1b206f286c 100644 --- a/crates/lib/core/tests/stark/batch_query_gen.rs +++ b/crates/lib/core/tests/stark/batch_query_gen.rs @@ -106,9 +106,14 @@ fn reference_source(setup: &str) -> String { #! sample_bits using the safe wrapper. proc sample_bits_safe - dup - pow2 - u32assert u32overflowing_sub.1 assertz + dup eq.32 + if.true + push.0xffffffff + else + dup + pow2 + u32assert u32overflowing_sub.1 assertz + end exec.sample_felt_safe u32split swap @@ -234,15 +239,14 @@ fn batch_vs_reference_num_queries(#[case] num_queries: u32) { assert_batch_matches_reference(&sponge, 7, num_queries, 17); } -/// Test across a range of LDE domain depths. -/// depth must be in 1..=31 (since pow2_shift = 2^(32-depth) must fit in u32, -/// and mask = 2^depth - 1 must be valid). +/// Depth 32 requires an all-ones u32 mask. #[rstest] #[case::depth_10(10)] #[case::depth_13(13)] #[case::depth_17(17)] #[case::depth_20(20)] #[case::depth_24(24)] +#[case::depth_32(32)] fn batch_vs_reference_depth(#[case] depth: u32) { let sponge = random_sponge(99); assert_batch_matches_reference(&sponge, 7, 27, depth); diff --git a/crates/lib/core/tests/stark/mod.rs b/crates/lib/core/tests/stark/mod.rs index 257da9d644..d0b1957af7 100644 --- a/crates/lib/core/tests/stark/mod.rs +++ b/crates/lib/core/tests/stark/mod.rs @@ -1,12 +1,11 @@ use std::{array, sync::Arc}; -use miden_air::PublicInputs; use miden_assembly::{Assembler, testing::source_file}; use miden_core::{ - Felt, WORD_SIZE, - deferred::{DeferredState, TRUE_DIGEST}, + Felt, WORD_SIZE, Word, field::{BasedVectorSpace, Field, PrimeCharacteristicRing, QuadFelt}, - proof::{DeferredProof, HashFunction}, + program::ExecutionClaim, + proof::HashFunction, }; use miden_mast_package::Package; use miden_processor::{DefaultHost, ExecutionOptions, Program, ProgramInfo}; @@ -73,9 +72,7 @@ fn stark_verifier_e2f4_with_kernel_single() { run_recursive_verifier(&data); } -// TODO: Un-ignore once recursive verifier supports deferred proofs #[test] -#[ignore = "recursive verifier does not yet support verifying deferred proofs"] fn stark_verifier_e2f4_with_deferred_root() { let data = generate_recursive_verifier_data(EXAMPLE_LOG_DEFERRED, fib_stack_inputs(), None); run_recursive_verifier(&data); @@ -307,81 +304,391 @@ pub fn generate_recursive_verifier_data( .unwrap(); let program_info = ProgramInfo::from(program); + let claim = ExecutionClaim::from_program_info(program_info, stack_inputs, stack_outputs); - // Resolve the proof-carried deferred root instead of assuming TRUE. This helper tests the - // recursive verifier for the outer VM STARK only; `prove_sync` constructed any nested deferred - // STARK proof locally, so its public root is the outer proof's public input. - let stark_proof = proof.miden_proof(); - let deferred_proof = proof.deferred_proof(); - let final_deferred_root = match deferred_proof { - DeferredProof::Empty => TRUE_DIGEST, - DeferredProof::Wire(wire) => { - DeferredState::from_wire(Arc::new(miden_precompiles::registry()), wire, usize::MAX) - .unwrap() - .root() - }, - DeferredProof::Stark { public_root, .. } => *public_root, - }; - let pub_inputs = - PublicInputs::new(program_info, stack_inputs, stack_outputs, final_deferred_root); - - generate_advice_inputs(stark_proof.bytes(), pub_inputs).unwrap() + generate_advice_inputs(&proof, &claim).unwrap() } -/// Run the recursive verifier MASM program with the given VerifierData. -fn run_recursive_verifier(data: &VerifierData) { - let source = " - use miden::core::sys::vm +/// The MAST root of `sys::vm::verify_vm_proof` - the verifier identity request keys +/// name. The operator side is `CoreLibrary::recursive_verifier_root`; a consumer computes the +/// identical value in-VM with `procref` (a procedure's root is intrinsic to its own MAST, +/// independent of the enclosing program), so the two sides agree without any shared constant. +fn verify_vm_proof_root() -> Word { + miden_core_lib::CoreLibrary::default().recursive_verifier_root() +} - # Copy `count` felts (a multiple of 4) from the advice tape into memory starting at `dst`. - # Input: [dst, count, ...] - # Output: [...] +/// Test-harness staging prologue: copies `count` felts (a multiple of 4) from the advice tape +/// into memory starting at `dst` (`[dst, count, ...] -> [...]`). Tests use the tape as their only +/// input channel, so claim staging means copying from it; a real consumer derives its claim from +/// its own data structures instead. +pub(crate) const COPY_ADVICE_TO_MEM: &str = " proc copy_advice_to_mem dup.1 push.0 neq while.true - # [dst, count, ...] padw adv_loadw - # [w0, w1, w2, w3, dst, count, ...] dup.4 mem_storew_le dropw - # [dst, count, ...] add.4 - # [dst+4, count, ...] swap sub.4 swap - # [dst+4, count-4, ...] dup.1 push.0 neq end drop drop end +"; + +/// Builds the consumer program: stage the claim from the consumer's own inputs, derive its +/// commitment, fetch the proof package registered under +/// `request_key(verifier_root, claim_commitment)`, verify, then grade the returned security +/// parameters and assert an acceptance threshold. `verify_vm_proof` holds no estimate formula +/// and no policy; both live in the consumer. +fn request_consumer_source() -> String { + format!( + " + use miden::core::sys + use miden::core::sys::vm + use miden::core::sys::vm::claim + + {COPY_ADVICE_TO_MEM} begin - # Initial stack: [kernel_ptr, num_kernel_digests, stack_io_ptr, PROG0..3]. + # Initial stack: [claim_ptr]. - # Copy kernel digests (4·num_kernel_digests felts) from advice into the caller region - # (kernel_ptr = 0). Build [dst=0, count=4N]. - dup.1 mul.4 push.0 + # 1) Fill the claim (the canonical 40-felt encoding) into VM memory from the + # consumer's own inputs (the advice tape) and derive the commitment that names it. + push.40 push.4096 exec.copy_advice_to_mem + exec.claim::claim_commitment + # => [CLAIM_COMMITMENT] + + # 2) Fetch the registered proof package by content: request keys name + # verify_vm_proof's root, derived in-VM via procref. + procref.vm::verify_vm_proof exec.claim::request_key + adv.push_mapval dropw + # => [...] + + # 3) Verify the staged claim; verify_vm_proof returns the deferred obligation + # and the proof's transcript-bound security parameters. + push.4096 + exec.vm::verify_vm_proof + # => [D, num_queries, query_pow_bits, deep_pow_bits, folding_pow_bits] + + # 4) Grade the returned parameters and assert the consumer's acceptance + # threshold (>= 96 conjectured bits). + swapw + # => [num_queries, query_pow_bits, deep_pow_bits, folding_pow_bits, D] + exec.vm::conjectured_security_level + # => [conjectured_level, deep_pow_bits, folding_pow_bits, D] + u32lt.96 assertz.err=\"proof security level is below the accepted target\" + drop drop + # => [D] + exec.sys::truncate_stack + end + " + ) +} + +/// The end-to-end guarantee of fetching by content: a proof fetched via `request_key` -> +/// `adv.push_mapval`) verifies when it matches the consumer's claim, and is rejected when it +/// does not — substitution-resistance falls out of verification, with no binding check. +#[test] +fn request_flow_binds_proof_to_claim() { + use miden_utils_testing::recursive_verifier::request_key; + + let intended = generate_recursive_verifier_data(EXAMPLE_FIB_SMALL, fib_stack_inputs(), None); + let other = generate_recursive_verifier_data(EXAMPLE_LOG_DEFERRED, fib_stack_inputs(), None); - # Copy stack i/o (32 felts) from advice into the caller region (stack_io_ptr = 4096). - # Build [dst=4096, count=32]. - push.32 push.4096 + let source = request_consumer_source(); + let entry = |proof_stream: &[u64]| -> (Word, Vec) { + let felts: Vec = proof_stream.iter().map(|&v| Felt::new_unchecked(v)).collect(); + (request_key(verify_vm_proof_root(), intended.claim_commitment), felts) + }; + + // Control: the intended proof, registered under its key, verifies. + let (k, v) = entry(&intended.proof_stream); + let mut advice_map = intended.advice_map.clone(); + advice_map.push((k, v)); + let ok = build_test!( + source.as_str(), + &intended.initial_stack, + &intended.claim_advice, + intended.store.clone(), + advice_map + ); + let (output, _) = ok.execute_for_output().expect("the matching proof must verify"); + ace_read_check::cross_check_ace_circuit(&output); + + // Substitution: a different claim's proof under the same key fails against the consumer's + // claim — the advice provider cannot pass off another proof. The intended claim's own + // content-addressed entries stay available so the kernel-witness fetch succeeds and + // rejection happens in verification, not because of a missing key. + let (k, v) = entry(&other.proof_stream); + let mut advice_map = other.advice_map.clone(); + advice_map.extend(intended.advice_map.iter().cloned()); + advice_map.push((k, v)); + let bad = build_test!( + source.as_str(), + &intended.initial_stack, + &intended.claim_advice, + other.store, + advice_map + ); + assert!( + bad.execute_for_output().is_err(), + "a proof for a different claim must be rejected by verification" + ); +} + +/// Two independently proven executions of one program (distinct stack i/o) verified inside a +/// single consumer program — each proof is registered +/// under `request_key(verifier_root, claim_commitment)` and fetched by content, independent of +/// its position in the advice. The consumer stages each claim from its own inputs and derives +/// the commitment that names the claim and addresses its proof entry, so passing requires the +/// in-VM claim-commitment, kernel-commitment, and request-key derivations to match their native +/// mirrors (a mismatch is a missing advice-map key). +#[test] +fn stark_verifier_e2f4_request_multi_proof() { + use miden_utils_testing::{crypto::MerkleStore, recursive_verifier::request_key}; + + let mut inputs = fib_stack_inputs(); + let tx0 = generate_recursive_verifier_data(EXAMPLE_FIB_SMALL, inputs.clone(), None); + inputs[13] = 7; // distinct claim: same program, different stack inputs + let tx1 = generate_recursive_verifier_data(EXAMPLE_FIB_SMALL, inputs, None); + + // One advice provider for both proofs: the tape carries only the consumer's claims; the + // proof streams are content-addressed in the advice map, merged with the (also + // content-addressed) query maps, kernel entries, and Merkle stores. + let verifier_root = verify_vm_proof_root(); + let mut tape = Vec::new(); + let mut store = MerkleStore::new(); + let mut advice_map = Vec::new(); + for tx in [&tx0, &tx1] { + tape.extend(tx.claim_advice.iter().copied()); + store.extend(tx.store.inner_nodes()); + advice_map.extend(tx.advice_map.iter().cloned()); + let stream: Vec = tx.proof_stream.iter().map(|&v| Felt::new_unchecked(v)).collect(); + advice_map.push((request_key(verifier_root, tx.claim_commitment), stream)); + } + + let source = format!( + " + use miden::core::sys + use miden::core::sys::vm + use miden::core::sys::vm::claim + + {COPY_ADVICE_TO_MEM} + + proc verify_one_claim + # Per claim: stage the fields from the consumer's own inputs, derive the + # commitment that names the claim, fetch and verify the proof package it + # addresses, then grade the returned parameters against the acceptance + # threshold. + push.40 push.4096 exec.copy_advice_to_mem # claim encoding -> claim region + push.4096 exec.claim::claim_commitment # => [CLAIM_COMMITMENT] + procref.vm::verify_vm_proof exec.claim::request_key + adv.push_mapval dropw # proof package -> advice stack + push.4096 exec.vm::verify_vm_proof # => [D, nq, q_pow, deep_pow, fold_pow] + swapw exec.vm::conjectured_security_level # => [level, deep_pow, fold_pow, D] + u32lt.96 assertz.err=\"proof security level is below the accepted target\" + drop drop # => [D] + end + + begin + exec.verify_one_claim dropw + exec.verify_one_claim dropw + exec.sys::truncate_stack + end + " + ); + + let test = build_test!(source.as_str(), &[0_u64], &tape, store, advice_map); + test.execute_for_output().expect("both content-addressed proofs must verify"); +} + +/// Runs the recursive verifier MASM program with the proof pre-loaded on the advice stack. +/// These runs are the differential guardrail that pins the proof-stream order against the MASM +/// consumption sequence, so they deliberately feed `verify_vm_proof` the proof stream directly +/// rather than fetching it through a request. +/// The MASM program that stages the claim into memory at `claim_ptr = 4096` and runs +/// `verify_vm_proof` positionally. Shared by the differential runner and the negative tests that +/// tamper the advice before verifying. +fn verify_vm_proof_program() -> String { + format!( + " + use miden::core::sys + use miden::core::sys::vm + + {COPY_ADVICE_TO_MEM} + + begin + # Initial stack: [claim_ptr]. + + # Copy the claim encoding P | K | I | O (40 felts) from advice into the claim + # region (claim_ptr = 4096); the kernel digest witness travels in the advice map. + push.40 push.4096 exec.copy_advice_to_mem - exec.vm::verify_proof + exec.vm::verify_vm_proof + # => [D, num_queries, query_pow_bits, deep_pow_bits, folding_pow_bits] + exec.sys::truncate_stack end - "; + " + ) +} + +fn run_recursive_verifier(data: &VerifierData) { + let source = verify_vm_proof_program(); let test = build_test!( - source, + source.as_str(), &data.initial_stack, - &data.advice_stack, + &data.advice_stack(), data.store.clone(), data.advice_map.clone() ); let (output, _host) = test.execute_for_output().expect("recursive verifier execution failed"); + // `verify_vm_proof` returns [D, num_queries, query_pow_bits, deep_pow_bits, folding_pow_bits]. + // Pin D (stack positions 0..4) to the proof-stream value and the parameter tail (positions + // 4..8) to the deployed PCS config so a change to the returned tuple's values or order is + // caught across every e2e configuration. + let params = miden_air::config::pcs_params(); + let returned = |i: usize| output.stack.get_element(i).map(|f| f.as_canonical_u64()); + for i in 0..WORD_SIZE { + assert_eq!(returned(i), Some(data.proof_stream[4 + i]), "returned deferred root felt {i}"); + } + assert_eq!(returned(4), Some(params.num_queries() as u64), "returned num_queries"); + assert_eq!(returned(5), Some(params.query_pow_bits() as u64), "returned query_pow_bits"); + assert_eq!(returned(6), Some(params.deep_pow_bits() as u64), "returned deep_pow_bits"); + assert_eq!(returned(7), Some(params.folding_pow_bits() as u64), "returned folding_pow_bits"); + // Cross-check: extract READ section, sanity-check values, evaluate circuit in Rust. ace_read_check::cross_check_ace_circuit(&output); } +/// Each of the four security parameters (num_queries, query_pow_bits, deep_pow_bits, +/// folding_pow_bits) is absorbed into the Fiat-Shamir transcript, so forging any one of them in +/// the proof stream diverges the transcript and fails verification. They are the first four +/// advice values `verify_vm_proof` reads, i.e. `proof_stream[0..4]`. +#[test] +fn each_security_parameter_is_transcript_bound() { + let source = verify_vm_proof_program(); + let base = generate_recursive_verifier_data(EXAMPLE_FIB_SMALL, fib_stack_inputs(), None); + for param in 0usize..4 { + let mut data = base.clone(); + // Forge the parameter downward. In particular, the proof's original PoW nonces satisfy + // the weaker targets, so rejection cannot be explained solely by demanding more work; + // the changed transcript/verification schedule must invalidate the proof. + data.proof_stream[param] -= 1; + let test = build_test!( + source.as_str(), + &data.initial_stack, + &data.advice_stack(), + data.store.clone(), + data.advice_map.clone() + ); + assert!( + test.execute_for_output().is_err(), + "verifier accepted a forged security parameter (index {param})" + ); + } +} + +/// The advice-fetched kernel digest list is copied into the verifier-owned region, then must hash +/// to the claim's kernel commitment K before it is folded into the outer-LogUp boundary. That +/// equality check in `verify_vm_proof` is the sole binding of the fetched digests to K, so its +/// rejection arm is pinned here: tampering the witness under K must fail at *that* assertion +/// specifically (matched by error code), not merely somewhere downstream — the boundary check +/// would also reject a tampered witness, so a plain `is_err` would not prove the bind is enforced. +#[test] +fn tampered_kernel_witness_is_rejected() { + let mut data = generate_recursive_verifier_data( + EXAMPLE_FIB_KERNEL_SMALL, + fib_stack_inputs(), + Some(KERNEL_EVEN_NUM_PROC), + ); + let k = claim_kernel_commitment(&data); + let witness = advice_map_value_mut(&mut data, k); + // Flip one felt of the first digest; the count (index 0) stays valid so the flow reaches the + // hash check rather than the count bound. + witness[1] = Felt::new_unchecked(witness[1].as_canonical_u64() ^ 1); + + let source = verify_vm_proof_program(); + let test = build_test!( + source.as_str(), + &data.initial_stack, + &data.advice_stack(), + data.store.clone(), + data.advice_map.clone() + ); + expect_assert_error_code_from_msg!( + test, + "fetched kernel digests do not hash to the claim's kernel commitment" + ); +} + +/// `verify_vm_proof` bounds the advice-supplied kernel digest count before copying it, on the +/// actual advice-map path (the direct `stage_boundary_inputs` bound is covered in `sys`). A +/// witness claiming 256 digests (one over `KernelDescriptor::MAX_NUM_PROCEDURES`) under K must be +/// rejected at that bound. +#[test] +fn verify_vm_proof_rejects_oversized_kernel_witness() { + let mut data = generate_recursive_verifier_data( + EXAMPLE_FIB_KERNEL_SMALL, + fib_stack_inputs(), + Some(KERNEL_EVEN_NUM_PROC), + ); + let k = claim_kernel_commitment(&data); + // Replace the witness with a count one over the maximum; the bound fires before the copy, so + // no digests are needed. + *advice_map_value_mut(&mut data, k) = vec![Felt::new_unchecked(256)]; + + let source = verify_vm_proof_program(); + let test = build_test!( + source.as_str(), + &data.initial_stack, + &data.advice_stack(), + data.store.clone(), + data.advice_map.clone() + ); + expect_assert_error_code_from_msg!( + test, + "number of kernel procedure digests exceeds KernelDescriptor::MAX_NUM_PROCEDURES" + ); +} + +/// Reject a claim that crosses into verifier-owned memory. +#[test] +fn verify_vm_proof_rejects_claim_crossing_verifier_memory_start() { + let source = " + use miden::core::stark::constants + use miden::core::sys::vm + begin + exec.constants::verifier_memory_start sub.4 + exec.vm::verify_vm_proof + end + "; + let test = build_test!(source, &[]); + expect_assert_error_code_from_msg!(test, "claim memory region overlaps verifier-owned memory"); +} + +/// The claim's kernel commitment K, read from felts [4, 8) of the caller-owned claim input. +fn claim_kernel_commitment(data: &VerifierData) -> Word { + Word::new([ + Felt::new_unchecked(data.claim_advice[4]), + Felt::new_unchecked(data.claim_advice[5]), + Felt::new_unchecked(data.claim_advice[6]), + Felt::new_unchecked(data.claim_advice[7]), + ]) +} + +/// Mutable reference to the advice-map value stored under `key`. +fn advice_map_value_mut(data: &mut VerifierData, key: Word) -> &mut Vec { + let entry = data + .advice_map + .iter_mut() + .find(|(k, _)| *k == key) + .expect("advice map has an entry under the requested key"); + &mut entry.1 +} + // EXAMPLE PROGRAMS // ================================================================================================ @@ -434,7 +741,7 @@ fn fib_stack_inputs() -> Vec { // 255 = KernelDescriptor::MAX_NUM_PROCEDURES, the maximum number of kernel procedures a Statement // accepts. #[case(255)] -fn reduced_inputs_and_outer_logup_boundary(#[case] num_kernel_proc_digests: usize) { +fn boundary_inputs_and_outer_logup_boundary(#[case] num_kernel_proc_digests: usize) { let seed = [0_u8; 32]; let mut rng = ChaCha20Rng::from_seed(seed); @@ -447,51 +754,55 @@ fn reduced_inputs_and_outer_logup_boundary(#[case] num_kernel_proc_digests: usiz let auxiliary_rand_values: [u64; 4] = array::from_fn(|_| rng.next_u64()); // Caller-owned memory regions (must match the MASM constants below): kernel digests at 0, - // stack i/o at 4096. + // the claim region at 4096. const KERNEL_PTR: u64 = 0; - const STACK_IO_PTR: u64 = 4096; + const CLAIM_PTR: u64 = 4096; - // 2) Initial operand stack: `stage_reduced_inputs` operands. - let mut initial_stack = vec![KERNEL_PTR, num_kernel_proc_digests as u64, STACK_IO_PTR]; - initial_stack.extend_from_slice(&program_digest); + // 2) Initial operand stack: `stage_boundary_inputs` operands. + let initial_stack = vec![CLAIM_PTR, KERNEL_PTR, num_kernel_proc_digests as u64]; - // 3) Build the advice stack: kernel digests (4N) and stack i/o (32) for the marshalling, then - // deferred root for `stage_reduced_inputs`, then the aux randomness consumed by the test - // prologue that drives `compute_outer_logup_correction`. + // 3) Build the advice stack: kernel digests (4N) for the caller witness region, then the full + // claim encoding (P, K, I, O) for the staging — the claim region arrives at + // `stage_boundary_inputs` fully populated, K included — then the deferred root for + // `stage_boundary_inputs`, then the aux randomness consumed by the test prologue that drives + // `compute_outer_logup_correction`. + let digest_felts: Vec = + kernel_digest_felts.iter().map(|&v| Felt::new_unchecked(v)).collect(); + let expected_kernel_h = miden_air::hash_kernel_digests(&digest_felts); let mut advice_stack = Vec::new(); advice_stack.extend_from_slice(&kernel_digest_felts); + advice_stack.extend_from_slice(&program_digest); + advice_stack.extend(expected_kernel_h.iter().map(Felt::as_canonical_u64)); advice_stack.extend_from_slice(&stack_inputs); advice_stack.extend_from_slice(&stack_outputs); advice_stack.extend_from_slice(&deferred_root); advice_stack.extend_from_slice(&auxiliary_rand_values); - // 4) Marshal the caller regions, stage the reduced-inputs block, run process_public_inputs, - // then emulate step II: place the aux randomness at AUX_RAND_ELEM_PTR (where + // 4) Stage the caller regions, stage the boundary-inputs block, run process_public_inputs, then + // emulate step II: place the aux randomness at AUX_RAND_ELEM_PTR (where // `generate_aux_randomness` samples it) and compute `c_total`. - let source = " + let source = format!( + " use miden::core::stark::random_coin use miden::core::stark::constants use miden::core::sys::vm::public_inputs - proc copy_advice_to_mem - dup.1 push.0 neq - while.true - padw adv_loadw - dup.4 mem_storew_le dropw - add.4 - swap sub.4 swap - dup.1 push.0 neq - end - drop drop - end + {COPY_ADVICE_TO_MEM} begin - dup.1 mul.4 push.0 + # Initial stack: [claim_ptr, kernel_ptr, num_kernel_digests]. + + # Copy kernel digests (4·num_kernel_digests felts) from advice into the witness + # region (kernel_ptr = 0). Build [dst=0, count=4N]. + dup.2 mul.4 push.0 exec.copy_advice_to_mem - push.32 push.4096 + + # Copy the full claim encoding P | K | I | O (40 felts) from advice into the claim + # region (claim_ptr = 4096). + push.40 push.4096 exec.copy_advice_to_mem - exec.public_inputs::stage_reduced_inputs + exec.public_inputs::stage_boundary_inputs push.10 exec.constants::set_core_trace_length_log push.10 exec.constants::set_chiplets_trace_length_log @@ -505,9 +816,10 @@ fn reduced_inputs_and_outer_logup_boundary(#[case] num_kernel_proc_digests: usiz padw adv_loadw exec.constants::aux_rand_elem_ptr mem_storew_le dropw exec.public_inputs::compute_outer_logup_correction end - "; + " + ); - let test = build_test!(source, &initial_stack, &advice_stack); + let test = build_test!(source.as_str(), &initial_stack, &advice_stack); let (output, _host) = test.execute_for_output().expect("execution failed"); use miden_processor::ContextId; @@ -520,16 +832,14 @@ fn reduced_inputs_and_outer_logup_boundary(#[case] num_kernel_proc_digests: usiz .as_canonical_u64() }; - // Must match `REDUCED_INPUTS_ADDRESS_PTR` / `PUBLIC_INPUTS_ADDRESS_PTR` / `C_TOTAL_PTR` + // Must match `BOUNDARY_INPUTS_ADDRESS_PTR` / `PUBLIC_INPUTS_ADDRESS_PTR` / `C_TOTAL_PTR` // in `crates/lib/core/asm/stark/constants.masm`. let reduced_ptr = read_elem(3223322670) as u32; let pi_ptr = read_elem(3223322671) as u32; let c_total_ptr = 3223322704_u32; - // 4) kernel_H at reduced_inputs+0..4 must match the Rust mirror. - let digest_felts: Vec = - kernel_digest_felts.iter().map(|&v| Felt::new_unchecked(v)).collect(); - let expected_kernel_h = miden_air::hash_kernel_digests(&digest_felts); + // 4) kernel_H at boundary_inputs+0..4 must match the Rust mirror (staged from the claim + // region's K slot). for (i, expected) in expected_kernel_h.iter().enumerate() { assert_eq!( read_elem(reduced_ptr + i as u32), @@ -538,19 +848,14 @@ fn reduced_inputs_and_outer_logup_boundary(#[case] num_kernel_proc_digests: usiz ); } - // 5) program_digest / deferred_root pass through to reduced_inputs+4..12; the trailing pad word - // at +12..16 must be zero. + // 5) program_digest / deferred_root pass through to boundary_inputs+4..12. for (i, &v) in program_digest.iter().chain(deferred_root.iter()).enumerate() { assert_eq!( read_elem(reduced_ptr + 4 + i as u32), v, - "reduced-inputs window felt {i} mismatch" + "boundary-inputs window felt {i} mismatch" ); } - for i in 12..16 { - assert_eq!(read_elem(reduced_ptr + i), 0, "reduced-inputs pad felt {i} must be zero"); - } - // 6) FLPI region holds the stack i/o as EF elements ([val, 0] per slot). for (i, &v) in stack_inputs.iter().chain(stack_outputs.iter()).enumerate() { assert_eq!(read_elem(pi_ptr + 2 * i as u32), v, "FLPI slot {i} value mismatch"); @@ -608,30 +913,30 @@ fn reduced_inputs_and_outer_logup_boundary(#[case] num_kernel_proc_digests: usiz ); } -/// The recursive verifier must reject statements with more kernel-procedure digests than a -/// `KernelDescriptor` can contain. 256 digests is one over the maximum, so -/// `stage_reduced_inputs` must fail on the digest-count bound before reading caller memory or -/// advice. +/// `stage_boundary_inputs` must reject a kernel-procedure digest count over the maximum +/// (`KernelDescriptor::MAX_NUM_PROCEDURES` = 255) before reading caller memory or advice — the +/// count bound is its first check. The same bound on the top-level `verify_vm_proof` advice path +/// is covered by `verify_vm_proof_rejects_oversized_kernel_witness`. #[test] fn rejects_too_many_kernel_proc_digests() { let num_kernel_proc_digests = 256_u64; // one over the maximum (255) - // Operands: [kernel_ptr, N, stack_io_ptr, PROG0..3]. The bound on N is the first check in - // `stage_reduced_inputs`, so no caller memory or advice is needed. - let initial_stack = vec![0_u64, num_kernel_proc_digests, 4096, 1, 2, 3, 4]; + // Operands: [claim_ptr, kernel_ptr, N]. The bound on N is the first check in + // `stage_boundary_inputs`, so the pointer operands are unused and no memory or advice is set. + let initial_stack = vec![0_u64, 0, num_kernel_proc_digests]; let source = " use miden::core::sys::vm::public_inputs begin - exec.public_inputs::stage_reduced_inputs + exec.public_inputs::stage_boundary_inputs end "; let test = build_test!(source, &initial_stack); assert!( test.execute_for_output().is_err(), - "verifier accepted {num_kernel_proc_digests} kernel digests, exceeding max_aux_inputs" + "stage_boundary_inputs accepted {num_kernel_proc_digests} kernel digests, exceeding the maximum" ); } diff --git a/crates/lib/core/tests/sys/mod.rs b/crates/lib/core/tests/sys/mod.rs index 09043ceba2..ec400657b0 100644 --- a/crates/lib/core/tests/sys/mod.rs +++ b/crates/lib/core/tests/sys/mod.rs @@ -11,21 +11,21 @@ fn truncate_stack() { } #[test] -fn reduce_kernel_digests_upper_bound() { - // `stage_reduced_inputs` takes the digest count `N` as an operand and asserts it fits +fn stage_rejects_digest_count_over_bound() { + // `stage_boundary_inputs` takes the digest count `N` as an operand and asserts it fits // `Kernel::MAX_NUM_PROCEDURES` (`N < 256`). The bound is its first check, so no caller memory // or advice is required. // - // Operands: [kernel_ptr, N, stack_io_ptr, PROG0..3]. + // Operands: [claim_ptr, kernel_ptr, N]. let source = " use miden::core::sys::vm::public_inputs begin - exec.public_inputs::stage_reduced_inputs + exec.public_inputs::stage_boundary_inputs end "; let num_kernel_proc_digests = 256_u64; // one over the maximum (255) - let initial_stack = vec![0_u64, num_kernel_proc_digests, 4096, 1, 2, 3, 4]; + let initial_stack = vec![4096_u64, 0, num_kernel_proc_digests]; let test = build_test!(source, &initial_stack); expect_assert_error_message!(test); @@ -49,3 +49,354 @@ proptest! { build_test!(&source, &test_values).prop_expect_stack(&expected_values)?; } } + +// EXECUTION CLAIM CROSS-TESTS +// ================================================================================================ + +/// The MASM `sys::vm::claim::claim_commitment` procedure must agree with the native +/// `ExecutionClaim::commitment` on the same claim region (same encoding, same domain tag, same +/// capacity layout). +#[test] +fn masm_claim_commitment_matches_native() { + use miden_core::{ + Felt, Word, + program::{ExecutionClaim, KernelDescriptor, ProgramInfo, StackInputs, StackOutputs}, + }; + + let word = |a: u64, b: u64, c: u64, d: u64| -> Word { + [ + Felt::new_unchecked(a), + Felt::new_unchecked(b), + Felt::new_unchecked(c), + Felt::new_unchecked(d), + ] + .into() + }; + + let kernel = + KernelDescriptor::from_hashes(vec![word(11, 12, 13, 14), word(21, 22, 23, 24)]).unwrap(); + let program_info = ProgramInfo::new(word(1, 2, 3, 4), kernel); + let stack_inputs = + StackInputs::new(&[Felt::new_unchecked(5), Felt::new_unchecked(6), Felt::new_unchecked(7)]) + .unwrap(); + let stack_outputs = + StackOutputs::new(&[Felt::new_unchecked(8), Felt::new_unchecked(9)]).unwrap(); + let claim = ExecutionClaim::from_program_info(program_info, stack_inputs, stack_outputs); + + // stage the canonical 40-felt encoding into a claim region at CLAIM_PTR + const CLAIM_PTR: u64 = 1000; + let elements = claim.to_elements(); + let mut store_ops = String::new(); + for (i, chunk) in elements.chunks(4).enumerate() { + // `push.e3.e2.e1.e0.addr mem_storew_le` stores [e0, e1, e2, e3] at addr..addr+4 + store_ops.push_str(&format!( + "push.{}.{}.{}.{}.{} mem_storew_le dropw\n", + chunk[3].as_canonical_u64(), + chunk[2].as_canonical_u64(), + chunk[1].as_canonical_u64(), + chunk[0].as_canonical_u64(), + CLAIM_PTR + 4 * i as u64, + )); + } + + let source = format!( + " + use miden::core::sys + use miden::core::sys::vm::claim + + begin + {store_ops} + push.{CLAIM_PTR} + exec.claim::claim_commitment + exec.sys::truncate_stack + end + " + ); + + let mut expected: Vec = + claim.commitment().as_elements().iter().map(Felt::as_canonical_u64).collect(); + expected.resize(16, 0); + build_test!(source.as_str(), &[]).expect_stack(&expected); +} + +/// The MASM `poseidon2::hash_elements_in_domain` must agree with the native implementation for +/// rate-aligned, unaligned, and empty inputs, exercising the kernel commitment's domain. +#[test] +fn hash_elements_in_domain_matches_native() { + use miden_core::{Felt, chiplets::hasher}; + + for num_elements in [0usize, 5, 8, 11, 16, 40] { + let values: Vec = (1..=num_elements as u64).collect(); + let felts: Vec = values.iter().map(|&v| Felt::new_unchecked(v)).collect(); + let domain = miden_core::program::KERNEL_DOMAIN_TAG; + + const PTR: u64 = 1000; + let mut store_ops = String::new(); + let mut padded = values.clone(); + padded.resize(values.len().next_multiple_of(4).max(4), 0); + for (i, chunk) in padded.chunks(4).enumerate() { + store_ops.push_str(&format!( + "push.{}.{}.{}.{}.{} mem_storew_le dropw\n", + chunk[3], + chunk[2], + chunk[1], + chunk[0], + PTR + 4 * i as u64, + )); + } + + let source = format!( + " + use miden::core::sys + use miden::core::crypto::hashes::poseidon2 + + begin + {store_ops} + push.{domain_int} + push.{num_elements} + push.{PTR} + exec.poseidon2::hash_elements_in_domain + exec.sys::truncate_stack + end + ", + domain_int = domain.as_canonical_u64(), + ); + + let mut expected: Vec = hasher::hash_elements_in_domain(&felts, domain) + .as_elements() + .iter() + .map(Felt::as_canonical_u64) + .collect(); + expected.resize(16, 0); + build_test!(source.as_str(), &[]).expect_stack(&expected); + } +} + +/// The MASM `sys::vm::claim::request_key` must agree with the native `request_key` on the same +/// (verifier_root, claim_commitment) pair. +#[test] +fn masm_request_key_matches_native() { + use miden_core::{Felt, Word, program::request_key}; + + let word = |a: u64, b: u64, c: u64, d: u64| -> Word { + [ + Felt::new_unchecked(a), + Felt::new_unchecked(b), + Felt::new_unchecked(c), + Felt::new_unchecked(d), + ] + .into() + }; + let verifier_root = word(101, 102, 103, 104); + let claim_commitment = word(201, 202, 203, 204); + + // Push CLAIM_COMMITMENT then VERIFIER_ROOT so VERIFIER_ROOT ends on top (word 0). + let push = |w: Word| -> String { + let e = w.as_elements(); + format!( + "push.{}.{}.{}.{}", + e[3].as_canonical_u64(), + e[2].as_canonical_u64(), + e[1].as_canonical_u64(), + e[0].as_canonical_u64() + ) + }; + let source = format!( + " + use miden::core::sys + use miden::core::sys::vm::claim + + begin + {} + {} + exec.claim::request_key + exec.sys::truncate_stack + end + ", + push(claim_commitment), + push(verifier_root), + ); + + let mut expected: Vec = request_key(verifier_root, claim_commitment) + .as_elements() + .iter() + .map(Felt::as_canonical_u64) + .collect(); + expected.resize(16, 0); + build_test!(source.as_str(), &[]).expect_stack(&expected); +} + +/// End-to-end request round-trip: the host registers a package stream under +/// `request_key(verifier_root, claim_commitment)`, and a consumer that holds only those two +/// words computes the same key and retrieves the stream with `adv.push_mapval`. Proves the +/// host helper and the MASM `request_key` address the same advice-map entry. +#[test] +fn request_round_trip_retrieves_registered_package() { + use miden_core::{Felt, Word}; + use miden_utils_testing::recursive_verifier::request_key; + + let word = |a: u64, b: u64, c: u64, d: u64| -> Word { + [ + Felt::new_unchecked(a), + Felt::new_unchecked(b), + Felt::new_unchecked(c), + Felt::new_unchecked(d), + ] + .into() + }; + let verifier_root = word(11, 12, 13, 14); + let claim_commitment = word(21, 22, 23, 24); + let stream: [Felt; 4] = [ + Felt::new_unchecked(100), + Felt::new_unchecked(200), + Felt::new_unchecked(300), + Felt::new_unchecked(400), + ]; + + let key = request_key(verifier_root, claim_commitment); + let values: Vec = stream.to_vec(); + + let push = |w: Word| -> String { + let e = w.as_elements(); + format!( + "push.{}.{}.{}.{}", + e[3].as_canonical_u64(), + e[2].as_canonical_u64(), + e[1].as_canonical_u64(), + e[0].as_canonical_u64() + ) + }; + // Consumer holds (claim_commitment, verifier_root) from its own inputs; pushes them in the + // request_key contract order (verifier on top), derives the key, fetches the stream, and + // reads the four values back onto the operand stack. + let source = format!( + " + use miden::core::sys + use miden::core::sys::vm::claim + + begin + {} + {} + exec.claim::request_key + adv.push_mapval + drop drop drop drop + adv_push adv_push adv_push adv_push + exec.sys::truncate_stack + end + ", + push(claim_commitment), + push(verifier_root), + ); + + // Map value the host registered under the request key. + let advice_map = vec![(key, values)]; + let mut expected: Vec = stream.iter().map(Felt::as_canonical_u64).collect(); + expected.reverse(); // four adv_push results, top-first + expected.resize(16, 0); + build_test!( + source.as_str(), + &[], + Vec::::new(), + miden_utils_testing::crypto::MerkleStore::new(), + advice_map + ) + .expect_stack(&expected); +} + +/// The MASM `sys::vm::conjectured_security_level` procedure must agree with the native +/// `miden_air::config::conjectured_security_level` on every input in the verifier's domain: +/// `num_queries` is effectively a `u8` (the generic verifier bounds it to `<= 150`) and +/// `query_pow_bits < 32`. One VM run evaluates the whole grid, storing the MASM level for +/// `(nq, pow)` at address `nq * POW_BOUND + pow`; the host then checks every cell against the +/// native value. This includes the calibration points +/// (27, 16) -> 95 and (27, 17) -> 96. +#[test] +fn masm_conjectured_security_level_matches_native() { + use miden_core::Felt; + use miden_processor::ContextId; + + const NQ_BOUND: u64 = 256; + const POW_BOUND: u64 = 32; + + let source = format!( + " + use miden::core::sys::vm + + begin + push.0 + dup push.{NQ_BOUND} u32lt + while.true + # => [nq] + push.0 + dup push.{POW_BOUND} u32lt + while.true + # => [pow, nq] + dup dup.2 + # => [nq, pow, pow, nq] + exec.vm::conjectured_security_level + # => [level, pow, nq] + dup.2 push.{POW_BOUND} mul dup.2 add + # => [nq*POW_BOUND + pow, level, pow, nq] + mem_store + # => [pow, nq] + add.1 + dup push.{POW_BOUND} u32lt + end + drop + add.1 + dup push.{NQ_BOUND} u32lt + end + drop + end + " + ); + + let test = build_test!(source.as_str(), &[]); + let (output, _host) = test.execute_for_output().expect("estimator sweep execution failed"); + + let ctx = ContextId::root(); + for nq in 0..NQ_BOUND { + for pow in 0..POW_BOUND { + let addr = (nq * POW_BOUND + pow) as u32; + let masm = output + .memory + .read_element(ctx, Felt::new_unchecked(u64::from(addr))) + .expect("every swept address is written") + .as_canonical_u64(); + let native = + u64::from(miden_air::config::conjectured_security_level(nq as u32, pow as u32)); + assert_eq!(masm, native, "mismatch at num_queries={nq}, query_pow_bits={pow}"); + } + } +} + +/// A consumer's acceptance threshold (`u32lt.TARGET assertz` over the estimator's level) must +/// reject a below-target level and accept an at-target one. This exercises the estimator and +/// threshold in isolation; the stark e2e consumer tests apply the same threshold after a real +/// verification but cannot reach the reject arm, because the standard prover does not emit +/// reduced-query proofs. +#[test] +fn security_level_threshold_rejects_below_target() { + // Same target as the stark e2e consumer program. + const TARGET: u64 = 96; + + let source = format!( + " + use miden::core::sys::vm + + begin + # Stack: [num_queries, query_pow_bits] - as returned by `verify_vm_proof`. + exec.vm::conjectured_security_level + u32lt.{TARGET} assertz + end + " + ); + + // (22 queries, 16 pow) grades to 80 < 96: the threshold assert must fail. + let below = build_test!(source.as_str(), &[22_u64, 16]); + assert!(below.execute_for_output().is_err(), "a below-target level must be rejected"); + + // (27 queries, 17 pow) grades to exactly 96: the threshold assert must pass. + let at = build_test!(source.as_str(), &[27_u64, 17]); + at.execute_for_output().expect("an at-target level must be accepted"); +} diff --git a/crates/test-utils/Cargo.toml b/crates/test-utils/Cargo.toml index db53c40265..a89140d182 100644 --- a/crates/test-utils/Cargo.toml +++ b/crates/test-utils/Cargo.toml @@ -37,9 +37,7 @@ miden-processor = { workspace = true, features = ["testing"] } miden-prover.workspace = true miden-verifier.workspace = true proptest = { workspace = true, optional = true } -serde-wincode.workspace = true test-case = "3.2" -thiserror.workspace = true [target.'cfg(target_family = "wasm")'.dependencies] pretty_assertions = { workspace = true, default-features = false, features = [ diff --git a/crates/test-utils/src/lib.rs b/crates/test-utils/src/lib.rs index e95e473735..e73ef0d6d3 100644 --- a/crates/test-utils/src/lib.rs +++ b/crates/test-utils/src/lib.rs @@ -26,7 +26,7 @@ pub use miden_core::{ EMPTY_WORD, Felt, ONE, WORD_SIZE, Word, ZERO, chiplets::hasher::{STATE_WIDTH, hash_elements}, field::{Field, PrimeCharacteristicRing, PrimeField64, QuadFelt}, - program::{MIN_STACK_DEPTH, StackInputs, StackOutputs}, + program::{ExecutionClaim, MIN_STACK_DEPTH, StackInputs, StackOutputs}, utils::{IntoBytes, ToElements, group_slice_elements}, }; use miden_core::{ @@ -48,7 +48,7 @@ use miden_processor::{ #[cfg(not(target_family = "wasm"))] pub use miden_prover::prove_sync; pub use miden_prover::{ProvingOptions, prove}; -pub use miden_verifier::Verifier; +pub use miden_verifier::verify; pub use pretty_assertions::{assert_eq, assert_ne, assert_str_eq}; #[cfg(all(feature = "arbitrary", not(target_family = "wasm")))] use proptest::prelude::{Arbitrary, Strategy}; @@ -694,13 +694,13 @@ impl Test { elements[0] += ONE; let stack_outputs = StackOutputs::new(&elements).expect("stack outputs should fit the VM stack"); - assert!( - Verifier::new() - .verify(program_info, stack_inputs, stack_outputs, proof) - .is_err() - ); + let claim = + ExecutionClaim::from_program_info(program_info, stack_inputs, stack_outputs); + assert!(verify(proof, claim).is_err()); } else { - let result = Verifier::new().verify(program_info, stack_inputs, stack_outputs, proof); + let claim = + ExecutionClaim::from_program_info(program_info, stack_inputs, stack_outputs); + let result = verify(proof, claim); assert!(result.is_ok(), "error: {result:?}"); } } diff --git a/crates/test-utils/src/recursive_verifier.rs b/crates/test-utils/src/recursive_verifier.rs index 35325e1c11..08ae0075e1 100644 --- a/crates/test-utils/src/recursive_verifier.rs +++ b/crates/test-utils/src/recursive_verifier.rs @@ -1,407 +1,70 @@ -//! Advice provision for the MASM recursive STARK verifier. +//! Test-side adapter over the production recursive-verifier advice builder +//! (`miden_verifier::recursive`). //! -//! The Rust side parses the proof transcript, then provides the stack, Merkle store, -//! and advice-map entries consumed by `crates/lib/core/asm/stark`. -//! -//! The advice stack ordering must match the MASM consumption order exactly. The kernel digests and -//! stack i/o lead the tape because the test marshalling in `run_recursive_verifier` copies them -//! into caller-owned memory before `verify_proof` runs: -//! -//! kernel_digests -> stack i/o -> -//! security params (nq, query_pow, deep_pow, folding_pow) -> -//! deferred root -> Miden AIR heights -> main commit -> aux commit -> -//! aux finals -> quotient commit -> deep alpha ND -> OOD evals -> -//! DEEP PoW witness -> FRI rounds -> FRI remainder -> query PoW witness -//! -//! The program digest, kernel digest count, and kernel/stack-i/o pointers are supplied on the -//! initial operand stack. See `build_advice` for the authoritative layout. +//! The production builder produces the advice-stack stream, Merkle store, and advice map; the +//! test harness additionally needs the operand-stack pointers for its fixed memory layout and the +//! stream as `u64`s for `build_test!`. This module bundles those into [`VerifierData`] so the +//! recursive-verification tests drive the real MASM verifier over production-built advice. -use alloc::{ - string::{String, ToString}, - vec, - vec::Vec, -}; +use alloc::vec::Vec; -use miden_air::{ - MIDEN_AIR_COUNT, MidenMultiAir, ProofOrder, PublicInputs, Statement, - ace::build_recursive_verifier_ace_circuit, config, -}; -use miden_core::{Felt, Word, field::QuadFelt}; -use miden_crypto::{ - field::BasedVectorSpace, - stark::{ - StarkConfig, VerifierInstance, - lmcs::{Lmcs, proof::BatchProofView}, - pcs::PcsProof, - proof::{StarkProof, StarkProofData}, - verifier::VerifierError as CryptoVerifierError, - }, -}; -use serde_wincode::{SerdeCompat, wincode}; +pub use miden_core::program::request_key; +use miden_core::{Felt, Word, program::ExecutionClaim, proof::ExecutionProof}; +pub use miden_verifier::recursive::RecursiveAdviceError; -use crate::crypto::{MerklePath, MerkleStore, PartialMerkleTree}; - -// TYPES -// ================================================================================================ - -type Challenge = QuadFelt; -type P2Config = config::Poseidon2Config; -type P2Lmcs = >::Lmcs; -const MAX_STARK_PROOF_BYTES: usize = 64 * 1024 * 1024; +use crate::crypto::MerkleStore; +/// The advice inputs plus test operand-stack layout for one recursive verification. +/// +/// `claim_advice` (the consumer's claim: the canonical 40-felt encoding) and `proof_stream` +/// (the proof as the verifier consumes it) are kept separate because they feed different +/// channels: a directly staged run concatenates them on the advice stack; a request-fetched run +/// keeps the claim on the advice stack and registers the proof in the advice map instead. #[derive(Debug, Clone, Eq, PartialEq)] pub struct VerifierData { + /// Operand stack for `verify_vm_proof`: `[claim_ptr]`. pub initial_stack: Vec, - pub advice_stack: Vec, + /// The consumer's claim, copied into VM memory before verification: the canonical 40-felt + /// encoding `P | K | I | O`. + pub claim_advice: Vec, + /// The proof stream consumed by `verify_vm_proof` (production advice-builder + /// output). + pub proof_stream: Vec, pub store: MerkleStore, pub advice_map: Vec<(Word, Vec)>, + /// Commitment to the execution claim (the content address the proof is registered under). + pub claim_commitment: Word, } -#[derive(Debug, thiserror::Error)] -pub enum VerifierError { - #[error("proof deserialization error: {0}")] - ProofDeserializationError(String), - #[error("invalid proof shape: {0}")] - InvalidProofShape(&'static str), - #[error("transcript error: {0}")] - Transcript(#[from] CryptoVerifierError), -} - -/// Merkle store + advice map pair returned by Merkle data construction. -type MerkleAdvice = (MerkleStore, Vec<(Word, Vec)>); - -/// Partial trees + advice map entries returned by single batch proof conversion. -type BatchMerkleResult = (Vec, Vec<(Word, Vec)>); - -struct MidenTraceHeights { - instance_order: [usize; MIDEN_AIR_COUNT], - proof_order: ProofOrder, +impl VerifierData { + /// The full advice stack for a directly staged run: the consumer's claim followed by the + /// proof stream, in consumption order — the prologue copies the claim into memory, then + /// `verify_vm_proof` consumes the proof. + pub fn advice_stack(&self) -> Vec { + [self.claim_advice.as_slice(), self.proof_stream.as_slice()].concat() + } } -// PUBLIC API -// ================================================================================================ +// Caller-owned claim region in the test staging prologue. +const CLAIM_PTR: u64 = 4096; -/// Deserialize a STARK proof and build the advice inputs for the MASM recursive verifier. +/// Builds [`VerifierData`] for a proof of the given claim via the production advice builder. pub fn generate_advice_inputs( - proof_bytes: &[u8], - pub_inputs: PublicInputs, -) -> Result { - let params = config::pcs_params(); - let config = config::poseidon2_config(params, config::RELATION_DIGEST); - - let proof_encoding_config = wincode::config::Configuration::default() - .with_preallocation_size_limit::(); - let proof: StarkProofData = - > as wincode::config::Deserialize< - _, - >>::deserialize(proof_bytes, proof_encoding_config) - .map_err(|e| VerifierError::ProofDeserializationError(e.to_string()))?; - - let (public_values, aux_inputs) = pub_inputs.to_air_inputs(); - let mut challenger = config.challenger(); - config::observe_protocol_params(&mut challenger); - - let statement = - Statement::::new(MidenMultiAir::new(), public_values, aux_inputs) - .map_err(|e| VerifierError::ProofDeserializationError(e.to_string()))?; - let verifier_instance = VerifierInstance::new(&config, &statement, None) - .expect("Miden AIRs declare no preprocessed columns"); - - let (stark, _digest) = StarkProof::from_data(&verifier_instance, &proof, challenger)?; - - let heights = miden_trace_heights(&stark)?; - - let kernel_digests: Vec = pub_inputs.program_info().kernel_procedures().to_vec(); - - build_advice(&config, &stark, heights, pub_inputs, &kernel_digests) -} - -fn miden_trace_heights( - stark: &StarkProof, -) -> Result { - let log_heights = stark.log_trace_heights(); - let Ok(log_heights): Result<[u8; MIDEN_AIR_COUNT], _> = log_heights.try_into() else { - return Err(VerifierError::InvalidProofShape("unexpected number of AIR log heights")); - }; - let instance_order = log_heights.map(usize::from); - - Ok(MidenTraceHeights { - instance_order, - proof_order: ProofOrder::from_instance_log_heights(&log_heights), - }) -} + proof: &ExecutionProof, + claim: &ExecutionClaim, +) -> Result { + let inputs = miden_verifier::recursive::advice_inputs(proof, claim)?; -// ADVICE CONSTRUCTION -// ================================================================================================ - -/// Packs the parsed STARK transcript into the advice inputs consumed by the MASM verifier. -/// -/// The initial operand stack contains caller pointers, the kernel digest count, and the program -/// digest. The advice stack starts with data copied into caller memory by the test prologue, then -/// continues in the order consumed by the verifier. -fn build_advice( - config: &P2Config, - stark: &StarkProof, - heights: MidenTraceHeights, - pub_inputs: PublicInputs, - kernel_digests: &[Word], -) -> Result { - let pcs = &stark.pcs_proof; - if stark.all_aux_values.len() != MIDEN_AIR_COUNT { - return Err(VerifierError::InvalidProofShape("unexpected number of aux-final groups")); - } - - // Caller-owned memory regions consumed by the test marshalling in `run_recursive_verifier`: - // kernel digests at KERNEL_PTR, stack i/o at STACK_IO_PTR. These must match the constants in - // that MASM prologue. - const KERNEL_PTR: u64 = 0; - const STACK_IO_PTR: u64 = 4096; - - let num_kernel_proc_digests = kernel_digests.len(); - let program_digest: Word = *pub_inputs.program_info().program_hash(); - let program_digest = program_digest.as_elements(); - - // `kernel_ptr` is on top. `StackInputs::try_from_ints` puts `vec[0]` on top. - let initial_stack = vec![ - KERNEL_PTR, - num_kernel_proc_digests as u64, - STACK_IO_PTR, - program_digest[0].as_canonical_u64(), - program_digest[1].as_canonical_u64(), - program_digest[2].as_canonical_u64(), - program_digest[3].as_canonical_u64(), - ]; - - let mut advice_stack = Vec::new(); - - // Kernel procedure digests are copied into the caller region at KERNEL_PTR. - let kernel_advice = build_kernel_digest_advice(kernel_digests); - advice_stack.extend_from_slice(&kernel_advice); - - // Stack i/o is copied into the caller region at STACK_IO_PTR. - advice_stack.extend_from_slice(&build_stack_io_advice(&pub_inputs)); - - // Security parameters: [num_queries, query_pow_bits, deep_pow_bits, folding_pow_bits]. - let params = config::pcs_params(); - let num_queries = params.num_queries(); - advice_stack.push(num_queries as u64); - advice_stack.push(params.query_pow_bits() as u64); - // DEEP and folding PoW bits are not publicly exposed on PcsParams; - // use the constants from air/src/config.rs directly. - advice_stack.push(config::DEEP_POW_BITS as u64); - advice_stack.push(config::FOLDING_POW_BITS as u64); - - // Final deferred root, loaded by `public_inputs::stage_reduced_inputs`. - advice_stack.extend(pub_inputs.deferred_root().as_ref().iter().map(Felt::as_canonical_u64)); - - for height in heights.instance_order { - advice_stack.push(height as u64); - } - - advice_stack.extend_from_slice(&commitment_to_u64s(stark.main_commit)); - advice_stack.extend_from_slice(&commitment_to_u64s(stark.aux_commit)); - - // Normalized LogUp sums (`sigma_prime`), one per AIR in proof order. The recursive verifier - // scales each value by the matching trace length for the outer boundary check. - for aux_values in &stark.all_aux_values { - advice_stack.extend_from_slice(&challenges_to_u64s(aux_values)); - } - - advice_stack.extend_from_slice(&commitment_to_u64s(stark.quotient_commit)); - - let deep_alpha = pcs.deep_proof.challenge_columns; - let deep_coeffs: &[Felt] = deep_alpha.as_basis_coefficients_slice(); - advice_stack - .extend_from_slice(&[deep_coeffs[1].as_canonical_u64(), deep_coeffs[0].as_canonical_u64()]); - - append_ood_evaluations(&mut advice_stack, pcs); - - advice_stack.push(pcs.deep_proof.pow_witness.as_canonical_u64()); - - for round in &pcs.fri_proof.rounds { - advice_stack.extend_from_slice(&commitment_to_u64s(round.commitment)); - advice_stack.push(round.pow_witness.as_canonical_u64()); - } - - let final_poly = &pcs.fri_proof.final_poly; - let remainder_base: Vec = QuadFelt::flatten_to_base(final_poly.to_vec()); - let remainder_u64s: Vec = remainder_base.iter().map(Felt::as_canonical_u64).collect(); - advice_stack.extend_from_slice(&remainder_u64s); - - advice_stack.push(pcs.query_pow_witness.as_canonical_u64()); - - let (store, advice_map) = build_merkle_data(config, stark, &heights.proof_order)?; + // The consumer's claim: the canonical 40-felt encoding. In a real protocol consumer these + // fields are derived/held; here the test supplies the proof's own claim. + let claim_advice: Vec = claim.to_elements().iter().map(Felt::as_canonical_u64).collect(); Ok(VerifierData { - initial_stack, - advice_stack, - store, - advice_map, + initial_stack: alloc::vec![CLAIM_PTR], + claim_advice, + proof_stream: inputs.advice_stack.iter().map(Felt::as_canonical_u64).collect(), + store: inputs.store, + advice_map: inputs.advice_map, + claim_commitment: inputs.claim_commitment, }) } - -// OOD EVALUATIONS -// ================================================================================================ - -/// Flatten OOD evaluations into the advice stack. -/// -/// The DEEP transcript contains evaluations at two points (z and z*g) for each committed -/// matrix (main, aux, quotient). We split them into local (at z) and next (at z*g) rows, -/// then append local followed by next. -fn append_ood_evaluations(advice_stack: &mut Vec, pcs: &PcsProof) -where - L: Lmcs, -{ - let evals = &pcs.deep_proof.evals; - let mut local_values = Vec::new(); - let mut next_values = Vec::new(); - - for group in evals { - for matrix in group { - let width = matrix.width; - let values = matrix.values.as_slice(); - let local_row = &values[..width]; - let next_row = if values.len() > width { - &values[width..2 * width] - } else { - &[] - }; - local_values.extend_from_slice(local_row); - next_values.extend_from_slice(next_row); - } - } - - advice_stack.extend_from_slice(&challenges_to_u64s(&local_values)); - advice_stack.extend_from_slice(&challenges_to_u64s(&next_values)); -} - -// MERKLE DATA -// ================================================================================================ - -/// Build Merkle store and advice map from the DEEP and FRI opening proofs. -/// -/// Each opening proof is converted into a `PartialMerkleTree` (for the Merkle store) -/// and leaf-hash -> leaf-data entries (for the advice map). The MASM verifier uses -/// `mtree_get` to fetch authentication paths and `adv_keyval` to retrieve leaf data. -fn build_merkle_data( - config: &P2Config, - stark: &StarkProof, - proof_order: &ProofOrder, -) -> Result { - let pcs = &stark.pcs_proof; - let lmcs = config.lmcs(); - - let mut partial_trees = Vec::new(); - let mut advice_map = Vec::new(); - - // DEEP openings -- one BatchProof per commitment (main, aux, quotient). - for batch_proof in pcs.deep_witnesses.iter() { - let (trees, advs) = batch_proof_to_merkle(lmcs, batch_proof)?; - partial_trees.extend(trees); - advice_map.extend(advs); - } - - // FRI openings -- one BatchProof per FRI round. - for batch_proof in pcs.fri_witnesses.iter() { - let (trees, advs) = batch_proof_to_merkle(lmcs, batch_proof)?; - partial_trees.extend(trees); - advice_map.extend(advs); - } - - let mut store = MerkleStore::new(); - for tree in &partial_trees { - store.extend(tree.inner_nodes()); - } - extend_ace_registry_store(&mut store); - extend_ace_circuit_advice(&mut advice_map, proof_order)?; - - Ok((store, advice_map)) -} - -fn extend_ace_registry_store(store: &mut MerkleStore) { - let registry_tree = config::ace_circuit_registry_tree(); - store.extend(registry_tree.inner_nodes()); -} - -fn extend_ace_circuit_advice( - advice_map: &mut Vec<(Word, Vec)>, - proof_order: &ProofOrder, -) -> Result<(), VerifierError> { - let circuit = build_recursive_verifier_ace_circuit(proof_order) - .map_err(|_| VerifierError::InvalidProofShape("failed to build recursive ACE circuit"))?; - advice_map.push((circuit.commitment, circuit.instructions)); - Ok(()) -} - -/// Convert a `BatchProof` into `PartialMerkleTree` entries and advice map entries. -/// -/// For each query index, reconstructs the Merkle authentication path from the batch proof, -/// computes the leaf hash, and produces: -/// - A `(index, leaf_hash, path)` triple for the partial Merkle tree -/// - A `(leaf_hash, leaf_data)` pair for the advice map -fn batch_proof_to_merkle( - lmcs: &L, - batch_proof: &L::BatchProof, -) -> Result -where - L: Lmcs, - L::Commitment: Copy + Into<[Felt; 4]>, - L::BatchProof: BatchProofView, - L::Commitment: PartialEq, -{ - let mut paths = Vec::new(); - let mut advice_entries = Vec::new(); - - for index in batch_proof.indices() { - let rows = batch_proof - .opening(index) - .ok_or(VerifierError::InvalidProofShape("missing opening for query index"))?; - let siblings = batch_proof - .path(index) - .ok_or(VerifierError::InvalidProofShape("missing Merkle path for query index"))?; - - let leaf_data: Vec = rows.as_slice().to_vec(); - let leaf_hash = lmcs.hash(rows.iter_rows()); - let leaf_word: Word = Word::new(leaf_hash.into()); - let merkle_path = - MerklePath::new(siblings.into_iter().map(|c| Word::new(c.into())).collect()); - - paths.push((index as u64, leaf_word, merkle_path)); - advice_entries.push((leaf_word, leaf_data)); - } - - let tree = PartialMerkleTree::with_paths(paths) - .map_err(|_| VerifierError::InvalidProofShape("invalid merkle paths"))?; - - Ok((vec![tree], advice_entries)) -} - -/// Build kernel digest advice data: 4 canonical felts per digest, in order. The test marshalling -/// copies these felts into the caller-owned kernel region at KERNEL_PTR, which `verify_proof` -/// hashes with `hash_elements` to recompute the kernel commitment. -fn build_kernel_digest_advice(kernel_digests: &[Word]) -> Vec { - let mut result = Vec::with_capacity(kernel_digests.len() * 4); - for digest in kernel_digests { - result.extend(digest.as_elements().iter().map(Felt::as_canonical_u64)); - } - result -} - -/// Build the fixed-length public inputs (stack i/o): stack inputs (16), stack outputs (16). The -/// test marshalling copies these 32 felts into the caller-owned region at STACK_IO_PTR. -fn build_stack_io_advice(pub_inputs: &PublicInputs) -> Vec { - let mut felts = Vec::::new(); - felts.extend_from_slice(pub_inputs.stack_inputs().as_ref()); - felts.extend_from_slice(pub_inputs.stack_outputs().as_ref()); - felts.iter().map(Felt::as_canonical_u64).collect() -} - -fn commitment_to_u64s>(commitment: C) -> Vec { - let felts: [Felt; 4] = commitment.into(); - felts.iter().map(Felt::as_canonical_u64).collect() -} - -fn challenges_to_u64s(challenges: &[Challenge]) -> Vec { - let base: Vec = QuadFelt::flatten_to_base(challenges.to_vec()); - base.iter().map(Felt::as_canonical_u64).collect() -} diff --git a/miden-vm/Cargo.toml b/miden-vm/Cargo.toml index 6c9b506278..a6ebdc12d1 100644 --- a/miden-vm/Cargo.toml +++ b/miden-vm/Cargo.toml @@ -97,7 +97,6 @@ tracing-forest = { workspace = true, optional = true, features = ["ansi", "small assert_cmd = { version = "2.1" } criterion = { workspace = true, features = ["async_tokio"] } miden-assembly = { workspace = true, features = ["testing"] } -miden-precompiles.workspace = true miden-processor = { workspace = true, features = ["testing"] } miden-test-serde-macros.workspace = true miden-utils-testing.workspace = true diff --git a/miden-vm/README.md b/miden-vm/README.md index 4bf00d58f5..59a9370b76 100644 --- a/miden-vm/README.md +++ b/miden-vm/README.md @@ -142,10 +142,8 @@ assert_eq!(8, outputs.first().unwrap().as_canonical_u64()); To verify program execution, use `Verifier::new().verify(...)`. The verifier takes the following parameters: -- `program_info: ProgramInfo` - a structure containing the hash of the program to be verified (represented as a 32-byte digest), and the hashes of the Kernel procedures used to execute the program. -- `stack_inputs: StackInputs` - a list of the values with which the stack was initialized prior to the program's execution.. -- `stack_outputs: StackOutputs` - a list of the values returned from the stack after the program completed execution. - `proof: ExecutionProof` - the proof generated during program execution. +- `claim: ExecutionClaim` - the claimed program information, stack inputs, and stack outputs. Stack inputs are expected to be ordered as if they would be pushed onto the stack one by one. Thus, their expected order on the stack will be the reverse of the order in which they are provided, and the last value in the `stack_inputs` is expected to be the value at the top of the stack. @@ -162,16 +160,21 @@ Notice how the verifier needs to know only the hash of the program - not what th Here is a simple example of verifying execution of the program from the previous example: ```rust,ignore -use miden_vm::{field::Felt, ProgramInfo, StackInputs, StackOutputs, Verifier}; +use miden_vm::{ExecutionClaim, ProgramInfo, StackInputs, StackOutputs, Verifier, field::Felt}; let program = /* value from previous example */; let proof = /* value from previous example */; let expected_outputs = StackOutputs::new(&[Felt::new(8).unwrap()]).unwrap(); +let claim = ExecutionClaim::from_program_info( + ProgramInfo::from(program), + StackInputs::default(), + expected_outputs, +); -// let's verify program execution -match Verifier::new().verify(ProgramInfo::from(program), StackInputs::default(), expected_outputs, proof) { +// Verify the execution claim. +match Verifier::new().verify(proof, claim) { Ok(_) => println!("Execution verified!"), - Err(msg) => println!("Something went terribly wrong: {}", msg), + Err(err) => eprintln!("Verification failed: {err}"), } ``` diff --git a/miden-vm/src/cli/verify.rs b/miden-vm/src/cli/verify.rs index c9c402f038..85d6133b2a 100644 --- a/miden-vm/src/cli/verify.rs +++ b/miden-vm/src/cli/verify.rs @@ -75,8 +75,9 @@ impl VerifyCmd { // verify proof let stack_outputs = outputs_data.stack_outputs().map_err(Report::msg)?; - miden_vm::Verifier::new() - .verify(program_info, stack_inputs, stack_outputs, proof) + let claim = + miden_vm::ExecutionClaim::from_program_info(program_info, stack_inputs, stack_outputs); + miden_vm::verify(proof, claim) .into_diagnostic() .wrap_err("Program failed verification!")?; diff --git a/miden-vm/src/lib.rs b/miden-vm/src/lib.rs index 853b8876ad..14de04b46e 100644 --- a/miden-vm/src/lib.rs +++ b/miden-vm/src/lib.rs @@ -9,7 +9,10 @@ pub use miden_assembly::{ ast::{Module, ModuleKind}, diagnostics, }; -pub use miden_core::proof::{DeferredProof, ExecutionProof, HashFunction, StarkProof}; +pub use miden_core::{ + program::ExecutionClaim, + proof::{DeferredProof, ExecutionProof, HashFunction, StarkProof}, +}; #[cfg(not(target_family = "wasm"))] pub use miden_processor::execute_sync; pub use miden_processor::{ @@ -21,7 +24,7 @@ pub use miden_processor::{ pub use miden_prover::{InputError, ProvingOptions, StackOutputs, TraceProvingInputs, Word, prove}; #[cfg(not(target_family = "wasm"))] pub use miden_prover::{prove_from_trace_sync, prove_sync}; -pub use miden_verifier::{VerificationError, Verifier}; +pub use miden_verifier::{Unsettled, VerificationError, Verifier}; // (private) exports // ================================================================================================ @@ -29,18 +32,10 @@ pub use miden_verifier::{VerificationError, Verifier}; #[cfg(feature = "internal")] pub mod internal; -/// Verifies a final Miden proof. -/// -/// Wire-backed deferred proofs are partial/delegable proof material and are rejected by this -/// verifier. Use [`Verifier::verify_partial`] to verify and hydrate wire-backed partial proofs. +/// Verifies a final Miden proof of the given execution claim. /// -/// Deprecated compatibility shim for [`Verifier::verify`]. -#[deprecated(since = "0.25.0", note = "use Verifier::new().verify(...) instead")] -pub fn verify( - program_info: ProgramInfo, - stack_inputs: StackInputs, - stack_outputs: StackOutputs, - proof: ExecutionProof, -) -> Result { - 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 { + miden_verifier::verify(proof, claim) } diff --git a/miden-vm/tests/integration/prove_verify.rs b/miden-vm/tests/integration/prove_verify.rs index ba969881c3..54e3ef4cd3 100644 --- a/miden-vm/tests/integration/prove_verify.rs +++ b/miden-vm/tests/integration/prove_verify.rs @@ -2,31 +2,21 @@ use alloc::sync::Arc; -use miden_assembly::{Assembler, DefaultSourceManager, Linkage}; +use miden_assembly::{Assembler, DefaultSourceManager}; use miden_core::{ - Felt, - deferred::{DeferredState, TRUE_DIGEST}, - proof::{DeferredProof, ExecutionProof}, - utils::bytes_to_packed_u32_elements, + program::ExecutionClaim, + proof::{DeferredProof, ExecutionProof, StarkProof}, }; use miden_core_lib::CoreLibrary; use miden_processor::ExecutionOptions; use miden_prover::{ - AdviceInputs, ProgramInfo, ProvingOptions, PublicInputs, StackInputs, StackOutputs, prove_sync, + AdviceInputs, ProgramInfo, ProvingOptions, StackInputs, StackOutputs, prove_partial_sync, + prove_sync, }; use miden_utils_testing::{recursive_verifier::generate_advice_inputs, stack_inputs_from_ints}; -use miden_verifier::Verifier; +use miden_verifier::{VerificationError, Verifier, verify}; use miden_vm::{DefaultHost, HashFunction}; -fn masm_push_felts(felts: &[Felt]) -> String { - felts - .iter() - .rev() - .map(|felt| format!("push.{}", felt.as_canonical_u64())) - .collect::>() - .join(" ") -} - fn assert_prove_verify( source: &str, hash_fn: HashFunction, @@ -60,16 +50,13 @@ fn assert_prove_verify( println!("Stack outputs: {stack_outputs:?}"); } - let proof = if verify_recursively { - assert_recursive_verify(program.to_info(), stack_inputs, stack_outputs, proof) - } else { - proof - }; + if verify_recursively { + assert_recursive_verify(program.to_info(), stack_inputs, stack_outputs, &proof); + } println!("Verifying proof..."); - let security_level = Verifier::new() - .verify(program.into(), stack_inputs, stack_outputs, proof) - .expect("Verification failed"); + let claim = ExecutionClaim::from_program_info(program.into(), stack_inputs, stack_outputs); + let security_level = verify(proof, claim).expect("Verification failed"); println!("Verification successful! Security level: {security_level}"); } @@ -78,29 +65,14 @@ fn assert_recursive_verify( program_info: ProgramInfo, stack_inputs: StackInputs, stack_outputs: StackOutputs, - proof: ExecutionProof, -) -> ExecutionProof { - let stark_proof = proof.miden_proof(); - let deferred_proof = proof.deferred_proof(); - assert_eq!(stark_proof.hash_fn(), HashFunction::Poseidon2); - - let final_deferred_root = match deferred_proof { - DeferredProof::Empty => TRUE_DIGEST, - DeferredProof::Wire(wire) => { - DeferredState::from_wire(Arc::new(miden_precompiles::registry()), wire, usize::MAX) - .expect("deferred wire should rehydrate under official precompiles") - .root() - }, - DeferredProof::Stark { .. } => { - panic!("recursive verifier does not support deferred STARK proofs") - }, - }; - let pub_inputs = - PublicInputs::new(program_info, stack_inputs, stack_outputs, final_deferred_root); - let verifier_inputs = generate_advice_inputs(stark_proof.bytes(), pub_inputs) + proof: &ExecutionProof, +) { + let claim = ExecutionClaim::from_program_info(program_info, stack_inputs, stack_outputs); + let verifier_inputs = generate_advice_inputs(proof, &claim) .expect("recursive verifier advice construction failed"); let source = " + use miden::core::sys use miden::core::sys::vm # Copy `count` felts (a multiple of 4) from the advice tape into memory starting at `dst`. @@ -124,76 +96,28 @@ fn assert_recursive_verify( end begin - # Initial stack: [kernel_ptr, num_kernel_digests, stack_io_ptr, PROG0..3]. + # Initial stack: [claim_ptr]. - # Copy kernel digests (4·num_kernel_digests felts) from advice into the caller region - # (kernel_ptr = 0). Build [dst=0, count=4N]. - dup.1 mul.4 push.0 + # Copy the claim encoding P | K | I | O (40 felts) into the claim region + # (claim_ptr = 4096); the kernel digest witness travels in the advice map. + push.40 push.4096 exec.copy_advice_to_mem - # Copy stack i/o (32 felts) from advice into the caller region (stack_io_ptr = 4096). - # Build [dst=4096, count=32]. - push.32 push.4096 - exec.copy_advice_to_mem - - exec.vm::verify_proof + exec.vm::verify_vm_proof + # => [D, num_queries, query_pow_bits, deep_pow_bits, folding_pow_bits] + exec.sys::truncate_stack end "; let mut test = crate::build_test!( source, &verifier_inputs.initial_stack, - &verifier_inputs.advice_stack, + &verifier_inputs.advice_stack(), verifier_inputs.store, verifier_inputs.advice_map ); test.libraries.push(CoreLibrary::default().package()); test.execute().expect("recursive verifier execution failed"); - - proof -} - -#[test] -fn test_keccak_precompile_wrapper_prove_verify_final() { - let core_lib = CoreLibrary::default(); - let input: Vec = (0u8..32).collect(); - let input = masm_push_felts(&bytes_to_packed_u32_elements(&input)); - let source = format!( - " - begin - {input} - exec.::miden::core::crypto::hashes::keccak256::hash - dropw dropw - end - " - ); - let program = Assembler::default() - .with_package(core_lib.package(), Linkage::Dynamic) - .expect("failed to link core library") - .assemble_program("keccak_precompile_wrapper_test", &source) - .expect("failed to assemble Keccak precompile wrapper test") - .unwrap_program(); - let stack_inputs = StackInputs::default(); - let advice_inputs = AdviceInputs::default(); - let mut host = DefaultHost::default() - .with_library(&core_lib) - .expect("failed to load CoreLibrary into the host"); - - let (stack_outputs, proof) = prove_sync( - &program, - stack_inputs, - advice_inputs, - &mut host, - ExecutionOptions::default(), - ProvingOptions::with_96_bit_security(HashFunction::Blake3_256), - ) - .expect("Keccak precompile wrapper should prove"); - - assert!(proof.is_final()); - assert!(matches!(proof.deferred_proof(), DeferredProof::Stark { .. })); - Verifier::new() - .verify(program.into(), stack_inputs, stack_outputs, proof) - .expect("Verification failed"); } #[test] @@ -334,7 +258,10 @@ mod fast_parallel { use alloc::sync::Arc; use miden_assembly::{Assembler, DefaultSourceManager}; - use miden_core::proof::{DeferredProof, ExecutionProof, HashFunction}; + use miden_core::{ + program::ExecutionClaim, + proof::{DeferredProof, ExecutionProof, HashFunction}, + }; use miden_processor::{ DefaultHost, ExecutionOptions, FastProcessor, StackInputs, advice::AdviceInputs, trace::build_trace, @@ -343,7 +270,7 @@ mod fast_parallel { ProvingOptions, TraceProvingInputs, config, prove_from_trace_sync, prove_partial_from_trace_sync, prove_stark, }; - use miden_verifier::{VerificationError, Verifier}; + use miden_verifier::verify; use miden_vm::{Program, TraceBuildInputs}; /// Default fragment size for parallel trace generation @@ -422,15 +349,18 @@ mod fast_parallel { ) .expect("Proving failed"); + // The fixture is deferred-free, so the final proof carries empty deferred material. assert_eq!(trace.deferred_state().root(), miden_core::deferred::TRUE_DIGEST); - - let proof = - ExecutionProof::from_parts(proof_bytes, HashFunction::Blake3_256, DeferredProof::Empty); + let proof = ExecutionProof::from_parts( + proof_bytes, + HashFunction::Blake3_256, + DeferredProof::empty(), + ); // Verify the proof - Verifier::new() - .verify(program.into(), stack_inputs, fast_stack_outputs, proof) - .expect("Verification failed"); + let claim = + ExecutionClaim::from_program_info(program.into(), stack_inputs, fast_stack_outputs); + verify(proof, claim).expect("Verification failed"); } #[test] @@ -459,15 +389,12 @@ mod fast_parallel { )) .expect("prove_from_trace_sync failed"); - assert!(proof.is_final()); - assert_eq!(proof.deferred_proof(), &DeferredProof::Empty); - Verifier::new() - .verify(program.into(), stack_inputs, stack_outputs, proof) - .expect("Verification failed"); + let claim = ExecutionClaim::from_program_info(program.into(), stack_inputs, stack_outputs); + verify(proof, claim).expect("Verification failed"); } #[test] - fn test_prove_partial_from_trace_sync_preserves_deferred_wire() { + fn test_prove_from_trace_sync_preserves_deferred_wire() { let source = "begin log_deferred end"; let program = Assembler::default() .assemble_program("program", source) @@ -478,7 +405,6 @@ mod fast_parallel { let mut host = default_source_manager_host(); let trace_inputs = execute_parallel_trace_inputs(&program, stack_inputs, advice_inputs, &mut host); - let expected_deferred_root = trace_inputs.deferred_state().root(); let expected_wire = trace_inputs .deferred_state() .to_wire() @@ -494,25 +420,133 @@ mod fast_parallel { )) .expect("prove_partial_from_trace_sync failed"); - assert!(!proof.is_final()); - assert_eq!(proof.deferred_proof(), &DeferredProof::Wire(expected_wire.clone())); + assert_eq!(proof.deferred_proof().as_wire(), Some(&expected_wire)); + let claim = ExecutionClaim::from_program_info(program.into(), stack_inputs, stack_outputs); + let (_, pending) = miden_verifier::Verifier::new() + .verify_partial(proof, claim) + .expect("partial verification failed"); + assert_ne!(pending.root(), miden_core::deferred::TRUE_DIGEST); + let _state = pending.into_state(); + } +} - let err = Verifier::new() - .verify(program.to_info(), stack_inputs, stack_outputs, proof.clone()) - .unwrap_err(); - assert!( - matches!(err, VerificationError::UnsupportedDeferredProof), - "wire-backed partial proofs should be rejected by final verification, got {err:?}" - ); +/// Proves a trivial program and returns the claim/proof pair for API-surface tests. +fn prove_fixture() -> (ExecutionClaim, ExecutionProof) { + let program = Assembler::default() + .assemble_program("program", "begin push.1 push.2 add swap drop end") + .unwrap() + .unwrap_program(); + let stack_inputs = stack_inputs_from_ints([0, 1]); + let mut host = + DefaultHost::default().with_source_manager(Arc::new(DefaultSourceManager::default())); + let (stack_outputs, proof) = prove_sync( + &program, + stack_inputs, + AdviceInputs::default(), + &mut host, + ExecutionOptions::default(), + ProvingOptions::with_96_bit_security(HashFunction::Blake3_256), + ) + .expect("Proving failed"); + ( + ExecutionClaim::from_program_info(program.into(), stack_inputs, stack_outputs), + proof, + ) +} - let (security_level, hydrated_state) = Verifier::new() - .verify_partial(program.to_info(), stack_inputs, stack_outputs, proof) - .expect("wire-backed partial proof should verify and hydrate deferred state"); - assert_eq!(security_level, 96); - assert_eq!(hydrated_state.root(), expected_deferred_root); - assert_eq!( - hydrated_state.to_wire().expect("hydrated state should serialize to wire"), - expected_wire - ); - } +/// Like [`prove_fixture`], but produces a wire-backed partial proof via `prove_partial_sync`. +fn prove_partial_fixture() -> (ExecutionClaim, ExecutionProof) { + let program = Assembler::default() + .assemble_program("program", "begin push.1 push.2 add swap drop end") + .unwrap() + .unwrap_program(); + let stack_inputs = stack_inputs_from_ints([0, 1]); + let mut host = + DefaultHost::default().with_source_manager(Arc::new(DefaultSourceManager::default())); + let (stack_outputs, proof) = prove_partial_sync( + &program, + stack_inputs, + AdviceInputs::default(), + &mut host, + ExecutionOptions::default(), + ProvingOptions::with_96_bit_security(HashFunction::Blake3_256), + ) + .expect("Proving failed"); + ( + ExecutionClaim::from_program_info(program.into(), stack_inputs, stack_outputs), + proof, + ) +} + +/// `verify` accepts the prover's final packages and refuses wire-backed partial material; a +/// partial package verifies through `Verifier::verify_partial`, which hydrates the wire and +/// returns the obligation. +#[test] +fn test_partial_obligation_flow() { + // the default prover emits final deferred material: `verify` accepts it directly + let (claim, proof) = prove_fixture(); + verify(proof, claim).expect("final verification should pass"); + + // a partial (wire-backed) package is refused by final verification... + let (claim, partial) = prove_partial_fixture(); + assert!(matches!( + verify(partial.clone(), claim.clone()), + Err(VerificationError::UnsupportedDeferredProof) + )); + + // ...and verified by the partial path, which returns the linear obligation + let (_, pending) = Verifier::new() + .verify_partial(partial, claim) + .expect("partial verification should pass"); + assert_eq!(pending.root(), miden_core::deferred::TRUE_DIGEST); + let _state = pending.into_state(); +} + +/// A STARK-backed deferred proof must be exactly encoded and match the root bound by the outer VM +/// proof. +#[test] +fn test_deferred_stark_proof_requires_exact_encoding_and_bound_root() { + // a program with a deferred request binds a non-TRUE deferred root into its statement + let source = " + begin + log_deferred + dropw dropw dropw + end + "; + let program = Assembler::default() + .assemble_program("program", source) + .unwrap() + .unwrap_program(); + let stack_inputs = stack_inputs_from_ints([0, 1]); + let mut host = + DefaultHost::default().with_source_manager(Arc::new(DefaultSourceManager::default())); + let (stack_outputs, proof) = prove_sync( + &program, + stack_inputs, + AdviceInputs::default(), + &mut host, + ExecutionOptions::default(), + ProvingOptions::with_96_bit_security(HashFunction::Poseidon2), + ) + .expect("Proving failed"); + let claim = ExecutionClaim::from_program_info(program.into(), stack_inputs, stack_outputs); + + verify(proof.clone(), claim.clone()).expect("untampered deferred proof should verify"); + + // The proof encoding is exact: an otherwise-valid proof with a trailing byte is rejected. + let stark = proof.miden_proof(); + let mut proof_bytes = stark.bytes().to_vec(); + proof_bytes.push(0); + let trailing = ExecutionProof::new( + StarkProof::new(proof_bytes, stark.hash_fn()), + proof.deferred_proof().clone(), + ); + verify(trailing, claim.clone()).expect_err("trailing proof bytes must be rejected"); + + // The deferred root is statement-bound: replacing it with TRUE must fail. + let tampered = ExecutionProof::new( + StarkProof::new(stark.bytes().to_vec(), stark.hash_fn()), + DeferredProof::empty(), + ); + assert!(verify(tampered, claim).is_err()); } diff --git a/precompiles-prover/src/session/prove.rs b/precompiles-prover/src/session/prove.rs index f072093936..347855b7e1 100644 --- a/precompiles-prover/src/session/prove.rs +++ b/precompiles-prover/src/session/prove.rs @@ -28,11 +28,26 @@ use miden_lifted_stark::{ }; use serde::{Serialize, de::DeserializeOwned}; use serde_wincode::SerdeCompat; +use wincode::io::Reader as _; use super::preprocessed_cache; const MAX_STARK_PROOF_BYTES: usize = 64 * 1024 * 1024; +/// Deserializes a serde-backed value and rejects trailing bytes. +fn deserialize_serde_exact<'de, T, C>(mut bytes: &'de [u8], _: C) -> wincode::ReadResult +where + C: wincode::config::Config, + SerdeCompat: wincode::SchemaRead<'de, C, Dst = T>, +{ + let value = as wincode::SchemaRead<'de, C>>::get(bytes.by_ref())?; + if bytes.is_empty() { + Ok(value) + } else { + Err(wincode::error::trailing_bytes()) + } +} + use crate::{ ProveError, ec::{EcPointStoreAir, add::EcGroupAddAir, groups::EcGroupsAir, msm::EcMsmAir}, @@ -343,7 +358,7 @@ impl SessionTraces { .expect("chiplet trace shapes are valid"); let mut challenger = config.challenger(); - observe_protocol_params(&mut challenger); + observe_protocol_params(config.pcs(), &mut challenger); let output: StarkOutput = ProverInstance::new(config, &prover_statement, Some(preprocessed))? @@ -426,10 +441,9 @@ where let proof_encoding_config = wincode::config::Configuration::default() .with_preallocation_size_limit::(); - let proof: StarkProofData = , - > as wincode::config::Deserialize<_>>::deserialize( - proof_bytes, proof_encoding_config + let proof = deserialize_serde_exact::, _>( + proof_bytes, + proof_encoding_config, )?; let statement = @@ -437,7 +451,7 @@ where .expect("chiplet statement inputs are valid"); let mut challenger = config.challenger(); - observe_protocol_params(&mut challenger); + observe_protocol_params(config.pcs(), &mut challenger); VerifierInstance::new(config, &statement, Some(preprocessed.commitment()))? .verify(&proof, challenger)?; diff --git a/precompiles-prover/src/stark_config.rs b/precompiles-prover/src/stark_config.rs index dbbb9a06f1..1f06160bf5 100644 --- a/precompiles-prover/src/stark_config.rs +++ b/precompiles-prover/src/stark_config.rs @@ -81,7 +81,7 @@ pub fn precompile_pcs_params() -> PcsParams { 4, // folding_pow_bits 12, // deep_pow_bits 27, // num_queries - 16, // query_pow_bits + 17, // query_pow_bits ) .expect("invalid precompile PCS parameters") } diff --git a/precompiles-prover/src/tests/deferred_state.rs b/precompiles-prover/src/tests/deferred_state.rs index d632110c52..33ffa2a6aa 100644 --- a/precompiles-prover/src/tests/deferred_state.rs +++ b/precompiles-prover/src/tests/deferred_state.rs @@ -7,7 +7,7 @@ use miden_core::{ DeferredState, DeferredStateWire, Digest, Node as VmNode, PrecompileRegistry, TRUE_DIGEST as VM_TRUE_DIGEST, TRUE_INDEX, Tag, WireEntry, }, - proof::{DeferredProof, HashFunction}, + proof::{DeferredProof, HashFunction, StarkProof}, }; use miden_precompiles::{ CurveId, CurvePrecompile, Keccak256Precompile, UintDomain, UintPrecompile, @@ -18,7 +18,7 @@ use crate::{ hash::keccak::sponge::trace::keccak_oracle, math::{U256, from_hex, to_limbs32}, prove_deferred_state, - session::{Session, SessionTraces, verify_deferred}, + session::{Session, SessionTraces, VerifyError, verify_deferred}, transcript::poseidon2::P2Digest, }; @@ -407,7 +407,7 @@ fn trailing_zero_input_changes_root() { } #[test] -fn keccak_deferred_state_root_proves_and_verifies() { +fn keccak_deferred_state_proof_verifies_and_rejects_trailing_bytes() { let input = b"abc"; let synthetic = synthetic_keccak_state(input); let DeferredSession { session, root } = session_from_deferred_state(&synthetic.state).unwrap(); @@ -416,11 +416,21 @@ fn keccak_deferred_state_root_proves_and_verifies() { assert_eq!(traces.public_root(), synthetic.root); let proof = traces.prove(); - let Some((_, public_root)) = proof.as_stark() else { + let Some((stark, public_root)) = proof.as_stark() else { panic!("precompile session should produce a deferred STARK proof"); }; assert_eq!(P2Digest::from(public_root), synthetic.root); verify_deferred(&proof).expect("Keccak deferred-state proof should verify"); + + // The proof encoding is exact: an otherwise-valid proof with a trailing byte is rejected. + let mut proof_bytes = stark.bytes().to_vec(); + proof_bytes.push(0); + let trailing = DeferredProof::stark(StarkProof::new(proof_bytes, stark.hash_fn()), public_root); + let err = verify_deferred(&trailing).expect_err("trailing proof bytes must be rejected"); + assert!(matches!( + err, + VerifyError::Deserialization(wincode::error::ReadError::TrailingBytes) + )); } #[test] diff --git a/precompiles/benches/precompiles_bench/support.rs b/precompiles/benches/precompiles_bench/support.rs index fbdf117469..9b6223633f 100644 --- a/precompiles/benches/precompiles_bench/support.rs +++ b/precompiles/benches/precompiles_bench/support.rs @@ -107,7 +107,12 @@ pub fn verify_once( stack_outputs: StackOutputs, proof: ExecutionProof, ) { + let claim = miden_vm::ExecutionClaim::from_program_info( + fixture.program.to_info(), + fixture.stack_inputs, + stack_outputs, + ); Verifier::new() - .verify(fixture.program.to_info(), fixture.stack_inputs, stack_outputs, proof) + .verify(proof, claim) .expect("failed to verify precompile benchmark proof"); } diff --git a/prover/src/lib.rs b/prover/src/lib.rs index 536c8fb34a..7c89786f4a 100644 --- a/prover/src/lib.rs +++ b/prover/src/lib.rs @@ -366,7 +366,7 @@ where ::Commitment: Serialize, { let mut challenger = config.challenger(); - config::observe_protocol_params(&mut challenger); + config::observe_protocol_params(config.pcs(), &mut challenger); // `air_inputs` are the public values read by the AIRs (stack i/o); `aux_inputs` are the // statement inputs read during observation/boundary correction. diff --git a/verifier/src/lib.rs b/verifier/src/lib.rs index 8f792816a4..b063ccb57d 100644 --- a/verifier/src/lib.rs +++ b/verifier/src/lib.rs @@ -18,16 +18,32 @@ use miden_crypto::stark::{ }; use serde::de::DeserializeOwned; use serde_wincode::{SerdeCompat, wincode}; +use wincode::io::Reader as _; +/// Maximum encoded STARK proof size and per-sequence preallocation. const MAX_STARK_PROOF_BYTES: usize = 64 * 1024 * 1024; +/// Deserializes a serde-backed value and rejects trailing bytes. +fn deserialize_serde_exact<'de, T, C>(mut bytes: &'de [u8], _: C) -> wincode::ReadResult +where + C: wincode::config::Config, + SerdeCompat: wincode::SchemaRead<'de, C, Dst = T>, +{ + let value = as wincode::SchemaRead<'de, C>>::get(bytes.by_ref())?; + if bytes.is_empty() { + Ok(value) + } else { + Err(wincode::error::trailing_bytes()) + } +} + // RE-EXPORTS // ================================================================================================ mod exports { pub use miden_core::{ Word, deferred::{DeferredState, IntegrityError}, - program::{KernelDescriptor, ProgramInfo, StackInputs, StackOutputs}, + program::{ExecutionClaim, KernelDescriptor, ProgramInfo, StackInputs, StackOutputs}, proof::{DeferredProof, ExecutionProof, HashFunction, StarkProof}, }; pub mod math { @@ -36,6 +52,8 @@ mod exports { } pub use exports::*; +pub mod recursive; + // VERIFIER // ================================================================================================ @@ -44,7 +62,7 @@ pub use exports::*; /// [`Verifier::verify`] performs final verification and rejects wire-backed partial proofs. /// [`Verifier::verify_partial`] accepts wire-backed partial proofs, rehydrates their deferred /// state using the standard precompile registry, verifies the Miden VM proof against the hydrated -/// root, and returns the Miden VM security level with the hydrated state. +/// root, and returns the Miden VM security level with the deferred obligation. #[derive(Debug, Clone, Copy, PartialEq, Eq)] pub struct Verifier { max_deferred_elements: usize, @@ -70,49 +88,30 @@ impl Verifier { self } - /// Returns the security level of the final proof if the specified program was executed - /// correctly against the specified inputs and outputs. + /// Returns the security level of the final proof if it proves a correct execution of the + /// given claim. /// /// If the proof contains STARK-backed precompile VM proof material, both the precompile VM /// proof and the Miden VM proof are verified, and the returned security level is the minimum /// of the verified proof security levels. If no precompile claims were produced, only the /// Miden VM proof is verified. /// - /// Stack inputs are expected to be ordered as if they would be pushed onto the stack one by - /// one. Thus, their expected order on the stack will be the reverse of the order in which - /// they are provided, and the last value in the `stack_inputs` slice is expected to be the - /// value at the top of the stack. - /// - /// Stack outputs are expected to be ordered as if they would be popped off the stack one by - /// one. Thus, the value at the top of the stack is expected to be in the first position of - /// the `stack_outputs` slice, and the order of the rest of the output elements will also - /// match the order on the stack. This is the reverse of the order of the `stack_inputs` - /// slice. - /// /// # Errors /// Returns an error if: - /// - The provided proof does not prove a correct execution of the program. + /// - The provided proof does not prove a correct execution of the claim. /// - The proof carries wire-backed deferred proof material, which is a partial/delegable form. /// - The proof's STARK-backed precompile VM proof, if present, does not verify against its /// public root. pub fn verify( &self, - program_info: ProgramInfo, - stack_inputs: StackInputs, - stack_outputs: StackOutputs, proof: ExecutionProof, + claim: ExecutionClaim, ) -> Result { let miden_security_level = proof.security_level(); let (final_deferred_root, precompile_security_level) = resolve_final_deferred_root(proof.deferred_proof())?; - verify_stark( - program_info, - stack_inputs, - stack_outputs, - final_deferred_root, - proof.miden_proof(), - )?; + verify_stark(claim, final_deferred_root, proof.miden_proof())?; Ok(precompile_security_level .map(|level| miden_security_level.min(level)) @@ -137,58 +136,53 @@ impl Verifier { /// deferred root. pub fn verify_partial( &self, - program_info: ProgramInfo, - stack_inputs: StackInputs, - stack_outputs: StackOutputs, proof: ExecutionProof, - ) -> Result<(u32, DeferredState), VerificationError> { + claim: ExecutionClaim, + ) -> Result<(u32, Unsettled), VerificationError> { let security_level = proof.security_level(); let deferred_state = hydrate_deferred_state(proof.deferred_proof(), self.max_deferred_elements)?; - verify_stark( - program_info, - stack_inputs, - stack_outputs, - deferred_state.root(), - proof.miden_proof(), - )?; + verify_stark(claim, deferred_state.root(), proof.miden_proof())?; - Ok((security_level, deferred_state)) + Ok((security_level, Unsettled(deferred_state))) } } -/// Returns the security level of the final proof if the specified program was executed correctly -/// against the specified inputs and outputs. -/// -/// This is a compatibility shim for `Verifier::default().verify(...)`. -/// -/// Specifically, verifies that if a program with the specified `program_hash` is executed against -/// the provided `stack_inputs` and some secret inputs, the result is equal to the `stack_outputs`. +/// The obligation a partially verified proof hands back: the hydrated deferred state whose root +/// the verified statement bound. /// -/// Stack inputs are expected to be ordered as if they would be pushed onto the stack one by one. -/// Thus, their expected order on the stack will be the reverse of the order in which they are -/// provided, and the last value in the `stack_inputs` slice is expected to be the value at the top -/// of the stack. +/// It must be settled into a final proof form or re-exposed in the caller's own statement; it +/// must not be dropped. +#[must_use = "the deferred obligation must be settled or re-exposed, not dropped"] +#[derive(Debug)] +pub struct Unsettled(DeferredState); + +impl Unsettled { + /// Returns the deferred root bound by the verified statement. + pub fn root(&self) -> Word { + self.0.root() + } + + /// Consumes the obligation into its hydrated deferred state, for settlement or re-exposure. + pub fn into_state(self) -> DeferredState { + self.0 + } +} + +/// Returns the security level of the final proof if it proves a correct execution of the given +/// claim, under the default verifier configuration. /// -/// Stack outputs are expected to be ordered as if they would be popped off the stack one by one. -/// Thus, the value at the top of the stack is expected to be in the first position of the -/// `stack_outputs` slice, and the order of the rest of the output elements will also match the -/// order on the stack. This is the reverse of the order of the `stack_inputs` slice. +/// 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. /// /// # Errors /// Returns an error if: -/// - The provided proof does not prove a correct execution of the program. +/// - The provided proof does not prove a correct execution of the claim. /// - The proof carries wire-backed deferred proof material, which is a partial/delegable form. /// - The proof's STARK-backed deferred proof, if present, does not verify against its public root. -#[deprecated(since = "0.25.0", note = "use Verifier::new().verify(...) instead")] -pub fn verify( - program_info: ProgramInfo, - stack_inputs: StackInputs, - stack_outputs: StackOutputs, - proof: ExecutionProof, -) -> Result { - Verifier::default().verify(program_info, stack_inputs, stack_outputs, proof) +pub fn verify(proof: ExecutionProof, claim: ExecutionClaim) -> Result { + Verifier::default().verify(proof, claim) } // HELPER FUNCTIONS @@ -224,21 +218,26 @@ fn hydrate_deferred_state( } fn stark_security_level(_proof: &StarkProof) -> u32 { - // 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 + // become real before the composite is trustworthy for deferred proofs. 96 } fn verify_stark( - program_info: ProgramInfo, - stack_inputs: StackInputs, - stack_outputs: StackOutputs, + claim: ExecutionClaim, final_deferred_root: Word, stark_proof: &StarkProof, ) -> Result<(), VerificationError> { - let program_hash = *program_info.program_hash(); - - let pub_inputs = - PublicInputs::new(program_info, stack_inputs, stack_outputs, final_deferred_root); + let program_hash = claim.program_root(); + + let pub_inputs = PublicInputs::new( + claim.to_program_info(), + *claim.stack_inputs(), + *claim.stack_outputs(), + final_deferred_root, + ); let (public_values, aux_inputs) = pub_inputs.to_air_inputs(); let hash_fn = stark_proof.hash_fn(); @@ -325,14 +324,13 @@ where let proof_encoding_config = wincode::config::Configuration::default() .with_preallocation_size_limit::(); - let proof: StarkProofData = , - > as wincode::config::Deserialize<_>>::deserialize( - proof_bytes, proof_encoding_config + let proof = deserialize_serde_exact::, _>( + proof_bytes, + proof_encoding_config, )?; let mut challenger = config.challenger(); - config::observe_protocol_params(&mut challenger); + config::observe_protocol_params(config.pcs(), &mut challenger); // `air_inputs` are the public values read by the AIRs (stack i/o); `aux_inputs` are the // statement inputs read during observation/boundary correction. The lifted verifier absorbs @@ -359,6 +357,20 @@ mod tests { use super::*; + #[test] + fn exact_serde_decoding_rejects_trailing_bytes() { + let encoding_config = wincode::config::Configuration::default() + .with_preallocation_size_limit::(); + let mut encoded = + as wincode::config::Serialize<_>>::serialize(&7, encoding_config) + .expect("u8 serialization must succeed"); + encoded.push(0); + + let err = deserialize_serde_exact::(&encoded, encoding_config) + .expect_err("trailing bytes must be rejected"); + assert!(matches!(err, wincode::error::ReadError::TrailingBytes)); + } + #[test] fn final_deferred_root_resolution_accepts_empty_rejects_wire_and_verifies_stark() { let (root, security_level) = resolve_final_deferred_root(&DeferredProof::Empty).unwrap(); diff --git a/verifier/src/recursive/mod.rs b/verifier/src/recursive/mod.rs new file mode 100644 index 0000000000..33f35a7ae9 --- /dev/null +++ b/verifier/src/recursive/mod.rs @@ -0,0 +1,531 @@ +//! Building the advice a MASM recursive verifier consumes to verify a Miden VM proof. +//! +//! `exec.vm::verify_vm_proof` reads a STARK proof from the advice provider in a fixed +//! order. This module is the producer side of that ABI: it destructures an [`ExecutionProof`] +//! against its [`ExecutionClaim`] into the advice-stack stream, the Merkle store, and the query +//! advice-map entries the verifier consumes. The consumption order is exercised end to end by the +//! recursive verification tests, which drive the real MASM verifier over this output. +//! +//! The stream carries only the proof — the claim is the consumer's and never travels in it: +//! +//! security params (nq, query_pow, deep_pow, folding_pow) -> +//! deferred root -> Miden AIR heights -> main commit -> aux commit -> +//! aux finals -> quotient commit -> deep alpha -> OOD evals -> +//! DEEP PoW witness -> FRI rounds -> FRI remainder -> query PoW witness +//! +//! The consumer stages the 40-felt claim encoding into VM memory from its own claim; +//! `verify_vm_proof` verifies this stream against that claim, so a substituted stream +//! fails rather than redefining the claim. Everything else is content-addressed in the advice +//! map and merges across proofs without collision: the kernel digest witness under the kernel +//! commitment K (`[count, digests..]`), the query rows, Merkle store, and ACE circuit. + +use alloc::{ + string::{String, ToString}, + sync::Arc, + vec, + vec::Vec, +}; + +use miden_air::{ + MIDEN_AIR_COUNT, MidenMultiAir, ProofOrder, PublicInputs, Statement, + ace::build_recursive_verifier_ace_circuit, config, +}; +use miden_core::{ + Felt, Word, + crypto::merkle::{MerklePath, MerkleStore, PartialMerkleTree}, + deferred::{DEFAULT_MAX_DEFERRED_ELEMENTS, DeferredState, IntegrityError, TRUE_DIGEST}, + field::QuadFelt, + program::{ExecutionClaim, request_key}, + proof::{DeferredProof, ExecutionProof, HashFunction}, +}; +use miden_crypto::{ + field::BasedVectorSpace, + stark::{ + StarkConfig, VerifierInstance, + lmcs::{Lmcs, proof::BatchProofView}, + pcs::{PcsParams, PcsProof}, + proof::{StarkProof, StarkProofData}, + verifier::VerifierError as CryptoVerifierError, + }, +}; +use serde_wincode::wincode; + +use crate::{MAX_STARK_PROOF_BYTES, deserialize_serde_exact}; + +// TYPES +// ================================================================================================ + +type Challenge = QuadFelt; +type P2Config = config::Poseidon2Config; +type P2Lmcs = >::Lmcs; +type P2ProofData = StarkProofData; + +/// The advice a MASM recursive verifier consumes to verify one Miden VM proof. +/// +/// The `advice_stack` stream feeds `exec.vm::verify_vm_proof` directly; +/// [`Self::into_request_package`] instead registers it in the advice map under +/// `request_key(verifier_root, claim_commitment)` for consumers that fetch proofs by content. +#[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, + /// 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)>, + /// Commitment to the execution claim: the content address (paired with a verifier root) the + /// proof stream is registered under. + pub claim_commitment: Word, +} + +impl RecursiveVerifierInputs { + /// Moves the proof stream into the advice map under + /// `request_key(verifier_root, claim_commitment)`, leaving the advice stack empty. + /// + /// All of it (Merkle nodes, query rows, proof stream) is content-addressed, so packages + /// for any number of proofs merge into one advice provider in any order. A consumer holding the + /// claim commitment fetches the package under this key and verifies it with + /// `exec.vm::verify_vm_proof`; the key is addressing, not trust — a package that does not match + /// the consumer's claim fails verification. + 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 + } +} + +/// Errors returned while building the advice for recursive verification. +#[derive(Debug, thiserror::Error)] +pub enum RecursiveAdviceError { + #[error("proof deserialization error: {0}")] + ProofDeserialization(String), + #[error("STARK proof is too large: {size} bytes exceeds the {max} byte limit")] + ProofTooLarge { size: usize, max: usize }, + #[error("invalid proof shape: {0}")] + InvalidProofShape(&'static str), + #[error("statement assembly error: {0}")] + StatementAssembly(String), + #[error("deferred wire hydration failed: {0}")] + DeferredIntegrity(#[from] IntegrityError), + #[error("recursive verification supports only Poseidon2 proofs, got {0:?}")] + UnsupportedHashFunction(HashFunction), + #[error("transcript error: {0}")] + Transcript(#[from] CryptoVerifierError), +} + +/// Merkle store + advice map pair returned by Merkle data construction. +type MerkleAdvice = (MerkleStore, Vec<(Word, Vec)>); + +/// The per-AIR log trace heights, in both arrangements the advice needs: the fixed instance +/// order (streamed to the verifier) and the sorted proof order (ACE circuit selection). +struct MidenTraceHeights { + instance_log_heights: [usize; MIDEN_AIR_COUNT], + proof_order: ProofOrder, +} + +// PUBLIC API +// ================================================================================================ + +/// Builds the advice a MASM recursive verifier consumes to verify a Miden VM proof against +/// its claim. +/// +/// The proof must be a Poseidon2 proof — the recursive verifier verifies only Poseidon2 STARKs. +pub fn advice_inputs( + proof: &ExecutionProof, + claim: &ExecutionClaim, +) -> Result { + let stark = proof.miden_proof(); + if stark.hash_fn() != HashFunction::Poseidon2 { + return Err(RecursiveAdviceError::UnsupportedHashFunction(stark.hash_fn())); + } + let pub_inputs = PublicInputs::new( + claim.to_program_info(), + *claim.stack_inputs(), + *claim.stack_outputs(), + resolve_deferred_root(proof.deferred_proof())?, + ); + + let mut inputs = build_from_proof_bytes(stark.bytes(), &pub_inputs, claim.commitment())?; + + // Content-addressed kernel advice. The verifier checks the fetched witness against K, so + // proofs sharing a kernel produce identical entries that merge. + let kernel = claim.kernel(); + let mut kernel_witness = vec![Felt::new_unchecked(kernel.proc_hashes().len() as u64)]; + for digest in kernel.proc_hashes() { + kernel_witness.extend_from_slice(digest.as_elements()); + } + inputs.advice_map.push((kernel.commitment(), kernel_witness)); + + Ok(inputs) +} + +/// Resolves the deferred root the outer VM statement binds, from the proof's deferred material: +/// the canonical TRUE digest when no precompile claims were produced, the nested proof's public +/// root when STARK-backed, and the hydrated wire's root for partial proofs (standard precompile +/// registry, default deferred-element budget). +fn resolve_deferred_root(deferred: &DeferredProof) -> Result { + match deferred { + DeferredProof::Empty => Ok(TRUE_DIGEST), + DeferredProof::Stark { public_root, .. } => Ok(*public_root), + DeferredProof::Wire(wire) => Ok(DeferredState::from_wire( + Arc::new(miden_precompiles::registry()), + wire, + DEFAULT_MAX_DEFERRED_ELEMENTS, + )? + .root()), + } +} + +// ADVICE CONSTRUCTION +// ================================================================================================ + +fn build_from_proof_bytes( + proof_bytes: &[u8], + pub_inputs: &PublicInputs, + claim_commitment: Word, +) -> Result { + let config = config::poseidon2_config(config::pcs_params(), config::RELATION_DIGEST); + + let proof = deserialize_proof(proof_bytes)?; + + let (public_values, aux_inputs) = pub_inputs.to_air_inputs(); + let mut challenger = config.challenger(); + config::observe_protocol_params(config.pcs(), &mut challenger); + + let statement = + Statement::::new(MidenMultiAir::new(), public_values, aux_inputs) + .map_err(|e| RecursiveAdviceError::StatementAssembly(e.to_string()))?; + let verifier_instance = VerifierInstance::new(&config, &statement, None) + .expect("Miden AIRs declare no preprocessed columns"); + + let (stark, _digest) = StarkProof::from_data(&verifier_instance, &proof, challenger)?; + + let heights = miden_trace_heights(&stark)?; + + build_advice(&config, &stark, heights, pub_inputs, claim_commitment) +} + +/// Deserializes a wincode-encoded Poseidon2 STARK proof, enforcing the total byte limit, +/// bounding preallocation, and rejecting trailing bytes. +fn deserialize_proof(proof_bytes: &[u8]) -> Result { + if proof_bytes.len() > MAX_STARK_PROOF_BYTES { + return Err(RecursiveAdviceError::ProofTooLarge { + size: proof_bytes.len(), + max: MAX_STARK_PROOF_BYTES, + }); + } + + let encoding_config = wincode::config::Configuration::default() + .with_preallocation_size_limit::(); + deserialize_serde_exact::(proof_bytes, encoding_config) + .map_err(|e| RecursiveAdviceError::ProofDeserialization(e.to_string())) +} + +fn miden_trace_heights( + stark: &StarkProof, +) -> Result { + let log_heights = stark.log_trace_heights(); + let Ok(log_heights): Result<[u8; MIDEN_AIR_COUNT], _> = log_heights.try_into() else { + return Err(RecursiveAdviceError::InvalidProofShape( + "unexpected number of AIR log heights", + )); + }; + Ok(MidenTraceHeights { + instance_log_heights: log_heights.map(usize::from), + proof_order: ProofOrder::from_instance_log_heights(&log_heights), + }) +} + +/// Packs the parsed STARK transcript into the advice-stack stream, Merkle store, and advice map. +fn build_advice( + config: &P2Config, + stark: &StarkProof, + heights: MidenTraceHeights, + pub_inputs: &PublicInputs, + claim_commitment: Word, +) -> Result { + let pcs = &stark.pcs_proof; + if stark.all_aux_values.len() != MIDEN_AIR_COUNT { + return Err(RecursiveAdviceError::InvalidProofShape( + "unexpected number of aux-final groups", + )); + } + + // The stream carries only the proof: the deferred root the execution produced, the proof + // shape, and the STARK transcript. The claim itself (kernel witness, program digest, stack + // i/o) is the consumer's — it fills those into VM memory from its own inputs, never from this + // (untrusted, fetched) stream — so a substituted package fails verification against the + // consumer's claim rather than silently redefining it. + // + // The section order below mirrors the consumption-order list in the module doc; both are + // pinned against the MASM verifier by the stark e2e differential tests. + + let mut advice_stack = security_parameter_words(config.pcs()).to_vec(); + + // Final deferred root, loaded by `public_inputs::stage_boundary_inputs`. + advice_stack.extend_from_slice(pub_inputs.deferred_root().as_ref()); + + for height in heights.instance_log_heights { + advice_stack.push(Felt::new_unchecked(height as u64)); + } + + advice_stack.extend_from_slice(&commitment_felts(stark.main_commit)); + advice_stack.extend_from_slice(&commitment_felts(stark.aux_commit)); + + for aux_values in &stark.all_aux_values { + advice_stack.extend_from_slice(&challenge_felts(aux_values)); + } + + advice_stack.extend_from_slice(&commitment_felts(stark.quotient_commit)); + + // The verifier consumes the DEEP alpha's two extension coordinates high-first. + let deep_alpha = pcs.deep_proof.challenge_columns; + let deep_coeffs: &[Felt] = deep_alpha.as_basis_coefficients_slice(); + advice_stack.extend_from_slice(&[deep_coeffs[1], deep_coeffs[0]]); + + append_ood_evaluations(&mut advice_stack, pcs)?; + + advice_stack.push(pcs.deep_proof.pow_witness); + + for round in &pcs.fri_proof.rounds { + advice_stack.extend_from_slice(&commitment_felts(round.commitment)); + advice_stack.push(round.pow_witness); + } + + let final_poly = &pcs.fri_proof.final_poly; + advice_stack.extend_from_slice(&QuadFelt::flatten_to_base(final_poly.to_vec())); + + advice_stack.push(pcs.query_pow_witness); + + let (store, advice_map) = build_merkle_data(config, stark, &heights.proof_order)?; + + Ok(RecursiveVerifierInputs { + advice_stack, + store, + advice_map, + claim_commitment, + }) +} + +/// Returns the proof-package header in the order consumed by the recursive MASM verifier. +fn security_parameter_words(params: &PcsParams) -> [Felt; 4] { + [ + Felt::new_unchecked(params.num_queries() as u64), + Felt::new_unchecked(params.query_pow_bits() as u64), + Felt::new_unchecked(params.deep_pow_bits() as u64), + Felt::new_unchecked(params.folding_pow_bits() as u64), + ] +} + +// OOD EVALUATIONS +// ================================================================================================ + +/// Flatten OOD evaluations into the advice stack. +/// +/// The DEEP transcript contains evaluations at two points (z and z*g) for each committed matrix +/// (main, aux, quotient), split into local (at z) and next (at z*g) rows, appended local-first. +fn append_ood_evaluations( + advice_stack: &mut Vec, + pcs: &PcsProof, +) -> Result<(), RecursiveAdviceError> +where + L: Lmcs, +{ + let evals = &pcs.deep_proof.evals; + let mut local_values = Vec::new(); + let mut next_values = Vec::new(); + + for group in evals { + for matrix in group { + let width = matrix.width; + let values = matrix.values.as_slice(); + // A matrix carries its local row and, for two-point openings, its next row. + if values.len() != width && values.len() != 2 * width { + return Err(RecursiveAdviceError::InvalidProofShape( + "OOD matrix must hold exactly one or two rows", + )); + } + local_values.extend_from_slice(&values[..width]); + if values.len() == 2 * width { + next_values.extend_from_slice(&values[width..]); + } + } + } + + advice_stack.extend_from_slice(&challenge_felts(&local_values)); + advice_stack.extend_from_slice(&challenge_felts(&next_values)); + Ok(()) +} + +// MERKLE DATA +// ================================================================================================ + +/// Build the Merkle store and advice map from the DEEP and FRI opening proofs. +/// +/// Each opening proof becomes a `PartialMerkleTree` (for the store) and `leaf_hash -> leaf_data` +/// entries (for the advice map). The verifier fetches authentication paths with `mtree_get` and +/// leaf data with `adv.push_mapval`. +fn build_merkle_data( + config: &P2Config, + stark: &StarkProof, + proof_order: &ProofOrder, +) -> Result { + let pcs = &stark.pcs_proof; + let lmcs = config.lmcs(); + + let mut store = MerkleStore::new(); + let mut advice_map = Vec::new(); + + // DEEP openings (one BatchProof per commitment: main, aux, quotient), then FRI openings + // (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)?; + store.extend(tree.inner_nodes()); + advice_map.extend(entries); + } + + let registry_tree = config::ace_circuit_registry_tree(); + store.extend(registry_tree.inner_nodes()); + + let circuit = build_recursive_verifier_ace_circuit(proof_order).map_err(|_| { + RecursiveAdviceError::InvalidProofShape("failed to build recursive ACE circuit") + })?; + advice_map.push((circuit.commitment, circuit.instructions)); + + Ok((store, advice_map)) +} + +/// Converts a `BatchProof` into a `PartialMerkleTree` (for the store) and its +/// `leaf_hash -> leaf_data` advice-map entries. +fn batch_proof_to_merkle( + lmcs: &L, + batch_proof: &L::BatchProof, +) -> Result<(PartialMerkleTree, Vec<(Word, Vec)>), RecursiveAdviceError> +where + L: Lmcs, + L::Commitment: Copy + PartialEq + Into<[Felt; 4]>, + L::BatchProof: BatchProofView, +{ + let mut paths = Vec::new(); + let mut advice_entries = Vec::new(); + + for index in batch_proof.indices() { + let rows = batch_proof + .opening(index) + .ok_or(RecursiveAdviceError::InvalidProofShape("missing opening for query index"))?; + let siblings = batch_proof.path(index).ok_or(RecursiveAdviceError::InvalidProofShape( + "missing Merkle path for query index", + ))?; + + let leaf_data: Vec = rows.as_slice().to_vec(); + let leaf_word: Word = Word::new(lmcs.hash(rows.iter_rows()).into()); + let merkle_path = + MerklePath::new(siblings.into_iter().map(|c| Word::new(c.into())).collect()); + + paths.push((index as u64, leaf_word, merkle_path)); + advice_entries.push((leaf_word, leaf_data)); + } + + let tree = PartialMerkleTree::with_paths(paths) + .map_err(|_| RecursiveAdviceError::InvalidProofShape("invalid merkle paths"))?; + + Ok((tree, advice_entries)) +} + +fn commitment_felts>(commitment: C) -> [Felt; 4] { + commitment.into() +} + +fn challenge_felts(challenges: &[Challenge]) -> Vec { + QuadFelt::flatten_to_base(challenges.to_vec()) +} + +// TESTS +// ================================================================================================ + +#[cfg(test)] +mod tests { + use miden_core::program::{KernelDescriptor, ProgramInfo, StackInputs, StackOutputs}; + + use super::*; + + /// The top-level entry rejects non-Poseidon2 proofs up front, before touching the proof + /// bytes — the recursive verifier verifies only Poseidon2 STARKs. + #[test] + fn advice_inputs_rejects_non_poseidon2_proofs() { + let proof = ExecutionProof::from_parts( + Vec::new(), + HashFunction::Blake3_256, + DeferredProof::empty(), + ); + let claim = ExecutionClaim::from_program_info( + ProgramInfo::new(Word::default(), KernelDescriptor::default()), + StackInputs::default(), + StackOutputs::default(), + ); + + let err = advice_inputs(&proof, &claim).expect_err("a Blake3 proof must be rejected"); + assert!(matches!( + err, + RecursiveAdviceError::UnsupportedHashFunction(HashFunction::Blake3_256) + )); + } + + /// The proof-package header must describe the supplied PCS parameters rather than the Miden + /// VM's current defaults; otherwise its transcript and MASM security checks can disagree. + #[test] + fn security_parameter_header_uses_the_supplied_pcs_params() { + let params = PcsParams::new(4, 3, 6, 5, 11, 19, 13).expect("valid distinct PCS params"); + + assert_eq!(security_parameter_words(¶ms), [19, 13, 11, 5].map(Felt::new_unchecked),); + } + + #[test] + fn proof_deserialization_rejects_oversized_input() { + let proof_bytes = vec![0; MAX_STARK_PROOF_BYTES + 1]; + + let err = deserialize_proof(&proof_bytes).expect_err("oversized proof must be rejected"); + assert!(matches!( + err, + RecursiveAdviceError::ProofTooLarge { + size, + max: MAX_STARK_PROOF_BYTES, + } if size == proof_bytes.len() + )); + } + + /// Request packaging is a pure repackaging: the proof stream moves — unchanged and in + /// order — into the advice map under `request_key(verifier_root, claim_commitment)`, and + /// everything else is untouched. + #[test] + fn request_package_moves_proof_under_request_key() { + let proof_stream: Vec = (1..=8u64).map(Felt::new_unchecked).collect(); + let claim_commitment = Word::from([11u64, 12, 13, 14].map(Felt::new_unchecked)); + let verifier_root = Word::from([21u64, 22, 23, 24].map(Felt::new_unchecked)); + let query_entry = ( + Word::from([31u64, 32, 33, 34].map(Felt::new_unchecked)), + vec![Felt::new_unchecked(7)], + ); + + let inputs = RecursiveVerifierInputs { + advice_stack: proof_stream.clone(), + store: MerkleStore::new(), + advice_map: vec![query_entry.clone()], + claim_commitment, + }; + + let package = inputs.into_request_package(verifier_root); + + assert!(package.advice_stack.is_empty(), "the proof must leave the advice stack"); + assert_eq!(package.claim_commitment, claim_commitment); + assert_eq!(package.advice_map.len(), 2, "existing entries stay, proof entry added"); + assert_eq!(package.advice_map[0], query_entry); + assert_eq!( + package.advice_map[1], + (request_key(verifier_root, claim_commitment), proof_stream) + ); + } +}