编码构造的证明思路

Huffman 构造的证明要把“数组里得到了一组数值”连接到“解码器按这些数值读回原符号”。树构造和码长两章给出了计算过程；本章沿着同一过程，解释每次合并、字段复用和码长修复需要保持什么，以及局部 Lean 结果如何接到块编码。

先说承诺，再看它怎样失败

输入仍是四符号频率表 A:8、B:4、C:2、D:2。期望输出是实际数组中的码长 1,2,3,3 和相应存储码字 0、1、3、7；按低位先行读出后，规范码字是 0、10、110、111。还要有一段描述，能让接收者恢复相同码长。构造器不能只返回“某棵合法树”：它必须覆盖输入中真正用到的符号，并把这些结论落实到返回的同一片堆内存。

用 C 的码字做一个完整的局部检查：存储整数 3、长度 3 产生到达顺序 110。在它后面接 B 的 10，得到 11010；独立解码器应返回 C，并原样留下后缀 10。再读后缀才得到 B。这就是符号级正确性要保留的边界。

现在看三个反例，它们各自指出必须补哪条证明：

证明的输入前提包括选择字母表与最大位长度的有效描述符、内嵌数组容量、静态表和相关位缓冲状态。证明的输出结论要同时覆盖无故障执行、实际码长／码字含义及所声明的保持性。完整调用者仍必须建立这些前提；不能先假定初始化和所有中间调用都已提供它们。精确边界见安全要求和树组件论证。

队列背后的森林

先解决表中第一种错误：四片叶子必须各出现一次，且后来的每个父节点确实连接选中的两棵子树。证明因此从扫描开始，而不是预先假设有一棵合法树。扫描建立有效字母表，清零未使用码长，并初始化 depth。这个数组保存已经组好的子树高度，以边数计；叶子从高度零开始，它并不是叶子距离最终根有多深。人工叶子循环改变准备后的集合和成本字段。表示关系要保留这段历史，避免后来把人工频率一误算成额外的输入符号。

合并过程中，可以把有效队列解释为一片森林的根。各子树的叶子身份彼此分离，合在一起正好是准备后的字母表。删除两个不同的根、加入一个新父节点，会保持这个并集。选中的节点还必须确实来自旧队列；一个仅仅落在数组范围内的整数，也可能指向无关的内部节点。

在算例第一轮，旧森林是 {A}、{B}、{C}、{D}，新森林是 {A}、{B}、{C,D}。第二轮变成 {A}、{B,C,D}，第三轮只剩 {A,B,C,D}。这说明“森林”不只是图的名字：它记录每个根下面究竟有哪些原始符号，正好排除重复 C、漏掉 D 的反例。

另外两组事实各有用途：堆顺序说明为什么选中的是源码频率／深度比较下的最小根；父关系和成员关系说明最终为什么得到完整的树。只限制索引范围，不能建立其中任何一种含义。队列修复例程 pqdownheap 在数组槽位之间移动节点编号，恢复最小权重优先的顺序。因此，它的证明要在恢复顺序时保持节点排列，合并证明则要沿着每次实际存储传递旧森林。

局部的 ws_build_tree_complete 组合实际准备、建堆、码长限制和编码分配路径。它的前提涉及选中的描述符指针、数组容量、静态表和相关内部存储，没有把所调用辅助函数的执行契约当作假设。辅助函数各有执行证明，在上一步产生的中间状态上应用。公开调用能否到达这个内部状态，以及整个压缩器最终产生什么，是另外两段连接。

保留顺序与机器边界

这一阶段的承诺是：保留的节点以后能安全地转成码长。即使所有地址都在界内，若孩子早于父节点被访问，就可能读到联合字段中的旧父编号，而不是本轮的父码长。

用 K 计准备后的叶子数，包括必要的人工叶子，用 t 计完成的合并次数。每次合并把两个有效根换成一个：四符号例子中 K=4，完成 t=1 次合并后剩三棵根；一般就是 K−t 个有效堆条目。每次合并的两个节点则保存在数组高端区域。这段数量记账证明两个区域保持分离，下一个内部节点编号也能装入选中的树数组。以后对叶子码长求和时，还要再次使用成员关系和不同节点的身份：如果保留区域中某个条目重复，就可能把一片叶子算两次，同时漏掉另一片。

