# The GKR Engine

> The proving engine at the centre of Apogee. Why a layered GKR circuit commits only its inputs, how one backward pass of sumchecks funnels a whole circuit to a single point, and what that buys.

Every shard in Apogee is proved the same way: by its family's circuit, written as a stack of layers, run backward by the GKR engine from the circuit's outputs to its committed columns. This page is about why that engine sits at the centre of the system, and why the family of proof systems it belongs to is where the frontier of proving is moving.

## The idea

The classical way to prove a computation is to lay it out as a table, commit to every column, the intermediate values included, and prove that a set of constraints vanishes over the table. Commitments are the expensive part: every committed column costs a multi-scalar multiplication or a Merkle tree, and an opening at each point the constraint argument asks about.

GKR, after Goldwasser, Kalai and Rothblum, changes what has to be committed. The computation is a **layered circuit**. Only the bottom layer, the inputs, is committed. Every layer above it is defined by gates over the layer below, and the prover never commits to it. Instead, a claim about the top layer is reduced to a claim about the layer beneath it by one sumcheck, then to the next, until the claims land on the committed inputs, all at a single random point. One opening settles them.

> [!NOTE]
> **An analogy, not a name.** A conventional prover is a rocket: it hauls every intermediate value it produces to the destination, committed, and pays for the mass. The GKR engine behaves more like the warp drive of science fiction, which moves the space around the ship rather than the ship itself. What travels is the *claim*, moved down through the circuit layer by layer, while the intermediate layers are never carried anywhere at all.

What that buys a zkVM:

- **Intermediate values cost no commitment.** A family circuit can compute hundreds of inner columns, product trees and fraction trees, and none of them is ever committed. Only its trace columns are.
- **One opening point per shard.** The backward pass ends with every committed column claimed at the same point. A shard needs exactly one batched opening, 704 bytes, however many columns it has.
- **Prover work is field arithmetic.** Each layer's sumcheck is linear in the layer's size, over `Fr`, with no commitment, transform or hash per layer.
- **Arguments compose inside the circuit.** The memory argument's grand products and the lookups' LogUp sums are just more layers of the same circuit, reduced in the same pass.

## A family circuit, layer by layer

> Figure: One family circuit. The prover computes every layer upward once (dashed). The proof runs downward: the outputs are absorbed, then each transition is a sumcheck that turns claims about one layer into claims about the layer below, until all of them meet at one point on the committed columns.

The bottom layer is the shard's committed columns, in three kinds that differ in when they are bound: **`M`**, the memory columns, committed in the statement's global transcript before any memory challenge exists; **`W`**, the witness columns, committed in the shard's own transcript; and **`S`**, the setup columns, bound by the program identity or by the ceremony. Beside them sit **virtual tables**: closed forms such as the row index or the 16-bit range, which the verifier evaluates at any point and which are never committed.

Above layer 0 every family circuit has the same anatomy:

1. **Gate list 0** computes, row by row, the memory leaves (each query's read and write tuples), the lookup fractions (one `(numerator, denominator)` pair per lookup, plus the table's), and every **enforcing gate**: the family's constraints, each a polynomial that must vanish on every row.
2. **Row-wise lists** combine sibling leaves: a product tree multiplies tuples, a fraction tree adds fractions as `(n_a·d_b + n_b·d_a, d_a·d_b)`, until each row holds one node per tree.
3. **Halving lists**, one per variable of the shard's height, combine the rows pairwise: the first half with the second. After `n` of them the circuit reaches a top with no variables: the shard's read root, its write root, and each lookup channel's final numerator and denominator.

So one circuit proves the family's constraints, computes its contribution to the memory argument, and sums its lookups, in one pass. Every gate has degree at most 2, so every round polynomial of every sumcheck is a cubic.

## The backward pass

The prover materializes every layer once, upward. The proof then runs downward, and its transcript schedule is the same for every circuit:

1. **The outputs are absorbed** first, so the prover is committed to the roots before any challenge exists.
2. For each transition from layer `k + 1` down to layer `k`, a challenge `λ` batches every claim on layer `k + 1`, together with every enforcing gate of the list, into one sum. A **sumcheck** reduces that sum to an evaluation at a random point `ρ`, one cubic message per variable.
3. The prover states the values of layer `k`'s columns at `ρ`. For a halving list it states both children, and a further challenge `τ` merges them into one claim per column.
4. At layer 0 every committed column has one claim, all at the same point `u`.

The shard's single Mercury opening proves those claims against the commitments: the memory columns' from the statement, the witness columns' from the shard proof, the setup columns' from the verifying key. Virtual tables are evaluated by the verifier itself.

Enforcing gates ride along for free. An enforcing gate claims 0 everywhere, so it joins the batch of the transition it sits in, and a violated gate makes the batched sum nonzero with overwhelming probability. A single `LayerInconsistency` error covers a wrong descending claim and a violated gate alike; a batched sum cannot tell them apart, and the proof spends nothing on telling them apart.

## Why it is sound

Each challenge is drawn after everything it protects:

- the output point after the outputs, so a prover cannot pick tables that agree with the truth only where it will be checked;
- `λ` after the claims and the point, so a false claim or a violated gate survives only at a root of a nonzero polynomial in `λ`;
- each sumcheck challenge after its round's cubic, so a wrong cubic agrees with the true one with probability at most `3/|Fr|`;
- `τ` after both children's values.

Summed over every transition of a registered circuit at its default height, the soundness error stays under `2^14/|Fr|`, with Fiat–Shamir over the Poseidon2 transcript in the random-oracle model.

## Circuits as data

A circuit is not code. It is a `CircuitArtifact`: its committed columns by name, its virtual tables, its gate lists with seven gate shapes, a flat list of the same relations, its lookups and its padding row, serialized canonically. Four laws hold every artifact to a consistent form: every operand is readable where it is read, every list's width is derived from its gates, the top layer is exactly the outputs, and the layered gates and the flat relations are one constraint set. They run once, where an artifact is built or a key is loaded, never per proof.

Two consequences matter to anyone evaluating the system:

- **A verifying key carries its circuits, and the verifier holds them to its own registry.** The program identity binds the program; the registry binds the circuits that prove it.
- **The circuits can be checked by a second implementation.** The `checker` crate re-implements the laws, the lookup rules and the padding contract without sharing the constructors' code, and evaluates gates only through the one gate kernel both sides use as the semantic authority.

## The cost

The engine trades commitments for memory. The forward pass holds every inner layer as field elements: about 8.4 GiB for a `2^20` shard of the widest instruction family, and 42 GiB for a `2^18` `KECCAK_F` shard, whose circuit computes 5,490 inner columns. That is why proving is memory-bound, why heights are a tuning parameter, and why [the streaming prover](https://apogee.gweb3networks.com/docs/architecture/streaming) bounds memory by the shards in flight. Proof size grows only by one sumcheck round per variable per layer: a `KECCAK_F` shard's proof is 381,100 bytes at `2^18` against 373,276 at `2^16`, for four times the work.

The specification: [The GKR engine](https://apogee.gweb3networks.com/docs/auditors/spec/gkr), and every family's own page under [Auditors](https://apogee.gweb3networks.com/docs/auditors).
