1(* 2 * Copyright 2014, NICTA 3 * 4 * This software may be distributed and modified according to the terms of 5 * the GNU General Public License version 2. Note that NO WARRANTY is provided. 6 * See "LICENSE_GPLv2.txt" for details. 7 * 8 * @TAG(NICTA_GPL) 9 *) 10 11theory Syscall_AC 12imports 13 Ipc_AC 14 Tcb_AC 15 Interrupt_AC 16 DomainSepInv 17begin 18 19context begin interpretation Arch . (*FIXME: arch_split*) 20 21definition 22 authorised_invocation :: "'a PAS \<Rightarrow> Invocations_A.invocation \<Rightarrow> 'z::state_ext state \<Rightarrow> bool" 23where 24 "authorised_invocation aag i \<equiv> \<lambda>s. case i of 25 Invocations_A.InvokeUntyped i' \<Rightarrow> valid_untyped_inv i' s \<and> (authorised_untyped_inv aag i') \<and> ct_active s 26 | Invocations_A.InvokeEndpoint epptr badge can_grant \<Rightarrow> 27 \<exists>ep. ko_at (Endpoint ep) epptr s \<and> 28 (can_grant \<longrightarrow> (\<forall>r \<in> ep_q_refs_of ep. snd r = EPRecv \<longrightarrow> is_subject aag (fst r)) \<and> aag_has_auth_to aag Grant epptr) 29 \<and> aag_has_auth_to aag SyncSend epptr 30 | Invocations_A.InvokeNotification ep badge \<Rightarrow> aag_has_auth_to aag Notify ep 31 | Invocations_A.InvokeReply thread slot \<Rightarrow> is_subject aag thread \<and> is_subject aag (fst slot) 32 | Invocations_A.InvokeTCB i' \<Rightarrow> Tcb_AI.tcb_inv_wf i' s \<and> authorised_tcb_inv aag i' 33 | Invocations_A.InvokeDomain thread slot \<Rightarrow> False 34 | Invocations_A.InvokeCNode i' \<Rightarrow> authorised_cnode_inv aag i' s \<and> is_subject aag (cur_thread s) 35 \<and> cnode_inv_auth_derivations i' s 36 | Invocations_A.InvokeIRQControl i' \<Rightarrow> authorised_irq_ctl_inv aag i' 37 | Invocations_A.InvokeIRQHandler i' \<Rightarrow> authorised_irq_hdl_inv aag i' 38 | Invocations_A.InvokeArchObject i' \<Rightarrow> valid_arch_inv i' s \<and> authorised_arch_inv aag i' \<and> ct_active s" 39 40lemma perform_invocation_pas_refined: 41 "\<lbrace>pas_refined aag and pas_cur_domain aag 42 and einvs and simple_sched_action and valid_invocation oper 43 and is_subject aag \<circ> cur_thread 44 and authorised_invocation aag oper\<rbrace> 45 perform_invocation blocking calling oper 46 \<lbrace>\<lambda>rv. pas_refined aag\<rbrace>" 47 apply (cases oper, simp_all) 48 apply (simp add: authorised_invocation_def validE_R_def[symmetric] invs_valid_objs 49 | wp invoke_untyped_pas_refined send_ipc_pas_refined send_signal_pas_refined 50 do_reply_transfer_pas_refined invoke_tcb_pas_refined invoke_cnode_pas_refined 51 invoke_irq_control_pas_refined invoke_irq_handler_pas_refined 52 invoke_arch_pas_refined decode_cnode_invocation_auth_derived 53 | fastforce)+ 54 done 55 56lemma ntfn_gives_obj_at: 57 "invs s \<Longrightarrow> (\<exists>ntfn. ko_at (Notification ntfn) ntfnptr s \<and> (\<forall>x\<in>ntfn_q_refs_of (ntfn_obj ntfn). (\<lambda>(t, rt). obj_at (\<lambda>tcb. ko_at tcb t s) t s) x)) = ntfn_at ntfnptr s" 58 apply (rule iffI) 59 apply (clarsimp simp: obj_at_def is_ntfn) 60 apply (clarsimp simp: obj_at_def is_ntfn) 61 apply (drule (1) ntfn_queued_st_tcb_at [where P = \<top>, unfolded obj_at_def, simplified]) 62 apply clarsimp 63 apply clarsimp 64 apply (clarsimp simp: st_tcb_def2 dest!: get_tcb_SomeD) 65 done 66 67lemma pi_cases: 68 "perform_invocation block call i = 69 (case i of 70 Invocations_A.InvokeUntyped i \<Rightarrow> perform_invocation block call (Invocations_A.InvokeUntyped i) 71 | Invocations_A.InvokeEndpoint ep badge canGrant 72 \<Rightarrow> perform_invocation block call (Invocations_A.InvokeEndpoint ep badge canGrant) 73 | Invocations_A.InvokeNotification ep badge \<Rightarrow> perform_invocation block call ( Invocations_A.InvokeNotification ep badge) 74 | Invocations_A.InvokeTCB i \<Rightarrow> perform_invocation block call ( Invocations_A.InvokeTCB i) 75 | Invocations_A.InvokeDomain thread slot \<Rightarrow> perform_invocation block call ( Invocations_A.InvokeDomain thread slot) 76 | Invocations_A.InvokeReply thread slot \<Rightarrow> perform_invocation block call ( Invocations_A.InvokeReply thread slot) 77 | Invocations_A.InvokeCNode i \<Rightarrow> perform_invocation block call ( Invocations_A.InvokeCNode i) 78 | Invocations_A.InvokeIRQControl i \<Rightarrow> perform_invocation block call ( Invocations_A.InvokeIRQControl i) 79 | Invocations_A.InvokeIRQHandler i \<Rightarrow> perform_invocation block call ( Invocations_A.InvokeIRQHandler i) 80 | Invocations_A.InvokeArchObject i \<Rightarrow> perform_invocation block call ( Invocations_A.InvokeArchObject i))" 81 by (cases i, simp_all) 82 83(* ((=) st) -- too strong, the thread state of the calling thread changes. *) 84lemma perform_invocation_respects: 85 "\<lbrace>pas_refined aag and integrity aag X st 86 and einvs and simple_sched_action and valid_invocation oper 87 and authorised_invocation aag oper 88 and is_subject aag \<circ> cur_thread 89 and (\<lambda>s. \<forall>p ko. kheap s p = Some ko \<longrightarrow> \<not> (is_tcb ko \<and> p = cur_thread st) \<longrightarrow> kheap st p = Some ko) 90 \<rbrace> 91 perform_invocation blocking calling oper 92 \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>" 93 apply (subst pi_cases) 94 apply (rule hoare_pre) 95 apply (wpc 96 | simp 97 | wp invoke_untyped_integrity send_ipc_integrity_autarch send_signal_respects 98 do_reply_transfer_respects invoke_tcb_respects invoke_cnode_respects 99 invoke_arch_respects invoke_irq_control_respects invoke_irq_handler_respects 100 | wp_once hoare_pre_cont)+ 101 apply (clarsimp simp: authorised_invocation_def split: Invocations_A.invocation.splits) 102 \<comment> \<open>EP case\<close> 103 apply (fastforce simp: obj_at_def is_tcb split: if_split_asm) 104 \<comment> \<open>NTFN case\<close> 105 apply fastforce 106 done 107 108declare AllowSend_def[simp] AllowRecv_def[simp] 109 110lemma diminshed_IRQControlCap_eq: 111 "diminished IRQControlCap = ((=) IRQControlCap)" 112 apply (rule ext) 113 apply (case_tac x, auto simp: diminished_def mask_cap_def cap_rights_update_def) 114 done 115 116lemma diminished_DomainCap_eq: 117 "diminished DomainCap = ((=) DomainCap)" 118 apply (rule ext) 119 apply (case_tac x, auto simp: diminished_def mask_cap_def cap_rights_update_def) 120 done 121 122lemma hoare_conjunct1_R: 123 "\<lbrace> P \<rbrace> f \<lbrace> \<lambda> r s. Q r s \<and> Q' r s\<rbrace>,- \<Longrightarrow> \<lbrace> P \<rbrace> f \<lbrace> Q \<rbrace>,-" 124 apply(auto intro: hoare_post_imp_R) 125 done 126 127lemma hoare_conjunct2_R: 128 "\<lbrace> P \<rbrace> f \<lbrace> \<lambda> r s. Q r s \<and> Q' r s\<rbrace>,- \<Longrightarrow> \<lbrace> P \<rbrace> f \<lbrace> Q' \<rbrace>,-" 129 apply(auto intro: hoare_post_imp_R) 130 done 131 132lemma decode_invocation_authorised: 133 "\<lbrace>pas_refined aag and valid_cap cap and invs and ct_active and cte_wp_at (diminished cap) slot 134 and ex_cte_cap_to slot 135 and (\<lambda>s. \<forall>r\<in>zobj_refs cap. ex_nonz_cap_to r s) 136 and (\<lambda>s. \<forall>r\<in>cte_refs cap (interrupt_irq_node s). ex_cte_cap_to r s) 137 and (\<lambda>s. \<forall>cap \<in> set excaps. \<forall>r\<in>cte_refs (fst cap) (interrupt_irq_node s). ex_cte_cap_to r s) 138 and (\<lambda>s. \<forall>x \<in> set excaps. s \<turnstile> (fst x)) 139 and (\<lambda>s. \<forall>x \<in> set excaps. \<forall>r\<in>zobj_refs (fst x). ex_nonz_cap_to r s) 140 and (\<lambda>s. \<forall>x \<in> set excaps. cte_wp_at (diminished (fst x)) (snd x) s) 141 and (\<lambda>s. \<forall>x \<in> set excaps. real_cte_at (snd x) s) 142 and (\<lambda>s. \<forall>x \<in> set excaps. ex_cte_cap_wp_to is_cnode_cap (snd x) s) 143 and (\<lambda>s. \<forall>x \<in> set excaps. cte_wp_at (interrupt_derived (fst x)) (snd x) s) 144 and (is_subject aag \<circ> cur_thread) and 145 K (is_subject aag (fst slot) \<and> pas_cap_cur_auth aag cap 146 \<and> (\<forall>slot \<in> set excaps. is_subject aag (fst (snd slot))) 147 \<and> (\<forall>slot \<in> set excaps. pas_cap_cur_auth aag (fst slot))) 148 and domain_sep_inv (pasMaySendIrqs aag) st'\<rbrace> 149 decode_invocation info_label args ptr slot cap excaps 150 \<lbrace>\<lambda>rv. authorised_invocation aag rv\<rbrace>, -" 151 unfolding decode_invocation_def 152 apply (rule hoare_pre) 153 apply (wp decode_untyped_invocation_authorised 154 decode_cnode_invocation_auth_derived 155 decode_cnode_inv_authorised 156 decode_tcb_invocation_authorised decode_tcb_inv_wf 157 decode_arch_invocation_authorised 158 | strengthen cnode_diminished_strg 159 | wpc | simp add: comp_def authorised_invocation_def decode_invocation_def 160 split del: if_split del: hoare_post_taut hoare_True_E_R 161 | wp_once hoare_FalseE_R)+ 162 163 apply (clarsimp simp: aag_has_Control_iff_owns split_def aag_cap_auth_def) 164 apply (cases cap, simp_all) 165 apply (fastforce simp: cte_wp_at_caps_of_state) 166 apply (clarsimp simp: valid_cap_def obj_at_def is_ep cap_auth_conferred_def cap_rights_to_auth_def 167 ball_Un) 168 apply (fastforce simp: valid_cap_def cap_auth_conferred_def cap_rights_to_auth_def obj_at_def is_ep intro!: owns_ep_owns_receivers) 169 apply (fastforce simp: cap_auth_conferred_def cap_rights_to_auth_def) 170 apply (fastforce simp: cap_auth_conferred_def cap_rights_to_auth_def pas_refined_Control [symmetric]) 171 apply ((clarsimp simp: valid_cap_def cte_wp_at_eq_simp 172 is_cap_simps 173 ex_cte_cap_wp_to_weakenE[OF _ TrueI] 174 cap_auth_conferred_def cap_rights_to_auth_def pas_refined_all_auth_is_owns 175 | rule conjI | (subst split_paired_Ex[symmetric], erule exI) 176 | erule cte_wp_at_weakenE 177 | drule(1) bspec 178 | erule diminished_no_cap_to_obj_with_diff_ref)+)[1] 179 apply (simp only: domain_sep_inv_def diminished_DomainCap_eq) 180 apply (rule impI, erule subst, rule pas_refined_sita_mem [OF sita_controlled], auto 181 simp: cte_wp_at_caps_of_state diminshed_IRQControlCap_eq)[1] 182 183 apply (clarsimp simp add: cap_links_irq_def ) 184 apply (drule (1) pas_refined_Control, simp) 185 186 apply (clarsimp simp: cap_links_asid_slot_def label_owns_asid_slot_def) 187 apply (fastforce dest!: pas_refined_Control) 188 done 189 190lemma in_extended: "(u,a) \<in> fst (do_extended_op f s) \<Longrightarrow> \<exists>e. a = (trans_state (\<lambda>_. e) s)" 191 apply (clarsimp simp add: do_extended_op_def bind_def gets_def return_def get_def 192 mk_ef_def modify_def select_f_def put_def trans_state_update') 193 apply force 194 done 195 196lemma set_thread_state_authorised[wp]: 197 "\<lbrace>authorised_invocation aag i and (\<lambda>s. thread = cur_thread s) and valid_objs\<rbrace> 198 set_thread_state thread Structures_A.thread_state.Restart 199 \<lbrace>\<lambda>rv. authorised_invocation aag i\<rbrace>" 200 apply (cases i) 201 apply (simp_all add: authorised_invocation_def) 202 apply (wp sts_valid_untyped_inv ct_in_state_set 203 hoare_vcg_ex_lift sts_obj_at_impossible 204 | simp)+ 205 apply (rename_tac cnode_invocation) 206 apply (case_tac cnode_invocation, 207 simp_all add: cnode_inv_auth_derivations_def authorised_cnode_inv_def)[1] 208 apply (wp set_thread_state_cte_wp_at | simp)+ 209 apply (rename_tac arch_invocation) 210 apply (case_tac arch_invocation, simp_all add: valid_arch_inv_def)[1] 211 apply (rename_tac page_table_invocation) 212 apply (case_tac page_table_invocation, simp_all add: valid_pti_def)[1] 213 apply (wp sts_typ_ats sts_obj_at_impossible ct_in_state_set 214 hoare_vcg_ex_lift hoare_vcg_conj_lift 215 | simp add: valid_pdi_def)+ 216 apply (rename_tac asid_control_invocation) 217 apply (case_tac asid_control_invocation, simp_all add: valid_aci_def) 218 apply (wp ct_in_state_set | simp)+ 219 apply (rename_tac asid_pool_invocation) 220 apply (case_tac asid_pool_invocation; simp add: valid_apinv_def) 221 apply (wp sts_obj_at_impossible ct_in_state_set 222 hoare_vcg_ex_lift 223 | simp)+ 224 done 225 226lemma sts_first_restart: 227 "\<lbrace>(=) st and (\<lambda>s. thread = cur_thread s)\<rbrace> 228 set_thread_state thread Structures_A.thread_state.Restart 229 \<lbrace>\<lambda>rv s. \<forall>p ko. kheap s p = Some ko \<longrightarrow> 230 (is_tcb ko \<longrightarrow> p \<noteq> cur_thread st) \<longrightarrow> kheap st p = Some ko\<rbrace>" 231 unfolding set_thread_state_def set_object_def 232 apply (wp dxo_wp_weak |simp)+ 233 apply (clarsimp simp: is_tcb) 234 done 235 236lemma lcs_reply_owns: 237 "\<lbrace>pas_refined aag and K (is_subject aag thread)\<rbrace> 238 lookup_cap_and_slot thread ptr 239 \<lbrace>\<lambda>rv s. \<forall>ep. (\<exists>m. fst rv = cap.ReplyCap ep m) \<longrightarrow> is_subject aag ep\<rbrace>, -" 240 apply (rule hoare_post_imp_R) 241 apply (rule hoare_pre) 242 apply (rule hoare_vcg_conj_lift_R [where S = "K (pas_refined aag)"]) 243 apply (rule lookup_cap_and_slot_cur_auth) 244 apply (simp | wp lookup_cap_and_slot_inv)+ 245 apply (clarsimp simp: aag_cap_auth_Reply) 246 done 247 248crunch pas_refined[wp]: reply_from_kernel "pas_refined aag" 249 (simp: split_def) 250 251lemma lookup_cap_and_slot_valid_fault3: 252 "\<lbrace>valid_objs\<rbrace> lookup_cap_and_slot thread cptr 253 -, 254 \<lbrace>\<lambda>ft s. valid_fault (ExceptionTypes_A.CapFault (of_bl cptr) rp ft)\<rbrace>" 255 apply (unfold validE_E_def) 256 apply (rule hoare_post_impErr) 257 apply (rule lookup_cap_and_slot_valid_fault) 258 apply auto 259 done 260 261declare hoare_post_taut [simp del] 262 263crunch pas_cur_domain[wp]: as_user "pas_cur_domain aag" 264 265definition guarded_pas_domain 266 where 267 "guarded_pas_domain aag \<equiv> 268 \<lambda>s. cur_thread s \<noteq> idle_thread s \<longrightarrow> 269 pasObjectAbs aag (cur_thread s) \<in> pasDomainAbs aag (cur_domain s)" 270 271 272lemma guarded_pas_domain_lift: 273 assumes a: "\<And>P. \<lbrace>\<lambda>s. P (cur_thread s)\<rbrace> f \<lbrace>\<lambda>r s. P (cur_thread s)\<rbrace>" 274 assumes b: "\<And>P. \<lbrace>\<lambda>s. P (cur_domain s)\<rbrace> f \<lbrace>\<lambda>r s. P (cur_domain s)\<rbrace>" 275 assumes c: "\<And>P. \<lbrace>\<lambda>s. P (idle_thread s)\<rbrace> f \<lbrace>\<lambda>r s. P (idle_thread s)\<rbrace>" 276 shows "\<lbrace>guarded_pas_domain aag\<rbrace> f \<lbrace>\<lambda>_. guarded_pas_domain aag\<rbrace>" 277 apply (simp add: guarded_pas_domain_def) 278 apply (rule hoare_pre) 279 apply (wps a b c) 280 apply wp 281 apply simp 282 done 283 284lemma guarded_to_cur_domain: "\<lbrakk>invs s; ct_in_state x s; \<not> x IdleThreadState; guarded_pas_domain aag s; is_subject aag (cur_thread s)\<rbrakk> \<Longrightarrow> pas_cur_domain aag s" 285 apply (auto simp: invs_def valid_state_def valid_idle_def pred_tcb_at_def obj_at_def 286 ct_in_state_def guarded_pas_domain_def) 287 done 288 289 290lemma handle_invocation_pas_refined: 291 shows "\<lbrace>pas_refined aag and guarded_pas_domain aag and domain_sep_inv (pasMaySendIrqs aag) st' 292 and einvs and ct_active and schact_is_rct 293 and is_subject aag \<circ> cur_thread\<rbrace> 294 handle_invocation calling blocking 295 \<lbrace>\<lambda>rv. pas_refined aag\<rbrace>" 296 apply (simp add: handle_invocation_def split_def) 297 apply (cases blocking, simp) 298 apply (rule hoare_pre) 299 apply (((wp syscall_valid without_preemption_wp 300 handle_fault_pas_refined set_thread_state_pas_refined 301 set_thread_state_runnable_valid_sched 302 perform_invocation_pas_refined 303 hoare_vcg_conj_lift hoare_vcg_all_lift 304 | wpc 305 | rule hoare_drop_imps 306 | simp add: if_apply_def2 conj_comms split del: if_split 307 del: hoare_True_E_R)+), 308 ((wp lookup_extra_caps_auth lookup_extra_caps_authorised 309 decode_invocation_authorised 310 lookup_cap_and_slot_authorised 311 lookup_cap_and_slot_cur_auth 312 as_user_pas_refined 313 lookup_cap_and_slot_valid_fault3 314 | simp add: split comp_def runnable_eq_active del: if_split)+), 315 (auto intro: guarded_to_cur_domain 316 simp: ct_in_state_def st_tcb_at_def live_def hyp_live_def 317 intro: if_live_then_nonz_capD)[1])+ 318 done 319 320lemma handle_invocation_respects: 321 "\<lbrace>integrity aag X st and pas_refined aag and guarded_pas_domain aag and domain_sep_inv (pasMaySendIrqs aag) st' 322 and einvs and ct_active and schact_is_rct 323 and is_subject aag \<circ> cur_thread 324 and ((=) st)\<rbrace> 325 handle_invocation calling blocking 326 \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>" 327 apply (simp add: handle_invocation_def split_def) 328 apply (wp syscall_valid without_preemption_wp handle_fault_integrity_autarch 329 reply_from_kernel_integrity_autarch 330 set_thread_state_integrity_autarch 331 hoare_vcg_conj_lift 332 hoare_vcg_all_lift_R hoare_vcg_all_lift 333 | rule hoare_drop_imps 334 | wpc | simp add: if_apply_def2 335 del: hoare_post_taut hoare_True_E_R 336 split del: if_split)+ 337 apply (simp add: conj_comms pred_conj_def comp_def if_apply_def2 split del: if_split 338 | wp perform_invocation_respects set_thread_state_pas_refined 339 set_thread_state_authorised 340 set_thread_state_runnable_valid_sched 341 set_thread_state_integrity_autarch 342 sts_first_restart 343 decode_invocation_authorised 344 lookup_extra_caps_auth lookup_extra_caps_authorised 345 set_thread_state_integrity_autarch 346 lookup_cap_and_slot_cur_auth lookup_cap_and_slot_authorised 347 hoare_vcg_const_imp_lift perform_invocation_pas_refined 348 set_thread_state_ct_st hoare_vcg_const_imp_lift_R 349 lookup_cap_and_slot_valid_fault3 350 | (rule valid_validE, strengthen invs_vobjs_strgs) 351 )+ 352 apply (fastforce intro: st_tcb_ex_cap' guarded_to_cur_domain simp: ct_in_state_def runnable_eq_active)+ 353 done 354 355crunch pas_refined[wp]: delete_caller_cap "pas_refined aag" 356 357crunch cur_thread[wp]: delete_caller_cap "\<lambda>s. P (cur_thread s)" 358 359lemma invs_sym_refs_strg: 360 "invs s \<longrightarrow> sym_refs (state_refs_of s)" by clarsimp 361 362lemma lookup_slot_for_thread_cap_fault: 363 "\<lbrace>invs\<rbrace> lookup_slot_for_thread t s -, \<lbrace>\<lambda>f s. valid_fault (CapFault x y f)\<rbrace>" 364 apply (simp add: lookup_slot_for_thread_def) 365 apply (wp resolve_address_bits_valid_fault2) 366 apply clarsimp 367 apply (erule (1) invs_valid_tcb_ctable) 368 done 369 370lemma handle_recv_pas_refined: 371 "\<lbrace>pas_refined aag and invs and is_subject aag \<circ> cur_thread\<rbrace> handle_recv is_blocking \<lbrace>\<lambda>rv. pas_refined aag\<rbrace>" 372 apply (simp add: handle_recv_def Let_def lookup_cap_def lookup_cap_def split_def) 373 apply (wp handle_fault_pas_refined receive_ipc_pas_refined receive_signal_pas_refined 374 get_cap_auth_wp [where aag=aag] lookup_slot_for_cnode_op_authorised 375 lookup_slot_for_thread_authorised lookup_slot_for_thread_cap_fault 376 hoare_vcg_all_lift_R get_simple_ko_wp 377 | wpc | simp 378 | rename_tac word1 word2 word3, rule_tac Q="\<lambda>rv s. invs s \<and> is_subject aag thread 379 \<and> (pasSubject aag, Receive, pasObjectAbs aag word1) \<in> pasPolicy aag" 380 in hoare_strengthen_post, wp, clarsimp simp: invs_valid_objs invs_sym_refs)+ 381 apply (rule_tac Q' = "\<lambda>rv s. pas_refined aag s \<and> invs s \<and> tcb_at thread s 382 \<and> cur_thread s = thread \<and> is_subject aag (cur_thread s) 383 \<and> is_subject aag thread" in hoare_post_imp_R [rotated]) 384 apply (fastforce simp: aag_cap_auth_def cap_auth_conferred_def cap_rights_to_auth_def valid_fault_def) 385 apply (wp user_getreg_inv | strengthen invs_vobjs_strgs invs_sym_refs_strg | simp)+ 386 apply clarsimp 387 done 388 389crunch respects[wp]: delete_caller_cap "integrity aag X st" 390 391lemma invs_mdb_strgs: "invs s \<longrightarrow> valid_mdb s" 392 by(auto) 393 394lemma handle_recv_integrity: 395 "\<lbrace>integrity aag X st and pas_refined aag and einvs and is_subject aag \<circ> cur_thread\<rbrace> 396 handle_recv is_blocking 397 \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>" 398 apply (simp add: handle_recv_def Let_def lookup_cap_def lookup_cap_def split_def) 399 apply (wp handle_fault_integrity_autarch receive_ipc_integrity_autarch receive_signal_integrity_autarch lookup_slot_for_thread_authorised lookup_slot_for_thread_cap_fault 400 get_cap_auth_wp [where aag=aag] get_simple_ko_wp 401 | wpc | simp 402 | rule_tac Q="\<lambda>rv s. invs s \<and> is_subject aag thread 403 \<and> (pasSubject aag, Receive, pasObjectAbs aag x31) \<in> pasPolicy aag" 404 in hoare_strengthen_post, wp, clarsimp simp: invs_valid_objs invs_sym_refs)+ 405 apply (rule_tac Q' = "\<lambda>rv s. pas_refined aag s \<and> einvs s \<and> is_subject aag (cur_thread s) 406 \<and> tcb_at thread s \<and> cur_thread s = thread 407 \<and> is_subject aag thread \<and> integrity aag X st s" in hoare_post_imp_R [rotated]) 408 apply (fastforce simp: aag_cap_auth_def cap_auth_conferred_def 409 cap_rights_to_auth_def valid_fault_def) 410 apply (wp user_getreg_inv | strengthen invs_vobjs_strgs invs_sym_refs_strg invs_mdb_strgs | simp)+ 411 apply clarsimp 412 done 413 414lemma handle_reply_pas_refined[wp]: 415 "\<lbrace> pas_refined aag and invs and is_subject aag \<circ> cur_thread\<rbrace> 416 handle_reply 417 \<lbrace>\<lambda>rv. pas_refined aag\<rbrace>" 418 unfolding handle_reply_def 419 apply (rule hoare_pre) 420 apply (wp do_reply_transfer_pas_refined get_cap_auth_wp [where aag = aag]| wpc)+ 421 apply (clarsimp simp: aag_cap_auth_Reply) 422 done 423 424lemma handle_reply_respects: 425 "\<lbrace>integrity aag X st and pas_refined aag 426 and einvs 427 and is_subject aag \<circ> cur_thread\<rbrace> 428 handle_reply 429 \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>" 430 unfolding handle_reply_def 431 apply (rule hoare_pre) 432 apply (wp do_reply_transfer_respects get_cap_auth_wp [where aag = aag]| wpc)+ 433 apply (clarsimp simp: aag_cap_auth_Reply) 434 done 435 436lemma ethread_set_time_slice_pas_refined[wp]: 437 "\<lbrace>pas_refined aag\<rbrace> 438 ethread_set (tcb_time_slice_update f) thread 439 \<lbrace>\<lambda>rv. pas_refined aag\<rbrace>" 440 apply (simp add: ethread_set_def set_eobject_def | wp)+ 441 apply (clarsimp simp: pas_refined_def tcb_domain_map_wellformed_aux_def) 442 apply (erule_tac x="(a, b)" in ballE) 443 apply force 444 apply (erule notE) 445 apply (erule domains_of_state_aux.cases, simp add: get_etcb_def split: if_split_asm) 446 apply (force intro: domtcbs)+ 447 done 448 449lemma thread_set_time_slice_pas_refined[wp]: 450 "\<lbrace>pas_refined aag\<rbrace> 451 thread_set_time_slice tptr time 452 \<lbrace>\<lambda>rv. pas_refined aag\<rbrace>" 453 apply (simp add: thread_set_time_slice_def | wp)+ 454 done 455 456lemma dec_domain_time_pas_refined[wp]: 457 "\<lbrace>pas_refined aag\<rbrace> 458 dec_domain_time 459 \<lbrace>\<lambda>rv. pas_refined aag\<rbrace>" 460 apply (simp add: dec_domain_time_def | wp)+ 461 apply (clarsimp simp: pas_refined_def tcb_domain_map_wellformed_aux_def) 462 done 463 464crunch pas_refined[wp]: timer_tick "pas_refined aag" 465 (wp_del: timer_tick_extended.pas_refined_tcb_domain_map_wellformed) 466 467lemma handle_interrupt_pas_refined: 468 "\<lbrace>pas_refined aag\<rbrace> 469 handle_interrupt irq 470 \<lbrace>\<lambda>rv. pas_refined aag\<rbrace>" 471 apply (simp add: handle_interrupt_def) 472 apply (rule conjI; rule impI;rule hoare_pre) 473 apply (wp send_signal_pas_refined get_cap_wp 474 | wpc 475 | simp add: get_irq_slot_def get_irq_state_def handle_reserved_irq_def)+ 476 done 477 478lemma dec_domain_time_integrity[wp]: 479 "\<lbrace>integrity aag X st\<rbrace> 480 dec_domain_time 481 \<lbrace>\<lambda>_. integrity aag X st\<rbrace>" 482 apply (simp add: dec_domain_time_def | wp)+ 483 apply (clarsimp simp: integrity_subjects_def) 484 done 485 486lemma timer_tick_integrity[wp]: 487 "\<lbrace>integrity aag X st and pas_refined aag and (\<lambda>s. ct_active s \<longrightarrow> is_subject aag (cur_thread s))\<rbrace> 488 timer_tick 489 \<lbrace>\<lambda>_. integrity aag X st\<rbrace>" 490 apply (simp add: timer_tick_def) 491 apply (wp ethread_set_integrity_autarch gts_wp 492 | wpc | simp add: thread_set_time_slice_def split del: if_split)+ 493 apply (clarsimp simp: ct_in_state_def st_tcb_at_def obj_at_def) 494 done 495 496lemma handle_interrupt_integrity_autarch: 497 "\<lbrace>integrity aag X st and pas_refined aag 498 and invs and (\<lambda>s. ct_active s \<longrightarrow> is_subject aag (cur_thread s)) 499 and K (is_subject_irq aag irq)\<rbrace> 500 handle_interrupt irq 501 \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>" 502 apply (simp add: handle_interrupt_def cong: irq_state.case_cong maskInterrupt_def ackInterrupt_def resetTimer_def ) 503 apply (rule conjI; rule impI; rule hoare_pre) 504 apply (wp_once send_signal_respects get_cap_auth_wp [where aag = aag] dmo_mol_respects 505 | simp add: get_irq_slot_def get_irq_state_def ackInterrupt_def resetTimer_def handle_reserved_irq_def 506 | wp dmo_no_mem_respects 507 | wpc)+ 508 apply (fastforce simp: is_cap_simps aag_cap_auth_def cap_auth_conferred_def cap_rights_to_auth_def) 509 done 510 511lemma hacky_ipc_Send: 512 "\<lbrakk> (pasObjectAbs aag (interrupt_irq_node s irq), Notify, pasObjectAbs aag p) \<in> pasPolicy aag; pas_refined aag s; pasMaySendIrqs aag \<rbrakk> 513 \<Longrightarrow> aag_has_auth_to aag Notify p" 514 unfolding pas_refined_def 515 apply (clarsimp simp: policy_wellformed_def irq_map_wellformed_aux_def) 516 apply (drule spec [where x = "pasIRQAbs aag irq"], drule spec [where x = "pasObjectAbs aag p"], erule mp) 517 apply simp 518 done 519 520 521lemma handle_interrupt_integrity: 522 "\<lbrace>integrity aag X st and pas_refined aag and invs and (\<lambda>s. pasMaySendIrqs aag \<or> interrupt_states s irq \<noteq> IRQSignal) 523 and (\<lambda>s. ct_active s \<longrightarrow> is_subject aag (cur_thread s))\<rbrace> 524 handle_interrupt irq 525 \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>" 526 apply (simp add: handle_interrupt_def maskInterrupt_def ackInterrupt_def resetTimer_def cong: irq_state.case_cong bind_cong) 527 apply (rule conjI; rule impI; rule hoare_pre) 528 apply (wp_once send_signal_respects get_cap_wp dmo_mol_respects dmo_no_mem_respects 529 | wpc 530 | simp add: get_irq_slot_def get_irq_state_def ackInterrupt_def resetTimer_def handle_reserved_irq_def)+ 531 apply clarsimp 532 apply (rule conjI, fastforce)+ \<comment> \<open>valid_objs etc.\<close> 533 apply (clarsimp simp: cte_wp_at_caps_of_state) 534 apply (rule_tac s = s in hacky_ipc_Send [where irq = irq]) 535 apply (drule (1) cap_auth_caps_of_state) 536 apply (clarsimp simp: aag_cap_auth_def is_cap_simps cap_auth_conferred_def cap_rights_to_auth_def split: if_split_asm) 537 apply assumption+ 538 done 539 540lemma handle_vm_fault_integrity: 541 "\<lbrace>integrity aag X st and K (is_subject aag thread)\<rbrace> 542 handle_vm_fault thread vmfault_type 543 \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>" 544 apply (cases vmfault_type, simp_all) 545 apply (rule hoare_pre) 546 apply (wp as_user_integrity_autarch dmo_wp | simp add: getDFSR_def getFAR_def getIFSR_def)+ 547 done 548 549lemma handle_vm_pas_refined[wp]: 550 "\<lbrace>pas_refined aag\<rbrace> 551 handle_vm_fault thread vmfault_type 552 \<lbrace>\<lambda>rv. pas_refined aag\<rbrace>" 553 apply (cases vmfault_type, simp_all) 554 apply (wp | simp)+ 555 done 556 557crunch pas_refined[wp]: handle_hypervisor_fault "pas_refined aag" 558crunch cur_thread[wp]: handle_hypervisor_fault "\<lambda>s. P (cur_thread s)" 559crunch integrity[wp]: handle_hypervisor_fault "integrity aag X st" 560 561lemma handle_vm_cur_thread [wp]: 562 "\<lbrace>\<lambda>s. P (cur_thread s)\<rbrace> 563 handle_vm_fault thread vmfault_type 564 \<lbrace>\<lambda>rv s. P (cur_thread s)\<rbrace>" 565 apply (cases vmfault_type, simp_all) 566 apply (wp | simp)+ 567 done 568 569lemma handle_vm_state_refs_of [wp]: 570 "\<lbrace>\<lambda>s. P (state_refs_of s)\<rbrace> 571 handle_vm_fault thread vmfault_type 572 \<lbrace>\<lambda>rv s. P (state_refs_of s)\<rbrace>" 573 apply (cases vmfault_type, simp_all) 574 apply (wp | simp)+ 575 done 576 577lemma handle_yield_pas_refined[wp]: 578 "\<lbrace>pas_refined aag\<rbrace> 579 handle_yield 580 \<lbrace>\<lambda>rv. pas_refined aag\<rbrace>" 581 by (simp add: handle_yield_def | wp)+ 582 583 584 585lemma handle_event_pas_refined: 586 "\<lbrace>pas_refined aag and guarded_pas_domain aag and domain_sep_inv (pasMaySendIrqs aag) st' 587 and einvs and schact_is_rct 588 and (\<lambda>s. ev \<noteq> Interrupt \<longrightarrow> is_subject aag (cur_thread s)) and (\<lambda>s. ev \<noteq> Interrupt \<longrightarrow> ct_active s) \<rbrace> 589 handle_event ev 590 \<lbrace>\<lambda>rv. pas_refined aag\<rbrace>" 591 apply (case_tac ev; simp) 592 apply (rename_tac syscall) 593 apply (case_tac syscall; simp add: handle_send_def handle_call_def) 594 apply ((wp handle_invocation_pas_refined handle_recv_pas_refined 595 handle_fault_pas_refined 596 | simp | clarsimp)+) 597 apply (fastforce simp: valid_fault_def) 598 apply (wp handle_fault_pas_refined 599 | simp)+ 600 apply (fastforce simp: valid_fault_def) 601 apply (wp handle_interrupt_pas_refined handle_fault_pas_refined 602 hoare_vcg_conj_lift hoare_vcg_all_lift 603 | wpc 604 | rule hoare_drop_imps 605 | strengthen invs_vobjs_strgs 606 | simp)+ 607 apply auto 608 apply wpsimp+ 609 done 610 611lemma valid_fault_Unknown [simp]: 612 "valid_fault (UnknownSyscallException x)" 613 by (simp add: valid_fault_def) 614 615lemma valid_fault_User [simp]: 616 "valid_fault (UserException word1 word2)" 617 by (simp add: valid_fault_def) 618 619 620declare hy_inv[wp del] 621 622lemma handle_yield_integrity[wp]: 623 "\<lbrace>integrity aag X st and pas_refined aag and is_subject aag \<circ> cur_thread\<rbrace> 624 handle_yield 625 \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>" 626 by (simp add: handle_yield_def | wp)+ 627 628lemma ct_in_state_machine_state_update[simp]: "ct_in_state s (st\<lparr>machine_state := x\<rparr>) = ct_in_state s st" 629 apply (simp add: ct_in_state_def) 630 done 631 632crunch integrity[wp]: handle_yield "integrity aag X st" 633 634lemma handle_event_integrity: 635 "\<lbrace>integrity aag X st and pas_refined aag and guarded_pas_domain aag and domain_sep_inv (pasMaySendIrqs aag) st' 636 and einvs and schact_is_rct 637 and (\<lambda>s. ct_active s \<longrightarrow> is_subject aag (cur_thread s)) and (\<lambda>s. ev \<noteq> Interrupt \<longrightarrow> ct_active s) and ((=) st)\<rbrace> 638 handle_event ev 639 \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>" 640 apply (case_tac "ev \<noteq> Interrupt") 641 apply (case_tac ev; simp) 642 apply (rename_tac syscall) 643 apply (case_tac syscall, simp_all add: handle_send_def handle_call_def) 644 apply (wp handle_recv_integrity handle_invocation_respects 645 handle_reply_respects handle_fault_integrity_autarch 646 handle_interrupt_integrity handle_vm_fault_integrity 647 handle_reply_pas_refined handle_vm_fault_valid_fault 648 handle_reply_valid_sched 649 hoare_vcg_conj_lift hoare_vcg_all_lift alternative_wp select_wp 650 | rule dmo_wp 651 | wpc 652 | simp add: getActiveIRQ_def domain_sep_inv_def 653 | clarsimp 654 | rule conjI hoare_vcg_E_elim 655 | strengthen invs_vobjs_strgs invs_mdb_strgs 656 | fastforce)+ 657 done 658 659lemma integrity_restart_context: 660 "\<lbrakk> integrity aag X st s; pasMayActivate aag; 661 st_tcb_at ((=) Structures_A.Restart) thread s; \<not> is_subject aag thread \<rbrakk> 662 \<Longrightarrow> \<exists>tcb tcb'. get_tcb thread st = Some tcb \<and> 663 get_tcb thread s = Some tcb' \<and> 664 (arch_tcb_context_get (tcb_arch tcb') = arch_tcb_context_get (tcb_arch tcb) \<or> 665 arch_tcb_context_get (tcb_arch tcb') = 666 (arch_tcb_context_get (tcb_arch tcb))(TPIDRURW := (arch_tcb_context_get (tcb_arch tcb)) FaultInstruction))" 667 apply (clarsimp simp: integrity_def) 668 apply (drule_tac x = thread in spec) 669 apply (erule integrity_obj.cases, auto simp add: tcb_states_of_state_def get_tcb_def st_tcb_def2) 670 done 671 672definition 673 "consistent_tpidrurw_at \<equiv> 674 obj_at (\<lambda>ko. \<exists>tcb. ko = TCB tcb \<and> arch_tcb_context_get (tcb_arch tcb) TPIDRURW = tcb_ipc_buffer tcb)" 675 676lemma set_thread_state_restart_to_running_respects: 677 "\<lbrace>integrity aag X st and st_tcb_at ((=) Structures_A.Restart) thread 678 and K (pasMayActivate aag)\<rbrace> 679 do pc \<leftarrow> as_user thread getRestartPC; 680 as_user thread $ setNextPC pc; 681 set_thread_state thread Structures_A.thread_state.Running 682 od 683 \<lbrace>\<lambda>_. integrity aag X st\<rbrace>" 684 apply (simp add: set_thread_state_def set_object_def as_user_def split_def setNextPC_def 685 getRestartPC_def setRegister_def bind_assoc getRegister_def) 686 apply wp 687 apply (clarsimp simp: in_monad fun_upd_def[symmetric] cong: if_cong) 688 apply (cases "is_subject aag thread") 689 apply (cut_tac aag=aag in integrity_update_autarch, simp+) 690 apply (erule integrity_trans) 691 apply (clarsimp simp: integrity_def obj_at_def st_tcb_at_def) 692 apply (clarsimp dest!: get_tcb_SomeD) 693 apply (rule_tac ntfn'="tcb_bound_notification ya" in tro_tcb_activate [OF refl refl]) 694 apply (clarsimp simp: obj_at_def) 695 apply (simp add: tcb_bound_notification_reset_integrity_def)+ 696 done 697 698lemma activate_thread_respects: 699 "\<lbrace>integrity aag X st and K (pasMayActivate aag)\<rbrace> 700 activate_thread 701 \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>" 702 apply (simp add: activate_thread_def arch_activate_idle_thread_def) 703 apply (rule hoare_pre) 704 apply (wp set_thread_state_restart_to_running_respects thread_get_wp' 705 | wpc | simp add: arch_activate_idle_thread_def get_thread_state_def)+ 706 apply (clarsimp simp: st_tcb_at_def obj_at_def) 707 done 708 709lemma activate_thread_integrity: 710 "\<lbrace>integrity aag X st and (\<lambda>s. cur_thread s \<noteq> idle_thread s \<longrightarrow> is_subject aag (cur_thread s)) and valid_idle\<rbrace> 711 activate_thread 712 \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>" 713 apply (simp add: activate_thread_def arch_activate_idle_thread_def) 714 apply (rule hoare_pre) 715 apply (wp gts_wp set_thread_state_integrity_autarch as_user_integrity_autarch | wpc | simp add: arch_activate_idle_thread_def)+ 716 apply(clarsimp simp: valid_idle_def pred_tcb_at_def obj_at_def) 717 done 718 719lemma activate_thread_pas_refined: 720 "\<lbrace> pas_refined aag \<rbrace> 721 activate_thread 722 \<lbrace>\<lambda>rv. pas_refined aag \<rbrace>" 723 unfolding activate_thread_def arch_activate_idle_thread_def 724 get_thread_state_def thread_get_def 725 apply (rule hoare_pre) 726 apply (wp set_thread_state_pas_refined hoare_drop_imps 727 | wpc | simp)+ 728 done 729 730definition "current_ipc_buffer_register s \<equiv> arch_tcb_context_get (tcb_arch (the (get_tcb (cur_thread s) s))) TPIDRURW" 731 732lemma integrity_exclusive_state [iff]: 733 "integrity aag X st (s\<lparr>machine_state := machine_state s \<lparr>exclusive_state := es \<rparr>\<rparr>) 734 = integrity aag X st s" 735 unfolding integrity_def 736 by simp 737 738lemma dmo_clearExMonitor_respects_globals[wp]: 739 "\<lbrace>integrity aag X st\<rbrace> 740 do_machine_op clearExMonitor 741 \<lbrace>\<lambda>_. integrity aag X st\<rbrace>" 742 apply (rule hoare_pre) 743 apply (simp add: clearExMonitor_def | wp dmo_wp)+ 744 done 745 746lemma integrity_cur_thread [iff]: 747 "integrity aag X st (s\<lparr>cur_thread := v\<rparr>) = integrity aag X st s" 748 unfolding integrity_def by simp 749 750lemma current_ipc_buffer_register_cong[cong]: 751 "\<lbrakk>cur_thread s = cur_thread s'; kheap s = kheap s'\<rbrakk> 752 \<Longrightarrow> current_ipc_buffer_register s = current_ipc_buffer_register s'" 753 by (simp add:current_ipc_buffer_register_def get_tcb_def) 754 755 756crunch current_ipc_buffer_register [wp]: store_hw_asid "\<lambda>s. P (current_ipc_buffer_register s)" 757 (simp: crunch_simps current_ipc_buffer_register_def get_tcb_def) 758 759crunch current_ipc_buffer_register [wp]: invalidate_hw_asid_entry "\<lambda>s. P (current_ipc_buffer_register s)" 760 (simp: crunch_simps current_ipc_buffer_register_def get_tcb_def) 761 762crunch current_ipc_buffer_register [wp]: invalidate_asid "\<lambda>s. P (current_ipc_buffer_register s)" 763 (simp: crunch_simps current_ipc_buffer_register_def get_tcb_def) 764 765crunch current_ipc_buffer_register [wp]: do_machine_op "\<lambda>s. P (current_ipc_buffer_register s)" 766 (simp: crunch_simps current_ipc_buffer_register_def get_tcb_def) 767 768crunch current_ipc_buffer_register [wp]: find_free_hw_asid "\<lambda>s. P (current_ipc_buffer_register s)" 769 (simp: crunch_simps get_tcb_def ) 770 771crunch current_ipc_buffer_register [wp]: load_hw_asid "\<lambda>s. P (current_ipc_buffer_register s)" 772 (simp: crunch_simps current_ipc_buffer_register_def get_tcb_def) 773 774crunch current_ipc_buffer_register [wp]: get_hw_asid "\<lambda>s. P (current_ipc_buffer_register s)" 775 (simp: crunch_simps) 776 777crunch current_ipc_buffer_register [wp]: arm_context_switch "\<lambda>s. P (current_ipc_buffer_register s)" 778 (simp: crunch_simps) 779 780crunch current_ipc_buffer_register [wp]: set_vm_root "\<lambda>s. P (current_ipc_buffer_register s)" 781 (simp: crunch_simps) 782 783 784crunch current_ipc_buffer_register [wp]: next_domain "\<lambda>s. P (current_ipc_buffer_register s)" 785 (simp: crunch_simps) 786 787lemma tcb_sched_action_dequeue_integrity_pasMayEditReadyQueues: 788 "\<lbrace>integrity aag X st and pas_refined aag and K (pasMayEditReadyQueues aag)\<rbrace> 789 tcb_sched_action tcb_sched_dequeue thread 790 \<lbrace>\<lambda>_. integrity aag X st\<rbrace>" 791 apply (simp add: tcb_sched_action_def) 792 apply wp 793 apply (clarsimp simp: integrity_def integrity_ready_queues_def pas_refined_def tcb_domain_map_wellformed_aux_def etcb_at_def get_etcb_def 794 split: option.splits) 795 done 796 797lemma as_user_set_register_respects_indirect: 798 "\<lbrace>integrity aag X st and st_tcb_at ((=) Structures_A.Running) thread and 799 K ((\<not> is_subject aag thread \<longrightarrow> st_tcb_at receive_blocked thread st 800 \<and> bound_tcb_at ((=) (Some ntfnptr)) thread st) 801 \<and> (aag_has_auth_to aag Notify ntfnptr)) \<rbrace> 802 as_user thread (setRegister r v) 803 \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>" 804 apply (simp add: as_user_def split_def set_object_def) 805 apply wp 806 apply (clarsimp simp: in_monad setRegister_def) 807 apply (cases "is_subject aag thread") 808 apply (erule (1) integrity_update_autarch [unfolded fun_upd_def]) 809 apply (clarsimp simp: st_tcb_def2 receive_blocked_def) 810 apply (simp split: thread_state.split_asm) 811 apply (rule send_upd_ctxintegrity [OF disjI2, unfolded fun_upd_def], 812 auto simp: st_tcb_def2 indirect_send_def pred_tcb_def2) 813 done 814 815lemma switch_to_thread_respects_pasMayEditReadyQueues: 816 notes tcb_sched_action_dequeue_integrity[wp del] 817 shows 818 "\<lbrace>integrity aag X st and pas_refined aag 819 and K (pasMayEditReadyQueues aag)\<rbrace> 820 switch_to_thread t 821 \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>" 822 unfolding switch_to_thread_def arch_switch_to_thread_def 823 apply (simp add: spec_valid_def) 824 apply (wp tcb_sched_action_dequeue_integrity_pasMayEditReadyQueues 825 | simp add: clearExMonitor_def)+ 826 done 827 828lemma switch_to_thread_respects: 829 "\<lbrace>integrity aag X st and pas_refined aag 830 and K (is_subject aag t) \<rbrace> 831 switch_to_thread t 832 \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>" 833 unfolding switch_to_thread_def arch_switch_to_thread_def 834 apply (simp add: spec_valid_def) 835 apply (wp | simp add: clearExMonitor_def)+ 836 done 837 838text {* 839Variants of scheduling lemmas without is_subject assumption. 840See comment for @{thm tcb_sched_action_dequeue_integrity'} 841*} 842lemma switch_to_thread_respects': 843 "\<lbrace>integrity aag X st and pas_refined aag 844 and (\<lambda>s. pasSubject aag \<in> pasDomainAbs aag (tcb_domain (the (ekheap s t)))) \<rbrace> 845 switch_to_thread t 846 \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>" 847 unfolding switch_to_thread_def arch_switch_to_thread_def 848 apply (simp add: spec_valid_def) 849 apply (wp tcb_sched_action_dequeue_integrity' 850 | simp add: clearExMonitor_def)+ 851 done 852 853lemma switch_to_idle_thread_respects: 854 "\<lbrace>integrity aag X st\<rbrace> 855 switch_to_idle_thread 856 \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>" 857 unfolding switch_to_idle_thread_def arch_switch_to_idle_thread_def 858 by (wp | simp)+ 859 860lemma choose_thread_respects_pasMayEditReadyQueues: 861 "\<lbrace>integrity aag X st and pas_refined aag and einvs and valid_queues and K (pasMayEditReadyQueues aag ) \<rbrace> 862 choose_thread 863 \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>" 864 by (simp add: choose_thread_def guarded_switch_to_def 865 | wp switch_to_thread_respects_pasMayEditReadyQueues switch_to_idle_thread_respects gts_wp)+ 866 867text {* integrity for @{const choose_thread} without @{const pasMayEditReadyQueues} *} 868lemma choose_thread_respects: 869 "\<lbrace>integrity aag X st and pas_refined aag and pas_cur_domain aag and einvs and valid_queues\<rbrace> 870 choose_thread 871 \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>" 872 apply (simp add: choose_thread_def guarded_switch_to_def 873 | wp switch_to_thread_respects' switch_to_idle_thread_respects gts_wp)+ 874 apply (clarsimp simp: pas_refined_def) 875 apply (clarsimp simp: tcb_domain_map_wellformed_aux_def) 876 apply (clarsimp simp: valid_queues_def is_etcb_at_def) 877 apply (erule_tac x="cur_domain s" in allE) 878 apply (erule_tac x="Max {prio. ready_queues s (cur_domain s) prio \<noteq> []}" in allE) 879 apply clarsimp 880 apply (erule_tac x="hd (max_non_empty_queue (ready_queues s (cur_domain s)))" in ballE) 881 apply (clarsimp simp: etcb_at_def) 882 (* thread we're switching to is in cur_domain *) 883 apply (rule_tac s = "cur_domain s" in subst) 884 apply (clarsimp simp: max_non_empty_queue_def) 885 apply (frule tcb_at_ekheap_dom[OF st_tcb_at_tcb_at]) 886 apply (simp add: valid_sched_def) 887 apply (clarsimp simp: max_non_empty_queue_def) 888 apply (metis (mono_tags, lifting) setcomp_Max_has_prop hd_in_set) 889 (* pas_cur_domain *) 890 apply assumption 891 done 892 893lemma guarded_switch_to_respects: 894 "\<lbrace> integrity aag X st 895 and pas_refined aag and (\<lambda>s. is_subject aag x)\<rbrace> 896 guarded_switch_to x 897 \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>" 898 apply (simp add: guarded_switch_to_def) 899 apply (simp add: choose_thread_def guarded_switch_to_def 900 | wp switch_to_thread_respects switch_to_idle_thread_respects gts_wp)+ 901 done 902 903lemma next_domain_integrity [wp]: 904 "\<lbrace>integrity aag X st\<rbrace> 905 next_domain 906 \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>" 907 apply (simp add: next_domain_def thread_set_domain_def ethread_set_def set_eobject_def Let_def | wp)+ 908 apply (clarsimp simp: get_etcb_def integrity_subjects_def lfp_def) 909 done 910 911lemma next_domain_tcb_domain_map_wellformed [wp]: 912 "\<lbrace>tcb_domain_map_wellformed aag\<rbrace> 913 next_domain 914 \<lbrace>\<lambda>rv. tcb_domain_map_wellformed aag\<rbrace>" 915 by (simp add: next_domain_def thread_set_domain_def ethread_set_def set_eobject_def Let_def | wp)+ 916 917 918crunch domain_time[wp]: tcb_sched_action "\<lambda>s. P (domain_time s)" 919 920lemma valid_blocked_2_valid_blocked_except[simp]: 921 "valid_blocked_2 queues kh sa ct \<Longrightarrow> valid_blocked_except_2 t queues kh sa ct" 922 by (clarsimp simp: valid_blocked_def valid_blocked_except_def) 923 924(* clagged from Schedule_R *) 925lemma next_domain_valid_sched: 926 "\<lbrace> valid_sched and (\<lambda>s. scheduler_action s = choose_new_thread)\<rbrace> next_domain \<lbrace> \<lambda>_. valid_sched \<rbrace>" 927 apply (simp add: next_domain_def Let_def) 928 apply (wp, simp add: valid_sched_def valid_sched_action_2_def ct_not_in_q_2_def) 929 apply (simp add:valid_blocked_2_def) 930 done 931 932crunch current_ipc_buffer_register [wp]: tcb_sched_action "\<lambda>s. P (current_ipc_buffer_register s)" 933 (wp: crunch_wps without_preemption_wp simp: crunch_simps current_ipc_buffer_register_def get_tcb_def) 934 935text {* 936We need to use the domain of t instead of @{term "is_subject aag t"} 937because t's domain may contain multiple labels. See the comment for 938@{thm tcb_sched_action_dequeue_integrity'} 939*} 940lemma valid_sched_action_switch_subject_thread: 941 "\<lbrakk> scheduler_action s = switch_thread t ; valid_sched_action s ; 942 valid_etcbs s ; pas_refined aag s ; pas_cur_domain aag s \<rbrakk> 943 \<Longrightarrow> pasObjectAbs aag t \<in> pasDomainAbs aag (tcb_domain (the (ekheap s t))) \<and> 944 pasSubject aag \<in> pasDomainAbs aag (tcb_domain (the (ekheap s t)))" 945 apply (clarsimp simp: valid_sched_action_def weak_valid_sched_action_2_def 946 switch_in_cur_domain_2_def in_cur_domain_2_def valid_etcbs_def 947 etcb_at_def st_tcb_at_def obj_at_def is_etcb_at_def) 948 apply (rule conjI) 949 apply (force simp: pas_refined_def tcb_domain_map_wellformed_aux_def 950 intro: domtcbs) 951 apply force 952 done 953 954 955lemma schedule_choose_new_thread_integrity: 956 "\<lbrace> invs and valid_sched and valid_list and integrity aag X st and pas_refined aag 957 and K (pasMayEditReadyQueues aag) 958 and (\<lambda>s. scheduler_action s = choose_new_thread) \<rbrace> 959 schedule_choose_new_thread 960 \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>" 961 unfolding schedule_choose_new_thread_def 962 by (wpsimp wp: choose_thread_respects_pasMayEditReadyQueues 963 next_domain_valid_sched next_domain_valid_queues 964 simp: schedule_choose_new_thread_def valid_sched_def) 965 966lemma schedule_integrity: 967 "\<lbrace>einvs and integrity aag X st and pas_refined aag and pas_cur_domain aag 968 and (\<lambda>s. domain_time s \<noteq> 0) \<rbrace> 969 schedule 970 \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>" 971 apply (simp add: schedule_def) 972 apply (rule hoare_pre) 973 supply ethread_get_wp[wp del] 974 apply (wp|wpc|simp only: schedule_choose_new_thread_def)+ 975 apply (wpsimp wp: alternative_wp switch_to_thread_respects' select_wp switch_to_idle_thread_respects 976 guarded_switch_to_lift choose_thread_respects gts_wp hoare_drop_imps 977 set_scheduler_action_cnt_valid_sched append_thread_queued enqueue_thread_queued 978 tcb_sched_action_enqueue_valid_blocked_except 979 tcb_sched_action_append_integrity' 980 wp_del: ethread_get_wp 981 | wpc 982 | simp add: allActiveTCBs_def schedule_choose_new_thread_def 983 | rule hoare_pre_cont[where a=next_domain])+ 984 apply (auto simp: obj_at_def st_tcb_at_def not_cur_thread_2_def valid_sched_def 985 valid_sched_action_def weak_valid_sched_action_def 986 valid_sched_action_switch_subject_thread schedule_choose_new_thread_def) 987 done 988 989lemma valid_sched_valid_sched_action: 990 "valid_sched s \<Longrightarrow> valid_sched_action s" 991 by (simp add: valid_sched_def) 992 993lemma schedule_integrity_pasMayEditReadyQueues: 994 "\<lbrace>einvs and integrity aag X st and pas_refined aag and guarded_pas_domain aag 995 and K (pasMayEditReadyQueues aag) \<rbrace> 996 schedule 997 \<lbrace>\<lambda>rv. integrity aag X st\<rbrace>" 998 supply ethread_get_wp[wp del] 999 supply schedule_choose_new_thread_integrity[wp] 1000 supply if_split[split del] 1001 apply (simp add: schedule_def wrap_is_highest_prio_def[symmetric]) 1002 apply (wp, wpc) 1003 (* resume current thread *) 1004 apply wp 1005 prefer 2 1006 (* choose thread *) 1007 apply wp 1008 (* switch_to *) 1009 apply (wpsimp wp: set_scheduler_action_cnt_valid_sched enqueue_thread_queued append_thread_queued 1010 tcb_sched_action_append_integrity_pasMayEditReadyQueues 1011 guarded_switch_to_lift switch_to_thread_respects_pasMayEditReadyQueues)+ 1012 (* is_highest_prio *) 1013 apply (simp add: wrap_is_highest_prio_def) 1014 apply ((wp_once hoare_drop_imp)+)[1] 1015 apply (wpsimp wp: tcb_sched_action_enqueue_valid_blocked_except hoare_vcg_imp_lift' gts_wp)+ 1016 apply (clarsimp simp: if_apply_def2 cong: imp_cong conj_cong) 1017 1018 apply (safe ; ((solves \<open>clarsimp simp: valid_sched_def not_cur_thread_def valid_sched_action_def 1019 weak_valid_sched_action_def\<close> 1020 )?)) 1021 apply (clarsimp simp: obj_at_def pred_tcb_at_def)+ 1022 done 1023 1024lemma pas_refined_cur_thread [iff]: 1025 "pas_refined aag (s\<lparr>cur_thread := v\<rparr>) = pas_refined aag s" 1026 unfolding pas_refined_def 1027 by (simp add: state_objs_to_policy_def) 1028 1029lemma switch_to_thread_pas_refined: 1030 "\<lbrace>pas_refined aag\<rbrace> 1031 switch_to_thread t 1032 \<lbrace>\<lambda>rv. pas_refined aag\<rbrace>" 1033 unfolding switch_to_thread_def arch_switch_to_thread_def 1034 by (wp do_machine_op_pas_refined | simp)+ 1035 1036lemma switch_to_idle_thread_pas_refined: 1037 "\<lbrace>pas_refined aag\<rbrace> 1038 switch_to_idle_thread 1039 \<lbrace>\<lambda>rv. pas_refined aag\<rbrace>" 1040 unfolding switch_to_idle_thread_def arch_switch_to_idle_thread_def 1041 by (wp do_machine_op_pas_refined | simp)+ 1042 1043crunch pas_refined[wp]: choose_thread "pas_refined aag" (wp: switch_to_thread_pas_refined switch_to_idle_thread_pas_refined crunch_wps) 1044 1045lemma schedule_pas_refined: 1046 "\<lbrace>pas_refined aag\<rbrace> 1047 schedule 1048 \<lbrace>\<lambda>rv. pas_refined aag\<rbrace>" 1049 apply (simp add: schedule_def allActiveTCBs_def) 1050 apply (wp add: alternative_wp guarded_switch_to_lift switch_to_thread_pas_refined select_wp 1051 switch_to_idle_thread_pas_refined gts_wp 1052 guarded_switch_to_lift switch_to_thread_respects_pasMayEditReadyQueues 1053 choose_thread_respects_pasMayEditReadyQueues 1054 next_domain_valid_sched next_domain_valid_queues gts_wp hoare_drop_imps 1055 set_scheduler_action_cnt_valid_sched enqueue_thread_queued 1056 tcb_sched_action_enqueue_valid_blocked_except 1057 del: ethread_get_wp 1058 | wpc | simp add: schedule_choose_new_thread_def)+ 1059 done 1060 1061lemma handle_interrupt_arch_state [wp]: 1062 "\<lbrace>\<lambda>s :: det_ext state. P (arch_state s)\<rbrace> handle_interrupt irq \<lbrace>\<lambda>_ s. P (arch_state s)\<rbrace>" 1063 unfolding handle_interrupt_def 1064 apply (rule hoare_if) 1065 apply (rule hoare_pre) 1066 apply clarsimp 1067 apply (wp get_cap_inv dxo_wp_weak send_signal_arch_state 1068 | wpc 1069 | simp add: get_irq_state_def handle_reserved_irq_def)+ 1070 done 1071 1072lemmas sequence_x_mapM_x = mapM_x_def [symmetric] 1073 1074crunch arch_state [wp]: invoke_untyped "\<lambda>s. P (arch_state s)" 1075 (wp: crunch_wps without_preemption_wp syscall_valid do_machine_op_arch hoare_unless_wp 1076 preemption_point_inv mapME_x_inv_wp 1077 simp: crunch_simps sequence_x_mapM_x 1078 ignore: do_machine_op freeMemory clearMemory) 1079 1080lemma set_cap_current_ipc_buffer_register[wp]: 1081 "\<lbrace>\<lambda>s. P (current_ipc_buffer_register s)\<rbrace> set_cap ptr c \<lbrace>\<lambda>r s. P (current_ipc_buffer_register s)\<rbrace>" 1082 apply (cases c) 1083 apply (clarsimp simp: set_cap_def get_object_def set_object_def valid_def put_def 1084 gets_def assert_def bind_def get_def return_def fail_def 1085 split: option.splits kernel_object.splits) 1086 apply (auto simp: current_ipc_buffer_register_def get_tcb_def) 1087 done 1088 1089crunch current_ipc_buffer_register [wp]: "set_thread_state_ext" "\<lambda>s. P (current_ipc_buffer_register s)" 1090 1091lemma set_thread_state_current_ipc_buffer_register[wp]: 1092 "\<lbrace>\<lambda>s. P (current_ipc_buffer_register s)\<rbrace> set_thread_state t b \<lbrace>\<lambda>r s. P (current_ipc_buffer_register s)\<rbrace>" 1093 apply (clarsimp simp: set_thread_state_def) 1094 apply (wp dxo_wp_weak) 1095 apply (simp add: trans_state_def) 1096 apply (clarsimp simp: set_thread_state_def get_object_def set_object_def valid_def put_def 1097 gets_def assert_def bind_def get_def return_def fail_def 1098 split: option.splits kernel_object.splits) 1099 apply simp 1100 apply wp 1101 apply (auto simp: current_ipc_buffer_register_def get_tcb_def) 1102 done 1103 1104lemma set_simple_ko_current_ipc_buffer_register[wp]: 1105 "\<lbrace>\<lambda>s. P (current_ipc_buffer_register s)\<rbrace> set_simple_ko f t ep \<lbrace>\<lambda>r s. P (current_ipc_buffer_register s)\<rbrace>" 1106 apply (clarsimp simp: set_simple_ko_def ) 1107 apply (wp dxo_wp_weak | wpc)+ 1108 apply (clarsimp simp: set_thread_state_def get_object_def set_object_def valid_def put_def 1109 gets_def assert_def bind_def get_def return_def fail_def gets_the_def 1110 assert_opt_def 1111 split: option.splits kernel_object.splits) 1112 apply simp 1113 apply (wp get_object_wp | simp add: get_simple_ko_def | wpc)+ 1114 apply (auto simp: a_type_def partial_inv_def obj_at_def current_ipc_buffer_register_def get_tcb_def 1115 split: kernel_object.split_asm) 1116 done 1117 1118crunch current_ipc_buffer_register [wp]: "set_cap" "\<lambda>s. P (current_ipc_buffer_register s)" 1119 1120lemma update_tcb_current_ipc_buffer_register: 1121 "\<lbrakk>get_tcb t s = Some tcb; P (current_ipc_buffer_register s); 1122 arch_tcb_context_get (tcb_arch tcb) TPIDRURW = arch_tcb_context_get (tcb_arch tcb') TPIDRURW\<rbrakk> 1123 \<Longrightarrow> P (current_ipc_buffer_register (s\<lparr>kheap := kheap s(t \<mapsto> TCB tcb')\<rparr>))" 1124 apply (erule arg_cong[where f = P,THEN iffD1,rotated]) 1125 apply (simp add: current_ipc_buffer_register_def get_tcb_def) 1126 done 1127 1128lemma unbind_maybe_notification_current_ipc_buffer_register[wp]: 1129 "\<lbrace>\<lambda>s. P (current_ipc_buffer_register s)\<rbrace> unbind_maybe_notification t \<lbrace>\<lambda>r s. P (current_ipc_buffer_register s)\<rbrace>" 1130 apply (clarsimp simp: unbind_maybe_notification_def ) 1131 apply (wp dxo_wp_weak | wpc)+ 1132 apply (simp add: trans_state_def set_bound_notification_def) 1133 apply (clarsimp simp: set_thread_state_def get_object_def set_object_def valid_def put_def 1134 gets_def assert_def bind_def get_def return_def fail_def gets_the_def 1135 assert_opt_def 1136 split: option.splits kernel_object.splits) 1137 apply (erule update_tcb_current_ipc_buffer_register) 1138 apply assumption 1139 apply simp 1140 apply (wp get_object_wp | simp add: get_simple_ko_def | wpc)+ 1141 done 1142 1143lemma set_bounded_notification_current_ipc_buffer_register[wp]: 1144 "\<lbrace>\<lambda>s. P (current_ipc_buffer_register s)\<rbrace> set_bound_notification t ep \<lbrace>\<lambda>r s. P (current_ipc_buffer_register s)\<rbrace>" 1145 apply (clarsimp simp: set_bound_notification_def ) 1146 apply (wp dxo_wp_weak | wpc)+ 1147 apply (clarsimp simp: set_thread_state_def get_object_def set_object_def valid_def put_def 1148 gets_def assert_def bind_def get_def return_def fail_def gets_the_def 1149 assert_opt_def 1150 split: option.splits kernel_object.splits) 1151 apply simp 1152 apply (wp get_object_wp | simp add: get_simple_ko_def | wpc)+ 1153 apply (auto simp: obj_at_def current_ipc_buffer_register_def get_tcb_def split: kernel_object.split_asm) 1154 done 1155 1156lemma set_pd_current_ipc_buffer_register[wp]: 1157 "\<lbrace>\<lambda>s. P (current_ipc_buffer_register s)\<rbrace> set_pd ptr pd \<lbrace>\<lambda>r s. P (current_ipc_buffer_register s)\<rbrace>" 1158 apply (clarsimp simp: set_pd_def ) 1159 apply (wp | wpc)+ 1160 apply (clarsimp simp: set_thread_state_def get_object_def set_object_def valid_def put_def 1161 gets_def assert_def bind_def get_def return_def fail_def gets_the_def 1162 assert_opt_def 1163 split: option.splits kernel_object.splits) 1164 apply simp 1165 apply (wp get_object_wp | simp add: get_simple_ko_def | wpc)+ 1166 apply (auto simp: obj_at_def current_ipc_buffer_register_def get_tcb_def split: kernel_object.split_asm) 1167 done 1168 1169lemma set_pt_current_ipc_buffer_register[wp]: 1170 "\<lbrace>\<lambda>s. P (current_ipc_buffer_register s)\<rbrace> set_pt ptr pt \<lbrace>\<lambda>r s. P (current_ipc_buffer_register s)\<rbrace>" 1171 apply (clarsimp simp: set_pt_def ) 1172 apply (wp | wpc)+ 1173 apply (clarsimp simp: set_thread_state_def get_object_def set_object_def valid_def put_def 1174 gets_def assert_def bind_def get_def return_def fail_def gets_the_def 1175 assert_opt_def 1176 split: option.splits kernel_object.splits) 1177 apply simp 1178 apply (wp get_object_wp | simp add: get_simple_ko_def | wpc)+ 1179 apply (auto simp: obj_at_def current_ipc_buffer_register_def get_tcb_def split: kernel_object.split_asm) 1180 done 1181 1182crunch current_ipc_buffer_register [wp]: post_cap_deletion, cap_delete_one "\<lambda>s. P (current_ipc_buffer_register s)" 1183 (wp: crunch_wps without_preemption_wp syscall_valid do_machine_op_arch 1184 hoare_unless_wp dxo_wp_weak 1185 simp: crunch_simps mapM_x_wp 1186 ignore: do_machine_op clearMemory empty_slot_ext tcb_sched_action reschedule_required) 1187 1188lemma dxo_current_ipc_buffer_register[wp]: 1189 "\<lbrace>\<lambda>s. P (current_ipc_buffer_register s)\<rbrace> do_extended_op eop \<lbrace>\<lambda>r s. P (current_ipc_buffer_register s)\<rbrace>" 1190 by (simp | wp dxo_wp_weak)+ 1191 1192lemma dxo_current_ipc_buffer_register_kheap_upd: 1193 "\<lbrace>\<lambda>s. P (current_ipc_buffer_register (s\<lparr>kheap:=kh\<rparr>))\<rbrace> do_extended_op eop \<lbrace>\<lambda>r s. P (current_ipc_buffer_register (s\<lparr>kheap:=kh\<rparr>))\<rbrace>" 1194 including no_pre 1195 apply (simp | wp dxo_wp_weak)+ 1196 apply (rule arg_cong[where f = P]) 1197 apply (simp add: trans_state_def current_ipc_buffer_register_def get_tcb_def) 1198 done 1199 1200crunch current_ipc_buffer_register [wp]: "deleting_irq_handler" "\<lambda>s. P (current_ipc_buffer_register s)" 1201 (wp: crunch_wps mapM_x_wp) 1202 1203(* FIXME: Crunch fails for the following simple valid rules *) 1204lemma cap_swap_current_ipc_buffer_register[wp]: 1205 "\<lbrace>\<lambda>s. P (current_ipc_buffer_register s)\<rbrace> cap_swap a b c d \<lbrace>\<lambda>r s. P (current_ipc_buffer_register s)\<rbrace>" 1206 by (simp add: cap_swap_def | wp)+ 1207 1208crunch current_ipc_buffer_register [wp]: "cap_swap_for_delete" "\<lambda>s. P (current_ipc_buffer_register s)" 1209 (wp: dxo_wp_weak dxo_current_ipc_buffer_register) 1210 1211crunch current_ipc_buffer_register [wp]: "set_bound_notification" "\<lambda>s. P (current_ipc_buffer_register s)" 1212 1213(* FIXME: Crunch fails for the following simple valid rules *) 1214lemma create_cap_current_ipc_buffer_register[wp]: 1215 "\<lbrace>\<lambda>s. P (current_ipc_buffer_register s)\<rbrace> create_cap a b c d e \<lbrace>\<lambda>r s. P (current_ipc_buffer_register s)\<rbrace>" 1216 apply (rule hoare_pre) 1217 by (simp add: create_cap_def | wp | wpc)+ 1218 1219crunch current_ipc_buffer_register [wp]: store_pde "\<lambda>s. P (current_ipc_buffer_register s)" 1220 (wp: crunch_wps) 1221 1222crunch current_ipc_buffer_register [wp]: init_arch_objects "\<lambda>s. P (current_ipc_buffer_register s)" 1223 (wp: crunch_wps without_preemption_wp hoare_unless_wp 1224 simp: crunch_simps 1225 ignore: do_machine_op clearMemory freeMemory) 1226 1227lemma current_ipc_buffer_register_weak_intro: 1228 assumes valid: "\<And>P. \<lbrace>\<lambda>s. obj_at P (cur_thread s) s \<and> Q s\<rbrace> f \<lbrace>\<lambda>_ s. obj_at P (cur_thread s) s\<rbrace>" 1229 shows "\<lbrace>\<lambda>s. P (current_ipc_buffer_register s) \<and> cur_tcb s \<and> Q s \<rbrace> f \<lbrace>\<lambda>r s. P (current_ipc_buffer_register s)\<rbrace>" 1230 apply (clarsimp simp: valid_def current_ipc_buffer_register_def) 1231 apply (drule use_valid) 1232 apply (rule_tac P = "\<lambda>ko. case ko of TCB t \<Rightarrow> P (arch_tcb_context_get (tcb_arch t) TPIDRURW) | _ \<Rightarrow> False" in valid) 1233 apply (clarsimp simp: cur_tcb_def tcb_at_def) 1234 apply (clarsimp simp: obj_at_def) 1235 apply (clarsimp split: kernel_object.split_asm) 1236 apply (clarsimp simp: get_tcb_def) 1237 done 1238 1239 1240(* FIXME: Crunch fails for the following simple valid rules *) 1241lemma retype_region_current_ipc_buffer_register: 1242 "\<lbrace>\<lambda>s. P (current_ipc_buffer_register s) \<and> pspace_no_overlap (up_aligned_area ptr sz) s 1243 \<and> valid_pspace s \<and> cur_tcb s \<and> range_cover ptr sz (obj_bits_api ty us) n\<rbrace> 1244 retype_region ptr n us ty dev \<lbrace>\<lambda>r s. P (current_ipc_buffer_register s)\<rbrace>" 1245 apply (rule hoare_pre) 1246 apply (wp current_ipc_buffer_register_weak_intro) 1247 apply (rule hoare_pre) 1248 apply wps 1249 apply (wp Retype_AI.retype_region_obj_at_other2) 1250 apply (erule conjE, erule conjI, assumption) 1251 apply clarsimp 1252 apply (drule(2) pspace_no_overlap_into_Int_none) 1253 apply (fastforce simp: cur_tcb_def obj_at_def) 1254 done 1255 1256lemma cancel_signal_current_ipc_buffer_register[wp]: 1257 "\<lbrace>\<lambda>s. P (current_ipc_buffer_register s)\<rbrace> cancel_signal a b \<lbrace>\<lambda>r s. P (current_ipc_buffer_register s)\<rbrace>" 1258 including no_pre 1259 apply (clarsimp simp: cancel_signal_def get_simple_ko_def) 1260 apply (wp | wpc)+ 1261 apply (clarsimp simp: get_object_def set_object_def valid_def put_def 1262 gets_def assert_def bind_def get_def return_def fail_def gets_the_def 1263 assert_opt_def 1264 split: option.splits kernel_object.splits) 1265 done 1266 1267crunch current_ipc_buffer_register [wp]: blocked_cancel_ipc "\<lambda>s. P (current_ipc_buffer_register s)" 1268 (wp: crunch_wps) 1269 1270lemma reply_cancel_ipc_current_ipc_buffer_register[wp]: 1271 "\<lbrace>\<lambda>s. P (current_ipc_buffer_register s)\<rbrace> reply_cancel_ipc a \<lbrace>\<lambda>r s. P (current_ipc_buffer_register s)\<rbrace>" 1272 including no_pre 1273 apply (clarsimp simp: reply_cancel_ipc_def) 1274 apply (wp select_wp| wpc)+ 1275 apply (rule_tac Q = "\<lambda>r s. P (current_ipc_buffer_register s)" in hoare_post_imp) 1276 apply simp 1277 apply (clarsimp simp: get_object_def set_object_def valid_def put_def 1278 gets_def assert_def bind_def get_def return_def 1279 fail_def gets_the_def 1280 thread_set_def assert_opt_def get_tcb_def 1281 split: option.splits kernel_object.splits) 1282 apply (clarsimp simp: current_ipc_buffer_register_def get_tcb_def) 1283 done 1284 1285lemma set_asid_pool_current_ipc_buffer_register[wp]: 1286 "\<lbrace>\<lambda>s. P (current_ipc_buffer_register s)\<rbrace> set_asid_pool a b \<lbrace>\<lambda>r s. P (current_ipc_buffer_register s)\<rbrace>" 1287 apply (clarsimp simp: set_asid_pool_def) 1288 apply (rule_tac Q = "\<lambda>r s. P (current_ipc_buffer_register s)" in hoare_post_imp) 1289 apply simp 1290 apply (clarsimp simp: get_object_def set_object_def valid_def put_def 1291 gets_def assert_def bind_def get_def return_def 1292 fail_def gets_the_def 1293 thread_set_def assert_opt_def get_tcb_def 1294 split: option.splits kernel_object.splits) 1295 apply (clarsimp simp: current_ipc_buffer_register_def get_tcb_def) 1296 done 1297 1298crunch current_ipc_buffer_register [wp]: finalise_cap "\<lambda>s. P (current_ipc_buffer_register s)" 1299 (wp: crunch_wps without_preemption_wp syscall_valid do_machine_op_arch 1300 hoare_unless_wp select_wp 1301 simp: crunch_simps 1302 ignore: do_machine_op clearMemory empty_slot_ext reschedule_required 1303 tcb_sched_action) 1304 1305 1306lemma rec_del_current_ipc_buffer_register [wp]: 1307 "invariant (rec_del call) (\<lambda>s. P (current_ipc_buffer_register s))" 1308 by (rule rec_del_preservation; wpsimp wp: preemption_point_inv) 1309 1310crunch current_ipc_buffer_register [wp]: cap_delete "\<lambda>s. P (current_ipc_buffer_register s)" 1311 (wp: crunch_wps simp: crunch_simps) 1312 1313lemma cap_revoke_current_ipc_buffer_register [wp]: 1314 "invariant (cap_revoke slot) (\<lambda>s. P (current_ipc_buffer_register s))" 1315 apply (rule validE_valid) 1316 apply (rule cap_revoke_preservation; wpsimp wp: preemption_point_inv) 1317 done 1318 1319end 1320 1321crunch_ignore (add: 1322 cap_swap_ext cap_move_ext cap_insert_ext empty_slot_ext create_cap_ext tcb_sched_action ethread_set 1323 reschedule_required set_thread_state_ext possible_switch_to next_domain 1324 set_domain 1325 timer_tick set_priority retype_region_ext) 1326 1327context begin interpretation Arch . (*FIXME: arch_split*) 1328 1329crunch current_ipc_buffer_register [wp]: cap_insert "\<lambda>s. P (current_ipc_buffer_register s)" 1330 (wp: crunch_wps simp: crunch_simps) 1331 1332crunch current_ipc_buffer_register [wp]: cap_move "\<lambda>s. P (current_ipc_buffer_register s)" 1333 (wp: crunch_wps simp: crunch_simps) 1334 1335crunch current_ipc_buffer_register [wp]: set_extra_badge "\<lambda>s. P (current_ipc_buffer_register s)" 1336 (wp: crunch_wps simp: crunch_simps) 1337 1338lemma transfer_caps_loop_current_ipc_buffer_register: 1339 "\<lbrace>\<lambda>s. P (current_ipc_buffer_register s)\<rbrace> transfer_caps_loop ep buffer n caps slots mi \<lbrace>\<lambda>r s. P (current_ipc_buffer_register s)\<rbrace>" 1340 by (wp transfer_caps_loop_pres) 1341 1342crunch current_ipc_buffer_register [wp]: transfer_caps "\<lambda>s. P (current_ipc_buffer_register s)" 1343 1344lemma set_tcb_context_current_ipc_buffer_register: 1345 "\<lbrace>\<lambda>s. (f = cur_thread s \<longrightarrow> (P (cxt TPIDRURW) = P (arch_tcb_context_get (tcb_arch tcb) TPIDRURW) \<and> 1346 obj_at (\<lambda>obj. obj = TCB tcb) f s)) \<and> P (current_ipc_buffer_register s)\<rbrace> 1347 set_object f (TCB (tcb\<lparr>tcb_arch := arch_tcb_context_set cxt (tcb_arch tcb)\<rparr>)) 1348 \<lbrace>\<lambda>_ s. P (current_ipc_buffer_register s)\<rbrace>" 1349 by (auto simp: current_ipc_buffer_register_def get_tcb_def set_object_def get_def put_def bind_def valid_def return_def obj_at_def) 1350 1351lemma as_user_current_ipc_buffer_register[wp]: 1352 assumes uc: "\<And>P. \<lbrace>\<lambda>s. P (s TPIDRURW)\<rbrace> a \<lbrace>\<lambda>r s. P (s TPIDRURW)\<rbrace>" 1353 shows "\<lbrace>\<lambda>s. P (current_ipc_buffer_register s)\<rbrace> as_user f a 1354 \<lbrace>\<lambda>_ s. P (current_ipc_buffer_register s)\<rbrace>" 1355 apply (simp add: as_user_def) 1356 apply (wp select_f_wp set_tcb_context_current_ipc_buffer_register | wpc | simp)+ 1357 apply (clarsimp dest!: get_tcb_SomeD) 1358 apply (simp add: obj_at_def get_tcb_def) 1359 apply (drule use_valid[OF _ uc]) 1360 apply (clarsimp simp: current_ipc_buffer_register_def get_tcb_def) 1361 apply assumption 1362 apply (clarsimp simp: current_ipc_buffer_register_def get_tcb_def) 1363 done 1364 1365lemma set_register_tpidrurw_inv[wp]: 1366 "r \<noteq> TPIDRURW \<Longrightarrow> \<lbrace>\<lambda>s. P (s TPIDRURW)\<rbrace> setRegister r v\<lbrace>\<lambda>r s. P (s TPIDRURW)\<rbrace>" 1367 by (simp add: setRegister_def simpler_modify_def valid_def) 1368 1369crunch tpidrurw_inv [wp]: getRegister "\<lambda>s. P (s TPIDRURW)" 1370 1371crunch current_ipc_buffer_register [wp]: handle_interrupt "\<lambda>s. P (current_ipc_buffer_register s)" 1372 (wp: crunch_wps simp: badge_register_def badgeRegister_def ) 1373 1374lemma TPIDRURW_notin_msg_registers[simp]: 1375 "TPIDRURW \<notin> set (take r msgRegisters)" 1376 "TPIDRURW \<notin> set syscallMessage" 1377 "TPIDRURW \<notin> set exceptionMessage" 1378 "TPIDRURW \<notin> set gpRegisters" 1379 "TPIDRURW \<notin> set frameRegisters" 1380 apply (auto simp: msgRegisters_def frameRegisters_def gpRegisters_def 1381 syscallMessage_def exceptionMessage_def) 1382 apply (rule ccontr) 1383 apply clarsimp 1384 apply (drule in_set_takeD) 1385 apply (simp_all add: upto_enum_red image_def) 1386 apply (auto simp add: toEnum_eq_to_fromEnum_eq fromEnum_def enum_register maxBound_def 1387 dest!: toEnum_eq_to_fromEnum_eq[THEN iffD1,rotated,OF sym]) 1388 done 1389 1390lemma zet_zip_contrapos: 1391 "fst t \<notin> set xs \<Longrightarrow> t \<notin> set (zip xs ys)" 1392 apply (rule ccontr) 1393 apply (simp add: set_zip_helper) 1394 done 1395 1396lemma set_mrs_current_ipc_buffer_register: 1397 "\<lbrace>(\<lambda>s. P (current_ipc_buffer_register s))\<rbrace> set_mrs a b c \<lbrace>\<lambda>_ s. P (current_ipc_buffer_register s)\<rbrace>" 1398 apply (simp add: set_mrs_def msg_registers_def) 1399 apply (subst zipWithM_x_mapM_x) 1400 apply (rule hoare_pre) 1401 apply (wp mapM_x_wp[where S = UNIV] | wpc | simp)+ 1402 apply (rule hoare_pre) 1403 apply (wp set_object_wp | wpc | simp)+ 1404 apply (auto simp: current_ipc_buffer_register_def arch_tcb_set_registers_def 1405 arch_tcb_get_registers_def get_tcb_def) 1406 done 1407 1408lemma thread_set_current_ipc_buffer_register: 1409 assumes tpidrurw_inv: "\<And>y. P (arch_tcb_context_get (tcb_arch (r y)) TPIDRURW) = P (arch_tcb_context_get (tcb_arch y) TPIDRURW)" 1410 shows "\<lbrace>(\<lambda>s. P (current_ipc_buffer_register s))\<rbrace> thread_set r ptr \<lbrace>\<lambda>_ s. P (current_ipc_buffer_register s)\<rbrace>" 1411 apply (simp add:thread_set_def) 1412 apply (wp set_object_wp) 1413 apply (auto simp: current_ipc_buffer_register_def get_tcb_def tpidrurw_inv) 1414 done 1415 1416lemma checked_cap_current_ipc_buffer_register_inv: 1417 "\<lbrace>(\<lambda>s. P (current_ipc_buffer_register s))\<rbrace> 1418 check_cap_at a b (check_cap_at c d (cap_insert a b e)) 1419 \<lbrace>\<lambda>_ s. P (current_ipc_buffer_register s)\<rbrace>" 1420 by (simp add:check_cap_at_def | wp hoare_vcg_if_lift2 hoare_drop_imps)+ 1421 1422lemma [simp]: 1423 "badge_register \<noteq> TPIDRURW" "msg_info_register \<noteq> TPIDRURW" 1424 by (auto simp add:badgeRegister_def badge_register_def msg_info_register_def msgInfoRegister_def) 1425 1426crunch current_ipc_buffer_register [wp]: setup_caller_cap "\<lambda>s. P (current_ipc_buffer_register s)" 1427 (wp: crunch_wps simp: crunch_simps ) 1428 1429crunch current_ipc_buffer_register [wp]: set_message_info "\<lambda>s. P (current_ipc_buffer_register s)" 1430 (wp: crunch_wps simp: crunch_simps ) 1431 1432crunch current_ipc_buffer_register [wp]: do_ipc_transfer "\<lambda>s. P (current_ipc_buffer_register s)" 1433 (wp: crunch_wps simp: crunch_simps msg_registers_def) 1434 1435crunch current_ipc_buffer_register [wp]: send_ipc "\<lambda>s. P (current_ipc_buffer_register s)" 1436 (wp: crunch_wps simp: crunch_simps ) 1437 1438crunch current_ipc_buffer_register [wp]: send_fault_ipc "\<lambda>s. P (current_ipc_buffer_register s)" 1439 (wp: crunch_wps thread_set_current_ipc_buffer_register simp: crunch_simps ignore: thread_set ) 1440 1441crunch current_ipc_buffer_register [wp]: handle_fault "\<lambda>s. P (current_ipc_buffer_register s)" 1442 (wp: crunch_wps simp: crunch_simps ) 1443 1444crunch current_ipc_buffer_register [wp]: reply_from_kernel "\<lambda>s. P (current_ipc_buffer_register s)" 1445 (wp: crunch_wps simp: crunch_simps ) 1446 1447crunch current_ipc_buffer_register [wp]: do_reply_transfer "\<lambda>s. P (current_ipc_buffer_register s)" 1448 ( wp: crunch_wps thread_set_current_ipc_buffer_register simp: crunch_simps zet_zip_contrapos 1449 ignore: do_extended_op thread_set 1450 tcb_fault_update) 1451 1452crunch current_ipc_buffer_register [wp]: invoke_domain "\<lambda>s. P (current_ipc_buffer_register s)" 1453 ( wp: crunch_wps simp: crunch_simps ignore: do_extended_op check_cap_at) 1454 1455crunch current_ipc_buffer_register [wp]: cancel_badged_sends "\<lambda>s. P (current_ipc_buffer_register s)" 1456 ( wp: crunch_wps filterM_preserved simp: crunch_simps ignore: do_extended_op) 1457 1458crunch current_ipc_buffer_register [wp]: finalise_slot "\<lambda>s. P (current_ipc_buffer_register s)" 1459 ( wp: crunch_wps filterM_preserved hoare_unless_wp simp: crunch_simps ignore: do_extended_op) 1460 1461lemma ct_active_update[simp]: 1462 "ct_active (s\<lparr>cdt := b\<rparr>) = ct_active s" 1463 "ct_active (s\<lparr>is_original_cap := ic\<rparr>) = ct_active s" 1464 "ct_active (s\<lparr>interrupt_states := st\<rparr>) = ct_active s" 1465 "ct_active (s\<lparr>arch_state := as\<rparr>) = ct_active s" 1466 by (auto simp: st_tcb_at_def ct_in_state_def) 1467 1468lemma set_cap_ct_active[wp]: 1469 "\<lbrace>ct_active\<rbrace> 1470 set_cap ptr c 1471 \<lbrace>\<lambda>_. ct_active \<rbrace>" 1472 apply (rule hoare_pre) 1473 apply (wp select_wp sts_st_tcb_at_cases thread_set_no_change_tcb_state 1474 | simp add: crunch_simps ct_in_state_def | wps)+ 1475 done 1476 1477lemma do_extended_op_ct_active[wp]: 1478 "\<lbrace>ct_active\<rbrace> 1479 do_extended_op ch 1480 \<lbrace>\<lambda>_. ct_active \<rbrace>" 1481 apply (rule hoare_pre) 1482 apply (wp | simp add: crunch_simps ct_in_state_def do_extended_op_def | wps)+ 1483 apply (auto simp: st_tcb_at_def obj_at_def) 1484 done 1485 1486crunch ct_active [wp]: set_original "ct_active" 1487 ( wp: crunch_wps 1488 simp: crunch_simps ct_in_state_def) 1489 1490crunch ct_active [wp]: set_cdt "ct_active" 1491 ( wp: crunch_wps 1492 simp: crunch_simps ct_in_state_def) 1493 1494lemma cap_swap_ct_active[wp]: 1495 "\<lbrace>ct_active\<rbrace> 1496 cap_swap a b c d 1497 \<lbrace>\<lambda>_. ct_active \<rbrace>" 1498 by (wp | simp add: cap_swap_def | wps)+ 1499 1500lemma unbind_maybe_notification_ct_active[wp]: 1501 "\<lbrace>ct_active\<rbrace> 1502 unbind_maybe_notification ptr 1503 \<lbrace>\<lambda>_. ct_active \<rbrace>" 1504 apply (rule hoare_pre) 1505 apply (wp | wps | simp add: unbind_maybe_notification_def ct_in_state_def | wpc)+ 1506 done 1507 1508lemma unbind_notification_ct_active[wp]: 1509 "\<lbrace>ct_active\<rbrace> 1510 unbind_notification ptr 1511 \<lbrace>\<lambda>_. ct_active \<rbrace>" 1512 apply (rule hoare_pre) 1513 apply (wp | wps | simp add: unbind_notification_def ct_in_state_def | wpc)+ 1514 done 1515 1516lemma sts_Restart_ct_active[wp]: 1517 "\<lbrace>ct_active\<rbrace> set_thread_state xa Restart \<lbrace>\<lambda>xb. ct_active\<rbrace>" 1518 apply (wp set_object_wp | simp add: set_thread_state_def)+ 1519 apply (clarsimp simp: ct_in_state_def st_tcb_at_def obj_at_def) 1520 done 1521 1522lemma cancel_all_ipc_ct_active[wp]: 1523 "\<lbrace>ct_active\<rbrace> 1524 cancel_all_ipc ptr 1525 \<lbrace>\<lambda>_. ct_active \<rbrace>" 1526 apply (wp mapM_x_wp set_simple_ko_ct_active | wps | simp add: cancel_all_ipc_def | wpc)+ 1527 apply force 1528 apply (wp mapM_x_wp set_simple_ko_ct_active)+ 1529 apply force 1530 apply (wp set_simple_ko_ct_active hoare_drop_imps hoare_vcg_conj_lift hoare_vcg_all_lift)+ 1531 apply simp 1532 done 1533 1534crunch ct_active [wp]: cap_swap_for_delete "ct_active" 1535 ( wp: crunch_wps filterM_preserved hoare_unless_wp 1536 simp: crunch_simps ignore: do_extended_op) 1537 1538crunch ct_active [wp]: post_cap_deletion, empty_slot "ct_active" 1539 ( wp: crunch_wps filterM_preserved hoare_unless_wp 1540 simp: crunch_simps ignore: do_extended_op) 1541 1542lemma thread_set_non_current_current_ipc_buffer_register: 1543 "\<lbrace>\<lambda>s. ptr \<noteq> cur_thread s \<and> P (current_ipc_buffer_register s)\<rbrace> 1544 thread_set f ptr 1545 \<lbrace>\<lambda>_ s. P (current_ipc_buffer_register s) \<rbrace>" 1546 apply (simp add: thread_set_def | wp set_object_wp)+ 1547 apply (auto simp: get_tcb_def current_ipc_buffer_register_def) 1548 done 1549 1550crunch cur_thread[wp]: cap_swap_for_delete,finalise_cap "\<lambda>s. P (cur_thread s)" (wp: select_wp dxo_wp_weak crunch_wps simp: crunch_simps ) 1551 1552lemma irq_state_indepenedent_cur_thread[simp]: "irq_state_independent_A (\<lambda>s. P (cur_thread s))" 1553 by (simp add: irq_state_independent_def) 1554 1555lemma rec_del_cur_thread[wp]:"\<lbrace>\<lambda>s. P (cur_thread s)\<rbrace> rec_del a \<lbrace>\<lambda>r s. P (cur_thread s)\<rbrace>" 1556 apply (rule rec_del_preservation) 1557 apply (wp preemption_point_inv|simp)+ 1558 done 1559 1560crunch cur_thread[wp]: cap_delete,cap_move "\<lambda>s. P (cur_thread s)" (wp: cap_revoke_preservation2 mapM_wp mapM_x_wp crunch_wps dxo_wp_weak simp: filterM_mapM unless_def ignore: without_preemption filterM) 1561 1562lemma cap_revoke_cur_thread[wp]: "\<lbrace>\<lambda>s. P (cur_thread s)\<rbrace> cap_revoke a \<lbrace>\<lambda>r s. P (cur_thread s)\<rbrace>" 1563 apply (rule cap_revoke_preservation2) 1564 apply (wp preemption_point_inv|simp)+ 1565 done 1566 1567crunch cur_thread[wp]: cancel_badged_sends "\<lambda>s. P (cur_thread s)" (wp: crunch_wps mapM_wp mapM_x_wp dxo_wp_weak simp: filterM_mapM unless_def ignore: without_preemption filterM) 1568 1569lemma invoke_cnode_cur_thread[wp]: "\<lbrace>\<lambda>s. P (cur_thread s)\<rbrace> invoke_cnode a \<lbrace>\<lambda>r s. P (cur_thread s)\<rbrace>" 1570 apply (simp add: invoke_cnode_def) 1571 apply (rule hoare_pre) 1572 apply (wp hoare_drop_imps hoare_vcg_all_lift | wpc | simp split del: if_split)+ 1573 done 1574 1575crunch cur_thread[wp]: handle_event "\<lambda>s. P (cur_thread s)" 1576 (wp: syscall_valid crunch_wps check_cap_inv dxo_wp_weak 1577 simp: crunch_simps filterM_mapM 1578 ignore: syscall) 1579 1580crunches ethread_set, timer_tick, possible_switch_to, handle_interrupt 1581 for pas_cur_domain[wp]: "pas_cur_domain pas" 1582 (wp: crunch_wps simp: crunch_simps) 1583 1584lemma dxo_idle_thread[wp]: 1585 "\<lbrace>\<lambda>s. P (idle_thread s) \<rbrace> do_extended_op f \<lbrace>\<lambda>_ s. P (idle_thread s)\<rbrace>" 1586 by (clarsimp simp: valid_def dest!: in_dxo_idle_threadD) 1587 1588crunch idle_thread[wp]: throwError "\<lambda>s. P (idle_thread s)" 1589 1590lemma preemption_point_idle_thread[wp]: 1591 "\<lbrace>\<lambda>s. P (idle_thread s) \<rbrace> preemption_point \<lbrace>\<lambda>_ s. P (idle_thread s)\<rbrace>" 1592 apply (clarsimp simp: preemption_point_def) 1593 by (wp OR_choiceE_weak_wp | wpc | simp)+ 1594 1595(* following idle_thread and cur_domain proofs clagged from infoflow/PasUpdates.thy *) 1596crunch idle_thread[wp]: cap_swap_for_delete,finalise_cap,cap_move,cap_swap,cap_delete,cancel_badged_sends 1597 "\<lambda>s. P (idle_thread s)" 1598 ( wp: syscall_valid crunch_wps rec_del_preservation cap_revoke_preservation modify_wp dxo_wp_weak 1599 simp: crunch_simps check_cap_at_def filterM_mapM unless_def 1600 ignore: without_preemption filterM rec_del check_cap_at cap_revoke ) 1601 1602lemma cap_revoke_idle_thread[wp]:"\<lbrace>\<lambda>s. P (idle_thread s)\<rbrace> cap_revoke a \<lbrace>\<lambda>r s. P (idle_thread s)\<rbrace>" 1603 by (rule cap_revoke_preservation2; wp) 1604 1605lemma invoke_cnode_idle_thread[wp]: "\<lbrace>\<lambda>s. P (idle_thread s)\<rbrace> invoke_cnode a \<lbrace>\<lambda>r s. P (idle_thread s)\<rbrace>" 1606 apply (simp add: invoke_cnode_def) 1607 apply (rule hoare_pre) 1608 apply (wp hoare_drop_imps hoare_vcg_all_lift | wpc | simp split del: if_split)+ 1609 done 1610 1611crunch idle_thread[wp]: handle_event "\<lambda>s::det_state. P (idle_thread s)" 1612 (wp: syscall_valid crunch_wps 1613 simp: crunch_simps check_cap_at_def 1614 ignore: check_cap_at syscall) 1615 1616crunch cur_domain[wp]: 1617 transfer_caps_loop, ethread_set, thread_set_priority, set_priority, 1618 set_domain, invoke_domain, cap_move_ext, timer_tick, 1619 cap_move, cancel_badged_sends, possible_switch_to 1620 "\<lambda>s. P (cur_domain s)" 1621 (wp: crunch_wps simp: crunch_simps filterM_mapM 1622 rule: transfer_caps_loop_pres) 1623 1624lemma invoke_cnode_cur_domain[wp]: "\<lbrace>\<lambda>s. P (cur_domain s)\<rbrace> invoke_cnode a \<lbrace>\<lambda>r s. P (cur_domain s)\<rbrace>" 1625 apply (simp add: invoke_cnode_def) 1626 apply (rule hoare_pre) 1627 apply (wp hoare_drop_imps hoare_vcg_all_lift | wpc | simp split del: if_split)+ 1628 done 1629 1630crunch cur_domain[wp]: handle_event "\<lambda>s. P (cur_domain s)" 1631 (wp: syscall_valid crunch_wps check_cap_inv 1632 simp: crunch_simps 1633 ignore: check_cap_at syscall) 1634 1635lemma handle_event_guarded_pas_domain[wp]: 1636 "\<lbrace>guarded_pas_domain aag\<rbrace> handle_event e \<lbrace>\<lambda>_. guarded_pas_domain aag\<rbrace>" 1637 by (wp guarded_pas_domain_lift) 1638 1639lemma handle_interrupt_guarded_pas_domain[wp]: 1640 "\<lbrace>guarded_pas_domain aag\<rbrace> handle_interrupt blah \<lbrace>\<lambda>_. guarded_pas_domain aag\<rbrace>" 1641 by (wp guarded_pas_domain_lift) 1642 1643lemma current_ipc_buffer_register_irq_state_update: "current_ipc_buffer_register (s\<lparr>machine_state := machine_state s \<lparr>irq_state := Suc (irq_state (machine_state s))\<rparr>\<rparr>) = current_ipc_buffer_register s" 1644by (clarsimp simp: current_ipc_buffer_register_def get_tcb_def) 1645 1646lemma call_kernel_integrity': 1647 "st \<turnstile> \<lbrace>einvs and pas_refined aag and is_subject aag \<circ> cur_thread and schact_is_rct and guarded_pas_domain aag 1648 and domain_sep_inv (pasMaySendIrqs aag) st' 1649 and (\<lambda>s. ev \<noteq> Interrupt \<longrightarrow> ct_active s) and (ct_active or ct_idle) 1650 and K (pasMayActivate aag \<and> pasMayEditReadyQueues aag)\<rbrace> 1651 call_kernel ev 1652 \<lbrace>\<lambda>_. integrity aag X st\<rbrace>" 1653 apply (simp add: call_kernel_def getActiveIRQ_def ) 1654 apply (simp add: spec_valid_def) 1655 apply (wp activate_thread_respects schedule_integrity_pasMayEditReadyQueues 1656 handle_interrupt_integrity handle_interrupt_current_ipc_buffer_register 1657 dmo_wp alternative_wp select_wp handle_interrupt_pas_refined 1658 | simp add: current_ipc_buffer_register_irq_state_update)+ 1659 apply (rule hoare_post_impErr, 1660 rule_tac Q = "integrity aag X st and pas_refined aag and einvs and guarded_pas_domain aag and domain_sep_inv (pasMaySendIrqs aag) st' 1661 and is_subject aag \<circ> cur_thread 1662 and (\<lambda>_. pasMayActivate aag \<and> pasMayEditReadyQueues aag)" in valid_validE) 1663 apply (wp handle_event_integrity he_invs handle_event_pas_refined 1664 handle_event_cur_thread handle_event_cur_domain 1665 handle_event_domain_sep_inv handle_event_valid_sched | simp)+ 1666 apply(fastforce simp: domain_sep_inv_def guarded_pas_domain_def)+ 1667 done 1668 1669 1670lemma call_kernel_integrity: 1671 "\<lbrace>pas_refined pas and einvs 1672 and (\<lambda>s. ev \<noteq> Interrupt \<longrightarrow> ct_active s) and (ct_active or ct_idle) 1673 and domain_sep_inv (pasMaySendIrqs pas) st' 1674 and schact_is_rct and guarded_pas_domain pas 1675 and is_subject pas o cur_thread and K (pasMayActivate pas \<and> pasMayEditReadyQueues pas) and (\<lambda>s. s = st)\<rbrace> 1676 call_kernel ev 1677 \<lbrace>\<lambda>_. integrity pas X st\<rbrace>" 1678 using call_kernel_integrity' [of st pas st' ev X] 1679 apply (simp add: spec_valid_def) 1680 apply (erule hoare_chain) 1681 apply clarsimp 1682 apply assumption 1683 done 1684 1685 1686lemma call_kernel_pas_refined: 1687 "\<lbrace>einvs and pas_refined aag and is_subject aag \<circ> cur_thread and guarded_pas_domain aag 1688 and (\<lambda>s. ev \<noteq> Interrupt \<longrightarrow> ct_active s) and (ct_active or ct_idle) 1689 and schact_is_rct and pas_cur_domain aag and domain_sep_inv (pasMaySendIrqs aag) st'\<rbrace> 1690 call_kernel ev 1691 \<lbrace>\<lambda>_. pas_refined aag\<rbrace>" 1692 apply (simp add: call_kernel_def getActiveIRQ_def) 1693 apply (wp activate_thread_pas_refined schedule_pas_refined handle_interrupt_pas_refined 1694 do_machine_op_pas_refined dmo_wp alternative_wp select_wp) 1695 apply simp 1696 apply (rule hoare_post_impErr [OF valid_validE [where Q = "pas_refined aag and invs"]]) 1697 apply (wp he_invs handle_event_pas_refined) 1698 apply auto 1699 done 1700 1701end 1702 1703end 1704