A Tutorial on Writing proofs with Plonky2 (Part I)

Prerequisites: you should have a basic understanding of zero-knowledge proofs and zkSNARKs. It’s helpful to have a general understanding of how they work so that you understand bottlenecks such as proof generating time. If you don’t know much about how zk-proofs/SNARKs work, there’s some great lectures from Dan Boneh here.

About Recursive zk proofs

Zero-knowledge (zk) proofs are powerful tools to reduce the gas and time of blockchain node verification. Computational verification can be done by re-running the computation (e.g. computing new state root for an incoming block), or it can be done by verifying a zk proof that such computation was done correctly. Surprisingly, verifying a proof of computation can be done in less time and gas than re-running the original computation.

There are many classes of zk proving schemes (SNARK, STARK, VPD, SNARG) and they vary in many properties such as trust minimization, security assumptions, proving time, and verification time. There are variations even with these broad categories, such as many different kinds of SNARKs. Like many design decisions, there are often tradeoffs between these properties.

The property this article focuses on is proving time/effort. This is of particular importance for rollups, where chain A’s state is proven on chain B by submitting proofs. Proving time can affect liveness, the ability for anyone to force the chain to advance by executing transactions and posting assertions. Liveness has several important downstream effects for rollups:

1. The costs of advancing the chain may be distributed over many participants instead of one person.

2. The latency of rollup data availability is greatly reduced, as anyone who needs the rollup updated can force that change on demand.

3. Censorship of data availability is less practical when more people can advance the rollup state.

4. If the proving time/effort becomes low enough, then proving can be done on commodity hardware instead of requiring the services of 3rd party data centers or requiring expensive hardware.

One of the latest advancements in efficient zk proof generation are recursive zk proofs. The main benefit of recursive proofs is that proof generation can be generated in parallel, meaning that the total work of proving can be divided between multiple computers instead of just one. The prover does linear work in the size of the circuit C so breaking up a larger circuit into smaller circuits will yield a performance gain.

₀ ₁ ₂ ₃ ₄ ₅ ₆ ₇ ₈ ₉

For a given proof, it might be divided into P individual proofs which are computed in parallel to give us a proof array [P₀⁰, P₀¹, …, P₀ˢ] of size S. Then for each two successive proofs, a new proof is generated to compress them into one proof, resulting in a new proof array [P₁⁰, P₁¹, …, P₁ˢᐟ²] of size S/2. This process repeats recursively until there is only one proof left: [Pₗₒ₉₍ₛ₎⁰].

One of the intuitive analogies to understanding recursive zk proofs is Merkle tree verification. In both Merkle trees and recursive zk proofs, each has the topology of a binary tree and each node is computed from its two children. For each level of the Merkle tree, computing the value of each node can be done independent of the other nodes on the same level. For a single computer, the total time required to verify a Merkle tree of size N would be N/2 time for the leaves (half of the nodes in a balanced binary tree are leaves), N/4 time for the level above it (each parent level has half the nodes of the level below it), N/8 above that etc. Since each Merkle node can be computed with 1 time unit, each level gets computed in 1 time unit. The total time to build a Merkle tree with maximum parallelism is 1 time unit * tree height = log₂(N).

The total time to recursively compose Plonky2 proofs with maximum parallelism is 1 time unit to generate Plonky2 proof +log₂(N) * time unit to generate recursive Plonky2 proof. We can assume a complex circuit C can be divided into many sub-circuits C_0, C_1 … C_N and each sub-circuit takes the same time to prove: O(1). For example, to prove a zk-tendermint light client we need to verify 100 ed25519 signatures which will take 100 * 30s = 3000s. Plonky2 recursion time is very fast, say it takes 1s to generate a recursion proof. Then the total time to prove a tendermint light client becomes 30s + log(100) * 1s ~= 37s. See here for our plonky2 ed25519 implementation.

