参考文档 / ZLIB × LEAN

inflateBackEnd

用途。释放回调初始化所分配的状态。

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

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

int ZEXPORT inflateBackEnd(z_streamp strm);

用途。 释放回调初始化所分配的状态。

定义域 受限定义域：使用有效默认释放函数的活跃回调解码器，另包括经检查的 NULL 流、NULL 状态和 NULL 释放函数拒绝情形。

前置条件 清理时初始化已成功、尚未结束，且没有解码或回调正在活动。流和所关联状态仍有效；保留匹配的 zfree 和 opaque。成功解码或任何解码错误后均允许清理。

内存与状态效果 恰好释放内部状态，并清除 state。

返回与保证 Z_OK 使 state 为 NULL。调用者的窗口及其他所有流字段不变。调用者此时可释放或复用窗口；库从不释放它。

错误路径 NULL strm、NULL 状态或 NULL zfree 返回 Z_STREAM_ERROR，不释放任何内存。这些检查不会验证任意非 NULL 状态，也不会检测所有权错误。

返回 API 手册 · 契约约定

本组共同前提与范围

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

回调接口允许调用者提供输入块，并直接从窗口接收解码输出。先用 inflateBackInit_ 初始化，再用 inflateBack 解码，最后用 inflateBackEnd 释放状态。窗口始终由调用者拥有。

这些聚焦契约对应固定版本的 infback.c 和 zlib.h，针对默认 LP64 Linux 构建。本页的受限定义域不会缩小 Back.lean 或 Sequences.lean 中更宽的目标。定义域和效果标签见契约约定；证明状态和剩余工作见进度。超出聚焦前提只表示本契约不作保证，不自动等于 C 未定义行为（UB），也不保证一定返回错误码。

inflateBack 解码 raw DEFLATE。任何 zlib/gzip 头部、尾部和校验和都由调用者处理。调用者拥有一个至少 2^windowBits 字节的可写窗口，它同时也是输出缓冲区。 windowBits 是窗口字节数的二进制指数：15 表示 2^15 = 32768 字节。对一般流使用这个配置；更小窗口可能拒绝有效的长距离引用。

flowchart LR
    I["inflateBackInit_: 分配状态"] --> B["inflateBack: 解码一个流"]
    B -->|另一个流| B
    B -->|成功或解码错误| E["inflateBackEnd: 释放状态"]
    I -->|无需解码| E

回调让库在需要数据时主动调用应用代码。输入回调的参数 in_desc 是应用自己的上下文；buf 接收下一块输入的起始指针，返回值给出这块输入的字节数。输出回调的 out_desc 也是应用上下文；buf 和 len 给出本次可以读取的输出范围，len 以字节计。库把指针和长度交给回调，不转移窗口的所有权。

回调类型如下：

typedef unsigned (*in_func)(void FAR *, z_const unsigned char FAR * FAR *);
typedef int (*out_func)(void FAR *, unsigned char FAR *, unsigned);

in(in_desc, &buf) 返回字节数并设置 buf；零表示没有输入，此时忽略 buf。 out(out_desc, buf, len) 接收至多一个窗口的字节；零表示成功。若回调支持 NULL，描述参数可以为 NULL。

形式化约定

ZlibF.Spec.Public.Goal.inflateBackEnd

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

/-- `int inflateBackEnd(z_streamp strm)`.
Free only the state record. The caller's window is retained, even when it is a slice of another object. -/
def Goal.inflateBackEnd : Prop :=
  (∀ h, C.run (Zlib.Infback.inflateBackEnd none) h = .ok (Z_STREAM_ERROR, h)) ∧
  (∀ h r z, r.get h = some z → z.state = none ∨ z.zfree = .null →
    C.run (Zlib.Infback.inflateBackEnd (some r)) h = .ok (Z_STREAM_ERROR, h)) ∧
  (∀ h r i z s, BackValid h r i z s →
    ∃ after, C.run (Zlib.Infback.inflateBackEnd (some r)) h = .ok (Z_OK, after) ∧
      r.get after = some { z with state := none } ∧
      LiveChange h after (fun _ => False) (fun b => b = i) ∧
      Frame h after (fun b => StreamRoot r b ∨ b = i) ∧
      after.nalloc = h.nalloc ∧ after.nextBlk = h.nextBlk)