Understanding and proving zlib

Read one task, then expand the mechanism you need. Each illustrated chapter explains what an operation does and the proof obligation that follows from it. The header language menu switches between English and 简体中文 on the same page.

Contents

• Reading path
• Shared proof rules
• Scope
• Argument
• Evidence

Reading path

Follow a chapter's links when you need an exact contract or C-level argument. Specifications define required behavior; implementation arguments give the technical derivation by C component. These references serve different questions from the guided examples. Review records are grouped under Checking, outside this first reading path.

Shared proof rules

Scope

The initial target uses default x86_64 Linux and default inputs. Wider nested ranges are defined once in input configurations. Examples select particular runs without narrowing public targets. The accepted platform premises include each represented byte object having fewer than 2^63 bytes; this does not bound total stream length. Safety owns the exact UB, frame, termination and resource rules. Trusted base and deviations own model limits.

Argument

The subject is the pinned C plus registered patches, translated statement by statement. Implementation readings in the chapters are unfinished by proof. Initialization must establish the state and ownership invariant. Each actual call derives its helper premises and preserves the required facts on the returned heap; End accounts for released resources. A callee contract must be proved about that callee. A top-level domain needs a concrete witness.

The common method connects these steps by induction over legal call histories and relates actual bytes to independent format meaning. The chapters explain each mechanism's specific invariant at its example.

Evidence

Inspect the exact statement, caller domain and returned state. A local branch lemma or heap-free model theorem does not establish a whole public API. Earlier C1–C7 labels refer to the API model goals; concrete execution needs its own refinement argument. Finite differential runs validate examples, not universal claims. Checking defines acceptance on a named commit. Progress alone records current evidence, the complete target dependency graph and remaining work.