Lean中快速的DEFLATE压缩

# 为什么 Lean 比 Rust 更快 — kim@lean 来源：https://kim-em.github.io/blog/2026-7-24-why-lean-is-faster-than-rust/ kim@lean:~$cat posts/2026·07·24\.md 2026·07·24\[性能\]\[lean\] 我说 Lean 比 Rust 更快，这听起来简直是在开玩笑吧？ 让我给你看点东西： `` # silesia.tar: 212 MB 标准测试集。每个工具均以 level 6 压缩， # 并输出结果大小（字节）；`time` 报告挂钟时间。 $ time deflate-rust silesia.tar # miniz_oxide（纯 Rust，无 'unsafe'） 68112144 real 0m5.78s $ time deflate-lean silesia.tar # lean-zip 67944712 real 0m4.97s `` 这到底是怎么回事？这是`lean\-zip` (https://github.com/kim-em/lean-zip) 实现的`DEFLATE` (https://www.rfc-editor.org/rfc/rfc1951) 压缩算法，对标准`silesia` (https://github.com/MiloszKrajewski/SilesiaCorpus) 压缩基准测试集进行压缩，结果比标准的纯 Rust 实现`miniz\_oxide` (https://github.com/Frommi/miniz_oxide)**更快**且**更好**。 这怎么可能？秘密在于： ``/\-\- Unified DEFLATE roundtrip: inflating what we deflate returns the input exactly\. \-/ theorem inflate\_deflateRaw \(data : ByteArray\) \(level : UInt8\) \(maxOutputSize : Nat\) \(hsize : data\.size ≤ maxOutputSize\) : inflate \(deflateRaw data level\) maxOutputSize = \.ok data := Zip\.Native\.Deflate\.inflate\_deflateRaw data level maxOutputSize hsize`` Lean 库不仅经过测试和验证，还经过**证明**是正确的。这使得我们可以放心地让 AI 对代码进行优化，并要求每当实现发生实质性变化时，它们必须更新证明。这种信心让我们能够以在其他语言中不可想象的方式，让 AI 自主工作。 这个过程产生的结果令人震惊。 lean-zip 与 miniz_oxide 的优化历史动画 这些图表展示了“帕累托前沿”，描述了`lean\-zip`和`miniz\_oxide`实现中压缩率与吞吐量的权衡关系。像所有 DEFLATE 实现一样，两个库都有一个可调参数（“level”），它以降低吞吐量为代价换取更好的压缩。这些图表的设置是：越靠左压缩越好，越靠上吞吐量越高。绿色线条显示的是使用`miniz\_oxide`对`silesia 测试集`进行压缩时，遍历各个 level 的结果。红色动画线条显示的是`lean\-zip`在整个自主优化过程中（结合使用 Claude 和 Codex 代理）得到的结果。 （注意，这些图表测量的是`silesia\.tar`中各个文件压缩率的几何平均值，所以与我们第一次的测量略有不同。） 我们没有接近`miniz\_oxide`的 L1（最低压缩、最快吞吐量设置）那么快。但在 L2 上，我们现在完全胜出：压缩率略好，吞吐量高出 20%。对于`miniz\_oxide`的 L3 和 L4，在对应的压缩率下，我们稍慢（最差的是 L4，慢 10%），在 L5 上我们打平。然后对于 L6-L9，`miniz\_oxide`被完全压制：`lean\-zip`能够压缩得更快更好。本文开头的数字取自 L6，这是 zip 算法的典型默认设置。在`miniz\_oxide`的 L9 上，我们的速度几乎翻倍。 我仍然觉得这难以置信！ 你可能会说，“当然，没人试过用同样的方法在这些代理上运行`miniz\_oxide`并尝试优化它”。这当然有道理：我相信我们可以改进性能！但我们能信任吗？AI 是否引入了当前测试套件未发现的细微错误？我们必须仔细审计和审查它建议的所有内容。但在 Lean 这边，我们只是耸耸肩，说“`inflate \(deflateRaw data level\) = \.ok data` 仍然成立，所以应该没问题”。 为了完整性，这里展示了一张帕累托前沿图，比较了其他几个 DEFLATE 库： 帕累托前沿：lean-zip 对比 zlib、miniz_oxide、zlib-rs、zlib-ng、libdeflate、Go、JS、Zig 和 OCaml `lean\-zip` 肯定不是这里最好的：`libdeflate` 毫无疑问地碾压了我们（这并不意外，因为它是一个经过精心调优的实现，使用了特定架构的 SIMD，而我们在 Lean 中无法做到）。`zlib\-ng` 和 `zlib\-rs` 在它们曲线覆盖的大部分范围内都比我们快，但在深度压缩区域就不再如此了：它们的 L9 正好落在 `lean\-zip` 在 L7 达到的压缩率上，而我们到达那里的速度比两者都快（比 `zlib\-rs` 快一点，比 `zlib\-ng` 快 11%）。`zlib\-ng` 是经过优化的 C 语言实现；`zlib\-rs` 是一个内存安全的 Rust 实现，大量基于 zlib-ng，内部包含一些谨慎使用的 unsafe。 与其他库相比，我们有竞争力，甚至更好。我们完全压制了 OCaml、JavaScript 和 `zlib` C 参考实现，在低 level 上输给 Go、纯 Rust（`miniz\_oxide`）和 Zig，但在高 level 上胜出。 也有一些值得考虑的注意事项： - Lean 实现的内存消耗高于 `miniz\_oxide`。 - 存在一些信任缺口，因为我们使用 Lean 的 `@[extern]` 注解来提供一些低级函数（例如对 `ByteArray` 进行字大小读取），这些函数目前 Lean 运行时中缺失。我们正在推动 Lean 作为通用编程语言的成熟度，所以这些函数很可能很快就会添加到运行时中。 - 证明我们的实现可以往返、生成有效的 DEFLATE 流并接受任何有效流，是一个良好的开端，但未解决其他有趣的问题，例如不存在侧信道或已验证的性能保证。 - 我们的解压实现仍然较慢：`miniz\_oxide` 的解压速度大约是 1.45 倍。 我并**不是**真的声称“Lean 比 Rust 更快”。坐下来用 Rust 产生一个高性能实现仍然比用 Lean 容易得多！这个实验仅仅表明： - 通过大量调优，用 Lean 编写的基本算法有可能与“快速”语言中的实现相竞争。 - 当你能够编写描述算法的定理时，这种努力可以愉快且令人惊讶地委托给 AI，从而允许在没有人工审查的情况下进行激进优化。 不过，我们能如此接近，这仍然值得深思！