Recufier

[aszepieniec]

Recursion is the holy grail for SNARKs and STARKs because it unlocks schemes like Incrementally Verifiable Computation (IVC), Proof-Carrying Data (PCD), and proof aggregation. After this threshold, more prover work simply means more parallelism; the proving time is barely affected.

This task involves writing a recursive verifier (recufier) for Triton-VM. This issue explains the steps involved and can be used to track progress.

writing tasm

Tasm is short for Triton-assembler. It is the assembler language native to Triton-VM. The specification for tasm is part of this repository as well as on the website. We do our best to keep it up to date and maximally informative; if you find a flaw or an omission or just have a suggestion for improvement, please make a PR.

Tasm is not stable. While we don't expect to be changing the definition of existing instructions much, we almost certainly will be adding new ones. The reason is that we anticipate needing them to make the recufier fast ;-)

The best way to get started writing tasm is contribute useful snippets to the standard library, tasm-lib. There are plenty of examples there to follow.

compiling from rust

In addition to writing tasm by hand, we are developing a compiler from a subset of rust to tasm. This project lives in tasm-lang. It uses rust's syn and quote packages to obtain an abstract syntax tree from an embedded snippet of rust.

The compiler is still in early stages, but it can already be used for simple arithmetic tasks.

Tasm-lang and tasm-lib are mutually supporting projects. The more tasm snippets live in tasm-lib, the more rust-like expressions we can compile. And we can accelerate the production of new tasm snippets by first writing them in a higher level representation and then compiling them down.

The ultimate goal is to have a decorator attribute mark rust functions as compilation targets like so:

#[triton_compile]
pub fn my_function(input: InputType, also_input: AlsoType, secret_witness: Witness) {
    // rust code goes here
}

and then obtain the Program through another macro, e.g., triton_program!(my_function).

writing the verifier

The code is essentially that of the current verifier. One way or another, we need tasm code for it.

While the exact prover (and thus verifier) pipeline may change, the underlying principles and mathematics will definitely remain. So as we build a codebase in tasm for the verifier, changes to the verifier pipeline might affect how snippets are linked together.

The language so far suggests that there is only one recufier, but in fact can be multiple programs that do similar things. For example:

• One recufier can merge two proofs.
• One recufier can reparameterize a proof such that the result is smaller in size.
• One recufier can merge two proofs for segments of a long-running computation, and moreover certify that the state transmitted across those segments is the same.

Naturally, all these flavors of recufiers share a lot of code.

optimizing the verifier

It is worth noting that using non-determinism we can make the recufier more efficient than a naive translation of the rust-verifier. Specifically:

• We can instantiate memory to contain the entire proof(s) initially, without having to read them in from an input stream.
• When verifying Merkle authentication paths we can divine the sibling nodes as opposed to reading them from the proof.
• Some arithmetic operations can be guessed-then-verified more efficiently than computed.

This goes to say that the recufier will look different from the rust-verifier evetually.

[ameya-deshmukh]

@aszepieniec thanks so much for writing up this issue! Looking forward to collaborate on it. Can you assign it to me in the meantime?

[jan-ferdinand]

See also #7.