跨调用的证明思路

应用要得到 ABABABAB，但输出缓冲区只有五字节。在真实 C 例子中，它提供压缩字节 73 74 82 40 00，调用 inflate，处理收到的 ABABA，然后重复使用缓冲区，拿到 BAB。第一次返回 Z_OK，第二次返回 Z_STREAM_END。

这次运行回答了“这些字节上发生了什么”。证明还要回答：“为什么对所有允许的调用历史，都能安全地继续，并恢复正确的字节？”它必须把实际写入连接到压缩输入，说明更换缓冲区后未完成的工作仍然存在，并涵盖失败和资源释放。ABABA 与 BAB 是需要解释的观察结果，不能当作解码正确的前提。

两次调用的证明义务

论证对象是逐语句翻译的 C：真实堆、保存字段和返回指针。独立格式关系说明压缩流应当表示哪些原文字节。下面解释如何连接这两者。文中局部引理分别处理读位、表和复制；完整解码器还需要证明它们的前提都由实际历史建立，并连接到同一次执行。进度页记录接受依据。

继续执行的关系

要继续这个例子，下一次调用需要的不只是“之前输出过 ABABA”。在调用边界保留四份互相连接的记录：

表示不变量说明保存字段、分配和字节内容彼此一致。证明模型以 Good 表示一项共用状态条件。证明必须让实际初始化建立这类条件，再让真实调用保持它，不能直接假定被调函数满足所期望的契约。

对于当前匹配，把以字节计量的回退距离记作 d，此处为 2。把下一次写入之前、按时间排列的历史字节列表记作 H。|H| 是它的字节数，方括号表示从零开始取索引。若 H = ABABA，来源索引就是 5 - 2 = 3，对应字节 B。因此，一步展开追加 H[|H|-d]。这个追加同时改变下一步使用的历史。因此，不变量必须把保存的剩余长度连接到已经展开的前缀，不能只说 length ≤ 258、距离没有超界。

第一次返回时，逻辑前缀是 ABABA。本例重复使用同一块输出内存；合法的后续调用也可以改用另一块分配。更换后，旧输出内存不一定仍可访问。必须保留的是所需后缀的有效表示。这里用 ++ 表示把两个字节列表接起来，再只取窗口容量内最新的后缀。例如，上限为八字节时，0123ABCD ++ ABCD 留下 ABCDABCD。内容关系可以写成：

新历史 = 取窗口大小的后缀(旧历史 ++ 本轮新产生的字节)

物理环形数组不一定按递增索引保存这个顺序，wnext 是下次写入的物理索引，whave 是有效历史字节数，二者决定时间顺序以及何处需要从数组末端绕回索引零。重新绑定缓冲区后，第一个 B 由这份历史列表支持；新输出足够多以后，读取来源又可以转到当前调用者缓冲区。每次读取的证明都要解释实际属于哪一种情况。

实际声明 updatewindow_ring_public把返回环形内容连接到“旧时间顺序历史追加新源字节，再丢弃超出窗口的前缀”。它要求已有可写窗口、Good、精确的分配尺寸、可读源范围，以及明确的范围分离。这是一块具体的内容保持论证。要让它服务于整个解码器，仍需建立旧窗口已经表示逻辑历史，并从所有需要的返回路径调用它。

输出前缀的输入依据

输入记账需要同样仔细。一次查表可能查看超过所选符号实际消耗的位。解码表示例中，根索引查看两位，A 却只消耗一位，第二位已经属于 D。若要求 A 的结果由全部预读位的一次完整解释支持，就给这个结果附加了错误长度的依据。

应当为每个输出前缀关联一段支撑位前缀：在独立格式关系下，足以确定这些输出字节的源位。超过它的位仍是预读。后续畸形符号或尾部，不应推翻此前已经有依据的输出前缀。快速路径还可能把预读的完整字节退回调用者输入；这一调整前后必须传递同一个源位置关系。

