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, 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 }
101 .map_err(|source| VerificationError::ProgramVerificationError(program_hash, source))?;
102
103 Ok(security_level)
104}
105
106// ERRORS
107// ================================================================================================
108
109/// TODO: add docs
110#[derive(Debug, thiserror::Error)]
111pub enum VerificationError {
112 #[error("failed to verify proof for program with hash {0}")]
113 ProgramVerificationError(Word, #[source] VerifierError),
114 #[error("the input {0} is not a valid field element")]
115 InputNotFieldElement(u64),
116 #[error("the output {0} is not a valid field element")]
117 OutputNotFieldElement(u64),
118}