# Speicher und Lookups

> Zwei Argumente tragen alles, was über eine Zeile hinausreicht. Eine einzige Lese-/Schreib-Multimenge über die gesamte Ausführung, einmal abgeglichen, sorgt dafür, dass jeder Lesezugriff den letzten Schreibzugriff liefert, und ordnet jede Zeile; LogUp-Kanäle machen jeden Wert zu einem Byte, einem Wort oder einer Tabellenzeile.

Die Gates einer Familie stellen Bedingungen an jeweils eine Zeile. Alles, was über Zeilen, Shards oder Familien hinausreicht, etwa was ein Register enthält, was ein Load liefert, welchen Befehl eine Zeile ausführt und ob ein Wert in 32 Bit passt, tragen zwei Argumente, die in denselben GKR-Schaltkreisen leben.

## Das Speicherargument

Jeder Speicherzugriff wird zu einem Körperelement, einem **Tupel**:

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

über dem Adressraum, der Adresse, dem Zeitstempel und dem Wert, mit vier Challenges, die einmal pro Aussage gezogen werden. Eine Abfrage trägt ihr Lesetupel zu einer Seite bei und ihr Schreibtupel zur anderen. Der Schaltkreis jedes Shards gibt zwei Zahlen aus, das Produkt seiner Lesetupel und das Produkt seiner Schreibtupel. Der Verifier prüft dann eine einzige Gleichung über die gesamte Aussage:

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

`W_b` und `R_b` sind die Anfangs- und Endtupel der 32 Register und des pc, die keine eigenen Zeilen haben: Der Verifier bildet sie aus 64 Randskalaren, die die Aussage mitführt, und multipliziert sie ein. Der RAM erhält seine Anfangs- und Endwerte aus den Shards der Fensterfamilien, die ein Wort pro Zeile enthalten: das Image des Programms in Fenster 0, Nullen in jedem anderen Fenster, das der Lauf berührt hat, die Eingabe der Aussage im öffentlichen Eingabefenster, die Bytes des Provers in den Hilfsdaten (Advice).

Gilt die Gleichung, sind die Multimengen mit überwältigender Wahrscheinlichkeit gleich. Gleiche Multimengen bedeuten, dass **jeder Lesezugriff den letzten Schreibzugriff davor liefert**: Jeder Lesezugriff wird genau einem Schreibzugriff zugeordnet, ein Lesezugriff muss strikt auf den Schreibzugriff folgen, den er konsumiert, und jede Adresse hat genau einen anfänglichen Schreibzugriff.

### Reihenfolge ohne Zusatzkosten

Der pc ist eine Speicherzelle wie jede andere, an Adresse 0 seines eigenen Adressraums. Jede Zeile liest den pc und schreibt den nächsten, und ihr Schaltkreis erzwingt, dass der Schreibzugriff mindestens vier Zeitstempel nach dem Lesezugriff liegt. Die Historie des pc ist also ein einziger Pfad durch jede aktive Zeile jeder Familie, vom Einsprungpunkt bis zur Exit-Zeile. Dieser eine Pfad liefert:

- **Programmreihenfolge**, da Zeilen nach ihren pc-Schreibzugriffen geordnet sind;
- **Kontinuität über Shards und Familien hinweg**, da der pc-Lesezugriff jeder Zeile den pc-Schreibzugriff irgendeiner Zeile konsumiert;
- **keinen doppelt bewiesenen Zyklus**, da kein Schreibzugriff zweimal konsumiert werden kann.

Kein Shard ist mit seinem Nachbarn verkettet, und keiner muss es sein. Das behauptete Zeitfenster eines Shards bindet nichts; es wird nur auf seine Form geprüft.

### Was zuerst feststehen muss

Die Speicher-Challenges werden einmal pro Aussage gezogen, am Ende des globalen Transkripts, nachdem alles feststeht, was ein Tupel lesen kann: die Speicher-Commitments jedes Shards, die Programmidentität (die den Einsprung-pc und das Image festlegt), der Digest der Zeremonie, die Shard-Zahlen und die Fensterliste, der Digest von öffentlicher Eingabe und Journal und zuletzt die 64 Randskalare. Ein nach den Challenges gewählter Wert ließe sich passend errechnen; die Reihenfolge des Transkripts verhindert das. Aus demselben Grund darf ein Speichertupel nur Speicher-, Setup- und virtuelle Spalten lesen, nie eine Witness-Spalte, die im eigenen Transkript des Shards nach den Challenges committet wird. Die Schaltkreiskonstruktoren weisen jedes Artefakt zurück, das dagegen verstößt.

