inflateBack

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 inflateBack(z_streamp strm, in_func in, void FAR *in_desc,
                        out_func out, void FAR *out_desc);

Purpose. Decode one complete raw stream through the input and output callbacks.

Domain Restricted domain: a live callback decoder, valid separated slices and a finite, returning callback protocol. Arbitrary malformed input bytes are included.

Pre Init succeeded and end has not run. Keep the stream, state and window live. Initialize next_in; NULL requests callback input immediately and ignores avail_in. Otherwise initialize avail_in and provide that many readable bytes at next_in. Initial and callback-provided input slices do not overlap the window, stream or private state. Neither callback is NULL. Every callback returns safely and the total input supplied is bounded.

Callbacks may read only the input/output bytes supplied to them and their own valid objects. They may update, allocate or free their own memory, but preserve the stream, private state and window slice. An input chunk remains readable and unchanged until the next input callback or return, including across output callbacks. Output callbacks read at most len window bytes. Callback storage and the window may share an allocation when their used byte slices do not overlap. No concurrent or re-entrant access to this stream is allowed.

Effects Reset decoding for a new stream, consume input, write the window and invoke callbacks. Full windows and a final nonempty partial window are delivered to out, including on error. Callbacks may therefore observe output before a later format or input failure. The library allocates and frees nothing; callback allocations remain the caller's responsibility.

Post Z_STREAM_END means the complete raw stream was decoded and every output call succeeded. The concatenated chunks are its uncompressed bytes, with no preset dictionary. next_in/avail_in identify the unread suffix of the initial or last callback chunk. After input exhaustion they are NULL/zero; otherwise the pointer advances by the consumed bytes. Totals, adler and data_type are unchanged; next_out/avail_out are not the output interface. The stream retains its state and window for another independent decode or end.

Errors Z_BUF_ERROR means input exhaustion or a nonzero output result; it never returns Z_OK. For Z_BUF_ERROR, NULL next_in identifies input exhaustion; non-NULL identifies output failure. Z_DATA_ERROR means malformed DEFLATE and sets msg. A final output failure changes Z_STREAM_END to Z_BUF_ERROR; it does not replace another error already selected. NULL strm or NULL state gives Z_STREAM_ERROR without callbacks. Other invalid states are outside this domain: a state from ordinary inflateInit_ is not a callback decoder. After a decode error, end still releases the state; another call starts a fresh stream.

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

typedef unsigned (*in_func)(void FAR *, z_const unsigned char FAR * FAR *);
typedef int (*out_func)(void FAR *, unsigned char FAR *, unsigned);

/-- `int inflateBack(z_streamp strm, in_func in, void *in_desc, out_func out, void *out_desc)`.
For every finite, returning caller protocol, decode raw DEFLATE and deliver the chunks through
that actual output callback. The protocol's observation relation records the bytes delivered.
No allocation or free by the library is charged to the caller's callbacks. -/
def Goal.inflateBack : Prop :=
  (∀ h input inDesc output outDesc,
    C.run (Zlib.Infback.inflateBack none input inDesc output outDesc) h = .ok (Z_STREAM_ERROR, h)) ∧
  (∀ h r i z s input inDesc output outDesc
      (protocol : CallbackProtocol r i s.window s.wsize.toNat input inDesc output outDesc) first,
    BackValid h r i z s →
    (if z.next_in = .null then first = [] else Bytes h z.next_in z.avail_in.toNat first) →
    Separate z.next_in first.length s.window s.wsize.toNat →
    protocol.invariant h { supplied := first, chunks := [], active := z.next_in, held := first } →
    ∃ rc after z' s' log unused consumed,
      C.run (Zlib.Infback.inflateBack (some r) input inDesc output outDesc) h = .ok (rc, after) ∧
      BackValid after r i z' s' ∧ s'.window = s.window ∧ s'.wsize = s.wsize ∧
      protocol.invariant after log ∧
      (rc = Z_STREAM_END ∨ rc = Z_DATA_ERROR ∨ rc = Z_BUF_ERROR) ∧
      consumed ++ unused = log.supplied ∧ unused.length = z'.avail_in.toNat ∧
      unused <:+ log.held ∧
      (log.exhausted = true → z'.next_in = .null ∧ unused = []) ∧
      (log.exhausted = false → z'.next_in = advance log.active (log.held.length - unused.length)) ∧
      (∀ chunk, chunk ∈ log.chunks → chunk ≠ [] ∧ chunk.length ≤ s.wsize.toNat) ∧
      (rc = Z_STREAM_END → Deflate.Decodes [] consumed log.chunks.flatten ∧ log.failed = false) ∧
      (rc = Z_BUF_ERROR → log.exhausted = true ∨ log.failed = true) ∧
      z'.total_in = z.total_in ∧ z'.total_out = z.total_out ∧ z'.adler = z.adler ∧
      CallbackFrame protocol.own h after r i s.window s.wsize.toNat ∧
      (∀ b, ¬ protocol.own b → (after.live b ↔ h.live b)))