Crate miden_vm

Expand description

§Miden VM

This crate aggregates all components of the Miden VM in a single place. Specifically, it re-exports functionality from processor, prover, and verifier crates. Additionally, when compiled as an executable, this crate can be used via a CLI interface to execute Miden VM programs and to verify correctness of their execution.

§Basic concepts

An in-depth description of Miden VM is available in the full Miden VM documentation. In this section we cover only the basics to make the included examples easier to understand.

§Writing programs

Our goal is to make Miden VM an easy compilation target for high-level languages such as Rust, Move, Sway, and others. We believe it is important to let people write programs in the languages of their choice. However, compilers to help with this have not been developed yet. Thus, for now, the primary way to write programs for Miden VM is to use Miden assembly.

Miden assembler compiles assembly source code in a program MAST, which is represented by a Program struct. It is possible to construct a Program struct manually, but we don’t recommend this approach because it is tedious, error-prone, and requires an in-depth understanding of VM internals. All examples throughout these docs use assembly syntax.

§Program hash

All Miden programs can be reduced to a single 32-byte value, called program hash. Once a Program object is constructed, you can access this hash via Program::hash() method. This hash value is used by a verifier when they verify program execution. This ensures that the verifier verifies execution of a specific program (e.g. a program which the prover had committed to previously). The methodology for computing program hash is described here.

§Inputs / outputs

Currently, there are 3 ways to get values onto the stack:

You can use push instruction to push values onto the stack. These values become a part of the program itself, and, therefore, cannot be changed between program executions. You can think of them as constants.
The stack can be initialized to some set of values at the beginning of the program. These inputs are public and must be shared with the verifier for them to verify a proof of the correct execution of a Miden program. At most 16 values could be provided for the stack initialization, attempts to provide more than 16 values will cause an error.
The program may request nondeterministic advice inputs from the prover. These inputs are secret inputs. This means that the prover does not need to share them with the verifier. There are three types of advice inputs: (1) a single advice stack which can contain any number of elements; (2) a key-mapped element lists which can be pushed onto the advice stack; (3) a Merkle store, which is used to provide nondeterministic inputs for instructions which work with Merkle trees. There are no restrictions on the number of advice inputs a program can request.

The stack is provided to Miden VM via StackInputs struct. These are public inputs of the execution, and should also be provided to the verifier. The secret inputs for the program are provided via the Host interface. The default implementation of the host relies on in-memory advice provider (AdviceProvider) that can be commonly used for operations that won’t require persistence.

Values remaining on the stack after a program is executed can be returned as stack outputs. You can specify exactly how many values (from the top of the stack) should be returned. Notice, that, similar to stack inputs, at most 16 values can be returned via the stack. Attempts to return more than 16 values will cause an error.

Having a small number elements to describe public inputs and outputs of a program may seem limiting, however, just 4 elements are sufficient to represent a root of a Merkle tree or a sequential hash of elements. Both of these can be expanded into an arbitrary number of values by supplying the actual values non-deterministically via the host interface.

§Usage

Miden crate exposes several functions which can be used to execute programs, generate proofs of their correct execution, and verify the generated proofs. How to do this is explained below, but you can also take a look at working examples here and find instructions for running them via CLI here.

§Executing programs

To execute a program on Miden VM, you can use execute(). The sync execute_sync() variant is also available for sync callers. These functions take the following arguments:

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.
advice_inputs: AdviceInputs - the private inputs used to build the advice provider; use AdviceInputs::default() when no private inputs are needed.
host - an instance of Host for execute() or SyncHost for execute_sync(), used to supply non-deterministic inputs to the VM and receive messages from the VM.
options: ExecutionOptions - a set of options for executing the specified program (e.g., max allowed number of cycles).

The function returns a Result<ExecutionOutput, ExecutionError> which will contain the final stack state and other execution outputs if the execution was successful, or an error if the execution failed. If you need an execution trace, use FastProcessor::execute_trace_inputs() / FastProcessor::execute_trace_inputs_sync() and pass the returned TraceBuildInputs bundle to trace::build_trace().

