# Programme und Identität

> Wie aus dem ELF eines Gastprogramms eine statische, dem Verifier bekannte Beschreibung eines Programms wird und warum ein einziges Körperelement als Identität genügt, um einem Verifier zu sagen, auf welches Programm sich ein Beweis bezieht.

Bevor irgendetwas ausgeführt wird, macht Apogee aus dem Binary des Gastprogramms (Guest) eine feste Beschreibung des Programms: sein Image, seine nach Schaltkreisfamilien sortierten Befehle, die Konfiguration, unter der es bewiesen wird, und ein einziges Körperelement, das all das committet. Jeder Schritt ist eine reine Funktion seiner Eingabe.

## Laden

Der Loader akzeptiert ein statisches 32-Bit-RISC-V-Executable im Little-Endian-Format, dessen ladbare Segmente im RAM des Gastprogramms an geraden Adressen liegen, paarweise disjunkt und mindestens eines davon ausführbar. Aus einem Program Header liest er Typ, Offsets, Größen und das Ausführbarkeits-Bit und sonst nichts: Die VM hat keine Speicherseiten und keine Berechtigungen, und der gesamte RAM ist adressierbar, was auch immer die Segmente deklarieren.

Danach durchläuft er jedes ausführbare Segment Halbwort für Halbwort. Ein Halbwort, das binär auf `11` endet, beginnt einen 4-Byte-Befehl; das Null-Halbwort ist ein Nicht-Befehl (LLVM füllt unerreichbare Blöcke damit auf); alles andere ist ein komprimierter Befehl, der an Ort und Stelle zu seiner 32-Bit-Form expandiert wird. Adressen werden nie verdichtet: Ein `c.addi` bei `0x1002` bleibt dort und belegt zwei Byte; jede vom Linker aufgelöste Adresse bleibt also gültig, und allein die Länge eines Befehls hält fest, ob der nächste pc `pc + 2` oder `pc + 4` ist.

Ein desynchronisierter Durchlauf kann keinen falschen Befehl beweisbar machen. Ein Slot ist eine Funktion der Bytes an seinem eigenen pc; jeder Befehls-Slot ist also das, was ein Hart dekodieren würde, der dort einen Befehl holt. Daten, die den Durchlauf von den wahren Grenzen verschieben, können nur echte Befehlsanfänge verlieren, deren pcs dann keine Tabellenzeile haben, oder auf eine nicht zugewiesene Kodierung treffen, woraufhin das ganze Image zurückgewiesen wird.

## Dekodieren und Zuordnen

Der Decoder nimmt nur 32-Bit-Wörter entgegen und akzeptiert genau die 59 Befehle von RV32IMA: 40 aus dem Basissatz, 8 aus M, 11 aus A. Alles andere, von RV64-Kodierungen und Gleitkomma bis zu CSRs und `fence.i`, ist ein Dekodierfehler, und ein einziges nicht dekodierbares Wort irgendwo im ausführbaren Code führt zur Zurückweisung des Programms, ob erreichbar oder nicht. Jeder Befehl wird genau einer von sieben **Befehlsfamilien** zugeordnet:

| Id | Familie | Befehle |
| --- | --- | --- |
| 0 | `ADD_SUB_LUI_AUIPC` | `ecall`, `ebreak`, `fence`, `addi`, `auipc`, `add`, `sub`, `lui` |
| 1 | `JUMP_BRANCH_SLT` | `slti`, `sltiu`, `slt`, `sltu`, die sechs Verzweigungen, `jalr`, `jal` |
| 2 | `SHIFT_BITWISE` | die sechs Shifts, `and`, `or`, `xor` und ihre Immediate-Formen |
| 3 | `MUL_DIV` | die acht Befehle der M-Erweiterung |
| 4 | `MEM_WORD` | `lw`, `sw` |
| 5 | `MEM_SUBWORD` | `lb`, `lh`, `lbu`, `lhu`, `sb`, `sh` |
| 6 | `ATOMICS` | `lr.w`, `sc.w` und die neun AMOs |

Die Gruppierung folgt dem, was die Schaltkreise gemeinsam haben. Ein einziges Vergleichs-Gadget entscheidet die Ordnung mit und ohne Vorzeichen für jede Art von Verzweigung und `slt`; eine einzige Produktidentität dient allen vier Multiplikationen und der Division; ein Shift in jede Richtung ist ein einziges Produkt mit einer nachgeschlagenen Zweierpotenz.

