压缩输出的证明思路

我们希望算法给出一个可以继续使用的结果：压缩后的位流解码成已经接受的输入；尚未读出的符号和调用者的其他内存保持完好；输出空间耗尽后还能从同一状态继续。这些保证要同时成立。只算出一串看起来正确的压缩字节，还没有回答后两个问题。

用同一个例子定位可能出错的地方。选定符号 A、B、长度 6／距离 2，应该展开为 ABABABAB；最终固定编码应有 38 个有效位，对齐后为 73 74 82 40 00。证明需要把这条具体的变化过程推广到前提允许的所有符号、堆状态和调用历史。

这张表描述要建立的保证，不表示它们已全部完成。下面的局部定理各有明确前提；它们到初始化、完整块输出和公开调用序列的连接，仍要按各自范围核对。本章按表格顺序往下走：先说明记录代表什么，再说明怎样追加比特，接着保护下一条记录，最后把已经生成的字节交给调用者。当前接受状态只在项目进度维护。

flowchart LR
    Input["已接受的输入字节"] -->|"匹配与符号记录"| Symbols["字面量 / 匹配记录"]
    Symbols -->|"块编码"| Bits["DEFLATE 比特"]
    Bits -->|"位写入器"| Pending["待交付字节与缓冲位"]
    Pending -->|"交付"| Output["调用者输出"]
    Storage["保持未读记录"] --> Symbols
    Storage --> Pending

符号的含义

先回到第一个输出比特产生之前。字面量展开成它自己。匹配则从已经展开的历史里逐字节读取；读取距离不变，历史却会随着写入增长。因此，例子中距离只有 2 的匹配，仍然可以产生 6 个字节。

压缩器需要把这种展开与已经接受的输入联系起来。提交一个字面量后，符号展开多出同一个字节。提交一个匹配后，展开多出的那段内容，要由此前的匹配搜索给出字节相等的依据。延迟匹配中的暂存决策也要进入这个记账：把输入接收到 预读区（lookahead，已经缓冲、尚未作出匹配决策的输入），与最终提交一个符号，是两个不同的时刻，不能把它们的游标混为一谈。

接下来才把逻辑符号连接到实际记录。存下的三个字节必须能还原相同的距离，以及字面量或长度偏移；频率更新也必须统计这个符号。现有的 tr_tally_spec 在明确的空间和符号取值前提下，描述翻译后的符号记录究竟写了什么。它本身没有证明此前搜索选中的字节与输入相同。连接的这一段属于调用者。

发射时，读出的同一条记录要变成格式要求的编码和额外位。固定编码与动态编码使用不同的编码表；原样存储走另一条分支，直接复制原始字节。这些分支使用不同的中间表示，但最终可以满足同一个独立解码关系。Deflate.Valid 通过解码定义无封装格式的目标，成功的含义因此不取决于“压缩器碰巧写出了什么”。

精确的比特输出

先看跨界发送 B 的那一步：调用前，待交付字节区为空，寄存器的 11 位代表块头和 A；调用后，73 74 的 16 位已成为待交付字节，剩余 3 位在寄存器。两边都必须表示原来的 11 位后接 B 的 8 位，即同样的 19 位。这个等式说明我们为何需要同时描述数组和寄存器。

位写入器把抽象比特落到实际状态里。一些完整字节已经在 pending_buf 中，随后几位还在 bi_buf 中。这里 pending 是已缓冲完整字节的数量，bi_buf 保存后续暂存位，bi_valid 记录这些位的个数。把同时涵盖这两个位置的逻辑位序列叫作 outBits：

outBits = byte_bits(pending_buf[0 .. pending))
          ++ low_bits(bi_buf, bi_valid)

这里的式子用于待交付字节区从缓冲区基址开始的局部发射状态。byte_bits 按最低位在先展开每个字节；++ 表示先后拼接；low_bits(x,n) 只取 x 的低 n 位，按最低位在先排列。部分交付以后，尚未交付的区间要从实际 pending_out 游标读取，最后一节会把这个游标接入全局关系。

每个字节按低位在先展开。存储的 Huffman 码字则已经为这个写入器反转过。于是，一次 send_bits 最有用的结论是：返回后的序列，恰好等于旧序列后接这次要求发送的字段。比特从寄存字段移到字节数组，并不会改变它们的顺序。

定理中的 TreesInvAt 给一组具体的状态条件起了名字：状态和字节数组确实存在于当前堆中；待交付字节与符号记录的指针指向同一个可写分配的规定位置；树描述符指向相应数组；有效位数在 0 到 16 之间；缓冲区没有越过有效位的杂位；符号游标处在三字节记录边界内。它没有替调用者提供“本次追加仍有空间”或“未读记录不会被覆盖”的结论，那些需要另行建立。

实际的 send_bits_spec 分别处理“留在缓冲区”和“写出一个 16 位字、保留余位”两条分支。当前命题明确要求 TreesInvAt、0 到 15 之间的发送长度、能装入该长度的值，以及足够的比特空间。它给出实际无故障执行、返回堆上的同一不变量、精确追加的比特，并保证写入区间之外的字节不变。

这种局部结论可以交给下一次调用。EmitState.step 把实际发射组合起来：先追加 u，再追加 v，就得到 u ++ v。它同时传递返回堆和保持不变的字段，而不只传递一个比特等式。调用者使用的是辅助函数已经证明的执行结果，并在调用点建立它的前提；不能把“辅助函数遵守契约”直接当作未经证明的假设。

未读存储的保持

比特正确，还不足以说明剩余符号能够继续编码。写入器可能刚刚追加了正确字段，却破坏了下一轮需要读取的记录。