For example:

use miden_vm::{
    advice::AdviceInputs,
    Assembler, execute_sync, ExecutionOptions, DefaultHost, StackInputs
};

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

// compile Miden assembly source code into a program
let program = assembler.assemble_program(
    "prg",
    "begin push.3 push.5 add swap drop end",
).unwrap();

// use an empty list as initial stack
let stack_inputs = StackInputs::default();

// do not include any initial advice data
let advice_inputs = AdviceInputs::default();

// instantiate a default host (with an empty advice provider)
let mut host = DefaultHost::default();

// instantiate default execution options
let exec_options = ExecutionOptions::default();

// execute the program with no inputs
let output =
    execute_sync(&program.unwrap_program(), stack_inputs, advice_inputs.clone(), &mut host, exec_options).unwrap();

§Proving program execution

To execute a program on Miden VM and generate a proof that the program was executed correctly, you can use the prove_sync() function. The async prove() variant is also available for async callers. prove_sync() takes the following arguments:

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.
advice_inputs: AdviceInputs - the initial nondeterministic inputs available to the VM.
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.
execution_options: ExecutionOptions - VM execution parameters such as cycle limits and trace fragmentation.
options: ProvingOptions - proof-generation parameters. 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_vm::{
    advice::AdviceInputs,
    field::PrimeField64,
    Assembler, DefaultHost, ExecutionOptions, ProvingOptions, prove_sync, StackInputs
};

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

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

// let's execute it and generate a STARK proof
let (outputs, proof) = prove_sync(
    &program.unwrap_program(),
    StackInputs::default(),       // we won't provide any inputs
    AdviceInputs::default(),      // we don't need any initial advice inputs
    &mut DefaultHost::default(),  // we'll be using a default host
    ExecutionOptions::default(),  // we'll use default VM execution options
    ProvingOptions::default(),    // we'll be using default options
)
.unwrap();

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

§Verifying program execution

To verify program execution, use Verifier::new().verify(...). The verifier takes the following parameters:

proof: ExecutionProof - the proof generated during program execution.
claim: ExecutionClaim - the claimed program information, stack inputs, and stack outputs.

Stack inputs are expected to be ordered as if they would be pushed onto the stack one by one. Thus, their expected order on the stack will be the reverse of the order in which they are provided, and the last value in the stack_inputs is expected to be the value at the top of the stack.

Stack outputs are expected to be ordered as if they would be popped off the stack one by one. Thus, the value at the top of the stack is expected to be in the first position of the stack_outputs, and the order of the rest of the output elements will also match the order on the stack. This is the reverse of the order of the stack_inputs.

The verifier returns Result<u32, VerificationError> which will be Ok(security_level) if verification passes, or Err(VerificationError) if verification fails, with VerificationError describing the reason for the failure.

If a program with the provided hash is executed against some secret inputs and the provided public inputs, it will produce the provided outputs.

Notice how the verifier needs to know only the hash of the program - not what the actual program was.

§Proof verification example

Here is a simple example of verifying execution of the program from the previous example:

use miden_vm::{ExecutionClaim, ProgramInfo, StackInputs, StackOutputs, Verifier, field::Felt};

let program =   /* value from previous example */;
let proof =     /* value from previous example */;
let expected_outputs = StackOutputs::new(&[Felt::new(8).unwrap()]).unwrap();
let claim = ExecutionClaim::from_program_info(
    ProgramInfo::from(program),
    StackInputs::default(),
    expected_outputs,
);

// Verify the execution claim.
match Verifier::new().verify(proof, claim) {
    Ok(_) => println!("Execution verified!"),
    Err(err) => eprintln!("Verification failed: {err}"),
}

§Fibonacci calculator

Let’s write a simple program for Miden VM (using Miden assembly). Our program will compute the 5-th Fibonacci number:

