zlib × Lean¶
I put zlib's algorithms, interfaces, and verification into a standalone interactive guide. It has two reading routes:
- Algorithms and interfaces: start with repeated bytes, follow matching, codes, and blocks, then read about decoding and streaming calls. Complete API contracts remain available throughout.
- Algorithm detail and formal verification: open the implementation, follow its data structures, execution, and optimizations, then understand how the proof connects those steps.
The detailed routes cover windows and matching, Huffman construction, block output, decoding, streaming state, resource lifetime, checksums, and buffer, callback, and gzip-file interfaces. Each topic explains its algorithms and optimizations before using worked executions to develop the proof argument. Chapters link their background, next step, exact contracts, and source.
The article, interactions, and reference documentation live in the zlib-f project site. This blog provides the entrance.