Libc.lean

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

1import ZlibF.Runtime.Ptr
2import ZlibF.Runtime.LibcTables
3
4/-!
5# Runtime: the C library
6
7Trusted base of every translation; see `docs/trusted-base.md`. Everything here models a function of the C library
8(or of the compiler's literal handling), not the C language: the language level (pointers, arithmetic, loops, the
9heap tables) is in `Space.lean`, `Monad.lean` and `Ptr.lean`. Each function says how it differs from the real one.
10
11| C library | Lean | Differs from the real function |
12| --- | --- | --- |
13| `memcpy`, `zmemcpy` | `Ptr.memcpy`, `memcpyB` (and `copyK` for a whole record, `LibcTables.lean`) | faults on NULL even for `n = 0`; on a read-only destination (for `n > 0`); on overlap; counts elements, not bytes |
14| `memmove` | `Ptr.memmove`, `memmoveB` | the same without the overlap fault |
15| `memset`, `zmemzero` | `Ptr.fill` (set `n` elements to a value), `Ptr.memset` (every byte of each element is `c`), `memsetB` | counts elements; `Ptr.fill` is `memset` only for bytes or the value 0 |
16| `strlen` | `strlenB` | faults when no NUL lies inside the block (the C reads past the object) |
17| `malloc` (through `ZALLOC`) | `allocB`, `allocW`, `allocK` per struct kind | the content is arbitrary integers and NULL pointers; success is decided by the oracle `Heap.allocOk`; faults if the heap is not `Fresh`; the size is a count of elements |
18| `free` | `freeB`, `freeW`, `freeK` | faults on a pointer that is not the start of a live block, on a freed block (double free), on a read-only block; NULL is a no-op |
19| string literal | `strLitRef` (the table `strTable`) | a static read-only array, the same pointer every time; a text outside the sources is a fault |
20| (test harness, not a C function) | `allocBytes`, `allocBytesRO` | put given bytes in a fresh block; take no allocation call |
21
22Not modelled: `calloc`, `realloc`, `printf` and the `gz` file calls other than through `GzFs` (the file system model of
23the translations, in `ZlibF/Zlib/gzfs.lean`), `errno`, `abs`, `strerror` (the translations write them themselves).
24-/
25
26namespace C
27
28/-! ## `memcpy`, `memmove`, `memset`, `strlen` on arrays -/
29
30/-- The value of an element of type `T` whose every byte is `c`: what `memset(p, c, n * sizeof(T))` stores in each
31element. -/
32class ByteRepeat (T : Type) where
33  ofByte : UInt8 → T
34
35instance : ByteRepeat UInt8 := ⟨id⟩
36instance : ByteRepeat UInt16 := ⟨fun c => (c.toUInt16 <<< 8) ||| c.toUInt16⟩
37instance : ByteRepeat UInt32 := ⟨fun c => let x := c.toUInt32; (x <<< 24) ||| (x <<< 16) ||| (x <<< 8) ||| x⟩
38instance : ByteRepeat UInt64 :=
39  ⟨fun c => let x := c.toUInt64; (x <<< 56) ||| (x <<< 48) ||| (x <<< 40) ||| (x <<< 32) ||| (x <<< 24) ||| (x <<< 16) ||| (x <<< 8) ||| x⟩
40instance : ByteRepeat Int8 := ⟨UInt8.toInt8⟩
41instance : ByteRepeat Int16 := ⟨fun c => ((c.toUInt16 <<< 8) ||| c.toUInt16).toInt16⟩
42instance : ByteRepeat Int32 := ⟨fun c => let x := c.toUInt32; ((x <<< 24) ||| (x <<< 16) ||| (x <<< 8) ||| x).toInt32⟩
43instance : ByteRepeat Int64 :=
44  ⟨fun c => let x := c.toUInt64; ((x <<< 56) ||| (x <<< 48) ||| (x <<< 40) ||| (x <<< 32) ||| (x <<< 24) ||| (x <<< 16) ||| (x <<< 8) ||| x).toInt64⟩
45
46section generic
47variable {R T : Type} [Space Heap R T]
48
49/-- `d` with `n` elements from `s` copied to it: element `doff + i` becomes element `soff + i` of `s`
50(read before any write, so it is also the result of `memmove`). -/
51def copyRange [Inhabited T] (d s : Array T) (doff soff n : Nat) : Array T :=
52  (List.range n).foldl (fun a i => a.set! (doff + i) s[soff + i]!) d
53
54/-- `d` with `n` elements from `off` on set to `v`. -/
55def fillRange (d : Array T) (off n : Nat) (v : T) : Array T :=
56  (List.range n).foldl (fun a i => a.set! (off + i) v) d
57
58/-- `memcpy(dst, src, n)` for `n` elements. Faults if either pointer is null (even for `n = 0`) or dangling, if a
59range leaves its array, if the destination is read-only and `n > 0`, or if the ranges overlap. -/
60def Ptr.memcpy [DecidableEq R] [Inhabited T] (dst src : Ptr R) (n : Nat) : M Unit := fun h =>
61  match dst, src with
62  | .ref rd od, .ref rs os =>
63    match Space.get h rd, Space.get h rs with
64    | some da, some sa =>
65      if Space.ro h rd && decide (n ≠ 0) then .error (.ub "memcpy into a read-only object")
66      else if od + n ≤ da.size ∧ os + n ≤ sa.size then
67        if rd ≠ rs ∨ od + n ≤ os ∨ os + n ≤ od then .ok ((), Space.modify h rd (fun da => copyRange da sa od os n))
68        else .error (.ub "memcpy with overlapping ranges")
69      else .error (.ub "memcpy outside its objects")
70    | _, _ => .error (.ub "memcpy through a dangling pointer")
71  | _, _ => .error (.ub "memcpy through a null pointer")
72
73/-- `memmove(dst, src, n)` for `n` elements: as `memcpy`, and the ranges may overlap (a read-only destination is a
74fault only when `n > 0`). -/
75def Ptr.memmove [DecidableEq R] [Inhabited T] (dst src : Ptr R) (n : Nat) : M Unit := fun h =>
76  match dst, src with
77  | .ref rd od, .ref rs os =>
78    match Space.get h rd, Space.get h rs with
79    | some da, some sa =>
80      if Space.ro h rd && decide (n ≠ 0) then .error (.ub "memmove into a read-only object")
81      else if od + n ≤ da.size ∧ os + n ≤ sa.size then .ok ((), Space.modify h rd (fun da => copyRange da sa od os n))
82      else .error (.ub "memmove outside its objects")
83    | _, _ => .error (.ub "memmove through a dangling pointer")
84  | _, _ => .error (.ub "memmove through a null pointer")
85
86/-- Set `n` elements to the value `v`. This is `memset(dst, c, n * sizeof(T))` only for a byte array, and for any
87element type when the value is zero (`zmemzero`). For a wider element type and another byte, use `Ptr.memset`, which
88stores the element whose every byte is `c`. Faults if `dst` is null or dangling, the range leaves the array, or the
89array is read-only and `n > 0`. -/
90def Ptr.fill (dst : Ptr R) (v : T) (n : Nat) : M Unit := fun h =>
91  match dst with
92  | .ref r off =>
93    match Space.get h r with
94    | none => .error (.ub "memset through a dangling pointer")
95    | some a =>
96      if Space.ro h r && decide (n ≠ 0) then .error (.ub "memset of a read-only object")
97      else if off + n ≤ a.size then .ok ((), Space.modify h r (fun a => fillRange a off n v))
98      else .error (.ub "memset outside its object")
99  | .null => .error (.ub "memset through a null pointer")
100
101/-- `memset(dst, c, n * sizeof(T))`: `n` elements, each with every byte equal to `c`. For a byte array it is `Ptr.fill`
102with `c`. The faults are those of `Ptr.fill`. -/
103def Ptr.memset [ByteRepeat T] (dst : Ptr R) (c : UInt8) (n : Nat) : M Unit :=
104  Ptr.fill dst (ByteRepeat.ofByte c) n
105
106/-! ### Rules -/
107
108theorem size_copyRange [Inhabited T] (d s : Array T) (doff soff n : Nat) :
109    (copyRange d s doff soff n).size = d.size := by
110  unfold copyRange
111  suffices ∀ (l : List Nat) (a : Array T), (l.foldl (fun a i => a.set! (doff + i) s[soff + i]!) a).size = a.size by
112    exact this _ _
113  intro l
114  induction l with
115  | nil => intro a; rfl
116  | cons i l ih => intro a; simp only [List.foldl]; rw [ih]; simp
117
118theorem size_fillRange (d : Array T) (off n : Nat) (v : T) : (fillRange d off n v).size = d.size := by
119  unfold fillRange
120  suffices ∀ (l : List Nat) (a : Array T), (l.foldl (fun a i => a.set! (off + i) v) a).size = a.size by
121    exact this _ _
122  intro l
123  induction l with
124  | nil => intro a; rfl
125  | cons i l ih => intro a; simp only [List.foldl]; rw [ih]; simp
126
127theorem Ptr.memcpy_ok [DecidableEq R] [Inhabited T] {h : Heap} {rd rs : R} {od os n : Nat} {da sa : Array T}
128    (hd : Space.get h rd = some da) (hs : Space.get h rs = some sa) (hro : Space.ro h rd = false)
129    (h1 : od + n ≤ da.size) (h2 : os + n ≤ sa.size) (hdis : rd ≠ rs ∨ od + n ≤ os ∨ os + n ≤ od) :
130    Ptr.memcpy (Ptr.ref rd od) (Ptr.ref rs os) n h = .ok ((), Space.put h rd (copyRange da sa od os n)) := by
131  simp [Ptr.memcpy, hd, hs, hro, h1, h2, hdis, Space.modify_eq _ _ _ _ hd]
132
133theorem Ptr.memmove_ok [DecidableEq R] [Inhabited T] {h : Heap} {rd rs : R} {od os n : Nat} {da sa : Array T}
134    (hd : Space.get h rd = some da) (hs : Space.get h rs = some sa) (hro : Space.ro h rd = false)
135    (h1 : od + n ≤ da.size) (h2 : os + n ≤ sa.size) :
136    Ptr.memmove (Ptr.ref rd od) (Ptr.ref rs os) n h = .ok ((), Space.put h rd (copyRange da sa od os n)) := by
137  simp [Ptr.memmove, hd, hs, hro, h1, h2, Space.modify_eq _ _ _ _ hd]
138
139theorem Ptr.fill_ok {h : Heap} {r : R} {a : Array T} {off n : Nat} {v : T}
140    (hg : Space.get h r = some a) (hro : Space.ro h r = false) (h1 : off + n ≤ a.size) :
141    Ptr.fill (Ptr.ref r off) v n h = .ok ((), Space.put h r (fillRange a off n v)) := by
142  simp [Ptr.fill, hg, hro, h1, Space.modify_eq _ _ _ _ hg]
143
144end generic
145
146/-- `memcpy(dst, src, n)` for byte pointers (`zmemcpy`). -/
147abbrev memcpyB (dst src : BPtr) (n : Nat) : M Unit := Ptr.memcpy dst src n
148/-- `memmove(dst, src, n)` for byte pointers. -/
149abbrev memmoveB (dst src : BPtr) (n : Nat) : M Unit := Ptr.memmove dst src n
150/-- `memset(dst, c, n)` for a byte pointer. -/
151abbrev memsetB (dst : BPtr) (c : UInt8) (n : Nat) : M Unit := Ptr.fill dst c n
152
153/-- `memcpy` between two different byte blocks, both writable-or-readable as needed: the destination block `nb` is
154writable, the ranges are inside the blocks. The result is the heap with the block `nb` replaced. -/
155theorem memcpyB_blk_ok {h : Heap} {nb no pb po n : Nat} {ob pbuf : Array UInt8}
156    (e1 : h.bytes nb = some ob) (e2 : h.bytes pb = some pbuf) (hro : h.ro nb = false) (hne : nb ≠ pb)
157    (h1 : no + n ≤ ob.size) (h2 : po + n ≤ pbuf.size) :
158    memcpyB (.ref (.blk nb) no) (.ref (.blk pb) po) n h =
159      .ok ((), { h with bytes := upd h.bytes nb (some (copyRange ob pbuf no po n)) }) :=
160  Ptr.memcpy_ok (rd := BRef.blk nb) (rs := BRef.blk pb) e1 e2 hro h1 h2 (Or.inl (fun hh => hne (BRef.blk.inj hh)))
161
162/-- The index of the first NUL byte of `a` at or after `i`. -/
163def strlenFrom (a : Array UInt8) (i : Nat) : Option Nat :=
164  if h : i < a.size then (if a[i] == 0 then some i else strlenFrom a (i + 1)) else none
165termination_by a.size - i
166
167/-- `strlen(p)`. Faults if `p` is null or dangling, or if no NUL byte follows inside the block (the C reads outside
168the object). -/
169def strlenB (p : BPtr) : M UInt64 := fun h =>
170  match p with
171  | .null => .error (.ub "strlen of a null pointer")
172  | .ref r off =>
173    match Space.get h r with
174    | none => .error (.ub "strlen through a dangling pointer")
175    | some a =>
176      match strlenFrom a off with
177      | some j => .ok (UInt64.ofNat (j - off), h)
178      | none => .error (.ub "strlen: no terminating NUL inside the object")
179
180theorem strlenFrom_eq (a : Array UInt8) (k : Nat) (hz : a[k]? = some 0) :
181    ∀ d i, i + d = k → (∀ j, i ≤ j → j < k → a[j]? ≠ some 0) → strlenFrom a i = some k := by
182  intro d
183  induction d with
184  | zero =>
185    intro i hi _
186    subst hi
187    have hlt : i < a.size := by
188      rcases Nat.lt_or_ge i a.size with hh | hh
189      · exact hh
190      · simp [Array.getElem?_eq_none hh] at hz
191    rw [strlenFrom]
192    simp [hlt]
193    have : a[i] = 0 := by simpa [hlt] using hz
194    simp [this]
195  | succ d ih =>
196    intro i hi hn
197    have hlt : i < a.size := by
198      rcases Nat.lt_or_ge i a.size with hh | hh
199      · exact hh
200      · simp [Array.getElem?_eq_none (by omega : a.size ≤ k)] at hz
201    have hne : a[i] ≠ 0 := by
202      intro h0
203      exact hn i (Nat.le_refl _) (by omega) (by simp [hlt, h0])
204    rw [strlenFrom]
205    simp only [hlt, dite_true]
206    have : (a[i] == 0) = false := by simpa using hne
207    simp only [this, Bool.false_eq_true, ite_false]
208    exact ih (i + 1) (by omega) (fun j hj hjk => hn j (by omega) hjk)
209
210theorem strlenB_ok {h : Heap} {r : BRef} {a : Array UInt8} {off k : Nat}
211    (hg : Space.get h r = some a) (hk : off ≤ k) (hz : a[k]? = some 0)
212    (hn : ∀ j, off ≤ j → j < k → a[j]? ≠ some 0) :
213    OkOn h (strlenB (Ptr.ref r off)) (UInt64.ofNat (k - off)) := by
214  unfold OkOn strlenB
215  simp [hg, strlenFrom_eq a k hz (k - off) off (by omega) hn]
216
217/-! ## `malloc`, `free` and string literals
218
219`malloc` and `free` through the default allocator, for byte blocks and for blocks of 16-bit words (the struct kinds
220have their own in `LibcTables.lean`). All kinds share one counter of block numbers: a new object takes `nextBlk`, which
221only grows, so a freed block number is never reused and a use after free is always detected. Whether the call succeeds
222is decided by the oracle `allocOk`; the content of the new memory is arbitrary (`garbage`), so a theorem holds for every
223content.
224
225**Block numbers.** `allocB`, `allocW`, `allocBytes`, `allocBytesRO` (and `allocK` for each struct kind) fault if the
226block number `nextBlk` is already in use (`Heap.slotUsed`). The fault is not a C behaviour: it says that the heap is not
227`Fresh`. A theorem about code that allocates carries `Fresh`; the rules (`allocB_some`, ...) take the hypothesis
228`h.slotUsed h.nextBlk = false`, which the tactic `fresh_slot` finds from `Fresh h` in the context. The names with the
229suffix `Chk` are aliases of the plain ones. -/
230
231
232/-- `malloc(n)` for `n` bytes: a fresh writable block with arbitrary content, or `NULL` when the failure oracle
233says so. -/
234def allocB (n : Nat) : M BPtr := fun h =>
235  if h.allocOk h.nalloc then
236    if h.slotUsed h.nextBlk then .error (.ub "allocation: the block number is in use (the heap is not Fresh)")
237    else
238      .ok (.ref (.blk h.nextBlk) 0,
239        { h with bytes := upd h.bytes h.nextBlk (some (Array.ofFn (n := n) fun i => Junk.of (h.garbage h.nalloc i.val))),
240                 ro := upd h.ro h.nextBlk false, nextBlk := h.nextBlk + 1, nalloc := h.nalloc + 1 })
241  else .ok (.null, { h with nalloc := h.nalloc + 1 })
242
243/-- For harnesses and tests, not a C operation: put the bytes `a` into a fresh writable block. It takes no allocation
244call of the oracle. -/
245def allocBytes (a : Array UInt8) : M BPtr := fun h =>
246  if h.slotUsed h.nextBlk then .error (.ub "allocation: the block number is in use (the heap is not Fresh)")
247  else
248    .ok (.ref (.blk h.nextBlk) 0,
249      { h with bytes := upd h.bytes h.nextBlk (some a), ro := upd h.ro h.nextBlk false, nextBlk := h.nextBlk + 1 })
250
251/-- For harnesses and tests, not a C operation: put the bytes `a` into a fresh read-only block (a string literal, a
252`const` buffer). -/
253def allocBytesRO (a : Array UInt8) : M BPtr := fun h =>
254  if h.slotUsed h.nextBlk then .error (.ub "allocation: the block number is in use (the heap is not Fresh)")
255  else
256    .ok (.ref (.blk h.nextBlk) 0,
257      { h with bytes := upd h.bytes h.nextBlk (some a), ro := upd h.ro h.nextBlk true, nextBlk := h.nextBlk + 1 })
258
259/-- `malloc(2 * n)` for `n` 16-bit words, as `allocB`. -/
260def allocW (n : Nat) : M WPtr := fun h =>
261  if h.allocOk h.nalloc then
262    if h.slotUsed h.nextBlk then .error (.ub "allocation: the block number is in use (the heap is not Fresh)")
263    else
264      .ok (.ref (.blk h.nextBlk) 0,
265        { h with words := upd h.words h.nextBlk (some (Array.ofFn (n := n) fun i => Junk.of (h.garbage h.nalloc i.val))),
266                 nextBlk := h.nextBlk + 1, nalloc := h.nalloc + 1 })
267  else .ok (.null, { h with nalloc := h.nalloc + 1 })
268
269/-- `free(p)` for a byte block: a no-op for `NULL`. Faults for a block that was freed already (double free), for a
270read-only block, and for a pointer that is not the start of an allocated block. -/
271def freeB (p : BPtr) : M Unit := fun h =>
272  match p with
273  | .null => .ok ((), h)
274  | .ref (.blk b) 0 =>
275    match h.bytes b with
276    | some _ => if h.ro b then .error (.ub "free of a read-only block") else .ok ((), { h with bytes := upd h.bytes b none })
277    | none => .error (.ub "free of a freed or invalid pointer")
278  | _ => .error (.ub "free of a pointer that is not the start of an allocated block")
279
280/-- `free(p)` for a block of 16-bit words, as `freeB`. -/
281def freeW (p : WPtr) : M Unit := fun h =>
282  match p with
283  | .null => .ok ((), h)
284  | .ref (.blk b) 0 =>
285    match h.words b with
286    | some _ => .ok ((), { h with words := upd h.words b none })
287    | none => .error (.ub "free of a freed or invalid pointer")
288  | _ => .error (.ub "free of a pointer that is not the start of an allocated block")
289
290/-- Alias of `allocB`. -/
291abbrev allocBChk := allocB
292/-- Alias of `allocW`. -/
293abbrev allocWChk := allocW
294/-- Alias of `allocBytes`. -/
295abbrev allocBytesChk := allocBytes
296/-- Alias of `allocBytesRO`. -/
297abbrev allocBytesROChk := allocBytesRO
298
299/-! ### String literals
300
301A literal is a static, read-only object that is never freed and never consumes an allocation (`BRef.str`, `strTable`
302in `Schema.lean`). `strLitRef s` is the pointer to the literal `s`: the same pointer every time, no change to the heap.
303The set of literals is closed (the string literals of the library sources); any other text is a fault. -/
304
305/-- The number of the literal `s` in `strTable`, if it is one. -/
306def strIndex (s : String) : Option Nat := strTable.findIdx? (fun t => t == s)
307
308/-- A string literal of the C sources: a pointer to its first byte. It reads the heap and does not change it; it
309faults if `s` is not a literal of the sources (`strTable`). -/
310def strLitRef (s : String) : M BPtr := fun h =>
311  match strIndex s with
312  | some i => .ok (.ref (.str i) 0, h)
313  | none => .error (.ub "string literal not in the table of literals of the sources")
314
315theorem strLitRef_of_index {h : Heap} {s : String} {i : Nat} (hi : strIndex s = some i) :
316    strLitRef s h = .ok (.ref (.str i) 0, h) := by
317  simp [strLitRef, hi]
318
319theorem strIndex_get {s : String} {i : Nat} (hi : strIndex s = some i) : strTable[i]? = some s := by
320  unfold strIndex at hi
321  rw [Array.findIdx?_eq_some_iff_getElem] at hi
322  obtain ⟨h1, h2, -⟩ := hi
323  rw [Array.getElem?_eq_getElem h1]
324  simpa using h2
325
326/-- Every text of `strTable` is found. -/
327theorem strIndex_of_mem {s : String} (hs : s ∈ strTable) : ∃ i, strIndex s = some i := by
328  cases hx : strIndex s with
329  | some i => exact ⟨i, rfl⟩
330  | none =>
331    exfalso
332    unfold strIndex at hx
333    rw [Array.findIdx?_eq_none_iff] at hx
334    have := hx s hs
335    simp at this
336
337/-- A literal of the sources: the pointer is the start of the read-only static array of its text and a NUL, and the
338heap is unchanged (no block is allocated). -/
339theorem strLitRef_of_mem {h : Heap} {s : String} (hs : s ∈ strTable) :
340    ∃ i, strLitRef s h = .ok (.ref (.str i) 0, h) ∧ strTable[i]? = some s := by
341  obtain ⟨i, hi⟩ := strIndex_of_mem hs
342  exact ⟨i, strLitRef_of_index hi, strIndex_get hi⟩
343
344/-- The bytes behind the pointer of a literal: the text and a NUL. -/
345theorem strLitRef_get {h : Heap} {s : String} {i : Nat} (hi : strIndex s = some i) :
346    Space.get h (BRef.str i) = some (strBytes s) := by
347  simp [strIndex_get hi]
348
349/-- A literal is read-only. -/
350theorem strLitRef_ro (h : Heap) (i : Nat) : Space.ro h (BRef.str i) = true := rfl
351
352/-! ### Rules -/
353
354theorem allocB_some {h : Heap} (n : Nat) (hok : h.allocOk h.nalloc = true)
355    (hs : h.slotUsed h.nextBlk = false := by fresh_slot) :
356    allocB n h = .ok (.ref (.blk h.nextBlk) 0,
357      { h with bytes := upd h.bytes h.nextBlk (some (Array.ofFn (n := n) fun i => Junk.of (h.garbage h.nalloc i.val))),
358               ro := upd h.ro h.nextBlk false, nextBlk := h.nextBlk + 1, nalloc := h.nalloc + 1 }) := by
359  simp [allocB, hok, hs]
360
361theorem allocBytesRO_ok {h : Heap} (a : Array UInt8) (hs : h.slotUsed h.nextBlk = false := by fresh_slot) :
362    allocBytesRO a h = .ok (.ref (.blk h.nextBlk) 0,
363      { h with bytes := upd h.bytes h.nextBlk (some a), ro := upd h.ro h.nextBlk true, nextBlk := h.nextBlk + 1 }) := by
364  simp [allocBytesRO, hs]
365
366theorem allocB_none {h : Heap} (n : Nat) (hok : ¬ h.allocOk h.nalloc = true) :
367    allocB n h = .ok (.null, { h with nalloc := h.nalloc + 1 }) := by
368  simp [allocB, hok]
369
370theorem allocW_some {h : Heap} (n : Nat) (hok : h.allocOk h.nalloc = true)
371    (hs : h.slotUsed h.nextBlk = false := by fresh_slot) :
372    allocW n h = .ok (.ref (.blk h.nextBlk) 0,
373      { h with words := upd h.words h.nextBlk (some (Array.ofFn (n := n) fun i => Junk.of (h.garbage h.nalloc i.val))),
374               nextBlk := h.nextBlk + 1, nalloc := h.nalloc + 1 }) := by
375  simp [allocW, hok, hs]
376
377theorem allocW_none {h : Heap} (n : Nat) (hok : ¬ h.allocOk h.nalloc = true) :
378    allocW n h = .ok (.null, { h with nalloc := h.nalloc + 1 }) := by
379  simp [allocW, hok]
380
381theorem freeB_null {h : Heap} : freeB .null h = .ok ((), h) := rfl
382
383theorem freeB_ok {h : Heap} {b : Nat} {a : Array UInt8} (hb : h.bytes b = some a) (hro : h.ro b = false) :
384    freeB (.ref (.blk b) 0) h = .ok ((), { h with bytes := upd h.bytes b none }) := by
385  simp [freeB, hb, hro]
386
387theorem freeB_freed {h : Heap} {b : Nat} (hb : h.bytes b = none) :
388    freeB (.ref (.blk b) 0) h = .error (.ub "free of a freed or invalid pointer") := by
389  simp [freeB, hb]
390
391theorem freeW_ok {h : Heap} {b : Nat} {a : Array UInt16} (hb : h.words b = some a) :
392    freeW (.ref (.blk b) 0) h = .ok ((), { h with words := upd h.words b none }) := by
393  simp [freeW, hb]
394
395/-! ### Faults and ownership
396
397A freed block is never reused, so a use after free and a double free are faults. `Owns` (see `Schema.lean`) says which
398blocks are live: the two lemmas below show how `allocB` and `freeB` change it, which is what a leak statement is built
399from. -/
400
401/-- A use after free is a fault: a read through a pointer into a block that was freed. -/
402theorem load_after_free {h : Heap} {b off : Nat} {a : Array UInt8} (hb : h.bytes b = some a) (hro : h.ro b = false) :
403    (freeB (.ref (.blk b) 0) >>= fun _ => load8 (.ref (.blk b) off)) h = .error (.ub "read through a dangling pointer") := by
404  rw [bind_app, freeB_ok hb hro]
405  simp [load8, Ptr.load]
406
407/-- A double free is a fault. -/
408theorem free_twice {h : Heap} {b : Nat} {a : Array UInt8} (hb : h.bytes b = some a) (hro : h.ro b = false) :
409    (freeB (.ref (.blk b) 0) >>= fun _ => freeB (.ref (.blk b) 0)) h = .error (.ub "free of a freed or invalid pointer") := by
410  rw [bind_app, freeB_ok hb hro]
411  simp [freeB]
412
413/-- A successful `allocB` adds exactly the new block to the live blocks. -/
414theorem allocB_owns {h : Heap} (n : Nat) {S : Nat → Prop} (hok : h.allocOk h.nalloc = true) (hO : h.Owns S)
415    (hs : h.slotUsed h.nextBlk = false := by fresh_slot) :
416    ∃ h', allocB n h = .ok (.ref (.blk h.nextBlk) 0, h') ∧ h'.Owns (fun b => S b ∨ b = h.nextBlk) := by
417  refine ⟨_, allocB_some n hok hs, ?_⟩
418  intro b
419  by_cases hb : b = h.nextBlk
420  · subst hb; simp [Heap.live]
421  · have := hO b
422    simp only [Heap.live] at this ⊢
423    simp [upd_ne _ _ _ _ hb, hb, this]
424
425/-- `free` of a byte block that no other table holds removes exactly that block from the live blocks. -/
426theorem freeB_owns {h : Heap} {b : Nat} {a : Array UInt8} {S : Nat → Prop} (hb : h.bytes b = some a)
427    (hro : h.ro b = false)
428    (hother : h.words b = none ∧ h.streams b = none ∧ h.gzheaders b = none ∧ h.dstates b = none ∧
429      h.istates b = none ∧ h.gzstates b = none)
430    (hO : h.Owns S) :
431    ∃ h', freeB (.ref (.blk b) 0) h = .ok ((), h') ∧ h'.Owns (fun x => S x ∧ x ≠ b) := by
432  refine ⟨_, freeB_ok hb hro, ?_⟩
433  intro x
434  by_cases hx : x = b
435  · subst hx
436    obtain ⟨e1, e2, e3, e4, e5, e6⟩ := hother
437    simp [Heap.live, e1, e2, e3, e4, e5, e6]
438  · have := hO x
439    simp only [Heap.live] at this ⊢
440    simp [upd_ne _ _ _ _ hx, hx, this]
441
442end C