Plonky3 Recursion

This book is the user guide for Plonky3 recursion, an independent project providing native recursive STARK verification for Plonky3.

The library lets you verify Plonky3 STARK proofs inside circuits, chain recursive layers to compress proof size, and aggregate independent proofs into a single attestation. It is built entirely on Plonky3's own STARK primitives — no separate plonkish SNARK wrapper.

What this book covers

• Getting Started — Motivation, design philosophy, and a quick start guide with working examples.
• User Guide — The unified recursion API, aggregation, configuration, public inputs, integration into your project, and the low-level API for advanced use cases.
• Architecture & Internals — How the fixed recursive verifier is built: the execution IR, shared witness memory model, operation-specific chips, circuit building pipeline, trace generation, and Poseidon2-based hashing.
• Advanced Topics — Scaling strategies for variable-length inputs, performance tuning, soundness considerations, and debugging tools.
• Appendix — Benchmarks, roadmap, and glossary.

Quick links

• Source: github.com/Plonky3/Plonky3-recursion
• API docs: cargo doc --open
• Examples: recursion/examples/ — recursive Fibonacci, Keccak, and 2-to-1 aggregation
• License: Dual MIT / Apache-2.0

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.

Quick Start

Requirements

• Rust stable (edition 2024)
• For best performance: RUSTFLAGS="-Ctarget-cpu=native"

Add the dependency

Plonky3-recursion is not yet published on crates.io. Add it as a git dependency:

[dependencies]
p3-recursion = { git = "https://github.com/Plonky3/Plonky3-recursion", package = "p3-recursion" }

You will also need Plonky3 crates for fields, STARKs, and hashing. The recursion library re-exports what it needs, but your base prover setup will require direct Plonky3 dependencies.

Minimal example

The fastest way to verify a proof recursively:

use p3_recursion::{
    FriRecursionBackend, ProveNextLayerParams, RecursionInput,
    build_and_prove_next_layer, BatchOnly, Poseidon2Config,
};

// 1. You already have a Plonky3 STARK proof (uni-stark or batch-stark).
//    Wrap it in a RecursionInput.
let input = RecursionInput::UniStark {
    proof: &base_proof,
    air: &my_air,
    public_inputs: public_values.clone(),
    preprocessed_commit: None,
};

// 2. Create the FRI backend with a Poseidon2 config matching your field.
let backend = FriRecursionBackend::<16, 8>::new(Poseidon2Config::KOALA_BEAR_D4_W16)
    .for_extension_degree::<4>();

// 3. Prove. This builds the verifier circuit, runs it, and produces a batch-STARK proof.
let params = ProveNextLayerParams::default();
let output = build_and_prove_next_layer::<_, _, _, 4>(
    &input, &config, &backend, &params,
)?;

// 4. Chain further layers by converting the output back to an input.
let next_input = output.into_recursion_input::<BatchOnly>();
let output_2 = build_and_prove_next_layer::<_, _, _, 4>(
    &next_input, &config, &backend, &params,
)?;

The config (&config) must implement FriRecursionConfig. KoalaBearD4Poseidon2BinaryConfig is the built-in suite that implements it directly. The other native FRI factories provide validated building blocks; using them with this recursion API requires a local StarkGenericConfig wrapper and FriRecursionConfig implementation. See the Integration Guide for that contract, or the Examples for working code. This one-shot API transports the proof's attached metadata; use a trusted prepared owner when independently fixed relation and statement authority is required.

Running the examples

Three examples ship with the library:

# Recursive Keccak (uni-STARK base proof)
cargo run --release --example recursive_keccak -- --field koala-bear --num-hashes 100

# Recursive Fibonacci (batch-STARK base proof built with CircuitBuilder)
cargo run --release --example recursive_fibonacci -- --field koala-bear --n 1000

# 2-to-1 aggregation (binary tree of proofs)
cargo run --release --example recursive_aggregation -- --field koala-bear

Each example also accepts --quintic (KoalaBear only) and --hash <poseidon2|poseidon1> (default poseidon2), e.g. --field baby-bear --hash poseidon1.

Add --features parallel and RUSTFLAGS="-Ctarget-cpu=native" for production-level performance.

Examples

The three recursive examples select their polynomial commitment scheme with --pcs fri|whir (default fri). WHIR supports BabyBear, KoalaBear, and Goldilocks with either --hash poseidon2 or --hash poseidon1, retaining the same base computations and configurable recursion depth. KoalaBear also supports its quintic challenge extension with --pcs whir --quintic and either hash family. --zk, --disable-recompose-npo, and aggregation's --arity4 require FRI.

cargo run --release --example recursive_fibonacci -- --pcs whir --n 1000 --num-recursive-layers 2
cargo run --release --example recursive_keccak -- --pcs whir --num-hashes 100 --num-recursive-layers 2
cargo run --release --example recursive_aggregation -- --pcs whir --num-recursive-layers 2

For WHIR, --log-blowup controls the starting inverse rate, --query-pow-bits controls the maximum PoW budget, and --whir-folding-factor controls the number of variables folded per round (default 4). --security-level defaults to 64 for WHIR and 124 for FRI. FRI's --max-log-arity, --log-final-poly-len, and --commit-pow-bits do not configure WHIR.

This section walks through the three provided examples to illustrate common recursion patterns.

Recursive Keccak — verifying a uni-STARK proof

Source: recursion/examples/recursive_keccak.rs

This example starts from a standard Plonky3 uni-STARK proof of the Keccak AIR, then recursively verifies it through multiple layers.

Flow:

1. Generate a Keccak trace and prove it with p3_uni_stark::prove.
2. Wrap the resulting Proof<SC> in a RecursionInput::UniStark.
3. Call build_and_prove_next_layer — this builds a verification circuit that checks the Keccak proof, runs it, and produces a batch-STARK proof.
4. For subsequent layers, convert the output with output.into_recursion_input::<BatchOnly>() and repeat.

The key point: the first recursive layer handles a uni-STARK proof (potentially large, depending on the AIR width). After that, every layer verifies the previous layer's batch-STARK proof, which has a predictable, smaller structure. This is why layer 1 is typically slower than layers 2+.

cargo run --release --example recursive_keccak -- \
    --field koala-bear --num-hashes 1000 --num-recursive-layers 3

Recursive Fibonacci — verifying a batch-STARK proof

Source: recursion/examples/recursive_fibonacci.rs

This example builds a Fibonacci circuit from scratch using CircuitBuilder, proves it with BatchStarkProver, then recurses.

Flow:

1. Build the circuit: CircuitBuilder::new(), add constants, public inputs, arithmetic, connect, build.
2. Run and prove the base circuit with BatchStarkProver.
3. Wrap the output in RecursionOutput (since it's already a batch proof), then use into_recursion_input::<BatchOnly>().
4. Call build_and_prove_next_layer in a loop for each recursive layer.

This example demonstrates how to use the CircuitBuilder for your own computations and then feed the resulting proof into the recursion pipeline.

cargo run --release --example recursive_fibonacci -- \
    --field koala-bear --n 10000 --num-recursive-layers 3

Recursive Aggregation — 2-to-1 proof merging

Source: recursion/examples/recursive_aggregation.rs

This example produces multiple independent base proofs and aggregates them pairwise in a binary tree.

Flow:

1. Produce 2^depth independent base proofs (each proving a different constant).
2. At each tree level, pair up proofs and call build_and_prove_aggregation_layer on each pair.
3. Repeat until a single root proof remains.

The aggregation circuit verifies two proofs in a single circuit — left and right children — producing one output proof. The two inputs may be different kinds of RecursionInput (e.g., one UniStark and one BatchStark), though in this example they are all BatchStark.

# 4 base proofs, 2 aggregation levels
cargo run --release --example recursive_aggregation -- \
    --field koala-bear --num-recursive-layers 2

Common CLI flags

All three examples accept the same selectors for the recursive verifier's field and hash:

• --field <koala-bear|baby-bear|goldilocks> — base field (default koala-bear).
• --quintic — use the quintic (D = 5) challenge extension (KoalaBear only).
• --hash <poseidon2|poseidon1> — permutation backing the Fiat-Shamir challenger and MMCS (default poseidon2).

cargo run --release --example recursive_fibonacci -- \
    --field baby-bear --hash poseidon1 --n 10000 --num-recursive-layers 3

Common patterns across examples

All three examples share the same setup pattern:

1. Config wrapper: A ConfigWithFriParams struct that wraps a StarkConfig and adds FriVerifierParams. It implements StarkGenericConfig (by delegating) and FriRecursionConfig.

2. Backend creation: FriRecursionBackend::<WIDTH, RATE>::new(poseidon2_config).

3. Table packing: Adjusted per layer — the first layer may need different packing than subsequent layers because the verification circuit has a different shape.

4. Verification after proving: Each example verifies the proof it just produced, using BatchStarkProver::verify_all_tables.

See the Integration Guide for how to adapt this pattern to your own project.

Unified Recursion API

The library exposes a unified API that handles both uni-STARK and batch-STARK proofs through a single set of entry points.

Core types

RecursionInput

Wraps the proof to verify at each recursion step:

pub enum RecursionInput<'a, SC, A> {
    /// A single-instance STARK proof (e.g. from p3-uni-stark).
    UniStark {
        proof: &'a Proof<SC>,
        air: &'a A,
        public_inputs: Vec<Val<SC>>,
        preprocessed_commit: Option<<SC::Pcs as Pcs<SC::Challenge, SC::Challenger>>::Commitment>,
    },
    /// A batch STARK proof (e.g. from p3-batch-stark or circuit-prover).
    BatchStark {
        proof: &'a BatchStarkProof<SC>,
        common_data: &'a CommonData<SC>,
        table_public_inputs: Vec<Vec<Val<SC>>>,
    },
}

Use UniStark when verifying an external Plonky3 proof (e.g. Keccak AIR). Use BatchStark when verifying a proof produced by this library's own prover.

RecursionOutput

The output of one recursion step:

pub struct RecursionOutput<SC>(pub BatchStarkProof<SC>, pub Arc<CircuitProverData<SC>>);

Contains the batch-STARK proof and prover data in an Arc. The latter is a compatibility handle, not independent verifier authority. Convert to an expert RecursionInput using proof-attached table public values:

let next_input = output.into_recursion_input::<BatchOnly>();

For trusted chaining, retain a CircuitVerifier separately and call output.into_trusted_recursion_input::<BatchOnly>(&verifier, &expected_statement). That method derives the per-table public vectors from the verifier's retained relation.

The BatchOnly marker type satisfies the RecursiveAir bound without carrying any AIR data — it's a no-op used when the next layer only needs to verify the recursive batch proof.

ProveNextLayerParams

Controls the proving pipeline:

pub struct ProveNextLayerParams {
    pub table_packing: TablePacking,
    pub constraint_profile: ConstraintProfile,
}

• table_packing: How to distribute operations across table lanes. See Configuration.
• constraint_profile: Which AIR variants the prover uses for this layer (ConstraintProfile::Standard for normal use).

The default is TablePacking::new(1, 4) with ConstraintProfile::Standard.

Entry points

build_and_prove_next_layer

The simplest way to prove one recursion step. Builds the verifier circuit, runs it, and proves it in one call:

let output = build_and_prove_next_layer::<SC, A, B, D>(
    &input, &config, &backend, &params,
)?;

PreparedLayer (repeated proving)

For repeated invocations, let an owner capture the native input contract and retain the verifier circuit, configuration, and prepared proving data together:

let owner = PreparedLayer::<SC, A, B, D>::new(
    PreparedSource::UniStark { air, proof, public_inputs, preprocessed_commit },
    config,
    backend,
    params,
)?;

// Check the native contract before each repeated proof.
owner.check_input(&input)?;
let output = owner.prove(input)?;

PreparedLayer owns the committed preprocessed columns and prover, and rejects malformed or incompatible native inputs before proving. Use a new owner when the native contract changes.

This compatibility check is shape-only: a prepared owner does not bind child proving keys, recursion statements, or public claims. Use TrustedPreparedLayer when the verifier relation must be fixed independently of each proof. Its TrustedPreparedSource::UniStark retains the trusted native config, AIR and preprocessing commitment; its BatchStark source retains a CircuitVerifier. TrustedPreparedInput supplies only a proof and caller-expected statement. The owner can export an independently retained verifier for its output. See the compiled prelude example and trusted layer tests.

build_and_prove_aggregation_layer

Verifies two proofs in a single circuit. The two inputs can be different RecursionInput variants:

let output = build_and_prove_aggregation_layer::<SC, A1, A2, B, D>(
    &left, &right, &config, &backend, &params,
)?;

PreparedAggregation (repeated aggregation)

For repeated aggregation at one compatible level, retain both verifier results and prepared proving data in an owner. Check both borrowed inputs before each reuse; construct a new owner when either native contract changes:

let owner = PreparedAggregation::new(
    PreparedSource::batch(&left_proof, &left_common_data, &left_table_public_inputs),
    PreparedSource::batch(&right_proof, &right_common_data, &right_table_public_inputs),
    config,
    backend,
    params,
)?;

let left = PreparedInput::BatchStark {
    proof: &left_proof,
    common_data: &left_common_data,
    table_public_inputs: &left_table_public_inputs,
};
let right = PreparedInput::BatchStark {
    proof: &right_proof,
    common_data: &right_common_data,
    table_public_inputs: &right_table_public_inputs,
};
owner.check_inputs(&left, &right)?;
let output = owner.prove(left, right)?;

