deflate.c.life.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.«deflate.c.base»
2
3/-!
4# deflate.c: `deflateEnd`
5
6`deflateEnd` frees the four buffers (`pending_buf`, `head`, `prev`, `window`, in this order) and the state, clears
7`strm->state`, and returns `Z_DATA_ERROR` if the stream was in the middle of a block (`BUSY_STATE`) and `Z_OK` otherwise.
8-/
9
10namespace Zlib.Deflate.Spec
11open C
12
13/-- The heap after `free(p)` of a byte pointer that is `NULL` or the start of a block. -/
14def freeBytes (h : Heap) (p : BPtr) : Heap :=
15  match p with
16  | .ref (.blk w) 0 => { h with bytes := upd h.bytes w none }
17  | _ => h
18
19/-- The heap after `free(p)` of a pointer to words that is `NULL` or the start of a block. -/
20def freeWords (h : Heap) (p : WPtr) : Heap :=
21  match p with
22  | .ref (.blk w) 0 => { h with words := upd h.words w none }
23  | _ => h
24
25/-- The heap after `deflateEnd` of the stream `r` (record `z`) whose state is the record `d` at block `ds`: the four
26buffers and the state record are gone, and the stream record has `state = NULL`. -/
27def endHeap (h : Heap) (r : ZStreamRef) (ds : Nat) (z : ZStream) (d : DeflateState) : Heap :=
28  { r.put (freeBytes (freeWords (freeWords (freeBytes h d.pending_buf) d.head) d.prev) d.window) { z with state := none }
29    with dstates := upd h.dstates ds none }
30
31end Zlib.Deflate.Spec
32
33namespace Zlib.Deflate.Proofs
34open C Zlib.Deflate Zlib.Deflate.Spec
35
36@[simp] theorem freeBytes_dstates (h : Heap) (p : BPtr) : (freeBytes h p).dstates = h.dstates := by
37  unfold freeBytes; split <;> rfl
38@[simp] theorem freeBytes_streams (h : Heap) (p : BPtr) : (freeBytes h p).streams = h.streams := by
39  unfold freeBytes; split <;> rfl
40@[simp] theorem freeBytes_gzstates (h : Heap) (p : BPtr) : (freeBytes h p).gzstates = h.gzstates := by
41  unfold freeBytes; split <;> rfl
42@[simp] theorem freeBytes_words (h : Heap) (p : BPtr) : (freeBytes h p).words = h.words := by
43  unfold freeBytes; split <;> rfl
44@[simp] theorem freeBytes_nextBlk (h : Heap) (p : BPtr) : (freeBytes h p).nextBlk = h.nextBlk := by
45  unfold freeBytes; split <;> rfl
46@[simp] theorem freeWords_dstates (h : Heap) (p : WPtr) : (freeWords h p).dstates = h.dstates := by
47  unfold freeWords; split <;> rfl
48@[simp] theorem freeWords_streams (h : Heap) (p : WPtr) : (freeWords h p).streams = h.streams := by
49  unfold freeWords; split <;> rfl
50@[simp] theorem freeWords_gzstates (h : Heap) (p : WPtr) : (freeWords h p).gzstates = h.gzstates := by
51  unfold freeWords; split <;> rfl
52@[simp] theorem freeWords_bytes (h : Heap) (p : WPtr) : (freeWords h p).bytes = h.bytes := by
53  unfold freeWords; split <;> rfl
54@[simp] theorem freeWords_nextBlk (h : Heap) (p : WPtr) : (freeWords h p).nextBlk = h.nextBlk := by
55  unfold freeWords; split <;> rfl
56@[simp] theorem freeWords_ro (h : Heap) (p : WPtr) : (freeWords h p).ro = h.ro := by
57  unfold freeWords; split <;> rfl
58@[simp] theorem freeBytes_ro (h : Heap) (p : BPtr) : (freeBytes h p).ro = h.ro := by
59  unfold freeBytes; split <;> rfl
60@[simp] theorem freeWords_gzheaders (h : Heap) (p : WPtr) : (freeWords h p).gzheaders = h.gzheaders := by
61  unfold freeWords; split <;> rfl
62@[simp] theorem freeBytes_gzheaders (h : Heap) (p : BPtr) : (freeBytes h p).gzheaders = h.gzheaders := by
63  unfold freeBytes; split <;> rfl
64@[simp] theorem freeWords_istates (h : Heap) (p : WPtr) : (freeWords h p).istates = h.istates := by
65  unfold freeWords; split <;> rfl
66@[simp] theorem freeBytes_istates (h : Heap) (p : BPtr) : (freeBytes h p).istates = h.istates := by
67  unfold freeBytes; split <;> rfl
68
69@[simp] theorem ZStreamRef.get_freeBytes (h : Heap) (p : BPtr) (r : ZStreamRef) : r.get (freeBytes h p) = r.get h := by
70  cases r <;> simp [ZStreamRef.get]
71@[simp] theorem ZStreamRef.get_freeWords (h : Heap) (p : WPtr) (r : ZStreamRef) : r.get (freeWords h p) = r.get h := by
72  cases r <;> simp [ZStreamRef.get]
73
74theorem zfreeB_run {h : Heap} {r : ZStreamRef} {z : ZStream} (hz : r.get h = some z) (hf : z.zfree = .fn "zcfree")
75    {p : BPtr} (hp : p = .null ∨ ∃ b a, p = .ref (.blk b) 0 ∧ h.bytes b = some a ∧ h.ro b = false) :
76    ZFREE_bytes (some r) p h = .ok ((), freeBytes h p) := by
77  rcases hp with rfl | ⟨b, a, rfl, hb, hro⟩
78  · simp [ZFREE_bytes, zfree_default, ldZ_eq, hz, hf, freeBytes, freeB_null, bind_app]
79  · simp [ZFREE_bytes, zfree_default, ldZ_eq, hz, hf, freeBytes, freeB_ok hb hro, bind_app]
80
81theorem zfreeW_run {h : Heap} {r : ZStreamRef} {z : ZStream} (hz : r.get h = some z) (hf : z.zfree = .fn "zcfree")
82    {p : WPtr} (hp : p = .null ∨ ∃ b a, p = .ref (.blk b) 0 ∧ h.words b = some a) :
83    ZFREE_words (some r) p h = .ok ((), freeWords h p) := by
84  rcases hp with rfl | ⟨b, a, rfl, hb⟩
85  · simp [ZFREE_words, zfree_default, ldZ_eq, hz, hf, freeWords, bind_app]; rfl
86  · simp [ZFREE_words, zfree_default, ldZ_eq, hz, hf, freeWords, freeW_ok hb, bind_app]
87
88
89@[simp] theorem ZStreamRef.get_dstates (g : Heap) (r : ZStreamRef) (t : Tbl (Option DeflateState)) :
90    r.get { g with dstates := t } = r.get g := by cases r <;> rfl
91
92theorem ZStreamRef.put_with_dstates (g : Heap) (r : ZStreamRef) (t : Tbl (Option DeflateState)) (v : ZStream) :
93    r.put { g with dstates := t } v = { r.put g v with dstates := t } := by
94  cases r with
95  | tab i => simp only [ZStreamRef.put]; cases g.streams i <;> rfl
96  | in_gzstate_strm i => simp only [ZStreamRef.put]; cases g.gzstates i <;> rfl
97
98theorem zfree_default_run {h : Heap} {r : ZStreamRef} {z : ZStream} (hz : r.get h = some z)
99    (hf : z.zfree = .fn "zcfree") : zfree_default (some r) h = .ok ((), h) := by
100  simp [zfree_default, ldZ_eq, hz, hf, bind_app]
101
102theorem freeDeflateState_free_ok {h' : Heap} {ds : Nat} {d : DeflateState} (hd : h'.dstates ds = some d) :
103    freeDeflateState (some (.tab ds)) h' = .ok ((), { h' with dstates := upd h'.dstates ds none }) :=
104  freeDeflateState_tab hd
105
106theorem deflateEnd_run {h : Heap} {r : ZStreamRef} {ds : Nat} {z : ZStream} {d : DeflateState} {w p q b : Nat}
107    (hL : DLive h r ds z d) (hf : z.zfree = .fn "zcfree") (hB : DBlocks h d w p q b) :
108    deflateEnd (some r) h =
109      .ok ((if d.status == BUSY_STATE then Z_DATA_ERROR else Z_OK), endHeap h r ds z d) := by
110  obtain ⟨wa, hwa, -⟩ := hB.wa
111  obtain ⟨pa, hpa, -⟩ := hB.pa
112  obtain ⟨qa, hqa, -⟩ := hB.qa
113  obtain ⟨ba, hba, -⟩ := hB.ba
114  have hbw : b ≠ w := fun e => hB.wb e.symm
115  have f1 := zfreeB_run (h := h) hL.hz hf (p := d.pending_buf) (Or.inr ⟨b, ba, hB.pbuf, hba, hB.bro⟩)
116  have f2 := zfreeW_run (h := freeBytes h d.pending_buf) (r := r) (z := z) (by simpa using hL.hz) hf (p := d.head)
117    (Or.inr ⟨q, qa, hB.head, by simpa using hqa⟩)
118  have f3 := zfreeW_run (h := freeWords (freeBytes h d.pending_buf) d.head) (r := r) (z := z) (by simpa using hL.hz) hf
119    (p := d.prev) (Or.inr ⟨p, pa, hB.prev, by
120      have : (freeWords (freeBytes h d.pending_buf) d.head).words p = h.words p := by
121        rw [hB.head]; simp [freeWords, upd_ne _ _ _ _ hB.pq]
122      rw [this]; exact hpa⟩)
123  have f4 := zfreeB_run (h := freeWords (freeWords (freeBytes h d.pending_buf) d.head) d.prev) (r := r) (z := z)
124    (by simpa using hL.hz) hf (p := d.window) (Or.inr ⟨w, wa, hB.win, by
125      simp only [freeWords_bytes, freeBytes, hB.pbuf, hB.win]
126      simp [upd_ne _ _ _ _ hbw.symm, hwa], by simpa using hB.wro⟩)
127  simp only [hB.pbuf, hB.head, hB.prev, hB.win] at f1 f2 f3 f4
128  unfold deflateEnd
129  dsimp' [stateCheck_live hL, hL.zst, hL.hz, hL.hs, hB.pbuf, hB.head, hB.prev, hB.win, f1, f2, f3, f4]
130  have hz' : ∀ h' : Heap, r.get h' = r.get h → zfree_default (some r) h' = .ok ((), h') := fun h' e =>
131    zfree_default_run (by rw [e]; exact hL.hz) hf
132  rw [hz']
133  · simp only [bind_app, pure_app]
134    rw [freeDeflateState_free_ok (d := d)]
135    · simp only [ZStreamRef.get_dstates, ZStreamRef.get_freeBytes, ZStreamRef.get_freeWords, hL.hz,
136        ZStreamRef.put_with_dstates, endHeap, hB.win, hB.prev, hB.head, hB.pbuf, freeBytes_dstates, freeWords_dstates]
137    · simp [hL.hs]
138  · simp
139
140
141theorem endHeap_eq {h : Heap} {r : ZStreamRef} {ds : Nat} {z : ZStream} {d : DeflateState} {w p q b : Nat}
142    (hB : DBlocks h d w p q b) :
143    endHeap h r ds z d = { r.put { h with bytes := upd (upd h.bytes b none) w none,
144                                          words := upd (upd h.words q none) p none } { z with state := none }
145                           with dstates := upd h.dstates ds none } := by
146  unfold endHeap
147  rw [hB.win, hB.prev, hB.head, hB.pbuf]
148  simp only [freeBytes, freeWords]
149
150theorem DOwned_iff {d : DeflateState} {ds w p q b : Nat} {h : Heap} (hB : DBlocks h d w p q b) (x : Nat) :
151    DOwned d ds x ↔ x = ds ∨ x = w ∨ x = p ∨ x = q ∨ x = b := by
152  unfold DOwned
153  rw [hB.win, hB.prev, hB.head, hB.pbuf]
154  constructor
155  · rintro (h1 | ⟨w', h2, h3⟩ | ⟨p', h2, h3⟩ | ⟨q', h2, h3⟩ | ⟨b', h2, h3⟩)
156    · exact Or.inl h1
157    · cases h2; exact Or.inr (Or.inl h3)
158    · cases h2; exact Or.inr (Or.inr (Or.inl h3))
159    · cases h2; exact Or.inr (Or.inr (Or.inr (Or.inl h3)))
160    · cases h2; exact Or.inr (Or.inr (Or.inr (Or.inr h3)))
161  · rintro (h1 | h1 | h1 | h1 | h1)
162    · exact Or.inl h1
163    · exact Or.inr (Or.inl ⟨w, by simp, h1⟩)
164    · exact Or.inr (Or.inr (Or.inl ⟨p, by simp, h1⟩))
165    · exact Or.inr (Or.inr (Or.inr (Or.inl ⟨q, by simp, h1⟩)))
166    · exact Or.inr (Or.inr (Or.inr (Or.inr ⟨b, by simp, h1⟩)))
167
168theorem ZStreamRef.get_bw (g : Heap) (r : ZStreamRef) (bs : Tbl (Option (Array UInt8))) (ws : Tbl (Option (Array UInt16))) :
169    r.get { g with bytes := bs, words := ws } = r.get g := by cases r <;> rfl
170
171theorem ZStreamRef.put_streams (r : ZStreamRef) (g : Heap) (v : ZStream) (x : Nat)
172    (hx : ∀ i, r = .tab i → x ≠ i) : (r.put g v).streams x = g.streams x := by
173  cases r with
174  | tab i => 
175    have := hx i rfl
176    simp only [ZStreamRef.put]; split <;> simp [upd_apply, this]
177  | in_gzstate_strm i => simp only [ZStreamRef.put]; split <;> rfl
178
179theorem ZStreamRef.put_gzstates (r : ZStreamRef) (g : Heap) (v : ZStream) (x : Nat)
180    (hx : ∀ i, r = .in_gzstate_strm i → x ≠ i) : (r.put g v).gzstates x = g.gzstates x := by
181  cases r with
182  | tab i => simp only [ZStreamRef.put]; split <;> rfl
183  | in_gzstate_strm i =>
184    have := hx i rfl
185    simp only [ZStreamRef.put]; split <;> simp [upd_apply, this]
186
187theorem endHeap_tables {h : Heap} {r : ZStreamRef} {ds : Nat} {z : ZStream} {d : DeflateState} {w p q b : Nat}
188    (hB : DBlocks h d w p q b) (hz : r.get h = some z) (x : Nat) :
189    (endHeap h r ds z d).bytes x = (if x = w ∨ x = b then none else h.bytes x) ∧
190    (endHeap h r ds z d).words x = (if x = p ∨ x = q then none else h.words x) ∧
191    (endHeap h r ds z d).dstates x = (if x = ds then none else h.dstates x) ∧
192    ((endHeap h r ds z d).streams x).isSome = (h.streams x).isSome ∧
193    ((endHeap h r ds z d).gzstates x).isSome = (h.gzstates x).isSome ∧
194    (endHeap h r ds z d).gzheaders x = h.gzheaders x ∧ (endHeap h r ds z d).istates x = h.istates x := by
195  have hS : Shape { h with bytes := upd (upd h.bytes b none) w none, words := upd (upd h.words q none) p none }
196      (r.put { h with bytes := upd (upd h.bytes b none) w none, words := upd (upd h.words q none) p none }
197        { z with state := none }) := shape_put (by rw [ZStreamRef.get_bw]; exact hz) _
198  obtain ⟨-, -, e4, -, -, -, e5⟩ := hS x
199  rw [endHeap_eq hB]
200  refine ⟨?_, ?_, ?_, ?_, ?_, ?_, ?_⟩
201  · simp only [ZStreamRef.put_bytes]; simp only [upd_apply]
202    by_cases h1 : x = w <;> by_cases h2 : x = b <;> simp [h1, h2]
203  · simp only [ZStreamRef.put_words]; simp only [upd_apply]
204    by_cases h1 : x = p <;> by_cases h2 : x = q <;> simp [h1, h2]
205  · simp only [ZStreamRef.put_dstates]; simp only [upd_apply]
206  · exact e4
207  · exact e5
208  · simp
209  · simp
210
211theorem endHeap_live {h : Heap} {r : ZStreamRef} {ds : Nat} {z : ZStream} {d : DeflateState} {w p q b : Nat}
212    (hB : DBlocks h d w p q b) (hU : Uniq h) (hz : r.get h = some z) (hs : h.dstates ds = some d) (x : Nat) :
213    (endHeap h r ds z d).live x ↔ h.live x ∧ ¬ (x = ds ∨ x = w ∨ x = p ∨ x = q ∨ x = b) := by
214  obtain ⟨wa, hwa, -⟩ := hB.wa
215  obtain ⟨pa, hpa, -⟩ := hB.pa
216  obtain ⟨qa, hqa, -⟩ := hB.qa
217  obtain ⟨ba, hba, -⟩ := hB.ba
218  obtain ⟨t1, t2, t3, t4, t5, t6, t7⟩ := endHeap_tables (ds := ds) hB hz x
219  have key : (endHeap h r ds z d).live x ↔
220      ((endHeap h r ds z d).bytes x ≠ none ∨ (endHeap h r ds z d).words x ≠ none ∨ (h.streams x).isSome ∨
221        h.gzheaders x ≠ none ∨ (endHeap h r ds z d).dstates x ≠ none ∨ h.istates x ≠ none ∨ (h.gzstates x).isSome) := by
222    unfold Heap.live
223    rw [t6, t7, ← Option.isSome_iff_ne_none (o := (endHeap h r ds z d).streams x), t4,
224      ← Option.isSome_iff_ne_none (o := (endHeap h r ds z d).gzstates x), t5]
225  rw [key]
226  unfold Heap.live
227  rw [t1, t2, t3]
228  by_cases hx : x = ds ∨ x = w ∨ x = p ∨ x = q ∨ x = b
229  · simp only [hx, not_true_eq_false, and_false, iff_false]
230    rcases hx with rfl | rfl | rfl | rfl | rfl
231    · obtain ⟨e1, e2, e3, e4, e5, e6⟩ := hU.dstates_only hs
232      simp [e1, e2, e3, e4, e5, e6]
233    · obtain ⟨e1, e2, e3, e4, e5, e6⟩ := hU.bytes_only hwa
234      simp [e1, e2, e3, e4, e5, e6, Option.isSome_none]
235    · obtain ⟨e1, e2, e3, e4, e5, e6⟩ := hU.words_only hpa
236      simp [e1, e2, e3, e4, e5, e6, Option.isSome_none]
237    · obtain ⟨e1, e2, e3, e4, e5, e6⟩ := hU.words_only hqa
238      simp [e1, e2, e3, e4, e5, e6, Option.isSome_none]
239    · obtain ⟨e1, e2, e3, e4, e5, e6⟩ := hU.bytes_only hba
240      simp [e1, e2, e3, e4, e5, e6, Option.isSome_none]
241  · have hx1 : ¬ (x = w ∨ x = b) := fun e => hx (by rcases e with e | e <;> simp [e])
242    have hx2 : ¬ (x = p ∨ x = q) := fun e => hx (by rcases e with e | e <;> simp [e])
243    have hx3 : ¬ x = ds := fun e => hx (Or.inl e)
244    have hn : ¬ (x = w ∨ x = p ∨ x = q ∨ x = b) := fun e => hx (Or.inr e)
245    simp only [hx1, hx2, hx3, ite_false]
246    simp [hn, Option.isSome_iff_ne_none]
247
248theorem endHeap_uniq {h : Heap} {r : ZStreamRef} {ds : Nat} {z : ZStream} {d : DeflateState} {w p q b : Nat}
249    (hB : DBlocks h d w p q b) (hU : Uniq h) (hz : r.get h = some z) : Uniq (endHeap h r ds z d) := by
250  intro x
251  obtain ⟨t1, t2, t3, t4, t5, t6, t7⟩ := endHeap_tables (ds := ds) hB hz x
252  have := hU x
253  have c1 : cnt ((endHeap h r ds z d).bytes x) ≤ cnt (h.bytes x) := by
254    rw [t1]; split <;> simp [cnt]
255  have c2 : cnt ((endHeap h r ds z d).words x) ≤ cnt (h.words x) := by
256    rw [t2]; split <;> simp [cnt]
257  have c3 : cnt ((endHeap h r ds z d).dstates x) ≤ cnt (h.dstates x) := by
258    rw [t3]; split <;> simp [cnt]
259  have c4 : cnt ((endHeap h r ds z d).streams x) = cnt (h.streams x) := by simp only [cnt, t4]
260  have c5 : cnt ((endHeap h r ds z d).gzstates x) = cnt (h.gzstates x) := by simp only [cnt, t5]
261  rw [t6, t7]
262  omega
263
264/-- **deflateEnd, safety and specification.** On an initialised stream with the invariant and the default `zfree`, the
265call never faults. It returns `Z_DATA_ERROR` if the status was `BUSY_STATE` (the stream ended in the middle of a block)
266and `Z_OK` otherwise. It frees exactly the state record and its four buffers (`window`, `prev`, `head`, `pending_buf`) and
267sets `strm->state` to `NULL`: the live blocks afterwards are the old ones minus those five (no leak, no double
268free), every other block of every table is as before, and the heap is again `Uniq` and `Fresh`. (The blocks are named by
269`DBlocks`.) -/
270theorem deflateEnd_safe {h : Heap} {r : ZStreamRef} {ds : Nat} {z : ZStream} {d : DeflateState}
271    (hG : DGood h r ds z d) (hf : z.zfree = .fn "zcfree") :
272    ∃ w p q b, DBlocks h d w p q b ∧ ∃ h',
273      C.run (deflateEnd (some r)) h = .ok ((if d.status = BUSY_STATE then Z_DATA_ERROR else Z_OK), h') ∧
274      h' = endHeap h r ds z d ∧ r.get h' = some { z with state := none } ∧
275      h'.dstates ds = none ∧ h'.bytes w = none ∧ h'.bytes b = none ∧ h'.words p = none ∧ h'.words q = none ∧
276      (∀ x, x ≠ ds → h'.dstates x = h.dstates x) ∧ (∀ x, x ≠ w → x ≠ b → h'.bytes x = h.bytes x) ∧
277      (∀ x, x ≠ p → x ≠ q → h'.words x = h.words x) ∧ h'.ro = h.ro ∧ h'.gzheaders = h.gzheaders ∧
278      h'.istates = h.istates ∧ h'.nextBlk = h.nextBlk ∧ h'.nalloc = h.nalloc ∧
279      (∀ x, (∀ i, r = .tab i → x ≠ i) → h'.streams x = h.streams x) ∧
280      (∀ x, (∀ i, r = .in_gzstate_strm i → x ≠ i) → h'.gzstates x = h.gzstates x) ∧
281      Uniq h' ∧ Fresh h' ∧ (∀ S, h.Owns S → h'.Owns (fun x => S x ∧ ¬ DOwned d ds x)) := by
282  obtain ⟨w, p, q, b, hB⟩ := hG.inv.blocks
283  refine ⟨w, p, q, b, hB, _, ?_, rfl, ?_⟩
284  · have := deflateEnd_run hG.live hf hB
285    rw [C.run, this]
286    simp [BEq.beq]
287  have hU := hG.uniq
288  have hF := hG.fresh
289  obtain ⟨wa, hwa, -⟩ := hB.wa
290  obtain ⟨pa, hpa, -⟩ := hB.pa
291  obtain ⟨qa, hqa, -⟩ := hB.qa
292  obtain ⟨ba, hba, -⟩ := hB.ba
293  have hbw : b ≠ w := fun e => hB.wb e.symm
294  have hz := hG.live.hz
295  have hs := hG.live.hs
296  have hUni := endHeap_uniq (ds := ds) hB hU hz
297  have hLive := endHeap_live hB hU hz hs
298  have hnb : (endHeap h r ds z d).nextBlk = h.nextBlk := by rw [endHeap_eq hB]; simp
299  rw [endHeap_eq hB]
300  refine ⟨?_, by simp, by simp, by simp [hbw], by simp, by simp [hB.pq.symm], ?_, ?_, ?_, by simp, by simp, by simp, by simp,
301    by simp, ?_, ?_, ?_, ?_, ?_⟩
302  · rw [ZStreamRef.get_dstates, ZStreamRef.get_put, ZStreamRef.get_bw, hz]; rfl
303  · intro x hx; simp [upd_apply, hx]
304  · intro x h1 h2; simp [upd_apply, h1, h2]
305  · intro x h1 h2; simp [upd_apply, h1, h2]
306  · intro x hx; simp [ZStreamRef.put_streams r _ _ x hx]
307  · intro x hx; simp [ZStreamRef.put_gzstates r _ _ x hx]
308  · rw [← endHeap_eq hB]; exact hUni
309  · intro x hx hl
310    rw [← endHeap_eq hB] at hl
311    rw [← endHeap_eq hB] at hx
312    rw [hnb] at hx
313    exact hF x hx ((hLive x).1 hl).1
314  · intro S hO x
315    rw [← endHeap_eq hB, hLive x, hO x]
316    show _ ↔ S x ∧ ¬ DOwned d ds x
317    rw [DOwned_iff hB x]
318
319/-- **deflateEnd, refusal.** On a stream the check refuses (including `NULL`) the call returns `Z_STREAM_ERROR` and changes
320nothing (in particular nothing is freed). -/
321theorem deflateEnd_reject {h : Heap} {strm : ZStreamPtr} (hD : StreamDom h strm) (hN : ¬ DInitialised h strm) :
322    C.run (deflateEnd strm) h = .ok (Z_STREAM_ERROR, h) := by
323  unfold deflateEnd
324  exact check_refuse hD hN _ _
325
326end Zlib.Deflate.Proofs