REFERENCE / ZLIB × LEAN
inftrees.c.step.lean
Source snapshot ·
fce9777d2a251f33 · Source at the matching commit ↗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.base»
2import ZlibF.Proof.«inftrees.c.geom»
3
4namespace Zlib.Inftrees.Proofs
5open C Zlib.Inftrees
6
7/-- Everything the main loop of `inflate_table` reads and never changes. `hb` is the heap before the loop (after the
8sort); inside the loop the heap is `hb` with the table array replaced. -/
9structure Env where
10 c : Ctx
11 f : Nat → Nat
12 n : Nat
13 R : Nat
14 cap : Nat
15 rc : CodeRef
16 oc : Nat
17 rw : WRef
18 ow : Nat
19 rl : WRef
20 ol : Nat
21 hb : Heap
22 la : Array UInt16
23 wa : Array UInt16
24 h_table : c.table = .ref rc oc
25 h_lens : c.lens = .ref rl ol
26 h_work : c.work = .ref rw ow
27 h_ro : Space.ro hb rc = false
28 h_live : ∃ ca0, Space.get hb rc = some ca0
29 h_get_la : Space.get hb rl = some la
30 h_get_wa : Space.get hb rw = some wa
31 h_f : ∀ k, f k = (la.getD (ol + k) 0).toNat
32 h_la : ol + n ≤ la.size
33 h_f15 : ∀ k, k < n → f k ≤ 15
34 h_wa : ow + n ≤ wa.size
35 h_wcont : ∀ i, i < Tc f n 15 → wa[ow + i]? = some (UInt16.ofNat ((wsAux f n 15).getD i 0))
36 h_n : n ≤ 288
37 h_root : c.root.toNat = R
38 h_max : c.max.toNat = mxl f n
39 h_R1 : 1 ≤ R
40 h_Rmx : R ≤ mxl f n
41 h_R0 : lenAt f n 0 ≤ R
42 h_pos : 0 < Tc f n 15
43 h_fits : Fits f n
44 h_end : Kc f n 15 = 2 ^ 15 ∨ (mxl f n = 1 ∧ Tc f n 15 = 1 ∧ c.type ≠ CODES)
45 h_type : c.type = CODES ∨ c.type = LENS ∨ c.type = DISTS
46 h_cap : cap = (if c.type = CODES then 128 else if c.type = LENS then 852 else 592)
47 h_codes : c.type = CODES → mxl f n ≤ 7 ∧ R = mxl f n ∧ n ≤ 19 ∧ c.match_ = 20
48 h_lens' : c.type = LENS → n ≤ 288 ∧ c.base = lbase ∧ c.extra = lext ∧ c.match_ = 257
49 h_dists : c.type = DISTS → n ≤ 32 ∧ c.base = dbase ∧ c.extra = dext ∧ c.match_ = 0
50
51namespace Env
52def m (e : Env) : Nat := Tc e.f e.n 15
53def l (e : Env) (i : Nat) : Nat := lenAt e.f e.n i
54def v (e : Env) (i : Nat) : Nat := val e.f e.n i
55def p (e : Env) (i : Nat) : Nat := pre e.f e.n e.R i
56def mx (e : Env) : Nat := mxl e.f e.n
57/-- The heap inside the loop: the table array is `ca`. -/
58def hc (e : Env) (ca : Array Code) : Heap := Space.put e.hb e.rc ca
59end Env
60
61/-- `count[l]` is the number of symbols of length `l` that are still to be coded. -/
62def CountOK (e : Env) (count : Array UInt16) (i : Nat) : Prop :=
63 count.size = 16 ∧ ∀ l, 1 ≤ l → l ≤ 15 → (count.getD l 0).toNat = rem e.f e.n i l
64
65/-- The state of the table that the main loop keeps while it handles the `i`-th code. -/
66def TabSt (e : Env) (i : Nat) (s : TS) : Prop :=
67 (∃ k, s.next = .ref e.rc (e.oc + k) ∧ k + 2 ^ s.curr.toNat = s.used.toNat) ∧
68 s.used.toNat ≤ e.cap ∧ 2 ^ e.R ≤ s.used.toNat ∧ 1 ≤ s.curr.toNat ∧ s.curr.toNat ≤ 15 ∧
69 (e.l i ≤ e.R → s.drop = 0 ∧ s.low = 0xffffffff ∧ s.curr.toNat = e.R ∧ s.used.toNat = 2 ^ e.R) ∧
70 (e.R < e.l i → s.drop.toNat = e.R ∧ s.low.toNat = rev e.R (e.p i) ∧ e.l i ≤ e.R + s.curr.toNat ∧
71 e.R + s.curr.toNat ≤ e.mx ∧
72 ∀ j, j < e.m → e.R < e.l j → e.p j = e.p i → e.l j ≤ e.R + s.curr.toNat)
73
74/-- The invariant of the main loop at the top of the iteration for the `i`-th code. -/
75def MI (e : Env) (i : Nat) (s : TS) (ca : Array Code) : Prop :=
76 i < e.m ∧ s.exit = 0 ∧ s.sym.toNat = i ∧ s.len.toNat = e.l i ∧ s.huff.toNat = rev (e.l i) (e.v i) ∧
77 s.mask.toNat = 2 ^ e.R - 1 ∧ CountOK e s.count i ∧ e.oc + e.cap ≤ ca.size ∧ TabSt e i s
78
79/-- After the new `huff` is computed and before `sym++`. -/
80def MI1 (e : Env) (i : Nat) (s : TS) (ca : Array Code) : Prop :=
81 i < e.m ∧ s.exit = 0 ∧ s.sym.toNat = i ∧ s.len.toNat = e.l i ∧
82 (i + 1 < e.m → s.huff.toNat = rev (e.l (i + 1)) (e.v (i + 1))) ∧
83 (i + 1 = e.m → s.huff.toNat = 0 ∨ s.huff.toNat < 2 ^ s.curr.toNat) ∧
84 s.mask.toNat = 2 ^ e.R - 1 ∧ CountOK e s.count i ∧ e.oc + e.cap ≤ ca.size ∧ TabSt e i s ∧
85 s.min.toNat = 2 ^ s.curr.toNat
86
87/-- After `sym++`, the count and the new length, before the test for a new sub-table. -/
88def MI2 (e : Env) (i : Nat) (s : TS) (ca : Array Code) : Prop :=
89 i + 1 < e.m ∧ s.exit = 0 ∧ s.sym.toNat = i + 1 ∧ s.len.toNat = e.l (i + 1) ∧
90 s.huff.toNat = rev (e.l (i + 1)) (e.v (i + 1)) ∧
91 s.mask.toNat = 2 ^ e.R - 1 ∧ CountOK e s.count (i + 1) ∧ e.oc + e.cap ≤ ca.size ∧ TabSt e i s ∧
92 s.min.toNat = 2 ^ s.curr.toNat
93
94/-- The state after the last code: what the final store and the pointer advance need. -/
95def Final (e : Env) (s : TS) : Prop :=
96 (∃ k, s.next = .ref e.rc (e.oc + k) ∧ k + 2 ^ s.curr.toNat = s.used.toNat) ∧
97 s.used.toNat ≤ e.cap ∧ (s.huff.toNat = 0 ∨ s.huff.toNat < 2 ^ s.curr.toNat)
98
99/-- The shape of the state after the last code of the one incomplete accepted code (one symbol of length 1). -/
100def Einc (e : Env) (s : TS) : Prop :=
101 e.m = 1 ∧ e.R = 1 ∧ s.huff.toNat = 1 ∧ s.next = .ref e.rc e.oc
102
103/-- The table array changes only inside the space the caller gave. -/
104def FrameCA (e : Env) (ca ca' : Array Code) : Prop :=
105 ca'.size = ca.size ∧ ∀ x, (x < e.oc ∨ e.oc + e.cap ≤ x) → ca'[x]? = ca[x]?
106
107def StepPost (e : Env) (i : Nat) (s' : TS) (ca' : Array Code) : Prop :=
108 (i + 1 < e.m ∧ MI e (i + 1) s' ca') ∨ (i + 1 = e.m ∧ s'.exit = 1 ∧ Final e s' ∧ e.oc + e.cap ≤ ca'.size) ∨
109 (s'.exit = 2 ∧ e.c.type ≠ CODES ∧ e.oc + e.cap ≤ ca'.size)
110
111/-! ### The cells of the table: closed form and invariant
112
113Cells are numbered from the start of the table (`oc` is added when the array is read). -/
114
115/-- The entry that the C builds for the symbol `w` with `bits` table bits. -/
116def hereC (c : Ctx) (w : UInt16) (bits : UInt8) : Code :=
117 if w.toUInt32 + 1 < c.match_ then ⟨0, bits, w⟩
118 else if w.toUInt32 ≥ c.match_ then
119 ⟨(c.extra[(w.toUInt32 - c.match_).toNat]!).toUInt8, bits, c.base[(w.toUInt32 - c.match_).toNat]!⟩
120 else ⟨96, bits, 0⟩
121
122/-- The table cell of the `m`-th copy of the entry of the code with allocation index `i`. -/
123def gAddr (ls : List Nat) (R mx i m : Nat) : Nat :=
124 (Canon.desc ls R mx i).base + Canon.H ls i / 2 ^ (Canon.desc ls R mx i).drop +
125 m * 2 ^ (Canon.L ls i - (Canon.desc ls R mx i).drop)
126
127/-- The number of copies of that entry. -/
128def gReps (ls : List Nat) (R mx i : Nat) : Nat :=
129 2 ^ ((Canon.desc ls R mx i).curr - (Canon.L ls i - (Canon.desc ls R mx i).drop))
130
131/-- The root cell of the link to the sub-table that starts at allocation index `a`. -/
132def gSlot (ls : List Nat) (R a : Nat) : Nat := Canon.rev R (Canon.grp ls R a)
133
134/-- The cells of different entries are different (the geometry of a complete or acceptable code). -/
135structure GeoOK (ls : List Nat) (R mx : Nat) : Prop where
136 uniq : ∀ i j m m', i < Canon.nz ls → j < Canon.nz ls → m < gReps ls R mx i → m' < gReps ls R mx j →
137 gAddr ls R mx i m = gAddr ls R mx j m' → i = j ∧ m = m'
138 slot_ne : ∀ a i m, 1 ≤ a → a < Canon.nz ls → Canon.startsAt ls R (a - 1) → i < Canon.nz ls →
139 m < gReps ls R mx i → gSlot ls R a ≠ gAddr ls R mx i m
140 slot_inj : ∀ a b, 1 ≤ a → a < Canon.nz ls → Canon.startsAt ls R (a - 1) → 1 ≤ b → b < Canon.nz ls →
141 Canon.startsAt ls R (b - 1) → gSlot ls R a = gSlot ls R b → a = b
142
143namespace Env
144def ls (e : Env) : List Nat := lensOf e.f e.n
145def D (e : Env) (i : Nat) : Canon.Desc := Canon.desc e.ls e.R e.mx i
146def here (e : Env) (j : Nat) : Code :=
147 hereC e.c (UInt16.ofNat ((wsAux e.f e.n 15).getD j 0)) (Canon.L e.ls j - (e.D j).drop).toUInt8
148def link (e : Env) (a : Nat) : Code :=
149 ⟨(Canon.width e.ls a e.R e.mx).toUInt8, e.R.toUInt8, (e.D a).base.toUInt16⟩
150/-- The geometry facts for this call. -/
151def Geo (e : Env) : Prop := GeoOK e.ls e.R e.mx
152end Env
153
154/-- The entries of the codes below `i` are in the table. -/
155def Written (e : Env) (i : Nat) (ca : Array Code) : Prop :=
156 ∀ j, j < i → ∀ m, m < gReps e.ls e.R e.mx j → ca[e.oc + gAddr e.ls e.R e.mx j m]? = some (e.here j)
157
158/-- The links of the sub-tables that start at allocation index at most `i` are in the table. -/
159def Links (e : Env) (i : Nat) (ca : Array Code) : Prop :=
160 ∀ a, 1 ≤ a → a ≤ i → a < e.m → Canon.startsAt e.ls e.R (a - 1) → ca[e.oc + gSlot e.ls e.R a]? = some (e.link a)
161
162/-- What the table array holds, given the geometry facts. -/
163def Cont (e : Env) (w l : Nat) (ca : Array Code) : Prop := e.Geo → Written e w ca ∧ Links e l ca
164
165/-- The state is the descriptor `desc` in force at allocation index `i`. -/
166def DescB (e : Env) (i : Nat) (s : TS) : Prop :=
167 (∃ k, s.next = .ref e.rc (e.oc + k) ∧ k = (e.D i).base) ∧ s.curr.toNat = (e.D i).curr ∧
168 s.used.toNat = (e.D i).used
169def DescIs (e : Env) (i : Nat) (s : TS) : Prop :=
170 DescB e i s ∧ s.drop.toNat = (e.D i).drop ∧ s.low.toNat = (e.D i).low
171
172/-- The invariant of the cells at the top of iteration `i`. -/
173def Ex (e : Env) (i : Nat) (s : TS) (ca : Array Code) : Prop := DescIs e i s ∧ Cont e i i ca
174/-- The same, after the entry of code `i` was written and before the next sub-table is opened. -/
175def Ex1 (e : Env) (i : Nat) (s : TS) (ca : Array Code) : Prop := DescIs e i s ∧ Cont e (i + 1) i ca
176
177/-- `StepPost` with the cells. -/
178def StepPostX (e : Env) (i : Nat) (s' : TS) (ca' : Array Code) : Prop :=
179 StepPost e i s' ca' ∧ (i + 1 < e.m → s'.exit = 0 → Ex e (i + 1) s' ca') ∧
180 (i + 1 = e.m → s'.exit = 1 → Cont e e.m e.m ca' ∧ (s'.huff.toNat ≠ 0 → Einc e s'))
181
182theorem Env.nz_eq (e : Env) : Canon.nz e.ls = e.m := Zlib.Inftrees.Proofs.nz_eq e.f e.n
183
184/-- The fill loop writes the entry of code `i` into its cells and nothing else. -/
185theorem cont_fill (e : Env) (i : Nat) (ca ca2 : Array Code) (hi : i < e.m) (k hd S N : Nat)
186 (hk : k = (e.D i).base) (hhd : hd = Canon.H e.ls i / 2 ^ (e.D i).drop)
187 (hS : S = 2 ^ (Canon.L e.ls i - (e.D i).drop)) (hN : N = gReps e.ls e.R e.mx i)
188 (h1 : ∀ x, (∃ q', q' < N ∧ x = e.oc + k + hd + S * q') → ca2[x]? = some (e.here i))
189 (h2 : ∀ x, ¬ (∃ q', q' < N ∧ x = e.oc + k + hd + S * q') → ca2[x]? = ca[x]?) :
190 Cont e i i ca → Cont e (i + 1) i ca2 := by
191 intro hC hg
192 obtain ⟨hW, hL⟩ := hC hg
193 have hnz := e.nz_eq
194 have hadd : ∀ q, e.oc + gAddr e.ls e.R e.mx i q = e.oc + k + hd + S * q := by
195 intro q
196 simp only [Env.D] at hk hhd hS
197 subst hk; subst hhd; subst hS
198 unfold gAddr
199 rw [Nat.mul_comm q]
200 omega
201 refine ⟨fun j hj m hm => ?_, fun a ha1 ha2 ha3 ha4 => ?_⟩
202 · by_cases hji : j = i
203 · subst hji
204 exact (hadd m) ▸ h1 _ ⟨m, by rw [hN]; exact hm, rfl⟩
205 · have hj' : j < i := by omega
206 rw [h2]
207 · exact hW j hj' m hm
208 · rintro ⟨q', hq, hx⟩
209 rw [← hadd q'] at hx
210 have := (hg.uniq j i m q' (by omega) (by omega) hm (by rw [← hN]; exact hq) (by omega)).1
211 exact hji this
212 · rw [h2]
213 · exact hL a ha1 ha2 ha3 ha4
214 · rintro ⟨q', hq, hx⟩
215 rw [← hadd q'] at hx
216 exact hg.slot_ne a i q' ha1 (by omega) ha4 (by omega) (by rw [← hN]; exact hq) (by omega)
217
218/-- Opening a sub-table writes its link into the root. -/
219theorem cont_link (e : Env) (i : Nat) (ca ca3 : Array Code) (hi1 : i + 1 < e.m)
220 (hs : Canon.startsAt e.ls e.R i)
221 (hlink : ca3[e.oc + gSlot e.ls e.R (i + 1)]? = some (e.link (i + 1)))
222 (hrest : ∀ x, x ≠ e.oc + gSlot e.ls e.R (i + 1) → ca3[x]? = ca[x]?) :
223 Cont e (i + 1) i ca → Cont e (i + 1) (i + 1) ca3 := by
224 intro hC hg
225 obtain ⟨hW, hL⟩ := hC hg
226 have hnz := e.nz_eq
227 refine ⟨fun j hj m hm => ?_, fun a ha1 ha2 ha3 ha4 => ?_⟩
228 · rw [hrest]
229 · exact hW j hj m hm
230 · intro hx
231 have : gSlot e.ls e.R (i + 1) = gAddr e.ls e.R e.mx j m := by omega
232 exact hg.slot_ne (i + 1) j m (by omega) (by omega) (by simpa using hs) (by omega) hm this
233 · by_cases hai : a = i + 1
234 · subst hai; exact hlink
235 · rw [hrest]
236 · exact hL a ha1 (by omega) ha3 ha4
237 · intro hx
238 have := hg.slot_inj a (i + 1) ha1 (by omega) ha4 (by omega) (by omega) (by simpa using hs) (by omega)
239 exact hai this
240
241theorem Env.get_hc (e : Env) (ca : Array Code) : Space.get (e.hc ca) e.rc = some ca := by
242 obtain ⟨ca0, h0⟩ := e.h_live
243 exact cget_put_self h0 e.h_ro ca
244
245theorem Env.get_wa (e : Env) (ca : Array Code) : Space.get (e.hc ca) e.rw = some e.wa := by
246 unfold Env.hc; rw [wget_put_code]; exact e.h_get_wa
247
248theorem Env.get_la (e : Env) (ca : Array Code) : Space.get (e.hc ca) e.rl = some e.la := by
249 unfold Env.hc; rw [wget_put_code]; exact e.h_get_la
250
251theorem Env.hc_hc (e : Env) (ca ca' : Array Code) : Space.put (e.hc ca) e.rc ca' = e.hc ca' := by
252 unfold Env.hc; rw [cput_put]
253
254theorem i32_ofInt_toInt {v : Int} (h1 : -2147483648 ≤ v) (h2 : v ≤ 2147483647) : (Int32.ofInt v).toInt = v := by
255 rw [Int32.toInt_ofInt]
256 simp only [Int32.size, Int.bmod]
257 omega
258
259theorem i32_le_zero {x : Int32} : x ≤ 0 ↔ x.toInt ≤ 0 := by
260 rw [Int32.le_iff_toInt_le, Int32.toInt_zero]
261
262theorem u32_succ {x : UInt32} (h : x.toNat < 1000000) : (x + 1).toNat = x.toNat + 1 := by
263 rw [u32_add (by simp [UInt32.toNat_one]; omega)]; simp [UInt32.toNat_one]
264
265def sizeCond (drop mx : UInt32) : UInt32 × Int32 × Bool → M (Bool × (UInt32 × Int32 × Bool)) :=
266 fun x => match x with | (curr, left, brk) => pure (!brk && decide (curr + drop < mx), (curr, left, brk))
267
268def sizeBody (count : Array UInt16) (drop : UInt32) : UInt32 × Int32 × Bool → M (UInt32 × Int32 × Bool) :=
269 fun x => match x with
270 | (curr, left, brk) => do
271 let cc ← geta count (curr + drop).toNat
272 let left ← chk32 (left.toInt - cc.toNat)
273 if left ≤ 0 then pure (curr, left, true)
274 else
275 let curr := curr + 1
276 let left ← chk32 (left.toInt * 2)
277 pure (curr, left, brk)
278
279theorem sizeBody_eq (count : Array UInt16) (drop curr : UInt32) (left : Int32) (brk : Bool)
280 (hi : (curr + drop).toNat < count.size)
281 (hv1 : -2147483648 ≤ left.toInt - (count[(curr + drop).toNat]).toNat)
282 (hv2 : left.toInt - (count[(curr + drop).toNat]).toNat ≤ 2147483647)
283 (hv3 : left.toInt - (count[(curr + drop).toNat]).toNat ≤ 0 ∨
284 (-2147483648 ≤ (left.toInt - (count[(curr + drop).toNat]).toNat) * 2 ∧
285 (left.toInt - (count[(curr + drop).toNat]).toNat) * 2 ≤ 2147483647)) :
286 sizeBody count drop (curr, left, brk) =
287 pure (if left.toInt - (count[(curr + drop).toNat]).toNat ≤ 0 then
288 (curr, Int32.ofInt (left.toInt - (count[(curr + drop).toNat]).toNat), true)
289 else (curr + 1, Int32.ofInt ((left.toInt - (count[(curr + drop).toNat]).toNat) * 2), brk)) := by
290 simp only [sizeBody]
291 rw [geta_eq hi, M_pure_bind, chk32_eq hv1 hv2, M_pure_bind]
292 generalize hv : left.toInt - (count[(curr + drop).toNat]).toNat = v at *
293 have hle : (Int32.ofInt v ≤ 0) ↔ v ≤ 0 := by rw [i32_le_zero, i32_ofInt_toInt hv1 hv2]
294 by_cases h0 : v ≤ 0
295 · rw [ite_eq_left (hle.mpr h0), ite_eq_left h0]
296 · rw [ite_eq_right (fun hh => h0 (hle.mp hh)), ite_eq_right h0]
297 have : -2147483648 ≤ v * 2 ∧ v * 2 ≤ 2147483647 := by
298 rcases hv3 with h | h
299 · exact absurd h h0
300 · exact h
301 rw [i32_ofInt_toInt hv1 hv2, chk32_eq this.1 this.2, M_pure_bind]
302
303/-- The sub-table sizing loop of `inflate_table`, run on the count array of the symbols that are still to be coded. -/
304theorem size_loop (e : Env) (i0 : Nat) (count : Array UInt16) (drop mx curr0 : UInt32) (left0 : Int32) (h : Heap)
305 (hcnt : CountOK e count i0) (hdrop : drop.toNat = e.R) (hmx : mx.toNat = e.mx) (hR : e.R < e.l i0)
306 (hc0 : curr0.toNat = e.l i0 - e.R) (hl0 : left0.toInt = 2 ^ curr0.toNat) (hi0 : i0 < e.m) :
307 Wp (cwhile (sizeCond drop mx) (sizeBody count drop) (curr0, left0, false)) h
308 (fun r h' => h' = h ∧ r.1.toNat = currOf e.f e.n e.R i0) := by
309 have hmxle : e.mx ≤ 15 := by
310 have := lenAt_bounds (f := e.f) (n := e.n) (show e.m - 1 < Tc e.f e.n 15 by have := e.h_pos; unfold Env.m; omega)
311 exact this.2
312 have hlmx : e.l i0 ≤ e.mx := lenAt_mono (f := e.f) (n := e.n) (show i0 ≤ Tc e.f e.n 15 - 1 by
313 have : i0 < e.m := hi0
314 unfold Env.m at this; omega) (by have := e.h_pos; omega)
315 have hR1 := e.h_R1
316 let T0 := SL (rem e.f e.n i0) e.R e.mx curr0.toNat left0.toInt
317 have hT0 : currOf e.f e.n e.R i0 = T0.1 := by
318 show (SL (rem e.f e.n i0) e.R e.mx (e.l i0 - e.R) ((2 ^ (e.l i0 - e.R) : Nat) : Int)).1 = T0.1
319 have : (curr0.toNat) = e.l i0 - e.R := hc0
320 simp only [T0, hl0, this]
321 push_cast; rfl
322 have hge1 : 1 ≤ e.l i0 - e.R := by omega
323 refine Wp.cwhile
324 (fun (x : UInt32 × Int32 × Bool) h' => h' = h ∧ x.1.toNat + e.R ≤ e.mx ∧
325 (x.2.2 = false → 0 < x.2.1.toInt ∧ x.2.1.toInt ≤ 2 ^ x.1.toNat ∧
326 SL (rem e.f e.n i0) e.R e.mx x.1.toNat x.2.1.toInt = T0) ∧
327 (x.2.2 = true → (x.1.toNat, x.2.1.toInt) = T0))
328 (fun (x : UInt32 × Int32 × Bool) => if x.2.2 then 0 else e.mx - e.R - x.1.toNat + 1)
329 (fun (x : UInt32 × Int32 × Bool) h' => h' = h ∧ x.1.toNat = currOf e.f e.n e.R i0) ?_ ?_ ?_
330 · rintro ⟨curr, left, brk⟩ h' ⟨hh, hb, hnb, hbk⟩
331 simp only at hb hnb hbk
332 by_cases hc : (!brk && decide (curr + drop < mx)) = true
333 · right
334 simp only [Bool.and_eq_true, Bool.not_eq_true', decide_eq_true_eq] at hc
335 obtain ⟨hbrk, hlt0⟩ := hc
336 have hlt : curr.toNat + e.R < e.mx := by
337 simp only [UInt32.lt_iff_toNat_lt] at hlt0
338 rw [u32_add (by have := UInt32.toNat_lt curr; omega)] at hlt0
339 omega
340 obtain ⟨hp, hle, hsl⟩ := hnb hbrk
341 have hidx : (curr + drop).toNat = curr.toNat + e.R := by
342 rw [u32_add (by have := UInt32.toNat_lt curr; have := UInt32.toNat_lt drop; omega), hdrop]
343 have hlt16 : (curr + drop).toNat < count.size := by rw [hcnt.1, hidx]; omega
344 have hcc : (count[(curr + drop).toNat]).toNat = rem e.f e.n i0 (curr.toNat + e.R) := by
345 have key := hcnt.2 (curr + drop).toNat (by omega) (by omega)
346 rw [Array.getD_eq_getD_getElem?, Array.getElem?_eq_getElem hlt16] at key
347 rw [← hidx]
348 simpa using key
349 have hccle : (count[(curr + drop).toNat]).toNat < 65536 := UInt16.toNat_lt _
350 have hpow : ((2:Int) ^ curr.toNat) ≤ 16384 := by
351 have h14 : 2 ^ curr.toNat ≤ 2 ^ 14 := Nat.pow_le_pow_right (by omega) (by omega)
352 have : ((2 ^ curr.toNat : Nat) : Int) ≤ ((2 ^ 14 : Nat) : Int) := Int.ofNat_le.mpr h14
353 simpa [Int.natCast_pow] using this
354 have e1 := sizeBody_eq count drop curr left brk hlt16 (by omega) (by omega) (by omega)
355 have hsl' := hsl
356 rw [SL_lt (show e.R + curr.toNat < e.mx by omega), show e.R + curr.toNat = curr.toNat + e.R by omega, ← hcc] at hsl'
357 have hrun : sizeBody count drop (curr, left, brk) h' = .ok
358 ((if left.toInt - (count[(curr + drop).toNat]).toNat ≤ 0 then
359 (curr, Int32.ofInt (left.toInt - (count[(curr + drop).toNat]).toNat), true)
360 else (curr + 1, Int32.ofInt ((left.toInt - (count[(curr + drop).toNat]).toNat) * 2), brk)), h') := by
361 rw [e1]; rfl
362 have hcond : sizeCond drop mx (curr, left, brk) h' = .ok ((true, (curr, left, brk)), h') := by
363 simp only [sizeCond]
364 show (pure ((!brk && decide (curr + drop < mx)), (curr, left, brk)) : M _) h' = _
365 rw [show ((!brk && decide (curr + drop < mx))) = true from by
366 simp only [Bool.and_eq_true, Bool.not_eq_true', decide_eq_true_eq]; exact ⟨hbrk, hlt0⟩]
367 rfl
368 generalize hvd : left.toInt - (count[(curr + drop).toNat]).toNat = v at *
369 have hr1 : -2147483648 ≤ v := by omega
370 have hr2 : v ≤ 2147483647 := by omega
371 have hp2 : (2:Int) ^ (curr.toNat + 1) = 2 ^ curr.toNat * 2 := Int.pow_succ _ _
372 refine ⟨(curr, left, brk), h', _, h', hcond, hrun, ?_, ?_⟩
373 · by_cases hv : v ≤ 0
374 · rw [ite_eq_left hv]
375 refine ⟨hh, by omega, fun hx => by simp at hx, fun _ => ?_⟩
376 rw [ite_eq_left hv] at hsl'
377 simp only []
378 rw [i32_ofInt_toInt hr1 hr2]
379 exact hsl'
380 · rw [ite_eq_right hv]
381 have hcu : (curr + 1).toNat = curr.toNat + 1 := u32_succ (by omega)
382 have hr3 : -2147483648 ≤ v * 2 := by omega
383 have hr4 : v * 2 ≤ 2147483647 := by omega
384 refine ⟨hh, by rw [hcu]; omega, fun _ => ?_, fun hx => by simp [hbrk] at hx⟩
385 simp only []
386 rw [hcu, i32_ofInt_toInt hr3 hr4]
387 refine ⟨by omega, by omega, ?_⟩
388 rw [ite_eq_right hv] at hsl'
389 exact hsl'
390 · by_cases hv : v ≤ 0
391 · rw [ite_eq_left hv]; simp [hbrk] <;> omega
392 · rw [ite_eq_right hv]
393 have hcu : (curr + 1).toNat = curr.toNat + 1 := u32_succ (by omega)
394 simp [hbrk, hcu] <;> omega
395 · left
396 have hcond : sizeCond drop mx (curr, left, brk) h' = .ok ((false, (curr, left, brk)), h') := by
397 simp only [sizeCond]
398 show (pure ((!brk && decide (curr + drop < mx)), (curr, left, brk)) : M _) h' = _
399 have : ((!brk && decide (curr + drop < mx))) = false := by
400 cases hb2 : ((!brk && decide (curr + drop < mx)))
401 · rfl
402 · exact absurd hb2 hc
403 rw [this]; rfl
404 refine ⟨(curr, left, brk), h', hcond, hh, ?_⟩
405 rw [hT0]
406 cases hbrk : brk
407 · have hn : ¬ (curr + drop < mx) := by
408 intro hlt0
409 apply hc
410 simp [hbrk, hlt0]
411 simp only [UInt32.lt_iff_toNat_lt] at hn
412 rw [u32_add (by have := UInt32.toNat_lt curr; omega)] at hn
413 obtain ⟨hp, hle, hsl⟩ := hnb hbrk
414 rw [SL_ge (by omega)] at hsl
415 rw [← hsl]
416 · have := hbk hbrk
417 rw [← this]
418 · dsimp only
419 refine ⟨rfl, by omega, fun _ => ⟨?_, ?_, rfl⟩, fun hx => by simp at hx⟩
420 · rw [hl0]; exact_mod_cast (Nat.pow_pos (by omega : 0 < 2) : 0 < 2 ^ curr0.toNat)
421 · rw [hl0]; exact Int.le_refl _
422 · show (if false = true then 0 else e.mx - e.R - curr0.toNat + 1) < fuel
423 simp only [Bool.false_eq_true, ite_false]
424 exact lt_fuel (by omega)
425
426theorem Wp.pure_eq {α : Type} {m : M α} {a : α} {h : Heap} {Q : α → Heap → Prop} (e : m = pure a) (hq : Q a h) :
427 Wp m h Q := ⟨a, h, by rw [e]; rfl, hq⟩
428
429theorem wp_add (e : Env) (ca : Array Code) (off n : Nat) (hn : off + n ≤ ca.size) :
430 Wp (Ptr.add (Ptr.ref e.rc off) (n : Int)) (e.hc ca) (fun q h' => q = Ptr.ref e.rc (off + n) ∧ h' = e.hc ca) :=
431 Wp.of_eq (Ptr.add_nat_ok (e.get_hc ca) hn) ⟨rfl, rfl⟩
432
433/-- `q = table + low; e = *q; *q = F e; K` -/
434theorem wp_update {β : Type} (e : Env) (ca : Array Code) (low : Nat) (F : Code → Code) (hlow : e.oc + low < ca.size)
435 (K : M β) (Q : β → Heap → Prop)
436 (hK : ∀ ca1, ca1 = ca.set! (e.oc + low) (F ca[e.oc + low]) → Wp K (e.hc ca1) Q) :
437 Wp (do
438 let q ← Ptr.add (Ptr.ref e.rc e.oc) (low : Int)
439 let x ← Ptr.load q
440 Ptr.store q (F x)
441 K) (e.hc ca) Q := by
442 apply Wp.bind' (wp_add e ca e.oc low (by omega))
443 rintro q h' ⟨rfl, rfl⟩
444 apply Wp.bind' (Q := fun x h' => x = ca[e.oc + low] ∧ h' = e.hc ca)
445 · exact Wp.of_eq (Ptr.load_ok (e.get_hc ca) hlow) ⟨rfl, rfl⟩
446 · rintro x h' ⟨rfl, rfl⟩
447 apply Wp.bind' (Q := fun _ h' => h' = e.hc (ca.set! (e.oc + low) (F ca[e.oc + low])))
448 · refine ⟨(), _, Ptr.store_ok (e.get_hc ca) e.h_ro (by omega), ?_⟩
449 rw [Env.hc_hc]
450 · rintro _ h' rfl
451 exact hK _ rfl
452
453theorem getElem?_set!_ne {α : Type} {a : Array α} {i j : Nat} {v : α} (h : i ≠ j) : (a.set! i v)[j]? = a[j]? := by
454 rw [Array.set!_eq_setIfInBounds, Array.getElem?_setIfInBounds]; simp [h]
455
456theorem getElem?_set!_self {α : Type} {a : Array α} {i : Nat} {v : α} (h : i < a.size) : (a.set! i v)[i]? = some v := by
457 rw [Array.set!_eq_setIfInBounds, Array.getElem?_setIfInBounds]; simp [h]
458
459theorem tooBig_ne {t u : UInt32} (h : tooBig t u = true) : t ≠ CODES := by
460 intro ht
461 subst ht
462 simp [tooBig, CODES, LENS, DISTS] at h
463
464theorem tooBig_le (e : Env) {u : UInt32} (h : tooBig e.c.type u = false) (hne : e.c.type ≠ CODES) :
465 u.toNat ≤ e.cap := by
466 have hcap := e.h_cap
467 rcases e.h_type with ht | ht | ht
468 · exact absurd ht hne
469 · rw [ht] at h hcap
470 simp only [tooBig, LENS, DISTS, CODES] at h hcap
471 have h2 : ¬ (u > ENOUGH_LENS.toUInt32) := by simpa using h
472 rw [UInt32.not_lt, UInt32.le_iff_toNat_le] at h2
473 have : (ENOUGH_LENS.toUInt32).toNat = 852 := rfl
474 simp at hcap
475 omega
476 · rw [ht] at h hcap
477 simp only [tooBig, LENS, DISTS, CODES] at h hcap
478 have h2 : ¬ (u > ENOUGH_DISTS.toUInt32) := by simpa using h
479 rw [UInt32.not_lt, UInt32.le_iff_toNat_le] at h2
480 have : (ENOUGH_DISTS.toUInt32).toNat = 592 := rfl
481 simp at hcap
482 omega
483
484def fillBody : TS → M TS := fun s => do
485 let fill := s.fill - s.incr
486 let hd ← shr32 s.huff s.drop
487 storeCode s.next (hd + fill).toNat s.here
488 pure { s with fill }
489
490def fillCond : TS → M (Bool × TS) := fun s => pure (s.fill != 0, s)
491
492theorem Nat_mul_pred (S q : Nat) (hq : 1 ≤ q) : S * (q - 1) + S = S * q := by
493 obtain ⟨r, rfl⟩ : ∃ r, q = r + 1 := ⟨q - 1, by omega⟩
494 simp [Nat.mul_succ]
495
496theorem fillBody_wp (e : Env) (s : TS) (ca1 : Array Code) (k : Nat) (hnext : s.next = .ref e.rc (e.oc + k))
497 (hdrop : s.drop.toNat < 32)
498 (hidx : e.oc + k + ((s.huff >>> s.drop) + (s.fill - s.incr)).toNat < ca1.size) :
499 Wp (fillBody s) (e.hc ca1) (fun s1 h1 => s1 = { s with fill := s.fill - s.incr } ∧
500 h1 = e.hc (ca1.set! (e.oc + k + ((s.huff >>> s.drop) + (s.fill - s.incr)).toNat) s.here)) := by
501 unfold fillBody
502 rw [shr32_eq hdrop]
503 apply Wp.bind' (Q := fun r h' => r = s.huff >>> s.drop ∧ h' = e.hc ca1) (Wp.pure' ⟨rfl, rfl⟩)
504 rintro hd h' ⟨rfl, rfl⟩
505 unfold storeCode
506 rw [hnext]
507 apply Wp.bind' (Q := fun _ h' => h' = e.hc (ca1.set! (e.oc + k + ((s.huff >>> s.drop) + (s.fill - s.incr)).toNat) s.here))
508 · apply Wp.bind' (wp_add e ca1 (e.oc + k) ((s.huff >>> s.drop) + (s.fill - s.incr)).toNat (by omega))
509 rintro q h' ⟨rfl, rfl⟩
510 refine ⟨(), _, Ptr.store_ok (e.get_hc ca1) e.h_ro (by omega), ?_⟩
511 rw [Env.hc_hc]
512 · rintro _ h' rfl
513 exact Wp.pure' ⟨rfl, rfl⟩
514
515/-- The `do ... while (fill != 0)` loop that writes a code into the table: `S = 2^b` is the stride, `N` the number
516of copies, `fill` starts at `S * N`. -/
517theorem fill_loop (e : Env) (s0 : TS) (ca : Array Code) (S N k hd : Nat)
518 (hnext : s0.next = .ref e.rc (e.oc + k)) (hS : s0.incr.toNat = S) (hF : s0.fill.toNat = S * N)
519 (hN : 1 ≤ N) (hSpos : 1 ≤ S) (hhd : (s0.huff >>> s0.drop).toNat = hd) (hhdS : hd < S)
520 (hdrop : s0.drop.toNat < 32) (hk : k + S * N ≤ e.cap) (hsz : e.oc + e.cap ≤ ca.size) :
521 Wp (cdoWhile fillBody fillCond s0) (e.hc ca) (fun s' h' => ∃ ca', h' = e.hc ca' ∧
522 s' = { s0 with fill := 0 } ∧ ca'.size = ca.size ∧
523 (∀ x, (∃ q', q' < N ∧ x = e.oc + k + hd + S * q') → ca'[x]? = some s0.here) ∧
524 (∀ x, ¬ (∃ q', q' < N ∧ x = e.oc + k + hd + S * q') → ca'[x]? = ca[x]?)) := by
525 refine Wp.cdoWhile
526 (fun (s : TS) h' => ∃ q ca1, 1 ≤ q ∧ q ≤ N ∧ s = { s0 with fill := UInt32.ofNat (S * q) } ∧ h' = e.hc ca1 ∧
527 ca1.size = ca.size ∧
528 (∀ x, (∃ q', q ≤ q' ∧ q' < N ∧ x = e.oc + k + hd + S * q') → ca1[x]? = some s0.here) ∧
529 (∀ x, ¬ (∃ q', q ≤ q' ∧ q' < N ∧ x = e.oc + k + hd + S * q') → ca1[x]? = ca[x]?))
530 (fun (s : TS) => s.fill.toNat) _ ?_ ?_ ?_
531 · rintro s h' ⟨q, ca1, hq1, hqN, rfl, rfl, hp0, hp1, hp2⟩
532 dsimp only
533 have hSq : S * q ≤ S * N := Nat.mul_le_mul_left S hqN
534 have hSq' := Nat_mul_pred S q hq1
535 have hlt32 : S * q < 2 ^ 32 := by
536 have : s0.fill.toNat < 2 ^ 32 := UInt32.toNat_lt _
537 omega
538 have hfill : (UInt32.ofNat (S * q)).toNat = S * q := by
539 rw [UInt32.toNat_ofNat', Nat.mod_eq_of_lt hlt32]
540 have hsub : (UInt32.ofNat (S * q) - s0.incr).toNat = S * (q - 1) := by
541 rw [u32_sub (by rw [hfill, hS]; omega), hfill, hS]; omega
542 have hidx : e.oc + k + hd + S * (q - 1) < e.oc + k + S * N := by omega
543 have hidx2 : e.oc + k + hd + S * (q - 1) < ca1.size := by omega
544 obtain ⟨s1, h1, hrun, hs1, hh1⟩ := fillBody_wp e { s0 with fill := UInt32.ofNat (S * q) } ca1 k hnext hdrop
545 (by
546 show e.oc + k + ((s0.huff >>> s0.drop) + (UInt32.ofNat (S * q) - s0.incr)).toNat < ca1.size
547 have : (s0.huff >>> s0.drop + (UInt32.ofNat (S * q) - s0.incr)).toNat = hd + S * (q - 1) := by
548 rw [u32_add (by rw [hsub, hhd]; omega), hsub, hhd]
549 omega)
550 have hidxv : ((s0.huff >>> s0.drop) + (UInt32.ofNat (S * q) - s0.incr)).toNat = hd + S * (q - 1) := by
551 rw [u32_add (by rw [hsub, hhd]; omega), hsub, hhd]
552 simp only [] at hs1 hh1
553 rw [hidxv] at hh1
554 refine ⟨s1, h1, hrun, ?_⟩
555 have hPlt : e.oc + k + (hd + S * (q - 1)) < ca1.size := by omega
556 have hnew : ∀ ca2 : Array Code, ca2 = ca1.set! (e.oc + k + (hd + S * (q - 1))) s0.here →
557 ca2.size = ca.size ∧
558 (∀ x, (∃ q', q - 1 ≤ q' ∧ q' < N ∧ x = e.oc + k + hd + S * q') → ca2[x]? = some s0.here) ∧
559 (∀ x, ¬ (∃ q', q - 1 ≤ q' ∧ q' < N ∧ x = e.oc + k + hd + S * q') → ca2[x]? = ca[x]?) := by
560 intro ca2 h2
561 refine ⟨by rw [h2, Array.size_set!]; exact hp0, ?_, ?_⟩
562 · rintro x ⟨q', hq1', hq2', hx⟩
563 by_cases hxP : x = e.oc + k + (hd + S * (q - 1))
564 · rw [h2, hxP]; exact getElem?_set!_self hPlt
565 · have hq'q : q ≤ q' := by
566 apply Classical.byContradiction; intro hcon
567 apply hxP
568 have : q' = q - 1 := by omega
569 rw [hx, this]; omega
570 rw [h2, getElem?_set!_ne (Ne.symm hxP)]
571 exact hp1 x ⟨q', hq'q, hq2', hx⟩
572 · intro x hx
573 have hxP : x ≠ e.oc + k + (hd + S * (q - 1)) := by
574 intro hxx; apply hx; exact ⟨q - 1, Nat.le_refl _, by omega, by omega⟩
575 rw [h2, getElem?_set!_ne (Ne.symm hxP)]
576 apply hp2
577 rintro ⟨q', hq1', hq2', hx'⟩
578 exact hx ⟨q', by omega, hq2', hx'⟩
579 by_cases hq : q = 1
580 · subst hq
581 left
582 have hfz : (UInt32.ofNat (S * 1) - s0.incr) = 0 := by
583 apply UInt32.toNat_inj.mp
584 rw [hsub]; simp
585 refine ⟨s1, h1, ?_, _, hh1, ?_, (hnew _ rfl).1, ?_, ?_⟩
586 · rw [hs1]; simp only [fillCond, hfz]; rfl
587 · rw [hs1, hfz]
588 · exact fun x ⟨q', h2, h3⟩ => (hnew _ rfl).2.1 x ⟨q', by omega, h2, h3⟩
589 · exact fun x hx => (hnew _ rfl).2.2 x (fun ⟨q', h2, h3, h4⟩ => hx ⟨q', h3, h4⟩)
590 · right
591 have hfnz : (UInt32.ofNat (S * q) - s0.incr) ≠ 0 := by
592 intro h0
593 have := congrArg UInt32.toNat h0
594 rw [hsub] at this
595 simp at this
596 have hpos : 0 < S * (q - 1) := Nat.mul_pos (by omega) (by omega)
597 omega
598 refine ⟨s1, h1, ?_, ?_, ?_⟩
599 · rw [hs1]; simp only [fillCond]
600 have : ((UInt32.ofNat (S * q) - s0.incr) != 0) = true := by simpa using hfnz
601 rw [this]; rfl
602 · refine ⟨q - 1, _, by omega, by omega, ?_, hh1, (hnew _ rfl).1, (hnew _ rfl).2.1, (hnew _ rfl).2.2⟩
603 rw [hs1]
604 have : UInt32.ofNat (S * (q - 1)) = UInt32.ofNat (S * q) - s0.incr := by
605 apply UInt32.toNat_inj.mp
606 rw [hsub, UInt32.toNat_ofNat', Nat.mod_eq_of_lt (by omega)]
607 rw [this]
608 · rw [hs1]
609 simp only []
610 rw [hsub, hfill]
611 have : 0 < S := hSpos
612 have : S * (q - 1) + S = S * q := hSq'
613 omega
614 · refine ⟨N, ca, hN, Nat.le_refl _, ?_, rfl, rfl, ?_, ?_⟩
615 · have : s0.fill = UInt32.ofNat (S * N) := by
616 apply UInt32.toNat_inj.mp
617 rw [hF, UInt32.toNat_ofNat', Nat.mod_eq_of_lt (by have := UInt32.toNat_lt s0.fill; omega)]
618 rw [← this]
619 · rintro x ⟨q', h1, h2, _⟩; omega
620 · intro x _; rfl
621 · exact lt_fuel (UInt32.toNat_lt s0.fill)
622
623theorem and_pow_zero_iff (x e : Nat) : x &&& 2 ^ e = 0 ↔ x.testBit e = false := by
624 constructor
625 · intro h
626 have := congrArg (fun y => y.testBit e) h
627 simpa [Nat.testBit_and, Nat.testBit_two_pow] using this
628 · intro h
629 apply Nat.eq_of_testBit_eq
630 intro i
631 simp only [Nat.testBit_and, Nat.testBit_two_pow, Nat.zero_testBit]
632 by_cases hie : e = i
633 · subst hie; simp [h]
634 · simp [hie]
635
636def incrCond : TS → M (Bool × TS) := fun s => pure (s.huff &&& s.incr != 0, s)
637def incrBody : TS → M TS := fun s => pure { s with incr := s.incr >>> 1 }
638
639/-- `while (huff & incr) incr >>= 1;` started at `incr = 2^e`. -/
640theorem incr_loop (s3 : TS) (e : Nat) (he : e < 32) (hi : s3.incr.toNat = 2 ^ e) (h : Heap) :
641 Wp (cwhile incrCond incrBody s3) h (fun s' h' => h' = h ∧
642 ∃ X : UInt32, s' = { s3 with incr := X } ∧ X.toNat = incrLoop s3.huff.toNat e) := by
643 refine Wp.cwhile
644 (fun (s : TS) h' => h' = h ∧ (∃ X : UInt32, s = { s3 with incr := X }) ∧
645 ((∃ e', e' ≤ e ∧ s.incr.toNat = 2 ^ e' ∧ incrLoop s3.huff.toNat e' = incrLoop s3.huff.toNat e) ∨
646 (s.incr = 0 ∧ incrLoop s3.huff.toNat e = 0)))
647 (fun (s : TS) => s.incr.toNat) _ ?_ ?_ ?_
648 · rintro s h' ⟨rfl, ⟨X, rfl⟩, hinv⟩
649 dsimp only at hinv ⊢
650 rcases hinv with ⟨e', he', hX, hT⟩ | ⟨hX, hT⟩
651 · have hand : (s3.huff &&& X).toNat = s3.huff.toNat &&& 2 ^ e' := by rw [UInt32.toNat_and, hX]
652 by_cases hb : s3.huff.toNat.testBit e' = true
653 · right
654 have hne : (s3.huff &&& X != 0) = true := by
655 simp only [bne_iff_ne, ne_eq, ← UInt32.toNat_inj, hand]
656 intro hz
657 have := (and_pow_zero_iff _ _).mp hz
658 rw [hb] at this; exact absurd this (by simp)
659 refine ⟨{ s3 with incr := X }, h', { s3 with incr := X >>> 1 }, h', ?_, ?_, ?_, ?_⟩
660 · simp only [incrCond]; rw [hne]; rfl
661 · simp only [incrBody]; rfl
662 · refine ⟨rfl, ⟨X >>> 1, rfl⟩, ?_⟩
663 rcases Nat.eq_zero_or_pos e' with h0 | hpos
664 · right
665 subst h0
666 refine ⟨?_, ?_⟩
667 · apply UInt32.toNat_inj.mp
668 rw [u32_shr (by decide), hX]; simp
669 · rw [← hT]; simp [incrLoop, hb]
670 · left
671 refine ⟨e' - 1, by omega, ?_, ?_⟩
672 · rw [u32_shr (by decide), hX]
673 obtain ⟨r, rfl⟩ : ∃ r, e' = r + 1 := ⟨e' - 1, by omega⟩
674 simp [Nat.pow_succ, Nat.mul_div_cancel]
675 · rw [← hT]
676 obtain ⟨r, rfl⟩ : ∃ r, e' = r + 1 := ⟨e' - 1, by omega⟩
677 simp [incrLoop, hb]
678 · dsimp only
679 rw [u32_shr (by decide), hX]
680 simp only [UInt32.toNat_one, Nat.pow_one]
681 have : 0 < 2 ^ e' := Nat.pow_pos (by omega)
682 omega
683 · left
684 have hb' : s3.huff.toNat.testBit e' = false := by simpa using hb
685 have hz : (s3.huff &&& X != 0) = false := by
686 have : (s3.huff &&& X).toNat = 0 := by rw [hand]; exact (and_pow_zero_iff _ _).mpr hb'
687 have h2 : s3.huff &&& X = 0 := UInt32.toNat_inj.mp (by rw [this]; rfl)
688 simp [h2]
689 refine ⟨{ s3 with incr := X }, h', ?_, rfl, X, rfl, ?_⟩
690 · simp only [incrCond]; rw [hz]; rfl
691 · rw [← hT, hX]
692 obtain ⟨r, hr⟩ : ∃ r, e' = r := ⟨e', rfl⟩
693 cases e' with
694 | zero => simp [incrLoop, hb']
695 | succ r => simp [incrLoop, hb']
696 · left
697 have hz : (s3.huff &&& X != 0) = false := by simp [hX]
698 refine ⟨{ s3 with incr := X }, h', ?_, rfl, X, rfl, ?_⟩
699 · simp only [incrCond]; rw [hz]; rfl
700 · rw [hX, hT]; rfl
701 · refine ⟨rfl, ⟨s3.incr, rfl⟩, Or.inl ⟨e, Nat.le_refl _, hi, rfl⟩⟩
702 · exact lt_fuel (UInt32.toNat_lt _)
703
704theorem FrameCA.trans {e : Env} {a b c : Array Code} (h1 : FrameCA e a b) (h2 : FrameCA e b c) : FrameCA e a c :=
705 ⟨h2.1.trans h1.1, fun x hx => (h2.2 x hx).trans (h1.2 x hx)⟩
706
707theorem i64_u16 (n : Nat) : (Int64.ofInt (n : Int)).toUInt64.toUInt16 = n.toUInt16 := by
708 have : (Int64.ofInt (n : Int)).toUInt64 = UInt64.ofNat n := rfl
709 rw [this]
710 apply UInt16.toNat_inj.mp
711 rw [UInt64.toNat_toUInt16, UInt64.toNat_ofNat']
712 simp [Nat.toUInt16, UInt16.toNat_ofNat']
713
714theorem u32_toUInt8 (x : UInt32) : x.toUInt8 = x.toNat.toUInt8 := by
715 apply UInt8.toNat_inj.mp
716 rw [UInt32.toNat_toUInt8]; simp [Nat.toUInt8, UInt8.toNat_ofNat']
717
718/-- Three updates of the same cell, each setting one field, leave the three fields set. -/
719theorem triple_entry {ca ca1 ca2 ca3 : Array Code} {idx : Nat} (hidx : idx < ca.size) (hs1 : idx < ca1.size)
720 (hs2 : idx < ca2.size) {c1 c2 : UInt8} {c3 : UInt16}
721 (h1 : ca1 = ca.set! idx ⟨c1, (ca[idx]'hidx).bits, (ca[idx]'hidx).val⟩)
722 (h2 : ca2 = ca1.set! idx ⟨(ca1[idx]'hs1).op, c2, (ca1[idx]'hs1).val⟩)
723 (h3 : ca3 = ca2.set! idx ⟨(ca2[idx]'hs2).op, (ca2[idx]'hs2).bits, c3⟩) :
724 ca3[idx]? = some ⟨c1, c2, c3⟩ := by
725 have e1 : ca1[idx]'hs1 = ⟨c1, (ca[idx]'hidx).bits, (ca[idx]'hidx).val⟩ := by
726 have := getElem?_set!_self (a := ca) (i := idx) (v := (⟨c1, (ca[idx]'hidx).bits, (ca[idx]'hidx).val⟩ : Code)) hidx
727 rw [← h1, Array.getElem?_eq_getElem hs1] at this
728 exact Option.some.inj this
729 have e2 : ca2[idx]'hs2 = ⟨(ca1[idx]'hs1).op, c2, (ca1[idx]'hs1).val⟩ := by
730 have := getElem?_set!_self (a := ca1) (i := idx) (v := (⟨(ca1[idx]'hs1).op, c2, (ca1[idx]'hs1).val⟩ : Code)) hs1
731 rw [← h2, Array.getElem?_eq_getElem hs2] at this
732 exact Option.some.inj this
733 have := getElem?_set!_self (a := ca2) (i := idx) (v := (⟨(ca2[idx]'hs2).op, (ca2[idx]'hs2).bits, c3⟩ : Code)) hs2
734 rw [← h3] at this
735 rw [this, e2, e1]
736
737/-- Premise of `openBody`: the state when a new sub-table is opened for the code `i + 1`. -/
738def OB (e : Env) (i : Nat) (s : TS) (ca : Array Code) : Prop :=
739 i + 1 < e.m ∧ s.exit = 0 ∧ s.sym.toNat = i + 1 ∧ s.len.toNat = e.l (i + 1) ∧
740 s.huff.toNat = rev (e.l (i + 1)) (e.v (i + 1)) ∧ s.mask.toNat = 2 ^ e.R - 1 ∧
741 CountOK e s.count (i + 1) ∧ e.oc + e.cap ≤ ca.size ∧
742 (∃ k, s.next = .ref e.rc (e.oc + k) ∧ k + 2 ^ s.curr.toNat = s.used.toNat) ∧
743 s.used.toNat ≤ e.cap ∧ 2 ^ e.R ≤ s.used.toNat ∧ 1 ≤ s.curr.toNat ∧ s.curr.toNat ≤ 15 ∧
744 s.min.toNat = 2 ^ s.curr.toNat ∧ e.R < e.l (i + 1) ∧ s.drop.toNat = e.R ∧
745 e.v (i + 1) % 2 ^ (e.l (i + 1) - e.R) = 0
746
747theorem openBody_wp (e : Env) (i : Nat) (s : TS) (ca : Array Code) (h : OB e i s ca)
748 (hx : DescB e i s ∧ Cont e (i + 1) i ca) (hst : Canon.startsAt e.ls e.R i) :
749 Wp (openBody e.c s) (e.hc ca) (fun s' h' => ∃ ca', h' = e.hc ca' ∧ FrameCA e ca ca' ∧
750 ((s'.exit = 0 ∧ MI e (i + 1) s' ca' ∧ Ex e (i + 1) s' ca') ∨
751 (s'.exit = 2 ∧ e.c.type ≠ CODES ∧ e.oc + e.cap ≤ ca'.size))) := by
752 obtain ⟨hxD, hxC⟩ := hx
753 obtain ⟨hi, hex, hsym, hlen, hhuff, hmask, hcnt, hsz, ⟨k, hnext, hku⟩, hucap, hu2R, hc1, hc15, hmin, hRl, hdrop, halign⟩ := h
754 have hmxle : e.mx ≤ 15 := by
755 have := lenAt_bounds (f := e.f) (n := e.n) (show e.m - 1 < Tc e.f e.n 15 by have := e.h_pos; unfold Env.m; omega)
756 exact this.2
757 have hlmx : e.l (i + 1) ≤ e.mx := lenAt_mono (f := e.f) (n := e.n) (show i + 1 ≤ Tc e.f e.n 15 - 1 by
758 have : i + 1 < e.m := hi
759 unfold Env.m at this; omega) (by have := e.h_pos; omega)
760 have hR1 := e.h_R1
761 rcases s with ⟨huff, sym, len, curr, drop, low, used, min, fill, incr, mask, left, next, here, count, exit⟩
762 dsimp only at *
763 subst hnext
764 obtain ⟨⟨k', hk'1, hk'2⟩, hcurrD, husedD⟩ := hxD
765 have hkb : k = (e.D i).base := by
766 have := Ptr.ref.inj hk'1
767 have : k = k' := by omega
768 rw [this]; exact hk'2
769 unfold openBody
770 apply Wp.bind' (wp_add e ca (e.oc + k) min.toNat (by rw [hmin]; omega))
771 rintro nxt h' ⟨rfl, rfl⟩
772 dsimp only
773 rw [e.h_table]
774 have hR15 : e.R + 1 ≤ e.l (i + 1) := hRl
775 have hsubl : (len - drop).toNat = e.l (i + 1) - e.R := by
776 rw [u32_sub (by omega), hlen, hdrop]
777 have hcl31 : (len - drop).toNat < 31 := by omega
778 apply Wp.bind' (Q := fun r h' => r = 1 <<< (len - drop).toInt32 ∧ h' = e.hc ca)
779 (Wp.pure_eq (shl1i32_eq hcl31) ⟨rfl, rfl⟩)
780 rintro l0 h' ⟨rfl, rfl⟩
781 have hl0 : (1 <<< (len - drop).toInt32 : Int32).toInt = 2 ^ (len - drop).toNat := shl1i32_toInt hcl31
782 apply Wp.bind' (size_loop e (i + 1) count drop e.c.max (len - drop) _ (e.hc ca) hcnt hdrop e.h_max hRl hsubl hl0 hi)
783 rintro ⟨cs, ls, bs⟩ h' ⟨rfl, hcs⟩
784 dsimp only at hcs ⊢
785 obtain ⟨bb1, bb2, bb3⟩ := block_bound (f := e.f) (n := e.n) (R := e.R) (i0 := i + 1) hi hRl halign
786 have hcs' : cs.toNat = currOf e.f e.n e.R (i + 1) := hcs
787 have hbb1 : e.l (i + 1) ≤ e.R + cs.toNat := by rw [hcs']; exact bb1
788 have hbb2 : e.R + cs.toNat ≤ e.mx := by rw [hcs']; exact bb2
789 have hne : e.c.type ≠ CODES := by
790 intro ht
791 have := (e.h_codes ht).2.1
792 have h3 : e.mx = mxl e.f e.n := rfl
793 omega
794 have hcs32 : cs.toNat < 32 := by omega
795 apply Wp.bind' (Q := fun r h' => r = 1 <<< cs ∧ h' = e.hc ca) (Wp.pure_eq (shl32_eq hcs32) ⟨rfl, rfl⟩)
796 rintro u h' ⟨rfl, rfl⟩
797 have hu : ((1 : UInt32) <<< cs).toNat = 2 ^ cs.toNat := u32_shl1 hcs32
798 have hpow14 : 2 ^ cs.toNat ≤ 2 ^ 14 := Nat.pow_le_pow_right (by omega) (by omega)
799 have hcap_le : e.cap ≤ 852 := by
800 have := e.h_cap
801 rcases e.h_type with ht | ht | ht <;> simp [ht, CODES, LENS, DISTS] at this <;> omega
802 have hused' : (used + (1 <<< cs)).toNat = used.toNat + 2 ^ cs.toNat := by
803 rw [u32_add (a := used) (b := 1 <<< cs) (by omega), hu]
804 by_cases hb : tooBig e.c.type (used + (1 <<< cs)) = true
805 · rw [ite_eq_left hb]
806 exact Wp.pure' ⟨ca, rfl, ⟨rfl, fun _ _ => rfl⟩, Or.inr ⟨rfl, tooBig_ne hb, hsz⟩⟩
807 · rw [ite_eq_right hb]
808 have hb' : tooBig e.c.type (used + (1 <<< cs)) = false := by simpa using hb
809 have hucap' := tooBig_le e hb' hne
810 rw [hused'] at hucap'
811 have hmask' : (huff &&& mask).toNat = rev e.R (e.p (i + 1)) := by
812 rw [u32_and_mod (k := e.R) (by rw [hmask]), hhuff]
813 exact huff_low (f := e.f) (n := e.n) (R := e.R) (j := i + 1) (show e.R ≤ e.l (i + 1) by omega)
814 have hlowlt : (huff &&& mask).toNat < 2 ^ e.R := by rw [hmask']; exact rev_lt _ _
815 have hidx : e.oc + (huff &&& mask).toNat < ca.size := by omega
816 refine wp_update e ca (huff &&& mask).toNat (fun x => ⟨cs.toUInt8, x.bits, x.val⟩) hidx _ _ (fun ca1 h1 => ?_)
817 have hs1 : ca1.size = ca.size := by rw [h1, Array.size_set!]
818 refine wp_update e ca1 (huff &&& mask).toNat (fun x => ⟨x.op, e.c.root.toUInt8, x.val⟩) (by omega) _ _
819 (fun ca2 h2 => ?_)
820 have hs2 : ca2.size = ca.size := by rw [h2, Array.size_set!, hs1]
821 apply Wp.bind' (Q := fun d h' => d = Int64.ofInt ((↑(e.oc + k + min.toNat) : Int) - ↑e.oc) ∧ h' = e.hc ca2)
822 (Wp.of_eq (Ptr.diff_ok (o1 := e.oc + k + min.toNat) (o2 := e.oc) (e.get_hc ca2) (by omega) (by omega)
823 (by constructor <;> omega)) ⟨rfl, rfl⟩)
824 rintro d h' ⟨hd, rfl⟩
825 refine wp_update e ca2 (huff &&& mask).toNat
826 (fun x => ⟨x.op, x.bits, d.toUInt64.toUInt16⟩)
827 (by omega) _ _ (fun ca3 h3 => ?_)
828 have hs3 : ca3.size = ca.size := by rw [h3, Array.size_set!, hs2]
829 have hfr : ∀ x, (x < e.oc ∨ e.oc + e.cap ≤ x) → ca3[x]? = ca[x]? := by
830 intro x hx
831 have hne1 : e.oc + (huff &&& mask).toNat ≠ x := by omega
832 rw [h3, getElem?_set!_ne hne1, h2, getElem?_set!_ne hne1, h1, getElem?_set!_ne hne1]
833 have hs1' : e.oc + (huff &&& mask).toNat < ca1.size := by omega
834 have hs2' : e.oc + (huff &&& mask).toNat < ca2.size := by omega
835 have hentry := triple_entry (idx := e.oc + (huff &&& mask).toNat) hidx hs1' hs2' (c1 := cs.toUInt8)
836 (c2 := e.c.root.toUInt8) (c3 := d.toUInt64.toUInt16) h1 h2 h3
837 have hge1 : 1 ≤ e.R := hR1
838 have hst' := (startsAt_iff e.f e.n e.R (show i + 1 < Tc e.f e.n 15 from hi)).mp hst
839 have hDn : e.D (i + 1) = ⟨e.R, Canon.width e.ls (i + 1) e.R e.mx, (e.D i).base + 2 ^ (e.D i).curr,
840 (e.D i).used + 2 ^ Canon.width e.ls (i + 1) e.R e.mx, Canon.rev e.R (Canon.grp e.ls e.R (i + 1))⟩ := by
841 exact desc_succ_of_starts e.ls e.R e.mx i hst
842 have hwid : Canon.width e.ls (i + 1) e.R e.mx = cs.toNat := by
843 rw [hcs']
844 exact width_eq e.f e.n e.R hR1 hi (by omega) hRl hmxle
845 have hgrp : Canon.grp e.ls e.R (i + 1) = e.p (i + 1) :=
846 grp_eq_pre e.f e.n e.R hi (by omega)
847 have hdd : d.toUInt64.toUInt16 = ((e.D i).base + 2 ^ (e.D i).curr).toUInt16 := by
848 rw [hd]
849 have : ((↑(e.oc + k + min.toNat) : Int) - ↑e.oc) = ((k + min.toNat : Nat) : Int) := by push_cast; omega
850 rw [this, i64_u16]
851 congr 1
852 rw [hmin, hcurrD, hkb]
853 have hrootR : e.c.root.toUInt8 = e.R.toUInt8 := by rw [u32_toUInt8, e.h_root]
854 have hlinke : ca3[e.oc + gSlot e.ls e.R (i + 1)]? = some (e.link (i + 1)) := by
855 have hsl : gSlot e.ls e.R (i + 1) = (huff &&& mask).toNat := by
856 unfold gSlot
857 rw [hmask', hgrp, canon_rev_eq]
858 rw [hsl, hentry]
859 unfold Env.link
860 rw [hDn, hwid, hrootR, hdd, u32_toUInt8]
861 have hrest : ∀ x, x ≠ e.oc + gSlot e.ls e.R (i + 1) → ca3[x]? = ca[x]? := by
862 intro x hx
863 have hsl : gSlot e.ls e.R (i + 1) = (huff &&& mask).toNat := by
864 unfold gSlot
865 rw [hmask', hgrp, canon_rev_eq]
866 rw [hsl] at hx
867 have hne1 : e.oc + (huff &&& mask).toNat ≠ x := fun h => hx h.symm
868 rw [h3, getElem?_set!_ne hne1, h2, getElem?_set!_ne hne1, h1, getElem?_set!_ne hne1]
869 refine Wp.pure' ⟨ca3, rfl, ⟨hs3, hfr⟩, Or.inl ⟨hex, ⟨hi, hex, hsym, hlen, hhuff, hmask, hcnt, by omega, ?_⟩, ?_, ?_⟩⟩
870 · unfold TabSt
871 dsimp only
872 rw [hused']
873 refine ⟨⟨k + min.toNat, by rw [Nat.add_assoc], by omega⟩, by omega, by omega, by omega, by omega,
874 fun h => by omega, fun _ => ⟨hdrop, hmask', hbb1, hbb2, ?_⟩⟩
875 intro j hj hRj hpj
876 rw [← hcs'] at bb3
877 exact bb3 j hj hRj hpj
878 · -- the descriptor of code i + 1
879 unfold DescIs DescB
880 dsimp only
881 rw [hDn]
882 dsimp only
883 refine ⟨⟨⟨k + min.toNat, by rw [Nat.add_assoc], ?_⟩, ?_, ?_⟩, hdrop, ?_⟩
884 · rw [hkb, hmin, hcurrD]
885 · rw [hwid]
886 · rw [hused', hwid, husedD]
887 · rw [hmask', hgrp, canon_rev_eq]
888 · exact cont_link e i ca ca3 hi hst hlinke hrest hxC
889
890theorem cont_nolink (e : Env) (i : Nat) (ca : Array Code) (hns : ¬ Canon.startsAt e.ls e.R i) :
891 Cont e (i + 1) i ca → Cont e (i + 1) (i + 1) ca := by
892 intro hC hg
893 obtain ⟨hW, hL⟩ := hC hg
894 refine ⟨hW, fun a h1 h2 h3 h4 => ?_⟩
895 by_cases ha : a = i + 1
896 · subst ha; exact absurd (by simpa using h4) hns
897 · exact hL a h1 (by omega) h3 h4
898
899theorem ex_nostart (e : Env) (i : Nat) (s : TS) (ca : Array Code) (hns : ¬ Canon.startsAt e.ls e.R i)
900 (hx : Ex1 e i s ca) : Ex e (i + 1) s ca := by
901 have hD : e.D (i + 1) = e.D i := desc_succ_of_not e.ls e.R e.mx i hns
902 refine ⟨?_, cont_nolink e i ca hns hx.2⟩
903 have := hx.1
904 unfold DescIs DescB at this ⊢
905 rw [hD]; exact this
906
907theorem cond_iff (len root huff mask low : UInt32) :
908 (decide (len > root) && huff &&& mask != low) = true ↔
909 (root.toNat < len.toNat ∧ (huff &&& mask).toNat ≠ low.toNat) := by
910 simp only [Bool.and_eq_true, decide_eq_true_eq, bne_iff_ne, ne_eq, UInt32.lt_iff_toNat_lt, gt_iff_lt]
911 rw [← UInt32.toNat_inj]
912
913theorem jp2_wp (e : Env) (i : Nat) (s : TS) (ca : Array Code) (h : MI2 e i s ca) (hx : Ex1 e i s ca) :
914 Wp (jp2 e.c s) (e.hc ca) (fun s' h' => ∃ ca', h' = e.hc ca' ∧ FrameCA e ca ca' ∧
915 ((s'.exit = 0 ∧ MI e (i + 1) s' ca' ∧ Ex e (i + 1) s' ca') ∨
916 (s'.exit = 2 ∧ e.c.type ≠ CODES ∧ e.oc + e.cap ≤ ca'.size))) := by
917 obtain ⟨hi, hex, hsym, hlen, hhuff, hmask, hcnt, hsz, hTab, hmin⟩ := h
918 have hTab' := hTab
919 obtain ⟨⟨k, hnext, hku⟩, hucap, hu2R, hc1, hc15, hphA, hphB⟩ := hTab'
920 have hmono : e.l i ≤ e.l (i + 1) := lenAt_mono (f := e.f) (n := e.n) (Nat.le_succ i) hi
921 have hroot := e.h_root
922 have hR1 := e.h_R1
923 have hmxle : e.mx ≤ 15 := by
924 have := lenAt_bounds (f := e.f) (n := e.n) (show e.m - 1 < Tc e.f e.n 15 by have := e.h_pos; unfold Env.m; omega)
925 exact this.2
926 have hlmx : e.l (i + 1) ≤ e.mx := lenAt_mono (f := e.f) (n := e.n) (show i + 1 ≤ Tc e.f e.n 15 - 1 by
927 have : i + 1 < e.m := hi
928 unfold Env.m at this; omega) (by have := e.h_pos; omega)
929 have hmask' : (s.huff &&& s.mask).toNat = rev e.R (e.p (i + 1)) ∨ ¬ (e.R ≤ e.l (i + 1)) := by
930 by_cases hle : e.R ≤ e.l (i + 1)
931 · left
932 rw [u32_and_mod (k := e.R) (by rw [hmask]), hhuff]
933 exact huff_low (f := e.f) (n := e.n) (R := e.R) (j := i + 1) hle
934 · right; exact hle
935 unfold jp2
936 by_cases hRl : e.R < e.l (i + 1)
937 · have hmk : (s.huff &&& s.mask).toNat = rev e.R (e.p (i + 1)) := by
938 rcases hmask' with h | h
939 · exact h
940 · omega
941 have hpl : e.p (i + 1) < 2 ^ e.R := pre_lt e.h_fits hi (show e.R ≤ e.l (i + 1) by omega)
942 have hne : e.c.type ≠ CODES := by
943 intro ht
944 have := (e.h_codes ht).2.1
945 have h3 : e.mx = mxl e.f e.n := rfl
946 omega
947 by_cases hAi : e.l i ≤ e.R
948 · -- no table so far: open one
949 obtain ⟨hd0, hlow, hcR, huR⟩ := hphA hAi
950 have hc : (decide (s.len > e.c.root) && s.huff &&& s.mask != s.low) = true := by
951 rw [cond_iff]
952 refine ⟨by omega, ?_⟩
953 rw [hlow, hmk]
954 have := rev_lt e.R (e.p (i + 1))
955 have h15 : 2 ^ e.R ≤ 2 ^ 15 := Nat.pow_le_pow_right (by omega) (by omega)
956 have : (0xffffffff : UInt32).toNat = 4294967295 := rfl
957 omega
958 rw [ite_eq_left hc, ite_eq_left (by simp [hd0])]
959 refine openBody_wp e i _ ca ⟨hi, hex, hsym, hlen, hhuff, hmask, hcnt, hsz, ⟨k, hnext, hku⟩, hucap, hu2R, hc1, hc15, hmin, hRl, hroot,
960 align_succ e.h_fits hi hRl (Or.inl hAi)⟩ ⟨hx.1.1, hx.2⟩
961 ((startsAt_iff e.f e.n e.R hi).mpr ⟨hRl, Or.inl hAi⟩)
962 · have hBi : e.R < e.l i := by omega
963 obtain ⟨hd, hlow, hbb1, hbb2, hblk⟩ := hphB hBi
964 by_cases hpe : e.p (i + 1) = e.p i
965 · -- same prefix: the table stays
966 have hc : ¬ ((decide (s.len > e.c.root) && s.huff &&& s.mask != s.low) = true) := by
967 rw [cond_iff]
968 rintro ⟨_, hh⟩
969 apply hh
970 rw [hlow, hmk, hpe]
971 rw [ite_eq_right hc]
972 have hns : ¬ Canon.startsAt e.ls e.R i := fun h =>
973 ((startsAt_iff e.f e.n e.R hi).mp h).2.elim (fun h' => by have h'' : e.l i ≤ e.R := h'; omega) (fun h' => h' hpe)
974 refine Wp.pure' ⟨ca, rfl, ⟨rfl, fun _ _ => rfl⟩, Or.inl ⟨hex, ⟨hi, hex, hsym, hlen, hhuff, hmask, hcnt, hsz, ?_⟩,
975 ex_nostart e i s ca hns hx⟩⟩
976 refine ⟨⟨k, hnext, hku⟩, hucap, hu2R, hc1, hc15, fun h => by omega, fun _ => ⟨hd, ?_, ?_, hbb2, ?_⟩⟩
977 · rw [hlow, hpe]
978 · exact hblk (i + 1) hi hRl hpe
979 · intro j hj hRj hpj
980 exact hblk j hj hRj (hpj.trans hpe)
981 · -- new prefix
982 have hc : (decide (s.len > e.c.root) && s.huff &&& s.mask != s.low) = true := by
983 rw [cond_iff]
984 refine ⟨by omega, ?_⟩
985 rw [hlow, hmk]
986 intro heq
987 apply hpe
988 have := rev_inj e.R _ _ heq
989 have hpi : e.p i < 2 ^ e.R := pre_lt e.h_fits (show i < Tc e.f e.n 15 by have : i + 1 < e.m := hi; unfold Env.m at this; omega) (show e.R ≤ e.l i by omega)
990 rw [Nat.mod_eq_of_lt hpl, Nat.mod_eq_of_lt hpi] at this
991 exact this
992 have hdne : ¬ ((s.drop == 0) = true) := by
993 simp only [beq_iff_eq]; intro h0; rw [h0] at hd; simp at hd; omega
994 rw [ite_eq_left hc, ite_eq_right hdne]
995 exact openBody_wp e i _ ca ⟨hi, hex, hsym, hlen, hhuff, hmask, hcnt, hsz, ⟨k, hnext, hku⟩, hucap, hu2R, hc1, hc15, hmin, hRl, hd,
996 align_succ e.h_fits hi hRl (Or.inr ⟨hBi, hpe⟩)⟩ ⟨hx.1.1, hx.2⟩
997 ((startsAt_iff e.f e.n e.R hi).mpr ⟨hRl, Or.inr hpe⟩)
998 · -- the code is not longer than the root: no table
999 have hc : ¬ ((decide (s.len > e.c.root) && s.huff &&& s.mask != s.low) = true) := by
1000 rw [cond_iff]; rintro ⟨h1, _⟩; omega
1001 rw [ite_eq_right hc]
1002 have hAi : e.l i ≤ e.R := by omega
1003 obtain ⟨hd0, hlow, hcR, huR⟩ := hphA hAi
1004 have hns : ¬ Canon.startsAt e.ls e.R i := fun h => by
1005 have : e.R < e.l (i + 1) := ((startsAt_iff e.f e.n e.R hi).mp h).1
1006 omega
1007 refine Wp.pure' ⟨ca, rfl, ⟨rfl, fun _ _ => rfl⟩, Or.inl ⟨hex, ⟨hi, hex, hsym, hlen, hhuff, hmask, hcnt, hsz, ?_⟩,
1008 ex_nostart e i s ca hns hx⟩⟩
1009 refine ⟨⟨k, hnext, hku⟩, hucap, hu2R, hc1, hc15, fun _ => ⟨hd0, hlow, hcR, huR⟩, fun h => by omega⟩
1010
1011theorem ws_getD_lt {f : Nat → Nat} {n i : Nat} (hi : i < Tc f n 15) : (wsAux f n 15).getD i 0 < n := by
1012 have hlen' : (wsAux f n 15).length = Tc f n 15 := wsAux_length 15
1013 have hlt' : i < (wsAux f n 15).length := by omega
1014 have hm := List.getElem_mem hlt'
1015 have := (mem_wsAux.mp hm).1
1016 rw [List.getD_eq_getElem?_getD, List.getElem?_eq_getElem hlt', Option.getD_some]
1017 exact this
1018
1019theorem cont_final (e : Env) (i : Nat) (ca : Array Code) (him : i + 1 = e.m) :
1020 Cont e (i + 1) i ca → Cont e e.m e.m ca := by
1021 intro hC hg
1022 obtain ⟨hW, hL⟩ := hC hg
1023 refine ⟨by rw [← him]; exact hW, fun a h1 h2 h3 h4 => hL a h1 (by omega) h3 h4⟩
1024
1025theorem jp1_wp (e : Env) (i : Nat) (s : TS) (ca : Array Code) (h : MI1 e i s ca) (hx : Ex1 e i s ca)
1026 (hinc : i + 1 = e.m → s.huff.toNat ≠ 0 → Einc e s) :
1027 Wp (jp1 e.c s) (e.hc ca) (fun s' h' => ∃ ca', h' = e.hc ca' ∧ FrameCA e ca ca' ∧ StepPostX e i s' ca') := by
1028 obtain ⟨hi, hex, hsym, hlen, hhuff, hhfin, hmask, hcnt, hsz, hTab, hmin⟩ := h
1029 have hmono := fun (hi1 : i + 1 < e.m) => lenAt_mono (f := e.f) (n := e.n) (Nat.le_succ i) hi1
1030 have hi0 : i < Tc e.f e.n 15 := hi
1031 obtain ⟨hb1, hb2⟩ := lenAt_bounds (f := e.f) (n := e.n) hi0
1032 have hblk := (lenAt_eq_iff (f := e.f) (n := e.n) (l := lenAt e.f e.n i) hb1 hb2 hi0).mp rfl
1033 have hm15 : e.m = Tc e.f e.n 15 := rfl
1034 have hmxle : e.mx ≤ 15 := by
1035 have := lenAt_bounds (f := e.f) (n := e.n) (show e.m - 1 < Tc e.f e.n 15 by have := e.h_pos; unfold Env.m; omega)
1036 exact this.2
1037 have hTs := Tc_succ' (f := e.f) (n := e.n) hb1
1038 simp only [Env.l] at hlen hblk hTs
1039 have hlen16 : s.len.toNat < 16 := by rw [hlen]; exact Nat.lt_succ_of_le hb2
1040 have hsz16 : s.len.toNat < s.count.size := by rw [hcnt.1]; exact hlen16
1041 have hcl : (s.count[s.len.toNat]).toNat = Tc e.f e.n (lenAt e.f e.n i) - i := by
1042 have key := hcnt.2 (lenAt e.f e.n i) hb1 hb2
1043 rw [Array.getD_eq_getD_getElem?, show lenAt e.f e.n i = s.len.toNat from hlen.symm, Array.getElem?_eq_getElem hsz16] at key
1044 simp only [Option.getD_some] at key
1045 rw [key, hlen]; unfold rem; omega
1046 have hcl_pos : 1 ≤ (s.count[s.len.toNat]).toNat := by rw [hcl]; omega
1047 have hcl1 : ((s.count[s.len.toNat]) - 1).toNat = (s.count[s.len.toNat]).toNat - 1 := by
1048 rw [UInt16.toNat_sub_of_le _ _ (by simp [UInt16.le_iff_toNat_le]; omega)]; rfl
1049 have hcnt' : ∀ cnt' : Array UInt16, cnt' = s.count.set! s.len.toNat ((s.count[s.len.toNat]) - 1) →
1050 CountOK e cnt' (i + 1) := by
1051 intro cnt' hc'
1052 refine ⟨by rw [hc', Array.size_set!]; exact hcnt.1, fun l hl1 hl2 => ?_⟩
1053 rw [hc', getD_set!, rem_succ hl1 hl2 hi0]
1054 by_cases hl : s.len.toNat = l
1055 · have hli : lenAt e.f e.n i = l := by rw [← hl]; exact hlen.symm
1056 rw [ite_eq_left ⟨hl, hsz16⟩, ite_eq_left hli, hcl1, hcl]
1057 subst hli
1058 unfold rem; omega
1059 · have hli : ¬ (lenAt e.f e.n i = l) := by intro h2; apply hl; rw [hlen]; exact h2
1060 rw [ite_eq_right (fun h2 => hl h2.1), ite_eq_right hli, Nat.sub_zero]
1061 exact hcnt.2 l hl1 hl2
1062 unfold jp1
1063 rcases s with ⟨huff, sym, len, curr, drop, low, used, min, fill, incr, mask, left, next, here, count, exit⟩
1064 dsimp only at *
1065 have hsym' : (sym + 1).toNat = i + 1 := by
1066 have := e.h_n; have : e.m ≤ e.n := Tc_le 15 e.n
1067 rw [u32_succ (by omega), hsym]
1068 apply Wp.bind' (Q := fun r h' => r = count[len.toNat] ∧ h' = e.hc ca) (Wp.pure_eq (geta_eq hsz16) ⟨rfl, rfl⟩)
1069 rintro cl h' ⟨rfl, rfl⟩
1070 try dsimp only
1071 apply Wp.bind' (Q := fun r h' => r = count.set! len.toNat (count[len.toNat] - 1) ∧ h' = e.hc ca)
1072 (Wp.pure_eq (seta_eq hsz16) ⟨rfl, rfl⟩)
1073 rintro cnt' h' ⟨hc', rfl⟩
1074 try dsimp only
1075 have hCO := hcnt' cnt' hc'
1076 have tail : ∀ (s2 : TS), s2.exit = 0 → s2.sym.toNat = i + 1 → s2.len.toNat = e.l (i + 1) → i + 1 < e.m →
1077 s2.huff = huff → s2.mask = mask → s2.count = cnt' → s2.curr = curr → s2.drop = drop → s2.low = low →
1078 s2.used = used → s2.min = min → s2.next = next →
1079 Wp (jp2 e.c s2) (e.hc ca) (fun s' h' => ∃ ca', h' = e.hc ca' ∧ FrameCA e ca ca' ∧ StepPostX e i s' ca') := by
1080 intro s2 h1 h2 h3 h4 h5 h6 h7 h8 h9 h10 h11 h12 h13
1081 have hx2 : Ex1 e i s2 ca := by
1082 refine ⟨?_, hx.2⟩
1083 have := hx.1
1084 unfold DescIs DescB at this ⊢
1085 rw [h13, h8, h11, h9, h10]; exact this
1086 refine Wp.mono (jp2_wp e i s2 ca ?_ hx2) ?_
1087 · refine ⟨h4, h1, h2, h3, ?_, by rw [h6]; exact hmask, by rw [h7]; exact hCO, hsz, ?_, by rw [h12, h8]; exact hmin⟩
1088 · rw [h5]; exact hhuff h4
1089 · obtain ⟨⟨k, hn, hk⟩, r⟩ := hTab
1090 unfold TabSt
1091 rw [h13, h8, h11, h9, h10]
1092 exact ⟨⟨k, hn, hk⟩, r⟩
1093 · rintro s' h' ⟨ca', hh, hf, hr⟩
1094 refine ⟨ca', hh, hf, ?_⟩
1095 rcases hr with ⟨hx', hm, hEx⟩ | ⟨hx', hy, hz⟩
1096 · exact ⟨Or.inl ⟨h4, hm⟩, fun _ _ => hEx, fun h => absurd h (by omega)⟩
1097 · exact ⟨Or.inr (Or.inr ⟨hx', hy, hz⟩), fun _ h => by rw [hx'] at h; exact absurd h (by decide),
1098 fun _ h => by rw [hx'] at h; exact absurd h (by decide)⟩
1099 have hmxeq : (len == e.c.max) = true ↔ lenAt e.f e.n i = e.mx := by
1100 rw [beq_iff_eq, ← UInt32.toNat_inj, e.h_max, hlen]; rfl
1101 have hTle : e.m ≤ e.n := Tc_le 15 e.n
1102 by_cases hz : ((count[len.toNat] - 1 == 0) = true)
1103 · rw [ite_eq_left hz]
1104 have hcl0 : (count[len.toNat] - 1).toNat = 0 := by
1105 have := beq_iff_eq.mp hz
1106 rw [this]; rfl
1107 have hTl : i + 1 = Tc e.f e.n (lenAt e.f e.n i) := by omega
1108 by_cases hmx : (len == e.c.max) = true
1109 · rw [ite_eq_left hmx]
1110 have hlm := hmxeq.mp hmx
1111 have him : i + 1 = e.m := by
1112 have h1 : Tc e.f e.n e.mx = Tc e.f e.n 15 := by
1113 have := Tc_mono (f := e.f) (n := e.n) (show e.mx ≤ 15 from hmxle)
1114 have hh := (lenAt_le_iff (f := e.f) (n := e.n) (l := e.mx) hmxle (show e.m - 1 < Tc e.f e.n 15 by have := e.h_pos; unfold Env.m; omega)).mp (Nat.le_refl _)
1115 omega
1116 rw [hTl, hlm]; exact h1
1117 refine Wp.pure' ⟨ca, rfl, ⟨rfl, fun _ _ => rfl⟩, ⟨Or.inr (Or.inl ⟨him, rfl, ?_, hsz⟩),
1118 fun h _ => absurd h (by omega), fun _ _ => ⟨cont_final e i ca him hx.2, fun hne => hinc him hne⟩⟩⟩
1119 obtain ⟨⟨k, hn, hk⟩, hu, _⟩ := hTab
1120 exact ⟨⟨k, hn, hk⟩, hu, hhfin him⟩
1121 · rw [ite_eq_right hmx]
1122 have hi1 : i + 1 < e.m := by
1123 apply Classical.byContradiction
1124 intro hcon
1125 apply hmx
1126 rw [hmxeq]
1127 have him : i + 1 = e.m := by omega
1128 have : i = Tc e.f e.n 15 - 1 := by have : e.m = Tc e.f e.n 15 := rfl; omega
1129 rw [this]; rfl
1130 have hwlt : e.ow + (i + 1) < e.wa.size := by have := e.h_wa; omega
1131 have hw := e.h_wcont (i + 1) hi1
1132 rw [Array.getElem?_eq_getElem hwlt] at hw
1133 have hw' : e.wa[e.ow + (i + 1)]'hwlt = UInt16.ofNat ((wsAux e.f e.n 15).getD (i + 1) 0) := Option.some.inj hw
1134 have hwsm : (wsAux e.f e.n 15).getD (i + 1) 0 < e.n := ws_getD_lt (by omega)
1135 have hlenx : e.l (i + 1) = e.f ((wsAux e.f e.n 15).getD (i + 1) 0) := rfl
1136 generalize (wsAux e.f e.n 15).getD (i + 1) 0 = x at hw' hwsm hlenx
1137 have hn288 := e.h_n
1138 have hx16 : x < 2 ^ 16 := by omega
1139 have hwn : (UInt16.ofNat x).toNat = x := by
1140 rw [UInt16.toNat_ofNat', Nat.mod_eq_of_lt hx16]
1141 rw [e.h_work, e.h_lens]
1142 apply Wp.bind' (Q := fun r h' => r = e.wa[e.ow + (i + 1)]'hwlt ∧ h' = e.hc ca)
1143 · rw [hsym']; exact Wp.of_eq (Ptr.index_ok (e.get_wa ca) hwlt) ⟨rfl, rfl⟩
1144 · rintro w h' ⟨rfl, rfl⟩
1145 rw [hw']
1146 have hlr : e.ol + (UInt16.ofNat x).toNat < e.la.size := by
1147 rw [hwn]; have := e.h_la; omega
1148 apply Wp.bind' (Q := fun r h' => r = e.la[e.ol + (UInt16.ofNat x).toNat]'hlr ∧ h' = e.hc ca)
1149 · exact Wp.of_eq (Ptr.index_ok (e.get_la ca) hlr) ⟨rfl, rfl⟩
1150 · rintro l h' ⟨rfl, rfl⟩
1151 have hlv : (e.la[e.ol + (UInt16.ofNat x).toNat]'hlr).toNat = e.l (i + 1) := by
1152 have hf := e.h_f x
1153 rw [hlenx, hf, Array.getD_eq_getD_getElem?, Array.getElem?_eq_getElem (show e.ol + x < e.la.size by rw [hwn] at hlr; exact hlr),
1154 Option.getD_some]
1155 simp only [hwn]
1156 have hl32 : (e.la[e.ol + (UInt16.ofNat x).toNat]'hlr).toUInt32.toNat = e.l (i + 1) := by
1157 rw [UInt16.toNat_toUInt32]; exact hlv
1158 exact tail { huff := huff, sym := sym + 1, len := (e.la[e.ol + (UInt16.ofNat x).toNat]'hlr).toUInt32, curr := curr, drop := drop, low := low, used := used, min := min, fill := fill, incr := incr, mask := mask, left := left, next := next, here := here, count := cnt', exit := exit } hex hsym' hl32 hi1 rfl rfl rfl rfl rfl rfl rfl rfl rfl
1159 · rw [ite_eq_right hz]
1160 have hcl2 : 2 ≤ (count[len.toNat]).toNat := by
1161 apply Classical.byContradiction
1162 intro hcon
1163 apply hz
1164 have : (count[len.toNat]).toNat = 1 := by omega
1165 have h1 : count[len.toNat] = 1 := by
1166 apply UInt16.toNat_inj.mp; rw [this]; rfl
1167 rw [h1]; rfl
1168 have hi1 : i + 1 < Tc e.f e.n (lenAt e.f e.n i) := by omega
1169 have hmi1 : i + 1 < e.m := by
1170 have := Tc_mono (f := e.f) (n := e.n) hb2
1171 have : e.m = Tc e.f e.n 15 := rfl
1172 omega
1173 have hl' : e.l (i + 1) = lenAt e.f e.n i := by
1174 have := (lenAt_eq_iff (f := e.f) (n := e.n) (l := lenAt e.f e.n i) hb1 hb2 hmi1).mpr ⟨by omega, hi1⟩
1175 exact this
1176 exact tail { huff := huff, sym := sym + 1, len := len, curr := curr, drop := drop, low := low, used := used, min := min, fill := fill, incr := incr, mask := mask, left := left, next := next, here := here, count := cnt', exit := exit } hex hsym' (by rw [hl']; exact hlen) hmi1 rfl rfl rfl rfl rfl rfl rfl rfl rfl
1177
1178theorem incrLoop_pow (h : Nat) : ∀ e, incrLoop h e = 0 ∨ ∃ e' ≤ e, incrLoop h e = 2 ^ e'
1179 | 0 => by
1180 by_cases hb : h.testBit 0
1181 · left; simp [incrLoop, hb]
1182 · right; exact ⟨0, Nat.le_refl _, by simp [incrLoop, hb]⟩
1183 | e + 1 => by
1184 by_cases hb : h.testBit (e + 1)
1185 · rcases incrLoop_pow h e with h0 | ⟨e', he', h1⟩
1186 · left; simp [incrLoop, hb, h0]
1187 · right; exact ⟨e', by omega, by simp [incrLoop, hb, h1]⟩
1188 · right; exact ⟨e + 1, Nat.le_refl _, by simp [incrLoop, hb]⟩
1189
1190theorem jp0_wp (e : Env) (i : Nat) (s : TS) (ca : Array Code) (h : MI e i s ca) (hEx : Ex e i s ca)
1191 (hhere0 : s.here = e.here i) :
1192 Wp (jp0 e.c s) (e.hc ca) (fun s' h' => ∃ ca', h' = e.hc ca' ∧ FrameCA e ca ca' ∧ StepPostX e i s' ca') := by
1193 obtain ⟨hi, hex, hsym, hlen, hhuff, hmask, hcnt, hsz, hTab⟩ := h
1194 have hTab' := hTab
1195 obtain ⟨⟨k, hnext, hku⟩, hucap, hu2R, hc1, hc15, hphA, hphB⟩ := hTab'
1196 have hi0 : i < Tc e.f e.n 15 := hi
1197 have hbd : 1 ≤ e.l i ∧ e.l i ≤ 15 := lenAt_bounds (f := e.f) (n := e.n) hi0
1198 have hR1 := e.h_R1
1199 have hdb : s.drop.toNat ≤ s.len.toNat ∧ s.len.toNat - s.drop.toNat ≤ s.curr.toNat ∧
1200 1 ≤ s.len.toNat - s.drop.toNat ∧ s.drop.toNat ≤ 15 := by
1201 by_cases hA : e.l i ≤ e.R
1202 · obtain ⟨hd0, _, hcR, _⟩ := hphA hA
1203 rw [hd0]
1204 simp only [UInt32.toNat_zero]
1205 omega
1206 · obtain ⟨hd, _, hbb1, hbb2, _⟩ := hphB (by omega)
1207 omega
1208 obtain ⟨hdn, hbc1, hbc2, hbc3⟩ := hdb
1209 have hb32 : (s.len - s.drop).toNat < 32 := by rw [u32_sub hdn]; omega
1210 have hcurr32 : s.curr.toNat < 32 := by omega
1211 have hmxle : e.mx ≤ 15 := by
1212 have := lenAt_bounds (f := e.f) (n := e.n) (show e.m - 1 < Tc e.f e.n 15 by have := e.h_pos; unfold Env.m; omega)
1213 exact this.2
1214 have hm15 : e.m = Tc e.f e.n 15 := rfl
1215 rcases s with ⟨huff, sym, len, curr, drop, low, used, min, fill, incr, mask, left, next, here, count, exit⟩
1216 dsimp only at *
1217 obtain ⟨hdesc, hcont⟩ := hEx
1218 obtain ⟨⟨⟨k', hk'1, hk'2⟩, hcurrD, husedD⟩, hdropD, hlowD⟩ := hdesc
1219 have hkb : k = (e.D i).base := by
1220 have := Ptr.ref.inj (hnext.symm.trans hk'1)
1221 have : k = k' := by omega
1222 rw [this]; exact hk'2
1223 unfold jp0
1224 apply Wp.bind' (Q := fun r h' => r = 1 <<< (len - drop) ∧ h' = e.hc ca) (Wp.pure_eq (shl32_eq hb32) ⟨rfl, rfl⟩)
1225 rintro incr0 h' ⟨rfl, rfl⟩
1226 apply Wp.bind' (Q := fun r h' => r = 1 <<< curr ∧ h' = e.hc ca) (Wp.pure_eq (shl32_eq hcurr32) ⟨rfl, rfl⟩)
1227 rintro fill0 h' ⟨rfl, rfl⟩
1228 have hS : ((1 : UInt32) <<< (len - drop)).toNat = 2 ^ (len.toNat - drop.toNat) := by rw [u32_shl1 hb32, u32_sub hdn]
1229 have hF : ((1 : UInt32) <<< curr).toNat = 2 ^ curr.toNat := u32_shl1 hcurr32
1230 have hSN : 2 ^ (len.toNat - drop.toNat) * 2 ^ (curr.toNat - (len.toNat - drop.toNat)) = 2 ^ curr.toNat := by
1231 rw [← Nat.pow_add]; congr 1; omega
1232 have hhd : (huff >>> drop).toNat = huff.toNat / 2 ^ drop.toNat := u32_shr (by omega)
1233 have hhdS : huff.toNat / 2 ^ drop.toNat < 2 ^ (len.toNat - drop.toNat) := by
1234 rw [Nat.div_lt_iff_lt_mul (Nat.pow_pos (by omega)), ← Nat.pow_add, show len.toNat - drop.toNat + drop.toNat = len.toNat by omega,
1235 hhuff, hlen]
1236 exact rev_lt _ _
1237 dsimp only
1238 have hN1 : 1 ≤ 2 ^ (curr.toNat - (len.toNat - drop.toNat)) := Nat.pow_pos (by omega)
1239 have hS1 : 1 ≤ 2 ^ (len.toNat - drop.toNat) := Nat.pow_pos (by omega)
1240 apply Wp.bind' (fill_loop e _ ca (2 ^ (len.toNat - drop.toNat)) (2 ^ (curr.toNat - (len.toNat - drop.toNat))) k
1241 (huff.toNat / 2 ^ drop.toNat) hnext hS (by rw [hF, hSN]) hN1 hS1 hhd hhdS (show drop.toNat < 32 by omega)
1242 (by rw [hSN]; omega) hsz)
1243 rintro s2 h' ⟨ca2, rfl, rfl, hs2, hp1, hp2⟩
1244 dsimp only
1245 have hfr : FrameCA e ca ca2 := by
1246 refine ⟨hs2, fun x hx => hp2 x ?_⟩
1247 rintro ⟨q', hq', hxq⟩
1248 have h1 : 2 ^ (len.toNat - drop.toNat) * (q' + 1) ≤ 2 ^ (len.toNat - drop.toNat) * 2 ^ (curr.toNat - (len.toNat - drop.toNat)) :=
1249 Nat.mul_le_mul_left _ hq'
1250 rw [Nat.mul_succ] at h1
1251 rw [hSN] at h1
1252 omega
1253 have hl31 : (len - 1).toNat < 32 := by rw [u32_one_sub (by omega)]; omega
1254 apply Wp.bind' (Q := fun r h' => r = 1 <<< (len - 1) ∧ h' = e.hc ca2) (Wp.pure_eq (shl32_eq hl31) ⟨rfl, rfl⟩)
1255 rintro incr2 h' ⟨rfl, rfl⟩
1256 apply Wp.bind' (incr_loop _ (len.toNat - 1) (by omega)
1257 (by rw [u32_shl1 hl31, u32_one_sub (by omega)]) (e.hc ca2))
1258 rintro s4 h' ⟨rfl, X, rfl, hX⟩
1259 dsimp only at hX ⊢
1260 have hlen1 : len.toNat - 1 = e.l i - 1 := by omega
1261 rw [hlen1] at hX
1262 have hXr : X.toNat = incrLoop (rev (e.l i) (e.v i)) (e.l i - 1) := by rw [hX, hhuff]
1263 -- the continuation, once the new `huff` is known
1264 have mi1 : ∀ hnew : UInt32, (i + 1 < e.m → hnew.toNat = rev (e.l (i + 1)) (e.v (i + 1))) →
1265 (i + 1 = e.m → hnew.toNat = 0 ∨ hnew.toNat < 2 ^ curr.toNat) →
1266 (i + 1 = e.m → hnew.toNat ≠ 0 → Einc e (TS.mk hnew sym len curr drop low used (1 <<< curr) 0 X mask left next here count exit)) →
1267 Wp (jp1 e.c (TS.mk hnew sym len curr drop low used (1 <<< curr) 0 X mask left next here count exit)) (e.hc ca2)
1268 (fun s' h' => ∃ ca', h' = e.hc ca' ∧ FrameCA e ca ca' ∧ StepPostX e i s' ca') := by
1269 intro hnew hA hB hC
1270 refine Wp.mono (jp1_wp e i _ ca2 ?_ ?_ hC) ?_
1271 · refine ⟨hi, hex, hsym, hlen, hA, hB, hmask, hcnt, by omega, hTab, ?_⟩
1272 show ((1 : UInt32) <<< curr).toNat = 2 ^ curr.toNat
1273 exact hF
1274 · refine ⟨⟨⟨⟨k', hk'1, hk'2⟩, hcurrD, husedD⟩, hdropD, hlowD⟩, ?_⟩
1275 have hLd : len.toNat = Canon.L e.ls i := by rw [hlen]; exact (L_eq e.f e.n hi).symm
1276 have hHd : huff.toNat = Canon.H e.ls i := by rw [hhuff]; exact (H_eq e.f e.n hi).symm
1277 refine cont_fill e i ca ca2 hi k (huff.toNat / 2 ^ drop.toNat) (2 ^ (len.toNat - drop.toNat))
1278 (2 ^ (curr.toNat - (len.toNat - drop.toNat))) hkb (by rw [hHd, hdropD]) (by rw [hLd, hdropD])
1279 (by unfold gReps; rw [hLd, hdropD, hcurrD]; rfl) ?_ ?_ hcont
1280 · intro x hx
1281 rw [← hhere0]; exact hp1 x hx
1282 · intro x hx
1283 exact hp2 x hx
1284 · rintro s' h' ⟨ca', hh, hf, hr⟩
1285 exact ⟨ca', hh, hfr.trans hf, hr⟩
1286 have hi1 := e.h_fits
1287 by_cases hXz : X = 0
1288 · have hXz' : (X != 0) = false := by simp [hXz]
1289 rw [ite_eq_right (by simp [hXz])]
1290 refine mi1 0 (fun hlt => ?_) (fun _ => Or.inl rfl) (fun _ h => absurd rfl h)
1291 exfalso
1292 obtain ⟨e', _, hinc, _⟩ := huff_step (f := e.f) (n := e.n) hi1 hlt
1293 have : X.toNat = 0 := by rw [hXz]; rfl
1294 have h3 : X.toNat = 2 ^ e' := hXr.trans hinc
1295 rw [this] at h3
1296 exact absurd h3.symm (Nat.pos_iff_ne_zero.mp (Nat.pow_pos (by omega)))
1297 · rw [ite_eq_left (by simpa using hXz)]
1298 have hXn : X.toNat ≠ 0 := fun h0 => hXz (UInt32.toNat_inj.mp (by rw [h0]; rfl))
1299 obtain ⟨e', he', hXp⟩ : ∃ e', e' ≤ e.l i - 1 ∧ X.toNat = 2 ^ e' := by
1300 rcases incrLoop_pow huff.toNat (e.l i - 1) with h0 | ⟨e', he', h1⟩
1301 · exact absurd (hX.trans h0) hXn
1302 · exact ⟨e', he', hX.trans h1⟩
1303 have hX1 : (X - 1).toNat = 2 ^ e' - 1 := by rw [u32_one_sub hXn, hXp]
1304 have hand : (huff &&& (X - 1)).toNat = huff.toNat % 2 ^ e' := u32_and_mod hX1
1305 have hmodlt : huff.toNat % 2 ^ e' < 2 ^ e' := Nat.mod_lt _ (Nat.pow_pos (by omega))
1306 have hp15 : 2 ^ e' ≤ 2 ^ 15 := Nat.pow_le_pow_right (by omega) (by omega)
1307 have hnewv : ((huff &&& (X - 1)) + X).toNat = huff.toNat % 2 ^ e' + 2 ^ e' := by
1308 have hlt : (huff &&& (X - 1)).toNat + X.toNat < 2 ^ 32 := by rw [hand, hXp]; omega
1309 rw [u32_add hlt, hand, hXp]
1310 have hincl : i + 1 = e.m → e.m = 1 ∧ e.R = 1 ∧ e.l i = 1 ∧ k = 0 ∧ e' = 0 := by
1311 intro him
1312 have hnc : ¬ (Kc e.f e.n 15 = 2 ^ 15) := by
1313 intro hc
1314 have := huff_last (f := e.f) (n := e.n) hc (m := i) (by have : e.m = Tc e.f e.n 15 := rfl; omega)
1315 have h0 : X.toNat = 0 := by rw [hXr]; exact this
1316 exact hXn h0
1317 have hmx1 : mxl e.f e.n = 1 := by
1318 rcases e.h_end with h | h
1319 · exact absurd h hnc
1320 · exact h.1
1321 have hT1 : Tc e.f e.n 15 = 1 := by
1322 rcases e.h_end with h | h
1323 · exact absurd h hnc
1324 · exact h.2.1
1325 have hlm : e.l i ≤ e.mx := lenAt_mono (f := e.f) (n := e.n) (show i ≤ Tc e.f e.n 15 - 1 by omega) (by have := e.h_pos; omega)
1326 have hl1 : e.l i = 1 := by have : e.mx = mxl e.f e.n := rfl; omega
1327 have hAi : e.l i ≤ e.R := by omega
1328 obtain ⟨_, _, hcR, huR⟩ := hphA hAi
1329 have hRR : e.R = 1 := by have := e.h_Rmx; omega
1330 have hk0 : k = 0 := by
1331 have : 2 ^ curr.toNat = 2 ^ e.R := by rw [hcR]
1332 omega
1333 exact ⟨hT1, hRR, hl1, hk0, by omega⟩
1334 refine mi1 _ (fun hlt => ?_) (fun him => ?_) (fun him hne => ?_)
1335 · obtain ⟨e2, _, hinc, hrev⟩ := huff_step (f := e.f) (n := e.n) hi1 hlt
1336 have : 2 ^ e' = 2 ^ e2 := by
1337 rw [← hXp, hXr]
1338 exact hinc
1339 rw [hnewv, this, hhuff]
1340 exact hrev
1341 · right
1342 -- the code is incomplete: its only symbol has length 1
1343 have hnc : ¬ (Kc e.f e.n 15 = 2 ^ 15) := by
1344 intro hc
1345 have := huff_last (f := e.f) (n := e.n) hc (m := i) (by have : e.m = Tc e.f e.n 15 := rfl; omega)
1346 have h0 : X.toNat = 0 := by rw [hXr]; exact this
1347 exact hXn h0
1348 have hmx1 : mxl e.f e.n = 1 := by
1349 rcases e.h_end with h | h
1350 · exact absurd h hnc
1351 · exact h.1
1352 have hlm : e.l i ≤ e.mx := lenAt_mono (f := e.f) (n := e.n) (show i ≤ Tc e.f e.n 15 - 1 by omega) (by have := e.h_pos; omega)
1353 have hl1 : e.l i = 1 := by have : e.mx = mxl e.f e.n := rfl; omega
1354 have hAi : e.l i ≤ e.R := by omega
1355 obtain ⟨_, _, hcR, _⟩ := hphA hAi
1356 rw [hnewv]
1357 have h2 : e' = 0 := by omega
1358 subst h2
1359 have := Nat.mod_lt huff.toNat (Nat.pow_pos (a := 2) (n := 0) (by omega))
1360 have hcpos : 2 ^ 1 ≤ 2 ^ curr.toNat := Nat.pow_le_pow_right (by omega) (by omega)
1361 simp at this
1362 omega
1363 · obtain ⟨hm1, hRR, hl1, hk0, he0⟩ := hincl him
1364 refine ⟨hm1, hRR, ?_, ?_⟩
1365 · show ((huff &&& (X - 1)) + X).toNat = 1
1366 rw [hnewv, he0]; simp [Nat.pow_zero, Nat.mod_one]
1367 · show next = .ref e.rc e.oc
1368 rw [hnext, hk0]; rfl
1369
1370theorem hereTop_wp (e : Env) (i : Nat) (s : TS) (ca : Array Code) (h : MI e i s ca) (hEx : Ex e i s ca) :
1371 Wp (hereTop e.c s) (e.hc ca) (fun s' h' => ∃ ca', h' = e.hc ca' ∧ FrameCA e ca ca' ∧ StepPostX e i s' ca') := by
1372 have hMI := h
1373 have hsym : s.sym.toNat = i := h.2.2.1
1374 have hi : i < e.m := h.1
1375 have hn288 := e.h_n
1376 have hTle : e.m ≤ e.n := Tc_le 15 e.n
1377 have hwlt : e.ow + i < e.wa.size := by have := e.h_wa; omega
1378 have hw := e.h_wcont i hi
1379 rw [Array.getElem?_eq_getElem hwlt] at hw
1380 have hw' : e.wa[e.ow + i]'hwlt = UInt16.ofNat ((wsAux e.f e.n 15).getD i 0) := Option.some.inj hw
1381 have hx : (wsAux e.f e.n 15).getD i 0 < e.n := ws_getD_lt hi
1382 generalize hxd : (wsAux e.f e.n 15).getD i 0 = x at hw' hx
1383 have hbits : (s.len - s.drop).toUInt8 = (Canon.L e.ls i - (e.D i).drop).toUInt8 := by
1384 rw [u32_toUInt8]
1385 have hdr := hEx.1.2.1
1386 have hle : s.drop.toNat ≤ s.len.toNat := by
1387 obtain ⟨_, _, _, hlen', _, _, _, _, hTab⟩ := h
1388 obtain ⟨_, _, _, _, _, hA, hB⟩ := hTab
1389 by_cases hh : e.l i ≤ e.R
1390 · rw [(hA hh).1]; simp
1391 · have := (hB (by omega)).1; omega
1392 rw [u32_sub hle, hdr, h.2.2.2.1]
1393 exact congrArg (fun t => (t - (e.D i).drop).toUInt8) (L_eq e.f e.n hi).symm
1394 have hhereE : e.here i = hereC e.c (UInt16.ofNat x) (s.len - s.drop).toUInt8 := by
1395 unfold Env.here; rw [hxd, hbits]
1396 have hx16 : x < 2 ^ 16 := by omega
1397 have hwn : (UInt16.ofNat x).toNat = x := by rw [UInt16.toNat_ofNat', Nat.mod_eq_of_lt hx16]
1398 have hw32 : (UInt16.ofNat x).toUInt32.toNat = x := by rw [UInt16.toNat_toUInt32, hwn]
1399 -- the table lookups are in range
1400 have hidx : x ≥ e.c.match_.toNat →
1401 x - e.c.match_.toNat < e.c.extra.size ∧ x - e.c.match_.toNat < e.c.base.size := by
1402 intro hge
1403 rcases e.h_type with ht | ht | ht
1404 · obtain ⟨_, _, h3, h4⟩ := e.h_codes ht
1405 have hm : e.c.match_.toNat = 20 := by rw [h4]; rfl
1406 omega
1407 · obtain ⟨h1, h2, h3, h4⟩ := e.h_lens' ht
1408 have hm : e.c.match_.toNat = 257 := by rw [h4]; rfl
1409 have hl1 : lbase.size = 31 := rfl
1410 have hl2 : lext.size = 31 := rfl
1411 rw [h2, h3, hm] at *
1412 omega
1413 · obtain ⟨h1, h2, h3, h4⟩ := e.h_dists ht
1414 have hm : e.c.match_.toNat = 0 := by rw [h4]; rfl
1415 have hl1 : dbase.size = 32 := rfl
1416 have hl2 : dext.size = 32 := rfl
1417 rw [h2, h3, hm] at *
1418 omega
1419 unfold hereTop
1420 dsimp only
1421 rw [e.h_work]
1422 rw [hsym]
1423 apply Wp.bind' (Q := fun r h' => r = e.wa[e.ow + i]'hwlt ∧ h' = e.hc ca)
1424 (Wp.of_eq (Ptr.index_ok (e.get_wa ca) hwlt) ⟨rfl, rfl⟩)
1425 rintro w h' ⟨rfl, rfl⟩
1426 rw [hw']
1427 have rd : Wp (Ptr.index (Ptr.ref e.rw e.ow) (i : Int)) (e.hc ca) (fun r h' => r = e.wa[e.ow + i]'hwlt ∧ h' = e.hc ca) :=
1428 Wp.of_eq (Ptr.index_ok (e.get_wa ca) hwlt) ⟨rfl, rfl⟩
1429 by_cases h1 : (UInt16.ofNat x).toUInt32 + 1 < e.c.match_
1430 · rw [ite_eq_left h1]
1431 try dsimp only
1432 apply Wp.bind' rd
1433 rintro w2 h' ⟨rfl, rfl⟩
1434 rw [hw']
1435 refine jp0_wp e i _ ca hMI hEx ?_
1436 show _ = e.here i
1437 rw [hhereE]; unfold hereC; rw [ite_eq_left h1]
1438 · rw [ite_eq_right h1]
1439 try dsimp only
1440 apply Wp.bind' rd
1441 rintro w2 h' ⟨rfl, rfl⟩
1442 rw [hw']
1443 by_cases h2 : (UInt16.ofNat x).toUInt32 ≥ e.c.match_
1444 · rw [ite_eq_left h2]
1445 have hge : x ≥ e.c.match_.toNat := by
1446 have := UInt32.le_iff_toNat_le.mp h2; rw [hw32] at this; exact this
1447 obtain ⟨hx1, hx2⟩ := hidx hge
1448 have hsb : ((UInt16.ofNat x).toUInt32 - e.c.match_).toNat = x - e.c.match_.toNat := by
1449 rw [u32_sub (by rw [hw32]; exact hge), hw32]
1450 apply Wp.bind' rd
1451 rintro w3 h' ⟨rfl, rfl⟩
1452 rw [hw']
1453 have ga : geta e.c.extra ((UInt16.ofNat x).toUInt32 - e.c.match_).toNat = pure (e.c.extra[x - e.c.match_.toNat]'hx1) := by
1454 rw [hsb]; exact geta_eq hx1
1455 have gb : geta e.c.base ((UInt16.ofNat x).toUInt32 - e.c.match_).toNat = pure (e.c.base[x - e.c.match_.toNat]'hx2) := by
1456 rw [hsb]; exact geta_eq hx2
1457 apply Wp.bind' (Q := fun r h' => r = e.c.extra[x - e.c.match_.toNat]'hx1 ∧ h' = e.hc ca)
1458 (Wp.pure_eq ga ⟨rfl, rfl⟩)
1459 rintro ex h' ⟨rfl, rfl⟩
1460 try dsimp only
1461 apply Wp.bind' rd
1462 rintro w4 h' ⟨rfl, rfl⟩
1463 rw [hw']
1464 apply Wp.bind' (Q := fun r h' => r = e.c.base[x - e.c.match_.toNat]'hx2 ∧ h' = e.hc ca)
1465 (Wp.pure_eq gb ⟨rfl, rfl⟩)
1466 rintro ba h' ⟨rfl, rfl⟩
1467 try dsimp only
1468 refine jp0_wp e i _ ca hMI hEx ?_
1469 show _ = e.here i
1470 rw [hhereE]; unfold hereC; rw [ite_eq_right h1, ite_eq_left h2, hsb]
1471 simp [getElem!_pos, hx1, hx2]
1472 · rw [ite_eq_right h2]
1473 refine jp0_wp e i _ ca hMI hEx ?_
1474 show _ = e.here i
1475 rw [hhereE]; unfold hereC; rw [ite_eq_right h1, ite_eq_right h2]
1476
1477end Zlib.Inftrees.Proofs