# Vérifier l’implémentation

> Comment le code est vérifié par rapport à autre chose que lui-même. L’oracle indépendant de chaque couche, la seconde implémentation des règles des circuits, les jumeaux falsifiés qui prouvent que les contrefaçons sont refusées, et ce qu’aucune vérification ne couvre.

Aucun composant d’Apogee n’est vérifié par rapport à une seconde implémentation du système entier. Chaque couche a plutôt son propre oracle, choisi pour que la vérification partage le moins de code possible avec ce qu’elle vérifie.

## Chaque couche et son oracle

| Couche | Vérifiée par rapport à |
| --- | --- |
| Corps, courbe, couplage, MSM | des vecteurs à réponse connue générés à partir d’arkworks, que les tests exécutent aussi en direct; les tests redérivent chaque constante arithmétique que lisent les crates |
| Poseidon2 et la transcription | `tools/transcript-ref` : le Poseidon2 de Plonky3 paramétré avec les constantes de tour de zkhash, et une traduction directe de la spécification exécutée à côté du *challenger* duplex de Plonky3, en accord à chaque essorage |
| Le décodeur | les `2^30` mots de 32 bits dont les bits de poids faible valent `11`, par rapport à des décomptes d’acceptation dérivés des tables de l’ISA et à un encodeur indépendant; `llvm-objdump` sur les programmes invités versionnés |
| Le développement RVC | l’encodeur même de LLVM, sur un programme invité assemblé à la fois avec et sans compression |
| Les circuits sous forme de données | `checker` : les quatre lois, les règles de lookup et le contrat de remplissage réimplémentés sans le code de `constraints`, en ne partageant que le noyau des portes |
| Les portes de chaque famille | des suites par ligne qui construisent des lignes avec l’arithmétique entière de Rust et les évaluent avec le checker; les cœurs arithmétiques, de façon exhaustive, à des largeurs de mot réduites |
| Les arguments de mémoire et de lookup | des évaluateurs natifs dans `checker`, exécutés sur des traces d’exécutions réelles |
| L’exécuteur | l’autovérification de sa propre trace et les arguments ci-dessus; il n’y a pas de second exécuteur |
| Le programme invité revm | revm natif, compilé à partir des crates amont non corrigées |
| Le validateur sans état | un sous-ensemble versionné de `tests-zkevm` v21.0.1, en natif dans la CI; la version complète en natif et le sous-ensemble à travers le binaire invité, à la main; `tools/stateless-ref` pour l’encodage des entrées |
| Le décideur | la preuve vérifiée en natif, et le contrat exécuté dans revm |

## Vérifications exhaustives à petites largeurs

Plusieurs cœurs arithmétiques sont écrits avec leur largeur de mot comme paramètre, afin que l’encodage puisse être vérifié sur toutes les entrées à une largeur assez petite pour être énumérée :

- le gadget de comparaison à 6 bits, sur chaque paire d’opérandes, signée et non signée, qui trouve exactement un `(lt, gap)`, celui de l’ISA;
- l’arithmétique de `MUL_DIV` à 4 bits, sur chaque dividende, chaque diviseur et chaque type de division, qui admet exactement un `(q, r)`, celui de RV32M;
- l’insertion de `MEM_SUBWORD` sur un mot de 4 bits, qui admet exactement un `(high, sub, low)` pour chaque mot, chaque décalage et chaque largeur.

## Les règles des circuits, deux fois

`CircuitArtifact::validate` et les règles de construction de la mémoire et des lookups s’exécutent partout où un artefact est construit ou une clé est chargée. `crates/checker` applique les mêmes règles une seconde fois avec son propre code, sans jamais appeler `validate`, et n’évalue les portes qu’au moyen de `gkr_verify::eval_gate`, le seul noyau que les deux côtés tiennent pour l’autorité sémantique. Ses validateurs vérifient les lois par évaluation en des points échantillonnés là où `validate` compare des développements normalisés, recalculent la somme de chaque canal ligne par ligne plutôt que par un arbre et nomment tout tuple qu’aucune ligne de table ne contient, et reconstruisent les colonnes mémoire d’une famille d’exécution à partir du journal d’événements plutôt qu’à partir des lignes d’un shard.

```sh
cargo run -p checker -- laws <artifact>       # Laws 1–4, then the lookup rules
cargo run -p checker -- padding <artifact>    # the padding contract
cargo run -p checker -- dump <artifact>       # the circuit, readably
```

## Jumeaux falsifiés

Un **jumeau falsifié** est une contrefaçon prouvée exactement comme un prouveur honnête la prouverait. La suite de falsification (`checker::TamperHarness`) prouve de nouveau un énoncé dont des cellules du témoin ou des scalaires de frontière ont été modifiés : les multiplicités de chaque canal sont recomptées, les colonnes mémoire modifiées sont engagées de nouveau dans une nouvelle phase d’engagement global, chaque shard est prouvé de nouveau. Elle vérifie ensuite un shard ou le bloc et contrôle par assertion la classe du refus, `Constraint`, `Lookup` avec son canal, ou `MemoryArgument`, ou bien contrôle qu’une modification qui ne casse rien passe la vérification.

Les jumeaux reposent sur le fait que le prouveur ne vérifie rien, ce qui est voulu : un témoin contrefait obtient la meilleure preuve qu’un prouveur honnête pourrait en faire, et le vérificateur doit le refuser dans la classe attendue. La suite contient aussi les contrefaçons de l’ancre de délégation et, sur le mini-bloc du réseau principal, elle montre l’autre face de la règle des données auxiliaires (*advice*) : une cellule de données auxiliaires corrompue est refusée par l’argument de mémoire, et une cellule corrompue de façon cohérente passe la vérification, car les données auxiliaires ne sont liées à rien.

```sh
cargo test --release -p checker --test tamper -- --include-ignored --test-threads=1
```

## Des données de référence qui se régénèrent

`kat-gen` écrit chaque vecteur à réponse connue, listage, artefact de circuit et identité versionnés, chacun avec son SHA-256, que fixent les tests qui le lisent. La CI régénère les groupes par défaut et les deux oracles de référence, et échoue à la moindre différence dans les répertoires de vecteurs :

```sh
cargo run -p kat-gen && git diff --exit-code
```

Un ELF de programme invité n’est pas reproductible d’une machine à l’autre, car rustc incorpore des chemins absolus dans les chaînes de localisation des paniques; deux compilations propres sur une même machine concordent. Les ELF des programmes invités sont donc régénérés à la main sur une seule machine, et la CI ne régénère que ce qui en dérive.

## Ce qu’aucune vérification ne couvre

- **Il n’y a pas de second exécuteur.** L’émulateur est confronté à une reformulation de sa propre table de cadres et aux arguments de mémoire et de lookup, et non à une implémentation RISC-V indépendante, et aucun exécuteur ici n’emprunte le repli logiciel d’un shim de délégation.
- **Les règles de construction que le checker ne répète pas** : les règles de construction de la mémoire, la règle de copuissance, et les autres règles de construction de `validate`, dont le plafond de degré, ne sont appliquées qu’une fois.
- **La correction du prouveur n’est pas vérifiée**, seulement sa complétude, par les suites qui prouvent de vrais shards, lesquelles s’exécutent hors de la CI parce que chacune nécessite des dizaines de GiB.
- **Les entrées sans état de la famille Osaka n’ont pas d’oracle de bout en bout.** La version des tests ne remplit qu’Amsterdam; la disposition Electra/Fulu est confrontée à `eth-act/ere-guests`, et les règles d’en-tête, à deux blocs du réseau principal.