inflate.c.sync2.lean

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

1import ZlibF.Proof.«inflate.c.sync»
2import ZlibF.Proof.«inflate.c.reset»
3import ZlibF.Proof.«inflate.c.misc»
4
5/-!
6# inflate.c: `inflateSync`
7
8Infrastructure: the local array `unsigned char buf[4]` is a block taken at the start of the call (`syncAlloc`) and
9freed before every return (`freeWin ... buf`); the block number is never reused.
10-/
11
12namespace Zlib.Inflate.Spec
13open C
14
15/-- The initial (arbitrary) content of `buf[4]`. -/
16def syncJunk (h : Heap) : Array UInt8 := Array.ofFn (n := 4) fun i => Junk.of (h.garbage h.nalloc i.val)
17
18/-- The heap after the local array `buf[4]` is made: block `h.nextBlk`, writable. -/
19def syncAlloc (h : Heap) : Heap :=
20  { h with bytes := upd h.bytes h.nextBlk (some (syncJunk h)), ro := upd h.ro h.nextBlk false, nextBlk := h.nextBlk + 1 }
21
22/-- The pointer to the local array. -/
23def syncBuf (h : Heap) : BPtr := .ref (.blk h.nextBlk) 0
24
25/-- The heap after a call that did nothing but make and free the local array. -/
26def tmpFreed (h : Heap) : Heap := freeWin (syncAlloc h) (syncBuf h)
27
28end Zlib.Inflate.Spec
29
30namespace Zlib.Inflate.Proofs
31open C Zlib.Inflate Zlib.Inflate.Spec
32
33theorem allocLocalB_run (h : Heap) (hF : Fresh h) : allocLocalB 4 h = .ok (syncBuf h, syncAlloc h) := by
34  have hs := hF.slotUsed_next
35  simp [allocLocalB, allocBytes, hs, syncBuf, syncAlloc, syncJunk]
36
37@[simp] theorem syncAlloc_streams (h : Heap) : (syncAlloc h).streams = h.streams := rfl
38@[simp] theorem syncAlloc_gzstates (h : Heap) : (syncAlloc h).gzstates = h.gzstates := rfl
39@[simp] theorem syncAlloc_istates (h : Heap) : (syncAlloc h).istates = h.istates := rfl
40@[simp] theorem syncAlloc_words (h : Heap) : (syncAlloc h).words = h.words := rfl
41@[simp] theorem syncAlloc_gzheaders (h : Heap) : (syncAlloc h).gzheaders = h.gzheaders := rfl
42@[simp] theorem syncAlloc_dstates (h : Heap) : (syncAlloc h).dstates = h.dstates := rfl
43@[simp] theorem syncAlloc_nextBlk (h : Heap) : (syncAlloc h).nextBlk = h.nextBlk + 1 := rfl
44@[simp] theorem syncAlloc_nalloc (h : Heap) : (syncAlloc h).nalloc = h.nalloc := rfl
45@[simp] theorem syncAlloc_allocOk (h : Heap) : (syncAlloc h).allocOk = h.allocOk := rfl
46@[simp] theorem syncAlloc_garbage (h : Heap) : (syncAlloc h).garbage = h.garbage := rfl
47@[simp] theorem syncAlloc_static (h : Heap) : (syncAlloc h).static = h.static := rfl
48
49@[simp] theorem ZStreamRef.get_syncAlloc (h : Heap) (r : ZStreamRef) : r.get (syncAlloc h) = r.get h := by
50  cases r <;> rfl
51
52theorem syncAlloc_bytes_buf (h : Heap) : (syncAlloc h).bytes h.nextBlk = some (syncJunk h) := by
53  simp [syncAlloc]
54theorem syncAlloc_ro_buf (h : Heap) : (syncAlloc h).ro h.nextBlk = false := by
55  simp [syncAlloc]
56theorem syncAlloc_bytes_ne (h : Heap) {b : Nat} (hb : b ≠ h.nextBlk) : (syncAlloc h).bytes b = h.bytes b := by
57  simp [syncAlloc, upd_ne _ _ _ _ hb]
58
59theorem fresh_dead {h : Heap} (hF : Fresh h) {b : Nat} (hb : h.nextBlk ≤ b) :
60    h.bytes b = none ∧ h.words b = none ∧ h.streams b = none ∧ h.gzheaders b = none ∧ h.dstates b = none ∧
61    h.istates b = none ∧ h.gzstates b = none :=
62  Heap.not_live.mp (hF b hb)
63
64theorem uniq_syncAlloc {h : Heap} (hU : Uniq h) (hF : Fresh h) : Uniq (syncAlloc h) := by
65  intro b
66  by_cases hb : b = h.nextBlk
67  · subst hb
68    obtain ⟨e0, e1, e2, e3, e4, e5, e6⟩ := fresh_dead hF (Nat.le_refl _)
69    simp [syncAlloc, e1, e2, e3, e4, e5, e6, cnt]
70  · have := hU b
71    simpa [syncAlloc, upd_ne _ _ _ _ hb] using this
72
73theorem fresh_syncAlloc {h : Heap} (hF : Fresh h) : Fresh (syncAlloc h) := by
74  intro b hb hl
75  simp only [syncAlloc_nextBlk] at hb
76  apply hF b (by omega)
77  have hne : b ≠ h.nextBlk := by omega
78  simpa [Heap.live, syncAlloc, upd_ne _ _ _ _ hne] using hl
79
80theorem live_syncAlloc {h : Heap} (b : Nat) : (syncAlloc h).live b ↔ h.live b ∨ b = h.nextBlk := by
81  by_cases hb : b = h.nextBlk
82  · subst hb; simp [Heap.live, syncAlloc]
83  · simp [Heap.live, syncAlloc, upd_ne _ _ _ _ hb, hb]
84
85theorem winInv_syncAlloc {h : Heap} (hF : Fresh h) {st : InflateState} (hW : WinInv h st) : WinInv (syncAlloc h) st := by
86  refine ⟨hW.wbits, ?_, hW.nullws, hW.ws, hW.hv, hW.wn, hW.eq⟩
87  rcases hW.block with hn | ⟨w, a, hw, ha, hro, hsz⟩
88  · exact Or.inl hn
89  · have hwn : w ≠ h.nextBlk := by
90      intro e; subst e
91      obtain ⟨e0, -⟩ := fresh_dead hF (Nat.le_refl _)
92      rw [ha] at e0; cases e0
93    exact Or.inr ⟨w, a, hw, by rw [syncAlloc_bytes_ne h hwn]; exact ha, by simp [syncAlloc, upd_ne _ _ _ _ hwn, hro], hsz⟩
94
95theorem good_syncAlloc {h : Heap} {r : ZStreamRef} {zs : Nat} {z : ZStream} {st : InflateState}
96    (hG : Good h r zs z st) : Good (syncAlloc h) r zs z st := by
97  obtain ⟨⟨hz, hs, zst, back, hm, za, zf⟩, ⟨wf, win, rq, bits, ptr⟩, hU, hF⟩ := hG
98  exact ⟨⟨by simpa using hz, by simpa using hs, zst, back, hm, za, zf⟩,
99    ⟨wf, winInv_syncAlloc hF win, rq, bits, ptr⟩, uniq_syncAlloc hU hF, fresh_syncAlloc hF⟩
100
101theorem live_tmpFreed {h : Heap} (b : Nat) : (tmpFreed h).live b → (syncAlloc h).live b :=
102  live_freeWin _ b
103
104theorem freeBuf_run {H : Heap} {nb : Nat} {a : Array UInt8} (hb : H.bytes nb = some a) (hro : H.ro nb = false) :
105    freeB (.ref (.blk nb) 0) H = .ok ((), freeWin H (.ref (.blk nb) 0)) := by
106  rw [freeB_ok hb hro]; rfl
107
108/-! ### The early returns -/
109
110/-- **inflateSync, refusal.** If the state check fails (`StreamDom`: `NULL`, or a live record whose state is not a usable
111inflate state) the call returns `Z_STREAM_ERROR`; nothing changes except that the local array `buf` was made and freed
112(the block number is used up). -/
113theorem inflateSync_check {h : Heap} (hF : Fresh h) {strm : ZStreamPtr} (hD : StreamDom h strm)
114    (hN : ¬ Initialised h strm) :
115    C.run (inflateSync strm) h = .ok (Z_STREAM_ERROR, tmpFreed h) := by
116  have hD' : StreamDom (syncAlloc h) strm := by
117    rcases hD with h0 | ⟨r, z, h0, hr, hc⟩
118    · exact Or.inl h0
119    · exact Or.inr ⟨r, z, h0, by simpa using hr, by simpa using hc⟩
120  have hN' : ¬ Initialised (syncAlloc h) strm := by
121    rintro ⟨r, zs, z, st, h0, hL⟩
122    exact hN ⟨r, zs, z, st, h0, ⟨by simpa using hL.hz, by simpa using hL.hs, hL.zst, hL.back, hL.mode, hL.zalloc, hL.zfree⟩⟩
123  show inflateSync strm h = _
124  unfold inflateSync
125  have hb : (syncAlloc h).bytes h.nextBlk = some (syncJunk h) := syncAlloc_bytes_buf h
126  simp [bind_app, pure_app, allocLocalB_run h hF, notInit_check hD' hN', freeBuf_run hb (syncAlloc_ro_buf h), tmpFreed,
127    syncBuf]
128
129/-- **inflateSync, no input.** On an initialised stream with `avail_in = 0` and fewer than 8 bits in the bit buffer the
130call returns `Z_BUF_ERROR`; nothing changes except that the local array `buf` was made and freed. -/
131theorem inflateSync_buf_error {h : Heap} {r : ZStreamRef} {zs : Nat} {z : ZStream} {st : InflateState}
132    (hG : Good h r zs z st) (hav : z.avail_in = 0) (hb : st.bits < 8) :
133    C.run (inflateSync (some r)) h = .ok (Z_BUF_ERROR, tmpFreed h) := by
134  have hG' := good_syncAlloc hG
135  have hL := hG'.live
136  show inflateSync (some r) h = _
137  unfold inflateSync
138  have hbb : (syncAlloc h).bytes h.nextBlk = some (syncJunk h) := syncAlloc_bytes_buf h
139  isimp [allocLocalB_run h hG.fresh, stateCheck_live hL, hL.zst, hG.live.hz, hG.live.hs, hav, hb,
140    freeBuf_run hbb (syncAlloc_ro_buf h), tmpFreed, syncBuf]
141
142/-- the part of `inflateSync` from the bit-buffer restore on, as a function of the state pointer -/
143def syncFirst (st : InflateStatePtr) (buf : BPtr) (s : InflateState) : M Unit := do
144  let h ← shr64 s.hold (s.bits &&& 7)
145  wrS st fun s => { s with mode := SYNC, hold := h, bits := s.bits - (s.bits &&& 7) }
146  let len ← cwhile (σ := UInt32)
147    (fun len => do return ((← rdS st (·.bits)) >= 8, len))
148    (fun len => do
149      let s ← ldInflateState st
150      store8 (← buf.add (len.toNat : Int)) s.hold.toUInt8
151      wrS st fun s => { s with hold := s.hold >>> 8, bits := s.bits - 8 }
152      pure (len + 1))
153    0
154  wrS st fun s => { s with «have» := 0 }
155  let (_, hv) ← syncsearch 0 buf len
156  wrS st fun s => { s with «have» := hv }
157
158def syncDone (strm : ZStreamPtr) (st : InflateStatePtr) : M Int32 := do
159    let flags ← rdS st (·.flags)
160    let z ← ldZStream strm
161    let in_ := z.total_in
162    let out_ := z.total_out
163    let _ ← inflateReset strm
164    wrZ strm fun z => { z with total_in := in_, total_out := out_ }
165    wrS st fun s => { s with flags := flags }
166    if flags == -1 then wrS st fun s => { s with wrap := 0 }
167    else wrS st fun s => { s with wrap := s.wrap &&& ~~~4 }
168    let s ← ldInflateState st
169    if s.wbits == 0 then
170      if s.window != .null then
171        ZFREEB strm s.window
172        wrS st fun s => { s with window := .null }
173      wrS st fun s => { s with wbits := 15 }
174    setMode st TYPE
175    return Z_OK
176
177def syncTail (strm : ZStreamPtr) (st : InflateStatePtr) : M Int32 := do
178    let z ← ldZStream strm
179    let (len, hv) ← syncsearch (← rdS st (·.«have»)) z.next_in z.avail_in
180    wrS st fun s => { s with «have» := hv }
181    let ni ← z.next_in.add (len.toNat : Int)
182    wrZ strm fun z => { z with avail_in := z.avail_in - len, next_in := ni, total_in := z.total_in + len.toUInt64 }
183    if (← rdS st (·.«have»)) != 4 then return Z_DATA_ERROR
184    syncDone strm st
185
186theorem bind_ite_unit {α : Type} (c : Prop) [Decidable c] (A : M Unit) (jp : Unit → M α) :
187    (ite c A (pure ()) >>= jp) = ite c (A >>= jp) (jp ()) := by
188  by_cases hc : c <;> simp [hc] <;> rfl
189
190theorem bind_assoc_M {α β γ : Type} (m : M α) (f : α → M β) (g : β → M γ) :
191    ((m >>= f) >>= g) = (m >>= fun x => f x >>= g) := by
192  funext h
193  simp only [bind_app]
194  cases m h with
195  | error e => rfl
196  | ok p => rfl
197
198theorem inflateSync_split (strm : ZStreamPtr) : inflateSync strm = (do
199  let buf ← allocLocalB 4
200  let r ← (do
201    if (← inflateStateCheck strm) != 0 then return Z_STREAM_ERROR
202    let z ← ldZStream strm
203    let st ← castInflateState z.state
204    let s ← ldInflateState st
205    if z.avail_in == 0 && s.bits < 8 then return Z_BUF_ERROR
206    if s.mode != SYNC then syncFirst st buf s
207    syncTail strm st)
208  freeB buf
209  return r) := by
210  unfold inflateSync syncFirst syncTail syncDone
211  simp only [bind_assoc_M]
212
213end Zlib.Inflate.Proofs
214
215namespace Zlib.Inflate.Spec
216open C
217
218/-- The state record after `inflateReset`, the restored flags and the wrapper change of `inflateSync`, before the window
219bits are looked at: the request is raw if no header was read (`flags = -1`), else the check bit is cleared. -/
220def syncC (zs : Nat) (s : InflateState) : InflateState :=
221  let sB := { resetKeepState zs (resetPre s) with flags := s.flags }
222  if s.flags == -1 then { sB with wrap := 0 } else { sB with wrap := sB.wrap &&& ~~~4 }
223
224/-- The state record after a successful `inflateSync` search: reset to wait for a block type (`TYPE`), the header flags
225kept, a window size that no header ever gave set to 15 (the window is dropped then). -/
226def syncOkState (zs : Nat) (s : InflateState) : InflateState :=
227  let sC := syncC zs s
228  { (if sC.wbits == 0 then { sC with window := .null, wbits := 15 } else sC) with mode := TYPE }
229
230/-- The stream record after a successful `inflateSync` search: reset (`inflateReset`) but `total_in` and `total_out`
231keep their values. `z` is the record after the search consumed its bytes. -/
232def syncOkStream (z : ZStream) (s : InflateState) : ZStream :=
233  { resetKeepStream z (resetPre s) with total_in := z.total_in, total_out := z.total_out }
234
235/-- The heap after a successful `inflateSync` search, from the heap `H` (the stream record `z` after the search, the state
236record `s`): the reset frees the window if its size is not the requested one; a window size of 0 frees the window. -/
237def syncOkHeap (H : Heap) (r : ZStreamRef) (zs : Nat) (z : ZStream) (s : InflateState) : Heap :=
238  let X := setI (r.put (resetHeap H s) (syncOkStream z s)) zs (syncOkState zs s)
239  if (syncC zs s).wbits == 0 then freeWin X (syncC zs s).window else X
240
241end Zlib.Inflate.Spec
242
243namespace Zlib.Inflate.Proofs
244open C Zlib.Inflate Zlib.Inflate.Spec
245
246/-- **inflateSync, found.** From a good stream (`zfree` the default) the part of `inflateSync` after the pattern is found
247returns `Z_OK` with the heap `syncOkHeap`: reset, `total_in`/`total_out` kept, mode `TYPE`. -/
248theorem syncDone_run {H : Heap} {r : ZStreamRef} {zs : Nat} {z : ZStream} {s : InflateState}
249    (hG : Good H r zs z s) (hf : z.zfree = .fn "zcfree") :
250    syncDone (some r) (some (.tab zs)) H = .ok (Z_OK, syncOkHeap H r zs z s) := by
251  have hL := hG.live
252  have hwo : s.wbits = s.reqbits ∨ WindowOk H s.window := Or.inr (windowBlock hG.inv.win)
253  have hz0 : r.get (resetHeap H s) = some z := by unfold resetHeap; split <;> simp [hL.hz]
254  have hs0 : (resetHeap H s).istates zs = some s := by unfold resetHeap; split <;> simp [hL.hs]
255  unfold syncDone
256  isimp [stateCheck_live hL, hL.zst, hL.hz, hL.hs]
257  rw [inflateReset_run hL hf hwo]
258  have hrb : (resetPre s).wbits = s.reqbits := by unfold resetPre; split <;> simp_all
259  have hwb := windowBlock (winInv_reset hG.inv.win hG.inv.reqbits)
260  unfold syncOkHeap syncOkState syncOkStream syncC
261  generalize resetPre s = sR at hrb hwb ⊢
262  have hzN : r.get (setI (r.put (resetHeap H s) { resetKeepStream z sR with total_in := z.total_in, total_out := z.total_out }) zs
263      (resetKeepState zs sR)) = some { resetKeepStream z sR with total_in := z.total_in, total_out := z.total_out } := by
264    simp [hz0]
265  by_cases hfl : s.flags = -1
266  · by_cases h0 : sR.wbits = 0
267    · rcases hwb with hn | ⟨b, a, hb, hba, hro⟩
268      · isimp [hz0, hs0, resetKeepState, hfl, h0, hn, freeWin_null, setMode]
269      · isimp [hz0, hs0, resetKeepState, hfl, h0, hb, setMode]
270        rw [zfreeB_run (r := r) (z := { resetKeepStream z sR with total_in := z.total_in, total_out := z.total_out })
271          (p := .ref (.blk b) 0) (by simp [hz0]) (by simpa [resetKeepStream] using hf) (Or.inr ⟨b, a, rfl, by simpa using hba, by simpa using hro⟩)]
272        isimp [setMode, freeWin_istates]
273    · isimp [hz0, hs0, resetKeepState, hfl, h0, setMode]
274  · by_cases h0 : sR.wbits = 0
275    · rcases hwb with hn | ⟨b, a, hb, hba, hro⟩
276      · isimp [hz0, hs0, resetKeepState, hfl, h0, hn, freeWin_null, setMode]
277      · isimp [hz0, hs0, resetKeepState, hfl, h0, hb, setMode]
278        rw [zfreeB_run (r := r) (z := { resetKeepStream z sR with total_in := z.total_in, total_out := z.total_out })
279          (p := .ref (.blk b) 0) (by simp [hz0]) (by simpa [resetKeepStream] using hf) (Or.inr ⟨b, a, rfl, by simpa using hba, by simpa using hro⟩)]
280        isimp [setMode, freeWin_istates]
281    · isimp [hz0, hs0, resetKeepState, hfl, h0, setMode]
282
283/-! ### The invariants after a found pattern -/
284
285theorem resetPre_win (st : InflateState) : (resetPre st).wsize = 0 ∧ (resetPre st).whave = 0 ∧ (resetPre st).wnext = 0 := by
286  unfold resetPre; split <;> simp
287
288theorem resetPre_wbits (st : InflateState) : (resetPre st).wbits = st.reqbits := by
289  unfold resetPre; split <;> simp_all
290
291theorem resetPre_strm (st : InflateState) : (resetPre st).strm = st.strm := by
292  unfold resetPre; split <;> simp
293
294theorem syncC_field (zs : Nat) (s : InflateState) :
295    (syncC zs s).wbits = s.reqbits ∧ (syncC zs s).window = (resetPre s).window ∧ (syncC zs s).wsize = 0 ∧
296    (syncC zs s).whave = 0 ∧ (syncC zs s).wnext = 0 ∧ (syncC zs s).reqbits = s.reqbits ∧ (syncC zs s).strm = s.strm ∧
297    (syncC zs s).bits = 0 ∧ (syncC zs s).lens = s.lens ∧ (syncC zs s).work = s.work ∧ (syncC zs s).codes = s.codes := by
298  obtain ⟨a1, a2, a3⟩ := resetPre_win s
299  have a4 := resetPre_wbits s
300  have a5 := resetPre_strm s
301  have a6 : (resetPre s).reqbits = s.reqbits := reqbits_resetPre s
302  have a7 : (resetPre s).lens = s.lens := by unfold resetPre; split <;> simp
303  have a8 : (resetPre s).work = s.work := by unfold resetPre; split <;> simp
304  have a9 : (resetPre s).codes = s.codes := by unfold resetPre; split <;> simp
305  unfold syncC
306  split <;> simp [resetKeepState, a1, a2, a3, a4, a5, a6, a7, a8, a9]
307
308theorem syncC_ptr (zs : Nat) (s : InflateState) :
309    (syncC zs s).next = .ref (.istate_codes zs) 0 ∧ (syncC zs s).lencode = .ref (.istate_codes zs) 0 ∧
310    (syncC zs s).distcode = .ref (.istate_codes zs) 0 := by
311  unfold syncC; split <;> simp [resetKeepState]
312
313theorem syncOkState_eq0 {zs : Nat} {s : InflateState} (h0 : s.reqbits = 0) :
314    syncOkState zs s = { syncC zs s with window := .null, wbits := 15, mode := TYPE } := by
315  unfold syncOkState
316  simp [(syncC_field zs s).1, h0]
317
318theorem syncOkState_ne0 {zs : Nat} {s : InflateState} (h0 : s.reqbits ≠ 0) :
319    syncOkState zs s = { syncC zs s with mode := TYPE } := by
320  unfold syncOkState
321  simp [(syncC_field zs s).1, h0]
322
323/-- The state record after a found pattern satisfies the representation invariant on the heap after the reset. -/
324theorem syncOk_inv {H : Heap} {r : ZStreamRef} {zs : Nat} {z : ZStream} {s : InflateState} (hG : Good H r zs z s) :
325    StInv (resetHeap H s) zs (syncOkState zs s) := by
326  have hwf := wf_resetPre hG.inv.wf
327  have hwr := winInv_reset hG.inv.win hG.inv.reqbits
328  obtain ⟨f1, f2, f3, f4, f5, f6, f7, f8, f9, f10, f11⟩ := syncC_field zs s
329  obtain ⟨p1, p2, p3⟩ := syncC_ptr zs s
330  have hwf' : s.WellFormed := hG.inv.wf
331  have hrq := hG.inv.reqbits
332  by_cases h0 : s.reqbits = 0
333  · rw [syncOkState_eq0 h0]
334    refine ⟨?_, ?_, ?_, ?_, ?_⟩
335    · unfold InflateState.WellFormed at hwf' ⊢
336      simp only [f9, f10, f11]; exact hwf'
337    · refine ⟨by simp, Or.inl rfl, fun _ => by simpa using f3, Or.inl (by simp [f3]), by simp [f3, f4], Or.inr ⟨by simp [f3], by simp [f5]⟩, fun hh => by simp [f3, f4] at hh⟩
338    · simpa [f6] using hrq
339    · simp [syncC, resetKeepState]; split <;> simp
340    · exact ⟨⟨0, by simp [p1], by omega⟩, Or.inl ⟨0, 0, by simp [p2], by simp [p3], by omega, by omega⟩⟩
341  · rw [syncOkState_ne0 h0]
342    refine ⟨?_, ?_, ?_, ?_, ?_⟩
343    · unfold InflateState.WellFormed at hwf' ⊢
344      simp only [f9, f10, f11]; exact hwf'
345    · have hb : (resetPre s).wbits.toNat ≤ 15 := hwr.wbits
346      refine ⟨by simpa [f1, resetPre_wbits] using hrq, ?_, fun hn => ?_, Or.inl (by simp [f3]), by simp [f3, f4], Or.inr ⟨by simp [f3], by simp [f5]⟩, fun hh => by simp [f3, f4] at hh⟩
347      · have := hwr.block
348        simpa [f2, f1, resetPre_wbits] using this
349      · simp [f3]
350    · simpa [f6] using hrq
351    · simp [syncC, resetKeepState]; split <;> simp
352    · exact ⟨⟨0, by simp [p1], by omega⟩, Or.inl ⟨0, 0, by simp [p2], by simp [p3], by omega, by omega⟩⟩
353
354theorem winInv_of_null {H H' : Heap} {st : InflateState} (hW : WinInv H' st) (hn : st.window = .null) : WinInv H st :=
355  ⟨hW.wbits, Or.inl hn, hW.nullws, hW.ws, hW.hv, hW.wn, hW.eq⟩
356
357theorem stInv_of_null {H H' : Heap} {zs : Nat} {st : InflateState} (hI : StInv H' zs st) (hn : st.window = .null) :
358    StInv H zs st :=
359  ⟨hI.wf, winInv_of_null hI.win hn, hI.reqbits, hI.bits, hI.ptr⟩
360
361theorem syncOk_window_null {zs : Nat} {s : InflateState} (h0 : s.reqbits = 0) : (syncOkState zs s).window = .null := by
362  rw [syncOkState_eq0 h0]
363
364/-- The window of the state is kept by a found pattern: it has the requested size, and the size is not 0. -/
365def SyncKeeps (s : InflateState) : Prop := s.wbits = s.reqbits ∧ s.reqbits ≠ 0
366
367theorem resetPre_window (st : InflateState) :
368    (resetPre st).window = if st.wbits = st.reqbits then st.window else .null := by
369  unfold resetPre; split <;> simp_all
370
371/-- After a found pattern the stream is good again and the live blocks only shrink. -/
372theorem syncDone_good {H : Heap} {r : ZStreamRef} {zs : Nat} {z : ZStream} {s : InflateState}
373    (hG : Good H r zs z s) :
374    Good (syncOkHeap H r zs z s) r zs (syncOkStream z s) (syncOkState zs s) ∧
375    (∀ b, (syncOkHeap H r zs z s).live b → H.live b) := by
376  have hL := hG.live
377  have hU : Uniq (resetHeap H s) := by
378    unfold resetHeap; split
379    · exact uniq_freeWin hG.uniq _
380    · exact hG.uniq
381  have hF : Fresh (resetHeap H s) := by
382    unfold resetHeap; split
383    · exact fresh_freeWin hG.fresh _
384    · exact hG.fresh
385  have hz0 : r.get (resetHeap H s) = some z := by unfold resetHeap; split <;> simp [hL.hz]
386  have hs0 : (resetHeap H s).istates zs = some s := by unfold resetHeap; split <;> simp [hL.hs]
387  obtain ⟨f1, f2, f3, f4, f5, f6, f7, f8, f9, f10, f11⟩ := syncC_field zs s
388  have hmode : HEAD ≤ (syncOkState zs s).mode ∧ (syncOkState zs s).mode ≤ SYNC := by
389    have : (syncOkState zs s).mode = TYPE := by unfold syncOkState; simp
390    rw [this]; decide
391  have hback : (syncOkState zs s).strm = some r := by
392    have : (syncOkState zs s).strm = s.strm := by
393      unfold syncOkState; simp [f7]
394      split <;> simp [f7]
395    rw [this]; exact hL.back
396  have hX : Good (setI (r.put (resetHeap H s) (syncOkStream z s)) zs (syncOkState zs s)) r zs (syncOkStream z s)
397      (syncOkState zs s) :=
398    good_set hz0 hs0 hU hF (by simp [syncOkStream, resetKeepStream, hL.zst]) (by simpa [syncOkStream, resetKeepStream] using hL.zalloc)
399      (by simpa [syncOkStream, resetKeepStream] using hL.zfree) hback hmode (syncOk_inv hG)
400  have hShape : Shape (resetHeap H s) (setI (r.put (resetHeap H s) (syncOkStream z s)) zs (syncOkState zs s)) :=
401    (shape_put hz0 _).trans (shape_setI (by simpa using hs0) _)
402  have hlive0 : ∀ b, (resetHeap H s).live b → H.live b := by
403    intro b hb
404    unfold resetHeap at hb; split at hb
405    · exact live_freeWin _ b hb
406    · exact hb
407  by_cases h0 : s.reqbits = 0
408  · have hc : ((syncC zs s).wbits == 0) = true := by simp [f1, h0]
409    have hHeap : syncOkHeap H r zs z s = freeWin (setI (r.put (resetHeap H s) (syncOkStream z s)) zs (syncOkState zs s)) (resetPre s).window := by
410      unfold syncOkHeap; simp [hc, f2]
411    rw [hHeap]
412    have hwn : (syncOkState zs s).window = .null := syncOk_window_null h0
413    exact ⟨⟨⟨by simpa using hX.live.hz, by simpa using hX.live.hs, hX.live.zst, hX.live.back, hX.live.mode, hX.live.zalloc, hX.live.zfree⟩,
414      stInv_of_null hX.inv hwn, uniq_freeWin hX.uniq _, fresh_freeWin hX.fresh _⟩,
415      fun b hb => hlive0 b ((hShape.live b).1 (live_freeWin _ b hb))⟩
416  · have hc : ¬ ((syncC zs s).wbits == 0) = true := by simp [f1, h0]
417    have hHeap : syncOkHeap H r zs z s = setI (r.put (resetHeap H s) (syncOkStream z s)) zs (syncOkState zs s) := by
418      unfold syncOkHeap; simp [hc]
419    rw [hHeap]
420    exact ⟨hX, fun b hb => hlive0 b ((hShape.live b).1 hb)⟩
421
422/-- Ownership after a found pattern: only the window block can be freed (`¬ SyncKeeps`); nothing is allocated. -/
423theorem syncDone_owns {H : Heap} {r : ZStreamRef} {zs : Nat} {z : ZStream} {s : InflateState}
424    (hG : Good H r zs z s) {S : Nat → Prop} (hO : H.Owns S) :
425    (syncOkHeap H r zs z s).Owns (fun b => S b ∧ ¬ (¬ SyncKeeps s ∧ WinBlk s b)) := by
426  have hL := hG.live
427  have hz0 : r.get (resetHeap H s) = some z := by unfold resetHeap; split <;> simp [hL.hz]
428  have hs0 : (resetHeap H s).istates zs = some s := by unfold resetHeap; split <;> simp [hL.hs]
429  obtain ⟨f1, f2, f3, f4, f5, f6, f7, f8, f9, f10, f11⟩ := syncC_field zs s
430  have hShape : Shape (resetHeap H s) (setI (r.put (resetHeap H s) (syncOkStream z s)) zs (syncOkState zs s)) :=
431    (shape_put hz0 _).trans (shape_setI (by simpa using hs0) _)
432  have hO2 := hShape.owns (resetHeap_owns hG.uniq hG.inv.win hO)
433  have hwb := windowBlock (winInv_reset hG.inv.win hG.inv.reqbits)
434  have hrw := resetPre_window s
435  by_cases h0 : s.reqbits = 0
436  · have hc : ((syncC zs s).wbits == 0) = true := by simp [f1, h0]
437    have hHeap : syncOkHeap H r zs z s = freeWin (setI (r.put (resetHeap H s) (syncOkStream z s)) zs (syncOkState zs s)) (resetPre s).window := by
438      unfold syncOkHeap; simp [hc, f2]
439    rw [hHeap]
440    rcases hwb with hn | ⟨w, a, hw, hba, hro⟩
441    · rw [hn, freeWin_null]
442      intro b; rw [hO2 b]
443      by_cases hwr : s.wbits = s.reqbits
444      · rw [hwr] at hrw
445        simp only [ite_true] at hrw
446        have : ¬ WinBlk s b := by
447          intro hb; unfold WinBlk at hb; rw [hrw] at hn; simp [hb] at hn
448        simp [SyncKeeps, this, hwr]
449      · simp [SyncKeeps, hwr]
450    · have hwr : s.wbits = s.reqbits := by
451        by_cases hh : s.wbits = s.reqbits
452        · exact hh
453        · rw [ite_eq_right hh] at hrw; rw [hrw] at hw; cases hw
454      rw [ite_eq_left hwr] at hrw
455      have hUX : Uniq (setI (r.put (resetHeap H s) (syncOkStream z s)) zs (syncOkState zs s)) :=
456        hShape.uniq (by
457          unfold resetHeap; split
458          · exact uniq_freeWin hG.uniq _
459          · exact hG.uniq)
460      have hbX : (setI (r.put (resetHeap H s) (syncOkStream z s)) zs (syncOkState zs s)).bytes w = some a := by simpa using hba
461      have := owns_freeWin hUX hbX hO2
462      rw [hw]
463      intro b
464      rw [this b]
465      have hws : s.window = .ref (.blk w) 0 := by rw [← hrw]; exact hw
466      have hWB : WinBlk s b ↔ b = w := by
467        unfold WinBlk; rw [hws]
468        constructor
469        · intro hh; exact (BRef.blk.inj (Ptr.ref.inj hh).1).symm
470        · intro hh; rw [hh]
471      simp [SyncKeeps, hwr, h0, hWB]
472  · have hc : ¬ ((syncC zs s).wbits == 0) = true := by simp [f1, h0]
473    have hHeap : syncOkHeap H r zs z s = setI (r.put (resetHeap H s) (syncOkStream z s)) zs (syncOkState zs s) := by
474      unfold syncOkHeap; simp [hc]
475    rw [hHeap]
476    intro b; rw [hO2 b]
477    simp [SyncKeeps, h0]
478
479end Zlib.Inflate.Proofs
480
481namespace Zlib.Inflate.Spec
482open C
483
484/-- The search state `g` is consistent with the bytes `w` seen so far: either the pattern has not occurred and `g` is the
485longest proper prefix of it that ends `w` (`SyncSt`), or the pattern has occurred in `w` and `g = 4`. -/
486def SyncAt (g : UInt32) (w : List UInt8) : Prop := SyncSt g w ∨ (g = 4 ∧ syncPat <:+: w)
487
488/-- `p + n` for a pointer into a block (`NULL` stays `NULL`: only `n = 0` occurs there). -/
489def syncAdv (p : BPtr) (n : Nat) : BPtr := match p with | .null => .null | .ref r o => .ref r (o + n)
490
491/-- The stream record after the search consumed `N` bytes of input: `avail_in` down, `next_in` and `total_in` up. -/
492def syncAdvance (z : ZStream) (N : UInt32) : ZStream :=
493  { z with avail_in := z.avail_in - N, next_in := syncAdv z.next_in N.toNat, total_in := z.total_in + N.toUInt64 }
494
495end Zlib.Inflate.Spec
496
497namespace Zlib.Inflate.Proofs
498open C Zlib.Inflate Zlib.Inflate.Spec
499
500theorem syncsearch_at {h : Heap} {p : BPtr} {len : UInt32} {bs : List UInt8} (I : SyncIn h p len bs)
501    {g : UInt32} {w : List UInt8} (hA : SyncAt g w) :
502    ∃ N G, syncsearch g p len h = .ok ((N, G), h) ∧ N.toNat ≤ len.toNat ∧
503      (G = 4 → syncPat <:+: w ++ bs.take N.toNat ∧ ∀ L', L' < N.toNat → ¬ syncPat <:+: w ++ bs.take L') ∧
504      (G ≠ 4 → N = len ∧ SyncSt G (w ++ bs)) := by
505  rcases hA with hs | ⟨rfl, hw⟩
506  · obtain ⟨N, G, hr, h1, h2, h3⟩ := syncsearch_spec I hs
507    refine ⟨N, G, hr, h1, ?_, h3⟩
508    intro h4
509    obtain ⟨-, a, b⟩ := h2 h4
510    exact ⟨List.IsSuffix.isInfix a, b⟩
511  · have hlen := syncIn_length I
512    rcases I with ⟨b, a, o, rfl, hg, hl, rfl⟩ | ⟨rfl, rfl, rfl⟩
513    · have := syncsearch_run (r := .blk b) (h := h) (a := a) (o := o) (len := len) 4 hg hl
514      rw [syncScan_ge (by decide)] at this
515      refine ⟨0, 4, by simpa using this, by simp, fun _ => ⟨by simpa using hw, fun L' hL' => by simp at hL'⟩, fun h4 => absurd rfl h4⟩
516    · refine ⟨0, 4, syncsearch_null 4 h, by simp, fun _ => ⟨by simpa using hw, fun L' hL' => by simp at hL'⟩, fun h4 => absurd rfl h4⟩
517
518/-- Reading the search result into the stream: advancing the input pointer by `N ≤ len` bytes. -/
519theorem syncAdd_run {H : Heap} {p : BPtr} {len : UInt32} {bs : List UInt8} (I : SyncIn H p len bs) {N : UInt32}
520    (hN : N.toNat ≤ len.toNat) {H' : Heap} (hb : H'.bytes = H.bytes) :
521    Ptr.add p (N.toNat : Int) H' = .ok (syncAdv p N.toNat, H') := by
522  rcases I with ⟨b, a, o, rfl, hg, hl, rfl⟩ | ⟨rfl, rfl, rfl⟩
523  · have hg' : Space.get H' (BRef.blk b) = some a := by simpa [Space.get, hb] using hg
524    exact Ptr.add_nat_ok (r := BRef.blk b) hg' (by omega)
525  · have : N.toNat = 0 := by simpa using hN
526    rw [this]; rfl
527
528/-- The state record after the search: only `have` changes. -/
529def syncHave (s : InflateState) (G : UInt32) : InflateState := { s with «have» := G }
530
531theorem good_syncSearch {H : Heap} {r : ZStreamRef} {zs : Nat} {z : ZStream} {s : InflateState}
532    (hG : Good H r zs z s) (N : UInt32) (G : UInt32) :
533    Good (setI (r.put H (syncAdvance z N)) zs (syncHave s G)) r zs (syncAdvance z N) (syncHave s G) :=
534  hG.setZI (by simp [syncAdvance]) (by simpa [syncAdvance] using hG.live.zalloc)
535    (by simpa [syncAdvance] using hG.live.zfree) (by simp [syncHave]) (by simpa [syncHave] using hG.live.mode)
536    (hG.inv.of_fields rfl rfl rfl rfl rfl rfl rfl rfl rfl hG.inv.bits rfl rfl rfl)
537
538/-- **The search step of `inflateSync`.** On a stream in the search (`Good`, with the state's `have` consistent with the
539bytes `w` seen so far, `SyncAt`) and an input `next_in[0 .. avail_in)` (`SyncIn`), the part of `inflateSync` from the call
540of `syncsearch` on runs without a fault. It stores the search result in `have`, consumes `N` bytes (`syncAdvance`) and
541returns `Z_DATA_ERROR` if the pattern is not complete (`G ≠ 4`, and then all the input was consumed), else `Z_OK` after the
542reset of the stream (`syncOkHeap`). -/
543theorem syncTail_run {H : Heap} {r : ZStreamRef} {zs : Nat} {z : ZStream} {s : InflateState} {bs w : List UInt8}
544    (hG : Good H r zs z s) (hf : z.zfree = .fn "zcfree") (hI : SyncIn H z.next_in z.avail_in bs)
545    (hA : SyncAt s.«have» w) :
546    ∃ N G, N.toNat ≤ z.avail_in.toNat ∧
547      (G = 4 → syncPat <:+: w ++ bs.take N.toNat ∧ ∀ L', L' < N.toNat → ¬ syncPat <:+: w ++ bs.take L') ∧
548      (G ≠ 4 → N = z.avail_in ∧ SyncSt G (w ++ bs)) ∧
549      Good (setI (r.put H (syncAdvance z N)) zs (syncHave s G)) r zs (syncAdvance z N) (syncHave s G) ∧
550      (G ≠ 4 → syncTail (some r) (some (.tab zs)) H =
551        .ok (Z_DATA_ERROR, setI (r.put H (syncAdvance z N)) zs (syncHave s G))) ∧
552      (G = 4 → syncTail (some r) (some (.tab zs)) H =
553        .ok (Z_OK, syncOkHeap (setI (r.put H (syncAdvance z N)) zs (syncHave s G)) r zs (syncAdvance z N) (syncHave s G))) := by
554  have hL := hG.live
555  obtain ⟨N, G, hse, hN, h4, h3⟩ := syncsearch_at hI hA
556  have hG1 := good_syncSearch hG N G
557  refine ⟨N, G, hN, h4, h3, hG1, fun hne => ?_, fun he => ?_⟩
558  · unfold syncTail
559    isimp [hL.hz, hL.hs, hse, syncAdd_run hI hN (H' := setI H zs { s with «have» := G }) rfl, syncAdvance, syncHave, hne]
560  · subst he
561    unfold syncTail
562    have hdone := syncDone_run (hG1) (by simpa [syncAdvance] using hf)
563    isimp [hL.hz, hL.hs, hse, syncAdd_run hI hN (H' := setI H zs { s with «have» := 4 }) rfl]
564    simpa [syncAdvance, syncHave] using hdone
565
566end Zlib.Inflate.Proofs