# Programmes et identité

> Comment un ELF de programme invité devient une description statique du programme, connue du vérificateur, et pourquoi un seul élément du corps, l’identité, suffit à indiquer à un vérificateur de quel programme parle une preuve.

Avant que quoi que ce soit ne s’exécute, Apogee transforme le binaire du programme invité en une description fixe du programme : son image, ses instructions réparties en familles de circuits, la configuration sous laquelle il sera prouvé, et un seul élément du corps qui engage le tout. Chaque étape est une fonction pure de son entrée.

## Chargement

Le chargeur accepte un exécutable RISC-V statique, 32 bits et petit-boutiste, dont les segments chargeables se trouvent dans la RAM du programme invité à des adresses paires, sont disjoints deux à deux et comprennent au moins un segment exécutable. Il lit le type, les décalages, les tailles et le bit d’exécution d’un en-tête de programme, et rien d’autre : la VM n’a ni pages ni permissions, et toute la RAM est adressable, quoi que déclarent les segments.

Il balaie ensuite chaque segment exécutable demi-mot par demi-mot. Un demi-mot qui se termine par `11` en binaire commence une instruction de 4 octets; le demi-mot nul est une non-instruction (LLVM en remplit les blocs inatteignables); tout le reste est une instruction compressée, développée sur place en sa forme de 32 bits. Les adresses ne sont jamais compactées : un `c.addi` à `0x1002` y reste et occupe deux octets, si bien que chaque adresse résolue par l’éditeur de liens reste valable, et que la longueur d’une instruction est la seule indication permettant de savoir si le pc suivant est `pc + 2` ou `pc + 4`.

Un balayage désynchronisé ne peut pas rendre prouvable une instruction erronée. Un emplacement est une fonction des octets situés à son propre pc : chaque emplacement d’instruction est donc ce que décoderait un hart qui irait y chercher une instruction. Des données qui décalent le balayage par rapport aux vraies frontières ne peuvent que faire perdre de vrais débuts d’instruction, dont les pc n’ont alors aucune ligne de table, ou tomber sur un encodage non reconnu et faire refuser l’image entière.

## Décodage et acheminement

Le décodeur ne prend que des mots de 32 bits et accepte exactement les 59 instructions de RV32IMA : 40 du jeu de base, 8 de M, 11 de A. Tout le reste, des encodages RV64 et de la virgule flottante aux CSR et à `fence.i`, est une erreur de décodage, et un seul mot indécodable n’importe où dans le code exécutable entraîne le refus du programme, qu’il soit atteignable ou non. Chaque instruction est acheminée vers exactement une des sept **familles d’instructions** :

| Id | Famille | Instructions |
| --- | --- | --- |
| 0 | `ADD_SUB_LUI_AUIPC` | `ecall`, `ebreak`, `fence`, `addi`, `auipc`, `add`, `sub`, `lui` |
| 1 | `JUMP_BRANCH_SLT` | `slti`, `sltiu`, `slt`, `sltu`, les six branchements, `jalr`, `jal` |
| 2 | `SHIFT_BITWISE` | les six décalages, `and`, `or`, `xor` et leurs formes immédiates |
| 3 | `MUL_DIV` | les huit instructions de l’extension M |
| 4 | `MEM_WORD` | `lw`, `sw` |
| 5 | `MEM_SUBWORD` | `lb`, `lh`, `lbu`, `lhu`, `sb`, `sh` |
| 6 | `ATOMICS` | `lr.w`, `sc.w` et les neuf AMO |

Le regroupement suit ce que partagent les circuits. Un seul gadget de comparaison tranche l’ordre signé et non signé pour chaque type de branchement et de `slt`; une seule identité de produit sert aux quatre multiplications et à la division; un décalage dans un sens ou dans l’autre est un seul produit avec une puissance de deux obtenue par lookup.

## Tables décodées

Chaque famille d’instructions reçoit une **table décodée** : ses colonnes de mise en place, où la ligne `i` correspond au pc `2i`, avec une ligne par demi-mot de l’espace d’adressage qu’atteint la table. Une ligne active contient l’une des instructions de la famille sous la forme d’un tuple `pc, next_pc, rs1, rs2, rd, imm, extra_mask`, où le masque est un seul bit qui désigne le mnémonique. Toute autre ligne est du remplissage, `−1` dans chaque champ : aucune ligne active n’est donc jamais la ligne de remplissage, et une ligne entièrement nulle ne peut jamais être revendiquée comme instruction au pc 0.

La ligne de chaque cycle se recherche elle-même dans la table de sa famille, par son pc. C’est ce lookup qui lie une exécution au programme : l’instruction d’une ligne est l’instruction du programme à ce pc, et un pc sans ligne active dans aucune table ne peut pas être exécuté de façon prouvable. Le code est par conséquent statique. Un rangement dans `.text` change ce que lit un chargement ultérieur, jamais ce qui s’exécute.

## La configuration

La forme statique d’un programme est sa **`VmConfig`** : les familles qu’il utilise, chacune avec une hauteur, et un plafond sur la taille de son code. L’ensemble des familles ne se choisit pas; il se dérive :

- une famille d’instructions est présente quand l’image contient l’une de ses instructions;
- les cinq familles de fenêtres, qui initialisent et finalisent la mémoire, sont toujours présentes;
- une famille de délégation est présente quand l’image la déclare, au moyen d’un enregistrement de 12 octets que l’édition de liens de son shim laisse parmi les octets de l’image.

La **hauteur** d’une famille est le nombre de lignes de l’un de ses shards, choisie parmi `2^8, 2^12, 2^16, 2^18, 2^20, 2^22`. Chaque hauteur est une puissance paire de deux, parce qu’une ouverture Mercury l’exige. Les hauteurs sont un paramètre du programme, et non d’une exécution, et chaque choix de hauteurs constitue un programme distinct.

## Identité du programme

L’**identité du programme** est un élément de `Fr` : un condensé Poseidon2 de la version du code, de la `VmConfig`, du pc d’entrée et des engagements de mise en place de chaque famille, qui sont des engagements Mercury sur les tables décodées et sur les mots mémoire initiaux de l’image.

Elle lie chaque instruction qu’a trouvée le balayage, avec son pc, sa longueur, ses opérandes et son type, ainsi que le fait qu’aucun autre pc n’en contient; chaque octet de l’image issu du fichier, ce qui inclut les déclarations de délégation; le pc d’entrée; l’ensemble des familles, chaque hauteur, le plafond de taille du code et la version du code. Elle ne lie ni la cérémonie ni la table de lookup générique, que couvre le condensé SRS; ni les circuits, que le chargement d’une clé astreint au registre du vérificateur; ni rien de ce que choisit une exécution; ni rien de l’ELF que le chargeur ne lit pas, comme la table des symboles.

La calculer exige les puissances de la cérémonie, pour engager. La vérifier n’exige que les engagements, que porte une clé de vérification : le chargement d’une clé recalcule l’identité à partir d’eux, et l’ouverture de chaque shard vérifie ses colonnes de mise en place par rapport aux mêmes points. C’est ce qui rattache les tables que lit une preuve à l’identité qu’un vérificateur a enregistrée.

> [!IMPORTANT]
> **Un vérificateur obtient l’identité par un canal que le prouveur ne contrôle pas.** Face à une identité fournie par le prouveur, une preuve montre seulement qu’un programme quelconque s’est exécuté. Quiconque détient l’ELF, les paramètres et le fichier de cérémonie peut la recalculer.

La spécification : [Programme et identité](https://apogee.gweb3networks.com/docs/auditors/spec/program).