1(* 2 * Copyright 2014, General Dynamics C4 Systems 3 * 4 * This software may be distributed and modified according to the terms of 5 * the GNU General Public License version 2. Note that NO WARRANTY is provided. 6 * See "LICENSE_GPLv2.txt" for details. 7 * 8 * @TAG(GD_GPL) 9 *) 10 11theory ArchIpc_AI 12imports "../Ipc_AI" 13begin 14 15context Arch begin global_naming ARM 16 17named_theorems Ipc_AI_assms 18 19crunch pspace_respects_device_region[wp]: set_extra_badge "pspace_respects_device_region" 20 21crunch cap_refs_respects_device_region[wp]: set_extra_badge "cap_refs_respects_device_region" 22 (wp: crunch_wps cap_refs_respects_device_region_dmo) 23 24lemma update_cap_data_closedform: 25 "update_cap_data pres w cap = 26 (case cap of 27 cap.EndpointCap r badge rights \<Rightarrow> 28 if badge = 0 \<and> \<not> pres then (cap.EndpointCap r (w && mask 28) rights) else cap.NullCap 29 | cap.NotificationCap r badge rights \<Rightarrow> 30 if badge = 0 \<and> \<not> pres then (cap.NotificationCap r (w && mask 28) rights) else cap.NullCap 31 | cap.CNodeCap r bits guard \<Rightarrow> 32 if word_bits < unat ((w >> 3) && mask 5) + bits 33 then cap.NullCap 34 else cap.CNodeCap r bits ((\<lambda>g''. drop (size g'' - unat ((w >> 3) && mask 5)) (to_bl g'')) ((w >> 8) && mask 18)) 35 | cap.ThreadCap r \<Rightarrow> cap.ThreadCap r 36 | cap.DomainCap \<Rightarrow> cap.DomainCap 37 | cap.UntypedCap d p n idx \<Rightarrow> cap.UntypedCap d p n idx 38 | cap.NullCap \<Rightarrow> cap.NullCap 39 | cap.ReplyCap t m \<Rightarrow> cap.ReplyCap t m 40 | cap.IRQControlCap \<Rightarrow> cap.IRQControlCap 41 | cap.IRQHandlerCap irq \<Rightarrow> cap.IRQHandlerCap irq 42 | cap.Zombie r b n \<Rightarrow> cap.Zombie r b n 43 | cap.ArchObjectCap cap \<Rightarrow> cap.ArchObjectCap cap)" 44 apply (cases cap, 45 simp_all only: cap.simps update_cap_data_def is_ep_cap.simps if_False if_True 46 is_ntfn_cap.simps is_cnode_cap.simps is_arch_cap_def word_size 47 cap_ep_badge.simps badge_update_def o_def cap_rights_update_def 48 simp_thms cap_rights.simps Let_def split_def 49 the_cnode_cap_def fst_conv snd_conv fun_app_def the_arch_cap_def 50 arch_update_cap_data_def 51 cong: if_cong) 52 apply (auto simp: word_bits_def) 53 done 54 55lemma cap_asid_PageCap_None [simp]: 56 "cap_asid (ArchObjectCap (PageCap dev r R pgsz None)) = None" 57 by (simp add: cap_asid_def) 58 59lemma arch_derive_cap_is_derived: 60 "\<lbrace>\<lambda>s. cte_wp_at (\<lambda>cap . cap_master_cap cap = 61 cap_master_cap (ArchObjectCap c') \<and> 62 cap_aligned cap \<and> 63 cap_asid cap = cap_asid (ArchObjectCap c') \<and> 64 vs_cap_ref cap = vs_cap_ref (ArchObjectCap c')) p s\<rbrace> 65 arch_derive_cap c' 66 \<lbrace>\<lambda>rv s. cte_wp_at (is_derived (cdt s) p rv) p s\<rbrace>, -" 67 unfolding arch_derive_cap_def 68 apply(cases c', simp_all add: is_cap_simps cap_master_cap_def) 69 apply((wp throwError_validE_R 70 | clarsimp simp: is_derived_def 71 is_cap_simps cap_master_cap_def 72 cap_aligned_def is_aligned_no_overflow is_pt_cap_def 73 cap_asid_def vs_cap_ref_def 74 | erule cte_wp_at_weakenE 75 | simp split: arch_cap.split_asm cap.split_asm option.splits 76 | rule conjI)+) 77 done 78 79lemma derive_cap_is_derived [Ipc_AI_assms]: 80 "\<lbrace>\<lambda>s. c'\<noteq> cap.NullCap \<longrightarrow> cte_wp_at (\<lambda>cap. cap_master_cap cap = cap_master_cap c' 81 \<and> (cap_badge cap, cap_badge c') \<in> capBadge_ordering False 82 \<and> cap_asid cap = cap_asid c' 83 \<and> vs_cap_ref cap = vs_cap_ref c') slot s 84 \<and> valid_objs s\<rbrace> 85 derive_cap slot c' 86 \<lbrace>\<lambda>rv s. rv \<noteq> cap.NullCap \<longrightarrow> 87 cte_wp_at (is_derived (cdt s) slot rv) slot s\<rbrace>, -" 88 unfolding derive_cap_def 89 apply (cases c', simp_all add: is_cap_simps) 90 apply ((wp ensure_no_children_wp 91 | clarsimp simp: is_derived_def is_cap_simps 92 cap_master_cap_def bits_of_def 93 same_object_as_def is_pt_cap_def 94 cap_asid_def 95 | fold validE_R_def 96 | erule cte_wp_at_weakenE 97 | simp split: cap.split_asm)+)[11] 98 apply(wp hoare_drop_imps arch_derive_cap_is_derived) 99 apply(clarify, drule cte_wp_at_eqD, clarify) 100 apply(frule(1) cte_wp_at_valid_objs_valid_cap) 101 apply(erule cte_wp_at_weakenE) 102 apply(clarsimp simp: valid_cap_def) 103 done 104 105lemma is_derived_cap_rights [simp, Ipc_AI_assms]: 106 "is_derived m p (cap_rights_update R c) = is_derived m p c" 107 apply (rule ext) 108 apply (simp add: cap_rights_update_def is_derived_def is_cap_simps) 109 apply (case_tac x, simp_all) 110 apply (simp add: cap_master_cap_def bits_of_def is_cap_simps 111 vs_cap_ref_def 112 split: cap.split)+ 113 apply (simp add: is_cap_simps is_page_cap_def 114 cong: arch_cap.case_cong) 115 apply (simp split: arch_cap.split cap.split 116 add: is_cap_simps acap_rights_update_def is_pt_cap_def) 117 done 118 119lemma data_to_message_info_valid [Ipc_AI_assms]: 120 "valid_message_info (data_to_message_info w)" 121 by (simp add: valid_message_info_def data_to_message_info_def word_and_le1 msg_max_length_def 122 msg_max_extra_caps_def Let_def not_less mask_def) 123 124lemma get_extra_cptrs_length[wp, Ipc_AI_assms]: 125 "\<lbrace>\<lambda>s . valid_message_info mi\<rbrace> 126 get_extra_cptrs buf mi 127 \<lbrace>\<lambda>rv s. length rv \<le> msg_max_extra_caps\<rbrace>" 128 apply (cases buf) 129 apply (simp, wp, simp) 130 apply (simp add: msg_max_length_def) 131 apply (subst hoare_liftM_subst, simp add: o_def) 132 apply (rule hoare_pre) 133 apply (rule mapM_length, simp) 134 apply (clarsimp simp: valid_message_info_def msg_max_extra_caps_def 135 word_le_nat_alt 136 intro: length_upt) 137 done 138 139lemma cap_asid_rights_update [simp, Ipc_AI_assms]: 140 "cap_asid (cap_rights_update R c) = cap_asid c" 141 apply (simp add: cap_rights_update_def acap_rights_update_def split: cap.splits arch_cap.splits) 142 apply (clarsimp simp: cap_asid_def) 143 done 144 145lemma cap_rights_update_vs_cap_ref[simp, Ipc_AI_assms]: 146 "vs_cap_ref (cap_rights_update rs cap) = vs_cap_ref cap" 147 by (simp add: vs_cap_ref_def cap_rights_update_def 148 acap_rights_update_def 149 split: cap.split arch_cap.split) 150 151lemma is_derived_cap_rights2[simp, Ipc_AI_assms]: 152 "is_derived m p c (cap_rights_update R c') = is_derived m p c c'" 153 apply (case_tac c') 154 apply (simp_all add: cap_rights_update_def) 155 apply (clarsimp simp: is_derived_def is_cap_simps cap_master_cap_def vs_cap_ref_def 156 split: cap.splits )+ 157 apply (rename_tac acap1 acap2) 158 apply (case_tac acap1) 159 by (auto simp: acap_rights_update_def) 160 161lemma cap_range_update [simp, Ipc_AI_assms]: 162 "cap_range (cap_rights_update R cap) = cap_range cap" 163 by (simp add: cap_range_def cap_rights_update_def acap_rights_update_def 164 split: cap.splits arch_cap.splits) 165 166lemma derive_cap_idle[wp, Ipc_AI_assms]: 167 "\<lbrace>\<lambda>s. global_refs s \<inter> cap_range cap = {}\<rbrace> 168 derive_cap slot cap 169 \<lbrace>\<lambda>c s. global_refs s \<inter> cap_range c = {}\<rbrace>, -" 170 apply (simp add: derive_cap_def) 171 apply (rule hoare_pre) 172 apply (wpc| wp | simp add: arch_derive_cap_def)+ 173 apply (case_tac cap, simp_all add: cap_range_def) 174 apply (rename_tac arch_cap) 175 apply (case_tac arch_cap, simp_all) 176 done 177 178lemma arch_derive_cap_objrefs_iszombie [Ipc_AI_assms]: 179 "\<lbrace>\<lambda>s . P (set_option (aobj_ref cap)) False s\<rbrace> 180 arch_derive_cap cap 181 \<lbrace>\<lambda>rv s. rv \<noteq> NullCap \<longrightarrow> P (obj_refs rv) (is_zombie rv) s\<rbrace>,-" 182 apply(cases cap, simp_all add: is_zombie_def arch_derive_cap_def) 183 apply(rule hoare_pre, wpc?, wp+, simp)+ 184 done 185 186lemma obj_refs_remove_rights[simp, Ipc_AI_assms]: 187 "obj_refs (remove_rights rs cap) = obj_refs cap" 188 by (simp add: remove_rights_def cap_rights_update_def 189 acap_rights_update_def 190 split: cap.splits arch_cap.splits) 191 192lemma storeWord_um_inv: 193 "\<lbrace>\<lambda>s. underlying_memory s = um\<rbrace> 194 storeWord a v 195 \<lbrace>\<lambda>_ s. is_aligned a 2 \<and> x \<in> {a,a+1,a+2,a+3} \<or> underlying_memory s x = um x\<rbrace>" 196 apply (simp add: storeWord_def is_aligned_mask) 197 apply wp 198 apply simp 199 done 200 201lemma store_word_offs_vms[wp, Ipc_AI_assms]: 202 "\<lbrace>valid_machine_state\<rbrace> store_word_offs ptr offs v \<lbrace>\<lambda>_. valid_machine_state\<rbrace>" 203proof - 204 have aligned_offset_ignore: 205 "\<And>(l::word32) (p::word32) sz. l<4 \<Longrightarrow> p && mask 2 = 0 \<Longrightarrow> 206 p+l && ~~ mask (pageBitsForSize sz) = p && ~~ mask (pageBitsForSize sz)" 207 proof - 208 fix l p sz 209 assume al: "(p::word32) && mask 2 = 0" 210 assume "(l::word32) < 4" hence less: "l<2^2" by simp 211 have le: "2 \<le> pageBitsForSize sz" by (case_tac sz, simp_all) 212 show "?thesis l p sz" 213 by (rule is_aligned_add_helper[simplified is_aligned_mask, 214 THEN conjunct2, THEN mask_out_first_mask_some, 215 where n=2, OF al less le]) 216 qed 217 218 show ?thesis 219 apply (simp add: valid_machine_state_def store_word_offs_def 220 do_machine_op_def split_def) 221 apply wp 222 apply clarsimp 223 apply (drule_tac use_valid) 224 apply (rule_tac x=p in storeWord_um_inv, simp+) 225 apply (drule_tac x=p in spec) 226 apply (erule disjE, simp) 227 apply (erule disjE, simp_all) 228 apply (erule conjE) 229 apply (erule disjE, simp) 230 apply (simp add: in_user_frame_def word_size_def) 231 apply (erule exEI) 232 apply (subgoal_tac "(ptr + of_nat offs * 4) && ~~ mask (pageBitsForSize x) = 233 p && ~~ mask (pageBitsForSize x)", simp) 234 apply (simp only: is_aligned_mask[of _ 2]) 235 apply (elim disjE, simp_all) 236 apply (rule aligned_offset_ignore[symmetric], simp+)+ 237 done 238qed 239 240lemma is_zombie_update_cap_data[simp, Ipc_AI_assms]: 241 "is_zombie (update_cap_data P data cap) = is_zombie cap" 242 by (simp add: update_cap_data_closedform is_zombie_def 243 split: cap.splits) 244 245lemma valid_msg_length_strengthen [Ipc_AI_assms]: 246 "valid_message_info mi \<longrightarrow> unat (mi_length mi) \<le> msg_max_length" 247 apply (clarsimp simp: valid_message_info_def) 248 apply (subgoal_tac "unat (mi_length mi) \<le> unat (of_nat msg_max_length :: word32)") 249 apply (clarsimp simp: unat_of_nat msg_max_length_def) 250 apply (clarsimp simp: un_ui_le word_le_def) 251 done 252 253lemma copy_mrs_in_user_frame[wp, Ipc_AI_assms]: 254 "\<lbrace>in_user_frame p\<rbrace> copy_mrs t buf t' buf' n \<lbrace>\<lambda>rv. in_user_frame p\<rbrace>" 255 by (simp add: in_user_frame_def) (wp hoare_vcg_ex_lift) 256 257lemma as_user_getRestart_invs[wp]: "\<lbrace>P\<rbrace> as_user t getRestartPC \<lbrace>\<lambda>_. P\<rbrace>" 258 by (simp add: getRestartPC_def, rule user_getreg_inv) 259 260lemma make_arch_fault_msg_inv[wp]: "\<lbrace>P\<rbrace> make_arch_fault_msg f t \<lbrace>\<lambda>_. P\<rbrace>" 261 apply (cases f) 262 apply simp 263 apply wp 264 done 265 266lemma make_fault_message_inv[wp, Ipc_AI_assms]: 267 "\<lbrace>P\<rbrace> make_fault_msg ft t \<lbrace>\<lambda>rv. P\<rbrace>" 268 apply (cases ft, simp_all split del: if_split) 269 apply (wp as_user_inv getRestartPC_inv mapM_wp' 270 | simp add: getRegister_def)+ 271 done 272 273lemma do_fault_transfer_invs[wp, Ipc_AI_assms]: 274 "\<lbrace>invs and tcb_at receiver\<rbrace> 275 do_fault_transfer badge sender receiver recv_buf 276 \<lbrace>\<lambda>rv. invs\<rbrace>" 277 by (simp add: do_fault_transfer_def split_def | wp 278 | clarsimp split: option.split)+ 279 280lemma lookup_ipc_buffer_in_user_frame[wp, Ipc_AI_assms]: 281 "\<lbrace>valid_objs and tcb_at t\<rbrace> lookup_ipc_buffer b t 282 \<lbrace>case_option (\<lambda>_. True) in_user_frame\<rbrace>" 283 apply (simp add: lookup_ipc_buffer_def) 284 apply (wp get_cap_wp thread_get_wp | wpc | simp)+ 285 apply (clarsimp simp add: obj_at_def is_tcb) 286 apply (rename_tac dev p R sz m) 287 apply (subgoal_tac "in_user_frame (p + (tcb_ipc_buffer tcb && 288 mask (pageBitsForSize sz))) s", simp) 289 apply (frule (1) cte_wp_valid_cap) 290 apply (clarsimp simp add: valid_cap_def cap_aligned_def in_user_frame_def) 291 apply (thin_tac "case_option a b c" for a b c) 292 apply (rule_tac x=sz in exI) 293 apply (subst is_aligned_add_helper[THEN conjunct2]) 294 apply simp 295 apply (simp add: and_mask_less' word_bits_def) 296 apply (clarsimp simp: caps_of_state_cteD'[where P = "\<lambda>x. True",simplified,symmetric]) 297 apply (drule(1) CSpace_AI.tcb_cap_slot_regular) 298 apply simp 299 apply (simp add: is_nondevice_page_cap_def is_nondevice_page_cap_arch_def case_bool_If 300 split: if_splits) 301 done 302 303lemma transfer_caps_loop_cte_wp_at: 304 assumes imp: "\<And>cap. P cap \<Longrightarrow> \<not> is_untyped_cap cap" 305 shows "\<lbrace>cte_wp_at P sl and K (sl \<notin> set slots) and (\<lambda>s. \<forall>x \<in> set slots. cte_at x s)\<rbrace> 306 transfer_caps_loop ep buffer n caps slots mi 307 \<lbrace>\<lambda>rv. cte_wp_at P sl\<rbrace>" 308 apply (induct caps arbitrary: slots n mi) 309 apply (simp, wp, simp) 310 apply (clarsimp simp: Let_def split_def whenE_def 311 cong: if_cong list.case_cong 312 split del: if_split) 313 apply (rule hoare_pre) 314 apply (wp hoare_vcg_const_imp_lift hoare_vcg_const_Ball_lift 315 derive_cap_is_derived_foo 316 hoare_drop_imps 317 | assumption | simp split del: if_split)+ 318 apply (wp hoare_vcg_conj_lift cap_insert_weak_cte_wp_at2) 319 apply (erule imp) 320 apply (wp hoare_vcg_ball_lift 321 | clarsimp simp: is_cap_simps split del:if_split 322 | unfold derive_cap_def arch_derive_cap_def 323 | wpc 324 | rule conjI 325 | case_tac slots)+ 326 done 327 328lemma transfer_caps_tcb_caps: 329 fixes P t ref mi caps ep receiver recv_buf 330 assumes imp: "\<And>c. P c \<Longrightarrow> \<not> is_untyped_cap c" 331 shows 332 "\<lbrace>valid_objs and cte_wp_at P (t, ref) and tcb_at t\<rbrace> 333 transfer_caps mi caps ep receiver recv_buf 334 \<lbrace>\<lambda>rv. cte_wp_at P (t, ref)\<rbrace>" 335 apply (simp add: transfer_caps_def) 336 apply (wp hoare_vcg_const_Ball_lift hoare_vcg_const_imp_lift 337 transfer_caps_loop_cte_wp_at 338 | wpc | simp)+ 339 apply (erule imp) 340 apply (wp hoare_vcg_conj_lift hoare_vcg_const_imp_lift hoare_vcg_all_lift 341 ) 342 apply (rule_tac Q = "\<lambda>rv s. ( \<forall>x\<in>set rv. real_cte_at x s ) 343 \<and> cte_wp_at P (t, ref) s \<and> tcb_at t s" 344 in hoare_strengthen_post) 345 apply (wp get_rs_real_cte_at) 346 apply clarsimp 347 apply (drule(1) bspec) 348 apply (clarsimp simp:obj_at_def is_tcb is_cap_table) 349 apply (rule hoare_post_imp) 350 apply (rule_tac Q="\<lambda>x. real_cte_at x s" in ballEI, assumption) 351 apply (erule real_cte_at_cte) 352 apply (rule get_rs_real_cte_at) 353 apply clarsimp 354 done 355 356lemma transfer_caps_non_null_cte_wp_at: 357 assumes imp: "\<And>c. P c \<Longrightarrow> \<not> is_untyped_cap c" 358 shows "\<lbrace>valid_objs and cte_wp_at (P and ((\<noteq>) cap.NullCap)) ptr\<rbrace> 359 transfer_caps mi caps ep receiver recv_buf 360 \<lbrace>\<lambda>_. cte_wp_at (P and ((\<noteq>) cap.NullCap)) ptr\<rbrace>" 361 unfolding transfer_caps_def 362 apply simp 363 apply (rule hoare_pre) 364 apply (wp hoare_vcg_ball_lift transfer_caps_loop_cte_wp_at static_imp_wp 365 | wpc | clarsimp simp:imp)+ 366 apply (rule hoare_strengthen_post 367 [where Q="\<lambda>rv s'. (cte_wp_at ((\<noteq>) cap.NullCap) ptr) s' 368 \<and> (\<forall>x\<in>set rv. cte_wp_at ((=) cap.NullCap) x s')", 369 rotated]) 370 apply (clarsimp) 371 apply (rule conjI) 372 apply (erule contrapos_pn) 373 apply (drule_tac x=ptr in bspec, assumption) 374 apply (clarsimp elim!: cte_wp_at_orth) 375 apply (rule ballI) 376 apply (drule(1) bspec) 377 apply (erule cte_wp_cte_at) 378 apply (wp) 379 apply (auto simp: cte_wp_at_caps_of_state) 380 done 381 382crunch cte_wp_at[wp,Ipc_AI_assms]: do_fault_transfer "cte_wp_at P p" 383 384lemma do_normal_transfer_non_null_cte_wp_at [Ipc_AI_assms]: 385 assumes imp: "\<And>c. P c \<Longrightarrow> \<not> is_untyped_cap c" 386 shows "\<lbrace>valid_objs and cte_wp_at (P and ((\<noteq>) cap.NullCap)) ptr\<rbrace> 387 do_normal_transfer st send_buffer ep b gr rt recv_buffer 388 \<lbrace>\<lambda>_. cte_wp_at (P and ((\<noteq>) cap.NullCap)) ptr\<rbrace>" 389 unfolding do_normal_transfer_def 390 apply simp 391 apply (wp transfer_caps_non_null_cte_wp_at 392 | clarsimp simp:imp)+ 393 done 394 395lemma is_derived_ReplyCap [simp, Ipc_AI_assms]: 396 "\<And>m p. is_derived m p (cap.ReplyCap t False) = (\<lambda>c. is_master_reply_cap c \<and> obj_ref_of c = t)" 397 apply (subst fun_eq_iff) 398 apply clarsimp 399 apply (case_tac x, simp_all add: is_derived_def is_cap_simps 400 cap_master_cap_def conj_comms is_pt_cap_def 401 vs_cap_ref_def) 402 done 403 404lemma do_normal_transfer_tcb_caps: 405 assumes imp: "\<And>c. P c \<Longrightarrow> \<not> is_untyped_cap c" 406 shows 407 "\<lbrace>valid_objs and cte_wp_at P (t, ref) and tcb_at t\<rbrace> 408 do_normal_transfer st sb ep badge grant rt rb 409 \<lbrace>\<lambda>rv. cte_wp_at P (t, ref)\<rbrace>" 410 apply (simp add: do_normal_transfer_def) 411 apply (rule hoare_pre) 412 apply (wp hoare_drop_imps transfer_caps_tcb_caps 413 | simp add:imp)+ 414 done 415 416lemma do_ipc_transfer_tcb_caps [Ipc_AI_assms]: 417 assumes imp: "\<And>c. P c \<Longrightarrow> \<not> is_untyped_cap c" 418 shows 419 "\<lbrace>valid_objs and cte_wp_at P (t, ref) and tcb_at t\<rbrace> 420 do_ipc_transfer st ep b gr rt 421 \<lbrace>\<lambda>rv. cte_wp_at P (t, ref)\<rbrace>" 422 apply (simp add: do_ipc_transfer_def) 423 apply (rule hoare_pre) 424 apply (wp do_normal_transfer_tcb_caps hoare_drop_imps 425 | wpc | simp add:imp)+ 426 done 427 428lemma set_thread_state_valid_vso_at[wp]: 429 "\<lbrace>valid_vso_at a\<rbrace> set_thread_state s st \<lbrace>\<lambda>rv. valid_vso_at a\<rbrace>" 430 apply (clarsimp simp: valid_vso_at_def) 431 by (wpsimp wp: sts_obj_at_impossible sts_typ_ats hoare_vcg_ex_lift) 432 433lemma cap_insert_valid_vso_at[wp]: 434 "\<lbrace>valid_vso_at a\<rbrace> cap_insert c sl sl' \<lbrace>\<lambda>rv. valid_vso_at a\<rbrace>" 435 apply (clarsimp simp: valid_vso_at_def) 436 by (wpsimp wp: sts_obj_at_impossible sts_typ_ats hoare_vcg_ex_lift) 437 438lemma setup_caller_cap_valid_global_objs[wp, Ipc_AI_assms]: 439 "\<lbrace>valid_global_objs\<rbrace> setup_caller_cap send recv \<lbrace>\<lambda>rv. valid_global_objs\<rbrace>" 440 apply (wp valid_global_objs_lift valid_ao_at_lift) 441 apply (simp_all add: setup_caller_cap_def) 442 apply (wp sts_obj_at_impossible | simp add: tcb_not_empty_table)+ 443 done 444 445crunch typ_at[Ipc_AI_assms]: handle_arch_fault_reply, arch_get_sanitise_register_info "P (typ_at T p s)" 446 447lemma transfer_caps_loop_valid_vspace_objs[wp, Ipc_AI_assms]: 448 "\<lbrace>valid_vspace_objs\<rbrace> 449 transfer_caps_loop ep buffer n caps slots mi 450 \<lbrace>\<lambda>rv. valid_vspace_objs\<rbrace>" 451 apply (induct caps arbitrary: slots n mi, simp) 452 apply (clarsimp simp: Let_def split_def whenE_def 453 cong: if_cong list.case_cong 454 split del: if_split) 455 apply (rule hoare_pre) 456 apply (wp hoare_vcg_const_imp_lift hoare_vcg_const_Ball_lift 457 derive_cap_is_derived_foo 458 hoare_drop_imps 459 | assumption | simp split del: if_split)+ 460 done 461 462crunch aligned [wp, Ipc_AI_assms]: make_arch_fault_msg "pspace_aligned" 463crunch distinct [wp, Ipc_AI_assms]: make_arch_fault_msg "pspace_distinct" 464crunch vmdb [wp, Ipc_AI_assms]: make_arch_fault_msg "valid_mdb" 465crunch vmdb [wp, Ipc_AI_assms]: make_arch_fault_msg "valid_mdb" 466crunch ifunsafe [wp, Ipc_AI_assms]: make_arch_fault_msg "if_unsafe_then_cap" 467crunch iflive [wp, Ipc_AI_assms]: make_arch_fault_msg "if_live_then_nonz_cap" 468crunch state_refs_of [wp, Ipc_AI_assms]: make_arch_fault_msg "\<lambda>s. P (state_refs_of s)" 469crunch ct [wp, Ipc_AI_assms]: make_arch_fault_msg "cur_tcb" 470crunch zombies [wp, Ipc_AI_assms]: make_arch_fault_msg "zombies_final" 471crunch it [wp, Ipc_AI_assms]: make_arch_fault_msg "\<lambda>s. P (idle_thread s)" 472crunch valid_globals [wp, Ipc_AI_assms]: make_arch_fault_msg "valid_global_refs" 473crunch reply_masters [wp, Ipc_AI_assms]: make_arch_fault_msg "valid_reply_masters" 474crunch valid_idle [wp, Ipc_AI_assms]: make_arch_fault_msg "valid_idle" 475crunch arch [wp, Ipc_AI_assms]: make_arch_fault_msg "\<lambda>s. P (arch_state s)" 476crunch typ_at [wp, Ipc_AI_assms]: make_arch_fault_msg "\<lambda>s. P (typ_at T p s)" 477crunch irq_node [wp, Ipc_AI_assms]: make_arch_fault_msg "\<lambda>s. P (interrupt_irq_node s)" 478crunch valid_reply [wp, Ipc_AI_assms]: make_arch_fault_msg "valid_reply_caps" 479crunch irq_handlers [wp, Ipc_AI_assms]: make_arch_fault_msg "valid_irq_handlers" 480crunch vspace_objs [wp, Ipc_AI_assms]: make_arch_fault_msg "valid_vspace_objs" 481crunch global_objs [wp, Ipc_AI_assms]: make_arch_fault_msg "valid_global_objs" 482crunch global_vspace_mapping [wp, Ipc_AI_assms]: make_arch_fault_msg "valid_global_vspace_mappings" 483crunch arch_caps [wp, Ipc_AI_assms]: make_arch_fault_msg "valid_arch_caps" 484crunch v_ker_map [wp, Ipc_AI_assms]: make_arch_fault_msg "valid_kernel_mappings" 485crunch eq_ker_map [wp, Ipc_AI_assms]: make_arch_fault_msg "equal_kernel_mappings" 486crunch asid_map [wp, Ipc_AI_assms]: make_arch_fault_msg "valid_asid_map" 487crunch only_idle [wp, Ipc_AI_assms]: make_arch_fault_msg "only_idle" 488crunch pspace_in_kernel_window [wp, Ipc_AI_assms]: make_arch_fault_msg "pspace_in_kernel_window" 489crunch cap_refs_in_kernel_window [wp, Ipc_AI_assms]: make_arch_fault_msg "cap_refs_in_kernel_window" 490crunch valid_objs [wp, Ipc_AI_assms]: make_arch_fault_msg "valid_objs" 491crunch valid_ioc [wp, Ipc_AI_assms]: make_arch_fault_msg "valid_ioc" 492crunch pred_tcb [wp, Ipc_AI_assms]: make_arch_fault_msg "pred_tcb_at proj P t" 493crunch cap_to [wp, Ipc_AI_assms]: make_arch_fault_msg "ex_nonz_cap_to p" 494crunch pred_tcb [wp, Ipc_AI_assms]: make_arch_fault_msg "pred_tcb_at proj P t" 495declare make_arch_fault_msg_inv[Ipc_AI_assms] 496 497crunch obj_at[wp, Ipc_AI_assms]: make_arch_fault_msg "\<lambda>s. P (obj_at P' pd s)" 498 (wp: as_user_inv getRestartPC_inv mapM_wp' simp: getRegister_def) 499 500crunch vms[wp, Ipc_AI_assms]: make_arch_fault_msg valid_machine_state 501 (wp: as_user_inv getRestartPC_inv mapM_wp' simp: getRegister_def ignore: do_machine_op) 502 503crunch valid_irq_states[wp, Ipc_AI_assms]: make_arch_fault_msg "valid_irq_states" 504 (wp: as_user_inv getRestartPC_inv mapM_wp' simp: getRegister_def ignore: do_machine_op) 505 506crunch cap_refs_respects_device_region[wp, Ipc_AI_assms]: make_arch_fault_msg "cap_refs_respects_device_region" 507 (wp: as_user_inv getRestartPC_inv mapM_wp' simp: getRegister_def ignore: do_machine_op) 508 509end 510 511interpretation Ipc_AI?: Ipc_AI 512 proof goal_cases 513 interpret Arch . 514 case 1 show ?case by (unfold_locales; (fact Ipc_AI_assms)?) 515 qed 516 517context Arch begin global_naming ARM 518 519named_theorems Ipc_AI_cont_assms 520 521crunch pspace_respects_device_region[wp, Ipc_AI_cont_assms]: do_ipc_transfer "pspace_respects_device_region" 522 (wp: crunch_wps ignore: const_on_failure simp: crunch_simps) 523 524lemma do_ipc_transfer_respects_device_region[Ipc_AI_cont_assms]: 525 "\<lbrace>cap_refs_respects_device_region and tcb_at t and valid_objs and valid_mdb\<rbrace> 526 do_ipc_transfer t ep bg grt r 527 \<lbrace>\<lambda>rv. cap_refs_respects_device_region\<rbrace>" 528 apply (wpsimp simp: do_ipc_transfer_def do_normal_transfer_def transfer_caps_def bind_assoc 529 wp: hoare_vcg_all_lift hoare_drop_imps)+ 530 apply (subst ball_conj_distrib) 531 apply (wpsimp wp: get_rs_cte_at2 thread_get_wp static_imp_wp grs_distinct 532 hoare_vcg_ball_lift hoare_vcg_all_lift hoare_vcg_conj_lift 533 simp: obj_at_def is_tcb_def)+ 534 apply (simp split: kernel_object.split_asm) 535 done 536 537lemma set_mrs_state_hyp_refs_of[wp]: 538 "\<lbrace>\<lambda> s. P (state_hyp_refs_of s)\<rbrace> set_mrs thread buf msgs \<lbrace>\<lambda>_ s. P (state_hyp_refs_of s)\<rbrace>" 539 by (wp set_mrs_thread_set_dmo thread_set_hyp_refs_trivial | simp)+ 540 541crunch state_hyp_refs_of[wp, Ipc_AI_cont_assms]: do_ipc_transfer "\<lambda> s. P (state_hyp_refs_of s)" 542 (wp: crunch_wps simp: zipWithM_x_mapM) 543 544lemma arch_derive_cap_untyped: 545 "\<lbrace>\<lambda>s. P (untyped_range (ArchObjectCap cap))\<rbrace> arch_derive_cap cap \<lbrace>\<lambda>rv s. rv \<noteq> cap.NullCap \<longrightarrow> P (untyped_range rv)\<rbrace>,-" 546 by (wpsimp simp: arch_derive_cap_def) 547 548lemma valid_arch_mdb_cap_swap: 549 "\<And>s cap capb. 550 \<lbrakk>valid_arch_mdb (is_original_cap s) (caps_of_state s); 551 weak_derived c cap; caps_of_state s a = Some cap; 552 is_untyped_cap cap \<longrightarrow> cap = c; a \<noteq> b; 553 weak_derived c' capb; caps_of_state s b = Some capb\<rbrakk> 554 \<Longrightarrow> valid_arch_mdb 555 ((is_original_cap s) 556 (a := is_original_cap s b, b := is_original_cap s a)) 557 (caps_of_state s(a \<mapsto> c', b \<mapsto> c))" 558 by auto 559 560end 561 562interpretation Ipc_AI?: Ipc_AI_cont 563 proof goal_cases 564 interpret Arch . 565 case 1 show ?case by (unfold_locales;(fact Ipc_AI_cont_assms)?) 566 qed 567 568end 569