# Die GKR-Engine

> Die Beweis-Engine im Zentrum von Apogee. Warum ein geschichteter GKR-Schaltkreis nur seine Eingaben committet, wie ein einziger Rückwärtsdurchlauf aus Sumchecks einen ganzen Schaltkreis auf einen einzigen Punkt zurückführt und was das einbringt.

Jeder Shard in Apogee wird auf dieselbe Weise bewiesen: durch den Schaltkreis seiner Familie, geschrieben als Stapel von Schichten, den die GKR-Engine rückwärts durchläuft, von den Ausgaben des Schaltkreises bis zu seinen committeten Spalten. Diese Seite erklärt, warum diese Engine im Zentrum des Systems steht und warum sich die Front des Beweisens in Richtung der Familie von Beweissystemen bewegt, zu der sie gehört.

## Die Idee

Der klassische Weg, eine Berechnung zu beweisen, besteht darin, sie als Tabelle anzulegen, jede Spalte einschließlich der Zwischenwerte zu committen und zu beweisen, dass eine Menge von Constraints über der Tabelle verschwindet. Die Commitments sind der teure Teil: Jede committete Spalte kostet eine Multi-Skalar-Multiplikation oder einen Merkle-Baum und eine Öffnung an jedem Punkt, nach dem das Constraint-Argument fragt.

GKR, nach Goldwasser, Kalai und Rothblum, ändert, was committet werden muss. Die Berechnung ist ein **geschichteter Schaltkreis**. Nur die unterste Schicht, die Eingaben, wird committet. Jede Schicht darüber ist durch Gates über der Schicht darunter definiert, und der Prover committet sie nie. Stattdessen wird eine Behauptung über die oberste Schicht durch einen Sumcheck auf eine Behauptung über die Schicht darunter zurückgeführt, dann auf die nächste, bis die Behauptungen bei den committeten Eingaben ankommen, alle an einem einzigen zufälligen Punkt. Eine einzige Öffnung löst sie ein.

> [!NOTE]
> **Eine Analogie, kein Name.** Ein herkömmlicher Prover ist eine Rakete: Er schleppt jeden Zwischenwert, den er erzeugt, committet bis ans Ziel und bezahlt für die Masse. Die GKR-Engine verhält sich eher wie der Warp-Antrieb der Science-Fiction, der den Raum um das Schiff bewegt statt des Schiffs selbst. Was reist, ist die *Behauptung*, Schicht für Schicht durch den Schaltkreis nach unten bewegt, während die Zwischenschichten überhaupt nirgendwohin getragen werden.

Was das einer zkVM einbringt:

- **Zwischenwerte kosten kein Commitment.** Ein Familienschaltkreis kann Hunderte innerer Spalten, Produktbäume und Bruchbäume berechnen, und nichts davon wird je committet. Nur seine Trace-Spalten werden committet.
- **Ein Öffnungspunkt pro Shard.** Der Rückwärtsdurchlauf endet mit Behauptungen über jede committete Spalte an demselben Punkt. Ein Shard braucht genau eine gebündelte Öffnung, 704 Byte, unabhängig davon, wie viele Spalten er hat.
- **Die Arbeit des Provers ist Körperarithmetik.** Der Sumcheck jeder Schicht ist linear in der Größe der Schicht, über `Fr`, ohne Commitment, Transformation oder Hash pro Schicht.
- **Argumente setzen sich innerhalb des Schaltkreises zusammen.** Die Grand Products des Speicherarguments und die LogUp-Summen der Lookups sind einfach weitere Schichten desselben Schaltkreises, reduziert im selben Durchlauf.

## Ein Familienschaltkreis, Schicht für Schicht

> Figure: Ein Familienschaltkreis. Der Prover berechnet jede Schicht einmal von unten nach oben (gestrichelt). Der Beweis läuft nach unten: Die Ausgaben werden absorbiert, dann ist jeder Übergang ein Sumcheck, der Behauptungen über eine Schicht in Behauptungen über die Schicht darunter verwandelt, bis sich alle an einem einzigen Punkt auf den committeten Spalten treffen.

