1(* 2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) 3 * 4 * SPDX-License-Identifier: GPL-2.0-only 5 *) 6 7theory Untyped_DR 8imports CNode_DR 9begin 10 11context begin interpretation Arch . (*FIXME: arch_split*) 12 13lemma detype_dcorres: 14 "S = {ptr..ptr + 2 ^ sz - 1} 15 \<Longrightarrow> dcorres dc \<top> (\<lambda>s. invs s \<and> (\<exists>cref. cte_wp_at ((=) (cap.UntypedCap dev ptr sz idx)) cref s) \<and> valid_etcbs s) 16 (modify (Untyped_D.detype S)) 17 (modify (Retype_A.detype S))" 18 apply (rule corres_modify) 19 apply (clarsimp simp: transform_def Untyped_D.detype_def 20 transform_cdt_def 21 split del: if_split 22 simp del: untyped_range.simps) 23 apply (simp add: Untyped_D.detype_def transform_def 24 transform_current_thread_def Retype_A.detype_def transform_asid_table_def 25 detype_ext_def wrap_ext_det_ext_ext_def) 26 apply (rule ext) 27 apply (clarsimp simp: map_option_case restrict_map_def transform_objects_def 28 map_add_def cte_wp_at_caps_of_state 29 split: option.split) 30 apply (drule valid_global_refsD2) 31 apply clarsimp 32 apply (clarsimp simp: global_refs_def transform_object_def detype_ext_def) 33 done 34 35(* FIXME: move *) 36lemma evalMonad_loadWords: 37 "evalMonad (mapM loadWord xs) ms = 38 (if (\<forall>x\<in>set xs. is_aligned x 2) then 39 Some (map (\<lambda>x. word_rcat [underlying_memory ms (x + 3), 40 underlying_memory ms (x + 2), 41 underlying_memory ms (x + 1), 42 underlying_memory ms x]) xs) 43 else None)" 44proof (induct xs) 45 case Nil thus ?case 46 by (simp add: evalMonad_def mapM_simps return_def) 47next 48 note mapM_simps[simp] 49 50 (* FIXME: could be generalized. *) 51 have evalMonad_bind_return: 52 "\<And>f g s. \<forall>x\<in>fst (f s). snd x = s \<Longrightarrow> \<exists>r. \<forall>x\<in>fst (f s). fst x = r \<Longrightarrow> 53 \<exists>r. \<forall>x\<in>fst (g s). fst x = r \<Longrightarrow> 54 evalMonad (do r \<leftarrow> f; rs \<leftarrow> g; return (r#rs) od) s = 55 (case evalMonad f s of None \<Rightarrow> None 56 | Some r \<Rightarrow> (case evalMonad g s of None \<Rightarrow> None 57 | Some rs \<Rightarrow> Some (r#rs)))" 58 apply (simp add: evalMonad_def bind_def split_def return_def) 59 apply safe 60 apply auto[2] 61 apply (rule sym) 62 apply (rule someI2_ex, fastforce) 63 apply (clarsimp split: if_split_asm) 64 apply (rule conjI) 65 apply (rule someI2_ex, fastforce+)+ 66 done 67 68 have loadWord_const: 69 "\<And>a s. \<forall>x\<in>fst (loadWord a s). snd x = s" 70 apply (case_tac "is_aligned a 2") 71 apply (simp add: loadWord_def is_aligned_mask exec_gets) 72 apply (simp add: return_def) 73 apply (simp add: loadWord_def exec_gets fail_def is_aligned_mask) 74 done 75 76 have loadWord_atMostOneResult: 77 "\<And>a s. \<exists>r. \<forall>x\<in>fst (loadWord a s). fst x = r" 78 apply (case_tac "is_aligned a 2") 79 apply (simp add: loadWord_def is_aligned_mask exec_gets) 80 apply (simp add: return_def) 81 apply (simp add: loadWord_def exec_gets fail_def is_aligned_mask) 82 done 83 84 have mapM_loadWord_atMostOneResult[rule_format]: 85 "\<And>as s. \<exists>rs. \<forall>x\<in>fst (mapM loadWord as s). fst x = rs" 86 apply (induct_tac as) 87 apply (simp add: return_def) 88 using loadWord_const loadWord_atMostOneResult 89 by (fastforce simp: bind_def split_def return_def) 90 91 case Cons thus ?case 92 by (simp add: evalMonad_bind_return[OF loadWord_const 93 loadWord_atMostOneResult mapM_loadWord_atMostOneResult] 94 evalMonad_loadWord is_aligned_mask 95 split: option.splits) 96qed 97 98(* FIXME: change definition! *) 99lemma get_ipc_buffer_words_def2: 100 "get_ipc_buffer_words ms tcb ns \<equiv> 101 (case tcb_ipcframe tcb of 102 cap.ArchObjectCap (arch_cap.PageCap dev buf rights sz mapdata) \<Rightarrow> 103 if AllowRead \<in> rights then 104 (if ns = Nil \<or> is_aligned (buf + tcb_ipc_buffer tcb) 2 then 105 map ((\<lambda>x. word_rcat [underlying_memory ms (x + 3), 106 underlying_memory ms (x + 2), 107 underlying_memory ms (x + 1), 108 underlying_memory ms x]) \<circ> 109 (\<lambda>n. buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + 110 of_nat n * of_nat word_size)) 111 ns 112 else the None) 113 else [] 114 | _ \<Rightarrow> [])" 115proof - 116 117 (* FIXME: extract *) 118 have mask_eq: 119 "\<And>p q m n. m\<ge>n \<Longrightarrow> p + (q && mask m) && mask n = p + q && mask n" 120 by (subst mask_eqs(2)[of p "q && mask m" for p q m, symmetric]) 121 (simp add: mask_twice min_def mask_eqs) 122 123 have eq: "\<And>x p b sz. is_aligned (p + (b && mask (pageBitsForSize sz)) + 124 of_nat x * of_nat word_size) 2 125 \<longleftrightarrow> is_aligned (p + b) 2" 126 apply (rule iffI) 127 apply (drule is_aligned_addD2) 128 apply (simp add: word_size_def is_aligned_mult_triv2[where n=2, 129 simplified word_bits_def, simplified]) 130 apply (simp add: is_aligned_mask mask_eq) 131 apply (rule is_aligned_add) 132 apply (simp add: is_aligned_mask mask_eq) 133 apply (simp add: word_size_def is_aligned_mult_triv2[where n=2, 134 simplified word_bits_def, simplified]) 135 done 136 137 show "PROP ?thesis" 138 apply (rule eq_reflection) 139 apply (auto simp: get_ipc_buffer_words_def evalMonad_loadWords eq 140 split: cap.splits arch_cap.splits) 141 done 142qed 143 144lemma is_arch_page_cap_def2: 145 "is_arch_page_cap cap \<longleftrightarrow> 146 (\<exists>dev buf rights sz mapdata. 147 cap = cap.ArchObjectCap (arch_cap.PageCap dev buf rights sz mapdata))" 148 by (simp add: is_arch_page_cap_def split: cap.splits arch_cap.splits) 149 150lemma transform_full_intent_machine_state_eq: 151 assumes 3: "tcb_ipcframe tcb = 152 cap.ArchObjectCap (arch_cap.PageCap dev buf rights sz opt)" 153 assumes 4: "is_aligned buf (pageBitsForSize sz)" 154 assumes 1: "is_aligned (tcb_ipc_buffer tcb) msg_align_bits" 155 assumes 5: "(\<forall>p. buf = (p && ~~ mask (pageBitsForSize sz)) \<longrightarrow> 156 underlying_memory ms' p = underlying_memory ms p)" 157 shows "transform_full_intent ms tref tcb = transform_full_intent ms' tref tcb" 158proof - 159 have 2: "valid_message_info (get_tcb_message_info tcb)" 160 by (simp add: get_tcb_message_info_def data_to_message_info_valid) 161 162 let ?p = "%x. buf + (tcb_ipc_buffer tcb && mask (pageBitsForSize sz)) + 163 of_nat x * of_nat word_size" 164 have word_rcat_eq: 165 "\<And>x. x<128 \<Longrightarrow> 166 word_rcat [underlying_memory ms (?p x + 3), 167 underlying_memory ms (?p x + 2), 168 underlying_memory ms (?p x + 1), 169 underlying_memory ms (?p x)] = 170 word_rcat [underlying_memory ms'(?p x + 3), 171 underlying_memory ms'(?p x + 2), 172 underlying_memory ms'(?p x + 1), 173 underlying_memory ms'(?p x)]" 174 proof - 175 fix x :: nat 176 assume x: "x<128" 177 have y: "!!y. y<4 \<Longrightarrow> ?p x + y && ~~ mask (pageBitsForSize sz) = buf" 178 apply (simp add: add.assoc) 179 apply (rule is_aligned_add_helper[OF 4, THEN conjunct2]) 180 apply (rule_tac n=msg_align_bits in is_aligned_add_less_t2n) 181 apply (rule is_aligned_andI1[OF 1]) 182 apply (rule_tac n=2 in is_aligned_add_less_t2n) 183 apply (simp add: word_size_def) 184 apply (rule is_aligned_mult_triv2[where n=2, simplified]) 185 apply simp 186 apply (simp add: msg_align_bits) 187 apply (simp add: word_size_def) 188 apply (rule word_less_power_trans_ofnat[where k=2, simplified], 189 simp_all add: x msg_align_bits word_bits_def)[1] 190 apply (case_tac sz, simp_all add: msg_align_bits)[1] 191 apply (rule and_mask_less_size) 192 apply (case_tac sz, simp_all add: word_size)[1] 193 done 194 195 note 6 = 5[rule_format, OF y[symmetric]] 196 show "?thesis x" 197 apply (rule arg_cong[where f=word_rcat]) 198 using 6[of 3] 6[of 2] 6[of 1] 6[of 0] 199 by simp 200 qed 201 202 show ?thesis 203 apply (clarsimp simp: transform_full_intent_def Let_def get_tcb_mrs_def 204 get_ipc_buffer_words_def2 3 205 Suc_leI[OF msg_registers_lt_msg_max_length] 206 simp del: upt_Suc 207 split del: if_split) 208 apply (case_tac "AllowRead \<in> rights", 209 simp_all del: upt_Suc split del: if_split) 210 apply (cut_tac y=2 in is_aligned_weaken[OF 1]) 211 apply (simp add: msg_align_bits) 212 apply (cut_tac y=2 in is_aligned_weaken[OF 4]) 213 apply (case_tac sz, simp_all)[1] 214 apply (frule (1) is_aligned_add[of buf 2 "tcb_ipc_buffer tcb"]) 215 apply (simp add: o_def del: upt_Suc) 216 apply (intro conjI) 217 apply (rule arg_cong2[where f=transform_intent, OF refl]) 218 apply (rule arg_cong2[where f="(@)", OF refl]) 219 apply (rule arg_cong2[where f=take, OF refl]) 220 apply (rule map_cong[OF refl]) 221 apply (rule word_rcat_eq) 222 apply (clarsimp simp: atLeastAtMost_upt[symmetric] msg_max_length_def 223 simp del: upt_Suc) 224 apply clarsimp 225 apply (rule word_rcat_eq) 226 using 2 227 apply (clarsimp simp: buffer_cptr_index_def msg_max_length_def 228 valid_message_info_def msg_max_extra_caps_def word_le_nat_alt) 229 apply (rule arg_cong2[where f="case_list None", OF refl]) 230 apply (rule map_cong[OF refl]) 231 apply (rule word_rcat_eq) 232 apply (clarsimp simp: atLeastAtMost_upt[symmetric] simp del: upt_Suc) 233 apply (simp add: msg_max_length_def msg_max_extra_caps_def) 234 done 235qed 236 237lemma valid_page_cap_imp_valid_buf: 238 "s \<turnstile> cap.ArchObjectCap (arch_cap.PageCap False buf rights sz mapdata) \<Longrightarrow> 239 is_aligned buf (pageBitsForSize sz) \<and> typ_at (AArch (AUserData sz)) buf s" 240 by (clarsimp simp add: valid_cap_simps cap_aligned_def) 241 242lemma freeMemory_dcorres: 243 "is_aligned ptr bits \<Longrightarrow> 2 \<le> bits \<Longrightarrow> bits < word_bits \<Longrightarrow> 244 dcorres dc (\<lambda>_. True) 245 (pspace_no_overlap_range_cover ptr bits and valid_objs and valid_etcbs) 246 (return rv) (do_machine_op (freeMemory ptr bits))" 247 apply (clarsimp simp add: corres_underlying_def split_def return_def) 248 apply (rename_tac s t) 249 apply (drule_tac P="(=) s" and 250 Q="%_ u. (\<exists>ms. u=s\<lparr>machine_state := ms\<rparr>) \<and> 251 (\<forall>p\<in>UNIV-{ptr..ptr + 2 ^ bits - 1}. 252 underlying_memory (machine_state s) p = 253 underlying_memory (machine_state u) p)" 254 in use_valid) 255 apply (simp add: do_machine_op_def split_def) 256 apply wp 257 apply (clarsimp simp: freeMemory_def mapM_x_storeWord_step[simplified word_size_bits_def] 258 intvl_range_conv') 259 apply (rule conjI, fastforce) 260 apply clarsimp 261 apply (erule use_valid[where P=P and Q="%_. P" for P]) 262 apply wp 263 apply (clarsimp simp: is_aligned_no_wrap' of_nat_less_pow_32 word_bits_def 264 x_power_minus_1 word_plus_mono_right) 265 apply (rule refl) 266 apply (rule refl) 267 apply (clarsimp simp: transform_def transform_current_thread_def) 268 apply (rule ext) 269 apply (clarsimp simp: transform_objects_def map_add_def) 270 apply (clarsimp simp: option_map_def split: option.splits) 271 apply (clarsimp simp: transform_object_def transform_tcb_def 272 split: Structures_A.kernel_object.split option.splits) 273 apply (rename_tac s ms tref etcb tcb) 274 apply (clarsimp simp: restrict_map_def split: if_split_asm) 275 apply (frule(1) valid_etcbs_tcb_etcb) 276 apply (case_tac "\<not> is_arch_page_cap (tcb_ipcframe tcb)") 277 apply (erule transform_full_intent_no_ipc_buffer) 278 apply (clarsimp simp: is_arch_page_cap_def2) 279 apply (simp add: valid_objs_def) 280 apply (drule_tac x=tref in bspec, clarsimp+) 281 apply (clarsimp simp: valid_obj_def valid_tcb_def) 282 (* FIXME: extract a sensible lemma for that *) 283 apply (drule_tac x="(tcb_ipcframe, tcb_ipcframe_update, 284 \<lambda>_ _. is_nondevice_page_cap or (=) cap.NullCap)" in bspec) 285 apply (simp add: ran_tcb_cap_cases) 286 apply clarsimp 287 apply (thin_tac "case_option x y z" for x y z) 288 apply (clarsimp simp add: valid_ipc_buffer_cap_def is_nondevice_page_cap_def split: bool.split_asm) 289 apply (drule valid_page_cap_imp_valid_buf) 290 apply (frule_tac transform_full_intent_machine_state_eq, simp_all) 291 apply clarsimp 292 apply (erule_tac x=p in bspec) 293 apply (frule is_aligned_no_overflow') 294 apply (clarsimp simp: pspace_no_overlap_def typ_at_eq_kheap_obj obj_at_def 295 mask_2pm1[symmetric]) 296 apply (erule_tac x="(p && ~~ mask (pageBitsForSize sz))" in allE) 297 apply clarsimp 298 apply (thin_tac "length xs = y" for xs y) 299 apply (erule impE) 300 apply (simp add:mask_def[unfolded shiftl_t2n,simplified,symmetric] p_assoc_help) 301 apply (erule order_trans[OF word_and_le2]) 302 apply (erule impE) 303 apply (rule_tac y = p in order_trans) 304 apply simp 305 apply (cut_tac ptr = p and n = "pageBitsForSize sz" in word_neg_and_le) 306 apply (simp add:mask_def[unfolded shiftl_t2n,simplified,symmetric] p_assoc_help) 307 apply (thin_tac "x\<noteq>y" for x y) 308 apply (erule notE)+ 309 apply (rule is_aligned_no_wrap'[OF is_aligned_neg_mask]) 310 apply (rule le_refl) 311 apply (simp add:mask_def not_le pbfs_less_wb'[unfolded word_bits_def, simplified]) 312 done 313 314declare wrap_ext_det_ext_ext_def[simp] 315 316(* Strictly speaking, we would not need ct_active, here. Proving that, 317 however, requires a stronger version of lemma detype_invariants. *) 318lemma delete_objects_dcorres: 319 notes order_class.Icc_eq_Icc [simp del] 320 is_aligned_neg_mask_eq[simp del] 321 is_aligned_neg_mask_weaken[simp del] 322 assumes S: "S = {ptr..ptr + 2 ^ bits - 1}" 323 shows "dcorres dc \<top> 324 (\<lambda>s. invs s \<and> ct_active s \<and> (\<exists>cref dev idx. 325 cte_wp_at ((=) (cap.UntypedCap dev ptr bits idx)) cref s 326 \<and> descendants_range (cap.UntypedCap dev ptr bits idx) cref s) \<and> valid_etcbs s) 327 (modify (Untyped_D.detype S)) 328 (delete_objects ptr bits)" 329 apply (clarsimp simp: S) 330 apply (unfold delete_objects_def2 K_bind_def) 331 apply (rule corres_bind_return) 332 apply (rule_tac F="is_aligned ptr bits \<and> 2 \<le> bits \<and> bits < word_bits" 333 in corres_req) 334 apply clarsimp 335 apply (drule cte_wp_valid_cap, clarsimp) 336 apply (simp add: valid_cap_def cap_aligned_def untyped_min_bits_def) 337 apply (rule corres_name_pre, clarify) 338 apply (rule corres_guard_imp) 339 apply (rule corres_split[OF _ detype_dcorres]) 340 apply (rule freeMemory_dcorres, simp+) 341 apply wp 342 apply clarsimp 343 apply (rule TrueI)? 344 apply clarsimp 345 apply (rule conjI) 346 apply fastforce 347 apply (frule cte_wp_valid_cap, clarsimp) 348 apply (intro conjI) 349 apply (erule pspace_no_overlap_detype) 350 apply clarsimp+ 351 apply (frule invs_untyped_children) 352 apply (drule_tac detype_invariants, simp_all) 353 apply (clarsimp simp: empty_descendants_range_in descendants_range_def2 invs_def valid_state_def 354 valid_pspace_def detype_clear_um_independent valid_etcbs_def) 355 apply (simp add: invs_def valid_state_def valid_pspace_def detype_clear_um_independent valid_etcbs_def 356 is_etcb_at_def detype_def detype_ext_def st_tcb_at_kh_def obj_at_kh_def obj_at_def) 357 done 358 359lemma unat_ptr_range_end: 360 "\<lbrakk> is_aligned (ptr :: 'a :: len word) sz; sz < len_of TYPE('a)\<rbrakk> 361 \<Longrightarrow> unat (ptr + 2 ^ sz - 1) = unat ptr + 2 ^ sz - 1" 362 apply (simp only: add_diff_eq[symmetric]) 363 apply (subst unat_plus_simple[THEN iffD1]) 364 apply (simp add: add_diff_eq) 365 apply (subst unat_minus_one) 366 apply simp_all 367 done 368 369definition 370 translate_object_type :: "Structures_A.apiobject_type \<Rightarrow> cdl_object_type" 371where 372 "translate_object_type type \<equiv> case type of 373 Structures_A.Untyped \<Rightarrow> UntypedType 374 | Structures_A.TCBObject \<Rightarrow> TcbType 375 | Structures_A.EndpointObject \<Rightarrow> EndpointType 376 | Structures_A.NotificationObject \<Rightarrow> NotificationType 377 | Structures_A.CapTableObject \<Rightarrow> CNodeType 378 | ArchObject SmallPageObj \<Rightarrow> FrameType 12 379 | ArchObject LargePageObj \<Rightarrow> FrameType 16 380 | ArchObject SectionObj \<Rightarrow> FrameType 20 381 | ArchObject SuperSectionObj \<Rightarrow> FrameType 24 382 | ArchObject PageTableObj \<Rightarrow> PageTableType 383 | ArchObject PageDirectoryObj \<Rightarrow> PageDirectoryType 384 | ArchObject ASIDPoolObj \<Rightarrow> AsidPoolType" 385 386definition 387 translate_untyped_invocation :: "Invocations_A.untyped_invocation \<Rightarrow> cdl_untyped_invocation" 388where 389 "translate_untyped_invocation x \<equiv> 390 case x of Invocations_A.Retype cref reset ptr_base ptr tp us slots dev 391 \<Rightarrow> cdl_untyped_invocation.Retype 392 (transform_cslot_ptr cref ) 393 (translate_object_type tp) 394 us 395 (map transform_cslot_ptr slots) 396 (\<not> reset) (length slots)" 397 398definition 399 "retype_transform_obj_ref type sz ptr 400 \<equiv> if type = Structures_A.Untyped then {ptr .. ptr + 2^sz - 1} 401 else {ptr}" 402 403lemma transform_empty_cnode: 404 "transform_cnode_contents o_bits (empty_cnode o_bits) = empty_cap_map o_bits" 405 apply (simp add: transform_cnode_contents_def dom_empty_cnode) 406 apply (rule ext, simp add: option_map_join_def empty_cap_map_def 407 nat_to_bl_def len_bin_to_bl_aux empty_cnode_def) 408 done 409 410lemma transform_default_tcb: 411 "transform_tcb ms x default_tcb (default_etcb\<lparr>tcb_domain := domain\<rparr>) 412 = Tcb (Types_D.default_tcb domain)" 413 apply (simp add: transform_tcb_def default_tcb_def Types_D.default_tcb_def default_arch_tcb_def) 414 apply (simp add: transform_full_intent_def Let_def new_context_def cap_register_def capRegister_def 415 get_tcb_mrs_def Suc_le_eq get_tcb_message_info_def msg_info_register_def 416 msgInfoRegister_def data_to_message_info_def arch_tcb_context_get_def 417 get_ipc_buffer_words_def) 418 apply (simp add: transform_intent_def invocation_type_def fromEnum_def enum_invocation_label 419 enum_gen_invocation_labels toEnum_def) 420 apply (simp add: fun_eq_iff tcb_slot_defs infer_tcb_pending_op_def infer_tcb_bound_notification_def 421 guess_error_def default_etcb_def default_domain_def) 422 done 423 424lemma transform_unat_map_empty: 425 "unat_map (\<lambda>_ :: ('a :: len) word. Some cdl_cap.NullCap) 426 = empty_cap_map (len_of TYPE('a))" 427 by (rule ext, simp add: unat_map_def empty_cap_map_def) 428 429lemma transform_default_object: 430 "\<lbrakk>type \<noteq> Structures_A.Untyped; type = Structures_A.CapTableObject \<longrightarrow> 0 < o_bits\<rbrakk> \<Longrightarrow> 431 transform_object ms word (default_ext type domain) (Retype_A.default_object type dev o_bits) 432 = the (Types_D.default_object (translate_object_type type) o_bits domain)" 433 by (cases type, simp_all add: translate_object_type_def default_object_def 434 Types_D.default_object_def transform_default_tcb default_ext_def 435 transform_unat_map_empty transform_empty_cnode 436 Types_D.empty_cnode_def dom_empty_cnode 437 transform_object_def default_arch_object_def 438 transform_page_table_contents_def o_def transform_pte_def 439 transform_page_directory_contents_def transform_pde_def kernel_pde_mask_def 440 transform_asid_pool_contents_def transform_asid_pool_entry_def asid_low_bits_def 441 split: aobject_type.split nat.splits) 442 443lemma obj_bits_bound32: 444 "\<lbrakk>type = Structures_A.Untyped \<longrightarrow> us < 32; type = Structures_A.CapTableObject \<longrightarrow> us < 28\<rbrakk> 445 \<Longrightarrow> obj_bits_api type us < word_bits" 446 apply (case_tac type; simp add: obj_bits_api_def word_bits_def slot_bits_def) 447 apply (rename_tac aobject_type) 448 apply (case_tac aobject_type; simp add: arch_kobj_size_def default_arch_object_def pageBits_def) 449 done 450 451lemma obj_bits_bound4: 452 "\<lbrakk>type = Structures_A.Untyped \<longrightarrow> untyped_min_bits \<le> us\<rbrakk> \<Longrightarrow> 453 untyped_min_bits \<le> obj_bits_api type us" 454 apply (case_tac type; simp add: obj_bits_api_def word_bits_def slot_bits_def untyped_min_bits_def) 455 apply (rename_tac aobject_type) 456 apply (case_tac aobject_type; simp add:arch_kobj_size_def default_arch_object_def pageBits_def) 457 done 458 459lemma distinct_retype_addrs: 460 "\<lbrakk>type = Structures_A.Untyped \<longrightarrow> untyped_min_bits \<le> us; 461 range_cover ptr sz (obj_bits_api type us) n\<rbrakk> 462 \<Longrightarrow> distinct (retype_addrs ptr type n us)" 463 supply untyped_min_bits_def[simp] 464 apply (clarsimp simp:retype_addrs_def distinct_map ptr_add_def inj_on_def) 465 apply (simp only: shiftl_t2n[symmetric, simplified field_simps, simplified]) 466 apply (drule shiftl_inj_if) 467 apply (rule shiftl_shiftr_id) 468 apply (simp add:range_cover_def) 469 apply (rule word_of_nat_less) 470 apply (subst unat_power_lower) 471 apply (rule diff_less) 472 apply (cut_tac obj_bits_bound4[where us = us and type = type]) 473 apply simp 474 apply simp 475 apply (simp add:word_bits_def) 476 apply (erule Retype_AI.range_cover.range_cover_le_n_less(2)) 477 apply simp 478 apply (rule shiftl_shiftr_id) 479 apply (simp add:range_cover_def) 480 apply (rule word_of_nat_less) 481 apply (subst unat_power_lower) 482 apply (rule diff_less) 483 apply (cut_tac obj_bits_bound4[where us = us and type = type]) 484 apply simp 485 apply simp 486 apply (simp add:word_bits_def) 487 apply (erule Retype_AI.range_cover.range_cover_le_n_less(2)) 488 apply simp 489 apply (rule of_nat_inj[where 'a=32, THEN iffD1]) 490 apply (simp add:range_cover.range_cover_le_n_less[where 'a=32, simplified])+ 491 done 492 493lemma length_retype_addrs[simp]: 494 "length (retype_addrs ptr type n us) = n" 495 by (simp add:retype_addrs_def) 496 497lemma retype_transform_obj_ref_ut: 498 "(p \<in> (retype_transform_obj_ref Structures_A.Untyped sz ptr)) = (p \<in> {ptr .. ptr + 2^sz - 1})" 499 by (clarsimp simp:retype_transform_obj_ref_def) 500 501lemma transform_none_to_untyped: 502 "\<lbrakk>valid_idle s'; kheap s' obj_id = None\<rbrakk> 503 \<Longrightarrow> cdl_objects (transform s') obj_id = Some Types_D.Untyped" 504 apply (clarsimp simp: transform_def restrict_map_def map_add_def transform_objects_def) 505 apply (clarsimp simp: valid_idle_def pred_tcb_at_def obj_at_def) 506 done 507 508lemma retype_transform_obj_ref_available: 509 "\<lbrakk>pspace_no_overlap_range_cover ptr sz s'; s = transform s'; valid_pspace s'; valid_idle s'; 510 range_cover ptr sz (obj_bits_api ty us) n; 511 y \<in> set (retype_addrs ptr ty n us)\<rbrakk> 512 \<Longrightarrow> retype_transform_obj_ref ty us y \<subseteq> 513 (cdl_objects s) -` {Some Types_D.Untyped}" 514 apply (clarsimp simp:retype_transform_obj_ref_def | rule conjI)+ 515 apply (rule transform_none_to_untyped, simp) 516 apply (rule ccontr, clarsimp) 517 apply (drule(1) retype_addrs_range_subset[where p = y]) 518 apply (drule(1) pspace_no_overlap_obj_range) 519 apply (simp only: field_simps) 520 apply (drule(1) disjoint_subset2) 521 apply (clarsimp simp:obj_bits_api_def) 522 apply (drule p_in_obj_range) 523 apply clarsimp+ 524 apply auto[1] 525 apply (drule(2) pspace_no_overlap_into_Int_none) 526 apply (clarsimp simp: transform_def restrict_map_def map_add_def transform_objects_def 527 split: if_splits option.splits) 528 apply (fastforce simp: valid_idle_def pred_tcb_at_def obj_at_def) 529 done 530 531lemma retype_transform_obj_ref_pick_id: 532 "type \<noteq> Structures_A.Untyped 533 \<Longrightarrow> map (\<lambda>x. {pick x}) (map (retype_transform_obj_ref type us) xs) 534 = map (retype_transform_obj_ref type us) xs" 535 by (simp add:retype_transform_obj_ref_def) 536 537lemma translate_object_type_not_untyped: 538 "type \<noteq> Structures_A.Untyped 539 \<Longrightarrow> Some (the (Types_D.default_object (translate_object_type type) us current_domain)) 540 = Types_D.default_object (translate_object_type type) us current_domain" 541 by (clarsimp simp:translate_object_type_def Types_D.default_object_def 542 split:Structures_A.apiobject_type.splits aobject_type.splits) 543 544lemma retype_transform_obj_ref_not_untyped: 545 "\<lbrakk>type \<noteq> Structures_A.Untyped\<rbrakk> 546 \<Longrightarrow> 547 {x} \<in> retype_transform_obj_ref type us ` set xs = (x \<in> set xs)" 548 apply (rule iffI) 549 apply (clarsimp simp:retype_transform_obj_ref_def)+ 550 done 551 552lemma retype_transform_obj_ref_in_untyped_range: 553 notes [simp del] = atLeastAtMost_iff atLeastatMost_subset_iff 554 shows "\<lbrakk>y \<in> set (retype_addrs ptr type n us); 555 range_cover ptr sz (obj_bits_api type us) n\<rbrakk> 556 \<Longrightarrow> retype_transform_obj_ref type us y \<subseteq> 557 {ptr &&~~ mask sz ..(ptr && ~~ mask sz) + (2 ^ sz - 1)}" 558 apply (frule retype_addrs_subset_ptr_bits) 559 apply (clarsimp simp:retype_transform_obj_ref_def) 560 apply (rule conjI) 561 apply (drule(1) set_mp) 562 apply clarsimp 563 apply (erule set_mp[rotated]) 564 apply (frule(1) retype_addrs_range_subset) 565 apply (simp add:obj_bits_api_def) 566 apply (erule subset_trans) 567 apply (clarsimp simp: atLeastatMost_subset_iff field_simps) 568 apply (rule word_and_le2) 569 apply clarsimp 570 apply (erule set_mp[rotated]) 571 apply (erule subset_trans) 572 apply (clarsimp simp: atLeastatMost_subset_iff field_simps) 573 apply (rule word_and_le2) 574 done 575 576lemma retype_region_dcorres: 577 "dcorres (\<lambda>rv rv'. rv = map (retype_transform_obj_ref type us) rv' 578 \<and> rv' = retype_addrs ptr type n us) 579 \<top> 580 (\<lambda>s. pspace_no_overlap_range_cover ptr sz s \<and> invs s 581 \<and> range_cover ptr sz (obj_bits_api type us) n 582 \<and> (type = Structures_A.Untyped \<longrightarrow> untyped_min_bits \<le> us) 583 \<and> (type = Structures_A.CapTableObject \<longrightarrow> us \<noteq> 0)) 584 (Untyped_D.retype_region 585 us (translate_object_type type) (map (retype_transform_obj_ref type us) (retype_addrs ptr type n us))) 586 (Retype_A.retype_region ptr n us type dev)" 587 supply if_cong[cong] 588 apply (simp add: retype_region_def Untyped_D.retype_region_def 589 split del: if_split) 590 apply (clarsimp simp:when_def generate_object_ids_def bind_assoc 591 split del:if_split) 592 apply (simp add:retype_addrs_fold split del:if_split) 593 apply (case_tac "type = Structures_A.Untyped") 594 apply (rule corres_guard_imp) 595 apply (simp add:translate_object_type_def) 596 apply (intro conjI impI ballI | simp)+ 597 apply (simp add:gets_fold_into_modify retype_addrs_fold retype_region_ext_def modify_modify 598 create_objects_def) 599 apply (rule dcorres_expand_pfx) 600 apply clarsimp 601 apply (rule corres_guard_imp) 602 apply (rule corres_split) 603 apply (rule corres_trivial) 604 apply simp 605 apply (rule_tac r = dc and Q = \<top> and Q' = "(=) s'" in corres_guard_imp) 606 apply (clarsimp simp: transform_def bind_def simpler_modify_def corres_underlying_def 607 transform_current_thread_def transform_cdt_def transform_asid_table_def) 608 apply (rule ext) 609 apply (clarsimp simp:foldr_upd_app_if foldr_fun_upd_value restrict_map_def map_add_def 610 transform_objects_def retype_transform_obj_ref_def image_def) 611 apply (subgoal_tac "idle_thread s' \<notin> set (retype_addrs ptr type n us)") 612 apply (subgoal_tac "type = Structures_A.CapTableObject \<longrightarrow> us \<noteq> 0") 613 apply (clarsimp simp:transform_default_object translate_object_type_not_untyped) 614 defer 615 apply clarsimp 616 apply (frule invs_valid_idle,clarsimp simp:valid_idle_def pred_tcb_at_def obj_at_def) 617 apply (erule(3) pspace_no_overlapC) 618 apply clarsimp 619 apply simp 620 apply assumption 621 apply wp+ 622 apply fastforce 623 apply simp 624 apply (case_tac type, simp_all add:translate_object_type_def) 625 apply (rename_tac aobject_type) 626 apply (case_tac aobject_type,simp_all) 627 done 628 629lemma page_objects_default_object: 630 "ty \<in> ArchObject ` {SmallPageObj, LargePageObj, SectionObj, SuperSectionObj} 631 \<Longrightarrow> \<exists>vmsz. (default_object ty dev us = ArchObj (DataPage dev vmsz) \<and> pageBitsForSize vmsz = obj_bits_api ty us)" 632 by (auto simp: default_object_def default_arch_object_def obj_bits_api_def pageBitsForSize_def) 633 634lemma clearMemory_unused_corres_noop: 635 "\<lbrakk> ty \<in> ArchObject ` {SmallPageObj, LargePageObj, SectionObj, SuperSectionObj}; 636 range_cover ptr sz (obj_bits_api ty us) n; 637 p \<in> set (retype_addrs ptr ty n us)\<rbrakk> 638 \<Longrightarrow> dcorres dc \<top> 639 (\<lambda>s. (\<forall>x \<in> set (retype_addrs ptr ty n us). 640 obj_at (\<lambda>ko. ko = Retype_A.default_object ty dev us) x s 641 \<and> (\<forall>cap\<in>ran (caps_of_state s). x \<notin> (obj_refs cap))) 642 \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_idle s \<and> valid_etcbs s) 643 (return ()) 644 (do_machine_op (clearMemory p (2 ^ (obj_bits_api ty us))))" 645 (is "\<lbrakk> ?def; ?szv; ?in \<rbrakk> \<Longrightarrow> dcorres dc \<top> ?P ?f ?g") 646 apply (drule page_objects_default_object[where us=us and dev = dev], clarsimp) 647 apply (rename_tac pgsz) 648 apply (simp add: clearMemory_def do_machine_op_bind 649 cleanCacheRange_PoU_def ef_storeWord 650 mapM_x_mapM dom_mapM) 651 apply (subst do_machine_op_bind) 652 apply (clarsimp simp: ef_storeWord 653 mapM_x_mapM dom_mapM cleanCacheRange_PoU_def cleanByVA_PoU_def)+ 654 apply (rule corres_guard_imp, rule corres_split_noop_rhs) 655 apply (rule dcorres_machine_op_noop, wp) 656 apply (rule corres_mapM_to_mapM_x) 657 apply (rule_tac P=\<top> and P'="?P" 658 and S="Id \<inter> ({p .. p + 2 ^ (obj_bits_api ty us) - 1} \<times> UNIV)" 659 in corres_mapM_x[where f="\<lambda>_. return ()", OF _ _ _ refl, 660 simplified mapM_x_return]) 661 apply clarsimp 662 apply (rule stronger_corres_guard_imp, 663 rule_tac sz=pgsz in dcorres_store_word_safe[where dev = dev]) 664 apply (simp add: within_page_def) 665 apply simp 666 apply (clarsimp simp: obj_at_def) 667 apply (subgoal_tac "y && ~~ mask (obj_bits_api ty us) = p") 668 apply (clarsimp simp: ipc_frame_wp_at_def obj_at_def ran_null_filter 669 split: cap.split_asm arch_cap.split_asm) 670 apply (cut_tac t="(t, tcb_cnode_index 4)" and P="(=) cap" for t cap 671 in cte_wp_at_tcbI, simp, fastforce, simp) 672 apply (clarsimp simp: cte_wp_at_caps_of_state) 673 apply (drule(1) bspec) 674 apply clarsimp 675 apply (drule(1) bspec[OF _ ranI]) 676 apply simp 677 apply (drule(2) retype_addrs_aligned 678 [OF _ range_cover.aligned range_cover_sz' 679 [where 'a=32, folded word_bits_def] le_refl]) 680 apply (simp add:mask_in_range) 681 apply wp 682 apply (simp | wp hoare_vcg_ball_lift)+ 683 apply (simp add:zip_same_conv_map) 684 apply (rule conjI) 685 apply clarsimp 686 apply (clarsimp simp: word_size_def) 687 apply (drule subsetD[OF upto_enum_step_subset]) 688 apply simp 689 apply (wp | simp)+ 690 done 691 692lemma init_arch_objects_corres_noop: 693 notes [simp del] = atLeastAtMost_iff atLeastatMost_subset_iff 694 shows 695 "\<lbrakk> \<forall>x \<in> set refs. is_aligned x (obj_bits_api ty obj_sz); 696 range_cover ptr sz (obj_bits_api ty obj_sz) n; 0 < n \<rbrakk> 697 \<Longrightarrow> dcorres dc \<top> 698 (\<lambda>s. (ty \<noteq> Structures_A.Untyped \<longrightarrow> 699 (\<forall>x\<in>set (retype_addrs ptr ty n obj_sz). 700 obj_at (\<lambda>ko. ko = Retype_A.default_object ty dev obj_sz) x s)) 701 \<and> (\<forall>cap \<in> ran (null_filter (caps_of_state s)). 702 obj_refs cap \<inter> {ptr .. (ptr && ~~ mask sz) + 2 ^ sz - 1} = {}) 703 \<and> valid_objs s \<and> pspace_aligned s \<and> pspace_distinct s \<and> valid_idle s \<and> valid_etcbs s) 704 (return ()) 705 (init_arch_objects ty ptr n obj_sz refs)" 706 apply (simp add: init_arch_objects_def 707 split: Structures_A.apiobject_type.split aobject_type.split) 708 apply (simp add: dcorres_machine_op_noop[THEN corres_guard_imp] 709 cleanCacheRange_PoU_def machine_op_lift) 710 apply safe 711 apply (simp add:mapM_x_mapM) 712 apply (rule corres_guard_imp) 713 apply (rule corres_split_noop_rhs) 714 apply (rule corres_noop[where P=\<top> and P'=valid_idle]) 715 apply (simp add: clearMemory_def do_machine_op_bind 716 cleanCacheRange_PoU_def ef_storeWord 717 mapM_x_mapM dom_mapM) 718 apply (wp mapM_wp' dmo_dwp | simp)+ 719 apply (rule corres_noop[where P=\<top> and P'=valid_idle]) 720 apply simp 721 apply (rule hoare_strengthen_post, rule mapM_wp') 722 apply (subst eq_commute, wp copy_global_mappings_dwp) 723 apply (simp add: obj_bits_api_def arch_kobj_size_def 724 default_arch_object_def pd_bits_def pageBits_def) 725 apply (wp mapM_wp' dmo_dwp | simp)+ 726 done 727 728lemma monad_commute_set_cap_cdt: 729 "monad_commute \<top> (KHeap_D.set_cap ptr cap) (modify (\<lambda>s. s\<lparr>cdl_cdt := cdl_cdt s(ptr2 \<mapsto> ptr3)\<rparr>))" 730 apply (clarsimp simp:monad_commute_def) 731 apply (rule sym) 732 apply (subst bind_assoc[symmetric]) 733 apply (subst oblivious_modify_swap) 734 apply (simp add: KHeap_D.set_cap_def split_def gets_the_def 735 KHeap_D.set_object_def) 736 apply (intro oblivious_bind oblivious_assert impI conjI allI oblivious_select | 737 simp split: cdl_object.split)+ 738 apply (clarsimp simp:bind_assoc) 739 done 740 741lemma monad_commute_set_cap_assert: 742 "monad_commute \<top> (KHeap_D.set_cap ptr cap) (assert F)" 743 apply (simp add: monad_commute_def 744 assert_def fail_def bind_def return_def) 745 apply (subgoal_tac "empty_fail (KHeap_D.set_cap ptr cap)") 746 apply (clarsimp simp:empty_fail_def) 747 apply fastforce 748 apply (simp add:KHeap_D.set_cap_def split_def) 749 apply (wp|wpc|clarsimp split:cdl_object.splits)+ 750 apply (simp add:KHeap_D.set_object_def) 751 done 752 753lemma monad_commute_set_cap_gets_cdt: 754 "monad_commute \<top> (KHeap_D.set_cap ptr cap) (gets cdl_cdt)" 755 apply (simp add: monad_commute_def gets_def get_def 756 assert_def fail_def bind_def return_def) 757 apply auto[1] 758 apply (rule bexI[rotated]) 759 apply simp 760 apply simp 761 apply (drule use_valid) 762 apply (rule KHeap_D_set_cap_cdl_cdt) 763 prefer 2 764 apply (fastforce +)[2] 765 apply (rule bexI[rotated]) 766 apply simp 767 apply simp 768 apply (drule use_valid) 769 apply (rule KHeap_D_set_cap_cdl_cdt) 770 prefer 2 771 apply (fastforce +)[2] 772 done 773 774lemma set_cap_set_parent_swap: 775 "do _ \<leftarrow> KHeap_D.set_cap ptr cap; set_parent ptr2 ptr3 od 776 = do _ \<leftarrow> set_parent ptr2 ptr3; KHeap_D.set_cap ptr cap od" 777 apply (rule bind_return_eq) 778 apply (subst bind_assoc)+ 779 apply (rule ext) 780 apply (subst monad_commute_simple) 781 apply (simp add:set_parent_def) 782 apply (rule monad_commute_split)+ 783 apply (rule monad_commute_set_cap_cdt) 784 apply (rule monad_commute_set_cap_assert) 785 apply wp 786 apply (rule monad_commute_set_cap_gets_cdt) 787 apply clarsimp 788 apply fastforce 789 apply fastforce 790 done 791 792lemma transform_default_cap: 793 "transform_cap (default_cap type ptr sz dev) 794 = Types_D.default_cap (translate_object_type type) 795 (retype_transform_obj_ref type sz ptr) sz dev" 796 by (cases type, 797 simp_all add: translate_object_type_def Types_D.default_cap_def 798 free_range_of_untyped_def 799 transform_cap_def arch_default_cap_def transform_mapping_def 800 retype_transform_obj_ref_def vm_read_write_def Nitpick.The_psimp 801 transform_asid_def asid_high_bits_of_def asid_low_bits_def 802 split: aobject_type.split) 803 804crunch valid_etcbs[wp]: create_cap_ext valid_etcbs 805 806lemma create_cap_dcorres: 807 "dcorres dc \<top> (cte_at parent and cte_wp_at ((=) cap.NullCap) slot 808 and not_idle_thread (fst slot) and valid_idle and valid_etcbs 809 and (\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s))) 810 (Untyped_D.create_cap (translate_object_type type) sz (transform_cslot_ptr parent) dev 811 (transform_cslot_ptr slot, retype_transform_obj_ref type sz ptr)) 812 (Retype_A.create_cap type sz parent dev (slot, ptr))" 813 supply if_cong[cong] 814 apply (simp add: Untyped_D.create_cap_def Retype_A.create_cap_def) 815 apply (rule stronger_corres_guard_imp) 816 apply (rule corres_gets_the_bind) 817 apply (rule corres_underlying_gets_pre_lhs) 818 apply (rule corres_assert_lhs) 819 apply (simp add: set_cap_set_parent_swap bind_assoc[symmetric]) 820 apply (rule corres_split_nor) 821 apply (fold dc_def) 822 apply (rule set_cap_corres, simp_all add: transform_default_cap)[1] 823 apply (simp add: bind_assoc set_original_def create_cap_ext_def 824 set_cdt_modify gets_fold_into_modify update_cdt_list_def 825 modify_modify set_cdt_list_modify) 826 apply (rule dcorres_set_parent_helper) 827 apply (rule_tac P'="\<lambda>s. mdb_cte_at (swp cte_at s) (cdt s) 828 \<and> cte_at parent s \<and> cte_at slot s" 829 in corres_modify[where P=\<top>]) 830 apply (clarsimp simp: transform_def transform_current_thread_def 831 transform_asid_table_def transform_objects_def) 832 apply (simp add: transform_cdt_def fun_upd_def[symmetric]) 833 apply (subst map_lift_over_upd) 834 apply (rule_tac P=\<top> and s=s' in transform_cdt_slot_inj_on_cte_at) 835 apply (auto dest: mdb_cte_atD[rotated] elim!: ranE)[1] 836 apply simp 837 apply (wp|simp)+ 838 apply (clarsimp simp: cte_wp_at_caps_of_state caps_of_state_transform_opt_cap not_idle_thread_def) 839 apply (clarsimp simp: swp_def not_idle_thread_def cte_wp_at_caps_of_state) 840 apply (drule mdb_cte_at_cdt_null) 841 apply (clarsimp simp:cte_wp_at_caps_of_state swp_def) 842 apply (fastforce simp:mdb_cte_at_def) 843 done 844 845lemma set_cap_default_not_none: 846 "\<lbrace>\<lambda>s. cte_wp_at (\<lambda>x. slot \<noteq> ptr \<longrightarrow> x \<noteq> cap.NullCap) slot s\<rbrace> CSpaceAcc_A.set_cap (Retype_A.default_cap type a b dev) ptr 847 \<lbrace>\<lambda>rv s. cte_wp_at ((\<noteq>) cap.NullCap) slot s\<rbrace>" 848 apply (clarsimp simp:cte_wp_at_caps_of_state valid_def) 849 apply (drule set_cap_caps_of_state_monad) 850 apply clarsimp 851 done 852 853lemma create_cap_mdb_cte_at: 854 "\<lbrace>\<lambda>s. mdb_cte_at (swp (cte_wp_at ((\<noteq>)cap.NullCap)) s) (cdt s) 855 \<and> cte_wp_at ((\<noteq>)cap.NullCap) parent s \<and> cte_at (fst tup) s\<rbrace> 856 create_cap type sz parent dev tup \<lbrace>\<lambda>rv s. mdb_cte_at (swp (cte_wp_at ((\<noteq>)cap.NullCap)) s) (cdt s)\<rbrace>" 857 apply (simp add: create_cap_def split_def mdb_cte_at_def) 858 apply (wp hoare_vcg_all_lift set_cap_default_not_none set_cdt_cte_wp_at static_imp_wp dxo_wp_weak 859 | simp | wps)+ 860 apply (fastforce simp: cte_wp_at_caps_of_state) 861 done 862 863lemma neg_mask_add_2p_helper: 864 "\<lbrakk>is_aligned (b::word32) us;us < 32\<rbrakk> \<Longrightarrow> b + 2 ^ us - 1 && ~~ mask us = b" 865 apply (simp add:p_assoc_help) 866 apply (rule is_aligned_add_helper[THEN conjunct2]; simp add:less_1_helper) 867 done 868 869lemma retype_transform_ref_subseteq_strong: 870 "\<lbrakk>p \<in> set (retype_addrs ptr ty n us);range_cover ptr sz (obj_bits_api ty us) n \<rbrakk> 871 \<Longrightarrow> retype_transform_obj_ref ty us p \<subseteq> {ptr..ptr + of_nat n * (2::word32) ^ obj_bits_api ty us - 1}" 872 apply (subgoal_tac "{p .. p + 2 ^ obj_bits_api ty us - 1} 873 \<subseteq> {ptr..ptr + of_nat n * 2 ^ obj_bits_api ty us - 1}") 874 apply (erule subset_trans[rotated]) 875 apply (clarsimp simp:retype_transform_obj_ref_def) 876 apply (rule conjI) 877 apply (clarsimp simp:obj_bits_api_def) 878 apply clarsimp 879 apply (rule is_aligned_no_overflow) 880 apply (erule retype_addrs_aligned) 881 apply (erule range_cover.aligned) 882 apply (drule range_cover.sz,simp add:word_bits_def) 883 apply (erule range_cover.sz) 884 apply (case_tac "n = 0") 885 apply (clarsimp simp:retype_addrs_def) 886 apply (frule(1) retype_addrs_range_subset) 887 apply clarsimp 888 proof - 889 assume cover:"range_cover ptr sz (obj_bits_api ty us) n" 890 and mem_p:"p \<in> set (retype_addrs ptr ty n us)" 891 and not_0:"0 < n" 892 note n_less = range_cover.range_cover_n_less[OF cover] 893 have unat_of_nat_m1: "unat (of_nat n - (1::word32)) < n" 894 using not_0 n_less 895 by (simp add:unat_of_nat_minus_1) 896 have decomp:"of_nat n * 2 ^ obj_bits_api ty us = of_nat (n - 1) * 2 ^ obj_bits_api ty us 897 + (2 :: word32) ^ obj_bits_api ty us" 898 apply (simp add:distrib_right[where b = "1::'a::len word",simplified,symmetric]) 899 using not_0 n_less 900 apply (simp add:unat_of_nat_minus_1 obj_bits_api_def3) 901 done 902 show "p + 2 ^ obj_bits_api ty us - 1 \<le> ptr + of_nat n * 2 ^ obj_bits_api ty us - 1" 903 apply (subst decomp) 904 apply (simp add:add.assoc[symmetric]) 905 apply (simp add:p_assoc_help) 906 apply (rule order_trans[OF word_plus_mono_left word_plus_mono_right]) 907 using mem_p not_0 908 apply (clarsimp simp:retype_addrs_def ptr_add_def shiftl_t2n) 909 apply (rule word_plus_mono_right) 910 apply (rule word_mult_le_mono1[OF word_of_nat_le]) 911 using n_less not_0 912 apply (subst unat_of_nat_minus_1) 913 apply simp 914 apply simp 915 apply (simp add:Set_Interval.ord_class.atLeastLessThan_def) 916 apply (rule p2_gt_0[THEN iffD2]) 917 using cover 918 apply (simp add:word_bits_def range_cover_def) 919 apply (simp only: word_bits_def[symmetric]) 920 using not_0 n_less 921 apply (clarsimp simp: unat_of_nat_minus_1) 922 apply (subst unat_power_lower) 923 using cover 924 apply (simp add:range_cover_def) 925 apply (rule nat_less_power_trans2[OF range_cover.range_cover_le_n_less(2),OF cover, folded word_bits_def]) 926 apply (simp add:unat_of_nat_m1 less_imp_le) 927 using cover 928 apply (simp add:range_cover_def word_bits_def) 929 apply (rule machine_word_plus_mono_right_split[where sz = sz]) 930 using range_cover.range_cover_compare[OF cover,where p = "unat (of_nat n - (1::word32))"] 931 apply (clarsimp simp:unat_of_nat_m1) 932 using cover 933 apply (simp add:range_cover_def word_bits_def) 934 apply (rule olen_add_eqv[THEN iffD2]) 935 apply (subst add.commute[where a = "2^(obj_bits_api ty us) - 1"]) 936 apply (subst p_assoc_help[symmetric]) 937 apply (rule is_aligned_no_overflow) 938 apply (insert cover) 939 apply (clarsimp simp:range_cover_def) 940 apply (erule aligned_add_aligned[OF _ is_aligned_mult_triv2]) 941 apply (simp add:range_cover_def)+ 942 done 943 qed 944 945lemma generate_object_ids_exec: 946 notes [simp del] = order_class.Icc_eq_Icc 947 shows 948 "dcorres r P P' (f (map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))) g 949 \<Longrightarrow> dcorres r P 950 (K ((ty = Structures_A.Untyped \<longrightarrow> (untyped_min_bits \<le> us)) 951 \<and> range_cover ptr sz (obj_bits_api ty us) n 952 \<and> is_aligned ptr (obj_bits_api ty us) 953 \<and> {ptr..ptr + of_nat n * 2 ^ obj_bits_api ty us - 1} \<subseteq> free_range ) 954 and (pspace_no_overlap_range_cover ptr sz) and valid_pspace and valid_idle and P') 955 (do 956 t \<leftarrow> generate_object_ids n (translate_object_type ty) free_range; 957 f t 958 od) g" 959 apply (clarsimp simp: generate_object_ids_def bind_assoc) 960 apply (rule dcorres_absorb_get_l) 961 apply (rule corres_guard_imp) 962 apply (rule_tac x = "(map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us))" 963 in select_pick_corres_asm[rotated]) 964 apply (rule corres_symb_exec_l) 965 apply (rule_tac F = "rv = map (retype_transform_obj_ref ty us) (retype_addrs ptr ty n us)" 966 in corres_gen_asm) 967 apply clarify 968 apply assumption 969 apply (clarsimp simp:return_def exs_valid_def) 970 apply (rule hoare_vcg_if_split) 971 apply (wp|simp)+ 972 apply (intro conjI impI) 973 apply (clarsimp simp:distinct_map distinct_retype_addrs) 974 apply (clarsimp simp:inj_on_def) 975 apply (clarsimp simp:retype_transform_obj_ref_def split: if_split_asm) 976 apply (frule range_cover.sz(1)) 977 apply (drule(1) retype_addrs_aligned[where sz = sz]) 978 apply (clarsimp simp:word_bits_def) 979 apply (erule range_cover.sz) 980 apply (drule(1) retype_addrs_aligned[where sz = sz]) 981 apply (clarsimp simp:word_bits_def) 982 apply (erule range_cover.sz) 983 apply (subst (asm) range_eq) 984 apply (clarsimp simp: obj_bits_api_def) 985 apply simp 986 apply (clarsimp simp:retype_transform_obj_ref_def split:if_splits) 987 apply (frule range_cover.sz(1)) 988 apply (drule(1) retype_addrs_aligned[where sz = sz]) 989 apply (clarsimp simp:word_bits_def) 990 apply (erule range_cover.sz) 991 apply (drule(1) retype_addrs_aligned[where sz = sz]) 992 apply (clarsimp simp:word_bits_def) 993 apply (erule range_cover.sz) 994 apply (clarsimp simp:obj_bits_api_def order_class.Icc_eq_Icc) 995 apply (drule_tac x = b in neg_mask_mono_le[where n = us]) 996 apply (drule_tac x = a in neg_mask_mono_le[where n = us]) 997 apply (clarsimp simp: neg_mask_add_2p_helper dest!: range_cover_sz') 998 apply (clarsimp) 999 apply (intro conjI) 1000 apply (clarsimp simp:retype_transform_obj_ref_def) 1001 apply (rule is_aligned_no_overflow) 1002 apply (drule(1) retype_addrs_aligned[where sz = sz]) 1003 apply (clarsimp simp:word_bits_def dest!:range_cover.sz(1)) 1004 apply (erule range_cover.sz) 1005 apply (simp add:obj_bits_api_def) 1006 apply (erule(2) subset_trans[OF retype_transform_ref_subseteq_strong]) 1007 apply (rule retype_transform_obj_ref_available) 1008 apply simp+ 1009 apply (clarsimp simp:retype_transform_obj_ref_def translate_object_type_def) 1010 apply simp 1011 done 1012 1013lemma create_caps_loop_dcorres: 1014 "dcorres dc \<top> 1015 (\<lambda>s. cte_wp_at ((\<noteq>) cap.NullCap) parent s \<and> valid_idle s \<and> mdb_cte_at (swp (cte_wp_at ((\<noteq>) cap.NullCap)) s) (cdt s) 1016 \<and> idle_thread s \<notin> fst ` fst ` set targets 1017 \<and> distinct (parent # map fst targets) 1018 \<and> (\<forall>tup \<in> set targets. cte_wp_at ((=) cap.NullCap) (fst tup) s) \<and> valid_etcbs s) 1019 (mapM_x 1020 (\<lambda>x. Untyped_D.create_cap (translate_object_type type) sz 1021 (transform_cslot_ptr parent) dev 1022 (transform_cslot_ptr (fst x), retype_transform_obj_ref type sz (snd x))) 1023 targets) 1024 (mapM_x (Retype_A.create_cap type sz parent dev) targets)" 1025 apply (induct targets) 1026 apply (simp add: mapM_x_Nil) 1027 apply (clarsimp simp: mapM_x_Cons) 1028 apply (rule corres_guard_imp) 1029 apply (erule corres_split_nor) 1030 apply (rule create_cap_dcorres) 1031 apply (wp create_cap_invs hoare_vcg_const_Ball_lift create_cap_mdb_cte_at[unfolded swp_def])+ 1032 apply simp 1033 apply (clarsimp simp: not_idle_thread_def swp_def) 1034 apply (auto simp: cte_wp_at_caps_of_state image_def) 1035 done 1036 1037crunch valid_idle[wp]: init_arch_objects "valid_idle" 1038 (wp: crunch_wps hoare_unless_wp ignore: clearMemory) 1039 1040lemma update_available_range_dcorres: 1041 "dcorres dc \<top> ( K(\<exists>idx. untyped_cap = transform_cap (cap.UntypedCap dev ptr sz idx) 1042 \<and> free_range_of_untyped idx' sz ptr \<subseteq> new_range - set oids) 1043 and valid_idle and (\<lambda>s. fst cref \<noteq> idle_thread s) and valid_etcbs) 1044 (update_available_range new_range oids 1045 (transform_cslot_ptr cref) untyped_cap) 1046 (CSpaceAcc_A.set_cap 1047 (cap.UntypedCap dev ptr sz idx') 1048 cref)" 1049 apply (rule dcorres_expand_pfx) 1050 apply (clarsimp simp:update_available_range_def) 1051 apply (rule corres_guard_imp) 1052 apply (rule select_pick_corres) 1053 apply (rule set_cap_corres) 1054 apply clarsimp 1055 apply simp+ 1056 done 1057 1058lemma subseteq_set_minus: 1059 "\<lbrakk>A \<subseteq> B; A\<inter> C = {}\<rbrakk> \<Longrightarrow> A \<subseteq> B - C" 1060 by auto 1061 1062lemma free_range_of_untyped_subseteq: 1063 "range_cover (ptr::word32) sz us n \<Longrightarrow> 1064 free_range_of_untyped (unat ((ptr && mask sz) + (of_nat n * 2^us))) sz (ptr &&~~ mask sz) 1065 \<subseteq> {ptr.. (ptr &&~~ mask sz) + 2 ^ sz - 1}" 1066 unfolding free_range_of_untyped_def 1067 apply clarsimp 1068 apply (subst AND_NOT_mask_plus_AND_mask_eq[symmetric,where n = sz]) 1069 apply (rule word_plus_mono_right) 1070 apply (drule range_cover.range_cover_base_le) 1071 apply (clarsimp simp:shiftl_t2n field_simps) 1072 apply (rule is_aligned_no_wrap'[OF is_aligned_neg_mask]) 1073 apply (rule le_refl) 1074 apply (rule word32_less_sub_le[THEN iffD1]) 1075 apply (simp add: range_cover_def word_bits_def) 1076 apply (simp add: word_le_nat_alt range_cover_def unat_2p_sub_1) 1077 done 1078 1079lemma retype_addrs_range_subset_strong: 1080 notes [simp del] = atLeastAtMost_iff atLeastatMost_subset_iff 1081 shows "\<lbrakk>p \<in> set (retype_addrs ptr ty n us); range_cover ptr sz (obj_bits_api ty us) n\<rbrakk> 1082 \<Longrightarrow> {p..p + 2 ^ obj_bits_api ty us - 1} \<subseteq> {ptr..ptr + of_nat n * 2 ^ obj_bits_api ty us - 1}" 1083 apply (clarsimp simp: retype_addrs_def ptr_add_def) 1084 apply (drule_tac p = x in range_cover_subset) 1085 apply clarsimp+ 1086 apply blast 1087 done 1088 1089lemma le_p2_minus_1: 1090 "a \<le> (2^z - (Suc 0::nat)) \<Longrightarrow> a < 2^z" 1091 apply (subgoal_tac "(0 :: nat)< 2^z") 1092 apply arith 1093 apply simp 1094 done 1095 1096lemma free_range_of_untyped_subseteq': 1097 "\<lbrakk>a \<le> a'; is_aligned ptr sz; sz < size (ptr)\<rbrakk> 1098 \<Longrightarrow> free_range_of_untyped a' sz ptr \<subseteq>free_range_of_untyped a sz ptr" 1099 apply (clarsimp simp:free_range_of_untyped_def) 1100 apply (rule word_plus_mono_right) 1101 apply (drule le_p2_minus_1) 1102 apply (rule of_nat_mono_maybe_le[THEN iffD1,rotated -1]) 1103 apply simp 1104 apply (erule less_le_trans) 1105 apply (simp add: word_size) 1106 apply (drule(1) le_less_trans) 1107 apply (erule less_le_trans) 1108 apply (simp add: word_size) 1109 apply (erule is_aligned_no_wrap') 1110 apply (rule word_of_nat_less) 1111 apply (drule le_p2_minus_1) 1112 apply (simp add: word_size) 1113 done 1114 1115lemma retype_transform_obj_ref_not_empty: 1116 "\<lbrakk>range_cover ptr sz (obj_bits_api tp us) n; 1117 is_aligned ptr (obj_bits_api tp us); 1118 y \<in> set (retype_addrs ptr tp n us)\<rbrakk> 1119 \<Longrightarrow> (retype_transform_obj_ref tp us y) \<noteq> {}" 1120 apply (frule(1) retype_addrs_aligned) 1121 apply (drule range_cover.sz,simp add:word_bits_def) 1122 apply (erule range_cover.sz) 1123 apply (clarsimp simp:retype_addrs_def retype_transform_obj_ref_def ptr_add_def) 1124 apply (rule is_aligned_no_overflow) 1125 apply (simp add:obj_bits_api_def) 1126 done 1127 1128lemma in_empty_setE: 1129 "\<lbrakk>x\<in> A;x\<in> B; A\<inter> B = {}\<rbrakk> \<Longrightarrow> Q" 1130 by blast 1131 1132lemma free_range_of_untyped_pick_retype_addrs: 1133 notes [simp del] = atLeastAtMost_iff 1134 shows "\<lbrakk>range_cover ptr sz (obj_bits_api tp us) (length slots) ; slots \<noteq> []\<rbrakk> \<Longrightarrow> 1135 free_range_of_untyped (unat ((ptr && mask sz) + (of_nat (length slots) << obj_bits_api tp us))) sz (ptr && ~~ mask sz) \<inter> 1136 (\<lambda>a. pick (retype_transform_obj_ref tp us a)) ` set (retype_addrs ptr tp (length slots) us) = 1137 {}" 1138 apply (clarsimp simp:image_def free_range_of_untyped_def) 1139 apply (rule disjointI) 1140 apply (drule CollectD) 1141 apply clarsimp 1142 apply (frule retype_transform_obj_ref_not_empty) 1143 apply (erule range_cover.aligned) 1144 apply simp 1145 apply (drule(1) retype_transform_ref_subseteq_strong) 1146 apply (drule nonempty_pick_in) 1147 apply (drule(1) set_mp[rotated]) 1148 apply (clarsimp simp:shiftl_t2n field_simps) 1149 apply (erule(1) in_empty_setE) 1150 apply clarsimp 1151 apply (drule leD[where y = "(ptr && mask sz) + ((ptr && ~~ mask sz) 1152 + of_nat (length slots) * 2 ^ obj_bits_api tp us)"]) 1153 apply (subgoal_tac " ptr + of_nat (length slots) * 2 ^ obj_bits_api tp us - 1 < 1154 (ptr && mask sz) + ((ptr && ~~ mask sz) + of_nat (length slots) * 2 ^ obj_bits_api tp us)") 1155 apply simp 1156 apply (subst group_add_class.add_diff_eq[symmetric]) 1157 apply (frule range_cover_not_zero_shift[rotated,OF _ le_refl]) 1158 apply simp 1159 apply (thin_tac "\<not>P" for P) 1160 apply (subst add.assoc[symmetric]) 1161 apply (subst AND_NOT_mask_plus_AND_mask_eq[symmetric,where n = sz]) 1162 apply (subst add.commute[where a = "(ptr && mask sz)"]) 1163 apply (rule word_plus_strict_mono_right) 1164 apply (rule word_leq_le_minus_one) 1165 apply simp 1166 apply (simp add:shiftl_t2n field_simps) 1167 apply (subst add.assoc) 1168 apply (rule word_plus_mono_right) 1169 apply (simp add:word_le_nat_alt) 1170 apply (simp add: range_cover_unat) 1171 apply (rule is_aligned_no_wrap'[OF is_aligned_neg_mask]) 1172 apply (rule le_refl) 1173 apply (drule le_p2_minus_1) 1174 apply (simp add:word_less_nat_alt) 1175 apply (subst unat_power_lower32[unfolded word_bits_def]) 1176 apply (erule range_cover.sz) 1177 apply simp 1178 done 1179 1180lemma clearMemory_corres_noop: 1181 "full_sz = 2 ^ sz \<Longrightarrow> is_aligned p sz \<Longrightarrow> 2 \<le> sz 1182 \<Longrightarrow> sz < word_bits 1183 \<Longrightarrow> dcorres dc \<top> 1184 (pspace_no_overlap {p .. p + 2 ^ sz - 1} and valid_objs and valid_etcbs) 1185 (return ()) 1186 (do_machine_op (clearMemory p full_sz))" 1187 apply (simp add: clearMemory_def freeMemory_def[symmetric] 1188 do_machine_op_bind empty_fail_freeMemory) 1189 apply (rule corres_guard_imp) 1190 apply (rule corres_add_noop_lhs) 1191 apply (rule corres_split_nor[OF _ freeMemory_dcorres]) 1192 apply (rule dcorres_machine_op_noop) 1193 apply (wp | simp)+ 1194 apply (clarsimp simp: field_simps) 1195 done 1196 1197lemma mapME_x_upt_length_ys: 1198 "mapME_x (\<lambda>_. f) [0 ..< length ys] 1199 = mapME_x (\<lambda>_. f) ys" 1200 by (metis mapME_x_map_simp[where f="\<lambda>_. ()" and m="\<lambda>_. m" for m, 1201 unfolded o_def] map_replicate_const length_upt minus_nat.diff_0) 1202 1203lemma monadic_set_cap_id: 1204 "monadic_rewrite False True 1205 (cte_wp_at ((=) cap) p) 1206 (set_cap cap p) (return ())" 1207 by (clarsimp simp: monadic_rewrite_def set_cap_id return_def) 1208 1209lemmas monadic_set_cap_id2 1210 = monadic_rewrite_transverse[OF monadic_set_cap_id monadic_rewrite_refl] 1211 1212lemma monadic_rewrite_corres_rhs: 1213 "\<lbrakk> monadic_rewrite False True Q c c'; 1214 corres_underlying R F F' r P P' a c' \<rbrakk> 1215 \<Longrightarrow> corres_underlying R F F' r P (P' and Q) a c" 1216 apply (clarsimp simp: corres_underlying_def monadic_rewrite_def) 1217 apply fastforce 1218 done 1219 1220(* FIXME: move *) 1221lemma mapME_x_append: 1222 "mapME_x f (xs @ ys) = (doE mapME_x f xs; mapME_x f ys odE)" 1223 apply (induct xs) 1224 apply (simp add: mapME_x_Nil) 1225 apply (simp add: mapME_x_Cons bindE_assoc) 1226 done 1227 1228lemma hd_filter_eq: 1229 "P (hd xs) \<Longrightarrow> hd (filter P xs) = hd xs" 1230 by (cases xs, simp_all) 1231 1232lemma free_range_of_untyped_subset'[rule_format]: 1233 assumes al: "is_aligned ptr sz" 1234 and sz: "sz < size (ptr)" 1235 shows "a < a' \<longrightarrow> a < 2 ^ sz \<longrightarrow> free_range_of_untyped a' sz ptr \<subset> free_range_of_untyped a sz ptr" 1236proof - 1237 note no_ov = is_aligned_no_overflow'[OF al] 1238 note mono = word_plus_mono_right[OF _ no_ov, simplified field_simps] 1239 note sz_len = sz[unfolded word_size] 1240(* 1241 note sz_simp[simp] = unat_2p_sub_1[OF sz_len] unat_power_lower[OF sz_len] 1242*) 1243 show ?thesis using sz 1244 apply (intro impI psubsetI) 1245 apply (rule free_range_of_untyped_subseteq', simp_all add: al) 1246 apply (clarsimp simp:free_range_of_untyped_def) 1247 apply (strengthen mono word_of_nat_le)+ 1248 apply (simp add: sz_len unat_2p_sub_1) 1249 apply (intro conjI impI; (clarsimp dest!: le_p2_minus_1)?) 1250 apply (drule word_unat.Abs_eqD, simp_all add: unats_def word_size 1251 less_trans[OF _ power_strict_increasing[OF sz_len]]) 1252 done 1253qed 1254 1255lemma delete_objects_invs2: 1256 "\<lbrace>(\<lambda>s. \<exists>slot dev f. cte_wp_at ((=) (cap.UntypedCap dev ptr bits f)) slot s 1257 \<and> descendants_range (cap.UntypedCap dev ptr bits f) slot s) and 1258 invs and ct_active\<rbrace> 1259 delete_objects ptr bits \<lbrace>\<lambda>_. invs\<rbrace>" 1260 by (rule hoare_name_pre_state, clarsimp, wp delete_objects_invs, fast) 1261 1262lemma reset_untyped_cap_corres: 1263 notes delete_objects_invs[wp del] 1264 shows 1265 "dcorres (dc \<oplus> dc) \<top> (invs and valid_etcbs and ct_active 1266 and cte_wp_at (\<lambda>cap. is_untyped_cap cap \<and> free_index_of cap = idx) cref 1267 and (\<lambda>s. descendants_of cref (cdt s) = {})) 1268 (Untyped_D.reset_untyped_cap (transform_cslot_ptr cref)) 1269 (Retype_A.reset_untyped_cap cref)" 1270 supply if_cong[cong] 1271 apply (rule dcorres_expand_pfx) 1272 apply (clarsimp simp: cte_wp_at_caps_of_state is_cap_simps) 1273 apply (simp add: Untyped_D.reset_untyped_cap_def reset_untyped_cap_def 1274 liftE_bindE) 1275 apply (rule corres_guard_imp) 1276 apply (rule corres_split[OF _ get_cap_corres]) 1277 apply (rule_tac F="is_untyped_cap capa \<and> cap_aligned capa 1278 \<and> bits_of capa > 2 \<and> free_index_of capa \<le> 2 ^ bits_of capa" 1279 in corres_gen_asm2) 1280 apply (simp add: whenE_def if_flip split del: if_split) 1281 apply (rule corres_if) 1282 apply (clarsimp simp: is_cap_simps free_range_of_untyped_def 1283 cap_aligned_def free_index_of_def) 1284 apply (simp add: word_unat.Rep_inject[symmetric]) 1285 apply (subst unat_of_nat_eq, erule order_le_less_trans, 1286 rule power_strict_increasing, simp_all add: word_bits_def bits_of_def)[1] 1287 apply (rule corres_trivial, rule corres_returnOk, simp) 1288 apply (rule_tac F="free_index_of capa \<noteq> 0" in corres_gen_asm2) 1289 apply (rule corres_split_nor) 1290 prefer 2 1291 apply (rule delete_objects_dcorres) 1292 apply (clarsimp simp: is_cap_simps bits_of_def) 1293 apply (rule corres_if_rhs) 1294 apply (rule_tac x="[cap_objects (transform_cap capa)]" in select_pick_corres_asm) 1295 apply (clarsimp simp: is_cap_simps cap_aligned_def free_index_of_def) 1296 apply (rule order_less_le_trans, rule free_range_of_untyped_subset'[where a=0], 1297 simp_all)[1] 1298 apply (simp add: word_size word_bits_def) 1299 apply (simp add: free_range_of_untyped_def) 1300 1301 apply (simp add: mapME_x_Nil mapME_x_Cons liftE_def bind_assoc) 1302 apply (rule corres_add_noop_lhs) 1303 apply (rule corres_split_nor) 1304 prefer 2 1305 apply (rule dcorres_unless_r) 1306 apply (rule clearMemory_corres_noop[OF refl]) 1307 apply (clarsimp simp: is_cap_simps cap_aligned_def bits_of_def) 1308 apply (clarsimp simp: is_cap_simps bits_of_def free_range_of_untyped_def) 1309 apply (clarsimp simp: is_cap_simps cap_aligned_def bits_of_def) 1310 apply (rule corres_trivial, simp) 1311 apply (rule corres_split_nor) 1312 apply (rule corres_alternate1) 1313 apply (rule corres_trivial, simp add: returnOk_def) 1314 apply (rule set_cap_corres) 1315 apply (clarsimp simp: is_cap_simps bits_of_def free_range_of_untyped_def) 1316 apply simp 1317 apply (wp | simp add: unless_def)+ 1318 apply (rule_tac F="\<not> (is_device_untyped_cap capa \<or> bits_of capa < reset_chunk_bits) 1319 \<and> (\<exists>s. s \<turnstile> capa)" 1320 in corres_gen_asm2) 1321 apply (rule_tac x="map (\<lambda>i. free_range_of_untyped (i * 2 ^ reset_chunk_bits) 1322 (bits_of capa) (obj_ref_of capa)) xs" for xs 1323 in select_pick_corres_asm) 1324 prefer 2 1325 apply (simp add: mapME_x_map_simp o_def) 1326 apply (rule_tac P="\<top>\<top>" and P'="\<lambda>_. valid_objs 1327 and valid_etcbs and pspace_no_overlap (untyped_range capa) 1328 and valid_idle and (\<lambda>s. idle_thread s \<noteq> fst cref) 1329 and cte_wp_at (\<lambda>cp. \<exists>idx. cp = free_index_update (\<lambda>_. idx) capa) cref" 1330 in mapME_x_corres_same_xs[OF _ _ _ refl]) 1331 apply (rule corres_guard_imp) 1332 apply (rule corres_add_noop_lhs) 1333 apply (rule corres_split_nor[OF _ clearMemory_corres_noop[OF refl]]) 1334 apply (rule corres_split[OF _ set_cap_corres]) 1335 apply (subst alternative_com) 1336 apply (rule throw_or_return_preemption_corres[where P=\<top> and P'=\<top>]) 1337 apply (clarsimp simp: is_cap_simps bits_of_def) 1338 apply simp 1339 apply wp+ 1340 apply (clarsimp simp add: is_cap_simps cap_aligned_def bits_of_def 1341 aligned_add_aligned is_aligned_shiftl) 1342 apply (simp add: reset_chunk_bits_def) 1343 apply (simp add: reset_chunk_bits_def word_bits_def) 1344 apply (wp hoare_vcg_all_lift hoare_vcg_const_imp_lift 1345 preemption_point_inv' set_cap_no_overlap 1346 update_untyped_cap_valid_objs set_cap_idle 1347 | simp)+ 1348 apply (clarsimp simp: is_cap_simps bits_of_def cap_aligned_def) 1349 apply (erule pspace_no_overlap_subset) 1350 apply (rule aligned_range_offset_subset, simp_all add: is_aligned_shiftl)[1] 1351 apply (rule shiftl_less_t2n[OF word_of_nat_less]) 1352 apply simp 1353 apply (simp add: word_bits_def) 1354 apply wpsimp 1355 apply (wp hoare_vcg_all_lift hoare_vcg_const_imp_lift 1356 update_untyped_cap_valid_objs set_cap_no_overlap 1357 set_cap_idle preemption_point_inv' 1358 set_cap_cte_wp_at 1359 | simp)+ 1360 apply (clarsimp simp: cte_wp_at_caps_of_state exI 1361 is_cap_simps bits_of_def) 1362 apply (frule(1) cte_wp_at_valid_objs_valid_cap[OF caps_of_state_cteD]) 1363 apply (clarsimp simp: valid_cap_simps cap_aligned_def 1364 valid_untyped_pspace_no_overlap 1365 free_index_of_def) 1366 1367 apply (clarsimp simp: is_cap_simps bits_of_def) 1368 apply (strengthen order_trans[OF free_range_of_untyped_subseteq'[where a=0]] 1369 free_range_of_untyped_subset') 1370 apply (clarsimp simp: conj_comms) 1371 apply (clarsimp simp: filter_empty_conv bexI[where x=0] 1372 last_rev hd_map hd_filter_eq 1373 is_cap_simps bits_of_def cap_aligned_def 1374 word_bits_def word_size exI 1375 rev_map[symmetric]) 1376 apply (clarsimp simp: free_index_of_def free_range_of_untyped_def) 1377 apply (simp del: hoare_TrueI) 1378 apply wp 1379 apply (wp add: hoare_vcg_const_imp_lift get_cap_wp delete_objects_invs2 1380 | simp 1381 | strengthen invs_valid_objs invs_valid_idle 1382 | rule impI)+ 1383 apply (clarsimp simp: cte_wp_at_caps_of_state 1384 descendants_range_def2) 1385 apply (strengthen empty_descendants_range_in 1386 subst[where P="\<lambda>x. descendants_of x c = {}" for c, mk_strg I _ E] 1387 | simp add: prod_eq_iff)+ 1388 apply (cases cref) 1389 apply (clarsimp simp: is_cap_simps bits_of_def free_index_of_def 1390 ) 1391 apply (frule cte_wp_at_valid_objs_valid_cap[OF caps_of_state_cteD], 1392 clarsimp+) 1393 apply (clarsimp simp: valid_cap_simps) 1394 apply (frule if_unsafe_then_capD[OF caps_of_state_cteD], clarsimp+) 1395 apply (frule(1) ex_cte_cap_protects[OF _ caps_of_state_cteD _ _ order_refl], 1396 simp add: empty_descendants_range_in, clarsimp+) 1397 apply (auto simp: not_idle_thread_def untyped_min_bits_def 1398 dest!: valid_idle_has_null_cap[rotated -1], 1399 auto intro: caps_of_state_valid)[1] 1400 done 1401 1402lemma range_le_free_range_of_untyped: 1403 "range_cover (ptr::word32) sz sbit n 1404 \<Longrightarrow> n \<noteq> 0 1405 \<Longrightarrow> idx \<le> unat (ptr && mask sz) 1406 \<Longrightarrow> {ptr..ptr + of_nat n * 2 ^ sbit - 1} 1407 \<subseteq> free_range_of_untyped idx sz (ptr && ~~ mask sz)" 1408 apply (rule order_trans, erule(1) range_cover_subset') 1409 apply (clarsimp simp: free_range_of_untyped_def 1410 split del: if_split del: subsetI) 1411 apply (subst if_P) 1412 prefer 2 1413 apply (rule range_subsetI, simp_all) 1414 apply (subst word_plus_and_or_coroll2[symmetric,where w = "mask sz" and t = ptr], 1415 subst add.commute, 1416 rule word_add_le_mono2) 1417 apply (simp add: word_of_nat_le) 1418 apply (simp only: no_olen_add_nat[symmetric] word_plus_and_or_coroll2 word_and_le2) 1419 apply (erule order_trans) 1420 apply (rule nat_le_Suc_less_imp) 1421 apply (rule word_unat_mask_lt) 1422 apply (simp add: range_cover_def word_size) 1423 done 1424 1425lemma invoke_untyped_corres: 1426 "dcorres (dc \<oplus> dc) (\<lambda>_. True) 1427 (invs and ct_active and valid_untyped_inv untyped_invocation and valid_etcbs) 1428 (Untyped_D.invoke_untyped (translate_untyped_invocation untyped_invocation)) 1429 (Retype_A.invoke_untyped untyped_invocation)" 1430 apply (rule dcorres_expand_pfx) 1431 apply (clarsimp simp only: valid_untyped_inv_wcap) 1432 apply (cases untyped_invocation) 1433 apply (rename_tac s s' sz idx creforef reset ptr ptr' tp us slots dev) 1434 proof - 1435 fix s cref reset ptr ptr' tp us slots sz idx dev 1436 assume vui1: "valid_untyped_inv_wcap untyped_invocation 1437 (Some (case untyped_invocation of 1438 Invocations_A.untyped_invocation.Retype slot reset ptr_base ptr ty us slots dev \<Rightarrow> 1439 cap.UntypedCap dev (ptr && ~~ mask sz) sz idx)) s" 1440 and ui: "untyped_invocation = 1441 Invocations_A.Retype cref reset ptr' ptr tp us slots dev" 1442 and etc: "valid_etcbs s" "invs s" "ct_active s" 1443 1444 note vui = vui1[simplified ui Invocations_A.untyped_invocation.simps] 1445 1446 have ptrs: "ptr' = ptr && ~~ mask sz" 1447 using vui 1448 by (auto simp: ui cte_wp_at_caps_of_state word_bw_assocs) 1449 1450 have cover: "range_cover ptr sz (obj_bits_api tp us) (length slots)" 1451 and vslot: "slots \<noteq> []" "distinct slots" 1452 and misc: "tp = Structures_A.apiobject_type.CapTableObject \<longrightarrow> 0 < us" 1453 "tp = Structures_A.apiobject_type.Untyped \<longrightarrow> untyped_min_bits \<le> us" 1454 using vui 1455 by (auto simp: ui cte_wp_at_caps_of_state) 1456 1457 have vcap: "s \<turnstile> cap.UntypedCap dev (ptr && ~~ mask sz) sz idx" 1458 using vui etc 1459 by (auto simp: ui cte_wp_at_caps_of_state 1460 dest!: caps_of_state_valid[rotated]) 1461 1462 note [simp del] = usable_untyped_range.simps atLeastAtMost_iff 1463 atLeastatMost_subset_iff split_paired_Ex 1464 1465 show "dcorres (dc \<oplus> dc) ((=) (transform s)) ((=) s) 1466 (Untyped_D.invoke_untyped 1467 (translate_untyped_invocation untyped_invocation)) 1468 (Retype_A.invoke_untyped untyped_invocation)" 1469 supply option.case_cong[cong] if_cong[cong] 1470 apply (clarsimp simp: Untyped_D.invoke_untyped_def mapM_x_def translate_untyped_invocation_def 1471 ui ptrs invoke_untyped_def unlessE_whenE) 1472 apply (rule corres_guard_imp) 1473 apply (rule corres_split_norE) 1474 prefer 2 1475 apply (rule corres_whenE, simp) 1476 apply (rule reset_untyped_cap_corres[where idx=idx]) 1477 apply simp 1478 apply simp 1479 apply (rule corres_split[OF _ get_cap_corres]) 1480 apply simp 1481 apply (rule generate_object_ids_exec[where ptr = ptr and us = us and sz = sz]) 1482 apply simp 1483 apply (rule corres_split[OF _ update_available_range_dcorres]) 1484 apply simp 1485 apply (rule corres_split[OF _ retype_region_dcorres[where sz = sz]]) 1486 apply (rule corres_split_noop_rhs[OF _ init_arch_objects_corres_noop[where sz =sz]]) 1487 apply (simp add: liftM_def[symmetric] mapM_x_def[symmetric] 1488 zip_map1 zip_map2 o_def split_beta dc_def[symmetric]) 1489 apply (rule_tac F = " (untyped_is_device (transform_cap cap)) = dev" in corres_gen_asm2) 1490 apply clarify 1491 apply (rule create_caps_loop_dcorres) 1492 apply clarsimp 1493 apply (erule retype_addrs_aligned[OF _ range_cover.aligned _ le_refl]) 1494 apply (rule cover) 1495 apply (rule range_cover_sz'[where 'a=32, folded word_bits_def, OF cover]) 1496 apply (rule cover) 1497 apply (simp add: vslot) 1498 apply ((wp | simp add: mdb_cte_at_def | rule hoare_vcg_conj_lift, wps)+)[2] 1499 supply send_signal_interrupt_states[wp_unsafe del] validNF_prop[wp_unsafe del] 1500 apply (wp retype_region_aligned_for_init[where sz = sz] 1501 retype_region_obj_at[THEN hoare_vcg_const_imp_lift] 1502 retype_region_caps_of[where sza = "\<lambda>_. sz"] 1503 | simp add: misc)+ 1504 apply (rule_tac Q="\<lambda>rv s. cte_wp_at ((\<noteq>) cap.NullCap) cref s 1505 \<and> post_retype_invs tp rv s 1506 \<and> idle_thread s \<notin> fst ` set slots 1507 \<and> untyped_is_device (transform_cap cap) = dev 1508 \<and> (\<forall>slot\<in>set slots. cte_wp_at ((=) cap.NullCap) slot s) 1509 \<and> valid_etcbs s" 1510 in hoare_post_imp) 1511 apply (simp add:post_retype_invs_def split:if_split_asm) 1512 apply ((clarsimp dest!: set_zip_leftD 1513 simp: vslot image_def invs_def valid_state_def valid_mdb_def 1514 cte_wp_at_caps_of_state 1515 | intro conjI | drule (1) bspec | drule(1) mdb_cte_atD[rotated])+)[2] 1516 apply (wp retype_region_cte_at_other'[where sz= sz] 1517 retype_region_post_retype_invs[where sz = sz] 1518 hoare_vcg_const_Ball_lift retype_region_aligned_for_init)+ 1519 apply (clarsimp simp:conj_comms misc cover) 1520 apply (rule_tac Q="\<lambda>r s. 1521 cte_wp_at (\<lambda>cp. \<exists>idx. cp = (cap.UntypedCap dev ptr' sz idx)) cref s \<and> 1522 invs s \<and> pspace_no_overlap_range_cover ptr sz s \<and> caps_no_overlap ptr sz s \<and> 1523 region_in_kernel_window {ptr..(ptr && ~~ mask sz) + 2 ^ sz - 1} s \<and> 1524 caps_overlap_reserved {ptr..ptr + of_nat (length slots) * 2 ^ obj_bits_api tp us - 1} s \<and> 1525 idle_thread s \<notin> fst ` set slots 1526 \<and> untyped_is_device (transform_cap cap) = dev 1527 \<and> (\<forall>x\<in>set slots. cte_wp_at ((=) cap.NullCap) x s) \<and> valid_etcbs s" 1528 in hoare_strengthen_post[rotated]) 1529 apply (clarsimp simp: invs_mdb invs_valid_pspace cte_wp_at_caps_of_state misc split_paired_Ex) 1530 apply (rule conjI,clarsimp) 1531 apply (erule ranE) 1532 apply (clarsimp simp:null_filter_def split:if_splits) 1533 apply (frule_tac cap = capa in caps_of_state_ko[OF caps_of_state_valid]) 1534 apply assumption 1535 apply (elim disjE) 1536 apply (clarsimp simp:cap_range_def is_cap_simps)+ 1537 apply (rule disjointI) 1538 apply clarsimp 1539 apply (drule bspec,fastforce,clarsimp) 1540 apply (drule(1) pspace_no_overlap_obj_range) 1541 apply (drule p_in_obj_range) 1542 apply clarsimp+ 1543 apply (auto simp: field_simps)[1] 1544 apply (cases cref, simp, intro exI, rule conjI, assumption, 1545 simp add: atLeastatMost_subset_iff word_and_le2 ptrs field_simps) 1546 apply (rule_tac P="bits_of cap = sz" in hoare_gen_asm) 1547 apply (simp add:bits_of_def) 1548 apply (strengthen caps_region_kernel_window_imp[where p=cref] invs_cap_refs_in_kernel_window)+ 1549 apply (wp set_cap_no_overlap hoare_vcg_ball_lift 1550 set_free_index_invs[where 'a=det_ext and 1551 cap = "cap.UntypedCap dev (ptr && ~~ mask sz) sz 1552 (if reset then 0 else idx)", 1553 simplified] 1554 set_cap_cte_wp_at set_cap_descendants_range_in set_cap_caps_no_overlap 1555 set_untyped_cap_caps_overlap_reserved set_cap_cte_cap_wp_to hoare_vcg_ex_lift) 1556 apply simp 1557 apply wp 1558 apply (simp split del: if_split) 1559 apply (wp get_cap_wp)+ 1560 apply (wp (once) hoare_drop_imps) 1561 apply wp 1562 apply ((rule validE_validE_R)?, 1563 rule_tac E="\<top>\<top>" and 1564 Q="\<lambda>_. valid_etcbs and invs and valid_untyped_inv_wcap untyped_invocation 1565 (Some (cap.UntypedCap dev ptr' sz (if reset then 0 else idx))) and ct_active 1566 and (\<lambda>s. reset \<longrightarrow> pspace_no_overlap {ptr' .. ptr' + 2 ^ sz - 1} s)" 1567 in hoare_post_impErr) 1568 apply (wp hoare_whenE_wp) 1569 apply (rule validE_validE_R, rule hoare_post_impErr, rule reset_untyped_cap_invs_etc) 1570 apply (clarsimp simp only: if_True simp_thms ptrs, intro conjI, assumption+) 1571 apply simp 1572 apply (clarsimp simp only: ui ptrs) 1573 apply (frule(2) invoke_untyped_proofs.intro) 1574 apply (clarsimp simp: ui cte_wp_at_caps_of_state bits_of_def empty_descendants_range_in exI 1575 free_index_of_def untyped_range_def if_split[where P="\<lambda>x. x \<le> unat v" for v] 1576 split del: if_split) 1577 apply (frule(1) valid_global_refsD2[OF _ invs_valid_global_refs]) 1578 apply (strengthen refl subseteq_set_minus free_range_of_untyped_subseteq' 1579 range_le_free_range_of_untyped[mk_strg I E] 1580 caps_region_kernel_window_imp[where p=cref])+ 1581 apply (simp only: word_size word_bits_def[symmetric]) 1582 apply (clarsimp simp: conj_comms invoke_untyped_proofs.simps range_le_free_range_of_untyped 1583 if_split[where P="\<lambda>x. x \<le> unat v" for v] 1584 split del: if_split) 1585 apply (simp add: arg_cong[OF mask_out_sub_mask, where f="\<lambda>y. x - y" for x] 1586 field_simps invoke_untyped_proofs.idx_le_new_offs 1587 invoke_untyped_proofs.idx_compare' 1588 untyped_range_def invs_valid_idle invs_valid_pspace 1589 is_aligned_neg_mask invoke_untyped_proofs.szw 1590 free_range_of_untyped_pick_retype_addrs vslot 1591 split del: if_split) 1592 apply (clarsimp simp: detype_clear_um_independent conj_comms not_idle_thread_def 1593 misc invs_valid_idle invs_valid_objs word_bits_def word_and_le2 1594 atLeastatMost_subset_iff[where b=x and d=x for x] 1595 split del: if_split) 1596 apply (clarsimp simp: range_cover.aligned bits_of_def field_simps split del: if_split) 1597 apply (intro conjI) 1598 apply (cases cref, fastforce dest: valid_idle_has_null_cap[rotated -1]) 1599 apply (fastforce dest: ex_cte_cap_to_not_idle) 1600 apply (cases reset) 1601 apply (simp, erule pspace_no_overlap_subset) 1602 apply (simp add: atLeastatMost_subset_iff word_and_le2) 1603 apply (clarsimp simp: field_simps dest!: invoke_untyped_proofs.ps_no_overlap) 1604 apply (auto dest: invoke_untyped_proofs.idx_le_new_offs)[1] 1605 apply (strengthen invoke_untyped_proofs.subset_stuff[THEN order_trans, mk_strg I E]) 1606 apply (simp add: atLeastatMost_subset_iff word_and_le2) 1607 apply (drule invoke_untyped_proofs.usable_range_disjoint) 1608 apply (clarsimp simp: field_simps mask_out_sub_mask shiftl_t2n) 1609 apply simp 1610 apply simp 1611 apply (cut_tac vui1) 1612 apply (clarsimp simp add: etc ptrs) 1613 apply (clarsimp simp: ui cte_wp_at_caps_of_state valid_cap_simps free_index_of_def) 1614 apply auto 1615 done 1616qed 1617 1618lemma transform_translate_type: 1619 "transform_type n = Some tp 1620 \<Longrightarrow> \<exists>v. data_to_obj_type n = returnOk v \<and> tp = translate_object_type v" 1621 apply (simp add: transform_type_def 1622 split: if_split_asm) 1623 apply (simp_all add: data_to_obj_type_def arch_data_to_obj_type_def) 1624 apply (auto simp add: translate_object_type_def) 1625 done 1626 1627lemma corres_whenE_throwError_split_rhs: 1628 "corres_underlying sr nf nf' r P Q a (whenE G (throwError e) >>=E (\<lambda>_. b)) 1629 = ((G \<longrightarrow> corres_underlying sr nf nf' r P Q a (throwError e)) 1630 \<and> (\<not> G \<longrightarrow> corres_underlying sr nf nf' r P Q a b))" 1631 by (simp add: whenE_bindE_throwError_to_if) 1632 1633lemma nat_bl_to_bin_nat_to_cref: 1634 assumes asms: "x < 2 ^ bits" "bits < word_bits" 1635 shows "nat (bl_to_bin (nat_to_cref bits x)) = x" 1636proof - 1637 note of_bl = of_bl_nat_to_cref[OF asms] 1638 have lt_bl: "bl_to_bin (nat_to_cref bits x) < 2 ^ 32" 1639 apply (rule order_less_le_trans, rule bl_to_bin_lt2p) 1640 apply (rule power_increasing) 1641 apply (simp add: nat_to_cref_def) 1642 apply simp 1643 done 1644 have lt_x: "x < 2 ^ 32" 1645 apply (rule order_less_le_trans, rule asms) 1646 apply (rule power_increasing, simp_all) 1647 apply (insert asms word_bits_conv, simp) 1648 done 1649 show ?thesis using of_bl lt_bl lt_x 1650 apply (simp add: of_bl_def word_of_nat) 1651 apply (drule word_uint.Abs_eqD) 1652 apply (simp add: uints_num bl_to_bin_ge0) 1653 apply (simp add: uints_num) 1654 apply simp 1655 done 1656qed 1657 1658context 1659notes if_cong[cong] 1660begin 1661crunch inv[wp]: "CSpace_D.ensure_empty" "P" 1662end 1663 1664lemma mapME_x_inv_wp2: 1665 "(\<And>x. \<lbrace>P and E\<rbrace> f x \<lbrace>\<lambda>rv. P and E\<rbrace>,\<lbrace>\<lambda>rv. E\<rbrace>) 1666 \<Longrightarrow> \<lbrace>P and E\<rbrace> mapME_x f xs \<lbrace>\<lambda>rv. P\<rbrace>,\<lbrace>\<lambda>rv. E\<rbrace>" 1667 apply (rule hoare_post_impErr) 1668 apply (rule mapME_x_inv_wp[where E="\<lambda>_. E"]) 1669 apply (rule hoare_post_impErr, assumption) 1670 apply simp_all 1671 done 1672 1673lemma gets_get: 1674 "get = gets id " 1675 by (simp add:gets_def) 1676 1677lemma transform_cdt_dom_standard: 1678 "transform_cdt s' slot' = Some (transform_cslot_ptr b) 1679 \<Longrightarrow> \<exists>slot. slot' = transform_cslot_ptr slot" 1680 apply (case_tac b) 1681 apply (fastforce simp:transform_cdt_def map_lift_over_def split:if_split_asm) 1682 done 1683 1684lemma descendants_of_empty_lift : 1685 "\<lbrakk>cte_at slot' s; valid_mdb s\<rbrakk> \<Longrightarrow> 1686 (CSpaceAcc_A.descendants_of slot' (cdt s) = {}) 1687 = (\<not> (\<exists>slot. transform_cdt s slot = Some (transform_cslot_ptr slot')))" 1688 apply (rule iffI) 1689 apply clarsimp 1690 apply (frule transform_cdt_dom_standard) 1691 apply (clarsimp simp:descendants_of_def) 1692 apply (thin_tac "(a,b) = P" for P) 1693 apply (drule(1) transform_cdt_some_rev) 1694 apply (clarsimp simp:valid_mdb_def) 1695 apply clarsimp 1696 apply (drule_tac x = a in spec,drule_tac x = b in spec) 1697 apply (subgoal_tac "cdt s \<Turnstile> slot' \<rightarrow> (a, b)") 1698 apply simp 1699 apply (rule r_into_trancl') 1700 apply (simp add:cdt_parent_rel_def is_cdt_parent_def) 1701 apply (rule ccontr) 1702 apply (clarsimp simp:descendants_of_def) 1703 apply (drule tranclD) 1704 apply clarsimp 1705 apply (drule_tac x = aa in spec,drule_tac x = "nat (bl_to_bin ba)" in spec) 1706 apply (frule descendants_of_cte_at[rotated]) 1707 apply (simp add:descendants_of_def) 1708 apply (rule r_into_trancl') 1709 apply simp 1710 apply (drule_tac slot = "(aa,ba)" in mdb_cte_transform_cdt_lift) 1711 apply (simp add:valid_mdb_def) 1712 apply (clarsimp simp:cdt_parent_rel_def is_cdt_parent_def transform_cslot_ptr_def) 1713 done 1714 1715lemma alignUp_gt_0: 1716 "\<lbrakk>is_aligned (x :: 'a :: len word) n; n < len_of TYPE('a); x \<noteq> 0 ; a \<le> x\<rbrakk> \<Longrightarrow> (0 < Word_Lib.alignUp a n) = (a \<noteq> 0)" 1717 apply (rule iffI) 1718 apply (rule ccontr) 1719 apply (clarsimp simp:not_less alignUp_def2 mask_def) 1720 apply (frule(1) alignUp_is_aligned_nz[where a = a]) 1721 apply (simp add:unat_1_0) 1722 apply simp 1723 apply (simp add:word_neq_0_conv) 1724 done 1725 1726lemma of_nat_0: 1727 "free_index < 2^word_bits - 1 1728 \<Longrightarrow> ((of_nat free_index::word32) = 0) = (free_index = 0)" 1729 apply (subst word_unat.inverse_norm) 1730 apply (subst word_bits_def[symmetric]) 1731 apply simp 1732 done 1733 1734lemma range_cover_sz_less': 1735 "range_cover (ptr :: word32) sz us n \<Longrightarrow> (2::nat) ^ sz < 2 ^ word_bits - 1" 1736 apply (simp add:range_cover_def) 1737 apply (rule le_less_trans[where y = "2^31"]) 1738 apply (rule power_increasing) 1739 apply (clarsimp simp:word_bits_def) 1740 apply simp 1741 apply (simp add:word_bits_def) 1742 done 1743 1744lemma decode_untyped_corres: 1745 "\<lbrakk> Some (UntypedIntent ui) = transform_intent (invocation_type label') args'; 1746 cap = transform_cap cap'; 1747 cap' = cap.UntypedCap dev ptr sz idx; 1748 slot = transform_cslot_ptr slot'; 1749 excaps = transform_cap_list excaps' \<rbrakk> \<Longrightarrow> 1750 dcorres (dc \<oplus> (\<lambda>x y. x = translate_untyped_invocation y)) 1751 \<top> (cte_wp_at ((=) cap') slot' and invs 1752 and (\<lambda>s. \<forall>x \<in> set (map fst excaps'). s \<turnstile> x) 1753 and (\<lambda>s. \<forall>x \<in> set excaps'. cte_wp_at ((=) (fst x)) (snd x) s) and valid_etcbs) 1754 (Untyped_D.decode_untyped_invocation cap slot excaps ui) 1755 (Decode_A.decode_untyped_invocation label' args' slot' cap' (map fst excaps'))" 1756 supply if_cong[cong] 1757 apply (simp add: transform_intent_def map_option_Some_eq2 1758 transform_intent_untyped_retype_def 1759 split: invocation_label.split_asm gen_invocation_labels.split_asm 1760 arch_invocation_label.split_asm list.split_asm option.split_asm) 1761 apply (cases ui) 1762 apply (drule transform_translate_type[where 'a=det_ext]) 1763 apply (clarsimp simp: Untyped_D.decode_untyped_invocation_def 1764 Decode_A.decode_untyped_invocation_def 1765 unlessE_whenE 1766 split del: if_split 1767 split: invocation_label.split_asm) 1768 apply (rename_tac a list w1 w2 w3 w4 w5 apiobject_type) 1769 apply (cases excaps') 1770 apply (simp add: get_index_def transform_cap_list_def 1771 alternative_refl gen_invocation_type_eq) 1772 apply (simp add: get_index_def transform_cap_list_def throw_on_none_def 1773 split_beta 1774 split del: if_split) 1775 apply (clarsimp simp: corres_whenE_throwError_split_rhs 1776 corres_alternate2 1777 split del: if_split) 1778 apply (simp add: bindE_assoc[symmetric] split del: if_split) 1779 apply (rule_tac r'="\<lambda>rv rv'. rv = transform_cap rv'" 1780 in corres_alternative_throw_splitE) 1781 apply (rule corres_guard_imp, rule corres_alternate1) 1782 apply (rule corres_if) 1783 apply (simp add: unat_eq_0) 1784 apply (rule corres_trivial, simp add: returnOk_def) 1785 apply (rule corres_splitEE[OF _ lookup_slot_for_cnode_op_corres]) 1786 apply clarsimp 1787 apply (rule get_cap_corres) 1788 apply simp+ 1789 apply (wp lsfco_not_idle | simp)+ 1790 apply (clarsimp simp: cte_wp_at_caps_of_state) 1791 apply auto[1] 1792 apply (rename_tac cnode_cap cnode_cap') 1793 apply (simp add: bindE_assoc split del: if_split) 1794 apply (simp add: if_to_top_of_bindE is_cnode_cap_transform_cap[symmetric] 1795 split del: if_split) 1796 apply (rule corres_if_rhs[rotated]) 1797 apply (rule corres_trivial, simp add: alternative_refl) 1798 apply (simp add: corres_whenE_throwError_split_rhs 1799 corres_alternate2) 1800 apply (intro impI) 1801 apply (rule_tac r'=dc in corres_alternative_throw_splitE[rotated]) 1802 apply (simp add:liftE_bindE) 1803 apply (rule corres_symb_exec_r) 1804 apply (clarsimp simp: corres_whenE_throwError_split_rhs corres_alternate2 1805 split del: if_split) 1806 apply (rule corres_alternate1) 1807 apply (simp add:gets_get split del: if_split) 1808 apply (rule corres_underlying_gets_pre_lhs) 1809 apply (rule_tac P' = "\<lambda>s. valid_mdb s \<and> cte_at slot' s \<and> is_cnode_cap cnode_cap' \<and> 1810 cap_aligned cnode_cap' \<and> invs s \<and> not_idle_thread (obj_ref_of cnode_cap') s \<and> 1811 is_aligned ptr sz \<and> idx \<le> 2 ^ sz \<and> sz < word_bits \<and> 1812 reset = (descendants_of slot' (cdt s) ={} ) \<and> valid_etcbs s" 1813 and P = "\<lambda>s. s = x" in corres_returnOk) 1814 apply (simp add: translate_untyped_invocation_def transform_def get_free_ref_def) 1815 apply (simp add:has_children_def KHeap_D.is_cdt_parent_def 1816 descendants_of_empty_lift word_neq_0_conv) 1817 apply (clarsimp simp: not_less is_cap_simps bits_of_def) 1818 apply (clarsimp simp: is_cap_simps transform_cslot_ptr_def bits_of_def 1819 cap_aligned_def nat_bl_to_bin_nat_to_cref) 1820 apply (wp check_children_wp) 1821 apply simp 1822 apply (simp add:const_on_failure_def) 1823 apply clarsimp 1824 apply wp+ 1825 apply (clarsimp simp:conj_comms) 1826 apply (wp mapME_x_inv_wp[OF hoare_pre(2)] | simp split del: if_split)+ 1827 apply (simp split del: if_split add: if_apply_def2) 1828 apply (rule corres_alternate1) 1829 apply (rule corres_guard_imp) 1830 apply (rule_tac F="cap_aligned cnode_cap' \<and> is_cnode_cap cnode_cap'" in corres_gen_asm2) 1831 apply (subgoal_tac "map (Pair (cap_object (transform_cap cnode_cap'))) 1832 [unat w4 ..< unat w4 + unat w5] 1833 = map (\<lambda>x. transform_cslot_ptr (obj_ref_of (cnode_cap'), 1834 (nat_to_cref (bits_of cnode_cap') x))) 1835 [unat w4 ..< unat w4 + unat w5]") 1836 apply (simp del: map_eq_conv) 1837 apply (simp add: mapME_x_map_simp) 1838 apply (rule mapME_x_corres_inv) 1839 apply (simp add: dc_def[symmetric]) 1840 apply (rule dcorres_ensure_empty) 1841 apply (wp mapME_x_inv_wp[OF hoare_pre(2)] | simp)+ 1842 apply (clarsimp simp: is_cap_simps transform_cslot_ptr_def bits_of_def cap_aligned_def 1843 nat_bl_to_bin_nat_to_cref) 1844 apply simp 1845 apply clarsimp 1846 apply (rule hoare_pre) 1847 apply (wp hoare_drop_imp | simp)+ 1848 apply fastforce 1849 apply (clarsimp simp: conj_comms is_cnode_cap_transform_cap split del: if_split) 1850 apply (rule validE_R_validE) 1851 apply (rule_tac Q' = "\<lambda>a s. invs s \<and> valid_etcbs s \<and> valid_cap a s \<and> cte_wp_at ((=) (cap.UntypedCap dev ptr sz idx)) slot' s 1852 \<and> (Structures_A.is_cnode_cap a \<longrightarrow> not_idle_thread (obj_ref_of a) s)" 1853 in hoare_post_imp_R) 1854 apply (rule hoare_pre) 1855 apply (wp get_cap_wp) 1856 apply (rule_tac Q' = "\<lambda>a s. invs s \<and> valid_etcbs s \<and> cte_wp_at ((=) (cap.UntypedCap dev ptr sz idx)) slot' s" 1857 in hoare_post_imp_R) 1858 apply wp 1859 apply (clarsimp simp: cte_wp_at_caps_of_state) 1860 apply (frule_tac p = "(x,y)" for x y in caps_of_state_valid[rotated]) 1861 apply simp 1862 apply (clarsimp simp:valid_cap_def obj_at_def valid_idle_def pred_tcb_at_def 1863 is_cap_simps not_idle_thread_def is_cap_table_def dest!:invs_valid_idle) 1864 apply (clarsimp simp:valid_cap_def obj_at_def valid_idle_def pred_tcb_at_def 1865 is_cap_simps not_idle_thread_def is_cap_table_def dest!:invs_valid_idle) 1866 apply (clarsimp simp:invs_mdb cte_wp_at_caps_of_state valid_cap_aligned) 1867 apply (frule(1) caps_of_state_valid) 1868 apply (rule ccontr) 1869 apply (clarsimp simp:valid_cap_simps cap_aligned_def) 1870 apply (rule hoare_pre,wp,simp) 1871 apply (wp hoare_drop_imp mapME_x_inv_wp2 | simp add:if_apply_def2 split del:if_split)+ 1872 done 1873 1874lemma decode_untyped_label_not_match: 1875 "\<lbrakk>Some intent = transform_intent (invocation_type label) args; \<forall>ui. intent \<noteq> UntypedIntent ui\<rbrakk> 1876 \<Longrightarrow> \<lbrace>(=) s\<rbrace> Decode_A.decode_untyped_invocation label args ref (cap.UntypedCap dev a b idx) e 1877 \<lbrace>\<lambda>r. \<bottom>\<rbrace>, \<lbrace>\<lambda>e. (=) s\<rbrace>" 1878 apply (case_tac "invocation_type label = GenInvocationLabel UntypedRetype") 1879 apply (clarsimp simp:Decode_A.decode_untyped_invocation_def transform_intent_def)+ 1880 apply (clarsimp simp:transform_intent_untyped_retype_def split:option.splits list.splits) 1881 apply (simp add:Decode_A.decode_untyped_invocation_def unlessE_def gen_invocation_type_eq) 1882 apply wp 1883 done 1884 1885end 1886 1887end 1888