参考文档 / ZLIB × LEAN
规范与证明目标
此页源文件快照 ·
75d616fc8a509c62 · 对应提交的原文 ↗这里是规范参考。阅读模型与证明指南前，先查阅本节。 它规定所需行为。可以先把它看作两份互相配合的承诺：API 契约说明一次调用可以读写什么、返回什么；格式契约说明交付的字节应当表示什么。安全性要求则贯穿两者，覆盖指针、内存、终止性和资源释放。 进度是当前状态与剩余工作的唯一记录。
建议阅读顺序
| 顺序 | 文档 | 回答的问题 |
|---|---|---|
| 1 | 平台假设 | 接受怎样的系统环境，包括每个对象的大小上界？ |
| 2 | 安全性 | UB、内存安全、终止性、帧性质和所有权分别要求什么？ |
| 3 | 输入配置 | 覆盖颜色描述哪个固定构建下、怎样嵌套的输入范围？ |
| 4 | API 契约 | 调用者可以传入什么，各入口必须返回或修改什么？ |
| 5 | 内部辅助函数契约 | 实际调用者调用辅助函数前必须建立什么？ |
| 6 | 压缩数据格式 | 独立于实现，DEFLATE、zlib 和 gzip 字节表示什么？ |
| 7 | 格式关系 | 怎样用数学关系表达字节的含义？ |
API 页面定义入口行为。格式页面定义字节含义。两个引擎和所有公开入口共享安全性要求。 这些是不同的证明义务，因此各自在这里保留唯一的规范来源。
文档陈述与形式化陈述
固定问题的精确表述是 ZlibF/Spec/ 及各文件规范命名空间下的 Lean 命题。
目标索引将每个问题链接到精确陈述和证明证据。
文档契约解释这些问题；修改文字不能完成目标、改变其前置条件或赋予覆盖颜色。
部分文档前置条件比公开头文件更窄。应阅读入口的明确范围和偏差记录。 一个范围较窄的内部引理不能建立完整的公开契约。
继续阅读模型与证明
模型指南解释 C 操作如何表示。 可信基础记录假设与表示缺口。 证明指南解释如何建立规范要求。 检查指南解释验收与登记。