As with PreparedLayer, this owner checks native shape compatibility only. Use TrustedPreparedAggregation to retain both child authorities and their left/right statement layout. Supply each child's expected statement on every proof attempt; see the trusted aggregation tests.

prove_aggregation_layer

The split build/prove variant is an expert API. Follow the checked build_aggregation_layer_circuit and prove_aggregation_layer signatures if you need to manage the circuit and verifier results directly.

Recursion loop pattern

A typical recursion loop looks like this:

let backend = FriRecursionBackend::<16, 8>::new(Poseidon2Config::KOALA_BEAR_D4_W16)
    .for_extension_degree::<4>();

// Layer 1: verify the base proof
let input = RecursionInput::UniStark { proof: &base_proof, air: &my_air, .. };
let mut output = build_and_prove_next_layer::<_, _, _, 4>(&input, &config, &backend, &params)?;

// Layers 2..N: verify the previous recursive proof
for _ in 2..=num_layers {
    let input = output.into_recursion_input::<BatchOnly>();
    output = build_and_prove_next_layer::<_, _, _, 4>(&input, &config, &backend, &params)?;
}

After enough layers, the recursive proof reaches a steady-state size — further layers don't meaningfully change the proof dimensions.

Type parameter D

The const generic D is the extension field degree. Built-in BabyBear and KoalaBear binomial suites use D = 4; Goldilocks uses D = 2. KoalaBear quintic FRI uses D = 5 through FriRecursionBackendD5, with a base-field (D1) challenger permutation. The built-in WHIR suites use D = 4.

FriRecursionBackend

FriRecursionBackend::for_extension_degree::<D>() returns a degree-tagged backend that implements PcsRecursionBackend for the matching FRI-based config. It handles:

• Preparing the circuit for verification (enabling the challenger permutation and NPOs)
• Building the verifier circuit (delegating to verify_p3_uni_proof_circuit or verify_p3_batch_proof_circuit)
• Packing public inputs
• Setting Merkle path private data

WIDTH and RATE describe the challenger permutation: 16 and 8 for BabyBear/KoalaBear, or 8 and 4 for Goldilocks. C is the challenger config (Poseidon1Config or Poseidon2Config); use _ in the type arguments to infer it from new.

// Standard Poseidon2 backend
let backend = FriRecursionBackend::<16, 8>::new(Poseidon2Config::KOALA_BEAR_D4_W16)
    .for_extension_degree::<4>();

// Quaternary FRI: narrow challenger, wider Poseidon2 MMCS table
let quaternary = FriRecursionBackend::<16, 8, _>::new(Poseidon2Config::KOALA_BEAR_D4_W16)
    .with_extra_poseidon2_table(Poseidon2Config::KOALA_BEAR_D4_W32)
    .for_extension_degree::<4>();

// KoalaBear quintic FRI: the challenger uses D1 base-field Poseidon lanes
let quintic = FriRecursionBackend::<16, 8, _>::new_d5(
    Poseidon2Config::KOALA_BEAR_D1_W16,
);

FriRecursionBackendD5 handles the supported quintic (D = 5) variant; FriRecursionBackendForExt<D> tags binomial extension degrees such as 2 and 4. For Poseidon1 suites, select the matching p3_recursion::ops::Poseidon1Config constant in new or new_d5. Quaternary built-ins use Poseidon2 and require the matching wide table; binary and hiding FRI do not add one. See built-in backend selection for the suite map and FRI table shapes.

WhirRecursionBackend

The BabyBear and KoalaBear built-in WHIR suites use a Poseidon2 challenger, binary commitments, and a degree-4 extension:

let backend = p3_recursion::backend::whir::WhirRecursionBackend::<16, 8>::new(
    Poseidon2Config::BABY_BEAR_D4_W16,
).for_extension_degree::<4>();

Choose recursively admissible WHIR geometry as described in Configuration.

Aggregation

The library supports 2-to-1 recursive aggregation: verifying two proofs inside a single circuit and producing one output proof. This enables binary tree aggregation of independent computations.

How it works

An aggregation circuit contains two verifier sub-circuits sharing the same CircuitBuilder. Both verifications use the matching permutation tables and primitive chips. The combined circuit is then proved as a single batch-STARK.

       ┌────────────────────────┐
       │   Aggregation Circuit  │
       │                        │
       │  ┌──────┐  ┌──────┐   │
       │  │Verify│  │Verify│   │
       │  │ left │  │right │   │
       │  └──────┘  └──────┘   │
       │                        │
       └────────────────────────┘
                  │
            One batch-STARK
               proof out

The left and right inputs are independent — they can be different RecursionInput variants (e.g., one UniStark and one BatchStark), and they can verify different AIRs entirely.

API

use p3_recursion::{
    build_and_prove_aggregation_layer, RecursionInput, BatchOnly,
    FriRecursionBackend, ProveNextLayerParams, Poseidon2Config,
};

let left = RecursionInput::UniStark {
    proof: &proof_a, air: &air_a, public_inputs: pis_a.clone(), preprocessed_commit: None,
};
let right = RecursionInput::UniStark {
    proof: &proof_b, air: &air_b, public_inputs: pis_b.clone(), preprocessed_commit: None,
};

let backend = FriRecursionBackend::<16, 8>::new(Poseidon2Config::KOALA_BEAR_D4_W16)
    .for_extension_degree::<4>();
let params = ProveNextLayerParams::default();

let output = build_and_prove_aggregation_layer::<_, _, _, _, 4>(
    &left, &right, &config, &backend, &params,
)?;

The output is a regular RecursionOutput and can be fed into further aggregation or recursion layers via into_recursion_input::<BatchOnly>(). That helper carries proof-attached values; use TrustedPreparedAggregation with independently retained child verifier authority and caller-expected statements when aggregating trusted relations.

Composing state transitions

Use TrustedPreparedAggregation::new_state_transition when each trusted child proves a transition with the exact statement schema state_schema || state_schema || [Base]. Its values are ordered [initial_state coefficients, final_state coefficients, count]. The constructor takes the same left and right TrustedPreparedSources, output config, backend, and parameters as new, plus a StateTransitionLayout:

use p3_circuit::StateTransitionLayout;
use p3_recursion::TrustedPreparedAggregation;

let layout = StateTransitionLayout::base(2, 4)?; // two Base state coefficients; 4 count bits
let owner = TrustedPreparedAggregation::new_state_transition(
    left_source, right_source, output_config, backend, params, layout.clone(),
)?;
let output = owner.prove(left_input, right_input)?;

For example, [10, 20, 13, 26, 3] followed by [13, 26, 20, 40, 7] produces [10, 20, 20, 40, 10]. The merger connects every left final-state coefficient to the corresponding right initial-state coefficient, adds the two counts, and exports the left initial state, right final state, and sum. All child schemas must equal the layout exactly, including semantic StatementField boundaries. Use StateTransitionLayout::try_new(state_schema, count_bits) for a state schema containing extension fields.

Counts are canonical nonnegative integers from 0 through 2^b - 1, where b = count_bits. The layout requires 2 * (2^b - 1) < p for the base-field modulus p; each child count and their sum must also fit in b bits. These checks make addition an ordinary integer sum without field wraparound. Zero is allowed; the authorized leaf relation defines what a zero-count transition means and what the count measures. The merger only adds the counts asserted by those child relations.

The prepared owner can prove multiple compatible pairs with different states and counts. At each level, supply each child's proof and caller-expected statement; retain the child verifier authority independently. The application should also retain its own expected root statement and verify the final proof against it, including when using a portable verifier. The same concrete base-field type is supported across the input and output configurations of a prepared owner. The FRI and WHIR backends each support this constructor with that field type.

TrustedPreparedAggregation::new still exports the ordered concatenation of its child statements. Transition composition exports a compact statement of the same width as one child, and its verifier has no concat-specific aggregation_statement_layout() metadata. The compiled verifier relation enforces the transition rules. See the layout implementation, prepared constructor, and two-level FRI transition test for the API, prepared reuse, and portable root verification.

When child proofs arrive as serialized artifacts, typed import checks each proof against an independently pinned verifier and caller-expected statement before its as_source() or as_input() view enters a prepared owner.

Tree aggregation

To aggregate N independent proofs, arrange them as leaves of a binary tree and aggregate pairwise, bottom up:

Level 0 (leaves):  P0   P1   P2   P3
                    \  /      \  /
Level 1:           Agg01    Agg23
                      \    /
Level 2 (root):      Root

At each level, every pair is aggregated independently — this is embarrassingly parallel.

let mut proofs: Vec<RecursionOutput<SC>> = base_proofs;

while proofs.len() > 1 {
    let mut next = Vec::new();
    for pair in proofs.chunks(2) {
        let left = pair[0].into_recursion_input::<BatchOnly>();
        let right = pair[1].into_recursion_input::<BatchOnly>();
        let out = build_and_prove_aggregation_layer::<_, _, _, _, 4>(
            &left, &right, &config, &backend, &params,
        )?;
        next.push(out);
    }
    proofs = next;
}
// proofs[0] is the root proof

Cost

An aggregation circuit is roughly twice the size of a single-verification circuit (two verifiers in one circuit). Matching permutation tables are shared, so the overhead is less than 2x for hash-heavy proofs.

Adjust TablePacking for aggregation circuits — they produce wider traces than single-verification circuits. See Configuration for guidance.

Configuration

This section covers the parameters you need to choose when setting up recursive verification.

Field selection

Native FRI factories include these base fields:

BabyBear and KoalaBear have degree-4 binomial suites. KoalaBear also has a degree-5 quintic suite. All 19 registered FRI configuration aliases implement FriRecursionConfig; both registered WHIR aliases implement WhirRecursionConfig. Their factories validate native parameters, while recursive proving also requires a matching backend and admissible proof geometry. For the seven generic random-codeword and salted FRI aliases, recursion and typed artifact import additionally require R: CryptoRng + SeedableRng + Send + Sync + 'static; the native factories require only CryptoRng + SeedableRng. See the integration guide for custom configurations.

Built-in native configuration suites

The V1 suite registry defines the following 21 native suites. D is the challenge extension degree; arity is the commitment tree arity. Every row is constructed by its typed native FRI or WHIR factory and proves and verifies a bounded Fibonacci trace in builtin_config_proofs.rs.

builtin_config_native.rs additionally checks that each factory retains its descriptor and native parameters. The ordinary FRI proof tests use 8-row traces, the hiding FRI tests use 32-row traces, and the WHIR tests use 64-row traces. The hiding tests use independent seeded proving and verifying RNGs and check that verification draws no RNG. These small parameters establish factory interoperability, not a production security level; choose security parameters for your application.

The binary FRI, quaternary FRI, hiding FRI, and WHIR lifecycle tests cover the 21 concrete aliases: prepared reuse, typed artifact reentry, a second recursive layer, and portable verification against independent expected statements. The typed importer uses the application-supplied native configuration, including its hiding RNG setup; a separate output configuration is supplied to the recursive owner. Custom recursion configurations remain an extension route for setups outside the registered aliases. The artifact round-trip tests cover representative native suites, while the recursive artifact round-trip uses that KoalaBear binary suite. Binary-field foundations are partial and are outside this native suite matrix.

The PR CI matrix runs workspace tests with default and all features, each with and without AVX2. It therefore runs these bounded factory proof tests on every PR. The weekly assurance workflow runs a separate bounded seeded verifier corpus; it does not replace the 21-suite native factory checks.

Choosing a built-in recursion backend

Choose the backend from the native suite's challenger permutation. For binary FRI, random-codeword FRI, and salted FRI, its MMCS uses the same permutation width. The four registered quaternary suites all use Poseidon2: they keep the narrower challenger backend and register the wider MMCS table separately with with_extra_poseidon2_table:

The two D5 FRI challengers use a quintic extension for proof challenges but base-field (D1) Poseidon lanes. new_d5 requires a D1 challenger config; the quaternary D5 MMCS table is also D1. Match Poseidon1 versus Poseidon2 as well as the field, width, rate, extension degree, and native Merkle arity. Keep input_cap_height and commit_cap_height distinct when choosing FRI parameters; the built-in configuration retains both for path restoration. For hiding suites, provide the native proving RNGs through the application configuration; typed import retains it. Salted FRI path restoration constructs private, fixed-seed MMCS helpers for verification only. Those helpers never commit or draw randomness and do not replace the retained proving config.

