匹配搜索的证明思路

压缩器可以少搜几个候选，也可以把决定推迟一步；但它不能用一条会还原成别的字节的引用替换输入。这一篇要解释的承诺是：策略每提交一个字面量或匹配，独立展开这些符号，恰好得到已提交的输入前缀。 最终的压缩位串还要经过树构造与块发射，本篇只追踪走到符号这一段。

先把承诺放回搜索例子：历史是 ABCQABCR，当前输入是 ABCQABCX。长度 3、距离 4 会恢复 ABC；长度 7、距离 8 会恢复 ABCQABC。它们覆盖的输入长度不同，但都可以是正确选择。如果把后一条距离误写成 4，复制会在第四字节产生 R 而非 Q。这个错误引用即使没有越界，也破坏了功能正确性。因此，证明不能只检查数组上下界，还必须说明每个被引用字节的身份。

把一次选择拆成可连接的保证

证明接收的是实际翻译后执行、明确的调用前提，以及该状态与逻辑输入的关系；要给出无故障的执行结果、正确的新状态和字节含义。一个自然数等式只能承担其中一部分。每层的前提必须由上一层实际建立，不能把尚未证明的被调函数契约当作假设。

这也解释了下面的顺序。窗口先保证来源字节还在，而且搬移后位置没有指错；候选链保证搜索追到的确是那些已插入位置；搜索保证被接受的长度有相等字节作见证；策略再保证提交的是正确起点的匹配。一次交接的局部定理，不会自动提供整个 deflate API 的保证。

移动表示中的字节

先看一种会让后续搜索失效的错误：搬动了位置计数器，却没有把对应字节搬到新下标。数字仍可能都在界内，搜索读到的内容却已经不是原来的历史。为排除这种错误，需要同时描述存储范围和内容。

先给存储界中的三个字节量命名：W 是配置的窗口尺度，字节数组容量为 2W；strstart 是当前输入起点的数组下标；lookahead 是从该下标开始已经装入的真实未处理字节数。例如 W=512、下标为 800、装入 100 字节时，真实数据末尾是 900，仍在 1024 字节的分配范围内。一般的窗口形状关系就是 strstart + lookahead ≤ 2W。它能解释补充输入为什么放得下，却没有说明复制了什么内容。

功能关系还必须把每个保留窗口位置连接到逻辑流位置。把数组下标零对应的逻辑流位置记为 L，单位是从整条输入起点计算的字节数；把数组字节下标记为 i。保留数组位置 i 的字节，应等于逻辑输入中 L+i 的字节。例如 L=512、i=188 时，该单元代表输入字节 700，而不是输入字节 188。

滑动 W 之后，新基准是 L+W，新数组位置 i 保存旧位置 i+W 的字节。两个表达式指向同一个逻辑位置：

(L + W) + i = L + (i + W)

窗口例子把它具体化了：滑动 512 后，当前位置 800 和候选 700 分别变成 288 和 188，字节身份与距离 100 一起保持。如果只证明计数器都减去 512，就会遗漏必需的内容相等关系。

分配区间论证是另一件事。滑动把 [W, strstart+lookahead) 复制到起点，目标长度为 strstart+lookahead-W。在把源码无符号减法解释成数学减法之前，必须先建立边界；memcpy 的源、目标也必须有效且不重叠。自然数定理 slide_copy在 W ≥ 512、窗口形状界与滑动条件下建立相应区间算术。它是数值引理，单独并不执行整个 fill_window。

读取操作随后要把调用者字节连接到实际窗口数组，并更新输入游标。read_buf_ok描述有明确范围的翻译后复制及其记账；其中的缓冲区与流前提需要由调用点建立。保护尾部的初始化写入必须留在分配内，同时不扩大逻辑输入。block_start 记录当前块的原始字节相对数组基准从哪里开始。滑动可能让基准越过这个块的起点，因此它是有符号量，也必须允许为负；要求它处处非负，会悄悄删掉真实执行路径。

有意义的链接与槽位复用

