本周是六周计划的 Week 4，目标是双侧 Lean 4 生成与 Rocq/Coq 的可行性结论。两项都完成了，另外有一处方法上的改变和一次版本基线调整需要说明。
做了什么
Rust 侧：用 Charon + Aeneas 把 CKB-VM 的生产执行路径翻译成 Lean 4 定义，279 个定义、65 个 axiom，编译通过。提取入口是 ckb_vm::instructions::execute，common::add 出现在生成物里是因为生产路径到达它，不是我们点名它；指令的 PC 推进也在里面。
Sail 侧：固定配置下重新生成并编译通过，172 个文件、125 个 .olean。
Rocq spike：结论是 NO-GO，两半各自卡在不同位置，都不是 CKB-VM 代码的问题：
- Rust → Rocq：Aeneas 的 Rocq 支持库定义的
result被 Rocq 9.1 标准库的同名类型遮蔽，生成物在第一个 trait 声明就类型检查失败。同一份代码 Aeneas 的 Lean 后端处理得了。 - Sail → Rocq：生成的模型需要一个符号，最新发布的 Sail Rocq 支持库还没有提供。
按计划约定，NO-GO 不替代 Lean 主线，Lean 主线是通的。完整证据和四行最小复现已随仓库提交。
一处方法改变
原计划是先从生产路径抽出一个纯 ADD 函数、再让解释器调用它。实测发现不需要——Charon 能直接处理生产代码的形状（trait 泛型加可变引用）。因此这一轮没有修改任何一行 CKB-VM 生产代码。
这让结论更强而不是更弱：被翻译的就是运行时差分实际跑的那份代码，不存在"为了证明而做的重构是否改变了被验证对象"这个问题。连带的影响是，原计划 Week 5 里"向 CKB-VM 提交上游 PR 或 patch"这一项不再需要。
一次版本基线调整
给生成步骤加上真实编译检查之后，发现 Sail 侧的 Lean 模型其实编译不过。之前"生成可复现"的说法字面没错，但很容易被读成"生成物可用"——这两件事现在是分开检查的。
原因是 sail-riscv 需要一个只在 Sail 某个时间窗内存在的命名空间，而我们钉的是发布版。上游自己就用两个不同的 Sail 构建跑这两个目标，我们钉的组合他们从未测过。解决办法是把 sail-riscv 和 Sail 两个 pin 一起前移，Sail 改为按 commit 钉死的源码构建。
重要的是这次调整对既有证据的影响：物化配置hash、ISA 串、RVFI-DII 线格式、32/32 语料结果、395 个提交步、188 次 mutation 检测——全部未变。连之前用旧模拟器抓的实包，在新模拟器上也逐字节相同。变的只有模拟器二进制和 Sail 构建本身。
还没有的东西
生成物能编译不等于存在定理。状态桥接和 ADD 精化定理都还没做。已知的第一个障碍是两侧 Lean 工具链版本不同，同时引用两边的定理目前放不进任何一个工程——这是下周要先解决的。
另外三条已记录的限制：DefaultMachine 因为带 trait object，它到底层机器的委托在生成物里是 axiom 而非翻译出的函数体，ADD 定理必须把它写成前提；BEQ 用到的比较函数因为一个 Aeneas 库的缺口暂时无法翻译；Aeneas 支持库自身有 4 处 sorry，不过 ADD 路径用不到它们。这些都在仓库的语义缺口文档里。