Implementation proof reference

For the first reading, follow the illustrated guide. Its chapters explain the algorithms and API uses together with their proof obligations. This section supplies the detailed arguments by C component.

This guide explains the arguments that connect the translated C to zlib's contracts. It separates mathematical lemmas, memory reasoning and composition across calls. The pages are proof plans and explanations. An argument in prose is not a kernel-checked theorem, and a theorem about a model is not yet a theorem about the translated function.

Read progress for the current checkpoint and the single list of remaining work. Read safety for the properties being claimed and checking for the evidence needed to accept a result. Historical proof names below help locate earlier arguments. They do not certify the present source, runtime or caller domain.

Choose a reading path

For the overall method, start with proving one function. It explains contracts, invariants, framing, ownership and the diagnosis of a stuck proof. Then read the API contracts, the format specification and the design guide as the function requires.

For decompression, read the checksum and allocator pages, then table construction, the fast decoder and the main decoder. The main decoder must establish the fast path's entry conditions. Table construction must establish the predicates that both decoders use.

For compression, read the checksum and allocator pages, then window and hash-chain reasoning in deflate.c. Read trees.c for tree construction, bit emission and the shared output/symbol buffer. The overlay bound is part of memory safety.

The single target graph shows actual proof references as solid arrows and C calls as dotted arrows. The evidence index separates those references from C calls and specification dependencies. A caller establishes each actual callee precondition; it need not assume a complete general-parameter API goal. The input-range guide also distinguishes strategy selection from the decoder's buffer-driven fast/slow dispatch.

Read a component page

Each page identifies its source and contract vocabulary, then explains the invariants and lemmas the function needs. A stated bound is conditional on the premises written beside it. The public theorem must obtain those premises from initialization, preceding calls and the documented caller requirements. It cannot assume a callee contract or discard a legal API case.

A source reading that still needs proof is marked unfinished. The identifiers U1–U12, F1–F9 and I-* link the reasoning to the safety document, method and internal contracts. They describe obligations, not acceptance status.

Intervals [a, b) include a and exclude b. An array pointer may be formed at its one-past position; that position may not be read. Unsigned operations wrap as in C. A proof that needs ordinary arithmetic must establish that wrapping does not change the relevant value.

The guide follows the default x86_64 Linux build first. A bound derived from that build's widths, tables or allocator branch must be revisited for another configuration. The trust boundary and deviations remain part of every claimed result.

Source correspondence and earlier arguments

Each component owns its file-specific C correspondence checks. Shared integer, object and control-flow rules stay in translation semantics. The gzip world has one external-I/O definition guide. The reference appendix retains earlier theorem-family mappings and historical experiments with their evidence limits. None supplies missing proofs or a second current-status list.