push.0      // stack state: 0
push.1      // stack state: 1 0
swap        // stack state: 0 1
dup.1       // stack state: 1 0 1
add         // stack state: 1 1
swap        // stack state: 1 1
dup.1       // stack state: 1 1 1
add         // stack state: 2 1
swap        // stack state: 1 2
dup.1       // stack state: 2 1 2
add         // stack state: 3 2

Notice that except for the first 2 operations which initialize the stack, the sequence of swap dup.1 add operations repeats over and over. In fact, we can repeat these operations an arbitrary number of times to compute an arbitrary Fibonacci number. In Rust, it would look like this:

use miden_vm::{
    advice::AdviceInputs,
    field::PrimeField64,
    Assembler, DefaultHost, ProvingOptions, StackInputs
};

// set the number of terms to compute
let n = 50;

// instantiate the default assembler and compile the program
let source = format!(
    "
    begin
        repeat.{}
            swap dup.1 add
        end
    end",
    n - 1
);
let assembler = Assembler::default();
let program = assembler.assemble_program("prg", &source).unwrap();

// initialize a default host (with an empty advice provider)
let mut host = DefaultHost::default();

// initialize the stack with values 0 and 1
let stack_inputs = StackInputs::try_from_ints([1, 0]).unwrap();

// execute the program
let (outputs, proof) = miden_vm::prove_sync(
    &program.unwrap_program(),
    stack_inputs,
    AdviceInputs::default(), // without initial advice inputs
    &mut host,
    miden_vm::ExecutionOptions::default(), // use default VM execution options
    ProvingOptions::default(), // use default proving options
)
.unwrap();

// fetch the stack outputs, truncating to the first element
let stack = outputs.get_num_elements(1);

// the output should be the 50th Fibonacci number
assert_eq!(12586269025, stack[0].as_canonical_u64());

Above, we used public inputs to initialize the stack rather than using push operations. This makes the program a bit simpler, and also allows us to run the program from arbitrary starting points without changing program hash.

§CLI interface

If you want to execute, prove, and verify programs on Miden VM, but don’t want to write Rust code, you can use Miden CLI. It also contains a number of useful tools to help analyze and debug programs.

§Compiling Miden VM

First, make sure you have Rust installed. The current version of Miden VM requires Rust version 1.96 or later.

Then, to compile Miden VM into a binary, run the following make command:

make exec

This will place miden-vm executable in the ./target/optimized directory.

By default, the executable will be compiled in the multi-threaded mode. If you would like to enable single-threaded proof generation, you can compile Miden VM using the following command:

make exec-single

We also provide a number of make commands to simplify building Miden VM for various targets:

# build an executable for a generic target (concurrent)
make exec

# build an executable for targets with AVX2 instructions (concurrent)
make exec-avx2

# build an executable for targets with SVE instructions (concurrent)
make exec-sve

# build an executable with log tree enabled
make exec-info

§Running Miden VM

Once the executable has been compiled, you can run Miden VM like so:

./target/optimized/miden-vm [subcommand] [parameters]

Currently, Miden VM can be executed with the following subcommands:

run - this will execute a Miden assembly program and output the result, but will not generate a proof of execution.
prove - this will execute a Miden assembly program, and will also generate a STARK proof of execution.
verify - this will verify a previously generated proof of execution for a given program.
compile - this will compile a Miden assembly program and outputs stats about the compilation process.
debug - this will instantiate a CLI debugger against the specified Miden assembly program and inputs.
analyze - this will run a Miden assembly program against specific inputs and will output stats about its execution.

All of the above subcommands require various parameters to be provided. To get more detailed help on what is needed for a given subcommand, you can run the following:

./target/optimized/miden-vm [subcommand] --help

For example:

./target/optimized/miden-vm prove --help

§Fibonacci example

In the miden-vm/masm-examples/fib directory, we provide a very simple Fibonacci calculator example. This example computes the 1000th term of the Fibonacci sequence. You can execute this example on Miden VM like so:

