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(* 12Lemmas on arch get/set object etc 13*) 14 15theory ArchAcc_AI 16imports "../SubMonad_AI" 17 "Lib.Crunch_Instances_NonDet" 18begin 19 20context Arch begin global_naming ARM 21 22 23bundle unfold_objects = 24 obj_at_def[simp] 25 kernel_object.splits[split] 26 arch_kernel_obj.splits[split] 27 28bundle unfold_objects_asm = 29 obj_at_def[simp] 30 kernel_object.split_asm[split] 31 arch_kernel_obj.split_asm[split] 32 33definition 34 "valid_asid asid s \<equiv> arm_asid_map (arch_state s) asid \<noteq> None" 35 36 37lemma get_asid_pool_wp [wp]: 38 "\<lbrace>\<lambda>s. \<forall>pool. ko_at (ArchObj (ASIDPool pool)) p s \<longrightarrow> Q pool s\<rbrace> 39 get_asid_pool p 40 \<lbrace>Q\<rbrace>" 41 apply (simp add: get_asid_pool_def get_object_def) 42 apply (wp|wpc)+ 43 apply (clarsimp simp: obj_at_def) 44 done 45 46 47lemma set_asid_pool_typ_at [wp]: 48 "\<lbrace>\<lambda>s. P (typ_at T p s)\<rbrace> set_asid_pool ptr pool \<lbrace>\<lambda>_ s. P (typ_at T p s)\<rbrace>" 49 apply (simp add: set_asid_pool_def set_object_def get_object_def) 50 apply wp 51 including unfold_objects 52 by clarsimp (simp add: a_type_def) 53 54 55lemmas set_asid_pool_typ_ats [wp] = abs_typ_at_lifts [OF set_asid_pool_typ_at] 56 57 58lemma get_pd_wp [wp]: 59 "\<lbrace>\<lambda>s. \<forall>pd. ko_at (ArchObj (PageDirectory pd)) p s \<longrightarrow> Q pd s\<rbrace> get_pd p \<lbrace>Q\<rbrace>" 60 apply (simp add: get_pd_def get_object_def) 61 apply (wp|wpc)+ 62 apply (clarsimp simp: obj_at_def) 63 done 64 65 66lemma get_pde_wp: 67 "\<lbrace>\<lambda>s. \<forall>pd. ko_at (ArchObj (PageDirectory pd)) (p && ~~ mask pd_bits) s \<longrightarrow> 68 Q (pd (ucast (p && mask pd_bits >> pde_bits))) s\<rbrace> 69 get_pde p 70 \<lbrace>Q\<rbrace>" 71 by (simp add: get_pde_def vspace_bits_defs) wp 72 73 74lemma get_pde_inv [wp]: "\<lbrace>P\<rbrace> get_pde p \<lbrace>\<lambda>_. P\<rbrace>" 75 by (wp get_pde_wp) simp 76 77bundle pagebits = 78 pd_bits_def[simp] pt_bits_def[simp] pde_bits_def[simp] 79 pageBits_def[simp] mask_lower_twice[simp] 80 word_bool_alg.conj_assoc[symmetric,simp] obj_at_def[simp] 81 pde.splits[split] 82 pte.splits[split] 83 84lemma get_master_pde_wp: 85 "\<lbrace>\<lambda>s. \<forall>pd. ko_at (ArchObj (PageDirectory pd)) (p && ~~ mask pd_bits) s 86 \<longrightarrow> Q (case (pd (ucast (p && ~~ mask 7 && mask pd_bits >> pde_bits))) of 87 SuperSectionPDE x xa xb \<Rightarrow> pd (ucast (p && ~~ mask 7 && mask pd_bits >> pde_bits)) 88 | _ \<Rightarrow> pd (ucast (p && mask pd_bits >> pde_bits))) s\<rbrace> 89 get_master_pde p 90 \<lbrace>Q\<rbrace>" 91 apply (simp add: get_master_pde_def vspace_bits_defs) 92 apply (wp get_pde_wp | wpc)+ 93 including pagebits 94 by auto 95 96lemma store_pde_typ_at [wp]: 97 "\<lbrace>\<lambda>s. P (typ_at T p s)\<rbrace> store_pde ptr pde \<lbrace>\<lambda>_ s. P (typ_at T p s)\<rbrace>" 98 apply (simp add: store_pde_def set_pd_def set_object_def get_object_def) 99 apply wp 100 apply (clarsimp simp: obj_at_def a_type_def) 101 done 102 103 104lemmas store_pde_typ_ats [wp] = abs_typ_at_lifts [OF store_pde_typ_at] 105 106 107lemma get_pt_wp [wp]: 108 "\<lbrace>\<lambda>s. \<forall>pt. ko_at (ArchObj (PageTable pt)) p s \<longrightarrow> Q pt s\<rbrace> get_pt p \<lbrace>Q\<rbrace>" 109 apply (simp add: get_pt_def get_object_def) 110 apply (wp|wpc)+ 111 apply (clarsimp simp: obj_at_def) 112 done 113 114 115lemma get_pte_wp: 116 "\<lbrace>\<lambda>s. \<forall>pt. ko_at (ArchObj (PageTable pt)) (p && ~~mask pt_bits) s \<longrightarrow> 117 Q (pt (ucast (p && mask pt_bits >> pte_bits))) s\<rbrace> 118 get_pte p 119 \<lbrace>Q\<rbrace>" 120 by (simp add: get_pte_def) wp 121 122 123lemma get_pte_inv [wp]: 124 "\<lbrace>P\<rbrace> get_pte p \<lbrace>\<lambda>_. P\<rbrace>" 125 by (wp get_pte_wp) simp 126 127 128lemma get_master_pte_wp: 129 "\<lbrace>\<lambda>s. \<forall>pt. ko_at (ArchObj (PageTable pt)) (p && ~~ mask pt_bits) s \<longrightarrow> 130 Q (case pt (ucast (p && ~~ mask 7 && mask pt_bits >> pte_bits)) of 131 LargePagePTE x xa xb \<Rightarrow> 132 pt (ucast (p && ~~ mask 7 && mask pt_bits >> pte_bits)) 133 | _ \<Rightarrow> pt (ucast (p && mask pt_bits >> pte_bits))) 134 s\<rbrace> 135 get_master_pte p \<lbrace>Q\<rbrace>" 136 apply (simp add: get_master_pte_def) 137 apply (wp get_pte_wp | wpc)+ 138 including pagebits 139 by auto 140 141lemma store_pte_typ_at: 142 "\<lbrace>\<lambda>s. P (typ_at T p s)\<rbrace> store_pte ptr pte \<lbrace>\<lambda>_ s. P (typ_at T p s)\<rbrace>" 143 apply (simp add: store_pte_def set_pt_def set_object_def get_object_def) 144 apply wp 145 apply (clarsimp simp: obj_at_def a_type_def) 146 done 147 148 149lemmas store_pte_typ_ats [wp] = abs_typ_at_lifts [OF store_pte_typ_at] 150 151 152lemma lookup_pt_slot_inv: 153 "\<lbrace>P\<rbrace> lookup_pt_slot pd vptr \<lbrace>\<lambda>_. P\<rbrace>" 154 apply (simp add: lookup_pt_slot_def) 155 apply (wp get_pde_wp|wpc)+ 156 apply clarsimp 157 done 158 159lemma lookup_pt_slot_inv_any: 160 "\<lbrace>\<lambda>s. \<forall>x. Q x s\<rbrace> lookup_pt_slot pd vptr \<lbrace>Q\<rbrace>,-" 161 "\<lbrace>E\<rbrace> lookup_pt_slot pd vptr -, \<lbrace>\<lambda>ft. E\<rbrace>" 162 apply (simp_all add: lookup_pt_slot_def) 163 apply (wp get_pde_wp | simp | wpc)+ 164 done 165 166crunch cte_wp_at[wp]: set_irq_state "\<lambda>s. P (cte_wp_at P' p s)" 167 168lemma set_pt_cte_wp_at: 169 "\<lbrace>\<lambda>s. P (cte_wp_at P' p s)\<rbrace> 170 set_pt ptr val 171 \<lbrace>\<lambda>rv s. P (cte_wp_at P' p s)\<rbrace>" 172 apply (simp add: set_pt_def set_object_def get_object_def) 173 apply wp 174 including unfold_objects_asm 175 by (clarsimp elim!: rsubst[where P=P] 176 simp: cte_wp_at_after_update) 177 178 179lemma set_pd_cte_wp_at: 180 "\<lbrace>\<lambda>s. P (cte_wp_at P' p s)\<rbrace> 181 set_pd ptr val 182 \<lbrace>\<lambda>rv s. P (cte_wp_at P' p s)\<rbrace>" 183 apply (simp add: set_pd_def set_object_def get_object_def) 184 apply wp 185 including unfold_objects_asm 186 by (clarsimp elim!: rsubst[where P=P] 187 simp: cte_wp_at_after_update) 188 189 190lemma set_asid_pool_cte_wp_at: 191 "\<lbrace>\<lambda>s. P (cte_wp_at P' p s)\<rbrace> 192 set_asid_pool ptr val 193 \<lbrace>\<lambda>rv s. P (cte_wp_at P' p s)\<rbrace>" 194 apply (simp add: set_asid_pool_def set_object_def get_object_def) 195 apply wp 196 including unfold_objects_asm 197 by (clarsimp elim!: rsubst[where P=P] 198 simp: cte_wp_at_after_update) 199 200lemma set_pt_pred_tcb_at[wp]: 201 "\<lbrace>pred_tcb_at proj P t\<rbrace> set_pt ptr val \<lbrace>\<lambda>_. pred_tcb_at proj P t\<rbrace>" 202 apply (simp add: set_pt_def set_object_def) 203 including no_pre apply wp 204 apply (rule hoare_strengthen_post [OF get_object_sp]) 205 apply (clarsimp simp: pred_tcb_at_def obj_at_def) 206 done 207 208 209lemma set_pd_pred_tcb_at[wp]: 210 "\<lbrace>pred_tcb_at proj P t\<rbrace> set_pd ptr val \<lbrace>\<lambda>_. pred_tcb_at proj P t\<rbrace>" 211 apply (simp add: set_pd_def set_object_def) 212 including no_pre apply wp 213 apply (rule hoare_strengthen_post [OF get_object_sp]) 214 apply (clarsimp simp: pred_tcb_at_def obj_at_def) 215 done 216 217 218lemma set_asid_pool_pred_tcb_at[wp]: 219 "\<lbrace>pred_tcb_at proj P t\<rbrace> set_asid_pool ptr val \<lbrace>\<lambda>_. pred_tcb_at proj P t\<rbrace>" 220 apply (simp add: set_asid_pool_def set_object_def) 221 including no_pre apply wp 222 apply (rule hoare_strengthen_post [OF get_object_sp]) 223 apply (clarsimp simp: pred_tcb_at_def obj_at_def) 224 done 225 226 227(* FIXME move * 228lemma add_3_eq_Suc'[simp]: "n + 3 = Suc (Suc (Suc n))" by simp 229***) 230 231lemma mask_pd_bits_inner_beauty: (* ARMHYP *) (* 11 = pd_bits - pde_bits *) 232 "is_aligned p pde_bits \<Longrightarrow> 233 (p && ~~ mask pd_bits) + (ucast ((ucast (p && mask pd_bits >> pde_bits))::11 word) << pde_bits) = (p::word32)" 234 by (rule mask_split_aligned; simp add: vspace_bits_defs) 235 236 237lemma more_pd_inner_beauty: 238 fixes x :: "11 word" 239 fixes p :: word32 240 assumes x: "x \<noteq> ucast (p && mask pd_bits >> 3)" 241 shows "(p && ~~ mask pd_bits) + (ucast x << 3) = p \<Longrightarrow> False" 242 by (rule mask_split_aligned_neg[OF _ _ x]; simp add: vspace_bits_defs) 243 244 245lemma mask_pt_bits_inner_beauty: 246 "is_aligned p pte_bits \<Longrightarrow> 247 (p && ~~ mask pt_bits) + (ucast ((ucast (p && mask pt_bits >> pte_bits))::9 word) << pte_bits) = (p::word32)" 248 by (rule mask_split_aligned; simp add: vspace_bits_defs) 249 250 251lemma more_pt_inner_beauty: 252 fixes x :: "9 word" 253 fixes p :: word32 254 assumes x: "x \<noteq> ucast (p && mask pt_bits >> pte_bits)" 255 shows "(p && ~~ mask pt_bits) + (ucast x << pte_bits) = p \<Longrightarrow> False" 256 by (rule mask_split_aligned_neg[OF _ _ x]; simp add: vspace_bits_defs) 257 258 259lemma set_pd_aligned [wp]: 260 "\<lbrace>pspace_aligned\<rbrace> set_pd base pd \<lbrace>\<lambda>_. pspace_aligned\<rbrace>" 261 apply (simp add: set_pd_def) 262 apply (wp set_object_aligned get_object_wp) 263 including unfold_objects_asm 264 by (clarsimp simp: a_type_def) 265 266 267crunch aligned [wp]: store_pde pspace_aligned 268 (wp: hoare_drop_imps) 269 270 271lemmas undefined_validE_R = hoare_FalseE_R[where f=undefined] 272 273 274lemma arch_derive_cap_valid_cap: 275 "\<lbrace>valid_cap (cap.ArchObjectCap arch_cap)\<rbrace> 276 arch_derive_cap arch_cap 277 \<lbrace>valid_cap\<rbrace>, -" 278 apply(simp add: arch_derive_cap_def) 279 apply(cases arch_cap, simp_all add: arch_derive_cap_def o_def) 280 apply(rule hoare_pre, wpc?, wp+, 281 clarsimp simp add: cap_aligned_def valid_cap_def split: option.splits)+ 282 done 283 284 285lemma arch_derive_cap_inv: 286 "\<lbrace>P\<rbrace> arch_derive_cap arch_cap \<lbrace>\<lambda>rv. P\<rbrace>" 287 apply(simp add: arch_derive_cap_def, cases arch_cap, simp_all) 288 apply(rule hoare_pre, wpc?, wp+, simp)+ 289 done 290 291definition 292 "valid_mapping_entries m \<equiv> case m of 293 Inl (InvalidPTE, _) \<Rightarrow> \<top> 294 | Inl (LargePagePTE _ _ _, xs) \<Rightarrow> \<lambda>s. \<forall>p \<in> set xs. pte_at p s 295 | Inl (SmallPagePTE _ _ _, xs) \<Rightarrow> \<lambda>s. \<forall>p \<in> set xs. pte_at p s 296 | Inr (InvalidPDE, _) \<Rightarrow> \<top> 297 | Inr (PageTablePDE _, _) \<Rightarrow> \<bottom> 298 | Inr (SectionPDE _ _ _, xs) \<Rightarrow> \<lambda>s. \<forall>p \<in> set xs. pde_at p s 299 | Inr (SuperSectionPDE _ _ _, xs) \<Rightarrow> \<lambda>s. \<forall>p \<in> set xs. pde_at p s" 300 301definition "invalid_pte_at p \<equiv> obj_at (\<lambda>ko. \<exists>pt. ko = (ArchObj (PageTable pt)) 302 \<and> pt (ucast (p && mask pt_bits) >> pte_bits) = pte.InvalidPTE) (p && ~~ mask pt_bits)" 303 304definition "invalid_pde_at p \<equiv> obj_at (\<lambda>ko. \<exists>pd. ko = (ArchObj (PageDirectory pd)) 305 \<and> pd (ucast (p && mask pd_bits) >> pde_bits) = pde.InvalidPDE) (p && ~~ mask pd_bits)" 306 307definition 308 "valid_slots m \<equiv> case m of 309 Inl (pte, xs) \<Rightarrow> 310 \<lambda>s. xs \<noteq> [] \<and> 311 (\<forall>p \<in> set xs. (\<exists>\<rhd> (p && ~~ mask pt_bits) and pte_at p) s) \<and> 312 wellformed_pte pte \<and> valid_pte pte s 313 | Inr (pde, xs) \<Rightarrow> 314 \<lambda>s. xs \<noteq> [] \<and> 315 (\<forall>p \<in> set xs. (\<exists>\<rhd> (p && ~~ mask pd_bits) and pde_at p) s) \<and> 316 wellformed_pde pde \<and> valid_pde pde s" 317 318crunch inv[wp]: get_master_pte P 319crunch inv[wp]: get_master_pde P 320 321lemma ucast_mask_asid_low_bits [simp]: 322 "ucast ((asid::word32) && mask asid_low_bits) = (ucast asid :: 10 word)" 323 apply (rule word_eqI) 324 apply (simp add: word_size nth_ucast asid_low_bits_def) 325 done 326 327 328lemma ucast_ucast_asid_high_bits [simp]: 329 "ucast (ucast (asid_high_bits_of asid)::word32) = asid_high_bits_of asid" 330 apply (rule word_eqI) 331 apply (simp add: word_size nth_ucast asid_low_bits_def) 332 done 333 334 335lemma mask_asid_low_bits_ucast_ucast: 336 "((asid::word32) && mask asid_low_bits) = ucast (ucast asid :: 10 word)" 337 apply (rule word_eqI) 338 apply (simp add: word_size nth_ucast asid_low_bits_def) 339 done 340 341 342 343lemma set_asid_pool_cur [wp]: 344 "\<lbrace>\<lambda>s. P (cur_thread s)\<rbrace> set_asid_pool p a \<lbrace>\<lambda>_ s. P (cur_thread s)\<rbrace>" 345 unfolding set_asid_pool_def by (wp get_object_wp) simp 346 347 348lemma set_asid_pool_cur_tcb [wp]: 349 "\<lbrace>\<lambda>s. cur_tcb s\<rbrace> set_asid_pool p a \<lbrace>\<lambda>_ s. cur_tcb s\<rbrace>" 350 unfolding cur_tcb_def 351 by (rule hoare_lift_Pf [where f=cur_thread]) wp+ 352 353 354crunch arch [wp]: set_asid_pool "\<lambda>s. P (arch_state s)" 355 (wp: get_object_wp) 356 357 358lemma set_asid_pool_valid_arch [wp]: 359 "\<lbrace>valid_arch_state\<rbrace> set_asid_pool p a \<lbrace>\<lambda>_. valid_arch_state\<rbrace>" 360 apply (rule valid_arch_state_lift; (wp set_asid_pool_typ_at)?) 361 apply (simp add: set_asid_pool_def) 362 apply (wp set_object_wp get_object_wp) 363 apply (clarsimp simp: obj_at_def is_vcpu_def) 364 done 365 366lemma set_asid_pool_valid_objs [wp]: 367 "\<lbrace>valid_objs\<rbrace> set_asid_pool p a \<lbrace>\<lambda>_. valid_objs\<rbrace>" 368 apply (simp add: set_asid_pool_def) 369 apply (wp set_object_valid_objs get_object_wp) 370 including unfold_objects 371 by (clarsimp simp: a_type_def valid_obj_def wellformed_vspace_obj_def) 372 373(* FIXME move *) 374lemma word_shift_by_n: 375 "x * (2^n) = (x::'a::len word) << n" 376 by (simp add: shiftl_t2n) 377 378lemma pde_at_aligned_vptr: (* ARMHYP *) (* 0x3C \<rightarrow> 0x78?, 24 \<rightarrow> 25? *) 379 "\<lbrakk>x \<in> set [0 , 8 .e. 0x78]; page_directory_at pd s; 380 pspace_aligned s; is_aligned vptr 25 \<rbrakk> 381 \<Longrightarrow> pde_at (x + lookup_pd_slot pd vptr) s" 382 apply (clarsimp simp: lookup_pd_slot_def Let_def 383 obj_at_def pde_at_def) 384 apply (drule(1) pspace_alignedD[rotated]) 385 apply (clarsimp simp: a_type_def 386 split: kernel_object.split_asm 387 arch_kernel_obj.split_asm if_split_asm 388 cong: kernel_object.case_cong) 389 apply (prove "is_aligned x 3") 390 subgoal 391 apply (clarsimp simp: upto_enum_step_def word_shift_by_n[of _ 3, simplified]) 392 by (rule is_aligned_shiftl_self) 393 apply (simp add: vspace_bits_defs aligned_add_aligned word_bits_conv 394 is_aligned_shiftl_self)+ 395 apply (prove "pd = (x + (pd + (vptr >> pageBits + pt_bits - pte_bits << pde_bits)) && ~~ mask pd_bits)") 396 subgoal 397 apply (subst mask_lower_twice[symmetric, where n=7]) 398 apply (simp add: pd_bits_def pageBits_def) 399 apply (subst add.commute, subst add_mask_lower_bits) 400 apply (erule aligned_add_aligned) 401 apply (intro is_aligned_shiftl is_aligned_shiftr) 402 apply (simp add: vspace_bits_defs) 403 apply (simp add: vspace_bits_defs word_bits_conv) 404 apply simp 405 apply (subst upper_bits_unset_is_l2p_32[unfolded word_bits_conv]) 406 apply (simp add: pd_bits_def) 407 apply (clarsimp simp: pd_bits_def pde_bits_def upto_enum_step_def word_shift_by_n[of _ 3, simplified]) 408 apply (rule shiftl_less_t2n[where m=7, simplified]) 409 apply (rule minus_one_helper5) 410 apply simp+ 411 apply (rule sym, rule add_mask_lower_bits) 412 apply (simp add: vspace_bits_defs) 413 apply (subst upper_bits_unset_is_l2p) 414 apply (simp add: vspace_bits_defs) 415 apply (rule shiftl_less_t2n) 416 apply (rule shiftr_less_t2n') 417 apply (simp add: vspace_bits_defs)+ 418 done 419by (simp add: vspace_bits_defs) 420 421lemma pde_shifting: (* ARMHYP >> 20? *) 422 "\<lbrakk>is_aligned (vptr::word32) 25; x \<le> 0xF\<rbrakk> 423 \<Longrightarrow> x + (vptr >> pageBits + pt_bits - pte_bits) < 2 ^ (pd_bits - pde_bits)" 424 apply (rule order_less_le_trans) 425 apply (subst upper_bits_unset_is_l2p_32 [where n=11, symmetric]) 426 apply (clarsimp simp: word_bits_def vspace_bits_defs) 427 prefer 2 428 apply (simp add: vspace_bits_defs) 429 apply (clarsimp simp: word_bits_def vspace_bits_defs) 430 subgoal premises prems for n' 431 proof - 432 have H: "(0xF::word32) < 2 ^ 4" by simp 433 from prems show ?thesis 434 apply (subst (asm) word_plus_and_or_coroll) 435 apply (rule word_eqI) 436 subgoal for n 437 apply (clarsimp simp: word_size nth_shiftr is_aligned_nth vspace_bits_defs) 438 apply (spec "n + 21") 439 apply (frule test_bit_size[where n="n + 21"]) 440 apply (simp add: word_size) 441 apply (insert H) 442 apply (drule (1) order_le_less_trans) 443 apply (drule bang_is_le) 444 apply (drule_tac z="2 ^ 4" in order_le_less_trans, assumption) 445 apply (drule word_power_increasing) 446 by simp+ 447 apply (clarsimp simp: word_size nth_shiftl nth_shiftr is_aligned_nth vspace_bits_defs) 448 apply (erule disjE) 449 apply (insert H)[1] 450 apply (drule (1) order_le_less_trans) 451 apply (drule bang_is_le) 452 apply (drule order_le_less_trans[where z="2 ^ 4"], assumption) 453 apply (drule word_power_increasing; simp) 454 apply (spec "n' + 21") 455 apply (frule test_bit_size[where n = "n' + 21"]) 456 by (simp add: word_size) 457 qed 458done 459 460lemma p_le_0xF_helper: 461 "((p::word32) \<le> 0xF) = (\<forall>n'\<ge>4. n'< word_bits \<longrightarrow> \<not> p !! n')" 462 apply (subst upper_bits_unset_is_l2p_32) 463 apply (simp add: word_bits_def) 464 apply (auto intro: plus_one_helper dest: plus_one_helper2) 465 done 466 467lemma pd_shifting: 468 "is_aligned (pd::word32) 14 \<Longrightarrow> 469 pd + (vptr >> (pageBits + pt_bits - pte_bits) << pde_bits) && ~~ mask pd_bits = pd" 470 apply (rule word_eqI[rule_format]) 471 apply (subst word_plus_and_or_coroll) 472 apply (rule word_eqI) 473 subgoal for \<dots> na 474 apply (clarsimp simp: word_size nth_shiftr nth_shiftl is_aligned_nth) 475 apply (spec na) 476 apply (simp add: linorder_not_less) 477 apply (drule test_bit_size)+ 478 by (simp add: word_size vspace_bits_defs) 479 subgoal for n 480 apply (clarsimp simp: word_size nth_shiftr nth_shiftl is_aligned_nth word_ops_nth_size 481 pd_bits_def pageBits_def linorder_not_less pde_bits_def) 482 apply (rule iffI) 483 apply clarsimp 484 apply (drule test_bit_size)+ 485 apply (simp add: word_size vspace_bits_defs) 486 apply clarsimp 487 apply (spec n) 488 by simp 489done 490 491lemma pd_shifting_dual: 492 "is_aligned (pd::word32) 14 \<Longrightarrow> 493 pd + (vptr >> (pageBits + pt_bits - pte_bits) << pde_bits) && mask pd_bits = vptr >> 21 << 3" 494 apply (simp add: pd_bits_def pageBits_def) 495 apply (subst word_plus_and_or_coroll) 496 apply (rule word_eqI) 497 subgoal for n 498 apply (clarsimp simp: word_size nth_shiftr nth_shiftl is_aligned_nth) 499 apply (spec n) 500 apply (simp add: linorder_not_less) 501 apply (drule test_bit_size)+ 502 by (simp add: word_size vspace_bits_defs) 503 apply (rule word_eqI) 504 apply (clarsimp simp: word_size nth_shiftr nth_shiftl is_aligned_nth word_ops_nth_size 505 vspace_bits_defs linorder_not_less) 506 apply (rule iffI) 507 apply clarsimp 508 apply clarsimp 509 apply (drule test_bit_size)+ 510 apply (simp add: word_size) 511 done 512 513 514lemma pd_shifting_at: 515 "\<lbrakk> page_directory_at pd s; pspace_aligned s \<rbrakk> \<Longrightarrow> 516 pd + (vptr >> (pageBits + pt_bits - pte_bits) << pde_bits) && ~~ mask pd_bits = pd" 517 apply (rule pd_shifting) 518 apply (clarsimp simp: pspace_aligned_def obj_at_def) 519 apply (drule bspec, blast) 520 including unfold_objects 521 by (clarsimp simp: a_type_def vspace_bits_defs) 522 523lemma is_aligned_pt: 524 "page_table_at pt s \<Longrightarrow> pspace_aligned s 525 \<Longrightarrow> is_aligned pt pt_bits" 526 apply (clarsimp simp: obj_at_def) 527 apply (drule(1) pspace_alignedD) 528 apply (simp add: pt_bits_def pageBits_def) 529 done 530 531lemma page_table_pte_at_diffE: 532 "\<lbrakk> page_table_at p s; q - p = x << pte_bits; 533 x < 2^(pt_bits - pte_bits); pspace_aligned s \<rbrakk> \<Longrightarrow> pte_at q s" 534 apply (clarsimp simp: diff_eq_eq add.commute) 535 apply (erule(2) page_table_pte_atI) 536 done 537 538lemma pte_at_aligned_vptr: 539 "\<lbrakk>x \<in> set [0 , 8 .e. 0x78]; page_table_at pt s; (* 0x78? *) 540 pspace_aligned s; is_aligned vptr 16 \<rbrakk> 541 \<Longrightarrow> pte_at (x + (pt + (((vptr >> pageBits) && mask (pt_bits - pte_bits)) << pte_bits))) s" 542 apply (erule page_table_pte_at_diffE[where x="(x >> pte_bits) + ((vptr >> 12) && mask (pt_bits - pte_bits))"];simp?) 543 apply (simp add: word_shiftl_add_distrib upto_enum_step_def) 544 apply (clarsimp simp: word_shift_by_n[of _ 3, simplified] shiftr_shiftl1 vspace_bits_defs 545 is_aligned_neg_mask_eq is_aligned_shift) 546 apply (simp only: vspace_bits_defs) 547 apply (subst add.commute, rule is_aligned_add_less_t2n) 548 apply (rule is_aligned_andI1[where n=4], rule is_aligned_shiftr, simp add: pt_bits_def pte_bits_def) 549 apply (rule shiftr_less_t2n) 550 apply (clarsimp dest!: upto_enum_step_subset[THEN subsetD]) 551 apply (erule order_le_less_trans, simp) 552 apply simp 553 apply (rule and_mask_less') 554 apply (simp add: pt_bits_def pageBits_def pte_bits_def) 555 done 556 557lemma lookup_pt_slot_ptes_aligned_valid: (* ARMHYP *) 558 "\<lbrace>valid_vspace_objs and valid_arch_state 559 and equal_kernel_mappings and pspace_aligned 560 and valid_global_objs 561 and \<exists>\<rhd> pd and page_directory_at pd 562 and K (is_aligned vptr 16)\<rbrace> 563 lookup_pt_slot pd vptr 564 \<lbrace>\<lambda>r s. is_aligned r 7 \<and> (\<forall>x\<in>set [0 , 8 .e. 0x78]. pte_at (r + x) s)\<rbrace>, -" 565 apply (simp add: lookup_pt_slot_def) 566 apply (wp get_pde_wp|wpc)+ 567 apply (clarsimp simp: lookup_pd_slot_def Let_def) 568 apply (simp add: pd_shifting_at) 569 apply (frule (2) valid_vspace_objsD) 570 apply clarsimp 571 subgoal for s _ _ x 572 apply (prove "page_table_at (ptrFromPAddr x) s") 573 subgoal 574 by (spec "(ucast (pd + (vptr >> (pageBits + pt_bits - pte_bits) << pde_bits) && mask pd_bits >> pde_bits))";clarsimp) 575 apply (rule conjI) 576 apply (rule is_aligned_add) 577 apply (rule is_aligned_weaken, erule(1) is_aligned_pt) 578 apply (simp add: pt_bits_def pte_bits_def pageBits_def) 579 apply (simp add: pt_bits_def pte_bits_def pageBits_def pde_bits_def pd_bits_def) 580 apply (rule is_aligned_shiftl, simp) 581 apply (rule is_aligned_andI1) 582 apply (rule is_aligned_shiftr, simp) 583 apply clarsimp 584 by (simp add: add.commute; rule_tac pte_at_aligned_vptr; simp) 585 done 586 587lemma p_0x3C_shift: (* FIXME change the name *) 588 "is_aligned (p :: word32) 7 \<Longrightarrow> 589 (\<forall>p\<in>set [p , p + 8 .e. p + 0x78]. f p) = (\<forall>x\<in>set [0, 8 .e. 0x78]. f (p + x))" 590 apply (clarsimp simp: upto_enum_step_def add.commute) 591 apply (frule is_aligned_no_overflow, simp add: word_bits_def) 592 apply (simp add: linorder_not_le [symmetric]) 593 apply (erule notE) 594 apply (simp add: add.commute) 595 apply (erule word_random) 596 apply simp 597 done 598 599lemma lookup_pt_slot_pte [wp]: 600 "\<lbrace>pspace_aligned and valid_vspace_objs and valid_arch_state 601 and equal_kernel_mappings and valid_global_objs 602 and \<exists>\<rhd> pd and page_directory_at pd\<rbrace> 603 lookup_pt_slot pd vptr \<lbrace>pte_at\<rbrace>,-" 604 apply (simp add: lookup_pt_slot_def) 605 apply (wp get_pde_wp|wpc)+ 606 apply (clarsimp simp: lookup_pd_slot_def Let_def) 607 apply (simp add: pd_shifting_at) 608 apply (drule (2) valid_vspace_objsD) 609 apply clarsimp 610 apply (spec "ucast (pd + (vptr >> pageBits + pt_bits - pte_bits << pde_bits) && mask pd_bits >> pde_bits)") 611 apply clarsimp 612 apply (erule page_table_pte_atI, simp_all) 613 apply (simp add: vspace_bits_defs) 614 apply (simp add: mask_2pm1) 615 apply (rule order_le_less_trans, rule word_and_le1, simp) 616 done 617 618lemma shiftr_w2p: 619 "x < len_of TYPE('a) \<Longrightarrow> 620 2 ^ x = (2^(len_of TYPE('a) - 1) >> (len_of TYPE('a) - 1 - x) :: 'a :: len word)" 621 apply simp 622 apply (rule word_eqI) 623 apply (auto simp: word_size nth_shiftr nth_w2p) 624 done 625 626lemma vptr_shiftr_le_2p: 627 "(vptr :: word32) >> 21 < 2 ^ pageBits" 628 apply (rule le_less_trans[rotated]) 629 apply (rule and_mask_less' [where w=max_word]) 630 apply (simp add: pageBits_def) 631 apply (rule word_leI) 632 apply (simp add: word_size nth_shiftr) 633 apply (drule test_bit_size) 634 apply (simp add: pageBits_def word_size) 635 done 636 637lemma vptr_shiftr_le_2p_gen: 638 "(vptr :: word32) >> pageBits + pt_bits - pte_bits < 2 ^ (pd_bits - pde_bits)" 639 apply (rule le_less_trans[rotated]) 640 apply (rule and_mask_less' [where w=max_word]) 641 apply (simp add: vspace_bits_defs) 642 apply (rule word_leI) 643 apply (simp add: word_size nth_shiftr vspace_bits_defs) 644 apply (drule test_bit_size) 645 apply (simp add: pageBits_def word_size) 646 done 647 648lemma page_directory_pde_at_lookupI: 649 "\<lbrakk>page_directory_at pd s; pspace_aligned s\<rbrakk> \<Longrightarrow> pde_at (lookup_pd_slot pd vptr) s" 650 apply (simp add: lookup_pd_slot_def Let_def) 651 apply (erule (1) page_directory_pde_atI[rotated 2]) 652 apply (rule vptr_shiftr_le_2p_gen) 653 done 654 655(* FIXME move to Word_Lemmas? *) 656lemma word_FFF_is_mask: 657 "0xFFF = mask 12" 658 by (simp add: mask_def) 659 660lemma word_1FF_is_mask: 661 "0x1FF = mask 9" 662 by (simp add: mask_def) 663 664 665lemma vptr_shiftr_le_2pt: 666 "((vptr :: word32) >> 12) && 0x1FF < 2 ^ (pt_bits - pte_bits)" 667 apply (clarsimp simp: word_1FF_is_mask vspace_bits_defs) 668 apply (rule and_mask_less_size[where n=9, simplified]) 669 apply (clarsimp simp: word_size) 670 done 671 672lemma vptr_shiftr_le_2pt_gen: 673 "((vptr :: word32) >> pageBits) && mask (pt_bits - pte_bits) < 2 ^ (pt_bits - pte_bits)" 674 apply (clarsimp simp: vspace_bits_defs) 675 apply (rule and_mask_less_size[where n=9, simplified]) 676 apply (clarsimp simp: word_size) 677 done 678 679lemma page_table_pte_at_lookupI: 680 "\<lbrakk>page_table_at pt s; pspace_aligned s\<rbrakk> \<Longrightarrow> pte_at (lookup_pt_slot_no_fail pt vptr) s" 681 apply (simp add: lookup_pt_slot_no_fail_def) 682 apply (erule (1) page_table_pte_atI[rotated 2]) 683 apply (rule vptr_shiftr_le_2pt_gen) 684 done 685 686lemmas lookup_pt_slot_ptes[wp] = 687 lookup_pt_slot_ptes_aligned_valid 688 [@ \<open>post_asm \<open>thin_tac "is_aligned x y" for x y\<close>\<close>] 689 690lemmas lookup_pt_slot_ptes2[wp] = 691 lookup_pt_slot_ptes_aligned_valid 692 [@ \<open>post_asm \<open>drule (1) p_0x3C_shift[THEN iffD2], thin_tac _\<close>\<close>] 693 694lemmas lookup_pt_slot_ptes3[wp] = 695 lookup_pt_slot_ptes_aligned_valid 696 [@ \<open>post_asm \<open>thin_tac _\<close>\<close>] 697 698lemma create_mapping_entries_valid [wp]: 699 "\<lbrace>pspace_aligned and valid_arch_state and valid_vspace_objs (* ARMHYP *) 700 and equal_kernel_mappings and valid_global_objs 701 and \<exists>\<rhd> pd and page_directory_at pd and 702 K ((sz = ARMLargePage \<longrightarrow> is_aligned vptr 16) \<and> 703 (sz = ARMSuperSection \<longrightarrow> is_aligned vptr 25)) \<rbrace> 704 create_mapping_entries base vptr sz vm_rights attrib pd 705 \<lbrace>\<lambda>m. valid_mapping_entries m\<rbrace>, -" 706 apply (cases sz) 707 apply (rule hoare_pre) 708 apply (wpsimp simp: valid_mapping_entries_def largePagePTE_offsets_def vspace_bits_defs 709 superSectionPDE_offsets_def add.commute)+ 710 apply (erule (1) page_directory_pde_at_lookupI) 711 apply (wpsimp simp: valid_mapping_entries_def superSectionPDE_offsets_def vspace_bits_defs 712 lookup_pd_slot_def) 713 apply (prove "is_aligned pd 14") 714 apply (clarsimp simp: obj_at_def add.commute invs_def valid_state_def valid_pspace_def pspace_aligned_def) 715 apply (drule bspec, blast) 716 apply (clarsimp simp: a_type_def vspace_bits_defs split: kernel_object.splits arch_kernel_obj.splits if_split_asm) 717 apply (clarsimp simp: upto_enum_step_def word_shift_by_n[of _ 3, simplified]) 718 apply (clarsimp simp: pde_at_def vspace_bits_defs) 719 apply (simp add: add.commute add.left_commute) 720 apply (subst add_mask_lower_bits) 721 apply (simp add: pd_bits_def pageBits_def) 722 apply (clarsimp simp: pd_bits_def pageBits_def) 723 apply (subst (asm) word_plus_and_or_coroll) 724 prefer 2 725 apply (clarsimp simp: word_size nth_shiftr nth_shiftl is_aligned_nth p_le_0xF_helper word_bits_def) 726 apply (drule test_bit_size)+ 727 apply (simp add: word_size) 728 apply (rule word_eqI) 729 apply (clarsimp simp: word_size nth_shiftr nth_shiftl is_aligned_nth p_le_0xF_helper word_bits_def) 730 apply (frule_tac w=vptr in test_bit_size) 731 apply (simp add: word_size) 732 apply (thin_tac "\<forall>n<14. \<not> pd !! n" for n) 733 subgoal for \<dots> n 734 apply (spec "18+n") 735 by simp 736 apply (clarsimp simp: a_type_simps) 737 apply (rule aligned_add_aligned is_aligned_shiftl_self 738 | simp add: word_bits_conv)+ 739 done 740 741lemma set_pt_distinct [wp]: 742 "\<lbrace>pspace_distinct\<rbrace> set_pt p pt \<lbrace>\<lambda>_. pspace_distinct\<rbrace>" 743 apply (simp add: set_pt_def) 744 apply (wp set_object_distinct get_object_wp) 745 apply (clarsimp simp: obj_at_def a_type_def 746 split: kernel_object.splits arch_kernel_obj.splits) 747 done 748 749 750lemma set_pd_distinct [wp]: 751 "\<lbrace>pspace_distinct\<rbrace> set_pd p pd \<lbrace>\<lambda>_. pspace_distinct\<rbrace>" 752 apply (simp add: set_pd_def) 753 apply (wp set_object_distinct get_object_wp) 754 apply (clarsimp simp: obj_at_def a_type_def 755 split: kernel_object.splits arch_kernel_obj.splits) 756 done 757 758 759lemma store_pte_valid_objs [wp]: 760 "\<lbrace>(%s. wellformed_pte pte) and valid_objs\<rbrace> store_pte p pte \<lbrace>\<lambda>_. valid_objs\<rbrace>" 761 apply (simp add: store_pte_def set_pt_def get_pt_def bind_assoc set_object_def get_object_def) 762 apply (rule hoare_pre) 763 apply (wp|wpc)+ 764 apply (clarsimp simp: valid_objs_def dom_def simp del: fun_upd_apply) 765 subgoal for \<dots> ptr _ 766 apply (rule valid_obj_same_type) 767 apply (cases "ptr = p && ~~ mask pt_bits") 768 apply (erule allE, erule impE, blast) 769 apply (clarsimp simp: valid_obj_def wellformed_vspace_obj_def) 770 apply clarsimp 771 apply fastforce 772 apply (erule allE, erule impE, blast) 773 apply (clarsimp simp: valid_obj_def wellformed_vspace_obj_def) 774 apply assumption 775 by (simp add: a_type_def) 776 done 777 778 779lemma set_pt_caps_of_state [wp]: 780 "\<lbrace>\<lambda>s. P (caps_of_state s)\<rbrace> set_pt p pt \<lbrace>\<lambda>_ s. P (caps_of_state s)\<rbrace>" 781 apply (wpsimp simp: set_pt_def get_object_def bind_assoc set_object_def) 782 apply (subst cte_wp_caps_of_lift) 783 prefer 2 784 apply assumption 785 subgoal for _ y 786 by (cases y, auto simp: cte_wp_at_cases) 787 done 788 789 790lemma set_pd_caps_of_state [wp]: 791 "\<lbrace>\<lambda>s. P (caps_of_state s)\<rbrace> set_pd p pd \<lbrace>\<lambda>_ s. P (caps_of_state s)\<rbrace>" 792 apply (wpsimp simp: set_pd_def get_object_def bind_assoc set_object_def) 793 apply (subst cte_wp_caps_of_lift) 794 prefer 2 795 apply assumption 796 subgoal for _ y 797 by (cases y, auto simp: cte_wp_at_cases) 798 done 799 800 801lemma store_pte_aligned [wp]: 802 "\<lbrace>pspace_aligned\<rbrace> store_pte pt p \<lbrace>\<lambda>_. pspace_aligned\<rbrace>" 803 apply (simp add: store_pte_def set_pt_def) 804 apply (wp set_object_aligned get_object_wp) 805 including unfold_objects 806 by (clarsimp simp: a_type_def) 807 808 809lemma store_pde_valid_objs [wp]: 810 "\<lbrace>(%s. wellformed_pde pde) and valid_objs\<rbrace> store_pde p pde \<lbrace>\<lambda>_. valid_objs\<rbrace>" 811 apply (simp add: store_pde_def set_pd_def get_pd_def bind_assoc set_object_def get_object_def) 812 apply (rule hoare_pre) 813 apply (wp|wpc)+ 814 apply (clarsimp simp: valid_objs_def dom_def simp del: fun_upd_apply) 815 subgoal for \<dots> ptr _ 816 apply (rule valid_obj_same_type) 817 apply (cases "ptr = p && ~~ mask pd_bits") 818 apply (erule allE, erule impE, blast) 819 apply (clarsimp simp: valid_obj_def wellformed_vspace_obj_def) 820 apply clarsimp 821 apply fastforce 822 apply (erule allE, erule impE, blast) 823 apply (clarsimp simp: valid_obj_def wellformed_vspace_obj_def) 824 apply assumption 825 by (simp add: a_type_def) 826 done 827 828 829lemma set_asid_pool_aligned [wp]: 830 "\<lbrace>pspace_aligned\<rbrace> set_asid_pool p ptr \<lbrace>\<lambda>_. pspace_aligned\<rbrace>" 831 apply (simp add: set_asid_pool_def get_object_def) 832 apply (wp set_object_aligned|wpc)+ 833 including unfold_objects 834 apply (clarsimp simp: a_type_def) 835 apply (rule_tac x = "ArchObj (ASIDPool x)" for x in exI) 836 apply auto 837 done 838 839lemma set_asid_pool_distinct [wp]: 840 "\<lbrace>pspace_distinct\<rbrace> set_asid_pool p ptr \<lbrace>\<lambda>_. pspace_distinct\<rbrace>" 841 apply (simp add: set_asid_pool_def get_object_def) 842 apply (wp set_object_distinct|wpc)+ 843 including unfold_objects 844 apply (clarsimp simp: a_type_def) 845 apply (rule_tac x = "ArchObj (ASIDPool x)" for x in exI) 846 apply auto 847 done 848 849 850lemma store_pde_arch [wp]: 851 "\<lbrace>\<lambda>s. P (arch_state s)\<rbrace> store_pde p pde \<lbrace>\<lambda>_ s. P (arch_state s)\<rbrace>" 852 apply (simp add: store_pde_def set_pd_def get_object_def) 853 apply (wp|wpc)+ 854 apply clarsimp 855 done 856 857 858lemma store_pte_valid_pte [wp]: 859 "\<lbrace>valid_pte pt\<rbrace> store_pte p pte \<lbrace>\<lambda>_. valid_pte pt\<rbrace>" 860 by (wp valid_pte_lift store_pte_typ_at) 861 862 863lemma store_pde_valid_pde [wp]: 864 "\<lbrace>valid_pde pde\<rbrace> store_pde slot pde' \<lbrace>\<lambda>rv. valid_pde pde\<rbrace>" 865 by (wp valid_pde_lift store_pde_typ_at) 866 867 868lemma set_pd_typ_at [wp]: 869 "\<lbrace>\<lambda>s. P (typ_at T p s)\<rbrace> set_pd ptr pd \<lbrace>\<lambda>_ s. P (typ_at T p s)\<rbrace>" 870 including unfold_objects 871 apply (wpsimp simp: set_pd_def set_object_def get_object_def) 872 apply (erule rsubst [where P=P]) 873 by (clarsimp simp: a_type_def) 874 875 876lemma set_pd_valid_objs: 877 "\<lbrace>(%s. \<forall>i. wellformed_pde (pd i)) and valid_objs\<rbrace> 878 set_pd p pd 879 \<lbrace>\<lambda>_. valid_objs\<rbrace>" 880 including unfold_objects 881 by (wpsimp simp: set_pd_def valid_obj_def wellformed_vspace_obj_def a_type_def 882 wp: get_object_wp set_object_valid_objs) 883 884 885lemma set_pd_iflive: 886 "\<lbrace>\<lambda>s. if_live_then_nonz_cap s\<rbrace> 887 set_pd p pd 888 \<lbrace>\<lambda>_ s. if_live_then_nonz_cap s\<rbrace>" 889 including unfold_objects 890 by (wpsimp simp: set_pd_def live_def hyp_live_def arch_live_def wp: get_object_wp set_object_iflive) 891 892 893lemma set_pd_zombies: 894 "\<lbrace>\<lambda>s. zombies_final s\<rbrace> 895 set_pd p pd 896 \<lbrace>\<lambda>_ s. zombies_final s\<rbrace>" 897 including unfold_objects 898 by (wpsimp simp: set_pd_def wp: get_object_wp set_object_zombies) 899 900 901lemma set_pd_zombies_state_refs: 902 "\<lbrace>\<lambda>s. P (state_refs_of s)\<rbrace> 903 set_pd p pd 904 \<lbrace>\<lambda>_ s. P (state_refs_of s)\<rbrace>" 905 including unfold_objects 906 apply (wpsimp simp: set_pd_def set_object_def wp: get_object_wp) 907 apply (erule rsubst [where P=P]) 908 apply (rule ext) 909 by (clarsimp simp: state_refs_of_def split: option.splits) 910 911 912lemma set_pd_zombies_state_hyp_refs: 913 "\<lbrace>\<lambda>s. P (state_hyp_refs_of s)\<rbrace> 914 set_pd p pd 915 \<lbrace>\<lambda>_ s. P (state_hyp_refs_of s)\<rbrace>" 916 apply (wpsimp simp: set_pd_def set_object_def wp: get_object_wp) 917 including unfold_objects 918 apply clarsimp 919 apply (erule rsubst [where P=P]) 920 apply (rule ext) 921 by (clarsimp simp: state_hyp_refs_of_def split: option.splits) 922 923 924lemma set_pd_cdt: 925 "\<lbrace>\<lambda>s. P (cdt s)\<rbrace> 926 set_pd p pd 927 \<lbrace>\<lambda>_ s. P (cdt s)\<rbrace>" 928 by (wpsimp simp: set_pd_def wp: get_object_wp) 929 930lemma set_pd_valid_mdb: 931 "\<lbrace>\<lambda>s. valid_mdb s\<rbrace> 932 set_pd p pd 933 \<lbrace>\<lambda>_ s. valid_mdb s\<rbrace>" 934 by (rule valid_mdb_lift; wpsimp simp: set_pd_def set_object_def wp: set_pd_cdt get_object_wp) 935 936lemma set_pd_valid_idle: 937 "\<lbrace>\<lambda>s. valid_idle s\<rbrace> 938 set_pd p pd 939 \<lbrace>\<lambda>_ s. valid_idle s\<rbrace>" 940 by (rule valid_idle_lift; wpsimp simp: set_pd_def wp: get_object_wp) 941 942 943lemma set_pd_ifunsafe: 944 "\<lbrace>\<lambda>s. if_unsafe_then_cap s\<rbrace> 945 set_pd p pd 946 \<lbrace>\<lambda>_ s. if_unsafe_then_cap s\<rbrace>" 947 apply (simp add: set_pd_def) 948 apply (wp get_object_wp set_object_ifunsafe) 949 including unfold_objects 950 by clarsimp 951 952 953lemma set_pd_reply_caps: 954 "\<lbrace>\<lambda>s. valid_reply_caps s\<rbrace> 955 set_pd p pd 956 \<lbrace>\<lambda>_ s. valid_reply_caps s\<rbrace>" 957 by (wp valid_reply_caps_st_cte_lift) 958 959 960lemma set_pd_reply_masters: 961 "\<lbrace>valid_reply_masters\<rbrace> 962 set_pd p pd 963 \<lbrace>\<lambda>_. valid_reply_masters\<rbrace>" 964 by (wp valid_reply_masters_cte_lift) 965 966 967lemma global_refs_kheap [simp]: 968 "global_refs (kheap_update f s) = global_refs s" 969 by (simp add: global_refs_def) 970 971 972crunch global_ref [wp]: set_pd "\<lambda>s. P (global_refs s)" 973 (wp: crunch_wps) 974 975 976crunch arch [wp]: set_pd "\<lambda>s. P (arch_state s)" 977 (wp: crunch_wps) 978 979 980crunch idle [wp]: set_pd "\<lambda>s. P (idle_thread s)" 981 (wp: crunch_wps) 982 983 984crunch irq [wp]: set_pd "\<lambda>s. P (interrupt_irq_node s)" 985 (wp: crunch_wps) 986 987 988lemma set_pd_valid_global: 989 "\<lbrace>\<lambda>s. valid_global_refs s\<rbrace> 990 set_pd p pd 991 \<lbrace>\<lambda>_ s. valid_global_refs s\<rbrace>" 992 by (wp valid_global_refs_cte_lift) 993 994lemma set_pd_no_vcpu[wp]: 995 "\<lbrace>obj_at (is_vcpu and P) p'\<rbrace> set_pd p pd \<lbrace>\<lambda>_. obj_at (is_vcpu and P) p'\<rbrace>" 996 unfolding set_pd_def 997 by (wpsimp wp: set_object_wp get_object_wp simp: obj_at_def is_vcpu_def) 998 999lemma set_pd_valid_arch: 1000 "\<lbrace>\<lambda>s. valid_arch_state s\<rbrace> 1001 set_pd p pd 1002 \<lbrace>\<lambda>_ s. valid_arch_state s\<rbrace>" 1003 by (wp valid_arch_state_lift) 1004 1005 1006lemma set_pd_cur: 1007 "\<lbrace>\<lambda>s. cur_tcb s\<rbrace> 1008 set_pd p pd 1009 \<lbrace>\<lambda>_ s. cur_tcb s\<rbrace>" 1010 apply (simp add: cur_tcb_def set_pd_def set_object_def) 1011 apply (wp get_object_wp) 1012 apply clarsimp 1013 apply (clarsimp split: kernel_object.splits arch_kernel_obj.splits) 1014 apply (clarsimp simp: obj_at_def is_tcb_def) 1015 done 1016 1017 1018crunch interrupt_states[wp]: set_pd "\<lambda>s. P (interrupt_states s)" 1019 (wp: crunch_wps) 1020 1021lemma set_pd_vspace_objs_unmap: 1022 "\<lbrace>valid_vspace_objs and (\<lambda>s. (\<exists>\<rhd>p) s \<longrightarrow> valid_vspace_obj (PageDirectory pd') s) and 1023 obj_at (\<lambda>ko. vs_refs (ArchObj (PageDirectory pd')) \<subseteq> vs_refs ko) p\<rbrace> 1024 set_pd p pd' \<lbrace>\<lambda>_. valid_vspace_objs\<rbrace>" 1025 apply (simp add: set_pd_def) 1026 apply (wp set_object_vspace_objs get_object_wp) 1027 including unfold_objects 1028 by (fastforce simp: a_type_def valid_vspace_obj_def) 1029 1030declare graph_of_None_update[simp] 1031declare graph_of_Some_update[simp] 1032 1033 1034lemma set_pt_typ_at [wp]: 1035 "\<lbrace>\<lambda>s. P (typ_at T p s)\<rbrace> set_pt ptr pt \<lbrace>\<lambda>_ s. P (typ_at T p s)\<rbrace>" 1036 apply (simp add: set_pt_def set_object_def get_object_def) 1037 apply wp 1038 apply clarsimp 1039 apply (erule rsubst [where P=P]) 1040 including unfold_objects 1041 by (clarsimp simp: a_type_def) 1042 1043 1044lemma set_pt_valid_objs: 1045 "\<lbrace>(%s. \<forall>i. wellformed_pte (pt i)) and valid_objs\<rbrace> 1046 set_pt p pt 1047 \<lbrace>\<lambda>_. valid_objs\<rbrace>" 1048 apply (simp add: set_pt_def) 1049 apply (wp get_object_wp set_object_valid_objs) 1050 apply (clarsimp split: kernel_object.splits 1051 arch_kernel_obj.splits) 1052 apply (clarsimp simp: valid_obj_def obj_at_def a_type_def 1053 wellformed_vspace_obj_def) 1054 done 1055 1056 1057lemma set_pt_iflive: 1058 "\<lbrace>\<lambda>s. if_live_then_nonz_cap s\<rbrace> 1059 set_pt p pt 1060 \<lbrace>\<lambda>_ s. if_live_then_nonz_cap s\<rbrace>" 1061 apply (simp add: set_pt_def) 1062 apply (wp get_object_wp set_object_iflive) 1063 apply (clarsimp split: kernel_object.splits arch_kernel_obj.splits) 1064 apply (clarsimp simp: obj_at_def live_def hyp_live_def arch_live_def) 1065 done 1066 1067 1068lemma set_pt_zombies: 1069 "\<lbrace>\<lambda>s. zombies_final s\<rbrace> 1070 set_pt p pt 1071 \<lbrace>\<lambda>_ s. zombies_final s\<rbrace>" 1072 apply (simp add: set_pt_def) 1073 apply (wp get_object_wp set_object_zombies) 1074 apply (clarsimp split: kernel_object.splits arch_kernel_obj.splits) 1075 apply (clarsimp simp: obj_at_def) 1076 done 1077 1078 1079lemma set_pt_zombies_state_refs: 1080 "\<lbrace>\<lambda>s. P (state_refs_of s)\<rbrace> 1081 set_pt p pt 1082 \<lbrace>\<lambda>_ s. P (state_refs_of s)\<rbrace>" 1083 apply (clarsimp simp: set_pt_def set_object_def) 1084 apply (wp get_object_wp) 1085 apply (clarsimp split: kernel_object.splits arch_kernel_obj.splits) 1086 apply (erule rsubst [where P=P]) 1087 apply (rule ext) 1088 apply (clarsimp simp: obj_at_def state_refs_of_def split: option.splits) 1089 done 1090 1091lemma set_pt_zombies_state_hyp_refs: 1092 "\<lbrace>\<lambda>s. P (state_hyp_refs_of s)\<rbrace> 1093 set_pt p pt 1094 \<lbrace>\<lambda>_ s. P (state_hyp_refs_of s)\<rbrace>" 1095 apply (clarsimp simp: set_pt_def set_object_def) 1096 apply (wp get_object_wp) 1097 apply (clarsimp split: kernel_object.splits arch_kernel_obj.splits) 1098 apply (erule rsubst [where P=P]) 1099 apply (rule ext) 1100 apply (clarsimp simp: obj_at_def state_hyp_refs_of_def split: option.splits) 1101 done 1102 1103 1104lemma set_pt_cdt: 1105 "\<lbrace>\<lambda>s. P (cdt s)\<rbrace> 1106 set_pt p pt 1107 \<lbrace>\<lambda>_ s. P (cdt s)\<rbrace>" 1108 apply (clarsimp simp: set_pt_def) 1109 apply (wp get_object_wp) 1110 apply simp 1111 done 1112 1113 1114lemma set_pt_valid_mdb: 1115 "\<lbrace>\<lambda>s. valid_mdb s\<rbrace> 1116 set_pt p pt 1117 \<lbrace>\<lambda>_ s. valid_mdb s\<rbrace>" 1118 by (rule valid_mdb_lift; wpsimp simp: set_pt_def set_object_def wp: set_pt_cdt get_object_wp) 1119 1120 1121lemma set_pt_valid_idle: 1122 "\<lbrace>\<lambda>s. valid_idle s\<rbrace> 1123 set_pt p pt 1124 \<lbrace>\<lambda>_ s. valid_idle s\<rbrace>" 1125 apply (rule valid_idle_lift, wp+) 1126 apply (simp add: set_pt_def) 1127 apply (wp get_object_wp) 1128 apply simp 1129 done 1130 1131 1132lemma set_pt_ifunsafe: 1133 "\<lbrace>\<lambda>s. if_unsafe_then_cap s\<rbrace> 1134 set_pt p pt 1135 \<lbrace>\<lambda>_ s. if_unsafe_then_cap s\<rbrace>" 1136 apply (simp add: set_pt_def) 1137 apply (wp get_object_wp set_object_ifunsafe) 1138 apply (clarsimp split: kernel_object.splits arch_kernel_obj.splits) 1139 apply (clarsimp simp: obj_at_def) 1140 done 1141 1142 1143lemma set_pt_reply_caps: 1144 "\<lbrace>\<lambda>s. valid_reply_caps s\<rbrace> 1145 set_pt p pt 1146 \<lbrace>\<lambda>_ s. valid_reply_caps s\<rbrace>" 1147 by (wp valid_reply_caps_st_cte_lift) 1148 1149 1150lemma set_pt_reply_masters: 1151 "\<lbrace>valid_reply_masters\<rbrace> 1152 set_pt p pt 1153 \<lbrace>\<lambda>_. valid_reply_masters\<rbrace>" 1154 by (wp valid_reply_masters_cte_lift) 1155 1156 1157crunch global_ref [wp]: set_pt "\<lambda>s. P (global_refs s)" 1158 (wp: crunch_wps) 1159 1160 1161crunch arch [wp]: set_pt "\<lambda>s. P (arch_state s)" 1162 (wp: crunch_wps) 1163 1164 1165crunch idle [wp]: set_pt "\<lambda>s. P (idle_thread s)" 1166 (wp: crunch_wps) 1167 1168 1169crunch irq [wp]: set_pt "\<lambda>s. P (interrupt_irq_node s)" 1170 (wp: crunch_wps) 1171 1172 1173lemma set_pt_valid_global: 1174 "\<lbrace>\<lambda>s. valid_global_refs s\<rbrace> 1175 set_pt p pt 1176 \<lbrace>\<lambda>_ s. valid_global_refs s\<rbrace>" 1177 by (wp valid_global_refs_cte_lift) 1178 1179lemma set_pt_no_vcpu[wp]: 1180 "\<lbrace>obj_at (is_vcpu and P) p'\<rbrace> set_pt p pt \<lbrace>\<lambda>_. obj_at (is_vcpu and P) p'\<rbrace>" 1181 unfolding set_pt_def 1182 by (wpsimp wp: set_object_wp get_object_wp simp: obj_at_def is_vcpu_def) 1183 1184lemma set_pt_valid_arch_state[wp]: 1185 "\<lbrace>\<lambda>s. valid_arch_state s\<rbrace> 1186 set_pt p pt 1187 \<lbrace>\<lambda>_ s. valid_arch_state s\<rbrace>" 1188 by (wp valid_arch_state_lift) 1189 1190 1191lemma set_pt_cur: 1192 "\<lbrace>\<lambda>s. cur_tcb s\<rbrace> 1193 set_pt p pt 1194 \<lbrace>\<lambda>_ s. cur_tcb s\<rbrace>" 1195 apply (simp add: cur_tcb_def set_pt_def set_object_def) 1196 apply (wp get_object_wp) 1197 apply clarsimp 1198 apply (clarsimp split: kernel_object.splits arch_kernel_obj.splits) 1199 apply (clarsimp simp: obj_at_def is_tcb_def) 1200 done 1201 1202 1203lemma set_pt_aligned [wp]: 1204 "\<lbrace>pspace_aligned\<rbrace> set_pt p pt \<lbrace>\<lambda>_. pspace_aligned\<rbrace>" 1205 apply (simp add: set_pt_def) 1206 apply (wp get_object_wp set_object_aligned) 1207 apply (clarsimp simp: a_type_def obj_at_def 1208 split: kernel_object.splits arch_kernel_obj.splits) 1209 done 1210 1211 1212crunch interrupt_states[wp]: set_pt "\<lambda>s. P (interrupt_states s)" 1213 (wp: crunch_wps) 1214 1215lemma set_pt_vspace_objs [wp]: 1216 "\<lbrace>valid_vspace_objs and (\<lambda>s. (\<exists>\<rhd>p) s \<longrightarrow> valid_vspace_obj (PageTable pt) s)\<rbrace> 1217 set_pt p pt 1218 \<lbrace>\<lambda>_. valid_vspace_objs\<rbrace>" 1219 apply (simp add: set_pt_def) 1220 apply (wp set_object_vspace_objs get_object_wp) 1221 apply (clarsimp simp: obj_at_def) 1222 apply (rule conjI) 1223 apply (clarsimp simp: a_type_def 1224 split: kernel_object.splits arch_kernel_obj.splits) 1225 apply (clarsimp split: kernel_object.splits arch_kernel_obj.splits) 1226 apply (simp add: vs_refs_def) 1227 done 1228 1229 1230lemma set_pt_vs_lookup [wp]: 1231 "\<lbrace>\<lambda>s. P (vs_lookup s)\<rbrace> set_pt p pt \<lbrace>\<lambda>x s. P (vs_lookup s)\<rbrace>" 1232 unfolding set_pt_def set_object_def 1233 apply (wp get_object_wp) 1234 apply clarsimp 1235 apply (erule rsubst [where P=P]) 1236 apply (clarsimp split: kernel_object.splits arch_kernel_obj.splits) 1237 apply (rule order_antisym) 1238 apply (rule vs_lookup_sub) 1239 apply (clarsimp simp: obj_at_def vs_refs_def) 1240 apply simp 1241 apply (rule vs_lookup_sub) 1242 apply (clarsimp simp: obj_at_def vs_refs_def split: if_split_asm) 1243 apply simp 1244 done 1245 1246 1247lemma store_pte_vs_lookup [wp]: 1248 "\<lbrace>\<lambda>s. P (vs_lookup s)\<rbrace> store_pte x pte \<lbrace>\<lambda>_ s. P (vs_lookup s)\<rbrace>" 1249 unfolding store_pte_def by wp simp 1250 1251 1252lemma unique_table_caps_ptD: 1253 "\<lbrakk> cs p = Some cap; cap_asid cap = None; 1254 cs p' = Some cap'; is_pt_cap cap; is_pt_cap cap'; 1255 obj_refs cap' = obj_refs cap; 1256 unique_table_caps cs\<rbrakk> 1257 \<Longrightarrow> p = p'" 1258 by (fastforce simp add: unique_table_caps_def) 1259 1260 1261lemma unique_table_caps_pdD: 1262 "\<lbrakk> cs p = Some cap; cap_asid cap = None; 1263 cs p' = Some cap'; is_pd_cap cap; is_pd_cap cap'; 1264 obj_refs cap' = obj_refs cap; 1265 unique_table_caps cs\<rbrakk> 1266 \<Longrightarrow> p = p'" 1267 by (fastforce simp add: unique_table_caps_def) 1268 1269 1270lemma valid_objs_caps: 1271 "valid_objs s \<Longrightarrow> valid_caps (caps_of_state s) s" 1272 apply (clarsimp simp: valid_caps_def) 1273 apply (erule (1) caps_of_state_valid_cap) 1274 done 1275 1276 1277lemma simpler_set_pt_def: 1278 "set_pt p pt = 1279 (\<lambda>s. if \<exists>pt. kheap s p = Some (ArchObj (PageTable pt)) then 1280 ({((), s\<lparr>kheap := kheap s(p \<mapsto> ArchObj (PageTable pt))\<rparr>)}, False) 1281 else ({}, True))" 1282 by (rule ext) (auto simp: set_pt_def set_object_def get_object_def assert_def 1283 put_def get_def simpler_gets_def bind_def 1284 return_def fail_def 1285 split: kernel_object.splits 1286 arch_kernel_obj.splits) 1287 1288 1289lemma valid_set_ptI: 1290 "(!!s opt. \<lbrakk>P s; kheap s p = Some (ArchObj (PageTable opt))\<rbrakk> 1291 \<Longrightarrow> Q () (s\<lparr>kheap := kheap s(p \<mapsto> ArchObj (PageTable pt))\<rparr>)) 1292 \<Longrightarrow> \<lbrace>P\<rbrace> set_pt p pt \<lbrace>Q\<rbrace>" 1293 by (rule validI) (clarsimp simp: simpler_set_pt_def split: if_split_asm) 1294 1295lemma set_pt_table_caps [wp]: 1296 "\<lbrace>valid_table_caps and (\<lambda>s. valid_caps (caps_of_state s) s) and 1297 (\<lambda>s. ((\<exists>slot. caps_of_state s slot = 1298 Some (ArchObjectCap (PageTableCap p None))) \<longrightarrow> 1299 pt = (\<lambda>x. InvalidPTE)) \<or> 1300 (\<forall>slot. \<exists>asid. caps_of_state s slot = 1301 Some (ArchObjectCap (PageTableCap p (Some asid)))))\<rbrace> 1302 set_pt p pt 1303 \<lbrace>\<lambda>rv. valid_table_caps\<rbrace>" 1304 unfolding valid_table_caps_def 1305 apply (rule valid_set_ptI) 1306 apply (intro allI impI, simp add: obj_at_def del: HOL.imp_disjL) 1307 apply (cut_tac s=s and val= "ArchObj (PageTable pt)" and p=p 1308 in caps_of_state_after_update[folded fun_upd_def]) 1309 apply (simp add: obj_at_def) 1310 apply (clarsimp simp del: HOL.imp_disjL) 1311 apply (thin_tac "ALL x. P x" for P) 1312 apply (case_tac cap, simp_all add: is_pd_cap_def is_pt_cap_def) 1313 apply (erule disjE) 1314 apply (simp add: valid_caps_def) 1315 apply ((drule spec)+, erule impE, assumption) 1316 apply (rename_tac arch_cap) 1317 apply (case_tac arch_cap, 1318 simp_all add: valid_cap_def obj_at_def aa_type_simps) 1319 apply clarsimp 1320 apply (erule impE, fastforce simp: cap_asid_def split: option.splits) 1321 apply (erule disjE, simp add: empty_table_def) 1322 apply (drule_tac x=a in spec, drule_tac x=b in spec) 1323 apply (clarsimp simp add: cap_asid_def split: option.splits) 1324 done 1325 1326 1327lemma set_object_caps_of_state: 1328 "\<lbrace>(\<lambda>s. \<not>(tcb_at p s) \<and> \<not>(\<exists>n. cap_table_at n p s)) and 1329 K ((\<forall>x y. obj \<noteq> CNode x y) \<and> (\<forall>x. obj \<noteq> TCB x)) and 1330 (\<lambda>s. P (caps_of_state s))\<rbrace> 1331 set_object p obj 1332 \<lbrace>\<lambda>_ s. P (caps_of_state s)\<rbrace>" 1333 apply (clarsimp simp: set_object_def) 1334 apply wp 1335 apply clarify 1336 apply (erule rsubst[where P=P]) 1337 apply (rule ext) 1338 apply (simp add: caps_of_state_cte_wp_at obj_at_def is_cap_table_def 1339 is_tcb_def) 1340 apply (auto simp: cte_wp_at_cases) 1341 done 1342 1343 1344(* FIXME: Move to Invariants_A *) 1345lemma pte_ref_pagesD: 1346 "pte_ref_pages (pt y) = Some x \<Longrightarrow> 1347 (VSRef (ucast y) (Some APageTable), x) 1348 \<in> vs_refs_pages (ArchObj (PageTable pt))" 1349 by (auto simp: pte_ref_pages_def vs_refs_pages_def graph_of_def) 1350 1351lemma set_pt_valid_vspace_objs[wp]: 1352 "valid (\<lambda>s. valid_vspace_objs s \<and> ((\<exists>\<rhd> p) s \<longrightarrow> (\<forall>x. valid_pte (pt x) s))) 1353 (set_pt p pt) (\<lambda>_. valid_vspace_objs)" 1354 apply (rule valid_set_ptI) 1355 apply (clarsimp simp: valid_vspace_objs_def) 1356 subgoal for s opt pa rs ao 1357 apply (spec pa) 1358 apply (prove "(\<exists>\<rhd> pa) s") 1359 apply (rule exI[where x=rs]) 1360 apply (erule vs_lookupE) 1361 apply clarsimp 1362 apply (erule vs_lookupI) 1363 apply (erule rtrancl.induct, simp) 1364 subgoal for \<dots> b c 1365 apply (prove "(b \<rhd>1 c) s") 1366 apply (thin_tac "_ : rtrancl _")+ 1367 apply (clarsimp simp add: vs_lookup1_def obj_at_def vs_refs_def 1368 split: if_split_asm) 1369 by simp 1370 apply simp 1371 apply (spec ao) 1372 apply (cases "pa = p") 1373 apply (clarsimp simp: obj_at_def) 1374 subgoal for _ x 1375 apply (drule_tac x=x in spec) 1376 by (cases "pt x"; clarsimp simp: obj_at_def data_at_def a_type_simps) 1377 apply (cases ao; simp add: obj_at_def a_type_simps) 1378 apply clarsimp 1379 apply (drule bspec, assumption, clarsimp) 1380 apply clarsimp 1381 subgoal for "fun" _ x 1382 apply (spec x) 1383 by (cases "fun x"; clarsimp simp: obj_at_def data_at_def a_type_simps) 1384 apply clarsimp 1385 subgoal for "fun" _ x 1386 apply (spec x) 1387 by (cases "fun x"; clarsimp simp: obj_at_def data_at_def a_type_simps) 1388 done 1389done 1390 1391lemma set_pt_valid_vs_lookup [wp]: (* ARMHYP *) 1392 "\<lbrace>\<lambda>s. valid_vs_lookup s \<and> valid_arch_state s \<and> 1393 valid_vspace_objs s \<and> ((\<exists>\<rhd> p) s \<longrightarrow> (\<forall>x. valid_pte (pt x) s)) \<and> 1394 (\<forall>ref. (ref \<unrhd> p) s \<longrightarrow> 1395 (\<forall>x p. pte_ref_pages (pt x) = Some p \<longrightarrow> 1396 (\<exists>p' cap. caps_of_state s p' = Some cap \<and> 1397 p \<in> obj_refs cap \<and> 1398 vs_cap_ref cap = 1399 Some (VSRef (ucast x) (Some APageTable) # ref))))\<rbrace> 1400 set_pt p pt 1401 \<lbrace>\<lambda>rv. valid_vs_lookup\<rbrace>" 1402 using set_pt_valid_vspace_objs[of p pt] set_pt_valid_arch_state[of p pt] 1403 apply (clarsimp simp: valid_def simpler_set_pt_def) 1404 apply (drule_tac x=s in spec)+ 1405 apply (clarsimp simp: valid_vs_lookup_def split: if_split_asm) 1406 apply (erule (1) vs_lookup_pagesE_alt) 1407 apply (clarsimp simp: valid_arch_state_def valid_asid_table_def 1408 fun_upd_def) 1409 apply (drule_tac x=pa in spec) 1410 apply (drule_tac x="[VSRef (ucast a) None]" in spec)+ 1411 apply simp 1412 apply (drule vs_lookup_pages_atI) 1413 apply simp 1414 apply (subst caps_of_state_after_update, simp add: obj_at_def) 1415 apply simp 1416 apply (drule_tac x=pa in spec) 1417 apply (drule_tac x="[VSRef (ucast b) (Some AASIDPool), 1418 VSRef (ucast a) None]" in spec)+ 1419 apply simp 1420 apply (drule vs_lookup_pages_apI) 1421 apply (simp split: if_split_asm) 1422 apply simp+ 1423 apply (subst caps_of_state_after_update, simp add: obj_at_def) 1424 apply simp 1425 apply (drule_tac x=pa in spec) 1426 apply (drule_tac x="[VSRef (ucast c) (Some APageDirectory), 1427 VSRef (ucast b) (Some AASIDPool), 1428 VSRef (ucast a) None]" in spec)+ 1429 apply simp 1430 apply (drule vs_lookup_pages_pdI) 1431 apply (simp split: if_split_asm)+ 1432 apply (subst caps_of_state_after_update, simp add: obj_at_def) 1433 apply fastforce 1434 apply (clarsimp simp: fun_upd_def split: if_split_asm) 1435 apply (thin_tac "valid_vspace_objs s" for s, thin_tac "valid_arch_state s" for s) 1436 apply (subst caps_of_state_after_update, simp add: obj_at_def) 1437 apply (thin_tac "\<forall>p ref. P p ref" for P) 1438 apply (drule_tac x="[VSRef (ucast c) (Some APageDirectory), 1439 VSRef (ucast b) (Some AASIDPool), 1440 VSRef (ucast a) None]" in spec) 1441 apply (thin_tac "valid_pte pte s" for pte s) 1442 apply (erule impE, fastforce intro: vs_lookup_pdI) 1443 apply (drule_tac x=d in spec) 1444 apply (erule impE) 1445 apply (erule (4) vs_lookup_pdI[THEN vs_lookup_pages_vs_lookupI]) 1446 apply (drule spec, drule spec, erule impE, assumption) 1447 apply assumption 1448 apply (thin_tac "valid_vspace_objs s" for s, thin_tac "valid_arch_state s" for s) 1449 apply (subst caps_of_state_after_update, simp add: obj_at_def) 1450 apply (thin_tac "\<forall>ref. (ref \<unrhd> p) s \<longrightarrow> P ref" for P) 1451 apply (drule_tac x=pa in spec) 1452 apply (drule_tac x="[VSRef (ucast d) (Some APageTable), 1453 VSRef (ucast c) (Some APageDirectory), 1454 VSRef (ucast b) (Some AASIDPool), 1455 VSRef (ucast a) None]" in spec) 1456 apply (thin_tac "(\<exists>\<rhd> p) s \<longrightarrow> P" for P) 1457 apply (erule impE, fastforce intro: vs_lookup_pages_ptI) 1458 apply simp 1459 done 1460 1461lemma set_pt_arch_caps [wp]: (* ARMHYP *) 1462 "\<lbrace>valid_arch_caps and valid_arch_state and valid_vspace_objs and 1463 (\<lambda>s. valid_caps (caps_of_state s) s) and 1464 (\<lambda>s. ((\<exists>slot. caps_of_state s slot = 1465 Some (ArchObjectCap (PageTableCap p None))) \<longrightarrow> 1466 pt = (\<lambda>x. InvalidPTE)) \<or> 1467 (\<forall>slot. \<exists>asid. caps_of_state s slot = 1468 Some (ArchObjectCap (PageTableCap p (Some asid))))) and 1469 (\<lambda>s. ((\<exists>\<rhd> p) s \<longrightarrow> (\<forall>x. valid_pte (pt x) s)) \<and> 1470 (\<forall>ref. (ref \<unrhd> p) s \<longrightarrow> 1471 (\<forall>x p. pte_ref_pages (pt x) = Some p \<longrightarrow> 1472 (\<exists>p' cap. caps_of_state s p' = Some cap \<and> 1473 p \<in> obj_refs cap \<and> 1474 vs_cap_ref cap = 1475 Some (VSRef (ucast x) (Some APageTable) # ref)))))\<rbrace> 1476 set_pt p pt \<lbrace>\<lambda>_. valid_arch_caps\<rbrace>" 1477 unfolding valid_arch_caps_def 1478 apply (rule hoare_pre) 1479 apply (wp set_pt_valid_vs_lookup) 1480 apply clarsimp 1481 done 1482 1483 1484lemma valid_global_refsD2: 1485 "\<lbrakk> caps_of_state s ptr = Some cap; valid_global_refs s \<rbrakk> 1486 \<Longrightarrow> global_refs s \<inter> cap_range cap = {}" 1487 by (cases ptr, 1488 simp add: valid_global_refs_def valid_refs_def 1489 cte_wp_at_caps_of_state) 1490 1491 1492lemma valid_global_refsD: 1493 "\<lbrakk> valid_global_refs s; cte_wp_at ((=) cap) ptr s; 1494 r \<in> global_refs s \<rbrakk> 1495 \<Longrightarrow> r \<notin> cap_range cap" 1496 apply (clarsimp simp: cte_wp_at_caps_of_state) 1497 apply (drule(1) valid_global_refsD2) 1498 apply fastforce 1499 done 1500 1501lemma set_pt_global_objs: 1502 "\<lbrace>valid_global_objs and valid_arch_state and 1503 (\<lambda>s. p \<in> set (arm_global_pts (arch_state s)) \<longrightarrow> 1504 (\<forall>x. aligned_pte (pt x)))\<rbrace> 1505 set_pt p pt 1506 \<lbrace>\<lambda>rv. valid_global_objs\<rbrace>" 1507 apply (rule valid_set_ptI) 1508 apply (clarsimp simp: valid_global_objs_def valid_arch_state_def valid_vspace_obj_def 1509 valid_vso_at_def obj_at_def empty_table_def) 1510 done 1511 1512crunch v_ker_map[wp]: set_pt "valid_kernel_mappings" 1513 (ignore: set_object wp: set_object_v_ker_map crunch_wps) 1514 1515 1516lemma set_pt_asid_map [wp]: 1517 "\<lbrace>valid_asid_map\<rbrace> set_pt p pt \<lbrace>\<lambda>_. valid_asid_map\<rbrace>" 1518 apply (simp add: valid_asid_map_def vspace_at_asid_def) 1519 apply (rule hoare_lift_Pf2 [where f="arch_state"]) 1520 apply wp+ 1521 done 1522 1523 1524lemma set_pt_only_idle [wp]: 1525 "\<lbrace>only_idle\<rbrace> set_pt p pt \<lbrace>\<lambda>_. only_idle\<rbrace>" 1526 by (wp only_idle_lift) 1527 1528 1529lemma set_pt_equal_mappings [wp]: 1530 "\<lbrace>equal_kernel_mappings\<rbrace> set_pt p pt \<lbrace>\<lambda>rv. equal_kernel_mappings\<rbrace>" 1531 by (simp add: set_pt_def | wp set_object_equal_mappings get_object_wp)+ 1532 1533 1534lemma set_pt_kernel_window[wp]: 1535 "\<lbrace>pspace_in_kernel_window\<rbrace> set_pt p pt \<lbrace>\<lambda>rv. pspace_in_kernel_window\<rbrace>" 1536 apply (simp add: set_pt_def) 1537 apply (wp set_object_pspace_in_kernel_window get_object_wp) 1538 apply (clarsimp simp: obj_at_def a_type_def 1539 split: kernel_object.split_asm 1540 arch_kernel_obj.split_asm) 1541 done 1542 1543lemma set_pt_respects_device_region[wp]: 1544 "\<lbrace>pspace_respects_device_region\<rbrace> set_pt p pt \<lbrace>\<lambda>rv. pspace_respects_device_region\<rbrace>" 1545 apply (simp add: set_pt_def) 1546 apply (wp set_object_pspace_respects_device_region get_object_wp) 1547 apply (clarsimp simp: obj_at_def a_type_def 1548 split: Structures_A.kernel_object.split_asm 1549 arch_kernel_obj.split_asm) 1550 done 1551 1552 1553lemma set_pt_valid_global_vspace_mappings: 1554 "\<lbrace>\<lambda>s. valid_global_vspace_mappings s\<rbrace> 1555 set_pt p pt 1556 \<lbrace>\<lambda>rv. valid_global_vspace_mappings\<rbrace>" 1557 by (wpsimp simp: valid_global_vspace_mappings_def valid_global_objs_def) 1558 1559lemma set_pt_valid_global_objs: 1560 "\<lbrace>\<lambda>s. valid_global_objs s\<rbrace> 1561 set_pt p pt 1562 \<lbrace>\<lambda>rv. valid_global_objs\<rbrace>" 1563 by (wpsimp simp: valid_global_objs_def) 1564 1565lemma set_pt_caps_in_kernel_window[wp]: 1566 "\<lbrace>cap_refs_in_kernel_window\<rbrace> set_pt p pt \<lbrace>\<lambda>rv. cap_refs_in_kernel_window\<rbrace>" 1567 apply (simp add: set_pt_def) 1568 apply (wp set_object_cap_refs_in_kernel_window get_object_wp) 1569 apply (clarsimp simp: obj_at_def a_type_def 1570 split: kernel_object.split_asm 1571 arch_kernel_obj.split_asm) 1572 done 1573 1574lemma set_pt_caps_respects_device_region[wp]: 1575 "\<lbrace>cap_refs_respects_device_region\<rbrace> set_pt p pt \<lbrace>\<lambda>rv. cap_refs_respects_device_region\<rbrace>" 1576 apply (simp add: set_pt_def) 1577 apply (wp set_object_cap_refs_respects_device_region get_object_wp) 1578 apply (clarsimp simp: obj_at_def a_type_def 1579 split: Structures_A.kernel_object.split_asm 1580 arch_kernel_obj.split_asm) 1581 done 1582 1583lemma set_pt_valid_ioc[wp]: 1584 "\<lbrace>valid_ioc\<rbrace> set_pt p pt \<lbrace>\<lambda>_. valid_ioc\<rbrace>" 1585 apply (simp add: set_pt_def) 1586 apply (wp set_object_valid_ioc_no_caps get_object_wp) 1587 by (clarsimp simp: a_type_simps obj_at_def is_tcb is_cap_table 1588 split: kernel_object.splits arch_kernel_obj.splits) 1589 1590 1591lemma valid_machine_stateE: 1592 assumes vm: "valid_machine_state s" 1593 assumes e: "\<lbrakk>in_user_frame p s 1594 \<or> underlying_memory (machine_state s) p = 0 \<rbrakk> \<Longrightarrow> E " 1595 shows E 1596 using vm 1597 apply (clarsimp simp: valid_machine_state_def) 1598 apply (drule_tac x = p in spec) 1599 apply (rule e) 1600 apply auto 1601 done 1602 1603lemma in_user_frame_same_type_upd: 1604 "\<lbrakk>typ_at type p s; type = a_type obj; in_user_frame q s\<rbrakk> 1605 \<Longrightarrow> in_user_frame q (s\<lparr>kheap := kheap s(p \<mapsto> obj)\<rparr>)" 1606 apply (clarsimp simp: in_user_frame_def obj_at_def) 1607 apply (rule_tac x=sz in exI) 1608 apply (auto simp: a_type_simps) 1609 done 1610 1611lemma in_device_frame_same_type_upd: 1612 "\<lbrakk>typ_at type p s; type = a_type obj ; in_device_frame q s\<rbrakk> 1613 \<Longrightarrow> in_device_frame q (s\<lparr>kheap := kheap s(p \<mapsto> obj)\<rparr>)" 1614 apply (clarsimp simp: in_device_frame_def obj_at_def) 1615 apply (rule_tac x=sz in exI) 1616 apply (auto simp: a_type_simps) 1617 done 1618 1619lemma store_word_offs_in_user_frame[wp]: 1620 "\<lbrace>\<lambda>s. in_user_frame p s\<rbrace> store_word_offs a x w \<lbrace>\<lambda>_ s. in_user_frame p s\<rbrace>" 1621 unfolding in_user_frame_def 1622 by (wp hoare_vcg_ex_lift) 1623 1624lemma store_word_offs_in_device_frame[wp]: 1625 "\<lbrace>\<lambda>s. in_device_frame p s\<rbrace> store_word_offs a x w \<lbrace>\<lambda>_ s. in_device_frame p s\<rbrace>" 1626 unfolding in_device_frame_def 1627 by (wp hoare_vcg_ex_lift) 1628 1629 1630lemma as_user_in_user_frame[wp]: 1631 "\<lbrace>\<lambda>s. in_user_frame p s\<rbrace> as_user t m \<lbrace>\<lambda>_ s. in_user_frame p s\<rbrace>" 1632 unfolding in_user_frame_def 1633 by (wp hoare_vcg_ex_lift) 1634 1635lemma as_user_in_device_frame[wp]: 1636 "\<lbrace>\<lambda>s. in_device_frame p s\<rbrace> as_user t m \<lbrace>\<lambda>_ s. in_device_frame p s\<rbrace>" 1637 unfolding in_device_frame_def 1638 by (wp hoare_vcg_ex_lift) 1639 1640crunch obj_at[wp]: load_word_offs "\<lambda>s. P (obj_at Q p s)" 1641 1642lemma load_word_offs_in_user_frame[wp]: 1643 "\<lbrace>\<lambda>s. in_user_frame p s\<rbrace> load_word_offs a x \<lbrace>\<lambda>_ s. in_user_frame p s\<rbrace>" 1644 unfolding in_user_frame_def 1645 by (wp hoare_vcg_ex_lift) 1646 1647lemma valid_machine_state_heap_updI: 1648assumes vm : "valid_machine_state s" 1649assumes tyat : "typ_at type p s" 1650shows 1651 " a_type obj = type \<Longrightarrow> valid_machine_state (s\<lparr>kheap := kheap s(p \<mapsto> obj)\<rparr>)" 1652 apply (clarsimp simp: valid_machine_state_def) 1653 subgoal for p 1654 apply (rule valid_machine_stateE[OF vm,where p = p]) 1655 apply (elim disjE,simp_all) 1656 apply (drule(1) in_user_frame_same_type_upd[OF tyat]) 1657 apply simp+ 1658 done 1659 done 1660 1661lemma set_pt_vms[wp]: 1662 "\<lbrace>valid_machine_state\<rbrace> set_pt p pt \<lbrace>\<lambda>_. valid_machine_state\<rbrace>" 1663 apply (simp add: set_pt_def set_object_def) 1664 apply (wp get_object_wp) 1665 apply (clarsimp simp: valid_machine_state_def in_user_frame_def obj_at_def 1666 split: kernel_object.splits arch_kernel_obj.splits) 1667 apply (frule_tac x=pa in spec) 1668 apply (frule_tac x=p in spec) 1669 apply (clarsimp simp add: a_type_simps) 1670 apply (rule_tac x=sz in exI) 1671 apply (clarsimp simp: a_type_simps) 1672 done 1673 1674crunch valid_irq_states[wp]: set_pt "valid_irq_states" 1675 (wp: crunch_wps) 1676 1677crunch valid_irq_states[wp]: set_pd "valid_irq_states" 1678 (wp: crunch_wps) 1679 1680 1681lemma set_pt_invs: (* ARMHYP *) 1682 "\<lbrace>invs and (\<lambda>s. \<forall>i. wellformed_pte (pt i)) and 1683 (\<lambda>s. (\<exists>\<rhd>p) s \<longrightarrow> valid_vspace_obj (PageTable pt) s) and 1684 (\<lambda>s. \<exists>slot asid. caps_of_state s slot = 1685 Some (cap.ArchObjectCap (arch_cap.PageTableCap p asid)) \<and> 1686 (pt = (\<lambda>x. InvalidPTE) \<or> asid \<noteq> None)) and 1687 (\<lambda>s. \<forall>ref. (ref \<unrhd> p) s \<longrightarrow> 1688 (\<forall>x p. pte_ref_pages (pt x) = Some p \<longrightarrow> 1689 (\<exists>p' cap. caps_of_state s p' = Some cap \<and> 1690 p \<in> obj_refs cap \<and> 1691 vs_cap_ref cap = 1692 Some (VSRef (ucast x) (Some APageTable) # ref))))\<rbrace> 1693 set_pt p pt 1694 \<lbrace>\<lambda>_. invs\<rbrace>" 1695 apply (simp add: invs_def valid_state_def valid_pspace_def) 1696 apply (rule hoare_pre) 1697 apply (wp set_pt_valid_objs set_pt_iflive set_pt_zombies 1698 set_pt_zombies_state_refs set_pt_zombies_state_hyp_refs set_pt_valid_mdb 1699 set_pt_valid_idle set_pt_ifunsafe set_pt_reply_caps set_pt_valid_global_objs 1700 set_pt_valid_arch_state set_pt_valid_global set_pt_cur 1701 set_pt_reply_masters valid_irq_node_typ set_pt_valid_global_vspace_mappings 1702 valid_irq_handlers_lift) 1703 apply (clarsimp dest!: valid_objs_caps) 1704 apply (frule (1) valid_global_refsD2) 1705 apply (clarsimp simp add: cap_range_def is_pt_cap_def) 1706 apply (thin_tac "ALL x. P x" for P)+ 1707 apply (clarsimp simp: valid_arch_caps_def unique_table_caps_def) 1708 apply (drule_tac x=aa in spec, drule_tac x=ba in spec) 1709 apply (drule_tac x=a in spec, drule_tac x=b in spec) 1710 apply (clarsimp simp: is_pt_cap_def cap_asid_def) 1711 done 1712 1713(* FIXME: move to Invariants_A *) 1714lemma invs_valid_asid_table [elim!]: 1715 "invs s \<Longrightarrow> valid_asid_table (arm_asid_table (arch_state s)) s" 1716 by (simp add: invs_def valid_state_def valid_arch_state_def) 1717 1718 1719(* FIXME: move to Invariants_A *) 1720lemma valid_asid_table_ran: 1721 "valid_asid_table atcb s \<Longrightarrow> \<forall>p\<in>ran atcb. asid_pool_at p s" 1722 by (simp add: invs_def valid_state_def valid_arch_state_def 1723 valid_asid_table_def) 1724 1725 1726lemma vs_lookup_pages_pt_eq: (* ARMHYP *) 1727 "\<lbrakk>valid_vspace_objs s; 1728 \<forall>p\<in>ran (arm_asid_table (arch_state s)). asid_pool_at p s; 1729 page_table_at p s\<rbrakk> 1730 \<Longrightarrow> (ref \<unrhd> p) s = (ref \<rhd> p) s" 1731 apply (rule iffI[rotated]) 1732 apply (erule vs_lookup_pages_vs_lookupI) 1733 apply (erule (2) vs_lookup_pagesE_alt) 1734 apply (clarsimp simp: obj_at_def)+ 1735 apply (clarsimp simp: obj_at_def pde_ref_pages_def 1736 split: pde.splits) 1737 apply (erule (4) vs_lookup_pdI) 1738 apply (auto simp: obj_at_def pte_ref_pages_def data_at_def 1739 split: pte.splits) 1740 done 1741 1742 1743lemmas invs_ran_asid_table = invs_valid_asid_table[THEN valid_asid_table_ran] 1744 1745 1746(* NOTE: we use vs_lookup in the precondition because in this case, 1747 both are equivalent, but vs_lookup is generally preserved 1748 by store_pte while vs_lookup_pages might not. *) 1749lemma store_pte_invs [wp]: 1750 "\<lbrace>invs and (\<lambda>s. (\<exists>\<rhd>(p && ~~ mask pt_bits)) s \<longrightarrow> valid_pte pte s) and 1751 (\<lambda>s. wellformed_pte pte) and 1752 (\<lambda>s. \<exists>slot asid. caps_of_state s slot = 1753 Some (ArchObjectCap 1754 (PageTableCap (p && ~~ mask pt_bits) asid)) \<and> 1755 (pte = InvalidPTE \<or> asid \<noteq> None)) and 1756 (\<lambda>s. \<forall>ref. (ref \<rhd> (p && ~~ mask pt_bits)) s \<longrightarrow> 1757 (\<forall>q. pte_ref_pages pte = Some q \<longrightarrow> 1758 (\<exists>p' cap. caps_of_state s p' = Some cap \<and> 1759 q \<in> obj_refs cap \<and> 1760 vs_cap_ref cap = 1761 Some (VSRef (p && mask pt_bits >> pte_bits) 1762 (Some APageTable) # ref))))\<rbrace> 1763 store_pte p pte \<lbrace>\<lambda>_. invs\<rbrace>" 1764 apply (simp add: store_pte_def) 1765 apply (wp dmo_invs set_pt_invs) 1766 apply clarsimp 1767 apply (intro conjI) 1768 apply (drule invs_valid_objs) 1769 apply (fastforce simp: valid_objs_def dom_def obj_at_def valid_obj_def wellformed_vspace_obj_def) 1770 apply clarsimp 1771 apply (drule (1) valid_vspace_objsD, fastforce) 1772 apply simp 1773 apply (thin_tac "All _") 1774 apply (rule exI)+ 1775 apply (rule conjI, assumption) 1776 subgoal premises prems for \<dots> asid 1777 proof (cases asid) 1778 case (Some a) from this show ?thesis 1779 by fastforce 1780 next 1781 case None from this prems show ?thesis 1782 apply clarsimp 1783 apply (rule ext) 1784 apply clarsimp 1785 apply (frule invs_pd_caps) 1786 apply (clarsimp simp add: valid_table_caps_def simp del: HOL.imp_disjL) 1787 apply (spec "p && ~~ mask pt_bits") 1788 apply (drule spec)+ 1789 apply (erule impE, assumption) 1790 by (simp add: is_pt_cap_def cap_asid_def empty_table_def obj_at_def) 1791 qed 1792 apply (clarsimp simp: obj_at_def) 1793 apply (intro impI conjI allI) 1794 apply (drule (2) vs_lookup_pages_pt_eq[OF invs_vspace_objs invs_ran_asid_table, 1795 THEN iffD1, rotated -1]) 1796 apply (clarsimp simp: obj_at_def a_type_simps) 1797 apply (drule spec, erule impE, assumption)+ 1798 apply (erule exEI)+ 1799 apply clarsimp 1800 apply (rule sym) 1801 apply (rule ucast_ucast_len) 1802 apply (rule shiftr_less_t2n) 1803 using and_mask_less'[of 12 p] 1804 apply (simp add: vspace_bits_defs) 1805 subgoal for \<dots> pa 1806 apply (thin_tac "All _", thin_tac "_ \<longrightarrow> _", thin_tac "_ \<or> _") 1807 apply (frule invs_valid_vs_lookup) 1808 apply (simp add: valid_vs_lookup_def) 1809 apply (spec pa) 1810 apply (drule spec, erule impE) 1811 apply (erule vs_lookup_pages_step) 1812 by (fastforce simp: vs_lookup_pages1_def obj_at_def 1813 vs_refs_pages_def graph_of_def image_def) simp 1814 done 1815 1816lemma set_asid_pool_iflive [wp]: 1817 "\<lbrace>\<lambda>s. if_live_then_nonz_cap s\<rbrace> 1818 set_asid_pool p ap 1819 \<lbrace>\<lambda>_ s. if_live_then_nonz_cap s\<rbrace>" 1820 apply (wpsimp simp: set_asid_pool_def wp: get_object_wp set_object_iflive) 1821 apply (clarsimp split: kernel_object.splits arch_kernel_obj.splits) 1822 apply (clarsimp simp: obj_at_def live_def hyp_live_def arch_live_def) 1823 done 1824 1825 1826lemma set_asid_pool_zombies [wp]: 1827 "\<lbrace>\<lambda>s. zombies_final s\<rbrace> 1828 set_asid_pool p ap 1829 \<lbrace>\<lambda>_ s. zombies_final s\<rbrace>" 1830 apply (wpsimp simp: set_asid_pool_def wp: get_object_wp set_object_zombies) 1831 apply (clarsimp split: kernel_object.splits arch_kernel_obj.splits) 1832 apply (clarsimp simp: obj_at_def) 1833 done 1834 1835 1836lemma set_asid_pool_zombies_state_refs [wp]: 1837 "\<lbrace>\<lambda>s. P (state_refs_of s)\<rbrace> 1838 set_asid_pool p ap 1839 \<lbrace>\<lambda>_ s. P (state_refs_of s)\<rbrace>" 1840 apply (wpsimp simp: set_asid_pool_def set_object_def wp: get_object_wp) 1841 apply (clarsimp split: kernel_object.splits arch_kernel_obj.splits) 1842 apply (erule rsubst [where P=P]) 1843 apply (rule ext) 1844 apply (clarsimp simp: obj_at_def state_refs_of_def split: option.splits) 1845 done 1846 1847lemma set_asid_pool_zombies_state_hyp_refs [wp]: 1848 "\<lbrace>\<lambda>s. P (state_hyp_refs_of s)\<rbrace> 1849 set_asid_pool p ap 1850 \<lbrace>\<lambda>_ s. P (state_hyp_refs_of s)\<rbrace>" 1851 apply (wpsimp simp: set_asid_pool_def set_object_def wp: get_object_wp) 1852 apply (clarsimp split: kernel_object.splits arch_kernel_obj.splits) 1853 apply (erule rsubst [where P=P]) 1854 apply (rule ext) 1855 apply (clarsimp simp: obj_at_def state_hyp_refs_of_def split: option.splits) 1856 done 1857 1858 1859lemma set_asid_pool_cdt [wp]: 1860 "\<lbrace>\<lambda>s. P (cdt s)\<rbrace> 1861 set_asid_pool p ap 1862 \<lbrace>\<lambda>_ s. P (cdt s)\<rbrace>" 1863 by (wpsimp simp: set_asid_pool_def wp: get_object_wp) 1864 1865 1866lemma set_asid_pool_caps_of_state [wp]: 1867 "\<lbrace>\<lambda>s. P (caps_of_state s)\<rbrace> set_asid_pool p ap \<lbrace>\<lambda>_ s. P (caps_of_state s)\<rbrace>" 1868 apply (wpsimp simp: set_asid_pool_def get_object_def bind_assoc set_object_def) 1869 apply (subst cte_wp_caps_of_lift) 1870 prefer 2 1871 apply assumption 1872 subgoal for _ y 1873 by (cases y, auto simp: cte_wp_at_cases) 1874 done 1875 1876lemma set_asid_pool_valid_mdb [wp]: 1877 "\<lbrace>\<lambda>s. valid_mdb s\<rbrace> 1878 set_asid_pool p ap 1879 \<lbrace>\<lambda>_ s. valid_mdb s\<rbrace>" 1880 by (wpsimp simp: set_asid_pool_def set_object_def wp: valid_mdb_lift get_object_wp) 1881 1882 1883lemma set_asid_pool_valid_idle [wp]: 1884 "\<lbrace>\<lambda>s. valid_idle s\<rbrace> 1885 set_asid_pool p ap 1886 \<lbrace>\<lambda>_ s. valid_idle s\<rbrace>" 1887 by (rule valid_idle_lift; wpsimp simp: set_asid_pool_def wp: get_object_wp) 1888 1889 1890lemma set_asid_pool_ifunsafe [wp]: 1891 "\<lbrace>\<lambda>s. if_unsafe_then_cap s\<rbrace> 1892 set_asid_pool p ap 1893 \<lbrace>\<lambda>_ s. if_unsafe_then_cap s\<rbrace>" 1894 apply (wpsimp simp: set_asid_pool_def wp: get_object_wp set_object_ifunsafe) 1895 apply (clarsimp split: kernel_object.splits arch_kernel_obj.splits) 1896 apply (clarsimp simp: obj_at_def) 1897 done 1898 1899 1900lemma set_asid_pool_reply_caps [wp]: 1901 "\<lbrace>\<lambda>s. valid_reply_caps s\<rbrace> 1902 set_asid_pool p ap 1903 \<lbrace>\<lambda>_ s. valid_reply_caps s\<rbrace>" 1904 by (wp valid_reply_caps_st_cte_lift) 1905 1906 1907lemma set_asid_pool_reply_masters [wp]: 1908 "\<lbrace>valid_reply_masters\<rbrace> 1909 set_asid_pool p ap 1910 \<lbrace>\<lambda>_. valid_reply_masters\<rbrace>" 1911 by (wp valid_reply_masters_cte_lift) 1912 1913 1914crunch global_ref [wp]: set_asid_pool "\<lambda>s. P (global_refs s)" 1915 (wp: crunch_wps) 1916 1917 1918crunch arch [wp]: set_asid_pool "\<lambda>s. P (arch_state s)" 1919 (wp: crunch_wps) 1920 1921 1922crunch idle [wp]: set_asid_pool "\<lambda>s. P (idle_thread s)" 1923 (wp: crunch_wps) 1924 1925 1926crunch irq [wp]: set_asid_pool "\<lambda>s. P (interrupt_irq_node s)" 1927 (wp: crunch_wps) 1928 1929crunch valid_irq_states[wp]: set_asid_pool "valid_irq_states" 1930 (wp: crunch_wps) 1931 1932lemma set_asid_pool_valid_global [wp]: 1933 "\<lbrace>\<lambda>s. valid_global_refs s\<rbrace> 1934 set_asid_pool p ap 1935 \<lbrace>\<lambda>_ s. valid_global_refs s\<rbrace>" 1936 by (wp valid_global_refs_cte_lift) 1937 1938 1939crunch interrupt_states[wp]: set_asid_pool "\<lambda>s. P (interrupt_states s)" 1940 (wp: crunch_wps) 1941 1942 1943lemma set_asid_pool_vspace_objs_unmap': 1944 "\<lbrace>valid_vspace_objs and (\<lambda>s. (\<exists>\<rhd>p) s \<longrightarrow> valid_vspace_obj (ASIDPool ap) s) and 1945 obj_at (\<lambda>ko. \<exists>ap'. ko = ArchObj (ASIDPool ap') \<and> graph_of ap \<subseteq> graph_of ap') p\<rbrace> 1946 set_asid_pool p ap \<lbrace>\<lambda>_. valid_vspace_objs\<rbrace>" 1947 apply (wpsimp simp: set_asid_pool_def obj_at_def wp: get_object_wp set_object_vspace_objs) 1948 apply (rule conjI) 1949 apply (clarsimp simp: a_type_def split: kernel_object.splits arch_kernel_obj.splits) 1950 apply (clarsimp simp: vs_refs_def) 1951 apply fastforce 1952 done 1953 1954 1955lemma set_asid_pool_vspace_objs_unmap: 1956 "\<lbrace>valid_vspace_objs and ko_at (ArchObj (ASIDPool ap)) p\<rbrace> 1957 set_asid_pool p (ap |` S) \<lbrace>\<lambda>_. valid_vspace_objs\<rbrace>" 1958 apply (wpsimp wp: set_asid_pool_vspace_objs_unmap' simp: obj_at_def graph_of_restrict_map) 1959 apply (drule valid_vspace_objsD, simp add: obj_at_def, assumption) 1960 apply simp 1961 by (auto simp: obj_at_def dest!: ran_restrictD) 1962 1963 1964lemma set_asid_pool_table_caps [wp]: 1965 "\<lbrace>valid_table_caps\<rbrace> set_asid_pool p ap \<lbrace>\<lambda>_. valid_table_caps\<rbrace>" 1966 apply (simp add: valid_table_caps_def) 1967 apply (rule hoare_lift_Pf2 [where f=caps_of_state];wp?) 1968 apply (simp add: set_asid_pool_def set_object_def) 1969 apply (wp get_object_wp) 1970 by (clarsimp split: kernel_object.splits arch_kernel_obj.splits) 1971 (fastforce simp: obj_at_def empty_table_def) 1972 1973 1974 1975(* FIXME: Move to Invariants_A *) 1976lemma vs_lookup_pages_stateI: 1977 assumes 1: "(ref \<unrhd> p) s" 1978 assumes ko: "\<And>ko p. ko_at ko p s \<Longrightarrow> obj_at (\<lambda>ko'. vs_refs_pages ko \<subseteq> vs_refs_pages ko') p s'" 1979 assumes table: "graph_of (arm_asid_table (arch_state s)) \<subseteq> graph_of (arm_asid_table (arch_state s'))" 1980 shows "(ref \<unrhd> p) s'" 1981 using 1 vs_lookup_pages_sub [OF ko table] by blast 1982 1983lemma set_asid_pool_vs_lookup_unmap': 1984 "\<lbrace>valid_vs_lookup and 1985 obj_at (\<lambda>ko. \<exists>ap'. ko = ArchObj (ASIDPool ap') \<and> graph_of ap \<subseteq> graph_of ap') p\<rbrace> 1986 set_asid_pool p ap \<lbrace>\<lambda>_. valid_vs_lookup\<rbrace>" 1987 apply (simp add: valid_vs_lookup_def pred_conj_def) 1988 apply (rule hoare_lift_Pf2 [where f=caps_of_state];wp?) 1989 apply (simp add: set_asid_pool_def set_object_def) 1990 apply (wp get_object_wp) 1991 apply (clarsimp simp: obj_at_def simp del: fun_upd_apply del: disjCI 1992 split: kernel_object.splits arch_kernel_obj.splits) 1993 subgoal for \<dots> pa ref 1994 apply (spec pa) 1995 apply (spec ref) 1996 apply (erule impE) 1997 apply (erule vs_lookup_pages_stateI) 1998 by (clarsimp simp: obj_at_def vs_refs_pages_def split: if_split_asm) 1999 fastforce+ 2000 done 2001 2002 2003lemma set_asid_pool_vs_lookup_unmap: 2004 "\<lbrace>valid_vs_lookup and ko_at (ArchObj (ASIDPool ap)) p\<rbrace> 2005 set_asid_pool p (ap |` S) \<lbrace>\<lambda>_. valid_vs_lookup\<rbrace>" 2006 apply (wp set_asid_pool_vs_lookup_unmap') 2007 by (clarsimp simp: obj_at_def 2008 elim!: subsetD [OF graph_of_restrict_map]) 2009 2010 2011lemma valid_pte_typ_at: 2012 "(\<And>T p. typ_at (AArch T) p s = typ_at (AArch T) p s') \<Longrightarrow> 2013 valid_pte pte s = valid_pte pte s'" 2014 by (case_tac pte, auto simp add: data_at_def) 2015 2016 2017lemma valid_pde_typ_at: 2018 "(\<And>T p. typ_at (AArch T) p s = typ_at (AArch T) p s') \<Longrightarrow> 2019 valid_pde pde s = valid_pde pde s'" 2020 by (case_tac pde, auto simp add: data_at_def) 2021 2022 2023crunch v_ker_map[wp]: set_asid_pool "valid_kernel_mappings" 2024 (ignore: set_object wp: set_object_v_ker_map crunch_wps) 2025 2026 2027lemma set_asid_pool_restrict_asid_map: 2028 "\<lbrace>valid_asid_map and ko_at (ArchObj (ASIDPool ap)) p and 2029 (\<lambda>s. \<forall>asid. asid \<le> mask asid_bits \<longrightarrow> ucast asid \<notin> S \<longrightarrow> 2030 arm_asid_table (arch_state s) (asid_high_bits_of asid) = Some p \<longrightarrow> 2031 arm_asid_map (arch_state s) asid = None)\<rbrace> 2032 set_asid_pool p (ap |` S) \<lbrace>\<lambda>_. valid_asid_map\<rbrace>" 2033 apply (simp add: set_asid_pool_def valid_asid_map_def set_object_def) 2034 apply (wp get_object_wp) 2035 apply (clarsimp split: kernel_object.splits arch_kernel_obj.splits 2036 simp del: fun_upd_apply) 2037 apply (drule(1) bspec) 2038 apply (clarsimp simp: vspace_at_asid_def obj_at_def graph_of_def) 2039 apply (drule subsetD, erule domI) 2040 apply simp 2041 apply (drule spec, drule(1) mp) 2042 apply simp 2043 apply (erule vs_lookupE) 2044 apply (rule vs_lookupI, simp) 2045 apply (clarsimp simp: vs_asid_refs_def graph_of_def) 2046 apply (drule rtranclD) 2047 apply (erule disjE, clarsimp) 2048 apply clarsimp 2049 apply (drule tranclD) 2050 apply clarsimp 2051 apply (rule r_into_rtrancl) 2052 apply (drule vs_lookup1D) 2053 apply clarsimp 2054 apply (subst vs_lookup1_def) 2055 apply (clarsimp simp: obj_at_def) 2056 apply (erule rtranclE) 2057 apply (clarsimp simp: vs_refs_def graph_of_def) 2058 apply (rule image_eqI[where x="(_, _)"]) 2059 apply (simp add: split_def) 2060 apply (clarsimp simp: restrict_map_def) 2061 apply (drule ucast_up_inj, simp) 2062 apply (simp add: mask_asid_low_bits_ucast_ucast) 2063 apply (drule ucast_up_inj, simp) 2064 apply clarsimp 2065 apply clarsimp 2066 apply (drule vs_lookup1_trans_is_append) 2067 apply clarsimp 2068 apply (drule vs_lookup1D) 2069 by clarsimp 2070 2071 2072lemma set_asid_pool_asid_map_unmap: 2073 "\<lbrace>valid_asid_map and ko_at (ArchObj (ASIDPool ap)) p and 2074 (\<lambda>s. \<forall>asid. asid \<le> mask asid_bits \<longrightarrow> 2075 ucast asid = x \<longrightarrow> 2076 arm_asid_table (arch_state s) (asid_high_bits_of asid) = Some p \<longrightarrow> 2077 arm_asid_map (arch_state s) asid = None)\<rbrace> 2078 set_asid_pool p (ap(x := None)) \<lbrace>\<lambda>_. valid_asid_map\<rbrace>" 2079 using set_asid_pool_restrict_asid_map[where S="- {x}"] 2080 by (simp add: restrict_map_def fun_upd_def if_flip) 2081 2082 2083lemma set_asid_pool_vspace_objs_unmap_single: 2084 "\<lbrace>valid_vspace_objs and ko_at (ArchObj (ASIDPool ap)) p\<rbrace> 2085 set_asid_pool p (ap(x := None)) \<lbrace>\<lambda>_. valid_vspace_objs\<rbrace>" 2086 using set_asid_pool_vspace_objs_unmap[where S="- {x}"] 2087 by (simp add: restrict_map_def fun_upd_def if_flip) 2088 2089 2090lemma set_asid_pool_only_idle [wp]: 2091 "\<lbrace>only_idle\<rbrace> set_asid_pool p ap \<lbrace>\<lambda>_. only_idle\<rbrace>" 2092 by (wp only_idle_lift set_asid_pool_typ_at) 2093 2094 2095lemma set_asid_pool_equal_mappings [wp]: 2096 "\<lbrace>equal_kernel_mappings\<rbrace> set_asid_pool p ap \<lbrace>\<lambda>rv. equal_kernel_mappings\<rbrace>" 2097 by (simp add: set_asid_pool_def | wp set_object_equal_mappings get_object_wp)+ 2098 2099lemma set_asid_pool_kernel_window[wp]: 2100 "\<lbrace>pspace_in_kernel_window\<rbrace> set_asid_pool p ap \<lbrace>\<lambda>rv. pspace_in_kernel_window\<rbrace>" 2101 apply (simp add: set_asid_pool_def) 2102 apply (wp set_object_pspace_in_kernel_window get_object_wp) 2103 including unfold_objects_asm 2104 by (clarsimp simp: a_type_def) 2105 2106lemma set_asid_pool_pspace_respects_device_region[wp]: 2107 "\<lbrace>pspace_respects_device_region\<rbrace> set_asid_pool p ap \<lbrace>\<lambda>rv. pspace_respects_device_region\<rbrace>" 2108 apply (simp add: set_asid_pool_def) 2109 apply (wp set_object_pspace_respects_device_region get_object_wp) 2110 including unfold_objects_asm 2111 by (clarsimp simp: a_type_def) 2112 2113lemma set_asid_pool_caps_kernel_window[wp]: 2114 "\<lbrace>cap_refs_in_kernel_window\<rbrace> set_asid_pool p ap \<lbrace>\<lambda>rv. cap_refs_in_kernel_window\<rbrace>" 2115 apply (simp add: set_asid_pool_def) 2116 apply (wp set_object_cap_refs_in_kernel_window get_object_wp) 2117 including unfold_objects_asm 2118 by clarsimp 2119 2120lemma set_asid_pool_caps_respects_device_region[wp]: 2121 "\<lbrace>cap_refs_respects_device_region\<rbrace> set_asid_pool p ap \<lbrace>\<lambda>rv. cap_refs_respects_device_region\<rbrace>" 2122 apply (simp add: set_asid_pool_def) 2123 apply (wp set_object_cap_refs_respects_device_region get_object_wp) 2124 including unfold_objects_asm 2125 by clarsimp 2126 2127lemma set_asid_pool_valid_ioc[wp]: 2128 "\<lbrace>valid_ioc\<rbrace> set_asid_pool p ap \<lbrace>\<lambda>_. valid_ioc\<rbrace>" 2129 apply (simp add: set_asid_pool_def) 2130 apply (wp set_object_valid_ioc_no_caps get_object_inv) 2131 including unfold_objects 2132 by (clarsimp simp: valid_def get_object_def simpler_gets_def assert_def 2133 return_def fail_def bind_def 2134 a_type_simps is_tcb is_cap_table) 2135 2136 2137lemma set_asid_pool_vms[wp]: 2138 "\<lbrace>valid_machine_state\<rbrace> set_asid_pool p S \<lbrace>\<lambda>_. valid_machine_state\<rbrace>" 2139 apply (simp add: set_asid_pool_def set_object_def) 2140 apply (wp get_object_wp) 2141 apply clarify 2142 apply (erule valid_machine_state_heap_updI) 2143 apply (fastforce simp: a_type_def obj_at_def 2144 split: kernel_object.splits arch_kernel_obj.splits)+ 2145 done 2146 2147lemma set_asid_pool_valid_global_vspace_mappings[wp]: 2148 "\<lbrace>valid_global_vspace_mappings\<rbrace> 2149 set_asid_pool p ap \<lbrace>\<lambda>rv. valid_global_vspace_mappings\<rbrace>" 2150 by (wpsimp simp: valid_global_vspace_mappings_def) 2151 2152lemma set_asid_pool_global_objs [wp]: 2153 "\<lbrace>valid_global_objs and valid_arch_state\<rbrace> 2154 set_asid_pool p ap 2155 \<lbrace>\<lambda>_. valid_global_objs\<rbrace>" 2156 apply (simp add: set_asid_pool_def set_object_def) 2157 apply (wp get_object_wp) 2158 apply (clarsimp simp del: fun_upd_apply 2159 split: kernel_object.splits arch_kernel_obj.splits) 2160 apply (clarsimp simp: valid_global_objs_def valid_vso_at_def) 2161 done 2162 2163lemma set_asid_pool_invs_restrict: 2164 "\<lbrace>invs and ko_at (ArchObj (ASIDPool ap)) p and 2165 (\<lambda>s. \<forall>asid. asid \<le> mask asid_bits \<longrightarrow> ucast asid \<notin> S \<longrightarrow> 2166 arm_asid_table (arch_state s) (asid_high_bits_of asid) = Some p \<longrightarrow> 2167 arm_asid_map (arch_state s) asid = None)\<rbrace> 2168 set_asid_pool p (ap |` S) \<lbrace>\<lambda>_. invs\<rbrace>" 2169 apply (simp add: invs_def valid_state_def valid_pspace_def 2170 valid_arch_caps_def) 2171 apply (rule hoare_pre, 2172 wp valid_irq_node_typ set_asid_pool_typ_at 2173 set_asid_pool_vspace_objs_unmap valid_irq_handlers_lift 2174 set_asid_pool_vs_lookup_unmap set_asid_pool_restrict_asid_map) 2175 apply simp 2176 done 2177 2178lemmas set_asid_pool_cte_wp_at1[wp] 2179 = hoare_cte_wp_caps_of_state_lift [OF set_asid_pool_caps_of_state] 2180 2181 2182lemma mdb_cte_at_set_asid_pool[wp]: 2183 "\<lbrace>\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)\<rbrace> 2184 set_asid_pool y pool 2185 \<lbrace>\<lambda>r s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s)\<rbrace>" 2186 apply (clarsimp simp:mdb_cte_at_def) 2187 apply (simp only: imp_conv_disj) 2188 apply (wp hoare_vcg_disj_lift hoare_vcg_all_lift) 2189done 2190 2191lemma set_asid_pool_invs_unmap: 2192 "\<lbrace>invs and ko_at (ArchObj (ASIDPool ap)) p and 2193 (\<lambda>s. \<forall>asid. asid \<le> mask asid_bits \<longrightarrow> ucast asid = x \<longrightarrow> 2194 arm_asid_table (arch_state s) (asid_high_bits_of asid) = Some p \<longrightarrow> 2195 arm_asid_map (arch_state s) asid = None)\<rbrace> 2196 set_asid_pool p (ap(x := None)) \<lbrace>\<lambda>_. invs\<rbrace>" 2197 using set_asid_pool_invs_restrict[where S="- {x}"] 2198 by (simp add: restrict_map_def fun_upd_def if_flip) 2199 2200 2201lemma valid_slots_typ_at: 2202 assumes x: "\<And>T p. \<lbrace>typ_at (AArch T) p\<rbrace> f \<lbrace>\<lambda>rv. typ_at (AArch T) p\<rbrace>" 2203 assumes y: "\<And>p. \<lbrace>\<exists>\<rhd> p\<rbrace> f \<lbrace>\<lambda>rv. \<exists>\<rhd> p\<rbrace>" 2204 shows "\<lbrace>valid_slots m\<rbrace> f \<lbrace>\<lambda>rv. valid_slots m\<rbrace>" 2205 unfolding valid_slots_def 2206 by (cases m; clarsimp; wp x y hoare_vcg_const_Ball_lift valid_pte_lift 2207 valid_pde_lift pte_at_atyp pde_at_atyp) 2208 2209 2210lemma ucast_ucast_id: 2211 "(len_of TYPE('a)) < (len_of TYPE('b)) \<Longrightarrow> ucast ((ucast (x::('a::len) word))::('b::len) word) = x" 2212 by (auto intro: ucast_up_ucast_id simp: is_up_def source_size_def target_size_def word_size) 2213 2214 2215lemma lookup_pt_slot_looks_up [wp]: (* ARMHYP *) 2216 "\<lbrace>ref \<rhd> pd and K (is_aligned pd 14 \<and> vptr < kernel_base) 2217 and valid_arch_state and valid_vspace_objs and equal_kernel_mappings 2218 and pspace_aligned and valid_global_objs\<rbrace> 2219 lookup_pt_slot pd vptr 2220 \<lbrace>\<lambda>pt_slot. (VSRef (vptr >> pageBits + pt_bits - pte_bits << pde_bits >> pde_bits) (Some APageDirectory) # ref) \<rhd> (pt_slot && ~~ mask pt_bits)\<rbrace>, -" 2221 apply (simp add: lookup_pt_slot_def vspace_bits_defs) 2222 apply (wp get_pde_wp|wpc)+ 2223 apply clarsimp 2224 apply (rule vs_lookup_step, assumption) 2225 apply (clarsimp simp: vs_lookup1_def lookup_pd_slot_def Let_def pd_shifting pd_shifting_dual) 2226 apply (rule exI, rule conjI, assumption) 2227 subgoal for s _ x 2228 apply (prove "ptrFromPAddr x + ((vptr >> 12) && 0x1FF << 3) && ~~ mask pt_bits = ptrFromPAddr x") 2229 apply (prove "is_aligned (ptrFromPAddr x) 12") 2230 apply (drule (2) valid_vspace_objsD) 2231 apply clarsimp 2232 apply (erule_tac x="ucast (vptr >> pageBits + pt_bits - pte_bits << pde_bits >> pde_bits)" in allE) 2233 apply (thin_tac "obj_at P x s" for P x)+ 2234 apply (clarsimp simp: obj_at_def invs_def valid_state_def valid_pspace_def pspace_aligned_def vspace_bits_defs) 2235 apply (drule bspec, blast) 2236 apply (clarsimp simp: a_type_def vspace_bits_defs 2237 split: kernel_object.splits arch_kernel_obj.splits if_split_asm) 2238 apply (subgoal_tac "(vptr >> 12) && 0x1FF << 3 < 2 ^ 12") 2239 apply (subst is_aligned_add_or, (simp add: vspace_bits_defs)+) 2240 apply (subst word_ao_dist) 2241 apply (subst mask_out_sub_mask [where x="(vptr >> 12) && 0x1FF << 3"]) 2242 apply (fastforce simp: less_mask_eq) 2243 apply (rule shiftl_less_t2n, simp add: vspace_bits_defs) 2244 apply (rule and_mask_less'[where n=9, unfolded mask_def, simplified], (simp )+) 2245 apply (simp add: vspace_bits_defs mask_def) 2246 apply (erule vs_refs_pdI) 2247 apply (subst shiftl_shiftr_id) 2248 apply (simp add: word_bits_def)+ 2249 apply word_bitwise 2250 apply (clarsimp simp: nth_shiftr) 2251 apply (frule_tac n="n + 21" in test_bit_size) 2252 by (simp add: word_size) 2253done 2254 2255lemma lookup_pt_slot_reachable [wp]: (* ARMHYP *) 2256 "\<lbrace>\<exists>\<rhd> pd and K (is_aligned pd 14 \<and> vptr < kernel_base) 2257 and valid_arch_state and valid_vspace_objs and equal_kernel_mappings 2258 and pspace_aligned and valid_global_objs\<rbrace> 2259 lookup_pt_slot pd vptr 2260 \<lbrace>\<lambda>pt_slot. \<exists>\<rhd> (pt_slot && ~~ mask pt_bits)\<rbrace>, -" 2261 apply (simp add: pred_conj_def ex_simps [symmetric] del: ex_simps) 2262 apply (rule hoare_vcg_ex_lift_R1) 2263 apply (rule hoare_pre) 2264 apply (rule hoare_post_imp_R) 2265 apply (rule lookup_pt_slot_looks_up) 2266 prefer 2 2267 apply clarsimp 2268 apply assumption 2269 apply fastforce 2270 done 2271 2272lemma lookup_pt_slot_reachable2 [wp]: (* ARMHYP *) 2273 "\<lbrace>\<exists>\<rhd> pd and K (is_aligned pd 14 \<and> is_aligned vptr 16 \<and> vptr < kernel_base) 2274 and valid_arch_state and valid_vspace_objs and equal_kernel_mappings 2275 and pspace_aligned and valid_global_objs\<rbrace> 2276 lookup_pt_slot pd vptr 2277 \<lbrace>\<lambda>rv s. \<forall>x\<in>set [0 , 8 .e. 0x78]. (\<exists>\<rhd> (rv + x && ~~ mask pt_bits)) s\<rbrace>, -" 2278 apply (simp add: lookup_pt_slot_def) 2279 apply (wp get_pde_wp|wpc)+ 2280 apply clarsimp 2281 apply (rule exI) 2282 apply (rule vs_lookup_step, assumption) 2283 apply (clarsimp simp: vs_lookup1_def lookup_pd_slot_def Let_def) 2284 apply (clarsimp simp: pd_shifting_dual pd_shifting) 2285 apply (rule exI, rule conjI, assumption) 2286 apply (rule_tac x="VSRef (vptr >> pageBits + pt_bits - pte_bits << pde_bits >> pde_bits) (Some APageDirectory)" in exI) 2287 apply (subgoal_tac "ptrFromPAddr x + (xa + ((vptr >> pageBits) && 0x1FF << 3)) && ~~ mask pt_bits = ptrFromPAddr x") 2288 prefer 2 2289 apply (subgoal_tac "is_aligned (ptrFromPAddr x) 12") 2290 prefer 2 2291 apply (clarsimp simp: vspace_bits_defs) 2292 apply (drule (2) valid_vspace_objsD) 2293 apply clarsimp 2294 apply (erule_tac x="ucast (vptr >> pageBits + pt_bits - pte_bits << pde_bits >> pde_bits)" in allE) 2295 apply (clarsimp simp: vspace_bits_defs) 2296 apply (drule is_aligned_pt; (assumption|simp add: vspace_bits_defs)) 2297 apply (subst add_mask_lower_bits) 2298 apply (simp add: vspace_bits_defs) 2299 prefer 2 2300 apply simp 2301 apply (clarsimp simp: vspace_bits_defs) 2302 apply (clarsimp simp: upto_enum_step_def word_shift_by_n[of _ 3, simplified] p_le_0xF_helper) 2303 apply (thin_tac "pda x = t" for x t) 2304 apply (subst (asm) word_plus_and_or_coroll) 2305 apply (rule word_eqI) 2306 apply (clarsimp simp: word_1FF_is_mask word_size word_bits_def nth_shiftr nth_shiftl is_aligned_nth) 2307 apply (erule_tac x="n - 3" in allE) 2308 apply simp 2309 apply (clarsimp simp: word_size nth_shiftr nth_shiftl is_aligned_nth word_bits_def) 2310 apply (simp add: vspace_bits_defs) 2311 apply (rule conjI, rule refl) 2312 apply (simp add: add.commute add.left_commute word_1FF_is_mask) 2313 apply (rule vs_refs_pdI) 2314 prefer 2 2315 apply (clarsimp simp: word_ops_nth_size word_size nth_shiftr nth_shiftl) 2316 apply (drule test_bit_size) 2317 apply (simp add: word_size) 2318 apply fastforce 2319 done 2320 2321lemma lookup_pt_slot_reachable3 [wp]: (* ARMHYP *) 2322 "\<lbrace>\<exists>\<rhd> pd and K (is_aligned pd 14 \<and> is_aligned vptr 16 \<and> vptr < kernel_base) 2323 and valid_arch_state and valid_vspace_objs and equal_kernel_mappings 2324 and pspace_aligned and valid_global_objs\<rbrace> 2325 lookup_pt_slot pd vptr 2326 \<lbrace>\<lambda>p s. \<forall>x\<in>set [p, p + 8 .e. p + 0x78]. (\<exists>\<rhd> (x && ~~ mask pt_bits)) s\<rbrace>, -" 2327 apply (simp add: lookup_pt_slot_def) 2328 apply (wp get_pde_wp|wpc)+ 2329 apply (clarsimp del: ballI) 2330 apply (clarsimp simp: lookup_pd_slot_def Let_def del: ballI) 2331 apply (simp add: pd_shifting) 2332 apply (frule (2) valid_vspace_objsD) 2333 apply (clarsimp del: ballI) 2334 apply (erule_tac x="(ucast (pd + (vptr >> pageBits + pt_bits - pte_bits << pde_bits) && mask pd_bits >> pde_bits))" in allE) 2335 apply (clarsimp del: ballI) 2336 apply (subgoal_tac "is_aligned (ptrFromPAddr x) pageBits") 2337 prefer 2 2338 apply (thin_tac "ko_at P p s" for P p)+ 2339 apply (clarsimp simp: obj_at_def add.commute add.left_commute pspace_aligned_def vspace_bits_defs) 2340 apply (drule bspec, blast) 2341 apply (clarsimp simp: a_type_def vspace_bits_defs 2342 split: kernel_object.splits arch_kernel_obj.splits if_split_asm) 2343 apply (simp add: vspace_bits_defs) 2344 apply (subst p_0x3C_shift) 2345 apply (rule aligned_add_aligned, assumption) 2346 apply (clarsimp intro!: is_aligned_andI1 is_aligned_shiftl is_aligned_shiftr) 2347 apply simp 2348 apply clarsimp 2349 apply (rule exI) 2350 apply (rule vs_lookup_step, assumption) 2351 apply (clarsimp simp: vs_lookup1_def lookup_pd_slot_def Let_def 2352 pd_shifting[simplified vspace_bits_defs, simplified] 2353 pd_shifting_dual[simplified vspace_bits_defs, simplified] 2354 add.commute add.left_commute) 2355 apply (rule exI, rule conjI, assumption) 2356 apply (rule_tac x="VSRef (vptr >> pageBits + pt_bits - pte_bits << pde_bits >> pde_bits) (Some APageDirectory)" in exI) 2357 apply (rule conjI, rule refl) 2358 apply (rename_tac xa) 2359 apply (subgoal_tac "ptrFromPAddr x + (xa + ((vptr >> 12) && 0x1FF << 3)) && ~~ mask pt_bits = ptrFromPAddr x") 2360 prefer 2 2361 apply (subst add_mask_lower_bits) 2362 apply (simp add: vspace_bits_defs) 2363 prefer 2 2364 apply simp 2365 apply (clarsimp simp: vspace_bits_defs) 2366 apply (clarsimp simp: upto_enum_step_def word_shift_by_n[of _ 3, simplified] p_le_0xF_helper) 2367 apply (thin_tac "pda x = t" for x t) 2368 apply (subst (asm) word_plus_and_or_coroll) 2369 apply (rule word_eqI) 2370 apply (clarsimp simp: vspace_bits_defs word_size word_bits_def nth_shiftr nth_shiftl is_aligned_nth word_FF_is_mask) 2371 apply (erule_tac x="n - 3" in allE) 2372 apply simp 2373 apply (clarsimp simp: vspace_bits_defs word_size nth_shiftr nth_shiftl is_aligned_nth word_FF_is_mask word_bits_def) 2374 apply (simp add: word_1FF_is_mask vspace_bits_defs add.commute add.left_commute) 2375 apply (rule vs_refs_pdI) 2376 prefer 2 2377 apply (clarsimp simp: word_ops_nth_size word_size nth_shiftr nth_shiftl) 2378 apply (drule test_bit_size) 2379 apply (simp add: word_size) 2380 apply fastforce 2381 done 2382 2383lemma pd_aligned: 2384 "\<lbrakk>pspace_aligned s; page_directory_at pd s\<rbrakk> \<Longrightarrow> is_aligned pd 14" 2385 apply (clarsimp simp: pspace_aligned_def obj_at_def) 2386 apply (drule bspec, blast) 2387 apply (clarsimp simp: a_type_def vspace_bits_defs 2388 split: kernel_object.splits arch_kernel_obj.splits if_split_asm) 2389 done 2390 2391 2392lemma shiftr_shiftl_mask_pd_bits: 2393 "(((vptr :: word32) >> pageBits + pt_bits - pte_bits) << pde_bits) && mask pd_bits = (vptr >> pageBits + pt_bits - pte_bits) << pde_bits" 2394 apply (rule iffD2 [OF mask_eq_iff_w2p]) 2395 apply (simp add: vspace_bits_defs word_size) 2396 apply (simp only: vspace_bits_defs) 2397 apply (rule shiftl_less_t2n) 2398 apply (rule shiftr_less_t2n3, 2399 simp_all add: pd_bits_def word_bits_def pageBits_def) 2400 done 2401 2402 2403lemma triple_shift_fun: 2404 "x >> 21 << 3 >> 3 = (x :: ('a :: len) word) >> 21" 2405 apply (rule word_eqI) 2406 apply (simp add: word_size nth_shiftr nth_shiftl) 2407 apply safe 2408 apply (drule test_bit_size) 2409 apply (simp add: word_size) 2410 done 2411 2412 2413lemma shiftr_21_unat_ucast: 2414 "unat (ucast (x >> 21 :: word32) :: 12 word) = unat (x >> 21)" 2415 using vptr_shiftr_le_2p[where vptr=x] 2416 apply (simp only: unat_ucast) 2417 apply (rule mod_less) 2418 apply (rule unat_less_power) 2419 apply (simp add: word_bits_def) 2420 apply (simp add: pageBits_def) 2421 done 2422 2423 2424lemma shiftr_21_less: 2425 "((ucast (x >> 21) :: 12 word) < ucast (y >> 21)) = ((x >> 21 :: word32) < y >> 21)" 2426 "((ucast (x >> 21) :: 12 word) \<le> ucast (y >> 21)) = ((x >> 21 :: word32) \<le> y >> 21)" 2427 by (simp add: word_less_nat_alt word_le_nat_alt shiftr_21_unat_ucast)+ 2428 2429 2430lemma kernel_base_ge_observation: 2431 "(kernel_base \<le> x) = (x && ~~ mask 29 = kernel_base)" 2432 apply (subst mask_in_range) 2433 apply (simp add: kernel_base_def is_aligned_def) 2434 apply (simp add: kernel_base_def) 2435 done 2436 2437 2438lemma kernel_base_less_observation: 2439 "(x < kernel_base) = (x && ~~ mask 29 \<noteq> kernel_base)" 2440 apply (simp add: linorder_not_le[symmetric] kernel_base_ge_observation) 2441 done 2442 2443lemma is_aligned_lookup_pd_slot: 2444 "\<lbrakk>is_aligned vptr 25; is_aligned pd 7\<rbrakk> 2445 \<Longrightarrow> is_aligned (lookup_pd_slot pd vptr) 7" 2446 apply (clarsimp simp: lookup_pd_slot_def) 2447 apply (erule aligned_add_aligned) 2448 apply (rule is_aligned_shiftl) 2449 apply (rule is_aligned_shiftr) 2450 apply (simp add: vspace_bits_defs) 2451 apply (simp add: word_bits_conv) 2452 done 2453 2454lemma lookup_pd_slot_eq: 2455 "is_aligned pd pd_bits \<Longrightarrow> 2456 (lookup_pd_slot pd vptr && ~~ mask pd_bits) = pd" 2457 apply (clarsimp simp: lookup_pd_slot_def) 2458 apply (erule conjunct2[OF is_aligned_add_helper]) 2459 apply (rule shiftl_less_t2n) 2460 apply (rule shiftr_less_t2n3) 2461 apply (simp_all add: vspace_bits_defs) 2462 done 2463 2464lemma is_aligned_lookup_pt_slot_no_fail: 2465 "\<lbrakk>is_aligned vptr 16; is_aligned pt 7\<rbrakk> 2466 \<Longrightarrow> is_aligned (lookup_pt_slot_no_fail pt vptr) 7" 2467 apply (clarsimp simp: lookup_pt_slot_no_fail_def) 2468 apply (erule aligned_add_aligned) 2469 apply (rule is_aligned_shiftl) 2470 apply (rule is_aligned_andI1) 2471 apply (rule is_aligned_shiftr) 2472 by (simp add: vspace_bits_defs)+ 2473 2474lemma lookup_pt_slot_non_empty: 2475 "\<lbrace>valid_vspace_objs and \<exists>\<rhd> pd and page_directory_at pd and pspace_aligned 2476 and K (is_aligned vptr 16 \<and> vptr < kernel_base)\<rbrace> 2477 lookup_pt_slot pd vptr \<lbrace>\<lambda>rv s. [0 , 8 .e. 0x78] \<noteq> []\<rbrace>, -" 2478 apply (simp add:lookup_pt_slot_def) 2479 apply (wp get_pde_wp| wpc | clarsimp)+ 2480 apply (simp add:valid_vspace_objs_def) 2481 apply (drule_tac x = "(lookup_pd_slot pd vptr && ~~ mask pd_bits)" in spec) 2482 apply (erule impE) 2483 apply (subst lookup_pd_slot_eq) 2484 apply (clarsimp simp: obj_at_def) 2485 apply (drule_tac p = pd in pspace_alignedD) 2486 apply simp 2487 apply (simp add:obj_bits_def vspace_bits_defs) 2488 apply fastforce 2489 apply (drule spec) 2490 apply (clarsimp simp:valid_vspace_obj_def ) 2491 apply (clarsimp simp: obj_at_def) 2492 apply (drule_tac p = pd in pspace_alignedD) 2493 apply simp 2494 apply (simp add:obj_bits_def vspace_bits_defs) 2495 apply (drule arg_cong[where f = length]) 2496 apply (subst (asm) length_upto_enum_step) 2497 apply simp+ 2498done 2499 2500 2501lemma create_mapping_entries_valid_slots [wp]: (* ARMHYP *) 2502 "\<lbrace>valid_arch_state and valid_vspace_objs and equal_kernel_mappings 2503 and pspace_aligned and valid_global_objs 2504 and \<exists>\<rhd> pd and page_directory_at pd and data_at sz (ptrFromPAddr base) and 2505 K (is_aligned base pageBits \<and> vmsz_aligned vptr sz \<and> vptr < kernel_base \<and> 2506 vm_rights \<in> valid_vm_rights)\<rbrace> 2507 create_mapping_entries base vptr sz vm_rights attrib pd 2508 \<lbrace>\<lambda>m. valid_slots m\<rbrace>, -" 2509 apply (cases sz) 2510 apply (rule hoare_pre) 2511 apply (wp lookup_pt_slot_inv | simp add: valid_slots_def)+ 2512 apply (clarsimp simp: pd_aligned) 2513 apply (rule hoare_pre) 2514 apply (simp add: valid_slots_def largePagePTE_offsets_def vspace_bits_defs) 2515 apply (wp lookup_pt_slot_inv; simp add: ) 2516 apply (simp add: valid_slots_def ball_conj_distrib add.commute 2517 largePagePTE_offsets_def)+ 2518 apply (wp lookup_pt_slot_non_empty) 2519 apply (wp lookup_pt_slot_inv) 2520 apply (clarsimp simp: pd_aligned vmsz_aligned_def) 2521 apply (clarsimp simp add: valid_slots_def) 2522 apply (rule hoare_pre) 2523 apply wp 2524 apply (clarsimp simp: valid_slots_def ) 2525 apply (rule conjI) 2526 apply (simp add: lookup_pd_slot_def Let_def) 2527 apply (fastforce simp: pd_shifting pd_aligned) 2528 apply (simp add: page_directory_pde_at_lookupI) 2529 apply simp 2530 apply (rule hoare_pre) 2531 apply (clarsimp simp add: valid_slots_def) 2532 apply wp 2533 apply simp 2534 apply (elim conjE) 2535 apply (thin_tac "is_aligned base b" for b) 2536 apply (subgoal_tac "is_aligned pd 14") 2537 prefer 2 2538 apply (clarsimp simp: pd_aligned) 2539 apply (simp add: superSectionPDE_offsets_def vspace_bits_defs) 2540 apply (clarsimp simp: upto_enum_step_def word_shift_by_n[of _ 3, simplified]) 2541 apply (clarsimp simp: obj_at_def pde_at_def) 2542 apply (subgoal_tac "is_aligned pd pd_bits") 2543 prefer 2 2544 apply (simp add: vspace_bits_defs) 2545 apply (rule conjI) 2546 apply (simp add: upto_enum_def) 2547 apply (intro allI impI) 2548 apply (simp add: pd_bits_def vmsz_aligned_def) 2549 apply (frule (1) is_aligned_lookup_pd_slot 2550 [OF _ is_aligned_weaken[of _ 14 7, simplified]]) 2551 apply (subgoal_tac "(p<<3) + lookup_pd_slot pd vptr && ~~ mask 14 = pd") 2552 prefer 2 2553 apply (subst add.commute add.left_commute) 2554 apply (subst and_not_mask_twice[where n=7 and m=14, simplified, symmetric]) 2555 apply (subst is_aligned_add_helper[THEN conjunct2], simp) 2556 apply (rule shiftl_less_t2n) 2557 apply (rule word_less_sub_le[THEN iffD1], simp+) 2558 apply (erule lookup_pd_slot_eq[simplified vspace_bits_defs, simplified]) 2559 apply (simp add: a_type_simps vspace_bits_defs) 2560 apply (subst add.commute) 2561 apply (fastforce intro!: aligned_add_aligned is_aligned_shiftl_self) 2562 done 2563 2564lemma is_aligned_addrFromPPtr_n: 2565 "\<lbrakk> is_aligned p n; n \<le> 28 \<rbrakk> \<Longrightarrow> is_aligned (Platform.ARM_HYP.addrFromPPtr p) n" 2566 apply (simp add: Platform.ARM_HYP.addrFromPPtr_def) 2567 apply (erule aligned_sub_aligned, simp_all) 2568 apply (simp add: physMappingOffset_def physBase_def 2569 kernelBase_addr_def pageBits_def) 2570 apply (erule is_aligned_weaken[rotated]) 2571 apply (simp add: is_aligned_def) 2572 done 2573 2574lemma is_aligned_addrFromPPtr: 2575 "is_aligned p pageBits \<Longrightarrow> is_aligned (Platform.ARM_HYP.addrFromPPtr p) pageBits" 2576 by (simp add: is_aligned_addrFromPPtr_n pageBits_def) 2577 2578lemma is_aligned_ptrFromPAddr_n: 2579 "\<lbrakk>is_aligned x sz; sz\<le> 28\<rbrakk> 2580 \<Longrightarrow> is_aligned (ptrFromPAddr x) sz" 2581 apply (simp add:ptrFromPAddr_def physMappingOffset_def 2582 kernelBase_addr_def physBase_def) 2583 apply (erule aligned_add_aligned) 2584 apply (erule is_aligned_weaken[rotated]) 2585 apply (simp add:is_aligned_def) 2586 apply (simp add:word_bits_def) 2587 done 2588 2589lemma is_aligned_ptrFromPAddr: 2590 "is_aligned p pageBits \<Longrightarrow> is_aligned (ptrFromPAddr p) pageBits" 2591 by (simp add: is_aligned_ptrFromPAddr_n pageBits_def) 2592 2593lemma store_pde_lookup_pd: (* ARMHYP *) 2594 "\<lbrace>\<exists>\<rhd> pd and page_directory_at pd and valid_vspace_objs 2595 and (\<lambda>s. valid_asid_table (arm_asid_table (arch_state s)) s)\<rbrace> 2596 store_pde p pde \<lbrace>\<lambda>_. \<exists>\<rhd> pd\<rbrace>" 2597 apply (simp add: store_pde_def set_pd_def set_object_def) 2598 apply (wp get_object_wp) 2599 apply clarsimp 2600 apply (clarsimp split: kernel_object.splits arch_kernel_obj.splits) 2601 apply (clarsimp simp: obj_at_def) 2602 apply (erule vs_lookupE) 2603 apply (clarsimp simp: vs_asid_refs_def graph_of_def) 2604 apply (drule rtranclD) 2605 apply (erule disjE) 2606 apply clarsimp 2607 apply (rule exI) 2608 apply (rule vs_lookup_atI) 2609 apply simp 2610 apply clarsimp 2611 apply (frule (1) valid_asid_tableD) 2612 apply (frule vs_lookup_atI) 2613 apply (frule (2) stronger_vspace_objsD) 2614 apply (clarsimp simp: obj_at_def a_type_def) 2615 apply (case_tac ao, simp_all, clarsimp) 2616 apply (drule tranclD) 2617 apply clarsimp 2618 apply (drule rtranclD) 2619 apply (erule disjE) 2620 apply clarsimp 2621 apply (rule_tac x=ref in exI) 2622 apply (rule vs_lookup_step) 2623 apply (rule vs_lookup_atI) 2624 apply simp 2625 apply (clarsimp simp: vs_lookup1_def) 2626 apply (clarsimp simp: obj_at_def vs_refs_def graph_of_def) 2627 apply clarsimp 2628 apply (drule (1) vs_lookup_step) 2629 apply (frule (2) stronger_vspace_objsD) 2630 apply clarsimp 2631 apply (drule vs_lookup1D) 2632 apply clarsimp 2633 apply (erule obj_atE)+ 2634 apply (clarsimp simp: vs_refs_def graph_of_def) 2635 apply (drule bspec, blast) 2636 apply (erule obj_atE)+ 2637 apply clarsimp 2638 apply (drule tranclD) 2639 apply clarsimp 2640 apply (drule rtranclD) 2641 apply clarsimp 2642 apply (drule vs_lookup1D) 2643 apply clarsimp 2644 apply (erule obj_atE)+ 2645 apply (clarsimp simp: vs_refs_def graph_of_def) 2646 apply (erule_tac x=ab in allE) 2647 apply (case_tac "pdb ab", simp_all add: pde_ref_def split: if_split_asm) 2648 apply (erule obj_atE) 2649 apply clarsimp 2650 apply (erule disjE) 2651 apply (clarsimp simp: a_type_def) 2652 apply clarsimp 2653 apply (drule tranclD) 2654 apply clarsimp 2655 apply (drule vs_lookup1D) 2656 apply clarsimp 2657 apply (erule obj_atE)+ 2658 apply (clarsimp simp: vs_refs_def graph_of_def) 2659 done 2660 2661 2662lemma store_pde_arch_objs_unmap: (* ARMHYP *) 2663 "\<lbrace>valid_vspace_objs 2664 and valid_pde pde 2665 and K (pde_ref pde = None)\<rbrace> 2666 store_pde p pde \<lbrace>\<lambda>_. valid_vspace_objs\<rbrace>" 2667 apply (simp add: store_pde_def) 2668 apply (wpsimp wp: set_pd_vspace_objs_unmap) 2669 apply (rule conjI) 2670 apply clarsimp 2671 apply (drule (1) valid_vspace_objsD, fastforce) 2672 apply simp 2673 apply (clarsimp simp add: obj_at_def vs_refs_def ) 2674 apply (rule pair_imageI) 2675 apply (simp add: graph_of_def split: if_split_asm) 2676 done 2677 2678 2679(* FIXME: remove magic numbers in other lemmas, use in pde_at_aligned_vptr et al *) 2680lemma lookup_pd_slot_add_eq: 2681 "\<lbrakk> is_aligned pd pd_bits; is_aligned vptr 25; x \<in> set [0 , 8 .e. 0x78] \<rbrakk> 2682 \<Longrightarrow> (x + lookup_pd_slot pd vptr && ~~ mask pd_bits) = pd" 2683 apply (simp add: vspace_bits_defs add.commute add.left_commute lookup_pd_slot_def Let_def) 2684 apply (clarsimp simp: upto_enum_step_def word_shift_by_n[of _ 3, simplified]) 2685 apply (subst add_mask_lower_bits, assumption) 2686 prefer 2 2687 apply simp 2688 apply clarsimp 2689 subgoal premises prems for _ n' 2690 proof - 2691 have H: "(0xF::word32) < 2 ^ 4" by simp 2692 from prems show ?thesis 2693 apply (subst (asm) word_plus_and_or_coroll) 2694 apply (rule word_eqI) 2695 apply (thin_tac "is_aligned pd _") 2696 apply (clarsimp simp: word_size nth_shiftl nth_shiftr is_aligned_nth) 2697 subgoal for n 2698 apply (spec "18 + n") 2699 apply (frule test_bit_size[where n="18 + n"]) 2700 apply (simp add: word_size) 2701 apply (insert H)[1] 2702 apply (drule (1) order_le_less_trans) 2703 apply (drule bang_is_le) 2704 apply (drule_tac z="2 ^ 4" in order_le_less_trans, assumption) 2705 apply (drule word_power_increasing) 2706 apply simp 2707 apply simp 2708 apply simp 2709 by arith 2710 apply simp 2711 apply (clarsimp simp: word_size nth_shiftl nth_shiftr is_aligned_nth) 2712 apply (erule disjE) 2713 apply (insert H)[1] 2714 apply (drule (1) order_le_less_trans) 2715 apply (drule bang_is_le) 2716 apply (drule_tac z="2 ^ 4" in order_le_less_trans, assumption) 2717 apply (drule word_power_increasing) 2718 apply simp 2719 apply simp 2720 apply simp 2721 apply arith 2722 apply (spec "18 + n'") 2723 apply (frule test_bit_size[where n="18 + n'"]) 2724 by (simp add: word_size) 2725 qed 2726done 2727 2728 2729lemma lookup_pd_slot_add: 2730 "\<lbrakk> page_directory_at pd s; pspace_aligned s; is_aligned vptr 25; x \<in> set [0 , 8 .e. 0x78] \<rbrakk> 2731 \<Longrightarrow> (x + lookup_pd_slot pd vptr && ~~ mask pd_bits) = pd" 2732 apply (clarsimp simp: obj_at_def pspace_aligned_def) 2733 apply (drule bspec, blast) 2734 apply (clarsimp simp: pd_bits_def pageBits_def a_type_def 2735 split: kernel_object.splits arch_kernel_obj.splits if_split_asm) 2736 apply (drule (1) lookup_pd_slot_add_eq [rotated]) 2737 apply (simp add: pd_bits_def pageBits_def) 2738 apply (simp add: pd_bits_def pageBits_def) 2739 done 2740 2741 2742lemma vs_lookup_arch_update: 2743 "arm_asid_table (f (arch_state s)) = arm_asid_table (arch_state s) \<Longrightarrow> 2744 vs_lookup (arch_state_update f s) = vs_lookup s" 2745 apply (rule order_antisym) 2746 apply (rule vs_lookup_sub) 2747 apply (clarsimp simp: obj_at_def) 2748 apply simp 2749 apply (rule vs_lookup_sub) 2750 apply (clarsimp simp: obj_at_def) 2751 apply simp 2752 done 2753 2754 2755lemma vs_lookup_pages_arch_update: 2756 "arm_asid_table (f (arch_state s)) = arm_asid_table (arch_state s) \<Longrightarrow> 2757 vs_lookup_pages (arch_state_update f s) = vs_lookup_pages s" 2758 apply (rule order_antisym) 2759 apply (rule vs_lookup_pages_sub) 2760 apply (clarsimp simp: obj_at_def) 2761 apply simp 2762 apply (rule vs_lookup_pages_sub) 2763 apply (clarsimp simp: obj_at_def) 2764 apply simp 2765 done 2766 2767 2768lemma vs_lookup_asid_map [iff]: 2769 "vs_lookup (s\<lparr>arch_state := arm_asid_map_update f (arch_state s)\<rparr>) = vs_lookup s" 2770 by (simp add: vs_lookup_arch_update) 2771 2772 2773lemma vs_lookup_hwasid_table [iff]: 2774 "vs_lookup (s\<lparr>arch_state := arm_hwasid_table_update f (arch_state s)\<rparr>) = vs_lookup s" 2775 by (simp add: vs_lookup_arch_update) 2776 2777 2778lemma vs_lookup_next_asid [iff]: 2779 "vs_lookup (s\<lparr>arch_state := arm_next_asid_update f (arch_state s)\<rparr>) = vs_lookup s" 2780 by (simp add: vs_lookup_arch_update) 2781 2782 2783lemma vs_lookup_pages_asid_map[iff]: 2784 "vs_lookup_pages (s\<lparr>arch_state := arm_asid_map_update f (arch_state s)\<rparr>) = 2785 vs_lookup_pages s" 2786 by (simp add: vs_lookup_pages_arch_update) 2787 2788 2789lemma vs_lookup_pages_hwasid_table[iff]: 2790 "vs_lookup_pages (s\<lparr>arch_state := arm_hwasid_table_update f (arch_state s)\<rparr>) = 2791 vs_lookup_pages s" 2792 by (simp add: vs_lookup_pages_arch_update) 2793 2794 2795lemma vs_lookup_pages_next_asid[iff]: 2796 "vs_lookup_pages (s\<lparr>arch_state := arm_next_asid_update f (arch_state s)\<rparr>) = 2797 vs_lookup_pages s" 2798 by (simp add: vs_lookup_pages_arch_update) 2799 2800 2801lemma valid_vspace_objs_arch_update: 2802 "arm_asid_table (f (arch_state s)) = arm_asid_table (arch_state s) \<Longrightarrow> 2803 valid_vspace_objs (arch_state_update f s) = valid_vspace_objs s" 2804 apply (rule iffI) 2805 apply (erule valid_vspace_objs_stateI) 2806 apply (clarsimp simp: obj_at_def) 2807 apply simp 2808 apply simp 2809 apply (erule valid_vspace_objs_stateI) 2810 apply (clarsimp simp: obj_at_def) 2811 apply simp 2812 apply simp 2813 done 2814 2815lemma store_pte_valid_vspace_objs[wp]: 2816 "\<lbrace>valid_vspace_objs and valid_pte pte\<rbrace> 2817 store_pte p pte 2818 \<lbrace>\<lambda>_. (valid_vspace_objs)\<rbrace>" 2819 unfolding store_pte_def 2820 apply wp 2821 apply clarsimp 2822 apply (unfold valid_vspace_objs_def) 2823 apply (erule_tac x="p && ~~ mask pt_bits" in allE) 2824 apply auto 2825done 2826 2827crunch valid_arch [wp]: store_pte valid_arch_state 2828 2829lemma set_pd_vs_lookup_unmap: 2830 "\<lbrace>valid_vs_lookup and 2831 obj_at (\<lambda>ko. vs_refs_pages (ArchObj (PageDirectory pd)) \<subseteq> vs_refs_pages ko) p\<rbrace> 2832 set_pd p pd 2833 \<lbrace>\<lambda>_. valid_vs_lookup\<rbrace>" 2834 apply (simp add: valid_vs_lookup_def pred_conj_def) 2835 apply (rule hoare_lift_Pf2 [where f=caps_of_state]) 2836 prefer 2 2837 apply wp 2838 apply (simp add: set_pd_def set_object_def) 2839 apply (wp get_object_wp) 2840 apply (clarsimp simp del: fun_upd_apply del: disjCI 2841 split: kernel_object.splits arch_kernel_obj.splits) 2842 apply (erule allE)+ 2843 apply (erule impE) 2844 apply (erule vs_lookup_pages_stateI) 2845 apply (clarsimp simp: obj_at_def split: if_split_asm) 2846 apply simp 2847 apply simp 2848 done 2849 2850 2851lemma unique_table_caps_pdE: 2852 "\<lbrakk> unique_table_caps cs; cs p = Some cap; cap_asid cap = None; 2853 cs p' = Some cap'; cap_asid cap' = Some v; is_pd_cap cap; 2854 is_pd_cap cap'; obj_refs cap' = obj_refs cap \<rbrakk> 2855 \<Longrightarrow> P" 2856 apply (frule(6) unique_table_caps_pdD[where cs=cs]) 2857 apply simp 2858 done 2859 2860lemma set_pd_table_caps [wp]: 2861 "\<lbrace>valid_table_caps and (\<lambda>s. 2862 (obj_at (empty_table {}) p s \<longrightarrow> 2863 empty_table {} (ArchObj (PageDirectory pd))) \<or> 2864 (\<exists>slot cap. caps_of_state s slot = Some cap \<and> is_pd_cap cap \<and> p \<in> obj_refs cap \<and> cap_asid cap \<noteq> None) \<and> 2865 valid_caps (caps_of_state s) s \<and> 2866 unique_table_caps (caps_of_state s))\<rbrace> 2867 set_pd p pd 2868 \<lbrace>\<lambda>_. valid_table_caps\<rbrace>" 2869 unfolding valid_table_caps_def 2870 apply (simp add: pred_conj_def 2871 del: split_paired_All split_paired_Ex imp_disjL cap_asid_simps) 2872 apply (rule hoare_lift_Pf2 [where f=caps_of_state]) 2873 prefer 2 2874 apply wp 2875 apply (unfold set_pd_def set_object_def) 2876 apply (wp get_object_wp) 2877 apply (rule allI, intro impI) 2878 apply (elim exE conjE) 2879 apply (elim allEI) 2880 apply (intro impI, simp del: cap_asid_simps) 2881 apply (clarsimp simp: obj_at_def simp del: cap_asid_simps) 2882 apply (clarsimp split: kernel_object.splits arch_kernel_obj.splits simp del: cap_asid_simps) 2883 apply (erule disjE) 2884 apply (erule(6) unique_table_caps_pdE) 2885 apply (clarsimp simp: is_arch_cap_simps) 2886 apply (simp add: valid_caps_def) 2887 apply (erule_tac x=a in allE, erule allE, erule allE, erule (1) impE) 2888 apply (clarsimp simp: is_arch_cap_simps valid_cap_def obj_at_def) 2889done 2890 2891lemma eq_ucast_word11[simp]: 2892 "((ucast (x :: 11 word) :: word32) = ucast y) = (x = y)" 2893 apply safe 2894 apply (drule_tac f="ucast :: (word32 \<Rightarrow> 11 word)" in arg_cong) 2895 apply (simp add: ucast_up_ucast_id is_up_def 2896 source_size_def target_size_def word_size) 2897 done 2898 2899 2900 2901lemma set_pd_unmap_mappings: 2902 "\<lbrace>valid_kernel_mappings and 2903 obj_at (\<lambda>ko. vs_refs (ArchObj (PageDirectory pd)) \<subseteq> vs_refs ko) p\<rbrace> 2904 set_pd p pd 2905 \<lbrace>\<lambda>rv. valid_kernel_mappings\<rbrace>" 2906 apply (simp add: set_pd_def) 2907 apply (wp set_object_v_ker_map get_object_wp) 2908 apply (clarsimp simp: obj_at_def 2909 split: kernel_object.split_asm 2910 arch_kernel_obj.split_asm) 2911 done 2912 2913 2914lemma set_pd_asid_map [wp]: 2915 "\<lbrace>valid_asid_map\<rbrace> set_pd p pd \<lbrace>\<lambda>_. valid_asid_map\<rbrace>" 2916 apply (simp add: set_pd_def set_object_def) 2917 apply (wp get_object_wp) 2918 apply (clarsimp simp del: fun_upd_apply 2919 split: kernel_object.splits 2920 arch_kernel_obj.splits) 2921 apply (clarsimp simp: valid_asid_map_def) 2922 apply (drule bspec, blast) 2923 apply (clarsimp simp: vspace_at_asid_def obj_at_def) 2924 apply (erule vs_lookupE) 2925 apply (rule vs_lookupI, simp) 2926 apply (clarsimp simp: vs_asid_refs_def dest!: graph_ofD) 2927 apply (frule vs_lookup1_trans_is_append) 2928 apply clarsimp 2929 apply (drule rtranclD) 2930 apply clarsimp 2931 apply (drule tranclD) 2932 apply clarsimp 2933 apply (drule vs_lookup1D) 2934 apply clarsimp 2935 apply (rule rtrancl_trans) 2936 apply (rule r_into_rtrancl) 2937 apply (rule vs_lookup1I) 2938 apply (clarsimp simp: obj_at_def) 2939 apply (rule conjI, clarsimp) 2940 prefer 2 2941 apply clarsimp 2942 apply (rule refl) 2943 apply clarsimp 2944 apply (clarsimp simp: vs_refs_def) 2945 apply (drule vs_lookup1_trans_is_append) 2946 apply clarsimp 2947 apply assumption 2948 apply (rule refl) 2949 apply (frule vs_lookup1_trans_is_append, clarsimp) 2950 apply (drule rtranclD) 2951 apply (erule disjE, clarsimp) 2952 apply clarsimp 2953 apply (drule tranclD) 2954 apply clarsimp 2955 apply (drule vs_lookup1D) 2956 apply clarsimp 2957 apply (drule vs_lookup1_trans_is_append, clarsimp) 2958 done 2959 2960 2961lemma set_pd_only_idle [wp]: 2962 "\<lbrace>only_idle\<rbrace> set_pd p pd \<lbrace>\<lambda>_. only_idle\<rbrace>" 2963 by (wp only_idle_lift) 2964 2965 2966lemma set_pd_equal_kernel_mappings_triv: 2967 "\<lbrace> equal_kernel_mappings\<rbrace> 2968 set_pd p pd 2969 \<lbrace>\<lambda>rv. equal_kernel_mappings\<rbrace>" 2970 apply (simp add: equal_kernel_mappings_def valid_def) 2971done (* do we need this? *) 2972 2973lemma set_pd_kernel_window[wp]: 2974 "\<lbrace>pspace_in_kernel_window\<rbrace> set_pd p pd \<lbrace>\<lambda>rv. pspace_in_kernel_window\<rbrace>" 2975 apply (simp add: set_pd_def) 2976 apply (wp set_object_pspace_in_kernel_window get_object_wp) 2977 apply (clarsimp simp: obj_at_def a_type_def 2978 split: kernel_object.split_asm 2979 arch_kernel_obj.split_asm) 2980 done 2981 2982lemma set_pd_device_region[wp]: 2983 "\<lbrace>pspace_respects_device_region\<rbrace> set_pd p pd \<lbrace>\<lambda>rv. pspace_respects_device_region\<rbrace>" 2984 apply (simp add: set_pd_def) 2985 apply (wp set_object_pspace_respects_device_region get_object_wp) 2986 apply (clarsimp simp: obj_at_def a_type_def 2987 split: Structures_A.kernel_object.split_asm 2988 arch_kernel_obj.split_asm) 2989 done 2990 2991 2992lemma set_pd_caps_kernel_window[wp]: 2993 "\<lbrace>cap_refs_in_kernel_window\<rbrace> set_pd p pd \<lbrace>\<lambda>rv. cap_refs_in_kernel_window\<rbrace>" 2994 apply (simp add: set_pd_def) 2995 apply (wp set_object_cap_refs_in_kernel_window get_object_wp) 2996 apply (clarsimp simp: obj_at_def a_type_def 2997 split: kernel_object.split_asm 2998 arch_kernel_obj.split_asm) 2999 done 3000 3001lemma set_pd_caps_respects_device_region[wp]: 3002 "\<lbrace>cap_refs_respects_device_region\<rbrace> set_pd p pd \<lbrace>\<lambda>rv. cap_refs_respects_device_region\<rbrace>" 3003 apply (simp add: set_pd_def) 3004 apply (wp set_object_cap_refs_respects_device_region get_object_wp) 3005 apply (clarsimp simp: obj_at_def a_type_def 3006 split: Structures_A.kernel_object.split_asm 3007 arch_kernel_obj.split_asm) 3008 done 3009 3010 3011lemma set_pd_valid_ioc[wp]: 3012 "\<lbrace>valid_ioc\<rbrace> set_pd p pt \<lbrace>\<lambda>_. valid_ioc\<rbrace>" 3013 apply (simp add: set_pd_def) 3014 apply (wp set_object_valid_ioc_no_caps get_object_inv) 3015 by (clarsimp simp: valid_def get_object_def simpler_gets_def assert_def 3016 return_def fail_def bind_def 3017 a_type_simps obj_at_def is_tcb is_cap_table 3018 split: kernel_object.splits arch_kernel_obj.splits) 3019 3020 3021lemma set_pd_vms[wp]: 3022 "\<lbrace>valid_machine_state\<rbrace> set_pd p pt \<lbrace>\<lambda>_. valid_machine_state\<rbrace>" 3023 apply (simp add: set_pd_def set_object_def) 3024 apply (wp get_object_wp) 3025 apply clarify 3026 apply (erule valid_machine_state_heap_updI) 3027 apply (fastforce simp: a_type_def obj_at_def 3028 split: Structures_A.kernel_object.splits arch_kernel_obj.splits)+ 3029 done 3030 3031 3032(* FIXME: Move to Invariants_A *) 3033lemma vs_refs_pages_subset: "vs_refs ko \<subseteq> vs_refs_pages ko" 3034 apply (clarsimp simp: vs_refs_pages_def vs_refs_def graph_of_def 3035 split: kernel_object.splits arch_kernel_obj.splits pde.splits) 3036 subgoal for "fun" a b 3037 using 3038 imageI[where A="{(x, y). (pde_ref_pages (fun x)) = Some y}" 3039 and f="(\<lambda>(r, y). (VSRef (ucast r) (Some APageDirectory), y))" and x="(a,b)"] 3040 by (clarsimp simp: pde_ref_def pde_ref_pages_def split: pde.splits) 3041 done 3042 3043lemma vs_refs_pages_subset2: 3044 "\<lbrakk>vs_refs_pages ko \<subseteq> vs_refs_pages ko'; 3045 (\<forall>ao. (ko = ArchObj ao) \<longrightarrow> valid_vspace_obj ao s); 3046 (\<forall>ao'. (ko' = ArchObj ao') \<longrightarrow> valid_vspace_obj ao' s)\<rbrakk> 3047 \<Longrightarrow> vs_refs ko \<subseteq> vs_refs ko'" 3048 apply clarsimp 3049 apply (drule (1) subsetD[OF _ subsetD[OF vs_refs_pages_subset]]) 3050 3051 apply (case_tac ko; simp add: vs_refs_def) 3052 subgoal for fstref b arch_kernel_obj 3053 apply (cases arch_kernel_obj; simp add: vs_refs_def) 3054 apply (cases ko'; simp add: vs_refs_pages_def) 3055 subgoal for \<dots> arch_kernel_obja 3056 by (cases arch_kernel_obja;clarsimp) 3057 apply (cases ko'; simp add: vs_refs_pages_def) 3058 subgoal for \<dots> arch_kernel_obja 3059 apply (cases arch_kernel_obja; clarsimp) 3060 apply (clarsimp simp: graph_of_def split: if_splits) 3061 subgoal for "fun" a 3062 apply (cut_tac 3063 imageI[where 3064 A="{(x, y). (pde_ref (fun x)) = Some y}" 3065 and f="(\<lambda>(r, y). (VSRef (ucast r) (Some APageDirectory), y))" and x="(a,b)"]) 3066 apply simp 3067 apply (clarsimp simp: pde_ref_def pde_ref_pages_def 3068 split: pde.splits) 3069 apply (drule_tac x=a in spec)+ 3070 apply (simp add: valid_pde_def) 3071 apply (clarsimp simp: data_at_def obj_at_def a_type_def) 3072 apply (drule_tac x=a in spec, simp split: if_splits)+ 3073 by (clarsimp simp: obj_at_def a_type_def data_at_def) 3074 done 3075done 3076done 3077 3078 3079lemma set_pd_global_objs[wp]: 3080 "\<lbrace>valid_global_objs and valid_global_refs and 3081 valid_arch_state\<rbrace> 3082 set_pd p pd \<lbrace>\<lambda>rv. valid_global_objs\<rbrace>" 3083 apply (simp add: set_pd_def set_object_def) 3084 apply (wp get_object_wp) 3085 apply (clarsimp simp del: fun_upd_apply 3086 split: kernel_object.splits arch_kernel_obj.splits) 3087 apply (clarsimp simp add: valid_global_objs_def valid_vso_at_def 3088 cte_wp_at_caps_of_state) 3089 done 3090 3091 3092lemma set_pd_global_mappings[wp]: 3093 "\<lbrace>\<lambda>s. valid_global_vspace_mappings s \<and> valid_global_objs s 3094 \<and> p \<notin> global_refs s\<rbrace> 3095 set_pd p pd 3096 \<lbrace>\<lambda>rv. valid_global_vspace_mappings\<rbrace>" 3097 apply (wpsimp simp: valid_global_vspace_mappings_def) 3098 done 3099 3100 3101lemma set_pd_invs_unmap: (* ARMHYP *) 3102 "\<lbrace>invs and (\<lambda>s. \<forall>i. wellformed_pde (pd i)) and 3103 (\<lambda>s. (\<exists>\<rhd>p) s \<longrightarrow> valid_vspace_obj (PageDirectory pd) s) and 3104 obj_at (\<lambda>ko. vs_refs_pages (ArchObj (PageDirectory pd)) \<subseteq> vs_refs_pages ko) p and 3105 obj_at (\<lambda>ko. vs_refs (ArchObj (PageDirectory pd)) \<subseteq> vs_refs ko) p and 3106(* obj_at (\<lambda>ko. \<exists>pd'. ko = ArchObj (PageDirectory pd') 3107 \<and> (\<forall>x \<in> kernel_mapping_slots. pd x = pd' x)) p and *) 3108 (\<lambda>s. p \<notin> global_refs s) and 3109 (\<lambda>s. (obj_at (empty_table {}) p s \<longrightarrow> 3110 empty_table {} (ArchObj (PageDirectory pd))))\<rbrace> 3111 set_pd p pd 3112 \<lbrace>\<lambda>_. invs\<rbrace>" 3113 apply (simp add: invs_def valid_state_def valid_pspace_def valid_arch_caps_def) 3114 apply (rule hoare_pre) 3115 apply (wp set_pd_valid_objs set_pd_iflive set_pd_zombies 3116 set_pd_zombies_state_refs set_pd_zombies_state_hyp_refs set_pd_valid_mdb 3117 set_pd_valid_idle set_pd_ifunsafe set_pd_reply_caps 3118 set_pd_valid_arch set_pd_valid_global set_pd_cur 3119 set_pd_reply_masters valid_irq_node_typ 3120 set_pd_vspace_objs_unmap set_pd_vs_lookup_unmap 3121 valid_irq_handlers_lift 3122 set_pd_unmap_mappings set_pd_equal_kernel_mappings_triv) 3123 apply (clarsimp simp: cte_wp_at_caps_of_state valid_arch_caps_def 3124 del: disjCI) 3125done 3126 3127 3128lemma store_pde_invs_unmap: 3129 "\<lbrace>invs and valid_pde pde and (\<lambda>s. wellformed_pde pde) 3130 and (\<lambda>s. p && ~~ mask pd_bits \<notin> global_refs s) 3131 and K (pde = InvalidPDE)\<rbrace> 3132 store_pde p pde \<lbrace>\<lambda>_. invs\<rbrace>" 3133 apply (simp add: store_pde_def del: split_paired_Ex) 3134 apply (wp set_pd_invs_unmap) 3135 apply (clarsimp simp del: split_paired_Ex del: exE) 3136 apply (rule conjI) 3137 apply (drule invs_valid_objs) 3138 apply (fastforce simp: valid_objs_def dom_def obj_at_def valid_obj_def) 3139 apply (rule conjI) 3140 apply (clarsimp) 3141 apply (drule (1) valid_vspace_objsD, fastforce) 3142 apply simp 3143 apply (rule conjI) 3144 apply (clarsimp intro!: pair_imageI 3145 simp: obj_at_def vs_refs_def vs_refs_pages_def map_conv_upd 3146 graph_of_def pde_ref_pages_def 3147 split: if_split_asm pde.splits)+ 3148 apply (clarsimp simp: pde_ref_def valid_pde_mappings_def empty_table_def 3149 split:if_split_asm) 3150 apply fastforce 3151done 3152 3153 3154lemma store_pde_state_refs_of: 3155 "\<lbrace>\<lambda>s. P (state_refs_of s)\<rbrace> store_pde ptr val \<lbrace>\<lambda>rv s. P (state_refs_of s)\<rbrace>" 3156 apply (simp add: store_pde_def set_pd_def set_object_def) 3157 apply (wp get_object_wp) 3158 apply (clarsimp elim!: rsubst[where P=P] intro!: ext) 3159 apply (clarsimp simp: state_refs_of_def obj_at_def) 3160 done 3161 3162lemma store_pde_state_hyp_refs_of: 3163 "\<lbrace>\<lambda>s. P (state_hyp_refs_of s)\<rbrace> store_pde ptr val \<lbrace>\<lambda>rv s. P (state_hyp_refs_of s)\<rbrace>" 3164 apply (simp add: store_pde_def set_pd_def set_object_def) 3165 apply (wp get_object_wp) 3166 apply (clarsimp elim!: rsubst[where P=P] intro!: ext) 3167 apply (clarsimp simp: state_hyp_refs_of_def obj_at_def) 3168 done 3169 3170lemma valid_asid_map_next_asid [iff]: 3171 "valid_asid_map (s\<lparr>arch_state := arm_next_asid_update f (arch_state s)\<rparr>) = 3172 valid_asid_map s" 3173 by (simp add: valid_asid_map_def vspace_at_asid_def) 3174 3175 3176lemma pspace_respects_device_region_dmo: 3177 assumes valid_f: "\<And>P. \<lbrace>\<lambda>ms. P (device_state ms)\<rbrace> f \<lbrace>\<lambda>r ms. P (device_state ms)\<rbrace>" 3178 shows "\<lbrace>pspace_respects_device_region\<rbrace>do_machine_op f\<lbrace>\<lambda>r. pspace_respects_device_region\<rbrace>" 3179 apply (clarsimp simp: do_machine_op_def gets_def select_f_def simpler_modify_def bind_def valid_def 3180 get_def return_def) 3181 apply (drule_tac P1 = "(=) (device_state (machine_state s))" in use_valid[OF _ valid_f]) 3182 apply auto 3183 done 3184 3185lemma cap_refs_respects_device_region_dmo: 3186 assumes valid_f: "\<And>P. \<lbrace>\<lambda>ms. P (device_state ms)\<rbrace> f \<lbrace>\<lambda>r ms. P (device_state ms)\<rbrace>" 3187 shows "\<lbrace>cap_refs_respects_device_region\<rbrace>do_machine_op f\<lbrace>\<lambda>r. cap_refs_respects_device_region\<rbrace>" 3188 apply (clarsimp simp: do_machine_op_def gets_def select_f_def simpler_modify_def bind_def valid_def 3189 get_def return_def) 3190 apply (drule_tac P1 = "(=) (device_state (machine_state s))" in use_valid[OF _ valid_f]) 3191 apply auto 3192 done 3193 3194lemma machine_op_lift_device_state[wp]: 3195 "\<lbrace>\<lambda>ms. P (device_state ms)\<rbrace> machine_op_lift f \<lbrace>\<lambda>_ ms. P (device_state ms)\<rbrace>" 3196 by (clarsimp simp: machine_op_lift_def NonDetMonad.valid_def bind_def 3197 machine_rest_lift_def gets_def simpler_modify_def get_def return_def 3198 select_def ignore_failure_def select_f_def 3199 split: if_splits) 3200 3201crunch device_state_inv[wp]: invalidateLocalTLB_ASID "\<lambda>ms. P (device_state ms)" 3202crunch device_state_inv[wp]: invalidateLocalTLB_VAASID "\<lambda>ms. P (device_state ms)" 3203crunch device_state_inv[wp]: setHardwareASID "\<lambda>ms. P (device_state ms)" 3204crunch device_state_inv[wp]: isb "\<lambda>ms. P (device_state ms)" 3205crunch device_state_inv[wp]: dsb "\<lambda>ms. P (device_state ms)" 3206crunch device_state_inv[wp]: set_current_pd "\<lambda>ms. P (device_state ms)" 3207 (simp: setCurrentPDPL2_def) 3208crunch device_state_inv[wp]: storeWord "\<lambda>ms. P (device_state ms)" 3209crunch device_state_inv[wp]: cleanByVA_PoU "\<lambda>ms. P (device_state ms)" 3210crunch device_state_inv[wp]: cleanL2Range "\<lambda>ms. P (device_state ms)" 3211 3212lemma as_user_inv: 3213 assumes x: "\<And>P. \<lbrace>P\<rbrace> f \<lbrace>\<lambda>x. P\<rbrace>" 3214 shows "\<lbrace>P\<rbrace> as_user t f \<lbrace>\<lambda>x. P\<rbrace>" 3215proof - 3216 have P: "\<And>a b input. (a, b) \<in> fst (f input) \<Longrightarrow> b = input" 3217 by (rule use_valid [OF _ x], assumption, rule refl) 3218 have Q: "\<And>s ps. ps (kheap s) = kheap s \<Longrightarrow> kheap_update ps s = s" 3219 by simp 3220 show ?thesis 3221 apply (simp add: as_user_def gets_the_def assert_opt_def set_object_def split_def) 3222 apply wp 3223 apply (clarsimp dest!: P) 3224 apply (subst Q) 3225 prefer 2 3226 apply assumption 3227 apply (rule ext) 3228 apply (simp add: get_tcb_def) 3229 apply (case_tac "kheap s t"; simp) 3230 apply (case_tac a; simp) 3231 apply (clarsimp simp: arch_tcb_context_set_def arch_tcb_context_get_def) 3232 done 3233qed 3234 3235lemma user_getreg_inv[wp]: 3236 "\<lbrace>P\<rbrace> as_user t (getRegister r) \<lbrace>\<lambda>x. P\<rbrace>" 3237 apply (rule as_user_inv) 3238 apply (simp add: getRegister_def) 3239 done 3240 3241end 3242 3243end 3244