快速解码：余量、历史与源比特

快速路径把“读一个符号、恢复输出、再读下一个符号”的过程批量放进一个紧凑循环，减少反复检查空间的开销。例如长度 6、距离 2 的匹配，仍要把已有 AB 扩展成 ABABABAB；加速不能改变逐字节历史复制的规则。证明先建立每轮足够的空间，再把循环恢复出的字节接回独立格式含义。

源文件：zlib/inffast.c；翻译：ZlibF/Zlib/inffast.c.lean。 契约术语是内部契约中的 I-if-*。 表谓词来自解码表构造。窗口不变量 W 见流式解码。

这是内部函数。带有 I-if-pre-* 前提的定理，并不能证明所有合法的 inflate 调用都会建立这些前提。源比特保持结果也需要与独立格式语义连接。 这些结果的当前范围见进度。

入口视图与循环不变量

先给本轮游标和计数命名：in 指向下一个输入字节，out 指向下一个输出位置；avail_in、avail_out 分别计数剩余可读输入、可写输出，单位为字节。hold 暂存已读入的比特值，bits 是尚未消费的有效位数。查表要多少位，与匹配要复制多少字节，是不同的计数。

I-if-pre-room 给出 LEN 模式、至少六个输入字节和 258 个输出字节的空间， 以及外层 inflate 调用在同一输出对象中已经产生的、可读的输出前缀。 输入与输出不相交。I-if-pre-bits 给出 bits < 8，并说明 hold 恰好保存这些低位缓冲比特。 I-if-pre-tables 提供已初始化且具有正确含义的根表、子表项。 I-if-pre-window 提供有效历史，以及默认的合理距离检查模式。

代码用两个停止界限减少循环内检查：last 配合严格小于条件保证下一轮仍有六个输入字节，end 保证仍有 258 个输出字节。start 是外层调用开始时的输出容量；beg 据此找回这次外层调用的输出起点。

源代码形成以下表达式：

last = in + (avail_in - 5)
end  = out + (avail_out - 257)
beg  = out - (start - avail_out)

这里 beg 是外层调用输出的起点，不一定是本次快速调用输出的起点。 前置条件必须针对实际缓冲区视图，证明该指针减法有依据。 用 in0、out0 表示快速调用的初始游标。

在每次循环体入口使用以下命名不变量：

首个循环体由 do 循环直接进入，因此入口前提必须直接提供所需余量。 后续循环体依靠 in < last && out < end。

比特数与六字节界限

长度／距离符号通常由码字和附加位组成。码字先确定一个基值，再读取指定数量的附加位来细化数值。下表的 op 在补充位置表示所需的附加位数；R1 到 R4 是本节给这四处补充操作起的编号。

一个长度／距离对有四个补充输入的位置。

如果跳过 R1 或 R3，就已经有至少 15 位。表项含义保证完整码字连同可能的子表查找 至多需要 15 位。R2 提供至多五个附加位所需的比特；R4 提供至多 13 个。 所以，每次 bits -= op 都只移除已有比特。补充操作保持 I3，相应移位也不超出机器位宽。

分别取各处最大值似乎允许读取七个输入字节，但这种组合不可能出现。 假设 R1、R2、R3、R4 分别读取 2、1、2、2 个字节。R1 之后再消费至多 15 位的长度码， 至少留下一位。R2 之后再消费至多五个长度附加位，至少留下 1 + 8 - 5 = 4 位。 R3 之后再消费至多 15 个距离码比特，至少留下 4 + 16 - 15 = 5 位。 而 R4 要读取第二个字节，第一次补充前必须不足五位，因为第一次补充后仍不足 op ≤ 13 位。 矛盾。

因此每个循环体至多读取六个字节。这解释了 last 中减去五个字节的原因。 字面量写一个字节；按照长度表的基值／附加位含义，匹配至多写 258 个字节。 这解释了 end 中减去 257 个字节的原因。空间界限依赖表语义，不仅依赖已分配的表容量。

表读取

根表先用一小段低位比特查出叶子或子表链接。rootbits 是第一次查表使用的位数，因此表有 2^rootbits 项；掩码 (1 << rootbits) - 1 只保留这些低位。前文 T2 是成功解码表的语义契约，不只是“表已分配”。

根索引 hold & ((1 << rootbits) - 1) 小于 2^rootbits。T2 提供对应的已初始化表项。 链接项提供有界子表区间，掩码后的子索引位于其中。表谓词还必须建立表项的操作、码长、 基值／附加位范围，并说明第二级表项不会再次成为链接。 于是 goto dolen／dodist 路径至多经过一次链接查找就终止。

保留符号必须到达正确的错误出口。块结束符必须到达调用者契约规定的模式转换。 这些出口仍需准确的游标、位缓冲区和状态效果。

匹配复制：F3 与 F4

复制先判断来源在本次已写输出里，还是在先前调用保留的窗口里。done 是本次外层调用已产生的字节数，dist 是解出的回退距离，len 是此次需恢复的字节数；三者都按字节计数。历史窗口的 wsize 是容量，whave 是有效历史数量，wnext 是下次写入的环下标。

令 done = out - beg，解出的距离为 dist ≥ 1，匹配长度为 3 ≤ len ≤ 258。