We can get even more practical than talking about how recursive proofs work by writing recursive proofs. Plonky2 is a new recursive SNARK from Polygon with an open source implementation. It boasts of 100x speedups from existing alternatives and native Ethereum compatibility.

Running plonky2 examples

First, we’ll show you how to run the examples in plonky2, then we’ll get into a discussion about how to write proofs.

First you’ll need some computer to run this on. Because this requires installing new software, werecommend doing this either in a virtual machine or in the cloud. For this example we’ve used AWS to create an EC2 instance running Ubuntu 22.04.1 LTS. If you choose to use AWS this won’t require the use of any paid services but you may be required to input payment information. You’ll create an EC2 instance with any instance size (choose the free tier, which should be the default). If you want to follow my example you’ll need to select Ubuntu as your operating system. Note that if you don’t choose the free tier, you’ll be billed per hour for the instance so you’ll need to take care to shut off or delete the instance via the AWS console when you’re done.

# We've chosen to ssh into our instance using a public-private key authentication. The way you access your machine may differ
ssh -i "polymer-ec2.pem" ubuntu@ec2–XX–XXX–XXX–XX.us-west-2.compute.amazonaws.com

# pull down the plonky2 library
cd ~
git clone https://github.com/mir-protocol/plonky2

# rust isn't installed on Ubuntu 22 by default so you need to download it
# https://doc.rust-lang.org/cargo/getting-started/installation.html
cd ~
curl https://sh.rustup.rs -sSf | sh
source "$HOME/.cargo/env"

# rust depends on some C libraries which need to be installed separately
# https://stackoverflow.com/questions/52445961/how-do-i-fix-the-rust-error-linker-cc-not-found-for-debian-on-windows-10
sudo apt-get update
sudo apt install build-essential

# use the rust nightly toolchain
cd ~/plonky2
rustup override set nightly

# run an example, let's start with factorial
cd ~/plonky2
RUSTFLAGS=-Ctarget-cpu=native cargo run - release - example factorial - -vv
Compiling plonky2 v0.1.0 (/home/ubuntu/plonky2/plonky2)
Finished release [optimized] target(s) in 44.92s
Running `target/release/examples/factorial -vv`
Factorial starting at 1 is 3822706312645553057!

# let's verify this example
# all arithmetic in plonky2 is modulo 2**64–2**32 + 1
$ cd ~
$ python3
>>> product = 1
>>> for x in range(1, 101):
… product = product * x
…
>>> modulus = 2**64–2**32 + 1
>>> product % modulus
3822706312645553057

What we just did was run a plonky2 proof example showing that we computed 100! = 100 * 99 * 98 * … * 2 * 1. Now we can talk about how to write your own proofs.

Writing zk-proofs as arithmetic circuits

Ultimately zk proofs are generated from arithmetic circuits. This means if you want to write a zk proof, what you’re really writing is an arithmetic circuit, and the proof library will take that input and use it to build a proof.

Through a process called arithmetization, we convert a circuit into a polynomial (Polynomial IOP) which is used as an information theoretic object to prove a statement to the verifier. A circuit is converted into an execution trace where the columns are the gates in the computation, the rows are the constraints and the values in the table are wires. This is then combined with some polynomial commitment scheme which acts as the agreed upon computation between a prover and a verifier.

For simplicity, we’ll focus on computations that are trivially convertible to arithmetic circuits, but it’s worth noting that converting arbitrary programs to arithmetic circuits is highly non-trivial.

Arithmetic circuits are kind of like boolean circuits. You may have heard of boolean circuits, the underlying computational model for combinational digital logic circuits (read: modern computers). Unlike boolean circuits, arithmetic circuits are the computational model for polynomials. This means that zk proofs are really just proving some polynomial. Polynomials are a concept you’ve probably learned in high school. Polynomials are mathematical expressions that can be formed from variables (e.g. x, y, z) and real numbers when the only operations you have are addition, subtraction, and multiplication.

e.g.

