早期论证与参考来源

主要参考快照为 zlib-formal 的 0f1428677ebf5b1614ff77f4702bbb382b2bf3c6。参考审查阅读过其源代码和审计文档，没有重新构建快照，也没有在本仓库建立其结果。这里是复用记录；进度负责当前工作，检查指南定义验收。

借鉴的思路

阅读这份索引时，先用中间一列找需要的论证，再用左列定位旧来源，最后看右列的适用边界。路径和声明名保持原样，是为了能跳到实际定义；它们不是要求读者预先掌握的算法术语。后面的函数族表也按“可复用内容 → 当前落点”提供检索。

表中路径相对于参考仓库的 lean/ 目录。下表映射函数族与改变的表示。

不能直接迁移的部分

参考堆使用带类型单元和字节块；当前堆使用对象记录与表。堆声明和证明项需要适配。纯算术、位流关系、循环度量和分解，只有比较其定义与定义域之后才能保留含义。

参考序列定理 Zlib.Api.seq_safe 将 ApiContract 作为假设。其契约审计记录过假前置条件实例与错误策略契约。调用集合与归纳结构有价值，但条件序列定理不能在这里建立安全：每个库内被调用函数需要关于实际翻译的定理，实际初始化必须建立不变量。不相关的见证不能补足这一连接。

参考仓库的 ub.patch 政策及启用补丁不同，其构建配置和证明状态不会自动迁移。本仓库验证自己的上游固定版本与已审查补丁，采用自己的公开定义域和验收规则。

flowchart LR
    R[固定参考版本] --> M[提取数学与论证结构]
    M --> T[针对当前源代码与堆重新陈述]
    T --> K[内核检查、审计与变异]
    K --> C[仅接受本仓库的证据]

下表用于定位可复用论证族。组件证明指南解释当前论证结构。参考链接与历史测试报告都不属于新的验证运行。

复用早期论证

旧堆使用带标签单元和字节块，当前堆使用记录与对象表。纯论证只有在定义和定义域一致后才能迁移。堆级证明需要新的执行、帧性质和所有权论证。早期对被调用函数契约的假设不能替代实际翻译后函数的定理。

Deflate 引擎来源

Deflate 生命周期来源

Inflate 来源

表与尾部来源

回调来源

Gzip 来源

历史短距离检查

旧记录报告过一次实验，检查快速路径前可能缺少 whave 更新的疑点。raw 固定 Huffman 流使用一至三个字面量，随后接长度三、距离一至四的匹配。矩阵包括：至少六个输入字节、258 字节输出空间的快速调用；输入每次只给一字节；以及使用新输出缓冲区的两次调用解码。记录报告路径一致、出现预期的“invalid distance too far back”错误，且运行时检测器没有发现问题。

实验只对这些普通 inflate 情形反驳了候选问题，未覆盖长距离、完整或环绕窗口、其他窗口大小或回调解码器。它是历史测试证据，不是内核证明，也不是本次重新执行的验证。

证据边界

早期审查记录过 8000 次随机压缩会话，使用运行时检测器与往返比较。变化包括级别、策略、内存级别、包装、最小一字节输出块、刷新模式、参数改变和复制。记录报告这些会话中无不一致或运行时检测器诊断。该运行不包含字典设置、位预置、自定义 gzip 头，也排除了单字节窗口的 stored 路径。

这些观察不证明全部输入的安全、初始化历史、共享存储容量、其他配置或上述 C 假设。聚焦且可复现的证据应与其回归放在一起。验收规则属于检查指南，进度记录当前未解决项与证明验收。

历史 gzip 定位观察

早期记录报告：读取五字节到 EOF，再从当前位置向前定位五字节。Seek 返回十，而 tell 仍为五。其解释是向前定位保留 past；旧抽象关系却要求目标位置并清除该标志。本次修订未重新执行此实验。该源代码路径的操作细化尚未完成，记录只保留这次历史观察。