解码器的证明思路

解码器承诺按顺序恢复压缩输入所描述的字节。提前读取、使用查表、把几次复制放进一轮循环，或暂停等待新缓冲区，都必须保持这个承诺。同时，它要始终访问有效内存，并通过有定义的错误返回处理检测到的坏数据。

起点包括未消费压缩输入、保存的工作和历史字节，以及调用者提供的缓冲区。结果是有依据的输出前缀和精确的继续状态，或规定的完成、错误结果。“有依据”指独立格式规则能解释这些输出字节，不表示任何已缓冲前缀都是完整合法流。分段输入、小输出缓冲区、畸形数据和范围内的失败，都留在所声明的定义域中。

先在例子上检查承诺

前三章跟踪了源位、已安装的表和输出复制。继续看这几步计算：

例子帮助定位义务，不能证明所有输入。形式论证需要在每个允许步骤之后仍能表达这些事实的关系。始终保持的关系称为不变量。要证明实际 C 翻译满足它，先由真实初始化建立，再逐个说明实际分支如何保持。只有数组界不能确定符号，抽象上正确的符号也不能为无效读取提供依据。

未消费输入

对前两行，要比较步骤前后全部未读位。整数 hold 保存接下来要读的位，计数 bits 说明其中有多少有效位；调用者的未读字节排在它们后面。把合起来的位序列叫作 remainingBits。下面的教学等式中，low_bits 按读取顺序列出位缓冲的有效位置，byte_bits(unread_input_bytes) 以同样顺序展开未读字节，++ 拼接列表。这是解释性记号，不是照抄 Lean 定义：

remainingBits = low_bits(hold, bits) ++ byte_bits(unread_input_bytes)

取入一个字节只改变这条序列存放的位置，不改变值和顺序。丢弃已解码字段则恰好移除它的前缀。inflate 实际使用的消费操作来自固定版本 inflate.c 第 387–391 行：

#define DROPBITS(n) \
    do { \
        hold >>= (n); \
        bits -= (unsigned)(n); \
    } while (0)

对于 A，调用处必须提供 n=1：1110 右移得到 111，位数从四减到三。若提供二，整数运算可能仍不越界，却会删除 D 的第一位。所以证明既要建立移位有定义，也要建立移除量正确。源码中的 BitInv 和 stream 把局部量连接到实际可读输入范围与归一化的 hold 值。

PULLBYTE_succ 在该不变量和明确移位界下描述一次真实翻译后的取入。NEEDBITS_run 同时包括成功与输入耗尽退出，在统计取入字节的同时保持未消费序列。这些局部命题本身不建立主解码器的所有入口条件。

解码符号依赖支撑它的前缀，不必解释已经缓冲的每个推测性位。对 AD，尽管根查表查看两位，A 只消费第一位。相同区别必须经过快速路径字节回退，并在换用新输入视图恢复执行后继续成立。

实际表内容

对子表那一行，仅有足够单元的表还不够，它必须真的返回 D。构造器的输出必须正是解码器随后读取的表。构造章节 解释了生产过程：count 统计各码长数量，offs 定位临时存储位置，work 按编码顺序列出符号。先跟踪这些真实更新、反转编码、重复存储和子表链接，再建立已写单元对给定码长的含义。

声明 inflate_table_content 保留实际执行、返回分类和表内容。目标定义 把这层连接具体化：返回堆含有该数组，内部环境是执行结果，并与输入码长、类型、位置和根宽度相联系。这里“几何”指表区域、索引界和链接。不能由调用者直接提供这些条件，代替运行构造器。

这仍然不同于完整的解码器接口。inflate_table_complete_decoder_safe 明确要求完整字母表，即分配的编码没有在二叉编码树中留下未用分支。不能因为构造器能够处理空表或被接受的不完整单符号字母表，就说这个命题也覆盖它们。inflate_table_codes_decoder_safe 在其构造器前提下处理码长表接口。必须分别阅读每个命题的定义域。

表的存储边界与符号含义

