inflate.c.sync.lean

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

1import ZlibF.Proof.«inflate.c.misc2»
2
3/-!
4# inflate.c: `syncsearch`
5
6The pattern search of `inflateSync`. `syncsearch(have, buf, len)` is a four-state automaton: `got` counts how many bytes
7of the pattern `00 00 FF FF` are matched at the end of the input so far. It stops after the byte that completes the
8pattern, or at the end of the input. The pure part (`syncStep`, `syncScan`) is the loop of the C function on a list of
9bytes; `syncScan_spec` shows what it computes: the position of the first occurrence of the pattern, and, when there is
10none, the longest proper prefix of the pattern that ends the input (the state to carry into the next call).
11-/
12
13namespace Zlib.Inflate.Spec
14open C
15
16/-- The pattern that `inflateSync` looks for: the end of an empty stored block (`00 00` is its length, `FF FF` the
17complement), which `deflate` writes at a sync or full flush point. -/
18def syncPat : List UInt8 := [0, 0, 255, 255]
19
20/-- One step of the loop of `syncsearch`: the new value of `got` after the byte `b`. -/
21def syncStep (got : UInt32) (b : UInt8) : UInt32 :=
22  if b.toNat == (if got < 2 then 0 else 0xff) then got + 1 else if b != 0 then 0 else 4 - got
23
24/-- The loop of `syncsearch` on the bytes `bs`, starting with `got`: the final `got` and the number of bytes consumed
25(the loop stops after the byte that makes `got` 4, or at the end of the input). -/
26def syncScan (got : UInt32) : List UInt8 → UInt32 × Nat
27  | [] => (got, 0)
28  | b :: bs => if got < 4 then ((syncScan (syncStep got b) bs).1, (syncScan (syncStep got b) bs).2 + 1)
29    else (got, 0)
30
31/-- `got` is the state of the search after the bytes `w`: the pattern has not occurred in `w`, and `got` is the length
32of the longest proper prefix of the pattern (at most 3 bytes) that ends `w`. -/
33def SyncSt (g : UInt32) (w : List UInt8) : Prop :=
34  g.toNat < 4 ∧ ¬ syncPat <:+: w ∧ syncPat.take g.toNat <:+ w ∧ ∀ k, k < 4 → syncPat.take k <:+ w → k ≤ g.toNat
35
36/-- The bytes `buf[0 .. len)` of a pointer `buf = .ref r o` into the array `a`. -/
37def syncBytes (a : Array UInt8) (o : Nat) (len : UInt32) : List UInt8 := (a.toList.drop o).take len.toNat
38
39/-- The input `p[0 .. len)` that `syncsearch` and `inflateSync` read, as `zlib.h` allows it: `len` readable bytes `bs`
40of a byte block of the heap (`o + len` within the block), or `NULL` with `len = 0` (`bs = []`). -/
41def SyncIn (h : Heap) (p : BPtr) (len : UInt32) (bs : List UInt8) : Prop :=
42  (∃ b a o, p = .ref (.blk b) o ∧ h.bytes b = some a ∧ o + len.toNat ≤ a.size ∧ bs = syncBytes a o len) ∨
43  (p = .null ∧ len = 0 ∧ bs = [])
44
45end Zlib.Inflate.Spec
46
47namespace Zlib.Inflate.Proofs
48open C Zlib.Inflate Zlib.Inflate.Spec
49
50/-! ### The pure part -/
51
52theorem infix_snoc {l w : List UInt8} {b : UInt8} : l <:+: w ++ [b] ↔ l <:+: w ∨ l <:+ w ++ [b] := by
53  have e1 : l <:+: w ++ [b] ↔ l.reverse <:+: (w ++ [b]).reverse := List.reverse_infix.symm
54  have e2 : l <:+ w ++ [b] ↔ l.reverse <+: (w ++ [b]).reverse := List.reverse_prefix.symm
55  have e3 : l <:+: w ↔ l.reverse <:+: w.reverse := List.reverse_infix.symm
56  rw [e1, e2, e3, List.reverse_append, List.reverse_singleton, List.singleton_append, List.infix_cons_iff]
57  exact Iff.intro (fun h => h.elim Or.inr Or.inl) (fun h => h.elim Or.inr Or.inl)
58
59theorem suffix_snoc {l w : List UInt8} {x b : UInt8} : l ++ [x] <:+ w ++ [b] ↔ x = b ∧ l <:+ w := by
60  rw [← List.reverse_prefix, ← List.reverse_prefix (l₁ := l)]
61  simp [List.cons_prefix_cons, eq_comm]
62
63theorem suffix_snoc0 {w : List UInt8} {b : UInt8} : [b] <:+ w ++ [b] := List.suffix_append _ _
64
65theorem suffix_snoc1 {w : List UInt8} {x b : UInt8} : [x] <:+ w ++ [b] ↔ x = b := by
66  have := @suffix_snoc [] w x b
67  simpa using this
68
69/-- Suffix facts used to step the search: the last byte of `w ++ [b]`, and the suffixes `[0]`, `[0,0]`, `[0,0,255]`. -/
70theorem sfx1 {w : List UInt8} {b : UInt8} : [0] <:+ w ++ [b] ↔ b = 0 := by
71  rw [suffix_snoc1]; exact ⟨fun h => h.symm, fun h => h.symm⟩
72theorem sfx2 {w : List UInt8} {b : UInt8} : [0, 0] <:+ w ++ [b] ↔ b = 0 ∧ [0] <:+ w := by
73  have := @suffix_snoc [0] w 0 b
74  simp only [List.cons_append, List.nil_append] at this
75  rw [this]; exact ⟨fun h => ⟨h.1.symm, h.2⟩, fun h => ⟨h.1.symm, h.2⟩⟩
76theorem sfx3 {w : List UInt8} {b : UInt8} : [0, 0, 255] <:+ w ++ [b] ↔ b = 255 ∧ [0, 0] <:+ w := by
77  have := @suffix_snoc [0, 0] w 255 b
78  simp only [List.cons_append, List.nil_append] at this
79  rw [this]; exact ⟨fun h => ⟨h.1.symm, h.2⟩, fun h => ⟨h.1.symm, h.2⟩⟩
80theorem sfx4 {w : List UInt8} {b : UInt8} : syncPat <:+ w ++ [b] ↔ b = 255 ∧ [0, 0, 255] <:+ w := by
81  have := @suffix_snoc [0, 0, 255] w 255 b
82  simp only [List.cons_append, List.nil_append] at this
83  unfold syncPat
84  rw [this]; exact ⟨fun h => ⟨h.1.symm, h.2⟩, fun h => ⟨h.1.symm, h.2⟩⟩
85
86theorem sfx2_1 {w : List UInt8} (h : [0, 0] <:+ w) : [0] <:+ w :=
87  List.IsSuffix.trans ⟨[0], rfl⟩ h
88
89theorem sfx3_not1 {w : List UInt8} (h : [0, 0, 255] <:+ w) : ¬ [0] <:+ w := by
90  obtain ⟨t, rfl⟩ := h
91  intro ⟨s, hs⟩
92  have : ([0] : List UInt8) <:+ t ++ [0, 0, 255] := ⟨s, hs⟩
93  have e : t ++ [0, 0, 255] = (t ++ [0, 0]) ++ [255] := by simp
94  rw [e, sfx1] at this
95  exact absurd this (by decide)
96
97theorem sfx3_not2 {w : List UInt8} (h : [0, 0, 255] <:+ w) : ¬ [0, 0] <:+ w :=
98  fun h2 => sfx3_not1 h (sfx2_1 h2)
99
100/-- The state description for each value of `got`. -/
101theorem syncSt_cases {g : UInt32} {w : List UInt8} (hs : SyncSt g w) :
102    (g = 0 ∧ ¬ [0] <:+ w ∧ ¬ [0, 0] <:+ w ∧ ¬ [0, 0, 255] <:+ w) ∨
103    (g = 1 ∧ [0] <:+ w ∧ ¬ [0, 0] <:+ w ∧ ¬ [0, 0, 255] <:+ w) ∨
104    (g = 2 ∧ [0, 0] <:+ w ∧ ¬ [0, 0, 255] <:+ w) ∨
105    (g = 3 ∧ [0, 0, 255] <:+ w) := by
106  obtain ⟨hlt, -, hpre, hmax⟩ := hs
107  have m1 := hmax 1 (by omega)
108  have m2 := hmax 2 (by omega)
109  have m3 := hmax 3 (by omega)
110  have e1 : syncPat.take 1 = [0] := rfl
111  have e2 : syncPat.take 2 = [0, 0] := rfl
112  have e3 : syncPat.take 3 = [0, 0, 255] := rfl
113  rw [e1] at m1; rw [e2] at m2; rw [e3] at m3
114  have hg : g.toNat = 0 ∨ g.toNat = 1 ∨ g.toNat = 2 ∨ g.toNat = 3 := by omega
115  rcases hg with hg | hg | hg | hg
116  · left
117    refine ⟨UInt32.toNat_inj.mp (by simpa using hg), fun h => ?_, fun h => ?_, fun h => ?_⟩
118    · have := m1 h; omega
119    · have := m2 h; omega
120    · have := m3 h; omega
121  · right; left
122    rw [hg] at hpre
123    refine ⟨UInt32.toNat_inj.mp (by simpa using hg), hpre, fun h => ?_, fun h => ?_⟩
124    · have := m2 h; omega
125    · have := m3 h; omega
126  · right; right; left
127    rw [hg] at hpre
128    refine ⟨UInt32.toNat_inj.mp (by simpa using hg), hpre, fun h => ?_⟩
129    have := m3 h; omega
130  · right; right; right
131    rw [hg] at hpre
132    exact ⟨UInt32.toNat_inj.mp (by simpa using hg), hpre⟩
133
134theorem syncSt_mk {g : UInt32} {w : List UInt8}
135    (hn : ¬ syncPat <:+: w)
136    (hc : (g = 0 ∧ ¬ [0] <:+ w ∧ ¬ [0, 0] <:+ w ∧ ¬ [0, 0, 255] <:+ w) ∨
137    (g = 1 ∧ [0] <:+ w ∧ ¬ [0, 0] <:+ w ∧ ¬ [0, 0, 255] <:+ w) ∨
138    (g = 2 ∧ [0, 0] <:+ w ∧ ¬ [0, 0, 255] <:+ w) ∨
139    (g = 3 ∧ [0, 0, 255] <:+ w)) : SyncSt g w := by
140  have e1 : syncPat.take 1 = [0] := rfl
141  have e2 : syncPat.take 2 = [0, 0] := rfl
142  have e3 : syncPat.take 3 = [0, 0, 255] := rfl
143  have e0 : syncPat.take 0 = [] := rfl
144  rcases hc with ⟨rfl, a1, a2, a3⟩ | ⟨rfl, a1, a2, a3⟩ | ⟨rfl, a2, a3⟩ | ⟨rfl, a3⟩
145  · refine ⟨by decide, hn, ?_, ?_⟩
146    · show syncPat.take 0 <:+ w
147      rw [e0]; exact List.nil_suffix
148    · intro k hk hs
149      have : k = 0 ∨ k = 1 ∨ k = 2 ∨ k = 3 := by omega
150      rcases this with rfl | rfl | rfl | rfl
151      · decide
152      · rw [e1] at hs; exact absurd hs a1
153      · rw [e2] at hs; exact absurd hs a2
154      · rw [e3] at hs; exact absurd hs a3
155  · refine ⟨by decide, hn, ?_, ?_⟩
156    · show syncPat.take 1 <:+ w
157      rw [e1]; exact a1
158    · intro k hk hs
159      have : k = 0 ∨ k = 1 ∨ k = 2 ∨ k = 3 := by omega
160      rcases this with rfl | rfl | rfl | rfl
161      · decide
162      · decide
163      · rw [e2] at hs; exact absurd hs a2
164      · rw [e3] at hs; exact absurd hs a3
165  · refine ⟨by decide, hn, ?_, ?_⟩
166    · show syncPat.take 2 <:+ w
167      rw [e2]; exact a2
168    · intro k hk hs
169      have : k = 0 ∨ k = 1 ∨ k = 2 ∨ k = 3 := by omega
170      rcases this with rfl | rfl | rfl | rfl
171      · decide
172      · decide
173      · decide
174      · rw [e3] at hs; exact absurd hs a3
175  · refine ⟨by decide, hn, ?_, ?_⟩
176    · show syncPat.take 3 <:+ w
177      rw [e3]; exact a3
178    · intro k hk hs
179      have : k = 0 ∨ k = 1 ∨ k = 2 ∨ k = 3 := by omega
180      rcases this with rfl | rfl | rfl | rfl <;> decide
181
182/-- The search starts in state 0 with nothing read. -/
183theorem syncSt_zero : SyncSt 0 [] := by
184  refine syncSt_mk (by decide) (Or.inl ⟨rfl, ?_, ?_, ?_⟩)
185  · rintro ⟨t, ht⟩; simp at ht
186  · rintro ⟨t, ht⟩; simp at ht
187  · rintro ⟨t, ht⟩; simp at ht
188
189theorem u8_eq255 {b : UInt8} : b.toNat = 255 ↔ b = 255 := by
190  constructor
191  · intro h; exact UInt8.toNat_inj.mp (by simpa using h)
192  · rintro rfl; rfl
193
194theorem u8_eq0 {b : UInt8} : b.toNat = 0 ↔ b = 0 := by
195  constructor
196  · intro h; exact UInt8.toNat_inj.mp (by simpa using h)
197  · rintro rfl; rfl
198
199/-- **One step.** If the pattern has not occurred in `w` and `got` is the state after `w`, then after the byte `b`: either
200the pattern ends here (`syncStep` gives 4 and the pattern is a suffix of `w ++ [b]`), or the pattern has still not
201occurred and `syncStep` gives the state after `w ++ [b]`. -/
202theorem syncStep_spec {g : UInt32} {w : List UInt8} (hs : SyncSt g w) (b : UInt8) :
203    (syncStep g b = 4 ∧ syncPat <:+ w ++ [b]) ∨ (syncStep g b < 4 ∧ SyncSt (syncStep g b) (w ++ [b])) := by
204  have hn := hs.2.1
205  have hP : syncPat <:+ w ++ [b] ↔ b = 255 ∧ [0, 0, 255] <:+ w := sfx4
206  have hI : syncPat <:+: w ++ [b] ↔ syncPat <:+: w ∨ syncPat <:+ w ++ [b] := infix_snoc
207  have t1 : [0] <:+ w ++ [b] ↔ b = 0 := sfx1
208  have t2 : [0, 0] <:+ w ++ [b] ↔ b = 0 ∧ [0] <:+ w := sfx2
209  have t3 : [0, 0, 255] <:+ w ++ [b] ↔ b = 255 ∧ [0, 0] <:+ w := sfx3
210  have hno : ¬ syncPat <:+: w ++ [b] ↔ ¬ (b = 255 ∧ [0, 0, 255] <:+ w) := by
211    rw [hI, hP]; simp [hn]
212  by_cases hb0 : b = 0
213  · subst hb0
214    have h255 : ¬ ((0 : UInt8) = 255 ∧ [0, 0, 255] <:+ w) := fun h => absurd h.1 (by decide)
215    rcases syncSt_cases hs with ⟨rfl, a1, a2, a3⟩ | ⟨rfl, a1, a2, a3⟩ | ⟨rfl, a2, a3⟩ | ⟨rfl, a3⟩
216    · have e : syncStep 0 0 = 1 := by decide
217      rw [e]; right
218      refine ⟨by decide, syncSt_mk (hno.mpr h255) (Or.inr (Or.inl ⟨rfl, t1.mpr rfl, ?_, ?_⟩))⟩
219      · rw [t2]; simp [a1]
220      · rw [t3]; simp
221    · have e : syncStep 1 0 = 2 := by decide
222      rw [e]; right
223      refine ⟨by decide, syncSt_mk (hno.mpr h255) (Or.inr (Or.inr (Or.inl ⟨rfl, ?_, ?_⟩)))⟩
224      · rw [t2]; simp [a1]
225      · rw [t3]; simp
226    · have e : syncStep 2 0 = 2 := by decide
227      rw [e]; right
228      refine ⟨by decide, syncSt_mk (hno.mpr h255) (Or.inr (Or.inr (Or.inl ⟨rfl, ?_, ?_⟩)))⟩
229      · rw [t2]; exact ⟨rfl, sfx2_1 a2⟩
230      · rw [t3]; simp
231    · have e : syncStep 3 0 = 1 := by decide
232      rw [e]; right
233      refine ⟨by decide, syncSt_mk (hno.mpr h255) (Or.inr (Or.inl ⟨rfl, t1.mpr rfl, ?_, ?_⟩))⟩
234      · rw [t2]; simp; exact sfx3_not1 a3
235      · rw [t3]; simp
236  · by_cases hb255 : b = 255
237    · subst hb255
238      rcases syncSt_cases hs with ⟨rfl, a1, a2, a3⟩ | ⟨rfl, a1, a2, a3⟩ | ⟨rfl, a2, a3⟩ | ⟨rfl, a3⟩
239      · have e : syncStep 0 255 = 0 := by decide
240        rw [e]; right
241        refine ⟨by decide, syncSt_mk (hno.mpr (by simp [a3])) (Or.inl ⟨rfl, ?_, ?_, ?_⟩)⟩
242        · rw [t1]; decide
243        · rw [t2]; simp
244        · rw [t3]; simp [a2]
245      · have e : syncStep 1 255 = 0 := by decide
246        rw [e]; right
247        refine ⟨by decide, syncSt_mk (hno.mpr (by simp [a3])) (Or.inl ⟨rfl, ?_, ?_, ?_⟩)⟩
248        · rw [t1]; decide
249        · rw [t2]; simp
250        · rw [t3]; simp [a2]
251      · have e : syncStep 2 255 = 3 := by decide
252        rw [e]; right
253        refine ⟨by decide, syncSt_mk (hno.mpr (by simp [a3])) (Or.inr (Or.inr (Or.inr ⟨rfl, ?_⟩)))⟩
254        rw [t3]; exact ⟨rfl, a2⟩
255      · have e : syncStep 3 255 = 4 := by decide
256        rw [e]; left
257        exact ⟨rfl, hP.mpr ⟨rfl, a3⟩⟩
258    · have hb0' : ¬ b.toNat = 0 := fun h => hb0 (u8_eq0.mp h)
259      have hb255' : ¬ b.toNat = 255 := fun h => hb255 (u8_eq255.mp h)
260      have e : ∀ g : UInt32, syncStep g b = 0 := by
261        intro g
262        unfold syncStep
263        by_cases hg : g < 2
264        · simp [hg, hb0, hb0']
265        · simp [hg, hb0, hb255']
266      have h255 : ¬ (b = 255 ∧ [0, 0, 255] <:+ w) := fun h => hb255 h.1
267      have fin : SyncSt 0 (w ++ [b]) := by
268        refine syncSt_mk (hno.mpr h255) (Or.inl ⟨rfl, ?_, ?_, ?_⟩)
269        · rw [t1]; exact hb0
270        · rw [t2]; exact fun h => hb0 h.1
271        · rw [t3]; exact fun h => hb255 h.1
272      rw [e]; right
273      exact ⟨by decide, fin⟩
274
275theorem syncScan_nil (g : UInt32) : syncScan g [] = (g, 0) := rfl
276
277theorem syncScan_cons_lt {g : UInt32} (hg : g < 4) (b : UInt8) (bs : List UInt8) :
278    syncScan g (b :: bs) = ((syncScan (syncStep g b) bs).1, (syncScan (syncStep g b) bs).2 + 1) := by
279  simp [syncScan, hg]
280
281theorem syncScan_ge {g : UInt32} (hg : ¬ g < 4) (bs : List UInt8) : syncScan g bs = (g, 0) := by
282  cases bs <;> simp [syncScan, hg]
283
284theorem syncScan_le (g : UInt32) (bs : List UInt8) : (syncScan g bs).2 ≤ bs.length := by
285  induction bs generalizing g with
286  | nil => simp [syncScan]
287  | cons b bs ih =>
288    by_cases hg : g < 4
289    · rw [syncScan_cons_lt hg]; simp; exact ih _
290    · rw [syncScan_ge hg]; simp
291
292/-- **The search (pure part).** Let `g` be the state after the bytes `w` (`SyncSt`: the pattern `00 00 FF FF` has not
293occurred in `w`, and `g` is the longest proper prefix of it that ends `w`). Scanning the bytes `bs` from `g` gives
294`(G, L)` with `L ≤ |bs|` and:
295* if `G = 4` the pattern was found, and `L` is the number of bytes consumed up to and including its last byte: `L > 0`,
296  the pattern ends `w ++ bs[0 .. L)`, and it does not occur in `w ++ bs[0 .. L')` for any `L' < L` (the first
297  occurrence);
298* otherwise all of `bs` was consumed (`L = |bs|`) and `G` is the state after `w ++ bs`: the pattern has not occurred and
299  `G` is the longest proper prefix of the pattern that ends the whole input (the state to carry into the next call). -/
300theorem syncScan_spec {g : UInt32} {w : List UInt8} (hs : SyncSt g w) (bs : List UInt8) {G : UInt32} {L : Nat}
301    (hr : syncScan g bs = (G, L)) :
302    L ≤ bs.length ∧
303    (G = 4 → 0 < L ∧ syncPat <:+ w ++ bs.take L ∧ ∀ L', L' < L → ¬ syncPat <:+: w ++ bs.take L') ∧
304    (G ≠ 4 → L = bs.length ∧ SyncSt G (w ++ bs)) := by
305  induction bs generalizing g w G L with
306  | nil =>
307    rw [syncScan_nil] at hr
308    obtain ⟨rfl, rfl⟩ := Prod.mk.inj hr
309    refine ⟨Nat.le_refl _, fun h4 => ?_, fun _ => ⟨rfl, by simpa using hs⟩⟩
310    have := hs.1; rw [h4] at this; exact absurd this (by decide)
311  | cons b bs ih =>
312    have hg4 : g < 4 := UInt32.lt_iff_toNat_lt.mpr (by simpa using hs.1)
313    rw [syncScan_cons_lt hg4] at hr
314    obtain ⟨hG, hL⟩ := Prod.mk.inj hr
315    rcases syncStep_spec hs b with ⟨h4, hpat⟩ | ⟨hlt, hs'⟩
316    · have hfin : syncScan (syncStep g b) bs = (4, 0) := syncScan_ge (by rw [h4]; decide) bs |>.trans (by rw [h4])
317      rw [hfin] at hG hL
318      simp only at hG hL
319      subst hG; subst hL
320      refine ⟨by simp, fun _ => ⟨by simp, by simpa using hpat, ?_⟩, fun h => absurd rfl h⟩
321      intro L' hL'
322      have : L' = 0 := by omega
323      subst this
324      simpa using hs.2.1
325    · obtain ⟨ih1, ih2, ih3⟩ := ih hs' (show syncScan (syncStep g b) bs = ((syncScan (syncStep g b) bs).1, (syncScan (syncStep g b) bs).2) from rfl)
326      rw [← hG, ← hL]
327      refine ⟨by simp; omega, fun h4 => ?_, fun h4 => ?_⟩
328      · obtain ⟨a1, a2, a3⟩ := ih2 h4
329        refine ⟨by omega, ?_, ?_⟩
330        · simpa [List.append_assoc] using a2
331        · intro L' hL'
332          cases L' with
333          | zero => simpa using hs.2.1
334          | succ j =>
335            have := a3 j (by omega)
336            simpa [List.append_assoc] using this
337      · obtain ⟨a1, a2⟩ := ih3 h4
338        refine ⟨by simp; omega, ?_⟩
339        simpa [List.append_assoc] using a2
340
341/-- The search finds the pattern exactly when it occurs in the history followed by the new bytes. -/
342theorem syncScan_found_iff {g : UInt32} {w : List UInt8} (hs : SyncSt g w) (bs : List UInt8) :
343    (syncScan g bs).1 = 4 ↔ syncPat <:+: w ++ bs := by
344  obtain ⟨-, h1, h2⟩ := syncScan_spec hs bs rfl
345  constructor
346  · intro h
347    obtain ⟨-, a2, -⟩ := h1 h
348    have hin : w ++ bs.take (syncScan g bs).2 <:+: w ++ bs :=
349      ⟨[], bs.drop (syncScan g bs).2, by simp [List.append_assoc]⟩
350    exact (List.IsSuffix.isInfix a2).trans hin
351  · intro h
352    refine Classical.byContradiction fun hne => ?_
353    exact (h2 hne).2.2.1 (by simpa using h)
354
355/-! ### The loop on the heap -/
356
357theorem syncBytes_length {a : Array UInt8} {o : Nat} {len : UInt32} (hl : o + len.toNat ≤ a.size) :
358    (syncBytes a o len).length = len.toNat := by
359  simp [syncBytes]; omega
360
361theorem syncBytes_drop {a : Array UInt8} {o : Nat} {len : UInt32} (hl : o + len.toNat ≤ a.size) (n : Nat)
362    (hn : n < len.toNat) :
363    (syncBytes a o len).drop n = a[o + n]'(by omega) :: (syncBytes a o len).drop (n + 1) := by
364  have hn' : n < (syncBytes a o len).length := by rw [syncBytes_length hl]; exact hn
365  rw [List.drop_eq_getElem_cons hn']
366  congr 1
367  simp [syncBytes, List.getElem_take, List.getElem_drop]
368
369theorem syncScan_zero {g G : UInt32} {bs : List UInt8} (h : syncScan g bs = (G, 0)) :
370    G = g ∧ (¬ g < 4 ∨ bs = []) := by
371  cases bs with
372  | nil => simp [syncScan] at h; exact ⟨h.symm, Or.inr rfl⟩
373  | cons b bs =>
374    by_cases hg : g < 4
375    · rw [syncScan_cons_lt hg] at h; simp at h
376    · rw [syncScan_ge hg] at h; simp at h; exact ⟨h.symm, Or.inl hg⟩
377
378/-- **`syncsearch`, the loop on the heap.** For a pointer `buf = .ref r o` into a live array `a` with `len` readable
379bytes (`o + len ≤ |a|`) the call returns, without a fault and without changing the heap, the number of bytes
380consumed and the final `*have`, as the pure loop `syncScan` computes them on the bytes `a[o .. o + len)`. -/
381theorem syncsearch_run {h : Heap} {r : BRef} {a : Array UInt8} {o : Nat} {len : UInt32} (g : UInt32)
382    (hg : Space.get h r = some a) (hl : o + len.toNat ≤ a.size) :
383    syncsearch g (.ref r o) len h =
384      .ok ((UInt32.ofNat (syncScan g (syncBytes a o len)).2, (syncScan g (syncBytes a o len)).1), h) := by
385  have hL := syncBytes_length hl
386  have hlt := len.toNat_lt
387  generalize hR : syncScan g (syncBytes a o len) = R
388  obtain ⟨G, K⟩ := R
389  have hK : K ≤ len.toNat := by
390    have := syncScan_le g (syncBytes a o len); rw [hR] at this; simp at this; omega
391  let P : Nat → UInt32 × UInt32 → Prop := fun k s =>
392    s.1.toNat + k = K ∧ syncScan s.2 ((syncBytes a o len).drop s.1.toNat) = (G, k)
393  let Q : UInt32 × UInt32 → Prop := fun s => s.2 = G ∧ s.1.toNat = K
394  have key := cwhile_ok (h := h) (σ := UInt32 × UInt32)
395    (cond := fun (next, got) => pure (next < len && got < 4, (next, got)))
396    (body := fun (next, got) => do
397      let b ← index8 (.ref r o) next.toNat
398      let got := if b.toNat == (if got < 2 then 0 else 0xff) then got + 1 else if b != 0 then 0 else 4 - got
399      pure (next + 1, got)) P Q ?step ?stop (k := K) (s := (0, g)) ⟨by simp, by simpa using hR⟩ (by unfold fuel; omega)
400  · obtain ⟨⟨n, gg⟩, hs, hq⟩ := key
401    unfold syncsearch
402    have hs' : cwhile (σ := UInt32 × UInt32)
403        (fun (next, got) => pure (next < len && got < 4, (next, got)))
404        (fun (next, got) => do
405          let b ← index8 (.ref r o) next.toNat
406          let got := if b.toNat == (if got < 2 then 0 else 0xff) then got + 1 else if b != 0 then 0 else 4 - got
407          pure (next + 1, got)) (0, g) h = .ok ((n, gg), h) := hs
408    simp only [bind_app, pure_app]
409    rw [hs']
410    obtain ⟨h1, h2⟩ := hq
411    try simp only at h1 h2 ⊢
412    subst h1
413    have : n = UInt32.ofNat K := by rw [← h2]; simp
414    subst this
415    rfl
416  case step =>
417    intro k ⟨n, gg⟩ ⟨h1, h2⟩
418    simp only at h1 h2
419    have hn : n.toNat < len.toNat := by omega
420    have hd := syncBytes_drop hl n.toNat hn
421    have hg4 : gg < 4 := Classical.byContradiction fun hc => by
422      rw [syncScan_ge hc] at h2; simp at h2
423    rw [hd, syncScan_cons_lt hg4] at h2
424    simp at h2
425    refine ⟨(n, gg), (n + 1, syncStep gg a[o + n.toNat]), ?_, ?_, ?_⟩
426    · unfold OkOn; simp [UInt32.lt_iff_toNat_lt, hn, hg4]
427    · have hb : OkOn h (index8 (.ref r o) n.toNat) a[o + n.toNat] := Ptr.index_ok hg (by omega)
428      unfold OkOn at hb ⊢
429      simp only [bind_app, hb, pure_app, syncStep]
430    · have e : (n + 1).toNat = n.toNat + 1 := by
431        rw [UInt32.toNat_add]; simp; omega
432      show (n + 1).toNat + k = K ∧ syncScan (syncStep gg a[o + n.toNat]) ((syncBytes a o len).drop (n + 1).toNat) = (G, k)
433      rw [e]
434      exact ⟨by omega, Prod.ext h2.1 h2.2⟩
435  case stop =>
436    intro ⟨n, gg⟩ ⟨h1, h2⟩
437    try simp only at h1 h2
438    obtain ⟨hgG, hor⟩ := syncScan_zero h2
439    refine ⟨(n, gg), ?_, hgG.symm, by omega⟩
440    unfold OkOn
441    rcases hor with hg4 | hd
442    · simp [hg4]
443    · have : ¬ n.toNat < len.toNat := by
444        intro hl'
445        have := syncBytes_drop hl n.toNat hl'
446        rw [hd] at this; simp at this
447      simp [UInt32.lt_iff_toNat_lt, this]
448
449/-- **`syncsearch` on `NULL` with length 0.** The loop test fails at once, `buf` is never read; `*have` is unchanged. -/
450theorem syncsearch_null (g : UInt32) (h : Heap) : syncsearch g .null 0 h = .ok ((0, g), h) := by
451  have key := cwhile_ok (h := h) (σ := UInt32 × UInt32)
452    (cond := fun (next, got) => pure (next < 0 && got < 4, (next, got)))
453    (body := fun (next, got) => do
454      let b ← index8 .null next.toNat
455      let got := if b.toNat == (if got < 2 then 0 else 0xff) then got + 1 else if b != 0 then 0 else 4 - got
456      pure (next + 1, got)) (fun k s => k = 0 ∧ s = (0, g)) (fun s => s = (0, g))
457    (fun k s ⟨hk, _⟩ => by omega)
458    (fun s ⟨_, hs⟩ => ⟨s, by subst hs; unfold OkOn; simp [bind_app, pure_app], hs⟩)
459    (k := 0) (s := (0, g)) ⟨rfl, rfl⟩ (by unfold fuel; omega)
460  obtain ⟨s, hs, hq⟩ := key
461  subst hq
462  unfold syncsearch
463  simp only [bind_app, pure_app]
464  have hs' : cwhile (σ := UInt32 × UInt32)
465      (fun (next, got) => pure (next < 0 && got < 4, (next, got)))
466      (fun (next, got) => do
467        let b ← index8 .null next.toNat
468        let got := if b.toNat == (if got < 2 then 0 else 0xff) then got + 1 else if b != 0 then 0 else 4 - got
469        pure (next + 1, got)) (0, g) h = .ok ((0, g), h) := hs
470  rw [hs']
471
472theorem syncIn_length {h : Heap} {p : BPtr} {len : UInt32} {bs : List UInt8} (I : SyncIn h p len bs) :
473    bs.length = len.toNat := by
474  rcases I with ⟨b, a, o, rfl, hg, hl, rfl⟩ | ⟨rfl, rfl, rfl⟩
475  · exact syncBytes_length hl
476  · rfl
477
478/-- **`syncsearch`, specification.** Let `g` be the state after the bytes `w` (`SyncSt`; `g = 0` and `w = []` for the
479first call). On an input `buf[0 .. len)` (`SyncIn`) the call never faults, does not change the heap, and returns the
480number `N` of bytes consumed and the new `*have` `G`:
481* `G = 4`: the pattern `00 00 FF FF` was found, `N > 0`, it ends `w ++ buf[0 .. N)` and does not occur in `w ++ buf[0 .. N')` for
482  `N' < N` (the first occurrence), and `N ≤ len`;
483* `G ≠ 4`: all `len` bytes were consumed and `G` is the state after `w ++ buf[0 .. len)` (the longest proper prefix of
484  the pattern that ends the input): the pattern has not occurred and a later call carries on from `G`. -/
485theorem syncsearch_spec {h : Heap} {p : BPtr} {len : UInt32} {bs : List UInt8} (I : SyncIn h p len bs)
486    {g : UInt32} {w : List UInt8} (hs : SyncSt g w) :
487    ∃ N G, syncsearch g p len h = .ok ((N, G), h) ∧ N.toNat ≤ len.toNat ∧
488      (G = 4 → 0 < N.toNat ∧ syncPat <:+ w ++ bs.take N.toNat ∧ ∀ L', L' < N.toNat → ¬ syncPat <:+: w ++ bs.take L') ∧
489      (G ≠ 4 → N = len ∧ SyncSt G (w ++ bs)) := by
490  have hlen := syncIn_length I
491  rcases I with ⟨b, a, o, rfl, hg, hl, rfl⟩ | ⟨rfl, rfl, rfl⟩
492  · refine ⟨UInt32.ofNat (syncScan g (syncBytes a o len)).2, (syncScan g (syncBytes a o len)).1,
493      syncsearch_run (r := .blk b) g hg hl, ?_⟩
494    obtain ⟨h1, h2, h3⟩ := syncScan_spec hs (syncBytes a o len) rfl
495    have hn : (UInt32.ofNat (syncScan g (syncBytes a o len)).2).toNat = (syncScan g (syncBytes a o len)).2 := by
496      have := len.toNat_lt
497      rw [UInt32.toNat_ofNat_of_lt' (by simp [UInt32.size]; omega)]
498    rw [hn]
499    refine ⟨by omega, h2, fun hne => ?_⟩
500    obtain ⟨e, st⟩ := h3 hne
501    refine ⟨?_, st⟩
502    apply UInt32.toNat_inj.mp; rw [hn]; omega
503  · refine ⟨0, g, syncsearch_null g h, by simp, ?_, ?_⟩
504    · intro h4
505      have := hs.1; rw [h4] at this; exact absurd this (by decide)
506    · intro _; exact ⟨rfl, by simpa using hs⟩
507
508end Zlib.Inflate.Proofs