These articles explain how zlib compresses and recovers data, how applications use it, and what the implementation’s proofs must establish. Start with the component map below, then choose the algorithm overview, implementation detail, or a function’s complete contract.
Part one builds the overall picture of algorithms and interfaces. Part two opens each topic’s algorithms and optimizations before developing its proof argument. Chapters link their background and next step; global contents are always available at the side.
The compression and decoding map
See each component’s job before opening its algorithm or proof. Hover, focus, or select a node to explore its inputs, outputs, and reading links.
Windows and matching
A repeated passage can be described by a backward distance and a copy length. The compressor keeps recent history to find reusable content. A sliding window limits the retained history; hash chains reduce the candidates that need byte comparisons.
- Input
- Input bytes and recent history
- Result
- Literals and length/distance pairs
Huffman construction
Symbols occur at different frequencies. Shorter codes for frequent symbols can reduce the cost. The decoder also needs to know which codes were used, so code lengths must be described.
- Input
- Symbols and their frequencies
- Result
- Lengths, codes, and tree descriptions
Blocks and compression output
Codes have different lengths, while applications receive whole bytes. This component chooses a block representation, packs codes into bytes, and holds undelivered bytes until the caller supplies space.
- Input
- Symbols, codes, and output space
- Result
- Blocks and bytes awaiting delivery
Bit input, decode tables, and copying
The decoder reads blocks and code tables and recovers literals and matches. Literals become bytes directly; matches copy from history, one byte at a time, to recover the original content.
- Input
- Compressed bits and available history
- Result
- Recovered original bytes
Streaming state and wrappers
Applications often divide a large task into input and output batches. When input or output space runs out, stream state remembers the progress so a later call can continue with new buffers. Zlib and gzip headers and trailers belong to the same task.
- Input
- Batched input and finite output space
- Result
- A state that can pause and resume
State operations and resource lifetime
Windows and internal state need storage, and allocation can fail. Initialization, reset, copy, and end determine what can be retained and what must be cleaned up.
- Input
- State, windows, and other resources
- Result
- Usable state and exact cleanup
Checksums and composition
Zlib and gzip wrappers store a checksum of the uncompressed data. Recomputing and comparing it during decoding helps detect damage. Adler and CRC accumulate this information in a small state and continue across buffers.
- Input
- Uncompressed data
- Result
- Checksums and comparison results
Application interfaces and external interaction
An application supplies input, receives output, and handles results. Buffers, callbacks, and file interfaces offer different ways to use the same compression and decoding engines.
- Input
- Requests and application data
- Result
- Delivered data and results
Algorithms & interfaces
From repetition to a compressed stream and back to caller-owned bytes. Build the overall picture, then consult exact interfaces.
Read the algorithm overview →Explore calls and interfaces ↗Algorithm detail and formal verification
Follow an implementation path: how data is laid out, how optimizations work, and which facts the proof must establish.
Choose a detailed topic →Consult the other component arguments ↗Three symbols, five bytes
This detailed route starts with A, B, and a length-6, distance-2 match. Choose the block representation, emit its bits, follow reads and writes in shared memory, then connect those facts into a proof.
- 01IMPLEMENTATION DETAIL↗
Block selection and symbol costs
Compare three block representations and see when sending new codes is worth its cost.
- 02IMPLEMENTATION DETAIL↗
Bit output and byte buffering
Pack variable-length codes into bytes and deliver them to the caller.
- 03IMPLEMENTATION DETAIL↗
Shared storage and output prefixes
Understand how shared memory can preserve symbols that have not yet been read.
- 04PROOF ARGUMENT↗
The output proof argument
Explain how each write preserves meaning from symbols to delivered output.
All detailed topics
Windows and matching ↗
Where match lengths and distances come from, and why recent history is enough.
Huffman construction ↗
Use fewer bits for frequent symbols and reconstruct the same codes at the decoder.
Blocks and compression output ↗
Write selected symbols into compressed blocks and safely deliver their bytes.
Bit input, decode tables, and copying ↗
Read compressed bytes, identify symbols, and recover the original data.
Streaming state and wrappers ↗
Understand why one task spans calls and how it resumes after a pause.
State operations and resource lifetime ↗
Start, reuse, copy, and end tasks while handling allocation failure.
Checksums and composition ↗
Check data across batches and retain the information needed to combine sequences.
Application interfaces and external interaction ↗
Choose suitable calls for whole buffers, callbacks, and gzip files.
From overview to detailed reading
Complete reference
Function pages retain complete domains, results, and error paths. Follow chapter links into component arguments and Lean proof bodies.