若 dist ≤ done，源起点为 out - dist ≥ beg。复制按顺序进行：第 k 步的源是 相对位置 k - dist 处已经产生的字节。即使源、目标区间重叠，源字节也先于目标。 这正是 DEFLATE 的重复规则；用不相交复制的论证替代循环会丢失该含义。

例如本次已经写出 2 字节而回退距离为 5，还需要从旧窗口向前找 3 字节；这个差值就是下一个分支的 op。这里同名 op 已改为字节数，不再表示查表阶段的附加位数。

若 dist > done，令 op = dist - done。合理距离检查拒绝 op > whave。 检查通过后，1 ≤ op ≤ whave ≤ wsize，所以已分配窗口包含所需的先前历史。 有三种源区间形状：

每段只复制其历史字节数与剩余匹配长度中的较小者。如果窗口部分不足以覆盖整个匹配， 剩余源位于本次调用已产生的输出中，可以应用顺序复制论证。 必须证明展开循环的准确迭代数，包括每个 do … while (--op) 的初始计数为正。

F4 说明，whave < wsize 蕴含 wnext = whave。环未填满时，只可能出现第三种形状， 其源位于已初始化历史中。环已填满时，所有字节都属于历史，跨环末尾的形状也有效。 更强的功能不变量必须把这些字节对应到逻辑输出与字典历史的后缀。

回退与最终写回

为快速查表，循环可能读入尚未消费的整字节。离开前要把这些字节归还给调用者，否则外层解码器会跳过它们。下面局部 len 计算可以归还多少完整字节；它在此处不再表示匹配长度。右移 3 位等价于对位数除以 8 后取整数部分。

退出时归还预读但未使用的完整输入字节：

len = bits >> 3
in -= len
bits -= len << 3
hold &= (1U << bits) - 1

如果本次快速调用读取了 B 个字节，计数不变量给出 bits ≤ bits_entry + 8B < 8 + 8B。因此 len ≤ B，回退不会越过 in0。 结果保留的缓冲比特不足八位，所以最终掩码移位有效。 随后函数把准确的剩余输入／输出计数和游标、hold、bits、到达的模式写回流。

bits_entry < 8 至关重要。没有它，回退可能归还本次快速调用从未读取的字节。 未完成的证明步骤： 主解码器在每次实际转换／调用进入快速路径时都建立该前提， 包括恢复调用，以及固定／动态表安装。仅对补充／丢弃宏作一般观察还不够，必须检查这些路径和缓冲区视图。

从安全到解码含义

“源出处”回答每一段已消费比特来自原输入的哪里；“格式语义”回答这些比特表示哪个符号。二者要在同一次运行中连接起来。例如，距离码的几位来自正确输入位置，并不单独保证复制循环输出了正确的历史字节。

功能循环不变量必须把已消费的低位比特对应到原始源比特流，并把发出的字面量／匹配 对应到独立格式符号。该关系必须经过长度／距离选择、附加位读取、所有复制形状、 链接表、结束与错误出口、回退及最终写回而保持。 源关系必须在整个循环体和整个调用的组合中保持，不能只覆盖局部成功解出的一个符号。

内部源出处引理可以在其声明的定义域内，确定所选比特的准确来源。 把它们连接到初始化所建立的状态、已安装的表、所有合法调用者视图及独立输出语义， 仍是单独的细化义务。解出一个符号所依赖的比特，并不会自动证明更远的推测性预读合理； 其因果区别见 inflate。

终止性方面，每个循环体至少写一个字节，或通过结束／错误出口退出。 有限输出范围限制继续执行的循环体数量。复制循环与链接查找也各有有界度量。 应把这些界限换算到实际执行步数预算预算，并在所有出口保持帧性质。 这里不分配内存；现有状态／窗口的所有权不变。

与 C 的对应检查

快速解码器：余量、复制与回退

inflate_fast 在 LEN 模式进入，输入至少六个字节，输出空间至少 258 个字节， 满足 start ≥ avail_out，缓冲比特少于八位。inflate 检查这些余量。 inflateBack 检查字节余量，但依靠模式转换保证 bits < 8： 这部分模式转换证明未完成，其中包括动态表与存储块。

last = in + (avail_in - 5) 与 end = out + (avail_out - 257) 使用无符号减法。 其安全性依赖入口余量。每次迭代至多读六个字节、写 258 个字节。 beg = out - (start - avail_out) 表示本次调用输出的起点。 两个调用者分别把 start 设置为原始输出空间或回调窗口大小。

这里 here 是表项指针，而慢速解码器会复制表项值。 dolen 与 dodist 保留链接的向后跳转。有效表限制链接深度；翻译中的执行步数预算本身并不证明终止。 错误和块结束时的 break 跳过循环条件。该条件及最终计数中的指针比较必须发生在同一对象内。

从窗口和当前输出复制时，必须保留源代码展开后的循环以及读写顺序。 输出匹配的重叠是有意的：新写字节可以被后续复制步骤读取。 不能改成 memcpy，也不能改成初始源区间的快照。 最小匹配长度为三。每个前置递减复制循环都需要正计数。

每个出口，包括无效符号与距离过远的出口，都会在收尾阶段归还完整的未使用输入字节， 只保留低 bits mod 8 位，并写回指针与剩余计数。 语义证明必须跟踪该回退过程中准确的源比特前缀，不能只跟踪消费字节数。