内核检查与可信边界
9e785de585c0e313 · 对应提交的原文 ↗内核检查证明是否符合其 Lean 命题。将结果用于选定 C 源码，还依赖以下事项。它们经过审阅、锁定和测试，不能仅靠编译证明消除。结论、验收规则和当前状态分别见安全性、验证策略和进度。
1. 内核与允许的公理
信任 Lean 内核，以及 propext、Classical.choice、Quot.sound。声明审计只允许这三个公理。新鲜内核重放检查编译后的证明闭包；执行测试不能替代它。
2. 运行时与对象结构
这里先固定“运行”的含义，再谈证明。可以把堆理解为一本对象账簿：每个分配对象有自己的编号和内容，指针用“对象编号加对象内偏移”定位。无故障证明检查操作是否符合这本账簿的规则；这些规则是否忠实覆盖相关 C 行为，还需要逐项审阅。
ZlibF/Runtime/ 定义翻译后运行的含义。Space.lean 提供对象引用和更新，Monad.lean 提供故障、顺序执行和循环，Ptr.lean 提供指针算术、读写和比较。Libc.lean 建模所需库操作，Alloc.lean 导入它。Schema.lean、Tables.lean、LibcTables.lean 提供生成的记录、常量、堆表和每类结构体的操作。其生成器和运行时结构参考也属于该依赖。
无故障定理针对这些定义。预期对应关系是可达 C 未定义行为成为 Fault.ub，但受下述限制。无符号算术是模算术。每处翻译必须检查有符号算术、移位和转换。循环额度为 2^64，耗尽产生 Fault.outOfFuel，终止证明必须排除它。
内存与库操作
“存活”表示对象尚未释放；“新鲜”表示准备分配的编号没有被占用；“帧性质”表示调用没有改动它无权修改的其他对象。例如，释放流私有窗口不应改写调用者的另一块输入缓冲区。这三个条件回答不同的问题，后面的表分别说明运行时怎样检查它们。
堆为各种对象设置独立表。已释放块号永不复用。分配器只在 nextBlk 标识在对应位置尚未使用时写入，否则故障。Fresh 保护未来标识。初始堆还必须在 nextBlk 以下跨表具有唯一块标识；单独 Fresh 不表达该条件。
| 操作 | 需要审阅的模型行为 |
|---|---|
memcpy, zmemcpy |
即使长度为零也拒绝空指针，并拒绝重叠范围和只读目标。整记录复制使用 copyK，会拒绝对象复制到自身。直接记录读取/存储对不会检查重叠。 |
memmove |
检查相同范围与可写性，但允许重叠，并从原始源复制。 |
memset, zmemzero |
Ptr.fill 按元素计数并赋值；只有指定用法才表示字节 memset 或零填充。Ptr.memset 重复一个字节。整记录清零存储显式零记录。 |
strlen |
要求表示出的块内有 NUL。 |
| 分配 | 新鲜整数来自任意初值函数，新鲜指针字段为 NULL。allocOk 预言机决定失败。自动局部对象绕过它，不消耗分配尝试。 |
free |
NULL 无操作。否则参数必须指向对应种类的存活可写分配起点。没有分配来源标签。 |
| 字符串字面量 | strLitRef 表示生成的封闭 strTable 中静态、只读、NUL 结尾的条目。它始终存活、身份稳定且永不释放。未知字面量文本会故障。其他外部字符串使用不同分配路径。 |
运行时没有提供通用的 calloc、realloc、格式化、errno、abs 或 strerror 模型。翻译提供其需要的特定行为。这些定义也需要审阅；放在 Runtime/ 外不会降低其语义作用。
表示缺口与证明义务
| 选择或缺口 | 对 C 结论的影响 |
|---|---|
| 未初始化指针变成 NULL | 相等比较、复制和释放 NULL 可在没有先写入时成功。每次指针读取都需要先写后读论证。init 翻译显式清零两个分配的流状态记录；这不是新鲜记录或自动 z_stream 存储的普遍性质。弥补缺口需要为所有指针形式跟踪初始化，或引入独立未初始化值，并检查操作、修改对应翻译。 |
| 每单元一个任意初值 | 整数定理对每个 Heap.garbage 量化，以分配尝试和单元位置为索引。但同一单元重复读取仍一致。在 C 允许不稳定未指定值的情形，证明不能依赖这种一致性。 |
| 数组范围由谓词表达 | WellFormed、Heap.RecordsWellFormed、Statics.WellFormed 必须建立 C 长度。生成的保持引理保留它们。静态内容必须匹配定义它的 C 翻译；运行时不与 C 比较。 |
| 指针相等采用结构相等 | 不同对象比较为不等，悬空指针相等比较不故障。证明不能依赖 C 不保证的结果，包括相邻对象边界处的相等。关系比较要求同一个存活数组。 |
| 部分允许空指针算术 | Ptr.add NULL 0 返回 NULL。Ptr.diff 拒绝空参数，但 Compress.ptrDiff 对两个空指针返回零。这些选择需要针对相应 C 调用单独论证有定义性。Ptr.diff 注释归因于 C23 并不准确；见操作与语言对照。 |
| 地址与布局模型不完整 | 没有通用 ABI 地址、有效类型或记录字节视图模型。CRC 观察地址低位：堆字节块保留对齐起点，静态和内嵌字节起点有任意稳定余数。可配置这些元数据而不改变现有存储。按字节组装的字加载不能解决 C 转换的别名语义。标量单元适配器可能省略别名。见偏离。 |
| 只读标记不完整 | 字节块、具名静态表和实例可以只读。字块和表内记录不能表示该限定。 |
| 指针构造检查不完整 | Ptr.add 检查结果，不检查手工构造的起始偏移是否有效。翻译审阅必须排除公开 Ptr.ref 构造器的无效用法。 |
| 不跟踪对象来源 | 翻译代码可释放由 allocBytes 创建的调用者块。在 API 禁止时，帧性质和所有权条款必须防止它。错误种类的状态转换会比对应 C 访问更早故障。 |
这些是模型限制，不允许悄悄缩小公开定理。运行时审阅是这些选择的历史证据，不是对当前基线的独立批准。
表更新
Tbl 包装数组，并按块标识作为全函数读取。不存在的条目返回默认值（none 或 false）。upd 从 Tbl.get_set 得到已证明的同键、异键和重复更新规则。
写入原语使用 Space.modify 移出、修改并放回数组，避免保留此前数组的链。Space.modify_eq 声明它与更简单的函数式 put 操作相等。可信审阅必须覆盖 Tbl.get_set、Tbl.modify_eq，以及每个生成的 Space 实例的 modify 和 modify_eq。操作引理用 put 推理；执行性能不能建立对应关系。见表更新审阅。
3. 手工翻译
ZlibF/Zlib/ 中的翻译逐语句编写。内核不检查其与 C 的对应关系。审阅必须检查求值顺序、检查条件、算术、存储生命周期和效果。不匹配是翻译缺陷，必须修正并加入差分回归，绝不能通过改变定理隐藏。翻译规则要求逐函数证据。测试清单为 tests/list.txt。
差分测试将有限执行与真实 C 比较，提供忠实性证据而非证明。尤其是，结果一致和 sanitizer 没有报错，都不能建立 C 表达式具有有定义语义。
4. 选定源码
验证源码是固定的 zlib/ 子模块，加上按文件名顺序应用的 patches/*.patch。绝不修改子模块。只有阻碍证明的确认上游缺陷才允许补丁；它必须最小化，并匹配已提交的上游修复。上游合并且固定版本移过修复后删除补丁。
当前没有补丁。补丁登记记录选定源码策略。历史提案不会仅因笔记提及，就成为验证源码的一部分。
5. 配置与外部世界
首个目标是默认 x86_64 Linux/LP64 静态构建和默认分配器。接受的平台范围要求每个表示出的字节对象小于 2^63 字节。这是环境前提；zlib 证明建立其操作保持该条件。
分配失败仍在范围内。其他上游配置和自定义分配器需要自己的对应关系论证；完整项目目标包含它们。
gz 文件世界和格式化模型是额外的可信语义。其支持的文件种类、错误、转换和外部字符串分配不能表示每种操作系统或库行为。回调正确性依赖显式返回协议、有限输入界限和窗口保持假设。偏离记录公开适配器的相应限制。编译器、操作系统和硬件正确性在证明之外。
6. 命题与权威
证明可能建立不完整或错误的规范。审阅者必须将目标、前置条件和具名规范标识与 API、格式及选定 C 比较，还要确认 init 建立不变量、调用者定义域没有缩小。
锁保留定义和定理类型，不批准其含义。独立基线审阅与强制仓库保护构成这条权威边界。验证策略解释该机制。当前已检查结果和未解决义务统一放在进度。