公开验证目标

结论要求公开 API 安全并满足文档规定的行为。首个目标是默认 x86_64 Linux 静态构建，使用默认分配器。分配失败属于范围之内。项目还以覆盖上游 CI 构建的每一种配置为目标。

tests/audit/public-api.json 根据固定版本的 zlib.h 固定公开入口清单。每个条目给出翻译后的函数、手册章节及其所需最终目标。共有 95 个默认构建入口和八个族级义务：四个生命周期契约和四个初始化定义域契约。仅 Windows 支持的 gzopen_w 单独标识。清单条目是一项要求，不是证明。

契约覆盖整个调用

先以一次有输出的解压调用为例：返回码正确还不够，写入字节、输入／输出指针、保留状态与内存访问范围都必须描述同一次执行。“帧性质”约束没有被授权修改的内存保持不变；“所有权”约束哪些分配归流保管、最终由谁释放。

具体目标位于 ZlibF/Spec/Public/；Domains.lean 和 Sequences.lean 添加族级义务。Calls.lean 固定实际翻译后的执行。契约审阅解释它们与无堆 API 模型、独立字节格式的区别。任何一种模型定理都不能单独证明具体公开契约。

API 手册解释签名、参数、作用、调用顺序和所有权。有些简短手册描述受限用法。其文档前提不会从已登记目标中移除其他情形。手册范围和偏离说明明确这些限制。形式目标变化需要单独审阅。

生命周期与非空性

四个目标覆盖 inflate、deflate、回调 inflate 和 gz 调用历史。安全和清理对有限的合法历史量化，包括允许的 Reset、字典变化、Copy、恢复、End 和 Close。副本拥有独立存储，并保留可观察的后续行为。

普通数据阶段把实际已接受和已产生的字节联系到独立格式。完成的压缩产生有效数据。在包装、窗口和字典设置兼容时，解压还原输入。校验和满足其数学定义。高级操作仍须满足各入口作用和无条件的序列安全；普通数据阶段的精确边界见契约审阅。不能把这个边界误认为已经完整细化所有高级组合。

“定义域非空”要求允许的状态确实能由初始化产生，不能只证明一个永远无法满足的前提。四个初始化定义域目标要求：Init 对每个文档规定的参数组合，在成功时建立表示不变量，失败时清理。实际初始化由此保证定义域非空。一个方便的见证不能替代所有参数的覆盖。具体见证补充顶层结果。最终定理不得假设未经证明的库内被调函数契约。

flowchart LR
    I["Init 建立不变量"] --> C["逐次调用的执行与作用"]
    C --> P["不变量保持"]
    P --> C
    C --> E["End 释放所拥有资源"]
    C --> S["合法历史与字节格式正确性"]

调用者假设与语义边界

调用者提供存活对象，以及 API 要求的可读或可写范围。同一个流上的调用按顺序执行。调用者不修改库所拥有的状态。缓冲区重叠条件和标量指针的表示限制需要对照公开契约审阅。任何更强限制都应写入偏离说明。允许的库调用若出现未定义行为，这是阻塞问题，而不是新增调用者限制的理由。

回调和系统调用属于外部。其文档规定的内存契约是前提假设。终止性还假设它们会返回，并且在无限输入可能导致永久运行的场景中，回调输入有限。这不是关于任意调用者代码或操作系统的定理。

结论不包括编译器和操作系统正确性、性能、常数时间行为，也不包括抵御解压炸弹的资源界限。格式错误的压缩数据仍在范围内。可信语义边界见可信基础。

验收

检查指南区分覆盖、开发检查、规范就绪和最终证明验收。每个最终目标都需要精确匹配的已登记定理、允许的公理依赖、由 Init 建立的不变量、帧性质与所有权证明，以及函数证明变异。问题和基线必须得到独立审阅批准。明确命名的提交上，四个 CI 作业都必须通过。有限差分测试支持忠实性判断，但不是证明。当前证明进度和阻塞项只在进度中记录。