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 15autocorres 16 [ skip_heap_abs, skip_word_abs, 17 scope = handleVMFault lookupPDPTSlot, 18 scope_depth = 0, 19 c_locale = kernel_all_substitute 20 ] "../c/build/$L4V_ARCH/kernel_all.c_pp" 21 22context begin interpretation Arch . (*FIXME: arch_split*) 23 24lemma ccorres_name_pre_C: 25 "(\<And>s. s \<in> P' \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf P {s} hs f g) 26 \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf P P' hs f g" 27 apply (rule ccorres_guard_imp) 28 apply (rule_tac xf'=id in ccorres_abstract, rule ceqv_refl) 29 apply (rule_tac P="rv' \<in> P'" in ccorres_gen_asm2) 30 apply assumption 31 apply simp 32 apply simp 33 done 34 35lemma ccorres_flip_Guard: 36 assumes cc: "ccorres_underlying sr \<Gamma> r xf arrel axf A C hs a (Guard F S (Guard F1 S1 c))" 37 shows "ccorres_underlying sr \<Gamma> r xf arrel axf A C hs a (Guard F1 S1 (Guard F S c))" 38 apply (rule ccorres_name_pre_C) 39 using cc 40 apply (case_tac "s \<in> (S1 \<inter> S)") 41 apply (clarsimp simp: ccorres_underlying_def) 42 apply (erule exec_handlers.cases; 43 fastforce elim!: exec_Normal_elim_cases intro: exec_handlers.intros exec.Guard) 44 apply (clarsimp simp: ccorres_underlying_def) 45 apply (case_tac "s \<in> S") 46 apply (fastforce intro: exec.Guard exec.GuardFault exec_handlers.intros) 47 apply (fastforce intro: exec.Guard exec.GuardFault exec_handlers.intros) 48 done 49 50(* FIXME: move *) 51lemma empty_fail_findVSpaceForASID[iff]: 52 "empty_fail (findVSpaceForASID asid)" 53 apply (simp add: findVSpaceForASID_def liftME_def) 54 apply (intro empty_fail_bindE, simp_all split: option.split) 55 apply (simp add: assertE_def split: if_split) 56 apply (simp add: assertE_def split: if_split) 57 apply (simp add: empty_fail_getObject) 58 apply (simp add: assertE_def liftE_bindE checkPML4At_def split: if_split) 59 done 60 61(* FIXME: move *) 62lemma empty_fail_findVSpaceForASIDAssert[iff]: 63 "empty_fail (findVSpaceForASIDAssert asid)" 64 apply (simp add: findVSpaceForASIDAssert_def catch_def 65 checkPML4At_def) 66 apply (intro empty_fail_bind, simp_all split: sum.split) 67 done 68 69end 70 71context kernel_m begin 72 73local_setup 74 \<open>AutoCorresModifiesProofs.new_modifies_rules "../c/build/$L4V_ARCH/kernel_all.c_pp"\<close> 75 76lemma pageBitsForSize_le: 77 "pageBitsForSize x \<le> 30" 78 by (simp add: pageBitsForSize_def bit_simps split: vmpage_size.splits) 79 80lemma unat_of_nat_pageBitsForSize [simp]: 81 "unat (of_nat (pageBitsForSize x)::machine_word) = pageBitsForSize x" 82 apply (subst unat_of_nat64) 83 apply (rule order_le_less_trans, rule pageBitsForSize_le) 84 apply (simp add: word_bits_def) 85 apply simp 86 done 87 88lemma checkVPAlignment_ccorres: 89 "ccorres (\<lambda>a c. if to_bool c then a = Inr () else a = Inl AlignmentError) ret__unsigned_long_' 90 \<top> 91 (UNIV \<inter> \<lbrace>sz = framesize_to_H \<acute>sz \<and> \<acute>sz < 3\<rbrace> \<inter> \<lbrace>\<acute>w = w\<rbrace>) 92 [] 93 (checkVPAlignment sz w) 94 (Call checkVPAlignment_'proc)" 95 apply (cinit lift: sz_' w_') 96 apply (csymbr) 97 apply clarsimp 98 apply (rule ccorres_Guard [where A=\<top> and C'=UNIV]) 99 apply (simp split: if_split) 100 apply (rule conjI) 101 apply (clarsimp simp: mask_def unlessE_def returnOk_def) 102 apply (rule ccorres_guard_imp) 103 apply (rule ccorres_return_C) 104 apply simp 105 apply simp 106 apply simp 107 apply simp 108 apply (simp split: if_split add: to_bool_def) 109 apply (clarsimp simp: mask_def unlessE_def throwError_def split: if_split) 110 apply (rule ccorres_guard_imp) 111 apply (rule ccorres_return_C) 112 apply simp 113 apply simp 114 apply simp 115 apply simp 116 apply (simp split: if_split add: to_bool_def) 117 apply (clarsimp split: if_split) 118 apply (simp add: word_less_nat_alt) 119 apply (rule order_le_less_trans, rule pageBitsForSize_le) 120 apply simp 121 done 122 123lemma rf_asidTable: 124 "\<lbrakk> (\<sigma>, x) \<in> rf_sr; valid_arch_state' \<sigma>; idx \<le> mask asid_high_bits \<rbrakk> 125 \<Longrightarrow> case x64KSASIDTable (ksArchState \<sigma>) 126 idx of 127 None \<Rightarrow> 128 index (x86KSASIDTable_' (globals x)) (unat idx) = 129 NULL 130 | Some v \<Rightarrow> 131 index (x86KSASIDTable_' (globals x)) (unat idx) = Ptr v \<and> 132 index (x86KSASIDTable_' (globals x)) (unat idx) \<noteq> NULL" 133 apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def 134 carch_state_relation_def 135 array_relation_def) 136 apply (drule_tac x=idx in spec)+ 137 apply (clarsimp simp: mask_def split: option.split) 138 apply (drule sym, simp) 139 apply (simp add: option_to_ptr_def option_to_0_def) 140 apply (clarsimp simp: invs'_def valid_state'_def valid_arch_state'_def 141 valid_asid_table'_def ran_def) 142 done 143 144lemma getKSASIDTable_ccorres_stuff: 145 "\<lbrakk> invs' \<sigma>; (\<sigma>, x) \<in> rf_sr; idx' = unat idx; 146 idx < 2 ^ asid_high_bits \<rbrakk> 147 \<Longrightarrow> case x64KSASIDTable (ksArchState \<sigma>) 148 idx of 149 None \<Rightarrow> 150 index (x86KSASIDTable_' (globals x)) 151 idx' = 152 NULL 153 | Some v \<Rightarrow> 154 index (x86KSASIDTable_' (globals x)) 155 idx' = Ptr v \<and> 156 index (x86KSASIDTable_' (globals x)) 157 idx' \<noteq> NULL" 158 apply (drule rf_asidTable [where idx=idx]) 159 apply fastforce 160 apply (simp add: mask_def) 161 apply (simp add: minus_one_helper3) 162 apply (clarsimp split: option.splits) 163 done 164 165lemma asidLowBits_handy_convs: 166 "sint Kernel_C.asidLowBits = 9" 167 "Kernel_C.asidLowBits \<noteq> 0x20" 168 "unat Kernel_C.asidLowBits = asid_low_bits" 169 by (simp add: Kernel_C.asidLowBits_def asid_low_bits_def)+ 170 171lemma rf_sr_x86KSASIDTable: 172 "\<lbrakk> (s, s') \<in> rf_sr; n \<le> 2 ^ asid_high_bits - 1 \<rbrakk> 173 \<Longrightarrow> index (x86KSASIDTable_' (globals s')) (unat n) 174 = option_to_ptr (x64KSASIDTable (ksArchState s) n)" 175 by (clarsimp simp: rf_sr_def cstate_relation_def Let_def 176 carch_state_relation_def array_relation_def) 177 178lemma asid_high_bits_word_bits: 179 "asid_high_bits < word_bits" 180 by (simp add: asid_high_bits_def word_bits_def) 181 182lemma page_map_l4_at'_array_assertion: 183 assumes "(s,s') \<in> rf_sr" 184 assumes "page_map_l4_at' pm s" 185 shows "array_assertion (pml4e_Ptr pm) (2^ptTranslationBits) (hrs_htd (t_hrs_' (globals s')))" 186 using assms array_assertion_abs_pml4[where n="\<lambda>_. 2^ptTranslationBits" and x="\<lambda>_. (1::nat)"] 187 by (simp add: bit_simps) 188 189lemma vspace_at_asid_cross_over: 190 "\<lbrakk> vspace_at_asid' pm asid s; asid \<le> mask asid_bits; 191 (s, s') \<in> rf_sr\<rbrakk> 192 \<Longrightarrow> \<exists>apptr ap. index (x86KSASIDTable_' (globals s')) (unat (asid >> asid_low_bits)) 193 = (ap_Ptr apptr) \<and> cslift s' (ap_Ptr apptr) = Some (asid_pool_C ap) 194 \<and> asid_map_lift (index ap (unat (asid && mask asid_low_bits))) 195 = Some (Asid_map_asid_map_vspace \<lparr>vspace_root_CL = pm\<rparr>) 196 \<and> is_aligned pm pml4Bits 197 \<and> array_assertion (pml4e_Ptr pm) 512 (hrs_htd (t_hrs_' (globals s')))" 198 apply (clarsimp simp: vspace_at_asid'_def) 199 apply (subgoal_tac "asid >> asid_low_bits \<le> 2 ^ asid_high_bits - 1") 200 prefer 2 201 apply (simp add: asid_high_bits_word_bits) 202 apply (rule shiftr_less_t2n) 203 apply (simp add: mask_def) 204 apply (simp add: asid_low_bits_def asid_high_bits_def asid_bits_def) 205 apply (simp add: rf_sr_x86KSASIDTable) 206 apply (subgoal_tac "ucast (asid_high_bits_of asid) = asid >> asid_low_bits") 207 prefer 2 208 apply (simp add: asid_high_bits_of_def ucast_ucast_mask asid_high_bits_def[symmetric]) 209 apply (subst mask_eq_iff_w2p, simp add: asid_high_bits_def word_size) 210 apply (rule shiftr_less_t2n) 211 apply (simp add: mask_def, simp add: asid_bits_def asid_low_bits_def asid_high_bits_def) 212 apply (simp add: option_to_ptr_def option_to_0_def) 213 apply (rule cmap_relationE1 [OF rf_sr_cpspace_asidpool_relation], 214 assumption, erule ko_at_projectKO_opt) 215 apply (clarsimp simp: casid_pool_relation_def array_relation_def 216 split: asid_pool_C.split_asm) 217 apply (apply_conjunct \<open>solves \<open>simp add: page_map_l4_at'_def\<close>\<close>) 218 apply (drule spec, drule mp, rule word_and_mask_le_2pm1[of asid]) 219 using page_map_l4_at'_array_assertion 220 by (simp add: asid_map_relation_def bit_simps asid_bits_defs asid_bits_of_defs ucast_ucast_mask 221 split: option.splits asid_map_CL.splits) 222 223(* FIXME remove *) 224lemmas findVSpaceForASIDAssert_pd_at_wp2 = findVSpaceForASIDAssert_vs_at_wp 225 226lemma asid_shiftr_low_bits_less: 227 "(asid :: machine_word) \<le> mask asid_bits \<Longrightarrow> asid >> asid_low_bits < 0x8" 228 apply (rule_tac y="2 ^ 3" in order_less_le_trans) 229 apply (rule shiftr_less_t2n) 230 apply (simp add: le_mask_iff_lt_2n[THEN iffD1] asid_bits_def asid_low_bits_def) 231 apply simp 232 done 233 234lemma array_relation_update: 235 "\<lbrakk> array_relation R bnd table (arr :: 'a['b :: finite]); 236 x' = unat (x :: ('td :: len) word); R v v'; 237 unat bnd < card (UNIV :: 'b set) \<rbrakk> 238 \<Longrightarrow> array_relation R bnd (table (x := v)) 239 (Arrays.update arr x' v')" 240 by (simp add: array_relation_def word_le_nat_alt split: if_split) 241 242definition 243 vm_fault_type_from_H :: "vmfault_type \<Rightarrow> machine_word" 244where 245 "vm_fault_type_from_H fault \<equiv> 246 case fault of 247 vmfault_type.X64DataFault \<Rightarrow> scast Kernel_C.X86DataFault 248 | vmfault_type.X64InstructionFault \<Rightarrow> scast Kernel_C.X86InstructionFault" 249 250lemmas mask_64_id[simp] = mask_len_id[where 'a=64, folded word_bits_def] 251 mask_len_id[where 'a=64, simplified] 252 253(* FIXME: automate this *) 254lemma seL4_Fault_VMFault_new'_spec: 255 "\<lbrace> \<lambda>s. s = \<sigma> \<rbrace> seL4_Fault_VMFault_new' addr FSR i 256 \<lbrace> \<lambda>r s. s = \<sigma> 257 \<and> seL4_Fault_VMFault_lift r = \<lparr>address_CL = addr, FSR_CL = FSR && mask 5, instructionFault_CL = i && mask 1\<rparr> 258 \<and> seL4_Fault_get_tag r = scast seL4_Fault_VMFault \<rbrace>" 259 apply (rule hoare_weaken_pre, rule hoare_strengthen_post) 260 apply (rule autocorres_transfer_spec_no_modifies 261 [where cs="undefined\<lparr>globals := \<sigma>, address_' := addr, 262 FSR_' := FSR, instructionFault_' := i\<rparr>", 263 OF seL4_Fault_VMFault_new'_def seL4_Fault_VMFault_new_spec 264 seL4_Fault_VMFault_new_modifies]) 265 by auto 266 267lemma no_fail_seL4_Fault_VMFault_new': 268 "no_fail \<top> (seL4_Fault_VMFault_new' addr fault i)" 269 apply (rule terminates_spec_no_fail'[OF seL4_Fault_VMFault_new'_def seL4_Fault_VMFault_new_spec]) 270 apply clarsimp 271 apply terminates_trivial 272 done 273 274lemma returnVMFault_corres: 275 "\<lbrakk> addr = addr'; i = i' && mask 1; fault = fault' && mask 5 \<rbrakk> \<Longrightarrow> 276 corres_underlying 277 {(x, y). cstate_relation x y} True True 278 (lift_rv id (\<lambda>y. ()) (\<lambda>e. e) (\<lambda>_ _. False) 279 (\<lambda>e f e'. f = SCAST(32 signed \<rightarrow> 64) EXCEPTION_FAULT \<and> 280 (\<exists>vf. e = ArchFault (VMFault (address_CL vf) [instructionFault_CL vf, FSR_CL vf]) 281 \<and> errfault e' = Some (SeL4_Fault_VMFault vf)))) 282 \<top> \<top> 283 (throwError (Fault_H.fault.ArchFault (VMFault addr [i, fault]))) 284 (do f <- seL4_Fault_VMFault_new' addr' fault' i'; 285 _ <- modify (current_fault_'_update (\<lambda>_. f)); 286 e <- gets errglobals; 287 return (scast EXCEPTION_FAULT, e) 288 od)" 289 apply (rule corres_symb_exec_r) 290 apply (rename_tac vmf) 291 apply (rule_tac F="seL4_Fault_VMFault_lift vmf = \<lparr>address_CL = addr, FSR_CL = fault && mask 5, instructionFault_CL = i && mask 1\<rparr> 292 \<and> seL4_Fault_get_tag vmf = scast seL4_Fault_VMFault" 293 in corres_gen_asm2) 294 apply (rule lift_rv_throwError; 295 clarsimp simp: exception_defs seL4_Fault_VMFault_lift) 296 apply (wpsimp wp: valid_spec_to_wp'[OF seL4_Fault_VMFault_new'_spec] 297 no_fail_seL4_Fault_VMFault_new' 298 simp: mask_twice)+ 299 done 300 301lemma handleVMFault_ccorres: 302 "ccorres ((\<lambda>f ex v. ex = scast EXCEPTION_FAULT 303 \<and> (\<exists>vf. f = ArchFault (VMFault (address_CL vf) 304 [instructionFault_CL vf, FSR_CL vf]) 305 \<and> errfault v = Some (SeL4_Fault_VMFault vf))) \<currency> \<bottom>\<bottom>) 306 (liftxf errstate id (K ()) ret__unsigned_long_') 307 \<top> 308 (UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace> 309 \<inter> \<lbrace>\<acute>vm_faultType = vm_fault_type_from_H vm_fault\<rbrace>) 310 [] 311 (handleVMFault thread vm_fault) 312 (Call handleVMFault_'proc)" 313 (* FIXME x64: make this a real ac_init *) 314 apply (rule corres_to_ccorres_rv_spec_errglobals[OF _ _ refl], 315 rule handleVMFault'_ac_corres[simplified o_def]) 316 prefer 3 apply simp 317 apply (simp add: handleVMFault_def handleVMFault'_def liftE_bindE condition_const 318 ucast_ucast_mask bind_assoc) 319 apply (rule corres_split[OF _ getFaultAddr_ccorres[ac]], drule sym, clarsimp) 320 apply (rule corres_split[OF _ getRegister_ccorres[ac]], drule sym, clarsimp) 321 apply (wpc; simp add: vm_fault_type_from_H_def X86InstructionFault_def X86DataFault_def 322 true_def false_def bind_assoc) 323 apply (rule returnVMFault_corres; 324 clarsimp simp: exception_defs mask_twice lift_rv_def)+ 325 apply (wpsimp simp: mask_def | terminates_trivial)+ 326 done 327 328lemma unat_asidLowBits [simp]: 329 "unat Kernel_C.asidLowBits = asidLowBits" 330 by (simp add: asidLowBits_def Kernel_C.asidLowBits_def asid_low_bits_def) 331 332lemma rf_sr_asidTable_None: 333 "\<lbrakk> (\<sigma>, x) \<in> rf_sr; asid && mask asid_bits = asid; valid_arch_state' \<sigma> \<rbrakk> \<Longrightarrow> 334 (index (x86KSASIDTable_' (globals x)) (unat (asid >> asid_low_bits)) = ap_Ptr 0) = 335 (x64KSASIDTable (ksArchState \<sigma>) (ucast (asid_high_bits_of asid)) = None)" 336 apply (simp add: asid_high_bits_of_def ucast_ucast_mask) 337 apply (subgoal_tac "(asid >> asid_low_bits) && mask 3 = asid >> asid_low_bits")(*asid_high_bits*) 338 prefer 2 339 apply (rule word_eqI) 340 apply (subst (asm) bang_eq) 341 apply (simp add: word_size nth_shiftr asid_bits_def asid_low_bits_def) 342 apply (case_tac "n < 3", simp) (*asid_high_bits*) 343 apply (clarsimp simp: linorder_not_less) 344 apply (erule_tac x="n+9" in allE) (*asid_low_bits*) 345 apply simp 346 apply simp 347 apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def carch_state_relation_def) 348 apply (simp add: array_relation_def option_to_0_def) 349 apply (erule_tac x="asid >> asid_low_bits" in allE) 350 apply (erule impE) 351 prefer 2 352 apply (drule sym [where t="index a b" for a b]) 353 apply (simp add: option_to_0_def option_to_ptr_def split: option.splits) 354 apply (clarsimp simp: valid_arch_state'_def valid_asid_table'_def ran_def) 355 apply (simp add: and_mask_eq_iff_le_mask) 356 apply (simp add: asid_high_bits_def mask_def) 357 done 358 359lemma leq_asid_bits_shift: 360 "x \<le> mask asid_bits \<Longrightarrow> (x::machine_word) >> asid_low_bits \<le> mask asid_high_bits" 361 apply (rule word_leI) 362 apply (simp add: nth_shiftr word_size) 363 apply (rule ccontr) 364 apply (clarsimp simp: linorder_not_less asid_high_bits_def asid_low_bits_def) 365 apply (simp add: mask_def) 366 apply (simp add: upper_bits_unset_is_l2p_64 [symmetric]) 367 apply (simp add: asid_bits_def word_bits_def) 368 apply (erule_tac x="n+9" in allE) (*asid_low_bits*) 369 apply (simp add: linorder_not_less) 370 apply (drule test_bit_size) 371 apply (simp add: word_size) 372 done 373 374lemma ucast_asid_high_bits_is_shift: 375 "asid \<le> mask asid_bits \<Longrightarrow> ucast (asid_high_bits_of asid) = (asid >> asid_low_bits)" 376 apply (simp add: mask_def upper_bits_unset_is_l2p_64 [symmetric]) 377 apply (simp add: asid_high_bits_of_def) 378 apply (rule word_eqI[rule_format]) 379 apply (simp add: word_size nth_shiftr nth_ucast asid_low_bits_def asid_bits_def word_bits_def) 380 apply (erule_tac x="n+9" in allE)(*asid_low_bits*) 381 apply simp 382 apply (case_tac "n < 3", simp) (*asid_high_bits*) 383 apply (simp add: linorder_not_less) 384 apply (rule notI) 385 apply (frule test_bit_size) 386 apply (simp add: word_size) 387 done 388 389lemma clift_ptr_safe: 390 "clift (h, x) ptr = Some a 391 \<Longrightarrow> ptr_safe ptr x" 392 by (erule lift_t_ptr_safe[where g = c_guard]) 393 394lemma clift_ptr_safe2: 395 "clift htd ptr = Some a 396 \<Longrightarrow> ptr_safe ptr (hrs_htd htd)" 397 by (cases htd, simp add: hrs_htd_def clift_ptr_safe) 398 399lemma ptTranslationBits_mask_le: "(x::machine_word) && 0x1FF < 0x200" 400 by (word_bitwise) 401 402lemma lookupPML4Slot_spec: 403 "\<forall>s. \<Gamma> \<turnstile> \<lbrace> s. array_assertion (pml4_' s) (2 ^ ptTranslationBits) (hrs_htd (\<acute>t_hrs)) \<rbrace> 404 Call lookupPML4Slot_'proc 405 \<lbrace> \<acute>ret__ptr_to_struct_pml4e_C = Ptr (lookupPML4Slot (ptr_val (pml4_' s)) (vptr_' s)) \<rbrace>" 406 apply vcg 407 apply clarsimp 408 apply (clarsimp simp: lookup_pml4_slot_def) 409 apply (simp add: bit_simps) 410 apply (subst array_assertion_shrink_right, assumption) 411 apply (rule unat_le_helper, clarsimp simp: ptTranslationBits_mask_le order_less_imp_le) 412 apply (simp add: Let_def word_sle_def bit_simps getPML4Index_def mask_def) 413 apply (case_tac pml4) 414 apply (simp add: shiftl_t2n) 415 done 416 417lemma ccorres_pre_getObject_pml4e: 418 assumes cc: "\<And>rv. ccorres r xf (P rv) (P' rv) hs (f rv) c" 419 shows "ccorres r xf 420 (\<lambda>s. (\<forall>pml4e. ko_at' pml4e p s \<longrightarrow> P pml4e s)) 421 {s. \<forall>pml4e pml4e'. cslift s (pml4e_Ptr p) = Some pml4e' \<and> cpml4e_relation pml4e pml4e' 422 \<longrightarrow> s \<in> P' pml4e} 423 hs (getObject p >>= (\<lambda>rv. f rv)) c" 424 apply (rule ccorres_guard_imp2) 425 apply (rule ccorres_symb_exec_l) 426 apply (rule ccorres_guard_imp2) 427 apply (rule cc) 428 apply (rule conjI) 429 apply (rule_tac Q="ko_at' rv p s" in conjunct1) 430 apply assumption 431 apply assumption 432 apply (wp getPML4E_wp empty_fail_getObject | simp)+ 433 apply clarsimp 434 apply (erule cmap_relationE1 [OF rf_sr_cpml4e_relation], 435 erule ko_at_projectKO_opt) 436 apply simp 437 done 438 439lemma ccorres_pre_getObject_pde: 440 assumes cc: "\<And>rv. ccorres r xf (P rv) (P' rv) hs (f rv) c" 441 shows "ccorres r xf 442 (\<lambda>s. (\<forall>pde. ko_at' pde p s \<longrightarrow> P pde s)) 443 {s. \<forall>pde pde'. cslift s (pde_Ptr p) = Some pde' \<and> cpde_relation pde pde' 444 \<longrightarrow> s \<in> P' pde} 445 hs (getObject p >>= (\<lambda>rv. f rv)) c" 446 apply (rule ccorres_guard_imp2) 447 apply (rule ccorres_symb_exec_l) 448 apply (rule ccorres_guard_imp2) 449 apply (rule cc) 450 apply (rule conjI) 451 apply (rule_tac Q="ko_at' rv p s" in conjunct1) 452 apply assumption 453 apply assumption 454 apply (wp getPDE_wp empty_fail_getObject | simp)+ 455 apply clarsimp 456 apply (erule cmap_relationE1 [OF rf_sr_cpde_relation], 457 erule ko_at_projectKO_opt) 458 apply simp 459 done 460 461lemma ptrFromPAddr_spec: 462 "\<forall>s. \<Gamma> \<turnstile> {s} 463 Call ptrFromPAddr_'proc 464 \<lbrace> \<acute>ret__ptr_to_void = Ptr (ptrFromPAddr (paddr_' s) ) \<rbrace>" 465 apply vcg 466 apply (simp add: X64.ptrFromPAddr_def X64.pptrBase_def) 467 done 468 469lemma addrFromPPtr_spec: 470 "\<forall>s. \<Gamma> \<turnstile> {s} 471 Call addrFromPPtr_'proc 472 \<lbrace> \<acute>ret__unsigned_long = (addrFromPPtr (ptr_val (pptr_' s)) ) \<rbrace>" 473 apply vcg 474 apply (simp add: addrFromPPtr_def X64.pptrBase_def) 475 done 476 477lemma corres_symb_exec_unknown_r: 478 assumes "\<And>rv. corres_underlying sr nf nf' r P P' a (c rv)" 479 shows "corres_underlying sr nf nf' r P P' a (unknown >>= c)" 480 apply (simp add: unknown_def) 481 apply (rule corres_symb_exec_r[OF assms]; wp select_inv non_fail_select) 482 done 483 484(* FIXME: automate this. *) 485lemma lookupPML4Slot'_spec: 486 "\<lbrace> \<lambda>s. s = \<sigma> \<and> array_assertion pm (2 ^ ptTranslationBits) (hrs_htd (t_hrs_' s)) \<rbrace> 487 lookupPML4Slot' pm vptr 488 \<lbrace> \<lambda>r s. s = \<sigma> \<and> r = pml4e_Ptr (lookupPML4Slot (ptr_val pm) vptr) \<rbrace>" 489 apply (rule hoare_weaken_pre, rule hoare_strengthen_post) 490 apply (rule autocorres_transfer_spec_no_modifies 491 [where cs="undefined\<lparr>globals := \<sigma>, pml4_' := pm, vptr_' := vptr\<rparr>" 492 and P="\<lambda>s. array_assertion (pml4_' s) (2 ^ ptTranslationBits) (hrs_htd (t_hrs_' (globals s)))", 493 OF lookupPML4Slot'_def lookupPML4Slot_spec lookupPML4Slot_modifies]) 494 by auto 495 496lemma no_fail_lookupPML4Slot': 497 "no_fail (\<lambda>s. array_assertion pm (2 ^ ptTranslationBits) (hrs_htd (t_hrs_' s))) (lookupPML4Slot' pm vptr)" 498 apply (rule terminates_spec_no_fail[OF lookupPML4Slot'_def lookupPML4Slot_spec]; clarsimp) 499 apply terminates_trivial 500 done 501 502lemmas corres_symb_exec_lookupPML4Slot' = 503 valid_spec_to_corres_gen_symb_exec_r[OF lookupPML4Slot'_spec no_fail_lookupPML4Slot'] 504 505(* FIXME: automate this. *) 506lemma pml4e_ptr_get_present'_spec: 507 "\<lbrace> \<lambda>s. s = \<sigma> \<and> s \<Turnstile>\<^sub>g pml4e_ptr \<rbrace> 508 pml4e_ptr_get_present' pml4e_ptr 509 \<lbrace> \<lambda>r s. s = \<sigma> \<and> r = pml4e_CL.present_CL (pml4e_lift (the (gslift s pml4e_ptr))) \<rbrace>" 510 apply (rule hoare_weaken_pre, rule hoare_strengthen_post) 511 apply (rule autocorres_transfer_spec_no_modifies 512 [where cs="undefined\<lparr>globals := \<sigma>, pml4e_ptr_' := pml4e_ptr\<rparr>" 513 and P="\<lambda>s. s \<Turnstile>\<^sub>c pml4e_ptr_' s", 514 OF pml4e_ptr_get_present'_def pml4e_ptr_get_present_spec 515 pml4e_ptr_get_present_modifies]) 516 by (auto dest: spec[where x="undefined\<lparr>globals := \<sigma>\<rparr>"]) 517 518lemma pml4e_ptr_get_present'_no_fail: 519 "no_fail (\<lambda>s. s \<Turnstile>\<^sub>g pml4e_ptr) (pml4e_ptr_get_present' pml4e_ptr)" 520 apply (rule terminates_spec_no_fail[OF pml4e_ptr_get_present'_def pml4e_ptr_get_present_spec]; clarsimp) 521 apply terminates_trivial 522 done 523 524lemmas corres_symb_exec_pml4e_ptr_get_present' = 525 valid_spec_to_corres_symb_exec_r[OF pml4e_ptr_get_present'_spec pml4e_ptr_get_present'_no_fail] 526 527lemma lookup_fault_missing_capability_new'_spec: 528 "\<lbrace> \<lambda>s. s = \<sigma> \<rbrace> 529 lookup_fault_missing_capability_new' bits 530 \<lbrace> \<lambda>r s. s = \<sigma> 531 \<and> lookup_fault_missing_capability_lift r = 532 \<lparr>lookup_fault_missing_capability_CL.bitsLeft_CL = bits && mask 7\<rparr> 533 \<and> lookup_fault_get_tag r = scast lookup_fault_missing_capability \<rbrace>" 534 apply (rule hoare_weaken_pre, rule hoare_strengthen_post) 535 apply (rule autocorres_transfer_spec_no_modifies 536 [where cs="undefined\<lparr>globals := \<sigma>, bitsLeft_' := bits\<rparr>" and P=\<top>, 537 OF lookup_fault_missing_capability_new'_def 538 lookup_fault_missing_capability_new_spec 539 lookup_fault_missing_capability_new_modifies]) 540 by (auto dest: spec[where x="undefined\<lparr>globals := \<sigma>\<rparr>"]) 541 542lemma lookup_fault_missing_capability_new'_no_fail: 543 "no_fail \<top> (lookup_fault_missing_capability_new' bits)" 544 apply (rule terminates_spec_no_fail'[OF lookup_fault_missing_capability_new'_def 545 lookup_fault_missing_capability_new_spec]; 546 clarsimp) 547 apply terminates_trivial 548 done 549 550lemmas corres_symb_exec_lookup_fault_missing_capability_new' = 551 valid_spec_to_corres_gen_symb_exec_r'[OF lookup_fault_missing_capability_new'_spec 552 lookup_fault_missing_capability_new'_no_fail] 553 554lemma pml4e_ptr_get_pdpt_base_address'_spec: 555 "\<lbrace> \<lambda>s. s = \<sigma> \<and> s \<Turnstile>\<^sub>g pml4e_ptr \<rbrace> 556 pml4e_ptr_get_pdpt_base_address' pml4e_ptr 557 \<lbrace> \<lambda>r s. s = \<sigma> \<and> r = pdpt_base_address_CL (pml4e_lift (the (gslift s pml4e_ptr))) \<rbrace>" 558 apply (rule hoare_weaken_pre, rule hoare_strengthen_post) 559 apply (rule autocorres_transfer_spec_no_modifies 560 [where cs="undefined\<lparr>globals := \<sigma>, pml4e_ptr_' := pml4e_ptr\<rparr>" 561 and P="\<lambda>s. s \<Turnstile>\<^sub>c pml4e_ptr_' s", 562 OF pml4e_ptr_get_pdpt_base_address'_def 563 pml4e_ptr_get_pdpt_base_address_spec 564 pml4e_ptr_get_pdpt_base_address_modifies]) 565 by (auto dest: spec[where x="undefined\<lparr>globals := \<sigma>\<rparr>"]) 566 567lemma pml4e_ptr_get_pdpt_base_address'_no_fail: 568 "no_fail (\<lambda>s. s \<Turnstile>\<^sub>g pml4e_ptr) (pml4e_ptr_get_pdpt_base_address' pml4e_ptr)" 569 apply (rule terminates_spec_no_fail[OF pml4e_ptr_get_pdpt_base_address'_def 570 pml4e_ptr_get_pdpt_base_address_spec]; 571 clarsimp) 572 apply terminates_trivial 573 done 574 575lemmas corres_symb_exec_pml4e_ptr_get_pdpt_base_address' = 576 valid_spec_to_corres_symb_exec_r[OF pml4e_ptr_get_pdpt_base_address'_spec 577 pml4e_ptr_get_pdpt_base_address'_no_fail] 578 579lemma ptrFromPAddr'_spec: 580 "\<lbrace> \<lambda>s. s = \<sigma> \<rbrace> 581 ptrFromPAddr' paddr 582 \<lbrace> \<lambda>r s. s = \<sigma> \<and> r = Ptr (ptrFromPAddr paddr) \<rbrace>" 583 apply (rule hoare_weaken_pre, rule hoare_strengthen_post) 584 apply (rule autocorres_transfer_spec_no_modifies 585 [where cs="undefined\<lparr>globals := \<sigma>, paddr_' := paddr\<rparr>" and P=\<top>, 586 OF ptrFromPAddr'_def ptrFromPAddr_spec ptrFromPAddr_modifies]) 587 by (auto dest: spec[where x="undefined\<lparr>globals := \<sigma>\<rparr>"]) 588 589lemma ptrFromPAddr'_no_fail: 590 "no_fail \<top> (ptrFromPAddr' paddr)" 591 apply (rule terminates_spec_no_fail'[OF ptrFromPAddr'_def ptrFromPAddr_spec]; clarsimp) 592 apply terminates_trivial 593 done 594 595lemmas corres_symb_exec_ptrFromPAddr' = 596 valid_spec_to_corres_gen_symb_exec_r'[OF ptrFromPAddr'_spec ptrFromPAddr'_no_fail] 597 598(* Move near rf_sr_cpml4e_relation. *) 599lemma cstate_relation_cpml4e_relation: 600 "cstate_relation s s' \<Longrightarrow> 601 cmap_relation (map_to_pml4es (ksPSpace s)) (gslift s') pml4e_Ptr cpml4e_relation" 602 by (clarsimp simp: cstate_relation_def Let_def cpspace_relation_def) 603 604(* Mirrors proof of ccorres_pre_getObject_pml4e. 605 Is there a generic way to lift these existing rules? *) 606lemma corres_pre_getObject_pml4e: 607 assumes corres: "\<And>rv. corres_underlying {(x, y). cstate_relation x y} True True r (P rv) (P' rv) (f rv) c" 608 shows "corres_underlying 609 {(x, y). cstate_relation x y} True True r 610 (\<lambda>s. \<forall>pml4e. ko_at' pml4e p s \<longrightarrow> P pml4e s) 611 (\<lambda>s. \<forall>pml4e pml4e'. gslift s (pml4e_Ptr p) = Some pml4e' \<and> cpml4e_relation pml4e pml4e' 612 \<longrightarrow> P' pml4e s) 613 (getObject p >>= (\<lambda>rv. f rv)) c" 614 apply (rule stronger_corres_guard_imp[OF corres_symb_exec_l'']) 615 apply (rule stronger_corres_guard_imp[OF corres]) 616 apply (rule_tac Q="ko_at' rv p s" in conjunct1, assumption, assumption) 617 apply (wpsimp wp: getPML4E_wp simp: empty_fail_getObject)+ 618 by (auto elim: cmap_relationE1[OF cstate_relation_cpml4e_relation] ko_at_projectKO_opt) 619 620abbreviation 621 "lookupPDPTSlot_xf \<equiv> liftxf errstate 622 lookupPDPTSlot_ret_C.status_C 623 lookupPDPTSlot_ret_C.pdptSlot_C 624 ret__struct_lookupPDPTSlot_ret_C_'" 625 626(* Compare this AutoCorres-based proof with ccorres proof below. *) 627lemma lookupPDPTSlot_ccorres: 628 "ccorres (lookup_failure_rel \<currency> (\<lambda>rv rv'. rv' = pdpte_Ptr rv)) lookupPDPTSlot_xf 629 (page_map_l4_at' pm) 630 (UNIV \<inter> \<lbrace>\<acute>pml4 = Ptr pm \<rbrace> \<inter> \<lbrace>\<acute>vptr = vptr \<rbrace>) 631 [] 632 (lookupPDPTSlot pm vptr) 633 (Call lookupPDPTSlot_'proc)" 634 (* FIXME: get ac_init to do this. *) 635 apply (rule corres_to_ccorres_rv_spec_errglobals[OF _ _ refl], 636 rule lookupPDPTSlot'_ac_corres[simplified o_def]) 637 prefer 3 apply simp 638 apply (simp add: lookupPDPTSlot_def lookupPDPTSlot'_def 639 liftE_bindE condition_const bind_assoc) 640 apply (rule corres_pre_getObject_pml4e; rename_tac pml4e) 641 apply (rule corres_symb_exec_lookupPML4Slot'; rename_tac pml4e_ptr) 642 apply (rule corres_symb_exec_unknown_r; rename_tac undefined) 643 apply (rule corres_symb_exec_pml4e_ptr_get_present'; rename_tac present) 644 apply wpc 645 apply (rule_tac F="present = 0" in corres_gen_asm2) 646 apply (simp add: bind_assoc) 647 apply (rule corres_symb_exec_lookup_fault_missing_capability_new'; rename_tac lookup_fault) 648 apply (rule lift_rv_throwError) 649 apply (simp add: exception_defs) 650 apply (simp add: bind_assoc bit_simps mask_def errglobals_def 651 lookup_fault_missing_capability_lift) 652 apply (rename_tac base_addr acc cd wt ed rights) 653 apply (rule_tac F="present \<noteq> 0" in corres_gen_asm2) 654 apply (simp add: bind_assoc liftE_bind_return_bindE_returnOk liftE_bindE) 655 apply (rule corres_stateAssert_l) 656 apply (rule_tac Q="pd_pointer_table_at' (ptrFromPAddr base_addr)" in corres_cross_over_guard) 657 apply (rule corres_symb_exec_pml4e_ptr_get_pdpt_base_address'; rename_tac base_addr') 658 apply (rule_tac F="base_addr = base_addr'" in corres_gen_asm2) 659 apply (rule corres_symb_exec_ptrFromPAddr') 660 apply (rule corres_guard_r) 661 apply (rule lift_rv_returnOk; 662 simp add: exception_defs lookup_pdpt_slot_no_fail_def getPDPTIndex_def bit_simps 663 shiftl_t2n mask_def) 664 apply (clarsimp simp: Collect_const_mem h_t_valid_clift bit_simps) 665 apply (frule page_map_l4_at_rf_sr, simp add: rf_sr_def, clarsimp) 666 apply (subst array_ptr_valid_array_assertionI, erule h_t_valid_clift, simp+) 667 apply (rule conjI; clarsimp simp: cpml4e_relation_def Let_def) 668 apply (frule pd_pointer_table_at_rf_sr, simp add: rf_sr_def, clarsimp) 669 apply (subst (asm) array_ptr_valid_array_assertionI, erule h_t_valid_clift, simp+) 670 apply (rule unat_le_helper, rule order_trans[OF word_and_le1], simp+) 671 done 672 673(* For comparison, here is the ccorres proof. *) 674lemma lookupPDPTSlot_ccorres': 675 "ccorres (lookup_failure_rel \<currency> (\<lambda>rv rv'. rv' = pdpte_Ptr rv)) lookupPDPTSlot_xf 676 (page_map_l4_at' pm) 677 (UNIV \<inter> \<lbrace>\<acute>pml4 = Ptr pm \<rbrace> \<inter> \<lbrace>\<acute>vptr = vptr \<rbrace>) 678 [] 679 (lookupPDPTSlot pm vptr) 680 (Call lookupPDPTSlot_'proc)" 681 apply (cinit lift: pml4_' vptr_') 682 apply (simp add: liftE_bindE) 683 apply (rule ccorres_pre_getObject_pml4e) 684 apply csymbr 685 apply csymbr 686 apply csymbr 687 apply (rule ccorres_abstract_cleanup) 688 apply (rule_tac P="(ret__unsigned_longlong = 0) = (rv = X64_H.InvalidPML4E)" 689 in ccorres_gen_asm2) 690 apply (wpc; ccorres_rewrite) 691 apply (rule_tac P=\<top> and P' =UNIV in ccorres_from_vcg_throws) 692 apply (rule allI, rule conseqPre, vcg) 693 apply (clarsimp simp: throwError_def return_def syscall_error_rel_def) 694 apply (clarsimp simp: EXCEPTION_NONE_def EXCEPTION_LOOKUP_FAULT_def) 695 apply (simp add: lookup_fault_missing_capability_lift) 696 apply (simp add: mask_def bit_simps) 697 apply (thin_tac "_ = PDPointerTablePML4E _ _ _ _ _ _") 698 apply (simp add: bind_liftE_distrib liftE_bindE returnOk_liftE[symmetric]) 699 apply (rule ccorres_stateAssert) 700 apply (rule_tac P="pd_pointer_table_at' (ptrFromPAddr (pml4eTable rv)) 701 and ko_at' rv (lookup_pml4_slot pm vptr) 702 and K (isPDPointerTablePML4E rv)" 703 and P'=UNIV 704 in ccorres_from_vcg_throws) 705 apply (rule allI, rule conseqPre, vcg) 706 apply (clarsimp simp: returnOk_def return_def) 707 apply (frule (1) pd_pointer_table_at_rf_sr, clarsimp) 708 apply (erule cmap_relationE1[OF rf_sr_cpml4e_relation], erule ko_at_projectKO_opt) 709 apply (clarsimp simp: typ_heap_simps cpml4e_relation_def Let_def isPDPointerTablePML4E_def 710 split: pml4e.split_asm) 711 apply (subst array_ptr_valid_array_assertionI, erule h_t_valid_clift, simp+) 712 apply (rule unat_le_helper, rule order_trans[OF word_and_le1], simp) 713 apply (simp add: lookup_pdpt_slot_no_fail_def getPDPTIndex_def bit_simps shiftl_t2n mask_def) 714 apply (clarsimp simp: Collect_const_mem h_t_valid_clift bit_simps) 715 apply (frule(1) page_map_l4_at_rf_sr, clarsimp) 716 apply (subst array_ptr_valid_array_assertionI, erule h_t_valid_clift, simp+) 717 apply (clarsimp simp: cpml4e_relation_def Let_def isPDPointerTablePML4E_def 718 split: pml4e.splits) 719 done 720 721lemma ccorres_pre_getObject_pdpte: 722 assumes cc: "\<And>rv. ccorres r xf (P rv) (P' rv) hs (f rv) c" 723 shows "ccorres r xf 724 (\<lambda>s. (\<forall>pdpte. ko_at' pdpte p s \<longrightarrow> P pdpte s)) 725 {s. \<forall>pdpte pdpte'. cslift s (pdpte_Ptr p) = Some pdpte' \<and> cpdpte_relation pdpte pdpte' 726 \<longrightarrow> s \<in> P' pdpte} 727 hs (getObject p >>= (\<lambda>rv. f rv)) c" 728 apply (rule ccorres_guard_imp2) 729 apply (rule ccorres_symb_exec_l) 730 apply (rule ccorres_guard_imp2) 731 apply (rule cc) 732 apply (rule conjI) 733 apply (rule_tac Q="ko_at' rv p s" in conjunct1) 734 apply assumption 735 apply assumption 736 apply (wp getPDPTE_wp empty_fail_getObject | simp)+ 737 apply clarsimp 738 apply (erule cmap_relationE1 [OF rf_sr_cpdpte_relation], 739 erule ko_at_projectKO_opt) 740 apply simp 741 done 742 743abbreviation 744 "lookupPDSlot_xf \<equiv> liftxf errstate lookupPDSlot_ret_C.status_C lookupPDSlot_ret_C.pdSlot_C 745 ret__struct_lookupPDSlot_ret_C_'" 746 747lemma pdpte_case_isPageDirectoryPDPTE: 748 "(case pdpte of PageDirectoryPDPTE p _ _ _ _ _ \<Rightarrow> fn p | _ \<Rightarrow> g) 749 = (if isPageDirectoryPDPTE pdpte then fn (pdpteTable pdpte) else g)" 750 by (cases pdpte, simp_all add: isPageDirectoryPDPTE_def) 751 752lemma lookupPDSlot_ccorres: 753 "ccorres (lookup_failure_rel \<currency> (\<lambda>rv rv'. rv' = pde_Ptr rv)) lookupPDSlot_xf 754 (page_map_l4_at' pm) 755 (UNIV \<inter> \<lbrace>\<acute>pml4 = Ptr pm \<rbrace> \<inter> \<lbrace>\<acute>vptr = vptr \<rbrace>) 756 [] 757 (lookupPDSlot pm vptr) 758 (Call lookupPDSlot_'proc)" 759 apply (cinit lift: pml4_' vptr_') 760 apply (rename_tac vptr' pml4) 761 apply (simp add: liftE_bindE pdpte_case_isPageDirectoryPDPTE) 762 apply (ctac add: lookupPDPTSlot_ccorres) 763 apply (rename_tac pdpte_ptr lookup_ret, case_tac lookup_ret, clarsimp) 764 apply (rule ccorres_pre_getObject_pdpte, rename_tac pdpte) 765 apply (csymbr, rename_tac page_size, rule ccorres_abstract_cleanup) 766 apply (rule ccorres_rhs_assoc2) 767 apply (rule_tac ccorres_symb_exec_r) 768 apply (rule ccorres_if_lhs) 769 apply (rule ccorres_cond_false) 770 apply (simp add: bind_liftE_distrib liftE_bindE returnOk_liftE[symmetric]) 771 apply (rule ccorres_stateAssert) 772 apply (rule_tac P="page_directory_at' (ptrFromPAddr (pdpteTable pdpte)) 773 and ko_at' pdpte pdpte_ptr 774 and K (isPageDirectoryPDPTE pdpte)" 775 and P'=UNIV 776 in ccorres_from_vcg_throws) 777 apply (rule allI, rule conseqPre, vcg) 778 apply (clarsimp simp: returnOk_def return_def, rename_tac s s') 779 apply (frule (1) page_directory_at_rf_sr, clarsimp, rename_tac pd') 780 apply (rule cmap_relationE1[OF rf_sr_cpdpte_relation], assumption, 781 erule ko_at_projectKO_opt, rename_tac pdpte') 782 apply (clarsimp simp: typ_heap_simps cpdpte_relation_def Let_def isPageDirectoryPDPTE_def 783 split: pdpte.splits, 784 rename_tac pd_ptr ac cd wt xd rights) 785 apply (rule context_conjI, simp add: pdpte_lift_def Let_def split: if_splits, intro imp_ignore) 786 apply (clarsimp simp: pdpte_lift_def pdpte_pdpte_pd_lift_def Let_def pdpte_tag_defs) 787 apply (subst array_ptr_valid_array_assertionI[OF h_t_valid_clift], assumption, simp) 788 apply (rule unat_le_helper[OF order_trans[OF word_and_le1]], simp) 789 apply (simp add: lookup_pd_slot_no_fail_def getPDIndex_def mask_def bit_simps shiftl_t2n) 790 apply (rule ccorres_cond_true) 791 apply (rule_tac P=\<top> and P'=UNIV in ccorres_from_vcg_throws) 792 apply (rule allI, rule conseqPre, vcg) 793 apply (clarsimp simp: throwError_def return_def syscall_error_rel_def) 794 apply (clarsimp simp: EXCEPTION_NONE_def EXCEPTION_LOOKUP_FAULT_def) 795 apply (simp add: lookup_fault_missing_capability_lift mask_def bit_simps) 796 apply vcg 797 apply (rule conseqPre, vcg, clarsimp) 798 apply (ccorres_rewrite, rename_tac lookupPDPTSlot_errstate) 799 apply (rule_tac P=\<top> and P'="{s. lookupPDPTSlot_errstate = errstate s}" 800 in ccorres_from_vcg_throws) 801 apply (rule allI, rule conseqPre, vcg, clarsimp simp: throwError_def return_def) 802 apply (clarsimp, wp) 803 apply (vcg exspec=lookupPDPTSlot_modifies) 804 apply clarsimp 805 apply (frule h_t_valid_clift; simp) 806 apply (strengthen imp_ignore[where A="Ex P" for P]) 807 apply (clarsimp simp: cpdpte_relation_def isPageDirectoryPDPTE_def Let_def 808 pdpte_lift_def pdpte_pdpte_pd_lift_def pdpte_tag_defs 809 split: X64_H.pdpte.splits if_splits) 810 done 811 812abbreviation 813 "lookupPTSlot_xf \<equiv> liftxf errstate lookupPTSlot_ret_C.status_C lookupPTSlot_ret_C.ptSlot_C 814 ret__struct_lookupPTSlot_ret_C_'" 815 816lemma pde_case_isPageTablePDE: 817 "(case pde of PageTablePDE p _ _ _ _ _ \<Rightarrow> fn p | _ \<Rightarrow> g) 818 = (if isPageTablePDE pde then fn (pdeTable pde) else g)" 819 by (cases pde, simp_all add: isPageTablePDE_def) 820 821lemma lookupPTSlot_ccorres: 822 "ccorres (lookup_failure_rel \<currency> (\<lambda>rv rv'. rv' = pte_Ptr rv)) lookupPTSlot_xf 823 (page_map_l4_at' pm) 824 (UNIV \<inter> \<lbrace>\<acute>vspace = Ptr pm \<rbrace> \<inter> \<lbrace>\<acute>vptr = vptr \<rbrace>) 825 [] 826 (lookupPTSlot pm vptr) 827 (Call lookupPTSlot_'proc)" 828 apply (cinit lift: vspace_' vptr_') 829 apply (rename_tac vptr' pml4) 830 apply (simp add: liftE_bindE pde_case_isPageTablePDE) 831 apply (ctac add: lookupPDSlot_ccorres) 832 apply (rename_tac pde_ptr lookup_ret, case_tac lookup_ret, clarsimp) 833 apply (rule ccorres_pre_getObject_pde, rename_tac pde) 834 apply (csymbr, rename_tac page_size, rule ccorres_abstract_cleanup) 835 apply (rule ccorres_rhs_assoc2) 836 apply (rule_tac ccorres_symb_exec_r) 837 apply (rule ccorres_if_lhs) 838 apply (rule ccorres_cond_false) 839 apply (simp add: bind_liftE_distrib liftE_bindE returnOk_liftE[symmetric]) 840 apply (rule ccorres_stateAssert) 841 apply (rule_tac P="page_table_at' (ptrFromPAddr (pdeTable pde)) 842 and ko_at' pde pde_ptr 843 and K (isPageTablePDE pde)" 844 and P'=UNIV 845 in ccorres_from_vcg_throws) 846 apply (rule allI, rule conseqPre, vcg) 847 apply (clarsimp simp: returnOk_def return_def, rename_tac s s') 848 apply (frule (1) page_table_at_rf_sr, clarsimp, rename_tac pt') 849 apply (rule cmap_relationE1[OF rf_sr_cpde_relation], assumption, 850 erule ko_at_projectKO_opt, rename_tac pdpte') 851 apply (clarsimp simp: typ_heap_simps cpde_relation_def Let_def isPageTablePDE_def 852 split: pde.splits, 853 rename_tac pt_ptr ac cd wt xd rights) 854 apply (rule context_conjI, simp add: pde_lift_def Let_def split: if_splits, intro imp_ignore) 855 apply (clarsimp simp: pde_lift_def pde_pde_pt_lift_def Let_def pde_tag_defs) 856 apply (subst array_ptr_valid_array_assertionI[OF h_t_valid_clift], assumption, simp) 857 apply (rule unat_le_helper[OF order_trans[OF word_and_le1]], simp) 858 apply (simp add: lookup_pt_slot_no_fail_def getPTIndex_def mask_def bit_simps shiftl_t2n) 859 apply (rule ccorres_cond_true) 860 apply (rule_tac P=\<top> and P'=UNIV in ccorres_from_vcg_throws) 861 apply (rule allI, rule conseqPre, vcg) 862 apply (clarsimp simp: throwError_def return_def syscall_error_rel_def) 863 apply (clarsimp simp: EXCEPTION_NONE_def EXCEPTION_LOOKUP_FAULT_def) 864 apply (simp add: lookup_fault_missing_capability_lift mask_def bit_simps) 865 apply vcg 866 apply (rule conseqPre, vcg, clarsimp) 867 apply (ccorres_rewrite, rename_tac lookupPDSlot_errstate) 868 apply (rule_tac P=\<top> and P'="{s. lookupPDSlot_errstate = errstate s}" 869 in ccorres_from_vcg_throws) 870 apply (rule allI, rule conseqPre, vcg, clarsimp simp: throwError_def return_def) 871 apply (clarsimp, wp) 872 apply (vcg exspec=lookupPDSlot_modifies) 873 apply clarsimp 874 apply (frule h_t_valid_clift; simp) 875 apply (strengthen imp_ignore[where A="Ex P" for P]) 876 apply (clarsimp simp: cpde_relation_def isPageTablePDE_def Let_def 877 pde_lift_def pde_pde_pt_lift_def pde_tag_defs 878 split: X64_H.pde.splits if_splits) 879 done 880 881lemma cap_case_isPML4Cap: 882 "(case cap of ArchObjectCap (PML4Cap pm (Some asid)) \<Rightarrow> fn pm asid | _ => g) 883 = (if (if isArchObjectCap cap then if isPML4Cap (capCap cap) then capPML4MappedASID (capCap cap) \<noteq> None else False else False) 884 then fn (capPML4BasePtr (capCap cap)) (the (capPML4MappedASID (capCap cap))) else g)" 885 apply (cases cap; simp add: isArchObjectCap_def) 886 apply (rename_tac arch_capability) 887 apply (case_tac arch_capability, simp_all add: isPML4Cap_def) 888 apply (rename_tac option) 889 apply (case_tac option; simp) 890 done 891 892abbreviation 893 "findVSpaceForASID_xf \<equiv> liftxf errstate findVSpaceForASID_ret_C.status_C findVSpaceForASID_ret_C.vspace_root_C ret__struct_findVSpaceForASID_ret_C_'" 894 895lemma ccorres_pre_getObject_asidpool: 896 assumes cc: "\<And>rv. ccorres r xf (P rv) (P' rv) hs (f rv) c" 897 shows "ccorres r xf 898 (\<lambda>s. (\<forall>asidpool. ko_at' asidpool p s \<longrightarrow> P asidpool s)) 899 {s. \<forall> asidpool asidpool'. cslift s (ap_Ptr p) = Some asidpool' \<and> casid_pool_relation asidpool asidpool' 900 \<longrightarrow> s \<in> P' asidpool} 901 hs (getObject p >>= (\<lambda>rv :: asidpool. f rv)) c" 902 apply (rule ccorres_guard_imp2) 903 apply (rule ccorres_symb_exec_l) 904 apply (rule ccorres_guard_imp2) 905 apply (rule cc) 906 apply (rule conjI) 907 apply (rule_tac Q="ko_at' rv p s" in conjunct1) 908 apply assumption 909 apply assumption 910 apply (wpsimp wp: getASID_wp empty_fail_getObject)+ 911 apply (erule cmap_relationE1 [OF rf_sr_cpspace_asidpool_relation], 912 erule ko_at_projectKO_opt) 913 apply simp 914 done 915 916(* FIXME: move *) 917lemma ccorres_from_vcg_throws_nofail: 918 "\<forall>\<sigma>. \<Gamma>\<turnstile> {s. P \<sigma> \<and> s \<in> P' \<and> (\<sigma>, s) \<in> srel} c {}, 919 {s. \<not>snd (a \<sigma>) \<longrightarrow> (\<exists>(rv, \<sigma>')\<in>fst (a \<sigma>). (\<sigma>', s) \<in> srel \<and> arrel rv (axf s))} \<Longrightarrow> 920 ccorres_underlying srel \<Gamma> r xf arrel axf P P' (SKIP # hs) a c" 921 apply (rule ccorresI') 922 apply (drule_tac x = s in spec) 923 apply (drule hoare_sound) 924 apply (simp add: HoarePartialDef.valid_def cvalid_def) 925 apply (erule exec_handlers.cases) 926 apply clarsimp 927 apply (drule spec, drule spec, drule (1) mp) 928 apply (clarsimp dest!: exec_handlers_SkipD 929 simp: split_def unif_rrel_simps elim!: bexI [rotated]) 930 apply clarsimp 931 apply (drule spec, drule spec, drule (1) mp) 932 apply clarsimp 933 apply simp 934 done 935 936lemma findVSpaceForASID_ccorres: 937 "ccorres 938 (lookup_failure_rel \<currency> (\<lambda>pml4eptrc pml4eptr. pml4eptr = pml4e_Ptr pml4eptrc)) 939 findVSpaceForASID_xf 940 (valid_arch_state' and no_0_obj' and (\<lambda>_. asid_wf asid)) 941 (UNIV \<inter> \<lbrace>\<acute>asid = asid\<rbrace> ) 942 [] 943 (findVSpaceForASID asid) 944 (Call findVSpaceForASID_'proc)" 945 apply (rule ccorres_gen_asm) 946 apply (cinit lift: asid_') 947 apply (rule ccorres_assertE)+ 948 apply (rule ccorres_liftE_Seq) 949 apply (simp add: liftME_def bindE_assoc) 950 apply (rule ccorres_pre_gets_x86KSASIDTable_ksArchState') 951 apply (case_tac "asidTable (ucast (asid_high_bits_of asid))") 952 (* Case where the first look-up fails *) 953 apply clarsimp 954 apply (rule_tac P="valid_arch_state' and _" and P'=UNIV in ccorres_from_vcg_throws) 955 apply (rule allI, rule conseqPre, vcg) 956 apply (clarsimp simp: throwError_def return_def bindE_def NonDetMonad.lift_def 957 EXCEPTION_NONE_def EXCEPTION_LOOKUP_FAULT_def lookup_fault_lift_invalid_root) 958 apply (frule rf_sr_asidTable_None[where asid=asid, THEN iffD2], 959 simp add: asid_wf_def3, assumption, assumption) 960 apply (fastforce simp: asid_map_asid_map_none_def asid_map_asid_map_vspace_def asid_wf_def2 961 Kernel_C.asidLowBits_def asid_shiftr_low_bits_less) 962 (* Case where the first look-up succeeds *) 963 apply clarsimp 964 apply (rule ccorres_liftE_Seq) 965 apply (rule ccorres_guard_imp) 966 apply (rule ccorres_pre_getObject_asidpool) 967 apply (rename_tac asidPool) 968 apply (case_tac "inv ASIDPool asidPool (ucast (asid_low_bits_of asid)) = Some 0") 969 apply (clarsimp simp: ccorres_fail') 970 apply (rule_tac P="\<lambda>s. asidTable=x64KSASIDTable (ksArchState s) \<and> 971 valid_arch_state' s \<and> (asid_wf asid)" 972 and P'="{s'. (\<exists>ap'. cslift s' (ap_Ptr (the (asidTable (ucast (asid_high_bits_of asid))))) 973 = Some ap' \<and> casid_pool_relation asidPool ap')}" 974 in ccorres_from_vcg_throws_nofail) 975 apply (rule allI, rule conseqPre, vcg) 976 apply (clarsimp simp: ucast_asid_high_bits_is_shift asid_wf_def2) 977 apply (frule_tac idx="(asid >> asid_low_bits)" in rf_asidTable, assumption, 978 simp add: leq_asid_bits_shift) 979 apply (clarsimp simp: typ_heap_simps) 980 apply (case_tac asidPool, clarsimp simp: inv_def) 981 apply (simp add: casid_pool_relation_def) 982 apply (case_tac ap', simp) 983 apply (simp add: array_relation_def) 984 apply (erule_tac x="(asid && 2 ^ asid_low_bits - 1)" in allE) 985 apply (simp add: word_and_le1 mask_def option_to_ptr_def option_to_0_def 986 asid_shiftr_low_bits_less asid_low_bits_of_p2m1_eq) 987 apply (rename_tac "fun" array) 988 apply (case_tac "fun (asid && 2 ^ asid_low_bits - 1)", clarsimp) 989 apply (clarsimp simp: throwError_def return_def EXCEPTION_NONE_def EXCEPTION_LOOKUP_FAULT_def) 990 apply (simp add: lookup_fault_lift_invalid_root Kernel_C.asidLowBits_def) 991 apply (rule conjI) 992 apply (simp add: asid_low_bits_def asid_bits_def) 993 apply word_bitwise 994 apply (clarsimp simp: asid_map_relation_def asid_map_lift_def 995 asid_map_asid_map_none_def asid_map_asid_map_vspace_def) 996 apply (clarsimp simp: Kernel_C.asidLowBits_def) 997 apply (rule conjI) 998 apply (simp add: asid_low_bits_def asid_bits_def) 999 apply word_bitwise 1000 apply clarsimp 1001 apply (subgoal_tac "asid_map_get_tag (array.[unat (asid && 2 ^ asid_low_bits - 1)]) = 1002 SCAST(32 signed \<rightarrow> 64) asid_map_asid_map_vspace") 1003 prefer 2 1004 apply (rule classical) 1005 apply (fastforce simp: asid_map_relation_def asid_map_lift_def split: if_splits) 1006 apply (fastforce simp: returnOk_def return_def 1007 checkPML4At_def in_monad stateAssert_def liftE_bindE 1008 get_def bind_def assert_def fail_def 1009 asid_map_relation_def asid_map_lift_def 1010 asid_map_asid_map_none_def asid_map_asid_map_vspace_def 1011 asid_map_asid_map_vspace_lift_def 1012 split: if_splits) 1013 apply (simp add: mask_2pm1)+ 1014 done 1015 1016lemma ccorres_pre_gets_x64KSSKIMPML4_ksArchState: 1017 assumes cc: "\<And>rv. ccorres r xf (P rv) (P' rv) hs (f rv) c" 1018 shows "ccorres r xf 1019 (\<lambda>s. (\<forall>rv. x64KSSKIMPML4 (ksArchState s) = rv \<longrightarrow> P rv s)) 1020 (P' (ptr_val (pml4_Ptr (symbol_table ''x64KSSKIMPML4'')))) 1021 hs (gets (x64KSSKIMPML4 \<circ> ksArchState) >>= (\<lambda>rv. f rv)) c" 1022 apply (rule ccorres_guard_imp) 1023 apply (rule ccorres_symb_exec_l) 1024 defer 1025 apply wp[1] 1026 apply (rule gets_sp) 1027 apply (clarsimp simp: empty_fail_def simpler_gets_def) 1028 apply assumption 1029 apply clarsimp 1030 defer 1031 apply (rule ccorres_guard_imp) 1032 apply (rule cc) 1033 apply clarsimp 1034 apply assumption 1035 apply (drule rf_sr_x64KSSKIMPML4) 1036 apply simp 1037 done 1038 1039(* FIXME move *) 1040lemma ccorres_from_vcg_might_throw: 1041 "(\<forall>\<sigma>. Gamm \<turnstile> {s. P \<sigma> \<and> s \<in> P' \<and> (\<sigma>, s) \<in> sr} c 1042 {s. \<exists>(rv, \<sigma>') \<in> fst (a \<sigma>). (\<sigma>', s) \<in> sr \<and> r rv (xf s)}, 1043 {s. \<exists>(rv, \<sigma>') \<in> fst (a \<sigma>). (\<sigma>', s) \<in> sr \<and> arrel rv (axf s)}) 1044 \<Longrightarrow> ccorres_underlying sr Gamm r xf arrel axf P P' (SKIP # hs) a c" 1045 apply (rule ccorresI') 1046 apply (drule_tac x=s in spec) 1047 apply (erule exec_handlers.cases, simp_all) 1048 apply clarsimp 1049 apply (erule exec_handlers.cases, simp_all)[1] 1050 apply (auto elim!: exec_Normal_elim_cases)[1] 1051 apply (drule(1) exec_abrupt[rotated]) 1052 apply simp 1053 apply (clarsimp simp: unif_rrel_simps elim!: exec_Normal_elim_cases) 1054 apply fastforce 1055 apply (clarsimp simp: unif_rrel_simps) 1056 apply (drule hoare_sound) 1057 apply (clarsimp simp: cvalid_def HoarePartialDef.valid_def) 1058 apply fastforce 1059 done 1060 1061end 1062 1063context begin interpretation Arch . (*FIXME: arch_split*) 1064 1065end 1066 1067context kernel_m begin 1068 1069(* FIXME: move *) 1070lemma ccorres_h_t_valid_x64KSSKIMPML4: 1071 "ccorres r xf P P' hs f (f' ;; g') \<Longrightarrow> 1072 ccorres r xf P P' hs f 1073 (Guard C_Guard {s'. s' \<Turnstile>\<^sub>c pml4_Ptr (symbol_table ''x64KSSKIMPML4'')} f';; g')" 1074 apply (rule ccorres_guard_imp2) 1075 apply (rule ccorres_move_c_guards[where P = \<top>]) 1076 apply clarsimp 1077 apply assumption 1078 apply simp 1079 by (clarsimp simp add: rf_sr_def cstate_relation_def Let_def) 1080 1081lemma ccorres_pre_gets_x64KSCurrentUserCR3_ksArchState: 1082 assumes cc: "\<And>rv. ccorres r xf (P rv) (P' rv) hs (f rv) c" 1083 shows "ccorres r xf 1084 (\<lambda>s. (\<forall>rv. x64KSCurrentUserCR3 (ksArchState s) = rv \<longrightarrow> P rv s)) 1085 {s. \<forall>rv. s \<in> P' rv } 1086 hs (gets (x64KSCurrentUserCR3 \<circ> ksArchState) >>= (\<lambda>rv. f rv)) c" 1087 apply (rule ccorres_guard_imp) 1088 apply (rule ccorres_symb_exec_l) 1089 defer 1090 apply wp[1] 1091 apply (rule gets_sp) 1092 apply (clarsimp simp: empty_fail_def simpler_gets_def) 1093 apply assumption 1094 apply clarsimp 1095 defer 1096 apply (rule ccorres_guard_imp) 1097 apply (rule cc) 1098 apply clarsimp 1099 apply assumption 1100 apply clarsimp 1101 done 1102 1103(* MOVE copied from CSpace_RAB_C *) 1104lemma ccorres_gen_asm_state: 1105 assumes rl: "\<And>s. P s \<Longrightarrow> ccorres r xf G G' hs a c" 1106 shows "ccorres r xf (G and P) G' hs a c" 1107proof (rule ccorres_guard_imp2) 1108 show "ccorres r xf (G and (\<lambda>_. \<exists>s. P s)) G' hs a c" 1109 apply (rule ccorres_gen_asm) 1110 apply (erule exE) 1111 apply (erule rl) 1112 done 1113next 1114 fix s s' 1115 assume "(s, s') \<in> rf_sr" and "(G and P) s" and "s' \<in> G'" 1116 thus "(G and (\<lambda>_. \<exists>s. P s)) s \<and> s' \<in> G'" 1117 by (clarsimp elim!: exI) 1118qed 1119 1120(* FIXME move *) 1121lemma fromIntegral_simp_nat[simp]: "(fromIntegral :: nat \<Rightarrow> nat) = id" 1122 by (simp add: fromIntegral_def fromInteger_nat toInteger_nat) 1123 1124(* FIXME shadows two other identical versions in other files *) 1125lemma ccorres_abstract_known: 1126 "\<lbrakk> \<And>rv' t t'. ceqv \<Gamma> xf' rv' t t' g (g' rv'); ccorres rvr xf P P' hs f (g' val) \<rbrakk> 1127 \<Longrightarrow> ccorres rvr xf P (P' \<inter> {s. xf' s = val}) hs f g" 1128 apply (rule ccorres_guard_imp2) 1129 apply (rule_tac xf'=xf' in ccorres_abstract) 1130 apply assumption 1131 apply (rule_tac P="rv' = val" in ccorres_gen_asm2) 1132 apply simp 1133 apply simp 1134 done 1135 1136lemma setObject_modify: 1137 fixes v :: "'a :: pspace_storable" shows 1138 "\<lbrakk> obj_at' (P :: 'a \<Rightarrow> bool) p s; updateObject v = updateObject_default v; 1139 (1 :: machine_word) < 2 ^ objBits v \<rbrakk> 1140 \<Longrightarrow> setObject p v s 1141 = modify (ksPSpace_update (\<lambda>ps. ps (p \<mapsto> injectKO v))) s" 1142 apply (clarsimp simp: setObject_def split_def exec_gets 1143 obj_at'_def projectKOs lookupAround2_known1 1144 assert_opt_def updateObject_default_def 1145 bind_assoc) 1146 apply (simp add: projectKO_def alignCheck_assert) 1147 apply (simp add: project_inject objBits_def) 1148 apply (clarsimp simp only: objBitsT_koTypeOf[symmetric] koTypeOf_injectKO) 1149 apply (frule(2) in_magnitude_check[where s'=s]) 1150 apply (simp add: magnitudeCheck_assert in_monad) 1151 apply (simp add: simpler_modify_def) 1152 done 1153 1154lemma ccorres_name_pre_C: 1155 "(\<And>s. s \<in> P' \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf P {s} hs f g) 1156 \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf arrel axf P P' hs f g" 1157 apply (rule ccorres_guard_imp) 1158 apply (rule_tac xf'=id in ccorres_abstract, rule ceqv_refl) 1159 apply (rule_tac P="rv' \<in> P'" in ccorres_gen_asm2) 1160 apply assumption 1161 apply simp 1162 apply simp 1163 done 1164 1165lemma kpptr_to_paddr_spec: 1166 "\<forall>s. \<Gamma> \<turnstile> {s} 1167 Call kpptr_to_paddr_'proc 1168 \<lbrace> \<acute>ret__unsigned_long = X64_H.addrFromKPPtr (ptr_val (pptr_' s)) \<rbrace>" 1169 apply vcg 1170 apply (simp add: X64_H.addrFromKPPtr_def X64.addrFromKPPtr_def X64.kpptrBase_def) 1171 done 1172 1173(* A version of ccr3_relation in which the most significant bit is cleared. 1174 This reflects the behaviour of getCurrentUserCR3, which clears that bit. *) 1175definition 1176 ccr3_relation'' :: "machine_word \<Rightarrow> machine_word \<Rightarrow> cr3_C \<Rightarrow> bool" 1177where 1178 "ccr3_relation'' addr pcid ccr3 \<equiv> 1179 let ccr3' = cr3_C.words_C ccr3.[0] in 1180 addr = ccr3' && (mask 39 << 12) 1181 \<and> pcid = ccr3' && mask 12 1182 \<and> ccr3' && (~~ mask 51) = 0" 1183 1184definition 1185 ccr3_relation' :: "X64_H.cr3 \<Rightarrow> cr3_C \<Rightarrow> bool" 1186where 1187 "ccr3_relation' hcr3 \<equiv> case hcr3 of CR3 addr pcid \<Rightarrow> ccr3_relation'' addr pcid" 1188 1189lemmas ccr3_relation_defs = 1190 ccr3_relation_def ccr3_relation'_def ccr3_relation''_def 1191 1192(* The C kernel performs some operations on CR3s as words rather than bitfields. 1193 When we need to reason about the bits that the bitfield-generated specs ignore, 1194 we'll use the following stronger specs for cr3_new and makeCR3. *) 1195lemma cr3_new_spec': 1196 "\<forall>s. \<Gamma> \<turnstile> {s} Call cr3_new_'proc 1197 {t. globals t = globals s \<and> ccr3_relation'' 1198 (pml4_base_address_' s && (mask 39 << 12)) 1199 (pcid_' s && mask 12) 1200 (ret__struct_cr3_C_' t) }" 1201 apply (hoare_rule HoarePartial.ProcNoRec1) 1202 apply (rule allI, rule conseqPre, vcg) 1203 apply (clarsimp simp: mask_def ccr3_relation''_def Let_def word_ao_dist word_bw_assocs) 1204 done 1205 1206lemma makeCR3_spec: 1207 "\<forall>s. \<Gamma> \<turnstile> {s} Call makeCR3_'proc 1208 {t. globals t = globals s \<and> ccr3_relation'' 1209 (addr_' s && (mask 39 << 12)) 1210 (pcid___unsigned_long_' s && mask 12) 1211 (ret__struct_cr3_C_' t) }" 1212 apply (rule allI, rule conseqPre, vcg exspec=cr3_new_spec') 1213 apply clarsimp 1214 done 1215 1216lemma getCurrentUserCR3_ccorres: 1217 "ccorres ccr3_relation' ret__struct_cr3_C_' \<top> UNIV hs 1218 getCurrentUserCR3 (Call getCurrentUserCR3_'proc)" 1219 apply (rule ccorres_from_vcg, rule allI, rule conseqPre, vcg) 1220 apply (clarsimp simp: gets_def get_def return_def bind_def getCurrentUserCR3_def) 1221 apply (clarsimp simp: ccr3_relation_defs Let_def cr3_lift_def 1222 rf_sr_def cstate_relation_def carch_state_relation_def 1223 split: X64_H.cr3.splits) 1224 apply (drule_tac x="x64KSCurrentUserCR3_' (globals x) && ~~ mask 51" 1225 and f="\<lambda>x. x && mask 63" in arg_cong) 1226 apply (simp add: mask_def word_bw_assocs word_ao_dist) 1227 done 1228 1229lemma setCurrentUserCR3_ccorres: 1230 "ccorres dc xfdc 1231 \<top> (UNIV \<inter> \<lbrace>ccr3_relation'' addr asid \<acute>cr3\<rbrace>) 1232 hs 1233 (setCurrentUserCR3 (CR3 addr asid)) 1234 (Call setCurrentUserCR3_'proc)" 1235 (is "ccorres _ _ _ (UNIV \<inter> ?P') _ _ _") 1236 apply cinit 1237 apply (rule ccorres_from_vcg[where P=\<top> and P'="?P'"]) 1238 apply (rule allI, rule conseqPre, vcg) 1239 apply (clarsimp simp: modify_def bind_def get_def put_def) 1240 apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def) 1241 apply (clarsimp simp: carch_state_relation_def carch_globals_def cmachine_state_relation_def) 1242 apply (clarsimp simp: ccr3_relation_defs Let_def word_ao_dist mask_def) 1243 apply simp 1244 done 1245 1246lemma setCurrentUserVSpaceRoot_ccorres: 1247 "ccorres dc xfdc (K (asid_wf asid)) (UNIV \<inter> \<lbrace>\<acute>addr = addr\<rbrace> \<inter> \<lbrace>\<acute>pcid___unsigned_long = asid\<rbrace>) hs 1248 (setCurrentUserVSpaceRoot addr asid) 1249 (Call setCurrentUserVSpaceRoot_'proc)" 1250 apply cinit 1251 apply (simp add: makeCR3_def) 1252 apply (rule ccorres_symb_exec_r) 1253 apply (ctac add: setCurrentUserCR3_ccorres) 1254 apply vcg 1255 apply (rule conseqPre, vcg) 1256 apply clarsimp 1257 apply (simp add: asid_wf_def, drule less_mask_eq) 1258 apply (clarsimp simp: ccr3_relation_defs Let_def mask_def bit_simps asid_bits_def) 1259 done 1260 1261(* FIXME: move *) 1262lemma invs_cicd_valid_objs' [elim!]: 1263 "all_invs_but_ct_idle_or_in_cur_domain' s \<Longrightarrow> valid_objs' s" 1264 by (simp add: all_invs_but_ct_idle_or_in_cur_domain'_def valid_pspace'_def) 1265 1266lemma setVMRoot_ccorres: 1267 "ccorres dc xfdc 1268 (all_invs_but_ct_idle_or_in_cur_domain' and tcb_at' thread) 1269 (UNIV \<inter> {s. tcb_' s = tcb_ptr_to_ctcb_ptr thread}) hs 1270 (setVMRoot thread) (Call setVMRoot_'proc)" 1271 supply Collect_const[simp del] 1272 apply (cinit lift: tcb_') 1273 apply (rule ccorres_move_array_assertion_tcb_ctes) 1274 apply (rule ccorres_move_c_guard_tcb_ctes) 1275 apply (simp add: getThreadVSpaceRoot_def locateSlot_conv cap_case_isPML4Cap 1276 makeCR3_def bit_simps asid_bits_def) 1277 apply (ctac, rename_tac vRootCap vRootCap') 1278 apply (csymbr, rename_tac vRootTag) 1279 apply csymbr 1280 apply (simp add: cap_get_tag_isCap_ArchObject2) 1281 apply (rule ccorres_Cond_rhs_Seq) 1282 apply (simp add: throwError_def catch_def dc_def[symmetric]) 1283 apply (rule ccorres_cond_true_seq, ccorres_rewrite) 1284 apply (rule ccorres_rhs_assoc) 1285 apply (rule ccorres_h_t_valid_x64KSSKIMPML4) 1286 apply csymbr 1287 apply (rule ccorres_pre_gets_x64KSSKIMPML4_ksArchState[unfolded comp_def]) 1288 apply (rule ccorres_add_return2) 1289 apply (ctac (no_vcg) add: setCurrentUserVSpaceRoot_ccorres) 1290 apply (rule ccorres_return_void_C) 1291 apply (rule hoare_post_taut[where P=\<top>]) 1292 apply (rule ccorres_rhs_assoc) 1293 apply (csymbr, rename_tac is_mapped) 1294 apply csymbr 1295 apply (rule_tac P="to_bool (capPML4IsMapped_CL (cap_pml4_cap_lift vRootCap')) 1296 = (capPML4MappedASID (capCap vRootCap) \<noteq> None)" 1297 in ccorres_gen_asm2) 1298 apply (clarsimp simp: to_bool_def dc_def[symmetric]) 1299 apply (rule ccorres_Cond_rhs_Seq) 1300 apply (simp add: throwError_def catch_def dc_def[symmetric], ccorres_rewrite) 1301 apply (rule ccorres_rhs_assoc) 1302 apply (rule ccorres_h_t_valid_x64KSSKIMPML4) 1303 apply csymbr 1304 apply (rule ccorres_pre_gets_x64KSSKIMPML4_ksArchState[unfolded comp_def]) 1305 apply (rule ccorres_add_return2) 1306 apply (ctac (no_vcg) add: setCurrentUserVSpaceRoot_ccorres) 1307 apply (rule ccorres_return_void_C) 1308 apply (rule hoare_post_taut[where P=\<top>]) 1309 apply (simp add: catch_def bindE_bind_linearise bind_assoc liftE_def) 1310 apply (csymbr, rename_tac pml4_ptr, csymbr) 1311 apply (csymbr, rename_tac asid', csymbr) 1312 apply (rule_tac f'=lookup_failure_rel 1313 and r'="\<lambda>pml4_ptr pml4_ptr'. pml4_ptr' = pml4e_Ptr pml4_ptr" 1314 and xf'=find_ret_' 1315 in ccorres_split_nothrow_case_sum) 1316 apply (ctac add: findVSpaceForASID_ccorres) 1317 apply ceqv 1318 apply (rename_tac vspace vspace') 1319 apply (rule_tac P="capPML4BasePtr_CL (cap_pml4_cap_lift vRootCap') 1320 = capPML4BasePtr (capCap vRootCap)" 1321 in ccorres_gen_asm2) 1322 apply simp 1323 apply (rule ccorres_Cond_rhs_Seq) 1324 apply (simp add: whenE_def throwError_def dc_def[symmetric], ccorres_rewrite) 1325 apply (rule ccorres_rhs_assoc) 1326 apply (rule ccorres_h_t_valid_x64KSSKIMPML4) 1327 apply csymbr 1328 apply (rule ccorres_pre_gets_x64KSSKIMPML4_ksArchState[unfolded comp_def]) 1329 apply (rule ccorres_add_return2) 1330 apply (ctac (no_vcg) add: setCurrentUserVSpaceRoot_ccorres) 1331 apply (rule ccorres_return_void_C) 1332 apply (rule hoare_post_taut[where P=\<top>]) 1333 apply (simp add: whenE_def returnOk_def) 1334 apply (csymbr, rename_tac base_addr) 1335 apply (rule ccorres_symb_exec_r) 1336 apply (ctac add: getCurrentUserCR3_ccorres, rename_tac currentCR3 currentCR3') 1337 apply (rule ccorres_if_bind, rule ccorres_if_lhs; simp add: dc_def[symmetric]) 1338 apply (rule ccorres_cond_true) 1339 apply (ctac add: setCurrentUserCR3_ccorres) 1340 apply (rule ccorres_cond_false) 1341 apply (rule ccorres_return_Skip) 1342 apply (simp, rule hoare_post_taut[where P=\<top>]) 1343 apply vcg 1344 apply vcg 1345 apply (rule conseqPre, vcg, clarsimp) 1346 apply (rule ccorres_cond_true_seq, simp add: dc_def[symmetric], ccorres_rewrite) 1347 apply (rule ccorres_rhs_assoc) 1348 apply (rule ccorres_h_t_valid_x64KSSKIMPML4) 1349 apply csymbr 1350 apply (rule ccorres_pre_gets_x64KSSKIMPML4_ksArchState[unfolded comp_def]) 1351 apply (rule ccorres_add_return2) 1352 apply (ctac (no_vcg) add: setCurrentUserVSpaceRoot_ccorres) 1353 apply (rule ccorres_return_void_C) 1354 apply (rule hoare_post_taut[where P=\<top>]) 1355 apply (simp add: asid_wf_0, rule wp_post_tautE) 1356 apply (vcg exspec=findVSpaceForASID_modifies) 1357 apply (wpsimp wp: getSlotCap_wp) 1358 apply vcg 1359 apply (clarsimp simp: Collect_const_mem) 1360 apply (rule conjI) 1361 apply (frule cte_at_tcb_at_32', drule cte_at_cte_wp_atD) 1362 apply (clarsimp simp: cte_level_bits_def tcbVTableSlot_def) 1363 apply (rule_tac x="cteCap cte" in exI) 1364 apply (rule conjI, erule cte_wp_at_weakenE', simp) 1365 apply (clarsimp simp: invs_cicd_no_0_obj' invs_cicd_arch_state') 1366 apply (frule cte_wp_at_valid_objs_valid_cap'; clarsimp simp: invs_cicd_valid_objs') 1367 apply (clarsimp simp: isCap_simps valid_cap'_def mask_def asid_wf_def) 1368 apply (clarsimp simp: tcb_cnode_index_defs cte_level_bits_def tcbVTableSlot_def 1369 cte_at_tcb_at_32' to_bool_def) 1370 apply (clarsimp simp: cap_get_tag_isCap_ArchObject2 1371 dest!: isCapDs) 1372 apply (clarsimp simp: cap_get_tag_isCap_ArchObject[symmetric] 1373 cap_lift_pml4_cap cap_to_H_def 1374 cap_pml4_cap_lift_def 1375 to_bool_def mask_def 1376 ccr3_relation_defs Let_def 1377 cr3_lift_def word_bw_assocs 1378 elim!: ccap_relationE 1379 split: if_split_asm X64_H.cr3.splits) 1380 apply (rename_tac t t') 1381 apply (rule conjI; clarsimp) 1382 apply (drule_tac t="cr3_C.words_C (ret__struct_cr3_C_' t').[0]" in sym) 1383 apply (simp add: word_bw_assocs) 1384 apply (frule (1) word_combine_masks[where m="0x7FFFFFFFFF000" and m'="0xFFF"]; simp add: word_ao_dist2[symmetric]) 1385 apply (frule (1) word_combine_masks[where m="0x7FFFFFFFFFFFF" and m'="0x7FF8000000000000"]; simp) 1386 apply (match premises in H: \<open>cr3_C.words_C _.[0] && _ = 0\<close> \<Rightarrow> \<open>insert H; word_bitwise\<close>) 1387 done 1388 1389(* FIXME: remove *) 1390lemmas invs'_invs_no_cicd = invs_invs_no_cicd' 1391 1392lemma ccorres_seq_IF_False: 1393 "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)" 1394 by simp 1395 1396(* FIXME x64: needed? *) 1397lemma ptrFromPAddr_mask6_simp[simp]: 1398 "ptrFromPAddr ps && mask 6 = ps && mask 6" 1399 unfolding ptrFromPAddr_def X64.pptrBase_def 1400 by (subst add.commute, subst mask_add_aligned ; simp add: is_aligned_def) 1401 1402(* FIXME: move *) 1403lemma register_from_H_bound[simp]: 1404 "unat (register_from_H v) < 23" 1405 by (cases v, simp_all add: "StrictC'_register_defs") 1406 1407(* FIXME: move *) 1408lemma register_from_H_inj: 1409 "inj register_from_H" 1410 apply (rule inj_onI) 1411 apply (case_tac x) 1412 by (case_tac y, simp_all add: "StrictC'_register_defs")+ 1413 1414(* FIXME: move *) 1415lemmas register_from_H_eq_iff[simp] 1416 = inj_on_eq_iff [OF register_from_H_inj, simplified] 1417 1418lemma setRegister_ccorres: 1419 "ccorres dc xfdc \<top> 1420 (UNIV \<inter> \<lbrace>\<acute>thread = tcb_ptr_to_ctcb_ptr thread\<rbrace> \<inter> \<lbrace>\<acute>reg = register_from_H reg\<rbrace> 1421 \<inter> {s. w_' s = val}) [] 1422 (asUser thread (setRegister reg val)) 1423 (Call setRegister_'proc)" 1424 apply (cinit' lift: thread_' reg_' w_') 1425 apply (simp add: asUser_def dc_def[symmetric] split_def split del: if_split) 1426 apply (rule ccorres_pre_threadGet) 1427 apply (rule ccorres_Guard) 1428 apply (simp add: setRegister_def simpler_modify_def exec_select_f_singleton) 1429 apply (rule_tac P="\<lambda>tcb. (atcbContextGet o tcbArch) tcb = rv" 1430 in threadSet_ccorres_lemma2 [unfolded dc_def]) 1431 apply vcg 1432 apply (clarsimp simp: setRegister_def HaskellLib_H.runState_def 1433 simpler_modify_def typ_heap_simps) 1434 apply (subst StateSpace.state.fold_congs[OF refl refl]) 1435 apply (rule globals.fold_congs[OF refl refl]) 1436 apply (rule heap_update_field_hrs, simp) 1437 apply (fastforce intro: typ_heap_simps) 1438 apply simp 1439 apply (erule(1) rf_sr_tcb_update_no_queue2, 1440 (simp add: typ_heap_simps')+) 1441 apply (rule ball_tcb_cte_casesI, simp+) 1442 apply (clarsimp simp: ctcb_relation_def ccontext_relation_def cregs_relation_def 1443 atcbContextSet_def atcbContextGet_def 1444 carch_tcb_relation_def 1445 split: if_split) 1446 apply (clarsimp simp: Collect_const_mem register_from_H_sless 1447 register_from_H_less) 1448 apply (auto intro: typ_heap_simps elim: obj_at'_weakenE) 1449 done 1450 1451lemma msgRegisters_ccorres: 1452 "n < unat n_msgRegisters \<Longrightarrow> 1453 register_from_H (X64_H.msgRegisters ! n) = (index kernel_all_substitute.msgRegisters n)" 1454 apply (simp add: kernel_all_substitute.msgRegisters_def msgRegisters_unfold fupdate_def) 1455 apply (simp add: Arrays.update_def n_msgRegisters_def fcp_beta nth_Cons' split: if_split) 1456 done 1457 1458(* usually when we call setMR directly, we mean to only set a registers, which will 1459 fit in actual registers *) 1460lemma setMR_as_setRegister_ccorres: 1461 notes dc_simp[simp del] 1462 shows 1463 "ccorres (\<lambda>rv rv'. rv' = of_nat offset + 1) ret__unsigned_' 1464 (tcb_at' thread and K (TCB_H.msgRegisters ! offset = reg \<and> offset < length msgRegisters)) 1465 (UNIV \<inter> \<lbrace>\<acute>reg___unsigned_long = val\<rbrace> 1466 \<inter> \<lbrace>\<acute>offset = of_nat offset\<rbrace> 1467 \<inter> \<lbrace>\<acute>receiver = tcb_ptr_to_ctcb_ptr thread\<rbrace>) hs 1468 (asUser thread (setRegister reg val)) 1469 (Call setMR_'proc)" 1470 apply (rule ccorres_grab_asm) 1471 apply (cinit' lift: reg___unsigned_long_' offset_' receiver_') 1472 apply (clarsimp simp: n_msgRegisters_def length_of_msgRegisters) 1473 apply (rule ccorres_cond_false) 1474 apply (rule ccorres_move_const_guards) 1475 apply (rule ccorres_add_return2) 1476 apply (ctac add: setRegister_ccorres) 1477 apply (rule ccorres_from_vcg_throws[where P'=UNIV and P=\<top>]) 1478 apply (rule allI, rule conseqPre, vcg) 1479 apply (clarsimp simp: dc_def return_def) 1480 apply (rule hoare_post_taut[of \<top>]) 1481 apply (vcg exspec=setRegister_modifies) 1482 apply (clarsimp simp: n_msgRegisters_def length_of_msgRegisters not_le conj_commute) 1483 apply (subst msgRegisters_ccorres[symmetric]) 1484 apply (clarsimp simp: n_msgRegisters_def length_of_msgRegisters unat_of_nat_eq) 1485 apply (clarsimp simp: word_less_nat_alt word_le_nat_alt unat_of_nat_eq not_le[symmetric]) 1486 done 1487 1488lemma wordFromMessageInfo_spec: 1489 defines "mil s \<equiv> seL4_MessageInfo_lift (mi_' s)" 1490 shows "\<forall>s. \<Gamma> \<turnstile> {s} Call wordFromMessageInfo_'proc 1491 \<lbrace>\<acute>ret__unsigned_long = (label_CL (mil s) << 12) 1492 || (capsUnwrapped_CL (mil s) << 9) 1493 || (extraCaps_CL (mil s) << 7) 1494 || length_CL (mil s)\<rbrace>" 1495 unfolding mil_def 1496 apply vcg 1497 apply (simp add: seL4_MessageInfo_lift_def mask_shift_simps) 1498 apply word_bitwise 1499 done 1500 1501lemma wordFromMessageInfo_ccorres [corres]: 1502 "ccorres (=) ret__unsigned_long_' 1503 \<top> {s. mi = message_info_to_H (mi_' s)} [] 1504 (return (wordFromMessageInfo mi)) (Call wordFromMessageInfo_'proc)" 1505 apply (rule ccorres_from_spec_modifies [where P = \<top>, simplified]) 1506 apply (rule wordFromMessageInfo_spec) 1507 apply (rule wordFromMessageInfo_modifies) 1508 apply simp 1509 apply clarsimp 1510 apply (simp add: return_def wordFromMessageInfo_def Let_def message_info_to_H_def 1511 msgLengthBits_def msgExtraCapBits_def 1512 msgMaxExtraCaps_def shiftL_nat word_bw_assocs word_bw_comms word_bw_lcs) 1513 done 1514 1515(* FIXME move *) 1516lemma register_from_H_eq: 1517 "(r = r') = (register_from_H r = register_from_H r')" 1518 apply (case_tac r, simp_all add: C_register_defs) 1519 by (case_tac r', simp_all add: C_register_defs)+ 1520 1521lemma setMessageInfo_ccorres: 1522 "ccorres dc xfdc (tcb_at' thread) 1523 (UNIV \<inter> \<lbrace>mi = message_info_to_H mi'\<rbrace>) hs 1524 (setMessageInfo thread mi) 1525 (\<acute>ret__unsigned_long :== CALL wordFromMessageInfo(mi');; 1526 CALL setRegister(tcb_ptr_to_ctcb_ptr thread, 1527 scast Kernel_C.msgInfoRegister, 1528 \<acute>ret__unsigned_long))" 1529 unfolding setMessageInfo_def 1530 apply (rule ccorres_guard_imp2) 1531 apply ctac 1532 apply simp 1533 apply (ctac add: setRegister_ccorres) 1534 apply wp 1535 apply vcg 1536 apply (simp add: X64_H.msgInfoRegister_def X64.msgInfoRegister_def 1537 Kernel_C.msgInfoRegister_def Kernel_C.RSI_def) 1538 done 1539 1540lemma performPageGetAddress_ccorres: 1541 "ccorres (K (K \<bottom>) \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') 1542 \<top> 1543 (UNIV \<inter> {s. vbase_ptr_' s = Ptr ptr}) [] 1544 (liftE (performPageInvocation (PageGetAddr ptr))) 1545 (Call performPageGetAddress_'proc)" 1546 apply (simp only: liftE_liftM ccorres_liftM_simp) 1547 apply (cinit lift: vbase_ptr_') 1548 apply csymbr 1549 apply (rule ccorres_pre_getCurThread) 1550 apply (clarsimp simp: setMRs_def zipWithM_x_mapM_x mapM_x_Nil length_of_msgRegisters 1551 zip_singleton msgRegisters_unfold mapM_x_singleton) 1552 apply (ctac add: setRegister_ccorres) 1553 apply csymbr 1554 apply (rule ccorres_add_return2) 1555 apply (rule ccorres_rhs_assoc2) 1556 apply (rule ccorres_split_nothrow_novcg[where r'=dc and xf'=xfdc]) 1557 apply (unfold setMessageInfo_def) 1558 apply ctac 1559 apply (simp only: fun_app_def) 1560 apply (ctac add: setRegister_ccorres) 1561 apply wp 1562 apply vcg 1563 apply ceqv 1564 apply (rule_tac P=\<top> and P'=UNIV in ccorres_from_vcg_throws) 1565 apply (rule allI, rule conseqPre, vcg) 1566 apply (clarsimp simp: return_def) 1567 apply wp 1568 apply (simp add: guard_is_UNIV_def) 1569 apply wp 1570 apply vcg 1571 apply (auto simp: X64_H.fromPAddr_def message_info_to_H_def mask_def X64_H.msgInfoRegister_def 1572 X64.msgInfoRegister_def Kernel_C.msgInfoRegister_def Kernel_C.RSI_def 1573 word_sle_def word_sless_def Kernel_C.RDI_def 1574 kernel_all_global_addresses.msgRegisters_def fupdate_def) 1575 done 1576 1577lemma ignoreFailure_liftM: 1578 "ignoreFailure = liftM (\<lambda>v. ())" 1579 apply (rule ext)+ 1580 apply (simp add: ignoreFailure_def liftM_def 1581 catch_def) 1582 apply (rule bind_apply_cong[OF refl]) 1583 apply (simp split: sum.split) 1584 done 1585 1586lemma ccorres_pre_getObject_pte: 1587 assumes cc: "\<And>rv. ccorres r xf (P rv) (P' rv) hs (f rv) c" 1588 shows "ccorres r xf 1589 (\<lambda>s. (\<forall>pte. ko_at' pte p s \<longrightarrow> P pte s)) 1590 {s. \<forall>pte pte'. cslift s (pte_Ptr p) = Some pte' \<and> cpte_relation pte pte' 1591 \<longrightarrow> s \<in> P' pte} 1592 hs (getObject p >>= (\<lambda>rv. f rv)) c" 1593 apply (rule ccorres_guard_imp2) 1594 apply (rule ccorres_symb_exec_l) 1595 apply (rule ccorres_guard_imp2) 1596 apply (rule cc) 1597 apply (rule conjI) 1598 apply (rule_tac Q="ko_at' rv p s" in conjunct1) 1599 apply assumption 1600 apply assumption 1601 apply (wp getPTE_wp empty_fail_getObject | simp)+ 1602 apply clarsimp 1603 apply (erule cmap_relationE1 [OF rf_sr_cpte_relation], 1604 erule ko_at_projectKO_opt) 1605 apply simp 1606 done 1607 1608lemmas unfold_checkMapping_return 1609 = from_bool_0[where 'a=machine_word_len, folded exception_defs] 1610 to_bool_def 1611 1612lemma checkMappingPPtr_pte_ccorres: 1613 assumes pre: 1614 "\<And>pte \<sigma>. \<Gamma> \<turnstile> {s. True \<and> (\<exists>pte'. cslift s (pte_Ptr pte_ptr) = Some pte' \<and> cpte_relation pte pte') 1615 \<and> (\<sigma>, s) \<in> rf_sr} 1616 call1 ;; Cond S return_void_C Skip 1617 {s. (\<sigma>, s) \<in> rf_sr \<and> (isSmallPagePTE pte) \<and> pteFrame pte = addrFromPPtr pptr}, 1618 {s. (\<sigma>, s) \<in> rf_sr \<and> \<not> ((isSmallPagePTE pte) \<and> pteFrame pte = addrFromPPtr pptr)}" 1619 shows 1620 "ccorres_underlying rf_sr \<Gamma> (inr_rrel dc) xfdc (inl_rrel dc) xfdc 1621 \<top> UNIV [SKIP] 1622 (doE 1623 pte \<leftarrow> withoutFailure $ getObject pte_ptr; 1624 checkMappingPPtr pptr (VMPTE pte) 1625 odE) 1626 (call1;; Cond S return_void_C Skip)" 1627 apply (simp add: checkMappingPPtr_def liftE_bindE) 1628 apply (rule ccorres_symb_exec_l[where Q'="\<lambda>_. UNIV", OF _ _ getObject_ko_at, simplified]) 1629 apply (rule stronger_ccorres_guard_imp) 1630 apply (rule ccorres_from_vcg_might_throw[where P=\<top>]) 1631 apply (rule allI) 1632 apply (rule conseqPost, rule conseqPre, rule_tac \<sigma>1=\<sigma> and pte1=rv in pre) 1633 apply clarsimp 1634 apply (erule CollectE, assumption) 1635 apply (fold_subgoals (prefix))[2] 1636 subgoal by (auto simp: in_monad Bex_def isSmallPagePTE_def 1637 split: pte.split vmpage_size.split) 1638 apply (wp empty_fail_getObject | simp)+ 1639 apply (erule cmap_relationE1[OF rf_sr_cpte_relation]) 1640 apply (erule ko_at_projectKO_opt) 1641 apply simp 1642 apply (wp empty_fail_getObject | simp add: objBits_simps archObjSize_def bit_simps)+ 1643 done 1644 1645lemma checkMappingPPtr_pde_ccorres: 1646 assumes pre: 1647 "\<And>pde \<sigma>. \<Gamma> \<turnstile> {s. True \<and> (\<exists>pde'. cslift s (pde_Ptr pde_ptr) = Some pde' \<and> cpde_relation pde pde') 1648 \<and> (\<sigma>, s) \<in> rf_sr} 1649 call1;; Cond S return_void_C Skip 1650 {s. (\<sigma>, s) \<in> rf_sr \<and> (isLargePagePDE pde) \<and> pdeFrame pde = addrFromPPtr pptr}, 1651 {s. (\<sigma>, s) \<in> rf_sr \<and> \<not> ((isLargePagePDE pde) \<and> pdeFrame pde = addrFromPPtr pptr)}" 1652 shows 1653 "ccorres_underlying rf_sr \<Gamma> (inr_rrel dc) xfdc (inl_rrel dc) xfdc 1654 \<top> UNIV [SKIP] 1655 (doE 1656 pde \<leftarrow> withoutFailure $ getObject pde_ptr; 1657 checkMappingPPtr pptr (VMPDE pde) 1658 odE) 1659 (call1;; Cond S return_void_C Skip)" 1660 apply (simp add: checkMappingPPtr_def liftE_bindE) 1661 apply (rule ccorres_symb_exec_l[where Q'="\<lambda>_. UNIV", OF _ _ getObject_ko_at, simplified]) 1662 apply (rule stronger_ccorres_guard_imp) 1663 apply (rule ccorres_from_vcg_might_throw[where P=\<top>]) 1664 apply (rule allI) 1665 apply (rule conseqPost, rule conseqPre, rule_tac \<sigma>1=\<sigma> and pde1=rv in pre) 1666 apply clarsimp 1667 apply (erule CollectE, assumption) 1668 apply (fold_subgoals (prefix))[2] 1669 subgoal by (auto simp: in_monad Bex_def isLargePagePDE_def 1670 split: pde.split vmpage_size.split) 1671 apply (wp empty_fail_getObject | simp)+ 1672 apply (erule cmap_relationE1[OF rf_sr_cpde_relation]) 1673 apply (erule ko_at_projectKO_opt) 1674 apply simp 1675 apply (wp empty_fail_getObject | simp add: objBits_simps archObjSize_def bit_simps)+ 1676 done 1677 1678lemma checkMappingPPtr_pdpte_ccorres: 1679 assumes pre: 1680 "\<And>pdpte \<sigma>. \<Gamma> \<turnstile> {s. True \<and> (\<exists>pdpte'. cslift s (pdpte_Ptr pdpte_ptr) = Some pdpte' \<and> cpdpte_relation pdpte pdpte') 1681 \<and> (\<sigma>, s) \<in> rf_sr} 1682 call1;; 1683 Cond S (return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 64) false)) Skip 1684 {s. (\<sigma>, s) \<in> rf_sr \<and> (isHugePagePDPTE pdpte) \<and> pdpteFrame pdpte = addrFromPPtr pptr}, 1685 {s. (\<sigma>, s) \<in> rf_sr \<and> \<not> ((isHugePagePDPTE pdpte) \<and> pdpteFrame pdpte = addrFromPPtr pptr) 1686 \<and> ret__unsigned_long_' s = scast false }" 1687 shows 1688 "ccorres_underlying rf_sr \<Gamma> 1689 (inr_rrel dc) xfdc 1690 (inl_rrel (\<lambda>rv rv'. rv' = scast false)) ret__unsigned_long_' 1691 \<top> UNIV (SKIP # hs) 1692 (doE 1693 pdpte \<leftarrow> liftE (getObject pdpte_ptr); 1694 checkMappingPPtr pptr (VMPDPTE pdpte) 1695 odE) 1696 (call1;; 1697 Cond S (return_C ret__unsigned_long_'_update (\<lambda>s. SCAST(32 signed \<rightarrow> 64) false)) Skip)" 1698 apply (simp add: checkMappingPPtr_def liftE_bindE) 1699 apply (rule ccorres_symb_exec_l[where Q'="\<lambda>_. UNIV", OF _ _ getObject_ko_at, simplified]) 1700 apply (rule stronger_ccorres_guard_imp) 1701 apply (rule ccorres_from_vcg_might_throw[where P=\<top>]) 1702 apply (rule allI) 1703 apply (rule conseqPost, rule conseqPre, rule_tac \<sigma>1=\<sigma> and pdpte1=rv in pre) 1704 apply clarsimp 1705 apply (erule CollectE, assumption) 1706 apply (clarsimp split: pdpte.split_asm 1707 simp: isHugePagePDPTE_def throwError_def returnOk_def return_def 1708 EXCEPTION_NONE_def EXCEPTION_LOOKUP_FAULT_def 1709 lookup_fault_lift_invalid_root)+ 1710 apply (erule cmap_relationE1[OF rf_sr_cpdpte_relation]) 1711 apply (erule ko_at_projectKO_opt) 1712 apply simp 1713 apply (wp empty_fail_getObject | simp add: objBits_simps archObjSize_def bit_simps)+ 1714 done 1715 1716lemma ccorres_return_void_C': 1717 "ccorres_underlying rf_sr \<Gamma> (inr_rrel dc) xfdc (inl_rrel dc) xfdc (\<lambda>_. True) UNIV (SKIP # hs) (return (Inl rv)) return_void_C" 1718 apply (rule ccorres_from_vcg_throws) 1719 apply (simp add: return_def) 1720 apply (rule allI, rule conseqPre, vcg) 1721 apply auto 1722 done 1723 1724lemma makeUserPTEInvalid_spec: 1725 "\<forall>s. \<Gamma> \<turnstile> {s} 1726 \<acute>ret__struct_pte_C :== PROC makeUserPTEInvalid() 1727 \<lbrace> pte_lift \<acute>ret__struct_pte_C = \<lparr> 1728 pte_CL.xd_CL = 0, pte_CL.page_base_address_CL = 0, 1729 pte_CL.global_CL = 0, pte_CL.pat_CL = 0, 1730 pte_CL.dirty_CL = 0, pte_CL.accessed_CL = 0, 1731 pte_CL.cache_disabled_CL = 0, pte_CL.write_through_CL = 0, 1732 pte_CL.super_user_CL = 0, pte_CL.read_write_CL = 0, 1733 pte_CL.present_CL = 0 \<rparr> \<rbrace>" 1734 apply vcg 1735 apply (clarsimp simp: makeUserPTEInvalid_body_def makeUserPTEInvalid_impl 1736 pte_lift_def Let_def) 1737 done 1738 1739lemma makeUserPDEInvalid_spec: 1740 "\<forall>s. \<Gamma> \<turnstile> {s} 1741 \<acute>ret__struct_pde_C :== PROC makeUserPDEInvalid() 1742 \<lbrace> pde_lift \<acute>ret__struct_pde_C = Some (Pde_pde_pt \<lparr> 1743 pde_pde_pt_CL.xd_CL = 0, 1744 pde_pde_pt_CL.pt_base_address_CL = 0, 1745 pde_pde_pt_CL.accessed_CL = 0, 1746 pde_pde_pt_CL.cache_disabled_CL = 0, 1747 pde_pde_pt_CL.write_through_CL = 0, 1748 pde_pde_pt_CL.super_user_CL = 0, 1749 pde_pde_pt_CL.read_write_CL = 0, 1750 pde_pde_pt_CL.present_CL = 0 \<rparr>) \<rbrace>" 1751 apply vcg 1752 apply (clarsimp simp: makeUserPDEInvalid_body_def makeUserPDEInvalid_impl 1753 pde_lift_def Let_def pde_get_tag_def pde_tag_defs pde_pde_pt_lift_def) 1754 done 1755 1756lemma makeUserPDPTEInvalid_spec: 1757 "\<forall>s. \<Gamma> \<turnstile> {s} 1758 \<acute>ret__struct_pdpte_C :== PROC makeUserPDPTEInvalid() 1759 \<lbrace> pdpte_lift \<acute>ret__struct_pdpte_C = Some (Pdpte_pdpte_pd \<lparr> 1760 pdpte_pdpte_pd_CL.xd_CL = 0, 1761 pdpte_pdpte_pd_CL.pd_base_address_CL = 0, 1762 pdpte_pdpte_pd_CL.accessed_CL = 0, 1763 pdpte_pdpte_pd_CL.cache_disabled_CL = 0, 1764 pdpte_pdpte_pd_CL.write_through_CL = 0, 1765 pdpte_pdpte_pd_CL.super_user_CL = 0, 1766 pdpte_pdpte_pd_CL.read_write_CL = 0, 1767 pdpte_pdpte_pd_CL.present_CL = 0 \<rparr>) \<rbrace>" 1768 apply vcg 1769 apply (clarsimp simp: makeUserPDPTEInvalid_body_def makeUserPDPTEInvalid_impl 1770 pdpte_lift_def Let_def pdpte_get_tag_def pdpte_tag_defs 1771 pdpte_pdpte_pd_lift_def) 1772 done 1773 1774lemma makeUserPML4EInvalid_spec: 1775 "\<forall>s. \<Gamma> \<turnstile> {s} 1776 \<acute>ret__struct_pml4e_C :== PROC makeUserPML4EInvalid() 1777 \<lbrace> pml4e_lift \<acute>ret__struct_pml4e_C = \<lparr> 1778 pml4e_CL.xd_CL = 0, 1779 pml4e_CL.pdpt_base_address_CL = 0, 1780 pml4e_CL.accessed_CL = 0, 1781 pml4e_CL.cache_disabled_CL = 0, 1782 pml4e_CL.write_through_CL = 0, 1783 pml4e_CL.super_user_CL = 0, 1784 pml4e_CL.read_write_CL = 0, 1785 pml4e_CL.present_CL = 0 \<rparr> \<rbrace>" 1786 apply (hoare_rule HoarePartial.ProcNoRec1) (* force vcg to unfold non-recursive procedure *) 1787 apply vcg 1788 apply (clarsimp simp: makeUserPML4EInvalid_body_def makeUserPML4EInvalid_impl 1789 pml4e_lift_def Let_def) 1790 done 1791 1792lemma multiple_add_less_nat: 1793 "a < (c :: nat) \<Longrightarrow> x dvd a \<Longrightarrow> x dvd c \<Longrightarrow> b < x 1794 \<Longrightarrow> a + b < c" 1795 apply (subgoal_tac "b < c - a") 1796 apply simp 1797 apply (erule order_less_le_trans) 1798 apply (rule dvd_imp_le) 1799 apply simp 1800 apply simp 1801 done 1802 1803lemma findVSpaceForASID_page_map_l4_at'_simple[wp]: 1804 notes checkPML4At_inv[wp del] 1805 shows "\<lbrace>\<top>\<rbrace> findVSpaceForASID asiv 1806 \<lbrace>\<lambda>rv s. page_map_l4_at' rv s\<rbrace>,-" 1807 apply (simp add:findVSpaceForASID_def) 1808 apply (wpsimp wp:getASID_wp simp:checkPML4At_def) 1809 done 1810 1811lemma modeUnmapPage_ccorres: 1812 "ccorres 1813 (\<lambda>rv rv'. case rv of Inl _ \<Rightarrow> rv' = scast false | Inr _ \<Rightarrow> rv' = scast true) 1814 ret__unsigned_long_' 1815 (page_map_l4_at' pmPtr) 1816 (UNIV \<inter> {s. page_size_' s = scast X64_HugePage} 1817 \<inter> {s. vroot_' s = pml4e_Ptr pmPtr} 1818 \<inter> {s. vaddr___unsigned_long_' s = vptr} 1819 \<inter> {s. pptr_' s = Ptr pptr}) 1820 hs 1821 (doE p <- lookupPDPTSlot pmPtr vptr; 1822 pdpte <- liftE (getObject p); 1823 y <- checkMappingPPtr pptr (vmpage_entry.VMPDPTE pdpte); 1824 liftE (storePDPTE p X64_H.InvalidPDPTE) 1825 odE) 1826 (Call modeUnmapPage_'proc)" 1827 apply (cinit' lift: page_size_' vroot_' vaddr___unsigned_long_' pptr_') 1828 apply ccorres_rewrite 1829 apply (rule ccorres_rhs_assoc)+ 1830 apply csymbr 1831 apply (ctac add: lookupPDPTSlot_ccorres) 1832 apply ccorres_rewrite 1833 apply csymbr 1834 apply (rule ccorres_rhs_assoc2, rule ccorres_rhs_assoc2, 1835 rule ccorres_rhs_assoc2, rule ccorres_rhs_assoc2) 1836 apply (simp only: bindE_assoc[symmetric]) 1837 apply (rule ccorres_splitE_novcg) 1838 apply (clarsimp simp: inl_rrel_def) 1839 apply (rule checkMappingPPtr_pdpte_ccorres[simplified inl_rrel_def]) 1840 apply (rule conseqPre, vcg) 1841 apply (clarsimp simp: typ_heap_simps') 1842 apply (intro conjI impI) 1843 apply (auto simp: pdpte_pdpte_1g_lift_def pdpte_lift_def cpdpte_relation_def 1844 isHugePagePDPTE_def pdpteFrame_def 1845 split: if_split_asm pdpte.split_asm pdpte.split)[5] 1846 apply (case_tac pdpte; fastforce) 1847 apply ceqv 1848 apply csymbr 1849 apply (rule ccorres_add_returnOk) 1850 apply (rule ccorres_liftE_Seq) 1851 apply (rule ccorres_split_nothrow) 1852 apply (rule storePDPTE_Basic_ccorres) 1853 apply (simp add: cpdpte_relation_def Let_def) 1854 apply ceqv 1855 apply (rule ccorres_from_vcg_throws[where P=\<top> and P'=UNIV]) 1856 apply (rule allI, rule conseqPre, vcg) 1857 apply (fastforce simp: returnOk_def return_def) 1858 apply wp 1859 apply vcg 1860 apply wp 1861 apply (simp add: guard_is_UNIV_def) 1862 apply ccorres_rewrite 1863 apply (rule ccorres_from_vcg_throws[where P=\<top> and P'=UNIV]) 1864 apply (rule allI, rule conseqPre, vcg) 1865 apply (clarsimp simp: throwError_def return_def) 1866 apply wp 1867 apply (vcg exspec=lookupPDPTSlot_modifies) 1868 apply clarsimp 1869 done 1870 1871lemmas ccorres_name_ksCurThread = ccorres_pre_getCurThread[where f="\<lambda>_. f'" for f', 1872 unfolded getCurThread_def, simplified gets_bind_ign] 1873 1874lemma unmapPage_ccorres: 1875 "ccorres dc xfdc (invs' and (\<lambda>s. 2 ^ pageBitsForSize sz \<le> gsMaxObjectSize s) 1876 and (\<lambda>_. asid_wf asid \<and> vmsz_aligned' vptr sz 1877 \<and> vptr < pptrBase)) 1878 (UNIV \<inter> {s. framesize_to_H (page_size_' s) = sz \<and> page_size_' s < 3} 1879 \<inter> {s. asid_' s = asid} \<inter> {s. vptr_' s = vptr} \<inter> {s. pptr_' s = Ptr pptr}) [] 1880 (unmapPage sz asid vptr pptr) (Call unmapPage_'proc)" 1881 apply (rule ccorres_gen_asm) 1882 apply (cinit lift: page_size_' asid_' vptr_' pptr_') 1883 apply (simp add: ignoreFailure_liftM Collect_True 1884 del: Collect_const) 1885 apply (ctac add: findVSpaceForASID_ccorres) 1886 apply (rename_tac pmPtr pm') 1887 apply (rule_tac P="page_map_l4_at' pmPtr" in ccorres_cross_over_guard) 1888 apply (simp add: liftE_bindE Collect_False bind_bindE_assoc 1889 del: Collect_const) 1890 apply (rule ccorres_splitE_novcg[where r'=dc and xf'=xfdc]) 1891 \<comment> \<open>X64SmallPage\<close> 1892 apply (rule ccorres_Cond_rhs) 1893 apply (simp add: framesize_to_H_def dc_def[symmetric]) 1894 apply (rule ccorres_rhs_assoc)+ 1895 apply (ctac add: lookupPTSlot_ccorres) 1896 apply (rename_tac pt_slot pt_slot') 1897 apply (simp add: dc_def[symmetric]) 1898 apply (rule ccorres_rhs_assoc2, rule ccorres_rhs_assoc2, 1899 rule ccorres_rhs_assoc2) 1900 apply (simp only: bindE_assoc[symmetric]) 1901 apply (rule ccorres_splitE_novcg) 1902 apply (simp only: inl_rrel_inl_rrel) 1903 apply (rule checkMappingPPtr_pte_ccorres[simplified]) 1904 apply (rule conseqPre, vcg) 1905 apply (clarsimp simp: typ_heap_simps') 1906 apply (clarsimp simp: cpte_relation_def Let_def pte_lift_def 1907 isSmallPagePTE_def if_1_0_0 1908 split: if_split_asm pte.split_asm) 1909 apply (rule ceqv_refl) 1910 apply (simp add: unfold_checkMapping_return liftE_liftM 1911 Collect_const[symmetric] dc_def[symmetric] 1912 del: Collect_const) 1913 apply (rule ccorres_handlers_weaken2) 1914 apply csymbr 1915 apply (simp add: dc_def[symmetric]) 1916 apply (rule storePTE_Basic_ccorres) 1917 apply (simp add: cpte_relation_def Let_def) 1918 apply wp 1919 apply (simp add: guard_is_UNIV_def) 1920 apply (simp add: throwError_def) 1921 apply (rule ccorres_split_throws) 1922 apply (rule ccorres_return_void_C') 1923 apply vcg 1924 apply (wp) 1925 apply simp 1926 apply (vcg exspec=lookupPTSlot_modifies) 1927 \<comment> \<open>X64LargePage\<close> 1928 apply (rule ccorres_Cond_rhs) 1929 apply (simp add: framesize_to_H_def dc_def[symmetric] 1930 del: Collect_const) 1931 apply (rule ccorres_rhs_assoc)+ 1932 apply (ctac add: lookupPDSlot_ccorres) 1933 apply (rename_tac pd_slot pd_slot') 1934 apply (simp add: dc_def[symmetric]) 1935 apply csymbr 1936 apply (rule ccorres_rhs_assoc2, rule ccorres_rhs_assoc2, 1937 rule ccorres_rhs_assoc2, rule ccorres_rhs_assoc2) 1938 apply (simp only: bindE_assoc[symmetric]) 1939 apply (rule ccorres_splitE_novcg) 1940 apply (simp only: inl_rrel_inl_rrel) 1941 apply (rule checkMappingPPtr_pde_ccorres[simplified]) 1942 apply (rule conseqPre, vcg) 1943 apply (clarsimp simp: typ_heap_simps') 1944 apply (clarsimp simp: cpde_relation_def Let_def pde_lift_def pde_pde_large_lift_def 1945 isLargePagePDE_def pde_get_tag_def pde_tag_defs 1946 split: if_split_asm pde.split_asm) 1947 apply (rule ceqv_refl) 1948 apply (simp add: unfold_checkMapping_return liftE_liftM 1949 Collect_const[symmetric] dc_def[symmetric] 1950 del: Collect_const) 1951 apply (rule ccorres_handlers_weaken2) 1952 apply csymbr 1953 apply (simp add: dc_def[symmetric]) 1954 apply (rule storePDE_Basic_ccorres) 1955 apply (simp add: cpde_relation_def Let_def) 1956 apply wp 1957 apply (simp add: guard_is_UNIV_def) 1958 apply (simp add: throwError_def) 1959 apply (rule ccorres_split_throws) 1960 apply (rule ccorres_return_void_C') 1961 apply vcg 1962 apply (wp) 1963 apply simp 1964 apply (vcg exspec=lookupPDSlot_modifies) 1965 \<comment> \<open>X64HugePage\<close> 1966 apply (simp add: framesize_to_H_def dc_def[symmetric]) 1967 apply (rule ccorres_add_return2) 1968 apply (ctac add: modeUnmapPage_ccorres) 1969 apply (rule ccorres_from_vcg_might_throw[where P="\<top>" and P'=UNIV]) 1970 apply (rule allI, rule conseqPre, vcg) 1971 apply (clarsimp simp: true_def false_def return_def inl_rrel_def split: sum.split_asm) 1972 apply wp 1973 apply (vcg exspec=modeUnmapPage_modifies) 1974 apply ceqv 1975 apply (rule ccorres_name_ksCurThread) 1976 apply (rule_tac val="tcb_ptr_to_ctcb_ptr rv" and xf'="\<lambda>s. ksCurThread_' (globals s)" 1977 in ccorres_abstract_known, ceqv) 1978 apply (rule ccorres_move_array_assertion_tcb_ctes ccorres_move_c_guard_tcb_ctes)+ 1979 apply (rule ccorres_symb_exec_r) 1980 apply (rule ccorres_rhs_assoc2) 1981 apply (rule ccorres_symb_exec_r_known_rv[where R=\<top> and R'=UNIV and xf'=ret__int_' and val=1]) 1982 apply vcg 1983 apply clarsimp 1984 apply ceqv 1985 apply ccorres_rewrite 1986 apply (clarsimp simp: liftE_liftM) 1987 apply (ctac add: invalidateTranslationSingleASID_ccorres[simplified dc_def]) 1988 apply vcg 1989 apply clarsimp 1990 apply vcg 1991 apply (rule conseqPre, vcg) 1992 apply clarsimp 1993 apply (wpsimp simp: cur_tcb'_def[symmetric]) 1994 apply (clarsimp simp: guard_is_UNIV_def conj_comms tcb_cnode_index_defs) 1995 apply (simp add: throwError_def) 1996 apply (rule ccorres_split_throws) 1997 apply (rule ccorres_return_void_C[unfolded dc_def]) 1998 apply vcg 1999 apply wpsimp 2000 apply (simp add: Collect_const_mem) 2001 apply (vcg exspec=findVSpaceForASID_modifies) 2002 by (auto simp: invs_arch_state' invs_no_0_obj' invs_valid_objs' vmsz_aligned'_def 2003 is_aligned_weaken[OF _ pbfs_atleast_pageBits] pageBitsForSize_def 2004 Collect_const_mem vm_page_size_defs word_sle_def 2005 ccHoarePost_def typ_heap_simps bit_simps 2006 dest!: page_directory_at_rf_sr 2007 elim!: clift_array_assertion_imp 2008 split: vmpage_size.splits 2009 elim: is_aligned_weaken 2010 | unat_arith)+ 2011 2012(* FIXME: move *) 2013lemma cap_to_H_PageCap_tag: 2014 "\<lbrakk> cap_to_H cap = ArchObjectCap (PageCap p R sz mt d A); 2015 cap_lift C_cap = Some cap \<rbrakk> \<Longrightarrow> 2016 cap_get_tag C_cap = scast cap_frame_cap" 2017 apply (clarsimp simp: cap_to_H_def Let_def split: cap_CL.splits if_split_asm) 2018 by (simp_all add: Let_def cap_lift_def split_def split: if_splits) 2019 2020lemma updateCap_frame_mapped_addr_ccorres: 2021 notes option.case_cong_weak [cong] 2022 shows "ccorres dc xfdc 2023 (cte_wp_at' (\<lambda>c. ArchObjectCap cap = cteCap c) ctSlot and K (isPageCap cap)) 2024 UNIV [] 2025 (updateCap ctSlot (ArchObjectCap (capVPMapType_update (\<lambda>_. VMNoMap) (capVPMappedAddress_update Map.empty cap)))) 2026 (Guard C_Guard {s. s \<Turnstile>\<^sub>c cte_Ptr ctSlot} 2027 (CALL cap_frame_cap_ptr_set_capFMappedAddress(cap_Ptr &(cte_Ptr ctSlot\<rightarrow>[''cap_C'']), 0));; 2028 Guard C_Guard {s. s \<Turnstile>\<^sub>c cte_Ptr ctSlot} 2029 (CALL cap_frame_cap_ptr_set_capFMappedASID(cap_Ptr &(cte_Ptr ctSlot\<rightarrow>[''cap_C'']), scast asidInvalid));; 2030 Guard C_Guard {s. s \<Turnstile>\<^sub>c cte_Ptr ctSlot} 2031 (CALL cap_frame_cap_ptr_set_capFMapType(cap_Ptr &(cte_Ptr ctSlot\<rightarrow>[''cap_C'']), scast X86_MappingNone)))" 2032 unfolding updateCap_def 2033 apply (rule ccorres_guard_imp2) 2034 apply (rule ccorres_pre_getCTE) 2035 apply (rule_tac P = "\<lambda>s. ctes_of s ctSlot = Some cte 2036 \<and> cteCap cte = ArchObjectCap cap \<and> isPageCap cap" and 2037 P' = "UNIV" 2038 in ccorres_from_vcg) 2039 apply (rule allI, rule conseqPre, vcg) 2040 apply clarsimp 2041 apply (erule (1) rf_sr_ctes_of_cliftE) 2042 apply (frule cap_CL_lift) 2043 apply (clarsimp simp: typ_heap_simps) 2044 apply (rule context_conjI) 2045 apply (clarsimp simp: isCap_simps) 2046 apply (drule cap_CL_lift) 2047 apply (drule (1) cap_to_H_PageCap_tag) 2048 apply simp 2049 apply (clarsimp simp: isCap_simps typ_heap_simps) 2050 apply (rule fst_setCTE [OF ctes_of_cte_at], assumption) 2051 apply (erule bexI [rotated]) 2052 apply clarsimp 2053 apply (frule (1) rf_sr_ctes_of_clift) 2054 apply clarsimp 2055 prefer 2 apply (clarsimp simp: cte_wp_at_ctes_of) 2056 apply (clarsimp simp: packed_heap_update_collapse_hrs) 2057 apply (subgoal_tac "ccte_relation (cteCap_update (\<lambda>_. ArchObjectCap (PageCap v0 v1 VMNoMap v3 d None)) 2058 (cte_to_H ctel')) 2059 (cte_C.cap_C_update (\<lambda>_. capb) cte')") 2060 apply (clarsimp simp: rf_sr_def cstate_relation_def typ_heap_simps Let_def cpspace_relation_def) 2061 apply (rule conjI) 2062 apply (erule (3) cmap_relation_updI) 2063 subgoal by simp 2064 apply (erule_tac t=s' in ssubst) 2065 apply (simp add: heap_to_user_data_def) 2066 apply (rule conjI) 2067 apply (erule (1) setCTE_tcb_case) 2068 subgoal by (simp add: carch_state_relation_def cmachine_state_relation_def 2069 typ_heap_simps h_t_valid_clift_Some_iff 2070 cvariable_array_map_const_add_map_option[where f="tcb_no_ctes_proj"] 2071 fpu_null_state_heap_update_tag_disj_simps) 2072 apply (clarsimp simp: ccte_relation_def) 2073 apply (clarsimp simp: cte_lift_def) 2074 apply (simp split: option.splits) 2075 apply (clarsimp simp: cte_to_H_def c_valid_cte_def) 2076 apply (rule conjI, simp add: cap_frame_cap_lift) 2077 apply (clarsimp simp: cap_frame_cap_lift_def) 2078 apply (clarsimp simp: c_valid_cap_def cl_valid_cap_def 2079 cap_frame_cap_lift cap_to_H_def maptype_to_H_def 2080 X86_MappingNone_def asidInvalid_def) 2081 done 2082 2083(* FIXME: move *) 2084lemma diminished_PageCap: 2085 "diminished' (ArchObjectCap (PageCap p R mt sz d a)) cap \<Longrightarrow> 2086 \<exists>R'. cap = ArchObjectCap (PageCap p R' mt sz d a)" 2087 apply (clarsimp simp: diminished'_def) 2088 apply (clarsimp simp: maskCapRights_def Let_def) 2089 apply (cases cap, simp_all add: isCap_simps) 2090 apply (simp add: X64_H.maskCapRights_def) 2091 apply (simp add: isPageCap_def split: arch_capability.splits) 2092 done 2093 2094lemma ccap_relation_mapped_asid_0: 2095 "\<lbrakk>ccap_relation (ArchObjectCap (PageCap d v0 v1 v2 v3 v4)) cap\<rbrakk> 2096 \<Longrightarrow> (capFMappedASID_CL (cap_frame_cap_lift cap) \<noteq> 0 \<longrightarrow> v4 \<noteq> None) \<and> 2097 (capFMappedASID_CL (cap_frame_cap_lift cap) = 0 \<longrightarrow> v4 = None)" 2098 apply (frule cap_get_tag_PageCap_frame) 2099 apply (frule cap_get_tag_isCap_unfolded_H_cap) 2100 apply simp 2101 done 2102 2103(* FIXME: move *) 2104lemma getSlotCap_wp': 2105 "\<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>" 2106 apply (simp add: getSlotCap_def) 2107 apply (wp getCTE_wp') 2108 apply (clarsimp simp: cte_wp_at_ctes_of) 2109 done 2110 2111lemma vmsz_aligned_aligned_pageBits: 2112 "vmsz_aligned' ptr sz \<Longrightarrow> is_aligned ptr pageBits" 2113 apply (simp add: vmsz_aligned'_def) 2114 apply (erule is_aligned_weaken) 2115 apply (simp add: pageBits_def pageBitsForSize_def 2116 split: vmpage_size.split) 2117 done 2118 2119lemma framesize_from_H_bounded: 2120 "framesize_from_H x < 3" 2121 by (clarsimp simp: framesize_from_H_def X86_SmallPage_def X86_LargePage_def X64_HugePage_def 2122 split: vmpage_size.split) 2123 2124lemma performPageInvocationUnmap_ccorres': 2125 "ccorres (\<lambda>rv rv'. rv' = scast EXCEPTION_NONE) ret__unsigned_long_' 2126 (invs' and cte_wp_at' (diminished' (ArchObjectCap cap) o cteCap) ctSlot and K (isPageCap cap)) 2127 (UNIV \<inter> \<lbrace>ccap_relation (ArchObjectCap cap) \<acute>cap\<rbrace> \<inter> \<lbrace>\<acute>ctSlot = Ptr ctSlot\<rbrace>) 2128 hs 2129 (performPageInvocationUnmap cap ctSlot) 2130 (Call performX86PageInvocationUnmap_'proc)" 2131 apply (cinit lift: cap_' ctSlot_') 2132 apply csymbr 2133 apply (rule ccorres_guard_imp 2134 [where A="invs' and cte_wp_at' (diminished' (ArchObjectCap cap) o cteCap) ctSlot 2135 and K (isPageCap cap)"]) 2136 apply wpc 2137 apply (rule_tac P="ret__unsigned_longlong = 0" in ccorres_gen_asm) 2138 apply clarsimp 2139 apply (rule ccorres_symb_exec_l) 2140 apply (subst bind_return [symmetric]) 2141 apply (rule ccorres_rhs_assoc2)+ 2142 apply (rule ccorres_split_nothrow_novcg) 2143 apply (rule updateCap_frame_mapped_addr_ccorres) 2144 apply ceqv 2145 apply (rule_tac P=\<top> and P'=UNIV in ccorres_from_vcg_throws) 2146 apply (rule allI, rule conseqPre, vcg) 2147 apply (clarsimp simp: return_def) 2148 apply wp[1] 2149 apply (simp add: guard_is_UNIV_def) 2150 apply (wp getSlotCap_wp', simp) 2151 apply (wp getSlotCap_wp') 2152 apply simp 2153 apply (rule_tac P="ret__unsigned_longlong \<noteq> 0" in ccorres_gen_asm) 2154 apply (simp cong: Guard_no_cong) 2155 apply (rule ccorres_rhs_assoc)+ 2156 apply (csymbr) 2157 apply csymbr 2158 apply csymbr 2159 apply csymbr 2160 apply wpc 2161 apply (ctac (no_vcg) add: unmapPage_ccorres) 2162 apply (rule ccorres_add_return2) 2163 apply (rule ccorres_rhs_assoc2)+ 2164 apply (rule ccorres_split_nothrow_novcg) 2165 apply (rule ccorres_symb_exec_l) 2166 apply clarsimp 2167 apply (rule updateCap_frame_mapped_addr_ccorres) 2168 apply (wp getSlotCap_wp', simp) 2169 apply (wp getSlotCap_wp') 2170 apply simp 2171 apply ceqv 2172 apply (rule_tac P=\<top> and P'=UNIV in ccorres_from_vcg_throws) 2173 apply (rule allI, rule conseqPre, vcg) 2174 apply (clarsimp simp: return_def) 2175 apply wp[1] 2176 apply (simp add: guard_is_UNIV_def) 2177 apply (simp add: cte_wp_at_ctes_of) 2178 apply wp 2179 apply (clarsimp simp: cte_wp_at_ctes_of isCap_simps split: if_split) 2180 apply (drule diminished_PageCap) 2181 apply clarsimp 2182 apply (frule ccap_relation_mapped_asid_0) 2183 apply (frule ctes_of_valid', clarsimp) 2184 apply (drule valid_global_refsD_with_objSize, clarsimp) 2185 apply (fastforce simp: mask_def valid_cap'_def 2186 vmsz_aligned_aligned_pageBits) 2187 apply assumption 2188 apply (clarsimp simp: cte_wp_at_ctes_of isCap_simps split: if_split) 2189 apply (clarsimp simp: cap_get_tag_isCap_unfolded_H_cap 2190 framesize_from_H_bounded framesize_from_to_H 2191 ccap_relation_PageCap_BasePtr ccap_relation_PageCap_Size 2192 ccap_relation_PageCap_IsDevice ccap_relation_PageCap_MappedASID 2193 ccap_relation_PageCap_MappedAddress) 2194 done 2195 2196definition 2197 maptype_from_H :: "vmmap_type \<Rightarrow> machine_word" 2198where 2199 "maptype_from_H x \<equiv> case x of VMNoMap \<Rightarrow> scast X86_MappingNone 2200 | VMVSpaceMap \<Rightarrow> scast X86_MappingVSpace" 2201 2202lemma maptype_from_H_wf: 2203 "(maptype_to_H \<circ> maptype_from_H) = id" 2204 apply (clarsimp simp: maptype_to_H_def maptype_from_H_def o_def id_def) 2205 by (rule ext, clarsimp simp: vm_page_map_type_defs split: if_splits vmmap_type.splits ) 2206 2207lemma ccap_relation_PageCap_MapType: 2208 "ccap_relation (ArchObjectCap (PageCap p r t s d m)) ccap 2209 \<Longrightarrow> capFMapType_CL (cap_frame_cap_lift ccap) = maptype_from_H t" 2210 apply (frule cap_get_tag_isCap_unfolded_H_cap) 2211 apply (clarsimp simp: cap_frame_cap_lift_def ccap_relation_def cap_to_H_def cap_lift_def 2212 Let_def cap_tag_defs c_valid_cap_def cl_valid_cap_def 2213 split: if_splits) 2214 by (clarsimp simp: maptype_to_H_def maptype_from_H_def vm_page_map_type_defs mask_def 2215 split: vmmap_type.splits if_splits, word_bitwise, clarsimp)+ 2216 2217lemma performPageInvocationUnmap_ccorres: 2218 notes Collect_const[simp del] 2219 shows 2220 "ccorres (K (K \<bottom>) \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') 2221 (invs' and cte_wp_at' (diminished' (ArchObjectCap cap) o cteCap) ctSlot and K (isPageCap cap)) 2222 (UNIV \<inter> \<lbrace>ccap_relation (ArchObjectCap cap) \<acute>cap\<rbrace> \<inter> \<lbrace>\<acute>cte = Ptr ctSlot\<rbrace>) 2223 hs 2224 (liftE (performPageInvocation (PageUnmap cap ctSlot))) 2225 (Call performX86FrameInvocationUnmap_'proc)" 2226 apply (simp only: liftE_liftM ccorres_liftM_simp K_def) 2227 apply (rule ccorres_gen_asm) 2228 apply (cinit' lift: cap_' cte_' simp: performPageInvocation_def) 2229 apply csymbr 2230 apply (clarsimp simp: isCap_simps) 2231 apply (frule ccap_relation_mapped_asid_0) 2232 apply (rule ccorres_Cond_rhs_Seq) 2233 apply (rule ccorres_rhs_assoc)+ 2234 apply csymbr 2235 apply clarsimp 2236 apply (frule ccap_relation_PageCap_MapType) 2237 apply (frule cap_get_tag_isCap_unfolded_H_cap) 2238 apply (rule ccorres_Cond_rhs_Seq) 2239 apply (clarsimp simp: asidInvalid_def maptype_from_H_def vm_page_map_type_defs split: vmmap_type.splits) 2240 apply (rule ccorres_rhs_assoc) 2241 apply (drule_tac s=cap in sym, simp) (* schematic ugliness *) 2242 apply ccorres_rewrite 2243 apply (rule ccorres_add_return2) thm ccorres_add_returnOk 2244 apply (ctac add: performPageInvocationUnmap_ccorres'[simplified K_def, simplified]) 2245 apply (rule_tac P=\<top> and P'=UNIV in ccorres_from_vcg_throws) 2246 apply (rule allI, rule conseqPre, vcg) 2247 apply (clarsimp simp: return_def) 2248 apply wp 2249 apply (vcg exspec=performX86PageInvocationUnmap_modifies) 2250 apply (clarsimp simp: asidInvalid_def) 2251 apply (clarsimp simp: maptype_from_H_def split: vmmap_type.splits) 2252 apply(rule ccorres_fail) 2253 apply (clarsimp simp: asidInvalid_def) 2254 apply (rule_tac P=\<top> and P'=UNIV in ccorres_from_vcg_throws) 2255 apply (rule allI, rule conseqPre, vcg) 2256 apply (clarsimp simp: return_def) 2257 by (clarsimp simp: o_def isCap_simps cap_get_tag_isCap_unfolded_H_cap) 2258 2259 2260lemma SuperUserFromVMRights_spec: 2261 "\<forall>s. \<Gamma> \<turnstile> \<lbrace>s. \<acute>vm_rights < 4 \<and> \<acute>vm_rights \<noteq> 0\<rbrace> Call SuperUserFromVMRights_'proc 2262 \<lbrace> \<acute>ret__unsigned = superuser_from_vm_rights (vmrights_to_H \<^bsup>s\<^esup>vm_rights) \<rbrace>" 2263 apply vcg 2264 apply (simp add: vmrights_to_H_def superuser_from_vm_rights_def Kernel_C.VMKernelOnly_def 2265 Kernel_C.VMReadOnly_def Kernel_C.VMReadWrite_def) 2266 apply clarsimp 2267 apply (drule word_less_cases, auto)+ 2268 done 2269 2270lemma superuser_from_vm_rights_mask: 2271 "ucast ((superuser_from_vm_rights R) :: 32 word) && 1 = (superuser_from_vm_rights R :: machine_word)" 2272 by (simp add: superuser_from_vm_rights_def split: vmrights.splits) 2273 2274lemma WritableFromVMRights_spec: 2275 "\<forall>s. \<Gamma> \<turnstile> \<lbrace>s. \<acute>vm_rights < 4 \<and> \<acute>vm_rights \<noteq> 0\<rbrace> Call WritableFromVMRights_'proc 2276 \<lbrace> \<acute>ret__unsigned = writable_from_vm_rights (vmrights_to_H \<^bsup>s\<^esup>vm_rights) \<rbrace>" 2277 apply vcg 2278 apply (simp add: vmrights_to_H_def writable_from_vm_rights_def Kernel_C.VMKernelOnly_def 2279 Kernel_C.VMReadOnly_def Kernel_C.VMReadWrite_def) 2280 apply clarsimp 2281 apply (drule word_less_cases, auto)+ 2282 done 2283 2284lemma writable_from_vm_rights_mask: 2285 "ucast ((writable_from_vm_rights R) :: 32 word) && 1 = (writable_from_vm_rights R :: machine_word)" 2286 by (simp add: writable_from_vm_rights_def split: vmrights.splits) 2287 2288lemma makeUserPTE_spec: 2289 "\<forall>s. \<Gamma> \<turnstile> 2290 \<lbrace>s. \<acute>vm_rights < 4 \<and> \<acute>vm_rights \<noteq> 0\<rbrace> 2291 Call makeUserPTE_'proc 2292 \<lbrace> pte_lift \<acute>ret__struct_pte_C = \<lparr> 2293 pte_CL.xd_CL = 0, 2294 pte_CL.page_base_address_CL = \<^bsup>s\<^esup>paddr && (mask 39 << 12), 2295 pte_CL.global_CL = 0, 2296 pte_CL.pat_CL = x86PATBit_CL (vm_attributes_lift \<^bsup>s\<^esup>vm_attr), 2297 pte_CL.dirty_CL = 0, 2298 pte_CL.accessed_CL = 0, 2299 pte_CL.cache_disabled_CL = x86PCDBit_CL (vm_attributes_lift \<^bsup>s\<^esup>vm_attr), 2300 pte_CL.write_through_CL = x86PWTBit_CL (vm_attributes_lift \<^bsup>s\<^esup>vm_attr), 2301 pte_CL.super_user_CL = superuser_from_vm_rights (vmrights_to_H \<^bsup>s\<^esup>vm_rights), 2302 pte_CL.read_write_CL = writable_from_vm_rights (vmrights_to_H \<^bsup>s\<^esup>vm_rights), 2303 pte_CL.present_CL = 1\<rparr> \<rbrace>" 2304 apply (rule allI, rule conseqPre, vcg) 2305 apply (clarsimp simp: superuser_from_vm_rights_mask writable_from_vm_rights_mask 2306 vm_attributes_lift_def mask_def) 2307 done 2308 2309lemma makeUserPDELargePage_spec: 2310 "\<forall>s. \<Gamma> \<turnstile> 2311 \<lbrace>s. \<acute>vm_rights < 4 \<and> \<acute>vm_rights \<noteq> 0\<rbrace> 2312 Call makeUserPDELargePage_'proc 2313 \<lbrace> pde_lift \<acute>ret__struct_pde_C = Some (Pde_pde_large \<lparr> 2314 pde_pde_large_CL.xd_CL = 0, 2315 pde_pde_large_CL.page_base_address_CL = \<^bsup>s\<^esup>paddr && (mask 30 << 21), 2316 pde_pde_large_CL.pat_CL = x86PATBit_CL (vm_attributes_lift \<^bsup>s\<^esup>vm_attr), 2317 pde_pde_large_CL.global_CL = 0, 2318 pde_pde_large_CL.dirty_CL = 0, 2319 pde_pde_large_CL.accessed_CL = 0, 2320 pde_pde_large_CL.cache_disabled_CL = x86PCDBit_CL (vm_attributes_lift \<^bsup>s\<^esup>vm_attr), 2321 pde_pde_large_CL.write_through_CL = x86PWTBit_CL (vm_attributes_lift \<^bsup>s\<^esup>vm_attr), 2322 pde_pde_large_CL.super_user_CL = superuser_from_vm_rights (vmrights_to_H \<^bsup>s\<^esup>vm_rights), 2323 pde_pde_large_CL.read_write_CL = writable_from_vm_rights (vmrights_to_H \<^bsup>s\<^esup>vm_rights), 2324 pde_pde_large_CL.present_CL = 1\<rparr>) \<rbrace>" 2325 apply (rule allI, rule conseqPre, vcg) 2326 apply (clarsimp simp: pde_pde_large_lift 2327 superuser_from_vm_rights_mask writable_from_vm_rights_mask 2328 vm_attributes_lift_def mask_def) 2329 done 2330 2331lemma makeUserPDEPageTable_spec: 2332 "\<forall>s. \<Gamma> \<turnstile> 2333 \<lbrace>s. vmsz_aligned' (\<acute>paddr) X64SmallPage\<rbrace> 2334 Call makeUserPDEPageTable_'proc 2335 \<lbrace> pde_lift \<acute>ret__struct_pde_C = Some (Pde_pde_pt \<lparr> 2336 pde_pde_pt_CL.xd_CL = 0, 2337 pde_pde_pt_CL.pt_base_address_CL = \<^bsup>s\<^esup>paddr && (mask 39 << 12), 2338 pde_pde_pt_CL.accessed_CL = 0, 2339 pde_pde_pt_CL.cache_disabled_CL = x86PCDBit_CL (vm_attributes_lift \<^bsup>s\<^esup>vm_attr), 2340 pde_pde_pt_CL.write_through_CL = x86PWTBit_CL (vm_attributes_lift \<^bsup>s\<^esup>vm_attr), 2341 pde_pde_pt_CL.super_user_CL = 1, 2342 pde_pde_pt_CL.read_write_CL = 1, 2343 pde_pde_pt_CL.present_CL = 1\<rparr>) \<rbrace>" 2344 apply (rule allI, rule conseqPre, vcg) 2345 apply (clarsimp simp: pde_pde_pt_lift 2346 superuser_from_vm_rights_mask writable_from_vm_rights_mask 2347 vm_attributes_lift_def mask_def) 2348 done 2349 2350lemma makeUserPDPTEHugePage_spec: 2351 "\<forall>s. \<Gamma> \<turnstile> 2352 \<lbrace>s. \<acute>vm_rights < 4 \<and> \<acute>vm_rights \<noteq> 0 \<and> vmsz_aligned' (\<acute>paddr) X64HugePage \<rbrace> 2353 Call makeUserPDPTEHugePage_'proc 2354 \<lbrace> pdpte_lift \<acute>ret__struct_pdpte_C = Some (Pdpte_pdpte_1g \<lparr> 2355 pdpte_pdpte_1g_CL.xd_CL = 0, 2356 pdpte_pdpte_1g_CL.page_base_address_CL = \<^bsup>s\<^esup>paddr && (mask 21 << 30), 2357 pdpte_pdpte_1g_CL.pat_CL = 0, 2358 pdpte_pdpte_1g_CL.global_CL = 0, 2359 pdpte_pdpte_1g_CL.dirty_CL = 0, 2360 pdpte_pdpte_1g_CL.accessed_CL = 0, 2361 pdpte_pdpte_1g_CL.cache_disabled_CL = x86PCDBit_CL (vm_attributes_lift \<^bsup>s\<^esup>vm_attr), 2362 pdpte_pdpte_1g_CL.write_through_CL = x86PWTBit_CL (vm_attributes_lift \<^bsup>s\<^esup>vm_attr), 2363 pdpte_pdpte_1g_CL.super_user_CL = superuser_from_vm_rights (vmrights_to_H \<^bsup>s\<^esup>vm_rights), 2364 pdpte_pdpte_1g_CL.read_write_CL = writable_from_vm_rights (vmrights_to_H \<^bsup>s\<^esup>vm_rights), 2365 pdpte_pdpte_1g_CL.present_CL = 1\<rparr>) \<rbrace>" 2366 apply (rule allI, rule conseqPre, vcg) 2367 apply (clarsimp simp: pdpte_pdpte_1g_lift 2368 superuser_from_vm_rights_mask writable_from_vm_rights_mask 2369 vm_attributes_lift_def mask_def) 2370 done 2371 2372lemma vmAttributesFromWord_spec: 2373 "\<forall>s. \<Gamma> \<turnstile> \<lbrace>s. True\<rbrace> Call vmAttributesFromWord_'proc 2374 \<lbrace> vm_attributes_lift \<acute>ret__struct_vm_attributes_C = 2375 \<lparr> x86PATBit_CL = (\<^bsup>s\<^esup>w >> 2) && 1, 2376 x86PCDBit_CL = (\<^bsup>s\<^esup>w >> 1) && 1, 2377 x86PWTBit_CL = \<^bsup>s\<^esup>w && 1 \<rparr> \<rbrace>" 2378 by (vcg, simp add: vm_attributes_lift_def word_sless_def word_sle_def mask_def) 2379 2380lemma cap_to_H_PML4Cap_tag: 2381 "\<lbrakk> cap_to_H cap = ArchObjectCap (PML4Cap p A); 2382 cap_lift C_cap = Some cap \<rbrakk> \<Longrightarrow> 2383 cap_get_tag C_cap = scast cap_pml4_cap" 2384 apply (clarsimp simp: cap_to_H_def Let_def split: cap_CL.splits if_split_asm) 2385 apply (simp_all add: Let_def cap_lift_def split: if_splits) 2386 done 2387 2388lemma cap_to_H_PML4Cap: 2389 "cap_to_H cap = ArchObjectCap (PML4Cap p asid) \<Longrightarrow> 2390 \<exists>cap_CL. cap = Cap_pml4_cap cap_CL \<and> 2391 to_bool (capPML4IsMapped_CL cap_CL) = (asid \<noteq> None) \<and> 2392 (asid \<noteq> None \<longrightarrow> capPML4MappedASID_CL cap_CL = the asid) \<and> 2393 capPML4BasePtr_CL cap_CL = p" 2394 by (auto simp add: cap_to_H_def Let_def split: cap_CL.splits if_splits) 2395 2396lemma cap_lift_PML4Cap_Base: 2397 "\<lbrakk> cap_to_H cap_cl = ArchObjectCap (PML4Cap p asid); 2398 cap_lift cap_c = Some cap_cl \<rbrakk> 2399 \<Longrightarrow> p = capPML4BasePtr_CL (cap_pml4_cap_lift cap_c)" 2400 apply (simp add: cap_pml4_cap_lift_def) 2401 apply (clarsimp simp: cap_to_H_def Let_def split: cap_CL.splits if_splits) 2402 done 2403 2404declare mask_Suc_0[simp] 2405 2406(* FIXME: move *) 2407lemma setCTE_asidpool': 2408 "\<lbrace> ko_at' (ASIDPool pool) p \<rbrace> setCTE c p' \<lbrace>\<lambda>_. ko_at' (ASIDPool pool) p\<rbrace>" 2409 apply (clarsimp simp: setCTE_def) 2410 apply (simp add: setObject_def split_def) 2411 apply (rule hoare_seq_ext [OF _ hoare_gets_post]) 2412 apply (clarsimp simp: valid_def in_monad) 2413 apply (frule updateObject_type) 2414 apply (clarsimp simp: obj_at'_def projectKOs) 2415 apply (rule conjI) 2416 apply (clarsimp simp: lookupAround2_char1) 2417 apply (clarsimp split: if_split) 2418 apply (case_tac obj', auto)[1] 2419 apply (rename_tac arch_kernel_object) 2420 apply (case_tac arch_kernel_object, auto)[1] 2421 apply (simp add: updateObject_cte) 2422 apply (clarsimp simp: updateObject_cte typeError_def magnitudeCheck_def in_monad 2423 split: kernel_object.splits if_splits option.splits) 2424 apply (clarsimp simp: ps_clear_upd' lookupAround2_char1) 2425 done 2426 2427(* FIXME: move *) 2428lemma udpateCap_asidpool': 2429 "\<lbrace> ko_at' (ASIDPool pool) p \<rbrace> updateCap c p' \<lbrace>\<lambda>_. ko_at' (ASIDPool pool) p\<rbrace>" 2430 apply (simp add: updateCap_def) 2431 apply (wp setCTE_asidpool') 2432 done 2433 2434(* FIXME: move *) 2435lemma asid_pool_at_rf_sr: 2436 "\<lbrakk>ko_at' (ASIDPool pool) p s; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> 2437 \<exists>pool'. cslift s' (ap_Ptr p) = Some pool' \<and> 2438 casid_pool_relation (ASIDPool pool) pool'" 2439 apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def cpspace_relation_def) 2440 apply (erule (1) cmap_relation_ko_atE) 2441 apply clarsimp 2442 done 2443 2444(* FIXME: move *) 2445lemma asid_pool_at_ko: 2446 "asid_pool_at' p s \<Longrightarrow> \<exists>pool. ko_at' (ASIDPool pool) p s" 2447 apply (clarsimp simp: typ_at'_def obj_at'_def ko_wp_at'_def projectKOs) 2448 apply (case_tac ko, auto) 2449 apply (rename_tac arch_kernel_object) 2450 apply (case_tac arch_kernel_object, auto)[1] 2451 apply (rename_tac asidpool) 2452 apply (case_tac asidpool, auto)[1] 2453 done 2454 2455(* FIXME: move *) 2456lemma asid_pool_at_c_guard: 2457 "\<lbrakk>asid_pool_at' p s; (s, s') \<in> rf_sr\<rbrakk> \<Longrightarrow> c_guard (ap_Ptr p)" 2458 by (fastforce intro: typ_heap_simps dest!: asid_pool_at_ko asid_pool_at_rf_sr) 2459 2460(* FIXME: move *) 2461lemma setObjectASID_Basic_ccorres: 2462 "ccorres dc xfdc \<top> {s. f s = p \<and> casid_pool_relation pool (asid_pool_C (pool' s))} hs 2463 (setObject p pool) 2464 ((Basic (\<lambda>s. globals_update( t_hrs_'_update 2465 (hrs_mem_update (heap_update (Ptr &(ap_Ptr (f s)\<rightarrow>[''array_C''])) (pool' s)))) s)))" 2466 apply (rule setObject_ccorres_helper) 2467 apply (simp_all add: objBits_simps archObjSize_def pageBits_def) 2468 apply (rule conseqPre, vcg) 2469 apply (rule subsetI, clarsimp simp: Collect_const_mem) 2470 apply (rule cmap_relationE1, erule rf_sr_cpspace_asidpool_relation, 2471 erule ko_at_projectKO_opt) 2472 apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def) 2473 apply (rule conjI) 2474 apply (clarsimp simp: cpspace_relation_def typ_heap_simps 2475 update_asidpool_map_to_asidpools 2476 update_asidpool_map_tos) 2477 apply (case_tac y') 2478 apply clarsimp 2479 apply (erule cmap_relation_updI, 2480 erule ko_at_projectKO_opt, simp+) 2481 apply (simp add: cready_queues_relation_def 2482 carch_state_relation_def 2483 fpu_null_state_heap_update_tag_disj_simps 2484 cmachine_state_relation_def 2485 Let_def typ_heap_simps 2486 update_asidpool_map_tos) 2487 done 2488 2489lemma getObject_ap_inv [wp]: "\<lbrace>P\<rbrace> (getObject addr :: asidpool kernel) \<lbrace>\<lambda>rv. P\<rbrace>" 2490 apply (rule getObject_inv) 2491 apply simp 2492 apply (rule loadObject_default_inv) 2493 done 2494 2495lemma getObject_ko_at_ap [wp]: 2496 "\<lbrace>\<top>\<rbrace> getObject p \<lbrace>\<lambda>rv::asidpool. ko_at' rv p\<rbrace>" 2497 by (rule getObject_ko_at | simp add: objBits_simps archObjSize_def bit_simps)+ 2498 2499lemma canonical_address_page_map_l4_at': 2500 "\<lbrakk>page_map_l4_at' p s; pspace_canonical' s\<rbrakk> \<Longrightarrow> 2501 canonical_address p" 2502 apply (clarsimp simp: page_map_l4_at'_def) 2503 apply (drule_tac x=0 in spec, clarsimp simp: bit_simps typ_at_to_obj_at_arches) 2504 apply (erule (1) obj_at'_is_canonical) 2505 done 2506 2507lemma performASIDPoolInvocation_ccorres: 2508 notes option.case_cong_weak [cong] 2509 shows 2510 "ccorres (K (K \<bottom>) \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') 2511 (invs' and cte_wp_at' (isPML4Cap' o cteCap) ctSlot and asid_pool_at' poolPtr 2512 and K (asid \<le> mask asid_bits \<and> asid \<noteq> ucast asidInvalid)) 2513 (UNIV \<inter> \<lbrace>\<acute>poolPtr = Ptr poolPtr\<rbrace> \<inter> \<lbrace>\<acute>asid = asid\<rbrace> \<inter> \<lbrace>\<acute>vspaceCapSlot = Ptr ctSlot\<rbrace>) 2514 [] 2515 (liftE (performASIDPoolInvocation (Assign asid poolPtr ctSlot))) 2516 (Call performASIDPoolInvocation_'proc)" 2517 apply (simp only: liftE_liftM ccorres_liftM_simp) 2518 apply (cinit lift: poolPtr_' asid_' vspaceCapSlot_') 2519 apply (rule ccorres_symb_exec_l) 2520 apply (rule ccorres_rhs_assoc2) 2521 apply (rule_tac ccorres_split_nothrow [where r'=dc and xf'=xfdc]) 2522 apply (simp add: updateCap_def) 2523 apply (rule_tac A="cte_wp_at' ((=) rv o cteCap) ctSlot 2524 and K (isPML4Cap' rv \<and> asid \<le> mask asid_bits \<and> asid \<noteq> ucast asidInvalid)" 2525 and A'=UNIV in ccorres_guard_imp2) 2526 apply (rule ccorres_pre_getCTE) 2527 apply (rule_tac P="cte_wp_at' ((=) rv o cteCap) ctSlot 2528 and K (isPML4Cap' rv \<and> asid \<le> mask asid_bits \<and> asid \<noteq> ucast asidInvalid) 2529 and cte_wp_at' ((=) rva) ctSlot" 2530 and P'=UNIV in ccorres_from_vcg) 2531 apply (rule allI, rule conseqPre, vcg) 2532 apply (clarsimp simp: cte_wp_at_ctes_of) 2533 apply (erule (1) rf_sr_ctes_of_cliftE) 2534 apply (clarsimp simp: typ_heap_simps) 2535 apply (rule conjI) 2536 apply (clarsimp simp: isPML4Cap'_def) 2537 apply (drule cap_CL_lift) 2538 apply (drule (1) cap_to_H_PML4Cap_tag) 2539 apply simp 2540 apply (clarsimp simp: typ_heap_simps' isPML4Cap'_def) 2541 apply (rule fst_setCTE [OF ctes_of_cte_at], assumption) 2542 apply (erule bexI [rotated]) 2543 apply clarsimp 2544 apply (frule (1) rf_sr_ctes_of_clift) 2545 apply clarsimp 2546 apply (clarsimp simp: rf_sr_def cstate_relation_def typ_heap_simps 2547 Let_def cpspace_relation_def) 2548 apply (rule conjI) 2549 apply (erule (2) cmap_relation_updI) 2550 apply (clarsimp simp: ccte_relation_def) 2551 apply (clarsimp simp: cte_lift_def) 2552 apply (simp split: option.splits) 2553 apply clarsimp 2554 apply (case_tac cte') 2555 apply clarsimp 2556 apply (rule conjI) 2557 apply (clarsimp simp: cap_lift_def Let_def cap_tag_defs) 2558 apply clarsimp 2559 apply (simp add: cte_to_H_def c_valid_cte_def) 2560 apply (simp add: cap_pml4_cap_lift) 2561 apply (simp (no_asm) add: cap_to_H_def) 2562 apply (simp add: to_bool_def asid_bits_def le_mask_imp_and_mask word_bits_def) 2563 apply (clarsimp simp: c_valid_cap_def cl_valid_cap_def) 2564 apply (erule (1) cap_lift_PML4Cap_Base) 2565 apply simp 2566 apply (erule_tac t = s' in ssubst) 2567 apply (simp add: heap_to_user_data_def) 2568 apply (rule conjI) 2569 apply (erule (1) setCTE_tcb_case) 2570 apply (simp add: carch_state_relation_def cmachine_state_relation_def 2571 cvariable_array_map_const_add_map_option[where f="tcb_no_ctes_proj"] 2572 fpu_null_state_heap_update_tag_disj_simps 2573 global_ioport_bitmap_heap_update_tag_disj_simps 2574 packed_heap_update_collapse_hrs) 2575 apply (clarsimp simp: cte_wp_at_ctes_of) 2576 apply ceqv 2577 apply (rule ccorres_symb_exec_l) 2578 apply (rule_tac P="ko_at' (ASIDPool pool) poolPtr" in ccorres_cross_over_guard) 2579 apply (rule ccorres_move_c_guard_cte) 2580 apply (rule ccorres_symb_exec_r) 2581 apply csymbr 2582 apply (rule ccorres_abstract_cleanup) 2583 apply (rule ccorres_Guard_Seq[where F=ArrayBounds])? 2584 apply (rule ccorres_move_c_guard_ap) 2585 apply (simp only: Kernel_C.asidLowBits_def word_sle_def) 2586 apply (rule ccorres_Guard_Seq)+ 2587 apply (rule ccorres_add_return2) 2588 apply (rule ccorres_split_nothrow_novcg) 2589 apply (rule setObjectASID_Basic_ccorres) 2590 apply ceqv 2591 apply (rule ccorres_from_vcg_throws [where P=\<top> and P'=UNIV]) 2592 apply (rule allI, rule conseqPre, vcg) 2593 apply (clarsimp simp: return_def) 2594 apply wp 2595 apply (simp add: guard_is_UNIV_def) 2596 apply (vcg) 2597 apply (rule conseqPre, vcg) 2598 apply clarsimp 2599 apply (wpsimp wp: liftM_wp) 2600 apply (wpsimp wp: getASID_wp simp: o_def inv_def) 2601 apply (clarsimp simp: empty_fail_getObject) 2602 apply (wpsimp wp: udpateCap_asidpool' hoare_vcg_all_lift hoare_vcg_imp_lift') 2603 apply vcg 2604 apply wp 2605 apply simp 2606 apply (wp getSlotCap_wp') 2607 apply simp 2608 apply (clarsimp simp: cte_wp_at_ctes_of) 2609 apply (rule conjI) 2610 apply (clarsimp dest!: asid_pool_at_ko simp: obj_at'_def inv_def) 2611 apply (rule cmap_relationE1[OF cmap_relation_cte], assumption+) 2612 apply (clarsimp simp: typ_heap_simps cap_get_tag_isCap_ArchObject2 2613 isPML4Cap'_def isCap_simps 2614 order_le_less_trans[OF word_and_le1] asid_low_bits_def 2615 dest!: ccte_relation_ccap_relation) 2616 apply (simp add: casid_pool_relation_def mask_def) 2617 apply (rule array_relation_update) 2618 apply (drule (1) asid_pool_at_rf_sr) 2619 apply (clarsimp simp: typ_heap_simps) 2620 apply (case_tac pool') 2621 apply (simp add: casid_pool_relation_def) 2622 apply (simp add: asid_low_bits_of_mask_eq mask_def asid_low_bits_def) 2623 apply (clarsimp simp: asid_map_relation_def asid_map_asid_map_vspace_lift 2624 asid_map_asid_map_none_def asid_map_asid_map_vspace_def 2625 asid_map_lifts[simplified asid_map_asid_map_vspace_def, simplified] 2626 cap_pml4_cap_lift 2627 split: if_splits) 2628 apply (drule_tac s=sa in cmap_relation_cte) 2629 apply (erule_tac y=ctea in cmap_relationE1, assumption) 2630 apply (clarsimp simp: ccte_relation_def ccap_relation_def map_option_Some_eq2) 2631 apply (clarsimp simp: cap_pml4_cap_lift_def dest!: cap_to_H_PML4Cap) 2632 apply (simp add: sign_extend_canonical_address) 2633 apply (drule_tac cte=cte in ctes_of_valid'[OF _ invs_valid_objs'], assumption) 2634 apply (clarsimp simp: valid_cap'_def canonical_address_page_map_l4_at'[OF _ invs_pspace_canonical']) 2635 apply (simp add: asid_low_bits_def) 2636 done 2637 2638lemma pte_case_isInvalidPTE: 2639 "(case pte of InvalidPTE \<Rightarrow> P | _ \<Rightarrow> Q) 2640 = (if isInvalidPTE pte then P else Q)" 2641 by (cases pte, simp_all add: isInvalidPTE_def) 2642 2643lemma invalidatePageStructureCacheASID_ccorres: 2644 "ccorres dc xfdc \<top> (UNIV \<inter> \<lbrace>\<acute>root = vspace\<rbrace> \<inter> \<lbrace>\<acute>asid = asid\<rbrace>) [] 2645 (invalidatePageStructureCacheASID vspace asid) 2646 (Call invalidatePageStructureCacheASID_'proc)" 2647 apply (cinit lift: root_' asid_') 2648 apply (ctac add: invalidateLocalPageStructureCacheASID_ccorres) 2649 by simp 2650 2651lemma ccap_relation_page_table_mapped_asid: 2652 "ccap_relation (ArchObjectCap (PageTableCap p (Some (asid, vspace)))) cap 2653 \<Longrightarrow> asid = capPTMappedASID_CL (cap_page_table_cap_lift cap)" 2654 by (frule cap_get_tag_isCap_unfolded_H_cap) 2655 (clarsimp simp: cap_page_table_cap_lift ccap_relation_def cap_to_H_def split: if_splits) 2656 2657lemma performPageTableInvocationMap_ccorres: 2658 "ccorres (K (K \<bottom>) \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_') 2659 (cte_at' ctSlot) 2660 (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> 2661 \<inter> \<lbrace>\<acute>root___ptr_to_struct_pml4e_C = Ptr vspace\<rbrace>) 2662 [] 2663 (liftE (performPageTableInvocation (PageTableMap cap ctSlot pde pdSlot vspace))) 2664 (Call performX86PageTableInvocationMap_'proc)" 2665 apply (simp only: liftE_liftM ccorres_liftM_simp) 2666 apply (cinit lift: cap_' ctSlot_' pde_' pdSlot_' root___ptr_to_struct_pml4e_C_') 2667 apply (ctac (no_vcg)) 2668 apply (rule ccorres_split_nothrow) 2669 apply simp 2670 apply (erule storePDE_Basic_ccorres) 2671 apply ceqv 2672 apply (rule ccorres_cases[where P="\<exists>p a v. cap = ArchObjectCap (PageTableCap p (Some (a, v)))" and H=\<top> and H'=UNIV]; 2673 clarsimp split: capability.splits arch_capability.splits simp: ccorres_fail) 2674 apply csymbr 2675 apply csymbr 2676 apply (rule ccorres_add_return2) 2677 apply (rule ccorres_split_nothrow_novcg) 2678 apply (frule ccap_relation_page_table_mapped_asid) 2679 apply simp 2680 apply (rule ccorres_call[where xf'=xfdc, OF invalidatePageStructureCacheASID_ccorres]; simp) 2681 apply ceqv 2682 apply (rule_tac P=\<top> and P'=UNIV in ccorres_from_vcg_throws) 2683 apply (rule allI, rule conseqPre, vcg) 2684 apply (clarsimp simp: return_def) 2685 apply wp 2686 apply (simp add: guard_is_UNIV_def) 2687 apply (clarsimp, wp) 2688 apply vcg 2689 apply wp 2690 apply (clarsimp simp: cap_get_tag_isCap_unfolded_H_cap) 2691 apply simp 2692 done 2693 2694end 2695 2696end 2697