窗口中的字节正确，也不代表任意表项都能作为候选读取。如果前驱槽位已经被后来的位置复用，沿旧位置解释这个槽位，就可能走到另一代插入留下的链接。因此需要一条能区分“数组里有数值”和“这个数值真是当前链链接”的关系。

头表保存每个哈希桶最新的候选位置；前驱表 prev 保存某个已插入位置的下一个较早候选。它只有 W 个槽位，位置 p 与 p+W 会复用同一个槽位。源码分配后并不初始化每一个 prev 槽位，而是清空头表，再随着位置插入写入前驱槽位。若要求所有槽位都保存合法链接，描述的就是另一套初始化策略。真正有用的命题，应当针对搜索实际可达的槽位。

HashChains记录了这个想法：一个非零可达位置 p，在其槽位仍然属于它时，必须是有意义的已插入位置。对应三字节串的哈希等于选定桶号。因为 W 是二的幂，p & (W-1) 等于 p 对 W 取模：它选出的是前驱表槽位，不是待比较的字节位置。该槽位记录的前驱值必须是更早的位置，严格小于 p。参数 top 限制正在描述的插入代际；条件 top ≤ p+W 识别尚未被一个窗口之后的位置复用的链接槽位。

插入改变两个单元：前驱槽位接收旧桶头，桶头接收新位置。证明把新可达结点分成新位置本身和旧链已经可达的结点，还要说明新槽位写入不会破坏一个仍在保留范围内的前驱。chains_insert为数学表函数证明结构保持；INSERT_STRING_ok则在堆、参数和区间前提下给出实际翻译后的读取与存储。连接这两部分，结构命题才能进入程序证明。

滑动是另一次表示变换：每个保留位置减去 W，而减去 W 不改变它对 W 取模的槽位；窗口内容同时移动相同偏移。chains_slide把链关系传递到这些变换之后，slide_hash_ok描述表更新的实际执行。未使用的垃圾槽位也可能被变换；它们之所以无害，是因为论证从未把它们当作有意义的链链接。

跳过第三个字节的比较，也需要内容事实，不能只凭对冲突的直觉。hkey_third从键相等、前两个字节相等以及明示的哈希参数，推出第三个字节相等。这正是便宜探测通过后所需要的事实。

搜索含义与终止

有了正确的字节和可追踪的链，才轮到解释一次搜索的结果。例如长度 7 的承诺需要七个对应字节相等，而不是只有开头和末端相等。搜索不变量让当前候选始终位于已经说明的链上，让缓存的末端字节等于它们代表的窗口字节，并把最佳长度限制在允许范围内。循环体可以排除候选而不改变最佳结果；一旦改进结果，不变量就要增加一个见证：更早的位置、允许的距离，以及被声明区间内每个字节的相等关系。

展开后的比较会连接到一个更简单的数学扫描。firstMis_spec刻画第一个不相等位置，或最大边界 258。内层循环结果再把八次短路比较组成的条件连接到这次扫描。内存余量说明所有实际到达的读取都位于数组内；字节相等关系说明返回值确实是匹配。它们各自支撑不同的结论。

先看保证必须对应的实际写入：len 是刚比较的候选能匹配多少字节；best_len 是待超越的字节长度，初值来自调用者的基线 prev_length；cur_match 是这个候选的较早数组下标；状态字段 match_start 保存已经接受的来源下标；nice_match 是达到后就可以提前停止搜索的字节长度阈值。固定版本 longest_match，1543–1546 行的分支开头是：

