deflate.c.engine.lmmain.lean

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

1import ZlibF.Proof.«deflate.c.engine.lmbody»
2
3/-!
4# deflate.c, engine: `longest_match`
5
6`longest_match_ok`: under the environment `LMEnv` (window block, `prev` block, position facts and the chain facts that
7the hash invariant H gives), the function does not fault, only `match_start` changes, and it returns
8`min(best_len, lookahead)` where `prev_length <= best_len <= 258` and either `best_len = prev_length` with `match_start`
9unchanged, or `match_start` names a match: it lies before `strstart`, within `MAX_DIST`, and the window bytes at
10`match_start` and at `strstart` agree on the first `best_len` bytes (so on the returned length).
11-/
12
13namespace Zlib.Deflate.Engine.Proofs
14open C Zlib.Deflate
15
16/-- The condition of the `longest_match` loop, as in the translation. -/
17def lmCond (prev : WPtr) (wmask limit : UInt32) : LMState → M (Bool × LMState) := fun st => do
18  if st.brk then return (false, st)
19  let cm : UInt32 := (← Ptr.index prev (st.cur_match &&& wmask).toNat).toUInt32
20  let st := { st with cur_match := cm }
21  if cm > limit then
22    let cl := st.chain_length - 1
23    return (cl != 0, { st with chain_length := cl })
24  return (false, st)
25
26theorem longest_match_unfold (s : DeflateStatePtr) (cur_match : UInt32) : longest_match s cur_match = (do
27  let d ← ldDeflateState s
28  let mut chain_length : UInt32 := d.max_chain_length
29  let scan ← padd d.window d.strstart.toNat
30  let best_len : Int32 := d.prev_length.toInt32
31  let mut nice_match : Int32 := d.nice_match
32  let maxd : UInt32 := d.w_size - MIN_LOOKAHEAD_u
33  let limit : UInt32 := if d.strstart > maxd then d.strstart - maxd else 0
34  let prev := d.prev
35  let wmask := d.w_mask
36  let _strend ← padd (← padd d.window d.strstart.toNat) MAX_MATCH_u.toNat
37  let scan_end1 ← index8 scan (← isub best_len 1).toInt
38  let scan_end ← index8 scan best_len.toInt
39  if d.prev_length ≥ d.good_match then chain_length := chain_length >>> 2
40  if nice_match.toUInt32 > d.lookahead then nice_match := d.lookahead.toInt32
41  let st ← cdoWhile (lm_body s) (lmCond prev wmask limit)
42    { cur_match, chain_length, best_len, nice_match, scan, scan_end1, scan_end, brk := false }
43  let lookahead ← rd s (·.lookahead)
44  if st.best_len.toUInt32 ≤ lookahead then return st.best_len.toUInt32
45  return lookahead) := rfl
46
47/-- The state after the condition read `v = prev[cur_match & wmask]` and set the counter to `cl`. -/
48def lmStep (st1 : LMState) (v : UInt16) (cl : UInt32) : LMState := { st1 with cur_match := v.toUInt32, chain_length := cl }
49
50/-- What the loop guarantees at its end (or at `break`). -/
51def LMOut (h0 : Heap) (sr : Nat) (d : DeflateState) (wa : Array UInt8) (st : LMState) (h : Heap) : Prop :=
52  ∃ (ms : UInt32) (b : Nat), h = hAt h0 sr d ms ∧ st.best_len.toInt = (b : Int) ∧ d.prev_length.toNat ≤ b ∧ b ≤ 258 ∧
53    ((b = d.prev_length.toNat ∧ ms = d.match_start) ∨
54     (d.prev_length.toNat < b ∧ GoodMatch wa d.strstart.toNat d.w_size.toNat ms.toNat b))
55
56theorem LMInv.out {h0 : Heap} {sr wb pb : Nat} {d : DeflateState} {wa : Array UInt8} {pa : Array UInt16} {c : UInt32}
57    {st : LMState} {h : Heap} (hI : LMInv h0 sr d wb pb wa pa c st h) : LMOut h0 sr d wa st h := by
58  obtain ⟨ms, b, hh, _, hb, hpl, hb258, _, _, hgood⟩ := hI
59  exact ⟨ms, b, hh, hb, hpl, hb258, hgood⟩
60
61theorem u32_toInt32_toInt (x : UInt32) (hx : x.toNat < 2 ^ 31) : x.toInt32.toInt = (x.toNat : Int) := by
62  have h1 : x.toInt32.toInt = x.toBitVec.toInt := rfl
63  rw [BitVec.toInt_eq_toNat_cond] at h1
64  have : x.toBitVec.toNat = x.toNat := rfl
65  rw [this] at h1
66  split at h1 <;> omega
67
68theorem i32_toUInt32_toNat (x : Int32) (b : Nat) (hx : x.toInt = (b : Int)) (hb : b < 2 ^ 31) : x.toUInt32.toNat = b := by
69  have h1 : x.toInt = x.toBitVec.toInt := rfl
70  rw [BitVec.toInt_eq_toNat_cond] at h1
71  have : x.toUInt32.toNat = x.toBitVec.toNat := rfl
72  rw [this]
73  split at h1 <;> omega
74
75/-- **The loop.** From a state with the invariant and `brk = false`, the loop does not fault and ends in a state
76that satisfies `LMOut`. The measure is `cur_match`, which falls at every step because `prev[p & wmask] < p` (H). -/
77theorem lm_loop_ok {h0 : Heap} {sr wb pb : Nat} {d : DeflateState} {wa : Array UInt8} {pa : Array UInt16} {c : UInt32}
78    (E : LMEnv h0 sr d wb pb wa pa c) (limit : UInt32) (hlimit : limit.toNat = lmLimit d.strstart.toNat (d.w_size.toNat - 262))
79    (st : LMState) (h : Heap) (hbrk : st.brk = false) (hI : LMInv h0 sr d wb pb wa pa c st h) :
80    ∃ st' h', cdoWhile (lm_body (some (.tab sr))) (lmCond d.prev d.w_mask limit) st h = .ok (st', h') ∧
81      LMOut h0 sr d wa st' h' := by
82  have key := cdoWhile_measure (σ := LMState) (body := lm_body (some (.tab sr))) (cond := lmCond d.prev d.w_mask limit)
83    (fun st h => st.brk = false ∧ LMInv h0 sr d wb pb wa pa c st h) (fun st => st.cur_match.toNat)
84    (fun st h => LMOut h0 sr d wa st h) ?_ (s := st) (h := h) ⟨hbrk, hI⟩
85    (by unfold fuel; have := st.cur_match.toNat_lt; omega)
86  · exact key
87  · intro st h hIn
88    obtain ⟨hbrk, hI⟩ := hIn
89    obtain ⟨st1, h1, hrun, hI1, hcur, hcl, hnm⟩ := lm_body_ok E st hbrk hI
90    have hout := hI1.out
91    by_cases hb1 : st1.brk = true
92    · exact ⟨st1, h1, false, st1, h1, hrun, by simp [lmCond, hb1], fun _ => hout, by simp⟩
93    have hb1' : st1.brk = false := by simpa using hb1
94    obtain ⟨k, hk, hk9, hk15⟩ := E.wsb
95    have hws9 : 512 ≤ d.w_size.toNat := by
96      rw [hk]; calc 512 = 2 ^ 9 := by decide
97        _ ≤ 2 ^ k := Nat.pow_le_pow_right (by decide) hk9
98    have hI1' := hI1
99    obtain ⟨ms1, b1, hh1, hscan1, hb, hpl, hb258, hse', hch1, hgood1⟩ := hI1'
100    obtain ⟨hcm1, hcmlt, hcmprev, _⟩ := E.chain _ hch1
101    have hwm : d.w_mask.toNat = d.w_size.toNat - 1 := by
102      rw [E.wmask, UInt32.toNat_sub_of_le _ _ (by rw [UInt32.le_iff_toNat_le]; simp; omega)]
103      simp
104    have hidx : (st1.cur_match &&& d.w_mask).toNat = st1.cur_match.toNat &&& (d.w_size.toNat - 1) := by
105      rw [UInt32.toNat_and, hwm]
106    have hidx_lt : st1.cur_match.toNat &&& (d.w_size.toNat - 1) < d.w_size.toNat :=
107      and_wm_lt (by rw [hk]) _
108    have hpw : h1.words pb = some pa := by rw [hh1]; exact E.pwords
109    have hidx_arr : st1.cur_match.toNat &&& (d.w_size.toNat - 1) < pa.size := by have := E.psize; omega
110    have hrd : Ptr.index d.prev (↑(st1.cur_match &&& d.w_mask).toNat) h1 =
111        .ok (wfn pa (st1.cur_match.toNat &&& (d.w_size.toNat - 1)), h1) := by
112      rw [E.prevp, hidx]
113      have := Ptr.index_ok (h := h1) (r := WRef.blk pb) (a := pa) (off := 0)
114        (i := st1.cur_match.toNat &&& (d.w_size.toNat - 1)) (by simpa using hpw) (by omega)
115      unfold OkOn at this
116      simp only [Nat.zero_add] at this
117      rw [this, wfn_getElem _ _ hidx_arr]
118    by_cases big : limit.toNat < (wfn pa (st1.cur_match.toNat &&& (d.w_size.toNat - 1))).toNat
119    · have hgt : limit < (wfn pa (st1.cur_match.toNat &&& (d.w_size.toNat - 1))).toUInt32 := by
120        rw [UInt32.lt_iff_toNat_lt]; simpa using big
121      have hch2 : Chain (wfn pa) (d.w_size.toNat - 1) (lmLimit d.strstart.toNat (d.w_size.toNat - 262)) c.toNat
122          (wfn pa (st1.cur_match.toNat &&& (d.w_size.toNat - 1))).toNat :=
123        Chain.step hch1 rfl (by rw [← hlimit]; exact big)
124      by_cases hcl0 : (st1.chain_length - 1 != 0) = true
125      · refine ⟨st1, h1, true, lmStep st1 (wfn pa (st1.cur_match.toNat &&& (d.w_size.toNat - 1))) (st1.chain_length - 1), h1, hrun, ?_, by simp, ?_⟩
126        · simp only [lmCond, bind_app, pure_app, M_ite_app, hb1', Bool.false_eq_true, ↓reduceIte, hrd, GT.gt, hgt, hcl0, lmStep]
127        · intro _
128          refine ⟨⟨hb1', ms1, b1, hh1, hscan1, hb, hpl, hb258, hse', ?_, hgood1⟩, ?_⟩
129          · simpa [lmStep] using hch2
130          · simp only [lmStep, hcur] at hcmprev ⊢
131            simpa using hcmprev
132      · have hcl0' : (st1.chain_length - 1 != 0) = false := by simpa using hcl0
133        refine ⟨st1, h1, false, lmStep st1 (wfn pa (st1.cur_match.toNat &&& (d.w_size.toNat - 1))) (st1.chain_length - 1), h1, hrun, ?_, fun _ => hout, by simp⟩
134        simp only [lmCond, bind_app, pure_app, M_ite_app, hb1', Bool.false_eq_true, ↓reduceIte, hrd, GT.gt, hgt, hcl0', lmStep]
135    · have hng : ¬ limit < (wfn pa (st1.cur_match.toNat &&& (d.w_size.toNat - 1))).toUInt32 := by
136        rw [UInt32.lt_iff_toNat_lt]; simpa using big
137      refine ⟨st1, h1, false, lmStep st1 (wfn pa (st1.cur_match.toNat &&& (d.w_size.toNat - 1))) st1.chain_length, h1, hrun, ?_, fun _ => hout, by simp⟩
138      simp only [lmCond, bind_app, pure_app, M_ite_app, hb1', Bool.false_eq_true, ↓reduceIte, hrd, GT.gt, hng, lmStep]
139
140theorem hAt_self (h0 : Heap) (sr : Nat) (d : DeflateState) (hd : h0.dstates sr = some d) :
141    hAt h0 sr d d.match_start = h0 := by
142  simp [hAt, upd_self _ _ _ hd]
143
144/-- The initial state of the loop satisfies the invariant, whatever `chain_length` and `nice_match` are. -/
145theorem lm_init_inv {h0 : Heap} {sr wb pb : Nat} {d : DeflateState} {wa : Array UInt8} {pa : Array UInt16} {c : UInt32}
146    (E : LMEnv h0 sr d wb pb wa pa c) (cl : UInt32) (nm : Int32) :
147    LMInv h0 sr d wb pb wa pa c
148      { cur_match := c, chain_length := cl, best_len := d.prev_length.toInt32, nice_match := nm,
149        scan := Ptr.ref (BRef.blk wb) d.strstart.toNat,
150        scan_end1 := bfn wa (d.strstart.toNat + d.prev_length.toNat - 1),
151        scan_end := bfn wa (d.strstart.toNat + d.prev_length.toNat), brk := false } h0 := by
152  have h31 : d.prev_length.toNat < 2 ^ 31 := by have := E.plle; omega
153  refine ⟨d.match_start, d.prev_length.toNat, (hAt_self h0 sr d E.hd).symm, rfl, u32_toInt32_toInt _ h31, Nat.le_refl _,
154    E.plle, fun _ => ⟨rfl, rfl⟩, ?_, Or.inl ⟨rfl, rfl⟩⟩
155  exact Chain.start
156
157theorem lm_loop_total {h0 : Heap} {sr wb pb : Nat} {d : DeflateState} {wa : Array UInt8} {pa : Array UInt16} {c : UInt32}
158    (E : LMEnv h0 sr d wb pb wa pa c) (limit : UInt32) (hlimit : limit.toNat = lmLimit d.strstart.toNat (d.w_size.toNat - 262))
159    (st : LMState) (h : Heap) (hbrk : st.brk = false) (hI : LMInv h0 sr d wb pb wa pa c st h)
160    (res : Except Fault (LMState × Heap)) (hres : cdoWhile (lm_body (some (.tab sr))) (lmCond d.prev d.w_mask limit) st h = res) :
161    ∃ st' h', res = .ok (st', h') ∧ LMOut h0 sr d wa st' h' := by
162  obtain ⟨st', h', hr, ho⟩ := lm_loop_ok E limit hlimit st h hbrk hI
163  exact ⟨st', h', hres.symm.trans hr, ho⟩
164
165
166/-- The part of `longest_match` after the two tests on `prev_length` and `lookahead`: the loop and the final `min`. -/
167def lmRest (sr : Nat) (L : UInt32) (d : DeflateState) (c : UInt32) (wb : Nat) (wa : Array UInt8) (cl : UInt32) (nm : Int32) :
168    M UInt32 := do
169  let st ← cdoWhile (lm_body (some (.tab sr))) (lmCond d.prev d.w_mask L)
170      { cur_match := c, chain_length := cl, best_len := d.prev_length.toInt32, nice_match := nm,
171        scan := Ptr.ref (BRef.blk wb) d.strstart.toNat,
172        scan_end1 := bfn wa (d.strstart.toNat + d.prev_length.toNat - 1),
173        scan_end := bfn wa (d.strstart.toNat + d.prev_length.toNat), brk := false }
174  let lookahead ← rd (some (.tab sr)) (fun x => x.lookahead)
175  if st.best_len.toUInt32 ≤ lookahead then return st.best_len.toUInt32
176  return lookahead
177
178theorem lmRest_ok {h0 : Heap} {sr wb pb : Nat} {d : DeflateState} {wa : Array UInt8} {pa : Array UInt16} {c : UInt32}
179    (E : LMEnv h0 sr d wb pb wa pa c) (L : UInt32)
180    (hlimit : L.toNat = lmLimit d.strstart.toNat (d.w_size.toNat - 262)) (cl : UInt32) (nm : Int32) :
181    ∃ (r : UInt32) (h' : Heap) (ms : UInt32) (best : Nat),
182      lmRest sr L d c wb wa cl nm h0 = .ok (r, h') ∧
183      r = UInt32.ofNat (lmResult best d.lookahead.toNat) ∧ h' = hAt h0 sr d ms ∧
184      d.prev_length.toNat ≤ best ∧ best ≤ 258 ∧
185      ((best = d.prev_length.toNat ∧ ms = d.match_start) ∨
186       (d.prev_length.toNat < best ∧ GoodMatch wa d.strstart.toNat d.w_size.toNat ms.toNat best)) := by
187  obtain ⟨st', h', hrun, ms, b, hh, hb, hpl, hb258, hgood⟩ :=
188    lm_loop_ok E L hlimit _ h0 rfl (lm_init_inv E cl nm)
189  subst hh
190  have hdd : (hAt h0 sr d ms).dstates sr = some { d with match_start := ms } := by simp [hAt]
191  have hrd : rd (some (.tab sr)) (fun x => x.lookahead) (hAt h0 sr d ms) = .ok (d.lookahead, hAt h0 sr d ms) := by
192    simp [rd, ldDeflateState_tab hdd]
193  have hbn : st'.best_len.toUInt32.toNat = b := i32_toUInt32_toNat _ b hb (by omega)
194  have hbu : st'.best_len.toUInt32 = UInt32.ofNat b := by
195    apply UInt32.toNat_inj.mp; rw [hbn]; simp; omega
196  by_cases hle : b ≤ d.lookahead.toNat
197  · have hle' : st'.best_len.toUInt32 ≤ d.lookahead := by
198      rw [UInt32.le_iff_toNat_le, hbn]; exact hle
199    refine ⟨st'.best_len.toUInt32, hAt h0 sr d ms, ms, b, ?_, ?_, rfl, hpl, hb258, hgood⟩
200    · simp only [lmRest, bind_app, pure_app, M_ite_app, hrun, hrd, hle', ite_true]
201    · rw [hbu]; unfold lmResult; rw [ite_eq_left hle]
202  · have hle' : ¬ st'.best_len.toUInt32 ≤ d.lookahead := by
203      rw [UInt32.le_iff_toNat_le, hbn]; exact hle
204    refine ⟨d.lookahead, hAt h0 sr d ms, ms, b, ?_, ?_, rfl, hpl, hb258, hgood⟩
205    · simp only [lmRest, bind_app, pure_app, M_ite_app, hrun, hrd, hle', ite_false]
206    · unfold lmResult; rw [ite_eq_right hle]; simp
207
208/-- **longest_match, safety and specification.** Under `LMEnv` the call does not fault and only `match_start` changes
209(the result heap is `hAt h0 sr d ms`). It returns `min(best, lookahead)` for some `best` with
210`prev_length <= best <= 258`; either `best = prev_length` and `match_start` is unchanged, or `match_start` names a good
211match of length `best`: before `strstart`, within `MAX_DIST`, and the window bytes agree on the first `best` bytes. -/
212theorem longest_match_ok {h0 : Heap} {sr wb pb : Nat} {d : DeflateState} {wa : Array UInt8} {pa : Array UInt16} {c : UInt32}
213    (E : LMEnv h0 sr d wb pb wa pa c) :
214    ∃ (r : UInt32) (h' : Heap) (ms : UInt32) (best : Nat),
215      longest_match (some (.tab sr)) c h0 = .ok (r, h') ∧
216      r = UInt32.ofNat (lmResult best d.lookahead.toNat) ∧ h' = hAt h0 sr d ms ∧
217      d.prev_length.toNat ≤ best ∧ best ≤ 258 ∧
218      ((best = d.prev_length.toNat ∧ ms = d.match_start) ∨
219       (d.prev_length.toNat < best ∧ GoodMatch wa d.strstart.toNat d.w_size.toNat ms.toNat best)) := by
220  obtain ⟨k, hk, hk9, hk15⟩ := E.wsb
221  have hws9 : 512 ≤ d.w_size.toNat := by
222    rw [hk]; calc 512 = 2 ^ 9 := by decide
223      _ ≤ 2 ^ k := Nat.pow_le_pow_right (by decide) hk9
224  have hws15 : d.w_size.toNat ≤ 32768 := by
225    rw [hk]; calc 2 ^ k ≤ 2 ^ 15 := Nat.pow_le_pow_right (by decide) hk15
226      _ = 32768 := by decide
227  have hroom := E.room
228  have hasz := E.asize
229  have hss : d.strstart.toNat + 258 < wa.size := by omega
230  have hss2 : 2 ≤ d.strstart.toNat := by have := E.c1; have := E.clt; omega
231  have hmm : MAX_MATCH_u.toNat = 258 := rfl
232  have h1i : (1 : Int32).toInt = 1 := by decide
233  have hpl := E.plle
234  have e_ld0 : ldDeflateState (some (.tab sr)) h0 = .ok (d, h0) := ldDeflateState_tab E.hd
235  have hbytes : h0.bytes wb = some wa := E.wbytes
236  have f14 : padd (Ptr.ref (BRef.blk wb) 0) d.strstart.toNat h0 = .ok (Ptr.ref (BRef.blk wb) d.strstart.toNat, h0) := by
237    simpa using padd_ok' (h := h0) (r := BRef.blk wb) (a := wa) (off := 0) (n := d.strstart.toNat)
238      (by simpa using hbytes) (by omega)
239  have f15 : padd (Ptr.ref (BRef.blk wb) d.strstart.toNat) 258 h0 =
240      .ok (Ptr.ref (BRef.blk wb) (d.strstart.toNat + 258), h0) := padd_ok' (by simpa using hbytes) (by omega)
241  have i0 : d.prev_length.toInt32.toInt = (d.prev_length.toNat : Int) := u32_toInt32_toInt _ (by omega)
242  have i4 : isub d.prev_length.toInt32 1 h0 = .ok (Int32.ofInt ((d.prev_length.toNat : Int) - 1), h0) := by
243    rw [isub_ok _ 1 (by rw [i0, h1i]; omega), i0, h1i]
244  have i5' : (Int32.ofInt ((d.prev_length.toNat : Int) - 1)).toInt = (d.prev_length.toNat : Int) - 1 :=
245    Int32.toInt_ofInt_of_le (by omega) (by omega)
246  have i5 : index8 (Ptr.ref (BRef.blk wb) d.strstart.toNat) ((d.prev_length.toNat : Int) - 1) h0 =
247      .ok (bfn wa (d.strstart.toNat + d.prev_length.toNat - 1), h0) := index8_bfn hbytes (by omega) (by omega)
248  have i6 : index8 (Ptr.ref (BRef.blk wb) d.strstart.toNat) (d.prev_length.toNat : Int) h0 =
249      .ok (bfn wa (d.strstart.toNat + d.prev_length.toNat), h0) := index8_bfn hbytes (by omega) (by omega)
250  have hmin : MIN_LOOKAHEAD_u.toNat = 262 := rfl
251  have hsub : (d.w_size - MIN_LOOKAHEAD_u).toNat = d.w_size.toNat - 262 := by
252    rw [UInt32.toNat_sub_of_le _ _ (by rw [UInt32.le_iff_toNat_le, hmin]; omega), hmin]
253  obtain ⟨L, hL⟩ : ∃ L : UInt32, L = (if d.strstart > d.w_size - MIN_LOOKAHEAD_u then d.strstart - (d.w_size - MIN_LOOKAHEAD_u) else 0) :=
254    ⟨_, rfl⟩
255  have hlimit : L.toNat = lmLimit d.strstart.toNat (d.w_size.toNat - 262) := by
256    rw [hL]; unfold lmLimit
257    by_cases hg : d.strstart > d.w_size - MIN_LOOKAHEAD_u
258    · have hg' : d.strstart.toNat > d.w_size.toNat - 262 := by
259        rw [GT.gt, UInt32.lt_iff_toNat_lt, hsub] at hg; exact hg
260      rw [ite_eq_left hg, ite_eq_left hg', UInt32.toNat_sub_of_le _ _ (by rw [UInt32.le_iff_toNat_le]; rw [GT.gt, UInt32.lt_iff_toNat_lt] at hg; omega), hsub]
261    · have hg' : ¬ d.strstart.toNat > d.w_size.toNat - 262 := by
262        intro hh; apply hg; rw [GT.gt, UInt32.lt_iff_toNat_lt, hsub]; exact hh
263      rw [ite_eq_right hg, ite_eq_right hg']; rfl
264  have hLsame : (if d.strstart > d.w_size - MIN_LOOKAHEAD_u then d.strstart - (d.w_size - MIN_LOOKAHEAD_u) else 0) = L := hL.symm
265  have key : ∀ (cl : UInt32) (nm : Int32), ∃ (r : UInt32) (h' : Heap) (ms : UInt32) (best : Nat),
266      lmRest sr L d c wb wa cl nm h0 = .ok (r, h') ∧
267      r = UInt32.ofNat (lmResult best d.lookahead.toNat) ∧ h' = hAt h0 sr d ms ∧
268      d.prev_length.toNat ≤ best ∧ best ≤ 258 ∧
269      ((best = d.prev_length.toNat ∧ ms = d.match_start) ∨
270       (d.prev_length.toNat < best ∧ GoodMatch wa d.strstart.toNat d.w_size.toNat ms.toNat best)) :=
271    fun cl nm => lmRest_ok E L hlimit cl nm
272  rw [longest_match_unfold]
273  simp only [bind_app, pure_app, M_ite_app, e_ld0, E.win, f14, f15, i0, i4, i5', i5, i6, hmm, hLsame]
274  by_cases hg : d.prev_length ≥ d.good_match <;> by_cases hn : d.nice_match.toUInt32 > d.lookahead
275  · obtain ⟨r, h', ms, best, hr, hrest⟩ := key (d.max_chain_length >>> 2) d.lookahead.toInt32
276    refine ⟨r, h', ms, best, ?_, hrest⟩
277    simp only [hg, hn, ite_true]; simp only [lmRest, bind_app, pure_app, M_ite_app] at hr; exact hr
278  · obtain ⟨r, h', ms, best, hr, hrest⟩ := key (d.max_chain_length >>> 2) d.nice_match
279    refine ⟨r, h', ms, best, ?_, hrest⟩
280    simp only [hg, hn, ite_true, ite_false]; simp only [lmRest, bind_app, pure_app, M_ite_app] at hr; exact hr
281  · obtain ⟨r, h', ms, best, hr, hrest⟩ := key d.max_chain_length d.lookahead.toInt32
282    refine ⟨r, h', ms, best, ?_, hrest⟩
283    simp only [hg, hn, ite_true, ite_false]; simp only [lmRest, bind_app, pure_app, M_ite_app] at hr; exact hr
284  · obtain ⟨r, h', ms, best, hr, hrest⟩ := key d.max_chain_length d.nice_match
285    refine ⟨r, h', ms, best, ?_, hrest⟩
286    simp only [hg, hn, ite_true, ite_false]; simp only [lmRest, bind_app, pure_app, M_ite_app] at hr; exact hr
287
288end Zlib.Deflate.Engine.Proofs