参考文档 / ZLIB × LEAN
调用者定义域与表示限制
此页源文件快照 ·
3892229f4fe5c39d · 对应提交的原文 ↗超出模型能力的定理不是 C 正确性结果。本登记记录 API 适配器的受限定义域和缺口。每个强于 zlib.h 的前置条件，也必须写入定理文档字符串。聚焦手册中的狭窄例子不改变固定公开目标，也不把排除调用判为未定义。见契约约定。
完整目标仍是公开 API 允许的全部调用的安全性、终止、帧性质、所有权和功能正确性。进度记录已完成与未完成的工作；可信基础记录运行时选择。
构建与内存表示
本表按“模型能表示什么 → 哪些调用或结论受影响”阅读。比如，长度输出单元与数据缓冲区分开表示时，模型可以描述两者各自的值，却还不能描述它们占用同一块存储的情况。这样的缺口必须保留在适用范围里，不能用一个成功例子把它消掉。
| 领域 | 当前限制 | 影响 |
|---|---|---|
| 初始配置 | 默认 x86_64 Linux、LP64、静态构建和默认分配器 | 其他上游配置和自定义分配器需要独立覆盖。默认分配失败仍在范围内。 |
| 平台字节对象范围 | 每个表示出的字节对象小于 2^63 字节，包括调用者、静态和内嵌存储 |
这是接受的系统环境前提，由 Goal.inflate 与内部快速入口显式使用。限制逐对象成立，没有总内存或总流长度限制。执行证明保持它；证明操作系统限制不属于 zlib 证明。 |
| Adler 初始化查询 | AdlerBufferBytes 只允许零长度时为 NULL；非空可读对象保留原定义域 |
该显式限制窄于固定头文件对 NULL 不加限定的表述。它适用于 Goal.adler32_z 和 Goal.adler32；CRC 契约保留 BufferBytes 不变。 |
| 聚焦函数手册 | 条目可能要求有效句柄、分离缓冲区、实际字符串的校验和、生成的操作符或特定调用顺序 | 这些是明确的文字范围，不缩小更广泛 Lean 公开目标。 |
| 压缩器长度单元 | Concrete.compress2_z 和 Concrete.compress2 使用可选标量输入及返回的存储值 |
不表示该单元与输入或输出的别名。若 C API 允许，完整指针定义域结论需要解决它。_z 与兼容包装的空单元效果仍不同。 |
| 计数解压单元 | 草案适配器保持输入长度、输出长度和数据范围分离 | 单元与数据或彼此的别名在适配器之外。早期和后期内存失败保留不同标量效果。 |
| 压缩器数据关系 | Compress2 用粗粒度拒绝标志描述数据 |
Compress2Z 和 Compress2Wrapper 表达指针形状、错误顺序和长度存储。数据模型定理本身不是入口细化。 |
| 上界算术 | LP64 上两个长度都是 64 位 | Goal.compress_bound_value 覆盖每个 UInt64，没有更小数值前提。其他 ABI 需要大小转换命题。只有数值公式不能建立输出容量充足性。 |
| CRC 地址和字访问 | addrOf 只观察地址低位。堆字节块保留对齐起点；静态和内嵌字节对象有任意稳定余数。字加载按字节组装 |
通用 ABI 布局、任意原始块起点和 C 转换的别名语义仍不在该抽象内。公开校验和定义域不变。静态地址回归保留了此前模型反例的输入，作为正向检查。 |
| 空指针算术 | Ptr.add 允许空指针加零；Ptr.diff 对空指针故障，而压缩器辅助函数允许空指针减空指针 |
模型允许不等于 C 有定义。安全性规范区分操作和语言规则。分配回归为零容量空目标保留这一区别。 |
流与回调模型
| 领域 | 当前限制 | 影响 |
|---|---|---|
| Deflate 字典顺序 | DeflSetDict 的 zlib 分支在 started 后拒绝字典 |
C 可在流结束后接受字典。细化只能在文档顺序内使用该拒绝。deflate_valid 是模型定理，不是关于全部此类 C 执行的定理。 |
| 普通字节格式阶段 | 一个初始预置字典解释普通流 | 解码开始后的 raw 字典替换有构造器导出的标记。精确窗口效果和无条件序列安全仍须满足。一个初始字典不能描述完整高级历史。 |
| 高级操作组合 | Priming、头部和恢复保留具体逐入口目标 | 目标集合不是每种组合的完整操作细化。证明不能选择或清除历史资格标记来逃避义务。 |
| 快速解码辅助函数 | 局部执行和位来源引理假设互异原始字节块、六个输入字节、258 个输出字节、入口位数小于八及 sane 模式 | 这些是构造和 init 不变量必须建立的内部前提，既不限制也不证明公开 inflate 目标。 |
| 符号细化 | 规范表含义、后缀稳定性和兼容叶标志是显式前提；局部复制使用实际按时间顺序保存的字节 | 局部符号引理不建立表安装、窗口历史或整个流输出。 |
| 回调 | 回调返回、输入有有限界限、保留调用者窗口切片 | 描述符对象可共享窗口分配中切片以外的部分。观察不变量只忽略窗口字节，保留对其余字节的效果。这些外部假设必须显式保留。 |
Gz 外部世界
gz 世界是堆之外的可信语义。目前范围小于 C 调用的系统接口。外部 I/O 模型描述底层表示，公开 gz 契约给出操作定义域。
| 领域 | 当前限制 | 影响 |
|---|---|---|
| 文件与读取 | 扁平路径、普通文件和目录标记；普通读取仅在文件末尾短读 | 不表示管道、套接字、终端、一般短读和瞬态失败。非阻塞和描述符控制标志不会增加这些行为。 |
| 文件系统错误 | 不表示权限、父目录、链接、所有权和锁。写失败通过大小限制建模 | 这不覆盖任意 EINTR、EIO、ENOSPC 或所有打开失败。有符号 seek 溢出仍是翻译代码的义务。 |
| 格式化 | 表示出的整数、字符和字符串参数，以及支持的标志、宽度、精度和长度修饰符 | 浮点、指针、写计数和其他未表示转换需要扩展模型。草案契约显式要求可表示的有效格式化结果。 |
| 外部错误字符串 | strerror 文本分配为新鲜只读块，永不释放 |
这不同于借用外部静态存储。完整所有权结论必须计入该选择，不能悄悄当作库拥有存储。 |
| 循环额度 | 每个翻译循环使用固定运行时额度 | 即使每个外部操作都返回，也不能据此证明任意有限回调或外部世界行为终止。 |
这些限制不能成为压制失败公开用例的理由。若目标错误，应报告反例并通过独立审阅修正。若翻译或运行时错误，应在相应层修正，并提供所需审阅和回归证据。验证策略使这些改动与证明进度保持分离。
局部 open、close 与 priming 里程碑
open 入口引理覆盖 NULL 参数、负描述符和初次分配失败，不覆盖成功解析器，也不建立完整公开 open 契约。读取器 close 执行里程碑假设现有 GzGood 不变量、读模式和 size = 0。其定义域排除已初始化读取器，以及公开表示允许的含非活动悬空缓冲区句柄；它不从实际公开历史建立不变量。Priming 入口引理覆盖被拒绝流和 0 到 16 之外的计数；接受的位插入仍未完成。
这些是有范围限制的内部定理，没有一个替代或缩小公开目标。当前工作统一在进度。