miden_prover/
prover.rs

1use alloc::{string::ToString, vec, vec::Vec};
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    /// portable singleton witness for later 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        Ok(ExecutionProof::new(vm, PrecompileStatus::Deferred(precompile_witness)))
72    }
73
74    /// Proves a complete execution witness entirely in memory.
75    ///
76    /// VM replay and direct precompile import consume the in-memory witness without serialization.
77    pub fn prove_full(&self, witness: ExecutionWitness) -> Result<ExecutionProof, ProverError> {
78        let (vm_witness, precompile_witness) = witness.into_parts();
79        let vm = self.prove_vm(vm_witness)?;
80        let precompile = precompile_witness
81            .map(|witness| self.prove_precompiles(vec![witness]))
82            .transpose()?;
83        let precompile = match precompile {
84            Some(precompile) => PrecompileStatus::Proven(precompile),
85            None => PrecompileStatus::Empty,
86        };
87        Ok(ExecutionProof::new(vm, precompile))
88    }
89
90    /// Proves a VM witness that does not authenticate deferred precompile work.
91    ///
92    /// The returned execution proof has an empty precompile status. Use [`Self::prove`] or
93    /// [`Self::prove_full`] when the original execution witness contains precompile work.
94    pub fn prove_vm_witness(&self, witness: VmWitness) -> Result<ExecutionProof, ProverError> {
95        if witness.has_precompiles() {
96            return Err(ProverError::VmWitnessHasPrecompiles);
97        }
98
99        let vm = self.prove_vm(witness)?;
100        Ok(ExecutionProof::new(vm, PrecompileStatus::Empty))
101    }
102
103    /// Materializes and proves the VM trace represented by `witness`.
104    fn prove_vm(&self, witness: VmWitness) -> Result<VmProof, ProverError> {
105        let trace = {
106            let _span = tracing::info_span!("build_miden_vm_trace").entered();
107            build_trace_with_budget(witness, self.max_prover_memory_bytes)
108                .map_err(ProverError::TraceGeneration)?
109        };
110
111        self.prove_vm_trace(trace)
112    }
113
114    /// Proves an owned batch of singleton execution obligations in one STARK.
115    ///
116    /// The proof preserves the input roots in order, including repeated roots. An empty batch
117    /// is rejected. Single-execution proving uses this same path with a one-element vector.
118    ///
119    /// Batch-wide limits are checked during import, before STARK generation. Individually valid
120    /// witnesses may exceed these limits when combined. Input accounting counts each supplied
121    /// occurrence before sharing computations, including repeated data across witnesses.
122    pub fn prove_precompiles(
123        &self,
124        witnesses: Vec<PrecompileWitness>,
125    ) -> Result<PrecompileProof, ProverError> {
126        miden_precompiles_prover::prove_precompiles(witnesses, self.hash_fn)
127            .map_err(ProverError::PrecompileProofGeneration)
128    }
129
130    #[cfg(feature = "std")]
131    fn prove_full_trace(
132        &self,
133        trace: VmTrace,
134        precompile: Option<PrecompileWitness>,
135    ) -> Result<ExecutionProof, ProverError> {
136        let vm = self.prove_vm_trace(trace)?;
137        let precompile =
138            precompile.map(|witness| self.prove_precompiles(vec![witness])).transpose()?;
139        let precompile = match precompile {
140            Some(precompile) => PrecompileStatus::Proven(precompile),
141            None => PrecompileStatus::Empty,
142        };
143        Ok(ExecutionProof::new(vm, precompile))
144    }
145
146    /// Proves a fully materialized VM trace.
147    ///
148    /// Buffered and overlapped trace construction share this private implementation so STARK
149    /// generation and VM proof packaging cannot diverge.
150    #[tracing::instrument(name = "miden_vm", skip_all)]
151    fn prove_vm_trace(&self, trace: VmTrace) -> Result<VmProof, ProverError> {
152        let trace_len_summary = trace.trace_len_summary();
153        let params = config::pcs_params();
154        tracing::event!(
155            tracing::Level::INFO,
156            "Generated execution traces: core={}, range={}, chiplets={}, poseidon2={}, padded={}, \
157             estimated_prover_memory_bytes={:?}",
158            trace_len_summary.core_trace_len(),
159            trace_len_summary.range_trace_len(),
160            trace_len_summary.chiplets_trace_len().trace_len(),
161            trace_len_summary.poseidon2_permutation_trace_len(),
162            trace_len_summary.padded_trace_len(),
163            trace_len_summary.prover_memory_bytes(&params)
164        );
165
166        let precompile_root = trace.precompile_root();
167        let (public_values, aux_inputs) = trace.public_inputs().to_air_inputs();
168        let (core_matrix, chiplets_matrix, poseidon2_matrix) = trace.into_air_matrices();
169
170        let proof_bytes = match self.hash_fn {
171            HashFunction::Blake3_256 => {
172                let config = config::blake3_256_config(params, config::RELATION_DIGEST);
173                prove_stark(
174                    &config,
175                    core_matrix,
176                    chiplets_matrix,
177                    poseidon2_matrix,
178                    &public_values,
179                    &aux_inputs,
180                )
181            },
182            HashFunction::Keccak => {
183                let config = config::keccak_config(params, config::RELATION_DIGEST);
184                prove_stark(
185                    &config,
186                    core_matrix,
187                    chiplets_matrix,
188                    poseidon2_matrix,
189                    &public_values,
190                    &aux_inputs,
191                )
192            },
193            HashFunction::Rpo256 => {
194                let config = config::rpo_config(params, config::RELATION_DIGEST);
195                prove_stark(
196                    &config,
197                    core_matrix,
198                    chiplets_matrix,
199                    poseidon2_matrix,
200                    &public_values,
201                    &aux_inputs,
202                )
203            },
204            HashFunction::Poseidon2 => {
205                let config = config::poseidon2_config(params, config::RELATION_DIGEST);
206                prove_stark(
207                    &config,
208                    core_matrix,
209                    chiplets_matrix,
210                    poseidon2_matrix,
211                    &public_values,
212                    &aux_inputs,
213                )
214            },
215            HashFunction::Rpx256 => {
216                let config = config::rpx_config(params, config::RELATION_DIGEST);
217                prove_stark(
218                    &config,
219                    core_matrix,
220                    chiplets_matrix,
221                    poseidon2_matrix,
222                    &public_values,
223                    &aux_inputs,
224                )
225            },
226        }
227        .map_err(ProverError::VmProofGeneration)?;
228
229        let proof = miden_core::proof::StarkProof::new(proof_bytes, self.hash_fn);
230        Ok(VmProof { proof, precompile_root })
231    }
232}
233
234/// Executes and fully proves a program synchronously.
235///
236/// This FastProcessor-backed orchestration function preserves the optimized overlapped
237/// execution/trace-building path. Proving policy belongs on [`Prover`].
238///
239/// When enabled in `execution_options`, the processor may build the hasher chiplet alongside
240/// execution. A caller with no separate Rayon worker uses compact buffered replay. Both cases use
241/// the same private VM STARK and complete-local packaging implementation.
242#[tracing::instrument(name = "prove_program_sync", skip_all)]
243pub fn prove_sync(
244    prover: &Prover,
245    program: &Program,
246    stack_inputs: StackInputs,
247    advice_inputs: AdviceInputs,
248    host: &mut impl SyncHost,
249    execution_options: ExecutionOptions,
250) -> Result<(StackOutputs, ExecutionProof), ExecutionError> {
251    #[cfg(feature = "std")]
252    let overlapped_trace_build = execution_options.overlapped_trace_build();
253    let processor = FastProcessor::new_with_options(stack_inputs, advice_inputs, execution_options)
254        .map_err(ExecutionError::advice_error_no_context)?;
255
256    #[cfg(feature = "std")]
257    if overlapped_trace_build {
258        let (trace, precompile) = {
259            let _span = tracing::info_span!("execute_miden_vm").entered();
260            processor.execute_and_build_trace_sync(
261                program,
262                host,
263                prover.max_prover_memory_bytes(),
264            )?
265        };
266        let stack_outputs = *trace.stack_outputs();
267        let proof = prover
268            .prove_full_trace(trace, precompile)
269            .map_err(ProverError::into_execution_error)?;
270        return Ok((stack_outputs, proof));
271    }
272
273    let witness = {
274        let _span = tracing::info_span!("execute_miden_vm").entered();
275        processor.execute_for_proving_sync(program, host)?
276    };
277    let stack_outputs = *witness.claim().stack_outputs();
278    let proof = prover.prove_full(witness).map_err(ProverError::into_execution_error)?;
279    Ok((stack_outputs, proof))
280}
281
282impl Default for Prover {
283    fn default() -> Self {
284        Self::new()
285    }
286}
287
288/// Errors produced while proving post-execution witnesses.
289#[derive(Debug, thiserror::Error)]
290#[non_exhaustive]
291pub enum ProverError {
292    /// The VM witness authenticates deferred precompile work that this proving path cannot carry.
293    #[error("VM witness contains deferred precompile work")]
294    VmWitnessHasPrecompiles,
295    /// The processor witness could not be materialized into a valid execution trace.
296    #[error("failed to materialize VM execution trace: {0}")]
297    TraceGeneration(#[source] ExecutionError),
298    /// The materialized VM trace could not be proved.
299    #[error("failed to prove VM execution trace: {0}")]
300    VmProofGeneration(#[source] ExecutionError),
301    /// The deferred precompile witness could not be proved.
302    #[error("failed to prove precompile witness: {0}")]
303    PrecompileProofGeneration(#[source] miden_precompiles_prover::PrecompileProvingError),
304}
305
306impl ProverError {
307    fn into_execution_error(self) -> ExecutionError {
308        match self {
309            Self::VmWitnessHasPrecompiles => ExecutionError::ProvingError(self.to_string()),
310            Self::TraceGeneration(error) | Self::VmProofGeneration(error) => error,
311            Self::PrecompileProofGeneration(error) => {
312                ExecutionError::ProvingError(error.to_string())
313            },
314        }
315    }
316}
317
318#[cfg(test)]
319mod tests {
320    use super::*;
321
322    #[test]
323    fn prover_uses_canonical_default_and_allows_hash_override() {
324        let prover = Prover::new();
325        assert_eq!(prover.hash_fn, HashFunction::Blake3_256);
326
327        let prover = prover.with_hash_fn(HashFunction::Poseidon2);
328        assert_eq!(prover.hash_fn, HashFunction::Poseidon2);
329    }
330
331    #[test]
332    fn prover_uses_canonical_memory_budget_and_allows_override() {
333        let prover = Prover::new();
334        assert_eq!(prover.max_prover_memory_bytes(), Prover::DEFAULT_MAX_PROVER_MEMORY_BYTES);
335
336        let prover = prover.with_max_prover_memory_bytes(1 << 20);
337        assert_eq!(prover.max_prover_memory_bytes(), 1 << 20);
338    }
339}
miden_prover/prover.rs

miden_prover/
prover.rs