Die unterste Schicht bilden die committeten Spalten des Shards, in drei Arten, die sich darin unterscheiden, wann sie gebunden werden: **`M`**, die Speicherspalten, committet im globalen Transkript der Aussage, bevor es irgendeine Speicher-Challenge gibt; **`W`**, die Witness-Spalten, committet im eigenen Transkript des Shards; und **`S`**, die Setup-Spalten, gebunden durch die Programmidentität oder durch die Zeremonie. Daneben stehen **virtuelle Tabellen**: geschlossene Formen wie der Zeilenindex oder der 16-Bit-Bereich, die der Verifier an jedem beliebigen Punkt auswertet und die nie committet werden.

Oberhalb von Schicht 0 hat jeder Familienschaltkreis denselben Aufbau:

1. **Gate-Liste 0** berechnet Zeile für Zeile die Speicherblätter (die Lese- und Schreibtupel jeder Abfrage), die Lookup-Brüche (ein Paar `(numerator, denominator)` pro Lookup, dazu das der Tabelle) und jedes **Constraint-Gate**: die Constraints der Familie, jedes ein Polynom, das auf jeder Zeile verschwinden muss.
2. **Zeilenweise Listen** kombinieren Geschwisterblätter: Ein Produktbaum multipliziert Tupel, ein Bruchbaum addiert Brüche als `(n_a·d_b + n_b·d_a, d_a·d_b)`, bis jede Zeile einen Knoten pro Baum enthält.
3. **Halbierende Listen**, eine pro Variable der Höhe des Shards, kombinieren die Zeilen paarweise: die erste Hälfte mit der zweiten. Nach `n` von ihnen erreicht der Schaltkreis eine Spitze ohne Variablen: die Lesewurzel des Shards, seine Schreibwurzel sowie den finalen Zähler und Nenner jedes Lookup-Kanals.

Ein einziger Schaltkreis beweist also die Constraints der Familie, berechnet ihren Beitrag zum Speicherargument und summiert ihre Lookups, in einem einzigen Durchlauf. Jedes Gate hat höchstens Grad 2; jedes Rundenpolynom jedes Sumchecks ist also kubisch.

## Der Rückwärtsdurchlauf

Der Prover materialisiert jede Schicht einmal, von unten nach oben. Der Beweis läuft dann nach unten, und sein Transkriptablauf ist für jeden Schaltkreis derselbe:

1. **Die Ausgaben werden zuerst absorbiert**, sodass der Prover an die Wurzeln gebunden ist, bevor es irgendeine Challenge gibt.
2. Für jeden Übergang von Schicht `k + 1` hinunter zu Schicht `k` bündelt eine Challenge `λ` jede Behauptung über Schicht `k + 1` zusammen mit jedem Constraint-Gate der Liste zu einer einzigen Summe. Ein **Sumcheck** reduziert diese Summe auf eine Auswertung an einem zufälligen Punkt `ρ`, mit einer kubischen Nachricht pro Variable.
3. Der Prover nennt die Werte der Spalten von Schicht `k` an der Stelle `ρ`. Bei einer halbierenden Liste nennt er beide Kinder, und eine weitere Challenge `τ` führt sie zu einer Behauptung pro Spalte zusammen.
4. Auf Schicht 0 hat jede committete Spalte eine einzige Behauptung, alle am selben Punkt `u`.

Die eine Mercury-Öffnung des Shards beweist diese Behauptungen gegen die Commitments: die der Speicherspalten aus der Aussage, die der Witness-Spalten aus dem Shard-Beweis, die der Setup-Spalten aus dem Verifikationsschlüssel. Virtuelle Tabellen wertet der Verifier selbst aus.

Constraint-Gates fahren kostenlos mit. Ein Constraint-Gate behauptet überall 0; es tritt also dem Batch des Übergangs bei, in dem es liegt, und ein verletztes Gate macht die gebündelte Summe mit überwältigender Wahrscheinlichkeit ungleich null. Ein einziger Fehler `LayerInconsistency` deckt eine falsche absteigende Behauptung und ein verletztes Gate gleichermaßen ab; eine gebündelte Summe kann die beiden nicht unterscheiden, und der Beweis wendet nichts dafür auf, sie zu unterscheiden.

