解码表：从码长到已初始化表项

解压器拿到的是各符号的码长，随后需要一张能从比特前缀查出符号的表。例如长度为 2 的码字放在宽度为 3 的根表中时，剩余的一位还未属于当前码字；两个对应槽都应返回同一符号。建表证明要说明这种重复填充既不越界，也不会混淆符号。

源文件为 zlib/inftrees.c，翻译为 ZlibF/Zlib/inftrees.c.lean。内部术语是内部契约的 I-it-*；数学目标是格式指南的规范码关系 F-code-*。

核心证明分三层：码长描述规范前缀码；构造写入有界表；实际堆表项实现该码，包括无效标记。只有最后一层才能支持 inflate 和 inflate_fast 使用的表谓词。下文是证明策略；进度记录各项执行连接的状态。

定义域与结果

建表处理三种字母表：CODES 描述“码长本身如何编码”，LENS 描述字面量及匹配长度，DISTS 描述匹配距离。“根宽”是第一次查表取多少比特，不是表项数量；宽度 r 对应 2^r 个槽。work 是排序符号时使用的临时数组。

I-it-pre-lens 提供 0..15 范围内的可读码长。对 CODES，码长最多 7，请求根宽至少 7。I-it-pre-codes 对 CODES、LENS、DISTS 分别将符号数限制为 19、288、32。I-it-pre-work 提供可写且不相交的暂存区。I-it-pre-table 提供可写表／根宽单元，以及按类型分别容纳 128、852、592 项的不相交表区域。

安全目标在旧笔记中叫 T1：在这些内部前提下，每次返回都终止且无故障；0 表示成功，-1 表示码长无效，1 表示表容量不足。准确契约必须描述各返回的部分写入和参数单元效果。失败不承诺堆不变。

成功表目标 T2 给出根表／子表项覆盖、有界链接，以及每个可达表项的含义。全零码长和允许的单符号不完整码需要明确分支。调用者还需要实际指针推进与返回根宽。

计数与 Kraft 检查：F1 和 F2

先按码长分组。这里 l 是比特长度，c_l 是恰好使用该长度的符号个数，m 是所有有码符号的总数。码长零表示该符号未使用，不进入规范码分配。root 是根表宽度，min、max 是实际出现的最短和最长正码长。

令 c_l 计数正码长 l 的符号，m = Σ c_l；当 m > 0 时，min、max 是首尾非空码长。将请求根宽限幅后，得到 min ≤ root ≤ max ≤ 15。

规范分配给相同长度的符号连续编号，进入更长长度时再左移补零。B_l 是长度 l 的第一段编号起点；left_l 是分配完长度不超过 l 的符号后，在 l 位空间里还剩多少位置。它们分别用来证明“码字按序生成”和“码空间没有超额使用”。

长度为 l 的首个规范码定义为：

B_l = Σ_{1 ≤ j < l} c_j 2^(l-j)
B_1 = 0
B_(l+1) = 2 (B_l + c_l)
left_l = 2^l - B_l - c_l

例如只有两个长度为 1 的符号，c_1 = 2，可用位置恰好是二进制 0 和 1，余量为零；若有三个这样的符号，就需要把三个符号塞进两个位置，余量变为负数，必须拒绝。这是下面 Kraft 检查的直观含义。

有符号 Kraft 循环保持 left_0 = 1 与 left_l = 2 left_(l-1) - c_l。结果为负时拒绝。因此通过检查可得 B_l + c_l ≤ 2^l，每个分配的长度 l 编码都可放入 l 位。证明还必须界定有符号中间值。

最终的不完整码检查仅在类型不是 CODES 且 max = 1 时允许正剩余。此时非空不完整码恰好只有一个长度 1 的符号。这个例外对覆盖论证必不可少；它并非完整 Kraft 划分。

排序要给每组码长一段独立临时空间。offs[l] 是长度 l 这一组在 work 中的起点；i 是该组内从零开始的序号；codes 是调用者提供的符号总数。这样先证明每组有自己的槽，再证明后续建表读到的是正确符号。

计数偏移从 offs[1] = 0 开始，满足 offs[l+1] = offs[l] + c_l。码长 l 的第 i 个符号写入 work[Σ_(j<l) c_j + i]，其中 i < c_l。索引低于 m ≤ codes。不同符号占不同槽，因此 work[0..m) 已初始化，并按 (length, symbol) 排序。这就是 F2：它同时给出之后读取 work[sym] 的索引界限与含义。

反转码遍历

DEFLATE 的码字查表要配合按低位先进入寄存器的输入顺序。len 是当前符号的码长，huff 保存对应的反转码值，i 表示当前长度组内的符号序号。反转不是改变符号：例如把两位 10 反转成 01，只是换成适合低位索引的表示。

