kim-em/lean-zip

# lean-zip **一个在 Lean 4 中经过形式化验证的 zlib 实现。** [`lean-zip`](https://github.com/kim-em/lean-zip) 包含了一个纯 [Lean](https://lean-lang.org/) 的 DEFLATE 编码器和解码器，并且 Lean 的内核检查确认它们彼此互为逆运算。 我们已经证明，对于所有可能的输入，压缩都不会破坏您的数据， 并且该证明由 Lean 内核认证： ``` /-- Decompressing the output of `compress` returns the original data, for every input and every compression level. -/ theorem zlib_decompressSingle_compress (data : ByteArray) (level : UInt8) (maxOutputSize : Nat) (hsize : data.size ≤ maxOutputSize) : ZlibDecode.decompressSingle (ZlibEncode.compress data level) maxOutputSize = .ok data ``` 该定理依赖于关于 DEFLATE 算法的更低层定理， 即 `inflate (deflateRaw data level) = .ok data`，以及位于 [`Zip/Spec/`](Zip/Spec) 中约 32k 行证明代码里的超过 1,100 个定理。这里没有使用任何 `sorry`， 并且这些证明在每次提交时都会被从头重新检查。 令人惊讶的是，无论是实现还是验证，完全都是由几乎没有人工干预的 AI 编写的。 大部分的监督仅仅是通过一份 [`PLAN.md`](PLAN.md) 文件完成的， 工作者们在此基础上不断迭代，除了 Github 仓库之外没有任何其他状态管理。 （lean-zip 还附带了指向系统 zlib 的轻量级 FFI 绑定，供您在只想直接使用 C 库时使用，此外还包含纯 Lean 实现的 tar 和 ZIP 归档处理。请跳转至 [使用说明](#using-it)。） ## 验证赋能性能优化 这里是其中最有趣的部分。  *[Silesia](https://sun.aei.polsl.pl/~sdeor/index.php?page=silesia) 语料库。 x = 压缩率（← 越小越好），y = 吞吐量 （MB/s，对数刻度）；每个编解码器的不同级别通过其*可达混合边界*相连—— 即通过混合两个相邻级别所能达到的压缩率/速度点—— 因此越靠左上方表现越好，并且在相同压缩率下进行比较是客观诚实的（在 此对数轴上，直线线段会夸大实际可达的速度；详见 [`bench/README.md`](bench/README.md)）。参考曲线固定在 当前的仪表板上；红色曲线代表纯 Lean 编解码器**重演项目 git 历史中的** **每一次仪表板刷新**，每帧对应一次提交，并带有每个级别的微弱轨迹。 完整的仪表板（解码基准测试、单文件热力图及测试方法论）位于 [`bench/`](bench/README.md) 中，包括 [此图表的静态版本](bench/graphs/silesia_compress_pareto.svg）。* 一旦正确性成为一条*定理*，您就可以大胆激进地进行优化。 添加惰性匹配、引入基于成本模型的最优解析、在符号统计特征发生偏移时分割数据块、 将匹配器的链状态拆箱为扁平数组、用一个干净的高阶函数替换按字比较器，然后义务等式 `inflate (deflate x) = x` 要么依然成立，要么构建就会报错。一项优化*不可能* 悄无声息地牺牲正确性，因为在这里正确性并不是一个只对部分输入进行采样的测试套件；它是 一个关于**所有**输入的断言，并由内核强制执行。 这使得将优化工作交给机器变得安全。lean-zip 的很大一部分， 包括该图表背后几乎所有关于性能优化的工作，都是 由自主工作的编程代理完成的：每个代理认领一个 issue，在 自己的 git worktree 中工作，发起 pull request，并且只有当往返证明 依然成立时，该 PR 才能被合并。证明就是那个单向棘轮。 而且这确实奏效。在上图中，我们可以看到纯 Lean 编解码器（`native`）的性能。 请注意，y 轴是对数刻度，因此垂直方向的差距代表一个*乘积性*的倍速差异。 在相同的压缩率下进行比较，Lean 的实现： - 彻底**击败了**纯 OCaml 的 [`decompress`](https://github.com/mirage/decompress) 库：在其能达到的任何压缩率下速度快 2-4 倍，并且能够达到 OCaml 编码器无法达到的压缩率； - 已经**追平了 JS 的 [`fflate`](https://github.com/101arrowz/fflate)**：在 fflate 能够达到的任何 压缩率下，native 版本的速度都在其百分之几的误差范围内，并在 fflate 最高密度的设置下 进一步拉开速度优势——同时压缩得更彻底； - **在 Rust 的 miniz_oxide 和 C 的 zlib 默认级别附近运行，差距约在 ~20% 以内**，而在它们最快和最高密度的极端设置下差距扩大到约 1.4–1.7 倍； 最优解析级别 9/10 能够达到 zlib、zlib-rs、zlib-ng、 miniz_oxide、Go、Zig 和 fflate 在任何设置下都无法产生的压缩率； - 正如对该格式的预期一样，落后于手工调优的 **C + SIMD** 性能上限 3.5 到 11 倍。 该编解码器最初的性能远低于图表上的其他所有实现—— 上面的动画以每次仪表板刷新为一帧，重演了这一攀升过程。这一差距的缩小并非源于某个人类巧妙的洞察，而是通过一系列漫长、细小且各自经过验证的步骤。 这正是 Gwern 提出的 ["Lean 软件缩放定律"](https://gwern.net/lean-scaling) 背后的核心赌注： 形式化可验证的语言可能初始基线较差，但具有更好的扩展性， 因为经过验证的代码是自动化优化能够安全积累的基石。 作者坦然承认自己是性能优化方面的业余爱好者，这其实也正是关键所在：她不需要成为专家，只需要保证证明一直保持 绿色（通过）状态。如果您知道如何让 DEFLATE 跑得更快，这些证明正等着 捕捉您的错误；非常欢迎您的贡献。 ## 使用说明 将以下内容添加到您的 `lakefile.lean` 中： ``` require "kim-em" / "lean-zip" ``` ### 压缩 ``` import Zip -- Zlib format let compressed ← Zlib.compress data let original ← Zlib.decompress compressed -- Gzip format (compatible with gzip/gunzip) let gzipped ← Gzip.compress data (level := 6) let original ← Gzip.decompress gzipped -- Raw deflate (no header/trailer, used internally by ZIP) let deflated ← RawDeflate.compress data let original ← RawDeflate.decompress deflated ``` 上述高级的 `Zlib`/`Gzip`/`RawDeflate` 入口点通过 FFI 绑定了系统 zlib：这是快速且无处不在的基线。证明和基准测试中所涉及的经过验证的纯 Lean 编解码器位于 [`Zip.Native`](Zip/Native) 下（使用 `Zip.Native.Deflate.deflateRaw` 进行压缩， 使用 `Zip.Native.InflateBuf.inflate` 进行解压）；它完全不需要任何 C 库。 ### 流式传输 对于太大而无法装入内存的数据： ``` -- Stream between IO.FS.Streams (64KB chunks, bounded memory) Gzip.compressStream inputStream outputStream (level := 6) Gzip.decompressStream inputStream outputStream -- File helpers let gzPath ← Gzip.compressFile "/path/to/file" -- writes /path/to/file.gz let outPath ← Gzip.decompressFile "/path/to/file.gz" -- writes /path/to/file ``` ### 底层流式状态 ``` let state ← Gzip.DeflateState.new (level := 6) let compressed ← state.push chunk1 let compressed2 ← state.push chunk2 let final ← state.finish -- must call exactly once ``` ### 校验和 ``` let crc ← Checksum.crc32 0 data -- CRC-32 let adler ← Checksum.adler32 1 data -- Adler-32 -- Incremental: pass previous result as init let crc2 ← Checksum.crc32 crc moreData ``` CRC-32 和 Adler-32 同样在 [`Zip.Native`](Zip/Native) 中有经过验证的纯 Lean 实现， 并且每一个都证明了与其规范相等。 ### Tar 归档 ``` -- Create .tar.gz from a directory (streaming, bounded memory) Tar.createTarGz "/tmp/archive.tar.gz" "/path/to/dir" -- Extract .tar.gz Tar.extractTarGz "/tmp/archive.tar.gz" "/tmp/output" -- Create/extract raw .tar via IO.FS.Stream Tar.createFromDir stream dir Tar.extract stream outDir -- List entries without extracting let entries ← Tar.list stream ``` Tar 支持 UStar、PAX 扩展头（用于长路径、大文件、UTF-8）以及 GNU 长 名称/链接扩展。在创建归档时，超出 UStar 限制的路径会自动使用 PAX 头进行编码。 ### ZIP 归档 ``` -- Create from explicit file list Archive.create "/tmp/archive.zip" #[ ("name-in-zip.txt", "/path/on/disk.txt"), ("subdir/file.bin", "/other/file.bin") ] -- Create from directory Archive.createFromDir "/tmp/archive.zip" "/path/to/dir" -- Extract all files Archive.extract "/tmp/archive.zip" "/tmp/output" -- Extract a single file by name let data ← Archive.extractFile "/tmp/archive.zip" "name-in-zip.txt" -- List entries let entries ← Archive.list "/tmp/archive.zip" ``` ZIP 支持 stored（方法 0）和 deflated（方法 8）条目，并带有自动方法选择、CRC32 验证，以及针对超过 4GB 大小或包含超过 65535 个条目的归档的 ZIP64 扩展。 有关 Zstandard (zstd) 的支持，请参见 [lean-zstd](https://github.com/kim-em/lean-zstd)。 ## 组织结构 - [`Zip/`](Zip)：FFI 包装器和公共 API - [`Zip/Native/`](Zip/Native)：纯 Lean 实现（无 FFI） - [`Zip/Spec/`](Zip/Spec)：形式化规范和正确性证明 - [`ZipTest/`](ZipTest)：逐模块的合规性测试（native 与 FFI 对比） - [`bench/`](bench/README.md)：基准测试仪表板和方法论 每个源文件的开头都有一个模块文档字符串来描述其用途。共享的 实用工具（Binary、Handle、BitReader）位于 [lean-zip-common](https://github.com/kim-em/lean-zip-common) 中。 这些规范旨在超越同义反复。在可能的情况下，它们刻画了独立于实现的数学属性（例如用 `crc32 a` 和 `crc32 b` 来表示 `crc32 (a ++ b)`、Huffman 编码的前缀无关性与克拉夫特不等式、编解码器的可逆性），而不是仅仅断言两段代码一致。 上面的往返定理是核心基石：它表明编码器和解码器是真正的互逆运算，而不是说它们只是照抄自同一个 RFC 标准。 ## 环境要求 - Lean 4（已测试 v4.20.0 至 v4.30.0 版本） - zlib 开发头文件（`zlib-dev`、`zlib1g-dev` 或等效文件），用于 FFI 基准测试 - `pkg-config`（用于在 NixOS 和类似系统上发现头文件） - 可选的比较器工具链（`cargo`、`libdeflate`、`zopfli`、Go、Node、 Zig、OCaml）仅在基准测试套件中使用；缺失的工具链会自动降级。请参阅 [BENCH.md](BENCH.md)。 在 NixOS（或者任何 zlib 不在默认库路径的系统）上，可以使用 `shell.nix` 来提供 C 语言依赖： ``` nix-shell # then run lake build, lake exe test, etc. inside the shell ``` 或者使用 [direnv](https://direnv.net/) 进行自动激活（只需执行一次 `direnv allow`； 之后环境会在 `cd` 进入目录时自动激活）。您也可以手动设置 `ZLIB_CFLAGS` 以指向头文件。 ## 构建和测试 ``` lake build # library + test executable lake build test && .lake/build/bin/test # run all tests ``` ## 基准测试 位于 [`bench/`](bench/README.md) 中已提交的仪表板是由 单条 `bench/run.sh` 命令重新生成的。为了进行临时测量，还提供了一个可与 [hyperfine](https://github.com/sharkdp/hyperfine) 配合使用的驱动程序： ``` lake -d bench build bench hyperfine 'lake -d bench exe bench inflate 1048576 prng 6' ``` 操作包括：`inflate`、`deflate`、`gzip`、`zlib`、`crc32`、`adler32` 及其对应的 FFI 版本。请参阅 `lake -d bench exe bench` 获取完整列表。 ## 已知局限性 - **解压时存在 TOCTOU 问题**：解压过程会验证每一个归档路径（拒绝 `..` 组件、绝对路径和不安全的 symlink 目标），但它是在不同的步骤中分别 创建父目录和写入文件的。拥有对输出目录树并发写入权限的本地攻击者可能会在这个时间窗口内用一个 symlink 替换 刚创建的目录，并将写入操作重定向到目录之外。因此，这里的威胁模型范围很窄：它要求攻击者 在解压期间已经能够写入目标位置。要完全杜绝此问题，需要 在 C 语言中实现 `openat()`/`O_NOFOLLOW` 的组件遍历（目前尚未实现）。如果您将不受信任的归档文件解压到其他进程可以写入的位置， 请在您控制的私有目录中进行暂存解压。 - **原始流式处理原语是无限制的**：全缓冲区解压和 流式管道辅助函数（`Gzip.decompressStream`、`RawDeflate.decompressStream`） 强制执行 `maxDecompressedSize` 上限（默认为 1 GiB；传入 `0` 可选择无限制 模式），但底层不透明的 FFI 原语 `InflateState.push` 和 `InflateState.finish` 不接受任何限制，因此直接基于它们进行构建的调用者必须自行跟踪总输出量。 ## 许可证 Apache-2.0。请参阅 [LICENSE](LICENSE)。

标签：DEFLATE, Lean, zlib, 代码生成, 压缩算法, 形式化验证, 渗透测试工具