inflateBackInit_
Purpose. Allocate decoder state and attach the caller's window. The inflateBackInit macro supplies version and stream_size.
Full chapter and shared rules ↗c361e306c50783f5 · 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 inflateBackInit_(z_streamp strm, int windowBits, unsigned char FAR *window,
const char *version, int stream_size);
Purpose. Allocate decoder state and attach the caller's window.
The inflateBackInit macro supplies version and stream_size.
Domain Restricted domain: valid caller memory, an inactive stream and default allocation.
Pre A non-NULL strm points to a writable z_stream with initialized zalloc, zfree
and opaque. Use NULL or the default allocator/free pair; do not overwrite live library state.
A non-NULL version has a readable first byte. On the initialization path, window provides
2^windowBits writable bytes separate from the stream. Keep that slice alive until end.
Effects May initialize allocator fields and opaque, clear msg and allocate one state.
The window remains caller-owned and is not allocated, cleared or freed here.
Post Z_OK attaches fresh state for inflateBack with 8 <= windowBits <= 15.
Input/output pointers, availability counters, totals, adler and data_type are unchanged.
Only selected state fields are initialized; use this state with the callback API.
Errors A NULL version, different major-version byte or wrong stream size gives
Z_VERSION_ERROR before stream access. NULL strm/window, or bits outside 8..15, gives
Z_STREAM_ERROR. Allocation failure gives Z_MEM_ERROR: msg and allocator defaults may
have changed, but the old state field is retained. No state was allocated, so no end call
is needed after failed init in this inactive-stream domain.
Shared conditions and scope
API manual · Shared stream rules · Stream decompression
The callback interface lets a caller supply input chunks and receive decoded output directly from its window. Start with inflateBackInit_, decode with inflateBack, and release state with inflateBackEnd. The caller's window remains caller-owned throughout.
These focused contracts follow the pinned infback.c and zlib.h in the default LP64 Linux build. Source readings are to confirm by proof. Their restricted domains do not narrow the broader targets in Back.lean or Sequences.lean. See contract conventions for domain/effect labels and progress for proof status and remaining work.
inflateBack decodes raw DEFLATE. The caller handles any zlib/gzip header, trailer and checksum.
The caller owns a writable window of at least 2^windowBits bytes. It is also the output buffer.
Use 15 bits and 32768 bytes for general streams; smaller windows can reject valid long distances.
flowchart LR
I["inflateBackInit_: allocate state"] --> B["inflateBack: decode one stream"]
B -->|another stream| B
B -->|success or decode error| E["inflateBackEnd: free state"]
I -->|no decode needed| E
The callbacks have these types:
typedef unsigned (*in_func)(void FAR *, z_const unsigned char FAR * FAR *);
typedef int (*out_func)(void FAR *, unsigned char FAR *, unsigned);
in(in_desc, &buf) returns a byte count and sets buf; zero means no input and ignores buf.
out(out_desc, buf, len) receives up to one window of bytes; zero means success.
Descriptors may be NULL if the callback supports that value.
Formal contract
ZlibF.Spec.Public.Goal.inflateBackInit_
Proof status: Registered proof · Evidence and remaining work
/-- `int inflateBackInit_(z_streamp strm, int windowBits, unsigned char *window,
const char *version, int stream_size)`.
The caller retains the window. Only the state record is allocated; its other integer fields
remain arbitrary. Refusal precedes allocation, and allocation failure retains the old state field. -/
def Goal.inflateBackInit_ : Prop :=
(∀ h p wb window version head size, VersionValue h version head →
(head ≠ some 49 ∨ size ≠ 112) →
C.run (Zlib.Infback.inflateBackInit_ p wb window version size) h = .ok (Z_VERSION_ERROR, h)) ∧
(∀ h p wb window version, VersionValue h version (some 49) →
(p = none ∨ window = .null ∨ wb.toInt < 8 ∨ 15 < wb.toInt) →
C.run (Zlib.Infback.inflateBackInit_ p wb window version 112) h = .ok (Z_STREAM_ERROR, h)) ∧
(∀ h r z wb window version,
Fresh h → Zlib.Inflate.Spec.Uniq h → LibraryGlobals h → r.get h = some z →
DefaultOrNull z → VersionValue h version (some 49) →
8 ≤ wb.toInt → wb.toInt ≤ 15 → window ≠ .null → Writable h window (2 ^ wb.toInt.toNat) →
∃ rc after,
C.run (Zlib.Infback.inflateBackInit_ (some r) wb window version 112) h = .ok (rc, after) ∧
after.nalloc = h.nalloc + 1 ∧
if h.allocOk h.nalloc = false then
rc = Z_MEM_ERROR ∧ SameObjects (r.put h (preparedStream z)) after
else rc = Z_OK ∧
let z' := { preparedStream z with state := some (.inflate h.nextBlk) }
let s := backInitialState (h.garbage h.nalloc) window wb
BackValid after r h.nextBlk z' s ∧
Frame h after (StreamRoot r) ∧
LiveChange h after (fun b => b = h.nextBlk) (fun _ => False))