安全性主张与调用者义务

目标是：zlib.h 允许的每次调用都避免未定义行为、能够返回，并保持内存所有权。 这是目标，不是所有函数都已获证明的声明。 进度记录受检状态与剩余工作。证明方法解释这些义务如何成为 Lean 定理。 可信基础说明模型结果应用于 C 前，哪些地方还需要独立论证。

已接受的平台假设，包括每个字节对象的大小上界，属于环境前提。 执行证明建立这些前提在执行中的保持性。

术语与阅读指南

未定义行为（UB）指适用 C 标准对其行为不作保证的程序操作。 它不一定引发崩溃。一次执行成功或与测试一致，都不能证明该操作有定义。 这一术语遵循 C 草案 N1570 第 3.4.3 节。

应区分以下情况：

所选构建中由实现定义的选择必须明确写出。 对于未指定结果，只要它会影响结论，证明就必须覆盖每一种允许的结果。 这两个术语都不表示 UB。关于 C 的主张既需要无故障执行证明，也需要所用操作与 C 对应的论证， 包括已记录的模型缺口。

第 1 节介绍单次调用，第 2 节介绍完整生命周期，第 3 节介绍 UB 和模型限制，第 4 节介绍调用者义务。 API和格式规定功能要求。

1. 单次调用的安全保证

对每个允许的调用者状态和参数，翻译后的函数都无故障地返回。 它保持共享表示不变量，只修改许可内存，并核算每次分配和释放。错误返回也包括在内。这里的“表示不变量”是一组关于真实状态和内存的事实，例如某个窗口仍然存活、有效历史不超过容量、游标仍指向允许的范围；只有它们继续成立，下一次调用才有可靠的起点。

初始化必须从允许的调用者状态建立不变量。被调函数契约必须是关于该函数的已证明定理， 不能将它作为假设来完成调用者的证明。顶层定理还需要具体见证。 一个见证或不可满足的不变量，都不能替代对所有允许参数的覆盖。

flowchart LR
    I[初始化] -->|建立| V[共享不变量]
    V --> A[合法 API 调用]
    A -->|保持| V
    V --> E[结束]
    E --> Z[流不再拥有存活块]
    I -->|分配失败时清理| Z

无泄漏涉及整个生命周期。初始化成功后，分配的内存由流拥有。 结束操作恰好释放每个自有块一次。初始化失败则释放该次尝试分配的全部内存。 结束操作或初始化失败后的存活块集合，等于初始化前的集合。复制操作和部分失败路径需要相同核算。 失败操作必须留下一个状态，使文档允许的恢复或结束操作仍然安全。

2. 调用与调用序列

调用序列安全性也是目标的一部分。只有初始化建立不变量、每个允许的转换保持不变量后， 才能通过归纳得出这一性质。这包括重置、字典、位预置、复制、恢复和结束。 孤立函数引理的集合不足以建立序列安全性。

终止性指每个循环都在步数预算上限前完成。运行时使用 2^64 次迭代的预算；耗尽它是独立故障。 终止性和无泄漏在本项目中都属于安全义务，尽管它们本身并不是 C 未定义行为的实例。

3. 故障、未定义行为与模型缺口

下面的标识符命名安全性义务。运行时故障检测许多违规，但仅靠它们不能建立 C 安全性： 本节例外与可信基础第 2 项仍属于论证的一部分。

翻译中的无符号算术回绕。有符号算术和移位由翻译操作检查，计算单子本身不会自动检查。 U1 到 U10 描述 C 和表示义务。U11、U12 增加终止性和资源要求； 这不表示每种失败都是 C UB。

空指针与指针差

当前实现区分三类规则：

应阅读 Ptr.add 与 Ptr.diff 以及压缩器辅助函数的定义， 不要从“指针差”这一名称推断规则。NULL 可以展开为空指针常量；表格描述的是有类型指针值，而非宏的拼写。

N1570 第 6.5.6 节 要求指针算术相对于数组进行，相减的指针属于同一数组，结果也必须可表示。 空指针不指向数组元素。C23 草案 N3096 第 6.5.6 节 保留这些条件。因此，Ptr.diff 源码注释将两个空指针相减为零归因于 C23，并不准确。 该注释既不改变实际执行的定义，也不提供语言保证。

N3261为后续 C 修订版提议放宽空／零操作。 它不能授权本项目在现有 C 目标下悄悄将这些操作视为有定义。 对应关系审阅必须确定所依赖的语言版本及实现扩展。差分结果相同、运行时检测器未报错，都不能完成这一义务。

因此，当前模型不能检测 C 中每一种可能未定义的空指针算术操作。 这一限制必须纳入主张范围。运行时或翻译的任何修正都需要独立审阅，并重新检查证明。 进度记录尚待完成的审阅。

未初始化内存

新分配的整数单元包含来自 Heap.garbage 的任意值。 定理必须对每一种提供任意初值的函数 garbage 成立。模型在一次执行中为每个单元指定固定值，因此重复读取一致。 它不模拟每次读取都重新取得未指定值。证明不能依赖这种一致性来论证 C 行为。 字节复制也会复制这些值，包括垃圾值。

这一点关系到访问未清零 prev 项的 slide_hash，以及比较实际输入数据之外字节的 longest_match。 其源码注释解释了预期结果应独立于这些内容。相应执行证明需要建立这一独立性，并为实际到达的前驱槽提供先写后读的证据。 仅量化任意值，不能证明输出独立，也不能证明哈希链遍历只会到达写入真实位置的项。

模型把新分配的指针字段设为 NULL。这比跟踪未初始化指针更弱： 与 NULL 比较、复制和 free(NULL) 都可以成功，而不会检测缺失写入。 因此，每次读取指针字段都需要更早写入的证据。两个状态初始化的翻译显式清零其分配的状态记录。 这不会初始化所有调用者记录或自动流记录。压缩器的自动流最初含任意整数字段和模型空指针； 其字段写入必须遵循 C。

对象表示

声明的记录数组长度需要 WellFormed 和 Heap.RecordsWellFormed 假设。 静态长度需要 Statics.WellFormed，数值必须匹配翻译后的 C 表。 Lean 的 Array 类型不会强制 C 数组的长度。分配需要 Fresh，以及有效的跨表块标识纪律。 模型没有初始化位或分配来源标签。只读标记覆盖字节块和被表示的静态对象，不覆盖所有有类型对象。

指针相等性使用对象标识和偏移。不同对象比较为不等，比较悬空指针也不引发故障。 在 C 不保证这些结果的地方，证明不能依赖它们。CRC 地址辅助函数只表示地址最低三位。 堆字节块保持起始地址对齐的约定。静态和嵌入字节对象的起始地址具有任意但稳定的余数。 这不是一般的 ABI、有效类型或标量别名模型；这些限制仍记录于偏差。

4. 调用者义务

公开定理必须明确陈述这些义务，并区分需要规范错误返回的无效参数和 C API 定义域之外的输入。

5. 其他性质

也要求功能正确性，见格式和API 契约。 格式错误的输入仍属于安全性定义域；错误返回不能掩盖故障。 自定义分配器和其他上游配置排在初始默认 x86_64 Linux/LP64 静态构建目标之后。 编译器与操作系统正确性、性能、栈空间上界，以及防解压炸弹的资源限制都在模型之外。 可信基础记录这些边界。