inffast.c.copy.lean

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

1import ZlibF.Proof.«inffast.c.step1»
2
3namespace Zlib.Inffast.Proofs
4open C Zlib.Inffast Zlib.Inffast.Spec
5
6/-! ### Copying bytes: the pure array functions -/
7
8/-- `k` bytes copied from the fixed array `S` (offset `fo`) into `A` (offset `oo`), one at a time. -/
9def blitN (S : Array UInt8) : Nat → Nat → Nat → Array UInt8 → Array UInt8
10  | 0, _, _, A => A
11  | k + 1, fo, oo, A => blitN S k (fo + 1) (oo + 1) (A.set! oo (S.getD fo 0))
12
13/-- `k` bytes copied inside `A` from offset `fo` to offset `oo`, one at a time (the source may be written meanwhile). -/
14def cpyN : Nat → Nat → Nat → Array UInt8 → Array UInt8
15  | 0, _, _, A => A
16  | k + 1, fo, oo, A => cpyN k (fo + 1) (oo + 1) (A.set! oo (A.getD fo 0))
17
18theorem blitN_size (S : Array UInt8) : ∀ k fo oo A, (blitN S k fo oo A).size = A.size
19  | 0, _, _, _ => rfl
20  | k + 1, fo, oo, A => by simp [blitN, blitN_size S k]
21
22theorem cpyN_size : ∀ k fo oo (A : Array UInt8), (cpyN k fo oo A).size = A.size
23  | 0, _, _, _ => rfl
24  | k + 1, fo, oo, A => by simp [cpyN, cpyN_size k]
25
26theorem blitN_add (S : Array UInt8) : ∀ k1 k2 fo oo A,
27    blitN S (k1 + k2) fo oo A = blitN S k2 (fo + k1) (oo + k1) (blitN S k1 fo oo A)
28  | 0, k2, fo, oo, A => by simp [blitN]
29  | k1 + 1, k2, fo, oo, A => by
30    have := blitN_add S k1 k2 (fo + 1) (oo + 1) (A.set! oo (S.getD fo 0))
31    rw [show k1 + 1 + k2 = (k1 + k2) + 1 by omega]
32    simp only [blitN]
33    rw [this]
34    simp [Nat.add_assoc, Nat.add_comm 1 k1]
35
36theorem cpyN_add : ∀ k1 k2 fo oo (A : Array UInt8),
37    cpyN (k1 + k2) fo oo A = cpyN k2 (fo + k1) (oo + k1) (cpyN k1 fo oo A)
38  | 0, k2, fo, oo, A => by simp [cpyN]
39  | k1 + 1, k2, fo, oo, A => by
40    have := cpyN_add k1 k2 (fo + 1) (oo + 1) (A.set! oo (A.getD fo 0))
41    rw [show k1 + 1 + k2 = (k1 + k2) + 1 by omega]
42    simp only [cpyN]
43    rw [this]
44    simp [Nat.add_assoc, Nat.add_comm 1 k1]
45
46variable (e : Env)
47
48/-- Writing the output block of `e.heap A` gives `e.heap A'`. -/
49theorem Env.heap_put (A A' : Array UInt8) (msg m) :
50    Space.put (e.heap A msg m) (BRef.blk e.ob) A' = e.heap A' msg m := by
51  rw [BRef.put_blk]
52  unfold Env.heap
53  rw [put_bytes_comm]
54  simp only [put_bytes, upd_upd]
55
56/-- `*out++ = *from++;` on the heap `e.heap A msg m`, the source block `fb` holding `S`. -/
57theorem copy1_run (A S : Array UInt8) (msg : BPtr) (m : UInt32) (l : L) (fb fo oo : Nat)
58    (hf : l.from_ = .ref (BRef.blk fb) fo) (ho : l.out = .ref (BRef.blk e.ob) oo)
59    (hSg : (e.heap A msg m).bytes fb = some S) (hfo : fo < S.size) (hoo : oo < A.size) :
60    copy1 l (e.heap A msg m) = .ok ({ l with from_ := .ref (BRef.blk fb) (fo + 1), out := .ref (BRef.blk e.ob) (oo + 1) },
61      e.heap (A.set! oo (S.getD fo 0)) msg m) := by
62  have hAg : Space.get (e.heap A msg m) (BRef.blk e.ob) = some A := e.heap_bytes_ob A msg m
63  have hSg' : Space.get (e.heap A msg m) (BRef.blk fb) = some S := hSg
64  have hSd : S.getD fo 0 = S[fo] := by simp [Array.getD_eq_getD_getElem?, hfo]
65  have hst : store8 (Ptr.ref (BRef.blk e.ob) oo) S[fo] (e.heap A msg m) =
66      .ok ((), e.heap (A.set! oo S[fo]) msg m) := by
67    rw [← e.heap_put A (A.set! oo S[fo]) msg m]
68    exact Ptr.store_ok hAg (e.heap_ro_ob A msg m) hoo
69  have hsz : (A.set! oo S[fo]).size = A.size := by simp
70  have hAg2 : Space.get (e.heap (A.set! oo S[fo]) msg m) (BRef.blk e.ob) = some (A.set! oo S[fo]) :=
71    e.heap_bytes_ob _ msg m
72  have hadd := Ptr.add_nat_ok (h := e.heap A msg m) (r := BRef.blk fb) (a := S) (off := fo) (n := 1) hSg' (by omega)
73  have hadd2 := Ptr.add_nat_ok (h := e.heap (A.set! oo S[fo]) msg m) (r := BRef.blk e.ob) (a := A.set! oo S[fo])
74    (off := oo) (n := 1) hAg2 (by omega)
75  unfold copy1
76  rw [hf, ho, bind_ok (Ptr.load_ok hSg' hfo), bind_ok (by exact hadd), bind_ok hst,
77    bind_ok (by exact hadd2), hSd]
78  rfl
79
80
81theorem u32_sub_one_toNat {x : UInt32} (h : 1 ≤ x.toNat) : (x - 1).toNat = x.toNat - 1 :=
82  u32_toNat_sub (by simpa using h)
83
84theorem u32_sub_one_ne {x : UInt32} (h : 2 ≤ x.toNat) : ((x - 1) != 0) = true := by
85  have := u32_sub_one_toNat (x := x) (by omega)
86  simp only [bne_iff_ne, ne_eq]
87  intro h0
88  rw [h0] at this
89  simp at this
90  omega
91
92theorem u32_sub_one_eq {x : UInt32} (h : x.toNat = 1) : ((x - 1) != 0) = false := by
93  have := u32_sub_one_toNat (x := x) (by omega)
94  have h0 : x - 1 = 0 := by
95    apply UInt32.toNat_inj.mp
96    simp [this, h]
97  simp [h0]
98
99/-- `do { *out++ = *from++; } while (--op);` copying from a block `fb` other than the output block. -/
100theorem copyOp_win_go (A S : Array UInt8) (msg : BPtr) (m : UInt32) (fb : Nat) (hfb : fb ≠ e.ob)
101    (hSg : e.h0.bytes fb = some S) :
102    ∀ n (l : L) (fo oo : Nat) (A : Array UInt8) (fu : Nat), l.op.toNat = n + 1 → n ≤ fu →
103      l.from_ = .ref (BRef.blk fb) fo → l.out = .ref (BRef.blk e.ob) oo → fo + n + 1 ≤ S.size → oo + n + 1 ≤ A.size →
104      cdoWhile.go copy1 (fun l => let op := l.op - 1; pure (op != 0, { l with op })) (fu + 1) l (e.heap A msg m) =
105        .ok ({ l with from_ := .ref (BRef.blk fb) (fo + n + 1), out := .ref (BRef.blk e.ob) (oo + n + 1), op := 0 },
106          e.heap (blitN S (n + 1) fo oo A) msg m) := by
107  intro n
108  induction n with
109  | zero =>
110    intro l fo oo A fu hop _ hf ho hfo hoo
111    have hS : (e.heap A msg m).bytes fb = some S := by rw [e.heap_bytes_ne A msg m hfb]; exact hSg
112    simp only [cdoWhile.go, bind_app]
113    rw [copy1_run e A S msg m l fb fo oo hf ho hS (by omega) (by omega)]
114    simp only [pure_app]
115    have h1 : (l.op - 1 != 0) = false := u32_sub_one_eq (by omega)
116    have h0 : l.op - 1 = 0 := by
117      apply UInt32.toNat_inj.mp
118      simp [u32_sub_one_toNat (x := l.op) (by omega), hop]
119    simp [h1, h0, blitN]
120  | succ n ih =>
121    intro l fo oo A fu hop hfu hf ho hfo hoo
122    obtain ⟨fu, rfl⟩ : ∃ fu', fu = fu' + 1 := ⟨fu - 1, by omega⟩
123    have hS : (e.heap A msg m).bytes fb = some S := by rw [e.heap_bytes_ne A msg m hfb]; exact hSg
124    rw [cdoWhile.go]
125    simp only [bind_app]
126    rw [copy1_run e A S msg m l fb fo oo hf ho hS (by omega) (by omega)]
127    simp only [pure_app]
128    have h1 : (l.op - 1 != 0) = true := u32_sub_one_ne (by omega)
129    simp only [h1, ite_true]
130    have hop1 : (l.op - 1).toNat = n + 1 := by rw [u32_sub_one_toNat (by omega)]; omega
131    rw [ih { l with from_ := Ptr.ref (BRef.blk fb) (fo + 1), out := Ptr.ref (BRef.blk e.ob) (oo + 1), op := l.op - 1 }
132      (fo + 1) (oo + 1) (A.set! oo (S.getD fo 0)) fu hop1 (by omega) rfl rfl (by omega) (by simp; omega)]
133    have h0 : (0 : Nat) = 0 := rfl
134    simp [blitN, Nat.add_assoc, Nat.add_comm 1 n]
135
136theorem fuel_pred : fuel - 1 + 1 = fuel := by unfold fuel; omega
137
138/-- `do { *out++ = *from++; } while (--op);` with `op = n ≥ 1`, from a block other than the output block. -/
139theorem copyOp_win (S : Array UInt8) (msg : BPtr) (m : UInt32) (fb : Nat) (hfb : fb ≠ e.ob)
140    (hSg : e.h0.bytes fb = some S) (A : Array UInt8) (l : L) (n fo oo : Nat) (hop : l.op.toNat = n) (hn : 1 ≤ n)
141    (hf : l.from_ = .ref (BRef.blk fb) fo) (ho : l.out = .ref (BRef.blk e.ob) oo)
142    (hfo : fo + n ≤ S.size) (hoo : oo + n ≤ A.size) :
143    copyOp l (e.heap A msg m) = .ok ({ l with from_ := .ref (BRef.blk fb) (fo + n), out := .ref (BRef.blk e.ob) (oo + n), op := 0 },
144      e.heap (blitN S n fo oo A) msg m) := by
145  obtain ⟨n, rfl⟩ : ∃ k, n = k + 1 := ⟨n - 1, by omega⟩
146  have hlt := UInt32.toNat_lt l.op
147  have key := copyOp_win_go e A S msg m fb hfb hSg n l fo oo A (fuel - 1) (by omega) (by unfold fuel; omega) hf ho
148    (by omega) (by omega)
149  rw [fuel_pred] at key
150  unfold copyOp cdoWhile
151  rw [key]
152  simp [Nat.add_assoc]
153
154/-- The same, copying inside the output block. -/
155theorem copyOp_out_go : ∀ n (l : L) (fo oo : Nat) (A : Array UInt8) (msg : BPtr) (m : UInt32) (fu : Nat),
156    l.op.toNat = n + 1 → n ≤ fu →
157    l.from_ = .ref (BRef.blk e.ob) fo → l.out = .ref (BRef.blk e.ob) oo → fo + n + 1 ≤ A.size → oo + n + 1 ≤ A.size →
158    cdoWhile.go copy1 (fun l => let op := l.op - 1; pure (op != 0, { l with op })) (fu + 1) l (e.heap A msg m) =
159      .ok ({ l with from_ := .ref (BRef.blk e.ob) (fo + n + 1), out := .ref (BRef.blk e.ob) (oo + n + 1), op := 0 },
160        e.heap (cpyN (n + 1) fo oo A) msg m) := by
161  intro n
162  induction n with
163  | zero =>
164    intro l fo oo A msg m fu hop _ hf ho hfo hoo
165    have hS : (e.heap A msg m).bytes e.ob = some A := e.heap_bytes_ob A msg m
166    simp only [cdoWhile.go, bind_app]
167    rw [copy1_run e A A msg m l e.ob fo oo hf ho hS (by omega) (by omega)]
168    simp only [pure_app]
169    have h1 : (l.op - 1 != 0) = false := u32_sub_one_eq (by omega)
170    have h0 : l.op - 1 = 0 := by
171      apply UInt32.toNat_inj.mp
172      simp [u32_sub_one_toNat (x := l.op) (by omega), hop]
173    simp [h0, cpyN]
174  | succ n ih =>
175    intro l fo oo A msg m fu hop hfu hf ho hfo hoo
176    obtain ⟨fu, rfl⟩ : ∃ fu', fu = fu' + 1 := ⟨fu - 1, by omega⟩
177    have hS : (e.heap A msg m).bytes e.ob = some A := e.heap_bytes_ob A msg m
178    rw [cdoWhile.go]
179    simp only [bind_app]
180    rw [copy1_run e A A msg m l e.ob fo oo hf ho hS (by omega) (by omega)]
181    simp only [pure_app]
182    have h1 : (l.op - 1 != 0) = true := u32_sub_one_ne (by omega)
183    simp only [h1, ite_true]
184    have hop1 : (l.op - 1).toNat = n + 1 := by rw [u32_sub_one_toNat (by omega)]; omega
185    rw [ih { l with from_ := Ptr.ref (BRef.blk e.ob) (fo + 1), out := Ptr.ref (BRef.blk e.ob) (oo + 1), op := l.op - 1 }
186      (fo + 1) (oo + 1) (A.set! oo (A.getD fo 0)) msg m fu hop1 (by omega) rfl rfl (by simp; omega) (by simp; omega)]
187    simp [cpyN, Nat.add_assoc, Nat.add_comm 1 n]
188
189theorem copyOp_out (A : Array UInt8) (msg : BPtr) (m : UInt32) (l : L) (n fo oo : Nat) (hop : l.op.toNat = n)
190    (hn : 1 ≤ n) (hf : l.from_ = .ref (BRef.blk e.ob) fo) (ho : l.out = .ref (BRef.blk e.ob) oo)
191    (hfo : fo + n ≤ A.size) (hoo : oo + n ≤ A.size) :
192    copyOp l (e.heap A msg m) = .ok ({ l with from_ := .ref (BRef.blk e.ob) (fo + n), out := .ref (BRef.blk e.ob) (oo + n), op := 0 },
193      e.heap (cpyN n fo oo A) msg m) := by
194  obtain ⟨n, rfl⟩ : ∃ k, n = k + 1 := ⟨n - 1, by omega⟩
195  have hlt := UInt32.toNat_lt l.op
196  have key := copyOp_out_go e n l fo oo A msg m (fuel - 1) (by omega) (by unfold fuel; omega) hf ho (by omega) (by omega)
197  rw [fuel_pred] at key
198  unfold copyOp cdoWhile
199  rw [key]
200  simp [Nat.add_assoc]
201
202
203/-! ### The tail of a match copy, for either source -/
204
205/-- `k` bytes copied from `sel A` (offset `fo`) into `A` (offset `oo`), one at a time; `sel` is the identity when the
206source is the output block (it changes as the copy goes) and a constant when it is the window. -/
207def cpyG (sel : Array UInt8 → Array UInt8) : Nat → Nat → Nat → Array UInt8 → Array UInt8
208  | 0, _, _, A => A
209  | k + 1, fo, oo, A => cpyG sel k (fo + 1) (oo + 1) (A.set! oo ((sel A).getD fo 0))
210
211theorem cpyG_size (sel : Array UInt8 → Array UInt8) : ∀ k fo oo (A : Array UInt8), (cpyG sel k fo oo A).size = A.size
212  | 0, _, _, _ => rfl
213  | k + 1, fo, oo, A => by simp [cpyG, cpyG_size sel k]
214
215theorem cpyG_add (sel : Array UInt8 → Array UInt8) : ∀ k1 k2 fo oo (A : Array UInt8),
216    cpyG sel (k1 + k2) fo oo A = cpyG sel k2 (fo + k1) (oo + k1) (cpyG sel k1 fo oo A)
217  | 0, k2, fo, oo, A => by simp [cpyG]
218  | k1 + 1, k2, fo, oo, A => by
219    have := cpyG_add sel k1 k2 (fo + 1) (oo + 1) (A.set! oo ((sel A).getD fo 0))
220    rw [show k1 + 1 + k2 = (k1 + k2) + 1 by omega]
221    simp only [cpyG]
222    rw [this]
223    simp [Nat.add_assoc, Nat.add_comm 1 k1]
224
225theorem cpyG_id : ∀ k fo oo (A : Array UInt8), cpyG id k fo oo A = cpyN k fo oo A
226  | 0, _, _, _ => rfl
227  | k + 1, fo, oo, A => by simp [cpyG, cpyN, cpyG_id k]
228
229theorem cpyG_const (S : Array UInt8) : ∀ k fo oo (A : Array UInt8), cpyG (fun _ => S) k fo oo A = blitN S k fo oo A
230  | 0, _, _, _ => rfl
231  | k + 1, fo, oo, A => by simp [cpyG, blitN, cpyG_const S k]
232
233/-- The source block `fb` holds `sel A` while the output block holds `A`. -/
234structure Src (fb : Nat) (sel : Array UInt8 → Array UInt8) : Prop where
235  get : ∀ A msg m, (e.heap A msg m).bytes fb = some (sel A)
236  size : ∀ (A : Array UInt8) i x, (sel (A.set! i x)).size = (sel A).size
237
238theorem Src.out : Src e e.ob id :=
239  ⟨fun A msg m => e.heap_bytes_ob A msg m, fun A i x => by simp⟩
240
241theorem Src.win (fb : Nat) (S : Array UInt8) (hfb : fb ≠ e.ob) (hS : e.h0.bytes fb = some S) :
242    Src e fb (fun _ => S) :=
243  ⟨fun A msg m => by rw [e.heap_bytes_ne A msg m hfb]; exact hS, fun _ _ _ => rfl⟩
244
245variable {e}
246
247theorem copy1_src {fb : Nat} {sel : Array UInt8 → Array UInt8} (hs : Src e fb sel) (A : Array UInt8) (msg : BPtr)
248    (m : UInt32) (l : L) (fo oo : Nat) (hf : l.from_ = .ref (BRef.blk fb) fo) (ho : l.out = .ref (BRef.blk e.ob) oo)
249    (hfo : fo < (sel A).size) (hoo : oo < A.size) :
250    copy1 l (e.heap A msg m) = .ok ({ l with from_ := .ref (BRef.blk fb) (fo + 1), out := .ref (BRef.blk e.ob) (oo + 1) },
251      e.heap (A.set! oo ((sel A).getD fo 0)) msg m) :=
252  copy1_run e A (sel A) msg m l fb fo oo hf ho (hs.get A msg m) hfo hoo
253
254/-- `if (len) { *out++ = *from++; if (len > 1) *out++ = *from++; }` -/
255def tailIf (l : L) : M L := do
256  let mut l := l
257  if l.len != 0 then
258    l ← copy1 l
259    if l.len > 1 then l ← copy1 l
260  pure l
261
262/-- The condition `len > 2`. -/
263def cond3 (l : L) : M (Bool × L) := pure (l.len > 2, l)
264
265/-- The body `*out++ = *from++;` three times and `len -= 3;`. -/
266def body3 (l : L) : M L := do
267  let l ← copy1 l
268  let l ← copy1 l
269  let l ← copy1 l
270  pure { l with len := l.len - 3 }
271
272/-- Three copies in a row (the body of the unrolled loop, without `len -= 3`). -/
273theorem copy3_src {fb : Nat} {sel : Array UInt8 → Array UInt8} (hs : Src e fb sel) (A : Array UInt8) (msg : BPtr)
274    (m : UInt32) (l : L) (fo oo : Nat) (hf : l.from_ = .ref (BRef.blk fb) fo) (ho : l.out = .ref (BRef.blk e.ob) oo)
275    (hfo : fo + 3 ≤ (sel A).size) (hoo : oo + 3 ≤ A.size) :
276    body3 l (e.heap A msg m) =
277      .ok ({ l with from_ := .ref (BRef.blk fb) (fo + 3), out := .ref (BRef.blk e.ob) (oo + 3), len := l.len - 3 },
278        e.heap (cpyG sel 3 fo oo A) msg m) := by
279  have hsz : ∀ (B : Array UInt8) i x, (sel (B.set! i x)).size = (sel B).size := hs.size
280  unfold body3
281  rw [bind_ok (copy1_src hs A msg m l fo oo hf ho (by omega) (by omega))]
282  rw [bind_ok (copy1_src hs (A.set! oo ((sel A).getD fo 0)) msg m _ (fo + 1) (oo + 1) rfl rfl
283    (by rw [hsz]; omega) (by simp; omega))]
284  rw [bind_ok (copy1_src hs (A.set! oo ((sel A).getD fo 0) |>.set! (oo + 1) ((sel (A.set! oo ((sel A).getD fo 0))).getD (fo + 1) 0))
285    msg m _ (fo + 2) (oo + 2) rfl rfl (by rw [hsz, hsz]; omega) (by simp; omega))]
286  simp only [pure_app, cpyG]
287
288
289/-- `while (len > 2) { three copies; len -= 3; }` followed by `tailIf`. -/
290def tailW (l : L) : M L := do
291  let l ← cwhile cond3 body3 l
292  tailIf l
293
294/-- `do { three copies; len -= 3; } while (len > 2);` followed by `tailIf`. -/
295def tailD (l : L) : M L := do
296  let l ← cdoWhile body3 cond3 l
297  tailIf l
298
299theorem tailIf_run {fb : Nat} {sel : Array UInt8 → Array UInt8} (hs : Src e fb sel) (A : Array UInt8) (msg : BPtr)
300    (m : UInt32) (l : L) (r fo oo : Nat) (hr : l.len.toNat = r) (hr2 : r < 3)
301    (hf : l.from_ = .ref (BRef.blk fb) fo) (ho : l.out = .ref (BRef.blk e.ob) oo)
302    (hfo : fo + r ≤ (sel A).size) (hoo : oo + r ≤ A.size) :
303    tailIf l (e.heap A msg m) = .ok ({ l with from_ := .ref (BRef.blk fb) (fo + r), out := .ref (BRef.blk e.ob) (oo + r) },
304      e.heap (cpyG sel r fo oo A) msg m) := by
305  have hsz : ∀ (B : Array UInt8) i x, (sel (B.set! i x)).size = (sel B).size := hs.size
306  unfold tailIf
307  by_cases h0 : r = 0
308  · subst h0
309    have hl : l.len = 0 := by apply UInt32.toNat_inj.mp; simpa using hr
310    simp only [hl, bne_self_eq_false, Bool.false_eq_true, ite_false, pure_app, cpyG, Nat.add_zero]
311    rcases l with ⟨i1, o1, h1, b1, he1, op1, ln1, d1, f1, br1, al1, ad1⟩
312    simp only at hf ho hl ⊢
313    subst hf ho hl
314    rfl
315  · have hne : (l.len != 0) = true := by
316      simp only [bne_iff_ne, ne_eq]
317      intro h; rw [h] at hr; simp at hr; omega
318    simp only [hne, ite_true]
319    rw [bind_ok (copy1_src hs A msg m l fo oo hf ho (by omega) (by omega))]
320    dsimp only
321    by_cases h1 : r = 1
322    · subst h1
323      have hgt : ¬ (l.len > 1) := by
324        intro h; have := (UInt32.lt_iff_toNat_lt.mp h); simp at this; omega
325      simp only [hgt, ite_false, pure_app, cpyG]
326    · have h2 : r = 2 := by omega
327      subst h2
328      have hgt : (l.len > 1) := by
329        apply UInt32.lt_iff_toNat_lt.mpr; simp; omega
330      simp only [hgt, ite_true]
331      rw [bind_ok (copy1_src hs (A.set! oo ((sel A).getD fo 0)) msg m _ (fo + 1) (oo + 1) rfl rfl
332        (by rw [hsz]; omega) (by simp; omega))]
333      simp only [pure_app, cpyG]
334
335
336theorem len_gt2_iff (x : UInt32) : decide (x > 2) = decide (2 < x.toNat) := by
337  by_cases h : x > 2
338  · have := UInt32.lt_iff_toNat_lt.mp h; simp at this; simp [h]; omega
339  · have : ¬ (2 < x.toNat) := fun h2 => h (UInt32.lt_iff_toNat_lt.mpr (by simpa using h2))
340    simp [h, this]
341
342theorem len_sub3 {x : UInt32} (h : 3 ≤ x.toNat) : (x - 3).toNat = x.toNat - 3 :=
343  u32_toNat_sub (by simpa using h)
344
345theorem Src.sel_cpyG {fb : Nat} {sel : Array UInt8 → Array UInt8} (hs : Src e fb sel) :
346    ∀ k fo oo (A : Array UInt8), (sel (cpyG sel k fo oo A)).size = (sel A).size
347  | 0, _, _, _ => rfl
348  | k + 1, fo, oo, A => by
349    simp only [cpyG]
350    rw [Src.sel_cpyG hs k, hs.size]
351
352theorem cond3_true {l : L} (h : 3 ≤ l.len.toNat) (hp : Heap) : cond3 l hp = .ok ((true, l), hp) := by
353  have hd : decide (l.len > 2) = true := by rw [len_gt2_iff]; simp; omega
354  simp [cond3, hd]
355
356theorem cond3_false {l : L} (h : l.len.toNat ≤ 2) (hp : Heap) : cond3 l hp = .ok ((false, l), hp) := by
357  have hd : decide (l.len > 2) = false := by rw [len_gt2_iff]; simp; omega
358  simp [cond3, hd]
359
360theorem whileTail_go {fb : Nat} {sel : Array UInt8 → Array UInt8} (hs : Src e fb sel) (msg : BPtr) (m : UInt32) :
361    ∀ q (l : L) fo oo (A : Array UInt8) fu r, r < 3 → l.len.toNat = 3 * q + r → q ≤ fu →
362      l.from_ = .ref (BRef.blk fb) fo → l.out = .ref (BRef.blk e.ob) oo →
363      fo + 3 * q ≤ (sel A).size → oo + 3 * q ≤ A.size →
364      cwhile.go cond3 body3 (fu + 1) l (e.heap A msg m) =
365        .ok ({ l with from_ := .ref (BRef.blk fb) (fo + 3 * q), out := .ref (BRef.blk e.ob) (oo + 3 * q),
366                      len := UInt32.ofNat r }, e.heap (cpyG sel (3 * q) fo oo A) msg m) := by
367  intro q
368  induction q with
369  | zero =>
370    intro l fo oo A fu r hr hl _ hf ho _ _
371    rw [cwhile.go, bind_ok (cond3_false (by omega) _)]
372    simp only [Bool.false_eq_true, ite_false, pure_app, cpyG, Nat.mul_zero, Nat.add_zero]
373    have hlen : l.len = UInt32.ofNat r := by
374      apply UInt32.toNat_inj.mp; simp [UInt32.toNat_ofNat, Nat.mod_eq_of_lt (show r < 2 ^ 32 by omega)]; omega
375    rcases l with ⟨i1, o1, h1, b1, he1, op1, ln1, d1, f1, br1, al1, ad1⟩
376    simp only at hf ho hlen ⊢
377    subst hf ho hlen
378    rfl
379  | succ q ih =>
380    intro l fo oo A fu r hr hl hfu hf ho hfo hoo
381    obtain ⟨fu, rfl⟩ : ∃ fu', fu = fu' + 1 := ⟨fu - 1, by omega⟩
382    rw [cwhile.go, bind_ok (cond3_true (by omega) _)]
383    simp only [ite_true]
384    rw [bind_ok (copy3_src hs A msg m l fo oo hf ho (by omega) (by omega))]
385    have hl3 : (l.len - 3).toNat = 3 * q + r := by rw [len_sub3 (by omega)]; omega
386    rw [ih { l with from_ := Ptr.ref (BRef.blk fb) (fo + 3), out := Ptr.ref (BRef.blk e.ob) (oo + 3), len := l.len - 3 }
387      (fo + 3) (oo + 3) (cpyG sel 3 fo oo A) fu r hr hl3 (by omega) rfl rfl
388      (by rw [hs.sel_cpyG]; omega) (by rw [cpyG_size]; omega)]
389    have e1 : fo + 3 + 3 * q = fo + 3 * (q + 1) := by omega
390    have e2 : oo + 3 + 3 * q = oo + 3 * (q + 1) := by omega
391    have e3 : cpyG sel (3 * q) (fo + 3) (oo + 3) (cpyG sel 3 fo oo A) = cpyG sel (3 * (q + 1)) fo oo A := by
392      rw [show 3 * (q + 1) = 3 + 3 * q by omega, cpyG_add]
393    rw [e1, e2, e3]
394
395
396theorem tailW_run {fb : Nat} {sel : Array UInt8 → Array UInt8} (hs : Src e fb sel) (A : Array UInt8) (msg : BPtr)
397    (m : UInt32) (l : L) (n fo oo : Nat) (hn : l.len.toNat = n) (hf : l.from_ = .ref (BRef.blk fb) fo)
398    (ho : l.out = .ref (BRef.blk e.ob) oo) (hfo : fo + n ≤ (sel A).size) (hoo : oo + n ≤ A.size) :
399    tailW l (e.heap A msg m) = .ok ({ l with from_ := .ref (BRef.blk fb) (fo + n), out := .ref (BRef.blk e.ob) (oo + n), len := UInt32.ofNat (n % 3) }, e.heap (cpyG sel n fo oo A) msg m) := by
400  have hlt := UInt32.toNat_lt l.len
401  have key := whileTail_go hs msg m (n / 3) l fo oo A (fuel - 1) (n % 3) (by omega) (by omega) (by unfold fuel; omega)
402    hf ho (by omega) (by omega)
403  rw [fuel_pred] at key
404  unfold tailW cwhile
405  rw [bind_ok key]
406  have hr : (UInt32.ofNat (n % 3)).toNat = n % 3 := by simp [UInt32.toNat_ofNat]; omega
407  have hn3 : n = 3 * (n / 3) + n % 3 := by omega
408  rw [tailIf_run hs (cpyG sel (3 * (n / 3)) fo oo A) msg m _ (n % 3) (fo + 3 * (n / 3)) (oo + 3 * (n / 3)) hr
409    (by omega) rfl rfl (by rw [hs.sel_cpyG]; omega) (by rw [cpyG_size]; omega)]
410  have e1 : fo + 3 * (n / 3) + n % 3 = fo + n := by omega
411  have e2 : oo + 3 * (n / 3) + n % 3 = oo + n := by omega
412  have e3 : cpyG sel (n % 3) (fo + 3 * (n / 3)) (oo + 3 * (n / 3)) (cpyG sel (3 * (n / 3)) fo oo A) = cpyG sel n fo oo A := by
413    conv => rhs; rw [hn3, cpyG_add]
414  rw [e1, e2, e3]
415
416theorem doTail_go {fb : Nat} {sel : Array UInt8 → Array UInt8} (hs : Src e fb sel) (msg : BPtr) (m : UInt32) :
417    ∀ q (l : L) fo oo (A : Array UInt8) fu r, r < 3 → l.len.toNat = 3 * (q + 1) + r → q ≤ fu →
418      l.from_ = .ref (BRef.blk fb) fo → l.out = .ref (BRef.blk e.ob) oo →
419      fo + 3 * (q + 1) ≤ (sel A).size → oo + 3 * (q + 1) ≤ A.size →
420      cdoWhile.go body3 cond3 (fu + 1) l (e.heap A msg m) =
421        .ok ({ l with from_ := .ref (BRef.blk fb) (fo + 3 * (q + 1)), out := .ref (BRef.blk e.ob) (oo + 3 * (q + 1)), len := UInt32.ofNat r }, e.heap (cpyG sel (3 * (q + 1)) fo oo A) msg m) := by
422  intro q
423  induction q with
424  | zero =>
425    intro l fo oo A fu r hr hl _ hf ho hfo hoo
426    rw [cdoWhile.go, bind_ok (copy3_src hs A msg m l fo oo hf ho (by omega) (by omega))]
427    have hl3 : (l.len - 3).toNat = r := by rw [len_sub3 (by omega)]; omega
428    rw [bind_ok (cond3_false (l := { l with from_ := Ptr.ref (BRef.blk fb) (fo + 3), out := Ptr.ref (BRef.blk e.ob) (oo + 3), len := l.len - 3 }) (by simp; omega) _)]
429    simp only [Bool.false_eq_true, ite_false, pure_app, cpyG]
430    have hlen : l.len - 3 = UInt32.ofNat r := by
431      apply UInt32.toNat_inj.mp; simp [UInt32.toNat_ofNat, Nat.mod_eq_of_lt (show r < 2 ^ 32 by omega)]; omega
432    simp [hlen]
433  | succ q ih =>
434    intro l fo oo A fu r hr hl hfu hf ho hfo hoo
435    obtain ⟨fu, rfl⟩ : ∃ fu', fu = fu' + 1 := ⟨fu - 1, by omega⟩
436    rw [cdoWhile.go, bind_ok (copy3_src hs A msg m l fo oo hf ho (by omega) (by omega))]
437    have hl3 : (l.len - 3).toNat = 3 * (q + 1) + r := by rw [len_sub3 (by omega)]; omega
438    rw [bind_ok (cond3_true (l := { l with from_ := Ptr.ref (BRef.blk fb) (fo + 3), out := Ptr.ref (BRef.blk e.ob) (oo + 3), len := l.len - 3 }) (by simp; omega) _)]
439    simp only [ite_true]
440    rw [ih { l with from_ := Ptr.ref (BRef.blk fb) (fo + 3), out := Ptr.ref (BRef.blk e.ob) (oo + 3), len := l.len - 3 }
441      (fo + 3) (oo + 3) (cpyG sel 3 fo oo A) fu r hr hl3 (by omega) rfl rfl
442      (by rw [hs.sel_cpyG]; omega) (by rw [cpyG_size]; omega)]
443    have e1 : fo + 3 + 3 * (q + 1) = fo + 3 * (q + 1 + 1) := by omega
444    have e2 : oo + 3 + 3 * (q + 1) = oo + 3 * (q + 1 + 1) := by omega
445    have e3 : cpyG sel (3 * (q + 1)) (fo + 3) (oo + 3) (cpyG sel 3 fo oo A) = cpyG sel (3 * (q + 1 + 1)) fo oo A := by
446      rw [show 3 * (q + 1 + 1) = 3 + 3 * (q + 1) by omega, cpyG_add]
447    rw [e1, e2, e3]
448
449theorem tailD_run {fb : Nat} {sel : Array UInt8 → Array UInt8} (hs : Src e fb sel) (A : Array UInt8) (msg : BPtr)
450    (m : UInt32) (l : L) (n fo oo : Nat) (hn : l.len.toNat = n) (h3 : 3 ≤ n) (hf : l.from_ = .ref (BRef.blk fb) fo)
451    (ho : l.out = .ref (BRef.blk e.ob) oo) (hfo : fo + n ≤ (sel A).size) (hoo : oo + n ≤ A.size) :
452    tailD l (e.heap A msg m) = .ok ({ l with from_ := .ref (BRef.blk fb) (fo + n), out := .ref (BRef.blk e.ob) (oo + n), len := UInt32.ofNat (n % 3) }, e.heap (cpyG sel n fo oo A) msg m) := by
453  have hlt := UInt32.toNat_lt l.len
454  obtain ⟨q, hq⟩ : ∃ q, n / 3 = q + 1 := ⟨n / 3 - 1, by omega⟩
455  have key := doTail_go hs msg m q l fo oo A (fuel - 1) (n % 3) (by omega) (by omega) (by unfold fuel; omega)
456    hf ho (by omega) (by omega)
457  rw [fuel_pred] at key
458  unfold tailD cdoWhile
459  rw [bind_ok key]
460  have hr : (UInt32.ofNat (n % 3)).toNat = n % 3 := by simp [UInt32.toNat_ofNat]; omega
461  have hn3 : n = 3 * (q + 1) + n % 3 := by omega
462  rw [tailIf_run hs (cpyG sel (3 * (q + 1)) fo oo A) msg m _ (n % 3) (fo + 3 * (q + 1)) (oo + 3 * (q + 1)) hr
463    (by omega) rfl rfl (by rw [hs.sel_cpyG]; omega) (by rw [cpyG_size]; omega)]
464  have e1 : fo + 3 * (q + 1) + n % 3 = fo + n := by omega
465  have e2 : oo + 3 * (q + 1) + n % 3 = oo + n := by omega
466  have e3 : cpyG sel (n % 3) (fo + 3 * (q + 1)) (oo + 3 * (q + 1)) (cpyG sel (3 * (q + 1)) fo oo A) = cpyG sel n fo oo A := by
467    conv => rhs; rw [hn3, cpyG_add]
468  rw [e1, e2, e3]
469
470end Zlib.Inffast.Proofs