gzgets
读取一个行片段，并以 NUL 结尾。
完整章节与共同规则 ↗2425ced89b926581 · 对应提交的原文 ↗先看本函数的前置条件和返回结果；可展开下方共同规则，查看整组接口的缓冲区与所有权要求。
读取一个行片段，并以 NUL 结尾。
char * ZEXPORT gzgets(gzFile file, char *buf, int len);
定义域 受限定义域：读取句柄／目标；完整 int len 拒绝范围。
效果： 有状态读取和目标写入。
前置条件 buf 非 NULL 且 len > 0 时，目标按共享分离规则覆盖 len 个可写字节。
返回与保证 返回 buf，其中最多含 len - 1 个数据字节及一个终止 NUL。
在首个换行符后停止（包括该换行符），或在达到限制／EOF 时停止。
已消费数据推进位置。输入中的内嵌 NUL 也作为数据复制。
错误与边缘情形： NULL 句柄／缓冲区、模式错误或 len < 1 返回 NULL。
更大长度下，无字节的 EOF 或无法交付数据的错误返回 NULL；
已交付前缀仍可能返回，同时记录错误。
len == 1 时，其他条件可接受的调用不向 buf 复制输入字节，并返回空字符串，
即使已在 EOF。先执行待处理跳过：它可能消费输入、解压、分配、推进位置，
或失败并返回 NULL。适用共享的延迟错误和部分读取注意事项。
本组共同前提与范围
使用 gzFile 句柄进行带缓冲的 gzip 文件 I/O。打开时取得文件描述符和私有状态；
数据操作按需初始化缓冲区和编解码器状态；即使最终 I/O 失败，关闭也会释放句柄。
读取还可接受透明的未压缩输入：文件中的字节不经解压，直接作为结果交付。
| 任务 | 入口 |
|---|---|
| 打开或配置 | 打开路径、打开描述符、缓冲区大小、压缩参数 |
| 读取 | 字节、数据项、字符、回退字节、行 |
| 写入 | 字节、数据项、字符、字符串、格式化文本、刷新 |
| 位置 | 定位、回到起点、未压缩位置、文件偏移 |
| 查询或清除状态 | 文件末尾、透明模式、错误、清除错误 |
| 关闭 | 任意模式、读取句柄、写入句柄 |
本页按固定版本源码和 zlib.h 组织接口契约。各条目明确列出调用范围，
对应的完整执行要求见已登记公开目标，当前证据见进度。
超出聚焦前提只表示本契约不作保证，不自动等于 C 未定义行为（UB），也不保证一定返回错误码。
通用句柄条件
先分清两种位置。逻辑位置以未压缩字节计数；普通读写按已消费或接受的数量推进，定位还可以登记尚未执行的前移。底层文件另有物理偏移，它以文件中的字节计数。gztell 查询前者，gzoffset 查询后者。库会预读和缓冲，因此两个值通常不同；单次压缩率也不能用来换算它们。
例如，没有额外定位或字节回退时，读取句柄已向应用交付 1000 个解压字节，逻辑位置就是 1000；为了完成这些输出，底层可能已预读更靠后的压缩字节。相反，写入成功表示库接受了输入，不能据此推断这些字节已全部写入描述符。
后面的参数沿用这套单位：len 和缓冲区配置 size 按字节计；数据项接口中的 size 是每项字节数，nitems 是项数，总请求为 size * nitems 字节。offset 是有符号的未压缩字节位移；whence 指定从起点（SEEK_SET）还是当前位置（SEEK_CUR）计算。INT_MAX 是本构建中有符号 int 能表示的最大值，即 2^31 - 1。
本页把可直接重试的非阻塞停顿与其他已记录的“硬错误”分开描述。这个区别说明本次调用怎样返回；它不免除错误后的状态、重试和清理要求。
本页使用默认 x86_64 Linux 构建。int 和 unsigned 为 32 位。
long、z_off_t、z_off64_t 和 z_size_t 为 64 位。大文件声明已启用。
这里普通入口和 *64 入口的偏移范围相同。其他配置需要单独契约。
gzopen_w 仅适用于 Windows，下文另行限定其范围。
受限定义域指满足下列通用要求的普通用法：
- 非 NULL 句柄由成功打开返回、仍存活且尚未关闭。串行使用它，调用者不修改其私有状态。
- 读取或写入句柄具有入口指定的访问模式。NULL 和错误模式的拒绝情形分别说明。 已失效或任意指针不在本定义域内；检查模式字段不等于验证指针。
- 缓冲区覆盖请求的可读或可写范围，并与句柄拥有的内存分离。 字符串具有可读的终止 NUL。调用者保留这些对象的所有权。
- 位置运算和请求范围能由指定 C 类型表示。下述契约仍包括显式的超大请求和乘法溢出拒绝。
- 描述符在关闭前属于句柄。调用期间，没有其他操作改变其数据或位置。 操作系统失败和分配失败仍可能发生；成功打开不保证后续 I/O 成功。
每个入口均带定义域标签。“完整标量范围”仅在上述指针和生存期要求下， 适用于所指明的标量参数。文档中的限制不免除已知失败路径的义务。 特别地，部分读取错误和字节回退形成的负位置仍属于未改变的公开目标。
效果。 读、写、打开、定位、控制和关闭均为有状态操作，包括没有调用者输出缓冲区的操作。
位置查询（gztell、gzoffset）和文件末尾查询（gzeof）读取状态；gzerror 还可能写入可选错误码输出。
gzdirect 可读取文件并分配内存，因此也是有状态操作。
stateDiagram-v2
state "新建句柄" as Fresh
state "已开始数据处理" as Active
state "已关闭" as Closed
[*] --> Fresh: 成功打开
Fresh --> Active: 首次 I/O 或格式检查
Active --> Active: 读、写、定位、控制
Fresh --> Closed: 关闭
Active --> Closed: 关闭，包括最终 I/O 失败
Closed --> [*]
格式与缓冲。 打开时不对载荷执行 I/O。缓冲区和编解码器状态按需分配， 默认请求的缓冲区大小为 8192 字节。请求大小是配置量，实际内部存储还包括下述双倍缓冲区和编解码器状态。首次使用或后续解压期间都可能分配失败。 即使最终 I/O 失败，关闭也释放拥有的分配。
普通读取句柄根据合理的四字节头部识别 gzip；否则原样返回输入。
空输入属于透明输入。非阻塞输入在获得四字节前停顿时，检测保持等待。
一个 gzip 成员是一段带有自身头部、压缩数据和尾部校验信息的完整流；一个文件可以顺序放置多个成员。读取输出按顺序拼接各成员的未压缩数据。若尝试解码下一个成员时，在格式错误前未产生输出，
则忽略尾随的非成员数据。G 要求 gzip；T 选择透明输出，不能用于读取。
读取结果。 读取按已消费字节数推进未压缩位置，包括最终的部分数据项。
已缓冲字节可能在已记录错误被报告之前返回。gzeof 表示曾尝试读取可用数据之后的内容，
而不只是已交付最后一个字节。gzerror 区分 EOF、损坏（Z_DATA_ERROR）、
截断（Z_BUF_ERROR）、分配失败（Z_MEM_ERROR）和系统失败（Z_ERRNO）。
零长度读取不消费输入，也不执行待处理定位。
写入结果。 成功表示句柄已接受输入；数据仍可能在缓冲区内。 后续刷新或关闭仍可能失败。硬错误可能在消费一个前缀后返回失败； 仅凭返回值不总能确定重试偏移。非阻塞停顿则可能返回至今已消费的数量。
错误通常持续到被清除。已记录的非阻塞停顿允许下次数据 I/O 重试。
定位和回到起点仍拒绝该已记录的 Z_ERRNO。构造错误消息本身可能失败，
并将错误码改为 Z_MEM_ERROR。errno 只对关联的系统失败有意义，
不能普遍解释每个失败的 API 调用。
源码为 gzlib.c、gzread.c、
gzwrite.c、gzclose.c 和
zlib.h。抽象契约位于 Api/Gz.lean。
具体目标位于 GzOpen、
GzRead、GzWrite、
GzControl 和
GzClose。翻译在 ZlibF/Zlib/ 中保留 C 名称。
形式化约定
ZlibF.Spec.Public.Goal.gzgets
证明状态：未完成 · 证明记录与剩余工作
/-- `char *gzgets(gzFile file, char *buf, int len)`.
Copy at most len-1 bytes, stopping after the first newline, and append a NUL on success.
Length one succeeds with an empty string; an EOF with no bytes returns null for larger lengths. -/
def Goal.gzgets : Prop :=
(∀ h fs p n, Zlib.Gzread.gzgets none p n fs h = .ok ((.null, fs), h)) ∧
(∀ h fs i s p n, GzReachable h fs i → GzValid h i s →
(0 < n.toInt → p ≠ .null → GzRange h i s p n.toInt.toNat true) →
∃ result fs' after s' out,
Zlib.Gzread.gzgets (some (.in_gzstate_x i)) p n fs h = .ok ((result, fs'), after) ∧
GzStateFrame h after fs fs' i s s' [⟨p, if result = .null then out.length else out.length + 1⟩] ∧
out.length ≤ n.toInt.toNat - 1 ∧
(result = .null → out = []) ∧
(result = .null ∨ result = p ∧ Bytes after p (out.length + 1) (out ++ [0])) ∧
(∀ left right, out = left ++ 10 :: right → right = []) ∧
(p = .null ∨ n.toInt < 1 ∨ s.mode ≠ GZ_READ → result = .null ∧ after = h ∧ fs' = fs) ∧
(∀ decoded buffered, FileData fs s decoded → Buffered h s buffered →
out <+: availableRead s buffered decoded ∧
(NoAllocationFailure h → s.mode = GZ_READ → p ≠ .null → 0 < n.toInt →
s.err = Z_OK ∨ s.err = Z_BUF_ERROR →
let line := ((availableRead s buffered decoded).takeWhile (fun b => b != 10))
let full := if line.length < (availableRead s buffered decoded).length then line ++ [10] else line
out = full.take (n.toInt.toNat - 1) ∧
(n = 1 ∨ full ≠ [] → result = p))))