Skip to content
ZLIB × LEAN / ALGORITHM DETAIL & VERIFICATION

Bit input, decode tables, and copying

Read compressed bytes, identify symbols, and recover the original data.

THE JOB OF THIS COMPONENT

The decoder reads blocks and code tables and recovers literals and matches. Literals become bytes directly; matches copy from history, one byte at a time, to recover the original content.

Locate this topic on the global map ↗

The first 3 chapters explain algorithms, data layouts, and optimizations. The final chapter connects the proof argument. Read in order or enter from a familiar stage.

  1. 01
    IMPLEMENTATION DETAIL

    Bit input and lookahead

    Buffer arriving bytes and consume only the bits needed for the current field.

    ↗
  2. 02
    IMPLEMENTATION DETAIL

    Constructing decode tables

    Turn code lengths into tables that directly identify symbols.

    ↗
  3. 03
    IMPLEMENTATION DETAIL

    Fast decoding and back-reference copies

    Recover bytes from lengths and distances and understand the decoding fast path.

    ↗
  4. 04
    PROOF ARGUMENT

    The decoder proof argument

    Connect bit reading, table lookup, and copying into one decoding promise.

    ↗

Background and complete reference

Return to the algorithm overview ↗Complete API contracts ↗All detailed topics ↗
ZLIB × LEAN

Global contents

READING NOWBit input, decode tables, and copying