gzread
Read up to len uncompressed bytes.
Full chapter and shared rules ↗2425ced89b926581 · Source at the matching commit ↗Read the function’s preconditions and results first. Expand the shared rules below for buffer and ownership requirements used throughout this API group.
int ZEXPORT gzread(gzFile file, voidp buf, unsigned len);
Read up to len uncompressed bytes.
Domain Restricted domain: reader and destination; full unsigned len refusal range.
Effect: stateful read, destination write and possible allocation.
Pre For len <= INT_MAX, buf covers len writable bytes under the
shared separation rules. A zero extent needs no accessed bytes.
Post A positive result n <= len gives the next n bytes and advances
the position by n, after any pending skip. Format, member concatenation,
transparent input and deferred errors follow the shared read rules.
Errors and edges: Returns -1 for NULL, wrong mode, an undeliverable hard
error or len > INT_MAX; oversized requests record Z_STREAM_ERROR unless
preserving a more serious error. No output at EOF/truncation returns zero.
A zero request normally returns zero, but existing error/stall state can still
cause -1. Consult gzerror; truncation is Z_BUF_ERROR, not a successful
complete gzip member. A later error does not erase delivered
bytes. Blocking descriptors may wait to fill internal reads. Non-blocking
stalls are retryable and are not EOF. Partial transparent-read recovery has a
known to confirm caveat below; no unconditional safety claim is made here.
Shared conditions and scope
API manual · Contract conventions · Stream compression · Stream decompression
Use a gzFile handle for buffered gzip file I/O. Open acquires a file descriptor and private
state; data operations initialize buffers and codec state as needed; close releases the
handle even if final I/O fails. Reading can also accept transparent, uncompressed input.
| Task | Entries |
|---|---|
| Open or configure | Open path, open descriptor, buffer size, compression parameters |
| Read | Bytes, items, character, pushback, line |
| Write | Bytes, items, character, string, formatted text, flush |
| Position | Seek, rewind, uncompressed position, file offset |
| Inspect or clear status | EOF, transparent mode, error, clear error |
| Close | Any mode, reader, writer |
These focused contracts follow the pinned source and zlib.h. Source readings are
to confirm by implementation proof. They do not assert full API verification or narrow
the broader registered public goals. See
progress for proof status and remaining work.
Common handle conditions
This page uses the default x86_64 Linux build. int and unsigned have
32 bits. long, z_off_t, z_off64_t and z_size_t have 64 bits.
The large-file declarations are enabled. Plain and *64 entry points have
the same offset range here. Other configurations need separate contracts.
gzopen_w is a Windows-only entry and is scoped separately below.
Restricted domain means ordinary use with these common requirements:
- A non-NULL handle is live, returned by a successful open, and not closed. It is used serially and its private state is not modified by the caller.
- A reader or writer has the access mode named by the entry. NULL and wrong-mode refusals are documented separately. A stale or arbitrary pointer is outside this domain; checking a mode field does not validate a pointer.
- Buffers cover the requested readable or writable extent. They are separate from handle-owned memory. Strings have a readable terminating NUL. The caller retains ownership of these objects.
- Position arithmetic and requested extents are representable in the stated C types. Explicit oversized-request and multiplication-overflow refusals remain part of the contracts below.
- The descriptor belongs to the handle until close. No other operation changes its data or position during a call. OS failures and allocation failures remain possible; a successful open does not guarantee that later I/O succeeds.
Every entry carries a domain label. “Full scalar range” applies only to the named scalar argument, under these pointer and lifetime requirements. Documentary restrictions do not excuse known failure paths. In particular, partial-read errors and pushback-created negative positions remain obligations of the unchanged public goals.
Effects. Read, write, open, seek, control and close operations are stateful,
including operations without a caller output buffer. Tell, offset and EOF
queries read state; gzerror may also write its optional code output.
gzdirect can read the file and allocate, so it is stateful.
stateDiagram-v2
[*] --> Fresh: successful open
Fresh --> Active: first I/O or format inspection
Active --> Active: read, write, seek, control
Fresh --> Closed: close
Active --> Closed: close, including final I/O failure
Closed --> [*]
Format and buffering. Opening does no payload I/O. Buffers and codec state are allocated lazily, with a default requested buffer size of 8192 bytes. Allocation can fail at first use or later in decompression. Closing releases owned allocations even when final I/O fails.
An ordinary reader detects gzip from a plausible four-byte header; otherwise
it returns the input unchanged. Empty input is transparent. Detection waits
when non-blocking input stalls before four bytes are available. Gzip members
are concatenated in the output. Trailing non-member data is ignored when the
attempted following member produces no output before its format error.
G requires gzip; T selects transparent output and is invalid for reading.
Read results. Reads advance the uncompressed position by bytes consumed,
including a final partial item. Buffered bytes can be returned before a
recorded error is reported. gzeof reports an attempted read beyond available
data, not simply the delivery of the final byte. gzerror distinguishes EOF,
corruption (Z_DATA_ERROR), truncation (Z_BUF_ERROR), allocation failure
(Z_MEM_ERROR) and system failure (Z_ERRNO). Zero-length reads do not consume
input or carry out a pending seek.
Write results. Success means input was accepted by the handle. It can still be buffered. Flush or close can fail later. A hard error can return failure after consuming a prefix; the return value alone is not always a retry offset. A non-blocking stall can instead return the number consumed so far.
Errors normally persist until cleared. A recorded would-block condition permits
the next data I/O call to retry. Seek and rewind still refuse that recorded
Z_ERRNO. Constructing an error message can itself fail and replace the code
with Z_MEM_ERROR. errno is meaningful for the associated system failure,
not as a general explanation of every failed API call.
The source is gzlib.c,
gzread.c, gzwrite.c,
gzclose.c and zlib.h.
The abstract contracts are in Api/Gz.lean.
Concrete goals are in GzOpen,
GzRead,
GzWrite,
GzControl and
GzClose.
The translations mirror the C names in ZlibF/Zlib/.
Formal contract
ZlibF.Spec.Public.Goal.gzread
Proof status: Not completed · Evidence and remaining work
/-- `int gzread(gzFile file, voidp buf, unsigned len)`.
Return bytes, EOF zero, or -1. Requests above INT_MAX fail before touching the output.
Buffered bytes precede a later error; partial output remains part of the result. -/
def Goal.gzread : Prop :=
(∀ h fs p n, Zlib.Gzread.gzread none p n fs h = .ok ((-1, fs), h)) ∧
(∀ h fs i s p n, GzReachable h fs i → GzValid h i s →
(n.toNat < 2 ^ 31 → GzRange h i s p n.toNat true) →
∃ rc fs' after s' out,
Zlib.Gzread.gzread (some (.in_gzstate_x i)) p n fs h = .ok ((rc, fs'), after) ∧
ReturnedBytes after p out ∧
ReadEffect h after fs fs' i s s' (if n.toNat < 2 ^ 31 then n.toNat else 0) out [⟨p, out.length⟩] ∧
(rc = -1 ∧ out = [] ∨ 0 ≤ rc.toInt ∧ rc.toInt = (out.length : Int)) ∧
(2 ^ 31 ≤ n.toNat → rc = -1) ∧
(s.mode ≠ GZ_READ → rc = -1 ∧ after = h ∧ fs' = fs))