# Carte de solidité

> Chaque affirmation que fait une preuve vérifiée, l’argument qui la porte, et les sections exactes de la spécification où cet argument est énoncé et justifié.

Un bloc vérifié établit une seule phrase : *le programme de cette identité, lancé à son pc d’entrée sur son image, avec cette entrée publique et certaines données auxiliaires (advice), s’exécute instruction par instruction jusqu’à `EXIT` avec ce statut, après avoir écrit ce journal.* Cette page décompose cette phrase en les affirmations qui la constituent et mène chacune jusqu’à l’argument qui la prouve.

## Le programme

| Affirmation | Argument | Spécification |
| --- | --- | --- |
| La clé décrit le programme enregistré | le chargement d’une clé recalcule l’identité à partir de sa propre configuration, de son pc d’entrée et de ses engagements de mise en place; le vérificateur la compare à sa propre copie | [preuve §7.2](https://apogee.gweb3networks.com/docs/auditors/spec/proof#s7-2), [programme §8](https://apogee.gweb3networks.com/docs/auditors/spec/program#s8) |
| Les tables que lit une preuve sont celles que l’identité engage | l’ouverture groupée de chaque shard prend ses engagements de mise en place dans la clé | [preuve §5](https://apogee.gweb3networks.com/docs/auditors/spec/proof#s5) |
| Chaque ligne exécutée est l’instruction du programme à son pc | le lookup du décodeur, indexé par la lecture du pc propre à la ligne, dans une table dont les lignes actives sont one-hot et dont les lignes de remplissage valent `−1` | [lookup §10](https://apogee.gweb3networks.com/docs/auditors/spec/lookup#s10), [programme §5](https://apogee.gweb3networks.com/docs/auditors/spec/program#s5), [§6](https://apogee.gweb3networks.com/docs/auditors/spec/program#s6) |
| La mémoire part de l’image du programme | la colonne d’initialisation de la famille `INIT_TEARDOWN` est une colonne de mise en place que l’identité engage; aucun octet issu du fichier ne se trouve hors de la fenêtre 0 | [mémoire §6.2](https://apogee.gweb3networks.com/docs/auditors/spec/memory#s6-2), [§3.4](https://apogee.gweb3networks.com/docs/auditors/spec/memory#s3-4) |
| L’exécution commence au pc d’entrée | le tuple initial du pc utilise le pc d’entrée de la clé, que l’identité lie | [mémoire §4.2](https://apogee.gweb3networks.com/docs/auditors/spec/memory#s4-2), [§6.2](https://apogee.gweb3networks.com/docs/auditors/spec/memory#s6-2) |
| Les circuits sont les bons | les circuits d’une clé doivent être identiques au registre du vérificateur à leurs hauteurs et satisfaire les lois, les règles de mémoire et la règle d’acquittement | [preuve §7.2](https://apogee.gweb3networks.com/docs/auditors/spec/proof#s7-2), [circuits §1](https://apogee.gweb3networks.com/docs/auditors/spec/circuits#s1), [gkr §4.2](https://apogee.gweb3networks.com/docs/auditors/spec/gkr#s4-2) |

## Chaque ligne

| Affirmation | Argument | Spécification |
| --- | --- | --- |
| Une ligne obéit à son instruction | les portes de contrainte de la famille, nulles sur chaque ligne; l’argument de solidité (*soundness*) de chaque famille | [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) |
| Une ligne effectue exactement les requêtes de son instruction | chaque masque fixé à `m_pc` multiplié par les types qui effectuent cette requête | [mémoire §2.1](https://apogee.gweb3networks.com/docs/auditors/spec/memory#s2-1) |
| `x0` lit et écrit 0 | le gadget x0 et les écritures en retour | [mémoire §2.4](https://apogee.gweb3networks.com/docs/auditors/spec/memory#s2-4) |
| Les valeurs des registres et de la RAM sont des mots | chaque écriture de registre est bornée sur sa propre ligne; chaque écriture en RAM d’une famille d’exécution est un mot; les valeurs initiales sont des mots, sauf les données auxiliaires, sur lesquelles aucune famille ne s’appuie | [memory-ops §5](https://apogee.gweb3networks.com/docs/auditors/spec/memory-ops#s5) |
| Une ligne de remplissage n’ajoute aucun événement mémoire | chaque masque d’une ligne de remplissage vaut 0, donc ses feuilles valent 1 | [mémoire §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) |

## Mémoire et ordre

| Affirmation | Argument | Spécification |
| --- | --- | --- |
| Chaque lecture renvoie la dernière écriture | un seul multiensemble lecture/écriture sur tous les shards, rapproché une seule fois avec la frontière des registres et du pc | [mémoire §4](https://apogee.gweb3networks.com/docs/auditors/spec/memory#s4), [§9](https://apogee.gweb3networks.com/docs/auditors/spec/memory#s9) |
| Une lecture suit strictement l’écriture qu’elle consomme | l’écart d’horodatage de chaque requête est formé de deux fragments `TIMESTAMP` de 19 bits | [mémoire §2.4](https://apogee.gweb3networks.com/docs/auditors/spec/memory#s2-4), [§7](https://apogee.gweb3networks.com/docs/auditors/spec/memory#s7) |
| Chaque adresse a exactement une valeur initiale | les règles des fenêtres : une seule hauteur, des fenêtres disjointes, un seul shard pour chacune des fenêtres fixes | [mémoire §3.5](https://apogee.gweb3networks.com/docs/auditors/spec/memory#s3-5), [§9](https://apogee.gweb3networks.com/docs/auditors/spec/memory#s9) |
| Le multiensemble ne peut pas se refermer par une boucle | les horodatages sont des entiers sur des chemins bornés : une boucle nécessiterait plus de `2^215` arêtes | [mémoire §4.2](https://apogee.gweb3networks.com/docs/auditors/spec/memory#s4-2) |
| Les lignes forment un seul chemin de l’entrée à la sortie, dans l’ordre du programme | le pc est une cellule mémoire écrite au moins quatre horodatages après sa lecture | [mémoire §5](https://apogee.gweb3networks.com/docs/auditors/spec/memory#s5), [§9](https://apogee.gweb3networks.com/docs/auditors/spec/memory#s9) |
| L’exécution se termine à la ligne de sortie | `HALT_PC = 1` est impair; seule la ligne de sortie l’écrit; `JUMP_BRANCH_SLT` vérifie par intervalle que son `next_pc` est pair | [mémoire §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) |
| La fenêtre temporelle d’un shard n’ajoute rien | seule la forme des fenêtres temporelles est vérifiée; l’ordre provient du seul multiensemble | [preuve §8](https://apogee.gweb3networks.com/docs/auditors/spec/proof#s8) |

## Valeurs et lookups

| Affirmation | Argument | Spécification |
| --- | --- | --- |
| Chaque tuple sous sélecteur est une ligne de sa table | une identité LogUp par canal, sommée par un arbre de fractions dans la passe GKR; numérateur de la racine égal à 0 et dénominateur non nul | [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) |
| Les sélecteurs sont booléens | le sélecteur de chaque lookup est astreint à `s − s²` par une porte de contrainte de la liste 0 | [lookup §2](https://apogee.gweb3networks.com/docs/auditors/spec/lookup#s2) |
| Un lookup répond à partir de sa propre sous-table | une seule largeur par canal, des plages de clés disjointes avec le décalage `+1`, et la borne que chaque famille impose à sa clé | [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) |
| Les tables sont celles prévues | les tables virtuelles sont les formes closes du vérificateur; la table générique est liée par le condensé SRS; les tables décodées, par l’identité | [lookup §3](https://apogee.gweb3networks.com/docs/auditors/spec/lookup#s3), [§12](https://apogee.gweb3networks.com/docs/auditors/spec/lookup#s12) |
| Chaque obligation déclarée est acquittée | la règle d’acquittement, à l’assemblage et à chaque chargement de clé | [lookup §11](https://apogee.gweb3networks.com/docs/auditors/spec/lookup#s11) |

## Valeurs publiques

| Affirmation | Argument | Spécification |
| --- | --- | --- |
| La fenêtre d’entrée contenait l’entrée de l’énoncé | la colonne initiale de `PUBLIC_INPUT` est égale aux mots de l’entrée en un point aléatoire, après que G7 a fixé les octets | [valeurs publiques §5](https://apogee.gweb3networks.com/docs/auditors/spec/public-values#s5) |
| Le journal est ce qu’ont laissé les écritures du programme invité | la colonne finale de `PUBLIC_OUTPUT` est égale aux mots du journal; la fenêtre n’a pas de colonne initiale qu’un prouveur pourrait remplir | [valeurs publiques §5](https://apogee.gweb3networks.com/docs/auditors/spec/public-values#s5) |
| Le statut de sortie est la valeur finale de `x10` | la ligne de sortie réécrit le `a0` qu’elle a lu; le vérificateur astreint `v_10` au statut de l’énoncé | [add-sub §4](https://apogee.gweb3networks.com/docs/auditors/spec/add-sub#s4), [mémoire §4.1](https://apogee.gweb3networks.com/docs/auditors/spec/memory#s4-1), [preuve §6](https://apogee.gweb3networks.com/docs/auditors/spec/proof#s6) |

## Délégations

| Affirmation | Argument | Spécification |
| --- | --- | --- |
| Chaque demande est exécutée exactement une fois | l’ancre : demandes et invocations s’apparient une à une par le multiensemble, dans l’espace propre au type | [délégation §5](https://apogee.gweb3networks.com/docs/auditors/spec/delegation#s5) |
| Une invocation calcule sa fonction | l’argument de solidité de chaque circuit, cadre et chaînes de canonicité compris | [circuits de délégation §2–§7](https://apogee.gweb3networks.com/docs/auditors/spec/delegation-circuits#s2) |
| Une opération en plusieurs appels est la composition de ses étapes | le liant RAM : chaque étape lit les écritures de l’étape précédente sur un même historique mémoire; l’ordre est celui du code appelant | [circuits de délégation §1](https://apogee.gweb3networks.com/docs/auditors/spec/delegation-circuits#s1) |

## Le système de preuve

| Affirmation | Argument | Spécification |
| --- | --- | --- |
| Les sorties d’un shard sont son circuit évalué sur ses colonnes engagées | la passe arrière GKR, chaque défi étant tiré après ce qu’il protège | [gkr §5.4](https://apogee.gweb3networks.com/docs/auditors/spec/gkr#s5-4) |
| Les valeurs de colonnes annoncées sont celles des polynômes engagés | une seule ouverture Mercury groupée au point de la passe | [mercury §5](https://apogee.gweb3networks.com/docs/auditors/spec/mercury#s5), [§7](https://apogee.gweb3networks.com/docs/auditors/spec/mercury#s7) |
| Un énoncé n’est vérifié que par l’ensemble de ses shards | l’exactitude de l’ensemble des shards au décodage et dans `verify_block`; le rapprochement lit les racines de chaque shard | [preuve §1.3](https://apogee.gweb3networks.com/docs/auditors/spec/proof#s1-3), [§6](https://apogee.gweb3networks.com/docs/auditors/spec/proof#s6) |
| Les défis suivent chaque engagement qu’ils protègent | la transcription globale G1–G11 et la transcription du shard S1–S6 | [preuve §2](https://apogee.gweb3networks.com/docs/auditors/spec/proof#s2), [§4](https://apogee.gweb3networks.com/docs/auditors/spec/proof#s4), [transcription §3](https://apogee.gweb3networks.com/docs/auditors/spec/transcript#s3) |
| La mise en place est celle de la cérémonie | le condensé SRS, que le vérificateur compare à celui de la cérémonie | [preuve §3](https://apogee.gweb3networks.com/docs/auditors/spec/proof#s3), [srs §3](https://apogee.gweb3networks.com/docs/auditors/spec/srs#s3) |

## La récursion et le contrat

| Affirmation | Argument | Spécification |
| --- | --- | --- |
| Un nœud a exécuté exactement les vérifications du vérificateur de base | les vérifications sont compilées en bandes dans l’image du programme du nœud, que son identité lie | [récursion §7](https://apogee.gweb3networks.com/docs/auditors/spec/recursion#s7), [§8.1](https://apogee.gweb3networks.com/docs/auditors/spec/recursion#s8-1) |
| L’arbre couvre un seul énoncé de base, chaque shard, dans l’ordre | le chaînage des transcriptions entre les nœuds, des plages de shards adjacentes, et les vérifications que chaque nœud effectue sur ses enfants | [récursion §8.1](https://apogee.gweb3networks.com/docs/auditors/spec/recursion#s8-1), [§8.2](https://apogee.gweb3networks.com/docs/auditors/spec/recursion#s8-2) |
| Chaque ouverture différée tient | chacune repliée sous des poids tirés après tout ce qu’ils pondèrent, et acquittée par un seul couplage dans le contrat | [récursion §8.3](https://apogee.gweb3networks.com/docs/auditors/spec/recursion#s8-3), [mercury §6](https://apogee.gweb3networks.com/docs/auditors/spec/mercury#s6) |
| Le décideur lie ce que détient le contrat | des fils liés engagés avant leur défi; le circuit astreint le journal à toute la plage de base | [récursion §9](https://apogee.gweb3networks.com/docs/auditors/spec/recursion#s9) |
| La clé du décideur n’a pas de trappe connue | une cérémonie en deux phases avec un contributeur honnête par tour, les tours se succédant dans l’ordre | [récursion §9](https://apogee.gweb3networks.com/docs/auditors/spec/recursion#s9), [srs §7](https://apogee.gweb3networks.com/docs/auditors/spec/srs#s7) |

## Délibérément non affirmé

- **Quoi que ce soit au sujet des données auxiliaires.** Les données auxiliaires ne sont liées à rien, par conception; un programme invité les vérifie.
- **La divulgation nulle de connaissance.** Aucun aveuglement n’est appliqué.
- **La sémantique d’échec de `sc.w`.** `sc.w` réussit toujours; un programme qui compte sur son échec sort du cadre de l’affirmation.
- **Les déroutements (*traps*).** Une exécution qui déclenche un déroutement n’a aucune preuve.
- **Que le prouveur est correct.** Le prouveur n’est pas digne de confiance; seules les crates du vérificateur portent la solidité.
- **Qu’un fichier de cérémonie est bien celui de la cérémonie**, ni que le `τ` d’une clé est inconnu, sans la comparaison du condensé SRS effectuée par le vérificateur lui-même.