参考文档 / ZLIB × LEAN
inftrees.c.main.lean
此页源文件快照 ·
24039a675ace8b23 · 对应提交的原文 ↗本页保留 Lean 源码及行号。点击行号可定位语句，点击 import 中的模块名可查看依赖。
1import ZlibF.Proof.«inftrees.c.step»
2import ZlibF.Proof.«inftrees.c.spec»
3import ZlibF.Proof.«inftrees.c.link»
4
5namespace Zlib.Inftrees.Proofs
6open C Zlib.Inftrees Zlib.Inftrees.Spec
7
8/-! ### `inflate_table` cut at its join points -/
9
10/-- From the declaration of the state of the main loop on. -/
11def itTail (type : UInt32) (lens : WPtr) (table : CodePtr) (bits : UInt32) (work : WPtr) (count : Array UInt16)
12 (max min root : UInt32) (left : Int32) (base extra : Array UInt16) (match_ : UInt32) :
13 M (Int32 × CodePtr × UInt32) := do
14 let used ← shl32 1 root
15 let s : TS := { huff := 0, sym := 0, len := min, curr := root, drop := 0, low := 0xffffffff, used,
16 min := min, fill := 0, incr := 0, mask := used - 1, left, next := table, here := default,
17 count, exit := 0 }
18 if tooBig type used then return (1, table, bits)
19 let c : Ctx := { type, lens, work, table, root, max, base, extra, match_ }
20 let s ← cwhile (fun s => pure (s.exit == 0, s)) (buildStep c) s
21 if s.exit == 2 then return (1, table, bits)
22 let mut s := s
23 if s.huff != 0 then
24 s := { s with here := ⟨64, (s.len - s.drop).toUInt8, 0⟩ }
25 storeCode s.next s.huff.toNat s.here
26 let table ← table.add s.used.toNat
27 return (0, table, root)
28
29/-- From the check of the Kraft sum on. -/
30def itB (type : UInt32) (lens : WPtr) (codes : UInt32) (table : CodePtr) (bits : UInt32) (work : WPtr)
31 (count : Array UInt16) (max min root : UInt32) : M (Int32 × CodePtr × UInt32) := do
32 let offs : Array UInt16 := Array.replicate 16 0
33 let (left, bad, _) ← cwhile (fun (left, bad, len) => pure (!bad && len ≤ MAXBITS, (left, bad, len)))
34 (fun (left, bad, len) => do
35 if left < 0 then ub "left shift of a negative value" else
36 let left ← chk32 (left.toInt * 2)
37 let cc ← geta count len.toNat
38 let left ← chk32 (left.toInt - cc.toNat)
39 if left < 0 then pure (left, true, len) else pure (left, bad, len + 1)) ((1 : Int32), false, (1 : UInt32))
40 if bad then return (-1, table, bits)
41 if left > 0 && (type == CODES || max != 1) then return (-1, table, bits)
42 let offs ← seta offs 1 0
43 let (_, offs) ← cwhile (fun (len, offs) => pure (len < MAXBITS, (len, offs)))
44 (fun (len, offs) => do
45 let a ← geta offs len.toNat
46 let b ← geta count len.toNat
47 pure (len + 1, ← seta offs (len + 1).toNat (a + b))) ((1 : UInt32), offs)
48 let (_, offs) ← cwhile (fun (sym, offs) => pure (sym < codes, (sym, offs)))
49 (fun (sym, offs) => do
50 let l ← lens.index sym.toNat
51 if l != 0 then
52 let l ← lens.index sym.toNat
53 let o ← geta offs l.toNat
54 let offs ← seta offs l.toNat (o + 1)
55 let q ← work.add o.toNat
56 Ptr.store q sym.toUInt16
57 pure (sym + 1, offs)
58 else pure (sym + 1, offs)) ((0 : UInt32), offs)
59 let mut base : Array UInt16 := #[]
60 let mut extra : Array UInt16 := #[]
61 let mut match_ : UInt32 := 0
62 if type == CODES then
63 match_ := 20
64 else if type == LENS then
65 base := lbase; extra := lext; match_ := 257
66 else if type == DISTS then
67 base := dbase; extra := dext
68 itTail type lens table bits work count max min root left base extra match_
69
70/-- From the test `max == 0` on. -/
71def itA (type : UInt32) (lens : WPtr) (codes : UInt32) (table : CodePtr) (bits : UInt32) (work : WPtr)
72 (count : Array UInt16) (max root : UInt32) : M (Int32 × CodePtr × UInt32) := do
73 if max == 0 then
74 let here : Code := ⟨64, 1, 0⟩
75 Ptr.store table here
76 let table ← table.add 1
77 Ptr.store table here
78 let table ← table.add 1
79 return (0, table, 1)
80 let (min, _) ← cwhile (fun (min, brk) => pure (!brk && min < max, (min, brk)))
81 (fun (min, brk) => do
82 if (← geta count min.toNat) != 0 then pure (min, true) else pure (min + 1, brk)) ((1 : UInt32), false)
83 let mut root := root
84 if root < min then root := min
85 itB type lens codes table bits work count max min root
86
87def itTop (type : UInt32) (lens : WPtr) (codes : UInt32) (table : CodePtr) (bits : UInt32) (work : WPtr) :
88 M (Int32 × CodePtr × UInt32) := do
89 let count : Array UInt16 := Array.replicate 16 0
90 let (_, count) ← cwhile (fun (len, count) => pure (len ≤ MAXBITS, (len, count)))
91 (fun (len, count) => do pure (len + 1, ← seta count len.toNat 0)) ((0 : UInt32), count)
92 let (_, count) ← cwhile (fun (sym, count) => pure (sym < codes, (sym, count)))
93 (fun (sym, count) => do
94 let l ← lens.index sym.toNat
95 let c ← geta count l.toNat
96 pure (sym + 1, ← seta count l.toNat (c + 1))) ((0 : UInt32), count)
97 let mut root := bits
98 let (max, _) ← cwhile (fun (max, brk) => pure (!brk && max ≥ 1, (max, brk)))
99 (fun (max, brk) => do
100 if (← geta count max.toNat) != 0 then pure (max, true) else pure (max - 1, brk)) (MAXBITS, false)
101 if root > max then root := max
102 itA type lens codes table bits work count max root
103
104theorem gaddr0 (e : Env) (hm : e.m = 1) (hR : e.R = 1) {mm : Nat} (hmm : mm < gReps e.ls e.R e.mx 0) :
105 gAddr e.ls e.R e.mx 0 mm = 0 := by
106 have hpos := e.h_pos
107 obtain ⟨b1, b2⟩ := lenAt_bounds (f := e.f) (n := e.n) hpos
108 have hR0 := e.h_R0
109 have hL : Canon.L e.ls 0 = 1 := by
110 rw [show Canon.L e.ls 0 = lenAt e.f e.n 0 from L_eq e.f e.n hpos]; omega
111 have hD0 : Canon.desc e.ls e.R e.mx 0 = ⟨0, e.R, 0, 2 ^ e.R, 2 ^ 32 - 1⟩ := rfl
112 unfold gReps at hmm
113 rw [hD0, hL, hR] at hmm
114 simp at hmm
115 unfold gAddr
116 rw [hD0, hL, hR, Canon.H_zero]
117 simp [hmm]
118
119theorem itTail_wp (e : Env) (ca : Array Code) (count : Array UInt16) (bits min : UInt32) (left : Int32)
120 (hcnt : CountOK e count 0) (hmin : min.toNat = e.l 0) (hsz : e.oc + e.cap ≤ ca.size) :
121 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
122 e.c.match_) (e.hc ca)
123 (fun r h' => ∃ ca', h' = e.hc ca' ∧ FrameCA e ca ca' ∧
124 ((r.1 = 0 ∧ ∃ u, u ≤ e.cap ∧ r.2.1 = .ref e.rc (e.oc + u) ∧ r.2.2 = e.c.root) ∨
125 (r.1 = 1 ∧ r.2.1 = e.c.table ∧ r.2.2 = bits)) ∧ (r.1 = 1 → e.c.type ≠ CODES) ∧
126 (r.1 = 0 → Cont e e.m e.m ca')) := by
127 have hR1 := e.h_R1
128 have hroot := e.h_root
129 have hpos := e.h_pos
130 have hmxle : e.mx ≤ 15 := by
131 have := lenAt_bounds (f := e.f) (n := e.n) (show e.m - 1 < Tc e.f e.n 15 by unfold Env.m; omega)
132 exact this.2
133 have hRmx := e.h_Rmx
134 have hm15 : e.m = Tc e.f e.n 15 := rfl
135 have hmx15 : e.mx = mxl e.f e.n := rfl
136 have hR32 : e.c.root.toNat < 32 := by omega
137 unfold itTail
138 apply Wp.bind' (Q := fun r h' => r = 1 <<< e.c.root ∧ h' = e.hc ca) (Wp.pure_eq (shl32_eq hR32) ⟨rfl, rfl⟩)
139 rintro used0 h' ⟨rfl, rfl⟩
140 have hu0 : ((1 : UInt32) <<< e.c.root).toNat = 2 ^ e.R := by rw [u32_shl1 hR32, hroot]
141 by_cases hb : tooBig e.c.type (1 <<< e.c.root) = true
142 · rw [ite_eq_left hb]
143 exact Wp.pure' ⟨ca, rfl, ⟨rfl, fun _ _ => rfl⟩, Or.inr ⟨rfl, rfl, rfl⟩, fun _ => tooBig_ne hb, fun h => by cases h⟩
144 · rw [ite_eq_right hb]
145 have hb' : tooBig e.c.type (1 <<< e.c.root) = false := by simpa using hb
146 have hu0cap : 2 ^ e.R ≤ e.cap := by
147 by_cases hc : e.c.type = CODES
148 · obtain ⟨h1, h2, _, _⟩ := e.h_codes hc
149 have hcap := e.h_cap
150 rw [ite_eq_left hc] at hcap
151 have : 2 ^ e.R ≤ 2 ^ 7 := Nat.pow_le_pow_right (by omega) (by omega)
152 omega
153 · have := tooBig_le e hb' hc
154 omega
155 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
156 e.c.table default count 0) ca := by
157 refine ⟨hpos, rfl, rfl, hmin, ?_, ?_, hcnt, hsz, ?_⟩
158 · show (0 : UInt32).toNat = rev (e.l 0) (e.v 0)
159 rw [show e.v 0 = 0 from val_zero hpos, rev_zero]; rfl
160 · show ((1 <<< e.c.root) - 1 : UInt32).toNat = 2 ^ e.R - 1
161 rw [u32_sub (by rw [hu0]; exact Nat.pow_pos (by omega)), hu0]
162 simp [UInt32.toNat_one]
163 · refine ⟨⟨0, ?_, ?_⟩, ?_, ?_, ?_, ?_, fun _ => ⟨rfl, rfl, ?_, ?_⟩, fun h => ?_⟩
164 · show e.c.table = .ref e.rc (e.oc + 0); rw [e.h_table]; rfl
165 · show 0 + 2 ^ e.c.root.toNat = ((1 : UInt32) <<< e.c.root).toNat; rw [hu0, hroot]; omega
166 · show ((1 : UInt32) <<< e.c.root).toNat ≤ e.cap; omega
167 · show 2 ^ e.R ≤ ((1 : UInt32) <<< e.c.root).toNat; omega
168 · show 1 ≤ e.c.root.toNat; omega
169 · show e.c.root.toNat ≤ 15; omega
170 · show e.c.root.toNat = e.R; omega
171 · show ((1 : UInt32) <<< e.c.root).toNat = 2 ^ e.R; omega
172 · have := e.h_R0; have : e.l 0 = lenAt e.f e.n 0 := rfl; omega
173 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
174 e.c.table default count 0) ca := by
175 have hD0 : e.D 0 = ⟨0, e.R, 0, 2 ^ e.R, 2 ^ 32 - 1⟩ := rfl
176 refine ⟨?_, fun _ => ⟨fun j hj => absurd hj (by omega), fun a h1 h2 => by omega⟩⟩
177 unfold DescIs DescB
178 rw [hD0]
179 refine ⟨⟨⟨0, ?_, rfl⟩, ?_, ?_⟩, rfl, ?_⟩
180 · show e.c.table = .ref e.rc (e.oc + 0); rw [e.h_table]; rfl
181 · show e.c.root.toNat = e.R; omega
182 · show ((1 : UInt32) <<< e.c.root).toNat = 2 ^ e.R; omega
183 · show (0xffffffff : UInt32).toNat = 2 ^ 32 - 1; rfl
184 have hTle : e.m ≤ e.n := Tc_le 15 e.n
185 have hn288 := e.h_n
186 apply Wp.bind' (Q := fun s h' => (∃ ca', h' = e.hc ca' ∧ FrameCA e ca ca' ∧ s.exit = 1 ∧ Final e s ∧
187 e.oc + e.cap ≤ ca'.size ∧ Cont e e.m e.m ca' ∧ (s.huff.toNat ≠ 0 → Einc e s)) ∨
188 (∃ ca', h' = e.hc ca' ∧ FrameCA e ca ca' ∧ s.exit = 2 ∧ e.c.type ≠ CODES ∧ e.oc + e.cap ≤ ca'.size))
189 (Wp.cwhile
190 (fun (s : TS) h' => (∃ i ca', h' = e.hc ca' ∧ FrameCA e ca ca' ∧ MI e i s ca' ∧ Ex e i s ca') ∨
191 (∃ ca', h' = e.hc ca' ∧ FrameCA e ca ca' ∧ s.exit = 1 ∧ Final e s ∧ e.oc + e.cap ≤ ca'.size ∧
192 Cont e e.m e.m ca' ∧ (s.huff.toNat ≠ 0 → Einc e s)) ∨
193 (∃ ca', h' = e.hc ca' ∧ FrameCA e ca ca' ∧ s.exit = 2 ∧ e.c.type ≠ CODES ∧ e.oc + e.cap ≤ ca'.size))
194 (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⟩) ?_)
195 · rintro s h' hinv
196 rcases hinv with ⟨ca', rfl, hf, hx, hfin, hsz', hcF, hinc⟩ | ⟨ca', rfl, hf, hx, hnc, hsz'⟩
197 · rw [ite_eq_right (by simp [hx])]
198 obtain ⟨⟨k, hn, hk⟩, hucap, hh⟩ := hfin
199 by_cases hh0 : s.huff = 0
200 · rw [ite_eq_right (by simp [hh0])]
201 show Wp (do let table ← Ptr.add e.c.table ↑s.used.toNat; pure (0, table, e.c.root)) _ _
202 rw [e.h_table]
203 apply Wp.bind' (wp_add e ca' e.oc s.used.toNat (by omega))
204 rintro q h' ⟨rfl, rfl⟩
205 exact 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⟩
206 · rw [ite_eq_left (by simpa using hh0)]
207 have hhlt : s.huff.toNat < 2 ^ s.curr.toNat := by
208 rcases hh with h0 | h0
209 · exact absurd (UInt32.toNat_inj.mp (by rw [h0]; rfl)) hh0
210 · exact h0
211 have hidx : e.oc + k + s.huff.toNat < ca'.size := by
212 have := hf.1; omega
213 show Wp (do let __r ← storeCode s.next s.huff.toNat ⟨64, (s.len - s.drop).toUInt8, 0⟩
214 let table ← Ptr.add e.c.table ↑s.used.toNat; pure (0, table, e.c.root)) _ _
215 unfold storeCode
216 rw [hn, e.h_table]
217 apply Wp.bind' (Q := fun _ h' => h' = e.hc (ca'.set! (e.oc + k + s.huff.toNat) ⟨64, (s.len - s.drop).toUInt8, 0⟩))
218 · apply Wp.bind' (wp_add e ca' (e.oc + k) s.huff.toNat (by omega))
219 rintro q h' ⟨rfl, rfl⟩
220 refine ⟨(), _, Ptr.store_ok (e.get_hc ca') e.h_ro (by omega), ?_⟩
221 rw [Env.hc_hc]
222 · rintro _ h' rfl
223 apply Wp.bind' (wp_add e _ e.oc s.used.toNat (by rw [Array.size_set!]; omega))
224 rintro q h' ⟨rfl, rfl⟩
225 have hne0 : s.huff.toNat ≠ 0 := fun h0 => hh0 (UInt32.toNat_inj.mp (by rw [h0]; rfl))
226 obtain ⟨hm1, hRR, hh1, hnxt⟩ := hinc hne0
227 have hk0 : k = 0 := by
228 have := Ptr.ref.inj (hn.symm.trans hnxt)
229 omega
230 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 _ => ?_⟩
231 · refine ⟨by rw [Array.size_set!]; exact hf.1, fun x hx => ?_⟩
232 have hne : e.oc + k + s.huff.toNat ≠ x := by omega
233 rw [getElem?_set!_ne hne]
234 exact hf.2 x hx
235 · intro hg
236 obtain ⟨hW, hL⟩ := hcF hg
237 refine ⟨fun j hj mm hmm => ?_, fun a h1 h2 h3 h4 => absurd h3 (by omega)⟩
238 have hj0 : j = 0 := by omega
239 subst hj0
240 rw [getElem?_set!_ne (by rw [gaddr0 e hm1 hRR hmm]; omega)]
241 exact hW 0 (by omega) mm hmm
242 · rw [ite_eq_left (by simp [hx])]
243 exact Wp.pure' ⟨ca', rfl, hf, Or.inr ⟨rfl, rfl, rfl⟩, fun _ => hnc, fun h => by cases h⟩
244 · rintro s h' hinv
245 rcases hinv with ⟨i, ca', rfl, hf, hmi, hexi⟩ | ⟨ca', rfl, hf, hx, hfin, hsz', hcF, hinc⟩ | ⟨ca', rfl, hf, hx, hnc, hsz'⟩
246 · right
247 have hex : s.exit = 0 := hmi.2.1
248 have hsymi : s.sym.toNat = i := hmi.2.2.1
249 have hi : i < e.m := hmi.1
250 obtain ⟨s2, h2, hrun, ca2, hh, hf2, hpost, hpostE, hpostF⟩ := hereTop_wp e i s ca' hmi hexi
251 subst hh
252 refine ⟨s, e.hc ca', s2, e.hc ca2, ?_, ?_, ?_, ?_⟩
253 · show (pure (s.exit == 0, s) : M _) _ = _
254 simp [hex]
255 · rw [buildStep_eq]; exact hrun
256 · rcases hpost with ⟨him, hMI⟩ | ⟨him, hx, hfin, hsz2⟩ | ⟨hx, hnc, hsz2⟩
257 · exact Or.inl ⟨i + 1, ca2, rfl, hf.trans hf2, hMI, hpostE him hMI.2.1⟩
258 · exact Or.inr (Or.inl ⟨ca2, rfl, hf.trans hf2, hx, hfin, hsz2, (hpostF him hx).1, (hpostF him hx).2⟩)
259 · exact Or.inr (Or.inr ⟨ca2, rfl, hf.trans hf2, hx, hnc, hsz2⟩)
260 · rcases hpost with ⟨him, hMI⟩ | ⟨him, hx, hfin, hsz2⟩ | ⟨hx, hnc, hsz2⟩
261 · have h3 : s2.exit = 0 := hMI.2.1
262 have h4 : s2.sym.toNat = i + 1 := hMI.2.2.1
263 simp only [hex, h3, ite_true, hsymi, h4]; omega
264 · simp only [hx, hex]; simp; omega
265 · simp only [hx, hex]; simp; omega
266 · left
267 refine ⟨s, e.hc ca', ?_, Or.inl ⟨ca', rfl, hf, hx, hfin, hsz', hcF, hinc⟩⟩
268 show (pure (s.exit == 0, s) : M _) _ = _
269 simp [hx]
270 · left
271 refine ⟨s, e.hc ca', ?_, Or.inr ⟨ca', rfl, hf, hx, hnc, hsz'⟩⟩
272 show (pure (s.exit == 0, s) : M _) _ = _
273 simp [hx]
274 · dsimp only
275 split
276 · exact lt_fuel (by omega)
277 · exact lt_fuel (by omega)
278
279def kraftCond : Int32 × Bool × UInt32 → M (Bool × (Int32 × Bool × UInt32)) :=
280 fun (left, bad, len) => pure (!bad && len ≤ MAXBITS, (left, bad, len))
281
282def kraftBody (count : Array UInt16) : Int32 × Bool × UInt32 → M (Int32 × Bool × UInt32) :=
283 fun (left, bad, len) => do
284 if left < 0 then ub "left shift of a negative value" else
285 let left ← chk32 (left.toInt * 2)
286 let cc ← geta count len.toNat
287 let left ← chk32 (left.toInt - cc.toNat)
288 if left < 0 then pure (left, true, len) else pure (left, bad, len + 1)
289
290theorem i32_lt_zero {x : Int32} : x < 0 ↔ x.toInt < 0 := by
291 rw [Int32.lt_iff_toInt_lt, Int32.toInt_zero]
292
293theorem kraftBody_eq (count : Array UInt16) (left : Int32) (bad : Bool) (len : UInt32)
294 (hl0 : 0 ≤ left.toInt) (hi : len.toNat < count.size)
295 (hr1 : left.toInt * 2 ≤ 2147483647) :
296 kraftBody count (left, bad, len) =
297 pure (if left.toInt * 2 - (count[len.toNat]).toNat < 0 then
298 (Int32.ofInt (left.toInt * 2 - (count[len.toNat]).toNat), true, len)
299 else (Int32.ofInt (left.toInt * 2 - (count[len.toNat]).toNat), bad, len + 1)) := by
300 simp only [kraftBody]
301 have hn : ¬ (left < 0) := by rw [i32_lt_zero]; omega
302 rw [ite_eq_right hn]
303 have hr2 : -2147483648 ≤ left.toInt * 2 := by omega
304 rw [chk32_eq hr2 hr1, M_pure_bind, geta_eq hi, M_pure_bind]
305 have hv1 : -2147483648 ≤ (Int32.ofInt (left.toInt * 2)).toInt - (count[len.toNat]).toNat := by
306 rw [i32_ofInt_toInt hr2 hr1]; have := UInt16.toNat_lt count[len.toNat]; omega
307 have hv2 : (Int32.ofInt (left.toInt * 2)).toInt - (count[len.toNat]).toNat ≤ 2147483647 := by
308 rw [i32_ofInt_toInt hr2 hr1]; omega
309 rw [chk32_eq hv1 hv2, M_pure_bind]
310 rw [i32_ofInt_toInt hr2 hr1]
311 have hlt : Int32.ofInt (left.toInt * 2 - (count[len.toNat]).toNat) < 0 ↔ left.toInt * 2 - (count[len.toNat]).toNat < 0 := by
312 rw [i32_lt_zero, i32_ofInt_toInt (by have := UInt16.toNat_lt count[len.toNat]; omega) (by omega)]
313 by_cases hneg : left.toInt * 2 - (count[len.toNat]).toNat < 0
314 · rw [ite_eq_left (hlt.mpr hneg), ite_eq_left hneg]
315 · rw [ite_eq_right (fun h => hneg (hlt.mp h)), ite_eq_right hneg]
316
317/-- The Kraft loop of `inflate_table`. -/
318theorem kraft_loop (f : Nat → Nat) (n : Nat) (count : Array UInt16) (hs : count.size = 16)
319 (hc : ∀ l, 1 ≤ l → l ≤ 15 → (count.getD l 0).toNat = cnt f n l) (h : Heap) :
320 Wp (cwhile kraftCond (kraftBody count) ((1 : Int32), false, (1 : UInt32))) h
321 (fun r h' => h' = h ∧ ((r.2.1 = true ∧ ¬ Fits f n) ∨
322 (r.2.1 = false ∧ Fits f n ∧ r.1.toInt = 2 ^ 15 - (Kc f n 15 : Int)))) := by
323 refine Wp.cwhile
324 (fun (x : Int32 × Bool × UInt32) h' => h' = h ∧ 1 ≤ x.2.2.toNat ∧ x.2.2.toNat ≤ 16 ∧
325 (x.2.1 = false → 0 ≤ x.1.toInt ∧ x.1.toInt = 2 ^ (x.2.2.toNat - 1) - (Kc f n (x.2.2.toNat - 1) : Int) ∧
326 ∀ l, 1 ≤ l → l < x.2.2.toNat → Kc f n l ≤ 2 ^ l) ∧
327 (x.2.1 = true → ¬ Fits f n))
328 (fun (x : Int32 × Bool × UInt32) => if x.2.1 then 0 else 17 - x.2.2.toNat) _ ?_ ?_ ?_
329 · rintro ⟨left, bad, len⟩ h' ⟨rfl, hl1, hl2, hnb, hb⟩
330 dsimp only at hl1 hl2 hnb hb
331 by_cases hc' : (!bad && decide (len ≤ MAXBITS)) = true
332 · right
333 simp only [Bool.and_eq_true, Bool.not_eq_true', decide_eq_true_eq] at hc'
334 obtain ⟨hbad, hle⟩ := hc'
335 have hle' : len.toNat ≤ 15 := by
336 have := UInt32.le_iff_toNat_le.mp hle; exact this
337 obtain ⟨hp, hlv, hfit⟩ := hnb hbad
338 have hcnt := hc len.toNat hl1 hle'
339 have hlt16 : len.toNat < count.size := by omega
340 have hcc : (count[len.toNat]).toNat = cnt f n len.toNat := by
341 rw [Array.getD_eq_getD_getElem?, Array.getElem?_eq_getElem hlt16] at hcnt; simpa using hcnt
342 have hpow : (2:Int) ^ (len.toNat - 1) ≤ 16384 := by
343 have h14 : 2 ^ (len.toNat - 1) ≤ 2 ^ 14 := Nat.pow_le_pow_right (by omega) (by omega)
344 have : ((2 ^ (len.toNat - 1) : Nat) : Int) ≤ ((2 ^ 14 : Nat) : Int) := Int.ofNat_le.mpr h14
345 simpa [Int.natCast_pow] using this
346 have hKc := Kc_succ' (f := f) (n := n) hl1
347 have hcccast : ((count[len.toNat]).toNat : Int) = (cnt f n len.toNat : Int) := by rw [hcc]
348 have hp2 : (2:Int) ^ len.toNat = 2 * 2 ^ (len.toNat - 1) := by
349 obtain ⟨r, hr⟩ : ∃ r, len.toNat = r + 1 := ⟨len.toNat - 1, by omega⟩
350 rw [hr]; simp [Int.pow_succ, Int.mul_comm]
351 have heq := kraftBody_eq count left bad len hp (by omega) (by omega)
352 have hbody : kraftBody count (left, bad, len) h' = .ok
353 ((if left.toInt * 2 - (count[len.toNat]).toNat < 0 then
354 (Int32.ofInt (left.toInt * 2 - (count[len.toNat]).toNat), true, len)
355 else (Int32.ofInt (left.toInt * 2 - (count[len.toNat]).toNat), bad, len + 1)), h') := by
356 rw [heq]; rfl
357 have hcond : kraftCond (left, bad, len) h' = .ok ((true, (left, bad, len)), h') := by
358 show (pure ((!bad && decide (len ≤ MAXBITS)), (left, bad, len)) : M _) h' = _
359 rw [show ((!bad && decide (len ≤ MAXBITS))) = true from by
360 simp only [Bool.and_eq_true, Bool.not_eq_true', decide_eq_true_eq]; exact ⟨hbad, hle⟩]
361 rfl
362 refine ⟨(left, bad, len), h', _, h', hcond, hbody, ?_, ?_⟩
363 · by_cases hneg : left.toInt * 2 - (count[len.toNat]).toNat < 0
364 · rw [ite_eq_left hneg]
365 refine ⟨rfl, hl1, hl2, fun hx => by simp at hx, fun _ => ?_⟩
366 intro hfit'
367 have := hfit' len.toNat hl1 hle'
368 have h3 : (Kc f n len.toNat : Int) ≤ 2 ^ len.toNat := by exact_mod_cast this
369 generalize left.toInt = L at hlv hneg
370 generalize (2:Int) ^ (len.toNat - 1) = P at hlv hp2
371 generalize (2:Int) ^ len.toNat = Q at hp2 h3
372 generalize ((count[len.toNat]).toNat : Int) = cc at hneg hcccast
373 omega
374 · rw [ite_eq_right hneg]
375 have hu : (len + 1).toNat = len.toNat + 1 := u32_succ (by omega)
376 refine ⟨rfl, by rw [hu]; omega, by rw [hu]; omega, fun _ => ?_, fun hx => by simp [hbad] at hx⟩
377 have hv1 : -2147483648 ≤ left.toInt * 2 - (count[len.toNat]).toNat := by omega
378 have hv2 : left.toInt * 2 - (count[len.toNat]).toNat ≤ 2147483647 := by omega
379 rw [hu, i32_ofInt_toInt hv1 hv2]
380 simp only [Nat.add_sub_cancel]
381 refine ⟨by omega, ?_, ?_⟩
382 · rw [hcccast] at *
383 omega
384 · intro l hl1' hl2'
385 rcases Nat.lt_or_ge l len.toNat with h4 | h4
386 · exact hfit l hl1' h4
387 · have hl : l = len.toNat := by omega
388 rw [hl]
389 have hk : (Kc f n len.toNat : Int) ≤ 2 ^ len.toNat := by
390 have hneg' := hneg
391 generalize left.toInt = L at hlv hneg'
392 generalize (2:Int) ^ (len.toNat - 1) = P at hlv hp2
393 generalize (2:Int) ^ len.toNat = Q at hp2 ⊢
394 generalize ((count[len.toNat]).toNat : Int) = cc at hneg' hcccast
395 omega
396 exact_mod_cast hk
397 · by_cases hneg : left.toInt * 2 - (count[len.toNat]).toNat < 0
398 · rw [ite_eq_left hneg]; simp [hbad]; omega
399 · rw [ite_eq_right hneg]
400 have hu : (len + 1).toNat = len.toNat + 1 := u32_succ (by omega)
401 simp [hbad, hu]; omega
402 · left
403 have hcond : kraftCond (left, bad, len) h' = .ok ((false, (left, bad, len)), h') := by
404 show (pure ((!bad && decide (len ≤ MAXBITS)), (left, bad, len)) : M _) h' = _
405 have : ((!bad && decide (len ≤ MAXBITS))) = false := by
406 cases hh : ((!bad && decide (len ≤ MAXBITS)))
407 · rfl
408 · exact absurd hh hc'
409 rw [this]; rfl
410 refine ⟨(left, bad, len), h', hcond, rfl, ?_⟩
411 cases hbad : bad
412 · right
413 have hn : ¬ (len ≤ MAXBITS) := by
414 intro hle; apply hc'; simp [hbad, hle]
415 have hn' : 16 ≤ len.toNat := by
416 have := (not_congr UInt32.le_iff_toNat_le).mp hn
417 have h15 : MAXBITS.toNat = 15 := rfl
418 omega
419 obtain ⟨hp, hlv, hfit⟩ := hnb hbad
420 have h16 : len.toNat = 16 := by omega
421 refine ⟨rfl, fun l hl1' hl2' => hfit l hl1' (by omega), ?_⟩
422 rw [hlv, h16]
423 · left
424 exact ⟨rfl, hb hbad⟩
425 · refine ⟨rfl, Nat.le_refl _, by decide, fun _ => ⟨by decide, ?_, fun l h1 h2 => by simp at h2; omega⟩, fun hx => by simp at hx⟩
426 show ((1 : Int32).toInt) = 2 ^ 0 - (Kc f n 0 : Int)
427 have hK0 : Kc f n 0 = 0 := rfl
428 rw [hK0]; decide
429 · show (if false = true then 0 else 17 - (1 : UInt32).toNat) < fuel
430 exact lt_fuel (by decide)
431
432def offsCond : UInt32 × Array UInt16 → M (Bool × (UInt32 × Array UInt16)) :=
433 fun (len, offs) => pure (len < MAXBITS, (len, offs))
434
435def offsBody (count : Array UInt16) : UInt32 × Array UInt16 → M (UInt32 × Array UInt16) :=
436 fun (len, offs) => do
437 let a ← geta offs len.toNat
438 let b ← geta count len.toNat
439 pure (len + 1, ← seta offs (len + 1).toNat (a + b))
440
441/-- The loop that computes the offsets of the lengths in `work`. -/
442theorem offs_loop (f : Nat → Nat) (n : Nat) (hn : n ≤ 288) (count : Array UInt16) (hs : count.size = 16)
443 (hc : ∀ l, 1 ≤ l → l ≤ 15 → (count.getD l 0).toNat = cnt f n l) (h : Heap) :
444 Wp (cwhile offsCond (offsBody count) ((1 : UInt32), (Array.replicate 16 (0 : UInt16)).set! 1 0)) h
445 (fun r h' => h' = h ∧ r.2.size = 16 ∧ ∀ j, 1 ≤ j → j ≤ 15 → (r.2.getD j 0).toNat = Tc f n (j - 1)) := by
446 refine Wp.cwhile
447 (fun (x : UInt32 × Array UInt16) h' => h' = h ∧ 1 ≤ x.1.toNat ∧ x.1.toNat ≤ 15 ∧ x.2.size = 16 ∧
448 ∀ j, 1 ≤ j → j ≤ x.1.toNat → (x.2.getD j 0).toNat = Tc f n (j - 1))
449 (fun (x : UInt32 × Array UInt16) => 15 - x.1.toNat) _ ?_ ?_ ?_
450 · rintro ⟨len, offs⟩ h' ⟨rfl, hl1, hl2, hsz, hj⟩
451 dsimp only at hl1 hl2 hsz hj
452 by_cases hlt : len < MAXBITS
453 · right
454 have hlt' : len.toNat < 15 := by have := UInt32.lt_iff_toNat_lt.mp hlt; exact this
455 have hc1 := hc len.toNat hl1 (by omega)
456 have hlt16 : len.toNat < count.size := by omega
457 have hlt16' : len.toNat < offs.size := by omega
458 have hcc : (count[len.toNat]).toNat = cnt f n len.toNat := by
459 rw [Array.getD_eq_getD_getElem?, Array.getElem?_eq_getElem hlt16] at hc1; simpa using hc1
460 have hoo : (offs[len.toNat]).toNat = Tc f n (len.toNat - 1) := by
461 have := hj len.toNat hl1 (Nat.le_refl _)
462 rw [Array.getD_eq_getD_getElem?, Array.getElem?_eq_getElem hlt16'] at this; simpa using this
463 have hTs := Tc_succ' (f := f) (n := n) hl1
464 have hTle := Tc_le (f := f) len.toNat n
465 have hu : (len + 1).toNat = len.toNat + 1 := u32_succ (by omega)
466 have hsz2 : (len + 1).toNat < offs.size := by omega
467 have hrun : offsBody count (len, offs) = pure (len + 1, offs.set! (len + 1).toNat (offs[len.toNat] + count[len.toNat])) := by
468 simp only [offsBody]
469 rw [geta_eq hlt16', M_pure_bind, geta_eq hlt16, M_pure_bind, seta_eq hsz2, M_pure_bind]
470 have hadd : (offs[len.toNat] + count[len.toNat]).toNat = Tc f n len.toNat := by
471 rw [UInt16.toNat_add, hoo, hcc]
472 have : Tc f n len.toNat = Tc f n (len.toNat - 1) + cnt f n len.toNat := hTs
473 have := Tc_le (f := f) len.toNat n
474 rw [Nat.mod_eq_of_lt (by omega)]
475 omega
476 refine ⟨(len, offs), h', (len + 1, offs.set! (len + 1).toNat (offs[len.toNat] + count[len.toNat])), h', ?_, ?_, ?_, ?_⟩
477 · show (pure (decide (len < MAXBITS), (len, offs)) : M _) h' = _
478 simp [hlt]
479 · rw [hrun]; rfl
480 · refine ⟨rfl, by dsimp only; omega, by dsimp only; omega, by dsimp only; rw [Array.size_set!]; exact hsz, ?_⟩
481 intro j hj1 hj2
482 dsimp only at hj2 ⊢
483 rw [hu] at hj2
484 rw [getD_set!]
485 by_cases hjl : j = len.toNat + 1
486 · rw [ite_eq_left ⟨by rw [hu, hjl], hsz2⟩, hadd, hjl]; rfl
487 · rw [ite_eq_right (fun hh => hjl (by rw [hu] at hh; omega))]
488 exact hj j hj1 (by omega)
489 · dsimp only; omega
490 · left
491 have hn : ¬ (len.toNat < 15) := fun hh => hlt (UInt32.lt_iff_toNat_lt.mpr hh)
492 refine ⟨(len, offs), h', ?_, rfl, hsz, ?_⟩
493 · show (pure (decide (len < MAXBITS), (len, offs)) : M _) h' = _
494 simp [hlt]
495 · intro j hj1 hj2
496 exact hj j hj1 (by omega)
497 · refine ⟨rfl, by decide, by decide, by simp, ?_⟩
498 intro j hj1 hj2
499 have hj3 : j ≤ 1 := hj2
500 have : j = 1 := by omega
501 subst this
502 show ((Array.replicate 16 (0 : UInt16)).set! 1 0 |>.getD 1 0).toNat = Tc f n 0
503 rfl
504 · exact lt_fuel (by simp)
505
506theorem wro (h : Heap) (w : WRef) : Space.ro h w = false := by cases w <;> rfl
507
508theorem wput_self {h : Heap} {w : WRef} {a : Array UInt16} (hg : Space.get h w = some a) : Space.put h w a = h := by
509 cases w with
510 | blk b => simp only [Space.put, Space.get] at *; rw [upd_self _ _ _ hg]
511 | dstate_bl_count d =>
512 simp only [Space.get, Option.map_eq_some_iff] at hg
513 obtain ⟨s, hs, rfl⟩ := hg
514 simp only [Space.put, hs]; rw [upd_self _ _ _ hs]
515 | istate_lens d =>
516 simp only [Space.get, Option.map_eq_some_iff] at hg
517 obtain ⟨s, hs, rfl⟩ := hg
518 simp only [Space.put, hs]; rw [upd_self _ _ _ hs]
519 | istate_work d =>
520 simp only [Space.get, Option.map_eq_some_iff] at hg
521 obtain ⟨s, hs, rfl⟩ := hg
522 simp only [Space.put, hs]; rw [upd_self _ _ _ hs]
523
524theorem cput_self {h : Heap} {r : CodeRef} {a : Array Code} (hg : Space.get h r = some a) : Space.put h r a = h := by
525 cases r with
526 | istate_codes d =>
527 simp only [Space.get, Option.map_eq_some_iff] at hg
528 obtain ⟨s, hs, rfl⟩ := hg
529 simp only [Space.put, hs]; rw [upd_self _ _ _ hs]
530 | st_lenfix => rfl
531 | st_distfix => rfl
532
533theorem cnt_zero (f : Nat → Nat) (l : Nat) : cnt f 0 l = 0 := rfl
534
535def sortCond (codes : UInt32) : UInt32 × Array UInt16 → M (Bool × (UInt32 × Array UInt16)) :=
536 fun (sym, offs) => pure (sym < codes, (sym, offs))
537
538def sortBody (lens work : WPtr) : UInt32 × Array UInt16 → M (UInt32 × Array UInt16) :=
539 fun (sym, offs) => do
540 let l ← lens.index sym.toNat
541 if l != 0 then
542 let l ← lens.index sym.toNat
543 let o ← geta offs l.toNat
544 let offs ← seta offs l.toNat (o + 1)
545 let q ← work.add o.toNat
546 Ptr.store q sym.toUInt16
547 pure (sym + 1, offs)
548 else pure (sym + 1, offs)
549
550/-- What the sort loop has done after it has looked at the symbols below `k`. -/
551def SortInv (f : Nat → Nat) (n ow : Nat) (wa : Array UInt16) (k : Nat) (offs : Array UInt16) (wak : Array UInt16) : Prop :=
552 offs.size = 16 ∧ (∀ l, 1 ≤ l → l ≤ 15 → (offs.getD l 0).toNat = Tc f n (l - 1) + cnt f k l) ∧
553 wak.size = wa.size ∧ (∀ x, (x < ow ∨ ow + n ≤ x) → wak[x]? = wa[x]?) ∧
554 (∀ l j, 1 ≤ l → l ≤ 15 → j < cnt f k l →
555 wak[ow + Tc f n (l - 1) + j]? = some (UInt16.ofNat ((fl f l k).getD j 0)))
556
557theorem sortInv_skip {f : Nat → Nat} {n ow : Nat} {wa offs wak : Array UInt16} {k : Nat} (hf0 : f k = 0)
558 (h : SortInv f n ow wa k offs wak) : SortInv f n ow wa (k + 1) offs wak := by
559 obtain ⟨h1, h2, h3, h4, h5⟩ := h
560 have hc : ∀ l, 1 ≤ l → cnt f (k + 1) l = cnt f k l := by
561 intro l hl; rw [cnt_step, ite_eq_right (by omega)]; rfl
562 have hfl : ∀ l, 1 ≤ l → fl f l (k + 1) = fl f l k := fun l hl => fl_succ_ne (by omega)
563 refine ⟨h1, fun l hl1 hl2 => ?_, h3, h4, fun l j hl1 hl2 hj => ?_⟩
564 · rw [hc l hl1]; exact h2 l hl1 hl2
565 · rw [hc l hl1] at hj; rw [hfl l hl1]; exact h5 l j hl1 hl2 hj
566
567theorem sortInv_step {f : Nat → Nat} {n ow : Nat} {wa offs wak : Array UInt16} {k l : Nat} (hkn : k < n)
568 (hfk : f k = l) (hl1 : 1 ≤ l) (hl2 : l ≤ 15) (hwa : ow + n ≤ wa.size) (hn : n ≤ 288)
569 (h : SortInv f n ow wa k offs wak) :
570 SortInv f n ow wa (k + 1) (offs.set! l (offs.getD l 0 + 1))
571 (wak.set! (ow + (offs.getD l 0).toNat) (UInt16.ofNat k)) := by
572 obtain ⟨h1, h2, h3, h4, h5⟩ := h
573 have hoff := h2 l hl1 hl2
574 have hj0 : cnt f k l < cnt f n l := cnt_lt hkn hfk
575 have hTl := Tc_succ' (f := f) (n := n) hl1
576 have hTn := Tc_le (f := f) l n
577 have hpos : ow + (offs.getD l 0).toNat < wak.size := by omega
578 have hcnew : ∀ l', cnt f (k + 1) l' = cnt f k l' + (if l' = l then 1 else 0) := by
579 intro l'; rw [cnt_step]; by_cases h : l' = l
580 · rw [ite_eq_left (by omega), ite_eq_left h]
581 · rw [ite_eq_right (by omega), ite_eq_right h]
582 have hn65 : (offs.getD l 0).toNat + 1 < 65536 := by omega
583 have hadd : (offs.getD l 0 + 1).toNat = (offs.getD l 0).toNat + 1 := by
584 rw [UInt16.toNat_add]; simp only [UInt16.toNat_one]; exact Nat.mod_eq_of_lt (by omega)
585 refine ⟨by rw [Array.size_set!]; exact h1, fun l' hl1' hl2' => ?_, by rw [Array.size_set!]; exact h3, ?_, ?_⟩
586 · rw [getD_set!, hcnew]
587 by_cases hll : l' = l
588 · subst hll
589 rw [ite_eq_left ⟨rfl, by omega⟩, hadd, ite_eq_left rfl]; omega
590 · rw [ite_eq_right (fun hh => hll hh.1.symm), ite_eq_right hll]; simp only [Nat.add_zero]; exact h2 l' hl1' hl2'
591 · intro x hx
592 have hne : ow + (offs.getD l 0).toNat ≠ x := by omega
593 rw [getElem?_set!_ne hne]; exact h4 x hx
594 · intro l' j hl1' hl2' hj
595 rw [hcnew] at hj
596 have hTs' := Tc_succ' (f := f) (n := n) hl1'
597 have hTle' : Tc f n l' ≤ n := Tc_le l' n
598 have hcm := cnt_mono (f := f) (l := l') (show k ≤ n by omega)
599 have hset : ∀ pos, (wak.set! (ow + (offs.getD l 0).toNat) (UInt16.ofNat k))[pos]? =
600 if ow + (offs.getD l 0).toNat = pos then some (UInt16.ofNat k) else wak[pos]? := by
601 intro pos
602 rw [Array.set!_eq_setIfInBounds, Array.getElem?_setIfInBounds]
603 by_cases hp : ow + (offs.getD l 0).toNat = pos
604 · rw [ite_eq_left hp, ite_eq_left hp, ite_eq_left (by omega)]
605 · rw [ite_eq_right hp, ite_eq_right hp]
606 by_cases hll : l' = l
607 · subst hll
608 rw [ite_eq_left rfl] at hj
609 by_cases hjj : j = cnt f k l'
610 · subst hjj
611 rw [hset, ite_eq_left (by omega), fl_getD_new hfk]
612 · have hjlt : j < cnt f k l' := by omega
613 rw [hset, ite_eq_right (by omega), h5 l' j hl1' hl2' hjlt, fl_getD_old hfk hjlt]
614 · rw [ite_eq_right hll] at hj
615 simp only [Nat.add_zero] at hj
616 have hne : ow + (offs.getD l 0).toNat ≠ ow + Tc f n (l' - 1) + j := by
617 rcases Nat.lt_or_gt_of_ne hll with hlt | hgt
618 · have m1 := Tc_mono (f := f) (n := n) (show l' ≤ l - 1 by omega)
619 omega
620 · have m2 := Tc_mono (f := f) (n := n) (show l ≤ l' - 1 by omega)
621 omega
622 rw [hset, ite_eq_right hne, h5 l' j hl1' hl2' hj, fl_succ_ne (by omega)]
623
624theorem sort_loop (f : Nat → Nat) (n : Nat) (hn : n ≤ 288) (rl rw : WRef) (hne : rw ≠ rl) (ol ow : Nat)
625 (la wa : Array UInt16) (codes : UInt32) (hcodes : codes.toNat = n) (h : Heap)
626 (hgl : Space.get h rl = some la) (hgw : Space.get h rw = some wa) (hla : ol + n ≤ la.size)
627 (hf : ∀ k, f k = (la.getD (ol + k) 0).toNat) (hf15 : ∀ k, k < n → f k ≤ 15) (hwa : ow + n ≤ wa.size)
628 (offs0 : Array UInt16) (ho : offs0.size = 16)
629 (ho' : ∀ j, 1 ≤ j → j ≤ 15 → (offs0.getD j 0).toNat = Tc f n (j - 1)) :
630 Wp (cwhile (sortCond codes) (sortBody (Ptr.ref rl ol) (Ptr.ref rw ow)) ((0 : UInt32), offs0)) h
631 (fun r h' => r.1.toNat = n ∧ ∃ wa', h' = Space.put h rw wa' ∧ SortInv f n ow wa n r.2 wa') := by
632 refine Wp.cwhile
633 (fun (x : UInt32 × Array UInt16) h' => x.1.toNat ≤ n ∧ ∃ wak, h' = Space.put h rw wak ∧ SortInv f n ow wa x.1.toNat x.2 wak)
634 (fun (x : UInt32 × Array UInt16) => n - x.1.toNat) _ ?_ ?_ ?_
635 · rintro ⟨sym, offs⟩ h' ⟨hsn, wak, rfl, hinv⟩
636 dsimp only at hsn hinv
637 by_cases hlt : sym < codes
638 · right
639 have hk : sym.toNat < n := by have := UInt32.lt_iff_toNat_lt.mp hlt; omega
640 have hglw : Space.get (Space.put h rw wak) rw = some wak := wget_put_self hgw wak
641 have hgll : Space.get (Space.put h rw wak) rl = some la := by rw [wget_put_ne hne]; exact hgl
642 have hkl : ol + sym.toNat < la.size := by omega
643 have hfk : f sym.toNat = (la[ol + sym.toNat]'hkl).toNat := by
644 rw [hf, Array.getD_eq_getD_getElem?, Array.getElem?_eq_getElem hkl]; simp
645 have hcond : sortCond codes (sym, offs) (Space.put h rw wak) = .ok ((true, (sym, offs)), Space.put h rw wak) := by
646 show (pure (decide (sym < codes), (sym, offs)) : M _) _ = _
647 simp [hlt]
648 have hw : Wp (sortBody (Ptr.ref rl ol) (Ptr.ref rw ow) (sym, offs)) (Space.put h rw wak)
649 (fun r h2 => ∃ wak', h2 = Space.put h rw wak' ∧ r.1.toNat = sym.toNat + 1 ∧
650 SortInv f n ow wa (sym.toNat + 1) r.2 wak') := by
651 simp only [sortBody]
652 apply Wp.bind' (Q := fun r h2 => r = la[ol + sym.toNat]'hkl ∧ h2 = Space.put h rw wak)
653 (Wp.of_eq (Ptr.index_ok hgll hkl) ⟨rfl, rfl⟩)
654 rintro l h2 ⟨rfl, rfl⟩
655 have hu : (sym + 1).toNat = sym.toNat + 1 := u32_succ (by omega)
656 by_cases hl0 : (la[ol + sym.toNat]'hkl != 0) = true
657 · rw [ite_eq_left hl0]
658 have hl0' : f sym.toNat ≠ 0 := by
659 rw [hfk]; intro h0
660 apply (by simpa using hl0 : ¬ (la[ol + sym.toNat]'hkl = 0))
661 exact UInt16.toNat_inj.mp (by rw [h0]; rfl)
662 have hf15' := hf15 sym.toNat hk
663 apply Wp.bind' (Q := fun r h2 => r = la[ol + sym.toNat]'hkl ∧ h2 = Space.put h rw wak)
664 (Wp.of_eq (Ptr.index_ok hgll hkl) ⟨rfl, rfl⟩)
665 rintro l2 h2 ⟨rfl, rfl⟩
666 have hlt16 : (la[ol + sym.toNat]'hkl).toNat < offs.size := by rw [← hfk, hinv.1]; omega
667 apply Wp.bind' (Q := fun r h2 => r = offs[(la[ol + sym.toNat]'hkl).toNat]'hlt16 ∧ h2 = Space.put h rw wak)
668 (Wp.pure_eq (geta_eq hlt16) ⟨rfl, rfl⟩)
669 rintro o h2 ⟨rfl, rfl⟩
670 apply Wp.bind' (Q := fun r h2 => r = offs.set! (la[ol + sym.toNat]'hkl).toNat
671 (offs[(la[ol + sym.toNat]'hkl).toNat]'hlt16 + 1) ∧ h2 = Space.put h rw wak)
672 (Wp.pure_eq (seta_eq hlt16) ⟨rfl, rfl⟩)
673 rintro offs2 h2 ⟨rfl, rfl⟩
674 have hog : (offs.getD (f sym.toNat) 0) = offs[(la[ol + sym.toNat]'hkl).toNat]'hlt16 := by
675 rw [hfk, Array.getD_eq_getD_getElem?, Array.getElem?_eq_getElem hlt16]; simp
676 have hoff := hinv.2.1 (f sym.toNat) (by omega) hf15'
677 have hj0 := cnt_lt (f := f) hk rfl
678 have hTl := Tc_succ' (f := f) (n := n) (show 1 ≤ f sym.toNat by omega)
679 have hTn := Tc_le (f := f) (f sym.toNat) n
680 have hobd : ow + (offs[(la[ol + sym.toNat]'hkl).toNat]'hlt16).toNat < wak.size := by
681 have := hinv.2.2.1
682 rw [← hog]; omega
683 apply Wp.bind' (Q := fun q h2 => q = Ptr.ref rw (ow + (offs[(la[ol + sym.toNat]'hkl).toNat]'hlt16).toNat) ∧
684 h2 = Space.put h rw wak)
685 (Wp.of_eq (Ptr.add_nat_ok hglw (by omega)) ⟨rfl, rfl⟩)
686 rintro q h2 ⟨rfl, rfl⟩
687 apply Wp.bind' (Q := fun _ h2 => h2 = Space.put h rw
688 (wak.set! (ow + (offs[(la[ol + sym.toNat]'hkl).toNat]'hlt16).toNat) sym.toUInt16))
689 · refine ⟨(), _, Ptr.store_ok hglw (wro _ _) hobd, ?_⟩
690 rw [wput_put]
691 · rintro _ h2 rfl
692 refine Wp.pure' ⟨_, rfl, hu, ?_⟩
693 have hsy : sym.toUInt16 = UInt16.ofNat sym.toNat := by
694 apply UInt16.toNat_inj.mp
695 rw [UInt32.toNat_toUInt16, UInt16.toNat_ofNat']
696 rw [hsy, ← hog]
697 have := sortInv_step (f := f) (n := n) (ow := ow) (wa := wa) (offs := offs) (wak := wak) (k := sym.toNat)
698 (l := f sym.toNat) hk rfl (by omega) hf15' hwa hn hinv
699 show SortInv f n ow wa (sym.toNat + 1) (offs.set! (la[ol + sym.toNat]'hkl).toNat (offs.getD (f sym.toNat) 0 + 1))
700 (wak.set! (ow + (offs.getD (f sym.toNat) 0).toNat) (UInt16.ofNat sym.toNat))
701 rw [← hfk]
702 exact this
703 · rw [ite_eq_right hl0]
704 have hf0 : f sym.toNat = 0 := by
705 have : (la[ol + sym.toNat]'hkl) = 0 := by simpa using hl0
706 rw [hfk, this]; rfl
707 exact Wp.pure' ⟨wak, rfl, hu, sortInv_skip hf0 hinv⟩
708 obtain ⟨s2, h2, hrun, wak', rfl, hs2, hinv'⟩ := hw
709 refine ⟨(sym, offs), _, s2, _, hcond, hrun, ⟨by omega, wak', rfl, by rw [hs2]; exact hinv'⟩, ?_⟩
710 dsimp only; omega
711 · left
712 have hsn' : sym.toNat = n := by
713 have : ¬ sym.toNat < n := fun hh => hlt (by rw [UInt32.lt_iff_toNat_lt, hcodes]; exact hh)
714 omega
715 refine ⟨(sym, offs), _, ?_, ⟨hsn', wak, rfl, by have := hinv; rw [hsn'] at this; exact this⟩⟩
716 show (pure (decide (sym < codes), (sym, offs)) : M _) _ = _
717 simp [hlt]
718 · refine ⟨by simp [hcodes], wa, ?_, ?_⟩
719 · rw [wput_self hgw]
720 · refine ⟨ho, fun l hl1 hl2 => ?_, rfl, fun _ _ => rfl, fun l j _ _ hj => ?_⟩
721 · show (offs0.getD l 0).toNat = Tc f n (l - 1) + cnt f 0 l
722 rw [cnt_zero]; exact ho' l hl1 hl2
723 · have hj' : j < cnt f 0 l := hj
724 rw [cnt_zero] at hj'; omega
725 · exact lt_fuel (by omega)
726
727theorem ws_getD {f : Nat → Nat} {n i : Nat} (hi : i < Tc f n 15) :
728 (wsAux f n 15).getD i 0 = (fl f (lenAt f n i) n).getD (i - Tc f n (lenAt f n i - 1)) 0 := by
729 obtain ⟨b1, b2⟩ := lenAt_bounds (f := f) (n := n) hi
730 have blk := (lenAt_eq_iff (f := f) (n := n) (l := lenAt f n i) b1 b2 hi).mp rfl
731 obtain ⟨rest, h1, _⟩ := wsAux_split (f := f) (n := n) b2
732 obtain ⟨ℓ, hℓ⟩ : ∃ ℓ, ℓ = lenAt f n i := ⟨_, rfl⟩
733 rw [← hℓ] at b1 b2 blk h1 ⊢
734 obtain ⟨m, rfl⟩ : ∃ m, ℓ = m + 1 := ⟨ℓ - 1, by omega⟩
735 have hA : (wsAux f n m).length = Tc f n m := wsAux_length m
736 have hB : (fl f (m + 1) n).length = cnt f n (m + 1) := rfl
737 have hT : Tc f n (m + 1) = Tc f n m + cnt f n (m + 1) := rfl
738 simp only [Nat.add_sub_cancel] at blk ⊢
739 rw [h1, show wsAux f n (m + 1) = wsAux f n m ++ fl f (m + 1) n from rfl, List.append_assoc,
740 List.getD_eq_getElem?_getD, List.getD_eq_getElem?_getD,
741 List.getElem?_append_right (by omega)]
742 rw [hA, List.getElem?_append_left (show i - Tc f n m < (fl f (m + 1) n).length by omega)]
743
744/-- What the result code says about the lengths. -/
745def RetInfo (type : UInt32) (f : Nat → Nat) (n : Nat) (r : Int32 × CodePtr × UInt32) : Prop :=
746 (r.1 = 0 → Acc type f n) ∧ (r.1 = 1 → Acc type f n ∧ type ≠ CODES) ∧ (r.1 = -1 → ¬ Acc type f n)
747
748theorem incomplete_one {f : Nat → Nat} {n : Nat} (hpos : 0 < Tc f n 15) (hfit : Fits f n)
749 (hlt : Kc f n 15 < 2 ^ 15) (hmx : mxl f n = 1) : Tc f n 15 = 1 := by
750 have hl := lenAt_le_iff (f := f) (n := n) (i := Tc f n 15 - 1) (l := 1) (by omega) (by omega)
751 have h1 : Tc f n 15 - 1 < Tc f n 1 := hl.mp (by unfold mxl at hmx; omega)
752 have hm := Tc_mono (f := f) (n := n) (show 1 ≤ 15 by omega)
753 have hT : Tc f n (1 + 14) = Tc f n 1 := by simp only [Nat.reduceAdd]; omega
754 have hK := Kc_gap (f := f) (n := n) 1 14 hT
755 have hK1 : Kc f n 1 = cnt f n 1 := by simp [Kc]
756 have hT1 : Tc f n 1 = cnt f n 1 := by simp [Tc]
757 simp only [Nat.reduceAdd] at hK
758 rw [hK1] at hK
759 have hfit1 := hfit 1 (by omega) (by omega)
760 rw [hK1] at hfit1
761 omega
762
763/-- The inputs of the call that `zlib.h` and `inflate.c` allow (the part that lives in the heap). -/
764structure CallPre (h : Heap) (type : UInt32) (rl : WRef) (ol : Nat) (codes : UInt32) (rc : CodeRef) (oc : Nat)
765 (bits : UInt32) (rw : WRef) (ow : Nat) where
766 la : Array UInt16
767 wa : Array UInt16
768 ca : Array Code
769 hty : type = CODES ∨ type = LENS ∨ type = DISTS
770 hgl : Space.get h rl = some la
771 hgw : Space.get h rw = some wa
772 hgc : Space.get h rc = some ca
773 hro : Space.ro h rc = false
774 hne : rw ≠ rl
775 hla : ol + codes.toNat ≤ la.size
776 hwa : ow + codes.toNat ≤ wa.size
777 hca : oc + capOf type ≤ ca.size
778 hf15 : ∀ k, k < codes.toNat → (la.getD (ol + k) 0).toNat ≤ 15
779 hcodes : type = CODES → codes.toNat ≤ 19 ∧ (∀ k, k < codes.toNat → (la.getD (ol + k) 0).toNat ≤ 7) ∧ 7 ≤ bits.toNat
780 hlens : type = LENS → codes.toNat ≤ 288
781 hdists : type = DISTS → codes.toNat ≤ 32
782
783def CallPre.f {h : Heap} {type : UInt32} {rl : WRef} {ol : Nat} {codes : UInt32} {rc : CodeRef} {oc : Nat}
784 {bits : UInt32} {rw : WRef} {ow : Nat} (P : CallPre h type rl ol codes rc oc bits rw ow) (k : Nat) : Nat :=
785 (P.la.getD (ol + k) 0).toNat
786
787theorem Result.unchanged {h : Heap} {rw : WRef} {rc : CodeRef} {ow oc cap n : Nat} {wa : Array UInt16}
788 {ca : Array Code} {table : CodePtr} {bits : UInt32} {r : Int32 × CodePtr × UInt32}
789 (hgw : Space.get h rw = some wa) (hgc : Space.get h rc = some ca) (hr : (r.1 = 1 ∨ r.1 = -1) ∧ r.2.1 = table ∧ r.2.2 = bits) :
790 Result h rw rc ow oc cap n wa ca table bits r h := by
791 refine ⟨wa, ca, ?_, rfl, rfl, fun _ _ => rfl, fun _ _ => rfl, Or.inr hr⟩
792 rw [wput_self hgw, cput_self hgc]
793
794theorem itB_wp {h : Heap} {type : UInt32} {rl : WRef} {ol : Nat} {codes : UInt32} {rc : CodeRef} {oc : Nat}
795 {bits : UInt32} {rw : WRef} {ow : Nat} (P : CallPre h type rl ol codes rc oc bits rw ow)
796 (count : Array UInt16) (max min root : UInt32)
797 (hcs : count.size = 16) (hcc : ∀ l, 1 ≤ l → l ≤ 15 → (count.getD l 0).toNat = cnt P.f codes.toNat l)
798 (hmax : max.toNat = mxl P.f codes.toNat) (hpos : 0 < Tc P.f codes.toNat 15)
799 (hmin : min.toNat = lenAt P.f codes.toNat 0)
800 (hr1 : 1 ≤ root.toNat) (hr0 : lenAt P.f codes.toNat 0 ≤ root.toNat) (hrm : root.toNat ≤ mxl P.f codes.toNat)
801 (hrC : type = CODES → root.toNat = mxl P.f codes.toNat) :
802 Wp (itB type (Ptr.ref rl ol) codes (Ptr.ref rc oc) bits (Ptr.ref rw ow) count max min root) h
803 (fun r h' => Result h rw rc ow oc (capOf type) codes.toNat P.wa P.ca (Ptr.ref rc oc) bits r h' ∧
804 RetInfo type P.f codes.toNat r) := by
805 unfold itB
806 apply Wp.bind' (kraft_loop P.f codes.toNat count hcs hcc h)
807 rintro ⟨left, bad, len⟩ h' ⟨rfl, hk⟩
808 dsimp only at hk ⊢
809 by_cases hbad : bad = true
810 · rw [ite_eq_left hbad]
811 have hnf : ¬ Fits P.f codes.toNat := by
812 rcases hk with ⟨_, h2⟩ | ⟨h1, _⟩
813 · exact h2
814 · exact absurd (hbad.symm.trans h1) (by decide)
815 exact Wp.pure' ⟨Result.unchanged P.hgw P.hgc ⟨Or.inr rfl, rfl, rfl⟩,
816 fun h => absurd (show (-1 : Int32) = 0 from h) (by decide),
817 fun h => absurd (show (-1 : Int32) = 1 from h) (by decide), fun _ hacc => hnf hacc.1⟩
818 · rw [ite_eq_right hbad]
819 have hbad' : bad = false := by simpa using hbad
820 obtain ⟨hfit, hleft⟩ : Fits P.f codes.toNat ∧ left.toInt = 2 ^ 15 - (Kc P.f codes.toNat 15 : Int) := by
821 rcases hk with ⟨h1, _⟩ | ⟨_, h2, h3⟩
822 · exact absurd h1 hbad
823 · exact ⟨h2, h3⟩
824 have hK15 := hfit 15 (by omega) (by omega)
825 by_cases hg : (decide (left > 0) && (type == CODES || max != 1)) = true
826 · rw [ite_eq_left hg]
827 have hgl' : left > 0 ∧ (type == CODES || max != 1) = true := by
828 simpa [Bool.and_eq_true, decide_eq_true_eq] using hg
829 have hl' : 0 < left.toInt := by
830 have := Int32.lt_iff_toInt_lt.mp hgl'.1; simpa using this
831 have hnacc : ¬ Acc type P.f codes.toNat := by
832 rintro ⟨_, h2 | h2 | ⟨hnc, hm1, _⟩⟩
833 · omega
834 · omega
835 · have hmax1 : max = 1 := UInt32.toNat_inj.mp (by rw [hmax, hm1]; rfl)
836 have := hgl'.2
837 simp [hnc, hmax1] at this
838 exact Wp.pure' ⟨Result.unchanged P.hgw P.hgc ⟨Or.inr rfl, rfl, rfl⟩,
839 fun h => absurd (show (-1 : Int32) = 0 from h) (by decide),
840 fun h => absurd (show (-1 : Int32) = 1 from h) (by decide), fun _ => hnacc⟩
841 · rw [ite_eq_right hg]
842 have hend : Kc P.f codes.toNat 15 = 2 ^ 15 ∨ (mxl P.f codes.toNat = 1 ∧ Tc P.f codes.toNat 15 = 1 ∧ type ≠ CODES) := by
843 by_cases hl : left > 0
844 · right
845 have hl' : 0 < left.toInt := by
846 have := Int32.lt_iff_toInt_lt.mp hl; simpa using this
847 have hnc1 : type ≠ CODES := fun ht => hg (by simp [hl, ht])
848 have hnc2 : max = 1 := Classical.byContradiction (fun hne => hg (by simp [hl, hne]))
849 have hm1 : mxl P.f codes.toNat = 1 := by
850 have := congrArg UInt32.toNat hnc2; rw [hmax] at this; simpa using this
851 have hlt : Kc P.f codes.toNat 15 < 2 ^ 15 := by
852 have : (Kc P.f codes.toNat 15 : Int) < 2 ^ 15 := by omega
853 exact_mod_cast this
854 exact ⟨hm1, incomplete_one hpos hfit hlt hm1, hnc1⟩
855 · left
856 have hl' : left.toInt ≤ 0 := by
857 have : ¬ (0 < left.toInt) := fun hh => hl (Int32.lt_iff_toInt_lt.mpr (by simpa using hh))
858 omega
859 have : (2 ^ 15 : Int) ≤ Kc P.f codes.toNat 15 := by omega
860 have : 2 ^ 15 ≤ Kc P.f codes.toNat 15 := by exact_mod_cast this
861 omega
862 have hn288 : codes.toNat ≤ 288 := by
863 rcases P.hty with ht | ht | ht
864 · have := (P.hcodes ht).1; omega
865 · exact P.hlens ht
866 · have := P.hdists ht; omega
867 rw [seta_eq (by simp)]
868 rw [M_pure_bind]
869 apply Wp.bind' (offs_loop P.f codes.toNat hn288 count hcs hcc _)
870 rintro ⟨len2, offs⟩ h' ⟨rfl, hos, hoj⟩
871 dsimp only at hos hoj ⊢
872 apply Wp.bind' (sort_loop P.f codes.toNat hn288 rl rw P.hne ol ow P.la P.wa codes rfl _ P.hgl P.hgw P.hla
873 (fun k => rfl) P.hf15 P.hwa offs hos hoj)
874 rintro ⟨sym, offs'⟩ h2 ⟨hsym, wa1, rfl, hinv⟩
875 dsimp only at hinv ⊢
876 obtain ⟨_, _, hsz1, hfr1, hcont1⟩ := hinv
877 have key : ∀ (base extra : Array UInt16) (match_ : UInt32),
878 (type = CODES → match_ = 20) →
879 (type = LENS → base = lbase ∧ extra = lext ∧ match_ = 257) →
880 (type = DISTS → base = dbase ∧ extra = dext ∧ match_ = 0) →
881 Wp (itTail type (Ptr.ref rl ol) (Ptr.ref rc oc) bits (Ptr.ref rw ow) count max min root left base extra match_)
882 (Space.put h' rw wa1)
883 (fun r h2 => Result h' rw rc ow oc (capOf type) codes.toNat P.wa P.ca (Ptr.ref rc oc) bits r h2 ∧
884 RetInfo type P.f codes.toNat r) := by
885 intro base extra match_ hC hL hD
886 let c0 : Ctx := { type, lens := Ptr.ref rl ol, work := Ptr.ref rw ow, table := Ptr.ref rc oc, root, max, base, extra, match_ }
887 let e : Env :=
888 { c := c0,
889 f := P.f, n := codes.toNat, R := root.toNat, cap := capOf type, rc := rc, oc := oc, «rw» := «rw», ow := ow,
890 rl := rl, ol := ol, hb := Space.put h' rw wa1, la := P.la, wa := wa1,
891 h_table := rfl, h_lens := rfl, h_work := rfl, h_ro := P.hro,
892 h_live := ⟨P.ca, by rw [cget_put_word]; exact P.hgc⟩,
893 h_get_la := by rw [wget_put_ne P.hne]; exact P.hgl,
894 h_get_wa := wget_put_self P.hgw wa1, h_f := fun k => rfl, h_la := P.hla, h_f15 := P.hf15,
895 h_wa := by rw [hsz1]; exact P.hwa,
896 h_wcont := fun i hi => by
897 have hb := lenAt_bounds (f := P.f) (n := codes.toNat) hi
898 have blk := (lenAt_eq_iff (f := P.f) (n := codes.toNat) (l := lenAt P.f codes.toNat i) hb.1 hb.2 hi).mp rfl
899 have hlt : i - Tc P.f codes.toNat (lenAt P.f codes.toNat i - 1) < cnt P.f codes.toNat (lenAt P.f codes.toNat i) := by
900 have := Tc_succ' (f := P.f) (n := codes.toNat) hb.1
901 omega
902 have := hcont1 (lenAt P.f codes.toNat i) (i - Tc P.f codes.toNat (lenAt P.f codes.toNat i - 1)) hb.1 hb.2 hlt
903 rw [show ow + Tc P.f codes.toNat (lenAt P.f codes.toNat i - 1) + (i - Tc P.f codes.toNat (lenAt P.f codes.toNat i - 1)) = ow + i by omega] at this
904 rw [this, ws_getD hi],
905 h_n := hn288, h_root := rfl, h_max := hmax, h_R1 := hr1, h_Rmx := hrm, h_R0 := hr0, h_pos := hpos,
906 h_fits := hfit, h_end := hend, h_type := P.hty, h_cap := rfl,
907 h_codes := fun ht => ⟨by
908 have hall := (P.hcodes ht).2.1
909 show lenAt P.f codes.toNat (Tc P.f codes.toNat 15 - 1) ≤ 7
910 unfold lenAt
911 exact hall _ (ws_getD_lt (by omega)), hrC ht, (P.hcodes ht).1, hC ht⟩,
912 h_lens' := fun ht => ⟨hn288, hL ht⟩, h_dists := fun ht => ⟨(P.hdists ht), hD ht⟩ }
913 have hcnt0 : CountOK e count 0 := ⟨hcs, fun l h1 h2 => by
914 rw [hcc l h1 h2]; exact (rem_zero (f := P.f) (n := codes.toNat) h1).symm⟩
915 have hhc : e.hc P.ca = Space.put h' rw wa1 :=
916 cput_self (by rw [cget_put_word]; exact P.hgc)
917 have := itTail_wp e P.ca count bits min left hcnt0 hmin P.hca
918 rw [hhc] at this
919 refine Wp.mono this ?_
920 rintro r h3 ⟨ca', rfl, hf, hr, hrne⟩
921 have hacc : Acc type P.f codes.toNat := by
922 refine ⟨hfit, ?_⟩
923 rcases hend with h | ⟨a, b, c⟩
924 · exact Or.inl h
925 · exact Or.inr (Or.inr ⟨c, a, b⟩)
926 have hr01 : r.1 = 0 ∨ r.1 = 1 := by
927 rcases hr with ⟨h0, _⟩ | ⟨h1, _⟩
928 · exact Or.inl h0
929 · exact Or.inr h1
930 refine ⟨⟨wa1, ca', rfl, hsz1, hf.1.trans rfl, hfr1, hf.2, ?_⟩,
931 fun _ => hacc, fun h1 => ⟨hacc, hrne.1 h1⟩, fun hm => ?_⟩
932 · rcases hr with ⟨h0, u, hu, hr2, _⟩ | ⟨h1, h2, h3⟩
933 · exact Or.inl ⟨h0, u, hu, hr2⟩
934 · exact Or.inr ⟨Or.inl h1, h2, h3⟩
935 · exfalso
936 rcases hr01 with h0 | h0 <;> rw [h0] at hm <;> exact absurd hm (by decide)
937 rcases P.hty with ht | ht | ht
938 · subst ht
939 rw [ite_eq_left (by decide)]
940 exact key #[] #[] 20 (fun _ => rfl) (fun h => absurd h (by decide)) (fun h => absurd h (by decide))
941 · subst ht
942 rw [ite_eq_right (by decide), ite_eq_left (by decide)]
943 exact key lbase lext 257 (fun h => absurd h (by decide)) (fun _ => ⟨rfl, rfl, rfl⟩) (fun h => absurd h (by decide))
944 · subst ht
945 rw [ite_eq_right (by decide), ite_eq_right (by decide), ite_eq_left (by decide)]
946 exact key dbase dext 0 (fun h => absurd h (by decide)) (fun h => absurd h (by decide)) (fun _ => ⟨rfl, rfl, rfl⟩)
947
948theorem Tc_gap {f : Nat → Nat} {n : Nat} : ∀ a d, (∀ j, a < j → j ≤ a + d → cnt f n j = 0) → Tc f n (a + d) = Tc f n a
949 | a, 0, _ => rfl
950 | a, d + 1, h => by
951 have ih := Tc_gap a d (fun j h1 h2 => h j h1 (by omega))
952 have : Tc f n (a + (d + 1)) = Tc f n (a + d) + cnt f n (a + d + 1) := rfl
953 rw [this, ih, h (a + d + 1) (by omega) (by omega)]
954 rfl
955
956theorem mxl_eq {f : Nat → Nat} {n M : Nat} (hpos : 0 < Tc f n 15) (hM1 : 1 ≤ M) (hM2 : M ≤ 15)
957 (hc : cnt f n M ≠ 0) (hgt : ∀ j, M < j → j ≤ 15 → cnt f n j = 0) : mxl f n = M := by
958 have hT : Tc f n 15 = Tc f n M := by
959 have := Tc_gap (f := f) (n := n) M (15 - M) (fun j h1 h2 => hgt j h1 (by omega))
960 rwa [show M + (15 - M) = 15 by omega] at this
961 have hTs := Tc_succ' (f := f) (n := n) hM1
962 have hi : Tc f n 15 - 1 < Tc f n 15 := by omega
963 have := (lenAt_eq_iff (f := f) (n := n) (i := Tc f n 15 - 1) (l := M) hM1 hM2 hi).mpr ⟨by omega, by omega⟩
964 exact this
965
966theorem min_facts {f : Nat → Nat} {n : Nat} (hpos : 0 < Tc f n 15) :
967 (∀ j, 1 ≤ j → j < lenAt f n 0 → cnt f n j = 0) ∧ cnt f n (lenAt f n 0) ≠ 0 := by
968 obtain ⟨b1, b2⟩ := lenAt_bounds (f := f) (n := n) hpos
969 have blk := (lenAt_eq_iff (f := f) (n := n) (l := lenAt f n 0) b1 b2 hpos).mp rfl
970 have hTs := Tc_succ' (f := f) (n := n) b1
971 refine ⟨fun j hj1 hj2 => ?_, by omega⟩
972 have hm := Tc_mono (f := f) (n := n) (show j ≤ lenAt f n 0 - 1 by omega)
973 have := Tc_succ' (f := f) (n := n) hj1
974 omega
975
976def zeroCond : UInt32 × Array UInt16 → M (Bool × (UInt32 × Array UInt16)) :=
977 fun (len, count) => pure (len ≤ MAXBITS, (len, count))
978
979def zeroBody : UInt32 × Array UInt16 → M (UInt32 × Array UInt16) :=
980 fun (len, count) => do pure (len + 1, ← seta count len.toNat 0)
981
982theorem zero_loop (h : Heap) :
983 Wp (cwhile zeroCond zeroBody ((0 : UInt32), Array.replicate 16 (0 : UInt16))) h
984 (fun r h' => h' = h ∧ r.2.size = 16 ∧ ∀ l, l < 16 → (r.2.getD l 0).toNat = 0) := by
985 refine Wp.cwhile
986 (fun (x : UInt32 × Array UInt16) h' => h' = h ∧ x.1.toNat ≤ 16 ∧ x.2.size = 16 ∧ ∀ l, l < 16 → (x.2.getD l 0).toNat = 0)
987 (fun (x : UInt32 × Array UInt16) => 16 - x.1.toNat) _ ?_ ?_ ?_
988 · rintro ⟨len, count⟩ h' ⟨rfl, hl, hsz, hz⟩
989 dsimp only at hl hsz hz
990 by_cases hle : len ≤ MAXBITS
991 · right
992 have hle' : len.toNat ≤ 15 := UInt32.le_iff_toNat_le.mp hle
993 have hu : (len + 1).toNat = len.toNat + 1 := u32_succ (by omega)
994 have hlt : len.toNat < count.size := by omega
995 refine ⟨(len, count), h', (len + 1, count.set! len.toNat 0), h', ?_, ?_, ?_, ?_⟩
996 · show (pure (decide (len ≤ MAXBITS), (len, count)) : M _) h' = _
997 simp [hle]
998 · show (do pure (len + 1, ← seta count len.toNat 0) : M _) h' = _
999 rw [seta_eq hlt]; rfl
1000 · refine ⟨rfl, by dsimp only; omega, by dsimp only; rw [Array.size_set!]; exact hsz, fun l hl2 => ?_⟩
1001 dsimp only
1002 rw [getD_set!]
1003 by_cases hh : len.toNat = l
1004 · rw [ite_eq_left ⟨hh, hlt⟩]; rfl
1005 · rw [ite_eq_right (fun hh2 => hh hh2.1)]; exact hz l hl2
1006 · dsimp only; omega
1007 · left
1008 have hn : 16 ≤ len.toNat := by
1009 have := (not_congr UInt32.le_iff_toNat_le).mp hle
1010 have h15 : MAXBITS.toNat = 15 := rfl
1011 omega
1012 refine ⟨(len, count), h', ?_, rfl, hsz, hz⟩
1013 show (pure (decide (len ≤ MAXBITS), (len, count)) : M _) h' = _
1014 simp [hle]
1015 · refine ⟨rfl, by decide, by simp, fun l hl => ?_⟩
1016 simp [Array.getD_eq_getD_getElem?, Array.getElem?_replicate, hl]
1017 · exact lt_fuel (by simp)
1018
1019def countCond (codes : UInt32) : UInt32 × Array UInt16 → M (Bool × (UInt32 × Array UInt16)) :=
1020 fun (sym, count) => pure (sym < codes, (sym, count))
1021
1022def countBody (lens : WPtr) : UInt32 × Array UInt16 → M (UInt32 × Array UInt16) :=
1023 fun (sym, count) => do
1024 let l ← lens.index sym.toNat
1025 let c ← geta count l.toNat
1026 pure (sym + 1, ← seta count l.toNat (c + 1))
1027
1028theorem count_loop (f : Nat → Nat) (n : Nat) (hn : n ≤ 288) (rl : WRef) (ol : Nat) (la : Array UInt16)
1029 (codes : UInt32) (hcodes : codes.toNat = n) (h : Heap) (hgl : Space.get h rl = some la) (hla : ol + n ≤ la.size)
1030 (hf : ∀ k, f k = (la.getD (ol + k) 0).toNat) (hf15 : ∀ k, k < n → f k ≤ 15)
1031 (count0 : Array UInt16) (hs0 : count0.size = 16) (hz0 : ∀ l, l < 16 → (count0.getD l 0).toNat = 0) :
1032 Wp (cwhile (countCond codes) (countBody (Ptr.ref rl ol)) ((0 : UInt32), count0)) h
1033 (fun r h' => h' = h ∧ r.1.toNat = n ∧ r.2.size = 16 ∧ ∀ l, l < 16 → (r.2.getD l 0).toNat = cnt f n l) := by
1034 refine Wp.cwhile
1035 (fun (x : UInt32 × Array UInt16) h' => h' = h ∧ x.1.toNat ≤ n ∧ x.2.size = 16 ∧
1036 ∀ l, l < 16 → (x.2.getD l 0).toNat = cnt f x.1.toNat l)
1037 (fun (x : UInt32 × Array UInt16) => n - x.1.toNat) _ ?_ ?_ ?_
1038 · rintro ⟨sym, count⟩ h' ⟨rfl, hsn, hsz, hcn⟩
1039 dsimp only at hsn hsz hcn
1040 by_cases hlt : sym < codes
1041 · right
1042 have hk : sym.toNat < n := by have := UInt32.lt_iff_toNat_lt.mp hlt; omega
1043 have hkl : ol + sym.toNat < la.size := by omega
1044 have hfk : f sym.toNat = (la[ol + sym.toNat]'hkl).toNat := by
1045 rw [hf, Array.getD_eq_getD_getElem?, Array.getElem?_eq_getElem hkl]; simp
1046 have hf15' := hf15 sym.toNat hk
1047 have hlt16 : (la[ol + sym.toNat]'hkl).toNat < count.size := by rw [← hfk, hsz]; omega
1048 have hcnt := hcn (la[ol + sym.toNat]'hkl).toNat (by omega)
1049 rw [Array.getD_eq_getD_getElem?, Array.getElem?_eq_getElem hlt16] at hcnt
1050 simp only [Option.getD_some] at hcnt
1051 have hcle := cnt_le (f := f) (la[ol + sym.toNat]'hkl).toNat sym.toNat
1052 have hu : (sym + 1).toNat = sym.toNat + 1 := u32_succ (by omega)
1053 have hw : Wp (countBody (Ptr.ref rl ol) (sym, count)) h'
1054 (fun r h2 => h2 = h' ∧ r = (sym + 1, count.set! (la[ol + sym.toNat]'hkl).toNat
1055 (count[(la[ol + sym.toNat]'hkl).toNat]'hlt16 + 1))) := by
1056 simp only [countBody]
1057 apply Wp.bind' (Q := fun r h2 => r = la[ol + sym.toNat]'hkl ∧ h2 = h')
1058 (Wp.of_eq (Ptr.index_ok hgl hkl) ⟨rfl, rfl⟩)
1059 rintro l h2 ⟨rfl, hh⟩
1060 subst h2
1061 apply Wp.bind' (Q := fun r h2 => r = count[(la[ol + sym.toNat]'hkl).toNat]'hlt16 ∧ h2 = h')
1062 (Wp.pure_eq (geta_eq hlt16) ⟨rfl, rfl⟩)
1063 rintro c h2 ⟨rfl, hh⟩
1064 subst h2
1065 apply Wp.bind' (Q := fun r h2 => r = count.set! (la[ol + sym.toNat]'hkl).toNat
1066 (count[(la[ol + sym.toNat]'hkl).toNat]'hlt16 + 1) ∧ h2 = h')
1067 (Wp.pure_eq (seta_eq hlt16) ⟨rfl, rfl⟩)
1068 rintro c2 h2 ⟨rfl, hh⟩
1069 subst h2
1070 exact Wp.pure' ⟨rfl, rfl⟩
1071 obtain ⟨r2, h2, hrun, rfl, rfl⟩ := hw
1072 refine ⟨(sym, count), _, _, _, ?_, hrun, ⟨rfl, by dsimp only; omega, by dsimp only; rw [Array.size_set!]; exact hsz, ?_⟩, by dsimp only; omega⟩
1073 · show (pure (decide (sym < codes), (sym, count)) : M _) _ = _
1074 simp [hlt]
1075 · intro l hl
1076 dsimp only
1077 rw [getD_set!, hu, cnt_step]
1078 have hadd : (count[(la[ol + sym.toNat]'hkl).toNat]'hlt16 + 1).toNat = cnt f sym.toNat (la[ol + sym.toNat]'hkl).toNat + 1 := by
1079 rw [UInt16.toNat_add]; simp only [UInt16.toNat_one]; rw [hcnt]
1080 exact Nat.mod_eq_of_lt (by omega)
1081 by_cases hh : (la[ol + sym.toNat]'hkl).toNat = l
1082 · rw [ite_eq_left ⟨hh, hlt16⟩, hadd, ite_eq_left (by rw [hfk]; exact hh)]
1083 rw [hh]
1084 · rw [ite_eq_right (fun hh2 => hh hh2.1), ite_eq_right (by rw [hfk]; exact hh), Nat.add_zero]
1085 exact hcn l hl
1086 · left
1087 have hsn' : sym.toNat = n := by
1088 have : ¬ sym.toNat < n := fun hh => hlt (by rw [UInt32.lt_iff_toNat_lt, hcodes]; exact hh)
1089 omega
1090 refine ⟨(sym, count), _, ?_, rfl, hsn', hsz, by rw [← hsn']; exact hcn⟩
1091 show (pure (decide (sym < codes), (sym, count)) : M _) _ = _
1092 simp [hlt]
1093 · refine ⟨rfl, by simp, hs0, fun l hl => ?_⟩
1094 show (count0.getD l 0).toNat = cnt f 0 l
1095 rw [cnt_zero]; exact hz0 l hl
1096 · exact lt_fuel (by omega)
1097
1098def maxCond : UInt32 × Bool → M (Bool × (UInt32 × Bool)) :=
1099 fun (max, brk) => pure (!brk && max ≥ 1, (max, brk))
1100
1101def maxBody (count : Array UInt16) : UInt32 × Bool → M (UInt32 × Bool) :=
1102 fun (max, brk) => do
1103 if (← geta count max.toNat) != 0 then pure (max, true) else pure (max - 1, brk)
1104
1105theorem max_loop (f : Nat → Nat) (n : Nat) (count : Array UInt16) (hs : count.size = 16)
1106 (hc : ∀ l, 1 ≤ l → l ≤ 15 → (count.getD l 0).toNat = cnt f n l) (h : Heap) :
1107 Wp (cwhile maxCond (maxBody count) (MAXBITS, false)) h
1108 (fun r h' => h' = h ∧ ((Tc f n 15 = 0 ∧ r.1.toNat = 0) ∨ (0 < Tc f n 15 ∧ r.1.toNat = mxl f n))) := by
1109 refine Wp.cwhile
1110 (fun (x : UInt32 × Bool) h' => h' = h ∧ x.1.toNat ≤ 15 ∧
1111 (x.2 = false → ∀ j, x.1.toNat < j → j ≤ 15 → cnt f n j = 0) ∧
1112 (x.2 = true → 1 ≤ x.1.toNat ∧ cnt f n x.1.toNat ≠ 0 ∧ ∀ j, x.1.toNat < j → j ≤ 15 → cnt f n j = 0))
1113 (fun (x : UInt32 × Bool) => if x.2 then 0 else x.1.toNat + 1) _ ?_ ?_ ?_
1114 · rintro ⟨max, brk⟩ h' ⟨rfl, hm, hnb, hb⟩
1115 dsimp only at hm hnb hb
1116 by_cases hcnd : (!brk && decide (max ≥ 1)) = true
1117 · right
1118 simp only [Bool.and_eq_true, Bool.not_eq_true', decide_eq_true_eq] at hcnd
1119 obtain ⟨hbrk, hge⟩ := hcnd
1120 have hge' : 1 ≤ max.toNat := by
1121 have := UInt32.le_iff_toNat_le.mp hge; simpa using this
1122 have hlt16 : max.toNat < count.size := by omega
1123 have hcm : (count[max.toNat]).toNat = cnt f n max.toNat := by
1124 have := hc max.toNat hge' hm
1125 rw [Array.getD_eq_getD_getElem?, Array.getElem?_eq_getElem hlt16] at this; simpa using this
1126 have hcond : maxCond (max, brk) h' = .ok ((true, (max, brk)), h') := by
1127 show (pure ((!brk && decide (max ≥ 1)), (max, brk)) : M _) h' = _
1128 rw [show ((!brk && decide (max ≥ 1))) = true from by
1129 simp only [Bool.and_eq_true, Bool.not_eq_true', decide_eq_true_eq]; exact ⟨hbrk, hge⟩]
1130 rfl
1131 by_cases hz : (count[max.toNat] != 0) = true
1132 · have hbody : maxBody count (max, brk) h' = .ok ((max, true), h') := by
1133 simp only [maxBody]
1134 rw [geta_eq hlt16, M_pure_bind, ite_eq_left hz]; rfl
1135 refine ⟨(max, brk), h', (max, true), h', hcond, hbody, ⟨rfl, hm, fun hx => by simp at hx, fun _ => ⟨hge', ?_, ?_⟩⟩, ?_⟩
1136 · dsimp only; rw [← hcm]; intro h0; apply (by simpa using hz : ¬ (count[max.toNat] = 0)); exact UInt16.toNat_inj.mp (by rw [h0]; rfl)
1137 · exact hnb hbrk
1138 · dsimp only; simp [hbrk]
1139 · have hbody : maxBody count (max, brk) h' = .ok ((max - 1, brk), h') := by
1140 simp only [maxBody]
1141 rw [geta_eq hlt16, M_pure_bind, ite_eq_right hz]; rfl
1142 have hz0 : cnt f n max.toNat = 0 := by
1143 rw [← hcm]
1144 have : count[max.toNat] = 0 := by simpa using hz
1145 rw [this]; rfl
1146 have hm1 : (max - 1).toNat = max.toNat - 1 := u32_one_sub (by omega)
1147 refine ⟨(max, brk), h', (max - 1, brk), h', hcond, hbody, ⟨rfl, by dsimp only; rw [hm1]; omega, fun _ j hj1 hj2 => ?_, fun hx => by simp [hbrk] at hx⟩, ?_⟩
1148 · dsimp only at hj1
1149 rw [hm1] at hj1
1150 by_cases hjj : j = max.toNat
1151 · rw [hjj]; exact hz0
1152 · exact hnb hbrk j (by omega) hj2
1153 · dsimp only; simp [hbrk, hm1]; omega
1154 · left
1155 have hcond : maxCond (max, brk) h' = .ok ((false, (max, brk)), h') := by
1156 show (pure ((!brk && decide (max ≥ 1)), (max, brk)) : M _) h' = _
1157 have : ((!brk && decide (max ≥ 1))) = false := by
1158 cases hh : ((!brk && decide (max ≥ 1)))
1159 · rfl
1160 · exact absurd hh hcnd
1161 rw [this]; rfl
1162 refine ⟨(max, brk), h', hcond, rfl, ?_⟩
1163 cases hbrk : brk
1164 · have hmax0 : max.toNat = 0 := by
1165 have hn : ¬ (max ≥ 1) := fun hh => hcnd (by simp [hbrk, hh])
1166 have := (not_congr UInt32.le_iff_toNat_le).mp hn
1167 simp at this; omega
1168 have hall := hnb hbrk
1169 left
1170 refine ⟨?_, hmax0⟩
1171 have := Tc_gap (f := f) (n := n) 0 15 (fun j h1 h2 => hall j (by omega) (by omega))
1172 have h0 : Tc f n 0 = 0 := rfl
1173 simp only [Nat.zero_add] at this
1174 omega
1175 · right
1176 obtain ⟨h1, h2, h3⟩ := hb hbrk
1177 have hTs := Tc_succ' (f := f) (n := n) h1
1178 have hmono := Tc_mono (f := f) (n := n) (show max.toNat ≤ 15 by omega)
1179 have hpos : 0 < Tc f n 15 := by
1180 have : 0 < cnt f n max.toNat := Nat.pos_of_ne_zero h2
1181 omega
1182 refine ⟨hpos, ?_⟩
1183 exact (mxl_eq hpos h1 hm h2 h3).symm
1184 · refine ⟨rfl, by decide, fun _ j hj1 hj2 => ?_, fun hx => by simp at hx⟩
1185 have hM : (MAXBITS, false).fst.toNat = 15 := rfl
1186 omega
1187 · show (if false = true then 0 else (MAXBITS, false).fst.toNat + 1) < fuel
1188 exact lt_fuel (by decide)
1189
1190def minCond (max : UInt32) : UInt32 × Bool → M (Bool × (UInt32 × Bool)) :=
1191 fun (min, brk) => pure (!brk && min < max, (min, brk))
1192
1193def minBody (count : Array UInt16) : UInt32 × Bool → M (UInt32 × Bool) :=
1194 fun (min, brk) => do
1195 if (← geta count min.toNat) != 0 then pure (min, true) else pure (min + 1, brk)
1196
1197theorem min_loop (f : Nat → Nat) (n : Nat) (count : Array UInt16) (hs : count.size = 16)
1198 (hc : ∀ l, 1 ≤ l → l ≤ 15 → (count.getD l 0).toNat = cnt f n l) (max : UInt32)
1199 (hmax : max.toNat = mxl f n) (hpos : 0 < Tc f n 15) (h : Heap) :
1200 Wp (cwhile (minCond max) (minBody count) ((1 : UInt32), false)) h
1201 (fun r h' => h' = h ∧ r.1.toNat = lenAt f n 0) := by
1202 obtain ⟨b1, b2⟩ := lenAt_bounds (f := f) (n := n) hpos
1203 obtain ⟨hz, hnz⟩ := min_facts (f := f) (n := n) hpos
1204 have hl0mx : lenAt f n 0 ≤ mxl f n := lenAt_mono (f := f) (n := n) (show 0 ≤ Tc f n 15 - 1 by omega) (by omega)
1205 refine Wp.cwhile
1206 (fun (x : UInt32 × Bool) h' => h' = h ∧ 1 ≤ x.1.toNat ∧ x.1.toNat ≤ lenAt f n 0 ∧
1207 (x.2 = true → x.1.toNat = lenAt f n 0))
1208 (fun (x : UInt32 × Bool) => if x.2 then 0 else lenAt f n 0 + 1 - x.1.toNat) _ ?_ ?_ ?_
1209 · rintro ⟨min, brk⟩ h' ⟨rfl, hm1, hm2, hb⟩
1210 dsimp only at hm1 hm2 hb
1211 by_cases hcnd : (!brk && decide (min < max)) = true
1212 · right
1213 simp only [Bool.and_eq_true, Bool.not_eq_true', decide_eq_true_eq] at hcnd
1214 obtain ⟨hbrk, hlt⟩ := hcnd
1215 have hlt' : min.toNat < max.toNat := UInt32.lt_iff_toNat_lt.mp hlt
1216 have hlt16 : min.toNat < count.size := by omega
1217 have hcm : (count[min.toNat]).toNat = cnt f n min.toNat := by
1218 have := hc min.toNat hm1 (by omega)
1219 rw [Array.getD_eq_getD_getElem?, Array.getElem?_eq_getElem hlt16] at this; simpa using this
1220 have hcond : minCond max (min, brk) h' = .ok ((true, (min, brk)), h') := by
1221 show (pure ((!brk && decide (min < max)), (min, brk)) : M _) h' = _
1222 rw [show ((!brk && decide (min < max))) = true from by
1223 simp only [Bool.and_eq_true, Bool.not_eq_true', decide_eq_true_eq]; exact ⟨hbrk, hlt⟩]
1224 rfl
1225 by_cases hzz : (count[min.toNat] != 0) = true
1226 · have hbody : minBody count (min, brk) h' = .ok ((min, true), h') := by
1227 simp only [minBody]
1228 rw [geta_eq hlt16, M_pure_bind, ite_eq_left hzz]; rfl
1229 have hne : cnt f n min.toNat ≠ 0 := by
1230 rw [← hcm]; intro h0; apply (by simpa using hzz : ¬ (count[min.toNat] = 0))
1231 exact UInt16.toNat_inj.mp (by rw [h0]; rfl)
1232 have heq : min.toNat = lenAt f n 0 := by
1233 apply Classical.byContradiction; intro hh
1234 exact hne (hz _ hm1 (by omega))
1235 refine ⟨(min, brk), h', (min, true), h', hcond, hbody, ⟨rfl, hm1, hm2, fun _ => heq⟩, ?_⟩
1236 dsimp only; simp [hbrk]; omega
1237 · have hbody : minBody count (min, brk) h' = .ok ((min + 1, brk), h') := by
1238 simp only [minBody]
1239 rw [geta_eq hlt16, M_pure_bind, ite_eq_right hzz]; rfl
1240 have hz0 : cnt f n min.toNat = 0 := by
1241 rw [← hcm]
1242 have : count[min.toNat] = 0 := by simpa using hzz
1243 rw [this]; rfl
1244 have hlt0 : min.toNat < lenAt f n 0 := by
1245 apply Classical.byContradiction; intro hh
1246 have : min.toNat = lenAt f n 0 := by omega
1247 rw [this] at hz0; exact hnz hz0
1248 have hu : (min + 1).toNat = min.toNat + 1 := u32_succ (by omega)
1249 refine ⟨(min, brk), h', (min + 1, brk), h', hcond, hbody, ⟨rfl, by dsimp only; omega, by dsimp only; omega, fun hx => by simp [hbrk] at hx⟩, ?_⟩
1250 dsimp only; simp [hbrk, hu]; omega
1251 · left
1252 have hcond : minCond max (min, brk) h' = .ok ((false, (min, brk)), h') := by
1253 show (pure ((!brk && decide (min < max)), (min, brk)) : M _) h' = _
1254 have : ((!brk && decide (min < max))) = false := by
1255 cases hh : ((!brk && decide (min < max)))
1256 · rfl
1257 · exact absurd hh hcnd
1258 rw [this]; rfl
1259 refine ⟨(min, brk), h', hcond, rfl, ?_⟩
1260 cases hbrk : brk
1261 · have hn : ¬ (min < max) := fun hh => hcnd (by simp [hbrk, hh])
1262 have := (not_congr UInt32.lt_iff_toNat_lt).mp hn
1263 show min.toNat = lenAt f n 0
1264 omega
1265 · exact hb hbrk
1266 · have h1 : ((1 : UInt32), false).fst.toNat = 1 := rfl
1267 exact ⟨rfl, by omega, by omega, fun hx => by simp at hx⟩
1268 · show (if false = true then 0 else lenAt f n 0 + 1 - ((1 : UInt32), false).fst.toNat) < fuel
1269 have h1 : ((1 : UInt32), false).fst.toNat = 1 := rfl
1270 simp only [Bool.false_eq_true, ite_false]
1271 exact lt_fuel (by omega)
1272
1273theorem capOf_ge (type : UInt32) : 2 ≤ capOf type := by
1274 unfold capOf; split <;> (try split) <;> omega
1275
1276theorem wpC_add {R T : Type} [Space Heap R T] (h : Heap) (r : R) (a : Array T) (off n : Nat)
1277 (hg : Space.get h r = some a) (hn : off + n ≤ a.size) :
1278 Wp (Ptr.add (Ptr.ref r off) (n : Int)) h (fun q h' => q = Ptr.ref r (off + n) ∧ h' = h) :=
1279 Wp.of_eq (Ptr.add_nat_ok hg hn) ⟨rfl, rfl⟩
1280
1281theorem wpC_store {R T : Type} [Space Heap R T] (h : Heap) (r : R) (a : Array T) (off : Nat) (v : T)
1282 (hg : Space.get h r = some a) (hro : Space.ro h r = false) (hlt : off < a.size) :
1283 Wp (Ptr.store (Ptr.ref r off) v) h (fun _ h' => h' = Space.put h r (a.set! off v)) :=
1284 ⟨(), _, Ptr.store_ok hg hro hlt, rfl⟩
1285
1286theorem fits_of_zero {f : Nat → Nat} {n : Nat} (hT : Tc f n 15 = 0) : Fits f n := by
1287 intro l hl1 hl2
1288 have hm := Tc_mono (f := f) (n := n) hl2
1289 have := Kc_gap (f := f) (n := n) 0 l (by rw [Nat.zero_add]; show Tc f n l = Tc f n 0; have : Tc f n 0 = 0 := rfl; omega)
1290 have hK0 : Kc f n 0 = 0 := rfl
1291 rw [Nat.zero_add, hK0, Nat.mul_zero] at this
1292 rw [this]; exact Nat.zero_le _
1293
1294theorem itA_wp {h : Heap} {type : UInt32} {rl : WRef} {ol : Nat} {codes : UInt32} {rc : CodeRef} {oc : Nat}
1295 {bits : UInt32} {rw : WRef} {ow : Nat} (P : CallPre h type rl ol codes rc oc bits rw ow)
1296 (count : Array UInt16) (max root : UInt32)
1297 (hcs : count.size = 16) (hcc : ∀ l, 1 ≤ l → l ≤ 15 → (count.getD l 0).toNat = cnt P.f codes.toNat l)
1298 (hmaxq : (Tc P.f codes.toNat 15 = 0 ∧ max.toNat = 0) ∨ (0 < Tc P.f codes.toNat 15 ∧ max.toNat = mxl P.f codes.toNat))
1299 (hroot : root.toNat ≤ max.toNat) (hrC : type = CODES → root.toNat = max.toNat) :
1300 Wp (itA type (Ptr.ref rl ol) codes (Ptr.ref rc oc) bits (Ptr.ref rw ow) count max root) h
1301 (fun r h' => Result h rw rc ow oc (capOf type) codes.toNat P.wa P.ca (Ptr.ref rc oc) bits r h' ∧
1302 RetInfo type P.f codes.toNat r) := by
1303 unfold itA
1304 by_cases hm0 : (max == 0) = true
1305 · rw [ite_eq_left hm0]
1306 have hcap2 := capOf_ge type
1307 have hca := P.hca
1308 show Wp (do Ptr.store (Ptr.ref rc oc) (⟨64, 1, 0⟩ : Code)
1309 let table ← Ptr.add (Ptr.ref rc oc) 1
1310 Ptr.store table (⟨64, 1, 0⟩ : Code)
1311 let table ← Ptr.add table 1
1312 return ((0 : Int32), table, (1 : UInt32))) _ _
1313 apply Wp.bind' (Q := fun _ h2 => h2 = Space.put h rc (P.ca.set! oc ⟨64, 1, 0⟩))
1314 (wpC_store h rc P.ca oc _ P.hgc P.hro (by omega))
1315 rintro _ h1 rfl
1316 have hg1 := cget_put_self P.hgc P.hro (P.ca.set! oc (⟨64, 1, 0⟩ : Code))
1317 apply Wp.bind' (Q := fun q h2 => q = Ptr.ref rc (oc + 1) ∧ h2 = Space.put h rc (P.ca.set! oc ⟨64, 1, 0⟩))
1318 (wpC_add _ rc _ oc 1 hg1 (by rw [Array.size_set!]; omega))
1319 rintro q h2 ⟨rfl, rfl⟩
1320 apply Wp.bind' (Q := fun _ h3 => h3 = Space.put h rc ((P.ca.set! oc ⟨64, 1, 0⟩).set! (oc + 1) ⟨64, 1, 0⟩))
1321 (by
1322 have := wpC_store _ rc _ (oc + 1) (⟨64, 1, 0⟩ : Code) hg1 P.hro (by rw [Array.size_set!]; omega)
1323 refine Wp.mono this ?_
1324 intro _ h3 hh; rw [hh, cput_put])
1325 rintro _ h3 rfl
1326 have hg2 := cget_put_self P.hgc P.hro ((P.ca.set! oc (⟨64, 1, 0⟩ : Code)).set! (oc + 1) (⟨64, 1, 0⟩ : Code))
1327 apply Wp.bind' (Q := fun q h4 => q = Ptr.ref rc (oc + 1 + 1) ∧ h4 = Space.put h rc ((P.ca.set! oc ⟨64, 1, 0⟩).set! (oc + 1) ⟨64, 1, 0⟩))
1328 (wpC_add _ rc _ (oc + 1) 1 hg2 (by rw [Array.size_set!, Array.size_set!]; omega))
1329 rintro q h4 ⟨rfl, rfl⟩
1330 have hT0 : Tc P.f codes.toNat 15 = 0 := by
1331 have hm0' : max.toNat = 0 := by
1332 have : max = 0 := by simpa using hm0
1333 rw [this]; rfl
1334 rcases hmaxq with ⟨a, _⟩ | ⟨a, b⟩
1335 · exact a
1336 · have := lenAt_bounds (f := P.f) (n := codes.toNat) a
1337 have h3 : mxl P.f codes.toNat = lenAt P.f codes.toNat (Tc P.f codes.toNat 15 - 1) := rfl
1338 have := lenAt_bounds (f := P.f) (n := codes.toNat) (show Tc P.f codes.toNat 15 - 1 < Tc P.f codes.toNat 15 by omega)
1339 omega
1340 have hacc : Acc type P.f codes.toNat := ⟨fits_of_zero hT0, Or.inr (Or.inl hT0)⟩
1341 refine Wp.pure' ⟨⟨P.wa, (P.ca.set! oc ⟨64, 1, 0⟩).set! (oc + 1) ⟨64, 1, 0⟩, ?_, rfl, ?_, fun _ _ => rfl, ?_, Or.inl ⟨rfl, 2, hcap2, rfl⟩⟩,
1342 fun _ => hacc, fun h => absurd (show (0 : Int32) = 1 from h) (by decide),
1343 fun h => absurd (show (0 : Int32) = -1 from h) (by decide)⟩
1344 · rw [wput_self P.hgw]
1345 · simp [Array.size_set!]
1346 · intro x hx
1347 have h1 : oc + 1 ≠ x := by omega
1348 have h2 : oc ≠ x := by omega
1349 rw [getElem?_set!_ne h1, getElem?_set!_ne h2]
1350 · rw [ite_eq_right hm0]
1351 have hm0' : max.toNat ≠ 0 := fun h0 => hm0 (by
1352 have : max = 0 := UInt32.toNat_inj.mp (by rw [h0]; rfl)
1353 simp [this])
1354 obtain ⟨hpos, hmx⟩ : 0 < Tc P.f codes.toNat 15 ∧ max.toNat = mxl P.f codes.toNat := by
1355 rcases hmaxq with ⟨_, h2⟩ | h2
1356 · exact absurd h2 hm0'
1357 · exact h2
1358 obtain ⟨hl1, hl2⟩ := lenAt_bounds (f := P.f) (n := codes.toNat) hpos
1359 have hl0mx : lenAt P.f codes.toNat 0 ≤ mxl P.f codes.toNat :=
1360 lenAt_mono (f := P.f) (n := codes.toNat) (show 0 ≤ Tc P.f codes.toNat 15 - 1 by omega) (by omega)
1361 apply Wp.bind' (min_loop P.f codes.toNat count hcs hcc max hmx hpos _)
1362 rintro ⟨min, brk⟩ h' ⟨rfl, hmin⟩
1363 dsimp only at hmin ⊢
1364 by_cases hr : root < min
1365 · rw [ite_eq_left hr]
1366 have hr' : root.toNat < min.toNat := UInt32.lt_iff_toNat_lt.mp hr
1367 exact itB_wp P count max min min hcs hcc hmx hpos hmin (by omega) (by omega) (by omega)
1368 (fun hC => by have := hrC hC; omega)
1369 · rw [ite_eq_right hr]
1370 have hr' : min.toNat ≤ root.toNat := by
1371 have := (not_congr UInt32.lt_iff_toNat_lt).mp hr; omega
1372 exact itB_wp P count max min root hcs hcc hmx hpos hmin (by omega) (by omega) (by omega)
1373 (fun hC => by have := hrC hC; omega)
1374
1375theorem mxl_le7 {f : Nat → Nat} {n : Nat} (hpos : 0 < Tc f n 15) (hall : ∀ k, k < n → f k ≤ 7) : mxl f n ≤ 7 := by
1376 unfold mxl lenAt
1377 exact hall _ (ws_getD_lt (by omega))
1378
1379theorem itTop_wp {h : Heap} {type : UInt32} {rl : WRef} {ol : Nat} {codes : UInt32} {rc : CodeRef} {oc : Nat}
1380 {bits : UInt32} {rw : WRef} {ow : Nat} (P : CallPre h type rl ol codes rc oc bits rw ow) :
1381 Wp (itTop type (Ptr.ref rl ol) codes (Ptr.ref rc oc) bits (Ptr.ref rw ow)) h
1382 (fun r h' => Result h rw rc ow oc (capOf type) codes.toNat P.wa P.ca (Ptr.ref rc oc) bits r h' ∧
1383 RetInfo type P.f codes.toNat r) := by
1384 have hn288 : codes.toNat ≤ 288 := by
1385 rcases P.hty with ht | ht | ht
1386 · have := (P.hcodes ht).1; omega
1387 · exact P.hlens ht
1388 · have := P.hdists ht; omega
1389 unfold itTop
1390 apply Wp.bind' (zero_loop h)
1391 rintro ⟨len, count⟩ h' ⟨rfl, hs, hz⟩
1392 dsimp only at hs hz ⊢
1393 apply Wp.bind' (count_loop P.f codes.toNat hn288 rl ol P.la codes rfl _ P.hgl P.hla (fun k => rfl) P.hf15 count hs hz)
1394 rintro ⟨sym, count2⟩ h2 ⟨rfl, hsym, hs2, hc2⟩
1395 dsimp only at hs2 hc2 ⊢
1396 have hcc : ∀ l, 1 ≤ l → l ≤ 15 → (count2.getD l 0).toNat = cnt P.f codes.toNat l := fun l h1 h2 => hc2 l (by omega)
1397 apply Wp.bind' (max_loop P.f codes.toNat count2 hs2 hcc _)
1398 rintro ⟨max, brk⟩ h3 ⟨rfl, hmaxq⟩
1399 dsimp only at hmaxq ⊢
1400 by_cases hgt : bits > max
1401 · rw [ite_eq_left hgt]
1402 exact itA_wp P count2 max max hs2 hcc hmaxq (Nat.le_refl _) (fun _ => rfl)
1403 · rw [ite_eq_right hgt]
1404 have hle : bits.toNat ≤ max.toNat := by
1405 have := (not_congr UInt32.lt_iff_toNat_lt).mp hgt; omega
1406 exact itA_wp P count2 max bits hs2 hcc hmaxq hle
1407 (fun hC => by
1408 obtain ⟨_, h7, hb7⟩ := P.hcodes hC
1409 rcases hmaxq with ⟨a, b⟩ | ⟨a, b⟩
1410 · omega
1411 · have := mxl_le7 (f := P.f) (n := codes.toNat) a h7
1412 omega)
1413
1414theorem inflate_table_eq : inflate_table = itTop := rfl
1415
1416end Zlib.Inftrees.Proofs