deflateInit_
Start a compressor with the default zlib 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 deflateInit_(z_streamp strm, int level, const char *version, int stream_size);
Start a compressor with the default zlib wrapper and compression settings.
Domain Restricted domain. Effect: allocate and initialise.
Pre strm is writable and owns no live compressor state. Its allocator fields are
initialised as above. level is -1 or 0..9. version has a readable first byte matching
ZLIB_VERSION, and stream_size == sizeof(z_stream).
Post the deflateInit2_ contract holds with method Z_DEFLATED, window 15,
memLevel 8 and Z_DEFAULT_STRATEGY. Level -1 selects 6. No input is consumed and
no output is written. Return Z_OK on success or Z_MEM_ERROR with complete cleanup.
Outside focused scope: the same version and argument refusals as deflateInit2_ apply.
The deflateInit macro supplies version and structure size.
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.deflateInit_
Proof status: Registered proof · Evidence and remaining work
/-- `int deflateInit_(z_streamp strm, int level, const char *version, int stream_size)`.
The default method, window, memory level and strategy; the level remains arbitrary. -/
def Goal.deflateInit_ : Prop :=
∀ level, DeflateInitContract (fun p v size => Zlib.Deflate.deflateInit_ p level v size)
level 8 15 8 0