缓冲区工具与输出界限

源文件是 compress.c、uncompr.c 和 deflate.c 的界限查询入口。API 契约说明调用者义务，进度记录已接受范围与剩余工作。本指南把容量公式、调用循环和资源清理的证明义务串在一起。

界限与缓冲区工具包装

这类接口先根据输入长度准备输出容量，再在局部流中多次调用引擎，直到完成或出错。证明要分开两个承诺：一个数值上界公式算对了，以及实际压缩输出确实不会超过它。名称带 _z 的入口使用 z_size_t 长度；兼容入口还需保留较窄长度字段的转换和分批处理。

compressBound_z 使用回绕加法和饱和测试。只证明公式，不足以说明所有压缩输出都能放入该容量。deflateBound_z 还读取包装状态字段 wrap 和可选头字符串；该字段区分 raw、zlib 和 gzip，并在完成后可变成负值。它计算开销时，每次扫描包括终止空字符。它会在完成后将负 wrap 规范化，并保留每项溢出检查。

历史上的 deflateBound_z 头部问题涉及正确性，而非有符号溢出：2 + extra_len 先以 32 位无符号类型求值，随后才加到 64 位包装开销中。extra_len >= 0xfffffffe 时它会回绕，而输出只使用 extra_len & 0xffff。早期建议改为 2 + (z_size_t)(extra_len & 0xffff)（上游讨论）。这段历史不授权未登记补丁。输出界限证明需要覆盖这里的实际运算顺序及所述头部定义域。

compress2_z 和 uncompress2_z 使用自动局部流。创建这些对象不能失败、消费分配器预言机调用，或改变库分配的失败索引。被取址的标量局部变量也具有自动生命周期。模型存储应在源代码每个返回点释放，不额外增加 C 分配。分配回归记录修正后的区分及错误顺序观察。

工具循环从更宽的剩余长度补充 32 位可用数量字段。它们只在 Z_OK 时继续；初始化成功后调用 End，并保留结果映射和最终标量写入。解码器后期内存失败可能发生在输出之后，并不表示目标为空。

原审查的两项命名结论仍相关：

• R-2，包装函数的空指针读取。 compress2 在调用 _z 版本前读取 *destLen；uncompress2 读取两个标量单元。_z 中的空指针测试保护不了这些先前读取。单独的执行见证诊断过它们；它们不属于合法调用的比较行。
• D-4，空指针相减。 compress2_z 在零容量空目标之后计算 next_out - dest。其翻译明确允许空指针减空指针等于零。这一模型选择与选定 C 语言语义的对应尚未完成。相同结果与无报错的运行时检测器不能解决这个问题。

压缩适配器把长度指针表示为可选输入和返回值，无法表达它与字节缓冲区的别名。带计数的解压适配器也有标量分离限制。见偏差记录；这些限制不解决完整 C 定义域的问题。

uncompress2_z 在零容量时使用局部流的 reserved 字段地址，作为非空的占位输出。只有证明它从不被解引用，并说明其生命周期与别名，才能用单独的模型字节表示这一用途。实际解码调用还需要证明：零容量会排除经此指针写入。