inflate.c.main.table4.lean

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

1import ZlibF.Proof.«inflate.c.main.table3»
2
3/-!
4# inflate.c: `case LENLENS:` -- the first loop (reading the code-length code lengths)
5-/
6
7namespace Zlib.Inflate.Proofs
8open C Zlib.Inflate Zlib.Inflate.Spec
9open Zlib.Inftrees (inflate_table)
10
11/-- The state record after the first `m` iterations of the first loop of `LENLENS`, reading from the stream `S`. -/
12def llSt (s : InflateState) (S : List Bool) (m : Nat) : InflateState :=
13  { s with «have» := s.«have» + m.toUInt32, lens := lensRead s.lens s.«have».toNat S m }
14
15theorem llSt_zero (s : InflateState) (S : List Bool) : llSt s S 0 = s := by
16  simp [llSt, lensRead]
17
18theorem tcU32_add_nat (a : UInt32) (m : Nat) (h : a.toNat + m < 2 ^ 32) : (a + m.toUInt32).toNat = a.toNat + m := by
19  rw [UInt32.toNat_add]
20  simp only [Nat.toUInt32_eq, UInt32.toNat_ofNat']
21  rw [Nat.mod_eq_of_lt (by omega : m < 2 ^ 32), Nat.mod_eq_of_lt h]
22
23theorem llSt_have (s : InflateState) (S : List Bool) (m : Nat) (hb : s.«have».toNat + m ≤ 19) :
24    (llSt s S m).«have».toNat = s.«have».toNat + m := by
25  simp only [llSt]
26  exact tcU32_add_nat _ _ (by omega)
27
28theorem llSt_succ (s : InflateState) (S : List Bool) (m : Nat) (hb : s.«have».toNat + m < 19) (v : UInt16)
29    (hv : v = (grp S m).toUInt16) :
30    { llSt s S m with «have» := (llSt s S m).«have» + 1, lens := (llSt s S m).lens.set! (orderNat (llSt s S m).«have».toNat) v } = llSt s S (m + 1) := by
31  have h1 := llSt_have s S m (by omega)
32  subst hv
33  simp only [llSt, lensRead] at h1 ⊢
34  congr 1
35  · rw [UInt32.add_assoc]; congr 1
36    show m.toUInt32 + 1 = UInt32.ofNat (m + 1)
37    rw [UInt32.ofNat_add]; rfl
38  · rw [h1]
39
40theorem tcSetI_same {h : Heap} {zs : Nat} {s : InflateState} (e : h.istates zs = some s) : setI h zs s = h := by
41  unfold setI
42  rw [upd_self _ _ _ e]
43
44/-- `l'` differs from `l` only in `next`, `have`, `hold`, `bits`. -/
45def TcRegShape (l l' : IL) : Prop := l' = { l with next := l'.next, have_ := l'.have_, hold := l'.hold, bits := l'.bits }
46
47theorem TcRegShape.refl (l : IL) : TcRegShape l l := rfl
48
49theorem TcRegShape.trans {l1 l2 l3 : IL} (a : TcRegShape l1 l2) (b : TcRegShape l2 l3) : TcRegShape l1 l3 := by
50  unfold TcRegShape at *
51  rw [b, a]
52
53theorem TcRegShape.drop {l l' : IL} (a : TcRegShape l l') (hold : UInt64) (bits : UInt32) :
54    TcRegShape l { l' with hold := hold, bits := bits } := by
55  unfold TcRegShape at *
56  rw [a]
57
58theorem tcStream_length {h : Heap} {l : IL} {bs : List UInt8} (B : BitInv h l bs) :
59    (stream l bs).length = l.bits.toNat + 8 * bs.length := by
60  unfold stream
61  simp [natBits_length, bytesBits_length]
62
63theorem tcDrop_drop (L : List α) (a b : Nat) : (L.drop a).drop b = L.drop (a + b) := by
64  rw [List.drop_drop]
65
66/-- **The first loop of `LENLENS`.** From `have ≤ ncode ≤ 19`, `M = min (ncode - have) (⌊|S| / 3⌋)` three-bit code lengths are
67read from the unread stream `S` into `lens[order[have + u]]`, `u < M`; `have` grows by `M`. If `M < ncode - have` the input
68ran out (`goto inf_leave`): every byte was pulled, fewer than 3 bits remain. -/
69theorem ll1_run {c : Ctx} {l : IL} {h : Heap} {zs : Nat} {s : InflateState} {bs : List UInt8}
70    (hc : c.st = some (.tab zs)) (hs : h.istates zs = some s) (hsz : s.lens.size = 320)
71    (hnc : s.ncode.toNat ≤ 19) (hhn : s.«have».toNat ≤ s.ncode.toNat) (B : BitInv h l bs) :
72    ∃ r l' j, runX (xwhile (llCond c) (llBody c)) l h =
73        .ok ((r, l'), setI h zs (llSt s (stream l bs) (min (s.ncode.toNat - s.«have».toNat) ((stream l bs).length / 3)))) ∧
74      j ≤ bs.length ∧ BitInv h l' (bs.drop j) ∧
75      stream l' (bs.drop j) = (stream l bs).drop (3 * min (s.ncode.toNat - s.«have».toNat) ((stream l bs).length / 3)) ∧
76      TcRegShape l l' ∧
77      (min (s.ncode.toNat - s.«have».toNat) ((stream l bs).length / 3) < s.ncode.toNat - s.«have».toNat →
78        r = .error Ex.leave ∧ l'.have_ = 0 ∧ j = bs.length ∧ l'.bits.toNat < 3) ∧
79      (min (s.ncode.toNat - s.«have».toNat) ((stream l bs).length / 3) = s.ncode.toNat - s.«have».toNat → r = .ok ()) := by
80  obtain ⟨n, hn⟩ : ∃ n, n = s.ncode.toNat - s.«have».toNat := ⟨_, rfl⟩
81  obtain ⟨S, hS⟩ : ∃ S, S = stream l bs := ⟨_, rfl⟩
82  obtain ⟨M, hM⟩ : ∃ M, M = min n (S.length / 3) := ⟨_, rfl⟩
83  rw [← hn, ← hS, ← hM]
84  have key := xwhileBrk_run (cond := llCond c) (body := (do llBody c; pure false : X Bool))
85    (fun k l1 h1 => ∃ m j, k + m = n ∧ m ≤ M ∧ j ≤ bs.length ∧ h1 = setI h zs (llSt s S m) ∧
86      BitInv h l1 (bs.drop j) ∧ stream l1 (bs.drop j) = S.drop (3 * m) ∧ TcRegShape l l1)
87    (fun r l1 h1 => ∃ j, j ≤ bs.length ∧ h1 = setI h zs (llSt s S M) ∧ BitInv h l1 (bs.drop j) ∧
88      stream l1 (bs.drop j) = S.drop (3 * M) ∧ TcRegShape l l1 ∧
89      (M < n → r = .error Ex.leave ∧ l1.have_ = 0 ∧ j = bs.length ∧ l1.bits.toNat < 3) ∧ (M = n → r = .ok ()))
90    (fun k l1 h1 hP => by
91      obtain ⟨m, j, hk, hmM, hj, hh1, B1, hS1, hsh1⟩ := hP
92      subst hh1
93      have hmn : m < n := by omega
94      have hb19 : s.«have».toNat + m < 19 := by omega
95      have hht := llSt_have s S m (by omega)
96      have ht : (setI h zs (llSt s S m)).istates zs = some (llSt s S m) := by simp
97      have hszt : (llSt s S m).lens.size = 320 := by simp [llSt, lensRead_size, hsz]
98      have hHt : (llSt s S m).«have».toNat < 19 := by omega
99      have hcond : runX (llCond c) l1 (setI h zs (llSt s S m)) = .ok ((.ok true, l1), setI h zs (llSt s S m)) := by
100        unfold llCond
101        rw [hc]
102        simp only [runX_bind, runX_lift, ldI_eq, ht, runX_pure]
103        have : (llSt s S m).«have» < (llSt s S m).ncode := by
104          rw [UInt32.lt_iff_toNat_lt, hht]
105          show _ < s.ncode.toNat
106          omega
107        simp [this]
108      obtain ⟨rr, l', jn, hrun, hjn, B', hS', hshape, hleave, hok⟩ :=
109        llBody_run (c := c) hc ht hszt hHt (B1.tc_setI zs _)
110      have hlen := tcStream_length B1
111      have hlen' := tcStream_length B'
112      refine ⟨l1, setI h zs (llSt s S m), hcond, ?_⟩
113      cases rr with
114      | error e =>
115        cases e with
116        | leave =>
117          obtain ⟨h1, h2, h3, hbody⟩ := hleave rfl
118          refine ⟨.error Ex.leave, l', setI h zs (llSt s S m), ?_, ?_⟩
119          · rw [runX_bind, hbody]
120          · -- the loop stops here: `m = M`
121            have hlenS : (S.drop (3 * m)).length = l'.bits.toNat := by
122              rw [← hS1, ← hS', tcStream_length B', h2, List.drop_length]; simp
123            simp only [List.length_drop] at hlenS
124            have hmM' : m = M := by omega
125            subst hmM'
126            have hjl : j + jn = bs.length := by
127              have : (bs.drop j).length = bs.length - j := by simp
128              omega
129            refine ⟨j + jn, by omega, rfl, ?_, ?_, ?_, fun _ => ⟨rfl, h1, hjl, h3⟩, fun hh => by omega⟩
130            · simpa [tcDrop_drop] using B'.tc_of_heap (h' := h) rfl rfl rfl
131            · rw [← hS1, ← hS']; simp [tcDrop_drop]
132            · exact hsh1.trans hshape
133        | ret v => exact absurd rfl (noRet_NEEDBITS 3 l1 _ _ l' _ hrun v)
134      | ok u =>
135        cases u
136        obtain ⟨h3, hbody⟩ := hok rfl
137        have hSlen : 3 ≤ (S.drop (3 * m)).length := by
138          have hh : (S.drop (3 * m)).length = l'.bits.toNat + 8 * ((bs.drop j).drop jn).length := by
139            rw [← hS1, ← hS']; exact tcStream_length B'
140          omega
141        simp only [List.length_drop] at hSlen
142        have hmM1 : m + 1 ≤ M := by
143          rw [hM]
144          apply Nat.le_min.mpr
145          constructor <;> omega
146        have hgrp : grp S m = l'.hold.toNat % 8 := by
147          unfold grp
148          rw [← hS1, ← hS']
149          simp only [stream, tcDrop_drop]
150          exact grp_head _ _ _ h3
151        have hbits7 : (l'.hold.toUInt32 &&& 7).toNat = grp S m := by
152          rw [hgrp]
153          have := BITS_toNat l' 3 (by decide)
154          rw [show ((1 : UInt32) <<< (3 : UInt32) - 1) = 7 by decide] at this
155          rw [this]
156          rfl
157        have hv : (l'.hold.toUInt32 &&& 7).toUInt16 = (grp S m).toUInt16 := by
158          show UInt16.ofNat (l'.hold.toUInt32 &&& 7).toNat = UInt16.ofNat (grp S m)
159          rw [hbits7]
160        obtain ⟨hB3, hS3, hsub3⟩ := DROPBITS_inv B' 3 h3 (by decide)
161        have hB3' : BitInv h { l' with hold := l'.hold >>> 3, bits := l'.bits - 3 } ((bs.drop j).drop jn) := by
162          have := hB3.tc_of_heap (h := setI h zs (llSt s S m)) (h' := h) rfl rfl rfl
163          exact this
164        refine ⟨.ok false, { l' with hold := l'.hold >>> 3, bits := l'.bits - 3 }, setI h zs (llSt s S (m + 1)), ?_, ?_⟩
165        · rw [runX_bind, hbody, ← llSt_succ s S m hb19 _ hv]
166          simp [runX_pure, setI_setI]
167        · have hjn' : jn ≤ bs.length - j := by simpa using hjn
168          refine ⟨m + 1, j + jn, by omega, hmM1, by omega, rfl, ?_, ?_, ?_⟩
169          · simpa [tcDrop_drop] using hB3'
170          · have hS3' : stream { l' with hold := l'.hold >>> 3, bits := l'.bits - 3 } ((bs.drop j).drop jn) =
171                (stream l' ((bs.drop j).drop jn)).drop 3 := hS3
172            rw [hS'] at hS3'
173            simp only [tcDrop_drop] at hS3' ⊢
174            rw [hS3', hS1, tcDrop_drop]
175            congr 1
176          · exact (hsh1.trans hshape).drop _ _)
177    (fun l1 h1 hP => by
178      obtain ⟨m, j, hk, hmM, hj, hh1, B1, hS1, hsh1⟩ := hP
179      subst hh1
180      have hmn : m = n := by omega
181      have hMm : M = m := by omega
182      have ht : (setI h zs (llSt s S m)).istates zs = some (llSt s S m) := by simp
183      have hht := llSt_have s S m (by omega)
184      have hcond : runX (llCond c) l1 (setI h zs (llSt s S m)) = .ok ((.ok false, l1), setI h zs (llSt s S m)) := by
185        unfold llCond
186        rw [hc]
187        simp only [runX_bind, runX_lift, ldI_eq, ht, runX_pure]
188        have : ¬ (llSt s S m).«have» < (llSt s S m).ncode := by
189          rw [UInt32.lt_iff_toNat_lt, hht]
190          show ¬ _ < s.ncode.toNat
191          omega
192        simp [this]
193      refine ⟨l1, _, hcond, j, hj, by rw [hMm], B1, by rw [hMm]; exact hS1, hsh1, fun hh => by omega, fun _ => rfl⟩)
194    (k := n) (l := l) (h := h)
195    ⟨0, 0, by omega, by omega, by omega, by rw [llSt_zero]; exact (tcSetI_same hs).symm, by simpa using B,
196      by simp [hS], TcRegShape.refl l⟩ (by unfold fuel; omega)
197  obtain ⟨r, l', h', hrun, j, hj, hh', B', hS', hsh, hl, hok⟩ := key
198  subst hh'
199  exact ⟨r, l', j, hrun, hj, B', hS', hsh, hl, hok⟩
200
201/-! ## The second loop: the remaining code lengths are 0 -/
202
203/-- The state record after the first `m` iterations of the second loop of `LENLENS`. -/
204def lzSt (s : InflateState) (m : Nat) : InflateState :=
205  { s with «have» := s.«have» + m.toUInt32, lens := lensZero s.lens s.«have».toNat m }
206
207theorem lzSt_zero (s : InflateState) : lzSt s 0 = s := by simp [lzSt, lensZero]
208
209theorem lzSt_have (s : InflateState) (m : Nat) (hb : s.«have».toNat + m ≤ 19) :
210    (lzSt s m).«have».toNat = s.«have».toNat + m := by
211  simp only [lzSt]
212  exact tcU32_add_nat _ _ (by omega)
213
214theorem lzSt_succ (s : InflateState) (m : Nat) (hb : s.«have».toNat + m < 19) :
215    { lzSt s m with «have» := (lzSt s m).«have» + 1, lens := (lzSt s m).lens.set! (orderNat (lzSt s m).«have».toNat) 0 } = lzSt s (m + 1) := by
216  have h1 := lzSt_have s m (by omega)
217  simp only [lzSt, lensZero] at h1 ⊢
218  congr 1
219  · rw [UInt32.add_assoc]; congr 1
220    show m.toUInt32 + 1 = UInt32.ofNat (m + 1)
221    rw [UInt32.ofNat_add]; rfl
222  · rw [h1]
223
224/-- One iteration of the second loop of `LENLENS`: `lens[order[have++]] = 0`, in a state with `have < 19`. -/
225theorem lzBody_run {c : Ctx} {l : IL} {h : Heap} {zs : Nat} {t : InflateState}
226    (hc : c.st = some (.tab zs)) (ht : h.istates zs = some t) (hsz : t.lens.size = 320) (hH : t.«have».toNat < 19) :
227    runX (lzBody c) l h = .ok ((.ok (), l),
228      setI h zs { t with «have» := t.«have» + 1, lens := t.lens.set! (orderNat t.«have».toNat) 0 }) := by
229  have ho : orderNat t.«have».toNat < 19 := order_lt _ hH
230  have hoa := orderAt_run (setI h zs { t with «have» := t.«have» + 1 }) t.«have» hH
231  have hadd := tcAdd_lens (h := setI h zs { t with «have» := t.«have» + 1 }) (zs := zs)
232    (t := { t with «have» := t.«have» + 1 }) (k := (order[t.«have».toNat]!).toNat) (by simp)
233    (by have := ho; unfold orderNat at this; simp [hsz]; omega)
234  have hst := tcStore_lens (h := setI h zs { t with «have» := t.«have» + 1 }) (zs := zs)
235    (t := { t with «have» := t.«have» + 1 }) (k := (order[t.«have».toNat]!).toNat) (0 : UInt16)
236    (by simp) (by have := ho; unfold orderNat at this; simp [hsz]; omega)
237  unfold lzBody
238  rw [hc]
239  simp at hst
240  simp [runX_bind, runX_lift, ldI_eq, ht, wrI_eq, hoa, hadd, hst, lensP, orderNat]
241
242/-- **The second loop of `LENLENS`**: `while (have < 19) lens[order[have++]] = 0`, from `have ≤ 19`: the registers are unchanged,
243`have` becomes 19 (at least) and the entries `lens[order[have ..]]` are 0 (`lzSt`). -/
244theorem lz_run {c : Ctx} {l : IL} {h : Heap} {zs : Nat} {s : InflateState}
245    (hc : c.st = some (.tab zs)) (hs : h.istates zs = some s) (hsz : s.lens.size = 320)
246    (hHv : s.«have».toNat ≤ 19) :
247    runX (xwhile (lzCond c) (lzBody c)) l h = .ok ((.ok (), l), setI h zs (lzSt s (19 - s.«have».toNat))) := by
248  obtain ⟨n, hn⟩ : ∃ n, n = 19 - s.«have».toNat := ⟨_, rfl⟩
249  rw [← hn]
250  have key := xwhileBrk_run (cond := lzCond c) (body := (do lzBody c; pure false : X Bool))
251    (fun k l1 h1 => ∃ m, k + m = n ∧ h1 = setI h zs (lzSt s m) ∧ l1 = l)
252    (fun r l1 h1 => h1 = setI h zs (lzSt s n) ∧ l1 = l ∧ r = .ok ())
253    (fun k l1 h1 hP => by
254      obtain ⟨m, hk, hh1, hl1⟩ := hP
255      subst h1 l1
256      have hb19 : s.«have».toNat + m < 19 := by omega
257      have hht := lzSt_have s m (by omega)
258      have ht : (setI h zs (lzSt s m)).istates zs = some (lzSt s m) := by simp
259      have hszt : (lzSt s m).lens.size = 320 := by simp [lzSt, lensZero_size, hsz]
260      have hcond : runX (lzCond c) l (setI h zs (lzSt s m)) = .ok ((.ok true, l), setI h zs (lzSt s m)) := by
261        unfold lzCond
262        rw [hc]
263        simp only [runX_bind, runX_lift, ldI_eq, ht, runX_pure]
264        have : (lzSt s m).«have» < 19 := by
265          rw [UInt32.lt_iff_toNat_lt, hht]
266          show _ < 19
267          omega
268        simp [this]
269      refine ⟨l, setI h zs (lzSt s m), hcond, .ok false, l, setI h zs (lzSt s (m + 1)), ?_, ?_⟩
270      · rw [runX_bind, lzBody_run hc ht hszt (by omega), ← lzSt_succ s m hb19]
271        simp [runX_pure, setI_setI]
272      · exact ⟨m + 1, by omega, rfl, rfl⟩)
273    (fun l1 h1 hP => by
274      obtain ⟨m, hk, hh1, hl1⟩ := hP
275      subst h1 l1
276      have hmn : m = n := by omega
277      subst hmn
278      have ht : (setI h zs (lzSt s m)).istates zs = some (lzSt s m) := by simp
279      have hht := lzSt_have s m (by omega)
280      refine ⟨l, setI h zs (lzSt s m), ?_, rfl, rfl, rfl⟩
281      unfold lzCond
282      rw [hc]
283      simp only [runX_bind, runX_lift, ldI_eq, ht, runX_pure]
284      have : ¬ (lzSt s m).«have» < 19 := by
285        rw [UInt32.lt_iff_toNat_lt, hht]
286        show ¬ _ < 19
287        omega
288      simp [this])
289    (k := n) (l := l) (h := h) ⟨0, by omega, by rw [lzSt_zero]; exact (tcSetI_same hs).symm, rfl⟩ (by unfold fuel; omega)
290  obtain ⟨r, l', h', hrun, hh', hl', hr⟩ := key
291  subst hh' hl' hr
292  exact hrun
293
294end Zlib.Inflate.Proofs