inftrees.c.base.lean

本页保留 Lean 源码及行号。点击行号可定位语句，点击 import 中的模块名可查看依赖。

1import ZlibF.Zlib.«inftrees.c»
2import ZlibF.Proof.«inftrees.c.math»
3
4namespace Zlib.Inftrees.Proofs
5open C Zlib.Inftrees
6
7/-! ### A weakest-precondition calculus for `M` -/
8
9/-- `m` runs on `h` without a fault and its result satisfies `Q`. -/
10def Wp {α : Type} (m : M α) (h : Heap) (Q : α → Heap → Prop) : Prop :=
11  ∃ a h', m h = .ok (a, h') ∧ Q a h'
12
13theorem Wp.pure' {α : Type} {a : α} {h : Heap} {Q : α → Heap → Prop} (hq : Q a h) : Wp (Pure.pure a : M α) h Q :=
14  ⟨a, h, rfl, hq⟩
15
16theorem Wp.bind' {α β : Type} {m : M α} {f : α → M β} {h : Heap} {Q : α → Heap → Prop} {R : β → Heap → Prop}
17    (hm : Wp m h Q) (hf : ∀ a h', Q a h' → Wp (f a) h' R) : Wp (m >>= f) h R := by
18  obtain ⟨a, h1, e, hq⟩ := hm
19  obtain ⟨b, h2, e2, hr⟩ := hf a h1 hq
20  exact ⟨b, h2, by rw [bind_app, e]; exact e2, hr⟩
21
22theorem Wp.mono {α : Type} {m : M α} {h : Heap} {Q R : α → Heap → Prop} (hm : Wp m h Q)
23    (hr : ∀ a h', Q a h' → R a h') : Wp m h R := by
24  obtain ⟨a, h1, e, hq⟩ := hm
25  exact ⟨a, h1, e, hr a h1 hq⟩
26
27theorem Wp.ite {α : Type} {c : Prop} [Decidable c] {m1 m2 : M α} {h : Heap} {Q : α → Heap → Prop}
28    (h1 : c → Wp m1 h Q) (h2 : ¬ c → Wp m2 h Q) : Wp (if c then m1 else m2) h Q := by
29  by_cases hc : c
30  · simp only [hc, ite_true]; exact h1 hc
31  · simp only [hc, ite_false]; exact h2 hc
32
33theorem Wp.of_eq {α : Type} {m : M α} {h h' : Heap} {a : α} (e : m h = .ok (a, h')) {Q : α → Heap → Prop}
34    (hq : Q a h') : Wp m h Q := ⟨a, h', e, hq⟩
35
36/-- Loop with a measure: `Inv` is kept, the measure decreases at each iteration, and `Q` holds when the
37condition fails. -/
38theorem Wp.cwhile {σ : Type} {cond : σ → M (Bool × σ)} {body : σ → M σ} (Inv : σ → Heap → Prop) (μ : σ → Nat)
39    (Q : σ → Heap → Prop)
40    (hstep : ∀ s h, Inv s h →
41      (∃ s1 h1, cond s h = .ok ((false, s1), h1) ∧ Q s1 h1) ∨
42      (∃ s1 h1 s2 h2, cond s h = .ok ((true, s1), h1) ∧ body s1 h1 = .ok (s2, h2) ∧ Inv s2 h2 ∧ μ s2 < μ s))
43    {s : σ} {h : Heap} (hI : Inv s h) (hfuel : μ s < fuel) :
44    Wp (cwhile cond body s) h Q := by
45  have key : ∀ k n s h, Inv s h → μ s ≤ k → k < n → ∃ s' h', cwhile.go cond body n s h = .ok (s', h') ∧ Q s' h' := by
46    intro k
47    induction k using Nat.strongRecOn with
48    | _ k ih =>
49      intro n s h hI hμ hn
50      obtain ⟨n, rfl⟩ : ∃ m, n = m + 1 := ⟨n - 1, by omega⟩
51      rcases hstep s h hI with ⟨s1, h1, hc, hq⟩ | ⟨s1, h1, s2, h2, hc, hb, hI2, hlt⟩
52      · exact ⟨s1, h1, by simp [cwhile.go, hc], hq⟩
53      · obtain ⟨s', h', hgo, hq⟩ := ih (μ s2) (by omega) n s2 h2 hI2 (Nat.le_refl _) (by omega)
54        exact ⟨s', h', by simp [cwhile.go, hc, hb, hgo], hq⟩
55  obtain ⟨s', h', e, hq⟩ := key (μ s) fuel s h hI (Nat.le_refl _) hfuel
56  exact ⟨s', h', e, hq⟩
57
58/-- `do ... while` with a measure: `Inv` holds before each body; the measure decreases. -/
59theorem Wp.cdoWhile {σ : Type} {cond : σ → M (Bool × σ)} {body : σ → M σ} (Inv : σ → Heap → Prop) (μ : σ → Nat)
60    (Q : σ → Heap → Prop)
61    (hstep : ∀ s h, Inv s h → ∃ s1 h1, body s h = .ok (s1, h1) ∧
62      ((∃ s2 h2, cond s1 h1 = .ok ((false, s2), h2) ∧ Q s2 h2) ∨
63       (∃ s2 h2, cond s1 h1 = .ok ((true, s2), h2) ∧ Inv s2 h2 ∧ μ s2 < μ s)))
64    {s : σ} {h : Heap} (hI : Inv s h) (hfuel : μ s < fuel) :
65    Wp (cdoWhile body cond s) h Q := by
66  have key : ∀ k n s h, Inv s h → μ s ≤ k → k < n → ∃ s' h', cdoWhile.go body cond n s h = .ok (s', h') ∧ Q s' h' := by
67    intro k
68    induction k using Nat.strongRecOn with
69    | _ k ih =>
70      intro n s h hI hμ hn
71      obtain ⟨n, rfl⟩ : ∃ m, n = m + 1 := ⟨n - 1, by omega⟩
72      obtain ⟨s1, h1, hb, hc⟩ := hstep s h hI
73      rcases hc with ⟨s2, h2, hc, hq⟩ | ⟨s2, h2, hc, hI2, hlt⟩
74      · exact ⟨s2, h2, by simp [cdoWhile.go, hb, hc], hq⟩
75      · obtain ⟨s', h', hgo, hq⟩ := ih (μ s2) (by omega) n s2 h2 hI2 (Nat.le_refl _) (by omega)
76        exact ⟨s', h', by simp [cdoWhile.go, hb, hc, hgo], hq⟩
77  obtain ⟨s', h', e, hq⟩ := key (μ s) fuel s h hI (Nat.le_refl _) hfuel
78  exact ⟨s', h', e, hq⟩
79
80end Zlib.Inftrees.Proofs
81
82namespace Zlib.Inftrees.Proofs
83open C Zlib.Inftrees
84
85/-! ### The two kinds of array the function writes: the table (`Code`) and `work` (`UInt16`) -/
86
87theorem CodeRef.ro_false_iff {h : Heap} {r : CodeRef} (hro : Space.ro h r = false) : ∃ id, r = CodeRef.istate_codes id := by
88  cases r with
89  | istate_codes id => exact ⟨id, rfl⟩
90  | st_lenfix => simp at hro
91  | st_distfix => simp at hro
92
93/-- Writing the table array does not change any 16-bit word array, and conversely. -/
94theorem wget_put_code (h : Heap) (r : CodeRef) (a : Array Code) (w : WRef) :
95    Space.get (Space.put h r a) w = Space.get h w := by
96  cases r with
97  | istate_codes id =>
98    simp only [Space.put]
99    cases hs : h.istates id with
100    | none => simp
101    | some s =>
102      cases w <;> simp [Space.get, upd_apply, hs] <;> (try split) <;> simp_all
103  | st_lenfix => rfl
104  | st_distfix => rfl
105
106theorem cget_put_word (h : Heap) (w : WRef) (a : Array UInt16) (r : CodeRef) :
107    Space.get (Space.put h w a) r = Space.get h r := by
108  cases r with
109  | istate_codes id =>
110    cases w with
111    | blk b => simp [Space.put, Space.get]
112    | dstate_bl_count d =>
113      simp only [Space.put]
114      cases hs : h.dstates d <;> simp [Space.get, hs]
115    | istate_lens d =>
116      simp only [Space.put]
117      cases hs : h.istates d with
118      | none => simp
119      | some s => simp [Space.get, upd_apply]; split <;> simp_all
120    | istate_work d =>
121      simp only [Space.put]
122      cases hs : h.istates d with
123      | none => simp
124      | some s => simp [Space.get, upd_apply]; split <;> simp_all
125  | st_lenfix => cases w <;> simp [Space.put, Space.get] <;> (try split) <;> simp
126  | st_distfix => cases w <;> simp [Space.put, Space.get] <;> (try split) <;> simp
127
128theorem wput_put (h : Heap) (w : WRef) (a b : Array UInt16) :
129    Space.put (Space.put h w a) w b = Space.put h w b := by
130  cases w with
131  | blk x => simp [Space.put, upd_upd]
132  | dstate_bl_count d =>
133    simp only [Space.put]
134    cases hs : h.dstates d with
135    | none => simp [hs]
136    | some s => simp only [hs, upd_same]; rw [upd_upd]
137  | istate_lens d =>
138    simp only [Space.put]
139    cases hs : h.istates d with
140    | none => simp [hs]
141    | some s => simp only [hs, upd_same]; rw [upd_upd]
142  | istate_work d =>
143    simp only [Space.put]
144    cases hs : h.istates d with
145    | none => simp [hs]
146    | some s => simp only [hs, upd_same]; rw [upd_upd]
147
148theorem wget_put_self {h : Heap} {w : WRef} {a0 : Array UInt16} (hg : Space.get h w = some a0) (b : Array UInt16) :
149    Space.get (Space.put h w b) w = some b := by
150  cases w with
151  | blk x => simp [Space.put, Space.get]
152  | dstate_bl_count d =>
153    simp only [Space.get, Option.map_eq_some_iff] at hg
154    obtain ⟨s, hs, _⟩ := hg
155    simp [Space.put, Space.get, hs, upd_apply]
156  | istate_lens d =>
157    simp only [Space.get, Option.map_eq_some_iff] at hg
158    obtain ⟨s, hs, _⟩ := hg
159    simp [Space.put, Space.get, hs, upd_apply]
160  | istate_work d =>
161    simp only [Space.get, Option.map_eq_some_iff] at hg
162    obtain ⟨s, hs, _⟩ := hg
163    simp [Space.put, Space.get, hs, upd_apply]
164
165theorem wget_put_ne {h : Heap} {w w' : WRef} (hne : w ≠ w') (b : Array UInt16) :
166    Space.get (Space.put h w b) w' = Space.get h w' := by
167  cases w with
168  | blk x =>
169    cases w' with
170    | blk y =>
171      have : x ≠ y := fun e => hne (by rw [e])
172      simp [Space.put, Space.get, upd_apply, this, Ne.symm this]
173    | dstate_bl_count y => simp [Space.put, Space.get]
174    | istate_lens y => simp [Space.put, Space.get]
175    | istate_work y => simp [Space.put, Space.get]
176  | dstate_bl_count x =>
177    cases w' with
178    | blk y => simp only [Space.put]; cases h.dstates x <;> simp [Space.get]
179    | dstate_bl_count y =>
180      have : x ≠ y := fun e => hne (by rw [e])
181      simp only [Space.put]
182      cases hs : h.dstates x with
183      | none => simp [hs]
184      | some s => simp [Space.get, upd_apply, this, Ne.symm this]
185    | istate_lens y => simp only [Space.put]; cases h.dstates x <;> simp [Space.get]
186    | istate_work y => simp only [Space.put]; cases h.dstates x <;> simp [Space.get]
187  | istate_lens x =>
188    cases w' with
189    | blk y => simp only [Space.put]; cases h.istates x <;> simp [Space.get]
190    | dstate_bl_count y => simp only [Space.put]; cases h.istates x <;> simp [Space.get]
191    | istate_lens y =>
192      have : x ≠ y := fun e => hne (by rw [e])
193      simp only [Space.put]
194      cases hs : h.istates x with
195      | none => simp [hs]
196      | some s => simp [Space.get, upd_apply, this, Ne.symm this]
197    | istate_work y =>
198      simp only [Space.put]
199      cases hs : h.istates x with
200      | none => simp [hs]
201      | some s =>
202        by_cases hxy : y = x
203        · subst hxy; simp [Space.get, upd_apply, hs]
204        · simp [Space.get, upd_apply, hxy]
205  | istate_work x =>
206    cases w' with
207    | blk y => simp only [Space.put]; cases h.istates x <;> simp [Space.get]
208    | dstate_bl_count y => simp only [Space.put]; cases h.istates x <;> simp [Space.get]
209    | istate_lens y =>
210      simp only [Space.put]
211      cases hs : h.istates x with
212      | none => simp [hs]
213      | some s =>
214        by_cases hxy : y = x
215        · subst hxy; simp [Space.get, upd_apply, hs]
216        · simp [Space.get, upd_apply, hxy]
217    | istate_work y =>
218      have : x ≠ y := fun e => hne (by rw [e])
219      simp only [Space.put]
220      cases hs : h.istates x with
221      | none => simp [hs]
222      | some s => simp [Space.get, upd_apply, this, Ne.symm this]
223
224theorem cput_put (h : Heap) (r : CodeRef) (a b : Array Code) :
225    Space.put (Space.put h r a) r b = Space.put h r b := by
226  cases r with
227  | istate_codes d =>
228    simp only [Space.put]
229    cases hs : h.istates d with
230    | none => simp [hs]
231    | some s => simp only [hs, upd_same]; rw [upd_upd]
232  | st_lenfix => rfl
233  | st_distfix => rfl
234
235theorem cget_put_self {h : Heap} {r : CodeRef} {a0 : Array Code} (hg : Space.get h r = some a0)
236    (hro : Space.ro h r = false) (b : Array Code) : Space.get (Space.put h r b) r = some b := by
237  obtain ⟨d, rfl⟩ := CodeRef.ro_false_iff hro
238  simp only [Space.get, Option.map_eq_some_iff] at hg
239  obtain ⟨s, hs, _⟩ := hg
240  simp [Space.put, Space.get, hs, upd_apply]
241
242
243/-! ### Machine integers -/
244
245theorem u32_shl1 {n : UInt32} (h : n.toNat < 32) : ((1 : UInt32) <<< n).toNat = 2 ^ n.toNat := by
246  rw [UInt32.toNat_shiftLeft, Nat.mod_eq_of_lt h]
247  have : (1 : UInt32).toNat = 1 := rfl
248  rw [this, Nat.shiftLeft_eq, Nat.one_mul]
249  exact Nat.mod_eq_of_lt (Nat.pow_lt_pow_right (by omega) h)
250
251theorem u32_shr {x n : UInt32} (h : n.toNat < 32) : (x >>> n).toNat = x.toNat / 2 ^ n.toNat := by
252  rw [UInt32.toNat_shiftRight, Nat.mod_eq_of_lt h, Nat.shiftRight_eq_div_pow]
253
254theorem u32_sub {a b : UInt32} (h : b.toNat ≤ a.toNat) : (a - b).toNat = a.toNat - b.toNat := by
255  rw [UInt32.toNat_sub]
256  have := UInt32.toNat_lt a
257  have : (2 ^ 32 - b.toNat + a.toNat) = 2 ^ 32 + (a.toNat - b.toNat) := by omega
258  rw [this, Nat.add_mod, Nat.mod_self, Nat.zero_add, Nat.mod_mod]
259  exact Nat.mod_eq_of_lt (by have := UInt32.toNat_lt a; omega)
260
261theorem u32_add {a b : UInt32} (h : a.toNat + b.toNat < 2 ^ 32) : (a + b).toNat = a.toNat + b.toNat := by
262  rw [UInt32.toNat_add]; exact Nat.mod_eq_of_lt h
263
264theorem u32_and_mod {a m : UInt32} {k : Nat} (hm : m.toNat = 2 ^ k - 1) : (a &&& m).toNat = a.toNat % 2 ^ k := by
265  rw [UInt32.toNat_and, hm]; exact Nat.and_two_pow_sub_one_eq_mod _ _
266
267theorem u32_one_sub {x : UInt32} (hx : x.toNat ≠ 0) : (x - 1).toNat = x.toNat - 1 :=
268  u32_sub (by simp [UInt32.toNat_one]; omega)
269
270theorem u32_ofNat_toNat' (x : UInt32) : UInt32.ofNat x.toNat = x := UInt32.ofNat_toNat
271
272theorem shl32_eq {x n : UInt32} (h : n.toNat < 32) : shl32 x n = pure (x <<< n) := by
273  funext hp; simp [shl32, UInt32.lt_iff_toNat_lt, h]
274
275theorem shr32_eq {x n : UInt32} (h : n.toNat < 32) : shr32 x n = pure (x >>> n) := by
276  funext hp; simp [shr32, UInt32.lt_iff_toNat_lt, h]
277
278theorem geta_eq {a : Array UInt16} {i : Nat} (h : i < a.size) : geta a i = pure a[i] := by
279  funext hp; simp [geta, h]
280
281theorem seta_eq {a : Array UInt16} {i : Nat} {v : UInt16} (h : i < a.size) : seta a i v = pure (a.set! i v) := by
282  funext hp; simp [seta, h]
283
284theorem chk32_eq {v : Int} (h1 : -2147483648 ≤ v) (h2 : v ≤ 2147483647) : chk32 v = pure (Int32.ofInt v) := by
285  funext hp; simp [chk32, h1, h2]
286
287theorem shl1i32_eq {n : UInt32} (h : n.toNat < 31) : shl1i32 n = pure (1 <<< n.toInt32) := by
288  funext hp; simp [shl1i32, UInt32.lt_iff_toNat_lt, h]
289
290theorem shl1i32_toInt {n : UInt32} (h : n.toNat < 31) : ((1 : Int32) <<< n.toInt32).toInt = 2 ^ n.toNat := by
291  have key : ∀ k : Fin 31, ((1 : Int32) <<< (UInt32.ofNat k.val).toInt32).toInt = 2 ^ k.val := by decide
292  have := key ⟨n.toNat, h⟩
293  simpa [u32_ofNat_toNat'] using this
294
295theorem M_pure_bind {α β : Type} (a : α) (f : α → M β) : (pure a >>= f : M β) = f a := rfl
296
297theorem getD_set! {a : Array UInt16} {i j : Nat} {v : UInt16} :
298    (a.set! i v).getD j 0 = if i = j ∧ i < a.size then v else a.getD j 0 := by
299  rw [Array.set!_eq_setIfInBounds, Array.getD_eq_getD_getElem?, Array.getD_eq_getD_getElem?,
300    Array.getElem?_setIfInBounds]
301  by_cases h1 : i = j
302  · subst h1
303    by_cases h2 : i < a.size
304    · simp [h2]
305    · simp [h2, Array.getElem?_eq_none (show a.size ≤ i by omega)]
306  · simp [h1]
307
308theorem u16_succ {a : Nat} (h : a + 1 < 65536) : UInt16.ofNat a + 1 = UInt16.ofNat (a + 1) := by
309  apply UInt16.toNat_inj.mp
310  have e1 : (UInt16.ofNat a).toNat = a := by simp [UInt16.toNat_ofNat', Nat.mod_eq_of_lt (show a < 2 ^ 16 by omega)]
311  have e2 : (UInt16.ofNat (a + 1)).toNat = a + 1 := by simp [UInt16.toNat_ofNat', Nat.mod_eq_of_lt (show a + 1 < 2 ^ 16 by omega)]
312  rw [UInt16.toNat_add, e1, e2]
313  have : (1 : UInt16).toNat = 1 := rfl
314  rw [this]
315  exact Nat.mod_eq_of_lt (by omega)
316
317theorem lt_fuel {k : Nat} (h : k < 2 ^ 32) : k < fuel := by
318  unfold fuel
319  exact Nat.lt_of_lt_of_le h (Nat.pow_le_pow_right (by omega) (by omega))
320
321/-! ### The loop body of `inflate_table`, cut at its join points
322
323The translation (`buildStep`) is one function; the compiler cuts it at the places where the C control flow joins.
324These definitions are those pieces; `buildStep_eq` says that they are the same function. -/
325
326
327/-- The opening of a sub-table (the body of the `if` at the end of the loop body), followed by `pure s`. -/
328def openBody (c : Ctx) (s : TS) : M TS := do
329  let mut s := s
330  s := { s with next := ← s.next.add s.min.toNat }
331  s := { s with curr := s.len - s.drop }
332  s := { s with left := ← shl1i32 s.curr }
333  let (curr, left, _) ← cwhile
334    (fun (curr, left, brk) => pure (!brk && curr + s.drop < c.max, (curr, left, brk)))
335    (fun (curr, left, brk) => do
336      let cc ← geta s.count (curr + s.drop).toNat
337      let left ← chk32 (left.toInt - cc.toNat)
338      if left ≤ 0 then pure (curr, left, true)
339      else
340        let curr := curr + 1
341        let left ← chk32 (left.toInt * 2)
342        pure (curr, left, brk))
343    (s.curr, s.left, false)
344  s := { s with curr, left }
345  let u ← shl32 1 s.curr
346  s := { s with used := s.used + u }
347  if tooBig c.type s.used then
348    return { s with exit := 2 }
349  s := { s with low := s.huff &&& s.mask }
350  let q ← c.table.add s.low.toNat
351  let e ← q.load
352  q.store { e with op := s.curr.toUInt8 }
353  let q ← c.table.add s.low.toNat
354  let e ← q.load
355  q.store { e with bits := c.root.toUInt8 }
356  let d ← s.next.diff c.table
357  let q ← c.table.add s.low.toNat
358  let e ← q.load
359  q.store { e with val := d.toUInt64.toUInt16 }
360  pure s
361
362/-- The test for a new sub-table (after `len` is updated). -/
363def jp2 (c : Ctx) (s : TS) : M TS :=
364  if (decide (s.len > c.root) && s.huff &&& s.mask != s.low) = true then
365    (if (s.drop == 0) = true then openBody c { s with drop := c.root } else openBody c s)
366  else pure s
367
368/-- From `sym++` on. -/
369def jp1 (c : Ctx) (s : TS) : M TS := do
370  let mut s := s
371  s := { s with sym := s.sym + 1 }
372  let cl ← geta s.count s.len.toNat
373  let cl := cl - 1
374  s := { s with count := ← seta s.count s.len.toNat cl }
375  if cl == 0 then
376    if s.len == c.max then
377      return { s with exit := 1 }
378    let w ← c.work.index s.sym.toNat
379    let l ← c.lens.index w.toNat
380    jp2 c { s with len := l.toUInt32 }
381  else jp2 c s
382
383/-- From the computation of `incr` and `fill` on. -/
384def jp0 (c : Ctx) (s : TS) : M TS := do
385  let mut s := s
386  let incr ← shl32 1 (s.len - s.drop)
387  let fill ← shl32 1 s.curr
388  s := { s with incr, fill, min := fill }
389  s ← cdoWhile
390    (fun s => do
391      let fill := s.fill - s.incr
392      let hd ← shr32 s.huff s.drop
393      storeCode s.next (hd + fill).toNat s.here
394      pure { s with fill })
395    (fun s => pure (s.fill != 0, s)) s
396  let incr ← shl32 1 (s.len - 1)
397  s := { s with incr }
398  s ← cwhile (fun s => pure (s.huff &&& s.incr != 0, s)) (fun s => pure { s with incr := s.incr >>> 1 }) s
399  if s.incr != 0 then
400    jp1 c { s with huff := (s.huff &&& (s.incr - 1)) + s.incr }
401  else jp1 c { s with huff := 0 }
402
403/-- The loop body of `inflate_table`. -/
404def hereTop (c : Ctx) (s : TS) : M TS := do
405  let mut s := s
406  s := { s with here := { s.here with bits := (s.len - s.drop).toUInt8 } }
407  let w ← c.work.index s.sym.toNat
408  if w.toUInt32 + 1 < c.match_ then
409    s := { s with here := { s.here with op := 0 } }
410    let w ← c.work.index s.sym.toNat
411    s := { s with here := { s.here with val := w } }
412    jp0 c s
413  else
414    let w ← c.work.index s.sym.toNat
415    if w.toUInt32 ≥ c.match_ then
416      let w ← c.work.index s.sym.toNat
417      let e ← geta c.extra (w.toUInt32 - c.match_).toNat
418      s := { s with here := { s.here with op := e.toUInt8 } }
419      let w ← c.work.index s.sym.toNat
420      let b ← geta c.base (w.toUInt32 - c.match_).toNat
421      s := { s with here := { s.here with val := b } }
422      jp0 c s
423    else
424      s := { s with here := { s.here with op := 96, val := 0 } }
425      jp0 c s
426
427theorem buildStep_eq (c : Ctx) (s : TS) : buildStep c s = hereTop c s := rfl
428
429end Zlib.Inftrees.Proofs