# Mémoire et lookups

> Deux arguments portent tout ce qui traverse une ligne. Un seul multiensemble lecture/écriture sur toute l’exécution, rapproché une seule fois, fait que chaque lecture renvoie la dernière écriture et ordonne chaque ligne; des canaux LogUp font de chaque valeur un octet, un mot ou une ligne de table.

Les portes d’une famille contraignent une ligne à la fois. Tout ce qui traverse les lignes, les shards ou les familles, comme ce que contient un registre, ce que renvoie un chargement, l’instruction qu’exécute une ligne ou le fait qu’une valeur tienne sur 32 bits, est porté par deux arguments qui résident dans les mêmes circuits GKR.

## L’argument de mémoire

Chaque accès mémoire devient un élément du corps, un **tuple** :

```text
T(AS, ADDR, TS, VAL) = γ + AS + α_addr·ADDR + α_ts·TS + α_val·VAL
```

sur l’espace d’adressage, l’adresse, l’horodatage et la valeur, avec quatre défis tirés une fois par énoncé. Une requête apporte son tuple de lecture à un côté et son tuple d’écriture à l’autre. Le circuit de chaque shard produit en sortie deux nombres, le produit de ses tuples de lecture et le produit de ses tuples d’écriture. Le vérificateur vérifie ensuite une seule équation sur l’énoncé entier :

```text
∏ read roots · R_b  =  ∏ write roots · W_b          over every shard of every family
```

`W_b` et `R_b` sont les tuples initiaux et finaux des 32 registres et du pc, qui n’ont pas de lignes propres : le vérificateur les intègre aux produits à partir de 64 scalaires de frontière que porte l’énoncé. La RAM reçoit ses valeurs initiales et finales des shards des familles de fenêtres, qui contiennent un mot par ligne : l’image du programme dans la fenêtre 0, des zéros dans chaque autre fenêtre que l’exécution a touchée, l’entrée de l’énoncé dans la fenêtre de l’entrée publique, les octets du prouveur dans les données auxiliaires (*advice*).

Si l’équation tient, les multiensembles sont égaux avec une probabilité écrasante. Des multiensembles égaux signifient que **chaque lecture renvoie la dernière écriture qui la précède** : chaque lecture est appariée à exactement une écriture, une lecture doit suivre strictement l’écriture qu’elle consomme, et chaque adresse a exactement une écriture initiale.

### L’ordre sans frais

Le pc est une cellule mémoire comme une autre, à l’adresse 0 de son propre espace. Chaque ligne lit le pc et écrit le suivant, et son circuit astreint l’écriture à se situer au moins quatre horodatages après la lecture. L’historique du pc est donc un seul chemin qui passe par chaque ligne active de chaque famille, du point d’entrée jusqu’à la ligne de sortie. Ce chemin unique donne :

- **l’ordre du programme**, puisque les lignes sont ordonnées par leurs écritures du pc;
- **la continuité d’un shard et d’une famille à l’autre**, puisque la lecture du pc de chaque ligne consomme l’écriture du pc d’une ligne;
- **aucun cycle prouvé deux fois**, puisqu’aucune écriture ne peut être consommée deux fois.

Aucun shard ne s’enchaîne à son voisin, et aucun n’en a besoin. La fenêtre temporelle annoncée d’un shard ne lie rien; seule sa forme est vérifiée.

### Ce qui doit venir en premier

Les défis mémoire sont tirés une fois par énoncé, à la fin de la transcription globale, après que tout ce qu’un tuple peut lire a été fixé : les engagements mémoire de chaque shard, l’identité du programme (qui fixe le pc d’entrée et l’image), le condensé de la cérémonie, les nombres de shards et la liste des fenêtres, le condensé de l’entrée publique et du journal, et en dernier les 64 scalaires de frontière. Une valeur choisie après les défis pourrait être obtenue par résolution; c’est l’ordre de la transcription qui l’interdit. Pour la même raison, un tuple mémoire ne peut lire que des colonnes mémoire, de mise en place et virtuelles, jamais une colonne témoin, laquelle est engagée dans la transcription propre au shard, après les défis. Les constructeurs de circuits refusent tout artefact qui enfreint cette règle.

