Miden prover

This crate contains the Miden VM prover, which proves correct execution of Miden VM. Internally, the prover uses Miden processor to execute the programs, and then relies on the Winterfell prover to generate STARK proofs.

Usage

This crate exposes a prove() function which can be used to execute Miden VM programs and generate proofs of their execution. The function takes the following parameters:

• program: &Program - a reference to a Miden program to be executed.
• stack_inputs: StackInputs - a set of public inputs with which to execute the program.
• host: Host - an instance of a Host which can be used to supply non-deterministic inputs to the VM and receive messages from the VM.
• options: &ProvingOptions - config parameters for proof generation. The default options target 96-bit security level.

If the program is executed successfully, the function returns a tuple with 2 elements:

• outputs: StackOutputs - the outputs generated by the program.
• proof: ExecutionProof - proof of program execution. ExecutionProof can be easily serialized and deserialized using to_bytes() and from_bytes() functions respectively.

Proof generation example

Here is a simple example of executing a program which pushes two numbers onto the stack and computes their sum:

use miden_assembly::Assembler;
use miden_prover::{prove, ProvingOptions, StackInputs, DefaultHost};

// instantiate the assembler
let assembler = Assembler::default();

// this is our program, we compile it from assembly code
let program = assembler.compile("begin push.3 push.5 add end").unwrap();

// let's execute it and generate a STARK proof
let (outputs, proof) = prove(
    &program,
    StackInputs::default(),       // we won't provide any stack inputs
    &mut DefaultHost::default(),  // we'll be using a default host
    &ProvingOptions::default(),   // we'll be using default options
)
.unwrap();

// the output should be 8
assert_eq!(8, outputs.first().unwrap().as_int());

Crate features

Miden prover can be compiled with the following features:

• std - enabled by default and relies on the Rust standard library.
• concurrent - implies std and also enables multi-threaded proof generation.
• metal - enables Metal-based acceleration of proof generation (for recursive proofs) on supported platforms (e.g., Apple silicon).
• no_std does not rely on the Rust standard library and enables compilation 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 concurrent feature enabled, the prover will generate STARK proofs using multiple threads. For benefits of concurrent proof generation check out these benchmarks.

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

License

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