保留顺序还要保证第一遍码长计算先访问父节点，再访问孩子。节点字段 Dad 先保存父编号，随后同一存储被复用成保存位长度的 Len。因此，读取 Len(parent) 必须是在读取这次刚分配的父码长，而不是留在联合字段中的旧父编号。更早阶段的子树高度初始化也有同样的问题。字段复用要成立，证明必须跟随字段含义的变化。

先给片段中的存储量命名：s 指向压缩器状态，s->heap 是节点编号数组；heap_max 标记数组高端保留区域的起点，先减一就空出一个保存槽位；n、m 是选中的节点编号。为什么实际顺序有用，可以直接对照固定源码。每次合并把两个选中编号写向数组低地址方向，见 trees.c:677–678：

        s->heap[--(s->heap_max)] = n; /* keep the nodes sorted by frequency */
        s->heap[--(s->heap_max)] = m;

第一轮的 C、D 留在尾端；后来取出的 CD、BCD 等祖先会写在更靠前的位置。再把最终根写到最前，向前遍历便先遇到祖先。下一遍中，h 是保留数组的槽位，n 是从该槽位取出的节点编号；tree[n].Dad 是它的父编号，父节点的 Len 是已经分配好的位长度。局部变量 bits 计算孩子的码长，max_length 是以位计的上限；overflow 统计计算结果需要被截断的节点。实际码长读取逐字见 562–565 行：

        n = s->heap[h];
        bits = tree[tree[n].Dad].Len + 1;
        if (bits > max_length) bits = max_length, overflow++;
        tree[n].Len = (ush)bits;

例如读 B 时，Dad 指向 BCD，已经写好的 BCD 码长为 1，故 B 得到 2。最后一行会覆写 B 的旧 Dad；证明必须在这次覆写之前用完该父链接。这也解释了为什么保留顺序能省去另一次递归树遍历，却带来较强的表示义务。

频率求和和子树深度还会跨越机器宽度。若无符号加法可能回绕，就不能把自然数权重定理中的和直接套进去。字节大小的子树高度也需要范围论证，才能在频率／深度估计中作为没有界限的数学高度使用。F7 论证指出这些要求。它们也解释了：对同一个构造器，编码合法性的证明与更强的前缀成本证明，可能需要不同的信息。

用守恒量解释修复

先用 L 表示允许的最大码长，单位为位：字面量／长度和距离码取 15，小型码长字母表取 7。这里的承诺是把“最多 L 位”与“仍可解码”同时满足。上一章的五符号反例 1,2,3,3,3 虽都不超过教学上限 3，却占用 9/8 的编码空间；所以证明不能在截断后结束。

码长修复的关键来自完整树，而不是任意直方图的一般性质。完整二叉树的每个内部节点都恰有两个孩子。长度 b 的码字占二进制路径空间的 2^-b，把所有叶子的份额相加，就是 Kraft 和；完整树的这个和为一。教学码长 1,2,3,3,3 给出 1/2+1/4+3/8=9/8，因此放不下。

考虑深度恰好为 L 的一个内部节点，它下面有 a 片叶子。把这些叶子都截到长度 L，会使这棵子树的贡献从 2^-L 变成 a×2^-L，多出 (a−1)×2^-L。这棵完整子树在根以下恰好有 2a−2 个节点，源码的超限计数遍历会把它们全部计入。

对这些互不相交的深度 L 子树求和，得到：

clamped_Kraft = 1 + (overflow / 2) × 2^-L

它同时解释了超限计数为什么为偶数，以及一次修复为什么对应两个超限计数单位。例如 L=3、某棵深度三子树有四片叶子时，原来的编码份额是 1/8，截断后变为 4/8，多出 3/8；它在根以下的六个节点贡献计数 6，正好需要三轮各移除 1/8 的修复。这里 b 表示一个短于 L 的非空码长类别。把一个 b<L 的编码分裂成两个长度 b+1 的孩子，保持 Kraft 权重；删去一个长度 L 编码，恰好移除 2^-L。叶子总数不变。教学例子中，超限计数 2、L=3 对应多出的 1/8，一轮修复便将其移除。

