inflateBackEnd
Purpose. Release the state allocated by callback init.
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 inflateBackEnd(z_streamp strm);
Purpose. Release the state allocated by callback init.
Domain Restricted domain: a live callback decoder with valid default free, plus the checked NULL-stream, NULL-state and NULL-free refusal cases.
Pre For cleanup, init succeeded, end has not run and no decode or callback is active.
The stream and attached state remain valid; retain the matching zfree and opaque.
Cleanup is permitted after successful decoding and after any decode error.
Effects Free exactly the internal state and clear state.
Post Z_OK leaves state NULL. The caller's window and all other stream fields are unchanged.
The caller may now release or reuse its window; the library never frees it.
Errors NULL strm, NULL state or NULL zfree gives Z_STREAM_ERROR and frees nothing.
These checks do not validate an arbitrary non-NULL state or detect ownership mistakes.
Back to the API manual · Contract conventions
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.inflateBackEnd
Proof status: Registered proof · Evidence and remaining work
/-- `int inflateBackEnd(z_streamp strm)`.
Free only the state record. The caller's window is retained, even when it is a slice of another object. -/
def Goal.inflateBackEnd : Prop :=
(∀ h, C.run (Zlib.Infback.inflateBackEnd none) h = .ok (Z_STREAM_ERROR, h)) ∧
(∀ h r z, r.get h = some z → z.state = none ∨ z.zfree = .null →
C.run (Zlib.Infback.inflateBackEnd (some r)) h = .ok (Z_STREAM_ERROR, h)) ∧
(∀ h r i z s, BackValid h r i z s →
∃ after, C.run (Zlib.Infback.inflateBackEnd (some r)) h = .ok (Z_OK, after) ∧
r.get after = some { z with state := none } ∧
LiveChange h after (fun _ => False) (fun b => b = i) ∧
Frame h after (fun b => StreamRoot r b ∨ b = i) ∧
after.nalloc = h.nalloc ∧ after.nextBlk = h.nextBlk)