inflate

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 inflate(z_streamp strm, int flush);

Consume compressed bytes and write decoded bytes, preserving state across calls.

Domain Restricted domain: live streams with common buffer/header lifetimes; arbitrary compressed bytes, input/output splits and signed flush values.

Effects Mutates stream, output and registered header storage; may allocate the history window.

Pre next_in describes avail_in readable bytes and may be NULL only when that count is zero. next_out is non-NULL even for zero avail_out, and describes that many writable bytes. A registered header and its buffers remain writable. Calls may continue with more input/room, supply a requested dictionary, or follow successful reset/recovery. Terminal/error repeats have the behavior below.

Post Reads/writes within the stated ranges. Advances pointers and reduces available counts by bytes consumed/produced. In an ordinary run from init/reset, with a valid selected format and the correct dictionary, accumulated output is a prefix of the decoded data and equals it at Z_STREAM_END. Malformed bytes are part of the domain: detected format or enabled checksum/length failures return Z_DATA_ERROR, possibly after output. Incomplete input alone needs more input; it need not be reported as a data error.

Accounting Normal returns, including data and buffer errors, update totals by consumed/produced bytes and update the enabled output checksum. Z_NEED_DICT accounts for consumed header bytes and leaves adler as the dictionary identifier. A late window-allocation failure can follow input consumption and output writes: pointers/counts already reflect them, but normal final total/checksum/data_type accounting is skipped. Do not treat Z_MEM_ERROR as an unchanged-output result.

Edges Zero input or output room is allowed. Z_BLOCK stops at a header or block boundary; Z_TREES also stops after block descriptions. Z_FINISH changes an otherwise Z_OK result to Z_BUF_ERROR. Other signed flush values are accepted and behave like Z_NO_FLUSH. data_type on normal returns records unused bits, plus 64 for the last block, 128 at a header/block boundary, and 256 after a block header. Data and memory errors are sticky; completed streams repeat Z_STREAM_END.

Ownership New window storage belongs to the stream and remains available for reset/end, including after errors. A one-call Z_FINISH completion may need no window. Concatenated gzip members require reset between members. Error messages are borrowed static strings. Buffer and stream check refusals change nothing.

flowchart LR
    I["Init"] --> F["inflate"]
    F -->|"Z_NEED_DICT"| D["SetDictionary"] --> F
    F -->|"more room or input"| F
    F -->|"end or abandon"| E["End"]
    F -->|"data error"| R["Reset or Sync"] --> F

/-- `int inflate(z_streamp strm, int flush)`.
The domain is actual init/call history, not an arbitrary hand-built decoder state.
The selected LP64 platform scope explicitly requires every live represented
byte object to have at most PTRDIFF_MAX bytes (size < 2^63), including caller
storage from non-malloc origins. See docs/deviations.md.
Includes all signed flush arguments, progress, terminal/error modes, output bounds,
counter timing on late memory failure, caller frame and ownership of a new window.
The sequence target states format correctness across all input/output splits. -/
def Goal.inflate : Prop :=
  ∀ h r i z s flush,
    StreamReachable .inflate h r → Zlib.Inflate.Spec.Good h r i z s →
    ZlibF.PlatformMemory.ByteObjectsFit h →
    Zlib.Inflate.Spec.DefAlloc z → StreamBuffers h r → ActiveHeader h r →
    ∃ rc after z' s' used out,
      C.run (Zlib.Inflate.inflate (some r) flush) h = .ok (rc, after) ∧
      Zlib.Inflate.Spec.Good after r i z' s' ∧ StreamAccounting z z' used out.length ∧
      Bytes after z.next_out out.length out ∧
      (rc = Z_OK ∨ rc = Z_STREAM_END ∨ rc = Z_NEED_DICT ∨ rc = Z_STREAM_ERROR ∨
       rc = Z_DATA_ERROR ∨ rc = Z_MEM_ERROR ∨ rc = Z_BUF_ERROR) ∧
      (rc = Z_OK → (used ≠ 0 ∨ out ≠ []) ∧ flush ≠ Z_FINISH) ∧
      (rc = Z_STREAM_END → s'.mode = DONE) ∧
      (rc = Z_NEED_DICT → s'.mode = DICT) ∧
      (rc = Z_DATA_ERROR → s'.mode = BAD) ∧
      (rc = Z_MEM_ERROR → s'.mode = MEM ∧ z'.total_in = z.total_in ∧ z'.total_out = z.total_out) ∧
      (rc = Z_OK ∨ rc = Z_STREAM_END ∨ rc = Z_DATA_ERROR ∨ rc = Z_BUF_ERROR →
        z'.total_in = z.total_in + UInt64.ofNat used ∧
        z'.total_out = z.total_out + UInt64.ofNat out.length) ∧
      BufferFrame h after
        (fun b => StreamRoot r b ∨ InflateOwned i s b ∨ s.head = some (.tab b))
        (⟨z.next_out, out.length⟩ :: HeaderRegions h s.head) ∧
      LiveChange h after (fun b => InflateOwned i s' b ∧ ¬ h.live b) (fun _ => False)