inffast.c.body-token.lean

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

1import ZlibF.Spec.InflateFastBodyToken
2import ZlibF.Proof.«inffast.c.length-trace»
3import ZlibF.Proof.«inffast.c.length-semantics»
4import ZlibF.Proof.«inffast.c.distance-result»
5
6set_option autoImplicit false
7
8namespace Zlib.Inffast.Proofs.BodyTokenProof
9open C Zlib.Inffast Zlib.Inffast.Spec Zlib.Inffast.Proofs ZlibF.Spec
10open Zlib.Inftrees Zlib.Inftrees.Spec ZlibF.Math.LZ77Copy
11open Zlib.Inffast.Spec.BodyToken
12open Zlib.Inffast.Spec.LengthTrace
13variable {e : Env} {c : Ctx}
14
15private theorem written_length (bytes : Array UInt8) (offset count : Nat)
16    (hc : count ≤ offset) (hb : offset ≤ bytes.size) :
17    (writtenBytes bytes offset count).length = count := by
18  simp only [writtenBytes, List.length_take, List.length_drop, Array.length_toList]
19  omega
20
21private theorem written_get (bytes : Array UInt8) (offset count i : Nat) :
22    (writtenBytes bytes offset count)[i]? =
23      if i < count then bytes[offset - count + i]? else none := by
24  simp only [writtenBytes, List.getElem?_take, List.getElem?_drop, Array.getElem?_toList]
25
26private theorem written_set_append (bytes : Array UInt8) (offset count : Nat)
27    (value : UInt8) (hc : count ≤ offset) (hb : offset < bytes.size) :
28    writtenBytes (bytes.set! offset value) (offset + 1) (count + 1) =
29      writtenBytes bytes offset count ++ [value] := by
30  apply List.ext_getElem?
31  intro i
32  rw [written_get, List.getElem?_append, written_length bytes offset count hc (by omega)]
33  have hstart : offset + 1 - (count + 1) = offset - count := by omega
34  rw [hstart]
35  by_cases hi : i < count
36  · have hne : offset ≠ offset - count + i := by omega
37    simp [hi, show i < count + 1 by omega, written_get, Array.set!_eq_setIfInBounds,
38      Array.getElem?_setIfInBounds, hne]
39  · by_cases he : i = count
40    · subst i
41      have hs : offset - count + count = offset := by omega
42      simp [show ¬ count < count by omega, show count < count + 1 by omega, hs,
43        Array.set!_eq_setIfInBounds, Array.getElem?_setIfInBounds, hb]
44    · have hn : ¬ i < count + 1 := by omega
45      have hz : i - count ≠ 0 := by omega
46      simp [hi, hn, List.getElem?_singleton, hz]
47
48
49private theorem length_base_fields (symbol : Nat) (entry : Code)
50    (lo : 257 ≤ symbol) (hi : symbol ≤ 285)
51    (meaning : DecodeSemantics.SymbolEntry LENS symbol entry) :
52    entry.op &&& 16 ≠ 0 ∧
53    (entry.op &&& 15).toNat = lengthExtras.getD (symbol - 257) 0 ∧
54    entry.val.toNat = lengthBases.getD (symbol - 257) 0 := by
55  have extrasBound : ∀ n : Fin 29, lengthExtras.getD n.val 0 ≤ 5 := by decide +kernel
56  have bound : lengthExtras.getD (symbol - 257) 0 ≤ 5 := extrasBound ⟨symbol - 257, by omega⟩
57  have fields : entry.op.toNat = 16 + lengthExtras.getD (symbol - 257) 0 ∧
58      entry.val.toNat = lengthBases.getD (symbol - 257) 0 := by
59    simpa only [DecodeSemantics.SymbolEntry, ite_true,
60      ite_eq_right (show ¬ symbol < 256 by omega), ite_eq_right (show symbol ≠ 256 by omega), ite_eq_left hi] using meaning
61  have mask : ∀ op : UInt8, 16 ≤ op.toNat → op.toNat ≤ 21 →
62      op &&& 16 ≠ 0 ∧ (op &&& 15).toNat = op.toNat - 16 := by
63    apply u8_forall
64    decide +kernel
65  have shape := mask entry.op (by omega) (by omega)
66  exact ⟨shape.1, by rw [shape.2, fields.1]; omega, fields.2⟩
67
68private theorem literal_symbol (symbol : Nat) (entry : Code) (hi : symbol ≤ 285)
69    (meaning : DecodeSemantics.SymbolEntry LENS symbol entry) (literal : entry.op = 0) :
70    symbol < 256 ∧ entry.val.toNat = symbol := by
71  by_cases small : symbol < 256
72  · have fields : entry.op = 0 ∧ entry.val.toNat = symbol := by
73      simpa only [DecodeSemantics.SymbolEntry, ite_true, ite_eq_left small] using meaning
74    exact ⟨small, fields.2⟩
75  · by_cases eob : symbol = 256
76    · subst symbol
77      have fields : entry.op = 96 ∧ entry.val = 0 := by
78        simpa [DecodeSemantics.SymbolEntry] using meaning
79      simp [literal] at fields
80    · have fields := length_base_fields symbol entry (by omega) hi meaning
81      simp [literal] at fields
82
83private theorem base_symbol (symbol : Nat) (entry : Code) (hi : symbol ≤ 285)
84    (meaning : DecodeSemantics.SymbolEntry LENS symbol entry) (base : entry.op &&& 16 ≠ 0) :
85    257 ≤ symbol := by
86  by_cases small : symbol < 256
87  · have fields : entry.op = 0 ∧ entry.val.toNat = symbol := by
88      simpa only [DecodeSemantics.SymbolEntry, ite_true, ite_eq_left small] using meaning
89    simp [fields.1] at base
90  · by_cases eob : symbol = 256
91    · subst symbol
92      have fields : entry.op = 96 ∧ entry.val = 0 := by
93        simpa [DecodeSemantics.SymbolEntry] using meaning
94      exact False.elim (base (by rw [fields.1]; decide +kernel))
95    · omega
96
97private theorem eob_symbol (symbol : Nat) (entry : Code) (hi : symbol ≤ 285)
98    (meaning : DecodeSemantics.SymbolEntry LENS symbol entry)
99    (nonzero : entry.op ≠ 0) (noBase : entry.op &&& 16 = 0) : symbol = 256 := by
100  by_cases small : symbol < 256
101  · have fields : entry.op = 0 ∧ entry.val.toNat = symbol := by
102      simpa only [DecodeSemantics.SymbolEntry, ite_true, ite_eq_left small] using meaning
103    exact False.elim (nonzero fields.1)
104  · by_cases eob : symbol = 256
105    · exact eob
106    · have fields := length_base_fields symbol entry (by omega) hi meaning
107      exact False.elim (fields.1 noBase)
108
109private theorem refill_entry_wp (hc : CtxOK e c) (A : Array UInt8) (msg : BPtr) (m : UInt32) (l : L) (i o s : Nat)
110    (hts : DistTableSafe e.DCA e.od e.s0.distbits.toNat)
111    (hls : LS e l i o) (hA : e.o0 + e.sm0.avail_out.toNat ≤ A.size) (ho : o + 258 ≤ e.o0 + e.sm0.avail_out.toNat)
112    (hAb : A.size < 2 ^ 63) (hbroke : l.broke = false) (hlen : 3 ≤ l.len.toNat ∧ l.len.toNat ≤ 258)
113    (hs6 : s + 6 ≤ e.i0 + e.sm0.avail_in.toNat) (hT : i ≤ s + 3) (hT3 : i = s + 3 → 4 ≤ l.bits.toNat) :
114    Wp (dolenRefill c l) (e.heap A msg m) (fun l' h' =>
115      DistanceEntry e c A msg m (Sg e l.hold.toNat l.bits.toNat i) i o l.len.toNat l' h') := by
116  unfold dolenRefill
117  by_cases h1 : l.bits < 15
118  · simp only [h1, ite_true]
119    have h1' : l.bits.toNat < 15 := by simpa using UInt32.lt_iff_toNat_lt.mp h1
120    have hiin : i < e.i0 + e.sm0.avail_in.toNat := by omega
121    refine Wp.bindO (pull_run e _ l i o hls (by omega) hiin (e.heap_bytes_in A msg m)) ?_
122    have hl3 := hls.pullL (by omega) hiin
123    have hs3 := Sg_pullL hls (by omega) hiin
124    have hb3 := pullL_bits l (e.IN.getD i 0) (.ref (BRef.blk e.ib) (i + 1)) hls.hb
125    have hi2 : i + 1 < e.i0 + e.sm0.avail_in.toNat := by omega
126    have hb3' : (pullL l (e.IN.getD i 0) (.ref (BRef.blk e.ib) (i + 1))).bits.toNat ≤ 22 := by
127      simp only [pullL] at hb3 ⊢; omega
128    refine Wp.bindO (pull_run e _ _ (i + 1) o hl3 hb3' hi2 (e.heap_bytes_in A msg m)) ?_
129    have hl4 := hl3.pullL hb3' hi2
130    have hs4 := Sg_pullL hl3 hb3' hi2
131    have hb4 := pullL_bits (pullL l (e.IN.getD i 0) (.ref (BRef.blk e.ib) (i + 1))) (e.IN.getD (i + 1) 0)
132      (.ref (BRef.blk e.ib) (i + 1 + 1)) hl3.hb
133    simp only [pullL] at hb3 hb4
134    have pullRoom : i + 1 + 1 + 2 ≤ e.i0 + e.sm0.avail_in.toNat ∨
135        (i + 1 + 1 + 1 ≤ e.i0 + e.sm0.avail_in.toNat ∧
136          20 ≤ (pullL (pullL l (e.IN.getD i 0) (.ref (.blk e.ib) (i + 1)))
137            (e.IN.getD (i + 1) 0) (.ref (.blk e.ib) (i + 1 + 1))).bits.toNat) := by
138      by_cases hc3 : i = s + 3
139      · right; have := hT3 hc3; simp only [pullL]; omega
140      · left; omega
141    obtain ⟨l', after, run, _⟩ := dolenDist_wp hc A msg m _ (i + 1 + 1) o hts hl4 hA ho hAb hbroke hlen
142      (by simp only [pullL]; omega) pullRoom
143    exact Wp.of_eq run ⟨_, i + 1 + 1, by omega, by omega, hl4, hbroke, rfl,
144      by simp only [pullL]; omega, pullRoom, hs4.trans hs3, run⟩
145  · simp only [h1, ite_false]
146    have h1' : 15 ≤ l.bits.toNat := by
147      have : ¬ (l.bits.toNat < 15) := fun h => h1 (UInt32.lt_iff_toNat_lt.mpr (by simpa using h))
148      omega
149    obtain ⟨l', after, run, _⟩ := dolenDist_wp hc A msg m l i o hts hls hA ho hAb hbroke hlen h1' (Or.inl (by omega))
150    exact Wp.of_eq run ⟨l, i, by omega, by omega, hls, hbroke, rfl, h1', Or.inl (by omega), rfl, run⟩
151
152private theorem ext_entry_wp (hc : CtxOK e c) (A : Array UInt8) (msg : BPtr) (m : UInt32) (l : L) (i o s : Nat)
153    (hts : DistTableSafe e.DCA e.od e.s0.distbits.toNat)
154    (hls : LS e l i o) (hA : e.o0 + e.sm0.avail_out.toNat ≤ A.size) (ho : o + 258 ≤ e.o0 + e.sm0.avail_out.toNat)
155    (hAb : A.size < 2 ^ 63) (hbroke : l.broke = false) (hx : l.op.toNat ≤ 5) (hxb : l.op.toNat ≤ l.bits.toNat)
156    (hlen : 3 ≤ l.len.toNat ∧ l.len.toNat + 2 ^ l.op.toNat ≤ 259)
157    (hs6 : s + 6 ≤ e.i0 + e.sm0.avail_in.toNat) (hT : i ≤ s + 3)
158    (hT3 : i = s + 3 → 4 + l.op.toNat ≤ l.bits.toNat) :
159    Wp (dolenExt c l) (e.heap A msg m) (fun l' h' =>
160      ∃ lx S1, readBits l.op.toNat (Sg e l.hold.toNat l.bits.toNat i) = some (lx, S1) ∧
161        DistanceEntry e c A msg m S1 i o (l.len.toNat + lx) l' h') := by
162  unfold dolenExt
163  have hxs : l.op.toNat < 32 := by omega
164  refine Wp.bindO (shl32_ok hxs) ?_
165  dsimp only
166  have hlow := hold_low32 (x := l.hold) (k := l.op) hxs
167  have hlowlt : l.hold.toNat % 2 ^ l.op.toNat < 2 ^ l.op.toNat := Nat.mod_lt _ (Nat.pow_pos (by omega))
168  have hpow : 0 < 2 ^ l.op.toNat := Nat.pow_pos (by omega)
169  have hlen' : (l.len + (l.hold.toUInt32 &&& (1 <<< l.op) - 1)).toNat = l.len.toNat + l.hold.toNat % 2 ^ l.op.toNat := by
170    rw [u32_toNat_add (by rw [hlow]; omega), hlow]
171  refine Wp.bindO (shr64_ok (x := l.hold) (n := l.op.toUInt64) (by rw [UInt32.toNat_toUInt64]; omega)) ?_
172  have hls1 : LS e (dropL l l.op) i o := hls.dropL l.op hxb (by omega)
173  have hbn := dropL_bits l l.op hxb
174  have hrb := readBits_bitsOfNat l.op.toNat l.bits.toNat l.hold.toNat (inBits e i) hxb
175  have hsg := Sg_dropL (e := e) l l.op i hxb (by omega)
176  refine Wp.mono (refill_entry_wp hc A msg m
177    { in_ := l.in_, out := l.out, hold := l.hold >>> l.op.toUInt64, bits := l.bits - l.op, here := l.here, op := l.op,
178      len := l.len + (l.hold.toUInt32 &&& (1 <<< l.op) - 1), dist := l.dist, from_ := l.from_, broke := l.broke,
179      againL := l.againL, againD := l.againD } i o s hts (LS.congr hls1 rfl rfl rfl rfl) hA ho hAb hbroke
180    (by rw [hlen']; omega) hs6 hT (by intro h3; have := hT3 h3; show 4 ≤ (l.bits - l.op).toNat; simp only [dropL] at hbn; omega)) ?_
181  intro l' h' hq
182  refine ⟨l.hold.toNat % 2 ^ l.op.toNat, Sg e (dropL l l.op).hold.toNat (dropL l l.op).bits.toNat i, ?_, ?_⟩
183  · unfold Sg; rw [hrb, dropL_hold l l.op (by omega), dropL_bits l l.op hxb]
184  · simp only [hlen'] at hq
185    exact hq
186
187
188private theorem len_entry_wp (hc : CtxOK e c) (A : Array UInt8) (msg : BPtr) (m : UInt32) (l : L) (i o s : Nat)
189    (hts : DistTableSafe e.DCA e.od e.s0.distbits.toNat)
190    (hls : LS e l i o) (hA : e.o0 + e.sm0.avail_out.toNat ≤ A.size) (ho : o + 258 ≤ e.o0 + e.sm0.avail_out.toNat)
191    (hAb : A.size < 2 ^ 63) (hbroke : l.broke = false) (hx : l.op.toNat ≤ 5)
192    (hlen : 3 ≤ l.len.toNat ∧ l.len.toNat + 2 ^ l.op.toNat ≤ 259)
193    (hs6 : s + 6 ≤ e.i0 + e.sm0.avail_in.toNat) (hT : i ≤ s + 2) (hb2 : i = s + 2 → 1 ≤ l.bits.toNat) :
194    Wp (dolenLen c l) (e.heap A msg m) (fun l' h' =>
195      ∃ i2 lx S1, i ≤ i2 ∧ i2 ≤ i + 1 ∧ readBits l.op.toNat (Sg e l.hold.toNat l.bits.toNat i) = some (lx, S1) ∧
196        DistanceEntry e c A msg m S1 i2 o (l.len.toNat + lx) l' h') := by
197  unfold dolenLen
198  by_cases h0 : l.op != 0
199  · simp only [h0, ite_true]
200    have h0' : l.op.toNat ≠ 0 := by
201      intro h; apply (by simpa using h0 : l.op ≠ 0); exact UInt32.toNat_inj.mp (by simpa using h)
202    by_cases h1 : l.bits < l.op
203    · simp only [h1, ite_true]
204      have h1' : l.bits.toNat < l.op.toNat := UInt32.lt_iff_toNat_lt.mp h1
205      have hiin : i < e.i0 + e.sm0.avail_in.toNat := by omega
206      refine Wp.bindO (pull_run e _ l i o hls (by omega) hiin (e.heap_bytes_in A msg m)) ?_
207      have hl3 := hls.pullL (by omega) hiin
208      have hs3 := Sg_pullL hls (by omega) hiin
209      have hb3 := pullL_bits l (e.IN.getD i 0) (.ref (BRef.blk e.ib) (i + 1)) hls.hb
210      refine Wp.mono (ext_entry_wp hc A msg m _ (i + 1) o s hts hl3 hA ho hAb hbroke (by simp only [pullL]; omega)
211        (by simp only [pullL] at hb3 ⊢; omega) (by simp only [pullL]; omega) hs6 (by omega)
212        (by intro h3; simp only [pullL] at hb3 ⊢; have := hb2 (by omega); omega)) ?_
213      intro l' h' hq
214      obtain ⟨lx, S1, hr, hrp⟩ := hq
215      refine ⟨i + 1, lx, S1, by omega, by omega, ?_, ?_⟩
216      · simp only [pullL] at hr hs3 ⊢; rw [hs3] at hr; exact hr
217      · simp only [pullL] at hrp ⊢; exact hrp
218    · simp only [h1, ite_false]
219      have h1' : l.op.toNat ≤ l.bits.toNat := by
220        have : ¬ (l.bits.toNat < l.op.toNat) := fun h => h1 (UInt32.lt_iff_toNat_lt.mpr h)
221        omega
222      refine Wp.mono (ext_entry_wp hc A msg m l i o s hts hls hA ho hAb hbroke hx h1' hlen hs6 (by omega)
223        (by intro h3; omega)) ?_
224      intro l' h' hq
225      obtain ⟨lx, S1, hr, hrp⟩ := hq
226      exact ⟨i, lx, S1, by omega, by omega, hr, hrp⟩
227  · simp only [h0, ite_false]
228    have h0' : l.op.toNat = 0 := by
229      have : l.op = 0 := by simpa using h0
230      rw [this]; rfl
231    refine Wp.mono (refill_entry_wp hc A msg m l i o s hts hls hA ho hAb hbroke ⟨hlen.1, by
232      have : 0 < 2 ^ l.op.toNat := Nat.pow_pos (by omega)
233      omega⟩ hs6 (by omega) (by intro h3; omega)) ?_
234    intro l' h' hq
235    refine ⟨i, 0, Sg e l.hold.toNat l.bits.toNat i, by omega, by omega, ?_, ?_⟩
236    · rw [h0']; rfl
237    · simpa using hq
238
239set_option maxHeartbeats 1000000 in
240private theorem pass_entry_wp (hc : CtxOK e c) (A : Array UInt8) (msg : BPtr) (m : UInt32)
241    (l : L) (i o s d k : Nat) (hls : LS e l i o) (hAsz : A.size = e.A0.size)
242    (ho : o + 258 ≤ e.o0 + e.sm0.avail_out.toNat) (hbroke : l.broke = false)
243    (hs6 : s + 6 ≤ e.i0 + e.sm0.avail_in.toNat) (hsi : s ≤ i) (hT : i ≤ s + 2)
244    (hb15 : 15 ≤ l.bits.toNat + d) (hbi2 : i = s + 2 → 16 ≤ l.bits.toNat + d)
245    (hhere : l.here = .ref e.rl k) (hk : k < e.LCA.size)
246    (hEb : (e.LCA.getD k default).bits.toNat ≤ l.bits.toNat)
247    (hEd : (e.LCA.getD k default).bits.toNat + d ≤ 15)
248    (hcl : (LenLink (e.LCA.getD k default) ∧ LinkOK LenLeaf e.LCA e.ol (e.LCA.getD k default)) ∨
249      LenLeaf d (e.LCA.getD k default)) :
250    Wp (dolen c l) (e.heap A msg m) (fun l' h' =>
251      (l'.againL = true ∧ l'.broke = false ∧ h' = e.heap A msg m ∧
252        LenLink (e.LCA.getD k default) ∧
253        ∃ j, j < 2 ^ (e.LCA.getD k default).op.toNat ∧
254          l'.here = .ref e.rl (e.ol + (e.LCA.getD k default).val.toNat + j) ∧
255          j = (l.hold.toNat / 2 ^ (e.LCA.getD k default).bits.toNat) % 2 ^ (e.LCA.getD k default).op.toNat ∧
256          LS e l' i o ∧ l'.bits.toNat = l.bits.toNat - (e.LCA.getD k default).bits.toNat ∧
257          Sg e l'.hold.toNat l'.bits.toNat i = (Sg e l.hold.toNat l.bits.toNat i).drop (e.LCA.getD k default).bits.toNat) ∨
258      EndWithDistanceEntry e c A msg m ((Sg e l.hold.toNat l.bits.toNat i).drop (e.LCA.getD k default).bits.toNat)
259        i o (e.LCA.getD k default) l' h') := by
260  have hA : e.o0 + e.sm0.avail_out.toNat ≤ A.size := by rw [hAsz]; exact e.hAsz
261  have hAb : A.size < 2 ^ 63 := by rw [hAsz]; exact e.hAbig
262  have hkE : e.LCA[k]'hk = e.LCA.getD k default := by simp [Array.getD_eq_getD_getElem?, hk]
263  have hld : OkOn (e.heap A msg m) (Ptr.load l.here) (e.LCA.getD k default) := by
264    rw [hhere, ← hkE]; exact Ptr.load_ok (e.heap_cget_LCA A msg m) hk
265  have hEbn : (e.LCA.getD k default).bits.toUInt32.toNat = (e.LCA.getD k default).bits.toNat := toNat32 _
266  have hEb64 : (e.LCA.getD k default).bits.toUInt32.toUInt64.toNat = (e.LCA.getD k default).bits.toNat := by simp [toNat32]
267  have hls1 := hls.dropL (e.LCA.getD k default).bits.toUInt32 (by omega) (by omega)
268  have hsg1 := Sg_dropL (e := e) l (e.LCA.getD k default).bits.toUInt32 i (by omega) (by omega)
269  rw [dolen_eq_len]
270  dsimp only
271  refine Wp.bindO hld ?_
272  refine Wp.bindO (shr64_ok (x := l.hold) (by omega)) ?_
273  refine Wp.bindO hld ?_
274  generalize e.LCA.getD k default = E at *
275  have hsg1' : Sg e (l.hold >>> E.bits.toUInt32.toUInt64).toNat (l.bits - E.bits.toUInt32).toNat i =
276      (Sg e l.hold.toNat l.bits.toNat i).drop E.bits.toNat := by
277    simpa only [dropL, hEbn] using hsg1
278  by_cases hz : (E.op.toUInt32 == 0) = true
279  · simp only [hz, ite_true]
280    refine Wp.bindO hld ?_
281    have hst : store8 l.out E.val.toUInt8 (e.heap A msg m) =
282        .ok ((), e.heap (A.set! o E.val.toUInt8) msg m) := by
283      rw [hls.hout, ← e.heap_put A (A.set! o E.val.toUInt8) msg m]
284      exact Ptr.store_ok (e.heap_bytes_ob A msg m) (e.heap_ro_ob A msg m) (by omega)
285    refine Wp.bindE hst ?_
286    refine Wp.bindO (x := Ptr.ref (BRef.blk e.ob) (o + 1)) ?_ ?_
287    · rw [hls.hout]
288      exact Ptr.add_nat_ok (e.heap_bytes_ob _ msg m) (by simp; omega)
289    · have hop : E.op = 0 := by rw [mask0] at hz; simpa using hz
290      refine Wp.pure' (Or.inr ?_)
291      refine ⟨?_, ?_⟩
292      · refine ⟨?_, rfl, Or.inl ⟨hop, hbroke, ?_, hsg1', rfl⟩⟩
293        · intro link; exact link.1 hop
294        · exact ⟨hls.hin, rfl, hls.hi0, hls.hi1, by have := hls.ho0; omega, hls1.hb, hls1.hH, hls1.hacc⟩
295      · intro bad; exact False.elim (bad.1 hop)
296  · have hz' : E.op ≠ 0 := by rw [mask0] at hz; simpa using hz
297    by_cases hb16 : (E.op.toUInt32 &&& 16 != 0) = true
298    · simp only [hz, hb16, ite_true, ite_false, Bool.false_eq_true]
299      have hb16' : E.op &&& 16 ≠ 0 := by rw [mask16] at hb16; simpa using hb16
300      have hbase : (E.op &&& 15).toNat ≤ 5 ∧ 3 ≤ E.val.toNat ∧
301          E.val.toNat + 2 ^ (E.op &&& 15).toNat ≤ 259 := by
302        rcases hcl with h | h
303        · exact False.elim (hb16' h.1.2.1)
304        · rcases h.2 with h0 | h | h
305          · exact False.elim (hz' h0)
306          · exact h.2
307          · exact False.elim (hb16' h.1)
308      refine Wp.bindO hld ?_
309      let stage : L :=
310        { in_ := l.in_, out := l.out, hold := l.hold >>> E.bits.toUInt32.toUInt64, bits := l.bits - E.bits.toUInt32,
311          here := l.here, op := E.op.toUInt32 &&& 15, len := E.val.toUInt32, dist := l.dist, from_ := l.from_,
312          broke := l.broke, againL := false, againD := l.againD }
313      obtain ⟨l', h', run, tail⟩ := len_entry_wp hc A msg m stage i o s e.hdt
314        (LS.congr hls1 rfl rfl rfl rfl) hA ho hAb hbroke
315        (by dsimp [stage]; rw [mask15]; exact hbase.1)
316        (by simpa [stage, mask15] using hbase.2) hs6 hT
317        (by intro hi; have := hbi2 hi; show 1 ≤ (l.bits - E.bits.toUInt32).toNat
318            rw [u32_toNat_sub (by omega), hEbn]; omega)
319      have oldRun := dolenLen_wp hc A msg m stage i o s e.hdt
320        (LS.congr hls1 rfl rfl rfl rfl) hA ho hAb hbroke
321        (by dsimp [stage]; rw [mask15]; exact hbase.1)
322        (by simpa [stage, mask15] using hbase.2) hs6 hT
323        (by intro hi; have := hbi2 hi; show 1 ≤ (l.bits - E.bits.toUInt32).toNat
324            rw [u32_toNat_sub (by omega), hEbn]; omega)
325      have result := Wp.at_run oldRun run
326      have hag : l'.againL = false := by simpa [stage] using dolenLen_againL run
327      refine Wp.of_eq run (Or.inr ?_)
328      refine ⟨?_, ?_⟩
329      · refine ⟨?_, hag, Or.inr (Or.inl ⟨hz', hb16', ?_⟩)⟩
330        · intro link; exact hb16' link.2.1
331        · obtain ⟨i', extra, rest, hi, hi1, read, refill⟩ := result
332          refine ⟨i', extra, rest, hi, hi1, ?_, ?_⟩
333          · simpa only [stage, mask15, hsg1'] using read
334          · simpa only [stage, UInt16.toNat_toUInt32] using refill
335      · intro _
336        obtain ⟨i', extra, rest, hi, hi1, read, distance⟩ := tail
337        refine ⟨i', extra, rest, hi, hi1, ?_, ?_⟩
338        · simpa only [stage, mask15, hsg1'] using read
339        · simpa only [stage, UInt16.toNat_toUInt32] using distance
340    · have hb16' : E.op &&& 16 = 0 := by rw [mask16] at hb16; simpa using hb16
341      by_cases hb64 : (E.op.toUInt32 &&& 64 == 0) = true
342      · simp only [hz, hb16, hb64, ite_true, ite_false, Bool.false_eq_true]
343        have hb64' : E.op &&& 64 = 0 := by rw [mask64] at hb64; simpa using hb64
344        have hl : LenLink E := ⟨hz', hb16', hb64'⟩
345        have hlk : LinkOK LenLeaf e.LCA e.ol E := by
346          rcases hcl with h | h
347          · exact h.2
348          · rcases h.2 with h0 | h | h
349            · exact False.elim (hz' h0)
350            · exact False.elim (h.1 hb16')
351            · exact False.elim (h.2 hb64')
352        refine Wp.bindO hld ?_
353        have hlc : c.lcode = .ref e.rl e.ol := by rw [hc.lcode]; exact e.hlc
354        have hop32 : E.op.toUInt32.toNat < 32 := by rw [toNat32]; have := hlk.2.2.1; omega
355        refine Wp.bindO (x := Ptr.ref e.rl (e.ol + E.val.toNat)) ?_ ?_
356        · rw [hlc]
357          exact Ptr.add_nat_ok (h := e.heap A msg m) (r := e.rl) (a := e.LCA) (off := e.ol)
358            (n := E.val.toNat) (e.heap_cget_LCA A msg m)
359            (Nat.le_trans (Nat.le_add_right _ _) hlk.2.2.2.1)
360        refine Wp.bindO (shl32_ok hop32) ?_
361        have hlow := hold_low64 (x := l.hold >>> E.bits.toUInt32.toUInt64) (k := E.op.toUInt32) hop32
362        have hjlt : (l.hold >>> E.bits.toUInt32.toUInt64).toNat % 2 ^ E.op.toUInt32.toNat < 2 ^ E.op.toNat := by
363          rw [toNat32]; exact Nat.mod_lt _ (Nat.pow_pos (by omega))
364        generalize hjd : (l.hold >>> E.bits.toUInt32.toUInt64).toNat % 2 ^ E.op.toUInt32.toNat = j at hlow hjlt
365        refine Wp.bindO (x := Ptr.ref e.rl (e.ol + E.val.toNat + j)) ?_ ?_
366        · rw [hlow]
367          exact Ptr.add_nat_ok (h := e.heap A msg m) (r := e.rl) (a := e.LCA) (off := e.ol + E.val.toNat)
368            (n := j) (e.heap_cget_LCA A msg m) (by have := hlk.2.2.2.1; omega)
369        refine Wp.pure' (Or.inl ⟨rfl, hbroke, rfl, hl, j, hjlt, rfl, ?_,
370          LS.congr hls1 rfl rfl rfl rfl, ?_, hsg1'⟩)
371        · have hshift : (l.hold >>> E.bits.toUInt32.toUInt64).toNat = l.hold.toNat / 2 ^ E.bits.toNat := by
372            rw [u64_shr (by omega), hEbn]
373          simpa only [hshift, toNat32] using hjd.symm
374        · rw [u32_toNat_sub (by omega), hEbn]
375      · simp only [hz, hb16, hb64, ite_false, Bool.false_eq_true]
376        by_cases hb32 : (E.op.toUInt32 &&& 32 != 0) = true
377        · simp only [hb32, ite_true]
378          refine Wp.bindE (e.heap_ldstate hc A msg m) ?_
379          refine Wp.bindE (e.heap_stmode hc A msg m TYPE _ rfl) ?_
380          have hb64' : E.op &&& 64 ≠ 0 := by rw [mask64] at hb64; simpa using hb64
381          have hb32' : E.op &&& 32 ≠ 0 := by rw [mask32] at hb32; simpa using hb32
382          refine Wp.pure' (Or.inr ?_)
383          refine ⟨?_, ?_⟩
384          · refine ⟨?_, rfl, Or.inr (Or.inr (Or.inl ⟨hz', hb16', hb64', hb32', rfl,
385              LS.congr hls1 rfl rfl rfl rfl, hsg1', rfl⟩))⟩
386            intro link; exact hb64' link.2.2
387          · intro bad; exact False.elim (bad.2 hb16')
388        · simp only [hb32, ite_false, Bool.false_eq_true]
389          obtain ⟨ip, hip⟩ := badData_run hc A msg m "invalid literal/length code" (by decide +kernel)
390          refine Wp.bindE hip ?_
391          have hb64' : E.op &&& 64 ≠ 0 := by rw [mask64] at hb64; simpa using hb64
392          have hb32' : E.op &&& 32 = 0 := by rw [mask32] at hb32; simpa using hb32
393          refine Wp.pure' (Or.inr ?_)
394          refine ⟨?_, ?_⟩
395          · refine ⟨?_, rfl, Or.inr (Or.inr (Or.inr ⟨hz', hb16', hb64', hb32', rfl,
396              LS.congr hls1 rfl rfl rfl rfl, hsg1', .ref (.str ip) 0, rfl⟩))⟩
397            intro link; exact hb64' link.2.2
398          · intro bad; exact False.elim (bad.2 hb16')
399
400private theorem loop_entry_wp (hc : CtxOK e c) (A : Array UInt8) (msg : BPtr) (m : UInt32)
401    (l : L) (i o s kidx : Nat) (hls : LS e l i o) (hAsz : A.size = e.A0.size)
402    (ho : o + 258 ≤ e.o0 + e.sm0.avail_out.toNat) (hbroke : l.broke = false)
403    (hs6 : s + 6 ≤ e.i0 + e.sm0.avail_in.toNat) (hsi : s ≤ i) (hT : i ≤ s + 2)
404    (hb15 : 15 ≤ l.bits.toNat) (hbi2 : i = s + 2 → 16 ≤ l.bits.toNat)
405    (hk : kidx < 2 ^ e.s0.lenbits.toNat) (hhere : l.here = .ref e.rl (e.ol + kidx)) :
406    Wp (cdoWhile (dolen c) (fun l => pure (l.againL, l)) l) (e.heap A msg m)
407      (fun l' h' => ∃ entry consumed, consumed ≤ 15 ∧
408        LengthSemantics.Look e l.hold.toNat kidx entry consumed ∧
409        EndWithDistanceEntry e c A msg m ((Sg e l.hold.toNat l.bits.toNat i).drop consumed) i o entry l' h') := by
410  obtain ⟨hR, hsz, hall⟩ := e.hlt
411  have hksz : e.ol + kidx < e.LCA.size := by omega
412  have hclass : (LenLink (e.LCA.getD (e.ol + kidx) default) ∧
413      LinkOK LenLeaf e.LCA e.ol (e.LCA.getD (e.ol + kidx) default)) ∨
414      LenLeaf 0 (e.LCA.getD (e.ol + kidx) default) := by
415    have hh := hall kidx hk
416    by_cases hl : LenLink (e.LCA.getD (e.ol + kidx) default)
417    · rw [ite_eq_left hl] at hh; exact Or.inl ⟨hl, hh⟩
418    · rw [ite_eq_right hl] at hh; exact Or.inr hh
419  have hEd0 : (e.LCA.getD (e.ol + kidx) default).bits.toNat + 0 ≤ 15 := by
420    rcases hclass with h | h
421    · exact h.2.1
422    · exact h.1
423  obtain ⟨l1, h1, run1, result1⟩ := pass_entry_wp hc A msg m l i o s 0 (e.ol + kidx) hls hAsz ho hbroke
424    hs6 hsi hT (by omega) (by intro hi; have := hbi2 hi; omega) hhere hksz (by omega) hEd0 hclass
425  generalize firstCell : e.LCA.getD (e.ol + kidx) default = first at result1 hclass hEd0
426  rcases result1 with ⟨again1, broke1, heap1, link1, j, jLt, here1, jEq, locals1, bits1, stream1⟩ | end1
427  · subst heap1
428    have links : LinkOK LenLeaf e.LCA e.ol first := by
429      rcases hclass with h | h
430      · exact h.2
431      · rcases h.2 with h0 | h | h
432        · exact False.elim (link1.1 h0)
433        · exact False.elim (h.1 link1.2.1)
434        · exact False.elim (h.2 link1.2.2)
435    have leaf := links.2.2.2.2 j jLt
436    have secondIn : e.ol + first.val.toNat + j < e.LCA.size := by have := links.2.2.2.1; omega
437    obtain ⟨l2, h2, run2, result2⟩ := pass_entry_wp hc A msg m l1 i o s first.bits.toNat
438      (e.ol + first.val.toNat + j) locals1 hAsz ho broke1 hs6 hsi hT
439      (by omega) (by intro hi; have := hbi2 hi; omega) here1 secondIn
440      (by have := leaf.1; omega) leaf.1 (Or.inr leaf)
441    rcases result2 with ⟨_, _, _, link2, _⟩ | end2
442    · rcases leaf.2 with h0 | h | h
443      · exact False.elim (link2.1 h0)
444      · exact False.elim (h.1 link2.2.1)
445      · exact False.elim (h.2 link2.2.2)
446    · have cond1 : (fun q : L => (pure (q.againL, q) : M (Bool × L))) l1 (e.heap A msg m) =
447          .ok ((true, l1), e.heap A msg m) := by simp [again1]
448      have cond2 : (fun q : L => (pure (q.againL, q) : M (Bool × L))) l2 h2 =
449          .ok ((false, l2), h2) := by simp [end2.1.2.1]
450      refine Wp.of_eq (cdoWhile_two run1 cond1 run2 cond2)
451        ⟨e.LCA.getD (e.ol + first.val.toNat + j) default,
452          first.bits.toNat + (e.LCA.getD (e.ol + first.val.toNat + j) default).bits.toNat,
453          by have := leaf.1; omega, ?_, ?_⟩
454      · exact Or.inr ⟨first, j, firstCell, link1, jLt, jEq, rfl, rfl, by have := leaf.1; omega, end2.1.1⟩
455      · simpa only [stream1, List.drop_drop] using end2
456  · have cond1 : (fun q : L => (pure (q.againL, q) : M (Bool × L))) l1 h1 =
457        .ok ((false, l1), h1) := by simp [end1.1.2.1]
458    exact Wp.of_eq (cdoWhile_one run1 cond1)
459      ⟨first, first.bits.toNat, by omega, Or.inl ⟨firstCell, rfl, end1.1.1⟩, end1⟩
460
461private theorem root_entry_wp (hc : CtxOK e c) (A : Array UInt8) (msg : BPtr) (m : UInt32)
462    (l : L) (i o s : Nat) (hls : LS e l i o) (hAsz : A.size = e.A0.size)
463    (ho : o + 258 ≤ e.o0 + e.sm0.avail_out.toNat) (hbroke : l.broke = false)
464    (hs6 : s + 6 ≤ e.i0 + e.sm0.avail_in.toNat) (hsi : s ≤ i) (hT : i ≤ s + 2)
465    (hb15 : 15 ≤ l.bits.toNat) (hbi2 : i = s + 2 → 16 ≤ l.bits.toNat) :
466    Wp (do
467      let here ← c.lcode.add (l.hold &&& c.lmask.toUInt64).toNat
468      cdoWhile (dolen c) (fun l => pure (l.againL, l)) {l with here}) (e.heap A msg m)
469      (fun l' h' => ∃ entry consumed, consumed ≤ 15 ∧
470        LengthSemantics.Look e l.hold.toNat (l.hold.toNat % 2 ^ e.s0.lenbits.toNat) entry consumed ∧
471        EndWithDistanceEntry e c A msg m ((Sg e l.hold.toNat l.bits.toNat i).drop consumed) i o entry l' h') := by
472  have hlc : c.lcode = .ref e.rl e.ol := by rw [hc.lcode]; exact e.hlc
473  have hR : e.s0.lenbits.toNat < 32 := by have := e.hlt.1; omega
474  have hmask : c.lmask.toUInt64.toNat = 2 ^ e.s0.lenbits.toNat - 1 := by
475    rw [hc.lmask, UInt32.toNat_toUInt64]; exact u32_shl1_sub1 hR
476  have hidx := u64_and_mask (x := l.hold) hmask
477  have hmod : l.hold.toNat % 2 ^ e.s0.lenbits.toNat < 2 ^ e.s0.lenbits.toNat :=
478    Nat.mod_lt _ (Nat.pow_pos (by omega))
479  refine Wp.bindO (x := Ptr.ref e.rl (e.ol + l.hold.toNat % 2 ^ e.s0.lenbits.toNat)) ?_ ?_
480  · rw [hlc, hidx]
481    exact Ptr.add_nat_ok (e.heap_cget_LCA A msg m) (by have := e.hlt.2.1; omega)
482  · exact loop_entry_wp hc A msg m _ i o s _ (LS.congr hls rfl rfl rfl rfl)
483      hAsz ho hbroke hs6 hsi hT hb15 hbi2 hmod rfl
484
485private theorem body_entry_wp (e : Env) (c : Ctx) (A : Array UInt8) (msg : BPtr) (m : UInt32)
486    (l : L) (i o : Nat) (hp : StepPre e c A l i o) :
487    Wp (inflate_fast_body c l) (e.heap A msg m) (fun l' h' =>
488      Sg e (ready e l i).1.hold.toNat (ready e l i).1.bits.toNat (ready e l i).2 =
489        Sg e l.hold.toNat l.bits.toNat i ∧
490      ∃ entry consumed, consumed ≤ 15 ∧
491        LengthSemantics.Look e (ready e l i).1.hold.toNat
492          ((ready e l i).1.hold.toNat % 2 ^ e.s0.lenbits.toNat) entry consumed ∧
493        EndWithDistanceEntry e c A msg m ((Sg e (ready e l i).1.hold.toNat (ready e l i).1.bits.toNat
494          (ready e l i).2).drop consumed) (ready e l i).2 o entry l' h') := by
495  have hc := hp.context
496  have hls := hp.locals
497  have hAsz := hp.outputSize
498  have hi6 := hp.inputRoom
499  have ho258 := hp.outputRoom
500  have hbroke := hp.notStopped
501  have trace : Wp (inflate_fast_body c l) (e.heap A msg m) (fun l' h' =>
502      Sg e (ready e l i).1.hold.toNat (ready e l i).1.bits.toNat (ready e l i).2 =
503        Sg e l.hold.toNat l.bits.toNat i ∧
504      ∃ entry consumed, consumed ≤ 15 ∧
505        LengthSemantics.Look e (ready e l i).1.hold.toNat
506          ((ready e l i).1.hold.toNat % 2 ^ e.s0.lenbits.toNat) entry consumed ∧
507        EndWithDistanceEntry e c A msg m ((Sg e (ready e l i).1.hold.toNat (ready e l i).1.bits.toNat
508          (ready e l i).2).drop consumed) (ready e l i).2 o entry l' h') := by
509    unfold inflate_fast_body
510    by_cases h1 : l.bits < 15
511    · simp only [ready, h1, ite_true]
512      have hb : l.bits.toNat < 15 := by simpa using UInt32.lt_iff_toNat_lt.mp h1
513      have hiin : i < e.i0 + e.sm0.avail_in.toNat := by omega
514      refine Wp.bindO (pull_run e _ l i o hls (by omega) hiin (e.heap_bytes_in A msg m)) ?_
515      have hl1 := hls.pullL (by omega) hiin
516      have stream1 := Sg_pullL hls (by omega) hiin
517      have hb1 := pullL_bits l (e.IN.getD i 0) (.ref (.blk e.ib) (i + 1)) hls.hb
518      have hi2 : i + 1 < e.i0 + e.sm0.avail_in.toNat := by omega
519      have hb1' : (pullL l (e.IN.getD i 0) (.ref (.blk e.ib) (i + 1))).bits.toNat ≤ 22 := by
520        simp only [pullL] at hb1 ⊢; omega
521      refine Wp.bindO (pull_run e _ _ (i + 1) o hl1 hb1' hi2 (e.heap_bytes_in A msg m)) ?_
522      have hl2 := hl1.pullL hb1' hi2
523      have stream2 := Sg_pullL hl1 hb1' hi2
524      have hb2 := pullL_bits (pullL l (e.IN.getD i 0) (.ref (.blk e.ib) (i + 1)))
525        (e.IN.getD (i + 1) 0) (.ref (.blk e.ib) (i + 1 + 1)) hl1.hb
526      refine Wp.mono (root_entry_wp hc A msg m _ (i + 1 + 1) o i hl2 hAsz ho258 hbroke hi6 (by omega) (by omega)
527        (by simp only [pullL] at hb1 hb2 ⊢; omega)
528        (by intro _; simp only [pullL] at hb1 hb2 ⊢; omega)) ?_
529      intro l' h' result
530      exact ⟨stream2.trans stream1, result⟩
531    · simp only [ready, h1, ite_false]
532      have hb : 15 ≤ l.bits.toNat := by
533        have : ¬ l.bits.toNat < 15 := fun h => h1 (UInt32.lt_iff_toNat_lt.mpr (by simpa using h))
534        omega
535      exact Wp.mono (root_entry_wp hc A msg m l i o i hls hAsz ho258 hbroke hi6 (by omega) (by omega) hb (by omega))
536        (fun _ _ result => ⟨by trivial, result⟩)
537  exact trace
538
539private theorem ready_locals (e : Env) (c : Ctx) (A : Array UInt8)
540    (l : L) (i o : Nat) (pre : StepPre e c A l i o) :
541    LS e (ready e l i).1 (ready e l i).2 o ∧ 15 ≤ (ready e l i).1.bits.toNat := by
542  by_cases short : l.bits < 15
543  · have bitsLt : l.bits.toNat < 15 := by simpa using UInt32.lt_iff_toNat_lt.mp short
544    have in1 : i < e.i0 + e.sm0.avail_in.toNat := by have := pre.inputRoom; omega
545    have first := pre.locals.pullL (by omega) in1
546    have bits1 := pullL_bits l (e.IN.getD i 0) (.ref (.blk e.ib) (i + 1)) pre.locals.hb
547    have bound1 : (pullL l (e.IN.getD i 0) (.ref (.blk e.ib) (i + 1))).bits.toNat ≤ 22 := by
548      simp only [pullL] at bits1 ⊢; omega
549    have in2 : i + 1 < e.i0 + e.sm0.avail_in.toNat := by have := pre.inputRoom; omega
550    have second := first.pullL bound1 in2
551    have bits2 := pullL_bits (pullL l (e.IN.getD i 0) (.ref (.blk e.ib) (i + 1)))
552      (e.IN.getD (i + 1) 0) (.ref (.blk e.ib) (i + 1 + 1)) first.hb
553    simp only [ready, short, ite_true]
554    constructor
555    · simpa only [Nat.add_assoc] using second
556    · simp only [pullL] at bits1 bits2 ⊢; omega
557  · simp only [ready, short, ite_false]
558    refine ⟨pre.locals, ?_⟩
559    have large : ¬ l.bits.toNat < 15 := fun h => short (UInt32.lt_iff_toNat_lt.mpr (by simpa using h))
560    omega
561
562
563
564theorem actual_body_refines_token : BodyToken.Goal.actual_body_refines_token := by
565  intro e c bytes msg mode l input output L D pre tables
566  obtain ⟨l', after, run, sameStream, entry, consumed, limit, look, oldEnd, tail⟩ :=
567    body_entry_wp e c bytes msg mode l input output pre
568  have safe := Wp.at_run (inflate_fast_body_step_safe e c bytes msg mode l input output pre) run
569  obtain ⟨readyLS, enough⟩ := ready_locals e c bytes l input output pre
570  obtain ⟨usedL, invL⟩ := tables.lengthTable
571  obtain ⟨query, positive, codeBound, leaf, semantic⟩ := length_lookup_matches_format e
572    (ready e l input).1.hold.toNat (ready e l input).1.bits.toNat (ready e l input).2
573    usedL L entry consumed invL tables.lengthStable tables.lengthFlags readyLS.hH enough look
574  rw [sameStream] at semantic oldEnd tail
575  have acceptedMeaning (accepts : FastTableFlags.FastLeafAccepted LENS entry) :
576      ∃ symbol, symbol ≤ 285 ∧ DecodeSemantics.SymbolEntry LENS symbol entry ∧
577        consumed = L.getD symbol 0 ∧
578        decodeSym L (Sg e l.hold.toNat l.bits.toNat input) =
579          some (symbol, (Sg e l.hold.toNat l.bits.toNat input).drop consumed) := by
580    rcases semantic with ⟨rejects, _⟩ | ⟨_, symbol, valid, meaning, length, decoded, _⟩
581    · exact False.elim (rejects accepts)
582    · exact ⟨symbol, valid, meaning, length, decoded⟩
583  have bgLe : e.bg ≤ output := Nat.le_trans e.bg_le pre.locals.ho0
584  have outSize : output < bytes.size := by
585    have := pre.outputRoom
586    have endSize := e.hAsz
587    rw [← pre.outputSize] at endSize
588    omega
589  rcases oldEnd.2.2 with literal | length | eob | invalid
590  · obtain ⟨hop, stopped, locals, rest, heap⟩ := literal
591    have accepts : FastTableFlags.FastLeafAccepted LENS entry := by
592      simp [FastTableFlags.FastLeafAccepted, hop]
593    obtain ⟨symbol, valid, meaning, _, decoded⟩ := acceptedMeaning accepts
594    obtain ⟨small, value⟩ := literal_symbol symbol entry valid meaning hop
595    refine ⟨l', after, (ready e l input).2, output + 1, bytes.set! output entry.val.toUInt8,
596      msg, mode, run, safe, locals, by simp, heap, Or.inl ⟨stopped, ?_⟩⟩
597    have written := written_set_append bytes output (output - e.bg) entry.val.toUInt8 (by omega) outSize
598    have count : output + 1 - e.bg = output - e.bg + 1 := by omega
599    rw [count, written, rest]
600    have byte : entry.val.toUInt8 = symbol.toUInt8 := by
601      apply UInt8.toNat_inj.mp
602      simp only [UInt16.toNat_toUInt8, UInt8.toNat_ofNat']
603      rw [value]
604    rw [byte]
605    exact Token.Step.literal decoded small
606  · obtain ⟨nonzero, hasBase, _⟩ := length
607    have accepts : FastTableFlags.FastLeafAccepted LENS entry := by
608      simp [FastTableFlags.FastLeafAccepted, hasBase]
609    obtain ⟨symbol, valid, meaning, _, decoded⟩ := acceptedMeaning accepts
610    have lower := base_symbol symbol entry valid meaning hasBase
611    obtain ⟨_, extraBits, baseValue⟩ := length_base_fields symbol entry lower valid meaning
612    obtain ⟨input2, xl, r2, _, _, readLength, distEntry⟩ := tail ⟨nonzero, hasBase⟩
613    obtain ⟨dl, di, _, _, dlLocals, dlRunning, dlLength, dlBits, dlRoom, dlSource, dlRun⟩ := distEntry
614    have lenBase : 3 ≤ entry.val.toNat ∧
615        entry.val.toNat + 2 ^ (entry.op &&& 15).toNat ≤ 259 := by
616      rcases leaf.2 with literal | base | invalid
617      · exact False.elim (nonzero literal)
618      · exact base.2.2
619      · exact False.elim (hasBase invalid.1)
620    have xlBound := readBits_value_lt readLength
621    have dlLen : 3 ≤ dl.len.toNat ∧ dl.len.toNat ≤ 258 := by omega
622    obtain ⟨usedD, invD⟩ := tables.distanceTable
623    obtain ⟨dl', dh, distanceEntry, dc, distanceRun, _, _, _, outcome⟩ := actual_distance_refines_lz77
624      e c bytes msg mode dl di output usedD D pre.context dlLocals
625      (by rw [pre.outputSize]; exact e.hAsz) pre.outputRoom
626      (by rw [pre.outputSize]; exact e.hAbig) dlRunning dlLen dlBits dlRoom
627      invD tables.distanceStable tables.distanceFlags
628    have sameRun := distanceRun.symm.trans dlRun
629    cases sameRun
630    unfold DistanceResult.Outcome at outcome
631    dsimp only at outcome
632    rw [dlSource] at outcome
633    rw [extraBits] at readLength
634    rcases outcome with ⟨noBase, rejected, di', errorMsg, stopped, locals, rest, heap⟩ |
635      ⟨base, distanceSymbol, xd, codeRest, finalRest, distanceValid, distanceMeaning, _,
636        distanceDecoded, readDistance, copy⟩
637    · refine ⟨l', after, di', output, bytes, errorMsg, BAD, run, safe, locals, rfl, heap,
638        Or.inr (Or.inr ⟨stopped, rfl, rfl, ?_⟩)⟩
639      exact Token.Rejected.distance decoded lower valid readLength rejected
640    · by_cases tooFar : (MatchHistory.saved e.W e.s0.wsize.toNat e.s0.wnext.toNat
641          e.s0.whave.toNat e.woff).length + (writtenBytes bytes output (output - e.bg)).length <
642          distBases.getD distanceSymbol 0 + xd
643      · rw [ite_eq_left tooFar] at copy
644        obtain ⟨di', errorMsg, stopped, locals, rest, heap⟩ := copy
645        refine ⟨l', after, di', output, bytes, errorMsg, BAD, run, safe, locals, rfl, heap,
646          Or.inr (Or.inr ⟨stopped, rfl, rfl, ?_⟩)⟩
647        exact Token.Rejected.tooFar decoded lower valid readLength distanceDecoded distanceValid
648          readDistance (by simpa only [List.length_append] using tooFar)
649      · rw [ite_eq_right tooFar] at copy
650        obtain ⟨di', stopped, locals, rest, heap, written⟩ := copy
651        refine ⟨l', after, di', output + dl.len.toNat, _, msg, mode, run, safe, locals,
652          matchArr_size _ _ _ _ _ _ _ _ _, heap, Or.inl ⟨stopped, ?_⟩⟩
653        have count : output + dl.len.toNat - e.bg = output - e.bg + dl.len.toNat := by omega
654        rw [count, written, rest, dlLength, baseValue]
655        exact Token.Step.copy decoded lower valid readLength distanceDecoded distanceValid readDistance
656          (by simp only [List.length_append]; omega)
657  · obtain ⟨nonzero, noBase, invalidFlag, endFlag, stopped, locals, rest, heap⟩ := eob
658    have accepts : FastTableFlags.FastLeafAccepted LENS entry := by
659      simp [FastTableFlags.FastLeafAccepted, invalidFlag, endFlag]
660    obtain ⟨symbol, valid, meaning, _, decoded⟩ := acceptedMeaning accepts
661    have symbolIsEnd := eob_symbol symbol entry valid meaning nonzero noBase
662    subst symbol
663    refine ⟨l', after, (ready e l input).2, output, bytes, msg, TYPE,
664      run, safe, locals, rfl, heap, Or.inr (Or.inl ⟨stopped, rfl, ?_⟩)⟩
665    rw [rest]
666    exact Token.Step.eob decoded
667  · obtain ⟨nonzero, noBase, invalidFlag, noEnd, stopped, locals, rest, errorMsg, heap⟩ := invalid
668    have rejects : ¬ FastTableFlags.FastLeafAccepted LENS entry := by
669      simp [FastTableFlags.FastLeafAccepted, nonzero, noBase, noEnd]
670    have future : ∀ more : List Bool,
671        ¬ ∃ symbol remaining, decodeSym L (Sg e l.hold.toNat l.bits.toNat input ++ more) =
672          some (symbol, remaining) ∧ symbol ≤ 285 := by
673      rcases semantic with ⟨_, allFuture⟩ | ⟨accepts, _⟩
674      · exact allFuture
675      · exact False.elim (rejects accepts)
676    refine ⟨l', after, (ready e l input).2, output, bytes, errorMsg, BAD,
677      run, safe, locals, rfl, heap, Or.inr (Or.inr ⟨stopped, rfl, rfl, ?_⟩)⟩
678    exact Token.Rejected.length future
679
680end Zlib.Inffast.Proofs.BodyTokenProof
681
682namespace Zlib.Inffast.Proofs
683/-- The actual fast body emits one independent token, ends the block,
684or rejects the current token without emitting output. -/
685theorem actual_body_refines_token : Spec.BodyToken.Goal.actual_body_refines_token :=
686  BodyTokenProof.actual_body_refines_token
687end Zlib.Inffast.Proofs