## Lookups

Ein **Lookup** besagt, dass ein Tupel aus Werten einer Zeile eine Zeile irgendeiner Tabelle ist. Apogee beweist jeden Lookup eines Shards mit **LogUp**: eine Identität pro Tabelle oder **Kanal**,

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

summiert über einen Bruchbaum im eigenen GKR-Schaltkreis der Familie und an dessen Wurzel geprüft: Zähler null, Nenner ungleich null. Die Multiplizitätsspalte braucht überhaupt keinen Constraint: Ein Tupel, das in keiner Tabellenzeile vorkommt, hinterlässt eine Polstelle, die die Multiplizitäten nicht aufheben können.

| Kanal | Tabelle | Verwendet für |
| --- | --- | --- |
| `TIMESTAMP` | `[0, 2^19)`, virtuell | den Zeitstempelabstand jeder Abfrage, als zwei Chunks zu je 19 Bit |
| `RANGE16` | `[0, 2^16)`, virtuell | 32-Bit-Werte als zwei Halbwörter; Überträge; Frame-Schranken |
| `XOR8` | alle Bytepaare und ihr XOR, virtuell | Keccak und SHA-256, Byte für Byte |
| `GENERIC` | eine committete Tabelle aus Zeilen für AND, Vorzeichen und Shift-Potenzen | bitweise Operationen, Vorzeichenbits, Shift-Beträge |
| `DECODER` | die dekodierte Tabelle der Familie, committet durch die Identität | Bindung jeder ausgeführten Zeile an das Programm |

Drei der Tabellen sind virtuell: geschlossene Formen des Zeilenindex, die der Verifier selbst auswertet und die kein Commitment kosten. Die generische Tabelle wird einmal mit den Potenzen der Zeremonie committet und ist durch den SRS-Digest abgedeckt.

### Der Decoder-Lookup

Jede Ausführungsfamilie macht pro aktiver Zeile einen Lookup in ihre eigene dekodierte Tabelle, mit dem pc als Schlüssel, den die Zeile aus dem Speicher gelesen hat. Dieser eine Lookup bindet den Zyklus an das Programm: Operanden, Immediate und Befehlsart der Zeile sind die des Programms an diesem pc, und ihre Bits für die Befehlsart sind one-hot, weil jede aktive Zeile der Tabelle eine One-hot-Maske enthält und jede Padding-Zeile `−1`, was keine Summe solcher Bits erreicht. Eine Zeile an einem pc, an dem das Programm keinen Befehl hat, findet überhaupt keine Tabellenzeile.

### Schlüssel müssen beschränkt sein

Ein Kanal beweist die Zugehörigkeit zu einer Tabelle und nichts weiter. Mehrere Teiltabellen teilen sich die generische Tabelle unter disjunkten Schlüsselbereichen; ein unbeschränkter Schlüssel könnte also in der falschen Teiltabelle landen und ein falsches AND beweisen. Jede Familie beschränkt deshalb jeden Schlüssel, den sie nachschlägt, mit einem Bereichs-Lookup unter demselben Selektor, und die Schaltkreiskonstruktoren prüfen, dass eine über einen Skalierungsfaktor geschriebene Schranke zusätzlich eine direkte Schranke trägt. Die Spezifikation nennt für jede Familie den Angriff, den das verhindert.

## Wie sich alles zusammenfügt

Zusammen mit den Gates jeder Familie geben diese beiden Argumente der Aussage ihre Bedeutung: Jede Zeile befolgt ihren Befehl, der Befehl ist der des Programms, jeder Lesezugriff sieht den letzten Schreibzugriff, die Zeilen bilden einen einzigen Pfad vom Einsprung bis zum Exit, jeder Wert ist die ganze Zahl, die er zu sein behauptet, und die öffentlichen Fenster enthalten die Bytes der Aussage. Die [Soundness-Karte](https://apogee.gweb3networks.com/docs/auditors/soundness-map) führt jede Behauptung zu den Abschnitten, die sie beweisen.

Die Spezifikation: [Das Speicherargument](https://apogee.gweb3networks.com/docs/auditors/spec/memory), [Lookups](https://apogee.gweb3networks.com/docs/auditors/spec/lookup).