令 rev_l(v) 反转 v 的 l 位。主循环不变量把当前符号识别为 huff = rev_len(B_len + i)，并给出 huff < 2^len。

首个正码长的首个规范码为零。同长度后继中，下降掩码清除反转字的前导一并设置下一个零，正好对应普通二进制递增的反转；若全为一则回绕到零。下个非空码长更大时，规范递推在普通码低端追加零；反转后这些是高端零，因此 huff 在新位宽保留正确值。

完整码的最后一个普通码是 2^max - 1，最终反转递增得到零。单符号例外中结果为 1。这些事实决定是否执行尾部无效标记写入。

复制填充与子表大小

若当前码字比根表宽度短，根索引的高几位不属于当前符号，必须允许任意取值。举例 len = 2、root = 3、反转码值 huff = 1，索引 1 和 5 的低两位同为 01，都应返回该符号。下面的填充序列枚举的就是这种槽位。

对 len ≤ root 的根表项，填充循环写入索引：

huff + (2^root - 2^len), …, huff + 2^len, huff

因 huff < 2^len，所有索引都低于 2^root。递减计数器 fill 从 2^root 开始，每次先减去步长 incr = 2^len，再写入一项。由于 len ≤ root，初值能被步长整除，恰好经过 2^(root-len) 次写入后减到零，不会回绕。这个写入项数与步长是两种量：上面的两位码／三位根表例子，步长为 4，实际写两项，依次是索引 5 和 1。这些恰是低 len 位匹配反转码的索引。

长码不能在根表中直接完成。p 是根宽部分的前缀，curr 是子表还要读取的位数，left 是当前深度尚可填入的子表槽数。这里的 left 是子表局部计数，不能与前面检查整个码空间的 left_l 混用。

对 len > root，根前缀 p 将连续普通规范码分组。大小循环从 curr = len - root、left = 2^curr 开始，减去当前深度的剩余计数，下降时将空闲槽翻倍。若该深度剩余码少于 p 下空闲槽，这些码全属于 p；若填满槽，则该深度下此前缀完整。循环也在 max 停止。计数论证必须说明 p 下每个码都满足 len - root ≤ curr。

drop 记录已经由根表消费的位数，所以剩余码长是 len-drop。移位 huff >> drop 去掉根前缀后，才得到子表使用的码值。子表宽度则是 curr，可以比剩余码长大；此时仍需要重复填充。

随后取 drop = root，在 2^curr 表内按 2^(len-drop) 步长重复填充，实际写入 2^(curr-(len-drop)) 项。这里步长仍按表项下标计数，写入次数由表容量除以步长得到。整除性和 huff >> drop < 2^(len-drop) 给出与根表相同的界限。前瞻计数在最终深度可能包含后续前缀的码；证明必须说明其停止条件对当前前缀仍充分。

容量与指针构造

根表和各子表在同一片表存储中前后排列。used 计数已预留的表项数，next 指向正在填充的表。公式中把初始输出表指针 *table 记为 base；这是本文的基址记号，与源码另一个名为 base 的长度／距离基值指针用途不同。表容量及两个表指针之间的偏移均按表项计数，而不是按字节计数。

used 初值为 2^root，随后逐个增加子表的 2^curr。当前 next 指针等于表基址加此前各表容量。LENS／DISTS 检查在新子表写入或链接之前拒绝超过 852／592 的容量。检查之前的指针构造和算术仍需从先前预留得到自己的末尾后一位置界限。

CODES 没有这种容量检查。其更强码长／根宽前提保证 max ≤ 7、root = max，因此不打开子表，最多使用 128 项。其他类型的守卫论证不能替代此调用者前提。

常量 852、592 来自穷举表大小分析。若检查前所有操作安全，明确的容量检查足以证明所选构造的安全。但要证明每个格式有效的码都被接受，还需独立界限；安全的容量拒绝本身不能证明这种完备性。

根链接使用 low = huff & (2^root - 1) < 2^root，存储子表宽和偏移 next - base。必须证明偏移适合其 16 位字段，链接区间位于已预留表内。

覆盖与含义：T2

“覆盖”要求每种可读比特前缀都找到正确结果，而不仅是下标不越界。长度 len 的码字占二进制码空间的 2^-len 份额；完整前缀码正好把整个空间分完。下文把这个数学划分对应到实际被写过的根表和子表槽。

完整码中，宽度为 2^-len 的叶区间划分码空间。根表项或者属于某个短叶，由复制填充写入；或者包含更长叶，由首个成员创建并链接子表。子表内应用相同区间论证。不相交叶区间阻止不同符号给同一表项赋予冲突含义。