./target/optimized/miden-vm run miden-vm/masm-examples/fib/fib.masm -n 1

This will run the example code to completion and will output the top element remaining on the stack.

§Crate features

Miden VM 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.
executable - required for building Miden VM binary as described above. Implies std.
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 VM 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.

Re-exports§

pub use miden_assembly as assembly;
pub use miden_assembly::diagnostics;

Modules§

advice
crypto
field
serde
trace
utils

Structs§

Assembler: The Assembler produces a Merkelized Abstract Syntax Tree (MAST) from Miden Assembly sources, as a Package artifact. In general, packages come in three primary varieties:
DefaultHost: A default SyncHost implementation that provides the essential functionality required by the VM.
ExecutionClaim: The external statement a Miden VM proof attests: the program root and kernel identify the executed code and its syscall authorization set; the stack inputs and outputs are the execution’s public I/O.
ExecutionOptions: A set of parameters specifying execution parameters of the VM.
ExecutionOutput: The output of a program execution, containing the state of the stack, advice provider, memory, and final deferred state at the end of execution.
ExecutionProof: A proof of correct execution of Miden VM.
ExecutionTrace: Execution trace which is generated when a program is executed on the VM.
FastProcessor: A fast processor which doesn’t generate any trace.
KernelDescriptor: A list of exported kernel procedure hashes defining a VM kernel.
Module: The abstract syntax tree for a single Miden Assembly module.
Program: An executable program for Miden VM.
ProgramInfo: A program information set consisting of its MAST root and set of kernel procedure roots used for its compilation.
ProvingOptions: A set of parameters specifying how Miden VM execution proofs are to be generated.
StackInputs: Defines the initial state of the VM’s operand stack.
StackOutputs: Defines the final state of the VM’s operand stack at the end of program execution.
StarkProof: A serialized STARK proof and the hash function used during proof generation.
TraceBuildInputs: Inputs required to build an execution trace from pre-executed data.
TraceGenerationContext
TraceProvingInputs: Inputs required to prove from pre-executed trace data.
Unsettled: The obligation a partially verified proof hands back: the hydrated deferred state whose root the verified statement bound.
Verifier: Configurable verifier for Miden execution proofs.
Word: A unit of data consisting of 4 field elements.

Enums§

DeferredProof: Proof material for the precompile claims associated with an execution proof.
ExecutionError
HashFunction: A hash function used during STARK proof generation.
InputError
ModuleKind: Represents the kind of a Module.
Operation: The set of native VM basic block operations executable which take exactly one cycle to execute.
VerificationError: Errors that can occur during proof verification.

Constants§

ZERO: Field element representing ZERO in the Miden base field.

Traits§

BaseHost: Defines the host functionality shared by both sync and async execution.
FutureMaybeSend: Alias for a Future
Host: Defines an async interface by which the VM can interact with the host during execution.
SyncHost: Defines a synchronous interface by which the VM can interact with the host during execution.

Functions§

execute: Executes the provided program against the provided inputs and returns the resulting execution output.
execute_sync: Synchronous wrapper for the async execute() function.
prove: Executes and proves the specified program and returns the result together with a final STARK-based proof of the program’s execution.
prove_from_trace_sync: Builds an execution trace from pre-executed trace inputs and proves it synchronously.
prove_sync: Synchronous variant of prove().
verify: Verifies a final Miden proof of the given execution claim.

Crate miden_vm

Crate miden_vm Copy item path

§Miden VM

§Basic concepts

§Writing programs

§Program hash

§Inputs / outputs

§Usage

§Executing programs

§Proving program execution

§Proof generation example

§Verifying program execution

§Proof verification example

§Fibonacci calculator

§CLI interface

§Compiling Miden VM

§Running Miden VM

§Fibonacci example

§Crate features

§Concurrent proof generation

§License

Re-exports§

Modules§

Structs§

Enums§

Constants§

Traits§

Functions§

Crate miden_vm