inflateBackInit_
用途。 分配解码器状态并关联调用者的窗口。 inflateBackInit 宏提供 version 和 stream_size。
完整章节与共同规则 ↗c361e306c50783f5 · 对应提交的原文 ↗先看本函数的前置条件和返回结果；可展开下方共同规则，查看整组接口的缓冲区与所有权要求。
int ZEXPORT inflateBackInit_(z_streamp strm, int windowBits, unsigned char FAR *window,
const char *version, int stream_size);
用途。 分配解码器状态并关联调用者的窗口。
inflateBackInit 宏提供 version 和 stream_size。
定义域 受限定义域：有效调用者内存、未活动的流和默认分配器。
前置条件 非 NULL 的 strm 指向可写 z_stream，其 zalloc、zfree 和
opaque 已初始化。使用 NULL 或默认分配／释放函数对；不得覆盖仍活跃的库状态。
非 NULL 的 version 的首字节可读。在初始化路径上，window 提供与流分离的
2^windowBits 个可写字节。该切片须保持存活直到结束操作。
内存与状态效果 可能初始化分配器字段和 opaque，清除 msg，并分配一个状态。
窗口仍由调用者拥有，此处不分配、不清空，也不释放窗口。
返回与保证 Z_OK 关联供 inflateBack 使用的新状态，且 8 <= windowBits <= 15。
输入／输出指针、可用计数、累计计数、adler 和 data_type 不变。
只初始化指定的状态字段；该状态须用于回调 API。
错误路径 NULL 版本、主版本字节不同或流大小错误，会在访问流前返回 Z_VERSION_ERROR。
NULL strm／window，或位数不在 8..15 内，返回 Z_STREAM_ERROR。
分配失败返回 Z_MEM_ERROR：msg 和默认分配器字段可能已改变，但保留原 state 字段。
没有分配状态，因此在此未活动流定义域内，初始化失败后不需要结束调用。
本组共同前提与范围
回调接口允许调用者提供输入块，并直接从窗口接收解码输出。 先用 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.inflateBackInit_
证明状态：已登记证明 · 证明记录与剩余工作
/-- `int inflateBackInit_(z_streamp strm, int windowBits, unsigned char *window,
const char *version, int stream_size)`.
The caller retains the window. Only the state record is allocated; its other integer fields
remain arbitrary. Refusal precedes allocation, and allocation failure retains the old state field. -/
def Goal.inflateBackInit_ : Prop :=
(∀ h p wb window version head size, VersionValue h version head →
(head ≠ some 49 ∨ size ≠ 112) →
C.run (Zlib.Infback.inflateBackInit_ p wb window version size) h = .ok (Z_VERSION_ERROR, h)) ∧
(∀ h p wb window version, VersionValue h version (some 49) →
(p = none ∨ window = .null ∨ wb.toInt < 8 ∨ 15 < wb.toInt) →
C.run (Zlib.Infback.inflateBackInit_ p wb window version 112) h = .ok (Z_STREAM_ERROR, h)) ∧
(∀ h r z wb window version,
Fresh h → Zlib.Inflate.Spec.Uniq h → LibraryGlobals h → r.get h = some z →
DefaultOrNull z → VersionValue h version (some 49) →
8 ≤ wb.toInt → wb.toInt ≤ 15 → window ≠ .null → Writable h window (2 ^ wb.toInt.toNat) →
∃ rc after,
C.run (Zlib.Infback.inflateBackInit_ (some r) wb window version 112) h = .ok (rc, after) ∧
after.nalloc = h.nalloc + 1 ∧
if h.allocOk h.nalloc = false then
rc = Z_MEM_ERROR ∧ SameObjects (r.put h (preparedStream z)) after
else rc = Z_OK ∧
let z' := { preparedStream z with state := some (.inflate h.nextBlk) }
let s := backInitialState (h.garbage h.nalloc) window wb
BackValid after r h.nextBlk z' s ∧
Frame h after (StreamRoot r) ∧
LiveChange h after (fun b => b = h.nextBlk) (fun _ => False))