Both WHIR aliases use Poseidon2, D4, and binary Merkle commitments. The built-in WhirConfigV1 descriptor still specifies one constant folding factor. Custom WHIR recursion backends support Poseidon1 or Poseidon2 at D2 or D4. The input PCS permutation must match the backend challenger after table-role normalization, including its family and full configuration. Its field must match Val<SC>, its width and rate must match the backend, and the actual SC::Challenge dimension must equal the backend D. The permutation's own degree may differ from that D (for example, a D1 permutation in a D4 circuit). The output PCS may use different protocol parameters and a different permutation. Input and output configurations still use the same base and challenge fields and backend degree, with compatible domains. Statement-bound parents chain through their retained trusted verifier. For a custom WhirUniPcs and WhirUniVerifierParams, the recursive verifier supports native FoldingFactor::Constant, ConstantFromSecondRound, and PerRound with positive factors, canonical Prefix or Suffix variable order, unstratified query sampling, and binary commitments. The first fold controls table padding; the complete strategy is retained for native WHIR configuration and transcript seeding. Every commitment's stacked arity must fit that strategy exactly. In particular, a PerRound vector must supply exactly the factors used at each commitment arity, so one vector may not fit both leaf and recursive trace sizes. An explicit round-rate schedule must likewise match the intermediate round count derived from each commitment's stacked arity; leave ProtocolParameters::round_log_inv_rates empty to derive rates automatically for each arity when leaf and recursive trace sizes differ. In any intermediate or final phase where the raw configured query count reaches or exceeds domain_size >> folding_factor, the verifier opens the entire folded domain in ascending order and makes no query-index challenger draws. The effective opening count is the minimum of the raw count and folded domain size; the raw count remains part of the canonical security configuration. The public low-level WhirVerifierParams::from_config and verify_whir_circuit path accepts canonical, unstratified Prefix and Suffix variable orders. Its query-index circuit currently consumes one base-field sample per unsaturated query, so native uniform-bit rejection or resampling is outside the supported transcript cases. Custom univariate recursion supports the two native canonical layouts, including prepared proof production under a custom Suffix configuration. Arbitrary layouts with independent selector and fold-order settings are outside this adapter's contract. The registered V1 aliases and descriptors remain Prefix with Constant folding; no portable Suffix artifact format is registered. The WHIR descriptor's cap height is retained when restoring paths.

FRI parameters

FRI parameters control the trade-off between proof size, verifier cost, and security level.

Security level

The number of FRI queries is derived as:

num_queries = (target_security_bits - query_pow_bits) / log_blowup

With default parameters (target = 100 bits, query_pow_bits = 16, log_blowup = 3):

num_queries = (100 - 16) / 3 = 28

See related section in the Soundness and Security chapter for a more thorough analysis of the security estimate in the light of recent findings against the underlying assumptions used in these heuristics.

Intermediate layer relaxation

For intermediate recursive layers (not the final one), soundness requirements compose, so relaxed parameters can be used:

• query_pow_bits = 20, num_queries = 26 — saves 2 queries worth of in-circuit work
• query_pow_bits = 24, num_queries = 25 — more aggressive, suitable for deeply nested layers

The outermost (final) layer should use full-strength parameters.

FriVerifierParams

The recursion circuit uses FriVerifierParams to know the FRI structure without accessing the native FriParameters directly:

let fri_verifier_params = FriVerifierParams::try_with_mmcs(
    log_blowup,
    log_final_poly_len,
    max_log_arity,
    commit_pow_bits,
    query_pow_bits,
    num_queries,
    poseidon2_config,
)?;

This is stored in your config wrapper and returned via FriRecursionConfig::pcs_verifier_params().

Poseidon2 configuration

Poseidon2Config provides named constants for in-circuit permutation parameters:

For a degree-4 suite using width 16, select the D4_W16 constant matching your field. The wider W16/W32 entries above describe quaternary MMCS tables; the backend WIDTH and RATE type parameters still describe the narrow challenger. Choose the backend degree tag to match the circuit extension, for example FriRecursionBackend::new(Poseidon2Config::KOALA_BEAR_D4_W16).for_extension_degree::<4>() for trusted prepared recursion.

The Poseidon2Config must be consistent between:

• The FriRecursionBackend constructor
• The FriVerifierParams
• The Poseidon2 permutation enabled on the CircuitBuilder

Table packing

TablePacking controls how circuit operations are distributed across table lanes. Each lane adds columns to a table; more lanes means shorter (fewer rows) but wider (more columns) tables.

TablePacking::new(public_lanes, alu_lanes)

The total row count of each table is ceil(num_ops / num_lanes), padded to the next power of two. The maximum table height across all tables determines the FRI polynomial degree and dominates proving cost.

Choosing packing values

The goal is to balance table heights so no single table forces a large power-of-two padding.

Example — a recursive verification circuit with ~43K public ops and ~60K ALU ops (columns are public_lanes, alu_lanes):

Halving the max table height cuts FRI proving time by roughly 40-50% (one fewer folding round, half the polynomial size).

Use .with_fri_params(log_final_poly_len, log_blowup) to set minimum row counts:

let packing = TablePacking::new(2, 3)
    .with_fri_params(log_final_poly_len, log_blowup);

Layer-specific packing

The first recursive layer (verifying the original proof) often has a different operation distribution than subsequent layers. It's common to use different packing per layer:

let packing = if layer == 1 {
    TablePacking::new(1, 1)
} else {
    TablePacking::new(1, 3)
}.with_fri_params(log_final_poly_len, log_blowup);

Public Inputs

Public inputs are the values the verifier knows — they connect the circuit to the proof being verified. In recursive verification, the previous proof's commitments, opened values, and challenges become public inputs to the recursive circuit.

How public inputs flow

When a verifier circuit is built, it allocates public input targets in a specific order. At proving time, concrete values must be packed in exactly the same order. If the order doesn't match, the proof will fail.

Base proof (commitments, openings, challenges)
         │
         ▼
┌─────────────────────────┐
│   pack_public_inputs()  │  ← extracts values from the proof in allocation order
└─────────────────────────┘
         │
         ▼
   runner.set_public_inputs(&packed_values)

Automatic packing via the unified API

When using prove_next_layer or build_and_prove_next_layer, public input packing is handled automatically. The VerifierCircuitResult::pack_public_inputs method extracts values from the RecursionInput in the correct order.

You don't need to interact with the builders directly unless you're using the low-level API.

Manual packing (low-level API)

If building the verification circuit manually, use the dedicated builders:

StarkVerifierInputsBuilder (uni-STARK)

Returned by verify_p3_uni_proof_circuit. Packs values from a Proof<SC>:

let public_inputs = verifier_inputs.pack_public_values(
    &air_public_inputs,
    &proof,
    &preprocessed_commit,
);
runner.set_public_inputs(&public_inputs)?;

BatchStarkVerifierInputsBuilder (batch-STARK)

Returned by verify_p3_batch_proof_circuit. Packs values from a BatchProof<SC> and CommonData<SC>:

let public_inputs = verifier_inputs.pack_public_values(
    &table_public_inputs,
    &batch_proof,
    &common_data,
);
runner.set_public_inputs(&public_inputs)?;

PublicInputBuilder (generic)

For custom circuits (not recursive verification), use the generic builder:

let mut builder = PublicInputBuilder::new();
builder
    .add_proof_values(proof_values)
    .add_challenge(alpha)
    .add_challenges(betas);
let public_inputs = builder.build();

Public inputs in aggregation

For aggregation circuits, the internal verifier inputs from both child proofs are packed left first, then right. This is handled automatically by prove_aggregation_layer and by prepared aggregation owners:

let mut public_inputs = left_result.pack_public_inputs(&left)?;
public_inputs.extend(right_result.pack_public_inputs(&right)?);

This packing order is separate from the public statement exported by the parent proof. TrustedPreparedAggregation::new exports the two child statements in left-right order. With TrustedPreparedAggregation::new_state_transition, each child statement has the exact schema state_schema || state_schema || [Base] and values [initial_state coefficients, final_state coefficients, count]; the parent exports [left.initial_state, right.final_state, left.count + right.count]. Its statement has the same width and schema as either child, even though the internal verifier still packs both proofs' inputs. See state-transition composition.

Integration Guide

This section explains how to connect a native Plonky3 prover to recursive verification.

Choose a native config

The 19 built-in FRI aliases implement FriRecursionConfig, and the two built-in WHIR aliases implement WhirRecursionConfig. Use a matching backend and parameters that the recursive verifier accepts; native factory validation alone does not establish recursive admissibility. The built-in FRI integration and WHIR integration show how each family prepares the circuit and restores opening witnesses. For generic random-codeword and salted FRI configs, recursion and typed import require R: CryptoRng + SeedableRng + Send + Sync + 'static; native factory construction itself requires only CryptoRng + SeedableRng.

For a custom PCS setup outside those aliases, implement FriRecursionConfig or WhirRecursionConfig on a StarkGenericConfig wrapper. The FRI contract supplies verifier target types, matching FRI parameters, circuit preparation, and opening witness restoration. In particular, set_fri_private_data receives the config and an OpeningTranscript; restore each query's Merkle path from the proof's pruned multiproof before calling set_fri_mmcs_private_data. The trait's rustdoc and the built-in implementation show the current signature and transcript steps. Match the native prover parameters, including query count and MMCS permutation.

Verify your AIR

AIRs implementing Plonky3's Air trait get a blanket RecursiveAir implementation from the symbolic constraint system. If your AIR needs a manual implementation, follow the current RecursiveAir trait, including its trace-length and lookup-aware quotient-degree calculation. For trusted prepared uni-STARK verification, expected_public_input_count must identify the fixed public-input width.

Wrap a native proof in RecursionInput::UniStark for one-shot recursion, or construct TrustedPreparedSource::UniStark with the trusted config, AIR, and preprocessing commitment for repeated verification. See the compiled prelude example and trusted layer tests for the prepared contract. Use FriRecursionBackend::new(challenger_config).for_extension_degree::<D>() for a matching binomial extension, FriRecursionBackend::new_d5 for a KoalaBear quintic suite, or WhirRecursionBackend::new(...).for_extension_degree::<D>() for WHIR, where D is 2 or 4 and matches the input's actual challenge dimension. See backend selection.

Import portable artifacts into trusted recursion

Use TypedArtifactVerifier<SC> when a serialized verifier and proof must enter a TrustedPreparedLayer or TrustedPreparedAggregation. Provision the expected verifier bytes through an independent trusted channel, choose the matching application-owned native SC configuration, and set ArtifactLimits. The candidate verifier must match the pinned bytes exactly and its complete built-in configuration descriptor must match the supplied configuration; matching only the field or suite is insufficient. The sealed PortableArtifactImport trait exposes this import for supported built-in configurations. The typed importer keeps that configuration and those limits for subsequent proof imports.

use p3_recursion::artifact::{
    ArtifactLimits, CanonicalStatement, ExpectedVerifierArtifact,
    PortableArtifactImport, TypedArtifactVerifier,
};

let authority = TypedArtifactVerifier::<Config>::decode_with_config(
    app_config,
    candidate_verifier_bytes,
    ExpectedVerifierArtifact::from_trusted_bytes(pinned_verifier_bytes),
    ArtifactLimits::default(),
)?;
let verified = authority.import_proof(
    proof_bytes,
    CanonicalStatement::new(expected_statement_bytes, statement_width),
)?;

Encode expected values as canonical base-field coefficients in schema order: little-endian 4-byte words for BabyBear/KoalaBear or 8-byte words for Goldilocks, with statement_width == authority.schema().base_len(). The CanonicalStatement bytes have no length prefix.

The application supplies expected_statement_bytes independently of the proof attachment. import_proof decodes under the retained limits and verifies the native proof against that expected statement before returning a VerifiedArtifactProof<SC>. Its statement() and trusted_identity_bytes() accessors report the checked statement and pinned identity. as_source() supplies the retained verifier authority and a representative proof when preparing a trusted owner; as_input() supplies a proof and expected statement for a compatible prepared owner's prove call. The destination owner still checks its own retained relation and input contract. Imported proofs own their native data and remain usable after the input byte buffers and importer are dropped.

The caller-supplied configuration matters for hiding suites: typed import retains its application-controlled RNG setup. Salted FRI path restoration may construct a private, fixed-seed MMCS helper for verification; it draws no randomness and is not exposed as the proving configuration. PortableVerifier can verify encoded proofs but does not expose a native configuration or proving authority. Typed import supports the library's built-in artifact codecs; the 19 FRI and two WHIR aliases have corresponding direct recursion integrations for admissible parameters. An output proving configuration and backend are selected separately when constructing the trusted prepared owner. See configuration support and transition aggregation.

The portable aggregation example runs trusted setup, proof production, aggregation, and final verification in separate processes:

cargo run --locked --release -p p3-recursion --example portable_aggregation -- setup --trusted-dir ./demo-auth
cargo run --locked --release -p p3-recursion --example portable_aggregation -- produce --out-dir ./demo-children
cargo run --locked --release -p p3-recursion --example portable_aggregation -- aggregate --trusted-dir ./demo-auth --children-dir ./demo-children --out-dir ./demo-root
cargo run --locked --release -p p3-recursion --example portable_aggregation -- verify --trusted-dir ./demo-auth --root-dir ./demo-root --expected 10,20,20,40,10

Run with fresh output directories. Setup provisions demo-auth/leaf.verifier and demo-auth/root.verifier from a separate valid fixture, before the producer artifacts are consumed; it does not produce the root proof. The producer writes demo-children/leaf.verifier and four leaf-0.proof through leaf-3.proof payloads. Aggregation checks the child verifier against the trusted leaf pin, imports all four proofs with independently specified statements, reuses one prepared owner for both first-level pairs, and checks its emitted demo-root/root.verifier against the trusted root pin. Verification reads demo-root/root.proof and uses the --expected state and count supplied by the caller. The producer's verifier and attached proof statements are payload data; neither establishes the trusted identity or expected root. The example's small FRI settings are for demonstration and testing. Production parameters require separately provisioned trusted verifier artifacts.

Custom non-primitive chips

Custom non-primitive operations must be enabled on the CircuitBuilder before use. They need matching trace generation, preprocessing, AIR builders, and table provers. The PcsRecursionBackend interface supplies the preprocessor, AIR-builder, and table-prover registration hooks. Prepared owners reuse that backend through the prepared contract.

