diff --git a/proof/crefine/RISCV64/IpcCancel_C.thy b/proof/crefine/RISCV64/IpcCancel_C.thy index 567f1b5588..aaf1aa5aef 100644 --- a/proof/crefine/RISCV64/IpcCancel_C.thy +++ b/proof/crefine/RISCV64/IpcCancel_C.thy @@ -2739,7 +2739,8 @@ lemma epQueue_tail_sign[simp]: (* Clag from cancelSignal_ccorres_helper *) lemma cancelIPC_ccorres_helper: - "ccorres dc xfdc (invs' and (\s. sym_refs (state_refs_of' s)) and + "\epptr = Ptr ep\ \ + ccorres dc xfdc (invs' and (\s. sym_refs (state_refs_of' s)) and st_tcb_at' (\st. (isBlockedOnSend st \ isBlockedOnReceive st) \ blockingObject st = ep) thread and ko_at' ep' ep) @@ -2915,9 +2916,13 @@ sorry (* FIXME RT: reply_remove_tcb_corres *) lemma reply_unlink_ccorres: "ccorres dc xfdc - (invs' and tcb_at' tcbPtr and reply_at' replyPtr) - (\\tcb = tcb_ptr_to_ctcb_ptr tcbPtr\ \ \\reply = Ptr replyPtr\) [] - (replyUnlink tcbPtr replyPtr) (Call reply_unlink_'proc)" + (valid_tcbs' and pspace_aligned' and pspace_distinct' + and st_tcb_at' (\st. (\oref cg. st = Structures_H.BlockedOnReceive oref cg (Some replyPtr)) + \ st = Structures_H.BlockedOnReply (Some replyPtr)) + tcbPtr + and obj_at' (\reply. replyTCB reply = Some tcbPtr) replyPtr) + (\\reply = Ptr replyPtr\ \ \\tcb = tcb_ptr_to_ctcb_ptr tcbPtr\) [] + (replyUnlink replyPtr tcbPtr) (Call reply_unlink_'proc)" sorry (* FIXME RT: reply_unlink_ccorres *) lemma reply_pop_ccorres: @@ -2934,6 +2939,88 @@ lemma reply_remove_ccorres: (replyRemove replyPtr tcbPtr) (Call reply_remove_'proc)" sorry (* FIXME RT: reply_remove_ccorres *) +lemma getBlockingObject_BlockedOnReceive_return: + "(getBlockingObject (Structures_H.thread_state.BlockedOnReceive oref cg ro)) = return oref" + unfolding getBlockingObject_def epBlocked_def by simp + +lemma getBlockingObject_BlockedOnSend_return: + "(getBlockingObject (Structures_H.thread_state.BlockedOnSend oref badge cg cgr isc)) = return oref" + unfolding getBlockingObject_def epBlocked_def by simp + +lemma BlockedOnReceive_replyObject_no_0: + "\ ts = BlockedOnReceive oref cg ro; no_0_obj' s; valid_tcb_state' ts s \ + \ ro \ Some 0" + by (auto simp: valid_tcb_state'_def) + +lemma ctcb_relation_BlockedOnReceive_blockingObject: + "\ BlockedOnReceive oref cg ro = tcbState tcb; ctcb_relation tcb ctcb \ + \ blockingObject_CL (thread_state_lift (tcbState_C ctcb)) = oref" + by (cases "(tcbState tcb)", simp_all add: ctcb_relation_def cthread_state_relation_def) + +lemma ctcb_relation_BlockedOnReceive_replyObject: + "\ BlockedOnReceive oref cg ro = tcbState tcb; ctcb_relation tcb ctcb \ + \ replyObject_CL (thread_state_lift (tcbState_C ctcb)) = option_to_0 ro" + by (cases "(tcbState tcb)", simp_all add: ctcb_relation_def cthread_state_relation_def) + +lemma ctcb_relation_BlockedOnSend_blockingObject: + "\ BlockedOnSend oref badge cg cgr isc = tcbState tcb; ctcb_relation tcb ctcb \ + \ blockingObject_CL (thread_state_lift (tcbState_C ctcb)) = oref" + by (cases "(tcbState tcb)", simp_all add: ctcb_relation_def cthread_state_relation_def) + +lemma BlockedOnReceive_ep_at': + "\ st_tcb_at' ((=) (BlockedOnReceive oref cg ro)) t s; valid_objs' s \ + \ ep_at' oref s" + by (fastforce dest!: tcb_in_valid_state' simp: obj_at'_def valid_tcb_state'_def) + +lemma BlockedOnSend_ep_at': + "\ st_tcb_at' ((=) (BlockedOnSend oref badge cg cgr isc)) t s; valid_objs' s \ + \ ep_at' oref s" + by (fastforce dest!: tcb_in_valid_state' simp: obj_at'_def valid_tcb_state'_def) + +lemma sym_ref_BlockedOnReceive_replyObject_linked: + assumes st: "st_tcb_at' ((=) (Structures_H.thread_state.BlockedOnReceive oref cg (Some ro))) thread s" + assumes sy: "sym_refs (state_refs_of' s)" + assumes vo: "valid_objs' s" + shows "obj_at' (\reply. replyTCB reply = Some thread) ro s" +proof - + from vo and st have ra: + "reply_at' ro s" + by - (drule (1) tcb_in_valid_state', fastforce simp: obj_at'_def valid_tcb_state'_def) + from st have ko: + "\tcb. ko_at' tcb thread s \ tcbState tcb = BlockedOnReceive oref cg (Some ro)" + by (clarsimp simp: st_tcb_at'_def obj_at'_def) + with sy and vo and st and ra show ?thesis + apply (clarsimp simp: st_tcb_at'_def) + apply (frule (1) sym_ref_Receive_or_Reply_replyTCB') + apply simp + apply (clarsimp simp: obj_at'_def) + done +qed + +lemma cancelIPC_threadSet_wp: + shows "threadSet (tcbFault_update (\_. None)) t + \\s. st_tcb_at' ((=) ts) t s \ invs' s + \ weak_sch_act_wf (ksSchedulerAction s) s \ sym_refs_asrt s\" +proof - + have sy: "threadSet (tcbFault_update (\_. None)) t \sym_refs_asrt\" + unfolding sym_refs_asrt_def + by (wpsimp wp: threadSet_state_refs_of') + (force simp: tcb_bound_refs'_def)+ + show ?thesis + by (wpsimp wp: threadSet_fault_invs' threadSet_pred_tcb_no_state + weak_sch_act_wf_lift tcb_in_cur_domain'_lift sy) +qed + +lemma thread_state_to_tsType_eq_BlockedOnReceive: + "BlockedOnReceive oref cg ro = ts + \ thread_state_to_tsType ts = scast ThreadState_BlockedOnReceive" + by (cases ts, simp_all add: ThreadState_defs) + +lemma thread_state_to_tsType_eq_BlockedOnSend: + "BlockedOnSend oref badge cg cgr isc = ts + \ thread_state_to_tsType ts = scast ThreadState_BlockedOnSend" + by (cases ts, simp_all add: ThreadState_defs) + lemma cancelIPC_ccorres1: assumes cteDeleteOne_ccorres: "\w slot. ccorres dc xfdc @@ -2948,198 +3035,256 @@ lemma cancelIPC_ccorres1: (UNIV \ {s. tptr_' s = tcb_ptr_to_ctcb_ptr thread}) [] (cancelIPC thread) (Call cancelIPC_'proc)" apply (cinit lift: tptr_' simp: Let_def cong: call_ignore_cong) -sorry (* FIXME RT: cancelIPC_ccorres1 *) (* apply (rule ccorres_move_c_guard_tcb) - apply csymbr + apply (rule ccorres_stateAssert) + apply (rule ccorres_stateAssert) apply (rule getThreadState_ccorres_foo) - apply (rule ccorres_symb_exec_r) - apply (rule_tac xf'=ret__unsigned_longlong_' in ccorres_abstract, ceqv) - apply (rule_tac P="rv' = thread_state_to_tsType rv" in ccorres_gen_asm2) - apply wpc - \ \BlockedOnReceive\ - apply (simp add: word_sle_def ccorres_cond_iffs cong: call_ignore_cong) - apply (rule ccorres_rhs_assoc)+ - apply csymbr - apply csymbr - apply (rule ccorres_pre_getEndpoint) - apply (rule ccorres_assert) - apply (rule ccorres_symb_exec_r) \ \ptr_get lemmas don't work so well :(\ + apply (rename_tac threadState) + apply csymbr + apply csymbr + apply (rule ccorres_split_nothrow) + apply (rule threadSet_ccorres_lemma2[where P=\]) + apply vcg + apply (clarsimp simp: typ_heap_simps') + apply (erule(1) rf_sr_tcb_update_no_queue2, (simp add: typ_heap_simps')+)[1] + apply (rule ball_tcb_cte_casesI, simp_all)[1] + apply (clarsimp simp: ctcb_relation_def seL4_Fault_lift_NullFault + cfault_rel_def cthread_state_relation_def) + apply (case_tac "tcbState tcb", simp_all add: is_cap_fault_def)[1] + apply ceqv + apply (rule_tac xf'=ret__unsigned_longlong_' + and val="thread_state_to_tsType threadState" + and R="st_tcb_at' ((=) threadState) thread" + and R'=UNIV + in ccorres_symb_exec_r_known_rv) + apply (rule conseqPre, vcg) + apply (clarsimp simp: st_tcb_at'_def) + apply (frule (1) obj_at_cslift_tcb) + apply (clarsimp simp: typ_heap_simps ctcb_relation_thread_state_to_tsType) + apply ceqv + apply wpc + \ \BlockedOnReceive\ + apply (rename_tac oref cg ro) + apply (unfold blockedCancelIPC_def) + apply (simp add: ccorres_cond_iffs getBlockingObject_BlockedOnReceive_return + return_bind) + apply (rule ccorres_rhs_assoc)+ + apply csymbr + apply csymbr + apply (rule ccorres_pre_getEndpoint) + apply (rule ccorres_assert) + apply (rule_tac xf'=ret__unsigned_longlong_' + and val="oref" + and R="st_tcb_at' ((=) (BlockedOnReceive oref cg ro)) thread" + and R'=UNIV + in ccorres_symb_exec_r_known_rv) + apply (rule conseqPre, vcg) + apply (clarsimp simp: st_tcb_at'_def) + apply (frule (1) obj_at_cslift_tcb) + apply (clarsimp simp: typ_heap_simps ctcb_relation_BlockedOnReceive_blockingObject) + apply ceqv apply (rule ccorres_symb_exec_r) - apply (simp only: fun_app_def simp_list_case_return - return_bind ccorres_seq_skip) + apply (simp only: list_case_If) apply (rule ccorres_rhs_assoc2) apply (rule ccorres_rhs_assoc2) apply (rule ccorres_rhs_assoc2) apply (ctac (no_vcg) add: cancelIPC_ccorres_helper) - apply (ctac add: setThreadState_ccorres_valid_queues') - apply (wp hoare_vcg_all_lift set_ep_valid_objs' | simp add: valid_tcb_state'_def split del: if_split)+ - apply (simp add: ThreadState_defs) + apply (rule_tac P="tcb_at' thread" in ccorres_cross_over_guard) + apply (rule_tac xf'=ret__unsigned_longlong_' + and val="thread_state_to_tsType threadState" + and R="st_tcb_at' ((=) threadState) thread" + and R'=UNIV + in ccorres_symb_exec_r_known_rv) + apply (rule conseqPre, vcg) + apply (clarsimp simp: st_tcb_at'_def) + apply (frule (1) obj_at_cslift_tcb) + apply (fastforce simp: typ_heap_simps ctcb_relation_thread_state_to_tsType + thread_state_to_tsType_eq_BlockedOnReceive) + apply ceqv + apply ccorres_rewrite + apply (rule ccorres_rhs_assoc) + apply (rule ccorres_rhs_assoc) + apply (rule_tac xf'=ret__unsigned_longlong_' + and val="option_to_0 ro" + and R="st_tcb_at' ((=) threadState) thread" + and R'=UNIV + in ccorres_symb_exec_r_known_rv) + apply (rule conseqPre, vcg) + apply (clarsimp simp: st_tcb_at'_def) + apply (frule (1) obj_at_cslift_tcb) + apply (clarsimp simp: typ_heap_simps + ctcb_relation_BlockedOnReceive_replyObject) + apply ceqv + apply csymbr + apply (rule_tac P="ro \ Some 0" in ccorres_gen_asm) + apply wpc + \ \None\ + apply simp + apply (ctac add: setThreadState_ccorres) + \ \Some\ + apply simp + apply (ctac (no_vcg) add: reply_unlink_ccorres) + apply (ctac add: setThreadState_ccorres) + apply wp + apply vcg + apply vcg + apply (subst option.split[symmetric, where P=id, simplified]) + apply (wpsimp wp: hoare_case_option_wp2) + apply simp + apply clarsimp + apply (frule (1) tcb_at_h_t_valid) + apply simp apply vcg apply (rule conseqPre, vcg) apply clarsimp - apply clarsimp - apply (rule conseqPre, vcg) - apply (rule subset_refl) - apply (rule conseqPre, vcg) - apply clarsimp - \ \BlockedOnReply case\ - apply (simp add: ThreadState_defs ccorres_cond_iffs - Collect_False Collect_True word_sle_def - cong: call_ignore_cong del: Collect_const) - apply (rule ccorres_rhs_assoc)+ - apply csymbr - apply csymbr - apply csymbr - apply (rule ccorres_move_c_guard_tcb)+ - apply (rule ccorres_split_nothrow_novcg) - apply (rule_tac P=\ in threadSet_ccorres_lemma2) - apply vcg - apply (clarsimp simp: typ_heap_simps') - apply (erule(1) rf_sr_tcb_update_no_queue2, - (simp add: typ_heap_simps')+)[1] - apply (rule ball_tcb_cte_casesI, simp_all)[1] - apply (clarsimp simp: ctcb_relation_def seL4_Fault_lift_NullFault - cfault_rel_def cthread_state_relation_def) - apply (case_tac "tcbState tcb", simp_all add: is_cap_fault_def)[1] - apply ceqv - apply ccorres_remove_UNIV_guard - apply (rule ccorres_move_array_assertion_tcb_ctes) - apply (rule_tac P="tcb_at' thread" in ccorres_cross_over_guard) - apply (simp add: getThreadReplySlot_def) - apply ctac - apply (simp only: liftM_def bind_assoc return_bind del: Collect_const) - apply (rule ccorres_pre_getCTE) - apply (rename_tac slot slot' cte) - apply (rule ccorres_move_c_guard_cte) - apply (rule_tac xf'=ret__unsigned_longlong_' and val="mdbNext (cteMDBNode cte)" - and R="cte_wp_at' ((=) cte) slot and invs'" - in ccorres_symb_exec_r_known_rv_UNIV[where R'=UNIV]) - apply vcg - apply (clarsimp simp: cte_wp_at_ctes_of) - apply (erule(1) cmap_relationE1[OF cmap_relation_cte]) - apply (clarsimp simp: typ_heap_simps) - apply (clarsimp simp: ccte_relation_def map_option_Some_eq2) - apply ceqv - apply csymbr - apply (rule ccorres_Cond_rhs) - apply (simp add: nullPointer_def when_def) - apply (rule ccorres_symb_exec_l[OF _ _ _ empty_fail_stateAssert]) - apply (rule ccorres_symb_exec_r) - apply (ctac add: cteDeleteOne_ccorres[where w1="scast cap_reply_cap"]) - apply vcg - apply (rule conseqPre, vcg, clarsimp simp: rf_sr_def - gs_set_assn_Delete_cstate_relation[unfolded o_def]) - apply (wp | simp)+ - apply (rule ccorres_return_Skip) - apply (simp add: guard_is_UNIV_def ghost_assertion_data_get_def - ghost_assertion_data_set_def cap_tag_defs) - apply (simp add: locateSlot_conv, wp) apply vcg - apply (rule_tac Q'="\rv. tcb_at' thread and invs'" in hoare_post_imp) - apply (clarsimp simp: cte_wp_at_ctes_of capHasProperty_def - cap_get_tag_isCap ucast_id) - apply (wp threadSet_invs_trivial | simp)+ - apply (clarsimp simp add: guard_is_UNIV_def tcbReplySlot_def - Kernel_C.tcbReply_def tcbCNodeEntries_def) - \ \BlockedOnNotification\ - apply (simp add: word_sle_def ThreadState_defs ccorres_cond_iffs - cong: call_ignore_cong) - apply (rule ccorres_symb_exec_r) - apply (ctac (no_vcg)) - apply clarsimp + \ \BlockedOnReply case\ + apply (simp add: ThreadState_defs ccorres_cond_iffs + Collect_False Collect_True word_sle_def + cong: call_ignore_cong del: Collect_const) + apply simp + apply (ctac add: reply_remove_tcb_ccorres) + \ \BlockedOnNotification\ + apply (simp add: word_sle_def ThreadState_defs ccorres_cond_iffs + cong: call_ignore_cong) + apply (rule ccorres_symb_exec_r) + apply (ctac (no_vcg)) + apply clarsimp + apply (rule conseqPre, vcg) + apply (rule subset_refl) apply (rule conseqPre, vcg) - apply (rule subset_refl) + apply clarsimp + \ \Running, Inactive, and Idle\ + apply (simp add: word_sle_def ThreadState_defs ccorres_cond_iffs + cong: call_ignore_cong, + rule ccorres_return_Skip)+ + + \ \BlockedOnSend\ + apply (simp add: word_sle_def ccorres_cond_iffs + cong: call_ignore_cong) + \ \clag\ + apply (rename_tac oref badge cg cgr isc) + apply (unfold getBlockingObject_BlockedOnSend_return) + apply (simp only: return_bind) + apply (rule ccorres_rhs_assoc)+ + apply csymbr + apply csymbr + apply (rule ccorres_pre_getEndpoint) + apply (rule ccorres_assert) + apply (rule_tac xf'=ret__unsigned_longlong_' + and val="oref" + and R="st_tcb_at' ((=) (BlockedOnSend oref badge cg cgr isc)) thread" + and R'=UNIV + in ccorres_symb_exec_r_known_rv) apply (rule conseqPre, vcg) - apply clarsimp - \ \Running, Inactive, and Idle\ - apply (simp add: word_sle_def ThreadState_defs ccorres_cond_iffs - cong: call_ignore_cong, - rule ccorres_return_Skip)+ - \ \BlockedOnSend\ - apply (simp add: word_sle_def ccorres_cond_iffs - cong: call_ignore_cong) - \ \clag\ - apply (rule ccorres_rhs_assoc)+ - apply csymbr - apply csymbr - apply (rule ccorres_pre_getEndpoint) - apply (rule ccorres_assert) - apply (rule ccorres_symb_exec_r) \ \ptr_get lemmas don't work so well :(\ + apply (clarsimp simp: st_tcb_at'_def) + apply (frule (1) obj_at_cslift_tcb) + apply (clarsimp simp: typ_heap_simps ctcb_relation_BlockedOnSend_blockingObject) + apply ceqv apply (rule ccorres_symb_exec_r) - apply (simp only: fun_app_def simp_list_case_return return_bind ccorres_seq_skip) + apply (simp only: list_case_If) apply (rule ccorres_rhs_assoc2) apply (rule ccorres_rhs_assoc2) apply (rule ccorres_rhs_assoc2) apply (ctac (no_vcg) add: cancelIPC_ccorres_helper) - apply (ctac add: setThreadState_ccorres_valid_queues') - apply (wp hoare_vcg_all_lift set_ep_valid_objs' | simp add: valid_tcb_state'_def split del:if_split)+ - apply (simp add: ThreadState_defs) - apply clarsimp - apply (rule conseqPre, vcg, rule subset_refl) + apply (rule_tac P="tcb_at' thread" in ccorres_cross_over_guard) + apply (rule_tac xf'=ret__unsigned_longlong_' + and val="scast ThreadState_BlockedOnSend" + and R="st_tcb_at' ((=) threadState) thread" + and R'=UNIV + in ccorres_symb_exec_r_known_rv) + apply (rule conseqPre, vcg) + apply (clarsimp simp: st_tcb_at'_def) + apply (frule (1) obj_at_cslift_tcb) + apply (fastforce simp: typ_heap_simps ctcb_relation_thread_state_to_tsType + thread_state_to_tsType_eq_BlockedOnSend) + apply ceqv + apply (simp only: ThreadState_defs) + apply ccorres_rewrite + apply (ctac add: setThreadState_ccorres) + apply vcg + apply wp + apply simp + apply (clarsimp simp: ThreadState_defs) + apply (frule (1) tcb_at_h_t_valid) + apply simp + apply vcg apply (rule conseqPre, vcg) apply clarsimp - apply clarsimp - apply (rule conseqPre, vcg, rule subset_refl) - apply (rule conseqPre, vcg) + apply vcg + \ \Restart\ + apply (simp add: word_sle_def ThreadState_defs ccorres_cond_iffs + cong: call_ignore_cong, + rule ccorres_return_Skip) + \ \Post wp proofs\ + apply vcg + apply (rule_tac Q'="\rv s. tcb_at' thread s + \ st_tcb_at' ((=) threadState) thread s + \ invs' s \ weak_sch_act_wf (ksSchedulerAction s) s + \ sym_refs_asrt s" + in hoare_strengthen_post) + apply (wp add: cancelIPC_threadSet_wp) + apply clarsimp + apply (frule obj_at_valid_objs', clarsimp+) + apply (clarsimp simp: valid_obj'_def valid_tcb'_def valid_tcb_state'_def invs_valid_objs' + BlockedOnReceive_ep_at') + apply (rule conjI, clarsimp) + apply (rename_tac oref cg ro) + apply (rule conjI) + apply (clarsimp simp: invs_valid_objs' BlockedOnReceive_ep_at') + apply clarsimp + apply (frule tcb_in_valid_state') + apply (simp add: invs'_implies) + apply (elim conjE exE) + apply (rule conjI) + apply (case_tac ro) + apply (clarsimp simp: sym_refs_asrt_def invs'_implies valid_objs'_valid_tcbs' + sym_ref_BlockedOnReceive_replyObject_linked) + subgoal by (auto simp: obj_at'_def pred_tcb_at'_def valid_ep'_def isTS_defs + split: thread_state.splits) + apply (clarsimp simp: sym_refs_asrt_def invs'_implies valid_objs'_valid_tcbs' + sym_ref_BlockedOnReceive_replyObject_linked) + apply (simp only: conj_assoc[symmetric]) + apply (rule conjI) + subgoal by (auto simp: st_tcb_at'_def obj_at'_def isTS_defs valid_ep'_def + split: thread_state.splits) + subgoal by (auto simp: invs'_implies valid_tcb_state'_def BlockedOnReceive_replyObject_no_0) + apply (clarsimp simp: sym_refs_asrt_def invs'_implies valid_objs'_valid_tcbs' + sym_ref_BlockedOnReceive_replyObject_linked) + apply (case_tac ro) apply clarsimp - \ \Restart\ - apply (simp add: word_sle_def ThreadState_defs ccorres_cond_iffs - cong: call_ignore_cong, - rule ccorres_return_Skip) - \ \Post wp proofs\ - apply vcg - apply clarsimp - apply (rule conseqPre, vcg) - apply clarsimp - apply clarsimp - apply (drule(1) obj_at_cslift_tcb) - apply clarsimp - apply (frule obj_at_valid_objs', clarsimp+) - apply (clarsimp simp: projectKOs valid_obj'_def valid_tcb'_def - valid_tcb_state'_def typ_heap_simps - word_sle_def) - apply (rule conjI, clarsimp) - apply (rule conjI, clarsimp) + apply (frule (3) ep_blocked_in_queueD_recv) + apply (frule (1) ko_at_valid_ep'[OF _ invs_valid_objs']) + subgoal by (auto simp: obj_at'_def pred_tcb_at'_def valid_ep'_def isTS_defs isRecvEP_def + split: thread_state.splits endpoint.splits) + apply (clarsimp simp: sym_refs_asrt_def invs'_implies valid_objs'_valid_tcbs' + sym_ref_BlockedOnReceive_replyObject_linked) + apply (frule (3) ep_blocked_in_queueD_recv) + apply (frule (1) ko_at_valid_ep'[OF _ invs_valid_objs']) + apply (simp only: conj_assoc[symmetric]) + apply (rule conjI) + subgoal by (auto simp: obj_at'_def pred_tcb_at'_def valid_ep'_def isTS_defs isRecvEP_def + split: thread_state.splits endpoint.splits) + subgoal by (auto simp: invs'_implies valid_tcb_state'_def BlockedOnReceive_replyObject_no_0) apply (rule conjI) - subgoal by (auto simp: projectKOs obj_at'_def pred_tcb_at'_def split: thread_state.splits)[1] - apply (clarsimp) + apply (clarsimp simp: inQ_def) + apply clarsimp apply (rule conjI) - subgoal by (auto simp: obj_at'_def projectKOs pred_tcb_at'_def invs'_def valid_state'_def - isTS_defs cte_wp_at_ctes_of - cthread_state_relation_def sch_act_wf_weak valid_ep'_def - split: thread_state.splits) + apply (clarsimp simp: invs_valid_objs' BlockedOnSend_ep_at') apply clarsimp - apply (frule (2) ep_blocked_in_queueD_recv) + apply (rule conjI) + apply (clarsimp simp: sym_refs_asrt_def invs'_implies) + subgoal by (auto simp: obj_at'_def pred_tcb_at'_def valid_ep'_def isTS_defs isSendEP_def + split: thread_state.splits endpoint.splits) + apply (clarsimp simp: sym_refs_asrt_def invs'_implies valid_objs'_valid_tcbs' + sym_ref_BlockedOnReceive_replyObject_linked) + apply (frule (3) ep_blocked_in_queueD_send) apply (frule (1) ko_at_valid_ep'[OF _ invs_valid_objs']) - subgoal by (auto simp: obj_at'_def projectKOs pred_tcb_at'_def invs'_def valid_state'_def - isTS_defs cte_wp_at_ctes_of isRecvEP_def - cthread_state_relation_def sch_act_wf_weak valid_ep'_def - split: thread_state.splits endpoint.splits) - apply (rule conjI) - apply (clarsimp simp: inQ_def) - apply clarsimp - apply (rule conjI) - subgoal by (auto simp: obj_at'_def projectKOs pred_tcb_at'_def invs'_def valid_state'_def - isTS_defs cte_wp_at_ctes_of - cthread_state_relation_def sch_act_wf_weak valid_ep'_def - split: thread_state.splits) - apply clarsimp - apply (rule conjI) - subgoal by (auto simp: obj_at'_def projectKOs pred_tcb_at'_def invs'_def valid_state'_def - isTS_defs cte_wp_at_ctes_of - cthread_state_relation_def sch_act_wf_weak valid_ep'_def - split: thread_state.splits) - apply clarsimp - apply (frule (2) ep_blocked_in_queueD_send) - apply (frule (1) ko_at_valid_ep'[OF _ invs_valid_objs']) - subgoal by (auto simp: obj_at'_def projectKOs pred_tcb_at'_def invs'_def valid_state'_def - isTS_defs cte_wp_at_ctes_of isSendEP_def - cthread_state_relation_def sch_act_wf_weak valid_ep'_def - split: thread_state.splits endpoint.splits)[1] - apply (auto simp: isTS_defs cthread_state_relation_def typ_heap_simps weak_sch_act_wf_def) - apply (case_tac ts, - auto simp: isTS_defs cthread_state_relation_def typ_heap_simps) - done *) + subgoal by (auto simp: obj_at'_def pred_tcb_at'_def valid_ep'_def isTS_defs isSendEP_def + split: thread_state.splits endpoint.splits) + apply vcg + apply (auto simp: cthread_state_relation_def typ_heap_simps) + done end end