参考文档 / ZLIB × LEAN

公开契约审阅记录

此页源文件快照 · b36c493fd192988f · 对应提交的原文 ↗

本记录解释 95 个默认构建入口契约和八个族级目标背后的源码审阅与反例。它不是对语义基线的独立批准。下文关于已检查证明的陈述描述记录下来的审阅证据；当前验收仍需要明确命名的提交上的登记项与 CI。当前剩余工作只列在进度中。

三层规范

层	含义
`ZlibF/Spec/Format`	合法的 DEFLATE、zlib 和 gzip 字节、解码与校验和。
`ZlibF/Spec/Api`	无堆 API 模型。有些旧模型只覆盖文档规定的调用模式。
`ZlibF/Spec/Public`	固定实现目标：实际执行、调用者定义域、结果、帧性质和所有权。

“无堆模型”只描述抽象状态转换，不执行具体指针访问；“公开实现目标”则必须描述实际翻译在某个内存状态上的执行。Calls.lean 固定实际翻译后的入口。公开目标不能用空执行关系替代它，也不能假设库内被调函数满足规范。格式或抽象模型的证明不能单独验证公开函数。

flowchart LR
    F["独立字节格式"] --> A["API 行为"]
    A --> P["公开实现目标"]
    C["实际翻译后的调用"] --> P
    P --> T["精确匹配的已登记定理"]

命题审阅的范围

分组	目标模块	审阅的义务
校验和与查询	`Checksums`、`Queries`	空缓冲区约定、全部标量值、有符号组合长度、不可变堆和常量表。
Init 与 Reset	`Initialisation`、`Lifecycle`、`Domains`	版本／错误顺序、每个有符号参数、分配失败、精确清理，以及已建立的非空定义域。
流操作	`StreamQueries`、`Streams`、`Copy`	干净拒绝、计数器、部分输出、字典窗口、位插入、界限和复制后的独立所有权。
缓冲区辅助接口	`Utilities`	兼容包装、标量单元、尾随输入、内存失败时的部分输出、精确长度和临时资源清理。
回调 inflate	`Back`	实际的有限且会返回的回调、自适应输入、与窗口共享分配的描述符、原始输出及调用者拥有的窗口。
Gz 句柄	`GzState`、`GzOpen`、`GzControl`、`GzRead`、`GzWrite`、`GzClose`	延迟分配、不活跃的悬空字段、恢复、位置、完整元素计数、借用消息、已接受字节、Seek 补零及描述符清理。
生命周期	`Sequences`、`GzTrace`	每个允许的后续调用都会返回、由 Init 建立的不变量、精确分配变化、清理、普通格式阶段和完整写入器输出。

除明确命名的已检查结果外，完整实现证明未完成，仍需把目标中的作用与实际翻译执行连接起来。API 手册解释操作。历史执行笔记和证明状态文字不能覆盖登记项或所需 CI。

源码审阅修正

审阅在目标命题中明确了以下区别：

Uncompress2 允许在较晚的内存失败前产生输出。它与具体辅助接口目标共享数据关系。缓冲区耗尽不表示未使用的尾随字节会扩展有效流。Init 失败时长度单元可以保持不变；之后的失败会保存计数。
流查询包括空指针和干净的无效状态拒绝。位预置遵循源码中零、负值和溢出的检查顺序。可选输出单元各自独立可选。
固定版本的 gz_look 首先检查四个头字节。错误的方法、标志或更短文件可以选择透明输入。后续成员直接进入 inflate。默认缓冲区为 8192 字节；gzbuffer 将最小值限制为八，并拒绝翻倍溢出。格式化拒绝返回流错误，与空结果或过大结果分开。
头文件不保证 gzsetparams 会拒绝每个无效标量。对有效参数，成功既更新内层压缩器，也更新外层字段。
回调描述符可以与窗口共享一次分配。它们保留窗口切片；其观察不变量只忽略该切片。整个函数目标对这些不变量作全称量化，因此选择宽松不变量不能完成该目标。

上述修正来自所选 C 的源码；完整实现证明未完成，仍需逐条建立这些结果。将它们写成可编译命题，不代表这些命题已完备。

旧命题的反例