Integration checklist

1. Choose a directly integrated built-in suite and matching backend, or implement the recursive PCS contract for a custom config.
2. Supply an AIR with a RecursiveAir implementation and fixed public-input width when using a trusted owner.
3. Choose a backend with the matching field, permutation, and extension degree.
4. Use a prepared owner for reuse; choose a trusted prepared owner when relation and statement authority must be fixed.
5. Verify output against an independently retained CircuitVerifier and caller-expected statement.

Low-Level API

Use the low-level API when you need to add constraints to a verifier circuit or control its construction and execution. The unified API handles the usual recursion flow; prepared owners retain the circuit and prover setup for repeated proving.

Build a verifier circuit

The expert entry points are verify_p3_uni_proof_circuit and verify_batch_circuit. Their target, config, and lookup parameters depend on the native PCS. The FriRecursionBackend implementation is the checked reference for allocating targets, enabling the permutation tables, and building a FRI verifier circuit. Keep the circuit's permutation and FRI parameters aligned with the native proof's suite.

Supply opening witnesses

A FRI proof carries pruned multiproofs; the MMCS circuit needs a path for each query. Replay the opening transcript and call restore_fri_query_paths before set_fri_mmcs_private_data. The built-in config implementation shows the current set_fri_private_data(config, runner, op_ids, opening_proof, transcript) contract and the required opened-value observation. A hiding PCS also needs its random openings merged into the transcript at the same point as native verification.

Prove and verify the circuit

BatchStarkProver::prepare_circuit finalizes the relation and preprocessing once, then returns a PreparedCircuitProver. Feed runner traces to prepared.prove(&traces) and verify with the independently retained prepared.verifier() and a caller-supplied expected statement. The executable BabyBear example uses this path, including a public statement export.

For ordinary repeated recursion, PreparedLayer and PreparedAggregation also check the native input's shape before reuse. TrustedPreparedLayer and TrustedPreparedAggregation retain child authority and check statements as described in the API guide.

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.

By fixing the program to execute, in particular here proving the correct verification of some known AIR(s) program(s), prover and verifier can agree on the integral execution flow of the program. As such, each step corresponds to an instruction known at compile-time with operands either known at compile-time in the case of constants, or defined by the prover at runtime. This removes all the overhead of handling arbitrary control flow, and makes the resulting AIR(s) statement(s) effectively tailored for the program they represent, as opposed to regular VMs.

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 itself proved, but will be used as source of truth between prover and verifier to guide trace population. The actual soundness comes from the constraints inside the operation-specific STARK chips along with an aggregated lookup argument ensuring consistency of the common values they operate on. The lookups can be seen as representing READ/WRITE interactions on a shared witness memory bus, without requiring a dedicated witness table.

The example below represents the (fixed) IR associated to the statement 37.x - 111 = 0, where x is a public input. It can be reproduced by running

RUST_LOG=debug cargo test --package p3-circuit --lib -- tables::runner::tests::test_toy_example_37_times_x_minus_111 --exact --show-output

A given row of the represented IR contains an operation and its associated operands.

=== CIRCUIT PRIMITIVE OPERATIONS ===
0: Const { out: WitnessId(0), val: 0 }
1: Const { out: WitnessId(1), val: 37 }
2: Const { out: WitnessId(2), val: 111 }
3: Public { out: WitnessId(3), public_pos: 0 }
4: Alu { a: WitnessId(1), b: WitnessId(3), out: WitnessId(4), mul_selector: 1 }
5: Alu { a: WitnessId(2), b: WitnessId(0), out: WitnessId(4), add_selector: 1 }

i.e. operation 4 performs w[4] <- w[1] * w[3], and operation 5 encodes the subtraction check as an addition w[2] + w[0] = w[4] (verifying 37 * x - 111 = 0).

In order to generate the IR, the first step is to create all operations symbolically.

In the symbolic executor, the computation is represented as a graph where nodes are called either ExprId (since they represent the index of an expression) or Target in the code. Each Target can be:

• a constant,
• a public input,
• the output of an operation.

The computation graph that represents all operations in the IR is called Circuit.

A circuit_builder provides convenient helper functions and macros for representing and defining operations within this graph. See section Building Circuits for more details on how to build a circuit.

Witness memory

Conceptually, we still think in terms of a central memory bus that stores values shared across all operations. This bus is indexed by WitnessId and can be represented as pairs (index, value), where indices are accessed by the different chips via lookups to enforce consistency.

• The index information is preprocessed, or read-after-preprocess (RAP): it is known to both prover and verifier in advance, requiring no online commitment.¹
• Values are represented as extension field elements directly (where base field elements are padded with 0 on higher coordinates) for addressing efficiency.

From the fixed IR of the example above, we can deduce an associated witness memory view as follows:

=== WITNESS MEMORY ===
Row 0: WitnessId(w0) = 0
Row 1: WitnessId(w1) = 37
Row 2: WitnessId(w2) = 111
Row 3: WitnessId(w3) = 3
Row 4: WitnessId(w4) = 111

This dedicated table does not actually exist: the same witness indices are instead enforced via cross-table lookups directly between operation-specific chips.

Operation-specific STARK Chips

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

A chip contains:

• Local columns for its variables.
• Lookup ports that describe which witness indices they read from and write to.
• An AIR that enforces its semantics.

We distinguish two kind of chips: those representing native, i.e. primitive operations, and additional non-primitive ones, defined at runtime, that serve as precompiles to optimize certain operations. The recursion machine contains 3 primitive chips: CONST, PUBLIC_INPUT, and a unified ALU chip with three selector columns (add/mul, bool-check, mul-add). SUB and DIV are encoded as ALU rows using the add or mul operation.

Given only the primitive operations, one should be able to carry out most operations necessary in circuit verification. Primitive operations have the following properties:

• They operate on witness slots identified by WitnessId indices in the shared memory bus.
• The representation can be heavily optimized. For example, every time a constant is added to the IR, we either create a new WitnessId or return an already existing one. We could also carry out common subexpression elimination.
• They are executed in topological order during the circuit evaluation, and they form a directed acyclic graph of dependencies.

But relying only on primitive operations for the entire verification would lead to the introduction of many temporary values in the IR. In turn, this would lead to enlarged Witness and primitive tables. To reduce the overall surface area of our AIRs, we can introduce non-primitive specialized chips that carry out specific (non-primitive) operations. We can offload repeated computations to these non-primitive chips to optimize the overall proving flow.

These non-primitive operations use not only Witness table elements (including public inputs), but may also require the use of private data. For example, when verifying a Merkle path, hash outputs are not stored in the Witness table.

This library aims at providing a certain number of non-primary chips so that projects can natively inherit from full recursive verifiers, which implies chips for FRI, MMCS path verification, etc. Specific applications can also build their own non-primitive chips and plug them at runtime.

Non-primitive operations (NPOs) in practice

In the codebase, non-primitive chips are exposed as non-primitive operations (NPOs) that can be plugged into a circuit and executed at runtime. Conceptually, each NPO has three responsibilities:

• A circuit-level plugin that describes how a high-level call to the operation is lowered into a concrete row in the execution IR.
• A runtime executor that knows how to read input witnesses, compute outputs (and any associated private data), and write the results back.
• Optionally, a dedicated table and AIR when we want to prove the internal structure of the operation instead of treating it as an opaque black box.

On the circuit side, an NPO implements a small plugin interface that:

• advertises a unique operation type identifier (for example, a toy cube operation uses a type id of the form cube_simple/x_cubed),
• maps circuit expressions to WitnessIds and creates a non-primitive operation row in the IR,
• exposes a configuration object used when building AIRs and preprocessed columns,
• optionally provides a trace generator for its own dedicated table.

At execution time, the recursion machine walks the IR and, for each non-primitive row, calls the operation’s executor. The executor:

• receives the input and output WitnessIds for that row,
• reads the input values from the Witness table,
• performs the desired computation (possibly using additional private data),
• writes the outputs back into the Witness table, and, if needed, updates preprocessed columns used by its table AIR.

A simple end-to-end example of this pattern is the “cube” NPO used in the integration tests. It defines an operation y = x^3 with one input and one output. Its circuit plugin registers a new NPO type id, lowers calls to y = x^3 into non-primitive IR rows, and attaches a cube executor to those rows. The executor then reads x from the shared witness memory, computes x^3, and writes y back. In that example, the trace generator returns no dedicated table, so only the existing primitive chips appear in the STARK; more sophisticated NPOs (e.g. permutation or Merkle-path verifiers) can in addition expose their own tables and AIRs that are proven alongside the primitive chips.

Going back to the previous example, prover and verifier can agree on the following logic for each chip:

=== CONST TRACE ===
Row 0: WitnessId(w0) = 0
Row 1: WitnessId(w1) = 37
Row 2: WitnessId(w2) = 111

=== PUBLIC TRACE ===
Row 0: WitnessId(w3) = 3

=== ALU TRACE ===
Row 0: mul: WitnessId(w1) * WitnessId(w3) -> WitnessId(w4) | 37 * 3 -> 111
Row 1: add: WitnessId(w2) + WitnessId(w0) -> WitnessId(w4) | 111 + 0 -> 111

Note that because we started from a known, fixed program that has been lowered to a deterministic IR, we can have the CONST chip's table entirely preprocessed (i.e. known to the verifier), as well as all index columns of the other primitive chips.

Lookups

All chip interactions are performed via a lookup argument. Enforcing multiset equality between all chip ports and the shared witness memory view ensures correctness without proving the execution order of the entire IR itself. Lookups can be seen as READ/WRITE or RECEIVE/SEND interactions between tables which allow global consistency over local AIRs.

Cross-table lookups (CTLs) ensure that every chip interaction is mediated by shared witness indices: producers expose a (index, value) pair and consumers read the same pair back. In the current design this is encoded directly as CTL relations between operation tables, rather than through a separate Witness table. No chip talks directly to any other chip; the aggregated LogUp argument enforces multiset equality between the writes and reads.

For the toy example the CTL relations are:²

(index 0, value 0)   : CONST → Witness → ALU(add row)
(index 1, value 37)  : CONST → Witness → ALU(mul row)
(index 2, value 111) : CONST → Witness → ALU(add row)
(index 3, value 3)   : PUBLIC → Witness → ALU(mul row)
(index 4, value 111) : ALU(mul row) → Witness ← ALU(add row)

For the full protocol specification — including the LogUp accumulation formula, per-chip multiplicity encoding, the global_lookup_data proof field, challenge derivation, and how the recursive verifier checks the argument — see Lookups & CTL Spec.

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. ↩

2. The two ALU rows both write w4 = 111 to the shared witness memory (once via a mul row, once via an add row). Because this memory is modeled as a read-only / write-once bus, the aggregated lookup forces those duplicate writes to agree, which is exactly the constraint 37 * 3 = 111 = 0 + 111. ↩

Building Circuits

This section explains how the CircuitBuilder allows to build a concrete Circuit for a given program. We’ll use a simple Fibonacci example throughout this page to ground the ideas behind circuit building:

let mut builder = CircuitBuilder::<F>::new();

// Public input: expected F(n)
let expected_result = builder.public_input();

// Compute F(n) iteratively
let mut a = builder.define_const(F::ZERO); // F(0)
let mut b = builder.define_const(F::ONE);  // F(1)

for _i in 2..=n {
    let next = builder.add(a, b); // F(N) <- F(N-1) + F(N-2)
    a = b;
    b = next;
}

// Assert computed F(n) equals expected result
builder.connect(b, expected_result);

let circuit = builder.build()?;
let mut runner = circuit.runner();

Building Pipeline

In what follows, we call WitnessId what serves as identifier for values in the global Witness storage bus, and ExprId position identifiers in the ExpressionGraph (with the hardcoded constant ZERO always stored at position 0).

Building a circuit works in 4 successive steps:

Stage 1 — Lower to primitives

This stage will go through the ExpressionGraph in successive passes and emit primitive operations.

• when going through emitted Const nodes, the builder ensures no identical constants appear in distinct nodes of the circuit, seen as a DAG (Directed Acyclic Graph), by performing witness aliasing, i.e. looking at node equivalence classes. This allows to prune duplicated Const nodes by replacing further references with the single equivalence class representative that will be part of the DAG. This allows to enforce equality constraints are structurally, without requiring extra gates.

• public inputs and arithmetic operations may also reuse pre-allocated slots if connected to some existing node.

Stage 2 — Lower non-primitives

This stage translates the ExprId of logged non-primitive operations inputs (from the set of non-primitive operations allowed at runtime) to WitnessIds similarly to Stage 1.

Stage 3 — Optimize primitives

This stage aims at optimizing the generated circuit by removing or optimizing redundant operations within the graph. For instance, if the output of a primitive operation is never used elsewhere in the circuit, its associated node can be pruned away from the graph, and the operation removed.

Once all the nodes have been assigned, and the circuit has been fully optimized, we output it.

Building recursive AIR constraints

In order to recursively verify an AIR, its constraints need to be added to the circuit and folded together. In Plonky3, we can get an AIR's constraints in symbolic form. Since our primitive chips (see section Execution IR) encompass the various entries in the symbolic representation, we can simply map each symbolic operation to its circuit counterpart. The symbolic_to_circuit function does exactly that for a given symbolic constraint.