循环仍然需要实际的安全和终止论证。只要超限计数为正，就一定存在一个较短的非空类别；否则所有叶子都具有长度 L，正的超额将要求叶子数超过 2^L，与描述符的字母表容量矛盾。最长类别也必须有足够条目供减法使用，反向分配扫描则必须恰好遇到所需叶子。这些事实解释源码的搜索和减法为什么能够执行，不能直接把搜索成功当作前提。

局部的码长结果把这段记账接回数组单元。GBDone.symbolic_lengths 从保留节点的位置转成按符号编号描述的码长和计数。这个重新索引依赖森林中叶子身份的唯一性。准备阶段用 max_code 记录纳入的最大符号编号。覆盖整个字母表的码长结论还包括这个编号以上的条目：它们的零长度，也要来自实际准备与保持步骤。

从存储码字到解码

现在的承诺是刚才的 11010 检查对每个使用符号、每个后缀都成立。表中“不反转”的反例说明，仅有合法码长还不能推出这个结论。

编码分配例程 gen_codes 使用一张直方图，也就是“每种位长度有多少个符号”的计数表。即使这张表没有正确统计数组中的实际码长，它仍然可以执行自己的运算。这时，精确的执行描述也只是忠实地描述了错误数据。因此，语义正确性还需要前一阶段的直方图／码长关系，以及修复建立的完整编码性质。

把这些事实连接起来后，起始码字递推与按符号顺序分配，才能与独立格式的规范编码规则一致。恰好反转正码长对应的位，再把低位先行存储的整数接到高位先行的规范码字上。覆写码字单元时，码长本身和无关字段保持不变。

这个结论可以写成一个很有用的符号级形式：把使用过的符号的实际存储位后接任意后缀，独立解码器都返回该符号，并原样保留后缀。build_tree_decodable_initialized 在明确的内部前提下给出这样的实际构造器结果：TreesRun0 固定描述符指针和位缓冲事实；DeflateState.WellFormed 固定内嵌数组大小；静态表事实提供描述符数据。这些前提必须在实际调用构造器时成立。仅引用 deflateInit 的名字，并不能建立调用点的前提：初始化结果，以及中间各次调用的保持性，需要提供这段连接。该定理讨论各棵构造树及其使用符号，没有声称动态编码块已经发送头部、选择了正确记录，或完成公开流。

描述一致性与输出预算

接收者必须恢复编码器实际使用的码长，才谈得上解码载荷。描述中的指令有的直接给出码长，有的表示重复。指令 16 表示“把前一码长再重复 3–6 次”，随后的两位额外值保存重复次数减 3。例如四个 3 应由 3,16(extra=0) 恢复：直接给出的 3 加上三次重复，恰好四项。若第二遍把额外值发成 1，就会恢复五项；每条指令仍各自合法，后面的树边界却错了。因此还需要“描述相同序列”的承诺。

下一段连接跨越 scan_tree、小型码长树和 send_tree。扫描为每条指令统计的频率，必须对应实际发射时会用到的指令。两次执行可以关联到同一个游程状态：此前码长、下一个码长、当前计数和阈值。哨兵必须让最后一个游程结束，却不能把它自身当成 19 符号码长字母表中的值。

对符号 16，此前必须已经解出码长，额外值也必须正确表示三到六次重复。指令 17、18 表示零游程：17 用三位额外值指定 3–10 个零，18 用七位额外值指定 11–138 个零。它们的额外字段必须还原对应的零个数。直接码长与游程展开合起来，要按原顺序得到原码长序列，且总数符合宣布的计数。小树的编码合法性和精确比特追加，再把这些指令连接到发出的字节。

现有 send_tree_emit 把实际发射连接到基于游程的比特序列。它明确要求码长可读、实际使用指令的码字能装入对应长度，以及足够的总比特空间。空间仍是内部调用者的义务；不能仅从描述本身合法，就推断存储一定足够。

这一点接到共享存储与输出证明。合法树建立不含歧义的编码含义；保护未读符号，还需要限制树描述位数和每个数据发射前缀。这个更强的估计必须使用实际频率、构造选择和修复影响，不能只靠 Kraft 合法性或最终整块大小比较。完整调用者与输出预算的组合证明尚未完成，需要把实际树频率、每个发射前缀和未读记录边界放进同一个执行不变量。项目进度记录接受范围；块选择则说明这些成本最终怎样回到实际编码决策。