# Le moteur GKR

> Le moteur de preuve au centre d’Apogee. Pourquoi un circuit GKR en couches n’engage que ses entrées, comment une seule passe arrière de sumchecks ramène un circuit entier à un seul point, et ce que cela rapporte.

Chaque shard d’Apogee est prouvé de la même façon : par le circuit de sa famille, écrit sous forme d’empilement de couches, que le moteur GKR parcourt à rebours, des sorties du circuit jusqu’à ses colonnes engagées. Cette page explique pourquoi ce moteur occupe le centre du système, et pourquoi la famille de systèmes de preuve à laquelle il appartient est celle vers laquelle se déplace la frontière de la génération de preuves.

## L’idée

La façon classique de prouver un calcul consiste à le disposer sous forme de table, à engager chaque colonne, valeurs intermédiaires comprises, et à prouver qu’un ensemble de contraintes s’annule sur la table. Les engagements en sont la partie coûteuse : chaque colonne engagée coûte une multiplication multi-scalaire ou un arbre de Merkle, ainsi qu’une ouverture en chaque point qu’interroge l’argument de contraintes.

GKR, d’après Goldwasser, Kalai et Rothblum, change ce qui doit être engagé. Le calcul est un **circuit en couches**. Seule la couche inférieure, celle des entrées, est engagée. Chaque couche au-dessus est définie par des portes sur la couche du dessous, et le prouveur ne l’engage jamais. À la place, une affirmation sur la couche supérieure est ramenée par un sumcheck à une affirmation sur la couche située juste en dessous, puis à la suivante, jusqu’à ce que les affirmations aboutissent aux entrées engagées, toutes en un seul point aléatoire. Une seule ouverture les tranche toutes.

> [!NOTE]
> **Une analogie, pas un nom.** Un prouveur conventionnel est une fusée : il transporte jusqu’à destination chaque valeur intermédiaire qu’il produit, engagée, et paie le prix de cette masse. Le moteur GKR se comporte plutôt comme le moteur de distorsion de la science-fiction, qui déplace l’espace autour du vaisseau plutôt que le vaisseau lui-même. Ce qui voyage, c’est l’*affirmation*, descendue à travers le circuit couche par couche, tandis que les couches intermédiaires ne sont jamais transportées nulle part.

Ce que cela rapporte à une zkVM :

- **Les valeurs intermédiaires ne coûtent aucun engagement.** Un circuit de famille peut calculer des centaines de colonnes internes, des arbres de produits et des arbres de fractions, sans qu’aucun ne soit jamais engagé. Seules ses colonnes de trace le sont.
- **Un seul point d’ouverture par shard.** La passe arrière se termine avec une affirmation sur chaque colonne engagée, toutes au même point. Un shard a besoin d’exactement une ouverture groupée, de 704 octets, quel que soit son nombre de colonnes.
- **Le travail du prouveur est de l’arithmétique de corps.** Le sumcheck de chaque couche est linéaire en la taille de la couche, sur `Fr`, sans engagement, transformée ni hachage par couche.
- **Les arguments se composent à l’intérieur du circuit.** Les grands produits de l’argument de mémoire et les sommes LogUp des lookups ne sont que des couches supplémentaires du même circuit, réduites dans la même passe.

## Un circuit de famille, couche par couche

> Figure: Un circuit de famille. Le prouveur calcule chaque couche une fois, en montant (pointillés). La preuve descend : les sorties sont absorbées, puis chaque transition est un sumcheck qui transforme des affirmations sur une couche en affirmations sur la couche du dessous, jusqu’à ce qu’elles se rejoignent toutes en un seul point sur les colonnes engagées.

La couche inférieure est formée des colonnes engagées du shard, de trois sortes qui diffèrent par le moment où elles sont liées : **`M`**, les colonnes mémoire, engagées dans la transcription globale de l’énoncé avant qu’existe le moindre défi mémoire; **`W`**, les colonnes témoins, engagées dans la transcription propre au shard; et **`S`**, les colonnes de mise en place, liées par l’identité du programme ou par la cérémonie. À côté d’elles se trouvent les **tables virtuelles** : des formes closes comme l’indice de ligne ou l’intervalle de 16 bits, que le vérificateur évalue en n’importe quel point et qui ne sont jamais engagées.

Au-dessus de la couche 0, chaque circuit de famille a la même anatomie :

1. **La liste de portes 0** calcule, ligne par ligne, les feuilles mémoire (les tuples de lecture et d’écriture de chaque requête), les fractions de lookup (une paire `(numerator, denominator)` par lookup, plus celle de la table), et chaque **porte de contrainte** : les contraintes de la famille, chacune étant un polynôme qui doit s’annuler sur chaque ligne.
2. **Les listes ligne par ligne** combinent les feuilles sœurs : un arbre de produits multiplie des tuples, un arbre de fractions additionne des fractions sous la forme `(n_a·d_b + n_b·d_a, d_a·d_b)`, jusqu’à ce que chaque ligne ne contienne plus qu’un nœud par arbre.
3. **Les listes à réduction de moitié**, une par variable de la hauteur du shard, combinent les lignes deux à deux : la première moitié avec la seconde. Après `n` d’entre elles, le circuit atteint un sommet sans variables : la racine de lecture du shard, sa racine d’écriture, et le numérateur et le dénominateur finaux de chaque canal de lookup.

