外部 I/O：文件、格式化与局部存储
9d47b7d12597c7bf · 对应提交的原文 ↗gzip 翻译除对象堆外，还需要文件操作、errno、字符串和格式化输出。已实现模型位于翻译 C 文件旁的 gzfs.lean，属于可信基础。Gzip 源码说明解释库控制流，API 契约定义预期公开行为。进度统一记录状态和剩余工作。
文件与堆效果
例如，读取三字节既要推进描述符位置，也要把三字节写入目的缓冲区。文件位置正确不代表内存写入范围正确；缓冲区安全也不代表文件读写行为已经完整表示。下面逐项列出模型实际实现的效果。
一次文件操作会同时改变两类状态：文件系统里的内容和描述符，以及库使用的内存。Fs 表示前者，Heap 表示后者；α 表示这次操作返回的值的类型。类型式 G α = StateT Fs C.M α 把文件系统状态接在运行时计算 C.M 上。计算返回一个值、两个更新后的状态，或者运行时故障。路径是扁平字节串。节点包含字节数组或目录标记。每个已打开描述符保存节点、位置及读/写/追加标志。描述符从 3 起分配，选择模型中最低的空闲槽位。
| 操作 | 已实现行为 |
|---|---|
open |
表示读写模式、创建、排他创建、截断和追加。无效模式和建模的路径失败设置 errno 并返回 -1。 |
read |
复制请求的普通文件字节，最多到 EOF。无效描述符、错误访问模式和目录读取会失败。没有独立短读或失败预言机。 |
write |
在当前位置写入，追加模式则在末尾写入。越过 EOF 定位后，后续写入用零填空隙。越过 fsizeLimit 会短写；在限制位置写入以 EFBIG 失败。 |
lseek |
支持 set/current/end 偏移，拒绝负结果和大于 2^63 - 1 的结果。 |
close |
释放模型中的描述符；无效描述符会失败。 |
fcntl |
在模型中没有效果。 |
errno 与 strerror |
显式整数，加上模型错误文本表。成功调用保留 errno；库显式重置它是另一种效果。 |
外部世界不表示管道、套接字、终端、信号、并发文件修改、权限、目录遍历、链接，或通过复制描述符共享打开文件。O_NONBLOCK、O_CLOEXEC 和 O_LARGEFILE 没有模型效果。尤其是，普通文件读取不能通过 EAGAIN 设置 again，不能在正数部分读取后失败，也无法暴露更广泛 I/O 预言机的所有清理路径。写失败主要模拟文件大小限制，不覆盖任意 EIO、EINTR 或 ENOSPC 行为。
这些是外部世界表示的限制。早期关于任意 POSIX 结果预言机、共享打开文件描述和进展假设的设计只是提案，Fs 没有实现它。仅关于该模型的定理不能建立 C API 允许的每种外部行为下的安全性。
C 字符串字面量使用运行时静态只读块。strerror 文本则使用 libcStr：它创建新的只读分配且不释放。这表示外部库存储，但精确的存活块结论必须计入这些分配，不能悄悄把它们算作 gzip 拥有的缓冲区，也不能假设它们不存在。
用于读取和格式化结果的 storeBytes 通过临时字节块复制，然后释放该块。其结果是块复制，而非一串字节存储。memchrB 在首个匹配字节处停止。内存操作仍检查对象边界、只读目标及相关重叠条件。无效用户缓冲区引发模型故障；这不是操作系统 EFAULT 行为的完整模型。
格式化输出
可变参数表示为 VaArg 中的值，包括有符号/无符号 32 位和 64 位整数及字节串指针。gzprintf 接收该列表并委托给 gzvprintf。不表示 C va_list 的 ABI 存储。
格式化器支持 %%、%c、%s、%d、%i、%u、%x、%X、%o，标志 -0+ #，十进制宽度和精度，以及长度修饰符 l、ll、z、j、t。不支持的转换包括浮点、%p、%n、%*d、%hd 和 %ls。不支持语法、参数类型不匹配或缺失都会故障。无符号转换也接受相应有符号参数类型，并重新解释其位。没有返回任意格式化字节的已实现后备行为。早期提案中的 h/hh、动态宽度和任意结果后备不能被理解为受支持行为。
对于模型中有效格式化，vsnprintf 最多写入 capacity - 1 个文本字节再加 NUL，并像所选 C99 路径一样返回未截断长度。长度大于 INT_MAX 的结果在模型中故障。gzip 包装仍执行自己的长度与哨兵检查，再执行自己的缓冲区腾空和错误处理。格式化模型不是可用来替代这些效果的被调用者契约。公开表示限制见偏离与限制。
指针与局部存储选择
GzFilePtr 标识其所有者的 x 前缀；castState 恢复所有者。strmOf 标识内嵌流。字段写入加载并更新同一个记录。这为编解码器反向指针和共享公开字段保留对象身份。
调用者标量指针，例如 gzerror 的可选 int *errnum 和 uncompress2 的长度输出，表示为小端字节块，使用四字节或八字节读写访问。gz_load 内部的 unsigned *have 则变成返回值，由每个调用者在成功和失败时存储。C 被调用者不会通过另一个别名观察该目标；对应证明还需要逐调用点建立相同的效果顺序。
被取地址的局部字节、局部流和标量输出存储使用不消耗调用者分配失败预言机的局部分配器。每个返回路径都必须释放它们。这适用于 gzgetc/gzputc 的单字节缓冲区，以及便利解压接口的局部流和长度单元。有符号文件位置算术使用经过检查的 64 位操作。模型允许空指针加零，并不能证明使用悬空指针有定义。
翻译文件保留了源码中缺失的 x.next 初始化、部分读取赋值顺序、直接缓冲区指针保留和 seek 算术。历史报告和修复提案在 gzip 证明指南中分开记录。这里没有应用 gzip 补丁。
差分证据
gzip 差分用例定义于 tests/gen/gz.py、tests/c/gz.c 和 tests/lean/Driver/Gz.lean。它们将临时真实文件上的操作观察与 Fs 上的运行比较。同一测试类别也比较 uncompress2 的字节和长度。
一致性检查将翻译和外部模型一起对照选定 C 执行。它提供忠实性证据，不是编解码器正确性、所有错误路径、所有 POSIX 行为或无泄漏性的证明。受限文件模型无法生成 gzip 证明指南中的部分成功后读取失败反例。运行结果和验收要求统一放在检查与进度，这里不另设测试历史清单。