生命周期的证明思路

应用需要的生命周期保证很直接：初始化流之后，每个允许的后续调用都使用有效存储；尝试失败或流结束时，不会丢失任何私有对象。难点落在具体情形上：早先的缓冲区请求失败后，后面的分配仍可能成功；复制的指针仍可能指向原状态；重置可以保留物理字节，却不允许把它们继续用作历史。

沿用分配示例：状态、窗口、哈希头和待发送字节存储分配成功，前驱分配失败。清理必须释放这四个成功对象，包括失败之后才分配的对象。再看复制示例：解码器 A 已交付 ABAB，新解码器必须能继续 A，同时不依赖 A 私有存储的生命周期。

下面从初始化、下一次调用和最终清理三个边界解释这些义务。完整生命周期组合仍未完成。进展记录保存当前接受证据。证明必须沿实际翻译调用跟踪同一批对象，从初始化推导有用事实，而不是先假设它们成立。

通过初始化建立可用的流

先回到第一次分配之前。应用提供不拥有活 zlib 状态的可写流、可读版本信息和恰当的分配器字段。它不必知道未来的私有窗口、表或指针。若已经要求这些作为前提，初始化就无法解释应用怎样获得可用流。

公开初始化命题区分调用者存储和它们建立的状态。InitDomain描述新身份、唯一对象表示、库全局对象、可读版本信息，以及分配器字段兼容的可写非活流。它不提供初始化后的库不变量，也不假设被调用函数契约。

InflateInitial 和 DeflateInitial在返回堆上描述成功结果。它们包含具体字段设置、流表示和精确分配账本。Deflate 结果指出五个新拥有的身份；inflate 从一个状态和 NULL 窗口开始。初始化证明必须从实际写入和分配结果导出这些事实。

默认压缩器成功时，“五个新身份”分别是状态、窗口、前驱、哈希头和待发送字节；它们拥有独立存储，字段指向相应对象。对失败示例，这个成功后置条件并不适用：失败分支另有状态码和清理结论。证明必须分类实际分配结果，不能悄悄假设走到成功分支。

这也是非空泛性义务。前提不可能成立的保持命题，不能为应用证明有用性质。初始化域目标量化覆盖可接受参数组合和允许的不失败分配，再要求成功的实际执行。固定 witnessHeap 还展示调用者域能够成立。一个见证补充全称覆盖，不代替其他窗口尺寸或压缩设置。

沿实际历史保证下一次调用安全

在 A 的 ABAB 检查点，下一次匹配需要的不只是“指针存在”。它需要容量正确的活窗口、有效历史字节数，以及能定位这些字节的索引。动态解码表指针也必须落在真正拥有它的状态内。把这些持续需要的事实放进表示不变量，每个函数就能沿用同一份状态描述。

例如，把窗口有效量误写成 100，而实际只保存了 5 个字节，指针即使没有越出分配，也可能读到不属于历史的内容。把动态表指针留在另一个解码器内，则可能在另一流结束后失效。第一种错误需要历史内容关系排除，第二种需要指针布局约束排除。先看描述存储表示的条件，再把它接到算法历史。

Zlib.Inflate.Spec.Good把活流与几类事实组合起来：

窗口条款还描述实际容量，表指针条款区分内嵌 codes 和共享静态表。Lean 数组值本身不强制 C 声明的长度，所以固定数组范围也必须明确。下一节继续区分后两种身份条件。

Zlib.Deflate.Spec.DGood类似地包含活压缩器、存储/尺寸约束、唯一性、新鲜性和树不变量。活状态检查中的非 NULL 分配器字段，不等于单独的 DefAlloc 断言；后者指定模型支持的默认分配/释放回调。

这些是具体表示谓词，不是完整的算法历史。形状事实本身不确定窗口的逻辑字节，也不建立表项实现了规范编码。精化所用关系必须把这些含义连接到同一个返回堆。

