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(* 12 Lemmas on arch get/set object etc 13*) 14 15theory ArchAcc_R 16imports SubMonad_R 17begin 18 19(*FIXME move*) 20lemma hoare_add_post': 21 "\<lbrakk>\<lbrace>P'\<rbrace> f \<lbrace>Q'\<rbrace>; \<lbrace>P''\<rbrace> f \<lbrace>\<lambda>rv s. Q' rv s \<longrightarrow> Q rv s\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P' and P''\<rbrace> f \<lbrace>Q\<rbrace>" 22 by (fastforce simp add: valid_def) 23 24context begin 25 26lemma fun_all: "f = f' \<Longrightarrow> (\<forall>s. f s \<longrightarrow> f' s)" 27 by simp 28 29lemma distrib_imp: 30 "P \<longrightarrow> Q \<and> Q' \<Longrightarrow> ((P \<longrightarrow> Q) \<Longrightarrow> (P \<longrightarrow> Q') \<Longrightarrow> R) \<Longrightarrow> R" 31 by simp 32 33method def_to_elim = (drule meta_eq_to_obj_eq, drule fun_all, elim allE, elim distrib_imp) 34method simp_to_elim = (drule fun_all, elim allE impE) 35 36end 37 38context Arch begin global_naming ARM_A (*FIXME: arch_split*) 39 40lemma asid_pool_at_ko: 41 "asid_pool_at p s \<Longrightarrow> \<exists>pool. ko_at (ArchObj (ARM_A.ASIDPool pool)) p s" 42 apply (clarsimp simp: obj_at_def a_type_def) 43 apply (case_tac ko, simp_all split: if_split_asm) 44 apply (rename_tac arch_kernel_obj) 45 apply (case_tac arch_kernel_obj, auto split: if_split_asm) 46 done 47 48declare valid_arch_state_def[@def_to_elim, conjuncts] 49 50lemmas valid_arch_state_elims[rule_format, elim!] = conjuncts 51 52lemmas valid_vspace_obj_elims [rule_format, elim!] = 53 valid_vspace_obj.simps[@simp_to_elim, @ \<open>(drule bspec)?\<close>] 54 55end 56 57context begin interpretation Arch . (*FIXME: arch_split*) 58 59(*FIXME move *) 60 61lemma pspace_relation_None: 62 "\<lbrakk>pspace_relation p p'; p' ptr = None \<rbrakk> \<Longrightarrow> p ptr = None" 63 apply (rule not_Some_eq[THEN iffD1, OF allI, OF notI]) 64 apply (drule(1) pspace_relation_absD) 65 apply (case_tac y; clarsimp simp: cte_map_def of_bl_def well_formed_cnode_n_def split: if_splits) 66 subgoal for n 67 apply (drule spec[of _ ptr]) 68 apply (drule spec) 69 apply clarsimp 70 apply (drule spec[of _ "replicate n False"]) 71 apply (drule mp[OF _ refl]) 72 apply (drule mp) 73 subgoal premises by (induct n; simp) 74 apply clarsimp 75 done 76 subgoal for x 77 apply (cases x; clarsimp) 78 apply ((drule spec[of _ 0], fastforce)+)[2] 79 apply (drule spec[of _ ptr]) 80 apply (drule spec) 81 apply clarsimp 82 apply (drule mp[OF _ refl]) 83 apply (drule spec[of _ 0]) 84 subgoal for _ sz by (cases sz; simp add: pageBits_def) 85 done 86 done 87 88lemma no_0_obj'_abstract: 89 "(s, s') \<in> state_relation \<Longrightarrow> no_0_obj' s' \<Longrightarrow> kheap s 0 = None" 90 by (auto intro: pspace_relation_None simp add: no_0_obj'_def) 91 92declare if_cong[cong] 93 94lemma corres_gets_asid [corres]: 95 "corres (\<lambda>a c. a = c o ucast) \<top> \<top> (gets (arm_asid_table \<circ> arch_state)) (gets (armKSASIDTable \<circ> ksArchState))" 96 by (simp add: state_relation_def arch_state_relation_def) 97 98lemmas arm_asid_table_related = corres_gets_asid[simplified, rule_format] 99 100lemma asid_low_bits [simp]: 101 "asidLowBits = asid_low_bits" 102 by (simp add: asid_low_bits_def asidLowBits_def) 103 104lemma get_asid_pool_corres [corres]: 105 "p = p' \<Longrightarrow> corres (\<lambda>p p'. p = inv ASIDPool p' o ucast) 106 (asid_pool_at p) (asid_pool_at' p') 107 (get_asid_pool p) (getObject p')" 108 apply (simp add: getObject_def get_asid_pool_def get_object_def split_def) 109 apply (rule corres_no_failI) 110 apply (rule no_fail_pre, wp) 111 apply (clarsimp simp: typ_at'_def ko_wp_at'_def) 112 apply (case_tac ko; simp) 113 apply (rename_tac arch_kernel_object) 114 apply (case_tac arch_kernel_object, simp_all)[1] 115 apply (clarsimp simp: lookupAround2_known1 116 projectKOs) 117 apply (clarsimp simp: obj_at'_def projectKOs objBits_simps 118 archObjSize_def) 119 apply (erule (1) ps_clear_lookupAround2) 120 apply simp 121 apply (erule is_aligned_no_overflow) 122 apply simp 123 apply (clarsimp simp add: objBits_simps archObjSize_def 124 split: option.split) 125 apply (clarsimp simp: in_monad loadObject_default_def projectKOs) 126 apply (simp add: bind_assoc exec_gets) 127 apply (drule asid_pool_at_ko) 128 apply (clarsimp simp: obj_at_def) 129 apply (simp add: return_def) 130 apply (simp add: in_magnitude_check objBits_simps 131 archObjSize_def pageBits_def) 132 apply clarsimp 133 apply (clarsimp simp: state_relation_def pspace_relation_def) 134 apply (drule bspec, blast) 135 apply (clarsimp simp: other_obj_relation_def asid_pool_relation_def) 136 done 137 138lemma aligned_distinct_obj_atI': 139 "\<lbrakk> ksPSpace s x = Some ko; pspace_aligned' s; 140 pspace_distinct' s; ko = injectKO v \<rbrakk> 141 \<Longrightarrow> ko_at' v x s" 142 apply (simp add: obj_at'_def projectKOs project_inject 143 pspace_distinct'_def pspace_aligned'_def) 144 apply (drule bspec, erule domI)+ 145 apply simp 146 done 147 148lemmas aligned_distinct_asid_pool_atI' 149 = aligned_distinct_obj_atI'[where 'a=asidpool, 150 simplified, OF _ _ _ refl] 151 152lemma aligned_distinct_relation_asid_pool_atI'[elim]: 153 "\<lbrakk> asid_pool_at p s; pspace_relation (kheap s) (ksPSpace s'); 154 pspace_aligned' s'; pspace_distinct' s' \<rbrakk> 155 \<Longrightarrow> asid_pool_at' p s'" 156 apply (drule asid_pool_at_ko) 157 apply (clarsimp simp add: obj_at_def) 158 apply (drule(1) pspace_relation_absD) 159 apply (clarsimp simp: other_obj_relation_def) 160 apply (simp split: Structures_H.kernel_object.split_asm 161 arch_kernel_object.split_asm) 162 apply (drule(2) aligned_distinct_asid_pool_atI') 163 apply (clarsimp simp: obj_at'_def typ_at'_def ko_wp_at'_def 164 projectKOs) 165 done 166 167lemma get_asid_pool_corres': 168 "corres (\<lambda>p p'. p = inv ASIDPool p' o ucast) 169 (asid_pool_at p) (pspace_aligned' and pspace_distinct') 170 (get_asid_pool p) (getObject p)" 171 apply (rule stronger_corres_guard_imp, 172 rule get_asid_pool_corres) 173 apply auto 174 done 175 176lemma storePDE_cte_wp_at'[wp]: 177 "\<lbrace>\<lambda>s. P (cte_wp_at' P' p s)\<rbrace> 178 storePDE ptr val 179 \<lbrace>\<lambda>rv s. P (cte_wp_at' P' p s)\<rbrace>" 180 apply (simp add: storePDE_def) 181 apply (wp setObject_cte_wp_at2'[where Q="\<top>"]) 182 apply (clarsimp simp: updateObject_default_def in_monad 183 projectKO_opts_defs projectKOs) 184 apply (rule equals0I) 185 apply (clarsimp simp: updateObject_default_def in_monad 186 projectKOs projectKO_opts_defs) 187 apply simp 188 done 189 190lemma storePDE_state_refs_of[wp]: 191 "\<lbrace>\<lambda>s. P (state_refs_of' s)\<rbrace> 192 storePDE ptr val 193 \<lbrace>\<lambda>rv s. P (state_refs_of' s)\<rbrace>" 194 unfolding storePDE_def 195 by (wp setObject_state_refs_of_eq; clarsimp simp: updateObject_default_def in_monad projectKOs) 196 197lemma storePTE_cte_wp_at'[wp]: 198 "\<lbrace>\<lambda>s. P (cte_wp_at' P' p s)\<rbrace> 199 storePTE ptr val 200 \<lbrace>\<lambda>rv s. P (cte_wp_at' P' p s)\<rbrace>" 201 apply (simp add: storePTE_def) 202 apply (wp setObject_cte_wp_at2'[where Q="\<top>"]) 203 apply (clarsimp simp: updateObject_default_def in_monad 204 projectKO_opts_defs projectKOs) 205 apply (rule equals0I) 206 apply (clarsimp simp: updateObject_default_def in_monad 207 projectKOs projectKO_opts_defs) 208 apply simp 209 done 210 211lemma storePTE_state_refs_of[wp]: 212 "\<lbrace>\<lambda>s. P (state_refs_of' s)\<rbrace> 213 storePTE ptr val 214 \<lbrace>\<lambda>rv s. P (state_refs_of' s)\<rbrace>" 215 unfolding storePTE_def 216 apply (wp setObject_state_refs_of_eq; 217 clarsimp simp: updateObject_default_def in_monad 218 projectKOs) 219 done 220 221crunch cte_wp_at'[wp]: setIRQState "\<lambda>s. P (cte_wp_at' P' p s)" 222crunch inv[wp]: getIRQSlot "P" 223 224lemma set_asid_pool_corres [corres]: 225 "p = p' \<Longrightarrow> a = inv ASIDPool a' o ucast \<Longrightarrow> 226 corres dc (asid_pool_at p and valid_etcbs) (asid_pool_at' p') 227 (set_asid_pool p a) (setObject p' a')" 228 apply (simp add: set_asid_pool_def) 229 apply (corressimp search: set_other_obj_corres[where P="\<lambda>_. True"] 230 wp: get_object_ret get_object_wp) 231 apply (simp add: other_obj_relation_def asid_pool_relation_def) 232 apply (clarsimp simp: obj_at_simps ) 233 by (auto simp: obj_at_simps typ_at_to_obj_at_arches 234 split: Structures_A.kernel_object.splits if_splits arch_kernel_obj.splits) 235 236lemma set_asid_pool_corres': 237 "a = inv ASIDPool a' o ucast \<Longrightarrow> 238 corres dc (asid_pool_at p and valid_etcbs) (pspace_aligned' and pspace_distinct') 239 (set_asid_pool p a) (setObject p a')" 240 apply (rule stronger_corres_guard_imp[OF set_asid_pool_corres]) 241 apply auto 242 done 243 244 245lemma pde_relation_aligned_simp: 246 "pde_relation_aligned (ucast (p && mask pd_bits >> 2)::12 word) pde pde' 247 = pde_relation_aligned ((p::word32) >> 2) pde pde'" 248 by (clarsimp simp: pde_relation_aligned_def 249 split: ARM_H.pde.splits if_splits) 250 251lemma get_pde_corres [corres]: 252 "p = p' \<Longrightarrow> corres (pde_relation_aligned (p >> 2)) (pde_at p) (pde_at' p') 253 (get_pde p) (getObject p')" 254 apply (simp add: getObject_def get_pde_def get_pd_def get_object_def split_def bind_assoc) 255 apply (rule corres_no_failI) 256 apply (rule no_fail_pre, wp) 257 apply (clarsimp simp: ko_wp_at'_def typ_at'_def lookupAround2_known1) 258 apply (case_tac ko; simp) 259 apply (rename_tac arch_kernel_object) 260 apply (case_tac arch_kernel_object; simp add: projectKOs) 261 apply (clarsimp simp: objBits_def cong: option.case_cong) 262 apply (erule (1) ps_clear_lookupAround2) 263 apply simp 264 apply (erule is_aligned_no_overflow) 265 apply (simp add: objBits_simps archObjSize_def word_bits_def) 266 apply simp 267 apply (clarsimp simp: in_monad loadObject_default_def projectKOs) 268 apply (simp add: bind_assoc exec_gets) 269 apply (clarsimp simp: pde_at_def obj_at_def) 270 apply (clarsimp simp add: a_type_def return_def 271 split: if_split_asm Structures_A.kernel_object.splits arch_kernel_obj.splits) 272 apply (clarsimp simp: typ_at'_def ko_wp_at'_def) 273 apply (simp add: in_magnitude_check objBits_simps archObjSize_def pageBits_def pdeBits_def) 274 apply (clarsimp simp: bind_def) 275 apply (clarsimp simp: state_relation_def pspace_relation_def) 276 apply (drule bspec, blast) 277 apply (clarsimp simp: other_obj_relation_def pde_relation_def) 278 apply (erule_tac x="(ucast (p && mask pd_bits >> 2))" in allE) 279 apply (clarsimp simp: mask_pd_bits_inner_beauty) 280 apply (clarsimp simp: obj_at_def pde_relation_aligned_simp) 281 done 282 283lemmas aligned_distinct_pde_atI' 284 = aligned_distinct_obj_atI'[where 'a=pde, 285 simplified, OF _ _ _ refl] 286 287lemma aligned_distinct_relation_pde_atI'[elim]: 288 "\<lbrakk> pde_at p s; pspace_relation (kheap s) (ksPSpace s'); 289 pspace_aligned' s'; pspace_distinct' s' \<rbrakk> 290 \<Longrightarrow> pde_at' p s'" 291 apply (clarsimp simp add: pde_at_def obj_at_def a_type_def) 292 apply (simp split: Structures_A.kernel_object.split_asm 293 if_split_asm arch_kernel_obj.split_asm) 294 apply (drule(1) pspace_relation_absD) 295 apply (clarsimp simp: other_obj_relation_def) 296 apply (drule_tac x="ucast ((p && mask pd_bits) >> 2)" 297 in spec) 298 apply (subst(asm) ucast_ucast_len) 299 apply (rule shiftr_less_t2n) 300 apply (rule less_le_trans, rule and_mask_less_size) 301 apply (simp add: word_size pd_bits_def pageBits_def) 302 apply (simp add: pd_bits_def pageBits_def) 303 apply (simp add: shiftr_shiftl1) 304 apply (subst(asm) is_aligned_neg_mask_eq[where n=2]) 305 apply (erule is_aligned_andI1) 306 apply (subst(asm) add.commute, 307 subst(asm) word_plus_and_or_coroll2) 308 apply (clarsimp simp: pde_relation_def) 309 apply (drule(2) aligned_distinct_pde_atI') 310 apply (clarsimp simp: obj_at'_def typ_at'_def ko_wp_at'_def 311 projectKOs) 312 done 313 314lemma pde_relation_alignedD: 315 "\<lbrakk> kheap s (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); 316 pspace_relation (kheap s) (ksPSpace s'); 317 ksPSpace s' ((p && ~~ mask pd_bits) + (ucast x << 2)) = Some (KOArch (KOPDE pde))\<rbrakk> 318 \<Longrightarrow> pde_relation_aligned x (pd x) pde" 319 apply (clarsimp simp:pspace_relation_def) 320 apply (drule bspec,blast) 321 apply (clarsimp simp:pde_relation_def) 322 apply (drule_tac x = x in spec) 323 apply (clarsimp simp:pde_relation_aligned_def 324 split:ARM_H.pde.splits) 325 done 326 327lemma pde_at_ksPSpace_not_None: 328 "\<lbrakk>kheap (a::('a ::state_ext) state) (p && ~~ mask pd_bits) = Some (ArchObj (PageDirectory pd)); 329 pd (ucast ((p && ~~ mask 6) && mask pd_bits >> 2)) = pde; 330 pspace_relation (kheap a) (ksPSpace (b::kernel_state)); 331 pspace_aligned' b;pspace_distinct' b\<rbrakk> 332 \<Longrightarrow> ksPSpace b ((p && ~~ mask 6)::word32) \<noteq> None" 333 apply (drule aligned_distinct_relation_pde_atI'[rotated,where p = "p && ~~ mask 6"]) 334 apply simp+ 335 apply (simp add:pde_at_def obj_at_def) 336 apply (intro conjI exI) 337 apply (simp add:pd_bits_def pageBits_def 338 and_not_mask_twice) 339 apply (simp add:a_type_simps) 340 apply (rule is_aligned_weaken) 341 apply (rule is_aligned_neg_mask[OF le_refl]) 342 apply (simp add:is_aligned_andI1) 343 apply (clarsimp simp:typ_at'_def ko_wp_at'_def) 344 done 345 346lemma get_master_pde_corres [@lift_corres_args, corres]: 347 "corres pde_relation' (pde_at p) 348 (pde_at' p and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and 349 pspace_aligned' and pspace_distinct') 350 (get_master_pde p) (getObject p)" 351 proof - 352 have [simp]: "max pd_bits 6 = pd_bits" 353 by (simp add:pd_bits_def pageBits_def) 354 have expand: "p && ~~ mask pd_bits = (p && ~~ mask 6) && ~~ mask pd_bits" 355 by (simp add: and_not_mask_twice) 356 have [simp]: "is_aligned (p && ~~ mask 6 >> 2) 4" 357 apply (rule is_aligned_shiftr) 358 apply (simp add:is_aligned_neg_mask) 359 done 360 show ?thesis 361 apply (simp add: getObject_def get_pde_def get_pd_def get_object_def 362 split_def bind_assoc pde_relation_aligned_def get_master_pde_def) 363 apply (rule corres_no_failI) 364 apply (rule no_fail_pre, wp) 365 apply (clarsimp simp: ko_wp_at'_def typ_at'_def lookupAround2_known1) 366 apply (case_tac ko, simp_all)[1] 367 apply (rename_tac arch_kernel_object) 368 apply (case_tac arch_kernel_object, simp_all add: projectKOs)[1] 369 apply (clarsimp simp: objBits_def cong: option.case_cong) 370 apply (erule (1) ps_clear_lookupAround2) 371 apply simp 372 apply (erule is_aligned_no_overflow) 373 apply (simp add: objBits_simps archObjSize_def word_bits_def) 374 apply simp 375 apply (clarsimp simp: in_monad loadObject_default_def 376 projectKOs and_not_mask_twice) 377 apply (simp add: bind_assoc exec_gets) 378 apply (clarsimp simp: pde_at_def obj_at_def) 379 apply (clarsimp split:ARM_A.pde.splits) 380 apply (intro conjI impI) 381 \<comment> \<open>master_pde = InvaliatePTE\<close> 382 apply (clarsimp simp add: a_type_def return_def get_pd_def 383 bind_def get_pde_def get_object_def gets_def get_def 384 split: if_split_asm Structures_A.kernel_object.splits arch_kernel_obj.splits) 385 apply (clarsimp simp:typ_at'_def ko_wp_at'_def) 386 apply (clarsimp simp: in_magnitude_check objBits_simps archObjSize_def pageBits_def pdeBits_def) 387 apply (clarsimp simp:state_relation_def) 388 apply (frule_tac x = "(ucast (p && mask pd_bits >> 2))" 389 in pde_relation_alignedD) 390 apply assumption 391 apply (simp add:mask_pd_bits_inner_beauty) 392 apply (clarsimp simp: pde_relation_aligned_def 393 split: if_splits ARM_H.pde.splits) 394 apply (drule_tac p' = "p && ~~ mask 6" in valid_duplicates'_D[rotated]) 395 apply (simp add:is_aligned_neg_mask is_aligned_weaken[where y = 2]) 396 apply (clarsimp simp: vs_ptr_align_def and_not_mask_twice) 397 apply simp 398 apply (frule_tac x = "(ucast ((p && ~~ mask 6) && mask pd_bits >> 2))" 399 in pde_relation_alignedD) 400 apply assumption 401 apply (simp add:expand) 402 apply (subst mask_pd_bits_inner_beauty) 403 apply (simp add:is_aligned_neg_mask) 404 apply assumption 405 apply (clarsimp simp: pde_relation_aligned_def 406 is_aligned_mask[where 'a=32, symmetric]) 407 408 \<comment> \<open>master_pde = PageTablePDE\<close> 409 apply (clarsimp simp add: a_type_def return_def get_pd_def 410 bind_def get_pde_def get_object_def gets_def get_def 411 split: if_split_asm Structures_A.kernel_object.splits arch_kernel_obj.splits) 412 apply (clarsimp simp:typ_at'_def ko_wp_at'_def) 413 apply (clarsimp simp: in_magnitude_check objBits_simps archObjSize_def pageBits_def pdeBits_def) 414 apply (clarsimp simp:state_relation_def) 415 apply (frule_tac x = "(ucast (p && mask pd_bits >> 2))" in pde_relation_alignedD) 416 apply assumption 417 apply (simp add:mask_pd_bits_inner_beauty) 418 apply (clarsimp simp:pde_relation_aligned_def 419 split:if_splits ARM_H.pde.splits) 420 apply (drule_tac p' = "p && ~~ mask 6" in valid_duplicates'_D[rotated]) 421 apply (simp add:is_aligned_neg_mask is_aligned_weaken[where y = 2]) 422 apply (clarsimp simp: vs_ptr_align_def) 423 apply (simp add:and_not_mask_twice) 424 apply (drule_tac x = "(ucast ((p && ~~ mask 6) && mask pd_bits >> 2))" in pde_relation_alignedD) 425 apply assumption 426 apply (simp add:expand) 427 apply (subst mask_pd_bits_inner_beauty) 428 apply (simp add:is_aligned_neg_mask) 429 apply assumption 430 apply (clarsimp simp:pde_relation_aligned_def 431 is_aligned_mask[symmetric]) 432 \<comment> \<open>master_pde = SectionPDE\<close> 433 apply (clarsimp simp add: a_type_def return_def get_pd_def 434 bind_def get_pde_def get_object_def gets_def get_def 435 split: if_split_asm Structures_A.kernel_object.splits arch_kernel_obj.splits) 436 apply (clarsimp simp:typ_at'_def ko_wp_at'_def) 437 apply (clarsimp simp: in_magnitude_check objBits_simps archObjSize_def pageBits_def pdeBits_def) 438 apply (clarsimp simp:state_relation_def) 439 apply (frule_tac x = "(ucast (p && mask pd_bits >> 2))" in pde_relation_alignedD) 440 apply assumption 441 apply (simp add:mask_pd_bits_inner_beauty) 442 apply (clarsimp simp:pde_relation_aligned_def 443 split:if_splits ARM_H.pde.splits) 444 apply (drule_tac p' = "p && ~~ mask 6" in valid_duplicates'_D[rotated]) 445 apply (simp add:is_aligned_neg_mask is_aligned_weaken[where y = 2]) 446 apply (clarsimp simp: vs_ptr_align_def) 447 apply (simp add:and_not_mask_twice) 448 apply (drule_tac x = "(ucast ((p && ~~ mask 6) && mask pd_bits >> 2))" in pde_relation_alignedD) 449 apply assumption 450 apply (simp add: expand) 451 apply (subst mask_pd_bits_inner_beauty) 452 apply (simp add:is_aligned_neg_mask) 453 apply assumption 454 apply (clarsimp simp:pde_relation_aligned_def 455 is_aligned_mask[symmetric]) 456 \<comment> \<open>master_pde = SuperSectionPDE\<close> 457 apply (clarsimp simp add: a_type_def return_def get_pd_def 458 bind_def get_pde_def get_object_def gets_def get_def 459 split: if_split_asm Structures_A.kernel_object.splits arch_kernel_obj.splits) 460 apply (clarsimp simp:typ_at'_def ko_wp_at'_def) 461 apply (clarsimp simp: in_magnitude_check objBits_simps archObjSize_def pageBits_def pdeBits_def) 462 apply (clarsimp simp:state_relation_def) 463 apply (drule_tac s = a and s' = b and p = "p && ~~ mask 6" 464 in aligned_distinct_relation_pde_atI'[rotated -1]) 465 apply (clarsimp simp:pde_at_def obj_at_def 466 and_not_mask_twice a_type_simps is_aligned_neg_mask) 467 apply simp 468 apply simp 469 apply (clarsimp simp:typ_at'_def ko_wp_at'_def) 470 apply (case_tac ko; simp) 471 apply (rename_tac arch_kernel_object) 472 apply (case_tac arch_kernel_object; simp add: projectKOs) 473 apply clarsimp 474 apply (frule_tac x = "(ucast ((p && ~~ mask 6 )&& mask pd_bits >> 2))" in pde_relation_alignedD) 475 apply assumption 476 apply (simp add: expand) 477 apply (subst mask_pd_bits_inner_beauty) 478 apply (simp add:is_aligned_neg_mask) 479 apply assumption 480 apply (rename_tac pde) 481 apply (case_tac pde) 482 apply (simp add: pde_relation_aligned_def 483 is_aligned_mask[where 'a=32, symmetric])+ 484 apply clarsimp 485 apply (drule_tac p = "p && ~~ mask 6" and p' = p in valid_duplicates'_D) 486 apply assumption 487 apply simp 488 apply (clarsimp simp: vs_ptr_align_def and_not_mask_twice) 489 apply simp 490 done 491 qed 492 493lemma get_pde_corres' : 494 "corres (pde_relation_aligned (p >> 2)) (pde_at p) 495 (pspace_aligned' and pspace_distinct') 496 (get_pde p) (getObject p)" 497 apply (rule stronger_corres_guard_imp, 498 rule get_pde_corres) 499 apply auto[1] 500 apply clarsimp 501 apply (rule aligned_distinct_relation_pde_atI') 502 apply (simp add:state_relation_def)+ 503 done 504 505lemma get_master_pde_corres': 506 "corres pde_relation' (pde_at p) 507 ((\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and 508 pspace_aligned' and pspace_distinct') 509 (get_master_pde p) (getObject p)" 510 apply (rule stronger_corres_guard_imp, 511 rule get_master_pde_corres) 512 apply auto 513 done 514 515 516lemma pte_relation_aligned_simp: 517 "pte_relation_aligned (ucast (p && mask pt_bits >> 2)::word8) pde pde' = 518 pte_relation_aligned ((p::word32) >> 2) pde pde'" 519 by (clarsimp simp: pte_relation_aligned_def 520 split: ARM_H.pte.splits if_splits) 521 522lemma get_pte_corres [corres]: 523 "p = p' \<Longrightarrow> corres (pte_relation_aligned (p >> 2)) (pte_at p) (pte_at' p') 524 (get_pte p) (getObject p')" 525 apply (simp add: getObject_def get_pte_def get_pt_def get_object_def split_def bind_assoc) 526 apply (rule corres_no_failI) 527 apply (rule no_fail_pre, wp) 528 apply (clarsimp simp: ko_wp_at'_def typ_at'_def lookupAround2_known1) 529 apply (case_tac ko, simp_all)[1] 530 apply (rename_tac arch_kernel_object) 531 apply (case_tac arch_kernel_object, simp_all add: projectKOs)[1] 532 apply (clarsimp simp: objBits_def cong: option.case_cong) 533 apply (erule (1) ps_clear_lookupAround2) 534 apply simp 535 apply (erule is_aligned_no_overflow) 536 apply (simp add: objBits_simps archObjSize_def word_bits_def) 537 apply simp 538 apply (clarsimp simp: in_monad loadObject_default_def projectKOs) 539 apply (simp add: bind_assoc exec_gets) 540 apply (clarsimp simp: obj_at_def pte_at_def) 541 apply (clarsimp simp add: a_type_def return_def 542 split: if_split_asm Structures_A.kernel_object.splits arch_kernel_obj.splits) 543 apply (clarsimp simp: typ_at'_def ko_wp_at'_def) 544 apply (simp add: in_magnitude_check objBits_simps archObjSize_def pageBits_def pteBits_def) 545 apply (clarsimp simp: bind_def) 546 apply (clarsimp simp: state_relation_def pspace_relation_def) 547 apply (drule bspec, blast) 548 apply (clarsimp simp: other_obj_relation_def pte_relation_def) 549 apply (erule_tac x="(ucast (p && mask pt_bits >> 2))" in allE) 550 apply (clarsimp simp: mask_pt_bits_inner_beauty 551 pte_relation_aligned_simp obj_at_def) 552 done 553 554lemma pte_relation_alignedD: 555 "\<lbrakk> kheap s (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pt)); 556 pspace_relation (kheap s) (ksPSpace s'); 557 ksPSpace s' ((p && ~~ mask pt_bits) + (ucast x << 2)) = Some (KOArch (KOPTE pte))\<rbrakk> 558 \<Longrightarrow> pte_relation_aligned x (pt x) pte" 559 apply (clarsimp simp:pspace_relation_def) 560 apply (drule bspec,blast) 561 apply (clarsimp simp:pte_relation_def) 562 apply (drule_tac x = x in spec) 563 apply clarsimp 564 done 565 566lemmas aligned_distinct_pte_atI' 567 = aligned_distinct_obj_atI'[where 'a=pte, 568 simplified, OF _ _ _ refl] 569 570lemma aligned_distinct_relation_pte_atI'[elim]: 571 "\<lbrakk> pte_at p s; pspace_relation (kheap s) (ksPSpace s'); 572 pspace_aligned' s'; pspace_distinct' s' \<rbrakk> 573 \<Longrightarrow> pte_at' p s'" 574 apply (clarsimp simp add: pte_at_def obj_at_def a_type_def) 575 apply (simp split: Structures_A.kernel_object.split_asm 576 if_split_asm arch_kernel_obj.split_asm) 577 apply (drule(1) pspace_relation_absD) 578 apply (clarsimp simp: other_obj_relation_def) 579 apply (drule_tac x="ucast ((p && mask pt_bits) >> 2)" 580 in spec) 581 apply (subst(asm) ucast_ucast_len) 582 apply (rule shiftr_less_t2n) 583 apply (rule less_le_trans, rule and_mask_less_size) 584 apply (simp add: word_size pt_bits_def pageBits_def) 585 apply (simp add: pt_bits_def pageBits_def) 586 apply (simp add: shiftr_shiftl1) 587 apply (subst(asm) is_aligned_neg_mask_eq[where n=2]) 588 apply (erule is_aligned_andI1) 589 apply (subst(asm) add.commute, 590 subst(asm) word_plus_and_or_coroll2) 591 apply (clarsimp simp: pte_relation_def) 592 apply (drule(2) aligned_distinct_pte_atI') 593 apply (clarsimp simp: obj_at'_def typ_at'_def ko_wp_at'_def 594 projectKOs) 595 done 596 597lemma pte_at_ksPSpace_not_None: 598 "\<lbrakk>kheap (a :: ('a ::state_ext) state) (p && ~~ mask pt_bits) = Some (ArchObj (PageTable pt)); 599 pt (ucast ((p && ~~ mask 6) && mask pt_bits >> 2)) = pte; 600 pspace_relation (kheap a) (ksPSpace (b::kernel_state)); 601 pspace_aligned' b;pspace_distinct' b\<rbrakk> 602 \<Longrightarrow> ksPSpace b ((p && ~~ mask 6)::word32) \<noteq> None" 603 apply (drule aligned_distinct_relation_pte_atI'[rotated,where p = "p && ~~ mask 6"]) 604 apply simp+ 605 apply (simp add:pte_at_def obj_at_def) 606 apply (intro conjI exI) 607 apply (simp add:pt_bits_def pageBits_def 608 and_not_mask_twice) 609 apply (simp add:a_type_simps) 610 apply (rule is_aligned_weaken) 611 apply (rule is_aligned_neg_mask[OF le_refl]) 612 apply (simp add:is_aligned_andI1) 613 apply (clarsimp simp:typ_at'_def ko_wp_at'_def) 614 done 615 616lemma get_master_pte_corres [@lift_corres_args, corres]: 617 "corres pte_relation' (pte_at p) 618 (pte_at' p and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and 619 pspace_aligned' and pspace_distinct') 620 (get_master_pte p) (getObject p)" 621 proof - 622 have [simp]: "max pt_bits 6 = pt_bits" 623 by (simp add:pd_bits_def pageBits_def pt_bits_def) 624 have expand: "p && ~~ mask pt_bits = (p && ~~ mask 6) && ~~ mask pt_bits" 625 by (simp add: and_not_mask_twice) 626 have [simp]: "is_aligned (p && ~~ mask 6 >> 2) 4" 627 apply (rule is_aligned_shiftr) 628 apply (simp add:is_aligned_neg_mask) 629 done 630 show ?thesis 631 apply (simp add: getObject_def get_pte_def get_pt_def get_object_def 632 split_def bind_assoc pte_relation_aligned_def get_master_pte_def) 633 apply (rule corres_no_failI) 634 apply (rule no_fail_pre, wp) 635 apply (clarsimp simp: ko_wp_at'_def typ_at'_def lookupAround2_known1) 636 apply (case_tac ko, simp_all)[1] 637 apply (rename_tac arch_kernel_object) 638 apply (case_tac arch_kernel_object, simp_all add: projectKOs)[1] 639 apply (clarsimp simp: objBits_def cong: option.case_cong) 640 apply (erule (1) ps_clear_lookupAround2) 641 apply simp 642 apply (erule is_aligned_no_overflow) 643 apply (simp add: objBits_simps archObjSize_def word_bits_def) 644 apply simp 645 apply (clarsimp simp: in_monad loadObject_default_def 646 projectKOs and_not_mask_twice) 647 apply (simp add: bind_assoc exec_gets) 648 apply (clarsimp simp: pte_at_def obj_at_def) 649 apply (clarsimp split:ARM_A.pte.splits) 650 apply (intro conjI impI) 651 \<comment> \<open>master_pde = InvaliatePTE\<close> 652 apply (clarsimp simp add: a_type_def return_def get_pt_def 653 bind_def get_pte_def get_object_def gets_def get_def 654 split: if_split_asm Structures_A.kernel_object.splits arch_kernel_obj.splits) 655 apply (clarsimp simp:typ_at'_def ko_wp_at'_def) 656 apply (clarsimp simp: in_magnitude_check objBits_simps archObjSize_def pageBits_def pteBits_def) 657 apply (clarsimp simp:state_relation_def) 658 apply (frule_tac x = "(ucast (p && mask pt_bits >> 2))" in pte_relation_alignedD) 659 apply assumption 660 apply (simp add:mask_pt_bits_inner_beauty) 661 apply (clarsimp simp:pte_relation_aligned_def 662 split:if_splits ARM_H.pte.splits) 663 apply (drule_tac p' = "p && ~~ mask 6" in valid_duplicates'_D[rotated]) 664 apply (simp add:is_aligned_weaken[where y = 2] is_aligned_neg_mask) 665 apply (clarsimp simp: vs_ptr_align_def) 666 apply (simp add:and_not_mask_twice) 667 apply (frule_tac x = "(ucast ((p && ~~ mask 6) && mask pt_bits >> 2))" in pte_relation_alignedD) 668 apply assumption 669 apply (simp add:expand) 670 apply (subst mask_pt_bits_inner_beauty) 671 apply (simp add:is_aligned_neg_mask) 672 apply assumption 673 apply (clarsimp simp: pte_relation_aligned_def 674 is_aligned_mask[where 'a=32, symmetric]) 675 \<comment> \<open>master_pde = LargePagePTE\<close> 676 apply (clarsimp simp add: a_type_def return_def get_pt_def 677 bind_def get_pte_def get_object_def gets_def get_def 678 split: if_split_asm Structures_A.kernel_object.splits arch_kernel_obj.splits) 679 apply (clarsimp simp:typ_at'_def ko_wp_at'_def) 680 apply (clarsimp simp: in_magnitude_check objBits_simps archObjSize_def pageBits_def pteBits_def) 681 apply (clarsimp simp:state_relation_def) 682 apply (drule_tac s = a and s' = b and p = "p && ~~ mask 6" 683 in aligned_distinct_relation_pte_atI'[rotated -1]) 684 apply (clarsimp simp:pte_at_def obj_at_def 685 and_not_mask_twice a_type_simps is_aligned_neg_mask) 686 apply simp 687 apply simp 688 apply (clarsimp simp:typ_at'_def ko_wp_at'_def) 689 apply (case_tac ko; simp) 690 apply (rename_tac arch_kernel_object) 691 apply (case_tac arch_kernel_object, simp_all add: projectKOs)[1] 692 apply clarsimp 693 apply (frule_tac x = "(ucast ((p && ~~ mask 6 )&& mask pt_bits >> 2))" in pte_relation_alignedD) 694 apply assumption 695 apply (simp add: expand) 696 apply (subst mask_pt_bits_inner_beauty) 697 apply (simp add:is_aligned_neg_mask) 698 apply assumption 699 apply (rename_tac pte) 700 apply (case_tac pte) 701 apply (simp_all add:pte_relation_aligned_def is_aligned_mask[symmetric]) 702 apply (drule_tac p = "p && ~~ mask 6" and p' = p in valid_duplicates'_D) 703 apply assumption 704 apply simp 705 apply (clarsimp simp: vs_ptr_align_def and_not_mask_twice) 706 apply (clarsimp simp: if_bool_eq_disj) 707 \<comment> \<open>master_pde = SmallPagePTE\<close> 708 apply (clarsimp simp add: a_type_def return_def get_pt_def 709 bind_def get_pte_def get_object_def gets_def get_def 710 split: if_split_asm Structures_A.kernel_object.splits 711 arch_kernel_obj.splits) 712 apply (clarsimp simp:typ_at'_def ko_wp_at'_def) 713 apply (clarsimp simp: in_magnitude_check objBits_simps 714 archObjSize_def pageBits_def pteBits_def) 715 apply (clarsimp simp:state_relation_def) 716 apply (frule_tac x = "(ucast (p && mask pt_bits >> 2))" 717 in pte_relation_alignedD) 718 apply assumption 719 apply (simp add:mask_pt_bits_inner_beauty) 720 apply (clarsimp simp:pte_relation_aligned_def 721 split:if_splits ARM_H.pte.splits) 722 apply (drule_tac p' = "p && ~~ mask 6" in valid_duplicates'_D[rotated]) 723 apply (simp add:is_aligned_weaken[where y = 2] is_aligned_neg_mask) 724 apply (clarsimp simp: vs_ptr_align_def) 725 apply (simp add:and_not_mask_twice) 726 apply (drule_tac x = "(ucast ((p && ~~ mask 6) && mask pt_bits >> 2))" 727 in pte_relation_alignedD) 728 apply assumption 729 apply (simp add: expand) 730 apply (subst mask_pt_bits_inner_beauty) 731 apply (simp add:is_aligned_neg_mask) 732 apply assumption 733 apply (clarsimp simp: pte_relation_aligned_def 734 is_aligned_mask[where 'a=32, symmetric]) 735 done 736 qed 737 738lemma get_pte_corres': 739 "corres (pte_relation_aligned (p >> 2)) (pte_at p) 740 (pspace_aligned' and pspace_distinct') 741 (get_pte p) (getObject p)" 742 apply (rule stronger_corres_guard_imp, 743 rule get_pte_corres) 744 apply auto[1] 745 apply clarsimp 746 apply (rule aligned_distinct_relation_pte_atI') 747 apply (simp add:state_relation_def)+ 748 done 749 750lemma get_master_pte_corres': 751 "corres pte_relation' (pte_at p) 752 ((\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and 753 pspace_aligned' and pspace_distinct') 754 (get_master_pte p) (getObject p)" 755 apply (rule stronger_corres_guard_imp, 756 rule get_master_pte_corres) 757 apply auto 758 done 759 760(* FIXME: move *) 761lemma pd_slot_eq: 762 "((p::word32) && ~~ mask pd_bits) + (ucast x << 2) = p \<Longrightarrow> 763 (x::12 word) = ucast (p && mask pd_bits >> 2)" 764 apply (clarsimp simp:mask_def pd_bits_def pageBits_def) 765 apply word_bitwise 766 apply clarsimp 767 done 768 769(* FIXME: move *) 770lemma pt_slot_eq: 771 "((p::word32) && ~~ mask pt_bits) + (ucast x << 2) = p \<Longrightarrow> 772 (x::word8) = ucast (p && mask pt_bits >> 2)" 773 apply (clarsimp simp:mask_def pt_bits_def pageBits_def) 774 apply word_bitwise 775 apply clarsimp 776 done 777 778\<comment> \<open>set_other_obj_corres unfortunately doesn't work here\<close> 779lemma set_pd_corres [@lift_corres_args, corres]: 780 "pde_relation_aligned (p>>2) pde pde' \<Longrightarrow> 781 corres dc (ko_at (ArchObj (PageDirectory pd)) (p && ~~ mask pd_bits) 782 and pspace_aligned and valid_etcbs) 783 (pde_at' p) 784 (set_pd (p && ~~ mask pd_bits) (pd(ucast (p && mask pd_bits >> 2) := pde))) 785 (setObject p pde')" 786 apply (simp add: set_pd_def get_object_def bind_assoc) 787 apply (rule corres_no_failI) 788 apply (rule no_fail_pre, wp) 789 apply simp 790 apply (clarsimp simp: obj_at'_def ko_wp_at'_def typ_at'_def lookupAround2_known1 projectKOs) 791 apply (case_tac ko, simp_all)[1] 792 apply (rename_tac arch_kernel_object) 793 apply (case_tac arch_kernel_object, simp_all add: projectKOs)[1] 794 apply (simp add: objBits_simps archObjSize_def word_bits_def) 795 apply (clarsimp simp: setObject_def in_monad split_def updateObject_default_def projectKOs) 796 apply (simp add: in_magnitude_check objBits_simps archObjSize_def pageBits_def pdeBits_def) 797 apply (clarsimp simp: obj_at_def exec_gets) 798 apply (clarsimp simp: set_object_def bind_assoc exec_get) 799 apply (clarsimp simp: put_def) 800 apply (clarsimp simp: state_relation_def mask_pd_bits_inner_beauty) 801 apply (rule conjI) 802 apply (clarsimp simp: pspace_relation_def split del: if_split) 803 apply (rule conjI) 804 apply (subst pspace_dom_update, assumption) 805 apply (simp add: a_type_def) 806 apply (auto simp: dom_def)[1] 807 apply (rule conjI) 808 apply (drule bspec, blast) 809 apply clarsimp 810 apply (drule_tac x = x in spec) 811 apply (clarsimp simp: pde_relation_def mask_pd_bits_inner_beauty pde_relation_aligned_simp 812 dest!: more_pd_inner_beauty) 813 apply (rule ballI) 814 apply (drule (1) bspec) 815 apply clarsimp 816 apply (rule conjI) 817 apply (clarsimp simp: pde_relation_def mask_pd_bits_inner_beauty pde_relation_aligned_simp 818 dest!: more_pd_inner_beauty) 819 apply clarsimp 820 apply (drule bspec, assumption) 821 apply clarsimp 822 apply (erule (1) obj_relation_cutsE) 823 apply simp 824 apply simp 825 apply clarsimp 826 apply (frule (1) pspace_alignedD) 827 apply (drule_tac p=x in pspace_alignedD, assumption) 828 apply simp 829 apply (drule mask_alignment_ugliness) 830 apply (simp add: pd_bits_def pageBits_def) 831 apply (simp add: pd_bits_def pageBits_def) 832 apply clarsimp 833 apply (clarsimp simp: nth_ucast nth_shiftl) 834 apply (drule test_bit_size) 835 apply (clarsimp simp: word_size pd_bits_def pageBits_def) 836 apply arith 837 apply (simp split: if_split_asm) 838 apply (simp split: if_split_asm) 839 apply (simp add: other_obj_relation_def 840 split: Structures_A.kernel_object.splits arch_kernel_obj.splits) 841 apply (rule conjI) 842 apply (clarsimp simp: ekheap_relation_def pspace_relation_def) 843 apply (drule(1) ekheap_kheap_dom) 844 apply clarsimp 845 apply (drule_tac x=p in bspec, erule domI) 846 apply (simp add: other_obj_relation_def 847 split: Structures_A.kernel_object.splits) 848 apply (rule conjI) 849 apply (clarsimp simp add: ghost_relation_def) 850 apply (erule_tac x="p && ~~ mask pd_bits" in allE)+ 851 apply fastforce 852 apply (simp add: map_to_ctes_upd_other) 853 apply (simp add: fun_upd_def) 854 apply (simp add: caps_of_state_after_update obj_at_def swp_cte_at_caps_of) 855 done 856 857 858lemma set_pt_corres [@lift_corres_args, corres]: 859 "pte_relation_aligned (p >> 2) pte pte' \<Longrightarrow> 860 corres dc (ko_at (ArchObj (PageTable pt)) (p && ~~ mask pt_bits) 861 and pspace_aligned and valid_etcbs) 862 (pte_at' p) 863 (set_pt (p && ~~ mask pt_bits) (pt(ucast (p && mask pt_bits >> 2) := pte))) 864 (setObject p pte')" 865 apply (simp add: set_pt_def get_object_def bind_assoc) 866 apply (rule corres_no_failI) 867 apply (rule no_fail_pre, wp) 868 apply simp 869 apply (clarsimp simp: obj_at'_def ko_wp_at'_def typ_at'_def lookupAround2_known1 projectKOs) 870 apply (case_tac ko, simp_all)[1] 871 apply (rename_tac arch_kernel_object) 872 apply (case_tac arch_kernel_object, simp_all add: projectKOs)[1] 873 apply (simp add: objBits_simps archObjSize_def word_bits_def) 874 apply (clarsimp simp: setObject_def in_monad split_def updateObject_default_def projectKOs) 875 apply (simp add: in_magnitude_check objBits_simps archObjSize_def pageBits_def pteBits_def) 876 apply (clarsimp simp: obj_at_def exec_gets) 877 apply (clarsimp simp: set_object_def bind_assoc exec_get) 878 apply (clarsimp simp: put_def) 879 apply (clarsimp simp: state_relation_def mask_pt_bits_inner_beauty) 880 apply (rule conjI) 881 apply (clarsimp simp: pspace_relation_def split del: if_split) 882 apply (rule conjI) 883 apply (subst pspace_dom_update, assumption) 884 apply (simp add: a_type_def) 885 apply (auto simp: dom_def)[1] 886 apply (rule conjI) 887 apply (drule bspec, blast) 888 apply (clarsimp simp: pte_relation_def mask_pt_bits_inner_beauty pte_relation_aligned_simp 889 dest!: more_pt_inner_beauty) 890 apply (rule ballI) 891 apply (drule (1) bspec) 892 apply clarsimp 893 apply (rule conjI) 894 apply (clarsimp simp: pte_relation_def mask_pt_bits_inner_beauty pte_relation_aligned_simp 895 dest!: more_pt_inner_beauty) 896 apply clarsimp 897 apply (drule bspec, assumption) 898 apply clarsimp 899 apply (erule (1) obj_relation_cutsE) 900 apply simp 901 apply clarsimp 902 apply (frule (1) pspace_alignedD) 903 apply (drule_tac p=x in pspace_alignedD, assumption) 904 apply simp 905 apply (drule mask_alignment_ugliness) 906 apply (simp add: pt_bits_def pageBits_def) 907 apply (simp add: pt_bits_def pageBits_def) 908 apply clarsimp 909 apply (clarsimp simp: nth_ucast nth_shiftl) 910 apply (drule test_bit_size) 911 apply (clarsimp simp: word_size pt_bits_def pageBits_def) 912 apply arith 913 apply simp 914 apply (simp split: if_split_asm) 915 apply (simp split: if_split_asm) 916 apply (simp add: other_obj_relation_def 917 split: Structures_A.kernel_object.splits arch_kernel_obj.splits) 918 apply (rule conjI) 919 apply (clarsimp simp: ekheap_relation_def pspace_relation_def) 920 apply (drule(1) ekheap_kheap_dom) 921 apply clarsimp 922 apply (drule_tac x=p in bspec, erule domI) 923 apply (simp add: other_obj_relation_def 924 split: Structures_A.kernel_object.splits) 925 apply (rule conjI) 926 apply (clarsimp simp add: ghost_relation_def) 927 apply (erule_tac x="p && ~~ mask pt_bits" in allE)+ 928 apply fastforce 929 apply (simp add: map_to_ctes_upd_other) 930 apply (simp add: fun_upd_def) 931 apply (simp add: caps_of_state_after_update obj_at_def swp_cte_at_caps_of) 932 done 933lemma store_pde_corres [@lift_corres_args, corres]: 934 "pde_relation_aligned (p >> 2) pde pde' \<Longrightarrow> 935 corres dc (pde_at p and pspace_aligned and valid_etcbs) (pde_at' p) (store_pde p pde) (storePDE p pde')" 936 apply (simp add: store_pde_def storePDE_def) 937 apply (rule corres_symb_exec_l) 938 apply (erule set_pd_corres[OF _ refl]) 939 apply (clarsimp simp: exs_valid_def get_pd_def get_object_def exec_gets bind_assoc 940 obj_at_def pde_at_def) 941 apply (clarsimp simp: a_type_def return_def 942 split: Structures_A.kernel_object.splits arch_kernel_obj.splits if_split_asm) 943 apply wp 944 apply clarsimp 945 apply (clarsimp simp: get_pd_def obj_at_def no_fail_def pde_at_def 946 get_object_def bind_assoc exec_gets) 947 apply (clarsimp simp: a_type_def return_def 948 split: Structures_A.kernel_object.splits arch_kernel_obj.splits if_split_asm) 949 done 950 951lemma store_pde_corres': 952 "pde_relation_aligned (p >> 2) pde pde' \<Longrightarrow> 953 corres dc 954 (pde_at p and pspace_aligned and valid_etcbs) (pspace_aligned' and pspace_distinct') 955 (store_pde p pde) (storePDE p pde')" 956 apply (rule stronger_corres_guard_imp, rule store_pde_corres) 957 apply auto 958 done 959 960lemma store_pte_corres [@lift_corres_args, corres]: 961 "pte_relation_aligned (p>>2) pte pte' \<Longrightarrow> 962 corres dc (pte_at p and pspace_aligned and valid_etcbs) (pte_at' p) (store_pte p pte) (storePTE p pte')" 963 apply (simp add: store_pte_def storePTE_def) 964 apply (rule corres_symb_exec_l) 965 apply (erule set_pt_corres[OF _ refl]) 966 apply (clarsimp simp: exs_valid_def get_pt_def get_object_def 967 exec_gets bind_assoc obj_at_def pte_at_def) 968 apply (clarsimp simp: a_type_def return_def 969 split: Structures_A.kernel_object.splits arch_kernel_obj.splits if_split_asm) 970 apply wp 971 apply clarsimp 972 apply (clarsimp simp: get_pt_def obj_at_def pte_at_def no_fail_def 973 get_object_def bind_assoc exec_gets) 974 apply (clarsimp simp: a_type_def return_def 975 split: Structures_A.kernel_object.splits arch_kernel_obj.splits if_split_asm) 976 done 977 978lemma store_pte_corres': 979 "pte_relation_aligned (p >> 2) pte pte' \<Longrightarrow> 980 corres dc (pte_at p and pspace_aligned and valid_etcbs) 981 (pspace_aligned' and pspace_distinct') 982 (store_pte p pte) (storePTE p pte')" 983 apply (rule stronger_corres_guard_imp, rule store_pte_corres) 984 apply auto 985 done 986 987lemma lookup_pd_slot_corres [simp]: 988 "lookupPDSlot pd vptr = lookup_pd_slot pd vptr" 989 by (simp add: lookupPDSlot_def lookup_pd_slot_def pageBits_def ptBits_def pdeBits_def) 990 991defs checkPDAt_def: 992 "checkPDAt pd \<equiv> stateAssert (page_directory_at' pd) []" 993 994defs checkPTAt_def: 995 "checkPTAt pt \<equiv> stateAssert (page_table_at' pt) []" 996 997lemma pte_relation_must_pte: 998 "pte_relation m (ArchObj (PageTable pt)) ko \<Longrightarrow> \<exists>pte. ko = (KOArch (KOPTE pte))" 999 apply (case_tac ko) 1000 apply (simp_all add:pte_relation_def) 1001 apply clarsimp 1002 done 1003 1004lemma pde_relation_must_pde: 1005 "pde_relation m (ArchObj (PageDirectory pd)) ko \<Longrightarrow> \<exists>pde. ko = (KOArch (KOPDE pde))" 1006 apply (case_tac ko) 1007 apply (simp_all add:pde_relation_def) 1008 apply clarsimp 1009 done 1010 1011lemma page_table_at_state_relation: 1012 "\<lbrakk>page_table_at (ptrFromPAddr ptr) s; pspace_aligned s; 1013 (s, sa) \<in> state_relation;pspace_distinct' sa\<rbrakk> 1014 \<Longrightarrow> page_table_at' (ptrFromPAddr ptr) sa" 1015 apply (clarsimp simp:page_table_at'_def state_relation_def 1016 obj_at_def) 1017 apply (clarsimp simp:pspace_relation_def) 1018 apply (drule bspec) 1019 apply fastforce 1020 apply clarsimp 1021 apply (frule(1) pspace_alignedD) 1022 apply (simp add:ptrFromPAddr_def ptBits_def pageBits_def pteBits_def) 1023 apply clarsimp 1024 apply (drule_tac x = "ucast y" in spec) 1025 apply (drule sym[where s = "pspace_dom (kheap s)"]) 1026 apply (clarsimp simp:typ_at'_def ko_wp_at'_def) 1027 apply (subgoal_tac "(ptr + physMappingOffset + (y << 2)) \<in> dom (ksPSpace sa)") 1028 prefer 2 1029 apply (clarsimp simp: pspace_dom_def) 1030 apply (rule_tac x = "ptr + physMappingOffset" in bexI[where A = "dom (kheap s)"]) 1031 apply (simp add:image_def) 1032 apply (rule_tac x = "ucast y" in exI) 1033 apply (simp add:ucast_ucast_len) 1034 apply fastforce 1035 apply (thin_tac "dom a = b" for a b) 1036 apply (frule(1) pspace_alignedD) 1037 apply (clarsimp simp:ucast_ucast_len 1038 split:if_splits) 1039 apply (drule pte_relation_must_pte) 1040 apply (drule(1) pspace_distinctD') 1041 apply (clarsimp simp:objBits_simps archObjSize_def) 1042 apply (rule is_aligned_weaken) 1043 apply (erule aligned_add_aligned) 1044 apply (rule is_aligned_shiftl_self) 1045 apply simp 1046 apply (simp add: pteBits_def) 1047 done 1048 1049lemma page_directory_at_state_relation: 1050 "\<lbrakk>page_directory_at ptr s; pspace_aligned s; 1051 (s, sa) \<in> state_relation;pspace_distinct' sa\<rbrakk> 1052 \<Longrightarrow> page_directory_at' ptr sa" 1053 apply (clarsimp simp:page_directory_at'_def state_relation_def obj_at_def) 1054 apply (clarsimp simp:pspace_relation_def) 1055 apply (drule bspec) 1056 apply fastforce 1057 apply clarsimp 1058 apply (frule(1) pspace_alignedD) 1059 apply (simp add: pdBits_def pageBits_def pdeBits_def) 1060 apply clarsimp 1061 apply (drule_tac x = "ucast y" in spec) 1062 apply (drule sym[where s = "pspace_dom (kheap s)"]) 1063 apply (clarsimp simp:typ_at'_def ko_wp_at'_def) 1064 apply (subgoal_tac "(ptr + (y << 2)) \<in> dom (ksPSpace sa)") 1065 prefer 2 1066 apply (clarsimp simp: pspace_dom_def) 1067 apply (rule_tac x = "ptr" in bexI[where A = "dom (kheap s)"]) 1068 apply (simp add: image_def) 1069 apply (rule_tac x = "ucast y" in exI) 1070 apply (simp add:ucast_ucast_len) 1071 apply fastforce 1072 apply (thin_tac "dom a = b" for a b) 1073 apply (frule(1) pspace_alignedD) 1074 apply (clarsimp simp:ucast_ucast_len split:if_splits) 1075 apply (drule pde_relation_must_pde) 1076 apply (drule(1) pspace_distinctD') 1077 apply (clarsimp simp:objBits_simps archObjSize_def) 1078 apply (rule is_aligned_weaken) 1079 apply (erule aligned_add_aligned) 1080 apply (rule is_aligned_shiftl_self) 1081 apply simp 1082 apply (simp add: pdeBits_def) 1083 done 1084 1085lemma getPDE_wp: 1086 "\<lbrace>\<lambda>s. \<forall>ko. ko_at' (ko::pde) p s \<longrightarrow> Q ko s\<rbrace> getObject p \<lbrace>Q\<rbrace>" 1087 by (clarsimp simp: getObject_def split_def loadObject_default_def 1088 archObjSize_def in_magnitude_check pdeBits_def 1089 projectKOs in_monad valid_def obj_at'_def objBits_simps) 1090 1091lemma getPTE_wp: 1092 "\<lbrace>\<lambda>s. \<forall>ko. ko_at' (ko::pte) p s \<longrightarrow> Q ko s\<rbrace> getObject p \<lbrace>Q\<rbrace>" 1093 by (clarsimp simp: getObject_def split_def loadObject_default_def 1094 archObjSize_def in_magnitude_check pteBits_def 1095 projectKOs in_monad valid_def obj_at'_def objBits_simps) 1096 1097lemmas get_pde_wp_valid = hoare_add_post'[OF get_pde_valid get_pde_wp] 1098 1099lemma page_table_at_lift: 1100 "\<forall>s s'. (s, s') \<in> state_relation \<longrightarrow> (ptrFromPAddr ptr) = ptr' \<longrightarrow> 1101 (pspace_aligned s \<and> valid_pde (ARM_A.PageTablePDE ptr x z) s) \<longrightarrow> 1102 pspace_distinct' s' \<longrightarrow> page_table_at' ptr' s'" 1103 by (fastforce intro!: page_table_at_state_relation) 1104 1105lemmas checkPTAt_corres [corresK] = 1106 corres_stateAssert_implied_frame[OF page_table_at_lift, folded checkPTAt_def] 1107 1108 1109lemma lookup_pt_slot_corres [@lift_corres_args, corres]: 1110 "corres (lfr \<oplus> (=)) 1111 (pde_at (lookup_pd_slot pd vptr) and pspace_aligned and valid_vspace_objs 1112 and (\<exists>\<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) and 1113 K (is_aligned pd pd_bits \<and> vptr < kernel_base 1114 \<and> ucast (lookup_pd_slot pd vptr && mask pd_bits >> 2) \<notin> kernel_mapping_slots)) 1115 (pspace_aligned' and pspace_distinct') 1116 (lookup_pt_slot pd vptr) (lookupPTSlot pd vptr)" 1117 unfolding lookup_pt_slot_def lookupPTSlot_def lookupPTSlotFromPT_def 1118 apply (corressimp simp: pde_relation_aligned_def lookup_failure_map_def 1119 ptBits_def pdeBits_def pageBits_def pteBits_def mask_def 1120 wp: get_pde_wp_valid getPDE_wp) 1121 by (auto simp: lookup_failure_map_def obj_at_def) 1122 1123declare in_set_zip_refl[simp] 1124 1125crunch typ_at' [wp]: storePDE "\<lambda>s. P (typ_at' T p s)" 1126 (wp: crunch_wps mapM_x_wp' simp: crunch_simps) 1127 1128crunch typ_at' [wp]: storePTE "\<lambda>s. P (typ_at' T p s)" 1129 (wp: crunch_wps mapM_x_wp' simp: crunch_simps) 1130 1131lemmas storePDE_typ_ats[wp] = typ_at_lifts [OF storePDE_typ_at'] 1132lemmas storePTE_typ_ats[wp] = typ_at_lifts [OF storePTE_typ_at'] 1133 1134lemma setObject_asid_typ_at' [wp]: 1135 "\<lbrace>\<lambda>s. P (typ_at' T p s)\<rbrace> setObject p' (v::asidpool) \<lbrace>\<lambda>_ s. P (typ_at' T p s)\<rbrace>" 1136 by (wp setObject_typ_at') 1137 1138lemmas setObject_asid_typ_ats' [wp] = typ_at_lifts [OF setObject_asid_typ_at'] 1139 1140lemma getObject_pte_inv[wp]: 1141 "\<lbrace>P\<rbrace> getObject p \<lbrace>\<lambda>rv :: pte. P\<rbrace>" 1142 by (simp add: getObject_inv loadObject_default_inv) 1143 1144lemma getObject_pde_inv[wp]: 1145 "\<lbrace>P\<rbrace> getObject p \<lbrace>\<lambda>rv :: pde. P\<rbrace>" 1146 by (simp add: getObject_inv loadObject_default_inv) 1147 1148crunch typ_at'[wp]: copyGlobalMappings "\<lambda>s. P (typ_at' T p s)" 1149 (wp: mapM_x_wp' ignore: forM_x getObject) 1150 1151lemmas copyGlobalMappings_typ_ats[wp] = typ_at_lifts [OF copyGlobalMappings_typ_at'] 1152 1153lemma align_entry_add_cong: 1154 "\<lbrakk>is_aligned (pd::word32) 6; is_aligned pd' 6\<rbrakk> 1155 \<Longrightarrow> is_aligned (pd + x >> 2) (pde_align' y) = 1156 is_aligned (pd' + x >> 2) (pde_align' y) " 1157 apply (clarsimp simp: pde_align'_def is_aligned_mask mask_def 1158 split: ARM_H.pde.splits) 1159 apply word_bitwise 1160 apply auto 1161 done 1162 1163lemma arm_global_pd_corres [corres]: 1164 "corres (=) (\<lambda>_. True) (\<lambda>_. True) 1165 (gets (arm_global_pd \<circ> arch_state)) (gets (armKSGlobalPD \<circ> ksArchState))" 1166 by (clarsimp simp: state_relation_def arch_state_relation_def) 1167 1168 1169 1170lemma copy_global_mappings_corres [@lift_corres_args, corres]: 1171 "corres dc (page_directory_at pd and pspace_aligned and valid_arch_state and valid_etcbs) 1172 (page_directory_at' pd and valid_arch_state') 1173 (copy_global_mappings pd) (copyGlobalMappings pd)" (is "corres _ ?apre _ _ _") 1174 unfolding copy_global_mappings_def copyGlobalMappings_def pd_bits_def pdBits_def objBits_simps 1175 archObjSize_def kernel_base_def ARM.kernelBase_def ARM_H.kernelBase_def 1176 apply corressimp 1177 apply (rule_tac P="page_directory_at global_pd 1178 and (\<lambda>_. is_aligned global_pd 6 \<and> is_aligned pd 6) and ?apre" and 1179 P'="page_directory_at' globalPD and page_directory_at' pd" 1180 in corresK_mapM_x[OF order_refl]) 1181 apply (corressimp simp: pdeBits_def ptBits_def pdeBits_def pageBits_def pteBits_def mask_def 1182 wp: get_pde_wp getPDE_wp)+ 1183 apply (rule conjI) 1184 subgoal by (auto intro!: page_directory_pde_atI page_directory_pde_atI' 1185 simp: pde_relation_aligned_def pageBits_def le_less_trans 1186 dest: align_entry_add_cong) 1187 by (auto simp: valid_arch_state_def obj_at_def valid_arch_state'_def 1188 intro: is_aligned_weaken[of _ 14] 1189 dest!:pspace_alignedD) 1190 1191lemma arch_cap_rights_update: 1192 "acap_relation c c' \<Longrightarrow> 1193 cap_relation (cap.ArchObjectCap (acap_rights_update (acap_rights c \<inter> msk) c)) 1194 (Arch.maskCapRights (rights_mask_map msk) c')" 1195 apply (cases c, simp_all add: ARM_H.maskCapRights_def 1196 acap_rights_update_def Let_def isCap_simps) 1197 apply (simp add: maskVMRights_def vmrights_map_def rights_mask_map_def 1198 validate_vm_rights_def vm_read_write_def vm_read_only_def 1199 vm_kernel_only_def ) 1200 done 1201 1202lemma arch_deriveCap_inv: 1203 "\<lbrace>P\<rbrace> Arch.deriveCap arch_cap u \<lbrace>\<lambda>rv. P\<rbrace>" 1204 apply (simp add: ARM_H.deriveCap_def 1205 cong: if_cong 1206 split del: if_split) 1207 apply (rule hoare_pre, wp undefined_valid) 1208 apply (cases u, simp_all add: isCap_defs) 1209 done 1210 1211lemma arch_deriveCap_valid: 1212 "\<lbrace>valid_cap' (ArchObjectCap arch_cap)\<rbrace> 1213 Arch.deriveCap u arch_cap 1214 \<lbrace>\<lambda>rv. valid_cap' rv\<rbrace>,-" 1215 apply (simp add: ARM_H.deriveCap_def 1216 cong: if_cong 1217 split del: if_split) 1218 apply (rule hoare_pre, wp undefined_validE_R) 1219 apply (cases arch_cap, simp_all add: isCap_defs) 1220 apply (simp add: valid_cap'_def capAligned_def 1221 capUntypedPtr_def ARM_H.capUntypedPtr_def) 1222 done 1223 1224lemma arch_derive_corres [corres]: 1225 "cap_relation (cap.ArchObjectCap c) (ArchObjectCap c') \<Longrightarrow> 1226 corres (ser \<oplus> (\<lambda>c c'. cap_relation c c')) 1227 \<top> \<top> 1228 (arch_derive_cap c) 1229 (Arch.deriveCap slot c')" 1230 unfolding arch_derive_cap_def ARM_H.deriveCap_def Let_def 1231 apply (cases c, simp_all add: isCap_simps split: option.splits split del: if_split) 1232 apply (clarify?, rule corres_noopE; wpsimp)+ 1233 done 1234 1235definition 1236 "vmattributes_map \<equiv> \<lambda>R. VMAttributes (PageCacheable \<in> R) (ParityEnabled \<in> R) (XNever \<in> R)" 1237 1238definition 1239 mapping_map :: "ARM_A.pte \<times> word32 list + ARM_A.pde \<times> word32 list \<Rightarrow> 1240 ARM_H.pte \<times> word32 list + ARM_H.pde \<times> word32 list \<Rightarrow> bool" 1241where 1242 "mapping_map \<equiv> pte_relation' \<otimes> (=) \<oplus> pde_relation' \<otimes> (=)" 1243 1244lemma create_mapping_entries_corres [corres]: 1245 "\<lbrakk> vm_rights' = vmrights_map vm_rights; 1246 attrib' = vmattributes_map attrib; base = base'; vptr = vptr'; pgsz = pgsz'; pd = pd' \<rbrakk> 1247 \<Longrightarrow> corres (ser \<oplus> mapping_map) 1248 (\<lambda>s. (pgsz = ARMSmallPage \<or> pgsz = ARMLargePage \<longrightarrow> pde_at (lookup_pd_slot pd vptr) s) 1249 \<and> (is_aligned pd pd_bits \<and> vmsz_aligned vptr pgsz \<and> vptr < kernel_base \<and> vm_rights \<in> valid_vm_rights) 1250 \<and> valid_vspace_objs s \<and> pspace_aligned s \<and> (\<exists>\<rhd> (lookup_pd_slot pd vptr && ~~ mask pd_bits)) s) 1251 (pspace_aligned' and pspace_distinct') 1252 (create_mapping_entries base vptr pgsz vm_rights attrib pd) 1253 (createMappingEntries base' vptr' pgsz' vm_rights' attrib' pd')" 1254 unfolding createMappingEntries_def mapping_map_def 1255 by (cases pgsz; corressimp simp: vmattributes_map_def less_kernel_base_mapping_slots 1256 largePagePTEOffsets_def 1257 largePagePTE_offsets_def 1258 superSectionPDEOffsets_def 1259 superSectionPDE_offsets_def 1260 pteBits_def pdeBits_def) 1261 1262lemma pte_relation'_Invalid_inv [simp]: 1263 "pte_relation' x ARM_H.pte.InvalidPTE = (x = ARM_A.pte.InvalidPTE)" 1264 by (cases x) auto 1265 1266definition 1267 "valid_slots' m \<equiv> case m of 1268 Inl (pte, xs) \<Rightarrow> \<lambda>s. valid_pte' pte s 1269 | Inr (pde, xs) \<Rightarrow> \<lambda>s. valid_pde' pde s" 1270 1271lemma valid_slots_typ_at': 1272 assumes x: "\<And>T p. \<lbrace>typ_at' T p\<rbrace> f \<lbrace>\<lambda>rv. typ_at' T p\<rbrace>" 1273 shows "\<lbrace>valid_slots' m\<rbrace> f \<lbrace>\<lambda>rv. valid_slots' m\<rbrace>" 1274 unfolding valid_slots'_def 1275 apply (cases m) 1276 apply (case_tac a) 1277 apply simp 1278 apply (wp x valid_pte_lift') 1279 apply (case_tac b) 1280 apply simp 1281 apply (wp x valid_pde_lift') 1282 done 1283 1284lemma createMappingEntries_valid_slots' [wp]: 1285 "\<lbrace>valid_objs' and 1286 K (vmsz_aligned' base sz \<and> vmsz_aligned' vptr sz \<and> ptrFromPAddr base \<noteq> 0) \<rbrace> 1287 createMappingEntries base vptr sz vm_rights attrib pd 1288 \<lbrace>\<lambda>m. valid_slots' m\<rbrace>, -" 1289 apply (simp add: createMappingEntries_def) 1290 apply (rule hoare_pre) 1291 apply (wp|wpc|simp add: valid_slots'_def valid_mapping'_def)+ 1292 apply (simp add: vmsz_aligned'_def) 1293 apply auto 1294 done 1295 1296lemma ensure_safe_mapping_corres [corres]: 1297 "mapping_map m m' \<Longrightarrow> 1298 corres (ser \<oplus> dc) (valid_mapping_entries m) 1299 (pspace_aligned' and pspace_distinct' 1300 and (\<lambda>s. vs_valid_duplicates' (ksPSpace s))) 1301 (ensure_safe_mapping m) (ensureSafeMapping m')" 1302 unfolding mapping_map_def ensureSafeMapping_def 1303 apply (cases m; cases m'; simp; 1304 match premises in "(_ \<otimes> (=)) p p'" for p p' \<Rightarrow> \<open>cases "fst p"; cases "fst p'"\<close>; clarsimp) 1305 by (corressimp corresK: mapME_x_corresK_inv 1306 wp: get_master_pte_wp get_master_pde_wp getPTE_wp getPDE_wp; 1307 auto simp add: valid_mapping_entries_def)+ 1308 1309lemma asidHighBitsOf [simp]: 1310 "asidHighBitsOf asid = ucast (asid_high_bits_of asid)" 1311 apply (simp add: asidHighBitsOf_def asid_high_bits_of_def asidHighBits_def) 1312 apply (rule word_eqI) 1313 apply (simp add: word_size nth_ucast) 1314 done 1315 1316 1317lemma page_directory_at_lift: 1318 "corres_inst_eq ptr ptr' \<Longrightarrow> \<forall>s s'. (s, s') \<in> state_relation \<longrightarrow> True \<longrightarrow> 1319 (pspace_aligned s \<and> page_directory_at ptr s) \<longrightarrow> 1320 pspace_distinct' s' \<longrightarrow> page_directory_at' ptr' s'" 1321 by (fastforce simp: corres_inst_eq_def intro!: page_directory_at_state_relation ) 1322 1323lemmas checkPDAt_corres = 1324 corres_stateAssert_implied_frame[OF page_directory_at_lift, folded checkPDAt_def] 1325 1326lemma getASID_wp: 1327 "\<lbrace>\<lambda>s. \<forall>ko. ko_at' (ko::asidpool) p s \<longrightarrow> Q ko s\<rbrace> getObject p \<lbrace>Q\<rbrace>" 1328 by (clarsimp simp: getObject_def split_def loadObject_default_def 1329 archObjSize_def in_magnitude_check pageBits_def 1330 projectKOs in_monad valid_def obj_at'_def objBits_simps) 1331 1332lemma ko_at_typ_at_asidpool: 1333 "ko_at (ArchObj (arch_kernel_obj.ASIDPool pool)) x s \<Longrightarrow> typ_at (AArch AASIDPool) x s" 1334 by (clarsimp simp: obj_at_def a_type_simps) 1335 1336 1337 1338 1339 1340lemma find_pd_for_asid_corres [corres]: 1341 "asid = asid' \<Longrightarrow> corres (lfr \<oplus> (=)) ((\<lambda>s. valid_arch_state s \<or> vspace_at_asid asid pd s) 1342 and valid_vspace_objs and pspace_aligned 1343 and K (0 < asid \<and> asid \<le> mask asidBits)) 1344 (pspace_aligned' and pspace_distinct' and no_0_obj') 1345 (find_pd_for_asid asid) (findPDForASID asid')" 1346 apply (simp add: find_pd_for_asid_def findPDForASID_def liftME_def bindE_assoc) 1347 apply (corressimp simp: liftE_bindE assertE_assert mask_asid_low_bits_ucast_ucast 1348 lookup_failure_map_def 1349 wp: getPDE_wp getASID_wp 1350 search: checkPDAt_corres corres_gets_asid) 1351 subgoal premises prems for s s' 1352 apply (intro allI impI conjI) 1353 subgoal asid_pool_at for x 1354 apply (insert prems) 1355 apply (elim conjE disjE) 1356 apply (fastforce dest: valid_asid_tableD) 1357 apply (clarsimp simp: vspace_at_asid_def) 1358 apply (clarsimp simp: vs_asid_refs_def graph_of_def elim!: vs_lookupE) 1359 apply (erule rtranclE) 1360 subgoal by simp 1361 apply (simp add: arm_asid_table_related) 1362 apply (clarsimp dest!: vs_lookup1D) 1363 apply (erule rtranclE) 1364 apply (clarsimp simp: vs_refs_def graph_of_def obj_at_def a_type_def 1365 split: Structures_A.kernel_object.splits 1366 arch_kernel_obj.splits) 1367 apply (clarsimp dest!: vs_lookup1D) 1368 apply (erule rtranclE) 1369 apply (fastforce dest!: vs_lookup1D) 1370 by (clarsimp dest!: vs_lookup1D) 1371 subgoal pd_at for x pool xa 1372 apply (insert prems) 1373 apply (rule valid_vspace_obj_elims) 1374 apply (rule valid_vspace_objsD) 1375 apply (rule vs_lookupI) 1376 apply (rule vs_asid_refsI) 1377 apply fastforce 1378 apply (rule rtrancl_refl) 1379 by (simp add: ranI)+ 1380 apply (insert prems) 1381 apply (fastforce simp add: asidRange_def mask_2pm1[symmetric]) 1382 subgoal for x by (insert asid_pool_at[of x], auto simp: arm_asid_table_related) 1383 subgoal for x ko 1384 apply (cases ko; simp) 1385 apply (frule arm_asid_table_related[where s'=s', simplified o_def]) 1386 apply (cut_tac asid_pool_at[of x, simplified obj_at_def]) 1387 apply clarsimp 1388 apply (frule pspace_relation_absD, fastforce) 1389 apply (clarsimp simp: other_obj_relation_def obj_at'_def projectKOs asid_pool_relation_def) 1390 apply (cut_tac pd_at[of _ _ 0]; assumption?) 1391 apply (drule(1) no_0_obj'_abstract) 1392 by (auto simp add: obj_at_def inv_def o_def) 1393 done 1394 done 1395 1396lemma find_pd_for_asid_corres': 1397 "corres (lfr \<oplus> (=)) (vspace_at_asid asid pd and valid_vspace_objs 1398 and pspace_aligned and K (0 < asid \<and> asid \<le> mask asidBits)) 1399 (pspace_aligned' and pspace_distinct' and no_0_obj') 1400 (find_pd_for_asid asid) (findPDForASID asid)" 1401 apply (rule corres_guard_imp, rule find_pd_for_asid_corres) 1402 apply fastforce+ 1403 done 1404 1405lemma setObject_arch: 1406 assumes X: "\<And>p q n ko. \<lbrace>\<lambda>s. P (ksArchState s)\<rbrace> updateObject val p q n ko \<lbrace>\<lambda>rv s. P (ksArchState s)\<rbrace>" 1407 shows "\<lbrace>\<lambda>s. P (ksArchState s)\<rbrace> setObject t val \<lbrace>\<lambda>rv s. P (ksArchState s)\<rbrace>" 1408 apply (simp add: setObject_def split_def) 1409 apply (wp X | simp)+ 1410 done 1411 1412lemma setObject_ASID_arch [wp]: 1413 "\<lbrace>\<lambda>s. P (ksArchState s)\<rbrace> setObject p (v::asidpool) \<lbrace>\<lambda>_ s. P (ksArchState s)\<rbrace>" 1414 apply (rule setObject_arch) 1415 apply (simp add: updateObject_default_def) 1416 apply wp 1417 apply simp 1418 done 1419 1420lemma setObject_PDE_arch [wp]: 1421 "\<lbrace>\<lambda>s. P (ksArchState s)\<rbrace> setObject p (v::pde) \<lbrace>\<lambda>_ s. P (ksArchState s)\<rbrace>" 1422 apply (rule setObject_arch) 1423 apply (simp add: updateObject_default_def) 1424 apply wp 1425 apply simp 1426 done 1427 1428lemma setObject_PTE_arch [wp]: 1429 "\<lbrace>\<lambda>s. P (ksArchState s)\<rbrace> setObject p (v::pte) \<lbrace>\<lambda>_ s. P (ksArchState s)\<rbrace>" 1430 apply (rule setObject_arch) 1431 apply (simp add: updateObject_default_def) 1432 apply wp 1433 apply simp 1434 done 1435 1436lemma setObject_ASID_valid_arch [wp]: 1437 "\<lbrace>valid_arch_state'\<rbrace> setObject p (v::asidpool) \<lbrace>\<lambda>_. valid_arch_state'\<rbrace>" 1438 by (rule valid_arch_state_lift'; wp) 1439 1440lemma setObject_PDE_valid_arch [wp]: 1441 "\<lbrace>valid_arch_state'\<rbrace> setObject p (v::pde) \<lbrace>\<lambda>_. valid_arch_state'\<rbrace>" 1442 by (rule valid_arch_state_lift') (wp setObject_typ_at')+ 1443 1444lemma setObject_PTE_valid_arch [wp]: 1445 "\<lbrace>valid_arch_state'\<rbrace> setObject p (v::pte) \<lbrace>\<lambda>_. valid_arch_state'\<rbrace>" 1446 by (rule valid_arch_state_lift') (wp setObject_typ_at')+ 1447 1448lemma setObject_ASID_ct [wp]: 1449 "\<lbrace>\<lambda>s. P (ksCurThread s)\<rbrace> setObject p (e::asidpool) \<lbrace>\<lambda>_ s. P (ksCurThread s)\<rbrace>" 1450 apply (simp add: setObject_def updateObject_default_def split_def) 1451 apply (wp updateObject_default_inv | simp)+ 1452 done 1453 1454lemma setObject_PDE_ct [wp]: 1455 "\<lbrace>\<lambda>s. P (ksCurThread s)\<rbrace> setObject p (e::pde) \<lbrace>\<lambda>_ s. P (ksCurThread s)\<rbrace>" 1456 apply (simp add: setObject_def updateObject_default_def split_def) 1457 apply (wp updateObject_default_inv | simp)+ 1458 done 1459 1460lemma setObject_pte_ct [wp]: 1461 "\<lbrace>\<lambda>s. P (ksCurThread s)\<rbrace> setObject p (e::pte) \<lbrace>\<lambda>_ s. P (ksCurThread s)\<rbrace>" 1462 apply (simp add: setObject_def updateObject_default_def split_def) 1463 apply (wp updateObject_default_inv | simp)+ 1464 done 1465 1466lemma setObject_ASID_cur_tcb' [wp]: 1467 "\<lbrace>\<lambda>s. cur_tcb' s\<rbrace> setObject p (e::asidpool) \<lbrace>\<lambda>_ s. cur_tcb' s\<rbrace>" 1468 apply (simp add: cur_tcb'_def) 1469 apply (rule hoare_lift_Pf [where f=ksCurThread]) 1470 apply wp+ 1471 done 1472 1473lemma setObject_PDE_cur_tcb' [wp]: 1474 "\<lbrace>\<lambda>s. cur_tcb' s\<rbrace> setObject p (e::pde) \<lbrace>\<lambda>_ s. cur_tcb' s\<rbrace>" 1475 apply (simp add: cur_tcb'_def) 1476 apply (rule hoare_lift_Pf [where f=ksCurThread]) 1477 apply wp+ 1478 done 1479 1480lemma setObject_pte_cur_tcb' [wp]: 1481 "\<lbrace>\<lambda>s. cur_tcb' s\<rbrace> setObject p (e::pte) \<lbrace>\<lambda>_ s. cur_tcb' s\<rbrace>" 1482 apply (simp add: cur_tcb'_def) 1483 apply (rule hoare_lift_Pf [where f=ksCurThread]) 1484 apply wp+ 1485 done 1486 1487 1488 1489lemma pde_at_aligned_vptr': 1490 "\<lbrakk>x \<in> set [0 , 4 .e. 0x3C]; page_directory_at' pd s; is_aligned vptr 24 \<rbrakk> \<Longrightarrow> 1491 pde_at' (x + lookup_pd_slot pd vptr) s" 1492 apply (simp add: lookup_pd_slot_def Let_def page_directory_at'_def add.commute add.left_commute) 1493 apply (clarsimp simp: upto_enum_step_def) 1494 apply (clarsimp simp: shiftl_t2n) 1495 apply (subst mult.commute) 1496 apply (subst ring_distribs [symmetric]) 1497 apply (erule allE) 1498 apply (erule impE) 1499 prefer 2 1500 apply assumption 1501 apply (erule (1) pde_shifting) 1502 done 1503 1504lemma page_directory_pde_at_lookupI': 1505 "page_directory_at' pd s \<Longrightarrow> pde_at' (lookup_pd_slot pd vptr) s" 1506 apply (simp add: lookup_pd_slot_def Let_def) 1507 apply (erule page_directory_pde_atI') 1508 apply (rule vptr_shiftr_le_2p) 1509 done 1510 1511lemma pt_bits_stuff: 1512 "pt_bits = ptBits" 1513 "ptBits < word_bits" 1514 "2 \<le> ptBits" 1515 by (simp add: pt_bits_def ptBits_def pageBits_def word_bits_def pteBits_def)+ 1516 1517lemma page_table_pte_at_lookupI': 1518 "page_table_at' pt s \<Longrightarrow> pte_at' (lookup_pt_slot_no_fail pt vptr) s" 1519 apply (simp add: lookup_pt_slot_no_fail_def) 1520 apply (erule page_table_pte_atI') 1521 apply (rule vptr_shiftr_le_2pt[simplified pt_bits_stuff]) 1522 done 1523 1524lemma storePTE_ctes [wp]: 1525 "\<lbrace>\<lambda>s. P (ctes_of s)\<rbrace> storePTE p pte \<lbrace>\<lambda>_ s. P (ctes_of s)\<rbrace>" 1526 apply (rule ctes_of_from_cte_wp_at [where Q=\<top>, simplified]) 1527 apply (rule storePTE_cte_wp_at') 1528 done 1529 1530lemma storePDE_ctes [wp]: 1531 "\<lbrace>\<lambda>s. P (ctes_of s)\<rbrace> storePDE p pte \<lbrace>\<lambda>_ s. P (ctes_of s)\<rbrace>" 1532 apply (rule ctes_of_from_cte_wp_at [where Q=\<top>, simplified]) 1533 apply (rule storePDE_cte_wp_at') 1534 done 1535 1536 1537lemma storePDE_valid_objs [wp]: 1538 "\<lbrace>valid_objs' and valid_pde' pde\<rbrace> storePDE p pde \<lbrace>\<lambda>_. valid_objs'\<rbrace>" 1539 apply (simp add: storePDE_def doMachineOp_def split_def) 1540 apply (rule hoare_pre) 1541 apply (wp hoare_drop_imps|wpc|simp)+ 1542 apply (rule setObject_valid_objs') 1543 prefer 2 1544 apply assumption 1545 apply (clarsimp simp: updateObject_default_def in_monad) 1546 apply (clarsimp simp: valid_obj'_def) 1547 done 1548 1549lemma setObject_ASID_cte_wp_at'[wp]: 1550 "\<lbrace>\<lambda>s. P (cte_wp_at' P' p s)\<rbrace> 1551 setObject ptr (asid::asidpool) 1552 \<lbrace>\<lambda>rv s. P (cte_wp_at' P' p s)\<rbrace>" 1553 apply (wp setObject_cte_wp_at2'[where Q="\<top>"]) 1554 apply (clarsimp simp: updateObject_default_def in_monad 1555 projectKO_opts_defs projectKOs) 1556 apply (rule equals0I) 1557 apply (clarsimp simp: updateObject_default_def in_monad 1558 projectKOs projectKO_opts_defs) 1559 apply simp 1560 done 1561 1562lemma setObject_ASID_ctes_of'[wp]: 1563 "\<lbrace>\<lambda>s. P (ctes_of s)\<rbrace> 1564 setObject ptr (asid::asidpool) 1565 \<lbrace>\<lambda>rv s. P (ctes_of s)\<rbrace>" 1566 by (rule ctes_of_from_cte_wp_at [where Q=\<top>, simplified]) wp 1567 1568lemma loadWordUser_inv : 1569 "\<lbrace>P\<rbrace> loadWordUser p \<lbrace>\<lambda>_. P\<rbrace>" 1570 unfolding loadWordUser_def 1571 by (wp dmo_inv' loadWord_inv stateAssert_wp | simp)+ 1572 1573lemma clearMemory_vms': 1574 "valid_machine_state' s \<Longrightarrow> 1575 \<forall>x\<in>fst (clearMemory ptr bits (ksMachineState s)). 1576 valid_machine_state' (s\<lparr>ksMachineState := snd x\<rparr>)" 1577 apply (clarsimp simp: valid_machine_state'_def 1578 disj_commute[of "pointerInUserData p s" for p s]) 1579 apply (drule_tac x=p in spec, simp) 1580 apply (drule_tac P4="\<lambda>m'. underlying_memory m' p = 0" 1581 in use_valid[where P=P and Q="\<lambda>_. P" for P], simp_all) 1582 apply (rule clearMemory_um_eq_0) 1583 done 1584 1585lemma ct_not_inQ_ksMachineState_update[simp]: 1586 "ct_not_inQ (s\<lparr>ksMachineState := v\<rparr>) = ct_not_inQ s" 1587 by (simp add: ct_not_inQ_def) 1588 1589lemma ct_in_current_domain_ksMachineState_update[simp]: 1590 "ct_idle_or_in_cur_domain' (s\<lparr>ksMachineState := v\<rparr>) = ct_idle_or_in_cur_domain' s" 1591 by (simp add: ct_idle_or_in_cur_domain'_def tcb_in_cur_domain'_def) 1592 1593lemma dmo_clearMemory_invs'[wp]: 1594 "\<lbrace>invs'\<rbrace> doMachineOp (clearMemory w sz) \<lbrace>\<lambda>_. invs'\<rbrace>" 1595 apply (simp add: doMachineOp_def split_def) 1596 apply wp 1597 apply (clarsimp simp: invs'_def valid_state'_def) 1598 apply (rule conjI) 1599 apply (simp add: valid_irq_masks'_def, elim allEI, clarsimp) 1600 apply (drule use_valid) 1601 apply (rule no_irq_clearMemory[simplified no_irq_def, rule_format]) 1602 apply simp_all 1603 apply (drule clearMemory_vms') 1604 apply fastforce 1605 done 1606 1607end 1608end 1609