zutil.c.lean

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

1import ZlibF.Zlib.«zutil.c»
2
3/-!
4# zutil.c: specification, safety and correctness
5
6Statements of `docs/proof/zutil.md`. Every function of the translation (`zError`, `zlibVersion`,
7`zlibCompileFlags`, `zcalloc`, `zcfree`) has a `_safe` theorem (no fault, on every input `zutil.h` and `zlib.h`
8allow, with the frame, ownership and `Fresh` facts the callers need) and a `_correct` theorem (the value, against
9the specification in `Zlib.Zutil.Spec`, which does not mention the translation).
10
11`zmemcpy`, `zmemzero` and `zmemcmp` are not compiled in the default build (`HAVE_MEMCPY`): the macros of
12`zutil.h` expand to `memcpy`, `memset`, `memcmp`, so there is no translation of them here. The behaviour of the
13two the runtime provides is in `Ptr.memcpy_ok` and `Ptr.fill_ok`.
14
15String literals: a literal is a static read-only array (`BRef.str i`, see `zutil.c.lean`). Evaluating one does not
16change the heap, so the ownership statements say that the live blocks are the same as before.
17-/
18
19namespace Zlib.Zutil.Spec
20open C
21
22/-- The message of `z_errmsg` for a return code: `Z_NEED_DICT` (2) to `Z_VERSION_ERROR` (-6); every other code,
23and `Z_OK`, gives the empty string. -/
24def errText : Int → String
25  | 2 => "need dictionary"
26  | 1 => "stream end"
27  | 0 => ""
28  | -1 => "file error"
29  | -2 => "stream error"
30  | -3 => "data error"
31  | -4 => "insufficient memory"
32  | -5 => "buffer error"
33  | -6 => "incompatible version"
34  | _ => ""
35
36/-- The two-bit code of `zlibCompileFlags` for a type size in bytes (2: 0, 4: 1, 8: 2, otherwise 3). -/
37def sizeCode (n : Nat) : Nat := if n = 2 then 0 else if n = 4 then 1 else if n = 8 then 2 else 3
38
39/-- Bits 0..7 of `zlibCompileFlags`: the sizes of `uInt`, `uLong`, `voidpf`, `z_off_t`, two bits each. -/
40def compileFlags (uInt uLong voidpf zoff : Nat) : Nat :=
41  sizeCode uInt + 4 * sizeCode uLong + 16 * sizeCode voidpf + 64 * sizeCode zoff
42
43/-- The NUL-terminated string `s` is stored at the start of the read-only static array that `p` points to (a string
44literal: it is in no table of the heap and is always live). -/
45def CString (h : Heap) (p : BPtr) (s : String) : Prop :=
46  ∃ i, p = .ref (.str i) 0 ∧ Space.get h (BRef.str i) = some (s.toUTF8.data.push 0) ∧ Space.ro h (BRef.str i) = true
47
48end Zlib.Zutil.Spec
49
50namespace Zlib.Zutil.Proofs
51open C Zlib.Zutil Zlib.Zutil.Spec
52
53/-- The heap after `strLit s`: the same heap (a literal is static). -/
54def litHeap (h : Heap) (_s : String) : Heap := h
55
56/-- What evaluating a literal leaves of the heap: all of it. -/
57def LitFrame (h h' : Heap) : Prop := h' = h
58
59/-- `s` is a string literal of the sources. -/
60def IsLit (s : String) : Prop := s ∈ strTable
61
62theorem strLit_run (h : Heap) (s : String) (hs : IsLit s) :
63    ∃ i, strLit s h = .ok (.ref (.str i) 0, litHeap h s) ∧ strTable[i]? = some s := by
64  unfold strLit
65  exact strLitRef_of_mem hs
66
67theorem litHeap_cstring (h : Heap) (s : String) (i : Nat) (hi : strTable[i]? = some s) :
68    CString (litHeap h s) (.ref (.str i) 0) s :=
69  ⟨i, rfl, by simp [litHeap, hi, strBytes], rfl⟩
70
71theorem litHeap_frame (h : Heap) (s : String) : LitFrame h (litHeap h s) := rfl
72
73set_option maxRecDepth 100000 in
74theorem errText_lit (k : Int) : IsLit (errText k) := by
75  unfold IsLit errText
76  rw [Array.mem_def]
77  split <;> decide +kernel
78
79set_option maxRecDepth 100000 in
80theorem version_lit : IsLit ZLIB_VERSION := by
81  unfold IsLit ZLIB_VERSION
82  rw [Array.mem_def]
83  decide +kernel
84
85/-! ### zError -/
86
87theorem zError_eval (err : Int32) :
88    zError err = strLit (errText err.toInt) := by
89  funext h
90  by_cases hr : err < -6 || err > 2
91  · have h1 : err.toInt < -6 ∨ 2 < err.toInt := by
92      simp only [Bool.or_eq_true, decide_eq_true_eq] at hr
93      rcases hr with hr | hr
94      · left; have := Int32.lt_iff_toInt_lt.mp hr; simpa using this
95      · right; have := Int32.lt_iff_toInt_lt.mp hr; simpa using this
96    have : errText err.toInt = "" := by
97      unfold errText
98      split <;> first | omega | rfl
99    rw [this]
100    simp [zError, hr, z_errmsg, strLit]
101  · have h1 : -6 ≤ err.toInt ∧ err.toInt ≤ 2 := by
102      simp only [Bool.or_eq_true, decide_eq_true_eq, not_or, Int32.not_lt] at hr
103      have a := Int32.le_iff_toInt_le.mp hr.1
104      have b := Int32.le_iff_toInt_le.mp hr.2
105      simpa using And.intro a b
106    obtain ⟨k, hk1, hk2, rfl⟩ : ∃ k : Int, -6 ≤ k ∧ k ≤ 2 ∧ err = Int32.ofInt k :=
107      ⟨err.toInt, h1.1, h1.2, (Int32.ofInt_toInt err).symm⟩
108    rcases (by omega : k = -6 ∨ k = -5 ∨ k = -4 ∨ k = -3 ∨ k = -2 ∨ k = -1 ∨ k = 0 ∨ k = 1 ∨ k = 2) with
109      rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl | rfl <;> rfl
110
111/-- **zError, safety.** For every `int` argument (no restriction: the index is always in `0..9`), `zError` runs
112without undefined behaviour. It returns a string literal and changes nothing, in particular allocates nothing. -/
113theorem zError_safe (h : Heap) (err : Int32) :
114    ∃ p h', C.run (zError err) h = .ok (p, h') ∧ LitFrame h h' := by
115  obtain ⟨i, hr, -⟩ := strLit_run h (errText err.toInt) (errText_lit _)
116  exact ⟨_, _, by rw [C.run, zError_eval, hr], litHeap_frame h _⟩
117
118/-- **zError, correctness.** For every `int` `err`, `zError err` returns a pointer to the NUL-terminated message of
119`z_errmsg` for the code (`Spec.errText`): the zlib texts for `2` down to `-6`, the empty string otherwise. The
120message is a static read-only literal and the heap is unchanged. -/
121theorem zError_correct (h : Heap) (err : Int32) :
122    ∃ i h', C.run (zError err) h = .ok (.ref (.str i) 0, h') ∧
123      CString h' (.ref (.str i) 0) (errText err.toInt) ∧ h' = litHeap h (errText err.toInt) := by
124  obtain ⟨i, hr, hi⟩ := strLit_run h (errText err.toInt) (errText_lit _)
125  exact ⟨i, _, by rw [C.run, zError_eval, hr], litHeap_cstring h _ i hi, rfl⟩
126
127/-! ### zlibVersion -/
128
129/-- **zlibVersion, safety.** `zlibVersion` never faults, on any heap; it returns a static literal and changes nothing. -/
130theorem zlibVersion_safe (h : Heap) :
131    ∃ p h', C.run zlibVersion h = .ok (p, h') ∧ LitFrame h h' := by
132  obtain ⟨i, hr, -⟩ := strLit_run h ZLIB_VERSION version_lit
133  exact ⟨_, _, hr, litHeap_frame h _⟩
134
135theorem strlen_lit (h : Heap) (s : String) (i : Nat) (hi : strTable[i]? = some s)
136    (hnz : ∀ x ∈ s.toUTF8.data.toList, x ≠ 0) :
137    OkOn h (strlenB (.ref (.str i) 0)) (UInt64.ofNat s.utf8ByteSize) := by
138  have hg : Space.get h (BRef.str i) = some (s.toUTF8.data.push 0) := by
139    simp [hi, strBytes]
140  have hsz : s.toUTF8.data.size = s.utf8ByteSize := by simp [String.toUTF8]
141  have := strlenB_ok (h := h) (r := BRef.str i) (off := 0)
142    (a := s.toUTF8.data.push 0) (k := s.utf8ByteSize) hg (Nat.zero_le _)
143    (by rw [Array.getElem?_push, hsz]; simp) (by
144      intro j _ hj
145      have hj' : j < s.toUTF8.data.size := by omega
146      have hne := hnz (s.toUTF8.data[j]) (by simp)
147      rw [Array.getElem?_push, ite_eq_right (by omega), Array.getElem?_eq_getElem hj']
148      simpa using hne)
149  simpa using this
150
151/-- **zlibVersion, correctness.** It returns a pointer to the NUL-terminated text `ZLIB_VERSION` (the release string
152of the verified source), and `strlen` of the result is the length of that text. -/
153theorem zlibVersion_correct (h : Heap) :
154    ∃ i h', C.run zlibVersion h = .ok (.ref (.str i) 0, h') ∧
155      CString h' (.ref (.str i) 0) ZLIB_VERSION ∧ h' = litHeap h ZLIB_VERSION ∧
156      OkOn h' (strlenB (.ref (.str i) 0)) (UInt64.ofNat ZLIB_VERSION.utf8ByteSize) := by
157  obtain ⟨i, hr, hi⟩ := strLit_run h ZLIB_VERSION version_lit
158  exact ⟨i, _, hr, litHeap_cstring h _ i hi, rfl, strlen_lit h _ i hi (by decide)⟩
159
160/-! ### zlibCompileFlags -/
161
162/-- **zlibCompileFlags, safety.** It never faults and leaves the heap unchanged. -/
163theorem zlibCompileFlags_safe (h : Heap) : ∃ r, C.run zlibCompileFlags h = .ok (r, h) := by
164  exact ⟨_, rfl⟩
165
166/-- **zlibCompileFlags, correctness.** On the default LP64 target (`uInt` 4, `uLong` 8, `voidpf` 8, `z_off_t` 8
167bytes) the result is `Spec.compileFlags 4 8 8 8 = 0xA9`: the four size fields are 1, 2, 2, 2 and no option bit
168(bits 8 and up: `ZLIB_DEBUG`, `ZLIB_WINAPI`, `BUILDFIXED`, ...) is set. -/
169theorem zlibCompileFlags_correct (h : Heap) :
170    ∃ r, C.run zlibCompileFlags h = .ok (r, h) ∧ r.toNat = compileFlags 4 8 8 8 ∧ r = 0xA9 ∧
171      r &&& 3 = 1 ∧ (r >>> 2) &&& 3 = 2 ∧ (r >>> 4) &&& 3 = 2 ∧ (r >>> 6) &&& 3 = 2 ∧ r >>> 8 = 0 := by
172  exact ⟨0xA9, rfl, by decide, rfl, by decide, by decide, by decide, by decide, by decide⟩
173
174/-! ### zcalloc -/
175
176/-- The heap after a successful `malloc` of `n` bytes, as `allocB_some` has it. -/
177def allocHeap (h : Heap) (n : Nat) : Heap :=
178  { h with bytes := upd h.bytes h.nextBlk (some (Array.ofFn (n := n) fun i => Junk.of (h.garbage h.nalloc i.val))),
179           ro := upd h.ro h.nextBlk false, nextBlk := h.nextBlk + 1, nalloc := h.nalloc + 1 }
180
181/-- What a heap that gained one fresh writable byte block shares with the one before. -/
182def AllocFrame (h h' : Heap) : Prop :=
183  (∀ S, h.Owns S → h'.Owns (fun b => S b ∨ b = h.nextBlk)) ∧ (Fresh h → Fresh h') ∧
184  h'.nextBlk = h.nextBlk + 1 ∧ h'.nalloc = h.nalloc + 1 ∧
185  (∀ b, b ≠ h.nextBlk → h'.bytes b = h.bytes b ∧ h'.ro b = h.ro b) ∧
186  h'.words = h.words ∧ h'.streams = h.streams ∧ h'.gzheaders = h.gzheaders ∧ h'.dstates = h.dstates ∧
187  h'.istates = h.istates ∧ h'.gzstates = h.gzstates ∧ h'.static = h.static ∧
188  h'.allocOk = h.allocOk ∧ h'.garbage = h.garbage
189
190theorem allocHeap_frame (h : Heap) (n : Nat) : AllocFrame h (allocHeap h n) := by
191  refine ⟨?_, ?_, rfl, rfl, ?_, rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl, rfl⟩
192  · intro S hO b
193    by_cases hb : b = h.nextBlk
194    · subst hb; simp [Heap.live, allocHeap]
195    · have := hO b
196      simp only [Heap.live, allocHeap] at this ⊢
197      simp [upd_ne _ _ _ _ hb, hb, this]
198  · intro hF
199    refine Fresh.mono hF (by simp [allocHeap]) ?_
200    intro x hx
201    have hx' : x ≠ h.nextBlk := by simp [allocHeap] at hx; omega
202    simp [allocHeap, upd_ne _ _ _ _ hx']
203  · intro b hb
204    simp [allocHeap, upd_ne _ _ _ _ hb]
205
206/-- The heap after a failed `malloc`: only the call counter moves. -/
207def failHeap (h : Heap) : Heap := { h with nalloc := h.nalloc + 1 }
208
209theorem zcalloc_ok_run (h : Heap) (op : BPtr) (items sz : UInt32) (hok : h.allocOk h.nalloc = true)
210    (hF : Fresh h) :
211    zcalloc op items sz h = .ok (.ref (.blk h.nextBlk) 0, allocHeap h (items * sz).toNat) := by
212  unfold zcalloc
213  exact allocB_some _ hok
214
215theorem zcalloc_fail_run (h : Heap) (op : BPtr) (items sz : UInt32) (hok : ¬ h.allocOk h.nalloc = true) :
216    zcalloc op items sz h = .ok (.null, failHeap h) := by
217  unfold zcalloc
218  exact allocB_none _ hok
219
220theorem failHeap_live (h : Heap) (b : Nat) : (failHeap h).live b ↔ h.live b := Iff.rfl
221
222theorem failHeap_fresh {h : Heap} (hF : Fresh h) : Fresh (failHeap h) := hF
223
224/-- **zcalloc, safety.** For every `opaque` argument, `items` and `size` (the product is taken modulo 2^32, as in C, and is
225defined for every `unsigned` pair), `zcalloc` runs without undefined behaviour. Either it returns `NULL` and only
226the allocation counter moves (nothing is allocated, nothing leaks), or it returns the start of a new writable byte
227block and adds exactly that block to the live blocks. -/
228theorem zcalloc_safe (h : Heap) (op : BPtr) (items sz : UInt32) (hF : Fresh h) :
229    ∃ p h', C.run (zcalloc op items sz) h = .ok (p, h') ∧
230      ((p = .null ∧ h' = failHeap h ∧ (∀ b, h'.live b ↔ h.live b) ∧ (Fresh h → Fresh h')) ∨
231       (p = .ref (.blk h.nextBlk) 0 ∧ h' = allocHeap h (items * sz).toNat ∧ AllocFrame h h' ∧
232         h'.ro h.nextBlk = false)) := by
233  by_cases hok : h.allocOk h.nalloc = true
234  · exact ⟨_, _, zcalloc_ok_run h op items sz hok hF,
235      Or.inr ⟨rfl, rfl, allocHeap_frame h _, by simp [allocHeap]⟩⟩
236  · exact ⟨_, _, zcalloc_fail_run h op items sz hok,
237      Or.inl ⟨rfl, rfl, failHeap_live h, failHeap_fresh⟩⟩
238
239/-- **zcalloc, correctness (allocation succeeds).** When the allocation oracle says yes, the result is the start of
240a new block; the block is writable; its size in bytes is `items * size` reduced modulo 2^32 (the `unsigned`
241product of the C); and its content is arbitrary (`malloc` does not clear: this is not `calloc`). -/
242theorem zcalloc_correct_some (h : Heap) (op : BPtr) (items sz : UInt32) (hok : h.allocOk h.nalloc = true)
243    (hF : Fresh h) :
244    ∃ h' a, C.run (zcalloc op items sz) h = .ok (.ref (.blk h.nextBlk) 0, h') ∧
245      h'.bytes h.nextBlk = some a ∧ h'.ro h.nextBlk = false ∧
246      a.size = items.toNat * sz.toNat % 2 ^ 32 ∧
247      (∀ i (hi : i < a.size), a[i] = Junk.of (h.garbage h.nalloc i)) ∧ AllocFrame h h' := by
248  refine ⟨_, Array.ofFn (n := (items * sz).toNat) fun i => Junk.of (h.garbage h.nalloc i.val),
249    zcalloc_ok_run h op items sz hok hF, by simp [allocHeap], by simp [allocHeap], ?_, ?_, allocHeap_frame h _⟩
250  · simp [allocHeap, UInt32.toNat_mul]
251  · intro i hi
252    simp [allocHeap]
253
254/-- **zcalloc, correctness without wrap.** If `items * size` fits in 32 bits (every call site of zlib, whose largest
255product is 131072: `docs/proof/zutil.md` section 1), the block has exactly `items * size` bytes. -/
256theorem zcalloc_correct_size (h : Heap) (op : BPtr) (items sz : UInt32) (hok : h.allocOk h.nalloc = true)
257    (hnw : items.toNat * sz.toNat < 2 ^ 32) (hF : Fresh h) :
258    ∃ h' a, C.run (zcalloc op items sz) h = .ok (.ref (.blk h.nextBlk) 0, h') ∧
259      h'.bytes h.nextBlk = some a ∧ a.size = items.toNat * sz.toNat := by
260  obtain ⟨h', a, hr, hb, -, hsz, -⟩ := zcalloc_correct_some h op items sz hok hF
261  exact ⟨h', a, hr, hb, by rw [hsz]; exact Nat.mod_eq_of_lt hnw⟩
262
263/-- **zcalloc, correctness (allocation fails).** When the oracle says no, the result is `NULL` and the heap changes
264only in the call counter. -/
265theorem zcalloc_correct_none (h : Heap) (op : BPtr) (items sz : UInt32) (hok : ¬ h.allocOk h.nalloc = true) :
266    C.run (zcalloc op items sz) h = .ok (.null, { h with nalloc := h.nalloc + 1 }) := by
267  exact zcalloc_fail_run h op items sz hok
268
269/-! ### zcfree -/
270
271/-- **zcfree, safety.** `ptr` is `NULL`, or the start of a live writable byte block (a block returned by `zcalloc`
272and not yet freed, `zlib.h`'s `free_func` contract). Then `zcfree` runs without undefined behaviour: for `NULL`
273the heap is unchanged, otherwise exactly that block is removed. `op` (the `opaque` argument) is ignored. -/
274theorem zcfree_safe (h : Heap) (op ptr : BPtr)
275    (hp : ptr = .null ∨ ∃ b a, ptr = .ref (.blk b) 0 ∧ h.bytes b = some a ∧ h.ro b = false) :
276    ∃ h', C.run (zcfree op ptr) h = .ok ((), h') ∧
277      ((ptr = .null ∧ h' = h) ∨ ∃ b, ptr = .ref (.blk b) 0 ∧ h' = { h with bytes := upd h.bytes b none }) := by
278  rcases hp with rfl | ⟨b, a, rfl, hb, hro⟩
279  · exact ⟨h, freeB_null, Or.inl ⟨rfl, rfl⟩⟩
280  · exact ⟨_, freeB_ok hb hro, Or.inr ⟨b, rfl, rfl⟩⟩
281
282/-- **zcfree, correctness (ownership).** Freeing a live writable byte block `b` that no other table holds removes
283exactly `b` from the live blocks; freeing `NULL` changes nothing. -/
284theorem zcfree_correct (h : Heap) (op : BPtr) (b : Nat) (a : Array UInt8) (S : Nat → Prop)
285    (hb : h.bytes b = some a) (hro : h.ro b = false)
286    (hother : h.words b = none ∧ h.streams b = none ∧ h.gzheaders b = none ∧ h.dstates b = none ∧
287      h.istates b = none ∧ h.gzstates b = none)
288    (hO : h.Owns S) :
289    ∃ h', C.run (zcfree op (.ref (.blk b) 0)) h = .ok ((), h') ∧ h'.Owns (fun x => S x ∧ x ≠ b) ∧
290      h'.bytes b = none ∧ (∀ x, x ≠ b → h'.bytes x = h.bytes x) := by
291  obtain ⟨h', hr, hO'⟩ := freeB_owns hb hro hother hO
292  refine ⟨h', hr, hO', ?_⟩
293  have : h' = { h with bytes := upd h.bytes b none } := by
294    have := freeB_ok hb hro
295    rw [hr] at this
296    simp only [Except.ok.injEq, Prod.mk.injEq, true_and] at this
297    exact this
298  subst this
299  exact ⟨by simp, fun x hx => by simp [upd_ne _ _ _ _ hx]⟩
300
301/-- `zcfree(NULL)` does nothing. -/
302theorem zcfree_correct_null (h : Heap) (op : BPtr) : C.run (zcfree op .null) h = .ok ((), h) := by
303  exact freeB_null
304
305/-! ### No leak: allocate, then free -/
306
307/-- **zcalloc then zcfree.** On a heap whose block numbers from `nextBlk` on are unused, `zcalloc` followed by
308`zcfree` of its result runs without undefined behaviour (also when the allocation fails: `zcfree(NULL)`) and the set
309of live blocks afterwards is the set before. -/
310theorem zcalloc_zcfree_no_leak (h : Heap) (op : BPtr) (items sz : UInt32) (hF : Fresh h) :
311    ∃ h', C.run (zcalloc op items sz >>= fun p => zcfree op p) h = .ok ((), h') ∧
312      ∀ b, h'.live b ↔ h.live b := by
313  rw [C.run]
314  by_cases hok : h.allocOk h.nalloc = true
315  · rw [bind_app, zcalloc_ok_run h op items sz hok hF]
316    have hb : (allocHeap h (items * sz).toNat).bytes h.nextBlk = some (Array.ofFn (n := (items * sz).toNat)
317        fun i => Junk.of (h.garbage h.nalloc i.val)) := by simp [allocHeap]
318    have hro : (allocHeap h (items * sz).toNat).ro h.nextBlk = false := by simp [allocHeap]
319    refine ⟨_, freeB_ok hb hro, ?_⟩
320    intro b
321    by_cases hbn : b = h.nextBlk
322    · subst hbn
323      have := Heap.not_live.mp (hF _ (Nat.le_refl _))
324      obtain ⟨e0, e1, e2, e3, e4, e5, e6⟩ := this
325      simp [Heap.live, allocHeap, e1, e2, e3, e4, e5, e6]
326      simpa [Heap.live, e0, e1, e2, e3, e4, e5, e6] using hF _ (Nat.le_refl _)
327    · simp [Heap.live, allocHeap, upd_ne _ _ _ _ hbn]
328  · rw [bind_app, zcalloc_fail_run h op items sz hok]
329    exact ⟨_, freeB_null, fun b => Iff.rfl⟩
330
331/-! ### Non-vacuity: concrete runs of the real functions -/
332
333/-- The hypotheses of the `zcalloc` and `zcfree` theorems hold together on a heap made by the real functions: on
334the empty heap `zcalloc` of 16 bytes (allocation succeeds) is run, its result satisfies the hypotheses of
335`zcfree_safe` and `zcfree_correct` (live writable block, owned by the one-block set), and `zcfree` frees it. -/
336example : ∃ h1 : Heap, C.run (zcalloc .null 1 16) Heap.empty = .ok (.ref (.blk 0) 0, h1) ∧
337    (∃ a, h1.bytes 0 = some a ∧ a.size = 16 ∧ h1.ro 0 = false) ∧
338    ∃ h2 : Heap, C.run (zcfree .null (.ref (.blk 0) 0)) h1 = .ok ((), h2) ∧ h2.Owns (fun _ => False) := by
339  obtain ⟨h1, a, hr, hb, hro, hsz, -, hO, -, -, -, -, hw, hs, hg, hd, hi, hz, -⟩ :=
340    zcalloc_correct_some Heap.empty .null 1 16 rfl Heap.empty_fresh
341  have hO0 : (Heap.empty).Owns (fun _ => False) := by
342    intro b; simp [Heap.live, Heap.empty]
343  have hO1 : h1.Owns (fun b => False ∨ b = 0) := hO _ hO0
344  obtain ⟨h2, hr2, hO2, -⟩ := zcfree_correct h1 .null 0 a _ hb hro
345    ⟨by rw [hw]; rfl, by rw [hs]; rfl, by rw [hg]; rfl, by rw [hd]; rfl, by rw [hi]; rfl, by rw [hz]; rfl⟩ hO1
346  refine ⟨h1, hr, ⟨a, hb, by simpa using hsz, hro⟩, h2, hr2, ?_⟩
347  intro b
348  have := hO2 b
349  simpa using this
350
351/-- `zError` on the empty heap for the code `Z_MEM_ERROR` (-4) returns the text "insufficient memory" in a
352read-only static literal and leaves the heap as it was (an instance of `zError_correct`). -/
353example : ∃ i, C.run (zError (-4)) Heap.empty = .ok (.ref (.str i) 0, Heap.empty) ∧
354    strTable[i]? = some "insufficient memory" ∧ Space.ro Heap.empty (BRef.str i) = true := by
355  obtain ⟨i, hr, hi⟩ := strLit_run Heap.empty (errText (-4 : Int32).toInt) (errText_lit _)
356  have e : errText (-4 : Int32).toInt = "insufficient memory" := rfl
357  rw [e] at hi
358  exact ⟨i, by rw [C.run, zError_eval, hr] <;> rfl, hi, rfl⟩
359
360end Zlib.Zutil.Proofs