参考文档 / ZLIB × LEAN

本地证明登记检查

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

这里的“登记”把一个现有证明与固定目标对应起来，供审计检查类型和依赖；它没有让未证明的函数自动成为已证明。下文的数量属于记录中的批次，不代替当前进度。

此批次登记 59 个既有的精确目标证明：六个查询、九个校验和入口、29 个流或 gzip 入口、两个初始化定义域目标和 13 个抽象模型目标。不改变目标命题、规范或翻译。

CRC 生成器包装证明现在显式拆分零长度情况，再使用已有的 64 位定理。其类型不变。二十三个既有证明补充了缺失的 C 签名和范围文档字符串。

变异证据

列表	情形数	范围
`public-queries.tsv`	20	查询结果和边界行为。
`public-checksums.tsv`	9	Adler 更新／组合和 CRC 组合入口。
`public-streams.tsv`	94	流和 gzip 入口结果、守卫和状态变化。
`api-boundary.tsv`	18	既有抽象模型和查询边界检查。

48 个映射公开目标的原精确证明通过全新内核重放。全部 61 个所需变异都被这些原证明拒绝，且在对应函数证明模块中也出现失败。集成快照上的四个严格列表全部通过：141 个拒绝，没有等价情形、已知缺口或无效变异。补充情形测试其他分支。超时或内核资源错误不计为拒绝。

校验和变异在已记录定义域中具有具体见证：

入口	允许输入	变化的行为
`adler32`	NULL 缓冲区，长度为零。	包装将长度改为一，触发禁止的解引用。
`adler32_z`	一个零字节；更新前传入的校验值为 `(65520 << 16) + 1`。	等于 65521 的高位和未被约减。
`adler32_combine`	两个空输入校验和（均为一），第二段长度为零。	拼接校验和变为零。
`adler32_combine64`	同样的空输入情形。	拼接校验和变为零。
`crc32_combine_gen`	长度为零，CRC 表已初始化。	恒等运算符变成单字节运算符。
`crc32_combine_gen64`	长度为负一。	拒绝结果从零变成一。
`crc32_combine_op`	生成的零长度运算符，第一个 CRC 为零，第二个 CRC 为一。	省略 XOR 使结果从一变成零。
`crc32_combine`	第一个 CRC 为零，第二个 CRC 为一，长度为一。	交换参数改变精确多项式结果。
`crc32_combine64`	同样的数值输入。	交换委托参数改变精确结果。

CRC 运算符和组合目标覆盖任意校验值及指定的生成运算符；最后三个见证使用该数值定义域。将其解释为拼接仍需要真实的校验和。

三个必需的流映射避开了更早尝试中的资源失败：

入口	所需变异	被改变的允许行为
`inflateInit_`	省略委托，直接返回成功。	必须拒绝 NULL 版本。
`inflateMark`	对拒绝的流返回零。	NULL 流必须返回文档规定的负哨兵值。
`gzerror`	返回 NULL，而非消息指针。	允许的非内存错误视图保留非 NULL 消息。

默认窗口初始化变异仍为补充检查。其第一个失败发生在包装函数的源码方程证明中。仅凭该失败不足以满足精确公开证明验收。所需的省略变异另行拒绝了原来的精确公开证明。

查询边界资源限制及必需的替代映射见查询审阅。

范围

抽象模型证明建立这些模型的性质，不建立翻译后 C 实现的细化。初始化定义域目标建立可用调用定义域，不完成每个初始化入口契约。有限差分测试是翻译忠实性的证据，不是证明。

登记审计检查编译后的项、允许公理和精确目标类型。规范的锁再生成还包含之前累积的源码变化，包括经过独立审阅的 CRC 字节地址表示。十三个保留定理类型展开新的 Heap.byteBase 字段。比较导出内核语法显示每个类型恰好增加一个复制的元数据字段。仅移除这个新构造器参数，就能逐字节复现各个旧类型。其源堆与复制的 garbage 字段相同。既有绑定、假设和其他结果字段不变。这个只读比较不修改任何规范锁。

110 个变化的保留定义分为八个早期源码或命名空间变化、70 个堆构造器展开、21 个生成绑定名变化、九个堆构造器／递归器声明，以及 CRC 地址函数和其对齐谓词。只擦除匿名函数 lambda、全称量词 forall 和局部定义 let 的绑定变量名称后，21 个绑定名变化消失；其 de Bruijn 变量和其他语法相同。堆与 CRC 变化属于更早的字节地址修复，不属于本登记补丁。

基线还在早期模块移除之后退役 42 个过时的 Pilot 定义条目，以及两个被替代的生成地址辅助声明。编译器生成的辅助声明新增项由递归辅助声明审阅覆盖。锁变化需要审阅；再生成本身不批准它们。

集成根通过全新内核检查和声明审计。审计识别 77 个精确已登记目标、382 个列出定理和 20,014 个声明。本地审计器／测试框架测试（24 个）、图测试（18 个）、无 sorry 检查和禁用构造检查通过。修复后的树深度测试框架情形也通过其 C／Lean 正向基线并检测到变异。这些检查不报告集成提交上完整 Linux 或 Sanitizer 差分测试通过。

当前计数、剩余工作和最终验收状态只在进度中维护。本地登记不是最终 CI 验收报告。

受限范围的打开、关闭和位预置分支

此批次将十四个受限范围的执行／帧性质定理加入登记表，没有新增完整公开目标的证明。公开与支持目标数量不变；新分支不能让整个函数节点变绿。

源码	已检查定义域与结果	剩余公开工作
`gzlib.c.open`	NULL 路径／模式、负描述符，或初始分配失败；`gzopen`、`gzopen64` 和 `gzdopen` 的精确返回句柄、堆及文件系统作用。	模式解析、成功构造、后续失败，以及公开不变量建立。
`gzread.c.close`	NULL／错误模式拒绝；在已有 `GzGood` 下完整执行 `size = 0` 读取器关闭，包括所拥有字符串、句柄释放、描述符失败和无关分配帧性质。	已初始化读取器，以及从公开历史推导所有权／解码器不变量。
`deflate.c.prime`	被拒绝的流，或位数不在 0 到 16；拒绝发生于压紧之前，且不影响堆。	接受的位数、待发字节压紧、已发位和不变量保持。

正向根构建通过。严格定向变异列表 tests/proofmut/gzip-frontier.tsv 和 tests/proofmut/deflate-prime-entry.tsv 分别拒绝全部八个和两个直接源码变异，错误位于相应函数证明模块。这些检查覆盖所述分支，而非公开入口的每个分支。三个新证明模块及其依赖分别通过独立的全新内核重放。根声明审计通过，共 20,047 个声明和 396 个列出定理，181 个精确目标中仍有 77 个登记。这不声称完整根经过全新重放。机器报告将诊断输出分开。所有既有语义锁和命题锁记录逐字节不变。新增锁项为两个源码辅助声明、五个生成的匹配／拆分定义，以及十四个定理类型。生成定义是关闭结果匹配器和检查关闭证明时产生的私有拆分器，不改变已有文件系统或 monad 定义。查看器的 28 个测试也通过，包括就绪标签不能授予证明状态或创建阻塞项的检查。本记录不是最终 CI 验收。

契约、翻译和运行时不变。新增纯辅助定义给关闭后的堆和固定的外部关闭结果命名，不是对库内被调函数的假设。语义锁与定理类型锁新增项由声明审计生成。源码策略更新覆盖明确的阶段偏离说明、变异列表和所请求的进度查看器变化。已有锁定含义和定理类型必须不变。当前先决条件见进度。