inftrees.c.content.tail.lean

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

1import ZlibF.Proof.«inftrees.c.main»
2import ZlibF.Proof.«inftrees.c.final-layout»
3
4namespace Zlib.Inftrees.Proofs
5open C Zlib.Inftrees Zlib.Inftrees.Spec
6set_option autoImplicit false
7
8def EndFields (e : Env) (s : TS) : Prop :=
9  DescB e (e.m - 1) s ∧ s.drop.toNat = (e.D (e.m - 1)).drop ∧
10    s.len.toNat = e.mx ∧ (e.m = 1 → e.mx = 1 → s.huff = 1)
11
12def TailDetails (e : Env) (r : Int32 × CodePtr × UInt32) (ca : Array Code) : Prop :=
13  r.1 = 0 → ∃ used, r.2.1 = .ref e.rc (e.oc + used) ∧
14    used = (e.D (e.m - 1)).used ∧
15    (e.m = 1 → e.mx = 1 → ca[e.oc + 1]? = some ⟨64, 1, 0⟩)
16
17theorem itTail_cells_wp (e : Env) (ca : Array Code) (count : Array UInt16) (bits min : UInt32) (left : Int32)
18    (hcnt : CountOK e count 0) (hmin : min.toNat = e.l 0) (hsz : e.oc + e.cap ≤ ca.size) :
19    Wp (itTail e.c.type e.c.lens e.c.table bits e.c.work count e.c.max min e.c.root left e.c.base e.c.extra
20        e.c.match_) (e.hc ca)
21      (fun r h' => ∃ ca', h' = e.hc ca' ∧ FrameCA e ca ca' ∧
22        ((r.1 = 0 ∧ ∃ u, u ≤ e.cap ∧ r.2.1 = .ref e.rc (e.oc + u) ∧ r.2.2 = e.c.root) ∨
23         (r.1 = 1 ∧ r.2.1 = e.c.table ∧ r.2.2 = bits)) ∧ (r.1 = 1 → e.c.type ≠ CODES) ∧
24        (r.1 = 0 → Cont e e.m e.m ca') ∧ TailDetails e r ca') := by
25  have hR1 := e.h_R1
26  have hroot := e.h_root
27  have hpos := e.h_pos
28  have hmxle : e.mx ≤ 15 := by
29    have := lenAt_bounds (f := e.f) (n := e.n) (show e.m - 1 < Tc e.f e.n 15 by unfold Env.m; omega)
30    exact this.2
31  have hRmx := e.h_Rmx
32  have hm15 : e.m = Tc e.f e.n 15 := rfl
33  have hmx15 : e.mx = mxl e.f e.n := rfl
34  have hR32 : e.c.root.toNat < 32 := by omega
35  unfold itTail
36  apply Wp.bind' (Q := fun r h' => r = 1 <<< e.c.root ∧ h' = e.hc ca) (Wp.pure_eq (shl32_eq hR32) ⟨rfl, rfl⟩)
37  rintro used0 h' ⟨rfl, rfl⟩
38  have hu0 : ((1 : UInt32) <<< e.c.root).toNat = 2 ^ e.R := by rw [u32_shl1 hR32, hroot]
39  by_cases hb : tooBig e.c.type (1 <<< e.c.root) = true
40  · rw [ite_eq_left hb]
41    exact Wp.pure' ⟨ca, rfl, ⟨rfl, fun _ _ => rfl⟩, Or.inr ⟨rfl, rfl, rfl⟩,
42      fun _ => tooBig_ne hb, (fun h => by cases h), (fun h => by cases h)⟩
43  · rw [ite_eq_right hb]
44    have hb' : tooBig e.c.type (1 <<< e.c.root) = false := by simpa using hb
45    have hu0cap : 2 ^ e.R ≤ e.cap := by
46      by_cases hc : e.c.type = CODES
47      · obtain ⟨h1, h2, _, _⟩ := e.h_codes hc
48        have hcap := e.h_cap
49        rw [ite_eq_left hc] at hcap
50        have : 2 ^ e.R ≤ 2 ^ 7 := Nat.pow_le_pow_right (by omega) (by omega)
51        omega
52      · have := tooBig_le e hb' hc
53        omega
54    have hMI0 : MI e 0 (TS.mk 0 0 min e.c.root 0 0xffffffff (1 <<< e.c.root) min 0 0 ((1 <<< e.c.root) - 1) left
55        e.c.table default count 0) ca := by
56      refine ⟨hpos, rfl, rfl, hmin, ?_, ?_, hcnt, hsz, ?_⟩
57      · show (0 : UInt32).toNat = rev (e.l 0) (e.v 0)
58        rw [show e.v 0 = 0 from val_zero hpos, rev_zero]; rfl
59      · show ((1 <<< e.c.root) - 1 : UInt32).toNat = 2 ^ e.R - 1
60        rw [u32_sub (by rw [hu0]; exact Nat.pow_pos (by omega)), hu0]
61        simp [UInt32.toNat_one]
62      · refine ⟨⟨0, ?_, ?_⟩, ?_, ?_, ?_, ?_, fun _ => ⟨rfl, rfl, ?_, ?_⟩, fun h => ?_⟩
63        · show e.c.table = .ref e.rc (e.oc + 0); rw [e.h_table]; rfl
64        · show 0 + 2 ^ e.c.root.toNat = ((1 : UInt32) <<< e.c.root).toNat; rw [hu0, hroot]; omega
65        · show ((1 : UInt32) <<< e.c.root).toNat ≤ e.cap; omega
66        · show 2 ^ e.R ≤ ((1 : UInt32) <<< e.c.root).toNat; omega
67        · show 1 ≤ e.c.root.toNat; omega
68        · show e.c.root.toNat ≤ 15; omega
69        · show e.c.root.toNat = e.R; omega
70        · show ((1 : UInt32) <<< e.c.root).toNat = 2 ^ e.R; omega
71        · have := e.h_R0; have : e.l 0 = lenAt e.f e.n 0 := rfl; omega
72    have hEx0 : Ex e 0 (TS.mk 0 0 min e.c.root 0 0xffffffff (1 <<< e.c.root) min 0 0 ((1 <<< e.c.root) - 1) left
73        e.c.table default count 0) ca := by
74      have hD0 : e.D 0 = ⟨0, e.R, 0, 2 ^ e.R, 2 ^ 32 - 1⟩ := rfl
75      refine ⟨?_, fun _ => ⟨fun j hj => absurd hj (by omega), fun a h1 h2 => by omega⟩⟩
76      unfold DescIs DescB
77      rw [hD0]
78      refine ⟨⟨⟨0, ?_, rfl⟩, ?_, ?_⟩, rfl, ?_⟩
79      · show e.c.table = .ref e.rc (e.oc + 0); rw [e.h_table]; rfl
80      · show e.c.root.toNat = e.R; omega
81      · show ((1 : UInt32) <<< e.c.root).toNat = 2 ^ e.R; omega
82      · show (0xffffffff : UInt32).toNat = 2 ^ 32 - 1; rfl
83    have hTle : e.m ≤ e.n := Tc_le 15 e.n
84    have hn288 := e.h_n
85    apply Wp.bind' (Q := fun s h' => (∃ ca', h' = e.hc ca' ∧ FrameCA e ca ca' ∧ s.exit = 1 ∧ Final e s ∧
86          e.oc + e.cap ≤ ca'.size ∧ Cont e e.m e.m ca' ∧ (s.huff.toNat ≠ 0 → Einc e s) ∧ EndFields e s) ∨
87        (∃ ca', h' = e.hc ca' ∧ FrameCA e ca ca' ∧ s.exit = 2 ∧ e.c.type ≠ CODES ∧ e.oc + e.cap ≤ ca'.size))
88      (Wp.cwhile
89        (fun (s : TS) h' => (∃ i ca', h' = e.hc ca' ∧ FrameCA e ca ca' ∧ MI e i s ca' ∧ Ex e i s ca') ∨
90          (∃ ca', h' = e.hc ca' ∧ FrameCA e ca ca' ∧ s.exit = 1 ∧ Final e s ∧ e.oc + e.cap ≤ ca'.size ∧
91            Cont e e.m e.m ca' ∧ (s.huff.toNat ≠ 0 → Einc e s) ∧ EndFields e s) ∨
92          (∃ ca', h' = e.hc ca' ∧ FrameCA e ca ca' ∧ s.exit = 2 ∧ e.c.type ≠ CODES ∧ e.oc + e.cap ≤ ca'.size))
93        (fun (s : TS) => if s.exit = 0 then e.m + 1 - s.sym.toNat else 0) _ ?_ (Or.inl ⟨0, ca, rfl, ⟨rfl, fun _ _ => rfl⟩, hMI0, hEx0⟩) ?_)
94    · rintro s h' hinv
95      rcases hinv with ⟨ca', rfl, hf, hx, hfin, hsz', hcF, hinc, endFields⟩ | ⟨ca', rfl, hf, hx, hnc, hsz'⟩
96      · rw [ite_eq_right (by simp [hx])]
97        obtain ⟨⟨k, hn, hk⟩, hucap, hh⟩ := hfin
98        by_cases hh0 : s.huff = 0
99        · rw [ite_eq_right (by simp [hh0])]
100          show Wp (do let table ← Ptr.add e.c.table ↑s.used.toNat; pure (0, table, e.c.root)) _ _
101          rw [e.h_table]
102          apply Wp.bind' (wp_add e ca' e.oc s.used.toNat (by omega))
103          rintro q h' ⟨rfl, rfl⟩
104          refine Wp.pure' ⟨ca', rfl, hf, Or.inl ⟨rfl, s.used.toNat, hucap, rfl, rfl⟩, fun h => absurd (show (0 : Int32) = 1 from h) (by decide), fun _ => hcF, ?_⟩
105          intro _
106          refine ⟨s.used.toNat, rfl, endFields.1.2.2, ?_⟩
107          intro single one
108          have impossible := endFields.2.2.2 single one
109          rw [hh0] at impossible
110          contradiction
111        · rw [ite_eq_left (by simpa using hh0)]
112          have hhlt : s.huff.toNat < 2 ^ s.curr.toNat := by
113            rcases hh with h0 | h0
114            · exact absurd (UInt32.toNat_inj.mp (by rw [h0]; rfl)) hh0
115            · exact h0
116          have hidx : e.oc + k + s.huff.toNat < ca'.size := by
117            have := hf.1; omega
118          show Wp (do let __r ← storeCode s.next s.huff.toNat ⟨64, (s.len - s.drop).toUInt8, 0⟩
119                      let table ← Ptr.add e.c.table ↑s.used.toNat; pure (0, table, e.c.root)) _ _
120          unfold storeCode
121          rw [hn, e.h_table]
122          apply Wp.bind' (Q := fun _ h' => h' = e.hc (ca'.set! (e.oc + k + s.huff.toNat) ⟨64, (s.len - s.drop).toUInt8, 0⟩))
123          · apply Wp.bind' (wp_add e ca' (e.oc + k) s.huff.toNat (by omega))
124            rintro q h' ⟨rfl, rfl⟩
125            refine ⟨(), _, Ptr.store_ok (e.get_hc ca') e.h_ro (by omega), ?_⟩
126            rw [Env.hc_hc]
127          · rintro _ h' rfl
128            apply Wp.bind' (wp_add e _ e.oc s.used.toNat (by rw [Array.size_set!]; omega))
129            rintro q h' ⟨rfl, rfl⟩
130            have hne0 : s.huff.toNat ≠ 0 := fun h0 => hh0 (UInt32.toNat_inj.mp (by rw [h0]; rfl))
131            obtain ⟨hm1, hRR, hh1, hnxt⟩ := hinc hne0
132            have hk0 : k = 0 := by
133              have := Ptr.ref.inj (hn.symm.trans hnxt)
134              omega
135            refine Wp.pure' ⟨_, rfl, ?_, Or.inl ⟨rfl, s.used.toNat, hucap, rfl, rfl⟩, fun h => absurd (show (0 : Int32) = 1 from h) (by decide), fun _ => ?_, ?_⟩
136            · refine ⟨by rw [Array.size_set!]; exact hf.1, fun x hx => ?_⟩
137              have hne : e.oc + k + s.huff.toNat ≠ x := by omega
138              rw [getElem?_set!_ne hne]
139              exact hf.2 x hx
140            · intro hg
141              obtain ⟨hW, hL⟩ := hcF hg
142              refine ⟨fun j hj mm hmm => ?_, fun a h1 h2 h3 h4 => absurd h3 (by omega)⟩
143              have hj0 : j = 0 := by omega
144              subst hj0
145              rw [getElem?_set!_ne (by rw [gaddr0 e hm1 hRR hmm]; omega)]
146              exact hW 0 (by omega) mm hmm
147            · intro _
148              refine ⟨s.used.toNat, rfl, endFields.1.2.2, ?_⟩
149              intro single one
150              have lastIndex : e.m - 1 = 0 := by omega
151              have drop0 : s.drop = 0 := by
152                apply UInt32.toNat_inj.mp
153                have drop := endFields.2.1
154                rw [lastIndex] at drop
155                exact drop
156              have len1 : s.len = 1 := by
157                apply UInt32.toNat_inj.mp
158                exact endFields.2.2.1.trans one
159              simp only [hk0, hh1, Nat.add_zero, len1, drop0]
160              exact getElem?_set!_self (by omega)
161      · rw [ite_eq_left (by simp [hx])]
162        exact Wp.pure' ⟨ca', rfl, hf, Or.inr ⟨rfl, rfl, rfl⟩,
163          fun _ => hnc, (fun h => by cases h), (fun h => by cases h)⟩
164    · rintro s h' hinv
165      rcases hinv with ⟨i, ca', rfl, hf, hmi, hexi⟩ | ⟨ca', rfl, hf, hx, hfin, hsz', hcF, hinc, endFields⟩ | ⟨ca', rfl, hf, hx, hnc, hsz'⟩
166      · right
167        have hex : s.exit = 0 := hmi.2.1
168        have hsymi : s.sym.toNat = i := hmi.2.2.1
169        have hi : i < e.m := hmi.1
170        obtain ⟨s2, h2, hrun, ca2, hh, hf2, hpost, hpostE, hpostF⟩ := hereTop_wp e i s ca' hmi hexi
171        subst hh
172        refine ⟨s, e.hc ca', s2, e.hc ca2, ?_, ?_, ?_, ?_⟩
173        · show (pure (s.exit == 0, s) : M _) _ = _
174          simp [hex]
175        · rw [buildStep_eq]; exact hrun
176        · rcases hpost with ⟨him, hMI⟩ | ⟨him, hx, hfin, hsz2⟩ | ⟨hx, hnc, hsz2⟩
177          · exact Or.inl ⟨i + 1, ca2, rfl, hf.trans hf2, hMI, hpostE him hMI.2.1⟩
178          · refine Or.inr (Or.inl ⟨ca2, rfl, hf.trans hf2, hx, hfin, hsz2, (hpostF him hx).1, (hpostF him hx).2, ?_⟩)
179            obtain ⟨descriptor, drop, len⟩ := hereTop_final_descriptor hmi hexi him hrun
180            have index : i = e.m - 1 := by omega
181            have maxLen : e.l i = e.mx := by
182              change lenAt e.f e.n i = lenAt e.f e.n (Tc e.f e.n 15 - 1)
183              rw [index, hm15]
184            refine ⟨?_, ?_, len.trans maxLen, ?_⟩
185            · simpa only [index] using descriptor
186            · simpa only [index] using drop
187            · intro single one
188              exact hereTop_final_single_huff hmi him single one hrun
189          · exact Or.inr (Or.inr ⟨ca2, rfl, hf.trans hf2, hx, hnc, hsz2⟩)
190        · rcases hpost with ⟨him, hMI⟩ | ⟨him, hx, hfin, hsz2⟩ | ⟨hx, hnc, hsz2⟩
191          · have h3 : s2.exit = 0 := hMI.2.1
192            have h4 : s2.sym.toNat = i + 1 := hMI.2.2.1
193            simp only [hex, h3, ite_true, hsymi, h4]; omega
194          · simp only [hx, hex]; simp; omega
195          · simp only [hx, hex]; simp; omega
196      · left
197        refine ⟨s, e.hc ca', ?_, Or.inl ⟨ca', rfl, hf, hx, hfin, hsz', hcF, hinc, endFields⟩⟩
198        show (pure (s.exit == 0, s) : M _) _ = _
199        simp [hx]
200      · left
201        refine ⟨s, e.hc ca', ?_, Or.inr ⟨ca', rfl, hf, hx, hnc, hsz'⟩⟩
202        show (pure (s.exit == 0, s) : M _) _ = _
203        simp [hx]
204    · dsimp only
205      split
206      · exact lt_fuel (by omega)
207      · exact lt_fuel (by omega)
208
209end Zlib.Inftrees.Proofs