inflate.c.window.lean

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

1import ZlibF.Proof.«inflate.c.misc2»
2import ZlibF.Proof.«pointer-arithmetic»
3
4/-!
5# inflate.c: the ring buffer of `updatewindow`
6
7The copy lemmas establish the two ring-buffer branches for `wbits ≤ 15`.
8Pointer arithmetic uses the checked rules in `ZlibF.Proof.PointerArithmetic`.
9-/
10
11namespace Zlib.Inflate.Proofs.W
12open C ZlibF.Proof
13
14
15/-- `if (state->wsize == 0) { wsize = 1U << wbits; wnext = 0; whave = 0; }` -/
16def initWin (st : InflateState) : InflateState :=
17  if st.wsize == 0 then { st with wsize := (1 : UInt32) <<< st.wbits, wnext := 0, whave := 0 } else st
18
19/-- `if (copy >= wsize)`: copy the last `wsize` bytes before `end` into the whole window. -/
20def uw_big (ist : InflateStatePtr) (st : InflateState) (e : BPtr) : M UInt32 := do
21  let src ← PointerArithmetic.subNat e st.wsize.toNat
22  memcpyB st.window src st.wsize.toNat
23  stInflateState ist { st with wnext := 0, whave := st.wsize }
24  return 0
25
26/-- `else`: copy `copy` bytes into the ring buffer, in at most two pieces. -/
27def uw_small (ist : InflateStatePtr) (st : InflateState) (e : BPtr) (copy : UInt32) : M UInt32 := do
28  let dist : UInt32 := if st.wsize - st.wnext > copy then copy else st.wsize - st.wnext
29  let dst ← PointerArithmetic.addNat st.window st.wnext.toNat
30  let src ← PointerArithmetic.subNat e copy.toNat
31  memcpyB dst src dist.toNat
32  let copy' : UInt32 := copy - dist
33  if copy' != 0 then
34    let src2 ← PointerArithmetic.subNat e copy'.toNat
35    memcpyB st.window src2 copy'.toNat
36    stInflateState ist { st with wnext := copy', whave := st.wsize }
37    return 0
38  else
39    let wn : UInt32 := st.wnext + dist
40    let wn : UInt32 := if wn == st.wsize then 0 else wn
41    let wh : UInt32 := if st.whave < st.wsize then st.whave + dist else st.whave
42    stInflateState ist { st with wnext := wn, whave := wh }
43    return 0
44
45/-- The part of `updatewindow(strm, end, copy)` after the window has been allocated. -/
46def update2 (sr : Nat) (e : BPtr) (copy : UInt32) : M UInt32 := do
47  let z ← ldZStream (some (.tab sr))
48  let ist ← castInflateState z.state
49  let st0 ← ldInflateState ist
50  let st := initWin st0
51  if copy ≥ st.wsize then uw_big ist st e else uw_small ist st e copy
52
53/-- The window invariant W of `docs/proof/inflate.md`: the window is a writable byte block of `2^wbits` bytes. -/
54structure WInv (h : Heap) (st : InflateState) : Prop where
55  k : st.wbits.toNat ≤ 15
56  win : ∃ w a, st.window = .ref (.blk w) 0 ∧ h.bytes w = some a ∧ h.ro w = false ∧ a.size = 2 ^ st.wbits.toNat
57  ws : st.wsize.toNat = 0 ∨ st.wsize.toNat = 2 ^ st.wbits.toNat
58  hv : st.whave.toNat ≤ st.wsize.toNat
59  wn : st.wnext.toNat < st.wsize.toNat ∨ (st.wsize.toNat = 0 ∧ st.wnext.toNat = 0)
60  eq : st.whave.toNat < st.wsize.toNat → st.wnext.toNat = st.whave.toNat
61
62theorem shl_toNat (b : UInt32) (hb : b.toNat ≤ 15) : ((1 : UInt32) <<< b).toNat = 2 ^ b.toNat := by
63  have h15 : 2 ^ b.toNat ≤ 2 ^ 15 := Nat.pow_le_pow_right (by decide) hb
64  have e32 : b.toNat % 32 = b.toNat := Nat.mod_eq_of_lt (by omega)
65  rw [UInt32.toNat_shiftLeft, e32]
66  simp [Nat.shiftLeft_eq]
67  omega
68
69/-- After `initWin` the window is in use and the invariant still holds. -/
70theorem initWin_inv {h : Heap} {st : InflateState} (hW : WInv h st) :
71    WInv h (initWin st) ∧ 0 < (initWin st).wsize.toNat ∧ (initWin st).window = st.window ∧
72    (initWin st).wbits = st.wbits := by
73  obtain ⟨hk2, ⟨w, a, hw, ha, hro, hasz⟩, hws, hv, hwn, heq⟩ := hW
74  have hpow : ((1 : UInt32) <<< st.wbits).toNat = 2 ^ st.wbits.toNat := shl_toNat _ hk2
75  have hp : 0 < 2 ^ st.wbits.toNat := Nat.two_pow_pos _
76  unfold initWin
77  by_cases h0 : st.wsize == 0
78  · have h0' : st.wsize = 0 := by simpa using h0
79    have h00 : st.wsize.toNat = 0 := by rw [h0']; rfl
80    simp only [h0, ite_true]
81    refine ⟨⟨hk2, ⟨w, a, hw, ha, hro, hasz⟩, ?_, ?_, ?_, ?_⟩, ?_, ?_, ?_⟩ <;> simp [hpow, hp]
82  · have h0' : ¬ st.wsize = 0 := by simpa using h0
83    have h00 : st.wsize.toNat ≠ 0 := fun h => h0' (UInt32.toNat_inj.mp (by simpa using h))
84    have h0'' : (st.wsize == 0) = false := by simpa using h0
85    simp only [h0'', Bool.false_eq_true, ite_false]
86    refine ⟨⟨hk2, ⟨w, a, hw, ha, hro, hasz⟩, hws, hv, hwn, heq⟩, by omega, ?_⟩
87    simp
88
89/-- `zmemcpy(w + d, e - n, m)` on a window block `w` and a different block `eb`, then the rest `k`: the heap with the
90window block replaced by a block of the same size. -/
91theorem cpy_step {h : Heap} {w eb : Nat} {a ebytes : Array UInt8} {eo n m d : Nat}
92    (ha : h.bytes w = some a) (hro : h.ro w = false) (heb : h.bytes eb = some ebytes) (hne : w ≠ eb)
93    (hn : n ≤ eo) (hm : m ≤ n) (hoff : eo ≤ ebytes.size) (hd : d + m ≤ a.size) :
94    ∃ A, (∀ {α : Type} (k : Unit → M α),
95        (PointerArithmetic.subNat (.ref (.blk eb) eo) n >>= fun src => (memcpyB (.ref (.blk w) d) src m >>= k)) h =
96          k () { h with bytes := upd h.bytes w (some A) }) ∧ A.size = a.size := by
97  refine ⟨copyRange a ebytes d (eo - n) m, ?_, size_copyRange ..⟩
98  intro α k
99  have h2 : eo - n + m ≤ ebytes.size := by omega
100  simp only [bind_app, PointerArithmetic.subNat_ok (r := BRef.blk eb) (by simpa using heb) hn hoff]
101  simp only [bind_app, memcpyB_blk_ok ha heb hro hne hd h2]
102
103/-- `zmemcpy(w + d, e - n, m)` where `w + d` is computed first (the first copy of `uw_small`). -/
104theorem cpy_step_off {h : Heap} {w eb : Nat} {a ebytes : Array UInt8} {eo n m d : Nat}
105    (ha : h.bytes w = some a) (hro : h.ro w = false) (heb : h.bytes eb = some ebytes) (hne : w ≠ eb)
106    (hn : n ≤ eo) (hm : m ≤ n) (hoff : eo ≤ ebytes.size) (hd : d + m ≤ a.size) (hda : d ≤ a.size) :
107    ∃ A, (∀ {α : Type} (k : Unit → M α),
108        (PointerArithmetic.addNat (.ref (.blk w) 0) d >>= fun dst => (PointerArithmetic.subNat (.ref (.blk eb) eo) n >>= fun src =>
109          (memcpyB dst src m >>= k))) h = k () { h with bytes := upd h.bytes w (some A) }) ∧ A.size = a.size := by
110  obtain ⟨A, hA, hs⟩ := cpy_step (d := 0 + d) ha hro heb hne hn hm hoff (by omega)
111  refine ⟨A, fun {α} k => ?_, hs⟩
112  rw [bind_ok (PointerArithmetic.addNat_ok (r := BRef.blk w) (a := a) (off := 0) (n := d) (by simpa using ha) (by omega))]
113  exact hA k
114
115/-- The tables other than `bytes` and `istates` are unchanged, and so are the read-only flags and the block counter. -/
116def Same (h h' : Heap) : Prop :=
117  h'.words = h.words ∧ h'.dstates = h.dstates ∧ h'.gzheaders = h.gzheaders ∧ h'.gzstates = h.gzstates ∧
118    h'.streams = h.streams ∧ h'.ro = h.ro ∧ h'.nextBlk = h.nextBlk
119
120/-- What the two branches of `updatewindow` establish. -/
121def UwPost (h h' : Heap) (zs w : Nat) (st' : InflateState) : Prop :=
122  h'.istates zs = some st' ∧ WInv h' st' ∧ (∀ r, r ≠ zs → h'.istates r = h.istates r) ∧
123    Same h h' ∧ (∀ b, b ≠ w → h'.bytes b = h.bytes b) ∧ st'.window = .ref (.blk w) 0
124
125/-- The branch `copy ≥ wsize` of `updatewindow` never faults and establishes the window invariant. -/
126theorem uw_big_ok {h : Heap} {zs w eb eo : Nat} {st : InflateState} {ebytes : Array UInt8}
127    (hW : WInv h st) (hw : st.window = .ref (.blk w) 0) (hpos : 0 < st.wsize.toNat)
128    (hex : ∃ s, h.istates zs = some s) (heb : h.bytes eb = some ebytes) (hne : w ≠ eb)
129    (hc : st.wsize.toNat ≤ eo) (hoff : eo ≤ ebytes.size) :
130    ∃ h' st', uw_big (some (.tab zs)) st (.ref (.blk eb) eo) h = .ok (0, h') ∧ UwPost h h' zs w st' := by
131  obtain ⟨hk2, ⟨w', a, hw', ha, hro, hasz⟩, hws, hv, hwn, heq⟩ := hW
132  have hww : w' = w := by rw [hw] at hw'; exact (Ptr.ref.inj hw').1 |> BRef.blk.inj |>.symm
133  subst hww
134  have hsz : st.wsize.toNat = 2 ^ st.wbits.toNat := by omega
135  obtain ⟨A, hstep, hAsz⟩ :=
136    cpy_step (h := h) (w := w') (eb := eb) (a := a) (ebytes := ebytes) (eo := eo) (n := st.wsize.toNat)
137      (m := st.wsize.toNat) (d := 0) ha hro heb hne hc (Nat.le_refl _) hoff (by omega)
138  obtain ⟨s0, hs0⟩ := hex
139  have hs0' : ({ h with bytes := upd h.bytes w' (some A) } : Heap).istates zs = some s0 := hs0
140  refine ⟨{ { h with bytes := upd h.bytes w' (some A) } with
141      istates := upd h.istates zs (some { st with wnext := 0, whave := st.wsize }) },
142    { st with wnext := 0, whave := st.wsize }, ?_, ?_⟩
143  · simp only [uw_big, hw, hstep, bind_app, stInflateState_tab hs0', pure_app]
144  · refine ⟨by simp, ⟨hk2, ⟨w', A, hw, by simp, by simpa using hro, hAsz.trans hasz⟩, hws, ?_, ?_, ?_⟩,
145      fun r hr => by simp [upd_ne _ _ _ _ hr], ⟨rfl, rfl, rfl, rfl, rfl, rfl, rfl⟩,
146      fun b hb => by simp [upd_ne _ _ _ _ hb], hw⟩
147    · show st.wsize.toNat ≤ st.wsize.toNat
148      exact Nat.le_refl _
149    · exact Or.inl (by show 0 < st.wsize.toNat; exact hpos)
150    · intro hh; exact absurd hh (Nat.lt_irrefl _)
151
152theorem uadd (a b : UInt32) (h : a.toNat + b.toNat < 2 ^ 32) : (a + b).toNat = a.toNat + b.toNat := by
153  rw [UInt32.toNat_add]; exact Nat.mod_eq_of_lt h
154
155/-- The branch `copy < wsize` of `updatewindow` (one or two pieces) never faults and keeps the window invariant. -/
156theorem uw_small_ok {h : Heap} {zs w eb eo : Nat} {st : InflateState} {copy : UInt32} {ebytes : Array UInt8}
157    (hW : WInv h st) (hw : st.window = .ref (.blk w) 0) (hpos : 0 < st.wsize.toNat)
158    (hex : ∃ s, h.istates zs = some s) (heb : h.bytes eb = some ebytes) (hne : w ≠ eb)
159    (hc : copy.toNat ≤ eo) (hlt : copy.toNat < st.wsize.toNat) (hoff : eo ≤ ebytes.size) :
160    ∃ h' st', uw_small (some (.tab zs)) st (.ref (.blk eb) eo) copy h = .ok (0, h') ∧ UwPost h h' zs w st' := by
161  obtain ⟨hk2, ⟨w', a, hw', ha, hro, hasz⟩, hws, hv, hwn, heq⟩ := hW
162  have hww : w' = w := by rw [hw] at hw'; exact (BRef.blk.inj (Ptr.ref.inj hw').1).symm
163  subst hww
164  have hsz : st.wsize.toNat = 2 ^ st.wbits.toNat := by omega
165  have hwn' : st.wnext.toNat < st.wsize.toNat := by omega
166  have h15 : 2 ^ st.wbits.toNat ≤ 2 ^ 15 := Nat.pow_le_pow_right (by decide) hk2
167  obtain ⟨dist, hdist⟩ : ∃ d : UInt32, d = (if st.wsize - st.wnext > copy then copy else st.wsize - st.wnext) := ⟨_, rfl⟩
168  have hsub : (st.wsize - st.wnext).toNat = st.wsize.toNat - st.wnext.toNat :=
169    UInt32.toNat_sub_of_le _ _ (by rw [UInt32.le_iff_toNat_le]; omega)
170  have hdn : (dist.toNat = copy.toNat ∧ copy.toNat < st.wsize.toNat - st.wnext.toNat) ∨
171      (dist.toNat = st.wsize.toNat - st.wnext.toNat ∧ ¬ copy.toNat < st.wsize.toNat - st.wnext.toNat) := by
172    rw [hdist]
173    by_cases hc' : st.wsize - st.wnext > copy
174    · left; rw [ite_eq_left hc']; have := UInt32.lt_iff_toNat_lt.mp hc'; omega
175    · right; rw [ite_eq_right hc']; refine ⟨hsub, fun hh => hc' (UInt32.lt_iff_toNat_lt.mpr (by omega))⟩
176  have hd1 : dist.toNat ≤ copy.toNat := by omega
177  have hd2 : dist.toNat ≤ st.wsize.toNat - st.wnext.toNat := by omega
178  obtain ⟨A1, hstep1, hA1sz⟩ :=
179    cpy_step_off (h := h) (w := w') (eb := eb) (a := a) (ebytes := ebytes) (eo := eo) (n := copy.toNat) (m := dist.toNat)
180      (d := st.wnext.toNat) ha hro heb hne hc hd1 hoff (by omega) (by omega)
181  obtain ⟨s0, hs0⟩ := hex
182  have hcsub : (copy - dist).toNat = copy.toNat - dist.toNat := UInt32.toNat_sub_of_le _ _ (by rw [UInt32.le_iff_toNat_le]; omega)
183  by_cases hcp : (copy - dist != 0) = true
184  · -- the window wraps: a second piece goes to the start
185    have hcn : 0 < (copy - dist).toNat := by
186      have : copy - dist ≠ 0 := by simpa using hcp
187      have h0 : (copy - dist).toNat ≠ 0 := fun hh => this (UInt32.toNat_inj.mp (by simpa using hh))
188      omega
189    obtain ⟨A2, hstep2, hA2sz⟩ :=
190      cpy_step (h := { h with bytes := upd h.bytes w' (some A1) }) (w := w') (eb := eb) (a := A1) (ebytes := ebytes)
191        (eo := eo) (n := (copy - dist).toNat) (m := (copy - dist).toNat) (d := 0) (by simp) (by simpa using hro)
192        (by simp [upd_ne _ _ _ _ hne.symm, heb]) hne (by omega) (Nat.le_refl _) hoff (by omega)
193    have hs0' : ({ { h with bytes := upd h.bytes w' (some A1) } with
194        bytes := upd (upd h.bytes w' (some A1)) w' (some A2) } : Heap).istates zs = some s0 := hs0
195    refine ⟨{ { { h with bytes := upd h.bytes w' (some A1) } with
196        bytes := upd (upd h.bytes w' (some A1)) w' (some A2) } with
197        istates := upd h.istates zs (some { st with wnext := copy - dist, whave := st.wsize }) },
198      { st with wnext := copy - dist, whave := st.wsize }, ?_, ?_⟩
199    · simp only [uw_small, hw, ← hdist, hstep1, hcp, ite_true, hstep2]
200      simp only [bind_app, stInflateState_tab hs0', pure_app]
201    · refine ⟨by simp, ⟨hk2, ⟨w', A2, hw, by simp, by simpa using hro, by show A2.size = 2 ^ st.wbits.toNat; omega⟩,
202          hws, ?_, ?_, ?_⟩,
203        fun r hr => by simp [upd_ne _ _ _ _ hr], ⟨rfl, rfl, rfl, rfl, rfl, rfl, rfl⟩,
204        fun b hb => by simp [upd_ne _ _ _ _ hb], hw⟩
205      · show st.wsize.toNat ≤ st.wsize.toNat
206        exact Nat.le_refl _
207      · exact Or.inl (by show (copy - dist).toNat < st.wsize.toNat; omega)
208      · intro hh; exact absurd hh (Nat.lt_irrefl _)
209  · -- everything fits before the end of the window
210    have hcp' : (copy - dist != 0) = false := by simpa using hcp
211    have hc0 : copy.toNat = dist.toNat := by
212      have : copy - dist = 0 := by simpa using hcp'
213      have : (copy - dist).toNat = 0 := by rw [this]; rfl
214      omega
215    have hwd : st.wnext.toNat + dist.toNat ≤ st.wsize.toNat := by omega
216    have hadd : (st.wnext + dist).toNat = st.wnext.toNat + dist.toNat := uadd _ _ (by omega)
217    obtain ⟨wn, hwn_def⟩ : ∃ x : UInt32, x = (if st.wnext + dist == st.wsize then 0 else st.wnext + dist) := ⟨_, rfl⟩
218    obtain ⟨wh, hwh_def⟩ : ∃ x : UInt32, x = (if st.whave < st.wsize then st.whave + dist else st.whave) := ⟨_, rfl⟩
219    have hwn_nat : (wn.toNat = 0 ∧ st.wnext.toNat + dist.toNat = st.wsize.toNat) ∨
220        (wn.toNat = st.wnext.toNat + dist.toNat ∧ st.wnext.toNat + dist.toNat < st.wsize.toNat) := by
221      rw [hwn_def]
222      by_cases hq : st.wnext + dist == st.wsize
223      · left; rw [ite_eq_left hq]
224        have := UInt32.toNat_inj.mpr (beq_iff_eq.mp hq)
225        refine ⟨rfl, by omega⟩
226      · right; rw [ite_eq_right hq]
227        have hne' : ¬ (st.wnext + dist = st.wsize) := fun hh => hq (beq_iff_eq.mpr hh)
228        have : st.wnext.toNat + dist.toNat ≠ st.wsize.toNat := fun hh =>
229          hne' (UInt32.toNat_inj.mp (by omega))
230        exact ⟨hadd, by omega⟩
231    have hwh_nat : (st.whave.toNat < st.wsize.toNat ∧ wh.toNat = st.whave.toNat + dist.toNat) ∨
232        (¬ st.whave.toNat < st.wsize.toNat ∧ wh.toNat = st.whave.toNat) := by
233      rw [hwh_def]
234      by_cases hl : st.whave < st.wsize
235      · left; rw [ite_eq_left hl]
236        have hl' := UInt32.lt_iff_toNat_lt.mp hl
237        have := heq hl'
238        exact ⟨hl', uadd _ _ (by omega)⟩
239      · right; rw [ite_eq_right hl]; exact ⟨fun hh => hl (UInt32.lt_iff_toNat_lt.mpr hh), rfl⟩
240    have hs0' : ({ h with bytes := upd h.bytes w' (some A1) } : Heap).istates zs = some s0 := hs0
241    refine ⟨{ { h with bytes := upd h.bytes w' (some A1) } with
242        istates := upd h.istates zs (some { st with wnext := wn, whave := wh }) },
243      { st with wnext := wn, whave := wh }, ?_, ?_⟩
244    · simp only [uw_small, hw, ← hdist, hstep1, hcp', Bool.false_eq_true, ite_false, ← hwn_def, ← hwh_def]
245      simp only [bind_app, stInflateState_tab hs0', pure_app]
246    · refine ⟨by simp, ⟨hk2, ⟨w', A1, hw, by simp, by simpa using hro, by show A1.size = 2 ^ st.wbits.toNat; omega⟩,
247          hws, ?_, ?_, ?_⟩,
248        fun r hr => by simp [upd_ne _ _ _ _ hr], ⟨rfl, rfl, rfl, rfl, rfl, rfl, rfl⟩,
249        fun b hb => by simp [upd_ne _ _ _ _ hb], hw⟩
250      · show wh.toNat ≤ st.wsize.toNat
251        omega
252      · show wn.toNat < st.wsize.toNat ∨ (st.wsize.toNat = 0 ∧ wn.toNat = 0)
253        omega
254      · show wh.toNat < st.wsize.toNat → wn.toNat = wh.toNat
255        omega
256
257
258end Zlib.Inflate.Proofs.W