x² − 4x + 7 = x * x — 4 * x + 7

x³ + 2xyz2 − yz + 1 = x * x * x + 2 * x * y * z * z — y * z + 1

Our first step to get an arithmetic circuit is to get a polynomial expression. The computation we’ve chosen is x²–4x + 7, which is already a polynomial.

Arithmetic circuits are just a way to model these polynomial expressions. The way to form arithmetic circuits is to express this as a sequence of statements as variable assignment and mathematical binary operations such as multiplication and addition. The mathematical expressions shown above already use binary operators (+ and * are binary operators) but we’re rewriting this in a way that makes the structure of the arithmetic circuit explicit. For example, x²–4x + 7 could be expressed as

a = x * x

b = 4 * x

c = b * -1

d = a + c

e = d + 7

Arithmetic circuits can also be visualized as a directed acyclic graph where inbound edges are inputs and nodes are operations which assign the new values to their outbound edges. For example, x²–4x + 7 can be shown as

In the graph above we’ve made the operators red and the inputs (just x) blue.

So let’s assume you’ve converted your computation into an arithmetic circuit. How do you run it? Broadly speaking, any zk proof library should give you a facility to model your computations. In plonky2 this is done with a builder object. The builder object allows you to sequentially add your computations with its APIs. For our example of x²–4x + 7, it’ll look like the following:

// The arithmetic circuit.
let x = builder.add_virtual_target();
let a = builder.mul(x, x);
let b = builder.mul_const(F::from_canonical_u32(4), x);
let c = builder.mul_const(F::NEG_ONE, b);
let d = builder.add(a, c);
let e = builder.add_const(d, F::from_canonical_u32(7));

When we run plonky2, it’ll take this arithmetic circuit and compile it into a zk proof. Of course there’s more code to write, but the core aspect of the proof is the arithmetic circuit. While plonky2 or other zk proof libraries may provide other functions to model your computation on, those functions are ultimately just higher-level arithmetic circuits.

Note that virtual targets are not actual wires in the witness. You can think of these as the dynamic values in an execution trace. Some of which are dependent on public/private inputs and others are dependent on the result of a previous wire. When we compute the final proof/witness, these virtual targets become populated with concrete values.

In the example above, we’re merely building a circuit and generating a single plonky2 proof. In subsequent articles we’ll demonstrate how to recursively compose proofs in plonky2.

Full example

use anyhow::Result;
use plonky2::field::types::Field;
use plonky2::iop::witness::{PartialWitness, Witness};
use plonky2::plonk::circuit_builder::CircuitBuilder;
use plonky2::plonk::circuit_data::CircuitConfig;
use plonky2::plonk::config::{GenericConfig, PoseidonGoldilocksConfig};

/// An example of using Plonky2 to prove a statement of the form
/// "I know x² - 4x + 7".
fn main() -> Result<()> {
    const D: usize = 2;
    type C = PoseidonGoldilocksConfig;
    type F = <C as GenericConfig<D>>::F;

    let config = CircuitConfig::standard_recursion_config();
    let mut builder = CircuitBuilder::<F, D>::new(config);

    // The arithmetic circuit.
    let x = builder.add_virtual_target();
    let a = builder.mul(x, x);
    let b = builder.mul_const(F::from_canonical_u32(4), x);
    let c = builder.mul_const(F::NEG_ONE, b);
    let d = builder.add(a, c);
    let e = builder.add_const(d, F::from_canonical_u32(7));

    // Public inputs are the initial value (provided below) and the result (which is generated).
    builder.register_public_input(x);
    builder.register_public_input(e);
    let mut pw = PartialWitness::new();
    pw.set_target(x, F::from_canonical_u32(1));
    let data = builder.build::<C>();
    let proof = data.prove(pw)?;
    println!(
        "x² - 4 *x + 7 where x = {} is {}",
        proof.public_inputs[0],
        proof.public_inputs[1]
    );
    data.verify(proof)
}