InflateTableCoverage.lean

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

1import ZlibF.Math.InflateTableGeometry
2import ZlibF.Proof.«inftrees.c.cover.group»
3
4/-! Every cell of a complete canonical table belongs to an actual write.
5Subtable descriptors agree throughout a prefix group. Their offsets fit
6the 16-bit link field; this follows from the layout rather than an array
7size restriction on the caller. -/
8
9namespace Zlib.Inftrees.Proofs
10open Zlib.Inftrees.Canon
11set_option autoImplicit false
12
13theorem desc_same_group {ls : List Nat} {root mx i j : Nat}
14    (hi : i < nz ls) (hj : j < nz ls) (li : root < L ls i) (lj : root < L ls j)
15    (same : grp ls root i = grp ls root j) : desc ls root mx i = desc ls root mx j := by
16  suffices ordered : ∀ a b, a ≤ b → b < nz ls → root < L ls a →
17      grp ls root a = grp ls root b → desc ls root mx a = desc ls root mx b by
18    rcases Nat.le_total i j with le | le
19    · exact ordered i j le hj li same
20    · exact (ordered j i le hi lj same.symm).symm
21  intro a b order bound long equal
22  induction b with
23  | zero => have : a = 0 := by omega
24            subst a
25            rfl
26  | succ b ih =>
27    by_cases last : a = b + 1
28    · subst a
29      rfl
30    have before : a ≤ b := by omega
31    have g1 := grp_mono ls root before
32    have g2 := grp_mono ls root (by omega : b ≤ b + 1)
33    have l := L_mono ls before (by omega : b < nz ls)
34    have noStart : ¬ startsAt ls root b := by
35      rintro ⟨_, short | different⟩
36      · omega
37      · apply different
38        omega
39    rw [desc_succ_of_not ls root mx b noStart]
40    exact ih before (by omega) (by omega)
41
42/-- A complete subtable has no unwritten holes. The returned replica is
43one of the addresses retained by the actual constructor's Written clause. -/
44theorem long_subtable_replica {ls : List Nat} {root mx i cell : Nat}
45    (code : CompleteCode ls root mx) (index : i < nz ls) (long : root < L ls i)
46    (inside : cell < 2 ^ (desc ls root mx i).curr) :
47    ∃ j replica, j < nz ls ∧ desc ls root mx j = desc ls root mx i ∧
48      replica < gReps ls root mx j ∧
49      gAddr ls root mx j replica = (desc ls root mx i).base + cell := by
50  obtain ⟨a, order, start, group, drop, width, _⟩ :=
51    desc_long (mx := mx) code.min_le index long
52  have widths := width_spec ls (by omega : a + 1 < nz ls) code.mx_le
53    start.1 (code.L_le_mx (by omega))
54  have fits : root + (desc ls root mx i).curr ≤ 15 := by
55    have := code.mx_le
56    rw [width]
57    omega
58  have covers : ∀ j, Cover.Group ls root (grp ls root i) j →
59      L ls j ≤ root + (desc ls root mx i).curr := by
60    intro j member
61    have same := desc_same_group (mx := mx) member.1 index member.2.1 long member.2.2
62    have fit := desc_fits code member.1
63    rw [same, drop] at fit
64    omega
65  obtain ⟨j, member, ⟨replica, bound, address⟩, _⟩ :=
66    Cover.group_cover_idx code.complete (Nat.le_trans code.root_le code.mx_le)
67      (j0 := i) ⟨index, long, rfl⟩ fits covers inside
68  have same := desc_same_group (mx := mx) member.1 index member.2.1 long member.2.2
69  refine ⟨j, replica, member.1, same, ?_, ?_⟩
70  · unfold gReps
71    rw [same, drop]
72    rw [show (desc ls root mx i).curr - (L ls j - root) =
73      root + (desc ls root mx i).curr - L ls j by have := member.2.1; omega]
74    exact bound
75  · unfold gAddr
76    rw [same, drop, address, Nat.add_assoc, Nat.mul_comm replica]
77
78/-- The table budget follows the monotone prefix-group number. -/
79theorem desc_group_budget {ls : List Nat} {root mx : Nat}
80    (code : CompleteCode ls root mx) {i : Nat} (index : i < nz ls) :
81    (desc ls root mx i).used ≤ 2 ^ root + (grp ls root i + 1) * 2 ^ (mx - root) := by
82  induction i with
83  | zero => simp only [desc]; omega
84  | succ i ih =>
85    have previous := ih (by omega)
86    by_cases start : startsAt ls root i
87    · have width := width_spec ls index code.mx_le start.1 (code.L_le_mx index)
88      have power : 2 ^ Canon.width ls (i + 1) root mx ≤ 2 ^ (mx - root) :=
89        Nat.pow_le_pow_right (by omega) (by omega)
90      rw [desc_succ_of_starts ls root mx i start]
91      dsimp only
92      by_cases short : L ls i ≤ root
93      · rw [desc_short ls (by omega) short] at previous ⊢
94        dsimp only [desc]
95        have group : 1 ≤ grp ls root (i + 1) + 1 := by omega
96        have budget := Nat.mul_le_mul_right (2 ^ (mx - root)) group
97        omega
98      · have increasing := grp_mono ls root (by omega : i ≤ i + 1)
99        have strict : grp ls root i + 1 ≤ grp ls root (i + 1) := by
100          rcases start.2 with impossible | different
101          · contradiction
102          · omega
103        have budget := Nat.mul_le_mul_right (2 ^ (mx - root)) strict
104        rw [Nat.add_mul, Nat.one_mul]
105        omega
106    · rw [desc_succ_of_not ls root mx i start]
107      have monotone := Nat.mul_le_mul_right (2 ^ (mx - root))
108        (Nat.succ_le_succ (grp_mono ls root (by omega : i ≤ i + 1)))
109      change (grp ls root i + 1) * 2 ^ (mx - root) ≤
110        (grp ls root (i + 1) + 1) * 2 ^ (mx - root) at monotone
111      omega
112
113/-- Link offsets do not truncate when stored as unsigned short. -/
114theorem desc_base_lt_u16 {ls : List Nat} {root mx : Nat}
115    (code : CompleteCode ls root mx) {i : Nat} (index : i < nz ls) :
116    (desc ls root mx i).base < 2 ^ 16 := by
117  have budget := desc_group_budget code index
118  have groups := Nat.mul_le_mul_right (2 ^ (mx - root)) (grp_lt code index)
119  change (grp ls root i + 1) * 2 ^ (mx - root) ≤
120    2 ^ root * 2 ^ (mx - root) at groups
121  have factor : 2 ^ root * 2 ^ (mx - root) = 2 ^ mx := by
122    rw [← Nat.pow_add]
123    congr 1
124    have := code.root_le
125    omega
126  rw [factor] at groups
127  have rootPower : 2 ^ root ≤ 2 ^ 15 :=
128    Nat.pow_le_pow_right (by omega) (Nat.le_trans code.root_le code.mx_le)
129  have maxPower : 2 ^ mx ≤ 2 ^ 15 := Nat.pow_le_pow_right (by omega) code.mx_le
130  have positive := Nat.two_pow_pos (desc ls root mx i).curr
131  rw [desc_used] at budget
132  omega
133
134end Zlib.Inftrees.Proofs