deflateSetDictionary
Load preset bytes as compression history without emitting them as input data.
Full chapter and shared rules ↗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 deflateSetDictionary(z_streamp strm, const Bytef *dictionary, uInt dictLength);
Load preset bytes as compression history without emitting them as input data.
Domain Restricted domain. Effect: update history and dictionary checksum.
Pre live raw or zlib stream, immediately after init or deflateReset, before its first
deflate and first dictionary call. dictionary is non-NULL, covers dictLength
readable bytes and is separate from the window.
Post return Z_OK. History retains an available suffix of the dictionary, at most
one window. The dictionary checksum for zlib covers the entire supplied dictionary.
The original next_in and avail_in are restored; total_in increases by
min(dictLength, window size). No compressed output is delivered and no allocation occurs.
The decoder must be given the same preset dictionary when required.
Outside focused scope: gzip, NULL dictionary, zlib after its initial state, nonzero
lookahead, or raw input not at a completed block boundary returns Z_STREAM_ERROR
without changes. Raw replacement at legal boundaries and repeated pre-start zlib calls
remain in the public goal. Repeated zlib calls accumulate Adler-32 rather than restarting it.
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_streamwith 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_inreadable bytes; output coversavail_outwritable 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
deflateEndfree 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
nameandcommenthave a terminating zero;extracovers its stated length. Focused format contracts useextra_len <= 65535. - Checked refusals: except for init and bounds, a failed stream check returns
Z_STREAM_ERRORbefore normal operation, without writes.deflateCopyadditionally 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.deflateSetDictionary
Proof status: Not completed · Evidence and remaining work
/-- `int deflateSetDictionary(z_streamp strm, const Bytef *dictionary, uInt dictLength)`.
The raw path checks the block boundary. Repeated zlib dictionaries accumulate their checksum.
The temporary input binding is restored, and no allocation is performed. -/
def Goal.deflateSetDictionary : Prop :=
∀ h r i z s source n xs old,
Zlib.Deflate.Spec.DGood h r i z s → LibraryGlobals h →
DeflateDictionary h s old → (source ≠ .null → Bytes h source n.toNat xs) →
Separate source n.toNat s.window s.window_size.toNat →
∃ rc after, C.run (Zlib.Deflate.deflateSetDictionary (some r) source n) h = .ok (rc, after) ∧
(if source = .null ∨ s.wrap = 2 ∨ (s.wrap = 1 ∧ s.status ≠ INIT_STATE) ∨
s.lookahead ≠ 0 ∨ (s.wrap = 0 ∧ s.strstart.toUInt64.toInt64 ≠ s.block_start) then
rc = Z_STREAM_ERROR ∧ after = h
else rc = Z_OK ∧ ∃ z' s' dict,
Zlib.Deflate.Spec.DGood after r i z' s' ∧ DeflateDictionary after s' dict ∧
z' = { z with
total_in := z.total_in + UInt64.ofNat (min xs.length s.w_size.toNat)
adler := if s.wrap = 1 then adlerValue z.adler xs else z.adler } ∧
s'.wrap = s.wrap ∧ s'.lookahead = 0 ∧ s'.block_start = s'.strstart.toUInt64.toInt64 ∧
dict <:+ old ++ xs ∧ dict.length ≤ s.w_size.toNat ∧
min (old.length + xs.length) (s.w_size.toNat - 262) ≤ dict.length) ∧
Frame h after (fun b => StreamRoot r b ∨ DeflateOwned i s b) ∧
LiveChange h after (fun _ => False) (fun _ => False) ∧ after.nalloc = h.nalloc