参考文档 / ZLIB × LEAN

inflateSetDictionary

设置或补充可供向后匹配使用的字节。

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

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

int ZEXPORT inflateSetDictionary(z_streamp strm, const Bytef *dictionary, uInt dictLength);

设置或补充可供向后匹配使用的字节。

定义域 受限定义域：在 Z_NEED_DICT 后等待的有效 zlib 流，或处于任意调用边界的有效 raw 流。

内存与状态效果 修改历史，可能分配窗口。

前置条件 dictionary 非 NULL，描述 dictLength 个可读字节，即使长度为零也如此。要产生正确输出，它须与压缩器字典一致。

返回与保证 保留“旧历史后接新字典”这一序列的最后一个窗口大小的后缀后，返回 Z_OK。整个给定字典都参与 zlib 标识检查。调用者字节被复制，不保留其存储，也不释放它。

错误路径 错误的 zlib 标识返回 Z_DATA_ERROR，不发生变化；可以尝试另一个字典。NULL 字典、流检查失败，或不在等待字典的包装流，返回 Z_STREAM_ERROR。分配失败返回 Z_MEM_ERROR，使流处于内存错误模式，仍可结束。

边界情况 gzip 没有预置字典路径。raw 模式不检查标识；错误字典可能产生错误输出或较晚的错误。接受零长度 raw 字典。不推进输入/输出指针或总计数。

本组共同前提与范围

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.inflateSetDictionary

证明状态：已登记证明 · 证明记录与剩余工作

/-- `int inflateSetDictionary(z_streamp strm, const Bytef *dictionary, uInt dictLength)`.
Raw streams append to their window. Wrapped streams require DICT mode and the exact Adler id. -/
def Goal.inflateSetDictionary : Prop :=
  ∀ h r i z s source n xs old,
    Zlib.Inflate.Spec.Good h r i z s → z.zalloc = .fn "zcalloc" →
    InflateDictionary h s old → (source ≠ .null → Bytes h source n.toNat xs) →
    Separate source n.toNat s.window (2 ^ s.wbits.toNat) →
    ((s.wrap = 0 ∨ s.mode = DICT) → 8 ≤ s.wbits.toNat) →
    ∃ rc after, C.run (Zlib.Inflate.inflateSetDictionary (some r) source n) h = .ok (rc, after) ∧
      (source = .null ∨ (s.wrap ≠ 0 ∧ s.mode ≠ DICT) → rc = Z_STREAM_ERROR ∧ after = h) ∧
      (source ≠ .null → (s.wrap = 0 ∨ s.mode = DICT) →
        if s.mode = DICT ∧ s.check ≠ (ZlibF.Spec.adler32 xs).toUInt64 then rc = Z_DATA_ERROR ∧ after = h
        else (rc = Z_MEM_ERROR ∧ AllocationFailed h after ∧
          ∃ s', Zlib.Inflate.Spec.Good after r i z s' ∧ s'.mode = MEM) ∨
          (rc = Z_OK ∧ ∃ s', Zlib.Inflate.Spec.Good after r i z s' ∧
            s'.havedict = 1 ∧ s'.mode = s.mode ∧
            InflateDictionary after s' ((old ++ xs).drop ((old ++ xs).length - 2 ^ s.wbits.toNat)))) ∧
      Frame h after (fun b => StreamRoot r b ∨ InflateOwned i s b) ∧
      (∃ s', h.istates i = some s ∧ after.istates i = some s' ∧
        LiveChange h after (fun b => InflateOwned i s' b ∧ ¬ h.live b) (fun _ => False))