Miden prover

This crate proves post-execution witnesses produced by the Miden processor using Plonky3. The synchronous Prover does not execute programs: it consumes ExecutionWitness values and owned batches of portable PrecompileWitness values.

Usage

Prover is synchronous and consumes post-execution witnesses. Prover::prove(ExecutionWitness) proves the VM portion. Its PrecompileStatus is Empty when there is no deferred work, or Deferred with a portable singleton PrecompileWitness. Prover::prove_full(ExecutionWitness) proves the VM and any precompile work locally. Prover::prove_precompiles(Vec<PrecompileWitness>) imports a nonempty batch directly into one Session and returns one proof. Its root metadata preserves input order and repeated roots.

Use Prover::with_hash_fn to select the proof hash function.

Tracing must be selected before execution starts. Ordinary FastProcessor::execute* calls use a no-op tracer and return ExecutionOutput, which cannot be promoted to ExecutionWitness after the run because it contains no replay data. Call FastProcessor::execute_for_proving* when the result will be passed to Prover.

Deferred precompile workflow

use miden_prover::{ExecutionProof, PrecompileStatus, Prover};
use miden_verifier::Verifier;

// `witness` is an ExecutionWitness produced by FastProcessor.
let claim = witness.claim();
let prover = Prover::new();
let deferred = prover.prove(witness)?;

// Transport and decode the proof without a registry.
let bytes = deferred.to_bytes();
let proof = ExecutionProof::read_from_bytes(&bytes)?;
let PrecompileStatus::Deferred(precompile_witness) = proof.precompile_status() else {
    unreachable!("precompile proving is only needed for deferred proofs");
};

// Direct import checks the portable operations and assertions when proving begins.
let precompile_proof = prover.prove_precompiles(vec![precompile_witness.clone()])?;
let complete = proof.complete(precompile_proof)?;
let outcome = Verifier::new().verify(&claim, &complete)?;
assert!(outcome.is_complete());

To share precompile proving across several deferred proofs, collect their portable singleton witnesses in the required order and pass the vector to prove_precompiles once. Computations are shared inside proving; no merged portable witness is created. Attach the resulting PrecompileProof to each deferred proof with complete, then verify each completed proof. complete performs only the deferred-to-complete lifecycle transition; it does not check artifact compatibility.

Transport, direct import, structural validity, and fixed limits are specified in the deferred-proof semantics.

Recursive batch settlement

The batch settlement example verifies multiple Miden VM proofs and settles their deferred work with one precompile VM proof. It also proves the batcher itself, leaving no deferred work for the recipient. The MASM verification guide explains the claim list, ordered root fold, and host request.

Synchronous execution and proving

The FastProcessor-backed prove_sync(&Prover, ...) function is the direct synchronous path for executing and fully proving a program. When enabled in ExecutionOptions, it overlaps execution with hasher trace construction when a Rayon worker is available. A caller with no separate Rayon worker uses compact buffered replay. Proof generation remains configured on Prover.

STARK Backend

The prover uses Plonky3, a modular STARK proving framework. STARK configurations are defined in the miden-air crate and shared between the prover and verifier, ensuring consistency across the system.

Hash Function Selection

Different hash functions offer different tradeoffs:

BLAKE3 and Keccak provide faster proving, but they are not efficient for recursion. RPO256, Poseidon2, and RPX256 prove more slowly but support efficient recursive verification in Miden VM.

Crate features

Miden prover can be compiled with the following features:

The std feature is enabled by default and relies on the Rust standard library. The concurrent feature implies std and also enables multi-threaded proof generation. A no_std build does not rely on the Rust standard library and can compile to WebAssembly. Only the wasm32-unknown-unknown and wasm32-wasip1 targets are officially supported.

To compile with no_std, disable default features via --no-default-features flag.

Concurrent proof generation

When compiled with the concurrent feature enabled, the prover generates STARK proofs using multiple threads. For the benefits of concurrent proof generation, see these benchmarks.

Internally, we use rayon for parallel computations. Use the RAYON_NUM_THREADS environment variable to control the number of threads used to generate a STARK proof.

License

This project is dual-licensed under the MIT and Apache 2.0 licenses.