REFERENCE / ZLIB × LEAN

deflateCopy

Create an independent compressor with the same compression progress.

Source snapshot · 39ab1ace4bbe0b0e · 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 deflateCopy(z_streamp dest, z_streamp source);

Create an independent compressor with the same compression progress.

Domain Restricted domain. Effect: allocate and copy owned state.

Pre source is live. dest is a different writable z_stream with no owned state, separate from the source's memory. Source buffers and any retained header satisfy their lifetimes.

Post Z_OK gives dest five new owned allocations containing equivalent compression state; the source is unchanged. The copied stream fields include totals, allocator fields, I/O pointers and retained header pointer. Internal owned pointers are relocated to the new allocations. Both streams require their own deflateEnd and can continue independently. Their copied caller I/O pointers initially refer to the same buffers; assign separate output room before continuing both. The header remains shared caller-owned storage.

Z_MEM_ERROR frees every new allocation, clears dest->state and leaves other destination fields and the source unchanged. There is no new live state to release.

Outside focused scope: NULL destination gives Z_STREAM_ERROR; a failed source check also clears a non-NULL destination's state. The public goal explicitly assumes distinct streams. Self-copy and overwriting an already live destination are excluded here and do not receive a leak-free contract.

Back to the API manual · Contract conventions

Shared conditions and scope

API manual · Shared stream rules · Stream decompression

Use a z_stream compressor when input arrives in pieces, output space is limited, or you need a chosen wrapper, dictionary or flush boundary. Initialize once, call deflate with successive buffers, and end the stream even if compression is abandoned. For a single buffer, see compress and compress2.

Task	Entries
Start or reuse	Init, configured init, reset, reset retaining history
Supply metadata or history	Dictionary, read history, gzip header
Compress and size output	Deflate, bound, pending output, last flush bits
Adjust or branch	Parameters, tuning, priming, copy
Release storage	End

These focused contracts follow the pinned deflate.c, applied patches and zlib.h in the default LP64 Linux build. Source readings are to confirm by proof. They leave the broader registered public goals unchanged. See contract conventions for domain/effect labels and progress for proof status and remaining work.

Shared conventions

Each stated Pre requires termination without runtime faults and the stated Post. A call that retains a live stream preserves its representation invariant.

Live stream: a writable z_stream with a compressor state established by successful init or copy, preserved by legal calls, and not ended. The caller does not alter its internal state or allocator fields. Calls on one stream are sequential.
Buffers: input covers avail_in readable bytes; output covers avail_out writable bytes. They do not overlap each other, the stream or its owned state. A non-NULL scalar result points to a writable cell separate from other results and stream memory. These separation conditions are explicit focused assumptions; see safety.md.
Allocator: the default allocator/free pair is used, or both fields are NULL before init. Allocation may fail on any attempt. Custom allocator callbacks are outside this page's scope.
Frame and ownership: calls change only their stream, its owned state and stated output regions. Caller input is read-only. Caller buffers and header records remain caller-owned. Only init and copy allocate; only their failure cleanup and deflateEnd free memory. Other calls preserve the stream's allocation set.
Header lifetime: a retained gzip header and its optional fields remain readable and unchanged while used. Non-NULL name and comment have a terminating zero; extra covers its stated length. Focused format contracts use extra_len <= 65535.
Checked refusals: except for init and bounds, a failed stream check returns Z_STREAM_ERROR before normal operation, without writes. deflateCopy additionally clears a non-NULL destination state. Query output cells are untouched on this refusal.
Restricted domain means these explicit memory, lifetime and call-order conditions, plus the entry's Pre. It does not mean every representable pointer or integer is accepted. Error summaries cover readable checked states, not arbitrary invalid addresses.

Formal contract

ZlibF.Spec.Public.Goal.deflateCopy

Proof status: Not completed · Evidence and remaining work

/-- `int deflateCopy(z_streamp dest, z_streamp source)`.
Copy the initialized window, hash entries, pending bytes and symbols. Relocate the owned
buffers and tree descriptors. A failure clears destination state and releases every new block. -/
def Goal.deflateCopy : Prop :=
  (∀ h source, C.run (Zlib.Deflate.deflateCopy none source) h = .ok (Z_STREAM_ERROR, h)) ∧
  (∀ h dest z, dest.get h = some z →
    C.run (Zlib.Deflate.deflateCopy (some dest) none) h =
      .ok (Z_STREAM_ERROR, dest.put h { z with state := none })) ∧
  (∀ h source i z s dest oldDest,
    StreamReachable .deflate h source → Zlib.Deflate.Spec.DGood h source i z s →
    Zlib.Deflate.Spec.DefAlloc z → source ≠ dest → dest.get h = some oldDest →
    ∃ rc after,
      C.run (Zlib.Deflate.deflateCopy (some dest) (some source)) h = .ok (rc, after) ∧
      source.get after = some z ∧ after.dstates i = some s ∧ Frame h after (StreamRoot dest) ∧
      ((rc = Z_MEM_ERROR ∧ AllocationFailed h after ∧
        dest.get after = some { oldDest with state := none } ∧
        LiveChange h after (fun _ => False) (fun _ => False)) ∨
       (rc = Z_OK ∧ ∃ copied,
         Zlib.Deflate.Spec.DGood after dest h.nextBlk
           { z with state := some (.deflate h.nextBlk) } copied ∧
         copied = copiedDeflate dest h.nextBlk s copied ∧
         SameBytePrefix h after s.window copied.window s.high_water.toNat ∧
         SameWordPrefix h after s.head copied.head s.hash_size.toNat ∧
         SameWordPrefix h after s.prev copied.prev
           (if s.slid ≠ 0 ∨ s.strstart - s.insert > s.w_size then s.w_size.toNat
            else (s.strstart - s.insert).toNat) ∧
         SameBytePrefix h after s.pending_out copied.pending_out s.pending.toNat ∧
         SameBytePrefix h after s.sym_buf copied.sym_buf s.sym_next.toNat ∧
         (∀ b, DeflateOwned h.nextBlk copied b ↔ h.nextBlk ≤ b ∧ b < h.nextBlk + 5) ∧
         LiveChange h after (DeflateOwned h.nextBlk copied) (fun _ => False))))

Related definitions and source ↗