参考文档 / ZLIB × LEAN

compress2_z

按请求级别，将输入压缩为一个完整 zlib 流。

此页源文件快照 · 767fa1407a7fe3d1 · 对应提交的原文 ↗

先看本函数的前置条件和返回结果；可展开下方共同规则，查看整组接口的缓冲区与所有权要求。

int ZEXPORT compress2_z(Bytef *dest, z_size_t *destLen, const Bytef *source,
                        z_size_t sourceLen, int level);

按请求级别，将输入压缩为一个完整 zlib 流。

定义域 受限定义域。

前置条件 上述受限缓冲区定义域。source 可在零输入或经检查的拒绝情形中为 NULL。 destLen 可在经检查的拒绝情形中为 NULL。dest 可在经检查的拒绝情形中为 NULL，包括下面的零容量情形。有效级别为 -1 和 0–9；-1 选择级别 6。

返回与保证 Z_OK 表示输出是输入的完整 zlib 编码，且 *destLen 是其长度。 Z_BUF_ERROR 表示容量已由该编码的一个前缀填满。 Z_MEM_ERROR 表示分配失败，且没有写入输出。

内存与状态效果 有状态；适用通用效果。非零输入的 NULL 源、NULL destLen，或非零容量的 NULL 目标，会在任何长度写入之前返回 Z_STREAM_ERROR。否则在初始化前清零 *destLen。错误级别在任何分配前返回 Z_STREAM_ERROR，长度为零。后续返回会存储已写字节数。

边界情况 NULL 目标配合零容量会进入初始化：若分配失败，返回 Z_MEM_ERROR，否则返回 Z_STREAM_ERROR，长度为零。非 NULL 目标配合零容量，在成功初始化后返回 Z_BUF_ERROR。空输入有效。

本组共同前提与范围

API 手册 · 共享流规则 · 校验和

调用时已知完整输入和输出容量，可使用缓冲区工具。它们在内部管理临时流。需要增量 I/O、其他包装、字典或显式刷新边界时，应使用流式接口页面。

任务	入口
压缩缓冲区	选择级别、默认级别、确定目标容量
解压缓冲区	报告已消费输入、仅报告输出
查询库信息	版本、编译标志、错误文本

这些聚焦契约对应默认 LP64 Linux 构建中的 compress.c、uncompr.c、zutil.c 和 zlib.h。_z 形式使用 z_size_t；普通形式使用 uLong。这里两者均为 64 位。本页契约不会缩小 Utilities.lean 和 Queries.lean 中登记的目标。 Calls.lean 固定翻译后的参数和结果。定义域和效果标签见契约约定；证明状态和剩余工作见进度。超出聚焦前提只表示本契约不作保证，不自动等于 C 未定义行为（UB），也不保证一定返回错误码。

缓冲区工具使用 zlib 包装和默认设置，创建并释放一个局部流。

先看输入／输出长度的约定：sourceLen 指定可读输入的字节数；*destLen 在调用前是目标数组的可写容量，调用后改为实际写入量。例如目标有 1000 字节容量、最终写入 120 字节，调用前应设置 *destLen = 1000，成功返回后读取到 120。这个长度单元自身也是需要保持存活、可读写的调用者存储。uncompress2_z 的 *sourceLen 同样在调用前给出输入容量，返回后报告已消费量。

查询上界的函数只计算一个数，并不替调用者分配目标数组。

flowchart LR
    B["compressBound"] --> C["compress / compress2"]
    C --> Z["zlib 流"] --> U["uncompress / uncompress2"]
    U --> D["解码字节"]

通用约定

缓冲区调用的定义域限于有效内存：非 NULL 源覆盖指定的可读输入；非 NULL 目标覆盖指定的可写容量。非 NULL 长度指针指向可读写的标量单元。输入、输出和长度单元互相分离，包括同时出现的两个长度单元。调用期间，调用者保持这些对象存活且不修改它们。各入口分别说明允许的 NULL 情形。其他无效指针不在此范围内。处理解压错误不要求压缩数据有效。

通用效果。 每个范围内调用都终止且不产生故障。缓冲区调用保持输入以及输出、长度单元以外的内存不变，写入不超过原始容量。返回前释放所有内部分配，包括分配失败路径；不返回局部流或其拥有的分配。返回指针的查询交付借用的不可变存储。这些要求适用于每一条所述返回路径，包括分配失败和部分输出之后的清理。

形式化约定

ZlibF.Spec.Public.Goal.compress2_z

证明状态：未完成 · 证明记录与剩余工作

/-- `int compress2_z(Bytef *dest, z_size_t *destLen, const Bytef *source, z_size_t sourceLen, int level)`.
Includes null-cell rejection, unchanged capacity on argument rejection, exact stored length,
valid compressed data, buffer exhaustion, allocation failure, frame and complete cleanup. -/
def Goal.compress2_z : Prop :=
  ∀ level, CompressorContract (fun d c s n => Zlib.Compress.compress2_z d c s n level) level true