接着追问 A 怎样到达检查点：先成功初始化，再通过调用接受输入、交付 ABAB，期间也许合法更换了调用者缓冲区。仅从手工构造的“良好检查点”开始，不能证明应用的这段历史建立了它。归纳必须从实际初始化开始，覆盖每种允许转换，包括让流继续存活的错误返回。

StreamReachable记录实际成功初始化、实际返回操作、允许的调用者缓冲区更换和成功复制。执行等式记录调用发生过，不会免费提供其规格。StreamSequenceSafety 要求把不变量作为每个允许历史的结论，并要求下一个允许调用返回。它不只是当调用者假设不变量时，有条件地保持它。

区分新对象与既有对象

复制成功后，结束操作 A 必须保留副本的新状态和窗口。为表达这一点，证明模型给每项分配一个身份。身份区分两份尺寸相同的窗口，让释放其中一份不会顺带移除另一份。

堆在不同类型表中保存不同对象。字节块和状态记录不能暗中共用一个分配身份。Uniq 声明每个块编号至多在其中一张表中有对象。

C.Fresh把 nextBlk 作为尚未发放的首个分配身份，并声明从这里开始的每个身份都未使用。这是对象编号计数，不是内存地址或字节数。分配证明必须在计数器推进时保持此条件。Fresh 和 Uniq 的职责不同：前者保护未来分配，后者保护现有身份的解释。两者单独都不声明某两个流拥有缓冲区具有合适的分离关系；相应表示条款也须建立它。

新鲜性不会初始化对象。在失败压缩器尝试中，清理会读取缓冲区指针字段，因此必须证明每个字段在清理读取之前已经写入。在成功压缩中，前驱索引即使范围正确，也仍需证明链位置有意义。

新整数单元的任意内容仍在范围内。已分配容量不证明前驱或指针字段已经写入。安全参考解释模型固定的整数垃圾值和新指针为 NULL 的约定。运行时无法检测遗漏指针写入的地方，建立阶段需要先写后读证据。

解释每个活块和每次允许写入

回到第三次分配失败的情形。初始化之前，调用者可能已拥有与该流无关的其他活对象。清理之后，这些旧对象必须保留，本次获得的状态、窗口、哈希头和待发送字节必须消失。同时，流的错误消息或默认分配器字段可能改变，分配器也已观察到这些尝试。因此，“本次没有遗留分配”是有用结论；“整个堆不变”则过强。

Frame保护显式改变集合之外的既有分配。它也保持静态对象、分配结果函数和垃圾函数，同时允许新身份及分配尝试计数器推进。它不是整个堆相等。

写精确账本之前，固定一个分配身份 b。before、after 分别是调用前后的堆，live 记录该身份是否仍然分配。removed、created 是按身份判断的移除集合与新增集合。符号 ∧、∨、¬、↔ 分别表示“并且”“或者”“不”“当且仅当”。独立的 LiveChange 定义写成：

after.live b ↔ (before.live b ∧ ¬ removed b) ∨ created b

对某个分配身份 b 来读：它在返回后存活，当且仅当它原本存活且未被移除，或者属于本次新增的活集合。失败尝试返回时，新增活集合为空，先前的活块也没有被移除。中途成功分配的对象，必须由返回之前的实际释放解释。复制成功时，则加入新的目标块，同时保留 A 的块。

成功初始化时，created 指出新拥有块；初始化失败时，没有新的活块遗留，也不移除旧活块。结束操作的移除集合恰好是原流拥有集合。失败的五请求轨迹必须解释早先缓冲区请求失败之后发生的成功分配。

相较之下，inflate 可以先向允许的四个输出字节写入 ABAB，再因历史窗口分配失败返回。对象仍然存活，但这四个字节已经改变。仅有所有权账本，不能说明第五个字节是否被误写。

调用者输出需要比整个对象的框架条件更细的范围。BufferFrame保持字节数组尺寸，以及授权区域并集之外的字节。它允许已交付前缀或登记头部目标变化，但不授予任意修改同一分配其余部分的权利。

