inflate.c.ring.lean

Lean source with line numbers. Follow a line number to locate a statement, or an import to read its dependency.

1import ZlibF.Proof.«inflate.c.uw»
2
3namespace Zlib.Inflate.Spec
4
5/-- The slot of the ring buffer (of size `ws`, next write position `wn`, `wh` valid bytes) that holds the `j`-th oldest
6valid byte: the valid bytes end just before `wn` and wrap around the end of the buffer. -/
7def ringSlot (ws wn wh j : Nat) : Nat :=
8  if wh ≤ wn then wn - wh + j else if j < wh - wn then ws - (wh - wn) + j else j - (wh - wn)
9
10/-- The history the ring buffer `win` holds, oldest byte first: the last `wh` bytes written. -/
11def ringList (win : Array UInt8) (ws wn wh : Nat) : List UInt8 :=
12  (List.range wh).map (fun j => win[ringSlot ws wn wh j]!)
13
14/-- The `c` bytes of the buffer `e` that end at offset `eo`. -/
15def newBytes (e : Array UInt8) (eo c : Nat) : List UInt8 := (List.range c).map (fun i => e[eo - c + i]!)
16
17end Zlib.Inflate.Spec
18
19namespace Zlib.Inflate.Proofs
20open C Zlib.Inflate Zlib.Inflate.Spec
21
22theorem copyRange_succ (d s : Array UInt8) (doff soff n : Nat) :
23    copyRange d s doff soff (n + 1) = (copyRange d s doff soff n).set! (doff + n) s[soff + n]! := by
24  unfold copyRange
25  rw [List.range_succ, List.foldl_append]
26  rfl
27
28theorem copyRange_getElem? (d s : Array UInt8) (doff soff n : Nat) (hd : doff + n ≤ d.size) (hs : soff + n ≤ s.size) (i : Nat) :
29    (copyRange d s doff soff n)[i]? = if doff ≤ i ∧ i < doff + n then s[soff + (i - doff)]? else d[i]? := by
30  induction n generalizing i with
31  | zero =>
32    simp only [copyRange, List.range_zero, List.foldl_nil]
33    by_cases h : doff ≤ i ∧ i < doff + 0
34    · omega
35    · rw [ite_eq_right h]
36  | succ n ih =>
37    rw [copyRange_succ, Array.set!_eq_setIfInBounds, Array.getElem?_setIfInBounds, ih (by omega) (by omega)]
38    have hsz : (copyRange d s doff soff n).size = d.size := size_copyRange ..
39    by_cases h1 : doff + n = i
40    · subst h1
41      have : ¬ (doff ≤ doff + n ∧ doff + n < doff + n) := by omega
42      have h3 : doff + n < (copyRange d s doff soff n).size := by omega
43      have h4 : soff + n < s.size := by omega
44      simp [h3, getElem!_pos s (soff + n) h4, Array.getElem?_eq_getElem h4]
45    · by_cases h2 : doff ≤ i ∧ i < doff + (n + 1)
46      · have h5 : doff ≤ i ∧ i < doff + n := by omega
47        simp [h1, h2, h5]
48      · have h5 : ¬ (doff ≤ i ∧ i < doff + n) := by omega
49        simp [h1, h2, h5]
50
51/-- The four ways `uwPost` fills the ring buffer, in terms of `Nat` (`ws` = `wsize`, `wn` = `wnext`, `wh` = `whave`). -/
52theorem uwPost_nat {st : InflateState} {a ebytes : Array UInt8} {eo : Nat} {copy : UInt32}
53    (hpos : st.wsize.toNat ≠ 0)
54    (hv : st.whave.toNat ≤ st.wsize.toNat) (hwn : st.wnext.toNat < st.wsize.toNat)
55    (heq : st.whave.toNat < st.wsize.toNat → st.wnext.toNat = st.whave.toNat) (hw32 : st.wsize.toNat ≤ 2 ^ 16) :
56    let ws := st.wsize.toNat; let wn := st.wnext.toNat; let wh := st.whave.toNat; let c := copy.toNat
57    let P := uwPost st a ebytes eo copy
58    (ws ≤ c ∧ P.1 = copyRange a ebytes 0 (eo - ws) ws ∧ P.2.wnext.toNat = 0 ∧ P.2.whave.toNat = ws) ∨
59    (wn + c < ws ∧ P.1 = copyRange a ebytes wn (eo - c) c ∧ P.2.wnext.toNat = wn + c ∧
60      P.2.whave.toNat = (if wh < ws then wh + c else wh)) ∨
61    (wn + c = ws ∧ c < ws ∧ P.1 = copyRange a ebytes wn (eo - c) c ∧ P.2.wnext.toNat = 0 ∧
62      P.2.whave.toNat = (if wh < ws then wh + c else wh)) ∨
63    (ws < wn + c ∧ c < ws ∧
64      P.1 = copyRange (copyRange a ebytes wn (eo - c) (ws - wn)) ebytes 0 (eo - (c - (ws - wn))) (c - (ws - wn)) ∧
65      P.2.wnext.toNat = c - (ws - wn) ∧ P.2.whave.toNat = ws) := by
66  intro ws wn wh c P
67  have e1 := st.wsize.toNat_lt
68  have e2 := st.wnext.toNat_lt
69  have e3 := st.whave.toNat_lt
70  have e4 := copy.toNat_lt
71  simp only [ws, wn, wh, c, P]
72  unfold uwPost
73  repeat' split
74  all_goals
75    simp only [UInt32.lt_iff_toNat_lt, UInt32.le_iff_toNat_le, UInt32.toNat_add, UInt32.toNat_sub, gt_iff_lt, beq_iff_eq,
76      bne_iff_ne, ne_eq, ← UInt32.toNat_inj, UInt32.toNat_zero, Nat.not_lt, Nat.not_le] at *
77  all_goals first
78    | (refine Or.inl ⟨?_, ?_, ?_, ?_⟩ <;> first | omega | rfl | trivial | (congr 1 <;> first | omega | (congr 1 <;> first | omega | (congr 1 <;> omega))))
79    | (refine Or.inr (Or.inl ⟨?_, ?_, ?_, ?_⟩) <;> first | omega | rfl | trivial | (congr 1 <;> first | omega | (congr 1 <;> first | omega | (congr 1 <;> omega))))
80    | (refine Or.inr (Or.inr (Or.inl ⟨?_, ?_, ?_, ?_, ?_⟩)) <;> first | omega | rfl | trivial | (congr 1 <;> first | omega | (congr 1 <;> first | omega | (congr 1 <;> omega))))
81    | (refine Or.inr (Or.inr (Or.inr ⟨?_, ?_, ?_, ?_, ?_⟩)) <;> first | omega | rfl | trivial | (congr 1 <;> first | omega | (congr 1 <;> first | omega | (congr 1 <;> omega))))
82
83theorem copyRange_bang (d s : Array UInt8) (doff soff n : Nat) (hd : doff + n ≤ d.size) (hs : soff + n ≤ s.size) (i : Nat)
84    (hi : i < d.size) :
85    (copyRange d s doff soff n)[i]! = if doff ≤ i ∧ i < doff + n then s[soff + (i - doff)]! else d[i]! := by
86  have hsz : (copyRange d s doff soff n).size = d.size := size_copyRange ..
87  have := copyRange_getElem? d s doff soff n hd hs i
88  rw [getElem!_pos _ _ (by omega)]
89  by_cases h : doff ≤ i ∧ i < doff + n
90  · rw [ite_eq_left h] at this ⊢
91    rw [getElem!_pos s _ (by omega)]
92    have h2 : soff + (i - doff) < s.size := by omega
93    rw [Array.getElem?_eq_getElem h2, Array.getElem?_eq_getElem (by omega)] at this
94    exact Option.some.inj this
95  · rw [ite_eq_right h] at this ⊢
96    rw [getElem!_pos d _ hi]
97    rw [Array.getElem?_eq_getElem hi, Array.getElem?_eq_getElem (by omega)] at this
98    exact Option.some.inj this
99
100set_option hygiene false in
101/-- One element of the ring after the copy: evaluate the slots, split the cases, compare the indices. -/
102macro "ring_tail" : tactic => `(tactic| (
103  simp only [ringList, newBytes, List.getElem_drop, List.getElem_append, List.getElem_map, List.getElem_range,
104    List.length_map, List.length_range] at h1 h2 ⊢
105  subst hA'
106  rw [hwn', hwh'] at *
107  unfold ringSlot
108  repeat' split
109  all_goals (rw [copyRange_bang _ _ _ _ _ (by omega) (by omega) _ (by omega)]; repeat' split)
110  all_goals (try (rw [copyRange_bang _ _ _ _ _ (by omega) (by omega) _ (by omega)]; repeat' split))
111  all_goals first | rfl | (exfalso; omega) | (congr 1 <;> omega)))
112
113/-- **The ring buffer after `updatewindow` holds the last `wsize` bytes of the history.** The history before the call is
114the ring (`ringList`); the call appends the `copy` bytes that end at offset `eo` of the buffer; the new ring is the last
115`min wsize (whave + copy)` bytes of that concatenation. -/
116theorem ring_spec {st : InflateState} {a ebytes : Array UInt8} {eo : Nat} {copy : UInt32}
117    (hpos : st.wsize.toNat ≠ 0)
118    (hv : st.whave.toNat ≤ st.wsize.toNat) (hwn : st.wnext.toNat < st.wsize.toNat)
119    (heq : st.whave.toNat < st.wsize.toNat → st.wnext.toNat = st.whave.toNat) (hw32 : st.wsize.toNat ≤ 2 ^ 16)
120    (hasz : st.wsize.toNat ≤ a.size) (hc : copy.toNat ≤ eo) (hoff : eo ≤ ebytes.size) (hA : a.size = st.wsize.toNat) :
121    ringList (uwPost st a ebytes eo copy).1 st.wsize.toNat (uwPost st a ebytes eo copy).2.wnext.toNat
122        (uwPost st a ebytes eo copy).2.whave.toNat =
123      ((ringList a st.wsize.toNat st.wnext.toNat st.whave.toNat ++ newBytes ebytes eo copy.toNat).drop
124        (st.whave.toNat + copy.toNat - (uwPost st a ebytes eo copy).2.whave.toNat)) := by
125  have hn := uwPost_nat (a := a) (ebytes := ebytes) (eo := eo) (copy := copy) hpos hv hwn heq hw32
126  simp only at hn
127  have hsz := uwPost_size st a ebytes eo copy
128  generalize uwPost st a ebytes eo copy = P at *
129  obtain ⟨A', st'⟩ := P
130  simp only at *
131  rcases hn with ⟨c1, hA', hwn', hwh'⟩ | ⟨c1, hA', hwn', hwh'⟩ | ⟨c1, c2, hA', hwn', hwh'⟩ | ⟨c1, c2, hA', hwn', hwh'⟩
132  · apply List.ext_getElem
133    · simp [ringList, newBytes, hwh'] <;> omega
134    · intro j h1 h2; ring_tail
135  · by_cases hw : st.whave.toNat < st.wsize.toNat
136    · have hq := heq hw
137      simp only [hw, ite_true] at hwh'
138      apply List.ext_getElem
139      · simp [ringList, newBytes, hwh'] <;> omega
140      · intro j h1 h2; ring_tail
141    · simp only [hw, ite_false] at hwh'
142      apply List.ext_getElem
143      · simp [ringList, newBytes, hwh'] <;> omega
144      · intro j h1 h2; ring_tail
145  · by_cases hw : st.whave.toNat < st.wsize.toNat
146    · have hq := heq hw
147      simp only [hw, ite_true] at hwh'
148      apply List.ext_getElem
149      · simp [ringList, newBytes, hwh'] <;> omega
150      · intro j h1 h2; ring_tail
151    · simp only [hw, ite_false] at hwh'
152      apply List.ext_getElem
153      · simp [ringList, newBytes, hwh'] <;> omega
154      · intro j h1 h2; ring_tail
155  · by_cases hw : st.whave.toNat < st.wsize.toNat
156    · have hq := heq hw
157      apply List.ext_getElem
158      · simp [ringList, newBytes, hwh'] <;> omega
159      · intro j h1 h2
160        have hin : (copyRange a ebytes st.wnext.toNat (eo - copy.toNat) (st.wsize.toNat - st.wnext.toNat)).size = a.size := size_copyRange ..
161        ring_tail
162    · apply List.ext_getElem
163      · simp [ringList, newBytes, hwh'] <;> omega
164      · intro j h1 h2
165        have hin : (copyRange a ebytes st.wnext.toNat (eo - copy.toNat) (st.wsize.toNat - st.wnext.toNat)).size = a.size := size_copyRange ..
166        ring_tail
167
168/-- **The indices after `updatewindow`.** `whave` becomes `min wsize (whave + copy)`; `wnext` advances by `copy`
169modulo `wsize` (it is 0 when `copy ≥ wsize`). -/
170theorem uwPost_counts {st : InflateState} {a ebytes : Array UInt8} {eo : Nat} {copy : UInt32}
171    (hpos : st.wsize.toNat ≠ 0)
172    (hv : st.whave.toNat ≤ st.wsize.toNat) (hwn : st.wnext.toNat < st.wsize.toNat)
173    (heq : st.whave.toNat < st.wsize.toNat → st.wnext.toNat = st.whave.toNat) (hw32 : st.wsize.toNat ≤ 2 ^ 16) :
174    (uwPost st a ebytes eo copy).2.whave.toNat = min st.wsize.toNat (st.whave.toNat + copy.toNat) ∧
175    ((st.wsize.toNat ≤ copy.toNat ∧ (uwPost st a ebytes eo copy).2.wnext.toNat = 0) ∨
176     (st.wnext.toNat + copy.toNat < st.wsize.toNat ∧ copy.toNat < st.wsize.toNat ∧
177       (uwPost st a ebytes eo copy).2.wnext.toNat = st.wnext.toNat + copy.toNat) ∨
178     (st.wsize.toNat ≤ st.wnext.toNat + copy.toNat ∧ copy.toNat < st.wsize.toNat ∧
179       (uwPost st a ebytes eo copy).2.wnext.toNat = st.wnext.toNat + copy.toNat - st.wsize.toNat)) := by
180  have hn := uwPost_nat (a := a) (ebytes := ebytes) (eo := eo) (copy := copy) hpos hv hwn heq hw32
181  simp only at hn
182  generalize uwPost st a ebytes eo copy = P at *
183  obtain ⟨A', st'⟩ := P
184  simp only at *
185  rcases hn with ⟨c1, -, hwn', hwh'⟩ | ⟨c1, -, hwn', hwh'⟩ | ⟨c1, c2, -, hwn', hwh'⟩ | ⟨c1, c2, -, hwn', hwh'⟩
186  all_goals
187    by_cases hw : st.whave.toNat < st.wsize.toNat
188    all_goals first
189      | (have hq := heq hw; simp only [hw, ite_true] at hwh'; omega)
190      | (simp only [hw, ite_false] at hwh'; omega)
191      | omega
192
193/-- **updatewindow, window content.** On a good stream whose window block exists, the window after the call, read as a
194ring (`ringList`), is the last `wsize` bytes of the history before the call (the ring read from the state with `wsize`
195set, empty when it was just set) followed by the `copy` bytes that end at offset `eo` of the caller's buffer;
196`whave` is `min wsize (whave + copy)`. -/
197theorem updatewindow_ring {H : Heap} {r : ZStreamRef} {zs : Nat} {z : ZStream} {st : InflateState} {w eb eo : Nat}
198    {a ebytes : Array UInt8} {copy : UInt32}
199    (hG : Good H r zs z st) (hw : st.window = .ref (.blk w) 0) (ha : H.bytes w = some a) (hro : H.ro w = false)
200    (hasz : a.size = 2 ^ st.wbits.toNat)
201    (heb : H.bytes eb = some ebytes) (hne : w ≠ eb) (hc : copy.toNat ≤ eo) (hoff : eo ≤ ebytes.size) :
202    ∃ H' st' A', updatewindow (some r) (.ref (.blk eb) eo) copy H = .ok (0, H') ∧ Good H' r zs z st' ∧
203      H'.bytes w = some A' ∧
204      ringList A' (initWinS st).wsize.toNat st'.wnext.toNat st'.whave.toNat =
205        ((ringList a (initWinS st).wsize.toNat (initWinS st).wnext.toNat (initWinS st).whave.toNat ++
206            newBytes ebytes eo copy.toNat).drop ((initWinS st).whave.toNat + copy.toNat - st'.whave.toNat)) ∧
207      st'.whave.toNat = min (initWinS st).wsize.toNat ((initWinS st).whave.toNat + copy.toNat) := by
208  have hI := hG.inv
209  obtain ⟨f1, f2, f3, hv1, hwn1, heq1, -⟩ := initWinS_facts hI.win.wbits hI.win.ws hI.win.hv hI.win.wn hI.win.eq
210  have hwb := hI.win.wbits
211  have hle : (initWinS st).wsize.toNat ≤ 2 ^ 16 := by
212    rw [f1]; have := Nat.pow_le_pow_right (by decide : 0 < 2) (by omega : st.wbits.toNat ≤ 16); omega
213  have hposn : (initWinS st).wsize.toNat ≠ 0 := by rw [f1]; exact Nat.pos_iff_ne_zero.mp (Nat.two_pow_pos _)
214  obtain ⟨H', st', hrun, hH', hst', hG', -, hb', -, -, -, -⟩ := uw_post hG hw ha hro hasz heb hne hc hoff
215  refine ⟨H', st', _, hrun, hG', hb', ?_, ?_⟩
216  · rw [hst']
217    exact ring_spec hposn hv1 hwn1 heq1 hle (by rw [f1]; omega) hc hoff (by rw [f1]; omega)
218  · rw [hst']
219    exact (uwPost_counts hposn hv1 hwn1 heq1 hle).1
220
221end Zlib.Inflate.Proofs