1(* 2 * Copyright 2014, NICTA 3 * 4 * This software may be distributed and modified according to the terms of 5 * the GNU General Public License version 2. Note that NO WARRANTY is provided. 6 * See "LICENSE_GPLv2.txt" for details. 7 * 8 * @TAG(NICTA_GPL) 9 *) 10 11(* 12 * Well formed constraints of what capDL specifications the system-initialiser can initialise. 13 * 14 * There are two types of constraints: 15 * - fundamental ones (such as that specs must be finite), 16 * and other seL4 limitations (such as that page tables can't be shared). 17 * - limitations of the initialiser. 18 * 19 * The latter are commented with LIMITATION. 20 *) 21 22theory WellFormed_SI 23imports 24 "DSpecProofs.Kernel_DP" 25 "SepDSpec.Separation_SD" 26 "Lib.SimpStrategy" 27begin 28 29context begin interpretation Arch . (*FIXME: arch_split*) 30 31lemma cap_has_object_NullCap [simp]: 32 "\<not>cap_has_object NullCap" 33 by (clarsimp simp: cap_has_object_def) 34 35lemma cap_has_object_not_NullCap: 36 "cap_has_object cap \<Longrightarrow> cap \<noteq> NullCap" 37 by clarsimp 38 39lemma is_irqhandler_cap_not_NullCap: 40 "is_irqhandler_cap cap \<Longrightarrow> cap \<noteq> NullCap" 41 by clarsimp 42 43lemma cap_has_object_not_irqhandler_cap: 44 "cap_has_object cap \<Longrightarrow> \<not> is_irqhandler_cap cap" 45 by (clarsimp simp: cap_has_object_def cap_type_def 46 split: cdl_cap.splits) 47 48lemmas cap_has_object_not_irqhandler_cap_simp[simp] = cap_has_object_not_irqhandler_cap[OF ByAssum] 49lemmas cap_has_object_not_NullCap_simp[simp] = cap_has_object_not_NullCap[OF ByAssum] 50lemmas is_irqhandler_cap_not_NullCap_simp[simp] = is_irqhandler_cap_not_NullCap[OF ByAssum] 51 52 53 54 55 56 57 58definition 59 cap_ref_object :: "cdl_cap_ref \<Rightarrow> cdl_state \<Rightarrow> cdl_object_id" 60where 61 "cap_ref_object cap_ref s \<equiv> cap_object (the (opt_cap cap_ref s))" 62 63definition 64 cap_ref_irq :: "cdl_cap_ref \<Rightarrow> cdl_state \<Rightarrow> cdl_irq" 65where 66 "cap_ref_irq cap_ref s \<equiv> cap_irq (the (opt_cap cap_ref s))" 67 68definition real_cap_ref :: "cdl_cap_ref \<Rightarrow> cdl_state \<Rightarrow> bool" 69where 70 "real_cap_ref cap_ref s \<equiv> \<exists>cap. opt_cap cap_ref s = Some cap \<and> cap \<noteq> NullCap \<and> 71 cnode_at (fst cap_ref) s" 72 73definition object_cap_ref :: "cdl_cap_ref \<Rightarrow> cdl_state \<Rightarrow> bool" 74where 75 "object_cap_ref cap_ref s \<equiv> \<exists>cap. opt_cap cap_ref s = Some cap \<and> 76 cap_has_object cap \<and> 77 cnode_at (fst cap_ref) s" 78 79(* MOVE ME *) 80definition "guard_bits = (18::nat)" 81 82lemma guard_less_guard_bits: 83 "\<lbrakk>guard_size < guard_bits; (g::word32) < 2 ^ guard_size\<rbrakk> \<Longrightarrow> 84 g < 2 ^ guard_bits" 85 apply (erule less_le_trans) 86 apply (rule two_power_increasing, simp) 87 apply (clarsimp simp: guard_bits_def) 88 done 89 90lemma guard_size_shiftl_non_zero: 91 "\<lbrakk>guard_size < guard_bits; guard_size \<noteq> 0\<rbrakk> \<Longrightarrow> 92 ((of_nat guard_size)::word32) << 3 \<noteq> 0" 93 apply (rule word_shift_nonzero [where m=guard_bits]) 94 apply clarsimp 95 apply (rule order_less_imp_le) 96 apply (rule guard_less_guard_bits, assumption) 97 apply (insert n_less_equal_power_2 [where n=guard_size]) 98 apply clarsimp 99 apply (rule of_nat_n_less_equal_power_2) 100 apply (clarsimp simp: guard_bits_def) 101 apply (clarsimp simp: guard_bits_def) 102 apply (clarsimp simp: of_nat_0) 103 apply (drule of_nat_0) 104 apply (erule less_le_trans) 105 apply (clarsimp simp: guard_bits_def word_bits_def) 106 apply clarsimp 107 done 108 109(* End of MOVE ME 110 *) 111definition well_formed_cap :: "cdl_cap \<Rightarrow> bool" 112where 113 "well_formed_cap cap \<equiv> (case cap of 114 EndpointCap _ b _ \<Rightarrow> b < 2 ^ badge_bits 115 | NotificationCap _ b r \<Rightarrow> (b < 2 ^ badge_bits) \<and> (r \<subseteq> {AllowRead, AllowWrite}) 116 | CNodeCap _ g gs sz \<Rightarrow> (gs < guard_bits) \<and> (g < 2 ^ gs) \<and> (sz + gs \<le> 32) 117 | TcbCap _ \<Rightarrow> True 118 | FrameCap _ _ r _ _ ad \<Rightarrow> r \<in> {vm_read_write, vm_read_only} \<and> ad = None 119 | PageTableCap _ _ ad \<Rightarrow> ad = None 120 | PageDirectoryCap _ _ ad \<Rightarrow> ad = None 121 | IrqHandlerCap _ \<Rightarrow> True 122(* LIMITATION: The following should probably eventually be true. *) 123 | IrqControlCap \<Rightarrow> False 124 | UntypedCap _ _ _ \<Rightarrow> False 125 | AsidControlCap \<Rightarrow> False 126 | AsidPoolCap _ _ \<Rightarrow> False 127 | _ \<Rightarrow> False)" 128 129(* LIMITATION: The specification cannot contain ASID numbers. *) 130definition vm_cap_has_asid :: "cdl_cap \<Rightarrow> bool" 131where 132 "vm_cap_has_asid cap \<equiv> 133 (case cap of 134 FrameCap _ _ _ _ _ ad \<Rightarrow> ad \<noteq> None 135 | PageTableCap _ _ ad \<Rightarrow> ad \<noteq> None 136 | PageDirectoryCap _ _ ad \<Rightarrow> ad \<noteq> None 137 | _ \<Rightarrow> False)" 138 139definition is_real_vm_cap :: "cdl_cap \<Rightarrow> bool" 140where 141 "is_real_vm_cap cap \<equiv> 142 (case cap of 143 FrameCap _ _ _ _ Real _ \<Rightarrow> True 144 | PageTableCap _ Real _ \<Rightarrow> True 145 | PageDirectoryCap _ Real _ \<Rightarrow> True 146 | _ \<Rightarrow> False)" 147 148definition is_fake_vm_cap :: "cdl_cap \<Rightarrow> bool" 149where 150 "is_fake_vm_cap cap \<equiv> 151 (case cap of 152 FrameCap _ _ _ _ Fake _ \<Rightarrow> True 153 | PageTableCap _ Fake _ \<Rightarrow> True 154 | PageDirectoryCap _ Fake _ \<Rightarrow> True 155 | _ \<Rightarrow> False)" 156 157(* Original caps must have default rights, 158 * and original endpoint + notification caps must not be badged. 159 *) 160definition 161 is_copyable_cap :: "cdl_cap \<Rightarrow> bool" 162where 163 "is_copyable_cap cap \<equiv> \<not> is_irqhandler_cap cap" 164 165definition 166 well_formed_orig_cap :: "cdl_cap \<Rightarrow> bool" 167where 168 "well_formed_orig_cap cap \<equiv> 169 (cap_has_type cap \<longrightarrow> cap_rights (default_cap (the (cap_type cap)) undefined undefined undefined) 170 = cap_rights cap) \<and> 171 (ep_related_cap cap \<longrightarrow> cap_badge cap = 0)" 172 173definition 174 well_formed_cdt :: "cdl_state \<Rightarrow> cdl_cap_ref \<Rightarrow> cdl_cap \<Rightarrow> bool" 175where 176 "well_formed_cdt spec cap_ref cap \<equiv> 177 cnode_at (fst cap_ref) spec \<longrightarrow> 178 cap_has_object cap \<longrightarrow> 179 (\<exists>orig_obj_id orig_slot orig_cap. 180 cnode_at orig_obj_id spec \<and> 181 (\<exists>obj. opt_object (cap_object cap) spec = Some obj) \<and> 182 original_cap_at (orig_obj_id, orig_slot) spec \<and> 183 opt_cap (orig_obj_id, orig_slot) spec = Some orig_cap \<and> 184 cap_has_object orig_cap \<and> cap_object orig_cap = cap_object cap)" 185 186(* MOVEME *) 187lemma well_formed_cdt_irqhandler_cap: 188 "is_irqhandler_cap cap \<Longrightarrow> well_formed_cdt spec cap_ref cap" 189 by (clarsimp simp: well_formed_cdt_def split: cdl_cap.splits) 190 191 192(* The only thing that points to IRQ objects is the IRQ table (not a cap). *) 193definition 194 well_formed_cap_to_real_object :: "cdl_state \<Rightarrow> cdl_cap \<Rightarrow> bool" 195where 196 "well_formed_cap_to_real_object spec cap \<equiv> 197 cap_has_object cap \<longrightarrow> real_object_at (cap_object cap) spec" 198 199definition 200 well_formed_cap_types_match :: "cdl_state \<Rightarrow> cdl_cap \<Rightarrow> bool" 201where 202 "well_formed_cap_types_match spec cap \<equiv> 203 (cap_has_object cap \<longrightarrow> 204 (\<exists>cap_obj. cdl_objects spec (cap_object cap) = Some cap_obj \<and> 205 cap_type cap = Some (object_type cap_obj))) \<and> 206 (is_irqhandler_cap cap \<longrightarrow> 207 (\<exists>cap_obj. cdl_objects spec (cdl_irq_node spec (cap_irq cap)) = Some cap_obj \<and> 208 cap_type cap = Some (object_type cap_obj)))" 209 210definition well_formed_caps :: "cdl_state \<Rightarrow> cdl_object_id \<Rightarrow> cdl_object \<Rightarrow> bool" 211where 212 "well_formed_caps spec obj_id obj \<equiv> \<forall>slot cap. 213 object_slots obj slot = Some cap \<longrightarrow> 214 cap \<noteq> NullCap \<longrightarrow> 215 (well_formed_cap cap \<and> 216 (original_cap_at (obj_id, slot) spec \<longrightarrow> well_formed_orig_cap cap) \<and> 217 (\<not>original_cap_at (obj_id, slot) spec \<longrightarrow> is_copyable_cap cap) \<and> 218 well_formed_cdt spec (obj_id, slot) cap \<and> 219 well_formed_cap_to_real_object spec cap \<and> 220 well_formed_cap_types_match spec cap \<and> 221 ((is_cnode obj \<or> is_tcb obj) \<longrightarrow> (\<not> is_fake_vm_cap cap)))" 222 223definition 224 well_formed_cap_to_object :: "cdl_state \<Rightarrow> cdl_object_id \<Rightarrow> cdl_object \<Rightarrow> bool" 225where 226 "well_formed_cap_to_object spec obj_id obj \<equiv> (\<exists>cnode_id slot cap. 227 opt_cap (cnode_id, slot) spec = Some cap \<and> 228 original_cap_at (cnode_id, slot) spec \<and> 229 cnode_at cnode_id spec \<and> 230 (real_object_at obj_id spec \<longrightarrow> cap_object cap = obj_id \<and> cap_has_object cap) \<and> 231 (\<not>real_object_at obj_id spec \<longrightarrow> is_irqhandler_cap cap \<and> cdl_irq_node spec (cap_irq cap) = obj_id)) \<and> 232 233 (\<forall>slot cap. (opt_cap slot spec = Some cap \<and> is_cnode_cap cap \<and> cap_object cap = obj_id) 234 \<longrightarrow> object_size_bits obj = cnode_cap_size cap)" 235 236(* For every IRQ object that has a cap in it, 237 * there should be an IRQ handler cap to that object. 238 * There can be more IRQ handler caps than this, 239 * but every object must have a cap to it. 240 *) 241definition 242 well_formed_irqhandler_caps :: "cdl_state \<Rightarrow> bool" 243where 244 "well_formed_irqhandler_caps spec \<equiv> (\<forall>irq. irq \<in> bound_irqs spec \<longrightarrow> 245 (\<exists>cnode_id slot cap. opt_cap (cnode_id, slot) spec = Some cap \<and> 246 is_irqhandler_cap cap \<and> 247 cap_irq cap = irq))" 248 249definition 250 well_formed_orig_caps_unique :: "cdl_state \<Rightarrow> bool" 251where 252 "well_formed_orig_caps_unique spec \<equiv> \<forall>obj_id obj_id' slot slot' cap cap'. 253 cnode_at obj_id spec \<longrightarrow> 254 cnode_at obj_id' spec \<longrightarrow> 255 cap_has_object cap \<longrightarrow> 256 cap_has_object cap' \<longrightarrow> 257 opt_cap (obj_id, slot) spec = Some cap \<longrightarrow> 258 opt_cap (obj_id', slot') spec = Some cap' \<longrightarrow> 259 cap \<noteq> NullCap \<longrightarrow> original_cap_at (obj_id, slot) spec \<longrightarrow> 260 cap' \<noteq> NullCap \<longrightarrow> original_cap_at (obj_id', slot') spec \<longrightarrow> 261 cap_object cap = cap_object cap' \<longrightarrow> 262 (obj_id = obj_id' \<and> slot = slot')" 263 264definition 265 well_formed_irqhandler_caps_unique :: "cdl_state \<Rightarrow> bool" 266where 267 "well_formed_irqhandler_caps_unique spec \<equiv> \<forall>obj_id obj_id' slot slot' cap cap'. 268 opt_cap (obj_id, slot) spec = Some cap \<longrightarrow> 269 opt_cap (obj_id', slot') spec = Some cap' \<longrightarrow> 270 is_irqhandler_cap cap \<longrightarrow> 271 is_irqhandler_cap cap' \<longrightarrow> 272 cap_irq cap = cap_irq cap' \<longrightarrow> 273 (obj_id = obj_id' \<and> slot = slot')" 274 275definition well_formed_tcb :: "cdl_state \<Rightarrow> cdl_object_id \<Rightarrow> cdl_object \<Rightarrow> bool" 276where 277 "well_formed_tcb spec obj_id obj \<equiv> 278 is_tcb obj \<longrightarrow> 279 \<not> tcb_has_fault obj \<and> 280 tcb_domain obj = minBound \<and> 281 (\<forall>slot cap. object_slots obj slot = Some cap \<longrightarrow> 282 ((slot = tcb_cspace_slot \<longrightarrow> is_cnode_cap cap \<and> 283 cap_guard_size cap \<noteq> 0 \<and> 284 cap_object cap \<notin> irq_nodes spec) \<and> 285 (slot = tcb_vspace_slot \<longrightarrow> is_pd_cap cap) \<and> 286 (slot = tcb_ipcbuffer_slot \<longrightarrow> is_frame_cap cap \<and> is_default_cap cap) \<and> 287 (slot = tcb_replycap_slot \<longrightarrow> cap = NullCap \<or> cap = MasterReplyCap obj_id) \<and> 288 (slot = tcb_caller_slot \<longrightarrow> cap = NullCap) \<and> 289 (slot = tcb_pending_op_slot \<longrightarrow> cap = NullCap \<or> cap = RestartCap) \<and> 290 (slot = tcb_boundntfn_slot \<longrightarrow> cap = NullCap) )) \<and> 291 ((object_slots obj tcb_replycap_slot = Some (MasterReplyCap obj_id)) = 292 (object_slots obj tcb_pending_op_slot = Some RestartCap))" 293 294definition 295 well_formed_fake_pt_caps_unique :: "cdl_state \<Rightarrow> bool" 296where 297 "well_formed_fake_pt_caps_unique spec \<equiv> \<forall>obj_id obj_id' slot slot' cap cap'. 298 pd_at obj_id spec \<longrightarrow> 299 pd_at obj_id' spec \<longrightarrow> 300 opt_cap (obj_id, slot) spec = Some cap \<longrightarrow> 301 opt_cap (obj_id', slot') spec = Some cap' \<longrightarrow> 302 cap \<noteq> NullCap \<longrightarrow> is_fake_pt_cap cap \<longrightarrow> 303 cap' \<noteq> NullCap \<longrightarrow> is_fake_pt_cap cap' \<longrightarrow> 304 cap_object cap = cap_object cap' \<longrightarrow> (obj_id = obj_id' \<and> slot = slot')" 305 306definition 307 well_formed_cap_to_non_empty_pt :: "cdl_state \<Rightarrow> cdl_object_id \<Rightarrow> cdl_object \<Rightarrow> bool" 308where 309 "well_formed_cap_to_non_empty_pt spec obj_id obj \<equiv> 310 pt_at obj_id spec \<longrightarrow> 311 object_default_state obj \<noteq> obj \<longrightarrow> 312 (\<exists>pd_id slot cap. 313 opt_cap (pd_id, slot) spec = Some cap \<and> 314 pd_at pd_id spec \<and> 315 cap_object cap = obj_id \<and> 316 cap_has_object cap)" 317 318definition well_formed_vspace :: "cdl_state \<Rightarrow> cdl_object_id \<Rightarrow> cdl_object \<Rightarrow> bool" 319where 320 "well_formed_vspace spec obj_id obj \<equiv> 321 well_formed_cap_to_non_empty_pt spec obj_id obj \<and> 322 (\<forall>slot cap. 323 (is_pt obj \<longrightarrow> 324 object_slots obj slot = Some cap \<longrightarrow> 325 cap \<noteq> NullCap \<longrightarrow> (\<exists>sz. cap_type cap = Some (FrameType sz) \<and> (sz = 12 \<or> sz = 16) \<and> is_fake_vm_cap cap) 326 ) \<and> 327 (is_pd obj \<longrightarrow> 328 object_slots obj slot = Some cap \<longrightarrow> 329 cap \<noteq> NullCap \<longrightarrow> 330 (is_fake_pt_cap cap \<or> 331 (\<exists>sz. cap_type cap = Some (FrameType sz) \<and> (sz = 20 \<or> sz = 24) \<and> is_fake_vm_cap cap) )))" 332 333(* LIMITATION: The caps in a IRQ Node must have full permissions and be unbadged. *) 334definition well_formed_irq_node :: "cdl_state \<Rightarrow> cdl_object_id \<Rightarrow> cdl_object \<Rightarrow> bool" 335where 336 "well_formed_irq_node spec obj_id obj \<equiv> \<forall>slot cap. 337 obj_id \<in> irq_nodes spec \<longrightarrow> 338 dom (object_slots obj) = {0} \<and> 339 (object_slots obj slot = Some cap \<longrightarrow> 340 (cap \<noteq> NullCap \<longrightarrow> (is_ntfn_cap cap \<and> is_default_cap cap)))" 341 342definition well_formed_irq_table :: "cdl_state \<Rightarrow> bool" 343where 344 "well_formed_irq_table spec \<equiv> inj (cdl_irq_node spec) \<and> 345 irq_nodes spec = {obj_id. \<exists>irq. cdl_irq_node spec irq = obj_id \<and> 346 obj_id \<in> dom (cdl_objects spec)}" 347 348definition 349 well_formed :: "cdl_state \<Rightarrow> bool" 350where 351 "well_formed spec \<equiv> well_formed_orig_caps_unique spec \<and> 352 well_formed_irqhandler_caps_unique spec \<and> 353 well_formed_fake_pt_caps_unique spec \<and> 354 well_formed_irqhandler_caps spec \<and> 355 well_formed_irq_table spec \<and> 356 (\<forall>obj_id. 357 case cdl_objects spec obj_id of 358 Some obj \<Rightarrow> well_formed_caps spec obj_id obj \<and> 359 well_formed_cap_to_object spec obj_id obj \<and> 360 well_formed_tcb spec obj_id obj \<and> 361 well_formed_vspace spec obj_id obj \<and> 362 well_formed_irq_node spec obj_id obj \<and> 363 object_size_bits obj < word_bits \<and> 364 object_size_bits (object_default_state obj) = object_size_bits obj \<and> 365 dom (object_slots (object_default_state obj)) = dom (object_slots obj) \<and> 366 (cnode_at obj_id spec \<longrightarrow> 0 < object_size_bits obj) 367 | None \<Rightarrow> True) 368 \<and> (\<forall>slot. \<not> cap_at (\<lambda>c. is_device_cap c = True) slot spec)" 369 370lemma dom_cap_map [simp]: 371 "dom (\<lambda>n. if n \<le> N then Some a else None) = {0::nat .. N}" 372 by (rule, clarsimp simp: dom_def)+ 373 374lemma dom_cap_map' [simp]: 375 "dom (\<lambda>n. if n < N then Some a else None) = {0::nat ..< N}" 376 by (rule, clarsimp simp: dom_def)+ 377 378(******************************* 379 * Rules about well_formed_cap. * 380 *******************************) 381 382lemma well_formed_cap_cap_has_object_eq: 383 "\<lbrakk>well_formed_cap cap; cap_has_object cap; cap_type cap = cap_type cap'\<rbrakk> \<Longrightarrow> cap_has_object cap'" 384 by (clarsimp simp: well_formed_cap_def cap_type_def cap_has_object_def split: cdl_cap.splits)+ 385 386lemma well_formed_cap_update_cap_objects [simp]: 387 "is_untyped_cap cap 388 \<Longrightarrow> well_formed_cap (update_cap_objects x cap) = well_formed_cap cap" 389 apply (clarsimp simp: update_cap_object_def 390 update_cap_objects_def well_formed_cap_def) 391 apply (cases cap, simp_all) 392 done 393 394lemma well_formed_cap_update_cap_object [simp]: 395 "well_formed_cap (update_cap_object x cap) = well_formed_cap cap" 396 apply (clarsimp simp: update_cap_object_def well_formed_cap_def) 397 apply (cases cap, simp_all add:is_default_cap_def cap_type_def cap_badge_def default_cap_def) 398 done 399 400lemma cap_rights_inter_default_cap_rights: 401 "\<lbrakk>well_formed_cap cap; cap_type cap = Some type\<rbrakk> 402 \<Longrightarrow> cap_rights (default_cap type ids sz dev) \<inter> cap_rights cap 403 = cap_rights cap" 404 by (fastforce simp: well_formed_cap_def default_cap_def cap_type_def cap_rights_def 405 validate_vm_rights_def vm_read_write_def 406 vm_kernel_only_def vm_read_only_def 407 split: cdl_cap.splits cdl_object_type.splits) 408 409lemma well_formed_cap_derived_cap [simp]: 410 "\<lbrakk>well_formed_cap cap; \<not> vm_cap_has_asid cap\<rbrakk> \<Longrightarrow> derived_cap cap = cap" 411 by (clarsimp simp: well_formed_cap_def vm_cap_has_asid_def derived_cap_def not_Some_eq_tuple 412 split: cdl_cap.splits) 413 414(********************************* 415 * Rules about well_formed spec. * 416 *********************************) 417lemma dom_if_0 [simp]: 418 "dom (\<lambda>a. if a = 0 then Some b else None) = {0}" 419 by (auto split: if_split_asm) 420 421lemma well_formed_finite [elim!]: 422 "well_formed spec \<Longrightarrow> finite (dom (slots_of obj_id spec))" 423 apply (clarsimp simp: well_formed_def) 424 apply (erule_tac x=obj_id in allE) 425 apply (clarsimp simp: opt_object_def slots_of_def split: option.splits) 426 apply (rename_tac obj) 427 apply (drule_tac t="dom (object_slots obj)" in sym) (* Makes rewriting work. *) 428 apply (clarsimp simp: object_default_state_def2 object_slots_def 429 default_tcb_def tcb_pending_op_slot_def 430 empty_cnode_def empty_irq_node_def empty_cap_map_def 431 split: cdl_object.splits) 432 done 433 434lemma well_formed_finite_object_slots: 435 "\<lbrakk>well_formed spec; cdl_objects spec obj_id = Some obj\<rbrakk> \<Longrightarrow> finite (dom (object_slots obj))" 436 apply (drule well_formed_finite [where obj_id=obj_id]) 437 apply (clarsimp simp: slots_of_def opt_object_def) 438 done 439 440lemma well_formed_distinct_slots_of_list [elim!]: 441 "well_formed spec \<Longrightarrow> distinct (slots_of_list spec obj_id)" 442 apply (drule_tac obj_id=obj_id in well_formed_finite) 443 apply (clarsimp simp: slots_of_list_def) 444 done 445 446lemma well_formed_object_size_bits: 447 "\<lbrakk>well_formed spec; cdl_objects spec obj_id = Some obj\<rbrakk> 448 \<Longrightarrow> object_size_bits (object_default_state obj) = object_size_bits obj" 449 apply (clarsimp simp: well_formed_def) 450 apply (erule_tac x=obj_id in allE) 451 apply (clarsimp) 452 done 453 454lemma well_formed_well_formed_caps: 455 "\<lbrakk>well_formed spec; cdl_objects spec obj_id = Some obj\<rbrakk> 456 \<Longrightarrow> well_formed_caps spec obj_id obj" 457 by (clarsimp simp: well_formed_def split: option.splits) 458 459lemma well_formed_well_formed_cap: 460 "\<lbrakk>well_formed spec; cdl_objects spec obj_id = Some obj; 461 object_slots obj slot = Some cap; cap \<noteq> NullCap\<rbrakk> 462 \<Longrightarrow> well_formed_cap cap" 463 apply (clarsimp simp: well_formed_def) 464 apply (erule_tac x=obj_id in allE) 465 apply (clarsimp simp: well_formed_caps_def) 466 done 467 468lemma well_formed_well_formed_cap': 469 "\<lbrakk>well_formed spec; opt_cap (obj_id, slot) spec = Some cap; cap \<noteq> NullCap\<rbrakk> \<Longrightarrow> 470 well_formed_cap cap" 471 apply (frule opt_cap_dom_cdl_objects) 472 apply clarsimp 473 apply (frule (1) object_slots_opt_cap, simp) 474 apply (erule (3) well_formed_well_formed_cap) 475 done 476 477lemma well_formed_well_formed_cap_to_object: 478 "\<lbrakk>well_formed spec; cdl_objects spec obj_id = Some obj\<rbrakk> 479 \<Longrightarrow> well_formed_cap_to_object spec obj_id obj" 480 by (clarsimp simp: well_formed_def split: option.splits) 481 482lemma well_formed_well_formed_cap_to_real_object: 483 "\<lbrakk>well_formed spec; cdl_objects spec obj_id = Some obj; 484 object_slots obj slot = Some cap; cap \<noteq> NullCap\<rbrakk> 485 \<Longrightarrow> well_formed_cap_to_real_object spec cap" 486 apply (clarsimp simp: well_formed_def) 487 apply (erule_tac x=obj_id in allE) 488 apply (clarsimp simp: well_formed_caps_def) 489 done 490 491lemma well_formed_well_formed_cap_to_real_object': 492 "\<lbrakk>well_formed spec; opt_cap cap_ref spec = Some cap; cap \<noteq> NullCap\<rbrakk> \<Longrightarrow> 493 well_formed_cap_to_real_object spec cap" 494 apply (frule opt_cap_dom_cdl_objects) 495 apply (clarsimp split: prod.splits) 496 apply (frule (1) object_slots_opt_capD) 497 apply (erule (3) well_formed_well_formed_cap_to_real_object) 498 done 499 500lemma well_formed_well_formed_cap_types_match: 501 "\<lbrakk>well_formed spec; cdl_objects spec obj_id = Some obj; 502 object_slots obj slot = Some cap; cap \<noteq> NullCap\<rbrakk> 503 \<Longrightarrow> well_formed_cap_types_match spec cap" 504 apply (clarsimp simp: well_formed_def) 505 apply (erule_tac x=obj_id in allE) 506 apply (clarsimp simp: well_formed_caps_def) 507 done 508 509lemma well_formed_well_formed_cap_types_match': 510 "\<lbrakk>well_formed spec; opt_cap cap_ref spec = Some cap; cap \<noteq> NullCap\<rbrakk> \<Longrightarrow> 511 well_formed_cap_types_match spec cap" 512 apply (frule opt_cap_dom_cdl_objects) 513 apply (clarsimp) 514 apply (frule (1) object_slots_opt_capD) 515 apply (erule (3) well_formed_well_formed_cap_types_match) 516 done 517 518lemma well_formed_cap_object_is_real: 519 "\<lbrakk>well_formed spec; opt_cap slot spec = Some cap; cap_has_object cap\<rbrakk> 520 \<Longrightarrow> real_object_at (cap_object cap) spec" 521 apply (drule (1) well_formed_well_formed_cap_to_real_object', simp) 522 apply (clarsimp simp: well_formed_cap_to_real_object_def) 523 done 524 525lemma well_formed_types_match: 526 "\<lbrakk>well_formed spec; opt_cap (obj_id, slot) spec = Some cap; 527 cdl_objects spec (cap_object cap) = Some cap_obj; cap_has_object cap\<rbrakk> 528 \<Longrightarrow> Some (object_type cap_obj) = cap_type cap" 529 apply (frule cap_has_object_not_NullCap) 530 apply (clarsimp simp: well_formed_def) 531 apply (erule_tac x=obj_id in allE) 532 apply (clarsimp simp: opt_cap_def opt_object_def slots_of_def) 533 apply (clarsimp split: option.splits) 534 apply (rename_tac obj) 535 apply (clarsimp simp: well_formed_caps_def well_formed_cap_types_match_def) 536 apply (erule_tac x=slot in allE) 537 apply (clarsimp) 538 done 539 540lemma well_formed_object_slots: 541 "\<lbrakk>well_formed spec; cdl_objects spec obj_id = Some obj\<rbrakk> 542 \<Longrightarrow> dom (object_slots obj) = dom (object_slots (object_default_state obj))" 543 apply (clarsimp simp: well_formed_def) 544 apply (erule allE [where x=obj_id]) 545 apply simp 546 done 547 548lemma well_formed_slot_object_size_bits: 549 "\<lbrakk>well_formed spec; opt_cap (obj_id, slot) spec = Some cap; 550 cdl_objects spec obj_id = Some obj; cnode_at obj_id spec\<rbrakk> 551 \<Longrightarrow> slot < 2 ^ object_size_bits obj" 552 apply (frule opt_cap_cdl_objects) 553 apply (clarsimp simp: well_formed_def object_at_def is_cnode_def) 554 apply (erule_tac x=obj_id in allE) 555 apply clarsimp 556 apply (clarsimp simp: opt_cap_def opt_object_def) 557 apply (subgoal_tac "slot \<in> dom (object_slots (object_default_state obj))") 558 apply (thin_tac "dom P = dom Q" for P Q) 559 apply (clarsimp simp: well_formed_caps_def) 560 apply (erule_tac x=slot in allE) 561 apply (clarsimp simp: object_default_state_def2 object_type_def has_slots_def 562 default_tcb_def object_size_bits_def object_slots_def 563 empty_cnode_def empty_cap_map_def pt_size_def pd_size_def 564 split: cdl_object.splits if_split_asm) 565 apply (clarsimp simp: object_slots_slots_of) 566 done 567 568lemma well_formed_cnode_object_size_bits: 569 "\<lbrakk>well_formed spec; cnode_at obj_id spec; cdl_objects spec obj_id = Some obj\<rbrakk> 570 \<Longrightarrow> 0 < object_size_bits obj" 571 apply (clarsimp simp: well_formed_def) 572 apply (erule_tac x=obj_id in allE) 573 apply (clarsimp simp: is_cnode_def object_at_def) 574 done 575 576lemma well_formed_cnode_object_size_bits_eq: 577 "\<lbrakk>well_formed spec; opt_cap slot spec = Some cap; 578 cdl_objects spec (cap_object cap) = Some obj; is_cnode_cap cap\<rbrakk> 579 \<Longrightarrow> object_size_bits obj = cnode_cap_size cap" 580 apply (frule (1) well_formed_cap_object_is_real) 581 apply (clarsimp simp: cap_has_object_def cap_type_def split: cdl_cap.splits) 582 apply (clarsimp simp: well_formed_def split_def split:option.splits) 583 apply (erule_tac x="cap_object cap" in allE) 584 apply (case_tac slot) 585 apply (clarsimp simp: is_cnode_def opt_object_def well_formed_cap_to_object_def) 586 done 587 588lemma slots_of_set [simp]: 589 "well_formed spec \<Longrightarrow> set (slots_of_list spec obj) = dom (slots_of obj spec)" 590 by (clarsimp simp: slots_of_list_def well_formed_finite) 591 592lemma well_formed_well_formed_tcb: 593 "\<lbrakk>well_formed spec; cdl_objects spec obj_id = Some obj\<rbrakk> 594 \<Longrightarrow> well_formed_tcb spec obj_id obj" 595 apply (clarsimp simp: well_formed_def) 596 apply (erule_tac x=obj_id in allE) 597 apply clarsimp 598 done 599 600lemma well_formed_well_formed_vspace: 601 "\<lbrakk>well_formed spec; cdl_objects spec obj_id = Some obj\<rbrakk> 602 \<Longrightarrow> well_formed_vspace spec obj_id obj" 603 apply (clarsimp simp: well_formed_def) 604 apply (erule_tac x=obj_id in allE) 605 apply clarsimp 606 done 607 608lemma well_formed_well_formed_irq_node: 609 "\<lbrakk>well_formed spec; cdl_objects spec obj_id = Some obj\<rbrakk> 610 \<Longrightarrow> well_formed_irq_node spec obj_id obj" 611 apply (clarsimp simp: well_formed_def) 612 apply (erule_tac x=obj_id in allE) 613 apply clarsimp 614 done 615 616lemma well_formed_well_formed_irqhandler_caps: 617 "well_formed spec \<Longrightarrow> well_formed_irqhandler_caps spec" 618 by (clarsimp simp: well_formed_def) 619 620lemma well_formed_well_formed_irq_table: 621 "well_formed spec \<Longrightarrow> well_formed_irq_table spec" 622 by (clarsimp simp: well_formed_def) 623 624lemma well_formed_inj_cdl_irq_node: 625 "well_formed spec \<Longrightarrow> inj (cdl_irq_node spec)" 626 by (clarsimp simp: well_formed_def well_formed_irq_table_def) 627 628lemma well_formed_vm_cap_has_asid: 629 "\<lbrakk>well_formed spec; cdl_objects spec obj_id = Some obj; 630 object_slots obj slot = Some cap\<rbrakk> 631 \<Longrightarrow> \<not>vm_cap_has_asid cap" 632 apply (case_tac "cap = NullCap") 633 apply (clarsimp simp: vm_cap_has_asid_def) 634 apply (drule (3) well_formed_well_formed_cap) 635 apply (clarsimp simp: well_formed_cap_def vm_cap_has_asid_def 636 split: cdl_cap.splits) 637 done 638 639lemma is_fake_vm_cap_cap_type: 640 "is_fake_vm_cap cap \<Longrightarrow> (\<exists>sz. cap_type cap = Some (FrameType sz)) \<or> 641 (cap_type cap = Some PageTableType) \<or> 642 (cap_type cap = Some PageDirectoryType)" 643 by (clarsimp simp: is_fake_vm_cap_def cap_type_def 644 split: cdl_cap.splits) 645 646lemma well_formed_irq_node_in_irq_nodes: 647 "\<lbrakk>well_formed spec; cdl_objects spec obj_id = Some obj; is_irq_node obj\<rbrakk> 648 \<Longrightarrow> obj_id \<in> irq_nodes spec" 649 oops 650 651term real_object_at 652lemma well_formed_irq_node_cap_is_ntfn_cap: 653 "\<lbrakk>well_formed spec; cdl_objects spec obj_id = Some obj; is_irq_node obj; 654 object_slots obj slot = Some cap; cap \<noteq> NullCap\<rbrakk> 655 \<Longrightarrow> is_ntfn_cap cap" 656 apply (frule (3) well_formed_well_formed_cap_types_match) 657 658 apply (clarsimp simp: well_formed_cap_types_match_def) 659 660 661 oops 662 663lemma well_formed_is_fake_vm_cap: 664 "\<lbrakk>well_formed spec; cdl_objects spec obj_id = Some obj; is_cnode obj \<or> is_tcb obj \<or> is_irq_node obj; 665 object_slots obj slot = Some cap\<rbrakk> 666 \<Longrightarrow> \<not>is_fake_vm_cap cap" 667 apply (case_tac "is_irq_node obj") 668 apply (frule (1) well_formed_well_formed_irq_node) 669 apply (clarsimp simp: well_formed_irq_node_def object_at_def irq_nodes_def) 670 apply (drule is_fake_vm_cap_cap_type) 671 apply (cases "cap = NullCap", simp_all) 672 apply (clarsimp simp: well_formed_def) 673 apply (erule_tac x=obj_id in allE) 674 apply (clarsimp simp: well_formed_caps_def) 675 apply (erule_tac x=slot in allE) 676 apply (clarsimp simp: domI is_fake_vm_cap_def) 677 done 678 679lemma vm_cap_has_asid_update_cap_object [simp]: 680 "vm_cap_has_asid (update_cap_object obj_id cap) = vm_cap_has_asid cap" 681 by (clarsimp simp: cap_has_object_def update_cap_object_def 682 vm_cap_has_asid_def 683 split: cdl_cap.splits) 684 685lemma well_formed_object_size_bits_word_bits [simp]: 686 "\<lbrakk>well_formed spec; cdl_objects spec obj_id = Some spec_obj\<rbrakk> 687 \<Longrightarrow> object_size_bits spec_obj < word_bits" 688 apply (clarsimp simp: well_formed_def) 689 apply (erule_tac x=obj_id in allE) 690 apply clarsimp 691 done 692 693lemma well_formed_is_untyped_cap: 694 "\<lbrakk>well_formed spec; cnode_at obj_id spec; 695 opt_cap (obj_id, slot) spec = Some cap\<rbrakk> 696 \<Longrightarrow> \<not> is_untyped_cap cap" 697 apply (frule opt_cap_cdl_objects) 698 apply (clarsimp simp: well_formed_def) 699 apply (erule_tac x=obj_id in allE) 700 apply (clarsimp simp: opt_cap_def well_formed_caps_def) 701 apply (erule_tac x=slot in allE) 702 apply (clarsimp simp: slots_of_def opt_object_def well_formed_cap_def 703 cap_type_def 704 split: cdl_cap.splits) 705 done 706 707lemma well_formed_cap_has_object: 708 "\<lbrakk>well_formed spec; opt_cap (obj_id, slot) spec = Some spec_cap; 709 spec_cap \<noteq> NullCap; \<not> is_untyped_cap spec_cap; \<not> is_irqhandler_cap spec_cap\<rbrakk> 710 \<Longrightarrow> cap_has_object spec_cap" 711 apply (clarsimp simp: opt_cap_def opt_object_def slots_of_def) 712 apply (clarsimp simp: well_formed_def) 713 apply (clarsimp split: option.splits) 714 apply (rename_tac obj) 715 apply (erule_tac x=obj_id in allE) 716 apply (erule_tac x=obj in allE) 717 apply (clarsimp simp: well_formed_caps_def) 718 apply (erule_tac x=slot in allE) 719 apply (clarsimp simp: domI) 720 apply (clarsimp simp: cap_has_object_def well_formed_cap_def 721 split: cdl_cap.splits) 722 done 723 724lemma well_formed_cap_object: 725 "\<lbrakk>well_formed spec; opt_cap (obj_id, slot) spec = Some spec_cap; 726 cap_has_object spec_cap\<rbrakk> 727 \<Longrightarrow> \<exists>obj. cdl_objects spec (cap_object spec_cap) = Some obj" 728 apply (frule (1) well_formed_well_formed_cap', clarsimp) 729 apply (frule (1) well_formed_cap_has_object) 730 apply clarsimp 731 apply (clarsimp simp: well_formed_cap_def cap_type_def split: cdl_cap.splits) 732 apply simp 733 apply (clarsimp simp: opt_cap_def slots_of_def opt_object_def split: option.splits) 734 apply (frule (1) well_formed_well_formed_caps) 735 apply (clarsimp simp: well_formed_caps_def well_formed_cap_types_match_def) 736 apply (erule allE [where x=slot]) 737 apply (erule allE [where x=spec_cap]) 738 apply clarsimp 739 done 740 741lemma well_formed_cap_object_in_dom: 742 "\<lbrakk>well_formed spec; opt_cap (obj_id, slot) spec = Some spec_cap; 743 cap_has_object spec_cap\<rbrakk> 744 \<Longrightarrow> cap_object spec_cap \<in> dom (cdl_objects spec)" 745 by (drule (2) well_formed_cap_object, clarsimp) 746 747lemma well_formed_all_caps_cap_object: 748 "\<lbrakk>well_formed spec; cap \<in> all_caps spec; cap_has_object cap\<rbrakk> 749 \<Longrightarrow>\<exists>obj. cdl_objects spec (cap_object cap) = Some obj" 750 apply (clarsimp simp: all_caps_def) 751 apply (erule (2) well_formed_cap_object) 752 done 753 754lemma well_formed_all_caps_cap_irq: 755 "\<lbrakk>well_formed spec; cap \<in> all_caps spec; is_irqhandler_cap cap\<rbrakk> 756 \<Longrightarrow>\<exists>obj. cdl_objects spec (cdl_irq_node spec (cap_irq cap)) = Some obj" 757 apply (clarsimp simp: all_caps_def) 758 apply (frule (1) well_formed_well_formed_cap_types_match', simp) 759 apply (clarsimp simp: well_formed_cap_types_match_def) 760 done 761 762lemma well_formed_update_cap_rights_idem: 763 "\<lbrakk>well_formed_cap cap; rights = cap_rights cap\<rbrakk> 764 \<Longrightarrow> update_cap_rights rights cap = cap" 765 by (auto simp: update_cap_rights_def cap_rights_def well_formed_cap_def 766 validate_vm_rights_def vm_kernel_only_def vm_read_write_def 767 vm_read_only_def split: cdl_cap.splits) 768 769lemma default_ep_cap[simp]: 770 "is_default_cap (EndpointCap a 0 UNIV)" 771 by (simp add:is_default_cap_def default_cap_def 772 cap_type_def) 773 774lemma default_ntfn_cap[simp]: 775 "is_default_cap (NotificationCap a 0 {AllowRead, AllowWrite})" 776 by (simp add:is_default_cap_def default_cap_def cap_type_def) 777 778lemma default_cap_well_formed_cap: 779 "\<lbrakk>well_formed_cap cap; cap_type cap = Some type; cnode_cap_size cap = sz\<rbrakk> 780 \<Longrightarrow> well_formed_cap (default_cap type obj_ids sz dev)" 781 by (auto simp: well_formed_cap_def default_cap_def cap_type_def 782 word_gt_a_gt_0 vm_read_write_def cnode_cap_size_def 783 split: cdl_cap.splits) 784 785lemma default_cap_well_formed_cap2: 786 "\<lbrakk>is_default_cap cap; cap_type cap = Some type; sz \<le> 32; 787 \<not> is_untyped_cap cap; \<not> is_asidpool_cap cap\<rbrakk> 788 \<Longrightarrow> well_formed_cap (default_cap type obj_ids sz dev )" 789 apply (clarsimp simp: is_default_cap_def) 790 apply (clarsimp simp: default_cap_def well_formed_cap_def 791 word_gt_a_gt_0 badge_bits_def guard_bits_def 792 vm_read_write_def cnode_cap_size_def 793 split: cdl_object_type.splits cdl_cap.splits) 794 done 795 796lemma well_formed_well_formed_orig_cap: 797 "\<lbrakk>well_formed spec; 798 opt_cap (obj_id, slot) spec = Some cap; cap \<noteq> NullCap; 799 original_cap_at (obj_id, slot) spec\<rbrakk> 800 \<Longrightarrow> well_formed_orig_cap cap" 801 apply (frule opt_cap_dom_cdl_objects) 802 apply (clarsimp simp: dom_def, rename_tac obj) 803 apply (frule (1) object_slots_opt_cap, simp) 804 apply (clarsimp simp: well_formed_def well_formed_caps_def) 805 apply (erule allE [where x=obj_id]) 806 apply (clarsimp simp: well_formed_caps_def) 807 done 808 809lemma well_formed_orig_ep_cap_is_default_helper: 810 "\<lbrakk>well_formed_orig_cap cap; ep_related_cap cap; cap_has_type cap\<rbrakk> \<Longrightarrow> is_default_cap cap" 811 by (clarsimp simp: well_formed_orig_cap_def is_default_cap_def cap_rights_def 812 ep_related_cap_def default_cap_def cap_type_def 813 split: cdl_cap.splits) 814 815lemma well_formed_orig_ep_cap_is_default: 816 "\<lbrakk>well_formed spec; original_cap_at (obj_id, slot) spec; 817 opt_cap (obj_id, slot) spec = Some cap; 818 ep_related_cap cap; cap \<noteq> NullCap\<rbrakk> 819 \<Longrightarrow> is_default_cap cap" 820 apply (case_tac "\<exists>obj_id. cap = ReplyCap obj_id") 821 apply (frule (1) well_formed_well_formed_cap', simp) 822 apply (clarsimp simp: well_formed_cap_def) 823 apply (frule (3) well_formed_well_formed_orig_cap) 824 apply (erule (1) well_formed_orig_ep_cap_is_default_helper) 825 apply (fastforce simp: ep_related_cap_def split: cdl_cap.splits) 826 done 827 828lemma cap_rights_default_cap_eq: 829 "cap_rights (default_cap type obj_ids sz dev) = 830 cap_rights (default_cap type obj_ids' sz' dev')" 831 apply (clarsimp simp: cap_rights_def default_cap_def) 832 apply (case_tac type, simp_all) 833 done 834 835lemma well_formed_orig_caps: 836 "\<lbrakk>well_formed spec; original_cap_at (obj_id, slot) spec; 837 slots_of obj_id spec slot = Some cap; cap \<noteq> NullCap; cap_type cap = Some type\<rbrakk> 838 \<Longrightarrow> cap_rights (default_cap type obj_ids sz dev) = cap_rights cap" 839 apply (frule well_formed_well_formed_orig_cap, simp add: opt_cap_def, assumption+) 840 apply (clarsimp simp: well_formed_orig_cap_def) 841 apply (subst (asm) cap_rights_default_cap_eq, fast) 842 done 843 844lemma well_formed_cdt: 845 "\<lbrakk>well_formed spec; opt_cap (obj_id, slot) spec = Some cap; cap_has_object cap; 846 cnode_at obj_id spec\<rbrakk> \<Longrightarrow> 847 \<exists>orig_obj_id orig_slot orig_cap. 848 cnode_at orig_obj_id spec \<and> 849 original_cap_at (orig_obj_id, orig_slot) spec \<and> 850 opt_cap (orig_obj_id, orig_slot) spec = Some orig_cap \<and> 851 cap_has_object orig_cap \<and> cap_object orig_cap = cap_object cap" 852 apply (clarsimp simp: well_formed_def) 853 apply (erule_tac x=obj_id in allE) 854 apply (clarsimp simp: split: option.splits) 855 apply (clarsimp simp: object_at_def) 856 apply (clarsimp simp: well_formed_caps_def) 857 apply (erule_tac x=slot in allE) 858 apply (clarsimp simp: well_formed_cdt_def object_slots_opt_cap) 859 by blast 860 861lemma well_formed_cap_to_real_object: 862 "\<lbrakk>well_formed spec; real_object_at obj_id spec\<rbrakk> 863 \<Longrightarrow> \<exists>cnode_id slot cap. 864 opt_cap (cnode_id, slot) spec = Some cap \<and> 865 original_cap_at (cnode_id, slot) spec \<and> 866 cnode_at cnode_id spec \<and> 867 cap_object cap = obj_id \<and> 868 cap_has_object cap" 869 apply (clarsimp simp: well_formed_def) 870 apply (erule_tac x=obj_id in allE) 871 apply (clarsimp simp: well_formed_cap_to_object_def real_object_at_def split: option.splits) 872 done 873 874lemma well_formed_cap_to_irq_object: 875 "\<lbrakk>well_formed spec; cdl_objects spec obj_id = Some obj; obj_id \<in> irq_nodes spec\<rbrakk> 876 \<Longrightarrow> \<exists>cnode_id slot cap. 877 opt_cap (cnode_id, slot) spec = Some cap \<and> 878 original_cap_at (cnode_id, slot) spec \<and> 879 cnode_at cnode_id spec \<and> 880 is_irqhandler_cap cap \<and> 881 cdl_irq_node spec (cap_irq cap) = obj_id" 882 apply (frule (1) well_formed_well_formed_cap_to_object) 883 apply (clarsimp simp: well_formed_cap_to_object_def real_object_at_def split: option.splits) 884 done 885 886lemma well_formed_cap_to_non_empty_pt: 887 "\<lbrakk>well_formed spec; pt_at obj_id spec; 888 object_at (\<lambda>obj. object_default_state obj \<noteq> obj) obj_id spec\<rbrakk> 889 \<Longrightarrow> \<exists>pd_id slot cap. 890 opt_cap (pd_id, slot) spec = Some cap \<and> 891 pd_at pd_id spec \<and> 892 cap_object cap = obj_id \<and> 893 cap_has_object cap" 894 apply (clarsimp simp: well_formed_def) 895 apply (erule_tac x=obj_id in allE) 896 apply (clarsimp simp: object_at_def) 897 apply (clarsimp simp: well_formed_vspace_def well_formed_cap_to_non_empty_pt_def object_at_def) 898 done 899 900lemma dom_object_slots_default_tcb: 901 "dom (object_slots (Tcb (default_tcb domain))) = {0..tcb_boundntfn_slot}" 902 by (clarsimp simp: object_slots_def default_tcb_def) 903 904lemma well_formed_tcb_has_fault: 905 "\<lbrakk>well_formed spec; cdl_objects spec obj_id = Some (Tcb tcb)\<rbrakk> 906 \<Longrightarrow> \<not> cdl_tcb_has_fault tcb" 907 apply (drule (1) well_formed_well_formed_tcb) 908 apply (clarsimp simp: well_formed_tcb_def tcb_has_fault_def) 909 done 910 911lemma well_formed_tcb_domain: 912 "\<lbrakk>well_formed spec; cdl_objects spec obj_id = Some (Tcb tcb)\<rbrakk> 913 \<Longrightarrow> cdl_tcb_domain tcb = minBound" 914 apply (drule (1) well_formed_well_formed_tcb) 915 apply (clarsimp simp: well_formed_tcb_def tcb_domain_def) 916 done 917 918lemma well_formed_object_domain: 919 "\<lbrakk>well_formed spec; cdl_objects spec obj_id = Some obj\<rbrakk> 920 \<Longrightarrow> object_domain obj = minBound" 921 apply (case_tac "\<exists>tcb. obj = Tcb tcb") 922 apply clarsimp 923 apply (drule (1) well_formed_tcb_domain) 924 apply (clarsimp simp: object_domain_def) 925 apply (clarsimp simp: object_domain_def minBound_word 926 split: cdl_object.splits) 927 done 928 929lemma well_formed_tcb_object_slots: 930 "\<lbrakk>well_formed spec; cdl_objects spec obj_id = Some tcb; is_tcb tcb\<rbrakk> 931 \<Longrightarrow> dom (object_slots tcb) = {0..tcb_boundntfn_slot}" 932 apply (frule (1) well_formed_object_slots) 933 apply (clarsimp simp: object_default_state_def2 is_tcb_def split: cdl_object.splits) 934 apply (rule dom_object_slots_default_tcb) 935 done 936 937lemma well_formed_tcb_cspace_cap: 938 "\<lbrakk>well_formed spec; 939 tcb_at obj_id spec\<rbrakk> 940 \<Longrightarrow> \<exists>cspace_cap. opt_cap (obj_id, tcb_cspace_slot) spec = Some cspace_cap \<and> 941 is_cnode_cap cspace_cap \<and> cap_guard_size cspace_cap \<noteq> 0 \<and> 942 real_object_at (cap_object cspace_cap) spec" 943 apply (clarsimp simp: object_at_def) 944 apply (frule (1) well_formed_well_formed_caps) 945 apply (frule (1) well_formed_well_formed_tcb) 946 apply (frule (2) well_formed_tcb_object_slots) 947 apply (clarsimp simp: well_formed_caps_def) 948 apply (clarsimp simp: well_formed_tcb_def) 949 apply (erule_tac x=tcb_cspace_slot in allE)+ 950 apply (clarsimp simp: is_tcb_def object_default_state_def2 split: cdl_object.splits) 951 apply (rename_tac cdl_tcb) 952 apply (clarsimp simp: opt_cap_def slots_of_def opt_object_def split: option.splits) 953 apply (subgoal_tac "\<exists>cspace_cap. object_slots (Tcb cdl_tcb) tcb_cspace_slot = 954 Some cspace_cap") 955 apply (clarsimp simp: dom_def well_formed_tcb_def real_object_at_def) 956 apply (erule well_formed_cap_object [where obj_id=obj_id and slot=tcb_cspace_slot]) 957 apply (simp add: opt_cap_def slots_of_def opt_object_def) 958 apply (clarsimp simp: cap_has_object_def cap_type_def split: cdl_cap.splits) 959 apply (auto simp: dom_def tcb_pending_op_slot_def tcb_cspace_slot_def) 960 done 961 962lemma cap_data_cap_guard_size_0: 963 "\<lbrakk>well_formed_cap cap; is_cnode_cap cap; cap_data cap = 0\<rbrakk> 964 \<Longrightarrow> cap_guard_size cap = 0" 965 apply (clarsimp simp: cap_type_def cap_data_def guard_as_rawdata_def 966 well_formed_cap_def 967 split: cdl_cap.splits) 968 apply (subst (asm) is_aligned_add_or [where n=8]) 969 apply (rule is_aligned_shift) 970 apply (rule shiftl_less_t2n) 971 apply (rule word_of_nat_less) 972 apply (clarsimp simp: guard_bits_def) 973 apply clarsimp 974 apply (clarsimp simp: word_or_zero) 975 apply (rule ccontr) 976 apply (drule (1) guard_size_shiftl_non_zero) 977 apply simp 978 done 979 980lemma well_formed_tcb_cspace_cap_cap_data: 981 "\<lbrakk>well_formed spec; tcb_at obj_id spec; 982 cdl_objects spec obj_id = Some (Tcb tcb); 983 opt_cap (obj_id, tcb_cspace_slot) spec = Some spec_cspace_cap\<rbrakk> 984 \<Longrightarrow> cap_data spec_cspace_cap \<noteq> 0" 985 apply (frule (1) well_formed_tcb_cspace_cap, clarsimp) 986 apply (frule (1) well_formed_well_formed_cap', clarsimp) 987 apply (drule (2) cap_data_cap_guard_size_0, simp) 988 done 989 990lemma well_formed_tcb_opt_cap: 991 "\<lbrakk>well_formed spec; tcb_at obj_id spec; slot \<in> {0..tcb_boundntfn_slot}\<rbrakk> 992 \<Longrightarrow> \<exists>cap. opt_cap (obj_id, slot) spec = Some cap" 993 apply (clarsimp simp: object_at_def) 994 apply (drule (1) well_formed_object_slots) 995 apply (fastforce simp: object_default_state_def2 is_tcb_def 996 opt_cap_def slots_of_def opt_object_def object_slots_def 997 default_tcb_def dom_def tcb_pending_op_slot_def 998 split: cdl_object.splits if_split_asm) 999 done 1000 1001 1002lemma well_formed_tcb_vspace_cap: 1003 "\<lbrakk>well_formed spec; 1004 tcb_at obj_id spec\<rbrakk> 1005 \<Longrightarrow> \<exists>vspace_cap. 1006 opt_cap (obj_id, tcb_vspace_slot) spec = Some vspace_cap \<and> is_pd_cap vspace_cap" 1007 apply (frule (1) well_formed_tcb_opt_cap [where slot=tcb_vspace_slot], simp add: tcb_slot_defs) 1008 apply (clarsimp simp: object_at_def) 1009 apply (frule (1) well_formed_well_formed_tcb) 1010 apply (auto simp: well_formed_tcb_def opt_cap_def slots_of_def opt_object_def ) 1011 done 1012 1013lemma well_formed_tcb_ipcbuffer_cap: 1014 "\<lbrakk>well_formed spec; 1015 tcb_at obj_id spec\<rbrakk> 1016 \<Longrightarrow> \<exists>tcb_ipcbuffer_cap. 1017 opt_cap (obj_id, tcb_ipcbuffer_slot) spec = Some tcb_ipcbuffer_cap \<and> 1018 is_default_cap tcb_ipcbuffer_cap \<and> is_frame_cap tcb_ipcbuffer_cap" 1019 apply (frule (1) well_formed_tcb_opt_cap [where slot=tcb_ipcbuffer_slot], simp add: tcb_slot_defs) 1020 apply (clarsimp simp: object_at_def) 1021 apply (frule (1) well_formed_well_formed_tcb) 1022 apply (auto simp: well_formed_tcb_def opt_cap_def slots_of_def opt_object_def) 1023 done 1024 1025lemma well_formed_tcb_caller_cap: 1026 "\<lbrakk>well_formed spec; tcb_at obj_id spec\<rbrakk> 1027 \<Longrightarrow> opt_cap (obj_id, tcb_caller_slot) spec = Some NullCap" 1028 apply (frule (1) well_formed_tcb_opt_cap [where slot=tcb_caller_slot], simp add: tcb_slot_defs) 1029 apply (clarsimp simp: object_at_def) 1030 apply (frule (1) well_formed_well_formed_tcb) 1031 apply (auto simp: well_formed_tcb_def opt_cap_def slots_of_def opt_object_def) 1032 done 1033 1034lemma well_formed_tcb_replycap_cap: 1035 "\<lbrakk>well_formed spec; tcb_at obj_id spec\<rbrakk> 1036 \<Longrightarrow> opt_cap (obj_id, tcb_replycap_slot) spec = Some NullCap \<or> 1037 opt_cap (obj_id, tcb_replycap_slot) spec = Some (MasterReplyCap obj_id)" 1038 apply (frule (1) well_formed_tcb_opt_cap [where slot=tcb_replycap_slot], simp add: tcb_slot_defs) 1039 apply (clarsimp simp: object_at_def) 1040 apply (frule (1) well_formed_well_formed_tcb) 1041 apply (auto simp: well_formed_tcb_def opt_cap_def slots_of_def opt_object_def) 1042 done 1043 1044 1045lemma well_formed_tcb_pending_op_cap: 1046 "\<lbrakk>well_formed spec; tcb_at obj_id spec\<rbrakk> 1047 \<Longrightarrow> opt_cap (obj_id, tcb_pending_op_slot) spec = Some NullCap \<or> 1048 opt_cap (obj_id, tcb_pending_op_slot) spec = Some RestartCap" 1049 apply (frule (1) well_formed_tcb_opt_cap [where slot=tcb_pending_op_slot], simp add: tcb_slot_defs) 1050 apply (clarsimp simp: object_at_def) 1051 apply (frule (1) well_formed_well_formed_tcb) 1052 apply (auto simp: well_formed_tcb_def opt_cap_def slots_of_def opt_object_def) 1053 done 1054 1055lemma well_formed_tcb_pending_op_replycap: 1056 "\<lbrakk>well_formed spec; tcb_at obj_id spec\<rbrakk> 1057 \<Longrightarrow> (opt_cap (obj_id, tcb_replycap_slot) spec = Some (MasterReplyCap obj_id)) 1058 = (opt_cap (obj_id, tcb_pending_op_slot) spec = Some RestartCap)" 1059 apply (clarsimp simp: object_at_def) 1060 apply (drule (1) well_formed_well_formed_tcb) 1061 apply (clarsimp simp: well_formed_tcb_def opt_cap_def slots_of_def opt_object_def) 1062 done 1063 1064lemma well_formed_tcb_boundntfn_cap: 1065 "\<lbrakk>well_formed spec; tcb_at obj_id spec\<rbrakk> 1066 \<Longrightarrow> opt_cap (obj_id, tcb_boundntfn_slot) spec = Some NullCap" 1067 apply (frule (1) well_formed_tcb_opt_cap [where slot=tcb_boundntfn_slot], simp add: tcb_slot_defs) 1068 apply (elim exE) 1069 apply (clarsimp simp: object_at_def) 1070 apply (drule (1) well_formed_well_formed_tcb) 1071 by (auto simp: well_formed_tcb_def opt_cap_def slots_of_def opt_object_def) 1072 1073lemma well_formed_orig_caps_unique: 1074 "\<lbrakk>well_formed spec; original_cap_at (obj_id, slot) spec; original_cap_at (obj_id', slot') spec; 1075 cnode_at obj_id spec; cnode_at obj_id' spec; cap_has_object cap; cap_has_object cap'; 1076 opt_cap (obj_id, slot) spec = Some cap; opt_cap (obj_id', slot') spec = Some cap'; 1077 cap_object cap = cap_object cap'\<rbrakk> 1078 \<Longrightarrow> obj_id = obj_id' \<and> slot = slot'" 1079 by (clarsimp simp: well_formed_def well_formed_orig_caps_unique_def) 1080 1081lemma well_formed_orig_caps_unique': 1082 "\<lbrakk>well_formed spec; original_cap_at (obj_id, slot) spec; original_cap_at (obj_id', slot') spec; 1083 real_cap_ref (obj_id, slot) spec; real_cap_ref (obj_id', slot') spec; 1084 opt_cap (obj_id, slot) spec = Some cap; opt_cap (obj_id', slot') spec = Some cap'; 1085 cap_has_object cap; cap_has_object cap'; 1086 cap_object cap = cap_object cap'\<rbrakk> 1087 \<Longrightarrow> obj_id = obj_id' \<and> slot = slot'" 1088 by (clarsimp simp: well_formed_def well_formed_orig_caps_unique_def real_cap_ref_def) 1089 1090lemma well_formed_irqhandler_caps_unique: 1091 "\<lbrakk>well_formed s; is_irqhandler_cap cap; is_irqhandler_cap cap'; 1092 opt_cap (obj_id, slot) s = Some cap; opt_cap (obj_id', slot') s = Some cap'; 1093 cap_irq cap = cap_irq cap'\<rbrakk> 1094 \<Longrightarrow> obj_id = obj_id' \<and> slot = slot'" 1095 by (clarsimp simp: well_formed_def well_formed_irqhandler_caps_unique_def) 1096 1097lemma object_cap_ref_cap_irq: 1098 "\<lbrakk>object_cap_ref (obj_id, slot) spec; opt_cap (obj_id, slot) spec = Some cap\<rbrakk> 1099 \<Longrightarrow> cap_irq cap = undefined" 1100 by (auto simp: object_cap_ref_def cap_has_object_def cap_irq_def 1101 split: cdl_cap.splits) 1102 1103lemma object_cap_ref_real_cap_ref: 1104 "object_cap_ref (obj_id, slot) spec \<Longrightarrow> real_cap_ref (obj_id, slot) spec" 1105 by (clarsimp simp: object_cap_ref_def real_cap_ref_def) 1106 1107lemma well_formed_orig_caps_unique_object_cap: 1108 "\<lbrakk>well_formed spec; original_cap_at (obj_id, slot) spec; original_cap_at (obj_id', slot') spec; 1109 object_cap_ref (obj_id, slot) spec; object_cap_ref (obj_id', slot') spec; 1110 opt_cap (obj_id, slot) spec = Some cap; opt_cap (obj_id', slot') spec = Some cap'; 1111 cap_has_object cap; cap_has_object cap'; 1112 cap_object cap = cap_object cap'\<rbrakk> 1113 \<Longrightarrow> obj_id = obj_id' \<and> slot = slot'" 1114 apply (frule object_cap_ref_real_cap_ref, drule (1) object_cap_ref_cap_irq)+ 1115 apply (erule (8) well_formed_orig_caps_unique', simp) 1116 done 1117 1118lemma well_formed_child_cap_not_copyable: 1119 "\<lbrakk>well_formed spec; \<not> original_cap_at (obj_id, slot) spec; 1120 opt_cap (obj_id, slot) spec = Some cap; cap \<noteq> NullCap\<rbrakk> 1121 \<Longrightarrow> is_copyable_cap cap" 1122 apply (clarsimp simp: well_formed_def) 1123 apply (erule_tac x=obj_id in allE) 1124 apply (clarsimp simp: opt_cap_def opt_object_def slots_of_def) 1125 apply (clarsimp split: option.splits) 1126 apply (rename_tac obj) 1127 apply (clarsimp simp: well_formed_caps_def) 1128 done 1129 1130lemma well_formed_child_cap_not_copyable': 1131 "\<lbrakk>well_formed spec; 1132 opt_cap (obj_id, slot) spec = Some cap; cap \<noteq> NullCap\<rbrakk> 1133 \<Longrightarrow> \<not>original_cap_at (obj_id, slot) spec \<longrightarrow> is_copyable_cap cap" 1134 by (rule impI, erule (3) well_formed_child_cap_not_copyable) 1135 1136lemma well_formed_pd: 1137 "\<lbrakk>well_formed spec; opt_cap (obj_id, slot) spec = Some cap; 1138 pd_at obj_id spec; cap \<noteq> NullCap\<rbrakk> 1139 \<Longrightarrow> is_frame_cap cap \<or> is_fake_pt_cap cap" 1140 apply (clarsimp simp: object_at_def) 1141 apply (frule (1) well_formed_well_formed_vspace) 1142 apply (clarsimp simp: well_formed_vspace_def) 1143 apply (erule allE [where x=slot]) 1144 apply (erule allE [where x=cap]) 1145 apply (clarsimp simp: opt_cap_def slots_of_def opt_object_def split: option.splits) 1146 done 1147 1148lemma well_formed_pt: 1149 "\<lbrakk>well_formed spec; opt_cap (obj_id, slot) spec = Some cap; 1150 pt_at obj_id spec; cap \<noteq> NullCap\<rbrakk> 1151 \<Longrightarrow> is_frame_cap cap" 1152 apply (clarsimp simp: object_at_def) 1153 apply (frule (1) well_formed_well_formed_vspace) 1154 apply (clarsimp simp: well_formed_vspace_def) 1155 apply (erule allE [where x=slot]) 1156 apply (erule allE [where x=cap]) 1157 apply (clarsimp simp: opt_cap_def slots_of_def opt_object_def split: option.splits) 1158 done 1159 1160lemma well_formed_pt_cap_is_fake_pt_cap: 1161 "\<lbrakk>well_formed spec; opt_cap (obj_id, slot) spec = Some cap; 1162 pd_at obj_id spec; is_pt_cap cap\<rbrakk> 1163 \<Longrightarrow> is_fake_pt_cap cap" 1164 by (frule (2) well_formed_pd, clarsimp+) 1165 1166 1167 1168(**************************************** 1169 * Rules about IRQ caps and IRQ CNodes. * 1170 ****************************************) 1171 1172lemma well_formed_irq_nodes_object_type: 1173 "\<lbrakk>well_formed spec; obj_id \<in> irq_nodes spec; 1174 cdl_objects spec obj_id = Some object\<rbrakk> 1175 \<Longrightarrow> object_type object = IRQNodeType" 1176 apply (frule (1) well_formed_well_formed_irq_node) 1177 apply (frule (2) well_formed_cap_to_irq_object) 1178 apply (clarsimp simp: opt_cap_def slots_of_def opt_object_def split: option.splits) 1179 apply (frule (2) well_formed_well_formed_cap_types_match, simp) 1180 apply (clarsimp simp: well_formed_cap_types_match_def) 1181 done 1182 1183lemma well_formed_object_at_irq_node_irq_node_at: 1184 "\<lbrakk>well_formed spec; object_at P obj_id spec; obj_id \<in> irq_nodes spec\<rbrakk> \<Longrightarrow> irq_node_at obj_id spec" 1185 apply (clarsimp simp: object_at_def) 1186 apply (frule (2) well_formed_irq_nodes_object_type) 1187 apply (simp add: object_type_is_object) 1188 done 1189 1190lemma real_object_not_irq_node: 1191 "well_formed spec \<Longrightarrow> (real_object_at obj_id spec \<and> cnode_at obj_id spec) = cnode_at obj_id spec" 1192 "well_formed spec \<Longrightarrow> (real_object_at obj_id spec \<and> tcb_at obj_id spec) = tcb_at obj_id spec" 1193 "well_formed spec \<Longrightarrow> (real_object_at obj_id spec \<and> table_at obj_id spec) = table_at obj_id spec" 1194 "well_formed spec \<Longrightarrow> (real_object_at obj_id spec \<and> capless_at obj_id spec) = capless_at obj_id spec" 1195 apply (insert well_formed_object_at_irq_node_irq_node_at [where spec=spec and obj_id=obj_id]) 1196 apply (fastforce simp: real_object_at_def object_at_def object_type_is_object)+ 1197 done 1198 1199lemma object_at_real_object_at: 1200 "\<lbrakk>well_formed spec; cnode_at obj_id spec\<rbrakk> \<Longrightarrow> real_object_at obj_id spec" 1201 "\<lbrakk>well_formed spec; tcb_at obj_id spec\<rbrakk> \<Longrightarrow> real_object_at obj_id spec" 1202 "\<lbrakk>well_formed spec; ep_at obj_id spec\<rbrakk> \<Longrightarrow> real_object_at obj_id spec" 1203 "\<lbrakk>well_formed spec; ntfn_at obj_id spec\<rbrakk> \<Longrightarrow> real_object_at obj_id spec" 1204 "\<lbrakk>well_formed spec; table_at obj_id spec\<rbrakk> \<Longrightarrow> real_object_at obj_id spec" 1205 "\<lbrakk>well_formed spec; pd_at obj_id spec\<rbrakk> \<Longrightarrow> real_object_at obj_id spec" 1206 "\<lbrakk>well_formed spec; pt_at obj_id spec\<rbrakk> \<Longrightarrow> real_object_at obj_id spec" 1207 "\<lbrakk>well_formed spec; frame_at obj_id spec\<rbrakk> \<Longrightarrow> real_object_at obj_id spec" 1208 apply (insert well_formed_object_at_irq_node_irq_node_at [where spec=spec and obj_id=obj_id]) 1209 apply (fastforce simp: real_object_at_def object_at_def object_type_is_object)+ 1210 done 1211 1212lemma well_formed_irq_node_slot_0: 1213 "\<lbrakk>well_formed spec; irq_id \<in> irq_nodes spec; 1214 opt_cap (irq_id, slot) spec = Some cap\<rbrakk> \<Longrightarrow> 1215 slot = 0" 1216 apply (frule opt_cap_cdl_objects, clarsimp) 1217 apply (frule (1) well_formed_well_formed_irq_node) 1218 apply (frule (1) object_slots_opt_cap, simp) 1219 apply (simp add: well_formed_irq_node_def dom_def, blast) 1220 done 1221 1222lemma well_formed_irq_nodes_cdl_irq_node: 1223 "cdl_irq_node spec irq \<in> irq_nodes spec \<Longrightarrow> irq_node_at (cdl_irq_node spec irq) spec" 1224 by (simp add: irq_nodes_def) 1225 1226lemma well_formed_cdl_irq_node_irq_nodes: 1227 "\<lbrakk>well_formed spec; cdl_objects spec (cdl_irq_node spec irq) = Some irq_node\<rbrakk> 1228 \<Longrightarrow> cdl_irq_node spec irq \<in> irq_nodes spec" 1229 apply (drule well_formed_well_formed_irq_table) 1230 apply (clarsimp simp: well_formed_irq_table_def) 1231 apply (fastforce simp: object_at_def) 1232 done 1233 1234lemma well_formed_irq_is_irq_node: 1235 "\<lbrakk>well_formed spec; cdl_objects spec (cdl_irq_node spec irq) = Some irq_node\<rbrakk> 1236 \<Longrightarrow> is_irq_node irq_node" 1237 apply (frule (1) well_formed_cdl_irq_node_irq_nodes) 1238 apply (clarsimp simp: irq_nodes_def object_at_def) 1239 done 1240 1241lemma well_formed_object_slots_irq_node: 1242 "\<lbrakk>well_formed spec; cdl_objects spec (cdl_irq_node spec irq) = Some irq_node\<rbrakk> 1243 \<Longrightarrow> dom (object_slots irq_node) = {0}" 1244 apply (frule (1) well_formed_cdl_irq_node_irq_nodes) 1245 apply (frule (1) well_formed_well_formed_irq_node) 1246 apply (clarsimp simp: well_formed_irq_node_def) 1247 done 1248 1249lemma well_formed_irq_ntfn_cap: 1250 "\<lbrakk>well_formed spec; 1251 irq \<in> bound_irqs spec; 1252 opt_cap (cdl_irq_node spec irq, 0) spec = Some ntfn_cap\<rbrakk> 1253 \<Longrightarrow> ntfn_cap = NotificationCap (cap_object ntfn_cap) 0 {AllowRead, AllowWrite}" 1254 apply (frule opt_cap_cdl_objects, clarsimp) 1255 apply (frule (1) well_formed_object_slots_irq_node [where irq=irq]) 1256 apply (frule (1) well_formed_well_formed_irq_node) 1257 apply (frule (1) well_formed_cdl_irq_node_irq_nodes) 1258 apply (clarsimp simp: well_formed_irq_node_def) 1259 apply (erule allE [where x=0]) 1260 apply (erule allE [where x=ntfn_cap]) 1261 apply (fastforce simp: bound_irqs_def opt_cap_def slots_of_def opt_object_def 1262 is_default_cap_def default_cap_def cap_object_def 1263 cap_has_object_def 1264 split: cdl_cap.splits) 1265 done 1266 1267lemma well_formed_bound_irqs_are_used_irqs: 1268 "well_formed spec \<Longrightarrow> bound_irqs spec \<subseteq> used_irqs spec" 1269 apply (frule well_formed_well_formed_irqhandler_caps) 1270 apply (fastforce simp: well_formed_irqhandler_caps_def used_irqs_def bound_irqs_def all_caps_def) 1271 done 1272 1273lemma well_formed_slots_of_used_irq_node: 1274 "\<lbrakk>well_formed spec; irq \<in> used_irqs spec\<rbrakk> 1275 \<Longrightarrow> dom (slots_of (cdl_irq_node spec irq) spec) = {0}" 1276 apply (clarsimp simp: used_irqs_def slots_of_def opt_object_def split: option.splits) 1277 apply (frule (2) well_formed_all_caps_cap_irq, clarsimp) 1278 apply (erule (1) well_formed_object_slots_irq_node) 1279 done 1280 1281lemma well_formed_slot_0_of_used_irq_node: 1282 "\<lbrakk>well_formed spec; irq \<in> used_irqs spec\<rbrakk> 1283 \<Longrightarrow> \<exists>ntfn_cap. slots_of (cdl_irq_node spec irq) spec 0 = Some ntfn_cap" 1284 apply (frule (1) well_formed_slots_of_used_irq_node) 1285 apply (clarsimp simp: dom_eq_singleton_conv) 1286 done 1287 1288lemma well_formed_object_slots_default_irq_node: 1289 "\<lbrakk>well_formed spec; cdl_objects spec (cdl_irq_node spec irq) = Some irq_node\<rbrakk> 1290 \<Longrightarrow> dom (object_slots (object_default_state irq_node)) = {0}" 1291 by (metis well_formed_object_slots well_formed_object_slots_irq_node) 1292 1293lemma object_slots_empty_cnode: 1294 "object_slots (CNode (empty_cnode sz)) = empty_cap_map sz" 1295 by (clarsimp simp: object_slots_def empty_cnode_def) 1296 1297lemma dom_empty_cap_map_singleton: 1298 "dom (empty_cap_map (sz)) = {0} \<Longrightarrow> sz = 0" 1299 apply (clarsimp simp: empty_cap_map_def) 1300 apply (subst (asm) atLeastLessThan_singleton [symmetric]) 1301 apply (drule atLeastLessThan_inj(2), simp+) 1302 done 1303 1304lemma well_formed_size_irq_node: 1305 "\<lbrakk>well_formed spec; cdl_objects spec (cdl_irq_node spec irq) = Some irq_node\<rbrakk> 1306 \<Longrightarrow> object_size_bits irq_node = 0" 1307 apply (frule (1) well_formed_irq_is_irq_node) 1308 apply (frule (1) well_formed_object_slots) 1309 apply (drule (1) well_formed_object_slots_default_irq_node) 1310 apply (clarsimp simp: object_default_state_def2 is_cnode_def object_slots_empty_cnode 1311 object_size_bits_def dom_empty_cap_map_singleton is_irq_node_def 1312 split: cdl_object.splits) 1313 done 1314 1315lemma well_formed_used_irqs_have_irq_node: 1316 "\<lbrakk>well_formed spec; irq \<in> used_irqs spec\<rbrakk> 1317 \<Longrightarrow> \<exists>irq_node. cdl_objects spec (cdl_irq_node spec irq) = Some irq_node" 1318 apply (clarsimp simp: used_irqs_def) 1319 apply (erule (2) well_formed_all_caps_cap_irq) 1320 done 1321 1322lemma well_formed_bound_irqs_have_irq_node: 1323 "\<lbrakk>well_formed spec; irq \<in> bound_irqs spec\<rbrakk> 1324 \<Longrightarrow> \<exists>irq_node. cdl_objects spec (cdl_irq_node spec irq) = Some irq_node" 1325 apply (frule well_formed_well_formed_irqhandler_caps) 1326 apply (clarsimp simp: well_formed_irqhandler_caps_def used_irqs_def bound_irqs_def all_caps_def) 1327 done 1328 1329lemma well_formed_irq_node_is_bound: 1330 "\<lbrakk>well_formed spec; cdl_objects spec (cdl_irq_node spec irq) = Some irq_node; 1331 object_slots irq_node 0 \<noteq> Some NullCap\<rbrakk> 1332 \<Longrightarrow> irq \<in> bound_irqs spec" 1333 apply (frule well_formed_well_formed_irqhandler_caps) 1334 apply (frule (1) well_formed_object_slots_default_irq_node) 1335 apply (frule (1) well_formed_object_slots) 1336 apply (clarsimp simp: well_formed_irqhandler_caps_def bound_irqs_def 1337 dom_eq_singleton_conv slots_of_def opt_object_def) 1338 done 1339 1340lemma well_formed_cap_object_cdl_irq_node: 1341 "\<lbrakk>well_formed spec; irq \<in> bound_irqs spec\<rbrakk> 1342 \<Longrightarrow> \<exists>obj. is_ntfn obj \<and> 1343 cdl_objects spec (cap_object (the (opt_cap (cdl_irq_node spec irq, 0) spec))) = Some obj" 1344 apply (frule well_formed_bound_irqs_are_used_irqs) 1345 apply (frule (1) well_formed_bound_irqs_have_irq_node, clarsimp) 1346 apply (frule well_formed_slot_0_of_used_irq_node [where irq=irq], fast) 1347 apply (clarsimp simp: opt_cap_def) 1348 apply (rename_tac cap) 1349 apply (frule (1) well_formed_irq_ntfn_cap, simp add: opt_cap_def) 1350 apply (frule well_formed_cap_object, simp add: opt_cap_def) 1351 apply (metis cap_has_object_simps(12)) 1352 apply clarsimp 1353 apply (frule well_formed_types_match [where obj_id = "cdl_irq_node spec irq" and slot = 0]) 1354 apply (simp add: opt_cap_def) 1355 apply simp 1356 apply (metis cap_has_object_simps(12)) 1357 apply (clarsimp simp: object_type_is_object cap_type_def split: cdl_cap.splits) 1358 done 1359 1360 1361 1362 1363 1364(* There are no untyped objects (as there are no untyped caps). *) 1365lemma well_formed_object_untyped: 1366 "\<lbrakk>well_formed spec; cdl_objects spec obj_id = Some object\<rbrakk> 1367 \<Longrightarrow> object_type object \<noteq> UntypedType" 1368 apply (case_tac "real_object_at obj_id spec") 1369 apply (frule (1) well_formed_cap_to_real_object) 1370 apply clarsimp 1371 apply (frule (1) well_formed_types_match, simp add: cap_has_object_def) 1372 apply (clarsimp simp: cap_has_object_def) 1373 apply (clarsimp simp: cap_type_def cap_has_object_def 1374 split: cdl_cap.splits) 1375 apply (frule (2) well_formed_is_untyped_cap) 1376 apply (clarsimp simp: cap_type_def) 1377 apply (clarsimp simp: real_object_at_def dom_def) 1378 apply (drule (2) well_formed_irq_nodes_object_type) 1379 apply simp 1380 done 1381 1382lemma well_formed_asidpool_at: 1383 "well_formed spec \<Longrightarrow> \<not> asidpool_at obj_id spec" 1384 apply (clarsimp simp: object_at_def object_type_is_object) 1385 apply (frule well_formed_cap_to_real_object [where obj_id=obj_id]) 1386 apply (clarsimp simp: real_object_at_def dom_def) 1387 apply (drule (2) well_formed_irq_nodes_object_type, simp) 1388 apply clarsimp 1389 apply (frule (2) well_formed_types_match [symmetric], clarsimp+) 1390 apply (frule (1) well_formed_well_formed_cap', clarsimp) 1391 apply (clarsimp simp: well_formed_cap_def cap_type_def 1392 split: cdl_cap.splits) 1393 done 1394 1395lemma well_formed_no_asidpools: 1396 "well_formed spec \<Longrightarrow> [obj \<leftarrow> obj_ids. asidpool_at obj spec] = []" 1397 by (clarsimp simp: filter_empty_conv well_formed_asidpool_at) 1398 1399 1400lemma well_formed_fake_pt_cap_in_pd: 1401 "\<lbrakk>well_formed spec; slots_of obj_id spec slot = Some cap; is_fake_pt_cap cap\<rbrakk> 1402 \<Longrightarrow> pd_at obj_id spec" 1403 apply (clarsimp simp: slots_of_def opt_object_def split: option.splits) 1404 apply (rename_tac obj) 1405 apply (frule well_formed_asidpool_at [where obj_id=obj_id]) 1406 apply (frule (1) well_formed_well_formed_vspace) 1407 apply (case_tac "is_cnode obj \<or> is_tcb obj \<or> is_irq_node obj") 1408 apply (frule (3) well_formed_is_fake_vm_cap) 1409 apply (clarsimp simp: is_fake_vm_cap_def is_fake_pt_cap_def split: cdl_cap.splits) 1410 apply clarsimp 1411 apply (clarsimp simp: object_at_def object_type_is_object) 1412 apply (case_tac obj, simp_all add: object_slots_def object_at_def object_type_is_object object_type_def) 1413 apply (clarsimp simp: well_formed_vspace_def) 1414 apply (erule allE [where x=slot]) 1415 apply (erule allE [where x=cap]) 1416 apply (clarsimp simp: is_fake_pt_cap_is_pt_cap object_slots_def) 1417 done 1418 1419lemma cap_has_object_cap_irq [simp]: 1420 "cap_has_object cap \<Longrightarrow> cap_irq cap = undefined" 1421 by (auto simp: cap_has_object_def cap_irq_def split: cdl_cap.splits) 1422 1423definition 1424 cap_at_to_real_object :: "cdl_cap_ref \<Rightarrow> cdl_state \<Rightarrow> bool" 1425where 1426 "cap_at_to_real_object cap_ref s = 1427 cap_at (\<lambda>cap. cap_has_object cap \<and> cap_object cap \<notin> irq_nodes s) cap_ref s" 1428(* FIXME: Why doesn't every cap pointing to an object not point to an IRQ Node? *) 1429 1430(* There is a bijection between objects and orig caps. *) 1431lemma well_formed_bij: 1432 "well_formed s \<Longrightarrow> 1433 bij_betw 1434 (\<lambda>cap_ref. cap_ref_object cap_ref s) 1435 {cap_ref. original_cap_at cap_ref s \<and> 1436 cap_at_to_real_object cap_ref s \<and> 1437 cnode_at (fst cap_ref) s} 1438 ((real_objects s))" 1439 apply (clarsimp simp: bij_betw_def) 1440 apply (rule conjI) 1441 apply (clarsimp simp: inj_on_def real_cap_ref_def cap_ref_object_def 1442 object_cap_ref_def cap_at_to_real_object_def cap_at_def) 1443 apply (erule_tac cap=cap and cap'=capa in well_formed_orig_caps_unique, 1444 (assumption|fastforce)+) 1445 apply (clarsimp simp: image_def) 1446 apply rule 1447 apply (clarsimp simp: real_cap_ref_def cap_ref_object_def object_cap_ref_def 1448 cap_at_to_real_object_def cap_at_def 1449 real_objects_def real_object_at_def) 1450 apply (erule (1) well_formed_cap_object, clarsimp) 1451 apply clarsimp 1452 apply (clarsimp simp: real_cap_ref_def cap_ref_object_def 1453 real_objects_def real_object_at_def) 1454 apply (frule_tac well_formed_cap_to_real_object, fastforce simp: real_object_at_def) 1455 apply (fastforce simp: cap_at_to_real_object_def cap_at_def) 1456 done 1457 1458lemma well_formed_irqhandler_bij: 1459 "well_formed s \<Longrightarrow> 1460 bij_betw (\<lambda>cap_ref. cap_ref_irq cap_ref s) 1461 {cap_ref. irqhandler_cap_at cap_ref s} 1462 (used_irqs s)" 1463 apply (clarsimp simp: bij_betw_def) 1464 apply (rule conjI) 1465 apply (clarsimp simp: inj_on_def real_cap_ref_def cap_ref_object_def 1466 object_cap_ref_def cap_at_to_real_object_def cap_at_def) 1467 apply (erule_tac cap=cap and cap'=capa in well_formed_irqhandler_caps_unique, 1468 (assumption|clarsimp simp: cap_ref_irq_def)+) 1469 apply (fastforce simp: image_def used_irqs_def cap_ref_irq_def cap_at_def all_caps_def) 1470 done 1471 1472lemma fake_cap_rewrite: 1473 "well_formed spec \<Longrightarrow> 1474 Set.filter (\<lambda>cap_ref. fake_pt_cap_at cap_ref spec) 1475 (SIGMA obj_id:{obj_id. pd_at obj_id spec}. 1476 dom (slots_of obj_id spec)) 1477 = {cap_ref. fake_pt_cap_at cap_ref spec}" 1478 apply (clarsimp simp: Set.filter_def cap_at_def opt_cap_def 1479 split: option.splits) 1480 apply (rule) 1481 apply clarsimp 1482 apply clarsimp 1483 apply (frule (2) well_formed_fake_pt_cap_in_pd) 1484 apply (fastforce) 1485 done 1486 1487lemma well_formed_fake_pt_caps_unique: 1488 "\<lbrakk>well_formed spec; pd_at obj_id spec; pd_at obj_id' spec; 1489 opt_cap (obj_id, slot) spec = Some cap; opt_cap (obj_id', slot') spec = Some cap'; 1490 is_fake_pt_cap cap; is_fake_pt_cap cap'; 1491 cap_object cap = cap_object cap'\<rbrakk> 1492 \<Longrightarrow> obj_id = obj_id' \<and> slot = slot'" 1493 by (fastforce simp: well_formed_def well_formed_fake_pt_caps_unique_def) 1494 1495lemma well_formed_fake_pt_caps_unique': 1496 "\<lbrakk>well_formed spec; pd_at obj_id spec; pd_at obj_id' spec; 1497 fake_pt_cap_at (obj_id, slot) spec; fake_pt_cap_at (obj_id', slot') spec; 1498 cap_ref_object (obj_id, slot) spec = cap_ref_object (obj_id', slot') spec\<rbrakk> 1499 \<Longrightarrow> obj_id = obj_id' \<and> slot = slot'" 1500 by (erule well_formed_fake_pt_caps_unique 1501 [where cap="the (opt_cap (obj_id, slot) spec)" and 1502 cap'="the (opt_cap (obj_id', slot') spec)"], 1503 (clarsimp simp: cap_ref_object_def cap_at_def)+) 1504 1505(* There is a bijection between pts and pts in pds. *) 1506lemma well_formed_pt_cap_bij: 1507 "well_formed spec \<Longrightarrow> 1508 bij_betw 1509 (\<lambda>cap_ref. cap_ref_object cap_ref spec) 1510 {(obj_id, slot). pd_at obj_id spec \<and> fake_pt_cap_at (obj_id, slot) spec} 1511 {obj_id. \<exists>cap. cap \<in> all_caps spec \<and> obj_id = cap_object cap \<and> is_fake_pt_cap cap}" 1512 apply (clarsimp simp: bij_betw_def) 1513 apply (rule conjI) 1514 apply (clarsimp simp: inj_on_def) 1515 apply (erule (5) well_formed_fake_pt_caps_unique') 1516 apply (rule) 1517 apply (clarsimp simp: cap_at_def) 1518 apply (rule_tac x=cap in exI) 1519 apply (rule conjI, clarsimp) 1520 apply (clarsimp simp: cap_ref_object_def cap_at_def) 1521 apply (clarsimp simp: image_def all_caps_def) 1522 apply (rename_tac obj_id slot) 1523 apply (rule_tac x=obj_id in exI) 1524 apply (rule conjI) 1525 apply (clarsimp simp: opt_cap_def) 1526 apply (erule (2) well_formed_fake_pt_cap_in_pd) 1527 apply (rule_tac x=slot in exI) 1528 apply (clarsimp simp: cap_ref_object_def cap_at_def) 1529 done 1530 1531lemma well_formed_objects_real_or_irq: 1532 "well_formed spec \<Longrightarrow> 1533 {obj_id. real_object_at obj_id spec} \<union> (cdl_irq_node spec ` used_irqs spec) = 1534 dom (cdl_objects spec)" 1535 apply (frule well_formed_well_formed_irqhandler_caps) 1536 apply (frule well_formed_inj_cdl_irq_node) 1537 apply (rule) 1538 apply clarsimp 1539 apply (rule conjI) 1540 apply (clarsimp simp: real_object_at_def object_at_def) 1541 apply (clarsimp simp: used_irqs_def all_caps_def opt_cap_def slots_of_def opt_object_def 1542 split: option.splits) 1543 apply (frule (2) well_formed_well_formed_cap_types_match, simp) 1544 apply (clarsimp simp: well_formed_cap_types_match_def) 1545 apply (clarsimp simp: real_object_at_def) 1546 apply (rule conjI) 1547 apply clarsimp 1548 apply clarsimp 1549 apply (frule (1) well_formed_cap_to_irq_object, simp add: irq_nodes_def) 1550 apply (fastforce simp: used_irqs_def all_caps_def dest!: injD) 1551 done 1552 1553lemma well_formed_objects_only_real_or_irq: 1554 "well_formed spec \<Longrightarrow> 1555 {obj_id. real_object_at obj_id spec} \<inter> (cdl_irq_node spec ` used_irqs spec) = {}" 1556 apply (subst disjoint_iff_not_equal, clarsimp) 1557 apply (frule (1) well_formed_used_irqs_have_irq_node, clarsimp) 1558 apply (frule (1) well_formed_cdl_irq_node_irq_nodes) 1559 apply (auto simp: real_object_at_def) 1560 done 1561 1562lemma well_formed_objects_card: 1563 "\<lbrakk>well_formed spec \<rbrakk> 1564 \<Longrightarrow> card (used_irqs spec) + card {x. real_object_at x spec} = card (dom (cdl_objects spec))" 1565 apply (frule well_formed_inj_cdl_irq_node) 1566 apply (frule well_formed_objects_real_or_irq) 1567 apply (frule well_formed_objects_only_real_or_irq) 1568 apply (subgoal_tac " card (used_irqs spec) = card (used_irq_nodes spec)", simp) 1569 apply (subst card_Un_Int, simp+) 1570 apply (metis Int_commute Nat.add_0_right Un_commute card_empty used_irq_nodes_def) 1571 by (metis card_image inj_inj_on used_irq_nodes_def) 1572 1573 1574(**************************************** 1575 * Packing data into a well_formed cap. * 1576 ****************************************) 1577 1578lemma update_cap_rights_and_data: 1579 "\<lbrakk>t (cap_object spec_cap) = Some client_object_id; \<not> is_untyped_cap spec_cap; 1580 well_formed_cap spec_cap; \<not> vm_cap_has_asid spec_cap; \<not> is_fake_vm_cap spec_cap; 1581 \<not> is_irqhandler_cap spec_cap; cap_type spec_cap = Some type\<rbrakk> 1582 \<Longrightarrow> update_cap_data_det 1583 (cap_data spec_cap) 1584 (update_cap_rights (cap_rights spec_cap) 1585 (default_cap type {client_object_id} (cnode_cap_size spec_cap) (is_device_cap spec_cap))) = 1586 update_cap_object client_object_id spec_cap" 1587 apply (case_tac "\<not>is_cnode_cap spec_cap") 1588 apply (case_tac spec_cap, simp_all add: cap_type_def, 1589 (fastforce simp: cap_data_def cap_rights_def default_cap_def 1590 update_cap_rights_def badge_update_def update_cap_badge_def 1591 update_cap_object_def update_cap_data_det_def 1592 well_formed_cap_def Word.less_mask_eq 1593 is_fake_vm_cap_def validate_vm_rights_def 1594 vm_read_write_def vm_read_only_def 1595 split: cdl_frame_cap_type.splits)+) 1596 apply (case_tac spec_cap, simp_all add: cap_type_def) 1597 apply (rename_tac word1 word2 nat1 nat2) 1598 apply (clarsimp simp: update_cap_data_det_def update_cap_rights_def 1599 default_cap_def well_formed_cap_def update_cap_object_def 1600 cap_rights_def cap_data_def cnode_cap_size_def) 1601 apply (case_tac "guard_as_rawdata (CNodeCap word1 word2 nat1 nat2) = 0") 1602 apply (clarsimp simp: guard_update_def guard_as_rawdata_def) 1603 apply (cut_tac p="word2 << 8" and d="of_nat nat1 << 3" and n=8 in is_aligned_add_or) 1604 apply (simp add: is_aligned_shiftl) 1605 apply (rule shiftl_less_t2n) 1606 apply (clarsimp simp: guard_bits_def word_of_nat_less) 1607 apply simp 1608 apply (clarsimp simp: word_or_zero) 1609 apply (drule word_shift_zero, erule less_imp_le) 1610 apply (clarsimp simp: guard_bits_def) 1611 apply (drule_tac m=8 in word_shift_zero, rule less_imp_le) 1612 apply (clarsimp simp: guard_bits_def word_of_nat_less) 1613 apply simp 1614 apply (clarsimp simp: of_nat_0 guard_bits_def word_bits_def) 1615 apply (clarsimp simp: badge_update_def cap_rights_def cap_data_def 1616 guard_update_def guard_as_rawdata_def) 1617 apply (cut_tac p="word2 << 8" and d="of_nat nat1 << 3" and n=8 in is_aligned_add_or) 1618 apply (simp add: is_aligned_shiftl) 1619 apply (rule shiftl_less_t2n) 1620 apply (clarsimp simp: guard_bits_def word_of_nat_less) 1621 apply simp 1622 apply (simp add: word_ao_dist shiftr_over_or_dist shiftl_shiftr1 word_size shiftl_mask_is_0 1623 word_bw_assocs mask_and_mask guard_as_rawdata_def guard_update_def) 1624 apply (subst le_mask_iff[THEN iffD1]) 1625 apply (rule plus_one_helper) 1626 apply (unfold mask_plus_1) 1627 apply (rule shiftl_less_t2n) 1628 apply (clarsimp simp: guard_bits_def word_of_nat_less) 1629 apply simp 1630 apply (subst less_mask_eq) 1631 apply (subst less_mask_eq) 1632 apply (clarsimp simp: guard_bits_def word_of_nat_less) 1633 apply (subst unat_of_nat32) 1634 apply (clarsimp simp: guard_bits_def word_bits_def) 1635 apply (clarsimp simp: min_def guard_bits_def) 1636 apply simp 1637 apply (subst less_mask_eq) 1638 apply (clarsimp simp: guard_bits_def word_of_nat_less) 1639 apply (clarsimp simp: guard_bits_def word_of_nat_less word_bits_def unat_of_nat32) 1640 done 1641 1642lemma update_cap_data: 1643 "\<lbrakk>t (cap_object spec_cap) = Some client_object_id; 1644 cap_type spec_cap = Some type; cap_data spec_cap = data; 1645 well_formed_cap spec_cap; \<not> is_untyped_cap spec_cap; 1646 \<not> vm_cap_has_asid spec_cap; \<not> is_fake_vm_cap spec_cap; \<not> is_irqhandler_cap spec_cap; 1647 cap_rights (default_cap type {obj_id} sz (is_device_cap spec_cap)) = cap_rights spec_cap; 1648 dev = is_device_cap spec_cap\<rbrakk> 1649 \<Longrightarrow> update_cap_data_det data (default_cap type {client_object_id} (cnode_cap_size spec_cap) dev) = 1650 update_cap_object client_object_id spec_cap" 1651 apply (frule (6) update_cap_rights_and_data) 1652 apply clarsimp 1653 apply (subgoal_tac "\<And>dev. update_cap_rights 1654 (cap_rights spec_cap) 1655 (default_cap type {client_object_id} (cnode_cap_size spec_cap) dev) 1656 = default_cap type {client_object_id} (cnode_cap_size spec_cap) dev") 1657 apply clarsimp 1658 apply (subst well_formed_update_cap_rights_idem) 1659 apply (erule (1) default_cap_well_formed_cap, simp) 1660 apply (subst cap_rights_default_cap_eq, fast) 1661 apply simp 1662 done 1663 1664end 1665 1666end 1667