deflate
接受输入，交付有效压缩流的一部分或全部。
完整章节与共同规则 ↗39ab1ace4bbe0b0e · 对应提交的原文 ↗先看本函数的前置条件和返回结果；可展开下方共同规则，查看整组接口的缓冲区与所有权要求。
int ZEXPORT deflate(z_streamp strm, int flush);
接受输入，交付有效压缩流的一部分或全部。
flush 描述调用者希望推进到哪里：普通调用交给压缩器选择输出时机，刷新请求建立所选边界，Z_FINISH 请求结束整个流。请求不会让有限输出空间变大；空间用完时，仍要取走输出并按下述协议继续。
定义域 受限定义域。影响： 消费输入、输出数据并更新进度。
前置条件 有效流，缓冲区和任何正在使用的头部均有效。next_out 非 NULL，avail_out > 0；仅输入为零时 next_in 可为 NULL。flush 为 Z_NO_FLUSH、Z_PARTIAL_FLUSH、Z_SYNC_FLUSH、Z_FULL_FLUSH、Z_FINISH 或 Z_BLOCK。刷新期间输出填满时，以相同刷新请求和更多空间继续。开始完成操作后，不提供新输入，只以 Z_FINISH 继续。普通格式有效性要求从初始化/deflateReset（或该历史的副本）开始，使用合法字典/头部设置、标准调优，且不进行任意位预置。
返回与保证 记本轮消费的输入字节数为 used，交付的输出字节数为 made；old avail_in 和 old avail_out 是调用前提供的输入量和输出容量。满足 used <= old avail_in、made <= old avail_out。指针按相应数量推进，可用计数按相应数量减少，总计数按相应数量增加并遵循无符号回绕。输入不变；已交付前缀以外的输出不变。输出填满时可能仍有输入未消费。不分配或释放。
跨调用交付的字节构成已接受输入的一种有效编码的前缀，使用所选包装、设置和预置字典。完成的输出可解码为该输入。这里规定有效输出，而非唯一的压缩字节序列。头部输出之后，adler 用 Adler-32 跟踪 zlib 已接受输入，用 CRC-32 跟踪 gzip 已接受输入；raw 没有输入校验和。
Z_OK 表示可能需要继续。Z_STREAM_END 只在 Z_FINISH 下发生，且所有给定输入及所有压缩输出（包括尾部）都已交付。有效状态仍被拥有，直到 deflateEnd 释放，或通过 deflateReset 复用。
请求的刷新完全交付后，Z_BLOCK 完成一个块但不填充到字节边界；Z_PARTIAL_FLUSH 添加空固定块；Z_SYNC_FLUSH 使此前全部输入可供解码器解码，并以对齐的空存储块结尾。Z_FULL_FLUSH 还重置匹配历史：后续块不引用该次已完成刷新之前的数据。若要在那里重新启动 raw 解码器，需要保留精确边界，并先交付完整刷新标记。Z_FINISH 关闭最终块并写入包装尾部。
错误路径 Z_BUF_ERROR 覆盖输出空间为零、无输入且无更强刷新请求因而无法推进，或最终块处理已开始后又提供输入。它保留有效流；应按需提供空间/输入。Z_STREAM_ERROR 覆盖流检查失败、无效刷新（包括 Z_TREES）、无效 NULL 输入／输出组合，或完成操作开始后请求非完成刷新。初始参数拒绝不消费输入、不交付输出。开始完成操作后，因新输入而产生的较晚 Z_BUF_ERROR，可能先交付旧的待输出数据；不接受新输入。msg 和记录的刷新请求可能改变。未改变的公开目标包括所有有符号刷新值及这些拒绝。
本组共同前提与范围
输入分批到达、输出空间有限，或需要选择封装、字典、刷新边界时，使用 z_stream 压缩器。封装是在 DEFLATE 压缩数据之外增加的头部、尾部和完整性信息；raw DEFLATE 则不带这些封装。初始化一次，使用连续的缓冲区调用 deflate，即使放弃压缩也要结束流。单个缓冲区的操作见 compress 和 compress2。
| 任务 | 条目 |
|---|---|
| 开始或复用 | 初始化、配置初始化、重置、保留历史的重置 |
| 提供元数据或历史 | 字典、读取历史、gzip 头 |
| 压缩与输出大小 | 压缩、上界、待输出数据、最近刷新位数 |
| 调整或分支 | 参数、调优、位预置、复制 |
| 释放存储 | 结束 |
这些聚焦契约遵循固定版本的 deflate.c、已应用补丁和 zlib.h，采用默认 LP64 Linux 构建。它们不改变范围更广的已登记公开目标。定义域/影响标签见契约约定，证明状态和剩余工作见进度。
共享约定
在每条所述前置条件下，都要求执行无运行时故障地终止，并满足所述后置条件。调用若保留有效流，就保持其表示不变量。
先看一次调用的数据交接。next_in 指向本轮尚未读取的输入起点，avail_in 是从这里开始可读的字节数；next_out 指向本轮下一个可写位置，avail_out 是剩余输出容量，也以字节计。一次调用可以只消耗部分输入、只交付部分输出。调用者应读取更新后的指针和计数，接走已交付字节，再为同一个流补充输入或输出空间。
- 有效流： 可写的
z_stream，其压缩器状态由成功初始化或复制建立，经过合法调用保持，且尚未结束。调用者不改变其内部状态或分配器字段。同一个流的调用按顺序执行。 - 缓冲区： 输入覆盖
avail_in个可读字节；输出覆盖avail_out个可写字节。它们彼此不重叠，也不与流或流拥有的状态重叠。非 NULL 标量结果指向可写单元，与其他结果及流内存分离。这些分离条件是聚焦契约的显式假设；见 safety.md。 - 分配器： 使用默认分配/释放函数对，或在初始化前将两个字段都置为 NULL。任意一次分配尝试都可能失败。自定义分配器回调不在本页范围内。
- 帧性质与所有权： 调用只改变自己的流、其拥有的状态和所述输出区域。调用者输入只读。调用者缓冲区和头部记录仍归调用者所有。只有初始化和复制会分配；只有它们失败时的清理与
deflateEnd会释放内存。其他调用保持流的分配集合。 - 头部生命周期： 保留的 gzip 头及其可选字段在使用期间保持可读且不变。非 NULL 的
name和comment以零终止；extra覆盖所述长度。聚焦格式契约使用extra_len <= 65535。 - 检查后的拒绝： 除初始化和上界查询外，流检查失败会在正常操作之前返回
Z_STREAM_ERROR，不发生写入。deflateCopy还会清空非 NULL 目标的状态。这种拒绝不修改查询输出单元。 - 受限定义域指这些显式内存、生命周期和调用顺序条件，加上条目自身的前置条件。它不意味着接受每个可表示的指针或整数。错误概述覆盖可读、可检查的状态，不覆盖任意无效地址。
形式化约定
ZlibF.Spec.Public.Goal.deflate
证明状态：未完成 · 证明记录与剩余工作
/-- `int deflate(z_streamp strm, int flush)`.
Preserve the live stream and its five allocations. Account for exactly the bytes accepted
and delivered, including progress on a full output buffer and clean parameter refusals.
The sequence target states valid encoding, flush semantics and completion. -/
def Goal.deflate : Prop :=
∀ h r i z s flush,
StreamReachable .deflate h r → Zlib.Deflate.Spec.DGood h r i z s →
StreamBuffers h r → ActiveHeader h r →
∃ rc after z' s' used out,
C.run (Zlib.Deflate.deflate (some r) flush) h = .ok (rc, after) ∧
Zlib.Deflate.Spec.DGood after r i z' s' ∧ StreamAccounting z z' used out.length ∧
Bytes after z.next_out out.length out ∧
z'.total_in = z.total_in + UInt64.ofNat used ∧
z'.total_out = z.total_out + UInt64.ofNat out.length ∧
(rc = Z_OK ∨ rc = Z_STREAM_END ∨ rc = Z_STREAM_ERROR ∨ rc = Z_BUF_ERROR) ∧
(rc = Z_STREAM_ERROR ↔
flush.toInt < 0 ∨ 5 < flush.toInt ∨ z.next_out = .null ∨
(z.next_in = .null ∧ z.avail_in ≠ 0) ∨
(s.status = FINISH_STATE ∧ flush ≠ Z_FINISH)) ∧
(flush.toInt < 0 ∨ 5 < flush.toInt → rc = Z_STREAM_ERROR ∧ after = h) ∧
(rc = Z_STREAM_END → flush = Z_FINISH ∧ s'.status = FINISH_STATE ∧
z'.avail_in = 0 ∧ s'.pending = 0 ∧ s'.bi_valid = 0) ∧
BufferFrame h after (fun b => StreamRoot r b ∨ DeflateOwned i s b) [⟨z.next_out, out.length⟩] ∧
LiveChange h after (fun _ => False) (fun _ => False) ∧ after.nalloc = h.nalloc