参考文档 / ZLIB × LEAN

inflate

消费压缩字节，写入解码字节，跨调用保留状态。

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

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

int ZEXPORT inflate(z_streamp strm, int flush);

消费压缩字节，写入解码字节，跨调用保留状态。

这次调用只使用当前给出的输入和输出空间。返回时先看实际推进了多少，再看返回码决定是继续、提供字典、结束还是处理错误。flush 请求的是停止边界或完成方式，不是压缩级别。输出空间用完不表示数据流已经解完，输入暂时不够也不等于格式损坏。

定义域 受限定义域：满足公共缓冲区/头部生命周期条件的有效流；覆盖任意压缩字节、输入/输出分块和有符号 flush 值。

内存与状态效果 修改流、输出和已登记头部存储；可能分配历史窗口。

前置条件 next_in 描述 avail_in 个可读字节，仅在计数为零时可为 NULL。即使 avail_out 为零，next_out 也非 NULL，并描述该数量的可写字节。已登记头部及其缓冲区保持可写。调用可以提供更多输入/空间继续，可以提供请求的字典，也可以在成功重置/恢复之后继续。终止/错误状态下的重复调用行为如下。

返回与保证 在所述范围内读写。按已消费/已产生字节数推进指针并减少可用计数。从初始化/重置开始的普通运行中，如果所选格式有效且字典正确，累计输出是解码数据的前缀，在 Z_STREAM_END 时等于完整数据。畸形字节也在定义域内：检测到格式错误，或启用的校验和/长度检查失败时，返回 Z_DATA_ERROR，此前可能已有输出。仅有输入不完整时需要更多输入；不必把它报告为数据错误。

结果	含义与下一步
`Z_OK`	输入或输出有所推进；利用可用输入/空间继续
`Z_STREAM_END`	完成一个流/成员，包括启用的尾部检查；尾随输入保留
`Z_NEED_DICT`	需要 zlib 字典；`adler` 为其标识；设置字典
`Z_BUF_ERROR`	没有推进，或 `Z_FINISH` 未能完成；提供输入/空间
`Z_DATA_ERROR`	检测到畸形数据；重置、恢复或结束
`Z_MEM_ERROR`	窗口分配失败；重置或结束
`Z_STREAM_ERROR`	流/缓冲区检查失败，或恢复搜索尚未完成

计数记账 正常返回，包括数据错误和缓冲区错误，按已消费/已产生字节数更新总计数，并更新已启用的输出校验和。Z_NEED_DICT 记录已消费的头部字节，并让 adler 保持为字典标识。晚期窗口分配失败可能发生在消费输入和写入输出之后：指针/计数已经反映这些操作，但跳过正常最终总计数/校验和/data_type 记账。不能把 Z_MEM_ERROR 当作输出未变的结果。

边界情况 允许输入或输出空间为零。Z_BLOCK 在头部或块边界停止；Z_TREES 还在块描述之后停止。Z_FINISH 将本来为 Z_OK 的结果改为 Z_BUF_ERROR。其他有符号刷新值被接受，行为与 Z_NO_FLUSH 相同。正常返回时，data_type 记录未用位数；最终块再加 64，头部/块边界再加 128，块头之后再加 256。数据和内存错误会保持；完成的流重复返回 Z_STREAM_END。

所有权 新窗口存储归流所有，仍可用于重置/结束，包括错误之后。一次调用的 Z_FINISH 完成可能无需窗口。拼接 gzip 成员要求成员之间重置。错误消息是借用的静态字符串。缓冲区和流检查的拒绝不改变任何内容。

本组共同前提与范围

API 手册 · 共享流规则 · 流式压缩

使用 inflate 流分批解码输入，同时控制输出空间。初始化时选择 zlib、gzip 或不带封装的 raw DEFLATE，随后提供更多输入或空间继续，直到完成、请求字典或发生错误。无论出现哪种结果，inflateEnd 都可释放解码器。整块缓冲区的 zlib 解码见 uncompress。

任务	条目
开始或复用	初始化、配置初始化、重置、新配置、保留历史
解码或提供元数据	解压、设置字典、读取历史、gzip 头
恢复或检查	同步搜索、同步点、位置标记、表使用量
调整或分支	预置位、校验、距离选项、复制
释放存储	结束

聚焦契约遵循固定版本的 inflate.c 和 zlib.h，采用默认 LP64 Linux 构建，启用 gzip，不启用可选的无效距离或严格距离模式。范围更广的已登记公开目标保持各自定义域。术语见契约约定，证明状态和剩余工作见进度。

公共条件

调用者与解码器各自保留不同的内容。调用者提供本轮输入和输出缓冲区；解码器保留当前解析阶段、尚未用完的位，以及可能供后续复制使用的历史。更换调用者的输出数组，并不会开始一个新解码任务。

