A compression task begins with caller-provided bytes. Windows and matching produce symbols; the encoder turns symbols into bits; the decoder recovers bytes. Caller buffers can change between calls, and allocation can fail.
The proof follows those actual objects. Read a component’s algorithms, layouts, and optimizations first, then the relations it establishes and passes onward. Each topic ends with a proof chapter, linked back to its algorithm background.
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
| Object in the task | Proof connection |
|---|---|
| Input and symbols | Chosen symbols expand to the accepted input. |
| Encoding and decoding | Actual output satisfies an independent format relation and decodes to the same bytes. |
| States across calls | Every legal return preserves a usable state and exact consumption and delivery. |
| Live memory and resources | Accesses are valid, unrelated objects are preserved, and allocations and frees are accounted for. |
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.
Targets, implementation, and acceptance scope
Chapters distinguish source readings, available local results, and remaining composition obligations. Follow links to complete targets, caller premises, and Lean proof bodies. The project progress page records acceptance scope and remaining work.
Complete targets and call sequences ↗Translation and model boundary ↗Project progress ↗