Usage
Before using Miden VM, make sure you have Rust installed. Miden VM v0.7 requires Rust version 1.67 or later.
Miden VM consists of several crates, each of which exposes a small set of functionality. The most notable of these crates are:
- miden-processor: Execute Miden VM programs.
- miden-prover: Execute Miden VM programs and generate proofs of their execution.
- miden-verifier: Verify proofs of program execution generated by Miden VM prover.
The above functionality is also exposed via the single miden-vm crate, which also provides a CLI interface for interacting with Miden VM.
CLI interface¶
Compiling Miden VM¶
To compile Miden VM into a binary, we have a Makefile with the following tasks:
make exec
This will place an optimized, multi-threaded miden executable into the ./target/optimized directory. It is equivalent to executing:
cargo build --profile optimized --features concurrent,executable
If you would like to enable single-threaded mode, you can compile Miden VM using the following command:
cargo build --profile optimized --features executable
For a faster build, you can compile with less optimizations, replacing --profile optimized by --release. Example:
cargo build --release --features concurrent,executable
In this case, the miden executable will be placed in the ./target/release directory.
Controlling parallelism¶
Internally, Miden VM uses rayon for parallel computations. To control the number of threads used to generate a STARK proof, you can use RAYON_NUM_THREADS environment variable.
GPU acceleration¶
Miden VM proof generation can be accelerated via GPUs. Currently, GPU acceleration is enabled only on Apple silicon hardware (via Metal). To compile Miden VM with Metal acceleration enabled, you can run the following command:
make exec-metal
Similar to make exec command, this will place the resulting miden executable into the ./target/optimized directory.
Currently, GPU acceleration is applicable only to recursive proofs which can be generated using the -r flag.
SIMD acceleration¶
Miden VM execution and proof generation can be accelerated via vectorized instructions. Currently, SIMD acceleration can be enabled only on platforms supporting SVE instructions (e.g., Graviton 3). To compile Miden VM with SVE acceleration enabled, you can run the following command:
make exec-graviton
This will place the resulting miden executable into the ./target/optimized directory.
Similar to Metal acceleration, SVE acceleration is currently applicable only to recursive proofs which can be generated using the -r flag.
Running Miden VM¶
Once the executable has been compiled, you can run Miden VM like so:
./target/optimized/miden [subcommand] [parameters]
Currently, Miden VM can be executed with the following subcommands:
run: Executes a Miden assembly program and output the result, but will not generate a proof of execution.prove: Executes a Miden assembly program, and will also generate a STARK proof of execution.verify: Verifies a previously generated proof of execution for a given program.compile: Compiles a Miden assembly program (i.e., build a program MAST) and outputs stats about the compilation process.debug: Instantiates a Miden debugger against the specified Miden assembly program and inputs.analyze: Runs a Miden assembly program against specific inputs and will output stats about its execution.repl: Initiates the Miden REPL tool.
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 [subcommand] --help
For example:
./target/optimized/miden prove --help
To execute a program using the Miden VM there needs to be a .masm file containing the Miden Assembly code and a .inputs file containing the inputs.
Inputs¶
As described here the Miden VM can consume public and secret inputs.
- Public inputs:
operand_stack- can be supplied to the VM to initialize the stack with the desired values before a program starts executing. There is no limit on the number of stack inputs that can be initialized in this way, although increasing the number of public inputs increases the cost to the verifier.
- Secret (or nondeterministic) inputs:
advice_stack- can be supplied to the VM. There is no limit on how much data the advice provider can hold. This is provided as a string array where each string entry represents a field element.advice_map- is supplied as a map of 64-character hex keys, each mapped to an array of numbers. The hex keys are interpreted as 4 field elements and the arrays of numbers are interpreted as arrays of field elements.merkle_store- the Merkle store is container that allows the user to definemerkle_tree,sparse_merkle_treeandpartial_merkle_treedata structures.merkle_tree- is supplied as an array of 64-character hex values where each value represents a leaf (4 elements) in the tree.sparse_merkle_tree- is supplied as an array of tuples of the form (number, 64-character hex string). The number represents the leaf index and the hex string represents the leaf value (4 elements).partial_merkle_tree- is supplied as an array of tuples of the form ((number, number), 64-character hex string). The internal tuple represents the leaf depth and index at this depth, and the hex string represents the leaf value (4 elements).
Info
Check out the comparison example to see how secret inputs work.
After a program finishes executing, the elements that remain on the stack become the outputs of the program, along with the overflow addresses (overflow_addrs) that are required to reconstruct the stack overflow table.
Fibonacci example¶
In the miden/examples/fib directory, we provide a very simple Fibonacci calculator example. This example computes the 1001st term of the Fibonacci sequence. You can execute this example on Miden VM like so:
./target/optimized/miden run -a miden/examples/fib/fib.masm -n 1
This will run the example code to completion and will output the top element remaining on the stack.
If you want the output of the program in a file, you can use the --output or -o flag and specify the path to the output file. For example:
./target/optimized/miden run -a miden/examples/fib/fib.masm -o fib.out
This will dump the output of the program into the fib.out file. The output file will contain the state of the stack at the end of the program execution.