if (len > best_len) {
    s->match_start = cur_match;
    best_len = len;
    if (len >= nice_match) break;

第一行要求严格改进；第二行才把候选位置发布到 match_start；第三行同步最佳长度；第四行允许达到目标长度时提前结束。执行这条写入时，证明必须已经取得该候选的字节相等见证。没有进入分支时，旧 match_start 不会因此变成当前位置的新见证。

同一函数的返回处，1557–1558 行另做一件事：

if ((uInt)best_len <= s->lookahead) return (uInt)best_len;
return s->lookahead;

第一行在最佳长度没有超出真实输入时原样返回；第二行在它超出时返回 lookahead。这给出真实输入长度上界，不能替代前面的内容证明。片段均为真实 C，省略的函数其余部分仍须由执行定理覆盖。

有明确范围的 longest_match_ok在 LMEnv 下给出执行结果。这个环境提供实际窗口和前驱数组、512 到 32768 之间的二次幂 W、掩码、覆盖比较范围的空间、合法的较早初始候选，以及链的语义事实。定理把搜索结束时内部的最佳长度记为 best，返回它与真实已装入输入数的较小者 min(best, lookahead)；只改变 match_start，并区分两种情况：

• 没有超过 prev_length：保留旧 match_start。
• 得到改进：match_start 见证字节相等、位置在前、距离合法且长度至多 258。

第一种情况并不是针对当前位置的新匹配见证。策略决定保留前一个匹配时，必须使用上一状态的对应关系。这个定理也不承诺在所有窗口位置中达到最大长度；搜索预算与停止搜索阈值正是为了免除这种要求。

终止可以使用当前链结点的位置：每个继续访问的前驱都严格更小，而表示中的位置能够放进运行时循环预算。lm_loop_ok把 cur_match.toNat 用作递减度量，并不依赖“无符号链计数器绝不会从零回绕”这一假设。这对从配置默认值扩展到更宽的 deflateTune 契约尤其重要。每条允许调参及调用历史究竟怎样建立所需链关系，仍然属于调用者组合义务。

从决策到符号序列

把一个逻辑输入字节位置记为 S，S+1 就是它的下一字节。最后一步要排除另一种错位：搜索为 S+1 找到了正确匹配，策略却把它当成从 S 开始的匹配提交。两处搜索都没有越界，也各自找到了相等字节，组合仍可能丢掉或重复一个输入字节。因此需要重新把搜索接回数据流。在普通策略边界，需要区分已经提交的逻辑前缀、可能暂缓的字节，以及尚未处理的输入。延迟匹配可以推进 strstart，同时把一个字节留作延期工作；它并没有因此把这个字节发射出去。若只把 strstart 当作已提交输出字节个数，关系就会写错。

对 XABCDEFGQ，发射字面量 X，让已提交展开增加一个字节；接受保存的七字节匹配，再让它增加 ABCDEFG。匹配长度可以大于距离：独立展开语义逐字节从不断增长的逻辑历史读取。相应窗口字节相等时，对复制长度作归纳，就能说明每个新字节都是所需的下一个输入字节。这里把匹配的逻辑输出起点记为 S，回退距离记为 d 字节，复制步骤从 j=0 开始计数。第 j 步写入 S+j，所以读取的逻辑源位置为 S+j-d。这里 j 从零编号，所以 j=3 表示第四次复制。距离为 2 时，这次读取 S+1，也就是 j=1 时已经生成的字节。

一般地，j < d 时来源属于较早历史；否则，它是第 j-d 步产生的字节。因为 d 为正，j-d < j，归纳时已经知道那个字节的含义。这就说明长度超过距离时，读取本次匹配刚生成的内容仍有依据。

策略在符号记录之前还必须建立精确的长度和距离界。字面量是一个字节；匹配长度为 3 到 258，所以保存的长度偏移为 0 到 255。其正距离不超过格式界 32768。选定搜索路径建立的是更强的实现界 W-262，单位为字节：配置尺度 W 减去为输入和比较预留的余量。这就是算法章节中的最大搜索距离 MAX_DIST。符号记录增加一条三字节记录，并更新对应频率。tallyCalls_preserves在足够符号空间下，给出实际合法符号记录调用的有范围组合。它自己的命题明确没有建立翻译后策略的输入历史，也没有建立发射块的含义。

这里就是接往Huffman 构造、块选择和输出保持的边界。完整论证必须让同一组选定符号穿过记录、树构造和发射，并保持其含义及未读存储。分别对互不相关的符号列表证明性质，再把它们当作压缩器的真实决策，是无法完成这个连接的。

初始化、策略循环、补充输入、刷新与公开历史之间的完整组合证明尚未完成；上面各局部结果没有覆盖这些连接。实现论证解释它们怎样组合，当前进度记录接受范围与剩余工作；公开 deflate 目标则保留自己的明示定义域。