RESEARCH — NOTHING BUILT
— Recursion —

SCOPING, NOT IMPLEMENTATION

A literature-review document, not a design doc. Its job is to make 'should we start this' a real decision later, not an open-ended fear.

What we have today

One Winterfell proof over VmAir, Blake3-hashed, ~5–11 KB for the examples in this repo, growing with trace length. It verifies off-chain in milliseconds. Nothing about it is compact enough, or in a format cheap enough, to check inside an EVM transaction — a STARK is typically tens of KB minimum, too large and too gas-expensive to verify directly. See the On-Chain Verifier page.

The two paths

(a) Recursive STARK composition. Prove, in a second, smaller STARK, the statement "the first STARK proof verifies." This stays inside STARK-land (no pairing-based trusted setup), but means implementing a STARK verifier as an AIR — encoding FRI folding, Merkle path checks, and out-of-domain constraint evaluation as constraints in a new circuit. Well-trodden elsewhere (SP1, RISC Zero, StarkWare's own construction do this) — but not yet designed for this specific AIR.

(b) External SNARK wrapping. Prove "the STARK verifier accepts this proof" as a Groth16 or PLONK circuit over BN254 — a field switch from the current 128-bit prime, since pairing-friendly curves use different primes. Needs a trusted setup and R1CS/arithmetic-circuit tooling entirely outside what this repo currently touches.

Both paths converge on the same hard sub-problem: implementing this STARK verifier's arithmetic as constraints in some proving system.

What's specific to this AIR, versus generic

  • Field: Winterfell's 128-bit prime. Any recursive verifier circuit must do arithmetic in this exact field, or handle a field switch explicitly — get this wrong and the recursive proof verifies something other than intended.
  • Hash: Blake3_256 — no EVM precompile, no widely-used circuit-friendly implementation. The Keccak-family switch flagged in the On-Chain Verifier page applies here too, and should happen first regardless of which recursion path is chosen.
  • Constraint count: VmAir has one transition constraint shape today — unusually small. A recursive circuit's size scales with the inner AIR's complexity, so it would need redoing as branching, registers, and memory grow the AIR. Worth sequencing after the ISA stabilizes.

Open questions

  1. Do we even need hiding? This system has no secret witness anywhere — see Architecture. If that never changes, recursion only needs to solve succinctness, not zero-knowledge — a meaningfully smaller problem, worth confirming before designing around hiding that isn't needed.
  2. What's the real proving-time budget? No target has been set — current settings are correctness-first, not performance-first.
  3. Composition depth: one level, or folding many executions before the final wrap? The latter amortizes the expensive wrap step but is meaningfully more design work.
  4. Trusted setup, if path (b): a per-circuit Groth16 setup versus a universal PLONK setup — different stacks entirely.

Verdict

This is a 2–3 month research-and-implementation project, done properly.

It does not block the ISA expansion, the MCP endpoint, or anything else in this repo. Nothing here is implemented, and nothing should be started opportunistically alongside other work — it deserves being picked up as its own deliberate effort, after the Keccak-hasher switch and after the AIR has stabilized. See the real roadmap for where this sits relative to everything else.

Full document, including references to SP1's and StarkWare's own recursion writeups: docs/RECURSION.md.