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 CSpace_RAB_C 12imports CSpaceAcc_C "CLib.MonadicRewrite_C" 13begin 14 15context kernel 16begin 17 18abbreviation 19 "rab_xf \<equiv> (liftxf errstate resolveAddressBits_ret_C.status_C 20 (\<lambda>v. (resolveAddressBits_ret_C.slot_C v, bitsRemaining_C v)) 21 ret__struct_resolveAddressBits_ret_C_')" 22 23lemma rab_failure_case_ccorres: 24 fixes v :: "machine_word" and ist :: "cstate \<Rightarrow> cstate" and f :: int 25 defines "call_part \<equiv> (call ist f (\<lambda>s t. s\<lparr>globals := globals t\<rparr>) 26 (\<lambda>ts s'. Basic (\<lambda>s. 27 globals_update (current_lookup_fault_'_update 28 (\<lambda>_. ret__struct_lookup_fault_C_' s')) s)))" 29 assumes spec: "\<Gamma>\<turnstile> G' call_part {s. v \<noteq> scast EXCEPTION_NONE \<and> lookup_failure_rel e v (errstate s)}" 30 and mod: "\<And>s. \<Gamma>\<turnstile> {s'. (s, s') \<in> rf_sr} call_part {s'. (s, s') \<in> rf_sr}" 31 shows "ccorres (lookup_failure_rel \<currency> r) rab_xf \<top> G' (SKIP # hs) 32 (throwError e) 33 (call_part ;; 34 \<acute>ret___struct_resolveAddressBits_ret_C :== 35 resolveAddressBits_ret_C.status_C_update (\<lambda>_. v) \<acute>ret___struct_resolveAddressBits_ret_C;; 36 return_C ret__struct_resolveAddressBits_ret_C_'_update ret___struct_resolveAddressBits_ret_C_')" 37 apply (rule ccorres_rhs_assoc)+ 38 apply (rule ccorres_symb_exec_r [where R=\<top>, OF _ spec]) 39 apply (rule ccorres_from_vcg_throws) 40 apply (simp add: throwError_def return_def) 41 apply (rule allI) 42 apply (rule conseqPre) 43 apply vcg 44 apply (auto simp add: exception_defs errstate_def)[1] 45 apply (rule conseqPre [OF mod]) 46 apply clarsimp 47 done 48 49lemma not_snd_bindE_I1: 50 "\<not> snd ((a >>=E b) s) \<Longrightarrow> \<not> snd (a s)" 51 unfolding bindE_def 52 by (erule not_snd_bindI1) 53 54lemma ccorres_remove_bind_returnOk_noguard: 55 assumes ac: "ccorres (f \<currency> r') xf P P' (SKIP # hs) a c" 56 and rr: "\<And>v s'. r' v (exvalue (xf s')) \<Longrightarrow> r (g v) (exvalue (xf s'))" 57 shows "ccorres (f \<currency> r) xf P P' (SKIP # hs) (a >>=E (\<lambda>v. returnOk (g v))) c" 58 apply (rule ccorresI') 59 apply clarsimp 60 apply (drule not_snd_bindE_I1) 61 apply (erule (4) ccorresE[OF ac]) 62 apply (clarsimp simp add: bindE_def returnOk_def NonDetMonad.lift_def bind_def return_def 63 split_def) 64 apply (rule bexI [rotated], assumption) 65 apply (simp add: throwError_def return_def unif_rrel_def 66 split: sum.splits) 67 apply (auto elim!: rr) 68 done 69 70declare isCNodeCap_CNodeCap[simp] 71 72(* MOVE *) 73lemma ccorres_gen_asm_state: 74 assumes rl: "\<And>s. P s \<Longrightarrow> ccorres r xf G G' hs a c" 75 shows "ccorres r xf (G and P) G' hs a c" 76proof (rule ccorres_guard_imp2) 77 show "ccorres r xf (G and (\<lambda>_. \<exists>s. P s)) G' hs a c" 78 apply (rule ccorres_gen_asm) 79 apply (erule exE) 80 apply (erule rl) 81 done 82next 83 fix s s' 84 assume "(s, s') \<in> rf_sr" and "(G and P) s" and "s' \<in> G'" 85 thus "(G and (\<lambda>_. \<exists>s. P s)) s \<and> s' \<in> G'" 86 by (clarsimp elim!: exI) 87qed 88 89(* MOVE, generalise *) 90lemma ccorres_req: 91 assumes rl: "\<And>s s'. \<lbrakk> (s, s') \<in> rf_sr; Q s; Q' s' \<rbrakk> \<Longrightarrow> F s s'" 92 and cc: "\<And>s s'. F s s' \<Longrightarrow> ccorres r xf P P' hs a c" 93 shows "ccorres r xf (P and Q) (P' \<inter> Collect Q') hs a c" 94 apply (rule ccorresI') 95 apply clarsimp 96 apply (frule (2) rl) 97 apply (erule (5) ccorresE [OF cc]) 98 apply (clarsimp elim!: bexI [rotated]) 99 done 100 101lemma valid_cap_cte_at': 102 "\<lbrakk>isCNodeCap cap; valid_cap' cap s'\<rbrakk> \<Longrightarrow> cte_at' (capCNodePtr cap + 2^cteSizeBits * (addr && mask (capCNodeBits cap))) s'" 103 apply (clarsimp simp: isCap_simps valid_cap'_def) 104 apply (rule real_cte_at') 105 apply (erule spec) 106 done 107 108lemma mask_64_max_word [simp]: 109 shows "mask 64 = (max_word :: machine_word)" 110 unfolding mask_def 111 by (simp add: max_word_def) 112 113declare ucast_id [simp] 114declare resolveAddressBits.simps [simp del] 115 116lemma rightsFromWord_wordFromRights: 117 "rightsFromWord (wordFromRights rghts) = rghts" 118 apply (cases rghts) 119 apply (simp add: wordFromRights_def rightsFromWord_def 120 split: if_split) 121 done 122 123lemma wordFromRights_inj: 124 "inj wordFromRights" 125 by (rule inj_on_inverseI, rule rightsFromWord_wordFromRights) 126 127lemmas wordFromRights_eq = inj_eq [OF wordFromRights_inj] 128 129lemma rightsFromWord_and: 130 "rightsFromWord (a && b) = andCapRights (rightsFromWord a) (rightsFromWord b)" 131 by (simp add: rightsFromWord_def andCapRights_def) 132 133lemma andCapRights_ac: 134 "andCapRights (andCapRights a b) c = andCapRights a (andCapRights b c)" 135 "andCapRights a b = andCapRights b a" 136 "andCapRights a (andCapRights b c) = andCapRights b (andCapRights a c)" 137 by (simp add: andCapRights_def conj_comms split: cap_rights.split)+ 138 139lemma wordFromRights_rightsFromWord: 140 "wordFromRights (rightsFromWord w) = w && mask 3" 141 apply (simp add: wordFromRights_def rightsFromWord_def 142 mask_def) 143 apply (auto simp: bin_nth_ops bin_nth_Bit0 bin_nth_Bit1 numeral_2_eq_2 144 intro!: word_eqI) 145 done 146 147 148(* FIXME: move, duplicated in CSpace_C *) 149lemma ccorres_cases: 150 assumes P: " P \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf ar axf G G' hs a b" 151 assumes notP: "\<not>P \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf ar axf H H' hs a b" 152 shows "ccorres_underlying sr \<Gamma> r xf ar axf (\<lambda>s. (P \<longrightarrow> G s) \<and> (\<not>P \<longrightarrow> H s)) 153 ({s. P \<longrightarrow> s \<in> G'} \<inter> {s. \<not>P \<longrightarrow> s \<in> H'}) 154 hs a b" 155 apply (cases P, auto simp: P notP) 156 done 157 158lemma monadic_rewrite_stateAssert: 159 "monadic_rewrite F E P (stateAssert P xs) (return ())" 160 by (simp add: stateAssert_def monadic_rewrite_def exec_get) 161 162lemma ccorres_locateSlotCap_push: 163 "ccorres_underlying sr \<Gamma> r xf ar axf P P' hs 164 (a >>=E (\<lambda>x. locateSlotCap cp n >>= (\<lambda>p. b p x))) c 165 \<Longrightarrow> (\<And>P. \<lbrace>P\<rbrace> a \<lbrace>\<lambda>_. P\<rbrace>, - ) 166 \<Longrightarrow> ccorres_underlying sr \<Gamma> r xf ar axf P P' hs 167 (locateSlotCap cp n >>= (\<lambda>p. a >>=E (\<lambda>x. b p x))) c" 168 apply (simp add: locateSlot_conv) 169 apply (rule ccorres_guard_imp2) 170 apply (rule ccorres_stateAssert) 171 apply (erule monadic_rewrite_ccorres_assemble) 172 apply (rule monadic_rewrite_bindE[OF monadic_rewrite_refl]) 173 apply (rule monadic_rewrite_transverse) 174 apply (rule monadic_rewrite_bind_head) 175 apply (rule monadic_rewrite_stateAssert) 176 apply simp 177 apply (rule monadic_rewrite_refl) 178 apply assumption 179 apply simp 180 done 181 182declare Kernel_C.cte_C_size[simp del] 183 184(* FIXME x64: redo after guard bits changes *) 185lemma resolveAddressBits_ccorres [corres]: 186 shows "ccorres (lookup_failure_rel \<currency> 187 (\<lambda>(cte, bits) (cte', bits'). cte' = Ptr cte \<and> bits = unat bits' \<and> bits'\<le> 64)) rab_xf 188 (valid_pspace' and valid_cap' cap' 189 and K (guard' \<le> 64)) 190 ({s. ccap_relation cap' (nodeCap_' s)} \<inter> 191 {s. capptr_' s = cptr'} \<inter> {s. unat (n_bits_' s) = guard'}) [] 192 (resolveAddressBits cap' cptr' guard') (Call resolveAddressBits_'proc)" 193 (is "ccorres ?rvr rab_xf ?P ?P' [] ?rab ?rab'") 194proof (cases "isCNodeCap cap'") 195 case False 196 197 note Collect_const [simp del] 198 199 show ?thesis using False 200 apply (cinit' lift: nodeCap_' capptr_' n_bits_') 201 apply csymbr+ 202 \<comment> \<open>Exception stuff\<close> 203 apply (rule ccorres_split_throws) 204 apply (simp add: Collect_const cap_get_tag_isCap isCap_simps ccorres_cond_iffs 205 resolveAddressBits.simps scast_id) 206 apply (rule ccorres_from_vcg_throws [where P = \<top> and P' = UNIV]) 207 apply (rule allI) 208 apply (rule conseqPre) 209 apply (simp add: throwError_def return_def split) 210 apply vcg 211 apply (clarsimp simp add: exception_defs lookup_fault_lift_def) 212 apply (simp split: if_split) 213 apply (vcg strip_guards=true) 214 apply (clarsimp simp: cap_get_tag_isCap isCap_simps) 215 done 216next 217 case True 218 219 note word_neq_0_conv [simp del] 220 221 from True show ?thesis 222 apply - 223 apply (cinit' simp add: whileAnno_def ucast_id) 224 \<comment> \<open>This is done here as init lift usually throws away the relationship between nodeCap_' s and nodeCap. Normally 225 this OK, but the induction messes with everything :(\<close> 226 apply (rule ccorres_abstract [where xf' = nodeCap_']) 227 apply ceqv 228 apply (rename_tac "nodeCap") 229 apply (rule ccorres_abstract [where xf' = n_bits_']) 230 apply ceqv 231 apply (rename_tac "n_bits") 232 apply (rule ccorres_abstract [where xf' = capptr_']) 233 apply ceqv 234 apply (rename_tac "capptr") 235 apply (rule_tac P = "capptr = cptr' \<and> ccap_relation cap' nodeCap" in ccorres_gen_asm2) 236 apply (erule conjE) 237 apply (erule_tac t = capptr in ssubst) 238 apply csymbr+ 239 apply (simp add: cap_get_tag_isCap split del: if_split) 240 apply (thin_tac "ret__unsigned_longlong = X" for X) 241 apply (rule ccorres_split_throws [where P = "?P"]) 242 apply (rule_tac G' = "\<lambda>w_rightsMask. ({s. nodeCap_' s = nodeCap} 243 \<inter> {s. unat (n_bits_' s) = guard'})" 244 in ccorres_abstract [where xf' = w_rightsMask_']) 245 apply (rule ceqv_refl) 246 apply (rule_tac r' = "?rvr" in 247 ccorres_rel_imp [where xf' = rab_xf]) 248 defer 249 apply (case_tac x) 250 apply clarsimp 251 apply clarsimp 252 apply (rule_tac I = "{s. cap_get_tag (nodeCap_' s) = scast cap_cnode_cap}" 253 in HoarePartial.While [unfolded whileAnno_def, OF subset_refl]) 254 apply (vcg strip_guards=true) \<comment> \<open>takes a while\<close> 255 apply clarsimp 256 apply simp 257 apply (clarsimp simp: cap_get_tag_isCap to_bool_def) 258 \<comment> \<open>Main thm\<close> 259 proof (induct cap' cptr' guard' rule: resolveAddressBits.induct [case_names ind]) 260 case (ind cap cptr guard) 261 262 note conj_refl = conjI [OF refl refl] 263 have imp_rem: "\<And>P X. P \<Longrightarrow> P \<and> (P \<longrightarrow> X = X)" by clarsimp 264 have imp_rem': "\<And>P R X. P \<and> R \<Longrightarrow> P \<and> R \<and> (P \<and> R \<longrightarrow> X = X)" by clarsimp 265 note conj_refl_r = conjI [OF _ refl] 266 267 have getSlotCap_in_monad: 268 "\<And>a b p rs s. ((a, b) \<in> fst (getSlotCap p s)) = 269 (option_map cteCap (ctes_of s p) = Some a 270 \<and> b = s)" 271 apply (simp add: getSlotCap_def return_def bind_def objBits_simps split_def) 272 apply rule 273 apply (clarsimp simp: in_getCTE_cte_wp_at' cte_wp_at_ctes_of) 274 apply clarsimp 275 apply (subgoal_tac "cte_wp_at' ((=) z) p s") 276 apply (clarsimp simp: getCTE_def cte_wp_at'_def) 277 apply (simp add: cte_wp_at_ctes_of) 278 done 279 280 note ih = ind.hyps[simplified, simplified in_monad 281 getSlotCap_in_monad locateSlot_conv stateAssert_def, simplified] 282 283 have gsCNodes: "\<And>s bits p x P Q. bits = capCNodeBits cap \<Longrightarrow> capCNodeBits cap < 64 \<Longrightarrow> 284 (case gsCNodes (s \<lparr> gsCNodes := [p \<mapsto> bits ] \<rparr>) p of None \<Rightarrow> False 285 | Some n \<Rightarrow> ((n = capCNodeBits cap \<or> Q n)) 286 \<and> (x && mask bits :: machine_word) < 2 ^ n) \<or> P" 287 by (clarsimp simp: word_size and_mask_less_size) 288 289 have case_into_if: 290 "\<And>c f g. (case c of CNodeCap _ _ _ _ \<Rightarrow> f | _ \<Rightarrow> g) = (if isCNodeCap c then f else g)" 291 by (case_tac c, simp_all add: isCap_simps) 292 293 note [split del] = if_split 294 295 have gbD: "\<And>guardBits cap cap'. \<lbrakk> guardBits = capCNodeGuardSize_CL (cap_cnode_cap_lift cap'); 296 ccap_relation cap cap'; isCNodeCap cap \<rbrakk> 297 \<Longrightarrow> unat guardBits = capCNodeGuardSize cap \<and> capCNodeGuardSize cap < 64" 298 apply (simp add: cap_get_tag_isCap[symmetric]) 299 apply (frule(1) cap_get_tag_CNodeCap [THEN iffD1]) 300 apply simp 301 apply (simp add: cap_cnode_cap_lift_def cap_lift_cnode_cap) 302 apply (rule order_le_less_trans, rule word_le_nat_alt[THEN iffD1], 303 rule word_and_le1) 304 apply (simp add: mask_def) 305 done 306 307 have cgD: "\<And>capGuard cap cap'. \<lbrakk> capGuard = capCNodeGuard_CL (cap_cnode_cap_lift cap'); 308 ccap_relation cap cap'; isCNodeCap cap \<rbrakk> \<Longrightarrow> capGuard = capCNodeGuard cap" 309 apply (frule cap_get_tag_CNodeCap [THEN iffD1]) 310 apply (simp add: cap_get_tag_isCap) 311 apply simp 312 done 313 314 have rbD: "\<And>radixBits cap cap'. \<lbrakk> radixBits = capCNodeRadix_CL (cap_cnode_cap_lift cap'); 315 ccap_relation cap cap'; isCNodeCap cap \<rbrakk> 316 \<Longrightarrow> unat radixBits = capCNodeBits cap \<and> capCNodeBits cap < 64" 317 apply (simp add: cap_get_tag_isCap[symmetric]) 318 apply (frule(1) cap_get_tag_CNodeCap [THEN iffD1]) 319 apply simp 320 apply (simp add: cap_cnode_cap_lift_def cap_lift_cnode_cap) 321 apply (rule order_le_less_trans, rule word_le_nat_alt[THEN iffD1], 322 rule word_and_le1) 323 apply (simp add: mask_def) 324 done 325 326 have rxgd: 327 "\<And>cap cap'. \<lbrakk> ccap_relation cap cap'; isCNodeCap cap \<rbrakk> 328 \<Longrightarrow> unat (capCNodeRadix_CL (cap_cnode_cap_lift cap') 329 + capCNodeGuardSize_CL (cap_cnode_cap_lift cap')) 330 = unat (capCNodeRadix_CL (cap_cnode_cap_lift cap')) 331 + unat (capCNodeGuardSize_CL (cap_cnode_cap_lift cap'))" 332 apply (simp add: cap_get_tag_isCap[symmetric]) 333 apply (frule(1) cap_get_tag_CNodeCap [THEN iffD1]) 334 apply (simp add: cap_cnode_cap_lift_def cap_lift_cnode_cap) 335 apply (subst unat_plus_simple[symmetric], subst no_olen_add_nat) 336 apply (rule order_le_less_trans, rule add_le_mono) 337 apply (rule word_le_nat_alt[THEN iffD1], rule word_and_le1)+ 338 apply (simp add: mask_def) 339 done 340 341 (* Move outside this context? *) 342 note cap_simps = rxgd cgD [OF refl] 343 rbD [OF refl, THEN conjunct1] rbD [OF refl, THEN conjunct2] 344 gbD [OF refl, THEN conjunct1] gbD [OF refl, THEN conjunct2] 345 346 have cond1: "\<And>(nb :: machine_word) guardBits capGuard. 347 \<lbrakk>unat nb = guard; unat guardBits = capCNodeGuardSize cap; capGuard = capCNodeGuard cap; 348 guard \<le> 64\<rbrakk> 349 \<Longrightarrow> \<forall>s s'. 350 (s, s') \<in> rf_sr \<and> True \<and> True \<longrightarrow> 351 (\<not> (capCNodeGuardSize cap \<le> guard \<and> 352 (cptr >> guard - capCNodeGuardSize cap) && 353 mask (capCNodeGuardSize cap) = 354 capCNodeGuard cap)) = 355 (s' \<in> \<lbrace>nb < guardBits \<or> 356 (cptr >> unat (nb - guardBits && 0x3F)) && 357 2 ^ unat guardBits - 1 \<noteq> capGuard\<rbrace>)" 358 apply (subst not_le [symmetric]) 359 apply (clarsimp simp: mask_def unat_of_nat Collect_const_mem) 360 apply (cases "capCNodeGuardSize cap = 0") 361 apply (simp add: word_le_nat_alt) 362 apply (subgoal_tac "(0x3F :: machine_word) = mask 6") 363 apply (erule ssubst [where t = "0x3F"]) 364 apply (simp add: less_mask_eq word_less_nat_alt word_le_nat_alt) 365 apply (subst imp_cong) 366 apply (rule refl) 367 prefer 2 368 apply (rule refl) 369 apply (subst less_mask_eq) 370 apply (simp add: word_less_nat_alt word_le_nat_alt unat_sub) 371 apply (simp add: word_less_nat_alt word_le_nat_alt unat_sub) 372 apply (simp add: mask_def) 373 done 374 375 have cond2: "\<And>nb (radixBits :: machine_word) (guardBits :: machine_word). 376 \<lbrakk> unat nb = guard; unat radixBits = capCNodeBits cap; capCNodeBits cap < 64; capCNodeGuardSize cap < 64; 377 unat guardBits = capCNodeGuardSize cap \<rbrakk> \<Longrightarrow> 378 \<forall>s s'. (s, s') \<in> rf_sr \<and> True \<and> True \<longrightarrow> 379 (guard < capCNodeBits cap + capCNodeGuardSize cap) = (s' \<in> \<lbrace>nb < radixBits + guardBits\<rbrace>)" 380 by (simp add: Collect_const_mem word_less_nat_alt unat_word_ariths) 381 382 have cond3: "\<And>nb (radixBits :: machine_word) (guardBits :: machine_word). 383 \<lbrakk> unat nb = guard; unat radixBits = capCNodeBits cap; capCNodeBits cap < 64; capCNodeGuardSize cap < 64; 384 unat guardBits = capCNodeGuardSize cap; 385 \<not> guard < capCNodeBits cap + capCNodeGuardSize cap \<rbrakk> \<Longrightarrow> 386 \<forall>s s'. (s, s') \<in> rf_sr \<and> True \<and> True \<longrightarrow> 387 (guard = capCNodeBits cap + capCNodeGuardSize cap) = (s' \<in> \<lbrace>nb \<le> radixBits + guardBits\<rbrace>)" 388 by (simp add: Collect_const_mem word_le_nat_alt unat_word_ariths) 389 390 have cond4: 391 "\<And>rva nodeCapb ret__unsigned_long. 392 \<lbrakk> ccap_relation rva nodeCapb; ret__unsigned_long = cap_get_tag nodeCapb\<rbrakk> 393 \<Longrightarrow> \<forall>s s'. (s, s') \<in> rf_sr \<and> True \<and> True \<longrightarrow> (\<not> isCNodeCap rva) = (s' \<in> \<lbrace>ret__unsigned_long \<noteq> scast cap_cnode_cap\<rbrace>)" 394 by (simp add: cap_get_tag_isCap Collect_const_mem) 395 396 let ?p = "(capCNodePtr cap + 0x20 * ((cptr >> guard - (capCNodeBits cap + capCNodeGuardSize cap)) && 397 mask (capCNodeBits cap)))" 398 399 have n_bits_guard: "\<And>nb :: machine_word. \<lbrakk> guard \<le> 64; unat nb = guard \<rbrakk> \<Longrightarrow> unat (nb && mask 7) = guard" 400 apply (subgoal_tac "nb \<le> 64") 401 apply (clarsimp) 402 apply (rule less_mask_eq) 403 apply (erule order_le_less_trans) 404 apply simp 405 apply (simp add: word_le_nat_alt) 406 done 407 408 have mask7_eqs: 409 "\<And>cap ccap. \<lbrakk> ccap_relation cap ccap; isCNodeCap cap \<rbrakk> 410 \<Longrightarrow> (capCNodeRadix_CL (cap_cnode_cap_lift ccap) + capCNodeGuardSize_CL (cap_cnode_cap_lift ccap)) && mask 7 411 = capCNodeRadix_CL (cap_cnode_cap_lift ccap) + capCNodeGuardSize_CL (cap_cnode_cap_lift ccap)" 412 "\<And>cap ccap. \<lbrakk> ccap_relation cap ccap; isCNodeCap cap \<rbrakk> 413 \<Longrightarrow> capCNodeRadix_CL (cap_cnode_cap_lift ccap) && mask 7 = capCNodeRadix_CL (cap_cnode_cap_lift ccap)" 414 "\<And>cap ccap. \<lbrakk> ccap_relation cap ccap; isCNodeCap cap \<rbrakk> 415 \<Longrightarrow> capCNodeGuardSize_CL (cap_cnode_cap_lift ccap) && mask 7 = capCNodeGuardSize_CL (cap_cnode_cap_lift ccap)" 416 apply (frule(1) rxgd) 417 defer 418 apply (simp_all add: cap_cnode_cap_lift_def cap_get_tag_isCap[symmetric] 419 cap_lift_cnode_cap) 420 apply (rule less_mask_eq 421 | rule order_le_less_trans, (rule word_and_le1)+ 422 | simp add: mask_def)+ 423 apply (simp add: word_less_nat_alt) 424 apply (rule order_le_less_trans, rule add_le_mono) 425 apply (rule word_le_nat_alt[THEN iffD1], rule word_and_le1)+ 426 apply simp 427 done 428 429 have gm: "\<And>(nb :: machine_word) cap cap'. \<lbrakk> unat nb = guard; ccap_relation cap cap'; isCNodeCap cap \<rbrakk> 430 \<Longrightarrow> nb \<ge> capCNodeRadix_CL (cap_cnode_cap_lift cap') + 431 capCNodeGuardSize_CL (cap_cnode_cap_lift cap') 432 \<longrightarrow> unat (nb - 433 (capCNodeRadix_CL (cap_cnode_cap_lift cap') + 434 capCNodeGuardSize_CL (cap_cnode_cap_lift cap'))) 435 = guard - (capCNodeBits cap + capCNodeGuardSize cap)" 436 apply (simp add: unat_sub) 437 apply (subst unat_plus_simple[THEN iffD1]) 438 apply (subst no_olen_add_nat) 439 apply (simp add: cap_lift_cnode_cap cap_cnode_cap_lift_def 440 cap_get_tag_isCap[symmetric] mask_def) 441 apply (rule order_le_less_trans, rule add_le_mono) 442 apply (rule word_le_nat_alt[THEN iffD1], rule word_and_le1)+ 443 apply simp 444 apply (simp add: cap_simps) 445 done 446 447 note if_cong[cong] 448 show ?case 449 using ind.prems 450 apply - 451 apply (rule iffD1 [OF ccorres_expand_while_iff]) 452 apply (subst resolveAddressBits.simps) 453 apply (unfold case_into_if) 454 apply (simp add: Let_def ccorres_cond_iffs split del: if_split) 455 apply (rule ccorres_rhs_assoc)+ 456 apply (cinitlift nodeCap_' n_bits_') 457 apply (erule_tac t = nodeCapa in ssubst) 458 apply (rule ccorres_guard_imp2) 459 apply (rule ccorres_gen_asm [where P="0 < capCNodeBits cap \<or> 0 < capCNodeGuardSize cap"]) 460 apply (rule ccorres_assertE) 461 apply (csymbr | rule iffD2 [OF ccorres_seq_skip])+ 462 apply (rule ccorres_Guard_Seq)+ 463 apply csymbr 464 \<comment> \<open>handle the stateAssert in locateSlotCap very carefully\<close> 465 apply (simp(no_asm) only: liftE_bindE[where a="locateSlotCap a b" for a b]) 466 apply (rule ccorres_locateSlotCap_push[rotated]) 467 apply (simp add: unlessE_def) 468 apply (rule hoare_pre, wp, simp) 469 \<comment> \<open>Convert guardBits, radixBits and capGuard to their Haskell versions\<close> 470 apply (drule (2) cgD, drule (2) rbD, drule (2) gbD) 471 apply (elim conjE) 472 apply (rule ccorres_gen_asm [where P = "guard \<le> 64"]) 473 apply (rule ccorres_split_unless_throwError_cond [OF cond1], assumption+) 474 apply (rule rab_failure_case_ccorres, vcg, rule conseqPre, vcg) 475 apply clarsimp 476 apply (rule ccorres_locateSlotCap_push[rotated]) 477 apply (rule hoare_pre, wp whenE_throwError_wp, simp) 478 apply (rule ccorres_split_when_throwError_cond [OF cond2], assumption+) 479 apply (rule rab_failure_case_ccorres, vcg, rule conseqPre, vcg) 480 apply clarsimp 481 apply (rule ccorres_Guard_Seq)+ 482 apply csymbr 483 apply csymbr 484 apply (simp only: locateSlotCap_def Let_def if_True) 485 apply (rule ccorres_split_nothrow) 486 apply (rule locateSlotCNode_ccorres[where xf="slot_'" and xfu="slot_'_update"], 487 simp+)[1] 488 apply ceqv 489 apply (rename_tac rv slot) 490 apply (erule_tac t = slot in ssubst) 491 apply (simp del: Collect_const) 492 apply (rule ccorres_if_cond_throws [OF cond3], assumption+) 493 apply (rule ccorres_rhs_assoc)+ 494 apply csymbr+ 495 apply (rule ccorres_return_CE, simp_all)[1] 496 apply (rule ccorres_Guard_Seq) 497 apply (rule ccorres_basic_srnoop2, simp) 498 apply csymbr 499 apply (ctac pre: ccorres_liftE_Seq) 500 apply (rename_tac rva nodeCapa) 501 apply csymbr 502 apply (rule ccorres_if_cond_throws2 [OF cond4], assumption+) 503 apply (rule ccorres_rhs_assoc)+ 504 apply csymbr+ 505 apply (rule ccorres_return_CE, simp_all)[1] 506 apply (frule_tac v1 = rva in iffD1 [OF isCap_simps(4)]) 507 apply (elim exE) 508 apply (rule_tac 509 Q = "\<lambda>s. option_map cteCap (ctes_of s ?p) = Some rva" 510 and F = "\<lambda>s s'. 511 (option_map cteCap (ctes_of s ?p) = Some rva 512 \<and> (ccap_relation rva (h_val (hrs_mem (t_hrs_' (globals s'))) (Ptr &(Ptr ?p :: cte_C ptr\<rightarrow>[''cap_C'']) :: cap_C ptr))))" 513 in ccorres_req [where Q' = "\<lambda>s'. s' \<Turnstile>\<^sub>c (Ptr ?p :: cte_C ptr)"]) 514 apply (thin_tac "rva = X" for X) 515 apply (clarsimp simp: h_t_valid_clift_Some_iff typ_heap_simps) 516 apply (rule ccte_relation_ccap_relation) 517 apply (erule (2) rf_sr_cte_relation) 518 apply (elim conjE) 519 apply (rule_tac nodeCap1 = "nodeCapa" in ih, 520 (simp | rule conjI refl gsCNodes)+)[1] 521 apply (clarsimp simp: cte_level_bits_def field_simps isCap_simps, fast) 522 apply (rule refl) 523 apply assumption 524 apply assumption 525 apply assumption 526 apply vcg 527 apply (simp add: getSlotCap_def imp_conjR) 528 apply (wp getCTE_ctes_of | (wp_once hoare_drop_imps))+ 529 apply (clarsimp simp: Collect_const_mem if_then_simps lookup_fault_lifts cong: imp_cong conj_cong) 530 apply vcg 531 apply (vcg strip_guards=true) 532 apply (simp add: locateSlot_conv) 533 apply wp 534 apply vcg 535 apply (vcg strip_guards=true) 536 apply (vcg strip_guards=true) 537 apply (rule conjI) 538 \<comment> \<open>Haskell guard\<close> 539 apply (thin_tac "unat n_bits = guard") 540 apply (clarsimp simp del: imp_disjL) \<comment> \<open>take a while\<close> 541 apply (intro impI conjI allI) 542 apply fastforce 543 apply clarsimp 544 apply arith 545 apply (clarsimp simp: isCap_simps cte_level_bits_def 546 option.split[where P="\<lambda>x. x"]) 547 apply (clarsimp simp: isCap_simps valid_cap_simps' cte_level_bits_def cteSizeBits_def 548 real_cte_at') 549 apply (clarsimp simp: isCap_simps valid_cap'_def) 550 \<comment> \<open>C guard\<close> 551 apply (frule (1) cgD [OF refl], frule (1) rbD [OF refl], frule (1) gbD [OF refl]) 552 apply (simp add: Collect_const_mem cap_get_tag_isCap exception_defs lookup_fault_lifts 553 n_bits_guard mask7_eqs word_le_nat_alt word_less_nat_alt gm) 554 apply (elim conjE) 555 apply (frule rf_sr_cte_at_valid [where p = 556 "cte_Ptr (capCNodePtr cap + 2^cteSizeBits * ((cptr >> guard - (capCNodeBits cap + capCNodeGuardSize cap)) && mask (capCNodeBits cap)))", rotated]) 557 apply simp 558 apply (erule (1) valid_cap_cte_at') 559 apply (simp add: objBits_defs) 560 apply (frule(2) gm) 561 apply (simp add: word_less_nat_alt word_le_nat_alt less_mask_eq) 562 apply (intro impI conjI allI, simp_all) 563 apply (simp add: cap_simps) 564 apply (frule iffD1 [OF cap_get_tag_CNodeCap]) 565 apply (simp add: cap_get_tag_isCap) 566 apply (erule ssubst [where t = cap]) 567 apply simp 568 apply (simp add: mask_def) 569 apply (subgoal_tac "capCNodeBits cap \<noteq> 0") 570 apply (clarsimp simp: linorder_not_less cap_simps) 571 apply (clarsimp simp: isCap_simps valid_cap'_def) 572 apply (clarsimp simp: linorder_not_less cap_simps) 573 apply (clarsimp simp: isCap_simps valid_cap'_def) 574 apply (clarsimp simp: linorder_not_less cap_simps) 575 apply (clarsimp simp: isCap_simps valid_cap'_def) 576 apply arith 577 apply (subgoal_tac "(0x3F :: machine_word) = mask 6") 578 apply (erule ssubst [where t = "0x3F"]) 579 apply (subst word_mod_2p_is_mask [symmetric]) 580 apply simp 581 apply (simp add: unat_word_ariths) 582 apply (simp add: mask_def) 583 done 584 qed 585qed 586 587abbreviation 588 "lookupSlot_xf \<equiv> liftxf errstate lookupSlot_ret_C.status_C 589 lookupSlot_ret_C.slot_C ret__struct_lookupSlot_ret_C_'" 590 591 592lemma rightsFromWord_spec: 593 shows "\<forall>s. \<Gamma> \<turnstile> {s} \<acute>ret__struct_seL4_CapRights_C :== PROC rightsFromWord(\<acute>w) 594 \<lbrace>seL4_CapRights_lift \<acute>ret__struct_seL4_CapRights_C = cap_rights_from_word_canon \<^bsup>s\<^esup>w \<rbrace>" 595 apply vcg 596 apply (simp add: seL4_CapRights_lift_def nth_shiftr mask_shift_simps nth_shiftr 597 cap_rights_from_word_canon_def from_bool_def word_and_1 eval_nat_numeral 598 word_sless_def word_sle_def) 599 done 600 601 602abbreviation 603 "lookupSlot_rel' \<equiv> \<lambda>(cte, rm) (cte', rm'). cte' = Ptr cte \<and> rm = cap_rights_to_H (seL4_CapRights_lift rm')" 604 605(* MOVE *) 606lemma cap_rights_to_H_from_word_canon [simp]: 607 "cap_rights_to_H (cap_rights_from_word_canon wd) = rightsFromWord wd" 608 unfolding cap_rights_from_word_def rightsFromWord_def 609 apply (simp add: cap_rights_from_word_canon_def) 610 apply (simp add: cap_rights_to_H_def) 611 done 612 613(* MOVE *) 614lemma to_bool_false [simp]: 615 "to_bool false = False" 616 unfolding to_bool_def false_def 617 by simp 618 619(* MOVE *) 620lemma tcb_aligned': 621 "tcb_at' t s \<Longrightarrow> is_aligned t tcbBlockSizeBits" 622 apply (drule obj_at_aligned') 623 apply (simp add: objBits_simps) 624 apply (simp add: objBits_simps) 625 done 626 627lemma tcb_ptr_to_ctcb_ptr_mask [simp]: 628 assumes tcbat: "tcb_at' thread s" 629 shows "ptr_val (tcb_ptr_to_ctcb_ptr thread) && ~~ mask tcbBlockSizeBits = thread" 630proof - 631 have "thread + ctcb_offset && ~~ mask tcbBlockSizeBits = thread" 632 proof (rule add_mask_lower_bits) 633 show "is_aligned thread tcbBlockSizeBits" using tcbat by (rule tcb_aligned') 634 qed (auto simp: word_bits_def ctcb_offset_defs objBits_defs) 635 thus ?thesis 636 unfolding tcb_ptr_to_ctcb_ptr_def ctcb_offset_def 637 by (simp add: mask_def) 638qed 639 640abbreviation 641 "lookupSlot_raw_xf \<equiv> 642 liftxf errstate lookupSlot_raw_ret_C.status_C 643 lookupSlot_raw_ret_C.slot_C 644 ret__struct_lookupSlot_raw_ret_C_'" 645 646definition 647 lookupSlot_raw_rel :: "machine_word \<Rightarrow> cte_C ptr \<Rightarrow> bool" 648where 649 "lookupSlot_raw_rel \<equiv> \<lambda>slot slot'. slot' = cte_Ptr slot" 650 651lemma lookupSlotForThread_ccorres': 652 "ccorres (lookup_failure_rel \<currency> lookupSlot_raw_rel) lookupSlot_raw_xf 653 (valid_pspace' and tcb_at' thread) 654 ({s. capptr_' s = cptr} \<inter> {s. thread_' s = tcb_ptr_to_ctcb_ptr thread}) [] 655 (lookupSlotForThread thread cptr) (Call lookupSlot_'proc)" 656 apply (cinit lift: capptr_' thread_' 657 simp add: getThreadCSpaceRoot_def locateSlot_conv 658 returnOk_liftE [symmetric] split_def) 659 apply (ctac pre: ccorres_liftE_Seq) 660 apply (ctac (no_vcg) add: resolveAddressBits_ccorres) 661 apply csymbr+ 662 apply (ctac add: ccorres_return_CE) 663 apply csymbr+ 664 apply (ctac add: ccorres_return_C_errorE) 665 apply wp+ 666 apply vcg 667 apply (rule conjI) 668 apply (clarsimp simp add: conj_comms word_size tcbSlots Kernel_C.tcbCTable_def) 669 apply (rule conjI) 670 apply fastforce 671 apply (erule tcb_at_cte_at') 672 apply (clarsimp simp add: Collect_const_mem errstate_def tcbSlots 673 Kernel_C.tcbCTable_def word_size lookupSlot_raw_rel_def 674 word_sle_def 675 split del: if_split) 676 done 677 678lemma lookupSlotForThread_ccorres[corres]: 679 "ccorres (lookup_failure_rel \<currency> lookupSlot_raw_rel) lookupSlot_raw_xf 680 (invs' and tcb_at' thread) 681 (UNIV \<inter> {s. capptr_' s = cptr} \<inter> {s. thread_' s = tcb_ptr_to_ctcb_ptr thread}) [] 682 (lookupSlotForThread thread cptr) (Call lookupSlot_'proc)" 683 apply (rule ccorres_guard_imp2, rule lookupSlotForThread_ccorres') 684 apply fastforce 685 done 686 687end 688end 689