实现证明参考

压缩器把原文字节写成压缩流，解压器再把压缩流恢复为原文。这里要论证的是实际 C 执行如何完成这件事：每次读写都在许可范围内，暂停后能够继续，最终输出具有格式规定的含义。先沿一个组件理解算法，再沿同一组件的状态和内存变化阅读证明。

首次阅读请从图解导读开始。各章把算法、API 用法与相应证明义务放在一起说明。本节按 C 组件给出详细论证。

本指南按数学引理、实际内存执行和跨调用组合三层，解释翻译后的 C 如何满足 zlib 契约。每项论证标明所用前提、已建立的关系，以及实现连接中未完成的步骤。

进度是当前检查点和剩余工作的唯一记录。安全规范定义所声称的性质，检查指南说明接受结果所需的证据。下文保留历史证明名称，便于定位其源代码版本和适用前提。

选择阅读路线

本节中的“契约”描述调用者必须提供什么、函数返回后保证什么；“不变量”描述处理过程中始终要成立的状态关系；“帧性质”说明未获授权的内存保持不变；“所有权”记录哪些分配块应由当前流最终释放。四者分别回答调用、执行、隔离和清理的问题。

总体方法从证明一个函数开始，其中解释契约、不变量、帧性质、所有权和证明受阻时的诊断。随后按函数需要阅读 API 契约、格式规范和设计指南。

解压方向先读校验和与分配器，再读建表、快速解码器和主解码器。主解码器必须建立快速路径的进入条件；建表必须建立两种解码器都要使用的谓词。

压缩方向先读校验和与分配器，再读 deflate.c 的窗口和哈希链论证。trees.c 涵盖建树、位输出以及共享的输出／符号缓冲区。共享存储的覆盖界限也是内存安全的一部分。

唯一的目标图用实线表示实际证明引用、虚线表示 C 调用。证据索引区分这些引用、C 调用和规范依赖。调用者建立实际被调用函数的每项前置条件，无须假定其完整的通用参数 API 目标。输入范围指南也区分了压缩策略选择与由缓冲区驱动的解码快慢路径分派。

阅读组件页面

每页先指出源文件和契约术语，再解释函数所需的不变量与引理。所述界限依赖其旁边明确写出的前提。公开定理必须从初始化、先前调用和文档中的调用者要求取得这些前提，不能假定被调用函数契约，也不能丢弃合法 API 情形。

例如，一次历史复制既需要“距离不超过已有历史”的边界条件，也需要“历史中的那些字节正是此前恢复的内容”的数据关系。前者排除越界，后者说明复制结果正确。各组件页面会把这两类义务连接到同一段执行。

U1–U12 是安全要求的编号，F1–F9 是多个组件共用的结构事实，I-* 是内部函数契约。沿这些编号可以回到精确定义；每个未完成步骤会写明还缺少哪一段执行或组合论证。

区间 [a, b) 包含 a，不包含 b。可以构造指向数组末尾后一位置的指针，但不能读取该位置。无符号运算像 C 一样回绕。需要普通算术的证明必须说明回绕不会改变相关值。

本指南先针对默认 x86_64 Linux 构建。由该构建的位宽、表或分配器分支推出的界限，在其他配置下必须重新审查。信任边界和偏差记录仍属于每项结果的范围。

源代码对应与早期论证

各组件负责自己的 C 文件对应检查。共享的整数、对象和控制流规则保留在翻译语义中。gzip 外部世界只有一份外部 I/O 定义指南。参考附录保留早期定理族映射与历史实验，并说明其证据边界；当前结果与未完成工作仍统一见进度。