# 验证实现

> 代码如何对照自身以外的东西接受检查：每一层的独立参照（oracle）、电路规则的第二套实现、证明伪造会被拒绝的篡改孪生，以及任何检查都没有覆盖的部分。

远地虚拟机的任何组件都不是对照整个系统的第二套实现来检查的。相反，每一层都有自己的参照（oracle），其选择原则是让检查与被检查的对象共享尽可能少的代码。

## 每一层及其参照

| 层 | 对照的参照 |
| --- | --- |
| 域、曲线、配对、MSM | 由 arkworks 生成的已知答案向量，测试也会实时运行 arkworks 加以对照；测试会重新推导各 crate 读取的每一个算术常量 |
| Poseidon2 与 transcript | `tools/transcript-ref`：使用 zkhash 轮常数的 Plonky3 Poseidon2，以及一份按规范转写的实现，与 Plonky3 的双工挑战器（duplex challenger）并行运行，每一次挤出都一致 |
| 解码器 | 所有低位为 `11` 的 `2^30` 个 32 位字，分别对照由 ISA 各表推导出的接受数量和一个独立的编码器；对已提交的客户程序（guest）运行 `llvm-objdump` |
| RVC 展开 | LLVM 自己的编码器，作用于一个分别以压缩和非压缩方式汇编的客户程序 |
| 以数据表示的电路 | `checker`：四条法则、查找规则和填充约定，不借用 `constraints` 的代码重新实现，只共享门内核 |
| 各电路族的门 | 行测试套件：用 Rust 自身的整数运算构造行，再经由 checker 求值；算术核心在缩小的字宽下穷举检查 |
| 内存论证与查找论证 | `checker` 中的原生求值器，在实际执行得到的执行轨迹上运行 |
| 执行器 | 其执行轨迹的自检以及上述论证；没有第二个执行器 |
| revm 客户程序 | 由未打补丁的上游 crate 构建的原生 revm |
| 无状态校验器 | CI 中原生运行 `tests-zkevm` v21.0.1 的一个已提交子集；手动原生运行整个发布版本，并通过客户程序二进制运行该子集；输入编码由 `tools/stateless-ref` 检查 |
| 判定器 | 原生检查证明，并在 revm 中执行合约 |

## 小位宽下的穷举检查

有几个算术核心把字宽写成参数，这样就能在小到可以枚举的位宽下，对所有输入检查编码：

- 比较 gadget 在 6 位下，遍历每一对操作数，有符号与无符号各一遍，恰好找到一个 `(lt, gap)`，即 ISA 规定的那个；
- `MUL_DIV` 的算术在 4 位下，遍历每个被除数、除数和每种除法，恰好只接受一个 `(q, r)`，即 RV32M 规定的那个；
- `MEM_SUBWORD` 的拼接在 4 位字下，对每个字、偏移和宽度，恰好只接受一个 `(high, sub, low)`。

## 电路规则，实现两遍

凡是构建制品或加载密钥的地方，都会运行 `CircuitArtifact::validate` 以及内存与查找的构造规则。`crates/checker` 用自己的代码把同样的规则再执行一遍，从不调用 `validate`，并且只通过 `gkr_verify::eval_gate` 对门求值；这是双方都视为语义权威的唯一内核。在 `validate` 比较规范化展开式的地方，它的校验器改为在采样点上求值来检查各项法则；它逐行而不是借助树来重新计算每个通道的和，并指出任何表行中都不存在的元组；它从事件日志而不是分片的行来重建执行电路族的内存列。

```sh
cargo run -p checker -- laws <artifact>       # Laws 1–4, then the lookup rules
cargo run -p checker -- padding <artifact>    # the padding contract
cargo run -p checker -- dump <artifact>       # the circuit, readably
```

## 篡改孪生

**篡改孪生**是一份完全按照诚实证明者的方式证明出来的伪造。篡改测试套件（`checker::TamperHarness`）在修改了见证单元或边界标量之后重新证明一个陈述：重新统计每个通道的重数，在一次全新的全局承诺阶段中重新承诺被修改的内存列，并重新证明每一个分片。然后它验证某个分片或整个块（block），并断言拒绝所属的类别：`Constraint`、带通道的 `Lookup`，或 `MemoryArgument`；或者断言一个不破坏任何东西的修改能够通过验证。

篡改孪生依赖于证明者不做任何检查，而这正是设计使然：伪造的见证能得到诚实证明者所能给出的最好证明，验证者必须以预期的类别拒绝它。该套件还包含针对委托锚点的伪造；在主网 mini-block 上，它展示了证明者提示（advice）规则的另一面：一个被篡改的证明者提示单元会被内存论证拒绝，而一个被一致地篡改的单元则能通过验证，因为证明者提示不绑定任何东西。

```sh
cargo test --release -p checker --test tamper -- --include-ignored --test-threads=1
```

## 可重新生成的测试数据

`kat-gen` 写出每一个已提交的已知答案向量、清单、电路制品和程序身份，每一项都附带 SHA-256，读取它的测试会固定这个值。CI 会重新生成默认分组以及两个参照实现（reference oracle）的数据，只要向量目录中出现任何差异就判定失败：

```sh
cargo run -p kat-gen && git diff --exit-code
```

客户程序 ELF 无法跨机器复现，因为 rustc 会把绝对路径嵌入 panic 位置字符串；同一台机器上的两次干净构建结果一致。因此客户程序 ELF 在一台机器上手动重新生成，CI 只重新生成由它们派生的内容。

## 任何检查都未覆盖的部分

- **没有第二个执行器。** 模拟器只对照其自身帧表的一份重述以及内存与查找论证来检查，而不是对照一个独立的 RISC-V 实现；这里也没有任何执行器会走委托 shim 的软件回退路径。
- **checker 不重复执行的构造规则**：内存构造规则、copower 规则，以及 `validate` 其余的构造规则（其中包括次数上限），都只执行一次。
- **证明者的正确性不受检查**，只通过证明真实分片的测试套件检查其完备性；这些套件在 CI 之外运行，因为每个都需要数十 GiB 内存。
- **Osaka 系列的无状态输入没有端到端参照。** 该测试发布版本只填充了 Amsterdam；Electra/Fulu 布局对照 `eth-act/ere-guests` 检查，区块头规则则对照两个主网区块检查。