单符号不完整码中，root = 1：循环写表项 0，尾部将表项 1 写为无效。没有有码符号时，独立分支写两个无效项，返回宽 1，并将表指针推进两项。两者都不能假装码完整来证明。

实际表项还告诉解码器如何继续：bits 是本次查表需要消费的位数，val 是字面量、基值或子表偏移，op 区分字面量、附加位、链接、结束或无效情形。数值字段必须与所构造符号一致；读到一个已初始化的任意表项仍不足以正确解码。

覆盖本身不够。须证明 op、bits、val 的解释：字面量、长度／距离基值加额外位、块结束、无效标记或子表链接。建立跨链接的总码长界限，以及二级表项不再是链接的事实。inflate_fixed 安装的固定表也需要相同读取谓词，包括保留的无效符号。

其他局部条件

下表把 T1 的安全要求和 T2 的表项含义落实到每一种实际操作。

纯规范码引理放在 ZlibF/Math/。将它们联系到翻译后的存储、全部退出和已安装解码器不变量，属于执行证明。方法说明调用者如何在不假设被调用函数契约的情况下建立这些前提。

C 对应检查

解码表与标志

code 有字节字段 op、bits，以及 16 位 val。默认表容量为 ENOUGH_LENS = 852、ENOUGH_DISTS = 592，合计 1444。码长最多 15。码长排列为 16,17,18,0,8,7,9,6,10,5,11,4,12,3,13,2,14,1,15。

标志测试顺序很重要。慢速字面量／长度解码器先测试块结束，再测试无效性。快速解码器按源顺序测试字面量、长度、链接，再处理块结束／无效退出。任意满足安全形状的表，不足以证明交换这些测试正确。语义对应需要实际构造或固定表提供兼容叶标志。DIST 缺少 LEN 使用的 op != 0 守卫；只有距离表不变量才能使之安全。CODELENS 不检查 op 就读取 val。全零字母表产生两个 val = 0 的无效项，解码最终在缺少块结束符检查处失败。

固定表复制自 inffixed.h：512 项字面量／长度表和 32 项距离表，根宽为 9、5。通过 inflate_table 重建会改变四个字面量／长度表项，索引为 99、227、355、483。生成的无效标志是 68 或 193，头文件使用 64。它们都拒绝保留符号，但逐字节忠实性要求采用头文件值。旧文档关于 inflate.c 的 fixedtables 内表的引用已过时。基值／额外位数组和排列是索引常量。错误消息须保留为可读的只读字符串块，因为调用者可以检查 strm->msg。

inflate_table

按源顺序保留计数、Kraft 检查、排序、填表和尾部。码长位于 0..15、足够的 lens／work 空间及表容量，是调用者必须建立的内部前提；函数自身不验证全部索引。没有有码符号的情形写入两个无效项，更新两个输出参数，再返回成功。过度订阅或不允许的不完整字母表返回 -1。容量耗尽返回 1，此时可能已写入表项。

翻译按值传入 *table、*bits 并返回新值。错误保持这两个标量值，但不撤销表项写入。调用者必须在每条返回路径保留此区别。CODELENS 中，lencode 在长度表调用之前赋值；distcode 在距离调用之前由推进后的 next 赋值。调换任一赋值都会改变堆历史。

保留这些算术细节：

• count、offs 是 16 位数组，具有 C 提升和窄化。
• left 为有符号，包括其移位和减法。后面的 1 << curr 为有符号表达式，前面的 1U << root 为无符号。
• min 在 min = fill 处改变含义，此后保存当前表大小。
• fill -= incr 与调用者最后的 while (copy--) 保留无符号行为。
• 根链接存储窄化为 16 位的指针差。其索引和移位界限依赖规范码构造，把规范码构造对应到实际堆写入的证明尚未完成。

慢速查找与格式错误的前瞻

即使名义根宽尚不可用，根查找仍可选择表项，只要该项自身消费长度适合已有前缀。所需性质是：未来后缀位不会改变当前选择。链接需要对应二级查找与两段消费长度。仅内存界限不能建立符号含义。

已取入输入与已检查输入不同。解码器已具有足够已检查位来证明字面量或匹配时，仍可能取入格式错误的未来位。要求每个已取字节都有有效续接是错误的。因果模型改用具有有效补全的已检查位前缀，并要求输出与每个兼容补全、每个仍允许的字典一致。未知包装字典不能被悄悄替换为空字典。这是规范区别，不授权改变补充顺序。见 API 契约和证明说明。

更早固定八字节错误检测延迟也存在反例。不能把它当作源代码不变量，也不能仅增大常量来修复。当前状态属于进度。