inflate.c.sync4.lean

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

1import ZlibF.Proof.«inflate.c.sync3»
2
3/-!
4# inflate.c: `inflateSync`, the first call (restore of the bit buffer)
5
6On the first call (`mode != SYNC`) the whole bytes of the bit buffer are moved to `buf` and searched first.
7-/
8
9namespace Zlib.Inflate.Spec
10open C
11
12/-- `x >> (8 n)`, as the restore loop computes it: `n` shifts by 8. -/
13def shr8N : Nat → UInt64 → UInt64
14  | 0, x => x
15  | n + 1, x => shr8N n x >>> 8
16
17/-- The array `buf` after the restore loop has stored the low bytes of `x`, `i` times. -/
18def fillBuf (A : Array UInt8) (x : UInt64) : Nat → Array UInt8
19  | 0 => A
20  | i + 1 => (fillBuf A x i).set! i (shr8N i x).toUInt8
21
22/-- The bit buffer after its partial byte (`bits & 7` bits) is dropped. -/
23def syncHold0 (st : InflateState) : UInt64 := st.hold >>> (st.bits &&& 7).toUInt64
24
25/-- The number of whole bytes in the bit buffer. -/
26def syncNB (st : InflateState) : Nat := (st.bits.toNat) / 8
27
28/-- The bytes `inflateSync` moves out of the bit buffer, in the order they were read from the input (low byte first). -/
29def syncRestore (st : InflateState) : List UInt8 :=
30  (List.range (syncNB st)).map fun j => (shr8N j (syncHold0 st)).toUInt8
31
32end Zlib.Inflate.Spec
33
34namespace Zlib.Inflate.Proofs
35open C Zlib.Inflate _root_.Zlib.Inflate.Spec
36
37theorem sync_and7_toNat (x : UInt32) : (x &&& 7).toNat = x.toNat % 8 := by
38  rw [UInt32.toNat_and]
39  have : (7 : UInt32).toNat = 2 ^ 3 - 1 := by decide
40  rw [this, Nat.and_two_pow_sub_one_eq_mod]
41
42theorem bitsDrop_toNat (b : UInt32) (hb : b.toNat ≤ 39) :
43    (b - (b &&& 7)) = UInt32.ofNat (8 * (b.toNat / 8)) := by
44  apply UInt32.toNat_inj.mp
45  have h7 := sync_and7_toNat b
46  have hle : (b &&& 7) ≤ b := by
47    rw [UInt32.le_iff_toNat_le, h7]; omega
48  rw [UInt32.toNat_sub_of_le _ _ hle, h7, UInt32.toNat_ofNat_of_lt' (by simp [UInt32.size]; omega)]
49  omega
50
51theorem sync_shr64_run (h : Heap) (x : UInt64) (n : UInt32) (hn : n < 64) : shr64 x n h = .ok (x >>> n.toUInt64, h) := by
52  simp [shr64, hn]
53
54theorem fillBuf_size (A : Array UInt8) (x : UInt64) (i : Nat) : (fillBuf A x i).size = A.size := by
55  induction i with
56  | zero => rfl
57  | succ i ih => simp [fillBuf, ih]
58
59/-- The heap after `i` iterations of the restore loop. -/
60def restoreHeap (H0 : Heap) (zs nb : Nat) (s0 : InflateState) (A : Array UInt8) (n i : Nat) : Heap :=
61  { H0 with
62    istates := upd H0.istates zs (some { s0 with hold := shr8N i s0.hold, bits := UInt32.ofNat (8 * (n - i)) }),
63    bytes := upd H0.bytes nb (some (fillBuf A s0.hold i)) }
64
65/-- **The restore loop.** `cond` and `body` are the loop of `inflateSync`; the hypotheses say what they do on the heap
66`restoreHeap ... i`: the test is `bits >= 8`, the body stores the low byte of `hold` at `buf[len]`, shifts the buffer and
67counts. -/
68theorem restore_loop {cond : UInt32 → M (Bool × UInt32)} {body : UInt32 → M UInt32} {H0 : Heap} {zs nb : Nat}
69    {s0 : InflateState} {A : Array UInt8} (n : Nat) (hn : n ≤ 4)
70    (hc : ∀ i len, len = UInt32.ofNat i → i ≤ n → cond len (restoreHeap H0 zs nb s0 A n i) =
71      .ok ((decide (i < n), len), restoreHeap H0 zs nb s0 A n i))
72    (hb : ∀ i len, len = UInt32.ofNat i → i < n → body len (restoreHeap H0 zs nb s0 A n i) =
73      .ok (len + 1, restoreHeap H0 zs nb s0 A n (i + 1))) :
74    cwhile cond body 0 (restoreHeap H0 zs nb s0 A n 0) = .ok (UInt32.ofNat n, restoreHeap H0 zs nb s0 A n n) := by
75  have key := cwhile_run (cond := cond) (body := body)
76    (fun k len H => ∃ i, i + k = n ∧ len = UInt32.ofNat i ∧ H = restoreHeap H0 zs nb s0 A n i)
77    (fun len H => len = UInt32.ofNat n ∧ H = restoreHeap H0 zs nb s0 A n n) ?_ ?_
78    (k := n) (s := 0) (h := restoreHeap H0 zs nb s0 A n 0) ⟨0, by omega, rfl, rfl⟩ (by unfold fuel; omega)
79  · obtain ⟨s', h', hh, hq1, hq2⟩ := key
80    rw [hh, hq1, hq2]
81  · intro k len H ⟨i, hi, hl, hH⟩
82    subst hl; subst hH
83    refine ⟨_, _, _, _, ?_, hb i _ rfl (by omega), i + 1, by omega, ?_, rfl⟩
84    · rw [hc i _ rfl (by omega)]
85      simp [show i < n by omega]
86    · have : (UInt32.ofNat i + 1) = UInt32.ofNat (i + 1) := by
87        apply UInt32.toNat_inj.mp
88        rw [UInt32.toNat_add, UInt32.toNat_ofNat_of_lt' (by simp [UInt32.size]; omega),
89          UInt32.toNat_ofNat_of_lt' (by simp [UInt32.size]; omega)]
90        simp; omega
91      exact this
92  · intro len H ⟨i, hi, hl, hH⟩
93    subst hl; subst hH
94    have : i = n := by omega
95    subst this
96    refine ⟨_, _, ?_, rfl, rfl⟩
97    rw [hc i _ rfl (Nat.le_refl _)]
98    simp
99
100end Zlib.Inflate.Proofs
101
102namespace Zlib.Inflate.Spec
103open C
104/-- The state after the restore and the search of its bytes. -/
105def syncFirstState (st : InflateState) : InflateState :=
106  { st with «have» := (syncScan 0 (syncRestore st)).1, mode := SYNC, hold := shr8N (syncNB st) (syncHold0 st), bits := 0 }
107
108/-- The heap after the restore and the search of its bytes (`buf` is the block `nb` with content `A`). -/
109def syncFirstHeap (H0 : Heap) (zs nb : Nat) (st : InflateState) (A : Array UInt8) : Heap :=
110  { H0 with bytes := upd H0.bytes nb (some (fillBuf A (syncHold0 st) (syncNB st))), istates := upd H0.istates zs (some (syncFirstState st)) }
111end Zlib.Inflate.Spec
112
113namespace Zlib.Inflate.Proofs
114open C Zlib.Inflate _root_.Zlib.Inflate.Spec
115
116theorem syncHold0_eq (st : InflateState) : syncHold0 st = st.hold >>> (st.bits.toUInt64 &&& 7) := by
117  unfold syncHold0
118  congr 1
119
120theorem fillBuf_get (A : Array UInt8) (x : UInt64) : ∀ i j, j < i → i ≤ A.size →
121    (fillBuf A x i)[j]? = some (shr8N j x).toUInt8 := by
122  intro i
123  induction i with
124  | zero => intro j hj; omega
125  | succ i ih =>
126    intro j hj hi
127    have hs := fillBuf_size A x i
128    simp only [fillBuf, Array.set!_eq_setIfInBounds, Array.getElem?_setIfInBounds]
129    by_cases hji : j = i
130    · subst hji; simp [hs]; omega
131    · have := ih j (by omega) (by omega)
132      have hij : ¬ i = j := fun h => hji h.symm
133      simpa [hij] using this
134
135theorem syncBytes_fillBuf (A : Array UInt8) (x : UInt64) (n : Nat) (hn : n ≤ 4) (hA : A.size = 4) :
136    syncBytes (fillBuf A x n) 0 (UInt32.ofNat n) = (List.range n).map fun j => (shr8N j x).toUInt8 := by
137  have hs := fillBuf_size A x n
138  unfold syncBytes
139  rw [UInt32.toNat_ofNat_of_lt' (by simp [UInt32.size]; omega)]
140  apply List.ext_getElem?
141  intro j
142  by_cases hj : j < n
143  · have := fillBuf_get A x n j hj (by omega)
144    simp [List.getElem?_take, hj, List.getElem?_range]
145    simpa using this
146  · simp [List.getElem?_take, hj, List.getElem?_range]
147
148theorem dec8 (m : Nat) (hm : m ≤ 4) : decide (8 ≤ UInt32.ofNat (8 * m)) = decide (0 < m) := by
149  have : m = 0 ∨ m = 1 ∨ m = 2 ∨ m = 3 ∨ m = 4 := by omega
150  rcases this with rfl | rfl | rfl | rfl | rfl <;> decide
151
152theorem ofNat_sub8 (m : Nat) (hm : m ≤ 4) (h1 : 1 ≤ m) : UInt32.ofNat (8 * m) - 8 = UInt32.ofNat (8 * (m - 1)) := by
153  have : m = 0 ∨ m = 1 ∨ m = 2 ∨ m = 3 ∨ m = 4 := by omega
154  rcases this with rfl | rfl | rfl | rfl | rfl <;> first | (exfalso; omega) | decide
155
156theorem bits_step (m : Nat) (hm : m ≤ 4) (h1 : 1 ≤ m) : 8 * UInt32.ofNat m - 8 = 8 * UInt32.ofNat (m - 1) := by
157  have : m = 0 ∨ m = 1 ∨ m = 2 ∨ m = 3 ∨ m = 4 := by omega
158  rcases this with rfl | rfl | rfl | rfl | rfl <;> first | (exfalso; omega) | decide
159
160theorem ofNat_succ (i : Nat) (hi : i ≤ 4) : UInt32.ofNat i + 1 = UInt32.ofNat (i + 1) := by
161  have : i = 0 ∨ i = 1 ∨ i = 2 ∨ i = 3 ∨ i = 4 := by omega
162  rcases this with rfl | rfl | rfl | rfl | rfl <;> decide
163
164theorem syncFirst_run {H0 : Heap} {zs nb : Nat} {st : InflateState} {A : Array UInt8}
165    (hs : H0.istates zs = some st) (hA : H0.bytes nb = some A) (hAs : A.size = 4) (hro : H0.ro nb = false)
166    (hb39 : st.bits.toNat ≤ 39) :
167    syncFirst (some (.tab zs)) (.ref (.blk nb) 0) st H0 = .ok ((), syncFirstHeap H0 zs nb st A) := by
168  have h7 : (st.bits &&& 7) < 64 := by
169    rw [UInt32.lt_iff_toNat_lt, sync_and7_toNat]; simp; omega
170  have hbd := bitsDrop_toNat st.bits hb39
171  unfold syncFirst
172  isimp [hs, sync_shr64_run H0 _ _ h7]
173  have hn4 : syncNB st ≤ 4 := by unfold syncNB; omega
174  have hs0 : (setI H0 zs { st with mode := SYNC, hold := st.hold >>> (st.bits.toUInt64 &&& 7), bits := st.bits - (st.bits &&& 7) }) = restoreHeap H0 zs nb { st with mode := SYNC, hold := st.hold >>> (st.bits.toUInt64 &&& 7), bits := st.bits - (st.bits &&& 7) } A (syncNB st) 0 := by
175    have hb8 : UInt32.ofNat (8 * syncNB st) = st.bits - (st.bits &&& 7) := by rw [hbd]; rfl
176    unfold restoreHeap setI
177    simp only [shr8N, Nat.sub_zero, fillBuf, upd_self _ _ _ hA, hb8]
178  rw [hs0]
179  rw [restore_loop (n := syncNB st) hn4 ?hc ?hb]
180  case hc =>
181    intro i len hl hi
182    have hlt : decide (8 ≤ UInt32.ofNat (8 * (syncNB st - i))) = decide (i < syncNB st) := by
183      rw [dec8 _ (by omega)]; simp; omega
184    have hi : (restoreHeap H0 zs nb { st with mode := SYNC, hold := st.hold >>> (st.bits.toUInt64 &&& 7), bits := st.bits - (st.bits &&& 7) } A (syncNB st) i).istates zs = some { st with mode := SYNC, hold := shr8N i (st.hold >>> (st.bits.toUInt64 &&& 7)), bits := UInt32.ofNat (8 * (syncNB st - i)) } := by
185      simp [restoreHeap]
186    simp only [bind_app, pure_app, rdI_eq, hi, hlt]
187  case hb =>
188    intro i len hl hi
189    have hlen : len.toNat = i := by rw [hl, UInt32.toNat_ofNat_of_lt' (by simp [UInt32.size]; omega)]
190    have hg : Space.get (restoreHeap H0 zs nb { st with mode := SYNC, hold := st.hold >>> (st.bits.toUInt64 &&& 7), bits := st.bits - (st.bits &&& 7) } A (syncNB st) i) (BRef.blk nb) = some (fillBuf A (st.hold >>> (st.bits.toUInt64 &&& 7)) i) := by
191      simp [Space.get, restoreHeap]
192    have hsz : (fillBuf A (st.hold >>> (st.bits.toUInt64 &&& 7)) i).size = 4 := by rw [fillBuf_size]; exact hAs
193    have hadd := Ptr.add_nat_ok (r := BRef.blk nb) (off := 0) (n := i) hg (by omega)
194    have hro' : Space.ro (restoreHeap H0 zs nb { st with mode := SYNC, hold := st.hold >>> (st.bits.toUInt64 &&& 7), bits := st.bits - (st.bits &&& 7) } A (syncNB st) i) (BRef.blk nb) = false := by
195      simpa [Space.ro, restoreHeap] using hro
196    have hstore := fun v => Ptr.store_ok (r := BRef.blk nb) (off := i) (v := v) hg hro' (by omega)
197    have hi : (restoreHeap H0 zs nb { st with mode := SYNC, hold := st.hold >>> (st.bits.toUInt64 &&& 7), bits := st.bits - (st.bits &&& 7) } A (syncNB st) i).istates zs = some { st with mode := SYNC, hold := shr8N i (st.hold >>> (st.bits.toUInt64 &&& 7)), bits := UInt32.ofNat (8 * (syncNB st - i)) } := by
198      simp [restoreHeap]
199    have hsub := ofNat_sub8 (syncNB st - i) (by omega) (by omega)
200    have hsu := ofNat_succ i (by omega)
201    have hadd' := hadd
202    unfold OkOn at hadd'
203    simp only [Nat.zero_add] at hadd'
204    simp only [bind_app, pure_app, ldI_eq, hi, hlen, hadd', store8, hstore, wrI_eq, Space.put]
205    simp [restoreHeap, setI, upd_upd, fillBuf, shr8N, hsub, hsu, hsub, Nat.sub_sub]
206    have e1 : 8 * UInt32.ofNat (syncNB st - i) - 8 = 8 * UInt32.ofNat (syncNB st - (i + 1)) := by
207      rw [bits_step (syncNB st - i) (by omega) (by omega)]
208      congr 2
209    rw [e1]
210  have hist : (restoreHeap H0 zs nb { st with mode := SYNC, hold := st.hold >>> (st.bits.toUInt64 &&& 7), bits := st.bits - (st.bits &&& 7) } A (syncNB st) (syncNB st)).istates zs = some { st with mode := SYNC, hold := shr8N (syncNB st) (st.hold >>> (st.bits.toUInt64 &&& 7)), bits := UInt32.ofNat (8 * (syncNB st - syncNB st)) } := by
211    simp [restoreHeap]
212  simp only [bind_app, pure_app, ldI_eq, hist, wrI_eq]
213  have hsz : (fillBuf A (st.hold >>> (st.bits.toUInt64 &&& 7)) (syncNB st)).size = 4 := by rw [fillBuf_size]; exact hAs
214  have hnn : (UInt32.ofNat (syncNB st)).toNat = syncNB st := UInt32.toNat_ofNat_of_lt' (by simp [UInt32.size]; omega)
215  rw [syncsearch_run (r := BRef.blk nb) (a := fillBuf A (st.hold >>> (st.bits.toUInt64 &&& 7)) (syncNB st)) (o := 0)
216    (len := UInt32.ofNat (syncNB st)) 0 (by simp [Space.get, restoreHeap, setI]) (by rw [hnn, hsz]; omega)]
217  have hR : syncBytes (fillBuf A (st.hold >>> (st.bits.toUInt64 &&& 7)) (syncNB st)) 0 (UInt32.ofNat (syncNB st)) = syncRestore st := by
218    rw [syncBytes_fillBuf _ _ _ hn4 hAs]
219    unfold syncRestore; rw [syncHold0_eq]
220  rw [hR]
221  simp only [bind_app, pure_app, ldI_eq, setI_istates_same]
222  simp [setI, restoreHeap, syncFirstHeap, syncFirstState, upd_upd, Nat.sub_self, syncHold0_eq]
223
224theorem good_setBuf {H : Heap} {r : ZStreamRef} {zs : Nat} {z : ZStream} {st : InflateState} {nb : Nat} {a0 : Array UInt8}
225    (hG : Good H r zs z st) (e : H.bytes nb = some a0) (hn : ∀ w, st.window = .ref (.blk w) 0 → w ≠ nb)
226    (A : Array UInt8) : Good { H with bytes := upd H.bytes nb (some A) } r zs z st := by
227  have hS := shape_setB e A
228  obtain ⟨⟨hz, hs, zst, back, hm, za, zf⟩, ⟨wf, win, rq, bits, ptr⟩, hU, hF⟩ := hG
229  refine ⟨⟨hz, hs, zst, back, hm, za, zf⟩, ⟨wf, ?_, rq, bits, ptr⟩, hS.uniq hU, hS.fresh rfl hF⟩
230  refine ⟨win.wbits, ?_, win.nullws, win.ws, win.hv, win.wn, win.eq⟩
231  rcases win.block with h0 | ⟨w, a, hw, ha, hro, hsz⟩
232  · exact Or.inl h0
233  · exact Or.inr ⟨w, a, hw, by rw [upd_ne _ _ _ _ (hn w hw)]; exact ha, hro, hsz⟩
234
235theorem good_firstState {H : Heap} {r : ZStreamRef} {zs : Nat} {z : ZStream} {st : InflateState} {nb : Nat} {A : Array UInt8}
236    (hG : Good H r zs z st) (e : H.bytes nb = some A) (hn : ∀ w, st.window = .ref (.blk w) 0 → w ≠ nb) :
237    Good (syncFirstHeap H zs nb st A) r zs z (syncFirstState st) := by
238  have h1 := good_setBuf hG e hn (fillBuf A (syncHold0 st) (syncNB st))
239  have h2 := good_state h1 (st' := syncFirstState st) rfl (by simp [syncFirstState]; decide)
240    (h1.inv.of_fields rfl rfl rfl rfl rfl rfl rfl rfl rfl (by simp [syncFirstState]) rfl rfl rfl)
241  exact h2
242
243theorem syncIn_first {h : Heap} (hF : Fresh h) {zs : Nat} {st : InflateState} {A : Array UInt8}
244    {p : BPtr} {len : UInt32} {bs : List UInt8} (I : SyncIn h p len bs) :
245    SyncIn (syncFirstHeap (syncAlloc h) zs h.nextBlk st A) p len bs := by
246  rcases I with ⟨b, a, o, rfl, hg, hl, rfl⟩ | h2
247  · have hb : b ≠ h.nextBlk := by
248      intro hh; subst hh
249      obtain ⟨e0, -⟩ := fresh_dead hF (Nat.le_refl _)
250      rw [hg] at e0; cases e0
251    exact Or.inl ⟨b, a, o, rfl, by simp [syncFirstHeap, syncAlloc, upd_ne _ _ _ _ hb, hg], hl, rfl⟩
252  · exact Or.inr h2
253
254theorem syncAt_restore (st : InflateState) : SyncAt (syncScan 0 (syncRestore st)).1 (syncRestore st) := by
255  obtain ⟨-, h2, h3⟩ := syncScan_spec syncSt_zero (syncRestore st) rfl
256  by_cases h4 : (syncScan 0 (syncRestore st)).1 = 4
257  · right
258    refine ⟨h4, ?_⟩
259    obtain ⟨-, a, -⟩ := h2 h4
260    have hin : [] ++ (syncRestore st).take (syncScan 0 (syncRestore st)).2 <:+: syncRestore st :=
261      ⟨[], (syncRestore st).drop (syncScan 0 (syncRestore st)).2, by simp⟩
262    exact (List.IsSuffix.isInfix a).trans (by simpa using hin)
263  · left
264    simpa using (h3 h4).2
265
266/-- **inflateSync, first call** (`mode != SYNC`). The whole bytes of the bit buffer (`syncRestore st`: the bits below the next
267byte boundary are dropped; at most 4 bytes, as the bit buffer holds at most 39 bits) are searched first, then the input
268`next_in[0 .. avail_in)` (`SyncIn`), in the same state machine, so the pattern `00 00 FF FF` is found if it occurs in
269`restore ++ input` (`syncScan_spec`; the search stops after its first occurrence and `N` counts input bytes only, 0 if the
270pattern lies in the restored bytes). The state gets `mode = SYNC`, the bit buffer emptied (`hold` shifted, `bits = 0`) and `have`
271set; the stream consumes `N` bytes. Not found (`G ≠ 4`): `Z_DATA_ERROR`, all input consumed. Found: `Z_OK` with the heap
272`syncOkHeap` (reset, totals kept, mode `TYPE`). There must be input or a whole byte in the bit buffer (else `Z_BUF_ERROR`,
273`inflateSync_buf_error`). The local array is made and freed. Default `zfree` only. -/
274theorem inflateSync_first {h : Heap} {r : ZStreamRef} {zs : Nat} {z : ZStream} {st : InflateState} {bs : List UInt8}
275    (hG : Good h r zs z st) (hf : z.zfree = .fn "zcfree") (hmode : st.mode ≠ SYNC)
276    (hprog : ¬ (z.avail_in = 0 ∧ st.bits < 8)) (hI : SyncIn h z.next_in z.avail_in bs) :
277    ∃ N G, N.toNat ≤ z.avail_in.toNat ∧
278      (G = 4 → syncPat <:+: syncRestore st ++ bs.take N.toNat ∧ ∀ L', L' < N.toNat → ¬ syncPat <:+: syncRestore st ++ bs.take L') ∧
279      (G ≠ 4 → N = z.avail_in ∧ SyncSt G (syncRestore st ++ bs)) ∧
280      (G ≠ 4 → ∃ h', C.run (inflateSync (some r)) h = .ok (Z_DATA_ERROR, h') ∧
281        h' = freeWin (setI (r.put (syncFirstHeap (syncAlloc h) zs h.nextBlk st (syncJunk h)) (syncAdvance z N)) zs
282          (syncHave (syncFirstState st) G)) (syncBuf h) ∧
283        Good h' r zs (syncAdvance z N) (syncHave (syncFirstState st) G)) ∧
284      (G = 4 → ∃ h', C.run (inflateSync (some r)) h = .ok (Z_OK, h') ∧
285        h' = freeWin (syncOkHeap (setI (r.put (syncFirstHeap (syncAlloc h) zs h.nextBlk st (syncJunk h)) (syncAdvance z N)) zs
286          (syncHave (syncFirstState st) G)) r zs (syncAdvance z N) (syncHave (syncFirstState st) G)) (syncBuf h) ∧
287        Good h' r zs (syncOkStream (syncAdvance z N) (syncHave (syncFirstState st) G))
288          (syncOkState zs (syncHave (syncFirstState st) G))) := by
289  have hF := hG.fresh
290  have hG0 := good_syncAlloc hG
291  have hwn := win_ne_buf hF hG.inv.win
292  have hbb : (syncAlloc h).bytes h.nextBlk = some (syncJunk h) := syncAlloc_bytes_buf h
293  have hAs : (syncJunk h).size = 4 := by simp [syncJunk]
294  have hGf := good_firstState hG0 hbb hwn
295  have hIf := syncIn_first (zs := zs) (st := st) (A := syncJunk h) hF hI
296  have hL0 := hG0.live
297  have hrun1 := syncFirst_run (H0 := syncAlloc h) (zs := zs) (nb := h.nextBlk) (st := st) (A := syncJunk h)
298    (by simpa using hG.live.hs) hbb hAs (syncAlloc_ro_buf h) hG.inv.bits
299  obtain ⟨N, G, hN, h4, h3, hG1, hne, he⟩ := syncTail_run hGf hf hIf (syncAt_restore st)
300  have hnbf : (syncFirstHeap (syncAlloc h) zs h.nextBlk st (syncJunk h)).bytes h.nextBlk =
301      some (fillBuf (syncJunk h) (syncHold0 st) (syncNB st)) := by simp [syncFirstHeap]
302  have hrof : (syncFirstHeap (syncAlloc h) zs h.nextBlk st (syncJunk h)).ro h.nextBlk = false := by
303    simp [syncFirstHeap, syncAlloc_ro_buf]
304  refine ⟨N, G, hN, h4, h3, fun hG4 => ?_, fun hG4 => ?_⟩
305  · refine ⟨_, ?_, rfl, ?_⟩
306    · show inflateSync (some r) h = _
307      rw [inflateSync_split]
308      isimp [allocLocalB_run h hF, stateCheck_live hL0, hL0.zst, hG.live.hz, hG.live.hs, hprog, hmode, syncBuf, hrun1,
309        hne hG4, freeBuf_run (H := setI (r.put (syncFirstHeap (syncAlloc h) zs h.nextBlk st (syncJunk h)) (syncAdvance z N)) zs
310          (syncHave (syncFirstState st) G)) (nb := h.nextBlk) (a := fillBuf (syncJunk h) (syncHold0 st) (syncNB st))
311          (by simpa using hnbf) (by simpa using hrof)]
312    · exact good_freeBuf (nb := h.nextBlk) hG1 (fun w hw => hwn w (by simpa [syncHave, syncFirstState] using hw))
313  · refine ⟨_, ?_, rfl, ?_⟩
314    · have hbn : ∀ w', (syncHave (syncFirstState st) G).window = .ref (.blk w') 0 → w' ≠ h.nextBlk :=
315        fun w' hw' => hwn w' (by simpa [syncHave, syncFirstState] using hw')
316      have hby := syncOkHeap_bytes_ne (setI (r.put (syncFirstHeap (syncAlloc h) zs h.nextBlk st (syncJunk h)) (syncAdvance z N)) zs
317        (syncHave (syncFirstState st) G)) r zs (syncAdvance z N) (syncHave (syncFirstState st) G) hbn
318      show inflateSync (some r) h = _
319      rw [inflateSync_split]
320      isimp [allocLocalB_run h hF, stateCheck_live hL0, hL0.zst, hG.live.hz, hG.live.hs, hprog, hmode, syncBuf, hrun1,
321        he hG4, freeBuf_run (H := syncOkHeap (setI (r.put (syncFirstHeap (syncAlloc h) zs h.nextBlk st (syncJunk h)) (syncAdvance z N)) zs
322          (syncHave (syncFirstState st) G)) r zs (syncAdvance z N) (syncHave (syncFirstState st) G)) (nb := h.nextBlk)
323          (a := fillBuf (syncJunk h) (syncHold0 st) (syncNB st))
324          (by rw [hby.1]; simpa using hnbf) (by rw [hby.2]; simpa using hrof)]
325    · have hGd := (syncDone_good hG1).1
326      exact good_freeBuf (nb := h.nextBlk) hGd (fun w hw => hwn w (by simpa [syncHave, syncFirstState] using syncOkState_window_ref hw))
327
328end Zlib.Inflate.Proofs