REFERENCE / ZLIB × LEAN
Documentation
The guide, complete interface contracts, and detailed proofs share one documentation system. Original material is read at build time, preserving long arguments and error paths.
Algorithms and interfaces
All public API contracts ↗Formal verification
Inflate and deflate proof routes ↗Complete original documentation tree
- Documentation ↗
README.md - Fixed questions, editable proofs ↗
anti-cheating.md - Checking a verification claim ↗
checking/README.md - Reviewed recursive execution helpers ↗
checking/compiler-helper-review.md - Public contract review record ↗
checking/contract-review.md - Public verification goals ↗
checking/goals.md - Independent integration review ↗
checking/pr-integration-review.md - Proof mutants ↗
checking/proof-mutants.md - Public query registration review ↗
checking/query-registration-review.md - Local proof registration checks ↗
checking/registration-review.md - Trusted-runtime review record ↗
checking/runtime-review.md - Heap-table review record ↗
checking/runtime-tables-review.md - Memory, translation and external-I/O semantics ↗
design/README.md - API models and the concrete boundary ↗
design/api-model.md - From C to a checked theorem ↗
design/architecture.md - External I/O: files, formatting and local storage ↗
design/external-io.md - Translating C without changing its behaviour ↗
design/translation.md - Caller domains and representation limits ↗
deviations.md - Historical evidence register ↗
findings.md - 2. Repetition, symbols and bits ↗
guide/encoding.md - 6. Choosing an application interface ↗
guide/interfaces.md - 1. A complete compression and decompression task ↗
guide/round-trip.md - 5. Reuse, checkpoints and controlled changes ↗
guide/state-operations.md - 3. Pausing and continuing a stream ↗
guide/streaming.md - 4. One DEFLATE body, three format paths ↗
guide/wrappers.md - Understanding and proving zlib ↗
overview.md - Proof progress and remaining work ↗
progress.md - Implementation proof reference ↗
proof/README.md - Adler-32: bounded sums and modular refinement ↗
proof/adler32.md - Buffer utilities and output bounds ↗
proof/buffers.md - Callback decoding: ownership and finite input ↗
proof/callbacks.md - CRC-32: byte ranges, braids and polynomial meaning ↗
proof/crc32.md - Stream compression: window, chains and lifecycle ↗
proof/deflate.md - Gzip files: source flow, ownership and cleanup ↗
proof/gzip.md - Fast decoding: margins, history and source bits ↗
proof/inffast.md - Stream decoding: modes, history and call composition ↗
proof/inflate.md - Decode tables: from lengths to initialized entries ↗
proof/inftrees.md - Proving one function ↗
proof/method.md - Earlier arguments and reference sources ↗
proof/references.md - Trees and block emission: bounds, codes and shared storage ↗
proof/trees.md - Utilities: allocation and constant queries ↗
proof/zutil.md - Runtime schema: the structs of zlib on the object heap ↗
runtime-schema.md - What must be proved ↗
spec/README.md - zlib API manual ↗
spec/api/README.md - Checksums ↗
spec/api/checksums.md - How to read a contract ↗
spec/api/contracts.md - Stream compression ↗
spec/api/deflate-stream.md - Gzip files ↗
spec/api/gz-file.md - Callback decompression ↗
spec/api/inflate-back.md - Stream decompression ↗
spec/api/inflate-stream.md - Shared stream rules ↗
spec/api/streams.md - Buffer utilities and library information ↗
spec/api/utility.md - Data format ↗
spec/format/README.md - Format model in Lean ↗
spec/format/model.md - Input configurations and coverage colours ↗
spec/input-configurations.md - Obligations at internal calls ↗
spec/internal-contracts.md - Accepted platform assumptions ↗
spec/platform.md - Safety claims and caller obligations ↗
spec/safety.md - What the kernel does not establish ↗
trusted-base.md