Skip to main content

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