Un seul circuit prouve donc les contraintes de la famille, calcule sa contribution à l’argument de mémoire et somme ses lookups, en une seule passe. Chaque porte est de degré au plus 2 : chaque polynôme de tour de chaque sumcheck est donc cubique.

## La passe arrière

Le prouveur matérialise chaque couche une fois, en montant. La preuve descend ensuite, et l’ordonnancement de sa transcription est le même pour chaque circuit :

1. **Les sorties sont absorbées** en premier : le prouveur est ainsi engagé sur les racines avant qu’existe le moindre défi.
2. Pour chaque transition de la couche `k + 1` vers la couche `k`, un défi `λ` regroupe en une seule somme chaque affirmation sur la couche `k + 1`, ainsi que chaque porte de contrainte de la liste. Un **sumcheck** ramène cette somme à une évaluation en un point aléatoire `ρ`, à raison d’un message cubique par variable.
3. Le prouveur annonce les valeurs des colonnes de la couche `k` en `ρ`. Pour une liste à réduction de moitié, il annonce les deux enfants, et un défi supplémentaire `τ` les fusionne en une seule affirmation par colonne.
4. À la couche 0, chaque colonne engagée fait l’objet d’une seule affirmation, toutes au même point `u`.

L’unique ouverture Mercury du shard prouve ces affirmations par rapport aux engagements : ceux des colonnes mémoire, tirés de l’énoncé; ceux des colonnes témoins, tirés de la preuve du shard; ceux des colonnes de mise en place, tirés de la clé de vérification. Les tables virtuelles sont évaluées par le vérificateur lui-même.

Les portes de contrainte voyagent sans frais. Une porte de contrainte affirme 0 partout : elle rejoint donc le lot de la transition où elle se trouve, et une porte violée rend la somme groupée non nulle avec une probabilité écrasante. Une seule erreur `LayerInconsistency` couvre aussi bien une affirmation descendante erronée qu’une porte violée; une somme groupée ne peut pas les distinguer, et la preuve ne dépense rien pour les distinguer.

## Pourquoi c’est solide

Chaque défi est tiré après tout ce qu’il protège :

- le point de sortie après les sorties, si bien qu’un prouveur ne peut pas choisir des tables qui ne concordent avec la vérité que là où elles seront vérifiées;
- `λ` après les affirmations et le point, si bien qu’une affirmation fausse ou une porte violée ne survit qu’en une racine d’un polynôme non nul en `λ`;
- chaque défi du sumcheck après la cubique de son tour, si bien qu’une cubique erronée concorde avec la vraie avec une probabilité d’au plus `3/|Fr|`;
- `τ` après les valeurs des deux enfants.

Sommée sur chaque transition d’un circuit enregistré à sa hauteur par défaut, l’erreur de solidité (*soundness*) reste inférieure à `2^14/|Fr|`, avec Fiat–Shamir sur la transcription Poseidon2 dans le modèle de l’oracle aléatoire.

## Les circuits sous forme de données

Un circuit n’est pas du code. C’est un `CircuitArtifact` : ses colonnes engagées, par nom, ses tables virtuelles, ses listes de portes avec sept formes de portes, une liste plate des mêmes relations, ses lookups et sa ligne de remplissage, le tout sérialisé de façon canonique. Quatre lois astreignent chaque artefact à une forme cohérente : chaque opérande est lisible là où il est lu, la largeur de chaque liste est dérivée de ses portes, la couche supérieure correspond exactement aux sorties, et les portes en couches et les relations plates forment un seul ensemble de contraintes. Elles sont vérifiées une seule fois, là où un artefact est construit ou une clé chargée, jamais à chaque preuve.

Deux conséquences comptent pour quiconque évalue le système :

- **Une clé de vérification porte ses circuits, et le vérificateur les astreint à son propre registre.** L’identité du programme lie le programme; le registre lie les circuits qui le prouvent.
- **Les circuits peuvent être vérifiés par une seconde implémentation.** La crate `checker` réimplémente les lois, les règles de lookup et le contrat de remplissage sans partager le code des constructeurs, et n’évalue les portes qu’au moyen du seul noyau de portes que les deux côtés tiennent pour l’autorité sémantique.

## Le coût

Le moteur échange des engagements contre de la mémoire. La passe avant détient chaque couche interne sous forme d’éléments du corps : environ 8,4 GiB pour un shard `2^20` de la famille d’instructions la plus large, et 42 GiB pour un shard `KECCAK_F` de `2^18`, dont le circuit calcule 5 490 colonnes internes. C’est pourquoi la génération de preuves est limitée par la mémoire, pourquoi les hauteurs sont un paramètre de réglage, et pourquoi [le prouveur en flux](https://apogee.gweb3networks.com/docs/architecture/streaming) borne la mémoire par les shards en cours de traitement. La taille de la preuve ne croît que d’un tour de sumcheck par variable et par couche : la preuve d’un shard `KECCAK_F` fait 381 100 octets à `2^18`, contre 373 276 à `2^16`, pour quatre fois plus de travail.

La spécification : [Le moteur GKR](https://apogee.gweb3networks.com/docs/auditors/spec/gkr), et la page propre à chaque famille sous [Auditeurs](https://apogee.gweb3networks.com/docs/auditors).