参考文档 / ZLIB × LEAN
inffast.c.match-history.lean
此页源文件快照 ·
57392327370b7558 · 对应提交的原文 ↗本页保留 Lean 源码及行号。点击行号可定位语句，点击 import 中的模块名可查看依赖。
1import ZlibF.Spec.InflateFastMatchHistory
2import ZlibF.Math.InflateFastMatchHistory
3
4namespace Zlib.Inffast.Proofs
5open C Zlib.Inffast Zlib.Inffast.Spec
6
7variable {e : Env} {c : Ctx}
8
9/- The original execution proof is strengthened with the actual branch test.
10The bit/input frame and both original postconditions are preserved. -/
11private theorem copy_match_branch_run (hc : CtxOK e c) (A : Array UInt8) (msg : BPtr) (m : UInt32) (l : L) (o : Nat)
12 (hout : l.out = .ref (BRef.blk e.ob) o) (hbg : e.bg ≤ o) (hop : l.op.toNat = o - e.bg)
13 (hdist : 1 ≤ l.dist.toNat) (hlen : 3 ≤ l.len.toNat) (hroom : o + l.len.toNat ≤ A.size)
14 (hbroke : l.broke = false) :
15 Wp (copyMatch c l) (e.heap A msg m) (fun l' h' =>
16 l'.in_ = l.in_ ∧ l'.hold = l.hold ∧ l'.bits = l.bits ∧ l'.againL = l.againL ∧ l'.againD = l.againD ∧
17 l'.broke = decide (c.whave.toNat + (o - e.bg) < l.dist.toNat) ∧
18 ((l'.broke = false ∧ l'.out = .ref (BRef.blk e.ob) (o + l.len.toNat) ∧
19 h' = e.heap (matchArr e.s0.wsize.toNat e.s0.wnext.toNat e.woff e.W e.bg o l.dist.toNat l.len.toNat A) msg m) ∨
20 (l'.broke = true ∧ ∃ p, h' = e.heap A p BAD ∧ l'.out = l.out))) := by
21 have hoA : o ≤ A.size := by omega
22 unfold copyMatch
23 dsimp only
24 by_cases hd : l.dist > l.op
25 · simp only [hd, ite_true]
26 have hd1 : l.op.toNat < l.dist.toNat := UInt32.lt_iff_toNat_lt.mp hd
27 have hop1 : (l.dist - l.op).toNat = l.dist.toNat - (o - e.bg) := by
28 rw [u32_toNat_sub (by omega)]; omega
29 by_cases hw : l.dist - l.op > c.whave
30 · -- too far back
31 simp only [hw, ite_true]
32 refine Wp.bindO (e.heap_ldstate hc A msg m) ?_
33 have hsane : (({ e.s0 with mode := m } : InflateState).sane != 0) = true := by
34 simp only [bne_iff_ne, ne_eq]; exact e.hsane
35 simp only [hsane, ite_true]
36 obtain ⟨i, hi⟩ := badData_run hc A msg m "invalid distance too far back" (by decide +kernel)
37 refine Wp.bindE hi ?_
38 refine Wp.pure' ?_
39 have hhw : c.whave.toNat < (l.dist - l.op).toNat := UInt32.lt_iff_toNat_lt.mp hw
40 have htoo : c.whave.toNat + (o - e.bg) < l.dist.toNat := by omega
41 exact ⟨rfl, rfl, rfl, rfl, rfl, (by simp [htoo]), Or.inr ⟨rfl, _, rfl, rfl⟩⟩
42 · simp only [hw, ite_false]
43 have hw' : (l.dist - l.op).toNat ≤ c.whave.toNat := by
44 have h1 : ¬ (c.whave < l.dist - l.op) := hw
45 have h2 : ¬ (c.whave.toNat < (l.dist - l.op).toNat) := fun h => h1 (UInt32.lt_iff_toNat_lt.mpr h)
46 omega
47 have hwh : c.whave.toNat ≤ c.wsize.toNat := by rw [hc.whave, hc.wsize]; exact e.hwh
48 have hwn : c.wnext.toNat ≤ c.wsize.toNat := by rw [hc.wnext, hc.wsize]; exact e.hwn
49 have hws : c.wsize.toNat ≤ 32768 := by rw [hc.wsize]; exact e.hws
50 have hwne : e.s0.whave ≠ 0 := by
51 intro h0
52 have : c.whave.toNat = 0 := by rw [hc.whave, h0]; rfl
53 omega
54 obtain ⟨hwptr, hwb, hWb, hWsz⟩ := e.hwin hwne
55 have hwptr' : c.window = Ptr.ref (BRef.blk e.wb) e.woff := by rw [hc.window]; exact hwptr
56 have hsrc : Src e e.wb (fun _ => e.W) := Src.win e e.wb e.W hwb hWb
57 have hWg : Space.get (e.heap A msg m) (BRef.blk e.wb) = some e.W := by
58 show (e.heap A msg m).bytes e.wb = some e.W
59 rw [e.heap_bytes_ne A msg m hwb]; exact hWb
60 have hwsz : c.wsize.toNat = e.s0.wsize.toNat := by rw [hc.wsize]
61 have hwnx : c.wnext.toNat = e.s0.wnext.toNat := by rw [hc.wnext]
62 by_cases hn0 : c.wnext = 0
63 · -- (i) the window has not wrapped
64 have hn0' : (c.wnext == 0) = true := by simp [hn0]
65 simp only [hn0', ite_true]
66 have hsubw : (c.wsize - (l.dist - l.op)).toNat = c.wsize.toNat - (l.dist.toNat - (o - e.bg)) := by
67 rw [u32_toNat_sub (by omega), hop1]
68 have hadd : OkOn (e.heap A msg m) (Ptr.add c.window ↑(c.wsize - (l.dist - l.op)).toNat)
69 (Ptr.ref (BRef.blk e.wb) (e.woff + (c.wsize.toNat - (l.dist.toNat - (o - e.bg))))) := by
70 rw [hwptr', hsubw]
71 exact Ptr.add_nat_ok hWg (by omega)
72 refine Wp.bindO hadd ?_
73 generalize l.dist - l.op = op1 at hop1 hw' hadd ⊢
74 by_cases hlt : op1 < l.len
75 · simp only [hlt, ite_true]
76 have hlt' : op1.toNat < l.len.toNat := UInt32.lt_iff_toNat_lt.mp hlt
77 have hlen1 : (l.len - op1).toNat = l.len.toNat - op1.toNat := u32_toNat_sub (by omega)
78 refine Wp.bindE (copyOp_win e e.W msg m e.wb hwb hWb A
79 { l with op := op1, len := l.len - op1, from_ := Ptr.ref (BRef.blk e.wb) (e.woff + (c.wsize.toNat - (l.dist.toNat - (o - e.bg)))) }
80 op1.toNat (e.woff + (c.wsize.toNat - (l.dist.toNat - (o - e.bg)))) o rfl (by omega) rfl hout
81 (by omega) (by omega)) ?_
82 dsimp only
83 generalize hA1 : blitN e.W op1.toNat (e.woff + (c.wsize.toNat - (l.dist.toNat - (o - e.bg)))) o A = A1
84 have hA1sz : A1.size = A.size := by rw [← hA1]; exact blitN_size _ _ _ _ _
85 have hsub2 : OkOn (e.heap A1 msg m) (subn (Ptr.ref (BRef.blk e.ob) (o + op1.toNat)) l.dist)
86 (Ptr.ref (BRef.blk e.ob) (o + op1.toNat - l.dist.toNat)) :=
87 subn_ok (r := BRef.blk e.ob) (a := A1) (e.heap_bytes_ob A1 msg m) (by omega) (by omega)
88 refine Wp.bindO hsub2 ?_
89 refine Wp.of_eq (a := _) (h' := _) (tailW_run (Src.out e) A1 msg m
90 { l with out := Ptr.ref (BRef.blk e.ob) (o + op1.toNat), op := 0, len := l.len - op1,
91 from_ := Ptr.ref (BRef.blk e.ob) (o + op1.toNat - l.dist.toNat) }
92 (l.len - op1).toNat (o + op1.toNat - l.dist.toNat) (o + op1.toNat) rfl rfl rfl (by simp; omega)
93 (by omega)) ?_
94 refine ⟨rfl, rfl, rfl, rfl, rfl, (by simp only [hbroke]; have hn : ¬ (c.whave.toNat + (o - e.bg) < l.dist.toNat) := (by omega); simp [hn]), Or.inl ⟨hbroke, ?_, ?_⟩⟩
95 · simp only [hlen1]; rw [show o + op1.toNat + (l.len.toNat - op1.toNat) = o + l.len.toNat by omega]
96 · simp only [hlen1]
97 rw [cpyG_id]
98 unfold matchArr
99 have h1 : o - e.bg < l.dist.toNat := by omega
100 have h2 : e.s0.wnext.toNat = 0 := by rw [← hwnx]; rw [hn0]; rfl
101 simp only [h1, h2, hwsz, ite_true]
102 have h3 : op1.toNat = l.dist.toNat - (o - e.bg) := hop1
103 have h4 : op1.toNat < l.len.toNat := by omega
104 have h4' : l.dist.toNat - (o - e.bg) < l.len.toNat := by omega
105 have h5 : e.woff + (c.wsize.toNat - (l.dist.toNat - (o - e.bg))) =
106 e.woff + e.s0.wsize.toNat - (l.dist.toNat - (o - e.bg)) := by omega
107 simp only [h3, h4'] at hA1 ⊢
108 rw [h5] at hA1
109 rw [← hA1]
110 try simp
111 · simp only [hlt, ite_false]
112 have hlt' : l.len.toNat ≤ op1.toNat := by
113 have h1 : ¬ (op1 < l.len) := hlt
114 have h2 : ¬ (op1.toNat < l.len.toNat) := fun h => h1 (UInt32.lt_iff_toNat_lt.mpr h)
115 omega
116 refine Wp.of_eq (a := _) (h' := _) (tailW_run hsrc A msg m
117 { l with op := op1, from_ := Ptr.ref (BRef.blk e.wb) (e.woff + (c.wsize.toNat - (l.dist.toNat - (o - e.bg)))) }
118 l.len.toNat (e.woff + (c.wsize.toNat - (l.dist.toNat - (o - e.bg)))) o rfl rfl hout
119 (by show _ ≤ e.W.size; omega) (by omega)) ?_
120 refine ⟨rfl, rfl, rfl, rfl, rfl, (by simp only [hbroke]; have hn : ¬ (c.whave.toNat + (o - e.bg) < l.dist.toNat) := (by omega); simp [hn]), Or.inl ⟨hbroke, rfl, ?_⟩⟩
121 rw [cpyG_const]
122 unfold matchArr
123 have h1 : o - e.bg < l.dist.toNat := by omega
124 have h2 : e.s0.wnext.toNat = 0 := by rw [← hwnx]; rw [hn0]; rfl
125 have h3 : op1.toNat = l.dist.toNat - (o - e.bg) := hop1
126 have h4' : ¬ (l.dist.toNat - (o - e.bg) < l.len.toNat) := by omega
127 have h5 : e.woff + (c.wsize.toNat - (l.dist.toNat - (o - e.bg))) =
128 e.woff + e.s0.wsize.toNat - (l.dist.toNat - (o - e.bg)) := by omega
129 simp only [h1, h2, h4', ite_true, ite_false, h5]
130 · -- the window has wrapped (ii) or the data is contiguous (iii)
131 have hn0' : (c.wnext == 0) = false := by simp [hn0]
132 simp only [hn0']
133 have hn0n : 0 < c.wnext.toNat := by
134 have : c.wnext.toNat ≠ 0 := fun h => hn0 (UInt32.toNat_inj.mp (by simpa using h))
135 omega
136 by_cases hwl : c.wnext < l.dist - l.op
137 · -- (ii)
138 simp only [hwl, ite_true]
139 have hwl' : c.wnext.toNat < (l.dist - l.op).toNat := UInt32.lt_iff_toNat_lt.mp hwl
140 have hsum : (c.wsize + c.wnext).toNat = c.wsize.toNat + c.wnext.toNat := u32_toNat_add (by omega)
141 have hsubw : (c.wsize + c.wnext - (l.dist - l.op)).toNat =
142 c.wsize.toNat + c.wnext.toNat - (l.dist.toNat - (o - e.bg)) := by
143 rw [u32_toNat_sub (by omega), hsum, hop1]
144 have hadd : OkOn (e.heap A msg m) (Ptr.add c.window ↑(c.wsize + c.wnext - (l.dist - l.op)).toNat)
145 (Ptr.ref (BRef.blk e.wb) (e.woff + (c.wsize.toNat + c.wnext.toNat - (l.dist.toNat - (o - e.bg))))) := by
146 rw [hwptr', hsubw]
147 exact Ptr.add_nat_ok hWg (by omega)
148 refine Wp.bindO hadd ?_
149 generalize l.dist - l.op = op1 at hop1 hw' hadd hwl' ⊢
150 have hop2 : (op1 - c.wnext).toNat = op1.toNat - c.wnext.toNat := u32_toNat_sub (by omega)
151 generalize op1 - c.wnext = op2 at hop2 ⊢
152 have hfo1 : e.woff + (c.wsize.toNat + c.wnext.toNat - (l.dist.toNat - (o - e.bg))) =
153 e.woff + e.s0.wsize.toNat + e.s0.wnext.toNat - (l.dist.toNat - (o - e.bg)) := by omega
154 by_cases hlt : op2 < l.len
155 · simp only [hlt, ite_true]
156 have hlt' : op2.toNat < l.len.toNat := UInt32.lt_iff_toNat_lt.mp hlt
157 have hlen1 : (l.len - op2).toNat = l.len.toNat - op2.toNat := u32_toNat_sub (by omega)
158 refine Wp.bindE (copyOp_win e e.W msg m e.wb hwb hWb A
159 { l with op := op2, len := l.len - op2, from_ := Ptr.ref (BRef.blk e.wb) (e.woff + (c.wsize.toNat + c.wnext.toNat - (l.dist.toNat - (o - e.bg)))) }
160 op2.toNat (e.woff + (c.wsize.toNat + c.wnext.toNat - (l.dist.toNat - (o - e.bg)))) o rfl (by omega) rfl hout
161 (by omega) (by omega)) ?_
162 dsimp only
163 generalize hA1 : blitN e.W op2.toNat (e.woff + (c.wsize.toNat + c.wnext.toNat - (l.dist.toNat - (o - e.bg)))) o A = A1
164 have hA1sz : A1.size = A.size := by rw [← hA1]; exact blitN_size _ _ _ _ _
165 by_cases hwl2 : c.wnext < l.len - op2
166 · simp only [hwl2, ite_true]
167 have hwl2' : c.wnext.toNat < (l.len - op2).toNat := UInt32.lt_iff_toNat_lt.mp hwl2
168 have hlen2 : (l.len - op2 - c.wnext).toNat = l.len.toNat - op2.toNat - c.wnext.toNat := by
169 rw [u32_toNat_sub (by omega), hlen1]
170 refine Wp.bindE (copyOp_win e e.W msg m e.wb hwb hWb A1
171 { l with out := Ptr.ref (BRef.blk e.ob) (o + op2.toNat), op := c.wnext, len := l.len - op2 - c.wnext,
172 from_ := c.window }
173 c.wnext.toNat e.woff (o + op2.toNat) rfl hn0n hwptr' rfl (by omega) (by omega)) ?_
174 dsimp only
175 generalize hA2 : blitN e.W c.wnext.toNat e.woff (o + op2.toNat) A1 = A2
176 have hA2sz : A2.size = A.size := by rw [← hA2]; rw [blitN_size]; exact hA1sz
177 have hsub2 : OkOn (e.heap A2 msg m) (subn (Ptr.ref (BRef.blk e.ob) (o + op2.toNat + c.wnext.toNat)) l.dist)
178 (Ptr.ref (BRef.blk e.ob) (o + op2.toNat + c.wnext.toNat - l.dist.toNat)) :=
179 subn_ok (r := BRef.blk e.ob) (a := A2) (e.heap_bytes_ob A2 msg m) (by omega) (by omega)
180 refine Wp.bindO hsub2 ?_
181 refine Wp.of_eq (a := _) (h' := _) (tailW_run (Src.out e) A2 msg m
182 { l with out := Ptr.ref (BRef.blk e.ob) (o + op2.toNat + c.wnext.toNat), op := 0,
183 len := l.len - op2 - c.wnext,
184 from_ := Ptr.ref (BRef.blk e.ob) (o + op2.toNat + c.wnext.toNat - l.dist.toNat) }
185 (l.len - op2 - c.wnext).toNat (o + op2.toNat + c.wnext.toNat - l.dist.toNat)
186 (o + op2.toNat + c.wnext.toNat) rfl rfl rfl (by simp; omega) (by omega)) ?_
187 refine ⟨rfl, rfl, rfl, rfl, rfl, (by simp only [hbroke]; have hn : ¬ (c.whave.toNat + (o - e.bg) < l.dist.toNat) := (by omega); simp [hn]), Or.inl ⟨hbroke, ?_, ?_⟩⟩
188 · simp only [hlen2]; rw [show o + op2.toNat + c.wnext.toNat + (l.len.toNat - op2.toNat - c.wnext.toNat) = o + l.len.toNat by omega]
189 · simp only [hlen2]
190 rw [cpyG_id]
191 unfold matchArr
192 have h1 : o - e.bg < l.dist.toNat := by omega
193 have h2 : ¬ (e.s0.wnext.toNat = 0) := by rw [← hwnx]; omega
194 have h3 : e.s0.wnext.toNat < l.dist.toNat - (o - e.bg) := by rw [← hwnx]; omega
195 have h4 : l.dist.toNat - (o - e.bg) - e.s0.wnext.toNat < l.len.toNat := by rw [← hwnx]; omega
196 have h5 : e.s0.wnext.toNat < l.len.toNat - (l.dist.toNat - (o - e.bg) - e.s0.wnext.toNat) := by
197 rw [← hwnx]; omega
198 simp only [h1, h2, h3, h4, h5, ite_true, ite_false]
199 rw [← hA2, ← hA1, hfo1]
200 have hop2' : op2.toNat = l.dist.toNat - (o - e.bg) - e.s0.wnext.toNat := by omega
201 simp only [hop2', hwnx]
202 · simp only [hwl2, ite_false]
203 have hwl2' : (l.len - op2).toNat ≤ c.wnext.toNat := by
204 have h1 : ¬ (c.wnext < l.len - op2) := hwl2
205 have h2 : ¬ (c.wnext.toNat < (l.len - op2).toNat) := fun h => h1 (UInt32.lt_iff_toNat_lt.mpr h)
206 omega
207 refine Wp.of_eq (a := _) (h' := _) (tailW_run hsrc A1 msg m
208 { l with out := Ptr.ref (BRef.blk e.ob) (o + op2.toNat), op := 0, len := l.len - op2, from_ := c.window }
209 (l.len - op2).toNat e.woff (o + op2.toNat) rfl hwptr' rfl (by show _ ≤ e.W.size; omega) (by omega)) ?_
210 refine ⟨rfl, rfl, rfl, rfl, rfl, (by simp only [hbroke]; have hn : ¬ (c.whave.toNat + (o - e.bg) < l.dist.toNat) := (by omega); simp [hn]), Or.inl ⟨hbroke, ?_, ?_⟩⟩
211 · simp only [hlen1]; rw [show o + op2.toNat + (l.len.toNat - op2.toNat) = o + l.len.toNat by omega]
212 · simp only [hlen1]
213 rw [cpyG_const]
214 unfold matchArr
215 have h1 : o - e.bg < l.dist.toNat := by omega
216 have h2 : ¬ (e.s0.wnext.toNat = 0) := by rw [← hwnx]; omega
217 have h3 : e.s0.wnext.toNat < l.dist.toNat - (o - e.bg) := by rw [← hwnx]; omega
218 have h4 : l.dist.toNat - (o - e.bg) - e.s0.wnext.toNat < l.len.toNat := by rw [← hwnx]; omega
219 have h5 : ¬ (e.s0.wnext.toNat < l.len.toNat - (l.dist.toNat - (o - e.bg) - e.s0.wnext.toNat)) := by
220 rw [← hwnx]; omega
221 simp only [h1, h2, h3, h4, h5, ite_true, ite_false]
222 rw [← hA1, hfo1]
223 have hop2' : op2.toNat = l.dist.toNat - (o - e.bg) - e.s0.wnext.toNat := by omega
224 simp only [hop2', hwnx]
225 · simp only [hlt, ite_false]
226 have hlt' : l.len.toNat ≤ op2.toNat := by
227 have h1 : ¬ (op2 < l.len) := hlt
228 have h2 : ¬ (op2.toNat < l.len.toNat) := fun h => h1 (UInt32.lt_iff_toNat_lt.mpr h)
229 omega
230 refine Wp.of_eq (a := _) (h' := _) (tailW_run hsrc A msg m
231 { l with op := op2, from_ := Ptr.ref (BRef.blk e.wb) (e.woff + (c.wsize.toNat + c.wnext.toNat - (l.dist.toNat - (o - e.bg)))) }
232 l.len.toNat (e.woff + (c.wsize.toNat + c.wnext.toNat - (l.dist.toNat - (o - e.bg)))) o rfl rfl hout
233 (by show _ ≤ e.W.size; omega) (by omega)) ?_
234 refine ⟨rfl, rfl, rfl, rfl, rfl, (by simp only [hbroke]; have hn : ¬ (c.whave.toNat + (o - e.bg) < l.dist.toNat) := (by omega); simp [hn]), Or.inl ⟨hbroke, rfl, ?_⟩⟩
235 rw [cpyG_const]
236 unfold matchArr
237 have h1 : o - e.bg < l.dist.toNat := by omega
238 have h2 : ¬ (e.s0.wnext.toNat = 0) := by rw [← hwnx]; omega
239 have h3 : e.s0.wnext.toNat < l.dist.toNat - (o - e.bg) := by rw [← hwnx]; omega
240 have h4 : ¬ (l.dist.toNat - (o - e.bg) - e.s0.wnext.toNat < l.len.toNat) := by rw [← hwnx]; omega
241 simp only [h1, h2, h3, h4, ite_true, ite_false]
242 rw [hfo1]
243 · -- (iii)
244 simp only [hwl, ite_false]
245 have hwl' : (l.dist - l.op).toNat ≤ c.wnext.toNat := by
246 have h2 : ¬ (c.wnext.toNat < (l.dist - l.op).toNat) := fun h => hwl (UInt32.lt_iff_toNat_lt.mpr h)
247 omega
248 have hsubw : (c.wnext - (l.dist - l.op)).toNat = c.wnext.toNat - (l.dist.toNat - (o - e.bg)) := by
249 rw [u32_toNat_sub (by omega), hop1]
250 have hadd : OkOn (e.heap A msg m) (Ptr.add c.window ↑(c.wnext - (l.dist - l.op)).toNat)
251 (Ptr.ref (BRef.blk e.wb) (e.woff + (c.wnext.toNat - (l.dist.toNat - (o - e.bg))))) := by
252 rw [hwptr', hsubw]
253 exact Ptr.add_nat_ok hWg (by omega)
254 refine Wp.bindO hadd ?_
255 generalize l.dist - l.op = op1 at hop1 hw' hadd hwl' ⊢
256 by_cases hlt : op1 < l.len
257 · simp only [hlt, ite_true]
258 have hlt' : op1.toNat < l.len.toNat := UInt32.lt_iff_toNat_lt.mp hlt
259 have hlen1 : (l.len - op1).toNat = l.len.toNat - op1.toNat := u32_toNat_sub (by omega)
260 refine Wp.bindE (copyOp_win e e.W msg m e.wb hwb hWb A
261 { l with op := op1, len := l.len - op1, from_ := Ptr.ref (BRef.blk e.wb) (e.woff + (c.wnext.toNat - (l.dist.toNat - (o - e.bg)))) }
262 op1.toNat (e.woff + (c.wnext.toNat - (l.dist.toNat - (o - e.bg)))) o rfl (by omega) rfl hout
263 (by omega) (by omega)) ?_
264 dsimp only
265 generalize hA1 : blitN e.W op1.toNat (e.woff + (c.wnext.toNat - (l.dist.toNat - (o - e.bg)))) o A = A1
266 have hA1sz : A1.size = A.size := by rw [← hA1]; exact blitN_size _ _ _ _ _
267 have hsub2 : OkOn (e.heap A1 msg m) (subn (Ptr.ref (BRef.blk e.ob) (o + op1.toNat)) l.dist)
268 (Ptr.ref (BRef.blk e.ob) (o + op1.toNat - l.dist.toNat)) :=
269 subn_ok (r := BRef.blk e.ob) (a := A1) (e.heap_bytes_ob A1 msg m) (by omega) (by omega)
270 refine Wp.bindO hsub2 ?_
271 refine Wp.of_eq (a := _) (h' := _) (tailW_run (Src.out e) A1 msg m
272 { l with out := Ptr.ref (BRef.blk e.ob) (o + op1.toNat), op := 0, len := l.len - op1,
273 from_ := Ptr.ref (BRef.blk e.ob) (o + op1.toNat - l.dist.toNat) }
274 (l.len - op1).toNat (o + op1.toNat - l.dist.toNat) (o + op1.toNat) rfl rfl rfl (by simp; omega)
275 (by omega)) ?_
276 refine ⟨rfl, rfl, rfl, rfl, rfl, (by simp only [hbroke]; have hn : ¬ (c.whave.toNat + (o - e.bg) < l.dist.toNat) := (by omega); simp [hn]), Or.inl ⟨hbroke, ?_, ?_⟩⟩
277 · simp only [hlen1]; rw [show o + op1.toNat + (l.len.toNat - op1.toNat) = o + l.len.toNat by omega]
278 · simp only [hlen1]
279 rw [cpyG_id]
280 unfold matchArr
281 have h1 : o - e.bg < l.dist.toNat := by omega
282 have h2 : ¬ (e.s0.wnext.toNat < l.dist.toNat - (o - e.bg)) := by rw [← hwnx]; omega
283 have h3 : op1.toNat = l.dist.toNat - (o - e.bg) := hop1
284 have h4' : l.dist.toNat - (o - e.bg) < l.len.toNat := by omega
285 have h5 : e.woff + (c.wnext.toNat - (l.dist.toNat - (o - e.bg))) =
286 e.woff + e.s0.wnext.toNat - (l.dist.toNat - (o - e.bg)) := by omega
287 have h6 : ¬ (e.s0.wnext.toNat = 0) := by rw [← hwnx]; omega
288 simp only [h1, h2, h3, h4', h6, ite_true, ite_false] at hA1 ⊢
289 rw [h5] at hA1
290 rw [← hA1]
291 · simp only [hlt, ite_false]
292 have hlt' : l.len.toNat ≤ op1.toNat := by
293 have h1 : ¬ (op1 < l.len) := hlt
294 have h2 : ¬ (op1.toNat < l.len.toNat) := fun h => h1 (UInt32.lt_iff_toNat_lt.mpr h)
295 omega
296 refine Wp.of_eq (a := _) (h' := _) (tailW_run hsrc A msg m
297 { l with op := op1, from_ := Ptr.ref (BRef.blk e.wb) (e.woff + (c.wnext.toNat - (l.dist.toNat - (o - e.bg)))) }
298 l.len.toNat (e.woff + (c.wnext.toNat - (l.dist.toNat - (o - e.bg)))) o rfl rfl hout
299 (by show _ ≤ e.W.size; omega) (by omega)) ?_
300 refine ⟨rfl, rfl, rfl, rfl, rfl, (by simp only [hbroke]; have hn : ¬ (c.whave.toNat + (o - e.bg) < l.dist.toNat) := (by omega); simp [hn]), Or.inl ⟨hbroke, rfl, ?_⟩⟩
301 rw [cpyG_const]
302 unfold matchArr
303 have h1 : o - e.bg < l.dist.toNat := by omega
304 have h2 : ¬ (e.s0.wnext.toNat < l.dist.toNat - (o - e.bg)) := by rw [← hwnx]; omega
305 have h4' : ¬ (l.dist.toNat - (o - e.bg) < l.len.toNat) := by omega
306 have h5 : e.woff + (c.wnext.toNat - (l.dist.toNat - (o - e.bg))) =
307 e.woff + e.s0.wnext.toNat - (l.dist.toNat - (o - e.bg)) := by omega
308 have h6 : ¬ (e.s0.wnext.toNat = 0) := by rw [← hwnx]; omega
309 simp only [h1, h2, h4', h6, ite_true, ite_false, h5]
310 · simp only [hd, ite_false]
311 have hd' : l.dist.toNat ≤ o - e.bg := by
312 have h1 : ¬ (l.op < l.dist) := hd
313 have h2 : ¬ (l.op.toNat < l.dist.toNat) := fun h => h1 (UInt32.lt_iff_toNat_lt.mpr h)
314 omega
315 have hsub : OkOn (e.heap A msg m) (subn l.out l.dist) (Ptr.ref (BRef.blk e.ob) (o - l.dist.toNat)) := by
316 rw [hout]; exact subn_ok (r := BRef.blk e.ob) (a := A) (e.heap_bytes_ob A msg m) (by omega) hoA
317 refine Wp.bindO hsub ?_
318 refine Wp.of_eq (a := _) (h' := _) (tailD_run (Src.out e) A msg m
319 { l with from_ := Ptr.ref (BRef.blk e.ob) (o - l.dist.toNat) } l.len.toNat (o - l.dist.toNat) o rfl hlen rfl hout
320 (by simp; omega) (by omega)) ?_
321 have hmb : ¬ (o - e.bg < l.dist.toNat) := by omega
322 refine ⟨rfl, rfl, rfl, rfl, rfl, (by simp only [hbroke]; have hn : ¬ (c.whave.toNat + (o - e.bg) < l.dist.toNat) := (by omega); simp [hn]), Or.inl ⟨hbroke, rfl, ?_⟩⟩
323 simp [matchArr, hmb, cpyG_id]
324
325
326
327/-- The actual fast copy cut point rejects exactly unavailable history, and
328otherwise implements the independent growing-history match operation. -/
329theorem actual_copy_match_refines_lz77 : MatchHistory.Goal.actual_copy_match_refines_lz77 := by
330 intro e c bytes msg mode l o hc hout hbg hop hdist hlen hroom hbroke
331 dsimp only
332 have hsaved : (MatchHistory.saved e.W e.s0.wsize.toNat e.s0.wnext.toNat
333 e.s0.whave.toNat e.woff).length = e.s0.whave.toNat := by
334 simp [MatchHistory.saved]
335 have hcurrent : (ZlibF.Math.LZ77Copy.writtenBytes bytes o (o - e.bg)).length = o - e.bg := by
336 simp only [ZlibF.Math.LZ77Copy.writtenBytes, List.length_take,
337 List.length_drop, Array.length_toList]
338 omega
339 simp only [hsaved, hcurrent]
340 obtain ⟨l', after, hrun, hin, hhold, hbits, hagainL, hagainD, hbranch, hpost⟩ :=
341 copy_match_branch_run hc bytes msg mode l o hout hbg hop hdist hlen hroom hbroke
342 rw [hc.whave] at hbranch
343 by_cases htoo : e.s0.whave.toNat + (o - e.bg) < l.dist.toNat
344 · simp only [htoo, ite_true]
345 have hbreak : l'.broke = true := by simpa only [htoo, decide_true] using hbranch
346 rcases hpost with hsuccess | ⟨_, p, hheap, hout'⟩
347 · rw [hsuccess.1] at hbreak
348 contradiction
349 · exact ⟨l', after, p, hrun, hin, hhold, hbits, hagainL, hagainD, hbreak, hout', hheap⟩
350 · simp only [htoo, ite_false]
351 have hbreak : l'.broke = false := by simpa only [htoo, decide_false] using hbranch
352 rcases hpost with ⟨_, hout', hheap⟩ | ⟨hbad, _⟩
353 · refine ⟨l', after, hrun, hin, hhold, hbits, hagainL, hagainD, hbreak, hout', hheap, ?_⟩
354 apply fast_match_array_refines_lz77 e.W bytes e.s0.wsize.toNat e.s0.wnext.toNat
355 e.s0.whave.toNat e.woff e.bg o l.dist.toNat l.len.toNat e.hwh e.hwn
356 · intro hwh
357 have hne : e.s0.whave ≠ 0 := by
358 intro hz
359 apply hwh
360 simp [hz]
361 exact (e.hwin hne).2.2.2
362 · exact hbg
363 · exact hroom
364 · omega
365 · omega
366 · rw [hbad] at hbreak
367 contradiction
368
369end Zlib.Inffast.Proofs