LenTableSafe 和 DistTableSafe 描述有界的根区域、有界的单级链接和合适的叶项。它们的码长与额外位界为快速解码器的补充和移位提供依据。默认的 1444 项预留由字面量／长度表的 852 项和距离表的 592 项相加得到。仅仅分配这些单元，并不能建立它们的内容或链接边界。

在教学表中，根槽 11 必须指向两个可读单元，这是几何条件；子表 1 必须保存 D 且消费一位，这是与独立编码一致。两者都需要。交换 C、D 的变异可以保留每个索引界，却改变解码输出。生产者到消费者的连接必须在同一堆和返回宽度下，保留每个表项的精确操作标记 op、消费位数 bits，以及返回值或链接偏移 val，包括无效与结束标记。

调用者先建立前提，再使用关于翻译后构造器的定理。不能假设未经证明的被调函数规格，也不能因为某个方便的中间定理定义域较窄，就悄悄排除合法输入。

输出与逻辑历史

对复制和暂停两行，要比较字节，不能只比较指针位置。字面量把输出扩展一个字节。匹配按独立重复规则执行：在当前末尾之前指定距离处取一个字节，追加后再重复。可用的过去是预设字典接上已经产生的输出，称为逻辑历史。它包括本匹配刚写出的字节，正如 AB 例子所需。物理来源可以从环尾切到环头，再切到当前输出，正如前面六字节匹配的例子。

所以证明同时携带形状与内容。窗口索引、存活存储和已初始化范围论证访问合法；后缀关系说明窗口按精确顺序保留逻辑历史最近的那一段，并确定每个物理单元保存哪个历史字节。字典提供历史，但不计作新输出。更换输出缓冲区必须保持逻辑值，不能假装旧的借用内存永远可用。

copyMatch_run 在明确的上下文、距离、长度和空间前提下，记录实际快速复制的成功或距离过远行为。它是内部执行结果，不是整个公开解码器，也不证明初始化与每种历史都会建立这些前提。

快路与慢路组合

安全还包括保持不相关内存，称为框架条件（frame）。源码中的 inflate_fast_safe 描述辅助函数的安全、终止、框架条件、归一化和写回目标。actual_body_refines_token 把一次实际快速循环体联系到独立解码指令、块结束或被拒绝的解码指令。单次循环体精化与整个辅助函数安全命题，提供的是不同结论。

只有先建立前提才能采用优化。主解码器必须在真实快速条件处建立足够完成一条指令的空间：六字节输入覆盖最坏补充序列，258 字节输出容纳最长匹配。此外，为了精确退回整字节，还要建立少于八个已保存位，以及表性质和有效历史。慢速分派必须为小缓冲区、未完成字段和返回的匹配保持相容关系。LOAD、RESTORE 连接局部寄存器与边界状态，不表示两种表示在整个函数体中始终相等。有些模式变化既不消费输入也不写输出。这种无声转移需要递减的秩，即一个度量，说明解码器不能永远只切换模式而不前进或返回。

内存、终止与公开范围

每次访问还需要存活性、读写权限、边界以及正确对象。写入必须按框架条件保持不相关内存。清理对成功、失败和结束操作中的分配进行记账。C 与运行时之间的对应仍有指针、对齐和未初始化内存方面的限制，见 安全要求 和 信任基础。

可执行模型为循环设置有限的迭代预算，称为迭代额度（fuel）。终止性必须排除实际预算耗尽。有限复制次数、有界表链接、进展度量和无声转移秩，需要组合进具体预算。定理的内部前提必须来自实际初始化和允许的历史操作，包括被拒绝的调用。

完整解码器组合还未完成，需要把上述输入、表内容、历史复制和退出关系在同一次执行中接起来。进度 记录已接受范围和剩余工作；inflate 描述需要建立的公开行为。接下来进入 流状态，继续跟踪跨调用边界的同一论证。另外也可对照 压缩块输出，沿反方向看符号怎样成为比特、待发送字节和已交付输出。