参考文档 / ZLIB × LEAN
文档索引
导读、完整接口契约和证明细节共用同一套文档。原始内容在构建时读入，没有删去长推导或错误路径。
算法与接口
全部公开 API 契约 ↗形式化验证
inflate 与 deflate 的证明路线 ↗原有文档的完整目录
- 文档 ↗
README.md - 固定问题，可编辑证明 ↗
anti-cheating.md - 检查一个验证结论 ↗
checking/README.md - 已审阅的递归执行辅助声明 ↗
checking/compiler-helper-review.md - 公开契约审阅记录 ↗
checking/contract-review.md - 公开验证目标 ↗
checking/goals.md - 独立集成审阅 ↗
checking/pr-integration-review.md - 证明变异 ↗
checking/proof-mutants.md - 公开查询登记审阅 ↗
checking/query-registration-review.md - 本地证明登记检查 ↗
checking/registration-review.md - 可信运行时审阅记录 ↗
checking/runtime-review.md - 堆表审阅记录 ↗
checking/runtime-tables-review.md - 内存、翻译与外部输入输出语义 ↗
design/README.md - API 模型与具体实现边界 ↗
design/api-model.md - 从 C 到经过检查的定理 ↗
design/architecture.md - 外部 I/O：文件、格式化与局部存储 ↗
design/external-io.md - 保持行为不变地翻译 C ↗
design/translation.md - 调用者定义域与表示限制 ↗
deviations.md - 历史证据登记 ↗
findings.md - 2. 重复、符号与位 ↗
guide/encoding.md - 6. 选择应用接口 ↗
guide/interfaces.md - 1. 一次完整的压缩与解压任务 ↗
guide/round-trip.md - 5. 复用、检查点与受控变更 ↗
guide/state-operations.md - 3. 流的暂停与继续 ↗
guide/streaming.md - 4. 一个 DEFLATE 主体，三条格式路径 ↗
guide/wrappers.md - 理解并证明 zlib ↗
overview.md - 证明进度与剩余工作 ↗
progress.md - 实现证明参考 ↗
proof/README.md - Adler-32：有界求和与模运算细化 ↗
proof/adler32.md - 缓冲区工具与输出界限 ↗
proof/buffers.md - 回调解码：所有权与有限输入 ↗
proof/callbacks.md - CRC-32：字节范围、交织与多项式含义 ↗
proof/crc32.md - 流式压缩：窗口、链与生命周期 ↗
proof/deflate.md - Gzip 文件：源代码流程、所有权与清理 ↗
proof/gzip.md - 快速解码：余量、历史与源比特 ↗
proof/inffast.md - 流式解码：模式、历史与调用组合 ↗
proof/inflate.md - 解码表：从码长到已初始化表项 ↗
proof/inftrees.md - 证明一个函数 ↗
proof/method.md - 早期论证与参考来源 ↗
proof/references.md - 树与块输出：界限、码字及共用存储 ↗
proof/trees.md - 工具函数：分配与常量查询 ↗
proof/zutil.md - 运行时结构：对象堆上的 zlib 结构体 ↗
runtime-schema.md - 规范与证明目标 ↗
spec/README.md - zlib API 手册 ↗
spec/api/README.md - 校验和 ↗
spec/api/checksums.md - 契约的结构与范围 ↗
spec/api/contracts.md - 流式压缩 ↗
spec/api/deflate-stream.md - Gzip 文件 ↗
spec/api/gz-file.md - 回调解压 ↗
spec/api/inflate-back.md - 流式解压 ↗
spec/api/inflate-stream.md - 共享流规则 ↗
spec/api/streams.md - 缓冲区工具与库信息 ↗
spec/api/utility.md - 数据格式 ↗
spec/format/README.md - Lean 中的格式模型 ↗
spec/format/model.md - 输入配置与覆盖颜色 ↗
spec/input-configurations.md - 内部调用处的证明义务 ↗
spec/internal-contracts.md - 已接受的平台假设 ↗
spec/platform.md - 安全性主张与调用者义务 ↗
spec/safety.md - 内核检查与可信边界 ↗
trusted-base.md