1(* 2 * Copyright 2014, NICTA 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(NICTA_GPL) 9 *) 10 11theory Retype_AC 12imports CNode_AC 13begin 14 15context begin interpretation Arch . (*FIXME: arch_split*) 16 17(* put in here that we own the region mentioned in the invocation *) 18definition 19 authorised_untyped_inv :: "'a PAS \<Rightarrow> Invocations_A.untyped_invocation \<Rightarrow> bool" 20where 21 "authorised_untyped_inv aag ui \<equiv> case ui of 22 Invocations_A.untyped_invocation.Retype src_slot reset base aligned_free_ref new_type obj_sz slots dev \<Rightarrow> 23 is_subject aag (fst src_slot) \<and> (0::word32) < of_nat (length slots) \<and> 24 (\<forall>x\<in>set (retype_addrs aligned_free_ref new_type (length slots) obj_sz). is_subject aag x) \<and> 25 (\<forall>x\<in>{aligned_free_ref..aligned_free_ref + of_nat (length slots)*2^(obj_bits_api new_type obj_sz) - 1}. is_subject aag x) \<and> 26 new_type \<noteq> ArchObject ASIDPoolObj \<and> 27 (\<forall>x\<in>set slots. is_subject aag (fst x))" 28 29subsection{* invoke *} 30 31lemma create_cap_integrity: 32 "\<lbrace>integrity aag X st and K (is_subject aag (fst (fst ref)))\<rbrace> 33 create_cap tp sz p dev ref 34 \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>" 35 apply (simp add: create_cap_def split_def) 36 apply (wp set_cap_integrity_autarch[unfolded pred_conj_def K_def] 37 create_cap_extended.list_integ_lift 38 create_cap_list_integrity 39 set_original_integrity_autarch 40 | simp add: set_cdt_def)+ 41 apply (simp add: integrity_def) 42 apply (clarsimp simp: integrity_cdt_def) 43 done 44 45crunch inv[wp]: reserve_region P 46 47lemma mol_respects: 48 "\<lbrace>\<lambda>ms. integrity aag X st (s\<lparr>machine_state := ms\<rparr>)\<rbrace> machine_op_lift mop \<lbrace>\<lambda>a b. integrity aag X st (s\<lparr>machine_state := b\<rparr>)\<rbrace>" 49 unfolding machine_op_lift_def 50 apply (simp add: machine_rest_lift_def split_def) 51 apply wp 52 apply (clarsimp simp: integrity_def) 53 done 54 55lemma ptr_range_memI: 56 "is_aligned p n \<Longrightarrow> p \<in> ptr_range p n" 57 unfolding ptr_range_def 58 apply (erule is_aligned_get_word_bits) 59 apply (drule (1) base_member_set) 60 apply (simp add: field_simps) 61 apply simp 62 done 63 64lemma ptr_range_add_memI: 65 "\<lbrakk> is_aligned (p :: 'a :: len word) n; k < 2 ^ n \<rbrakk> \<Longrightarrow> (p + k) \<in> ptr_range p n" 66 unfolding ptr_range_def 67 apply (erule is_aligned_get_word_bits) 68 apply clarsimp 69 apply (rule conjI) 70 apply (erule (1) is_aligned_no_wrap') 71 apply (subst p_assoc_help, rule word_plus_mono_right) 72 apply simp 73 apply (erule is_aligned_no_overflow') 74 apply (subgoal_tac "2 ^ n = (0 :: 'a word)") 75 apply simp 76 apply (simp add: word_bits_conv) 77 done 78 79lemma storeWord_integrity_autarch: 80 "\<lbrace>\<lambda>ms. integrity aag X st (s\<lparr>machine_state := ms\<rparr>) \<and> (is_aligned p 2 \<longrightarrow> (\<forall>p' \<in> ptr_range p 2. is_subject aag p'))\<rbrace> storeWord p v \<lbrace>\<lambda>a b. integrity aag X st (s\<lparr>machine_state := b\<rparr>)\<rbrace>" 81 unfolding storeWord_def 82 apply wp 83 apply (auto simp: integrity_def is_aligned_mask [symmetric] intro!: trm_lrefl ptr_range_memI ptr_range_add_memI) 84 done 85 86lemma word_minus_1: 87 "x + (0xFFFFFFFF::word32) = x - 1" 88 by simp 89 90lemma Suc_0_lt_cases: 91 "\<lbrakk>(x = 0 \<Longrightarrow> False); (x = 1 \<Longrightarrow> False)\<rbrakk> \<Longrightarrow> Suc 0 < x" 92 apply (rule classical) 93 apply (auto simp add: not_less le_Suc_eq) 94 done 95 96lemmas upto_enum_step_shift_red = 97 upto_enum_step_shift_red[where 'a=32, simplified, simplified word_bits_def[symmetric, simplified]] 98 99lemma clearMemory_respects: 100 "\<lbrace>\<lambda> a. integrity aag X st (s\<lparr>machine_state := a\<rparr>) \<and> 101 is_aligned ptr sz \<and> sz < word_bits \<and> 2 \<le> sz \<and> 102 (\<forall> y\<in>ptr_range ptr sz. is_subject aag y)\<rbrace> 103 clearMemory ptr (2 ^ sz) 104 \<lbrace>\<lambda>rv a. integrity aag X st (s\<lparr>machine_state := a\<rparr>)\<rbrace>" 105 unfolding clearMemory_def 106 apply (rule hoare_pre) 107 apply (simp add: split_def cleanCacheRange_PoU_def) 108 apply wp 109 apply (simp add: cleanByVA_PoU_def) 110 apply (wp mol_respects) 111 apply (rule_tac Q="\<lambda> x ms. integrity aag X st (s\<lparr>machine_state := ms\<rparr>) \<and> (\<forall> y\<in> set [ptr , ptr + 4 .e. ptr + of_nat (2 ^ sz) - 1]. (is_aligned y 2 \<longrightarrow> (\<forall> z \<in> ptr_range y 2. is_subject aag z)))" in hoare_strengthen_post) 112 apply(wp mapM_x_wp' storeWord_integrity_autarch | simp add: no_irq_storeWord word_size_def)+ 113 apply(clarsimp simp: upto_enum_step_shift_red[where us=2, simplified] word_bits_def) 114 apply(erule bspec) 115 apply(erule subsetD[rotated]) 116 apply(rule ptr_range_subset) 117 apply assumption 118 apply(rule is_aligned_mult_triv2[where n=2, simplified]) 119 apply assumption 120 apply (auto simp: word_bits_def 121 intro: word_less_power_trans_ofnat[where k=2, simplified]) 122 done 123 124crunch integrity_autarch: set_pd "integrity aag X st" 125 (wp: crunch_wps simp: crunch_simps) 126 127lemma store_pde_integrity: 128 "\<lbrace>integrity aag X st and K (is_subject aag (p && ~~ mask pd_bits))\<rbrace> 129 store_pde p pde 130 \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>" 131 apply(simp add: store_pde_def) 132 apply(wp set_pd_integrity_autarch) 133 apply(auto) 134 done 135 136(* Borrowed from part of copy_global_mappings_nonempty_table in Untyped_R.thy *) 137lemma copy_global_mappings_index_subset: 138 "set [kernel_base >> 20.e.2 ^ (pd_bits - 2) - 1] \<subseteq> {x. \<exists>y. x = y >> 20}" 139 apply clarsimp 140 apply (rule_tac x="x << 20" in exI) 141 apply (subst shiftl_shiftr1, simp) 142 apply (simp add: word_size) 143 apply (rule sym, rule less_mask_eq) 144 apply (simp add: minus_one_helper5 pd_bits_def pageBits_def) 145 done 146 147lemma copy_global_mappings_integrity: 148 "is_aligned x pd_bits \<Longrightarrow> 149 \<lbrace>integrity aag X st and K (is_subject aag x)\<rbrace> 150 copy_global_mappings x 151 \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>" 152 apply (rule hoare_gen_asm) 153 apply (simp add: copy_global_mappings_def) 154 apply (wp mapM_x_wp[OF _ subset_refl] store_pde_integrity) 155 apply (drule subsetD[OF copy_global_mappings_index_subset]) 156 apply (fastforce simp: pd_shifting') 157 apply wpsimp+ 158 done 159 160lemma dmo_mol_respects: 161 "\<lbrace>integrity aag X st\<rbrace> do_machine_op (machine_op_lift mop) \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>" 162 unfolding do_machine_op_def 163 apply (simp add: split_def) 164 apply wp 165 apply clarsimp 166 apply (erule use_valid) 167 apply (wp mol_respects) 168 apply simp 169 done 170 171lemma dmo_bind_valid: 172 "\<lbrace>P\<rbrace> do_machine_op (a >>= b) \<lbrace>Q\<rbrace> = \<lbrace>P\<rbrace> do_machine_op a >>= (\<lambda>rv. do_machine_op (b rv)) \<lbrace>Q\<rbrace>" 173 by (fastforce simp: do_machine_op_def gets_def get_def select_f_def modify_def put_def return_def bind_def valid_def) 174 175lemma dmo_bind_valid': 176 "\<lbrace>P\<rbrace> a >>= (\<lambda>rv. do_machine_op (b rv >>= c rv)) \<lbrace>Q\<rbrace> 177 = \<lbrace>P\<rbrace> a >>= (\<lambda>rv. do_machine_op (b rv) >>= (\<lambda>rv'. do_machine_op (c rv rv'))) \<lbrace>Q\<rbrace>" 178 by (fastforce simp: do_machine_op_def gets_def get_def select_f_def modify_def put_def return_def bind_def valid_def) 179 180lemma dmo_mapM_wp: 181 assumes x: "\<And>x. x \<in> S \<Longrightarrow> \<lbrace>P\<rbrace> do_machine_op (f x) \<lbrace>\<lambda>rv. P\<rbrace>" 182 shows "set xs \<subseteq> S \<Longrightarrow> \<lbrace>P\<rbrace> do_machine_op (mapM f xs) \<lbrace>\<lambda>rv. P\<rbrace>" 183 apply (induct xs) 184 apply (simp add: mapM_def sequence_def) 185 apply (simp add: mapM_Cons dmo_bind_valid dmo_bind_valid') 186 apply (wpsimp | rule x)+ 187 done 188 189lemma dmo_mapM_x_wp: 190 assumes x: "\<And>x. x \<in> S \<Longrightarrow> \<lbrace>P\<rbrace> do_machine_op (f x) \<lbrace>\<lambda>rv. P\<rbrace>" 191 shows "set xs \<subseteq> S \<Longrightarrow> \<lbrace>P\<rbrace> do_machine_op (mapM_x f xs) \<lbrace>\<lambda>rv. P\<rbrace>" 192 apply (subst mapM_x_mapM) 193 apply (simp add: do_machine_op_return_foo) 194 apply wp 195 apply (rule dmo_mapM_wp) 196 apply (rule x) 197 apply assumption+ 198 done 199 200lemmas dmo_mapM_x_wp_inv = dmo_mapM_x_wp[where S=UNIV, simplified] 201 202lemma dmo_cacheRangeOp_lift: 203 "(\<And>a b. \<lbrace>P\<rbrace> do_machine_op (oper a b) \<lbrace>\<lambda>_. P\<rbrace>) 204 \<Longrightarrow> \<lbrace>P\<rbrace> do_machine_op (cacheRangeOp oper x y z) \<lbrace>\<lambda>_. P\<rbrace>" 205 apply (simp add: cacheRangeOp_def) 206 apply (wp dmo_mapM_x_wp_inv) 207 apply (simp add: split_def)+ 208 done 209 210lemma dmo_cleanCacheRange_PoU_respects [wp]: 211 "\<lbrace>integrity aag X st\<rbrace> do_machine_op (cleanCacheRange_PoU vstart vend pstart) \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>" 212 by (simp add: cleanCacheRange_PoU_def cleanByVA_PoU_def | wp dmo_cacheRangeOp_lift dmo_mol_respects)+ 213 214lemma dmo_mapM_x_cleanCacheRange_PoU_integrity: 215 "\<lbrace>integrity aag X st\<rbrace> 216 do_machine_op 217 (mapM_x (\<lambda>x. cleanCacheRange_PoU (f x) (g x) (h x)) refs) 218 \<lbrace>\<lambda>_. integrity aag X st\<rbrace>" 219 by (wp dmo_mapM_x_wp_inv) 220 221definition word_object_size :: "apiobject_type \<Rightarrow> nat" where 222 "word_object_size aobject_type \<equiv> 223 (case aobject_type of 224 (ArchObject SmallPageObj) \<Rightarrow> 12 | 225 (ArchObject LargePageObj) \<Rightarrow> 16 | 226 (ArchObject SectionObj) \<Rightarrow> 20 | 227 (ArchObject SuperSectionObj) \<Rightarrow> 24)" 228 229lemma init_arch_objects_integrity: 230 "\<lbrace>integrity aag X st and 231 K (\<forall> x\<in>set refs. is_subject aag x) and 232 K (\<forall>ref \<in> set refs. is_aligned ref (obj_bits_api new_type obj_sz))\<rbrace> 233 init_arch_objects new_type ptr num_objects obj_sz refs 234 \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>" 235 apply(rule hoare_gen_asm)+ 236 apply(cases new_type) 237 apply(simp_all add: init_arch_objects_def split del: if_split) 238 apply(rule hoare_pre) 239 apply(wpc 240 | wp mapM_x_wp[OF _ subset_refl] 241 copy_global_mappings_integrity dmo_mapM_x_cleanCacheRange_PoU_integrity 242 | simp add: obj_bits_api_def default_arch_object_def pd_bits_def pageBits_def)+ 243 done 244 245lemma foldr_upd_app_if': "foldr (\<lambda>p ps. ps(p := f p)) as g = (\<lambda>x. if x \<in> set as then (f x) else g x)" 246 apply (induct as) 247 apply simp 248 apply simp 249 apply (rule ext) 250 apply simp 251 done 252 253 254lemma retype_region_integrity: 255 "\<lbrace>integrity aag X st and 256 K (range_cover ptr sz (obj_bits_api type o_bits) num_objects \<and> 257 (\<forall>x\<in>{ptr..(ptr && ~~ mask sz) + (2 ^ sz - 1)}. is_subject aag x))\<rbrace> 258 retype_region ptr num_objects o_bits type dev 259 \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>" 260 apply(rule hoare_gen_asm)+ 261 apply(simp only: retype_region_def retype_region_ext_extended.dxo_eq) 262 apply(simp only: retype_addrs_def retype_region_ext_def 263 foldr_upd_app_if' fun_app_def K_bind_def) 264 apply(wp) 265 apply (clarsimp simp: not_less) 266 apply (erule integrity_trans) 267 apply (clarsimp simp add: integrity_def) 268 apply(fastforce intro: tro_lrefl tre_lrefl 269 dest: retype_addrs_subset_ptr_bits[simplified retype_addrs_def] 270 simp: image_def p_assoc_help power_sub integrity_def) 271 done 272 273lemma retype_region_ret_is_subject: 274 "\<lbrace>K (range_cover ptr sz (obj_bits_api tp us) num_objects \<and> 275 (\<forall>x\<in>{ptr..(ptr && ~~ mask sz) + (2 ^ sz - 1)}. is_subject aag x))\<rbrace> 276 retype_region ptr num_objects us tp dev 277 \<lbrace>\<lambda>rv. K (\<forall> ref \<in> set rv. is_subject aag ref)\<rbrace>" 278 apply(rule hoare_gen_asm2 | rule hoare_gen_asm)+ 279 apply(rule hoare_strengthen_post) 280 apply(rule retype_region_ret) 281 apply(simp only: K_def) 282 apply(rule ballI) 283 apply(elim conjE) 284 apply(erule bspec) 285 apply(rule rev_subsetD, assumption) 286 apply(simp add: p_assoc_help del: set_map) 287 apply(rule retype_addrs_subset_ptr_bits[simplified retype_addrs_def]) 288 apply simp 289 done 290 291lemma retype_region_ret_pd_aligned: 292 "\<lbrace>K (range_cover ptr sz (obj_bits_api tp us) num_objects)\<rbrace> 293 retype_region ptr num_objects us tp dev 294 \<lbrace>\<lambda>rv. K (\<forall> ref \<in> set rv. tp = ArchObject PageDirectoryObj \<longrightarrow> is_aligned ref pd_bits)\<rbrace>" 295 apply(rule hoare_strengthen_post) 296 apply(rule hoare_weaken_pre) 297 apply(rule retype_region_aligned_for_init) 298 apply simp 299 apply (clarsimp simp: obj_bits_api_def default_arch_object_def pd_bits_def pageBits_def) 300 done 301 302declare wrap_ext_det_ext_ext_def[simp] 303 304lemma detype_integrity: 305 "\<lbrakk>integrity aag X st s; (\<forall> r\<in>refs. is_subject aag r)\<rbrakk> \<Longrightarrow> 306 integrity aag X st (detype refs s)" 307 apply (erule integrity_trans) 308 apply (auto simp: detype_def detype_ext_def integrity_def) 309 done 310 311lemma state_vrefs_detype [simp]: 312 "state_vrefs (detype R s) = (\<lambda>x. if x \<in> R then {} else state_vrefs s x)" 313 unfolding state_vrefs_def 314 apply (rule ext) 315 apply (clarsimp simp: detype_def) 316 done 317 318lemma global_refs_detype [simp]: 319 "global_refs (detype R s) = global_refs s" 320 by(simp add: detype_def) 321 322lemma thread_states_detype[simp]: 323 "thread_states (detype S s) = (\<lambda>x. if x \<in> S then {} else thread_states s x)" 324 by (rule ext, simp add: thread_states_def get_tcb_def o_def detype_def tcb_states_of_state_def) 325 326lemma thread_bound_ntfns_detype[simp]: 327 "thread_bound_ntfns (detype S s) = (\<lambda>x. if x \<in> S then None else thread_bound_ntfns s x)" 328 by (rule ext, simp add: thread_bound_ntfns_def get_tcb_def o_def detype_def tcb_states_of_state_def) 329 330lemma sta_detype: 331 "state_objs_to_policy (detype R s) \<subseteq> state_objs_to_policy s" 332 apply (clarsimp simp add: state_objs_to_policy_def state_refs_of_detype) 333 apply (erule state_bits_to_policy.induct) 334 apply (auto intro: state_bits_to_policy.intros split: if_split_asm) 335 done 336 337lemma sita_detype: 338 "state_irqs_to_policy aag (detype R s) \<subseteq> state_irqs_to_policy aag s" 339 apply (clarsimp) 340 apply (erule state_irqs_to_policy_aux.induct) 341 apply (auto simp: detype_def intro: state_irqs_to_policy_aux.intros split: if_split_asm) 342 done 343 344lemma sata_detype: 345 "state_asids_to_policy aag (detype R s) \<subseteq> state_asids_to_policy aag s" 346 apply (clarsimp) 347 apply (erule state_asids_to_policy_aux.induct) 348 apply (auto intro: state_asids_to_policy_aux.intros split: if_split_asm) 349 done 350 351(* FIXME: move *) 352lemmas pas_refined_by_subsets = pas_refined_state_objs_to_policy_subset 353 354 355lemma detype_irqs [simp]: 356 "interrupt_irq_node (detype R s) = interrupt_irq_node s" 357 unfolding detype_def by simp 358 359lemma dtsa_detype: "domains_of_state (detype R s) \<subseteq> domains_of_state s" 360by (auto simp: detype_def detype_ext_def 361 intro: domtcbs 362 elim!: domains_of_state_aux.cases 363 split: if_splits) 364 365lemma pas_refined_detype: 366 "pas_refined aag s \<Longrightarrow> pas_refined aag (detype R s)" 367 apply (rule pas_refined_by_subsets) 368 apply (blast intro!: sta_detype sata_detype sita_detype detype_irqs dtsa_detype)+ 369 done 370 371(* TODO: proof has mainly been copied from dmo_clearMemory_respects *) 372lemma dmo_freeMemory_respects: 373 "\<lbrace>integrity aag X st and 374 K (is_aligned ptr bits \<and> bits < word_bits \<and> 2 \<le> bits \<and> 375 (\<forall>p \<in> ptr_range ptr bits. is_subject aag p))\<rbrace> 376 do_machine_op (freeMemory ptr bits) \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>" 377 unfolding do_machine_op_def freeMemory_def 378 apply (simp add: split_def) 379 apply wp 380 apply clarsimp 381 apply (erule use_valid) 382 apply (wp mol_respects mapM_x_wp' storeWord_integrity_autarch) 383 apply simp 384 apply (clarsimp simp: word_size_def word_bits_def upto_enum_step_shift_red [where us=2, simplified]) 385 apply (erule bspec) 386 apply (erule set_mp [rotated]) 387 apply (rule ptr_range_subset) 388 apply simp 389 apply (simp add: is_aligned_mult_triv2 [where n = 2, simplified]) 390 apply assumption 391 apply (erule word_less_power_trans_ofnat [where k = 2, simplified]) 392 apply assumption 393 apply simp 394 apply simp 395 done 396 397lemma delete_objects_respects[wp]: 398 "\<lbrace>integrity aag X st and 399 K (is_aligned ptr bits \<and> bits < word_bits \<and> 400 2 \<le> bits \<and> (\<forall>p\<in>ptr_range ptr bits. is_subject aag p))\<rbrace> 401 delete_objects ptr bits 402 \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>" 403 apply (simp add: delete_objects_def) 404 apply (rule_tac seq_ext) 405 apply (rule hoare_triv[of P _ "%_. P" for P]) 406 apply (wp dmo_freeMemory_respects | simp)+ 407 apply (clarsimp simp: ptr_range_def intro!: detype_integrity) 408 done 409 410lemma storeWord_respects: 411 "\<lbrace>\<lambda>ms. integrity aag X st (s\<lparr>machine_state := ms\<rparr>) \<and> (\<forall>p' \<in> ptr_range p 2. aag_has_auth_to aag Write p')\<rbrace> storeWord p v \<lbrace>\<lambda>a b. integrity aag X st (s\<lparr>machine_state := b\<rparr>)\<rbrace>" 412 unfolding storeWord_def 413 apply wp 414 apply (auto simp: integrity_def is_aligned_mask [symmetric] intro!: trm_write ptr_range_memI ptr_range_add_memI) 415 done 416 417lemma dmo_clearMemory_respects': 418 "\<lbrace>integrity aag X st and K (is_aligned ptr bits \<and> bits < word_bits \<and> 2 \<le> bits \<and> (\<forall>p \<in> ptr_range ptr bits. aag_has_auth_to aag Write p))\<rbrace> 419 do_machine_op (clearMemory ptr (2 ^ bits)) 420 \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>" 421 unfolding do_machine_op_def clearMemory_def 422 apply (simp add: split_def cleanCacheRange_PoU_def) 423 apply wp 424 apply clarsimp 425 apply (erule use_valid) 426 apply wp 427 apply (simp add: cleanByVA_PoU_def) 428 apply (wp mol_respects mapM_x_wp' storeWord_respects)+ 429 apply simp 430 apply (clarsimp simp add: word_size_def word_bits_def upto_enum_step_shift_red[where us=2, simplified]) 431 apply (erule bspec) 432 apply (erule set_mp [rotated]) 433 apply (rule ptr_range_subset) 434 apply simp 435 apply (simp add: is_aligned_mult_triv2 [where n = 2, simplified]) 436 apply assumption 437 apply (erule word_less_power_trans_ofnat [where k = 2, simplified]) 438 apply assumption 439 apply simp 440 apply simp 441 done 442 443lemma integrity_work_units_completed_update[simp]: 444 "integrity aag X st (work_units_completed_update f s) = integrity aag X st s" 445 by (simp add: integrity_def) 446 447lemma reset_untyped_cap_integrity: 448 "\<lbrace>integrity aag X st and pas_refined aag 449 and valid_objs and cte_wp_at is_untyped_cap slot 450 and K (is_subject aag (fst slot))\<rbrace> 451 reset_untyped_cap slot 452 \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>" 453 apply (rule hoare_gen_asm) 454 apply (simp add: reset_untyped_cap_def) 455 apply (rule hoare_pre) 456 apply (wp set_cap_integrity_autarch dmo_clearMemory_respects' 457 | simp add: unless_def)+ 458 apply (rule valid_validE, rule_tac P="cap_aligned cap \<and> is_untyped_cap cap 459 \<and> (\<forall>r \<in> cap_range cap. aag_has_auth_to aag Write r)" in hoare_gen_asm) 460 apply (rule validE_valid, rule mapME_x_wp') 461 apply (rule hoare_pre) 462 apply (wp mapME_x_inv_wp[OF hoare_pre(2)] preemption_point_inv' 463 set_cap_integrity_autarch dmo_clearMemory_respects' | simp)+ 464 apply (clarsimp simp: cap_aligned_def is_cap_simps bits_of_def) 465 apply (subst aligned_add_aligned, assumption, rule is_aligned_shiftl, simp+) 466 apply (clarsimp simp: arg_cong2[where f="(\<le>)", OF refl reset_chunk_bits_def]) 467 apply (drule bspec, erule subsetD[rotated]) 468 apply (simp only: ptr_range_def, rule new_range_subset', 469 simp_all add: is_aligned_shiftl)[1] 470 apply (rule shiftl_less_t2n) 471 apply (rule word_of_nat_less) 472 apply simp 473 apply (simp add: word_bits_def) 474 apply clarsimp 475 apply (simp add: if_apply_def2) 476 apply (wp hoare_vcg_const_imp_lift get_cap_wp)+ 477 apply (clarsimp simp: cte_wp_at_caps_of_state) 478 apply (frule caps_of_state_valid_cap, clarsimp+) 479 apply (clarsimp simp: cap_aligned_def is_cap_simps valid_cap_simps bits_of_def 480 untyped_min_bits_def) 481 apply (frule(2) cap_cur_auth_caps_of_state) 482 apply (clarsimp simp: aag_cap_auth_def ptr_range_def aag_has_Control_iff_owns 483 pas_refined_refl) 484 done 485 486lemma bool_enum[simp]: "(\<forall>x. d = (\<not> x)) = False" "(\<forall>x. d = x) = False" 487 by blast+ 488 489lemma invoke_untyped_integrity: 490 "\<lbrace>integrity aag X st and pas_refined aag 491 and valid_objs 492 and valid_untyped_inv ui and K (authorised_untyped_inv aag ui)\<rbrace> 493 invoke_untyped ui 494 \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>" 495 apply (rule hoare_name_pre_state) 496 apply (clarsimp simp only: valid_untyped_inv_wcap) 497 apply (cases ui) 498 apply (simp add: mapM_x_def[symmetric] authorised_untyped_inv_def 499 invoke_untyped_def) 500 apply (rule hoare_pre) 501 apply (wp mapM_x_wp[OF _ subset_refl] create_cap_integrity 502 init_arch_objects_integrity retype_region_integrity 503 retype_region_ret_is_subject retype_region_ret_pd_aligned 504 set_cap_integrity_autarch hoare_vcg_if_lift 505 hoare_whenE_wp reset_untyped_cap_integrity 506 | clarsimp simp: split_paired_Ball 507 | erule in_set_zipE | blast)+ 508 apply(clarsimp simp: is_aligned_neg_mask_eq 509 ptr_range_def p_assoc_help bits_of_def 510 cte_wp_at_caps_of_state) 511 apply (frule(1) cap_cur_auth_caps_of_state, simp+) 512 apply (clarsimp simp: aag_cap_auth_def pas_refined_all_auth_is_owns) 513 apply (intro conjI impI, (simp add: word_and_le2 field_simps 514 | erule ball_subset[where A="{a && c .. b}" for a b c])+) 515 done 516 517lemma clas_default_cap: 518 "tp \<noteq> ArchObject ASIDPoolObj \<Longrightarrow> cap_links_asid_slot aag p (default_cap tp p' sz dev)" 519 unfolding cap_links_asid_slot_def 520 apply (cases tp, simp_all) 521 apply (rename_tac aobject_type) 522 apply (case_tac aobject_type, simp_all add: arch_default_cap_def) 523 done 524 525lemma cli_default_cap: 526 "tp \<noteq> ArchObject ASIDPoolObj \<Longrightarrow> cap_links_irq aag p (default_cap tp p' sz dev)" 527 unfolding cap_links_irq_def 528 apply (cases tp, simp_all) 529 done 530 531lemma obj_refs_default_nut: 532 "\<lbrakk> tp \<noteq> Untyped; \<forall>atp. tp \<noteq> ArchObject atp \<rbrakk> \<Longrightarrow> 533 obj_refs (default_cap tp oref sz dev) = {oref}" 534 by (cases tp, simp_all add: arch_default_cap_def split: aobject_type.splits) 535 536lemma obj_refs_default': 537 "is_aligned oref (obj_bits_api tp sz) \<Longrightarrow> obj_refs (default_cap tp oref sz dev) \<subseteq> ptr_range oref (obj_bits_api tp sz)" 538 by (cases tp, simp_all add: arch_default_cap_def ptr_range_memI obj_bits_api_def default_arch_object_def split: aobject_type.splits) 539 540lemma create_cap_pas_refined: 541 "\<lbrace>pas_refined aag and K (tp \<noteq> ArchObject ASIDPoolObj \<and> is_subject aag (fst p) \<and> is_subject aag (fst (fst ref)) \<and> 542 (\<forall>x \<in> ptr_range (snd ref) (obj_bits_api tp sz). is_subject aag x) 543 \<and> is_aligned (snd ref) (obj_bits_api tp sz))\<rbrace> 544 create_cap tp sz p dev ref 545 \<lbrace>\<lambda>rv. pas_refined aag\<rbrace>" 546 apply(simp add: create_cap_def split_def) 547 apply(wp set_cdt_pas_refined | clarsimp)+ 548 apply (rule conjI) 549 apply (cases "fst ref", clarsimp simp: pas_refined_refl) 550 apply (cases "tp = Untyped") 551 apply (simp add: cap_links_asid_slot_def pas_refined_refl cap_links_irq_def aag_cap_auth_def ptr_range_def obj_bits_api_def) 552 apply (clarsimp simp add: obj_refs_default_nut clas_default_cap pas_refined_refl cli_default_cap aag_cap_auth_def) 553 apply(drule obj_refs_default') 554 apply(case_tac tp, simp_all) 555 apply(auto intro: pas_refined_refl dest!: subsetD) 556 done 557 558lemma pd_shifting_dual': 559 "is_aligned (pd::word32) pd_bits \<Longrightarrow> 560 pd + (vptr >> 20 << 2) && mask pd_bits = vptr >> 20 << 2" 561 apply (subst (asm) pd_bits_def) 562 apply (subst (asm) pageBits_def) 563 apply( simp add: pd_shifting_dual) 564 done 565 566 567lemma empty_table_update_from_arm_global_pts: 568 "\<lbrakk>valid_global_objs s; 569 kernel_base >> 20 \<le> y >> 20; y >> 20 \<le> 2 ^ (pd_bits - 2) - 1; 570 is_aligned pd pd_bits; 571 kheap s (arm_global_pd (arch_state s)) = Some (ArchObj (PageDirectory pda)); 572 obj_at (empty_table (set (second_level_tables (arch_state s)))) pd s\<rbrakk> 573 \<Longrightarrow> 574 (\<forall>pdb. ko_at (ArchObj (PageDirectory pdb)) pd s \<longrightarrow> 575 empty_table (set (second_level_tables (arch_state s))) 576 (ArchObj 577 (PageDirectory 578 (pdb(ucast (y >> 20) := pda (ucast (y >> 20)))))))" 579 apply(clarsimp simp: empty_table_def obj_at_def) 580 apply(clarsimp simp: valid_global_objs_def obj_at_def empty_table_def) 581 done 582 583lemma copy_global_mappings_pas_refined: 584 "is_aligned pd pd_bits \<Longrightarrow> 585 \<lbrace>pas_refined aag and valid_kernel_mappings and 586 valid_arch_state and valid_global_objs and valid_global_refs and 587 pspace_aligned\<rbrace> 588 copy_global_mappings pd 589 \<lbrace>\<lambda>rv. pas_refined aag\<rbrace>" 590 apply(simp add: copy_global_mappings_def) 591 apply(rule hoare_weaken_pre) 592 apply(wp) 593 (* Use \<circ> to avoid wp filtering out the global_pd condition here 594 TODO: see if we can clean this up *) 595 apply(rule_tac Q="\<lambda> rv s. is_aligned global_pd pd_bits \<and> (global_pd = (arm_global_pd \<circ> arch_state) s \<and> valid_kernel_mappings s \<and> valid_arch_state s \<and> valid_global_objs s \<and> valid_global_refs s \<and> pas_refined aag s)" in hoare_strengthen_post) 596 apply(rule mapM_x_wp[OF _ subset_refl]) 597 apply (rule hoare_seq_ext) 598 apply(unfold o_def) 599 (* Use [1] so wp doesn't filter out the global_pd condition *) 600 apply(wp store_pde_pas_refined store_pde_valid_kernel_mappings_map_global)[1] 601 apply(frule subsetD[OF copy_global_mappings_index_subset]) 602 apply(rule hoare_gen_asm[simplified K_def pred_conj_def conj_commute]) 603 apply(simp add: get_pde_def) 604 apply(subst kernel_vsrefs_kernel_mapping_slots[symmetric]) 605 apply(wp) 606 apply(clarsimp simp: get_pde_def pd_shifting' pd_shifting_dual' triple_shift_fun) 607 apply(subst (asm) obj_at_def, erule exE, erule conjE) 608 apply(rotate_tac -1, drule sym, simp) 609 apply(frule (1) valid_kernel_mappingsD[folded obj_at_def]) 610 apply(clarsimp simp: kernel_mapping_slots_def shiftr_20_less 611 empty_table_update_from_arm_global_pts 612 global_refs_def pde_ref_def) 613 apply(fastforce) 614 apply fastforce 615 apply(rule gets_wp) 616 apply(simp, blast intro: invs_aligned_pdD) 617 done 618 619lemma copy_global_invs_mappings_restricted': 620 "pd \<in> S \<Longrightarrow> 621 \<lbrace>all_invs_but_equal_kernel_mappings_restricted S 622 and (\<lambda>s. S \<inter> global_refs s = {}) 623 and K (is_aligned pd pd_bits)\<rbrace> 624 copy_global_mappings pd 625 \<lbrace>\<lambda>rv. all_invs_but_equal_kernel_mappings_restricted S\<rbrace>" 626 apply(rule hoare_weaken_pre) 627 apply(rule copy_global_invs_mappings_restricted) 628 apply(simp add: insert_absorb) 629 done 630 631lemma init_arch_objects_pas_refined: 632 "\<lbrace>pas_refined aag and 633 post_retype_invs tp refs and 634 (\<lambda> s. \<forall> x\<in>set refs. x \<notin> global_refs s) and 635 K (\<forall>ref \<in> set refs. is_aligned ref (obj_bits_api tp obj_sz))\<rbrace> 636 init_arch_objects tp ptr bits obj_sz refs 637 \<lbrace>\<lambda>rv. pas_refined aag\<rbrace>" 638 apply(rule hoare_gen_asm) 639 apply(cases tp) 640 apply(simp_all add: init_arch_objects_def) 641 apply(wp | simp)+ 642 apply(rename_tac aobject_type) 643 apply(case_tac aobject_type, simp_all) 644 apply((simp | wp)+)[5] 645 apply(wp) 646 apply(rule_tac Q="\<lambda> rv. pas_refined aag and all_invs_but_equal_kernel_mappings_restricted (set refs) and (\<lambda> s. \<forall> x\<in>set refs. x \<notin> global_refs s)" in hoare_strengthen_post) 647 apply(wp mapM_x_wp[OF _ subset_refl]) 648 apply((wp copy_global_mappings_pas_refined 649 copy_global_invs_mappings_restricted' 650 copy_global_mappings_global_refs_inv 651 copy_global_invs_mappings_restricted' | 652 fastforce simp: obj_bits_api_def default_arch_object_def 653 pd_bits_def pageBits_def)+)[2] 654 apply(wp dmo_invs hoare_vcg_const_Ball_lift 655 valid_irq_node_typ | 656 fastforce simp: post_retype_invs_def)+ 657 done 658 659end 660 661locale retype_region_proofs' = retype_region_proofs + constrains s ::"det_ext state" and s' :: "det_ext state" 662 663context retype_region_proofs 664begin 665 666interpretation Arch . (*FIXME; arch_split*) 667 668lemma vs_refs_no_global_pts_default [simp]: 669 "vs_refs_no_global_pts (default_object ty dev us) = {}" 670 by (simp add: default_object_def default_arch_object_def tyunt 671 vs_refs_no_global_pts_def pde_ref2_def pte_ref_def 672 o_def 673 split: Structures_A.apiobject_type.splits aobject_type.splits) 674 675lemma vrefs_eq: "state_vrefs s' = state_vrefs s" 676 apply(rule ext) 677 apply(simp add: s'_def state_vrefs_def ps_def orthr split: option.split) 678 done 679 680lemma ts_eq[simp]: "thread_states s' = thread_states s" 681 apply (rule ext) 682 apply (simp add: s'_def ps_def thread_states_def get_tcb_def orthr tcb_states_of_state_def 683 split: option.split Structures_A.kernel_object.split) 684 apply (simp add: default_object_def default_tcb_def tyunt 685 split: Structures_A.apiobject_type.split) 686 done 687 688lemma bas_eq[simp]: "thread_bound_ntfns s' = thread_bound_ntfns s" 689 apply (rule ext) 690 apply (simp add: s'_def ps_def thread_bound_ntfns_def get_tcb_def orthr tcb_states_of_state_def 691 split: option.split Structures_A.kernel_object.split) 692 apply (simp add: default_object_def default_tcb_def tyunt 693 split: Structures_A.apiobject_type.split) 694 done 695end 696 697context retype_region_proofs' 698begin 699 700interpretation Arch . (*FIXME; arch_split*) 701 702lemma domains_of_state: "domains_of_state s' \<subseteq> domains_of_state s" 703 unfolding s'_def by simp 704 705lemma pas_refined: "pas_refined aag s \<Longrightarrow> pas_refined aag s'" 706 apply(erule pas_refined_state_objs_to_policy_subset) 707 apply(simp add: state_objs_to_policy_def refs_eq vrefs_eq mdb_and_revokable) 708 apply(rule subsetI, rename_tac x, case_tac x, simp) 709 apply(erule state_bits_to_policy.cases) 710 apply(auto intro!: sbta_caps intro: caps_retype split: cap.split)[1] 711 apply(auto intro!: sbta_untyped intro: caps_retype split: cap.split)[1] 712 apply((blast intro: state_bits_to_policy.intros)+)[4] 713 apply (simp add: vrefs_eq) 714 apply(auto elim!: state_asids_to_policy_aux.cases 715 intro: state_asids_to_policy_aux.intros caps_retype 716 split: cap.split dest: sata_asid[OF caps_retype, rotated])[1] 717 apply clarsimp 718 apply (erule state_irqs_to_policy_aux.cases) 719 apply(auto intro!: sita_controlled intro: caps_retype split: cap.split)[1] 720 apply (rule domains_of_state) 721 apply simp 722 done 723 724end 725 726context begin interpretation Arch . (*FIXME: arch_split*) 727 728lemma retype_region_ext_kheap_update: 729 "\<lbrace>Q xs and R xs\<rbrace> retype_region_ext xs ty \<lbrace>\<lambda>_. Q xs\<rbrace> 730 \<Longrightarrow> \<lbrace>\<lambda>s. Q xs (kheap_update f s) \<and> R xs (kheap_update f s)\<rbrace> retype_region_ext xs ty \<lbrace>\<lambda>_ s. Q xs (kheap_update f s)\<rbrace>" 731 apply (clarsimp simp: valid_def retype_region_ext_def) 732 apply (erule_tac x="kheap_update f s" in allE) 733 apply (clarsimp simp: split_def bind_def gets_def get_def return_def modify_def put_def) 734 done 735 736lemma use_retype_region_proofs_ext': 737 assumes x: "\<And>(s::det_ext state). \<lbrakk> retype_region_proofs s ty us ptr sz n dev; P s \<rbrakk> 738 \<Longrightarrow> Q (retype_addrs ptr ty n us) (s\<lparr>kheap := 739 \<lambda>x. if x \<in> set (retype_addrs ptr ty n us) 740 then Some (default_object ty dev us ) 741 else kheap s x\<rparr>)" 742 assumes y: "\<And>xs. \<lbrace>Q xs and R xs\<rbrace> retype_region_ext xs ty \<lbrace>\<lambda>_. Q xs\<rbrace>" 743 assumes z: "\<And>f xs s. R xs (kheap_update f s) = R xs s" 744 shows 745 "\<lbrakk> ty = CapTableObject \<Longrightarrow> 0 < us; 746 \<And>s. P s \<Longrightarrow> Q (retype_addrs ptr ty n us) s \<rbrakk> \<Longrightarrow> 747 \<lbrace>\<lambda>s. valid_pspace s \<and> valid_mdb s \<and> range_cover ptr sz (obj_bits_api ty us) n 748 \<and> caps_overlap_reserved {ptr..ptr + of_nat n * 2 ^ obj_bits_api ty us - 1} s 749 \<and> caps_no_overlap ptr sz s \<and> pspace_no_overlap_range_cover ptr sz s 750 \<and> (\<exists>slot. cte_wp_at (\<lambda>c. up_aligned_area ptr sz \<subseteq> cap_range c \<and> cap_is_device c = dev) slot s) \<and> 751 P s \<and> R (retype_addrs ptr ty n us) s\<rbrace> retype_region ptr n us ty dev \<lbrace>Q\<rbrace>" 752 apply (simp add: retype_region_def split del: if_split) 753 apply (rule hoare_pre, (wp|simp)+) 754 apply (rule retype_region_ext_kheap_update[OF y]) 755 apply (wp|simp)+ 756 apply (clarsimp simp: retype_addrs_fold 757 foldr_upd_app_if fun_upd_def[symmetric]) 758 apply safe 759 apply (rule x) 760 apply (rule retype_region_proofs.intro, simp_all)[1] 761 apply (fastforce simp add: range_cover_def obj_bits_api_def z 762 slot_bits_def word_bits_def cte_level_bits_def)+ 763 done 764 765lemmas use_retype_region_proofs_ext 766 = use_retype_region_proofs_ext'[where Q="\<lambda>_. Q" and P=Q, simplified] for Q 767 768end 769 770lemma (in is_extended) pas_refined_tcb_domain_map_wellformed': 771 assumes tdmw: "\<lbrace>tcb_domain_map_wellformed aag and P\<rbrace> f \<lbrace>\<lambda>_. tcb_domain_map_wellformed aag\<rbrace>" 772 shows "\<lbrace>pas_refined aag and P\<rbrace> f \<lbrace>\<lambda>_. pas_refined aag\<rbrace>" 773apply (simp add: pas_refined_def) 774apply (wp tdmw) 775apply (wp lift_inv) 776apply simp+ 777done 778 779context begin interpretation Arch . (*FIXME: arch_split*) 780 781lemma retype_region_ext_pas_refined: 782 "\<lbrace>pas_refined aag and pas_cur_domain aag and K (\<forall>x\<in> set xs. is_subject aag x)\<rbrace> retype_region_ext xs ty \<lbrace>\<lambda>_. pas_refined aag\<rbrace>" 783 including no_pre 784 apply (subst and_assoc[symmetric]) 785 apply (wp retype_region_ext_extended.pas_refined_tcb_domain_map_wellformed') 786 apply (simp add: retype_region_ext_def, wp) 787 apply (clarsimp simp: tcb_domain_map_wellformed_aux_def) 788 apply (erule domains_of_state_aux.cases) 789 apply (clarsimp simp: foldr_upd_app_if' fun_upd_def[symmetric] split: if_split_asm) 790 apply (clarsimp simp: default_ext_def default_etcb_def split: apiobject_type.splits) 791 defer 792 apply (force intro: domtcbs) 793 done 794 795lemma retype_region_pas_refined: 796 "\<lbrace>pas_refined aag and pas_cur_domain aag and 797 valid_pspace and valid_mdb and 798 caps_overlap_reserved 799 {ptr..ptr + of_nat num_objects * 2 ^ obj_bits_api type o_bits - 800 1} and 801 caps_no_overlap ptr sz and pspace_no_overlap_range_cover ptr sz and 802 (\<lambda>s. \<exists>slot. cte_wp_at (\<lambda>c. up_aligned_area ptr sz \<subseteq> cap_range c \<and> cap_is_device c = dev) slot s) and 803 K (range_cover ptr sz (obj_bits_api type o_bits) num_objects) and 804 K (\<forall>x\<in>set (retype_addrs ptr type num_objects o_bits). is_subject aag x) and 805 K ((type = CapTableObject \<longrightarrow> 0 < o_bits))\<rbrace> 806 retype_region ptr num_objects o_bits type dev 807 \<lbrace>\<lambda>rv. pas_refined aag\<rbrace>" 808 apply (rule hoare_gen_asm) 809 apply (rule hoare_pre) 810 apply(rule use_retype_region_proofs_ext) 811 apply(erule (1) retype_region_proofs'.pas_refined[OF retype_region_proofs'.intro]) 812 apply (wp retype_region_ext_pas_refined) 813 apply simp 814 apply auto 815 done 816 817(* MOVE *) 818lemma retype_region_aag_bits: 819 "\<lbrace>\<lambda>s. P (null_filter (caps_of_state s)) (state_refs_of s) (cdt s) (state_vrefs s) 820 \<and> valid_pspace s \<and> valid_mdb s \<and> 821 caps_overlap_reserved 822 {ptr..ptr + of_nat num_objects * 2 ^ obj_bits_api tp us - 1} s \<and> 823 caps_no_overlap ptr sz s \<and> pspace_no_overlap_range_cover ptr sz s \<and> 824 (\<exists>slot. cte_wp_at (\<lambda>c. up_aligned_area ptr sz \<subseteq> cap_range c \<and> cap_is_device c = dev) slot s) 825 \<and> ((tp = CapTableObject \<longrightarrow> 0 < us) \<and> range_cover ptr sz (obj_bits_api tp us) num_objects)\<rbrace> 826 retype_region ptr num_objects us tp dev 827 \<lbrace>\<lambda>_ s. P (null_filter (caps_of_state s)) (state_refs_of s) (cdt s) (state_vrefs s)\<rbrace>" 828 apply (subst conj_assoc [symmetric])+ 829 apply (rule hoare_gen_asm [unfolded pred_conj_def K_def])+ 830 apply (rule hoare_pre) 831 apply (rule use_retype_region_proofs) 832 apply (frule retype_region_proofs.null_filter, erule ssubst) 833 apply (frule retype_region_proofs.refs_eq, erule ssubst) 834 apply (frule retype_region_proofs.vrefs_eq, erule ssubst) 835 apply (frule retype_region_proofs.mdb_and_revokable, erule ssubst) 836 apply assumption 837 apply simp 838 apply simp 839 apply simp 840 apply blast 841 done 842 843lemma retype_region_ranges'': 844 "\<lbrace>K (range_cover ptr sz (obj_bits_api tp us) num_objects \<and> num_objects \<noteq> 0)\<rbrace> 845 retype_region ptr num_objects us tp dev 846 \<lbrace>\<lambda>rv s. \<forall>y\<in>set rv. ptr_range y (obj_bits_api tp us) \<subseteq> {ptr..ptr + of_nat num_objects * 2 ^ (obj_bits_api tp us) - 1}\<rbrace>" 847 apply simp 848 apply (rule hoare_gen_asm[where P'="\<top>", simplified]) 849 apply (rule hoare_strengthen_post [OF retype_region_ret]) 850 apply (clarsimp) 851 apply (frule_tac p=y in range_cover_subset) 852 apply assumption 853 apply simp 854 apply(rule conjI) 855 apply (fastforce simp: ptr_range_def ptr_add_def) 856 apply(clarsimp simp: ptr_range_def ptr_add_def intro: order_trans) 857 apply(erule order_trans) 858 apply(erule impE) 859 apply(simp add: p_assoc_help) 860 apply(rule is_aligned_no_wrap') 861 apply(rule is_aligned_add) 862 apply(fastforce simp: range_cover_def) 863 apply(simp add: is_aligned_mult_triv2) 864 apply(rule minus_one_helper, simp) 865 apply(rule power_not_zero) 866 apply(simp add: range_cover_def) 867 apply simp 868 done 869 870lemma region_in_kernel_window_preserved: 871 assumes "\<And> P. \<lbrace>\<lambda> s. P (arch_state s) \<rbrace> f \<lbrace>\<lambda> rv s. P (arch_state s) \<rbrace>" 872 shows "\<And> S. \<lbrace> region_in_kernel_window S \<rbrace> f \<lbrace> \<lambda>_. region_in_kernel_window S \<rbrace>" 873 apply(clarsimp simp: valid_def region_in_kernel_window_def) 874 apply(erule use_valid) 875 apply(rule assms) 876 apply simp 877 done 878 879lemma pspace_no_overlap_msu[simp]: 880 "pspace_no_overlap S (machine_state_update f s) = pspace_no_overlap S s" 881 apply(clarsimp simp: pspace_no_overlap_def) 882 done 883 884lemma descendants_range_in_msu[simp]: 885 "descendants_range_in S slot (machine_state_update f s) = descendants_range_in S slot s" 886 apply(clarsimp simp: descendants_range_in_def) 887 done 888 889(* proof clagged from Retype_AI.clearMemory_vms *) 890lemma freeMemory_vms: 891 "valid_machine_state s \<Longrightarrow> 892 \<forall>x\<in>fst (freeMemory ptr bits (machine_state s)). 893 valid_machine_state (s\<lparr>machine_state := snd x\<rparr>)" 894 apply (clarsimp simp: valid_machine_state_def 895 disj_commute[of "in_user_frame p s" for p s]) 896 apply (drule_tac x=p in spec, simp) 897 apply (drule_tac P4="\<lambda>m'. underlying_memory m' p = 0" 898 in use_valid[where P=P and Q="\<lambda>_. P" for P], simp_all) 899 apply (simp add: freeMemory_def machine_op_lift_def 900 machine_rest_lift_def split_def) 901 apply (wp hoare_drop_imps | simp | wp mapM_x_wp_inv)+ 902 apply (simp add: storeWord_def | wp)+ 903 apply (simp add: word_rsplit_0)+ 904 done 905 906 907lemma dmo_freeMemory_vms: 908 "\<lbrace>valid_machine_state\<rbrace> 909 do_machine_op (freeMemory ptr bits) 910 \<lbrace>\<lambda>_. valid_machine_state\<rbrace>" 911 apply(unfold do_machine_op_def) 912 apply (wp modify_wp freeMemory_vms | simp add: split_def)+ 913 done 914 915lemma freeMemory_valid_irq_states: 916 "\<lbrace>\<lambda>m. valid_irq_states (s\<lparr>machine_state := m\<rparr>) \<rbrace> 917 freeMemory ptr bits 918 \<lbrace>\<lambda>a b. valid_irq_states (s\<lparr>machine_state := b\<rparr>)\<rbrace>" 919 unfolding freeMemory_def 920 apply(wp mapM_x_wp[OF _ subset_refl] storeWord_valid_irq_states) 921 done 922 923crunch pspace_respects_device_region[wp]: freeMemory "\<lambda>ms. P (device_state ms)" 924 (wp: crunch_wps) 925 926lemma dmo_freeMemory_invs: 927 "\<lbrace> invs \<rbrace> 928 do_machine_op (freeMemory ptr bits) 929 \<lbrace>\<lambda>_. invs\<rbrace>" 930 apply (simp add: do_machine_op_def invs_def valid_state_def cur_tcb_def | wp | wpc)+ 931 apply (clarsimp) 932 apply (frule_tac P1="(=) (device_state (machine_state s))" in 933 use_valid[OF _ freeMemory_pspace_respects_device_region]) 934 apply simp 935 apply simp 936 apply(rule conjI) 937 apply(erule use_valid[OF _ freeMemory_valid_irq_states], simp) 938 apply(drule freeMemory_vms) 939 by auto 940 941 942lemma delete_objects_pas_refined: 943 "\<lbrace>pas_refined aag\<rbrace> delete_objects ptr sz \<lbrace>\<lambda>_. pas_refined aag\<rbrace>" 944 apply(simp add: delete_objects_def do_machine_op_def) 945 apply (wp modify_wp | simp add: split_def)+ 946 apply clarsimp 947 apply(rule pas_refined_detype) 948 apply simp 949 done 950 951 952lemma cte_wp_at_sym: 953 "cte_wp_at (\<lambda> c. c = cap) slot s = cte_wp_at ((=) cap) slot s" 954 apply(simp add: cte_wp_at_def) 955 done 956 957lemma untyped_slots_not_in_untyped_range: 958 "\<lbrakk>invs s; descendants_range_in S slot s; cte_wp_at ((=) cap) slot s; 959 is_untyped_cap cap; S = untyped_range cap; T \<subseteq> S\<rbrakk> \<Longrightarrow> 960 fst slot \<notin> T" 961 apply(erule contra_subsetD) 962 proof - 963 assume i: "invs s" and 964 dr: "descendants_range_in S slot s" and 965 ct: "cte_wp_at ((=) cap) slot s" and 966 ut: "is_untyped_cap cap" and 967 r: "S = untyped_range cap" 968 hence dt: "detype_locale cap slot s" 969 by(simp add: detype_locale_def descendants_range_def2 invs_untyped_children) 970 show "fst slot \<notin> S" 971 apply - 972 apply (insert r) 973 apply (simp, rule detype_locale.non_null_present[OF dt]) 974 apply (insert ct ut) 975 apply (case_tac cap, simp_all) 976 apply (auto simp: cte_wp_at_def) 977 done 978 qed 979 980lemma descendants_range_in_detype: 981 "\<lbrakk>invs s; descendants_range_in S slot s; cte_wp_at ((=) cap) slot s; 982 is_untyped_cap cap; S = untyped_range cap; T \<subseteq> S\<rbrakk> \<Longrightarrow> 983 descendants_range_in T slot (detype S s)" 984 apply(erule descendants_range_in_subseteq[rotated]) 985 proof - 986 assume i: "invs s" and 987 dr: "descendants_range_in S slot s" and 988 ct: "cte_wp_at ((=) cap) slot s" and 989 ut: "is_untyped_cap cap" and 990 r: "S = untyped_range cap" 991 hence dt: "detype_locale cap slot s" 992 by(simp add: detype_locale_def descendants_range_def2 invs_untyped_children) 993 show "descendants_range_in S slot (detype S s)" 994 apply - 995 apply(insert i dr ct ut r) 996 apply(simp add: valid_mdb_descendants_range_in[OF invs_mdb]) 997 apply(simp add: descendants_range_in_def) 998 apply(rule ballI) 999 apply(drule_tac x=p' in bspec, assumption) 1000 apply(clarsimp simp: null_filter_def split: if_split_asm) 1001 apply(rule conjI) 1002 apply(simp add: cte_wp_at_caps_of_state) 1003 apply(rule_tac t=a in ssubst[OF fst_conv[symmetric]]) 1004 apply(rule_tac ptr=slot and s=s in detype_locale.non_null_present) 1005 apply(rule dt) 1006 apply(simp add: cte_wp_at_caps_of_state) 1007 apply fastforce 1008 done 1009 qed 1010 1011lemma descendants_range_in_detype_ex: 1012 "\<lbrakk>invs s; descendants_range_in S slot s; \<exists> cap. cte_wp_at ((=) cap) slot s \<and> 1013 is_untyped_cap cap \<and> S = untyped_range cap; T \<subseteq> S\<rbrakk> \<Longrightarrow> 1014 descendants_range_in T slot (detype S s)" 1015 apply clarsimp 1016 apply(blast intro: descendants_range_in_detype) 1017 done 1018 1019lemma descendants_range_in_detype_ex_strengthen: 1020 "(invs s \<and> descendants_range_in S slot s \<and> (\<exists> cap. cte_wp_at ((=) cap) slot s \<and> 1021 is_untyped_cap cap \<and> S = untyped_range cap) \<and> T \<subseteq> S) \<longrightarrow> 1022 descendants_range_in T slot (detype S s)" 1023 apply(blast intro: descendants_range_in_detype_ex) 1024 done 1025 1026lemma delete_objects_descendants_range_in': 1027 notes modify_wp[wp del] 1028 shows 1029 "\<lbrace>invs and (\<lambda> s. \<exists> idx. cte_wp_at ((=) (UntypedCap dev word2 sz idx)) slot s) and 1030 descendants_range_in {word2..word2 + 2 ^ sz - 1} slot\<rbrace> 1031 (delete_objects word2 sz) 1032 \<lbrace>\<lambda>_. descendants_range_in {word2..word2 + 2 ^ sz - 1} slot\<rbrace>" 1033 apply(rule hoare_pre) 1034 unfolding delete_objects_def 1035 apply (wp modify_wp dmo_freeMemory_invs 1036 | strengthen descendants_range_in_detype_ex_strengthen)+ 1037 apply (wp descendants_range_in_lift hoare_vcg_ex_lift | elim conjE | simp)+ 1038 apply clarsimp 1039 apply(fastforce) 1040 done 1041 1042lemma untyped_cap_aligned: 1043 "\<lbrakk>cte_wp_at ((=) (UntypedCap dev word sz idx)) slot s; valid_objs s\<rbrakk> \<Longrightarrow> 1044 is_aligned word sz" 1045 apply(fastforce dest: cte_wp_at_valid_objs_valid_cap simp: valid_cap_def cap_aligned_def) 1046 done 1047 1048lemma delete_objects_descendants_range_in'': 1049 shows 1050 "\<lbrace>invs and (\<lambda> s. \<exists> idx. cte_wp_at ((=) (UntypedCap dev word2 sz idx)) slot s) and 1051 descendants_range_in {word2..word2 + 2 ^ sz - 1} slot\<rbrace> 1052 (delete_objects word2 sz) 1053 \<lbrace>\<lambda>_. descendants_range_in {word2..(word2 && ~~ mask sz) + 2 ^ sz - 1} slot\<rbrace>" 1054 apply(clarsimp simp: valid_def) 1055 apply(frule untyped_cap_aligned, fastforce) 1056 apply(clarsimp simp: is_aligned_neg_mask_eq) 1057 apply(erule use_valid) 1058 apply(wp delete_objects_descendants_range_in' | clarsimp | blast)+ 1059 done 1060 1061lemma delete_objects_descendants_range_in''': 1062 shows 1063 "\<lbrace>invs and (\<lambda> s. \<exists> idx. cte_wp_at ((=) (UntypedCap dev word2 sz idx)) slot s) and 1064 descendants_range_in {word2..word2 + 2 ^ sz - 1} slot\<rbrace> 1065 (delete_objects word2 sz) 1066 \<lbrace>\<lambda>_. descendants_range_in {word2 && ~~ mask sz..(word2 && ~~ mask sz) + 2 ^ sz - 1} slot\<rbrace>" 1067 apply(clarsimp simp: valid_def) 1068 apply(frule untyped_cap_aligned, fastforce) 1069 apply(clarsimp simp: is_aligned_neg_mask_eq) 1070 apply(erule use_valid) 1071 apply(wp delete_objects_descendants_range_in' | clarsimp | blast)+ 1072 done 1073 1074lemma range_cover_subset'': 1075 "\<lbrakk>range_cover ptr sz sbit n; n \<noteq> 0\<rbrakk> 1076 \<Longrightarrow> {ptr ..ptr + of_nat n * 2 ^ sbit - 1} \<subseteq> {ptr && ~~ mask sz..(ptr && ~~ mask sz) + 2^ sz - 1}" 1077 apply (rule order_trans, erule(1) range_cover_subset') 1078 apply (simp add: word_and_le2) 1079 done 1080 1081lemma delete_objects_descendants_range_in'''': 1082 shows 1083 "\<lbrace>invs and (\<lambda> s. \<exists> idx. cte_wp_at ((=) (UntypedCap dev word2 sz idx)) slot s) and 1084 ct_active and descendants_range_in {word2..word2 + 2 ^ sz - 1} slot and 1085 K (range_cover word2 sz bits n \<and> 1086 n \<noteq> 0)\<rbrace> 1087 (delete_objects word2 sz) 1088 \<lbrace>\<lambda>_. descendants_range_in {word2..word2 + of_nat n * 2 ^ bits - 1} slot\<rbrace>" 1089 apply(clarsimp simp: valid_def) 1090 apply(rule descendants_range_in_subseteq) 1091 apply(erule use_valid) 1092 apply(wp delete_objects_descendants_range_in' | clarsimp | blast)+ 1093 apply(drule range_cover_subset'', simp) 1094 apply(fastforce dest: untyped_cap_aligned simp: is_aligned_neg_mask_eq) 1095 done 1096 1097lemmas delete_objects_descendants_range_in = 1098 delete_objects_descendants_range_in' 1099 delete_objects_descendants_range_in'' 1100 delete_objects_descendants_range_in''' 1101 delete_objects_descendants_range_in'''' 1102 1103crunch global_refs[wp]: delete_objects "\<lambda> s. P (global_refs s)" 1104 (ignore: do_machine_op freeMemory) 1105 1106crunch arch_state[wp]: delete_objects "\<lambda> s. P (arch_state s)" 1107 (ignore: do_machine_op freeMemory) 1108 1109 1110 1111lemma bits_of_UntypedCap: 1112 "bits_of (UntypedCap dev ptr sz free) = sz" 1113 apply(simp add: bits_of_def split: cap.splits) 1114 done 1115 1116 1117lemma mask_neg_mask_is_zero: 1118 "((x::word32) && ~~ a) && a = 0" 1119 apply(subst word_bw_assocs) 1120 apply simp 1121 done 1122 1123(* clagged from Untyped_R.invoke_untyped_proofs.usable_range_disjoint *) 1124lemma usable_range_disjoint: 1125 assumes cte_wp_at: "cte_wp_at ((=) (cap.UntypedCap dev (ptr && ~~ mask sz) sz idx)) cref s" 1126 assumes misc : "distinct slots" "idx \<le> unat (ptr && mask sz) \<or> ptr = ptr && ~~ mask sz" 1127 "invs s" "slots \<noteq> []" "ct_active s" 1128 "\<forall>slot\<in>set slots. cte_wp_at ((=) cap.NullCap) slot s" 1129 "\<forall>x\<in>set slots. ex_cte_cap_wp_to (\<lambda>_. True) x s" 1130 assumes cover: "range_cover ptr sz (obj_bits_api tp us) (length slots)" 1131 notes blah[simp del] = untyped_range.simps usable_untyped_range.simps atLeastAtMost_iff atLeastatMost_subset_iff atLeastLessThan_iff 1132 Int_atLeastAtMost atLeastatMost_empty_iff split_paired_Ex 1133 shows 1134 "usable_untyped_range (cap.UntypedCap dev (ptr && ~~ mask sz) sz 1135 (unat ((ptr && mask sz) + of_nat (length slots) * 2 ^ obj_bits_api tp us))) \<inter> 1136 {ptr..ptr + of_nat (length slots) * 2 ^ obj_bits_api tp us - 1} = {}" 1137 proof - 1138 have not_0_ptr[simp]: "ptr\<noteq> 0" 1139 using misc cte_wp_at 1140 apply (clarsimp simp:cte_wp_at_caps_of_state) 1141 apply (drule(1) caps_of_state_valid) 1142 apply (clarsimp simp:valid_cap_def) 1143 done 1144 1145 have idx_compare''[simp]: 1146 "unat ((ptr && mask sz) + (of_nat (length slots) * (2::word32) ^ obj_bits_api tp us)) < 2 ^ sz 1147 \<Longrightarrow> ptr + of_nat (length slots) * 2 ^ obj_bits_api tp us - 1 1148 < ptr + of_nat (length slots) * 2 ^ obj_bits_api tp us" 1149 apply (rule minus_one_helper,simp) 1150 apply (rule neq_0_no_wrap) 1151 apply (rule machine_word_plus_mono_right_split) 1152 apply (simp add:shiftl_t2n range_cover_unat[OF cover] field_simps) 1153 apply (simp add:range_cover.sz[where 'a=32, folded word_bits_def, OF cover])+ 1154 done 1155 show ?thesis 1156 apply (clarsimp simp:mask_out_sub_mask blah) 1157 apply (drule idx_compare'') 1158 apply (simp add:not_le[symmetric]) 1159 done 1160 qed 1161 1162lemma set_free_index_invs': 1163 "\<lbrace> (\<lambda>s. invs s \<and> 1164 cte_wp_at ((=) cap) slot s \<and> 1165 (free_index_of cap \<le> idx' \<or> 1166 (descendants_range_in {word1..word1 + 2 ^ (bits_of cap) - 1} slot s \<and> 1167 pspace_no_overlap_range_cover word1 (bits_of cap) s)) \<and> 1168 idx' \<le> 2 ^ cap_bits cap \<and> 1169 is_untyped_cap cap) and K(word1 = obj_ref_of cap \<and> dev = (cap_is_device cap))\<rbrace> 1170 set_cap 1171 (UntypedCap dev word1 (bits_of cap) idx') 1172 slot 1173 \<lbrace>\<lambda>_. invs \<rbrace>" 1174 apply(rule hoare_gen_asm) 1175 apply(case_tac cap, simp_all add: bits_of_def) 1176 apply(case_tac "free_index_of cap \<le> idx'") 1177 apply simp 1178 apply(cut_tac cap=cap and cref=slot and idx="idx'" in set_free_index_invs) 1179 apply(simp add: free_index_update_def conj_comms is_cap_simps) 1180 apply simp 1181 apply(wp set_untyped_cap_invs_simple | simp)+ 1182 apply(fastforce simp: cte_wp_at_def) 1183 done 1184 1185lemma delete_objects_pspace_no_overlap: 1186 "\<lbrace> pspace_aligned and valid_objs and 1187 cte_wp_at ((=) (UntypedCap dev ptr sz idx)) slot\<rbrace> 1188 delete_objects ptr sz 1189 \<lbrace>\<lambda>rv. pspace_no_overlap_range_cover ptr sz\<rbrace>" 1190 unfolding delete_objects_def do_machine_op_def 1191 apply(wp | simp add: split_def detype_machine_state_update_comm)+ 1192 apply clarsimp 1193 apply(rule pspace_no_overlap_detype) 1194 apply(auto dest: cte_wp_at_valid_objs_valid_cap) 1195 done 1196 1197lemma delete_objects_pspace_no_overlap': 1198 "\<lbrace> pspace_aligned and valid_objs and 1199 cte_wp_at ((=) (UntypedCap dev ptr sz idx)) slot\<rbrace> 1200 delete_objects ptr sz 1201 \<lbrace>\<lambda>rv. pspace_no_overlap_range_cover (ptr && ~~ mask sz) sz\<rbrace>" 1202 apply(clarsimp simp: valid_def) 1203 apply(frule untyped_cap_aligned, simp) 1204 apply(clarsimp simp: is_aligned_neg_mask_eq) 1205 apply(frule(1) cte_wp_at_valid_objs_valid_cap) 1206 apply(erule use_valid, wp delete_objects_pspace_no_overlap, auto) 1207 done 1208 1209(* FIXME: move *) 1210lemma valid_cap_range_untyped: 1211 "\<lbrakk> valid_objs s; cte_wp_at ((=) (UntypedCap dev (ptr && ~~ mask sz) sz idx)) slot s\<rbrakk> 1212 \<Longrightarrow> cte_wp_at (\<lambda>c. up_aligned_area ptr sz \<subseteq> cap_range c \<and> cap_is_device c = dev) slot s" 1213 apply (rule cte_wp_at_weakenE) 1214 apply simp 1215 apply (clarsimp simp: word_and_le2 p_assoc_help) 1216 done 1217 1218lemma retype_region_pas_refined': 1219 "\<lbrace>pas_refined aag and pas_cur_domain aag and invs and 1220 caps_overlap_reserved 1221 {ptr..ptr + of_nat num_objects * 2 ^ obj_bits_api type o_bits - 1222 1} and 1223 (\<lambda> s. \<exists> idx. cte_wp_at (\<lambda> c. c = (UntypedCap dev (ptr && ~~ mask sz) sz idx)) slot s \<and> 1224 (idx \<le> unat (ptr && mask sz) \<or> 1225 (descendants_range_in {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} slot s) \<and> 1226 pspace_no_overlap_range_cover ptr sz s)) and 1227 K (sz < word_bits) and 1228 K (range_cover ptr sz (obj_bits_api type o_bits) num_objects) and 1229 K (\<forall>x\<in>set (retype_addrs ptr type num_objects o_bits). is_subject aag x) and 1230 K ((type = CapTableObject \<longrightarrow> 0 < o_bits))\<rbrace> 1231 retype_region ptr num_objects o_bits type dev 1232 \<lbrace>\<lambda>rv. pas_refined aag\<rbrace>" 1233 apply(rule hoare_gen_asm)+ 1234 apply(rule hoare_weaken_pre) 1235 apply(rule use_retype_region_proofs_ext) 1236 apply(erule (1) retype_region_proofs'.pas_refined[OF retype_region_proofs'.intro]) 1237 apply (wp retype_region_ext_pas_refined) 1238 apply simp 1239 apply fastforce 1240 apply fastforce 1241 apply clarsimp 1242 apply (frule valid_cap_range_untyped[OF invs_valid_objs]) 1243 apply (fastforce simp: cte_wp_at_caps_of_state) 1244 apply (cases slot) 1245 apply (auto intro: cte_wp_at_caps_no_overlapI descendants_range_caps_no_overlapI 1246 cte_wp_at_pspace_no_overlapI simp: cte_wp_at_sym) 1247 done 1248 1249 1250lemma free_index_of_UntypedCap: 1251 "free_index_of (UntypedCap dev ptr sz idx) = idx" 1252 apply(simp add: free_index_of_def) 1253 done 1254 1255fun slot_of_untyped_inv where "slot_of_untyped_inv (Retype slot _ _ _ _ _ _ _) = slot" 1256 1257lemma region_in_kernel_window_subseteq: 1258 "\<lbrakk> region_in_kernel_window S s; T \<subseteq> S\<rbrakk> \<Longrightarrow> 1259 region_in_kernel_window T s" 1260 apply(fastforce simp: region_in_kernel_window_def) 1261 done 1262 1263lemma aag_cap_auth_UntypedCap_idx_dev: 1264 "aag_cap_auth aag l (UntypedCap dev base sz idx) \<Longrightarrow> 1265 aag_cap_auth aag l (UntypedCap dev' base sz idx')" 1266 by (clarsimp simp: aag_cap_auth_def cap_links_asid_slot_def 1267 cap_links_irq_def) 1268 1269lemma cte_wp_at_pas_cap_cur_auth_UntypedCap_idx_dev: 1270 "\<lbrakk>cte_wp_at ((=) (UntypedCap dev base sz idx)) slot s; is_subject aag (fst slot); 1271 pas_refined aag s\<rbrakk> \<Longrightarrow> 1272 pas_cap_cur_auth aag (UntypedCap dev' base sz idx')" 1273 apply(rule aag_cap_auth_UntypedCap_idx_dev) 1274 apply(auto intro: cap_cur_auth_caps_of_state simp: cte_wp_at_caps_of_state) 1275 done 1276 1277lemmas caps_pas_cap_cur_auth_UntypedCap_idx_dev 1278 = cte_wp_at_pas_cap_cur_auth_UntypedCap_idx_dev[OF caps_of_state_cteD] 1279 1280lemma retype_addrs_aligned_range_cover: 1281 assumes xin: "x \<in> set (retype_addrs ptr ty n us)" 1282 and co: "range_cover ptr sz (obj_bits_api ty us) n" 1283 shows "is_aligned x (obj_bits_api ty us)" 1284 using co 1285 apply (clarsimp simp: range_cover_def) 1286 apply (rule retype_addrs_aligned[OF xin, where sz=sz], simp_all) 1287 apply (simp add: word_bits_def) 1288 done 1289 1290lemma pas_refined_work_units_complete[simp]: 1291 "pas_refined aag (work_units_completed_update f s) = pas_refined aag s" 1292 by (simp add: pas_refined_def) 1293 1294lemma reset_untyped_cap_pas_refined[wp]: 1295 "\<lbrace>pas_refined aag and cte_wp_at is_untyped_cap slot 1296 and K (is_subject aag (fst slot))\<rbrace> 1297 reset_untyped_cap slot 1298 \<lbrace>\<lambda>_. pas_refined aag\<rbrace>" 1299 apply (rule hoare_gen_asm) 1300 apply (clarsimp simp: reset_untyped_cap_def) 1301 apply (rule hoare_pre) 1302 apply (wp | simp add: unless_def)+ 1303 apply (rule valid_validE, rule_tac P="is_untyped_cap cap 1304 \<and> pas_cap_cur_auth aag cap" in hoare_gen_asm) 1305 apply (rule validE_valid, rule mapME_x_inv_wp) 1306 apply (rule hoare_pre) 1307 apply (wp preemption_point_inv' | simp)+ 1308 apply (clarsimp simp: is_cap_simps aag_cap_auth_UntypedCap_idx_dev bits_of_def) 1309 apply (wp hoare_vcg_const_imp_lift get_cap_wp 1310 delete_objects_pas_refined | simp add: if_apply_def2)+ 1311 apply (clarsimp simp: cte_wp_at_caps_of_state is_cap_simps bits_of_def) 1312 apply (auto elim: caps_pas_cap_cur_auth_UntypedCap_idx_dev) 1313 done 1314 1315lemma retype_region_post_retype_invs_spec: 1316 "\<lbrace>invs and caps_no_overlap ptr sz and pspace_no_overlap_range_cover ptr sz 1317 and caps_overlap_reserved {ptr..ptr + of_nat n * 2 ^ obj_bits_api ty us - 1} 1318 and region_in_kernel_window {ptr .. (ptr && ~~ mask sz) + 2 ^ sz - 1} 1319 and (\<lambda>s. \<exists>idx. cte_wp_at ((=) (UntypedCap dev (ptr && ~~ mask sz) sz idx)) slot s) 1320 and K (ty = Structures_A.CapTableObject \<longrightarrow> 0 < us) 1321 and K (range_cover ptr sz (obj_bits_api ty us) n) \<rbrace> 1322 retype_region ptr n us ty dev\<lbrace>\<lambda>rv. post_retype_invs ty rv\<rbrace>" 1323 apply (rule hoare_pre) 1324 apply (wp retype_region_post_retype_invs) 1325 apply (clarsimp simp del: split_paired_Ex) 1326 apply (frule valid_cap_range_untyped[OF invs_valid_objs],simp) 1327 apply (intro conjI) 1328 apply fastforce+ 1329 done 1330 1331lemma invoke_untyped_pas_refined: 1332 notes modify_wp[wp del] 1333 notes usable_untyped_range.simps[simp del] 1334 shows 1335 "\<lbrace>pas_refined aag and pas_cur_domain aag and invs and valid_untyped_inv ui and ct_active and K (authorised_untyped_inv aag ui)\<rbrace> 1336 invoke_untyped ui 1337 \<lbrace>\<lambda>rv. pas_refined aag\<rbrace>" 1338 apply(rule hoare_gen_asm) 1339 apply (rule hoare_pre) 1340 apply (rule_tac Q="\<lambda>_. pas_refined aag and pas_cur_domain aag" in hoare_strengthen_post) 1341 apply (rule invoke_untyped_Q) 1342 apply (rule hoare_pre, wp create_cap_pas_refined) 1343 apply (clarsimp simp: authorised_untyped_inv_def 1344 range_cover.aligned ptr_range_def[symmetric] 1345 retype_addrs_aligned_range_cover) 1346 apply (clarsimp simp: cte_wp_at_caps_of_state 1347 is_cap_simps ptr_range_def[symmetric]) 1348 apply (frule cap_cur_auth_caps_of_state[where 1349 cap="cap.UntypedCap dev p sz idx" for dev p sz idx], simp+) 1350 apply (clarsimp simp add: aag_cap_auth_def ptr_range_def[symmetric] 1351 pas_refined_all_auth_is_owns) 1352 apply blast 1353 apply (rule hoare_pre, wp init_arch_objects_pas_refined) 1354 apply (clarsimp simp: retype_addrs_aligned_range_cover 1355 cte_wp_at_caps_of_state) 1356 apply (drule valid_global_refsD[rotated 2]) 1357 apply (clarsimp simp: post_retype_invs_def split: if_split_asm) 1358 apply (erule caps_of_state_cteD) 1359 apply (erule notE, erule subsetD[rotated]) 1360 apply (rule order_trans, erule retype_addrs_subset_ptr_bits) 1361 apply (simp add: field_simps word_and_le2) 1362 apply (rule hoare_name_pre_state, clarsimp) 1363 apply (rule hoare_pre, wp retype_region_pas_refined) 1364 apply (clarsimp simp: authorised_untyped_inv_def) 1365 apply (strengthen range_cover_le[mk_strg I E], simp) 1366 apply (intro conjI exI; (erule cte_wp_at_weakenE)?, 1367 clarsimp simp: field_simps word_and_le2) 1368 1369 apply (rule hoare_pre, wp) 1370 apply (clarsimp simp: cte_wp_at_caps_of_state is_cap_simps) 1371 apply (cases ui, clarsimp simp: authorised_untyped_inv_def 1372 caps_pas_cap_cur_auth_UntypedCap_idx_dev) 1373 apply wp 1374 apply clarsimp 1375 apply (cases ui, clarsimp simp: cte_wp_at_caps_of_state authorised_untyped_inv_def) 1376 done 1377 1378subsection{* decode *} 1379 1380lemma data_to_obj_type_ret_not_asid_pool: 1381 "\<lbrace> \<top> \<rbrace> data_to_obj_type v \<lbrace> \<lambda>r s. r \<noteq> ArchObject ASIDPoolObj \<rbrace>,-" 1382 apply(clarsimp simp: validE_R_def validE_def valid_def) 1383 apply(auto simp: data_to_obj_type_def arch_data_to_obj_type_def throwError_def simp: returnOk_def bindE_def return_def bind_def lift_def split: if_split_asm) 1384 done 1385 1386definition authorised_untyped_inv' where 1387 "authorised_untyped_inv' aag ui \<equiv> case ui of 1388 Invocations_A.untyped_invocation.Retype src_slot reset base aligned_free_ref new_type obj_sz slots dev \<Rightarrow> 1389 is_subject aag (fst src_slot) \<and> (0::word32) < of_nat (length slots) \<and> 1390 new_type \<noteq> ArchObject ASIDPoolObj \<and> 1391 (\<forall>x\<in>set slots. is_subject aag (fst x))" 1392 1393lemma authorised_untyped_invI: 1394 notes blah[simp del] = atLeastAtMost_iff atLeastatMost_subset_iff atLeastLessThan_iff 1395 Int_atLeastAtMost atLeastatMost_empty_iff split_paired_Ex 1396 1397 shows 1398 "\<lbrakk>valid_untyped_inv ui s; pas_refined aag s; 1399 authorised_untyped_inv' aag ui\<rbrakk> \<Longrightarrow> 1400 authorised_untyped_inv aag ui" 1401 apply(case_tac ui) 1402 apply(clarsimp simp: cte_wp_at_caps_of_state 1403 authorised_untyped_inv_def authorised_untyped_inv'_def 1404 del: ballI) 1405 apply (frule(1) cap_cur_auth_caps_of_state, simp) 1406 apply (simp add: aag_cap_auth_def aag_has_Control_iff_owns) 1407 apply (frule range_cover_subset'', simp) 1408 apply (frule retype_addrs_subset_ptr_bits) 1409 apply (subgoal_tac "case ui of Retype src r base aligned_free_ref new_type obj_sz slots dev \<Rightarrow> 1410 {aligned_free_ref .. base + 2 ^ sz - 1} \<subseteq> {base .. base + 2 ^ sz - 1}") 1411 apply (simp add: field_simps) 1412 apply blast 1413 apply (simp add: blah word_and_le2) 1414 done 1415 1416lemma nonzero_unat_simp: 1417 "0 < unat (x::word32) \<Longrightarrow> 0 < x" 1418 apply(auto dest: word_of_nat_less) 1419 done 1420 1421lemma decode_untyped_invocation_authorised: 1422 "\<lbrace>invs and pas_refined aag and valid_cap cap 1423 and cte_wp_at ((=) cap) slot 1424 and (\<lambda>s. \<forall>cap\<in>set excaps. 1425 is_cnode_cap cap \<longrightarrow> 1426 (\<forall>r\<in>cte_refs cap (interrupt_irq_node s). 1427 ex_cte_cap_wp_to is_cnode_cap r s)) 1428 and (\<lambda>s. \<forall>x\<in>set excaps. s \<turnstile> x) 1429 and K (cap = cap.UntypedCap dev base sz idx 1430 \<and> is_subject aag (fst slot) 1431 \<and> (\<forall>c \<in> set excaps. pas_cap_cur_auth aag c) 1432 \<and> (\<forall> ref \<in> untyped_range cap. is_subject aag ref))\<rbrace> 1433 decode_untyped_invocation label args slot cap excaps 1434 \<lbrace>\<lambda>rv s. authorised_untyped_inv aag rv\<rbrace>,-" 1435 apply(rule hoare_gen_asmE) 1436 apply(rule hoare_pre) 1437 apply (strengthen authorised_untyped_invI[mk_strg I]) 1438 apply(wp dui_inv_wf | simp)+ 1439 apply (clarsimp simp: decode_untyped_invocation_def split_def 1440 authorised_untyped_inv'_def 1441 split del: if_split split: untyped_invocation.splits) 1442 (* need to hoist the is_cnode_cap assumption into postcondition later on *) 1443 1444 apply (simp add: unlessE_def[symmetric] whenE_def[symmetric] unlessE_whenE 1445 split del: if_split) 1446 apply (wp whenE_throwError_wp hoare_vcg_all_lift mapME_x_inv_wp 1447 | simp split: untyped_invocation.splits 1448 | (auto)[1])+ 1449 apply (rule_tac Q="\<lambda>node_cap s. 1450 (is_cnode_cap node_cap \<longrightarrow> is_subject aag (obj_ref_of node_cap)) \<and> 1451 is_subject aag (fst slot) \<and> 1452 new_type \<noteq> ArchObject ASIDPoolObj \<and> 1453 (\<forall> cap. cte_wp_at ((=) cap) slot s \<longrightarrow> 1454 (\<forall>ref\<in>ptr_range base (bits_of cap). is_subject aag ref))" 1455 in hoare_strengthen_post) 1456 apply (wp get_cap_inv get_cap_ret_is_subject) 1457 apply (fastforce simp: nonzero_unat_simp) 1458 apply clarsimp 1459 apply(wp lookup_slot_for_cnode_op_authorised 1460 lookup_slot_for_cnode_op_inv whenE_throwError_wp)+ 1461 apply(rule hoare_drop_imps)+ 1462 apply(clarsimp) 1463 apply(rule_tac Q'="\<lambda>rv s. rv \<noteq> ArchObject ASIDPoolObj \<and> 1464 (\<forall> cap. cte_wp_at ((=) cap) slot s \<longrightarrow> 1465 (\<forall>ref\<in>ptr_range base (bits_of cap). is_subject aag ref)) \<and> 1466 is_subject aag (fst slot) \<and> 1467 pas_refined aag s \<and> 2 \<le> sz \<and> 1468 sz < word_bits \<and> is_aligned base sz \<and> 1469 (is_cnode_cap (excaps ! 0) \<longrightarrow> 1470 (\<forall> x\<in>obj_refs (excaps ! 0). is_subject aag x))" 1471 in hoare_post_imp_R) 1472 apply(wp data_to_obj_type_ret_not_asid_pool data_to_obj_type_inv2) 1473 apply(case_tac "excaps ! 0", simp_all, fastforce simp: nonzero_unat_simp)[1] 1474 apply(wp whenE_throwError_wp)+ 1475 apply(auto dest!: bang_0_in_set 1476 simp: valid_cap_def cap_aligned_def obj_ref_of_def is_cap_simps 1477 cap_auth_conferred_def pas_refined_all_auth_is_owns 1478 aag_cap_auth_def ptr_range_def untyped_min_bits_def 1479 dest: cte_wp_at_eqD2 simp: bits_of_UntypedCap) 1480 done 1481 1482end 1483 1484end 1485