# 可靠性地图

> 一份通过验证的证明所做出的每一项断言、支撑它的论证，以及规范中阐述该论证并说明其成立理由的确切章节。

一个通过验证的块（block）确立的是一句话：*具有此身份的程序，在其映像上从入口 pc 启动，以此公开输入和某份证明者提示（advice）逐条指令执行，直至以此状态调用 `EXIT`，并已写出此公开输出（journal）。* 本页把这句话拆成组成它的各项断言，并把每一项对应到证明它的论证。

## 程序

| 断言 | 论证 | 规范 |
| --- | --- | --- |
| 密钥描述的是已登记的程序 | 加载密钥时，根据其自身的配置、入口 pc 和设置承诺重新计算程序身份；验证者将其与自己持有的副本比对 | [proof §7.2](https://apogee.gweb3networks.com/docs/auditors/spec/proof#s7-2)、[program §8](https://apogee.gweb3networks.com/docs/auditors/spec/program#s8) |
| 证明读取的表就是程序身份所承诺的表 | 每个分片的批量打开都从密钥中取得设置承诺 | [proof §5](https://apogee.gweb3networks.com/docs/auditors/spec/proof#s5) |
| 每个被执行的行，都是程序在该行 pc 处的指令 | 解码器查找：以该行自身读到的 pc 为键，查询一张有效行为 one-hot、填充行为 `−1` 的表 | [lookup §10](https://apogee.gweb3networks.com/docs/auditors/spec/lookup#s10)、[program §5](https://apogee.gweb3networks.com/docs/auditors/spec/program#s5)、[§6](https://apogee.gweb3networks.com/docs/auditors/spec/program#s6) |
| 内存从程序映像开始 | `INIT_TEARDOWN` 的初始化列是程序身份所承诺的设置列；没有任何来自文件的字节位于窗口 0 之外 | [memory §6.2](https://apogee.gweb3networks.com/docs/auditors/spec/memory#s6-2)、[§3.4](https://apogee.gweb3networks.com/docs/auditors/spec/memory#s3-4) |
| 执行从入口 pc 开始 | pc 的初始元组使用密钥中的入口 pc，而它由程序身份绑定 | [memory §4.2](https://apogee.gweb3networks.com/docs/auditors/spec/memory#s4-2)、[§6.2](https://apogee.gweb3networks.com/docs/auditors/spec/memory#s6-2) |
| 电路是正确的电路 | 密钥中的电路必须在其高度上与验证者的注册表一致，并通过各项法则、内存规则和履行规则（discharge rule） | [proof §7.2](https://apogee.gweb3networks.com/docs/auditors/spec/proof#s7-2)、[circuits §1](https://apogee.gweb3networks.com/docs/auditors/spec/circuits#s1)、[gkr §4.2](https://apogee.gweb3networks.com/docs/auditors/spec/gkr#s4-2) |

## 每一行

| 断言 | 论证 | 规范 |
| --- | --- | --- |
| 每一行都遵循其指令 | 电路族的约束门（在每一行上均为零），以及各电路族的可靠性论证 | [add-sub §4](https://apogee.gweb3networks.com/docs/auditors/spec/add-sub#s4)、[jump-branch-slt §5](https://apogee.gweb3networks.com/docs/auditors/spec/jump-branch-slt#s5)、[shift-bitwise §5](https://apogee.gweb3networks.com/docs/auditors/spec/shift-bitwise#s5)、[mul-div §5](https://apogee.gweb3networks.com/docs/auditors/spec/mul-div#s5)、[memory-ops §3–§6](https://apogee.gweb3networks.com/docs/auditors/spec/memory-ops#s3) |
| 每一行恰好发起其指令应有的查询 | 每个掩码都固定为 `m_pc` 乘以会发起该查询的那些 kind | [memory §2.1](https://apogee.gweb3networks.com/docs/auditors/spec/memory#s2-1) |
| `x0` 读写的都是 0 | x0 gadget 与写回 | [memory §2.4](https://apogee.gweb3networks.com/docs/auditors/spec/memory#s2-4) |
| 寄存器和 RAM 中的值都是字 | 每次寄存器写入都在其所在行上限定范围；执行电路族的每次 RAM 写入都是字；初始值都是字，证明者提示除外，而没有任何电路族依赖它 | [memory-ops §5](https://apogee.gweb3networks.com/docs/auditors/spec/memory-ops#s5) |
| 填充行不增加任何内存事件 | 填充行的每个掩码都是 0，因此它的叶子都是 1 | [memory §2.3](https://apogee.gweb3networks.com/docs/auditors/spec/memory#s2-3)、[gkr §4.3](https://apogee.gweb3networks.com/docs/auditors/spec/gkr#s4-3) |

## 内存与顺序

| 断言 | 论证 | 规范 |
| --- | --- | --- |
| 每次读取都返回最近一次写入 | 覆盖所有分片的单一读/写多重集，与寄存器及 pc 边界做一次核对 | [memory §4](https://apogee.gweb3networks.com/docs/auditors/spec/memory#s4)、[§9](https://apogee.gweb3networks.com/docs/auditors/spec/memory#s9) |
| 读取严格晚于它所消费的那次写入 | 每个查询的时间戳差由两个 19 位的 `TIMESTAMP` 块组成 | [memory §2.4](https://apogee.gweb3networks.com/docs/auditors/spec/memory#s2-4)、[§7](https://apogee.gweb3networks.com/docs/auditors/spec/memory#s7) |
| 每个地址恰好有一个初始值 | 窗口规则：统一的高度、互不相交的窗口、每个固定窗口各占一个分片 | [memory §3.5](https://apogee.gweb3networks.com/docs/auditors/spec/memory#s3-5)、[§9](https://apogee.gweb3networks.com/docs/auditors/spec/memory#s9) |
| 多重集无法靠一个环闭合 | 时间戳是有界路径上的整数：形成一个环需要超过 `2^215` 条边 | [memory §4.2](https://apogee.gweb3networks.com/docs/auditors/spec/memory#s4-2) |
| 各行按程序顺序构成一条从入口到出口的路径 | pc 是一个内存单元，写入它的时间戳至少比读取它的晚四个 | [memory §5](https://apogee.gweb3networks.com/docs/auditors/spec/memory#s5)、[§9](https://apogee.gweb3networks.com/docs/auditors/spec/memory#s9) |
| 执行在退出行结束 | `HALT_PC = 1` 是奇数；只有退出行写入它；`JUMP_BRANCH_SLT` 用范围检查确保其 `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)、[add-sub §4](https://apogee.gweb3networks.com/docs/auditors/spec/add-sub#s4) |
| 分片的时间窗口不提供任何额外保证 | 时间窗口只检查形状；顺序完全来自多重集 | [proof §8](https://apogee.gweb3networks.com/docs/auditors/spec/proof#s8) |

## 取值与查找

| 断言 | 论证 | 规范 |
| --- | --- | --- |
| 每个带门控的元组都是其表中的一行 | 每个通道一个 LogUp 恒等式，在 GKR 过程中由分式树求和；根的分子为 0，分母非零 | [lookup §1](https://apogee.gweb3networks.com/docs/auditors/spec/lookup#s1)、[§6](https://apogee.gweb3networks.com/docs/auditors/spec/lookup#s6)、[§8](https://apogee.gweb3networks.com/docs/auditors/spec/lookup#s8) |
| 选择子是布尔值 | 每个查找的选择子都由门列表 0 中的一个约束门以 `s − s²` 加以约束 | [lookup §2](https://apogee.gweb3networks.com/docs/auditors/spec/lookup#s2) |
| 查找只由它自己的子表应答 | 每个通道一个宽度、带 `+1` 偏移且互不相交的键范围，以及各电路族对其键的界 | [lookup §4](https://apogee.gweb3networks.com/docs/auditors/spec/lookup#s4)、[§9](https://apogee.gweb3networks.com/docs/auditors/spec/lookup#s9)、[§11](https://apogee.gweb3networks.com/docs/auditors/spec/lookup#s11) |
| 表就是预期的那些表 | 虚拟表是验证者的闭式表达式；通用表由 SRS 摘要绑定；解码表由程序身份绑定 | [lookup §3](https://apogee.gweb3networks.com/docs/auditors/spec/lookup#s3)、[§12](https://apogee.gweb3networks.com/docs/auditors/spec/lookup#s12) |
| 每个已声明的义务都得到履行 | 在组装时和每次加载密钥时检查的履行规则 | [lookup §11](https://apogee.gweb3networks.com/docs/auditors/spec/lookup#s11) |

## 公开值

| 断言 | 论证 | 规范 |
| --- | --- | --- |
| 输入窗口存放的是陈述中的输入 | 在 G7 固定这些字节之后，`PUBLIC_INPUT` 的初始列在一个随机点上等于输入的各个字 | [public values §5](https://apogee.gweb3networks.com/docs/auditors/spec/public-values#s5) |
| 公开输出就是客户程序（guest）的存储指令留下的内容 | `PUBLIC_OUTPUT` 的最终列等于公开输出的各个字；该窗口没有可供证明者填充的初始列 | [public values §5](https://apogee.gweb3networks.com/docs/auditors/spec/public-values#s5) |
| 退出状态就是 `x10` 的最终值 | 退出行写回它读到的 `a0`；验证者要求 `v_10` 等于陈述中的状态 | [add-sub §4](https://apogee.gweb3networks.com/docs/auditors/spec/add-sub#s4)、[memory §4.1](https://apogee.gweb3networks.com/docs/auditors/spec/memory#s4-1)、[proof §6](https://apogee.gweb3networks.com/docs/auditors/spec/proof#s6) |

## 委托

| 断言 | 论证 | 规范 |
| --- | --- | --- |
| 每个请求恰好执行一次 | 锚点：请求与调用在该委托类型自己的空间中，通过多重集一一配对 | [delegation §5](https://apogee.gweb3networks.com/docs/auditors/spec/delegation#s5) |
| 每次调用都计算其函数 | 各电路的可靠性论证，包括帧与规范性链（canonicity chain） | [delegation circuits §2–§7](https://apogee.gweb3networks.com/docs/auditors/spec/delegation-circuits#s2) |
| 多次调用的操作是其各步骤的复合 | RAM 粘合：在同一条内存历史上，每一步读取上一步的写入；顺序由调用方代码决定 | [delegation circuits §1](https://apogee.gweb3networks.com/docs/auditors/spec/delegation-circuits#s1) |

## 证明系统

| 断言 | 论证 | 规范 |
| --- | --- | --- |
| 分片的输出就是其电路在其已承诺列上的求值结果 | GKR 反向过程，每个挑战都在其所保护的内容之后抽取 | [gkr §5.4](https://apogee.gweb3networks.com/docs/auditors/spec/gkr#s5-4) |
| 声称的列值就是已承诺多项式的值 | 在该过程所得的点上做一次批量 Mercury 打开 | [mercury §5](https://apogee.gweb3networks.com/docs/auditors/spec/mercury#s5)、[§7](https://apogee.gweb3networks.com/docs/auditors/spec/mercury#s7) |
| 一个陈述只有在其全部分片都通过时才算验证通过 | 解码时和 `verify_block` 中的分片集合精确性检查；核对等式读取每个分片的根 | [proof §1.3](https://apogee.gweb3networks.com/docs/auditors/spec/proof#s1-3)、[§6](https://apogee.gweb3networks.com/docs/auditors/spec/proof#s6) |
| 挑战在其所保护的每个承诺之后产生 | 全局 transcript G1–G11 与分片 transcript S1–S6 | [proof §2](https://apogee.gweb3networks.com/docs/auditors/spec/proof#s2)、[§4](https://apogee.gweb3networks.com/docs/auditors/spec/proof#s4)、[transcript §3](https://apogee.gweb3networks.com/docs/auditors/spec/transcript#s3) |
| 可信设置就是该仪式的设置 | SRS 摘要，由验证者与仪式的 SRS 摘要比对 | [proof §3](https://apogee.gweb3networks.com/docs/auditors/spec/proof#s3)、[srs §3](https://apogee.gweb3networks.com/docs/auditors/spec/srs#s3) |

## 递归与合约

| 断言 | 论证 | 规范 |
| --- | --- | --- |
| 节点执行的恰好是基础验证者的检查 | 这些检查被编译成节点程序映像中的 tape，而该映像由节点程序的身份绑定 | [recursion §7](https://apogee.gweb3networks.com/docs/auditors/spec/recursion#s7)、[§8.1](https://apogee.gweb3networks.com/docs/auditors/spec/recursion#s8-1) |
| 递归树按顺序覆盖同一个基础陈述的每一个分片 | 跨节点的 transcript 链、相邻的分片区间，以及每个节点对其子节点的检查 | [recursion §8.1](https://apogee.gweb3networks.com/docs/auditors/spec/recursion#s8-1)、[§8.2](https://apogee.gweb3networks.com/docs/auditors/spec/recursion#s8-2) |
| 每个延迟打开都成立 | 每一个都以在其全部被加权对象之后抽取的权重折叠，最后由合约中的一次配对兑现 | [recursion §8.3](https://apogee.gweb3networks.com/docs/auditors/spec/recursion#s8-3)、[mercury §6](https://apogee.gweb3networks.com/docs/auditors/spec/mercury#s6) |
| 判定器绑定合约所持有的内容 | 绑定线在其挑战之前承诺；电路把公开输出约束到整个基础区间 | [recursion §9](https://apogee.gweb3networks.com/docs/auditors/spec/recursion#s9) |
| 判定器密钥没有已知的陷门 | 两阶段仪式，每轮有一位诚实贡献者，各轮按顺序进行 | [recursion §9](https://apogee.gweb3networks.com/docs/auditors/spec/recursion#s9)、[srs §7](https://apogee.gweb3networks.com/docs/auditors/spec/srs#s7) |

## 有意不作的断言

- **关于证明者提示的任何断言。** 证明者提示在设计上不绑定任何东西；由客户程序来检查它。
- **零知识。** 没有任何内容被盲化。
- **`sc.w` 的失败语义。** `sc.w` 总是成功；依赖其失败的程序不在断言范围之内。
- **陷入（trap）。** 发生陷入的运行根本没有证明。
- **证明者是正确的。** 证明者不受信任；只有验证者的 crate 承担可靠性。
- **仪式文件确实出自该仪式**，或者密钥的 `τ` 无人知晓：没有验证者自己对 SRS 摘要的比对，这两点都不在断言之内。