How to Use the Miden Virtual Machine
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.
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 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 --release
. Example:
cargo build --release --features concurrent,executable
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.
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
For example:
./target/release/miden prove --help
Fibonacci example
In the 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 --output
or -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
Miden Debugger
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:
Command | Shortcut | Arguments | Description |
---|---|---|---|
next | n | count? | Steps count clock cycles. Will step 1 cycle of count is omitted. |
continue | c | - | Executes the program until completion, failure or a breakpoint. |
back | b | count? | Backward step count clock cycles. Will back-step 1 cycle of count is omitted. |
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 address . If address is omitted, didisplays all the memory values. |
print stack | p s | index? | Displays the stack value at index . If index is omitted, displays all the stack values. |
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 MASM
program:
cargo run --features executable -- debug --assembly miden/examples/nprime/nprime.masm
The expected output is:
============================================================
Debug program
============================================================
Reading program file `miden/examples/nprime/nprime.masm`
Compiling program... done (16 ms)
Debugging program with hash 11dbbddff27e26e48be3198133df8cbed6c5875d0fb
606c9f037c7893fde4118...
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 foo
:
proc.foo
dup
dup.2
breakpoint
swap
add.1
end
begin
exec.foo
end
REPL
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
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.
repeat.20
pow2
end
The above example should be written as follows in the REPL tool:
repeat.20 pow2 end
!help
The !help
command prints out all the available commands in the REPL tool.
!program
The !program
command prints out the entire Miden program being executed. E.g., in the below scenario:
>> push.1.2.3.4
>> repeat.16 pow2 end
>> u32checked_add
>> !program
begin
push.1.2.3.4
repeat.16 pow2 end
u32checked_add
end
!stack
The !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
>> exp
>> u32checked_mul
>> swap
>> eq.2
>> assert
The !stack
command will print out the following state of the stack:
>> !stack
3072 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0
!mem
The !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:
>> !mem
7: [1, 2, 0, 3]
8: [5, 7, 3, 32]
9: [9, 10, 2, 0]
If the memory is not yet been initialized:
>> !mem
The memory has not been initialized yet
!mem[addr]
The !mem[addr]
command prints out memory contents at the address specified by addr
.
If the addr
has been initialized:
>> !mem[9]
9: [9, 10, 2, 0]
If the addr
has not been initialized:
>> !mem[87]
Memory at address 87 is empty
!undo
The !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
>> push.4
>> !stack
4 3 2 1 0 0 0 0 0 0 0 0 0 0 0 0
>> push.5
>> !stack
5 4 3 2 1 0 0 0 0 0 0 0 0 0 0 0
>> !undo
4 3 2 1 0 0 0 0 0 0 0 0 0 0 0 0
>> !undo
3 2 1 0 0 0 0 0 0 0 0 0 0 0 0 0