1(* 2 * Copyright 2014, General Dynamics C4 Systems 3 * 4 * This software may be distributed and modified according to the terms of 5 * the GNU General Public License version 2. Note that NO WARRANTY is provided. 6 * See "LICENSE_GPLv2.txt" for details. 7 * 8 * @TAG(GD_GPL) 9 *) 10 11theory VSpace_C 12imports TcbAcc_C CSpace_C PSpace_C TcbQueue_C 13begin 14 15context begin interpretation Arch . (*FIXME: arch_split*) 16 17lemma ccorres_name_pre_C: 18 "(\<And>s. s \<in> P' \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf P {s} hs f g) 19 \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf P P' hs f g" 20 apply (rule ccorres_guard_imp) 21 apply (rule_tac xf'=id in ccorres_abstract, rule ceqv_refl) 22 apply (rule_tac P="rv' \<in> P'" in ccorres_gen_asm2) 23 apply assumption 24 apply simp 25 apply simp 26 done 27 28lemma ccorres_flip_Guard: 29 assumes cc: "ccorres_underlying sr \<Gamma> r xf arrel axf A C hs a (Guard F S (Guard F1 S1 c))" 30 shows "ccorres_underlying sr \<Gamma> r xf arrel axf A C hs a (Guard F1 S1 (Guard F S c))" 31 apply (rule ccorres_name_pre_C) 32 using cc 33 apply (case_tac "s \<in> (S1 \<inter> S)") 34 apply (clarsimp simp: ccorres_underlying_def) 35 apply (erule exec_handlers.cases; 36 fastforce elim!: exec_Normal_elim_cases intro: exec_handlers.intros exec.Guard) 37 apply (clarsimp simp: ccorres_underlying_def) 38 apply (case_tac "s \<in> S") 39 apply (fastforce intro: exec.Guard exec.GuardFault exec_handlers.intros) 40 apply (fastforce intro: exec.Guard exec.GuardFault exec_handlers.intros) 41 done 42 43(* FIXME: move *) 44lemma empty_fail_findPDForASID[iff]: 45 "empty_fail (findPDForASID asid)" 46 apply (simp add: findPDForASID_def liftME_def) 47 apply (intro empty_fail_bindE, simp_all split: option.split) 48 apply (simp add: assertE_def split: if_split) 49 apply (simp add: assertE_def split: if_split) 50 apply (simp add: empty_fail_getObject) 51 apply (simp add: assertE_def liftE_bindE checkPDAt_def split: if_split) 52 done 53 54(* FIXME: move *) 55lemma empty_fail_findPDForASIDAssert[iff]: 56 "empty_fail (findPDForASIDAssert asid)" 57 apply (simp add: findPDForASIDAssert_def catch_def 58 checkPDAt_def checkPDUniqueToASID_def 59 checkPDASIDMapMembership_def) 60 apply (intro empty_fail_bind, simp_all split: sum.split) 61 done 62 63 64end 65 66context kernel_m begin 67 68(* FIXME move, depends on setObject_modify which lives in kernel_m *) 69lemma setObject_modify: 70 fixes v :: "'a :: pspace_storable" shows 71 "\<lbrakk> obj_at' (P :: 'a \<Rightarrow> bool) p s; updateObject v = updateObject_default v; 72 (1 :: word32) < 2 ^ objBits v \<rbrakk> 73 \<Longrightarrow> setObject p v s 74 = modify (ksPSpace_update (\<lambda>ps. ps (p \<mapsto> injectKO v))) s" 75 apply (clarsimp simp: setObject_def split_def exec_gets 76 obj_at'_def projectKOs lookupAround2_known1 77 assert_opt_def updateObject_default_def 78 bind_assoc) 79 apply (simp add: projectKO_def alignCheck_assert) 80 apply (simp add: project_inject objBits_def) 81 apply (clarsimp simp only: objBitsT_koTypeOf[symmetric] koTypeOf_injectKO) 82 apply (frule(2) in_magnitude_check[where s'=s]) 83 apply (simp add: magnitudeCheck_assert in_monad) 84 apply (simp add: simpler_modify_def) 85 done 86 87lemma pageBitsForSize_le: 88 "pageBitsForSize x \<le> 25" 89 by (simp add: pageBitsForSize_def split: vmpage_size.splits) 90 91lemma unat_of_nat_pageBitsForSize [simp]: 92 "unat (of_nat (pageBitsForSize x)::word32) = pageBitsForSize x" 93 apply (subst unat_of_nat32) 94 apply (rule order_le_less_trans, rule pageBitsForSize_le) 95 apply (simp add: word_bits_def) 96 apply simp 97 done 98 99lemma checkVPAlignment_ccorres: 100 "ccorres (\<lambda>a c. if to_bool c then a = Inr () else a = Inl AlignmentError) ret__unsigned_long_' 101 \<top> 102 (UNIV \<inter> \<lbrace>sz = gen_framesize_to_H \<acute>sz \<and> \<acute>sz && mask 2 = \<acute>sz\<rbrace> \<inter> \<lbrace>\<acute>w = w\<rbrace>) 103 [] 104 (checkVPAlignment sz w) 105 (Call checkVPAlignment_'proc)" 106proof - 107 note [split del] = if_split 108 show ?thesis 109 apply (cinit lift: sz_' w_') 110 apply (csymbr) 111 apply clarsimp 112 apply (rule ccorres_Guard [where A=\<top> and C'=UNIV]) 113 apply (simp split: if_split) 114 apply (rule conjI) 115 apply (clarsimp simp: mask_def unlessE_def returnOk_def) 116 apply (rule ccorres_guard_imp) 117 apply (rule ccorres_return_C) 118 apply simp 119 apply simp 120 apply simp 121 apply simp 122 apply (simp split: if_split add: to_bool_def) 123 apply (clarsimp simp: mask_def unlessE_def throwError_def split: if_split) 124 apply (rule ccorres_guard_imp) 125 apply (rule ccorres_return_C) 126 apply simp 127 apply simp 128 apply simp 129 apply simp 130 apply (simp split: if_split add: to_bool_def) 131 apply (clarsimp split: if_split) 132 apply (simp add: word_less_nat_alt) 133 apply (rule order_le_less_trans, rule pageBitsForSize_le) 134 apply simp 135 done 136qed 137 138 139lemma rf_asidTable: 140 "\<lbrakk> (\<sigma>, x) \<in> rf_sr; valid_arch_state' \<sigma>; idx \<le> mask asid_high_bits \<rbrakk> 141 \<Longrightarrow> case armKSASIDTable (ksArchState \<sigma>) 142 idx of 143 None \<Rightarrow> 144 index (armKSASIDTable_' (globals x)) (unat idx) = 145 NULL 146 | Some v \<Rightarrow> 147 index (armKSASIDTable_' (globals x)) (unat idx) = Ptr v \<and> 148 index (armKSASIDTable_' (globals x)) (unat idx) \<noteq> NULL" 149 apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def 150 carch_state_relation_def 151 array_relation_def) 152 apply (drule_tac x=idx in spec)+ 153 apply (clarsimp simp: mask_def split: option.split) 154 apply (drule sym, simp) 155 apply (simp add: option_to_ptr_def option_to_0_def) 156 apply (clarsimp simp: invs'_def valid_state'_def valid_arch_state'_def 157 valid_asid_table'_def ran_def) 158 done 159 160lemma getKSASIDTable_ccorres_stuff: 161 "\<lbrakk> invs' \<sigma>; (\<sigma>, x) \<in> rf_sr; idx' = unat idx; 162 idx < 2 ^ asid_high_bits \<rbrakk> 163 \<Longrightarrow> case armKSASIDTable (ksArchState \<sigma>) 164 idx of 165 None \<Rightarrow> 166 index (armKSASIDTable_' (globals x)) 167 idx' = 168 NULL 169 | Some v \<Rightarrow> 170 index (armKSASIDTable_' (globals x)) 171 idx' = Ptr v \<and> 172 index (armKSASIDTable_' (globals x)) 173 idx' \<noteq> NULL" 174 apply (drule rf_asidTable [where idx=idx]) 175 apply fastforce 176 apply (simp add: mask_def) 177 apply (simp add: minus_one_helper3) 178 apply (clarsimp split: option.splits) 179 done 180 181lemma asidLowBits_handy_convs: 182 "sint Kernel_C.asidLowBits = 10" 183 "Kernel_C.asidLowBits \<noteq> 0x20" 184 "unat Kernel_C.asidLowBits = asid_low_bits" 185 by (simp add: Kernel_C.asidLowBits_def asid_low_bits_def)+ 186 187lemma rf_sr_armKSASIDTable: 188 "\<lbrakk> (s, s') \<in> rf_sr; n \<le> 2 ^ asid_high_bits - 1 \<rbrakk> 189 \<Longrightarrow> index (armKSASIDTable_' (globals s')) (unat n) 190 = option_to_ptr (armKSASIDTable (ksArchState s) n)" 191 by (clarsimp simp: rf_sr_def cstate_relation_def Let_def 192 carch_state_relation_def array_relation_def) 193 194lemma asid_high_bits_word_bits: 195 "asid_high_bits < word_bits" 196 by (simp add: asid_high_bits_def word_bits_def) 197 198lemma rf_sr_asid_map_pd_to_hwasids: 199 "(s, s') \<in> rf_sr \<Longrightarrow> 200 asid_map_pd_to_hwasids (armKSASIDMap (ksArchState s)) 201 = set_option \<circ> (pde_stored_asid \<circ>\<^sub>m cslift s' \<circ>\<^sub>m pd_pointer_to_asid_slot)" 202 by (simp add: rf_sr_def cstate_relation_def Let_def 203 carch_state_relation_def) 204 205lemma pd_at_asid_cross_over: 206 "\<lbrakk> pd_at_asid' pd asid s; asid \<le> mask asid_bits; 207 (s, s') \<in> rf_sr\<rbrakk> 208 \<Longrightarrow> \<exists>apptr ap pde. index (armKSASIDTable_' (globals s')) (unat (asid >> asid_low_bits)) 209 = (ap_Ptr apptr) \<and> cslift s' (ap_Ptr apptr) = Some (asid_pool_C ap) 210 \<and> index ap (unat (asid && 2 ^ asid_low_bits - 1)) = pde_Ptr pd 211 \<and> cslift s' (pde_Ptr (pd + 0x3FC0)) = Some pde 212 \<and> is_aligned pd pdBits 213 \<and> array_assertion (pde_Ptr pd) 2048 (hrs_htd (t_hrs_' (globals s'))) 214 \<and> (valid_pde_mappings' s \<longrightarrow> pde_get_tag pde = scast pde_pde_invalid)" 215 apply (clarsimp simp: pd_at_asid'_def) 216 apply (subgoal_tac "asid >> asid_low_bits \<le> 2 ^ asid_high_bits - 1") 217 prefer 2 218 apply (simp add: asid_high_bits_word_bits) 219 apply (rule shiftr_less_t2n) 220 apply (simp add: mask_def) 221 apply (simp add: asid_low_bits_def asid_high_bits_def asid_bits_def) 222 apply (simp add: rf_sr_armKSASIDTable) 223 apply (subgoal_tac "ucast (asid_high_bits_of asid) = asid >> asid_low_bits") 224 prefer 2 225 apply (simp add: asid_high_bits_of_def ucast_ucast_mask asid_high_bits_def[symmetric]) 226 apply (subst mask_eq_iff_w2p, simp add: asid_high_bits_def word_size) 227 apply (rule shiftr_less_t2n) 228 apply (simp add: mask_def, simp add: asid_bits_def asid_low_bits_def asid_high_bits_def) 229 apply (simp add: option_to_ptr_def option_to_0_def) 230 apply (rule cmap_relationE1 [OF rf_sr_cpspace_asidpool_relation], 231 assumption, erule ko_at_projectKO_opt) 232 apply (clarsimp simp: casid_pool_relation_def array_relation_def 233 split: asid_pool_C.split_asm) 234 apply (drule spec, drule sym [OF mp]) 235 apply (rule_tac y=asid in word_and_le1) 236 apply (frule(1) page_directory_at_rf_sr) 237 apply (clarsimp simp: mask_2pm1[symmetric] option_to_ptr_def option_to_0_def 238 page_directory_at'_def typ_at_to_obj_at_arches) 239 apply (drule_tac x="pd_asid_slot" in spec, 240 simp add: pd_asid_slot_def pt_index_bits_def' pageBits_def) 241 apply (drule obj_at_ko_at'[where 'a=pde], clarsimp) 242 apply (rule cmap_relationE1 [OF rf_sr_cpde_relation], 243 assumption, erule ko_at_projectKO_opt) 244 apply (subst array_ptr_valid_array_assertionI, erule h_t_valid_clift, simp+) 245 apply (clarsimp simp: valid_pde_mappings'_def) 246 apply (elim allE, drule(1) mp) 247 apply (simp add: valid_pde_mapping'_def valid_pde_mapping_offset'_def 248 pd_asid_slot_def mask_add_aligned table_bits_defs) 249 apply (simp add: mask_def) 250 apply (clarsimp simp add: cpde_relation_def Let_def) 251 by (simp add: pde_lift_def Let_def split: if_split_asm) 252 253lemma findPDForASIDAssert_pd_at_wp2: 254 "\<lbrace>\<lambda>s. \<forall>pd. pd_at_asid' pd asid s 255 \<and> pd \<notin> ran (option_map snd \<circ> armKSASIDMap (ksArchState s) |` (- {asid})) 256 \<and> option_map snd (armKSASIDMap (ksArchState s) asid) \<in> {None, Some pd} 257 \<longrightarrow> P pd s\<rbrace> findPDForASIDAssert asid \<lbrace>P\<rbrace>" 258 apply (rule hoare_pre) 259 apply (simp add: findPDForASIDAssert_def const_def 260 checkPDAt_def checkPDUniqueToASID_def 261 checkPDASIDMapMembership_def) 262 apply (wp findPDForASID_pd_at_wp) 263 apply clarsimp 264 apply (drule spec, erule mp) 265 apply clarsimp 266 apply (clarsimp split: option.split_asm) 267 done 268 269lemma asid_shiftr_low_bits_less: 270 "(asid :: word32) \<le> mask asid_bits \<Longrightarrow> asid >> asid_low_bits < 0x80" 271 apply (rule_tac y="2 ^ 7" in order_less_le_trans) 272 apply (rule shiftr_less_t2n) 273 apply (simp add: le_mask_iff_lt_2n[THEN iffD1] asid_bits_def asid_low_bits_def) 274 apply simp 275 done 276 277lemma loadHWASID_ccorres: 278 "ccorres (\<lambda>a b. a = pde_stored_asid b \<and> pde_get_tag b = scast pde_pde_invalid) 279 ret__struct_pde_C_' 280 (valid_pde_mappings' and (\<lambda>_. asid \<le> mask asid_bits)) (UNIV \<inter> {s. asid_' s = asid}) [] 281 (loadHWASID asid) (Call loadHWASID_'proc)" 282 apply (rule ccorres_gen_asm) 283 apply (cinit lift: asid_') 284 apply (rule ccorres_Guard_Seq)+ 285 apply (rule ccorres_symb_exec_l [OF _ _ _ empty_fail_gets]) 286 apply (rule ccorres_symb_exec_l [OF _ _ _ empty_fail_findPDForASIDAssert]) 287 apply (rename_tac pd) 288 apply (rule_tac P="\<lambda>s. pd_at_asid' pd asid s \<and> rv = armKSASIDMap (ksArchState s) 289 \<and> pd \<notin> ran (option_map snd o armKSASIDMap (ksArchState s) 290 |` (- {asid})) 291 \<and> option_map snd (armKSASIDMap (ksArchState s) asid) \<in> {None, Some pd} 292 \<and> valid_pde_mappings' s" 293 in ccorres_from_vcg_throws[where P'=UNIV]) 294 apply (rule allI, rule conseqPre, vcg) 295 apply (clarsimp simp: return_def) 296 apply (frule(2) pd_at_asid_cross_over) 297 apply (clarsimp simp: asidLowBits_handy_convs word_sless_def word_sle_def) 298 apply (clarsimp simp: typ_heap_simps order_le_less_trans[OF word_and_le1] 299 array_assertion_shrink_right ptr_add_assertion_def 300 arg_cong[where f="\<lambda>x. 2 ^ x", OF meta_eq_to_obj_eq, OF asid_low_bits_def]) 301 apply (clarsimp split: option.split) 302 apply (frule_tac x=pd in fun_cong [OF rf_sr_asid_map_pd_to_hwasids]) 303 apply (simp add: asid_map_pd_to_hwasids_def 304 pd_pointer_to_asid_slot_def) 305 apply (intro conjI allI impI) 306 apply (rule ccontr, clarsimp) 307 apply (drule singleton_eqD) 308 apply (clarsimp elim!: ranE) 309 apply (erule notE, rule_tac a=xa in ranI) 310 apply (simp add: restrict_map_def split: if_split) 311 apply clarsimp 312 apply clarsimp 313 apply (drule_tac x=a in eqset_imp_iff) 314 apply (drule iffD1) 315 apply fastforce 316 apply simp 317 apply wp[1] 318 apply (rule findPDForASIDAssert_pd_at_wp2) 319 apply wp+ 320 apply (clarsimp simp: asidLowBits_handy_convs word_sless_def word_sle_def 321 Collect_const_mem asid_shiftr_low_bits_less) 322 done 323 324lemma array_relation_update: 325 "\<lbrakk> array_relation R bnd table (arr :: 'a['b :: finite]); 326 x' = unat (x :: ('td :: len) word); R v v'; 327 unat bnd < card (UNIV :: 'b set) \<rbrakk> 328 \<Longrightarrow> array_relation R bnd (table (x := v)) 329 (Arrays.update arr x' v')" 330 by (simp add: array_relation_def word_le_nat_alt split: if_split) 331 332lemma asid_map_pd_to_hwasids_update: 333 "\<lbrakk> pd \<notin> ran (option_map snd \<circ> m |` (- {asid})); 334 \<forall>hw_asid pd'. m asid = Some (hw_asid, pd') \<longrightarrow> pd' = pd \<rbrakk> \<Longrightarrow> 335 asid_map_pd_to_hwasids (m (asid \<mapsto> (hw_asid, pd))) 336 = (asid_map_pd_to_hwasids m) (pd := {hw_asid})" 337 apply (rule ext, rule set_eqI) 338 apply (simp add: asid_map_pd_to_hwasids_def split: if_split) 339 apply (intro conjI impI) 340 apply (rule iffI) 341 apply (rule ccontr, clarsimp elim!: ranE split: if_split_asm) 342 apply (erule notE, rule ranI, simp add: restrict_map_def) 343 apply (subst if_P, assumption) 344 apply simp 345 apply (fastforce split: if_split) 346 apply (simp add: ran_def split: if_split) 347 apply (rule iffI) 348 apply fastforce 349 apply (erule exEI) 350 apply clarsimp 351 done 352 353lemma storeHWASID_ccorres: 354 "ccorres dc xfdc (valid_pde_mappings' and (\<lambda>_. asid \<le> mask asid_bits)) 355 (UNIV \<inter> {s. asid_' s = asid} \<inter> {s. hw_asid_' s = ucast hw_asid}) [] 356 (storeHWASID asid hw_asid) (Call storeHWASID_'proc)" 357 apply (rule ccorres_gen_asm) 358 apply (cinit lift: asid_' hw_asid_') 359 apply (rule ccorres_Guard_Seq)+ 360 apply (rule ccorres_symb_exec_l [OF _ _ _ empty_fail_findPDForASIDAssert]) 361 apply (rename_tac pd) 362 apply (rule_tac P="\<lambda>s. pd_at_asid' pd asid s 363 \<and> pd \<notin> ran (option_map snd o armKSASIDMap (ksArchState s) 364 |` (- {asid})) 365 \<and> option_map snd (armKSASIDMap (ksArchState s) asid) \<in> {None, Some pd} 366 \<and> valid_pde_mappings' s" 367 in ccorres_from_vcg[where P'=UNIV]) 368 apply (rule allI, rule conseqPre, vcg) 369 apply (clarsimp simp: Collect_const_mem word_sle_def word_sless_def 370 asidLowBits_handy_convs simpler_gets_def 371 simpler_modify_def bind_def) 372 apply (frule(2) pd_at_asid_cross_over) 373 apply (clarsimp simp: typ_heap_simps) 374 apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def 375 cpspace_relation_def) 376 apply (clarsimp simp: typ_heap_simps cmachine_state_relation_def 377 carch_state_relation_def pd_at_asid'_def 378 fun_upd_def[symmetric] carch_globals_def 379 order_le_less_trans[OF word_and_le1] 380 ptr_add_assertion_positive 381 array_assertion_shrink_right 382 arg_cong[where f="\<lambda>x. 2 ^ x", OF meta_eq_to_obj_eq, OF asid_low_bits_def]) 383 apply (subgoal_tac "ucast hw_asid <s (256 :: sword32) \<and> ucast hw_asid < (256 :: sword32) 384 \<and> (0 :: sword32) <=s ucast hw_asid") 385 prefer 2 386 subgoal by (simp add: word_sless_msb_less ucast_less[THEN order_less_le_trans] 387 word_0_sle_from_less) 388 apply (simp add: word_sless_def word_sle_def cslift_ptr_safe) 389 apply (intro conjI) 390 apply (erule iffD1 [OF cmap_relation_cong, rotated -1], simp_all)[1] 391 apply (simp split: if_split_asm) 392 apply (clarsimp simp: cpde_relation_def Let_def 393 pde_lift_pde_invalid 394 cong: ARM_HYP_H.pde.case_cong) 395 apply (erule array_relation_update) 396 subgoal by simp 397 subgoal by (simp add: option_to_0_def) 398 subgoal by simp 399 apply (subst asid_map_pd_to_hwasids_update, assumption) 400 subgoal by clarsimp 401 apply (rule ext, simp add: pd_pointer_to_asid_slot_def map_comp_def split: if_split) 402 apply (clarsimp simp: pde_stored_asid_def true_def mask_def[where n="Suc 0"]) 403 apply (subst less_mask_eq) 404 apply (rule order_less_le_trans, rule ucast_less) 405 subgoal by simp 406 subgoal by simp 407 apply (subst ucast_up_ucast_id) 408 subgoal by (simp add: is_up_def source_size_def target_size_def word_size) 409 subgoal by simp 410 apply wp[1] 411 apply (rule findPDForASIDAssert_pd_at_wp2) 412 apply (clarsimp simp: asidLowBits_handy_convs word_sle_def word_sless_def 413 Collect_const_mem asid_shiftr_low_bits_less) 414 done 415 416lemma invalidateHWASIDEntry_ccorres: 417 "hwasid' = unat hwasid \<Longrightarrow> 418 ccorres dc xfdc \<top> UNIV 419 [] (invalidateHWASIDEntry hwasid) 420 (Basic (\<lambda>s. globals_update ( 421 armKSHWASIDTable_'_update 422 (\<lambda>_. Arrays.update (armKSHWASIDTable_' (globals s)) 423 hwasid' (scast asidInvalid))) s))" 424 apply (clarsimp simp: invalidateHWASIDEntry_def) 425 apply (rule ccorres_from_vcg) 426 apply (rule allI, rule conseqPre, vcg) 427 apply (clarsimp simp: bind_def simpler_gets_def 428 simpler_modify_def) 429 apply (clarsimp simp: rf_sr_def cstate_relation_def 430 Let_def) 431 apply (clarsimp simp: carch_state_relation_def carch_globals_def 432 cmachine_state_relation_def) 433 apply (simp add: array_relation_def split: if_split, erule allEI) 434 apply (clarsimp simp: word_le_nat_alt) 435 apply (simp add: option_to_0_def asidInvalid_def) 436 done 437 438lemma asid_map_pd_to_hwasids_clear: 439 "\<lbrakk> pd \<notin> ran (option_map snd \<circ> m |` (- {asid})); 440 \<forall>hw_asid pd'. m asid = Some (hw_asid, pd') \<longrightarrow> pd' = pd \<rbrakk> \<Longrightarrow> 441 asid_map_pd_to_hwasids (m (asid := None)) 442 = (asid_map_pd_to_hwasids m) (pd := {})" 443 apply (rule ext, rule set_eqI) 444 apply (simp add: asid_map_pd_to_hwasids_def split: if_split) 445 apply (intro conjI impI) 446 apply (clarsimp elim!: ranE split: if_split_asm) 447 apply (erule notE, rule ranI, simp add: restrict_map_def) 448 apply (subst if_P, assumption) 449 apply simp 450 apply (simp add: ran_def split: if_split) 451 apply (rule iffI) 452 apply fastforce 453 apply (erule exEI) 454 apply clarsimp 455 done 456 457lemma invalidateASID_ccorres: 458 "ccorres dc xfdc (valid_pde_mappings' and (\<lambda>_. asid \<le> mask asid_bits)) 459 (UNIV \<inter> {s. asid_' s = asid}) [] 460 (invalidateASID asid) (Call invalidateASID_'proc)" 461 apply (rule ccorres_gen_asm) 462 apply (cinit lift: asid_') 463 apply (rule ccorres_Guard_Seq)+ 464 apply (rule ccorres_symb_exec_l [OF _ _ _ empty_fail_findPDForASIDAssert]) 465 apply (rename_tac pd) 466 apply (rule_tac P="\<lambda>s. pd_at_asid' pd asid s \<and> valid_pde_mappings' s 467 \<and> pd \<notin> ran (option_map snd o armKSASIDMap (ksArchState s) 468 |` (- {asid})) 469 \<and> option_map snd (armKSASIDMap (ksArchState s) asid) \<in> {None, Some pd}" 470 in ccorres_from_vcg[where P'=UNIV]) 471 apply (rule allI, rule conseqPre, vcg) 472 apply (clarsimp simp: Collect_const_mem word_sle_def word_sless_def 473 asidLowBits_handy_convs simpler_gets_def 474 simpler_modify_def bind_def) 475 apply (frule(2) pd_at_asid_cross_over) 476 apply (clarsimp simp: typ_heap_simps) 477 apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def 478 cpspace_relation_def 479 ptr_add_assertion_positive 480 array_assertion_shrink_right) 481 apply (clarsimp simp: typ_heap_simps cmachine_state_relation_def 482 carch_state_relation_def pd_at_asid'_def carch_globals_def 483 fun_upd_def[symmetric] order_le_less_trans[OF word_and_le1] 484 arg_cong[where f="\<lambda>x. 2 ^ x", OF meta_eq_to_obj_eq, OF asid_low_bits_def]) 485 apply (intro conjI) 486 apply (erule iffD1 [OF cmap_relation_cong, rotated -1], simp_all)[1] 487 apply (simp split: if_split_asm) 488 apply (clarsimp simp: cpde_relation_def Let_def 489 pde_lift_pde_invalid 490 cong: ARM_HYP_H.pde.case_cong) 491 apply (subst asid_map_pd_to_hwasids_clear, assumption) 492 subgoal by clarsimp 493 apply (rule ext, simp add: pd_pointer_to_asid_slot_def map_comp_def split: if_split) 494 subgoal by (clarsimp simp: pde_stored_asid_def false_def mask_def[where n="Suc 0"]) 495 apply wp[1] 496 apply (wp findPDForASIDAssert_pd_at_wp2) 497 apply (clarsimp simp: asidLowBits_handy_convs word_sle_def word_sless_def 498 asid_shiftr_low_bits_less) 499 done 500 501definition 502 "vm_fault_type_from_H fault \<equiv> 503 case fault of 504 vmfault_type.ARMDataAbort \<Rightarrow> (scast Kernel_C.ARMDataAbort :: word32) 505 | vmfault_type.ARMPrefetchAbort \<Rightarrow> scast Kernel_C.ARMPrefetchAbort" 506 507 508lemma handleVMFault_ccorres: 509 "ccorres ((\<lambda>a ex v. ex = scast EXCEPTION_FAULT \<and> (\<exists>vf. 510 a = ArchFault (VMFault (seL4_Fault_VMFault_CL.address_CL vf) [instructionFault_CL vf, FSR_CL vf]) \<and> 511 errfault v = Some (SeL4_Fault_VMFault vf))) \<currency> 512 (\<lambda>_. \<bottom>)) 513 (liftxf errstate id (K ()) ret__unsigned_long_') 514 \<top> 515 (UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace> \<inter> \<lbrace>\<acute>vm_faultType = vm_fault_type_from_H vm_fault\<rbrace>) 516 [] 517 (handleVMFault thread vm_fault) 518 (Call handleVMFault_'proc)" 519 apply (cinit lift: vm_faultType_') 520 apply wpc 521 apply (simp add: vm_fault_type_from_H_def Kernel_C.ARMDataAbort_def Kernel_C.ARMPrefetchAbort_def) 522 apply (simp add: ccorres_cond_univ_iff) 523 apply (rule ccorres_rhs_assoc)+ 524 apply csymbr 525 apply csymbr 526 apply (ctac (no_vcg) add: getHDFAR_ccorres pre: ccorres_liftE_Seq) 527 apply (ctac (no_vcg) add: addressTranslateS1CPR_ccorres pre: ccorres_liftE_Seq) 528 apply csymbr 529 apply (ctac (no_vcg) add: getHSR_ccorres pre: ccorres_liftE_Seq) 530 apply csymbr 531 apply (clarsimp simp: pageBits_def) 532 apply (rule ccorres_from_vcg_throws [where P=\<top> and P'=UNIV]) 533 apply (clarsimp simp add: throwError_def return_def) 534 apply (rule conseqPre) 535 apply vcg 536 apply (clarsimp simp: errstate_def EXCEPTION_FAULT_def EXCEPTION_NONE_def) 537 apply (wpsimp simp: seL4_Fault_VMFault_lift false_def mask_def)+ 538 apply (simp add: vm_fault_type_from_H_def Kernel_C.ARMDataAbort_def Kernel_C.ARMPrefetchAbort_def) 539 apply (simp add: ccorres_cond_univ_iff ccorres_cond_empty_iff) 540 apply (rule ccorres_rhs_assoc)+ 541 apply csymbr 542 apply csymbr 543 apply (ctac (no_vcg) pre: ccorres_liftE_Seq) 544 apply (ctac (no_vcg) add: addressTranslateS1CPR_ccorres pre: ccorres_liftE_Seq) 545 apply csymbr 546 apply (ctac (no_vcg) add: getHSR_ccorres pre: ccorres_liftE_Seq) 547 apply csymbr 548 apply (clarsimp simp: pageBits_def) 549 apply (rule ccorres_from_vcg_throws [where P=\<top> and P'=UNIV]) 550 apply (clarsimp simp add: throwError_def return_def) 551 apply (rule conseqPre) 552 apply vcg 553 apply (clarsimp simp: errstate_def EXCEPTION_FAULT_def EXCEPTION_NONE_def) 554 apply (wpsimp simp: seL4_Fault_VMFault_lift true_def mask_def)+ 555 done 556 557lemma unat_asidLowBits [simp]: 558 "unat Kernel_C.asidLowBits = asidLowBits" 559 by (simp add: asidLowBits_def Kernel_C.asidLowBits_def asid_low_bits_def) 560 561lemma rf_sr_asidTable_None: 562 "\<lbrakk> (\<sigma>, x) \<in> rf_sr; asid && mask asid_bits = asid; valid_arch_state' \<sigma> \<rbrakk> \<Longrightarrow> 563 (index (armKSASIDTable_' (globals x)) (unat (asid >> asid_low_bits)) = ap_Ptr 0) = 564 (armKSASIDTable (ksArchState \<sigma>) (ucast (asid_high_bits_of asid)) = None)" 565 apply (simp add: asid_high_bits_of_def ucast_ucast_mask) 566 apply (subgoal_tac "(asid >> asid_low_bits) && mask 7 = asid >> asid_low_bits")(*asid_low_bits*) 567 prefer 2 568 apply (rule word_eqI) 569 apply (subst (asm) bang_eq) 570 apply (simp add: word_size nth_shiftr asid_bits_def asid_low_bits_def) 571 apply (case_tac "n < 7", simp) (*asid_low_bits*) 572 apply (clarsimp simp: linorder_not_less) 573 apply (erule_tac x="n+10" in allE) 574 apply simp 575 apply simp 576 apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def carch_state_relation_def) 577 apply (simp add: array_relation_def option_to_0_def) 578 apply (erule_tac x="asid >> asid_low_bits" in allE) 579 apply (erule impE) 580 prefer 2 581 apply (drule sym [where t="index a b" for a b]) 582 apply (simp add: option_to_0_def option_to_ptr_def split: option.splits) 583 apply (clarsimp simp: valid_arch_state'_def valid_asid_table'_def ran_def) 584 apply (simp add: and_mask_eq_iff_le_mask) 585 apply (simp add: asid_high_bits_def mask_def) 586 done 587 588lemma leq_asid_bits_shift: 589 "x \<le> mask asid_bits 590 \<Longrightarrow> (x :: word32) >> asid_low_bits \<le> mask asid_high_bits" 591 by (simp add: leq_mask_shift asid_bits_def asid_low_bits_def asid_high_bits_def) 592 593lemma ucast_asid_high_bits_is_shift: 594 "asid \<le> mask asid_bits 595 \<Longrightarrow> ucast (asid_high_bits_of asid) = (asid >> asid_low_bits)" 596 unfolding asid_bits_def asid_low_bits_def asid_high_bits_of_def 597 by (rule ucast_ucast_eq_mask_shift, simp) 598 599lemma cap_small_frame_cap_get_capFMappedASID_spec: 600 "\<forall>s. \<Gamma>\<turnstile> \<lbrace>s. cap_get_tag \<acute>cap = scast cap_small_frame_cap\<rbrace> 601 Call cap_small_frame_cap_get_capFMappedASID_'proc 602 \<lbrace>\<acute>ret__unsigned_long = 603 (cap_small_frame_cap_CL.capFMappedASIDHigh_CL (cap_small_frame_cap_lift \<^bsup>s\<^esup>cap) << asidLowBits) 604 + (cap_small_frame_cap_CL.capFMappedASIDLow_CL (cap_small_frame_cap_lift \<^bsup>s\<^esup>cap))\<rbrace>" 605 apply vcg 606 apply (clarsimp simp: asidLowBits_def Kernel_C.asidLowBits_def word_sle_def 607 asid_low_bits_def) 608 done 609 610lemma cap_frame_cap_get_capFMappedASID_spec: 611 "\<forall>s. \<Gamma>\<turnstile> \<lbrace>s. cap_get_tag \<acute>cap = scast cap_frame_cap\<rbrace> 612 Call cap_frame_cap_get_capFMappedASID_'proc 613 \<lbrace>\<acute>ret__unsigned_long = 614 (cap_frame_cap_CL.capFMappedASIDHigh_CL (cap_frame_cap_lift \<^bsup>s\<^esup>cap) << asidLowBits) 615 + (cap_frame_cap_CL.capFMappedASIDLow_CL (cap_frame_cap_lift \<^bsup>s\<^esup>cap))\<rbrace>" 616 apply vcg 617 apply (clarsimp simp: asidLowBits_def Kernel_C.asidLowBits_def word_sle_def 618 asid_low_bits_def) 619 done 620 621 622 623definition 624 generic_frame_cap_get_capFMappedASID_CL :: "cap_CL option \<Rightarrow> word32" where 625 "generic_frame_cap_get_capFMappedASID_CL \<equiv> \<lambda>cap. case cap of 626 Some (Cap_small_frame_cap c) \<Rightarrow> 627 (cap_small_frame_cap_CL.capFMappedASIDHigh_CL c << asidLowBits) 628 + (cap_small_frame_cap_CL.capFMappedASIDLow_CL c) 629 | Some (Cap_frame_cap c) \<Rightarrow> 630 (cap_frame_cap_CL.capFMappedASIDHigh_CL c << asidLowBits) 631 + (cap_frame_cap_CL.capFMappedASIDLow_CL c) 632 | Some _ \<Rightarrow> 0" 633 634lemma generic_frame_cap_get_capFMappedASID_spec: 635 "\<forall>s. \<Gamma> \<turnstile> \<lbrace>s. cap_get_tag \<acute>cap = scast cap_small_frame_cap \<or> 636 cap_get_tag \<acute>cap = scast cap_frame_cap\<rbrace> 637 Call generic_frame_cap_get_capFMappedASID_'proc 638 \<lbrace>\<acute>ret__unsigned_long = generic_frame_cap_get_capFMappedASID_CL (cap_lift \<^bsup>s\<^esup>cap)\<rbrace>" 639 apply vcg 640 apply (clarsimp simp: generic_frame_cap_get_capFMappedASID_CL_def Kernel_C.asidLowBits_def word_sle_def ) 641 642 apply (intro conjI impI, simp_all) 643 apply (clarsimp simp: cap_lift_small_frame_cap cap_small_frame_cap_lift_def) 644 apply (clarsimp simp: cap_lift_frame_cap cap_frame_cap_lift_def) 645 done 646 647 648lemma generic_frame_cap_get_capFIsMapped_spec: 649 "\<forall>s. \<Gamma> \<turnstile> \<lbrace>s. cap_get_tag \<acute>cap = scast cap_small_frame_cap \<or> 650 cap_get_tag \<acute>cap = scast cap_frame_cap\<rbrace> 651 Call generic_frame_cap_get_capFIsMapped_'proc 652 \<lbrace>\<acute>ret__unsigned_long = (if generic_frame_cap_get_capFMappedASID_CL (cap_lift \<^bsup>s\<^esup>cap) \<noteq> 0 then 1 else 0)\<rbrace>" 653 apply vcg 654 apply (clarsimp simp: generic_frame_cap_get_capFMappedASID_CL_def if_distrib [where f=scast]) 655done 656 657 658 659 660definition 661 generic_frame_cap_get_capFMappedAddress_CL :: "cap_CL option \<Rightarrow> word32" where 662 "generic_frame_cap_get_capFMappedAddress_CL \<equiv> \<lambda>cap. case cap of 663 Some (Cap_small_frame_cap c) \<Rightarrow> cap_small_frame_cap_CL.capFMappedAddress_CL c 664 | Some (Cap_frame_cap c) \<Rightarrow> cap_frame_cap_CL.capFMappedAddress_CL c 665 | Some _ \<Rightarrow> 0" 666 667lemma generic_frame_cap_get_capFMappedAddress_spec: 668 "\<forall>s. \<Gamma> \<turnstile> \<lbrace>s. cap_get_tag \<acute>cap = scast cap_small_frame_cap \<or> 669 cap_get_tag \<acute>cap = scast cap_frame_cap\<rbrace> 670 Call generic_frame_cap_get_capFMappedAddress_'proc 671 \<lbrace>\<acute>ret__unsigned_long = generic_frame_cap_get_capFMappedAddress_CL (cap_lift \<^bsup>s\<^esup>cap)\<rbrace>" 672 apply vcg 673 apply (clarsimp simp: generic_frame_cap_get_capFMappedAddress_CL_def) 674 apply (auto simp: cap_lift_small_frame_cap cap_small_frame_cap_lift_def 675 cap_lift_frame_cap cap_frame_cap_lift_def) 676done 677 678 679 680definition 681 generic_frame_cap_set_capFMappedAddress_CL :: "cap_CL option \<Rightarrow> word32 \<Rightarrow> word32 \<Rightarrow> cap_CL option " where 682 "generic_frame_cap_set_capFMappedAddress_CL \<equiv> \<lambda>cap asid addr. case cap of 683 Some (Cap_small_frame_cap c) \<Rightarrow> 684 Some ( Cap_small_frame_cap 685 (c \<lparr> cap_small_frame_cap_CL.capFMappedASIDHigh_CL := (asid >> asidLowBits) && mask asidHighBits, 686 cap_small_frame_cap_CL.capFMappedASIDLow_CL := asid && mask asidLowBits, 687 cap_small_frame_cap_CL.capFMappedAddress_CL := addr AND NOT (mask 12) \<rparr>)) 688 | Some (Cap_frame_cap c) \<Rightarrow> 689 Some ( Cap_frame_cap 690 (c \<lparr> cap_frame_cap_CL.capFMappedASIDHigh_CL := (asid >> asidLowBits) && mask asidHighBits, 691 cap_frame_cap_CL.capFMappedASIDLow_CL := asid && mask asidLowBits, 692 cap_frame_cap_CL.capFMappedAddress_CL := addr AND NOT (mask 14) \<rparr>)) 693 | Some ccap \<Rightarrow> Some ccap" 694 695 696lemma generic_frame_cap_set_capFMappedAddress_spec: 697 "\<forall>s. \<Gamma> \<turnstile> \<lbrace>s. cap_get_tag \<acute>cap = scast cap_small_frame_cap \<or> 698 cap_get_tag \<acute>cap = scast cap_frame_cap\<rbrace> 699 Call generic_frame_cap_set_capFMappedAddress_'proc 700 \<lbrace> cap_lift \<acute>ret__struct_cap_C 701 = generic_frame_cap_set_capFMappedAddress_CL (cap_lift \<^bsup>s\<^esup>cap) (\<^bsup>s\<^esup>asid ) (\<^bsup>s\<^esup>addr ) \<rbrace>" 702 apply vcg 703 apply (clarsimp simp: generic_frame_cap_set_capFMappedAddress_CL_def) 704 apply (intro conjI impI) 705 by (clarsimp simp: cap_lift_small_frame_cap cap_small_frame_cap_lift_def 706 cap_lift_frame_cap cap_frame_cap_lift_def)+ 707 708lemma clift_ptr_safe: 709 "clift (h, x) ptr = Some a 710 \<Longrightarrow> ptr_safe ptr x" 711 by (erule lift_t_ptr_safe[where g = c_guard]) 712 713lemma clift_ptr_safe2: 714 "clift htd ptr = Some a 715 \<Longrightarrow> ptr_safe ptr (hrs_htd htd)" 716 by (cases htd, simp add: hrs_htd_def clift_ptr_safe) 717 718lemma generic_frame_cap_ptr_set_capFMappedAddress_spec: 719 "\<forall>s cte_slot. 720 \<Gamma> \<turnstile> \<lbrace>s. (\<exists> cap. cslift s \<^bsup>s\<^esup>cap_ptr = Some cap \<and> cap_lift cap \<noteq> None \<and> 721 (cap_get_tag cap = scast cap_small_frame_cap \<or> 722 cap_get_tag cap = scast cap_frame_cap)) \<and> 723 \<acute>cap_ptr = cap_Ptr &(cte_slot\<rightarrow>[''cap_C'']) \<and> 724 cslift s cte_slot \<noteq> None\<rbrace> 725 Call generic_frame_cap_ptr_set_capFMappedAddress_'proc 726 {t. (\<exists>cte' cap'. 727 generic_frame_cap_set_capFMappedAddress_CL (cap_lift (the (cslift s \<^bsup>s\<^esup>cap_ptr))) \<^bsup>s\<^esup>asid \<^bsup>s\<^esup>addr = Some cap' \<and> 728 cte_lift cte' = option_map (cap_CL_update (K cap')) (cte_lift (the (cslift s cte_slot))) \<and> 729 t_hrs_' (globals t) = hrs_mem_update (heap_update cte_slot cte') 730 (t_hrs_' (globals s)))}" 731 apply vcg 732 apply (clarsimp simp: typ_heap_simps) 733 apply (subgoal_tac "cap_lift ret__struct_cap_C \<noteq> None") 734 prefer 2 735 apply (clarsimp simp: generic_frame_cap_set_capFMappedAddress_CL_def split: cap_CL.splits) 736 apply (clarsimp simp: clift_ptr_safe2 typ_heap_simps) 737 apply (rule_tac x="cte_C.cap_C_update (\<lambda>_. ret__struct_cap_C) y" in exI) 738 apply (case_tac y) 739 apply (clarsimp simp: cte_lift_def typ_heap_simps') 740 done 741 742lemma lookupPDSlot_spec: 743 "\<forall>s. \<Gamma> \<turnstile> \<lbrace>s. array_assertion (pd_' s) (2 ^ (pdBits - pdeBits)) (hrs_htd (\<acute>t_hrs))\<rbrace> 744 Call lookupPDSlot_'proc 745 \<lbrace> \<acute>ret__ptr_to_struct_pde_C = Ptr (lookupPDSlot (ptr_val (pd_' s)) (vptr_' s)) \<rbrace>" 746 using vptr_shiftr_le_2p_gen 747 apply vcg 748 apply clarsimp 749 apply (clarsimp simp: lookup_pd_slot_def) 750 apply (simp add: table_bits_defs) 751 apply (subst array_assertion_shrink_right, assumption) 752 apply (fastforce intro: unat_le_helper order_less_imp_le) 753 apply (simp add: Let_def word_sle_def table_bits_defs) 754 apply (case_tac pd) 755 apply (simp add: shiftl_t2n) 756 done 757 758lemma lookupPTSlot_nofail_spec: 759 "\<forall>s. \<Gamma> \<turnstile> \<lbrace>s. array_assertion (pt_' s) (2 ^ (ptBits - pteBits)) (hrs_htd (\<acute>t_hrs))\<rbrace> 760 Call lookupPTSlot_nofail_'proc 761 \<lbrace> \<acute>ret__ptr_to_struct_pte_C = Ptr (lookup_pt_slot_no_fail (ptr_val (pt_' s)) (vptr_' s)) \<rbrace>" 762 supply table_bits_defs[simp] 763 apply vcg 764 apply (clarsimp) 765 apply (simp add: lookup_pt_slot_no_fail_def) 766 apply (subst array_assertion_shrink_right, assumption) 767 apply (rule order_less_imp_le, rule unat_less_helper, simp) 768 apply (rule order_le_less_trans, rule word_and_le1, simp) 769 apply (simp add: Let_def word_sle_def) 770 apply (case_tac pt) 771 apply (simp add: shiftl_t2n mask_def) 772 done 773 774lemma ccorres_pre_getObject_pde: 775 assumes cc: "\<And>rv. ccorres r xf (P rv) (P' rv) hs (f rv) c" 776 shows "ccorres r xf 777 (\<lambda>s. (\<forall>pde. ko_at' pde p s \<longrightarrow> P pde s)) 778 {s. \<forall>pde pde'. cslift s (pde_Ptr p) = Some pde' \<and> cpde_relation pde pde' 779 \<longrightarrow> s \<in> P' pde} 780 hs (getObject p >>= (\<lambda>rv. f rv)) c" 781 apply (rule ccorres_guard_imp2) 782 apply (rule ccorres_symb_exec_l) 783 apply (rule ccorres_guard_imp2) 784 apply (rule cc) 785 apply (rule conjI) 786 apply (rule_tac Q="ko_at' rv p s" in conjunct1) 787 apply assumption 788 apply assumption 789 apply (wp getPDE_wp empty_fail_getObject | simp)+ 790 apply clarsimp 791 apply (erule cmap_relationE1 [OF rf_sr_cpde_relation], 792 erule ko_at_projectKO_opt) 793 apply simp 794 done 795 796 797(* FIXME: move *) 798(* FIXME: delete duplicates in Corres_C *) 799lemma ccorres_abstract_cleanup: 800 "ccorres r xf G G' hs a c \<Longrightarrow> 801 ccorres r xf G ({s. s \<in> S \<longrightarrow> s \<in> G'} \<inter> S) hs a c" 802 by (fastforce intro: ccorres_guard_imp) 803 804lemma pde_case_isPageTablePDE: 805 "(case pde of PageTablePDE p \<Rightarrow> fn p | _ \<Rightarrow> g) 806 = (if isPageTablePDE pde then fn (pdeTable pde) else g)" 807 by (cases pde, simp_all add: isPageTablePDE_def) 808 809lemma ptrFromPAddr_spec: 810 "\<forall>s. \<Gamma> \<turnstile> {s} 811 Call ptrFromPAddr_'proc 812 \<lbrace> \<acute>ret__ptr_to_void = Ptr (ptrFromPAddr (paddr_' s) ) \<rbrace>" 813 apply vcg 814 apply (simp add: ARM_HYP.ptrFromPAddr_def physMappingOffset_def 815 kernelBase_addr_def physBase_def ARM_HYP.physBase_def) 816 done 817 818lemma addrFromPPtr_spec: 819 "\<forall>s. \<Gamma> \<turnstile> {s} 820 Call addrFromPPtr_'proc 821 \<lbrace> \<acute>ret__unsigned_long = (addrFromPPtr (ptr_val (pptr_' s)) ) \<rbrace>" 822 apply vcg 823 apply (simp add: addrFromPPtr_def 824 ARM_HYP.addrFromPPtr_def physMappingOffset_def 825 kernelBase_addr_def physBase_def ARM_HYP.physBase_def) 826 done 827 828 829abbreviation 830 "lookupPTSlot_xf \<equiv> liftxf errstate lookupPTSlot_ret_C.status_C lookupPTSlot_ret_C.ptSlot_C ret__struct_lookupPTSlot_ret_C_'" 831 832lemma cpde_relation_pde_coarse: 833 "cpde_relation pdea pde \<Longrightarrow> (pde_get_tag pde = scast pde_pde_coarse) = isPageTablePDE pdea" 834 apply (simp add: cpde_relation_def Let_def) 835 apply (simp add: pde_pde_coarse_lift) 836 apply (case_tac pdea, simp_all add: isPageTablePDE_def) [1] 837 apply clarsimp 838 apply (simp add: pde_pde_coarse_lift_def) 839done 840 841lemma lookupPTSlot_ccorres: 842 "ccorres (lookup_failure_rel \<currency> (\<lambda>rv rv'. rv' = pte_Ptr rv)) lookupPTSlot_xf 843 (page_directory_at' pd) 844 (UNIV \<inter> \<lbrace>\<acute>pd = Ptr pd \<rbrace> \<inter> \<lbrace>\<acute>vptr = vptr \<rbrace>) 845 [] 846 (lookupPTSlot pd vptr) 847 (Call lookupPTSlot_'proc)" 848 apply (cinit lift: pd_' vptr_') 849 apply (simp add: liftE_bindE pde_case_isPageTablePDE) 850 apply (rule ccorres_pre_getObject_pde) 851 apply csymbr 852 apply csymbr 853 apply (rule ccorres_abstract_cleanup) 854 apply (rule_tac P="(ret__unsigned = scast pde_pde_coarse) = (isPageTablePDE rv)" 855 in ccorres_gen_asm2) 856 apply (rule ccorres_cond2'[where R=\<top>]) 857 apply (clarsimp simp: Collect_const_mem) 858 apply simp 859 apply (rule_tac P=\<top> and P' =UNIV in ccorres_from_vcg_throws) 860 apply (rule allI, rule conseqPre, vcg) 861 apply (clarsimp simp: throwError_def return_def syscall_error_rel_def) 862 apply (clarsimp simp: EXCEPTION_NONE_def EXCEPTION_LOOKUP_FAULT_def) 863 apply (simp add: lookup_fault_missing_capability_lift) 864 apply (simp add: mask_def) 865 apply (rule ccorres_rhs_assoc)+ 866 apply (simp add: checkPTAt_def bind_liftE_distrib liftE_bindE 867 returnOk_liftE[symmetric]) 868 apply (rule ccorres_stateAssert) 869 apply (rule_tac P="page_table_at' (ptrFromPAddr (pdeTable rv)) 870 and ko_at' rv (lookup_pd_slot pd vptr) 871 and K (isPageTablePDE rv)" and P'=UNIV in ccorres_from_vcg_throws) 872 apply (rule allI, rule conseqPre, vcg) 873 apply (clarsimp simp: returnOk_def return_def Collect_const_mem 874 lookup_pd_slot_def word_sle_def) 875 apply (frule(1) page_table_at_rf_sr, clarsimp) 876 apply (erule cmap_relationE1[OF rf_sr_cpde_relation], erule ko_at_projectKO_opt) 877 apply (clarsimp simp: typ_heap_simps cpde_relation_def Let_def isPageTablePDE_def 878 pde_pde_coarse_lift_def pde_pde_coarse_lift 879 split: pde.split_asm) 880 apply (subst array_ptr_valid_array_assertionI, erule h_t_valid_clift, simp+) 881 apply (rule unat_le_helper, rule order_trans[OF word_and_le1], simp) 882 apply (simp add: word_shift_by_2 lookup_pt_slot_no_fail_def) 883 apply (simp add: table_bits_defs mask_def shiftl_t2n) 884 apply (clarsimp simp: Collect_const_mem h_t_valid_clift) 885 apply (frule(1) page_directory_at_rf_sr, clarsimp) 886 apply (subst array_ptr_valid_array_assertionI, erule h_t_valid_clift, simp+) 887 apply (simp add: table_bits_defs) 888 apply (clarsimp simp: cpde_relation_def pde_pde_coarse_lift_def 889 pde_pde_coarse_lift Let_def isPageTablePDE_def 890 split: ARM_HYP_H.pde.split_asm) 891 done 892 893lemma cap_case_isPageDirectoryCap: 894 "(case cap of capability.ArchObjectCap (arch_capability.PageDirectoryCap pd ( Some asid)) \<Rightarrow> fn pd asid 895 | _ => g) 896 = (if ( if (isArchObjectCap cap) then if (isPageDirectoryCap (capCap cap)) then capPDMappedASID (capCap cap) \<noteq> None else False else False) 897 then fn (capPDBasePtr (capCap cap)) (the ( capPDMappedASID (capCap cap))) else g)" 898 apply (cases cap; simp add: isArchObjectCap_def) 899 apply (rename_tac arch_capability) 900 apply (case_tac arch_capability, simp_all add: isPageDirectoryCap_def) 901 apply (rename_tac option) 902 apply (case_tac option; simp) 903 done 904 905(* FIXME: MOVE to CSpaceAcc_C *) 906lemma ccorres_pre_gets_armKSASIDTable_ksArchState: 907 assumes cc: "\<And>rv. ccorres r xf (P rv) (P' rv) hs (f rv) c" 908 shows "ccorres r xf 909 (\<lambda>s. (\<forall>rv. armKSASIDTable (ksArchState s) = rv \<longrightarrow> P rv s)) 910 {s. \<forall>rv. s \<in> P' rv } 911 hs (gets (armKSASIDTable \<circ> ksArchState) >>= (\<lambda>rv. f rv)) c" 912 apply (rule ccorres_guard_imp) 913 apply (rule ccorres_symb_exec_l) 914 defer 915 apply wp[1] 916 apply (rule gets_sp) 917 apply (clarsimp simp: empty_fail_def simpler_gets_def) 918 apply assumption 919 apply clarsimp 920 defer 921 apply (rule ccorres_guard_imp) 922 apply (rule cc) 923 apply clarsimp 924 apply assumption 925 apply clarsimp 926 done 927 928abbreviation 929 "findPDForASID_xf \<equiv> liftxf errstate findPDForASID_ret_C.status_C findPDForASID_ret_C.pd_C ret__struct_findPDForASID_ret_C_'" 930 931lemma ccorres_pre_getObject_asidpool: 932 assumes cc: "\<And>rv. ccorres r xf (P rv) (P' rv) hs (f rv) c" 933 shows "ccorres r xf 934 (\<lambda>s. (\<forall>asidpool. ko_at' asidpool p s \<longrightarrow> P asidpool s)) 935 {s. \<forall> asidpool asidpool'. cslift s (ap_Ptr p) = Some asidpool' \<and> casid_pool_relation asidpool asidpool' 936 \<longrightarrow> s \<in> P' asidpool} 937 hs (getObject p >>= (\<lambda>rv :: asidpool. f rv)) c" 938 apply (rule ccorres_guard_imp2) 939 apply (rule ccorres_symb_exec_l) 940 apply (rule ccorres_guard_imp2) 941 apply (rule cc) 942 apply (rule conjI) 943 apply (rule_tac Q="ko_at' rv p s" in conjunct1) 944 apply assumption 945 apply assumption 946 apply (wpsimp wp: getASID_wp empty_fail_getObject)+ 947 apply (erule cmap_relationE1 [OF rf_sr_cpspace_asidpool_relation], 948 erule ko_at_projectKO_opt) 949 apply simp 950 done 951 952(* FIXME: move *) 953lemma ccorres_from_vcg_throws_nofail: 954 "\<forall>\<sigma>. \<Gamma>\<turnstile> {s. P \<sigma> \<and> s \<in> P' \<and> (\<sigma>, s) \<in> srel} c {}, 955 {s. \<not>snd (a \<sigma>) \<longrightarrow> (\<exists>(rv, \<sigma>')\<in>fst (a \<sigma>). (\<sigma>', s) \<in> srel \<and> arrel rv (axf s))} \<Longrightarrow> 956 ccorres_underlying srel \<Gamma> r xf arrel axf P P' (SKIP # hs) a c" 957 apply (rule ccorresI') 958 apply (drule_tac x = s in spec) 959 apply (drule hoare_sound) 960 apply (simp add: HoarePartialDef.valid_def cvalid_def) 961 apply (erule exec_handlers.cases) 962 apply clarsimp 963 apply (drule spec, drule spec, drule (1) mp) 964 apply (clarsimp dest!: exec_handlers_SkipD 965 simp: split_def unif_rrel_simps elim!: bexI [rotated]) 966 apply clarsimp 967 apply (drule spec, drule spec, drule (1) mp) 968 apply clarsimp 969 apply simp 970 done 971 972lemma findPDForASID_ccorres: 973 "ccorres (lookup_failure_rel \<currency> (\<lambda>pdeptrc pdeptr. pdeptr = pde_Ptr pdeptrc)) findPDForASID_xf 974 (valid_arch_state' and no_0_obj' and (\<lambda>_. asid \<le> mask asid_bits)) 975 (UNIV \<inter> \<lbrace>\<acute>asid = asid\<rbrace> ) 976 [] 977 (findPDForASID asid) 978 (Call findPDForASID_'proc)" 979 apply (rule ccorres_gen_asm) 980 apply (cinit lift: asid_') 981 apply (rule ccorres_Guard_Seq) 982 apply (rule ccorres_Guard_Seq) 983 apply (rule ccorres_assertE) 984 apply (rule ccorres_assertE) 985 apply (rule ccorres_liftE_Seq) 986 apply (rule_tac r'="\<lambda>asidTable rv'. rv' = option_to_ptr (asidTable (ucast (asid_high_bits_of asid)))" 987 and xf'=poolPtr_' in ccorres_split_nothrow) 988 apply (rule ccorres_from_vcg[where P=\<top> and P'=UNIV]) 989 apply (rule allI, rule conseqPre, vcg) 990 apply (clarsimp simp: simpler_gets_def Kernel_C.asidLowBits_def) 991 apply (simp add: ucast_asid_high_bits_is_shift) 992 apply (erule rf_sr_armKSASIDTable) 993 apply (drule leq_asid_bits_shift) 994 apply (simp add: asid_high_bits_def mask_def) 995 apply ceqv 996 apply (simp add: liftME_def) 997 apply (simp add: bindE_assoc) 998 apply (rename_tac asidTable poolPtr) 999 1000 apply (subgoal_tac "(doE x \<leftarrow> case asidTable (ucast (asid_high_bits_of asid)) of 1001 None \<Rightarrow> throw Fault_H.lookup_failure.InvalidRoot 1002 | Some ptr \<Rightarrow> withoutFailure $ getObject ptr; 1003 (case inv asidpool.ASIDPool x (asid && mask asid_low_bits) of 1004 None \<Rightarrow> throw Fault_H.lookup_failure.InvalidRoot 1005 | Some ptr \<Rightarrow> doE haskell_assertE (ptr \<noteq> 0) []; 1006 withoutFailure $ checkPDAt ptr; 1007 returnOk ptr 1008 odE) 1009 odE) = 1010 (if ( asidTable (ucast (asid_high_bits_of asid))=None) 1011 then (doE x\<leftarrow> throw Fault_H.lookup_failure.InvalidRoot; 1012 (case inv asidpool.ASIDPool x (asid && mask asid_low_bits) of 1013 None \<Rightarrow> throw Fault_H.lookup_failure.InvalidRoot 1014 | Some ptr \<Rightarrow> doE haskell_assertE (ptr \<noteq> 0) []; 1015 withoutFailure $ checkPDAt ptr; 1016 returnOk ptr 1017 odE) 1018 odE) 1019 else (doE x\<leftarrow> withoutFailure $ getObject (the (asidTable (ucast (asid_high_bits_of asid)))); 1020 (case inv asidpool.ASIDPool x (asid && mask asid_low_bits) of 1021 None \<Rightarrow> throw Fault_H.lookup_failure.InvalidRoot 1022 | Some ptr \<Rightarrow> doE haskell_assertE (ptr \<noteq> 0) []; 1023 withoutFailure $ checkPDAt ptr; 1024 returnOk ptr 1025 odE) 1026 odE))") 1027 1028 prefer 2 1029 apply (case_tac "asidTable (ucast (asid_high_bits_of asid))", clarsimp, clarsimp) 1030 1031 apply simp 1032 apply (thin_tac "a = (if b then c else d)" for a b c d) 1033 1034 apply (rule_tac Q="\<lambda>s. asidTable = (armKSASIDTable (ksArchState s))\<and> valid_arch_state' s \<and> no_0_obj' s \<and> (asid \<le> mask asid_bits) " 1035 and Q'="\<lambda>s'. option_to_ptr (asidTable (ucast (asid_high_bits_of asid))) = 1036 index (armKSASIDTable_' (globals s')) (unat (asid >> asid_low_bits))" 1037 in ccorres_if_cond_throws) 1038 apply clarsimp 1039 apply (subgoal_tac "asid && mask asid_bits = asid") 1040 prefer 2 1041 apply (rule less_mask_eq) 1042 apply (simp add: mask_def) 1043 apply (simp add: rf_sr_asidTable_None [symmetric] Collect_const_mem) 1044 1045 apply (rule_tac P=\<top> and P' =UNIV in ccorres_from_vcg_throws) 1046 apply (rule allI, rule conseqPre, vcg) 1047 apply (clarsimp simp: throwError_def return_def bindE_def bind_def NonDetMonad.lift_def) 1048 apply (clarsimp simp: EXCEPTION_NONE_def EXCEPTION_LOOKUP_FAULT_def) 1049 apply (simp add: lookup_fault_lift_invalid_root) 1050 1051 apply (simp add: Collect_const[symmetric] del: Collect_const) 1052 apply (rule ccorres_liftE_Seq) 1053 apply (rule ccorres_pre_getObject_asidpool) 1054 apply (rule ccorres_Guard_Seq)+ 1055 1056(*Note for Tom: apply wpc breaks here - blocks everything, cannot be interrupted *) 1057 apply (case_tac "inv ASIDPool rv (asid && mask asid_low_bits) = Some 0") 1058 apply simp 1059 apply (rule ccorres_fail') 1060 apply (rule_tac P="\<lambda>s. asidTable=armKSASIDTable (ksArchState s) \<and> 1061 valid_arch_state' s \<and> (asid \<le> mask asid_bits) " 1062 and P'= "{s'. (\<exists> ap'. cslift s' (ap_Ptr (the (asidTable (ucast (asid_high_bits_of asid))))) 1063 = Some ap' \<and> casid_pool_relation rv ap')}" 1064 in ccorres_from_vcg_throws_nofail) 1065 apply (rule allI, rule conseqPre, vcg) 1066 apply (clarsimp simp: ucast_asid_high_bits_is_shift) 1067 apply (frule_tac idx="(asid >> asid_low_bits)" in rf_asidTable, assumption, 1068 simp add: leq_asid_bits_shift) 1069 apply (clarsimp simp: option_to_ptr_def option_to_0_def) 1070 apply (clarsimp simp: typ_heap_simps) 1071 apply (case_tac rv, clarsimp simp: inv_def) 1072 apply (simp add:casid_pool_relation_def) 1073 apply (case_tac ap', simp) 1074 apply (simp add: array_relation_def) 1075 apply (erule_tac x="(asid && 2 ^ asid_low_bits - 1)" in allE) 1076 apply (simp add: word_and_le1 mask_def option_to_ptr_def option_to_0_def) 1077 apply (rename_tac "fun" array) 1078 apply (case_tac "fun (asid && 2 ^ asid_low_bits - 1)", clarsimp) 1079 apply (clarsimp simp: throwError_def return_def ) 1080 apply (clarsimp simp: EXCEPTION_NONE_def EXCEPTION_LOOKUP_FAULT_def) 1081 apply (simp add: lookup_fault_lift_invalid_root) 1082 apply (clarsimp simp: returnOk_def return_def 1083 checkPDAt_def in_monad stateAssert_def liftE_bindE 1084 get_def bind_def assert_def fail_def 1085 split:if_splits) 1086 apply vcg 1087 apply simp 1088 apply wp 1089 apply vcg 1090 apply (clarsimp simp: Collect_const_mem) 1091 apply (simp add: Kernel_C.asidLowBits_def word_sle_def 1092 asid_shiftr_low_bits_less order_le_less_trans[OF word_and_le1] 1093 arg_cong[where f="\<lambda>x. 2 ^ x", OF meta_eq_to_obj_eq, OF asid_low_bits_def]) 1094 apply (clarsimp simp: option_to_0_def option_to_ptr_def) 1095 apply (clarsimp simp: typ_heap_simps split: option.split_asm) 1096done 1097 1098 1099lemma ccorres_pre_gets_armUSGlobalPD_ksArchState: 1100 assumes cc: "\<And>rv. ccorres r xf (P rv) (P' rv) hs (f rv) c" 1101 shows "ccorres r xf 1102 (\<lambda>s. (\<forall>rv. armUSGlobalPD (ksArchState s) = rv \<longrightarrow> P rv s)) 1103 (P' (ptr_val ((Ptr ::(32 word \<Rightarrow> (pde_C[2048]) ptr)) (symbol_table ''armUSGlobalPD'')))) 1104 hs (gets (armUSGlobalPD \<circ> ksArchState) >>= (\<lambda>rv. f rv)) c" 1105 apply (rule ccorres_guard_imp) 1106 apply (rule ccorres_symb_exec_l) 1107 defer 1108 apply wp[1] 1109 apply (rule gets_sp) 1110 apply (clarsimp simp: empty_fail_def simpler_gets_def) 1111 apply assumption 1112 apply clarsimp 1113 defer 1114 apply (rule ccorres_guard_imp) 1115 apply (rule cc) 1116 apply clarsimp 1117 apply assumption 1118 apply (drule rf_sr_armUSGlobalPD) 1119 apply simp 1120 done 1121 1122lemma invalidateTranslationASIDLocal_ccorres: 1123 "ccorres dc xfdc \<top> (\<lbrace>\<acute>hw_asid = hw_asid \<rbrace>) [] 1124 (doMachineOp (invalidateLocalTLB_ASID hw_asid)) 1125 (Call invalidateTranslationASIDLocal_'proc)" 1126 apply cinit' 1127 apply (ctac (no_vcg) add: invalidateLocalTLB_ASID_ccorres) 1128 apply clarsimp 1129 done 1130 1131lemma invalidateTranslationASID_ccorres: 1132 "ccorres dc xfdc \<top> (\<lbrace>\<acute>hw_asid = hw_asid \<rbrace>) [] 1133 (doMachineOp (invalidateLocalTLB_ASID hw_asid)) 1134 (Call invalidateTranslationASID_'proc)" 1135 apply cinit' 1136 apply (ctac (no_vcg) add: invalidateTranslationASIDLocal_ccorres) 1137 apply clarsimp 1138 done 1139 1140lemma flushSpace_ccorres: 1141 "ccorres dc xfdc 1142 (valid_pde_mappings' and (\<lambda>_. asid \<le> mask asid_bits)) 1143 (UNIV \<inter> {s. asid_' s = asid}) [] 1144 (flushSpace asid) (Call flushSpace_'proc)" 1145 apply (rule ccorres_gen_asm) 1146 apply (cinit lift: asid_') 1147 apply (ctac (no_vcg) add: loadHWASID_ccorres) 1148 apply (ctac (no_vcg) add: cleanCaches_PoU_ccorres) 1149 apply csymbr 1150 apply (simp add: case_option_If2) 1151 apply (rule_tac Q=\<top> and Q'=\<top> in ccorres_if_cond_throws2) 1152 apply (clarsimp simp: Collect_const_mem pde_stored_asid_def) 1153 apply (simp add: if_split_eq1 to_bool_def) 1154 apply (rule ccorres_return_void_C [unfolded dc_def]) 1155 apply csymbr 1156 apply (clarsimp simp: pde_stored_asid_def) 1157 apply (case_tac "to_bool (stored_asid_valid_CL (pde_pde_invalid_lift stored_hw_asid___struct_pde_C))") 1158 prefer 2 1159 apply clarsimp 1160 apply clarsimp 1161 apply (case_tac "pde_get_tag stored_hw_asid___struct_pde_C = scast pde_pde_invalid") 1162 prefer 2 1163 apply clarsimp 1164 apply clarsimp 1165 apply (rule ccorres_call, 1166 rule invalidateTranslationASID_ccorres [simplified dc_def xfdc_def], 1167 simp+)[1] 1168 apply vcg 1169 apply wp+ 1170 apply simp 1171 done 1172 1173 1174 1175(* FIXME: MOVE *) 1176lemma ccorres_pre_gets_armKSHWASIDTable_ksArchState: 1177 assumes cc: "\<And>rv. ccorres r xf (P rv) (P' rv) hs (f rv) c" 1178 shows "ccorres r xf 1179 (\<lambda>s. (\<forall>rv. armKSHWASIDTable (ksArchState s) = rv \<longrightarrow> P rv s)) 1180 {s. \<forall>rv. s \<in> P' rv } 1181 hs (gets (armKSHWASIDTable \<circ> ksArchState) >>= (\<lambda>rv. f rv)) c" 1182 apply (rule ccorres_guard_imp) 1183 apply (rule ccorres_symb_exec_l) 1184 defer 1185 apply wp[1] 1186 apply (rule gets_sp) 1187 apply (clarsimp simp: empty_fail_def simpler_gets_def) 1188 apply assumption 1189 apply clarsimp 1190 defer 1191 apply (rule ccorres_guard_imp) 1192 apply (rule cc) 1193 apply clarsimp 1194 apply assumption 1195 apply clarsimp 1196 done 1197 1198(* FIXME: MOVE *) 1199lemma ccorres_pre_gets_armKSNextASID_ksArchState: 1200 assumes cc: "\<And>rv. ccorres r xf (P rv) (P' rv) hs (f rv) c" 1201 shows "ccorres r xf 1202 (\<lambda>s. (\<forall>rv. armKSNextASID (ksArchState s) = rv \<longrightarrow> P rv s)) 1203 {s. \<forall>rv. s \<in> P' rv } 1204 hs (gets (armKSNextASID \<circ> ksArchState) >>= (\<lambda>rv. f rv)) c" 1205 apply (rule ccorres_guard_imp) 1206 apply (rule ccorres_symb_exec_l) 1207 defer 1208 apply wp[1] 1209 apply (rule gets_sp) 1210 apply (clarsimp simp: empty_fail_def simpler_gets_def) 1211 apply assumption 1212 apply clarsimp 1213 defer 1214 apply (rule ccorres_guard_imp) 1215 apply (rule cc) 1216 apply clarsimp 1217 apply assumption 1218 apply clarsimp 1219 done 1220 1221 1222lemma ccorres_from_vcg_might_throw: 1223 "(\<forall>\<sigma>. Gamm \<turnstile> {s. P \<sigma> \<and> s \<in> P' \<and> (\<sigma>, s) \<in> sr} c 1224 {s. \<exists>(rv, \<sigma>') \<in> fst (a \<sigma>). (\<sigma>', s) \<in> sr \<and> r rv (xf s)}, 1225 {s. \<exists>(rv, \<sigma>') \<in> fst (a \<sigma>). (\<sigma>', s) \<in> sr \<and> arrel rv (axf s)}) 1226 \<Longrightarrow> ccorres_underlying sr Gamm r xf arrel axf P P' (SKIP # hs) a c" 1227 apply (rule ccorresI') 1228 apply (drule_tac x=s in spec) 1229 apply (erule exec_handlers.cases, simp_all) 1230 apply clarsimp 1231 apply (erule exec_handlers.cases, simp_all)[1] 1232 apply (auto elim!: exec_Normal_elim_cases)[1] 1233 apply (drule(1) exec_abrupt[rotated]) 1234 apply simp 1235 apply (clarsimp simp: unif_rrel_simps elim!: exec_Normal_elim_cases) 1236 apply fastforce 1237 apply (clarsimp simp: unif_rrel_simps) 1238 apply (drule hoare_sound) 1239 apply (clarsimp simp: cvalid_def HoarePartialDef.valid_def) 1240 apply fastforce 1241 done 1242 1243lemma rf_sr_armKSASIDTable_rel: 1244 "(s, s') \<in> rf_sr 1245 \<Longrightarrow> array_relation ((=) \<circ> option_to_0) 0xFF (armKSHWASIDTable (ksArchState s)) 1246 (armKSHWASIDTable_' (globals s'))" 1247 by (clarsimp simp: rf_sr_def cstate_relation_def 1248 Let_def carch_state_relation_def) 1249 1250lemma rf_sr_armKSASIDTable_rel': 1251 "\<lbrakk> (s, s') \<in> rf_sr; valid_arch_state' s \<rbrakk> 1252 \<Longrightarrow> index (armKSHWASIDTable_' (globals s')) (unat x) = 1253 option_to_0 (armKSHWASIDTable (ksArchState s) x) 1254 \<and> ((option_to_0 (armKSHWASIDTable (ksArchState s) x) = 0) 1255 = (armKSHWASIDTable (ksArchState s) x = None))" 1256 apply (rule conjI) 1257 apply (drule rf_sr_armKSASIDTable_rel) 1258 apply (clarsimp simp: array_relation_def) 1259 apply (rule sym, drule spec, erule mp) 1260 apply (rule order_trans, rule word_n1_ge) 1261 apply simp 1262 apply (clarsimp simp: option_to_0_def split: option.splits) 1263 apply (clarsimp simp: valid_arch_state'_def valid_asid_map'_def) 1264 apply (drule (1) is_inv_SomeD) 1265 apply (drule subsetD, fastforce) 1266 apply simp 1267 done 1268 1269lemma rf_sr_armKSNextASID: 1270 "(s, s') \<in> rf_sr \<Longrightarrow> armKSNextASID_' (globals s') = armKSNextASID (ksArchState s)" 1271 by (clarsimp simp: rf_sr_def cstate_relation_def 1272 Let_def carch_state_relation_def) 1273 1274end 1275 1276context begin interpretation Arch . (*FIXME: arch_split*) 1277 1278crunch armKSNextASID[wp]: invalidateASID 1279 "\<lambda>s. P (armKSNextASID (ksArchState s))" 1280crunch armKSNextASID[wp]: invalidateHWASIDEntry 1281 "\<lambda>s. P (armKSNextASID (ksArchState s))" 1282 1283 1284end 1285 1286context kernel_m begin 1287 1288 1289lemma findFreeHWASID_ccorres: 1290 "ccorres (=) ret__unsigned_char_' 1291 (valid_arch_state' and valid_pde_mappings') UNIV [] 1292 (findFreeHWASID) (Call findFreeHWASID_'proc)" 1293 apply (cinit) 1294 apply csymbr 1295 apply (rule ccorres_pre_gets_armKSHWASIDTable_ksArchState) 1296 apply (rule ccorres_pre_gets_armKSNextASID_ksArchState) 1297 apply (simp add: whileAnno_def case_option_find_give_me_a_map 1298 mapME_def 1299 del: Collect_const map_append) 1300 apply (rule ccorres_splitE_novcg) 1301 apply (subgoal_tac "[nextASID .e. maxBound] @ init [minBound .e. nextASID] 1302 = map (\<lambda>x. nextASID + (of_nat x)) [0 ..< 256]") 1303 apply clarsimp 1304 apply (rule_tac xf=hw_asid_offset_' and i=0 1305 and xf_update=hw_asid_offset_'_update 1306 and r'=dc and xf'=xfdc and Q=UNIV 1307 and F="\<lambda>n s. rv = armKSHWASIDTable (ksArchState s) 1308 \<and> nextASID = armKSNextASID (ksArchState s) 1309 \<and> valid_arch_state' s" 1310 in ccorres_sequenceE_while_gen') 1311 apply (rule ccorres_from_vcg_might_throw) 1312 apply (rule allI, rule conseqPre, vcg) 1313 apply (clarsimp simp: rf_sr_armKSNextASID) 1314 apply (subst down_cast_same [symmetric], 1315 simp add: is_down_def target_size_def source_size_def word_size)+ 1316 apply (simp add: ucast_ucast_mask 1317 ucast_ucast_add ucast_and_mask 1318 ucast_of_nat_small asidInvalid_def 1319 word_sless_msb_less ucast_less[THEN order_less_le_trans] 1320 word_0_sle_from_less) 1321 apply (simp add: word_sint_msb_eq not_msb_from_less word_of_nat_less 1322 trans[OF msb_nth nth_ucast] bang_big word_size 1323 uint_up_ucast is_up_def source_size_def 1324 target_size_def) 1325 apply (simp add: uint_nat unat_of_nat) 1326 apply (rule conjI, unat_arith, simp) 1327 apply (simp add: rf_sr_armKSASIDTable_rel' 1328 throwError_def return_def) 1329 apply (clarsimp simp: returnOk_def return_def) 1330 apply (simp add: minus_one_norm) 1331 apply unat_arith 1332 apply (rule conseqPre, vcg) 1333 apply clarsimp 1334 apply simp 1335 apply (rule hoare_pre, wp) 1336 apply simp 1337 apply simp 1338 apply simp 1339 apply simp 1340 1341 apply (cut_tac x=nextASID in leq_maxBound[unfolded word_le_nat_alt]) 1342 apply (simp add: minBound_word init_def maxBound_word minus_one_norm) 1343 apply (simp add: upto_enum_word) 1344 apply (rule nth_equalityI) 1345 apply (simp add: min.absorb2 1346 del: upt.simps) 1347 apply (simp add: min.absorb2 1348 del: upt.simps) 1349 apply (simp add: nth_append 1350 split: if_split) 1351 1352 apply ceqv 1353 apply (rule ccorres_assert) 1354 apply (rule_tac A="\<lambda>s. nextASID = armKSNextASID (ksArchState s) 1355 \<and> rv = armKSHWASIDTable (ksArchState s) 1356 \<and> valid_arch_state' s \<and> valid_pde_mappings' s" 1357 in ccorres_guard_imp2[where A'=UNIV]) 1358 apply (simp add: split_def) 1359 apply (rule ccorres_symb_exec_r) 1360 apply (rule_tac xf'=hw_asid_' in ccorres_abstract, ceqv) 1361 apply (rule_tac P="rv'a = nextASID" in ccorres_gen_asm2) 1362 apply (simp del: Collect_const) 1363 apply ((rule ccorres_move_const_guard )+)? 1364 apply (ctac(no_vcg) add: invalidateASID_ccorres) 1365 apply ((rule ccorres_move_const_guard 1366 | simp only: ccorres_seq_simps)+)? 1367 apply (ctac(no_vcg) add: invalidateTranslationASID_ccorres) 1368 apply (rule ccorres_split_nothrow) 1369 apply (rule ccorres_move_const_guard )+ 1370 apply (rule ccorres_handlers_weaken) 1371 apply (rule invalidateHWASIDEntry_ccorres[OF refl]) 1372 apply ceqv 1373 apply (rule_tac P="\<lambda>s. nextASID = armKSNextASID (ksArchState s)" 1374 in ccorres_from_vcg_throws[where P'=UNIV]) 1375 apply (rule allI, rule conseqPre, vcg) 1376 apply (clarsimp simp del: rf_sr_upd_safe) 1377 apply (clarsimp simp: rf_sr_def bind_def simpler_modify_def 1378 return_def cstate_relation_def Let_def) 1379 apply (simp add: carch_state_relation_def carch_globals_def 1380 cmachine_state_relation_def) 1381 apply (subst down_cast_same [symmetric], 1382 simp add: is_down_def target_size_def source_size_def word_size)+ 1383 apply (clarsimp simp: maxBound_word minBound_word 1384 ucast_ucast_add minus_one_norm 1385 split: if_split) 1386 apply (simp add: word_sint_msb_eq uint_up_ucast word_size 1387 msb_nth nth_ucast bang_big is_up_def source_size_def 1388 target_size_def) 1389 apply (simp add: uint_nat) 1390 apply unat_arith 1391 subgoal by simp 1392 apply wp 1393 apply vcg 1394 apply simp 1395 apply wp[1] 1396 apply simp 1397 apply wp 1398 apply vcg 1399 apply (rule conseqPre, vcg) 1400 apply clarsimp 1401 apply (drule_tac x=nextASID in bspec, simp) 1402 apply clarsimp 1403 apply (clarsimp simp: rf_sr_armKSNextASID 1404 rf_sr_armKSASIDTable_rel' 1405 valid_arch_state'_def 1406 valid_asid_map'_def 1407 Collect_const_mem word_sless_msb_less 1408 ucast_less[THEN order_less_le_trans] 1409 word_0_sle_from_less asid_bits_def) 1410 apply (frule(1) is_inv_SomeD, clarsimp) 1411 apply (drule subsetD, erule domI) 1412 apply simp 1413 apply (fold mapME_def) 1414 apply (wp mapME_wp') 1415 apply (rule hoare_pre, wp) 1416 apply simp 1417 apply (clarsimp simp: guard_is_UNIV_def) 1418 apply simp 1419 done 1420 1421lemma all_invs_but_ct_idle_or_in_cur_domain_valid_pde_mappings': 1422 "all_invs_but_ct_idle_or_in_cur_domain' s \<longrightarrow> valid_pde_mappings' s" 1423 by (clarsimp simp: all_invs_but_ct_idle_or_in_cur_domain'_def valid_state'_def) 1424 1425lemma invs_valid_pde_mappings': 1426 "invs' s \<longrightarrow> valid_pde_mappings' s" 1427 by (clarsimp simp: invs'_def valid_state'_def) 1428 1429lemmas invs_valid_pde_mappings'[rule_format, elim!] 1430 1431lemma getHWASID_ccorres: 1432 "ccorres (=) ret__unsigned_char_' 1433 (all_invs_but_ct_idle_or_in_cur_domain' and (\<lambda>s. asid \<le> mask asid_bits)) (UNIV \<inter> {s. asid_' s = asid}) [] 1434 (getHWASID asid) (Call getHWASID_'proc)" 1435 apply (cinit lift: asid_') 1436 apply (ctac(no_vcg) add: loadHWASID_ccorres) 1437 apply csymbr 1438 apply wpc 1439 apply (rule ccorres_cond_false) 1440 apply (rule ccorres_rhs_assoc)+ 1441 apply csymbr 1442 apply simp 1443 apply (ctac(no_vcg) add: findFreeHWASID_ccorres) 1444 apply (ctac(no_vcg) add: storeHWASID_ccorres) 1445 apply (rule ccorres_return_C, simp+)[1] 1446 apply wp+ 1447 apply (strengthen all_invs_but_ct_idle_or_in_cur_domain_valid_pde_mappings') 1448 apply (wp findFreeHWASID_invs_no_cicd') 1449 apply (rule ccorres_cond_true) 1450 apply (rule ccorres_from_vcg_throws[where P=\<top> and P'=UNIV]) 1451 apply (rule allI, rule conseqPre, vcg) 1452 apply (clarsimp simp: return_def pde_stored_asid_def 1453 split: if_split_asm) 1454 apply wp 1455 apply (clarsimp simp: pde_stored_asid_def) 1456 apply (clarsimp simp: to_bool_def split: if_split) 1457 apply (auto simp: all_invs_but_ct_idle_or_in_cur_domain'_def) 1458 done 1459 1460lemma armv_contextSwitch_ccorres: 1461 "ccorres dc xfdc (all_invs_but_ct_idle_or_in_cur_domain' and (\<lambda>s. asid \<le> mask asid_bits)) 1462 (UNIV \<inter> {s. cap_pd_' s = pde_Ptr pd} \<inter> {s. asid_' s = asid} ) [] 1463 (armv_contextSwitch pd asid) (Call armv_contextSwitch_'proc)" 1464 apply (cinit lift: cap_pd_' asid_') 1465 apply simp 1466 apply (ctac(no_vcg) add: getHWASID_ccorres) 1467 apply (fold dc_def) 1468 apply (ctac (no_vcg)add: armv_contextSwitch_HWASID_ccorres) 1469 apply wp 1470 apply clarsimp 1471 done 1472 1473(* FIXME: move *) 1474lemma ccorres_h_t_valid_armUSGlobalPD: 1475 "ccorres r xf P P' hs f (f' ;; g') \<Longrightarrow> 1476 ccorres r xf P P' hs f 1477 (Guard C_Guard {s'. s' \<Turnstile>\<^sub>c (Ptr::(32 word \<Rightarrow> (pde_C[2048]) ptr)) (symbol_table ''armUSGlobalPD'')} f';; 1478 g')" 1479 apply (rule ccorres_guard_imp2) 1480 apply (rule ccorres_move_c_guards[where P = \<top>]) 1481 apply clarsimp 1482 apply assumption 1483 apply simp 1484 by (simp add:rf_sr_def cstate_relation_def Let_def) 1485 1486lemma ccorres_pre_gets_armHSCurVCPU_ksArchState: (* not used: insufficient preconditions *) 1487 assumes cc: "\<And>rv. ccorres r xf (P rv) (P' rv) hs (f rv) c" 1488 shows "ccorres r xf 1489 (\<lambda>s. (\<forall>rv. armHSCurVCPU (ksArchState s) = rv \<longrightarrow> P rv s)) 1490 {s. \<forall>rv. s \<in> P' rv } 1491 hs (gets (armHSCurVCPU \<circ> ksArchState) >>= (\<lambda>rv. f rv)) c" 1492 apply (rule ccorres_guard_imp) 1493 apply (rule ccorres_symb_exec_l) 1494 defer 1495 apply wp[1] 1496 apply (rule gets_sp) 1497 apply (clarsimp simp: empty_fail_def simpler_gets_def) 1498 apply assumption 1499 apply clarsimp 1500 defer 1501 apply (rule ccorres_guard_imp) 1502 apply (rule cc) 1503 apply clarsimp 1504 apply assumption 1505 apply clarsimp 1506 done 1507 1508lemma setObject_vcpuRegs_update_ccorres: 1509 "ccorres dc xfdc (ko_at' vcpu vcpuptr) UNIV hs 1510 (setObject vcpuptr (vcpuRegs_update (\<lambda>_ a. if a = r then v else vcpuRegs vcpu a) vcpu)) 1511 ((Basic_heap_update 1512 (\<lambda>s. regs_C_Ptr &(vcpu_Ptr vcpuptr\<rightarrow>[''regs_C''])) 1513 (\<lambda>s. Arrays.update (h_val (hrs_mem (t_hrs_' (globals s))) 1514 (regs_C_Ptr &(vcpu_Ptr vcpuptr\<rightarrow>[''regs_C'']))) (fromEnum r) v)))" 1515 apply (rule ccorres_guard_imp) 1516 apply (rule_tac P="ko_at' vcpu vcpuptr" in setObject_ccorres_helper[where P'=UNIV] 1517 , rule conseqPre, vcg) 1518 apply clarsimp 1519 apply (rule cmap_relationE1[OF cmap_relation_vcpu] 1520 ; (clarsimp simp: objBits_simps archObjSize_def machine_bits_defs)?) 1521 apply (assumption, erule ko_at_projectKO_opt) 1522 apply (frule h_t_valid_clift) 1523 apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def carch_state_relation_def 1524 cmachine_state_relation_def update_vcpu_map_to_vcpu 1525 typ_heap_simps' cpspace_relation_def update_vcpu_map_tos) 1526 apply (erule (1) cmap_relation_updI 1527 ; clarsimp simp: cvcpu_relation_regs_def cvgic_relation_def ; (rule refl)?) 1528 1529 using maxBound_is_bound[where 'a=vcpureg, simplified fromEnum_maxBound_vcpureg_def] 1530 apply - 1531 apply (clarsimp simp: fromEnum_eq_iff less_eq_Suc_le fromEnum_eq_iff split: if_split) 1532 apply (simp add: objBits_simps archObjSize_def machine_bits_defs)+ 1533 done 1534 1535lemma vcpuUpdate_vcpuRegs_ccorres: 1536 "ccorres dc xfdc \<top> UNIV hs 1537 (vcpuUpdate vcpuptr (\<lambda>vcpu. vcpuRegs_update (\<lambda>_. (vcpuRegs vcpu)(r := v)) vcpu)) 1538 (Basic_heap_update 1539 (\<lambda>_. regs_C_Ptr &(vcpu_Ptr vcpuptr\<rightarrow>[''regs_C''])) 1540 (\<lambda>s. Arrays.update (h_val (hrs_mem (t_hrs_' (globals s))) 1541 (regs_C_Ptr &(vcpu_Ptr vcpuptr\<rightarrow>[''regs_C'']))) (fromEnum r) v))" 1542 unfolding vcpuUpdate_def 1543 apply (rule ccorres_guard_imp) 1544 apply (rule ccorres_pre_getObject_vcpu, rename_tac vcpu) 1545 apply (clarsimp simp: fun_upd_def) 1546 apply (ctac add: setObject_vcpuRegs_update_ccorres) 1547 apply simp+ 1548 done 1549 1550lemma vgicUpdate_HCR_ccorres: 1551 "ccorres dc xfdc \<top> UNIV hs 1552 (vgicUpdate vcpuptr (vgicHCR_update (\<lambda>_. hcr))) 1553 (Basic_heap_update 1554 (\<lambda>_. word_Ptr &(vgic_C_Ptr &(vcpu_Ptr vcpuptr\<rightarrow>[''vgic_C''])\<rightarrow>[''hcr_C''])) (\<lambda>_. hcr))" 1555 apply (rule ccorres_guard_imp) 1556 apply (simp add: vgicUpdate_def vcpuUpdate_def) 1557 apply (rule ccorres_pre_getObject_vcpu, rename_tac vcpu) 1558 apply (rule_tac P="ko_at' vcpu vcpuptr" in setObject_ccorres_helper[where P'=UNIV] 1559 , rule conseqPre, vcg) 1560 apply clarsimp 1561 apply (rule cmap_relationE1[OF cmap_relation_vcpu] 1562 ; (clarsimp simp: objBits_simps archObjSize_def machine_bits_defs)?) 1563 apply (assumption, erule ko_at_projectKO_opt) 1564 apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def carch_state_relation_def 1565 cmachine_state_relation_def update_vcpu_map_to_vcpu 1566 typ_heap_simps' cpspace_relation_def update_vcpu_map_tos) 1567 apply (erule (1) cmap_relation_updI 1568 ; clarsimp simp: cvcpu_relation_regs_def cvgic_relation_def ; (rule refl)?) 1569 apply (simp add: objBits_simps archObjSize_def machine_bits_defs)+ 1570 done 1571 1572(* FIXME generalise if possible, proof is copied from vgicUpdate_HCR_ccorres *) 1573lemma vgicUpdate_APR_ccorres: 1574 "ccorres dc xfdc \<top> UNIV hs 1575 (vgicUpdate vcpuptr (vgicAPR_update (\<lambda>_. hcr))) 1576 (Basic_heap_update 1577 (\<lambda>_. word_Ptr &(vgic_C_Ptr &(vcpu_Ptr vcpuptr\<rightarrow>[''vgic_C''])\<rightarrow>[''apr_C''])) (\<lambda>_. hcr))" 1578 apply (rule ccorres_guard_imp) 1579 apply (simp add: vgicUpdate_def vcpuUpdate_def) 1580 apply (rule ccorres_pre_getObject_vcpu, rename_tac vcpu) 1581 apply (rule_tac P="ko_at' vcpu vcpuptr" in setObject_ccorres_helper[where P'=UNIV] 1582 , rule conseqPre, vcg) 1583 apply clarsimp 1584 apply (rule cmap_relationE1[OF cmap_relation_vcpu] 1585 ; (clarsimp simp: objBits_simps archObjSize_def machine_bits_defs)?) 1586 apply (assumption, erule ko_at_projectKO_opt) 1587 apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def carch_state_relation_def 1588 cmachine_state_relation_def update_vcpu_map_to_vcpu 1589 typ_heap_simps' cpspace_relation_def update_vcpu_map_tos) 1590 apply (erule (1) cmap_relation_updI 1591 ; clarsimp simp: cvcpu_relation_regs_def cvgic_relation_def ; (rule refl)?) 1592 apply (simp add: objBits_simps archObjSize_def machine_bits_defs)+ 1593 done 1594 1595(* FIXME generalise if possible, proof is copied from vgicUpdate_HCR_ccorres *) 1596lemma vgicUpdate_VMCR_ccorres: 1597 "ccorres dc xfdc \<top> UNIV hs 1598 (vgicUpdate vcpuptr (vgicVMCR_update (\<lambda>_. hcr))) 1599 (Basic_heap_update 1600 (\<lambda>_. word_Ptr &(vgic_C_Ptr &(vcpu_Ptr vcpuptr\<rightarrow>[''vgic_C''])\<rightarrow>[''vmcr_C''])) (\<lambda>_. hcr))" 1601 apply (rule ccorres_guard_imp) 1602 apply (simp add: vgicUpdate_def vcpuUpdate_def) 1603 apply (rule ccorres_pre_getObject_vcpu, rename_tac vcpu) 1604 apply (rule_tac P="ko_at' vcpu vcpuptr" in setObject_ccorres_helper[where P'=UNIV] 1605 , rule conseqPre, vcg) 1606 apply clarsimp 1607 apply (rule cmap_relationE1[OF cmap_relation_vcpu] 1608 ; (clarsimp simp: objBits_simps archObjSize_def machine_bits_defs)?) 1609 apply (assumption, erule ko_at_projectKO_opt) 1610 apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def carch_state_relation_def 1611 cmachine_state_relation_def update_vcpu_map_to_vcpu 1612 typ_heap_simps' cpspace_relation_def update_vcpu_map_tos) 1613 apply (erule (1) cmap_relation_updI 1614 ; clarsimp simp: cvcpu_relation_regs_def cvgic_relation_def ; (rule refl)?) 1615 apply (simp add: objBits_simps archObjSize_def machine_bits_defs)+ 1616 done 1617 1618lemma vcpu_write_reg_ccorres: 1619 "ccorres dc xfdc 1620 (vcpu_at' vcpuptr) 1621 (UNIV \<inter> \<lbrace> \<acute>vcpu = vcpu_Ptr vcpuptr \<rbrace> \<inter> \<lbrace> \<acute>reg = of_nat (fromEnum reg) \<rbrace> 1622 \<inter> \<lbrace> \<acute>value = v \<rbrace>) hs 1623 (vcpuWriteReg vcpuptr reg v) 1624 (Call vcpu_write_reg_'proc)" 1625 supply Collect_const[simp del] dc_simp[simp del] 1626 apply (cinit lift: vcpu_' reg_' value_') 1627 apply (rule ccorres_assert) 1628 apply clarsimp 1629 apply (rule ccorres_cond_false_seq, simp) 1630 apply (rule ccorres_move_const_guards) 1631 apply ccorres_rewrite 1632 apply (rule ccorres_move_c_guard_vcpu, rule vcpuUpdate_vcpuRegs_ccorres) 1633 using maxBound_is_bound[of reg, simplified fromEnum_maxBound_vcpureg_def] 1634 apply (clarsimp simp: seL4_VCPUReg_Num_def not_le word_less_nat_alt) 1635 done 1636 1637lemma vcpu_save_reg_ccorres: 1638 "ccorres dc xfdc (vcpu_at' vcpuptr) (UNIV \<inter> \<lbrace>unat \<acute>reg = fromEnum r\<rbrace> \<inter> \<lbrace> \<acute>vcpu = vcpu_Ptr vcpuptr \<rbrace>) hs 1639 (vcpuSaveReg vcpuptr r) (Call vcpu_save_reg_'proc)" 1640 supply dc_simp[simp del] Collect_const[simp del] 1641 apply (cinit lift: reg_' vcpu_') 1642 apply (rule ccorres_assert2) 1643 apply (rule ccorres_cond_false_seq, simp) 1644 apply (ctac add: vcpu_hw_read_reg_ccorres) 1645 apply (rule ccorres_move_const_guard ccorres_move_c_guard_vcpu, simp del: fun_upd_apply)+ 1646 apply (ctac add: vcpuUpdate_vcpuRegs_ccorres) 1647 apply wpsimp 1648 apply (vcg exspec=vcpu_hw_read_reg_modifies) 1649 apply (fastforce dest: maxBound_is_bound' 1650 simp: fromEnum_maxBound_vcpureg_def seL4_VCPUReg_Num_def unat_arith_simps) 1651 done 1652 1653lemma vcpu_restore_reg_ccorres: 1654 "ccorres dc xfdc 1655 (vcpu_at' vcpuptr) (UNIV \<inter> \<lbrace>unat \<acute>reg = fromEnum r\<rbrace> \<inter> \<lbrace> \<acute>vcpu = vcpu_Ptr vcpuptr \<rbrace>) hs 1656 (vcpuRestoreReg vcpuptr r) (Call vcpu_restore_reg_'proc)" 1657 supply dc_simp[simp del] Collect_const[simp del] 1658 apply (cinit lift: reg_' vcpu_') 1659 apply (rule ccorres_assert2) 1660 apply (rule ccorres_cond_false_seq, simp) 1661 apply (rule ccorres_move_const_guard ccorres_move_c_guard_vcpu, simp)+ 1662 apply (rule ccorres_pre_getObject_vcpu, rename_tac vcpu) 1663 apply (ctac add: vcpu_hw_write_reg_ccorres) 1664 apply (frule maxBound_is_bound') 1665 apply (clarsimp simp: word_le_nat_alt word_less_nat_alt 1666 fromEnum_maxBound_vcpureg_def seL4_VCPUReg_Num_def) 1667 apply (frule cmap_relation_vcpu) 1668 apply (clarsimp simp: typ_heap_simps cvcpu_relation_def cvcpu_regs_relation_def) 1669 done 1670 1671lemma ccorres_dc_from_rrel: 1672 "ccorres r xf P P' hs a c \<Longrightarrow> ccorres dc xf' P P' hs a c" 1673 unfolding ccorres_underlying_def 1674 by (fastforce simp: unif_rrel_def split: xstate.splits) 1675 1676lemma ccorres_mapM_x_while_gen'x: 1677 fixes xf :: "globals myvars \<Rightarrow> ('c :: len) word" 1678 assumes rl: "\<forall>n. n < length xs \<longrightarrow> 1679 ccorres dc xfdc (F (n * j)) {s. xf s = of_nat (i + n * j)} hs (f (xs ! n)) body" 1680 and guard: "\<And>n. P n = (n < of_nat (i + length xs * j))" 1681 and bodyi: "\<forall>s. \<Gamma>\<turnstile>\<^bsub>/UNIV\<^esub> {s} body {s'. xf s' = xf s}" 1682 and hi: "\<And>n. Suc n < length xs \<Longrightarrow> \<lbrace>F (n *j)\<rbrace> f (xs ! n) \<lbrace>\<lambda>_. F (Suc n * j)\<rbrace>" 1683 and wb: "i + length xs * j < 2 ^ len_of TYPE('c)" 1684 and xf: "\<forall>s f. xf (xf_update f s) = f (xf s) \<and> globals (xf_update f s) = globals s" 1685 and j: "0 < j" 1686 shows "ccorres dc xfdc 1687 (F (0 :: nat)) {s. xf s = of_nat i} hs 1688 (mapM_x f xs) 1689 (While {s. P (xf s)} 1690 (body ;; Basic (\<lambda>s. xf_update (\<lambda>_. xf s + of_nat j) s)))" 1691 unfolding mapM_x_def 1692 apply (rule ccorres_rel_imp) 1693 apply (rule ccorres_sequence_x_while_gen'[where xf_update=xf_update]) 1694 apply (clarsimp simp only: length_map nth_map rl) 1695 apply (simp add: assms hi[simplified])+ 1696 done 1697 1698lemma vcpu_restore_reg_range_ccorres: 1699 "ccorres dc xfdc 1700 (vcpu_at' vcpuptr and K (fromEnum start \<le> fromEnum end)) 1701 (UNIV \<inter> \<lbrace>unat \<acute>start = fromEnum start\<rbrace> \<inter> \<lbrace>unat \<acute>end = fromEnum end\<rbrace> 1702 \<inter> \<lbrace> \<acute>vcpu = vcpu_Ptr vcpuptr \<rbrace>) hs 1703 (vcpuRestoreRegRange vcpuptr start end) (Call vcpu_restore_reg_range_'proc)" 1704 apply (rule ccorres_grab_asm) 1705 apply (cinit lift: start_' end_' vcpu_' simp: whileAnno_def) 1706 apply csymbr 1707 apply (clarsimp, fold dc_def) 1708 apply (rule ccorres_dc_from_rrel) 1709 (* supplying these as dest/intro/simp to proof tactics has no desired effect *) 1710 using maxBound_is_bound[of start, simplified fromEnum_maxBound_vcpureg_def] 1711 length_upto_enum_le_maxBound[of start "end", simplified fromEnum_maxBound_vcpureg_def] 1712 apply - 1713 apply (rule ccorres_mapM_x_while'[where i="fromEnum start" 1714 and F="\<lambda>n s. vcpu_at' vcpuptr s"]) 1715 apply clarsimp 1716 apply (rule ccorres_guard_imp) 1717 apply (ctac add: vcpu_restore_reg_ccorres) 1718 apply assumption 1719 subgoal 1720 apply (clarsimp simp: fromEnum_upto_nth dest!: less_length_upto_enum_maxBoundD) 1721 by (subst unat_add_lem'; clarsimp simp: fromEnum_maxBound_vcpureg_def unat_of_nat_eq) 1722 subgoal 1723 apply (simp add: word_less_nat_alt word_le_nat_alt) 1724 apply (subst unat_add_lem'; clarsimp simp: unat_of_nat_eq) 1725 apply (fastforce simp add: upto_enum_red split: if_splits) 1726 done 1727 apply (rule allI, rule conseqPre, vcg exspec=vcpu_restore_reg_modifies) 1728 apply fastforce 1729 apply wpsimp 1730 apply (fastforce simp: word_bits_def) 1731 apply (clarsimp simp: Collect_const_mem) 1732 apply (subst unat_eq_of_nat[symmetric]; clarsimp) 1733 done 1734 1735lemma vcpu_save_reg_range_ccorres: 1736 "ccorres dc xfdc 1737 (vcpu_at' vcpuptr and K (fromEnum start \<le> fromEnum end)) 1738 (UNIV \<inter> \<lbrace>unat \<acute>start = fromEnum start\<rbrace> \<inter> \<lbrace>unat \<acute>end = fromEnum end\<rbrace> 1739 \<inter> \<lbrace> \<acute>vcpu = vcpu_Ptr vcpuptr \<rbrace>) hs 1740 (vcpuSaveRegRange vcpuptr start end) (Call vcpu_save_reg_range_'proc)" 1741 apply (rule ccorres_grab_asm) 1742 apply (cinit lift: start_' end_' vcpu_' simp: whileAnno_def) 1743 apply csymbr 1744 apply (clarsimp, fold dc_def) 1745 apply (rule ccorres_dc_from_rrel) 1746 (* supplying these as dest/intro/simp to proof tactics has no desired effect *) 1747 using maxBound_is_bound[of start, simplified fromEnum_maxBound_vcpureg_def] 1748 length_upto_enum_le_maxBound[of start "end", simplified fromEnum_maxBound_vcpureg_def] 1749 apply - 1750 apply (rule ccorres_mapM_x_while'[where i="fromEnum start" 1751 and F="\<lambda>n s. vcpu_at' vcpuptr s"]) 1752 apply clarsimp 1753 apply (rule ccorres_guard_imp) 1754 apply (ctac add: vcpu_save_reg_ccorres) 1755 apply assumption 1756 subgoal 1757 apply (clarsimp simp: fromEnum_upto_nth dest!: less_length_upto_enum_maxBoundD) 1758 by (subst unat_add_lem'; clarsimp simp: fromEnum_maxBound_vcpureg_def unat_of_nat_eq) 1759 subgoal 1760 apply (simp add: word_less_nat_alt word_le_nat_alt) 1761 apply (subst unat_add_lem'; clarsimp simp: unat_of_nat_eq) 1762 apply (fastforce simp add: upto_enum_red split: if_splits) 1763 done 1764 apply (rule allI, rule conseqPre, vcg exspec=vcpu_save_reg_modifies) 1765 apply fastforce 1766 apply wpsimp 1767 apply (fastforce simp: word_bits_def) 1768 apply (clarsimp simp: Collect_const_mem) 1769 apply (subst unat_eq_of_nat[symmetric]; clarsimp) 1770 done 1771 1772lemma vcpu_disable_ccorres: 1773 "ccorres dc xfdc 1774 (pspace_aligned' and pspace_distinct' and valid_objs' and no_0_obj' and valid_arch_state' 1775 and (case v of None \<Rightarrow> \<top> | Some new \<Rightarrow> vcpu_at' new)) 1776 (UNIV \<inter> {s. vcpu_' s = option_to_ptr v}) hs 1777 (vcpuDisable v) (Call vcpu_disable_'proc)" 1778 apply (cinit lift: vcpu_') 1779 apply (ctac (no_vcg) add: dsb_ccorres) 1780 apply (rule ccorres_split_nothrow_novcg) 1781 apply wpc 1782 (* v=None *) 1783 apply simp 1784 apply ccorres_rewrite 1785 apply (rule ccorres_return_Skip) 1786 (* v=Some x2 *) 1787 apply (rule ccorres_cond_true) 1788 apply (rule ccorres_rhs_assoc)+ 1789 apply (ctac (no_vcg) add: get_gic_vcpu_ctrl_hcr_ccorres) 1790 apply (rule ccorres_split_nothrow_novcg[of _ _ dc xfdc]) 1791 apply (rule ccorres_move_const_guard ccorres_move_c_guard_vcpu, simp) 1792 apply clarsimp 1793 apply (ctac (no_vcg) add: vgicUpdate_HCR_ccorres) 1794 apply ceqv 1795 apply (ctac (no_vcg) add: vcpu_save_reg_ccorres) 1796 apply (ctac (no_vcg) pre: ccorres_call[where r=dc and xf'=xfdc] add: isb_ccorres) 1797 apply (wpsimp simp: guard_is_UNIV_def)+ 1798 apply ceqv 1799 apply (clarsimp simp: doMachineOp_bind empty_fail_isb) 1800 apply (ctac (no_vcg) add: set_gic_vcpu_ctrl_hcr_ccorres) 1801 apply (ctac (no_vcg) add: isb_ccorres) 1802 apply (ctac (no_vcg) add: setSCTLR_ccorres) 1803 apply (ctac (no_vcg) add: setHCR_ccorres) 1804 apply (ctac (no_vcg) add: isb_ccorres[unfolded dc_def]) 1805 apply simp+ 1806 apply wp+ 1807 apply clarsimp 1808 apply (simp add: guard_is_UNIV_def) 1809 apply (clarsimp simp: Collect_const_mem hcrNative_def, rule refl) 1810 apply (wpsimp wp: hoare_vcg_all_lift)+ 1811 apply (clarsimp simp: Collect_const_mem ko_at'_not_NULL dest!: vcpu_at_ko split: option.splits) 1812 done 1813 1814lemma vcpu_enable_ccorres: 1815 "ccorres dc xfdc 1816 (pspace_aligned' and pspace_distinct' and valid_objs' and no_0_obj' 1817 and valid_arch_state' and vcpu_at' v) 1818 (UNIV \<inter> {s. vcpu_' s = vcpu_Ptr v}) hs 1819 (vcpuEnable v) (Call vcpu_enable_'proc)" 1820 apply (cinit lift: vcpu_') 1821 apply (ctac (no_vcg) add: vcpu_restore_reg_ccorres) 1822 apply (rule ccorres_pre_getObject_vcpu, rename_tac vcpu) 1823 apply (clarsimp simp: doMachineOp_bind empty_fail_isb) 1824 apply (ctac (no_vcg) add: setHCR_ccorres) 1825 apply (ctac (no_vcg) add: isb_ccorres) 1826 apply (rule_tac P="ko_at' vcpu v" in ccorres_cross_over_guard) 1827 apply (ctac pre: ccorres_move_c_guard_vcpu add: set_gic_vcpu_ctrl_hcr_ccorres[unfolded dc_def]) 1828 apply wpsimp+ 1829 apply (rule_tac Q="\<lambda>_. vcpu_at' v" in hoare_post_imp, fastforce) 1830 apply wpsimp 1831 apply (clarsimp simp: typ_heap_simps' Collect_const_mem cvcpu_relation_def 1832 cvcpu_regs_relation_def Let_def cvgic_relation_def hcrVCPU_def 1833 | rule conjI | simp)+ 1834 apply (drule (1) vcpu_at_rf_sr) 1835 apply (clarsimp simp: typ_heap_simps' cvcpu_relation_def cvgic_relation_def) 1836 done 1837 1838(* MOVE copied from CSpace_RAB_C *) 1839lemma ccorres_gen_asm_state: 1840 assumes rl: "\<And>s. P s \<Longrightarrow> ccorres r xf G G' hs a c" 1841 shows "ccorres r xf (G and P) G' hs a c" 1842proof (rule ccorres_guard_imp2) 1843 show "ccorres r xf (G and (\<lambda>_. \<exists>s. P s)) G' hs a c" 1844 apply (rule ccorres_gen_asm) 1845 apply (erule exE) 1846 apply (erule rl) 1847 done 1848next 1849 fix s s' 1850 assume "(s, s') \<in> rf_sr" and "(G and P) s" and "s' \<in> G'" 1851 thus "(G and (\<lambda>_. \<exists>s. P s)) s \<and> s' \<in> G'" 1852 by (clarsimp elim!: exI) 1853qed 1854 1855(* FIXME shadows two other identical versions in other files *) 1856lemma ccorres_abstract_known: 1857 "\<lbrakk> \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' g (g' rv'); ccorres rvr xf P P' hs f (g' val) \<rbrakk> 1858 \<Longrightarrow> ccorres rvr xf P (P' \<inter> {s. xf' s = val}) hs f g" 1859 apply (rule ccorres_guard_imp2) 1860 apply (rule_tac xf'=xf' in ccorres_abstract) 1861 apply assumption 1862 apply (rule_tac P="rv' = val" in ccorres_gen_asm2) 1863 apply simp 1864 apply simp 1865 done 1866 1867lemma vcpu_restore_ccorres: 1868 notes upt_Suc[simp del] dc_simp[simp del] Collect_const[simp del] 1869 shows 1870 "ccorres dc xfdc 1871 (pspace_aligned' and pspace_distinct' and valid_objs' and no_0_obj' and valid_arch_state' 1872 and vcpu_at' vcpuPtr) 1873 (UNIV \<inter> {s. vcpu_' s = vcpu_Ptr vcpuPtr}) hs 1874 (vcpuRestore vcpuPtr) (Call vcpu_restore_'proc)" 1875 apply (cinit lift: vcpu_' simp: whileAnno_def) 1876 apply (simp add: doMachineOp_bind uncurry_def split_def doMachineOp_mapM_x)+ 1877 apply (clarsimp simp: bind_assoc) 1878 apply (ctac (no_vcg) add: set_gic_vcpu_ctrl_hcr_ccorres) 1879 apply (ctac (no_vcg) add: isb_ccorres) 1880 apply (rule ccorres_pre_getObject_vcpu) 1881 apply (rule ccorres_move_c_guard_vcpu, rename_tac vcpu) 1882 apply (rule ccorres_pre_gets_armKSGICVCPUNumListRegs_ksArchState, rename_tac lr_num) 1883 apply (ctac (no_vcg) add: set_gic_vcpu_ctrl_vmcr_ccorres) 1884 apply (rule_tac P="ko_at' vcpu vcpuPtr" in ccorres_cross_over_guard) 1885 apply (ctac (no_vcg) add: set_gic_vcpu_ctrl_apr_ccorres) 1886 apply (rule_tac xf'=lr_num_' and R="\<lambda>s. lr_num = (armKSGICVCPUNumListRegs \<circ> ksArchState) s" 1887 and val="of_nat lr_num" in ccorres_symb_exec_r_known_rv_UNIV[where R'=UNIV]) 1888 apply vcg 1889 apply (fastforce intro!: rf_sr_armKSGICVCPUNumListRegs) 1890 apply ceqv 1891 apply (rule ccorres_rhs_assoc2) 1892 apply (rule ccorres_split_nothrow_novcg) 1893 (* the loop *) 1894 apply (rule_tac P="lr_num \<le> 63" in ccorres_gen_asm) 1895 apply (rule_tac F="\<lambda>_ s. lr_num \<le> 63 \<and> ko_at' vcpu vcpuPtr s" in ccorres_mapM_x_while) 1896 apply (intro allI impI) 1897 apply clarsimp 1898 apply (rule ccorres_guard_imp2) 1899 apply (rule_tac P="\<lambda>s. lr_num \<le> 63" in ccorres_cross_over_guard) 1900 apply (rule ccorres_Guard) 1901 apply (rule_tac val="of_nat n" in ccorres_abstract_known[where xf'=i_'], ceqv) 1902 apply (rule_tac P="n \<le> 63" in ccorres_gen_asm) 1903 apply (rule ccorres_move_c_guard_vcpu) 1904 apply (ctac (no_vcg) add: set_gic_vcpu_ctrl_lr_ccorres) 1905 1906 apply (clarsimp simp: virq_to_H_def ko_at_vcpu_at'D dc_def upt_Suc) 1907 apply (rule conjI[rotated]) 1908 subgoal (* FIXME extract into separate lemma *) 1909 by (fastforce simp: word_less_nat_alt unat_of_nat_eq elim: order_less_le_trans) 1910 1911 apply (frule (1) vcpu_at_rf_sr) 1912 apply (clarsimp simp: typ_heap_simps cvcpu_relation_regs_def cvgic_relation_def virq_to_H_def unat_of_nat) 1913 apply (simp add: word_less_nat_alt upt_Suc) 1914 apply vcg 1915 apply clarsimp 1916 apply wpsimp 1917 apply (simp add: upt_Suc) 1918 apply (fastforce simp: word_less_nat_alt unat_of_nat_eq word_bits_def elim: order_less_le_trans) 1919 apply ceqv 1920 1921apply (ctac add: vcpu_restore_reg_range_ccorres) 1922 1923 apply (ctac add: vcpu_enable_ccorres) 1924 1925apply wpsimp 1926 1927apply (vcg exspec=vcpu_restore_reg_range_modifies) 1928apply (wpsimp wp: crunch_wps) 1929 1930 apply (wpsimp simp: guard_is_UNIV_def dc_def upt_Suc ko_at_vcpu_at'D wp: mapM_x_wp_inv | rule UNIV_I | wp hoare_vcg_imp_lift hoare_vcg_all_lift hoare_vcg_disj_lift)+ 1931 1932 apply (fastforce simp: fromEnum_def enum_vcpureg seL4_VCPUReg_SPSRfiq_def) 1933 1934apply (clarsimp simp: guard_is_UNIV_def) 1935apply (wpsimp simp: vcpu_at_ko'_eq wp: hoare_vcg_imp_lift')+ 1936 1937 apply (rule conjI) 1938 apply (fastforce simp: invs_no_cicd'_def valid_arch_state'_def max_armKSGICVCPUNumListRegs_def) 1939 apply (rule conjI) 1940 apply (fastforce simp: fromEnum_def enum_vcpureg) 1941 apply (fastforce dest!: vcpu_at_rf_sr 1942 simp: typ_heap_simps' cvcpu_relation_def cvgic_relation_def) 1943 done 1944 1945lemma ccorres_pre_getsNumListRegs: 1946 assumes cc: "\<And>rv. ccorres r xf (P rv) (P' rv) hs (f rv) c" 1947 shows "ccorres r xf 1948 (\<lambda>s. (\<forall>rv. (armKSGICVCPUNumListRegs \<circ> ksArchState) s = rv \<longrightarrow> P rv s)) 1949 {s. \<forall>rv num'. gic_vcpu_num_list_regs_' (globals s) = num' 1950 \<longrightarrow> s \<in> P' rv } 1951 hs (gets (armKSGICVCPUNumListRegs \<circ> ksArchState) >>= (\<lambda>rv. f rv)) c" 1952 apply (rule ccorres_guard_imp) 1953 apply (rule ccorres_symb_exec_l) 1954 defer 1955 apply wp 1956 apply (rule hoare_gets_sp) 1957 apply (clarsimp simp: empty_fail_def getCurThread_def simpler_gets_def) 1958 apply assumption 1959 apply clarsimp 1960 defer 1961 apply (rule ccorres_guard_imp) 1962 apply (rule cc) 1963 apply clarsimp 1964 apply assumption 1965 apply (clarsimp simp: rf_sr_ksArchState_armHSCurVCPU) 1966 done 1967 1968lemma ccorres_gets_armKSGICVCPUNumListRegs: 1969 "ccorres ((=) \<circ> of_nat) lr_num_' \<top> UNIV hs 1970 (gets (armKSGICVCPUNumListRegs \<circ> ksArchState)) (\<acute>lr_num :== \<acute>gic_vcpu_num_list_regs)" 1971 apply (rule ccorres_from_vcg_nofail) 1972 apply clarsimp 1973 apply (rule conseqPre, vcg) 1974 apply (clarsimp simp: simpler_gets_def) 1975 apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def carch_state_relation_def) 1976 done 1977 1978lemma vgicUpdateLR_ccorres: 1979 "ccorres dc xfdc (\<top> and K (n \<le> 63 \<and> n' = n \<and> virq_to_H v' = v)) UNIV hs 1980 (vgicUpdateLR vcpuptr n v) 1981 (Basic_heap_update 1982 (\<lambda>_. vgic_lr_C_Ptr &(vgic_C_Ptr &(vcpu_Ptr vcpuptr\<rightarrow>[''vgic_C''])\<rightarrow>[''lr_C''])) 1983 (\<lambda>s. Arrays.update 1984 (h_val (hrs_mem (t_hrs_' (globals s))) 1985 (vgic_lr_C_Ptr &(vgic_C_Ptr &(vcpu_Ptr vcpuptr\<rightarrow>[''vgic_C''])\<rightarrow>[''lr_C'']))) 1986 n' v'))" 1987 apply (rule ccorres_grab_asm) 1988 supply from_bool_eq_if[simp] from_bool_eq_if'[simp] from_bool_0[simp] 1989 apply (rule ccorres_guard_imp) 1990 apply (simp add: vgicUpdate_def vcpuUpdate_def vgicUpdateLR_def) 1991 apply (rule ccorres_pre_getObject_vcpu, rename_tac vcpu) 1992 apply (rule_tac P="ko_at' vcpu vcpuptr" in setObject_ccorres_helper[where P'=UNIV] 1993 , rule conseqPre, vcg) 1994 apply clarsimp 1995 apply (rule cmap_relationE1[OF cmap_relation_vcpu] 1996 ; (clarsimp simp: objBits_simps archObjSize_def machine_bits_defs)?) 1997 apply (assumption, erule ko_at_projectKO_opt) 1998 apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def carch_state_relation_def 1999 cmachine_state_relation_def update_vcpu_map_to_vcpu 2000 typ_heap_simps' cpspace_relation_def update_vcpu_map_tos) 2001 apply (erule (1) cmap_relation_updI 2002 ; clarsimp simp: cvcpu_relation_regs_def cvgic_relation_def ; (rule refl)?) 2003 apply (fastforce simp: virq_to_H_def split: if_split) 2004 apply (simp add: objBits_simps archObjSize_def machine_bits_defs)+ 2005 done 2006 2007lemma vcpu_save_ccorres: 2008 notes dc_simp[simp del] Collect_const[simp del] 2009 shows 2010 "ccorres dc xfdc 2011 (pspace_aligned' and pspace_distinct' and valid_objs' and no_0_obj' and valid_arch_state' 2012 and case_option \<top> (vcpu_at' \<circ> fst) v) 2013 (UNIV \<inter> {s. vcpu_' s = case_option NULL (vcpu_Ptr \<circ> fst) v} 2014 \<inter> {s. active_' s = case_option 0 (from_bool \<circ> snd) v}) hs 2015 (vcpuSave v) (Call vcpu_save_'proc)" 2016 apply (cinit lift: vcpu_' active_' simp: whileAnno_def) 2017 apply wpc 2018 (* v = None *) 2019 apply (rule ccorres_fail) 2020 (* v = Some (vcpuPtr, active) *) 2021 apply wpc 2022 apply (rename_tac vcpuPtr act) 2023 apply (ctac (no_vcg) add: dsb_ccorres) 2024 apply (rule ccorres_split_nothrow_novcg) 2025 apply (rule_tac R=\<top> in ccorres_when) 2026 apply clarsimp 2027 apply (rule ccorres_rhs_assoc) 2028 apply (ctac (no_vcg) add: vcpu_save_reg_ccorres) 2029 apply (ctac (no_vcg) add: get_gic_vcpu_ctrl_hcr_ccorres) 2030 apply (rule ccorres_move_c_guard_vcpu) 2031 apply (clarsimp) 2032 apply (ctac (no_vcg) add: vgicUpdate_HCR_ccorres) 2033 apply wpsimp+ 2034 apply ceqv 2035 apply (ctac (no_vcg) add: get_gic_vcpu_ctrl_vmcr_ccorres) 2036 apply clarsimp 2037 apply (rule ccorres_move_c_guard_vcpu) 2038 apply (ctac (no_vcg) add: vgicUpdate_VMCR_ccorres) 2039 apply (ctac (no_vcg) add: get_gic_vcpu_ctrl_apr_ccorres) 2040 apply (rule ccorres_move_c_guard_vcpu) 2041 apply clarsimp 2042 apply (ctac (no_vcg) add: vgicUpdate_APR_ccorres) 2043 apply (ctac (no_vcg) add: ccorres_gets_armKSGICVCPUNumListRegs[simplified comp_def]) 2044 apply (rename_tac lr_num lr_num') 2045 apply (rule ccorres_rhs_assoc2) 2046 apply (rule ccorres_split_nothrow_novcg) 2047 (* the loop *) 2048 apply (rule_tac P="lr_num \<le> 63" in ccorres_gen_asm) 2049 apply (rule_tac F="\<lambda>_ s. lr_num \<le> 63 \<and> vcpu_at' vcpuPtr s" in ccorres_mapM_x_while) 2050 apply (intro allI impI) 2051 apply clarsimp 2052 apply (rule ccorres_guard_imp2) 2053 apply (rule_tac P="\<lambda>s. lr_num \<le> 63" in ccorres_cross_over_guard) 2054 apply (ctac (no_vcg) add: get_gic_vcpu_ctrl_lr_ccorres) 2055 apply (rule ccorres_Guard) 2056 apply (rule_tac val="of_nat n" in ccorres_abstract_known[where xf'=i_'], ceqv) 2057 apply (rule_tac P="n \<le> 63" in ccorres_gen_asm) 2058 apply (rule ccorres_move_c_guard_vcpu) 2059 apply (clarsimp simp: unat_of_nat_eq) 2060 apply (ctac (no_vcg) add: vgicUpdateLR_ccorres) 2061 apply (wpsimp simp: virq_to_H_def)+ 2062 apply (fastforce intro: word_of_nat_less) 2063 apply fastforce 2064 apply clarsimp 2065 apply (rule conseqPre, vcg exspec=get_gic_vcpu_ctrl_lr_modifies) 2066 apply fastforce 2067 apply wpsimp 2068 apply (fastforce simp: word_bits_def) 2069 apply ceqv 2070 apply (ctac (no_vcg) add: vcpu_save_reg_range_ccorres) 2071 apply (ctac (no_vcg) add: isb_ccorres) 2072 apply (wpsimp simp: guard_is_UNIV_def wp: mapM_x_wp_inv)+ 2073 apply (fastforce simp: seL4_VCPUReg_SPSRfiq_def fromEnum_def enum_vcpureg) 2074 apply (wpsimp simp: guard_is_UNIV_def | rule UNIV_I)+ 2075 apply (simp add: invs_no_cicd'_def valid_arch_state'_def max_armKSGICVCPUNumListRegs_def dc_def) 2076 apply (fastforce simp: fromEnum_def enum_vcpureg) 2077 done 2078 2079lemma vcpu_switch_ccorres_None: 2080 "ccorres dc xfdc 2081 (pspace_aligned' and pspace_distinct' and valid_objs' and no_0_obj' 2082 and valid_arch_state') 2083 (UNIV \<inter> {s. new_' s = NULL}) hs 2084 (vcpuSwitch None) (Call vcpu_switch_'proc)" 2085 apply (cinit lift: new_') 2086 (* v = None *) 2087 apply ccorres_rewrite 2088 apply (simp add: when_def) 2089 apply (rule ccorres_pre_getCurVCPU) 2090 apply wpc 2091 (* v = None & CurVCPU = None *) 2092 apply (rule ccorres_cond_false) 2093 apply (rule ccorres_return_Skip[unfolded dc_def]) 2094 (* v = None & CurVCPU \<noteq> None *) 2095 apply ccorres_rewrite 2096 apply wpc 2097 apply (rename_tac ccurv cactive) 2098 apply simp 2099 apply (rule ccorres_cond_true) 2100 apply (rule_tac R="\<lambda>s. armHSCurVCPU (ksArchState s) = Some (ccurv, cactive)" in ccorres_cond) 2101 apply (clarsimp simp: cur_vcpu_relation_def dest!: rf_sr_ksArchState_armHSCurVCPU) 2102 apply (ctac add: vcpu_disable_ccorres) 2103 apply (rule_tac v=x2 in armHSCurVCPU_update_active_ccorres[simplified dc_def]) 2104 apply (simp add: from_bool_def false_def) 2105 apply simp 2106 apply wp 2107 apply clarsimp 2108 apply assumption 2109 apply clarsimp 2110 apply (vcg exspec=vcpu_disable_modifies) 2111 apply (rule ccorres_return_Skip[unfolded dc_def]) 2112 apply (clarsimp, rule conjI) 2113 apply (fastforce dest: invs_cicd_arch_state' simp: valid_arch_state'_def vcpu_at_is_vcpu' ko_wp_at'_def split: option.splits) 2114 by (auto dest!: rf_sr_ksArchState_armHSCurVCPU simp: cur_vcpu_relation_def)+ 2115 2116lemma vcpu_switch_ccorres_Some: 2117 "ccorres dc xfdc 2118 (pspace_aligned' and pspace_distinct' and valid_objs' and no_0_obj' 2119 and valid_arch_state' and vcpu_at' v) 2120 (UNIV \<inter> {s. new_' s = vcpu_Ptr v}) hs 2121 (vcpuSwitch (Some v)) (Call vcpu_switch_'proc)" 2122 apply (cinit lift: new_') 2123 (* v \<noteq> None *) 2124 apply simp 2125 apply (rule ccorres_pre_getCurVCPU) 2126 apply wpc 2127 (* v \<noteq> None & CurVCPU = None *) 2128 apply (rule ccorres_cond_true) 2129 apply (rule ccorres_cond_true) 2130 apply (rule ccorres_rhs_assoc)+ 2131 apply (rule ccorres_cond_false_seq) 2132 apply ccorres_rewrite 2133 apply (ctac add: vcpu_restore_ccorres) 2134 apply (rule_tac curv="Some (v, True)" in armHSCurVCPU_update_ccorres[unfolded dc_def]) 2135 apply wp 2136 apply clarsimp 2137 apply (vcg exspec=vcpu_restore_modifies) 2138 (* v \<noteq> None & CurVCPU \<noteq> None *) 2139 apply wpc 2140 apply (rename_tac ccurv cactive) 2141 apply (rule_tac R="\<lambda>s. (armHSCurVCPU \<circ> ksArchState) s = Some (ccurv, cactive)" in ccorres_cond) 2142 apply (clarsimp dest!: rf_sr_ksArchState_armHSCurVCPU 2143 simp: Collect_const_mem cur_vcpu_relation_def from_bool_def true_def 2144 split: option.splits) 2145 (* new \<noteq> CurVCPU or equivalently v \<noteq> ccurv *) 2146 apply (rule ccorres_cond_true) 2147 apply (rule ccorres_rhs_assoc)+ 2148 apply (rule ccorres_cond_true_seq) 2149 apply (ctac add: vcpu_save_ccorres) 2150 apply (ctac add: vcpu_restore_ccorres) 2151 apply (rule_tac curv="Some (v, True)" in armHSCurVCPU_update_ccorres[unfolded dc_def]) 2152 apply wp 2153 apply clarsimp 2154 apply (vcg exspec=vcpu_restore_modifies) 2155 apply (wpsimp wp: hoare_vcg_conj_lift vcpuSave_invs_no_cicd' vcpuSave_typ_at') 2156 apply clarsimp 2157 apply (vcg exspec=vcpu_save_modifies) 2158 (* new = CurVCPU or equivalently v = ccurv *) 2159 apply (unfold when_def) 2160 apply (rule_tac R="\<lambda>s. (ccurv = v) \<and> (armHSCurVCPU \<circ> ksArchState) s = Some (ccurv, cactive)" 2161 in ccorres_cond) 2162 apply (clarsimp dest!: rf_sr_ksArchState_armHSCurVCPU 2163 simp: Collect_const_mem cur_vcpu_relation_def from_bool_def 2164 split: option.splits bool.splits) 2165 (* ccactive = false *) 2166 apply (rule ccorres_rhs_assoc) 2167 apply (ctac (no_vcg) add: isb_ccorres) 2168 apply (ctac (no_vcg) add: vcpu_enable_ccorres) 2169 apply (rule_tac v="(v, cactive)" in armHSCurVCPU_update_active_ccorres[simplified dc_def]) 2170 apply (simp add: from_bool_def true_def) 2171 apply simp 2172 apply wp 2173 apply (wpsimp wp: hoare_vcg_conj_lift vcpuSave_invs_no_cicd' vcpuSave_typ_at') 2174 (* ccactive =true *) 2175 apply (rule ccorres_return_Skip[unfolded dc_def]) 2176 (* last goal *) 2177 apply simp 2178 apply (rule conjI 2179 | clarsimp dest!: rf_sr_ksArchState_armHSCurVCPU 2180 simp: Collect_const_mem cur_vcpu_relation_def from_bool_def true_def 2181 | fastforce dest: invs_cicd_arch_state' split: option.splits 2182 simp: valid_arch_state'_def vcpu_at_is_vcpu' ko_wp_at'_def Collect_const_mem)+ 2183 done 2184 2185lemma vcpu_switch_ccorres: 2186 "ccorres dc xfdc 2187 (pspace_aligned' and pspace_distinct' and valid_objs' and no_0_obj' 2188 and valid_arch_state' 2189 and (case v of None \<Rightarrow> \<top> | Some new \<Rightarrow> vcpu_at' new)) 2190 (UNIV \<inter> {s. new_' s = option_to_ptr v (*(case v of None \<Rightarrow> NULL | Some new \<Rightarrow> vcpu_Ptr new)*) }) hs 2191 (vcpuSwitch v) (Call vcpu_switch_'proc)" 2192 by (cases v; clarsimp simp: vcpu_switch_ccorres_None[simplified] vcpu_switch_ccorres_Some[simplified]) 2193 2194 2195lemma invs_no_cicd_sym_hyp' [elim!]: 2196 "invs_no_cicd' s \<Longrightarrow> sym_refs (state_hyp_refs_of' s)" 2197 by (simp add: invs_no_cicd'_def valid_state'_def) 2198 2199lemma setVMRoot_ccorres: 2200 "ccorres dc xfdc 2201 (all_invs_but_ct_idle_or_in_cur_domain' and tcb_at' thread) 2202 (UNIV \<inter> {s. tcb_' s = tcb_ptr_to_ctcb_ptr thread}) [] 2203 (setVMRoot thread) (Call setVMRoot_'proc)" 2204 apply (cinit lift: tcb_') 2205 apply (rule ccorres_move_array_assertion_tcb_ctes) 2206 apply (rule ccorres_move_c_guard_tcb_ctes) 2207 apply (simp add: getThreadVSpaceRoot_def locateSlot_conv) 2208 apply (ctac) 2209 apply csymbr 2210 apply csymbr 2211 apply (simp add: if_1_0_0 cap_get_tag_isCap_ArchObject2 del: Collect_const) 2212 apply (rule ccorres_Cond_rhs_Seq) 2213 apply (simp add: cap_case_isPageDirectoryCap cong: if_cong) 2214 apply (rule ccorres_cond_true_seq) 2215 apply (rule ccorres_rhs_assoc) 2216 apply (simp add: throwError_def catch_def dc_def[symmetric]) 2217 apply (rule ccorres_rhs_assoc)+ 2218 apply (rule ccorres_h_t_valid_armUSGlobalPD) 2219 apply csymbr 2220 apply (rule ccorres_pre_gets_armUSGlobalPD_ksArchState[unfolded comp_def]) 2221 apply (rule ccorres_add_return2) 2222 apply (ctac (no_vcg) add: setCurrentPD_ccorres) 2223 apply (rule ccorres_split_throws) 2224 apply (rule ccorres_return_void_C) 2225 apply vcg 2226 apply wp 2227 apply (rule ccorres_rhs_assoc)+ 2228 apply csymbr 2229 apply csymbr 2230 apply (rule_tac P="to_bool (capPDIsMapped_CL (cap_page_directory_cap_lift threadRoot)) 2231 = (capPDMappedASID (capCap rv) \<noteq> None)" 2232 in ccorres_gen_asm2) 2233 apply (simp add: if_1_0_0 to_bool_def del: Collect_const) 2234 apply (rule ccorres_Cond_rhs_Seq) 2235 apply (simp add: cap_case_isPageDirectoryCap cong: if_cong) 2236 apply (simp add: throwError_def catch_def) 2237 apply (rule ccorres_rhs_assoc)+ 2238 apply (rule ccorres_h_t_valid_armUSGlobalPD) 2239 apply csymbr 2240 apply (rule ccorres_pre_gets_armUSGlobalPD_ksArchState[unfolded comp_def]) 2241 apply (rule ccorres_add_return2) 2242 apply (ctac (no_vcg) add: setCurrentPD_ccorres) 2243 apply (rule ccorres_split_throws) 2244 apply (rule ccorres_return_void_C [unfolded dc_def]) 2245 apply vcg 2246 apply wp 2247 apply (simp add: cap_case_isPageDirectoryCap) 2248 apply (simp add: catch_def) 2249 apply csymbr 2250 apply csymbr 2251 apply csymbr 2252 apply csymbr 2253 apply (simp add: liftE_bindE) 2254 apply (simp add: bindE_bind_linearise bind_assoc liftE_def) 2255 apply (rule_tac f'=lookup_failure_rel and r'="\<lambda>pdeptrc pdeptr. pdeptr = pde_Ptr pdeptrc" 2256 and xf'=find_ret_' 2257 in ccorres_split_nothrow_case_sum) 2258 apply (ctac add: findPDForASID_ccorres) 2259 apply ceqv 2260 apply (rule_tac P="capPDBasePtr_CL (cap_page_directory_cap_lift threadRoot) 2261 = capPDBasePtr (capCap rv)" 2262 in ccorres_gen_asm2) 2263 apply (simp del: Collect_const) 2264 apply (rule ccorres_Cond_rhs_Seq) 2265 apply (simp add: whenE_def throwError_def 2266 checkPDNotInASIDMap_def checkPDASIDMapMembership_def) 2267 apply (rule ccorres_stateAssert) 2268 apply (rule ccorres_pre_gets_armUSGlobalPD_ksArchState[unfolded o_def]) 2269 apply (rule ccorres_rhs_assoc)+ 2270 apply (rule ccorres_h_t_valid_armUSGlobalPD) 2271 apply csymbr 2272 apply (rule ccorres_add_return2) 2273 apply (ctac(no_vcg) add: setCurrentPD_ccorres) 2274 apply (rule ccorres_split_throws) 2275 apply (rule ccorres_return_void_C[unfolded dc_def]) 2276 apply vcg 2277 apply wp 2278 apply (simp add: whenE_def returnOk_def) 2279 apply (ctac (no_vcg) add: armv_contextSwitch_ccorres[unfolded dc_def]) 2280 apply (rule ccorres_move_c_guard_tcb) 2281 apply (rule ccorres_symb_exec_l3) 2282 apply (rename_tac tcb) 2283 apply (rule_tac P="ko_at' tcb thread" in ccorres_cross_over_guard) 2284 apply (ctac add: vcpu_switch_ccorres[unfolded dc_def]) (* c *) 2285 apply wp 2286 apply (wp getObject_tcb_wp) 2287 apply simp 2288 apply clarsimp 2289 apply (wp hoare_drop_imp hoare_vcg_ex_lift armv_contextSwitch_invs_no_cicd' valid_case_option_post_wp') 2290 apply (simp add: checkPDNotInASIDMap_def checkPDASIDMapMembership_def) 2291 apply (rule ccorres_stateAssert) 2292 apply (rule ccorres_rhs_assoc)+ 2293 apply (rule ccorres_pre_gets_armUSGlobalPD_ksArchState[unfolded o_def]) 2294 apply (rule ccorres_h_t_valid_armUSGlobalPD) 2295 apply csymbr 2296 apply (rule ccorres_add_return2) 2297 apply (ctac(no_vcg) add: setCurrentPD_ccorres) 2298 apply (rule ccorres_split_throws) 2299 apply (rule ccorres_return_void_C[unfolded dc_def]) 2300 apply vcg 2301 apply wp 2302 apply simp 2303 apply (wp hoare_drop_imps)[1] 2304 apply (simp add: Collect_const_mem) 2305 apply (vcg exspec=findPDForASID_modifies) 2306 apply (simp add: getSlotCap_def) 2307 apply (wp getCTE_wp') 2308 apply (clarsimp simp add: if_1_0_0 simp del: Collect_const) 2309 apply vcg 2310 apply (clarsimp simp: Collect_const_mem word_sle_def) 2311 apply (rule conjI) 2312 apply (clarsimp simp: all_invs_but_ct_idle_or_in_cur_domain'_def) 2313 apply (frule cte_wp_at_valid_objs_valid_cap', clarsimp+) 2314 apply (auto simp: isCap_simps valid_cap'_def mask_def dest!: tcb_ko_at')[1] 2315 apply (rule_tac x=ta in exI, auto split: option.splits)[1] 2316 apply (frule (2) sym_refs_tcb_vcpu', clarsimp) 2317 apply (clarsimp simp: obj_at'_def typ_at'_def ko_wp_at'_def projectKOs) 2318 apply (clarsimp simp: ptr_val_tcb_ptr_mask' 2319 size_of_def cte_level_bits_def 2320 tcbVTableSlot_def tcb_cnode_index_defs 2321 ccap_rights_relation_def cap_rights_to_H_def 2322 to_bool_def true_def allRights_def 2323 mask_def[where n="Suc 0"] 2324 cte_at_tcb_at_16' addrFromPPtr_def) 2325 apply (clarsimp simp: cap_get_tag_isCap_ArchObject2 2326 dest!: isCapDs) 2327 apply (clarsimp simp: cap_get_tag_isCap_ArchObject[symmetric] 2328 cap_lift_page_directory_cap cap_to_H_def 2329 cap_page_directory_cap_lift_def 2330 to_bool_def 2331 elim!: ccap_relationE split: if_split_asm) 2332 apply (rename_tac s'') 2333 apply (drule_tac s=s'' in obj_at_cslift_tcb, assumption) 2334 apply (clarsimp simp: typ_heap_simps) 2335 apply (clarsimp simp: ctcb_relation_def carch_tcb_relation_def) 2336 done 2337 2338(* FIXME: remove *) 2339lemmas invs'_invs_no_cicd = invs_invs_no_cicd' 2340 2341lemma setVMRootForFlush_ccorres: 2342 "ccorres (\<lambda>rv rv'. rv' = from_bool rv) ret__unsigned_long_' 2343 (invs' and (\<lambda>s. asid \<le> mask asid_bits)) 2344 (UNIV \<inter> {s. pd_' s = pde_Ptr pd} \<inter> {s. asid_' s = asid}) [] 2345 (setVMRootForFlush pd asid) (Call setVMRootForFlush_'proc)" 2346 apply (cinit lift: pd_' asid_') 2347 apply (rule ccorres_pre_getCurThread) 2348 apply (simp add: getThreadVSpaceRoot_def locateSlot_conv 2349 del: Collect_const) 2350 apply (rule ccorres_Guard_Seq)+ 2351 apply (ctac add: getSlotCap_h_val_ccorres) 2352 apply csymbr 2353 apply csymbr 2354 apply (simp add: cap_get_tag_isCap_ArchObject2 if_1_0_0 2355 del: Collect_const) 2356 apply (rule ccorres_if_lhs) 2357 apply (rule_tac P="(capPDIsMapped_CL (cap_page_directory_cap_lift threadRoot) = 0) 2358 = (capPDMappedASID (capCap rva) = None) 2359 \<and> capPDBasePtr_CL (cap_page_directory_cap_lift threadRoot) 2360 = capPDBasePtr (capCap rva)" in ccorres_gen_asm2) 2361 apply (rule ccorres_rhs_assoc | csymbr | simp add: Collect_True del: Collect_const)+ 2362 apply (rule ccorres_split_throws) 2363 apply (rule ccorres_return_C, simp+) 2364 apply vcg 2365 apply (rule ccorres_rhs_assoc2, 2366 rule ccorres_rhs_assoc2, 2367 rule ccorres_symb_exec_r) 2368 apply simp 2369 apply (ctac (no_vcg)add: armv_contextSwitch_ccorres) 2370 apply (ctac add: ccorres_return_C) 2371 apply wp 2372 apply (simp add: true_def from_bool_def) 2373 apply vcg 2374 apply (rule conseqPre, vcg) 2375 apply (simp add: Collect_const_mem) 2376 apply clarsimp 2377 apply simp 2378 apply (wp hoare_drop_imps) 2379 apply vcg 2380 apply (clarsimp simp: Collect_const_mem if_1_0_0 word_sle_def 2381 ccap_rights_relation_def cap_rights_to_H_def 2382 mask_def[where n="Suc 0"] true_def to_bool_def 2383 allRights_def size_of_def cte_level_bits_def 2384 tcbVTableSlot_def Kernel_C.tcbVTable_def invs'_invs_no_cicd) 2385 apply (clarsimp simp: rf_sr_ksCurThread ptr_add_assertion_positive) 2386 apply (subst rf_sr_tcb_ctes_array_assertion[THEN array_assertion_shrink_right], 2387 assumption, simp add: tcb_at_invs', simp add: tcb_cnode_index_defs)+ 2388 apply (clarsimp simp: rf_sr_ksCurThread ptr_val_tcb_ptr_mask' [OF tcb_at_invs']) 2389 apply (frule cte_at_tcb_at_16'[OF tcb_at_invs'], clarsimp simp: cte_wp_at_ctes_of) 2390 apply (rule cmap_relationE1[OF cmap_relation_cte], assumption+) 2391 apply (clarsimp simp: false_def true_def from_bool_def 2392 typ_heap_simps') 2393 apply (case_tac "isArchObjectCap rv \<and> isPageDirectoryCap (capCap rv)") 2394 apply (clarsimp simp: isCap_simps(2) cap_get_tag_isCap_ArchObject[symmetric]) 2395 apply (clarsimp simp: cap_page_directory_cap_lift cap_to_H_def 2396 elim!: ccap_relationE) 2397 apply (simp add: to_bool_def split: if_split) 2398 by (auto simp: cap_get_tag_isCap_ArchObject2) 2399 2400 2401 2402(* FIXME: move to StateRelation_C *) 2403definition 2404 "framesize_from_H sz \<equiv> case sz of 2405 ARM_HYP.ARMSmallPage \<Rightarrow> (scast Kernel_C.ARMSmallPage :: word32) 2406 | ARM_HYP.ARMLargePage \<Rightarrow> scast Kernel_C.ARMLargePage 2407 | ARM_HYP.ARMSection \<Rightarrow> scast Kernel_C.ARMSection 2408 | ARM_HYP.ARMSuperSection \<Rightarrow> scast Kernel_C.ARMSuperSection" 2409 2410lemma framesize_from_to_H: 2411 "gen_framesize_to_H (framesize_from_H sz) = sz" 2412 by (simp add: gen_framesize_to_H_def framesize_from_H_def 2413 Kernel_C.ARMSmallPage_def Kernel_C.ARMLargePage_def 2414 Kernel_C.ARMSection_def Kernel_C.ARMSuperSection_def 2415 split: if_split vmpage_size.splits) 2416 2417lemma framesize_from_H_mask: 2418 "framesize_from_H vmsz && mask 2 = framesize_from_H vmsz" 2419 by (simp add: framesize_from_H_def mask_def 2420 Kernel_C.ARMSmallPage_def Kernel_C.ARMLargePage_def 2421 Kernel_C.ARMSection_def Kernel_C.ARMSuperSection_def 2422 split: vmpage_size.splits) 2423 2424(* FIXME: move *) 2425 2426lemma dmo_invalidateCacheRange_RAM_invs'[wp]: 2427 "valid invs' (doMachineOp (invalidateCacheRange_RAM vs ve ps)) (\<lambda>rv. invs')" 2428 apply (wp dmo_invs' no_irq no_irq_invalidateCacheRange_RAM) 2429 apply (clarsimp simp: disj_commute[of "pointerInUserData p s" for p s]) 2430 apply (erule use_valid) 2431 apply (wp, simp) 2432 done 2433 2434lemma dmo_flushtype_case: 2435 "(doMachineOp (case t of 2436 ARM_HYP_H.flush_type.Clean \<Rightarrow> f 2437 | ARM_HYP_H.flush_type.Invalidate \<Rightarrow> g 2438 | ARM_HYP_H.flush_type.CleanInvalidate \<Rightarrow> h 2439 | ARM_HYP_H.flush_type.Unify \<Rightarrow> i)) = 2440 (case t of 2441 ARM_HYP_H.flush_type.Clean \<Rightarrow> doMachineOp f 2442 | ARM_HYP_H.flush_type.Invalidate \<Rightarrow> doMachineOp g 2443 | ARM_HYP_H.flush_type.CleanInvalidate \<Rightarrow> doMachineOp h 2444 | ARM_HYP_H.flush_type.Unify \<Rightarrow> doMachineOp i)" 2445 by (case_tac "t", simp_all) 2446 2447definition 2448 "flushtype_relation typ label \<equiv> case typ of 2449 ARM_HYP_H.flush_type.Clean \<Rightarrow> (label = Kernel_C.ARMPageClean_Data \<or> label = Kernel_C.ARMPDClean_Data) 2450 | ARM_HYP_H.flush_type.Invalidate \<Rightarrow>(label = Kernel_C.ARMPageInvalidate_Data \<or> label = Kernel_C.ARMPDInvalidate_Data) 2451 | ARM_HYP_H.flush_type.CleanInvalidate \<Rightarrow> (label = Kernel_C.ARMPageCleanInvalidate_Data \<or> label = Kernel_C.ARMPDCleanInvalidate_Data) 2452 | ARM_HYP_H.flush_type.Unify \<Rightarrow> (label = Kernel_C.ARMPageUnify_Instruction \<or> label = Kernel_C.ARMPDUnify_Instruction)" 2453 2454lemma ccorres_seq_IF_False: 2455 "ccorres_underlying sr \<Gamma> r xf arrel axf G G' hs a (IF False THEN x ELSE y FI ;; c) = ccorres_underlying sr \<Gamma> r xf arrel axf G G' hs a (y ;; c)" 2456 by simp 2457 2458lemma ptrFromPAddr_mask6_simp[simp]: 2459 "ptrFromPAddr ps && mask 6 = ps && mask 6" 2460 unfolding ptrFromPAddr_def physMappingOffset_def kernelBase_addr_def ARM_HYP.physBase_def 2461 by (subst add.commute, subst mask_add_aligned ; simp add: is_aligned_def) 2462 2463lemma doFlush_ccorres: 2464 "ccorres dc xfdc (\<lambda>s. vs \<le> ve \<and> ps \<le> ps + (ve - vs) \<and> vs && mask 6 = ps && mask 6 2465 (* hyp version translates ps into kernel virtual before flushing *) 2466 \<and> ptrFromPAddr ps \<le> ptrFromPAddr ps + (ve - vs) 2467 \<and> unat (ve - vs) \<le> gsMaxObjectSize s) 2468 (\<lbrace>flushtype_relation t \<acute>invLabel___int\<rbrace> \<inter> \<lbrace>\<acute>start = vs\<rbrace> \<inter> \<lbrace>\<acute>end = ve\<rbrace> \<inter> \<lbrace>\<acute>pstart = ps\<rbrace>) [] 2469 (doMachineOp (doFlush t vs ve ps)) (Call doFlush_'proc)" 2470 apply (cinit' lift: pstart_') 2471 apply (unfold doMachineOp_bind doFlush_def) 2472 apply (simp add: Let_def) 2473 apply (rule ccorres_Guard_Seq) 2474 apply (rule ccorres_basic_srnoop2, simp) 2475 apply (rule ccorres_rhs_assoc)+ 2476 apply csymbr 2477 apply (rule_tac xf'=end_' in ccorres_abstract, ceqv, rename_tac end') 2478 apply (rule_tac P="end' = ve" in ccorres_gen_asm2) 2479 apply (rule_tac xf'=start_' in ccorres_abstract, ceqv, rename_tac start') 2480 apply (rule_tac P="start' = vs" in ccorres_gen_asm2) 2481 apply csymbr 2482 apply csymbr 2483 apply csymbr 2484 apply (rule_tac xf'=invLabel___int_' in ccorres_abstract, ceqv, rename_tac invlabel) 2485 apply (rule_tac P="flushtype_relation t invlabel" in ccorres_gen_asm2) 2486 apply (simp only: dmo_flushtype_case Let_def) 2487 apply (wpc ; simp add: dc_def[symmetric]) 2488 apply (rule ccorres_cond_true) 2489 apply (ctac (no_vcg) add: cleanCacheRange_RAM_ccorres) 2490 apply (rule ccorres_cond_false) 2491 apply (rule ccorres_cond_true) 2492 apply (ctac (no_vcg) add: invalidateCacheRange_RAM_ccorres) 2493 apply (rule ccorres_cond_false) 2494 apply (rule ccorres_cond_false) 2495 apply (rule ccorres_cond_true) 2496 apply (ctac (no_vcg) add: cleanInvalidateCacheRange_RAM_ccorres) 2497 apply (rule ccorres_cond_false) 2498 apply (rule ccorres_cond_false) 2499 apply (rule ccorres_cond_false) 2500 apply (rule ccorres_cond_true) 2501 apply (simp add: empty_fail_cleanCacheRange_PoU empty_fail_dsb 2502 empty_fail_invalidateCacheRange_I empty_fail_branchFlushRange empty_fail_isb 2503 doMachineOp_bind) 2504 apply (rule ccorres_rhs_assoc)+ 2505 apply (fold dc_def) 2506 apply (ctac (no_vcg) add: cleanCacheRange_PoU_ccorres) 2507 apply (ctac (no_vcg) add: dsb_ccorres) 2508 apply (ctac (no_vcg) add: invalidateCacheRange_I_ccorres) 2509 apply (ctac (no_vcg) add: branchFlushRange_ccorres) 2510 apply (ctac (no_vcg) add: isb_ccorres) 2511 apply wp+ 2512 apply (clarsimp simp: Collect_const_mem) 2513 apply (auto simp: flushtype_relation_def o_def 2514 Kernel_C.ARMPageClean_Data_def Kernel_C.ARMPDClean_Data_def 2515 Kernel_C.ARMPageInvalidate_Data_def Kernel_C.ARMPDInvalidate_Data_def 2516 Kernel_C.ARMPageCleanInvalidate_Data_def Kernel_C.ARMPDCleanInvalidate_Data_def 2517 Kernel_C.ARMPageUnify_Instruction_def Kernel_C.ARMPDUnify_Instruction_def 2518 dest: ghost_assertion_size_logic[rotated] 2519 split: ARM_HYP_H.flush_type.splits) 2520 done 2521end 2522 2523context begin interpretation Arch . (*FIXME: arch_split*) 2524crunch gsMaxObjectSize[wp]: setVMRootForFlush "\<lambda>s. P (gsMaxObjectSize s)" 2525 (wp: crunch_wps) 2526end 2527 2528context kernel_m begin 2529 2530lemma performPageFlush_ccorres: 2531 "ccorres (K (K \<bottom>) \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') 2532 (invs' and K (asid \<le> mask asid_bits) 2533 and (\<lambda>s. ps \<le> ps + (ve - vs) \<and> vs && mask 6 = ps && mask 6 2534 \<and> ptrFromPAddr ps \<le> ptrFromPAddr ps + (ve - vs) 2535 \<and> unat (ve - vs) \<le> gsMaxObjectSize s)) 2536 (\<lbrace>\<acute>pd = Ptr pd\<rbrace> \<inter> \<lbrace>\<acute>asid = asid\<rbrace> \<inter> 2537 \<lbrace>\<acute>start = vs\<rbrace> \<inter> \<lbrace>\<acute>end = ve\<rbrace> \<inter> \<lbrace>\<acute>pstart = ps\<rbrace> \<inter> \<lbrace>flushtype_relation typ \<acute>invLabel___int \<rbrace>) 2538 [] 2539 (liftE (performPageInvocation (PageFlush typ vs ve ps pd asid))) 2540 (Call performPageFlush_'proc)" 2541 apply (simp only: liftE_liftM ccorres_liftM_simp) 2542 apply (cinit lift: pd_' asid_' start_' end_' pstart_' invLabel___int_') 2543 apply (unfold when_def) 2544 apply (rule ccorres_cond_seq) 2545 apply (rule ccorres_cond2[where R=\<top>]) 2546 apply (simp split: if_split) 2547 apply (rule ccorres_rhs_assoc)+ 2548 apply (ctac (no_vcg) add: setVMRootForFlush_ccorres) 2549 apply (ctac (no_vcg) add: doFlush_ccorres) 2550 apply (rule ccorres_add_return2) 2551 apply (rule ccorres_split_nothrow_novcg_dc) 2552 apply (rule ccorres_cond2[where R=\<top>]) 2553 apply (simp add: from_bool_def split: if_split bool.splits) 2554 apply (rule ccorres_pre_getCurThread) 2555 apply (ctac add: setVMRoot_ccorres) 2556 apply (rule ccorres_return_Skip) 2557 apply (rule_tac P=\<top> and P'=UNIV in ccorres_from_vcg_throws) 2558 apply (rule allI, rule conseqPre, vcg) 2559 apply (clarsimp simp: return_def) 2560 apply wp 2561 apply (simp add: guard_is_UNIV_def) 2562 apply (simp add: cur_tcb'_def[symmetric]) 2563 apply (rule_tac Q="\<lambda>_ s. invs' s \<and> cur_tcb' s" in hoare_post_imp) 2564 apply (simp add: invs'_invs_no_cicd) 2565 apply wp+ 2566 apply (simp) 2567 apply (rule_tac P=\<top> and P'=UNIV in ccorres_from_vcg_throws) 2568 apply (rule allI, rule conseqPre, vcg) 2569 apply (clarsimp simp: return_def) 2570 apply (clarsimp simp: order_less_imp_le) 2571 done 2572 2573(* FIXME: move *) 2574lemma register_from_H_bound[simp]: 2575 "unat (register_from_H v) < 20" 2576 by (cases v, simp_all add: "StrictC'_register_defs") 2577 2578(* FIXME: move *) 2579lemma register_from_H_inj: 2580 "inj register_from_H" 2581 apply (rule inj_onI) 2582 apply (case_tac x) 2583 by (case_tac y, simp_all add: "StrictC'_register_defs")+ 2584 2585(* FIXME: move *) 2586lemmas register_from_H_eq_iff[simp] 2587 = inj_on_eq_iff [OF register_from_H_inj, simplified] 2588 2589lemma setRegister_ccorres: 2590 "ccorres dc xfdc \<top> 2591 (UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace> \<inter> \<lbrace>\<acute>reg = register_from_H reg\<rbrace> 2592 \<inter> {s. w_' s = val}) [] 2593 (asUser thread (setRegister reg val)) 2594 (Call setRegister_'proc)" 2595 apply (cinit' lift: thread_' reg_' w_') 2596 apply (simp add: asUser_def dc_def[symmetric] split_def split del: if_split) 2597 apply (rule ccorres_pre_threadGet) 2598 apply (rule ccorres_Guard) 2599 apply (simp add: setRegister_def simpler_modify_def exec_select_f_singleton) 2600 apply (rule_tac P="\<lambda>tcb. (atcbContextGet o tcbArch) tcb = rv" 2601 in threadSet_ccorres_lemma2 [unfolded dc_def]) 2602 apply vcg 2603 apply (clarsimp simp: setRegister_def HaskellLib_H.runState_def 2604 simpler_modify_def typ_heap_simps) 2605 apply (subst StateSpace.state.fold_congs[OF refl refl]) 2606 apply (rule globals.fold_congs[OF refl refl]) 2607 apply (rule heap_update_field_hrs, simp) 2608 apply (fastforce intro: typ_heap_simps) 2609 apply simp 2610 apply (erule(1) rf_sr_tcb_update_no_queue2, 2611 (simp add: typ_heap_simps')+) 2612 apply (rule ball_tcb_cte_casesI, simp+) 2613 apply (clarsimp simp: ctcb_relation_def ccontext_relation_def 2614 atcbContextSet_def atcbContextGet_def 2615 carch_tcb_relation_def 2616 split: if_split) 2617 apply (clarsimp simp: Collect_const_mem register_from_H_sless 2618 register_from_H_less) 2619 apply (auto intro: typ_heap_simps elim: obj_at'_weakenE) 2620 done 2621 2622lemma msgRegisters_ccorres: 2623 "n < unat n_msgRegisters \<Longrightarrow> 2624 register_from_H (ARM_HYP_H.msgRegisters ! n) = (index kernel_all_substitute.msgRegisters n)" 2625 apply (simp add: kernel_all_substitute.msgRegisters_def msgRegisters_unfold fupdate_def) 2626 apply (simp add: Arrays.update_def n_msgRegisters_def fcp_beta nth_Cons' split: if_split) 2627 done 2628 2629(* usually when we call setMR directly, we mean to only set a registers, which will 2630 fit in actual registers *) 2631lemma setMR_as_setRegister_ccorres: 2632 notes dc_simp[simp del] 2633 shows 2634 "ccorres (\<lambda>rv rv'. rv' = of_nat offset + 1) ret__unsigned_' 2635 (tcb_at' thread and K (TCB_H.msgRegisters ! offset = reg \<and> offset < length msgRegisters)) 2636 (UNIV \<inter> \<lbrace>\<acute>reg = val\<rbrace> 2637 \<inter> \<lbrace>\<acute>offset = of_nat offset\<rbrace> 2638 \<inter> \<lbrace>\<acute>receiver = tcb_ptr_to_ctcb_ptr thread\<rbrace>) hs 2639 (asUser thread (setRegister reg val)) 2640 (Call setMR_'proc)" 2641 apply (rule ccorres_grab_asm) 2642 apply (cinit' lift: reg_' offset_' receiver_') 2643 apply (clarsimp simp: n_msgRegisters_def length_of_msgRegisters) 2644 apply (rule ccorres_cond_false) 2645 apply (rule ccorres_move_const_guards) 2646 apply (rule ccorres_add_return2) 2647 apply (ctac add: setRegister_ccorres) 2648 apply (rule ccorres_from_vcg_throws[where P'=UNIV and P=\<top>]) 2649 apply (rule allI, rule conseqPre, vcg) 2650 apply (clarsimp simp: dc_def return_def) 2651 apply (rule hoare_post_taut[of \<top>]) 2652 apply (vcg exspec=setRegister_modifies) 2653 apply (clarsimp simp: n_msgRegisters_def length_of_msgRegisters not_le conj_commute) 2654 apply (subst msgRegisters_ccorres[symmetric]) 2655 apply (clarsimp simp: n_msgRegisters_def length_of_msgRegisters unat_of_nat_eq) 2656 apply (clarsimp simp: word_less_nat_alt word_le_nat_alt unat_of_nat_eq not_le[symmetric]) 2657 done 2658 2659lemma wordFromMessageInfo_spec: 2660 defines "mil s \<equiv> seL4_MessageInfo_lift \<^bsup>s\<^esup>mi" 2661 shows "\<forall>s. \<Gamma> \<turnstile> {s} Call wordFromMessageInfo_'proc 2662 \<lbrace>\<acute>ret__unsigned_long = (label_CL (mil s) << 12) 2663 || (capsUnwrapped_CL (mil s) << 9) 2664 || (extraCaps_CL (mil s) << 7) 2665 || length_CL (mil s)\<rbrace>" 2666 unfolding mil_def 2667 apply vcg 2668 apply (simp add: seL4_MessageInfo_lift_def mask_shift_simps word_sless_def word_sle_def) 2669 apply word_bitwise 2670 done 2671 2672lemmas wordFromMessageInfo_spec2 = wordFromMessageInfo_spec 2673 2674lemma wordFromMessageInfo_ccorres [corres]: 2675 "\<And>mi. ccorres (=) ret__unsigned_long_' \<top> {s. mi = message_info_to_H (mi_' s)} [] 2676 (return (wordFromMessageInfo mi)) (Call wordFromMessageInfo_'proc)" 2677 apply (rule ccorres_from_spec_modifies [where P = \<top>, simplified]) 2678 apply (rule wordFromMessageInfo_spec) 2679 apply (rule wordFromMessageInfo_modifies) 2680 apply simp 2681 apply simp 2682 apply (simp add: return_def wordFromMessageInfo_def Let_def message_info_to_H_def 2683 Types_H.msgLengthBits_def Types_H.msgExtraCapBits_def 2684 Types_H.msgMaxExtraCaps_def shiftL_nat word_bw_assocs word_bw_comms word_bw_lcs) 2685 done 2686 2687(* FIXME move *) 2688lemma register_from_H_eq: 2689 "(r = r') = (register_from_H r = register_from_H r')" 2690 apply (case_tac r, simp_all add: C_register_defs) 2691 by (case_tac r', simp_all add: C_register_defs)+ 2692 2693lemma setMessageInfo_ccorres: 2694 "ccorres dc xfdc (tcb_at' thread) 2695 (UNIV \<inter> \<lbrace>mi = message_info_to_H mi'\<rbrace>) hs 2696 (setMessageInfo thread mi) 2697 (\<acute>ret__unsigned_long :== CALL wordFromMessageInfo(mi');; 2698 CALL setRegister(tcb_ptr_to_ctcb_ptr thread, scast Kernel_C.msgInfoRegister, \<acute>ret__unsigned_long))" 2699 unfolding setMessageInfo_def 2700 apply (rule ccorres_guard_imp2) 2701 apply ctac 2702 apply simp 2703 apply (ctac add: setRegister_ccorres) 2704 apply wp 2705 apply vcg 2706 apply (simp add: ARM_HYP_H.msgInfoRegister_def ARM_HYP.msgInfoRegister_def 2707 Kernel_C.msgInfoRegister_def Kernel_C.R1_def) 2708 done 2709 2710lemma performPageGetAddress_ccorres: 2711 "ccorres (K (K \<bottom>) \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') 2712 \<top> 2713 (UNIV \<inter> {s. vbase_ptr_' s = Ptr ptr}) [] 2714 (liftE (performPageInvocation (PageGetAddr ptr))) 2715 (Call performPageGetAddress_'proc)" 2716 apply (simp only: liftE_liftM ccorres_liftM_simp) 2717 apply (cinit lift: vbase_ptr_') 2718 apply csymbr 2719 apply (rule ccorres_pre_getCurThread) 2720 apply (clarsimp simp add: setMRs_def zipWithM_x_mapM_x mapM_x_Nil length_of_msgRegisters zip_singleton msgRegisters_unfold mapM_x_singleton) 2721 apply (ctac add: setRegister_ccorres) 2722 apply csymbr 2723 apply (rule ccorres_add_return2) 2724 apply (rule ccorres_rhs_assoc2) 2725 apply (rule ccorres_split_nothrow_novcg[where r'=dc and xf'=xfdc]) 2726 apply (unfold setMessageInfo_def) 2727 apply ctac 2728 apply (simp only: fun_app_def) 2729 apply (ctac add: setRegister_ccorres) 2730 apply wp 2731 apply vcg 2732 apply ceqv 2733 apply (rule_tac P=\<top> and P'=UNIV in ccorres_from_vcg_throws) 2734 apply (rule allI, rule conseqPre, vcg) 2735 apply (clarsimp simp: return_def) 2736 apply wp 2737 apply (simp add: guard_is_UNIV_def) 2738 apply wp 2739 apply vcg 2740 by (auto simp: ARM_HYP_H.fromPAddr_def message_info_to_H_def mask_def ARM_HYP_H.msgInfoRegister_def 2741 ARM_HYP.msgInfoRegister_def Kernel_C.msgInfoRegister_def Kernel_C.R1_def 2742 word_sle_def word_sless_def Kernel_C.R2_def 2743 kernel_all_global_addresses.msgRegisters_def fupdate_def Arrays.update_def 2744 fcp_beta) 2745 2746 2747lemma performPageDirectoryInvocationFlush_ccorres: 2748 "ccorres (K (K \<bottom>) \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') 2749 (invs' and K (asid \<le> mask asid_bits) 2750 and (\<lambda>s. ps \<le> ps + (ve - vs) \<and> vs && mask 6 = ps && mask 6 2751 \<and> ptrFromPAddr ps \<le> ptrFromPAddr ps + (ve - vs) 2752 \<and> unat (ve - vs) \<le> gsMaxObjectSize s)) 2753 (\<lbrace>\<acute>pd = Ptr pd\<rbrace> \<inter> \<lbrace>\<acute>asid = asid\<rbrace> \<inter> 2754 \<lbrace>\<acute>start = vs\<rbrace> \<inter> \<lbrace>\<acute>end = ve\<rbrace> \<inter> \<lbrace>\<acute>pstart = ps\<rbrace> \<inter> \<lbrace>flushtype_relation typ \<acute>invLabel___int \<rbrace>) 2755 [] 2756 (liftE (performPageDirectoryInvocation (PageDirectoryFlush typ vs ve ps pd asid))) 2757 (Call performPDFlush_'proc)" 2758 apply (simp only: liftE_liftM ccorres_liftM_simp) 2759 apply (cinit lift: pd_' asid_' start_' end_' pstart_' invLabel___int_') 2760 apply (unfold when_def) 2761 apply (rule ccorres_cond_seq) 2762 apply (rule ccorres_cond2[where R=\<top>]) 2763 apply (simp split: if_split) 2764 apply (rule ccorres_rhs_assoc)+ 2765 apply (ctac (no_vcg) add: setVMRootForFlush_ccorres) 2766 apply (ctac (no_vcg) add: doFlush_ccorres) 2767 apply (rule ccorres_add_return2) 2768 apply (rule ccorres_split_nothrow_novcg_dc) 2769 apply (rule ccorres_cond2[where R=\<top>]) 2770 apply (simp add: from_bool_def split: if_split bool.splits) 2771 apply (rule ccorres_pre_getCurThread) 2772 apply (ctac add: setVMRoot_ccorres) 2773 apply (rule ccorres_return_Skip) 2774 apply (rule_tac P=\<top> and P'=UNIV in ccorres_from_vcg_throws) 2775 apply (rule allI, rule conseqPre, vcg) 2776 apply (clarsimp simp: return_def) 2777 apply wp 2778 apply (simp add: guard_is_UNIV_def) 2779 apply (simp add: cur_tcb'_def[symmetric]) 2780 apply (rule_tac Q="\<lambda>_ s. invs' s \<and> cur_tcb' s" in hoare_post_imp) 2781 apply (simp add: invs'_invs_no_cicd) 2782 apply wp+ 2783 apply (simp) 2784 apply (rule_tac P=\<top> and P'=UNIV in ccorres_from_vcg_throws) 2785 apply (rule allI, rule conseqPre, vcg) 2786 apply (clarsimp simp: return_def) 2787 apply (clarsimp simp: order_less_imp_le) 2788 done 2789 2790lemma invalidateTranslationSingleLocal_ccorres: 2791 "ccorres dc xfdc \<top> (\<lbrace>\<acute>vptr = w\<rbrace>) [] 2792 (doMachineOp (invalidateLocalTLB_VAASID w)) 2793 (Call invalidateTranslationSingleLocal_'proc)" 2794 apply cinit' 2795 apply (ctac (no_vcg) add: invalidateLocalTLB_VAASID_ccorres) 2796 apply clarsimp 2797 done 2798 2799lemma invalidateTranslationSingle_ccorres: 2800 "ccorres dc xfdc \<top> (\<lbrace>\<acute>vptr = w\<rbrace>) [] 2801 (doMachineOp (invalidateLocalTLB_VAASID w)) 2802 (Call invalidateTranslationSingle_'proc)" 2803 apply cinit' 2804 apply (ctac (no_vcg) add: invalidateTranslationSingleLocal_ccorres) 2805 apply clarsimp 2806 done 2807 2808lemma flushPage_ccorres: 2809 "ccorres dc xfdc (invs' and (\<lambda>s. asid \<le> mask asid_bits \<and> is_aligned vptr pageBits)) 2810 (UNIV \<inter> {s. gen_framesize_to_H (page_size_' s) = sz 2811 \<and> page_size_' s < 4} 2812 \<inter> {s. pd_' s = pde_Ptr pd} \<inter> {s. asid_' s = asid} 2813 \<inter> {s. vptr_' s = vptr}) [] 2814 (flushPage sz pd asid vptr) (Call flushPage_'proc)" 2815 apply (cinit lift: page_size_' pd_' asid_' vptr_') 2816 apply (rule ccorres_assert) 2817 apply (simp del: Collect_const) 2818 apply (ctac(no_vcg) add: setVMRootForFlush_ccorres) 2819 apply (ctac(no_vcg) add: loadHWASID_ccorres) 2820 apply csymbr 2821 apply (simp add: when_def del: Collect_const) 2822 apply (rule ccorres_cond2[where R=\<top>]) 2823 apply (clarsimp simp: pde_stored_asid_def to_bool_def split: if_split) 2824 apply (rule ccorres_Guard_Seq ccorres_rhs_assoc)+ 2825 apply csymbr 2826 apply csymbr 2827 apply (ctac(no_vcg) add: invalidateTranslationSingle_ccorres) 2828 apply (rule ccorres_cond2[where R=\<top>]) 2829 apply (simp add: from_bool_0 Collect_const_mem) 2830 apply (rule ccorres_pre_getCurThread) 2831 apply (fold dc_def) 2832 apply (ctac add: setVMRoot_ccorres) 2833 apply (rule ccorres_return_Skip) 2834 apply (wp | simp add: cur_tcb'_def[symmetric])+ 2835 apply (rule_tac Q="\<lambda>_ s. invs' s \<and> cur_tcb' s" in hoare_post_imp) 2836 apply (simp add: invs'_invs_no_cicd) 2837 apply (wp | simp add: cur_tcb'_def[symmetric])+ 2838 apply (rule ccorres_return_Skip) 2839 apply wp 2840 apply (simp only: pred_conj_def simp_thms) 2841 apply (strengthen invs_valid_pde_mappings') 2842 apply (wp hoare_drop_imps setVMRootForFlush_invs') 2843 apply (clarsimp simp: Collect_const_mem word_sle_def) 2844 apply (rule conjI, clarsimp+) 2845 apply (clarsimp simp: pde_stored_asid_def to_bool_def cong: conj_cong 2846 ucast_ucast_mask) 2847 apply (drule is_aligned_neg_mask_eq) 2848 apply (simp add: pde_pde_invalid_lift_def pde_lift_def mask_def[where n=8] 2849 word_bw_assocs mask_def[where n=pageBits]) 2850 apply (simp add: pageBits_def mask_eq_iff_w2p word_size) 2851 done 2852 2853lemma ignoreFailure_liftM: 2854 "ignoreFailure = liftM (\<lambda>v. ())" 2855 apply (rule ext)+ 2856 apply (simp add: ignoreFailure_def liftM_def 2857 catch_def) 2858 apply (rule bind_apply_cong[OF refl]) 2859 apply (simp split: sum.split) 2860 done 2861 2862lemma ccorres_pre_getObject_pte: 2863 assumes cc: "\<And>rv. ccorres r xf (P rv) (P' rv) hs (f rv) c" 2864 shows "ccorres r xf 2865 (\<lambda>s. (\<forall>pte. ko_at' pte p s \<longrightarrow> P pte s)) 2866 {s. \<forall>pte pte'. cslift s (pte_Ptr p) = Some pte' \<and> cpte_relation pte pte' 2867 \<longrightarrow> s \<in> P' pte} 2868 hs (getObject p >>= (\<lambda>rv. f rv)) c" 2869 apply (rule ccorres_guard_imp2) 2870 apply (rule ccorres_symb_exec_l) 2871 apply (rule ccorres_guard_imp2) 2872 apply (rule cc) 2873 apply (rule conjI) 2874 apply (rule_tac Q="ko_at' rv p s" in conjunct1) 2875 apply assumption 2876 apply assumption 2877 apply (wp getPTE_wp empty_fail_getObject | simp)+ 2878 apply clarsimp 2879 apply (erule cmap_relationE1 [OF rf_sr_cpte_relation], 2880 erule ko_at_projectKO_opt) 2881 apply simp 2882 done 2883 2884lemmas unfold_checkMapping_return 2885 = from_bool_0[where 'a=32, folded exception_defs] 2886 to_bool_def 2887 2888end 2889 2890context begin interpretation Arch . (*FIXME: arch_split*) 2891crunch no_0_obj'[wp]: flushPage "no_0_obj'" 2892end 2893 2894context kernel_m begin 2895 2896lemma checkMappingPPtr_pte_ccorres: 2897 assumes pre: 2898 "\<And>pte \<sigma>. \<Gamma> \<turnstile> {s. True \<and> (\<exists>pte'. cslift s (pte_Ptr pte_ptr) = Some pte' \<and> cpte_relation pte pte') 2899 \<and> (\<sigma>, s) \<in> rf_sr} 2900 call1 ;; Cond S return_void_C Skip;; call2;; Cond T return_void_C Skip 2901 {s. (\<sigma>, s) \<in> rf_sr \<and> (isSmallPagePTE pte \<and> pgsz = ARMSmallPage 2902 \<or> isLargePagePTE pte \<and> pgsz = ARMLargePage) 2903 \<and> pteFrame pte = addrFromPPtr pptr}, 2904 {s. (\<sigma>, s) \<in> rf_sr \<and> \<not> ((isSmallPagePTE pte \<and> pgsz = ARMSmallPage 2905 \<or> isLargePagePTE pte \<and> pgsz = ARMLargePage) 2906 \<and> pteFrame pte = addrFromPPtr pptr)}" 2907 shows 2908 "ccorres_underlying rf_sr \<Gamma> (inr_rrel dc) xfdc (inl_rrel dc) xfdc 2909 \<top> UNIV [SKIP] 2910 (checkMappingPPtr pptr pgsz (Inl pte_ptr)) 2911 (call1;; Cond S return_void_C Skip;; call2;; Cond T return_void_C Skip)" 2912 apply (simp add: checkMappingPPtr_def liftE_bindE) 2913 apply (rule ccorres_symb_exec_l[where Q'="\<lambda>_. UNIV", OF _ _ getObject_ko_at, simplified]) 2914 apply (rule stronger_ccorres_guard_imp) 2915 apply (rule ccorres_from_vcg_might_throw[where P=\<top>]) 2916 apply (rule allI) 2917 apply (rule conseqPost, rule conseqPre, rule_tac \<sigma>1=\<sigma> and pte1=rv in pre) 2918 apply clarsimp 2919 apply (erule CollectE, assumption) 2920 apply (fold_subgoals (prefix))[2] 2921 subgoal by (auto simp: in_monad Bex_def isSmallPagePTE_def isLargePagePTE_def 2922 split: pte.split vmpage_size.split) 2923 apply (wp empty_fail_getObject | simp)+ 2924 apply (erule cmap_relationE1[OF rf_sr_cpte_relation]) 2925 apply (erule ko_at_projectKO_opt) 2926 apply simp 2927 apply (wp empty_fail_getObject | simp add: objBits_simps archObjSize_def table_bits_defs)+ 2928 done 2929 2930lemma checkMappingPPtr_pde_ccorres: 2931 assumes pre: 2932 "\<And>pde \<sigma>. \<Gamma> \<turnstile> {s. True \<and> (\<exists>pde'. cslift s (pde_Ptr pde_ptr) = Some pde' \<and> cpde_relation pde pde') 2933 \<and> (\<sigma>, s) \<in> rf_sr} 2934 call1;; Cond S return_void_C Skip;; call2;; Cond T return_void_C Skip;; 2935 call3;; Cond U return_void_C Skip 2936 {s. (\<sigma>, s) \<in> rf_sr \<and> (isSectionPDE pde \<and> pgsz = ARMSection 2937 \<or> isSuperSectionPDE pde \<and> pgsz = ARMSuperSection) 2938 \<and> pdeFrame pde = addrFromPPtr pptr}, 2939 {s. (\<sigma>, s) \<in> rf_sr \<and> \<not> ((isSectionPDE pde \<and> pgsz = ARMSection 2940 \<or> isSuperSectionPDE pde \<and> pgsz = ARMSuperSection) 2941 \<and> pdeFrame pde = addrFromPPtr pptr)}" 2942 shows 2943 "ccorres_underlying rf_sr \<Gamma> (inr_rrel dc) xfdc (inl_rrel dc) xfdc 2944 \<top> UNIV [SKIP] 2945 (checkMappingPPtr pptr pgsz (Inr pde_ptr)) 2946 (call1;; Cond S return_void_C Skip;; call2;; Cond T return_void_C Skip;; 2947 call3;; Cond U return_void_C Skip)" 2948 apply (simp add: checkMappingPPtr_def liftE_bindE) 2949 apply (rule ccorres_symb_exec_l[where Q'="\<lambda>_. UNIV", OF _ _ getObject_ko_at, simplified]) 2950 apply (rule stronger_ccorres_guard_imp) 2951 apply (rule ccorres_from_vcg_might_throw[where P=\<top>]) 2952 apply (rule allI) 2953 apply (rule conseqPost, rule conseqPre, rule_tac \<sigma>1=\<sigma> and pde1=rv in pre) 2954 apply clarsimp 2955 apply (erule CollectE, assumption) 2956 apply (fold_subgoals (prefix))[2] 2957 subgoal by (auto simp: in_monad Bex_def isSectionPDE_def isSuperSectionPDE_def 2958 split: pde.split vmpage_size.split) 2959 apply (wp empty_fail_getObject | simp)+ 2960 apply (erule cmap_relationE1[OF rf_sr_cpde_relation]) 2961 apply (erule ko_at_projectKO_opt) 2962 apply simp 2963 apply (wp empty_fail_getObject | simp add: objBits_simps archObjSize_def table_bits_defs)+ 2964 done 2965 2966 2967 2968lemma ccorres_return_void_C': 2969 "ccorres_underlying rf_sr \<Gamma> (inr_rrel dc) xfdc (inl_rrel dc) xfdc (\<lambda>_. True) UNIV (SKIP # hs) (return (Inl rv)) return_void_C" 2970 apply (rule ccorres_from_vcg_throws) 2971 apply (simp add: return_def) 2972 apply (rule allI, rule conseqPre, vcg) 2973 apply auto 2974 done 2975 2976lemma is_aligned_cache_preconds: 2977 "\<lbrakk>is_aligned rva n; n \<ge> 7\<rbrakk> \<Longrightarrow> rva \<le> rva + 0x7F \<and> 2978 addrFromPPtr rva \<le> addrFromPPtr rva + 0x7F \<and> rva && mask 6 = addrFromPPtr rva && mask 6" 2979 apply (drule is_aligned_weaken, simp) 2980 apply (rule conjI) 2981 apply (drule is_aligned_no_overflow, simp, unat_arith)[1] 2982 apply (rule conjI) 2983 apply (drule is_aligned_addrFromPPtr_n, simp) 2984 apply (drule is_aligned_no_overflow, unat_arith) 2985 apply (frule is_aligned_addrFromPPtr_n, simp) 2986 apply (drule_tac x=7 and y=6 in is_aligned_weaken, simp)+ 2987 apply (simp add: is_aligned_mask) 2988 done 2989 2990lemma pte_pte_invalid_new_spec: 2991 "\<forall>s. \<Gamma> \<turnstile> {s} 2992 \<acute>ret__struct_pte_C :== PROC pte_pte_invalid_new() 2993 \<lbrace> pte_lift \<acute>ret__struct_pte_C = Some Pte_pte_invalid \<rbrace>" 2994 apply (hoare_rule HoarePartial.ProcNoRec1) (* force vcg to unfold non-recursive procedure *) 2995 apply vcg 2996 apply (clarsimp simp: pte_pte_invalid_new_body_def pte_pte_invalid_new_impl 2997 pte_lift_def Let_def pte_get_tag_def pte_tag_defs) 2998 done 2999 3000lemma multiple_add_less_nat: 3001 "a < (c :: nat) \<Longrightarrow> x dvd a \<Longrightarrow> x dvd c \<Longrightarrow> b < x 3002 \<Longrightarrow> a + b < c" 3003 apply (subgoal_tac "b < c - a") 3004 apply simp 3005 apply (erule order_less_le_trans) 3006 apply (rule dvd_imp_le) 3007 apply simp 3008 apply simp 3009 done 3010 3011(* 7 = log2 (pte size * 16), where pte size is 8 3012 496 = number of entries in pt - 16, where number of entries is 512 *) 3013lemma large_ptSlot_array_constraint: 3014 "is_aligned (ptSlot :: word32) 7 \<Longrightarrow> n \<le> limit - 496 \<and> 496 \<le> limit 3015 \<Longrightarrow> \<exists>i. ptSlot = (ptSlot && ~~ mask ptBits) + of_nat i * 8 \<and> i + n \<le> limit" 3016 apply (rule_tac x="unat ((ptSlot && mask ptBits) >> 3)" in exI) 3017 apply (simp add: shiftl_t2n[where n=3, symmetric, THEN trans[rotated], 3018 OF mult.commute, simplified]) 3019 apply (simp add: shiftr_shiftl1) 3020 apply (rule conjI, rule trans, 3021 rule word_plus_and_or_coroll2[symmetric, where w="mask ptBits"]) 3022 apply (simp, rule is_aligned_neg_mask_eq[THEN sym], rule is_aligned_andI1, 3023 erule is_aligned_weaken, simp) 3024 apply (clarsimp simp add: le_diff_conv2) 3025 apply (erule order_trans[rotated], simp) 3026 apply (rule unat_le_helper) 3027 apply (simp add: is_aligned_mask mask_def table_bits_defs) 3028 apply (word_bitwise, simp?) 3029 done 3030 3031(* pde size is 8 3032 2032 = number of entries in pd - 16, where number of entries is 2048 *) 3033lemma large_pdSlot_array_constraint: 3034 "is_aligned pd pdBits \<Longrightarrow> vmsz_aligned vptr ARMSuperSection \<Longrightarrow> n \<le> limit - 2032 \<and> 2032 \<le> limit 3035 \<Longrightarrow> \<exists>i. lookup_pd_slot pd vptr = pd + of_nat i * 8 \<and> i + n \<le> limit" 3036 apply (rule_tac x="unat (vptr >> 21)" in exI) 3037 apply (rule conjI) 3038 apply (simp add: lookup_pd_slot_def shiftl_t2n table_bits_defs) 3039 apply (clarsimp simp add: le_diff_conv2) 3040 apply (erule order_trans[rotated], simp) 3041 apply (rule unat_le_helper) 3042 apply (simp add: is_aligned_mask mask_def table_bits_defs 3043 vmsz_aligned_def) 3044 apply (word_bitwise, simp?) 3045 done 3046 3047lemma findPDForASID_page_directory_at'_simple[wp]: 3048 notes checkPDAt_inv[wp del] 3049 shows "\<lbrace>\<top>\<rbrace> findPDForASID asiv 3050 \<lbrace>\<lambda>rv s. page_directory_at' rv s\<rbrace>,-" 3051 apply (simp add:findPDForASID_def) 3052 apply (wp getASID_wp|simp add:checkPDAt_def | wpc)+ 3053 apply auto? 3054 done 3055 3056lemma array_assertion_abs_pte_16: 3057 "\<forall>s s'. (s, s') \<in> rf_sr \<and> (page_table_at' (ptr_val ptPtr && ~~ mask ptBits) s 3058 \<and> is_aligned (ptr_val ptPtr) 7) \<and> (n s' \<le> 16 \<and> (x s' \<noteq> 0 \<longrightarrow> n s' \<noteq> 0)) 3059 \<longrightarrow> (x s' = 0 \<or> array_assertion (ptPtr :: pte_C ptr) (n s') (hrs_htd (t_hrs_' (globals s'))))" 3060 apply (intro allI impI disjCI2, clarsimp) 3061 apply (drule(1) page_table_at_rf_sr, clarsimp) 3062 apply (cases ptPtr, simp) 3063 apply (erule clift_array_assertion_imp, simp_all) 3064 apply (rule large_ptSlot_array_constraint, simp_all) 3065 done 3066 3067lemmas ccorres_move_array_assertion_pte_16 3068 = ccorres_move_array_assertions [OF array_assertion_abs_pte_16] 3069 3070lemma array_assertion_abs_pde_16: 3071 "\<forall>s s'. (s, s') \<in> rf_sr \<and> (page_directory_at' pd s 3072 \<and> vmsz_aligned vptr ARMSuperSection) \<and> (n s' \<le> 16 \<and> (x s' \<noteq> 0 \<longrightarrow> n s' \<noteq> 0)) 3073 \<longrightarrow> (x s' = 0 \<or> array_assertion (pde_Ptr (lookup_pd_slot pd vptr)) (n s') (hrs_htd (t_hrs_' (globals s'))))" 3074 apply (intro allI impI disjCI2, clarsimp) 3075 apply (frule(1) page_directory_at_rf_sr, clarsimp) 3076 apply (erule clift_array_assertion_imp, simp_all) 3077 apply (rule large_pdSlot_array_constraint, simp_all add: page_directory_at'_def) 3078 done 3079 3080lemmas array_assertion_abs_pde_16_const = array_assertion_abs_pde_16[where x="\<lambda>_. Suc 0", 3081 simplified nat.simps simp_thms] 3082 3083lemmas ccorres_move_array_assertion_pde_16 3084 = ccorres_move_Guard_Seq [OF array_assertion_abs_pde_16] 3085 ccorres_move_Guard [OF array_assertion_abs_pde_16] 3086 ccorres_move_Guard_Seq [OF array_assertion_abs_pde_16] 3087 ccorres_move_Guard [OF array_assertion_abs_pde_16] 3088 ccorres_move_Guard_Seq [OF array_assertion_abs_pde_16_const] 3089 ccorres_move_Guard [OF array_assertion_abs_pde_16_const] 3090 ccorres_move_Guard_Seq [OF array_assertion_abs_pde_16_const] 3091 ccorres_move_Guard [OF array_assertion_abs_pde_16_const] 3092 3093lemma unmapPage_ccorres: 3094 "ccorres dc xfdc (invs' and (\<lambda>s. 2 ^ pageBitsForSize sz \<le> gsMaxObjectSize s) 3095 and (\<lambda>_. asid \<le> mask asid_bits \<and> vmsz_aligned' vptr sz 3096 \<and> vptr < kernelBase)) 3097 (UNIV \<inter> {s. gen_framesize_to_H (page_size_' s) = sz \<and> page_size_' s < 4} 3098 \<inter> {s. asid_' s = asid} \<inter> {s. vptr_' s = vptr} \<inter> {s. pptr_' s = Ptr pptr}) [] 3099 (unmapPage sz asid vptr pptr) (Call unmapPage_'proc)" 3100 apply (rule ccorres_gen_asm) 3101 apply (cinit lift: page_size_' asid_' vptr_' pptr_') 3102 apply (simp add: ignoreFailure_liftM ptr_add_assertion_positive 3103 Collect_True 3104 del: Collect_const) 3105 apply ccorres_remove_UNIV_guard 3106 apply csymbr 3107 apply (ctac add: findPDForASID_ccorres) 3108 apply (rename_tac pdPtr pd') 3109 apply (rule_tac P="page_directory_at' pdPtr" in ccorres_cross_over_guard) 3110 apply (simp add: liftE_bindE Collect_False bind_bindE_assoc 3111 del: Collect_const) 3112 apply (rule ccorres_splitE_novcg[where r'=dc and xf'=xfdc]) 3113 \<comment> \<open>ARMSmallPage\<close> 3114 apply (rule ccorres_Cond_rhs) 3115 apply (simp add: gen_framesize_to_H_def dc_def[symmetric]) 3116 apply (rule ccorres_rhs_assoc)+ 3117 apply csymbr 3118 apply (ctac add: lookupPTSlot_ccorres) 3119 apply (rename_tac pt_slot pt_slot') 3120 apply (simp add: dc_def[symmetric]) 3121 apply (rule ccorres_rhs_assoc2, rule ccorres_rhs_assoc2, 3122 rule ccorres_rhs_assoc2, rule ccorres_rhs_assoc2, 3123 rule ccorres_rhs_assoc2) 3124 apply (rule ccorres_splitE_novcg) 3125 apply (simp only: inl_rrel_inl_rrel) 3126 apply (rule checkMappingPPtr_pte_ccorres) 3127 apply (rule conseqPre, vcg) 3128 apply (clarsimp simp: typ_heap_simps') 3129 apply (simp add: cpte_relation_def Let_def pte_lift_def 3130 isSmallPagePTE_def pte_tag_defs 3131 pte_pte_small_lift_def 3132 split: if_split_asm pte.split_asm) 3133 apply (rule ceqv_refl) 3134 apply (simp add: unfold_checkMapping_return liftE_liftM 3135 Collect_const[symmetric] dc_def[symmetric] 3136 del: Collect_const) 3137 apply (rule ccorres_handlers_weaken2) 3138 apply csymbr 3139 apply (rule ccorres_split_nothrow_novcg_dc) 3140 apply (rule storePTE_Basic_ccorres) 3141 apply (simp add: cpte_relation_def Let_def) 3142 apply csymbr 3143 apply simp 3144 apply (ctac add: cleanByVA_PoU_ccorres[unfolded dc_def]) 3145 apply wp 3146 apply (simp add: guard_is_UNIV_def) 3147 apply wp 3148 apply (simp add: ccHoarePost_def guard_is_UNIV_def) 3149 apply (simp add: throwError_def) 3150 apply (rule ccorres_split_throws) 3151 apply (rule ccorres_return_void_C') 3152 apply vcg 3153 apply (wp) 3154 apply simp 3155 apply (vcg exspec=lookupPTSlot_modifies) 3156 \<comment> \<open>ARMLargePage\<close> 3157 apply (rule ccorres_Cond_rhs) 3158 apply (simp add: gen_framesize_to_H_def dc_def[symmetric]) 3159 apply (rule ccorres_rhs_assoc)+ 3160 apply csymbr 3161 apply csymbr 3162 apply (ctac add: lookupPTSlot_ccorres) 3163 apply (rename_tac ptSlot lookupPTSlot_ret) 3164 apply (simp add: Collect_False dc_def[symmetric] del: Collect_const) 3165 apply (rule ccorres_rhs_assoc2, rule ccorres_rhs_assoc2, 3166 rule ccorres_rhs_assoc2, rule ccorres_rhs_assoc2, 3167 rule ccorres_rhs_assoc2) 3168 apply (rule ccorres_splitE_novcg, simp only: inl_rrel_inl_rrel, 3169 rule checkMappingPPtr_pte_ccorres) 3170 apply (rule conseqPre, vcg) 3171 apply (clarsimp simp: typ_heap_simps') 3172 subgoal by (simp add: cpte_relation_def Let_def pte_lift_def 3173 isLargePagePTE_def pte_tag_defs 3174 pte_pte_small_lift_def 3175 split: if_split_asm pte.split_asm) 3176 apply (rule ceqv_refl) 3177 apply (simp add: liftE_liftM dc_def[symmetric] 3178 mapM_discarded whileAnno_def ARMLargePageBits_def ARMSmallPageBits_def 3179 Collect_False unfold_checkMapping_return word_sle_def 3180 del: Collect_const) 3181 apply (ccorres_remove_UNIV_guard) 3182 apply (rule ccorres_rhs_assoc2) 3183 apply (rule ccorres_split_nothrow_novcg) 3184 apply (rule_tac P="is_aligned ptSlot 7" in ccorres_gen_asm) 3185 apply (rule_tac F="\<lambda>_. page_table_at' (ptSlot && ~~ mask ptBits)" 3186 in ccorres_mapM_x_while) 3187 apply clarsimp 3188 apply (rule ccorres_guard_imp2) 3189 apply csymbr 3190 apply (rule ccorres_move_array_assertion_pte_16) 3191 apply (rule ccorres_flip_Guard, rule ccorres_move_array_assertion_pte_16) 3192 apply (rule storePTE_Basic_ccorres) 3193 apply (simp add: cpte_relation_def Let_def) 3194 apply clarsimp 3195 apply (simp add: unat_of_nat upto_enum_word of_nat_gt_0 3196 largePagePTEOffsets_def Let_def table_bits_defs 3197 upto_enum_step_def del: upt.simps) 3198 apply (simp add: upto_enum_step_def largePagePTEOffsets_def Let_def 3199 table_bits_defs) 3200 apply (rule allI, rule conseqPre, vcg) 3201 apply clarsimp 3202 apply wp 3203 apply (simp add: upto_enum_step_def word_bits_def largePagePTEOffsets_def 3204 Let_def table_bits_defs) 3205 apply ceqv 3206 apply (rule ccorres_handlers_weaken2) 3207 apply (rule ccorres_move_c_guard_pte) 3208 apply csymbr 3209 apply (rule ccorres_move_c_guard_pte ccorres_move_array_assertion_pte_16)+ 3210 apply (rule ccorres_add_return2, 3211 ctac(no_vcg) add: cleanCacheRange_PoU_ccorres[unfolded dc_def]) 3212 apply (rule ccorres_move_array_assertion_pte_16, rule ccorres_return_Skip') 3213 apply wp 3214 apply (rule_tac P="is_aligned ptSlot 7" in hoare_gen_asm) 3215 apply (rule hoare_strengthen_post) 3216 apply (rule hoare_vcg_conj_lift) 3217 apply (rule_tac P="\<lambda>s. page_table_at' (ptSlot && ~~ mask ptBits) s 3218 \<and> 2 ^ pageBitsForSize sz \<le> gsMaxObjectSize s" 3219 in mapM_x_wp') 3220 apply wp[1] 3221 apply (rule mapM_x_accumulate_checks) 3222 apply (simp add: storePTE_def wordsFromPTE_def) 3223 apply (rule obj_at_setObject3) 3224 apply simp 3225 apply (simp add: objBits_simps archObjSize_def table_bits_defs) 3226 apply (simp add: typ_at_to_obj_at_arches[symmetric]) 3227 apply wp 3228 apply clarify 3229 apply (subgoal_tac "P" for P) 3230 apply (frule bspec, erule hd_in_set) 3231 apply (frule bspec, erule last_in_set) 3232 subgoal by (simp add: upto_enum_step_def upto_enum_word 3233 hd_map last_map typ_at_to_obj_at_arches field_simps 3234 objBits_simps archObjSize_def largePagePTEOffsets_def 3235 Let_def table_bits_defs, 3236 clarsimp dest!: is_aligned_cache_preconds) 3237 apply (simp add: upto_enum_step_def upto_enum_word largePagePTEOffsets_def Let_def) 3238 apply (clarsimp simp: guard_is_UNIV_def Collect_const_mem) 3239 apply (simp add: hd_map last_map upto_enum_step_def objBits_simps archObjSize_def 3240 upto_enum_word largePagePTEOffsets_def Let_def table_bits_defs) 3241 apply wp 3242 apply (simp add: guard_is_UNIV_def) 3243 apply (simp add: throwError_def) 3244 apply (rule ccorres_split_throws) 3245 apply (rule ccorres_return_void_C') 3246 apply vcg 3247 apply (wp lookupPTSlot_inv Arch_R.lookupPTSlot_aligned 3248 lookupPTSlot_page_table_at' | simp add: ptBits_eq)+ 3249 apply (vcg exspec=lookupPTSlot_modifies) 3250 \<comment> \<open>ARMSection\<close> 3251 apply (rule ccorres_Cond_rhs) 3252 apply (rule ccorres_rhs_assoc)+ 3253 apply (csymbr, csymbr) 3254 apply (simp add: gen_framesize_to_H_def dc_def[symmetric] 3255 liftE_liftM 3256 del: Collect_const) 3257 apply (simp split: if_split, rule conjI[rotated], rule impI, 3258 rule ccorres_empty, rule impI) 3259 apply (rule ccorres_rhs_assoc2, rule ccorres_rhs_assoc2, 3260 rule ccorres_rhs_assoc2, rule ccorres_rhs_assoc2, 3261 rule ccorres_rhs_assoc2) 3262 apply (rule ccorres_splitE_novcg, simp only: inl_rrel_inl_rrel, 3263 rule checkMappingPPtr_pde_ccorres) 3264 apply (rule conseqPre, vcg) 3265 apply (clarsimp simp: typ_heap_simps') 3266 subgoal by (simp add: pde_pde_section_lift_def cpde_relation_def pde_lift_def 3267 Let_def pde_tag_defs isSectionPDE_def 3268 split: pde.split_asm if_split_asm) 3269 apply (rule ceqv_refl) 3270 apply (simp add: unfold_checkMapping_return Collect_False dc_def[symmetric] 3271 del: Collect_const) 3272 apply (rule ccorres_handlers_weaken2, simp) 3273 apply csymbr 3274 apply (rule ccorres_split_nothrow_novcg_dc) 3275 apply (rule storePDE_Basic_ccorres) 3276 apply (simp add: cpde_relation_def Let_def 3277 pde_lift_pde_invalid) 3278 apply csymbr 3279 apply (ctac add: cleanByVA_PoU_ccorres[unfolded dc_def]) 3280 apply wp 3281 apply (clarsimp simp: guard_is_UNIV_def) 3282 apply simp 3283 apply wp 3284 apply (simp add: guard_is_UNIV_def) 3285 \<comment> \<open>ARMSuperSection\<close> 3286 apply (rule ccorres_Cond_rhs) 3287 apply (rule ccorres_rhs_assoc)+ 3288 apply csymbr 3289 apply csymbr 3290 apply csymbr 3291 apply (case_tac "pd = pde_Ptr (lookup_pd_slot pdPtr vptr)") 3292 prefer 2 3293 apply (simp, rule ccorres_empty) 3294 apply (simp add: gen_framesize_to_H_def dc_def[symmetric] 3295 liftE_liftM mapM_discarded whileAnno_def 3296 del: Collect_const) 3297 apply (rule ccorres_rhs_assoc2, rule ccorres_rhs_assoc2, 3298 rule ccorres_rhs_assoc2, rule ccorres_rhs_assoc2, 3299 rule ccorres_rhs_assoc2) 3300 apply (rule ccorres_splitE_novcg, simp only: inl_rrel_inl_rrel, 3301 rule checkMappingPPtr_pde_ccorres) 3302 apply (rule conseqPre, vcg) 3303 apply (clarsimp simp: typ_heap_simps') 3304 subgoal by (simp add: cpde_relation_def Let_def pde_lift_def 3305 isSuperSectionPDE_def pde_tag_defs 3306 pde_pde_section_lift_def 3307 split: if_split_asm pde.split_asm) 3308 apply (rule ceqv_refl) 3309 apply (simp add: unfold_checkMapping_return Collect_False ARMSuperSectionBits_def 3310 ARMSectionBits_def word_sle_def 3311 del: Collect_const) 3312 apply (ccorres_remove_UNIV_guard) 3313 apply (rule ccorres_rhs_assoc2, 3314 rule ccorres_split_nothrow_novcg) 3315 apply (rule_tac P="is_aligned pdPtr pdBits" in ccorres_gen_asm) 3316 apply (rule_tac F="\<lambda>_. page_directory_at' pdPtr" in ccorres_mapM_x_while) 3317 apply clarsimp 3318 apply (rule ccorres_guard_imp2) 3319 apply csymbr 3320 apply (rule ccorres_move_array_assertion_pde_16) 3321 apply (rule ccorres_flip_Guard, rule ccorres_move_array_assertion_pde_16) 3322 apply (rule storePDE_Basic_ccorres) 3323 apply (simp add: cpde_relation_def Let_def 3324 pde_lift_pde_invalid) 3325 apply clarsimp 3326 apply (simp add: superSectionPDEOffsets_nth length_superSectionPDEOffsets 3327 unat_of_nat of_nat_gt_0) 3328 apply (simp add: vmsz_aligned'_def vmsz_aligned_def) 3329 apply (clarsimp simp: lookup_pd_slot_def Let_def table_bits_defs 3330 mask_add_aligned field_simps) 3331 apply (erule less_kernelBase_valid_pde_offset' [simplified table_bits_defs]) 3332 apply (simp add: vmsz_aligned'_def) 3333 apply (simp add: word_le_nat_alt unat_of_nat) 3334 apply (simp add: length_superSectionPDEOffsets) 3335 apply (rule allI, rule conseqPre, vcg) 3336 apply clarsimp 3337 apply wp 3338 apply (simp add: length_superSectionPDEOffsets word_bits_def) 3339 apply ceqv 3340 apply (rule ccorres_handlers_weaken2) 3341 apply (rule ccorres_move_c_guard_pde) 3342 apply csymbr 3343 apply (rule ccorres_move_c_guard_pde ccorres_move_array_assertion_pde_16)+ 3344 apply (rule ccorres_add_return2) 3345 apply (ctac(no_vcg) add: cleanCacheRange_PoU_ccorres[unfolded dc_def]) 3346 apply (rule ccorres_move_array_assertion_pde_16, rule ccorres_return_Skip') 3347 apply wp 3348 apply (rule_tac P="is_aligned pdPtr pdBits" in hoare_gen_asm) 3349 apply (rule hoare_strengthen_post) 3350 apply (rule hoare_vcg_conj_lift) 3351 apply (rule_tac P="\<lambda>s. page_directory_at' pdPtr s 3352 \<and> 2 ^ pageBitsForSize sz \<le> gsMaxObjectSize s" 3353 in mapM_x_wp') 3354 apply wp[1] 3355 apply (rule mapM_x_accumulate_checks) 3356 apply (simp add: storePDE_def wordsFromPDE_def) 3357 apply (rule obj_at_setObject3) 3358 apply simp 3359 apply (simp add: objBits_simps archObjSize_def table_bits_defs) 3360 apply (simp add: typ_at_to_obj_at_arches[symmetric]) 3361 apply wp 3362 apply (clarsimp simp: vmsz_aligned_def vmsz_aligned'_def) 3363 apply (subgoal_tac "P" for P) 3364 apply (frule bspec, erule hd_in_set) 3365 apply (frule bspec, erule last_in_set) 3366 apply (simp add: upto_enum_step_def upto_enum_word superSectionPDEOffsets_def 3367 hd_map last_map typ_at_to_obj_at_arches field_simps 3368 objBits_simps archObjSize_def vmsz_aligned'_def 3369 pageBitsForSize_def table_bits_defs) 3370 apply (frule_tac x=14 and y=7 in is_aligned_weaken, clarsimp+) 3371 apply (drule is_aligned_lookup_pd_slot, simp) 3372 apply (clarsimp dest!: is_aligned_cache_preconds) 3373 apply (simp add: upto_enum_step_def upto_enum_word superSectionPDEOffsets_def Let_def 3374 table_bits_defs) 3375 apply (clarsimp simp: guard_is_UNIV_def Collect_const_mem objBits_simps archObjSize_def) 3376 apply (simp add: upto_enum_step_def upto_enum_word superSectionPDEOffsets_def Let_def 3377 hd_map last_map table_bits_defs) 3378 apply (simp, wp) 3379 apply (simp add: guard_is_UNIV_def) 3380 apply (rule ccorres_empty[where P=\<top>]) 3381 apply ceqv 3382 apply (simp add: liftE_liftM) 3383 apply (ctac add: flushPage_ccorres[unfolded dc_def]) 3384 apply ((wp lookupPTSlot_inv mapM_storePTE_invs[unfolded swp_def] 3385 mapM_storePDE_invs[unfolded swp_def] 3386 | wpc | simp)+)[1] 3387 apply (simp add: guard_is_UNIV_def) 3388 apply (simp add: throwError_def) 3389 apply (rule ccorres_split_throws) 3390 apply (rule ccorres_return_void_C[unfolded dc_def]) 3391 apply vcg 3392 apply (simp add: lookup_pd_slot_def Let_def table_bits_defs) 3393 apply (wp hoare_vcg_const_imp_lift_R findPDForASID_valid_offset'[simplified table_bits_defs] 3394 findPDForASID_aligned[simplified table_bits_defs]) 3395 apply (simp add: Collect_const_mem) 3396 apply (vcg exspec=findPDForASID_modifies) 3397 apply (clarsimp simp: invs_arch_state' invs_no_0_obj' invs_valid_objs' 3398 is_aligned_weaken[OF _ pbfs_atleast_pageBits] 3399 vmsz_aligned'_def) 3400 by (auto simp: invs_arch_state' invs_no_0_obj' invs_valid_objs' vmsz_aligned'_def 3401 is_aligned_weaken[OF _ pbfs_atleast_pageBits] 3402 pageBitsForSize_def gen_framesize_to_H_def 3403 Collect_const_mem vm_page_size_defs word_sle_def 3404 ccHoarePost_def typ_heap_simps table_bits_defs 3405 dest!: page_directory_at_rf_sr 3406 elim!: clift_array_assertion_imp 3407 split: vmpage_size.splits 3408 elim: is_aligned_weaken 3409 | unat_arith)+ 3410 3411 3412(* FIXME: move *) 3413lemma cap_to_H_PageCap_tag: 3414 "\<lbrakk> cap_to_H cap = ArchObjectCap (PageCap d p R sz A); 3415 cap_lift C_cap = Some cap \<rbrakk> \<Longrightarrow> 3416 cap_get_tag C_cap = scast cap_frame_cap \<or> cap_get_tag C_cap = scast cap_small_frame_cap" 3417 apply (clarsimp simp: cap_to_H_def Let_def split: cap_CL.splits if_split_asm) 3418 by (simp_all add: Let_def cap_lift_def split_def split: if_splits) 3419 3420lemma generic_frame_mapped_address: 3421 "\<lbrakk> cap_to_H a = capability.ArchObjectCap (arch_capability.PageCap d v0 v1 v2 v3); 3422 cap_lift (cte_C.cap_C cte') = Some a; 3423 cl_valid_cte \<lparr>cap_CL = a, cteMDBNode_CL = mdb_node_lift (cteMDBNode_C cte')\<rparr>; 3424 generic_frame_cap_set_capFMappedAddress_CL (Some a) (scast asidInvalid) 0 = Some cap'; 3425 cap_lift (cte_C.cap_C cte'a) = Some cap'\<rbrakk> 3426 \<Longrightarrow> ArchObjectCap (PageCap d v0 v1 v2 None) = cap_to_H cap' \<and> c_valid_cap (cte_C.cap_C cte'a)" 3427 apply (cases cte') 3428 apply (cases cte'a) 3429 apply (clarsimp simp: cl_valid_cte_def) 3430 apply (frule (1) cap_to_H_PageCap_tag) 3431 apply (erule disjE) 3432 apply (simp add: cap_frame_cap_lift) 3433 apply (simp add: generic_frame_cap_set_capFMappedAddress_CL_def) 3434 apply (clarsimp simp: cap_to_H_def) 3435 apply (simp add: asidInvalid_def split: if_split) 3436 apply (simp add: c_valid_cap_def cl_valid_cap_def) 3437 apply (simp add: cap_small_frame_cap_lift) 3438 apply (simp add: generic_frame_cap_set_capFMappedAddress_CL_def) 3439 apply (clarsimp simp: cap_to_H_def) 3440 apply (simp add: asidInvalid_def split: if_split) 3441 apply (simp add: c_valid_cap_def cl_valid_cap_def) 3442 done 3443 3444lemma updateCap_frame_mapped_addr_ccorres: 3445 notes option.case_cong_weak [cong] 3446 shows "ccorres dc xfdc 3447 (cte_wp_at' (\<lambda>c. ArchObjectCap cap = cteCap c) ctSlot and K (isPageCap cap)) 3448 UNIV [] 3449 (updateCap ctSlot (ArchObjectCap (capVPMappedAddress_update Map.empty cap))) 3450 (CALL generic_frame_cap_ptr_set_capFMappedAddress(cap_Ptr &(cte_Ptr ctSlot\<rightarrow>[''cap_C'']),(scast asidInvalid),0))" 3451 unfolding updateCap_def 3452 apply (rule ccorres_guard_imp2) 3453 apply (rule ccorres_pre_getCTE) 3454 apply (rule_tac P = "\<lambda>s. ctes_of s ctSlot = Some cte \<and> cteCap cte = ArchObjectCap cap \<and> isPageCap cap" and 3455 P' = "UNIV" 3456 in ccorres_from_vcg) 3457 apply (rule allI, rule conseqPre, vcg) 3458 apply clarsimp 3459 apply (erule (1) rf_sr_ctes_of_cliftE) 3460 apply (frule cap_CL_lift) 3461 apply (clarsimp simp: typ_heap_simps) 3462 apply (rule conjI) 3463 apply (clarsimp simp: isCap_simps) 3464 apply (drule cap_CL_lift) 3465 apply (drule (1) cap_to_H_PageCap_tag) 3466 apply simp 3467 apply (clarsimp simp: isCap_simps) 3468 apply (rule exI) 3469 apply (rule conjI, rule refl) 3470 apply clarsimp 3471 apply (rule fst_setCTE [OF ctes_of_cte_at], assumption) 3472 apply (erule bexI [rotated]) 3473 apply clarsimp 3474 apply (frule (1) rf_sr_ctes_of_clift) 3475 apply clarsimp 3476 apply (subgoal_tac "ccte_relation (cteCap_update (\<lambda>_. ArchObjectCap (PageCap d v0 v1 v2 None)) (cte_to_H ctel')) cte'a") 3477 prefer 2 3478 apply (clarsimp simp: ccte_relation_def) 3479 apply (clarsimp simp: cte_lift_def) 3480 apply (simp split: option.splits) 3481 apply clarsimp 3482 apply (simp add: cte_to_H_def c_valid_cte_def) 3483 apply (erule (4) generic_frame_mapped_address) 3484 apply (clarsimp simp add: rf_sr_def cstate_relation_def typ_heap_simps 3485 Let_def cpspace_relation_def) 3486 apply (rule conjI) 3487 apply (erule (3) cmap_relation_updI) 3488 subgoal by simp 3489 apply (erule_tac t = s' in ssubst) 3490 apply (simp add: heap_to_user_data_def) 3491 apply (rule conjI) 3492 apply (erule (1) setCTE_tcb_case) 3493 subgoal by (simp add: carch_state_relation_def cmachine_state_relation_def 3494 typ_heap_simps h_t_valid_clift_Some_iff 3495 cvariable_array_map_const_add_map_option[where f="tcb_no_ctes_proj"]) 3496 apply (clarsimp simp: cte_wp_at_ctes_of) 3497 done 3498 3499(* FIXME: move *) 3500lemma diminished_PageCap: 3501 "diminished' (ArchObjectCap (PageCap d p R sz a)) cap \<Longrightarrow> 3502 \<exists>R'. cap = ArchObjectCap (PageCap d p R' sz a)" 3503 apply (clarsimp simp: diminished'_def) 3504 apply (clarsimp simp: maskCapRights_def Let_def) 3505 apply (cases cap, simp_all add: isCap_simps) 3506 apply (simp add: ARM_HYP_H.maskCapRights_def) 3507 apply (simp add: isPageCap_def split: arch_capability.splits) 3508 done 3509 3510 3511(* FIXME: move *) 3512lemma ccap_relation_mapped_asid_0: 3513 "ccap_relation (ArchObjectCap (PageCap d v0 v1 v2 v3)) cap 3514 \<Longrightarrow> (generic_frame_cap_get_capFMappedASID_CL (cap_lift cap) \<noteq> 0 \<longrightarrow> v3 \<noteq> None) \<and> 3515 (generic_frame_cap_get_capFMappedASID_CL (cap_lift cap) = 0 \<longrightarrow> v3 = None)" 3516 apply (erule ccap_relationE) 3517 apply (drule sym, frule (1) cap_to_H_PageCap_tag) 3518 apply (rule conjI) 3519 apply (rule impI) 3520 apply (rule notI, erule notE) 3521 apply clarsimp 3522 apply (erule disjE) 3523 apply (clarsimp simp: cap_lift_frame_cap cap_to_H_def 3524 generic_frame_cap_get_capFMappedASID_CL_def 3525 split: if_split_asm) 3526 apply (clarsimp simp: cap_lift_small_frame_cap cap_to_H_def 3527 generic_frame_cap_get_capFMappedASID_CL_def 3528 split: if_split_asm) 3529 apply clarsimp 3530 apply (erule disjE) 3531 apply (rule ccontr) 3532 apply clarsimp 3533 apply (clarsimp simp: cap_lift_frame_cap cap_to_H_def 3534 generic_frame_cap_get_capFMappedASID_CL_def 3535 split: if_split_asm) 3536 apply (drule word_aligned_0_sum [where n=asid_low_bits]) 3537 apply fastforce 3538 apply (simp add: mask_def asid_low_bits_def word_and_le1) 3539 apply (simp add: asid_low_bits_def word_bits_def) 3540 apply clarsimp 3541 apply (drule word_shift_zero [where m=8]) 3542 apply (rule order_trans) 3543 apply (rule word_and_le1) 3544 apply (simp add: mask_def) 3545 apply (simp add: asid_low_bits_def word_bits_def) 3546 apply simp 3547 apply (rule ccontr) 3548 apply clarsimp 3549 apply (clarsimp simp: cap_lift_small_frame_cap cap_to_H_def 3550 generic_frame_cap_get_capFMappedASID_CL_def 3551 split: if_split_asm) 3552 apply (drule word_aligned_0_sum [where n=asid_low_bits]) 3553 apply fastforce 3554 apply (simp add: mask_def asid_low_bits_def word_and_le1) 3555 apply (simp add: asid_low_bits_def word_bits_def) 3556 apply clarsimp 3557 apply (drule word_shift_zero [where m=8]) 3558 apply (rule order_trans) 3559 apply (rule word_and_le1) 3560 apply (simp add: mask_def) 3561 apply (simp add: asid_low_bits_def word_bits_def) 3562 apply simp 3563 done 3564 3565(* FIXME: move *) 3566lemma getSlotCap_wp': 3567 "\<lbrace>\<lambda>s. \<forall>cap. cte_wp_at' (\<lambda>c. cteCap c = cap) p s \<longrightarrow> Q cap s\<rbrace> getSlotCap p \<lbrace>Q\<rbrace>" 3568 apply (simp add: getSlotCap_def) 3569 apply (wp getCTE_wp') 3570 apply (clarsimp simp: cte_wp_at_ctes_of) 3571 done 3572 3573lemma vmsz_aligned_aligned_pageBits: 3574 "vmsz_aligned' ptr sz \<Longrightarrow> is_aligned ptr pageBits" 3575 apply (simp add: vmsz_aligned'_def) 3576 apply (erule is_aligned_weaken) 3577 apply (simp add: pageBits_def pageBitsForSize_def 3578 split: vmpage_size.split) 3579 done 3580 3581lemma ccap_relation_PageCap_generics: 3582 "ccap_relation (ArchObjectCap (PageCap d ptr rghts sz mapdata)) cap' 3583 \<Longrightarrow> (mapdata \<noteq> None \<longrightarrow> 3584 generic_frame_cap_get_capFMappedAddress_CL (cap_lift cap') 3585 = snd (the mapdata) 3586 \<and> generic_frame_cap_get_capFMappedASID_CL (cap_lift cap') 3587 = fst (the mapdata)) 3588 \<and> ((generic_frame_cap_get_capFMappedASID_CL (cap_lift cap') = 0) 3589 = (mapdata = None)) 3590 \<and> vmrights_to_H (generic_frame_cap_get_capFVMRights_CL (cap_lift cap')) = rghts 3591 \<and> gen_framesize_to_H (generic_frame_cap_get_capFSize_CL (cap_lift cap')) = sz 3592 \<and> generic_frame_cap_get_capFBasePtr_CL (cap_lift cap') = ptr 3593 \<and> generic_frame_cap_get_capFVMRights_CL (cap_lift cap') < 4 3594 \<and> generic_frame_cap_get_capFSize_CL (cap_lift cap') < 4 3595 \<and> to_bool (generic_frame_cap_get_capFIsDevice_CL (cap_lift cap')) = d" 3596 apply (frule ccap_relation_mapped_asid_0) 3597 apply (case_tac "sz = ARMSmallPage") 3598 apply (frule(1) cap_get_tag_isCap_unfolded_H_cap) 3599 apply (clarsimp simp: cap_lift_small_frame_cap cap_to_H_def 3600 generic_frame_cap_get_capFMappedAddress_CL_def 3601 generic_frame_cap_get_capFVMRights_CL_def 3602 generic_frame_cap_get_capFSize_CL_def 3603 generic_frame_cap_get_capFMappedASID_CL_def 3604 generic_frame_cap_get_capFBasePtr_CL_def 3605 generic_frame_cap_get_capFIsDevice_CL_def 3606 elim!: ccap_relationE) 3607 apply (simp add: gen_framesize_to_H_def) 3608 apply (simp add: vm_page_size_defs order_le_less_trans [OF word_and_le1] mask_def 3609 split: if_split) 3610 apply (clarsimp split: if_split_asm) 3611 apply (frule(1) cap_get_tag_isCap_unfolded_H_cap) 3612 apply (clarsimp simp: cap_lift_frame_cap cap_to_H_def 3613 generic_frame_cap_get_capFMappedAddress_CL_def 3614 generic_frame_cap_get_capFVMRights_CL_def 3615 generic_frame_cap_get_capFSize_CL_def 3616 generic_frame_cap_get_capFMappedASID_CL_def 3617 generic_frame_cap_get_capFBasePtr_CL_def 3618 generic_frame_cap_get_capFIsDevice_CL_def 3619 c_valid_cap_def cl_valid_cap_def 3620 option_to_0_def 3621 elim!: ccap_relationE) 3622 apply (simp add: gen_framesize_to_H_is_framesize_to_H_if_not_ARMSmallPage) 3623 apply (simp add: vm_page_size_defs order_le_less_trans [OF word_and_le1] mask_def 3624 split: if_split) 3625 apply (clarsimp split: if_split_asm) 3626 done 3627 3628lemma performPageInvocationUnmap_ccorres: 3629 "ccorres (K (K \<bottom>) \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') 3630 (invs' and cte_wp_at' (diminished' (ArchObjectCap cap) o cteCap) ctSlot and K (isPageCap cap)) 3631 (UNIV \<inter> \<lbrace>ccap_relation (ArchObjectCap cap) \<acute>cap\<rbrace> \<inter> \<lbrace>\<acute>ctSlot = Ptr ctSlot\<rbrace>) 3632 [] 3633 (liftE (performPageInvocation (PageUnmap cap ctSlot))) 3634 (Call performPageInvocationUnmap_'proc)" 3635 apply (simp only: liftE_liftM ccorres_liftM_simp) 3636 apply (cinit lift: cap_' ctSlot_') 3637 apply csymbr 3638 apply (rule ccorres_guard_imp [where A= 3639 "invs' 3640 and cte_wp_at' (diminished' (ArchObjectCap cap) o cteCap) ctSlot 3641 and K (isPageCap cap)"]) 3642 apply wpc 3643 apply (rule_tac P=" ret__unsigned_long = 0" in ccorres_gen_asm) 3644 apply simp 3645 apply (rule ccorres_symb_exec_l) 3646 apply (subst bind_return [symmetric]) 3647 apply (rule ccorres_split_nothrow_novcg) 3648 apply (rule ccorres_Guard) 3649 apply (rule updateCap_frame_mapped_addr_ccorres) 3650 apply ceqv 3651 apply (rule_tac P=\<top> and P'=UNIV in ccorres_from_vcg_throws) 3652 apply (rule allI, rule conseqPre, vcg) 3653 apply (clarsimp simp: return_def) 3654 apply wp[1] 3655 apply (simp add: guard_is_UNIV_def) 3656 apply (wp getSlotCap_wp', simp) 3657 apply (wp getSlotCap_wp') 3658 apply simp 3659 apply (rule_tac P=" ret__unsigned_long \<noteq> 0" in ccorres_gen_asm) 3660 apply (simp cong: Guard_no_cong) 3661 apply (rule ccorres_rhs_assoc)+ 3662 apply (csymbr) 3663 apply csymbr 3664 apply csymbr 3665 apply csymbr 3666 apply wpc 3667 apply (ctac (no_vcg) add: unmapPage_ccorres) 3668 apply (rule ccorres_add_return2) 3669 apply (rule ccorres_split_nothrow_novcg) 3670 apply (rule ccorres_move_Guard [where P="cte_at' ctSlot" and P'=\<top>]) 3671 apply (clarsimp simp: cte_wp_at_ctes_of) 3672 apply (drule (1) rf_sr_ctes_of_clift) 3673 apply (fastforce intro: typ_heap_simps) 3674 apply (rule ccorres_symb_exec_l) 3675 apply (rule updateCap_frame_mapped_addr_ccorres) 3676 apply (wp getSlotCap_wp', simp) 3677 apply (wp getSlotCap_wp') 3678 apply simp 3679 apply ceqv 3680 apply (rule_tac P=\<top> and P'=UNIV in ccorres_from_vcg_throws) 3681 apply (rule allI, rule conseqPre, vcg) 3682 apply (clarsimp simp: return_def) 3683 apply wp[1] 3684 apply (simp add: guard_is_UNIV_def) 3685 apply (simp add: cte_wp_at_ctes_of) 3686 apply wp 3687 apply (clarsimp simp: cte_wp_at_ctes_of isCap_simps split: if_split) 3688 apply (drule diminished_PageCap) 3689 apply clarsimp 3690 apply (drule ccap_relation_mapped_asid_0) 3691 apply (frule ctes_of_valid', clarsimp) 3692 apply (drule valid_global_refsD_with_objSize, clarsimp) 3693 apply (fastforce simp: mask_def valid_cap'_def 3694 vmsz_aligned_aligned_pageBits) 3695 apply assumption 3696 apply (clarsimp simp: cte_wp_at_ctes_of isCap_simps split: if_split) 3697 apply (drule diminished_PageCap) 3698 apply clarsimp 3699 apply (frule (1) rf_sr_ctes_of_clift) 3700 apply (clarsimp simp: typ_heap_simps') 3701 apply (frule ccap_relation_PageCap_generics) 3702 apply (case_tac "v2 = ARMSmallPage") 3703 apply (auto simp add: cap_get_tag_isCap_ArchObject2 isCap_simps) 3704 done 3705 3706lemma HAPFromVMRights_spec: 3707 "\<forall>s. \<Gamma> \<turnstile> \<lbrace>s. \<acute>vm_rights < 4\<rbrace> Call HAPFromVMRights_'proc 3708 \<lbrace> \<acute>ret__unsigned_long = hap_from_vm_rights (vmrights_to_H \<^bsup>s\<^esup>vm_rights) \<rbrace>" 3709 apply vcg 3710 apply (simp add: vmrights_to_H_def hap_from_vm_rights_def 3711 Kernel_C.VMNoAccess_def Kernel_C.VMKernelOnly_def 3712 Kernel_C.VMReadOnly_def Kernel_C.VMReadWrite_def) 3713 apply clarsimp 3714 apply (drule word_less_cases, auto)+ 3715 done 3716 3717 3718lemma hap_from_vm_rights_mask: 3719 "hap_from_vm_rights R && 3 = (hap_from_vm_rights R :: word32)" 3720 by (simp add: hap_from_vm_rights_def split: vmrights.splits) 3721 3722 3723definition 3724 "shared_bit_from_cacheable cacheable \<equiv> if cacheable = 0x1 then 0 else 1" 3725 3726definition 3727 "tex_bits_from_cacheable cacheable \<equiv> if cacheable = 0x1 then 5 else 0" 3728 3729definition 3730 "iwb_from_cacheable cacheable \<equiv> if cacheable = 0x1 then 1 else 0" 3731 3732lemma makeUserPDE_spec: 3733 "\<forall>s. \<Gamma> \<turnstile> 3734 \<lbrace>s. (\<acute>page_size = scast Kernel_C.ARMSection \<or> \<acute>page_size = scast Kernel_C.ARMSuperSection) \<and> 3735 \<acute>vm_rights < 4 \<and> vmsz_aligned' (\<acute>paddr) (gen_framesize_to_H \<acute>page_size) \<and> 3736 \<acute>cacheable && 1 = \<acute>cacheable \<and> 3737 \<acute>nonexecutable && 1 = \<acute>nonexecutable\<rbrace> 3738 Call makeUserPDE_'proc 3739 \<lbrace> pde_lift \<acute>ret__struct_pde_C = Some (Pde_pde_section \<lparr> 3740 pde_pde_section_CL.XN_CL = \<^bsup>s\<^esup>nonexecutable, 3741 contiguous_hint_CL = if \<^bsup>s\<^esup>page_size = scast Kernel_C.ARMSection then 0 else 1, 3742 pde_pde_section_CL.address_CL = \<^bsup>s\<^esup>paddr, 3743 AF_CL = 1, 3744 SH_CL = 0, 3745 HAP_CL = hap_from_vm_rights (vmrights_to_H \<^bsup>s\<^esup>vm_rights), 3746 MemAttr_CL = memattr_from_cacheable (to_bool \<^bsup>s\<^esup>cacheable) 3747 \<rparr>) \<rbrace>" 3748 apply (rule allI, rule conseqPre, vcg) 3749 apply (clarsimp simp: hap_from_vm_rights_mask split: if_splits) 3750 apply (intro conjI impI allI | clarsimp )+ 3751 apply (simp only: pde_pde_section_lift pde_pde_section_lift_def) 3752 apply (simp add: vmsz_aligned'_def gen_framesize_to_H_def hap_from_vm_rights_mask) 3753 apply (clarsimp simp: Kernel_C.ARMSection_def Kernel_C.ARMSmallPage_def 3754 Kernel_C.ARMLargePage_def) 3755 apply (fastforce simp:mask_def hap_from_vm_rights_mask memattr_from_cacheable_def 3756 split:if_splits dest!:mask_eq1_nochoice intro: is_aligned_neg_mask_weaken) 3757 apply (simp only: pde_pde_section_lift pde_pde_section_lift_def) 3758 apply (simp add: vmsz_aligned'_def gen_framesize_to_H_def hap_from_vm_rights_mask) 3759 apply (clarsimp simp: Kernel_C.ARMSection_def Kernel_C.ARMSmallPage_def 3760 Kernel_C.ARMLargePage_def is_aligned_neg_mask_eq) 3761 apply (fastforce simp:mask_def hap_from_vm_rights_mask memattr_from_cacheable_def 3762 split:if_splits dest!:mask_eq1_nochoice intro: is_aligned_neg_mask_weaken) 3763 apply (clarsimp) 3764 apply (intro conjI impI allI) 3765 apply (simp add:pde_pde_section_lift pde_pde_section_lift_def) 3766 apply (simp add: vmsz_aligned'_def gen_framesize_to_H_def hap_from_vm_rights_mask) 3767 apply (drule is_aligned_weaken[where y = 21]) 3768 apply (clarsimp simp: Kernel_C.ARMSuperSection_def Kernel_C.ARMSmallPage_def 3769 Kernel_C.ARMLargePage_def is_aligned_neg_mask_eq)+ 3770 apply (fastforce simp:mask_def hap_from_vm_rights_mask memattr_from_cacheable_def 3771 split:if_splits dest!:mask_eq1_nochoice intro: is_aligned_neg_mask_weaken) 3772 apply (simp add:pde_pde_section_lift pde_pde_section_lift_def) 3773 apply (simp add: vmsz_aligned'_def gen_framesize_to_H_def hap_from_vm_rights_mask) 3774 apply (drule is_aligned_weaken[where y = 21]) 3775 apply (clarsimp simp: Kernel_C.ARMSuperSection_def Kernel_C.ARMSmallPage_def 3776 Kernel_C.ARMLargePage_def is_aligned_neg_mask_eq)+ 3777 apply (fastforce simp:mask_def hap_from_vm_rights_mask memattr_from_cacheable_def 3778 split:if_splits dest!:mask_eq1_nochoice intro: is_aligned_neg_mask_weaken) 3779 done 3780 3781lemma makeUserPTE_spec: 3782 "\<forall>s. \<Gamma> \<turnstile> 3783 \<lbrace>s. (\<acute>page_size = scast Kernel_C.ARMSmallPage \<or> \<acute>page_size = scast Kernel_C.ARMLargePage) \<and> 3784 \<acute>vm_rights < 4 \<and> vmsz_aligned' \<acute>paddr (gen_framesize_to_H \<acute>page_size) \<and> 3785 \<acute>cacheable && 1 = \<acute>cacheable \<and> \<acute>nonexecutable && 1 = \<acute>nonexecutable\<rbrace> 3786 Call makeUserPTE_'proc 3787 \<lbrace> pte_lift \<acute>ret__struct_pte_C = Some (Pte_pte_small \<lparr> 3788 pte_pte_small_CL.XN_CL = \<^bsup>s\<^esup>nonexecutable, 3789 contiguous_hint_CL = if \<^bsup>s\<^esup>page_size = scast Kernel_C.ARMSmallPage then 0 else 1, 3790 pte_pte_small_CL.address_CL = \<^bsup>s\<^esup>paddr, 3791 AF_CL = 1, 3792 SH_CL = 0, 3793 HAP_CL = hap_from_vm_rights (vmrights_to_H \<^bsup>s\<^esup>vm_rights), 3794 MemAttr_CL = memattr_from_cacheable (to_bool \<^bsup>s\<^esup>cacheable) 3795 \<rparr>)\<rbrace>" 3796 apply vcg 3797 apply (clarsimp simp:vmsz_aligned'_def) 3798 apply (intro conjI) 3799 apply (rule impI) 3800 apply (drule is_aligned_weaken[where y = 12]) 3801 apply (clarsimp simp:gen_framesize_to_H_def pageBitsForSize_def split:if_splits) 3802 apply (clarsimp dest:is_aligned_neg_mask_eq) 3803 apply (intro conjI impI allI) 3804 apply (fold_subgoals (prefix))[2] 3805 subgoal premises prems using prems 3806 by ((clarsimp simp add: pte_lift_def pte_pte_small_lift_def pte_tag_defs 3807 mask_def hap_from_vm_rights_mask addrFromPPtr_def 3808 memattr_from_cacheable_def 3809 iwb_from_cacheable_def dest!:mask_eq1_nochoice)+) 3810 apply clarsimp 3811 apply (drule is_aligned_weaken[where y = 16]) 3812 apply (clarsimp simp: gen_framesize_to_H_def pageBitsForSize_def split: if_splits) 3813 apply (intro conjI impI allI 3814 ; clarsimp simp: pte_lift_def pte_pte_small_lift_def pte_tag_defs) 3815 apply (fastforce simp:mask_def hap_from_vm_rights_mask memattr_from_cacheable_def 3816 split:if_splits dest!:mask_eq1_nochoice intro: is_aligned_neg_mask_weaken)+ 3817 done 3818 3819lemma vmAttributesFromWord_spec: 3820 "\<forall>s. \<Gamma> \<turnstile> \<lbrace>s. True\<rbrace> Call vmAttributesFromWord_'proc 3821 \<lbrace> vm_attributes_lift \<acute>ret__struct_vm_attributes_C = 3822 \<lparr> armExecuteNever_CL = (\<^bsup>s\<^esup>w >> 2) && 1, 3823 armParityEnabled_CL = (\<^bsup>s\<^esup>w >> 1) && 1, 3824 armPageCacheable_CL = \<^bsup>s\<^esup>w && 1 \<rparr> \<rbrace>" 3825 by (vcg, simp add: vm_attributes_lift_def word_sless_def word_sle_def mask_def) 3826 3827lemma cap_to_H_PDCap_tag: 3828 "\<lbrakk> cap_to_H cap = ArchObjectCap (PageDirectoryCap p A); 3829 cap_lift C_cap = Some cap \<rbrakk> \<Longrightarrow> 3830 cap_get_tag C_cap = scast cap_page_directory_cap" 3831 apply (clarsimp simp: cap_to_H_def Let_def split: cap_CL.splits if_split_asm) 3832 apply (simp_all add: Let_def cap_lift_def split: if_splits) 3833 done 3834 3835lemma cap_to_H_PDCap: 3836 "cap_to_H cap = ArchObjectCap (PageDirectoryCap p asid) \<Longrightarrow> 3837 \<exists>cap_CL. cap = Cap_page_directory_cap cap_CL \<and> 3838 to_bool (capPDIsMapped_CL cap_CL) = (asid \<noteq> None) \<and> 3839 (asid \<noteq> None \<longrightarrow> capPDMappedASID_CL cap_CL = the asid) \<and> 3840 capPDBasePtr_CL cap_CL = p" 3841 by (auto simp add: cap_to_H_def Let_def split: cap_CL.splits if_splits) 3842 3843lemma cap_lift_PDCap_Base: 3844 "\<lbrakk> cap_to_H cap_cl = ArchObjectCap (PageDirectoryCap p asid); 3845 cap_lift cap_c = Some cap_cl \<rbrakk> 3846 \<Longrightarrow> p = capPDBasePtr_CL (cap_page_directory_cap_lift cap_c)" 3847 apply (simp add: cap_page_directory_cap_lift_def) 3848 apply (clarsimp simp: cap_to_H_def Let_def split: cap_CL.splits if_splits) 3849 done 3850 3851 3852declare mask_Suc_0[simp] 3853 3854(* FIXME: move *) 3855lemma setCTE_asidpool': 3856 "\<lbrace> ko_at' (ASIDPool pool) p \<rbrace> setCTE c p' \<lbrace>\<lambda>_. ko_at' (ASIDPool pool) p\<rbrace>" 3857 apply (clarsimp simp: setCTE_def) 3858 apply (simp add: setObject_def split_def) 3859 apply (rule hoare_seq_ext [OF _ hoare_gets_post]) 3860 apply (clarsimp simp: valid_def in_monad) 3861 apply (frule updateObject_type) 3862 apply (clarsimp simp: obj_at'_def projectKOs) 3863 apply (rule conjI) 3864 apply (clarsimp simp: lookupAround2_char1) 3865 apply (clarsimp split: if_split) 3866 apply (case_tac obj', auto)[1] 3867 apply (rename_tac arch_kernel_object) 3868 apply (case_tac arch_kernel_object, auto)[1] 3869 apply (simp add: updateObject_cte) 3870 apply (clarsimp simp: updateObject_cte typeError_def magnitudeCheck_def in_monad 3871 split: kernel_object.splits if_splits option.splits) 3872 apply (clarsimp simp: ps_clear_upd' lookupAround2_char1) 3873 done 3874 3875(* FIXME: move *) 3876lemma udpateCap_asidpool': 3877 "\<lbrace> ko_at' (ASIDPool pool) p \<rbrace> updateCap c p' \<lbrace>\<lambda>_. ko_at' (ASIDPool pool) p\<rbrace>" 3878 apply (simp add: updateCap_def) 3879 apply (wp setCTE_asidpool') 3880 done 3881 3882(* FIXME: move *) 3883lemma asid_pool_at_rf_sr: 3884 "\<lbrakk>ko_at' (ASIDPool pool) p s; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> 3885 \<exists>pool'. cslift s' (ap_Ptr p) = Some pool' \<and> 3886 casid_pool_relation (ASIDPool pool) pool'" 3887 apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def cpspace_relation_def) 3888 apply (erule (1) cmap_relation_ko_atE) 3889 apply clarsimp 3890 done 3891 3892(* FIXME: move *) 3893lemma asid_pool_at_ko: 3894 "asid_pool_at' p s \<Longrightarrow> \<exists>pool. ko_at' (ASIDPool pool) p s" 3895 apply (clarsimp simp: typ_at'_def obj_at'_def ko_wp_at'_def projectKOs) 3896 apply (case_tac ko, auto) 3897 apply (rename_tac arch_kernel_object) 3898 apply (case_tac arch_kernel_object, auto)[1] 3899 apply (rename_tac asidpool) 3900 apply (case_tac asidpool, auto)[1] 3901 done 3902 3903(* FIXME: move *) 3904lemma asid_pool_at_c_guard: 3905 "\<lbrakk>asid_pool_at' p s; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> c_guard (ap_Ptr p)" 3906 by (fastforce intro: typ_heap_simps dest!: asid_pool_at_ko asid_pool_at_rf_sr) 3907 3908(* FIXME: move *) 3909lemma setObjectASID_Basic_ccorres: 3910 "ccorres dc xfdc \<top> {s. f s = p \<and> casid_pool_relation pool (asid_pool_C (pool' s))} hs 3911 (setObject p pool) 3912 ((Basic (\<lambda>s. globals_update( t_hrs_'_update 3913 (hrs_mem_update (heap_update (Ptr &(ap_Ptr (f s)\<rightarrow>[''array_C''])) (pool' s)))) s)))" 3914 apply (rule setObject_ccorres_helper) 3915 apply (simp_all add: objBits_simps archObjSize_def pageBits_def) 3916 apply (rule conseqPre, vcg) 3917 apply (rule subsetI, clarsimp simp: Collect_const_mem) 3918 apply (rule cmap_relationE1, erule rf_sr_cpspace_asidpool_relation, 3919 erule ko_at_projectKO_opt) 3920 apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def) 3921 apply (rule conjI) 3922 apply (clarsimp simp: cpspace_relation_def typ_heap_simps 3923 update_asidpool_map_to_asidpools 3924 update_asidpool_map_tos) 3925 apply (case_tac y') 3926 apply clarsimp 3927 apply (erule cmap_relation_updI, 3928 erule ko_at_projectKO_opt, simp+) 3929 apply (simp add: cready_queues_relation_def 3930 carch_state_relation_def 3931 cmachine_state_relation_def 3932 Let_def typ_heap_simps 3933 update_asidpool_map_tos) 3934 done 3935 3936lemma performASIDPoolInvocation_ccorres: 3937 notes option.case_cong_weak [cong] 3938 shows 3939 "ccorres (K (K \<bottom>) \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') 3940 (invs' and cte_wp_at' (isPDCap o cteCap) ctSlot and asid_pool_at' poolPtr 3941 and K (asid \<le> mask asid_bits)) 3942 (UNIV \<inter> \<lbrace>\<acute>poolPtr = Ptr poolPtr\<rbrace> \<inter> \<lbrace>\<acute>asid = asid\<rbrace> \<inter> \<lbrace>\<acute>pdCapSlot = Ptr ctSlot\<rbrace>) 3943 [] 3944 (liftE (performASIDPoolInvocation (Assign asid poolPtr ctSlot))) 3945 (Call performASIDPoolInvocation_'proc)" 3946 apply (simp only: liftE_liftM ccorres_liftM_simp) 3947 apply (cinit lift: poolPtr_' asid_' pdCapSlot_') 3948 apply (rule ccorres_symb_exec_l) 3949 apply (rule ccorres_symb_exec_l) 3950 apply (rule_tac P="ko_at' (ASIDPool pool) poolPtr" in ccorres_cross_over_guard) 3951 apply (rule ccorres_rhs_assoc2) 3952 apply (rule_tac ccorres_split_nothrow [where r'=dc and xf'=xfdc]) 3953 apply (simp add: updateCap_def) 3954 apply (rule_tac A="cte_wp_at' ((=) rv o cteCap) ctSlot 3955 and K (isPDCap rv \<and> asid \<le> mask asid_bits)" 3956 and A'=UNIV in ccorres_guard_imp2) 3957 apply (rule ccorres_pre_getCTE) 3958 apply (rule_tac P="cte_wp_at' ((=) rv o cteCap) ctSlot 3959 and K (isPDCap rv \<and> asid \<le> mask asid_bits) 3960 and cte_wp_at' ((=) rva) ctSlot" 3961 and P'=UNIV in ccorres_from_vcg) 3962 apply (rule allI, rule conseqPre, vcg) 3963 apply (clarsimp simp: cte_wp_at_ctes_of) 3964 apply (erule (1) rf_sr_ctes_of_cliftE) 3965 apply (clarsimp simp: typ_heap_simps) 3966 apply (rule conjI) 3967 apply (clarsimp simp: isPDCap_def) 3968 apply (drule cap_CL_lift) 3969 apply (drule (1) cap_to_H_PDCap_tag) 3970 apply simp 3971 apply (clarsimp simp: typ_heap_simps' isPDCap_def) 3972 apply (rule fst_setCTE [OF ctes_of_cte_at], assumption) 3973 apply (erule bexI [rotated]) 3974 apply clarsimp 3975 apply (frule (1) rf_sr_ctes_of_clift) 3976 apply clarsimp 3977 apply (clarsimp simp: rf_sr_def cstate_relation_def typ_heap_simps 3978 Let_def cpspace_relation_def) 3979 apply (rule conjI) 3980 apply (erule (2) cmap_relation_updI) 3981 apply (clarsimp simp: ccte_relation_def) 3982 apply (clarsimp simp: cte_lift_def) 3983 apply (simp split: option.splits) 3984 apply clarsimp 3985 apply (case_tac cte') 3986 apply clarsimp 3987 apply (rule conjI) 3988 apply (clarsimp simp: cap_lift_def Let_def cap_tag_defs) 3989 apply clarsimp 3990 apply (simp add: cte_to_H_def c_valid_cte_def) 3991 apply (simp add: cap_page_directory_cap_lift) 3992 apply (simp (no_asm) add: cap_to_H_def) 3993 apply (simp add: to_bool_def asid_bits_def le_mask_imp_and_mask word_bits_def) 3994 apply (erule (1) cap_lift_PDCap_Base) 3995 apply simp 3996 apply (erule_tac t = s' in ssubst) 3997 apply (simp add: heap_to_user_data_def) 3998 apply (rule conjI) 3999 apply (erule (1) setCTE_tcb_case) 4000 apply (simp add: carch_state_relation_def cmachine_state_relation_def 4001 typ_heap_simps h_t_valid_clift_Some_iff 4002 cvariable_array_map_const_add_map_option[where f="tcb_no_ctes_proj"]) 4003 apply (clarsimp simp: cte_wp_at_ctes_of) 4004 apply ceqv 4005 apply (rule ccorres_move_c_guard_cte) 4006 apply (rule ccorres_symb_exec_r) 4007 apply (rule ccorres_Guard_Seq[where F=ArrayBounds])? 4008 apply (rule ccorres_move_c_guard_ap) 4009 apply (simp only: Kernel_C.asidLowBits_def word_sle_def) 4010 apply (rule ccorres_Guard_Seq)+ 4011 apply (rule ccorres_add_return2) 4012 apply (rule ccorres_split_nothrow_novcg) 4013 apply (rule setObjectASID_Basic_ccorres) 4014 apply ceqv 4015 apply (rule ccorres_from_vcg_throws [where P=\<top> and P'=UNIV]) 4016 apply (rule allI, rule conseqPre, vcg) 4017 apply (clarsimp simp: return_def) 4018 apply wp 4019 apply (simp add: guard_is_UNIV_def) 4020 apply (vcg) 4021 apply (rule conseqPre, vcg) 4022 apply clarsimp 4023 apply (wp udpateCap_asidpool') 4024 apply vcg 4025 apply (wp getASID_wp) 4026 apply simp 4027 apply wp 4028 apply (simp add: o_def inv_def) 4029 apply (wp getASID_wp) 4030 apply simp 4031 apply (rule empty_fail_getObject) 4032 apply simp 4033 apply wp 4034 apply (wp getSlotCap_wp') 4035 apply simp 4036 apply (clarsimp simp: cte_wp_at_ctes_of) 4037 apply (rule conjI) 4038 apply (clarsimp dest!: asid_pool_at_ko simp: obj_at'_def) 4039 apply (rule cmap_relationE1[OF cmap_relation_cte], assumption+) 4040 apply (clarsimp simp: typ_heap_simps cap_get_tag_isCap_ArchObject2 4041 isPDCap_def isCap_simps 4042 order_le_less_trans[OF word_and_le1] asid_low_bits_def 4043 dest!: ccte_relation_ccap_relation) 4044 apply (simp add: casid_pool_relation_def mask_def) 4045 apply (rule array_relation_update) 4046 apply (drule (1) asid_pool_at_rf_sr) 4047 apply (clarsimp simp: typ_heap_simps) 4048 apply (case_tac pool') 4049 apply (simp add: casid_pool_relation_def) 4050 apply simp 4051 apply (simp add: option_to_ptr_def option_to_0_def) 4052 apply (erule(1) rf_sr_ctes_of_cliftE, simp(no_asm_simp)) 4053 apply (clarsimp simp: ccap_relation_def map_option_Some_eq2 cap_lift_PDCap_Base) 4054 apply (simp add: asid_low_bits_def) 4055 done 4056 4057lemma pte_case_isInvalidPTE: 4058 "(case pte of InvalidPTE \<Rightarrow> P | _ \<Rightarrow> Q) 4059 = (if isInvalidPTE pte then P else Q)" 4060 by (cases pte, simp_all add: isInvalidPTE_def) 4061 4062 4063lemma flushTable_ccorres: 4064 "ccorres dc xfdc (invs' and cur_tcb' and (\<lambda>_. asid \<le> mask asid_bits)) 4065 (UNIV \<inter> {s. pd_' s = pde_Ptr pd} \<inter> {s. asid_' s = asid} 4066 \<inter> {s. vptr_' s = vptr} \<inter> {s. pt_' s = pte_Ptr pt}) [] 4067 (flushTable pd asid vptr) (Call flushTable_'proc)" 4068 apply (cinit lift: pd_' asid_' vptr_' pt_') 4069 4070 apply (rule ccorres_assert) 4071 apply (simp add: objBits_simps archObjSize_def 4072 ARMSmallPageBits_def word_sle_def 4073 del: Collect_const) 4074 apply (ctac (no_vcg) add: setVMRootForFlush_ccorres) 4075 apply (ctac (no_vcg) add: loadHWASID_ccorres) 4076 apply csymbr 4077 apply (simp add: when_def del: Collect_const) 4078 apply (rule ccorres_cond2[where R=\<top>]) 4079 apply (clarsimp simp: pde_stored_asid_def to_bool_def split: if_split) 4080 apply (rule ccorres_Guard_Seq ccorres_rhs_assoc)+ 4081 4082 apply csymbr 4083 apply (simp add: word_sle_def mapM_discarded whileAnno_def Collect_False 4084 del: Collect_const) 4085 apply (ctac (no_vcg) add: invalidateTranslationASID_ccorres) 4086 apply (rule_tac R=\<top> in ccorres_cond2) 4087 apply (clarsimp simp: from_bool_0 Collect_const_mem) 4088 apply (rule ccorres_pre_getCurThread) 4089 apply (ctac (no_vcg) add: setVMRoot_ccorres [unfolded dc_def]) 4090 apply (rule ccorres_return_Skip[unfolded dc_def]) 4091 apply (wp static_imp_wp) 4092 apply clarsimp 4093 apply (rule_tac Q="\<lambda>_ s. invs' s \<and> cur_tcb' s" in hoare_post_imp) 4094 apply (simp add: invs'_invs_no_cicd cur_tcb'_def) 4095 apply (wp mapM_x_wp_inv getPTE_wp | wpc)+ 4096 apply (rule ccorres_return_Skip[unfolded dc_def]) 4097 apply wp 4098 apply clarsimp 4099 apply (strengthen invs_valid_pde_mappings') 4100 apply (wp setVMRootForFlush_invs' hoare_drop_imps) 4101 apply (clarsimp simp:Collect_const_mem) 4102 apply (simp add: pde_pde_invalid_lift_def 4103 pde_lift_def pde_stored_asid_def to_bool_def) 4104 done 4105 4106lemma performPageTableInvocationMap_ccorres: 4107 "ccorres (K (K \<bottom>) \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') 4108 (cte_at' ctSlot and (\<lambda>_. valid_pde_mapping_offset' (pdSlot && mask pdBits))) 4109 (UNIV \<inter> \<lbrace>ccap_relation cap \<acute>cap\<rbrace> \<inter> \<lbrace>\<acute>ctSlot = Ptr ctSlot\<rbrace> \<inter> \<lbrace>cpde_relation pde \<acute>pde\<rbrace> \<inter> \<lbrace>\<acute>pdSlot = Ptr pdSlot\<rbrace>) 4110 [] 4111 (liftE (performPageTableInvocation (PageTableMap cap ctSlot pde pdSlot))) 4112 (Call performPageTableInvocationMap_'proc)" 4113 apply (simp only: liftE_liftM ccorres_liftM_simp) 4114 apply (cinit lift: cap_' ctSlot_' pde_' pdSlot_') 4115 apply (ctac (no_vcg)) 4116 apply (rule ccorres_split_nothrow_novcg) 4117 apply simp 4118 apply (erule storePDE_Basic_ccorres) 4119 apply ceqv 4120 apply (rule ccorres_symb_exec_r) 4121 apply (rule ccorres_add_return2) 4122 apply (rule ccorres_split_nothrow_novcg) 4123 apply simp 4124 apply (rule ccorres_call) 4125 apply (rule cleanByVA_PoU_ccorres) 4126 apply (rule refl) 4127 apply (simp add: xfdc_def) 4128 apply simp 4129 apply ceqv 4130 apply (rule_tac P=\<top> and P'=UNIV in ccorres_from_vcg_throws) 4131 apply (rule allI, rule conseqPre, vcg) 4132 apply (clarsimp simp: return_def) 4133 apply wp 4134 apply (simp add: guard_is_UNIV_def) 4135 apply vcg 4136 apply (rule conseqPre, vcg) 4137 apply clarsimp 4138 apply wp 4139 apply (simp add: guard_is_UNIV_def) 4140 apply wp 4141 apply simp 4142 apply simp 4143 done 4144 4145end 4146 4147end 4148