uncompress2_z
Decodes the first zlib stream and reports both output size and input consumption.
Full chapter and shared rules ↗767fa1407a7fe3d1 · 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 uncompress2_z(Bytef *dest, z_size_t *destLen, const Bytef *source, z_size_t *sourceLen);
Decodes the first zlib stream and reports both output size and input consumption.
Domain Restricted domain.
Pre Restricted buffer domain above. *sourceLen is the available input and *destLen
the output capacity. Either length pointer may be NULL for checked rejection.
A NULL data pointer is allowed only with a zero corresponding length, or for checked rejection.
Malformed, truncated, raw, gzip and dictionary-dependent input are included as error cases.
Post Z_OK means a complete checked zlib stream decoded to the output.
Trailing input is unused. Z_BUF_ERROR means output filled the capacity and input remains.
Z_DATA_ERROR covers malformed or incomplete input and a required preset dictionary.
Z_MEM_ERROR means allocation failed and can follow partial output.
Effects Stateful; common effects apply. The argument checks precede initialisation:
NULL sourceLen, nonempty NULL source, NULL destLen, or positive-capacity NULL destination
returns Z_STREAM_ERROR with both existing length cells unchanged.
Initialisation failure also preserves both lengths and writes no output.
After initialisation, every return stores bytes consumed in *sourceLen and bytes produced
in *destLen, including later memory failure. Output already written remains available.
Edges NULL destination with zero capacity is accepted using a private output pointer;
a complete empty stream can succeed. Empty input is a data error after successful initialisation.
The exact final mapping is Z_STREAM_END to Z_OK, Z_NEED_DICT to Z_DATA_ERROR,
and Z_BUF_ERROR to Z_DATA_ERROR when no input remains. Other decoder codes are retained.
Shared conditions and scope
API manual · Shared stream rules · Checksums
Use the buffer utilities when the complete input and output capacity are known at the call. They manage a temporary stream internally. Use the stream pages when you need incremental I/O, a different wrapper, a dictionary or explicit flush boundaries.
| Task | Entries |
|---|---|
| Compress a buffer | Choose a level, default level, size the destination |
| Decompress a buffer | Report input consumed, output only |
| Inspect the library | Version, compile flags, error text |
The focused contracts follow compress.c, uncompr.c, zutil.c and zlib.h in the default
LP64 Linux build. _z forms use z_size_t; plain forms use uLong. Both are 64-bit here.
Source readings are to confirm by proof. They do not narrow the registered targets in
Utilities.lean and
Queries.lean.
Calls.lean fixes translated arguments and results.
See contract conventions for domain/effect labels and
progress for proof status and remaining work.
The buffer utilities create and release a local stream with the zlib wrapper and default settings.
flowchart LR
B["compressBound"] --> C["compress / compress2"]
C --> Z["zlib stream"] --> U["uncompress / uncompress2"]
U --> D["decoded bytes"]
Common conventions
For buffer calls, the domain is restricted to valid memory: non-NULL sources cover the stated readable input; non-NULL destinations cover the stated writable capacity. Non-NULL length pointers name readable, writable scalar cells. Input, output and length cells are separate, including the two length cells when both occur. The caller keeps those objects live and does not modify them during the call. Each entry states its allowed NULL cases. Other invalid pointers are outside this scope. Decompression error handling needs no valid compressed-data assumption.
Common effects. Every in-scope call terminates without a fault. Buffer calls preserve input and memory outside the output and length cells. They write at most the original capacity. All internal allocations are released before return, including on allocation failure; no local stream or owned allocation is returned. Pointer-valued queries return borrowed immutable storage. These are contract requirements, not claims that the implementation proofs are complete.
Formal contract
ZlibF.Spec.Public.Goal.uncompress2_z
Proof status: Not completed · Evidence and remaining work
/-- `int uncompress2_z(Bytef *dest, z_size_t *destLen, const Bytef *source, z_size_t *sourceLen)`.
Includes both nullable scalar checks, trailing input, partial output on memory failure and cleanup. -/
def Goal.uncompress2_z : Prop := UncompressCounted Zlib.Uncompr.uncompress2_z true