We can consider a small example to show how operations are mapped. Given public inputs a and b, and a constant c, we have the following symbolic constraint: Mul{ a, Sub {b, Const{ c }}} (which corresponds to: a * (b - c)).

// We get the `ExprId` corresponding to Const{ c } by adding a constant to the circuit.
let x = builder.define_const(c);
// We use the previously computed `x` to compute the subtraction in the circuit.
let y = builder.sub(b, x);
// We use the previously computed `y` to compute the multiplication in the circuit.
let z = builder.mul(a, y);

z is then the output ExprId of the constraint in the circuit.

Using this function, we have implemented, for all AIRs, the automatic translation from their set of symbolic constraints to the circuit version of the folded constraints:

// Transforms an AIR's symbolic constraints into its counterpart circuit version,
// and folds all the constraints in the circuit using the challenge `alpha`.
fn eval_folded_circuit(
        // The AIR at hand.
        &self,
        builder: &mut CircuitBuilder<EF>,
        // Circuit version of Lagrange selectors.
        sels: &RecursiveLagrangeSelectors,
        // Folding challenge.
        alpha: &Target,
        // Lookup contexts and data (empty for uni-STARK verification).
        lookup_metadata: &LookupMetadata<'_, F>,
        // All kinds of columns that could be involved in constraints.
        columns: ColumnsTargets<'_>,
        // Gadget for encoding lookup interactions in the circuit.
        lookup_gadget: &LG,
    ) -> Target {
        // Get all the constraints in symbolic form.
        let symbolic_constraints =
            get_symbolic_constraints(self, 0, columns.public_values.len());

        // Fold all the constraints using the folding challenge.
        let mut acc = builder.define_const(EF::ZERO);
        for s_c in symbolic_constraints {
            let mul_prev = builder.mul(acc, *alpha);

            // Get the current constraint in circuit form.
            let constraint =
                symbolic_to_circuit(sels.row_selectors, &columns, &s_c, builder);

            // Fold the current constraint with the previous value.
            acc = builder.add(mul_prev, constraint);
        }

        acc
    }

This facilitates the integration of any AIR verification into our circuit.

Proving

Calling circuit.runner() will return a instance of CircuitRunner allowing to execute the represented program and generate associated execution traces needed for proving:

let mut runner = circuit.runner();

// Set public input
let expected_fib = compute_fibonacci_classical(n);
runner.set_public_inputs(&[expected_fib])?;

// Instantiate prover instance
let config = build_standard_config_koalabear();
let prover = BatchStarkProver::new(config);

// Generate traces
let traces = runner.run()?;

// Prove the program (circuit_prover_data holds the preprocessed columns)
let proof = prover.prove_all_tables(&traces, &circuit_prover_data)?;

Key takeaways

• “Free” equality constraints: by leveraging witness aliasing, we obtain essentially free equality constraints for the prover, removing the need for additional arithmetic constraints.

• Deterministic layout: The ordered primitive lowering combined with equivalence class allocation yields predictable WitnessIds.

• Minimal primitive set: With Sub/Div being effectively translated as equivalent Add/Mul operations, the IR stays extremely lean, consisting only of Const, Public, Add and Mul, simplifying the design and implementation details.

Lookups and Cross-Table Lookup (CTL) Spec

This page specifies how multiset equality is enforced across all operation-specific chips via a shared witness bus, how each chip participates in the lookup argument, and how the recursive verifier checks the resulting proof data.

The WitnessChecks bus

All chips in the recursion machine communicate through a single virtual bus named WitnessChecks. There is no physical table for this bus — it exists only as the aggregate of each chip's lookup contributions. The bus carries tuples of the form (index, value), where:

• index is a WitnessId scaled by the extension degree D (i.e. WitnessId * D),
• value is a D-element extension field value (the basis coefficients of the witness slot).

A chip sends a tuple to the bus when it creates a witness value, and receives a tuple from the bus when it consumes one. The lookup argument enforces that every sent tuple is received the correct number of times, without requiring a shared table to be committed to.

The LogUp argument

The system uses the LogUp accumulation scheme. For a random challenge α drawn after all trace commitments are observed, define the compressed row for a tuple (idx, v[0], ..., v[D-1]) as:

compressed = α^0 * idx + α^1 * v[0] + ... + α^D * v[D-1]

Each chip row contributes a rational term mult / (β - compressed) to a running accumulator, where β is a second random challenge and mult is the signed multiplicity for that row:

• Positive multiplicity means the row is a sender (it writes a value onto the bus).
• Negative multiplicity means the row is a receiver (it reads a value from the bus).

The lookup argument is satisfied when the sum of all contributions across all chips and all rows equals zero:

Σ_{chip} Σ_{row} mult_row / (β - compressed_row) = 0

This is equivalent to asserting multiset equality between the multiset of all sent (index, value) tuples and the multiset of all received (index, value) tuples.

In practice, the prover computes a permutation polynomial (the running cumulative sum) for each lookup, commits to it, and the verifier checks the boundary condition at the last row. The permutation columns are opened during the FRI query phase alongside the main trace.

Multiplicities and preprocessed columns

Because the circuit's IR is fixed at compile time, the WitnessId index for every operation is known before proving begins. This means all index and multiplicity columns are preprocessed — they require no online commitment and can be reconstructed by the verifier.

Each chip encodes its multiplicities differently:

ConstAir

