可信运行时审阅记录

这是一份历史源码审阅。发现描述审阅当时读取的定义与文档，不是当前缺陷清单，也不是独立基线批准。有些观察后来已处理；另一些描述有意保留的语义边界。当前工作见进度，当前假设说明见可信基础。

范围与证据

审阅读取 ZlibF/Runtime/ 下的 Space、Monad、Ptr、Alloc、Tables 和 Schema 模块、模式生成器、运行时模式文档、安全文档与翻译规则，并与固定版本的 zlib.h、deflate.h、inflate.h、inftrees.h、gzguts.h、zutil.h、zconf.h、deflate.c、inflate.c、trees.c 和 uncompr.c 比较。首轮之后又进行了对抗性重读。没有执行构建或差分运行。下文“已确认”表示有这些定义和源码解读支持，不是编译后的证明或 Sanitizer 复现。审阅没有修改源码。

严重程度衡量对“成功模型运行排除 C 未定义行为”这一结论的风险。高风险允许实质错误的安全论证；中风险需要另一个翻译或定理错误，或给出不同的 C 语义；低风险涉及完备性或文档。这些是历史评级，不评价上游漏洞。

模型把执行写成逐步组合的计算：后一步接收前一步返回的内存和结果；这种组合结构称为 monad。审阅发现故障会经这种结构传播，循环规则不会隐藏步数预算耗尽。其关注点是表示边界、缺失的初始化历史、模式常量，以及文档的过度陈述。

发现 R1–R13

R1. 新分配的指针字段被建模为空，而非不确定指针

历史严重程度：对一般结论为 高风险，对审阅过的 zlib 路径为 中风险。Schema.lean 的垃圾值构造器使用默认指针；Space.lean 将该默认值定义为空；Tables.lean 分配这些记录。因此，分配记录后加载未写入的指针，将其与空指针比较或传给 freeB 都可能成功。整数垃圾值的全称量化没有覆盖不确定指针。

审阅使用以下 C 例子暴露差距：

z_stream *s = malloc(sizeof *s);
if (s) { free(s->next_in); free(s); }

审阅过的 inflate 和 deflate 初始化路径在分配后立即将其状态清零。其他记录，尤其是 gz_state，需要单独检查。建议修复包括指针字段初始化标记，或显式的未初始化指针值。核心证明义务涉及时间顺序：每个指针字段必须先写后读。旧安全与翻译文档声称会出现故障，而模式文档描述为空指针；这个矛盾也是 R1 的一部分。

R2. 空指针算术是一项语义决定

历史严重程度：低风险。Ptr.add 和 Ptr.add_null_zero 接受 NULL + 0。审阅将其视为有意的模型例外，不是新发现的 zlib 缺陷。历史日期标签不能证明 C23 中该操作有定义；见当前操作／语言对比。审阅还记录 Ptr.diff null null 会故障。

任何支持的 C 方言及空指针算术例外都必须写入可信基础；证明不能悄悄将模型决定变成对所有 C 构建的结论。

R3. 一个模式名称代表两个不同的 COPY 常量

历史严重程度：若使用则为 高风险，按审阅到的可达路径为 中风险。Schema.COPY 是 inflate 模式值 16195，而 gzguts.h 对 state->how 定义的 COPY 是 1。生成器跳过与枚举项名称冲突的宏。使用共享名称的 gz 翻译因此可能验证错误的状态机。GZIP 也有相关名称冲突，但其数值与 gz 用法一致。建议使用不同名称，或让常量按翻译单元划分作用域。

R4. 枚举常量被赋予无符号类型

历史严重程度：中风险。枚举项数值与 C 一致，但模式将 HEAD、CODES 等常量赋为 UInt32。在审阅目标上，C 枚举常量类型为 int。例如，将 int x = -1 与 HEAD 比较时，若常量强制无符号比较，结果就会不同。正确的字段存储类型不能修正常量表达式类型。建议将有符号常量与转为枚举存储类型的转换分开。

R5. 固定数组长度与静态内容需要不变量

历史严重程度：中风险。记录字段是 Lean 数组，C 长度只写在注释中。stK 接受任意记录，只有垃圾值构造器施加长度限制。具有 lens.size = 321 的 inflate 状态在模型中允许访问下标 320，尽管 C 只有 320 个单元。静态数组默认空；任意假定内容也可能满足一个过弱定理。审阅建议生成由存储操作保持的形状谓词，并对照 C 检查规范静态数据。内部形状要求必须由 Init 建立并持续保持，不能悄悄作为更窄的公开调用者定义域。