模型中的 output_evidence_determined从因果位前缀依据导出字节前缀的确定性。它研究的是无堆 API 关系，不是 C 翻译。这一区别指出了实质工作：证明真实的表项、额外位和复制执行建立了模型所需的依据。只有这座桥建立以后，模型定理才能用于实现。

源文件还包含一项防止关系过于宽松的具体结果：inflate_no_input_mem_cannot_guess排除了新裸模式流在没有消耗输入时凭空产生字节 a，即使返回结果是内存错误。允许错误并不许可任意输出。同样的原则也约束普通成功前缀和依赖字典的输出。

下一次调用的可达状态

单次保持性声明以输入状态满足条件为前提。要得到整个生命周期的结论，这个条件必须来自实际初始化和之前的合法调用。StreamReachable由实际成功初始化、合法的调用者重新绑定、真实操作和成功 copy 构成，没有把先前被调函数的期望契约直接插成假设。

调用者步骤使用 Rebuffer：应用可以替换输入输出绑定、改变非自有存储，同时保持流的内部存储和其他控制字段。下一次操作还要分别满足可读可写范围、分离、借用头部仍然存活，以及选定的平台前提。LP64 范围中的字节对象尺寸上界是显式环境条件，不限制一个长流累计可以处理多少字节。

对于数据含义，DataStep记录真实执行及其返回输出切片中的字节。这里 input 是该次提供的可读字节列表，used 是本轮消费的字节数；input.take used 表示取列表开头的 used 个字节。调用历史追加这段实际消费的前缀和本轮新输出。这是观察记录，不是假定输出正确；序列目标需要进一步证明累计观察满足独立解码关系。

字典是另一类历史贡献。在 zlib 握手解决前，即使知道所需校验和标识符，字典字节仍可能未知。实际 inflateSetDictionary 接受字典后，论证才把复制到窗口的后缀连接到格式关系使用的字典。裸模式解码开始后替换字典，可能引入多份历史上下文；DataLog.singleDictionary 明确记录普通单字典声明何时不再描述当前数据阶段。抹掉这个区别，就会声称比目标本身更强的定理。

返回时已经发生的变化

沿同一次真实执行检查全部出口。模式中的局部 break 返回分派。翻译另用两个名字区分更大的出口：Ex.leave 携带当时的局部寄存器进入共用返回路径，Ex.ret 则直接从函数返回。直接返回可能跳过共用路径中的记账。因此，字典请求、畸形数据模式和窗口分配失败，不能都简化成同一个抽象“停止”。

StreamAccounting把 used 和产生长度连接到新指针及可用数量，并保持流身份与固定的分配器、控制字段。公开 inflate 目标还区分普通总量更新与较晚的 Z_MEM_ERROR：调用可以在 updatewindow 失败前写出输出、发布前移的游标，而后续总量和校验和更新尚未执行。对这条出口，“总量未变化”可以与“实际输出非空”同时成立，“输出未变化”则不成立。

下面的条件决定是否需要让近期输出活过本次调用。out 保存一份输出空间基线，单位为字节；strm->avail_out 是尚未使用的空间，二者之差就是基线之后写出的字节数。state->wsize 在历史窗口尚未启用时为零。按顺序编号的模式常量 CHECK、BAD、MEM 分别表示尾部处理、畸形数据和内存失败；Z_FINISH 则是调用者提出的完成请求。

固定版本的共用返回路径直接展示了证明必须保留的顺序：

    RESTORE();
    if (state->wsize || (out != strm->avail_out && state->mode < BAD &&
            (state->mode < CHECK || flush != Z_FINISH)))
        if (updatewindow(strm, strm->next_out, out - strm->avail_out)) {
            state->mode = MEM;
            return Z_MEM_ERROR;
        }

RESTORE 先发布新指针，随后才可能分配失败。增加 total_in、total_out 和 state->total 的语句位于这段代码之后。本例的两次成功调用会执行到它们；这条较晚的内存错误出口则会跳过它们。因此，证明必须把返回输出切片与总计数分开追踪。完整调用组合还未完成，需要从每条真实出口推导这组不同的输出和总计数效果。

