inftrees.c.cover.leaf.lean

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

1import ZlibF.Proof.«inffast.c.tableok»
2import ZlibF.Zlib.«inftrees.c»
3
4/-!
5# The leaves that `inflate_table` writes
6
7`inflate_table` stores, for the symbol `w` of a code, the entry `here` with `op` and `val` taken from `lbase` / `lext`
8(`LENS`: `match = 257`) or `dbase` / `dext` (`DISTS`: `match = 0`) or the literal/end-of-block cases, and
9`bits = len - drop`. `LenLeaf` and `DistLeaf` (`inffast.c.tableok`) are the shapes `inflate_fast` needs. This module
10proves them for every symbol that the call can read (`w < 288` for `LENS`, `w < 32` for `DISTS`) by kernel
11evaluation of the tables of the translation, and that `bits + drop ≤ 15`.
12-/
13set_option autoImplicit false
14
15namespace Zlib.Inftrees.Proofs.Cover
16open C Zlib.Inffast.Spec
17
18set_option maxRecDepth 100000 in
19/-- All the `LENS` symbols `257 ≤ w < 288` get a length base (`w ≤ 285`: extra bits `≤ 5`, base `≥ 3`, base plus
20the largest extra at most 258) or an invalid code (`286`, `287`). -/
21theorem lext_lbase_shape : ∀ w, w < 288 → 257 ≤ w →
22    let op := (Zlib.Inftrees.lext.getD (w - 257) 0).toUInt8
23    let v := Zlib.Inftrees.lbase.getD (w - 257) 0
24    (op &&& 16 ≠ 0 ∧ (op &&& 15).toNat ≤ 5 ∧ 3 ≤ v.toNat ∧ v.toNat + 2 ^ (op &&& 15).toNat ≤ 259) ∨
25    (op &&& 16 = 0 ∧ op &&& 64 ≠ 0) := by
26  decide +kernel
27
28set_option maxRecDepth 100000 in
29/-- All the `DISTS` symbols `w < 32`: a distance base (`w ≤ 29`: extra bits `≤ 13`, base `≥ 1`) or an invalid code
30(`30`, `31`). -/
31theorem dext_dbase_shape : ∀ w, w < 32 →
32    let op := (Zlib.Inftrees.dext.getD w 0).toUInt8
33    let v := Zlib.Inftrees.dbase.getD w 0
34    (op &&& 16 ≠ 0 ∧ (op &&& 15).toNat ≤ 13 ∧ 1 ≤ v.toNat) ∨ (op &&& 16 = 0 ∧ op &&& 64 ≠ 0) := by
35  decide +kernel
36
37/-- The leaf stored for a symbol `w < 288` of a `LENS` code is a `LenLeaf` after `d` dropped bits: a literal
38(`w < 256`, `op = 0`), the end of block (`w = 256`, `op = 96`), or `op = lext[w - 257]`, `val = lbase[w - 257]` for
39`257 ≤ w < 288`; the stored `bits` plus `d` is at most 15. -/
40theorem lenLeaf_of (d w : Nat) (hw : w < 288) (e : Code) (hb : e.bits.toNat + d ≤ 15)
41    (h0 : w < 256 → e.op = 0) (h1 : w = 256 → e.op = 96)
42    (h2 : 257 ≤ w → e.op = (Zlib.Inftrees.lext.getD (w - 257) 0).toUInt8 ∧
43      e.val = Zlib.Inftrees.lbase.getD (w - 257) 0) : LenLeaf d e := by
44  refine ⟨hb, ?_⟩
45  by_cases a : w < 256
46  · exact Or.inl (h0 a)
47  · by_cases b : w = 256
48    · have := h1 b; right; right; rw [this]; decide
49    · obtain ⟨ho, hv⟩ := h2 (by omega)
50      have := lext_lbase_shape w hw (by omega)
51      simp only at this
52      rw [ho, hv]
53      exact Or.inr this
54
55/-- The leaf stored for a symbol `w < 32` of a `DISTS` code is a `DistLeaf`: `op = dext[w]`, `val = dbase[w]`. -/
56theorem distLeaf_of (d w : Nat) (hw : w < 32) (e : Code) (hb : e.bits.toNat + d ≤ 15)
57    (h : e.op = (Zlib.Inftrees.dext.getD w 0).toUInt8 ∧ e.val = Zlib.Inftrees.dbase.getD w 0) : DistLeaf d e := by
58  refine ⟨hb, ?_⟩
59  have := dext_dbase_shape w hw
60  simp only at this
61  rw [h.1, h.2]
62  exact this
63
64/-- The entry `op = 64, val = 0` (invalid code) written for the empty code, and for the unused second cell of the
65single-symbol code, is a leaf of both tables. -/
66theorem invalid_leaf (d : Nat) (b : UInt8) (hb : b.toNat + d ≤ 15) :
67    LenLeaf d ⟨64, b, 0⟩ ∧ DistLeaf d ⟨64, b, 0⟩ :=
68  have h1 : (64 : UInt8) &&& 16 = 0 := by decide
69  have h2 : (64 : UInt8) &&& 64 ≠ 0 := by decide
70  ⟨⟨hb, Or.inr (Or.inr ⟨h1, h2⟩)⟩, ⟨hb, Or.inr ⟨h1, h2⟩⟩⟩
71
72/-- `here.bits = (unsigned char)(len - drop)`: with `drop ≤ len ≤ 15` it is `len - drop`, so that bits plus the bits
73`drop` already consumed is `len ≤ 15`. -/
74theorem bits_toNat {len drop : UInt32} (h1 : drop.toNat ≤ len.toNat) (h2 : len.toNat ≤ 15) :
75    (len - drop).toUInt8.toNat = len.toNat - drop.toNat := by
76  rw [UInt32.toNat_toUInt8, UInt32.toNat_sub_of_le _ _ (by rw [UInt32.le_iff_toNat_le]; exact h1)]
77  omega
78
79/-- The bits stored plus the bits already dropped are at most 15 (`LenLeaf`/`DistLeaf` first conjunct). -/
80theorem bits_add_drop {len drop : UInt32} (h1 : drop.toNat ≤ len.toNat) (h2 : len.toNat ≤ 15) :
81    (len - drop).toUInt8.toNat + drop.toNat ≤ 15 := by
82  rw [bits_toNat h1 h2]; omega
83
84end Zlib.Inftrees.Proofs.Cover