|
1 (* Author: Andrew Boyton, 2012 |
|
2 Maintainers: Gerwin Klein <kleing at cse.unsw.edu.au> |
|
3 Rafal Kolanski <rafal.kolanski at nicta.com.au> |
|
4 *) |
|
5 |
|
6 header "Instantiating capDL as a separation algebra." |
|
7 |
|
8 theory Abstract_Separation_D |
|
9 imports "../../Sep_Tactics" Types_D "../../Map_Extra" |
|
10 begin |
|
11 |
|
12 (************************************** |
|
13 * Start of lemmas to move elsewhere. * |
|
14 **************************************) |
|
15 |
|
16 lemma inter_empty_not_both: |
|
17 "\<lbrakk>x \<in> A; A \<inter> B = {}\<rbrakk> \<Longrightarrow> x \<notin> B" |
|
18 by fastforce |
|
19 |
|
20 lemma union_intersection: |
|
21 "A \<inter> (A \<union> B) = A" |
|
22 "B \<inter> (A \<union> B) = B" |
|
23 "(A \<union> B) \<inter> A = A" |
|
24 "(A \<union> B) \<inter> B = B" |
|
25 by fastforce+ |
|
26 |
|
27 lemma union_intersection1: "A \<inter> (A \<union> B) = A" |
|
28 by (rule inf_sup_absorb) |
|
29 lemma union_intersection2: "B \<inter> (A \<union> B) = B" |
|
30 by fastforce |
|
31 |
|
32 (* This lemma is strictly weaker than restrict_map_disj. *) |
|
33 lemma restrict_map_disj': |
|
34 "S \<inter> T = {} \<Longrightarrow> h |` S \<bottom> h' |` T" |
|
35 by (auto simp: map_disj_def restrict_map_def dom_def) |
|
36 |
|
37 lemma map_add_restrict_comm: |
|
38 "S \<inter> T = {} \<Longrightarrow> h |` S ++ h' |` T = h' |` T ++ h |` S" |
|
39 apply (drule restrict_map_disj') |
|
40 apply (erule map_add_com) |
|
41 done |
|
42 |
|
43 (************************************ |
|
44 * End of lemmas to move elsewhere. * |
|
45 ************************************) |
|
46 |
|
47 |
|
48 |
|
49 (* The state for separation logic has: |
|
50 * The memory heap. |
|
51 * A function for which objects own which fields. |
|
52 In capDL, we say that an object either owns all of its fields, or none of them. |
|
53 These are both taken from the cdl_state. |
|
54 *) |
|
55 |
|
56 datatype sep_state = SepState cdl_heap cdl_ghost_state |
|
57 |
|
58 (* Functions to get the heap and the ghost_state from the sep_state. *) |
|
59 primrec sep_heap :: "sep_state \<Rightarrow> cdl_heap" |
|
60 where "sep_heap (SepState h gs) = h" |
|
61 |
|
62 primrec sep_ghost_state :: "sep_state \<Rightarrow> cdl_ghost_state" |
|
63 where "sep_ghost_state (SepState h gs) = gs" |
|
64 |
|
65 definition |
|
66 the_set :: "'a option set \<Rightarrow> 'a set" |
|
67 where |
|
68 "the_set xs = {x. Some x \<in> xs}" |
|
69 |
|
70 lemma the_set_union [simp]: |
|
71 "the_set (A \<union> B) = the_set A \<union> the_set B" |
|
72 by (fastforce simp: the_set_def) |
|
73 |
|
74 lemma the_set_inter [simp]: |
|
75 "the_set (A \<inter> B) = the_set A \<inter> the_set B" |
|
76 by (fastforce simp: the_set_def) |
|
77 |
|
78 lemma the_set_inter_empty: |
|
79 "A \<inter> B = {} \<Longrightarrow> the_set A \<inter> the_set B = {}" |
|
80 by (fastforce simp: the_set_def) |
|
81 |
|
82 |
|
83 (* As the capDL operations mostly take the state (rather than the heap) |
|
84 * we need to redefine some of them again to take just the heap. |
|
85 *) |
|
86 definition |
|
87 slots_of_heap :: "cdl_heap \<Rightarrow> cdl_object_id \<Rightarrow> cdl_cap_map" |
|
88 where |
|
89 "slots_of_heap h \<equiv> \<lambda>obj_id. |
|
90 case h obj_id of |
|
91 None \<Rightarrow> empty |
|
92 | Some obj \<Rightarrow> object_slots obj" |
|
93 |
|
94 (* Adds new caps to an object. It won't overwrite on a collision. *) |
|
95 definition |
|
96 add_to_slots :: "cdl_cap_map \<Rightarrow> cdl_object \<Rightarrow> cdl_object" |
|
97 where |
|
98 "add_to_slots new_val obj \<equiv> update_slots (new_val ++ (object_slots obj)) obj" |
|
99 |
|
100 lemma add_to_slots_assoc: |
|
101 "add_to_slots x (add_to_slots (y ++ z) obj) = |
|
102 add_to_slots (x ++ y) (add_to_slots z obj)" |
|
103 apply (clarsimp simp: add_to_slots_def update_slots_def object_slots_def) |
|
104 apply (fastforce simp: cdl_tcb.splits cdl_cnode.splits |
|
105 split: cdl_object.splits) |
|
106 done |
|
107 |
|
108 (* Lemmas about add_to_slots, update_slots and object_slots. *) |
|
109 lemma add_to_slots_twice [simp]: |
|
110 "add_to_slots x (add_to_slots y a) = add_to_slots (x ++ y) a" |
|
111 by (fastforce simp: add_to_slots_def update_slots_def object_slots_def |
|
112 split: cdl_object.splits) |
|
113 |
|
114 lemma slots_of_heap_empty [simp]: "slots_of_heap empty object_id = empty" |
|
115 by (simp add: slots_of_heap_def) |
|
116 |
|
117 lemma slots_of_heap_empty2 [simp]: |
|
118 "h obj_id = None \<Longrightarrow> slots_of_heap h obj_id = empty" |
|
119 by (simp add: slots_of_heap_def) |
|
120 |
|
121 lemma update_slots_add_to_slots_empty [simp]: |
|
122 "update_slots empty (add_to_slots new obj) = update_slots empty obj" |
|
123 by (clarsimp simp: update_slots_def add_to_slots_def split:cdl_object.splits) |
|
124 |
|
125 lemma update_object_slots_id [simp]: "update_slots (object_slots a) a = a" |
|
126 by (clarsimp simp: update_slots_def object_slots_def |
|
127 split: cdl_object.splits) |
|
128 |
|
129 lemma update_slots_of_heap_id [simp]: |
|
130 "h obj_id = Some obj \<Longrightarrow> update_slots (slots_of_heap h obj_id) obj = obj" |
|
131 by (clarsimp simp: update_slots_def slots_of_heap_def object_slots_def |
|
132 split: cdl_object.splits) |
|
133 |
|
134 lemma add_to_slots_empty [simp]: "add_to_slots empty h = h" |
|
135 by (simp add: add_to_slots_def) |
|
136 |
|
137 lemma update_slots_eq: |
|
138 "update_slots a o1 = update_slots a o2 \<Longrightarrow> update_slots b o1 = update_slots b o2" |
|
139 by (fastforce simp: update_slots_def cdl_tcb.splits cdl_cnode.splits |
|
140 split: cdl_object.splits) |
|
141 |
|
142 |
|
143 |
|
144 (* If there are not two conflicting objects at a position in two states. |
|
145 * Objects conflict if their types are different or their ghost_states collide. |
|
146 *) |
|
147 definition |
|
148 not_conflicting_objects :: "sep_state \<Rightarrow> sep_state \<Rightarrow> cdl_object_id \<Rightarrow> bool" |
|
149 where |
|
150 "not_conflicting_objects state_a state_b = (\<lambda>obj_id. |
|
151 let heap_a = sep_heap state_a; |
|
152 heap_b = sep_heap state_b; |
|
153 gs_a = sep_ghost_state state_a; |
|
154 gs_b = sep_ghost_state state_b |
|
155 in case (heap_a obj_id, heap_b obj_id) of |
|
156 (Some o1, Some o2) \<Rightarrow> object_type o1 = object_type o2 \<and> gs_a obj_id \<inter> gs_b obj_id = {} |
|
157 | _ \<Rightarrow> True)" |
|
158 |
|
159 |
|
160 (* "Cleans" slots to conform with the compontents. *) |
|
161 definition |
|
162 clean_slots :: "cdl_cap_map \<Rightarrow> cdl_components \<Rightarrow> cdl_cap_map" |
|
163 where |
|
164 "clean_slots slots cmp \<equiv> slots |` the_set cmp" |
|
165 |
|
166 (* Sets the fields of an object to a "clean" state. |
|
167 Because a frame's size is part of it's type, we don't reset it. *) |
|
168 definition |
|
169 object_clean_fields :: "cdl_object \<Rightarrow> cdl_components \<Rightarrow> cdl_object" |
|
170 where |
|
171 "object_clean_fields obj cmp \<equiv> if None \<in> cmp then obj else case obj of |
|
172 Tcb x \<Rightarrow> Tcb (x\<lparr>cdl_tcb_fault_endpoint := undefined\<rparr>) |
|
173 | CNode x \<Rightarrow> CNode (x\<lparr>cdl_cnode_size_bits := undefined \<rparr>) |
|
174 | _ \<Rightarrow> obj" |
|
175 |
|
176 (* Sets the slots of an object to a "clean" state. *) |
|
177 definition |
|
178 object_clean_slots :: "cdl_object \<Rightarrow> cdl_components \<Rightarrow> cdl_object" |
|
179 where |
|
180 "object_clean_slots obj cmp \<equiv> update_slots (clean_slots (object_slots obj) cmp) obj" |
|
181 |
|
182 (* Sets an object to a "clean" state. *) |
|
183 definition |
|
184 object_clean :: "cdl_object \<Rightarrow> cdl_components \<Rightarrow> cdl_object" |
|
185 where |
|
186 "object_clean obj gs \<equiv> object_clean_slots (object_clean_fields obj gs) gs" |
|
187 |
|
188 (* Overrides the left object with the attributes of the right, as specified by the ghost state. |
|
189 If the components for an object are empty, then this object is treated as empty, and thus ignored. |
|
190 *) |
|
191 definition |
|
192 object_add :: "cdl_object \<Rightarrow> cdl_object \<Rightarrow> cdl_components \<Rightarrow> cdl_components \<Rightarrow> cdl_object" |
|
193 where |
|
194 "object_add obj_a obj_b cmps_a cmps_b \<equiv> |
|
195 let clean_obj_a = object_clean obj_a cmps_a; |
|
196 clean_obj_b = object_clean obj_b cmps_b |
|
197 in if (cmps_a = {}) |
|
198 then clean_obj_b |
|
199 else if (cmps_b = {}) |
|
200 then clean_obj_a |
|
201 else if (None \<in> cmps_b) |
|
202 then (update_slots (object_slots clean_obj_a ++ object_slots clean_obj_b) clean_obj_b) |
|
203 else (update_slots (object_slots clean_obj_a ++ object_slots clean_obj_b) clean_obj_a)" |
|
204 |
|
205 (* Heaps are added by adding their repsective objects. |
|
206 * The ghost state tells us which object's fields should be taken. |
|
207 * Adding objects of the same type adds their caps |
|
208 * (overwrites the left with the right). |
|
209 *) |
|
210 definition |
|
211 cdl_heap_add :: "sep_state \<Rightarrow> sep_state \<Rightarrow> cdl_heap" |
|
212 where |
|
213 "cdl_heap_add state_a state_b \<equiv> \<lambda>obj_id. |
|
214 let heap_a = sep_heap state_a; |
|
215 heap_b = sep_heap state_b; |
|
216 gs_a = sep_ghost_state state_a; |
|
217 gs_b = sep_ghost_state state_b |
|
218 in case heap_b obj_id of |
|
219 None \<Rightarrow> heap_a obj_id |
|
220 | Some obj_b \<Rightarrow> case heap_a obj_id of |
|
221 None \<Rightarrow> heap_b obj_id |
|
222 | Some obj_a \<Rightarrow> Some (object_add obj_a obj_b (gs_a obj_id) (gs_b obj_id))" |
|
223 |
|
224 (* Heaps are added by adding their repsective objects. |
|
225 * The ghost state tells us which object's fields should be taken. |
|
226 * Adding objects of the same type adds their caps |
|
227 * (overwrites the left with the right). |
|
228 *) |
|
229 definition |
|
230 cdl_ghost_state_add :: "sep_state \<Rightarrow> sep_state \<Rightarrow> cdl_ghost_state" |
|
231 where |
|
232 "cdl_ghost_state_add state_a state_b \<equiv> \<lambda>obj_id. |
|
233 let heap_a = sep_heap state_a; |
|
234 heap_b = sep_heap state_b; |
|
235 gs_a = sep_ghost_state state_a; |
|
236 gs_b = sep_ghost_state state_b |
|
237 in if heap_a obj_id = None \<and> heap_b obj_id \<noteq> None then gs_b obj_id |
|
238 else if heap_b obj_id = None \<and> heap_a obj_id \<noteq> None then gs_a obj_id |
|
239 else gs_a obj_id \<union> gs_b obj_id" |
|
240 |
|
241 |
|
242 (* Adding states adds their heaps, |
|
243 * and each objects owns whichever fields it owned in either heap. |
|
244 *) |
|
245 definition |
|
246 sep_state_add :: "sep_state \<Rightarrow> sep_state \<Rightarrow> sep_state" |
|
247 where |
|
248 "sep_state_add state_a state_b \<equiv> |
|
249 let |
|
250 heap_a = sep_heap state_a; |
|
251 heap_b = sep_heap state_b; |
|
252 gs_a = sep_ghost_state state_a; |
|
253 gs_b = sep_ghost_state state_b |
|
254 in |
|
255 SepState (cdl_heap_add state_a state_b) (cdl_ghost_state_add state_a state_b)" |
|
256 |
|
257 |
|
258 (* Heaps are disjoint if for all of their objects: |
|
259 * the caps of their respective objects are disjoint, |
|
260 * their respective objects don't conflict, |
|
261 * they don't both own any of the same fields. |
|
262 *) |
|
263 definition |
|
264 sep_state_disj :: "sep_state \<Rightarrow> sep_state \<Rightarrow> bool" |
|
265 where |
|
266 "sep_state_disj state_a state_b \<equiv> |
|
267 let |
|
268 heap_a = sep_heap state_a; |
|
269 heap_b = sep_heap state_b; |
|
270 gs_a = sep_ghost_state state_a; |
|
271 gs_b = sep_ghost_state state_b |
|
272 in |
|
273 \<forall>obj_id. not_conflicting_objects state_a state_b obj_id" |
|
274 |
|
275 lemma not_conflicting_objects_comm: |
|
276 "not_conflicting_objects h1 h2 obj = not_conflicting_objects h2 h1 obj" |
|
277 apply (clarsimp simp: not_conflicting_objects_def split:option.splits) |
|
278 apply (fastforce simp: update_slots_def cdl_tcb.splits cdl_cnode.splits |
|
279 split: cdl_object.splits) |
|
280 done |
|
281 |
|
282 lemma object_clean_comm: |
|
283 "\<lbrakk>object_type obj_a = object_type obj_b; |
|
284 object_slots obj_a ++ object_slots obj_b = object_slots obj_b ++ object_slots obj_a; None \<notin> cmp\<rbrakk> |
|
285 \<Longrightarrow> object_clean (add_to_slots (object_slots obj_a) obj_b) cmp = |
|
286 object_clean (add_to_slots (object_slots obj_b) obj_a) cmp" |
|
287 apply (clarsimp simp: object_type_def split: cdl_object.splits) |
|
288 apply (clarsimp simp: object_clean_def object_clean_slots_def object_clean_fields_def |
|
289 add_to_slots_def object_slots_def update_slots_def |
|
290 cdl_tcb.splits cdl_cnode.splits |
|
291 split: cdl_object.splits)+ |
|
292 done |
|
293 |
|
294 lemma add_to_slots_object_slots: |
|
295 "object_type y = object_type z |
|
296 \<Longrightarrow> add_to_slots (object_slots (add_to_slots (x) y)) z = |
|
297 add_to_slots (x ++ object_slots y) z" |
|
298 apply (clarsimp simp: add_to_slots_def update_slots_def object_slots_def) |
|
299 apply (fastforce simp: object_type_def cdl_tcb.splits cdl_cnode.splits |
|
300 split: cdl_object.splits) |
|
301 done |
|
302 |
|
303 lemma not_conflicting_objects_empty [simp]: |
|
304 "not_conflicting_objects s (SepState empty (\<lambda>obj_id. {})) obj_id" |
|
305 by (clarsimp simp: not_conflicting_objects_def split:option.splits) |
|
306 |
|
307 lemma empty_not_conflicting_objects [simp]: |
|
308 "not_conflicting_objects (SepState empty (\<lambda>obj_id. {})) s obj_id" |
|
309 by (clarsimp simp: not_conflicting_objects_def split:option.splits) |
|
310 |
|
311 lemma not_conflicting_objects_empty_object [elim!]: |
|
312 "(sep_heap x) obj_id = None \<Longrightarrow> not_conflicting_objects x y obj_id" |
|
313 by (clarsimp simp: not_conflicting_objects_def) |
|
314 |
|
315 lemma empty_object_not_conflicting_objects [elim!]: |
|
316 "(sep_heap y) obj_id = None \<Longrightarrow> not_conflicting_objects x y obj_id" |
|
317 apply (drule not_conflicting_objects_empty_object [where y=x]) |
|
318 apply (clarsimp simp: not_conflicting_objects_comm) |
|
319 done |
|
320 |
|
321 lemma cdl_heap_add_empty [simp]: |
|
322 "cdl_heap_add (SepState h gs) (SepState empty (\<lambda>obj_id. {})) = h" |
|
323 by (simp add: cdl_heap_add_def) |
|
324 |
|
325 lemma empty_cdl_heap_add [simp]: |
|
326 "cdl_heap_add (SepState empty (\<lambda>obj_id. {})) (SepState h gs)= h" |
|
327 apply (simp add: cdl_heap_add_def) |
|
328 apply (rule ext) |
|
329 apply (clarsimp split: option.splits) |
|
330 done |
|
331 |
|
332 lemma map_add_result_empty1: "a ++ b = empty \<Longrightarrow> a = empty" |
|
333 apply (subgoal_tac "dom (a++b) = {}") |
|
334 apply (subgoal_tac "dom (a) = {}") |
|
335 apply clarsimp |
|
336 apply (unfold dom_map_add)[1] |
|
337 apply clarsimp |
|
338 apply clarsimp |
|
339 done |
|
340 |
|
341 lemma map_add_result_empty2: "a ++ b = empty \<Longrightarrow> b = empty" |
|
342 apply (subgoal_tac "dom (a++b) = {}") |
|
343 apply (subgoal_tac "dom (a) = {}") |
|
344 apply clarsimp |
|
345 apply (unfold dom_map_add)[1] |
|
346 apply clarsimp |
|
347 apply clarsimp |
|
348 done |
|
349 |
|
350 lemma map_add_emptyE [elim!]: "\<lbrakk>a ++ b = empty; \<lbrakk>a = empty; b = empty\<rbrakk> \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R" |
|
351 apply (frule map_add_result_empty1) |
|
352 apply (frule map_add_result_empty2) |
|
353 apply clarsimp |
|
354 done |
|
355 |
|
356 lemma clean_slots_empty [simp]: |
|
357 "clean_slots empty cmp = empty" |
|
358 by (clarsimp simp: clean_slots_def) |
|
359 |
|
360 lemma object_type_update_slots [simp]: |
|
361 "object_type (update_slots slots x) = object_type x" |
|
362 by (clarsimp simp: object_type_def update_slots_def split: cdl_object.splits) |
|
363 |
|
364 lemma object_type_object_clean_slots [simp]: |
|
365 "object_type (object_clean_slots x cmp) = object_type x" |
|
366 by (clarsimp simp: object_clean_slots_def) |
|
367 |
|
368 lemma object_type_object_clean_fields [simp]: |
|
369 "object_type (object_clean_fields x cmp) = object_type x" |
|
370 by (clarsimp simp: object_clean_fields_def object_type_def split: cdl_object.splits) |
|
371 |
|
372 lemma object_type_object_clean [simp]: |
|
373 "object_type (object_clean x cmp) = object_type x" |
|
374 by (clarsimp simp: object_clean_def) |
|
375 |
|
376 lemma object_type_add_to_slots [simp]: |
|
377 "object_type (add_to_slots slots x) = object_type x" |
|
378 by (clarsimp simp: object_type_def add_to_slots_def update_slots_def split: cdl_object.splits) |
|
379 |
|
380 lemma object_slots_update_slots [simp]: |
|
381 "has_slots obj \<Longrightarrow> object_slots (update_slots slots obj) = slots" |
|
382 by (clarsimp simp: object_slots_def update_slots_def has_slots_def |
|
383 split: cdl_object.splits) |
|
384 |
|
385 lemma object_slots_update_slots_empty [simp]: |
|
386 "\<not>has_slots obj \<Longrightarrow> object_slots (update_slots slots obj) = empty" |
|
387 by (clarsimp simp: object_slots_def update_slots_def has_slots_def |
|
388 split: cdl_object.splits) |
|
389 |
|
390 lemma update_slots_no_slots [simp]: |
|
391 "\<not>has_slots obj \<Longrightarrow> update_slots slots obj = obj" |
|
392 by (clarsimp simp: update_slots_def has_slots_def split: cdl_object.splits) |
|
393 |
|
394 lemma update_slots_update_slots [simp]: |
|
395 "update_slots slots (update_slots slots' obj) = update_slots slots obj" |
|
396 by (clarsimp simp: update_slots_def split: cdl_object.splits) |
|
397 |
|
398 lemma update_slots_same_object: |
|
399 "a = b \<Longrightarrow> update_slots a obj = update_slots b obj" |
|
400 by (erule arg_cong) |
|
401 |
|
402 lemma object_type_has_slots: |
|
403 "\<lbrakk>has_slots x; object_type x = object_type y\<rbrakk> \<Longrightarrow> has_slots y" |
|
404 by (clarsimp simp: object_type_def has_slots_def split: cdl_object.splits) |
|
405 |
|
406 lemma object_slots_object_clean_fields [simp]: |
|
407 "object_slots (object_clean_fields obj cmp) = object_slots obj" |
|
408 by (clarsimp simp: object_slots_def object_clean_fields_def split: cdl_object.splits) |
|
409 |
|
410 lemma object_slots_object_clean_slots [simp]: |
|
411 "object_slots (object_clean_slots obj cmp) = clean_slots (object_slots obj) cmp" |
|
412 by (clarsimp simp: object_clean_slots_def object_slots_def update_slots_def split: cdl_object.splits) |
|
413 |
|
414 lemma object_slots_object_clean [simp]: |
|
415 "object_slots (object_clean obj cmp) = clean_slots (object_slots obj) cmp" |
|
416 by (clarsimp simp: object_clean_def) |
|
417 |
|
418 lemma object_slots_add_to_slots [simp]: |
|
419 "object_type y = object_type z \<Longrightarrow> object_slots (add_to_slots (object_slots y) z) = object_slots y ++ object_slots z" |
|
420 by (clarsimp simp: object_slots_def add_to_slots_def update_slots_def object_type_def split: cdl_object.splits) |
|
421 |
|
422 lemma update_slots_object_clean_slots [simp]: |
|
423 "update_slots slots (object_clean_slots obj cmp) = update_slots slots obj" |
|
424 by (clarsimp simp: object_clean_slots_def) |
|
425 |
|
426 lemma object_clean_fields_idem [simp]: |
|
427 "object_clean_fields (object_clean_fields obj cmp) cmp = object_clean_fields obj cmp" |
|
428 by (clarsimp simp: object_clean_fields_def split: cdl_object.splits) |
|
429 |
|
430 lemma object_clean_slots_idem [simp]: |
|
431 "object_clean_slots (object_clean_slots obj cmp) cmp = object_clean_slots obj cmp" |
|
432 apply (case_tac "has_slots obj") |
|
433 apply (clarsimp simp: object_clean_slots_def clean_slots_def)+ |
|
434 done |
|
435 |
|
436 lemma object_clean_fields_object_clean_slots [simp]: |
|
437 "object_clean_fields (object_clean_slots obj gs) gs = object_clean_slots (object_clean_fields obj gs) gs" |
|
438 by (clarsimp simp: object_clean_fields_def object_clean_slots_def |
|
439 clean_slots_def object_slots_def update_slots_def |
|
440 split: cdl_object.splits) |
|
441 |
|
442 lemma object_clean_idem [simp]: |
|
443 "object_clean (object_clean obj cmp) cmp = object_clean obj cmp" |
|
444 by (clarsimp simp: object_clean_def) |
|
445 |
|
446 lemma has_slots_object_clean_slots: |
|
447 "has_slots (object_clean_slots obj cmp) = has_slots obj" |
|
448 by (clarsimp simp: has_slots_def object_clean_slots_def update_slots_def split: cdl_object.splits) |
|
449 |
|
450 lemma has_slots_object_clean_fields: |
|
451 "has_slots (object_clean_fields obj cmp) = has_slots obj" |
|
452 by (clarsimp simp: has_slots_def object_clean_fields_def split: cdl_object.splits) |
|
453 |
|
454 lemma has_slots_object_clean: |
|
455 "has_slots (object_clean obj cmp) = has_slots obj" |
|
456 by (clarsimp simp: object_clean_def has_slots_object_clean_slots has_slots_object_clean_fields) |
|
457 |
|
458 lemma object_slots_update_slots_object_clean_fields [simp]: |
|
459 "object_slots (update_slots slots (object_clean_fields obj cmp)) = object_slots (update_slots slots obj)" |
|
460 apply (case_tac "has_slots obj") |
|
461 apply (clarsimp simp: has_slots_object_clean_fields)+ |
|
462 done |
|
463 |
|
464 lemma object_clean_fields_update_slots [simp]: |
|
465 "object_clean_fields (update_slots slots obj) cmp = update_slots slots (object_clean_fields obj cmp)" |
|
466 by (clarsimp simp: object_clean_fields_def update_slots_def split: cdl_object.splits) |
|
467 |
|
468 lemma object_clean_fields_twice [simp]: |
|
469 "(object_clean_fields (object_clean_fields obj cmp') cmp) = object_clean_fields obj (cmp \<inter> cmp')" |
|
470 by (clarsimp simp: object_clean_fields_def split: cdl_object.splits) |
|
471 |
|
472 lemma update_slots_object_clean_fields: |
|
473 "\<lbrakk>None \<notin> cmps; None \<notin> cmps'; object_type obj = object_type obj'\<rbrakk> |
|
474 \<Longrightarrow> update_slots slots (object_clean_fields obj cmps) = |
|
475 update_slots slots (object_clean_fields obj' cmps')" |
|
476 by (fastforce simp: update_slots_def object_clean_fields_def object_type_def split: cdl_object.splits) |
|
477 |
|
478 lemma object_clean_fields_no_slots: |
|
479 "\<lbrakk>None \<notin> cmps; None \<notin> cmps'; object_type obj = object_type obj'; \<not> has_slots obj; \<not> has_slots obj'\<rbrakk> |
|
480 \<Longrightarrow> object_clean_fields obj cmps = object_clean_fields obj' cmps'" |
|
481 by (fastforce simp: object_clean_fields_def object_type_def has_slots_def split: cdl_object.splits) |
|
482 |
|
483 lemma update_slots_object_clean: |
|
484 "\<lbrakk>None \<notin> cmps; None \<notin> cmps'; object_type obj = object_type obj'\<rbrakk> |
|
485 \<Longrightarrow> update_slots slots (object_clean obj cmps) = update_slots slots (object_clean obj' cmps')" |
|
486 apply (clarsimp simp: object_clean_def object_clean_slots_def) |
|
487 apply (erule (2) update_slots_object_clean_fields) |
|
488 done |
|
489 |
|
490 lemma cdl_heap_add_assoc': |
|
491 "\<forall>obj_id. not_conflicting_objects x z obj_id \<and> |
|
492 not_conflicting_objects y z obj_id \<and> |
|
493 not_conflicting_objects x z obj_id \<Longrightarrow> |
|
494 cdl_heap_add (SepState (cdl_heap_add x y) (cdl_ghost_state_add x y)) z = |
|
495 cdl_heap_add x (SepState (cdl_heap_add y z) (cdl_ghost_state_add y z))" |
|
496 apply (rule ext) |
|
497 apply (rename_tac obj_id) |
|
498 apply (erule_tac x=obj_id in allE) |
|
499 apply (clarsimp simp: cdl_heap_add_def cdl_ghost_state_add_def not_conflicting_objects_def) |
|
500 apply (simp add: Let_unfold split: option.splits) |
|
501 apply (rename_tac obj_y obj_x obj_z) |
|
502 apply (clarsimp simp: object_add_def clean_slots_def object_clean_def object_clean_slots_def Let_unfold) |
|
503 apply (case_tac "has_slots obj_z") |
|
504 apply (subgoal_tac "has_slots obj_y") |
|
505 apply (subgoal_tac "has_slots obj_x") |
|
506 apply ((clarsimp simp: has_slots_object_clean_fields has_slots_object_clean_slots has_slots_object_clean |
|
507 map_add_restrict union_intersection | |
|
508 drule inter_empty_not_both | |
|
509 erule update_slots_object_clean_fields | |
|
510 erule object_type_has_slots, simp | |
|
511 simp | safe)+)[3] |
|
512 apply (subgoal_tac "\<not> has_slots obj_y") |
|
513 apply (subgoal_tac "\<not> has_slots obj_x") |
|
514 apply ((clarsimp simp: has_slots_object_clean_fields has_slots_object_clean_slots has_slots_object_clean |
|
515 map_add_restrict union_intersection | |
|
516 drule inter_empty_not_both | |
|
517 erule object_clean_fields_no_slots | |
|
518 erule object_type_has_slots, simp | |
|
519 simp | safe)+) |
|
520 apply (fastforce simp: object_type_has_slots)+ |
|
521 done |
|
522 |
|
523 lemma cdl_heap_add_assoc: |
|
524 "\<lbrakk>sep_state_disj x y; sep_state_disj y z; sep_state_disj x z\<rbrakk> |
|
525 \<Longrightarrow> cdl_heap_add (SepState (cdl_heap_add x y) (cdl_ghost_state_add x y)) z = |
|
526 cdl_heap_add x (SepState (cdl_heap_add y z) (cdl_ghost_state_add y z))" |
|
527 apply (clarsimp simp: sep_state_disj_def) |
|
528 apply (cut_tac cdl_heap_add_assoc') |
|
529 apply fast |
|
530 apply fastforce |
|
531 done |
|
532 |
|
533 lemma cdl_ghost_state_add_assoc: |
|
534 "cdl_ghost_state_add (SepState (cdl_heap_add x y) (cdl_ghost_state_add x y)) z = |
|
535 cdl_ghost_state_add x (SepState (cdl_heap_add y z) (cdl_ghost_state_add y z))" |
|
536 apply (rule ext) |
|
537 apply (fastforce simp: cdl_heap_add_def cdl_ghost_state_add_def Let_unfold) |
|
538 done |
|
539 |
|
540 lemma clean_slots_map_add_comm: |
|
541 "cmps_a \<inter> cmps_b = {} |
|
542 \<Longrightarrow> clean_slots slots_a cmps_a ++ clean_slots slots_b cmps_b = |
|
543 clean_slots slots_b cmps_b ++ clean_slots slots_a cmps_a" |
|
544 apply (clarsimp simp: clean_slots_def) |
|
545 apply (drule the_set_inter_empty) |
|
546 apply (erule map_add_restrict_comm) |
|
547 done |
|
548 |
|
549 lemma object_clean_all: |
|
550 "object_type obj_a = object_type obj_b \<Longrightarrow> object_clean obj_b {} = object_clean obj_a {}" |
|
551 apply (clarsimp simp: object_clean_def object_clean_slots_def clean_slots_def the_set_def) |
|
552 apply (rule_tac cmps'1="{}" and obj'1="obj_a" in trans [OF update_slots_object_clean_fields], fastforce+) |
|
553 done |
|
554 |
|
555 lemma object_add_comm: |
|
556 "\<lbrakk>object_type obj_a = object_type obj_b; cmps_a \<inter> cmps_b = {}\<rbrakk> |
|
557 \<Longrightarrow> object_add obj_a obj_b cmps_a cmps_b = object_add obj_b obj_a cmps_b cmps_a" |
|
558 apply (clarsimp simp: object_add_def Let_unfold) |
|
559 apply (rule conjI | clarsimp)+ |
|
560 apply fastforce |
|
561 apply (rule conjI | clarsimp)+ |
|
562 apply (drule_tac slots_a = "object_slots obj_a" and slots_b = "object_slots obj_b" in clean_slots_map_add_comm) |
|
563 apply fastforce |
|
564 apply (rule conjI | clarsimp)+ |
|
565 apply (drule_tac slots_a = "object_slots obj_a" and slots_b = "object_slots obj_b" in clean_slots_map_add_comm) |
|
566 apply fastforce |
|
567 apply (rule conjI | clarsimp)+ |
|
568 apply (erule object_clean_all) |
|
569 apply (clarsimp) |
|
570 apply (rule_tac cmps'1=cmps_b and obj'1=obj_b in trans [OF update_slots_object_clean], assumption+) |
|
571 apply (drule_tac slots_a = "object_slots obj_a" and slots_b = "object_slots obj_b" in clean_slots_map_add_comm) |
|
572 apply fastforce |
|
573 done |
|
574 |
|
575 lemma sep_state_add_comm: |
|
576 "sep_state_disj x y \<Longrightarrow> sep_state_add x y = sep_state_add y x" |
|
577 apply (clarsimp simp: sep_state_add_def sep_state_disj_def) |
|
578 apply (rule conjI) |
|
579 apply (case_tac x, case_tac y, clarsimp) |
|
580 apply (rename_tac heap_a gs_a heap_b gs_b) |
|
581 apply (clarsimp simp: cdl_heap_add_def Let_unfold) |
|
582 apply (rule ext) |
|
583 apply (case_tac "heap_a obj_id") |
|
584 apply (case_tac "heap_b obj_id", simp_all add: slots_of_heap_def) |
|
585 apply (case_tac "heap_b obj_id", simp_all add: slots_of_heap_def) |
|
586 apply (rename_tac obj_a obj_b) |
|
587 apply (erule_tac x=obj_id in allE) |
|
588 apply (rule object_add_comm) |
|
589 apply (clarsimp simp: not_conflicting_objects_def) |
|
590 apply (clarsimp simp: not_conflicting_objects_def) |
|
591 apply (rule ext, fastforce simp: cdl_ghost_state_add_def Let_unfold Un_commute) |
|
592 done |
|
593 |
|
594 lemma add_to_slots_comm: |
|
595 "\<lbrakk>object_slots y_obj \<bottom> object_slots z_obj; update_slots empty y_obj = update_slots empty z_obj \<rbrakk> |
|
596 \<Longrightarrow> add_to_slots (object_slots z_obj) y_obj = add_to_slots (object_slots y_obj) z_obj" |
|
597 by (fastforce simp: add_to_slots_def update_slots_def object_slots_def |
|
598 cdl_tcb.splits cdl_cnode.splits |
|
599 dest!: map_add_com |
|
600 split: cdl_object.splits) |
|
601 |
|
602 lemma cdl_heap_add_none1: |
|
603 "cdl_heap_add x y obj_id = None \<Longrightarrow> (sep_heap x) obj_id = None" |
|
604 by (clarsimp simp: cdl_heap_add_def Let_unfold split:option.splits split_if_asm) |
|
605 |
|
606 lemma cdl_heap_add_none2: |
|
607 "cdl_heap_add x y obj_id = None \<Longrightarrow> (sep_heap y) obj_id = None" |
|
608 by (clarsimp simp: cdl_heap_add_def Let_unfold split:option.splits split_if_asm) |
|
609 |
|
610 lemma object_type_object_addL: |
|
611 "object_type obj = object_type obj' |
|
612 \<Longrightarrow> object_type (object_add obj obj' cmp cmp') = object_type obj" |
|
613 by (clarsimp simp: object_add_def Let_unfold) |
|
614 |
|
615 lemma object_type_object_addR: |
|
616 "object_type obj = object_type obj' |
|
617 \<Longrightarrow> object_type (object_add obj obj' cmp cmp') = object_type obj'" |
|
618 by (clarsimp simp: object_add_def Let_unfold) |
|
619 |
|
620 lemma sep_state_add_disjL: |
|
621 "\<lbrakk>sep_state_disj y z; sep_state_disj x (sep_state_add y z)\<rbrakk> \<Longrightarrow> sep_state_disj x y" |
|
622 apply (clarsimp simp: sep_state_disj_def sep_state_add_def) |
|
623 apply (rename_tac obj_id) |
|
624 apply (clarsimp simp: not_conflicting_objects_def) |
|
625 apply (erule_tac x=obj_id in allE)+ |
|
626 apply (fastforce simp: cdl_heap_add_def cdl_ghost_state_add_def object_type_object_addR |
|
627 split: option.splits) |
|
628 done |
|
629 |
|
630 lemma sep_state_add_disjR: |
|
631 "\<lbrakk>sep_state_disj y z; sep_state_disj x (sep_state_add y z)\<rbrakk> \<Longrightarrow> sep_state_disj x z" |
|
632 apply (clarsimp simp: sep_state_disj_def sep_state_add_def) |
|
633 apply (rename_tac obj_id) |
|
634 apply (clarsimp simp: not_conflicting_objects_def) |
|
635 apply (erule_tac x=obj_id in allE)+ |
|
636 apply (fastforce simp: cdl_heap_add_def cdl_ghost_state_add_def object_type_object_addR |
|
637 split: option.splits) |
|
638 done |
|
639 |
|
640 lemma sep_state_add_disj: |
|
641 "\<lbrakk>sep_state_disj y z; sep_state_disj x y; sep_state_disj x z\<rbrakk> \<Longrightarrow> sep_state_disj x (sep_state_add y z)" |
|
642 apply (clarsimp simp: sep_state_disj_def sep_state_add_def) |
|
643 apply (rename_tac obj_id) |
|
644 apply (clarsimp simp: not_conflicting_objects_def) |
|
645 apply (erule_tac x=obj_id in allE)+ |
|
646 apply (fastforce simp: cdl_heap_add_def cdl_ghost_state_add_def object_type_object_addR |
|
647 split: option.splits) |
|
648 done |
|
649 |
|
650 |
|
651 |
|
652 |
|
653 (*********************************************) |
|
654 (* Definition of separation logic for capDL. *) |
|
655 (*********************************************) |
|
656 |
|
657 instantiation "sep_state" :: zero |
|
658 begin |
|
659 definition "0 \<equiv> SepState empty (\<lambda>obj_id. {})" |
|
660 instance .. |
|
661 end |
|
662 |
|
663 instantiation "sep_state" :: stronger_sep_algebra |
|
664 begin |
|
665 |
|
666 definition "(op ##) \<equiv> sep_state_disj" |
|
667 definition "(op +) \<equiv> sep_state_add" |
|
668 |
|
669 |
|
670 |
|
671 (********************************************** |
|
672 * The proof that this is a separation logic. * |
|
673 **********************************************) |
|
674 |
|
675 instance |
|
676 apply default |
|
677 (* x ## 0 *) |
|
678 apply (simp add: sep_disj_sep_state_def sep_state_disj_def zero_sep_state_def) |
|
679 (* x ## y \<Longrightarrow> y ## x *) |
|
680 apply (clarsimp simp: not_conflicting_objects_comm sep_disj_sep_state_def sep_state_disj_def Let_unfold |
|
681 map_disj_com not_conflicting_objects_comm Int_commute) |
|
682 (* x + 0 = x *) |
|
683 apply (simp add: plus_sep_state_def sep_state_add_def zero_sep_state_def) |
|
684 apply (case_tac x) |
|
685 apply (clarsimp simp: cdl_heap_add_def) |
|
686 apply (rule ext) |
|
687 apply (clarsimp simp: cdl_ghost_state_add_def split:split_if_asm) |
|
688 (* x ## y \<Longrightarrow> x + y = y + x *) |
|
689 apply (clarsimp simp: plus_sep_state_def sep_disj_sep_state_def) |
|
690 apply (erule sep_state_add_comm) |
|
691 (* (x + y) + z = x + (y + z) *) |
|
692 apply (simp add: plus_sep_state_def sep_state_add_def) |
|
693 apply (rule conjI) |
|
694 apply (clarsimp simp: sep_disj_sep_state_def) |
|
695 apply (erule (2) cdl_heap_add_assoc) |
|
696 apply (rule cdl_ghost_state_add_assoc) |
|
697 (* x ## y + z = (x ## y \<and> x ## z) *) |
|
698 apply (clarsimp simp: plus_sep_state_def sep_disj_sep_state_def) |
|
699 apply (rule iffI) |
|
700 (* x ## y + z \<Longrightarrow> (x ## y \<and> x ## z) *) |
|
701 apply (rule conjI) |
|
702 (* x ## y + z \<Longrightarrow> (x ## y) *) |
|
703 apply (erule (1) sep_state_add_disjL) |
|
704 (* x ## y + z \<Longrightarrow> (x ## z) *) |
|
705 apply (erule (1) sep_state_add_disjR) |
|
706 (* x ## y + z \<Longleftarrow> (x ## y \<and> x ## z) *) |
|
707 apply clarsimp |
|
708 apply (erule (2) sep_state_add_disj) |
|
709 done |
|
710 |
|
711 end |
|
712 |
|
713 |
|
714 end |