Plonky3 recursion book

This book introduces the Plonky3 recursion stack, a Polygon Labs project, aimed at providing sufficient modularity and flexibility for developers, while maintaining high efficiency through its fixed recursive verifier design.

The material is organized to help potential contributors and users understand the motivation, construction and extensions of the recursive verifier.

Introduction

Plonky3 offers a comprehensive toolbox of cryptographic building blocks: hash functions, finite fields, and polynomial commitment schemes, ... to build tailored STARK proof systems. However, its adoption has been limited by the lack of native recursion, to allow arbitrary program execution replication in proof systems and to alleviate proof sizes and related on-chain verification costs.

This project aims at addressing this limitation, by proposing a minimal, fixed recursive verifier for Plonky3, which conceptual simplicity allows for blazing fast recursion performance. A key distinction with its predecessor plonky2, is that rather than wrapping a STARK proof in a separate plonkish SNARK, the Plonky3 recursion stack itself is built using Plonky3’s STARK primitives.

The source code is open-source, available at Plonky3 recursion and dual-licensed MIT/APACHE-2.

NOTE: This project is under active development, unaudited and as such not ready for production use. We welcome all external contributors who would like to support the development effort.

Recursion Approach and Construction

High-level architecture

Recursion in zero-knowledge proofs means using one proof to verify another: an (outer) prover will generate a proof to assert validity of an (inner) STARK proof. By applying this recursively, one obtains a (possibly compact) outer proof that attests to arbitrarily deep chains of computation.

Our approach to recursion for Plonky3 differs from a traditional zkVM approach: there is no program counter, instruction set, or branching logic. Instead, a fixed program is chosen, and the verifier circuit is specialized to this program only.

Why fixing the program shape?

• Performance: without program counter logic, branching, or instruction decoding, the verifier’s constraints are much lighter.

• Recursion efficiency: since the shape of the trace is predetermined, the recursion circuit can be aggressively optimized.

• Simplicity: all inputs follow the same structural pattern, which keeps implementation complexity low.

Limitations

• Rigidity: only the supported program(s) can be proven.

• No variable-length traces: input size must fit the circuit’s predefined structure.

• Reusability: adapting to a new program requires a new circuit.

The rest of this book explains how this approach is built, how to soften its rigidity, and why it provides a powerful foundation for recursive proof systems.

Execution IR

An Execution IR (intermediate representation) is defined to describe the steps of the verifier. This IR is not proved itself; it only guides trace population. The actual soundness comes from the constraints inside the operation-specific STARK chips along with their lookups into the central witness table.

Witness Table

The Witness table is a central bus that stores values shared across operations. It gathers the pairs (index, value) that will be accessed by the different chips via lookups to enforce consistency.

• The index column is preprocessed, or preprocessed [[rap]]: it is known to both prover and verifier in advance, requiring no online commitment.¹
• The Witness table values are represented as extension field elements directly (where base field elements are padded with 0 on higher coordinates) for addressing efficiency.

Operation-specific STARK Chips

Each operation family (e.g. addition, multiplication, Merkle path verification, FRI folding) has its own chip.

A chip contains:

• Local columns for its variables.
• Lookup ports into the witness table.
• An AIR that enforces its semantics.

Lookups

All chips interactions are performed via a lookup argument against the central Witness table. Enforcing multiset equality between chip ports and the Witness table entries ensures correctness without proving the execution order of the entire IR itself.

Below is a representation of the interactions between the main Witness table and the different chips.

%%{init: {'theme':'dark',"flowchart":{"htmlLabels":true}}}%%
flowchart TB
    subgraph P[PI Chip]
      P1["• Purpose: bind index=0 to the declared public input x."]
      P2["• Lookup: (0, x) must appear in Witness; also exposed as a public value."]
    end

    subgraph C[CONST Chip]
      C1["• Preprocessed rows: (1, 37), (3, 111), (4, 0)"]
      C2["• Lookup: preprocessed pairs must be present in Witness (aggregated lookup)."]
    end

    subgraph W[Witness Table]
      W0["0: 3 //      public input x"]
      W1["1: 37           // constant"]
      W2["2: 111        // p = 37 * x"]
      W3["3: 111          // constant"]
      W4["4: 0 // const (y = p - 111)"]
    end

    subgraph M[MUL chip]
      M1["• Ports: (0, x), (1, 37) → inputs; (2, p) → output."]
      M2["• AIR: x * 37 = p."]
    end

    subgraph S [ SUB Chip ]
      S1["• Ports: (2, p), (3, 111) → inputs; (4, y) → output."]
      S2["• AIR: p - 111 = y."]
    end

    W --- P
    W --- C
    W --- M
    W --- S

1. Preprocessed columns / polynomials can be reconstructed manually by the verifier, removing the need for a prover to commit to them and later perform the FRI protocol on them. However, the verifier needs $O(n)$ work when these columns are not structured, as it still needs to interpolate them. To alleviate this, the Plonky3 recursion stack performs offline commitment of unstructured preprocessed columns, so that we need only one instance of the FRI protocol to verify all preprocessed columns evaluations. ↩

Handling arbitrary programs

The fixed recursive verifier described in this book supports only fixed, predetermined programs.
This design choice maximizes performance but raises the question: how can one prove statements of varying size or complexity?

We highlight below two distinct approaches to alleviate this limitation and allow for arbitrary recursion

Tree-style recursion for variable-length inputs

One can split a large computation into chunks and prove each piece using a fixed inner circuit in parallel. These proofs can then be recursively aggregated in a tree structure, where each leaf of the tree corresponds to a prover portion of the computation. The tree root yields a single proof attesting to the validity of the entire computation.

A formal description of this tree-style recursion for STARKs can be seen in [[zktree]].

Flexible FRI verification

To support proofs with different FRI shapes, one can:

• Lift the proofs to a larger domain, as described in [[fri_lift]].
  Lifting allows a fixed circuit to efficiently verify proofs of varying trace sizes by projecting smaller domains into larger ones, reusing the original LDE and commitments without recomputation.

• Verify distinct proof shapes together inside a fixed FRI verifier circuit. Instead of having a single proof size that can be verified by a given FRI verifier circuit, one can extend it over a range of sizes instead at a minimal overhead cost. See a related implementation in plonky2 recursion: (Plonky2 PR #1635) for more details.

Benchmarks

This section will present empirical performance results for the Plonky3 recursion system, including instructions for reproducibility across target machines.

To be filled soon.

Bibliography