# 程序与身份

> 客户程序 ELF 如何变成一份验证者已知的静态程序描述，以及为什么一个作为程序身份的域元素，就足以告诉验证者一份证明针对的是哪个程序。

在任何东西执行之前，远地虚拟机先把客户程序（guest）二进制变成程序的一份固定描述：它的映像、按电路族归类的指令、证明时所依据的配置，以及承诺这一切的一个域元素。每一步都是其输入的纯函数。

## 加载

加载器接受静态的 32 位小端序 RISC-V 可执行文件，要求其可加载段位于客户程序 RAM 内的偶数地址上、两两不相交，并且至少有一个可执行段。它只读取程序头的类型、偏移、大小和可执行位，别的一概不读：这台虚拟机没有分页，也没有权限，无论各段声明了什么，整个 RAM 都可寻址。

随后它逐个半字扫描每个可执行段。二进制以 `11` 结尾的半字开始一条 4 字节指令；全零半字是非指令（LLVM 用它填充不可达的基本块）；其余的都是压缩指令，在原位展开为 32 位形式。地址从不紧缩：位于 `0x1002` 的 `c.addi` 留在原处并占两个字节，因此链接器解析出的每个地址都依然成立，而下一个 pc 是 `pc + 2` 还是 `pc + 4`，只由指令的长度记录。

扫描即使失去同步，也无法让错误的指令变得可证明。一个槽位是其自身 pc 处字节的函数，所以每个指令槽位都正是 hart 在那里取指时会解码出的内容。让扫描偏离真实边界的数据只会造成两种结果：丢失真实的指令起点，使这些 pc 在表中没有对应的行；或者遇到一个无人认领的编码，从而拒绝整个映像。

## 解码与路由

解码器只接受 32 位字，并且恰好接受 RV32IMA 的 59 条指令：基础指令集 40 条，M 扩展 8 条，A 扩展 11 条。其余一切，从 RV64 编码、浮点到 CSR 和 `fence.i`，都是解码错误；可执行代码中任何位置只要有一个无法解码的字，无论是否可达，程序都会被拒绝。每条指令都被路由到七个**指令电路族**中的恰好一个：

| 编号 | 电路族 | 指令 |
| --- | --- | --- |
| 0 | `ADD_SUB_LUI_AUIPC` | `ecall`、`ebreak`、`fence`、`addi`、`auipc`、`add`、`sub`、`lui` |
| 1 | `JUMP_BRANCH_SLT` | `slti`、`sltiu`、`slt`、`sltu`、六种分支指令、`jalr`、`jal` |
| 2 | `SHIFT_BITWISE` | 六种移位指令、`and`、`or`、`xor` 及其立即数形式 |
| 3 | `MUL_DIV` | M 扩展的八条指令 |
| 4 | `MEM_WORD` | `lw`、`sw` |
| 5 | `MEM_SUBWORD` | `lb`、`lh`、`lbu`、`lhu`、`sb`、`sh` |
| 6 | `ATOMICS` | `lr.w`、`sc.w` 以及九条 AMO 指令 |

这种分组依据的是电路之间共享的部分。一个比较 gadget 为每种分支和每种 `slt` 确定有符号与无符号的大小关系；一个乘积恒等式同时服务于全部四种乘法和除法；任一方向的移位都是与一个查表所得的 2 的幂的一次乘积。

## 解码表

每个指令电路族都有一张**解码表**，即它的设置列：第 `i` 行对应 pc `2i`，在表所覆盖的地址空间中每个半字一行。有效行以元组 `pc, next_pc, rs1, rs2, rd, imm, extra_mask` 存放该电路族的一条指令，其中掩码以一个比特指明助记符。其余每一行都是填充行，每个字段都是 `−1`，所以有效行永远不会是填充行，全零的行也永远不会成为 pc 0 处一条可被声称的指令。

每个周期的行都以自己的 pc 在其电路族的表中查找自身。正是这次查找把一次执行与程序绑定在一起：一行的指令就是程序在该 pc 处的指令，而在任何表中都没有有效行的 pc 无法被可证明地执行。代码因此是静态的。对 `.text` 的存储会改变之后的加载读到的内容，但永远不会改变执行的内容。

## 配置

程序的静态形状就是它的 **`VmConfig`**：它用到的电路族（每个都有一个高度），以及代码大小的上限。电路族集合不是选出来的，而是推导出来的：

- 映像中含有某个指令电路族的指令时，该电路族就存在；
- 负责内存初始化与收尾的五个窗口电路族总是存在；
- 委托电路族在映像声明它时存在，声明的方式是一条 12 字节的记录：链接该委托的 shim，就会在映像的字节中留下这条记录。

电路族的**高度**是它一个分片中的行数，从 `2^8, 2^12, 2^16, 2^18, 2^20, 2^22` 中选取。每个高度都是 2 的偶数次幂，因为 Mercury 打开要求如此。高度是程序的参数，而不是某次运行的参数；每一种高度选择都构成一个独立的程序。

## 程序身份

**程序身份**是 `Fr` 中的一个元素：对代码版本、`VmConfig`、入口 pc 以及每个电路族的设置承诺所做的 Poseidon2 摘要；这些设置承诺是对解码表和映像初始内存字的 Mercury 承诺。

它绑定：扫描找到的每条指令及其 pc、长度、操作数和类别，以及其他 pc 上都没有指令这一事实；映像中每个来自文件的字节，其中包括委托声明；入口 pc；电路族集合、每个高度、代码大小上限和代码版本。它不绑定：仪式和通用查找（lookup）表，它们由 SRS 摘要覆盖；电路，加载密钥时会要求它们与验证者的注册表一致；任何由执行过程选择的东西；以及 ELF 中加载器不读取的任何内容，例如符号表。

计算程序身份需要仪式提供的幂次，用来做承诺。检查它则只需要这些承诺，而验证密钥带有它们：加载密钥时会根据它们重新计算程序身份，每个分片的打开也会对照同样的这些点检查其设置列。正是这一点，把证明读取的表与验证者所登记的程序身份联系在一起。

> [!IMPORTANT]
> **验证者要从证明者无法控制的渠道获取程序身份。** 如果对照的是证明者提供的身份，证明只能说明有某个程序运行过。持有 ELF、参数和仪式文件的任何人都可以重新计算它。

规范见[程序与身份](https://apogee.gweb3networks.com/docs/auditors/spec/program)。