deflateBound_z
Compute a size bound using the stream's current configuration and wrapper.
Full chapter and shared rules ↗39ab1ace4bbe0b0e · 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.
z_size_t ZEXPORT deflateBound_z(z_streamp strm, z_size_t sourceLen);
Compute a size bound using the stream's current configuration and wrapper.
Domain Restricted domain (live stream and readable retained header); every
z_size_t sourceLen is included. Effect: query.
Pre live stream and shared header conditions. For the output-capacity guarantee below, call after init and any dictionary/header setup, before compression. Keep configuration, header and dictionary fixed; use standard tuning and no inserted prime bits.
Post the heap is unchanged. The numerical target is the following mathematical value,
saturated at SIZE_MAX, where n = sourceLen and w is the full wrapper size:
- Window 15 and memory level 8:
n + floor(n/4096) + floor(n/16384) + floor(n/33554432) + 7 + w. - Otherwise, if window bits are at most hash bits and level is nonzero:
n + floor(n/8) + floor(n/256) + floor(n/512) + 4 + w. - Otherwise:
n + floor(n/32) + floor(n/128) + floor(n/2048) + 7 + w.
w is 0 for raw, 6 for zlib plus 4 when preset history is present, or 18 for gzip plus
its optional extra field (including two length bytes), terminated name/comment and header CRC.
Output capacity: separately from the numerical formula, for a representable adequate
buffer, when the input and output sizes fit avail_in and avail_out, supplying all
n bytes to one deflate(Z_FINISH) with at least the bound of output room must return
Z_STREAM_END. A clean schedule using only Z_NO_FLUSH before
Z_FINISH has the total-output bound. Other flush schedules can exceed it.
A saturated result is not a promise that an addressable buffer of that size exists.
Outside focused scope: NULL or a safely checkable invalid stream receives the larger of the fixed/stored formulas above, plus 18, with saturation. There is no error code. The public numerical goal still includes every readable gzip header length, including lengths outside the focused 16-bit extra-field range; this page does not remove that obligation.
Shared conditions and scope
API manual · Shared stream rules · Stream decompression
Use a z_stream compressor when input arrives in pieces, output space is limited, or you
need a chosen wrapper, dictionary or flush boundary. Initialize once, call deflate with
successive buffers, and end the stream even if compression is abandoned. For a single buffer,
see compress and compress2.
| Task | Entries |
|---|---|
| Start or reuse | Init, configured init, reset, reset retaining history |
| Supply metadata or history | Dictionary, read history, gzip header |
| Compress and size output | Deflate, bound, pending output, last flush bits |
| Adjust or branch | Parameters, tuning, priming, copy |
| Release storage | End |
These focused contracts follow the pinned deflate.c, applied patches and zlib.h in the
default LP64 Linux build. Source readings are to confirm by proof. They leave the broader
registered public goals unchanged. See contract conventions
for domain/effect labels and progress for proof status and remaining work.
Shared conventions
Each stated Pre requires termination without runtime faults and the stated Post. A call that retains a live stream preserves its representation invariant.
- Live stream: a writable
z_streamwith a compressor state established by successful init or copy, preserved by legal calls, and not ended. The caller does not alter its internal state or allocator fields. Calls on one stream are sequential. - Buffers: input covers
avail_inreadable bytes; output coversavail_outwritable bytes. They do not overlap each other, the stream or its owned state. A non-NULL scalar result points to a writable cell separate from other results and stream memory. These separation conditions are explicit focused assumptions; see safety.md. - Allocator: the default allocator/free pair is used, or both fields are NULL before init. Allocation may fail on any attempt. Custom allocator callbacks are outside this page's scope.
- Frame and ownership: calls change only their stream, its owned state and stated
output regions. Caller input is read-only. Caller buffers and header records remain caller-owned.
Only init and copy allocate; only their failure cleanup and
deflateEndfree memory. Other calls preserve the stream's allocation set. - Header lifetime: a retained gzip header and its optional fields remain readable and
unchanged while used. Non-NULL
nameandcommenthave a terminating zero;extracovers its stated length. Focused format contracts useextra_len <= 65535. - Checked refusals: except for init and bounds, a failed stream check returns
Z_STREAM_ERRORbefore normal operation, without writes.deflateCopyadditionally clears a non-NULL destination state. Query output cells are untouched on this refusal. - Restricted domain means these explicit memory, lifetime and call-order conditions, plus the entry's Pre. It does not mean every representable pointer or integer is accepted. Error summaries cover readable checked states, not arbitrary invalid addresses.
Formal contract
ZlibF.Spec.Public.Goal.deflateBound_z
Proof status: Not completed · Evidence and remaining work
/-- `z_size_t deflateBound_z(z_streamp strm, z_size_t sourceLen)`.
The mathematical bound includes the entire gzip header, with saturation instead of overflow.
The known extra-length arithmetic issue remains an implementation proof blocker. -/
def Goal.deflateBound_z : Prop := DeflateBoundContract Zlib.Deflate.deflateBound_z