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.
print	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 $n$ instructions ago (provided there are $n$ 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