证明复用、独立副本与释放

有用的重置定理必须允许复用内存，又排除旧历史匹配。在 ABAB 例子中，物理字节未变与逻辑历史为空并不矛盾：有效历史计数变成了零。反过来，仅仅保留活窗口，也不能说明哪些历史被授权使用。

重置中，分配身份不变和逻辑历史改变必须同时成立。inflateResetPre 和 DeflateResetContract说明哪些计数器、指针和历史字段变化。不兼容的解码器窗口可以从拥有集合消失；普通压缩器重置保留分配并清空字典哈希。要求 DGood 的条件性重置定理，不能为新分配建立 DGood：初始化必须先构造所需状态和树事实。

对复制，可以比较两种错误。只复制字节而不修复内部表指针，会破坏私有所有权。分配独立缓冲区却遗漏持有比特或未完成匹配，会破坏后续执行。后置条件需要在同一个返回堆上，同时表达独立性和相同的已保存进度。

relocateCode、copiedDeflate 和复制目标描述相同进度与独立存储。静态编码指针可以共享；指向复制内嵌数组的引用改到新身份。Pending 游标和树描述符需要相应重定位。源流/状态保持不变，失败不留下新拥有的目标块。单独正确的字节复制会漏掉这些指针和所有权义务。

下面的结束操作节选用 TRY_FREE(stream, pointer) 释放非 NULL 的内部缓冲区，并跳过 NULL 指针；ZFREE 释放状态记录本身。status 保存释放前的压缩阶段，BUSY_STATE 表示普通压缩尚在进行。最后据此选择返回码，不需要让已释放状态继续存活。

结束操作封闭同一份账本。实际压缩器结束操作尾部清楚展示执行顺序：

TRY_FREE(strm, strm->state->pending_buf);
TRY_FREE(strm, strm->state->head);
TRY_FREE(strm, strm->state->prev);
TRY_FREE(strm, strm->state->window);

ZFREE(strm, strm->state);
strm->state = Z_NULL;

return status == BUSY_STATE ? Z_DATA_ERROR : Z_OK;

以上是逐字选取的源码行，不是教学实现。分配失败示例中，TRY_FREE 跳过 NULL 前驱，同时释放后来成功的对象。对有效的繁忙压缩器，释放仍先于 Z_DATA_ERROR。证明结束操作，意味着从这次执行推导精确移除集合、调用者对象保持和返回码，不能把非 Z_OK 等同于所有权未变。

固定快照的账本定义明确区分 Frame 和 LiveChange 义务。这些定义分别规定不相关对象的保持，以及新增、移除对象的精确集合。

诊断失败论证，保持调用域

如果论证卡住，先辨认失败的主张：是证明方法未能得到真的界限，表示允许了不可能的状态，翻译不同于 C，还是允许的真实 C 执行存在缺陷？这些诊断需要不同处理。过宽不变量构造出的不安全状态，本身不能证明应用可达失败。

方法记录描述了较早不变量允许 gzip EXTRA 阶段配合 NULL 头部的情况。该条件性执行暴露缺少的状态关系。它不建立允许的公开历史能到达此状态，也不支持排除合法调用者输入。

契约审查还记录了旧表查询允许 2^63 个槽位，而不是实际内嵌范围。对该表示问题的反例要求经过审查的命题修正，不能伪装为证明捷径。改变任何前提之前，先区分证明技术失败、错误规格、翻译不符和真实 C 缺陷。

历史、指针初始化和功能含义的完整组合尚未完成，需要从真实初始化证明每种允许转换都保留相应内容与存储关系。高级操作保留各入口效果和调用序列安全义务；普通格式阶段不自动精化字典替换、预置位和恢复的每种组合。各组件的前提与结果需要沿这些高级操作逐一传递。完整方法、流组合和当前进展保留精确义务、范围和具名提交的接受证据。