已接受的平台假设

初始范围是默认 x86_64 Linux/LP64 静态构建，使用默认分配器。 本页陈述其环境假设，不要求 zlib 证明操作系统、编译器或硬件的性质。

字节对象大小

每个被表示的字节对象都少于 2^63 字节。该上界作为系统环境的一部分被接受。 它覆盖调用者提供的存储、原始字节块、静态数组和嵌入的字节数组视图。

用 h 表示执行前的堆，ref 表示一个字节对象的引用，a 表示该引用对应的字节数组。Space.get h ref 查询这个对象，a.size 给出它的字节数。精确谓词是 PlatformMemory.lean 中的 ZlibF.PlatformMemory.ByteObjectsFit：

对每个被表示的字节引用 ref 及其数组 a：
    若 Space.get h ref = some a，则 a.size < 2^63

它分别约束每个对象，不约束所有分配的总大小，也不约束重复调用累计处理的长度。 默认、常见和全部支持的输入范围共享这一假设； 它不是额外的颜色，也不是压缩参数。

在执行证明中使用

定理可以把该谓词作为明确的环境前提。 Goal.inflate 直接写出这一前提。内部快速解码器入口证明从中推导整个输入／输出对象的大小事实。 这一上界使同一对象内有效偏移量的差处于有符号 64 位范围。

zlib 证明必须建立：实际初始化、分配和更新保持该前提。 替换缓冲区的调用者必须提供属于已接受环境的存储。 该谓词不能从任意数学堆或不受限制的运行时分配器中推导出来。

每条精确陈述保留自己的定义域。不需要该上界的陈述可以量化更大的数学定义域。 本页不会向这些陈述悄悄加入新假设。

其他指针义务

大小上界不能证明指针仍然存活、已初始化、与另一个指针属于同一对象，或偏移有效。 这些是独立的安全性义务。运行时关于空指针算术的选择仍记录在 模型比较和可信基础中。