1(* 2 * Copyright 2014, General Dynamics C4 Systems 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(GD_GPL) 9 *) 10 11theory ArchArch_AI 12imports "../Arch_AI" 13begin 14 15context Arch begin global_naming ARM 16 17definition 18 "valid_aci aci \<equiv> case aci of MakePool frame slot parent base \<Rightarrow> 19 \<lambda>s. cte_wp_at (\<lambda>c. c = cap.NullCap) slot s \<and> real_cte_at slot s \<and> 20 ex_cte_cap_wp_to is_cnode_cap slot s \<and> 21 slot \<noteq> parent \<and> 22 cte_wp_at (\<lambda>cap. \<exists>idx. cap = UntypedCap False frame pageBits idx ) parent s \<and> 23 descendants_of parent (cdt s) = {} \<and> 24 is_aligned base asid_low_bits \<and> base \<le> 2^asid_bits - 1 \<and> 25 arm_asid_table (arch_state s) (asid_high_bits_of base) = None" 26 27definition 28 "valid_vcpu_invocation vi \<equiv> case vi of 29 VCPUSetTCB vcpu_ptr tcb_ptr \<Rightarrow> vcpu_at vcpu_ptr and tcb_at tcb_ptr and 30 ex_nonz_cap_to vcpu_ptr and ex_nonz_cap_to tcb_ptr 31 and (\<lambda>s. tcb_ptr \<noteq> idle_thread s) 32 | VCPUInjectIRQ vcpu_ptr index virq \<Rightarrow> vcpu_at vcpu_ptr 33 | VCPUReadRegister vcpu_ptr reg \<Rightarrow> vcpu_at vcpu_ptr 34 | VCPUWriteRegister vcpu_ptr reg val \<Rightarrow> vcpu_at vcpu_ptr" 35 36lemma safe_parent_strg: 37 "cte_wp_at (\<lambda>cap. cap = UntypedCap False frame pageBits idx) p s \<and> 38 descendants_of p (cdt s) = {} \<and> 39 valid_objs s 40 \<longrightarrow> 41 cte_wp_at (safe_parent_for (cdt s) p 42 (ArchObjectCap (ASIDPoolCap frame base))) 43 p s" 44 apply (clarsimp simp: cte_wp_at_caps_of_state safe_parent_for_def is_physical_def arch_is_physical_def) 45 apply (rule is_aligned_no_overflow) 46 apply (drule (1) caps_of_state_valid_cap) 47 apply (clarsimp simp: valid_cap_def cap_aligned_def) 48 done 49 50 51lemma asid_low_bits_pageBits: 52 "Suc (Suc asid_low_bits) = pageBits" 53 by (simp add: pageBits_def asid_low_bits_def) 54 55 56(* 32-bit instance of Detype_AI.range_cover_full *) 57lemma range_cover_full: 58 "\<lbrakk>is_aligned ptr sz;sz<word_bits\<rbrakk> \<Longrightarrow> range_cover (ptr::word32) sz sz (Suc 0)" 59 by (clarsimp simp:range_cover_def unat_eq_0 le_mask_iff[symmetric] word_and_le1 word_bits_def) 60 61 62definition 63 valid_arch_inv :: "arch_invocation \<Rightarrow> 'z::state_ext state \<Rightarrow> bool" 64where 65 "valid_arch_inv \<equiv> \<lambda>ai. case ai of 66 InvokePageTable pti \<Rightarrow> 67 valid_pti pti 68 | InvokePageDirectory pdi \<Rightarrow> 69 valid_pdi pdi 70 | InvokePage pinv \<Rightarrow> 71 valid_page_inv pinv 72 | InvokeASIDControl aci \<Rightarrow> 73 valid_aci aci 74 | InvokeASIDPool ap \<Rightarrow> 75 valid_apinv ap 76 | InvokeVCPU vi \<Rightarrow> 77 valid_vcpu_invocation vi" 78 79 80lemma check_vp_wpR [wp]: 81 "\<lbrace>\<lambda>s. vmsz_aligned w sz \<longrightarrow> P () s\<rbrace> 82 check_vp_alignment sz w \<lbrace>P\<rbrace>, -" 83 apply (simp add: check_vp_alignment_def unlessE_whenE cong: vmpage_size.case_cong) 84 apply (rule hoare_pre) 85 apply (wp hoare_whenE_wp|wpc)+ 86 apply (simp add: vmsz_aligned_def) 87 done 88 89 90lemma check_vp_inv: "\<lbrace>P\<rbrace> check_vp_alignment sz w \<lbrace>\<lambda>_. P\<rbrace>" 91 apply (simp add: check_vp_alignment_def unlessE_whenE cong: vmpage_size.case_cong) 92 apply (rule hoare_pre) 93 apply (wp hoare_whenE_wp|wpc)+ 94 apply simp 95 done 96 97 98lemma p2_low_bits_max: 99 "(2 ^ asid_low_bits - 1) = (max_word :: 10 word)" 100 by (simp add: asid_low_bits_def max_word_def) 101 102 103lemma dom_ucast_eq: 104 "(- dom (\<lambda>a::asid_low_index. p (ucast a::machine_word)) \<inter> {x. ucast x + y \<noteq> 0} = {}) = 105 (- dom p \<inter> {x. x \<le> 2 ^ asid_low_bits - 1 \<and> x + y \<noteq> 0} = {})" 106 apply safe 107 apply clarsimp 108 apply (rule ccontr) 109 apply (erule_tac x="ucast x" in in_emptyE) 110 apply (clarsimp simp: p2_low_bits_max) 111 apply (rule conjI) 112 apply (clarsimp simp: ucast_ucast_mask) 113 apply (subst (asm) less_mask_eq) 114 apply (rule word_less_sub_le [THEN iffD1]) 115 apply (simp add: word_bits_def) 116 apply (simp add: asid_low_bits_def) 117 apply simp 118 apply (clarsimp simp: ucast_ucast_mask) 119 apply (subst (asm) less_mask_eq) 120 apply (rule word_less_sub_le [THEN iffD1]) 121 apply (simp add: word_bits_def) 122 apply (simp add: asid_low_bits_def) 123 apply simp 124 apply (clarsimp simp: p2_low_bits_max) 125 apply (rule ccontr) 126 apply simp 127 apply (erule_tac x="ucast x" in in_emptyE) 128 apply clarsimp 129 apply (rule conjI, blast) 130 apply (rule word_less_sub_1) 131 apply (rule order_less_le_trans) 132 apply (rule ucast_less, simp) 133 apply (simp add: asid_low_bits_def) 134 done 135 136 137lemma asid_high_bits_max_word: 138 "(2 ^ asid_high_bits - 1 :: 7 word) = max_word" 139 by (simp add: asid_high_bits_def max_word_def) 140 141 142lemma dom_ucast_eq_7: 143 "(- dom (\<lambda>a::7 word. p (ucast a::word32)) \<inter> {x. x \<le> 2 ^ asid_high_bits - 1} = {}) = 144 (- dom p \<inter> {x. x \<le> 2 ^ asid_high_bits - 1} = {})" 145 apply safe 146 apply clarsimp 147 apply (rule ccontr) 148 apply (erule_tac x="ucast x" in in_emptyE) 149 apply (clarsimp simp: asid_high_bits_max_word) 150 apply (clarsimp simp: ucast_ucast_mask) 151 apply (subst (asm) less_mask_eq) 152 apply (rule word_less_sub_le [THEN iffD1]) 153 apply (simp add: word_bits_def) 154 apply (simp add: asid_high_bits_def) 155 apply simp 156 apply (clarsimp simp: asid_high_bits_max_word) 157 apply (rule ccontr) 158 apply simp 159 apply (erule_tac x="ucast x" in in_emptyE) 160 apply clarsimp 161 apply (rule conjI, blast) 162 apply (rule word_less_sub_1) 163 apply (rule order_less_le_trans) 164 apply (rule ucast_less, simp) 165 apply (simp add: asid_high_bits_def) 166 done 167 168 169lemma ucast_fst_hd_assocs: 170 "- dom (\<lambda>x. pool (ucast (x::asid_low_index)::machine_word)) \<inter> {x. ucast x + (w::machine_word) \<noteq> 0} \<noteq> {} 171 \<Longrightarrow> 172 fst (hd [(x, y)\<leftarrow>assocs pool . x \<le> 2 ^ asid_low_bits - 1 \<and> x + w \<noteq> 0 \<and> y = None]) = 173 ucast (fst (hd [(x, y)\<leftarrow>assocs (\<lambda>a::asid_low_index. pool (ucast a)) . 174 x \<le> 2 ^ asid_low_bits - 1 \<and> 175 ucast x + w \<noteq> 0 \<and> y = None]))" 176 apply (simp add: ucast_assocs[unfolded o_def]) 177 apply (simp add: filter_map split_def) 178 apply (simp cong: conj_cong add: ucast_ucast_len) 179 apply (simp add: asid_low_bits_def minus_one_norm) 180 apply (simp add: ord_le_eq_trans [OF word_n1_ge]) 181 apply (simp add: word_le_make_less) 182 apply (subgoal_tac "P" for P) (* cut_tac but more awesome *) 183 apply (subst hd_map, assumption) 184 apply simp 185 apply (rule sym, rule ucast_ucast_len) 186 apply (drule hd_in_set) 187 apply simp 188 apply (simp add: assocs_empty_dom_comp null_def split_def) 189 apply (simp add: ucast_assocs[unfolded o_def] filter_map split_def) 190 apply (simp cong: conj_cong add: ucast_ucast_len) 191 done 192 193 194crunch typ_at [wp]: perform_page_table_invocation, perform_page_invocation, 195 perform_asid_pool_invocation, perform_page_directory_invocation "\<lambda>s. P (typ_at T p s)" 196 (wp: crunch_wps) 197 198crunch typ_at [wp]: perform_vcpu_invocation "\<lambda>s. P (typ_at T p s)" 199 (wp: crunch_wps) 200 201lemmas perform_page_table_invocation_typ_ats [wp] = 202 abs_typ_at_lifts [OF perform_page_table_invocation_typ_at] 203 204lemmas perform_page_directory_invocation_typ_ats [wp] = 205 abs_typ_at_lifts [OF perform_page_directory_invocation_typ_at] 206 207lemmas perform_page_invocation_typ_ats [wp] = 208 abs_typ_at_lifts [OF perform_page_invocation_typ_at] 209 210lemmas perform_asid_pool_invocation_typ_ats [wp] = 211 abs_typ_at_lifts [OF perform_asid_pool_invocation_typ_at] 212 213lemmas perform_vcpu_invocation_typ_ats [wp] = 214 abs_typ_at_lifts [OF perform_vcpu_invocation_typ_at] 215(* ARMHYP FIXME this is not enough, add appropriate lifting rule to abs_typ_at_lifts *) 216 217lemma perform_asid_control_invocation_tcb_at: 218 "\<lbrace>invs and valid_aci aci and st_tcb_at active p and 219 K (\<forall>w a b c. aci = asid_control_invocation.MakePool w a b c \<longrightarrow> w \<noteq> p)\<rbrace> 220 perform_asid_control_invocation aci 221 \<lbrace>\<lambda>rv. tcb_at p\<rbrace>" 222 apply (simp add: perform_asid_control_invocation_def) 223 apply (cases aci) 224 apply clarsimp 225 apply (wp |simp)+ 226 apply (wp obj_at_delete_objects retype_region_obj_at_other2 hoare_vcg_const_imp_lift|assumption)+ 227 apply (intro impI conjI) 228 apply (clarsimp simp: retype_addrs_def obj_bits_api_def default_arch_object_def image_def ptr_add_def) 229 apply (clarsimp simp: st_tcb_at_tcb_at)+ 230 apply (frule st_tcb_ex_cap) 231 apply fastforce 232 apply (clarsimp split: Structures_A.thread_state.splits) 233 apply auto[1] 234 apply (clarsimp simp: ex_nonz_cap_to_def valid_aci_def) 235 apply (frule invs_untyped_children) 236 apply (clarsimp simp:cte_wp_at_caps_of_state) 237 apply (erule_tac ptr="(aa,ba)" in untyped_children_in_mdbE[where P="\<lambda>c. t \<in> zobj_refs c" for t]) 238 apply (simp add: cte_wp_at_caps_of_state) 239 apply simp 240 apply (simp add:cte_wp_at_caps_of_state) 241 apply fastforce 242 apply (clarsimp simp: zobj_refs_to_obj_refs) 243 apply (erule(1) in_empty_interE) 244 apply (clarsimp simp:page_bits_def) 245 apply simp 246 done 247 248 249lemma ucast_asid_high_btis_of_le [simp]: 250 "ucast (asid_high_bits_of w) \<le> (2 ^ asid_high_bits - 1 :: word32)" 251 apply (simp add: asid_high_bits_of_def) 252 apply (rule word_less_sub_1) 253 apply (rule order_less_le_trans) 254 apply (rule ucast_less) 255 apply simp 256 apply (simp add: asid_high_bits_def) 257 done 258 259crunch tcb_at[wp]: perform_vcpu_invocation "tcb_at p" 260 261lemma invoke_arch_tcb: 262 "\<lbrace>invs and valid_arch_inv ai and st_tcb_at active tptr\<rbrace> 263 arch_perform_invocation ai 264 \<lbrace>\<lambda>rv. tcb_at tptr\<rbrace>" 265 apply (simp add: arch_perform_invocation_def) 266 apply (cases ai, simp_all) 267 apply (wp, clarsimp simp: st_tcb_at_tcb_at)+ 268 defer 269 apply (wp, clarsimp simp: st_tcb_at_tcb_at) 270 defer 271 apply (wp perform_asid_control_invocation_tcb_at) 272 apply (clarsimp simp add: valid_arch_inv_def) 273 apply (clarsimp simp: valid_aci_def) 274 apply (frule st_tcb_ex_cap) 275 apply fastforce 276 apply (clarsimp split: Structures_A.thread_state.splits) 277 apply auto[1] 278 apply (clarsimp simp: ex_nonz_cap_to_def) 279 apply (frule invs_untyped_children) 280 apply (clarsimp simp:cte_wp_at_caps_of_state) 281 apply (erule_tac ptr="(aa,ba)" in untyped_children_in_mdbE[where P="\<lambda>c. t \<in> zobj_refs c" for t]) 282 apply (simp add: cte_wp_at_caps_of_state)+ 283 apply fastforce 284 apply (clarsimp simp: zobj_refs_to_obj_refs cte_wp_at_caps_of_state) 285 apply (drule_tac p="(aa,ba)" in caps_of_state_valid_cap, fastforce) 286 apply (clarsimp simp: valid_cap_def cap_aligned_def) 287 apply (drule_tac x=tptr in base_member_set, simp) 288 apply (simp add: vspace_bits_defs field_simps del: atLeastAtMost_iff) 289 apply (metis (no_types) orthD1 x_power_minus_1) 290 apply simp 291 apply wp 292 apply (clarsimp simp: st_tcb_at_def tcb_at_def obj_at_def is_tcb_def) 293 done 294 295end 296 297 298locale asid_update = Arch + 299 fixes ap asid s s' 300 assumes ko: "ko_at (ArchObj (ASIDPool Map.empty)) ap s" 301 assumes empty: "arm_asid_table (arch_state s) asid = None" 302 defines "s' \<equiv> s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := arm_asid_table (arch_state s)(asid \<mapsto> ap)\<rparr>\<rparr>" 303 304 305context asid_update begin 306 307lemma vs_lookup1' [simp]: 308 "vs_lookup1 s' = vs_lookup1 s" 309 by (simp add: vs_lookup1_def s'_def) 310 311 312lemma vs_lookup_pages1' [simp]: 313 "vs_lookup_pages1 s' = vs_lookup_pages1 s" 314 by (simp add: vs_lookup_pages1_def s'_def) 315 316 317lemma vs_asid_refs' [simp]: 318 "vs_asid_refs (arm_asid_table (arch_state s')) = 319 vs_asid_refs (arm_asid_table (arch_state s)) \<union> {([VSRef (ucast asid) None], ap)}" 320 apply (simp add: s'_def) 321 apply (rule set_eqI) 322 apply (rule iffI) 323 apply (auto simp: vs_asid_refs_def split: if_split_asm)[1] 324 apply clarsimp 325 apply (erule disjE) 326 apply (auto simp: vs_asid_refs_def)[1] 327 apply (subst (asm) vs_asid_refs_def) 328 apply (clarsimp dest!: graph_ofD) 329 apply (rule vs_asid_refsI) 330 apply (clarsimp simp: empty) 331 done 332 333 334lemma vs_lookup': 335 "vs_lookup s' = vs_lookup s \<union> {([VSRef (ucast asid) None], ap)}" 336 using ko 337 apply (simp add: vs_lookup_def) 338 apply (rule rtrancl_insert) 339 apply (clarsimp simp: vs_lookup1_def obj_at_def vs_refs_def) 340 done 341 342 343lemma vs_lookup_pages': 344 "vs_lookup_pages s' = vs_lookup_pages s \<union> {([VSRef (ucast asid) None], ap)}" 345 using ko 346 apply (simp add: vs_lookup_pages_def) 347 apply (rule rtrancl_insert) 348 apply (clarsimp simp: vs_lookup_pages1_def obj_at_def vs_refs_pages_def) 349 done 350 351lemma obj_at [simp]: 352 "obj_at P p s' = obj_at P p s" 353 by (simp add: s'_def) 354 355lemma vs_lookup_neq: "\<lbrakk>(rs \<rhd> p) s' ; p \<noteq> ap\<rbrakk> \<Longrightarrow> (rs \<rhd> p) s" 356 by (clarsimp simp: vs_lookup') 357 358lemma vspace_objs': 359 "valid_vspace_objs s \<Longrightarrow> valid_vspace_objs s'" 360 using ko 361 apply (clarsimp simp: valid_vspace_objs_def) 362 apply (erule_tac x=p in allE) 363 apply (case_tac "p = ap"; 364 case_tac ao; 365 fastforce simp: obj_at_def s'_def 366 intro: vs_lookup_neq) 367 done 368 369lemma caps_of_state_s': 370 "caps_of_state s' = caps_of_state s" 371 by (rule caps_of_state_pspace, simp add: s'_def) 372 373 374lemma valid_vs_lookup': 375 "\<lbrakk> valid_vs_lookup s; 376 \<exists>ptr cap. caps_of_state s ptr = Some cap 377 \<and> ap \<in> obj_refs cap \<and> vs_cap_ref cap = Some [VSRef (ucast asid) None] \<rbrakk> 378 \<Longrightarrow> valid_vs_lookup s'" 379 by (clarsimp simp: valid_vs_lookup_def caps_of_state_s' vs_lookup_pages') 380 381 382lemma valid_table_caps': 383 "\<lbrakk> valid_table_caps s \<rbrakk> 384 \<Longrightarrow> valid_table_caps s'" 385 apply (simp add: valid_table_caps_def caps_of_state_s') 386 done 387 388 389lemma valid_arch_caps: 390 "\<lbrakk> valid_arch_caps s; 391 \<exists>ptr cap. caps_of_state s ptr = Some cap 392 \<and> ap \<in> obj_refs cap \<and> vs_cap_ref cap = Some [VSRef (ucast asid) None] \<rbrakk> 393 \<Longrightarrow> valid_arch_caps s'" 394 by (simp add: valid_arch_caps_def caps_of_state_s' 395 valid_table_caps' valid_vs_lookup') 396 397 398lemma valid_asid_map': 399 "valid_asid_map s \<Longrightarrow> valid_asid_map s'" 400 using empty 401 apply (clarsimp simp: valid_asid_map_def s'_def) 402 apply (drule bspec, blast) 403 apply (clarsimp simp: vspace_at_asid_def) 404 apply (drule vs_lookup_2ConsD) 405 apply clarsimp 406 apply (erule vs_lookup_atE) 407 apply (drule vs_lookup1D) 408 apply clarsimp 409 apply (rule vs_lookupI[rotated]) 410 apply (rule r_into_rtrancl) 411 apply (rule vs_lookup1I) 412 apply (fastforce simp: obj_at_def) 413 apply assumption 414 apply simp 415 apply (clarsimp simp: vs_asid_refs_def graph_of_def) 416 apply fastforce 417 done 418 419end 420 421 422context Arch begin global_naming ARM 423 424lemma valid_arch_state_strg: 425 "valid_arch_state s \<and> ap \<notin> ran (arm_asid_table (arch_state s)) \<and> asid_pool_at ap s \<longrightarrow> 426 valid_arch_state (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := arm_asid_table (arch_state s)(asid \<mapsto> ap)\<rparr>\<rparr>)" 427 apply (clarsimp simp: valid_arch_state_def split: option.split) 428 apply (clarsimp simp: valid_asid_table_def ran_def) 429 apply (fastforce intro!: inj_on_fun_updI) 430 done 431 432 433lemma valid_vs_lookup_at_upd_strg: 434 "valid_vs_lookup s \<and> 435 ko_at (ArchObj (ASIDPool Map.empty)) ap s \<and> 436 arm_asid_table (arch_state s) asid = None \<and> 437 (\<exists>ptr cap. caps_of_state s ptr = Some cap \<and> ap \<in> obj_refs cap \<and> 438 vs_cap_ref cap = Some [VSRef (ucast asid) None]) 439 \<longrightarrow> 440 valid_vs_lookup (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := arm_asid_table (arch_state s)(asid \<mapsto> ap)\<rparr>\<rparr>)" 441 apply clarsimp 442 apply (subgoal_tac "asid_update ap asid s") 443 prefer 2 444 apply unfold_locales[1] 445 apply assumption+ 446 apply (erule (1) asid_update.valid_vs_lookup') 447 apply fastforce 448 done 449 450 451lemma retype_region_ap: 452 "\<lbrace>\<top>\<rbrace> 453 retype_region ap 1 0 (ArchObject ASIDPoolObj) dev 454 \<lbrace>\<lambda>_. ko_at (ArchObj (arch_kernel_obj.ASIDPool Map.empty)) ap\<rbrace>" 455 apply (rule hoare_post_imp) 456 prefer 2 457 apply (rule retype_region_obj_at) 458 apply simp 459 apply simp 460 apply (clarsimp simp: retype_addrs_def obj_bits_api_def default_arch_object_def) 461 apply (clarsimp simp: obj_at_def default_object_def default_arch_object_def) 462 done 463 464 465lemma retype_region_ap': 466 "\<lbrace>\<top>\<rbrace> retype_region ap 1 0 (ArchObject ASIDPoolObj) dev \<lbrace>\<lambda>rv. asid_pool_at ap\<rbrace>" 467 apply (rule hoare_strengthen_post, rule retype_region_ap) 468 apply (clarsimp simp: a_type_def elim!: obj_at_weakenE) 469 done 470 471 472lemma no_cap_to_obj_with_diff_ref_null_filter: 473 "no_cap_to_obj_with_diff_ref cap S 474 = (\<lambda>s. \<forall>c \<in> ran (null_filter (caps_of_state s) |` (- S)). 475 obj_refs c = obj_refs cap 476 \<longrightarrow> table_cap_ref c = table_cap_ref cap)" 477 apply (simp add: no_cap_to_obj_with_diff_ref_def 478 ball_ran_eq cte_wp_at_caps_of_state) 479 apply (simp add: Ball_def) 480 apply (intro iff_allI ext) 481 apply (simp add: restrict_map_def null_filter_def) 482 apply (auto dest!: obj_ref_none_no_asid[rule_format] 483 simp: table_cap_ref_def) 484 done 485 486 487lemma retype_region_no_cap_to_obj: 488 "\<lbrace>valid_pspace and valid_mdb 489 and caps_overlap_reserved {ptr..ptr + 2 ^ obj_bits_api ty us - 1} 490 and caps_no_overlap ptr sz 491 and pspace_no_overlap_range_cover ptr sz 492 and no_cap_to_obj_with_diff_ref cap S 493 and (\<lambda>s. \<exists>slot. cte_wp_at (\<lambda>c. up_aligned_area ptr sz \<subseteq> cap_range c \<and> cap_is_device c = dev) slot s) 494 and K (ty = Structures_A.CapTableObject \<longrightarrow> 0 < us) 495 and K (range_cover ptr sz (obj_bits_api ty us) 1) \<rbrace> 496 retype_region ptr 1 us ty dev 497 \<lbrace>\<lambda>rv. no_cap_to_obj_with_diff_ref cap S\<rbrace>" 498 apply (rule hoare_gen_asm)+ 499 apply (simp add: no_cap_to_obj_with_diff_ref_null_filter) 500 apply (wp retype_region_caps_of | simp)+ 501 apply fastforce 502 done 503 504 505lemma valid_table_caps_asid_upd [iff]: 506 "valid_table_caps (s\<lparr>arch_state := (arm_asid_table_update f (arch_state s))\<rparr>) = 507 valid_table_caps s" 508 by (simp add: valid_table_caps_def) 509 510 511lemma vs_asid_ref_upd: 512 "([VSRef (ucast (asid_high_bits_of asid')) None] \<rhd> ap') 513 (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := arm_asid_table (arch_state s)(asid_high_bits_of asid \<mapsto> ap)\<rparr>\<rparr>) 514 = (if asid_high_bits_of asid' = asid_high_bits_of asid 515 then ap' = ap 516 else ([VSRef (ucast (asid_high_bits_of asid')) None] \<rhd> ap') s)" 517 by (fastforce intro: vs_lookup_atI elim: vs_lookup_atE) 518 519 520lemma vs_asid_ref_eq: 521 "([VSRef (ucast asid) None] \<rhd> ap) s 522 = (arm_asid_table (arch_state s) asid = Some ap)" 523 by (fastforce elim: vs_lookup_atE intro: vs_lookup_atI) 524 525 526lemma set_cap_reachable_pg_cap: 527 "\<lbrace>\<lambda>s. P (reachable_pg_cap cap s)\<rbrace> set_cap x y \<lbrace>\<lambda>_ s. P (reachable_pg_cap cap s)\<rbrace>" 528 by (unfold reachable_pg_cap_def, wp hoare_vcg_ex_lift set_cap.vs_lookup_pages) 529 530 531lemma cap_insert_simple_arch_caps_ap: 532 "\<lbrace>valid_arch_caps and (\<lambda>s. cte_wp_at (safe_parent_for (cdt s) src cap) src s) 533 and no_cap_to_obj_with_diff_ref cap {dest} 534 and (\<lambda>s. arm_asid_table (arch_state s) (asid_high_bits_of asid) = None) 535 and ko_at (ArchObj (ASIDPool Map.empty)) ap 536 and K (cap = ArchObjectCap (ASIDPoolCap ap asid)) \<rbrace> 537 cap_insert cap src dest 538 \<lbrace>\<lambda>rv s. valid_arch_caps (s\<lparr>arch_state := arch_state s 539 \<lparr>arm_asid_table := arm_asid_table (arch_state s)(asid_high_bits_of asid \<mapsto> ap)\<rparr>\<rparr>)\<rbrace>" 540 apply (simp add: cap_insert_def update_cdt_def set_cdt_def valid_arch_caps_def 541 set_untyped_cap_as_full_def bind_assoc) 542 apply (strengthen valid_vs_lookup_at_upd_strg) 543 apply (wp get_cap_wp set_cap_valid_vs_lookup set_cap_arch_obj 544 set_cap_valid_table_caps hoare_vcg_all_lift 545 | simp split del: if_split)+ 546 apply (rule_tac P = "cte_wp_at ((=) src_cap) src" in set_cap_orth) 547 apply (wp hoare_vcg_imp_lift hoare_vcg_ball_lift set_free_index_final_cap 548 hoare_vcg_disj_lift set_cap_reachable_pg_cap set_cap.vs_lookup_pages 549 | clarsimp)+ 550 apply (wp set_cap_arch_obj set_cap_valid_table_caps hoare_vcg_ball_lift 551 get_cap_wp static_imp_wp set_cap_empty_tables[simplified second_level_tables_def, simplified])+ 552 apply (clarsimp simp: cte_wp_at_caps_of_state is_cap_simps) 553 apply (rule conjI) 554 apply (clarsimp simp: vs_cap_ref_def) 555 apply (rule_tac x="fst dest" in exI) 556 apply (rule_tac x="snd dest" in exI) 557 apply simp 558 apply (rule conjI) 559 apply (simp add: unique_table_caps_def is_cap_simps) 560 apply (subst unique_table_refs_def) 561 apply (intro allI impI) 562 apply (simp split: if_split_asm) 563 apply (simp add: no_cap_to_obj_with_diff_ref_def cte_wp_at_caps_of_state) 564 apply (simp add: no_cap_to_obj_with_diff_ref_def cte_wp_at_caps_of_state) 565 apply (erule (3) unique_table_refsD) 566 done 567 568lemma valid_asid_map_asid_upd_strg: 569 "valid_asid_map s \<and> 570 ko_at (ArchObj (ASIDPool Map.empty)) ap s \<and> 571 arm_asid_table (arch_state s) asid = None \<longrightarrow> 572 valid_asid_map (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := arm_asid_table (arch_state s)(asid \<mapsto> ap)\<rparr>\<rparr>)" 573 apply clarsimp 574 apply (subgoal_tac "asid_update ap asid s") 575 prefer 2 576 apply unfold_locales[1] 577 apply assumption+ 578 apply (erule (1) asid_update.valid_asid_map') 579 done 580 581lemma valid_vspace_objs_asid_upd_strg: 582 "valid_vspace_objs s \<and> 583 ko_at (ArchObj (ASIDPool Map.empty)) ap s \<and> 584 arm_asid_table (arch_state s) asid = None \<longrightarrow> 585 valid_vspace_objs (s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := arm_asid_table (arch_state s)(asid \<mapsto> ap)\<rparr>\<rparr>)" 586 apply clarsimp 587 apply (subgoal_tac "asid_update ap asid s") 588 prefer 2 589 apply unfold_locales[1] 590 apply assumption+ 591 apply (erule (1) asid_update.vspace_objs') 592 done 593 594lemma safe_parent_cap_is_device: 595 "safe_parent_for m p cap pcap \<Longrightarrow> cap_is_device cap = cap_is_device pcap" 596 by (simp add: safe_parent_for_def) 597 598lemma cap_insert_ap_invs: 599 "\<lbrace>invs and valid_cap cap and tcb_cap_valid cap dest and 600 ex_cte_cap_wp_to (appropriate_cte_cap cap) dest and 601 cte_wp_at (\<lambda>c. c = NullCap) dest and 602 no_cap_to_obj_with_diff_ref cap {dest} and 603 (\<lambda>s. cte_wp_at (safe_parent_for (cdt s) src cap) src s) and 604 K (cap = ArchObjectCap (ASIDPoolCap ap asid)) and 605 (\<lambda>s. \<forall>irq \<in> cap_irqs cap. irq_issued irq s) and 606 ko_at (ArchObj (ASIDPool Map.empty)) ap and 607 (\<lambda>s. ap \<notin> ran (arm_asid_table (arch_state s)) \<and> 608 arm_asid_table (arch_state s) (asid_high_bits_of asid) = None)\<rbrace> 609 cap_insert cap src dest 610 \<lbrace>\<lambda>rv s. invs (s\<lparr>arch_state := arch_state s 611 \<lparr>arm_asid_table := (arm_asid_table \<circ> arch_state) s(asid_high_bits_of asid \<mapsto> ap)\<rparr>\<rparr>)\<rbrace>" 612 613 apply (simp add: invs_def valid_state_def valid_pspace_def) 614 apply (strengthen valid_arch_state_strg valid_vspace_objs_asid_upd_strg 615 valid_asid_map_asid_upd_strg ) 616 apply (simp cong: conj_cong) 617 apply (rule hoare_pre) 618 apply (wpsimp wp: cap_insert_simple_mdb cap_insert_iflive 619 cap_insert_zombies cap_insert_ifunsafe 620 cap_insert_valid_global_refs cap_insert_idle 621 valid_irq_node_typ cap_insert_simple_arch_caps_ap 622 simp: valid_global_objs_def valid_global_vspace_mappings_def) 623 apply (clarsimp simp: is_simple_cap_def cte_wp_at_caps_of_state is_cap_simps) 624 apply (frule safe_parent_cap_is_device) 625 apply (drule safe_parent_cap_range) 626 apply (simp add: cap_range_def) 627 apply (rule conjI) 628 apply clarsimp 629 apply (drule_tac p="(a,b)" in caps_of_state_valid_cap, fastforce) 630 apply (auto simp: obj_at_def is_tcb_def is_cap_table_def a_type_def 631 valid_cap_def [where c="cap.Zombie a b x" for a b x] 632 dest: obj_ref_is_tcb obj_ref_is_cap_table split: option.splits) 633 done 634 635lemma max_index_upd_no_cap_to: 636 "\<lbrace>\<lambda>s. no_cap_to_obj_with_diff_ref cap {slot} s \<and> 637 cte_wp_at ((=) ucap) cref s \<and> is_untyped_cap ucap\<rbrace> 638 set_cap (max_free_index_update ucap) cref 639 \<lbrace>\<lambda>rv s. no_cap_to_obj_with_diff_ref cap {slot} s \<rbrace>" 640 apply (clarsimp simp:no_cap_to_obj_with_diff_ref_def) 641 apply (wp hoare_vcg_ball_lift set_cap_cte_wp_at_neg) 642 apply (clarsimp simp:cte_wp_at_caps_of_state free_index_update_def is_cap_simps) 643 apply (drule_tac x = cref in bspec) 644 apply clarsimp 645 apply (clarsimp simp:table_cap_ref_def) 646 done 647 648 649lemma perform_asid_control_invocation_st_tcb_at: 650 "\<lbrace>st_tcb_at (P and (Not \<circ> inactive) and (Not \<circ> idle)) t 651 and ct_active and invs and valid_aci aci\<rbrace> 652 perform_asid_control_invocation aci 653 \<lbrace>\<lambda>y. st_tcb_at P t\<rbrace>" 654 supply 655 is_aligned_neg_mask_eq[simp del] 656 is_aligned_neg_mask_weaken[simp del] 657 apply (clarsimp simp: perform_asid_control_invocation_def split: asid_control_invocation.splits) 658 apply (rename_tac word1 a b aa ba word2) 659 apply (rule hoare_name_pre_state) 660 apply (subgoal_tac "is_aligned word1 page_bits") 661 prefer 2 662 apply (clarsimp simp: valid_aci_def cte_wp_at_caps_of_state) 663 apply (drule(1) caps_of_state_valid[rotated])+ 664 apply (simp add:valid_cap_simps cap_aligned_def page_bits_def) 665 apply (subst delete_objects_rewrite) 666 apply (simp add:page_bits_def word_bits_def word_size_bits_def pageBits_def)+ 667 apply (simp add:is_aligned_neg_mask_eq) 668 apply (wp hoare_vcg_const_imp_lift retype_region_st_tcb_at set_cap_no_overlap|simp)+ 669 apply (strengthen invs_valid_objs invs_psp_aligned) 670 apply (clarsimp simp:conj_comms) 671 apply (wp max_index_upd_invs_simple get_cap_wp)+ 672 apply (clarsimp simp: valid_aci_def) 673 apply (frule intvl_range_conv) 674 apply (simp add:word_bits_def page_bits_def pageBits_def) 675 apply (clarsimp simp:detype_clear_um_independent page_bits_def is_aligned_neg_mask_eq) 676 apply (rule conjI) 677 apply (clarsimp simp:cte_wp_at_caps_of_state) 678 apply (rule pspace_no_overlap_detype) 679 apply (rule caps_of_state_valid_cap) 680 apply (simp add:page_bits_def)+ 681 apply (simp add:invs_valid_objs invs_psp_aligned)+ 682 apply (rule conjI) 683 apply (erule pred_tcb_weakenE, simp) 684 apply (rule conjI) 685 apply (frule st_tcb_ex_cap) 686 apply clarsimp 687 apply (clarsimp split: Structures_A.thread_state.splits) 688 apply (clarsimp simp: ex_nonz_cap_to_def) 689 apply (frule invs_untyped_children) 690 apply (clarsimp simp:cte_wp_at_caps_of_state) 691 apply (erule_tac ptr="(aa,ba)" in untyped_children_in_mdbE[where P="\<lambda>c. t \<in> zobj_refs c" for t]) 692 apply (simp add: cte_wp_at_caps_of_state)+ 693 apply fastforce 694 apply (clarsimp simp: zobj_refs_to_obj_refs) 695 apply (fastforce simp:page_bits_def) 696 apply simp 697 apply (clarsimp simp:obj_bits_api_def arch_kobj_size_def cte_wp_at_caps_of_state 698 default_arch_object_def empty_descendants_range_in) 699 apply (frule_tac cap = "(cap.UntypedCap False word1 pageBits idx)" 700 in detype_invariants[rotated 3],clarsimp+) 701 apply (simp add:cte_wp_at_caps_of_state 702 empty_descendants_range_in descendants_range_def2)+ 703 apply (thin_tac "x = Some cap.NullCap" for x)+ 704 apply (drule(1) caps_of_state_valid_cap[OF _ invs_valid_objs]) 705 apply (intro conjI) 706 apply (clarsimp simp:valid_cap_def cap_aligned_def range_cover_full 707 invs_psp_aligned invs_valid_objs page_bits_def) 708 apply (erule pspace_no_overlap_detype) 709 apply (auto simp:page_bits_def detype_clear_um_independent) 710 done 711 712 713lemma set_cap_idx_up_aligned_area: 714 "\<lbrace>K (\<exists>idx. pcap = UntypedCap dev ptr pageBits idx) and cte_wp_at ((=) pcap) slot 715 and valid_objs\<rbrace> set_cap (max_free_index_update pcap) slot 716 \<lbrace>\<lambda>rv s. (\<exists>slot. cte_wp_at (\<lambda>c. up_aligned_area ptr pageBits \<subseteq> cap_range c \<and> cap_is_device c = dev) slot s)\<rbrace>" 717 apply (rule hoare_pre) 718 apply (wp hoare_vcg_ex_lift set_cap_cte_wp_at) 719 apply (rule_tac x = slot in exI) 720 apply clarsimp 721 apply (frule(1) cte_wp_valid_cap) 722 apply (clarsimp simp: cte_wp_at_caps_of_state is_aligned_neg_mask_eq 723 p_assoc_help valid_cap_def valid_untyped_def cap_aligned_def) 724 done 725 726primrec(nonexhaustive) get_untyped_cap_idx :: "cap \<Rightarrow> nat" 727where "get_untyped_cap_idx (UntypedCap dev ref sz idx) = idx" 728 729 730lemma aci_invs': 731 assumes Q_ignores_arch[simp]: "\<And>f s. Q (arch_state_update f s) = Q s" 732 assumes Q_ignore_machine_state[simp]: "\<And>f s. Q (machine_state_update f s) = Q s" 733 assumes Q_detype[simp]: "\<And>f s. Q (detype f s) = Q s" 734 assumes cap_insert_Q: "\<And>cap src dest. \<lbrace>Q and invs and K (src \<noteq> dest)\<rbrace> 735 cap_insert cap src dest 736 \<lbrace>\<lambda>_.Q\<rbrace>" 737 assumes retype_region_Q[wp]:"\<And>a b c d e. \<lbrace>Q\<rbrace> retype_region a b c d e \<lbrace>\<lambda>_.Q\<rbrace>" 738 assumes set_cap_Q[wp]: "\<And>a b. \<lbrace>Q\<rbrace> set_cap a b \<lbrace>\<lambda>_.Q\<rbrace>" 739 shows 740 "\<lbrace>invs and Q and ct_active and valid_aci aci\<rbrace> perform_asid_control_invocation aci \<lbrace>\<lambda>y s. invs s \<and> Q s\<rbrace>" 741 proof - 742 have cap_insert_invsQ: 743 "\<And>cap src dest ap asid. 744 \<lbrace>Q and (invs and valid_cap cap and tcb_cap_valid cap dest and 745 ex_cte_cap_wp_to (appropriate_cte_cap cap) dest and 746 cte_wp_at (\<lambda>c. c = NullCap) dest and 747 no_cap_to_obj_with_diff_ref cap {dest} and 748 (\<lambda>s. cte_wp_at (safe_parent_for (cdt s) src cap) src s) and 749 K (cap = ArchObjectCap (ASIDPoolCap ap asid)) and 750 (\<lambda>s. \<forall>irq\<in>cap_irqs cap. irq_issued irq s) and 751 ko_at (ArchObj (ASIDPool Map.empty)) ap and 752 (\<lambda>s. ap \<notin> ran (arm_asid_table (arch_state s)) \<and> 753 arm_asid_table (arch_state s) (asid_high_bits_of asid) = None))\<rbrace> 754 cap_insert cap src dest 755 \<lbrace>\<lambda>rv s. 756 invs 757 (s\<lparr>arch_state := arch_state s 758 \<lparr>arm_asid_table := (arm_asid_table \<circ> arch_state) s 759 (asid_high_bits_of asid \<mapsto> ap)\<rparr>\<rparr>) \<and> 760 Q 761 (s\<lparr>arch_state := arch_state s 762 \<lparr>arm_asid_table := (arm_asid_table \<circ> arch_state) s 763 (asid_high_bits_of asid \<mapsto> ap)\<rparr>\<rparr>)\<rbrace>" 764 apply (wp cap_insert_ap_invs) 765 apply simp 766 apply (rule hoare_pre) 767 apply (rule cap_insert_Q) 768 apply (auto simp: cte_wp_at_caps_of_state) 769 done 770 show ?thesis 771 apply (clarsimp simp: perform_asid_control_invocation_def valid_aci_def 772 split: asid_control_invocation.splits) 773 apply (rename_tac word1 a b aa ba word2) 774 apply (rule hoare_pre) 775 apply (wp hoare_vcg_const_imp_lift) 776 apply (wp cap_insert_invsQ hoare_vcg_ex_lift 777 | simp)+ 778 apply (simp add: valid_cap_def | 779 strengthen real_cte_tcb_valid safe_parent_strg 780 invs_vobjs_strgs 781 ex_cte_cap_to_cnode_always_appropriate_strg)+ 782 apply (wp hoare_vcg_const_imp_lift set_free_index_invs 783 retype_region_plain_invs[where sz = pageBits] 784 retype_cte_wp_at[where sz = pageBits] hoare_vcg_ex_lift 785 retype_region_obj_at_other3[where P="is_cap_table n" and sz = pageBits for n] 786 retype_region_ex_cte_cap_to[where sz = pageBits] 787 retype_region_ap[simplified] 788 retype_region_ap'[simplified] 789 retype_region_no_cap_to_obj[where sz = pageBits,simplified] 790 | simp del: split_paired_Ex)+ 791 apply (strengthen invs_valid_objs invs_psp_aligned invs_mdb invs_valid_pspace 792 exI[where x="case aci of MakePool frame slot parent base \<Rightarrow> parent"] 793 exI[where x="case aci of MakePool frame slot parent base \<Rightarrow> parent", simplified] 794 caps_region_kernel_window_imp[where 795 p = "case aci of MakePool frame slot parent base \<Rightarrow> parent"] 796 invs_cap_refs_in_kernel_window)+ 797 apply (wp set_cap_caps_no_overlap set_cap_no_overlap get_cap_wp 798 max_index_upd_caps_overlap_reserved max_index_upd_invs_simple 799 set_cap_cte_cap_wp_to set_cap_cte_wp_at max_index_upd_no_cap_to 800 | simp split del: if_split | wp_once hoare_vcg_ex_lift)+ 801 apply (rule_tac P = "is_aligned word1 page_bits" in hoare_gen_asm) 802 apply (subst delete_objects_rewrite) 803 apply (simp add:page_bits_def pageBits_def word_size_bits_def) 804 apply (simp add:page_bits_def pageBits_def word_bits_def) 805 apply (simp add:is_aligned_neg_mask_eq) 806 apply wp 807 apply (clarsimp simp: cte_wp_at_caps_of_state if_option_Some 808 Word_Miscellaneous.if_bool_simps 809 split del: if_split) 810 apply (strengthen refl) 811 apply (frule_tac cap = "(cap.UntypedCap False word1 pageBits idx)" 812 in detype_invariants[rotated 3],clarsimp+) 813 apply (simp add:cte_wp_at_caps_of_state)+ 814 apply (simp add:descendants_range_def2 empty_descendants_range_in) 815 apply (simp add:invs_mdb invs_valid_pspace invs_psp_aligned invs_valid_objs) 816 apply (clarsimp dest!:caps_of_state_cteD) 817 apply (frule(1) unsafe_protected[where p=t and p'=t for t]) 818 apply (simp add:empty_descendants_range_in)+ 819 apply fastforce 820 apply clarsimp 821 apply (frule_tac p = "(aa,ba)" in cte_wp_valid_cap) 822 apply fastforce 823 apply (clarsimp simp: detype_clear_um_independent obj_bits_api_def arch_kobj_size_def 824 default_arch_object_def conj_comms) 825 apply (rule conjI) 826 apply (clarsimp simp:valid_cap_simps cap_aligned_def page_bits_def not_le) 827 apply clarsimp 828 apply (simp add:empty_descendants_range_in) 829 apply (frule valid_cap_aligned) 830 apply (clarsimp simp: cap_aligned_def is_aligned_neg_mask_eq) 831 apply (subst caps_no_overlap_detype[OF descendants_range_caps_no_overlapI], 832 assumption, simp add: is_aligned_neg_mask_eq, 833 simp add: empty_descendants_range_in) 834 apply (frule pspace_no_overlap_detype, clarify+) 835 apply (frule intvl_range_conv[where bits = pageBits]) 836 apply (simp add:pageBits_def word_bits_def) 837 apply (simp add:is_aligned_neg_mask_eq) 838 apply (clarsimp simp:is_aligned_neg_mask_eq page_bits_def) 839 apply (frule(1) ex_cte_cap_protects) 840 apply (simp add:empty_descendants_range_in) 841 apply fastforce 842 apply (rule subset_refl) 843 apply fastforce 844 apply (clarsimp simp: field_simps) 845 apply (intro conjI impI, 846 simp_all add:free_index_of_def valid_cap_simps valid_untyped_def 847 empty_descendants_range_in range_cover_full clear_um_def max_free_index_def, 848 (clarsimp simp:valid_untyped_def valid_cap_simps)+)[1] 849 850 apply (erule(1) cap_to_protected) 851 apply (simp add:empty_descendants_range_in descendants_range_def2)+ 852 853 apply clarsimp 854 apply (drule invs_arch_state)+ 855 apply (clarsimp simp: valid_arch_state_def valid_asid_table_def) 856 apply (drule (1) bspec)+ 857 apply clarsimp 858 apply (erule notE, erule is_aligned_no_overflow) 859 860 apply (clarsimp simp: no_cap_to_obj_with_diff_ref_def) 861 apply (thin_tac "cte_wp_at ((=) cap.NullCap) p s" for p s) 862 apply (subst(asm) eq_commute, 863 erule(1) untyped_children_in_mdbE[where cap="cap.UntypedCap dev p bits idx" for dev p bits idx, 864 simplified, rotated]) 865 apply (simp add: is_aligned_no_overflow) 866 apply simp 867 apply clarsimp 868 done 869 870qed 871 872lemmas aci_invs[wp] = aci_invs'[where Q=\<top>,simplified hoare_post_taut, OF refl refl refl TrueI TrueI TrueI,simplified] 873 874lemma obj_at_upd2: 875 "obj_at P t' (s\<lparr>kheap := kheap s(t \<mapsto> v, x \<mapsto> v')\<rparr>) = (if t' = x then P v' else obj_at P t' (s\<lparr>kheap := kheap s(t \<mapsto> v)\<rparr>))" 876 by (simp add: obj_at_update obj_at_def) 877 878lemma vcpu_invalidate_active_hyp_refs_empty[wp]: 879 "\<lbrace>obj_at (\<lambda>ko. hyp_refs_of ko = {}) p\<rbrace> vcpu_invalidate_active \<lbrace>\<lambda>r. obj_at (\<lambda>ko. hyp_refs_of ko = {}) p\<rbrace>" 880 unfolding vcpu_invalidate_active_def vcpu_disable_def by wpsimp 881 882lemma as_user_hyp_refs_empty[wp]: 883 "\<lbrace>obj_at (\<lambda>ko. hyp_refs_of ko = {}) p\<rbrace> as_user t f \<lbrace>\<lambda>r. obj_at (\<lambda>ko. hyp_refs_of ko = {}) p\<rbrace>" 884 unfolding as_user_def 885 apply (wpsimp wp: set_object_wp) 886 by (clarsimp simp: get_tcb_Some_ko_at obj_at_def arch_tcb_context_set_def) 887 888lemma dissociate_vcpu_tcb_obj_at_hyp_refs[wp]: 889 "\<lbrace>\<lambda>s. p \<notin> {t, vr} \<longrightarrow> obj_at (\<lambda>ko. hyp_refs_of ko = {}) p s \<rbrace> 890 dissociate_vcpu_tcb t vr 891 \<lbrace>\<lambda>rv s. obj_at (\<lambda>ko. hyp_refs_of ko = {}) p s\<rbrace>" 892 unfolding dissociate_vcpu_tcb_def 893 apply (cases "p \<notin> {t, vr}"; clarsimp) 894 apply (wp arch_thread_set_wp set_vcpu_wp) 895 apply (clarsimp simp: obj_at_upd2 obj_at_update) 896 apply (wp hoare_drop_imp get_vcpu_wp)+ 897 apply (clarsimp simp: obj_at_upd2 obj_at_update) 898 apply (erule disjE; 899 (wp arch_thread_set_wp set_vcpu_wp 900 | clarsimp simp: obj_at_upd2 obj_at_update)+) 901 done 902 903lemma associate_vcpu_tcb_sym_refs_hyp[wp]: 904 "\<lbrace>\<lambda>s. sym_refs (state_hyp_refs_of s)\<rbrace> associate_vcpu_tcb vr t \<lbrace>\<lambda>rv s. sym_refs (state_hyp_refs_of s)\<rbrace>" 905 apply (simp add: associate_vcpu_tcb_def) 906 apply (wp arch_thread_set_wp set_vcpu_wp | clarsimp)+ 907 apply (rule_tac P="\<lambda>s. ko_at (ArchObj (VCPU v)) vr s \<and> 908 obj_at (\<lambda>ko. hyp_refs_of ko = {} ) t s \<and> 909 sym_refs (state_hyp_refs_of s)" 910 in hoare_triv) 911 apply (rule_tac Q="\<lambda>rv s. obj_at (\<lambda>ko. hyp_refs_of ko = {} ) vr s \<and> 912 obj_at (\<lambda>ko. hyp_refs_of ko = {} ) t s \<and> 913 sym_refs (state_hyp_refs_of s)" 914 in hoare_post_imp) 915 apply (clarsimp dest!: get_tcb_SomeD simp: obj_at_def) 916 apply (clarsimp simp add: sym_refs_def) 917 apply (case_tac "x = t"; case_tac "x = vr"; clarsimp simp add: state_hyp_refs_of_def obj_at_def 918 dest!: get_tcb_SomeD) 919 apply fastforce 920 apply (rule hoare_pre) 921 apply (wp | wpc | clarsimp)+ 922 apply (simp add: obj_at_def) 923 apply (wp get_vcpu_ko | wpc | clarsimp)+ 924 apply (rule_tac Q="\<lambda>rv s. (\<exists>t'. obj_at (\<lambda>tcb. tcb = TCB t' \<and> rv = tcb_vcpu (tcb_arch t')) t s) \<and> 925 sym_refs (state_hyp_refs_of s)" 926 in hoare_post_imp) 927 apply (clarsimp simp: obj_at_def) 928 apply (wp arch_thread_get_tcb) 929 apply simp 930 done 931 932lemma arch_thread_set_inv_neq: 933 "\<lbrace>obj_at P p and K (t \<noteq> p)\<rbrace> arch_thread_set f t \<lbrace>\<lambda>rv. obj_at P p\<rbrace>" 934 unfolding arch_thread_set_def by (wpsimp wp: set_object_wp) (simp add: obj_at_def) 935 936lemma live_vcpu [simp]: 937 "live (ArchObj (VCPU (v\<lparr>vcpu_tcb := Some tcb\<rparr>)))" 938 by (simp add: live_def hyp_live_def arch_live_def) 939 940lemma ex_nonz_cap_to_vcpu_udpate[simp]: 941 "ex_nonz_cap_to t (s\<lparr>arch_state := arm_current_vcpu_update f (arch_state s)\<rparr>) = ex_nonz_cap_to t s" 942 by (simp add: ex_nonz_cap_to_def) 943 944lemma caps_of_state_VCPU_update: 945 "vcpu_at a s \<Longrightarrow> caps_of_state (s\<lparr>kheap := kheap s(a \<mapsto> ArchObj (VCPU b))\<rparr>) = caps_of_state s" 946 by (rule ext) (auto simp: caps_of_state_cte_wp_at cte_wp_at_cases obj_at_def) 947 948lemma set_vcpu_ex_nonz_cap_to[wp]: 949 "\<lbrace>ex_nonz_cap_to t\<rbrace> set_vcpu a b \<lbrace>\<lambda>_. ex_nonz_cap_to t\<rbrace>" 950 apply (wp set_vcpu_wp) 951 apply (clarsimp simp: ex_nonz_cap_to_def cte_wp_at_caps_of_state caps_of_state_VCPU_update) 952 done 953 954lemma caps_of_state_tcb_arch_update: 955 "ko_at (TCB y) t' s \<Longrightarrow> caps_of_state (s\<lparr>kheap := kheap s(t' \<mapsto> TCB (y\<lparr>tcb_arch := f (tcb_arch y)\<rparr>))\<rparr>) = caps_of_state s" 956 by (rule ext) (auto simp: caps_of_state_cte_wp_at cte_wp_at_cases obj_at_def tcb_cap_cases_def) 957 958lemma arch_thread_set_ex_nonz_cap_to[wp]: 959 "\<lbrace>ex_nonz_cap_to t\<rbrace> arch_thread_set f t' \<lbrace>\<lambda>_. ex_nonz_cap_to t\<rbrace>" 960 apply (wp arch_thread_set_wp) 961 apply clarsimp 962 apply (clarsimp simp: ex_nonz_cap_to_def get_tcb_Some_ko_at cte_wp_at_caps_of_state 963 caps_of_state_tcb_arch_update) 964 done 965 966crunch ex_nonz_cap_to[wp]: dissociate_vcpu_tcb "ex_nonz_cap_to t" 967 (wp: crunch_wps) 968 969lemma associate_vcpu_tcb_if_live_then_nonz_cap[wp]: 970 "\<lbrace>if_live_then_nonz_cap and ex_nonz_cap_to vcpu and ex_nonz_cap_to tcb\<rbrace> 971 associate_vcpu_tcb vcpu tcb \<lbrace>\<lambda>_. if_live_then_nonz_cap\<rbrace>" 972 unfolding associate_vcpu_tcb_def 973 by (wpsimp wp: arch_thread_set_inv_neq hoare_disjI1 get_vcpu_wp hoare_vcg_all_lift hoare_drop_imps) 974 975lemma set_vcpu_valid_arch_Some[wp]: 976 "\<lbrace>valid_arch_state\<rbrace> set_vcpu vcpu (v\<lparr>vcpu_tcb := Some tcb\<rparr>) \<lbrace>\<lambda>_. valid_arch_state\<rbrace>" 977 apply (wp set_vcpu_wp) 978 apply (clarsimp simp: valid_arch_state_def) 979 apply (rule conjI) 980 apply (fastforce simp: valid_asid_table_def obj_at_def) 981 apply (clarsimp simp: obj_at_def is_vcpu_def hyp_live_def arch_live_def split: option.splits) 982 done 983 984lemma valid_global_objs_vcpu_update_str: 985 "valid_global_objs s \<Longrightarrow> valid_global_objs (s\<lparr>arch_state := arm_current_vcpu_update f (arch_state s)\<rparr>)" 986 by (simp add: valid_global_objs_def) 987 988lemma valid_global_vspace_mappings_vcpu_update_str: 989 "valid_global_vspace_mappings s \<Longrightarrow> valid_global_vspace_mappings (s\<lparr>arch_state := arm_current_vcpu_update f (arch_state s)\<rparr>)" 990 by (simp add: valid_global_vspace_mappings_def) 991 992lemma associate_vcpu_tcb_invs[wp]: 993 "\<lbrace>invs and ex_nonz_cap_to vcpu and ex_nonz_cap_to tcb and vcpu_at vcpu and (\<lambda>s. tcb \<noteq> idle_thread s)\<rbrace> 994 associate_vcpu_tcb vcpu tcb 995 \<lbrace>\<lambda>_. invs\<rbrace>" 996 using valid_global_vspace_mappings_def 997 apply (simp add: invs_def valid_state_def valid_pspace_def) 998 apply (simp add: pred_conj_def) 999 apply (rule hoare_pre) 1000 apply (rule hoare_vcg_conj_lift[rotated])+ 1001 by (wp get_vcpu_wp arch_thread_get_wp weak_if_wp as_user_only_idle hoare_vcg_all_lift 1002 | wp_once hoare_drop_imps 1003 | wpc 1004 | clarsimp 1005 | strengthen valid_arch_state_vcpu_update_str valid_global_refs_vcpu_update_str 1006 valid_global_vspace_mappings_vcpu_update_str valid_global_objs_vcpu_update_str 1007 | simp add: associate_vcpu_tcb_def valid_obj_def[abs_def] valid_vcpu_def 1008 dissociate_vcpu_tcb_def vcpu_invalidate_active_def vcpu_disable_def 1009 | simp add: obj_at_def)+ 1010 1011lemma set_vcpu_regs_update[wp]: 1012 "\<lbrace>invs and valid_obj p (ArchObj (VCPU vcpu)) and 1013 obj_at (\<lambda>ko'. hyp_refs_of ko' = vcpu_tcb_refs (vcpu_tcb vcpu)) p\<rbrace> 1014 set_vcpu p (vcpu_regs_update f vcpu) \<lbrace>\<lambda>_. invs\<rbrace>" 1015 unfolding invs_def valid_state_def 1016 by (wpsimp wp: set_vcpu_valid_pspace set_vcpu_valid_arch_eq_hyp) 1017 1018lemma vcpu_write_reg_invs[wp]: 1019 "\<lbrace>invs\<rbrace> vcpu_write_reg vcpuptr r v \<lbrace>\<lambda>_. invs\<rbrace>" 1020 unfolding vcpu_write_reg_def vcpu_update_def 1021 apply (wpsimp wp: get_vcpu_wp) 1022 apply (fastforce simp: obj_at_def dest!: invs_valid_objs) 1023 done 1024 1025lemma write_vcpu_register_invs[wp]: 1026 "\<lbrace>invs\<rbrace> write_vcpu_register vcpu reg val \<lbrace>\<lambda>_. invs\<rbrace>" 1027 unfolding write_vcpu_register_def 1028 by wpsimp 1029 1030lemma vgic_update_valid_pspace[wp]: 1031 "\<lbrace>valid_pspace\<rbrace> vgic_update vcpuptr f \<lbrace>\<lambda>_. valid_pspace\<rbrace>" 1032 unfolding vgic_update_def vcpu_update_def 1033 apply (wpsimp wp: set_vcpu_valid_pspace get_vcpu_wp simp: valid_vcpu_def) 1034 apply (fastforce simp: obj_at_def dest!: valid_pspace_vo) 1035 done 1036 1037crunches invoke_vcpu_inject_irq, vcpu_read_reg 1038 for invs[wp]: invs (ignore: do_machine_op) 1039 1040lemma perform_vcpu_invs[wp]: 1041 "\<lbrace>invs and valid_vcpu_invocation vi\<rbrace> perform_vcpu_invocation vi \<lbrace>\<lambda>_. invs\<rbrace>" 1042 apply (simp add: perform_vcpu_invocation_def valid_vcpu_invocation_def) 1043 apply (wpsimp simp: invoke_vcpu_read_register_def read_vcpu_register_def 1044 invoke_vcpu_write_register_def) 1045 done 1046 1047lemma invoke_arch_invs[wp]: 1048 "\<lbrace>invs and ct_active and valid_arch_inv ai\<rbrace> 1049 arch_perform_invocation ai 1050 \<lbrace>\<lambda>rv. invs\<rbrace>" 1051 apply (cases ai, simp_all add: valid_arch_inv_def arch_perform_invocation_def) 1052 apply (wp perform_vcpu_invs |simp)+ 1053 done 1054 1055 1056lemma sts_empty_pde [wp]: 1057 "\<lbrace>empty_pde_at p\<rbrace> set_thread_state t st \<lbrace>\<lambda>rv. empty_pde_at p\<rbrace>" 1058 apply (simp add: empty_pde_at_def) 1059 apply (rule hoare_pre) 1060 apply (wp hoare_vcg_ex_lift set_thread_state_ko) 1061 apply (clarsimp simp: is_tcb_def) 1062 done 1063 1064 1065lemma sts_pd_at_asid [wp]: 1066 "\<lbrace>vspace_at_asid asid pd\<rbrace> set_thread_state t st \<lbrace>\<lambda>rv. vspace_at_asid asid pd\<rbrace>" 1067 apply (simp add: vspace_at_asid_def) 1068 apply wp 1069 done 1070 1071 1072lemma sts_same_refs_inv[wp]: 1073 "\<lbrace>\<lambda>s. same_refs m cap s\<rbrace> set_thread_state t st \<lbrace>\<lambda>rv s. same_refs m cap s\<rbrace>" 1074 by (cases m, (clarsimp simp: same_refs_def, wp)+) 1075 1076 1077lemma sts_valid_slots_inv[wp]: 1078 "\<lbrace>valid_slots m\<rbrace> set_thread_state t st \<lbrace>\<lambda>rv. valid_slots m\<rbrace>" 1079 by (cases m, (clarsimp simp: valid_slots_def, wp hoare_vcg_ball_lift sts.vs_lookup sts_typ_ats)+) 1080 1081 1082lemma sts_valid_page_inv[wp]: 1083"\<lbrace>valid_page_inv page_invocation\<rbrace> set_thread_state t st \<lbrace>\<lambda>rv. valid_page_inv page_invocation\<rbrace>" 1084 by (cases page_invocation, 1085 (wp hoare_vcg_const_Ball_lift hoare_vcg_ex_lift hoare_vcg_imp_lift sts_typ_ats 1086 | clarsimp simp: valid_page_inv_def same_refs_def 1087 | wps)+) 1088 1089 1090lemma sts_valid_pdi_inv[wp]: 1091 "\<lbrace>valid_pdi page_directory_invocation\<rbrace> set_thread_state t st \<lbrace>\<lambda>rv. valid_pdi page_directory_invocation\<rbrace>" 1092 apply (cases page_directory_invocation) 1093 apply (wp | simp add: valid_pdi_def)+ 1094 done 1095 1096 1097lemma sts_valid_vcpu_invocation_inv: 1098 "\<lbrace>valid_vcpu_invocation vcpu_invocation\<rbrace> set_thread_state t st \<lbrace>\<lambda>rv. valid_vcpu_invocation vcpu_invocation\<rbrace>" 1099 unfolding valid_vcpu_invocation_def by (cases vcpu_invocation; wpsimp) 1100 1101lemma sts_valid_arch_inv: 1102 "\<lbrace>valid_arch_inv ai\<rbrace> set_thread_state t st \<lbrace>\<lambda>rv. valid_arch_inv ai\<rbrace>" 1103 apply (cases ai, simp_all add: valid_arch_inv_def) 1104 apply (rename_tac page_table_invocation) 1105 apply (case_tac page_table_invocation, simp_all add: valid_pti_def)[1] 1106 apply ((wp valid_pde_lift set_thread_state_valid_cap 1107 hoare_vcg_all_lift hoare_vcg_const_imp_lift 1108 hoare_vcg_ex_lift set_thread_state_ko 1109 sts_typ_ats set_thread_state_cte_wp_at 1110 | clarsimp simp: is_tcb_def)+)[4] 1111 apply (rename_tac asid_control_invocation) 1112 apply (case_tac asid_control_invocation) 1113 apply (clarsimp simp: valid_aci_def cte_wp_at_caps_of_state) 1114 apply (rule hoare_pre, wp hoare_vcg_ex_lift cap_table_at_typ_at) 1115 apply clarsimp 1116 apply (clarsimp simp: valid_apinv_def split: asid_pool_invocation.splits) 1117 apply (rule hoare_pre) 1118 apply (wp hoare_vcg_ex_lift set_thread_state_ko) 1119 apply (clarsimp simp: is_tcb_def, wp sts_valid_vcpu_invocation_inv) 1120 done 1121 1122crunch inv[wp]: ensure_safe_mapping, create_mapping_entries "P" 1123 (wp: crunch_wps mapME_x_inv_wp) 1124 1125crunch_ignore (add: select_ext) 1126 1127crunch inv [wp]: arch_decode_invocation "P" 1128 (wp: crunch_wps select_wp select_ext_weak_wp simp: crunch_simps) 1129 1130 1131lemma create_mappings_empty [wp]: 1132 "\<lbrace>\<top>\<rbrace> create_mapping_entries base vptr vmsz R A pd \<lbrace>\<lambda>m s. empty_refs m\<rbrace>, -" 1133 apply (cases vmsz, simp_all add: empty_refs_def) 1134 apply (wpsimp simp: pde_ref_def)+ 1135 done 1136 1137 1138lemma empty_pde_atI: 1139 "\<lbrakk> ko_at (ArchObj (PageDirectory pd)) (p && ~~ mask pd_bits) s; 1140 pd (ucast (p && mask pd_bits >> 3)) = InvalidPDE \<rbrakk> \<Longrightarrow> 1141 empty_pde_at p s" 1142 by (fastforce simp add: vspace_bits_defs empty_pde_at_def) 1143 1144 1145declare lookup_slot_for_cnode_op_cap_to [wp] 1146 1147 1148lemma shiftr_irrelevant: 1149 "x < 2 ^ asid_low_bits \<Longrightarrow> is_aligned (y :: word32) asid_low_bits \<Longrightarrow> 1150 x + y >> asid_low_bits = y >> asid_low_bits" 1151 apply (subst word_plus_and_or_coroll) 1152 apply (rule word_eqI) 1153 apply (clarsimp simp: is_aligned_nth) 1154 apply (drule(1) nth_bounded) 1155 apply (simp add: asid_low_bits_def word_bits_def) 1156 apply simp 1157 apply (rule word_eqI) 1158 apply (simp add: nth_shiftr) 1159 apply safe 1160 apply (drule(1) nth_bounded) 1161 apply (simp add: asid_low_bits_def word_bits_def) 1162 apply simp 1163 done 1164 1165lemma map_up_enum_0x78: 1166 "is_aligned (r::32 word) 7 \<Longrightarrow> map (\<lambda>x. x + r) [0 , 8 .e. 0x78] = [r, r + 8 .e. r + 0x78]" 1167 apply (simp add: upto_enum_step_def upto_enum_def not_less) 1168 apply (drule is_aligned_no_overflow') 1169 apply simp 1170 apply (erule word_plus_mono_right2) 1171 apply simp 1172 done 1173 1174lemma create_mapping_entries_parent_for_refs: 1175 "\<lbrace>invs and \<exists>\<rhd> pd and page_directory_at pd 1176 and K (is_aligned pd pd_bits) and K (vmsz_aligned vptr pgsz) 1177 and K (vptr < kernel_base)\<rbrace> 1178 create_mapping_entries ptr vptr pgsz 1179 rights attribs pd 1180 \<lbrace>\<lambda>rv s. \<exists>a b. cte_wp_at (parent_for_refs rv) (a, b) s\<rbrace>, -" 1181 apply (rule hoare_gen_asmE)+ 1182 apply (cases pgsz, 1183 simp_all add: vmsz_aligned_def largePagePTE_offsets_def superSectionPDE_offsets_def 1184 pte_bits_def pde_bits_def) 1185 apply (rule hoare_pre) 1186 apply wp 1187 apply (rule hoare_post_imp_R, rule lookup_pt_slot_cap_to) 1188 apply (elim exEI) 1189 apply (clarsimp simp: cte_wp_at_caps_of_state parent_for_refs_def) 1190 apply simp 1191 apply (rule hoare_pre) 1192 apply wp 1193 apply (rule hoare_post_imp_R) 1194 apply (rule lookup_pt_slot_cap_to_multiple1) 1195 apply (elim conjE exEI cte_wp_at_weakenE) 1196 apply (clarsimp simp: cte_wp_at_caps_of_state parent_for_refs_def 1197 subset_iff p_0x3C_shift map_up_enum_0x78) 1198 apply simp 1199 apply (rule hoare_pre, wp) 1200 apply (clarsimp dest!:vs_lookup_pages_vs_lookupI) 1201 apply (drule valid_vs_lookupD, clarsimp) 1202 apply (simp, elim exEI) 1203 apply (clarsimp simp: cte_wp_at_caps_of_state parent_for_refs_def 1204 lookup_pd_slot_def Let_def) 1205 apply (subst pd_shifting, simp add: pd_bits_def pageBits_def pde_bits_def) 1206 apply (clarsimp simp: vs_cap_ref_def 1207 split: cap.split_asm arch_cap.split_asm option.split_asm) 1208 apply (auto simp: valid_cap_def obj_at_def is_cap_simps cap_asid_def 1209 dest!: caps_of_state_valid_cap split:if_splits)[3] 1210 apply (frule(1) caps_of_state_valid) 1211 apply (clarsimp simp:valid_cap_def obj_at_def) 1212 apply (simp add:is_cap_simps) 1213 apply (rule hoare_pre, wp) 1214 apply (clarsimp dest!:vs_lookup_pages_vs_lookupI) 1215 apply (drule valid_vs_lookupD, clarsimp) 1216 apply (simp, elim exEI) 1217 apply (clarsimp simp: cte_wp_at_caps_of_state parent_for_refs_def) 1218 apply (rule conjI) 1219 apply (simp add: subset_eq) 1220 apply (clarsimp simp: lookup_pd_slot_add_eq) 1221 apply (clarsimp simp: vs_cap_ref_def 1222 split: cap.split_asm arch_cap.split_asm option.split_asm) 1223 apply (auto simp: valid_cap_def obj_at_def is_cap_simps cap_asid_def 1224 dest!: caps_of_state_valid_cap split:if_splits)[3] 1225 apply (frule(1) caps_of_state_valid) 1226 apply (clarsimp simp:valid_cap_def obj_at_def) 1227 apply (simp add:is_cap_simps) 1228 done 1229 1230 1231lemma find_pd_for_asid_shifting_voodoo: 1232 "\<lbrace>pspace_aligned and valid_vspace_objs\<rbrace> 1233 find_pd_for_asid asid 1234 \<lbrace>\<lambda>rv s. v >> 21 = rv + (v >> 21 << 3) && mask pd_bits >> 3\<rbrace>,-" 1235 apply (rule hoare_post_imp_R, 1236 rule find_pd_for_asid_aligned_pd, simp add: vspace_bits_defs) 1237 apply (subst pd_shifting_dual[simplified vspace_bits_defs, simplified], simp) 1238 apply (rule word_eqI) 1239 apply (simp add: nth_shiftr nth_shiftl word_size) 1240 apply safe 1241 apply (drule test_bit_size) 1242 apply (simp add: word_size) 1243 done 1244 1245 1246lemma find_pd_for_asid_ref_offset_voodoo: 1247 "\<lbrace>pspace_aligned and valid_vspace_objs and 1248 K (ref = [VSRef (asid && mask asid_low_bits) (Some AASIDPool), 1249 VSRef (ucast (asid_high_bits_of asid)) None])\<rbrace> 1250 find_pd_for_asid asid 1251 \<lbrace>\<lambda>rv. (ref \<rhd> (rv + (v >> 21 << 3) && ~~ mask pd_bits))\<rbrace>,-" 1252 apply (rule hoare_gen_asmE) 1253 apply (rule_tac Q'="\<lambda>rv s. is_aligned rv 14 \<and> (ref \<rhd> rv) s" 1254 in hoare_post_imp_R) 1255 apply (simp add: ucast_ucast_mask 1256 mask_asid_low_bits_ucast_ucast) 1257 apply (fold asid_low_bits_def) 1258 apply (rule hoare_pre, wp find_pd_for_asid_lookup_ref) 1259 apply (simp add: vspace_bits_defs) 1260 apply (simp add: pd_shifting[simplified vspace_bits_defs, simplified] vspace_bits_defs) 1261 done 1262 1263 1264declare asid_high_bits_of_shift [simp] 1265declare mask_shift [simp] 1266declare word_less_sub_le [simp del] 1267declare ptrFormPAddr_addFromPPtr [simp] 1268 1269 1270(* FIXME: move *) 1271lemma valid_mask_vm_rights[simp]: 1272 "mask_vm_rights V R \<in> valid_vm_rights" 1273 by (simp add: mask_vm_rights_def) 1274 1275 1276lemma vs_lookup_and_unique_refs: 1277 "\<lbrakk>(ref \<rhd> p) s; caps_of_state s cptr = Some cap; table_cap_ref cap = Some ref'; 1278 p \<in> obj_refs cap; valid_vs_lookup s; unique_table_refs (caps_of_state s)\<rbrakk> 1279 \<Longrightarrow> ref = ref'" 1280 apply (frule_tac ref=ref in valid_vs_lookupD[OF vs_lookup_pages_vs_lookupI], assumption) 1281 apply clarsimp 1282 apply (frule_tac cap'=capa in unique_table_refsD) 1283 apply simp+ 1284 apply (case_tac capa, simp_all) 1285 apply ((case_tac cap, simp_all)+)[6] 1286 apply (clarsimp simp add: table_cap_ref_def vs_cap_ref_def split: cap.splits arch_cap.splits option.splits) 1287 done 1288 1289 1290lemma create_mapping_entries_same_refs: 1291 "\<lbrace>valid_arch_state and valid_vspace_objs and valid_vs_lookup and (\<lambda>s. unique_table_refs (caps_of_state s)) 1292 and pspace_aligned and valid_objs and valid_kernel_mappings and \<exists>\<rhd> pd and 1293 (\<lambda>s. \<exists>dev pd_cap pd_cptr. cte_wp_at (diminished pd_cap) pd_cptr s 1294 \<and> pd_cap = ArchObjectCap (PageDirectoryCap pd (Some asid))) and 1295 page_directory_at pd and K (vaddr < kernel_base \<and> (cap = (ArchObjectCap (PageCap dev p rights' pgsz (Some (asid, vaddr))))))\<rbrace> 1296 create_mapping_entries (addrFromPPtr p) vaddr pgsz rights attribs pd 1297 \<lbrace>\<lambda>rv s. same_refs rv cap s\<rbrace>,-" 1298 apply (rule hoare_gen_asmE) 1299 apply (cases pgsz, simp_all add: lookup_pt_slot_def) 1300 apply (wp get_pde_wp | wpc)+ 1301 apply (clarsimp simp: lookup_pd_slot_def) 1302 apply (frule (1) pd_aligned) 1303 apply (simp add: pd_shifting) 1304 apply (simp add: vaddr_segment_nonsense2 pageBits_def pt_bits_def pte_bits_def pde_bits_def) 1305 apply (frule (2) valid_vspace_objsD[rotated], simp) 1306 apply (erule_tac x="ucast (vaddr >> 21)" in allE) 1307 apply (simp, drule (1) pt_aligned) 1308 apply (clarsimp simp: same_refs_def vs_cap_ref_def split: option.splits) 1309 apply (simp add: vaddr_segment_nonsense4 shiftl_shiftr_id mask_def[of 9] 1310 less_trans[OF and_mask_less'[where n=9, unfolded mask_def, simplified]] 1311 word_bits_def pageBits_def 1312 vaddr_segment_nonsense3) 1313 apply (rule conjI, simp add: mask_def pt_bits_def pte_bits_def) 1314 apply (clarsimp simp: cte_wp_at_caps_of_state diminished_def 1315 mask_cap_def cap_rights_update_def) 1316 apply (clarsimp split: Structures_A.cap.splits) 1317 apply (clarsimp simp: acap_rights_update_def split: arch_cap.splits) 1318 apply (frule (1) vs_lookup_and_unique_refs) 1319 apply (simp_all add: table_cap_ref_def obj_refs_def)[4] 1320 apply (frule_tac p=pd and p'="ptrFromPAddr x" in vs_lookup_step) 1321 apply (clarsimp simp: vs_lookup1_def) 1322 apply (rule exI, erule conjI) 1323 apply (rule exI[where x="VSRef (vaddr >> 21) (Some APageDirectory)"]) 1324 apply (rule conjI, rule refl) 1325 apply (simp add: vs_refs_def) 1326 apply (rule_tac x="(ucast (vaddr >> 21), ptrFromPAddr x)" in image_eqI) 1327 apply (simp add: ucast_ucast_len[OF shiftr_less_t2n'] mask_32_max_word graph_of_def) 1328 apply (clarsimp simp:graph_of_def) 1329 apply (simp add: pde_ref_def) 1330 apply simp 1331 apply (drule (1) ref_is_unique) 1332 apply (simp add: ptrFromPAddr_def) 1333 apply (simp_all add: pde_ref_def valid_arch_state_def valid_objs_caps pt_bits_def)[8] 1334 apply (wp get_pde_wp | wpc)+ 1335 apply (clarsimp simp: lookup_pd_slot_def) 1336 apply (frule (1) pd_aligned) 1337 apply (simp add: pd_shifting) 1338 apply (simp add: vaddr_segment_nonsense2 pageBits_def pt_bits_def pte_bits_def pde_bits_def) 1339 apply (frule (2) valid_vspace_objsD[rotated], simp) 1340 apply (erule_tac x="ucast (vaddr >> 21)" in allE) 1341 apply (simp, drule (1) pt_aligned) 1342 apply (simp add: largePagePTE_offsets_def pte_bits_def) 1343 apply (clarsimp simp: same_refs_def vs_cap_ref_def upto_enum_step_def upto_enum_word upt_conv_Cons) 1344 apply (simp add: vaddr_segment_nonsense4 shiftl_shiftr_id 1345 less_trans[OF and_mask_less'[where n=9, unfolded mask_def, simplified]] 1346 word_bits_def pageBits_def mask_def [of 9] 1347 vaddr_segment_nonsense3) 1348 apply (simp add: pt_bits_def pte_bits_def) 1349 apply (rule conjI, simp add: mask_def) 1350 apply (clarsimp simp: cte_wp_at_caps_of_state diminished_def 1351 mask_cap_def cap_rights_update_def) 1352 apply (clarsimp split: Structures_A.cap.splits ) 1353 apply (clarsimp simp: acap_rights_update_def split: arch_cap.splits) 1354 apply (frule (1) vs_lookup_and_unique_refs) 1355 apply (simp_all add: table_cap_ref_def obj_refs_def)[4] 1356 apply (frule_tac p=pd and p'="ptrFromPAddr x" in vs_lookup_step) 1357 apply (clarsimp simp: vs_lookup1_def) 1358 apply (rule exI, erule conjI) 1359 apply (rule exI[where x="VSRef (vaddr >> 21) (Some APageDirectory)"]) 1360 apply (rule conjI, rule refl) 1361 apply (simp add: vs_refs_def) 1362 apply (rule_tac x="(ucast (vaddr >> 21), ptrFromPAddr x)" in image_eqI) 1363 apply (simp add: ucast_ucast_len[OF shiftr_less_t2n'] mask_32_max_word graph_of_def) 1364 apply (clarsimp simp:graph_of_def) 1365 apply (simp add: pde_ref_def) 1366 apply simp 1367 apply (drule (1) ref_is_unique) 1368 apply (simp add: ptrFromPAddr_def) 1369 apply (simp_all add: pde_ref_def valid_arch_state_def valid_objs_caps)[8] 1370 apply (wp get_pde_wp returnOKE_R_wp | wpc)+ 1371 apply (clarsimp simp: lookup_pd_slot_def) 1372 apply (frule (1) pd_aligned) 1373 apply (clarsimp simp: same_refs_def vs_cap_ref_def pde_ref_pages_def) 1374 apply (simp add: vaddr_segment_nonsense vaddr_segment_nonsense2 1375 pageBits_def pt_bits_def pte_bits_def pde_bits_def) 1376 apply (clarsimp simp: cte_wp_at_caps_of_state diminished_def 1377 mask_cap_def cap_rights_update_def) 1378 apply (clarsimp split: Structures_A.cap.splits ) 1379 apply (clarsimp simp: acap_rights_update_def split: arch_cap.splits) 1380 apply (frule (1) vs_lookup_and_unique_refs) 1381 apply (simp_all add: table_cap_ref_def obj_refs_def)[4] 1382 apply (drule (1) ref_is_unique) 1383 apply (simp_all add: valid_arch_state_def valid_objs_caps)[7] 1384 apply (wp returnOKE_R_wp | wpc)+ 1385 apply (clarsimp simp: lookup_pd_slot_def) 1386 apply (frule (1) pd_aligned) 1387 apply (simp add: superSectionPDE_offsets_def pde_bits_def pageBits_def pt_bits_def) 1388 apply (clarsimp simp: same_refs_def vs_cap_ref_def pde_ref_pages_def upto_enum_step_def upto_enum_word upt_conv_Cons) 1389 apply (simp add: vaddr_segment_nonsense vaddr_segment_nonsense2 pageBits_def pt_bits_def) 1390 apply (clarsimp simp: cte_wp_at_caps_of_state diminished_def 1391 mask_cap_def cap_rights_update_def) 1392 apply (clarsimp split: Structures_A.cap.splits ) 1393 apply (clarsimp simp: acap_rights_update_def split: arch_cap.splits) 1394 apply (frule (1) vs_lookup_and_unique_refs) 1395 apply (simp_all add: table_cap_ref_def obj_refs_def)[4] 1396 apply (drule (1) ref_is_unique) 1397 apply (clarsimp simp: obj_at_def a_type_def valid_arch_state_def) 1398 apply (simp_all add: valid_arch_state_def valid_objs_caps) 1399 done 1400 1401 1402lemma create_mapping_entries_same_refs_ex: 1403 "\<lbrace>valid_arch_state and valid_vspace_objs and valid_vs_lookup and (\<lambda>s. unique_table_refs (caps_of_state s)) 1404 and pspace_aligned and valid_objs and valid_kernel_mappings and \<exists>\<rhd> pd and 1405 (\<lambda>s. \<exists>dev pd_cap pd_cptr asid rights'. cte_wp_at (diminished pd_cap) pd_cptr s 1406 \<and> pd_cap = cap.ArchObjectCap (arch_cap.PageDirectoryCap pd (Some asid)) 1407 \<and> page_directory_at pd s \<and> vaddr < kernel_base \<and> (cap = (cap.ArchObjectCap (arch_cap.PageCap dev p rights' pgsz (Some (asid, vaddr))))))\<rbrace> 1408 create_mapping_entries (Platform.ARM_HYP.addrFromPPtr p) vaddr pgsz rights attribs pd 1409 \<lbrace>\<lambda>rv s. same_refs rv cap s\<rbrace>,-" 1410 apply (clarsimp simp: validE_R_def validE_def valid_def split: sum.split) 1411 apply (erule use_validE_R[OF _ create_mapping_entries_same_refs]) 1412 apply fastforce 1413 done 1414 1415 1416lemma diminished_pd_capD: 1417 "diminished (ArchObjectCap (PageDirectoryCap a b)) cap 1418 \<Longrightarrow> cap = (ArchObjectCap (PageDirectoryCap a b))" 1419 apply (clarsimp simp: diminished_def mask_cap_def cap_rights_update_def) 1420 apply (clarsimp simp: acap_rights_update_def split: cap.splits arch_cap.splits) 1421 done 1422 1423 1424lemma diminished_pd_self: 1425 "diminished (ArchObjectCap (PageDirectoryCap a b)) (ArchObjectCap (PageDirectoryCap a b))" 1426 apply (clarsimp simp: diminished_def mask_cap_def cap_rights_update_def) 1427 apply (clarsimp simp: acap_rights_update_def split: cap.splits arch_cap.splits) 1428 done 1429 1430 1431lemma cte_wp_at_page_cap_weaken: 1432 "cte_wp_at (diminished (ArchObjectCap (PageCap dev word seta vmpage_size None))) slot s \<Longrightarrow> 1433 cte_wp_at (\<lambda>a. \<exists>dev p R sz m. a = ArchObjectCap (PageCap dev p R sz m)) slot s" 1434 apply (clarsimp simp: cte_wp_at_def diminished_def mask_cap_def cap_rights_update_def) 1435 apply (clarsimp simp: acap_rights_update_def split: cap.splits arch_cap.splits) 1436 done 1437 1438 1439lemma find_pd_for_asid_lookup_pd_wp: 1440 "\<lbrace> \<lambda>s. valid_vspace_objs s \<and> (\<forall>pd. vspace_at_asid asid pd s \<and> page_directory_at pd s 1441 \<and> (\<exists>\<rhd> pd) s \<longrightarrow> Q pd s) \<rbrace> find_pd_for_asid asid \<lbrace> Q \<rbrace>, -" 1442 apply (rule hoare_post_imp_R) 1443 apply (rule hoare_vcg_conj_lift_R[OF find_pd_for_asid_page_directory]) 1444 apply (rule hoare_vcg_conj_lift_R[OF find_pd_for_asid_lookup, simplified]) 1445 apply (rule hoare_vcg_conj_lift_R[OF find_pd_for_asid_pd_at_asid, simplified]) 1446 apply (wp_once find_pd_for_asid_inv) 1447 apply auto 1448 done 1449 1450 1451lemma aligned_sum_less_kernel_base: 1452 "vmsz_aligned p sz 1453 \<Longrightarrow> (p + 2 ^ pageBitsForSize sz - 1 < kernel_base) = (p < kernel_base)" 1454 apply (rule iffI) 1455 apply (rule le_less_trans) 1456 apply (rule is_aligned_no_overflow) 1457 apply (simp add: vmsz_aligned_def) 1458 apply simp 1459 apply (simp add:field_simps[symmetric]) 1460 apply (erule gap_between_aligned) 1461 apply (simp add: vmsz_aligned_def)+ 1462 apply (case_tac sz,simp_all add:kernel_base_def is_aligned_def)+ 1463 done 1464 1465lemma diminished_VCPUCap[simp]: 1466 "diminished (ArchObjectCap (VCPUCap vcpu_ptr)) c = (c = ArchObjectCap (VCPUCap vcpu_ptr))" 1467 apply (cases c; simp add: diminished_def mask_cap_def cap_rights_update_def) 1468 apply (rename_tac acap) 1469 apply (case_tac acap; simp add: acap_rights_update_def) 1470 apply auto 1471 done 1472 1473lemma diminshed_ThreadCap[simp]: 1474 "diminished (ThreadCap t) c = (c = ThreadCap t)" 1475 by (cases c) (auto simp: diminished_def mask_cap_def cap_rights_update_def) 1476 1477lemma find_pd_for_asid_pde_unfolded[wp]: 1478 "\<lbrace>valid_vspace_objs and pspace_aligned\<rbrace> 1479 find_pd_for_asid asid 1480 \<lbrace>\<lambda>pd. pde_at (pd + (vptr >> 21 << 3))\<rbrace>, -" 1481 apply (rule hoare_post_imp_R, rule find_pd_for_asid_pde) 1482 apply (simp add: pageBits_def pt_bits_def pde_bits_def) 1483 done 1484 1485lemma arch_decode_inv_wf[wp]: 1486 "\<lbrace>invs and valid_cap (ArchObjectCap arch_cap) and 1487 cte_wp_at (diminished (ArchObjectCap arch_cap)) slot and 1488 (\<lambda>s. \<forall>x \<in> set excaps. cte_wp_at (diminished (fst x)) (snd x) s)\<rbrace> 1489 arch_decode_invocation label args cap_index slot arch_cap excaps 1490 \<lbrace>valid_arch_inv\<rbrace>,-" 1491 apply (cases arch_cap) 1492 apply (rename_tac word1 word2) 1493 apply (simp add: arch_decode_invocation_def Let_def decode_mmu_invocation_def split_def cong: if_cong split del: if_split) 1494 apply (rule hoare_pre) 1495 apply ((wp whenE_throwError_wp check_vp_wpR ensure_empty_stronger select_wp select_ext_weak_wp| 1496 wpc| 1497 simp add: valid_arch_inv_def valid_apinv_def)+)[1] 1498 apply (simp add: if_apply_def2 valid_apinv_def) 1499 apply (intro allI impI ballI) 1500 apply (elim conjE exE) 1501 apply simp 1502 apply (clarsimp simp: dom_def neq_Nil_conv) 1503 apply (thin_tac "Ball S P" for S P)+ 1504 apply (clarsimp simp: valid_cap_def) 1505 apply (rule conjI) 1506 apply (clarsimp simp: obj_at_def) 1507 apply (subgoal_tac "ucast (ucast xa + word2) = xa") 1508 apply simp 1509 apply (simp add: is_aligned_nth) 1510 apply (subst word_plus_and_or_coroll) 1511 apply (rule word_eqI) 1512 apply (clarsimp simp: word_size word_bits_def nth_ucast) 1513 apply (drule test_bit_size) 1514 apply (simp add: word_size asid_low_bits_def) 1515 apply (rule word_eqI) 1516 apply (clarsimp simp: word_size word_bits_def nth_ucast) 1517 apply (auto simp: asid_low_bits_def)[1] 1518 apply (rule conjI) 1519 apply (clarsimp simp add: cte_wp_at_caps_of_state) 1520 apply (rename_tac c c') 1521 apply (frule_tac cap=c' in caps_of_state_valid, assumption) 1522 apply (drule (1) diminished_is_update) 1523 apply (clarsimp simp: is_pd_cap_def cap_rights_update_def acap_rights_update_def) 1524 apply (clarsimp simp: word_neq_0_conv) 1525 apply (rule conjI) 1526 apply (subst field_simps, erule is_aligned_add_less_t2n) 1527 apply (simp add: asid_low_bits_def) 1528 apply (rule ucast_less[where 'b=10, simplified], simp) 1529 apply (simp add: asid_low_bits_def asid_bits_def) 1530 apply (simp add: asid_bits_def) 1531 apply (drule vs_lookup_atI) 1532 apply (subst asid_high_bits_of_add_ucast, assumption) 1533 apply assumption 1534 apply (simp add: arch_decode_invocation_def Let_def split_def decode_mmu_invocation_def 1535 cong: if_cong split del: if_split) 1536 apply (rule hoare_pre) 1537 apply ((wp whenE_throwError_wp check_vp_wpR ensure_empty_stronger| 1538 wpc| 1539 simp add: valid_arch_inv_def valid_aci_def is_aligned_shiftl_self)+)[1] 1540 apply (rule_tac Q'= 1541 "\<lambda>rv. real_cte_at rv and 1542 ex_cte_cap_wp_to is_cnode_cap rv and 1543 (\<lambda>s. descendants_of (snd (excaps!0)) (cdt s) = {}) and 1544 cte_wp_at (\<lambda>c. \<exists>idx. c = (cap.UntypedCap False frame pageBits idx)) (snd (excaps!0)) and 1545 (\<lambda>s. arm_asid_table (arch_state s) free = None)" 1546 in hoare_post_imp_R) 1547 apply (simp add: lookup_target_slot_def) 1548 apply wp 1549 apply (clarsimp simp: cte_wp_at_def) 1550 apply (rule conjI, clarsimp) 1551 apply (rule shiftl_less_t2n) 1552 apply (rule order_less_le_trans, rule ucast_less, simp) 1553 apply (simp add: asid_bits_def asid_low_bits_def) 1554 apply (simp add: asid_bits_def) 1555 apply (simp split del: if_split) 1556 apply (wp ensure_no_children_sp select_ext_weak_wp select_wp whenE_throwError_wp|wpc | simp)+ 1557 apply clarsimp 1558 apply (rule conjI, fastforce) 1559 apply (cases excaps, simp) 1560 apply (case_tac list, simp) 1561 apply clarsimp 1562 apply (rule conjI) 1563 apply (drule cte_wp_at_norm, clarsimp, drule cte_wp_valid_cap, fastforce)+ 1564 apply (clarsimp simp add: diminished_def) 1565 apply (rule conjI) 1566 apply clarsimp 1567 apply (simp add: ex_cte_cap_wp_to_def) 1568 apply (rule_tac x=ac in exI) 1569 apply (rule_tac x=ba in exI) 1570 apply (clarsimp simp add: cte_wp_at_caps_of_state) 1571 apply (drule (1) caps_of_state_valid[rotated])+ 1572 apply (drule (1) diminished_is_update)+ 1573 1574 apply (clarsimp simp: is_cap_simps cap_rights_update_def) 1575 apply (clarsimp simp add: cte_wp_at_caps_of_state) 1576 apply (drule (1) caps_of_state_valid[rotated])+ 1577 apply (drule (1) diminished_is_update)+ 1578 apply (clarsimp simp: cap_rights_update_def) 1579 apply (clarsimp simp:diminished_def) 1580 apply (simp add: arch_decode_invocation_def Let_def split_def decode_mmu_invocation_def 1581 cong: if_cong split del: if_split) 1582 apply (cases "invocation_type label = ArchInvocationLabel ARMPageMap") 1583 apply (rename_tac word rights vmpage_size option) 1584 apply (simp split del: if_split) 1585 apply (rule hoare_pre) 1586 apply ((wp whenE_throwError_wp check_vp_wpR hoare_vcg_const_imp_lift_R 1587 create_mapping_entries_parent_for_refs find_pd_for_asid_pd_at_asid 1588 create_mapping_entries_valid_slots create_mapping_entries_same_refs_ex 1589 find_pd_for_asid_lookup_pd_wp 1590 | wpc 1591 | simp add: valid_arch_inv_def valid_page_inv_def is_pg_cap_def)+) 1592 apply (clarsimp simp: neq_Nil_conv) 1593 apply (frule diminished_cte_wp_at_valid_cap[where p="(a, b)" for a b], clarsimp) 1594 apply (frule diminished_cte_wp_at_valid_cap[where p=slot], clarsimp) 1595 apply (clarsimp simp: cte_wp_at_caps_of_state mask_cap_def conj_ac 1596 diminished_def[where cap="ArchObjectCap (PageCap x y z v w)" for x y z v w] 1597 linorder_not_le aligned_sum_less_kernel_base 1598 dest!: diminished_pd_capD) 1599 apply (clarsimp simp: cap_rights_update_def acap_rights_update_def 1600 split: cap.splits arch_cap.splits) 1601 apply (rule conjI, fastforce) 1602 apply (cases slot) 1603 apply (clarsimp simp: valid_cap_simps cap_aligned_def valid_kernel_mappings_def 1604 aligned_sum_less_kernel_base asid_bits_def mask_def 1605 is_arch_update_def cap_master_cap_simps is_arch_cap_def) 1606 apply (rule conjI, fastforce) 1607 apply (rule conjI, fastforce) 1608 apply (rule conjI, fastforce) 1609 apply (rule conjI, fastforce) 1610 apply (rule conjI, fastforce) 1611 apply (rule conjI, fastforce) 1612 apply (rule conjI, fastforce) 1613 apply (rule conjI, fastforce) 1614 apply (rule conjI) 1615 apply (fastforce elim!: is_aligned_weaken intro!: pbfs_atleast_pageBits is_aligned_addrFromPPtr) 1616 apply (rule conjI) 1617 apply (fastforce simp: data_at_def split: if_splits) 1618 apply (rule conjI, fastforce) 1619 apply (rule conjI) 1620 apply (clarsimp simp: vs_cap_ref_def split: vmpage_size.split) 1621 apply (rule conjI, fastforce) 1622 apply (fastforce intro: diminished_pd_self) 1623 apply (cases "invocation_type label = ArchInvocationLabel ARMPageRemap") 1624 apply (rename_tac word rights vmpage_size option) 1625 apply (simp split del: if_split) 1626 apply (rule hoare_pre) 1627 apply ((wp whenE_throwError_wp check_vp_wpR hoare_vcg_const_imp_lift_R 1628 create_mapping_entries_parent_for_refs 1629 find_pd_for_asid_lookup_pd_wp 1630 | wpc 1631 | simp add: valid_arch_inv_def valid_page_inv_def 1632 | (simp add: cte_wp_at_caps_of_state, 1633 wp create_mapping_entries_same_refs_ex hoare_vcg_ex_lift_R))+)[1] 1634 apply (clarsimp simp: valid_cap_def cap_aligned_def neq_Nil_conv) 1635 apply (frule diminished_cte_wp_at_valid_cap[where p="(a, b)" for a b], clarsimp) 1636 apply (clarsimp simp: cte_wp_at_caps_of_state mask_cap_def 1637 diminished_def[where cap="ArchObjectCap (PageCap x y z v w)" for x y z v w]) 1638 apply (clarsimp simp: cap_rights_update_def acap_rights_update_def 1639 split: cap.splits arch_cap.splits) 1640 apply (cases slot) 1641 apply (clarsimp simp: valid_cap_simps cap_aligned_def valid_kernel_mappings_def 1642 aligned_sum_less_kernel_base asid_bits_def mask_def 1643 is_arch_update_def cap_master_cap_simps is_arch_cap_def) 1644 apply (fastforce elim!: is_aligned_weaken 1645 intro!: pbfs_atleast_pageBits is_aligned_addrFromPPtr diminished_pd_self 1646 simp: data_at_def split: if_splits) 1647 apply (cases "invocation_type label = ArchInvocationLabel ARMPageUnmap") 1648 apply (simp split del: if_split) 1649 apply (rule hoare_pre, wp) 1650 apply (clarsimp simp: valid_arch_inv_def valid_page_inv_def) 1651 apply (thin_tac "Ball S P" for S P) 1652 apply (rule conjI) 1653 apply (clarsimp split: option.split) 1654 apply (clarsimp simp: valid_cap_def cap_aligned_def) 1655 apply (simp add: valid_unmap_def) 1656 apply (fastforce simp: vmsz_aligned_def elim: is_aligned_weaken intro!: pbfs_atleast_pageBits) 1657 apply (erule cte_wp_at_weakenE) 1658 apply (clarsimp simp: is_arch_diminished_def is_cap_simps) 1659 apply (cases "isPageFlushLabel (invocation_type label)") 1660 apply (simp split del: if_split) 1661 apply (rule hoare_pre) 1662 apply (wp whenE_throwError_wp static_imp_wp hoare_drop_imps) 1663 apply (simp add: valid_arch_inv_def valid_page_inv_def) 1664 apply (wp find_pd_for_asid_pd_at_asid | wpc)+ 1665 apply (clarsimp simp: valid_cap_def mask_def) 1666 apply (simp split del: if_split) 1667 apply (cases "invocation_type label = ArchInvocationLabel ARMPageGetAddress") 1668 apply (simp split del: if_split) 1669 apply (rule hoare_pre, wp) 1670 apply (clarsimp simp: valid_arch_inv_def valid_page_inv_def) 1671 apply (rule hoare_pre, wp) 1672 apply (simp) 1673 apply (simp add: arch_decode_invocation_def Let_def split_def 1674 is_final_cap_def decode_mmu_invocation_def 1675 cong: if_cong split del: if_split) 1676 apply (rename_tac word option) 1677 apply (rule hoare_pre) 1678 apply ((wp whenE_throwError_wp check_vp_wpR get_master_pde_wp hoare_vcg_all_lift_R| 1679 wpc| 1680 simp add: valid_arch_inv_def valid_pti_def unlessE_whenE vs_cap_ref_def| 1681 rule_tac x="fst p" in hoare_imp_eq_substR| 1682 wp_once hoare_vcg_ex_lift_R)+)[1] 1683 1684 apply (rule_tac Q'="\<lambda>a b. ko_at (ArchObj (PageDirectory pd)) 1685 (a + (args ! 0 >> 21 << 3) && ~~ mask pd_bits) b \<longrightarrow> 1686 pd (ucast (a + (args ! 0 >> 21 << 3) && mask pd_bits >> 3)) = 1687 InvalidPDE \<longrightarrow> L word option p pd a b" for L in hoare_post_imp_R[rotated]) 1688 apply (intro impI) 1689 apply (erule impE) 1690 apply (clarsimp simp: pageBits_def pde_bits_def pt_bits_def) 1691 apply (erule impE) 1692 apply (clarsimp simp: pageBits_def pde_bits_def pt_bits_def split:pde.splits) 1693 apply assumption 1694 apply ((wp whenE_throwError_wp hoare_vcg_all_lift_R 1695 find_pd_for_asid_lookup_slot [unfolded lookup_pd_slot_def Let_def] 1696 find_pd_for_asid_ref_offset_voodoo find_pd_for_asid_shifting_voodoo 1697 find_pd_for_asid_inv 1698 | wpc 1699 | simp add: valid_arch_inv_def valid_pti_def unlessE_whenE empty_pde_atI 1700 vs_cap_ref_def pageBits_def pt_bits_def pde_bits_def 1701 | wp_once hoare_drop_imps hoare_vcg_ex_lift_R)+)[6] 1702 apply (clarsimp simp: is_cap_simps if_apply_def2) 1703 apply (rule conjI) 1704 apply clarsimp 1705 apply (rule conjI, fastforce) 1706 apply (rule conjI, fastforce) 1707 apply (clarsimp simp: neq_Nil_conv) 1708 apply (thin_tac "Ball S P" for S P) 1709 apply (rule conjI) 1710 apply (clarsimp simp: valid_cap_def cap_aligned_def) 1711 apply (rule conjI) 1712 apply (drule cte_wp_at_norm, clarsimp, drule cte_wp_valid_cap, fastforce)+ 1713 apply (drule (1) diminished_is_update[rotated])+ 1714 apply (clarsimp simp add: cap_rights_update_def acap_rights_update_def) 1715 apply (clarsimp simp: valid_cap_def cap_aligned_def 1716 pt_bits_def pageBits_def 1717 linorder_not_le 1718 order_le_less_trans[OF word_and_le2]) 1719 apply (rule conjI) 1720 apply (clarsimp simp add: cte_wp_at_caps_of_state) 1721 apply (drule (1) caps_of_state_valid[rotated]) 1722 apply (drule (1) diminished_is_update) 1723 apply clarsimp 1724 apply (clarsimp simp: cap_master_cap_def is_arch_update_def) 1725 apply (clarsimp simp: cap_asid_def cap_rights_update_def acap_rights_update_def is_cap_simps 1726 split: option.split) 1727 apply (rule conjI, fastforce) 1728 apply (rule conjI, fastforce) 1729 apply (clarsimp simp: pde_ref_def) 1730 apply (frule invs_pd_caps) 1731 apply (clarsimp simp: cte_wp_at_caps_of_state) 1732 apply (frule (1) caps_of_state_valid[rotated]) 1733 apply (drule (1) diminished_is_update) 1734 apply (clarsimp simp: cap_rights_update_def acap_rights_update_def valid_cap_def) 1735 apply (drule (2) valid_table_caps_ptD) 1736 apply (rule conjI, fastforce)+ 1737 apply (clarsimp simp: kernel_vsrefs_def) 1738 apply fastforce 1739 apply (clarsimp simp: cte_wp_at_def is_arch_diminished_def is_cap_simps 1740 valid_arch_inv_def valid_pti_def) 1741 apply (simp add: arch_decode_invocation_def Let_def decode_mmu_invocation_def split del: if_split) 1742 apply (cases "isPDFlushLabel (invocation_type label)") 1743 apply (simp split del: if_split) 1744 apply (rule hoare_pre) 1745 apply (wp whenE_throwError_wp static_imp_wp hoare_drop_imp | wpc | simp)+ 1746 apply (simp add: resolve_vaddr_def) 1747 apply (wp get_master_pte_wp get_master_pde_wp whenE_throwError_wp | wpc | simp)+ 1748 apply (clarsimp simp: valid_arch_inv_def valid_pdi_def)+ 1749 apply (rule_tac Q'="\<lambda>pd' s. vspace_at_asid x2 pd' s \<and> x2 \<le> mask asid_bits \<and> x2 \<noteq> 0" in hoare_post_imp_R) 1750 apply wp 1751 apply clarsimp 1752 apply (wp | wpc)+ 1753 apply (clarsimp simp: valid_cap_def mask_def) 1754 apply (clarsimp, wp throwError_validE_R) 1755 1756 (* VCPU *) 1757 apply (rename_tac vcpu_ptr) 1758 apply (clarsimp simp: arch_decode_invocation_def decode_vcpu_invocation_def) 1759 apply (cases "invocation_type label"; (simp, wp?)) 1760 apply (rename_tac arch_iv) 1761 apply (case_tac "arch_iv"; (simp, wp?)) 1762 apply (simp add: decode_vcpu_set_tcb_def) 1763 apply (rule hoare_pre, wpsimp) 1764 apply (clarsimp simp: valid_arch_inv_def valid_vcpu_invocation_def) 1765 apply (rename_tac tcb_ptr) 1766 apply (frule_tac c="ThreadCap tcb_ptr" in diminished_cte_wp_at_valid_cap, fastforce) 1767 apply (simp add: valid_cap_def) 1768 apply (cases slot) 1769 apply (clarsimp simp: ex_nonz_cap_to_def) 1770 apply (rule conjI, fastforce elim: cte_wp_at_weakenE) 1771 apply (rule conjI, fastforce elim: cte_wp_at_weakenE) 1772 apply (clarsimp dest!: invs_valid_global_refs simp: cte_wp_at_caps_of_state) 1773 apply (drule_tac ?cap="ThreadCap (idle_thread s)" in valid_global_refsD2, assumption) 1774 apply (simp add:global_refs_def cap_range_def) 1775 apply (simp add: decode_vcpu_inject_irq_def) 1776 apply (rule hoare_pre, wpsimp simp: whenE_def wp: get_vcpu_wp) 1777 apply (clarsimp simp: valid_arch_inv_def valid_vcpu_invocation_def obj_at_def) 1778 apply (simp add: decode_vcpu_read_register_def) 1779 apply (rule hoare_pre, wpsimp) 1780 apply (clarsimp simp: valid_arch_inv_def valid_cap_def valid_vcpu_invocation_def) 1781 apply (simp add: decode_vcpu_write_register_def) 1782 apply (rule hoare_pre, wpsimp) 1783 apply (clarsimp simp: valid_arch_inv_def valid_cap_def valid_vcpu_invocation_def) 1784 done 1785 1786 1787declare word_less_sub_le [simp] 1788 1789crunches associate_vcpu_tcb 1790 for pred_tcb_at[wp_unsafe]: "pred_tcb_at proj P t" 1791 (wp: crunch_wps simp: crunch_simps) 1792 1793crunches vcpu_read_reg, vcpu_write_reg, invoke_vcpu_inject_irq 1794 for pred_tcb_at[wp]: "pred_tcb_at proj P t" 1795 1796lemma perform_vcpu_invocation_pred_tcb_at[wp_unsafe]: 1797 "\<lbrace>pred_tcb_at proj P t and K (proj_not_field proj tcb_arch_update)\<rbrace> 1798 perform_vcpu_invocation iv 1799 \<lbrace>\<lambda>_. pred_tcb_at proj P t\<rbrace>" 1800 apply (simp add: perform_vcpu_invocation_def) 1801 apply (rule hoare_pre) 1802 apply (wp associate_vcpu_tcb_pred_tcb_at | wpc 1803 | clarsimp simp: invoke_vcpu_read_register_def 1804 read_vcpu_register_def 1805 invoke_vcpu_write_register_def 1806 write_vcpu_register_def)+ 1807 done 1808 1809crunch pred_tcb_at: perform_page_table_invocation, perform_page_invocation, 1810 perform_asid_pool_invocation, 1811 perform_page_directory_invocation "pred_tcb_at proj P t" 1812 (wp: crunch_wps simp: crunch_simps) 1813 1814 1815lemma arch_pinv_st_tcb_at: 1816 "\<lbrace>invs and valid_arch_inv ai and ct_active and 1817 st_tcb_at (P and (Not \<circ> inactive) and (Not \<circ> idle)) t\<rbrace> 1818 arch_perform_invocation ai 1819 \<lbrace>\<lambda>rv. st_tcb_at P t\<rbrace>" 1820 apply (cases ai, simp_all add: arch_perform_invocation_def valid_arch_inv_def) 1821 apply (wp perform_page_table_invocation_pred_tcb_at, 1822 fastforce elim!: pred_tcb_weakenE) 1823 apply (wp perform_page_directory_invocation_pred_tcb_at, fastforce elim: pred_tcb_weakenE) 1824 apply (wp perform_page_invocation_pred_tcb_at, fastforce elim!: pred_tcb_weakenE) 1825 apply (wp perform_asid_control_invocation_st_tcb_at, 1826 fastforce elim!: pred_tcb_weakenE) 1827 apply (wp perform_asid_pool_invocation_pred_tcb_at, 1828 fastforce elim!: pred_tcb_weakenE) 1829 apply (wp perform_vcpu_invocation_pred_tcb_at, 1830 fastforce elim!: pred_tcb_weakenE) 1831 done 1832 1833 1834lemma get_cap_diminished: 1835 "\<lbrace>valid_objs\<rbrace> get_cap slot \<lbrace>\<lambda>cap. cte_wp_at (diminished cap) slot\<rbrace>" 1836 apply (wp get_cap_wp) 1837 apply (intro allI impI) 1838 apply (simp add: cte_wp_at_caps_of_state diminished_def) 1839 apply (frule (1) caps_of_state_valid_cap) 1840 apply (clarsimp simp add: valid_cap_def2 wellformed_cap_def mask_cap_def 1841 cap_rights_update_def acap_rights_update_def 1842 split: cap.splits arch_cap.splits) 1843 apply fastforce+ 1844 apply (clarsimp simp add: wellformed_acap_def 1845 split: cap.splits arch_cap.splits) 1846 apply (rename_tac rights vmpage_size option) 1847 apply (rule_tac x=rights in exI) 1848 apply auto 1849 done 1850 1851end 1852 1853 1854context begin interpretation Arch . 1855 1856requalify_consts 1857 valid_arch_inv 1858 1859requalify_facts 1860 invoke_arch_tcb 1861 invoke_arch_invs 1862 sts_valid_arch_inv 1863 arch_decode_inv_wf 1864 arch_pinv_st_tcb_at 1865 get_cap_diminished 1866 1867end 1868 1869declare invoke_arch_invs[wp] 1870declare arch_decode_inv_wf[wp] 1871 1872 1873end 1874