deflateInit2_
Start a compressor with a chosen wrapper and compression settings.
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.
int ZEXPORT deflateInit2_(z_streamp strm, int level, int method, int windowBits,
int memLevel, int strategy, const char *version, int stream_size);
Start a compressor with a chosen wrapper and compression settings.
Domain Restricted domain. Effect: allocate and initialise.
Pre the stream and version conditions of deflateInit_ hold. Parameters are:
level -1 or 0..9; method == Z_DEFLATED; memLevel 1..9; strategy 0..4;
windowBits 8..15 for zlib, -15..-9 for raw, or 25..31 for gzip.
Post Z_OK establishes a live stream with five owned allocations and the selected
settings. A zlib window request of 8 becomes 9. Totals are zero, msg is NULL,
data_type is Z_UNKNOWN, and adler is 1 for raw/zlib or 0 for gzip.
I/O pointers and available counts are unchanged; no bytes are consumed or emitted.
The caller releases the state with deflateEnd.
Z_MEM_ERROR leaves no newly allocated block live. If the state allocation fails,
state retains its entry value. If a later allocation fails, state becomes NULL and
msg reports insufficient memory. Once the state allocation succeeds, all four buffer
allocations are attempted before failure cleanup.
Outside focused scope: a NULL/mismatched version first byte or wrong structure size
returns Z_VERSION_ERROR without changing the stream. With compatible version and NULL
strm, return Z_STREAM_ERROR. Other scalar parameters outside the accepted ranges
return Z_STREAM_ERROR before allocation, after clearing msg and installing default
allocator fields where needed. Installing the default allocator clears opaque.
These refusals are required by the unchanged public init goals.
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.deflateInit2_
Proof status: Not completed · Evidence and remaining work
/-- `int deflateInit2_(z_streamp strm, int level, int method, int windowBits, int memLevel,
int strategy, const char *version, int stream_size)`.
Every signed argument, source-ordered refusal, five allocations, failure cleanup and success invariant. -/
def Goal.deflateInit2_ : Prop :=
∀ level method wb mem strategy,
DeflateInitContract (fun p v size => Zlib.Deflate.deflateInit2_ p level method wb mem strategy v size)
level method wb mem strategy