预读可能已经读入后续错误位，但此前输出仍有合法依据。因此，表中的“支持位前缀”是足以解释已产生输出的那部分输入位，不是要求所有缓存位都合法。独立后续审阅以不可变提交 a655458 作为旧规范，没有改变公开调用者定义域、翻译后的函数或运行时操作。

输入或状态	旧命题的错误	修正及已记录证据
原始字节 `73 04 42 00`，一个输出字节	实际首次调用在读入一个不可能距离后返回 `Z_OK` 和 `A`。要求整个预读内容有效会拒绝这个结果。	要求存在可有效完成的支持位前缀，并要求每个兼容完成都扩展已产生输出。内核证明拒绝旧条款，并检查一个模型见证。成对的 C／翻译回归包含随后出现的 `Z_DATA_ERROR`。
有效 gz 读取器，已分配消息，空只读表	`dropWindow` 通过保存默认值改变只读表的大小。实际 `freeB` 保持该表不变。	只移除字节块。通用定理覆盖每个 `WindowAllocation`；完整的 `gzclearerr` 公开证明检查修正后的目标。
具有 `2^63` 个解码表槽的模型状态	查询视图省略固定 C 数组布局，允许指针相减超过 `ptrdiff_t` 范围。	要求实际的 1444 项 `codes[ENOUGH]` 布局。内核反例保留旧问题；精确的公开 `inflateCodesUsed` 证明检查修正。

因果输出修正也适用于共享的 Uncompress2。仅有全称确定性在错误预读后可能空洞成立。两个修正条款都不假设剩余预读有效。未改变的解码器模型问题仍需要细化到实际解码执行。单独的旧固定检测延迟条款已有反例；本记录不把那个模型当成经过批准的实现细化。

清理辅助函数由 inflateReset、inflateReset2、gzrewind 和 gzclearerr 共享。它们分配的块可写，需要相同的字节块移除。通用作用证明不能证明每个调用者。这是规范表示错误，不是上游缺陷。

查询布局来自 inflate.h 和 inftrees.h 中的 852+592 界限。已有的 Good 不变量蕴含它。Init 和实际状态转换必须建立、保持这个不变量；序列目标要求将此作为结论。没有增加公开标量限制。

deflate 目标还在其存活状态前提下固定流错误分类的两个方向：无效 Flush、无效空缓冲区，或开始结束操作后调用非 Finish 操作。仅列出允许错误码会容许无理由拒绝。会写入消息的拒绝与更早的无效 Flush 返回不同；只有后者承诺堆不变。

记录中的模型变异会删除因果证据、恢复整个预读有效性的要求，或删除输入前缀要求。公开 gzclearerr 变异会省略错误清除或保留 EOF 标志。拒绝它们检查证明敏感性。差分比较仍是有限执行证据。

高级操作的边界

序列安全和清理包括所有允许操作，包括 Reset、Copy 和恢复。普通数据阶段把实际已接受、已产生的字节与独立格式关联，并包含空间充足时的完成性质。轨迹构造器计算适用性标记；证明不能随意选择或清除它们。

一个初始字典描述普通 RFC 流。在流中途替换 raw 解码器字典会改变这个上下文。标记记录这种改变；该入口的窗口作用与序列安全仍必须满足。位预置、头捕获和恢复也保留具体操作目标。目标集合尚不等于所有高级组合的完整操作细化。这个边界不会移除其安全义务。

Gz 写入器历史记录实际调用、已接受输入及已消费的 Seek 零字节。最终 Close 必须产生能解码为这些数据的 gzip 成员；透明模式下则产生相同字节。已有文件前缀和尾部都要计入。仅描述位置的契约不够。

审阅与批准

命题修正提议需要不可变的旧、新命题，C／手册对比，以及旧问题失败原因的说明。应区分证明技术问题、错误规范、翻译不匹配和上游缺陷。内部不变量的反例不能成为缩小公开前提的理由。Init 和早先调用必须建立任何替代不变量。被调函数契约仍必须是已证明结果。

确认的规范错误应单独提交审阅，附带回归证据和重新生成的锁。就绪检查验证存在性、编译、全新重放和锁一致；它不能判断语义完备性。提交成为权威基线之前，独立审阅必须批准公开定义域、表示限制和运行时。