Skip to main content

miden_prover/
prover.rs

1use alloc::string::ToString;
2
3use miden_core::proof::{ExecutionProof, HashFunction, PrecompileProof, PrecompileStatus, VmProof};
4use miden_processor::{
5    ExecutionError, ExecutionOptions, ExecutionWitness, FastProcessor, PrecompileWitness, Program,
6    StackInputs, StackOutputs, SyncHost, VmWitness,
7    advice::AdviceInputs,
8    trace::{self, VmTrace, build_trace_with_budget},
9};
10
11use crate::{config, prove_stark};
12
13/// A synchronous, configurable prover for post-execution Miden VM witnesses.
14///
15/// This type does not execute programs. It owns proof-generation policy — including the memory
16/// budget for materializing a VM execution trace — and consumes witnesses produced by the
17/// processor.
18#[derive(Debug, Clone, Eq, PartialEq)]
19pub struct Prover {
20    hash_fn: HashFunction,
21    max_prover_memory_bytes: u64,
22}
23
24impl Prover {
25    /// Default maximum memory, in bytes, this prover is permitted to allocate for a proof over a
26    /// VM execution trace.
27    ///
28    /// This bounds only the lifted-STARK Miden VM proof modelled by `miden_air::memory`; it does
29    /// not cover the precompile prover's memory footprint.
30    pub const DEFAULT_MAX_PROVER_MEMORY_BYTES: u64 = trace::DEFAULT_MAX_PROVER_MEMORY_BYTES;
31
32    /// Creates a prover with the canonical proof-generation configuration.
33    pub const fn new() -> Self {
34        Self {
35            hash_fn: HashFunction::Blake3_256,
36            max_prover_memory_bytes: Self::DEFAULT_MAX_PROVER_MEMORY_BYTES,
37        }
38    }
39
40    /// Sets the hash function used for proofs generated by this prover.
41    #[must_use]
42    pub const fn with_hash_fn(mut self, hash_fn: HashFunction) -> Self {
43        self.hash_fn = hash_fn;
44        self
45    }
46
47    /// Sets the maximum memory, in bytes, this prover is permitted to allocate for a proof over a
48    /// VM execution trace.
49    #[must_use]
50    pub const fn with_max_prover_memory_bytes(mut self, max_prover_memory_bytes: u64) -> Self {
51        self.max_prover_memory_bytes = max_prover_memory_bytes;
52        self
53    }
54
55    /// Returns the maximum memory, in bytes, this prover is permitted to allocate for a proof
56    /// over a VM execution trace.
57    pub const fn max_prover_memory_bytes(&self) -> u64 {
58        self.max_prover_memory_bytes
59    }
60
61    /// Proves only the VM portion of an execution witness.
62    ///
63    /// If the execution authenticated deferred precompile work, the returned proof carries its
64    /// passive singleton wire for later hydration and proving. Otherwise, it is complete.
65    pub fn prove(&self, witness: ExecutionWitness) -> Result<ExecutionProof, ProverError> {
66        let (vm_witness, precompile_witness) = witness.into_parts();
67        let vm = self.prove_vm(vm_witness)?;
68        let Some(precompile_witness) = precompile_witness else {
69            return Ok(ExecutionProof::new(vm, PrecompileStatus::Empty));
70        };
71        let precompile = precompile_witness
72            .state()
73            .to_wire()
74            .expect("execution witness state must have canonical deferred wire");
75        Ok(ExecutionProof::new(vm, PrecompileStatus::Deferred(precompile)))
76    }
77
78    /// Proves a complete execution witness entirely in memory.
79    ///
80    /// Both VM and precompile proving consume the hydrated witness directly; the witness is not
81    /// serialized on this local path.
82    pub fn prove_full(&self, witness: ExecutionWitness) -> Result<ExecutionProof, ProverError> {
83        let (vm_witness, precompile_witness) = witness.into_parts();
84        let vm = self.prove_vm(vm_witness)?;
85        let precompile = precompile_witness
86            .as_ref()
87            .map(|witness| self.prove_precompile(witness))
88            .transpose()?;
89        let precompile = match precompile {
90            Some(precompile) => PrecompileStatus::Proven(precompile),
91            None => PrecompileStatus::Empty,
92        };
93        Ok(ExecutionProof::new(vm, precompile))
94    }
95
96    /// Materializes and proves the VM trace represented by `witness`.
97    fn prove_vm(&self, witness: VmWitness) -> Result<VmProof, ProverError> {
98        let trace = {
99            let _span = tracing::info_span!("build_miden_vm_trace").entered();
100            build_trace_with_budget(witness, self.max_prover_memory_bytes)
101                .map_err(ProverError::TraceGeneration)?
102        };
103
104        self.prove_vm_trace(trace)
105    }
106
107    /// Proves one singleton or merged precompile witness without consuming its hydrated DAG.
108    pub fn prove_precompile(
109        &self,
110        witness: &PrecompileWitness,
111    ) -> Result<PrecompileProof, ProverError> {
112        let proof = miden_precompiles_prover::prove_deferred_state(witness.state(), self.hash_fn)
113            .map_err(ProverError::PrecompileProofGeneration)?;
114        Ok(PrecompileProof { proof, roots: witness.roots().to_vec() })
115    }
116
117    #[cfg(feature = "std")]
118    fn prove_full_trace(
119        &self,
120        trace: VmTrace,
121        precompile: Option<&PrecompileWitness>,
122    ) -> Result<ExecutionProof, ProverError> {
123        let vm = self.prove_vm_trace(trace)?;
124        let precompile = precompile.map(|witness| self.prove_precompile(witness)).transpose()?;
125        let precompile = match precompile {
126            Some(precompile) => PrecompileStatus::Proven(precompile),
127            None => PrecompileStatus::Empty,
128        };
129        Ok(ExecutionProof::new(vm, precompile))
130    }
131
132    /// Proves a fully materialized VM trace.
133    ///
134    /// Buffered and overlapped trace construction share this private implementation so STARK
135    /// generation and VM proof packaging cannot diverge.
136    #[tracing::instrument(name = "miden_vm", skip_all)]
137    fn prove_vm_trace(&self, trace: VmTrace) -> Result<VmProof, ProverError> {
138        let trace_len_summary = trace.trace_len_summary();
139        let params = config::pcs_params();
140        tracing::event!(
141            tracing::Level::INFO,
142            "Generated execution traces: core={}, range={}, chiplets={}, poseidon2={}, padded={}, \
143             estimated_prover_memory_bytes={:?}",
144            trace_len_summary.core_trace_len(),
145            trace_len_summary.range_trace_len(),
146            trace_len_summary.chiplets_trace_len().trace_len(),
147            trace_len_summary.poseidon2_permutation_trace_len(),
148            trace_len_summary.padded_trace_len(),
149            trace_len_summary.prover_memory_bytes(&params)
150        );
151
152        let precompile_root = trace.precompile_root();
153        let (public_values, aux_inputs) = trace.public_inputs().to_air_inputs();
154        let (core_matrix, chiplets_matrix, poseidon2_matrix) = trace.into_air_matrices();
155
156        let proof_bytes = match self.hash_fn {
157            HashFunction::Blake3_256 => {
158                let config = config::blake3_256_config(params, config::RELATION_DIGEST);
159                prove_stark(
160                    &config,
161                    core_matrix,
162                    chiplets_matrix,
163                    poseidon2_matrix,
164                    &public_values,
165                    &aux_inputs,
166                )
167            },
168            HashFunction::Keccak => {
169                let config = config::keccak_config(params, config::RELATION_DIGEST);
170                prove_stark(
171                    &config,
172                    core_matrix,
173                    chiplets_matrix,
174                    poseidon2_matrix,
175                    &public_values,
176                    &aux_inputs,
177                )
178            },
179            HashFunction::Rpo256 => {
180                let config = config::rpo_config(params, config::RELATION_DIGEST);
181                prove_stark(
182                    &config,
183                    core_matrix,
184                    chiplets_matrix,
185                    poseidon2_matrix,
186                    &public_values,
187                    &aux_inputs,
188                )
189            },
190            HashFunction::Poseidon2 => {
191                let config = config::poseidon2_config(params, config::RELATION_DIGEST);
192                prove_stark(
193                    &config,
194                    core_matrix,
195                    chiplets_matrix,
196                    poseidon2_matrix,
197                    &public_values,
198                    &aux_inputs,
199                )
200            },
201            HashFunction::Rpx256 => {
202                let config = config::rpx_config(params, config::RELATION_DIGEST);
203                prove_stark(
204                    &config,
205                    core_matrix,
206                    chiplets_matrix,
207                    poseidon2_matrix,
208                    &public_values,
209                    &aux_inputs,
210                )
211            },
212        }
213        .map_err(ProverError::VmProofGeneration)?;
214
215        let proof = miden_core::proof::StarkProof::new(proof_bytes, self.hash_fn);
216        Ok(VmProof { proof, precompile_root })
217    }
218}
219
220/// Executes and fully proves a program synchronously.
221///
222/// This FastProcessor-backed orchestration function preserves the optimized overlapped
223/// execution/trace-building path. Proving policy belongs on [`Prover`].
224///
225/// When enabled in `execution_options`, the processor may build the hasher chiplet alongside
226/// execution. A caller with no separate Rayon worker uses compact buffered replay. Both cases use
227/// the same private VM STARK and complete-local packaging implementation.
228#[tracing::instrument(name = "prove_program_sync", skip_all)]
229pub fn prove_sync(
230    prover: &Prover,
231    program: &Program,
232    stack_inputs: StackInputs,
233    advice_inputs: AdviceInputs,
234    host: &mut impl SyncHost,
235    execution_options: ExecutionOptions,
236) -> Result<(StackOutputs, ExecutionProof), ExecutionError> {
237    #[cfg(feature = "std")]
238    let overlapped_trace_build = execution_options.overlapped_trace_build();
239    let processor = FastProcessor::new_with_options(stack_inputs, advice_inputs, execution_options)
240        .map_err(ExecutionError::advice_error_no_context)?;
241
242    #[cfg(feature = "std")]
243    if overlapped_trace_build {
244        let (trace, precompile) = {
245            let _span = tracing::info_span!("execute_miden_vm").entered();
246            processor.execute_and_build_trace_sync(
247                program,
248                host,
249                prover.max_prover_memory_bytes(),
250            )?
251        };
252        let stack_outputs = *trace.stack_outputs();
253        let proof = prover
254            .prove_full_trace(trace, precompile.as_ref())
255            .map_err(ProverError::into_execution_error)?;
256        return Ok((stack_outputs, proof));
257    }
258
259    let witness = {
260        let _span = tracing::info_span!("execute_miden_vm").entered();
261        processor.execute_for_proving_sync(program, host)?
262    };
263    let stack_outputs = *witness.claim().stack_outputs();
264    let proof = prover.prove_full(witness).map_err(ProverError::into_execution_error)?;
265    Ok((stack_outputs, proof))
266}
267
268impl Default for Prover {
269    fn default() -> Self {
270        Self::new()
271    }
272}
273
274/// Errors produced while proving post-execution witnesses.
275#[derive(Debug, thiserror::Error)]
276#[non_exhaustive]
277pub enum ProverError {
278    /// The processor witness could not be materialized into a valid execution trace.
279    #[error("failed to materialize VM execution trace: {0}")]
280    TraceGeneration(#[source] ExecutionError),
281    /// The materialized VM trace could not be proved.
282    #[error("failed to prove VM execution trace: {0}")]
283    VmProofGeneration(#[source] ExecutionError),
284    /// The deferred precompile witness could not be proved.
285    #[error("failed to prove precompile witness: {0}")]
286    PrecompileProofGeneration(#[source] miden_precompiles_prover::ProveDeferredStateError),
287}
288
289impl ProverError {
290    fn into_execution_error(self) -> ExecutionError {
291        match self {
292            Self::TraceGeneration(error) | Self::VmProofGeneration(error) => error,
293            Self::PrecompileProofGeneration(error) => {
294                ExecutionError::ProvingError(error.to_string())
295            },
296        }
297    }
298}
299
300#[cfg(test)]
301mod tests {
302    use super::*;
303
304    #[test]
305    fn prover_uses_canonical_default_and_allows_hash_override() {
306        let prover = Prover::new();
307        assert_eq!(prover.hash_fn, HashFunction::Blake3_256);
308
309        let prover = prover.with_hash_fn(HashFunction::Poseidon2);
310        assert_eq!(prover.hash_fn, HashFunction::Poseidon2);
311    }
312
313    #[test]
314    fn prover_uses_canonical_memory_budget_and_allows_override() {
315        let prover = Prover::new();
316        assert_eq!(prover.max_prover_memory_bytes(), Prover::DEFAULT_MAX_PROVER_MEMORY_BYTES);
317
318        let prover = prover.with_max_prover_memory_bytes(1 << 20);
319        assert_eq!(prover.max_prover_memory_bytes(), 1 << 20);
320    }
321}