inflateCopy
Create a decoder that can resume from the source position.
Full chapter and shared rules ↗ecafc184cdf44b7f · 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 inflateCopy(z_streamp dest, z_streamp source);
Create a decoder that can resume from the source position.
Domain Restricted domain: live source, distinct writable non-live destination.
Effects Allocates independent state and, if present, a window.
Pre The common conditions hold for source. Destination does not overlap source or its owned storage. Shared input/output and header pointers retain their caller lifetimes; give the streams separate writable destinations before use.
Post Z_OK copies decoding position, history and stream fields. Both streams
own their state/window independently and must be ended. Source is unchanged.
Caller buffer pointers, message and any registered header pointer are shared,
not deep-copied. No caller data is consumed or produced.
Errors NULL dest returns Z_STREAM_ERROR. For other refusals, non-NULL
dest has state cleared and is otherwise unchanged. Allocation failure returns
Z_MEM_ERROR and frees all allocations made by this attempt. Source is unchanged.
Edges Self-copy is excluded explicitly: the C overwrites the original state pointer, so the ownership consequence remains to confirm, not a clean refusal.
Shared conditions and scope
API manual · Shared stream rules · Stream compression
Use an inflate stream to decode input in pieces while controlling output space. Select zlib,
gzip or raw DEFLATE at initialization, then continue with more input or room until completion,
a dictionary request or an error. End releases the decoder after any of those outcomes.
For whole-buffer zlib decoding, see uncompress.
| Task | Entries |
|---|---|
| Start or reuse | Init, configured init, reset, new configuration, keep history |
| Decode or provide metadata | Inflate, set dictionary, read history, gzip header |
| Recover or inspect | Sync search, sync point, mark, table use |
| Adjust or branch | Prime bits, validation, distance option, copy |
| Release storage | End |
The focused contracts follow the pinned inflate.c and zlib.h in the default LP64 Linux
build, with gzip enabled and without optional invalid-distance or strict-distance modes.
Source readings are to confirm by proof. The broader registered public goals
retain their domains. See contract conventions for terminology and
progress for proof status and remaining work.
Common conditions
All contracts below have a Restricted domain. A C pointer type alone does not supply the storage, lifetime or call history required here.
- A live stream was successfully initialised or copied, has not been ended, retains its library-owned state, and is used without concurrent calls. Use the default allocator and free function. Init takes a writable, non-live stream with allocator fields set to NULL or the default functions.
- A readable or writable range has the stated capacity for the whole call. Caller ranges are separate from the stream and its owned storage. Input and output ranges do not overlap. Dictionary destinations, the registered header record and its destination buffers are separate from each other and from the stream. Registered header storage is also separate from input/output ranges on calls using it. These are explicit focused-domain restrictions.
- The caller owns its stream object and buffers. The library owns the state and optional window. A call changes only its stream, owned storage, stated output ranges and any registered header destination. It never frees caller buffers.
- A rejected stream check returns
Z_STREAM_ERRORwithout changes, unless a query or copy contract says otherwise. This covers NULL and safely readable records rejected by the check; it does not cover dangling or arbitrary pointers. The check requires allocators, state, the state's back-pointer and a valid mode. - Counters use the C unsigned widths and wrap. No contract assumes allocation succeeds. End remains available after decoding, dictionary or allocation errors.
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
Formal contract
ZlibF.Spec.Public.Goal.inflateCopy
Proof status: Not completed · Evidence and remaining work
/-- `int inflateCopy(z_streamp dest, z_streamp source)`.
Copy every decoder field, relocate internal table pointers, share application header pointers,
and copy the initialized window bytes. All new storage is independent; failure releases it. -/
def Goal.inflateCopy : Prop :=
(∀ h source, C.run (Zlib.Inflate.inflateCopy none source) h = .ok (Z_STREAM_ERROR, h)) ∧
(∀ h dest z, dest.get h = some z →
C.run (Zlib.Inflate.inflateCopy (some dest) none) h =
.ok (Z_STREAM_ERROR, dest.put h { z with state := none })) ∧
(∀ h source i z s dest oldDest,
StreamReachable .inflate h source → Zlib.Inflate.Spec.Good h source i z s →
Zlib.Inflate.Spec.DefAlloc z → source ≠ dest → dest.get h = some oldDest →
∃ rc after,
C.run (Zlib.Inflate.inflateCopy (some dest) (some source)) h = .ok (rc, after) ∧
source.get after = some z ∧ after.istates 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.Inflate.Spec.Good after dest h.nextBlk
{ z with state := some (.inflate h.nextBlk) } copied ∧
copied = { s with
strm := some dest, window := copied.window
lencode := relocateCode i h.nextBlk s.lencode
distcode := relocateCode i h.nextBlk s.distcode
next := relocateCode i h.nextBlk s.next } ∧
(s.window = .null ↔ copied.window = .null) ∧
(s.window ≠ .null → SameBytePrefix h after s.window copied.window s.whave.toNat) ∧
(∀ b, InflateOwned h.nextBlk copied b → h.nextBlk ≤ b) ∧
LiveChange h after (InflateOwned h.nextBlk copied) (fun _ => False))))