mbrotli 与 mzstd 开始在 Lean 4 中形式化验证符合 RFC 7932 和 RFC 8878

为什么我们开始在 Lean 4 中针对 RFC 7932 和 RFC 8878 证明 mbrotli 与 mzstd 的正确性，Charon 和 Aeneas 如何将证明与 Rust 代码关联起来，目前已经证明了什么，以及在解码器整体得到验证之前还剩下哪些工作。

mbrotli 和 mzstd 现在在 Lean 4 中带有机器检查的证明，表明它们的部分代码遵循 RFC 7932 和 RFC 8878。它们还不是经过验证的编解码器，这篇文章也不是在宣布它们已经是。文章涵盖了我们为什么走这条路、证明如何与 Rust 代码关联、最初几天已经证明了什么，以及还剩下什么。

两个 crate 都承诺写出与它们的 C 参考实现相同的字节：Google Brotli 1.2.0 在质量 0–11 下，以及 zstd 1.5.7 在每个级别下。我们为守住这个承诺所构建的一切都是与 C 进行对比：

这很好地回答了两个问题：“mbrotli 是否做了 Google Brotli 所做的事？”以及“它会不会破坏内存？”。它没有回答第三个问题：“它是否做了 RFC 所说的事？”。差分测试把 C 库当作预言机。当预言机正确时，测试能抓住我们的错误。当预言机错误时，测试要么沉默，要么把我们正确的行为报告为 bug。

10 月 24 日，我们写到了 CVE-2026-111497，这是 C 版 Brotli 解码器中的一个越界写入。其根因是一个格式 bug：在 RFC 7932 下，一个只有单一块类型的类别其块计数为 16,777,216，需要更多块的流是无效的，而 C 解码器的快速路径忽略了这个失败，带着块切换从未建立的状态继续执行。mbrotli 在 CVE 意义上不受影响：安全 Rust 无法写出缓冲区之外。但当我们检查时，mbrotli 0.5.16 在同一处也偏离了 RFC。它把这个块计数的起点设为 u64::MAX，因此 RFC 判定为无效的流被无错误地解码了。Rust 把一个内存安全 bug 变成了一个“接受了本应拒绝的内容”的 bug，这更好，但仍然是 bug，而且与 C 库的任何对比都不可能标记出它，因为 C 库在那里也错了。mbrotli 0.5.17 修复了它。

内存安全和与 C 的一致性都是必要的。但它们并不等同于遵循规范，而对于一个读取不可信输入的解码器来说，规范才是关键。

我们想要第二个独立的答案：由机器读取的 RFC 本身，以及一个证明 Rust 代码计算出了它所规定内容的证明。具体来说，每个已证明的条目最多会得到三类陈述：

规范始终是 RFC，绝不是 C 库。与 C 的字节一致性留在它该在的地方：差分测试中。

关于代码的手写模型的证明，证明的是关于模型的事情。我们想要关于实际发布代码的证明，而不对它进行标注，也不手工维护一份同步的第二副本。两个仓库中的流水线是相同的：

scripts/extract_lean.py 固定 Aeneas 版本和已翻译函数的列表。在 CI 中，ci-lean.yml 重新生成翻译，如果与已提交的版本不同则失败，然后构建证明。因此，对 Rust 代码的更改要么不影响翻译，要么强制重新完成证明。我们通过变异检查了这种耦合：把 mbrotli 的 short_window_distance 中的 - 4 改成 - 5，或把 mzstd 的两字节 Frame_Content_Size 中的 + 256 改成 + 255，都会使漂移检查失败，并且在重新生成之后，相应的定理不再能证明。

下面是一个函数的示例。mzstd 的编码器在每个序列之后用从 zstd 移植的代码更新它的三个重复偏移：

pub(crate) const fn update_rep(rep: &mut [u32; REP_NUM], off_base: u32, ll0: bool) { if off_base > REP_NUM as u32 { rep[2] = rep[1]; rep[1] = rep[0]; rep[0] = offbase_to_offset(off_base); } else { let rep_code = off_base - 1 + ll0 as u32; if rep_code > 0 { let current = if rep_code == REP_NUM as u32 { rep[0].wrapping_sub(1) } else { rep[rep_code as usize] }; rep[2] = if rep_code >= 2 { rep[1] } else { rep[2] }; rep[1] = rep[0]; rep[0] = current;

关于其 Aeneas 翻译的定理说，对于每个偏移值和字面量长度的两种情况，结果都是 updateRepeats，即 RFC 8878 第 3.1.1.5 节的规则在 Rfc.lean 中的转写：

theorem update_rep.spec (rep : Std.Array U32 3#usize) (off_base : U32) (ll0 : Bool) (h1 : 1 ≤ off_base.val) (hpos : ll0 = true → off_base.val = 3 → 1 ≤ rep[0]!.val) : update_rep rep off_base ll0 ⦃ (r : Std.Array U32 3#usize) => repeats r = updateRepeats (repeats rep) off_base.val ll0 ⦄

唯一被排除的输入是对为零的第一个重复偏移做递减，没有任何流会到达这种情况。把 rep_code >= 2 改成 rep_code > 2 会破坏这个证明。

mzstd 帧头的解码器侧则完全没有前置条件：FrameHeader.parse.spec 对每个字节串都成立。解析器恰好在 RFC 的解读拒绝这些字节时返回错误，否则返回 RFC 的字段，因此它在任何输入上都不会 panic。

只有当以下条件成立时，这里的定理才是关于 Rust 代码的陈述：

有限事实，例如 mbrotli 的长度码合并器的全部 1,152 个输入，由 decide +kernel 检查，Lean 内核自己对其进行求值。没有任何东西依赖对 Rust 代码的手写重述。

第一批证明于 2026 年 10 月 25 日进入 mbrotli（#13），同样的设置第二天被移植到了 mzstd。

目前已验证的函数中没有发现 bug：它们很小，并且被差分测试很好地覆盖，这对于第一层来说是意料之中的。尽管如此，还是有两件事浮现出来。

RFC 本身也不完美。RFC 8878 印刷的表 18（重复偏移表）最后两行与其自身正文不一致。当前的 Zstandard 格式文档把两者都纠正了；我们的转写遵循正文，Rfc.lean 的自检使用纠正后的行。一个对照规范自身示例进行自检的转写，在第一次运行中就能发现这类问题。

代码必须是可翻译的。Aeneas 并不能处理每一种 Rust 构造，因此有几个 mzstd 函数在不改变其计算结果的前提下被重构了：

（原文较长，此处译出前 6000 字，完整内容请点「打开原文」。）