Format model in Lean

Documentation home · Data format · API guide

The format model describes how compressed bytes determine uncompressed bytes. It has no heap or pointers. It is a specification to refine, not an implementation of the streaming API. Read the format guide for the rules and the API model for calls, buffers and return values. Accepted results and remaining work live in progress.

The umbrella module is ZlibF/Spec/Format.lean. The token extension is imported separately. Definitions below are in namespace ZlibF.Spec, except the local token relations in ZlibF.Spec.Token.

Module map

From bytes to output

flowchart TD
    B["bytesToBits"] --> K["Blocks: header and body"]
    K --> S["Body.stored: aligned bytes"]
    K --> F["Body.fixed: fixed codes"]
    K --> D["Body.dynamic: lengths and codes"]
    D --> C["CodeLens: expand code-length symbols"]
    F --> Y["Symbols: literals, copies, end"]
    D --> Y
    S --> P["Deflate.Prefix: final padding and byte tail"]
    Y --> P
    P --> R["Deflate.Decodes: empty tail"]
    P --> Z["Zlib.Decodes: Adler-32 tail"]
    P --> G["Gzip.Decodes: CRC-32 and size tail"]

Readers such as readBits, readBytes and decodeSym return either none or a value paired with the remaining bits. Relation constructors require the appropriate reader equations. There is no constructor for an invalid block type or reserved length/distance symbol.

Symbols L D dict h inp rest out starts with history h, uses literal/length lengths L and distance lengths D, and ends at an end-of-block symbol. It consumes inp down to rest and leaves output out. copyBack appends each copied byte before reading the next one, so overlapping matches have their ordinary bytewise meaning.

Blocks dict h inp rest out composes bodies until a block with BFINAL = 1. The block grammar uses bits derived from whole input bytes. Under that entry condition, inp.length % 8 is the number of bits left before the next byte boundary; stored bodies drop that many bits.

The public format relations differ in what they require after the final block:

The wrappers use Deflate.Prefix with the required trailer bytes as its tail. They still describe exact streams: bytes after the trailer are excluded. An API theorem about input left after Z_STREAM_END needs a separate consumed-prefix statement.

Rule map

The F-* rules are defined in the format guide. This table locates their formal counterparts without making an implementation-correctness claim.

The Valid predicates reverse the emphasis of Decodes: the compressed argument must decode to the supplied input. They do not select one encoding. Zlib.ValidWith supplies the preset dictionary; the other listed Valid predicates use no dictionary.

Model choices and boundaries

History and small windows. Symbols.copy uses the full dict ++ h history, not an explicit saved-window state. The distance table caps a reference at 32768. The zlib header's window field limits the initial dictionary suffix, but does not add a distance premise to Symbols.copy. This keeps the existing model choice explicit: default decoding can use current-call output beyond a small saved window, while a later call may lack those bytes. The C also has a separate INFLATE_STRICT check. Refinement for all configured windows and output-buffer boundaries is unfinished. The declarative relation alone does not establish operational acceptance for every split.

Dictionaries. With FDICT, Zlib.Decodes dict checks the Adler-32 of the entire supplied dictionary but passes only its last Zlib.windowSize cmf bytes to the DEFLATE relation. Without FDICT, it passes [] and ignores dict. A dictionary with Adler-32 1 may be empty. Raw Deflate.Decodes takes its dictionary history directly. Gzip starts with empty history.

Table acceptance. Acceptable permits all-zero length sets for all three code kinds. Such a set gives no decodable symbol. The single used symbol of length 1 is allowed only for literal/length and distance kinds. HasEndOfBlock separately rules out an empty dynamic literal/length code. Neither table acceptance nor a local successful token implies a whole valid block.

Padding. Stored-block alignment and final-byte padding discard bits without requiring them to be zero. Extra complete bytes are handled by the explicit tail, rather than padding.

Gzip metadata. Gzip.Decodes requires four MTIME bytes, zero reserved flag bits, an extra-field length below 2^16, and no embedded zero in the chosen name or comment. FTEXT, MTIME, XFL and OS otherwise remain unconstrained. Witnesses for optional fields whose flags are clear do not contribute bytes; empty witnesses can satisfy their constraints. One relation covers one member, not a whole concatenated gzip file.

Local decoding. Token.Step describes one literal, match or end-of-block without assuming that later input is valid. Token.Rejected describes irreversible invalid-code or unavailable-history cases. The goals step_composes_symbols, symbols_exposes_step and rejected_has_no_symbols connect these local relations to the original Symbols grammar. This boundary prevents a valid future completion from serving as an assumption for output already returned by an API call.

What belongs outside the format relation

Examples.lean supplies concrete positive and negative checks of the specification. Its proofs use kernel evaluation and relation constructors or inversion. Such examples help review the definitions; they do not establish their correspondence to every RFC case or to the translated implementation. Differential tests likewise provide evidence of fidelity, not proof. See progress for the acceptance status of implementation refinements.