inffast.c.base.lean

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

1import ZlibF.Zlib.«inffast.c»
2
3/-!
4# inffast.c: tools for the proofs
5
6A weakest-precondition calculus for the monad `M`, rules for the checked operations of `inffast.c.lean`
7(`shl32`, `shl64`, `shr64`, `subn`, `chk64`), arithmetic of the machine integers, and the frame lemmas for
8`ZStreamRef.put`. Nothing here is part of the specification.
9-/
10
11namespace Zlib.Inffast.Proofs
12open C Zlib.Inffast
13
14/-! ### A weakest-precondition calculus for `M` -/
15
16/-- `m` runs on `h` without a fault and its result satisfies `Q`. -/
17def Wp {α : Type} (m : M α) (h : Heap) (Q : α → Heap → Prop) : Prop :=
18  ∃ a h', m h = .ok (a, h') ∧ Q a h'
19
20theorem Wp.pure' {α : Type} {a : α} {h : Heap} {Q : α → Heap → Prop} (hq : Q a h) : Wp (Pure.pure a : M α) h Q :=
21  ⟨a, h, rfl, hq⟩
22
23theorem Wp.bind' {α β : Type} {m : M α} {f : α → M β} {h : Heap} {Q : α → Heap → Prop} {R : β → Heap → Prop}
24    (hm : Wp m h Q) (hf : ∀ a h', Q a h' → Wp (f a) h' R) : Wp (m >>= f) h R := by
25  obtain ⟨a, h1, e, hq⟩ := hm
26  obtain ⟨b, h2, e2, hr⟩ := hf a h1 hq
27  exact ⟨b, h2, by rw [bind_app, e]; exact e2, hr⟩
28
29/-- A step that does not change the heap. -/
30theorem Wp.bindO {α β : Type} {m : M α} {f : α → M β} {h : Heap} {x : α} {R : β → Heap → Prop}
31    (hm : OkOn h m x) (hf : Wp (f x) h R) : Wp (m >>= f) h R := by
32  obtain ⟨b, h2, e2, hr⟩ := hf
33  exact ⟨b, h2, by rw [bind_app, hm]; exact e2, hr⟩
34
35/-- A step that changes the heap to `h1`. -/
36theorem Wp.bindE {α β : Type} {m : M α} {f : α → M β} {h h1 : Heap} {x : α} {R : β → Heap → Prop}
37    (hm : m h = .ok (x, h1)) (hf : Wp (f x) h1 R) : Wp (m >>= f) h R := by
38  obtain ⟨b, h2, e2, hr⟩ := hf
39  exact ⟨b, h2, by rw [bind_app, hm]; exact e2, hr⟩
40
41theorem Wp.mono {α : Type} {m : M α} {h : Heap} {Q R : α → Heap → Prop} (hm : Wp m h Q)
42    (hr : ∀ a h', Q a h' → R a h') : Wp m h R := by
43  obtain ⟨a, h1, e, hq⟩ := hm
44  exact ⟨a, h1, e, hr a h1 hq⟩
45
46theorem Wp.ite {α : Type} {c : Prop} [Decidable c] {m1 m2 : M α} {h : Heap} {Q : α → Heap → Prop}
47    (h1 : c → Wp m1 h Q) (h2 : ¬ c → Wp m2 h Q) : Wp (if c then m1 else m2) h Q := by
48  by_cases hc : c
49  · simp only [hc, ite_true]; exact h1 hc
50  · simp only [hc, ite_false]; exact h2 hc
51
52theorem Wp.of_eq {α : Type} {m : M α} {h h' : Heap} {a : α} (e : m h = .ok (a, h')) {Q : α → Heap → Prop}
53    (hq : Q a h') : Wp m h Q := ⟨a, h', e, hq⟩
54
55theorem Wp.of_ok {α : Type} {m : M α} {h : Heap} {a : α} (e : OkOn h m a) {Q : α → Heap → Prop}
56    (hq : Q a h) : Wp m h Q := ⟨a, h, e, hq⟩
57
58theorem Wp.cwhile {σ : Type} {cond : σ → M (Bool × σ)} {body : σ → M σ} (Inv : σ → Heap → Prop) (μ : σ → Nat)
59    (Q : σ → Heap → Prop)
60    (hstep : ∀ s h, Inv s h →
61      (∃ s1 h1, cond s h = .ok ((false, s1), h1) ∧ Q s1 h1) ∨
62      (∃ s1 h1 s2 h2, cond s h = .ok ((true, s1), h1) ∧ body s1 h1 = .ok (s2, h2) ∧ Inv s2 h2 ∧ μ s2 < μ s))
63    {s : σ} {h : Heap} (hI : Inv s h) (hfuel : μ s < fuel) :
64    Wp (cwhile cond body s) h Q := by
65  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
66    intro k
67    induction k using Nat.strongRecOn with
68    | _ k ih =>
69      intro n s h hI hμ hn
70      obtain ⟨n, rfl⟩ : ∃ m, n = m + 1 := ⟨n - 1, by omega⟩
71      rcases hstep s h hI with ⟨s1, h1, hc, hq⟩ | ⟨s1, h1, s2, h2, hc, hb, hI2, hlt⟩
72      · exact ⟨s1, h1, by simp [cwhile.go, hc], hq⟩
73      · obtain ⟨s', h', hgo, hq⟩ := ih (μ s2) (by omega) n s2 h2 hI2 (Nat.le_refl _) (by omega)
74        exact ⟨s', h', by simp [cwhile.go, hc, hb, hgo], hq⟩
75  obtain ⟨s', h', e, hq⟩ := key (μ s) fuel s h hI (Nat.le_refl _) hfuel
76  exact ⟨s', h', e, hq⟩
77
78/-- `do ... while` with a measure. `Inv` holds before each body; the measure decreases. -/
79theorem Wp.cdoWhile {σ : Type} {cond : σ → M (Bool × σ)} {body : σ → M σ} (Inv : σ → Heap → Prop) (μ : σ → Nat)
80    (Q : σ → Heap → Prop)
81    (hstep : ∀ s h, Inv s h → ∃ s1 h1, body s h = .ok (s1, h1) ∧
82      ((∃ s2 h2, cond s1 h1 = .ok ((false, s2), h2) ∧ Q s2 h2) ∨
83       (∃ s2 h2, cond s1 h1 = .ok ((true, s2), h2) ∧ Inv s2 h2 ∧ μ s2 < μ s)))
84    {s : σ} {h : Heap} (hI : Inv s h) (hfuel : μ s < fuel) :
85    Wp (cdoWhile body cond s) h Q := by
86  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
87    intro k
88    induction k using Nat.strongRecOn with
89    | _ k ih =>
90      intro n s h hI hμ hn
91      obtain ⟨n, rfl⟩ : ∃ m, n = m + 1 := ⟨n - 1, by omega⟩
92      obtain ⟨s1, h1, hb, hc⟩ := hstep s h hI
93      rcases hc with ⟨s2, h2, hc, hq⟩ | ⟨s2, h2, hc, hI2, hlt⟩
94      · exact ⟨s2, h2, by simp [cdoWhile.go, hb, hc], hq⟩
95      · obtain ⟨s', h', hgo, hq⟩ := ih (μ s2) (by omega) n s2 h2 hI2 (Nat.le_refl _) (by omega)
96        exact ⟨s', h', by simp [cdoWhile.go, hb, hc, hgo], hq⟩
97  obtain ⟨s', h', e, hq⟩ := key (μ s) fuel s h hI (Nat.le_refl _) hfuel
98  exact ⟨s', h', e, hq⟩
99
100/-- `Wp` of a loop in terms of `Wp` of its pieces (the loop rules above take equations; this one takes `Wp`). -/
101theorem Wp.exists_eq {α : Type} {m : M α} {h : Heap} {Q : α → Heap → Prop} (hw : Wp m h Q) :
102    ∃ a h', m h = .ok (a, h') ∧ Q a h' := hw
103
104theorem lt_fuel_of {k : Nat} (h : k < 2 ^ 32) : k < fuel := by
105  unfold fuel
106  exact Nat.lt_of_lt_of_le h (Nat.pow_le_pow_right (by omega) (by omega))
107
108/-! ### The checked operations of `inffast.c.lean` -/
109
110theorem shl32_eq {x n : UInt32} (h : n.toNat < 32) : shl32 x n = pure (x <<< n) := by
111  funext hp; simp [shl32, UInt32.lt_iff_toNat_lt, h]
112
113theorem shl64_eq {x n : UInt64} (h : n.toNat < 64) : shl64 x n = pure (x <<< n) := by
114  funext hp; simp [shl64, UInt64.lt_iff_toNat_lt, h]
115
116theorem shr64_eq {x n : UInt64} (h : n.toNat < 64) : shr64 x n = pure (x >>> n) := by
117  funext hp; simp [shr64, UInt64.lt_iff_toNat_lt, h]
118
119theorem chk64_eq {v : Int} (h1 : -9223372036854775808 ≤ v) (h2 : v ≤ 9223372036854775807) :
120    chk64 v = pure (Int64.ofInt v) := by
121  funext hp; simp [chk64, h1, h2]
122
123theorem M_pure_bind {α β : Type} (a : α) (f : α → M β) : (pure a >>= f : M β) = f a := rfl
124
125theorem subn_ok {h : Heap} {r : BRef} {a : Array UInt8} {off : Nat} {n : UInt32}
126    (hg : Space.get h r = some a) (hn : n.toNat ≤ off) (h1 : off ≤ a.size) :
127    OkOn h (subn (Ptr.ref r off) n) (Ptr.ref r (off - n.toNat)) :=
128  Ptr.sub_nat_ok hg hn h1
129
130/-! ### Machine integers -/
131
132theorem u32_toNat_add {a b : UInt32} (h : a.toNat + b.toNat < 2 ^ 32) : (a + b).toNat = a.toNat + b.toNat := by
133  rw [UInt32.toNat_add]; exact Nat.mod_eq_of_lt h
134
135theorem u32_toNat_sub {a b : UInt32} (h : b.toNat ≤ a.toNat) : (a - b).toNat = a.toNat - b.toNat := by
136  rw [UInt32.toNat_sub]
137  have := UInt32.toNat_lt a
138  have : (2 ^ 32 - b.toNat + a.toNat) = 2 ^ 32 + (a.toNat - b.toNat) := by omega
139  rw [this, Nat.add_mod, Nat.mod_self, Nat.zero_add, Nat.mod_mod]
140  exact Nat.mod_eq_of_lt (by have := UInt32.toNat_lt a; omega)
141
142theorem u64_toNat_add {a b : UInt64} (h : a.toNat + b.toNat < 2 ^ 64) : (a + b).toNat = a.toNat + b.toNat := by
143  rw [UInt64.toNat_add]; exact Nat.mod_eq_of_lt h
144
145theorem u32_shl1 {n : UInt32} (h : n.toNat < 32) : ((1 : UInt32) <<< n).toNat = 2 ^ n.toNat := by
146  rw [UInt32.toNat_shiftLeft, Nat.mod_eq_of_lt h]
147  have : (1 : UInt32).toNat = 1 := rfl
148  rw [this, Nat.shiftLeft_eq, Nat.one_mul]
149  exact Nat.mod_eq_of_lt (Nat.pow_lt_pow_right (by omega) h)
150
151theorem u32_shl1_sub1 {n : UInt32} (h : n.toNat < 32) : (((1 : UInt32) <<< n) - 1).toNat = 2 ^ n.toNat - 1 := by
152  have h1 := u32_shl1 h
153  have hp : 0 < 2 ^ n.toNat := Nat.pow_pos (by omega)
154  rw [u32_toNat_sub (by rw [h1]; exact hp), h1]
155  rfl
156
157theorem u64_shl (x : UInt8) {n : UInt32} (h : n.toNat ≤ 30) :
158    (x.toUInt64 <<< n.toUInt64).toNat = x.toNat * 2 ^ n.toNat := by
159  have hn : n.toUInt64.toNat = n.toNat := UInt32.toNat_toUInt64 n
160  have hm : n.toNat % 64 = n.toNat := Nat.mod_eq_of_lt (by omega)
161  rw [UInt64.toNat_shiftLeft, hn, hm, UInt8.toNat_toUInt64, Nat.shiftLeft_eq]
162  have hx := UInt8.toNat_lt x
163  have : x.toNat * 2 ^ n.toNat < 2 ^ 64 := by
164    calc x.toNat * 2 ^ n.toNat < 2 ^ 8 * 2 ^ n.toNat := Nat.mul_lt_mul_of_pos_right hx (Nat.pow_pos (by omega))
165      _ ≤ 2 ^ 8 * 2 ^ 30 := Nat.mul_le_mul_left _ (Nat.pow_le_pow_right (by omega) h)
166      _ < 2 ^ 64 := by decide
167  exact Nat.mod_eq_of_lt this
168
169theorem u64_shr {x : UInt64} {n : UInt32} (h : n.toNat < 64) : (x >>> n.toUInt64).toNat = x.toNat / 2 ^ n.toNat := by
170  have hn : n.toUInt64.toNat = n.toNat := UInt32.toNat_toUInt64 n
171  rw [UInt64.toNat_shiftRight, hn, Nat.mod_eq_of_lt h, Nat.shiftRight_eq_div_pow]
172
173theorem u64_and_mask {x m : UInt64} {k : Nat} (hm : m.toNat = 2 ^ k - 1) : (x &&& m).toNat = x.toNat % 2 ^ k := by
174  rw [UInt64.toNat_and, hm]; exact Nat.and_two_pow_sub_one_eq_mod _ _
175
176theorem u32_and_mask {x m : UInt32} {k : Nat} (hm : m.toNat = 2 ^ k - 1) : (x &&& m).toNat = x.toNat % 2 ^ k := by
177  rw [UInt32.toNat_and, hm]; exact Nat.and_two_pow_sub_one_eq_mod _ _
178
179theorem u64_toUInt32_mod {x : UInt64} : x.toUInt32.toNat = x.toNat % 2 ^ 32 := UInt64.toNat_toUInt32 x
180
181/-- The low `k` bits of a hold register, as a 32-bit mask operation (`(unsigned)hold & ((1U << k) - 1)`). -/
182theorem hold_low32 {x : UInt64} {k : UInt32} (hk : k.toNat < 32) :
183    (x.toUInt32 &&& (((1 : UInt32) <<< k) - 1)).toNat = x.toNat % 2 ^ k.toNat := by
184  rw [u32_and_mask (k := k.toNat) (u32_shl1_sub1 hk), u64_toUInt32_mod]
185  exact Nat.mod_mod_of_dvd _ (Nat.pow_dvd_pow 2 (by omega))
186
187/-- The same for the 64-bit mask `hold & ((1U << k) - 1)` (the mask is widened to `unsigned long`). -/
188theorem hold_low64 {x : UInt64} {k : UInt32} (hk : k.toNat < 32) :
189    (x &&& ((((1 : UInt32) <<< k) - 1).toUInt64)).toNat = x.toNat % 2 ^ k.toNat := by
190  have : ((((1 : UInt32) <<< k) - 1).toUInt64).toNat = 2 ^ k.toNat - 1 := by
191    rw [UInt32.toNat_toUInt64]; exact u32_shl1_sub1 hk
192  exact u64_and_mask this
193
194end Zlib.Inffast.Proofs