# Programs and Identity

> How a guest ELF becomes a static, verifier-known description of a program, and why one field element of identity is enough to tell a verifier which program a proof is about.

Before anything executes, Apogee turns the guest binary into a fixed description of the program: its image, its instructions sorted into circuit families, the configuration it will be proved under, and one field element that commits to all of it. Every step is a pure function of its input.

## Loading

The loader accepts a static 32-bit little-endian RISC-V executable whose loadable segments lie inside guest RAM at even addresses, pairwise disjoint, at least one executable. It reads a program header's type, offsets, sizes and executable bit, and nothing else: the VM has no pages and no permissions, and all of RAM is addressable whatever the segments declare.

It then sweeps each executable segment halfword by halfword. A halfword ending in binary `11` begins a 4-byte instruction; the zero halfword is a non-instruction (LLVM pads unreachable blocks with it); anything else is a compressed instruction, expanded to its 32-bit form in place. Addresses are never compacted: a `c.addi` at `0x1002` stays there and occupies two bytes, so every linker-resolved address holds, and an instruction's length is the only record of whether the next pc is `pc + 2` or `pc + 4`.

A desynchronized sweep cannot make a wrong instruction provable. A slot is a function of the bytes at its own pc, so every instruction slot is what a hart fetching there would decode. Data that shifts the sweep off the true boundaries can only lose true instruction starts, whose pcs then have no table row, or meet an unclaimed encoding and refuse the whole image.

## Decoding and routing

The decoder takes 32-bit words only and accepts exactly the 59 instructions of RV32IMA: 40 of the base set, 8 of M, 11 of A. Everything else, from RV64 encodings and floating point to CSRs and `fence.i`, is a decode error, and one undecodable word anywhere in executable code refuses the program, reachable or not. Each instruction is routed to exactly one of seven **instruction families**:

| Id | Family | Instructions |
| --- | --- | --- |
| 0 | `ADD_SUB_LUI_AUIPC` | `ecall`, `ebreak`, `fence`, `addi`, `auipc`, `add`, `sub`, `lui` |
| 1 | `JUMP_BRANCH_SLT` | `slti`, `sltiu`, `slt`, `sltu`, the six branches, `jalr`, `jal` |
| 2 | `SHIFT_BITWISE` | the six shifts, `and`, `or`, `xor` and their immediate forms |
| 3 | `MUL_DIV` | the eight instructions of the M extension |
| 4 | `MEM_WORD` | `lw`, `sw` |
| 5 | `MEM_SUBWORD` | `lb`, `lh`, `lbu`, `lhu`, `sb`, `sh` |
| 6 | `ATOMICS` | `lr.w`, `sc.w` and the nine AMOs |

The grouping follows what the circuits share. One comparison gadget settles signed and unsigned order for every branch and `slt` kind; one product identity serves all four multiplies and the division; a shift either way is one product with a looked-up power of two.

## Decoded tables

Each instruction family gets a **decoded table**: its setup columns, where row `i` is pc `2i`, one row per halfword of the address space the table reaches. A live row holds one of the family's instructions as a tuple `pc, next_pc, rs1, rs2, rd, imm, extra_mask`, where the mask is one bit naming the mnemonic. Every other row is padding, `−1` in every field, so no live row is ever the padding row and an all-zero row is never a claimable instruction at pc 0.

Every cycle's row looks itself up in its family's table by its pc. That lookup is what binds an execution to the program: a row's instruction is the program's instruction at that pc, and a pc with no live row in any table cannot be executed provably. Code is static as a result. A store into `.text` changes what a later load reads, never what executes.

## The configuration

A program's static shape is its **`VmConfig`**: the families it uses, each with a height, and a ceiling on its code size. Nothing chooses the family set; it is derived:

- an instruction family is present when the image holds one of its instructions;
- the five window families, which initialize and tear down memory, are always present;
- a delegation family is present when the image declares it, through a 12-byte record that linking its shim leaves among the image's bytes.

A family's **height** is the number of rows in one of its shards, chosen from `2^8, 2^12, 2^16, 2^18, 2^20, 2^22`. Every height is an even power of two because a Mercury opening needs one. Heights are a parameter of the program, not of a run, and each choice of heights is its own program.

## Program identity

The **program identity** is one element of `Fr`: a Poseidon2 digest of the code version, the `VmConfig`, the entry pc, and every family's setup commitments, which are Mercury commitments to the decoded tables and to the image's initial memory words.

It binds every instruction the sweep found, with its pc, length, operands and kind, and that no other pc holds one; every file-backed byte of the image, which includes the delegation declarations; the entry pc; the family set, every height, the code-size ceiling and the code version. It does not bind the ceremony or the generic lookup table, which the SRS digest covers; the circuits, which a key's load holds to the verifier's registry; anything an execution chooses; or anything of the ELF the loader does not read, such as the symbol table.

Computing it needs the ceremony's powers, to commit. Checking it needs only the commitments, which a verifying key carries: loading a key recomputes the identity from them, and every shard's opening checks its setup columns against the same points. That is what ties the tables a proof reads to the identity a verifier registered.

> [!IMPORTANT]
> **A verifier takes the identity from a channel the prover does not control.** Against an identity the prover supplied, a proof shows only that some program ran. Whoever holds the ELF, the parameters and the ceremony file can recompute it.

The specification: [Program and identity](https://apogee.gweb3networks.com/docs/auditors/spec/program).