Crate triton_vm

Triton Virtual Machine is a Zero-Knowledge Proof System (ZKPS) for proving correct execution of programs written in Triton assembly. The proof system is a zk-STARK, which is a state-of-the-art ZKPS.

Generally, all arithmetic performed by Triton VM happens in the prime field with 2^64 - 2^32 + 1 elements. Instructions for u32 operations are provided.

For a full overview over all available instructions and their effects, see the specification.

Triton VM’s STARK is parametric, but it is highly recommended to use the provided default. Furthermore, certain runtime characteristics are configurable, and usually don’t need changing.

Non-Determinism

Triton VM is a non-deterministic machine. That is,

1. Triton VM’s random access memory can be initialized arbitrarily, and
2. for a select few instructions (namely divine and merkle_step), correct state transition is not fully determined by the current state and Triton VM’s public input.

The input for those non-deterministic instructions use dedicated input streams. Those, together with the initial RAM, are collectively called NonDeterminism.

Examples

Below are a few examples on how to use Triton VM. They show the instruction set architecture in action and highlight the core methods required to generate & verify a proof of correct execution. Some of these are convenience function prove_program() as well as the prove() and verify() methods.

Factorial

Compute the factorial of the given public input.

The execution of the factorial program is already fully determined by the public input. Hence, in this case, there is no need for specifying non-determinism. Keep reading for an example that does use non-determinism.

The triton_program! macro is used to conveniently write Triton assembly. In below example, the state of the operational stack is shown as a comment after most instructions.

let factorial_program = triton_program!(
    read_io 1           // n
    push 1              // n 1
    call factorial      // 0 n!
    write_io 1          // 0
    halt

    factorial:          // n acc
        // if n == 0: return
        dup 1           // n acc n
        push 0 eq       // n acc n==0
        skiz            // n acc
            return      // 0 acc
        // else: multiply accumulator with n and recurse
        dup 1           // n acc n
        mul             // n acc·n
        swap 1          // acc·n n
        push -1 add     // acc·n n-1
        swap 1          // n-1 acc·n
        recurse
);
let public_input = PublicInput::new(bfe_vec![10]);
let non_determinism = NonDeterminism::default();

let (stark, claim, proof) =
    triton_vm::prove_program(factorial_program, public_input, non_determinism).unwrap();

let verdict = triton_vm::verify(stark, &claim, &proof);
assert!(verdict);

assert_eq!(1, claim.output.len());
assert_eq!(3_628_800, claim.output[0].value());

Non-Determinism

In the following example, a public field elements equality to the sum of some squared secret elements is proven. For demonstration purposes, some of the secret elements come from secret in, and some are read from RAM, which can be initialized arbitrarily.

Note that the non-determinism is not required for proof verification, and does not appear in the claim or the proof. It is only used for proof generation. This way, the verifier can be convinced that the prover did indeed know some input that satisfies the claim, but learns nothing beyond that fact.

The third potential source of non-determinism is intended for verifying Merkle authentication paths. It is not used in this example. See NonDeterminism for more information.

let sum_of_squares_program = triton_program!(
    read_io 1                       // n
    call sum_of_squares_secret_in   // n sum_1
    call sum_of_squares_ram         // n sum_1 sum_2
    add                             // n sum_1+sum_2
    eq                              // n==(sum_1+sum_2)
    assert                          // abort the VM if n!=(sum_1+sum_2)
    halt

    sum_of_squares_secret_in:
        divine 1 dup 0 mul          // s₁²
        divine 1 dup 0 mul add      // s₁²+s₂²
        divine 1 dup 0 mul add      // s₁²+s₂²+s₃²
        return

    sum_of_squares_ram:
        push 17                     // 18
        read_mem 1                  // s₄ 17
        pop 1                       // s₄
        dup 0 mul                   // s₄²
        push 42                     // s₄² 43
        read_mem 1                  // s₄² s₅ 42
        pop 1                       // s₄² s₅
        dup 0 mul                   // s₄² s₅²
        add                         // s₄²+s₅²
        return
);
let public_input = PublicInput::from([bfe!(597)]);
let secret_input = [5, 9, 11].map(|v| bfe!(v));
let initial_ram = [(17, 3), (42, 19)].map(|(address, v)| (bfe!(address), bfe!(v)));
let non_determinism = NonDeterminism::from(secret_input).with_ram(initial_ram);

let (stark, claim, proof) =
   triton_vm::prove_program(sum_of_squares_program, public_input, non_determinism).unwrap();

let verdict = triton_vm::verify(stark, &claim, &proof);
assert!(verdict);

Crashing Triton VM

Successful termination of a program is not guaranteed. For example, a program must execute halt as its last instruction. Certain instructions, such as assert, invert, or the u32 instructions, can also cause the VM to crash. Upon crashing Triton VM, methods like run and trace_execution will return a VMError. This can be helpful for debugging.

let crashing_program = triton_program!(push 2 assert error_id 42 halt);
let vm_error = VM::run(crashing_program, [].into(), [].into()).unwrap_err();
let InstructionError::AssertionFailed(ref assertion_error) = vm_error.source else {
    unreachable!();
};

assert_eq!(Some(42), assertion_error.id);
eprintln!("{vm_error}"); // inspect the VM state

Re-exports

• pub use air;
• pub use isa;
• pub use twenty_first;

Modules

• aet
• arithmetic_domain
• challenges
  Challenges are needed for the cross-table arguments, i.e., Permutation Arguments, Evaluation Arguments, and Lookup Arguments, as well as for the RAM Table’s Contiguity Argument.
• config
  This module contains various configuration options for Triton VM. In general, the configuration options impact performance only. In particular, any configuration provides the same completeness and soundness guarantees.
• constraints
• error
• example_programs
• execution_trace_profiler
• fri
• memory_layout
• prelude
  Re-exports the most commonly-needed APIs of Triton VM.
• profiler
  Allows profiling proving and verifying of Triton VM’s STARK proofs.
• proof
• proof_item
• proof_stream
• stark
• table
• vm

Functions

• prove
  A convenience function for proving a Claim and the program that claim corresponds to. Method prove_program gives a simpler interface with less control.
• prove_program
  Prove correct execution of a program written in Triton assembly. This is a convenience function, abstracting away the details of the STARK construction. If you want to have more control over the STARK construction, this method can serve as a reference for how to use Triton VM.
• verify
  Verify a proof generated by prove or prove_program.