Deflate.lean

Lean source with line numbers. Follow a line number to locate a statement, or an import to read its dependency.

1import ZlibF.Spec.Format.Huffman
2
3/-!
4# Format: DEFLATE (RFC 1951) as a declarative relation
5
6the DEFLATE block rules in `docs/spec/format/README.md`. The relations say exactly what zlib's `inflate` accepts
7(zlib is stricter than the RFC in the places listed in format.md; each is a premise below).
8
9Convention: the history `h` is the output produced so far (without the preset dictionary);
10a back-reference may reach into `dict ++ h` (`F-distance-bound`).
11Stored blocks need to know the position in the current byte. A relation here is always
12applied to the bits of a whole number of bytes (`bytesToBits`), so the number of bits left
13in the current byte is `inp.length % 8`; `Deflate.Prefix` is the entry point that guarantees this.
14-/
15
16namespace ZlibF.Spec
17
18/-- `F-match-copy`: copy `n` bytes one at a time from `dist` bytes back in `dict ++ h`.
19The copy may overlap itself (`n > dist`): bytes copied earlier are read again. -/
20def copyBack (dict : List UInt8) (dist : Nat) : Nat → List UInt8 → List UInt8
21  | 0, h => h
22  | n + 1, h => copyBack dict dist n (h ++ [(dict ++ h).getD ((dict ++ h).length - dist) 0])
23
24/-- The symbols of one Huffman block with the literal/length code `L` and distance code `D`
25(RFC 1951, 3.2.3 and 3.2.5; format.md 2.7). `Symbols L D dict h inp rest out`: starting with output
26`h` and bits `inp`, the block ends with the end-of-block symbol, leaves the bits `rest`, and
27the output is `out`. -/
28inductive Symbols (L D : List Nat) (dict : List UInt8) :
29    List UInt8 → List Bool → List Bool → List UInt8 → Prop
30  /-- Symbol 256: end of block. -/
31  | eob {h : List UInt8} {inp r : List Bool} :
32      decodeSym L inp = some (256, r) → Symbols L D dict h inp r h
33  /-- Symbols 0..255: output that byte. -/
34  | lit {h : List UInt8} {inp r rest : List Bool} {s : Nat} {out : List UInt8} :
35      decodeSym L inp = some (s, r) → s < 256 →
36      Symbols L D dict (h ++ [s.toUInt8]) r rest out → Symbols L D dict h inp rest out
37  /-- Symbols 257..285: length code, its extra bits, distance code, its extra bits (in this
38  order, `F-length-table`, `F-distance-table`), then a copy of `len` bytes from `dist` back.
39  Distance symbols 30 and 31 (possible in the fixed code) are invalid; `dist` may not exceed
40  the output so far plus the dictionary (`F-distance-bound`). -/
41  | copy {h : List UInt8} {inp r1 r2 r3 r4 rest : List Bool} {s d xl xd : Nat} {out : List UInt8} :
42      decodeSym L inp = some (s, r1) → 257 ≤ s → s ≤ 285 →
43      readBits (lengthExtras.getD (s - 257) 0) r1 = some (xl, r2) →
44      decodeSym D r2 = some (d, r3) → d ≤ 29 →
45      readBits (distExtras.getD d 0) r3 = some (xd, r4) →
46      xd + distBases.getD d 0 ≤ (dict ++ h).length →
47      Symbols L D dict
48        (copyBack dict (distBases.getD d 0 + xd) (lengthBases.getD (s - 257) 0 + xl) h) r4 rest out →
49      Symbols L D dict h inp rest out
50
51/-- The code lengths of a dynamic block, read with the code-length code `cl`
52(RFC 1951, 3.2.7; `F-dynamic-repeat`). `CodeLens cl total acc inp rest lens`: `acc` lengths are
53already read, reading continues until there are exactly `total`, and `lens` is the result.
54A repeat may not run past `total` and symbol 16 needs a previous length. -/
55inductive CodeLens (cl : List Nat) (total : Nat) :
56    List Nat → List Bool → List Bool → List Nat → Prop
57  /-- All `total` lengths are read. -/
58  | done {acc : List Nat} {inp : List Bool} : acc.length = total → CodeLens cl total acc inp inp acc
59  /-- Symbols 0..15: that length. -/
60  | len {acc : List Nat} {inp r rest : List Bool} {s : Nat} {out : List Nat} :
61      acc.length < total → decodeSym cl inp = some (s, r) → s < 16 →
62      CodeLens cl total (acc ++ [s]) r rest out → CodeLens cl total acc inp rest out
63  /-- Symbol 16: repeat the previous length 3 to 6 times (2 extra bits). -/
64  | rep16 {acc : List Nat} {inp r1 r2 rest : List Bool} {x : Nat} {out : List Nat} :
65      acc.length < total → decodeSym cl inp = some (16, r1) → acc ≠ [] →
66      readBits 2 r1 = some (x, r2) → acc.length + (3 + x) ≤ total →
67      CodeLens cl total (acc ++ List.replicate (3 + x) (acc.getLastD 0)) r2 rest out →
68      CodeLens cl total acc inp rest out
69  /-- Symbol 17: repeat length 0, 3 to 10 times (3 extra bits). -/
70  | rep17 {acc : List Nat} {inp r1 r2 rest : List Bool} {x : Nat} {out : List Nat} :
71      acc.length < total → decodeSym cl inp = some (17, r1) →
72      readBits 3 r1 = some (x, r2) → acc.length + (3 + x) ≤ total →
73      CodeLens cl total (acc ++ List.replicate (3 + x) 0) r2 rest out →
74      CodeLens cl total acc inp rest out
75  /-- Symbol 18: repeat length 0, 11 to 138 times (7 extra bits). -/
76  | rep18 {acc : List Nat} {inp r1 r2 rest : List Bool} {x : Nat} {out : List Nat} :
77      acc.length < total → decodeSym cl inp = some (18, r1) →
78      readBits 7 r1 = some (x, r2) → acc.length + (11 + x) ≤ total →
79      CodeLens cl total (acc ++ List.replicate (11 + x) 0) r2 rest out →
80      CodeLens cl total acc inp rest out
81
82/-- The order in which the lengths of the code-length alphabet are stored (RFC 1951, 3.2.7). -/
83def clOrder : List Nat := [16, 17, 18, 0, 8, 7, 9, 6, 10, 5, 11, 4, 12, 3, 13, 2, 14, 1, 15]
84
85/-- Read the `n` three-bit code-length-code lengths (`HCLEN + 4` of them, in `clOrder`) and
86return the lengths of the 19 symbols in symbol order; those not stored are 0. -/
87def readCodeLenLens (n : Nat) (inp : List Bool) : Option (List Nat × List Bool) :=
88  match readNats 3 n inp with
89  | none => none
90  | some (vs, r) =>
91    some ((List.range 19).map fun sym =>
92      if clOrder.idxOf sym < n then vs.getD (clOrder.idxOf sym) 0 else 0, r)
93
94/-- `F-dynamic-limits`: zlib rejects `HLIT + 257 > 286` and `HDIST + 1 > 30`
95(`too many length or distance symbols`). Here `hlit` and `hdist` are the raw 5-bit fields. -/
96abbrev DynamicCountsOK (hlit hdist : Nat) : Prop :=
97  hlit + 257 ≤ 286 ∧ hdist + 1 ≤ 30
98
99/-- `F-dynamic-eob`: the length of symbol 256 must not be 0
100(`invalid code -- missing end-of-block`). -/
101abbrev HasEndOfBlock (litLens : List Nat) : Prop :=
102  litLens.getD 256 0 ≠ 0
103
104/-- The body of a block of type `bt` (RFC 1951, 3.2.4 to 3.2.7), after the three header bits.
105`Body dict bt h inp rest out`. There is no constructor for `bt = 3` (`F-block-type-3`). -/
106inductive Body (dict : List UInt8) :
107    Nat → List UInt8 → List Bool → List Bool → List UInt8 → Prop
108  /-- `BTYPE = 0` (`F-stored-complement`): skip to the byte boundary, `LEN` and `NLEN` (16 bits
109  each, least significant bit first), `NLEN` is the complement of `LEN`, then `LEN` bytes. -/
110  | stored {h : List UInt8} {inp r1 r2 r3 : List Bool} {len nlen : Nat} {bs : List UInt8} :
111      readBits 16 (inp.drop (inp.length % 8)) = some (len, r1) →
112      readBits 16 r1 = some (nlen, r2) → nlen = 65535 - len →
113      readBytes len r2 = some (bs, r3) →
114      Body dict 0 h inp r3 (h ++ bs)
115  /-- `BTYPE = 1` (`F-fixed-lengths`): the fixed codes. -/
116  | fixed {h : List UInt8} {inp rest : List Bool} {out : List UInt8} :
117      Symbols fixedLitLens fixedDistLens dict h inp rest out → Body dict 1 h inp rest out
118  /-- `BTYPE = 2` (RFC 1951, 3.2.7; format.md 2.6): `HLIT`, `HDIST`, `HCLEN`, the code-length code,
119  the literal/length and distance lengths, then the symbols. `F-dynamic-limits`,
120  `F-dynamic-repeat` (in `CodeLens`), `F-dynamic-eob`, `F-dynamic-valid`. -/
121  | dynamic {h : List UInt8} {inp r1 r2 r3 r4 r5 rest : List Bool} {hlit hdist hclen : Nat}
122      {cl lens : List Nat} {out : List UInt8} :
123      readBits 5 inp = some (hlit, r1) → readBits 5 r1 = some (hdist, r2) →
124      readBits 4 r2 = some (hclen, r3) → DynamicCountsOK hlit hdist →
125      readCodeLenLens (hclen + 4) r3 = some (cl, r4) → Acceptable .codeLength cl →
126      CodeLens cl (hlit + 257 + (hdist + 1)) [] r4 r5 lens →
127      HasEndOfBlock (lens.take (hlit + 257)) →
128      Acceptable .litLen (lens.take (hlit + 257)) → Acceptable .dist (lens.drop (hlit + 257)) →
129      Symbols (lens.take (hlit + 257)) (lens.drop (hlit + 257)) dict h r5 rest out →
130      Body dict 2 h inp rest out
131
132/-- A sequence of blocks (RFC 1951, 3.2.3; format.md 2.2): the three header bits
133`BFINAL` and `BTYPE`, the body, and, unless `BFINAL` was 1, more blocks.
134`Blocks dict h inp rest out`: starting with output `h`, the blocks use the bits up to `rest`. -/
135inductive Blocks (dict : List UInt8) : List UInt8 → List Bool → List Bool → List UInt8 → Prop
136  /-- A block with `BFINAL = 1`. -/
137  | last {h : List UInt8} {inp r1 r2 rest : List Bool} {bt : Nat} {out : List UInt8} :
138      readBits 1 inp = some (1, r1) → readBits 2 r1 = some (bt, r2) →
139      Body dict bt h r2 rest out → Blocks dict h inp rest out
140  /-- A block with `BFINAL = 0`, followed by more blocks. -/
141  | more {h h' : List UInt8} {inp r1 r2 r3 rest : List Bool} {bt : Nat} {out : List UInt8} :
142      readBits 1 inp = some (0, r1) → readBits 2 r1 = some (bt, r2) →
143      Body dict bt h r2 r3 h' → Blocks dict h' r3 rest out → Blocks dict h inp rest out
144
145/-- A deflate stream that begins `stream`, with the preset dictionary `dict` (empty if none),
146is followed by the bytes `tail` and produces `out`: the blocks end at some bit; the rest of
147that byte is skipped (padding is ignored, as in zlib); and the bytes after it are exactly `tail`.
148This is how the wrappers find their trailer. -/
149def Deflate.Prefix (dict stream tail out : List UInt8) : Prop :=
150  ∃ rest, Blocks dict [] (bytesToBits stream) rest out ∧
151    rest.drop (rest.length % 8) = bytesToBits tail
152
153/-- Raw deflate data (RFC 1951): `stream` is exactly one deflate stream with no bytes
154after it, and it decodes to `out`. `dict` is the preset dictionary (`[]` if none). -/
155def Deflate.Decodes (dict stream out : List UInt8) : Prop :=
156  Deflate.Prefix dict stream [] out
157
158/-- `F-deflate-valid` for raw deflate: `compressed` is a valid compressed stream for
159`input`. This is what `deflate` has to produce (without a dictionary). -/
160def Deflate.Valid (input compressed : List UInt8) : Prop :=
161  Deflate.Decodes [] compressed input
162
163end ZlibF.Spec