deflateUsed
Report the last byte's bit use at the most recent byte-boundary flush.
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 deflateUsed(z_streamp strm, int *bits);
Report the last byte's bit use at the most recent byte-boundary flush.
Domain Restricted domain. Effect: query with an optional scalar result.
Pre live stream; bits is NULL or a valid output cell.
Post return Z_OK. If requested, store the saved bit-use count: 1..8 after a
byte-boundary flush, or 0 since init/reset if none occurred. The stream is unchanged.
This saved count differs from the currently pending bits returned by deflatePending.
The public goal returns the stored value for every checked state, without assuming that an arbitrary represented state satisfies the normal-history range.
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.deflateUsed
Proof status: Registered proof · Evidence and remaining work
/-- `int deflateUsed(z_streamp strm, int *bits)`.
Return the modulo-eight bit-use count through the optional scalar result. -/
def Goal.deflateUsed : Prop :=
∀ bits, CheckedDeflate (fun p => Zlib.Deflate.deflateUsed p bits) (Z_STREAM_ERROR, none) <|
∀ h r i z s, DeflateView h r i z s →
C.run (Zlib.Deflate.deflateUsed (some r) bits) h =
.ok ((Z_OK, if bits then some s.bi_used else none), h)