next_in 是本轮未读输入的起点，avail_in 是可读字节数；next_out 是下一个输出位置，avail_out 是从这里开始的剩余可写字节数。例如一块 5 字节输出数组返回时剩余 2 字节空间，就说明本轮写入了 3 字节。先接走这些结果，再把指针和容量设置为下一块可写区域。

下列所有契约都有受限定义域。仅凭 C 指针类型，不能提供这里要求的存储、生命周期或调用历史。

有效流已成功初始化或复制，尚未结束，保留库拥有的状态，且不发生并发调用。使用默认分配器和释放函数。初始化调用接收可写、尚未有效初始化为流的对象，分配器字段为 NULL 或默认函数。
可读或可写范围在整个调用期间都具有所述容量。调用者范围与流及流拥有的存储分离。输入与输出范围不重叠。字典目标、已登记头部记录及其目标缓冲区彼此分离，也与流分离。使用已登记头部存储的调用还要求它与输入/输出范围分离。这些是聚焦定义域的显式限制。
调用者拥有流对象及缓冲区。库拥有状态和可选窗口。调用只改变自己的流、拥有的存储、所述输出范围和任何已登记头部目标。它绝不释放调用者缓冲区。
流检查拒绝时返回 Z_STREAM_ERROR，不发生变化，除非查询或复制契约另有说明。这覆盖 NULL 和可安全读取但未通过检查的记录，不覆盖悬空或任意指针。检查要求分配器、状态、状态的回指针和有效模式满足条件。
计数器使用 C 无符号位宽并回绕。没有契约假设分配成功。解码、字典或分配错误之后，仍可调用 inflateEnd。

flowchart LR
    I["初始化"] --> F["inflate"]
    F -->|"Z_NEED_DICT"| D["设置字典"] --> F
    F -->|"更多空间或输入"| F
    F -->|"结束或放弃"| E["结束"]
    F -->|"数据错误"| R["重置或同步搜索"] --> F

形式化约定

ZlibF.Spec.Public.Goal.inflate

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

/-- `int inflate(z_streamp strm, int flush)`.
The domain is actual init/call history, not an arbitrary hand-built decoder state.
The selected LP64 platform scope explicitly requires every live represented
byte object to have at most PTRDIFF_MAX bytes (size < 2^63), including caller
storage from non-malloc origins. See docs/deviations.md.
Includes all signed flush arguments, progress, terminal/error modes, output bounds,
counter timing on late memory failure, caller frame and ownership of a new window.
The sequence target states format correctness across all input/output splits. -/
def Goal.inflate : Prop :=
  ∀ h r i z s flush,
    StreamReachable .inflate h r → Zlib.Inflate.Spec.Good h r i z s →
    ZlibF.PlatformMemory.ByteObjectsFit h →
    Zlib.Inflate.Spec.DefAlloc z → StreamBuffers h r → ActiveHeader h r →
    ∃ rc after z' s' used out,
      C.run (Zlib.Inflate.inflate (some r) flush) h = .ok (rc, after) ∧
      Zlib.Inflate.Spec.Good after r i z' s' ∧ StreamAccounting z z' used out.length ∧
      Bytes after z.next_out out.length out ∧
      (rc = Z_OK ∨ rc = Z_STREAM_END ∨ rc = Z_NEED_DICT ∨ rc = Z_STREAM_ERROR ∨
       rc = Z_DATA_ERROR ∨ rc = Z_MEM_ERROR ∨ rc = Z_BUF_ERROR) ∧
      (rc = Z_OK → (used ≠ 0 ∨ out ≠ []) ∧ flush ≠ Z_FINISH) ∧
      (rc = Z_STREAM_END → s'.mode = DONE) ∧
      (rc = Z_NEED_DICT → s'.mode = DICT) ∧
      (rc = Z_DATA_ERROR → s'.mode = BAD) ∧
      (rc = Z_MEM_ERROR → s'.mode = MEM ∧ z'.total_in = z.total_in ∧ z'.total_out = z.total_out) ∧
      (rc = Z_OK ∨ rc = Z_STREAM_END ∨ rc = Z_DATA_ERROR ∨ rc = Z_BUF_ERROR →
        z'.total_in = z.total_in + UInt64.ofNat used ∧
        z'.total_out = z.total_out + UInt64.ofNat out.length) ∧
      BufferFrame h after
        (fun b => StreamRoot r b ∨ InflateOwned i s b ∨ s.head = some (.tab b))
        (⟨z.next_out, out.length⟩ :: HeaderRegions h s.head) ∧
      LiveChange h after (fun b => InflateOwned i s' b ∧ ¬ h.live b) (fun _ => False)