1(* 2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3 * 4 * SPDX-License-Identifier: GPL-2.0-only 5 *) 6 7theory Arch_AC 8imports Retype_AC 9begin 10 11context begin interpretation Arch . (*FIXME: arch_split*) 12 13text\<open> 14 15Arch-specific access control. 16 17\<close> 18 19lemma store_pde_respects: 20 "\<lbrace>integrity aag X st and K (is_subject aag (p && ~~ mask pd_bits)) \<rbrace> 21 store_pde p pde 22 \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>" 23 apply (simp add: store_pde_def set_pd_def) 24 apply (wp get_object_wp set_object_integrity_autarch) 25 apply simp 26 done 27 28lemma store_pte_respects: 29 "\<lbrace>integrity aag X st and K (is_subject aag (p && ~~ mask pt_bits)) \<rbrace> 30 store_pte p pte 31 \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>" 32 apply (simp add: store_pte_def set_pt_def) 33 apply (wp get_object_wp set_object_integrity_autarch) 34 apply simp 35 done 36 37lemma integrity_arch_state [iff]: 38 "\<lbrakk>arm_asid_table v = arm_asid_table (arch_state s)\<rbrakk> \<Longrightarrow> 39 integrity aag X st (s\<lparr>arch_state := v\<rparr>) = integrity aag X st s" 40 unfolding integrity_def 41 by (simp ) 42 43lemma integrity_arm_asid_map [iff]: 44 "integrity aag X st (s\<lparr>arch_state := ((arch_state s)\<lparr>arm_asid_map := v\<rparr>)\<rparr>) = integrity aag X st s" 45 unfolding integrity_def 46 by (simp ) 47 48lemma integrity_arm_hwasid_table [iff]: 49 "integrity aag X st (s\<lparr>arch_state := ((arch_state s)\<lparr>arm_hwasid_table := v\<rparr>)\<rparr>) = integrity aag X st s" 50 unfolding integrity_def 51 by (simp ) 52 53lemma integrity_arm_next_asid [iff]: 54 "integrity aag X st (s\<lparr>arch_state := ((arch_state s)\<lparr>arm_next_asid := v\<rparr>)\<rparr>) = integrity aag X st s" 55 unfolding integrity_def 56 by (simp ) 57 58declare dmo_mol_respects [wp] 59 60crunch respects[wp]: arm_context_switch "integrity X aag st" 61 (simp: dmo_bind_valid dsb_def isb_def writeTTBR0_def invalidateLocalTLB_ASID_def 62 setHardwareASID_def set_current_pd_def 63 ignore: do_machine_op) 64 65crunch respects[wp]: set_vm_root "integrity X aag st" 66 (wp: crunch_wps 67 simp: set_current_pd_def isb_def dsb_def writeTTBR0_def dmo_bind_valid crunch_simps 68 ignore: do_machine_op) 69 70crunch respects[wp]: set_vm_root_for_flush "integrity X aag st" 71 (wp: crunch_wps simp: set_current_pd_def crunch_simps ignore: do_machine_op) 72 73crunch respects[wp]: flush_table "integrity X aag st" 74 (wp: crunch_wps simp: invalidateLocalTLB_ASID_def crunch_simps ignore: do_machine_op) 75 76crunch respects[wp]: page_table_mapped "integrity X aag st" 77 78lemma kheap_eq_state_vrefsD: 79 "kheap s p = Some ko \<Longrightarrow> state_vrefs s p = vs_refs_no_global_pts ko" 80 by (simp add: state_vrefs_def) 81 82lemma kheap_eq_state_vrefs_pas_refinedD: 83 "\<lbrakk> kheap s p = Some ko; 84 (p', r, a) \<in> vs_refs_no_global_pts ko; pas_refined aag s \<rbrakk> 85 \<Longrightarrow> (pasObjectAbs aag p, a, pasObjectAbs aag p') \<in> pasPolicy aag" 86 apply (drule kheap_eq_state_vrefsD) 87 apply (erule pas_refined_mem[OF sta_vref, rotated]) 88 apply simp 89 done 90 91lemma find_pd_for_asid_authority1: 92 "\<lbrace>pas_refined aag\<rbrace> 93 find_pd_for_asid asid 94 \<lbrace>\<lambda>pd s. (pasASIDAbs aag asid, Control, pasObjectAbs aag pd) \<in> pasPolicy aag\<rbrace>,-" 95 apply (rule hoare_pre) 96 apply (simp add: find_pd_for_asid_def) 97 apply (wp | wpc)+ 98 apply (clarsimp simp: obj_at_def pas_refined_def) 99 apply (erule subsetD, erule sata_asid_lookup) 100 apply (simp add: state_vrefs_def vs_refs_no_global_pts_def image_def) 101 apply (rule rev_bexI, erule graph_ofI) 102 apply (simp add: mask_asid_low_bits_ucast_ucast) 103 done 104 105lemma find_pd_for_asid_authority2: 106 "\<lbrace>\<lambda>s. \<forall>pd. (\<forall>aag. pas_refined aag s \<longrightarrow> (pasASIDAbs aag asid, Control, pasObjectAbs aag pd) \<in> pasPolicy aag) 107 \<and> (pspace_aligned s \<and> valid_vspace_objs s \<longrightarrow> is_aligned pd pd_bits) 108 \<and> (\<exists>\<rhd> pd) s 109 \<longrightarrow> Q pd s\<rbrace> find_pd_for_asid asid \<lbrace>Q\<rbrace>, -" 110 (is "\<lbrace>?P\<rbrace> ?f \<lbrace>Q\<rbrace>,-") 111 apply (clarsimp simp: validE_R_def validE_def valid_def imp_conjL[symmetric]) 112 apply (frule in_inv_by_hoareD[OF find_pd_for_asid_inv], clarsimp) 113 apply (drule spec, erule mp) 114 apply (simp add: use_validE_R[OF _ find_pd_for_asid_authority1] 115 use_validE_R[OF _ find_pd_for_asid_aligned_pd_bits] 116 use_validE_R[OF _ find_pd_for_asid_lookup]) 117 done 118 119lemma find_pd_for_asid_pd_slot_authorised [wp]: 120 "\<lbrace>pas_refined aag and K (is_subject_asid aag asid) and pspace_aligned and valid_vspace_objs\<rbrace> 121 find_pd_for_asid asid 122 \<lbrace>\<lambda>rv s. is_subject aag (lookup_pd_slot rv vptr && ~~ mask pd_bits) \<rbrace>, -" 123 apply (wp find_pd_for_asid_authority2) 124 apply (clarsimp simp: lookup_pd_slot_pd) 125 apply (fastforce dest: pas_refined_Control) 126 done 127 128lemma unmap_page_table_respects: 129 "\<lbrace>integrity aag X st and pas_refined aag and invs 130 and K (is_subject_asid aag asid \<and> vaddr < kernel_base)\<rbrace> 131 unmap_page_table asid vaddr pt 132 \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>" 133 apply (rule hoare_gen_asm) 134 apply (simp add: unmap_page_table_def page_table_mapped_def ) 135 apply (rule hoare_pre) 136 apply (wp store_pde_respects page_table_mapped_wp_weak get_pde_wp 137 hoare_vcg_all_lift_R dmo_mol_respects 138 | wpc 139 | simp add: cleanByVA_PoU_def 140 | wp (once) hoare_drop_imps)+ 141 apply auto 142 done 143 144definition 145 authorised_page_table_inv :: "'a PAS \<Rightarrow> page_table_invocation \<Rightarrow> bool" 146where 147 "authorised_page_table_inv aag pti \<equiv> case pti of 148 page_table_invocation.PageTableMap cap cslot_ptr pde obj_ref \<Rightarrow> 149 is_subject aag (fst cslot_ptr) \<and> is_subject aag (obj_ref && ~~ mask pd_bits) 150 \<and> (case_option True (is_subject aag o fst) (pde_ref2 pde)) 151 \<and> pas_cap_cur_auth aag cap 152 | page_table_invocation.PageTableUnmap cap cslot_ptr \<Rightarrow> 153 is_subject aag (fst cslot_ptr) \<and> aag_cap_auth aag (pasSubject aag) cap 154 \<and> (\<forall>p asid vspace_ref. cap = cap.ArchObjectCap (arch_cap.PageTableCap p (Some (asid, vspace_ref))) 155 \<longrightarrow> is_subject_asid aag asid 156 \<and> (\<forall>x \<in> set [p , p + 4 .e. p + 2 ^ pt_bits - 1]. is_subject aag (x && ~~ mask pt_bits)))" 157 158lemma perform_page_table_invocation_respects: 159 "\<lbrace>integrity aag X st and pas_refined aag and invs 160 and valid_pti page_table_invocation 161 and K (authorised_page_table_inv aag page_table_invocation)\<rbrace> 162 perform_page_table_invocation page_table_invocation 163 \<lbrace>\<lambda>s. integrity aag X st\<rbrace>" 164 apply (rule hoare_gen_asm) 165 apply (simp add: perform_page_table_invocation_def 166 cong: page_table_invocation.case_cong option.case_cong prod.case_cong 167 cap.case_cong arch_cap.case_cong) 168 apply (rule hoare_pre) 169 apply (wp store_pde_respects set_cap_integrity_autarch store_pte_respects unmap_page_table_respects mapM_wp' 170 | wpc 171 | simp add: mapM_x_mapM authorised_page_table_inv_def cleanByVA_PoU_def)+ 172 apply (auto simp: cap_auth_conferred_def is_page_cap_def 173 pas_refined_all_auth_is_owns 174 valid_pti_def valid_cap_simps) 175 done 176 177crunch arm_asid_table_inv [wp]: unmap_page_table "\<lambda>s. P (arm_asid_table (arch_state s))" 178 (wp: crunch_wps simp: crunch_simps) 179 180lemma clas_update_map_data_strg: 181 "(is_pg_cap cap \<or> is_pt_cap cap) \<longrightarrow> cap_links_asid_slot aag p (cap.ArchObjectCap (update_map_data (the_arch_cap cap) None))" 182 unfolding cap_links_asid_slot_def 183 by (fastforce simp: is_cap_simps update_map_data_def) 184 185lemmas pte_ref_simps = pte_ref_def[split_simps pte.split] 186 187lemmas store_pde_pas_refined_simple 188 = store_pde_pas_refined[where pde=InvalidPDE, simplified pde_ref_simps, simplified] 189 190crunch pas_refined[wp]: unmap_page_table "pas_refined aag" 191 (wp: crunch_wps store_pde_pas_refined_simple 192 simp: crunch_simps pde_ref_simps) 193 194lemma pde_ref_pde_ref2: 195 "\<lbrakk> pde_ref x = Some v; pde_ref2 x = Some v' \<rbrakk> \<Longrightarrow> v' = (v, 0, {Control})" 196 unfolding pde_ref_def pde_ref2_def 197 by (cases x, simp_all) 198 199lemma ptr_range_0 [simp]: "ptr_range (p :: word32) 0 = {p}" 200 unfolding ptr_range_def by simp 201 202lemma mask_PTCap_eq: 203 "(ArchObjectCap (PageTableCap a b) = mask_cap R cap) = (cap = ArchObjectCap (PageTableCap a b))" 204 by (auto simp: mask_cap_def cap_rights_update_def acap_rights_update_def 205 split: arch_cap.splits cap.splits bool.splits) 206 207 208(* FIXME MOVE *) 209crunch cdt[wp]: unmap_page_table "\<lambda>s. P (cdt s)" 210 (simp: crunch_simps wp: crunch_wps) 211 212(* FIXME MOVE *) 213lemma is_transferable_ArchCap[simp]: 214 "\<not> is_transferable 215 (Some (ArchObjectCap cap))" 216 using is_transferable.simps by simp 217 218 219 220lemma is_transferable_is_arch_update: 221 "is_arch_update cap cap' \<Longrightarrow> is_transferable (Some cap) = is_transferable (Some cap')" 222 using is_transferable.simps is_arch_cap_def is_arch_update_def cap_master_cap_def 223 by (simp split: cap.splits arch_cap.splits) 224 225lemma perform_page_table_invocation_pas_refined [wp]: 226 "\<lbrace> pas_refined aag and valid_pti page_table_invocation 227 and K (authorised_page_table_inv aag page_table_invocation)\<rbrace> 228 perform_page_table_invocation page_table_invocation 229 \<lbrace>\<lambda>s. pas_refined aag\<rbrace>" 230 apply (rule hoare_gen_asm) 231 apply (simp add: perform_page_table_invocation_def 232 cong: page_table_invocation.case_cong option.case_cong prod.case_cong 233 cap.case_cong arch_cap.case_cong) 234 apply (rule hoare_pre) 235 apply (wp get_cap_wp mapM_wp' store_pte_cte_wp_at do_machine_op_cte_wp_at 236 hoare_vcg_all_lift set_cap_pas_refined_not_transferable 237 | (wp hoare_vcg_imp_lift, unfold disj_not1) 238 | wpc 239 | simp add: mapM_x_mapM authorised_page_table_inv_def imp_conjR 240 pte_ref_simps 241 | wps 242 | blast)+ 243 apply (cases page_table_invocation) 244 apply (fastforce simp: cte_wp_at_caps_of_state Option.is_none_def 245 is_transferable_is_arch_update[symmetric] 246 valid_pti_def is_cap_simps pas_refined_refl auth_graph_map_def2 247 dest: pde_ref_pde_ref2) 248 apply (rename_tac s pt_cap page_cslot) 249 apply (case_tac page_cslot) 250 apply (rename_tac page_ptr page_slot) 251 apply (case_tac "\<exists>pt_ptr mapping. pt_cap = ArchObjectCap (PageTableCap pt_ptr mapping)") 252 prefer 2 253 apply fastforce 254 apply (elim exE) 255 apply clarsimp 256 apply (rename_tac page_cap) 257 apply (subgoal_tac 258 "cte_wp_at ((=) page_cap) (page_ptr, page_slot) s \<longrightarrow> 259 cte_wp_at (\<lambda>c. \<not> is_transferable (Some c)) (page_ptr, page_slot) s \<and> 260 pas_cap_cur_auth aag 261 (cap.ArchObjectCap (update_map_data (the_arch_cap page_cap) None))") 262 apply simp 263 apply (clarsimp simp: cte_wp_at_caps_of_state) 264 apply (frule (1) cap_cur_auth_caps_of_state) 265 apply simp 266 apply (clarsimp simp: valid_pti_def cte_wp_at_caps_of_state mask_PTCap_eq) 267 apply (clarsimp simp: cap_auth_conferred_def update_map_data_def is_page_cap_def 268 cap_links_asid_slot_def cap_links_irq_def aag_cap_auth_def) 269 done 270 271definition 272 authorised_slots :: "'a PAS \<Rightarrow> pte \<times> (obj_ref list) + pde \<times> (obj_ref list) \<Rightarrow> bool" 273where 274 "authorised_slots aag m \<equiv> case m of 275 Inl (pte, slots) \<Rightarrow> (\<forall>x. pte_ref pte = Some x \<longrightarrow> (\<forall>a \<in> (snd (snd x)). \<forall>p \<in> ptr_range (fst x) (fst (snd x)).(aag_has_auth_to aag a p))) 276 \<and> (\<forall>x \<in> set slots. is_subject aag (x && ~~ mask pt_bits)) 277 | Inr (pde, slots) \<Rightarrow> (\<forall>x. pde_ref2 pde = Some x \<longrightarrow> (\<forall>a \<in> (snd (snd x)). \<forall>p \<in> ptr_range (fst x) (fst (snd x)). (aag_has_auth_to aag a p))) 278 \<and> (\<forall>x \<in> set slots. is_subject aag (x && ~~ mask pd_bits))" 279 280definition 281 authorised_page_inv :: "'a PAS \<Rightarrow> page_invocation \<Rightarrow> bool" 282where 283 "authorised_page_inv aag pgi \<equiv> case pgi of 284 PageMap asid cap ptr slots \<Rightarrow> 285 pas_cap_cur_auth aag cap \<and> is_subject aag (fst ptr) \<and> authorised_slots aag slots 286 | PageUnmap cap ptr \<Rightarrow> pas_cap_cur_auth aag (Structures_A.ArchObjectCap cap) \<and> is_subject aag (fst ptr) 287 | PageFlush typ start end pstart pd asid \<Rightarrow> True 288 | PageGetAddr ptr \<Rightarrow> True" 289 290crunch respects[wp]: lookup_pt_slot "integrity X aag st" 291 292lemma ptrFromPAddr_inj: "inj ptrFromPAddr" 293 by (auto intro: injI simp: ptrFromPAddr_def) 294 295lemma vs_refs_no_global_pts_pdI: 296 "\<lbrakk>pd (ucast r) = PageTablePDE x a b; 297 ((ucast r)::12 word) < ucast (kernel_base >> 20) \<rbrakk> \<Longrightarrow> 298 (ptrFromPAddr x, VSRef (r && mask 12) 299 (Some APageDirectory), Control) 300 \<in> vs_refs_no_global_pts (ArchObj (PageDirectory pd))" 301 apply(clarsimp simp: vs_refs_no_global_pts_def) 302 apply (drule_tac f=pde_ref2 in arg_cong, simp add: pde_ref_simps o_def) 303 apply (rule rev_bexI, rule DiffI, erule graph_ofI) 304 apply simp 305 apply (clarsimp simp: ucast_ucast_mask ) 306 done 307 308lemma aag_has_auth_to_Control_eq_owns: 309 "pas_refined aag s \<Longrightarrow> aag_has_auth_to aag Control p = is_subject aag p" 310 by (auto simp: pas_refined_refl elim: aag_Control_into_owns) 311 312lemma lookup_pt_slot_authorised: 313 "\<lbrace>\<exists>\<rhd> pd and valid_vspace_objs and pspace_aligned and pas_refined aag 314 and K (is_subject aag pd) and K (is_aligned pd 14 \<and> vptr < kernel_base)\<rbrace> 315 lookup_pt_slot pd vptr 316 \<lbrace>\<lambda>rv s. is_subject aag (rv && ~~ mask pt_bits)\<rbrace>, -" 317 apply (simp add: lookup_pt_slot_def) 318 apply (wp get_pde_wp | wpc)+ 319 apply (subgoal_tac "is_aligned pd pd_bits") 320 apply (clarsimp simp: lookup_pd_slot_pd) 321 apply (drule(2) valid_vspace_objsD) 322 apply (clarsimp simp: obj_at_def) 323 apply (drule kheap_eq_state_vrefs_pas_refinedD) 324 apply (erule vs_refs_no_global_pts_pdI) 325 apply (drule(1) less_kernel_base_mapping_slots) 326 apply (simp add: kernel_mapping_slots_def) 327 apply assumption 328 apply (simp add: aag_has_auth_to_Control_eq_owns) 329 apply (drule_tac f="\<lambda>pde. valid_pde pde s" in arg_cong, simp) 330 apply (clarsimp simp: obj_at_def less_kernel_base_mapping_slots) 331 apply (erule pspace_alignedE, erule domI) 332 apply (simp add: pt_bits_def pageBits_def) 333 apply (subst is_aligned_add_helper, assumption) 334 apply (rule shiftl_less_t2n) 335 apply (rule order_le_less_trans, rule word_and_le1, simp) 336 apply simp 337 apply simp 338 apply (simp add: pd_bits_def pageBits_def) 339 done 340 341lemma is_aligned_6_masks: 342 fixes p :: word32 343 shows 344 "\<lbrakk> is_aligned p 6; bits = pt_bits \<or> bits = pd_bits \<rbrakk> 345 \<Longrightarrow> \<forall>x \<in> set [0, 4 .e. 0x3C]. x + p && ~~ mask bits = p && ~~ mask bits" 346 apply clarsimp 347 apply (drule subsetD[OF upto_enum_step_subset]) 348 apply (subst mask_lower_twice[symmetric, where n=6]) 349 apply (auto simp add: pt_bits_def pageBits_def pd_bits_def)[1] 350 apply (subst add.commute, subst is_aligned_add_helper, assumption) 351 apply (simp add: order_le_less_trans) 352 apply simp 353 done 354 355lemma lookup_pt_slot_authorised2: 356 "\<lbrace>\<exists>\<rhd> pd and K (is_subject aag pd) and 357 K (is_aligned pd 14 \<and> is_aligned vptr 16 \<and> vptr < kernel_base) and 358 valid_vspace_objs and valid_arch_state and equal_kernel_mappings and 359 valid_global_objs and pspace_aligned and pas_refined aag\<rbrace> 360 lookup_pt_slot pd vptr 361 \<lbrace>\<lambda>rv s. \<forall>x\<in>set [0 , 4 .e. 0x3C]. is_subject aag (x + rv && ~~ mask pt_bits)\<rbrace>, -" 362 apply (clarsimp simp: validE_R_def valid_def validE_def 363 split: sum.split) 364 apply (frule use_validE_R[OF _ lookup_pt_slot_authorised]) 365 apply fastforce 366 apply (frule use_validE_R[OF _ lookup_pt_slot_is_aligned_6]) 367 apply (fastforce simp add: vmsz_aligned_def pd_bits_def pageBits_def) 368 apply (simp add: is_aligned_6_masks) 369 done 370 371lemma lookup_pt_slot_authorised3: 372 "\<lbrace>\<exists>\<rhd> pd and K (is_subject aag pd) and 373 K (is_aligned pd 14 \<and> is_aligned vptr 16 \<and> vptr < kernel_base) and 374 valid_vspace_objs and valid_arch_state and equal_kernel_mappings and 375 valid_global_objs and pspace_aligned and pas_refined aag\<rbrace> 376 lookup_pt_slot pd vptr 377 \<lbrace>\<lambda>rv s. \<forall>x\<in>set [rv , rv + 4 .e. rv + 0x3C]. is_subject aag (x && ~~ mask pt_bits)\<rbrace>, -" 378 apply (rule hoare_post_imp_R [where Q' = "\<lambda>rv s. is_aligned rv 6 \<and> (\<forall>x\<in>set [0 , 4 .e. 0x3C]. is_subject aag (x + rv && ~~ mask pt_bits))"]) 379 apply (rule hoare_pre) 380 apply (wp lookup_pt_slot_is_aligned_6 lookup_pt_slot_authorised2) 381 apply (fastforce simp: vmsz_aligned_def pd_bits_def pageBits_def) 382 apply simp 383 apply (simp add: p_0x3C_shift) 384 done 385 386lemma mapM_set': 387 assumes ip: "\<And>x y. \<lbrakk> x \<in> set xs; y \<in> set xs \<rbrakk> \<Longrightarrow> \<lbrace>I x and I y\<rbrace> f x \<lbrace>\<lambda>_. I y\<rbrace>" 388 and rl: "\<And>s. (\<forall>x \<in> set xs. I x s) \<Longrightarrow> P s" 389 shows "\<lbrace>\<lambda>s. (\<forall>x \<in> set xs. I x s)\<rbrace> mapM f xs \<lbrace>\<lambda>_. P\<rbrace>" 390 apply (rule hoare_post_imp [OF rl]) 391 apply assumption 392 apply (rule mapM_set) 393 apply (rule hoare_pre) 394 apply (rule hoare_vcg_ball_lift) 395 apply (erule (1) ip) 396 apply clarsimp 397 apply (rule hoare_pre) 398 apply (rule ip) 399 apply assumption 400 apply assumption 401 apply clarsimp 402 apply (rule hoare_pre) 403 apply (rule ip) 404 apply simp+ 405 done 406 407lemma mapM_set'': 408 assumes ip: "\<And>x y. \<lbrakk> x \<in> set xs; y \<in> set xs \<rbrakk> \<Longrightarrow> \<lbrace>I x and I y and Q\<rbrace> f x \<lbrace>\<lambda>_. I y and Q\<rbrace>" 409 and rl: "\<And>s. (\<forall>x \<in> set xs. I x s) \<and> Q s \<Longrightarrow> P s" 410 shows "\<lbrace>\<lambda>s. (\<forall>x \<in> set xs. I x s) \<and> Q s\<rbrace> mapM f xs \<lbrace>\<lambda>_. P\<rbrace>" 411 apply (rule hoare_post_imp [OF rl]) 412 apply assumption 413 apply (cases "xs = []") 414 apply (simp add: mapM_Nil) 415 apply (rule hoare_pre) 416 apply (rule mapM_set' [where I = "\<lambda>x s. I x s \<and> Q s"]) 417 apply (rule hoare_pre) 418 apply (rule ip [simplified pred_conj_def]) 419 apply simp_all 420 apply (clarsimp simp add: neq_Nil_conv) 421 done 422 423crunch respects [wp]: flush_page "integrity aag X st" 424 (simp: invalidateLocalTLB_VAASID_def ignore: do_machine_op) 425 426lemma find_pd_for_asid_pd_owned[wp]: 427 "\<lbrace>pas_refined aag and K (is_subject_asid aag asid)\<rbrace> 428 find_pd_for_asid asid 429 \<lbrace>\<lambda>rv s. is_subject aag rv\<rbrace>,-" 430 apply (wp find_pd_for_asid_authority2) 431 apply (auto simp: aag_has_auth_to_Control_eq_owns) 432 done 433 434lemmas store_pte_pas_refined_simple 435 = store_pte_pas_refined[where pte=InvalidPTE, simplified pte_ref_simps, simplified] 436 437crunch pas_refined[wp]: unmap_page "pas_refined aag" 438 (wp: crunch_wps store_pde_pas_refined_simple store_pte_pas_refined_simple 439 simp: crunch_simps) 440 441lemma unmap_page_respects: 442 "\<lbrace>integrity aag X st and K (is_subject_asid aag asid) and pas_refined aag and pspace_aligned and valid_vspace_objs 443 and K (vmsz_aligned vptr sz \<and> vptr < kernel_base)\<rbrace> 444 unmap_page sz asid vptr pptr 445 \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>" 446 apply (rule hoare_gen_asm) 447 apply (simp add: unmap_page_def swp_def cong: vmpage_size.case_cong) 448 apply (rule hoare_pre) 449 apply (wp store_pte_respects store_pde_respects 450 hoare_drop_imps[where Q="\<lambda>rv. integrity aag X st"] 451 lookup_pt_slot_authorised 452 | wpc 453 | simp add: is_aligned_6_masks is_aligned_mask[symmetric] cleanByVA_PoU_def 454 | wp (once) hoare_drop_imps 455 mapM_set'' [where f = "(\<lambda>a. store_pte a InvalidPTE)" and I = "\<lambda>x s. is_subject aag (x && ~~ mask pt_bits)" and Q = "integrity aag X st"] 456 mapM_set'' [where f = "(\<lambda>a. store_pde a InvalidPDE)" and I = "\<lambda>x s. is_subject aag (x && ~~ mask pd_bits)" and Q = "integrity aag X st"] 457 | wp (once) hoare_drop_imps[where R="\<lambda>rv s. rv"])+ 458 done 459 460(* FIXME: MOVE *) 461lemma less_shiftr: 462 shows "\<lbrakk> x < y; is_aligned y n \<rbrakk> \<Longrightarrow> x >> n < y >> n" 463 apply (simp add: word_less_nat_alt shiftr_div_2n') 464 apply (subst td_gal_lt[symmetric]) 465 apply simp 466 apply (subst dvd_div_mult_self) 467 apply (simp add: is_aligned_def) 468 apply simp 469 done 470 471lemma kernel_base_aligned_20: 472 "is_aligned kernel_base 20" 473 apply(simp add: kernel_base_def is_aligned_def) 474 done 475 476(* FIXME: CLAG *) 477lemmas do_machine_op_bind = 478 submonad_bind [OF submonad_do_machine_op submonad_do_machine_op 479 submonad_do_machine_op] 480 481lemma mol_mem[wp]: 482 "\<lbrace>\<lambda>ms. P (underlying_memory ms)\<rbrace> machine_op_lift mop \<lbrace>\<lambda>rv ms. P (underlying_memory ms)\<rbrace>" 483 by (simp add: machine_op_lift_def machine_rest_lift_def split_def | wp)+ 484 485lemma mol_dvs[wp]: 486 "\<lbrace>\<lambda>ms. P (device_state ms)\<rbrace> machine_op_lift mop \<lbrace>\<lambda>rv ms. P (device_state ms)\<rbrace>" 487 by (simp add: machine_op_lift_def machine_rest_lift_def split_def | wp)+ 488 489lemmas do_flush_defs = cleanCacheRange_RAM_def cleanCacheRange_PoC_def cleanCacheRange_PoU_def invalidateCacheRange_RAM_def cleanInvalidateCacheRange_RAM_def branchFlushRange_def invalidateCacheRange_I_def 490 491lemma do_flush_respects[wp]: 492 "\<lbrace>integrity aag X st\<rbrace> do_machine_op (do_flush typ start end pstart) 493 \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>" 494 apply (cases "typ") 495 apply (wp dmo_no_mem_respects | simp add: do_flush_def cache_machine_op_defs do_flush_defs)+ 496 done 497 498lemma invalidate_tlb_by_asid_respects[wp]: 499 "\<lbrace>integrity aag X st\<rbrace> invalidate_tlb_by_asid asid 500 \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>" 501 apply (simp add: invalidate_tlb_by_asid_def) 502 apply (wp dmo_no_mem_respects | wpc | simp add: invalidateLocalTLB_ASID_def )+ 503 done 504 505lemma invalidate_tlb_by_asid_pas_refined[wp]: 506 "\<lbrace>pas_refined aag\<rbrace> invalidate_tlb_by_asid asid \<lbrace>\<lambda>rv. pas_refined aag\<rbrace>" 507 by (wp dmo_no_mem_respects | wpc | simp add: invalidate_tlb_by_asid_def invalidateLocalTLB_ASID_def)+ 508 509crunch pas_refined[wp]: set_message_info "pas_refined aag" 510 511(* FIXME: move *) 512lemma set_message_info_mdb[wp]: 513 "\<lbrace>\<lambda>s. P (cdt s)\<rbrace> set_message_info thread info \<lbrace>\<lambda>rv s. P (cdt s)\<rbrace>" 514 unfolding set_message_info_def by wp 515 516crunch state_vrefs[wp]: do_machine_op "\<lambda>s::'z::state_ext state. P (state_vrefs s)" 517 518crunch thread_states[wp]: do_machine_op "\<lambda>s. P (thread_states s)" 519 520(* FIXME: move *) 521lemma set_mrs_state_vrefs[wp]: 522 "\<lbrace>\<lambda>s. P (state_vrefs s)\<rbrace> set_mrs thread buf msgs \<lbrace>\<lambda>rv s. P (state_vrefs s)\<rbrace>" 523 apply (simp add: set_mrs_def split_def set_object_def get_object_def split del: if_split) 524 apply (wp gets_the_wp get_wp put_wp mapM_x_wp' 525 | wpc 526 | simp split del: if_split add: zipWithM_x_mapM_x split_def store_word_offs_def)+ 527 apply (auto simp: obj_at_def state_vrefs_def get_tcb_ko_at 528 elim!: rsubst[where P=P, OF _ ext] 529 split: if_split_asm simp: vs_refs_no_global_pts_def) 530 done 531 532(* FIXME: move *) 533lemma set_mrs_thread_states[wp]: 534 "\<lbrace>\<lambda>s. P (thread_states s)\<rbrace> set_mrs thread buf msgs \<lbrace>\<lambda>rv s. P (thread_states s)\<rbrace>" 535 apply (simp add: set_mrs_def split_def set_object_def get_object_def split del: if_split) 536 apply (wp gets_the_wp get_wp put_wp mapM_x_wp' 537 | wpc 538 | simp split del: if_split add: zipWithM_x_mapM_x split_def store_word_offs_def)+ 539 apply (clarsimp simp: fun_upd_def[symmetric] thread_states_preserved) 540 done 541 542lemma set_mrs_thread_bound_ntfns[wp]: 543 "\<lbrace>\<lambda>s. P (thread_bound_ntfns s)\<rbrace> set_mrs thread buf msgs \<lbrace>\<lambda>rv s. P (thread_bound_ntfns s)\<rbrace>" 544 apply (simp add: set_mrs_def split_def set_object_def get_object_def split del: if_split) 545 apply (wp gets_the_wp get_wp put_wp mapM_x_wp' dmo_wp 546 | wpc 547 | simp split del: if_split add: zipWithM_x_mapM_x split_def store_word_offs_def no_irq_storeWord)+ 548 apply (clarsimp simp: fun_upd_def[symmetric] thread_bound_ntfns_preserved ) 549 done 550 551lemma set_mrs_pas_refined[wp]: 552 "\<lbrace>pas_refined aag\<rbrace> set_mrs thread buf msgs \<lbrace>\<lambda>rv. pas_refined aag\<rbrace>" 553 apply (simp add: pas_refined_def state_objs_to_policy_def) 554 apply (rule hoare_pre) 555 apply (wp | wps)+ 556 apply (clarsimp dest!: auth_graph_map_memD) 557 done 558 559crunch integrity_autarch: set_message_info "integrity aag X st" 560 561lemma dmo_storeWord_respects_Write: 562 "\<lbrace>integrity aag X st and K (\<forall>p' \<in> ptr_range p 2. aag_has_auth_to aag Write p')\<rbrace> 563 do_machine_op (storeWord p v) 564 \<lbrace>\<lambda>a. integrity aag X st\<rbrace>" 565 apply (rule hoare_pre) 566 apply (wp dmo_wp storeWord_respects) 567 apply simp 568 done 569 570(* c.f. auth_ipc_buffers *) 571definition 572 ipc_buffer_has_auth :: "'a PAS \<Rightarrow> word32 \<Rightarrow> word32 option \<Rightarrow> bool" 573where 574 "ipc_buffer_has_auth aag thread \<equiv> 575 case_option True (\<lambda>buf'. is_aligned buf' msg_align_bits \<and> (\<forall>x \<in> ptr_range buf' msg_align_bits. (pasObjectAbs aag thread, Write, pasObjectAbs aag x) \<in> pasPolicy aag))" 576 577lemma ipc_buffer_has_auth_wordE: 578 "\<lbrakk> ipc_buffer_has_auth aag thread (Some buf); p \<in> ptr_range (buf + off) sz; is_aligned off sz; sz \<le> msg_align_bits; off < 2 ^ msg_align_bits \<rbrakk> 579 \<Longrightarrow> (pasObjectAbs aag thread, Write, pasObjectAbs aag p) \<in> pasPolicy aag" 580 unfolding ipc_buffer_has_auth_def 581 apply clarsimp 582 apply (erule bspec) 583 apply (erule (4) set_mp [OF ptr_range_subset]) 584 done 585 586 587lemma is_aligned_word_size_2 [simp]: 588 "is_aligned (p * of_nat word_size) 2" 589 unfolding word_size_def 590 by (simp add: is_aligned_mult_triv2 [where n = 2, simplified] word_bits_conv) 591 592 593 594lemma mul_word_size_lt_msg_align_bits_ofnat: 595 "p < 2 ^ (msg_align_bits - 2) \<Longrightarrow> of_nat p * of_nat word_size < (2 :: word32) ^ msg_align_bits" 596 unfolding word_size_def 597 apply simp 598 apply (rule word_less_power_trans_ofnat [where k = 2, simplified]) 599 apply (simp_all add: msg_align_bits word_bits_conv) 600 done 601 602lemma store_word_offs_integrity_autarch: 603 "\<lbrace>integrity aag X st and K (is_subject aag thread \<and> ipc_buffer_has_auth aag thread (Some buf) \<and> r < 2 ^ (msg_align_bits - 2))\<rbrace> 604 store_word_offs buf r v 605 \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>" 606 apply (simp add: store_word_offs_def) 607 apply (rule hoare_pre) 608 apply (wp dmo_storeWord_respects_Write) 609 apply clarsimp 610 apply (drule (1) ipc_buffer_has_auth_wordE) 611 apply simp 612 apply (simp add: msg_align_bits) 613 apply (erule mul_word_size_lt_msg_align_bits_ofnat) 614 apply simp 615 done 616 617lemma set_mrs_integrity_autarch: 618 "\<lbrace>integrity aag X st and K (is_subject aag thread \<and> ipc_buffer_has_auth aag thread buf)\<rbrace> 619 set_mrs thread buf msgs 620 \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>" 621 apply (rule hoare_gen_asm) 622 apply (simp add: set_mrs_def split del: if_split) 623 apply (wp gets_the_wp get_wp put_wp mapM_x_wp' store_word_offs_integrity_autarch [where aag = aag and thread = thread] 624 | wpc 625 | simp split del: if_split add: split_def zipWithM_x_mapM_x )+ 626 apply (clarsimp elim!: in_set_zipE split: if_split_asm) 627 apply (rule order_le_less_trans [where y = msg_max_length]) 628 apply (fastforce simp add: le_eq_less_or_eq) 629 apply (simp add: msg_max_length_def msg_align_bits) 630 apply simp 631 apply (wp set_object_integrity_autarch hoare_drop_imps hoare_vcg_all_lift)+ 632 apply simp 633 done 634 635lemma perform_page_invocation_respects: 636 "\<lbrace>integrity aag X st and pas_refined aag and K (authorised_page_inv aag pgi) and valid_page_inv pgi and valid_vspace_objs and pspace_aligned and is_subject aag \<circ> cur_thread\<rbrace> 637 perform_page_invocation pgi 638 \<lbrace>\<lambda>s. integrity aag X st\<rbrace>" 639proof - 640 (* does not work as elim rule with clarsimp, which hammers Ball in concl. *) 641 have set_tl_subset_mp: "\<And>xs a. a \<in> set (tl xs) \<Longrightarrow> a \<in> set xs" by (case_tac xs,clarsimp+) 642 have hd_valid_slots: 643 "\<And>a xs s. valid_slots (Inl (a, xs)) s \<Longrightarrow> hd xs \<in> set xs" 644 "\<And>a xs s. valid_slots (Inr (a, xs)) s \<Longrightarrow> hd xs \<in> set xs" 645 by (simp_all add: valid_slots_def) 646 647 show ?thesis 648 apply (simp add: perform_page_invocation_def mapM_discarded swp_def 649 valid_page_inv_def valid_unmap_def 650 authorised_page_inv_def authorised_slots_def 651 split: page_invocation.split sum.split 652 arch_cap.split option.split, 653 safe) 654 apply (wp set_cap_integrity_autarch unmap_page_respects 655 mapM_x_and_const_wp[OF store_pte_respects] store_pte_respects 656 mapM_x_and_const_wp[OF store_pde_respects] store_pde_respects 657 | elim conjE hd_valid_slots[THEN bspec[rotated]] 658 | clarsimp dest!:set_tl_subset_mp 659 | wpc )+ 660 apply (clarsimp simp: cte_wp_at_caps_of_state cap_auth_conferred_def cap_rights_update_def 661 acap_rights_update_def update_map_data_def is_pg_cap_def 662 valid_page_inv_def valid_cap_simps 663 dest!: cap_master_cap_eqDs) 664 apply (drule (1) clas_caps_of_state) 665 apply (simp add: cap_links_asid_slot_def label_owns_asid_slot_def) 666 apply (auto dest: pas_refined_Control)[1] 667 apply (wp set_mrs_integrity_autarch set_message_info_integrity_autarch | simp add: ipc_buffer_has_auth_def)+ 668 done 669qed 670 671(* FIXME MOVE *) 672crunch cdt[wp]: unmap_page "\<lambda>s. P (cdt s)" 673 (simp: crunch_simps wp: crunch_wps) 674 675 676lemma perform_page_invocation_pas_refined [wp]: 677 "\<lbrace>pas_refined aag and K (authorised_page_inv aag pgi) and valid_page_inv pgi\<rbrace> 678 perform_page_invocation pgi 679 \<lbrace>\<lambda>_. pas_refined aag\<rbrace>" 680 apply (simp add: perform_page_invocation_def mapM_discarded 681 valid_page_inv_def valid_unmap_def swp_def 682 authorised_page_inv_def authorised_slots_def 683 cong: page_invocation.case_cong sum.case_cong) 684 apply (rule hoare_pre) 685 apply wpc 686 apply (wp set_cap_pas_refined unmap_page_pas_refined case_sum_wp case_prod_wp 687 mapM_x_and_const_wp [OF store_pte_pas_refined] mapM_x_and_const_wp [OF store_pde_pas_refined] 688 hoare_vcg_all_lift hoare_vcg_const_imp_lift get_cap_wp 689 | (wp hoare_vcg_imp_lift, unfold disj_not1) 690 | strengthen clas_update_map_data_strg 691 | wpc 692 | wps 693 | simp)+ 694 apply (case_tac pgi) 695 apply ((force simp: valid_slots_def pte_ref_def cte_wp_at_caps_of_state 696 is_transferable_is_arch_update[symmetric] 697 pde_ref2_def auth_graph_map_mem pas_refined_refl 698 split: sum.splits)+)[2] 699 apply (clarsimp simp: cte_wp_at_caps_of_state is_transferable_is_arch_update[symmetric] 700 pte_ref_def pde_ref2_def is_cap_simps is_pg_cap_def cap_auth_conferred_def) 701 apply (frule(1) cap_cur_auth_caps_of_state, simp) 702 apply (intro impI conjI; 703 clarsimp; (* NB: for speed *) 704 clarsimp simp: update_map_data_def clas_no_asid aag_cap_auth_def 705 cap_auth_conferred_def vspace_cap_rights_to_auth_def 706 cli_no_irqs is_pg_cap_def 707 pte_ref_def[simplified aag_cap_auth_def])+ 708 done 709 710definition 711 authorised_asid_control_inv :: "'a PAS \<Rightarrow> asid_control_invocation \<Rightarrow> bool" 712where 713 "authorised_asid_control_inv aag aci \<equiv> case aci of 714 asid_control_invocation.MakePool frame slot parent base \<Rightarrow> 715 is_subject aag (fst slot) \<and> is_aligned frame pageBits \<and> (\<forall>asid. is_subject_asid aag asid) \<and> is_subject aag (fst parent) \<and> 716 (\<forall>x \<in> {frame..frame + 2 ^ pageBits - 1}. is_subject aag x)" 717 718 719lemma integrity_arm_asid_table_entry_update': 720 "\<lbrakk>integrity aag X st s; asid_table = arm_asid_table (arch_state s); 721 (\<forall>asid'. 722 asid' \<noteq> 0 \<and> 723 asid_high_bits_of asid' = asid_high_bits_of asid \<longrightarrow> 724 is_subject_asid aag asid')\<rbrakk> \<Longrightarrow> 725 integrity aag X st 726 (s\<lparr>arch_state := arch_state s 727 \<lparr>arm_asid_table := 728 \<lambda>a. if a = asid_high_bits_of asid then v 729 else asid_table a\<rparr>\<rparr>)" 730 apply(clarsimp simp: integrity_def integrity_asids_def) 731 done 732 733lemma arm_asid_table_entry_update_integrity[wp]: 734 "\<lbrace>integrity aag X st and (\<lambda> s. asid_table = arm_asid_table (arch_state s)) and K (\<forall>asid'. 735 asid' \<noteq> 0 \<and> 736 asid_high_bits_of asid' = asid_high_bits_of asid \<longrightarrow> 737 is_subject_asid aag asid')\<rbrace> 738 modify 739 (\<lambda>s. s\<lparr>arch_state := arch_state s 740 \<lparr>arm_asid_table := asid_table 741 (asid_high_bits_of asid := v)\<rparr>\<rparr>) 742 \<lbrace>\<lambda>_. integrity aag X st\<rbrace>" 743 apply (wp| simp)+ 744 apply (blast intro: integrity_arm_asid_table_entry_update') 745 done 746 747lemma perform_asid_control_invocation_respects: 748 "\<lbrace>integrity aag X st and K (authorised_asid_control_inv aag aci)\<rbrace> 749 perform_asid_control_invocation aci 750 \<lbrace>\<lambda>s. integrity aag X st\<rbrace>" 751 apply (simp add: perform_asid_control_invocation_def) 752 apply (rule hoare_pre) 753 apply (wpc, simp) 754 apply (wp set_cap_integrity_autarch cap_insert_integrity_autarch retype_region_integrity[where sz=12] static_imp_wp | simp)+ 755 apply (clarsimp simp: authorised_asid_control_inv_def 756 ptr_range_def page_bits_def add.commute 757 range_cover_def obj_bits_api_def default_arch_object_def 758 pageBits_def word_bits_def) 759 apply(subst is_aligned_neg_mask_eq[THEN sym], assumption) 760 apply(simp add: mask_neg_mask_is_zero mask_zero) 761 done 762 763lemma pas_refined_set_asid_strg: 764 "pas_refined aag s \<and> is_subject aag pool \<and> (\<forall>asid. asid_high_bits_of asid = base \<longrightarrow> is_subject_asid aag asid) 765 \<longrightarrow> 766 pas_refined aag (s\<lparr>arch_state := arch_state s \<lparr>arm_asid_table := (arm_asid_table (arch_state s))(base \<mapsto> pool)\<rparr>\<rparr>)" 767 apply (clarsimp simp: pas_refined_def state_objs_to_policy_def) 768 apply (erule state_asids_to_policy_aux.cases, simp_all split: if_split_asm) 769 apply (auto intro: state_asids_to_policy_aux.intros auth_graph_map_memI[OF sbta_vref] pas_refined_refl[simplified pas_refined_def state_objs_to_policy_def]) 770 done 771 772 773(* FIXME: copied from Detype_R. *) 774lemma gets_modify_comm2: 775 "\<forall>s. g (f s) = g s \<Longrightarrow> 776 (do x \<leftarrow> modify f; y \<leftarrow> gets g; m x y od) = 777 (do y \<leftarrow> gets g; x \<leftarrow> modify f; m x y od)" 778 apply (rule ext) 779 apply (drule spec) 780 by (rule gets_modify_comm) 781lemma dmo_detype_comm: 782 assumes "empty_fail f" 783 shows "do_machine_op f >>= (\<lambda>s. modify (detype S)) = 784 modify (detype S) >>= (\<lambda>s. do_machine_op f)" 785proof - 786 have machine_state_detype: "\<forall>s. machine_state (detype S s) = machine_state s" 787 by (simp add: detype_def) 788 have detype_msu_independent: 789 "\<And>f. detype S \<circ> machine_state_update f = machine_state_update f \<circ> detype S" 790 by (simp add: detype_def ext) 791 from assms 792 show ?thesis 793 apply (simp add: do_machine_op_def split_def bind_assoc) 794 apply (simp add: gets_modify_comm2[OF machine_state_detype]) 795 apply (rule arg_cong_bind1) 796 apply (simp add: empty_fail_def select_f_walk[OF empty_fail_modify] 797 modify_modify detype_msu_independent) 798 done 799qed 800 801(* FIXME: copied from Detype_R. *) 802lemma empty_fail_freeMemory: "empty_fail (freeMemory ptr bits)" 803 by (simp add: freeMemory_def mapM_x_mapM ef_storeWord) 804 805(* FIXME: copied from Detype_R. *) 806lemma delete_objects_def2: 807 "delete_objects ptr bits \<equiv> 808 do modify (detype {ptr..ptr + 2 ^ bits - 1}); 809 do_machine_op (freeMemory ptr bits) 810 od" 811 by (rule eq_reflection) 812 (simp add: delete_objects_def dmo_detype_comm[OF empty_fail_freeMemory]) 813 814lemma delete_objects_pspace_no_overlap: 815 "\<lbrace> pspace_aligned and valid_objs and 816 (\<lambda> s. \<exists> idx. cte_wp_at ((=) (UntypedCap dev ptr sz idx)) slot s)\<rbrace> 817 delete_objects ptr sz 818 \<lbrace>\<lambda>rv. pspace_no_overlap_range_cover ptr sz\<rbrace>" 819 unfolding delete_objects_def do_machine_op_def 820 apply(wp | simp add: split_def detype_machine_state_update_comm)+ 821 apply(clarsimp) 822 apply(rule pspace_no_overlap_detype) 823 apply(auto dest: cte_wp_at_valid_objs_valid_cap) 824 done 825 826 827lemma delete_objects_invs_ex: 828 "\<lbrace>(\<lambda>s. \<exists>slot dev f. 829 cte_wp_at ((=) (UntypedCap dev ptr bits f)) slot s \<and> 830 descendants_range (UntypedCap dev ptr bits f) slot s) and 831 invs and 832 ct_active\<rbrace> 833 delete_objects ptr bits \<lbrace>\<lambda>_. invs\<rbrace>" 834 apply(clarsimp simp: valid_def) 835 apply(erule use_valid) 836 apply wp 837 apply auto 838 done 839 840 841lemma perform_asid_control_invocation_pas_refined [wp]: 842 notes delete_objects_invs[wp del] 843 shows 844 "\<lbrace>pas_refined aag and pas_cur_domain aag and invs and valid_aci aci and ct_active and 845 K (authorised_asid_control_inv aag aci)\<rbrace> 846 perform_asid_control_invocation aci 847 \<lbrace>\<lambda>_. pas_refined aag\<rbrace>" 848 apply (simp add: perform_asid_control_invocation_def) 849 apply (rule hoare_pre) 850 apply (wp cap_insert_pas_refined' static_imp_wp 851 | strengthen pas_refined_set_asid_strg 852 | wpc 853 | simp add: delete_objects_def2 fun_upd_def[symmetric])+ 854 apply (wp retype_region_pas_refined'[where sz=pageBits] 855 hoare_vcg_ex_lift hoare_vcg_all_lift static_imp_wp hoare_wp_combs hoare_drop_imp 856 retype_region_invs_extras(4)[where sz = pageBits] 857 | simp add: do_machine_op_def split_def cte_wp_at_neg2)+ 858 apply (wp retype_region_cte_at_other'[where sz=pageBits] 859 max_index_upd_invs_simple max_index_upd_caps_overlap_reserved 860 hoare_vcg_ex_lift set_cap_cte_wp_at hoare_vcg_disj_lift set_free_index_valid_pspace 861 set_cap_descendants_range_in set_cap_no_overlap get_cap_wp set_cap_caps_no_overlap 862 hoare_vcg_all_lift static_imp_wp retype_region_invs_extras 863 set_cap_pas_refined_not_transferable 864 | simp add: do_machine_op_def split_def cte_wp_at_neg2 region_in_kernel_window_def)+ 865 apply (rename_tac frame slot parent base cap) 866 apply (case_tac slot, rename_tac slot_ptr slot_idx) 867 apply (case_tac parent, rename_tac parent_ptr parent_idx) 868 apply (rule_tac Q="\<lambda>rv s. 869 (\<exists>idx. cte_wp_at ((=) (UntypedCap False frame pageBits idx)) parent s) \<and> 870 (\<forall>x\<in>ptr_range frame pageBits. is_subject aag x) \<and> 871 pas_refined aag s \<and> 872 pas_cur_domain aag s \<and> 873 pspace_no_overlap_range_cover frame pageBits s \<and> 874 invs s \<and> 875 descendants_range_in 876 {frame..(frame && ~~ mask pageBits) + 2 ^ pageBits - 1} parent s \<and> 877 range_cover frame pageBits 878 (obj_bits_api (ArchObject ASIDPoolObj) 0) (Suc 0) \<and> 879 is_subject aag slot_ptr \<and> 880 is_subject aag parent_ptr \<and> 881 pas_cap_cur_auth aag (ArchObjectCap (ASIDPoolCap frame base)) \<and> 882 is_subject aag frame \<and> 883 (\<forall>x. asid_high_bits_of x = asid_high_bits_of base \<longrightarrow> 884 is_subject_asid aag x)" 885 in hoare_strengthen_post) 886 apply (simp add: page_bits_def) 887 apply (wp add: delete_objects_pspace_no_overlap hoare_vcg_ex_lift 888 delete_objects_descendants_range_in delete_objects_invs_ex 889 delete_objects_pas_refined 890 del: Untyped_AI.delete_objects_pspace_no_overlap 891 | simp add: page_bits_def)+ 892 apply clarsimp 893 apply (rename_tac s idx) 894 apply (frule untyped_cap_aligned, simp add: invs_valid_objs) 895 apply (clarsimp simp: cte_wp_at_def aag_cap_auth_def ptr_range_def pas_refined_refl 896 cap_links_asid_slot_def cap_links_irq_def 897 obj_bits_api_def default_arch_object_def retype_addrs_def) 898 apply (rule conjI, force intro: descendants_range_caps_no_overlapI 899 simp: cte_wp_at_def) 900 apply (rule conjI) 901 apply (cut_tac s=s and ptr="(parent_ptr, parent_idx)" in cap_refs_in_kernel_windowD) 902 apply ((fastforce simp add: caps_of_state_def cap_range_def)+)[3] 903 apply (rule conjI, force simp: field_simps) 904 apply (rule conjI, fastforce) 905 apply (fastforce dest: caps_of_state_valid 906 simp: caps_of_state_def free_index_of_def 907 max_free_index_def valid_cap_def) 908 apply (clarsimp simp: valid_aci_def authorised_asid_control_inv_def) 909 apply (rename_tac frame slot_ptr slot_idx parent_ptr parent_idx base) 910 apply (subgoal_tac "is_aligned frame pageBits") 911 apply (clarsimp simp: cte_wp_at_caps_of_state) 912 apply (rule conjI) 913 apply (drule untyped_slots_not_in_untyped_range) 914 apply (erule empty_descendants_range_in) 915 apply (simp add: cte_wp_at_caps_of_state) 916 apply simp 917 apply (rule refl) 918 apply (rule subset_refl) 919 apply (simp add: page_bits_def) 920 apply (clarsimp simp: ptr_range_def invs_psp_aligned invs_valid_objs 921 descendants_range_def2 empty_descendants_range_in page_bits_def) 922 apply ((strengthen refl | simp)+)? 923 apply (rule conjI, fastforce) 924 apply (rule conjI, fastforce intro: empty_descendants_range_in) 925 apply (rule conjI) 926 apply (clarsimp simp: range_cover_def obj_bits_api_def default_arch_object_def) 927 apply (subst is_aligned_neg_mask_eq[THEN sym], assumption) 928 apply (simp add: mask_neg_mask_is_zero pageBits_def mask_zero) 929 apply (clarsimp simp: aag_cap_auth_def pas_refined_refl) 930 apply (drule_tac x=frame in bspec) 931 apply (simp add: is_aligned_no_overflow) 932 apply (clarsimp simp: pas_refined_refl cap_links_asid_slot_def 933 label_owns_asid_slot_def cap_links_irq_def) 934 apply (fastforce dest: cte_wp_at_valid_objs_valid_cap simp: valid_cap_def cap_aligned_def) 935 done 936 937lemma set_asid_pool_respects: 938 "\<lbrace>integrity aag X st and K (is_subject aag ptr)\<rbrace> 939 set_asid_pool ptr pool 940 \<lbrace>\<lambda>s. integrity aag X st\<rbrace>" 941 apply (simp add: set_asid_pool_def) 942 apply (wp get_object_wp set_object_integrity_autarch) 943 apply simp 944 done 945 946definition 947 authorised_asid_pool_inv :: "'a PAS \<Rightarrow> asid_pool_invocation \<Rightarrow> bool" 948where 949 "authorised_asid_pool_inv aag api \<equiv> case api of 950 asid_pool_invocation.Assign asid pool_ptr ct_slot \<Rightarrow> 951 is_subject aag pool_ptr \<and> is_subject aag (fst ct_slot) 952 \<and> asid \<noteq> 0 953 \<and> (\<forall>asid'. asid_high_bits_of asid' = asid_high_bits_of asid \<and> asid' \<noteq> 0 954 \<longrightarrow> is_subject_asid aag asid')" 955 956lemma perform_asid_pool_invocation_respects: 957 "\<lbrace>integrity aag X st and K (authorised_asid_pool_inv aag api)\<rbrace> 958 perform_asid_pool_invocation api 959 \<lbrace>\<lambda>s. integrity aag X st\<rbrace>" 960 apply (simp add: perform_asid_pool_invocation_def) 961 apply (rule hoare_pre) 962 apply (wp set_asid_pool_respects get_cap_wp set_cap_integrity_autarch 963 | wpc 964 | simp)+ 965 apply (auto iff: authorised_asid_pool_inv_def) 966 done 967 968lemma is_subject_asid_into_loas: 969 "\<lbrakk> is_subject_asid aag asid; pas_refined aag s \<rbrakk> \<Longrightarrow> label_owns_asid_slot aag (pasSubject aag) asid" 970 unfolding label_owns_asid_slot_def 971 by (clarsimp simp: pas_refined_refl) 972 973lemma asid_pool_into_aag: 974 "\<lbrakk>kheap s p = Some (ArchObj (arch_kernel_obj.ASIDPool pool)); pool r = Some p'; pas_refined aag s \<rbrakk> 975 \<Longrightarrow> (pasObjectAbs aag p, Control, pasObjectAbs aag p') \<in> pasPolicy aag" 976 apply (rule pas_refined_mem [rotated], assumption) 977 apply (rule sta_vref) 978 apply (fastforce simp add: state_vrefs_def vs_refs_no_global_pts_def intro!: graph_ofI) 979 done 980 981lemma asid_pool_uniqueness: 982 "\<lbrakk> ([VSRef (ucast (asid_high_bits_of asid)) None] \<rhd> p) s; 983 arm_asid_table (arch_state s) (asid_high_bits_of asid') = Some p; 984 invs s; \<forall>pt. \<not> ko_at (ArchObj (PageTable pt)) p s \<rbrakk> 985 \<Longrightarrow> asid_high_bits_of asid' = asid_high_bits_of asid" 986 apply (drule valid_vs_lookupD[OF vs_lookup_pages_vs_lookupI], clarsimp) 987 apply (drule vs_lookup_atI, drule valid_vs_lookupD[OF vs_lookup_pages_vs_lookupI], clarsimp) 988 apply (clarsimp dest!: obj_ref_elemD) 989 apply (drule(1) unique_table_refsD[where cps="caps_of_state s", rotated]) 990 apply simp 991 apply (clarsimp simp: vs_cap_ref_def table_cap_ref_def up_ucast_inj_eq 992 split: vmpage_size.splits option.splits cap.splits arch_cap.splits)+ 993 done 994 995lemma perform_asid_pool_invocation_pas_refined [wp]: 996 "\<lbrace>pas_refined aag and invs and valid_apinv api and K (authorised_asid_pool_inv aag api)\<rbrace> 997 perform_asid_pool_invocation api 998 \<lbrace>\<lambda>_. pas_refined aag\<rbrace>" 999 apply (simp add: perform_asid_pool_invocation_def) 1000 apply (rule hoare_pre) 1001 apply (wp get_cap_auth_wp[where aag = aag] set_cap_pas_refined_not_transferable | wpc)+ 1002 apply (clarsimp simp: authorised_asid_pool_inv_def cap_links_asid_slot_def 1003 is_subject_asid_into_loas aag_cap_auth_def) 1004 apply (clarsimp simp: cap_auth_conferred_def is_cap_simps is_page_cap_def auth_graph_map_mem 1005 pas_refined_all_auth_is_owns pas_refined_refl cli_no_irqs 1006 cte_wp_at_caps_of_state 1007 dest!: graph_ofD) 1008 apply (clarsimp split: if_split_asm) 1009 apply (clarsimp simp add: pas_refined_refl auth_graph_map_def2 1010 mask_asid_low_bits_ucast_ucast[symmetric] 1011 valid_apinv_def obj_at_def) 1012 apply (drule(2) asid_pool_uniqueness) 1013 apply (simp add: obj_at_def) 1014 apply (case_tac "asid = 0"; simp add: pas_refined_refl) 1015 apply (simp add: asid_low_high_bits[rotated, OF arg_cong[where f=ucast]]) 1016 apply (clarsimp simp: obj_at_def) 1017 apply (frule (2) asid_pool_into_aag) 1018 apply (drule kheap_eq_state_vrefsD) 1019 apply (clarsimp simp: auth_graph_map_def2 pas_refined_refl) 1020 apply (clarsimp simp: pas_refined_def vs_refs_no_global_pts_def) 1021 apply (erule subsetD, erule state_asids_to_policy_aux.intros, 1022 simp add: split_def, rule image_eqI[rotated], erule graph_ofI) 1023 apply simp 1024 done 1025 1026definition 1027 authorised_page_directory_inv :: "'a PAS \<Rightarrow> page_directory_invocation \<Rightarrow> bool" 1028where 1029 "authorised_page_directory_inv aag pdi \<equiv> True" 1030 1031definition 1032 authorised_arch_inv :: "'a PAS \<Rightarrow> arch_invocation \<Rightarrow> bool" 1033where 1034 "authorised_arch_inv aag ai \<equiv> case ai of 1035 InvokePageTable pti \<Rightarrow> authorised_page_table_inv aag pti 1036 | InvokePageDirectory pdi \<Rightarrow> authorised_page_directory_inv aag pdi 1037 | InvokePage pgi \<Rightarrow> authorised_page_inv aag pgi 1038 | InvokeASIDControl aci \<Rightarrow> authorised_asid_control_inv aag aci 1039 | InvokeASIDPool api \<Rightarrow> authorised_asid_pool_inv aag api" 1040 1041crunch respects [wp]: perform_page_directory_invocation "integrity aag X st" 1042 (ignore: do_machine_op) 1043 1044lemma invoke_arch_respects: 1045 "\<lbrace>integrity aag X st and K (authorised_arch_inv aag ai) and 1046 pas_refined aag and invs and valid_arch_inv ai and is_subject aag \<circ> cur_thread\<rbrace> 1047 arch_perform_invocation ai 1048 \<lbrace>\<lambda>s. integrity aag X st\<rbrace>" 1049 apply (simp add: arch_perform_invocation_def) 1050 apply (rule hoare_pre) 1051 apply (wp perform_page_table_invocation_respects perform_page_invocation_respects 1052 perform_asid_control_invocation_respects perform_asid_pool_invocation_respects 1053 | wpc)+ 1054 apply (auto simp: authorised_arch_inv_def valid_arch_inv_def) 1055 done 1056 1057crunch pas_refined [wp]: perform_page_directory_invocation "pas_refined aag" 1058 1059lemma invoke_arch_pas_refined: 1060 "\<lbrace>pas_refined aag and pas_cur_domain aag and invs and ct_active and valid_arch_inv ai and K (authorised_arch_inv aag ai)\<rbrace> 1061 arch_perform_invocation ai 1062 \<lbrace>\<lambda>s. pas_refined aag\<rbrace>" 1063 apply (simp add: arch_perform_invocation_def valid_arch_inv_def) 1064 apply (rule hoare_pre) 1065 apply (wp | wpc)+ 1066 apply (fastforce simp add: authorised_arch_inv_def) 1067 done 1068 1069lemma create_mapping_entries_authorised_slots [wp]: 1070 "\<lbrace>\<exists>\<rhd> pd and invs and pas_refined aag 1071 and K (is_subject aag pd 1072 \<and> is_aligned pd pd_bits 1073 \<and> vmsz_aligned vptr vmpage_size 1074 \<and> vptr < kernel_base 1075 \<and> (\<forall>a\<in>vspace_cap_rights_to_auth rights. 1076 \<forall>p\<in>ptr_range (ptrFromPAddr base) (pageBitsForSize vmpage_size). 1077 aag_has_auth_to aag a p))\<rbrace> 1078 create_mapping_entries base vptr vmpage_size rights attrib pd 1079 \<lbrace>\<lambda>rv s. authorised_slots aag rv\<rbrace>, -" 1080 unfolding authorised_slots_def 1081 apply (rule hoare_gen_asmE) 1082 apply (cases vmpage_size) 1083 apply (wp lookup_pt_slot_authorised 1084 | simp add: pte_ref_simps | fold validE_R_def)+ 1085 apply (auto simp: pd_bits_def pageBits_def)[1] 1086 apply (wp lookup_pt_slot_authorised2 1087 | simp add: pte_ref_simps largePagePTE_offsets_def 1088 | fold validE_R_def)+ 1089 apply (auto simp: pd_bits_def pageBits_def vmsz_aligned_def)[1] 1090 apply (wp | simp)+ 1091 apply (auto simp: pde_ref2_def lookup_pd_slot_pd)[1] 1092 apply (wp | simp add: superSectionPDE_offsets_def)+ 1093 apply (auto simp: pde_ref2_def vmsz_aligned_def lookup_pd_slot_add_eq) 1094 done 1095 1096lemma x_t2n_sub_1_neg_mask: 1097 "\<lbrakk> is_aligned x n; n \<le> m \<rbrakk> 1098 \<Longrightarrow> x + 2 ^ n - 1 && ~~ mask m = x && ~~ mask m" 1099 apply (erule is_aligned_get_word_bits) 1100 apply (rule trans, rule mask_lower_twice[symmetric], assumption) 1101 apply (subst add_diff_eq[symmetric], subst is_aligned_add_helper, assumption) 1102 apply simp+ 1103 apply (simp add: mask_def power_overflow) 1104 done 1105 1106lemma pageBitsForSize_le_t28: 1107 "pageBitsForSize sz \<le> 28" 1108 by (cases sz, simp_all) 1109 1110lemma pageBitsForSize_le_t29: 1111 "pageBitsForSize sz \<le> 29" 1112 by (cases sz, simp_all) 1113 1114lemmas vmsz_aligned_t2n_neg_mask 1115 = x_t2n_sub_1_neg_mask[OF _ pageBitsForSize_le_t29, folded vmsz_aligned_def] 1116 1117 1118lemma decode_arch_invocation_authorised: 1119 "\<lbrace>invs and pas_refined aag 1120 and cte_wp_at ((=) (cap.ArchObjectCap cap)) slot 1121 and (\<lambda>s. \<forall>(cap, slot) \<in> set excaps. cte_wp_at ((=) cap) slot s) 1122 and K (\<forall>(cap, slot) \<in> {(cap.ArchObjectCap cap, slot)} \<union> set excaps. 1123 aag_cap_auth aag (pasObjectAbs aag (fst slot)) cap \<and> is_subject aag (fst slot) 1124 \<and> (\<forall>v \<in> cap_asid' cap. is_subject_asid aag v))\<rbrace> 1125 arch_decode_invocation label msg x_slot slot cap excaps 1126 \<lbrace>\<lambda>rv s. authorised_arch_inv aag rv\<rbrace>,-" 1127 unfolding arch_decode_invocation_def authorised_arch_inv_def aag_cap_auth_def 1128 apply (rule hoare_pre) 1129 apply (simp add: split_def Let_def 1130 cong: cap.case_cong arch_cap.case_cong if_cong option.case_cong split del: if_split) 1131 1132 apply (wp select_wp whenE_throwError_wp check_vp_wpR 1133 find_pd_for_asid_authority2 1134 | wpc 1135 | simp add: authorised_asid_control_inv_def authorised_page_inv_def 1136 authorised_page_directory_inv_def 1137 del: hoare_True_E_R 1138 split del: if_split)+ 1139 apply (clarsimp simp: authorised_asid_pool_inv_def authorised_page_table_inv_def 1140 neq_Nil_conv invs_psp_aligned invs_vspace_objs cli_no_irqs) 1141 apply (drule cte_wp_valid_cap, clarsimp+) 1142 apply (cases cap; simp) 1143 \<comment> \<open>asid pool\<close> 1144 apply (find_goal \<open>match premises in "cap = ASIDPoolCap _ _" \<Rightarrow> succeed\<close>) 1145 subgoal for s obj_ref asid 1146 by (clarsimp simp: cap_auth_conferred_def is_page_cap_def 1147 pas_refined_all_auth_is_owns asid_high_bits_of_add_ucast 1148 valid_cap_simps) 1149 \<comment> \<open>ControlCap\<close> 1150 apply (find_goal \<open>match premises in "cap = ASIDControlCap" \<Rightarrow> succeed\<close>) 1151 subgoal 1152 apply (clarsimp simp: neq_Nil_conv split_def valid_cap_simps) 1153 apply (cases excaps, solves simp) 1154 apply (clarsimp simp: neq_Nil_conv aag_has_auth_to_Control_eq_owns) 1155 apply (drule cte_wp_at_valid_objs_valid_cap, clarsimp) 1156 apply (clarsimp simp: valid_cap_def cap_aligned_def) 1157 apply (clarsimp simp: is_cap_simps cap_auth_conferred_def 1158 pas_refined_all_auth_is_owns aag_cap_auth_def) 1159 done 1160 \<comment> \<open>PageCap\<close> 1161 apply (find_goal \<open>match premises in "cap = PageCap _ _ _ _ _" \<Rightarrow> succeed\<close>) 1162 subgoal for s is_dev obj_ref cap_rights vmpage_size mapping 1163 apply (clarsimp simp: valid_cap_simps cli_no_irqs) 1164 apply (cases "invocation_type label"; (solves \<open>simp\<close>)?) 1165 apply (find_goal \<open>match premises in "_ = ArchInvocationLabel _" \<Rightarrow> succeed\<close>) 1166 apply (rename_tac archlabel) 1167 apply (case_tac archlabel; (solves \<open>simp\<close>)?) 1168 \<comment> \<open>Map\<close> 1169 apply (find_goal \<open>match premises in "_ = ARMPageMap" \<Rightarrow> succeed\<close>) 1170 subgoal 1171 apply (clarsimp simp: cap_auth_conferred_def is_cap_simps is_page_cap_def 1172 pas_refined_all_auth_is_owns) 1173 apply (rule conjI) 1174 apply (clarsimp simp: cap_auth_conferred_def is_page_cap_def pas_refined_all_auth_is_owns 1175 aag_cap_auth_def cli_no_irqs cap_links_asid_slot_def) 1176 apply (simp only: linorder_not_le kernel_base_less_observation 1177 vmsz_aligned_t2n_neg_mask simp_thms) 1178 apply (clarsimp simp: cap_auth_conferred_def vspace_cap_rights_to_auth_def 1179 mask_vm_rights_def validate_vm_rights_def vm_read_only_def 1180 vm_kernel_only_def) 1181 apply (clarsimp simp: cap_auth_conferred_def is_cap_simps is_page_cap_def 1182 pas_refined_all_auth_is_owns) 1183 apply (rule conjI) 1184 apply (clarsimp simp: cap_auth_conferred_def is_page_cap_def pas_refined_all_auth_is_owns 1185 aag_cap_auth_def cli_no_irqs cap_links_asid_slot_def) 1186 apply (clarsimp simp: cap_auth_conferred_def vspace_cap_rights_to_auth_def 1187 mask_vm_rights_def validate_vm_rights_def vm_read_only_def 1188 vm_kernel_only_def) 1189 done 1190 \<comment> \<open>Unmap\<close> 1191 subgoal by (simp add: aag_cap_auth_def cli_no_irqs) 1192 done 1193 \<comment> \<open>PageTableCap\<close> 1194 apply (find_goal \<open>match premises in "cap = PageTableCap _ _" \<Rightarrow> succeed\<close>) 1195 subgoal for s word option 1196 apply (cases "invocation_type label"; (solves \<open>simp\<close>)?) 1197 apply (find_goal \<open>match premises in "_ = ArchInvocationLabel _" \<Rightarrow> succeed\<close>) 1198 apply (rename_tac archlabel) 1199 apply (case_tac archlabel; (solves \<open>simp\<close>)?) 1200 \<comment> \<open>PTMap\<close> 1201 apply (find_goal \<open>match premises in "_ = ARMPageTableMap" \<Rightarrow> succeed\<close>) 1202 apply (clarsimp simp: aag_cap_auth_def cli_no_irqs cap_links_asid_slot_def 1203 cap_auth_conferred_def is_page_cap_def 1204 pde_ref2_def pas_refined_all_auth_is_owns pas_refined_refl 1205 pd_shifting[folded pd_bits_14]) 1206 \<comment> \<open>Unmap\<close> 1207 apply (find_goal \<open>match premises in "_ = ARMPageTableUnmap" \<Rightarrow> succeed\<close>) 1208 subgoal 1209 apply (clarsimp simp: aag_cap_auth_def cli_no_irqs cap_links_asid_slot_def 1210 cap_auth_conferred_def is_page_cap_def 1211 pde_ref2_def pas_refined_all_auth_is_owns pas_refined_refl) 1212 apply (subgoal_tac "x && ~~ mask pt_bits = word") 1213 apply simp 1214 apply (clarsimp simp: valid_cap_simps cap_aligned_def split: if_split_asm) 1215 apply (subst (asm) upto_enum_step_subtract) 1216 apply (subgoal_tac "is_aligned word pt_bits") 1217 apply (simp add: is_aligned_no_overflow) 1218 apply (simp add: pt_bits_def pageBits_def) 1219 apply (simp add: word_minus_1 minus_one_norm) 1220 apply (subst (asm) upto_enum_step_red [where us = 2, simplified]) 1221 apply (simp add: pt_bits_def pageBits_def word_bits_conv) 1222 apply (simp add: pt_bits_def pageBits_def word_bits_conv) 1223 apply clarsimp 1224 apply (subst is_aligned_add_helper) 1225 apply (simp add: pt_bits_def pageBits_def) 1226 apply (erule word_less_power_trans_ofnat [where k = 2, simplified]) 1227 apply (simp add: pt_bits_def pageBits_def) 1228 apply (simp add: pt_bits_def pageBits_def word_bits_conv) 1229 apply simp 1230 done 1231 done 1232 done 1233 1234crunch pas_refined[wp]: invalidate_asid_entry "pas_refined aag" 1235 (wp: crunch_wps simp: crunch_simps) 1236 1237crunch pas_refined[wp]: flush_space "pas_refined aag" 1238 (wp: crunch_wps simp: crunch_simps) 1239 1240lemma delete_asid_pas_refined[wp]: 1241 "\<lbrace>pas_refined aag\<rbrace> delete_asid asid pd \<lbrace>\<lambda>rv. pas_refined aag\<rbrace>" 1242 apply (simp add: delete_asid_def) 1243 apply (wp | wpc)+ 1244 apply (clarsimp simp add: split_def Ball_def obj_at_def) 1245 apply (rule conjI) 1246 apply (clarsimp dest!: auth_graph_map_memD graph_ofD) 1247 apply (erule pas_refined_mem[OF sta_vref, rotated]) 1248 apply (fastforce simp: state_vrefs_def vs_refs_no_global_pts_def 1249 image_def graph_of_def split: if_split_asm) 1250 apply (clarsimp simp: pas_refined_def dest!: graph_ofD) 1251 apply (erule subsetD, erule state_asids_to_policy_aux.intros) 1252 apply (fastforce simp: state_vrefs_def vs_refs_no_global_pts_def 1253 graph_of_def image_def split: if_split_asm) 1254 done 1255 1256lemma delete_asid_pool_pas_refined [wp]: 1257 "\<lbrace>pas_refined aag\<rbrace> delete_asid_pool param_a param_b \<lbrace>\<lambda>_. pas_refined aag\<rbrace>" 1258 unfolding delete_asid_pool_def 1259 apply (wp | wpc | simp)+ 1260 apply (rule_tac Q = "\<lambda>_ s. pas_refined aag s \<and> asid_table = arm_asid_table (arch_state s)" in hoare_post_imp) 1261 apply clarsimp 1262 apply (erule pas_refined_clear_asid) 1263 apply (wp mapM_wp' | simp)+ 1264 done 1265 1266crunch respects[wp]: invalidate_asid_entry "integrity aag X st" 1267 1268crunch respects[wp]: flush_space "integrity aag X st" 1269 (ignore: do_machine_op simp: invalidateLocalTLB_ASID_def cleanCaches_PoU_def dsb_def clean_D_PoU_def invalidate_I_PoU_def do_machine_op_bind) 1270 1271lemma delete_asid_pool_respects[wp]: 1272 "\<lbrace> integrity aag X st and K (\<forall>asid'. 1273 asid' \<noteq> 0 \<and> asid_high_bits_of asid' = asid_high_bits_of x \<longrightarrow> 1274 is_subject_asid aag asid')\<rbrace> 1275 delete_asid_pool x y 1276 \<lbrace> \<lambda>_. integrity aag X st \<rbrace>" 1277 unfolding delete_asid_pool_def 1278 apply simp 1279 apply (wp mapM_wp[OF _ subset_refl] | simp)+ 1280 done 1281 1282 1283lemma pas_refined_asid_mem: 1284 "\<lbrakk> v \<in> state_asids_to_policy aag s; pas_refined aag s \<rbrakk> 1285 \<Longrightarrow> v \<in> pasPolicy aag" 1286 by (auto simp add: pas_refined_def) 1287 1288 1289lemma set_asid_pool_respects_clear: 1290 "\<lbrace>(\<lambda>s. \<forall>pool'. ko_at (ArchObj (arch_kernel_obj.ASIDPool pool')) ptr s 1291 \<longrightarrow> asid_pool_integrity {pasSubject aag} aag pool' pool) 1292 and integrity aag X st\<rbrace> 1293 set_asid_pool ptr pool \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>" 1294 apply (simp add: set_asid_pool_def) 1295 apply (wpsimp wp: set_object_wp_strong 1296 simp: obj_at_def a_type_def 1297 split: Structures_A.kernel_object.split_asm arch_kernel_obj.split_asm if_splits) 1298 apply (erule integrity_trans) 1299 apply (clarsimp simp: integrity_def) 1300 apply (rule tro_asidpool_clear; simp add: asid_pool_integrity_def) 1301 done 1302 1303lemma delete_asid_respects: 1304 "\<lbrace>integrity aag X st and pas_refined aag and invs and K (is_subject aag pd)\<rbrace> 1305 delete_asid asid pd 1306 \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>" 1307 by (wpsimp wp: set_asid_pool_respects_clear hoare_vcg_all_lift 1308 simp: obj_at_def pas_refined_refl delete_asid_def asid_pool_integrity_def) 1309 1310end 1311 1312end 1313