# Soundness-Karte

> Jede Behauptung, die ein verifizierter Beweis aufstellt, das Argument, das sie trägt, und die genauen Abschnitte der Spezifikation, in denen dieses Argument formuliert und begründet wird.

Ein verifizierter Block begründet einen einzigen Satz: *Das Programm dieser Identität, gestartet an seinem Einsprung-pc auf seinem Image, mit dieser öffentlichen Eingabe und irgendwelchen Hilfsdaten (Advice), wird Befehl für Befehl bis zu `EXIT` mit diesem Status ausgeführt und hat dabei dieses Journal geschrieben.* Diese Seite zerlegt diesen Satz in die Behauptungen, aus denen er besteht, und führt jede zu dem Argument, das sie beweist.

## Das Programm

| Behauptung | Argument | Spezifikation |
| --- | --- | --- |
| Der Schlüssel beschreibt das registrierte Programm | beim Laden eines Schlüssels wird die Identität aus seiner eigenen Konfiguration, seinem Einsprung-pc und seinen Setup-Commitments neu berechnet; der Verifier vergleicht sie mit seiner eigenen Kopie | [Beweis §7.2](https://apogee.gweb3networks.com/docs/auditors/spec/proof#s7-2), [Programm §8](https://apogee.gweb3networks.com/docs/auditors/spec/program#s8) |
| Die Tabellen, die ein Beweis liest, sind die, die die Identität committet | die gebündelte Öffnung jedes Shards entnimmt ihre Setup-Commitments dem Schlüssel | [Beweis §5](https://apogee.gweb3networks.com/docs/auditors/spec/proof#s5) |
| Jede ausgeführte Zeile ist der Befehl des Programms an ihrem pc | der Decoder-Lookup, mit dem von der Zeile selbst gelesenen pc als Schlüssel, in eine Tabelle, deren aktive Zeilen one-hot und deren Padding-Zeilen `−1` sind | [Lookup §10](https://apogee.gweb3networks.com/docs/auditors/spec/lookup#s10), [Programm §5](https://apogee.gweb3networks.com/docs/auditors/spec/program#s5), [§6](https://apogee.gweb3networks.com/docs/auditors/spec/program#s6) |
| Der Speicher beginnt mit dem Image des Programms | die Init-Spalte von `INIT_TEARDOWN` ist eine Setup-Spalte, die von der Identität committet wird; kein aus der Datei stammendes Byte liegt außerhalb von Fenster 0 | [Speicher §6.2](https://apogee.gweb3networks.com/docs/auditors/spec/memory#s6-2), [§3.4](https://apogee.gweb3networks.com/docs/auditors/spec/memory#s3-4) |
| Die Ausführung beginnt am Einsprung-pc | das Anfangstupel des pc verwendet den Einsprung-pc des Schlüssels, den die Identität bindet | [Speicher §4.2](https://apogee.gweb3networks.com/docs/auditors/spec/memory#s4-2), [§6.2](https://apogee.gweb3networks.com/docs/auditors/spec/memory#s6-2) |
| Die Schaltkreise sind die richtigen | die Schaltkreise eines Schlüssels müssen bei seinen Höhen der Registry des Verifiers entsprechen und die Gesetze, die Speicherregeln und die Erfüllungsregel bestehen | [Beweis §7.2](https://apogee.gweb3networks.com/docs/auditors/spec/proof#s7-2), [Schaltkreise §1](https://apogee.gweb3networks.com/docs/auditors/spec/circuits#s1), [GKR §4.2](https://apogee.gweb3networks.com/docs/auditors/spec/gkr#s4-2) |

## Jede Zeile

| Behauptung | Argument | Spezifikation |
| --- | --- | --- |
| Eine Zeile befolgt ihren Befehl | die Constraint-Gates der Familie, null auf jeder Zeile, das Soundness-Argument jeder Familie | [add-sub §4](https://apogee.gweb3networks.com/docs/auditors/spec/add-sub#s4), [jump-branch-slt §5](https://apogee.gweb3networks.com/docs/auditors/spec/jump-branch-slt#s5), [shift-bitwise §5](https://apogee.gweb3networks.com/docs/auditors/spec/shift-bitwise#s5), [mul-div §5](https://apogee.gweb3networks.com/docs/auditors/spec/mul-div#s5), [memory-ops §3–§6](https://apogee.gweb3networks.com/docs/auditors/spec/memory-ops#s3) |
| Eine Zeile stellt genau die Abfragen ihres Befehls | jede Maske festgelegt auf `m_pc` mal die Arten, die diese Abfrage stellen | [Speicher §2.1](https://apogee.gweb3networks.com/docs/auditors/spec/memory#s2-1) |
| `x0` liest und schreibt 0 | das x0-Gadget und die Rückschreibungen | [Speicher §2.4](https://apogee.gweb3networks.com/docs/auditors/spec/memory#s2-4) |
| Register- und RAM-Werte sind Wörter | jeder Registerschreibzugriff auf seiner eigenen Zeile beschränkt; jeder RAM-Schreibzugriff einer Ausführungsfamilie ein Wort; Anfangswerte sind Wörter, außer Hilfsdaten, auf die sich keine Familie verlässt | [memory-ops §5](https://apogee.gweb3networks.com/docs/auditors/spec/memory-ops#s5) |
| Eine Padding-Zeile fügt kein Speicherereignis hinzu | jede Maske einer Padding-Zeile ist 0, also sind ihre Blätter 1 | [Speicher §2.3](https://apogee.gweb3networks.com/docs/auditors/spec/memory#s2-3), [GKR §4.3](https://apogee.gweb3networks.com/docs/auditors/spec/gkr#s4-3) |

## Speicher und Reihenfolge

| Behauptung | Argument | Spezifikation |
| --- | --- | --- |
| Jeder Lesezugriff liefert den letzten Schreibzugriff | eine Lese-/Schreib-Multimenge über alle Shards, einmal gegen die Randwerte von Registern und pc abgeglichen | [Speicher §4](https://apogee.gweb3networks.com/docs/auditors/spec/memory#s4), [§9](https://apogee.gweb3networks.com/docs/auditors/spec/memory#s9) |
| Ein Lesezugriff folgt strikt auf den Schreibzugriff, den er konsumiert | der Zeitstempelabstand jeder Abfrage besteht aus zwei `TIMESTAMP`-Chunks zu je 19 Bit | [Speicher §2.4](https://apogee.gweb3networks.com/docs/auditors/spec/memory#s2-4), [§7](https://apogee.gweb3networks.com/docs/auditors/spec/memory#s7) |
| Jede Adresse hat genau einen Anfangswert | die Fensterregeln: eine Höhe, disjunkte Fenster, je ein Shard für jedes der festen Fenster | [Speicher §3.5](https://apogee.gweb3networks.com/docs/auditors/spec/memory#s3-5), [§9](https://apogee.gweb3networks.com/docs/auditors/spec/memory#s9) |
| Die Multimenge kann sich nicht über eine Schleife schließen | Zeitstempel sind ganze Zahlen auf beschränkten Pfaden: Eine Schleife bräuchte mehr als `2^215` Kanten | [Speicher §4.2](https://apogee.gweb3networks.com/docs/auditors/spec/memory#s4-2) |
| Die Zeilen bilden einen einzigen Pfad vom Einsprung zum Exit, in Programmreihenfolge | der pc ist eine Speicherzelle, die mindestens vier Zeitstempel nach ihrem Lesen geschrieben wird | [Speicher §5](https://apogee.gweb3networks.com/docs/auditors/spec/memory#s5), [§9](https://apogee.gweb3networks.com/docs/auditors/spec/memory#s9) |
| Die Ausführung endet an der Exit-Zeile | `HALT_PC = 1` ist ungerade; nur die Exit-Zeile schreibt es; `JUMP_BRANCH_SLT` prüft per Range-Check, dass sein `next_pc` gerade ist | [Speicher §5](https://apogee.gweb3networks.com/docs/auditors/spec/memory#s5), [jump-branch-slt §5](https://apogee.gweb3networks.com/docs/auditors/spec/jump-branch-slt#s5), [add-sub §4](https://apogee.gweb3networks.com/docs/auditors/spec/add-sub#s4) |
| Das Zeitfenster eines Shards trägt nichts bei | Zeitfenster werden nur auf ihre Form geprüft; die Reihenfolge ergibt sich allein aus der Multimenge | [Beweis §8](https://apogee.gweb3networks.com/docs/auditors/spec/proof#s8) |

## Werte und Lookups

| Behauptung | Argument | Spezifikation |
| --- | --- | --- |
| Jedes per Selektor geschaltete Tupel ist eine Zeile seiner Tabelle | eine LogUp-Identität pro Kanal, summiert über einen Bruchbaum im GKR-Durchlauf; Zähler an der Wurzel 0, Nenner ungleich null | [Lookup §1](https://apogee.gweb3networks.com/docs/auditors/spec/lookup#s1), [§6](https://apogee.gweb3networks.com/docs/auditors/spec/lookup#s6), [§8](https://apogee.gweb3networks.com/docs/auditors/spec/lookup#s8) |
| Selektoren sind boolesch | der Selektor jedes Lookups wird durch ein Constraint-Gate der Liste 0 auf `s − s²` gehalten | [Lookup §2](https://apogee.gweb3networks.com/docs/auditors/spec/lookup#s2) |
| Ein Lookup antwortet aus seiner eigenen Teiltabelle | eine Breite pro Kanal, disjunkte Schlüsselbereiche mit dem Offset `+1` und die Schranke jeder Familie für ihren Schlüssel | [Lookup §4](https://apogee.gweb3networks.com/docs/auditors/spec/lookup#s4), [§9](https://apogee.gweb3networks.com/docs/auditors/spec/lookup#s9), [§11](https://apogee.gweb3networks.com/docs/auditors/spec/lookup#s11) |
| Die Tabellen sind die beabsichtigten | virtuelle Tabellen sind die geschlossenen Formen des Verifiers; die generische Tabelle ist durch den SRS-Digest gebunden, die dekodierten Tabellen durch die Identität | [Lookup §3](https://apogee.gweb3networks.com/docs/auditors/spec/lookup#s3), [§12](https://apogee.gweb3networks.com/docs/auditors/spec/lookup#s12) |
| Jede deklarierte Verpflichtung wird erfüllt | die Erfüllungsregel beim Zusammensetzen und bei jedem Laden eines Schlüssels | [Lookup §11](https://apogee.gweb3networks.com/docs/auditors/spec/lookup#s11) |

## Öffentliche Werte

| Behauptung | Argument | Spezifikation |
| --- | --- | --- |
| Das Eingabefenster enthielt die Eingabe der Aussage | die Anfangsspalte von `PUBLIC_INPUT` stimmt an einem zufälligen Punkt mit den Wörtern der Eingabe überein, nachdem G7 die Bytes festgelegt hat | [Öffentliche Werte §5](https://apogee.gweb3networks.com/docs/auditors/spec/public-values#s5) |
| Das Journal ist das, was die Store-Befehle des Gastprogramms (Guest) hinterlassen haben | die Endspalte von `PUBLIC_OUTPUT` stimmt mit den Wörtern des Journals überein; das Fenster hat keine Anfangsspalte, die ein Prover füllen könnte | [Öffentliche Werte §5](https://apogee.gweb3networks.com/docs/auditors/spec/public-values#s5) |
| Der Exit-Status ist der Endwert von `x10` | die Exit-Zeile schreibt das gelesene `a0` zurück; der Verifier gleicht `v_10` mit dem Status der Aussage ab | [add-sub §4](https://apogee.gweb3networks.com/docs/auditors/spec/add-sub#s4), [Speicher §4.1](https://apogee.gweb3networks.com/docs/auditors/spec/memory#s4-1), [Beweis §6](https://apogee.gweb3networks.com/docs/auditors/spec/proof#s6) |

## Delegationen

| Behauptung | Argument | Spezifikation |
| --- | --- | --- |
| Jede Anfrage wird genau einmal ausgeführt | der Anker: Anfragen und Aufrufe paaren sich eins zu eins über die Multimenge im eigenen Raum des Typs | [Delegation §5](https://apogee.gweb3networks.com/docs/auditors/spec/delegation#s5) |
| Ein Aufruf berechnet seine Funktion | das Soundness-Argument jedes Schaltkreises, einschließlich Frame und Kanonizitätsketten | [Delegationsschaltkreise §2–§7](https://apogee.gweb3networks.com/docs/auditors/spec/delegation-circuits#s2) |
| Eine Operation aus mehreren Aufrufen ist die Komposition ihrer Schritte | RAM-Glue: Jeder Schritt liest die Schreibzugriffe des vorherigen Schritts auf einer einzigen Speicherhistorie; die Reihenfolge bestimmt der aufrufende Code | [Delegationsschaltkreise §1](https://apogee.gweb3networks.com/docs/auditors/spec/delegation-circuits#s1) |

## Das Beweissystem

| Behauptung | Argument | Spezifikation |
| --- | --- | --- |
| Die Ausgaben eines Shards sind sein Schaltkreis, ausgewertet auf seinen committeten Spalten | der GKR-Rückwärtsdurchlauf, jede Challenge gezogen nach dem, was sie schützt | [GKR §5.4](https://apogee.gweb3networks.com/docs/auditors/spec/gkr#s5-4) |
| Die behaupteten Spaltenwerte sind die der committeten Polynome | eine gebündelte Mercury-Öffnung am Punkt des Durchlaufs | [Mercury §5](https://apogee.gweb3networks.com/docs/auditors/spec/mercury#s5), [§7](https://apogee.gweb3networks.com/docs/auditors/spec/mercury#s7) |
| Eine Aussage wird nur durch alle ihre Shards verifiziert | Exaktheit der Shard-Menge beim Dekodieren und in `verify_block`; der Abgleich liest die Wurzeln jedes Shards | [Beweis §1.3](https://apogee.gweb3networks.com/docs/auditors/spec/proof#s1-3), [§6](https://apogee.gweb3networks.com/docs/auditors/spec/proof#s6) |
| Challenges folgen auf jedes Commitment, das sie schützen | das globale Transkript G1–G11 und das Shard-Transkript S1–S6 | [Beweis §2](https://apogee.gweb3networks.com/docs/auditors/spec/proof#s2), [§4](https://apogee.gweb3networks.com/docs/auditors/spec/proof#s4), [Transkript §3](https://apogee.gweb3networks.com/docs/auditors/spec/transcript#s3) |
| Das Setup ist das der Zeremonie | der SRS-Digest, vom Verifier mit dem der Zeremonie verglichen | [Beweis §3](https://apogee.gweb3networks.com/docs/auditors/spec/proof#s3), [SRS §3](https://apogee.gweb3networks.com/docs/auditors/spec/srs#s3) |

## Rekursion und der Contract

| Behauptung | Argument | Spezifikation |
| --- | --- | --- |
| Ein Knoten hat genau die Prüfungen des Basis-Verifiers ausgeführt | die Prüfungen sind in Tapes im Image des Knotenprogramms kompiliert, das durch die Identität des Knotenprogramms gebunden ist | [Rekursion §7](https://apogee.gweb3networks.com/docs/auditors/spec/recursion#s7), [§8.1](https://apogee.gweb3networks.com/docs/auditors/spec/recursion#s8-1) |
| Der Baum deckt eine einzige Basisaussage ab, jeden Shard, in Reihenfolge | die Transkriptkette über die Knoten hinweg, benachbarte Shard-Bereiche und die Prüfungen jedes Knotens an seinen Kindern | [Rekursion §8.1](https://apogee.gweb3networks.com/docs/auditors/spec/recursion#s8-1), [§8.2](https://apogee.gweb3networks.com/docs/auditors/spec/recursion#s8-2) |
| Jede aufgeschobene Öffnung gilt | jede unter Gewichten gefaltet, die nach allem gezogen werden, was sie gewichten, und durch ein einziges Pairing im Contract eingelöst | [Rekursion §8.3](https://apogee.gweb3networks.com/docs/auditors/spec/recursion#s8-3), [Mercury §6](https://apogee.gweb3networks.com/docs/auditors/spec/mercury#s6) |
| Der Decider bindet, was der Contract hält | gebundene Wires, committet vor ihrer Challenge; der Schaltkreis bindet das Journal an den gesamten Basisbereich | [Rekursion §9](https://apogee.gweb3networks.com/docs/auditors/spec/recursion#s9) |
| Der Decider-Schlüssel hat keine bekannte Falltür | eine zweiphasige Zeremonie mit einem ehrlichen Beitragenden pro Runde, Runden in Reihenfolge | [Rekursion §9](https://apogee.gweb3networks.com/docs/auditors/spec/recursion#s9), [SRS §7](https://apogee.gweb3networks.com/docs/auditors/spec/srs#s7) |

## Bewusst nicht behauptet

- **Irgendetwas über Hilfsdaten.** Hilfsdaten sind bewusst an nichts gebunden; ein Gastprogramm prüft sie.
- **Zero-Knowledge.** Nichts wird verblindet.
- **Fehlschlagsemantik von `sc.w`.** `sc.w` gelingt immer; ein Programm, das sich auf sein Fehlschlagen verlässt, liegt außerhalb der Behauptung.
- **Traps.** Ein Lauf, der in einen Trap läuft, hat überhaupt keinen Beweis.
- **Dass der Prover korrekt ist.** Dem Prover wird nicht vertraut; nur die Crates des Verifiers tragen die Soundness.
- **Dass eine Zeremoniedatei die der Zeremonie ist**, oder dass das `τ` eines Schlüssels unbekannt ist, ohne den eigenen Vergleich des SRS-Digests durch den Verifier.