单次调用的终止性

终止既要约束逐字节循环，也要约束模式转换。安装表、从已解出的长度进入距离阶段，都可能在不消耗新字节、不产生输出的情况下推进状态。因此“每次迭代输入都减少”不是合适的论证。一条路线是把有限输入、输出和剩余复制量，与内部模式转换的有界顺序组合起来。

秩是证明为剩余工作选取的非负整数，不是运行时间。它每次严格减小，就不能无限下降。翻译还给每个循环一个有限的执行额度，称为迭代额度（fuel）；因此除了证明下降，还要说明初始秩没有超过这份额度。

已有的 xwhileBrk_rank精确给出局部步骤到循环的连接：继续迭代时保持谓词，并严格减小由寄存器和堆读出的秩；出口建立后置条件；初始秩加二必须小于循环迭代额度。该定理提供归纳原理。应用到完整解码器时，仍须给出具体谓词、证明每个实际模式情形，并建立初始迭代额度界。仅引用秩引理不能自动完成这些工作。

封装与完成关系

封装章补齐了同一任务的最后一段。头部建立所选格式和窗口条件；字典进入历史而非输出；载荷更新恰好覆盖产生的字节；尾部按规定字节序读取。登记的 gzip 元数据又增加了独立的调用者可写区域及生命周期要求。

实际 inflate_CHECK_run分别处理尾部输入不足、已启用检查不匹配，以及继续进入 LENGTH。其前提包括 BitInv，它联系暂存位、有效位数和未读输入；还包括正确 CRC 静态表，以及 PutAt，它在模型的字节数组中定位当前写入游标之前的输出切片。Adler 值条款显式保留了“单字节／非规范初始累加值”的条件，没有假设任意累加器都已规范化。完整调用者论证要从可达历史中导出适用的累加值性质。

CHECK 更新输出记账以后，还会改变局部输出基线。后面的返回记账必须使用这个新基线，才不会重复统计同一批字节。gzip 长度比较使用已产生大小的低 32 位。关闭验证则遵循实际选定的配置，不能通过忘掉配置，把它证明成与启用验证等价。

完成保证与窗口范围

两次调用的例子使用完整窗口大小的裸模式解码器。其他允许配置需要分别表述结论。inflate 序列目标区分：

FullWindow 是一项配置条件，表示使用完整的 32768 字节历史窗口，也包括规定的由头部或默认值选出完整窗口的情形。下表区分哪些结论需要这么多历史，不把所有可接受配置都当成完整窗口。

“单字典”描述这一数据阶段的含义可以用一份字典说明，不代表所有裸模式字典替换序列都符合该条款。

FullWindow 选择 32 KiB 窗口，或那些由头部／默认选择得到完整窗口的特定零位数请求。有效窗口位数为零时，zlib 头部必须声明 15；gzip 使用默认值 15；自动识别则允许相应的 zlib 或 gzip 情形。较小的保留窗口可能拒绝格式有效的流，且结果与调用者如何拆分输出有关：当前调用的输出与保留历史能提供不同数量的可访问匹配历史。因此，格式有效本身不能证明所有已接受窗口配置下都必然接受。

仅说明“完成时输出正确”，还没有说明下一次调用能否完成。独立的 InflateCompletes 对这个问题另设前提：

这些前提成立时，目标要求下一次真实调用达到 Z_STREAM_END，并写出剩余解码后缀。例如，若五字节示例第一次已交付 ABABA，余下结果就是 BAB；仅给三个输出位置还不够，还要给正确的剩余压缩输入、有效状态和已解决的字典上下文。

完整组合仍须把各组件接到同一返回堆上，证明每个实际出口都满足目标。组件指南列出详细义务，进度页记录哪些工作已经完成、哪些仍未完成。