独立集成审阅

多个单独检查过的改动合在一起，仍可能改变保护策略、引入冲突，或使某些检查没有跑完。本审阅检查这些集成边界，覆盖下面三个拉取请求。它不重新推导每条翻译后的 C 语句，也不建立完整的 zlib 验证。当前义务仍见进度。

审阅过的快照

“源码快照”用不可变的提交标识指明当时检查的版本；表中的请求编号属于这份历史记录。下面的通过或超时结果只对应各自记载的版本与检查范围。

发现与修正

请求 7 和 9 的失败审计报告了受保护源码策略差异，没有报告证明重复登记。旧批准策略漏掉十六个移动后的文档文件。兼容策略在两个审阅快照上都精确复现候选策略：分别为 310 和 312 个受保护文件。比较中没有缺失路径、多余路径或变化的摘要。

请求 8 保留旧文档范围，并添加新的 API 和格式目录。五个移动后的规范页面在新布局中是必需的。空布局、混合布局和未知手册布局都会被拒绝。其 21 个回归测试通过；三个布局测试也在禁用断言时通过。

集成请求 7 和 8 会在策略计算及其生成锁中产生冲突。集成保留兼容实现和新的拒绝测试。生成锁需要声明审计；不能通过手工编辑摘要来解决冲突标记。

默认初始化证明陈述精确的既有公开目标。成功路径从实际分配、Reset 和初始化建立表示不变量。失败清理和具体成功见证都显式给出。它不假设通用 Init2 契约。独立重跑的五个变异全部被拒绝：三个包装函数变化被原来的精确证明拒绝，两个同步主体变化被其执行证明拒绝。正向基线也通过。

更早的登记批次包含显式语义变化，不只是新增证明。尤其是 Adler NULL 查询定义域变窄，以及字节地址模型变化。其已记录范围仍然必要。抽象模型目标不能建立实现细化。

警告清理在 67 个数学和证明模块中替换 673 个已弃用条件引理引用。不改变定理命题、规范、翻译或运行时定义，也不关闭未使用化简诊断。工作流的检出引用使用发行版 7.0.1 的固定修订，其声明的运行时为 Node.js 24。这是有意修改受保护工作流文件。

请求 9 的完整重跑超过审计作业的 90 分钟限制。日志记录基线通过，以及取消前八个负向例子被拒绝。该次每轮声明审计约需五分半钟；剩余例子和运行时变异尚未完成。审计作业现在有 180 分钟。命令、锁、负向例子和证明变异不变。超时不是审计通过。

并行证明工作

另一个源码快照包含两条正在进行的流证明开发。压缩器将实际默认初始化、输入补充和一次不 Flush 的慢路径迭代，联系到同一堆上的已存符号含义。解码器将其慢路径的长度／距离／匹配链联系到调用者范围。这些是带条件的内部结果，不是精确公开流目标。两个选定组合模块都通过独立的全新内核重放。检查过的证明只使用三个允许公理。

捕获快照时，四个新解码器模块在根导入闭包之外。即使导入的根能构建，覆盖检查仍拒绝这个快照。这是对在建工作的观察，不是对三个已审阅提交的观察。并行源码未包含在本次集成中。

提出的字节对象平台前提也改变了此前的公开 inflate 定义域。文档显式说明了这个变化。未修改的序列目标不继承该前提。本审阅不将受限范围结果计为旧定义域或序列目标的证明。

验收

只有明确命名的最终集成提交上记录的检查，才能建立其 CI 状态。请求已合并、本地构建或锁已重新生成，本身都不代表验收。差分检查仍是翻译忠实性的有限证据，不是证明。本审阅不声称完整流正确性。

审计执行时间

集成后的主分支运行也超过 180 分钟。核心审计和全部十三个负向例子通过。三个函数变异批次通过，随后剩余工作因作业时间限制被取消。这不是完整审计通过，也不能建立未执行变异的结果。

核心审计、负向例子和函数变异检查现在在同一提交上的独立作业中运行。每个工作节点保留原始命令，并构建自己的检出目录。必需的 audit 状态只有在三个工作节点全部成功时才通过。任意节点失败、取消或跳过都会使该状态失败。其他必需状态仍为 build、no-sorry 和 difftest。