inflate.c.end.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.init»
2
3/-!
4# inflate.c: `inflateEnd`, `inflateInit2_`, `inflateInit_`
5-/
6
7namespace Zlib.Inflate.Spec
8open C
9
10/-- The heap after `free(state)`: the state record is gone. -/
11def freeIst (h : Heap) (zs : Nat) : Heap := { h with istates := upd h.istates zs none }
12
13/-- The heap after `inflateEnd`'s two frees: the window block (if any), then the state record. -/
14def endHeap (h : Heap) (zs : Nat) (st : InflateState) : Heap := freeIst (freeWin h st.window) zs
15
16/-- The heap after a successful `ZALLOC` of an inflate state whose content is then set to `st`: the next block number
17holds the record, the counters move. -/
18def allocIstHeap (h : Heap) (st : InflateState) : Heap :=
19  { h with istates := upd h.istates h.nextBlk (some st), nextBlk := h.nextBlk + 1, nalloc := h.nalloc + 1 }
20
21/-- The stream record after the first lines of `inflateInit2_`: no message, and the default allocator functions where
22the caller gave none (`opaque` is cleared with the default `zalloc`). -/
23def initStream (z : ZStream) : ZStream :=
24  { z with
25    msg := .null,
26    zalloc := if z.zalloc == .null then .fn "zcalloc" else z.zalloc,
27    «opaque» := if z.zalloc == .null then .null else z.opaque,
28    zfree := if z.zfree == .null then .fn "zcfree" else z.zfree }
29
30/-- The state record of `inflateInit2_` right after `zmemzero` and the three assignments, before `inflateReset2`. -/
31def initState (r : ZStreamRef) : InflateState :=
32  { InflateState.zeroed with strm := some r, window := .null, mode := HEAD }
33
34/-- The stream record once its state pointer is set to the new state `nb`. -/
35def initStream2 (z : ZStream) (nb : Nat) : ZStream := { initStream z with state := some (.inflate nb) }
36
37/-- The heap after a successful `inflateInit2_` (`wrap` and `wb` from `reset2Params`): the state record is the block
38`h.nextBlk`, built by `reset2Pre`/`inflateReset`; the stream record has the default allocator functions, a message of
39`NULL`, and points to the state. -/
40def initOkHeap (h : Heap) (r : ZStreamRef) (z : ZStream) (wrap wb : Int32) : Heap :=
41  let z2 : ZStream := initStream2 z h.nextBlk
42  let H := allocIstHeap (r.put h z2) (initState r)
43  let st0 := reset2Pre wrap wb (initState r)
44  setI (r.put (reset2Heap H wb (initState r)) (resetKeepStream z2 (resetPre st0))) h.nextBlk
45    (resetKeepState h.nextBlk (resetPre st0))
46
47/-- The heap after `inflateInit2_` found the window bits invalid: the new state was allocated and is freed again, the
48stream's state pointer is `NULL`. -/
49def initBadHeap (h : Heap) (r : ZStreamRef) (z : ZStream) : Heap :=
50  let z2 : ZStream := initStream2 z h.nextBlk
51  r.put (freeIst (allocIstHeap (r.put h z2) (initState r)) h.nextBlk) { z2 with state := none }
52
53/-- The heap after the allocation of the state failed: the stream has its defaults, the allocation counter moved. -/
54def initMemHeap (h : Heap) (r : ZStreamRef) (z : ZStream) : Heap :=
55  { r.put h (initStream z) with nalloc := h.nalloc + 1 }
56
57end Zlib.Inflate.Spec
58
59namespace Zlib.Inflate.Proofs
60open C Zlib.Inflate Zlib.Inflate.Spec
61
62@[simp] theorem freeIst_streams (h : Heap) (zs : Nat) : (freeIst h zs).streams = h.streams := rfl
63@[simp] theorem freeIst_gzstates (h : Heap) (zs : Nat) : (freeIst h zs).gzstates = h.gzstates := rfl
64@[simp] theorem freeIst_bytes (h : Heap) (zs : Nat) : (freeIst h zs).bytes = h.bytes := rfl
65@[simp] theorem freeIst_nextBlk (h : Heap) (zs : Nat) : (freeIst h zs).nextBlk = h.nextBlk := rfl
66@[simp] theorem freeIst_ro (h : Heap) (zs : Nat) : (freeIst h zs).ro = h.ro := rfl
67
68@[simp] theorem ZStreamRef.get_freeIst (h : Heap) (zs : Nat) (r : ZStreamRef) : r.get (freeIst h zs) = r.get h := by
69  cases r <;> simp [ZStreamRef.get]
70
71@[simp] theorem ZStreamRef.put_freeIst (h : Heap) (zs : Nat) (r : ZStreamRef) (v : ZStream) :
72    r.put (freeIst h zs) v = freeIst (r.put h v) zs := by
73  cases r <;> simp [ZStreamRef.put, freeIst] <;> split <;> rfl
74
75theorem uniq_freeIst {h : Heap} (hU : Uniq h) (zs : Nat) : Uniq (freeIst h zs) := by
76  intro b
77  have := hU b
78  by_cases hb : b = zs
79  · subst hb; simp only [freeIst, upd_same, cnt_none]; omega
80  · simpa only [freeIst, upd_ne _ _ _ _ hb] using this
81
82theorem fresh_freeIst {h : Heap} (hF : Fresh h) (zs : Nat) : Fresh (freeIst h zs) := by
83  intro b hb hl
84  apply hF b (by simpa using hb)
85  by_cases hbz : b = zs
86  · subst hbz
87    simp only [Heap.live, freeIst, upd_same] at hl
88    rcases hl with hl | hl | hl | hl | hl | hl | hl
89    · exact Or.inl hl
90    · exact Or.inr (Or.inl hl)
91    · exact Or.inr (Or.inr (Or.inl hl))
92    · exact Or.inr (Or.inr (Or.inr (Or.inl hl)))
93    · exact Or.inr (Or.inr (Or.inr (Or.inr (Or.inl hl))))
94    · exact absurd rfl hl
95    · exact Or.inr (Or.inr (Or.inr (Or.inr (Or.inr (Or.inr hl)))))
96  · simpa only [Heap.live, freeIst, upd_ne _ _ _ _ hbz] using hl
97
98theorem owns_freeIst {h : Heap} (hU : Uniq h) {zs : Nat} {s : InflateState} (hs : h.istates zs = some s) {S : Nat → Prop}
99    (hO : h.Owns S) : (freeIst h zs).Owns (fun b => S b ∧ b ≠ zs) := by
100  intro b
101  by_cases hbz : b = zs
102  · subst hbz
103    obtain ⟨e1, e2, e3, e4, e5, e6⟩ := Uniq.istates_only hU hs
104    simp [Heap.live, freeIst, e1, e2, e3, e4, e5, e6]
105  · have := hO b
106    simp only [Heap.live, freeIst, upd_ne _ _ _ _ hbz] at this ⊢
107    simp [hbz, this]
108
109theorem zfrees_run {h : Heap} {r : ZStreamRef} {z : ZStream} (hz : r.get h = some z) (hf : z.zfree = .fn "zcfree")
110    {zs : Nat} {s : InflateState} (hs : h.istates zs = some s) :
111    ZFREES (some r) (some (.tab zs)) h = .ok ((), freeIst h zs) := by
112  simp [ZFREES, ldZ_eq, hz, hf, freeInflateState_tab hs, freeIst]
113
114/-- **inflateEnd, safety and ownership.** On an initialised stream with the default `zfree` the call returns `Z_OK`
115without a fault. It frees exactly the window block (if there is one) and the state record, and sets the stream's
116state pointer to `NULL`. Nothing is allocated. Afterwards the live blocks are the old ones except the state and the
117window: if the stream owned them with the blocks `S` before, it owns `S` minus its own two after (no leak, no double
118free), and the stream check now fails. -/
119theorem inflateEnd_safe {h : Heap} {r : ZStreamRef} {zs : Nat} {z : ZStream} {st : InflateState}
120    (hG : Good h r zs z st) (hf : z.zfree = .fn "zcfree") :
121    ∃ h', C.run (inflateEnd (some r)) h = .ok (Z_OK, h') ∧
122      h' = r.put (endHeap h zs st) { z with state := none } ∧
123      Uniq h' ∧ Fresh h' ∧ r.get h' = some { z with state := none } ∧
124      (∀ S, h.Owns S → h'.Owns (fun b => S b ∧ ¬ OwnedBy zs st b)) ∧
125      inflateStateCheck (some r) h' = .ok (1, h') := by
126  have hL := hG.live
127  have hz := hL.hz
128  have hs := hL.hs
129  have hwo := windowBlock hG.inv.win
130  have hU1 : Uniq (freeWin h st.window) := uniq_freeWin hG.uniq _
131  have hs1 : (freeWin h st.window).istates zs = some st := by simpa using hs
132  have hz1 : r.get (freeWin h st.window) = some z := by simpa using hz
133  have hrun : inflateEnd (some r) h = .ok (Z_OK, r.put (endHeap h zs st) { z with state := none }) := by
134    unfold inflateEnd
135    rcases hwo with hn | ⟨b, a, hb, hba, hro⟩
136    · isimp [stateCheck_live hL, hL.zst, hz, hs, hn, zfrees_run (z := z) (by simpa using hz) hf (by simpa using hs : h.istates zs = some st), endHeap, freeWin_null]
137    · have hz2 : r.get (freeWin h (.ref (.blk b) 0)) = some z := by simpa using hz
138      have hs2 : (freeWin h (.ref (.blk b) 0)).istates zs = some st := by simpa using hs
139      have e : endHeap h zs st = freeIst (freeWin h (.ref (.blk b) 0)) zs := by simp [endHeap, hb]
140      rw [e]
141      isimp [stateCheck_live hL, hL.zst, hz, hs, hb, zfreeB_run (p := .ref (.blk b) 0) hz hf (Or.inr ⟨b, a, rfl, hba, hro⟩),
142        zfrees_run hz2 hf hs2]
143  have hpost : (r.put (endHeap h zs st) { z with state := none }).istates = (endHeap h zs st).istates := by simp
144  refine ⟨_, hrun, rfl, ?_, ?_, ?_, ?_, ?_⟩
145  · have : Uniq (endHeap h zs st) := uniq_freeIst hU1 zs
146    exact (shape_put (by simp [endHeap, hz] : r.get (endHeap h zs st) = some z) _).uniq this
147  · have : Fresh (endHeap h zs st) := fresh_freeIst (fresh_freeWin hG.fresh _) zs
148    exact (shape_put (by simp [endHeap, hz] : r.get (endHeap h zs st) = some z) _).fresh (by simp [endHeap]) this
149  · simp [endHeap, hz]
150  · intro S hO
151    have hO1 : (freeWin h st.window).Owns (fun b => S b ∧ ¬ WinBlk st b) := by
152      rcases hwo with hn | ⟨b, a, hb, hba, hro⟩
153      · rw [hn, freeWin_null]
154        intro x; rw [hO x]; simp [WinBlk, hn]
155      · rw [hb]
156        have := owns_freeWin hG.uniq hba hO
157        intro x
158        rw [this x]
159        constructor
160        · rintro ⟨h1, h2⟩; refine ⟨h1, ?_⟩
161          intro hh; unfold WinBlk at hh; rw [hb] at hh
162          exact h2 (BRef.blk.inj (Ptr.ref.inj hh).1).symm
163        · rintro ⟨h1, h2⟩; refine ⟨h1, ?_⟩
164          intro hh; apply h2; unfold WinBlk; rw [hb, hh]
165    have hO2 := owns_freeIst hU1 hs1 hO1
166    have hO3 : (endHeap h zs st).Owns (fun b => S b ∧ ¬ OwnedBy zs st b) := by
167      intro x
168      rw [show endHeap h zs st = freeIst (freeWin h st.window) zs from rfl, hO2 x]
169      constructor
170      · rintro ⟨⟨h1, h2⟩, h3⟩
171        refine ⟨h1, ?_⟩
172        rintro (e | ⟨w, hw, e⟩)
173        · exact h3 e
174        · subst e; exact h2 hw
175      · rintro ⟨h1, h2⟩
176        exact ⟨⟨h1, fun hw => h2 (Or.inr ⟨x, hw, rfl⟩)⟩, fun e => h2 (Or.inl e)⟩
177    exact (shape_put (by simp [endHeap, hz] : r.get (endHeap h zs st) = some z) _).owns hO3
178  · have hget : r.get (r.put (endHeap h zs st) { z with state := none }) = some { z with state := none } := by
179      simp [endHeap, hz]
180    have hD : StreamDom (r.put (endHeap h zs st) { z with state := none }) (some r) :=
181      Or.inr ⟨r, { z with state := none }, rfl, hget, Or.inr (Or.inr (Or.inl rfl))⟩
182    have hN : ¬ Initialised (r.put (endHeap h zs st) { z with state := none }) (some r) := by
183      rintro ⟨r', zs', z', st', hh, hLL⟩
184      cases hh
185      have h1 := hLL.hz
186      rw [hget] at h1
187      cases h1
188      have := hLL.zst
189      simp at this
190    exact notInit_check hD hN
191
192
193theorem stInv_rk {h : Heap} {zs : Nat} {st : InflateState} (hwf : st.WellFormed) (hw : WinInv h st)
194    (hq : st.reqbits.toNat ≤ 15) : StInv h zs (resetKeepState zs st) :=
195  ⟨wf_resetKeepState hwf, ⟨hw.wbits, hw.block, hw.nullws, hw.ws, hw.hv, hw.wn, hw.eq⟩, hq, by simp [resetKeepState],
196    ⟨⟨0, by simp [resetKeepState], by omega⟩,
197      Or.inl ⟨0, 0, by simp [resetKeepState], by simp [resetKeepState], by omega, by omega⟩⟩⟩
198
199end Zlib.Inflate.Proofs