A STARK-based virtual machine.
WARNING: This project is in an alpha stage. It has not been audited and may contain bugs and security flaws. This implementation is NOT ready for production use.
Miden is a zero-knowledge virtual machine written in Rust. For any program executed on Miden VM, a STARK-based proof of execution is automatically generated. This proof can then be used by anyone to verify that a program was executed correctly without the need for re-executing the program or even knowing what the program was.
- If you'd like to learn more about how Miden VM works, check out the miden crate.
- If you'd like to see Miden VM in action, check out the examples crate.
- If you'd like to learn more about STARKs, check out the references section.
Currently, this project contains a direct port of the original Distaff VM to Winterfell backend. This means that, as compared to the original Distaff VM, the proving system has been upgraded to a much more up-to-date and performant STARK prover - but, the functionality of the VM remained the same. This functionality includes:
- Field arithmetic. Miden VM can execute one field operation per cycle. This includes addition, multiplication, inversion, and boolean operations (on binary values).
- Conditional statements. Miden VM programs can include basic if-then-else statements, however, these statements can be nested at most 16 levels deep.
- Loops. Miden VM programs can include counter-controlled (for) and condition-controlled (while) loops. However, loops can be nested at most 8 levels deep.
- Inequality comparisons. Miden VM supports less-than and greater-than comparison of field elements (via binary decomposition). However, each comparison requires dozens of VM cycles.
- Hashing. Miden VM natively supports Rescue hash function. A 2-to-1 Rescue hash can be computed in as few as 10 VM cycles.
In the coming months we plan to make significant changes to the VM to expand its feature set. Among other things, these will include:
- Flow control. Restrictions on nestings of loops and conditional statements will be removed.
- Memory. Support for read-write random-access memory will be added to the VM.
- Storage. Support for read-write persistent storage will be added to the VM.
- Function calls. Miden programs will support hash-addressable function calls.
- u32 operations. The VM will be able to execute a single u32 operation per cycle.
Our ultimate goal is to make Miden VM an easy compilation target for high level languages such as Solidity, Move, and others.
The new version of the VM is being developed in the next branch.
The project is organized into several crates like so:
| Crate | Description |
|---|---|
| core | Contains components defining Miden VM instruction set, program structure, and a set of utility functions used by other crates. |
| assembly | Contains Miden assembler and definition of the Miden Assembly language. The assembler is used to compile Miden assembly source code into Miden VM programs. |
| processor | Contains Miden VM processor. The processor is used to execute Miden programs and to generate program execution traces. These traces are then used by the VM to generate proofs of correct program execution. |
| air | Contains algebraic intermediate representation (AIR) of Miden VM processor logic. This AIR is used by the VM during proof generation and verification processes. |
| miden | Contains the actual Miden VM which can be used to execute programs and verify proofs of their execution. |
| verifier | Contains a light-weight verifier which can be used to verify proofs of program execution generated by Miden VM. |
| examples | Contains several toy and real-world examples of Miden VM programs and demonstrates how these programs can be executed on Miden VM. |
Current version of Miden VM operates at around 10 KHz when run on a single CPU core. When run on a 16-core CPU, Miden VM can operate at over 80 KHz. In the future we hope to significantly improve this performance.
In the benchmarks below, the VM executes a Fibonacci calculator program on AMD Ryzen 9 5950X CPU (single thread):
| Operations | 96-bit security | 128-bit security | ||||
|---|---|---|---|---|---|---|
| Execution time | Execution RAM | Proof size | Execution time | Execution RAM | Proof size | |
| 28 | 27 ms | 9 MB | 28 KB | 200 ms | 9 MB | 45 KB |
| 210 | 81 ms | 11 MB | 34 KB | 170 ms | 13 MB | 59 KB |
| 212 | 314 ms | 22 MB | 42 KB | 680 ms | 58 MB | 70 KB |
| 214 | 1.3 sec | 81 MB | 51 KB | 2.2 sec | 204 MB | 82 KB |
| 216 | 5.4 sec | 313 MB | 59 KB | 9.1 sec | 800 MB | 100 KB |
| 218 | 22.3 sec | 1.2 GB | 69 KB | 39 sec | 3.2 GB | 115 KB |
| 220 | 1.5 min | 4.9 GB | 82 KB | 2.7 min | 12.3 GB | 129 KB |
A few notes about these results:
- Execution time is dominated by the proof generation time. In fact, the time needed to run the program is only about 3% of the time needed to generate the proof.
- Proof verification time is really fast. In most cases it is under 1 ms, but sometimes gets as high as 2 ms.
- Proof generation process is dynamically adjustable. In general, there is a trade-off between execution time, proof size, and security level (i.e. for a given security level, we can reduce proof size by increasing execution time, up to a point).
However, we don't have to limit ourselves to a single thread: STARK proof generation is massively parallelizable. The benchmarks below show program execution time for running the Fibonacci calculator for 216 operations (for 96-bit security level) using varying number of threads.
| Threads | Execution time | Improvement |
|---|---|---|
| 1 | 5.4 sec | 1x |
| 2 | 2.9 sec | 1.9x |
| 4 | 1.6 sec | 3.4x |
| 8 | 0.95 sec | 5.7x |
| 16 | 0.7 sec | 7.7x |
| 32 | 0.6 sec | 9x |
A few notes about these results:
- Ryzen 9 5950X has 16 cores. So, executing the program in 32 threads seems to lead a slightly better CPU core utilization as compared to running it in 16 threads.
- The Fibonacci calculator program is sequential - so, we can parallelize only the proof generation part. This means that the share of time taken up by running the program itself grows proportionally. For example, when we execute the program using 32 threads, the time it takes to run the program is roughly 25% of the overall execution time (vs 3% for a single thread).
Proofs of execution generated by Miden VM are based on STARKs. A STARK is a novel proof-of-computation scheme that allows you to create an efficiently verifiable proof that a computation was executed correctly. The scheme was developed by Eli Ben-Sasson, Michael Riabzev et al. at Technion - Israel Institute of Technology. STARKs do not require an initial trusted setup, and rely on very few cryptographic assumptions.
Here are some resources to learn more about STARKs:
- STARKs whitepaper: Scalable, transparent, and post-quantum secure computational integrity
- STARKs vs. SNARKs: A Cambrian Explosion of Crypto Proofs
Vitalik Buterin's blog series on zk-STARKs:
- STARKs, part 1: Proofs with Polynomials
- STARKs, part 2: Thank Goodness it's FRI-day
- STARKs, part 3: Into the Weeds
Alan Szepieniec's STARK tutorial:
StarkWare's STARK Math blog series:
- STARK Math: The Journey Begins
- Arithmetization I
- Arithmetization II
- Low Degree Testing
- A Framework for Efficient STARKs
This project is MIT licensed.