这里要比较同一共享分配内的两个字节偏移。B 是布局尺度，在状态中叫 lit_bufsize，也就是第一条记录的起点偏移。设 q 为已经完整读出的记录数，每条占三字节，因此下一条未读记录从 R(q) = B + 3q 开始。设 P(q) 为这些记录发射后，下一个空闲输出字节相对同一分配基址的偏移。证明必须让每次实际写入都避开未读后缀。项目采用的一个方便的充分边界是 P(q) < R(q)，并同时要求中间写入保持未读内容。边界恰好相等本身并不意味着发生覆盖；是否重叠，要看具体的半开写入区间。

回想上一章人为构造的前期集中写入方案。B = 8 时，读完第一条记录，未读起点变成 11。原本已有两个待交付字节，再写十二个字节后，下一个空闲位置变成 14。写入区间 [2,14) 与未读存储相交于 [11,14)。最终的 20 字节虽然装得进 32 字节的分配块，却无法恢复这三个字节。这说明归纳需要检查每个前缀，不能只检查最后一个。

固定编码块的数量关系比较直接：一个字面量至多 9 位，一个匹配至多 31 位。假设进入时没有待交付字节，且已有缓冲位至多 7 位。把三位块头和写入器的字节上界合起来，得到相应发射前缀的一个保守估计：

P(q) ≤ (7 + 3 + 31q) / 8 + 1

先统一单位。分子是位数：入口至多 7 位、块头 3 位、q 条记录至多 31q 位。除以 8 转换成字节；额外的 1 为暂存与取整留出保守余量。这里用有理数上界估计整数的字节数。

再比较两条边界的增长速度。每读完一条记录，读取边界前进 3 字节；输出的最坏预算却是 31/8 字节，多出 31/8 - 3 = 7/8 字节。q 条记录总共可能多用 (7/8)q 字节，入口还需 10/8 + 1 = 9/4 字节。只要初始间隔 B 能容纳这两项，即 (7/8)q + 9/4 < B，两条边界就仍然分开。

最后使用记录上限 q ≤ B−1。代入后，左边至多为 7B/8 + 11/8，因此 B > 11 足够；实际共享布局允许的最小 B 是 128。这个计算给出了充足间隔。把它接到程序时，还需要证明本次发射确实满足“入口无待交付字节、暂存位至多 7 位”等条件，并分别处理记录 0 之前的块头、各次中间写入、块结束标记和最终对齐。完整的 F9 论证 保留了这些具体义务。

动态编码的前缀成本

动态编码块在第一条记录之前，还要先发送树的描述。较早的符号也可能恰好使用长码。选择动态编码，是因为它完整的舍入成本优于固定编码；这个比较限制了总量，却没有限制昂贵的符号出现在什么位置。

需要的预算因此包含树描述，以及每个符号前缀的成本。仅靠 Kraft 不等式还不够。Kraft 描述合法的编码空间，而这里需要把码长与构造这棵树时实际使用的频率联系起来。

这一步需要进一步展开树构造算法。证明必须跟随优先队列的选择、节点合并、深度比较、码长限制与重新分配。数学上的频率与深度关系，只有在翻译后的构造器建立了那些前提之后，才能接到实际实现上。随后，还要把它传到规范码字、额外位，以及写入器实际采用的舍入方式。历史上的一条路线使用斐波那契数列：后一个数由前两个数相加得到，而树合并的父权重也是两个孩子权重之和。这样的增长估计可用于限制某些频率条件下的树深，再估计前缀成本。它有特定的参数范围；用于实际 C 之前，仍须建立对应频率、深度和机器运算之间的关系。树构造与码长修复 展开了所需的记账。

交付与调用边界

交付时，len 是内部待交付字节数 s->pending 与调用者可写字节数 strm->avail_out 的较小值。内部读取游标为 s->pending_out，调用者写入游标为 strm->next_out，total_out 统计此前累计交付的字节数。这里可直接跟随 flush_pending 的交付核心，deflate.c:978–983：

zmemcpy(strm->next_out, s->pending_out, len);
strm->next_out  += len;
s->pending_out  += len;
strm->total_out += len;
strm->avail_out -= len;
s->pending      -= len;

第一行从尚未交付的起点复制 len 个字节。第二、三行让调用者的写入位置和内部读取位置前进相同的量。第四行把这次交付加入累计输出；第五行扣除调用者空间；第六行扣除未交付字节。len 在前面的源码中取两边可用量的较小值，归零时另有游标复位。

对五字节例子，若调用者只能接收两字节，第一次复制 73 74，待交付从 5 变成 3，内部游标前进 2。下一次从该游标复制 82 40 00，而不是重新从分配起点复制。证明要同时保持这个字节等式、两边范围的合法性以及复制的分离条件。

这段复制移动的是已经编码好的一个前缀；它不应凭空产生字节，也不能丢掉尚未交付的后缀。输出空间有限时，一段交付可能跨越多次调用。因此，返回边界既需要字节记账，也需要保留编码器剩余的状态。

一个有用的关系，把累计交付给调用者的字节、当前待交付区域和缓冲位，连接到逻辑符号已经编码出的前缀。输出耗尽时，它解释已经交付了什么、还剩什么。恢复执行时，证明从这个实际返回状态继续。前一个块的字节尚未交付完毕时，不能直接给新块套上“初始待交付字节区为空”的前提。

最终，块的正确性还要与封装头尾、刷新操作、初始化和清理组合。公开的 deflate 契约 与 deflate_sequence 目标，都比上面的局部写入器结论更广。deflate 论证 连接这些层次；项目进度 记录接受范围与剩余工作。沿这条路线继续阅读时，每一步都有明确对象：保持记录，追加它们应有的比特，交付这些字节，再留下足够的状态继续同一个任务。