LibcTables.lean

Lean source with line numbers. Follow a line number to locate a statement, or an import to read its dependency.

1import ZlibF.Runtime.Tables
2
3/-!
4# `malloc`, `free` and `memcpy` of every struct kind (GENERATED, do not edit)
5
6`allocK` and `freeK` are `malloc(sizeof(K))` and `free` through the default allocator, `copyK dst src` is the
7`memcpy` of a whole record. They model the C library (see `Libc.lean` and `docs/trusted-base.md`); the loads and
8stores of the records are in `Tables.lean`.
9-/
10
11namespace C
12
13/-- `malloc(sizeof(z_stream))` through the default allocator: a fresh live record with arbitrary integers and
14null pointers (a documented gap: C leaves them indeterminate, see `docs/trusted-base.md`), or null when the
15failure oracle says so. It is a fault (not a C behaviour) if the block number `nextBlk` is already in use:
16the heap is then not `Fresh`, and a theorem about allocation carries `Fresh`. -/
17def allocZStream : M ZStreamPtr := fun h =>
18  if h.allocOk h.nalloc then
19    if h.slotUsed h.nextBlk then .error (.ub "allocation: the block number is in use (the heap is not Fresh)")
20    else .ok (some (.tab h.nextBlk), { h with streams := upd h.streams h.nextBlk (some (ZStream.garbage (h.garbage h.nalloc))), nextBlk := h.nextBlk + 1, nalloc := h.nalloc + 1 })
21  else .ok (none, { h with nalloc := h.nalloc + 1 })
22
23/-- Alias of `allocZStream`. -/
24abbrev allocZStreamChk := allocZStream
25
26theorem allocZStream_some {h : Heap} (hok : h.allocOk h.nalloc = true)
27    (hs : h.slotUsed h.nextBlk = false := by fresh_slot) :
28    allocZStream h = .ok (some (.tab h.nextBlk), { h with streams := upd h.streams h.nextBlk (some (ZStream.garbage (h.garbage h.nalloc))), nextBlk := h.nextBlk + 1, nalloc := h.nalloc + 1 }) := by simp [allocZStream, hok, hs]
29
30theorem allocZStream_none {h : Heap} (hok : ¬ h.allocOk h.nalloc = true) :
31    allocZStream h = .ok (none, { h with nalloc := h.nalloc + 1 }) := by simp [allocZStream, hok]
32
33/-- `free(p)` for a `z_stream *`: a no-op for null; faults for a block that is not live (double free) and for a
34pointer that was not returned by the allocator. -/
35def freeZStream (p : ZStreamPtr) : M Unit := fun h =>
36  match p with
37  | none => .ok ((), h)
38  | some (.tab i) => match h.streams i with
39    | some _ => .ok ((), { h with streams := upd h.streams i none })
40    | none => .error (.ub "free of a freed or invalid pointer (z_stream)")
41  | some _ => .error (.ub "free of a pointer that was not allocated (z_stream)")
42
43theorem freeZStream_null {h : Heap} : freeZStream none h = .ok ((), h) := rfl
44
45/-- `*dst = *src` for two `z_stream *` (`zmemcpy(dst, src, sizeof *dst)`): a whole-record copy. Faults if either pointer
46is null, dangling or the destination read-only, and if both denote the same object (`memcpy` with overlapping
47ranges is undefined; the `z_stream` objects of the heap do not contain one another). -/
48def copyZStream (dst src : ZStreamPtr) : M Unit := fun h =>
49  match dst, src with
50  | some d, some s =>
51    if d = s then .error (.ub "memcpy of a z_stream onto itself (overlapping ranges)")
52    else (ldZStream (some s) >>= fun v => stZStream (some d) v) h
53  | _, _ => .error (.ub "null dereference (z_stream)")
54
55theorem freeZStream_tab {h : Heap} {i : Nat} {v : ZStream} (e : h.streams i = some v) :
56    freeZStream (some (.tab i)) h = .ok ((), { h with streams := upd h.streams i none }) := by simp [freeZStream, e]
57
58/-- `malloc(sizeof(gz_header))` through the default allocator: a fresh live record with arbitrary integers and
59null pointers (a documented gap: C leaves them indeterminate, see `docs/trusted-base.md`), or null when the
60failure oracle says so. It is a fault (not a C behaviour) if the block number `nextBlk` is already in use:
61the heap is then not `Fresh`, and a theorem about allocation carries `Fresh`. -/
62def allocGzHeader : M GzHeaderPtr := fun h =>
63  if h.allocOk h.nalloc then
64    if h.slotUsed h.nextBlk then .error (.ub "allocation: the block number is in use (the heap is not Fresh)")
65    else .ok (some (.tab h.nextBlk), { h with gzheaders := upd h.gzheaders h.nextBlk (some (GzHeader.garbage (h.garbage h.nalloc))), nextBlk := h.nextBlk + 1, nalloc := h.nalloc + 1 })
66  else .ok (none, { h with nalloc := h.nalloc + 1 })
67
68/-- Alias of `allocGzHeader`. -/
69abbrev allocGzHeaderChk := allocGzHeader
70
71theorem allocGzHeader_some {h : Heap} (hok : h.allocOk h.nalloc = true)
72    (hs : h.slotUsed h.nextBlk = false := by fresh_slot) :
73    allocGzHeader h = .ok (some (.tab h.nextBlk), { h with gzheaders := upd h.gzheaders h.nextBlk (some (GzHeader.garbage (h.garbage h.nalloc))), nextBlk := h.nextBlk + 1, nalloc := h.nalloc + 1 }) := by simp [allocGzHeader, hok, hs]
74
75theorem allocGzHeader_none {h : Heap} (hok : ¬ h.allocOk h.nalloc = true) :
76    allocGzHeader h = .ok (none, { h with nalloc := h.nalloc + 1 }) := by simp [allocGzHeader, hok]
77
78/-- `free(p)` for a `gz_header *`: a no-op for null; faults for a block that is not live (double free) and for a
79pointer that was not returned by the allocator. -/
80def freeGzHeader (p : GzHeaderPtr) : M Unit := fun h =>
81  match p with
82  | none => .ok ((), h)
83  | some (.tab i) => match h.gzheaders i with
84    | some _ => .ok ((), { h with gzheaders := upd h.gzheaders i none })
85    | none => .error (.ub "free of a freed or invalid pointer (gz_header)")
86
87theorem freeGzHeader_null {h : Heap} : freeGzHeader none h = .ok ((), h) := rfl
88
89/-- `*dst = *src` for two `gz_header *` (`zmemcpy(dst, src, sizeof *dst)`): a whole-record copy. Faults if either pointer
90is null, dangling or the destination read-only, and if both denote the same object (`memcpy` with overlapping
91ranges is undefined; the `gz_header` objects of the heap do not contain one another). -/
92def copyGzHeader (dst src : GzHeaderPtr) : M Unit := fun h =>
93  match dst, src with
94  | some d, some s =>
95    if d = s then .error (.ub "memcpy of a gz_header onto itself (overlapping ranges)")
96    else (ldGzHeader (some s) >>= fun v => stGzHeader (some d) v) h
97  | _, _ => .error (.ub "null dereference (gz_header)")
98
99theorem freeGzHeader_tab {h : Heap} {i : Nat} {v : GzHeader} (e : h.gzheaders i = some v) :
100    freeGzHeader (some (.tab i)) h = .ok ((), { h with gzheaders := upd h.gzheaders i none }) := by simp [freeGzHeader, e]
101
102/-- `malloc(sizeof(deflate_state))` through the default allocator: a fresh live record with arbitrary integers and
103null pointers (a documented gap: C leaves them indeterminate, see `docs/trusted-base.md`), or null when the
104failure oracle says so. It is a fault (not a C behaviour) if the block number `nextBlk` is already in use:
105the heap is then not `Fresh`, and a theorem about allocation carries `Fresh`. -/
106def allocDeflateState : M DeflateStatePtr := fun h =>
107  if h.allocOk h.nalloc then
108    if h.slotUsed h.nextBlk then .error (.ub "allocation: the block number is in use (the heap is not Fresh)")
109    else .ok (some (.tab h.nextBlk), { h with dstates := upd h.dstates h.nextBlk (some (DeflateState.garbage (h.garbage h.nalloc))), nextBlk := h.nextBlk + 1, nalloc := h.nalloc + 1 })
110  else .ok (none, { h with nalloc := h.nalloc + 1 })
111
112/-- Alias of `allocDeflateState`. -/
113abbrev allocDeflateStateChk := allocDeflateState
114
115theorem allocDeflateState_some {h : Heap} (hok : h.allocOk h.nalloc = true)
116    (hs : h.slotUsed h.nextBlk = false := by fresh_slot) :
117    allocDeflateState h = .ok (some (.tab h.nextBlk), { h with dstates := upd h.dstates h.nextBlk (some (DeflateState.garbage (h.garbage h.nalloc))), nextBlk := h.nextBlk + 1, nalloc := h.nalloc + 1 }) := by simp [allocDeflateState, hok, hs]
118
119theorem allocDeflateState_none {h : Heap} (hok : ¬ h.allocOk h.nalloc = true) :
120    allocDeflateState h = .ok (none, { h with nalloc := h.nalloc + 1 }) := by simp [allocDeflateState, hok]
121
122/-- `free(p)` for a `deflate_state *`: a no-op for null; faults for a block that is not live (double free) and for a
123pointer that was not returned by the allocator. -/
124def freeDeflateState (p : DeflateStatePtr) : M Unit := fun h =>
125  match p with
126  | none => .ok ((), h)
127  | some (.tab i) => match h.dstates i with
128    | some _ => .ok ((), { h with dstates := upd h.dstates i none })
129    | none => .error (.ub "free of a freed or invalid pointer (deflate_state)")
130
131theorem freeDeflateState_null {h : Heap} : freeDeflateState none h = .ok ((), h) := rfl
132
133/-- `*dst = *src` for two `deflate_state *` (`zmemcpy(dst, src, sizeof *dst)`): a whole-record copy. Faults if either pointer
134is null, dangling or the destination read-only, and if both denote the same object (`memcpy` with overlapping
135ranges is undefined; the `deflate_state` objects of the heap do not contain one another). -/
136def copyDeflateState (dst src : DeflateStatePtr) : M Unit := fun h =>
137  match dst, src with
138  | some d, some s =>
139    if d = s then .error (.ub "memcpy of a deflate_state onto itself (overlapping ranges)")
140    else (ldDeflateState (some s) >>= fun v => stDeflateState (some d) v) h
141  | _, _ => .error (.ub "null dereference (deflate_state)")
142
143theorem freeDeflateState_tab {h : Heap} {i : Nat} {v : DeflateState} (e : h.dstates i = some v) :
144    freeDeflateState (some (.tab i)) h = .ok ((), { h with dstates := upd h.dstates i none }) := by simp [freeDeflateState, e]
145
146/-- `malloc(sizeof(inflate_state))` through the default allocator: a fresh live record with arbitrary integers and
147null pointers (a documented gap: C leaves them indeterminate, see `docs/trusted-base.md`), or null when the
148failure oracle says so. It is a fault (not a C behaviour) if the block number `nextBlk` is already in use:
149the heap is then not `Fresh`, and a theorem about allocation carries `Fresh`. -/
150def allocInflateState : M InflateStatePtr := fun h =>
151  if h.allocOk h.nalloc then
152    if h.slotUsed h.nextBlk then .error (.ub "allocation: the block number is in use (the heap is not Fresh)")
153    else .ok (some (.tab h.nextBlk), { h with istates := upd h.istates h.nextBlk (some (InflateState.garbage (h.garbage h.nalloc))), nextBlk := h.nextBlk + 1, nalloc := h.nalloc + 1 })
154  else .ok (none, { h with nalloc := h.nalloc + 1 })
155
156/-- Alias of `allocInflateState`. -/
157abbrev allocInflateStateChk := allocInflateState
158
159theorem allocInflateState_some {h : Heap} (hok : h.allocOk h.nalloc = true)
160    (hs : h.slotUsed h.nextBlk = false := by fresh_slot) :
161    allocInflateState h = .ok (some (.tab h.nextBlk), { h with istates := upd h.istates h.nextBlk (some (InflateState.garbage (h.garbage h.nalloc))), nextBlk := h.nextBlk + 1, nalloc := h.nalloc + 1 }) := by simp [allocInflateState, hok, hs]
162
163theorem allocInflateState_none {h : Heap} (hok : ¬ h.allocOk h.nalloc = true) :
164    allocInflateState h = .ok (none, { h with nalloc := h.nalloc + 1 }) := by simp [allocInflateState, hok]
165
166/-- `free(p)` for a `inflate_state *`: a no-op for null; faults for a block that is not live (double free) and for a
167pointer that was not returned by the allocator. -/
168def freeInflateState (p : InflateStatePtr) : M Unit := fun h =>
169  match p with
170  | none => .ok ((), h)
171  | some (.tab i) => match h.istates i with
172    | some _ => .ok ((), { h with istates := upd h.istates i none })
173    | none => .error (.ub "free of a freed or invalid pointer (inflate_state)")
174
175theorem freeInflateState_null {h : Heap} : freeInflateState none h = .ok ((), h) := rfl
176
177/-- `*dst = *src` for two `inflate_state *` (`zmemcpy(dst, src, sizeof *dst)`): a whole-record copy. Faults if either pointer
178is null, dangling or the destination read-only, and if both denote the same object (`memcpy` with overlapping
179ranges is undefined; the `inflate_state` objects of the heap do not contain one another). -/
180def copyInflateState (dst src : InflateStatePtr) : M Unit := fun h =>
181  match dst, src with
182  | some d, some s =>
183    if d = s then .error (.ub "memcpy of a inflate_state onto itself (overlapping ranges)")
184    else (ldInflateState (some s) >>= fun v => stInflateState (some d) v) h
185  | _, _ => .error (.ub "null dereference (inflate_state)")
186
187theorem freeInflateState_tab {h : Heap} {i : Nat} {v : InflateState} (e : h.istates i = some v) :
188    freeInflateState (some (.tab i)) h = .ok ((), { h with istates := upd h.istates i none }) := by simp [freeInflateState, e]
189
190/-- `malloc(sizeof(gz_state))` through the default allocator: a fresh live record with arbitrary integers and
191null pointers (a documented gap: C leaves them indeterminate, see `docs/trusted-base.md`), or null when the
192failure oracle says so. It is a fault (not a C behaviour) if the block number `nextBlk` is already in use:
193the heap is then not `Fresh`, and a theorem about allocation carries `Fresh`. -/
194def allocGzState : M GzStatePtr := fun h =>
195  if h.allocOk h.nalloc then
196    if h.slotUsed h.nextBlk then .error (.ub "allocation: the block number is in use (the heap is not Fresh)")
197    else .ok (some (.tab h.nextBlk), { h with gzstates := upd h.gzstates h.nextBlk (some (GzState.garbage (h.garbage h.nalloc))), nextBlk := h.nextBlk + 1, nalloc := h.nalloc + 1 })
198  else .ok (none, { h with nalloc := h.nalloc + 1 })
199
200/-- Alias of `allocGzState`. -/
201abbrev allocGzStateChk := allocGzState
202
203theorem allocGzState_some {h : Heap} (hok : h.allocOk h.nalloc = true)
204    (hs : h.slotUsed h.nextBlk = false := by fresh_slot) :
205    allocGzState h = .ok (some (.tab h.nextBlk), { h with gzstates := upd h.gzstates h.nextBlk (some (GzState.garbage (h.garbage h.nalloc))), nextBlk := h.nextBlk + 1, nalloc := h.nalloc + 1 }) := by simp [allocGzState, hok, hs]
206
207theorem allocGzState_none {h : Heap} (hok : ¬ h.allocOk h.nalloc = true) :
208    allocGzState h = .ok (none, { h with nalloc := h.nalloc + 1 }) := by simp [allocGzState, hok]
209
210/-- `free(p)` for a `gz_state *`: a no-op for null; faults for a block that is not live (double free) and for a
211pointer that was not returned by the allocator. -/
212def freeGzState (p : GzStatePtr) : M Unit := fun h =>
213  match p with
214  | none => .ok ((), h)
215  | some (.tab i) => match h.gzstates i with
216    | some _ => .ok ((), { h with gzstates := upd h.gzstates i none })
217    | none => .error (.ub "free of a freed or invalid pointer (gz_state)")
218
219theorem freeGzState_null {h : Heap} : freeGzState none h = .ok ((), h) := rfl
220
221/-- `*dst = *src` for two `gz_state *` (`zmemcpy(dst, src, sizeof *dst)`): a whole-record copy. Faults if either pointer
222is null, dangling or the destination read-only, and if both denote the same object (`memcpy` with overlapping
223ranges is undefined; the `gz_state` objects of the heap do not contain one another). -/
224def copyGzState (dst src : GzStatePtr) : M Unit := fun h =>
225  match dst, src with
226  | some d, some s =>
227    if d = s then .error (.ub "memcpy of a gz_state onto itself (overlapping ranges)")
228    else (ldGzState (some s) >>= fun v => stGzState (some d) v) h
229  | _, _ => .error (.ub "null dereference (gz_state)")
230
231theorem freeGzState_tab {h : Heap} {i : Nat} {v : GzState} (e : h.gzstates i = some v) :
232    freeGzState (some (.tab i)) h = .ok ((), { h with gzstates := upd h.gzstates i none }) := by simp [freeGzState, e]
233
234end C