What must be proved
75d616fc8a509c62 · Source at the matching commit ↗This is the specification section. Read it before the model and proof guides. It states required behaviour. It does not report completed verification. Progress is the single current-status and remaining-work page.
Read in this order
| Order | Document | Question it answers |
|---|---|---|
| 1 | Platform assumptions | Which system environment, including the per-object size bound, is accepted? |
| 2 | Safety | What are UB, memory safety, termination, frame and ownership obligations? |
| 3 | Input configurations | Which fixed build and nested input ranges does a coverage colour describe? |
| 4 | API contracts | What may each caller pass, and what must each entry return or change? |
| 5 | Internal helper contracts | What must the real caller establish before invoking a helper? |
| 6 | Compressed-data format | What do DEFLATE, zlib and gzip bytes mean independently of the implementation? |
| 7 | Format relations | How is that byte meaning expressed as mathematical relations? |
API pages define entry behaviour. Format pages define byte meaning. Safety is shared by both engines and every public entry. These are different obligations, so each has one canonical home here.
Documentary and formal statements
The exact fixed questions are Lean propositions under ZlibF/Spec/ and the
file-specific specification namespaces. The target index
links each question to its exact statement and proof evidence. The documentary
contracts explain those questions; a prose change cannot discharge a target,
change its preconditions or grant a coverage colour.
Some documentary preconditions are narrower than the public header. Read the entry's explicit scope and deviations. A narrow internal lemma does not establish the complete public contract.
Continue to the model and proofs
The model guide explains how C operations are represented. The trusted base records assumptions and representation gaps. The proof guides explain how the specifications are established. The checking guide explains acceptance and registration.