## Lookups

Un **lookup** affirme qu’un tuple de valeurs d’une ligne est une ligne d’une certaine table. Apogee prouve chaque lookup d’un shard avec **LogUp** : une identité par table, ou **canal**,

```text
Σ_rows Σ_lookups 1/(E(y) + g)  −  Σ_rows mult(y)/(T(y) + g)  =  0
```

sommée par un arbre de fractions à l’intérieur du circuit GKR propre à la famille et vérifiée à sa racine : numérateur nul, dénominateur non nul. La colonne des multiplicités n’a besoin d’aucune contrainte : un tuple qui ne figure dans aucune ligne de table laisse un pôle que les multiplicités ne peuvent pas annuler.

| Canal | Table | Utilisé pour |
| --- | --- | --- |
| `TIMESTAMP` | `[0, 2^19)`, virtuelle | l’écart d’horodatage de chaque requête, en deux fragments de 19 bits |
| `RANGE16` | `[0, 2^16)`, virtuelle | les valeurs de 32 bits, en deux demi-mots; les retenues; les bornes des cadres |
| `XOR8` | toutes les paires d’octets et leur XOR, virtuelle | Keccak et SHA-256, octet par octet |
| `GENERIC` | une table engagée de lignes AND, de signe et de puissances de décalage | les opérations bit à bit, les bits de signe, les amplitudes de décalage |
| `DECODER` | la table décodée de la famille, engagée par l’identité | lier chaque ligne exécutée au programme |

Trois des tables sont virtuelles : des formes closes de l’indice de ligne que le vérificateur évalue lui-même, et qui ne coûtent aucun engagement. La table générique est engagée une seule fois au moyen des puissances de la cérémonie et couverte par le condensé SRS.

### Le lookup du décodeur

Chaque famille d’exécution effectue un lookup par ligne active dans sa propre table décodée, indexé par le pc que la ligne a lu en mémoire. Ce seul lookup lie le cycle au programme : les opérandes, l’immédiat et le type d’instruction de la ligne sont ceux du programme à ce pc, et ses bits de type sont one-hot, parce que chaque ligne active de la table contient un masque one-hot et chaque ligne de remplissage contient `−1`, qu’aucune somme de bits de type n’atteint. Une ligne à un pc où le programme n’a pas d’instruction ne trouve aucune ligne de table.

### Les clés doivent être bornées

Un canal prouve l’appartenance à une table, et rien de plus. Plusieurs sous-tables partagent la table générique sous des plages de clés disjointes : une clé non bornée pourrait donc tomber dans la mauvaise sous-table et prouver un AND faux. Chaque famille borne par conséquent chaque clé qu’elle recherche, au moyen d’un lookup d’intervalle sous le même sélecteur, et les constructeurs de circuits vérifient qu’une borne écrite au moyen d’un facteur d’échelle porte aussi une borne directe. La spécification énonce, pour chaque famille, l’attaque que cela empêche.

## Comment le tout se compose

Avec les portes de chaque famille, ces deux arguments donnent son sens à l’énoncé : chaque ligne obéit à son instruction, l’instruction est celle du programme, chaque lecture voit la dernière écriture, les lignes forment un seul chemin de l’entrée à la sortie, chaque valeur est l’entier qu’elle prétend être, et les fenêtres publiques contiennent les octets de l’énoncé. La [carte de solidité](https://apogee.gweb3networks.com/docs/auditors/soundness-map) mène chaque affirmation jusqu’aux sections qui la prouvent.

La spécification : [L’argument de mémoire](https://apogee.gweb3networks.com/docs/auditors/spec/memory), [Lookups](https://apogee.gweb3networks.com/docs/auditors/spec/lookup).