R6. 分配依赖新鲜性，而不检查它

历史严重程度：中风险，有条件。审阅过的分配器直接写入 nextBlk，不检查其是否未用。若块 0 已有存活字节块且 nextBlk = 0，分配可能覆盖它并清除只读状态。从预期空堆开始的运行会保持新鲜性，但任意堆定理需要显式新鲜性，以及 nextBlk 以下跨表块编号唯一性。这记录的是旧实现，不能解读为当前分配仍会覆盖存活块。

R7. 只读状态没有覆盖每种对象

历史严重程度：中风险，对审阅过的 zlib 用法为 低风险。字节和命名静态对象支持只读标记；字块和已分配记录不支持，freeW 也不检查它。模型无法表达一般的常量字数组对象。审阅过的 zlib 源码不需要这种对象；未来翻译或见证不能假设具备这个能力。

R8. 指针相等性无条件区分对象身份

历史严重程度：低风险 到 中风险。派生的指针相等性使不同对象的引用不相等，包括相邻对象的尾后一位／起始地址。C 不一定对每种比较都给出该结果。涉及悬空指针的相等比较也仍可用。审阅建议显式的检查式或非确定相等性边界。这些情况是否可达、是否被依赖，需要翻译证据。

R9. 未初始化整数的每个单元只取一个固定值

历史严重程度：中风险，是语义选择。Alloc.lean 在分配时通过垃圾值预言机一次填充新单元。因此重复读取一致，而某些 C 解读允许不稳定的未指定值。依赖这种一致性的证明可能超出模型对 C 的正当依据。审阅过的 slide_hash 和 longest_match 用法没有依赖它。关于初始化位的旧注释也不正确，见 R12。

R10. 整记录复制缺少重叠检查

历史严重程度：中风险，是翻译规则问题。先加载记录再存储允许自复制，而重叠的 memcpy 在 C 中属于未定义行为。审阅过的 deflateCopy 和 inflateCopy 位置使用不同记录。未来复制原语或证明必须同时检查对象身份和嵌入记录重叠。整记录清零也需审阅是否清零每个 C 字段；手写零记录不自动保证忠实。

R11. 更小的原语边界

R12. 文档夸大或错误描述模型

旧文档声称存在运行时并未提供的初始化位、类型标签和未写指针读取故障。它们对固定 Huffman 表的位置说法不一致：所选源码在 inflate_fixed 中由 inftrees.c 包含 inffixed.h。生成器对冲突的 COPY 和 GZ_OFF_MAX 所给“不是整数常量表达式”的解释不正确；后者的 sizeof 表达式超出其求值器能力。可信基础文档还错误声称没有差分测试。这些是历史不匹配，不是对当前文档的断言。

R13. 静态数据生成省略了部分源码依据

历史严重程度：低风险。trees.c 的 bl_order 未出现在 Statics 中。StaticTreeDesc 采用硬编码而非提取，因此可能漏掉源码偏移。审阅的描述符三元组 (extra_base, elems, max_length) 为 (257, 286, 15)、(0, 30, 15) 和 (0, 19, 7)。默认静态值不能建立这些事实。

审阅记录的模式对比

审阅在 ZStream、GzHeader、CtData、TreeDesc、默认构建的 DeflateState、Code、InflateState、GzFile、GzState 和 StaticTreeDesc 中未发现字段遗漏、颠倒或尺寸错误。检查了数组长度 573、61、39、16、573、573、320、288 和 1444，以及不相交的垃圾值下标范围。宏和枚举项数值与所选默认分支一致，但有上述名称和类型发现的例外。不覆盖 LIT_MEM 或 ZLIB_DEBUG。目标上普通 char 有符号；字节指针表示仍要求在翻译后的字符读取处显式进行符号扩展。

尚缺执行证据的问题 U1–U5

在审阅范围内正确的原语行为

审阅过的加载／存储拒绝空指针、悬空和越界访问；存储还拒绝只读目标。尾后一位指针不可读。字节 memcpy 拒绝重叠，而移动操作在两个重叠方向都使用原始源内容。freeB 将空指针作为无操作接受，拒绝非零偏移、静态对象、嵌入数组、已释放块和只读块。从不复用的块编号支持审阅过的释放后使用和重复释放规则。移除父对象会使嵌入记录引用失效。

顺序组合操作 bind 传播错误，OkOn 要求实际成功结果，循环规则要求低于步数预算的界限。若块没有终止符，strlenB 会故障。这些源码观察不能建立完整运行时／C 等价性，也不批准基线。