# Die Implementierung prüfen > Wie der Code gegen etwas anderes als sich selbst geprüft wird. Das unabhängige Orakel jeder Schicht, die zweite Implementierung der Schaltkreisregeln, die Manipulations-Zwillinge, die belegen, dass Fälschungen zurückgewiesen werden, und was keine Prüfung abdeckt. Keine Komponente von Apogee wird gegen eine zweite Implementierung des gesamten Systems geprüft. Stattdessen hat jede Schicht ein eigenes Orakel, so gewählt, dass die Prüfung so wenig Code wie möglich mit dem Geprüften teilt. ## Jede Schicht und ihr Orakel | Schicht | Geprüft gegen | | --- | --- | | Körper, Kurve, Pairing, MSM | Known-Answer-Vektoren, erzeugt mit arkworks, das die Tests auch live ausführen; die Tests leiten jede arithmetische Konstante neu her, die die Crates lesen | | Poseidon2 und das Transkript | `tools/transcript-ref`: Poseidon2 aus Plonky3 mit den Rundenkonstanten aus zkhash und eine Umsetzung der Spezifikation, die neben dem Duplex-Challenger von Plonky3 läuft und bei jedem Squeeze übereinstimmt | | Der Decoder | alle `2^30` 32-Bit-Wörter mit den niedrigen Bits `11`, gegen die aus den Tabellen der ISA abgeleitete Anzahl akzeptierter Wörter und gegen einen unabhängigen Encoder; `llvm-objdump` über die eingecheckten Gastprogramme (Guests) | | RVC-Expansion | der eigene Encoder von LLVM, über ein Gastprogramm, das sowohl komprimiert als auch unkomprimiert assembliert wurde | | Schaltkreise als Daten | `checker`: die vier Gesetze, die Lookup-Regeln und der Padding-Vertrag, neu implementiert ohne den Code von `constraints`; gemeinsam ist nur der Gate-Kernel | | Die Gates jeder Familie | Zeilen-Suiten, die Zeilen mit Rusts eigener Ganzzahlarithmetik bauen und über den Checker auswerten; die arithmetischen Kerne erschöpfend bei reduzierten Wortbreiten | | Die Speicher- und Lookup-Argumente | native Evaluatoren in `checker`, angewandt auf ausgeführte Traces | | Der Executor | die Selbstprüfung seines eigenen Trace und die obigen Argumente; es gibt keinen zweiten Executor | | Das revm-Gastprogramm | natives revm, gebaut aus ungepatchten Upstream-Crates | | Der zustandslose Validator | eine eingecheckte Teilmenge von `tests-zkevm` v21.0.1 nativ in der CI; das gesamte Release nativ und die Teilmenge über das Binary des Gastprogramms von Hand; `tools/stateless-ref` für die Kodierung der Eingabe | | Der Decider | der Beweis nativ geprüft und der Contract in revm ausgeführt | ## Erschöpfende Prüfungen bei kleinen Breiten Mehrere arithmetische Kerne sind mit ihrer Wortbreite als Parameter geschrieben, sodass sich die Kodierung über jede Eingabe bei einer Breite prüfen lässt, die klein genug zum Aufzählen ist: - das Vergleichs-Gadget bei 6 Bit: Für jedes Operandenpaar, mit und ohne Vorzeichen, findet die Prüfung genau ein `(lt, gap)`, nämlich das der ISA; - die Arithmetik von `MUL_DIV` bei 4 Bit: Für jeden Dividenden und Divisor und jede Divisionsart ist genau ein `(q, r)` zulässig, nämlich das von RV32M; - das Einsetzen (Splice) von `MEM_SUBWORD` bei einem 4-Bit-Wort: Für jedes Wort, jeden Offset und jede Breite ist genau ein `(high, sub, low)` zulässig. ## Die Schaltkreisregeln, zweimal `CircuitArtifact::validate` und die Konstruktionsregeln für Speicher und Lookups laufen überall dort, wo ein Artefakt gebaut oder ein Schlüssel geladen wird. `crates/checker` setzt dieselben Regeln ein zweites Mal mit eigenem Code durch, ruft `validate` nie auf und wertet Gates ausschließlich über `gkr_verify::eval_gate` aus, den einen Kernel, den beide Seiten als semantische Autorität behandeln. Seine Validatoren prüfen die Gesetze durch Auswertung an Stichprobenpunkten, während `validate` normalisierte Expansionen vergleicht, berechnen die Summe jedes Kanals Zeile für Zeile statt über einen Baum neu und benennen jedes Tupel, das in keiner Tabellenzeile vorkommt, und bauen die Speicherspalten einer Ausführungsfamilie aus dem Ereignislog statt aus den Zeilen eines Shards neu auf. ```sh cargo run -p checker -- laws # Laws 1–4, then the lookup rules cargo run -p checker -- padding # the padding contract cargo run -p checker -- dump # the circuit, readably ``` ## Manipulations-Zwillinge Ein **Manipulations-Zwilling** ist eine Fälschung, die genau so bewiesen wird, wie ein ehrlicher Prover sie beweisen würde. Die Manipulations-Suite (`checker::TamperHarness`) beweist eine Aussage mit veränderten Witness-Zellen oder Randskalaren erneut: Die Multiplizitäten jedes Kanals werden neu gezählt, veränderte Speicherspalten in einer frischen globalen Commit-Phase neu committet, jeder Shard neu bewiesen. Dann verifiziert sie einen Shard oder den Block und prüft per Assertion die Klasse der Zurückweisung, `Constraint`, `Lookup` mit seinem Kanal oder `MemoryArgument`, oder sie stellt sicher, dass eine Änderung, die nichts bricht, verifiziert wird. Die Zwillinge beruhen darauf, dass der Prover nichts prüft, und das ist so gewollt: Ein gefälschter Witness erhält den besten Beweis, den ein ehrlicher Prover davon erstellen könnte, und der Verifier muss ihn in der erwarteten Klasse zurückweisen. Die Suite enthält auch die Fälschungen des Delegationsankers, und am Mainnet-Mini-Block zeigt sie die andere Seite der Regel für Hilfsdaten (Advice): Eine verfälschte Zelle der Hilfsdaten wird vom Speicherargument zurückgewiesen, eine konsistent verfälschte dagegen wird verifiziert, weil Hilfsdaten an nichts gebunden sind. ```sh cargo test --release -p checker --test tamper -- --include-ignored --test-threads=1 ``` ## Fixtures, die sich neu erzeugen lassen `kat-gen` schreibt jeden eingecheckten Known-Answer-Vektor, jedes Listing, jedes Schaltkreis-Artefakt und jede Identität, jeweils mit zugehörigem SHA-256, den die einlesenden Tests fest verankern. Die CI erzeugt die Standardgruppen und beide Referenzorakel neu und schlägt bei jeder Abweichung in den Vektorverzeichnissen fehl: ```sh cargo run -p kat-gen && git diff --exit-code ``` Ein ELF eines Gastprogramms ist nicht maschinenübergreifend reproduzierbar, weil rustc absolute Pfade in die Strings für Panic-Locations einbettet; zwei saubere Builds auf derselben Maschine stimmen überein. Deshalb werden die ELFs der Gastprogramme von Hand auf einer Maschine neu erzeugt, und die CI erzeugt nur neu, was sich von ihnen ableitet. ## Was keine Prüfung abdeckt - **Es gibt keinen zweiten Executor.** Der Emulator wird an einer Neuformulierung seiner eigenen Frame-Tabelle und an den Speicher- und Lookup-Argumenten gemessen, nicht an einer unabhängigen RISC-V-Implementierung, und kein Executor hier nimmt den Software-Fallback eines Delegations-Shims. - **Die Konstruktionsregeln, die der Checker nicht wiederholt**: Die Konstruktionsregeln für den Speicher, die Copower-Regel und die übrigen Konstruktionsregeln von `validate`, darunter die Gradobergrenze, werden nur einmal durchgesetzt. - **Der Prover wird nicht auf Korrektheit geprüft**, nur auf Vollständigkeit, und zwar über die Suiten, die echte Shards beweisen und außerhalb der CI laufen, weil jede Dutzende GiB braucht. - **Zustandslose Eingaben der Osaka-Familie haben kein End-to-End-Orakel.** Das Release befüllt nur Amsterdam; das Electra/Fulu-Layout wird an `eth-act/ere-guests` gemessen, die Header-Regeln an zwei Mainnet-Blöcken.