## Dekodierte Tabellen

Jede Befehlsfamilie erhält eine **dekodierte Tabelle**: ihre Setup-Spalten, in denen Zeile `i` zu pc `2i` gehört, eine Zeile pro Halbwort des Adressraums, den die Tabelle erreicht. Eine aktive Zeile enthält einen der Befehle der Familie als Tupel `pc, next_pc, rs1, rs2, rd, imm, extra_mask`, wobei ein einzelnes Bit der Maske das Mnemonic benennt. Jede andere Zeile ist Padding, `−1` in jedem Feld; keine aktive Zeile ist also je die Padding-Zeile, und eine Zeile aus lauter Nullen ist nie ein beanspruchbarer Befehl bei pc 0.

Die Zeile jedes Zyklus schlägt sich selbst anhand ihres pc in der Tabelle ihrer Familie nach. Dieser Lookup bindet eine Ausführung an das Programm: Der Befehl einer Zeile ist der Befehl des Programms an diesem pc, und ein pc ohne aktive Zeile in irgendeiner Tabelle kann nicht beweisbar ausgeführt werden. Code ist daher statisch. Ein Store in `.text` ändert, was ein späterer Load liest, nie, was ausgeführt wird.

## Die Konfiguration

Die statische Form eines Programms ist seine **`VmConfig`**: die Familien, die es verwendet, jede mit einer Höhe, und eine Obergrenze für seine Codegröße. Die Menge der Familien wird nicht gewählt, sondern abgeleitet:

- eine Befehlsfamilie ist vorhanden, wenn das Image einen ihrer Befehle enthält;
- die fünf Fensterfamilien, die den Speicher initialisieren und abschließen, sind immer vorhanden;
- eine Delegationsfamilie ist vorhanden, wenn das Image sie deklariert, über einen 12-Byte-Datensatz, den das Linken ihres Shims unter den Bytes des Images hinterlässt.

Die **Höhe** einer Familie ist die Zahl der Zeilen in einem ihrer Shards, gewählt aus `2^8, 2^12, 2^16, 2^18, 2^20, 2^22`. Jede Höhe ist eine Zweierpotenz mit geradem Exponenten, weil eine Mercury-Öffnung das verlangt. Höhen sind ein Parameter des Programms, nicht eines Laufs, und jede Wahl der Höhen ist ein eigenes Programm.

## Programmidentität

Die **Programmidentität** ist ein einziges Element von `Fr`: ein Poseidon2-Digest über die Codeversion, die `VmConfig`, den Einsprung-pc und die Setup-Commitments jeder Familie, also die Mercury-Commitments auf die dekodierten Tabellen und auf die anfänglichen Speicherwörter des Images.

Sie bindet jeden Befehl, den der Durchlauf gefunden hat, mit seinem pc, seiner Länge, seinen Operanden und seiner Art, sowie die Tatsache, dass kein anderer pc einen Befehl enthält; jedes in der Datei enthaltene Byte des Images, was die Delegationsdeklarationen einschließt; den Einsprung-pc; die Menge der Familien, jede Höhe, die Obergrenze der Codegröße und die Codeversion. Sie bindet nicht die Zeremonie oder die generische Lookup-Tabelle, die der SRS-Digest abdeckt; nicht die Schaltkreise, die beim Laden eines Schlüssels mit der Registry des Verifiers abgeglichen werden; nichts, was eine Ausführung wählt; und nichts aus dem ELF, was der Loader nicht liest, etwa die Symboltabelle.

Ihre Berechnung braucht die Potenzen der Zeremonie, um zu committen. Ihre Prüfung braucht nur die Commitments, die ein Verifikationsschlüssel mitführt: Beim Laden eines Schlüssels wird die Identität aus ihnen neu berechnet, und die Öffnung jedes Shards prüft seine Setup-Spalten gegen dieselben Punkte. Das verbindet die Tabellen, die ein Beweis liest, mit der Identität, die ein Verifier registriert hat.

> [!IMPORTANT]
> **Ein Verifier bezieht die Identität über einen Kanal, den der Prover nicht kontrolliert.** Gegenüber einer vom Prover gelieferten Identität zeigt ein Beweis nur, dass irgendein Programm gelaufen ist. Wer das ELF, die Parameter und die Zeremoniedatei besitzt, kann sie neu berechnen.

Die Spezifikation: [Programm und Identität](https://apogee.gweb3networks.com/docs/auditors/spec/program).