回调解码：所有权与有限输入

源文件为 infback.c。调用者拥有窗口，并提供输入／输出回调。API陈述公开契约，进度记录当前进展。本页依次展开回调前提、初始化顺序与窗口复制的证明义务。

回调定义域与终止

输入回调负责交出一段可读字节，输出回调负责接收已解码的一段窗口。库负责何时调用它们，调用者负责这些外部函数的返回与存储有效性。窗口参数 windowBits 是容量的二进制指数，例如 15 表示 2^15 = 32768 字节。下表把这些调用者责任与更窄的迁移论证假设分开。

回调假设描述调用者提供的代码，与禁止假定库内被调用函数契约是两回事。调用 inflate_fast 或 inflate_table 的定理，仍需关于该翻译后函数的定理。

终止证明需要一个会随执行推进而下降的自然数，称为度量。这里的 phi 把已保留位、剩余字节和回调仍可交付的输入预算合并计数；它必须同时覆盖不读新字节的内部步骤和请求新输入的步骤。无限产出输入的回调可能使 inflateBack 永不返回，却不产生 C 未定义行为。有限输入定理必须明确这个前提，不能对公开接口允许的所有回调声称无条件终止。任何更窄的定理定义域都必须明确，并记录在偏差记录中。

回调解码器

inflateBackInit_ 分配状态但不清零，只写窗口设置、窗口指针、历史计数器与 sane。模型中新鲜整数任意，新鲜指针字段为空；后者弱于 C。证明必须说明每个指针在读取之前已被写入，仅无运行时故障还不够。inflateBack 使用的模式、位寄存器、码长和表指针在各路径中初始化：完整论证还需要逐路径证明这些写入都先于对应读取。

窗口由调用者提供并拥有。inflateBackEnd 只释放状态。源码把输入、输出回调分别叫 in、out；whave 计数已经可用的历史字节。ROOM 是需要更多输出空间时执行的宏，它在调用 out 前重设输出空间并写入 whave。PULL 只在当前输入耗尽时调用 in；返回零时设 next = NULL 并返回缓冲区错误。最终部分窗口的 out 调用发生在判断 ret == Z_STREAM_END 之前，因此也可能出现在错误路径，包括先前回调拒绝之后。最终收尾只回写 next_in 和 avail_in，不回写输出寄存器。

回调运行在共享堆上。实现的 InCb 接收当前输入指针，返回 (count, newPointer)；它不会像旧提案那样为 &next 分配真实单元。若回调保留该地址并随后经它写入，则不在此表示范围内。OutCb 接收窗口指针和长度，返回整数。

回调义务属于调用者前提，不是对 zlib 被调用函数的假定规范。它们包括：输入在下次 in 前保持有效可读，保留活动窗口切片与流状态，并对回调效果建立恰当帧性质。描述符存储可以与窗口分配共享空间，但须位于该切片之外。额外限制必须明确记录在偏差记录中。顶层声明需要具体的已初始化示例。

仅回调会返回还不足以推出终止。输入回调可以提供无限多个空的非最终块。终止定理需要有限输入界限，或其他明确的进展条件。功能观察必须包含回调事件与失败；不能无条件承诺失败的输出恰好交付一次。

已安装表与窗口复制

表构造返回值的分类不能建立规范链接的界限。把输出与历史设为不同数组的快速路径定理，也不能覆盖输出位于回调窗口中的情形。实际调用者必须在返回堆上建立已安装表和复制所需前提。历史上报告过缺少 whave 更新的疑点，其在本 API 中的可达性论证尚未完成；普通 inflate 的例子不能解决这个 API 的问题。