trees.c.heap.gbfix.lean

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

1import ZlibF.Proof.«trees.c.heap.gbp1»
2
3/-!
4# trees.c: `gen_bitlen`, the repair of over-long codes
5
6`do { bits = max_length-1; while (bl_count[bits] == 0) bits--; bl_count[bits]--; bl_count[bits+1] += 2;
7bl_count[max_length]--; overflow -= 2; } while (overflow > 0);` on the counts `c b = bl_count[b]`.
8`fixStep` is one round; the pure part is copied from the earlier attempt (`GenBitlenFixX.lean`).
9-/
10
11namespace Zlib.Trees.Proofs
12open C Zlib.Trees Zlib.Trees.Proofs.GB
13
14/-- Point update of a count function. -/
15def updN (f : Nat → Nat) (a v : Nat) : Nat → Nat := fun x => if x = a then v else f x
16
17/-- The deepest `b' ≤ b` with `c b' ≠ 0` (`0` if there is none). -/
18def deepestX (c : Nat → Nat) : Nat → Nat
19  | 0 => 0
20  | b + 1 => if c (b + 1) ≠ 0 then b + 1 else deepestX c b
21
22theorem deepestX_eq (c : Nat → Nat) : ∀ b b', 1 ≤ b' → b' ≤ b → c b' ≠ 0 → (∀ y, b' < y → y ≤ b → c y = 0) →
23    deepestX c b = b'
24  | 0, b', h1, h2, _, _ => by omega
25  | b + 1, b', h1, h2, h3, h4 => by
26    unfold deepestX
27    by_cases e : b' = b + 1
28    · subst e; rw [ite_eq_left h3]
29    · rw [ite_eq_right (by rw [h4 (b + 1) (by omega) (Nat.le_refl _)]; simp)]
30      exact deepestX_eq c b b' h1 (by omega) h3 (fun y a b'' => h4 y a (by omega))
31
32/-- One round of the fix-up on the counts. -/
33def fixStep (L : Nat) (c : Nat → Nat) : Nat → Nat :=
34  let b := deepestX c (L - 1)
35  let c1 := updN c b (c b - 1)
36  let c2 := updN c1 (b + 1) (c1 (b + 1) + 2)
37  updN c2 L (c2 L - 1)
38
39/-- `M` rounds. -/
40def fixIter (L : Nat) : Nat → (Nat → Nat) → (Nat → Nat)
41  | 0, c => c
42  | M + 1, c => fixIter L M (fixStep L c)
43
44theorem fixIter_succ' (L : Nat) : ∀ M c, fixIter L (M + 1) c = fixStep L (fixIter L M c)
45  | 0, _ => rfl
46  | M + 1, c => by
47    show fixIter L (M + 1) (fixStep L c) = _
48    rw [fixIter_succ' L M (fixStep L c)]; rfl
49
50
51
52/-- `bl_count` of `e` holds the counts `c`. -/
53def BcIs (e : DeflateState) (c : Nat → Nat) : Prop :=
54  e.bl_count.size = 16 ∧ ∀ b, b < 16 → e.bl_count[b]! = UInt16.ofNat (c b)
55
56/-- The search `while (bl_count[bits] == 0) bits--`. -/
57theorem ws_gbSearch {h0 : Heap} {id : Nat} (e : DeflateState) (c : Nat → Nat) (hB : BcIs e c)
58    (hsmall : ∀ b, c b < 65536) (bits : Int32) (b : Nat) (hb : bits.toInt = b) (hb15 : b < 16)
59    (hex : ∃ b0, 1 ≤ b0 ∧ b0 ≤ b ∧ c b0 ≠ 0) :
60    WS h0 id (cwhile (σ := Int32)
61        (fun b => do pure (decide ((← Ptr.index (Ptr.ref (WRef.dstate_bl_count id) 0) b.toInt) == 0), b))
62        (fun b => isub b 1) bits) e (fun bits' e' => e' = e ∧ ∃ b' : Nat, bits'.toInt = b' ∧ 1 ≤ b' ∧ b' ≤ b ∧
63          c b' ≠ 0 ∧ ∀ y, b' < y → y ≤ b → c y = 0) := by
64  refine WS.cwhile2 (id := id)
65    (fun (bits' : Int32) e' => e' = e ∧ ∃ x : Nat, bits'.toInt = x ∧ x ≤ b ∧ (∃ b0, 1 ≤ b0 ∧ b0 ≤ x ∧ c b0 ≠ 0) ∧
66      ∀ y, x < y → y ≤ b → c y = 0)
67    (fun (bits' : Int32) _ => bits'.toInt.toNat)
68    (fun (bits' : Int32) e' => e' = e ∧ ∃ b' : Nat, bits'.toInt = b' ∧ 1 ≤ b' ∧ b' ≤ b ∧
69          c b' ≠ 0 ∧ ∀ y, b' < y → y ≤ b → c y = 0) ?_ ⟨rfl, b, hb, Nat.le_refl _, hex, fun y a b' => by omega⟩
70    (by show bits.toInt.toNat < fuel; rw [hb]; simp only [Int.toNat_natCast, fuel]; omega)
71  rintro bits' e' ⟨rfl, x, hx, hxb, ⟨b0, h1, h2, h3⟩, hdeep⟩
72  have h1i : (1 : Int32).toInt = 1 := rfl
73  have hv : WS h0 id (Ptr.index (Ptr.ref (WRef.dstate_bl_count id) 0) bits'.toInt) e'
74      (fun v e'' => v = UInt16.ofNat (c x) ∧ e'' = e') := by
75    refine WS.mono (ws_index_blc bits'.toInt (by omega) (by rw [hB.1]; omega)) ?_
76    rintro v e'' ⟨hv, rfl⟩
77    refine ⟨?_, rfl⟩
78    rw [hv, show bits'.toInt.toNat = x by omega]; exact hB.2 x (by omega)
79  refine WS.bind' hv fun v e1 ⟨hv1, he1⟩ => ?_
80  subst e1; subst hv1
81  by_cases hz : c x = 0
82  · have hb0x : b0 < x := by
83      by_cases e : b0 = x
84      · subst e; exact absurd hz h3
85      · omega
86    refine WS.pure' (Or.inr ⟨?_, ?_⟩)
87    · simp [hz]
88    · refine WS.mono (ws_isub bits' 1 (by omega) (by omega)) ?_
89      rintro b2 e2 ⟨hb2, rfl⟩
90      refine ⟨⟨rfl, x - 1, by omega, by omega, ⟨b0, h1, by omega, h3⟩, fun y a b' => ?_⟩, ?_⟩
91      · by_cases e : y = x
92        · rw [e]; exact hz
93        · exact hdeep y (by omega) b'
94      · show b2.toInt.toNat < bits'.toInt.toNat
95        omega
96  · refine WS.pure' (Or.inl ⟨?_, ?_⟩)
97    · have : (UInt16.ofNat (c x) == 0) = false := by
98        simp only [beq_eq_false_iff_ne, ne_eq]
99        intro e; apply hz
100        have := congrArg UInt16.toNat e
101        rw [UInt16.toNat_ofNat'] at this; simp at this; have := hsmall x; omega
102      simp [this]
103    · refine ⟨rfl, x, hx, ?_, hxb, hz, hdeep⟩
104      by_cases e : b0 = x
105      · omega
106      · omega
107
108
109theorem c_le_of {L NL : Nat} {c : Nat → Nat} (hc0 : ∀ b, L < b → c b = 0) (ht : rs c (L + 1) = NL) (x : Nat) :
110    c x ≤ NL := by
111  by_cases hx : x ≤ L
112  · rw [← ht]; exact le_rs (F := c) (by omega)
113  · rw [hc0 x (by omega)]; omega
114
115theorem u16_sub1 (a : Nat) (h1 : 1 ≤ a) : UInt16.ofNat a - 1 = UInt16.ofNat (a - 1) := by
116  have e : UInt16.ofNat a = UInt16.ofNat (a - 1) + 1 := by
117    rw [show (1 : UInt16) = UInt16.ofNat 1 from rfl, ← UInt16.ofNat_add]; congr 1; omega
118  rw [e, UInt16.add_sub_cancel]
119
120theorem u16_add_k (a k : Nat) : UInt16.ofNat a + (UInt16.ofNat k) = UInt16.ofNat (a + k) := by
121  rw [UInt16.ofNat_add]
122
123theorem BcIs_set {e : DeflateState} {c : Nat → Nat} (hB : BcIs e c) (i : Nat) (hi : i < 16) (f : UInt16 → UInt16)
124    (v : Nat) (hf : f (UInt16.ofNat (c i)) = UInt16.ofNat v) :
125    BcIs { e with bl_count := e.bl_count.set! i (f e.bl_count[i]!) } (updN c i v) := by
126  refine ⟨by simp [size_set!, hB.1], fun b hb => ?_⟩
127  show (e.bl_count.set! i (f e.bl_count[i]!))[b]! = _
128  rw [getD_set _ _ _ _ (by rw [hB.1]; exact hi)]
129  by_cases eb : b = i
130  · subst eb; simp only [ite_true, updN]; rw [hB.2 b hb, hf]
131  · simp only [eb, ite_false, updN]; exact hB.2 b hb
132
133/-- Invariant of the repair loop with `R` rounds left. -/
134def FixInvX (L NL R : Nat) (ov : Int32) (c : Nat → Nat) (e1 e : DeflateState) : Prop :=
135  ov.toInt = 2 * (R : Int) ∧ BcIs e c ∧ c 0 = 0 ∧ (∀ b, L < b → c b = 0) ∧ kc c L = 2 ^ L + R ∧
136    R + 1 ≤ c L ∧ rs c (L + 1) = NL ∧ ∃ Bc, e = { e1 with bl_count := Bc }
137
138theorem ws_gbFixRound {h0 : Heap} {id : Nat} (e1 : DeflateState) (ml : Int32) (L NL R : Nat) (hmlv : ml.toInt = L) (hL1 : 1 ≤ L)
139    (hL15 : L ≤ 15) (hNL : NL ≤ 2 ^ L) (hNL2 : NL ≤ 1000) (ov : Int32) (c : Nat → Nat) (e : DeflateState)
140    (hI : FixInvX L NL (R + 1) ov c e1 e) :
141    WS h0 id (gbFix (Sp id) ml ov) e (fun ov' e' => FixInvX L NL R ov' (fixStep L c) e1 e') := by
142  obtain ⟨ho, hB, hc0, hchi, hk, hcL, htot, Bc0, hex⟩ := hI
143  have hle : ∀ x, c x ≤ NL := c_le_of hchi htot
144  have hsmall : ∀ x, c x < 65536 := fun x => by have := hle x; omega
145  obtain ⟨b0, hb01, hb0L, hb0⟩ := exists_short c L (R + 1) (by omega) hk (by omega) hc0
146  have h1i : (1 : Int32).toInt = 1 := rfl
147  have h2i : (2 : Int32).toInt = 2 := rfl
148  have h2p : (2 : Int) ^ L = ((2 ^ L : Nat) : Int) := by push_cast; rfl
149  have hp15 : 2 ^ L ≤ 2 ^ 15 := Nat.pow_le_pow_right (by omega) hL15
150  unfold gbFix
151  refine WS.bind' (ws_isub ml 1 (by omega) (by omega)) fun bits0 e1 ⟨hbits0, he1⟩ => ?_
152  subst e1
153  refine WS.bind' ws_pBlCount fun bc e1 ⟨hbc, he1⟩ => ?_
154  subst e1; subst hbc
155  refine WS.bind' (ws_gbSearch e c hB hsmall bits0 (L - 1) (by omega) (by omega) ⟨b0, hb01, by omega, hb0⟩)
156    fun bits e1 ⟨he1, b, hbI, hb1, hbL, hcb, hdeep⟩ => ?_
157  subst e1
158  have hdb : deepestX c (L - 1) = b := deepestX_eq c (L - 1) b hb1 hbL hcb hdeep
159  have hcb1 : 1 ≤ c b := by have : c b ≠ 0 := hcb; omega
160  have e2lit : (2 : UInt16) = UInt16.ofNat 2 := rfl
161  have hbl : bits.toInt.toNat = b := by omega
162  -- bl_count[b]--
163  refine WS.bind' (ws_index_blc bits.toInt (by omega) (by rw [hB.1]; omega)) fun v1 e1 ⟨hv1, he1⟩ => ?_
164  subst e1; subst hv1
165  refine WS.bind' (ws_setAt_blc bits.toInt _ (by omega) (by rw [hB.1]; omega)) fun _ e1 he1 => ?_
166  subst e1
167  rw [hbl]
168  have hB1 : BcIs { e with bl_count := e.bl_count.set! b (e.bl_count[b]! - 1) } (updN c b (c b - 1)) :=
169    BcIs_set hB b (by omega) (fun x => x - 1) (c b - 1) (u16_sub1 _ hcb1)
170  -- bl_count[bits + 1] += 2
171  refine WS.bind' (ws_iadd bits 1 (by omega) (by omega)) fun b1 e1 ⟨hb1', he1⟩ => ?_
172  subst e1
173  have hbl1 : b1.toInt.toNat = b + 1 := by omega
174  refine WS.bind' (ws_index_blc b1.toInt (by omega) (by rw [(hB1).1]; omega)) fun v2 e1 ⟨hv2, he1⟩ => ?_
175  subst e1; subst hv2
176  refine WS.bind' (ws_setAt_blc b1.toInt _ (by omega) (by rw [(hB1).1]; omega)) fun _ e1 he1 => ?_
177  subst e1
178  rw [hbl1]
179  have hle1 := hle (b + 1)
180  have hB2 := BcIs_set hB1 (b + 1) (by omega) (fun x => x + 2) (updN c b (c b - 1) (b + 1) + 2)
181    (by rw [e2lit, u16_add_k])
182  -- bl_count[max_length]--
183  have hc1 : ∀ x, x ≠ b → updN c b (c b - 1) x = c x := fun x hx => by simp [updN, hx]
184  have hc1b : updN c b (c b - 1) (b + 1) = c (b + 1) := hc1 _ (by omega)
185  have hc2L : 1 ≤ updN (updN c b (c b - 1)) (b + 1) (updN c b (c b - 1) (b + 1) + 2) L := by
186    by_cases e : L = b + 1
187    · simp [updN, e]
188    · simp only [updN, e, ite_false, show L ≠ b by omega]; omega
189  refine WS.bind' (ws_index_blc ml.toInt (by omega) (by rw [(hB2).1]; omega)) fun v3 e1 ⟨hv3, he1⟩ => ?_
190  subst e1; subst hv3
191  refine WS.bind' (ws_setAt_blc ml.toInt _ (by omega) (by rw [(hB2).1]; omega)) fun _ e1 he1 => ?_
192  subst e1
193  rw [show ml.toInt.toNat = L by omega]
194  have hB3 := BcIs_set hB2 L (by omega) (fun x => x - 1)
195    (updN (updN c b (c b - 1)) (b + 1) (updN c b (c b - 1) (b + 1) + 2) L - 1) (u16_sub1 _ hc2L)
196  have hleL' := hle L
197  refine WS.mono (ws_isub ov 2 (by omega) (by omega)) ?_
198  rintro ov' e' ⟨hov', rfl⟩
199  have hfs : fixStep L c = updN (updN (updN c b (c b - 1)) (b + 1) (updN c b (c b - 1) (b + 1) + 2)) L
200      (updN (updN c b (c b - 1)) (b + 1) (updN c b (c b - 1) (b + 1) + 2) L - 1) := by
201    unfold fixStep; rw [hdb]
202  rw [hfs]
203  have hrel : ∀ x ≤ L, updN (updN (updN c b (c b - 1)) (b + 1) (updN c b (c b - 1) (b + 1) + 2)) L
204      (updN (updN c b (c b - 1)) (b + 1) (updN c b (c b - 1) (b + 1) + 2) L - 1) x + ind (x = b) + ind (x = L) =
205      c x + 2 * ind (x = b + 1) := by
206    intro x hx
207    simp only [updN, ind]; repeat' split <;> (try subst_vars)
208    all_goals omega
209  obtain ⟨hr1, hr2⟩ := round_kraft c _ L b (by omega) hrel
210  have hleL := hle L
211  refine ⟨by rw [hov', h2i, ho]; omega, hB3, ?_, ?_, ?_, ?_, ?_, _, by rw [hex]⟩
212  · simp only [updN]; repeat' split <;> (try subst_vars)
213    all_goals omega
214  · intro x hx
215    have := hchi x hx
216    simp only [updN]; repeat' split <;> (try subst_vars)
217    all_goals omega
218  · omega
219  · by_cases e : L = b + 1
220    · subst e; simp [updN]; omega
221    · simp [updN, e, show L ≠ b by omega]; omega
222  · omega
223
224
225/-- **The repair loop.** From `R + 1` rounds left, the loop ends with the counts `fixIter L (R + 1) c0`. -/
226theorem ws_gbFixLoop {h0 : Heap} {id : Nat} (e1 : DeflateState) (ml : Int32) (L NL R : Nat) (hmlv : ml.toInt = L) (hL1 : 1 ≤ L)
227    (hL15 : L ≤ 15) (hNL : NL ≤ 2 ^ L) (hNL2 : NL ≤ 1000) (ov : Int32) (c0 : Nat → Nat) (e : DeflateState)
228    (hI : FixInvX L NL (R + 1) ov c0 e1 e) :
229    WS h0 id (cdoWhile (σ := Int32) (gbFix (Sp id) ml)
230      (fun overflow => pure (decide (overflow.toInt > 0), overflow)) ov) e
231      (fun o e' => FixInvX L NL 0 o (fixIter L (R + 1) c0) e1 e') := by
232  refine WS.cdoWhile2 (id := id)
233    (fun (o : Int32) e' => ∃ k, k ≤ R ∧ FixInvX L NL (k + 1) o (fixIter L (R - k) c0) e1 e')
234    (fun (o : Int32) _ => o.toInt.toNat)
235    (fun (o : Int32) e' => FixInvX L NL 0 o (fixIter L (R + 1) c0) e1 e') ?_
236    ⟨R, Nat.le_refl _, by rw [Nat.sub_self]; exact hI⟩ (by
237      have := hI.1; simp only [fuel]; have := ov.toInt_le
238      have e : Int32.maxValue.toInt = 2147483647 := by decide
239      omega)
240  rintro o e' ⟨k, hk, hIk⟩
241  refine WS.mono (ws_gbFixRound (h0 := h0) (id := id) e1 ml L NL k hmlv hL1 hL15 hNL hNL2 o _ e' hIk) ?_
242  rintro o' e'' hI'
243  refine WS.pure' ?_
244  have ho' := hI'.1
245  have ho := hIk.1
246  cases k with
247  | zero =>
248    refine Or.inl ⟨?_, ?_⟩
249    · simp only [decide_eq_false_iff_not]; omega
250    · rw [← fixIter_succ'] at hI'; simpa using hI'
251  | succ k' =>
252    refine Or.inr ⟨?_, ⟨k', by omega, ?_⟩, ?_⟩
253    · simp only [decide_eq_true_eq]; omega
254    · rw [← fixIter_succ'] at hI'
255      rw [show R - k' = R - (k' + 1) + 1 by omega]; exact hI'
256    · show o'.toInt.toNat < o.toInt.toNat
257      omega
258
259end Zlib.Trees.Proofs