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.

Examples

Convenience function prove_program() as well as the prove() and verify() methods natively operate on BFieldElements, i.e, elements of the prime field with 2^64 - 2^32 + 1 elements.

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::from([bfe!(10)]);
let non_determinism = NonDeterminism::default();

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

let verdict = 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) =
   prove_program(&sum_of_squares_program, public_input, non_determinism).unwrap();

let verdict = 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 halt);
let vm_error = crashing_program.run([].into(), [].into()).unwrap_err();
assert!(matches!(vm_error.source, InstructionError::AssertionFailed));
// inspect the VM state
eprintln!("{vm_error}");

Re-exports

• pub use twenty_first;

Modules

• aet
• arithmetic_domain
• error
• example_programs
• fri
• instruction
• op_stack
• parser
• prelude
  Re-exports the most commonly-needed APIs of Triton VM.
• profiler
• program
• proof
• proof_item
• proof_stream
• stark
• table
• vm

Macros

• triton_asm
  Compile Triton assembly into a list of labelled Instructions. Similar to triton_program!, it is possible to use string-like interpolation to insert instructions, arguments, labels, or other expressions.
• triton_instr
  Compile a single Triton assembly instruction into a LabelledInstruction.
• triton_program
  Compile an entire program written in Triton assembly. The resulting Program can be run.

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.