triton-vm 0.43.0

A virtual machine that comes with Algebraic Execution Tables (AET) and Arithmetic Intermediate Representations (AIR) for use in combination with a STARK proof system to allow proving correct execution of arbitrary programs in zero-knowledge.
Documentation

Triton VM

License GitHub CI crates.io Spec: online Coverage Status

Triton is a virtual machine that comes with Algebraic Execution Tables (AET) and Arithmetic Intermediate Representations (AIR) for use in combination with a STARK proof system. It defines a Turing complete Instruction Set Architecture, as well as the corresponding arithmetization of the VM. The really cool thing about Triton VM is its efficient recursive verification of the STARKs produced when running Triton VM.

Getting Started

If you want to start writing programs for Triton VM, check out Triton TUI. If you want to generate or verify proofs of correct execution, take a look at the examples.

Recursive STARKs of Computational Integrity

Normally, when executing a machine – virtual or not – the flow of information can be regarded as follows. The tuple of (input, program) is given to the machine, which takes the program, evaluates it on the input, and produces some output.

If the – now almost definitely virtual – machine also has an associated STARK engine, one additional output is a proof of computational integrity.

Only if input, program, and output correspond to one another, i.e., if output is indeed the result of evaluating the program on the input according to the rules defined by the virtual machine, then producing such a proof is easy. Otherwise, producing a proof is next to impossible.

The routine that checks whether a proof is, in fact, a valid one, is called the Verifier. It takes as input a 4-tuple (input, program, output, proof) and evaluates to true if and only if that 4-tuple is consistent with the rules of the virtual machine.

Since the Verifier is a program taking some input and producing some output, the original virtual machine can be used to perform the computation.

The associated STARK engine will then produce a proof of computational integrity of verifying some other proof of computational integrity – recursion! Of course, the Verifier can be a subroutine in a larger program.

Triton VM is specifically designed to allow fast recursive verification.

Project Status

Triton VM is still under construction. We currently don't recommend using it in production.

Please note that the Instruction Set Architecture is not to be considered final. However, we don't currently foresee big changes.

Specification

The specification can be found online. Alternatively, you can self-host the mdBook by first installing the dependencies, then serving the mdBook.

cargo install mdbook
cargo install mdbook-katex
cargo install mdbook-linkcheck

mdbook serve --open

Potentially, ~/.cargo/bin needs to be added to the PATH.

Running the Code

The Rust implementation of Triton VM resides in triton-vm and can be found on crates.io.

Triton VM depends on the twenty-first cryptographic library.

For trying out the code, install Rust and run:

~ $ git clone https://github.com/TritonVM/triton-vm.git
~ $ cd triton-vm
~/triton-vm $ make test

For local development of both libraries, it is encouraged to follow GitHub's fork & pull workflow by forking and cloning both, place twenty-first relative to triton-vm, and change the dependency to be path-local:

~ $ git clone git@github.com:you/triton-vm.git
~ $ git clone git@github.com:you/twenty-first.git
~ $ cd triton-vm
~/triton-vm $ ln -s ../twenty-first/twenty-first twenty-first
~/triton-vm $ sed -i '/^twenty-first =/ s/{.*}/{ path = "..\/twenty-first" }/' triton-vm/Cargo.toml