deflate

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

Accept input and deliver part or all of a valid compressed stream.

Domain Restricted domain. Effect: consume input, emit output and update progress.

Pre live stream with valid buffers and any active header. next_out is non-NULL and avail_out > 0; next_in may be NULL only with zero input. flush is Z_NO_FLUSH, Z_PARTIAL_FLUSH, Z_SYNC_FLUSH, Z_FULL_FLUSH, Z_FINISH or Z_BLOCK. If output fills during a flush, continue with the same flush and more room. After finishing begins, supply no new input and continue only with Z_FINISH. For ordinary format validity, begin from init/deflateReset (or a copy of that history), use legal dictionary/header setup, standard tuning and no arbitrary priming.

Post accept used <= old avail_in bytes and deliver made <= old avail_out bytes. Pointers advance by those amounts, available counts fall by them, and totals increase by them with unsigned wrapping. Input stays unchanged; output outside the delivered prefix stays unchanged. Some input can remain when output fills. No allocation or free occurs.

Across calls, delivered bytes form a prefix of a valid encoding of accepted input, using the chosen wrapper, settings and preset dictionary. Completed output decodes to that input. This specifies valid output, not one unique compressed byte sequence. adler tracks accepted input using Adler-32 for zlib and CRC-32 for gzip after header emission; raw has no input checksum.

Z_OK means continuation may be needed. Z_STREAM_END occurs only with Z_FINISH, after all supplied input and all compressed output, including trailer, have been delivered. The live state remains owned until deflateEnd or reusable via deflateReset.

When a requested flush is fully delivered, Z_BLOCK completes a block without byte padding; Z_PARTIAL_FLUSH adds an empty fixed block; Z_SYNC_FLUSH makes all preceding input available to a decoder and ends with an aligned empty stored block. Z_FULL_FLUSH also resets match history: later blocks do not refer before that completed flush. Restarting a raw decoder there requires retaining the exact boundary and delivering the entire flush marker first. Z_FINISH closes the final block and writes the wrapper trailer.

Errors Z_BUF_ERROR covers zero output room, no possible progress with no input and no stronger flush, or input offered after final-block processing began. It preserves a live stream; provide room/input as appropriate. Z_STREAM_ERROR covers the stream check, invalid flush (including Z_TREES), invalid NULL I/O combinations, or non-finish flush after finishing began. Initial argument refusals consume no input or output. A later Z_BUF_ERROR for new input after finishing may first deliver old pending output; no new input is accepted. msg and remembered flush can change. The unchanged public goal includes all signed flush values and these refusals.

/-- `int deflate(z_streamp strm, int flush)`.
Preserve the live stream and its five allocations. Account for exactly the bytes accepted
and delivered, including progress on a full output buffer and clean parameter refusals.
The sequence target states valid encoding, flush semantics and completion. -/
def Goal.deflate : Prop :=
  ∀ h r i z s flush,
    StreamReachable .deflate h r → Zlib.Deflate.Spec.DGood h r i z s →
    StreamBuffers h r → ActiveHeader h r →
    ∃ rc after z' s' used out,
      C.run (Zlib.Deflate.deflate (some r) flush) h = .ok (rc, after) ∧
      Zlib.Deflate.Spec.DGood after r i z' s' ∧ StreamAccounting z z' used out.length ∧
      Bytes after z.next_out out.length out ∧
      z'.total_in = z.total_in + UInt64.ofNat used ∧
      z'.total_out = z.total_out + UInt64.ofNat out.length ∧
      (rc = Z_OK ∨ rc = Z_STREAM_END ∨ rc = Z_STREAM_ERROR ∨ rc = Z_BUF_ERROR) ∧
      (rc = Z_STREAM_ERROR ↔
        flush.toInt < 0 ∨ 5 < flush.toInt ∨ z.next_out = .null ∨
        (z.next_in = .null ∧ z.avail_in ≠ 0) ∨
        (s.status = FINISH_STATE ∧ flush ≠ Z_FINISH)) ∧
      (flush.toInt < 0 ∨ 5 < flush.toInt → rc = Z_STREAM_ERROR ∧ after = h) ∧
      (rc = Z_STREAM_END → flush = Z_FINISH ∧ s'.status = FINISH_STATE ∧
        z'.avail_in = 0 ∧ s'.pending = 0 ∧ s'.bi_valid = 0) ∧
      BufferFrame h after (fun b => StreamRoot r b ∨ DeflateOwned i s b) [⟨z.next_out, out.length⟩] ∧
      LiveChange h after (fun _ => False) (fun _ => False) ∧ after.nalloc = h.nalloc