ConstAir has 2 + D preprocessed columns per row: [multiplicity, index, value[0..D)]. Both the index and the value are fully preprocessed (the entire constant table is known before proving, and an AIR constraint binds the main-trace value to its preprocessed copy, so a trace cannot claim a different value than the circuit's constant). Each row sends (index, value) with the preprocessed multiplicity, which equals the number of times that constant slot is read by other chips. Because the value lives in the preprocessed columns, changing a constant's value changes the circuit's preprocessed commitment.

PublicAir

PublicAir has two preprocessed columns per lane: [multiplicity, index]. For active rows the multiplicity is +1; for padding rows it is 0. Each lane sends (index, value) once.

AluAir

AluAir has 13 preprocessed columns per lane (see PREP_* constants). The lookup-relevant ones are:

Each ALU row contributes four tuples to the WitnessChecks bus:

• a: received with effective multiplicity mult_a * a_is_reader
• b: received with multiplicity mult_b
• c: received with effective multiplicity mult_a * c_is_reader
• out: sent with multiplicity mult_out

The add operation does not use c (it is aliased to the zero witness slot), while mul_add and horner_acc use all four operands. Double-step HornerAcc rows additionally contribute two extra lookups (a1, c1) via five global extra preprocessed columns.

Non-primitive operations (NPOs)

Non-primitive chips such as Poseidon2 and MMCS can expose their own input/output ports on the WitnessChecks bus via CTL. The out_ctl flag on a Poseidon2PermCall controls which output limbs are made visible on the bus, allowing subsequent operations to read the hash outputs without committing them to the main witness table.

The global_lookup_data proof field

The BatchProof carries a field global_lookup_data: Vec<Vec<LookupData<F>>>, with one inner Vec per table instance. Each LookupData entry contains:

#![allow(unused)]
fn main() {
pub struct LookupData<F> {
    /// Unique name identifying the lookup (e.g. "WitnessChecks").
    pub name: String,
    /// Index of the auxiliary permutation column for this lookup.
    pub aux_idx: usize,
    /// The expected final value of the running accumulator (committed to as a public input).
    pub expected_cumulated: F,
}
}

The expected_cumulated value is the boundary check: after the prover runs the LogUp accumulation to the last row, the result must match this value. The verifier checks this in circuit. Because it is committed as a public input of the recursive circuit, tampering with it is caught immediately during circuit execution — a WitnessConflict error is raised (see test_wrong_expected_cumulated).

The name field determines how the random permutation challenges (α, β) are derived from the Fiat-Shamir transcript. Changing the name of a lookup while keeping the same proof is detected as an inconsistency between the challenge generation and the opened permutation values (see test_inconsistent_lookup_name).

Challenge generation

Lookup challenges are derived from the Fiat-Shamir transcript after the main trace commitment is absorbed. The generation follows this sequence:

1. Observe the main trace commitment.
2. For each named lookup, squeeze two extension field challenges (α, β) from the transcript using the lookup's name as domain-separation context.
3. The prover builds the permutation columns using these challenges and commits to them.
4. Observe the permutation commitment.
5. The expected_cumulated value is included as a public input to the recursive circuit, binding the proof to the correct permutation boundary.

The ordering of LookupData entries within each instance must be sorted by aux_idx (see test_inconsistent_lookup_order_shape). Mismatches in count or order cause InvalidProofShape errors before the recursive circuit is even built.

Recursive verification of lookups

During recursive verification, the circuit:

1. Allocates a public input target for each expected_cumulated value from global_lookup_data.
2. Evaluates the LogUp constraint at the opened permutation values (perm_local, perm_next) using the lookup challenges derived in-circuit via the circuit challenger.
3. Checks that the final running sum matches the committed expected_cumulated value via connect.

Because the permutation columns are opened through the same FRI batch as the main trace, their evaluations are private inputs to the recursive circuit. The expected_cumulated values, being public inputs, are visible to the outer proof.

CTL example: the toy circuit revisited

For the 37 * x - 111 = 0 example from the Construction section, the full set of WitnessChecks contributions is:

The c operand of the ALU add row reads w4 = 111 rather than producing it, closing the constraint 37 * x = 111 + 0. The net sum across all entries is zero iff multiset equality holds.

Hashing and Fiat-Shamir in Recursion

This section uses a width-16/rate-8, degree-4 Poseidon2 configuration to explain hashing in recursive verification and transcript compatibility with native Plonky3. Supported custom configurations also select Poseidon1 or a different geometry; see Configuration.

Overview

Recursive verification requires two distinct uses of the permutation used by the selected prover configuration:

1. Fiat-Shamir Challenger: Derives random challenges from the transcript (commitments, opened values, etc.)
2. MMCS/Merkle Verification: Verifies Merkle tree opening proofs for commitments

In the Poseidon2 example below, both operations use the same underlying permutation, but they interact with it differently:

┌─────────────────────────────────────────────────────────────────────┐
│                    Poseidon2 Permutation (WIDTH=16)                 │
├──────────────────────────────┬──────────────────────────────────────┤
│     Fiat-Shamir Challenger   │        MMCS/Merkle Hashing           │
├──────────────────────────────┼──────────────────────────────────────┤
│ • Duplex sponge construction │ • Compression function               │
│ • Absorb/squeeze pattern     │ • Hash two siblings → parent         │
│ • ~20 calls per verification │ • Hundreds of calls per verification │
│ • Transcript-sensitive       │ • Position-sensitive                 │
└──────────────────────────────┴──────────────────────────────────────┘

The Poseidon2 Permutation

The concrete Poseidon2 example uses:

• WIDTH = 16: The permutation operates on 16 field elements
• RATE = 8: In sponge mode, 8 elements are absorbed/squeezed per permutation

These width-16/rate-8 values describe this example. The selected supported permutation family, geometry, and backend degree depend on the configuration.

Base Field vs Extension Field Views

The same Poseidon2 permutation can be viewed in two equivalent ways:

D=1 View (Base Field)

Input:  [e₀, e₁, e₂, ..., e₁₅]     ← 16 base field elements
Output: [f₀, f₁, f₂, ..., f₁₅]     ← 16 base field elements

D=4 View (Extension Field)

Input:  [E₀, E₁, E₂, E₃]           ← 4 extension field elements
Output: [F₀, F₁, F₂, F₃]           ← 4 extension field elements

where each Eᵢ = eᵢ₀ + eᵢ₁·ω + eᵢ₂·ω² + eᵢ₃·ω³

Both views represent the same Poseidon2 permutation over the base field. The difference is purely representational:

• D=1: Direct representation as 16 base field elements
• D=4: Packed representation as 4 degree-4 extension field elements

The Fiat-Shamir Challenger

Native Plonky3 Behavior

Plonky3's native DuplexChallenger maintains internal state as base field elements:

#![allow(unused)]
fn main() {
struct DuplexChallenger<F, Permutation, const WIDTH: usize, const RATE: usize> {
    sponge_state: [F; WIDTH],        // 16 base field elements
    input_buffer: Vec<F>,            // Pending observations (0..RATE)
    output_buffer: Vec<F>,           // Available samples (0..RATE)
}
}

The challenger implements a duplex sponge construction as follows:

┌────────────────────────────────────────────────────────────────┐
│                     Duplex Sponge Operation                    │
├────────────────────────────────────────────────────────────────┤
│                                                                │
│   observe(value):                                              │
│     1. Clear output_buffer (any pending outputs are invalid)   │
│     2. Push value to input_buffer                              │
│     3. If input_buffer.len() == RATE, apply duplexing:         │
│        • Overwrite state[0..RATE] with input_buffer            │
│        • Apply Poseidon2 permutation                           │
│        • Fill output_buffer from state[0..RATE]                │
│        • Clear input_buffer                                    │
│                                                                │
│   sample():                                                    │
│     1. If input_buffer not empty OR output_buffer empty:       │
│        • Trigger duplexing (same as step 3 above)              │
│     2. Pop and return from output_buffer                       │
│                                                                │
└────────────────────────────────────────────────────────────────┘

Circuit Challenger Design

The recursive circuit operates over extension field elements, but must produce identical transcripts to the native challenger. This requires careful state management.

Conceptually, the Poseidon2 circuit challenger in this example maintains coefficient-level targets. This sketch is not its literal Rust definition:

#![allow(unused)]
fn main() {
struct CircuitChallenger<const WIDTH: usize, const RATE: usize> {
    state: Vec<Target>,           // Targets, (base field coefficients)
    input_buffer: Vec<Target>,    // Pending observations
    output_buffer: Vec<Target>,   // Available samples
    poseidon2_config: Poseidon2Config,
}
}

Each target in state represents a base field element embedded in the extension field (i.e., only the constant coefficient is non-zero).

Duplexing in the Circuit

When the circuit challenger needs to permute, it must bridge between coefficient-level state and the Poseidon2 permutation:

    16 coefficient targets                4 extension targets
    [c₀, c₁, c₂, ..., c₁₅]    ────►     [E₀, E₁, E₂, E₃]
                               recompose
                                  │
                                  ▼
                          ┌─────────────┐
                          │  Poseidon2  │
                          │ Permutation │
                          └─────────────┘
                                  │
                                  ▼
    [c'₀, c'₁, c'₂, ..., c'₁₅]  ◄────   [F₀, F₁, F₂, F₃]
                               decompose

Recomposition (16 coefficients → 4 extension elements):

E₀ = c₀ + c₁·ω + c₂·ω² + c₃·ω³
E₁ = c₄ + c₅·ω + c₆·ω² + c₇·ω³
E₂ = c₈ + c₉·ω + c₁₀·ω² + c₁₁·ω³
E₃ = c₁₂ + c₁₃·ω + c₁₄·ω² + c₁₅·ω³

Decomposition (4 extension elements → 16 coefficients): The inverse operation, extracting basis coefficients from each extension element.

Row Overhead

For this width-16/rate-8, degree-4 example, recomposition/decomposition adds overhead in the primitive tables:

This example adds a total of approximately 70 rows over the different primitive tables per challenger duplexing.

Optimization Note: When using D=1 configuration (base field challenges), no recomposition/decomposition is needed as the state maps directly to the Poseidon2 inputs, eliminating this overhead.

Coexistence on a Single Trace

Both D=1 and D=4 views share the same Poseidon2 AIR trace. The AIR constrains the Poseidon2 permutation over the base field regardless of how inputs/outputs are packed:

┌───────────────────────────────────────────────────────────────────────────────────┐
│                          Poseidon2 AIR Trace (WIDTH=16)                           │
├───────────────────────────────────────────────────────────────────────────────────┤
│                                                                                   │
│  Each row: [s₀, s₁, s₂, s₃, s₄, s₅, s₆, s₇, s₈, s₉, s₁₀, s₁₁, s₁₂, s₁₃, s₁₄, s₁₅] │
│                                                                                   │
│  The AIR constraints enforce the Poseidon2 round function:                        │
│     • S-box application                                                           │
│     • Linear layer (MDS matrix multiplication)                                    │
│     • Round constant addition                                                     │
│                                                                                   │
│  These constraints are identical whether the caller interprets the 16 columns as: │
│     • 16 individual base field elements (D=1), or                                 │
│     • 4 extension field elements of degree 4 (D=4)                                │
│                                                                                   │
└───────────────────────────────────────────────────────────────────────────────────┘

Transcript Compatibility

For recursive verification to be sound, the circuit challenger must produce identical challenge values to the native challenger given the same inputs. This requires:

1. Same observation order: Values must be absorbed in the exact same sequence
2. Same duplexing triggers: Permutation must occur at the same points
3. Same output buffer management: Samples must come from the same buffer positions

Extension Field Operations

The native challenger provides methods for extension field values:

These methods ensure that extension field observations/samples are transcript-compatible.

In addition, when observing opened values in batch verification, we must ensure to respect the order the native verifier performed for the recursive circuit to be able to satisfy the associated constraints.

Configuration

For the Poseidon2 examples here, Poseidon2Config specifies the field and permutation extension degree:

For supported custom WHIR configurations using Poseidon1 or Poseidon2, backend input validation also checks the actual base field and challenge dimension. See Configuration for the supported combinations and matching requirements.

Scaling Strategies

The fixed recursive verifier supports only predetermined programs. This section describes strategies for handling computations of varying size or complexity.

Tree-style recursion for variable-length inputs

Split a large computation into chunks and prove each chunk independently using a fixed inner circuit. Then aggregate the proofs in a binary tree, where each leaf corresponds to a portion of the computation. The tree root yields a single proof attesting to the entire computation.

This approach is naturally parallelizable: all leaf proofs are independent, and each tree level can be processed in parallel across pairs.

A formal description of tree-style recursion for STARKs can be found in zkTree. See also the Aggregation chapter for the API.

Flexible FRI verification

To support proofs with different FRI shapes (different trace sizes), two techniques apply:

Proof lifting

Lift smaller proofs to a larger domain, as described in Lifting Plonky3. Lifting projects a smaller domain into a larger one, reusing the original LDE and commitments. This lets a fixed circuit verify proofs from a range of trace sizes without recomputation.

Multi-shape FRI verification

Instead of fixing a single proof size per verifier circuit, extend the FRI verifier to handle a range of sizes within the same circuit, at minimal overhead. A related approach is implemented in Plonky2 recursion (PR #1635).

Soundness and Security

This section describes the security model, current guarantees, and known limitations.

What is proven

A recursive proof attests that:

1. The original computation (base layer) was executed correctly according to the AIR constraints.
2. Each intermediate STARK verification was performed correctly: commitments were checked, FRI queries were sampled from the transcript, Merkle paths were verified, and polynomial evaluations matched.
3. The Fiat-Shamir transcript was computed consistently — the circuit challenger produces identical challenges to the native Plonky3 challenger given the same observations.

Security parameters

FRI soundness depends on several parameters working together. However, it is not generally correct to model security as “num_queries × log_blowup bits”. That heuristic relied on strong proximity-gap / correlated-agreement assumptions that are no longer believed to hold in full generality. See for instance:

• https://eprint.iacr.org/2025/2010
• https://eprint.iacr.org/2025/2046

Instead, the soundness error must be derived from a proven bound for the specific FRI variant and parameter regime being used.

Let:

ε_FRI = soundness error derived from the relevant FRI theorem/bound
        (depends on blowup, proximity parameter δ, domain size,
         field size, and list-decodability/proximity-gap behavior)

Then the security level should be expressed as:

security ≈ -log2(ε_FRI) + query_pow_bits

Crucially, -log2(ε_FRI) must be computed from a proven soundness bound for the specific FRI configuration. It should not be replaced by num_queries × log_blowup unless an additional (explicitly stated) conjectural assumption is being made.

Cryptographic components verified in-circuit

Merkle tree verification

Every MMCS opening proof (Merkle path) is verified in-circuit with the permutation selected by the configuration (Poseidon1 or Poseidon2). The circuit:

• Hashes sibling pairs up the tree
• Checks that the reconstructed root matches the committed root (a public input)
• Handles position-dependent ordering (left vs right sibling)

FRI verification

The circuit performs the full FRI verification protocol:

• Samples folding challenges (beta) from the transcript
• Samples query indices from the transcript
• Verifies proof-of-work witnesses
• Checks the fold chain: at each FRI round, verifies that the folded polynomial evaluations are consistent with the committed Merkle trees
• Evaluates and checks the final polynomial

Fiat-Shamir challenger

The circuit challenger implements a duplex sponge construction identical to Plonky3's native DuplexChallenger. It absorbs commitments and opened values in the same order as the native verifier, producing identical challenges. See Hashing and Fiat-Shamir for details on transcript compatibility.

ZK mode

The recursive verifier supports ZK-enabled STARK configurations, including batch recursion transcript/randomization handling.

Challenger permutation: CTL-verified

The Fiat-Shamir challenger's permutations are connected to the matching Poseidon1 or Poseidon2 AIR table via cross-table lookups (CTLs). The circuit builder exposes the permutation input and rate output; the executor runs the selected permutation, and the lookup argument enforces that the input/output pair appears in its table. MMCS permutation calls for Merkle verification are also CTL-verified.

Current limitations

Supported permutation configurations

Custom recursion configurations support selected Poseidon1 or Poseidon2 permutations and matching backend geometry and challenge dimension, including BabyBear D4 with width 16/rate 8 and Goldilocks D2 with width 8/rate 4. See Configuration for supported combinations and the input PCS matching requirements.

Verifier trust model

Debugging

The CircuitBuilder provides debugging tools to identify wiring and runner execution errors.

Compile features

The workspace exposes several opt-in compile features that activate extra instrumentation. They are disabled by default to keep production binaries lean.

Enable a feature by passing --features <feature> (or --features parallel for the prover sub-crate) to Cargo:

# Enable allocation logging and circuit diagnostics
cargo test -p p3-circuit --features debugging

# Enable profiling (includes debugging)
cargo test -p p3-circuit --features profiling

# Enable parallel trace generation
cargo run --example recursive_fibonacci --features parallel

Build profiles

Two custom workspace profiles complement the features above:

# Profile-guided performance measurement (symbols + optimisation)
cargo run --profile profiling --example recursive_fibonacci --features parallel

# Maximum-performance binary (examples, benchmarks)
cargo run --profile optimized --example recursive_fibonacci --features parallel

Allocation Logging

The CircuitBuilder supports an allocation logger during circuit building that logs allocations being performed. These logs can then be analyzed at runtime and leveraged to detect issues in circuit constructions.

Requirement: allocation logging requires the debugging compile feature to be enabled on p3-circuit.

Enabling Debug Logging

Allocation logging is active whenever the debugging feature is compiled in. builder.dump_allocation_log() emits tracing events. Install a tracing subscriber that accepts DEBUG events to see them; the chosen subscriber controls where they are written.

Allocation Log Format

By default, the CircuitBuilder automatically logs all allocations with no specific labels. You can attach descriptive labels to make failures easier to locate:

let mut builder = CircuitBuilder::<F>::new();

// Allocating with custom labels
let input_a = builder.alloc_public_input("input_a");
let input_b = builder.alloc_public_input("input_b");
let input_c = builder.alloc_public_input("input_c");

let b_times_c = builder.alloc_mul(input_b, input_c, "b_times_c");
let a_plus_bc = builder.alloc_add(input_a, b_times_c, "a_plus_bc");
let a_minus_bc = builder.alloc_sub(input_a, b_times_c, "a_minus_bc");

// Default allocation
let x = builder.public_input(); // unlabelled
let y = builder.add(x, z);          // unlabelled

The CircuitBuilder also allows nested scopes. Each allocation records the innermost active scope name, not a full path through all parent scopes:

fn complex_function(builder: &mut CircuitBuilder) {
    builder.push_scope("complex function");

    // Do something
    inner_function(builder); // <- this will create a nested scope within the inner function

    builder.pop_scope();
}

fn inner_function(builder: &mut CircuitBuilder) {
    builder.push_scope("inner function");

    // Do something else

    builder.pop_scope();
}

An allocation records its source ExprId, type, label, scope, and direct dependency groups in operand order. Private inputs have AllocationType::PrivateInput; code that exhaustively matches the debugging-only AllocationType enum must handle this variant. The zero expression is preallocated without an allocation record. Constant pooling, arithmetic simplification, and expression-level common-subexpression reuse may return an existing ExprId; in that case its first allocation's label and scope remain the recorded ones.

Diagnosing runner errors

debugging also retains immutable source information on a circuit built by CircuitBuilder. Call run_with_diagnostics() to receive an owned CircuitDiagnostic when the runner returns an error. It works without a tracing subscriber and can outlive the runner and circuit:

use p3_baby_bear::BabyBear;
use p3_circuit::{CircuitBuilder, CircuitError};

let mut builder = CircuitBuilder::<BabyBear>::new();
builder.push_scope("inputs");
let _amount = builder.alloc_public_input("amount");
builder.pop_scope();
let circuit = builder.build().unwrap();

let diagnostic = circuit.runner().run_with_diagnostics().unwrap_err();
assert!(matches!(diagnostic.error(), CircuitError::PublicInputNotSet { .. }));
println!("{diagnostic}"); // Includes the input's label and scope.
for source in diagnostic.operation_origins() {
    if let Some(allocation) = &source.allocation {
        println!("source {}: {}", source.expr_id, allocation.label);
    }
}
let original_error: CircuitError = diagnostic.into_error();

The underlying CircuitError stays available through error(), into_error(), and the standard error source() method. Existing run() and input setters still return CircuitError directly. For an error from a setter, use circuit.diagnose_error(error); this reports the caller phase and only context that can be established from the error. It cannot infer which operation would later execute. For example:

let mut runner = circuit.runner();
let error = runner.set_public_inputs(&[]).unwrap_err();
let diagnostic = circuit.diagnose_error(error);
println!("{diagnostic}");

The reported compiled operation index is a zero-based position in Circuit::ops. It is different from both the original builder ExprId and a NonPrimitiveOpId. An operation's source list may contain more than one expression: exact duplicate operations merge during optimization, and an actual multiply-add fusion retains the source multiply and add. Subtraction and division can lower to backward arithmetic operations; a division error may therefore identify a compiled multiply while showing the original labeled Div expression and its numerator/denominator dependencies. A non-primitive or hint call can be the source even when it has no output witness.

Witness aliases are related but distinct from the source of the failing operation. Several expressions connected to one canonical witness can be listed as aliases. The diagnostic keeps the failing operation's origins in operation_origins() separate from an implicated witness's witness_aliases(). Each DiagnosticSource has an expr_id, an optional allocation, and dependencies grouped in the original operand order. These dependencies are one level deep; the report does not walk the whole expression graph. phase() and compiled_operation() provide the failure stage and actual compiled operation when known. Circuit::provenance() exposes the builder-produced snapshot through allocation(expr_id), operation_origins(compiled_op_index), and witness_origins(canonical_witness_id). Missing individual records remain missing; the API does not invent labels or scopes.

CircuitDiagnostic formats at most eight items per repeated section, marking skipped items with … (+N more). Its whole Display, including the original error text, is capped at 4,096 Unicode characters followed by … (+N characters omitted) if truncated. Its structured accessors and error() retain the complete recorded data. A circuit created directly with Circuit::new has no builder provenance; its diagnostic can still report the typed error and available compiled operation context. Provenance describes the compiled snapshot: changing the public Circuit::ops or expression-to-witness mapping after build can invalidate source-to-operation correspondence. A same-length mutation cannot be detected automatically. Debug metadata is kept outside compiled operations, preprocessed data, trace values, and proof/artifact identity. Diagnostics do not collect source file locations or stack traces.

Debugging constraints

Diagnostics enrich errors actually returned by the circuit runner; they do not add new runtime constraint checks. In particular, the runner's BoolCheck execution does not universally reject a non-boolean witness value. A successful trace run does not establish that every AIR constraint is satisfied. Plonky3's check_constraints feature can help check AIR constraints during proving in debug builds.

Binary Fields and Binary Hashes

Plonky3 0.7 and 0.8 added a native characteristic-2 proving stack alongside the two-adic prime fields this repository is built on:

• p3-binary-field: the tower GF(2) ⊂ GF(4) ⊂ … ⊂ GF(2^128) (Gf2, BinaryField8 … BinaryField128), GF(2^128) in the GHASH polynomial basis (Ghash128), and BinaryChallenger, a Fiat-Shamir transcript over a byte hash.
• p3-binary-dft, p3-binary-pcs, WHIR over binary additive domains, and p3-multi-stark: multilinear commitments and a SuperSpartan-style prover over those fields.
• Characteristic-2 AIRs for the bit-oriented hashes: KeccakBinaryAir (p3-keccak-air) and Blake3BinaryAir (p3-blake3-air).

What this repository supports today

The repository supports complete native binary recursion for Tower128, and for Poly64 with Poly192 challenges, using additive WHIR, product buses and native Keccak or Blake3 hash tables. The Tower128 owner also accepts Tower32 children. It separately verifies binary PCS and additive-WHIR proofs inside prime-field circuits, including indexed lookup variants. recursion/examples/native_binary_recursion.rs and recursion/examples/native_poly_recursion.rs demonstrate binary-in/binary-out proofs. recursion/examples/binary_prover.rs demonstrates the prime-field outer path.

• Circuits over binary fields. The primitive circuit layer (constants, public and private inputs, ALU ops, connections, tags) needs only field arithmetic, and runs unchanged over every tower level and Ghash128 (circuit/tests/binary_fields.rs). Two things behave differently from a prime field:

  • x - y = x + y and 2 = 0. Integer constructors such as F::from_u64 go through GF(2), so they keep only the parity of their argument.
  • Gadgets that read field elements as integers are rejected, not silently wrong. reconstruct_index_from_bits returns CircuitBuilderError::CharacteristicTwoUnsupported for a characteristic-2 base field. The decomposition and recomposition gadgets require BF: PrimeField64 with F: ExtensionField<BF>, and the binary tower only extends its byte-aligned levels, so they cannot be instantiated over it at all.
  • The separate binary_decompose_coordinates / binary_recompose_coordinates APIs use the field's raw basis through BinaryCoordinateField. Every coordinate is constrained Boolean, and requesting fewer than the full width also constrains the omitted coordinates to zero. These APIs preserve each field's own basis; they do not reinterpret a polynomial element as a tower element.

• Bit-oriented BinaryField128 arithmetic. BinaryTower128Target represents the Wiedemann tower type p3_binary_field::BinaryField128 as 128 Boolean coordinates in a prime or binary circuit field. It does not use the GHASH polynomial coordinates of Ghash128. At each level, a = a0 + a1 X_k stores the lower coefficient first and uses X_k² + X_(k-1) X_k + 1 = 0, with X_(-1) = 1. Bit 0 is one; bit j is the product of tower roots selected by the set bits of j. Every 128-bit pattern is a valid tower element. The raw u128 coordinates in native code come from TowerLevel::from_repr / to_repr, or from little-endian bytes, not from_u128 (which embeds through GF(2)).

  • Import/export uses eight little-endian 16-bit limbs: limb[j] = Σ_(i=0..15) bit[16j+i]·2^i. The base field must have order above 65535; both limb methods also reject characteristic two. Limb import constrains the range and base-field embedding, and raw-bit import asserts every input bit is Boolean.
  • binary128_add, binary128_mul, and binary128_square use the existing ALU relations for Boolean XOR/AND and recursive tower reduction. assert_binary128_inverse(value, candidate) constrains their product to tower one; the caller supplies the candidate, and zero has no satisfying inverse. There are no new tables, AIRs, or native-field hints.
  • All ExprIds passed to these methods must come from the same CircuitBuilder expression graph. The target's read-only bits do not carry a builder identity. A circuit using this arithmetic can be proved with the compact circuit prover and carried into the next recursion layer over the supported prime host fields. Bits-only arithmetic also runs over binary fields; integer-limb import/export remains prime-only.

• Native primitive circuit proofs. p3_circuit_prover::direct::DirectCircuitAir freezes a circuit's primitive relation and binds public values in caller order. It accepts native binary carrier fields without integer witness addresses or count-based lookups. recursion/tests/native_binary_circuit.rs proves and verifies circuits over both BinaryField128 and Poly64 (with Poly192 challenges). The AIR repeats the entire assignment on every row, so its width and openings grow with the circuit's witness count. It is a non-hiding correctness baseline, rejects custom non-primitive tables, and does not yet provide an efficient recursive binary prover.

• Native challenge scalars. NativeTower128Target keeps one expression per scalar and uses native addition, multiplication and squaring only on CircuitBuilder<BinaryField128>. Checked conversions materialize Boolean coordinates or raw words at serialization boundaries. It does not treat GHASH or polynomial carriers as the Wiedemann tower. NativePoly192Target separately represents the polynomial challenge as three Poly64 scalars, with reduction by y³ = y + 1.

• Compact native primitive tables. p3_circuit_prover::indexed::IndexedCircuit stores one canonical witness table and proves every gate operand and output with indexed reads. Trusted preprocessing pins the graph's positions, constants and selectors; public values bind in caller order, including aliases. No field-valued integer read counts or creator-role tags are used. Main and preprocessing PCS dimensions are computed from their complete stacked layouts. The native tower and polynomial tests in recursion/tests/native_indexed_circuit.rs exercise real indexed proofs. This path remains non-hiding and rejects custom non-primitive tables.

• Native Keccak circuit tables. p3_circuit_prover::native_binary::NativeBinaryCircuit extends the compact indexed relation with the explicitly enabled native_keccak_f1600 operation. native_keccak256_bytes accepts checked raw eight-coordinate bytes and returns 32 bytes in natural digest order. The default upstream binary Keccak AIR retains its Boolean constraints; fixed preprocessing pins each permutation's schedule, and indexed reads bind all 100 input and output limbs to canonical circuit witnesses. Other custom operations still fail closed. recursion/tests/native_keccak_circuit.rs exercises native proof verification and rejection of changed digest values and bridge payloads. The product-bus backend below also uses these hash tables.

• Native product-bus wiring. p3_circuit_prover::native_bus::NativeBusCircuit binds gates, public inputs and Keccak boundaries through fixed witness occurrences. Adjacent copies of each witness agree; native product buses authenticate their reads without sending a provider-sized pushforward vector. Each circuit requires a trusted, distinct bus namespace when composed with other circuits under one authority. The complete AIR/preprocessing bundle must be retained together. recursion/tests/native_bus_circuit.rs checks native tower and polynomial proofs, including rejection of cross-circuit public swaps and locally valid forged gate/hash payloads. This non-hiding backend proves the complete native recursive verifier described below. Its minimum-height constructor pads trusted inactive rows for larger initial PCS folds, without adding bus occurrences. Its Keccak table uses the upstream 1,625 bit columns and computes bus limbs from constrained bits, avoiding the indexed backend's 100 extra limb columns.

• Full native Tower128 recursion. prepared::PreparedNativeBinaryWhirLayer builds a complete native scalar verifier for a trusted Tower32 or Tower128 additive-WHIR MultiStark authority, including product GKR, generic sumcheck, AIR evaluation and both main/preprocessing openings. It proves that verifier over Tower128 using native hash tables (Keccak or Blake3) and product buses, and verifies against independently supplied child public values. Checked child tokens must match the retained authority identity before packing or witness execution. The output authority can be used as the next layer's trusted child. recursion/examples/native_binary_recursion.rs demonstrates one actual native outer proof; the prepared integration test covers wrong statements and foreign-authority rejection. Graph, trace and initial codeword limits are explicit; codeword counts exclude Merkle trees and proving workspaces. Dense Keccak openings currently cause substantial growth in later layers. These proofs are non-hiding.

• Full native folding recursion. prepared::PreparedNativeBinaryLayer verifies a trusted tower MultiStark authority committed with the BaseFold folding PCS (BinaryNativeAuthority) in a Tower128 circuit and proves it with the same folding PCS, product buses and native Keccak. Each output PCS draws its derived query count plus query_draw_slack candidates in circuit. The output authority is the next layer's trusted child; grouped, indexed and BLAKE3-hashed children are rejected before graph construction. These proofs are non-hiding.

• Full native polynomial recursion. prepared::PreparedNativeBinaryPolyWhirLayer verifies a trusted Poly64 additive-WHIR MultiStark proof in a Poly64 circuit, with Poly192 challenges represented by three coefficient cells. Product GKR, generic sumcheck, AIR evaluation, main openings and independently committed preprocessing openings all use native polynomial arithmetic. Base oracle rows serialize as eight bytes, while challenge oracle rows serialize as 24 coefficient-order bytes; base rows constrain the upper two coefficients to zero. Public values remain native Poly64 cells. The prepared owner checks authority identity, binds the caller's expected statement and exposes its output authority for another layer. recursion/examples/native_poly_recursion.rs produces an actual native outer proof; integration tests also reject changed statements and foreign tokens. The same non-hiding and resource limits as the Tower128 path apply.

• Construction budgets for native owners. Both prepared owners expose from_native_authority_with_construction_limits. CircuitConstructionLimits bounds retained expression nodes, pending connections, non-primitive calls and their slots at periodic checkpoints. A checkpoint can exceed a bound by its local group of work; the final builder also checks before lowering. These counts are separate from final witness/operation limits, trace cells and initial codeword cells, and do not bound bytes or process memory. The examples expose --max-expression-nodes and apply all four entry budgets.

• Non-native binary byte-hash transcript. BinaryTower128Challenger has a separate, fallible inherent API (new, with_initial_limbs, observe, observe_slice, observe_digest, sample, sample_bits, check_witness). It matches native BinaryChallenger<BinaryField128, HashChallenger<u8, H, 32>> for H = Keccak256Hash or p3_blake3::Blake3, selected by the fixed ByteHash passed to its constructor. It is separate from the prime-field RecursiveChallenger trait.

  • The initial transcript is empty or an even number of raw bytes, supplied as low-byte-first 16-bit limbs. There is no length prefix or padding. A tower observation appends its eight low-first limbs (the raw little-endian Wiedemann coordinates); a digest observation appends all sixteen 16-bit limbs in natural byte order. External initial and digest limbs are constrained to base-field integers at most 65535. The host base field must be an odd-characteristic PrimeField64 with order above 65535.
  • An observation clears unread output bytes and appends to the next hash input. A refill hashes that entire input; the resulting digest becomes both the forward input for the next chained hash and the current output. Sampling draws bytes from the end of that digest, retaining a short remainder across draws and refilling only when it is exhausted. Thus the first sample from an empty transcript starts with the last byte of H([]), while a refill after consuming its digest hashes H(previous_digest); later observations are appended to that digest in forward order before hashing. A field sample consumes 16 bytes and interprets them as raw little-endian tower coordinates, with no rejection sampling.
  • sample_bits(bits) consumes eight bytes even when bits == 0, returning Boolean targets for the requested low bits; bits must be below usize::BITS. By contrast, check_witness(0, witness) leaves the transcript and builder untouched. For nonzero difficulty, check_witness observes the canonical witness, samples eight bytes and constrains the requested low bits to zero. This is witness checking; native grinding search is outside this API.
  • Every target and ExprId used with one challenger must belong to the same CircuitBuilder graph; expression IDs do not enforce graph ownership. Enable the matching Keccak-f or BLAKE3 compression operation before a refill, and register its existing preprocessor, AIR builder and prover together with the statement table when proving. Bind dynamic transcript limbs, witnesses and returned samples through StatementExport::Base in an agreed order. An error leaves the challenger's transcript state unchanged for retry, although expressions or constraints already added to the builder by a fallible gadget may remain.

• Native binary transcript hosts. The challenger's _with_host methods share the same transcript implementation with an explicit BinaryCircuitHost. PrimeBinaryEncoding<BF> preserves integer words; NativeBinaryEncoding uses checked raw coordinates and native Keccak tables. Word packing, digest compression, refill order, partial samples and Poly192 coefficient serialization are tested across tower and polynomial carriers. Native BLAKE3 hashing is not yet available through this host. These APIs do not by themselves implement a complete binary-host proof verifier.

• Native byte Merkle verification. verify_byte_hash_mmcs_opening_bytes_with_host authenticates serialized rows with the chosen host, sharing the prime API's mixed-height injection, index bounds and cap selection. Native tests cover odd-width rows, non-power-of-two heights, tower/polynomial carriers and a cap at the leaf layer. The caller still supplies trusted row widths, heights and serialization rules. verify_byte_hash_mmcs_opening_bytes_with_host_arity::<_, 4> opens trees whose nodes compress four digests, in the level order of p3's MerkleTreeMmcs. Under Keccak a four-digest node hashes 128 bytes, one Keccak-f block like a pairwise node, so a path takes about half the Keccak-f calls. A native WHIR recursion layer chooses its output trees' arity in NativeBinaryRecursionOptions::arity; both native recursion examples use pairwise trees by default and four-digest trees under --hash keccak, and --merkle-arity overrides the arity.

• Binary hash configurations. p3_test_utils::binary_field_params provides the configuration p3-binary-pcs tests with, once per hash (keccak and blake3 submodules with identical item names):

  • Merkle commitments over any tower level that serialize rows to bytes, hash with Keccak-256 or BLAKE3, and compress node pairs with the same hash;
  • BinaryChallenger transcripts over the same byte hash.

• Binary hash AIRs. test-utils/tests/binary_hashes.rs checks that the Keccak-f and BLAKE3 AIRs over GF(2^128) accept their generated traces and reject a non-bit cell or a flipped bit, and that the byte-hash commitments round-trip and reject tampering.

• In-circuit Keccak. Prime-field circuits can call Keccak-f[1600] as a non-primitive operation (CircuitBuilder::enable_keccak_f1600 / add_keccak_f1600).

  • State layout: the state is 100 little-endian 16-bit limbs (limb 4·i + k is limb k of lane i = x + 5·y), matching p3-keccak-air.
  • Proving: the KeccakF1600Air table runs KeccakAir over 24 rows per call and ties the input and output limbs to the witness table through WitnessChecks lookups. KeccakAir's bit decompositions keep every limb below 2^16.
  • Registration: register it with KeccakF1600Preprocessor, KeccakF1600AirBuilder and KeccakF1600Prover.
  • Merkle compression: keccak256_compress builds on it. It computes Keccak-256 of two 32-byte digests in one call, matching CompressionFunctionFromHasher<Keccak256Hash, 2, 32>, the node compression of a Keccak Merkle tree.
  • Keccak-256 sponge: keccak256_limbs hashes messages of any even byte length. The first block fills the zero state directly; later blocks are XORed in with a bitwise gadget.
  • Leaf hash: keccak256_field_elements matches SerializingHasher<Keccak256Hash>, the leaf hash of a Keccak Merkle tree. Elements are serialized exactly as Plonky3 does it (Montgomery fields such as BabyBear hash x·2^32 mod p). Each serialized value is decomposed into canonical bits, so y + p cannot stand in for y.

• In-circuit BLAKE3. enable_blake3_compress / add_blake3_compress expose one BLAKE3 compression per call.

  • Limb layout: 56 input limbs (block, chaining value, counter, block length, flags, each 32-bit word as a little-endian 16-bit pair) and 32 output limbs.
  • Proving: the Blake3CompressAir table runs p3-blake3-air's Blake3Air, one compression per row, with each call's real counter, length and flags. It exposes the limbs through dedicated columns tied to Blake3Air's bit columns.
  • Registration: register it with Blake3CompressPreprocessor, Blake3CompressAirBuilder and Blake3CompressProver.
  • Gadgets: built on the compression are blake3_limbs (messages of any even byte length, through the full chunk tree), blake3_compress_digests (CompressionFunctionFromHasher<Blake3, 2, 32>) and blake3_field_elements (SerializingHasher<Blake3>).

• Merkle openings. verify_byte_hash_mmcs_opening constrains an opening of a Keccak-256 or BLAKE3 MerkleTreeMmcs batch commitment, mirroring the native binary-arity verify_batch:

  • Inputs: the opened rows of several matrices with their heights, the little-endian index bits, the sibling digests (bottom-up) and a cap of any power-of-two root count.
  • Heights: as natively, they need not be powers of two, but each must be ceil(max_height / 2^k). The index is constrained below the tallest height.
  • Injection: shorter matrices' rows are folded in at the level where their height is reached.
  • Cap: the remaining index bits select the cap root.
  • Shorthands: verify_byte_hash_merkle_path, verify_keccak_merkle_path and verify_blake3_merkle_path cover the single-matrix, one-root case.

• Recursion over hash tables. A batch proof whose circuit used Keccak-f or BLAKE3 can be verified by the next recursion layer.

  • Low-level: pass KeccakF1600Prover / Blake3CompressProver among the input table provers of verify_p3_batch_proof_circuit and replay_batch_layer_transcript.
  • Built-in backends: PcsRecursionBackend::input_table_provers adds these tables to the backend's own input provers in the input manifest's order, through with_hash_table_input_provers. The FRI and WHIR backends use it.
  • No relaxation: hash tables are only ever added. With its hash entries removed, the manifest must still list the backend's own tables exactly, as before.

Not yet supported

• Native scalar recursion for indexed lookup relations or a BLAKE3 circuit host. The complete native Tower128 and Poly64 paths use product buses, Keccak and additive WHIR; those other input adapters still use prime hosts.
• Efficient bounded-size composition across many native layers. Output authorities can prepare subsequent layers, but dense Keccak oracle openings currently make those verifier circuits grow substantially.
• Folding-PCS MMCS trees of arity above two.

Benchmarks

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

NOTE: This library is still at an early stage, parameters have not been finely tuned yet, and as such performance results here may not reflect the full potential of the library.

Setup

The reference examples are a Plonky3 uni-stark proof of the Keccak AIR imported directly, a Plonky3 batch-stark proof of the Fibonacci sequence generated with the CircuitBuilder of this library, and a 2-to-1 aggregation tree over basic p3-batch-stark proofs.

• Keccak example: set number of hashes with -n argument

RUSTFLAGS="-Ctarget-cpu=native -Copt-level=3" RUST_LOG=info cargo run --release \
    --example recursive_keccak --features parallel -- -n 2500 

• Fibonacci example: set element index in the sequence with -n argument

RUSTFLAGS="-Ctarget-cpu=native -Copt-level=3" RUST_LOG=info cargo run --release \
    --example recursive_fibonacci --features parallel -- -n 10000

• 2-to-1 aggregation example:

RUSTFLAGS="-Ctarget-cpu=native -Copt-level=3" RUST_LOG=info cargo run --release \
    --example recursive_aggregation --features parallel -- --field koala-bear

Parameterization

Each example supports additional parameterization around the FRI parameters, namely:

• --log-blowup: logarithmic blowup factor for the LDE. Default 2.
• --max-log-arity: maximum arity allowed during the FRI folding phases. Default 2 (3 for the aggregation example, except with --zk or --hash poseidon1).
• --log-final-poly-len: logarithmic size (or degree) allowed for the final polynomial after folding. Default 5 (6 for the aggregation example).
• --cap-height: the height at which the MMCS tree is truncated for commitments. Default 0.
• --commit-pow-bits: additional PoW grinding during the FRI commit phase. Default 0.
• --query-pow-bits: additional PoW grinding during the FRI query phase. Default 15.
• --num-recursive-layers: number of recursive proofs to be generated in a chain, starting from the base proof (Keccak or Fibonacci). Default 3. For the aggregation example, this is the depth of the aggregation tree. Default 1.
• --public-lanes: number of public lanes for the table packing in recursive layers. Default 1.
• --alu-lanes: number of ALU lanes for the table packing in recursive layers. Default 3.
• --horner-packed-steps: number of consecutive Horner steps packed per ALU row. Default 4.
• --recompose-lanes: number of recompose lanes for the table packing in recursive layers. Default 1.
• --security-level: targeted conjectured security in bits. Default 124.
• --zk: activates the Zero-Knowledge property. Default false.

The aggregation example additionally accepts --concurrent-pairs, which proves all pairs of an aggregation level concurrently against one shared preparation. It shortens the whole tree, but each individual proof then shares the cores, so its reported per-layer time grows; the results below are measured without it.

The examples run on the mimalloc allocator and keep freed memory mapped between recursion layers.

Results

Running on a Apple M4 pro, 14 Cores, with KoalaBear field and extension of degree 4, using default parameters mentioned above at a 124-bit security target, performance benchmarks are as follows:

NOTE: In production systems, circuits may be pre-generated offline and cached to reduce overhead in fixed recursive layers.

• Keccak AIR program: (1,000 hashes)

  • Base uni-stark proof: 707 ms
  • 1st recursion layer: 337 ms
  • 2nd and next recursion layers: 100 ms

• Fibonacci multi-AIR program: (10,000th element)

  • Base batch-stark proof: 39.2 ms
  • 1st recursion layer: 61 ms
  • 2nd and next recursion layers: 100 ms

• 2-to-1 aggregation:

  • Base batch-stark proof: 13.9 ms
  • 1st aggregation layer: 85 ms
  • 2nd and next aggregation layers: 174 ms

• 8-to-1 aggregation:

  • Base batch-stark proof: 13.9 ms
  • 1st aggregation layer: 229 ms
  • 2nd and next aggregation layers: 641 ms

Roadmap

This page tracks planned improvements and known optimization opportunities.

Performance

• Additional optimization passes: More aggressive dead-node pruning, common subexpression elimination, and chain fusion in the circuit optimizer.

Flexibility

• Configurable WIDTH/RATE: Currently fixed at WIDTH=16, RATE=8 for 32-bit fields, WIDTH=8, RATE=4 for Goldilocks. Making these configurable would support wider permutations and different security/performance trade-offs.
• Multi-shape FRI verification: A single verifier circuit that can handle proofs with different trace sizes, reducing the need for proof lifting.
• Binary fields: Circuits already run over the Plonky3 binary tower, and binary hash configurations are in p3-test-utils (see Binary Fields and Binary Hashes). In-circuit Keccak-f[1600], the Keccak-256 sponge, digest compression and field-element leaf hashing are available. In-circuit BLAKE3 (any message length, with the chunk tree) and single-matrix Keccak-256 and BLAKE3 Merkle paths are available too. Keccak-256 and BLAKE3 MMCS batch openings (mixed heights, powers of two or not, multi-root caps) and recursion over proofs containing these tables are available too. The remaining steps are proving binary-field circuits with the binary PCS, and recursively verifying binary proofs.

Glossary

AIR — Algebraic Intermediate Representation. A set of polynomial constraints that define the validity of an execution trace. Each row of the trace must satisfy the AIR's constraints.

ALU — Arithmetic Logic Unit. In this library, the primitive chip that handles add, mul, sub, div, bool_check, and mul_add operations via selector columns.

CTL — Cross-Table Lookup. A mechanism to enforce consistency between different AIR tables by proving that multisets of tuples match across tables. Uses the LogUp argument.

D — Extension field degree. The recursion stack uses degree-4 extensions (D = 4), meaning each extension field element is represented by 4 base field elements.

FRI — Fast Reed-Solomon Interactive Oracle Proof. The polynomial commitment scheme used by Plonky3. Proves that a committed function is close to a low-degree polynomial via iterative folding and random queries.

IR — Intermediate Representation. The deterministic sequence of operations (constants, public inputs, arithmetic, non-primitives) that defines a circuit's computation.

LDE — Low-Degree Extension. Evaluating a polynomial on a domain larger than its degree, used to create redundancy for FRI queries. The blowup factor controls the domain expansion ratio.

LogUp — Logarithmic derivative lookup argument. The specific lookup protocol used to enforce CTL relations between tables. Based on Ulrich Haböck's construction.

MMCS — Mixed Matrix Commitment Scheme. Plonky3's abstraction for committing to matrices of field elements. Typically instantiated with Merkle trees over Poseidon2 hashes.

PCS — Polynomial Commitment Scheme. A cryptographic primitive that allows committing to a polynomial and later proving evaluations at chosen points. FRI is the PCS used here.

Poseidon2 — An algebraic hash function optimized for arithmetic circuits. Used for Merkle tree hashing and Fiat-Shamir challenges. Parameterized by WIDTH (number of state elements) and RATE (elements absorbed per permutation).

RAP — Randomized AIR with Preprocessing. An extension of AIR that supports preprocessed columns (known to the verifier before the proof) and randomized columns (computed after an initial commitment round).

STARK — Scalable Transparent Argument of Knowledge. A proof system based on polynomial IOPs and hash functions (no trusted setup). Plonky3 implements uni-STARKs (single AIR) and batch-STARKs (multiple AIRs with shared FRI).

Target — An identifier for a value in the circuit's expression graph. Each Target (also called ExprId) refers to either a constant, a public input, or the output of an operation.

WitnessId — An index into the global witness memory bus. After circuit compilation, each Target is assigned a WitnessId that identifies its slot in this shared memory.