Using Miden VM
Before you can use Miden VM, you'll need to make sure you have Rust installed. Miden VM v0.5 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, which can be used to execute Miden VM programs.
- miden-prover, which can be used to execute Miden VM programs and generate proofs of their execution.
- miden-verifier, which can be used to verify proofs of program execution generated by Miden VM prover.
The above functionality is also exposed via the single miden crate, which also provides a CLI interface for interacting with Miden VM.
Compiling Miden VM
To compile Miden VM into a binary, we have a Makefile with the following tasks:
This will place an optimized, multi-threaded
miden executable in the
./target/release 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
cargo build --release --features concurrent,executable
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.
Running Miden VM
Once the executable has been compiled, you can run Miden VM like so:
./target/release/miden [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 (i.e., build a program MAST) 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.
repl- this will initiate 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/release/miden [subcommand] --help
./target/release/miden prove --help
miden/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/release/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
-o flag and specify the path to the output file. For example:
./target/release/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.
Miden Development Tooling
The Miden debugger is a command-line interface (CLI) application, inspired on GNU gdb, that allows debugging of Miden assembly (MASM) programs. The debugger allows the user to step through the execution of the program, both forward and backward, either per clock cycle tick, or via breakpoints.
The Miden debugger supports the following commands:
|continue||c||-||Executes the program until completion, failure or a breakpoint.|
|back||b||count?||Backward step |
|rewind||r||-||Executes the program backwards until the beginning, failure or a breakpoint.|
|p||-||Displays the complete state of the virtual machine.|
|print mem||p m||address?||Displays the memory value at |
|print stack||p s||index?||Displays the stack value at |
|clock||c||-||Displays the current clock cycle.|
|quit||q||-||Quits the debugger.|
|help||h||-||Displays the help message.|
In order to start debugging, the user should provide a
cargo run --features executable -- debug --assembly miden/examples/nprime/nprime.masm
The expected output is:
Reading program file `miden/examples/nprime/nprime.masm`
Compiling program... done (16 ms)
Debugging program with hash 11dbbddff27e26e48be3198133df8cbed6c5875d0fb
Reading input file `miden/examples/nprime/nprime.inputs`
Welcome! Enter `h` for help.
In order to add a breakpoint, the user should insert a
breakpoint instruction into the MASM file. This will generate a
Noop operation that will be decorated with the debug break configuration. This is a provisory solution until the source mapping is implemented.
The following example will halt on the third instruction of
The Miden Read–eval–print loop (REPL) is a Miden shell that allows for quick and easy debugging of Miden assembly. After the REPL gets initialized, you can execute any Miden instruction, undo executed instructions, check the state of the stack and memory at a given point, and do many other useful things! When the REPL is exited, a
history.txt file is saved. One thing to note is that all the REPL native commands start with an
! to differentiate them from regular assembly instructions. The REPL currently supports the following commands:
Miden assembly instruction
All Miden instructions mentioned in the Miden Assembly sections are valid. One can either input instructions one by one or multiple instructions in one input.
For example, the below two commands will result in the same output.
push.1 push.2 push.3
To execute a control flow operation, one must write the entire statement in a single line with spaces between individual operations.
The above example should be written as follows in the REPL tool:
repeat.20 pow2 end
!help command prints out all the available commands in the REPL tool.
!program command prints out the entire Miden program being executed. E.g., in the below scenario:
>> repeat.16 pow2 end
repeat.16 pow2 end
!stack command prints out the state of the stack at the last executed instruction. Since the stack always contains at least 16 elements, 16 or more elements will be printed out (even if all of them are zeros).
>> push.1 push.2 push.3 push.4 push.5
!stack command will print out the following state of the stack:
3072 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
!mem command prints out the contents of all initialized memory locations. For each such location, the address, along with its memory values, is printed. Recall that four elements are stored at each memory address.
If the memory has at least one value that has been initialized:
7: [1, 2, 0, 3]
8: [5, 7, 3, 32]
9: [9, 10, 2, 0]
If the memory is not yet been initialized:
The memory has not been initialized yet
!mem[addr] command prints out memory contents at the address specified by
addr has been initialized:
9: [9, 10, 2, 0]
addr has not been initialized:
Memory at address 87 is empty
!undo command reverts to the previous state of the stack and memory by dropping off the last executed assembly instruction from the program. One could use
!undo as often as they want to restore the state of a stack and memory instructions ago (provided there are instructions in the program). The
!undo command will result in an error if no remaining instructions are left in the Miden program.
>> push.1 push.2 push.3
4 3 2 1 0 0 0 0 0 0 0 0 0 0 0 0
5 4 3 2 1 0 0 0 0 0 0 0 0 0 0 0
4 3 2 1 0 0 0 0 0 0 0 0 0 0 0 0
3 2 1 0 0 0 0 0 0 0 0 0 0 0 0 0