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 11theory Dpolicy 12imports 13 "Access.Access" 14 "DRefine.Refine_D" 15 "DBaseRefine.Include_D" 16begin 17 18(* 19This file proves that the authority granted by any abstract state that 20satisfies the extended invariants agrees with the authority granted by the 21corresponding capDL state. This result is given by the final lemma in the file, 22pas_refined_transform. 23 24More details of this result and how it is used can be found in Section 6.1 of 25"Comprehensive Formal Verification of an OS Microkernel", which can be 26downloaded from 27https://ts.data61.csiro.au/publications/nictaabstracts/Klein_AEMSKH_14.abstract.pml 28*) 29 30context begin interpretation Arch . (*FIXME: arch_split*) 31 32definition 33 cdl_cap_auth_conferred :: "cdl_cap \<Rightarrow> auth set" 34where 35 "cdl_cap_auth_conferred cap \<equiv> 36 case cap of 37 cdl_cap.NullCap \<Rightarrow> {} 38 | cdl_cap.UntypedCap dev refs frange \<Rightarrow> {Control} 39 | cdl_cap.EndpointCap oref badge r \<Rightarrow> 40 cap_rights_to_auth r True 41 | cdl_cap.NotificationCap oref badge r \<Rightarrow> 42 cap_rights_to_auth (r - {AllowGrant}) False 43 | cdl_cap.ReplyCap oref \<Rightarrow> {Control} 44 | cdl_cap.MasterReplyCap oref \<Rightarrow> {Control} 45 | cdl_cap.CNodeCap oref bits guard sz \<Rightarrow> {Control} 46 | cdl_cap.TcbCap obj_ref \<Rightarrow> {Control} 47 | cdl_cap.DomainCap \<Rightarrow> {Control} 48 | cdl_cap.PendingSyncSendCap oref badge call grant fault \<Rightarrow> 49 {SyncSend} \<union> (if grant then {Access.Grant} else {}) 50 | cdl_cap.PendingSyncRecvCap oref fault \<Rightarrow> if fault then {} else {Receive} 51 | cdl_cap.PendingNtfnRecvCap oref \<Rightarrow> {Receive} 52 | cdl_cap.RestartCap \<Rightarrow> {} 53 | cdl_cap.IrqControlCap \<Rightarrow> {Control} 54 | cdl_cap.IrqHandlerCap irq \<Rightarrow> {Control} 55 | cdl_cap.FrameCap dev oref r sz is_real asid \<Rightarrow> vspace_cap_rights_to_auth r 56 | cdl_cap.PageTableCap oref is_real asid\<Rightarrow> {Control} 57 | cdl_cap.PageDirectoryCap oref is_real asid \<Rightarrow> {Control} 58 | cdl_cap.AsidControlCap \<Rightarrow> {Control} 59 | cdl_cap.AsidPoolCap oref asid \<Rightarrow> {Control} 60 | cdl_cap.ZombieCap ptr \<Rightarrow> {Control} 61 | cdl_cap.BoundNotificationCap word \<Rightarrow> {Receive, Reset} 62 | _ \<Rightarrow> {}" 63 64fun 65 cdl_obj_refs :: "cdl_cap \<Rightarrow> obj_ref set" 66where 67 "cdl_obj_refs cdl_cap.NullCap = {}" 68| "cdl_obj_refs (cdl_cap.UntypedCap dev rs frange) = rs" 69| "cdl_obj_refs (cdl_cap.EndpointCap r b cr) = {r}" 70| "cdl_obj_refs (cdl_cap.NotificationCap r b cr) = {r}" 71| "cdl_obj_refs (cdl_cap.ReplyCap r) = {r}" 72| "cdl_obj_refs (cdl_cap.MasterReplyCap r) = {r}" 73| "cdl_obj_refs (cdl_cap.CNodeCap r guard bits sz) = {r}" 74| "cdl_obj_refs (cdl_cap.TcbCap r) = {r}" 75| "cdl_obj_refs (cdl_cap.DomainCap) = UNIV" 76| "cdl_obj_refs (cdl_cap.PendingSyncSendCap r badge call guard fault) = {r}" 77| "cdl_obj_refs (cdl_cap.PendingSyncRecvCap r fault) = {r}" 78| "cdl_obj_refs (cdl_cap.PendingNtfnRecvCap r) = {r}" 79| "cdl_obj_refs cdl_cap.RestartCap = {}" 80| "cdl_obj_refs cdl_cap.IrqControlCap = {}" 81| "cdl_obj_refs (cdl_cap.IrqHandlerCap irq) = {}" 82| "cdl_obj_refs (cdl_cap.FrameCap dev x rs sz is_real asid) = ptr_range x sz" 83| "cdl_obj_refs (cdl_cap.PageDirectoryCap x is_real asid) = {x}" 84| "cdl_obj_refs (cdl_cap.PageTableCap x is_real asid) = {x}" 85| "cdl_obj_refs (cdl_cap.AsidPoolCap p asid) = {p}" 86| "cdl_obj_refs cdl_cap.AsidControlCap = {}" 87| "cdl_obj_refs (cdl_cap.ZombieCap ptr) = {ptr}" 88| "cdl_obj_refs (cdl_cap.BoundNotificationCap word) = {word}" 89| "cdl_obj_refs _ = {}" 90 91inductive_set 92 cdl_state_bits_to_policy for caps cdt 93where 94 csbta_caps: "\<lbrakk> caps ptr = Some cap; oref \<in> cdl_obj_refs cap; 95 auth \<in> cdl_cap_auth_conferred cap \<rbrakk> 96 \<Longrightarrow> (fst ptr, auth, oref) \<in> cdl_state_bits_to_policy caps cdt" 97| csbta_cdt: "\<lbrakk> cdt slot' = Some slot \<rbrakk> 98 \<Longrightarrow> (fst slot, Control, fst slot') \<in> cdl_state_bits_to_policy caps cdt" 99 100definition 101 "cdl_state_objs_to_policy s = cdl_state_bits_to_policy (\<lambda>ref. opt_cap ref s) 102 (cdl_cdt s)" 103 104fun 105 cdl_cap_irqs_controlled :: "cdl_cap \<Rightarrow> cdl_irq set" 106where 107 "cdl_cap_irqs_controlled cdl_cap.IrqControlCap = UNIV" 108 | "cdl_cap_irqs_controlled (cdl_cap.IrqHandlerCap irq) = {irq}" 109 | "cdl_cap_irqs_controlled _ = {}" 110 111inductive_set 112 cdl_state_irqs_to_policy_aux for aag caps 113where 114 csita_controlled: "\<lbrakk> caps ref = Some cap; irq \<in> cdl_cap_irqs_controlled cap \<rbrakk> 115 \<Longrightarrow> (pasObjectAbs aag (fst ref), Control, pasIRQAbs aag irq) \<in> 116 cdl_state_irqs_to_policy_aux aag caps" 117 118abbreviation 119 "cdl_state_irqs_to_policy aag s \<equiv> cdl_state_irqs_to_policy_aux aag 120 (\<lambda>ref. opt_cap ref s)" 121 122definition 123 transform_asid_rev :: "cdl_asid \<Rightarrow> asid" 124where 125 "transform_asid_rev asid = (of_nat (fst asid) << asid_low_bits) + of_nat (snd asid)" 126 127fun 128 cdl_cap_asid' :: "cdl_cap \<Rightarrow> asid set" 129where 130 "cdl_cap_asid' (Types_D.FrameCap _ _ _ _ _ asid) = (transform_asid_rev o fst) ` set_option asid" 131 | "cdl_cap_asid' (Types_D.PageTableCap _ _ asid) = (transform_asid_rev o fst) ` set_option asid" 132 | "cdl_cap_asid' (Types_D.PageDirectoryCap _ _ asid) = transform_asid_rev ` set_option asid" 133 | "cdl_cap_asid' (Types_D.AsidPoolCap _ asid) = 134 {x. fst (transform_asid x) = asid \<and> x \<noteq> 0}" 135 | "cdl_cap_asid' (Types_D.AsidControlCap) = UNIV" 136 | "cdl_cap_asid' _ = {}" 137 138definition 139 is_null_cap :: "cdl_cap \<Rightarrow> bool" 140where 141 "is_null_cap cap \<equiv> case cap of 142 cdl_cap.NullCap \<Rightarrow> True 143 | _ \<Rightarrow> False" 144 145inductive_set 146 cdl_state_asids_to_policy_aux for aag caps asid_tab 147where 148 csata_asid: "\<lbrakk> caps ptr = Some cap; asid \<in> cdl_cap_asid' cap \<rbrakk> \<Longrightarrow> 149 (pasObjectAbs aag (fst ptr), Control, pasASIDAbs aag asid) \<in> 150 cdl_state_asids_to_policy_aux aag caps asid_tab" 151 | csata_asid_lookup: "\<lbrakk> asid_tab (fst (transform_asid asid)) = Some poolcap; 152 \<not> is_null_cap poolcap; \<not> is_null_cap pdcap; pdptr = cap_object pdcap; 153 caps (cap_object poolcap, snd (transform_asid asid)) = Some pdcap \<rbrakk> \<Longrightarrow> 154 (pasASIDAbs aag asid, Control, pasObjectAbs aag pdptr) \<in> 155 cdl_state_asids_to_policy_aux aag caps asid_tab" 156 | csata_asidpool: "\<lbrakk> asid_tab (fst (transform_asid asid)) = Some poolcap; 157 \<not> is_null_cap poolcap; asid \<noteq> 0 \<rbrakk> \<Longrightarrow> 158 (pasObjectAbs aag (cap_object poolcap), ASIDPoolMapsASID, pasASIDAbs aag asid) \<in> 159 cdl_state_asids_to_policy_aux aag caps asid_tab" 160 161abbreviation 162 "cdl_state_asids_to_policy aag s \<equiv> cdl_state_asids_to_policy_aux aag 163 (\<lambda>ref. opt_cap ref s) (cdl_asid_table s)" 164 165definition 166 "cdl_irq_map_wellformed_aux aag irqs \<equiv> 167 \<forall>irq. pasObjectAbs aag (irqs irq) = pasIRQAbs aag irq" 168 169abbreviation 170 "cdl_irq_map_wellformed aag s \<equiv> cdl_irq_map_wellformed_aux aag (cdl_irq_node s)" 171 172inductive_set 173 cdl_domains_of_state_aux for cdl_heap 174where 175 domtcbs: "\<lbrakk> cdl_heap ptr = Some (Tcb cdl_tcb); 176 d = cdl_tcb_domain cdl_tcb\<rbrakk> 177 \<Longrightarrow> (ptr, d) \<in> cdl_domains_of_state_aux cdl_heap" | 178 domidle: "(idle_thread_ptr, default_domain) \<in> cdl_domains_of_state_aux cdl_heap" 179 180abbreviation 181 "cdl_domains_of_state s \<equiv> cdl_domains_of_state_aux (cdl_objects s)" 182 183definition 184 "cdl_tcb_domain_map_wellformed_aux aag tcbs_doms \<equiv> 185 \<forall>(ptr, d) \<in> tcbs_doms. pasObjectAbs aag ptr \<in> pasDomainAbs aag d" 186 187abbreviation 188 "cdl_tcb_domain_map_wellformed aag s \<equiv> 189 cdl_tcb_domain_map_wellformed_aux aag (cdl_domains_of_state s)" 190 191definition 192 pcs_refined :: "'a PAS \<Rightarrow> cdl_state \<Rightarrow> bool" 193where 194 "pcs_refined aag s \<equiv> 195 pas_wellformed aag 196 \<and> cdl_irq_map_wellformed aag s 197 \<and> cdl_tcb_domain_map_wellformed aag s 198 \<and> auth_graph_map (pasObjectAbs aag) (cdl_state_objs_to_policy s) \<subseteq> (pasPolicy aag) 199 \<and> cdl_state_asids_to_policy aag s \<subseteq> pasPolicy aag 200 \<and> cdl_state_irqs_to_policy aag s \<subseteq> pasPolicy aag" 201 202lemmas cdl_state_objs_to_policy_mem = eqset_imp_iff[OF cdl_state_objs_to_policy_def] 203 204lemmas cdl_state_objs_to_policy_intros 205 = cdl_state_bits_to_policy.intros[THEN cdl_state_objs_to_policy_mem[THEN iffD2]] 206 207lemmas csta_caps = cdl_state_objs_to_policy_intros(1) 208 and csta_cdt = cdl_state_objs_to_policy_intros(2) 209 210lemmas cdl_state_objs_to_policy_cases 211 = cdl_state_bits_to_policy.cases[OF cdl_state_objs_to_policy_mem[THEN iffD1]] 212 213lemma transform_asid_rev [simp]: 214 "asid \<le> 2 ^ ARM_A.asid_bits - 1 \<Longrightarrow> transform_asid_rev (transform_asid asid) = asid" 215 apply (clarsimp simp:transform_asid_def transform_asid_rev_def 216 asid_high_bits_of_def ARM_A.asid_low_bits_def) 217 apply (clarsimp simp:ucast_nat_def) 218 apply (subgoal_tac "asid >> 10 < 2 ^ asid_high_bits") 219 apply (simp add:ARM_A.asid_high_bits_def ARM_A.asid_bits_def) 220 apply (subst ucast_ucast_len) 221 apply simp 222 apply (subst shiftr_shiftl1) 223 apply simp 224 apply (subst ucast_ucast_mask) 225 apply (simp add:mask_out_sub_mask) 226 apply (simp add:ARM_A.asid_high_bits_def) 227 apply (rule shiftr_less_t2n[where m=7, simplified]) 228 apply (simp add:ARM_A.asid_bits_def) 229 done 230 231abbreviation 232 "valid_asid_mapping mapping \<equiv> (case mapping of 233 None \<Rightarrow> True 234 | Some (asid, ref) \<Rightarrow> asid \<le> 2 ^ ARM_A.asid_bits - 1)" 235 236lemma transform_asid_rev_transform_mapping [simp]: 237 "valid_asid_mapping mapping \<Longrightarrow> 238 (transform_asid_rev o fst) ` set_option (transform_mapping mapping) = fst ` set_option mapping" 239 apply (simp add:transform_mapping_def map_option_case) 240 apply (case_tac mapping) 241 apply clarsimp+ 242 done 243 244lemma fst_transform_cslot_ptr: 245 "fst ptr = fst (transform_cslot_ptr ptr)" 246 apply (case_tac ptr) 247 apply (clarsimp simp:transform_cslot_ptr_def) 248 done 249 250definition 251 transform_cslot_ptr_rev :: "cdl_cap_ref \<Rightarrow> cslot_ptr" 252where 253 "transform_cslot_ptr_rev \<equiv> \<lambda>(a, b). (a, the (nat_to_bl word_bits b))" 254 255lemma transform_cslot_pre_onto: 256 "snd ptr < 2 ^ word_bits \<Longrightarrow> \<exists>ptr'. ptr = transform_cslot_ptr ptr'" 257 apply (rule_tac x="transform_cslot_ptr_rev ptr" in exI) 258 apply (case_tac ptr) 259 apply (clarsimp simp: transform_cslot_ptr_def transform_cslot_ptr_rev_def) 260 apply (clarsimp simp: nat_to_bl_def bin_bl_bin' bintrunc_mod2p) 261 done 262 263definition 264 is_thread_state_cap :: "cdl_cap \<Rightarrow> bool" 265where 266 "is_thread_state_cap cap \<equiv> case cap of 267 cdl_cap.PendingSyncSendCap _ _ _ _ _ \<Rightarrow> True 268 | cdl_cap.PendingSyncRecvCap _ _ \<Rightarrow> True 269 | cdl_cap.PendingNtfnRecvCap _ \<Rightarrow> True 270 | cdl_cap.RestartCap \<Rightarrow> True 271 | cdl_cap.RunningCap \<Rightarrow> True 272 | _ \<Rightarrow> False" 273 274definition 275 is_bound_ntfn_cap :: "cdl_cap \<Rightarrow> bool" 276where 277 "is_bound_ntfn_cap cap \<equiv> case cap of 278 BoundNotificationCap a \<Rightarrow> True 279 | _ \<Rightarrow> False" 280 281definition 282 is_real_cap :: "cdl_cap \<Rightarrow> bool" 283where 284 "is_real_cap cap \<equiv> case cap of 285 cdl_cap.FrameCap _ _ _ _ Fake _ \<Rightarrow> False 286 | cdl_cap.PageTableCap _ Fake _ \<Rightarrow> False 287 | cdl_cap.PageDirectoryCap _ Fake _ \<Rightarrow> False 288 | _ \<Rightarrow> True" 289 290lemma is_real_cap_transform: 291 "cap = transform_cap cap' \<Longrightarrow> is_real_cap cap" 292 by (auto simp:transform_cap_def is_real_cap_def split:cap.splits arch_cap.splits) 293 294lemma is_real_cap_infer_tcb_pending_op: 295 "is_real_cap (infer_tcb_pending_op a tcb)" 296 by (auto simp:infer_tcb_pending_op_def is_real_cap_def split:Structures_A.thread_state.splits) 297 298lemma is_real_cap_infer_tcb_bound_notification: 299 "is_real_cap (infer_tcb_bound_notification a)" 300 by (auto simp: infer_tcb_bound_notification_def is_real_cap_def split: cdl_cap.splits option.splits) 301 302definition 303 is_untyped_cap :: "cdl_cap \<Rightarrow> bool" 304where 305 "is_untyped_cap cap \<equiv> case cap of 306 cdl_cap.UntypedCap _ _ _ \<Rightarrow> True 307 | _ \<Rightarrow> False" 308 309lemma valid_sched_etcbs[elim]: 310 "valid_sched s \<Longrightarrow> valid_etcbs s" 311 by (simp add: valid_sched_def) 312 313lemma caps_of_state_transform_opt_cap_rev: 314 "\<lbrakk> einvs s; opt_cap ptr (transform s) = Some cap; 315 is_real_cap cap; \<not> is_thread_state_cap cap; \<not> is_null_cap cap; \<not> is_bound_ntfn_cap cap \<rbrakk> \<Longrightarrow> 316 \<exists>cap' ptr'. cap = transform_cap cap' \<and> ptr = transform_cslot_ptr ptr' \<and> 317 caps_of_state s ptr' = Some cap'" 318 apply clarify 319 apply (drule invs_valid_objs) 320 apply (case_tac ptr) 321 apply (clarsimp simp:opt_cap_def transform_def transform_objects_def 322 transform_cslot_ptr_def slots_of_def opt_object_def) 323 apply (rule_tac P="a=idle_thread s" in case_split) 324 apply (clarsimp simp: map_add_def object_slots_def) 325 apply (case_tac "kheap s a") 326 apply (clarsimp simp: map_add_def object_slots_def) 327 apply (clarsimp simp:valid_objs_def dom_def) 328 apply (drule_tac x=a in spec, clarsimp) 329 apply (case_tac aa, simp_all add: object_slots_def caps_of_state_def2 nat_split_conv_to_if 330 split: if_split_asm) 331 apply (clarsimp simp:valid_obj_def valid_cs_def valid_cs_size_def) 332 apply (clarsimp simp:transform_cnode_contents_def) 333 apply (rule_tac x=z in exI, simp) 334 apply (rule_tac x="the (nat_to_bl 0 b)" in exI) 335 apply (clarsimp simp:option_map_join_def split:option.splits) 336 apply (rule nat_to_bl_to_bin, simp+) 337 apply (clarsimp simp:valid_obj_def valid_cs_def valid_cs_size_def) 338 apply (clarsimp simp:transform_cnode_contents_def) 339 apply (rule_tac x=z in exI, simp) 340 apply (rename_tac n list cap') 341 apply (rule_tac x="the (nat_to_bl n b)" in exI) 342 apply (clarsimp simp:option_map_join_def split:option.splits) 343 apply (rule nat_to_bl_to_bin, simp+) 344 apply (drule valid_etcbs_tcb_etcb [rotated], fastforce) 345 apply clarsimp 346 apply (clarsimp simp:transform_tcb_def tcb_slot_defs split:if_split_asm) 347 apply (clarsimp simp: is_null_cap_def is_bound_ntfn_cap_def infer_tcb_bound_notification_def 348 split: option.splits) 349 apply (simp add:is_thread_state_cap_def infer_tcb_pending_op_def is_null_cap_def is_real_cap_def 350 split:Structures_A.thread_state.splits option.splits) 351 apply (rule exI, rule conjI, simp, rule exI, rule conjI, 352 (rule bl_to_bin_tcb_cnode_index | rule bl_to_bin_tcb_cnode_index[symmetric]), 353 simp, simp add:tcb_cap_cases_def)+ 354 apply (rule exI, rule conjI, simp) 355 apply (rule_tac x="tcb_cnode_index 0" in exI) 356 apply (subst bl_to_bin_tcb_cnode_index_le0; simp) 357 apply (rename_tac arch_kernel_obj) 358 apply (case_tac arch_kernel_obj; simp) 359 apply (clarsimp simp:transform_asid_pool_contents_def unat_map_def split:if_split_asm) 360 apply (clarsimp simp:is_real_cap_def is_null_cap_def transform_asid_pool_entry_def 361 split:option.splits) 362 apply (clarsimp simp:transform_page_table_contents_def unat_map_def split:if_split_asm) 363 apply (clarsimp simp:is_real_cap_def is_null_cap_def transform_pte_def 364 split:ARM_A.pte.splits) 365 apply (clarsimp simp:transform_page_directory_contents_def unat_map_def split:if_split_asm) 366 apply (clarsimp simp:is_real_cap_def is_null_cap_def transform_pde_def 367 split:ARM_A.pde.splits) 368 done 369 370abbreviation 371 "get_size cap \<equiv> case cap of 372 cdl_cap.FrameCap _ _ _ sz _ _ \<Rightarrow> sz 373 | cdl_cap.PageTableCap _ _ _ \<Rightarrow> 0" 374 375lemma opt_cap_None_word_bits: 376 "\<lbrakk> einvs s; snd ptr \<ge> 2 ^ word_bits \<rbrakk> \<Longrightarrow> opt_cap ptr (transform s) = None" 377 apply (case_tac ptr) 378 apply (clarsimp simp:opt_cap_def transform_def transform_objects_def slots_of_def opt_object_def) 379 apply (rule_tac P="a=idle_thread s" in case_split) 380 apply (clarsimp simp: map_add_def object_slots_def) 381 apply (case_tac "kheap s a") 382 apply (clarsimp simp: map_add_def object_slots_def) 383 apply (drule invs_valid_objs) 384 apply (simp add:object_slots_def valid_objs_def) 385 apply (case_tac aa, simp_all add: nat_split_conv_to_if 386 split: if_split_asm) 387 apply (clarsimp simp:transform_cnode_contents_def object_slots_def) 388 apply (drule_tac x=a in bspec) 389 apply (simp add:dom_def)+ 390 apply (clarsimp simp:valid_obj_def valid_cs_def valid_cs_size_def) 391 apply (rule conjI) 392 apply (clarsimp simp:option_map_join_def nat_to_bl_def) 393 apply (metis gr0I le_antisym less_eq_Suc_le less_eq_nat.simps(1) 394 lt_word_bits_lt_pow zero_less_Suc) 395 apply (clarsimp simp:option_map_join_def nat_to_bl_def) 396 apply (drule not_le_imp_less) 397 apply (subgoal_tac "b < 2 ^ word_bits") 398 apply simp 399 apply (rule less_trans) 400 apply simp 401 apply (rule power_strict_increasing, simp+) 402 apply (frule valid_etcbs_tcb_etcb[rotated], fastforce) 403 apply (clarsimp simp:transform_tcb_def tcb_slot_defs word_bits_def) 404 apply (rename_tac arch_kernel_obj) 405 apply (case_tac arch_kernel_obj; simp) 406 apply (simp add:transform_asid_pool_contents_def transform_page_table_contents_def 407 transform_page_directory_contents_def unat_map_def word_bits_def)+ 408 done 409 410lemma opt_cap_Some_rev: 411 "\<lbrakk> einvs s; opt_cap ptr (transform s) = Some cap \<rbrakk> \<Longrightarrow> \<exists>ptr'. ptr = transform_cslot_ptr ptr'" 412 apply (rule transform_cslot_pre_onto) 413 apply (subst not_le[symmetric]) 414 apply (rule notI) 415 apply (drule_tac ptr=ptr in opt_cap_None_word_bits; simp) 416 done 417 418lemma obj_refs_transform: 419 "\<not> (\<exists>x sz i dev. cap = cap.UntypedCap dev x sz i) \<Longrightarrow> obj_refs cap = cdl_obj_refs (transform_cap cap)" 420 apply (case_tac cap; clarsimp) 421 apply (rename_tac arch_cap) 422 apply (case_tac arch_cap; clarsimp) 423 done 424 425lemma untyped_range_transform: 426 "(\<exists>x sz i dev. cap = cap.UntypedCap dev x sz i) \<Longrightarrow> untyped_range cap = cdl_obj_refs (transform_cap cap)" 427 by auto 428 429lemma cap_auth_conferred_transform: 430 "cap_auth_conferred cap = cdl_cap_auth_conferred (transform_cap cap)" 431 apply (case_tac cap; clarsimp simp:cap_auth_conferred_def cdl_cap_auth_conferred_def) 432 apply (rename_tac arch_cap) 433 apply (case_tac arch_cap; clarsimp simp:is_page_cap_def) 434 done 435 436lemma thread_states_transform: 437 "\<lbrakk> einvs s; (oref', auth) \<in> thread_states s oref \<rbrakk> \<Longrightarrow> 438 (oref, auth, oref') \<in> cdl_state_objs_to_policy (transform s)" 439 apply clarify 440 apply (simp add:thread_states_def tcb_states_of_state_def) 441 apply (cases "get_tcb oref s") 442 apply simp+ 443 apply (frule valid_etcbs_get_tcb_get_etcb[rotated], fastforce) 444 apply clarsimp 445 apply (rule_tac cap="infer_tcb_pending_op oref (tcb_state a)" in csta_caps[where ptr="(oref, 5)" 446 and auth=auth and oref=oref' and s="transform s", simplified]) 447 apply (rule opt_cap_tcb[where sl=5, unfolded tcb_slot_defs, simplified]) 448 apply simp 449 apply simp 450 apply (rule notI, drule invs_valid_idle, simp add:valid_idle_def pred_tcb_def2) 451 apply (simp add:infer_tcb_pending_op_def, case_tac "tcb_state a", 452 (simp add:if_split_asm| erule disjE)+) 453 apply (simp add:infer_tcb_pending_op_def cdl_cap_auth_conferred_def, 454 case_tac "tcb_state a", (simp add:if_split_asm| erule disjE)+) 455 done 456 457lemma thread_bound_ntfns_transform: 458 "\<lbrakk> einvs s; thread_bound_ntfns s oref = Some oref'; auth \<in> {Receive, Reset} \<rbrakk> \<Longrightarrow> 459 (oref, auth, oref') \<in> cdl_state_objs_to_policy (transform s)" 460 apply clarify 461 apply (simp add: thread_bound_ntfns_def ) 462 apply (cases "get_tcb oref s") 463 apply simp+ 464 apply (frule valid_etcbs_get_tcb_get_etcb[rotated], fastforce) 465 apply clarsimp 466 apply (rule_tac cap="infer_tcb_bound_notification (tcb_bound_notification a)" in csta_caps[where ptr="(oref, tcb_boundntfn_slot)" 467 and auth=auth and oref=oref' and s="transform s", simplified]) 468 apply (unfold tcb_boundntfn_slot_def) 469 apply (rule opt_cap_tcb[where sl=6, unfolded tcb_boundntfn_slot_def tcb_pending_op_slot_def tcb_slot_defs, simplified]) 470 apply simp 471 apply simp 472 apply (rule notI, drule invs_valid_idle, simp add:valid_idle_def pred_tcb_def2) 473 apply (clarsimp simp: infer_tcb_bound_notification_def cdl_cap_auth_conferred_def)+ 474 done 475 476lemma thread_state_cap_transform_tcb: 477 "\<lbrakk> opt_cap ptr (transform s) = Some cap; is_thread_state_cap cap \<rbrakk> \<Longrightarrow> 478 \<exists>tcb. get_tcb (fst ptr) s = Some tcb" 479 apply (case_tac ptr) 480 apply (simp add:opt_cap_def slots_of_def opt_object_def transform_def transform_objects_def) 481 apply (rule_tac P="a = idle_thread s" in case_split) 482 apply (clarsimp simp: map_add_def object_slots_def) 483 apply (case_tac "kheap s (fst ptr)") 484 apply (clarsimp simp: map_add_def object_slots_def) 485 apply (simp add:get_tcb_def object_slots_def) 486 apply (case_tac aa, simp_all add: nat_split_conv_to_if 487 split: if_split_asm) 488 apply (clarsimp simp:transform_cnode_contents_def) 489 apply (case_tac z, simp_all add:is_thread_state_cap_def split:if_split_asm) 490 apply (rename_tac arch_cap) 491 apply (case_tac arch_cap; simp) 492 apply (clarsimp simp:transform_cnode_contents_def) 493 apply (case_tac z, simp_all add:is_thread_state_cap_def split:if_split_asm) 494 apply (rename_tac arch_cap) 495 apply (case_tac arch_cap; simp) 496 apply (rename_tac arch_kernel_obj) 497 apply (case_tac arch_kernel_obj; simp) 498 apply (clarsimp simp:transform_asid_pool_contents_def unat_map_def transform_asid_pool_entry_def 499 split:if_split_asm option.splits) 500 apply (clarsimp simp:transform_page_table_contents_def unat_map_def transform_pte_def 501 split:if_split_asm ARM_A.pte.splits) 502 apply (clarsimp simp:transform_page_directory_contents_def unat_map_def transform_pde_def 503 split:if_split_asm ARM_A.pde.splits) 504 done 505 506 507lemma not_is_bound_ntfn_cap_transform_cap[simp]: "\<not>is_bound_ntfn_cap (transform_cap cn)" 508 apply (case_tac cn; simp add: is_bound_ntfn_cap_def) 509 apply (rename_tac foo) 510 apply (case_tac foo; simp) 511done 512 513lemma thread_bound_ntfn_cap_transform_tcb: 514 "\<lbrakk> opt_cap ptr (transform s) = Some cap; is_bound_ntfn_cap cap \<rbrakk> \<Longrightarrow> 515 \<exists>tcb. get_tcb (fst ptr) s = Some tcb" 516 apply (case_tac ptr) 517 apply (simp add:opt_cap_def slots_of_def opt_object_def transform_def transform_objects_def) 518 apply (rule_tac P="a = idle_thread s" in case_split) 519 apply (clarsimp simp: map_add_def object_slots_def) 520 apply (case_tac "kheap s (fst ptr)") 521 apply (clarsimp simp: map_add_def object_slots_def) 522 apply (simp add:get_tcb_def object_slots_def) 523 apply (case_tac aa, simp_all) 524 apply (case_tac x11; simp) 525 apply (clarsimp simp:transform_cnode_contents_def) 526 apply (clarsimp simp:transform_cnode_contents_def) 527 apply (rename_tac arch_obj) 528 apply (case_tac arch_obj;clarsimp simp:transform_asid_pool_contents_def unat_map_def split:if_split_asm) 529 apply (clarsimp simp:transform_asid_pool_entry_def is_bound_ntfn_cap_def split:option.splits) 530 apply (clarsimp simp:transform_page_table_contents_def unat_map_def transform_pte_def is_bound_ntfn_cap_def 531 split:if_split_asm ARM_A.pte.splits) 532 apply (clarsimp simp:transform_page_directory_contents_def unat_map_def transform_pde_def is_bound_ntfn_cap_def 533 split:if_split_asm ARM_A.pde.splits) 534 done 535 536 537lemma thread_states_transform_rev: 538 "\<lbrakk> einvs s; opt_cap ptr (transform s) = Some cap; is_thread_state_cap cap; 539 oref \<in> cdl_obj_refs cap; auth \<in> cdl_cap_auth_conferred cap; (fst ptr) \<noteq> idle_thread s \<rbrakk> \<Longrightarrow> 540 (oref, auth) \<in> thread_states s (fst ptr)" 541 apply (frule thread_state_cap_transform_tcb, simp) 542 apply (case_tac ptr) 543 apply (clarsimp simp:thread_states_def tcb_states_of_state_def) 544 apply (frule valid_etcbs_get_tcb_get_etcb[rotated], fastforce) 545 apply (frule_tac sl=b in opt_cap_tcb, assumption, simp) 546 apply (clarsimp split:if_split_asm) 547 apply (case_tac "aa tcb", simp_all add:is_thread_state_cap_def split:if_split_asm) 548 apply (rename_tac arch_cap) 549 apply (case_tac "arch_cap", simp_all split:if_split_asm) 550 apply (case_tac "tcb_state tcb", auto simp:infer_tcb_pending_op_def cdl_cap_auth_conferred_def 551 infer_tcb_bound_notification_def split: option.splits) 552 done 553 554lemma thread_bound_ntfns_transform_rev: 555 "\<lbrakk> einvs s; opt_cap ptr (transform s) = Some cap; is_bound_ntfn_cap cap; 556 oref \<in> cdl_obj_refs cap; auth \<in> cdl_cap_auth_conferred cap; (fst ptr) \<noteq> idle_thread s \<rbrakk> \<Longrightarrow> 557 thread_bound_ntfns s (fst ptr) = Some oref" 558 apply (frule thread_bound_ntfn_cap_transform_tcb, simp) 559 apply (case_tac ptr) 560 apply (clarsimp simp:thread_bound_ntfns_def) 561 apply (frule valid_etcbs_get_tcb_get_etcb[rotated], fastforce) 562 apply (frule_tac sl=b in opt_cap_tcb, assumption, simp) 563 apply (clarsimp split:if_split_asm) 564 apply (case_tac "tcb"; simp add:is_thread_state_cap_def is_bound_ntfn_cap_def split:if_split_asm) 565 apply (rename_tac arch_cap) 566 apply (case_tac "arch_cap", simp_all split:if_split_asm) 567 apply (clarsimp simp: infer_tcb_pending_op_def split: Structures_A.thread_state.splits) 568 apply (case_tac "tcb_bound_notification tcb", 569 auto simp: infer_tcb_pending_op_def cdl_cap_auth_conferred_def 570 infer_tcb_bound_notification_def 571 split: option.splits) 572 done 573 574lemma idle_thread_null_cap: 575 "\<lbrakk> invs s; caps_of_state s ptr = Some cap; fst ptr = idle_thread s \<rbrakk> \<Longrightarrow> cap = cap.NullCap" 576 apply (rule_tac s=s and v="snd ptr" in valid_idle_has_null_cap, 577 (simp add:invs_def valid_state_def)+) 578 apply (drule_tac s="fst x" for x in sym, simp) 579 done 580 581lemma idle_thread_no_authority: 582 "\<lbrakk> invs s; caps_of_state s ptr = Some cap; auth \<in> cap_auth_conferred cap \<rbrakk> \<Longrightarrow> 583 fst ptr \<noteq> idle_thread s" 584 apply (rule notI) 585 apply (drule idle_thread_null_cap, simp+) 586 apply (simp add:cap_auth_conferred_def) 587 done 588 589lemma idle_thread_no_untyped_range: 590 "\<lbrakk> invs s; caps_of_state s ptr = Some cap; auth \<in> untyped_range cap \<rbrakk> \<Longrightarrow> fst ptr \<noteq> idle_thread s" 591 apply (rule notI) 592 apply (drule idle_thread_null_cap, simp+) 593 done 594 595lemma fst': 596 "(a :: cdl_object_id) = fst (a, b)" 597 apply simp 598 done 599 600lemma opt_cap_pt_Some': 601 "\<lbrakk> valid_idle s; kheap s a = Some (ArchObj (arch_kernel_obj.PageTable fun)) \<rbrakk> 602 \<Longrightarrow> (opt_cap (a, unat slot) (transform s)) = Some (transform_pte (fun slot))" 603 apply (clarsimp simp:opt_cap_def transform_def slots_of_def opt_object_def object_slots_def 604 transform_objects_def map_add_def restrict_map_def not_idle_thread_def) 605 apply (frule arch_obj_not_idle,simp) 606 apply (clarsimp simp:transform_page_table_contents_def unat_map_def not_idle_thread_def) 607 apply (rule unat_lt2p[where 'a=8, simplified]) 608 done 609 610lemma pte_cdl_obj_refs: 611 "\<lbrakk> pte_ref pte = Some (a, b, c); ptr \<in> ptr_range a b \<rbrakk> \<Longrightarrow> 612 ptr \<in> cdl_obj_refs (transform_pte pte)" 613 apply (case_tac pte; simp add: pte_ref_def transform_pte_def) 614 done 615 616lemma pte_cdl_cap_auth_conferred: 617 "\<lbrakk> pte_ref pte = Some (a, b, c); auth \<in> c \<rbrakk> \<Longrightarrow> 618 auth \<in> cdl_cap_auth_conferred (transform_pte pte)" 619 apply (case_tac pte; simp add: pte_ref_def transform_pte_def cdl_cap_auth_conferred_def) 620 done 621 622lemma opt_cap_pd_Some': 623 "\<lbrakk> valid_idle s; kheap s a = Some (ArchObj (arch_kernel_obj.PageDirectory fun)); 624 slot < ucast (kernel_base >> 20) \<rbrakk> \<Longrightarrow> 625 (opt_cap (a, unat slot) (transform s)) = Some (transform_pde (fun slot))" 626 apply (clarsimp simp:opt_cap_def transform_def slots_of_def opt_object_def object_slots_def 627 transform_objects_def restrict_map_def map_add_def not_idle_thread_def) 628 apply (frule arch_obj_not_idle,simp) 629 apply (clarsimp simp:transform_page_directory_contents_def unat_map_def not_idle_thread_def 630 kernel_pde_mask_def word_not_le[symmetric]) 631 apply (rule unat_lt2p[where 'a="12", simplified]) 632 done 633 634lemma pde_cdl_obj_refs: 635 "\<lbrakk> pde_ref2 pde = Some (a, b, c); ptr \<in> ptr_range a b \<rbrakk> \<Longrightarrow> 636 ptr \<in> cdl_obj_refs (transform_pde pde)" 637 apply (case_tac pde; simp add: pde_ref2_def transform_pde_def ptr_range_def) 638 done 639 640lemma pde_cdl_cap_auth_conferred: 641 "\<lbrakk> pde_ref2 pde = Some (a, b, c); auth \<in> c \<rbrakk> \<Longrightarrow> 642 auth \<in> cdl_cap_auth_conferred (transform_pde pde)" 643 apply (case_tac pde; simp add: pde_ref2_def transform_pde_def cdl_cap_auth_conferred_def) 644 done 645 646lemma state_vrefs_transform: 647 "\<lbrakk> invs s; ptr \<noteq> idle_thread s; (ptr', ref, auth) \<in> state_vrefs s ptr \<rbrakk> \<Longrightarrow> 648 (ptr, auth, ptr') \<in> cdl_state_objs_to_policy (transform s)" 649 apply (simp add:state_vrefs_def, case_tac "kheap s ptr", simp+) 650 apply (case_tac a, simp_all add:vs_refs_no_global_pts_def) 651 apply (rename_tac arch_kernel_obj) 652 apply (case_tac arch_kernel_obj; simp add: vs_refs_no_global_pts_def) 653 apply (clarsimp simp:graph_of_def) 654 apply (subst fst') 655 apply (rule csta_caps) 656 apply (drule_tac asid="ucast aa" in opt_cap_asid_pool_Some[rotated]) 657 apply (simp add:invs_valid_idle) 658 apply (simp add:ucast_up_ucast_id is_up_def source_size_def target_size_def word_size) 659 apply (simp add:transform_asid_pool_entry_def) 660 apply (simp add:transform_asid_pool_entry_def cdl_cap_auth_conferred_def) 661 apply (clarsimp simp:graph_of_def) 662 apply (subst fst') 663 apply (rule csta_caps) 664 apply (drule_tac slot=aa in opt_cap_pt_Some'[rotated]) 665 apply (simp add:invs_valid_idle) 666 apply simp 667 apply (rule_tac a=ab and b=ac and c=b in pte_cdl_obj_refs, simp+) 668 apply (rule_tac a=ab and b=ac and c=b in pte_cdl_cap_auth_conferred, simp+) 669 apply (erule bexE) 670 apply (clarsimp simp:graph_of_def) 671 apply (subst fst') 672 apply (rule csta_caps) 673 apply (drule_tac slot=aa in opt_cap_pd_Some'[rotated]) 674 apply (simp add:word_not_le[symmetric]) 675 apply (simp add:invs_valid_idle) 676 apply simp 677 apply (rule_tac a=ab and b=ac and c=b in pde_cdl_obj_refs, simp+) 678 apply (rule_tac a=ab and b=ac and c=b in pde_cdl_cap_auth_conferred, simp+) 679 done 680 681lemma pte_ref_transform_rev: 682 "ptr' \<in> cdl_obj_refs (transform_pte pte) \<Longrightarrow> 683 pte_ref pte = Some (cap_object (transform_pte pte), get_size (transform_pte pte), 684 cdl_cap_auth_conferred (transform_pte pte)) \<and> 685 ptr' \<in> ptr_range (cap_object (transform_pte pte)) (get_size (transform_pte pte))" 686 apply (case_tac pte) 687 apply (simp_all add:pte_ref_def transform_pte_def 688 vspace_cap_rights_to_auth_def cdl_cap_auth_conferred_def) 689 done 690 691lemma pde_ref_transform_rev: 692 "ptr' \<in> cdl_obj_refs (transform_pde pde) \<Longrightarrow> 693 pde_ref2 pde = Some (cap_object (transform_pde pde), get_size (transform_pde pde), 694 cdl_cap_auth_conferred (transform_pde pde)) \<and> 695 ptr' \<in> ptr_range (cap_object (transform_pde pde)) (get_size (transform_pde pde))" 696 apply (case_tac pde) 697 apply (simp_all add:pde_ref2_def transform_pde_def ptr_range_def 698 vspace_cap_rights_to_auth_def cdl_cap_auth_conferred_def) 699 done 700 701lemma state_vrefs_transform_rev: 702 "\<lbrakk> einvs s; opt_cap ptr (transform s) = Some cap; ptr' \<in> cdl_obj_refs cap; 703 auth \<in> cdl_cap_auth_conferred cap; \<not> is_real_cap cap \<rbrakk> \<Longrightarrow> 704 \<exists>ref. (ptr', ref, auth) \<in> state_vrefs s (fst ptr)" 705 apply (case_tac ptr, clarsimp) 706 apply (subgoal_tac "a \<noteq> idle_thread s") 707 prefer 2 708 apply (clarsimp simp:state_vrefs_def transform_def transform_objects_def 709 opt_cap_def slots_of_def opt_object_def) 710 apply (clarsimp simp: map_add_def object_slots_def) 711 apply (case_tac "kheap s a") 712 apply (clarsimp simp: state_vrefs_def transform_def transform_objects_def 713 opt_cap_def slots_of_def opt_object_def) 714 apply (clarsimp simp: map_add_def object_slots_def) 715 apply (clarsimp simp:state_vrefs_def transform_def transform_objects_def 716 opt_cap_def slots_of_def opt_object_def) 717 apply (case_tac aa, simp_all add: transform_object_def object_slots_def nat_split_conv_to_if 718 split: if_split_asm) 719 apply (clarsimp simp:transform_cnode_contents_def is_real_cap_transform) 720 apply (clarsimp simp:transform_cnode_contents_def is_real_cap_transform) 721 apply (frule valid_etcbs_tcb_etcb [rotated], fastforce) 722 apply (clarsimp simp: transform_tcb_def is_real_cap_transform is_real_cap_infer_tcb_pending_op 723 is_real_cap_infer_tcb_bound_notification 724 split:if_split_asm) 725 apply (rename_tac arch_kernel_obj) 726 apply (case_tac arch_kernel_obj, simp_all add:vs_refs_no_global_pts_def graph_of_def) 727 apply (clarsimp simp:transform_asid_pool_contents_def unat_map_def split:if_split_asm) 728 apply (rule exI) 729 apply (rename_tac "fun") 730 apply (case_tac "fun (of_nat b)") 731 apply (clarsimp simp:transform_asid_pool_entry_def) 732 apply (rule_tac x="(of_nat b, ptr')" in image_eqI) 733 apply (clarsimp simp:transform_asid_pool_entry_def cdl_cap_auth_conferred_def) 734 apply simp 735 apply (clarsimp simp:transform_asid_pool_entry_def) 736 apply (clarsimp simp:transform_page_table_contents_def unat_map_def split:if_split_asm) 737 apply (rule exI)+ 738 apply (drule pte_ref_transform_rev) 739 apply safe[1] 740 apply simp 741 apply (rule_tac x="(ptr', auth)" in image_eqI) 742 apply simp 743 apply simp 744 apply (clarsimp simp:transform_page_directory_contents_def unat_map_def split:if_split_asm) 745 apply (subgoal_tac "(of_nat b :: 12 word) < ucast (kernel_base >> 20)") 746 prefer 2 747 apply (subst word_not_le[symmetric]) 748 apply (rule notI) 749 apply (clarsimp simp:kernel_pde_mask_def transform_pde_def) 750 apply (simp add:kernel_pde_mask_def not_less[symmetric]) 751 apply (rule exI) 752 apply (drule pde_ref_transform_rev, clarsimp) 753 apply (rule bexI) 754 prefer 2 755 apply fastforce 756 apply clarsimp 757 apply (rule_tac x="(ptr', auth)" in image_eqI) 758 apply simp 759 apply simp 760 done 761 762lemma cdl_cdt_transform_rev: 763 "\<lbrakk> invs s; cdl_cdt (transform s) slot' = Some slot \<rbrakk> \<Longrightarrow> 764 \<exists>ptr' ptr. slot' = transform_cslot_ptr ptr' \<and> slot = transform_cslot_ptr ptr \<and> 765 cdt s ptr' = Some ptr" 766 apply (clarsimp simp:cdt_transform map_lift_over_def split:if_split_asm) 767 apply (rule_tac x=a in exI, rule_tac x=b in exI) 768 apply (subst (asm) inv_into_f_f) 769 apply (rule subset_inj_on) 770 apply (simp add:dom_def)+ 771 done 772 773lemma state_objs_transform: 774 "\<lbrakk> einvs s; (x, a, y) \<in> state_objs_to_policy s \<rbrakk> \<Longrightarrow> 775 (x, a, y) \<in> cdl_state_objs_to_policy (transform s)" 776 apply (rule state_objs_to_policy_cases, simp) 777 apply (simp add:fst_transform_cslot_ptr) 778 apply (rule_tac ptr="transform_cslot_ptr ptr" and auth=auth and oref=oref and 779 cap="transform_cap cap" and s="transform s" in csta_caps) 780 apply (rule caps_of_state_transform_opt_cap) 781 apply simp 782 apply fastforce 783 apply (simp add:idle_thread_no_authority) 784 apply (case_tac cap; simp) 785 apply (rename_tac arch_cap) 786 apply (case_tac arch_cap; simp) 787 apply (simp add:cap_auth_conferred_transform) 788 apply (simp add:fst_transform_cslot_ptr) 789 apply (rule_tac ptr="transform_cslot_ptr ptr" and auth=Control and oref=oref and 790 cap="transform_cap cap" and s="transform s" in csta_caps) 791 apply (rule caps_of_state_transform_opt_cap) 792 apply simp 793 apply fastforce 794 apply (simp add:idle_thread_no_untyped_range) 795 apply (case_tac cap, (simp add:untyped_range_transform del:untyped_range.simps(1))+) 796 apply (case_tac cap, (simp add:cdl_cap_auth_conferred_def)+) 797 apply (rule thread_states_transform, simp+) 798apply (rule thread_bound_ntfns_transform, simp+) 799 apply (simp add:fst_transform_cslot_ptr) 800 apply (rule_tac slot="transform_cslot_ptr slot" and slot'="transform_cslot_ptr slot'" 801 and s="transform s" in csta_cdt) 802 apply (simp add:transform_def) 803 apply (rule transform_cdt_some) 804 apply (simp add:invs_mdb_cte) 805 apply simp 806 apply (subgoal_tac "ptr \<noteq> idle_thread s") 807 apply (simp add:state_vrefs_transform) 808 apply (clarsimp simp:state_vrefs_def vs_refs_no_global_pts_def invs_def valid_state_def 809 valid_idle_def pred_tcb_at_def obj_at_def) 810 done 811 812lemma state_objs_transform_rev: 813 "\<lbrakk> einvs s; (x, a, y) \<in> cdl_state_objs_to_policy (transform s) \<rbrakk> \<Longrightarrow> 814 (x, a, y) \<in> state_objs_to_policy s" 815 apply (rule cdl_state_objs_to_policy_cases, simp) 816 apply (rule_tac P="is_thread_state_cap cap" in case_split) 817 apply simp 818 apply (rule sta_ts) 819 apply (rule thread_states_transform_rev, simp+) 820 apply (clarsimp simp:opt_cap_def transform_def transform_objects_def slots_of_def opt_object_def) 821 apply (clarsimp simp: map_add_def object_slots_def) 822 apply (rule_tac P="is_real_cap cap" in case_split[rotated]) 823 apply (drule state_vrefs_transform_rev, simp+) 824 apply clarsimp 825 apply (rule sta_vref) 826 apply simp 827 apply (subgoal_tac "\<not> is_null_cap cap") 828 prefer 2 829 apply (clarsimp simp:is_null_cap_def split:cdl_cap.splits) 830 apply (rule_tac P="is_bound_ntfn_cap cap" in case_split) 831 apply simp 832 apply (rule sta_bas) 833 apply (rule thread_bound_ntfns_transform_rev, simp+) 834 apply (clarsimp simp: opt_cap_def transform_def transform_objects_def slots_of_def opt_object_def) 835 apply (clarsimp simp: map_add_def object_slots_def) 836 apply (clarsimp simp: cdl_cap_auth_conferred_def is_bound_ntfn_cap_def split: cdl_cap.splits) 837 apply (frule caps_of_state_transform_opt_cap_rev, simp+) 838 apply (rule_tac P="is_untyped_cap cap" in case_split) 839 apply (subgoal_tac "a = Control") 840 apply clarsimp 841 apply (subst fst_transform_cslot_ptr[symmetric]) 842 apply (rule_tac cap=cap' in sta_untyped) 843 apply simp 844 apply (subst (asm) untyped_range_transform[symmetric]) 845 apply (simp add:is_untyped_cap_def transform_cap_def 846 split:cap.splits arch_cap.splits if_split_asm) 847 apply simp 848 apply (simp add:cdl_cap_auth_conferred_def is_untyped_cap_def split:cdl_cap.splits) 849 apply clarsimp 850 apply (subst fst_transform_cslot_ptr[symmetric]) 851 apply (rule_tac cap=cap' in sta_caps) 852 apply simp 853 apply (subst (asm) obj_refs_transform[symmetric]) 854 apply (simp add:is_untyped_cap_def transform_cap_def 855 split:cap.splits arch_cap.splits if_split_asm) 856 apply simp 857 apply (simp add:cap_auth_conferred_transform) 858 apply (drule cdl_cdt_transform_rev [rotated], simp+) 859 apply clarsimp 860 apply (subst fst_transform_cslot_ptr[symmetric])+ 861 apply (rule sta_cdt) 862 apply simp 863 done 864 865lemma state_vrefs_asidpool_control: 866 "(pdptr, VSRef asid (Some AASIDPool), auth) \<in> 867 state_vrefs s poolptr \<Longrightarrow> auth = Control" 868 apply (clarsimp simp:state_vrefs_def ) 869 apply (cases "kheap s poolptr") 870 apply clarsimp 871 apply (simp add: vs_refs_no_global_pts_def, case_tac a; clarsimp) 872 apply (rename_tac arch_kernel_obj) 873 apply (case_tac arch_kernel_obj; clarsimp) 874 done 875 876lemma idle_thread_no_asid: 877 "\<lbrakk> invs s; caps_of_state s ptr = Some cap; 878 asid \<in> cap_asid' cap \<rbrakk> \<Longrightarrow> fst ptr \<noteq> idle_thread s" 879 apply (rule notI) 880 apply (drule idle_thread_null_cap, simp+) 881 done 882 883lemma asid_table_entry_transform: 884 "arm_asid_table (arch_state s) (asid_high_bits_of asid) = poolptr \<Longrightarrow> 885 cdl_asid_table (transform s) (fst (transform_asid asid)) = 886 Some (transform_asid_table_entry poolptr)" 887 apply (clarsimp simp:transform_def transform_asid_table_def unat_map_def 888 transform_asid_table_entry_def transform_asid_def) 889 apply (simp add:transform_asid_def asid_high_bits_of_def asid_low_bits_def) 890 apply (rule unat_lt2p[where 'a=7, simplified]) 891 done 892 893lemma transform_asid_high_bits_of: 894 "of_nat (fst (transform_asid asid)) = asid_high_bits_of asid" 895 apply (clarsimp simp:transform_asid_def asid_high_bits_of_def) 896 done 897 898lemma transform_asid_high_bits_of': 899 "fst (transform_asid asid) = unat (asid_high_bits_of asid)" 900 apply (clarsimp simp:transform_asid_def asid_high_bits_of_def) 901 done 902 903lemma transform_asid_low_bits_of: 904 "of_nat (snd (transform_asid asid)) = (ucast asid :: 10 word)" 905 apply (clarsimp simp:transform_asid_def) 906 done 907 908lemma cap_asid'_transform: 909 "\<lbrakk> invs s; caps_of_state s ptr = Some cap \<rbrakk> \<Longrightarrow> cap_asid' cap = cdl_cap_asid' (transform_cap cap)" 910 apply (case_tac cap; simp) 911 apply (drule caps_of_state_valid, simp) 912 apply (rename_tac arch_cap) 913 apply (case_tac arch_cap; simp) 914 apply (clarsimp simp:transform_asid_high_bits_of' valid_cap_def split:option.splits)+ 915 done 916 917lemma state_asids_transform: 918 "\<lbrakk> einvs s; (x, a, y) \<in> state_asids_to_policy aag s \<rbrakk> \<Longrightarrow> 919 (x, a, y) \<in> cdl_state_asids_to_policy aag (transform s)" 920 apply (drule state_asids_to_policy_aux.induct) 921 prefer 4 922 apply simp 923 apply (simp add: fst_transform_cslot_ptr) 924 apply (rule_tac cap="transform_cap cap" in csata_asid) 925 apply (rule caps_of_state_transform_opt_cap) 926 apply simp 927 apply fastforce 928 apply (clarsimp simp: idle_thread_no_asid) 929 apply (fastforce simp: cap_asid'_transform) 930 apply (frule state_vrefs_asidpool_control, simp) 931 apply (simp add: state_vrefs_def, case_tac "kheap s poolptr", simp_all) 932 apply (case_tac aa, simp_all add:vs_refs_no_global_pts_def) 933 apply (rename_tac arch_kernel_obj) 934 apply (case_tac arch_kernel_obj, simp_all add:graph_of_def, safe) 935 apply (rule_tac pdcap="cdl_cap.PageDirectoryCap b Fake None" in csata_asid_lookup) 936 apply (simp add: asid_table_entry_transform) 937 apply (simp add: is_null_cap_def transform_asid_table_entry_def) 938 apply (simp add: is_null_cap_def transform_asid_table_entry_def) 939 apply (simp add: ucast_up_ucast_id is_up_def source_size_def target_size_def word_size) 940 apply (simp add: transform_asid_table_entry_def) 941 apply (drule_tac asid="asid" in opt_cap_asid_pool_Some[rotated]) 942 apply (simp add: invs_valid_idle) 943 apply (subst (asm) mask_asid_low_bits_ucast_ucast) 944 apply (subst (asm) up_ucast_inj_eq) 945 apply simp 946 apply (simp add: transform_asid_pool_entry_def) 947 apply (cut_tac aag=aag and asid=asid and asid_tab="cdl_asid_table (transform s)" in csata_asidpool) 948 apply (clarsimp simp: transform_def transform_asid_table_def unat_map_def) 949 apply safe[1] 950 apply (simp add: transform_asid_table_entry_def transform_asid_high_bits_of) 951 apply (simp add: transform_asid_def unat_lt2p[where 'a=7, simplified]) 952 apply (simp add: is_null_cap_def) 953 apply simp 954 apply simp 955 done 956 957lemma opt_cap_Some_asid_real: 958 "\<lbrakk> opt_cap ref (transform s) = Some cap; asid \<in> cdl_cap_asid' cap; einvs s \<rbrakk> \<Longrightarrow> is_real_cap cap" 959 apply (case_tac ref) 960 apply (clarsimp simp:opt_cap_def transform_def transform_objects_def slots_of_def opt_object_def) 961 apply (rule_tac P="a=idle_thread s" in case_split) 962 apply (clarsimp simp: map_add_def object_slots_def) 963 apply (case_tac "kheap s a") 964 apply (clarsimp simp: map_add_def object_slots_def) 965 apply (case_tac aa, simp_all add:object_slots_def valid_objs_def nat_split_conv_to_if 966 split: if_split_asm) 967 apply (clarsimp simp:transform_cnode_contents_def is_real_cap_transform) 968 apply (clarsimp simp:transform_cnode_contents_def is_real_cap_transform) 969 apply (frule valid_etcbs_tcb_etcb[rotated], fastforce) 970 apply (clarsimp simp: transform_tcb_def tcb_slot_defs is_real_cap_infer_tcb_bound_notification 971 is_real_cap_transform is_real_cap_infer_tcb_pending_op 972 split: if_split_asm) 973 apply (rename_tac arch_kernel_obj) 974 apply (case_tac arch_kernel_obj; simp) 975 apply (clarsimp simp:transform_asid_pool_contents_def unat_map_def split:if_split_asm) 976 apply (clarsimp simp:transform_asid_pool_entry_def split:option.splits) 977 apply (clarsimp simp:transform_page_table_contents_def unat_map_def split:if_split_asm) 978 apply (clarsimp simp:transform_pte_def split:ARM_A.pte.splits) 979 apply (clarsimp simp:transform_page_directory_contents_def unat_map_def split:if_split_asm) 980 apply (clarsimp simp:transform_pde_def split:ARM_A.pde.splits) 981 done 982 983lemma state_vrefs_asid_pool_transform_rev: 984 "\<lbrakk> einvs s; cdl_asid_table (transform s) (fst (transform_asid asid)) = Some poolcap; 985 \<not> is_null_cap poolcap; \<not> is_null_cap pdcap; pdptr = cap_object pdcap; 986 opt_cap (cap_object poolcap, snd (transform_asid asid)) (transform s) = Some pdcap \<rbrakk> \<Longrightarrow> 987 (pdptr, VSRef (asid && mask ARM_A.asid_low_bits) (Some AASIDPool), Control) 988 \<in> state_vrefs s (cap_object poolcap)" 989 apply (subgoal_tac "cap_object poolcap \<noteq> idle_thread s") 990 prefer 2 991 apply (clarsimp simp:state_vrefs_def transform_def transform_objects_def 992 opt_cap_def slots_of_def opt_object_def) 993 apply (clarsimp simp: map_add_def object_slots_def) 994 apply (case_tac "kheap s (cap_object poolcap)") 995 apply (clarsimp simp:state_vrefs_def transform_def transform_objects_def 996 opt_cap_def slots_of_def opt_object_def) 997 apply (clarsimp simp: map_add_def object_slots_def) 998 apply (clarsimp simp:transform_asid_high_bits_of') 999 apply (simp add:asid_table_transform transform_asid_table_entry_def is_null_cap_def 1000 split:option.splits) 1001 apply (clarsimp simp:state_vrefs_def transform_def transform_objects_def 1002 opt_cap_def slots_of_def opt_object_def) 1003 apply (drule invs_valid_asid_table) 1004 apply (clarsimp simp:valid_asid_table_def) 1005 apply (drule bspec) 1006 apply fastforce 1007 apply (case_tac a, simp_all add:transform_object_def object_slots_def) 1008 apply (clarsimp simp:obj_at_def a_type_def split:if_split_asm)+ 1009 apply (rename_tac arch_kernel_obj) 1010 apply (case_tac arch_kernel_obj; simp add:vs_refs_no_global_pts_def graph_of_def) 1011 apply (simp add:transform_asid_pool_contents_def unat_map_def transform_asid_low_bits_of 1012 split:if_split_asm) 1013 apply (rule_tac x="(ucast asid, cap_object pdcap)" in image_eqI) 1014 apply (simp add:mask_asid_low_bits_ucast_ucast) 1015 apply (clarsimp simp:transform_asid_pool_entry_def split:option.splits) 1016 done 1017 1018lemma state_asids_transform_rev: 1019 "\<lbrakk> einvs s; (x, a, y) \<in> cdl_state_asids_to_policy aag (transform s) \<rbrakk> \<Longrightarrow> 1020 (x, a, y) \<in> state_asids_to_policy aag s" 1021 apply (erule cdl_state_asids_to_policy_aux.induct) 1022 apply (rule_tac P="is_thread_state_cap cap" in case_split) 1023 apply (clarsimp simp:is_thread_state_cap_def split:cdl_cap.splits) 1024 apply (rule_tac P="is_bound_ntfn_cap cap" in case_split) 1025 apply (clarsimp simp: is_bound_ntfn_cap_def split: cdl_cap.splits) 1026 apply (rule_tac P="\<not> is_real_cap cap" in case_split) 1027 apply (clarsimp simp:opt_cap_Some_asid_real) 1028 apply (rule_tac P="is_null_cap cap" in case_split) 1029 apply (clarsimp simp:is_null_cap_def split:cdl_cap.splits) 1030 apply (frule caps_of_state_transform_opt_cap_rev, simp+) 1031 apply clarsimp 1032 apply (subst fst_transform_cslot_ptr[symmetric]) 1033 apply (rule sata_asid) 1034 apply simp 1035 apply (simp add:cap_asid'_transform) 1036 apply (rule_tac poolptr="cap_object poolcap" in sata_asid_lookup) 1037 apply (clarsimp simp:transform_asid_high_bits_of') 1038 apply (simp add:asid_table_transform transform_asid_table_entry_def is_null_cap_def 1039 split:option.splits) 1040 apply (drule_tac t=poolcap in sym) 1041 apply simp 1042 apply (rule state_vrefs_asid_pool_transform_rev, simp_all) 1043 apply (rule sata_asidpool) 1044 apply (clarsimp simp:transform_asid_high_bits_of') 1045 apply (simp add:asid_table_transform transform_asid_table_entry_def is_null_cap_def 1046 split:option.splits) 1047 apply (drule_tac t=poolcap in sym) 1048 apply simp 1049 apply simp 1050 done 1051 1052lemma idle_thread_no_irqs: 1053 "\<lbrakk> invs s; caps_of_state s ptr = Some cap; 1054 irq \<in> cap_irqs_controlled cap \<rbrakk> \<Longrightarrow> fst ptr \<noteq> idle_thread s" 1055 apply (rule notI) 1056 apply (drule idle_thread_null_cap, simp+) 1057 done 1058 1059lemma cap_irqs_controlled_transform: 1060 "cap_irqs_controlled cap = cdl_cap_irqs_controlled (transform_cap cap)" 1061 apply (case_tac cap; simp) 1062 apply (rename_tac arch_cap) 1063 apply (case_tac arch_cap; simp) 1064 done 1065 1066lemma state_irqs_transform: 1067 "\<lbrakk> einvs s; (x, a, y) \<in> state_irqs_to_policy aag s \<rbrakk> \<Longrightarrow> 1068 (x, a, y) \<in> cdl_state_irqs_to_policy aag (transform s)" 1069 apply (erule state_irqs_to_policy_aux.induct) 1070 apply (simp add: fst_transform_cslot_ptr) 1071 apply (rule_tac cap="transform_cap cap" in csita_controlled) 1072 apply (rule caps_of_state_transform_opt_cap) 1073 apply simp 1074 apply fastforce 1075 apply (clarsimp simp:idle_thread_no_irqs) 1076 apply (simp add: cap_irqs_controlled_transform) 1077 done 1078 1079lemma state_irqs_transform_rev: 1080 "\<lbrakk> einvs s; (x, a, y) \<in> cdl_state_irqs_to_policy aag (transform s) \<rbrakk> \<Longrightarrow> 1081 (x, a, y) \<in> state_irqs_to_policy aag s" 1082 apply (erule cdl_state_irqs_to_policy_aux.induct) 1083 apply (rule_tac P="is_thread_state_cap cap" in case_split) 1084 apply (clarsimp simp:is_thread_state_cap_def split:cdl_cap.splits) 1085 apply (rule_tac P="is_bound_ntfn_cap cap" in case_split) 1086 apply (clarsimp simp:is_bound_ntfn_cap_def split:cdl_cap.splits) 1087 apply (rule_tac P="\<not> is_real_cap cap" in case_split) 1088 apply (clarsimp simp:is_real_cap_def split:cdl_cap.splits) 1089 apply (rule_tac P="is_null_cap cap" in case_split) 1090 apply (clarsimp simp:is_null_cap_def split:cdl_cap.splits) 1091 apply (frule caps_of_state_transform_opt_cap_rev, simp+) 1092 apply clarsimp 1093 apply (subst fst_transform_cslot_ptr[symmetric]) 1094 apply (rule_tac cap=cap' in sita_controlled) 1095 apply simp 1096 apply (simp add:cap_irqs_controlled_transform) 1097 done 1098 1099lemma irq_map_wellformed_transform: 1100 "irq_map_wellformed aag s = cdl_irq_map_wellformed aag (transform s)" 1101 apply (clarsimp simp:irq_map_wellformed_aux_def cdl_irq_map_wellformed_aux_def 1102 transform_def) 1103 done 1104 1105lemma einvs_idle: 1106 "einvs s \<Longrightarrow> idle_thread s = idle_thread_ptr" 1107 by (simp add: invs_def valid_state_def valid_idle_def) 1108 1109lemma einvs_idle_domain: 1110 "einvs s \<Longrightarrow> \<exists>etcb. ekheap s idle_thread_ptr = Some etcb \<and> tcb_domain etcb = default_domain" 1111 apply (clarsimp simp: valid_sched_def valid_idle_etcb_def etcb_at_def 1112 valid_etcbs_def invs_def valid_state_def valid_idle_def pred_tcb_at_def obj_at_def is_etcb_at_def 1113 split: option.splits) 1114 apply (erule_tac x="idle_thread s" in allE) 1115 apply simp 1116 done 1117 1118lemma cdl_domains_of_state_transform: 1119 assumes e: "einvs s" 1120 shows "cdl_domains_of_state (transform s) = domains_of_state s" 1121proof - 1122 { fix ptr d 1123 assume "(ptr, d) \<in> cdl_domains_of_state (transform s)" 1124 hence "(ptr, d) \<in> domains_of_state s" 1125 apply (cases) 1126 using e 1127 apply (clarsimp simp: transform_def transform_objects_def restrict_map_def 1128 split: if_split_asm Structures_A.kernel_object.splits) 1129 apply (case_tac z, simp_all add: nat_split_conv_to_if 1130 split: if_split_asm) 1131 prefer 2 1132 apply (rename_tac arch_kernel_obj) 1133 apply (case_tac arch_kernel_obj; simp) 1134 apply (drule valid_etcbs_tcb_etcb [rotated], fastforce) 1135 apply clarsimp 1136 apply (rule domains_of_state_aux.intros, assumption) 1137 apply (clarsimp simp: transform_tcb_def transform_full_intent_def Let_def) 1138 apply (insert einvs_idle [OF e]) 1139 apply (insert einvs_idle_domain [OF e]) 1140 apply clarsimp 1141 apply (erule domains_of_state_aux.domtcbs) 1142 apply simp 1143 done 1144 } 1145 note a = this 1146 { 1147 fix ptr d 1148 assume "(ptr, d) \<in> domains_of_state s" 1149 hence "(ptr, d) \<in> cdl_domains_of_state (transform s)" 1150 apply cases 1151 apply (case_tac "ptr = idle_thread_ptr") 1152 apply (insert einvs_idle [OF e])[1] 1153 apply (insert einvs_idle_domain [OF e])[1] 1154 apply simp 1155 apply (rule domidle) 1156 apply (frule ekheap_kheap_dom) 1157 using e apply fastforce 1158 apply clarsimp 1159 apply (drule (1) cdl_objects_tcb) 1160 apply (insert einvs_idle [OF e])[1] 1161 apply simp 1162 apply (erule domtcbs) 1163 apply (clarsimp simp: transform_full_intent_def Let_def) 1164 done 1165 } 1166 note b = this 1167 show ?thesis 1168 apply (rule set_eqI) 1169 apply clarify 1170 apply (blast intro!: a b) 1171 done 1172qed 1173 1174lemma tcb_domain_map_wellformed_transform: 1175 "einvs s \<Longrightarrow> 1176 tcb_domain_map_wellformed aag s = cdl_tcb_domain_map_wellformed aag (transform s)" 1177 by (clarsimp simp: tcb_domain_map_wellformed_aux_def cdl_tcb_domain_map_wellformed_aux_def 1178 cdl_domains_of_state_transform) 1179 1180lemma pas_refined_transform: 1181 "einvs s \<Longrightarrow> pas_refined aag s = pcs_refined aag (transform s)" 1182 apply (clarsimp simp:pcs_refined_def pas_refined_def irq_map_wellformed_transform tcb_domain_map_wellformed_transform) 1183 apply safe 1184 apply (rule subsetD, simp) 1185 apply (clarsimp simp:auth_graph_map_mem) 1186 apply (rule_tac x="x'" in exI, clarsimp, rule_tac x="y'" in exI, clarsimp) 1187 apply (clarsimp simp:state_objs_transform_rev) 1188 apply (rule_tac A="state_asids_to_policy aag s" in subsetD, simp) 1189 apply (clarsimp simp:state_asids_transform_rev) 1190 apply (rule_tac A="state_irqs_to_policy aag s" in subsetD, simp) 1191 apply (clarsimp simp:state_irqs_transform_rev) 1192 apply (rule subsetD, simp) 1193 apply (clarsimp simp:auth_graph_map_mem) 1194 apply (rule_tac x="x'" in exI, clarsimp, rule_tac x="y'" in exI, clarsimp) 1195 apply (clarsimp simp:state_objs_transform) 1196 apply (rule_tac A="cdl_state_asids_to_policy aag (transform s)" in subsetD, simp) 1197 apply (clarsimp simp:state_asids_transform) 1198 apply (rule_tac A="cdl_state_irqs_to_policy aag (transform s)" in subsetD, simp) 1199 apply (clarsimp simp:state_irqs_transform) 1200 done 1201 1202end 1203 1204end 1205