inflate.c.sync3.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.sync2»
2
3/-!
4# inflate.c: `inflateSync`, the whole call
5
6The call makes the local array `buf[4]`, runs the search and frees `buf` before returning.
7-/
8
9namespace Zlib.Inflate.Proofs
10open C Zlib.Inflate _root_.Zlib.Inflate.Spec
11
12theorem freeWin_bytes_ne (H : Heap) (p : BPtr) {b : Nat} (hp : ∀ w, p = .ref (.blk w) 0 → w ≠ b) :
13    (freeWin H p).bytes b = H.bytes b ∧ (freeWin H p).ro b = H.ro b := by
14  cases p with
15  | null => exact ⟨rfl, rfl⟩
16  | ref x o =>
17    cases x with
18    | blk w =>
19      cases o with
20      | zero => have := hp w rfl; simp [freeWin, upd_ne _ _ _ _ (Ne.symm this)]
21      | succ o => exact ⟨rfl, rfl⟩
22    | _ => exact ⟨rfl, rfl⟩
23
24theorem syncIn_syncAlloc {h : Heap} (hF : Fresh h) {p : BPtr} {len : UInt32} {bs : List UInt8}
25    (I : SyncIn h p len bs) : SyncIn (syncAlloc h) p len bs := by
26  rcases I with ⟨b, a, o, rfl, hg, hl, rfl⟩ | h2
27  · have hb : b ≠ h.nextBlk := by
28      intro e; subst e
29      obtain ⟨e0, -⟩ := fresh_dead hF (Nat.le_refl _)
30      rw [hg] at e0; cases e0
31    exact Or.inl ⟨b, a, o, rfl, by rw [syncAlloc_bytes_ne h hb]; exact hg, hl, rfl⟩
32  · exact Or.inr h2
33
34theorem win_ne_buf {h : Heap} {st : InflateState} (hF : Fresh h) (hW : WinInv h st) :
35    ∀ w, st.window = .ref (.blk w) 0 → w ≠ h.nextBlk := by
36  intro w hw e
37  subst e
38  rcases hW.block with hn | ⟨w', a, hw', ha, -⟩
39  · rw [hn] at hw; cases hw
40  · rw [hw] at hw'
41    have := (BRef.blk.inj (Ptr.ref.inj hw').1)
42    subst this
43    obtain ⟨e0, -⟩ := fresh_dead hF (Nat.le_refl _)
44    rw [ha] at e0; cases e0
45
46theorem syncOkHeap_bytes_ne (H : Heap) (r : ZStreamRef) (zs : Nat) (z : ZStream) (s : InflateState) {b : Nat}
47    (hb : ∀ w, s.window = .ref (.blk w) 0 → w ≠ b) :
48    (syncOkHeap H r zs z s).bytes b = H.bytes b ∧ (syncOkHeap H r zs z s).ro b = H.ro b := by
49  have hrp : ∀ w, (resetPre s).window = .ref (.blk w) 0 → w ≠ b := by
50    intro w hw
51    rw [resetPre_window] at hw
52    split at hw
53    · exact hb w hw
54    · cases hw
55  have hrh : (resetHeap H s).bytes b = H.bytes b ∧ (resetHeap H s).ro b = H.ro b := by
56    unfold resetHeap; split
57    · exact freeWin_bytes_ne H _ hb
58    · exact ⟨rfl, rfl⟩
59  unfold syncOkHeap
60  split
61  · have := freeWin_bytes_ne (setI (r.put (resetHeap H s) (syncOkStream z s)) zs (syncOkState zs s)) (syncC zs s).window
62      (by rw [(syncC_field zs s).2.1]; exact hrp)
63    simpa [hrh.1, hrh.2] using this
64  · simpa [hrh.1, hrh.2]
65
66theorem good_freeBuf {H : Heap} {r : ZStreamRef} {zs : Nat} {z : ZStream} {st : InflateState} {nb : Nat}
67    (hG : Good H r zs z st) (hn : ∀ w, st.window = .ref (.blk w) 0 → w ≠ nb) :
68    Good (freeWin H (.ref (.blk nb) 0)) r zs z st := by
69  obtain ⟨⟨hz, hs, zst, back, hm, za, zf⟩, ⟨wf, win, rq, bits, ptr⟩, hU, hF⟩ := hG
70  refine ⟨⟨by simpa using hz, by simpa using hs, zst, back, hm, za, zf⟩, ⟨wf, ?_, rq, bits, ptr⟩,
71    uniq_freeWin hU _, fresh_freeWin hF _⟩
72  refine ⟨win.wbits, ?_, win.nullws, win.ws, win.hv, win.wn, win.eq⟩
73  rcases win.block with h0 | ⟨w, a, hw, ha, hro, hsz⟩
74  · exact Or.inl h0
75  · have hne := hn w hw
76    have := freeWin_bytes_ne H (.ref (.blk nb) 0) (b := w) (by intro w' e; have := BRef.blk.inj (Ptr.ref.inj e).1; subst this; exact Ne.symm hne)
77    exact Or.inr ⟨w, a, hw, by rw [this.1]; exact ha, by rw [this.2]; exact hro, hsz⟩
78
79theorem syncOkState_window_ref {zs : Nat} {s : InflateState} {w : Nat}
80    (h : (syncOkState zs s).window = .ref (.blk w) 0) : s.window = .ref (.blk w) 0 := by
81  by_cases h0 : s.reqbits = 0
82  · rw [syncOkState_eq0 h0] at h; cases h
83  · rw [syncOkState_ne0 h0, ] at h
84    have h2 : (syncC zs s).window = .ref (.blk w) 0 := h
85    rw [(syncC_field zs s).2.1, resetPre_window] at h2
86    split at h2
87    · assumption
88    · cases h2
89
90/-- **inflateSync, continuing a search** (`mode = SYNC` already, as after an earlier call that returned `Z_DATA_ERROR`).
91The state's `have` is consistent with the bytes `w` searched so far (`SyncAt`); `zlib.h`: more input is given in
92`next_in[0 .. avail_in)` (`SyncIn`) and there is input or a whole byte in the bit buffer. The call never faults. It
93searches the input from `have` (`syncScan_spec` describes `N` and `G`) and consumes `N` bytes (`syncAdvance`). If the
94pattern is not complete (`G ≠ 4`) it returns `Z_DATA_ERROR`, all input is consumed, only `have` changes in the state, and
95the mode stays `SYNC`. If it is complete it returns `Z_OK` and the heap is `syncOkHeap` (the stream is reset but the
96totals are kept, mode `TYPE`). The local array is made and freed (its block number is used up). Default `zfree` only. -/
97theorem inflateSync_resume {h : Heap} {r : ZStreamRef} {zs : Nat} {z : ZStream} {st : InflateState} {bs w : List UInt8}
98    (hG : Good h r zs z st) (hf : z.zfree = .fn "zcfree") (hmode : st.mode = SYNC)
99    (hprog : ¬ (z.avail_in = 0 ∧ st.bits < 8)) (hI : SyncIn h z.next_in z.avail_in bs) (hA : SyncAt st.«have» w) :
100    ∃ N G, N.toNat ≤ z.avail_in.toNat ∧
101      (G = 4 → syncPat <:+: w ++ bs.take N.toNat ∧ ∀ L', L' < N.toNat → ¬ syncPat <:+: w ++ bs.take L') ∧
102      (G ≠ 4 → N = z.avail_in ∧ SyncSt G (w ++ bs)) ∧
103      (G ≠ 4 → ∃ h', C.run (inflateSync (some r)) h = .ok (Z_DATA_ERROR, h') ∧
104        h' = freeWin (setI (r.put (syncAlloc h) (syncAdvance z N)) zs (syncHave st G)) (syncBuf h) ∧
105        Good h' r zs (syncAdvance z N) (syncHave st G)) ∧
106      (G = 4 → ∃ h', C.run (inflateSync (some r)) h = .ok (Z_OK, h') ∧
107        h' = freeWin (syncOkHeap (setI (r.put (syncAlloc h) (syncAdvance z N)) zs (syncHave st G)) r zs (syncAdvance z N) (syncHave st G)) (syncBuf h) ∧
108        Good h' r zs (syncOkStream (syncAdvance z N) (syncHave st G)) (syncOkState zs (syncHave st G))) := by
109  have hF := hG.fresh
110  have hG0 := good_syncAlloc hG
111  have hI0 := syncIn_syncAlloc hF hI
112  have hwn := win_ne_buf hF hG.inv.win
113  obtain ⟨N, G, hN, h4, h3, hG1, hne, he⟩ := syncTail_run hG0 hf hI0 hA
114  have hL0 := hG0.live
115  have hbb : (syncAlloc h).bytes h.nextBlk = some (syncJunk h) := syncAlloc_bytes_buf h
116  refine ⟨N, G, hN, h4, h3, fun hG4 => ?_, fun hG4 => ?_⟩
117  · refine ⟨_, ?_, rfl, ?_⟩
118    · show inflateSync (some r) h = _
119      rw [inflateSync_split]
120      isimp [allocLocalB_run h hF, stateCheck_live hL0, hL0.zst, hG.live.hz, hG.live.hs, hprog, hmode, hne hG4,
121        freeBuf_run (H := setI (r.put (syncAlloc h) (syncAdvance z N)) zs (syncHave st G)) (nb := h.nextBlk) (a := syncJunk h)
122          (by simpa using hbb) (by simp [syncAlloc_ro_buf]), syncBuf]
123    · exact good_freeBuf (nb := h.nextBlk) hG1 (fun w hw => hwn w (by simpa [syncHave] using hw))
124  · refine ⟨_, ?_, rfl, ?_⟩
125    · have hbn : ∀ w', (syncHave st G).window = .ref (.blk w') 0 → w' ≠ h.nextBlk := fun w' hw' => hwn w' (by simpa [syncHave] using hw')
126      have hby := syncOkHeap_bytes_ne (setI (r.put (syncAlloc h) (syncAdvance z N)) zs (syncHave st G)) r zs (syncAdvance z N) (syncHave st G) hbn
127      show inflateSync (some r) h = _
128      rw [inflateSync_split]
129      isimp [allocLocalB_run h hF, stateCheck_live hL0, hL0.zst, hG.live.hz, hG.live.hs, hprog, hmode, he hG4,
130        freeBuf_run (H := syncOkHeap (setI (r.put (syncAlloc h) (syncAdvance z N)) zs (syncHave st G)) r zs (syncAdvance z N) (syncHave st G))
131          (nb := h.nextBlk) (a := syncJunk h) (by rw [hby.1]; simpa using hbb) (by rw [hby.2]; simp [syncAlloc_ro_buf]), syncBuf]
132    · have hGd := (syncDone_good hG1).1
133      exact good_freeBuf (nb := h.nextBlk) hGd (fun w hw => hwn w (by simpa [syncHave] using syncOkState_window_ref hw))
134
135end Zlib.Inflate.Proofs