## Woher die Soundness kommt

Jede Challenge wird nach allem gezogen, was sie schützt:

- der Ausgabepunkt nach den Ausgaben, sodass ein Prover keine Tabellen wählen kann, die nur dort mit der Wahrheit übereinstimmen, wo geprüft wird;
- `λ` nach den Behauptungen und dem Punkt, sodass eine falsche Behauptung oder ein verletztes Gate nur an einer Nullstelle eines von null verschiedenen Polynoms in `λ` überlebt;
- jede Sumcheck-Challenge nach dem kubischen Polynom ihrer Runde, sodass ein falsches kubisches Polynom mit Wahrscheinlichkeit höchstens `3/|Fr|` mit dem richtigen übereinstimmt;
- `τ` nach den Werten beider Kinder.

Summiert über alle Übergänge eines registrierten Schaltkreises bei seiner Standardhöhe bleibt der Soundness-Fehler unter `2^14/|Fr|`, mit Fiat–Shamir über dem Poseidon2-Transkript im Random-Oracle-Modell.

## Schaltkreise als Daten

Ein Schaltkreis ist kein Code. Er ist ein `CircuitArtifact`: seine committeten Spalten mit Namen, seine virtuellen Tabellen, seine Gate-Listen mit sieben Gate-Formen, eine flache Liste derselben Relationen, seine Lookups und seine Padding-Zeile, kanonisch serialisiert. Vier Gesetze halten jedes Artefakt in einer konsistenten Form: Jeder Operand ist dort lesbar, wo er gelesen wird, die Breite jeder Liste wird aus ihren Gates abgeleitet, die oberste Schicht besteht genau aus den Ausgaben, und die geschichteten Gates und die flachen Relationen bilden eine einzige Constraint-Menge. Sie laufen einmal, dort, wo ein Artefakt gebaut oder ein Schlüssel geladen wird, nie pro Beweis.

Zwei Folgen sind für alle wichtig, die das System bewerten:

- **Ein Verifikationsschlüssel führt seine Schaltkreise mit, und der Verifier gleicht sie mit seiner eigenen Registry ab.** Die Programmidentität bindet das Programm; die Registry bindet die Schaltkreise, die es beweisen.
- **Die Schaltkreise lassen sich von einer zweiten Implementierung prüfen.** Das Crate `checker` implementiert die Gesetze, die Lookup-Regeln und den Padding-Vertrag neu, ohne Code mit den Konstruktoren zu teilen, und wertet Gates ausschließlich über den einen Gate-Kernel aus, den beide Seiten als semantische Autorität verwenden.

## Die Kosten

Die Engine tauscht Commitments gegen Speicher. Der Vorwärtsdurchlauf hält jede innere Schicht als Körperelemente: etwa 8,4 GiB für einen `2^20`-Shard der breitesten Befehlsfamilie und 42 GiB für einen `KECCAK_F`-Shard der Höhe `2^18`, dessen Schaltkreis 5.490 innere Spalten berechnet. Deshalb ist die Beweiserzeugung speichergebunden, deshalb sind Höhen ein Tuning-Parameter, und deshalb beschränkt [der Streaming-Prover](https://apogee.gweb3networks.com/docs/architecture/streaming) den Speicherbedarf durch die gleichzeitig bearbeiteten Shards. Die Beweisgröße wächst nur um eine Sumcheck-Runde pro Variable und Schicht: Der Beweis eines `KECCAK_F`-Shards umfasst 381.100 Byte bei `2^18` gegenüber 373.276 bei `2^16`, für die vierfache Arbeit.

Die Spezifikation: [Die GKR-Engine](https://apogee.gweb3networks.com/docs/auditors/spec/gkr) sowie die eigene Seite jeder Familie unter [Auditoren](https://apogee.gweb3networks.com/docs/auditors).