/miden

STARK-based virtual machine

Primary LanguageRustMIT LicenseMIT

Polygon Miden

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.

Overview

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.

Status and features

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.

Planned features

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.

Project structure

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.

Performance

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:

  1. 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.
  2. Proof verification time is really fast. In most cases it is under 1 ms, but sometimes gets as high as 2 ms.
  3. 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:

  1. 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.
  2. 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).

References

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:

Vitalik Buterin's blog series on zk-STARKs:

Alan Szepieniec's STARK tutorial:

StarkWare's STARK Math blog series:

License

This project is MIT licensed.