理解并证明 zlib
5af3b71ac52d2f3f · 对应提交的原文 ↗先跟随一次完整任务，再逐层展开需要的机制。每章都把实际操作、例子和由此产生的证明义务放在一起讲。 页面顶部的语言菜单可在同一页切换 简体中文／English。
目录
阅读主线
| 章节 | 通过例子理解什么 |
|---|---|
| 1. 一次完整任务 | 原始字节 → 压缩字节 → 还原字节，以及创建、处理和释放。 |
| 2. 重复、编码与数据块 | 历史引用的重叠复制、Huffman 编码和数据块选择。 |
| 3. 流式处理 | 缓冲区耗尽时如何保留位和历史，再准确继续。 |
| 4. 格式与完整性检查 | 共用的 DEFLATE 主体、包装条件和尾部校验。 |
| 5. 状态操作 | 用 Reset 开始新任务，用 Copy 保存检查点，以及字典和刷新。 |
| 6. 应用接口 | 整块缓冲区、回调、gzip 文件与逻辑位置跳转（Seek）。 |
需要精确条件或 C 层面的论证时，再沿章内链接下钻。 规范定义必须满足的行为；实现证明参考按 C 组件给出技术推导。 它们与图解例子回答不同的问题。审阅记录收在“检查与验收”下，不放进入门阅读主线。
共用证明规则
范围
起点是默认 x86_64 Linux 构建与默认输入。更广的嵌套范围统一定义在输入配置。
例子选择具体运行，不会缩小公开目标的定义域。接受的平台前提包括：每个被表示的字节对象少于 2^63 字节；这不限制整个流的总长度。
安全规范统一规定 UB、帧性质、终止和资源义务。
可信基础与偏离记录统一记录模型限制。
论证
这里的“不变量”是每次继续调用前都必须成立的一组状态事实。例如，解压器保存的历史范围必须与已经恢复的字节一致，窗口指针也必须仍指向有效存储。初始化先建立这些事实；后续调用使用它们并重新建立它们；结束调用再释放相应资源。
对象是固定版本的 C 加上已登记补丁，并逐语句翻译。各章按执行步骤说明算法事实、表示不变量和相应证明义务。 初始化必须建立状态不变量与所有权。每次实际调用都要推出辅助函数的前提，并在返回的堆上保持所需性质；End 要交代资源释放。 被调用函数的契约必须是关于该函数的已证明定理。顶层定义域还需要具体见证。
共用证明方法对合法调用历史做归纳，把这些步骤连接起来，并将实际字节与独立格式含义对应。 各章只在相关例子处解释该机制特有的不变量。
证据
检查精确命题、调用者定义域与返回状态。局部分支引理或无堆模型定理不能独自证明整个公开 API。
早期的 C1–C7 标签指向 API 模型目标；具体执行仍需自己的细化论证。
有限差分运行只能核对例子，不能证明全称命题。检查指南定义指定提交上的验收要求。
只有进度页记录当前证据、完整目标依赖图与剩余工作。