miden_verifier/
lib.rs

1#![no_std]
2
3extern crate alloc;
4
5#[cfg(feature = "std")]
6extern crate std;
7
8use alloc::vec;
9
10use miden_air::{HashFunction, ProcessorAir, ProvingOptions, PublicInputs};
11use miden_core::crypto::{
12    hash::{Blake3_192, Blake3_256, Poseidon2, Rpo256, Rpx256},
13    random::{RpoRandomCoin, RpxRandomCoin, WinterRandomCoin},
14};
15// EXPORTS
16// ================================================================================================
17pub use miden_core::{Kernel, ProgramInfo, StackInputs, StackOutputs, Word};
18pub use winter_verifier::{AcceptableOptions, VerifierError};
19use winter_verifier::{crypto::MerkleTree, verify as verify_proof};
20pub mod math {
21    pub use miden_core::{Felt, FieldElement, StarkField};
22}
23pub use miden_air::ExecutionProof;
24
25// VERIFIER
26// ================================================================================================
27/// Returns the security level of the proof if the specified program was executed correctly against
28/// the specified inputs and outputs.
29///
30/// Specifically, verifies that if a program with the specified `program_hash` is executed against
31/// the provided `stack_inputs` and some secret inputs, the result is equal to the `stack_outputs`.
32///
33/// Stack inputs are expected to be ordered as if they would be pushed onto the stack one by one.
34/// Thus, their expected order on the stack will be the reverse of the order in which they are
35/// provided, and the last value in the `stack_inputs` slice is expected to be the value at the top
36/// of the stack.
37///
38/// Stack outputs are expected to be ordered as if they would be popped off the stack one by one.
39/// Thus, the value at the top of the stack is expected to be in the first position of the
40/// `stack_outputs` slice, and the order of the rest of the output elements will also match the
41/// order on the stack. This is the reverse of the order of the `stack_inputs` slice.
42///
43/// The verifier accepts proofs generated using a parameter set defined in [ProvingOptions].
44/// Specifically, parameter sets targeting the following are accepted:
45/// - 96-bit security level, non-recursive context (BLAKE3 hash function).
46/// - 96-bit security level, recursive context (BLAKE3 hash function).
47/// - 128-bit security level, non-recursive context (RPO hash function).
48/// - 128-bit security level, recursive context (RPO hash function).
49///
50/// # Errors
51/// Returns an error if:
52/// - The provided proof does not prove a correct execution of the program.
53/// - The protocol parameters used to generate the proof are not in the set of acceptable
54///   parameters.
55#[tracing::instrument("verify_program", skip_all)]
56pub fn verify(
57    program_info: ProgramInfo,
58    stack_inputs: StackInputs,
59    stack_outputs: StackOutputs,
60    proof: ExecutionProof,
61) -> Result<u32, VerificationError> {
62    // get security level of the proof
63    let security_level = proof.security_level();
64    let program_hash = *program_info.program_hash();
65
66    // build public inputs and try to verify the proof
67    let pub_inputs = PublicInputs::new(program_info, stack_inputs, stack_outputs);
68    let (hash_fn, proof) = proof.into_parts();
69    match hash_fn {
70        HashFunction::Blake3_192 => {
71            let opts = AcceptableOptions::OptionSet(vec![ProvingOptions::REGULAR_96_BITS]);
72            verify_proof::<ProcessorAir, Blake3_192, WinterRandomCoin<_>, MerkleTree<_>>(
73                proof, pub_inputs, &opts,
74            )
75        },
76        HashFunction::Blake3_256 => {
77            let opts = AcceptableOptions::OptionSet(vec![ProvingOptions::REGULAR_128_BITS]);
78            verify_proof::<ProcessorAir, Blake3_256, WinterRandomCoin<_>, MerkleTree<_>>(
79                proof, pub_inputs, &opts,
80            )
81        },
82        HashFunction::Rpo256 => {
83            let opts = AcceptableOptions::OptionSet(vec![
84                ProvingOptions::RECURSIVE_96_BITS,
85                ProvingOptions::RECURSIVE_128_BITS,
86            ]);
87            verify_proof::<ProcessorAir, Rpo256, RpoRandomCoin, MerkleTree<_>>(
88                proof, pub_inputs, &opts,
89            )
90        },
91        HashFunction::Rpx256 => {
92            let opts = AcceptableOptions::OptionSet(vec![
93                ProvingOptions::RECURSIVE_96_BITS,
94                ProvingOptions::RECURSIVE_128_BITS,
95            ]);
96            verify_proof::<ProcessorAir, Rpx256, RpxRandomCoin, MerkleTree<_>>(
97                proof, pub_inputs, &opts,
98            )
99        },
100        HashFunction::Poseidon2 => {
101            let opts = AcceptableOptions::OptionSet(vec![
102                ProvingOptions::RECURSIVE_96_BITS,
103                ProvingOptions::REGULAR_128_BITS,
104            ]);
105            verify_proof::<ProcessorAir, Poseidon2, WinterRandomCoin<_>, MerkleTree<_>>(
106                proof, pub_inputs, &opts,
107            )
108        },
109    }
110    .map_err(|source| VerificationError::ProgramVerificationError(program_hash, source))?;
111
112    Ok(security_level)
113}
114
115// ERRORS
116// ================================================================================================
117
118/// TODO: add docs
119#[derive(Debug, thiserror::Error)]
120pub enum VerificationError {
121    #[error("failed to verify proof for program with hash {0}")]
122    ProgramVerificationError(Word, #[source] VerifierError),
123    #[error("the input {0} is not a valid field element")]
124    InputNotFieldElement(u64),
125    #[error("the output {0} is not a valid field element")]
126    OutputNotFieldElement(u64),
127}
miden_verifier/lib.rs

miden_verifier/
lib.rs
