Tables.lean

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

1import ZlibF.Runtime.Monad
2
3/-!
4# Load and store for every struct kind (GENERATED, do not edit)
5
6`ldK p` is `*p` for a pointer to a struct of kind `K`, `stK p v` is `*p = v` (a whole-record store; a field
7write is a load, a record update and a store). Every primitive faults on a null, dangling or read-only target, as
8the C is undefined there. `malloc`, `free` and the whole-record `memcpy` of each kind are in `LibcTables.lean`.
9-/
10
11namespace C
12
13/-- `*p` for a `z_stream *`: faults if `p` is null or does not point to a live object. -/
14def ldZStream (p : ZStreamPtr) : M ZStream := fun h =>
15  match p with
16  | none => .error (.ub "null dereference (z_stream)")
17  | some r => match r.get h with
18    | some v => .ok (v, h)
19    | none => .error (.ub "access through a dangling pointer (z_stream)")
20
21/-- `*p = v` for a `z_stream *`: faults if `p` is null, dangling or read-only. -/
22def stZStream (p : ZStreamPtr) (v : ZStream) : M Unit := fun h =>
23  match p with
24  | none => .error (.ub "null dereference (z_stream)")
25  | some r => match r.get h with
26    | some _ => if r.isRo then .error (.ub "store into a read-only object (z_stream)") else .ok ((), r.put h v)
27    | none => .error (.ub "access through a dangling pointer (z_stream)")
28
29theorem ldZStream_ok {h : Heap} {r : ZStreamRef} {v : ZStream} (e : r.get h = some v) :
30    ldZStream (some r) h = .ok (v, h) := by simp [ldZStream, e]
31
32theorem stZStream_ok {h : Heap} {r : ZStreamRef} {v v' : ZStream} (e : r.get h = some v) (hro : r.isRo = false) :
33    stZStream (some r) v' h = .ok ((), r.put h v') := by simp [stZStream, e, hro]
34
35theorem ldZStream_tab {h : Heap} {i : Nat} {v : ZStream} (e : h.streams i = some v) :
36    ldZStream (some (.tab i)) h = .ok (v, h) := ldZStream_ok e
37
38theorem stZStream_tab {h : Heap} {i : Nat} {v v' : ZStream} (e : h.streams i = some v) :
39    stZStream (some (.tab i)) v' h = .ok ((), { h with streams := upd h.streams i (some v') }) := by
40  rw [stZStream_ok (r := .tab i) e rfl]
41  rw [ZStreamRef.put_tab e v']
42
43/-- `*p` for a `gz_header *`: faults if `p` is null or does not point to a live object. -/
44def ldGzHeader (p : GzHeaderPtr) : M GzHeader := fun h =>
45  match p with
46  | none => .error (.ub "null dereference (gz_header)")
47  | some r => match r.get h with
48    | some v => .ok (v, h)
49    | none => .error (.ub "access through a dangling pointer (gz_header)")
50
51/-- `*p = v` for a `gz_header *`: faults if `p` is null, dangling or read-only. -/
52def stGzHeader (p : GzHeaderPtr) (v : GzHeader) : M Unit := fun h =>
53  match p with
54  | none => .error (.ub "null dereference (gz_header)")
55  | some r => match r.get h with
56    | some _ => if r.isRo then .error (.ub "store into a read-only object (gz_header)") else .ok ((), r.put h v)
57    | none => .error (.ub "access through a dangling pointer (gz_header)")
58
59theorem ldGzHeader_ok {h : Heap} {r : GzHeaderRef} {v : GzHeader} (e : r.get h = some v) :
60    ldGzHeader (some r) h = .ok (v, h) := by simp [ldGzHeader, e]
61
62theorem stGzHeader_ok {h : Heap} {r : GzHeaderRef} {v v' : GzHeader} (e : r.get h = some v) (hro : r.isRo = false) :
63    stGzHeader (some r) v' h = .ok ((), r.put h v') := by simp [stGzHeader, e, hro]
64
65theorem ldGzHeader_tab {h : Heap} {i : Nat} {v : GzHeader} (e : h.gzheaders i = some v) :
66    ldGzHeader (some (.tab i)) h = .ok (v, h) := ldGzHeader_ok e
67
68theorem stGzHeader_tab {h : Heap} {i : Nat} {v v' : GzHeader} (e : h.gzheaders i = some v) :
69    stGzHeader (some (.tab i)) v' h = .ok ((), { h with gzheaders := upd h.gzheaders i (some v') }) := by
70  rw [stGzHeader_ok (r := .tab i) e rfl]
71  rw [GzHeaderRef.put_tab e v']
72
73/-- `*p` for a `deflate_state *`: faults if `p` is null or does not point to a live object. -/
74def ldDeflateState (p : DeflateStatePtr) : M DeflateState := fun h =>
75  match p with
76  | none => .error (.ub "null dereference (deflate_state)")
77  | some r => match r.get h with
78    | some v => .ok (v, h)
79    | none => .error (.ub "access through a dangling pointer (deflate_state)")
80
81/-- `*p = v` for a `deflate_state *`: faults if `p` is null, dangling or read-only. -/
82def stDeflateState (p : DeflateStatePtr) (v : DeflateState) : M Unit := fun h =>
83  match p with
84  | none => .error (.ub "null dereference (deflate_state)")
85  | some r => match r.get h with
86    | some _ => if r.isRo then .error (.ub "store into a read-only object (deflate_state)") else .ok ((), r.put h v)
87    | none => .error (.ub "access through a dangling pointer (deflate_state)")
88
89theorem ldDeflateState_ok {h : Heap} {r : DeflateStateRef} {v : DeflateState} (e : r.get h = some v) :
90    ldDeflateState (some r) h = .ok (v, h) := by simp [ldDeflateState, e]
91
92theorem stDeflateState_ok {h : Heap} {r : DeflateStateRef} {v v' : DeflateState} (e : r.get h = some v) (hro : r.isRo = false) :
93    stDeflateState (some r) v' h = .ok ((), r.put h v') := by simp [stDeflateState, e, hro]
94
95theorem ldDeflateState_tab {h : Heap} {i : Nat} {v : DeflateState} (e : h.dstates i = some v) :
96    ldDeflateState (some (.tab i)) h = .ok (v, h) := ldDeflateState_ok e
97
98theorem stDeflateState_tab {h : Heap} {i : Nat} {v v' : DeflateState} (e : h.dstates i = some v) :
99    stDeflateState (some (.tab i)) v' h = .ok ((), { h with dstates := upd h.dstates i (some v') }) := by
100  rw [stDeflateState_ok (r := .tab i) e rfl]
101  rw [DeflateStateRef.put_tab e v']
102
103/-- `*p` for a `inflate_state *`: faults if `p` is null or does not point to a live object. -/
104def ldInflateState (p : InflateStatePtr) : M InflateState := fun h =>
105  match p with
106  | none => .error (.ub "null dereference (inflate_state)")
107  | some r => match r.get h with
108    | some v => .ok (v, h)
109    | none => .error (.ub "access through a dangling pointer (inflate_state)")
110
111/-- `*p = v` for a `inflate_state *`: faults if `p` is null, dangling or read-only. -/
112def stInflateState (p : InflateStatePtr) (v : InflateState) : M Unit := fun h =>
113  match p with
114  | none => .error (.ub "null dereference (inflate_state)")
115  | some r => match r.get h with
116    | some _ => if r.isRo then .error (.ub "store into a read-only object (inflate_state)") else .ok ((), r.put h v)
117    | none => .error (.ub "access through a dangling pointer (inflate_state)")
118
119theorem ldInflateState_ok {h : Heap} {r : InflateStateRef} {v : InflateState} (e : r.get h = some v) :
120    ldInflateState (some r) h = .ok (v, h) := by simp [ldInflateState, e]
121
122theorem stInflateState_ok {h : Heap} {r : InflateStateRef} {v v' : InflateState} (e : r.get h = some v) (hro : r.isRo = false) :
123    stInflateState (some r) v' h = .ok ((), r.put h v') := by simp [stInflateState, e, hro]
124
125theorem ldInflateState_tab {h : Heap} {i : Nat} {v : InflateState} (e : h.istates i = some v) :
126    ldInflateState (some (.tab i)) h = .ok (v, h) := ldInflateState_ok e
127
128theorem stInflateState_tab {h : Heap} {i : Nat} {v v' : InflateState} (e : h.istates i = some v) :
129    stInflateState (some (.tab i)) v' h = .ok ((), { h with istates := upd h.istates i (some v') }) := by
130  rw [stInflateState_ok (r := .tab i) e rfl]
131  rw [InflateStateRef.put_tab e v']
132
133/-- `*p` for a `gz_state *`: faults if `p` is null or does not point to a live object. -/
134def ldGzState (p : GzStatePtr) : M GzState := fun h =>
135  match p with
136  | none => .error (.ub "null dereference (gz_state)")
137  | some r => match r.get h with
138    | some v => .ok (v, h)
139    | none => .error (.ub "access through a dangling pointer (gz_state)")
140
141/-- `*p = v` for a `gz_state *`: faults if `p` is null, dangling or read-only. -/
142def stGzState (p : GzStatePtr) (v : GzState) : M Unit := fun h =>
143  match p with
144  | none => .error (.ub "null dereference (gz_state)")
145  | some r => match r.get h with
146    | some _ => if r.isRo then .error (.ub "store into a read-only object (gz_state)") else .ok ((), r.put h v)
147    | none => .error (.ub "access through a dangling pointer (gz_state)")
148
149theorem ldGzState_ok {h : Heap} {r : GzStateRef} {v : GzState} (e : r.get h = some v) :
150    ldGzState (some r) h = .ok (v, h) := by simp [ldGzState, e]
151
152theorem stGzState_ok {h : Heap} {r : GzStateRef} {v v' : GzState} (e : r.get h = some v) (hro : r.isRo = false) :
153    stGzState (some r) v' h = .ok ((), r.put h v') := by simp [stGzState, e, hro]
154
155theorem ldGzState_tab {h : Heap} {i : Nat} {v : GzState} (e : h.gzstates i = some v) :
156    ldGzState (some (.tab i)) h = .ok (v, h) := ldGzState_ok e
157
158theorem stGzState_tab {h : Heap} {i : Nat} {v v' : GzState} (e : h.gzstates i = some v) :
159    stGzState (some (.tab i)) v' h = .ok ((), { h with gzstates := upd h.gzstates i (some v') }) := by
160  rw [stGzState_ok (r := .tab i) e rfl]
161  rw [GzStateRef.put_tab e v']
162
163/-- `*p` for a `gzFile_s *`: faults if `p` is null or does not point to a live object. -/
164def ldGzFile (p : GzFilePtr) : M GzFile := fun h =>
165  match p with
166  | none => .error (.ub "null dereference (gzFile_s)")
167  | some r => match r.get h with
168    | some v => .ok (v, h)
169    | none => .error (.ub "access through a dangling pointer (gzFile_s)")
170
171/-- `*p = v` for a `gzFile_s *`: faults if `p` is null, dangling or read-only. -/
172def stGzFile (p : GzFilePtr) (v : GzFile) : M Unit := fun h =>
173  match p with
174  | none => .error (.ub "null dereference (gzFile_s)")
175  | some r => match r.get h with
176    | some _ => if r.isRo then .error (.ub "store into a read-only object (gzFile_s)") else .ok ((), r.put h v)
177    | none => .error (.ub "access through a dangling pointer (gzFile_s)")
178
179theorem ldGzFile_ok {h : Heap} {r : GzFileRef} {v : GzFile} (e : r.get h = some v) :
180    ldGzFile (some r) h = .ok (v, h) := by simp [ldGzFile, e]
181
182theorem stGzFile_ok {h : Heap} {r : GzFileRef} {v v' : GzFile} (e : r.get h = some v) (hro : r.isRo = false) :
183    stGzFile (some r) v' h = .ok ((), r.put h v') := by simp [stGzFile, e, hro]
184
185/-- `*p` for a `tree_desc *`: faults if `p` is null or does not point to a live object. -/
186def ldTreeDesc (p : TreeDescPtr) : M TreeDesc := fun h =>
187  match p with
188  | none => .error (.ub "null dereference (tree_desc)")
189  | some r => match r.get h with
190    | some v => .ok (v, h)
191    | none => .error (.ub "access through a dangling pointer (tree_desc)")
192
193/-- `*p = v` for a `tree_desc *`: faults if `p` is null, dangling or read-only. -/
194def stTreeDesc (p : TreeDescPtr) (v : TreeDesc) : M Unit := fun h =>
195  match p with
196  | none => .error (.ub "null dereference (tree_desc)")
197  | some r => match r.get h with
198    | some _ => if r.isRo then .error (.ub "store into a read-only object (tree_desc)") else .ok ((), r.put h v)
199    | none => .error (.ub "access through a dangling pointer (tree_desc)")
200
201theorem ldTreeDesc_ok {h : Heap} {r : TreeDescRef} {v : TreeDesc} (e : r.get h = some v) :
202    ldTreeDesc (some r) h = .ok (v, h) := by simp [ldTreeDesc, e]
203
204theorem stTreeDesc_ok {h : Heap} {r : TreeDescRef} {v v' : TreeDesc} (e : r.get h = some v) (hro : r.isRo = false) :
205    stTreeDesc (some r) v' h = .ok ((), r.put h v') := by simp [stTreeDesc, e, hro]
206
207/-- `*p` for a `static_tree_desc *`: faults if `p` is null or does not point to a live object. -/
208def ldStaticTreeDesc (p : StaticTreeDescPtr) : M StaticTreeDesc := fun h =>
209  match p with
210  | none => .error (.ub "null dereference (static_tree_desc)")
211  | some r => match r.get h with
212    | some v => .ok (v, h)
213    | none => .error (.ub "access through a dangling pointer (static_tree_desc)")
214
215/-- `*p = v` for a `static_tree_desc *`: faults if `p` is null, dangling or read-only. -/
216def stStaticTreeDesc (p : StaticTreeDescPtr) (v : StaticTreeDesc) : M Unit := fun h =>
217  match p with
218  | none => .error (.ub "null dereference (static_tree_desc)")
219  | some r => match r.get h with
220    | some _ => if r.isRo then .error (.ub "store into a read-only object (static_tree_desc)") else .ok ((), r.put h v)
221    | none => .error (.ub "access through a dangling pointer (static_tree_desc)")
222
223theorem ldStaticTreeDesc_ok {h : Heap} {r : StaticTreeDescRef} {v : StaticTreeDesc} (e : r.get h = some v) :
224    ldStaticTreeDesc (some r) h = .ok (v, h) := by simp [ldStaticTreeDesc, e]
225
226theorem stStaticTreeDesc_ok {h : Heap} {r : StaticTreeDescRef} {v v' : StaticTreeDesc} (e : r.get h = some v) (hro : r.isRo = false) :
227    stStaticTreeDesc (some r) v' h = .ok ((), r.put h v') := by simp [stStaticTreeDesc, e, hro]
228
229/-! ## `struct internal_state *` and its casts -/
230
231/-- `(deflate_state *) p` for `p` of type `struct internal_state *`: faults if `p` points to the other kind of state. -/
232def castDeflateState (p : Option StateRef) : M DeflateStatePtr := fun h =>
233  match p with
234  | none => .ok (none, h)
235  | some (.deflate i) => .ok (some (.tab i), h)
236  | some (.inflate _) => .error (.ub "a inflate_state is used as a deflate_state")
237
238theorem castDeflateState_ok {h : Heap} {i : Nat} : castDeflateState (some (.deflate i)) h = .ok (some (.tab i), h) := rfl
239
240/-- `(struct internal_state *) p` for `p` of type `deflate_state *`. -/
241def StateRef.ofDeflateState : DeflateStatePtr → Option StateRef
242  | none => none
243  | some (.tab i) => some (.deflate i)
244
245/-- `(inflate_state *) p` for `p` of type `struct internal_state *`: faults if `p` points to the other kind of state. -/
246def castInflateState (p : Option StateRef) : M InflateStatePtr := fun h =>
247  match p with
248  | none => .ok (none, h)
249  | some (.inflate i) => .ok (some (.tab i), h)
250  | some (.deflate _) => .error (.ub "a deflate_state is used as a inflate_state")
251
252theorem castInflateState_ok {h : Heap} {i : Nat} : castInflateState (some (.inflate i)) h = .ok (some (.tab i), h) := rfl
253
254/-- `(struct internal_state *) p` for `p` of type `inflate_state *`. -/
255def StateRef.ofInflateState : InflateStatePtr → Option StateRef
256  | none => none
257  | some (.tab i) => some (.inflate i)
258
259end C