Triton VM

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 the Triton TUI. If you want to run a Triton assembly program, generate or verify proofs of correct execution, or profile the performance of either of these, check out the Triton CLI. If you want to use Triton VM as a library, check out the examples.

Project Status

We consider Triton VM to be usable in production. That said, there are plans to change some of the internals significantly. Some of these changes might have effects on the interface as well as the ISA.

As is common for rust projects, Triton VM follows Cargo-style SemVer.

Specification

Triton VM’s specification can be found online. Alternatively, you can self-host it.

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.