从 C 到经过检查的定理

定理针对的是一个 Lean 计算。将它用于 zlib，需要审阅两个联系：运行时必须表示相关 C 操作，翻译必须对应选定的 C 源码。内核在这些选择确定后检查证明，并不检查它们与 C 的这两个联系。可信基础记录了这条边界。

各层的关系

flowchart TD
    C["固定的 zlib 源码 + 按顺序应用的补丁"] --> T["逐语句翻译"]
    R["运行时：对象、指针、算术、故障、循环"] --> T
    T --> P["执行证明：无故障、终止、帧性质、所有权"]
    T --> F["细化证明"]
    M["不涉及堆的算法和 API 模型"] --> F
    S["独立的格式规范"] --> M
    S --> F
    P --> A["公开调用与合法调用序列"]
    F --> A

安全性与功能正确性使用同一组具体状态。不涉及堆的数学内容放在 ZlibF/Math/；不能仅因为内存证明使用它，就让它依赖堆。中间算法模型可用于分离数学推理与内存推理，但仍需要细化证明，将模型连接到翻译后的函数。

选定源码与模块布局

首个目标是默认 x86_64 Linux 静态构建，使用 LP64 位宽和默认分配器。分配失败在范围内。其他构建配置和自定义分配器实现是独立范围，记录在表示限制中。绝不修改源码子模块。只有确认的上游缺陷才允许补丁，并须遵守仓库 AGENTS.md 与 patches/README.md 的规则。

较大的 C 文件模块可以有支持子模块。函数名保留 C 名称，函数文档字符串以 C 签名开头。翻译规则详细描述对应关系。

对象堆与字段更新

例如，C 中的 s->strstart = 8 更新压缩状态的一项字段。对象堆把它表示为“在状态对象 s 中把 strstart 改成 8”，而不先计算该字段在机器地址中的字节偏移。这样，证明可以明确指出改了哪个对象、哪项字段，同时说明其他对象没有变化。

C 结构体表示为 Lean 记录。堆分别为记录、字节数组、字数组和其他元素类型设置表。指针命名一个对象、嵌入数组或静态数组，并附带元素索引；它不包含机器地址。

flowchart LR
    P["指针：空指针，或引用 + 索引"] --> B["堆字节块/字块"]
    P --> E["记录内嵌数组"]
    P --> S["静态数组"]
    H["堆"] --> B
    H --> K["记录表：流、inflate 状态、deflate 状态等"]
    K --> E
    H --> O["分配预言机、新鲜块计数器、任意初值"]

这样可以直接表达字段更新和帧性质。记录字段是投影，修改字段就是记录更新。更新字节不能改变另一张表中的记录。复制整个记录时，也复制其内嵌数组。生成的运行时结构参考列出全部字段、指针构造器和类型选择。

这种表示刻意避免 ABI 字节偏移，因此不能提供任意结构体的字节视图，也不能表示标量单元与缓冲区之间所有可能的别名。记录类型不保证数组字段的长度。需要时，由 WellFormed、Heap.RecordsWellFormed 和 Statics.WellFormed 提供这些事实。证明必须携带它们，或从表示不变量推出它们。

执行与故障

运行时返回结果值和最终堆，或者返回故障。Fault.ub 表示模型覆盖的未定义操作；Fault.outOfFuel 表示循环额度耗尽，终止证明必须排除它。安全性定义给出完整义务。

语言操作定义在 Space.lean、Monad.lean 和 Ptr.lean。建模的 C 库操作定义在 Libc.lean 和生成的 LibcTables.lean。生成的结构定义与记录访问操作位于 Schema.lean 和 Tables.lean。

证明必须尊重的语义差异

这些是设计限制，不是关于 C 的额外结论。准确细节以可信基础和表示限制为准。

自动存储必须保留 C 生命周期，且不能消耗默认分配器的失败索引。地址传入调用的局部对象仍需要表示出的存储和清理。证明不能通过悄悄限制公开定义域来弥补表示缺口。

设计决定

这些标识用于追溯较早的设计讨论。它们描述所选方案；其可靠性义务仍见可信基础与证明指南。

组合调用时不预设答案

辅助函数定理证明实际翻译后辅助函数的性质。调用者建立其前置条件，再使用定理。辅助函数契约绝不能作为替代执行的假设。内部义务命名了调用者必须建立的条件。

每个状态记录的表示不变量携带边界、所有权和正确性所需的历史。初始化建立它，后续调用保持它，结束函数释放拥有的存储。这也建立了不变量可达的事实。整个序列的证明随后组合这些函数定理，包括拒绝和分配失败。方法见证明指南，验收标准见检查指南。

设计指南 · 文档首页