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 11(* 12ARM-specific VSpace invariants 13*) 14 15theory ArchVSpace_AI 16imports "../VSpacePre_AI" 17begin 18 19context Arch begin global_naming ARM 20 21lemma kernel_base_shift_cast_le: 22 fixes x :: "12 word" 23 shows 24 "(kernel_base >> 20 \<le> ucast x) = 25 (ucast (kernel_base >> 20) \<le> x)" 26 apply (simp add: word_le_def) 27 apply (subst uint_ucast, simp, 28 simp add: kernel_base_def) 29 apply (simp add: ucast_def) 30 apply (subst word_uint.Abs_inverse) 31 apply (cut_tac x=x in word_uint.Rep) 32 apply (simp add: uints_num) 33 apply simp 34 done 35 36(* FIXME: move to Invariant_AI *) 37definition 38 glob_vs_refs_arch :: "arch_kernel_obj \<Rightarrow> (vs_ref \<times> obj_ref) set" 39 where "glob_vs_refs_arch \<equiv> \<lambda>ko. case ko of 40 (ASIDPool pool) \<Rightarrow> 41 (\<lambda>(r,p). (VSRef (ucast r) (Some AASIDPool), p)) ` graph_of pool 42 | (PageDirectory pd) \<Rightarrow> 43 (\<lambda>(r,p). (VSRef (ucast r) (Some APageDirectory), p)) 44 ` graph_of (pde_ref o pd) 45 | _ \<Rightarrow> {}" 46 47declare glob_vs_refs_arch_def[simp] 48 49definition 50 "glob_vs_refs \<equiv> arch_obj_fun_lift glob_vs_refs_arch {}" 51 52crunch pspace_in_kernel_window[wp]: perform_page_invocation "pspace_in_kernel_window" 53 (simp: crunch_simps wp: crunch_wps) 54 55definition 56 "pd_at_uniq asid pd \<equiv> \<lambda>s. pd \<notin> ran ((option_map snd o arm_asid_map (arch_state s) |` (- {asid})))" 57 58 59crunch inv[wp]: find_pd_for_asid_assert "P" 60 (simp: crunch_simps) 61 62lemma asid_word_bits [simp]: "asid_bits < word_bits" 63 by (simp add: asid_bits_def word_bits_def) 64 65 66lemma asid_low_high_bits: 67 "\<lbrakk> x && mask asid_low_bits = y && mask asid_low_bits; 68 ucast (asid_high_bits_of x) = (ucast (asid_high_bits_of y)::word32); 69 x \<le> 2 ^ asid_bits - 1; y \<le> 2 ^ asid_bits - 1 \<rbrakk> 70 \<Longrightarrow> x = y" 71 apply (rule word_eqI) 72 apply (simp add: upper_bits_unset_is_l2p_32 [symmetric] bang_eq nth_ucast word_size) 73 apply (clarsimp simp: asid_high_bits_of_def nth_ucast nth_shiftr) 74 apply (simp add: asid_high_bits_def asid_bits_def asid_low_bits_def word_bits_def) 75 subgoal premises prems[rule_format] for n 76 apply (cases "n < 10") 77 using prems(1) 78 apply fastforce 79 apply (cases "n < 17") 80 using prems(2)[where n="n - 10"] 81 apply fastforce 82 using prems(3-) 83 by (simp add: linorder_not_less) 84 done 85 86lemma asid_low_high_bits': 87 "\<lbrakk> ucast x = (ucast y :: 10 word); 88 asid_high_bits_of x = asid_high_bits_of y; 89 x \<le> 2 ^ asid_bits - 1; y \<le> 2 ^ asid_bits - 1 \<rbrakk> 90 \<Longrightarrow> x = y" 91 apply (rule asid_low_high_bits) 92 apply (rule word_eqI) 93 apply (subst (asm) bang_eq) 94 apply (simp add: nth_ucast asid_low_bits_def word_size) 95 apply (rule word_eqI) 96 apply (subst (asm) bang_eq)+ 97 apply (simp add: nth_ucast asid_low_bits_def) 98 apply assumption+ 99 done 100 101lemma table_cap_ref_at_eq: 102 "table_cap_ref c = Some [x] \<longleftrightarrow> vs_cap_ref c = Some [x]" 103 by (auto simp: table_cap_ref_def vs_cap_ref_simps vs_cap_ref_def 104 split: cap.splits arch_cap.splits vmpage_size.splits option.splits) 105 106 107lemma table_cap_ref_ap_eq: 108 "table_cap_ref c = Some [x,y] \<longleftrightarrow> vs_cap_ref c = Some [x,y]" 109 by (auto simp: table_cap_ref_def vs_cap_ref_simps vs_cap_ref_def 110 split: cap.splits arch_cap.splits vmpage_size.splits option.splits) 111 112lemma pd_at_asid_unique: 113 "\<lbrakk> vspace_at_asid asid pd s; vspace_at_asid asid' pd s; 114 unique_table_refs (caps_of_state s); 115 valid_vs_lookup s; valid_vspace_objs s; valid_global_objs s; 116 valid_arch_state s; asid < 2 ^ asid_bits; asid' < 2 ^ asid_bits \<rbrakk> 117 \<Longrightarrow> asid = asid'" 118 apply (clarsimp simp: vspace_at_asid_def) 119 apply (drule(1) valid_vs_lookupD[OF vs_lookup_pages_vs_lookupI])+ 120 apply (clarsimp simp: table_cap_ref_ap_eq[symmetric]) 121 apply (clarsimp simp: table_cap_ref_def 122 split: cap.split_asm arch_cap.split_asm option.split_asm) 123 apply (drule(2) unique_table_refsD, 124 simp+, clarsimp simp: table_cap_ref_def, 125 erule(1) asid_low_high_bits) 126 apply simp+ 127 done 128 129lemma pd_at_asid_unique2: 130 "\<lbrakk> vspace_at_asid asid pd s; vspace_at_asid asid pd' s \<rbrakk> 131 \<Longrightarrow> pd = pd'" 132 apply (clarsimp simp: vspace_at_asid_def vs_asid_refs_def 133 dest!: graph_ofD vs_lookup_2ConsD vs_lookup_atD 134 vs_lookup1D) 135 apply (clarsimp simp: obj_at_def vs_refs_def 136 split: Structures_A.kernel_object.splits 137 arch_kernel_obj.splits 138 dest!: graph_ofD) 139 apply (drule ucast_up_inj, simp+) 140 done 141 142 143lemma pd_at_asid_uniq: 144 "\<lbrakk> vspace_at_asid asid pd s; asid \<le> mask asid_bits; valid_asid_map s; 145 unique_table_refs (caps_of_state s); valid_vs_lookup s; 146 valid_vspace_objs s; valid_global_objs s; valid_arch_state s \<rbrakk> 147 \<Longrightarrow> pd_at_uniq asid pd s" 148 apply (clarsimp simp: pd_at_uniq_def ran_option_map 149 dest!: ran_restrictD) 150 apply (clarsimp simp: valid_asid_map_def) 151 apply (drule bspec, erule graph_ofI) 152 apply clarsimp 153 apply (rule pd_at_asid_unique, assumption+) 154 apply (drule subsetD, erule domI) 155 apply (simp add: mask_def) 156 apply (simp add: mask_def) 157 done 158 159 160lemma find_free_hw_asid_valid_arch [wp]: 161 "\<lbrace>valid_arch_state\<rbrace> find_free_hw_asid \<lbrace>\<lambda>_. valid_arch_state\<rbrace>" 162 apply (simp add: find_free_hw_asid_def invalidate_hw_asid_entry_def 163 invalidate_asid_def do_machine_op_def split_def 164 cong: option.case_cong) 165 apply (wp|wpc|simp)+ 166 apply (clarsimp simp: valid_arch_state_def) 167 apply (frule is_inv_inj) 168 apply (drule findNoneD) 169 apply (drule_tac x="arm_next_asid (arch_state s)" in bspec) 170 apply (simp add: minBound_word) 171 apply (clarsimp simp: is_inv_def ran_upd dom_option_map 172 dom_upd) 173 apply (drule_tac x="x" and y="arm_next_asid (arch_state s)" in inj_onD) 174 apply simp 175 apply blast 176 apply blast 177 apply simp 178 done 179 180 181lemma valid_vs_lookupE: 182 "\<lbrakk> valid_vs_lookup s; \<And>ref p. (ref \<unrhd> p) s' \<Longrightarrow> (ref \<unrhd> p) s; 183 set (arm_global_pts (arch_state s)) \<subseteq> set (arm_global_pts (arch_state s')); 184 caps_of_state s = caps_of_state s' \<rbrakk> 185 \<Longrightarrow> valid_vs_lookup s'" 186 by (simp add: valid_vs_lookup_def, blast) 187 188 189lemma find_free_hw_asid_vspace_objs [wp]: 190 "\<lbrace>valid_vspace_objs\<rbrace> find_free_hw_asid \<lbrace>\<lambda>asid. valid_vspace_objs\<rbrace>" 191 apply (simp add: find_free_hw_asid_def invalidate_hw_asid_entry_def invalidate_asid_def 192 do_machine_op_def split_def 193 cong: option.case_cong) 194 apply (wp|wpc)+ 195 apply (simp add: valid_vspace_objs_arch_update) 196 done 197 198lemma find_free_hw_asid_pd_at_asid [wp]: 199 "\<lbrace>vspace_at_asid pd asid\<rbrace> find_free_hw_asid \<lbrace>\<lambda>_. vspace_at_asid pd asid\<rbrace>" 200 apply (simp add: find_free_hw_asid_def invalidate_hw_asid_entry_def invalidate_asid_def 201 do_machine_op_def split_def 202 cong: option.case_cong) 203 apply (wp|wpc)+ 204 apply (clarsimp simp: vspace_at_asid_def vs_lookup_arch_update) 205 done 206 207 208lemma find_free_hw_asid_pd_at_uniq [wp]: 209 "\<lbrace>pd_at_uniq pd asid\<rbrace> find_free_hw_asid \<lbrace>\<lambda>_. pd_at_uniq pd asid\<rbrace>" 210 apply (simp add: find_free_hw_asid_def invalidate_hw_asid_entry_def invalidate_asid_def 211 do_machine_op_def split_def 212 cong: option.case_cong) 213 apply (wp|wpc)+ 214 apply (clarsimp simp: pd_at_uniq_def ran_option_map 215 dest!: ran_restrictD split: if_split_asm) 216 apply (rule ccontr, erule notE, rule image_eqI[rotated], 217 rule ranI) 218 apply (fastforce simp add: restrict_map_def) 219 apply simp 220 done 221 222 223lemma load_hw_asid_wp: 224 "\<lbrace>\<lambda>s. P (option_map fst (arm_asid_map (arch_state s) asid)) s\<rbrace> 225 load_hw_asid asid \<lbrace>P\<rbrace>" 226 apply (simp add: load_hw_asid_def) 227 apply wp 228 apply simp 229 done 230 231 232crunch aligned [wp]: find_free_hw_asid pspace_aligned 233 234crunch "distinct" [wp]: find_free_hw_asid pspace_distinct 235 236 237lemma invalidate_hw_asid_entry_asid_map [wp]: 238 "\<lbrace>valid_asid_map\<rbrace> invalidate_hw_asid_entry asid \<lbrace>\<lambda>_. valid_asid_map\<rbrace>" 239 apply (simp add: invalidate_hw_asid_entry_def) 240 apply wp 241 apply (simp add: valid_asid_map_def vspace_at_asid_def) 242 done 243 244 245lemma invalidate_asid_asid_map [wp]: 246 "\<lbrace>valid_asid_map\<rbrace> invalidate_asid asid \<lbrace>\<lambda>_. valid_asid_map\<rbrace>" 247 apply (simp add: invalidate_asid_def) 248 apply wp 249 apply (auto simp add: valid_asid_map_def vspace_at_asid_def graph_of_def split: if_split_asm) 250 done 251 252 253lemma find_free_hw_asid_asid_map [wp]: 254 "\<lbrace>valid_asid_map\<rbrace> find_free_hw_asid \<lbrace>\<lambda>_. valid_asid_map\<rbrace>" 255 apply (simp add: find_free_hw_asid_def) 256 apply (rule hoare_pre) 257 apply (wp|wpc|simp)+ 258 done 259 260 261lemma dmo_pd_at_asid [wp]: 262 "\<lbrace>vspace_at_asid a pd\<rbrace> do_machine_op f \<lbrace>\<lambda>_. vspace_at_asid a pd\<rbrace>" 263 apply (simp add: do_machine_op_def split_def) 264 apply wp 265 apply (simp add: vspace_at_asid_def) 266 done 267 268 269crunch inv: find_pd_for_asid "P" 270 (simp: assertE_def crunch_simps wp: crunch_wps) 271 272 273lemma find_pd_for_asid_pd_at_asid [wp]: 274 "\<lbrace>\<top>\<rbrace> find_pd_for_asid asid \<lbrace>\<lambda>pd. vspace_at_asid asid pd\<rbrace>, -" 275 apply (simp add: find_pd_for_asid_def assertE_def split del: if_split) 276 apply (rule hoare_pre) 277 apply (wp|wpc)+ 278 apply (clarsimp simp: vspace_at_asid_def) 279 apply (rule vs_lookupI) 280 apply (simp add: vs_asid_refs_def graph_of_def) 281 apply fastforce 282 apply (rule r_into_rtrancl) 283 apply (erule vs_lookup1I) 284 prefer 2 285 apply (rule refl) 286 apply (simp add: vs_refs_def graph_of_def mask_asid_low_bits_ucast_ucast) 287 apply fastforce 288 done 289 290crunch valid_vs_lookup[wp]: do_machine_op "valid_vs_lookup" 291 292lemma valid_asid_mapD: 293 "\<lbrakk> arm_asid_map (arch_state s) asid = Some (vasid, pd); valid_asid_map s \<rbrakk> 294 \<Longrightarrow> vspace_at_asid asid pd s \<and> asid \<le> mask asid_bits" 295 by (auto simp add: valid_asid_map_def graph_of_def) 296 297 298lemma page_directory_cap_pd_at_uniq: 299 "\<lbrakk> cte_wp_at ((=) (cap.ArchObjectCap (arch_cap.PageDirectoryCap pd (Some asid)))) slot s; 300 valid_asid_map s; valid_vs_lookup s; unique_table_refs (caps_of_state s); 301 valid_arch_state s; valid_global_objs s; valid_objs s \<rbrakk> 302 \<Longrightarrow> pd_at_uniq asid pd s" 303 apply (frule(1) cte_wp_at_valid_objs_valid_cap) 304 apply (clarsimp simp: pd_at_uniq_def restrict_map_def valid_cap_def 305 elim!: ranE split: if_split_asm) 306 apply (drule(1) valid_asid_mapD) 307 apply (clarsimp simp: vspace_at_asid_def) 308 apply (frule(1) valid_vs_lookupD[OF vs_lookup_pages_vs_lookupI]) 309 apply (clarsimp simp: cte_wp_at_caps_of_state dest!: obj_ref_elemD) 310 apply (drule(1) unique_table_refsD[rotated, where cps="caps_of_state s"], 311 simp+) 312 apply (clarsimp simp: table_cap_ref_ap_eq[symmetric] table_cap_ref_def 313 split: cap.splits arch_cap.splits option.splits) 314 apply (drule(1) asid_low_high_bits, simp_all add: mask_def) 315 done 316 317lemma invalidateLocalTLB_ASID_underlying_memory: 318 "\<lbrace>\<lambda>m'. underlying_memory m' p = um\<rbrace> 319 invalidateLocalTLB_ASID asid 320 \<lbrace>\<lambda>_ m'. underlying_memory m' p = um\<rbrace>" 321 by (clarsimp simp: invalidateLocalTLB_ASID_def machine_op_lift_def 322 machine_rest_lift_def split_def | wp)+ 323 324lemma isb_underlying_memory[wp]: 325 "\<lbrace>\<lambda>m'. underlying_memory m' p = um\<rbrace> 326 isb 327 \<lbrace>\<lambda>_ m'. underlying_memory m' p = um\<rbrace>" 328 by (clarsimp simp: isb_def machine_op_lift_def 329 machine_rest_lift_def split_def | wp)+ 330 331lemma dsb_underlying_memory[wp]: 332 "\<lbrace>\<lambda>m'. underlying_memory m' p = um\<rbrace> 333 dsb 334 \<lbrace>\<lambda>_ m'. underlying_memory m' p = um\<rbrace>" 335 by (clarsimp simp: dsb_def machine_op_lift_def 336 machine_rest_lift_def split_def | wp)+ 337 338lemma dmb_underlying_memory[wp]: 339 "\<lbrace>\<lambda>m'. underlying_memory m' p = um\<rbrace> 340 dmb 341 \<lbrace>\<lambda>_ m'. underlying_memory m' p = um\<rbrace>" 342 by (clarsimp simp: dmb_def machine_op_lift_def 343 machine_rest_lift_def split_def | wp)+ 344 345lemma invalidateLocalTLB_underlying_memory: 346 "\<lbrace>\<lambda>m'. underlying_memory m' p = um\<rbrace> 347 invalidateLocalTLB 348 \<lbrace>\<lambda>_ m'. underlying_memory m' p = um\<rbrace>" 349 by (clarsimp simp: invalidateLocalTLB_def machine_op_lift_def 350 machine_rest_lift_def split_def | wp)+ 351 352lemmas invalidateLocalTLB_ASID_irq_masks = no_irq[OF no_irq_invalidateLocalTLB_ASID] 353 354lemma dmo_invalidateLocalTLB_ASID_invs[wp]: 355 "\<lbrace>invs\<rbrace> do_machine_op (invalidateLocalTLB_ASID asid) \<lbrace>\<lambda>_. invs\<rbrace>" 356 apply (wp dmo_invs) 357 apply safe 358 apply (drule use_valid) 359 apply (rule invalidateLocalTLB_ASID_underlying_memory) 360 apply fastforce+ 361 apply(erule (1) use_valid[OF _ invalidateLocalTLB_ASID_irq_masks]) 362 done 363 364lemma load_hw_asid_invs[wp]: "\<lbrace>invs\<rbrace> load_hw_asid asid \<lbrace>\<lambda>y. invs\<rbrace>" 365 by (simp add: load_hw_asid_def) wp 366 367lemma invalidate_tlb_by_asid_invs[wp]: 368 "\<lbrace>invs\<rbrace> invalidate_tlb_by_asid asid \<lbrace>\<lambda>_. invs\<rbrace>" 369 apply (clarsimp simp: invalidate_tlb_by_asid_def | wp | wpc)+ 370 apply (rule_tac Q="K invs" in hoare_post_imp) 371 apply (clarsimp|wp load_hw_asid_invs)+ 372 done 373 374crunch typ_at [wp]: flush_space "\<lambda>s. P (typ_at T p s)" 375 376 377lemmas flush_space_typ_ats [wp] = abs_typ_at_lifts [OF flush_space_typ_at] 378 379crunch cur_tcb [wp]: flush_space cur_tcb 380 381crunch valid_arch [wp]: flush_space valid_arch_state 382 383crunch valid_objs [wp]: flush_space valid_objs 384 385 386lemma invalidate_hw_asid_vspace_objs [wp]: 387 "\<lbrace>valid_vspace_objs\<rbrace> invalidate_hw_asid_entry asid \<lbrace>\<lambda>_. valid_vspace_objs\<rbrace>" 388 apply (simp add: invalidate_hw_asid_entry_def) 389 apply wp 390 apply (simp add: valid_vspace_objs_arch_update) 391 done 392 393 394lemma invalidate_hw_asid_entry_pd_at_asid_uniq[wp]: 395 "\<lbrace>vspace_at_asid asid pd\<rbrace> 396 invalidate_hw_asid_entry y 397 \<lbrace>\<lambda>rv. vspace_at_asid asid pd\<rbrace>" 398 "\<lbrace>pd_at_uniq asid pd\<rbrace> 399 invalidate_hw_asid_entry y 400 \<lbrace>\<lambda>rv. pd_at_uniq asid pd\<rbrace>" 401 by (simp add: vspace_at_asid_def pd_at_uniq_def 402 invalidate_hw_asid_entry_def 403 | wp)+ 404 405 406lemma invalidate_hw_asid_entry_pd_still_uniq[wp]: 407 "\<lbrace>\<lambda>s. \<forall>pd. vspace_at_asid asid pd s \<longrightarrow> pd_at_uniq asid pd s\<rbrace> 408 invalidate_hw_asid_entry y 409 \<lbrace>\<lambda>rv s. \<forall>pd. vspace_at_asid asid pd s \<longrightarrow> pd_at_uniq asid pd s\<rbrace>" 410 (* this could be generalised to other functions on pd_at_* *) 411 apply (simp add: vspace_at_asid_def pd_at_uniq_def 412 invalidate_hw_asid_entry_def) 413 apply (wp | simp)+ 414 done 415 416lemma invalidate_asid_entry_arch_state [wp]: 417 "\<lbrace>valid_arch_state\<rbrace> invalidate_asid_entry asid \<lbrace>\<lambda>_. valid_arch_state\<rbrace>" 418 apply (simp add: invalidate_asid_entry_def invalidate_asid_def invalidate_hw_asid_entry_def) 419 apply (wp load_hw_asid_wp) 420 apply (clarsimp simp: valid_arch_state_def simp del: fun_upd_apply) 421 apply (rule conjI) 422 apply (clarsimp simp: is_inv_None_upd comp_upd_simp) 423 apply (simp add: None_upd_eq comp_upd_simp) 424 done 425 426 427lemma flush_space_asid_map[wp]: 428 "\<lbrace>valid_asid_map\<rbrace> flush_space space \<lbrace>\<lambda>rv. valid_asid_map\<rbrace>" 429 apply (simp add: flush_space_def) 430 apply (wp load_hw_asid_wp | wpc | simp | rule_tac Q="\<lambda>_. valid_asid_map" in hoare_strengthen_post)+ 431 done 432 433 434lemma flush_space_arch_objs[wp]: 435 "\<lbrace>valid_vspace_objs\<rbrace> flush_space space \<lbrace>\<lambda>rv. valid_vspace_objs\<rbrace>" 436 apply (simp add: flush_space_def) 437 apply (wp load_hw_asid_wp | wpc | simp | rule_tac Q="\<lambda>_. valid_vspace_objs" in hoare_strengthen_post)+ 438 done 439 440 441crunch typ_at [wp]: invalidate_asid_entry "\<lambda>s. P (typ_at T p s)" 442 443 444lemmas invalidate_asid_entry_typ_ats [wp] = 445 abs_typ_at_lifts [OF invalidate_asid_entry_typ_at] 446 447 448crunch cur [wp]: invalidate_asid_entry cur_tcb 449 450 451crunch valid_objs [wp]: invalidate_asid_entry valid_objs 452 453 454lemma invalidate_asid_entry_asid_map [wp]: 455 "\<lbrace>valid_asid_map\<rbrace> invalidate_asid_entry asid \<lbrace>\<lambda>_. valid_asid_map\<rbrace>" 456 apply (simp add: invalidate_asid_entry_def invalidate_asid_def invalidate_hw_asid_entry_def) 457 apply (wp load_hw_asid_wp) 458 apply (clarsimp simp: valid_asid_map_def simp del: fun_upd_apply) 459 apply (clarsimp simp: vspace_at_asid_def vs_lookup_arch_update) 460 apply blast 461 done 462 463 464crunch obj_at [wp]: invalidate_asid_entry "\<lambda>s. P (obj_at Q p s)" 465 466 467 468lemma invalidate_asid_entry_invalidates: 469 "\<lbrace>valid_asid_map and valid_arch_state and K (asid \<le> mask asid_bits) and 470 (\<lambda>s. arm_asid_table (arch_state s) (asid_high_bits_of asid) = Some ap)\<rbrace> 471 invalidate_asid_entry asid 472 \<lbrace>\<lambda>rv s. \<forall>asida. asida \<le> mask asid_bits \<longrightarrow> 473 ucast asida = (ucast asid :: 10 word) \<longrightarrow> 474 arm_asid_table (arch_state s) (asid_high_bits_of asida) = 475 Some ap \<longrightarrow> 476 arm_asid_map (arch_state s) asida = None\<rbrace>" 477 apply (simp add: invalidate_asid_entry_def invalidate_asid_def invalidate_hw_asid_entry_def) 478 apply (wp load_hw_asid_wp) 479 apply clarsimp 480 apply (rule drop_imp) 481 apply (clarsimp simp: valid_arch_state_def valid_asid_table_def) 482 apply (drule_tac x="asid_high_bits_of asid" and y="asid_high_bits_of asida" in inj_onD) 483 apply simp 484 apply blast 485 apply blast 486 apply clarsimp 487 apply (drule asid_low_high_bits', simp) 488 apply (fastforce simp: mask_def) 489 apply (fastforce simp: mask_def) 490 apply (erule (1) notE) 491 done 492 493 494crunch vspace_objs [wp]: invalidate_asid_entry valid_vspace_objs 495 (simp: valid_vspace_objs_arch_update) 496 497 498lemma flush_space_pd_at_asid [wp]: 499 "\<lbrace>vspace_at_asid a pd\<rbrace> flush_space asid \<lbrace>\<lambda>_. vspace_at_asid a pd\<rbrace>" 500 apply (simp add: flush_space_def) 501 apply (wp load_hw_asid_wp|wpc|rule_tac Q="\<lambda>_. vspace_at_asid a pd" in hoare_strengthen_post|simp)+ 502 done 503 504 505crunch obj_at [wp]: flush_space "\<lambda>s. P (obj_at Q p s)" 506 507 508lemma flush_space_arch [wp]: 509 "\<lbrace>\<lambda>s. P (arch_state s)\<rbrace> flush_space asid \<lbrace>\<lambda>rv s. P (arch_state s)\<rbrace>" 510 apply (simp add: flush_space_def) 511 apply (wp load_hw_asid_wp|wpc)+ 512 apply simp 513 done 514 515 516crunch aligned [wp]: invalidate_asid_entry pspace_aligned 517 518crunch "distinct" [wp]: invalidate_asid_entry pspace_distinct 519 520crunch aligned [wp]: flush_space pspace_aligned 521 522crunch "distinct" [wp]: flush_space pspace_distinct 523 524 525crunch caps_of_state[wp]: invalidate_asid_entry "\<lambda>s. P (caps_of_state s)" 526 527 528lemma pd_at_asid_arch_up': 529 "arm_asid_table (f (arch_state s)) = arm_asid_table (arch_state s) 530 \<Longrightarrow> vspace_at_asid asid pd (arch_state_update f s) = vspace_at_asid asid pd s" 531 by (clarsimp simp add: vspace_at_asid_def vs_lookup_def vs_lookup1_def) 532 533 534lemma pd_at_asid_arch_up: 535 "vspace_at_asid asid pd (s\<lparr>arch_state := arch_state s \<lparr>arm_asid_map := a, arm_hwasid_table := b\<rparr>\<rparr>) = 536 vspace_at_asid asid pd s" 537 by (simp add: pd_at_asid_arch_up') 538 539 540lemma invalidate_asid_entry_invs [wp]: 541 "\<lbrace>invs\<rbrace> invalidate_asid_entry asid \<lbrace>\<lambda>_. invs\<rbrace>" 542 apply (simp add: invalidate_asid_entry_def invalidate_asid_def 543 invalidate_hw_asid_entry_def) 544 apply (rule hoare_pre, wp load_hw_asid_wp) 545 apply (clarsimp simp del: fun_upd_apply) 546 apply (clarsimp simp: invs_def valid_state_def valid_irq_node_def 547 valid_arch_caps_def valid_table_caps_def 548 valid_kernel_mappings_def valid_global_objs_def 549 valid_global_refs_def global_refs_def 550 valid_vs_lookup_def second_level_tables_def 551 vs_lookup_arch_update vs_lookup_pages_arch_update 552 valid_vspace_objs_def valid_arch_state_def 553 simp del: fun_upd_apply) 554 apply (rule conjI) 555 apply (clarsimp simp: comp_upd_simp is_inv_None_upd) 556 apply (clarsimp simp: valid_asid_map_def valid_machine_state_def) 557 apply (rule conjI) 558 apply (erule order_trans[rotated], clarsimp) 559 apply (simp add: pd_at_asid_arch_up') 560 apply (clarsimp simp: comp_upd_simp None_upd_eq) 561 done 562 563lemmas cleanCaches_PoU_irq_masks = no_irq[OF no_irq_cleanCaches_PoU] 564 565lemmas ackInterrupt_irq_masks = no_irq[OF no_irq_ackInterrupt] 566 567lemmas setIRQTrigger_irq_masks = no_irq[OF no_irq_setIRQTrigger] 568 569lemma invalidate_I_PoU_underlying_memory[wp]: 570 "\<lbrace>\<lambda>m'. underlying_memory m' p = um\<rbrace> 571 invalidate_I_PoU 572 \<lbrace>\<lambda>_ m'. underlying_memory m' p = um\<rbrace>" 573 by (clarsimp simp: invalidate_I_PoU_def machine_op_lift_def 574 machine_rest_lift_def split_def | wp)+ 575 576lemma clean_D_PoU_underlying_memory[wp]: 577 "\<lbrace>\<lambda>m'. underlying_memory m' p = um\<rbrace> 578 clean_D_PoU 579 \<lbrace>\<lambda>_ m'. underlying_memory m' p = um\<rbrace>" 580 by (clarsimp simp: clean_D_PoU_def machine_op_lift_def 581 machine_rest_lift_def split_def | wp)+ 582 583crunches dsb, invalidate_I_PoU, clean_D_PoU, cleanCaches_PoU 584 for device_state_inv[wp]: "\<lambda>ms. P (device_state ms)" 585 and underlying_memory_inv[wp]: "\<lambda>ms. P (underlying_memory ms)" 586 587lemma dmo_cleanCaches_PoU_invs[wp]: "\<lbrace>invs\<rbrace> do_machine_op cleanCaches_PoU \<lbrace>\<lambda>y. invs\<rbrace>" 588 apply (wp dmo_invs) 589 apply clarsimp 590 apply safe 591 apply (simp add: use_valid[OF _ cleanCaches_PoU_underlying_memory_inv[where P="\<lambda>x. x = v" for v]]) 592 apply(erule(1) use_valid[OF _ cleanCaches_PoU_irq_masks]) 593 done 594 595lemma flush_space_invs[wp]: "\<lbrace>invs\<rbrace> flush_space asid \<lbrace>\<lambda>_. invs\<rbrace>" 596 apply (simp add: flush_space_def | wp | wpc)+ 597 apply (rule_tac Q="K invs" in hoare_post_imp, (simp|wp)+) 598 done 599 600crunch valid_vs_lookup[wp]: flush_space "valid_vs_lookup" 601 602crunch valid_arch_state[wp]: flush_space "valid_arch_state" 603 604crunch valid_global_objs[wp]: flush_space "valid_global_objs" 605 606crunch caps_of_state[wp]: flush_space "\<lambda>s. P (caps_of_state s)" 607 608 609lemma ucast_ucast_low_bits: 610 fixes x :: word32 611 shows "x \<le> 2^asid_low_bits - 1 \<Longrightarrow> ucast (ucast x:: 10 word) = x" 612 apply (simp add: ucast_ucast_mask) 613 apply (rule less_mask_eq) 614 apply (subst (asm) word_less_sub_le) 615 apply (simp add: asid_low_bits_def word_bits_def) 616 apply (simp add: asid_low_bits_def) 617 done 618 619 620lemma asid_high_bits_of_or: 621 "x \<le> 2^asid_low_bits - 1 \<Longrightarrow> asid_high_bits_of (base || x) = asid_high_bits_of base" 622 apply (rule word_eqI) 623 apply (drule le_2p_upper_bits) 624 apply (simp add: asid_low_bits_def word_bits_def) 625 apply (simp add: asid_high_bits_of_def word_size nth_ucast nth_shiftr asid_low_bits_def word_bits_def) 626 done 627 628 629crunch vs_lookup [wp]: invalidate_asid_entry "\<lambda>s. P (vs_lookup s)" 630 631crunch vs_lookup [wp]: flush_space "\<lambda>s. P (vs_lookup s)" 632 633 634lemma vs_lookup_clear_asid_table: 635 "(rf \<rhd> p) (s\<lparr>arch_state := arch_state s 636 \<lparr>arm_asid_table := (arm_asid_table (arch_state s)) 637 (pptr := None)\<rparr>\<rparr>) 638 \<longrightarrow> (rf \<rhd> p) s" 639 apply (simp add: vs_lookup_def vs_lookup1_def) 640 apply (rule impI, erule subsetD[rotated]) 641 apply (rule Image_mono[OF order_refl]) 642 apply (simp add: vs_asid_refs_def graph_of_def) 643 apply (rule image_mono) 644 apply (clarsimp split: if_split_asm) 645 done 646 647 648lemma vs_lookup_pages_clear_asid_table: 649 "(rf \<unrhd> p) (s\<lparr>arch_state := arch_state s 650 \<lparr>arm_asid_table := (arm_asid_table (arch_state s)) 651 (pptr := None)\<rparr>\<rparr>) 652 \<Longrightarrow> (rf \<unrhd> p) s" 653 apply (simp add: vs_lookup_pages_def vs_lookup_pages1_def) 654 apply (erule subsetD[rotated]) 655 apply (rule Image_mono[OF order_refl]) 656 apply (simp add: vs_asid_refs_def graph_of_def) 657 apply (rule image_mono) 658 apply (clarsimp split: if_split_asm) 659 done 660 661 662lemma valid_arch_state_unmap_strg: 663 "valid_arch_state s \<longrightarrow> 664 valid_arch_state(s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := (arm_asid_table (arch_state s))(ptr := None)\<rparr>\<rparr>)" 665 apply (clarsimp simp: valid_arch_state_def valid_asid_table_def) 666 apply (rule conjI) 667 apply (clarsimp simp add: ran_def) 668 apply blast 669 apply (clarsimp simp: inj_on_def) 670 done 671 672 673lemma valid_vspace_objs_unmap_strg: 674 "valid_vspace_objs s \<longrightarrow> 675 valid_vspace_objs(s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := (arm_asid_table (arch_state s))(ptr := None)\<rparr>\<rparr>)" 676 apply (clarsimp simp: valid_vspace_objs_def) 677 apply (drule vs_lookup_clear_asid_table [rule_format]) 678 apply blast 679 done 680 681 682lemma valid_vs_lookup_unmap_strg: 683 "valid_vs_lookup s \<longrightarrow> 684 valid_vs_lookup(s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := (arm_asid_table (arch_state s))(ptr := None)\<rparr>\<rparr>)" 685 apply (clarsimp simp: valid_vs_lookup_def) 686 apply (drule vs_lookup_pages_clear_asid_table) 687 apply blast 688 done 689 690 691lemma ex_asid_high_bits_plus: 692 "asid \<le> mask asid_bits \<Longrightarrow> \<exists>x \<le> 2^asid_low_bits - 1. asid = (ucast (asid_high_bits_of asid) << asid_low_bits) + x" 693 apply (rule_tac x="asid && mask asid_low_bits" in exI) 694 apply (rule conjI) 695 apply (simp add: mask_def) 696 apply (rule word_and_le1) 697 apply (subst (asm) mask_def) 698 apply (simp add: upper_bits_unset_is_l2p_32 [symmetric]) 699 apply (subst word_plus_and_or_coroll) 700 apply (rule word_eqI) 701 apply (clarsimp simp: word_size nth_ucast nth_shiftl) 702 apply (rule word_eqI) 703 apply (clarsimp simp: word_size nth_ucast nth_shiftl nth_shiftr asid_high_bits_of_def 704 asid_low_bits_def word_bits_def asid_bits_def) 705 apply (rule iffI) 706 prefer 2 707 apply fastforce 708 apply (clarsimp simp: linorder_not_less) 709 apply (rule conjI) 710 prefer 2 711 apply arith 712 apply (subgoal_tac "n < 17", simp) 713 apply (clarsimp simp add: linorder_not_le [symmetric]) 714 done 715 716 717lemma asid_high_bits_shl: 718 "\<lbrakk> is_aligned base asid_low_bits; base \<le> mask asid_bits \<rbrakk> \<Longrightarrow> ucast (asid_high_bits_of base) << asid_low_bits = base" 719 apply (simp add: mask_def upper_bits_unset_is_l2p_32 [symmetric]) 720 apply (rule word_eqI[rule_format]) 721 apply (simp add: is_aligned_nth nth_ucast nth_shiftl nth_shiftr asid_low_bits_def 722 asid_high_bits_of_def word_size asid_bits_def word_bits_def) 723 apply (rule iffI, clarsimp) 724 apply (rule context_conjI) 725 apply (clarsimp simp add: linorder_not_less [symmetric]) 726 apply simp 727 apply (rule conjI) 728 prefer 2 729 apply simp 730 apply (subgoal_tac "n < 17", simp) 731 apply (clarsimp simp add: linorder_not_le [symmetric]) 732 done 733 734 735lemma valid_asid_map_unmap: 736 "valid_asid_map s \<and> is_aligned base asid_low_bits \<and> base \<le> mask asid_bits \<and> 737 (\<forall>x \<in> set [0.e.2^asid_low_bits - 1]. arm_asid_map (arch_state s) (base + x) = None) \<longrightarrow> 738 valid_asid_map(s\<lparr>arch_state := arch_state s\<lparr>arm_asid_table := (arm_asid_table (arch_state s))(asid_high_bits_of base := None)\<rparr>\<rparr>)" 739 apply (clarsimp simp: valid_asid_map_def vspace_at_asid_def) 740 apply (drule bspec, blast) 741 apply clarsimp 742 apply (erule vs_lookupE) 743 apply (clarsimp simp: vs_asid_refs_def dest!: graph_ofD) 744 apply (frule vs_lookup1_trans_is_append, clarsimp) 745 apply (drule ucast_up_inj, simp) 746 apply clarsimp 747 apply (rule_tac ref'="([VSRef (ucast (asid_high_bits_of a)) None],ba)" in vs_lookupI) 748 apply (simp add: vs_asid_refs_def) 749 apply (simp add: graph_of_def) 750 apply (rule_tac x="(asid_high_bits_of a, ba)" in image_eqI) 751 apply simp 752 apply clarsimp 753 apply (subgoal_tac "a \<le> mask asid_bits") 754 prefer 2 755 apply fastforce 756 apply (drule_tac asid=a in ex_asid_high_bits_plus) 757 apply (clarsimp simp: asid_high_bits_shl) 758 apply (drule rtranclD, simp) 759 apply (drule tranclD) 760 apply clarsimp 761 apply (drule vs_lookup1D) 762 apply clarsimp 763 apply (frule vs_lookup1_trans_is_append, clarsimp) 764 apply (drule vs_lookup_trans_ptr_eq, clarsimp) 765 apply (rule r_into_rtrancl) 766 apply (rule vs_lookup1I) 767 apply simp 768 apply assumption 769 apply simp 770 done 771 772 773lemma invalidate_asid_entry_asid_map_None_inv: 774 "\<lbrace>\<lambda>s. arm_asid_map (arch_state s) y = None\<rbrace> 775 invalidate_asid_entry (base + x) 776 \<lbrace>\<lambda>_ s. arm_asid_map (arch_state s) y = None\<rbrace>" 777 apply (simp add: invalidate_asid_entry_def invalidate_asid_def 778 invalidate_hw_asid_entry_def) 779 apply (wp load_hw_asid_wp) 780 apply simp 781 done 782 783 784lemma mapM_invalidate: 785 "\<lbrace>[VSRef (ucast (asid_high_bits_of base)) None] \<rhd> ptr and 786 ko_at (ArchObj (arch_kernel_obj.ASIDPool pool)) ptr and 787 valid_asid_map and K (is_aligned base asid_low_bits)\<rbrace> 788 mapM (\<lambda>offset. when (\<exists>y. pool (ucast offset) = Some y) 789 (do y \<leftarrow> flush_space (base + offset); 790 invalidate_asid_entry (base + offset) 791 od)) 792 [0.e.2 ^ asid_low_bits - 1] 793 \<lbrace>\<lambda>rv s. \<forall>x\<le>2 ^ asid_low_bits - 1. arm_asid_map (arch_state s) (base + x) = None\<rbrace>" 794proof - 795 have ball: "\<And>P w::word32. (\<forall>x\<le>w. P x) = (\<forall>x \<in> set [0.e.w]. P x)" by simp 796 show ?thesis 797 apply (subst ball) 798 apply (rule mapM_set) 799 apply (wp, simp) 800 apply (wp | 801 simp add: invalidate_asid_entry_def invalidate_asid_def 802 invalidate_hw_asid_entry_def 803 cong: if_cong)+ 804 apply clarsimp 805 apply (rule ccontr) 806 apply clarsimp 807 apply (clarsimp simp: valid_asid_map_def) 808 apply (drule bspec, erule graph_ofI) 809 apply (erule vs_lookup_atE) 810 apply (clarsimp simp: vspace_at_asid_def) 811 apply (drule vs_lookup_2ConsD) 812 apply clarsimp 813 apply (erule vs_lookup_atE) 814 apply (drule vs_lookup1D) 815 apply clarsimp 816 apply (subgoal_tac "p' = ptr") 817 apply (clarsimp simp: obj_at_def vs_refs_def graph_of_def) 818 apply (subgoal_tac "base + x && mask asid_low_bits = x") 819 apply (simp add: ucast_ucast_mask) 820 apply (subgoal_tac "aa && mask 32 = aa") 821 apply simp 822 apply (rule word_eqI) 823 apply (simp add: word_size) 824 apply (subst add_mask_eq, assumption+) 825 apply (simp add: asid_low_bits_def word_bits_def) 826 apply (rule refl) 827 apply (subst (asm) asid_high_bits_of_add, assumption+) 828 apply simp 829 apply (wp invalidate_asid_entry_asid_map_None_inv) 830 apply simp 831 done 832qed 833 834 835lemma asid_low_bits_word_bits: 836 "asid_low_bits < word_bits" 837 by (simp add: asid_low_bits_def word_bits_def) 838 839 840lemma valid_global_objs_arch_update: 841 "arm_global_pd (f (arch_state s)) = arm_global_pd (arch_state s) 842 \<and> arm_global_pts (f (arch_state s)) = arm_global_pts (arch_state s) 843 \<Longrightarrow> valid_global_objs (arch_state_update f s) = valid_global_objs s" 844 by (simp add: valid_global_objs_def second_level_tables_def) 845 846 847crunch valid_global_objs[wp]: invalidate_asid_entry "valid_global_objs" 848 (simp: valid_global_objs_arch_update) 849 850crunch valid_vs_lookup[wp]: invalidate_hw_asid_entry "valid_vs_lookup" 851 (simp: valid_vs_lookup_def) 852 853crunch valid_vs_lookup[wp]: invalidate_asid "valid_vs_lookup" 854 (simp: valid_vs_lookup_def) 855 856crunch valid_vs_lookup[wp]: invalidate_asid_entry "valid_vs_lookup" 857 858 859crunch arm_asid_table_inv[wp]: invalidate_asid_entry 860 "\<lambda>s. P (arm_asid_table (arch_state s))" 861 862 863crunch pred_tcb_at_P [wp]: find_free_hw_asid "\<lambda>s. P (pred_tcb_at proj Q p s)" 864 865 866crunch pred_tcb_at [wp]: find_pd_for_asid "\<lambda>s. P (pred_tcb_at proj Q p s)" 867 (simp: crunch_simps) 868 869 870crunch aligned [wp]: load_hw_asid pspace_aligned 871 872 873lemma hw_asid_Some [wp]: 874 "\<lbrace>valid_asid asid\<rbrace> 875 load_hw_asid asid 876 \<lbrace>\<lambda>rv s. \<exists>y. rv = Some y\<rbrace>" 877 by (simp add: load_hw_asid_def, wp) (simp add: valid_asid_def) 878 879crunches set_vm_root_for_flush 880 for typ_at [wp]: "\<lambda>s. P (typ_at T p s)" 881 and cur [wp]: cur_tcb 882 and valid_objs [wp]: valid_objs 883 and aligned [wp]: pspace_aligned 884 885lemmas set_vm_root_for_flush_typ_ats [wp] = abs_typ_at_lifts [OF set_vm_root_for_flush_typ_at] 886 887lemma store_hw_asid_valid_arch: 888 notes hoare_pre [wp_pre del] 889 shows "\<lbrace>valid_arch_state and 890 (\<lambda>s. arm_asid_map (arch_state s) asid = None \<and> 891 arm_hwasid_table (arch_state s) hw_asid = None)\<rbrace> 892 store_hw_asid asid hw_asid 893 \<lbrace>\<lambda>_. valid_arch_state\<rbrace>" 894 apply (simp add: store_hw_asid_def) 895 apply wp 896 apply (simp add: valid_arch_state_def fun_upd_def[symmetric] comp_upd_simp) 897 apply (rule hoare_pre, wp) 898 apply clarsimp 899 apply (frule is_inv_NoneD[rotated]) 900 apply simp 901 apply (simp add: ran_def) 902 apply (simp add: is_inv_def) 903 done 904 905 906lemma invalidate_hw_asid_None [wp]: 907 "\<lbrace>\<top>\<rbrace> invalidate_hw_asid_entry hw_asid \<lbrace>\<lambda>_ s. arm_hwasid_table (arch_state s) hw_asid = None\<rbrace>" 908 apply (simp add: invalidate_hw_asid_entry_def) 909 apply wp 910 apply simp 911 done 912 913 914lemma find_free_hw_asid_None_hw [wp]: 915 "\<lbrace>\<top>\<rbrace> find_free_hw_asid \<lbrace>\<lambda>rv s. arm_hwasid_table (arch_state s) rv = None\<rbrace>" 916 apply (simp add: find_free_hw_asid_def) 917 apply (wp|wpc|simp)+ 918 apply (clarsimp dest!: findSomeD) 919 done 920 921 922lemma find_free_hw_asid_None_asid_map [wp]: 923 "\<lbrace>\<lambda>s. arm_asid_map (arch_state s) asid = None\<rbrace> 924 find_free_hw_asid 925 \<lbrace>\<lambda>rv s. arm_asid_map (arch_state s) asid = None\<rbrace>" 926 apply (simp add: find_free_hw_asid_def invalidate_hw_asid_entry_def invalidate_asid_def 927 cong: option.case_cong) 928 apply (wp|wpc|simp)+ 929 done 930 931 932lemma get_hw_asid_valid_arch: 933 "\<lbrace>valid_arch_state\<rbrace> get_hw_asid asid \<lbrace>\<lambda>_. valid_arch_state\<rbrace>" 934 apply (simp add: get_hw_asid_def) 935 apply (wp load_hw_asid_wp store_hw_asid_valid_arch|wpc)+ 936 apply simp 937 done 938 939 940crunch valid_arch [wp]: set_vm_root_for_flush valid_arch_state 941 942 943lemma svmrff_asid_mapped [wp]: 944 "\<lbrace>valid_asid asid\<rbrace> 945 set_vm_root_for_flush pd asid 946 \<lbrace>\<lambda>rv. valid_asid asid\<rbrace>" 947 apply (simp add: set_vm_root_for_flush_def arm_context_switch_def 948 get_hw_asid_def store_hw_asid_def find_free_hw_asid_def 949 load_hw_asid_def 950 cong: if_cong option.case_cong) 951 apply (wp|wpc|simp add: valid_asid_def|wp hoare_vcg_all_lift hoare_drop_imps)+ 952 done 953 954 955crunch vspace_at_asid[wp]: set_vm_root_for_flush "vspace_at_asid asid pd" 956 (simp: pd_at_asid_arch_up) 957 958 959lemma find_pd_for_asid_assert_wp: 960 "\<lbrace>\<lambda>s. \<forall>pd. vspace_at_asid asid pd s \<and> asid \<noteq> 0 \<longrightarrow> P pd s\<rbrace> find_pd_for_asid_assert asid \<lbrace>P\<rbrace>" 961 apply (simp add: find_pd_for_asid_assert_def 962 find_pd_for_asid_def assertE_def 963 split del: if_split) 964 apply (wp get_pde_wp get_asid_pool_wp | wpc)+ 965 apply clarsimp 966 apply (drule spec, erule mp) 967 apply (clarsimp simp: vspace_at_asid_def word_neq_0_conv) 968 apply (rule vs_lookupI) 969 apply (simp add: vs_asid_refs_def) 970 apply (rule image_eqI[OF refl]) 971 apply (erule graph_ofI) 972 apply (rule r_into_rtrancl, simp) 973 apply (erule vs_lookup1I) 974 apply (simp add: vs_refs_def) 975 apply (rule image_eqI[rotated]) 976 apply (erule graph_ofI) 977 apply simp 978 apply (simp add: mask_asid_low_bits_ucast_ucast) 979 done 980 981 982lemma store_hw_asid_asid_map [wp]: 983 "\<lbrace>valid_asid_map and K (asid \<le> mask asid_bits)\<rbrace> 984 store_hw_asid asid hw_asid \<lbrace>\<lambda>_. valid_asid_map\<rbrace>" 985 apply (simp add: store_hw_asid_def) 986 apply (wp find_pd_for_asid_assert_wp) 987 apply (clarsimp simp: valid_asid_map_def fun_upd_def[symmetric] 988 pd_at_asid_arch_up) 989 done 990 991 992lemma arm_context_switch_asid_map [wp]: 993 "\<lbrace>valid_asid_map and K (asid \<le> mask asid_bits)\<rbrace> 994 arm_context_switch pd asid \<lbrace>\<lambda>_. valid_asid_map\<rbrace>" 995 apply (simp add: arm_context_switch_def get_hw_asid_def) 996 apply (wp load_hw_asid_wp|wpc|simp)+ 997 done 998 999 1000lemma set_vm_root_for_flush_asid_map [wp]: 1001 "\<lbrace>valid_asid_map and K (asid \<le> mask asid_bits)\<rbrace> 1002 set_vm_root_for_flush pd asid \<lbrace>\<lambda>_. valid_asid_map\<rbrace>" 1003 apply (simp add: set_vm_root_for_flush_def) 1004 apply (wp|wpc|simp)+ 1005 apply (rule hoare_strengthen_post [where 1006 Q="\<lambda>_. valid_asid_map and K (asid \<le> mask asid_bits)"]) 1007 apply wp 1008 apply simp 1009 apply wp 1010 apply simp 1011 done 1012 1013 1014crunch "distinct" [wp]: set_vm_root_for_flush pspace_distinct 1015 1016crunch caps_of_state[wp]: set_vm_root_for_flush "\<lambda>s. P (caps_of_state s)" 1017 1018lemma valid_vs_lookup_arch_update: 1019 "arm_asid_table (f (arch_state s)) = arm_asid_table (arch_state s) 1020 \<Longrightarrow> valid_vs_lookup (arch_state_update f s) = valid_vs_lookup s" 1021 by (simp add: valid_vs_lookup_def vs_lookup_pages_arch_update) 1022 1023crunch valid_vs_lookup[wp]: set_vm_root_for_flush "valid_vs_lookup" 1024 (simp: valid_vs_lookup_arch_update) 1025 1026 1027crunch valid_global_objs[wp]: set_vm_root_for_flush "valid_global_objs" 1028 (simp: valid_global_objs_arch_update) 1029 1030crunch vspace_objs [wp]: set_vm_root_for_flush valid_vspace_objs 1031 (simp: valid_vspace_objs_arch_update) 1032 1033crunch typ_at [wp]: flush_table "\<lambda>s. P (typ_at T p s)" 1034 (simp: crunch_simps wp: crunch_wps) 1035 1036 1037lemmas flush_table_typ_ats [wp] = abs_typ_at_lifts [OF flush_table_typ_at] 1038 1039lemmas find_pd_for_asid_typ_ats [wp] = abs_typ_at_lifts [OF find_pd_for_asid_inv] 1040 1041crunch aligned [wp]: flush_table pspace_aligned 1042 (simp: crunch_simps wp: crunch_wps) 1043 1044 1045lemma find_pd_for_asid_page_directory [wp]: 1046 "\<lbrace>valid_vspace_objs\<rbrace> 1047 find_pd_for_asid asid 1048 \<lbrace>\<lambda>pd. page_directory_at pd\<rbrace>, -" 1049 apply (simp add: find_pd_for_asid_def assertE_def whenE_def split del: if_split) 1050 apply (wp|wpc|clarsimp|rule conjI)+ 1051 apply (drule vs_lookup_atI) 1052 apply (drule (2) valid_vspace_objsD) 1053 apply clarsimp 1054 apply (drule bspec, blast) 1055 apply (clarsimp simp: obj_at_def) 1056 done 1057 1058 1059lemma find_pd_for_asid_lookup_ref: 1060 "\<lbrace>\<top>\<rbrace> find_pd_for_asid asid \<lbrace>\<lambda>pd. ([VSRef (asid && mask asid_low_bits) (Some AASIDPool), 1061 VSRef (ucast (asid_high_bits_of asid)) None] \<rhd> pd)\<rbrace>, -" 1062 apply (simp add: find_pd_for_asid_def assertE_def whenE_def split del: if_split) 1063 apply (wp|wpc|clarsimp|rule conjI)+ 1064 apply (drule vs_lookup_atI) 1065 apply (erule vs_lookup_step) 1066 apply (erule vs_lookup1I [OF _ _ refl]) 1067 apply (simp add: vs_refs_def) 1068 apply (rule image_eqI[rotated], erule graph_ofI) 1069 apply (simp add: mask_asid_low_bits_ucast_ucast) 1070 done 1071 1072 1073lemma find_pd_for_asid_lookup[wp]: 1074 "\<lbrace>\<top>\<rbrace> find_pd_for_asid asid \<lbrace>\<lambda>pd. \<exists>\<rhd> pd\<rbrace>,-" 1075 apply (rule hoare_post_imp_R, rule find_pd_for_asid_lookup_ref) 1076 apply auto 1077 done 1078 1079 1080lemma find_pd_for_asid_pde [wp]: 1081 "\<lbrace>valid_vspace_objs and pspace_aligned\<rbrace> 1082 find_pd_for_asid asid 1083 \<lbrace>\<lambda>pd. pde_at (pd + (vptr >> 20 << 2))\<rbrace>, -" 1084proof - 1085 have x: 1086 "\<lbrace>valid_vspace_objs and pspace_aligned\<rbrace> find_pd_for_asid asid 1087 \<lbrace>\<lambda>pd. pspace_aligned and page_directory_at pd\<rbrace>, -" 1088 by (rule hoare_pre) (wp, simp) 1089 show ?thesis 1090 apply (rule hoare_post_imp_R, rule x) 1091 apply clarsimp 1092 apply (erule page_directory_pde_atI) 1093 prefer 2 1094 apply assumption 1095 apply (rule vptr_shiftr_le_2p) 1096 done 1097qed 1098 1099 1100crunch valid_objs [wp]: flush_page "valid_objs" 1101 (wp: crunch_wps hoare_drop_imps simp: crunch_simps) 1102 1103 1104crunch valid_arch [wp]: store_pde "valid_arch_state" 1105 1106 1107crunch valid_arch [wp]: flush_page "valid_arch_state" 1108 (wp: crunch_wps simp: crunch_simps) 1109 1110 1111lemma vs_lookup1_rtrancl_iterations: 1112 "(tup, tup') \<in> (vs_lookup1 s)\<^sup>* 1113 \<Longrightarrow> (length (fst tup) \<le> length (fst tup')) \<and> 1114 (tup, tup') \<in> ((vs_lookup1 s) 1115 ^^ (length (fst tup') - length (fst tup)))" 1116 apply (erule rtrancl_induct) 1117 apply simp 1118 apply (elim conjE) 1119 apply (subgoal_tac "length (fst z) = Suc (length (fst y))") 1120 apply (simp add: Suc_diff_le) 1121 apply (erule(1) relcompI) 1122 apply (clarsimp simp: vs_lookup1_def) 1123 done 1124 1125 1126lemma find_pd_for_asid_lookup_none: 1127 "\<lbrace>\<top>\<rbrace> 1128 find_pd_for_asid asid 1129 -, \<lbrace>\<lambda>e s. \<forall>p. \<not> ([VSRef (asid && mask asid_low_bits) (Some AASIDPool), 1130 VSRef (ucast (asid_high_bits_of asid)) None] \<rhd> p) s\<rbrace>" 1131 apply (simp add: find_pd_for_asid_def assertE_def 1132 split del: if_split) 1133 apply (rule hoare_pre) 1134 apply (wp | wpc)+ 1135 apply clarsimp 1136 apply (intro allI conjI impI) 1137 apply (clarsimp simp: vs_lookup_def vs_asid_refs_def up_ucast_inj_eq 1138 dest!: vs_lookup1_rtrancl_iterations 1139 graph_ofD vs_lookup1D) 1140 apply (clarsimp simp: vs_lookup_def vs_asid_refs_def 1141 dest!: vs_lookup1_rtrancl_iterations 1142 graph_ofD vs_lookup1D) 1143 apply (clarsimp simp: obj_at_def vs_refs_def up_ucast_inj_eq 1144 mask_asid_low_bits_ucast_ucast 1145 dest!: graph_ofD) 1146 done 1147 1148 1149lemma find_pd_for_asid_aligned_pd [wp]: 1150 "\<lbrace>pspace_aligned and valid_vspace_objs\<rbrace> find_pd_for_asid asid \<lbrace>\<lambda>rv s. is_aligned rv 14\<rbrace>,-" 1151 apply (simp add: find_pd_for_asid_def assertE_def split del: if_split) 1152 apply (rule hoare_pre) 1153 apply (wp|wpc)+ 1154 apply clarsimp 1155 apply (drule vs_lookup_atI) 1156 apply (drule (2) valid_vspace_objsD) 1157 apply clarsimp 1158 apply (drule bspec, blast) 1159 apply (thin_tac "ko_at ko p s" for ko p) 1160 apply (clarsimp simp: pspace_aligned_def obj_at_def) 1161 apply (drule bspec, blast) 1162 apply (clarsimp simp: a_type_def 1163 split: Structures_A.kernel_object.splits arch_kernel_obj.splits if_split_asm) 1164 done 1165 1166 1167lemma find_pd_for_asid_aligned_pd_bits[wp]: 1168 "\<lbrace>pspace_aligned and valid_vspace_objs\<rbrace> 1169 find_pd_for_asid asid 1170 \<lbrace>\<lambda>rv s. is_aligned rv pd_bits\<rbrace>, -" 1171 by (simp add: pd_bits_def pageBits_def, rule find_pd_for_asid_aligned_pd) 1172 1173 1174lemma find_pd_for_asid_lots: 1175 "\<lbrace>\<lambda>s. (\<forall>rv. ([VSRef (asid && mask asid_low_bits) (Some AASIDPool), 1176 VSRef (ucast (asid_high_bits_of asid)) None] \<rhd> rv) s 1177 \<longrightarrow> (valid_vspace_objs s \<longrightarrow> page_directory_at rv s) 1178 \<longrightarrow> Q rv s) 1179 \<and> ((\<forall>rv. \<not> ([VSRef (asid && mask asid_low_bits) (Some AASIDPool), 1180 VSRef (ucast (asid_high_bits_of asid)) None] \<rhd> rv) s) \<longrightarrow> (\<forall>e. E e s))\<rbrace> 1181 find_pd_for_asid asid 1182 \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>" 1183 apply (clarsimp simp: validE_def valid_def) 1184 apply (frule in_inv_by_hoareD [OF find_pd_for_asid_inv]) 1185 apply (frule use_valid [OF _ find_pd_for_asid_lookup_none 1186 [unfolded validE_E_def validE_def]]) 1187 apply simp 1188 apply (frule use_valid [OF _ find_pd_for_asid_lookup_ref 1189 [unfolded validE_R_def validE_def]]) 1190 apply simp 1191 apply (clarsimp split: sum.split_asm) 1192 apply (drule spec, drule uncurry, erule mp) 1193 apply clarsimp 1194 apply (frule use_valid [OF _ find_pd_for_asid_page_directory 1195 [unfolded validE_R_def validE_def]]) 1196 apply simp 1197 apply simp 1198 done 1199 1200 1201lemma vs_lookup1_inj: 1202 "\<lbrakk> ((ref, p), (ref', p')) \<in> vs_lookup1 s ^^ n; 1203 ((ref, p), (ref', p'')) \<in> vs_lookup1 s ^^ n \<rbrakk> 1204 \<Longrightarrow> p' = p''" 1205 apply (induct n arbitrary: ref ref' p p' p'') 1206 apply simp 1207 apply (clarsimp dest!: vs_lookup1D) 1208 apply (subgoal_tac "pa = pb", simp_all) 1209 apply (simp add: obj_at_def) 1210 apply (auto simp: vs_refs_def up_ucast_inj_eq dest!: graph_ofD 1211 split: Structures_A.kernel_object.split_asm arch_kernel_obj.split_asm) 1212 done 1213 1214 1215lemma vs_lookup_Cons_eq: 1216 "(ref \<rhd> p) s \<Longrightarrow> ((v # ref) \<rhd> p') s = ((ref, p) \<rhd>1 (v # ref, p')) s" 1217 apply (rule iffI) 1218 apply (clarsimp simp: vs_lookup_def vs_asid_refs_def 1219 dest!: graph_ofD) 1220 apply (frule vs_lookup1_trans_is_append[where ys=ref]) 1221 apply (frule vs_lookup1_trans_is_append[where ys="v # ref"]) 1222 apply (clarsimp dest!: vs_lookup1_rtrancl_iterations vs_lookup1D) 1223 apply (clarsimp simp add: up_ucast_inj_eq) 1224 apply (drule(1) vs_lookup1_inj) 1225 apply (simp add: vs_lookup1I) 1226 apply (erule vs_lookup_trancl_step) 1227 apply simp 1228 done 1229 1230 1231lemma vptr_shifting_3_ways: 1232 fixes vptr :: word32 shows 1233 "vptr >> 20 << 2 >> 2 = vptr >> 20" 1234 apply (rule shiftl_shiftr_id, simp add: word_bits_def) 1235 apply (rule shiftr_less_t2n', simp_all add: word_bits_def) 1236 apply (cut_tac word_log_esimps[where x=vptr]) 1237 apply (simp add: mask_def) 1238 done 1239 1240 1241lemma page_table_mapped_wp: 1242 "\<lbrace>\<lambda>s. valid_vspace_objs s \<and> pspace_aligned s 1243 \<and> (\<not> ([VSRef (vptr >> 20) (Some APageDirectory), 1244 VSRef (asid && mask asid_low_bits) (Some AASIDPool), 1245 VSRef (ucast (asid_high_bits_of asid)) None] \<rhd> pt) s 1246 \<longrightarrow> Q None s) 1247 \<and> (\<forall>pd. vspace_at_asid asid pd s \<and> page_directory_at pd s 1248 \<and> is_aligned pd pd_bits 1249 \<longrightarrow> Q (Some pd) s)\<rbrace> 1250 page_table_mapped asid vptr pt 1251 \<lbrace>Q\<rbrace>" 1252 (is "\<lbrace>?P\<rbrace> page_table_mapped asid vptr pt \<lbrace>Q\<rbrace>") 1253 apply (simp add: page_table_mapped_def) 1254 apply (rule hoare_pre) 1255 apply (wp get_pde_wp find_pd_for_asid_lots | wpc)+ 1256 apply (clarsimp simp: lookup_pd_slot_def Let_def vspace_at_asid_def) 1257 apply (rule conjI[rotated]) 1258 apply (clarsimp simp: vs_lookup_def vs_asid_refs_def 1259 dest!: graph_ofD vs_lookup1D vs_lookup1_rtrancl_iterations) 1260 apply (drule spec, erule notE, rule ImageI[rotated]) 1261 apply (rule image_eqI, rule refl, erule graph_ofI) 1262 apply (rule r_into_rtrancl, simp) 1263 apply (erule(1) vs_lookup1I) 1264 apply simp 1265 apply (clarsimp simp: vs_lookup_Cons_eq) 1266 apply (frule(1) pd_aligned) 1267 apply (clarsimp simp: vs_lookup1_def obj_at_def pd_shifting 1268 vs_refs_def pd_shifting_dual vptr_shifting_3_ways) 1269 apply (simp add: pd_bits_def pageBits_def) 1270 apply (auto simp: pde_ref_def ucast_up_ucast_id is_up_def a_type_simps 1271 source_size_def target_size_def word_size 1272 addrFromPPtr_def ptrFromPAddr_def 1273 split: if_split_asm 1274 dest!: graph_ofD) 1275 done 1276 1277 1278crunch typ_at [wp]: flush_page "\<lambda>s. P (typ_at T p s)" 1279 (wp: crunch_wps hoare_drop_imps) 1280 1281 1282lemmas flush_page_typ_ats [wp] = abs_typ_at_lifts [OF flush_page_typ_at] 1283 1284 1285crunch aligned [wp]: flush_page "pspace_aligned" 1286 (wp: crunch_wps hoare_drop_imps) 1287 1288 1289definition 1290 valid_unmap :: "vmpage_size \<Rightarrow> asid * vspace_ref \<Rightarrow> bool" 1291where 1292 "valid_unmap sz \<equiv> \<lambda>(asid, vptr). 0 < asid \<and> is_aligned vptr pageBits \<and> 1293 (sz = ARMSuperSection \<longrightarrow> is_aligned vptr 24) \<and> 1294 (sz = ARMLargePage \<longrightarrow> is_aligned vptr 16) \<and> 1295 (sz = ARMSection \<longrightarrow> is_aligned vptr 20)" 1296 1297 1298crunch vs_lookup [wp]: flush_page "\<lambda>s. P (vs_lookup s)" 1299 (wp: crunch_wps simp: crunch_simps vs_lookup_arch_update) 1300 1301crunch vs_lookup_pages [wp]: flush_page "\<lambda>s. P (vs_lookup_pages s)" 1302 (wp: crunch_wps simp: crunch_simps vs_lookup_pages_arch_update) 1303 1304lemma store_pde_pd_at_asid: 1305 "\<lbrace>vspace_at_asid asid pd\<rbrace> 1306 store_pde p pde \<lbrace>\<lambda>_. vspace_at_asid asid pd\<rbrace>" 1307 apply (simp add: store_pde_def set_pd_def set_object_def vspace_at_asid_def) 1308 apply (wp get_object_wp) 1309 apply clarsimp 1310 apply (clarsimp split: Structures_A.kernel_object.splits arch_kernel_obj.splits) 1311 apply (clarsimp simp: obj_at_def) 1312 apply (drule vs_lookup_2ConsD) 1313 apply clarsimp 1314 apply (erule vs_lookup_atE) 1315 apply (drule vs_lookup1D) 1316 apply clarsimp 1317 apply (rule_tac ref'="([VSRef (ucast (asid_high_bits_of asid)) None],p')" in vs_lookupI) 1318 apply (fastforce simp: vs_asid_refs_def graph_of_def) 1319 apply (rule r_into_rtrancl) 1320 apply (rule_tac ko=ko in vs_lookup1I) 1321 prefer 3 1322 apply (rule refl) 1323 prefer 2 1324 apply assumption 1325 apply (clarsimp simp: obj_at_def vs_refs_def) 1326 done 1327 1328 1329lemma flush_page_pd_at_asid [wp]: 1330 "\<lbrace>vspace_at_asid a pd\<rbrace> flush_page pgsz pd asid vptr \<lbrace>\<lambda>_. vspace_at_asid a pd\<rbrace>" 1331 apply (simp add: vspace_at_asid_def) 1332 apply wp 1333 done 1334 1335 1336crunch "distinct" [wp]: store_pde pspace_distinct 1337crunch "distinct" [wp]: flush_page pspace_distinct (simp: crunch_simps) 1338 1339definition "pg_entry_align pgsz \<equiv> case pgsz of 1340 ARMSmallPage \<Rightarrow> 2 1341 | ARMLargePage \<Rightarrow> 6 1342 | ARMSection \<Rightarrow> 2 1343 | ARMSuperSection \<Rightarrow> 6" 1344 1345crunch "distinct" [wp]: flush_page pspace_distinct (simp: crunch_simps) 1346 1347 1348crunch inv[wp]: check_mapping_pptr "P" 1349 1350lemma lookup_pd_slot_pd: 1351 "is_aligned pd pd_bits \<Longrightarrow> (lookup_pd_slot pd vptr && ~~ mask pd_bits) = pd" 1352 apply (simp add: lookup_pd_slot_def Let_def) 1353 apply (rule pd_shifting) 1354 apply (simp add: pd_bits_def pageBits_def) 1355 done 1356 1357crunch vspace_objs [wp]: flush_page valid_vspace_objs 1358 (simp: crunch_simps valid_vspace_objs_arch_update) 1359 1360crunch equal_mappings [wp]: flush_page equal_kernel_mappings 1361 (simp: crunch_simps) 1362 1363crunch global_objs [wp]: flush_page valid_global_objs 1364 (simp: crunch_simps) 1365 1366lemma lookup_pt_slot_is_aligned: 1367 "\<lbrace>(\<exists>\<rhd> pd) and K (vmsz_aligned vptr sz) and K (is_aligned pd pd_bits) 1368 and valid_arch_state and valid_vspace_objs and equal_kernel_mappings 1369 and pspace_aligned and valid_global_objs\<rbrace> 1370 lookup_pt_slot pd vptr 1371 \<lbrace>\<lambda>rv s. is_aligned rv (pg_entry_align sz)\<rbrace>,-" 1372 apply (simp add: lookup_pt_slot_def) 1373 apply (wp get_pde_wp | wpc)+ 1374 apply (clarsimp simp: lookup_pd_slot_pd) 1375 apply (frule(2) valid_vspace_objsD[rotated]) 1376 apply simp 1377 apply (rule is_aligned_add) 1378 apply (case_tac "ucast (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<in> kernel_mapping_slots") 1379 apply (frule kernel_mapping_slots_empty_pdeI) 1380 apply (simp add: obj_at_def)+ 1381 apply clarsimp 1382 apply (erule_tac x="ptrFromPAddr x" in allE) 1383 apply (simp add: pde_ref_def second_level_tables_def) 1384 apply (erule is_aligned_weaken[OF is_aligned_global_pt]) 1385 apply ((simp add: invs_psp_aligned invs_vspace_objs invs_arch_state 1386 pg_entry_align_def pt_bits_def pageBits_def 1387 split: vmpage_size.split)+)[3] 1388 apply (drule_tac x="ucast (lookup_pd_slot pd vptr && mask pd_bits >> 2)" in bspec, simp) 1389 apply (clarsimp simp: obj_at_def a_type_def) 1390 apply (simp split: Structures_A.kernel_object.split_asm if_split_asm 1391 arch_kernel_obj.split_asm) 1392 apply (erule is_aligned_weaken[OF pspace_alignedD], simp) 1393 apply (simp add: obj_bits_def pg_entry_align_def split: vmpage_size.splits) 1394 apply (rule is_aligned_shiftl) 1395 apply (rule is_aligned_andI1) 1396 apply (rule is_aligned_shiftr) 1397 apply (case_tac sz) 1398 apply (clarsimp simp: vmsz_aligned_def pg_entry_align_def 1399 elim!: is_aligned_weaken split: vmpage_size.splits)+ 1400 done 1401 1402lemmas lookup_pt_slot_is_aligned_6 = 1403 lookup_pt_slot_is_aligned[where sz=ARMLargePage, 1404 unfolded pg_entry_align_def, simplified vmpage_size.simps] 1405 1406lemma lookup_pd_slot_aligned_6: 1407 "\<lbrakk> vmsz_aligned vptr ARMSuperSection; is_aligned pd 14 \<rbrakk> 1408 \<Longrightarrow> is_aligned (lookup_pd_slot pd vptr) 6" 1409 apply (simp add: lookup_pd_slot_def) 1410 apply (erule aligned_add_aligned, simp_all add: word_bits_conv) 1411 apply (intro is_aligned_shiftl is_aligned_shiftr) 1412 apply (simp add: vmsz_aligned_def) 1413 done 1414 1415lemma page_directory_at_aligned_pd_bits: 1416 "\<lbrakk>page_directory_at pd s;pspace_aligned s\<rbrakk> 1417 \<Longrightarrow> is_aligned pd pd_bits" 1418 apply (clarsimp simp:obj_at_def) 1419 apply (drule(1) pspace_alignedD) 1420 apply (simp add:pd_bits_def pageBits_def) 1421 done 1422 1423crunch vspace_objs [wp]: flush_page valid_vspace_objs 1424 (simp: crunch_simps valid_vspace_objs_arch_update) 1425 1426 1427definition 1428 "empty_refs m \<equiv> case m of Inr (pde, _) \<Rightarrow> pde_ref pde = None | _ \<Rightarrow> True" 1429 1430 1431definition 1432 "parent_for_refs m \<equiv> \<lambda>cap. 1433 case m of Inl (_, slots) 1434 \<Rightarrow> (\<lambda>x. x && ~~ mask pt_bits) ` set slots \<subseteq> obj_refs cap 1435 \<and> is_pt_cap cap \<and> cap_asid cap \<noteq> None 1436 | Inr (_, slots) 1437 \<Rightarrow> (\<lambda>x. x && ~~ mask pd_bits) ` set slots \<subseteq> obj_refs cap 1438 \<and> is_pd_cap cap \<and> cap_asid cap \<noteq> None" 1439 1440definition 1441 "same_refs m cap s \<equiv> 1442 case m of 1443 Inl (pte, slots) \<Rightarrow> 1444 (\<exists>p. pte_ref_pages pte = Some p \<and> p \<in> obj_refs cap) \<and> 1445 (case slots of 1446 [] \<Rightarrow> True 1447 | x # xs \<Rightarrow> \<forall>ref. (ref \<rhd> (x && ~~ mask pt_bits)) s \<longrightarrow> 1448 vs_cap_ref cap = Some (VSRef (x && mask pt_bits >> 2) (Some APageTable) # ref)) 1449 | Inr (pde, slots) \<Rightarrow> 1450 (\<exists>p. pde_ref_pages pde = Some p \<and> p \<in> obj_refs cap) \<and> 1451 (case slots of 1452 [] \<Rightarrow> True 1453 | x # xs \<Rightarrow> \<forall>ref. (ref \<rhd> (x && ~~ mask pd_bits)) s \<longrightarrow> 1454 vs_cap_ref cap = Some (VSRef (x && mask pd_bits >> 2) (Some APageDirectory) # ref))" 1455 1456definition 1457 "valid_page_inv pg_inv \<equiv> case pg_inv of 1458 PageMap asid cap ptr m \<Rightarrow> 1459 cte_wp_at (is_arch_update cap and ((=) None \<circ> vs_cap_ref)) ptr 1460 and cte_wp_at is_pg_cap ptr 1461 and (\<lambda>s. same_refs m cap s) 1462 and valid_slots m 1463 and valid_cap cap 1464 and K (is_pg_cap cap \<and> empty_refs m \<and> asid \<le> mask asid_bits \<and> asid \<noteq> 0) 1465 and (\<lambda>s. \<exists>slot. cte_wp_at (parent_for_refs m) slot s) 1466 and (\<lambda>s. \<exists>pd. vspace_at_asid asid pd s) 1467 | PageRemap asid m \<Rightarrow> 1468 valid_slots m and K (empty_refs m \<and> asid \<le> mask asid_bits \<and> asid \<noteq> 0) 1469 and (\<lambda>s. \<exists>slot. cte_wp_at (parent_for_refs m) slot s) 1470 and (\<lambda>s. \<exists>slot. cte_wp_at (\<lambda>cap. same_refs m cap s) slot s) 1471 and (\<lambda>s. \<exists>pd. vspace_at_asid asid pd s) 1472 | PageUnmap cap ptr \<Rightarrow> 1473 \<lambda>s. \<exists>dev r R sz m. cap = PageCap dev r R sz m \<and> 1474 case_option True (valid_unmap sz) m \<and> 1475 cte_wp_at (is_arch_diminished (cap.ArchObjectCap cap)) ptr s \<and> 1476 s \<turnstile> (cap.ArchObjectCap cap) 1477 | PageFlush typ start end pstart pd asid \<Rightarrow> 1478 vspace_at_asid asid pd and K (asid \<le> mask asid_bits \<and> asid \<noteq> 0) 1479 | PageGetAddr ptr \<Rightarrow> \<top>" 1480 1481definition 1482 "valid_pdi pdi \<equiv> case pdi of 1483 PageDirectoryFlush typ start end pstart pd asid \<Rightarrow> 1484 vspace_at_asid asid pd and K (asid \<le> mask asid_bits \<and> asid \<noteq> 0) 1485 | PageDirectoryNothing \<Rightarrow> \<top>" 1486 1487 1488crunch aligned [wp]: unmap_page pspace_aligned 1489 (wp: crunch_wps) 1490 1491 1492crunch "distinct" [wp]: unmap_page pspace_distinct 1493 (wp: crunch_wps simp: crunch_simps) 1494 1495 1496crunch valid_objs[wp]: unmap_page "valid_objs" 1497 (wp: crunch_wps) 1498 1499 1500crunch caps_of_state [wp]: unmap_page "\<lambda>s. P (caps_of_state s)" 1501 (wp: crunch_wps simp: crunch_simps) 1502 1503lemma set_cap_valid_slots[wp]: 1504 "\<lbrace>valid_slots x2\<rbrace> set_cap cap (a, b) 1505 \<lbrace>\<lambda>rv s. valid_slots x2 s \<rbrace>" 1506 apply (case_tac x2) 1507 apply (clarsimp simp:valid_slots_def) 1508 apply (wp hoare_vcg_ball_lift) 1509 apply (clarsimp simp:valid_slots_def) 1510 apply (wp hoare_vcg_ball_lift) 1511 done 1512 1513definition 1514 empty_pde_at :: "obj_ref \<Rightarrow> 'z::state_ext state \<Rightarrow> bool" 1515where 1516 "empty_pde_at p \<equiv> \<lambda>s. 1517 \<exists>pd. ko_at (ArchObj (PageDirectory pd)) (p && ~~ mask pd_bits) s \<and> 1518 pd (ucast (p && mask pd_bits >> 2)) = InvalidPDE" 1519 1520 1521definition 1522 kernel_vsrefs :: "vs_ref set" 1523where 1524 "kernel_vsrefs \<equiv> {r. case r of VSRef x y \<Rightarrow> (kernel_base >> 20) \<le> x}" 1525 1526 1527definition 1528 "valid_pti pti \<equiv> case pti of 1529 PageTableMap cap ptr pde p \<Rightarrow> 1530 pde_at p and (\<lambda>s. wellformed_pde pde) and 1531 valid_pde pde and valid_cap cap and 1532 cte_wp_at (\<lambda>c. is_arch_update cap c \<and> cap_asid c = None) ptr and 1533 empty_pde_at p and 1534 (\<lambda>s. \<exists>p' ref. vs_cap_ref cap = Some (VSRef (p && mask pd_bits >> 2) (Some APageDirectory) # ref) 1535 \<and> (ref \<rhd> (p && ~~ mask pd_bits)) s 1536 \<and> pde_ref pde = Some p' \<and> p' \<in> obj_refs cap 1537 \<and> (\<exists>ao. ko_at (ArchObj ao) p' s \<and> valid_vspace_obj ao s) 1538 \<and> hd (the (vs_cap_ref cap)) \<notin> kernel_vsrefs) and 1539 K (is_pt_cap cap \<and> cap_asid cap \<noteq> None) 1540 | PageTableUnmap cap ptr \<Rightarrow> 1541 cte_wp_at (\<lambda>c. is_arch_diminished cap c) ptr and valid_cap cap 1542 and is_final_cap' cap 1543 and K (is_pt_cap cap)" 1544 1545crunch aligned [wp]: unmap_page_table pspace_aligned 1546 (wp: crunch_wps) 1547 1548 1549crunch valid_objs [wp]: unmap_page_table valid_objs 1550 (wp: crunch_wps simp: crunch_simps) 1551 1552 1553crunch "distinct" [wp]: unmap_page_table pspace_distinct 1554 (wp: crunch_wps simp: crunch_simps) 1555 1556 1557crunch caps_of_state [wp]: unmap_page_table "\<lambda>s. P (caps_of_state s)" 1558 (wp: crunch_wps simp: crunch_simps) 1559 1560 1561crunch typ_at [wp]: unmap_page_table "\<lambda>s. P (typ_at T p s)" 1562 (wp: crunch_wps hoare_drop_imps) 1563 1564 1565definition 1566 "valid_apinv ap \<equiv> case ap of 1567 asid_pool_invocation.Assign asid p slot \<Rightarrow> 1568 (\<lambda>s. \<exists>pool. ko_at (ArchObj (arch_kernel_obj.ASIDPool pool)) p s \<and> 1569 pool (ucast asid) = None) 1570 and cte_wp_at (\<lambda>cap. is_pd_cap cap \<and> cap_asid cap = None) slot 1571 and K (0 < asid \<and> asid \<le> 2^asid_bits - 1) 1572 and ([VSRef (ucast (asid_high_bits_of asid)) None] \<rhd> p)" 1573 1574lemma store_hw_asid_invs: 1575 "\<lbrace>invs and 1576 (\<lambda>s. arm_asid_map (arch_state s) asid = None \<and> 1577 arm_hwasid_table (arch_state s) hw_asid = None \<and> 1578 asid \<le> mask asid_bits)\<rbrace> 1579 store_hw_asid asid hw_asid 1580 \<lbrace>\<lambda>x. invs\<rbrace>" 1581 apply (rule hoare_add_post) 1582 apply (rule store_hw_asid_valid_arch) 1583 apply fastforce 1584 apply (simp add: store_hw_asid_def) 1585 apply (wp find_pd_for_asid_assert_wp) 1586 apply (clarsimp simp: invs_def valid_state_def) 1587 apply (simp add: valid_global_refs_def global_refs_def 1588 valid_irq_node_def valid_vspace_objs_arch_update 1589 valid_global_objs_def valid_arch_caps_def second_level_tables_def 1590 valid_table_caps_def valid_kernel_mappings_def 1591 valid_machine_state_def valid_vs_lookup_arch_update) 1592 apply (simp add: valid_asid_map_def fun_upd_def[symmetric] 1593 pd_at_asid_arch_up) 1594 done 1595 1596lemma invalidateLocalTLB_ASID_valid_irq_states: 1597 "\<lbrace>\<lambda>m. valid_irq_states (s\<lparr>machine_state := m\<rparr>)\<rbrace> invalidateLocalTLB_ASID x 1598 \<lbrace>\<lambda>a b. valid_irq_states (s\<lparr>machine_state := b\<rparr>)\<rbrace>" 1599 apply(simp add: valid_irq_states_def | wp no_irq | simp add: no_irq_invalidateLocalTLB_ASID)+ 1600 done 1601 1602lemma find_free_hw_asid_invs [wp]: 1603 "\<lbrace>invs\<rbrace> find_free_hw_asid \<lbrace>\<lambda>asid. invs\<rbrace>" 1604 apply (rule hoare_add_post) 1605 apply (rule find_free_hw_asid_valid_arch) 1606 apply fastforce 1607 apply (simp add: find_free_hw_asid_def invalidate_hw_asid_entry_def invalidate_asid_def 1608 do_machine_op_def split_def 1609 cong: option.case_cong) 1610 apply (wp|wpc)+ 1611 apply (clarsimp simp: invs_def valid_state_def split del: if_split) 1612 apply (simp add: valid_global_refs_def global_refs_def cur_tcb_def 1613 valid_irq_node_def valid_vspace_objs_arch_update 1614 valid_global_objs_def valid_arch_caps_def second_level_tables_def 1615 valid_table_caps_def valid_kernel_mappings_def 1616 valid_machine_state_def valid_vs_lookup_arch_update) 1617 apply (elim conjE) 1618 apply (rule conjI) 1619 apply(erule use_valid[OF _ invalidateLocalTLB_ASID_valid_irq_states]) 1620 apply fastforce 1621 apply(rule conjI) 1622 apply clarsimp 1623 apply (drule use_valid) 1624 apply (rule_tac p=p in invalidateLocalTLB_ASID_underlying_memory, simp, fastforce) 1625 apply (clarsimp simp: valid_asid_map_def fun_upd_def[symmetric] 1626 pd_at_asid_arch_up') 1627 apply (rule conjI, blast) 1628 apply (clarsimp simp: vspace_at_asid_def) 1629 apply (drule_tac P1 = "(=) (device_state (machine_state s))" in 1630 use_valid[OF _ invalidateLocalTLB_ASID_device_state_inv]) 1631 apply simp 1632 apply clarsimp 1633 done 1634 1635lemma get_hw_asid_invs [wp]: 1636 "\<lbrace>invs and K (a \<le> mask asid_bits)\<rbrace> get_hw_asid a \<lbrace>\<lambda>hw_asid. invs\<rbrace>" 1637 apply (simp add: get_hw_asid_def) 1638 apply (wp store_hw_asid_invs load_hw_asid_wp|wpc)+ 1639 apply simp 1640 done 1641 1642lemma arm_context_switch_invs [wp]: 1643 "\<lbrace>invs and K (a \<le> mask asid_bits)\<rbrace> arm_context_switch pd a \<lbrace>\<lambda>_. invs\<rbrace>" 1644 apply (simp add: arm_context_switch_def) 1645 apply (wp dmo_invs) 1646 apply (rule hoare_post_imp[rotated]) 1647 apply (rule get_hw_asid_invs[simplified]) 1648 apply safe 1649 apply (drule_tac Q="\<lambda>_ m'. underlying_memory m' p = underlying_memory m p" 1650 in use_valid) 1651 apply ((clarsimp simp: setHardwareASID_def set_current_pd_def writeTTBR0_def 1652 isb_def dsb_def machine_op_lift_def 1653 machine_rest_lift_def split_def | wp)+)[3] 1654 apply(erule use_valid) 1655 apply(wp no_irq | simp add: no_irq_setHardwareASID no_irq_set_current_pd)+ 1656 done 1657 1658lemmas set_current_pd_irq_masks = no_irq[OF no_irq_set_current_pd] 1659lemmas setHardwareASID_irq_masks = no_irq[OF no_irq_setHardwareASID] 1660 1661lemma dmo_set_current_pd_invs[wp]: "\<lbrace>invs\<rbrace> do_machine_op (set_current_pd addr) \<lbrace>\<lambda>y. invs\<rbrace>" 1662 apply (wp dmo_invs) 1663 apply safe 1664 apply (drule_tac Q="\<lambda>_ m'. underlying_memory m' p = underlying_memory m p" 1665 in use_valid) 1666 apply ((clarsimp simp: set_current_pd_def writeTTBR0_def dsb_def isb_def machine_op_lift_def 1667 machine_rest_lift_def split_def | wp)+)[3] 1668 apply(erule (1) use_valid[OF _ set_current_pd_irq_masks]) 1669 done 1670 1671crunch device_state_inv[wp]: ackInterrupt "\<lambda>ms. P (device_state ms)" 1672lemma dmo_ackInterrupt[wp]: "\<lbrace>invs\<rbrace> do_machine_op (ackInterrupt irq) \<lbrace>\<lambda>y. invs\<rbrace>" 1673 apply (wp dmo_invs) 1674 apply safe 1675 apply (drule_tac Q="\<lambda>_ m'. underlying_memory m' p = underlying_memory m p" 1676 in use_valid) 1677 apply ((clarsimp simp: ackInterrupt_def machine_op_lift_def 1678 machine_rest_lift_def split_def | wp)+)[3] 1679 apply(erule (1) use_valid[OF _ ackInterrupt_irq_masks]) 1680 done 1681 1682crunch device_state_inv[wp]: setIRQTrigger "\<lambda>ms. P (device_state ms)" 1683 1684lemma dmo_setIRQTrigger_invs[wp]: "\<lbrace>invs\<rbrace> do_machine_op (setIRQTrigger irq b) \<lbrace>\<lambda>y. invs\<rbrace>" 1685 apply (wp dmo_invs) 1686 apply safe 1687 apply (drule_tac Q="\<lambda>_ m'. underlying_memory m' p = underlying_memory m p" 1688 in use_valid) 1689 apply ((clarsimp simp: setIRQTrigger_def machine_op_lift_def 1690 machine_rest_lift_def split_def | wp)+)[3] 1691 apply(erule (1) use_valid[OF _ setIRQTrigger_irq_masks]) 1692 done 1693 1694lemma svr_invs [wp]: 1695 "\<lbrace>invs\<rbrace> set_vm_root t' \<lbrace>\<lambda>_. invs\<rbrace>" 1696 apply (simp add: set_vm_root_def) 1697 apply (rule hoare_pre) 1698 apply (wp hoare_whenE_wp find_pd_for_asid_inv hoare_vcg_all_lift | wpc | simp add: split_def)+ 1699 apply (rule_tac Q'="\<lambda>_ s. invs s \<and> x2 \<le> mask asid_bits" in hoare_post_imp_R) 1700 prefer 2 1701 apply simp 1702 apply (rule valid_validE_R) 1703 apply (wp find_pd_for_asid_inv | simp add: split_def)+ 1704 apply (rule_tac Q="\<lambda>c s. invs s \<and> s \<turnstile> c" in hoare_strengthen_post) 1705 apply wp 1706 apply (clarsimp simp: valid_cap_def mask_def) 1707 apply(simp add: invs_valid_objs) 1708 done 1709 1710crunch pred_tcb_at[wp]: set_vm_root "pred_tcb_at proj P t" 1711 (simp: crunch_simps) 1712 1713lemmas set_vm_root_typ_ats [wp] = abs_typ_at_lifts [OF set_vm_root_typ_at] 1714 1715lemma valid_pte_lift3: 1716 assumes x: "(\<And>P T p. \<lbrace>\<lambda>s. P (typ_at T p s)\<rbrace> f \<lbrace>\<lambda>rv s. P (typ_at T p s)\<rbrace>)" 1717 shows "\<lbrace>\<lambda>s. P (valid_pte pte s)\<rbrace> f \<lbrace>\<lambda>rv s. P (valid_pte pte s)\<rbrace>" 1718 apply (insert bool_function_four_cases[where f=P]) 1719 apply (erule disjE) 1720 apply (cases pte) 1721 apply (simp add: data_at_def | wp hoare_vcg_const_imp_lift x)+ 1722 apply (erule disjE) 1723 apply (cases pte) 1724 apply (simp add: data_at_def | wp hoare_vcg_disj_lift hoare_vcg_const_imp_lift x)+ 1725 apply (erule disjE) 1726 apply (simp | wp)+ 1727 done 1728 1729 1730lemma set_cap_valid_pte_stronger: 1731 "\<lbrace>\<lambda>s. P (valid_pte pte s)\<rbrace> set_cap cap p \<lbrace>\<lambda>rv s. P (valid_pte pte s)\<rbrace>" 1732 by (wp valid_pte_lift3 set_cap_typ_at) 1733 1734end 1735 1736locale vs_lookup_map_some_pdes = Arch + 1737 fixes pd pdp s s' S T pd' 1738 defines "s' \<equiv> s\<lparr>kheap := kheap s(pdp \<mapsto> ArchObj (PageDirectory pd'))\<rparr>" 1739 assumes refs: "vs_refs (ArchObj (PageDirectory pd')) = 1740 (vs_refs (ArchObj (PageDirectory pd)) - T) \<union> S" 1741 assumes old: "kheap s pdp = Some (ArchObj (PageDirectory pd))" 1742 assumes pts: "\<forall>x \<in> S. page_table_at (snd x) s" 1743begin 1744 1745definition 1746 "new_lookups \<equiv> {((rs,p),(rs',p')). \<exists>r. rs' = r # rs \<and> (r,p') \<in> S \<and> p = pdp}" 1747 1748 1749lemma vs_lookup1: 1750 "vs_lookup1 s' \<subseteq> vs_lookup1 s \<union> new_lookups" 1751 apply (simp add: vs_lookup1_def) 1752 apply (clarsimp simp: obj_at_def s'_def new_lookups_def) 1753 apply (auto split: if_split_asm simp: refs old) 1754 done 1755 1756 1757lemma vs_lookup_trans: 1758 "(vs_lookup1 s')^* \<subseteq> (vs_lookup1 s)^* \<union> (vs_lookup1 s)^* O new_lookups^*" 1759 apply (rule ord_le_eq_trans, rule rtrancl_mono, rule vs_lookup1) 1760 apply (rule union_trans) 1761 apply (clarsimp simp add: new_lookups_def) 1762 apply (drule bspec [OF pts]) 1763 apply (clarsimp simp: vs_lookup1_def obj_at_def vs_refs_def) 1764 done 1765 1766 1767lemma double_new_lookup: 1768 "\<lbrakk> (x, y) \<in> new_lookups; (y, z) \<in> new_lookups \<rbrakk> \<Longrightarrow> False" 1769 by (auto simp: new_lookups_def obj_at_def old a_type_def 1770 dest!: bspec [OF pts]) 1771 1772 1773lemma new_lookups_trans: 1774 "new_lookups^* = (new_lookups \<union> Id)" 1775 apply (rule set_eqI, clarsimp, rule iffI) 1776 apply (erule rtranclE) 1777 apply simp 1778 apply (erule rtranclE) 1779 apply simp 1780 apply (drule(1) double_new_lookup) 1781 apply simp 1782 apply auto 1783 done 1784 1785 1786lemma arch_state [simp]: 1787 "arch_state s' = arch_state s" 1788 by (simp add: s'_def) 1789 1790 1791lemma vs_lookup: 1792 "vs_lookup s' \<subseteq> vs_lookup s \<union> new_lookups^* `` vs_lookup s" 1793 unfolding vs_lookup_def 1794 apply (rule order_trans) 1795 apply (rule Image_mono [OF _ order_refl]) 1796 apply (rule vs_lookup_trans) 1797 apply (clarsimp simp: relcomp_Image Un_Image) 1798 done 1799 1800lemma vs_lookup2: 1801 "vs_lookup s' \<subseteq> vs_lookup s \<union> (new_lookups `` vs_lookup s)" 1802 apply (rule order_trans, rule vs_lookup) 1803 apply (auto simp add: vs_lookup new_lookups_trans) 1804 done 1805 1806 1807end 1808 1809context Arch begin global_naming ARM 1810 1811lemma set_pd_vspace_objs_map: 1812 notes valid_vspace_obj.simps[simp del] and a_type_elims[rule del] 1813 shows 1814 "\<lbrace>valid_vspace_objs and 1815 obj_at (\<lambda>ko. vs_refs (ArchObj (PageDirectory pd)) = vs_refs ko - T \<union> S) p and 1816 (\<lambda>s. \<forall>x \<in> S. page_table_at (snd x) s) and 1817 (\<lambda>s. \<forall>(r,p') \<in> S. \<forall>ao. (\<exists>\<rhd>p) s \<longrightarrow> ko_at (ArchObj ao) p' s 1818 \<longrightarrow> valid_vspace_obj ao s) and 1819 (\<lambda>s. (\<exists>\<rhd>p) s \<longrightarrow> valid_vspace_obj (PageDirectory pd) s)\<rbrace> 1820 set_pd p pd \<lbrace>\<lambda>_. valid_vspace_objs\<rbrace>" 1821 apply (simp add: set_pd_def set_object_def) 1822 apply (wp get_object_wp) 1823 apply (clarsimp simp: obj_at_def valid_vspace_objs_def 1824 simp del: fun_upd_apply 1825 split: Structures_A.kernel_object.splits arch_kernel_obj.splits) 1826 apply (frule (1) vs_lookup_map_some_pdes.intro, simp add: obj_at_def) 1827 apply (frule vs_lookup_map_some_pdes.vs_lookup2) 1828 apply (drule(1) subsetD) 1829 apply (erule UnE) 1830 apply (simp only: fun_upd_apply split: if_split_asm) 1831 apply (rule valid_vspace_obj_same_type) 1832 apply fastforce 1833 apply assumption 1834 apply (clarsimp simp add: a_type_def) 1835 apply (rule valid_vspace_obj_same_type) 1836 apply fastforce 1837 apply assumption 1838 apply (clarsimp simp: a_type_def) 1839 apply (clarsimp simp add: vs_lookup_map_some_pdes.new_lookups_def) 1840 apply (drule(1) bspec)+ 1841 apply (clarsimp simp add: a_type_simps split: if_split_asm) 1842 apply (drule mp, erule exI)+ 1843 apply (erule(1) valid_vspace_obj_same_type) 1844 apply (simp add: a_type_def) 1845 done 1846 1847(* FIXME: move *) 1848lemma simpler_set_pd_def: 1849 "set_pd p pd = 1850 (\<lambda>s. if \<exists>pd. kheap s p = Some (ArchObj (PageDirectory pd)) 1851 then ({((), s\<lparr>kheap := kheap s(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>)}, 1852 False) 1853 else ({}, True))" 1854 by (rule ext) 1855 (auto simp: set_pd_def get_object_def simpler_gets_def assert_def 1856 return_def fail_def set_object_def get_def put_def bind_def 1857 split: Structures_A.kernel_object.split arch_kernel_obj.split) 1858 1859lemma set_pd_valid_vs_lookup_map: 1860 "\<lbrace>valid_vs_lookup and valid_arch_state and valid_vspace_objs and 1861 obj_at (\<lambda>ko. vs_refs (ArchObj (PageDirectory pd)) = 1862 vs_refs ko - T \<union> S) p and 1863 (\<lambda>s. \<forall>x\<in>S. page_table_at (snd x) s) and 1864 obj_at (\<lambda>ko. vs_refs_pages (ArchObj (PageDirectory pd)) = 1865 vs_refs_pages ko - T' \<union> S') p and 1866 (\<lambda>s. \<forall>(r, p')\<in>S. \<forall>ao. (\<exists>\<rhd> p) s \<longrightarrow> 1867 ko_at (ArchObj ao) p' s \<longrightarrow> valid_vspace_obj ao s) and 1868 (\<lambda>s. (\<exists>\<rhd> p) s \<longrightarrow> valid_vspace_obj (PageDirectory pd) s) and 1869 (\<lambda>s. \<forall>r. (r \<unrhd> p) s \<longrightarrow> 1870 (\<forall>c\<in>- kernel_mapping_slots. \<forall>q. 1871 pde_ref_pages (pd c) = Some q \<longrightarrow> 1872 (\<exists>p' cap. caps_of_state s p' = Some cap \<and> 1873 q \<in> obj_refs cap \<and> vs_cap_ref cap = 1874 Some (VSRef (ucast c) (Some APageDirectory) # r)))) and 1875 (\<lambda>s. \<forall>r. (r \<unrhd> p) s \<longrightarrow> 1876 (\<forall>c\<in>- kernel_mapping_slots. \<forall>q. 1877 pde_ref (pd c) = Some q \<longrightarrow> 1878 (\<forall>q' pt d. ko_at (ArchObj (PageTable pt)) q s \<longrightarrow> 1879 pte_ref_pages (pt d) = Some q' \<longrightarrow> 1880 (\<exists>p' cap. caps_of_state s p' = Some cap \<and> 1881 q' \<in> obj_refs cap \<and> vs_cap_ref cap = 1882 Some (VSRef (ucast d) (Some APageTable) # 1883 VSRef (ucast c) (Some APageDirectory) # r)))))\<rbrace> 1884 set_pd p pd 1885 \<lbrace>\<lambda>rv. valid_vs_lookup\<rbrace>" 1886 using set_pd_vspace_objs_map[where p=p and pd=pd and T=T and S=S] 1887 set_pd_valid_arch[of p pd] 1888 apply (clarsimp simp: valid_def simpler_set_pd_def) 1889 apply (drule_tac x=s in spec)+ 1890 apply (clarsimp simp: valid_vs_lookup_def split: if_split_asm) 1891 apply (subst caps_of_state_after_update[folded fun_upd_apply], 1892 simp add: obj_at_def) 1893 apply (erule (1) vs_lookup_pagesE_alt) 1894 apply (clarsimp simp: valid_arch_state_def valid_asid_table_def 1895 fun_upd_def) 1896 apply (drule_tac x=pa in spec) 1897 apply simp 1898 apply (drule vs_lookup_pages_atI) 1899 apply simp 1900 apply (drule_tac x=pa in spec) 1901 apply (drule_tac x="[VSRef (ucast b) (Some AASIDPool), 1902 VSRef (ucast a) None]" in spec)+ 1903 apply simp 1904 apply (drule vs_lookup_pages_apI) 1905 apply (simp split: if_split_asm) 1906 apply (simp+)[2] 1907 apply (frule_tac s="s\<lparr>kheap := kheap s(p \<mapsto> ArchObj (PageDirectory pd))\<rparr>" 1908 in vs_lookup_pages_pdI[rotated -1]) 1909 apply (simp del: fun_upd_apply)+ 1910 apply (frule vs_lookup_pages_apI) 1911 apply (simp split: if_split_asm)+ 1912 apply (thin_tac "\<forall>r. (r \<unrhd> p) s \<longrightarrow> Q r" for Q)+ 1913 apply (thin_tac "P \<longrightarrow> Q" for P Q)+ 1914 apply (drule_tac x=pa in spec) 1915 apply (drule_tac x="[VSRef (ucast c) (Some APageDirectory), 1916 VSRef (ucast b) (Some AASIDPool), 1917 VSRef (ucast a) None]" in spec) 1918 apply (erule impE) 1919 apply (erule vs_lookup_pages_pdI) 1920 apply simp+ 1921 apply (thin_tac "\<forall>r. (r \<unrhd> p) s \<longrightarrow> Q r" for Q) 1922 apply (thin_tac "P \<longrightarrow> Q" for P Q)+ 1923 apply (case_tac "p=p\<^sub>2") 1924 apply (thin_tac "\<forall>p ref. P p ref" for P) 1925 apply (frule vs_lookup_pages_apI) 1926 apply (simp split: if_split_asm) 1927 apply simp+ 1928 apply (drule spec, erule impE, assumption) 1929 apply (clarsimp split: if_split_asm) 1930 apply (drule bspec, fastforce) 1931 apply (simp add: pde_ref_def obj_at_def) 1932 apply (thin_tac "\<forall>r. (r \<unrhd> p) s \<longrightarrow> Q r" for Q) 1933 apply (clarsimp split: if_split_asm) 1934 apply (drule (7) vs_lookup_pages_ptI) 1935 apply simp 1936 done 1937 1938 1939lemma set_pd_valid_arch_caps: 1940 "\<lbrace>valid_arch_caps and valid_arch_state and valid_vspace_objs and 1941 valid_objs and 1942 obj_at (\<lambda>ko. vs_refs (ArchObj (PageDirectory pd)) = 1943 vs_refs ko - T \<union> S) p and 1944 obj_at (\<lambda>ko. vs_refs_pages (ArchObj (PageDirectory pd)) = 1945 vs_refs_pages ko - T' \<union> S') p and 1946 (\<lambda>s. \<forall>x\<in>S. page_table_at (snd x) s) and 1947 (\<lambda>s. \<forall>p. (VSRef 0 (Some AASIDPool), p) \<notin> S) and 1948 (\<lambda>s. \<forall>(r, p')\<in>S. \<forall>ao. (\<exists>\<rhd> p) s \<longrightarrow> 1949 ko_at (ArchObj ao) p' s \<longrightarrow> valid_vspace_obj ao s) and 1950 (\<lambda>s. (\<exists>\<rhd> p) s \<longrightarrow> valid_vspace_obj (PageDirectory pd) s) and 1951 (\<lambda>s. (\<exists>p' cap. caps_of_state s p' = Some cap \<and> is_pd_cap cap \<and> 1952 p \<in> obj_refs cap \<and> cap_asid cap \<noteq> None) 1953 \<or> (obj_at (empty_table (set (second_level_tables (arch_state s)))) p s \<longrightarrow> 1954 empty_table (set (second_level_tables (arch_state s))) 1955 (ArchObj (PageDirectory pd)))) and 1956 (\<lambda>s. \<forall>r. (r \<unrhd> p) s \<longrightarrow> 1957 (\<forall>c\<in>- kernel_mapping_slots. \<forall>q. 1958 pde_ref_pages (pd c) = Some q \<longrightarrow> 1959 (\<exists>p' cap. caps_of_state s p' = Some cap \<and> 1960 q \<in> obj_refs cap \<and> vs_cap_ref cap = 1961 Some (VSRef (ucast c) (Some APageDirectory) # r)))) and 1962 (\<lambda>s. \<forall>r. (r \<unrhd> p) s \<longrightarrow> 1963 (\<forall>c\<in>- kernel_mapping_slots. \<forall>q. 1964 pde_ref (pd c) = Some q \<longrightarrow> 1965 (\<forall>q' pt d. ko_at (ArchObj (PageTable pt)) q s \<longrightarrow> 1966 pte_ref_pages (pt d) = Some q' \<longrightarrow> 1967 (\<exists>p' cap. caps_of_state s p' = Some cap \<and> 1968 q' \<in> obj_refs cap \<and> vs_cap_ref cap = 1969 Some (VSRef (ucast d) (Some APageTable) # 1970 VSRef (ucast c) (Some APageDirectory) # r)))))\<rbrace> 1971 set_pd p pd 1972 \<lbrace>\<lambda>rv. valid_arch_caps\<rbrace>" 1973 apply (simp add: set_pd_def set_object_def) 1974 apply (wp get_object_wp) 1975 apply (clarsimp simp: obj_at_def simp del: fun_upd_apply 1976 split: Structures_A.kernel_object.splits arch_kernel_obj.splits) 1977 apply (clarsimp simp: valid_arch_caps_def) 1978 apply (subst caps_of_state_after_update[folded fun_upd_def], 1979 simp add: obj_at_def)+ 1980 apply simp 1981 apply (rule conjI) 1982 using set_pd_valid_vs_lookup_map[where p=p and pd=pd and T=T and S=S 1983 and T'=T' and S'=S'] 1984 apply (clarsimp simp add: valid_def) 1985 apply (drule_tac x=s in spec) 1986 apply (simp add: simpler_set_pd_def obj_at_def) 1987 apply (simp add: valid_table_caps_def obj_at_def 1988 caps_of_state_after_update[folded fun_upd_def] 1989 del: imp_disjL) 1990 apply (drule_tac x=p in spec, elim allEI, intro impI) 1991 apply clarsimp 1992 apply (erule_tac P="is_pd_cap cap" in disjE) 1993 prefer 2 1994 apply (frule_tac p="(a,b)" in caps_of_state_valid_cap, simp) 1995 apply (clarsimp simp add: is_pt_cap_def valid_cap_def obj_at_def 1996 valid_arch_cap_def 1997 a_type_def) 1998 apply (frule_tac cap=cap and cap'=capa and cs="caps_of_state s" in unique_table_caps_pdD) 1999 apply (simp add: is_pd_cap_def)+ 2000 apply (clarsimp simp: is_pd_cap_def)+ 2001 done 2002 2003(* FIXME: move to wellformed *) 2004lemma global_pde_graph_ofI: 2005 " \<lbrakk>pd x = pde; pde_ref pde = Some v\<rbrakk> 2006 \<Longrightarrow> (x, v) \<in> graph_of (pde_ref o pd)" 2007 by (clarsimp simp: graph_of_def pde_ref_def comp_def) 2008 2009 2010 2011lemma set_pd_valid_kernel_mappings_map: 2012 "\<lbrace>valid_kernel_mappings and 2013 obj_at (\<lambda>ko. glob_vs_refs (ArchObj (PageDirectory pd)) = glob_vs_refs ko - T \<union> S) p and 2014 (\<lambda>s. \<forall>(r,p) \<in> S. (r \<in> kernel_vsrefs) 2015 = (p \<in> set (arm_global_pts (arch_state s))))\<rbrace> 2016 set_pd p pd 2017 \<lbrace>\<lambda>rv. valid_kernel_mappings\<rbrace>" 2018 apply (simp add: set_pd_def) 2019 apply (wp set_object_v_ker_map get_object_wp) 2020 apply (clarsimp simp: obj_at_def valid_kernel_mappings_def 2021 split: Structures_A.kernel_object.split_asm 2022 arch_kernel_obj.split_asm) 2023 apply (drule bspec, erule ranI) 2024 apply (clarsimp simp: valid_kernel_mappings_if_pd_def 2025 kernel_vsrefs_def) 2026 apply (drule_tac f="\<lambda>S. (VSRef (ucast x) (Some APageDirectory), r) \<in> S" 2027 in arg_cong) 2028 apply (simp add: glob_vs_refs_def) 2029 apply (drule iffD1) 2030 apply (rule image_eqI[rotated]) 2031 apply (erule global_pde_graph_ofI[rotated]) 2032 apply simp+ 2033 apply (elim conjE disjE) 2034 apply (clarsimp dest!: graph_ofD) 2035 apply (drule(1) bspec) 2036 apply (clarsimp simp: kernel_base_shift_cast_le 2037 kernel_mapping_slots_def) 2038 done 2039 2040lemma glob_vs_refs_subset: 2041 " vs_refs x \<subseteq> glob_vs_refs x" 2042 apply (clarsimp simp: glob_vs_refs_def vs_refs_def) 2043 apply (clarsimp split: Structures_A.kernel_object.splits arch_kernel_obj.splits) 2044 apply (rule pair_imageI) 2045 apply (simp add: graph_of_def split:if_split_asm) 2046 done 2047 2048lemma vs_refs_pages_pdI: 2049 "\<lbrakk>pde_ref_pages (pd x) = Some a; x \<notin> kernel_mapping_slots\<rbrakk> 2050 \<Longrightarrow> (VSRef (ucast x) (Some APageDirectory), a) \<in> vs_refs_pages (ArchObj (PageDirectory pd))" 2051 by (auto simp: pde_ref_pages_def vs_refs_pages_def graph_of_def image_def split: pde.splits) 2052 2053lemma pde_ref_pde_ref_pagesI[elim!]: 2054 "pde_ref (pd x) = Some a \<Longrightarrow> pde_ref_pages (pd x) = Some a" 2055 by (auto simp: pde_ref_def pde_ref_pages_def split: pde.splits) 2056 2057lemma vs_refs_pdI2: 2058 "\<lbrakk>pd r = PageTablePDE x a b; r \<notin> kernel_mapping_slots\<rbrakk> 2059 \<Longrightarrow> (VSRef (ucast r) (Some APageDirectory), ptrFromPAddr x) \<in> vs_refs (ArchObj (PageDirectory pd))" 2060 by (auto simp: vs_refs_def pde_ref_def graph_of_def) 2061 2062 2063lemma set_pd_invs_map: 2064 "\<lbrace>invs and (\<lambda>s. \<forall>i. wellformed_pde (pd i)) and 2065 obj_at (\<lambda>ko. vs_refs (ArchObj (PageDirectory pd)) = vs_refs ko \<union> S) p and 2066 obj_at (\<lambda>ko. vs_refs_pages (ArchObj (PageDirectory pd)) = vs_refs_pages ko - T' \<union> S') p and 2067 obj_at (\<lambda>ko. \<exists>pd'. ko = ArchObj (PageDirectory pd') 2068 \<and> (\<forall>x\<in>kernel_mapping_slots. pd x = pd' x)) p and 2069 (\<lambda>s. \<forall>(r,p) \<in> S. \<forall>ao. ko_at (ArchObj ao) p s \<longrightarrow> valid_vspace_obj ao s) and 2070 (\<lambda>s. \<forall>(r,p) \<in> S. page_table_at p s) and 2071 (\<lambda>s. \<forall>(r,p) \<in> S. (r \<in> kernel_vsrefs) 2072 = (p \<in> set (arm_global_pts (arch_state s)))) and 2073 (\<lambda>s. \<exists>p' cap. caps_of_state s p' = Some cap \<and> is_pd_cap cap 2074 \<and> p \<in> obj_refs cap \<and> cap_asid cap \<noteq> None) and 2075 (\<lambda>s. \<forall>p. (VSRef 0 (Some AASIDPool), p) \<notin> S) and 2076 (\<lambda>s. \<forall>ref. (ref \<unrhd> p) s \<longrightarrow> 2077 (\<forall>(r, p) \<in> S'. \<exists>p' cap. caps_of_state s p' = Some cap \<and> p \<in> obj_refs cap 2078 \<and> vs_cap_ref cap = Some (r # ref))) and 2079 (\<lambda>s. \<forall>ref. (ref \<unrhd> p) s \<longrightarrow> 2080 (\<forall>(r, p) \<in> S. (\<forall>q' pt d. 2081 ko_at (ArchObj (PageTable pt)) p s \<longrightarrow> 2082 pte_ref_pages (pt d) = Some q' \<longrightarrow> 2083 (\<exists>p' cap. caps_of_state s p' = Some cap \<and> 2084 q' \<in> obj_refs cap \<and> 2085 vs_cap_ref cap = 2086 Some (VSRef (ucast d) (Some APageTable) # r # ref))))) and 2087 2088 valid_vspace_obj (PageDirectory pd)\<rbrace> 2089 set_pd p pd \<lbrace>\<lambda>_. invs\<rbrace>" 2090 apply (simp add: invs_def valid_state_def valid_pspace_def) 2091 apply (rule hoare_pre) 2092 apply (wp set_pd_valid_objs set_pd_iflive set_pd_zombies 2093 set_pd_zombies_state_refs set_pd_valid_mdb set_pd_zombies_state_hyp_refs 2094 set_pd_valid_idle set_pd_ifunsafe set_pd_reply_caps 2095 set_pd_valid_arch set_pd_valid_global set_pd_cur 2096 set_pd_reply_masters valid_irq_node_typ 2097 set_pd_vspace_objs_map[where S=S and T="{}"] 2098 set_pd_valid_arch_caps[where S=S and T="{}" and S'=S' and T'=T'] 2099 valid_irq_handlers_lift 2100 set_pd_valid_kernel_mappings_map[where S=S and T="{}"] 2101 set_pd_equal_kernel_mappings_triv) 2102 apply (clarsimp simp: cte_wp_at_caps_of_state) 2103 apply (frule(1) valid_global_refsD2) 2104 apply (clarsimp simp: cap_range_def split_def) 2105 apply (rule conjI) 2106 apply clarsimp 2107 2108 apply (drule (1) vs_refs_pages_pdI) 2109 apply (clarsimp simp: obj_at_def) 2110 apply (erule disjE) 2111 apply (clarsimp simp: valid_arch_caps_def) 2112 apply (drule valid_vs_lookupD[OF vs_lookup_pages_step]) 2113 apply (clarsimp simp: vs_lookup_pages1_def obj_at_def) 2114 apply (rule_tac x="VSRef (ucast c) (Some APageDirectory)" in exI) 2115 apply (erule conjI[OF refl]) 2116 apply simp 2117 apply clarsimp 2118 apply (erule_tac x=r in allE, drule (1) mp, drule (1) bspec) 2119 apply clarsimp 2120 apply (rule conjI) 2121 apply (clarsimp simp: pde_ref_def split: pde.splits) 2122 apply (drule (1) vs_refs_pdI2) 2123 apply (clarsimp simp: obj_at_def) 2124 apply (erule disjE) 2125 apply (clarsimp simp: valid_arch_caps_def) 2126 apply (drule valid_vs_lookupD[OF vs_lookup_pages_step[OF vs_lookup_pages_step]]) 2127 apply (clarsimp simp: vs_lookup_pages1_def obj_at_def) 2128 apply (rule_tac x="VSRef (ucast c) (Some APageDirectory)" in exI) 2129 apply (rule conjI[OF refl]) 2130 apply (erule subsetD[OF vs_refs_pages_subset]) 2131 apply (clarsimp simp: vs_lookup_pages1_def obj_at_def) 2132 apply (rule_tac x="VSRef (ucast d) (Some APageTable)" in exI) 2133 apply (rule conjI[OF refl]) 2134 apply (erule pte_ref_pagesD) 2135 apply simp 2136 apply clarsimp 2137 apply (erule_tac x=r in allE, drule (1) mp, drule_tac P="(%x. \<forall>q' pt . Q x q' pt y s)" for Q s in bspec) 2138 apply simp 2139 apply clarsimp 2140 apply (rule conjI) 2141 apply clarsimp 2142 apply (clarsimp simp add: obj_at_def glob_vs_refs_def) 2143 apply safe[1] 2144 apply (rule pair_imageI) 2145 apply (clarsimp simp add: graph_of_def) 2146 apply (case_tac "ab \<in> kernel_mapping_slots") 2147 apply clarsimp 2148 apply (frule (1) pde_graph_ofI[rotated]) 2149 apply (case_tac "pd ab", simp_all) 2150 apply (clarsimp simp: vs_refs_def ) 2151 apply (drule_tac x="(ab, bb)" and f="(\<lambda>(r, y). (VSRef (ucast r) (Some APageDirectory), y))" 2152 in imageI) 2153 apply simp 2154 apply (erule imageE) 2155 apply (simp add: graph_of_def split_def) 2156 apply (rule pair_imageI) 2157 apply (case_tac "ab \<in> kernel_mapping_slots") 2158 apply (clarsimp simp add: graph_of_def)+ 2159 apply (frule (1) pde_graph_ofI[rotated]) 2160 apply (case_tac "pd ab", simp_all) 2161 apply (clarsimp simp: vs_refs_def ) 2162 apply (drule_tac x="(ab, bb)" and f="(\<lambda>(r, y). (VSRef (ucast r) (Some APageDirectory), y))" 2163 in imageI) 2164 apply (drule_tac s="(\<lambda>(r, y). (VSRef (ucast r) (Some APageDirectory), y)) ` 2165 graph_of 2166 (\<lambda>x. if x \<in> kernel_mapping_slots then None else pde_ref (pd x))" in sym) 2167 apply simp 2168 apply (drule_tac c="(VSRef (ucast ab) (Some APageDirectory), bb)" and B=S in UnI1) 2169 apply simp 2170 apply (erule imageE) 2171 apply (simp add: graph_of_def split_def) 2172 apply (subst (asm) Un_commute[where B=S]) 2173 apply (drule_tac c="(aa,ba)" and B="vs_refs (ArchObj (PageDirectory pd'))" in UnI1) 2174 apply (drule_tac t="S \<union> vs_refs (ArchObj (PageDirectory pd'))" in sym) 2175 apply (simp del:Un_iff) 2176 apply (drule rev_subsetD[OF _ glob_vs_refs_subset]) 2177 apply (simp add: glob_vs_refs_def) 2178 by blast 2179 2180lemma vs_refs_add_one': 2181 "p \<notin> kernel_mapping_slots \<Longrightarrow> 2182 vs_refs (ArchObj (PageDirectory (pd (p := pde)))) = 2183 vs_refs (ArchObj (PageDirectory pd)) 2184 - Pair (VSRef (ucast p) (Some APageDirectory)) ` set_option (pde_ref (pd p)) 2185 \<union> Pair (VSRef (ucast p) (Some APageDirectory)) ` set_option (pde_ref pde)" 2186 apply (simp add: vs_refs_def) 2187 apply (rule set_eqI) 2188 apply clarsimp 2189 apply (rule iffI) 2190 apply (clarsimp del: disjCI dest!: graph_ofD split: if_split_asm) 2191 apply (rule disjI1) 2192 apply (rule conjI) 2193 apply (rule_tac x="(aa,ba)" in image_eqI) 2194 apply simp 2195 apply (simp add: graph_of_def) 2196 apply clarsimp 2197 apply (erule disjE) 2198 apply (clarsimp dest!: graph_ofD) 2199 apply (rule_tac x="(aa,ba)" in image_eqI) 2200 apply simp 2201 apply (clarsimp simp: graph_of_def split:if_split_asm) 2202 apply clarsimp 2203 apply (rule_tac x="(p,x)" in image_eqI) 2204 apply simp 2205 apply (clarsimp simp: graph_of_def) 2206 done 2207 2208 2209lemma vs_refs_add_one: 2210 "\<lbrakk>pde_ref (pd p) = None; p \<notin> kernel_mapping_slots\<rbrakk> \<Longrightarrow> 2211 vs_refs (ArchObj (PageDirectory (pd (p := pde)))) = 2212 vs_refs (ArchObj (PageDirectory pd)) 2213 \<union> Pair (VSRef (ucast p) (Some APageDirectory)) ` set_option (pde_ref pde)" 2214 by (simp add: vs_refs_add_one') 2215 2216 2217lemma vs_refs_pages_add_one': 2218 "p \<notin> kernel_mapping_slots \<Longrightarrow> 2219 vs_refs_pages (ArchObj (PageDirectory (pd (p := pde)))) = 2220 vs_refs_pages (ArchObj (PageDirectory pd)) 2221 - Pair (VSRef (ucast p) (Some APageDirectory)) ` set_option (pde_ref_pages (pd p)) 2222 \<union> Pair (VSRef (ucast p) (Some APageDirectory)) ` set_option (pde_ref_pages pde)" 2223 apply (simp add: vs_refs_pages_def) 2224 apply (rule set_eqI) 2225 apply clarsimp 2226 apply (rule iffI) 2227 apply (clarsimp del: disjCI dest!: graph_ofD split: if_split_asm) 2228 apply (rule disjI1) 2229 apply (rule conjI) 2230 apply (rule_tac x="(aa,ba)" in image_eqI) 2231 apply simp 2232 apply (simp add: graph_of_def) 2233 apply clarsimp 2234 apply (erule disjE) 2235 apply (clarsimp dest!: graph_ofD) 2236 apply (rule_tac x="(aa,ba)" in image_eqI) 2237 apply simp 2238 apply (clarsimp simp: graph_of_def split:if_split_asm) 2239 apply clarsimp 2240 apply (rule_tac x="(p,x)" in image_eqI) 2241 apply simp 2242 apply (clarsimp simp: graph_of_def) 2243 done 2244 2245lemma vs_refs_pages_add_one: 2246 "\<lbrakk>pde_ref_pages (pd p) = None; p \<notin> kernel_mapping_slots\<rbrakk> \<Longrightarrow> 2247 vs_refs_pages (ArchObj (PageDirectory (pd (p := pde)))) = 2248 vs_refs_pages (ArchObj (PageDirectory pd)) 2249 \<union> Pair (VSRef (ucast p) (Some APageDirectory)) ` set_option (pde_ref_pages pde)" 2250 by (simp add: vs_refs_pages_add_one') 2251 2252definition is_asid_pool_cap :: "cap \<Rightarrow> bool" 2253 where "is_asid_pool_cap cap \<equiv> \<exists>ptr asid. cap = cap.ArchObjectCap (arch_cap.ASIDPoolCap ptr asid)" 2254 2255 2256(* FIXME: move *) 2257lemma valid_cap_to_pt_cap: 2258 "\<lbrakk>valid_cap c s; obj_refs c = {p}; page_table_at p s\<rbrakk> \<Longrightarrow> is_pt_cap c" 2259 by (clarsimp simp: valid_cap_def obj_at_def is_obj_defs is_pt_cap_def 2260 split: cap.splits option.splits arch_cap.splits if_splits) 2261 2262lemma ref_is_unique: 2263 "\<lbrakk>(ref \<rhd> p) s; (ref' \<rhd> p) s; p \<notin> set (arm_global_pts (arch_state s)); 2264 valid_vs_lookup s; unique_table_refs (caps_of_state s); 2265 valid_vspace_objs s; valid_asid_table (arm_asid_table (arch_state s)) s; 2266 valid_caps (caps_of_state s) s\<rbrakk> 2267 \<Longrightarrow> ref = ref'" 2268 apply (erule (1) vs_lookupE_alt[OF _ _ valid_asid_table_ran], clarsimp) 2269 apply (erule (1) vs_lookupE_alt[OF _ _ valid_asid_table_ran], clarsimp) 2270 apply (clarsimp simp: valid_asid_table_def up_ucast_inj_eq) 2271 apply (erule (2) inj_on_domD) 2272 apply ((clarsimp simp: obj_at_def)+)[2] 2273 apply (erule (1) vs_lookupE_alt[OF _ _ valid_asid_table_ran], clarsimp) 2274 apply (clarsimp simp: obj_at_def) 2275 apply (drule (2) vs_lookup_apI)+ 2276 apply (clarsimp dest!: valid_vs_lookupD[OF vs_lookup_pages_vs_lookupI] 2277 obj_ref_elemD 2278 simp: table_cap_ref_ap_eq[symmetric]) 2279 apply (drule_tac cap=cap and cap'=capa in unique_table_refsD, simp+)[1] 2280 apply (clarsimp simp: obj_at_def) 2281 apply (erule (1) vs_lookupE_alt[OF _ _ valid_asid_table_ran], clarsimp) 2282 apply ((clarsimp simp: obj_at_def)+)[2] 2283 apply (simp add: pde_ref_def split: pde.splits) 2284 apply (drule (5) vs_lookup_pdI)+ 2285 apply (clarsimp dest!: valid_vs_lookupD[OF vs_lookup_pages_vs_lookupI] 2286 obj_ref_elemD) 2287 apply (drule_tac cap=cap and cap'=capa in unique_table_refsD, simp+)[1] 2288 apply (drule (3) valid_capsD[THEN valid_cap_to_pt_cap])+ 2289 apply (clarsimp simp: is_pt_cap_def table_cap_ref_simps vs_cap_ref_simps) 2290 done 2291 2292lemma mask_shift_mask_helper: 2293 "(p && mask pd_bits >> 2) && mask 12 = (p && mask pd_bits >> 2)" 2294 apply (rule word_eqI) 2295 apply (simp add: word_size pd_bits_def pageBits_def nth_shiftr conj_comms) 2296 done 2297 2298lemma ucast_ucast_mask_shift_helper: 2299 "ucast (ucast (p && mask pd_bits >> 2 :: word32) :: 12 word) 2300 = (p && mask pd_bits >> 2 :: word32)" 2301 apply (rule ucast_ucast_len) 2302 apply (rule shiftr_less_t2n) 2303 apply (simp add: pd_bits_def pageBits_def) 2304 apply (rule order_less_le_trans, rule and_mask_less_size) 2305 apply (simp add: word_size)+ 2306 done 2307 2308lemma unat_ucast_pd_bits_shift: 2309 "unat (ucast ((p :: word32) && mask pd_bits >> 2) :: 12 word) 2310 = unat (p && mask pd_bits >> 2)" 2311 apply (simp only: unat_ucast) 2312 apply (rule mod_less) 2313 apply (rule unat_less_power) 2314 apply (simp add: word_bits_def) 2315 apply (rule shiftr_less_t2n) 2316 apply (rule order_le_less_trans [OF word_and_le1]) 2317 apply (simp add: pd_bits_def pageBits_def mask_def) 2318 done 2319 2320lemma kernel_vsrefs_kernel_mapping_slots: 2321 "(ucast (p && mask pd_bits >> 2) \<in> kernel_mapping_slots) = 2322 (VSRef (p && mask pd_bits >> 2) (Some APageDirectory) \<in> kernel_vsrefs)" 2323 by (clarsimp simp: kernel_mapping_slots_def kernel_vsrefs_def 2324 word_le_nat_alt unat_ucast_pd_bits_shift 2325 kernel_base_def) 2326 2327lemma vs_lookup_typI: 2328 "\<lbrakk>(r \<rhd> p) s; valid_vspace_objs s; valid_asid_table (arm_asid_table (arch_state s)) s\<rbrakk> 2329 \<Longrightarrow> page_table_at p s 2330 \<or> page_directory_at p s 2331 \<or> asid_pool_at p s" 2332 apply (erule (1) vs_lookupE_alt) 2333 apply (clarsimp simp: ran_def) 2334 apply (drule (2) valid_asid_tableD) 2335 apply simp+ 2336 done 2337 2338lemma vs_lookup_vs_lookup_pagesI': 2339 "\<lbrakk>(r \<unrhd> p) s; page_table_at p s \<or> page_directory_at p s \<or> asid_pool_at p s; 2340 valid_vspace_objs s; valid_asid_table (arm_asid_table (arch_state s)) s\<rbrakk> 2341 \<Longrightarrow> (r \<rhd> p) s" 2342 apply (erule (1) vs_lookup_pagesE_alt) 2343 apply (clarsimp simp:ran_def) 2344 apply (drule (2) valid_asid_tableD) 2345 apply (rule vs_lookupI) 2346 apply (fastforce simp: vs_asid_refs_def graph_of_def) 2347 apply simp 2348 apply (rule vs_lookupI) 2349 apply (fastforce simp: vs_asid_refs_def graph_of_def) 2350 apply (rule rtrancl_into_rtrancl[OF rtrancl.intros(1)]) 2351 apply (fastforce simp: vs_lookup1_def obj_at_def vs_refs_def graph_of_def) 2352 apply (rule vs_lookupI) 2353 apply (fastforce simp: vs_asid_refs_def graph_of_def) 2354 apply (rule_tac y="([VSRef (ucast b) (Some AASIDPool), VSRef (ucast a) None], p\<^sub>2)" in rtrancl_trans) 2355 apply (rule rtrancl_into_rtrancl[OF rtrancl.intros(1)]) 2356 apply (fastforce simp: vs_lookup1_def obj_at_def vs_refs_def graph_of_def) 2357 apply (rule rtrancl_into_rtrancl[OF rtrancl.intros(1)]) 2358 apply (clarsimp simp: vs_lookup1_def obj_at_def vs_refs_def graph_of_def) 2359 apply (rule_tac x="(c, p)" in image_eqI) 2360 apply simp 2361 apply (fastforce simp: pde_ref_def pde_ref_pages_def valid_pde_def obj_at_def 2362 a_type_def data_at_def 2363 split: pde.splits if_splits arch_kernel_obj.splits) 2364 apply (rule vs_lookupI) 2365 apply (fastforce simp: vs_asid_refs_def graph_of_def) 2366 apply (rule_tac y="([VSRef (ucast b) (Some AASIDPool), VSRef (ucast a) None], p\<^sub>2)" in rtrancl_trans) 2367 apply (rule rtrancl_into_rtrancl[OF rtrancl.intros(1)]) 2368 apply (fastforce simp: vs_lookup1_def obj_at_def vs_refs_def graph_of_def) 2369 apply (rule_tac y="([VSRef (ucast c) (Some APageDirectory), VSRef (ucast b) (Some AASIDPool), 2370 VSRef (ucast a) None], (ptrFromPAddr addr))" in rtrancl_trans) 2371 apply (rule rtrancl_into_rtrancl[OF rtrancl.intros(1)]) 2372 apply (clarsimp simp: vs_lookup1_def obj_at_def vs_refs_def graph_of_def) 2373 apply (rule_tac x="(c,(ptrFromPAddr addr))" in image_eqI) 2374 apply simp 2375 apply (clarsimp simp: pde_ref_def) 2376 apply (rule rtrancl_into_rtrancl[OF rtrancl.intros(1)]) 2377 apply (auto simp: data_at_def vs_lookup1_def obj_at_def vs_refs_def graph_of_def 2378 pte_ref_pages_def a_type_def 2379 split: pte.splits if_splits arch_kernel_obj.splits) 2380 done 2381 2382lemma vs_lookup_vs_lookup_pagesI: 2383 "\<lbrakk>(r \<rhd> p) s; (r' \<unrhd> p) s; valid_vspace_objs s; valid_asid_table (arm_asid_table (arch_state s)) s\<rbrakk> 2384 \<Longrightarrow> (r' \<rhd> p) s" 2385 by (erule (5) vs_lookup_vs_lookup_pagesI'[OF _ vs_lookup_typI]) 2386 2387(* FIXME: move *) 2388lemma valid_cap_to_pd_cap: 2389 "\<lbrakk>valid_cap c s; obj_refs c = {p}; page_directory_at p s\<rbrakk> \<Longrightarrow> is_pd_cap c" 2390 by (clarsimp simp: valid_cap_def obj_at_def is_obj_defs is_pd_cap_def 2391 split: cap.splits option.splits arch_cap.splits if_splits) 2392 2393lemma store_pde_map_invs: 2394 "\<lbrace>(\<lambda>s. wellformed_pde pde) and invs and empty_pde_at p and valid_pde pde 2395 and (\<lambda>s. \<forall>p. pde_ref pde = Some p \<longrightarrow> (\<exists>ao. ko_at (ArchObj ao) p s \<and> valid_vspace_obj ao s)) 2396 and K (VSRef (p && mask pd_bits >> 2) (Some APageDirectory) 2397 \<notin> kernel_vsrefs) 2398 and (\<lambda>s. \<exists>r. (r \<rhd> (p && (~~ mask pd_bits))) s \<and> 2399 (\<forall>p'. pde_ref_pages pde = Some p' \<longrightarrow> 2400 (\<exists>p'' cap. caps_of_state s p'' = Some cap \<and> p' \<in> obj_refs cap 2401 \<and> vs_cap_ref cap = Some (VSRef (p && mask pd_bits >> 2) (Some APageDirectory) # r)) 2402 \<and> (\<forall>p''' a b. pde = PageTablePDE p''' a b \<longrightarrow> 2403 (\<forall>pt. ko_at (ArchObj (PageTable pt)) (ptrFromPAddr p''') s \<longrightarrow> 2404 (\<forall>x word. pte_ref_pages (pt x) = Some word \<longrightarrow> 2405 (\<exists>p'' cap. caps_of_state s p'' = Some cap \<and> word \<in> obj_refs cap 2406 \<and> vs_cap_ref cap = 2407 Some (VSRef (ucast x) (Some APageTable) 2408 # VSRef (p && mask pd_bits >> 2) (Some APageDirectory) 2409 # r)))))))\<rbrace> 2410 store_pde p pde \<lbrace>\<lambda>_. invs\<rbrace>" 2411 apply (simp add: store_pde_def) 2412 apply (wp dmo_invs set_pd_invs_map) 2413 apply clarsimp 2414 apply (rule conjI) 2415 apply (drule invs_valid_objs) 2416 apply (fastforce simp: valid_objs_def dom_def obj_at_def valid_obj_def) 2417 apply (rule conjI) 2418 apply (clarsimp simp: empty_pde_at_def) 2419 apply (clarsimp simp: obj_at_def) 2420 apply (rule vs_refs_add_one) 2421 subgoal by (simp add: pde_ref_def) 2422 subgoal by (simp add: kernel_vsrefs_kernel_mapping_slots) 2423 apply (rule conjI) 2424 apply (clarsimp simp: empty_pde_at_def) 2425 apply (clarsimp simp: obj_at_def) 2426 apply (rule vs_refs_pages_add_one') 2427 subgoal by (simp add: kernel_vsrefs_kernel_mapping_slots) 2428 apply (rule conjI) 2429 apply (clarsimp simp: obj_at_def kernel_vsrefs_kernel_mapping_slots) 2430 apply (rule conjI) 2431 subgoal by (clarsimp simp: obj_at_def) 2432 apply (rule conjI) 2433 apply clarsimp 2434 subgoal by (case_tac pde, simp_all add: pde_ref_def) 2435 apply (rule conjI) 2436 apply (clarsimp simp: kernel_vsrefs_def 2437 ucast_ucast_mask_shift_helper) 2438 apply (drule pde_ref_pde_ref_pagesI) 2439 apply clarsimp 2440 apply (drule valid_global_refsD2, clarsimp) 2441 apply (simp add: cap_range_def global_refs_def) 2442 apply blast 2443 apply (rule conjI) 2444 apply (drule valid_vs_lookupD[OF vs_lookup_pages_vs_lookupI], clarsimp+) 2445 apply (rule_tac x=a in exI, rule_tac x=b in exI, rule_tac x=cap in exI) 2446 apply (clarsimp dest!: obj_ref_elemD) 2447 apply (frule caps_of_state_valid_cap, clarsimp) 2448 apply (drule (1) valid_cap_to_pd_cap, simp add: obj_at_def a_type_simps) 2449 apply (thin_tac " \<forall>p. Q p \<longrightarrow> P p" for Q P)+ 2450 subgoal by (simp add: is_pd_cap_def vs_cap_ref_def 2451 split: cap.split_asm arch_cap.split_asm option.split_asm) 2452 apply (rule conjI) 2453 apply clarsimp 2454 apply (rule conjI) 2455 apply clarsimp 2456 apply (frule (2) ref_is_unique[OF _ vs_lookup_vs_lookup_pagesI]) 2457 apply ((clarsimp simp: invs_def valid_state_def valid_arch_caps_def 2458 valid_arch_state_def)+)[2] 2459 apply (auto dest!: valid_global_ptsD [simplified second_level_tables_def] simp: obj_at_def )[1] 2460 apply clarsimp+ 2461 apply (rule valid_objs_caps) 2462 apply clarsimp 2463 apply (simp add: ucast_ucast_mask mask_shift_mask_helper) 2464 apply auto[1] 2465 apply clarsimp 2466 apply (frule (1) valid_vspace_objsD, fastforce) 2467 apply clarsimp 2468 apply (drule pde_ref_pde_ref_pagesI) 2469 apply clarsimp 2470 apply (simp add: ucast_ucast_mask mask_shift_mask_helper) 2471 apply (clarsimp simp: pde_ref_pages_def obj_at_def 2472 split: pde.splits) 2473 apply (erule_tac x=d in allE, erule_tac x=q' in allE) 2474 apply (frule (2) ref_is_unique[OF _ vs_lookup_vs_lookup_pagesI]) 2475 apply ((clarsimp simp: invs_def valid_state_def valid_arch_caps_def 2476 valid_arch_state_def)+)[2] 2477 apply (auto dest!: valid_global_ptsD[simplified second_level_tables_def] simp: obj_at_def )[1] 2478 apply (clarsimp simp: data_at_def)+ 2479 apply (rule valid_objs_caps) 2480 apply ((clarsimp elim!: impE)+)[2] 2481 apply (auto simp add: ucast_ucast_mask mask_shift_mask_helper 2482 data_at_def obj_at_def) 2483 done 2484 2485lemma set_cap_empty_pde: 2486 "\<lbrace>empty_pde_at p and cte_at p'\<rbrace> set_cap cap p' \<lbrace>\<lambda>_. empty_pde_at p\<rbrace>" 2487 apply (simp add: empty_pde_at_def) 2488 apply (rule hoare_pre) 2489 apply (wp set_cap_obj_at_other hoare_vcg_ex_lift) 2490 apply clarsimp 2491 apply (rule exI, rule conjI, assumption) 2492 apply (erule conjI) 2493 apply (clarsimp simp: cte_wp_at_cases obj_at_def) 2494 done 2495 2496lemma valid_cap_obj_ref_pt_pd: 2497 "\<lbrakk> s \<turnstile> cap; s \<turnstile> cap'; obj_refs cap = obj_refs cap' \<rbrakk> 2498 \<Longrightarrow> (is_pt_cap cap \<longrightarrow> is_pt_cap cap') 2499 \<and> (is_pd_cap cap \<longrightarrow> is_pd_cap cap')" 2500 by (auto simp: is_cap_simps valid_cap_def 2501 obj_at_def is_ep is_ntfn is_cap_table 2502 is_tcb a_type_def 2503 split: cap.split_asm if_split_asm 2504 arch_cap.split_asm option.split_asm) 2505 2506 2507 2508lemma is_pt_pd_cap_asid_None_table_ref: 2509 "is_pt_cap cap \<or> is_pd_cap cap 2510 \<Longrightarrow> ((table_cap_ref cap = None) = (cap_asid cap = None))" 2511 by (auto simp: is_cap_simps table_cap_ref_def cap_asid_def 2512 split: option.split_asm) 2513 2514lemma no_cap_to_obj_with_diff_ref_map: 2515 "\<lbrakk> caps_of_state s p = Some cap; is_pt_cap cap \<or> is_pd_cap cap; 2516 table_cap_ref cap = None; 2517 unique_table_caps (caps_of_state s); 2518 valid_objs s; obj_refs cap = obj_refs cap' \<rbrakk> 2519 \<Longrightarrow> no_cap_to_obj_with_diff_ref cap' {p} s" 2520 apply (clarsimp simp: no_cap_to_obj_with_diff_ref_def 2521 cte_wp_at_caps_of_state) 2522 apply (frule(1) caps_of_state_valid_cap[where p=p]) 2523 apply (frule(1) caps_of_state_valid_cap[where p="(a, b)" for a b]) 2524 apply (drule(1) valid_cap_obj_ref_pt_pd, simp) 2525 apply (drule(1) unique_table_capsD[rotated, where cps="caps_of_state s"]) 2526 apply simp 2527 apply (simp add: is_pt_pd_cap_asid_None_table_ref) 2528 apply fastforce 2529 apply assumption 2530 apply simp 2531 done 2532 2533 2534lemmas store_pte_cte_wp_at1[wp] 2535 = hoare_cte_wp_caps_of_state_lift [OF store_pte_caps_of_state] 2536 2537lemma mdb_cte_at_store_pte[wp]: 2538 "\<lbrace>\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)\<rbrace> 2539 store_pte y pte 2540 \<lbrace>\<lambda>r s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)\<rbrace>" 2541 apply (clarsimp simp:mdb_cte_at_def) 2542 apply (simp only: imp_conv_disj) 2543 apply (wp hoare_vcg_disj_lift hoare_vcg_all_lift) 2544 apply (simp add:store_pte_def set_pt_def) 2545 apply wp 2546 apply (rule hoare_drop_imp) 2547 apply (wp|simp)+ 2548done 2549 2550lemma valid_idle_store_pte[wp]: 2551 "\<lbrace>valid_idle\<rbrace> store_pte y pte \<lbrace>\<lambda>rv. valid_idle\<rbrace>" 2552 apply (simp add:store_pte_def) 2553 apply wp 2554 apply (rule hoare_vcg_precond_imp[where Q="valid_idle"]) 2555 apply (simp add:set_pt_def) 2556 apply wp 2557 apply (simp add:get_object_def) 2558 apply wp 2559 apply (clarsimp simp:obj_at_def 2560 split:Structures_A.kernel_object.splits arch_kernel_obj.splits) 2561 apply (fastforce simp:is_tcb_def) 2562 apply (assumption) 2563 apply (wp|simp)+ 2564done 2565 2566lemma mapM_swp_store_pte_invs[wp]: 2567 "\<lbrace>invs and (\<lambda>s. (\<exists>p\<in>set slots. (\<exists>\<rhd> (p && ~~ mask pt_bits)) s) \<longrightarrow> 2568 valid_pte pte s) and 2569 (\<lambda>s. wellformed_pte pte) and 2570 (\<lambda>s. \<exists>slot. cte_wp_at 2571 (\<lambda>c. image (\<lambda>x. x && ~~ mask pt_bits) (set slots) \<subseteq> obj_refs c \<and> 2572 is_pt_cap c \<and> (pte = InvalidPTE \<or> 2573 cap_asid c \<noteq> None)) slot s) and 2574 (\<lambda>s. \<forall>p\<in>set slots. \<forall>ref. (ref \<rhd> (p && ~~ mask pt_bits)) s \<longrightarrow> 2575 (\<forall>q. pte_ref_pages pte = Some q \<longrightarrow> 2576 (\<exists>p' cap. 2577 caps_of_state s p' = Some cap \<and> 2578 q \<in> obj_refs cap \<and> 2579 vs_cap_ref cap = 2580 Some 2581 (VSRef (p && mask pt_bits >> 2) (Some APageTable) # 2582 ref))))\<rbrace> 2583 mapM (swp store_pte pte) slots \<lbrace>\<lambda>_. invs\<rbrace>" 2584 apply (rule hoare_post_imp) 2585 prefer 2 2586 apply (rule mapM_wp') 2587 apply simp_all 2588 apply (wp mapM_wp' hoare_vcg_imp_lift hoare_vcg_ex_lift hoare_vcg_ball_lift 2589 hoare_vcg_all_lift hoare_vcg_imp_lift) 2590 apply clarsimp 2591 apply (fastforce simp: cte_wp_at_caps_of_state is_pt_cap_def cap_asid_def) 2592 done 2593 2594lemmas store_pde_cte_wp_at1[wp] 2595 = hoare_cte_wp_caps_of_state_lift [OF store_pde_caps_of_state] 2596 2597crunch global_refs_inv[wp]: store_pde "\<lambda>s. P (global_refs s)" 2598 (wp: get_object_wp) (* added by sjw, something dropped out of some set :( *) 2599 2600lemma mapM_swp_store_pde_invs_unmap: 2601 "\<lbrace>invs and 2602 (\<lambda>s. \<forall>sl\<in>set slots. 2603 ucast (sl && mask pd_bits >> 2) \<notin> kernel_mapping_slots) and 2604 (\<lambda>s. \<forall>sl\<in>set slots. sl && ~~ mask pd_bits \<notin> global_refs s) and 2605 K (pde = InvalidPDE)\<rbrace> 2606 mapM (swp store_pde pde) slots \<lbrace>\<lambda>_. invs\<rbrace>" 2607 apply (rule hoare_post_imp) 2608 prefer 2 2609 apply (rule mapM_wp') 2610 apply simp 2611 apply (rule hoare_pre, wp store_pde_invs_unmap hoare_vcg_const_Ball_lift 2612 hoare_vcg_ex_lift) 2613 apply clarsimp+ 2614 done 2615 2616lemma vs_refs_pdI3: 2617 "\<lbrakk>pde_ref (pd x) = Some p; x \<notin> kernel_mapping_slots\<rbrakk> 2618 \<Longrightarrow> (VSRef (ucast x) (Some APageDirectory), p) \<in> vs_refs (ArchObj (PageDirectory pd))" 2619 by (auto simp: pde_ref_def vs_refs_def graph_of_def) 2620 2621 2622lemma set_pd_invs_unmap': 2623 "\<lbrace>invs and (\<lambda>s. \<forall>i. wellformed_pde (pd i)) and 2624 (\<lambda>s. (\<exists>\<rhd>p) s \<longrightarrow> valid_vspace_obj (PageDirectory pd) s) and 2625 obj_at (\<lambda>ko. vs_refs (ArchObj (PageDirectory pd)) = vs_refs ko - T) p and 2626 obj_at (\<lambda>ko. vs_refs_pages (ArchObj (PageDirectory pd)) = vs_refs_pages ko - T' \<union> S') p and 2627 obj_at (\<lambda>ko. \<exists>pd'. ko = ArchObj (PageDirectory pd') 2628 \<and> (\<forall>x \<in> kernel_mapping_slots. pd x = pd' x)) p and 2629 (\<lambda>s. p \<notin> global_refs s) and 2630 (\<lambda>s. \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> 2631 is_pd_cap cap \<and> 2632 p \<in> obj_refs cap \<and> (\<exists>y. cap_asid cap = Some y)) and 2633 (\<lambda>s. \<forall>(a,b)\<in>S'. (\<forall>ref. 2634 (ref \<unrhd> p) s \<longrightarrow> 2635 (\<exists>p' cap. 2636 caps_of_state s p' = Some cap \<and> 2637 b \<in> obj_refs cap \<and> vs_cap_ref cap = Some (a # ref))))\<rbrace> 2638 set_pd p pd 2639 \<lbrace>\<lambda>_. invs\<rbrace>" 2640 apply (simp add: invs_def valid_state_def valid_pspace_def valid_arch_caps_def) 2641 apply (rule hoare_pre) 2642 apply (wp set_pd_valid_objs set_pd_iflive set_pd_zombies 2643 set_pd_zombies_state_refs set_pd_valid_mdb 2644 set_pd_zombies_state_hyp_refs 2645 set_pd_valid_idle set_pd_ifunsafe set_pd_reply_caps 2646 set_pd_valid_arch set_pd_valid_global set_pd_cur 2647 set_pd_reply_masters valid_irq_node_typ 2648 set_pd_vspace_objs_unmap set_pd_valid_vs_lookup_map[where T=T and S="{}" and T'=T' and S'=S'] 2649 valid_irq_handlers_lift 2650 set_pd_unmap_mappings set_pd_equal_kernel_mappings_triv) 2651 apply (clarsimp simp: cte_wp_at_caps_of_state valid_arch_caps_def valid_objs_caps obj_at_def 2652 del: disjCI) 2653 apply (rule conjI, clarsimp) 2654 apply (rule conjI) 2655 apply clarsimp 2656 apply (erule_tac x="(VSRef (ucast c) (Some APageDirectory), q)" in ballE) 2657 apply clarsimp 2658 apply (frule (1) vs_refs_pages_pdI) 2659 apply (clarsimp simp: valid_arch_caps_def) 2660 apply (drule_tac p'=q and ref'="VSRef (ucast c) (Some APageDirectory) # r" in vs_lookup_pages_step) 2661 apply (clarsimp simp: vs_lookup_pages1_def obj_at_def) 2662 apply (drule (1) valid_vs_lookupD) 2663 apply (clarsimp) 2664 apply (rule conjI) 2665 apply clarsimp 2666 apply (drule (1) vs_refs_pdI3) 2667 apply clarsimp 2668 apply (drule_tac p'=q and ref'="VSRef (ucast c) (Some APageDirectory) # r" in vs_lookup_pages_step) 2669 apply (clarsimp simp: vs_lookup_pages1_def obj_at_def) 2670 apply (erule subsetD[OF vs_refs_pages_subset]) 2671 apply (drule_tac p'=q' and ref'="VSRef (ucast d) (Some APageTable) # VSRef (ucast c) (Some APageDirectory) # r" 2672 in vs_lookup_pages_step) 2673 apply (clarsimp simp: vs_lookup_pages1_def obj_at_def) 2674 apply (erule pte_ref_pagesD) 2675 apply (drule (1) valid_vs_lookupD) 2676 apply clarsimp 2677 apply auto 2678 done 2679 2680lemma same_refs_lD: 2681 "\<lbrakk>same_refs (Inl(pte,p # slots)) cap s\<rbrakk> 2682 \<Longrightarrow> (\<exists>p. pte_ref_pages pte = Some p \<and> p \<in> obj_refs cap) \<and> 2683 (\<forall>ref. (ref \<rhd> (p && ~~ mask pt_bits)) s \<longrightarrow> 2684 vs_cap_ref cap = Some (VSRef (p && mask pt_bits >> 2) (Some APageTable) # ref))" 2685 by (clarsimp simp:same_refs_def split:list.splits) 2686 2687lemma same_refs_rD: 2688 "\<lbrakk>same_refs (Inr(pde,p # slots)) cap s\<rbrakk> 2689 \<Longrightarrow> (\<exists>p. pde_ref_pages pde = Some p \<and> p \<in> obj_refs cap) \<and> 2690 (\<forall>ref. (ref \<rhd> (p && ~~ mask pd_bits)) s \<longrightarrow> 2691 vs_cap_ref cap = 2692 Some (VSRef (p && mask pd_bits >> 2) (Some APageDirectory) # ref))" 2693 by (clarsimp simp:same_refs_def split:list.splits) 2694 2695lemma store_pde_invs_unmap': 2696 "\<lbrace>invs 2697 and (\<exists>\<rhd> (p && ~~ mask pd_bits)) 2698 and (\<lambda>s. \<exists>slot. cte_wp_at (parent_for_refs (Inr (pde, slots))) slot s) 2699 and (\<lambda>s. \<exists>ptr cap. caps_of_state s ptr = Some cap 2700 \<and> is_pg_cap cap 2701 \<and> same_refs (Inr (pde, slots)) cap s) 2702 and valid_pde pde 2703 and (\<lambda>s. p && ~~ mask pd_bits \<notin> global_refs s) 2704 and K (wellformed_pde pde \<and> pde_ref pde = None) 2705 and K (ucast (p && mask pd_bits >> 2) \<notin> kernel_mapping_slots 2706 \<and> (\<exists>xs. slots = p # xs) ) 2707 and (\<lambda>s. \<exists>pd. ko_at (ArchObj (PageDirectory pd)) (p && ~~ mask pd_bits) s)\<rbrace> 2708 store_pde p pde 2709 \<lbrace>\<lambda>_. invs\<rbrace>" 2710 apply (rule hoare_name_pre_state) 2711 apply (clarsimp simp: store_pde_def | wp)+ 2712 apply (rule_tac T =" Pair (VSRef (p && mask pd_bits >> 2) (Some APageDirectory)) 2713 ` set_option (pde_ref (pd (ucast (p && mask pd_bits >> 2))))" 2714 and T'=" Pair (VSRef (p && mask pd_bits >> 2) (Some APageDirectory)) 2715 ` set_option (pde_ref_pages (pd (ucast (p && mask pd_bits >> 2))))" 2716 and S'=" Pair (VSRef (p && mask pd_bits >> 2) (Some APageDirectory)) 2717 ` set_option (pde_ref_pages pde)" in set_pd_invs_unmap') 2718 apply wp 2719 apply (clarsimp simp: obj_at_def) 2720 apply (rule conjI) 2721 apply (clarsimp simp add: invs_def valid_state_def valid_pspace_def 2722 valid_objs_def valid_obj_def dom_def) 2723 apply (erule_tac P="\<lambda>x. (\<exists>y. a y x) \<longrightarrow> b x" for a b in allE[where x="(p && ~~ mask pd_bits)"]) 2724 apply (erule impE) 2725 apply (clarsimp simp: obj_at_def vs_refs_def)+ 2726 2727 apply (rule conjI) 2728 apply (clarsimp simp add: invs_def valid_state_def valid_vspace_objs_def) 2729 apply (erule_tac P="\<lambda>x. (\<exists>y. a y x) \<longrightarrow> b x" for a b in allE[where x="(p && ~~ mask pd_bits)"]) 2730 apply (erule impE) 2731 apply (erule_tac x=ref in exI) 2732 apply (erule_tac x="PageDirectory pd" in allE) 2733 apply (clarsimp simp: obj_at_def) 2734 2735 apply (rule conjI) 2736 apply (safe)[1] 2737 apply (clarsimp simp add: vs_refs_def graph_of_def split: if_split_asm) 2738 apply (rule pair_imageI) 2739 apply (clarsimp) 2740 apply (clarsimp simp: vs_refs_def graph_of_def split: if_split_asm) 2741 apply (subst (asm) ucast_ucast_mask_shift_helper[symmetric], simp) 2742 apply (clarsimp simp: vs_refs_def graph_of_def split: if_split_asm) 2743 apply (rule_tac x="(ac, bc)" in image_eqI) 2744 apply clarsimp 2745 apply (clarsimp simp: ucast_ucast_mask_shift_helper ucast_id) 2746 2747 apply (rule conjI) 2748 apply safe[1] 2749 apply (clarsimp simp: vs_refs_pages_def graph_of_def 2750 ucast_ucast_mask_shift_helper ucast_id 2751 split: if_split_asm) 2752 apply (rule_tac x="(ac, bc)" in image_eqI) 2753 apply clarsimp 2754 apply clarsimp 2755 apply (clarsimp simp: vs_refs_pages_def graph_of_def ucast_ucast_id 2756 split: if_split_asm) 2757 apply (clarsimp simp: vs_refs_pages_def graph_of_def 2758 split: if_split_asm) 2759 apply (rule_tac x="(ac,bc)" in image_eqI) 2760 apply clarsimp 2761 apply (clarsimp simp: ucast_ucast_mask_shift_helper ucast_id) 2762 apply (clarsimp simp: vs_refs_pages_def graph_of_def) 2763 apply (rule_tac x="(ucast (p && mask pd_bits >> 2), x)" in image_eqI) 2764 apply (clarsimp simp: ucast_ucast_mask_shift_helper) 2765 apply clarsimp 2766 apply (rule conjI) 2767 apply (clarsimp simp: cte_wp_at_caps_of_state parent_for_refs_def) 2768 apply (drule same_refs_rD) 2769 apply (clarsimp split: list.splits) 2770 apply blast 2771 apply (drule same_refs_rD) 2772 apply clarsimp 2773 apply (drule spec, drule (2) mp[OF _ vs_lookup_vs_lookup_pagesI]) 2774 apply ((clarsimp simp: invs_def valid_state_def valid_arch_state_def)+)[2] 2775 apply (rule_tac x=aa in exI, rule_tac x=ba in exI, rule_tac x=cap in exI) 2776 apply clarsimp 2777 done 2778 2779lemma update_self_reachable: 2780 "\<lbrakk>(ref \<rhd> p) s; valid_asid_table (arm_asid_table (arch_state s)) s; 2781 valid_vspace_objs s\<rbrakk> 2782 \<Longrightarrow> (ref \<rhd> p) (s \<lparr>kheap := \<lambda>a. if a = p then Some y else kheap s a\<rparr>)" 2783 apply (erule (2) vs_lookupE_alt[OF _ _ valid_asid_table_ran]) 2784 apply (rule vs_lookup_atI, clarsimp) 2785 apply (rule_tac ap=ap in vs_lookup_apI, auto simp: obj_at_def)[1] 2786 apply (clarsimp simp: pde_ref_def split: pde.splits) 2787 apply (rule_tac ap=ap and pd=pd in vs_lookup_pdI, auto simp: obj_at_def)[1] 2788 done 2789 2790lemma update_self_reachable_pages: 2791 "\<lbrakk>(ref \<unrhd> p) s; valid_asid_table (arm_asid_table (arch_state s)) s; 2792 valid_vspace_objs s\<rbrakk> 2793 \<Longrightarrow> (ref \<unrhd> p) (s \<lparr>kheap := \<lambda>a. if a = p then Some y else kheap s a\<rparr>)" 2794 apply (erule (2) vs_lookup_pagesE_alt[OF _ _ valid_asid_table_ran]) 2795 apply (rule vs_lookup_pages_atI, clarsimp) 2796 apply (rule_tac ap=ap in vs_lookup_pages_apI, auto simp: obj_at_def)[1] 2797 apply (rule_tac ap=ap and pd=pd in vs_lookup_pages_pdI, 2798 auto simp: obj_at_def pde_ref_pages_def data_at_def 2799 split: pde.splits)[1] 2800 apply (rule_tac ap=ap and pd=pd in vs_lookup_pages_ptI, 2801 auto simp: obj_at_def pde_ref_pages_def pte_ref_pages_def data_at_def 2802 split: pde.splits pte.splits)[1] 2803 done 2804 2805 2806lemma pd_slots_helper: 2807 "\<lbrakk>a \<in> set slots; b \<in> set slots; 2808 cte_wp_at (parent_for_refs (Inr (pde, slots))) cptr s\<rbrakk> 2809 \<Longrightarrow> a && ~~ mask pd_bits = b && ~~ mask pd_bits" 2810 apply (clarsimp simp add: cte_wp_at_def parent_for_refs_def) 2811 apply (drule imageI[where f="\<lambda>x. x && ~~ mask pd_bits"]) 2812 apply (drule imageI[where f="\<lambda>x. x && ~~ mask pd_bits"]) 2813 apply (simp add: obj_refs_def) 2814 apply (case_tac cap, simp+) 2815 apply (rename_tac arch_cap) 2816 apply (case_tac arch_cap, simp+) 2817 apply (drule (1) set_rev_mp) 2818 apply (drule (1) set_rev_mp) 2819 apply force 2820 apply (drule (1) set_rev_mp) 2821 apply (drule (1) set_rev_mp) 2822 apply force 2823 apply (drule (1) set_rev_mp) 2824 apply (drule (1) set_rev_mp) 2825 apply force 2826 done 2827 2828(* FIXME: move *) 2829lemma simpler_store_pde_def: 2830 "store_pde p pde s = 2831 (case kheap s (p && ~~ mask pd_bits) of 2832 Some (ArchObj (PageDirectory pd)) => 2833 ({((), s\<lparr>kheap := (kheap s((p && ~~ mask pd_bits) \<mapsto> 2834 (ArchObj (PageDirectory (pd(ucast (p && mask pd_bits >> 2) := pde))))))\<rparr>)}, False) 2835 | _ => ({}, True))" 2836 apply (auto simp: store_pde_def simpler_set_pd_def get_object_def simpler_gets_def assert_def 2837 return_def fail_def set_object_def get_def put_def bind_def get_pd_def 2838 split: Structures_A.kernel_object.splits option.splits arch_kernel_obj.splits if_split_asm) 2839 done 2840 2841lemma pde_update_valid_vspace_objs: 2842 "[|valid_vspace_objs s; valid_pde pde s; pde_ref pde = None; kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd))|] 2843 ==> valid_vspace_objs 2844 (s\<lparr>kheap := kheap s(p && ~~ mask pd_bits \<mapsto> ArchObj (PageDirectory (pd(ucast (p && mask pd_bits >> 2) := pde))))\<rparr>)" 2845 apply (cut_tac pde=pde and p=p in store_pde_vspace_objs_unmap) 2846 apply (clarsimp simp: valid_def) 2847 apply (erule allE[where x=s]) 2848 apply (clarsimp simp: split_def simpler_store_pde_def obj_at_def a_type_def 2849 split: if_split_asm option.splits Structures_A.kernel_object.splits 2850 arch_kernel_obj.splits) 2851 done 2852 2853lemma mapM_x_swp_store_pte_invs [wp]: 2854 "\<lbrace>invs and (\<lambda>s. (\<exists>p\<in>set slots. (\<exists>\<rhd> (p && ~~ mask pt_bits)) s) \<longrightarrow> 2855 valid_pte pte s) and 2856 (\<lambda>s. wellformed_pte pte) and 2857 (\<lambda>s. \<exists>slot. cte_wp_at 2858 (\<lambda>c. image (\<lambda>x. x && ~~ mask pt_bits) (set slots) \<subseteq> obj_refs c \<and> 2859 is_pt_cap c \<and> (pte = InvalidPTE \<or> 2860 cap_asid c \<noteq> None)) slot s) and 2861 (\<lambda>s. \<forall>p\<in>set slots. \<forall>ref. (ref \<rhd> (p && ~~ mask pt_bits)) s \<longrightarrow> 2862 (\<forall>q. pte_ref_pages pte = Some q \<longrightarrow> 2863 (\<exists>p' cap. 2864 caps_of_state s p' = Some cap \<and> 2865 q \<in> obj_refs cap \<and> 2866 vs_cap_ref cap = 2867 Some 2868 (VSRef (p && mask pt_bits >> 2) (Some APageTable) # 2869 ref))))\<rbrace> 2870 mapM_x (swp store_pte pte) slots \<lbrace>\<lambda>_. invs\<rbrace>" 2871 by (simp add: mapM_x_mapM | wp)+ 2872 2873lemma mapM_x_swp_store_pde_invs_unmap: 2874 "\<lbrace>invs and K (\<forall>sl\<in>set slots. 2875 ucast (sl && mask pd_bits >> 2) \<notin> kernel_mapping_slots) and 2876 (\<lambda>s. \<forall>sl \<in> set slots. sl && ~~ mask pd_bits \<notin> global_refs s) and 2877 K (pde = InvalidPDE)\<rbrace> 2878 mapM_x (swp store_pde pde) slots \<lbrace>\<lambda>_. invs\<rbrace>" 2879 by (simp add: mapM_x_mapM | wp mapM_swp_store_pde_invs_unmap)+ 2880 2881(* FIXME: move *) 2882lemma vs_cap_ref_table_cap_ref_None: 2883 "vs_cap_ref x = None \<Longrightarrow> table_cap_ref x = None" 2884 by (simp add: vs_cap_ref_def table_cap_ref_simps 2885 split: cap.splits arch_cap.splits) 2886 2887(* FIXME: move *) 2888lemma master_cap_eq_is_pg_cap_eq: 2889 "cap_master_cap c = cap_master_cap d \<Longrightarrow> is_pg_cap c = is_pg_cap d" 2890 by (simp add: cap_master_cap_def is_pg_cap_def 2891 split: cap.splits arch_cap.splits) 2892 2893(* FIXME: move *) 2894lemma master_cap_eq_is_device_cap_eq: 2895 "cap_master_cap c = cap_master_cap d \<Longrightarrow> cap_is_device c = cap_is_device d" 2896 by (simp add: cap_master_cap_def 2897 split: cap.splits arch_cap.splits) 2898 2899(* FIXME: move *) 2900lemmas vs_cap_ref_eq_imp_table_cap_ref_eq' = 2901 vs_cap_ref_eq_imp_table_cap_ref_eq[OF master_cap_eq_is_pg_cap_eq] 2902 2903lemma arch_update_cap_invs_map: 2904 "\<lbrace>cte_wp_at (is_arch_update cap and 2905 (\<lambda>c. \<forall>r. vs_cap_ref c = Some r \<longrightarrow> vs_cap_ref cap = Some r)) p 2906 and invs and valid_cap cap\<rbrace> 2907 set_cap cap p 2908 \<lbrace>\<lambda>rv. invs\<rbrace>" 2909 apply (simp add: invs_def valid_state_def) 2910 apply (rule hoare_pre) 2911 apply (wp arch_update_cap_pspace arch_update_cap_valid_mdb set_cap_idle 2912 update_cap_ifunsafe valid_irq_node_typ set_cap_typ_at 2913 set_cap_irq_handlers set_cap_valid_arch_caps 2914 set_cap_cap_refs_respects_device_region_spec[where ptr = p]) 2915 apply (clarsimp simp: cte_wp_at_caps_of_state 2916 simp del: imp_disjL) 2917 apply (frule(1) valid_global_refsD2) 2918 apply (frule(1) cap_refs_in_kernel_windowD) 2919 apply (clarsimp simp: is_cap_simps is_arch_update_def 2920 simp del: imp_disjL) 2921 apply (frule master_cap_cap_range, simp del: imp_disjL) 2922 apply (thin_tac "cap_range a = cap_range b" for a b) 2923 apply (rule conjI) 2924 apply (rule ext) 2925 apply (simp add: cap_master_cap_def split: cap.splits arch_cap.splits) 2926 apply (rule context_conjI) 2927 apply (simp add: appropriate_cte_cap_irqs) 2928 apply (clarsimp simp: cap_irqs_def cap_irq_opt_def cap_master_cap_def 2929 split: cap.split) 2930 apply (rule conjI) 2931 apply (drule(1) if_unsafe_then_capD [OF caps_of_state_cteD]) 2932 apply (clarsimp simp: cap_master_cap_def) 2933 apply (erule ex_cte_cap_wp_to_weakenE) 2934 apply (clarsimp simp: appropriate_cte_cap_def cap_master_cap_def 2935 split: cap.split_asm) 2936 apply (rule conjI) 2937 apply (frule master_cap_obj_refs) 2938 apply simp 2939 apply (rule conjI) 2940 apply (frule master_cap_obj_refs) 2941 apply (case_tac "table_cap_ref capa = 2942 table_cap_ref (ArchObjectCap a)") 2943 apply (frule unique_table_refs_no_cap_asidE[where S="{p}"]) 2944 apply (simp add: valid_arch_caps_def) 2945 apply (simp add: no_cap_to_obj_with_diff_ref_def Ball_def) 2946 apply (case_tac "table_cap_ref capa") 2947 apply clarsimp 2948 apply (erule no_cap_to_obj_with_diff_ref_map, 2949 simp_all)[1] 2950 apply (clarsimp simp: table_cap_ref_def cap_master_cap_simps 2951 is_cap_simps 2952 split: cap.split_asm arch_cap.split_asm 2953 dest!: cap_master_cap_eqDs) 2954 apply (simp add: valid_arch_caps_def) 2955 apply (simp add: valid_pspace_def) 2956 apply (erule swap) 2957 apply (erule vs_cap_ref_eq_imp_table_cap_ref_eq'[symmetric]) 2958 apply (frule table_cap_ref_vs_cap_ref_Some) 2959 apply simp 2960 apply (rule conjI) 2961 apply (clarsimp simp del: imp_disjL) 2962 apply (erule disjE) 2963 apply (clarsimp simp: is_pt_cap_def cap_master_cap_simps 2964 cap_asid_def vs_cap_ref_def 2965 dest!: cap_master_cap_eqDs split: option.split_asm prod.split_asm) 2966 apply (drule valid_table_capsD[OF caps_of_state_cteD]) 2967 apply (clarsimp simp: invs_def valid_state_def valid_arch_caps_def) 2968 apply (simp add: is_pt_cap_def) 2969 apply (simp add: cap_asid_def) 2970 apply simp 2971 apply (clarsimp simp: is_cap_simps cap_master_cap_simps 2972 cap_asid_def vs_cap_ref_def 2973 dest!: cap_master_cap_eqDs split: option.split_asm prod.split_asm) 2974 apply (drule valid_table_capsD[OF caps_of_state_cteD]) 2975 apply (clarsimp simp: invs_def valid_state_def valid_arch_caps_def) 2976 apply (simp add: is_cap_simps) 2977 apply (simp add: cap_asid_def) 2978 apply simp 2979 apply (clarsimp simp: is_cap_simps is_pt_cap_def cap_master_cap_simps 2980 cap_asid_def vs_cap_ref_def ranI 2981 dest!: cap_master_cap_eqDs split: option.split_asm if_split_asm 2982 elim!: ranE cong: master_cap_eq_is_device_cap_eq 2983 | rule conjI)+ 2984 apply (clarsimp dest!: master_cap_eq_is_device_cap_eq) 2985 2986 done 2987 2988 (* Want something like 2989 cte_wp_at (\<lambda>c. \<forall>p'\<in>obj_refs c. \<not>(vs_cap_ref c \<unrhd> p') s \<and> is_arch_update cap c) p 2990 So that we know the new cap isn't clobbering a cap with necessary mapping info. 2991 invs is fine here (I suspect) because we unmap the page BEFORE we replace the cap. 2992 *) 2993 2994lemma arch_update_cap_invs_unmap_page: 2995 "\<lbrace>(\<lambda>s. cte_wp_at (\<lambda>c. (\<forall>p'\<in>obj_refs c. \<forall>ref. vs_cap_ref c = Some ref \<longrightarrow> \<not> (ref \<unrhd> p') s) \<and> is_arch_update cap c) p s) 2996 and invs and valid_cap cap 2997 and K (is_pg_cap cap)\<rbrace> 2998 set_cap cap p 2999 \<lbrace>\<lambda>rv. invs\<rbrace>" 3000 apply (simp add: invs_def valid_state_def) 3001 apply (rule hoare_pre) 3002 apply (wp arch_update_cap_pspace arch_update_cap_valid_mdb set_cap_idle 3003 update_cap_ifunsafe valid_irq_node_typ set_cap_typ_at 3004 set_cap_irq_handlers set_cap_valid_arch_caps 3005 set_cap_cap_refs_respects_device_region_spec[where ptr = p]) 3006 apply clarsimp 3007 apply (clarsimp simp: cte_wp_at_caps_of_state is_arch_update_def 3008 is_cap_simps cap_master_cap_simps 3009 fun_eq_iff appropriate_cte_cap_irqs 3010 is_pt_cap_def 3011 dest!: cap_master_cap_eqDs 3012 simp del: imp_disjL) 3013 apply (rule conjI) 3014 apply (drule(1) if_unsafe_then_capD [OF caps_of_state_cteD]) 3015 apply (clarsimp simp: cap_master_cap_def) 3016 apply (erule ex_cte_cap_wp_to_weakenE) 3017 apply (clarsimp simp: appropriate_cte_cap_def) 3018 apply (rule conjI) 3019 apply (drule valid_global_refsD2, clarsimp) 3020 subgoal by (simp add: cap_range_def) 3021 apply (rule conjI[rotated]) 3022 apply (frule(1) cap_refs_in_kernel_windowD) 3023 apply (simp add: cap_range_def) 3024 apply (drule unique_table_refs_no_cap_asidE[where S="{p}"]) 3025 apply (simp add: valid_arch_caps_def) 3026 apply (simp add: no_cap_to_obj_with_diff_ref_def table_cap_ref_def Ball_def) 3027 done 3028 3029lemma arch_update_cap_invs_unmap_page_table: 3030 "\<lbrace>cte_wp_at (is_arch_update cap) p 3031 and invs and valid_cap cap 3032 and (\<lambda>s. cte_wp_at (\<lambda>c. is_final_cap' c s) p s) 3033 and obj_at (empty_table {}) (obj_ref_of cap) 3034 and (\<lambda>s. cte_wp_at (\<lambda>c. \<forall>r. vs_cap_ref c = Some r 3035 \<longrightarrow> \<not> (r \<unrhd> obj_ref_of cap) s) p s) 3036 and K (is_pt_cap cap \<and> vs_cap_ref cap = None)\<rbrace> 3037 set_cap cap p 3038 \<lbrace>\<lambda>rv. invs\<rbrace>" 3039 apply (simp add: invs_def valid_state_def) 3040 apply (rule hoare_pre) 3041 apply (wp arch_update_cap_pspace arch_update_cap_valid_mdb set_cap_idle 3042 update_cap_ifunsafe valid_irq_node_typ set_cap_typ_at 3043 set_cap_irq_handlers set_cap_valid_arch_caps 3044 set_cap_cap_refs_respects_device_region_spec[where ptr = p]) 3045 apply (simp add: final_cap_at_eq) 3046 apply (clarsimp simp: cte_wp_at_caps_of_state is_arch_update_def 3047 is_cap_simps cap_master_cap_simps 3048 appropriate_cte_cap_irqs is_pt_cap_def 3049 fun_eq_iff[where f="cte_refs cap" for cap] 3050 dest!: cap_master_cap_eqDs 3051 simp del: imp_disjL) 3052 apply (rule conjI) 3053 apply (drule(1) if_unsafe_then_capD [OF caps_of_state_cteD]) 3054 apply (clarsimp simp: cap_master_cap_def) 3055 apply (erule ex_cte_cap_wp_to_weakenE) 3056 apply (clarsimp simp: appropriate_cte_cap_def) 3057 apply (rule conjI) 3058 apply (drule valid_global_refsD2, clarsimp) 3059 apply (simp add: cap_range_def) 3060 apply (frule(1) cap_refs_in_kernel_windowD) 3061 apply (simp add: cap_range_def gen_obj_refs_def image_def) 3062 apply (intro conjI) 3063 apply (clarsimp simp: no_cap_to_obj_with_diff_ref_def 3064 cte_wp_at_caps_of_state) 3065 apply fastforce 3066 apply (clarsimp simp: obj_at_def empty_table_def) 3067 apply (clarsimp split: Structures_A.kernel_object.split_asm 3068 arch_kernel_obj.split_asm) 3069 apply clarsimp 3070 apply fastforce 3071 done 3072 3073lemma set_vm_root_for_flush_invs: 3074 "\<lbrace>invs and K (asid \<le> mask asid_bits)\<rbrace> 3075 set_vm_root_for_flush pd asid \<lbrace>\<lambda>_. invs\<rbrace>" 3076 apply (simp add: set_vm_root_for_flush_def) 3077 apply (wp hoare_drop_imps hoare_vcg_all_lift |wpc|simp)+ 3078 done 3079 3080lemma flush_table_invs[wp]: 3081 "\<lbrace>invs and K (asid \<le> mask asid_bits)\<rbrace> 3082 flush_table pd asid vptr pt \<lbrace>\<lambda>rv. invs\<rbrace>" 3083 apply (simp add: flush_table_def) 3084 apply (wp dmo_invalidateLocalTLB_ASID_invs | simp)+ 3085 apply (simp only: if_cancel 3086 | clarsimp simp: machine_op_lift_def 3087 machine_rest_lift_def split_def 3088 | wp set_vm_root_for_flush_invs)+ 3089 done 3090 3091crunch vs_lookup[wp]: flush_table "\<lambda>s. P (vs_lookup s)" 3092 (wp: crunch_wps simp: crunch_simps) 3093 3094crunch cte_wp_at[wp]: flush_table "\<lambda>s. P (cte_wp_at P' p s)" 3095 (wp: crunch_wps simp: crunch_simps) 3096 3097lemma global_refs_arch_update_eq: 3098 "\<lbrakk> arm_globals_frame (f (arch_state s)) = arm_globals_frame (arch_state s); 3099 arm_global_pd (f (arch_state s)) = arm_global_pd (arch_state s); 3100 arm_global_pts (f (arch_state s)) = arm_global_pts (arch_state s) \<rbrakk> 3101 \<Longrightarrow> global_refs (arch_state_update f s) = global_refs s" 3102 by (simp add: global_refs_def) 3103 3104crunch global_refs_inv[wp]: flush_table "\<lambda>s. P (global_refs s)" 3105 (wp: crunch_wps simp: crunch_simps global_refs_arch_update_eq) 3106 3107lemma lookup_pd_slot_kernel_mappings_strg: 3108 "is_aligned pd pd_bits \<and> vptr < kernel_base 3109 \<and> vmsz_aligned vptr ARMSection 3110 \<longrightarrow> ucast (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots" 3111 by (simp add: less_kernel_base_mapping_slots) 3112 3113lemma not_in_global_refs_vs_lookup: 3114 "(\<exists>\<rhd> p) s \<and> valid_vs_lookup s \<and> valid_global_refs s 3115 \<and> valid_arch_state s \<and> valid_global_objs s 3116 \<and> page_directory_at p s 3117 \<longrightarrow> p \<notin> global_refs s" 3118 apply (clarsimp dest!: valid_vs_lookupD[OF vs_lookup_pages_vs_lookupI]) 3119 apply (drule(1) valid_global_refsD2) 3120 apply (simp add: cap_range_def) 3121 apply blast 3122 done 3123 3124lemma cleanByVA_PoU_underlying_memory[wp]: 3125 "\<lbrace>\<lambda>m'. underlying_memory m' p = um\<rbrace> cleanByVA_PoU w q \<lbrace>\<lambda>_ m'. underlying_memory m' p = um\<rbrace>" 3126 by (clarsimp simp: cleanByVA_PoU_def machine_op_lift_def machine_rest_lift_def split_def | wp)+ 3127 3128lemma unmap_page_table_invs[wp]: 3129 "\<lbrace>invs and K (asid \<le> mask asid_bits \<and> vaddr < kernel_base 3130 \<and> vmsz_aligned vaddr ARMSection)\<rbrace> 3131 unmap_page_table asid vaddr pt 3132 \<lbrace>\<lambda>rv. invs\<rbrace>" 3133 apply (simp add: unmap_page_table_def) 3134 apply (rule hoare_pre) 3135 apply (wp dmo_invs | wpc | simp)+ 3136 apply (rule_tac Q="\<lambda>_. invs and K (asid \<le> mask asid_bits)" in hoare_post_imp) 3137 apply safe 3138 apply (drule_tac Q="\<lambda>_ m'. underlying_memory m' p = 3139 underlying_memory m p" in use_valid) 3140 apply ((wp | simp)+)[3] 3141 apply(erule use_valid, wp no_irq_cleanByVA_PoU no_irq, assumption) 3142 apply (wp store_pde_invs_unmap page_table_mapped_wp | wpc | simp)+ 3143 apply (simp add: lookup_pd_slot_pd pde_ref_def) 3144 apply (strengthen lookup_pd_slot_kernel_mappings_strg 3145 not_in_global_refs_vs_lookup) 3146 apply (auto simp: vspace_at_asid_def) 3147 done 3148 3149lemma final_cap_lift: 3150 assumes x: "\<And>P. \<lbrace>\<lambda>s. P (caps_of_state s)\<rbrace> f \<lbrace>\<lambda>rv s. P (caps_of_state s)\<rbrace>" 3151 shows "\<lbrace>\<lambda>s. P (is_final_cap' cap s)\<rbrace> f \<lbrace>\<lambda>rv s. P (is_final_cap' cap s)\<rbrace>" 3152 by (simp add: is_final_cap'_def2 cte_wp_at_caps_of_state, rule x) 3153 3154lemmas dmo_final_cap[wp] = final_cap_lift [OF do_machine_op_caps_of_state] 3155lemmas store_pte_final_cap[wp] = final_cap_lift [OF store_pte_caps_of_state] 3156lemmas unmap_page_table_final_cap[wp] = final_cap_lift [OF unmap_page_table_caps_of_state] 3157 3158lemma mapM_x_swp_store_empty_table': 3159 "\<lbrace>obj_at (\<lambda>ko. \<exists>pt. ko = ArchObj (PageTable pt) 3160 \<and> (\<forall>x. x \<in> (\<lambda>sl. ucast ((sl && mask pt_bits) >> 2)) ` set slots 3161 \<or> pt x = InvalidPTE)) p 3162 and K (is_aligned p pt_bits \<and> (\<forall>x \<in> set slots. x && ~~ mask pt_bits = p))\<rbrace> 3163 mapM_x (swp store_pte InvalidPTE) slots 3164 \<lbrace>\<lambda>rv. obj_at (empty_table {}) p\<rbrace>" 3165 apply (rule hoare_gen_asm) 3166 apply (induct slots, simp_all add: mapM_x_Nil mapM_x_Cons) 3167 apply wp 3168 apply (clarsimp simp: obj_at_def empty_table_def fun_eq_iff) 3169 apply (rule hoare_seq_ext, assumption) 3170 apply (thin_tac "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>" for P f Q) 3171 apply (simp add: store_pte_def set_pt_def set_object_def) 3172 apply (wp get_object_wp) 3173 apply (clarsimp simp: obj_at_def) 3174 apply auto 3175 done 3176 3177lemma mapM_x_swp_store_empty_table: 3178 "\<lbrace>page_table_at p and pspace_aligned 3179 and K ((UNIV :: word8 set) \<subseteq> (\<lambda>sl. ucast ((sl && mask pt_bits) >> 2)) ` set slots 3180 \<and> (\<forall>x\<in>set slots. x && ~~ mask pt_bits = p))\<rbrace> 3181 mapM_x (swp store_pte InvalidPTE) slots 3182 \<lbrace>\<lambda>rv. obj_at (empty_table {}) p\<rbrace>" 3183 apply (wp mapM_x_swp_store_empty_table') 3184 apply (clarsimp simp: obj_at_def a_type_def) 3185 apply (clarsimp split: Structures_A.kernel_object.split_asm 3186 arch_kernel_obj.split_asm if_split_asm) 3187 apply (frule(1) pspace_alignedD) 3188 apply (clarsimp simp: pt_bits_def pageBits_def) 3189 apply blast 3190 done 3191 3192lemma pd_shifting_again: 3193 "\<lbrakk> is_aligned pd pd_bits \<rbrakk> 3194 \<Longrightarrow> pd + (ucast (ae :: 12 word) << 2) && ~~ mask pd_bits = pd" 3195 apply (erule add_mask_lower_bits) 3196 apply (clarsimp simp add: nth_shiftl nth_ucast word_size 3197 pd_bits_def pageBits_def 3198 dest!: test_bit_size) 3199 apply arith 3200 done 3201 3202lemma pd_shifting_again2: 3203 "is_aligned (pd::word32) pd_bits \<Longrightarrow> 3204 pd + (ucast (ae::12 word) << 2) && mask pd_bits = (ucast ae << 2)" 3205 apply (rule conjunct1, erule is_aligned_add_helper) 3206 apply (rule ucast_less_shiftl_helper) 3207 apply (simp add: word_bits_def) 3208 apply (simp add: pd_bits_def pageBits_def) 3209 done 3210 3211(* FIXME: move near Invariants_A.vs_lookup_2ConsD *) 3212lemma vs_lookup_pages_2ConsD: 3213 "((v # v' # vs) \<unrhd> p) s \<Longrightarrow> 3214 \<exists>p'. ((v' # vs) \<unrhd> p') s \<and> ((v' # vs, p') \<unrhd>1 (v # v' # vs, p)) s" 3215 apply (clarsimp simp: vs_lookup_pages_def) 3216 apply (erule rtranclE) 3217 apply (clarsimp simp: vs_asid_refs_def) 3218 apply (fastforce simp: vs_lookup_pages1_def) 3219 done 3220 3221(* FIXME: move to Invariants_A *) 3222lemma vs_lookup_pages_eq_at: 3223 "[VSRef a None] \<rhd> pd = [VSRef a None] \<unrhd> pd" 3224 apply (simp add: vs_lookup_pages_def vs_lookup_def Image_def) 3225 apply (rule ext) 3226 apply (rule iffI) 3227 apply (erule bexEI) 3228 apply (erule rtranclE, simp) 3229 apply (clarsimp simp: vs_refs_def graph_of_def image_def 3230 dest!: vs_lookup1D 3231 split: Structures_A.kernel_object.splits 3232 arch_kernel_obj.splits) 3233 apply (erule bexEI) 3234 apply (erule rtranclE, simp) 3235 apply (clarsimp simp: vs_refs_pages_def graph_of_def image_def 3236 dest!: vs_lookup_pages1D 3237 split: Structures_A.kernel_object.splits 3238 arch_kernel_obj.splits) 3239 done 3240 3241(* FIXME: move to Invariants_A *) 3242lemma vs_lookup_pages_eq_ap: 3243 "[VSRef b (Some AASIDPool), VSRef a None] \<rhd> pd = 3244 [VSRef b (Some AASIDPool), VSRef a None] \<unrhd> pd" 3245 apply (simp add: vs_lookup_pages_def vs_lookup_def Image_def) 3246 apply (rule ext) 3247 apply (rule iffI) 3248 apply (erule bexEI) 3249 apply (erule rtranclE, simp) 3250 apply (clarsimp simp: vs_refs_def graph_of_def image_def 3251 dest!: vs_lookup1D 3252 split: Structures_A.kernel_object.splits 3253 arch_kernel_obj.splits) 3254 apply (erule rtranclE) 3255 apply (clarsimp simp: vs_asid_refs_def graph_of_def image_def) 3256 apply (rule converse_rtrancl_into_rtrancl[OF _ rtrancl_refl]) 3257 apply (fastforce simp: vs_refs_pages_def graph_of_def image_def 3258 vs_lookup_pages1_def) 3259 apply (clarsimp simp: vs_refs_def graph_of_def image_def 3260 dest!: vs_lookup1D 3261 split: Structures_A.kernel_object.splits 3262 arch_kernel_obj.splits) 3263 apply (erule bexEI) 3264 apply (erule rtranclE, simp) 3265 apply (clarsimp simp: vs_refs_pages_def graph_of_def image_def 3266 dest!: vs_lookup_pages1D 3267 split: Structures_A.kernel_object.splits 3268 arch_kernel_obj.splits) 3269 apply (erule rtranclE) 3270 apply (clarsimp simp: vs_asid_refs_def graph_of_def image_def) 3271 apply (rule converse_rtrancl_into_rtrancl[OF _ rtrancl_refl]) 3272 apply (fastforce simp: vs_refs_def graph_of_def image_def 3273 vs_lookup1_def) 3274 apply (clarsimp simp: vs_refs_pages_def graph_of_def image_def 3275 dest!: vs_lookup_pages1D 3276 split: Structures_A.kernel_object.splits 3277 arch_kernel_obj.splits) 3278 done 3279 3280lemma store_pde_unmap_pt: 3281 "\<lbrace>[VSRef (asid && mask asid_low_bits) (Some AASIDPool), 3282 VSRef (ucast (asid_high_bits_of asid)) None] \<rhd> pd 3283 and K (is_aligned pd pd_bits)\<rbrace> 3284 store_pde (pd + (vaddr >> 20 << 2)) InvalidPDE 3285 \<lbrace>\<lambda>rv s. 3286 \<not> ([VSRef (vaddr >> 20) (Some APageDirectory), 3287 VSRef (asid && mask asid_low_bits) (Some AASIDPool), 3288 VSRef (ucast (asid_high_bits_of asid)) None] \<rhd> pt) s\<rbrace>" 3289 apply (simp add: store_pde_def set_pd_def set_object_def) 3290 apply (wp get_object_wp) 3291 apply (clarsimp simp: obj_at_def fun_upd_def[symmetric]) 3292 apply (clarsimp simp: vs_lookup_def vs_asid_refs_def 3293 dest!: graph_ofD vs_lookup1_rtrancl_iterations) 3294 apply (clarsimp simp: vs_lookup1_def obj_at_def vs_refs_def 3295 dest!: graph_ofD 3296 split: if_split_asm 3297 Structures_A.kernel_object.split_asm 3298 arch_kernel_obj.split_asm) 3299 apply (simp add: pde_ref_def) 3300 apply (simp_all add: pd_shifting_again pd_shifting_again2 3301 pd_casting_shifting word_size) 3302 apply (simp add: up_ucast_inj_eq) 3303 done 3304 3305lemma vs_lookup_pages1_rtrancl_iterations: 3306 "(tup, tup') \<in> (vs_lookup_pages1 s)\<^sup>* 3307 \<Longrightarrow> (length (fst tup) \<le> length (fst tup')) \<and> 3308 (tup, tup') \<in> ((vs_lookup_pages1 s) 3309 ^^ (length (fst tup') - length (fst tup)))" 3310 apply (erule rtrancl_induct) 3311 apply simp 3312 apply (elim conjE) 3313 apply (subgoal_tac "length (fst z) = Suc (length (fst y))") 3314 apply (simp add: Suc_diff_le) 3315 apply (erule(1) relcompI) 3316 apply (clarsimp simp: vs_lookup_pages1_def) 3317 done 3318 3319lemma store_pde_unmap_page: 3320 "\<lbrace>[VSRef (asid && mask asid_low_bits) (Some AASIDPool), 3321 VSRef (ucast (asid_high_bits_of asid)) None] \<rhd> pd 3322 and K (is_aligned pd pd_bits)\<rbrace> 3323 store_pde (pd + (vaddr >> 20 << 2)) InvalidPDE 3324 \<lbrace>\<lambda>rv s. 3325 \<not> ([VSRef (vaddr >> 20) (Some APageDirectory), 3326 VSRef (asid && mask asid_low_bits) (Some AASIDPool), 3327 VSRef (ucast (asid_high_bits_of asid)) None] \<unrhd> pde) s\<rbrace>" 3328 apply (simp add: store_pde_def vs_lookup_pages_eq_ap set_pd_def set_object_def) 3329 apply (wp get_object_wp) 3330 apply (clarsimp simp: obj_at_def fun_upd_def[symmetric]) 3331 apply (clarsimp simp: vs_lookup_pages_def vs_asid_refs_def 3332 dest!: graph_ofD vs_lookup_pages1_rtrancl_iterations) 3333 apply (clarsimp simp: vs_lookup_pages1_def obj_at_def vs_refs_pages_def 3334 dest!: graph_ofD 3335 split: if_split_asm 3336 Structures_A.kernel_object.split_asm 3337 arch_kernel_obj.split_asm) 3338 apply (simp add: pde_ref_pages_def) 3339 apply (simp_all add: pd_shifting_again pd_shifting_again2 3340 pd_casting_shifting word_size) 3341 apply (simp add: up_ucast_inj_eq) 3342 done 3343 3344(* FIXME: move to Invariants_A *) 3345lemma pte_ref_pages_invalid_None[simp]: 3346 "pte_ref_pages InvalidPTE = None" 3347 by (simp add: pte_ref_pages_def) 3348 3349lemma store_pte_no_lookup_pages: 3350 "\<lbrace>\<lambda>s. \<not> (r \<unrhd> q) s\<rbrace> 3351 store_pte p InvalidPTE 3352 \<lbrace>\<lambda>_ s. \<not> (r \<unrhd> q) s\<rbrace>" 3353 apply (simp add: store_pte_def set_pt_def set_object_def) 3354 apply (wp get_object_wp) 3355 apply (clarsimp simp: obj_at_def) 3356 apply (erule swap, simp) 3357 apply (erule vs_lookup_pages_induct) 3358 apply (simp add: vs_lookup_pages_atI) 3359 apply (thin_tac "(ref \<unrhd> p) (kheap_update f s)" for ref p f) 3360 apply (erule vs_lookup_pages_step) 3361 by (fastforce simp: vs_lookup_pages1_def obj_at_def vs_refs_pages_def 3362 graph_of_def image_def 3363 split: if_split_asm) 3364 3365(* FIXME: move to Invariants_A *) 3366lemma pde_ref_pages_invalid_None[simp]: 3367 "pde_ref_pages InvalidPDE = None" 3368 by (simp add: pde_ref_pages_def) 3369 3370lemma store_pde_no_lookup_pages: 3371 "\<lbrace>\<lambda>s. \<not> (r \<unrhd> q) s\<rbrace> store_pde p InvalidPDE \<lbrace>\<lambda>_ s. \<not> (r \<unrhd> q) s\<rbrace>" 3372 apply (simp add: store_pde_def set_pd_def set_object_def) 3373 apply (wp get_object_wp) 3374 apply (clarsimp simp: obj_at_def) 3375 apply (erule swap, simp) 3376 apply (erule vs_lookup_pages_induct) 3377 apply (simp add: vs_lookup_pages_atI) 3378 apply (thin_tac "(ref \<unrhd> p) (kheap_update f s)" for ref p f) 3379 apply (erule vs_lookup_pages_step) 3380 by (fastforce simp: vs_lookup_pages1_def obj_at_def vs_refs_pages_def 3381 graph_of_def image_def 3382 split: if_split_asm) 3383 3384crunch vs_lookup_pages[wp]: 3385 get_hw_asid,find_pd_for_asid,set_vm_root_for_flush "\<lambda>s. P (vs_lookup_pages s)" 3386 3387lemma flush_table_vs_lookup_pages[wp]: 3388 "\<lbrace>\<lambda>s. P (vs_lookup_pages s)\<rbrace> 3389 flush_table a b c d 3390 \<lbrace>\<lambda>_ s. P (vs_lookup_pages s)\<rbrace>" 3391 by (simp add: flush_table_def | wp mapM_UNIV_wp hoare_drop_imps | wpc 3392 | intro conjI impI)+ 3393 3394crunch vs_lookup_pages[wp]: page_table_mapped "\<lambda>s. P (vs_lookup_pages s)" 3395 3396lemma unmap_page_table_unmapped[wp]: 3397 "\<lbrace>pspace_aligned and valid_vspace_objs\<rbrace> 3398 unmap_page_table asid vaddr pt 3399 \<lbrace>\<lambda>rv s. \<not> ([VSRef (vaddr >> 20) (Some APageDirectory), 3400 VSRef (asid && mask asid_low_bits) (Some AASIDPool), 3401 VSRef (ucast (asid_high_bits_of asid)) None] \<rhd> pt) s\<rbrace>" 3402 apply (simp add: unmap_page_table_def lookup_pd_slot_def Let_def 3403 cong: option.case_cong) 3404 apply (rule hoare_pre) 3405 apply ((wp store_pde_unmap_pt page_table_mapped_wp | wpc | simp)+)[1] 3406 apply (clarsimp simp: vspace_at_asid_def pd_aligned pd_bits_def pageBits_def) 3407 done 3408 3409lemma unmap_page_table_unmapped2: 3410 "\<lbrace>pspace_aligned and valid_vspace_objs and 3411 K (ref = [VSRef (vaddr >> 20) (Some APageDirectory), 3412 VSRef (asid && mask asid_low_bits) (Some AASIDPool), 3413 VSRef (ucast (asid_high_bits_of asid)) None] 3414 \<and> p = pt)\<rbrace> 3415 unmap_page_table asid vaddr pt 3416 \<lbrace>\<lambda>rv s. \<not> (ref \<rhd> p) s\<rbrace>" 3417 apply (rule hoare_gen_asm) 3418 apply simp 3419 apply wp 3420 done 3421 3422lemma cacheRangeOp_lift[wp]: 3423 assumes o: "\<And>a b. \<lbrace>P\<rbrace> oper a b \<lbrace>\<lambda>_. P\<rbrace>" 3424 shows "\<lbrace>P\<rbrace> cacheRangeOp oper x y z \<lbrace>\<lambda>_. P\<rbrace>" 3425 apply (clarsimp simp: cacheRangeOp_def lineStart_def cacheLineBits_def cacheLine_def) 3426 apply (rule hoare_pre) 3427 apply (wp mapM_x_wp_inv o) 3428 apply (case_tac x, simp, wp o, simp) 3429 done 3430 3431lemma cleanCacheRange_PoU_underlying_memory[wp]: 3432 "\<lbrace>\<lambda>m'. underlying_memory m' p = um\<rbrace> cleanCacheRange_PoU a b c \<lbrace>\<lambda>_ m'. underlying_memory m' p = um\<rbrace>" 3433 by (clarsimp simp: cleanCacheRange_PoU_def, wp) 3434 3435 3436lemma unmap_page_table_unmapped3: 3437 "\<lbrace>pspace_aligned and valid_vspace_objs and page_table_at pt and 3438 K (ref = [VSRef (vaddr >> 20) (Some APageDirectory), 3439 VSRef (asid && mask asid_low_bits) (Some AASIDPool), 3440 VSRef (ucast (asid_high_bits_of asid)) None] 3441 \<and> p = pt)\<rbrace> 3442 unmap_page_table asid vaddr pt 3443 \<lbrace>\<lambda>rv s. \<not> (ref \<unrhd> p) s\<rbrace>" 3444 apply (rule hoare_gen_asm) 3445 apply (simp add: unmap_page_table_def lookup_pd_slot_def Let_def 3446 cong: option.case_cong) 3447 apply (rule hoare_pre) 3448 apply ((wp store_pde_unmap_page | wpc | simp)+)[1] 3449 apply (rule page_table_mapped_wp) 3450 apply (clarsimp simp: vspace_at_asid_def pd_aligned pd_bits_def pageBits_def) 3451 apply (drule vs_lookup_pages_2ConsD) 3452 apply (clarsimp simp: obj_at_def vs_refs_pages_def 3453 dest!: vs_lookup_pages1D 3454 split: Structures_A.kernel_object.splits 3455 arch_kernel_obj.splits) 3456 apply (drule vs_lookup_pages_eq_ap[THEN fun_cong, symmetric, THEN iffD1]) 3457 apply (erule swap) 3458 apply (drule (1) valid_vspace_objsD[rotated 2]) 3459 apply (simp add: obj_at_def) 3460 apply (erule vs_lookup_step) 3461 apply (clarsimp simp: obj_at_def vs_refs_def vs_lookup1_def 3462 graph_of_def image_def 3463 split: if_split_asm) 3464 apply (drule bspec, fastforce) 3465 apply (auto simp: obj_at_def data_at_def valid_pde_def pde_ref_def pde_ref_pages_def 3466 split: pde.splits) 3467 done 3468 3469lemma is_final_cap_caps_of_state_2D: 3470 "\<lbrakk> caps_of_state s p = Some cap; caps_of_state s p' = Some cap'; 3471 is_final_cap' cap'' s; gen_obj_refs cap \<inter> gen_obj_refs cap'' \<noteq> {}; 3472 gen_obj_refs cap' \<inter> gen_obj_refs cap'' \<noteq> {} \<rbrakk> 3473 \<Longrightarrow> p = p'" 3474 apply (clarsimp simp: is_final_cap'_def3) 3475 apply (frule_tac x="fst p" in spec) 3476 apply (drule_tac x="snd p" in spec) 3477 apply (drule_tac x="fst p'" in spec) 3478 apply (drule_tac x="snd p'" in spec) 3479 apply (clarsimp simp: cte_wp_at_caps_of_state Int_commute 3480 prod_eqI) 3481 done 3482 3483(* FIXME: move *) 3484lemma empty_table_pt_capI: 3485 "\<lbrakk>caps_of_state s p = 3486 Some (cap.ArchObjectCap (arch_cap.PageTableCap pt None)); 3487 valid_table_caps s\<rbrakk> 3488 \<Longrightarrow> obj_at (empty_table (set (second_level_tables (arch_state s)))) pt s" 3489 apply (case_tac p) 3490 apply (clarsimp simp: valid_table_caps_def simp del: imp_disjL) 3491 apply (drule spec)+ 3492 apply (erule impE, simp add: is_cap_simps)+ 3493 by assumption 3494 3495crunch underlying_memory[wp]: cleanCacheRange_PoC, cleanL2Range, invalidateL2Range, invalidateByVA, 3496 cleanInvalidateL2Range, cleanInvalByVA, invalidateCacheRange_I, 3497 branchFlushRange, ackInterrupt 3498 "\<lambda>m'. underlying_memory m' p = um" 3499 (simp: cache_machine_op_defs machine_op_lift_def machine_rest_lift_def split_def) 3500 3501crunch underlying_memory[wp]: cleanCacheRange_RAM, invalidateCacheRange_RAM, 3502 cleanInvalidateCacheRange_RAM, do_flush 3503 "\<lambda>m'. underlying_memory m' p = um" 3504 (simp: crunch_simps) 3505 3506lemma no_irq_do_flush: 3507 "no_irq (do_flush a b c d)" 3508 apply (simp add: do_flush_def) 3509 apply (case_tac a) 3510 apply (wp no_irq_dsb no_irq_invalidateCacheRange_I no_irq_branchFlushRange no_irq_isb | simp)+ 3511 done 3512 3513lemma cleanCacheRange_PoU_respects_device_region[wp]: 3514 "\<lbrace>\<lambda>ms. P (device_state ms)\<rbrace> cleanCacheRange_PoU a b c \<lbrace>\<lambda>_ ms. P (device_state ms)\<rbrace>" 3515 apply (clarsimp simp: cleanCacheRange_PoU_def cacheRangeOp_def) 3516 apply (wp mapM_x_wp | wpc | clarsimp | fastforce)+ 3517 done 3518 3519lemma cacheRangeOp_respects_device_region[wp]: 3520 assumes valid_f: "\<And>a b P. \<lbrace>\<lambda>ms. P (device_state ms)\<rbrace> f a b \<lbrace>\<lambda>_ ms. P (device_state ms)\<rbrace>" 3521 shows "\<lbrace>\<lambda>ms. P (device_state ms)\<rbrace> cacheRangeOp f a b c\<lbrace>\<lambda>_ ms. P (device_state ms)\<rbrace>" 3522 apply (clarsimp simp: do_flush_def cacheRangeOp_def) 3523 apply (rule hoare_pre) 3524 apply (wp mapM_x_wp valid_f | wpc | clarsimp | assumption)+ 3525 done 3526 3527crunches cleanByVA, cleanCacheRange_PoC, cleanCacheRange_RAM, 3528 cleanInvalByVA, invalidateByVA, invalidateL2Range, 3529 invalidateCacheRange_RAM, branchFlush, branchFlushRange, 3530 invalidateByVA_I, cleanInvalidateL2Range, do_flush, storeWord 3531 for device_state_inv[wp]: "\<lambda>ms. P (device_state ms)" 3532 (wp: cacheRangeOp_respects_device_region simp: crunch_simps) 3533 3534crunch pspace_in_kernel_window[wp]: perform_page_invocation "pspace_in_kernel_window" 3535 (simp: crunch_simps wp: crunch_wps) 3536 3537crunch pspace_respects_device_region[wp]: perform_page_invocation "pspace_respects_device_region" 3538 (simp: crunch_simps wp: crunch_wps set_object_pspace_respects_device_region 3539 pspace_respects_device_region_dmo) 3540 3541lemma perform_page_directory_invocation_invs[wp]: 3542 "\<lbrace>invs and valid_pdi pdi\<rbrace> 3543 perform_page_directory_invocation pdi 3544 \<lbrace>\<lambda>_. invs\<rbrace>" 3545 apply (cases pdi) 3546 apply (clarsimp simp: perform_page_directory_invocation_def) 3547 apply (wp dmo_invs set_vm_root_for_flush_invs 3548 hoare_vcg_const_imp_lift hoare_vcg_all_lift 3549 | simp)+ 3550 apply (rule hoare_pre_imp[of _ \<top>], assumption) 3551 apply (clarsimp simp: valid_def) 3552 apply (thin_tac "p \<in> fst (set_vm_root_for_flush a b s)" for p a b) 3553 apply safe[1] 3554 apply (drule_tac Q="\<lambda>_ m'. underlying_memory m' p = underlying_memory m p" 3555 in use_valid) 3556 apply ((clarsimp | wp)+)[3] 3557 apply(erule use_valid, wp no_irq_do_flush no_irq, assumption) 3558 apply(wp set_vm_root_for_flush_invs | simp add: valid_pdi_def)+ 3559 apply (clarsimp simp: perform_page_directory_invocation_def) 3560 done 3561 3562lemma perform_page_table_invocation_invs[wp]: 3563 notes no_irq[wp] hoare_pre [wp_pre del] 3564 shows 3565 "\<lbrace>invs and valid_pti pti\<rbrace> 3566 perform_page_table_invocation pti 3567 \<lbrace>\<lambda>_. invs\<rbrace>" 3568 apply (cases pti) 3569 apply (clarsimp simp: valid_pti_def perform_page_table_invocation_def) 3570 apply (wp dmo_invs) 3571 apply (rule_tac Q="\<lambda>_. invs" in hoare_post_imp) 3572 apply safe 3573 apply (drule_tac Q="\<lambda>_ m'. underlying_memory m' p = 3574 underlying_memory m p" in use_valid) 3575 apply ((clarsimp simp: machine_op_lift_def 3576 machine_rest_lift_def split_def | wp)+)[3] 3577 apply(erule use_valid, wp no_irq_cleanByVA_PoU no_irq, assumption) 3578 apply (wp store_pde_map_invs)[1] 3579 apply simp 3580 apply (rule hoare_pre, wp arch_update_cap_invs_map arch_update_cap_pspace 3581 arch_update_cap_valid_mdb set_cap_idle update_cap_ifunsafe 3582 valid_irq_node_typ valid_pde_lift set_cap_typ_at 3583 set_cap_irq_handlers set_cap_empty_pde 3584 hoare_vcg_all_lift hoare_vcg_ex_lift hoare_vcg_imp_lift 3585 set_cap_arch_obj set_cap_obj_at_impossible set_cap_valid_arch_caps) 3586 apply (simp; intro conjI; clarsimp simp: cte_wp_at_caps_of_state) 3587 apply (clarsimp simp: is_pt_cap_def is_arch_update_def cap_master_cap_def 3588 vs_cap_ref_simps 3589 split: cap.splits arch_cap.splits option.splits) 3590 apply fastforce 3591 apply (rule exI, rule conjI, assumption) 3592 apply (clarsimp simp: is_pt_cap_def is_arch_update_def 3593 cap_master_cap_def cap_asid_def vs_cap_ref_simps 3594 is_arch_cap_def pde_ref_def pde_ref_pages_def 3595 split: cap.splits arch_cap.splits option.splits 3596 pde.splits) 3597 apply (intro allI impI conjI, fastforce) 3598 apply (clarsimp simp: caps_of_def cap_of_def) 3599 apply (frule invs_pd_caps) 3600 apply (drule (1) empty_table_pt_capI) 3601 apply (clarsimp simp: obj_at_def empty_table_def pte_ref_pages_def) 3602 apply (clarsimp simp: perform_page_table_invocation_def 3603 split: cap.split arch_cap.split) 3604 apply (rename_tac word option) 3605 apply (rule hoare_pre) 3606 apply (wp arch_update_cap_invs_unmap_page_table get_cap_wp) 3607 apply (simp add: cte_wp_at_caps_of_state) 3608 apply (wpc, wp, wpc) 3609 apply (rule hoare_lift_Pf2[where f=caps_of_state]) 3610 apply (wp hoare_vcg_all_lift hoare_vcg_const_imp_lift)+ 3611 apply (rule hoare_vcg_conj_lift) 3612 apply (wp dmo_invs) 3613 apply (wp hoare_vcg_all_lift hoare_vcg_const_imp_lift 3614 valid_cap_typ[OF do_machine_op_obj_at] 3615 mapM_x_swp_store_pte_invs[unfolded cte_wp_at_caps_of_state] 3616 mapM_x_swp_store_empty_table 3617 valid_cap_typ[OF unmap_page_table_typ_at] 3618 unmap_page_table_unmapped3)+ 3619 apply (rule hoare_pre_imp[of _ \<top>], assumption) 3620 apply (clarsimp simp: valid_def split_def) 3621 apply safe[1] 3622 apply (drule_tac Q="\<lambda>_ m'. underlying_memory m' p = 3623 underlying_memory m p" in use_valid) 3624 apply ((clarsimp | wp)+)[3] 3625 apply(erule use_valid, wp no_irq_cleanCacheRange_PoU, assumption) 3626 apply (wp hoare_vcg_all_lift hoare_vcg_const_imp_lift 3627 valid_cap_typ[OF do_machine_op_obj_at] 3628 mapM_x_swp_store_pte_invs[unfolded cte_wp_at_caps_of_state] 3629 mapM_x_swp_store_empty_table 3630 valid_cap_typ[OF unmap_page_table_typ_at] 3631 unmap_page_table_unmapped3 store_pte_no_lookup_pages 3632 | wp_once hoare_vcg_conj_lift 3633 | wp_once mapM_x_wp' 3634 | simp)+ 3635 apply (clarsimp simp: valid_pti_def cte_wp_at_caps_of_state 3636 is_arch_diminished_def is_cap_simps 3637 is_arch_update_def cap_rights_update_def 3638 acap_rights_update_def cap_master_cap_simps 3639 update_map_data_def) 3640 apply (frule (2) diminished_is_update') 3641 apply (simp add: cap_rights_update_def acap_rights_update_def) 3642 apply (rule conjI) 3643 apply (clarsimp simp: vs_cap_ref_def) 3644 apply (drule invs_pd_caps) 3645 apply (simp add: valid_table_caps_def) 3646 apply (elim allE, drule(1) mp) 3647 apply (simp add: is_cap_simps cap_asid_def) 3648 apply (drule mp, rule refl) 3649 apply (clarsimp simp: obj_at_def valid_cap_def empty_table_def 3650 a_type_def) 3651 apply (clarsimp split: Structures_A.kernel_object.split_asm 3652 arch_kernel_obj.split_asm) 3653 apply (clarsimp simp: valid_cap_def mask_def[where n=asid_bits] 3654 vmsz_aligned_def cap_aligned_def vs_cap_ref_def 3655 invs_psp_aligned invs_vspace_objs) 3656 apply (subgoal_tac "(\<forall>x\<in>set [word , word + 4 .e. word + 2 ^ pt_bits - 1]. 3657 x && ~~ mask pt_bits = word)") 3658 apply (intro conjI) 3659 apply (simp add: cap_master_cap_def) 3660 apply fastforce 3661 apply (clarsimp simp: image_def) 3662 apply (subgoal_tac "word + (ucast x << 2) 3663 \<in> set [word, word + 4 .e. word + 2 ^ pt_bits - 1]") 3664 apply (rule rev_bexI, assumption) 3665 apply (rule ccontr, erule more_pt_inner_beauty) 3666 apply simp 3667 apply (clarsimp simp: upto_enum_step_def linorder_not_less) 3668 apply (subst is_aligned_no_overflow, 3669 erule is_aligned_weaken, 3670 (simp_all add: pt_bits_def pageBits_def)[2])+ 3671 apply (clarsimp simp: image_def word_shift_by_2) 3672 apply (rule exI, rule conjI[OF _ refl]) 3673 apply (rule plus_one_helper) 3674 apply (rule order_less_le_trans, rule ucast_less, simp+) 3675 apply (clarsimp simp: upto_enum_step_def) 3676 apply (rule conjunct2, rule is_aligned_add_helper) 3677 apply (simp add: pt_bits_def pageBits_def) 3678 apply (simp only: word_shift_by_2) 3679 apply (rule shiftl_less_t2n) 3680 apply (rule minus_one_helper5) 3681 apply (simp add: pt_bits_def pageBits_def)+ 3682 done 3683 3684crunch cte_wp_at [wp]: unmap_page "\<lambda>s. P (cte_wp_at P' p s)" 3685 (wp: crunch_wps simp: crunch_simps) 3686 3687crunch typ_at [wp]: unmap_page "\<lambda>s. P (typ_at T p s)" 3688 (wp: crunch_wps simp: crunch_simps) 3689 3690lemmas unmap_page_typ_ats [wp] = abs_typ_at_lifts [OF unmap_page_typ_at] 3691 3692lemma invalidateLocalTLB_VAASID_underlying_memory[wp]: 3693 "\<lbrace>\<lambda>m'. underlying_memory m' p = um\<rbrace> invalidateLocalTLB_VAASID v \<lbrace>\<lambda>_ m'. underlying_memory m' p = um\<rbrace>" 3694 by (clarsimp simp: invalidateLocalTLB_VAASID_def machine_rest_lift_def machine_op_lift_def split_def | wp)+ 3695 3696lemma flush_page_invs: 3697 "\<lbrace>invs and K (asid \<le> mask asid_bits)\<rbrace> 3698 flush_page sz pd asid vptr \<lbrace>\<lambda>rv. invs\<rbrace>" 3699 apply (simp add: flush_page_def) 3700 apply (wp dmo_invs hoare_vcg_all_lift load_hw_asid_wp 3701 set_vm_root_for_flush_invs hoare_drop_imps 3702 | simp add: split_def)+ 3703 apply (rule hoare_pre_imp[of _ \<top>], assumption) 3704 apply (clarsimp simp: valid_def) 3705 apply (thin_tac "x : fst (set_vm_root_for_flush a b c)" for x a b c) 3706 apply safe 3707 apply (drule_tac Q="\<lambda>_ m'. underlying_memory m' p = underlying_memory m p" 3708 in use_valid) 3709 apply ((clarsimp | wp)+)[3] 3710 apply(erule use_valid, wp no_irq_invalidateLocalTLB_VAASID no_irq, assumption) 3711 apply (wp set_vm_root_for_flush_invs hoare_drop_imps|simp)+ 3712 done 3713 3714lemma find_pd_for_asid_lookup_slot [wp]: 3715 "\<lbrace>pspace_aligned and valid_vspace_objs\<rbrace> find_pd_for_asid asid 3716 \<lbrace>\<lambda>rv. \<exists>\<rhd> (lookup_pd_slot rv vptr && ~~ mask pd_bits)\<rbrace>, -" 3717 apply (rule hoare_pre) 3718 apply (rule hoare_post_imp_R) 3719 apply (rule hoare_vcg_R_conj) 3720 apply (rule find_pd_for_asid_lookup) 3721 apply (rule find_pd_for_asid_aligned_pd) 3722 apply (simp add: pd_shifting lookup_pd_slot_def Let_def) 3723 apply simp 3724 done 3725 3726lemma find_pd_for_asid_lookup_slot_large_page [wp]: 3727 "\<lbrace>pspace_aligned and valid_vspace_objs and K (x \<in> set [0, 4 .e. 0x3C] \<and> is_aligned vptr 24)\<rbrace> 3728 find_pd_for_asid asid 3729 \<lbrace>\<lambda>rv. \<exists>\<rhd> (x + lookup_pd_slot rv vptr && ~~ mask pd_bits)\<rbrace>, -" 3730 apply (rule hoare_pre) 3731 apply (rule hoare_post_imp_R) 3732 apply (rule hoare_vcg_R_conj) 3733 apply (rule hoare_vcg_R_conj) 3734 apply (rule find_pd_for_asid_inv [where P="K (x \<in> set [0, 4 .e. 0x3C] \<and> is_aligned vptr 24)", THEN valid_validE_R]) 3735 apply (rule find_pd_for_asid_lookup) 3736 apply (rule find_pd_for_asid_aligned_pd) 3737 apply (subst lookup_pd_slot_add_eq) 3738 apply (simp_all add: pd_bits_def pageBits_def) 3739 done 3740 3741lemma find_pd_for_asid_pde_at_add [wp]: 3742 "\<lbrace>K (x \<in> set [0,4 .e. 0x3C] \<and> is_aligned vptr 24) and pspace_aligned and valid_vspace_objs\<rbrace> 3743 find_pd_for_asid asid \<lbrace>\<lambda>rv. pde_at (x + lookup_pd_slot rv vptr)\<rbrace>, -" 3744 apply (rule hoare_pre) 3745 apply (rule hoare_post_imp_R) 3746 apply (rule hoare_vcg_R_conj) 3747 apply (rule find_pd_for_asid_inv [where P= 3748 "K (x \<in> set [0, 4 .e. 0x3C] \<and> is_aligned vptr 24) and pspace_aligned", THEN valid_validE_R]) 3749 apply (rule find_pd_for_asid_page_directory) 3750 apply (auto intro!: pde_at_aligned_vptr) 3751 done 3752 3753lemma valid_kernel_mappingsD: 3754 "\<lbrakk> kheap s pdptr = Some (ArchObj (PageDirectory pd)); 3755 valid_kernel_mappings s \<rbrakk> 3756 \<Longrightarrow> \<forall>x r. pde_ref (pd x) = Some r \<longrightarrow> 3757 (r \<in> set (arm_global_pts (arch_state s))) 3758 = (ucast (kernel_base >> 20) \<le> x)" 3759 apply (simp add: valid_kernel_mappings_def) 3760 apply (drule bspec, erule ranI) 3761 apply (simp add: valid_kernel_mappings_if_pd_def 3762 kernel_mapping_slots_def) 3763 done 3764 3765lemma lookup_pt_slot_cap_to: 3766 shows "\<lbrace>invs and \<exists>\<rhd>pd and K (is_aligned pd pd_bits) 3767 and K (vptr < kernel_base)\<rbrace> lookup_pt_slot pd vptr 3768 \<lbrace>\<lambda>rv s. \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> is_pt_cap cap 3769 \<and> rv && ~~ mask pt_bits \<in> obj_refs cap 3770 \<and> s \<turnstile> cap \<and> cap_asid cap \<noteq> None 3771 \<and> (is_aligned vptr 16 \<longrightarrow> is_aligned rv 6)\<rbrace>, -" 3772 proof - 3773 have shift: "(2::word32) ^ pt_bits = 2 ^ 8 << 2" 3774 by (simp add:pt_bits_def pageBits_def ) 3775 show ?thesis 3776 apply (simp add: lookup_pt_slot_def) 3777 apply (wp get_pde_wp | wpc)+ 3778 apply (clarsimp simp: lookup_pd_slot_pd) 3779 apply (frule(1) valid_vspace_objsD) 3780 apply fastforce 3781 apply (drule vs_lookup_step) 3782 apply (erule vs_lookup1I[OF _ _ refl]) 3783 apply (simp add: vs_refs_def image_def) 3784 apply (rule rev_bexI) 3785 apply (erule pde_graph_ofI) 3786 apply (erule (1) less_kernel_base_mapping_slots) 3787 apply (simp add: pde_ref_def) 3788 apply fastforce 3789 apply (drule valid_vs_lookupD[OF vs_lookup_pages_vs_lookupI], clarsimp) 3790 apply simp 3791 apply (elim exEI, clarsimp) 3792 apply (subst is_aligned_add_helper[THEN conjunct2]) 3793 apply (drule caps_of_state_valid) 3794 apply fastforce 3795 apply (clarsimp dest!:valid_cap_aligned simp:cap_aligned_def vs_cap_ref_def 3796 obj_refs_def obj_ref_of_def pageBitsForSize_def pt_bits_def pageBits_def 3797 elim!:is_aligned_weaken 3798 split:arch_cap.split_asm cap.splits option.split_asm vmpage_size.split_asm) 3799 apply (rule less_le_trans[OF shiftl_less_t2n[where m = 10]]) 3800 apply (rule le_less_trans[OF word_and_le1]) 3801 apply simp 3802 apply simp 3803 apply (simp add:pt_bits_def pageBits_def) 3804 apply (drule caps_of_state_valid) 3805 apply fastforce 3806 apply (drule bspec) 3807 apply (drule(1) less_kernel_base_mapping_slots) 3808 apply simp 3809 apply (clarsimp simp: valid_pde_def obj_at_def 3810 vs_cap_ref_def is_pt_cap_def valid_cap_simps cap_aligned_def 3811 split: cap.split_asm arch_cap.split_asm vmpage_size.splits 3812 option.split_asm if_splits) 3813 apply (erule is_aligned_add[OF is_aligned_weaken],simp 3814 ,rule is_aligned_shiftl[OF is_aligned_andI1,OF is_aligned_shiftr],simp)+ 3815 done 3816qed 3817 3818lemma lookup_pt_slot_cap_to1[wp]: 3819 "\<lbrace>invs and \<exists>\<rhd>pd and K (is_aligned pd pd_bits) 3820 and K (vptr < kernel_base)\<rbrace> lookup_pt_slot pd vptr 3821 \<lbrace>\<lambda>rv s. \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> is_pt_cap cap \<and> rv && ~~ mask pt_bits \<in> obj_refs cap\<rbrace>,-" 3822 apply (rule hoare_post_imp_R) 3823 apply (rule lookup_pt_slot_cap_to) 3824 apply auto 3825 done 3826 3827lemma lookup_pt_slot_cap_to_multiple1: 3828 "\<lbrace>invs and \<exists>\<rhd>pd and K (is_aligned pd pd_bits) 3829 and K (vptr < kernel_base) 3830 and K (is_aligned vptr 16)\<rbrace> 3831 lookup_pt_slot pd vptr 3832 \<lbrace>\<lambda>rv s. is_aligned rv 6 \<and> 3833 (\<exists>a b. cte_wp_at (\<lambda>c. is_pt_cap c \<and> cap_asid c \<noteq> None 3834 \<and> (\<lambda>x. x && ~~ mask pt_bits) ` set [rv , rv + 4 .e. rv + 0x3C] \<subseteq> obj_refs c) (a, b) s)\<rbrace>, -" 3835 apply (rule hoare_gen_asmE) 3836 apply (rule hoare_post_imp_R) 3837 apply (rule lookup_pt_slot_cap_to) 3838 apply (rule conjI, clarsimp) 3839 apply (elim exEI) 3840 apply (clarsimp simp: cte_wp_at_caps_of_state is_pt_cap_def 3841 valid_cap_def cap_aligned_def 3842 del: subsetI) 3843 apply (simp add: subset_eq p_0x3C_shift) 3844 apply (clarsimp simp: set_upto_enum_step_4) 3845 apply (fold mask_def[where n=4, simplified]) 3846 apply (subst(asm) le_mask_iff) 3847 apply (subst word_plus_and_or_coroll) 3848 apply (rule shiftr_eqD[where n=6]) 3849 apply (simp add: shiftr_over_and_dist shiftl_shiftr2) 3850 apply (simp add: is_aligned_andI2) 3851 apply simp 3852 apply (simp add: word_ao_dist) 3853 apply (simp add: and_not_mask pt_bits_def pageBits_def) 3854 apply (drule arg_cong[where f="\<lambda>x. x >> 4"]) 3855 apply (simp add: shiftl_shiftr2 shiftr_shiftr) 3856 done 3857 3858lemma lookup_pt_slot_cap_to_multiple[wp]: 3859 "\<lbrace>invs and \<exists>\<rhd>pd and K (is_aligned pd pd_bits) 3860 and K (vptr < kernel_base) 3861 and K (is_aligned vptr 16)\<rbrace> 3862 lookup_pt_slot pd vptr 3863 \<lbrace>\<lambda>rv s. \<exists>a b. cte_wp_at (\<lambda>c. (\<lambda>x. x && ~~ mask pt_bits) ` (\<lambda>x. x + rv) ` set [0 , 4 .e. 0x3C] \<subseteq> obj_refs c) (a, b) s\<rbrace>, -" 3864 apply (rule hoare_post_imp_R, rule lookup_pt_slot_cap_to_multiple1) 3865 apply (elim conjE exEI cte_wp_at_weakenE) 3866 apply (simp add: subset_eq p_0x3C_shift) 3867 done 3868 3869lemma find_pd_for_asid_cap_to: 3870 "\<lbrace>invs\<rbrace> find_pd_for_asid asid 3871 \<lbrace>\<lambda>rv s. \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> rv \<in> obj_refs cap 3872 \<and> is_pd_cap cap \<and> s \<turnstile> cap 3873 \<and> is_aligned rv pd_bits\<rbrace>, -" 3874 apply (simp add: find_pd_for_asid_def assertE_def split del: if_split) 3875 apply (rule hoare_pre) 3876 apply (wp | wpc)+ 3877 apply clarsimp 3878 apply (drule vs_lookup_atI) 3879 apply (frule(1) valid_vspace_objsD, clarsimp) 3880 apply (drule vs_lookup_step) 3881 apply (erule vs_lookup1I [OF _ _ refl]) 3882 apply (simp add: vs_refs_def image_def) 3883 apply (rule rev_bexI) 3884 apply (erule graph_ofI) 3885 apply fastforce 3886 apply (drule valid_vs_lookupD[OF vs_lookup_pages_vs_lookupI], clarsimp) 3887 apply (simp, elim exEI) 3888 apply clarsimp 3889 apply (frule caps_of_state_valid_cap, clarsimp+) 3890 apply (clarsimp simp: table_cap_ref_ap_eq[symmetric] table_cap_ref_def 3891 is_pd_cap_def valid_cap_def cap_aligned_def 3892 pd_bits_def pageBits_def 3893 split: cap.split_asm arch_cap.split_asm option.split_asm) 3894 done 3895 3896lemma find_pd_for_asid_cap_to1[wp]: 3897 "\<lbrace>invs\<rbrace> find_pd_for_asid asid 3898 \<lbrace>\<lambda>rv s. \<exists>a b cap. caps_of_state s (a, b) = Some cap \<and> lookup_pd_slot rv vptr && ~~ mask pd_bits \<in> obj_refs cap\<rbrace>, -" 3899 apply (rule hoare_post_imp_R, rule find_pd_for_asid_cap_to) 3900 apply (clarsimp simp: lookup_pd_slot_pd) 3901 apply auto 3902 done 3903 3904lemma find_pd_for_asid_cap_to2[wp]: 3905 "\<lbrace>invs\<rbrace> find_pd_for_asid asid 3906 \<lbrace>\<lambda>rv s. \<exists>a b. cte_wp_at 3907 (\<lambda>cp. lookup_pd_slot rv vptr && ~~ mask pd_bits \<in> obj_refs cp \<and> is_pd_cap cp) 3908 (a, b) s\<rbrace>, -" 3909 apply (rule hoare_post_imp_R, rule find_pd_for_asid_cap_to) 3910 apply (clarsimp simp: lookup_pd_slot_pd cte_wp_at_caps_of_state) 3911 apply auto 3912 done 3913 3914lemma find_pd_for_asid_cap_to_multiple[wp]: 3915 "\<lbrace>invs and K (is_aligned vptr 24)\<rbrace> find_pd_for_asid asid 3916 \<lbrace>\<lambda>rv s. \<exists>x xa. cte_wp_at (\<lambda>a. (\<lambda>x. x && ~~ mask pd_bits) ` (\<lambda>x. x + lookup_pd_slot rv vptr) ` set [0 , 4 .e. 0x3C] \<subseteq> obj_refs a) (x, xa) s\<rbrace>, -" 3917 apply (rule hoare_gen_asmE, rule hoare_post_imp_R, rule find_pd_for_asid_cap_to) 3918 apply (elim exEI, clarsimp simp: cte_wp_at_caps_of_state) 3919 apply (simp add: lookup_pd_slot_add_eq) 3920 done 3921 3922lemma find_pd_for_asid_cap_to_multiple2[wp]: 3923 "\<lbrace>invs and K (is_aligned vptr 24)\<rbrace> 3924 find_pd_for_asid asid 3925 \<lbrace>\<lambda>rv s. \<forall>x\<in>set [0 , 4 .e. 0x3C]. \<exists>a b. 3926 cte_wp_at (\<lambda>cp. x + lookup_pd_slot rv vptr && ~~ mask pd_bits 3927 \<in> obj_refs cp \<and> is_pd_cap cp) (a, b) s\<rbrace>, -" 3928 apply (rule hoare_gen_asmE, rule hoare_post_imp_R, 3929 rule find_pd_for_asid_cap_to) 3930 apply (intro ballI, elim exEI, 3931 clarsimp simp: cte_wp_at_caps_of_state) 3932 apply (simp add: lookup_pd_slot_add_eq) 3933 done 3934 3935lemma unat_ucast_kernel_base_rshift: 3936 "unat (ucast (kernel_base >> 20) :: 12 word) 3937 = unat (kernel_base >> 20)" 3938 by (simp add: kernel_base_def) 3939 3940lemma lookup_pd_slot_kernel_mappings_set_strg: 3941 "is_aligned pd pd_bits \<and> vmsz_aligned vptr ARMSuperSection 3942 \<and> vptr < kernel_base 3943 \<longrightarrow> 3944 (\<forall>x\<in>set [0 , 4 .e. 0x3C]. ucast (x + lookup_pd_slot pd vptr && mask pd_bits >> 2) 3945 \<notin> kernel_mapping_slots)" 3946 apply (clarsimp simp: upto_enum_step_def word_shift_by_2) 3947 apply (simp add: less_kernel_base_mapping_slots_both minus_one_helper5) 3948 done 3949 3950lemma lookup_pt_slot_cap_to2: 3951 "\<lbrace>invs and \<exists>\<rhd> pd and K (is_aligned pd pd_bits) and K (vptr < kernel_base)\<rbrace> 3952 lookup_pt_slot pd vptr 3953 \<lbrace>\<lambda>rv s. \<exists>oref cref cap. caps_of_state s (oref, cref) = Some cap 3954 \<and> rv && ~~ mask pt_bits \<in> obj_refs cap \<and> is_pt_cap cap\<rbrace>, -" 3955 apply (rule hoare_post_imp_R, rule lookup_pt_slot_cap_to) 3956 apply fastforce 3957 done 3958 3959lemma lookup_pt_slot_cap_to_multiple2: 3960 "\<lbrace>invs and \<exists>\<rhd> pd and K (is_aligned pd pd_bits) and K (vptr < kernel_base) and K (is_aligned vptr 16)\<rbrace> 3961 lookup_pt_slot pd vptr 3962 \<lbrace>\<lambda>rv s. \<exists>oref cref. cte_wp_at 3963 (\<lambda>c. (\<lambda>x. x && ~~ mask pt_bits) ` (\<lambda>x. x + rv) ` set [0 , 4 .e. 0x3C] \<subseteq> obj_refs c \<and> is_pt_cap c) 3964 (oref, cref) s\<rbrace>, -" 3965 apply (rule hoare_post_imp_R, rule lookup_pt_slot_cap_to_multiple1) 3966 apply (clarsimp simp: upto_enum_step_def image_image field_simps 3967 linorder_not_le[symmetric] 3968 split: if_split_asm) 3969 apply (erule notE, erule is_aligned_no_wrap') 3970 apply simp 3971 apply (fastforce simp: cte_wp_at_caps_of_state) 3972 done 3973 3974crunch global_refs[wp]: flush_page "\<lambda>s. P (global_refs s)" 3975 (simp: global_refs_arch_update_eq crunch_simps) 3976 3977lemma page_directory_at_lookup_mask_aligned_strg: 3978 "is_aligned pd pd_bits \<and> page_directory_at pd s 3979 \<longrightarrow> page_directory_at (lookup_pd_slot pd vptr && ~~ mask pd_bits) s" 3980 by (clarsimp simp: lookup_pd_slot_pd) 3981 3982lemma page_directory_at_lookup_mask_add_aligned_strg: 3983 "is_aligned pd pd_bits \<and> page_directory_at pd s 3984 \<and> vmsz_aligned vptr ARMSuperSection 3985 \<and> x \<in> set [0, 4 .e. 0x3C] 3986 \<longrightarrow> page_directory_at (x + lookup_pd_slot pd vptr && ~~ mask pd_bits) s" 3987 by (clarsimp simp: lookup_pd_slot_add_eq vmsz_aligned_def) 3988 3989lemma dmo_ccMVA_invs[wp]: 3990 "\<lbrace>invs\<rbrace> do_machine_op (cleanByVA_PoU a b) \<lbrace>\<lambda>r. invs\<rbrace>" 3991 apply (wp dmo_invs) 3992 apply safe 3993 apply (drule_tac Q="\<lambda>_ m'. underlying_memory m' p = underlying_memory m p" 3994 in use_valid) 3995 apply ((clarsimp | wp)+)[3] 3996 apply(erule use_valid, wp no_irq_cleanByVA_PoU no_irq, assumption) 3997 done 3998 3999 4000lemma dmo_ccr_invs[wp]: 4001 "\<lbrace>invs\<rbrace> do_machine_op (cleanCacheRange_PoU a b c) \<lbrace>\<lambda>r. invs\<rbrace>" 4002 apply (wp dmo_invs) 4003 apply safe 4004 apply (drule_tac Q="\<lambda>_ m'. underlying_memory m' p = underlying_memory m p" 4005 in use_valid) 4006 apply ((clarsimp | wp)+)[3] 4007 apply(erule use_valid, wp no_irq_cleanCacheRange_PoU no_irq, assumption) 4008 done 4009 4010(* FIXME: move to Invariants_A *) 4011lemmas pte_ref_pages_simps[simp] = 4012 pte_ref_pages_def[split_simps pte.split] 4013 4014lemma ex_pt_cap_eq: 4015 "(\<exists>ref cap. caps_of_state s ref = Some cap \<and> 4016 p \<in> obj_refs cap \<and> is_pt_cap cap) = 4017 (\<exists>ref asid. caps_of_state s ref = 4018 Some (cap.ArchObjectCap (arch_cap.PageTableCap p asid)))" 4019 by (fastforce simp add: is_pt_cap_def obj_refs_def) 4020 4021lemmas lookup_pt_slot_cap_to2' = 4022 lookup_pt_slot_cap_to2[simplified ex_pt_cap_eq[simplified split_paired_Ex]] 4023 4024lemma unmap_page_invs: 4025 "\<lbrace>invs and K (asid \<le> mask asid_bits \<and> vptr < kernel_base \<and> 4026 vmsz_aligned vptr sz)\<rbrace> 4027 unmap_page sz asid vptr pptr 4028 \<lbrace>\<lambda>rv. invs\<rbrace>" 4029 apply (simp add: unmap_page_def) 4030 apply (rule hoare_pre) 4031 apply (wp flush_page_invs hoare_vcg_const_imp_lift) 4032 apply (wp hoare_drop_imp[where f="check_mapping_pptr a b c" for a b c] 4033 hoare_drop_impE_R[where R="\<lambda>x y. x && mask b = c" for b c] 4034 lookup_pt_slot_inv lookup_pt_slot_cap_to2' 4035 lookup_pt_slot_cap_to_multiple2 4036 store_pde_invs_unmap mapM_swp_store_pde_invs_unmap 4037 mapM_swp_store_pte_invs 4038 | wpc | simp)+ 4039 apply (strengthen lookup_pd_slot_kernel_mappings_strg 4040 lookup_pd_slot_kernel_mappings_set_strg 4041 not_in_global_refs_vs_lookup 4042 page_directory_at_lookup_mask_aligned_strg 4043 page_directory_at_lookup_mask_add_aligned_strg)+ 4044 apply (wp find_pd_for_asid_page_directory 4045 hoare_vcg_const_imp_lift_R hoare_vcg_const_Ball_lift_R 4046 | wp_once hoare_drop_imps)+ 4047 apply (auto simp: vmsz_aligned_def) 4048 done 4049 4050crunch cte_wp_at [wp]: unmap_page "\<lambda>s. P (cte_wp_at P' p s)" 4051 (wp: crunch_wps simp: crunch_simps) 4052 4053lemma "\<lbrace>\<lambda>s. P (vs_lookup s) (valid_pte pte s)\<rbrace> set_cap cap cptr \<lbrace>\<lambda>_ s. P (vs_lookup s) (valid_pte pte s)\<rbrace>" 4054 apply (rule hoare_lift_Pf[where f=vs_lookup]) 4055 apply (rule hoare_lift_Pf[where f="valid_pte pte"]) 4056 apply (wp set_cap.vs_lookup set_cap_valid_pte_stronger)+ 4057 done 4058 4059lemma reachable_page_table_not_global: 4060 "\<lbrakk>(ref \<rhd> p) s; valid_kernel_mappings s; valid_global_pts s; 4061 valid_vspace_objs s; valid_asid_table (arm_asid_table (arch_state s)) s\<rbrakk> 4062 \<Longrightarrow> p \<notin> set (arm_global_pts (arch_state s))" 4063 apply clarsimp 4064 apply (erule (2) vs_lookupE_alt[OF _ _ valid_asid_table_ran]) 4065 apply (clarsimp simp: valid_global_pts_def) 4066 apply (drule (1) bspec) 4067 apply (clarsimp simp: obj_at_def a_type_def) 4068 apply (clarsimp simp: valid_global_pts_def) 4069 apply (drule (1) bspec) 4070 apply (clarsimp simp: obj_at_def a_type_def) 4071 apply (clarsimp simp: valid_kernel_mappings_def valid_kernel_mappings_if_pd_def ran_def) 4072 apply (drule_tac x="ArchObj (PageDirectory pd)" in spec) 4073 apply (drule mp, erule_tac x=p\<^sub>2 in exI) 4074 apply clarsimp 4075 done 4076 4077lemma store_pte_unmap_page: 4078 "\<lbrace>(\<lambda>s. \<exists>pt. ([VSRef (vaddr >> 20) (Some APageDirectory), 4079 VSRef (asid && mask asid_low_bits) (Some AASIDPool), 4080 VSRef (ucast (asid_high_bits_of asid)) None] \<rhd> pt) s 4081 \<and> is_aligned pt pt_bits \<and> p = (pt + ((vaddr >> 12) && mask 8 << 2 )))\<rbrace> 4082 store_pte p InvalidPTE 4083 \<lbrace>\<lambda>rv s.\<not> ([VSRef ((vaddr >> 12) && mask 8) (Some APageTable), 4084 VSRef (vaddr >> 20) (Some APageDirectory), 4085 VSRef (asid && mask asid_low_bits) (Some AASIDPool), 4086 VSRef (ucast (asid_high_bits_of asid)) None] \<unrhd> pptr) s\<rbrace>" 4087 apply (simp add: store_pte_def set_pt_def set_object_def) 4088 apply (wp get_object_wp) 4089 apply (clarsimp simp: obj_at_def fun_upd_def[symmetric] vs_lookup_pages_def vs_asid_refs_def) 4090 apply (drule vs_lookup_pages1_rtrancl_iterations) 4091 apply (clarsimp simp: vs_lookup_pages1_def vs_lookup_def vs_asid_refs_def) 4092 apply (drule vs_lookup1_rtrancl_iterations) 4093 apply (clarsimp simp: vs_lookup1_def obj_at_def split: if_split_asm) 4094 apply (clarsimp simp: vs_refs_pages_def)+ 4095 apply (thin_tac "(VSRef a (Some AASIDPool), b) \<in> c" for a b c) 4096 apply (clarsimp simp: graph_of_def 4097 split: Structures_A.kernel_object.split_asm 4098 arch_kernel_obj.splits 4099 if_split_asm) 4100 apply (erule_tac P="a = c" for c in swap) 4101 apply (rule up_ucast_inj[where 'a=8 and 'b=32]) 4102 apply (subst ucast_ucast_len) 4103 apply (simp add: pt_bits_def pageBits_def 4104 is_aligned_add_helper less_le_trans[OF ucast_less] 4105 shiftl_less_t2n'[where m=8 and n=2, simplified] 4106 shiftr_less_t2n'[where m=8 and n=2, simplified] 4107 word_bits_def shiftl_shiftr_id)+ 4108 apply (clarsimp simp: graph_of_def vs_refs_def vs_refs_pages_def 4109 pde_ref_def pde_ref_pages_def pte_ref_pages_def)+ 4110 apply (simp add: pt_bits_def pageBits_def 4111 is_aligned_add_helper less_le_trans[OF ucast_less] 4112 shiftl_less_t2n'[where m=8 and n=2, simplified] 4113 shiftr_less_t2n'[where m=8 and n=2, simplified] 4114 word_bits_def shiftl_shiftr_id)+ 4115 by (clarsimp split: Structures_A.kernel_object.split_asm arch_kernel_obj.split_asm, 4116 clarsimp simp: pde_ref_def pte_ref_pages_def pde_ref_pages_def data_at_def 4117 is_aligned_add_helper less_le_trans[OF ucast_less] 4118 shiftl_less_t2n'[where m=8 and n=2, simplified] 4119 dest!: graph_ofD ucast_up_inj[where 'a=10 (*asid_low_bits*)and 'b=32, simplified] 4120 ucast_up_inj[where 'a=7 (*asid_high_bits*) and 'b=32, simplified] 4121 split: if_split_asm pde.splits pte.splits if_splits) 4122 4123crunch pd_at: flush_page "\<lambda>s. P (ko_at (ArchObj (PageDirectory pd)) x s)" 4124 (wp: crunch_wps simp: crunch_simps) 4125 4126crunch pt_at: flush_page "\<lambda>s. P (ko_at (ArchObj (PageTable pt)) x s)" 4127 (wp: crunch_wps simp: crunch_simps) 4128 4129lemma vs_lookup_pages_pteD: 4130 "([VSRef ((vaddr >> 12) && mask 8) (Some APageTable), 4131 VSRef (vaddr >> 20) (Some APageDirectory), 4132 VSRef (asid && mask asid_low_bits) (Some AASIDPool), 4133 VSRef (ucast (asid_high_bits_of asid)) None] \<unrhd> pg) s 4134 \<Longrightarrow> \<exists>ap fun pd funa pt funb. ([VSRef (ucast (asid_high_bits_of asid)) None] \<unrhd> ap) s 4135 \<and> (arm_asid_table (arch_state s)) (asid_high_bits_of asid) = Some ap 4136 \<and> ko_at (ArchObj (ASIDPool fun)) ap s 4137 \<and> ([VSRef (asid && mask asid_low_bits) (Some AASIDPool), 4138 VSRef (ucast (asid_high_bits_of asid)) None] \<unrhd> pd) s 4139 \<and> fun (ucast (asid && mask asid_low_bits)) = Some pd 4140 \<and> ko_at (ArchObj (PageDirectory funa)) pd s 4141 \<and> ([VSRef (vaddr >> 20) (Some APageDirectory), 4142 VSRef (asid && mask asid_low_bits) (Some AASIDPool), 4143 VSRef (ucast (asid_high_bits_of asid)) None] \<unrhd> pt) s 4144 \<and> pde_ref_pages (funa (ucast (vaddr >> 20))) = Some pt 4145 \<and> ko_at (ArchObj (PageTable funb)) pt s 4146 \<and> pte_ref_pages (funb (ucast ((vaddr >> 12) && mask 8 ))) = Some pg" 4147 4148 apply (frule vs_lookup_pages_2ConsD) 4149 apply clarsimp 4150 apply (frule_tac vs="[z]" for z in vs_lookup_pages_2ConsD) 4151 apply clarsimp 4152 apply (frule_tac vs="[]" in vs_lookup_pages_2ConsD) 4153 apply clarsimp 4154 apply (rule_tac x=p'b in exI) 4155 apply (frule vs_lookup_atD[OF iffD2[OF fun_cong[OF vs_lookup_pages_eq_at]]]) 4156 apply (clarsimp simp: vs_lookup_pages1_def obj_at_def vs_refs_pages_def 4157 dest!: graph_ofD 4158 split: if_split_asm) 4159 apply (clarsimp split: Structures_A.kernel_object.split_asm arch_kernel_obj.splits) 4160 apply (simp add: up_ucast_inj_eq graph_of_def kernel_mapping_slots_def kernel_base_def 4161 not_le ucast_less_ucast[symmetric, where 'a=12 and 'b=32] 4162 mask_asid_low_bits_ucast_ucast pde_ref_pages_def pte_ref_pages_def 4163 split: if_split_asm) 4164 apply (simp add: ucast_ucast_id 4165 split: pde.split_asm pte.split_asm) 4166 done 4167 4168lemma vs_lookup_pages_pdeD: 4169 "([VSRef (vaddr >> 20) (Some APageDirectory), 4170 VSRef (asid && mask asid_low_bits) (Some AASIDPool), 4171 VSRef (ucast (asid_high_bits_of asid)) None] \<unrhd> p) s 4172 \<Longrightarrow> \<exists>ap fun pd funa. ([VSRef (ucast (asid_high_bits_of asid)) None] \<unrhd> ap) s 4173 \<and> (arm_asid_table (arch_state s)) (asid_high_bits_of asid) = Some ap 4174 \<and> ko_at (ArchObj (ASIDPool fun)) ap s 4175 \<and> ([VSRef (asid && mask asid_low_bits) (Some AASIDPool), 4176 VSRef (ucast (asid_high_bits_of asid)) None] \<unrhd> pd) s 4177 \<and> fun (ucast (asid && mask asid_low_bits)) = Some pd 4178 \<and> ko_at (ArchObj (PageDirectory funa)) pd s 4179 \<and> pde_ref_pages (funa (ucast (vaddr >> 20))) = Some p" 4180 4181 apply (frule vs_lookup_pages_2ConsD) 4182 apply clarsimp 4183 apply (frule_tac vs="[]" in vs_lookup_pages_2ConsD) 4184 apply clarsimp 4185 apply (rule_tac x=p'a in exI) 4186 apply (frule vs_lookup_atD[OF iffD2[OF fun_cong[OF vs_lookup_pages_eq_at]]]) 4187 apply (clarsimp simp: vs_lookup_pages1_def obj_at_def vs_refs_pages_def 4188 dest!: graph_ofD 4189 split: if_split_asm) 4190 apply (clarsimp split: Structures_A.kernel_object.split_asm arch_kernel_obj.splits) 4191 apply (simp add: up_ucast_inj_eq graph_of_def kernel_mapping_slots_def kernel_base_def 4192 not_le ucast_less_ucast[symmetric, where 'a=12 and 'b=32] 4193 mask_asid_low_bits_ucast_ucast pde_ref_pages_def 4194 split: if_split_asm) 4195 apply (simp add: ucast_ucast_id 4196 split: pde.split_asm) 4197 done 4198 4199lemma vs_lookup_ap_mappingD: 4200 "([VSRef (asid && mask asid_low_bits) (Some AASIDPool), 4201 VSRef (ucast (asid_high_bits_of asid)) None] \<rhd> pd) s 4202 \<Longrightarrow> \<exists>ap fun. (arm_asid_table (arch_state s)) (asid_high_bits_of asid) = Some ap 4203 \<and> ko_at (ArchObj (ASIDPool fun)) ap s 4204 \<and> fun (ucast (asid && mask asid_low_bits)) = Some pd" 4205apply (clarsimp simp: vs_lookup_def vs_asid_refs_def 4206 dest!: graph_ofD vs_lookup1_rtrancl_iterations) 4207 apply (clarsimp simp: vs_lookup1_def obj_at_def vs_refs_def 4208 dest!: graph_ofD 4209 split: if_split_asm) 4210 apply (clarsimp split: Structures_A.kernel_object.split_asm arch_kernel_obj.splits) 4211 apply (simp add: up_ucast_inj_eq graph_of_def kernel_mapping_slots_def kernel_base_def 4212 not_le ucast_less_ucast[symmetric, where 'a=12 and 'b=32] 4213 mask_asid_low_bits_ucast_ucast pde_ref_pages_def pte_ref_pages_def 4214 split: if_split_asm) 4215 done 4216 4217lemma kernel_slot_impossible_vs_lookup_pages: 4218 "(ucast (vaddr >> 20)) \<in> kernel_mapping_slots \<Longrightarrow> 4219 \<not> ([VSRef ((vaddr >> 12) && mask 8) (Some APageTable), 4220 VSRef (vaddr >> 20) (Some APageDirectory), 4221 VSRef (asid && mask asid_low_bits) (Some AASIDPool), 4222 VSRef (ucast (asid_high_bits_of asid)) None] \<unrhd> pptr) s" 4223 apply (clarsimp simp: vs_lookup_pages_def vs_asid_refs_def 4224 dest!: vs_lookup_pages1_rtrancl_iterations) 4225 apply (clarsimp simp: vs_lookup_pages1_def obj_at_def vs_refs_pages_def) 4226 apply (clarsimp simp: ucast_ucast_id 4227 dest!: graph_ofD 4228 split: Structures_A.kernel_object.split_asm arch_kernel_obj.splits 4229 if_split_asm) 4230 done 4231 4232lemma kernel_slot_impossible_vs_lookup_pages2: 4233 "(ucast (vaddr >> 20)) \<in> kernel_mapping_slots \<Longrightarrow> 4234 \<not> ([VSRef (vaddr >> 20) (Some APageDirectory), 4235 VSRef (asid && mask asid_low_bits) (Some AASIDPool), 4236 VSRef (ucast (asid_high_bits_of asid)) None] \<unrhd> pptr) s" 4237 apply (clarsimp simp: vs_lookup_pages_def vs_asid_refs_def 4238 dest!: vs_lookup_pages1_rtrancl_iterations) 4239 apply (clarsimp simp: vs_lookup_pages1_def obj_at_def vs_refs_pages_def) 4240 apply (clarsimp simp: ucast_ucast_id 4241 dest!: graph_ofD 4242 split: Structures_A.kernel_object.split_asm arch_kernel_obj.splits 4243 if_split_asm) 4244 done 4245 4246lemma pt_aligned: 4247 "\<lbrakk>page_table_at pt s; pspace_aligned s\<rbrakk> 4248 \<Longrightarrow> is_aligned pt 10" 4249 by (auto simp: obj_at_def pspace_aligned_def pt_bits_def pageBits_def dom_def) 4250 4251lemma vaddr_segment_nonsense: 4252 "is_aligned (p :: word32) 14 \<Longrightarrow> 4253 p + (vaddr >> 20 << 2) && ~~ mask pd_bits = p" 4254 by (simp add: mask_32_max_word 4255 shiftl_less_t2n'[where m=12 and n=2, simplified] 4256 shiftr_less_t2n'[where m=12 and n=20, simplified] 4257 pd_bits_def pageBits_def 4258 is_aligned_add_helper[THEN conjunct2]) 4259 4260lemma vaddr_segment_nonsense2: 4261 "is_aligned (p :: word32) 14 \<Longrightarrow> 4262 p + (vaddr >> 20 << 2) && mask pd_bits >> 2 = vaddr >> 20" 4263 by (simp add: mask_32_max_word 4264 shiftl_less_t2n'[where m=12 and n=2, simplified] 4265 shiftr_less_t2n'[where m=12 and n=20, simplified] 4266 pd_bits_def pageBits_def 4267 is_aligned_add_helper[THEN conjunct1] 4268 triple_shift_fun) 4269 4270lemma vaddr_segment_nonsense3: 4271 "is_aligned (p :: word32) 10 \<Longrightarrow> 4272 (p + ((vaddr >> 12) && 0xFF << 2) && ~~ mask pt_bits) = p" 4273 apply (rule is_aligned_add_helper[THEN conjunct2]) 4274 apply (simp add: pt_bits_def pageBits_def)+ 4275 apply (rule shiftl_less_t2n[where m=10 and n=2, simplified, OF and_mask_less'[where n=8, unfolded mask_def, simplified]]) 4276 apply simp+ 4277 done 4278 4279lemma vaddr_segment_nonsense4: 4280 "is_aligned (p :: word32) 10 \<Longrightarrow> 4281 p + ((vaddr >> 12) && 0xFF << 2) && mask pt_bits = (vaddr >> 12) && 0xFF << 2" 4282 apply (subst is_aligned_add_helper[THEN conjunct1]) 4283 apply (simp_all add: pt_bits_def pageBits_def) 4284 apply (rule shiftl_less_t2n'[where n=2 and m=8, simplified]) 4285 apply (rule and_mask_less'[where n=8, unfolded mask_def, simplified]) 4286 apply simp+ 4287 done 4288 4289(* FIXME: move near ArchAcc_R.lookup_pt_slot_inv? *) 4290lemma lookup_pt_slot_inv_validE: 4291 "\<lbrace>P\<rbrace> lookup_pt_slot pd vptr \<lbrace>\<lambda>_. P\<rbrace>, \<lbrace>\<lambda>_. P\<rbrace>" 4292 apply (simp add: lookup_pt_slot_def) 4293 apply (wp get_pde_inv hoare_drop_imp lookup_pt_slot_inv | wpc | simp)+ 4294 done 4295 4296lemma unmap_page_no_lookup_pages: 4297 "\<lbrace>\<lambda>s. \<not> (ref \<unrhd> p) s\<rbrace> 4298 unmap_page sz asid vaddr pptr 4299 \<lbrace>\<lambda>_ s. \<not> (ref \<unrhd> p) s\<rbrace>" 4300 apply (rule hoare_pre) 4301 apply (wp store_pte_no_lookup_pages hoare_drop_imps lookup_pt_slot_inv_validE 4302 mapM_UNIV_wp store_pde_no_lookup_pages 4303 | wpc | simp add: unmap_page_def swp_def | strengthen imp_consequent)+ 4304 done 4305 4306lemma vs_refs_pages_inj: 4307 "\<lbrakk> (r, p) \<in> vs_refs_pages ko; (r, p') \<in> vs_refs_pages ko \<rbrakk> \<Longrightarrow> p = p'" 4308 by (clarsimp simp: vs_refs_pages_def up_ucast_inj_eq dest!: graph_ofD 4309 split: Structures_A.kernel_object.split_asm arch_kernel_obj.splits) 4310 4311lemma unique_vs_lookup_pages_loop: 4312 "\<lbrakk> (([r], x), a # list, p) \<in> vs_lookup_pages1 s ^^ length list; 4313 (([r'], y), a # list, p') \<in> vs_lookup_pages1 s ^^ length list; 4314 r = r' \<longrightarrow> x = y \<rbrakk> 4315 \<Longrightarrow> p = p'" 4316 apply (induct list arbitrary: a p p') 4317 apply simp 4318 apply (clarsimp simp: obj_at_def dest!: vs_lookup_pages1D) 4319 apply (erule vs_refs_pages_inj) 4320 apply fastforce 4321 done 4322 4323lemma unique_vs_lookup_pages: 4324 "\<lbrakk>(r \<unrhd> p) s; (r \<unrhd> p') s\<rbrakk> \<Longrightarrow> p = p'" 4325 apply (clarsimp simp: vs_lookup_pages_def vs_asid_refs_def 4326 dest!: graph_ofD vs_lookup_pages1_rtrancl_iterations) 4327 apply (case_tac r, simp_all) 4328 apply (erule(1) unique_vs_lookup_pages_loop) 4329 apply (clarsimp simp: up_ucast_inj_eq) 4330 done 4331 4332lemma unmap_page_unmapped: 4333 "\<lbrace>pspace_aligned and valid_vspace_objs and data_at sz pptr and 4334 valid_objs and (\<lambda>s. valid_asid_table (arm_asid_table (arch_state s)) s) and 4335 K ((sz = ARMSmallPage \<or> sz = ARMLargePage \<longrightarrow> ref = 4336 [VSRef ((vaddr >> 12) && mask 8) (Some APageTable), 4337 VSRef (vaddr >> 20) (Some APageDirectory), 4338 VSRef (asid && mask asid_low_bits) (Some AASIDPool), 4339 VSRef (ucast (asid_high_bits_of asid)) None]) \<and> 4340 (sz = ARMSection \<or> sz = ARMSuperSection \<longrightarrow> ref = 4341 [VSRef (vaddr >> 20) (Some APageDirectory), 4342 VSRef (asid && mask asid_low_bits) (Some AASIDPool), 4343 VSRef (ucast (asid_high_bits_of asid)) None]) \<and> 4344 p = pptr)\<rbrace> 4345 unmap_page sz asid vaddr pptr 4346 \<lbrace>\<lambda>rv s. \<not> (ref \<unrhd> p) s\<rbrace>" 4347 apply (rule hoare_gen_asm) 4348 4349 (* Establish that pptr reachable, otherwise trivial *) 4350 apply (rule hoare_name_pre_state2) 4351 apply (case_tac "\<not> (ref \<unrhd> p) s") 4352 apply (rule hoare_pre(1)[OF unmap_page_no_lookup_pages]) 4353 apply clarsimp+ 4354 4355 (* This should be somewhere else but isn't *) 4356 apply (subgoal_tac "\<exists>xs. [0 :: word32, 4 .e. 0x3C] = 0 # xs") 4357 prefer 2 4358 apply (simp add: upto_enum_step_def upto_enum_word upt_rec) 4359 apply (clarsimp simp: unmap_page_def lookup_pd_slot_def lookup_pt_slot_def Let_def 4360 mapM_Cons 4361 cong: option.case_cong vmpage_size.case_cong) 4362 4363 (* Establish that pde in vsref chain isn't kernel mapping, 4364 otherwise trivial *) 4365 apply (case_tac "ucast (vaddr >> 20) \<in> kernel_mapping_slots") 4366 apply (case_tac sz) 4367 apply ((clarsimp simp: kernel_slot_impossible_vs_lookup_pages | wp)+)[2] 4368 apply ((clarsimp simp: kernel_slot_impossible_vs_lookup_pages2 | wp)+)[1] 4369 apply ((clarsimp simp: kernel_slot_impossible_vs_lookup_pages2 | wp)+)[1] 4370 4371 (* Proper cases *) 4372 apply (wp store_pte_unmap_page 4373 mapM_UNIV_wp[OF store_pte_no_lookup_pages] 4374 get_pte_wp get_pde_wp store_pde_unmap_page 4375 mapM_UNIV_wp[OF store_pde_no_lookup_pages] 4376 flush_page_vs_lookup flush_page_vs_lookup_pages 4377 hoare_vcg_all_lift hoare_vcg_const_imp_lift 4378 hoare_vcg_imp_lift[OF flush_page_pd_at] 4379 hoare_vcg_imp_lift[OF flush_page_pt_at] 4380 find_pd_for_asid_lots 4381 | wpc | simp add: swp_def check_mapping_pptr_def)+ 4382 apply clarsimp 4383 apply (case_tac sz, simp_all) 4384 apply (drule vs_lookup_pages_pteD) 4385 apply (rule conjI[rotated]) 4386 apply (fastforce simp add: vs_lookup_pages_eq_ap[THEN fun_cong, symmetric]) 4387 apply clarsimp 4388 apply (frule_tac p=pd and p'=rv in unique_vs_lookup_pages, erule vs_lookup_pages_vs_lookupI) 4389 apply (frule (1) pd_aligned) 4390 apply (simp add: vaddr_segment_nonsense[where vaddr=vaddr] vaddr_segment_nonsense2[where vaddr=vaddr]) 4391 apply (frule valid_vspace_objsD) 4392 apply (clarsimp simp: obj_at_def a_type_def) 4393 apply (rule refl) 4394 apply assumption 4395 apply (simp, drule bspec, fastforce) 4396 apply (clarsimp simp: pde_ref_pages_def 4397 split: pde.splits 4398 dest!: ) 4399 apply (frule pt_aligned[rotated]) 4400 apply (simp add: obj_at_def a_type_def) 4401 apply (simp split: Structures_A.kernel_object.splits arch_kernel_obj.splits, blast) 4402 apply (clarsimp simp: obj_at_def) 4403 apply (simp add: vaddr_segment_nonsense3[where vaddr=vaddr] 4404 vaddr_segment_nonsense4[where vaddr=vaddr]) 4405 apply (drule_tac p="ptrFromPAddr x" for x in vs_lookup_vs_lookup_pagesI') 4406 apply ((simp add: obj_at_def a_type_def)+)[3] 4407 apply (frule_tac p="ptrFromPAddr a" for a in valid_vspace_objsD) 4408 apply ((simp add: obj_at_def)+)[2] 4409 apply (simp add: ) 4410 apply (intro conjI impI) 4411 apply (simp add: pt_bits_def pageBits_def mask_def) 4412 apply (erule allE[where x="(ucast ((vaddr >> 12) && mask 8))"]) 4413 apply (fastforce simp: pte_ref_pages_def mask_def obj_at_def a_type_def data_at_def 4414 shiftl_shiftr_id[where n=2, 4415 OF _ less_le_trans[OF and_mask_less'[where n=8]], 4416 unfolded mask_def word_bits_def, simplified] 4417 split: pte.splits if_splits) 4418 apply ((clarsimp simp: obj_at_def a_type_def data_at_def)+)[2] 4419 4420 apply (drule vs_lookup_pages_pteD) 4421 apply (rule conjI[rotated]) 4422 apply (fastforce simp add: vs_lookup_pages_eq_ap[THEN fun_cong, symmetric]) 4423 apply clarsimp 4424 apply (frule_tac p=pd and p'=rv in unique_vs_lookup_pages, erule vs_lookup_pages_vs_lookupI) 4425 apply (frule (1) pd_aligned) 4426 apply (simp add: vaddr_segment_nonsense[where vaddr=vaddr] vaddr_segment_nonsense2[where vaddr=vaddr]) 4427 apply (frule valid_vspace_objsD) 4428 apply (clarsimp simp: obj_at_def a_type_def) 4429 apply (rule refl) 4430 apply assumption 4431 apply (simp, drule bspec, fastforce) 4432 apply (clarsimp simp: pde_ref_pages_def 4433 split: pde.splits 4434 dest!: ) 4435 apply (frule pt_aligned[rotated]) 4436 apply (simp add: obj_at_def a_type_def) 4437 apply (simp split: Structures_A.kernel_object.splits arch_kernel_obj.splits, blast) 4438 apply (clarsimp simp: obj_at_def) 4439 apply (simp add: vaddr_segment_nonsense3[where vaddr=vaddr] 4440 vaddr_segment_nonsense4[where vaddr=vaddr]) 4441 apply (drule_tac p="ptrFromPAddr x" for x in vs_lookup_vs_lookup_pagesI') 4442 apply ((simp add: obj_at_def a_type_def)+)[3] 4443 apply (frule_tac p="ptrFromPAddr a" for a in valid_vspace_objsD) 4444 apply ((simp add: obj_at_def)+)[2] 4445 apply (simp add: ) 4446 apply (intro conjI impI) 4447 apply (simp add: pt_bits_def pageBits_def mask_def) 4448 apply (erule allE[where x="(ucast ((vaddr >> 12) && mask 8))"]) 4449 4450 apply (fastforce simp: pte_ref_pages_def mask_def obj_at_def a_type_def data_at_def 4451 shiftl_shiftr_id[where n=2, 4452 OF _ less_le_trans[OF and_mask_less'[where n=8]], 4453 unfolded mask_def word_bits_def, simplified] 4454 split: pte.splits if_splits) 4455 apply ((clarsimp simp: obj_at_def a_type_def data_at_def)+)[2] 4456 apply (drule vs_lookup_pages_pdeD) 4457 apply (rule conjI[rotated]) 4458 apply (fastforce simp add: vs_lookup_pages_eq_ap[THEN fun_cong, symmetric]) 4459 apply clarsimp 4460 apply (frule_tac p=pd and p'=rv in unique_vs_lookup_pages, erule vs_lookup_pages_vs_lookupI) 4461 apply (frule (1) pd_aligned) 4462 apply (simp add: vaddr_segment_nonsense[where vaddr=vaddr] vaddr_segment_nonsense2[where vaddr=vaddr]) 4463 apply (frule valid_vspace_objsD) 4464 apply (clarsimp simp: obj_at_def a_type_def) 4465 apply (rule refl) 4466 apply assumption 4467 apply (simp, drule bspec, fastforce) 4468 apply (clarsimp simp: pde_ref_pages_def 4469 split: pde.splits) 4470 apply (clarsimp simp: obj_at_def data_at_def) 4471 apply (drule_tac p="rv" in vs_lookup_vs_lookup_pagesI') 4472 apply ((simp add: obj_at_def a_type_def)+)[3] 4473 apply (frule_tac p="rv" in valid_vspace_objsD) 4474 apply ((simp add: obj_at_def)+)[2] 4475 apply (fastforce simp: data_at_def) 4476 apply (fastforce simp: obj_at_def a_type_def pd_bits_def pageBits_def data_at_def 4477 split: pde.splits) 4478 apply (fastforce simp: obj_at_def a_type_def data_at_def) 4479 4480 apply (drule vs_lookup_pages_pdeD) 4481 apply (rule conjI[rotated]) 4482 apply (fastforce simp add: vs_lookup_pages_eq_ap[THEN fun_cong, symmetric]) 4483 apply clarsimp 4484 apply (frule_tac p=pd and p'=rv in unique_vs_lookup_pages, erule vs_lookup_pages_vs_lookupI) 4485 apply (frule (1) pd_aligned) 4486 apply (simp add: vaddr_segment_nonsense[where vaddr=vaddr] vaddr_segment_nonsense2[where vaddr=vaddr]) 4487 apply (frule valid_vspace_objsD) 4488 apply (clarsimp simp: obj_at_def a_type_def) 4489 apply (rule refl) 4490 apply assumption 4491 apply (simp, drule bspec, fastforce) 4492 apply (clarsimp simp: pde_ref_pages_def 4493 split: pde.splits) 4494 apply (fastforce simp: obj_at_def data_at_def) 4495 apply (drule_tac p="rv" in vs_lookup_vs_lookup_pagesI') 4496 apply ((simp add: obj_at_def a_type_def)+)[3] 4497 apply (frule_tac p="rv" in valid_vspace_objsD) 4498 apply ((simp add: obj_at_def)+)[2] 4499 apply (simp add: ) 4500 apply (drule bspec[where x="ucast (vaddr >> 20)"], simp) 4501 apply (fastforce simp: obj_at_def a_type_def pd_bits_def pageBits_def data_at_def 4502 split: pde.splits) 4503 apply (clarsimp simp: obj_at_def a_type_def pd_bits_def pageBits_def) 4504 done 4505 4506lemma unmap_page_page_unmapped: 4507 "\<lbrace>pspace_aligned and valid_objs and valid_vspace_objs and 4508 (\<lambda>s. valid_asid_table (arm_asid_table (arch_state s)) s) and 4509 data_at sz pptr and 4510 K (p = pptr) and K (sz = ARMSmallPage \<or> sz = ARMLargePage)\<rbrace> 4511 unmap_page sz asid vaddr pptr 4512 \<lbrace>\<lambda>rv s. \<not> ([VSRef ((vaddr >> 12) && mask 8) (Some APageTable), 4513 VSRef (vaddr >> 20) (Some APageDirectory), 4514 VSRef (asid && mask asid_low_bits) (Some AASIDPool), 4515 VSRef (ucast (asid_high_bits_of asid)) None] \<unrhd> p) s\<rbrace>" 4516 by (rule hoare_pre_imp[OF _ unmap_page_unmapped]) auto 4517 4518lemma unmap_page_section_unmapped: 4519 "\<lbrace>pspace_aligned and valid_objs and valid_vspace_objs and 4520 (\<lambda>s. valid_asid_table (arm_asid_table (arch_state s)) s) and 4521 data_at sz pptr and 4522 K (p = pptr) and K (sz = ARMSection \<or> sz = ARMSuperSection)\<rbrace> 4523 unmap_page sz asid vaddr pptr 4524 \<lbrace>\<lambda>rv s. \<not> ([VSRef (vaddr >> 20) (Some APageDirectory), 4525 VSRef (asid && mask asid_low_bits) (Some AASIDPool), 4526 VSRef (ucast (asid_high_bits_of asid)) None] \<unrhd> p) s\<rbrace>" 4527 by (rule hoare_pre_imp[OF _ unmap_page_unmapped]) auto 4528 4529crunch global_refs: store_pde "\<lambda>s. P (global_refs s)" 4530 4531crunch invs[wp]: pte_check_if_mapped, pde_check_if_mapped "invs" 4532 4533crunch vs_lookup[wp]: pte_check_if_mapped, pde_check_if_mapped "\<lambda>s. P (vs_lookup s)" 4534 4535crunch valid_pte[wp]: pte_check_if_mapped "\<lambda>s. P (valid_pte p s)" 4536 4537lemma set_mi_invs[wp]: "\<lbrace>invs\<rbrace> set_message_info t a \<lbrace>\<lambda>x. invs\<rbrace>" 4538 by (simp add: set_message_info_def, wp) 4539 4540lemma data_at_orth: 4541 "data_at a p s \<Longrightarrow> \<not> ep_at p s 4542 \<and> \<not> ntfn_at p s \<and>\<not> cap_table_at sz p s \<and> \<not> tcb_at p s \<and> \<not> asid_pool_at p s 4543 \<and> \<not> page_table_at p s \<and> \<not> page_directory_at p s \<and> \<not> asid_pool_at p s" 4544 apply (clarsimp simp: data_at_def obj_at_def a_type_def) 4545 apply (case_tac "kheap s p",simp) 4546 subgoal for ko 4547 by (case_tac ko,auto simp add: is_ep_def is_ntfn_def is_cap_table_def is_tcb_def) 4548 done 4549 4550lemma data_at_pg_cap: 4551 "\<lbrakk>data_at sz p s;valid_cap cap s; p \<in> obj_refs cap\<rbrakk> \<Longrightarrow> is_pg_cap cap" 4552 apply (case_tac cap) 4553 apply (clarsimp simp: is_pg_cap_def obj_refs.simps valid_cap_def 4554 data_at_orth split option.split)+ 4555 apply (clarsimp split: arch_cap.split_asm simp: data_at_orth) 4556 done 4557 4558lemma perform_page_invs [wp]: 4559 "\<lbrace>invs and valid_page_inv pg_inv\<rbrace> perform_page_invocation pg_inv \<lbrace>\<lambda>_. invs\<rbrace>" 4560 apply (simp add: perform_page_invocation_def) 4561 apply (cases pg_inv, simp_all) 4562 \<comment> \<open>PageMap\<close> 4563 apply (rename_tac asid cap cslot_ptr sum) 4564 apply clarsimp 4565 apply (rule hoare_pre) 4566 apply (wp get_master_pte_wp get_master_pde_wp mapM_swp_store_pde_invs_unmap store_pde_invs_unmap' hoare_vcg_const_imp_lift hoare_vcg_all_lift set_cap_arch_obj arch_update_cap_invs_map 4567 | wpc 4568 | simp add: pte_check_if_mapped_def pde_check_if_mapped_def del: fun_upd_apply 4569 | subst cte_wp_at_caps_of_state)+ 4570 apply (wp_once hoare_drop_imp) 4571 apply (wp arch_update_cap_invs_map) 4572 apply (rule hoare_vcg_conj_lift) 4573 apply (rule hoare_lift_Pf[where f=vs_lookup, OF _ set_cap.vs_lookup]) 4574 apply (rule_tac f="valid_pte xa" in hoare_lift_Pf[OF _ set_cap_valid_pte_stronger]) 4575 apply wp 4576 apply (rule hoare_lift_Pf2[where f=vs_lookup, OF _ set_cap.vs_lookup]) 4577 apply ((wp dmo_ccr_invs arch_update_cap_invs_map 4578 hoare_vcg_const_Ball_lift 4579 hoare_vcg_const_imp_lift hoare_vcg_all_lift set_cap_typ_at 4580 hoare_vcg_ex_lift hoare_vcg_ball_lift set_cap_arch_obj 4581 set_cap.vs_lookup 4582 | wpc | simp add: same_refs_def del: fun_upd_apply split del: if_split 4583 | subst cte_wp_at_caps_of_state)+) 4584 apply (wp_once hoare_drop_imp) 4585 apply (wp arch_update_cap_invs_map hoare_vcg_ex_lift set_cap_arch_obj) 4586 apply (clarsimp simp: valid_page_inv_def cte_wp_at_caps_of_state neq_Nil_conv 4587 valid_slots_def empty_refs_def parent_for_refs_def 4588 simp del: fun_upd_apply del: exE 4589 split: sum.splits) 4590 apply (rule conjI) 4591 apply (clarsimp simp: is_cap_simps is_arch_update_def 4592 cap_master_cap_simps 4593 dest!: cap_master_cap_eqDs) 4594 apply clarsimp 4595 apply (rule conjI) 4596 apply (rule_tac x=aa in exI, rule_tac x=ba in exI) 4597 apply (rule conjI) 4598 apply (clarsimp simp: is_arch_update_def is_pt_cap_def is_pg_cap_def 4599 cap_master_cap_def image_def 4600 split: Structures_A.cap.splits arch_cap.splits) 4601 apply (clarsimp simp: is_pt_cap_def cap_asid_def image_def neq_Nil_conv Collect_disj_eq 4602 split: Structures_A.cap.splits arch_cap.splits option.splits) 4603 apply (rule conjI) 4604 apply (drule same_refs_lD) 4605 apply clarsimp 4606 apply fastforce 4607 apply (rule_tac x=aa in exI, rule_tac x=ba in exI) 4608 apply (clarsimp simp: is_arch_update_def 4609 cap_master_cap_def is_cap_simps 4610 split: Structures_A.cap.splits arch_cap.splits) 4611 apply (rule conjI) 4612 apply (erule exEI) 4613 apply clarsimp 4614 apply (rule conjI) 4615 apply clarsimp 4616 apply (rule_tac x=aa in exI, rule_tac x=ba in exI) 4617 apply (clarsimp simp: is_arch_update_def 4618 cap_master_cap_def is_cap_simps 4619 split: Structures_A.cap.splits arch_cap.splits) 4620 apply (rule conjI) 4621 apply (rule_tac x=a in exI, rule_tac x=b in exI, rule_tac x=cap in exI) 4622 apply (clarsimp simp: same_refs_def) 4623 apply (rule conjI) 4624 apply (clarsimp simp: pde_at_def obj_at_def 4625 caps_of_state_cteD'[where P=\<top>, simplified]) 4626 apply (drule_tac cap=capc and ptr="(aa,ba)" 4627 in valid_global_refsD[OF invs_valid_global_refs]) 4628 apply assumption+ 4629 apply (clarsimp simp: cap_range_def) 4630 apply (clarsimp) 4631 apply (rule conjI) 4632 apply (clarsimp simp: pde_at_def obj_at_def a_type_def) 4633 apply (clarsimp split: Structures_A.kernel_object.split_asm 4634 if_split_asm arch_kernel_obj.splits) 4635 apply (erule ballEI) 4636 apply (clarsimp simp: pde_at_def obj_at_def 4637 caps_of_state_cteD'[where P=\<top>, simplified]) 4638 apply (drule_tac cap=capc and ptr="(aa,ba)" 4639 in valid_global_refsD[OF invs_valid_global_refs]) 4640 apply assumption+ 4641 apply (drule_tac x=sl in imageI[where f="\<lambda>x. x && ~~ mask pd_bits"]) 4642 apply (drule (1) subsetD) 4643 apply (clarsimp simp: cap_range_def) 4644 \<comment> \<open>PageRemap\<close> 4645 apply (rule hoare_pre) 4646 apply (wp get_master_pte_wp get_master_pde_wp hoare_vcg_ex_lift mapM_x_swp_store_pde_invs_unmap 4647 | wpc | simp add: pte_check_if_mapped_def pde_check_if_mapped_def 4648 | (rule hoare_vcg_conj_lift, rule_tac slots=x2a in store_pde_invs_unmap'))+ 4649 apply (clarsimp simp: valid_page_inv_def cte_wp_at_caps_of_state 4650 valid_slots_def empty_refs_def neq_Nil_conv 4651 split: sum.splits) 4652 apply (clarsimp simp: parent_for_refs_def same_refs_def is_cap_simps cap_asid_def split: option.splits) 4653 apply (rule conjI, fastforce) 4654 apply (rule conjI) 4655 apply clarsimp 4656 apply (rule_tac x=ac in exI, rule_tac x=bc in exI, rule_tac x=capa in exI) 4657 apply clarsimp 4658 apply (erule (2) ref_is_unique[OF _ _ reachable_page_table_not_global]) 4659 apply ((simp add: invs_def valid_state_def valid_arch_state_def 4660 valid_arch_caps_def valid_pspace_def valid_objs_caps)+)[9] 4661 apply fastforce 4662 apply( frule valid_global_refsD2) 4663 apply (clarsimp simp: cap_range_def parent_for_refs_def)+ 4664 apply (rule conjI, rule impI) 4665 apply (rule exI, rule exI, rule exI) 4666 apply (erule conjI) 4667 apply clarsimp 4668 apply (rule conjI, rule impI) 4669 apply (rule_tac x=ac in exI, rule_tac x=bc in exI, rule_tac x=capa in exI) 4670 apply (clarsimp simp: same_refs_def pde_ref_def pde_ref_pages_def 4671 valid_pde_def invs_def valid_state_def valid_pspace_def) 4672 apply (drule valid_objs_caps) 4673 apply (clarsimp simp: valid_caps_def) 4674 apply (drule spec, drule spec, drule_tac x=capa in spec, drule (1) mp) 4675 apply (case_tac aa, (clarsimp simp add: data_at_pg_cap)+)[1] 4676 apply (clarsimp simp: pde_at_def obj_at_def a_type_def) 4677 4678 apply (rule conjI) 4679 apply clarsimp 4680 apply (drule_tac ptr="(ab,bb)" in 4681 valid_global_refsD[OF invs_valid_global_refs caps_of_state_cteD]) 4682 apply simp+ 4683 apply force 4684 apply (erule ballEI) 4685 apply clarsimp 4686 apply (drule_tac ptr="(ab,bb)" in 4687 valid_global_refsD[OF invs_valid_global_refs caps_of_state_cteD]) 4688 apply simp+ 4689 apply force 4690 4691 \<comment> \<open>PageUnmap\<close> 4692 apply (rename_tac arch_cap cslot_ptr) 4693 apply (rule hoare_pre) 4694 apply (wp dmo_invs arch_update_cap_invs_unmap_page get_cap_wp 4695 hoare_vcg_const_imp_lift | wpc | simp)+ 4696 apply (rule_tac Q="\<lambda>_ s. invs s \<and> 4697 cte_wp_at (\<lambda>c. is_pg_cap c \<and> 4698 (\<forall>ref. vs_cap_ref c = Some ref \<longrightarrow> 4699 \<not> (ref \<unrhd> obj_ref_of c) s)) cslot_ptr s" 4700 in hoare_strengthen_post) 4701 prefer 2 4702 apply (clarsimp simp: cte_wp_at_caps_of_state is_cap_simps 4703 update_map_data_def 4704 is_arch_update_def cap_master_cap_simps) 4705 apply (drule caps_of_state_valid, fastforce) 4706 apply (clarsimp simp: valid_cap_def cap_aligned_def vs_cap_ref_def 4707 split: option.splits vmpage_size.splits cap.splits) 4708 apply (simp add: cte_wp_at_caps_of_state) 4709 apply (wp unmap_page_invs hoare_vcg_ex_lift hoare_vcg_all_lift 4710 hoare_vcg_imp_lift unmap_page_unmapped)+ 4711 apply (clarsimp simp: valid_page_inv_def cte_wp_at_caps_of_state) 4712 apply (clarsimp simp: is_arch_diminished_def) 4713 apply (drule (2) diminished_is_update') 4714 apply (clarsimp simp: is_cap_simps cap_master_cap_simps is_arch_update_def 4715 update_map_data_def cap_rights_update_def 4716 acap_rights_update_def) 4717 using valid_validate_vm_rights[simplified valid_vm_rights_def] 4718 apply (auto simp: valid_cap_def cap_aligned_def mask_def vs_cap_ref_def data_at_def 4719 split: vmpage_size.splits option.splits if_splits)[1] 4720 4721 \<comment> \<open>PageFlush\<close> 4722 apply (rule hoare_pre) 4723 apply (wp dmo_invs set_vm_root_for_flush_invs 4724 hoare_vcg_const_imp_lift hoare_vcg_all_lift 4725 | simp)+ 4726 apply (rule hoare_pre_imp[of _ \<top>], assumption) 4727 apply (clarsimp simp: valid_def) 4728 apply (thin_tac "p \<in> fst (set_vm_root_for_flush a b s)" for p a b) 4729 apply(safe) 4730 apply (drule_tac Q="\<lambda>_ m'. underlying_memory m' p = underlying_memory m p" 4731 in use_valid) 4732 apply ((clarsimp | wp)+)[3] 4733 apply(erule use_valid, wp no_irq_do_flush no_irq, assumption) 4734 apply(wp set_vm_root_for_flush_invs | simp add: valid_page_inv_def tcb_at_invs)+ 4735 done 4736 4737end 4738 4739locale asid_pool_map = Arch + 4740 fixes s ap pool asid pdp pd s' 4741 defines "(s' :: ('a::state_ext) state) \<equiv> 4742 s\<lparr>kheap := kheap s(ap \<mapsto> ArchObj (ASIDPool 4743 (pool(asid \<mapsto> pdp))))\<rparr>" 4744 assumes ap: "kheap s ap = Some (ArchObj (ASIDPool pool))" 4745 assumes new: "pool asid = None" 4746 assumes pd: "kheap s pdp = Some (ArchObj (PageDirectory pd))" 4747 assumes pde: "empty_table (set (second_level_tables (arch_state s))) 4748 (ArchObj (PageDirectory pd))" 4749begin 4750 4751definition 4752 "new_lookups \<equiv> 4753 {((rs,p),(rs',p')). rs' = VSRef (ucast asid) (Some AASIDPool) # rs \<and> 4754 p = ap \<and> p' = pdp}" 4755 4756lemma vs_lookup1: 4757 "vs_lookup1 s' = vs_lookup1 s \<union> new_lookups" 4758 using pde pd new ap 4759 apply (clarsimp simp: vs_lookup1_def new_lookups_def) 4760 apply (rule set_eqI) 4761 apply (clarsimp simp: obj_at_def s'_def vs_refs_def graph_of_def) 4762 apply (rule iffI) 4763 apply (clarsimp simp: image_def split: if_split_asm) 4764 apply fastforce 4765 apply fastforce 4766 done 4767 4768lemma vs_lookup_trans: 4769 "(vs_lookup1 s')^* = (vs_lookup1 s)^* \<union> (vs_lookup1 s)^* O new_lookups^*" 4770 using pd pde 4771 apply (simp add: vs_lookup1) 4772 apply (rule union_trans) 4773 apply (subst (asm) new_lookups_def) 4774 apply (clarsimp simp: vs_lookup1_def obj_at_def vs_refs_def graph_of_def 4775 empty_table_def pde_ref_def 4776 split: if_split_asm) 4777 done 4778 4779lemma arch_state [simp]: 4780 "arch_state s' = arch_state s" 4781 by (simp add: s'_def) 4782 4783lemma new_lookups_rtrancl: 4784 "new_lookups^* = Id \<union> new_lookups" 4785 using ap pd 4786 apply - 4787 apply (rule set_eqI) 4788 apply clarsimp 4789 apply (rule iffI) 4790 apply (erule rtrancl_induct2) 4791 apply clarsimp 4792 apply (clarsimp del: disjCI) 4793 apply (erule disjE) 4794 apply clarsimp 4795 apply (thin_tac "x \<in> R^*" for x R) 4796 apply (subgoal_tac "False", simp+) 4797 apply (clarsimp simp: new_lookups_def) 4798 apply (erule disjE, simp+) 4799 done 4800 4801lemma vs_lookup: 4802 "vs_lookup s' = vs_lookup s \<union> new_lookups^* `` vs_lookup s" 4803 unfolding vs_lookup_def 4804 by (simp add: vs_lookup_trans relcomp_Image Un_Image) 4805 4806lemma vs_lookup2: 4807 "vs_lookup s' = vs_lookup s \<union> (new_lookups `` vs_lookup s)" 4808 by (auto simp add: vs_lookup new_lookups_rtrancl) 4809 4810lemma vs_lookup_pages1: 4811 "vs_lookup_pages1 s' = vs_lookup_pages1 s \<union> new_lookups" 4812 using pde pd new ap 4813 apply (clarsimp simp: vs_lookup_pages1_def new_lookups_def) 4814 apply (rule set_eqI) 4815 apply (clarsimp simp: obj_at_def s'_def vs_refs_pages_def graph_of_def) 4816 apply (rule iffI) 4817 apply (clarsimp simp: image_def split: if_split_asm) 4818 apply fastforce 4819 apply fastforce 4820 done 4821 4822lemma vs_lookup_pages_trans: 4823 "(vs_lookup_pages1 s')^* = 4824 (vs_lookup_pages1 s)^* \<union> (vs_lookup_pages1 s)^* O new_lookups^*" 4825 using pd pde 4826 apply (simp add: vs_lookup_pages1) 4827 apply (rule union_trans) 4828 apply (subst (asm) new_lookups_def) 4829 apply (clarsimp simp: vs_lookup_pages1_def obj_at_def vs_refs_pages_def 4830 graph_of_def empty_table_def pde_ref_pages_def 4831 split: if_split_asm) 4832 done 4833 4834lemma vs_lookup_pages: 4835 "vs_lookup_pages s' = 4836 vs_lookup_pages s \<union> new_lookups^* `` vs_lookup_pages s" 4837 unfolding vs_lookup_pages_def 4838 by (simp add: vs_lookup_pages_trans relcomp_Image Un_Image) 4839 4840lemma vs_lookup_pages2: 4841 "vs_lookup_pages s' = vs_lookup_pages s \<union> (new_lookups `` vs_lookup_pages s)" 4842 by (auto simp add: vs_lookup_pages new_lookups_rtrancl) 4843 4844end 4845 4846context Arch begin global_naming ARM 4847 4848lemma not_kernel_slot_not_global_pt: 4849 "\<lbrakk>pde_ref (pd x) = Some p; x \<notin> kernel_mapping_slots; 4850 kheap s p' = Some (ArchObj (PageDirectory pd)); valid_kernel_mappings s\<rbrakk> 4851 \<Longrightarrow> p \<notin> set (second_level_tables (arch_state s))" 4852 apply (clarsimp simp: valid_kernel_mappings_def valid_kernel_mappings_if_pd_def) 4853 apply (drule_tac x="ArchObj (PageDirectory pd)" in bspec) 4854 apply ((fastforce simp: ran_def)+)[1] 4855 apply (simp add: second_level_tables_def split: arch_kernel_obj.split_asm) 4856 done 4857 4858lemma set_asid_pool_arch_objs_map: 4859 "\<lbrace>valid_vspace_objs and valid_arch_state and valid_global_objs and 4860 valid_kernel_mappings and 4861 ko_at (ArchObj (ASIDPool pool)) ap and 4862 K (pool asid = None) and 4863 \<exists>\<rhd> ap and page_directory_at pd and 4864 (\<lambda>s. obj_at (empty_table (set (second_level_tables (arch_state s)))) pd s) \<rbrace> 4865 set_asid_pool ap (pool(asid \<mapsto> pd)) 4866 \<lbrace>\<lambda>rv. valid_vspace_objs\<rbrace>" 4867 apply (simp add: set_asid_pool_def set_object_def) 4868 apply (wp get_object_wp) 4869 apply (clarsimp simp del: fun_upd_apply 4870 split: Structures_A.kernel_object.splits arch_kernel_obj.splits) 4871 apply (frule (2) valid_vspace_objsD) 4872 apply (clarsimp simp: valid_vspace_objs_def simp del: valid_vspace_obj.simps) 4873 apply (case_tac "p = ap") 4874 apply (clarsimp simp: obj_at_def 4875 simp del: fun_upd_apply valid_vspace_obj.simps) 4876 apply (clarsimp simp: ran_def) 4877 apply (case_tac "a = asid") 4878 apply clarsimp 4879 apply (rule typ_at_same_type) 4880 apply (simp add: obj_at_def a_type_simps) 4881 prefer 2 4882 apply assumption 4883 apply (simp add: a_type_def) 4884 apply clarsimp 4885 apply (erule allE, erule impE, rule exI, assumption)+ 4886 apply (erule typ_at_same_type) 4887 prefer 2 4888 apply assumption 4889 apply (simp add: a_type_def) 4890 apply (clarsimp simp: obj_at_def a_type_simps) 4891 apply (frule (3) asid_pool_map.intro) 4892 apply (subst (asm) asid_pool_map.vs_lookup, assumption) 4893 apply clarsimp 4894 apply (erule disjE) 4895 apply (erule_tac x=p in allE, simp) 4896 apply (erule impE, blast) 4897 apply (erule valid_vspace_obj_same_type) 4898 apply (simp add: obj_at_def a_type_def) 4899 apply (simp add: a_type_def) 4900 apply (clarsimp simp: asid_pool_map.new_lookups_rtrancl) 4901 apply (erule disjE) 4902 apply clarsimp 4903 apply (erule_tac x=p in allE, simp) 4904 apply (erule impE, blast) 4905 apply (erule valid_vspace_obj_same_type) 4906 apply (simp add: obj_at_def a_type_def) 4907 apply (simp add: a_type_def) 4908 apply (clarsimp simp: asid_pool_map.new_lookups_def empty_table_def) 4909 done 4910 4911lemma obj_at_not_pt_not_in_global_pts: 4912 "\<lbrakk> obj_at P p s; valid_arch_state s; valid_global_objs s; \<And>pt. \<not> P (ArchObj (PageTable pt)) \<rbrakk> 4913 \<Longrightarrow> p \<notin> set (second_level_tables (arch_state s))" 4914 unfolding second_level_tables_def 4915 apply (rule notI, drule(1) valid_global_ptsD) 4916 apply (clarsimp simp: obj_at_def) 4917 done 4918 4919lemma set_asid_pool_valid_arch_caps_map: 4920 "\<lbrace>valid_arch_caps and valid_arch_state and valid_global_objs and valid_objs 4921 and valid_vspace_objs and ko_at (ArchObj (ASIDPool pool)) ap 4922 and (\<lambda>s. \<exists>rf. (rf \<rhd> ap) s \<and> (\<exists>ptr cap. caps_of_state s ptr = Some cap 4923 \<and> pd \<in> obj_refs cap \<and> vs_cap_ref cap = Some ((VSRef (ucast asid) (Some AASIDPool)) # rf)) 4924 \<and> (VSRef (ucast asid) (Some AASIDPool) # rf \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None])) 4925 and page_directory_at pd 4926 and (\<lambda>s. obj_at (empty_table (set (second_level_tables (arch_state s)))) pd s) 4927 and K (pool asid = None)\<rbrace> 4928 set_asid_pool ap (pool(asid \<mapsto> pd)) 4929 \<lbrace>\<lambda>rv. valid_arch_caps\<rbrace>" 4930 apply (simp add: set_asid_pool_def set_object_def) 4931 apply (wp get_object_wp) 4932 apply clarsimp 4933 apply (frule obj_at_not_pt_not_in_global_pts[where p=pd], clarsimp+) 4934 apply (simp add: a_type_def) 4935 apply (frule obj_at_not_pt_not_in_global_pts[where p=ap], clarsimp+) 4936 apply (clarsimp simp: obj_at_def valid_arch_caps_def 4937 caps_of_state_after_update) 4938 apply (clarsimp simp: a_type_def 4939 split: Structures_A.kernel_object.split_asm if_split_asm 4940 arch_kernel_obj.split_asm) 4941 apply (frule(3) asid_pool_map.intro) 4942 apply (simp add: fun_upd_def[symmetric]) 4943 apply (rule conjI) 4944 apply (simp add: valid_vs_lookup_def 4945 caps_of_state_after_update[folded fun_upd_def] 4946 obj_at_def) 4947 apply (subst asid_pool_map.vs_lookup_pages2, assumption) 4948 apply simp 4949 apply (clarsimp simp: asid_pool_map.new_lookups_def) 4950 apply (frule(2) vs_lookup_vs_lookup_pagesI, simp add: valid_arch_state_def) 4951 apply (simp add: second_level_tables_def) 4952 apply (drule(2) ref_is_unique) 4953 apply (simp add: valid_vs_lookup_def) 4954 apply clarsimp+ 4955 apply (simp add: valid_arch_state_def) 4956 apply (rule valid_objs_caps, simp) 4957 apply fastforce 4958 apply (simp add: valid_table_caps_def 4959 caps_of_state_after_update[folded fun_upd_def] obj_at_def 4960 del: imp_disjL) 4961 apply (clarsimp simp del: imp_disjL) 4962 apply (drule(1) caps_of_state_valid_cap)+ 4963 apply (auto simp add: valid_cap_def is_pt_cap_def is_pd_cap_def obj_at_def 4964 a_type_def)[1] 4965 done 4966 4967lemma set_asid_pool_asid_map: 4968 "\<lbrace>valid_asid_map and ko_at (ArchObj (ASIDPool pool)) ap 4969 and K (pool asid = None)\<rbrace> 4970 set_asid_pool ap (pool(asid \<mapsto> pd)) 4971 \<lbrace>\<lambda>rv. valid_asid_map\<rbrace>" 4972 apply (simp add: set_asid_pool_def set_object_def) 4973 apply (wp get_object_wp) 4974 apply clarsimp 4975 apply (clarsimp split: Structures_A.kernel_object.split_asm arch_kernel_obj.split_asm) 4976 apply (clarsimp simp: obj_at_def) 4977 apply (clarsimp simp: valid_asid_map_def) 4978 apply (drule bspec, blast) 4979 apply (clarsimp simp: vspace_at_asid_def) 4980 apply (drule vs_lookup_2ConsD) 4981 apply clarsimp 4982 apply (erule vs_lookup_atE) 4983 apply (drule vs_lookup1D) 4984 apply clarsimp 4985 apply (case_tac "p'=ap") 4986 apply (clarsimp simp: obj_at_def) 4987 apply (rule vs_lookupI) 4988 apply (clarsimp simp: vs_asid_refs_def graph_of_def) 4989 apply fastforce 4990 apply (rule r_into_rtrancl) 4991 apply (rule_tac r="VSRef (a && mask asid_low_bits) (Some AASIDPool)" in vs_lookup1I) 4992 apply (simp add: obj_at_def) 4993 apply (simp add: vs_refs_def graph_of_def) 4994 apply fastforce 4995 apply simp 4996 apply (rule vs_lookupI) 4997 apply (clarsimp simp: vs_asid_refs_def graph_of_def) 4998 apply fastforce 4999 apply (rule r_into_rtrancl) 5000 apply (rule vs_lookup1I) 5001 apply (simp add: obj_at_def) 5002 apply simp 5003 apply simp 5004 done 5005 5006lemma set_asid_pool_invs_map: 5007 "\<lbrace>invs and ko_at (ArchObj (ASIDPool pool)) ap 5008 and (\<lambda>s. \<exists>rf. (rf \<rhd> ap) s \<and> (\<exists>ptr cap. caps_of_state s ptr = Some cap 5009 \<and> pd \<in> obj_refs cap \<and> vs_cap_ref cap = Some ((VSRef (ucast asid) (Some AASIDPool)) # rf)) 5010 \<and> (VSRef (ucast asid) (Some AASIDPool) # rf \<noteq> [VSRef 0 (Some AASIDPool), VSRef 0 None])) 5011 and page_directory_at pd 5012 and (\<lambda>s. obj_at (empty_table (set (second_level_tables (arch_state s)))) pd s) 5013 and K (pool asid = None)\<rbrace> 5014 set_asid_pool ap (pool(asid \<mapsto> pd)) 5015 \<lbrace>\<lambda>rv. invs\<rbrace>" 5016 apply (simp add: invs_def valid_state_def valid_pspace_def) 5017 apply (rule hoare_pre, wp valid_irq_node_typ set_asid_pool_typ_at set_asid_pool_arch_objs_map valid_irq_handlers_lift 5018 set_asid_pool_valid_arch_caps_map set_asid_pool_asid_map) 5019 apply clarsimp 5020 apply auto 5021 done 5022 5023lemma perform_asid_pool_invs [wp]: 5024 "\<lbrace>invs and valid_apinv api\<rbrace> perform_asid_pool_invocation api \<lbrace>\<lambda>_. invs\<rbrace>" 5025 apply (clarsimp simp: perform_asid_pool_invocation_def split: asid_pool_invocation.splits) 5026 apply (wp arch_update_cap_invs_map set_asid_pool_invs_map 5027 get_cap_wp set_cap_typ_at 5028 empty_table_lift[unfolded pred_conj_def, OF _ set_cap_obj_at_other] 5029 set_cap_obj_at_other 5030 |wpc|simp|wp_once hoare_vcg_ex_lift)+ 5031 apply (clarsimp simp: valid_apinv_def cte_wp_at_caps_of_state is_arch_update_def is_cap_simps cap_master_cap_simps) 5032 apply (frule caps_of_state_cteD) 5033 apply (drule cte_wp_valid_cap, fastforce) 5034 apply (simp add: valid_cap_def cap_aligned_def) 5035 apply (clarsimp simp: cap_asid_def split: option.splits) 5036 apply (rule conjI) 5037 apply (clarsimp simp: vs_cap_ref_def) 5038 apply (rule conjI) 5039 apply (erule vs_lookup_atE) 5040 apply clarsimp 5041 apply (drule caps_of_state_cteD) 5042 apply (clarsimp simp: cte_wp_at_cases obj_at_def) 5043 apply (rule conjI) 5044 apply (rule exI) 5045 apply (rule conjI, assumption) 5046 apply (rule conjI) 5047 apply (rule_tac x=a in exI) 5048 apply (rule_tac x=b in exI) 5049 apply (clarsimp simp: vs_cap_ref_def mask_asid_low_bits_ucast_ucast) 5050 apply (clarsimp simp: asid_low_bits_def[symmetric] ucast_ucast_mask 5051 word_neq_0_conv[symmetric]) 5052 apply (erule notE, rule asid_low_high_bits, simp_all)[1] 5053 apply (simp add: asid_high_bits_of_def) 5054 apply (rule conjI) 5055 apply (erule(1) valid_table_caps_pdD [OF _ invs_pd_caps]) 5056 apply (rule conjI) 5057 apply clarsimp 5058 apply (drule caps_of_state_cteD) 5059 apply (clarsimp simp: obj_at_def cte_wp_at_cases a_type_def) 5060 apply (clarsimp split: Structures_A.kernel_object.splits arch_kernel_obj.splits) 5061 apply (clarsimp simp: obj_at_def) 5062 done 5063 5064lemma invs_aligned_pdD: 5065 "\<lbrakk> pspace_aligned s; valid_arch_state s \<rbrakk> \<Longrightarrow> is_aligned (arm_global_pd (arch_state s)) pd_bits" 5066 apply (clarsimp simp: valid_arch_state_def) 5067 apply (drule (1) pd_aligned) 5068 apply (simp add: pd_bits_def pageBits_def) 5069 done 5070 5071end 5072end 5073