# 审计指南

> 审计远地虚拟机 v1.0.0 起步所需的一切：审计范围、规范原文及其组织方式、记号约定、信任边界、阅读顺序，以及最值得优先检查的性质。

本部分是远地虚拟机 v1.0.0 的完整构造，按评估的需要组织。其核心是逐字转载的**规范原文**：每个主题一页，列出每个已承诺列的索引与名称、写成多项式的每个门、每个查找及其通道、按顺序排列的每条 transcript 消息，以及每种序列化格式的每一个字节。围绕它，本指南和[可靠性地图](https://apogee.gweb3networks.com/docs/auditors/soundness-map)为审计者提供入口。

## 审计范围

| 审计范围 | 位置 |
| --- | --- |
| 证明所确立的陈述，以及验证者必须持有的内容 | [系统全貌](https://apogee.gweb3networks.com/docs/auditors/spec/architecture)、[证明](https://apogee.gweb3networks.com/docs/auditors/spec/proof) |
| 算术：`Fr`、`Fq` 扩域塔、G1 与 G2、配对、MSM、多线性多项式、求和校验（sumcheck） | [原语](https://apogee.gweb3networks.com/docs/auditors/spec/primitives) |
| Fiat–Shamir：Poseidon2、双工海绵、所有标签 | [Transcript](https://apogee.gweb3networks.com/docs/auditors/spec/transcript) |
| 可信设置与承诺方案 | [结构化参考串](https://apogee.gweb3networks.com/docs/auditors/spec/srs)、[Mercury](https://apogee.gweb3networks.com/docs/auditors/spec/mercury) |
| 程序：加载、解码、表、配置、程序身份 | [程序与身份](https://apogee.gweb3networks.com/docs/auditors/spec/program)、[客户程序（guest）ABI](https://apogee.gweb3networks.com/docs/auditors/spec/ecall-abi) |
| 执行模型与执行轨迹 | [执行轨迹](https://apogee.gweb3networks.com/docs/auditors/spec/execution-trace)、[公开值与证明者提示（advice）](https://apogee.gweb3networks.com/docs/auditors/spec/public-values) |
| 证明系统：GKR、电路注册表、内存论证、查找（lookup） | [GKR 引擎](https://apogee.gweb3networks.com/docs/auditors/spec/gkr)、[电路](https://apogee.gweb3networks.com/docs/auditors/spec/circuits)、[内存论证](https://apogee.gweb3networks.com/docs/auditors/spec/memory)、[查找](https://apogee.gweb3networks.com/docs/auditors/spec/lookup) |
| 每个电路族，逐列展开 | 七个指令电路族和六个委托电路 |
| 证明者的结构 | [流式证明者](https://apogee.gweb3networks.com/docs/auditors/spec/streaming) |
| 递归、Groth16 判定器及其仪式、合约 | [递归与判定器](https://apogee.gweb3networks.com/docs/auditors/spec/recursion) |
| 以太坊工作负载 | [以太坊区块](https://apogee.gweb3networks.com/docs/auditors/spec/ethereum) |

规范页面转载自远地虚拟机代码仓库在源码修订版 `3571370` 时的 `docs/`：相对链接改成了本站链接，每个 `§` 引用都改成了指向对应章节的链接。术语表中有一处措辞为与本站其余部分保持一致而改写；除此之外没有任何改动。**规范页面与代码不一致时，以代码为准**，而这种不一致本身就是一项审计发现。

## 如何阅读规范

这些页面是为对照代码阅读而写的。每一页都写明实现其所述内容的 crate 和函数，源码注释也按章节反向引用规范（`docs/spec/memory.md` §2.4）。以下是反复出现的一些约定：

| 记号 | 含义 |
| --- | --- |
| `M[i]`、`W[i]`、`S[i]` | 电路的已承诺列：内存列（在全局 transcript 中、内存挑战之前绑定）、见证列（在分片自己的 transcript 中绑定）、设置列（由程序身份或 SRS 摘要绑定） |
| `V[…]` | 虚拟表：行索引的闭式表达式，从不承诺 |
| `L{k}[j]`、`C{k}[j]`、`scratch[i]` | 第 `k` 层的内部列 `j`；缓存项；扁平关系的中间值 |
| `W[8..14]` | 列索引的半开区间，即 `W[8]` 到 `W[13]` |
| `T(AS, ADDR, TS, VAL)` | 内存元组，`γ_M + AS + α_addr·ADDR + α_ts·TS + α_val·VAL` |
| `4c + Δ` | 周期 `c` 中槽位 `Δ` 的时间戳 |
| G1–G11、S1–S6 | 全局 transcript 与分片 transcript 的步骤 |
| 步骤 1–12、B1–B6 | 验证者依次对分片和块（block）所做的检查 |
| `2^n` | 2 的幂；高度取 `2^8, 2^12, 2^16, 2^18, 2^20, 2^22` |

写成表达式的门，约束其值为 0。查找写成它的通道、选择子和元组。“有界”指经过范围检查；称为**字**的值是 `[0, 2^32)` 中的整数。

## 阅读顺序

第一遍阅读，先建立完整的论证，再深入各个电路：

1. **[系统全貌](https://apogee.gweb3networks.com/docs/auditors/spec/architecture)。** 断言、组合表、假设、限制。
2. **[证明](https://apogee.gweb3networks.com/docs/auditors/spec/proof)。** 陈述、两种 transcript、验证顺序、密钥及其加载规则。
3. **[GKR 引擎](https://apogee.gweb3networks.com/docs/auditors/spec/gkr)。** 层模型、制品及其法则、反向过程及其可靠的理由。
4. **[内存论证](https://apogee.gweb3networks.com/docs/auditors/spec/memory)** 与 **[查找](https://apogee.gweb3networks.com/docs/auditors/spec/lookup)。** 一切跨行内容所依赖的两种论证，以及它们的构造期规则。
5. **[电路](https://apogee.gweb3networks.com/docs/auditors/spec/circuits)。** 注册表、各电路的形状，以及电路族的电路如何组装。
6. **指令电路族**，从 **[`ADD_SUB_LUI_AUIPC`](https://apogee.gweb3networks.com/docs/auditors/spec/add-sub)** 开始，它承载每一个 `ecall` 以及每次委托的请求一侧。
7. **[委托 ABI](https://apogee.gweb3networks.com/docs/auditors/spec/delegation)** 与 **[委托电路](https://apogee.gweb3networks.com/docs/auditors/spec/delegation-circuits)。**
8. **[程序与身份](https://apogee.gweb3networks.com/docs/auditors/spec/program)**、**[公开值](https://apogee.gweb3networks.com/docs/auditors/spec/public-values)**、**[执行轨迹](https://apogee.gweb3networks.com/docs/auditors/spec/execution-trace)**。
9. **[Transcript](https://apogee.gweb3networks.com/docs/auditors/spec/transcript)**、**[SRS](https://apogee.gweb3networks.com/docs/auditors/spec/srs)**、**[Mercury](https://apogee.gweb3networks.com/docs/auditors/spec/mercury)**、**[原语](https://apogee.gweb3networks.com/docs/auditors/spec/primitives)。**
10. **[递归与判定器](https://apogee.gweb3networks.com/docs/auditors/spec/recursion)**，然后是合约。

## 信任边界

可靠性只取决于验证者，而验证者的代码是一组明确界定的 crate：

| 受信任的用途 | Crate |
| --- | --- |
| 验证一个块 | `constants`、`field`、`curve`、`transcript`、`poly`、`sumcheck`、`pcs-verify`、`pcs`、`gkr-verify`、`verifier-core`、`verifier`，以及 `constraints`，因为电路是陈述的一部分，缺失一个门就是可靠性漏洞 |
| 从 ELF 计算程序身份 | `loader`、`isa`、`program` |
| 上链的最后一步 | `guests/recursion`、`groth16`、判定器的电路、`contracts/ApogeeVerifier.sol` |
| 不受信任 | `prover`、`emulator`、`trace`、`host` 中负责证明的一半：证明者不做任何校验 |

所依赖的假设是：Mercury 与 KZG 在代数群模型中、q-DLOG 假设下的知识可靠性；Poseidon2 作为随机预言机；最后一步依赖 Groth16 自身的假设；每个仪式有一位诚实的贡献者。没有任何部分是常数时间的，也没有任何证明是零知识的。验证者必须从证明者无法控制的渠道获得程序身份和仪式的 SRS 摘要。

## 优先检查之处

下列性质一旦失效就意味着可以伪造，表中给出了每一项的论证位置。[可靠性地图](https://apogee.gweb3networks.com/docs/auditors/soundness-map)以同样的方式梳理了陈述中的每一项断言。

| 性质 | 论证位置 |
| --- | --- |
| 每个挑战都在其所保护的一切之后抽取：内存挑战在每个 `M` 承诺、窗口列表、`io_digest` 和 64 个边界标量之后；`g` 与 `β` 在该分片的 `W` 承诺之后 | [proof §2](https://apogee.gweb3networks.com/docs/auditors/spec/proof#s2)、[§4](https://apogee.gweb3networks.com/docs/auditors/spec/proof#s4)；[memory §6.1](https://apogee.gweb3networks.com/docs/auditors/spec/memory#s6-1) |
| 任何内存元组或根都不读取 `W` 列，这类列在内存挑战之后才承诺 | [memory §8](https://apogee.gweb3networks.com/docs/auditors/spec/memory#s8) |
| 帧只约束其掩码的布尔性；每个电路族都把每个掩码固定为 `m_pc` 乘以会发起该查询的那些 kind | [memory §2.1](https://apogee.gweb3networks.com/docs/auditors/spec/memory#s2-1)；各电路族页面 |
| 表通道所查找的每个键都由其电路族限定范围，而每个通过 copower 写出的界也同时带有直接界 | [lookup §4](https://apogee.gweb3networks.com/docs/auditors/spec/lookup#s4)、[§11](https://apogee.gweb3networks.com/docs/auditors/spec/lookup#s11)；[shift-bitwise §3](https://apogee.gweb3networks.com/docs/auditors/spec/shift-bitwise#s3) |
| 从帧字中解码出的选择子是 one-hot 的，因为编码会相加 | [delegation circuits §1](https://apogee.gweb3networks.com/docs/auditors/spec/delegation-circuits#s1) |
| 每个委托请求恰好与一次调用配对 | [delegation §5](https://apogee.gweb3networks.com/docs/auditors/spec/delegation#s5) |
| 只有退出行能写入 `HALT_PC`；凡是由电路族计算 `next_pc` 的地方，都将其约束为偶数 | [memory §5](https://apogee.gweb3networks.com/docs/auditors/spec/memory#s5)；[jump-branch-slt §5](https://apogee.gweb3networks.com/docs/auditors/spec/jump-branch-slt#s5) |
| 每个地址只有一个初始值：窗口规则 | [memory §3.5](https://apogee.gweb3networks.com/docs/auditors/spec/memory#s3-5)、[§9](https://apogee.gweb3networks.com/docs/auditors/spec/memory#s9) |
| 输入窗口与公开输出（journal）窗口存放的是陈述中的字节；公开输出没有初始列 | [public values §5](https://apogee.gweb3networks.com/docs/auditors/spec/public-values#s5) |
| 打开从密钥中取得设置承诺，从而绑定程序身份所承诺的表与映像 | [proof §5](https://apogee.gweb3networks.com/docs/auditors/spec/proof#s5)；[memory §6.2](https://apogee.gweb3networks.com/docs/auditors/spec/memory#s6-2) |
| 密钥中的电路就是注册表中的电路，其 SRS 摘要与仪式的 SRS 摘要进行比对 | [proof §3](https://apogee.gweb3networks.com/docs/auditors/spec/proof#s3)、[§7](https://apogee.gweb3networks.com/docs/auditors/spec/proof#s7) |
| 递归：由程序身份绑定的 tape、transcript 链、在被加权对象之后抽取的折叠权重、判定器的绑定线，以及仪式各轮的顺序 | [recursion §7](https://apogee.gweb3networks.com/docs/auditors/spec/recursion#s7)、[§8](https://apogee.gweb3networks.com/docs/auditors/spec/recursion#s8)、[§9](https://apogee.gweb3networks.com/docs/auditors/spec/recursion#s9) |

## 复现

CI 运行的所有内容都不需要仪式文件。证明真实分片的测试套件在各自的玩具 SRS 上运行，需要数十 GiB 内存，因此要按名称单独运行：

```sh
cargo test --workspace                                   # every unit, law and row suite
cargo run -p kat-gen && git diff --exit-code             # fixtures regenerate identically
cargo test --release -p prover --test <suite> -- --include-ignored --test-threads=1
#   acceptance, control, alu, mem, fills, block, streaming, keccak, recursion, public_io, revm
cargo test --release -p checker --test tamper -- --include-ignored --test-threads=1   # every tamper twin
cargo run -p checker -- laws <artifact>                  # Laws 1–4 and the lookup rules, independently
```

[验证实现](https://apogee.gweb3networks.com/docs/auditors/implementation-checks)说明了每个参照（oracle）和测试套件各自确立了什么，以及它们都没有确立什么。

## 报告发现

请将审计发现发送至 [admin@gweb3networks.com](mailto:admin@gweb3networks.com)，并附上规范章节或代码路径、所涉及的性质，以及在可能的情况下附上一个篡改孪生：一份按诚实证明者的方式证明、却能通过验证的伪造见证。
