参考文档 / ZLIB × LEAN

工具函数：分配与常量查询

此页源文件快照 · 7c5465dfed29b666 · 对应提交的原文 ↗

源文件为 zlib/zutil.c 和 zlib/zutil.h，翻译为 ZlibF/Zlib/zutil.c.lean。这些函数支持两个流实现。公开契约见 API 指南，所有权角色由安全规范定义。

默认 LP64 分配器分支使用 malloc，尽管函数名为 zcalloc。它不会清零块。初始化证明必须建立所需字段写入，包括模型不追踪的指针写入。

调用者的大小算术

分配请求包含“多少个元素”和“每个元素多少字节”。在 zcalloc(opaque, items, size) 中，它们分别是 items 和 size；opaque 是传入分配器的调用者上下文。只有先证明乘积未溢出，才能把返回块的模型容量解释为期望的总字节数。

此分支中，zcalloc(opaque, items, size) 以 32 位 unsigned 算术计算 items * size。包装定理必须忠实描述该乘积。若调用者期望普通乘积，依赖分配容量前必须证明它低于 2^32。

默认流分配	最大字节乘积
`deflateInit2_` 状态	LP64 `sizeof(deflate_state)`
压缩器窗口：`w_size * 2`	65536
压缩器 `prev`：`w_size * sizeof(Pos)`	65536
压缩器 `head`：`hash_size * sizeof(Pos)`	131072
压缩器待输出缓冲区：`lit_bufsize * 4`	131072
`inflateInit2_` 状态	LP64 `sizeof(inflate_state)`
解码器窗口：`(1U << wbits) * 1`	32768
`deflateCopy`, `inflateCopy`	上述相应状态和缓冲区大小

表中的窗口尺度 w_size、哈希桶数 hash_size 和符号容量尺度 lit_bufsize 都在初始化参数校验后确定；sizeof(Pos) 是每个位置表项占用的字节数。因此，容量按“表项数乘以每项字节数”换算成字节。状态大小必须来自所选 ABI 布局，并与 C 布局检查一致；它们不是跨配置的数学常量。缓冲区界限从已验证参数和流不变量保留的大小等式推出。此表只涉及所列流分配，不声称给出了所有 gz 或其他 API 路径的最大分配。

成功与失败效果

分配成功时增加一个指定模型大小的新鲜存活块；失败时返回空指针，不增加存活块。两种情况都不能让尚未写入的新指针字段变得可安全读取。未初始化整数依据运行时规则取任意值。

zcfree 接受空指针，或分配器接口允许的块。非空释放要求对应的存活所有权声明。End 和失败清理证明必须恰好提供一次。堆记录存活性和分配历史；证明的 Owns 关系把存活块归属于流。

deflateInit2_ 分配一个状态和四个缓冲区。合并的缓冲区失败检查在各次分配之后，因此前面一次失败不表示之后的分配从未尝试。清理必须释放该次尝试中所有成功分配，按源代码规定清除或保留字段，并恢复先前存活块集合。inflateInit2_、延迟解码窗口分配，以及两个复制函数，都需要各自的失败情形组合。仅分配器包装定理不能证明任何这些生命周期清理。

常量与错误查询

函数	要求的结果与帧性质
`zError(err)`	越界分支选择第 9 项。否则 `-6 ≤ err ≤ 2`，故 `2 - err` 位于 `[0, 8]`，没有有符号溢出。返回十项消息表的准确项，保持堆不变。
`zlibVersion`	返回所选版本字符串指针，静态内容满足契约，保持堆不变。
`zlibCompileFlags`	从所选类型位宽和启用的源分支推出准确数值标志，保持堆不变。

常量返回仍是准确契约：错误版本指针或改变的标志位必须使该函数的证明变异失败。早期文档曾将这些包装函数分类为旧模型中的已完成项。当前结果需要检查指南规定的准确目标、登记、变异证据和已审查 CI。当前检查点见进度。

C 对应检查

zError 在求值 2 - err 前检查错误范围。提前执行减法可能对任意 int 溢出。zlibCompileFlags 在已审查配置中得到 169；应保留产生它的源代码判断，不能把这个数当作普遍常量。返回的版本与错误字符串是只读静态对象。