miden_prover/
lib.rs

1#![no_std]
2
3extern crate alloc;
4
5#[cfg(feature = "std")]
6extern crate std;
7
8use alloc::{string::ToString, vec, vec::Vec};
9
10use ::serde::Serialize;
11use miden_air::{MidenMultiAir, ProverStatement, Statement};
12use miden_core::{Felt, field::QuadFelt, utils::RowMajorMatrix};
13use miden_crypto::stark::{
14    ProverInstance, StarkConfig,
15    lmcs::Lmcs,
16    proof::{StarkOutput, StarkProofData},
17};
18use miden_processor::{
19    FastProcessor, Program,
20    trace::{ExecutionTrace, build_trace},
21};
22use serde_wincode::SerdeCompat;
23use tracing::instrument;
24
25mod proving_options;
26
27// EXPORTS
28// ================================================================================================
29pub use miden_air::{DeserializationError, MidenAir, PublicInputs, config};
30pub use miden_core::proof::{ExecutionProof, HashFunction};
31pub use miden_processor::{
32    ExecutionError, ExecutionOptions, ExecutionOutput, FutureMaybeSend, Host, InputError,
33    ProgramInfo, StackInputs, StackOutputs, SyncHost, TraceBuildInputs, TraceGenerationContext,
34    Word, advice::AdviceInputs, crypto, field, serde, utils,
35};
36pub use proving_options::ProvingOptions;
37
38/// Inputs required to prove from pre-executed trace data.
39#[derive(Debug)]
40pub struct TraceProvingInputs {
41    trace_inputs: TraceBuildInputs,
42    options: ProvingOptions,
43}
44
45impl TraceProvingInputs {
46    /// Creates a new bundle of post-execution trace inputs and proof-generation options.
47    pub fn new(trace_inputs: TraceBuildInputs, options: ProvingOptions) -> Self {
48        Self { trace_inputs, options }
49    }
50
51    /// Consumes this bundle and returns its trace inputs and proof-generation options.
52    pub fn into_parts(self) -> (TraceBuildInputs, ProvingOptions) {
53        (self.trace_inputs, self.options)
54    }
55}
56
57// PROVER
58// ================================================================================================
59
60/// Executes and proves the specified `program` and returns the result together with a STARK-based
61/// proof of the program's execution.
62///
63/// - `stack_inputs` specifies the initial state of the stack for the VM.
64/// - `advice_inputs` provides the initial nondeterministic inputs for the VM.
65/// - `host` specifies the host environment which contain non-deterministic (secret) inputs for the
66///   prover.
67/// - `execution_options` defines VM execution parameters such as cycle limits and fragmentation.
68/// - `proving_options` defines parameters for STARK proof generation.
69///
70/// # Errors
71/// Returns an error if program execution or STARK proof generation fails for any reason.
72#[instrument("prove_program", skip_all)]
73pub async fn prove(
74    program: &Program,
75    stack_inputs: StackInputs,
76    advice_inputs: AdviceInputs,
77    host: &mut impl Host,
78    execution_options: ExecutionOptions,
79    proving_options: ProvingOptions,
80) -> Result<(StackOutputs, ExecutionProof), ExecutionError> {
81    // execute the program to create an execution trace using FastProcessor
82    let processor = FastProcessor::new_with_options(stack_inputs, advice_inputs, execution_options)
83        .map_err(ExecutionError::advice_error_no_context)?;
84
85    let trace_inputs = processor.execute_trace_inputs(program, host).await?;
86    prove_from_trace_sync(TraceProvingInputs::new(trace_inputs, proving_options))
87}
88
89/// Synchronous wrapper for [`prove()`].
90#[instrument("prove_program_sync", skip_all)]
91pub fn prove_sync(
92    program: &Program,
93    stack_inputs: StackInputs,
94    advice_inputs: AdviceInputs,
95    host: &mut impl SyncHost,
96    execution_options: ExecutionOptions,
97    proving_options: ProvingOptions,
98) -> Result<(StackOutputs, ExecutionProof), ExecutionError> {
99    let processor = FastProcessor::new_with_options(stack_inputs, advice_inputs, execution_options)
100        .map_err(ExecutionError::advice_error_no_context)?;
101
102    let trace_inputs = processor.execute_trace_inputs_sync(program, host)?;
103    prove_from_trace_sync(TraceProvingInputs::new(trace_inputs, proving_options))
104}
105
106/// Builds an execution trace from pre-executed trace inputs and proves it synchronously.
107///
108/// This is useful when program execution has already happened elsewhere and only trace building
109/// plus proof generation remain. The execution settings are already reflected in the supplied
110/// `TraceBuildInputs`, so only proof-generation options remain in this API.
111#[instrument("prove_trace_sync", skip_all)]
112pub fn prove_from_trace_sync(
113    inputs: TraceProvingInputs,
114) -> Result<(StackOutputs, ExecutionProof), ExecutionError> {
115    let (trace_inputs, options) = inputs.into_parts();
116    let trace = build_trace(trace_inputs)?;
117    prove_execution_trace(trace, options)
118}
119
120fn prove_execution_trace(
121    trace: ExecutionTrace,
122    options: ProvingOptions,
123) -> Result<(StackOutputs, ExecutionProof), ExecutionError> {
124    tracing::event!(
125        tracing::Level::INFO,
126        "Generated execution trace of {} columns and {} steps (padded from {})",
127        miden_air::trace::TRACE_WIDTH,
128        trace.trace_len_summary().padded_trace_len(),
129        trace.trace_len_summary().trace_len()
130    );
131
132    let stack_outputs = *trace.stack_outputs();
133    let precompile_requests = trace.precompile_requests().to_vec();
134    let hash_fn = options.hash_fn();
135
136    // Extract public inputs before consuming the trace for the per-AIR matrices.
137    let (public_values, kernel_felts) = trace.public_inputs().to_air_inputs();
138
139    let (core_matrix, chiplets_matrix) = {
140        let _span = tracing::info_span!("to_core_chiplets_matrices").entered();
141        trace.into_core_chiplets_matrices()
142    };
143
144    let params = config::pcs_params();
145    let proof_bytes = match hash_fn {
146        HashFunction::Blake3_256 => {
147            let config = config::blake3_256_config(params);
148            prove_stark(&config, core_matrix, chiplets_matrix, &public_values, &kernel_felts)
149        },
150        HashFunction::Keccak => {
151            let config = config::keccak_config(params);
152            prove_stark(&config, core_matrix, chiplets_matrix, &public_values, &kernel_felts)
153        },
154        HashFunction::Rpo256 => {
155            let config = config::rpo_config(params);
156            prove_stark(&config, core_matrix, chiplets_matrix, &public_values, &kernel_felts)
157        },
158        HashFunction::Poseidon2 => {
159            let config = config::poseidon2_config(params);
160            prove_stark(&config, core_matrix, chiplets_matrix, &public_values, &kernel_felts)
161        },
162        HashFunction::Rpx256 => {
163            let config = config::rpx_config(params);
164            prove_stark(&config, core_matrix, chiplets_matrix, &public_values, &kernel_felts)
165        },
166    }?;
167
168    let proof = ExecutionProof::new(proof_bytes, hash_fn, precompile_requests);
169
170    Ok((stack_outputs, proof))
171}
172// STARK PROOF GENERATION
173// ================================================================================================
174
175/// Generates a multi-AIR STARK proof for the (Core, Chiplets) trace pair and public values.
176///
177/// Pre-seeds the challenger with the protocol parameters, public values, and the
178/// concatenated kernel-procedure digests (the only variable-length public input today,
179/// owned by the Chiplets AIR). Then delegates to the lifted multi-AIR prover.
180pub fn prove_stark<SC>(
181    config: &SC,
182    core_trace: RowMajorMatrix<Felt>,
183    chiplets_trace: RowMajorMatrix<Felt>,
184    public_values: &[Felt],
185    kernel_felts: &[Felt],
186) -> Result<Vec<u8>, ExecutionError>
187where
188    SC: StarkConfig<Felt, QuadFelt>,
189    <SC::Lmcs as Lmcs>::Commitment: Serialize,
190{
191    let mut challenger = config.challenger();
192    config::observe_protocol_params(&mut challenger);
193
194    // `air_inputs` are the fixed public values; `aux_inputs` are the kernel-procedure
195    // digests (the only variable-length public input today). The lifted prover absorbs
196    // both into Fiat-Shamir internally, along with the per-AIR trace heights.
197    let statement =
198        Statement::new(MidenMultiAir::new(), public_values.to_vec(), kernel_felts.to_vec())
199            .map_err(|e| ExecutionError::ProvingError(e.to_string()))?;
200    let prover_statement = ProverStatement::new(statement, vec![core_trace, chiplets_trace])
201        .map_err(|e| ExecutionError::ProvingError(e.to_string()))?;
202
203    let output: StarkOutput<Felt, QuadFelt, SC> =
204        ProverInstance::new(config, &prover_statement, None)
205            .map_err(|e| ExecutionError::ProvingError(e.to_string()))?
206            .prove(challenger)
207            .map_err(|e| ExecutionError::ProvingError(e.to_string()))?;
208
209    let proof_encoding_config = wincode::config::Configuration::default();
210    let proof_bytes =
211        <SerdeCompat<StarkProofData<Felt, QuadFelt, SC>> as wincode::config::Serialize<_>>::serialize(
212            &output.proof,
213            proof_encoding_config,
214        )
215        .map_err(|e| ExecutionError::ProvingError(e.to_string()))?;
216    Ok(proof_bytes)
217}
miden_prover/lib.rs

miden_prover/
lib.rs
