From 96b3754455eab083b9ba55c922e85d8bdd957046 Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Sun, 7 Jul 2019 13:42:36 +1000 Subject: [PATCH] riscv refine: set up IpcCancel (0 sorries) --- proof/refine/RISCV64/IpcCancel_R.thy | 2654 ++++++++++++++++++++++++++ 1 file changed, 2654 insertions(+) create mode 100644 proof/refine/RISCV64/IpcCancel_R.thy diff --git a/proof/refine/RISCV64/IpcCancel_R.thy b/proof/refine/RISCV64/IpcCancel_R.thy new file mode 100644 index 000000000..e32b04842 --- /dev/null +++ b/proof/refine/RISCV64/IpcCancel_R.thy @@ -0,0 +1,2654 @@ +(* + * Copyright 2019, Data61, CSIRO + * + * This software may be distributed and modified according to the terms of + * the GNU General Public License version 2. Note that NO WARRANTY is provided. + * See "LICENSE_GPLv2.txt" for details. + * + * @TAG(DATA61_GPL) + *) + +theory IpcCancel_R +imports + Schedule_R + "Lib.SimpStrategy" +begin + +context begin interpretation Arch . (*FIXME: arch_split*) + +crunch aligned'[wp]: cancelAllIPC pspace_aligned' + (wp: crunch_wps mapM_x_wp' simp: unless_def) +crunch distinct'[wp]: cancelAllIPC pspace_distinct' + (wp: crunch_wps mapM_x_wp' simp: unless_def) + +crunch aligned'[wp]: cancelAllSignals pspace_aligned' + (wp: crunch_wps mapM_x_wp') +crunch distinct'[wp]: cancelAllSignals pspace_distinct' + (wp: crunch_wps mapM_x_wp') + +lemma cancelSignal_simple[wp]: + "\\\ cancelSignal t ntfn \\rv. st_tcb_at' simple' t\" + apply (simp add: cancelSignal_def Let_def) + apply (wp setThreadState_st_tcb | simp)+ + done + +lemma cancelSignal_pred_tcb_at': + "\pred_tcb_at' proj P t' and K (t \ t')\ + cancelSignal t ntfnptr + \\rv. pred_tcb_at' proj P t'\" + apply (simp add: cancelSignal_def) + apply (wp sts_pred_tcb_neq' getNotification_wp | wpc | clarsimp)+ + done + +crunch pred_tcb_at'[wp]: emptySlot "pred_tcb_at' proj P t" + (wp: setCTE_pred_tcb_at') + +(* valid_queues is too strong *) +definition valid_inQ_queues :: "KernelStateData_H.kernel_state \ bool" where + "valid_inQ_queues \ + \s. \d p. (\t\set (ksReadyQueues s (d, p)). obj_at' (inQ d p) t s) \ distinct (ksReadyQueues s (d, p))" + +defs capHasProperty_def: + "capHasProperty ptr P \ cte_wp_at' (\c. P (cteCap c)) ptr" + +end + +(* Assume various facts about cteDeleteOne, proved in Finalise_R *) +locale delete_one_conc_pre = + assumes delete_one_st_tcb_at: + "\P. (\st. simple' st \ P st) \ + \st_tcb_at' P t\ cteDeleteOne slot \\rv. st_tcb_at' P t\" + assumes delete_one_typ_at: + "\P. \\s. P (typ_at' T p s)\ cteDeleteOne slot \\rv s. P (typ_at' T p s)\" + assumes delete_one_aligned: + "\pspace_aligned'\ cteDeleteOne slot \\rv. pspace_aligned'\" + assumes delete_one_distinct: + "\pspace_distinct'\ cteDeleteOne slot \\rv. pspace_distinct'\" + assumes delete_one_it: + "\P. \\s. P (ksIdleThread s)\ cteDeleteOne cap \\rv s. P (ksIdleThread s)\" + assumes delete_one_queues: + "\Invariants_H.valid_queues and valid_objs' and (\s. weak_sch_act_wf (ksSchedulerAction s) s)\ + cteDeleteOne sl \\rv. Invariants_H.valid_queues\" + assumes delete_one_inQ_queues: + "\valid_inQ_queues\ cteDeleteOne sl \\rv. valid_inQ_queues\" + assumes delete_one_sch_act_simple: + "\sch_act_simple\ cteDeleteOne sl \\rv. sch_act_simple\" + assumes delete_one_sch_act_not: + "\t. \sch_act_not t\ cteDeleteOne sl \\rv. sch_act_not t\" + assumes delete_one_reply_st_tcb_at: + "\P t. \\s. st_tcb_at' P t s \ (\t' r. cte_wp_at' (\cte. cteCap cte = ReplyCap t' False r) slot s)\ + cteDeleteOne slot + \\rv. st_tcb_at' P t\" + assumes delete_one_ksCurDomain: + "\P. \\s. P (ksCurDomain s)\ cteDeleteOne sl \\_ s. P (ksCurDomain s)\" + assumes delete_one_tcbDomain_obj_at': + "\P. \obj_at' (\tcb. P (tcbDomain tcb)) t'\ cteDeleteOne slot \\_. obj_at' (\tcb. P (tcbDomain tcb)) t'\" + +lemma (in delete_one_conc_pre) cancelIPC_simple[wp]: + "\\\ cancelIPC t \\rv. st_tcb_at' simple' t\" + apply (simp add: cancelIPC_def Let_def getThreadReplySlot_def + cong: Structures_H.thread_state.case_cong list.case_cong) + apply (rule hoare_seq_ext [OF _ gts_sp']) + apply (rule hoare_pre) + apply (wpc + | wp sts_st_tcb_at'_cases hoare_vcg_conj_lift + hoare_vcg_const_imp_lift delete_one_st_tcb_at + threadSet_pred_tcb_no_state + hoare_strengthen_post [OF cancelSignal_simple] + | simp add: o_def if_fun_split + | rule hoare_drop_imps + | clarsimp elim!: pred_tcb'_weakenE)+ + apply (auto simp: pred_tcb_at' + elim!: pred_tcb'_weakenE) + done + +lemma (in delete_one_conc_pre) cancelIPC_st_tcb_at': + "\st_tcb_at' P t' and K (t \ t')\ + cancelIPC t + \\rv. st_tcb_at' P t'\" + apply (simp add: cancelIPC_def Let_def getThreadReplySlot_def locateSlot_conv + capHasProperty_def isCap_simps) + apply (wp sts_pred_tcb_neq' hoare_drop_imps delete_one_reply_st_tcb_at + | wpc | clarsimp)+ + apply (wp getCTE_wp | clarsimp)+ + apply (wp hoare_vcg_ex_lift threadSet_cte_wp_at' hoare_vcg_imp_lift + cancelSignal_pred_tcb_at' sts_pred_tcb_neq' getEndpoint_wp gts_wp' + threadSet_pred_tcb_no_state + | wpc | clarsimp)+ + apply (auto simp: cte_wp_at_ctes_of isCap_simps) + done + +context begin interpretation Arch . +crunch typ_at'[wp]: emptySlot "\s. P (typ_at' T p s)" +end + +crunch tcb_at'[wp]: cancelSignal "tcb_at' t" + (wp: crunch_wps simp: crunch_simps) + +context delete_one_conc_pre +begin + +lemmas delete_one_typ_ats[wp] = typ_at_lifts [OF delete_one_typ_at] + +lemma cancelIPC_tcb_at'[wp]: + "\tcb_at' t\ cancelIPC t' \\_. tcb_at' t\" + apply (simp add: cancelIPC_def Let_def getThreadReplySlot_def) + apply (wp delete_one_typ_ats hoare_drop_imps + | simp add: o_def if_apply_def2 | wpc | assumption)+ + done + +end + +declare delete_remove1 [simp] +declare delete.simps [simp del] + +lemma invs_weak_sch_act_wf[elim!]: + "invs' s \ weak_sch_act_wf (ksSchedulerAction s) s" + apply (drule invs_sch_act_wf') + apply (clarsimp simp: weak_sch_act_wf_def) + done + +lemma blocked_cancel_ipc_corres: + "\ st = Structures_A.BlockedOnReceive epPtr p' \ + st = Structures_A.BlockedOnSend epPtr p; thread_state_relation st st' \ \ + corres dc (invs and st_tcb_at ((=) st) t) (invs' and st_tcb_at' ((=) st') t) + (blocked_cancel_ipc st t) + (do ep \ getEndpoint epPtr; + y \ assert (\ (case ep of IdleEP \ True | _ \ False)); + ep' \ + if remove1 t (epQueue ep) = [] then return IdleEP + else + return $ epQueue_update (%_. (remove1 t (epQueue ep))) ep; + y \ setEndpoint epPtr ep'; + setThreadState Structures_H.thread_state.Inactive t + od)" + apply (simp add: blocked_cancel_ipc_def gbep_ret) + apply (rule corres_guard_imp) + apply (rule corres_split [OF _ get_ep_corres]) + apply (rule_tac F="ep \ IdleEP" in corres_gen_asm2) + apply (rule corres_assert_assume[rotated]) + apply (clarsimp split: endpoint.splits) + apply (rule_tac P="invs and st_tcb_at ((=) st) t" and + P'="invs' and st_tcb_at' ((=) st') t" in corres_inst) + apply (case_tac rv) + apply (simp add: ep_relation_def) + apply (simp add: get_ep_queue_def ep_relation_def split del: if_split) + apply (rename_tac list) + apply (case_tac "remove1 t list") + apply simp + apply (rule corres_guard_imp) + apply (rule corres_split [OF _ set_ep_corres]) + apply (rule sts_corres) + apply simp + apply (simp add: ep_relation_def) + apply (simp add: valid_tcb_state_def pred_conj_def) + apply (wp weak_sch_act_wf_lift)+ + apply (clarsimp simp: st_tcb_at_tcb_at) + apply (clarsimp simp: st_tcb_at_def obj_at_def) + apply (erule pspace_valid_objsE) + apply fastforce + apply (auto simp: valid_tcb_state_def valid_tcb_def + valid_obj_def obj_at_def)[1] + apply (clarsimp simp: pred_tcb_at') + apply (clarsimp simp: pred_tcb_at'_def) + apply (drule obj_at_ko_at') + apply clarify + apply (drule ko_at_valid_objs') + apply fastforce + apply simp + apply (auto simp add: valid_obj'_def valid_tcb'_def + valid_tcb_state'_def)[1] + apply clarsimp + apply (rule corres_guard_imp) + apply (rule corres_split [OF _ set_ep_corres]) + apply (rule sts_corres) + apply simp + apply (simp add: ep_relation_def) + apply (wp)+ + apply (clarsimp simp: st_tcb_at_tcb_at) + apply (clarsimp simp: st_tcb_at_def obj_at_def) + apply (erule pspace_valid_objsE) + apply fastforce + apply (auto simp: valid_tcb_state_def valid_tcb_def + valid_obj_def obj_at_def)[1] + apply (clarsimp simp: pred_tcb_at') + apply (clarsimp simp: pred_tcb_at'_def) + apply (drule obj_at_ko_at') + apply clarify + apply (drule ko_at_valid_objs') + apply fastforce + apply simp + apply (auto simp add: valid_obj'_def valid_tcb'_def + valid_tcb_state'_def)[1] + apply (simp add: get_ep_queue_def ep_relation_def split del: if_split) + apply (rename_tac list) + apply (case_tac "remove1 t list") + apply simp + apply (rule corres_guard_imp) + apply (rule corres_split [OF _ set_ep_corres]) + apply (rule sts_corres) + apply simp + apply (simp add: ep_relation_def) + apply (simp add: valid_tcb_state_def pred_conj_def) + apply (wp weak_sch_act_wf_lift)+ + apply (clarsimp simp: st_tcb_at_tcb_at) + apply (clarsimp simp: st_tcb_at_def obj_at_def) + apply (erule pspace_valid_objsE) + apply fastforce + apply (auto simp: valid_tcb_state_def valid_tcb_def + valid_obj_def obj_at_def)[1] + apply (clarsimp simp: pred_tcb_at') + apply (clarsimp simp: pred_tcb_at'_def) + apply (drule obj_at_ko_at') + apply clarify + apply (drule ko_at_valid_objs') + apply fastforce + apply simp + apply (auto simp add: valid_obj'_def valid_tcb'_def + valid_tcb_state'_def)[1] + apply clarsimp + apply (rule corres_guard_imp) + apply (rule corres_split [OF _ set_ep_corres]) + apply (rule sts_corres) + apply simp + apply (simp add: ep_relation_def) + apply (wp)+ + apply (clarsimp simp: st_tcb_at_tcb_at) + apply (clarsimp simp: st_tcb_at_def obj_at_def) + apply (erule pspace_valid_objsE) + apply fastforce + apply (auto simp: valid_tcb_state_def valid_tcb_def + valid_obj_def obj_at_def)[1] + apply (clarsimp simp: pred_tcb_at') + apply (clarsimp simp: pred_tcb_at'_def) + apply (drule obj_at_ko_at') + apply clarify + apply (drule ko_at_valid_objs') + apply fastforce + apply simp + apply (auto simp add: valid_obj'_def valid_tcb'_def + valid_tcb_state'_def)[1] + apply (wp getEndpoint_wp)+ + apply (clarsimp simp: st_tcb_at_def obj_at_def) + apply (erule pspace_valid_objsE) + apply fastforce + apply (auto simp: valid_tcb_state_def valid_tcb_def + valid_obj_def obj_at_def)[1] + apply clarsimp + apply (rule conjI) + apply (clarsimp simp: pred_tcb_at'_def) + apply (drule obj_at_ko_at') + apply clarify + apply (drule ko_at_valid_objs') + apply fastforce + apply simp + apply (auto simp add: valid_obj'_def valid_tcb'_def + valid_tcb_state'_def)[1] + apply (fastforce simp: ko_wp_at'_def obj_at'_def dest: sym_refs_st_tcb_atD') + done + +lemma ac_corres: + "corres dc + (invs and st_tcb_at ((=) (Structures_A.BlockedOnNotification ntfn)) t) + (invs' and st_tcb_at' ((=) (BlockedOnNotification ntfn)) t) + (cancel_signal t ntfn) + (cancelSignal t ntfn)" + apply (simp add: cancel_signal_def cancelSignal_def Let_def) + apply (rule corres_guard_imp) + apply (rule corres_split [OF _ get_ntfn_corres]) + apply (rule_tac F="isWaitingNtfn (ntfnObj ntfnaa)" in corres_gen_asm2) + apply (case_tac "ntfn_obj ntfna") + apply (simp add: ntfn_relation_def isWaitingNtfn_def) + apply (simp add: isWaitingNtfn_def ntfn_relation_def split del: if_split) + apply (rename_tac list) + apply (rule_tac R="remove1 t list = []" in corres_cases) + apply (simp del: dc_simp) + apply (rule corres_split [OF _ set_ntfn_corres]) + apply (rule sts_corres) + apply simp + apply (simp add: ntfn_relation_def) + apply (wp)+ + apply (simp add: list_case_If del: dc_simp) + apply (rule corres_split [OF _ set_ntfn_corres]) + apply (rule sts_corres) + apply simp + apply (clarsimp simp add: ntfn_relation_def neq_Nil_conv) + apply (wp)+ + apply (simp add: isWaitingNtfn_def ntfn_relation_def) + apply (wp getNotification_wp)+ + apply (clarsimp simp: conj_comms st_tcb_at_tcb_at) + apply (clarsimp simp: st_tcb_at_def obj_at_def) + apply (rule conjI, fastforce) + apply (rule conjI, fastforce) + apply (erule pspace_valid_objsE) + apply fastforce + apply (clarsimp simp: valid_obj_def valid_tcb_def valid_tcb_state_def) + apply (drule sym, simp add: obj_at_def) + apply (clarsimp simp: conj_comms pred_tcb_at' cong: conj_cong) + apply (rule conjI) + apply (simp add: pred_tcb_at'_def) + apply (drule obj_at_ko_at') + apply clarsimp + apply (frule ko_at_valid_objs') + apply fastforce + apply simp + apply (clarsimp simp: valid_obj'_def valid_tcb'_def valid_tcb_state'_def) + apply (drule sym, simp) + apply (clarsimp simp: invs_weak_sch_act_wf) + apply (drule sym_refs_st_tcb_atD', fastforce) + apply (fastforce simp: isWaitingNtfn_def ko_wp_at'_def obj_at'_def + ntfn_bound_refs'_def + split: Structures_H.notification.splits ntfn.splits option.splits) + done + +lemma cte_map_tcb_2: + "cte_map (t, tcb_cnode_index 2) = t + 2*2^cte_level_bits" + by (simp add: cte_map_def tcb_cnode_index_def to_bl_1 shiftl_t2n) + +(* FIXME: Use one of these forms everywhere, rather than choosing at random. *) +lemmas cte_index_repair = mult.commute[where a="(2::'a::len word) ^ cte_level_bits"] +lemmas cte_index_repair_sym = cte_index_repair[symmetric] + +context begin interpretation Arch . (*FIXME: arch_split*) + +lemma cte_wp_at_master_reply_cap_to_ex_rights: + "cte_wp_at (is_master_reply_cap_to t) ptr + = (\s. \rights. cte_wp_at ((=) (cap.ReplyCap t True rights)) ptr s)" + by (rule ext, rule iffI; clarsimp simp: cte_wp_at_def is_master_reply_cap_to_def) + +lemma cte_wp_at_reply_cap_to_ex_rights: + "cte_wp_at (is_reply_cap_to t) ptr + = (\s. \rights. cte_wp_at ((=) (cap.ReplyCap t False rights)) ptr s)" + by (rule ext, rule iffI; clarsimp simp: cte_wp_at_def is_reply_cap_to_def) + +lemma reply_no_descendants_mdbNext_null: + assumes descs: "descendants_of (t, tcb_cnode_index 2) (cdt s) = {}" + and sr: "(s, s') \ state_relation" + and invs: "valid_reply_caps s" "valid_reply_masters s" + "valid_objs s" "valid_mdb s" "valid_mdb' s'" "pspace_aligned' s'" + "pspace_distinct' s'" + and tcb: "st_tcb_at (Not \ halted) t s" + and cte: "ctes_of s' (t + 2*2^cte_level_bits) = Some cte" + shows "mdbNext (cteMDBNode cte) = nullPointer" +proof - + from invs st_tcb_at_reply_cap_valid[OF tcb] + have "cte_wp_at (is_master_reply_cap_to t) (t, tcb_cnode_index 2) s" + by (fastforce simp: cte_wp_at_caps_of_state is_cap_simps is_master_reply_cap_to_def) + + hence "\r. cteCap cte = capability.ReplyCap t True r" + using invs sr + by (fastforce simp: cte_wp_at_master_reply_cap_to_ex_rights shiftl_t2n cte_index_repair + cte_wp_at_ctes_of cte cte_map_def tcb_cnode_index_def + dest: pspace_relation_cte_wp_at state_relation_pspace_relation) + + hence class_link: + "\cte'. ctes_of s' (mdbNext (cteMDBNode cte)) = Some cte' \ + capClass (cteCap cte') = ReplyClass t" + using invs + apply (clarsimp simp: valid_mdb'_def valid_mdb_ctes_def) + apply (drule class_linksD[where m="ctes_of s'", OF cte]) + apply (simp add: mdb_next_unfold cte) + apply assumption + apply simp + done + + from invs tcb descs have "\ptr m g. + cte_wp_at ((=) (cap.ReplyCap t m g)) ptr s \ ptr = (t, tcb_cnode_index 2)" + apply (intro allI impI) + apply (case_tac m) + apply (fastforce simp: invs_def valid_state_def valid_reply_masters_def + cte_wp_at_master_reply_cap_to_ex_rights) + apply (fastforce simp: has_reply_cap_def cte_wp_at_reply_cap_to_ex_rights + dest: reply_master_no_descendants_no_reply elim: st_tcb_at_tcb_at) + done + hence "\ptr m mdb r. + ctes_of s' ptr = Some (CTE (capability.ReplyCap t m r) mdb) \ ptr = t + 2*2^cte_level_bits" + using sr invs + apply (intro allI impI) + apply (drule(2) pspace_relation_cte_wp_atI + [OF state_relation_pspace_relation]) + apply (elim exE, case_tac c, simp_all del: split_paired_All) + apply (elim allE, erule impE, fastforce) + apply (clarsimp simp: cte_map_def tcb_cnode_index_def shiftl_t2n) + done + hence class_unique: + "\ptr cte'. ctes_of s' ptr = Some cte' \ + capClass (cteCap cte') = ReplyClass t \ + ptr = t + 2*2^cte_level_bits" + apply (intro allI impI) + apply (case_tac cte', rename_tac cap node, case_tac cap, simp_all) + apply (rename_tac arch_capability) + apply (case_tac arch_capability, simp_all) + done + + from invs have no_null: "ctes_of s' nullPointer = None" + by (clarsimp simp: no_0_def nullPointer_def valid_mdb'_def valid_mdb_ctes_def) + + from invs cte have no_loop: "mdbNext (cteMDBNode cte) \ t + 2*2^cte_level_bits" + by (fastforce simp: mdb_next_rel_def mdb_next_def + valid_mdb'_def + dest: valid_mdb_no_loops no_loops_direct_simp) + + from invs cte have + "mdbNext (cteMDBNode cte) \ nullPointer \ + (\cte'. ctes_of s' (mdbNext (cteMDBNode cte)) = Some cte')" + by (fastforce simp: valid_mdb'_def valid_mdb_ctes_def nullPointer_def + elim: valid_dlistEn) + hence + "mdbNext (cteMDBNode cte) \ nullPointer \ + mdbNext (cteMDBNode cte) = t + 2*2^cte_level_bits" + using class_link class_unique + by clarsimp + thus ?thesis + by (simp add: no_loop) +qed + +lemma reply_descendants_mdbNext_nonnull: + assumes descs: "descendants_of (t, tcb_cnode_index 2) (cdt s) \ {}" + and sr: "(s, s') \ state_relation" + and tcb: "st_tcb_at (Not \ halted) t s" + and cte: "ctes_of s' (t + 2*2^cte_level_bits) = Some cte" + shows "mdbNext (cteMDBNode cte) \ nullPointer" +proof - + from tcb have "cte_at (t, tcb_cnode_index 2) s" + by (simp add: st_tcb_at_tcb_at tcb_at_cte_at dom_tcb_cap_cases) + hence "descendants_of' (t + 2*2^cte_level_bits) (ctes_of s') \ {}" + using sr descs + by (fastforce simp: state_relation_def cdt_relation_def cte_map_def tcb_cnode_index_def shiftl_t2n mult_ac) + thus ?thesis + using cte unfolding nullPointer_def + by (fastforce simp: descendants_of'_def dest: subtree_next_0) +qed + +lemma reply_descendants_of_mdbNext: + "\ (s, s') \ state_relation; valid_reply_caps s; valid_reply_masters s; + valid_objs s; valid_mdb s; valid_mdb' s'; pspace_aligned' s'; + pspace_distinct' s'; st_tcb_at (Not \ halted) t s; + ctes_of s' (t + 2*2^cte_level_bits) = Some cte \ \ + (descendants_of (t, tcb_cnode_index 2) (cdt s) = {}) = + (mdbNext (cteMDBNode cte) = nullPointer)" + apply (case_tac "descendants_of (t, tcb_cnode_index 2) (cdt s) = {}") + apply (simp add: reply_no_descendants_mdbNext_null) + apply (simp add: reply_descendants_mdbNext_nonnull) + done + +lemma reply_mdbNext_is_descendantD: + assumes sr: "(s, s') \ state_relation" + and invs: "invs' s'" + and tcb: "tcb_at t s" + and cte: "ctes_of s' (t + 2*2^cte_level_bits) = Some cte" + and desc: "descendants_of (t, tcb_cnode_index 2) (cdt s) = {sl}" + shows "mdbNext (cteMDBNode cte) = cte_map sl" +proof - + from tcb have "cte_at (t, tcb_cnode_index 2) s" + by (simp add: tcb_at_cte_at dom_tcb_cap_cases) + hence "descendants_of' (t + 2*2^cte_level_bits) (ctes_of s') = {cte_map sl}" + using sr desc + by (fastforce simp: state_relation_def cdt_relation_def cte_map_def tcb_cnode_index_def shiftl_t2n mult_ac) + thus ?thesis + using cte invs + apply (clarsimp simp: descendants_of'_def) + apply (frule singleton_eqD, drule CollectD) + apply (erule subtree.cases) + apply (clarsimp simp: mdb_next_rel_def mdb_next_def) + apply (subgoal_tac "c' = cte_map sl") + apply (fastforce dest: invs_no_loops no_loops_direct_simp) + apply fastforce + done +qed +end + +locale delete_one_conc = delete_one_conc_pre + + assumes delete_one_invs: + "\p. \invs'\ cteDeleteOne p \\rv. invs'\" + +locale delete_one = delete_one_conc + delete_one_abs + + assumes delete_one_corres: + "corres dc (einvs and cte_wp_at can_fast_finalise ptr) + (invs' and cte_at' (cte_map ptr)) + (cap_delete_one ptr) (cteDeleteOne (cte_map ptr))" + +lemma (in delete_one) reply_cancel_ipc_corres: + "corres dc (einvs and st_tcb_at awaiting_reply t) + (invs' and st_tcb_at' awaiting_reply' t) + (reply_cancel_ipc t) + (do y \ threadSet (\tcb. tcb \ tcbFault := None \) t; + slot \ getThreadReplySlot t; + callerCap \ liftM (mdbNext \ cteMDBNode) (getCTE slot); + when (callerCap \ nullPointer) (do + y \ stateAssert (capHasProperty callerCap (\cap. isReplyCap cap + \ \ capReplyMaster cap)) + []; + cteDeleteOne callerCap + od) + od)" + proof - + interpret Arch . (*FIXME: arch_split*) + show ?thesis + apply (simp add: reply_cancel_ipc_def getThreadReplySlot_def + locateSlot_conv liftM_def tcbReplySlot_def + del: split_paired_Ex) + apply (rule_tac Q="\_. invs and valid_list and valid_sched and st_tcb_at awaiting_reply t" + and Q'="\_. invs' and st_tcb_at' awaiting_reply' t" + in corres_split') + apply (rule corres_guard_imp) + apply (rule threadset_corresT) + apply (simp add: tcb_relation_def fault_rel_optionation_def) + apply (simp add: tcb_cap_cases_def) + apply (simp add: tcb_cte_cases_def cteSizeBits_def) + apply (simp add: exst_same_def) + apply (fastforce simp: st_tcb_at_tcb_at) + apply clarsimp + defer + apply (wp thread_set_invs_trivial thread_set_no_change_tcb_state + threadSet_invs_trivial threadSet_pred_tcb_no_state thread_set_not_state_valid_sched + | fastforce simp: tcb_cap_cases_def inQ_def + | wp (once) sch_act_simple_lift)+ + apply (rule corres_split') + apply (rule corres_guard_imp) + apply (rule get_cap_corres [where cslot_ptr="(t, tcb_cnode_index 2)", + simplified cte_map_tcb_2 cte_index_repair_sym]) + apply (clarsimp dest!: st_tcb_at_tcb_at + tcb_at_cte_at [where ref="tcb_cnode_index 2"]) + apply (clarsimp simp: invs'_def valid_state'_def valid_pspace'_def) + defer + apply (rule hoare_vcg_conj_lift [OF get_cap_inv get_cap_cte_wp_at, simplified]) + apply (rule hoare_vcg_conj_lift [OF getCTE_inv getCTE_cte_wp_at, simplified]) + apply (rename_tac cte) + apply (rule corres_symb_exec_l [OF _ _ gets_sp]) + apply (rule_tac F="\r. cap = cap.ReplyCap t True r \ + cteCap cte = capability.ReplyCap t True (AllowGrant \ r)" in corres_req) + apply (fastforce simp: cte_wp_at_caps_of_state is_cap_simps + dest!: st_tcb_at_reply_cap_valid) + apply (rule_tac F="(descs = {}) = (mdbNext (cteMDBNode cte) = nullPointer)" + in corres_req) + apply (fastforce simp: st_tcb_at_tcb_at cte_wp_at_ctes_of st_tcb_def2 cte_index_repair + dest: reply_descendants_of_mdbNext) + apply (elim exE) + apply (case_tac "descs = {}", simp add: when_def) + apply (rule_tac F="\sl. descs = {sl}" in corres_req) + apply (fastforce intro: st_tcb_at_tcb_at dest: reply_master_one_descendant) + apply (erule exE, frule singleton_eqD) + apply (rule_tac F="mdbNext (cteMDBNode cte) = cte_map sl" in corres_req) + apply (clarsimp dest!: st_tcb_at_tcb_at) + apply (fastforce simp: cte_wp_at_ctes_of cte_level_bits_def + elim!: reply_mdbNext_is_descendantD) + apply (simp add: when_def getSlotCap_def capHasProperty_def + del: split_paired_Ex) + apply (rule corres_guard_imp) + apply (rule_tac P'="\s. \r'. cte_wp_at ((=) (cap.ReplyCap t False r')) sl s" + in corres_stateAssert_implied [OF delete_one_corres]) + apply (fastforce dest: pspace_relation_cte_wp_at + state_relation_pspace_relation + simp: cte_wp_at_ctes_of isCap_simps) + apply (fastforce simp: invs_def valid_state_def valid_mdb_def reply_mdb_def + reply_masters_mdb_def cte_wp_at_caps_of_state + can_fast_finalise_def) + apply (fastforce simp: valid_mdb'_def valid_mdb_ctes_def + cte_wp_at_ctes_of nullPointer_def + elim: valid_dlistEn dest: invs_mdb') + apply (simp add: exs_valid_def gets_def get_def return_def bind_def + del: split_paired_Ex split_paired_All) + apply (wp) + done +qed + +lemma (in delete_one) cancel_ipc_corres: + "corres dc (einvs and tcb_at t) (invs' and tcb_at' t) + (cancel_ipc t) (cancelIPC t)" + apply (simp add: cancel_ipc_def cancelIPC_def Let_def) + apply (rule corres_guard_imp) + apply (rule corres_split [OF _ gts_corres]) + apply (rule_tac P="einvs and st_tcb_at ((=) state) t" and + P'="invs' and st_tcb_at' ((=) statea) t" in corres_inst) + apply (case_tac state, simp_all add: isTS_defs list_case_If)[1] + apply (rule corres_guard_imp) + apply (rule blocked_cancel_ipc_corres) + apply fastforce + apply fastforce + apply simp + apply simp + apply (clarsimp simp add: isTS_defs list_case_If) + apply (rule corres_guard_imp) + apply (rule blocked_cancel_ipc_corres) + apply fastforce + apply fastforce + apply simp + apply simp + apply (rule corres_guard_imp) + apply (rule reply_cancel_ipc_corres) + apply (clarsimp elim!: st_tcb_weakenE) + apply (clarsimp elim!: pred_tcb'_weakenE) + apply (rule corres_guard_imp [OF ac_corres], simp+) + apply (wp gts_sp[where P="\",simplified])+ + apply (rule hoare_strengthen_post) + apply (rule gts_sp'[where P="\"]) + apply (clarsimp elim!: pred_tcb'_weakenE) + apply fastforce + apply simp + done + +lemma setNotification_utr[wp]: + "\untyped_ranges_zero'\ setNotification ntfn nobj \\rv. untyped_ranges_zero'\" + apply (simp add: cteCaps_of_def) + apply (rule hoare_pre, wp untyped_ranges_zero_lift) + apply (simp add: o_def) + done + +crunch gsUntypedZeroRanges[wp]: setEndpoint "\s. P (gsUntypedZeroRanges s)" + (ignore: setObject wp: setObject_ksPSpace_only updateObject_default_inv) + +lemma setEndpoint_utr[wp]: + "\untyped_ranges_zero'\ setEndpoint p ep \\rv. untyped_ranges_zero'\" + apply (simp add: cteCaps_of_def) + apply (rule hoare_pre, wp untyped_ranges_zero_lift) + apply (simp add: o_def) + done + +declare cart_singleton_empty [simp] +declare cart_singleton_empty2[simp] + +crunch ksQ[wp]: setNotification "\s. P (ksReadyQueues s p)" + (wp: setObject_queues_unchanged_tcb updateObject_default_inv) + +lemma sch_act_simple_not_t[simp]: "sch_act_simple s \ sch_act_not t s" + by (clarsimp simp: sch_act_simple_def) + +context begin interpretation Arch . (*FIXME: arch_split*) + +lemma cancelSignal_invs': + "\invs' and st_tcb_at' (\st. st = BlockedOnNotification ntfn) t and sch_act_not t\ + cancelSignal t ntfn \\rv. invs'\" + proof - + have NIQ: "\s. \ Invariants_H.valid_queues s; st_tcb_at' (Not \ runnable') t s \ + \ \x. t \ set (ksReadyQueues s x)" + apply (clarsimp simp add: pred_tcb_at'_def Invariants_H.valid_queues_def + valid_queues_no_bitmap_def) + apply (drule spec | drule(1) bspec | clarsimp simp: obj_at'_def inQ_def)+ + done + have NTFNSN: "\ntfn ntfn'. + \\s. sch_act_not (ksCurThread s) s \ setNotification ntfn ntfn' + \\_ s. sch_act_not (ksCurThread s) s\" + apply (rule hoare_weaken_pre) + apply (wps setNotification_ksCurThread) + apply (wp, simp) + done + show ?thesis + apply (simp add: cancelSignal_def invs'_def valid_state'_def Let_def) + apply (wp valid_irq_node_lift sts_sch_act' irqs_masked_lift + hoare_vcg_all_lift [OF setNotification_ksQ] sts_valid_queues + setThreadState_ct_not_inQ NTFNSN + hoare_vcg_all_lift setNotification_ksQ + | simp add: valid_tcb_state'_def list_case_If split del: if_split)+ + prefer 2 + apply assumption + apply (rule hoare_strengthen_post) + apply (rule get_ntfn_sp') + apply (clarsimp simp: pred_tcb_at') + apply (frule NIQ) + apply (clarsimp simp: pred_tcb_at'_def obj_at'_def) + apply (rule conjI) + apply (clarsimp simp: valid_ntfn'_def) + apply (case_tac "ntfnObj r", simp_all add: isWaitingNtfn_def) + apply (frule ko_at_valid_objs') + apply (simp add: valid_pspace_valid_objs') + apply (clarsimp simp: projectKO_opt_ntfn split: kernel_object.splits) + apply (simp add: valid_obj'_def valid_ntfn'_def) + apply (frule st_tcb_at_state_refs_ofD') + apply (frule ko_at_state_refs_ofD') + apply (rule conjI, erule delta_sym_refs) + apply (clarsimp simp: ntfn_bound_refs'_def split: if_split_asm) + apply (clarsimp split: if_split_asm) + subgoal + by (safe; simp add: ntfn_bound_refs'_def tcb_bound_refs'_def + obj_at'_def tcb_ntfn_is_bound'_def + split: option.splits) + subgoal + by (fastforce simp: symreftype_inverse' ntfn_bound_refs'_def + tcb_bound_refs'_def) + subgoal + by (fastforce simp: symreftype_inverse' ntfn_bound_refs'_def + tcb_bound_refs'_def ntfn_q_refs_of'_def remove1_empty + split: ntfn.splits) + apply (rule conjI, clarsimp elim!: if_live_state_refsE) + apply (fastforce simp: sym_refs_def dest!: idle'_no_refs) + apply (case_tac "ntfnObj r", simp_all) + apply (frule obj_at_valid_objs', clarsimp) + apply (clarsimp simp: valid_obj'_def valid_ntfn'_def) + apply (rule conjI, clarsimp split: option.splits) + apply (frule st_tcb_at_state_refs_ofD') + apply (frule ko_at_state_refs_ofD') + apply (rule conjI) + apply (erule delta_sym_refs) + apply (fastforce simp: ntfn_bound_refs'_def split: if_split_asm) + apply (clarsimp split: if_split_asm) + apply (fastforce simp: symreftype_inverse' ntfn_bound_refs'_def tcb_bound_refs'_def + set_eq_subset) + apply (fastforce simp: symreftype_inverse' ntfn_bound_refs'_def tcb_bound_refs'_def + set_eq_subset) + apply (rule conjI, clarsimp elim!: if_live_state_refsE) + apply (rule conjI) + apply (case_tac "ntfnBoundTCB r") + apply (clarsimp elim!: if_live_state_refsE)+ + apply (rule conjI, clarsimp split: option.splits) + apply (clarsimp dest!: idle'_no_refs) + done + qed + +lemmas setEndpoint_valid_arch[wp] + = valid_arch_state_lift' [OF setEndpoint_typ_at' set_ep_arch'] + +lemma ep_redux_simps3: + "ep_q_refs_of' (case xs of [] \ IdleEP | y # ys \ RecvEP (y # ys)) + = (set xs \ {EPRecv})" + "ep_q_refs_of' (case xs of [] \ IdleEP | y # ys \ SendEP (y # ys)) + = (set xs \ {EPSend})" + by (fastforce split: list.splits simp: valid_ep_def valid_ntfn_def)+ + +declare setEndpoint_ksMachine [wp] +declare setEndpoint_valid_irq_states' [wp] + +lemma setEndpoint_vms[wp]: + "\valid_machine_state'\ setEndpoint epptr ep' \\_. valid_machine_state'\" + by (simp add: valid_machine_state'_def pointerInUserData_def pointerInDeviceData_def) + (wp hoare_vcg_all_lift hoare_vcg_disj_lift) + +crunch ksQ[wp]: setEndpoint "\s. P (ksReadyQueues s p)" + (wp: setObject_queues_unchanged_tcb updateObject_default_inv) + +crunch sch_act_not[wp]: setEndpoint "sch_act_not t" + +crunch ksCurDomain[wp]: setEndpoint "\s. P (ksCurDomain s)" + (wp: setObject_ep_cur_domain ignore: setObject) + +lemma setEndpoint_ksDomSchedule[wp]: + "\\s. P (ksDomSchedule s)\ setEndpoint ptr ep \\_ s. P (ksDomSchedule s)\" + apply (simp add: setEndpoint_def setObject_def split_def) + apply (wp updateObject_default_inv | simp)+ + done + +lemma setEndpoint_ct_idle_or_in_cur_domain'[wp]: + "\ ct_idle_or_in_cur_domain' \ setEndpoint ptr ep \ \_. ct_idle_or_in_cur_domain' \" + apply (rule ct_idle_or_in_cur_domain'_lift) + apply (wp hoare_vcg_disj_lift hoare_vcg_imp_lift setObject_ep_ct + | rule obj_at_setObject2 + | clarsimp simp: updateObject_default_def in_monad setEndpoint_def)+ + done + +lemma setEndpoint_ct_not_inQ[wp]: + "\ct_not_inQ\ setEndpoint eeptr ep' \\_. ct_not_inQ\" + apply (rule ct_not_inQ_lift [OF setEndpoint_nosch]) + apply (simp add: setEndpoint_def) + apply (rule hoare_weaken_pre) + apply (wps setObject_ep_ct) + apply (wp obj_at_setObject2) + apply (clarsimp simp: updateObject_default_def in_monad)+ + done + +lemma setEndpoint_ksDomScheduleIdx[wp]: + "\\s. P (ksDomScheduleIdx s)\ setEndpoint ptr ep \\_ s. P (ksDomScheduleIdx s)\" + apply (simp add: setEndpoint_def setObject_def split_def) + apply (wp updateObject_default_inv | simp)+ + done +end + +lemma (in delete_one_conc) cancelIPC_invs[wp]: + shows "\tcb_at' t and invs'\ cancelIPC t \\rv. invs'\" +proof - + have P: "\xs v f. (case xs of [] \ return v | y # ys \ return (f (y # ys))) + = return (case xs of [] \ v | y # ys \ f xs)" + by (clarsimp split: list.split) + have NIQ: "\s. \ Invariants_H.valid_queues s; st_tcb_at' (Not \ runnable') t s \ + \ \x. t \ set (ksReadyQueues s x)" + apply (clarsimp simp add: pred_tcb_at'_def Invariants_H.valid_queues_def valid_queues_no_bitmap_def) + apply (drule spec | drule(1) bspec | clarsimp simp: obj_at'_def inQ_def)+ + done + have EPSCHN: "\eeptr ep'. \\s. sch_act_not (ksCurThread s) s\ + setEndpoint eeptr ep' + \\_ s. sch_act_not (ksCurThread s) s\" + apply (rule hoare_weaken_pre) + apply (wps setEndpoint_ct') + apply (wp, simp) + done + have Q: + "\epptr. \st_tcb_at' (\st. \a. (st = BlockedOnReceive epptr a) + \ (\a b c d. st = BlockedOnSend epptr a b c d)) t + and invs'\ + do ep \ getEndpoint epptr; + y \ assert (\ (case ep of IdleEP \ True | _ \ False)); + ep' \ case remove1 t (epQueue ep) + of [] \ return Structures_H.endpoint.IdleEP + | x # xs \ return (epQueue_update (%_. x # xs) ep); + y \ setEndpoint epptr ep'; + setThreadState Inactive t + od \\rv. invs'\" + apply (simp add: invs'_def valid_state'_def) + apply (subst P) + apply (wp valid_irq_node_lift valid_global_refs_lift' valid_arch_state_lift' + irqs_masked_lift sts_sch_act' + hoare_vcg_all_lift [OF setEndpoint_ksQ] + sts_valid_queues setThreadState_ct_not_inQ EPSCHN + hoare_vcg_all_lift setNotification_ksQ + | simp add: valid_tcb_state'_def split del: if_split + | wpc)+ + prefer 2 + apply assumption + apply (rule hoare_strengthen_post [OF get_ep_sp']) + apply (clarsimp simp: pred_tcb_at' fun_upd_def[symmetric] conj_comms + split del: if_split cong: if_cong) + apply (rule conjI, clarsimp simp: valid_idle'_def pred_tcb_at'_def obj_at'_def projectKOs) + apply (frule obj_at_valid_objs', clarsimp) + apply (clarsimp simp: projectKOs valid_obj'_def) + apply (rule conjI) + apply (clarsimp simp: obj_at'_def valid_ep'_def projectKOs + dest!: pred_tcb_at') + apply (frule NIQ) + apply (erule pred_tcb'_weakenE, fastforce) + apply (clarsimp, rule conjI) + apply (auto simp: pred_tcb_at'_def obj_at'_def)[1] + apply (rule conjI) + apply (clarsimp split: Structures_H.endpoint.split_asm list.split + simp: valid_ep'_def) + apply (rename_tac list x xs) + apply (frule distinct_remove1[where x=t]) + apply (cut_tac xs=list in set_remove1_subset[where x=t]) + apply auto[1] + apply (rename_tac list x xs) + apply (frule distinct_remove1[where x=t]) + apply (cut_tac xs=list in set_remove1_subset[where x=t]) + apply auto[1] + apply (frule(1) sym_refs_ko_atD') + apply (rule conjI) + apply (clarsimp elim!: if_live_state_refsE split: Structures_H.endpoint.split_asm) + apply (drule st_tcb_at_state_refs_ofD') + apply (clarsimp simp: ep_redux_simps3 valid_ep'_def + split: Structures_H.endpoint.split_asm + cong: list.case_cong) + apply (frule_tac x=t in distinct_remove1) + apply (frule_tac x=t in set_remove1_eq) + by (auto elim!: delta_sym_refs + simp: symreftype_inverse' tcb_st_refs_of'_def tcb_bound_refs'_def + split: thread_state.splits if_split_asm) + have R: + "\invs' and tcb_at' t\ + do y \ threadSet (\tcb. tcb \ tcbFault := None \) t; + slot \ getThreadReplySlot t; + callerCap \ liftM (mdbNext \ cteMDBNode) (getCTE slot); + when (callerCap \ nullPointer) (do + y \ stateAssert (capHasProperty callerCap (\cap. isReplyCap cap + \ \ capReplyMaster cap)) + []; + cteDeleteOne callerCap + od) + od + \\rv. invs'\" + unfolding getThreadReplySlot_def + by (wp valid_irq_node_lift delete_one_invs hoare_drop_imps + threadSet_invs_trivial irqs_masked_lift + | simp add: o_def if_apply_def2 + | fastforce simp: inQ_def)+ + show ?thesis + apply (simp add: cancelIPC_def crunch_simps + cong: if_cong list.case_cong) + apply (rule hoare_seq_ext [OF _ gts_sp']) + apply (case_tac state, + simp_all add: isTS_defs) + apply (safe intro!: hoare_weaken_pre[OF Q] + hoare_weaken_pre[OF R] + hoare_weaken_pre[OF return_wp] + hoare_weaken_pre[OF cancelSignal_invs'] + elim!: pred_tcb'_weakenE) + apply (auto simp: pred_tcb_at'_def obj_at'_def + dest: invs_sch_act_wf') + done +qed + +lemma (in delete_one_conc_pre) cancelIPC_sch_act_simple[wp]: + "\sch_act_simple\ + cancelIPC t + \\rv. sch_act_simple\" + apply (simp add: cancelIPC_def cancelSignal_def Let_def + cong: if_cong Structures_H.thread_state.case_cong) + apply (wp hoare_drop_imps delete_one_sch_act_simple + | simp add: getThreadReplySlot_def | wpcw + | rule sch_act_simple_lift + | (rule_tac Q="\rv. sch_act_simple" in hoare_post_imp, simp))+ + done + +lemma cancelSignal_st_tcb_at: + assumes x[simp]: "P Inactive" shows + "\st_tcb_at' P t\ + cancelSignal t' ntfn + \\rv. st_tcb_at' P t\" + apply (simp add: cancelSignal_def Let_def list_case_If) + apply (wp sts_st_tcb_at'_cases hoare_vcg_const_imp_lift + hoare_drop_imp[where R="%rv s. P' rv" for P']) + apply clarsimp+ + done + +lemma (in delete_one_conc_pre) cancelIPC_st_tcb_at: + assumes x[simp]: "\st. simple' st \ P st" shows + "\st_tcb_at' P t\ + cancelIPC t' + \\rv. st_tcb_at' P t\" + apply (simp add: cancelIPC_def Let_def getThreadReplySlot_def + cong: if_cong Structures_H.thread_state.case_cong) + apply (rule hoare_seq_ext [OF _ gts_sp']) + apply (case_tac x, simp_all add: isTS_defs list_case_If) + apply (wp sts_st_tcb_at'_cases delete_one_st_tcb_at + threadSet_pred_tcb_no_state + cancelSignal_st_tcb_at hoare_drop_imps + | clarsimp simp: o_def if_fun_split)+ + done + +lemma weak_sch_act_wf_lift_linear: + "\ \t. \\s. sa s \ SwitchToThread t\ f \\rv s. sa s \ SwitchToThread t\; + \t. \st_tcb_at' runnable' t\ f \\rv. st_tcb_at' runnable' t\; + \t. \tcb_in_cur_domain' t\ f \\rv. tcb_in_cur_domain' t\ \ + \ \\s. weak_sch_act_wf (sa s) s\ f \\rv s. weak_sch_act_wf (sa s) s\" + apply (simp only: weak_sch_act_wf_def imp_conv_disj) + apply (intro hoare_vcg_all_lift hoare_vcg_disj_lift hoare_vcg_conj_lift) + apply simp_all + done + +lemma sts_sch_act_not[wp]: + "\sch_act_not t\ setThreadState st t' \\rv. sch_act_not t\" + apply (simp add: setThreadState_def rescheduleRequired_def) + apply (wp hoare_drop_imps | simp | wpcw)+ + done + +crunch sch_act_not[wp]: cancelSignal, setBoundNotification "sch_act_not t" + (wp: crunch_wps) + +lemma cancelSignal_tcb_at_runnable': + "t \ t' \ + \st_tcb_at' runnable' t'\ cancelSignal t ntfnptr \\_. st_tcb_at' runnable' t'\" + unfolding cancelSignal_def + by (wpsimp wp: sts_pred_tcb_neq' hoare_drop_imp) + +lemma cancelAllIPC_tcb_at_runnable': + "\st_tcb_at' runnable' t\ cancelAllIPC epptr \\_. st_tcb_at' runnable' t\" + unfolding cancelAllIPC_def + by (wpsimp wp: mapM_x_wp' sts_st_tcb' hoare_drop_imp) + +lemma cancelAllSignals_tcb_at_runnable': + "\st_tcb_at' runnable' t\ cancelAllSignals ntfnptr \\_. st_tcb_at' runnable' t\" + unfolding cancelAllSignals_def + by (wpsimp wp: mapM_x_wp' sts_st_tcb' hoare_drop_imp) + +crunch st_tcb_at'[wp]: unbindNotification, bindNotification, unbindMaybeNotification "st_tcb_at' P p" +(wp: threadSet_pred_tcb_no_state ignore: threadSet) + +lemma (in delete_one_conc_pre) finaliseCap_tcb_at_runnable': + "\st_tcb_at' runnable' t\ finaliseCap cap final True \\_. st_tcb_at' runnable' t\" + apply (clarsimp simp add: finaliseCap_def Let_def) + apply (rule conjI | clarsimp | wp cancelAllIPC_tcb_at_runnable' getObject_ntfn_inv + cancelAllSignals_tcb_at_runnable' + | wpc)+ + done + +crunch pred_tcb_at'[wp]: isFinalCapability "pred_tcb_at' proj st t" + (simp: crunch_simps) + +lemma (in delete_one_conc_pre) cteDeleteOne_tcb_at_runnable': + "\st_tcb_at' runnable' t\ cteDeleteOne callerCap \\_. st_tcb_at' runnable' t\" + apply (simp add: cteDeleteOne_def unless_def) + apply (wp finaliseCap_tcb_at_runnable' hoare_drop_imps | clarsimp)+ + done + +crunch pred_tcb_at'[wp]: getThreadReplySlot, getEndpoint "pred_tcb_at' proj st t" + +lemma (in delete_one_conc_pre) cancelIPC_tcb_at_runnable': + "\st_tcb_at' runnable' t'\ cancelIPC t \\_. st_tcb_at' runnable' t'\" + (is "\?PRE\ _ \_\") + apply (clarsimp simp: cancelIPC_def Let_def) + apply (case_tac "t'=t") + apply (rule_tac B="\st. st_tcb_at' runnable' t and K (runnable' st)" + in hoare_seq_ext) + apply (case_tac x; simp) + apply (wp sts_pred_tcb_neq' | simp | wpc)+ + apply (clarsimp) + apply (rule_tac Q="\rv. ?PRE" in hoare_post_imp, fastforce) + apply (wp cteDeleteOne_tcb_at_runnable' + threadSet_pred_tcb_no_state + cancelSignal_tcb_at_runnable' + sts_pred_tcb_neq' hoare_drop_imps + | wpc | simp add: o_def if_fun_split)+ + done + +crunch ksCurDomain[wp]: cancelSignal "\s. P (ksCurDomain s)" + (wp: crunch_wps) + +lemma (in delete_one_conc_pre) cancelIPC_ksCurDomain[wp]: + "\\s. P (ksCurDomain s)\ cancelIPC t \\_ s. P (ksCurDomain s)\" + unfolding cancelIPC_def Let_def + by (wpsimp wp: hoare_vcg_conj_lift delete_one_ksCurDomain hoare_drop_imps + simp: getThreadReplySlot_def o_def if_fun_split) + +(* FIXME move *) +lemma setBoundNotification_not_ntfn: + "(\tcb ntfn. P (tcb\tcbBoundNotification := ntfn\) \ P tcb) + \ \obj_at' P t'\ setBoundNotification ntfn t \\_. obj_at' P t'\" + apply (simp add: setBoundNotification_def) + apply (wp hoare_vcg_conj_lift + | wpc + | rule hoare_drop_imps + | simp)+ + done + +lemma setBoundNotification_tcb_in_cur_domain'[wp]: + "\tcb_in_cur_domain' t'\ setBoundNotification st t \\_. tcb_in_cur_domain' t'\" + apply (simp add: tcb_in_cur_domain'_def) + apply (rule hoare_pre) + apply wps + apply (wp setBoundNotification_not_ntfn | simp)+ + done + +lemma cancelSignal_tcb_obj_at': + "(\tcb st qd. P (tcb\tcbState := st, tcbQueued := qd\) \ P tcb) + \ \obj_at' P t'\ cancelSignal t word \\_. obj_at' P t'\" + apply (simp add: cancelSignal_def setNotification_def) + apply (wp setThreadState_not_st getNotification_wp | wpc | simp)+ + done + +lemma (in delete_one_conc_pre) cancelIPC_tcbDomain_obj_at': + "\obj_at' (\tcb. P (tcbDomain tcb)) t'\ cancelIPC t \\_. obj_at' (\tcb. P (tcbDomain tcb)) t'\" + apply (simp add: cancelIPC_def Let_def) + apply (wp hoare_vcg_conj_lift + setThreadState_not_st delete_one_tcbDomain_obj_at' cancelSignal_tcb_obj_at' + | wpc + | rule hoare_drop_imps + | simp add: getThreadReplySlot_def o_def if_fun_split)+ + done + +lemma (in delete_one_conc_pre) cancelIPC_tcb_in_cur_domain': + "\tcb_in_cur_domain' t'\ cancelIPC t \\_. tcb_in_cur_domain' t'\" + apply (simp add: tcb_in_cur_domain'_def) + apply (rule hoare_pre) + apply wps + apply (wp cancelIPC_tcbDomain_obj_at' | simp)+ + done + +lemma (in delete_one_conc_pre) cancelIPC_sch_act_not: + "\sch_act_not t'\ cancelIPC t \\_. sch_act_not t'\" + apply (simp add: cancelIPC_def Let_def) + apply (wp hoare_vcg_conj_lift + delete_one_sch_act_not + | wpc + | simp add: getThreadReplySlot_def o_def if_apply_def2 + split del: if_split + | rule hoare_drop_imps)+ + done + +lemma (in delete_one_conc_pre) cancelIPC_weak_sch_act_wf: + "\\s. weak_sch_act_wf (ksSchedulerAction s) s\ + cancelIPC t + \\rv s. weak_sch_act_wf (ksSchedulerAction s) s\" + apply (rule weak_sch_act_wf_lift_linear) + apply (wp cancelIPC_sch_act_not cancelIPC_tcb_in_cur_domain' cancelIPC_tcb_at_runnable')+ + done + +text \The suspend operation, significant as called from delete\ + +lemma rescheduleRequired_weak_sch_act_wf: + "\\\ rescheduleRequired \\rv s. weak_sch_act_wf (ksSchedulerAction s) s\" + apply (simp add: rescheduleRequired_def setSchedulerAction_def) + apply (wp hoare_post_taut | simp add: weak_sch_act_wf_def)+ + done + +lemma sts_weak_sch_act_wf[wp]: + "\\s. weak_sch_act_wf (ksSchedulerAction s) s + \ (ksSchedulerAction s = SwitchToThread t \ runnable' st)\ + setThreadState st t + \\_ s. weak_sch_act_wf (ksSchedulerAction s) s\" + including no_pre + apply (simp add: setThreadState_def) + apply (wp rescheduleRequired_weak_sch_act_wf) + apply (rule_tac Q="\_ s. weak_sch_act_wf (ksSchedulerAction s) s" in hoare_post_imp, simp) + apply (simp add: weak_sch_act_wf_def) + apply (wp hoare_vcg_all_lift) + apply (wps threadSet_nosch) + apply (wp hoare_vcg_const_imp_lift threadSet_pred_tcb_at_state threadSet_tcbDomain_triv | simp)+ + done + +lemma sbn_nosch[wp]: + "\\s. P (ksSchedulerAction s)\ setBoundNotification ntfn t \\rv s. P (ksSchedulerAction s)\" + by (simp add: setBoundNotification_def, wp threadSet_nosch) + + +lemma sbn_weak_sch_act_wf[wp]: + "\\s. weak_sch_act_wf (ksSchedulerAction s) s\ + setBoundNotification ntfn t + \\_ s. weak_sch_act_wf (ksSchedulerAction s) s\" + by (wp weak_sch_act_wf_lift sbn_st_tcb') + + +lemma set_ep_weak_sch_act_wf[wp]: + "\\s. weak_sch_act_wf (ksSchedulerAction s) s\ + setEndpoint epptr ep + \\rv s. weak_sch_act_wf (ksSchedulerAction s) s\" + apply (wp weak_sch_act_wf_lift) + done + +lemma setObject_ntfn_sa_unchanged[wp]: + "\\s. P (ksSchedulerAction s)\ + setObject ptr (ntfn::Structures_H.notification) + \\rv s. P (ksSchedulerAction s)\" + apply (simp add: setObject_def split_def) + apply (wp | simp add: updateObject_default_def)+ + done + +lemma setObject_oa_unchanged[wp]: + "\\s. obj_at' (\tcb::tcb. P tcb) t s\ + setObject ptr (ntfn::Structures_H.notification) + \\rv s. obj_at' P t s\" + apply (rule obj_at_setObject2) + apply (clarsimp simp add: updateObject_type + updateObject_default_def + in_monad) + done + +lemma setNotification_weak_sch_act_wf[wp]: + "\\s. weak_sch_act_wf (ksSchedulerAction s) s\ + setNotification ntfnptr ntfn + \\_ s. weak_sch_act_wf (ksSchedulerAction s) s\" + apply (wp hoare_vcg_all_lift hoare_convert_imp hoare_vcg_conj_lift + | simp add: setNotification_def weak_sch_act_wf_def st_tcb_at'_def tcb_in_cur_domain'_def)+ + apply (rule hoare_pre) + apply (wps setObject_ntfn_cur_domain) + apply (wp setObject_ntfn_obj_at'_tcb | simp add: o_def)+ + done + +lemmas ipccancel_weak_sch_act_wfs + = weak_sch_act_wf_lift[OF _ setCTE_pred_tcb_at'] + +lemma tcbSchedDequeue_corres': + "corres dc (is_etcb_at t and tcb_at t and pspace_aligned and pspace_distinct) + (valid_inQ_queues) + (tcb_sched_action (tcb_sched_dequeue) t) (tcbSchedDequeue t)" + apply (rule corres_cross_over_guard[where P'=P' and Q="tcb_at' t and P'" for P']) + apply (fastforce simp: tcb_at_cross dest: state_relation_pspace_relation) + apply (simp only: tcbSchedDequeue_def tcb_sched_action_def) + apply (rule corres_symb_exec_r[OF _ _ threadGet_inv, where Q'="\rv. tcb_at' t and valid_inQ_queues and obj_at' (\obj. tcbQueued obj = rv) t"]) + defer + apply (wp threadGet_obj_at', simp, simp) + apply (wp, simp) + apply (case_tac queued) + defer + apply (simp add: unless_def when_def) + apply (rule corres_no_failI) + apply (wp) + apply (clarsimp simp: in_monad ethread_get_def get_etcb_def set_tcb_queue_def is_etcb_at_def state_relation_def gets_the_def gets_def get_def return_def bind_def assert_opt_def get_tcb_queue_def modify_def put_def) + apply (subgoal_tac "t \ set (ready_queues a (tcb_domain y) (tcb_priority y))") + prefer 2 + apply (force simp: tcb_sched_dequeue_def valid_inQ_queues_def + ready_queues_relation_def obj_at'_def inQ_def project_inject) + apply (simp add: ready_queues_relation_def) + apply (simp add: unless_def when_def) + apply (rule corres_guard_imp) + apply (rule corres_split[where r'="(=)", OF _ ethreadget_corres]) + apply (simp split del: if_split) + apply (rule corres_split_eqr[OF _ ethreadget_corres]) + apply (rule corres_split_eqr[OF _ getQueue_corres]) + apply (simp split del: if_split) + apply (subst bind_return_unit, rule corres_split[where r'=dc]) + apply (rule corres_split_noop_rhs) + apply (simp add: dc_def[symmetric]) + apply (rule threadSet_corres_noop, simp_all add: tcb_relation_def exst_same_def)[1] + apply (clarsimp, rule removeFromBitmap_corres_noop) + apply wp + apply (simp add: tcb_sched_dequeue_def) + apply (rule setQueue_corres) + apply (wp | simp add: etcb_relation_def)+ + done + +lemma setQueue_valid_inQ_queues: + "\valid_inQ_queues + and (\s. \t \ set ts. obj_at' (inQ d p) t s) + and K (distinct ts)\ + setQueue d p ts + \\_. valid_inQ_queues\" + apply (simp add: setQueue_def valid_inQ_queues_def) + apply wp + apply clarsimp + done + +lemma threadSet_valid_inQ_queues: + "\valid_inQ_queues and (\s. \d p. (\tcb. (inQ d p tcb) \ \(inQ d p (f tcb))) + \ obj_at' (\tcb. (inQ d p tcb) \ \(inQ d p (f tcb))) t s + \ t \ set (ksReadyQueues s (d, p)))\ + threadSet f t + \\rv. valid_inQ_queues\" + apply (simp add: threadSet_def) + apply wp + apply (simp add: valid_inQ_queues_def pred_tcb_at'_def) + apply (wp setObject_queues_unchanged_tcb + hoare_Ball_helper + hoare_vcg_all_lift + setObject_tcb_strongest)[1] + apply (wp getObject_tcb_wp) + apply (clarsimp simp: valid_inQ_queues_def pred_tcb_at'_def) + apply (clarsimp simp: obj_at'_def) + apply (fastforce) + done + +lemma valid_inQ_queues_ksReadyQueuesL1Bitmap_upd[simp]: + "valid_inQ_queues (s\ksReadyQueuesL1Bitmap := f\) = valid_inQ_queues s" + unfolding valid_inQ_queues_def + by simp + +lemma valid_inQ_queues_ksReadyQueuesL2Bitmap_upd[simp]: + "valid_inQ_queues (s\ksReadyQueuesL2Bitmap := f\) = valid_inQ_queues s" + unfolding valid_inQ_queues_def + by simp + +(* reorder the threadSet before the setQueue, useful for lemmas that don't refer to bitmap *) +lemma setQueue_after_addToBitmap: + "(setQueue d p q >>= (\rv. (when P (addToBitmap d p)) >>= (\rv. threadSet f t))) = + (when P (addToBitmap d p) >>= (\rv. (threadSet f t) >>= (\rv. setQueue d p q)))" + apply (case_tac P, simp_all) + prefer 2 + apply (simp add: setQueue_after) + apply (simp add: setQueue_def when_def) + apply (subst oblivious_modify_swap) + apply (simp add: threadSet_def getObject_def setObject_def + loadObject_default_def bitmap_fun_defs + split_def projectKO_def2 alignCheck_assert + magnitudeCheck_assert updateObject_default_def) + apply (intro oblivious_bind, simp_all) + apply (clarsimp simp: bind_assoc) + done + +lemma tcbSchedEnqueue_valid_inQ_queues[wp]: + "\valid_inQ_queues\ tcbSchedEnqueue t \\_. valid_inQ_queues\" + apply (simp add: tcbSchedEnqueue_def setQueue_after_addToBitmap) + apply (rule hoare_pre) + apply (rule_tac B="\rv. valid_inQ_queues and obj_at' (\obj. tcbQueued obj = rv) t" + in hoare_seq_ext) + apply (rename_tac queued) + apply (case_tac queued, simp_all add: unless_def)[1] + apply (wp setQueue_valid_inQ_queues threadSet_valid_inQ_queues threadGet_wp + hoare_vcg_const_Ball_lift + | simp add: inQ_def bitmap_fun_defs + | fastforce simp: valid_inQ_queues_def inQ_def obj_at'_def)+ + done + + (* prevents wp from splitting on the when; stronger technique than hoare_when_weak_wp + FIXME: possible to replace with hoare_when_weak_wp? + *) +definition + "removeFromBitmap_conceal d p q t \ when (null [x\q . x \ t]) (removeFromBitmap d p)" + +lemma removeFromBitmap_conceal_valid_inQ_queues[wp]: + "\ valid_inQ_queues \ removeFromBitmap_conceal d p q t \ \_. valid_inQ_queues \" + unfolding valid_inQ_queues_def removeFromBitmap_conceal_def + by (wp|clarsimp simp: bitmap_fun_defs)+ + +lemma valid_inQ_queues_ksSchedulerAction_update[simp]: + "valid_inQ_queues (ksSchedulerAction_update f s) = valid_inQ_queues s" + by (simp add: valid_inQ_queues_def) + +lemma rescheduleRequired_valid_inQ_queues[wp]: + "\valid_inQ_queues\ rescheduleRequired \\_. valid_inQ_queues\" + apply (simp add: rescheduleRequired_def) + apply wpsimp + done + +lemma sts_valid_inQ_queues[wp]: + "\valid_inQ_queues\ setThreadState st t \\rv. valid_inQ_queues\" + apply (simp add: setThreadState_def) + apply (wp threadSet_valid_inQ_queues [THEN hoare_strengthen_post]) + apply (clarsimp simp: sch_act_simple_def Invariants_H.valid_queues_def inQ_def)+ + done + +lemma updateObject_ep_inv: + "\P\ updateObject (obj::endpoint) ko p q n \\rv. P\" + by simp (rule updateObject_default_inv) + +lemma sbn_valid_inQ_queues[wp]: + "\valid_inQ_queues\ setBoundNotification ntfn t \\rv. valid_inQ_queues\" + apply (simp add: setBoundNotification_def) + apply (wp threadSet_valid_inQ_queues [THEN hoare_strengthen_post]) + apply (clarsimp simp: sch_act_simple_def Invariants_H.valid_queues_def inQ_def)+ + done + +lemma setEndpoint_valid_inQ_queues[wp]: + "\valid_inQ_queues\ setEndpoint ptr ep \\rv. valid_inQ_queues\" + apply (unfold setEndpoint_def) + apply (rule setObject_ep_pre) + apply (simp add: valid_inQ_queues_def) + apply (wp hoare_Ball_helper hoare_vcg_all_lift setObject_queues_unchanged[OF updateObject_ep_inv]) + apply simp + done + +lemma set_ntfn_valid_inQ_queues[wp]: + "\valid_inQ_queues\ setNotification ptr ntfn \\rv. valid_inQ_queues\" + apply (unfold setNotification_def) + apply (rule setObject_ntfn_pre) + apply (simp add: valid_inQ_queues_def) + apply (wp hoare_Ball_helper hoare_vcg_all_lift) + apply (clarsimp simp: updateObject_default_def in_monad) + apply (wp updateObject_default_inv | simp)+ + done + +crunch valid_inQ_queues[wp]: cancelSignal valid_inQ_queues + (ignore: updateObject setObject simp: updateObject_tcb_inv crunch_simps wp: crunch_wps) + +lemma (in delete_one_conc_pre) cancelIPC_valid_inQ_queues[wp]: + "\valid_inQ_queues\ cancelIPC t \\_. valid_inQ_queues\" + apply (simp add: cancelIPC_def Let_def getThreadReplySlot_def) + apply (wp hoare_drop_imps delete_one_inQ_queues threadSet_valid_inQ_queues | wpc | simp add:if_apply_def2 Fun.comp_def)+ + apply (clarsimp simp: valid_inQ_queues_def inQ_def)+ + done + +lemma valid_queues_inQ_queues: + "Invariants_H.valid_queues s \ valid_inQ_queues s" + by (force simp: Invariants_H.valid_queues_def valid_inQ_queues_def obj_at'_def + valid_queues_no_bitmap_def) + +lemma asUser_tcbQueued_inv[wp]: + "\obj_at' (\tcb. P (tcbQueued tcb)) t'\ asUser t m \\_. obj_at' (\tcb. P (tcbQueued tcb)) t'\" + apply (simp add: asUser_def tcb_in_cur_domain'_def threadGet_def) + apply (wp threadSet_obj_at'_strongish getObject_tcb_wp | wpc | simp | clarsimp simp: obj_at'_def)+ + done + +lemma asUser_valid_inQ_queues[wp]: + "\valid_inQ_queues\ asUser t f \\rv. valid_inQ_queues\" + unfolding valid_inQ_queues_def Ball_def + apply (wpsimp wp: hoare_vcg_all_lift) + defer + apply (wp asUser_ksQ) + apply assumption + apply (simp add: inQ_def[abs_def] obj_at'_conj) + apply (rule hoare_convert_imp) + apply (wp asUser_ksQ) + apply wp + done + +context begin +interpretation Arch . + +crunches cancel_ipc + for pspace_aligned[wp]: "pspace_aligned :: det_state \ _" + and pspace_distinct[wp]: "pspace_distinct :: det_state \ _" + (simp: crunch_simps wp: crunch_wps select_wp) + +end + +lemma (in delete_one) suspend_corres: + "corres dc (einvs and tcb_at t) invs' + (IpcCancel_A.suspend t) (ThreadDecls_H.suspend t)" + apply (rule corres_cross_over_guard[where P'=P' and Q="tcb_at' t and P'" for P']) + apply (fastforce dest!: tcb_at_cross state_relation_pspace_relation) + apply (simp add: IpcCancel_A.suspend_def Thread_H.suspend_def) + apply (rule corres_guard_imp) + apply (rule corres_split_nor [OF _ cancel_ipc_corres]) + apply (rule corres_split [OF _ gts_corres]) + apply (rule corres_split_nor) + apply (rule corres_split_nor [OF _ sts_corres]) + apply (rule tcbSchedDequeue_corres') + apply wpsimp + apply wp + apply wpsimp + apply (rule corres_if) + apply (case_tac state; simp) + apply (simp add: update_restart_pc_def updateRestartPC_def) + apply (rule corres_as_user') + apply (simp add: RISCV64.nextInstructionRegister_def RISCV64.faultRegister_def + RISCV64_H.nextInstructionRegister_def RISCV64_H.faultRegister_def) + apply (simp add: RISCV64_H.Register_def) + apply (subst unit_dc_is_eq) + apply (rule corres_underlying_trivial) + apply (wpsimp simp: RISCV64.setRegister_def RISCV64.getRegister_def) + apply (rule corres_return_trivial) + apply (wpsimp simp: update_restart_pc_def updateRestartPC_def)+ + apply (rule hoare_post_imp[where Q = "\rv s. tcb_at t s \ is_etcb_at t s \ pspace_aligned s \ pspace_distinct s"]) + apply simp + apply (wp | simp)+ + apply (fastforce simp: valid_sched_def tcb_at_is_etcb_at) + apply (clarsimp simp add: invs'_def valid_state'_def valid_queues_inQ_queues) + done + +lemma (in delete_one) prepareThreadDelete_corres: + "corres dc \ \ + (prepare_thread_delete t) (ArchRetypeDecls_H.RISCV64_H.prepareThreadDelete t)" + by (simp add: RISCV64_A.prepare_thread_delete_def RISCV64_H.prepareThreadDelete_def) + +lemma no_refs_simple_strg': + "st_tcb_at' simple' t s' \ P {} \ st_tcb_at' (\st. P (tcb_st_refs_of' st)) t s'" + by (fastforce elim!: pred_tcb'_weakenE)+ + +crunch it[wp]: cancelSignal "\s. P (ksIdleThread s)" + (wp: crunch_wps simp: crunch_simps + ignore: getObject setObject) + +lemma (in delete_one_conc_pre) cancelIPC_it[wp]: + "\\s. P (ksIdleThread s)\ + cancelIPC t + \\_ s. P (ksIdleThread s)\" + apply (simp add: cancelIPC_def Let_def getThreadReplySlot_def) + apply (wp hoare_drop_imps delete_one_it | wpc | simp add:if_apply_def2 Fun.comp_def)+ + done + +lemma tcbSchedDequeue_notksQ: + "\\s. t' \ set(ksReadyQueues s p)\ + tcbSchedDequeue t + \\_ s. t' \ set(ksReadyQueues s p)\" + apply (simp add: tcbSchedDequeue_def removeFromBitmap_conceal_def[symmetric]) + apply wp + apply (rule hoare_pre_post, assumption) + apply (clarsimp simp: bitmap_fun_defs removeFromBitmap_conceal_def, wp, clarsimp) + apply wp+ + apply clarsimp + apply (rule_tac Q="\_ s. t' \ set(ksReadyQueues s p)" in hoare_post_imp) + apply (wp | clarsimp)+ + done + +lemma rescheduleRequired_oa_queued: + "\ (\s. P (obj_at' (\tcb. Q (tcbQueued tcb) (tcbDomain tcb) (tcbPriority tcb)) t' s)) and sch_act_simple\ + rescheduleRequired + \\_ s. P (obj_at' (\tcb. Q (tcbQueued tcb) (tcbDomain tcb) (tcbPriority tcb)) t' s)\" + (is "\?OAQ t' p and sch_act_simple\ _ \_\") + apply (simp add: rescheduleRequired_def sch_act_simple_def) + apply (rule_tac B="\rv s. (rv = ResumeCurrentThread \ rv = ChooseNewThread) + \ ?OAQ t' p s" in hoare_seq_ext) + including no_pre + apply (wp | clarsimp)+ + apply (case_tac x) + apply (wp | clarsimp)+ + done + +lemma setThreadState_oa_queued: + "\\s. P' (obj_at' (\tcb. P (tcbQueued tcb) (tcbDomain tcb) (tcbPriority tcb)) t' s) \ + setThreadState st t + \\_ s. P' (obj_at' (\tcb. P (tcbQueued tcb) (tcbDomain tcb) (tcbPriority tcb)) t' s) \" + (is "\\s. P' (?Q P s)\ _ \\_ s. P' (?Q P s)\") + proof (rule P_bool_lift [where P=P']) + show pos: + "\R. \ ?Q R \ setThreadState st t \\_. ?Q R \" + apply (simp add: setThreadState_def) + apply (wp rescheduleRequired_oa_queued) + apply (simp add: sch_act_simple_def) + apply (rule_tac Q="\_. ?Q R" in hoare_post_imp, clarsimp) + apply (wp threadSet_obj_at'_strongish) + apply (clarsimp) + done + show "\\s. \ ?Q P s\ setThreadState st t \\_ s. \ ?Q P s\" + by (simp add: not_obj_at' comp_def, wp hoare_convert_imp pos) + qed + +lemma setBoundNotification_oa_queued: + "\\s. P' (obj_at' (\tcb. P (tcbQueued tcb) (tcbDomain tcb) (tcbPriority tcb)) t' s) \ + setBoundNotification ntfn t + \\_ s. P' (obj_at' (\tcb. P (tcbQueued tcb) (tcbDomain tcb) (tcbPriority tcb)) t' s) \" + (is "\\s. P' (?Q P s)\ _ \\_ s. P' (?Q P s)\") + proof (rule P_bool_lift [where P=P']) + show pos: + "\R. \ ?Q R \ setBoundNotification ntfn t \\_. ?Q R \" + apply (simp add: setBoundNotification_def) + apply (wp threadSet_obj_at'_strongish) + apply (clarsimp) + done + show "\\s. \ ?Q P s\ setBoundNotification ntfn t \\_ s. \ ?Q P s\" + by (simp add: not_obj_at' comp_def, wp hoare_convert_imp pos) + qed + +lemma tcbSchedDequeue_ksQ_distinct[wp]: + "\\s. distinct (ksReadyQueues s p)\ + tcbSchedDequeue t + \\_ s. distinct (ksReadyQueues s p)\" + apply (simp add: tcbSchedDequeue_def removeFromBitmap_conceal_def[symmetric]) + apply wp + apply (rule hoare_pre_post, assumption) + apply (clarsimp simp: bitmap_fun_defs removeFromBitmap_conceal_def, wp, clarsimp) + apply wp+ + apply (rule_tac Q="\_ s. distinct (ksReadyQueues s p)" in hoare_post_imp) + apply (clarsimp | wp)+ + done + +lemma sts_valid_queues_partial: + "\Invariants_H.valid_queues and sch_act_simple\ + setThreadState st t + \\_ s. \t' d p. + (t' \ set(ksReadyQueues s (d, p)) \ + (obj_at' (\tcb. tcbQueued tcb \ tcbDomain tcb = d \ tcbPriority tcb = p) t' s + \ (t' \ t \ st_tcb_at' runnable' t' s))) + \ distinct (ksReadyQueues s (d, p))\" + (is "\_\ _ \\_ s. \t' d p. ?OA t' d p s \ ?DISTINCT d p s \") + apply (rule_tac Q="\_ s. (\t' d p. ?OA t' d p s) \ (\d p. ?DISTINCT d p s)" + in hoare_post_imp) + apply (clarsimp) + apply (rule hoare_conjI) + apply (rule_tac Q="\s. \t' d p. + ((t'\set(ksReadyQueues s (d, p)) + \ \ (sch_act_simple s)) + \ (obj_at'(\tcb. tcbQueued tcb \ tcbDomain tcb = d \ tcbPriority tcb = p) t' s + \ st_tcb_at' runnable' t' s))" in hoare_pre_imp) + apply (fastforce simp: Invariants_H.valid_queues_def valid_queues_no_bitmap_def + pred_tcb_at'_def obj_at'_def inQ_def) + apply (rule hoare_vcg_all_lift)+ + apply (rule hoare_convert_imp) + including no_pre + apply (wp sts_ksQ setThreadState_oa_queued hoare_impI sts_pred_tcb_neq' + | clarsimp)+ + apply (rule_tac Q="\s. \d p. ?DISTINCT d p s \ sch_act_simple s" in hoare_pre_imp) + apply (clarsimp simp: Invariants_H.valid_queues_def valid_queues_no_bitmap_def) + apply (wp hoare_vcg_all_lift sts_ksQ) + apply (clarsimp) + done + +lemma tcbSchedDequeue_t_notksQ: + "\\s. t \ set (ksReadyQueues s (d, p)) \ + obj_at' (\tcb. tcbQueued tcb \ tcbDomain tcb = d \ tcbPriority tcb = p) t s\ + tcbSchedDequeue t + \\_ s. t \ set (ksReadyQueues s (d, p))\" + apply (rule_tac Q="(\s. t \ set (ksReadyQueues s (d, p))) + or obj_at'(\tcb. tcbQueued tcb \ tcbDomain tcb = d \ tcbPriority tcb = p) t" + in hoare_pre_imp, clarsimp) + apply (rule hoare_pre_disj) + apply (wp tcbSchedDequeue_notksQ)[1] + apply (simp add: tcbSchedDequeue_def removeFromBitmap_conceal_def[symmetric]) + apply wp + apply (rule hoare_pre_post, assumption) + apply (clarsimp simp: bitmap_fun_defs removeFromBitmap_conceal_def, wp, clarsimp) + apply (wp threadGet_wp)+ + apply (auto simp: obj_at'_real_def ko_wp_at'_def) + done + +lemma sts_invs_minor'_no_valid_queues: + "\st_tcb_at' (\st'. tcb_st_refs_of' st' = tcb_st_refs_of' st + \ (st \ Inactive \ \ idle' st \ + st' \ Inactive \ \ idle' st')) t + and (\s. t = ksIdleThread s \ idle' st) + and (\s. runnable' st \ obj_at' tcbQueued t s \ st_tcb_at' runnable' t s) + and sch_act_simple + and invs'\ + setThreadState st t + \\_ s. (\t' d p. + (t' \ set(ksReadyQueues s (d, p)) \ + (obj_at' (\tcb. tcbQueued tcb \ tcbDomain tcb = d \ tcbPriority tcb = p) t' s + \ (t' \ t \ st_tcb_at' runnable' t' s))) + \ distinct (ksReadyQueues s (d, p)) \ (maxDomain < d \ maxPriority < p \ ksReadyQueues s (d, p) = [])) \ + valid_bitmapQ s \ + bitmapQ_no_L2_orphans s \ + bitmapQ_no_L1_orphans s \ + valid_pspace' s \ + sch_act_wf (ksSchedulerAction s) s \ + sym_refs (state_refs_of' s) \ + if_live_then_nonz_cap' s \ + if_unsafe_then_cap' s \ + valid_idle' s \ + valid_global_refs' s \ + valid_arch_state' s \ + valid_irq_node' (irq_node' s) s \ + valid_irq_handlers' s \ + valid_irq_states' s \ + valid_machine_state' s \ + irqs_masked' s \ + valid_queues' s \ + ct_not_inQ s \ + ct_idle_or_in_cur_domain' s \ + pspace_domain_valid s \ + ksCurDomain s \ maxDomain \ + valid_dom_schedule' s \ + untyped_ranges_zero' s \ + cur_tcb' s \ + tcb_at' t s\" + apply (simp add: invs'_def valid_state'_def valid_queues_def) + apply (wp sts_valid_queues_partial sts_ksQ + setThreadState_oa_queued sts_st_tcb_at'_cases + irqs_masked_lift + valid_irq_node_lift + setThreadState_ct_not_inQ + sts_valid_bitmapQ_sch_act_simple + sts_valid_bitmapQ_no_L2_orphans_sch_act_simple + sts_valid_bitmapQ_no_L1_orphans_sch_act_simple + hoare_vcg_conj_lift hoare_vcg_imp_lift hoare_vcg_all_lift)+ + apply (clarsimp simp: disj_imp) + apply (intro conjI) + apply (clarsimp simp: valid_queues_def) + apply (rule conjI, clarsimp) + apply (drule valid_queues_no_bitmap_objD, assumption) + apply (clarsimp simp: inQ_def comp_def) + apply (rule conjI) + apply (erule obj_at'_weaken) + apply (simp add: inQ_def) + apply (clarsimp simp: st_tcb_at'_def) + apply (erule obj_at'_weaken) + apply (simp add: inQ_def) + apply (simp add: valid_queues_no_bitmap_def) + apply clarsimp + apply (clarsimp simp: st_tcb_at'_def) + apply (drule obj_at_valid_objs') + apply (clarsimp simp: valid_pspace'_def) + apply (clarsimp simp: valid_obj'_def valid_tcb'_def) + subgoal + by (fastforce simp: valid_tcb_state'_def + split: Structures_H.thread_state.splits) + apply (clarsimp dest!: st_tcb_at_state_refs_ofD' + elim!: rsubst[where P=sym_refs] + intro!: ext) + apply (fastforce simp: valid_queues_def inQ_def pred_tcb_at' pred_tcb_at'_def + elim!: st_tcb_ex_cap'' obj_at'_weakenE)+ + done + +crunch ct_idle_or_in_cur_domain'[wp]: tcbSchedDequeue ct_idle_or_in_cur_domain' + +lemma tcbSchedDequeue_invs'_no_valid_queues: + "\\s. (\t' d p. + (t' \ set(ksReadyQueues s (d, p)) \ + (obj_at' (\tcb. tcbQueued tcb \ tcbDomain tcb = d \ tcbPriority tcb = p) t' s + \ (t' \ t \ st_tcb_at' runnable' t' s))) + \ distinct (ksReadyQueues s (d, p)) \ (maxDomain < d \ maxPriority < p \ ksReadyQueues s (d, p) = [])) \ + valid_bitmapQ s \ + bitmapQ_no_L2_orphans s \ + bitmapQ_no_L1_orphans s \ + valid_pspace' s \ + sch_act_wf (ksSchedulerAction s) s \ + sym_refs (state_refs_of' s) \ + if_live_then_nonz_cap' s \ + if_unsafe_then_cap' s \ + valid_idle' s \ + valid_global_refs' s \ + valid_arch_state' s \ + valid_irq_node' (irq_node' s) s \ + valid_irq_handlers' s \ + valid_irq_states' s \ + valid_machine_state' s \ + irqs_masked' s \ + valid_queues' s \ + ct_not_inQ s \ + ct_idle_or_in_cur_domain' s \ + pspace_domain_valid s \ + ksCurDomain s \ maxDomain \ + valid_dom_schedule' s \ + untyped_ranges_zero' s \ + cur_tcb' s \ + tcb_at' t s\ + tcbSchedDequeue t + \\_. invs' \" + apply (simp add: invs'_def valid_state'_def) + apply (wp tcbSchedDequeue_valid_queues_weak valid_irq_handlers_lift + valid_irq_node_lift valid_irq_handlers_lift' + tcbSchedDequeue_irq_states irqs_masked_lift cur_tcb_lift + untyped_ranges_zero_lift + | clarsimp simp add: cteCaps_of_def valid_queues_def o_def)+ + apply (rule conjI) + apply (fastforce simp: obj_at'_def inQ_def st_tcb_at'_def valid_queues_no_bitmap_except_def) + apply (rule conjI, clarsimp simp: correct_queue_def) + apply (fastforce simp: valid_pspace'_def intro: obj_at'_conjI + elim: valid_objs'_maxDomain valid_objs'_maxPriority) + done + +lemmas sts_tcbSchedDequeue_invs' = + sts_invs_minor'_no_valid_queues + tcbSchedDequeue_invs'_no_valid_queues + +lemma asUser_sch_act_simple[wp]: + "\sch_act_simple\ asUser s t \\_. sch_act_simple\" + unfolding sch_act_simple_def + apply (rule asUser_nosch) + done + +lemma (in delete_one_conc) suspend_invs'[wp]: + "\invs' and sch_act_simple and tcb_at' t and (\s. t \ ksIdleThread s)\ + ThreadDecls_H.suspend t \\rv. invs'\" + apply (simp add: suspend_def) + apply (wp sts_tcbSchedDequeue_invs') + apply (simp add: updateRestartPC_def | strengthen no_refs_simple_strg')+ + prefer 2 + apply (wpsimp wp: hoare_drop_imps hoare_vcg_imp_lift' + | strengthen no_refs_simple_strg')+ + done + +lemma (in delete_one_conc_pre) suspend_tcb'[wp]: + "\tcb_at' t'\ ThreadDecls_H.suspend t \\rv. tcb_at' t'\" + apply (simp add: suspend_def) + apply (wpsimp simp: updateRestartPC_def) + done + +lemma (in delete_one_conc_pre) suspend_sch_act_simple[wp]: + "\sch_act_simple\ + ThreadDecls_H.suspend t \\rv. sch_act_simple\" + apply (simp add: suspend_def when_def updateRestartPC_def) + apply (wp cancelIPC_sch_act_simple | simp add: unless_def + | rule sch_act_simple_lift)+ + apply (simp add: updateRestartPC_def) + apply (rule asUser_nosch) + apply wpsimp+ + done + +lemma (in delete_one_conc) suspend_objs': + "\invs' and sch_act_simple and tcb_at' t and (\s. t \ ksIdleThread s)\ + suspend t \\rv. valid_objs'\" + apply (rule_tac Q="\_. invs'" in hoare_strengthen_post) + apply (wp suspend_invs') + apply fastforce + done + +lemma (in delete_one_conc_pre) suspend_st_tcb_at': + assumes x[simp]: "\st. simple' st \ P st" shows + "\st_tcb_at' P t\ + suspend thread + \\rv. st_tcb_at' P t\" + apply (simp add: suspend_def) + unfolding updateRestartPC_def + apply (wp sts_st_tcb_at'_cases threadSet_pred_tcb_no_state + cancelIPC_st_tcb_at hoare_drop_imps + | simp)+ + apply clarsimp + done + +lemmas (in delete_one_conc_pre) suspend_makes_simple' = + suspend_st_tcb_at' [where P=simple', simplified] + +lemma valid_queues_not_runnable'_not_ksQ: + assumes "Invariants_H.valid_queues s" and "st_tcb_at' (Not \ runnable') t s" + shows "\d p. t \ set (ksReadyQueues s (d, p))" + using assms + apply - + apply (clarsimp simp: Invariants_H.valid_queues_def valid_queues_no_bitmap_def pred_tcb_at'_def) + apply (erule_tac x=d in allE) + apply (erule_tac x=p in allE) + apply (clarsimp) + apply (drule(1) bspec) + apply (clarsimp simp: obj_at'_def) + done + +declare valid_queues_not_runnable'_not_ksQ[OF ByAssum, simp] + +lemma cancelSignal_queues[wp]: + "\Invariants_H.valid_queues and st_tcb_at' (Not \ runnable') t\ + cancelSignal t ae \\_. Invariants_H.valid_queues \" + apply (simp add: cancelSignal_def) + apply (wp sts_valid_queues) + apply (rule_tac Q="\_ s. \p. t \ set (ksReadyQueues s p)" in hoare_post_imp, simp) + apply (wp hoare_vcg_all_lift) + apply (wpc) + apply (wp)+ + apply (rule_tac Q="\_ s. Invariants_H.valid_queues s \ (\p. t \ set (ksReadyQueues s p))" in hoare_post_imp) + apply (clarsimp) + apply (wp) + apply (clarsimp) + done + +lemma (in delete_one_conc_pre) cancelIPC_queues[wp]: + "\Invariants_H.valid_queues and valid_objs' and (\s. weak_sch_act_wf (ksSchedulerAction s) s)\ + cancelIPC t \\rv. Invariants_H.valid_queues\" + apply (simp add: cancelIPC_def Let_def getThreadReplySlot_def + cong: Structures_H.thread_state.case_cong list.case_cong) + apply (rule hoare_seq_ext [OF _ gts_sp']) + apply (rule hoare_pre) + apply (wpc + | wp hoare_vcg_conj_lift delete_one_queues threadSet_valid_queues + threadSet_valid_objs' sts_valid_queues setEndpoint_ksQ + hoare_vcg_all_lift threadSet_sch_act threadSet_weak_sch_act_wf + | simp add: o_def if_apply_def2 inQ_def + | rule hoare_drop_imps + | clarsimp simp: valid_tcb'_def tcb_cte_cases_def cteSizeBits_def + elim!: pred_tcb'_weakenE)+ + apply (fastforce dest: valid_queues_not_runnable'_not_ksQ elim: pred_tcb'_weakenE) + done + +(* FIXME: move to Schedule_R *) +lemma tcbSchedDequeue_nonq[wp]: + "\Invariants_H.valid_queues and tcb_at' t and K (t = t')\ + tcbSchedDequeue t \\_ s. \d p. t' \ set (ksReadyQueues s (d, p))\" + apply (rule hoare_gen_asm) + apply (simp add: tcbSchedDequeue_def) + apply (wp threadGet_wp|simp)+ + apply (fastforce simp: Invariants_H.valid_queues_def valid_queues_no_bitmap_def obj_at'_def projectKOs inQ_def) + done + +lemma sts_ksQ_oaQ: + "\Invariants_H.valid_queues\ + setThreadState st t + \\_ s. t \ set (ksReadyQueues s (d, p)) \ + obj_at' (\tcb. tcbQueued tcb \ tcbDomain tcb = d \ tcbPriority tcb = p) t s\" + (is "\_\ _ \\_. ?POST\") + proof - + have RR: "\sch_act_simple and ?POST\ rescheduleRequired \\_. ?POST\" + apply (simp add: rescheduleRequired_def) + apply (wp) + apply (clarsimp) + apply (rule_tac + Q="(\s. action = ResumeCurrentThread \ action = ChooseNewThread) and ?POST" + in hoare_pre_imp, assumption) + apply (case_tac action) + apply (clarsimp)+ + apply (wp) + apply (clarsimp simp: sch_act_simple_def) + done + show ?thesis + apply (simp add: setThreadState_def) + apply (wp RR) + apply (rule_tac Q="\_. ?POST" in hoare_post_imp) + apply (clarsimp simp add: sch_act_simple_def) + apply (wp hoare_convert_imp) + apply (clarsimp simp: Invariants_H.valid_queues_def valid_queues_no_bitmap_def) + apply (drule_tac x=d in spec) + apply (drule_tac x=p in spec) + apply (fastforce dest: bspec elim!: obj_at'_weakenE simp: inQ_def) + done + qed + +lemma (in delete_one_conc_pre) suspend_nonq: + "\Invariants_H.valid_queues and valid_objs' and tcb_at' t + and (\s. weak_sch_act_wf (ksSchedulerAction s) s) + and (\s. t \ ksIdleThread s) and K (t = t')\ + suspend t + \\rv s. \d p. t' \ set (ksReadyQueues s (d, p))\" + apply (rule hoare_gen_asm) + apply (simp add: suspend_def) + unfolding updateRestartPC_def + apply (wp hoare_allI tcbSchedDequeue_t_notksQ sts_ksQ_oaQ) + apply wpsimp+ + done + +lemma suspend_makes_inactive: + "\K (t = t')\ suspend t \\rv. st_tcb_at' ((=) Inactive) t'\" + apply (cases "t = t'", simp_all) + apply (simp add: suspend_def unless_def) + apply (wp threadSet_pred_tcb_no_state setThreadState_st_tcb | simp)+ + done + +declare threadSet_sch_act_sane [wp] +declare sts_sch_act_sane [wp] + +lemma tcbSchedEnqueue_ksQset_weak: + "\\s. t' \ set (ksReadyQueues s p)\ + tcbSchedEnqueue t + \\_ s. t' \ set (ksReadyQueues s p)\" (is "\?PRE\ _ \_\") + apply (simp add: tcbSchedEnqueue_def unless_def) + apply (wp hoare_vcg_conj_lift hoare_vcg_imp_lift hoare_vcg_if_lift) + apply (rule_tac Q="\_. ?PRE" in hoare_post_imp, ((wp | clarsimp)+))+ + done + +lemma tcbSchedEnqueue_sch_act_not_ct[wp]: + "\\s. sch_act_not (ksCurThread s) s\ tcbSchedEnqueue t \\_ s. sch_act_not (ksCurThread s) s\" + by (rule hoare_weaken_pre, wps tcbSchedEnqueue_ct', wp, simp) + +lemma sts_sch_act_not_ct[wp]: + "\\s. sch_act_not (ksCurThread s) s\ + setThreadState st t \\_ s. sch_act_not (ksCurThread s) s\" + by (rule hoare_weaken_pre, wps tcbSchedEnqueue_ct', wp, simp) + +text \Cancelling all IPC in an endpoint or notification object\ + +lemma ep_cancel_corres_helper: + "corres dc ((\s. \t \ set list. tcb_at t s) and valid_etcbs and pspace_aligned and pspace_distinct) + (Invariants_H.valid_queues and valid_queues' and valid_objs') + (mapM_x (\t. do + y \ set_thread_state t Structures_A.Restart; + tcb_sched_action tcb_sched_enqueue t + od) list) + (mapM_x (\t. do + y \ setThreadState Structures_H.thread_state.Restart t; + tcbSchedEnqueue t + od) list)" + apply (rule_tac S="{t. (fst t = snd t) \ fst t \ set list}" + in corres_mapM_x) + apply clarsimp + apply (rule corres_guard_imp) + apply (subst bind_return_unit, rule corres_split [OF tcbSchedEnqueue_corres]) + apply simp + apply (rule corres_guard_imp [OF sts_corres]) + apply simp + apply (simp add: valid_tcb_state_def) + apply simp + apply (wp sts_valid_queues)+ + apply (force simp: tcb_at_is_etcb_at) + apply (fastforce elim: obj_at'_weakenE) + apply ((wp hoare_vcg_const_Ball_lift | simp)+)[1] + apply (rule hoare_pre) + apply (wp hoare_vcg_const_Ball_lift + weak_sch_act_wf_lift_linear sts_st_tcb' setThreadState_not_st + sts_valid_queues tcbSchedEnqueue_not_st + | simp)+ + apply (auto elim: obj_at'_weakenE simp: valid_tcb_state'_def) + done + +lemma ep_cancel_corres: + "corres dc (invs and valid_sched and ep_at ep) (invs' and ep_at' ep) + (cancel_all_ipc ep) (cancelAllIPC ep)" +proof - + have P: + "\list. + corres dc (\s. (\t \ set list. tcb_at t s) \ valid_pspace s \ ep_at ep s + \ valid_etcbs s \ weak_valid_sched_action s) + (\s. (\t \ set list. tcb_at' t s) \ valid_pspace' s + \ ep_at' ep s \ weak_sch_act_wf (ksSchedulerAction s) s + \ Invariants_H.valid_queues s \ valid_queues' s \ valid_objs' s) + (do x \ set_endpoint ep Structures_A.IdleEP; + x \ mapM_x (\t. do + y \ set_thread_state t Structures_A.Restart; + tcb_sched_action tcb_sched_enqueue t + od) list; + reschedule_required + od) + (do x \ setEndpoint ep IdleEP; + x \ mapM_x (\t. do + y \ setThreadState Structures_H.thread_state.Restart t; + tcbSchedEnqueue t + od) list; + rescheduleRequired + od)" + apply (rule corres_split') + apply (rule corres_guard_imp [OF set_ep_corres]) + apply (simp add: ep_relation_def)+ + apply (rule corres_split [OF rescheduleRequired_corres]) + apply (rule ep_cancel_corres_helper) + apply (rule mapM_x_wp') + apply (wp weak_sch_act_wf_lift_linear set_thread_state_runnable_weak_valid_sched_action | simp)+ + apply (rule_tac R="\_ s. \x\set list. tcb_at' x s \ valid_objs' s" + in hoare_post_add) + apply (rule mapM_x_wp') + apply (rule hoare_name_pre_state) + apply ((wp hoare_vcg_const_Ball_lift mapM_x_wp' + sts_valid_queues setThreadState_not_st sts_st_tcb' tcbSchedEnqueue_not_st + | clarsimp + | fastforce elim: obj_at'_weakenE simp: valid_tcb_state'_def)+)[2] + apply (rule hoare_name_pre_state) + apply (wp hoare_vcg_const_Ball_lift set_ep_valid_objs' + | (clarsimp simp: valid_ep'_def) + | (drule (1) bspec, clarsimp simp: valid_pspace'_def valid_tcb'_def valid_ep'_def elim!: valid_objs_valid_tcbE))+ + done + + show ?thesis + apply (simp add: cancel_all_ipc_def cancelAllIPC_def) + apply (rule corres_split' [OF _ _ get_simple_ko_sp get_ep_sp']) + apply (rule corres_guard_imp [OF get_ep_corres], simp+) + apply (case_tac epa, simp_all add: ep_relation_def + get_ep_queue_def) + apply (rule corres_guard_imp [OF P] + | clarsimp simp: valid_obj_def valid_ep_def + valid_obj'_def valid_ep'_def + invs_valid_pspace + valid_sched_def valid_sched_action_def + | erule obj_at_valid_objsE + | drule ko_at_valid_objs' + | rule conjI | clarsimp simp: invs'_def valid_state'_def)+ + done +qed + +(* FIXME move *) +lemma set_ntfn_tcb_obj_at' [wp]: + "\obj_at' (P::tcb \ bool) t\ + setNotification ntfn v + \\_. obj_at' P t\" + apply (clarsimp simp: setNotification_def, wp) + done + +lemma ntfn_cancel_corres: + "corres dc (invs and valid_sched and ntfn_at ntfn) (invs' and ntfn_at' ntfn) + (cancel_all_signals ntfn) (cancelAllSignals ntfn)" + apply (simp add: cancel_all_signals_def cancelAllSignals_def) + apply (rule corres_split' [OF _ _ get_simple_ko_sp get_ntfn_sp']) + apply (rule corres_guard_imp [OF get_ntfn_corres]) + apply simp+ + apply (case_tac "ntfn_obj ntfna", simp_all add: ntfn_relation_def) + apply (rule corres_guard_imp) + apply (rule corres_split [OF _ set_ntfn_corres]) + apply (rule corres_split [OF rescheduleRequired_corres]) + apply (rule ep_cancel_corres_helper) + apply (wp mapM_x_wp'[where 'b="det_ext state"] + weak_sch_act_wf_lift_linear setThreadState_not_st + set_thread_state_runnable_weak_valid_sched_action + | simp)+ + apply (rename_tac list) + apply (rule_tac R="\_ s. (\x\set list. tcb_at' x s) \ valid_objs' s" + in hoare_post_add) + apply (rule mapM_x_wp') + apply (rule hoare_name_pre_state) + apply (wp hoare_vcg_const_Ball_lift + sts_st_tcb' sts_valid_queues setThreadState_not_st + tcbSchedEnqueue_not_st + | (clarsimp simp: valid_tcb_state'_def) + | fastforce elim: obj_at'_weakenE)+ + apply (simp add: ntfn_relation_def) + apply (wp hoare_vcg_const_Ball_lift set_ntfn_aligned' set_ntfn_valid_objs' + weak_sch_act_wf_lift_linear + | simp)+ + apply (clarsimp simp: invs'_def valid_state'_def invs_valid_pspace valid_obj_def valid_ntfn_def + invs_weak_sch_act_wf valid_ntfn'_def valid_pspace'_def valid_sched_def + valid_sched_action_def valid_obj'_def + | erule obj_at_valid_objsE | drule ko_at_valid_objs' + | fastforce)+ + done + +lemma ep'_Idle_case_helper: + "(case ep of IdleEP \ a | _ \ b) = (if (ep = IdleEP) then a else b)" + by (cases ep, simp_all) + +lemma rescheduleRequired_notresume: + "\\s. ksSchedulerAction s \ ResumeCurrentThread\ + rescheduleRequired \\_ s. ksSchedulerAction s = ChooseNewThread\" + proof - + have ssa: "\\\ setSchedulerAction ChooseNewThread + \\_ s. ksSchedulerAction s = ChooseNewThread\" + by (simp add: setSchedulerAction_def | wp)+ + show ?thesis + by (simp add: rescheduleRequired_def, wp ssa) + qed + +lemma setThreadState_ResumeCurrentThread_imp_notct[wp]: + "\\s. ksSchedulerAction s = ResumeCurrentThread \ ksCurThread s \ t'\ + setThreadState st t + \\_ s. ksSchedulerAction s = ResumeCurrentThread \ ksCurThread s \ t'\" + (is "\?PRE\ _ \_\") +proof - + have nrct: + "\\s. ksSchedulerAction s \ ResumeCurrentThread\ + rescheduleRequired + \\_ s. ksSchedulerAction s \ ResumeCurrentThread\" + by (rule hoare_strengthen_post [OF rescheduleRequired_notresume], simp) + show ?thesis + apply (simp add: setThreadState_def) + apply (wpsimp wp: hoare_vcg_imp_lift [OF nrct]) + apply (rule_tac Q="\_. ?PRE" in hoare_post_imp) + apply (clarsimp) + apply (rule hoare_convert_imp [OF threadSet_nosch threadSet_ct]) + apply assumption + done +qed + +lemma cancel_all_invs'_helper: + "\all_invs_but_sym_refs_ct_not_inQ' and (\s. \x \ set q. tcb_at' x s) + and (\s. sym_refs (\x. if x \ set q then {r \ state_refs_of' s x. snd r = TCBBound} + else state_refs_of' s x) + \ (\x \ set q. ex_nonz_cap_to' x s))\ + mapM_x (\t. do + y \ setThreadState Structures_H.thread_state.Restart t; + tcbSchedEnqueue t + od) q + \\rv. all_invs_but_ct_not_inQ'\" + apply (rule mapM_x_inv_wp2) + apply clarsimp + apply (rule hoare_pre) + apply (wp valid_irq_node_lift valid_irq_handlers_lift'' irqs_masked_lift + hoare_vcg_const_Ball_lift untyped_ranges_zero_lift + sts_valid_queues sts_st_tcb' setThreadState_not_st + | simp add: cteCaps_of_def o_def)+ + apply (unfold fun_upd_apply Invariants_H.tcb_st_refs_of'_simps) + apply clarsimp + apply (intro conjI) + apply (clarsimp simp: valid_tcb_state'_def global'_no_ex_cap + elim!: rsubst[where P=sym_refs] + dest!: set_mono_suffix + intro!: ext + | (drule (1) bspec, clarsimp simp: valid_pspace'_def valid_tcb'_def elim!: valid_objs_valid_tcbE))+ + done + +lemma ep_q_refs_max: + "\ ko_at' r p s; sym_refs (state_refs_of' s); r \ IdleEP \ + \ (state_refs_of' s p \ (set (epQueue r) \ {EPSend, EPRecv})) + \ (\x\set (epQueue r). \ntfnptr. state_refs_of' s x \ + {(p, TCBBlockedSend), (p, TCBBlockedRecv), (ntfnptr, TCBBound)})" + apply (frule(1) sym_refs_ko_atD') + apply (drule ko_at_state_refs_ofD') + apply (case_tac r) + apply (clarsimp simp: st_tcb_at_refs_of_rev' tcb_bound_refs'_def + | rule conjI | drule(1) bspec | drule st_tcb_at_state_refs_ofD' + | case_tac ntfnptr)+ + done + +lemma rescheduleRequired_invs'[wp]: + "\invs'\ rescheduleRequired \\rv. invs'\" + apply (simp add: rescheduleRequired_def) + apply (wp ssa_invs' | simp add: invs'_update_cnt | wpc)+ + apply (clarsimp simp: invs'_def valid_state'_def) + done + +lemma invs_rct_ct_activatable': + "\ invs' s; ksSchedulerAction s = ResumeCurrentThread \ + \ st_tcb_at' activatable' (ksCurThread s) s" + by (simp add: invs'_def valid_state'_def ct_in_state'_def) + +lemma not_in_epQueue: + assumes ko_at: "ko_at' r ep_ptr s" and + srefs: "sym_refs (state_refs_of' s)" and + nidle: "r \ IdleEP" and + st_act: "st_tcb_at' simple' t s" + shows "t \ set (epQueue r)" +proof + assume t_epQ: "t \ set (epQueue r)" + + with ko_at nidle + have "(t, EPRecv) \ state_refs_of' s ep_ptr + \ (t, EPSend) \ state_refs_of' s ep_ptr" + by - (drule ko_at_state_refs_ofD', case_tac r, (clarsimp)+) + + with ko_at srefs + have "(ep_ptr, TCBBlockedRecv) \ state_refs_of' s t + \ (ep_ptr, TCBBlockedSend) \ state_refs_of' s t" + apply - + apply (frule(1) sym_refs_ko_atD') + apply (drule ko_at_state_refs_ofD') + apply (case_tac r) + apply (clarsimp simp: st_tcb_at_refs_of_rev' + | drule(1) bspec | drule st_tcb_at_state_refs_ofD')+ + done + + with ko_at have "st_tcb_at' (Not \ simple') t s" + apply - + apply (erule disjE) + apply (drule state_refs_of'_elemD) + apply (simp add: st_tcb_at_refs_of_rev') + apply (erule pred_tcb'_weakenE) + apply (clarsimp) + apply (drule state_refs_of'_elemD) + apply (simp add: st_tcb_at_refs_of_rev') + apply (erule pred_tcb'_weakenE) + apply (clarsimp) + done + + with st_act show False + by (rule pred_tcb'_neq_contra) simp +qed + +lemma ct_not_in_epQueue: + assumes "ko_at' r ep_ptr s" and + "sym_refs (state_refs_of' s)" and + "r \ IdleEP" and + "ct_in_state' simple' s" + shows "ksCurThread s \ set (epQueue r)" + using assms unfolding ct_in_state'_def + by (rule not_in_epQueue) + +lemma not_in_ntfnQueue: + assumes ko_at: "ko_at' r ntfn_ptr s" and + srefs: "sym_refs (state_refs_of' s)" and + nidle: "ntfnObj r \ IdleNtfn \ (\b m. ntfnObj r \ ActiveNtfn b)" and + st_act: "st_tcb_at' simple' t s" + shows "t \ set (ntfnQueue (ntfnObj r))" +proof + assume t_epQ: "t \ set (ntfnQueue (ntfnObj r))" + + with ko_at nidle + have "(t, NTFNSignal) \ state_refs_of' s ntfn_ptr" + by - (drule ko_at_state_refs_ofD', case_tac "ntfnObj r", (clarsimp)+) + with ko_at srefs + have "(ntfn_ptr, TCBSignal) \ state_refs_of' s t" + apply - + apply (frule(1) sym_refs_ko_atD') + apply (drule ko_at_state_refs_ofD') + apply (case_tac "ntfnObj r") + apply (clarsimp simp: st_tcb_at_refs_of_rev' ntfn_bound_refs'_def + | drule st_tcb_at_state_refs_ofD')+ + apply (drule_tac x="(t, NTFNSignal)" in bspec, clarsimp) + apply (clarsimp simp: st_tcb_at_refs_of_rev' dest!: st_tcb_at_state_refs_ofD') + done + + with ko_at have "st_tcb_at' (Not \ simple') t s" + apply - + apply (drule state_refs_of'_elemD) + apply (simp add: st_tcb_at_refs_of_rev') + apply (erule pred_tcb'_weakenE) + apply (clarsimp) + done + + with st_act show False + by (rule pred_tcb'_neq_contra) simp +qed + +lemma ct_not_in_ntfnQueue: + assumes ko_at: "ko_at' r ntfn_ptr s" and + srefs: "sym_refs (state_refs_of' s)" and + nidle: "ntfnObj r \ IdleNtfn \ (\b m. ntfnObj r \ ActiveNtfn b)" and + st_act: "ct_in_state' simple' s" + shows "ksCurThread s \ set (ntfnQueue (ntfnObj r))" + using assms unfolding ct_in_state'_def + by (rule not_in_ntfnQueue) + +crunch valid_pspace'[wp]: rescheduleRequired "valid_pspace'" +crunch valid_global_refs'[wp]: rescheduleRequired "valid_global_refs'" +crunch valid_machine_state'[wp]: rescheduleRequired "valid_machine_state'" + +lemma sch_act_wf_weak[elim!]: + "sch_act_wf sa s \ weak_sch_act_wf sa s" + by (case_tac sa, (simp add: weak_sch_act_wf_def)+) + +lemma rescheduleRequired_all_invs_but_ct_not_inQ: + "\all_invs_but_ct_not_inQ'\ rescheduleRequired \\_. invs'\" + apply (simp add: invs'_def valid_state'_def) + apply (rule hoare_pre) + apply (wp rescheduleRequired_ct_not_inQ + valid_irq_node_lift valid_irq_handlers_lift'' + irqs_masked_lift cur_tcb_lift + untyped_ranges_zero_lift + | simp add: cteCaps_of_def o_def)+ + apply (auto simp: sch_act_wf_weak) + done + +lemma cancelAllIPC_invs'[wp]: + "\invs'\ cancelAllIPC ep_ptr \\rv. invs'\" + apply (simp add: cancelAllIPC_def ep'_Idle_case_helper cong del: if_cong) + apply (wp rescheduleRequired_all_invs_but_ct_not_inQ + cancel_all_invs'_helper hoare_vcg_const_Ball_lift + valid_global_refs_lift' valid_arch_state_lift' + valid_irq_node_lift ssa_invs' sts_sch_act' + irqs_masked_lift + | simp only: sch_act_wf.simps forM_x_def | simp)+ + prefer 2 + apply assumption + apply (rule hoare_strengthen_post [OF get_ep_sp']) + apply (clarsimp simp: invs'_def valid_state'_def valid_ep'_def) + apply (frule obj_at_valid_objs', fastforce) + apply (clarsimp simp: valid_obj'_def) + apply (rule conjI) + apply (case_tac r, simp_all add: valid_ep'_def)[1] + apply (rule conjI[rotated]) + apply (drule(1) sym_refs_ko_atD') + apply (case_tac r, simp_all add: st_tcb_at_refs_of_rev')[1] + apply (clarsimp elim!: if_live_state_refsE + | drule(1) bspec | drule st_tcb_at_state_refs_ofD')+ + apply (drule(2) ep_q_refs_max) + apply (erule delta_sym_refs) + apply (clarsimp dest!: symreftype_inverse' split: if_split_asm | drule(1) bspec subsetD)+ + done + +lemma cancelAllSignals_invs'[wp]: + "\invs'\ cancelAllSignals ntfn \\rv. invs'\" + apply (simp add: cancelAllSignals_def) + apply (rule hoare_seq_ext [OF _ get_ntfn_sp']) + apply (case_tac "ntfnObj ntfna", simp_all) + apply (wp, simp) + apply (wp, simp) + apply (rule hoare_pre) + apply (wp rescheduleRequired_all_invs_but_ct_not_inQ + cancel_all_invs'_helper hoare_vcg_const_Ball_lift + valid_irq_node_lift ssa_invs' irqs_masked_lift + | simp only: sch_act_wf.simps)+ + apply (clarsimp simp: invs'_def valid_state'_def valid_ntfn'_def) + apply (frule obj_at_valid_objs', clarsimp) + apply (clarsimp simp: valid_obj'_def valid_ntfn'_def) + apply (drule(1) sym_refs_ko_atD') + apply (rule conjI, clarsimp elim!: if_live_state_refsE) + apply (rule conjI[rotated]) + apply (clarsimp elim!: if_live_state_refsE) + apply (drule_tac x="(x, NTFNSignal)" in bspec) + apply (clarsimp simp: st_tcb_at_refs_of_rev')+ + apply (drule st_tcb_at_state_refs_ofD') + apply clarsimp + apply (erule delta_sym_refs) + apply (clarsimp split: if_split_asm) + apply (clarsimp split: if_split_asm) + apply (fastforce simp: symreftype_inverse' ntfn_bound_refs'_def) + apply (drule_tac x="(x, NTFNSignal)" in bspec) + apply (clarsimp simp: st_tcb_at_refs_of_rev')+ + apply (drule st_tcb_at_state_refs_ofD') + apply (fastforce simp: symreftype_inverse' ntfn_bound_refs'_def tcb_bound_refs'_def) + done + +lemma cancelAllIPC_valid_objs'[wp]: + "\valid_objs'\ cancelAllIPC ep \\rv. valid_objs'\" + apply (simp add: cancelAllIPC_def ep'_Idle_case_helper cong del: if_cong) + apply (rule hoare_seq_ext [OF _ get_ep_sp']) + apply (rule hoare_pre) + apply (wp set_ep_valid_objs' setSchedulerAction_valid_objs') + apply (rule_tac Q="\rv s. valid_objs' s \ (\x\set (epQueue ep). tcb_at' x s)" + in hoare_post_imp) + apply simp + apply (simp add: Ball_def) + apply (wp mapM_x_wp' sts_valid_objs' + hoare_vcg_all_lift hoare_vcg_const_imp_lift)+ + apply simp + apply (simp add: valid_tcb_state'_def) + apply (wp set_ep_valid_objs' hoare_vcg_all_lift hoare_vcg_const_imp_lift) + apply (clarsimp) + apply (frule(1) ko_at_valid_objs') + apply simp + apply (clarsimp simp: valid_obj'_def valid_ep'_def) + apply (case_tac epa, simp_all) + done + +lemma cancelAllSignals_valid_objs'[wp]: + "\valid_objs'\ cancelAllSignals ntfn \\rv. valid_objs'\" + apply (simp add: cancelAllSignals_def) + apply (rule hoare_seq_ext [OF _ get_ntfn_sp']) + apply (case_tac "ntfnObj ntfna", simp_all) + apply (wp, simp) + apply (wp, simp) + apply (rename_tac list) + apply (rule_tac Q="\rv s. valid_objs' s \ (\x\set list. tcb_at' x s)" + in hoare_post_imp) + apply (simp add: valid_ntfn'_def) + apply (simp add: Ball_def) + apply (wp setSchedulerAction_valid_objs' mapM_x_wp' + sts_valid_objs' hoare_vcg_all_lift hoare_vcg_const_imp_lift + | simp)+ + apply (simp add: valid_tcb_state'_def) + apply (wp set_ntfn_valid_objs' hoare_vcg_all_lift hoare_vcg_const_imp_lift) + apply clarsimp + apply (frule(1) ko_at_valid_objs') + apply simp + apply (clarsimp simp: valid_obj'_def valid_ntfn'_def) + done + +lemma cancelAllIPC_st_tcb_at: + assumes x[simp]: "P Restart" shows + "\st_tcb_at' P t\ cancelAllIPC epptr \\rv. st_tcb_at' P t\" + unfolding cancelAllIPC_def + by (wp ep'_cases_weak_wp mapM_x_wp' sts_st_tcb_at'_cases | clarsimp)+ + +lemmas cancelAllIPC_makes_simple[wp] = + cancelAllIPC_st_tcb_at [where P=simple', simplified] + +lemma cancelAllSignals_st_tcb_at: + assumes x[simp]: "P Restart" shows + "\st_tcb_at' P t\ cancelAllSignals epptr \\rv. st_tcb_at' P t\" + unfolding cancelAllSignals_def + by (wp ntfn'_cases_weak_wp mapM_x_wp' sts_st_tcb_at'_cases | clarsimp)+ + +lemmas cancelAllSignals_makes_simple[wp] = + cancelAllSignals_st_tcb_at [where P=simple', simplified] + +lemma threadSet_not_tcb[wp]: + "\ko_wp_at' (\x. P x \ (projectKO_opt x = (None :: tcb option))) p\ + threadSet f t + \\rv. ko_wp_at' (\x. P x \ (projectKO_opt x = (None :: tcb option))) p\" + by (clarsimp simp: threadSet_def valid_def getObject_def + setObject_def in_monad loadObject_default_def + ko_wp_at'_def split_def in_magnitude_check + objBits_simps' updateObject_default_def + ps_clear_upd' projectKO_opt_tcb) + +lemma setThreadState_not_tcb[wp]: + "\ko_wp_at' (\x. P x \ (projectKO_opt x = (None :: tcb option))) p\ + setThreadState st t + \\rv. ko_wp_at' (\x. P x \ (projectKO_opt x = (None :: tcb option))) p\" + apply (simp add: setThreadState_def setQueue_def + rescheduleRequired_def tcbSchedEnqueue_def + unless_def bitmap_fun_defs + cong: scheduler_action.case_cong cong del: if_cong + | wp | wpcw)+ + done + +lemma tcbSchedEnqueue_unlive: + "\ko_wp_at' (\x. \ live' x \ (projectKO_opt x = (None :: tcb option))) p + and tcb_at' t\ + tcbSchedEnqueue t + \\_. ko_wp_at' (\x. \ live' x \ (projectKO_opt x = (None :: tcb option))) p\" + apply (simp add: tcbSchedEnqueue_def unless_def) + apply (wp | simp add: setQueue_def bitmap_fun_defs)+ + done + +lemma cancelAll_unlive_helper: + "\\s. (\x\set xs. tcb_at' x s) \ + ko_wp_at' (\x. \ live' x \ (projectKO_opt x = (None :: tcb option))) p s\ + mapM_x (\t. do + y \ setThreadState Structures_H.thread_state.Restart t; + tcbSchedEnqueue t + od) xs + \\rv. ko_wp_at' (Not \ live') p\" + apply (rule hoare_strengthen_post) + apply (rule mapM_x_wp') + apply (rule hoare_pre) + apply (wp tcbSchedEnqueue_unlive hoare_vcg_const_Ball_lift) + apply clarsimp + apply (clarsimp elim!: ko_wp_at'_weakenE) + done + +context begin interpretation Arch . (*FIXME: arch_split*) +lemma setObject_ko_wp_at': + fixes v :: "'a :: pspace_storable" + assumes x: "\v :: 'a. updateObject v = updateObject_default v" + assumes n: "\v :: 'a. objBits v = n" + assumes v: "(1 :: machine_word) < 2 ^ n" + shows + "\\s. P (injectKO v)\ setObject p v \\rv. ko_wp_at' P p\" + by (clarsimp simp: setObject_def valid_def in_monad + ko_wp_at'_def x split_def n + updateObject_default_def + objBits_def[symmetric] ps_clear_upd' + in_magnitude_check v) + +lemma rescheduleRequired_unlive: + "\\s. ko_wp_at' (Not \ live') p s \ ksSchedulerAction s \ SwitchToThread p\ + rescheduleRequired + \\rv. ko_wp_at' (Not \ live') p\" + apply (simp add: rescheduleRequired_def) + apply (wp | simp | wpc)+ + apply (simp add: tcbSchedEnqueue_def unless_def + threadSet_def setQueue_def threadGet_def) + apply (wp setObject_ko_wp_at getObject_tcb_wp + | simp add: objBits_simps' bitmap_fun_defs split del: if_split)+ + apply (clarsimp simp: o_def) + apply (drule obj_at_ko_at') + apply clarsimp + done + +lemmas setEndpoint_ko_wp_at' + = setObject_ko_wp_at'[where 'a=endpoint, folded setEndpoint_def, simplified] + +lemma cancelAllIPC_unlive: + "\valid_objs' and (\s. sch_act_wf (ksSchedulerAction s) s)\ + cancelAllIPC ep \\rv. ko_wp_at' (Not \ live') ep\" + apply (simp add: cancelAllIPC_def ep'_Idle_case_helper) + apply (rule hoare_seq_ext [OF _ get_ep_sp']) + apply (rule hoare_pre) + apply (wp cancelAll_unlive_helper setEndpoint_ko_wp_at' + hoare_vcg_const_Ball_lift rescheduleRequired_unlive + mapM_x_wp' + | simp add: objBits_simps')+ + apply (clarsimp simp: projectKO_opt_tcb) + apply (frule(1) obj_at_valid_objs') + apply (intro conjI impI) + apply (clarsimp simp: valid_obj'_def valid_ep'_def obj_at'_def pred_tcb_at'_def ko_wp_at'_def + split: endpoint.split_asm)+ + done + +lemma cancelAllSignals_unlive: + "\\s. valid_objs' s \ sch_act_wf (ksSchedulerAction s) s + \ obj_at' (\ko. ntfnBoundTCB ko = None) ntfnptr s\ + cancelAllSignals ntfnptr \\rv. ko_wp_at' (Not \ live') ntfnptr\" + apply (simp add: cancelAllSignals_def) + apply (rule hoare_seq_ext [OF _ get_ntfn_sp']) + apply (case_tac "ntfnObj ntfn", simp_all add: setNotification_def) + apply wp + apply (fastforce simp: obj_at'_real_def + dest: obj_at_conj' + elim: ko_wp_at'_weakenE) + apply wp + apply (fastforce simp: obj_at'_real_def + dest: obj_at_conj' + elim: ko_wp_at'_weakenE) + apply (wp rescheduleRequired_unlive) + apply (wp cancelAll_unlive_helper) + apply ((wp mapM_x_wp' setObject_ko_wp_at' hoare_vcg_const_Ball_lift)+, + simp_all add: objBits_simps', simp_all) + apply (fold setNotification_def, wp) + apply (intro conjI[rotated]) + apply (clarsimp simp: pred_tcb_at'_def obj_at'_def) + apply (simp add: projectKO_opt_tcb) + apply (fastforce simp: ko_wp_at'_def valid_obj'_def valid_ntfn'_def obj_at'_def)+ + done + +crunch ep_at'[wp]: tcbSchedEnqueue "ep_at' epptr" + (simp: unless_def) + +declare if_cong[cong] + +lemma insert_eqD: + "A = insert a B \ a \ A" + by blast + +lemma cancelBadgedSends_filterM_helper': + notes if_cong[cong del] + shows + "\ys. + \\s. all_invs_but_sym_refs_ct_not_inQ' s + \ ex_nonz_cap_to' epptr s \ ep_at' epptr s + \ sym_refs ((state_refs_of' s) (epptr := set (xs @ ys) \ {EPSend})) + \ (\y \ set (xs @ ys). state_refs_of' s y = {(epptr, TCBBlockedSend)} + \ {r \ state_refs_of' s y. snd r = TCBBound}) + \ distinct (xs @ ys)\ + filterM (\t. do st \ getThreadState t; + if blockingIPCBadge st = badge then + do y \ setThreadState Structures_H.thread_state.Restart t; + y \ tcbSchedEnqueue t; + return False + od + else return True + od) xs + \\rv s. all_invs_but_sym_refs_ct_not_inQ' s + \ ex_nonz_cap_to' epptr s \ ep_at' epptr s + \ sym_refs ((state_refs_of' s) (epptr := (set rv \ set ys) \ {EPSend})) + \ (\y \ set ys. state_refs_of' s y = {(epptr, TCBBlockedSend)} + \ {r \ state_refs_of' s y. snd r = TCBBound}) + \ distinct rv \ distinct (xs @ ys) \ set rv \ set xs \ (\x \ set xs. tcb_at' x s)\" + apply (rule_tac xs=xs in rev_induct) + apply clarsimp + apply wp + apply clarsimp + apply (clarsimp simp: filterM_append bind_assoc simp del: set_append distinct_append) + apply (drule spec, erule hoare_seq_ext[rotated]) + apply (rule hoare_seq_ext [OF _ gts_inv']) + apply (rule hoare_pre) + apply (wp valid_irq_node_lift hoare_vcg_const_Ball_lift sts_sch_act' + sch_act_wf_lift valid_irq_handlers_lift'' cur_tcb_lift irqs_masked_lift + sts_st_tcb' sts_valid_queues setThreadState_not_st + tcbSchedEnqueue_not_st + untyped_ranges_zero_lift + | clarsimp simp: cteCaps_of_def o_def)+ + apply (frule insert_eqD, frule state_refs_of'_elemD) + apply (clarsimp simp: valid_tcb_state'_def st_tcb_at_refs_of_rev') + apply (frule pred_tcb_at') + apply (rule conjI[rotated], blast) + apply clarsimp + apply (intro conjI) + apply (clarsimp simp: valid_pspace'_def valid_tcb'_def elim!: valid_objs_valid_tcbE dest!: st_tcb_ex_cap'') + apply (fastforce dest!: st_tcb_ex_cap'') + apply (clarsimp simp: valid_idle'_def pred_tcb_at'_def obj_at'_def) + apply (erule delta_sym_refs) + apply (fastforce elim!: obj_atE' + simp: state_refs_of'_def tcb_bound_refs'_def + subsetD symreftype_inverse' + split: if_split_asm)+ + done + +lemmas cancelBadgedSends_filterM_helper + = spec [where x=Nil, OF cancelBadgedSends_filterM_helper', simplified] + +lemma cancelBadgedSends_invs[wp]: + notes if_cong[cong del] + shows + "\invs'\ cancelBadgedSends epptr badge \\rv. invs'\" + apply (simp add: cancelBadgedSends_def) + apply (rule hoare_seq_ext [OF _ get_ep_sp']) + apply (case_tac ep, simp_all) + apply ((wp | simp)+)[2] + apply (subst bind_assoc [where g="\_. rescheduleRequired", + symmetric])+ + apply (rule hoare_seq_ext + [OF rescheduleRequired_all_invs_but_ct_not_inQ]) + apply (simp add: list_case_return cong: list.case_cong) + apply (rule hoare_pre, wp valid_irq_node_lift irqs_masked_lift) + apply simp + apply (rule hoare_strengthen_post, + rule cancelBadgedSends_filterM_helper[where epptr=epptr]) + apply (clarsimp simp: ep_redux_simps3 fun_upd_def[symmetric]) + apply (clarsimp simp add: valid_ep'_def split: list.split) + apply blast + apply (wp valid_irq_node_lift irqs_masked_lift | wp (once) sch_act_sane_lift)+ + apply (clarsimp simp: invs'_def valid_state'_def + valid_ep'_def fun_upd_def[symmetric] + obj_at'_weakenE[OF _ TrueI]) + apply (frule obj_at_valid_objs', clarsimp) + apply (clarsimp simp: valid_obj'_def valid_ep'_def) + apply (frule if_live_then_nonz_capD', simp add: obj_at'_real_def) + apply clarsimp + apply (frule(1) sym_refs_ko_atD') + apply (clarsimp simp add: fun_upd_idem + st_tcb_at_refs_of_rev') + apply (drule (1) bspec, drule st_tcb_at_state_refs_ofD', clarsimp) + apply (fastforce simp: set_eq_subset tcb_bound_refs'_def) + done + +crunch state_refs_of[wp]: tcb_sched_action "\s. P (state_refs_of s)" + + +lemma cancel_badged_sends_corres: + "corres dc (invs and valid_sched and ep_at epptr) (invs' and ep_at' epptr) + (cancel_badged_sends epptr bdg) (cancelBadgedSends epptr bdg)" + apply (simp add: cancel_badged_sends_def cancelBadgedSends_def) + apply (rule corres_guard_imp) + apply (rule corres_split [OF _ get_ep_corres get_simple_ko_sp get_ep_sp', + where Q="invs and valid_sched" and Q'=invs']) + apply simp_all + apply (case_tac ep, simp_all add: ep_relation_def) + apply (simp add: filterM_mapM list_case_return cong: list.case_cong) + apply (rule corres_guard_imp) + apply (rule corres_split_nor [OF _ set_ep_corres]) + apply (rule corres_split_eqr[OF _ _ _ hoare_post_add[where R="\_. valid_objs'"]]) + apply (rule corres_split [OF rescheduleRequired_corres]) + apply (rule set_ep_corres) + apply (simp split: list.split add: ep_relation_def) + apply (wp weak_sch_act_wf_lift_linear)+ + apply (rule_tac S="(=)" + and Q="\xs s. (\x \ set xs. (epptr, TCBBlockedSend) \ state_refs_of s x) \ + distinct xs \ valid_etcbs s \ pspace_aligned s \ pspace_distinct s" + and Q'="\xs s. Invariants_H.valid_queues s \ valid_queues' s \ valid_objs' s" + in corres_mapM_list_all2[where r'="(=)"], + simp_all add: list_all2_refl)[1] + apply (clarsimp simp: liftM_def[symmetric] o_def) + apply (rule corres_guard_imp) + apply (rule corres_split [OF _ gts_corres]) + apply (rule_tac F="\pl. st = Structures_A.BlockedOnSend epptr pl" + in corres_gen_asm) + apply (clarsimp simp: o_def dc_def[symmetric] liftM_def) + apply (rule corres_split [OF _ sts_corres]) + apply (rule corres_split[OF _ tcbSchedEnqueue_corres]) + apply (rule corres_trivial) + apply simp + apply wp+ + apply simp + apply (wp sts_valid_queues gts_st_tcb_at)+ + apply (clarsimp simp: valid_tcb_state_def tcb_at_def st_tcb_def2 + st_tcb_at_refs_of_rev + dest!: state_refs_of_elemD elim!: tcb_at_is_etcb_at[rotated]) + apply (simp add: is_tcb_def) + apply simp + apply (wp hoare_vcg_const_Ball_lift gts_wp | clarsimp)+ + apply (wp gts_st_tcb_at hoare_vcg_const_Ball_lift hoare_vcg_imp_lift + weak_sch_act_wf_lift_linear mapM_wp' + sts_st_tcb' sts_valid_queues setThreadState_valid_objs' + set_thread_state_runnable_weak_valid_sched_action + | clarsimp simp: valid_tcb_state'_def)+ + apply (simp add: ep_relation_def) + apply (wp hoare_vcg_const_Ball_lift weak_sch_act_wf_lift_linear set_ep_valid_objs' + | simp)+ + apply (clarsimp simp: conj_comms) + apply (frule sym_refs_ko_atD, clarsimp+) + apply (rule obj_at_valid_objsE, assumption+, clarsimp+) + apply (clarsimp simp: valid_obj_def valid_ep_def valid_sched_def valid_sched_action_def) + apply (rule conjI, fastforce) + apply (rule conjI, fastforce) + apply (rule conjI, erule obj_at_weakenE, clarsimp simp: is_ep) + apply (clarsimp simp: st_tcb_at_refs_of_rev) + apply (drule(1) bspec, drule st_tcb_at_state_refs_ofD, clarsimp) + apply (simp add: set_eq_subset) + apply (clarsimp simp: obj_at'_weakenE[OF _ TrueI]) + apply (drule ko_at_valid_objs', clarsimp) + apply simp + apply (clarsimp simp: valid_obj'_def valid_ep'_def invs_weak_sch_act_wf + invs'_def valid_state'_def) + done + +lemma suspend_unqueued: + "\\\ suspend t \\rv. obj_at' (Not \ tcbQueued) t\" + apply (simp add: suspend_def unless_def tcbSchedDequeue_def) + apply (wp hoare_vcg_if_lift hoare_vcg_conj_lift hoare_vcg_imp_lift) + apply (simp add: threadGet_def| wp getObject_tcb_wp)+ + apply (rule hoare_strengthen_post, rule hoare_post_taut) + apply (fastforce simp: obj_at'_def) + apply (rule hoare_post_taut) + apply wp+ + done + +crunch unqueued: prepareThreadDelete "obj_at' (\a. \ tcbQueued a) t" +crunch inactive: prepareThreadDelete "st_tcb_at' ((=) Inactive) t'" +crunch nonq: prepareThreadDelete " \s. \d p. t' \ set (ksReadyQueues s (d, p))" + +end +end