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