参考文档 / ZLIB × LEAN

证明细节

先从引擎的完整论证进入，再按查表、复制、编码和内存等组件查阅细节。每条路线都连接到具体函数约定和相关定义。

inflate.c

解压引擎

窗口内容、真实模式、位前缀、查表、退出与跨调用序列。

deflate.c

窗口、哈希链、匹配搜索、策略循环、符号账本、块输出与默认封装。

下面按实现步骤排列关键引理。先读每项解决的问题和前提，再点击查看具体推导；完整接口证明需要把这些步骤连接起来。

动态表内容
动态块先给出码长，构造器必须把这些码长变成实际可读的表。这条结果展开 inflate_table，同时给出安全/返回分类和构造内容关系 TableConstruction：成功时记录规范编码叶子、子表链接和返回范围，也包括空表、单符号表和错误返回。
调用前提 CallPre 要求码长输入可读、目标表容量可写，并满足相应分离条件。构造内容还要连接到解码器使用的表关系和实际状态；完整流解码证明尚未由此完成。inflate_table_construction
状态与窗口释放
结束调用要释放流拥有的状态和窗口，同时保留调用者的其他对象。这条对应 Goal.inflateEnd 的执行返回 Z_OK、清空状态指针，按照所有权关系 InflateOwned 精确移除活块，并保持无关存储和分配计数。
Goal.inflateEnd 要求状态满足 Good，并使用默认释放函数 zcfree。它使用已有的 Good 条件；所有公开调用历史是否都能建立该条件，仍要通过初始化和保持性结果连接。当前接受证据见项目进度。inflate_end_public

默认初始化与分配失败
默认初始化先建立可继续使用的压缩器，也必须清理失败到一半的分配。这条结果展开固定配置的 deflateInit_，建立 Goal.deflateInit_，包括任意压缩级别、版本和参数拒绝、五次分配的成功/失败、清理、所有权与初始化不变量。
前提保留未来分配身份未占用 Fresh、现有身份唯一 Uniq、库静态数据、调用者存储、版本及默认或空分配器条件。配置固定为窗口指数 15、内存级别 8、策略 0；通用 Goal.deflateInit2_ 不在这条结果内。deflateInit_proof