Huffman.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.Bits
2
3/-!
4# Format: canonical Huffman codes
5
6RFC 1951, 3.2.2 and `docs/spec/format/README.md` sections on canonical Huffman codes, dynamic tables and code alphabets.
7A code is given by a list of code lengths: `lens[s]` is the length of symbol `s`,
8and 0 means the symbol is unused. A symbol beyond the end of the list is unused.
9-/
10
11namespace ZlibF.Spec
12
13/-- The longest code length of deflate (RFC 1951, 3.2.7). -/
14def maxCodeLen : Nat := 15
15
16/-- `count lens l` is `count[l]` of RFC 1951, 3.2.2: the number of symbols of length `l`. -/
17def count (lens : List Nat) (l : Nat) : Nat :=
18  (lens.filter (· == l)).length
19
20/-- `codeStart lens l` is `code_start[l]` of `F-code-fits` / RFC 1951, 3.2.2:
21`code_start[1] = 0` and `code_start[l] = (code_start[l-1] + count[l-1]) * 2`.
22(Length 0 is not a code length, so its count is taken as 0.) -/
23def codeStart (lens : List Nat) : Nat → Nat
24  | 0 => 0
25  | l + 1 => (codeStart lens l + (if l = 0 then 0 else count lens l)) * 2
26
27/-- The canonical code of symbol `s` (`F-code-fits`, RFC 1951, 3.2.2): the symbols of
28length `l`, in increasing symbol order, get the consecutive values
29`code_start[l]`, `code_start[l]+1`, ..., written in `l` bits, most significant bit first
30(`F-bit-order`). Meaningful only if `lens[s] > 0`. -/
31def codeOf (lens : List Nat) (s : Nat) : List Bool :=
32  let l := lens.getD s 0
33  natToBitsMSB l (codeStart lens l + ((lens.take s).filter (· == l)).length)
34
35/-- `F-code-fits`: no code overflows its length, `code_start[l] + count[l] <= 2^l` for
36`l = 1..15`. This is the Kraft inequality; a set that breaks it is over-subscribed. -/
37abbrev Fits (lens : List Nat) : Prop :=
38  ∀ l ∈ List.range' 1 maxCodeLen, codeStart lens l + count lens l ≤ 2 ^ l
39
40/-- `F-code-complete`: the Kraft sum is exactly 1, that is, the codes of length 15 and
41shorter fill all `2^15` leaves. (Meant together with `Fits`.) -/
42abbrev Complete (lens : List Nat) : Prop :=
43  codeStart lens maxCodeLen + count lens maxCodeLen = 2 ^ maxCodeLen
44
45/-- The three kinds of code of a dynamic block. The code-length code never gets the
46single-symbol exception (`F-code-complete`, table of format.md 2.4). -/
47inductive CodeKind where
48  | codeLength
49  | litLen
50  | dist
51  deriving DecidableEq
52
53/-- What zlib's `inflate_table` accepts as the lengths of one code (`F-code-fits`,
54`F-code-complete`, `F-dynamic-valid`; format.md 2.4): every length is at most 15, the set
55is not over-subscribed, and it is complete, or it has no symbol at all, or (not for the
56code-length code) its only symbol has length 1. -/
57abbrev Acceptable (k : CodeKind) (lens : List Nat) : Prop :=
58  (∀ x ∈ lens, x ≤ maxCodeLen) ∧ Fits lens ∧
59    (Complete lens ∨ (∀ x ∈ lens, x = 0) ∨ (k ≠ .codeLength ∧ lens.filter (· != 0) = [1]))
60
61/-- `decodeSym lens inp`: the first symbol whose canonical code is a prefix of `inp`,
62with the bits after that code. `none` if no code is a prefix (an invalid code).
63For an `Acceptable` set at most one code is a prefix, because the code is prefix-free. -/
64def decodeSym (lens : List Nat) (inp : List Bool) : Option (Nat × List Bool) :=
65  match (List.range lens.length).find?
66      (fun s => lens.getD s 0 != 0 && (codeOf lens s).isPrefixOf inp) with
67  | some s => some (s, inp.drop (lens.getD s 0))
68  | none => none
69
70/-- `F-fixed-lengths` (RFC 1951, 3.2.6): the 288 literal/length code lengths of a fixed block:
718 for 0..143, 9 for 144..255, 7 for 256..279, 8 for 280..287. -/
72def fixedLitLens : List Nat :=
73  List.replicate 144 8 ++ List.replicate 112 9 ++ List.replicate 24 7 ++ List.replicate 8 8
74
75/-- `F-fixed-lengths`: the 32 distance code lengths of a fixed block, all 5. -/
76def fixedDistLens : List Nat := List.replicate 32 5
77
78/-- `F-length-table` (RFC 1951, 3.2.5): first match length of symbols 257..285, indexed by `s - 257`. -/
79def lengthBases : List Nat :=
80  [3, 4, 5, 6, 7, 8, 9, 10, 11, 13, 15, 17, 19, 23, 27, 31, 35, 43, 51, 59, 67, 83, 99, 115,
81   131, 163, 195, 227, 258]
82
83/-- `F-length-table`: number of extra bits of symbols 257..285, indexed by `s - 257`. -/
84def lengthExtras : List Nat :=
85  [0, 0, 0, 0, 0, 0, 0, 0, 1, 1, 1, 1, 2, 2, 2, 2, 3, 3, 3, 3, 4, 4, 4, 4, 5, 5, 5, 5, 0]
86
87/-- `F-distance-table` (RFC 1951, 3.2.5): first distance of distance symbols 0..29. -/
88def distBases : List Nat :=
89  [1, 2, 3, 4, 5, 7, 9, 13, 17, 25, 33, 49, 65, 97, 129, 193, 257, 385, 513, 769, 1025, 1537,
90   2049, 3073, 4097, 6145, 8193, 12289, 16385, 24577]
91
92/-- `F-distance-table`: number of extra bits of distance symbols 0..29. -/
93def distExtras : List Nat :=
94  [0, 0, 0, 0, 1, 1, 2, 2, 3, 3, 4, 4, 5, 5, 6, 6, 7, 7, 8, 8, 9, 9, 10, 10, 11, 11, 12, 12, 13, 13]
95
96end ZlibF.Spec