miden_verifier/
lib.rs

1#![no_std]
2
3extern crate alloc;
4
5#[cfg(feature = "std")]
6extern crate std;
7
8use alloc::{boxed::Box, vec::Vec};
9
10use miden_air::{ProcessorAir, PublicInputs, config};
11use miden_core::{
12    Felt,
13    field::{QuadFelt, TwoAdicField},
14};
15use miden_crypto::stark::{
16    StarkConfig, air::VarLenPublicInputs, challenger::CanObserve, lmcs::Lmcs, proof::StarkProof,
17};
18use serde::de::DeserializeOwned;
19
20// RE-EXPORTS
21// ================================================================================================
22mod exports {
23    pub use miden_core::{
24        Word,
25        precompile::{
26            PrecompileTranscriptDigest, PrecompileTranscriptState, PrecompileVerificationError,
27            PrecompileVerifierRegistry,
28        },
29        program::{Kernel, ProgramInfo, StackInputs, StackOutputs},
30        proof::{ExecutionProof, HashFunction},
31    };
32    pub mod math {
33        pub use miden_core::Felt;
34    }
35}
36pub use exports::*;
37
38// VERIFIER
39// ================================================================================================
40
41/// Returns the security level of the proof if the specified program was executed correctly against
42/// the specified inputs and outputs.
43///
44/// Specifically, verifies that if a program with the specified `program_hash` is executed against
45/// the provided `stack_inputs` and some secret inputs, the result is equal to the `stack_outputs`.
46///
47/// Stack inputs are expected to be ordered as if they would be pushed onto the stack one by one.
48/// Thus, their expected order on the stack will be the reverse of the order in which they are
49/// provided, and the last value in the `stack_inputs` slice is expected to be the value at the top
50/// of the stack.
51///
52/// Stack outputs are expected to be ordered as if they would be popped off the stack one by one.
53/// Thus, the value at the top of the stack is expected to be in the first position of the
54/// `stack_outputs` slice, and the order of the rest of the output elements will also match the
55/// order on the stack. This is the reverse of the order of the `stack_inputs` slice.
56///
57/// # Errors
58/// Returns an error if:
59/// - The provided proof does not prove a correct execution of the program.
60/// - The proof contains one or more precompile requests. When precompile requests are present, use
61///   [`verify_with_precompiles`] instead with an appropriate [`PrecompileVerifierRegistry`] to
62///   verify the precompile computations.
63pub fn verify(
64    program_info: ProgramInfo,
65    stack_inputs: StackInputs,
66    stack_outputs: StackOutputs,
67    proof: ExecutionProof,
68) -> Result<u32, VerificationError> {
69    let (security_level, _commitment) = verify_with_precompiles(
70        program_info,
71        stack_inputs,
72        stack_outputs,
73        proof,
74        &PrecompileVerifierRegistry::new(),
75    )?;
76    Ok(security_level)
77}
78
79/// Identical to [`verify`], with additional verification of any precompile requests made during the
80/// VM execution. The resulting aggregated precompile commitment is returned, which can be compared
81/// against the commitment computed by the VM.
82///
83/// # Returns
84/// Returns a tuple `(security_level, aggregated_commitment)` where:
85/// - `security_level`: The security level (in bits) of the verified proof
86/// - `aggregated_commitment`: A [`Word`] containing the final aggregated commitment to all
87///   precompile requests, computed by recomputing and recording each precompile commitment in a
88///   transcript. This value is the finalized digest of the recomputed precompile transcript.
89///
90/// # Errors
91/// Returns any error produced by [`verify`], as well as any errors resulting from precompile
92/// verification.
93#[tracing::instrument("verify_program", skip_all)]
94pub fn verify_with_precompiles(
95    program_info: ProgramInfo,
96    stack_inputs: StackInputs,
97    stack_outputs: StackOutputs,
98    proof: ExecutionProof,
99    precompile_verifiers: &PrecompileVerifierRegistry,
100) -> Result<(u32, PrecompileTranscriptDigest), VerificationError> {
101    let security_level = proof.security_level();
102
103    let (hash_fn, proof_bytes, precompile_requests) = proof.into_parts();
104
105    // Recompute the precompile transcript by verifying all precompile requests and recording the
106    // commitments.
107    // If no verifiers were provided (e.g. when this function was called from `verify()`),
108    // but the proof contained requests anyway, returns a `NoVerifierFound` error.
109    let recomputed_transcript = precompile_verifiers
110        .requests_transcript(&precompile_requests)
111        .map_err(VerificationError::PrecompileVerificationError)?;
112    let pc_transcript_state = recomputed_transcript.state();
113
114    // Verify the STARK proof with the recomputed transcript state in public inputs
115    verify_stark(
116        program_info,
117        stack_inputs,
118        stack_outputs,
119        pc_transcript_state,
120        hash_fn,
121        proof_bytes,
122    )?;
123
124    // Finalize transcript to return the digest
125    let digest = recomputed_transcript.finalize();
126    Ok((security_level, digest))
127}
128
129// HELPER FUNCTIONS
130// ================================================================================================
131
132fn verify_stark(
133    program_info: ProgramInfo,
134    stack_inputs: StackInputs,
135    stack_outputs: StackOutputs,
136    pc_transcript_state: PrecompileTranscriptState,
137    hash_fn: HashFunction,
138    proof_bytes: Vec<u8>,
139) -> Result<(), VerificationError> {
140    let program_hash = *program_info.program_hash();
141
142    let pub_inputs =
143        PublicInputs::new(program_info, stack_inputs, stack_outputs, pc_transcript_state);
144    let (public_values, kernel_felts) = pub_inputs.to_air_inputs();
145    let var_len_public_inputs: &[&[Felt]] = &[&kernel_felts];
146
147    let params = config::pcs_params();
148    match hash_fn {
149        HashFunction::Blake3_256 => {
150            let config = config::blake3_256_config(params);
151            verify_stark_proof(&config, &public_values, var_len_public_inputs, &proof_bytes)
152        },
153        HashFunction::Rpo256 => {
154            let config = config::rpo_config(params);
155            verify_stark_proof(&config, &public_values, var_len_public_inputs, &proof_bytes)
156        },
157        HashFunction::Rpx256 => {
158            let config = config::rpx_config(params);
159            verify_stark_proof(&config, &public_values, var_len_public_inputs, &proof_bytes)
160        },
161        HashFunction::Poseidon2 => {
162            let config = config::poseidon2_config(params);
163            verify_stark_proof(&config, &public_values, var_len_public_inputs, &proof_bytes)
164        },
165        HashFunction::Keccak => {
166            let config = config::keccak_config(params);
167            verify_stark_proof(&config, &public_values, var_len_public_inputs, &proof_bytes)
168        },
169    }
170    .map_err(|e| VerificationError::StarkVerificationError(program_hash, Box::new(e)))?;
171
172    Ok(())
173}
174
175// ERRORS
176// ================================================================================================
177
178/// Errors that can occur during proof verification.
179#[derive(Debug, thiserror::Error)]
180pub enum VerificationError {
181    #[error("failed to verify STARK proof for program with hash {0}")]
182    StarkVerificationError(Word, #[source] Box<StarkVerificationError>),
183    #[error("failed to verify precompile calls")]
184    PrecompileVerificationError(#[source] PrecompileVerificationError),
185}
186
187// STARK PROOF VERIFICATION
188// ================================================================================================
189
190/// Errors that can occur during low-level STARK proof verification.
191#[derive(Debug, thiserror::Error)]
192pub enum StarkVerificationError {
193    #[error("failed to deserialize proof: {0}")]
194    Deserialization(#[from] bincode::Error),
195    #[error("log_trace_height {0} exceeds the two-adic order of the field")]
196    InvalidTraceHeight(u8),
197    #[error(transparent)]
198    Verifier(#[from] miden_crypto::stark::verifier::VerifierError),
199}
200
201/// Verifies a STARK proof for the given public values.
202///
203/// Pre-seeds the challenger with `public_values`, then delegates to the lifted
204/// verifier.
205fn verify_stark_proof<SC>(
206    config: &SC,
207    public_values: &[Felt],
208    var_len_public_inputs: VarLenPublicInputs<'_, Felt>,
209    proof_bytes: &[u8],
210) -> Result<(), StarkVerificationError>
211where
212    SC: StarkConfig<Felt, QuadFelt>,
213    <SC::Lmcs as Lmcs>::Commitment: DeserializeOwned,
214{
215    // Proof deserialization via bincode; see https://github.com/0xMiden/miden-vm/issues/2550
216    // The proof is serialized as a `(log_trace_height, stark_proof)` tuple; this is a temporary
217    // approach until the lifted STARK integrates trace height on its side.
218    let (log_trace_height, proof): (u8, StarkProof<Felt, QuadFelt, SC>) =
219        bincode::deserialize(proof_bytes)?;
220
221    if log_trace_height as usize > Felt::TWO_ADICITY {
222        return Err(StarkVerificationError::InvalidTraceHeight(log_trace_height));
223    }
224
225    let mut challenger = config.challenger();
226    challenger.observe_slice(public_values);
227    // TODO: observe log_trace_height in the transcript for Fiat-Shamir binding.
228    // TODO: observe var_len_public_inputs in the transcript for Fiat-Shamir binding.
229    //   This also requires updating the recursive verifier to absorb both fixed and
230    //   variable-length public inputs.
231    // TODO: observe ACE commitment once ACE verification is integrated.
232    // See https://github.com/0xMiden/miden-vm/issues/2822
233    miden_crypto::stark::verifier::verify_single(
234        config,
235        &ProcessorAir,
236        log_trace_height,
237        public_values,
238        var_len_public_inputs,
239        &proof,
240        challenger,
241    )?;
242    Ok(())
243}
miden_verifier/lib.rs

miden_verifier/
lib.rs
