From 97f292cab9f77f323121b5966216c730e7699514 Mon Sep 17 00:00:00 2001 From: Rafal Kolanski Date: Tue, 14 Apr 2020 23:17:33 +1000 Subject: [PATCH] riscv crefine: sorried Finalise_C Signed-off-by: Rafal Kolanski --- proof/crefine/RISCV64/Finalise_C.thy | 2207 ++++++++++++++++++++++++++ 1 file changed, 2207 insertions(+) create mode 100644 proof/crefine/RISCV64/Finalise_C.thy diff --git a/proof/crefine/RISCV64/Finalise_C.thy b/proof/crefine/RISCV64/Finalise_C.thy new file mode 100644 index 000000000..b17f0a578 --- /dev/null +++ b/proof/crefine/RISCV64/Finalise_C.thy @@ -0,0 +1,2207 @@ +(* + * Copyright 2014, General Dynamics C4 Systems + * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230) + * + * SPDX-License-Identifier: GPL-2.0-only + *) + +theory Finalise_C +imports IpcCancel_C +begin + +context kernel_m +begin + +declare if_split [split del] + +lemma empty_fail_getEndpoint: + "empty_fail (getEndpoint ep)" + unfolding getEndpoint_def + by (auto intro: empty_fail_getObject) + +definition + "option_map2 f m = option_map f \ m" + +lemma tcbSchedEnqueue_cslift_spec: + "\s. \\\<^bsub>/UNIV\<^esub> \s. \d v. option_map2 tcbPriority_C (cslift s) \tcb = Some v + \ v \ ucast maxPrio + \ option_map2 tcbDomain_C (cslift s) \tcb = Some d + \ d \ ucast maxDom + \ (end_C (index \ksReadyQueues (unat (d*0x100 + v))) \ NULL + \ option_map2 tcbPriority_C (cslift s) + (head_C (index \ksReadyQueues (unat (d*0x100 + v)))) + \ None + \ option_map2 tcbDomain_C (cslift s) + (head_C (index \ksReadyQueues (unat (d*0x100 + v)))) + \ None)\ + Call tcbSchedEnqueue_'proc + {s'. option_map2 tcbEPNext_C (cslift s') = option_map2 tcbEPNext_C (cslift s) + \ option_map2 tcbEPPrev_C (cslift s') = option_map2 tcbEPPrev_C (cslift s) + \ option_map2 tcbPriority_C (cslift s') = option_map2 tcbPriority_C (cslift s) + \ option_map2 tcbDomain_C (cslift s') = option_map2 tcbDomain_C (cslift s)}" + apply (hoare_rule HoarePartial.ProcNoRec1) + apply (rule allI, rule conseqPre, vcg) + apply (clarsimp simp: option_map2_def fun_eq_iff h_t_valid_clift + h_t_valid_field[OF h_t_valid_clift]) + apply (rule conjI) + apply (clarsimp simp: typ_heap_simps cong: if_cong) + apply (simp split: if_split) + apply (clarsimp simp: typ_heap_simps if_Some_helper cong: if_cong) + by (simp split: if_split) + +lemma setThreadState_cslift_spec: + "\s. \\\<^bsub>/UNIV\<^esub> \s. s \\<^sub>c \tptr \ (\x. ksSchedulerAction_' (globals s) = tcb_Ptr x + \ x \ 0 \ x \ 1 + \ (\d v. option_map2 tcbPriority_C (cslift s) (tcb_Ptr x) = Some v + \ v \ ucast maxPrio + \ option_map2 tcbDomain_C (cslift s) (tcb_Ptr x) = Some d + \ d \ ucast maxDom + \ (end_C (index \ksReadyQueues (unat (d*0x100 + v))) \ NULL + \ option_map2 tcbPriority_C (cslift s) + (head_C (index \ksReadyQueues (unat (d*0x100 + v)))) + \ None + \ option_map2 tcbDomain_C (cslift s) + (head_C (index \ksReadyQueues (unat (d*0x100 + v)))) + \ None)))\ + Call setThreadState_'proc + {s'. option_map2 tcbEPNext_C (cslift s') = option_map2 tcbEPNext_C (cslift s) + \ option_map2 tcbEPPrev_C (cslift s') = option_map2 tcbEPPrev_C (cslift s) + \ option_map2 tcbPriority_C (cslift s') = option_map2 tcbPriority_C (cslift s) + \ option_map2 tcbDomain_C (cslift s') = option_map2 tcbDomain_C (cslift s) + \ ksReadyQueues_' (globals s') = ksReadyQueues_' (globals s)}" + apply (rule allI, rule conseqPre) + apply vcg_step + apply vcg_step + apply vcg_step + apply vcg_step + apply vcg_step + apply vcg_step + apply vcg_step + apply (vcg exspec=tcbSchedEnqueue_cslift_spec) + apply (vcg_step+)[2] + apply vcg_step + apply (vcg exspec=isRunnable_modifies) + apply vcg + apply vcg_step + apply vcg_step + apply (vcg_step+)[1] + apply vcg + apply vcg_step+ + apply (clarsimp simp: typ_heap_simps h_t_valid_clift_Some_iff + fun_eq_iff option_map2_def) + by (simp split: if_split) + +lemma ep_queue_relation_shift: + "(option_map2 tcbEPNext_C (cslift s') + = option_map2 tcbEPNext_C (cslift s) + \ option_map2 tcbEPPrev_C (cslift s') + = option_map2 tcbEPPrev_C (cslift s)) + \ ep_queue_relation (cslift s') ts qPrev qHead + = ep_queue_relation (cslift s) ts qPrev qHead" + apply clarsimp + apply (induct ts arbitrary: qPrev qHead) + apply simp + apply simp + apply (simp add: option_map2_def fun_eq_iff + map_option_case) + apply (drule_tac x=qHead in spec)+ + apply (clarsimp split: option.split_asm) + done + +lemma rf_sr_cscheduler_relation: + "(s, s') \ rf_sr \ cscheduler_action_relation + (ksSchedulerAction s) (ksSchedulerAction_' (globals s'))" + by (clarsimp simp: rf_sr_def cstate_relation_def Let_def) + +lemma obj_at_ko_at2': + "\ obj_at' P p s; ko_at' ko p s \ \ P ko" + apply (drule obj_at_ko_at') + apply clarsimp + apply (drule ko_at_obj_congD', simp+) + done + +lemma ctcb_relation_tcbDomain: + "ctcb_relation tcb tcb' \ ucast (tcbDomain tcb) = tcbDomain_C tcb'" + by (simp add: ctcb_relation_def) + +lemma ctcb_relation_tcbPriority: + "ctcb_relation tcb tcb' \ ucast (tcbPriority tcb) = tcbPriority_C tcb'" + by (simp add: ctcb_relation_def) + +lemma ctcb_relation_tcbDomain_maxDom: + "\ ctcb_relation tcb tcb'; tcbDomain tcb \ maxDomain \ \ tcbDomain_C tcb' \ ucast maxDom" + apply (subst ctcb_relation_tcbDomain[symmetric], simp) + apply (subst ucast_le_migrate) + apply ((simp add:maxDom_def word_size)+)[2] + apply (simp add: ucast_up_ucast is_up_def source_size_def word_size target_size_def) + apply (simp add: maxDom_to_H) + done + +lemma ctcb_relation_tcbPriority_maxPrio: + "\ ctcb_relation tcb tcb'; tcbPriority tcb \ maxPriority \ + \ tcbPriority_C tcb' \ ucast maxPrio" + apply (subst ctcb_relation_tcbPriority[symmetric], simp) + apply (subst ucast_le_migrate) + apply ((simp add: seL4_MaxPrio_def word_size)+)[2] + apply (simp add: ucast_up_ucast is_up_def source_size_def word_size target_size_def) + apply (simp add: maxPrio_to_H) + done + +lemma tcbSchedEnqueue_cslift_precond_discharge: + "\ (s, s') \ rf_sr; obj_at' (P :: tcb \ bool) x s; + valid_queues s; valid_objs' s \ \ + (\d v. option_map2 tcbPriority_C (cslift s') (tcb_ptr_to_ctcb_ptr x) = Some v + \ v \ ucast maxPrio + \ option_map2 tcbDomain_C (cslift s') (tcb_ptr_to_ctcb_ptr x) = Some d + \ d \ ucast maxDom + \ (end_C (index (ksReadyQueues_' (globals s')) (unat (d*0x100 + v))) \ NULL + \ option_map2 tcbPriority_C (cslift s') + (head_C (index (ksReadyQueues_' (globals s')) (unat (d*0x100 + v)))) + \ None + \ option_map2 tcbDomain_C (cslift s') + (head_C (index (ksReadyQueues_' (globals s')) (unat (d*0x100 + v)))) + \ None))" + apply (drule(1) obj_at_cslift_tcb) + apply (clarsimp simp: typ_heap_simps' option_map2_def) + apply (frule_tac t=x in valid_objs'_maxPriority, fastforce simp: obj_at'_def) + apply (frule_tac t=x in valid_objs'_maxDomain, fastforce simp: obj_at'_def) + apply (drule_tac P="\tcb. tcbPriority tcb \ maxPriority" in obj_at_ko_at2', simp) + apply (drule_tac P="\tcb. tcbDomain tcb \ maxDomain" in obj_at_ko_at2', simp) + + apply (simp add: ctcb_relation_tcbDomain_maxDom ctcb_relation_tcbPriority_maxPrio) + apply (frule_tac d="tcbDomain ko" and p="tcbPriority ko" + in rf_sr_sched_queue_relation) + apply (simp add: maxDom_to_H maxPrio_to_H)+ + apply (simp add: cready_queues_index_to_C_def2 numPriorities_def) + apply (clarsimp simp: ctcb_relation_def) + apply (frule arg_cong[where f=unat], subst(asm) unat_ucast_up_simp, simp) + apply (frule tcb_queue'_head_end_NULL) + apply (erule conjunct1[OF valid_queues_valid_q]) + apply (frule(1) tcb_queue_relation_qhead_valid') + apply (simp add: valid_queues_valid_q) + apply (clarsimp simp: h_t_valid_clift_Some_iff) + done + +lemma cancel_all_ccorres_helper: + "ccorres dc xfdc + (\s. valid_objs' s \ valid_queues s + \ (\t\set ts. tcb_at' t s \ t \ 0) + \ sch_act_wf (ksSchedulerAction s) s) + {s'. \p. ep_queue_relation (cslift s') ts + p (thread_' s')} hs + (mapM_x (\t. do + y \ setThreadState Restart t; + tcbSchedEnqueue t + od) ts) + (WHILE \thread \ tcb_Ptr 0 DO + (CALL setThreadState(\thread, scast ThreadState_Restart));; + (CALL tcbSchedEnqueue(\thread));; + Guard C_Guard \hrs_htd \t_hrs \\<^sub>t \thread\ + (\thread :== h_val (hrs_mem \t_hrs) (Ptr &(\thread\[''tcbEPNext_C'']) :: tcb_C ptr ptr)) + OD)" + unfolding whileAnno_def +proof (induct ts) + case Nil + show ?case + apply (simp del: Collect_const) + apply (rule iffD1 [OF ccorres_expand_while_iff]) + apply (rule ccorres_tmp_lift2[where G'=UNIV and G''="\x. UNIV", simplified]) + apply ceqv + apply (simp add: ccorres_cond_iffs mapM_x_def sequence_x_def + dc_def[symmetric]) + apply (rule ccorres_guard_imp2, rule ccorres_return_Skip) + apply simp + done +next + case (Cons thread threads) + show ?case + apply (rule iffD1 [OF ccorres_expand_while_iff]) + apply (simp del: Collect_const + add: dc_def[symmetric] mapM_x_Cons) + apply (rule ccorres_guard_imp2) + apply (rule_tac xf'=thread_' in ccorres_abstract) + apply ceqv + apply (rule_tac P="rv' = tcb_ptr_to_ctcb_ptr thread" + in ccorres_gen_asm2) + apply (rule_tac P="tcb_ptr_to_ctcb_ptr thread \ Ptr 0" + in ccorres_gen_asm) + apply (clarsimp simp add: Collect_True ccorres_cond_iffs + simp del: Collect_const) + apply (rule_tac r'=dc and xf'=xfdc in ccorres_split_nothrow[where F=UNIV]) + apply (intro ccorres_rhs_assoc) + apply (ctac(no_vcg) add: setThreadState_ccorres) + apply (rule ccorres_add_return2) + apply (ctac(no_vcg) add: tcbSchedEnqueue_ccorres) + apply (rule_tac P="tcb_at' thread" + in ccorres_from_vcg[where P'=UNIV]) + apply (rule allI, rule conseqPre, vcg) + apply (clarsimp simp: return_def) + apply (drule obj_at_ko_at', clarsimp) + apply (erule cmap_relationE1 [OF cmap_relation_tcb]) + apply (erule ko_at_projectKO_opt) + apply (fastforce intro: typ_heap_simps) + apply (wp sts_running_valid_queues | simp)+ + apply (rule ceqv_refl) + apply (rule "Cons.hyps") + apply (wp sts_valid_objs' sts_sch_act sch_act_wf_lift hoare_vcg_const_Ball_lift + sts_running_valid_queues sts_st_tcb' setThreadState_oa_queued | simp)+ + + apply (vcg exspec=setThreadState_cslift_spec exspec=tcbSchedEnqueue_cslift_spec) + apply (clarsimp simp: tcb_at_not_NULL + Collect_const_mem valid_tcb_state'_def + ThreadState_Restart_def mask_def + valid_objs'_maxDomain valid_objs'_maxPriority) + apply (drule(1) obj_at_cslift_tcb) + apply (clarsimp simp: typ_heap_simps) + apply (rule conjI) + apply clarsimp + apply (frule rf_sr_cscheduler_relation) + apply (clarsimp simp: cscheduler_action_relation_def + st_tcb_at'_def + split: scheduler_action.split_asm) + apply (rename_tac word) + apply (frule_tac x=word in tcbSchedEnqueue_cslift_precond_discharge) + apply simp + apply clarsimp + apply clarsimp + apply clarsimp + apply clarsimp + apply (rule conjI) + apply (frule(3) tcbSchedEnqueue_cslift_precond_discharge) + apply clarsimp + apply clarsimp + apply (subst ep_queue_relation_shift, fastforce) + apply (drule_tac x="tcb_ptr_to_ctcb_ptr thread" + in fun_cong)+ + apply (clarsimp simp add: option_map2_def typ_heap_simps) + apply fastforce + done +qed + +lemma cancelAllIPC_ccorres: + "ccorres dc xfdc + (invs') (UNIV \ {s. epptr_' s = Ptr epptr}) [] + (cancelAllIPC epptr) (Call cancelAllIPC_'proc)" + apply (cinit lift: epptr_') + apply (rule ccorres_symb_exec_l [OF _ getEndpoint_inv _ empty_fail_getEndpoint]) + apply (rule_tac xf'=ret__unsigned_longlong_' + and val="case rv of IdleEP \ scast EPState_Idle + | RecvEP _ \ scast EPState_Recv | SendEP _ \ scast EPState_Send" + and R="ko_at' rv epptr" + in ccorres_symb_exec_r_known_rv_UNIV[where R'=UNIV]) + apply vcg + apply clarsimp + apply (erule cmap_relationE1 [OF cmap_relation_ep]) + apply (erule ko_at_projectKO_opt) + apply (clarsimp simp add: typ_heap_simps) + apply (simp add: cendpoint_relation_def Let_def + split: endpoint.split_asm) + apply ceqv + apply (rule_tac A="invs' and ko_at' rv epptr" + in ccorres_guard_imp2[where A'=UNIV]) + apply wpc + apply (rename_tac list) + apply (simp add: endpoint_state_defs + Collect_False Collect_True + ccorres_cond_iffs + del: Collect_const) + apply (rule ccorres_rhs_assoc)+ + apply csymbr + apply (rule ccorres_abstract_cleanup) + apply csymbr + apply (rule ccorres_rhs_assoc2, rule ccorres_rhs_assoc2) + apply (rule_tac r'=dc and xf'=xfdc + in ccorres_split_nothrow) + apply (rule_tac P="ko_at' (RecvEP list) epptr and invs'" + in ccorres_from_vcg[where P'=UNIV]) + apply (rule allI, rule conseqPre, vcg) + apply clarsimp + apply (rule cmap_relationE1 [OF cmap_relation_ep]) + apply assumption + apply (erule ko_at_projectKO_opt) + apply (clarsimp simp: typ_heap_simps setEndpoint_def) + apply (rule rev_bexI) + apply (rule setObject_eq; simp add: objBits_simps')[1] + apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def + carch_state_relation_def carch_globals_def + cmachine_state_relation_def + packed_heap_update_collapse_hrs) + apply (clarsimp simp: cpspace_relation_def + update_ep_map_tos typ_heap_simps') + apply (erule(2) cpspace_relation_ep_update_ep) + subgoal by (simp add: cendpoint_relation_def endpoint_state_defs) + subgoal by simp + apply (rule ceqv_refl) + apply (simp only: ccorres_seq_skip dc_def[symmetric]) + apply (rule ccorres_split_nothrow_novcg) + apply (rule cancel_all_ccorres_helper) + apply ceqv + apply (ctac add: rescheduleRequired_ccorres) + apply (wp weak_sch_act_wf_lift_linear + cancelAllIPC_mapM_x_valid_queues + | simp)+ + apply (rule mapM_x_wp', wp)+ + apply (wp sts_st_tcb') + apply (clarsimp split: if_split) + apply (rule mapM_x_wp', wp)+ + apply (clarsimp simp: valid_tcb_state'_def) + apply (simp add: guard_is_UNIV_def) + apply (wp set_ep_valid_objs' hoare_vcg_const_Ball_lift + weak_sch_act_wf_lift_linear) + apply vcg + apply (simp add: ccorres_cond_iffs dc_def[symmetric]) + apply (rule ccorres_return_Skip) + apply (rename_tac list) + apply (simp add: endpoint_state_defs + Collect_False Collect_True + ccorres_cond_iffs dc_def[symmetric] + del: Collect_const) + apply (rule ccorres_rhs_assoc)+ + apply csymbr + apply (rule ccorres_abstract_cleanup) + apply csymbr + apply (rule ccorres_rhs_assoc2, rule ccorres_rhs_assoc2) + apply (rule_tac r'=dc and xf'=xfdc + in ccorres_split_nothrow) + apply (rule_tac P="ko_at' (SendEP list) epptr and invs'" + in ccorres_from_vcg[where P'=UNIV]) + apply (rule allI, rule conseqPre, vcg) + apply clarsimp + apply (rule cmap_relationE1 [OF cmap_relation_ep]) + apply assumption + apply (erule ko_at_projectKO_opt) + apply (clarsimp simp: typ_heap_simps setEndpoint_def) + apply (rule rev_bexI) + apply (rule setObject_eq, simp_all add: objBits_simps')[1] + apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def + carch_state_relation_def carch_globals_def + cmachine_state_relation_def + packed_heap_update_collapse_hrs) + apply (clarsimp simp: cpspace_relation_def typ_heap_simps' + update_ep_map_tos) + apply (erule(2) cpspace_relation_ep_update_ep) + subgoal by (simp add: cendpoint_relation_def endpoint_state_defs) + subgoal by simp + apply (rule ceqv_refl) + apply (simp only: ccorres_seq_skip dc_def[symmetric]) + apply (rule ccorres_split_nothrow_novcg) + apply (rule cancel_all_ccorres_helper) + apply ceqv + apply (ctac add: rescheduleRequired_ccorres) + apply (wp cancelAllIPC_mapM_x_valid_queues) + apply (wp mapM_x_wp' weak_sch_act_wf_lift_linear + sts_st_tcb' | clarsimp simp: valid_tcb_state'_def split: if_split)+ + apply (simp add: guard_is_UNIV_def) + apply (wp set_ep_valid_objs' hoare_vcg_const_Ball_lift + weak_sch_act_wf_lift_linear) + apply vcg + apply (clarsimp simp: valid_ep'_def invs_valid_objs' invs_queues) + apply (rule cmap_relationE1[OF cmap_relation_ep], assumption) + apply (erule ko_at_projectKO_opt) + apply (frule obj_at_valid_objs', clarsimp+) + apply (clarsimp simp: projectKOs valid_obj'_def valid_ep'_def) + subgoal by (auto simp: typ_heap_simps cendpoint_relation_def + Let_def tcb_queue_relation'_def + invs_valid_objs' valid_objs'_maxDomain valid_objs'_maxPriority + intro!: obj_at_conj') + apply (clarsimp simp: guard_is_UNIV_def) + apply (wp getEndpoint_wp) + apply clarsimp + done + +lemma empty_fail_getNotification: + "empty_fail (getNotification ep)" + unfolding getNotification_def + by (auto intro: empty_fail_getObject) + +lemma cancelAllSignals_ccorres: + "ccorres dc xfdc + (invs') (UNIV \ {s. ntfnPtr_' s = Ptr ntfnptr}) [] + (cancelAllSignals ntfnptr) (Call cancelAllSignals_'proc)" + apply (cinit lift: ntfnPtr_') + apply (rule ccorres_symb_exec_l [OF _ get_ntfn_inv' _ empty_fail_getNotification]) + apply (rule_tac xf'=ret__unsigned_longlong_' + and val="case ntfnObj rv of IdleNtfn \ scast NtfnState_Idle + | ActiveNtfn _ \ scast NtfnState_Active | WaitingNtfn _ \ scast NtfnState_Waiting" + and R="ko_at' rv ntfnptr" + in ccorres_symb_exec_r_known_rv_UNIV[where R'=UNIV]) + apply vcg + apply clarsimp + apply (erule cmap_relationE1 [OF cmap_relation_ntfn]) + apply (erule ko_at_projectKO_opt) + apply (clarsimp simp add: typ_heap_simps) + apply (simp add: cnotification_relation_def Let_def + split: ntfn.split_asm) + apply ceqv + apply (rule_tac A="invs' and ko_at' rv ntfnptr" + in ccorres_guard_imp2[where A'=UNIV]) + apply wpc + apply (simp add: notification_state_defs ccorres_cond_iffs + dc_def[symmetric]) + apply (rule ccorres_return_Skip) + apply (simp add: notification_state_defs ccorres_cond_iffs + dc_def[symmetric]) + apply (rule ccorres_return_Skip) + apply (rename_tac list) + apply (simp add: notification_state_defs ccorres_cond_iffs + dc_def[symmetric] Collect_True + del: Collect_const) + apply (rule ccorres_rhs_assoc)+ + apply csymbr + apply (rule ccorres_abstract_cleanup) + apply csymbr + apply (rule ccorres_rhs_assoc2, rule ccorres_rhs_assoc2) + apply (rule_tac r'=dc and xf'=xfdc in ccorres_split_nothrow) + apply (rule_tac P="ko_at' rv ntfnptr and invs'" + in ccorres_from_vcg[where P'=UNIV]) + apply (rule allI, rule conseqPre, vcg) + apply clarsimp + apply (rule_tac x=ntfnptr in cmap_relationE1 [OF cmap_relation_ntfn], assumption) + apply (erule ko_at_projectKO_opt) + apply (clarsimp simp: typ_heap_simps setNotification_def) + apply (rule rev_bexI) + apply (rule setObject_eq, simp_all add: objBits_simps')[1] + apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def + carch_state_relation_def carch_globals_def + cmachine_state_relation_def + packed_heap_update_collapse_hrs) + apply (clarsimp simp: cpspace_relation_def typ_heap_simps' + update_ntfn_map_tos) + apply (erule(2) cpspace_relation_ntfn_update_ntfn) + subgoal by (simp add: cnotification_relation_def notification_state_defs Let_def) + subgoal by simp + apply (rule ceqv_refl) + apply (simp only: ccorres_seq_skip dc_def[symmetric]) + apply (rule ccorres_split_nothrow_novcg) + apply (rule cancel_all_ccorres_helper) + apply ceqv + apply (ctac add: rescheduleRequired_ccorres) + apply (wp cancelAllIPC_mapM_x_valid_queues) + apply (wp mapM_x_wp' weak_sch_act_wf_lift_linear + sts_st_tcb' | clarsimp simp: valid_tcb_state'_def split: if_split)+ + apply (simp add: guard_is_UNIV_def) + apply (wp set_ntfn_valid_objs' hoare_vcg_const_Ball_lift + weak_sch_act_wf_lift_linear) + apply vcg + apply clarsimp + apply (rule cmap_relationE1[OF cmap_relation_ntfn], assumption) + apply (erule ko_at_projectKO_opt) + apply (frule obj_at_valid_objs', clarsimp+) + apply (clarsimp simp add: valid_obj'_def valid_ntfn'_def projectKOs) + subgoal by (auto simp: typ_heap_simps cnotification_relation_def + Let_def tcb_queue_relation'_def + invs_valid_objs' valid_objs'_maxDomain valid_objs'_maxPriority + intro!: obj_at_conj') + apply (clarsimp simp: guard_is_UNIV_def) + apply (wp getNotification_wp) + apply clarsimp + done + +lemma tcb_queue_concat: + "tcb_queue_relation getNext getPrev mp (xs @ z # ys) qprev qhead + \ tcb_queue_relation getNext getPrev mp (z # ys) + (tcb_ptr_to_ctcb_ptr (last ((ctcb_ptr_to_tcb_ptr qprev) # xs))) (tcb_ptr_to_ctcb_ptr z)" + apply (induct xs arbitrary: qprev qhead) + apply clarsimp + apply clarsimp + apply (elim meta_allE, drule(1) meta_mp) + apply (clarsimp cong: if_cong) + done + +lemma tcb_fields_ineq_helper: + "\ tcb_at' (ctcb_ptr_to_tcb_ptr x) s; tcb_at' (ctcb_ptr_to_tcb_ptr y) s \ \ + &(x\[''tcbSchedPrev_C'']) \ &(y\[''tcbSchedNext_C''])" + apply (clarsimp dest!: tcb_aligned'[OF obj_at'_weakenE, OF _ TrueI] + ctcb_ptr_to_tcb_ptr_aligned) + apply (clarsimp simp: field_lvalue_def ctcb_size_bits_def) + apply (subgoal_tac "is_aligned (ptr_val y - ptr_val x) 9" (*ctcb_size_bits*)) + apply (drule sym, fastforce simp: is_aligned_def dvd_def) + apply (erule(1) aligned_sub_aligned) + apply (simp add: word_bits_conv) + done + +end + +primrec + tcb_queue_relation2 :: "(tcb_C \ tcb_C ptr) \ (tcb_C \ tcb_C ptr) + \ (tcb_C ptr \ tcb_C) \ tcb_C ptr list + \ tcb_C ptr \ tcb_C ptr \ bool" +where + "tcb_queue_relation2 getNext getPrev hp [] before after = True" +| "tcb_queue_relation2 getNext getPrev hp (x # xs) before after = + (\tcb. hp x = Some tcb \ getPrev tcb = before + \ getNext tcb = hd (xs @ [after]) + \ tcb_queue_relation2 getNext getPrev hp xs x after)" + +lemma use_tcb_queue_relation2: + "tcb_queue_relation getNext getPrev hp xs qprev qhead + = (tcb_queue_relation2 getNext getPrev hp + (map tcb_ptr_to_ctcb_ptr xs) qprev (tcb_Ptr 0) + \ qhead = (hd (map tcb_ptr_to_ctcb_ptr xs @ [tcb_Ptr 0])))" + apply (induct xs arbitrary: qhead qprev) + apply simp + apply (simp add: conj_comms cong: conj_cong) + done + +lemma tcb_queue_relation2_concat: + "tcb_queue_relation2 getNext getPrev hp + (xs @ ys) before after + = (tcb_queue_relation2 getNext getPrev hp + xs before (hd (ys @ [after])) + \ tcb_queue_relation2 getNext getPrev hp + ys (last (before # xs)) after)" + apply (induct xs arbitrary: before) + apply simp + apply (rename_tac x xs before) + apply (simp split del: if_split) + apply (case_tac "hp x") + apply simp + apply simp + done + +lemma tcb_queue_relation2_cong: + "\queue = queue'; before = before'; after = after'; + \p. p \ set queue' \ mp p = mp' p\ + \ tcb_queue_relation2 getNext getPrev mp queue before after = + tcb_queue_relation2 getNext getPrev mp' queue' before' after'" + using [[hypsubst_thin = true]] + apply clarsimp + apply (induct queue' arbitrary: before') + apply simp+ + done + +context kernel_m begin + +lemma setThreadState_ccorres_valid_queues'_simple: + "ccorres dc xfdc (\s. tcb_at' thread s \ valid_queues' s \ \ runnable' st \ sch_act_simple s) + ({s'. (\cl fl. cthread_state_relation_lifted st (cl\tsType_CL := ts_' s' && mask 4\, fl))} + \ {s. tptr_' s = tcb_ptr_to_ctcb_ptr thread}) [] + (setThreadState st thread) (Call setThreadState_'proc)" + apply (cinit lift: tptr_' cong add: call_ignore_cong) + apply (ctac (no_vcg) add: threadSet_tcbState_simple_corres) + apply (ctac add: scheduleTCB_ccorres_valid_queues'_simple) + apply (wp threadSet_valid_queues'_and_not_runnable') + apply (clarsimp simp: weak_sch_act_wf_def valid_queues'_def) + done + +lemma updateRestartPC_ccorres: + "ccorres dc xfdc (tcb_at' thread) \\tcb = tcb_ptr_to_ctcb_ptr thread \ hs + (updateRestartPC thread) (Call updateRestartPC_'proc)" + apply (cinit lift: tcb_') + apply (subst asUser_bind_distrib; (wp add: empty_fail_getRegister)?) + apply (ctac (no_vcg) add: getRegister_ccorres) + apply (ctac (no_vcg) add: setRegister_ccorres) + apply wpsimp+ + apply (simp add: RISCV64_H.faultRegister_def RISCV64_H.nextInstructionRegister_def + RISCV64.faultRegister_def RISCV64.nextInstructionRegister_def) + done + +crunches updateRestartPC + for valid_queues'[wp]: valid_queues' + and sch_act_simple[wp]: sch_act_simple + and valid_queues[wp]: Invariants_H.valid_queues + and valid_objs'[wp]: valid_objs' + and tcb_at'[wp]: "tcb_at' p" + +lemma suspend_ccorres: + assumes cteDeleteOne_ccorres: + "\w slot. ccorres dc xfdc + (invs' and cte_wp_at' (\ct. w = -1 \ cteCap ct = NullCap + \ (\cap'. ccap_relation (cteCap ct) cap' \ cap_get_tag cap' = w)) slot) + ({s. gs_get_assn cteDeleteOne_'proc (ghost'state_' (globals s)) = w} + \ {s. slot_' s = Ptr slot}) [] + (cteDeleteOne slot) (Call cteDeleteOne_'proc)" + shows + "ccorres dc xfdc + (invs' and sch_act_simple and tcb_at' thread and (\s. thread \ ksIdleThread s)) + (UNIV \ {s. target_' s = tcb_ptr_to_ctcb_ptr thread}) [] + (suspend thread) (Call suspend_'proc)" + apply (cinit lift: target_') + apply (ctac(no_vcg) add: cancelIPC_ccorres1 [OF cteDeleteOne_ccorres]) + apply (rule getThreadState_ccorres_foo) + apply (rename_tac threadState) + apply (rule ccorres_move_c_guard_tcb) + apply (rule_tac xf'=ret__unsigned_longlong_' + and val="thread_state_to_tsType threadState" + and R="st_tcb_at' ((=) threadState) thread" + and R'=UNIV + in + ccorres_symb_exec_r_known_rv) + apply clarsimp + apply (rule conseqPre, vcg) + apply (clarsimp simp: st_tcb_at'_def) + apply (frule (1) obj_at_cslift_tcb) + apply (clarsimp simp: typ_heap_simps ctcb_relation_thread_state_to_tsType) + apply ceqv + supply Collect_const[simp del] + apply (rule ccorres_split_nothrow) + apply (rule ccorres_cond[where R=\ and xf=xfdc]) + apply clarsimp + apply (rule iffI) + apply simp + apply (erule thread_state_to_tsType.elims; simp add: StrictC'_thread_state_defs) + apply (ctac (no_vcg) add: updateRestartPC_ccorres) + apply (rule ccorres_return_Skip) + apply ceqv + apply (ctac(no_vcg) add: setThreadState_ccorres_valid_queues'_simple) + apply (ctac add: tcbSchedDequeue_ccorres') + apply (rule_tac Q="\_. + (\s. \t' d p. (t' \ set (ksReadyQueues s (d, p)) \ + obj_at' (\tcb. tcbQueued tcb \ tcbDomain tcb = d + \ tcbPriority tcb = p) t' s \ + (t' \ thread \ st_tcb_at' runnable' t' s)) \ + distinct (ksReadyQueues s (d, p))) and valid_queues' and valid_objs' and tcb_at' thread" + in hoare_post_imp) + apply clarsimp + apply (drule_tac x="t" in spec) + apply (drule_tac x=d in spec) + apply (drule_tac x=p in spec) + apply (clarsimp elim!: obj_at'_weakenE simp: inQ_def) + apply (wp sts_valid_queues_partial)[1] + apply clarsimp + apply (wpsimp simp: valid_tcb_state'_def) + apply clarsimp + apply (rule conseqPre, vcg exspec=updateRestartPC_modifies) + apply (rule subset_refl) + apply clarsimp + apply (rule conseqPre, vcg) + apply (rule subset_refl) + apply (rule hoare_strengthen_post) + apply (rule hoare_vcg_conj_lift) + apply (rule hoare_vcg_conj_lift) + apply (rule cancelIPC_sch_act_simple) + apply (rule cancelIPC_tcb_at'[where t=thread]) + apply (rule delete_one_conc_fr.cancelIPC_invs) + apply (fastforce simp: invs_valid_queues' invs_queues invs_valid_objs' + valid_tcb_state'_def) + apply (auto simp: "StrictC'_thread_state_defs") + done + +lemma cap_to_H_NTFNCap_tag: + "\ cap_to_H cap = NotificationCap word1 word2 a b; + cap_lift C_cap = Some cap \ \ + cap_get_tag C_cap = scast cap_notification_cap" + apply (clarsimp simp: cap_to_H_def Let_def split: cap_CL.splits if_split_asm) + by (simp_all add: Let_def cap_lift_def split: if_splits) + +lemmas ccorres_pre_getBoundNotification = ccorres_pre_threadGet [where f=tcbBoundNotification, folded getBoundNotification_def] + +lemma option_to_ptr_not_NULL: + "option_to_ptr x \ NULL \ x \ None" + by (auto simp: option_to_ptr_def option_to_0_def split: option.splits) + +lemma doUnbindNotification_ccorres: + "ccorres dc xfdc (invs' and tcb_at' tcb) + (UNIV \ {s. ntfnPtr_' s = ntfn_Ptr ntfnptr} \ {s. tcbptr_' s = tcb_ptr_to_ctcb_ptr tcb}) [] + (do ntfn \ getNotification ntfnptr; doUnbindNotification ntfnptr ntfn tcb od) + (Call doUnbindNotification_'proc)" + apply (cinit' lift: ntfnPtr_' tcbptr_') + apply (rule ccorres_symb_exec_l [OF _ get_ntfn_inv' _ empty_fail_getNotification]) + apply (rule_tac P="invs' and ko_at' rv ntfnptr" and P'=UNIV + in ccorres_split_nothrow_novcg) + apply (rule ccorres_from_vcg[where rrel=dc and xf=xfdc]) + apply (rule allI, rule conseqPre, vcg) + apply (clarsimp simp: option_to_ptr_def option_to_0_def) + apply (frule cmap_relation_ntfn) + apply (erule (1) cmap_relation_ko_atE) + apply (rule conjI) + apply (erule h_t_valid_clift) + apply (clarsimp simp: setNotification_def split_def) + apply (rule bexI [OF _ setObject_eq]) + apply (simp add: rf_sr_def cstate_relation_def Let_def init_def + typ_heap_simps' + cpspace_relation_def update_ntfn_map_tos) + apply (elim conjE) + apply (intro conjI) + \ \tcb relation\ + apply (rule cpspace_relation_ntfn_update_ntfn, assumption+) + apply (clarsimp simp: cnotification_relation_def Let_def + mask_def [where n=2] NtfnState_Waiting_def) + apply (case_tac "ntfnObj rv", ((simp add: option_to_ctcb_ptr_def)+)[4]) + subgoal by (simp add: carch_state_relation_def) + subgoal by (simp add: cmachine_state_relation_def) + subgoal by (simp add: h_t_valid_clift_Some_iff) + subgoal by (simp add: objBits_simps') + subgoal by (simp add: objBits_simps) + apply assumption + apply ceqv + apply (rule ccorres_move_c_guard_tcb) + apply (simp add: setBoundNotification_def) + apply (rule_tac P'="\" and P="\" + in threadSet_ccorres_lemma3[unfolded dc_def]) + apply vcg + apply simp + apply (erule(1) rf_sr_tcb_update_no_queue2) + apply (simp add: typ_heap_simps')+ + sorry (* FIXME RISCV + apply (simp add: tcb_cte_cases_def) + apply (simp add: ctcb_relation_def option_to_ptr_def option_to_0_def) + apply (simp add: invs'_def valid_state'_def) + apply (wp get_ntfn_ko' | simp add: guard_is_UNIV_def)+ + done + *) + +lemma doUnbindNotification_ccorres': + "ccorres dc xfdc (invs' and tcb_at' tcb and ko_at' ntfn ntfnptr) + (UNIV \ {s. ntfnPtr_' s = ntfn_Ptr ntfnptr} \ {s. tcbptr_' s = tcb_ptr_to_ctcb_ptr tcb}) [] + (doUnbindNotification ntfnptr ntfn tcb) + (Call doUnbindNotification_'proc)" + apply (cinit' lift: ntfnPtr_' tcbptr_') + apply (rule_tac P="invs' and ko_at' ntfn ntfnptr" and P'=UNIV + in ccorres_split_nothrow_novcg) + apply (rule ccorres_from_vcg[where rrel=dc and xf=xfdc]) + apply (rule allI, rule conseqPre, vcg) + apply (clarsimp simp: option_to_ptr_def option_to_0_def) + apply (frule cmap_relation_ntfn) + apply (erule (1) cmap_relation_ko_atE) + apply (rule conjI) + apply (erule h_t_valid_clift) + apply (clarsimp simp: setNotification_def split_def) + apply (rule bexI [OF _ setObject_eq]) + apply (simp add: rf_sr_def cstate_relation_def Let_def init_def + typ_heap_simps' + cpspace_relation_def update_ntfn_map_tos) + apply (elim conjE) + apply (intro conjI) + \ \tcb relation\ + apply (rule cpspace_relation_ntfn_update_ntfn, assumption+) + apply (clarsimp simp: cnotification_relation_def Let_def + mask_def [where n=2] NtfnState_Waiting_def) + apply (fold_subgoals (prefix))[2] + subgoal premises prems using prems + by (case_tac "ntfnObj ntfn", (simp add: option_to_ctcb_ptr_def)+) + subgoal by (simp add: carch_state_relation_def) + subgoal by (simp add: cmachine_state_relation_def) + subgoal by (simp add: h_t_valid_clift_Some_iff) + subgoal by (simp add: objBits_simps') + subgoal by (simp add: objBits_simps) + apply assumption + apply ceqv + apply (rule ccorres_move_c_guard_tcb) + apply (simp add: setBoundNotification_def) + apply (rule_tac P'="\" and P="\" + in threadSet_ccorres_lemma3[unfolded dc_def]) + apply vcg + apply simp + apply (erule(1) rf_sr_tcb_update_no_queue2) + apply (simp add: typ_heap_simps')+ + sorry (* FIXME RISCV + apply (simp add: tcb_cte_cases_def) + apply (simp add: ctcb_relation_def option_to_ptr_def option_to_0_def) + apply (simp add: invs'_def valid_state'_def) + apply (wp get_ntfn_ko' | simp add: guard_is_UNIV_def)+ + done + *) + + +lemma unbindNotification_ccorres: + "ccorres dc xfdc + (invs') (UNIV \ {s. tcb_' s = tcb_ptr_to_ctcb_ptr tcb}) [] + (unbindNotification tcb) (Call unbindNotification_'proc)" + apply (cinit lift: tcb_') + apply (rule_tac xf'=ntfnPtr_' + and r'="\rv rv'. rv' = option_to_ptr rv \ rv \ Some 0" + in ccorres_split_nothrow) + apply (simp add: getBoundNotification_def) + apply (rule_tac P="no_0_obj' and valid_objs'" in threadGet_vcg_corres_P) + apply (rule allI, rule conseqPre, vcg) + apply clarsimp + apply (drule obj_at_ko_at', clarsimp) + apply (drule spec, drule(1) mp, clarsimp) + apply (clarsimp simp: typ_heap_simps ctcb_relation_def) + apply (drule(1) ko_at_valid_objs', simp add: projectKOs) + apply (clarsimp simp: option_to_ptr_def option_to_0_def projectKOs + valid_obj'_def valid_tcb'_def) + apply ceqv + apply simp + apply wpc + apply (rule ccorres_cond_false) + apply (rule ccorres_return_Skip[unfolded dc_def]) + apply (rule ccorres_cond_true) + apply (ctac (no_vcg) add: doUnbindNotification_ccorres[unfolded dc_def, simplified]) + apply (wp gbn_wp') + apply vcg + apply (clarsimp simp: option_to_ptr_def option_to_0_def pred_tcb_at'_def + obj_at'_weakenE[OF _ TrueI] + split: option.splits) + apply (clarsimp simp: invs'_def valid_pspace'_def valid_state'_def) + done + + +lemma unbindMaybeNotification_ccorres: + "ccorres dc xfdc (invs') (UNIV \ {s. ntfnPtr_' s = ntfn_Ptr ntfnptr}) [] + (unbindMaybeNotification ntfnptr) (Call unbindMaybeNotification_'proc)" + apply (cinit lift: ntfnPtr_') + apply (rule ccorres_symb_exec_l [OF _ get_ntfn_inv' _ empty_fail_getNotification]) + apply (rule ccorres_rhs_assoc2) + apply (rule_tac P="ntfnBoundTCB rv \ None \ + option_to_ctcb_ptr (ntfnBoundTCB rv) \ NULL" + in ccorres_gen_asm) + apply (rule_tac xf'=boundTCB_' + and val="option_to_ctcb_ptr (ntfnBoundTCB rv)" + and R="ko_at' rv ntfnptr and valid_bound_tcb' (ntfnBoundTCB rv)" + in ccorres_symb_exec_r_known_rv_UNIV[where R'=UNIV]) + apply vcg + apply clarsimp + apply (erule cmap_relationE1[OF cmap_relation_ntfn]) + apply (erule ko_at_projectKO_opt) + apply (clarsimp simp: typ_heap_simps cnotification_relation_def Let_def) + apply ceqv + apply wpc + apply (rule ccorres_cond_false) + apply (rule ccorres_return_Skip) + apply (rule ccorres_cond_true) + apply (rule ccorres_call[where xf'=xfdc]) + apply (rule doUnbindNotification_ccorres'[simplified]) + apply simp + apply simp + apply simp + apply (clarsimp simp add: guard_is_UNIV_def option_to_ctcb_ptr_def ) + apply (wp getNotification_wp) + apply (clarsimp ) + apply (frule (1) ko_at_valid_ntfn'[OF _ invs_valid_objs']) + by (auto simp: valid_ntfn'_def valid_bound_tcb'_def obj_at'_def projectKOs + objBitsKO_def is_aligned_def option_to_ctcb_ptr_def tcb_at_not_NULL + split: ntfn.splits) + +(* FIXME RISCV: this definition needs to be reviewed, see sorry in finaliseCap_ccorres and + the return relation of deletingIRQHandler_ccorres *) +(* TODO: move *) +definition + irq_opt_relation_def: + "irq_opt_relation (airq :: (6 word) option) (cirq :: machine_word) \ + case airq of + Some irq \ (cirq = ucast irq \ + irq \ ucast irqInvalid \ + ucast irq \ UCAST(32 signed \ 6) Kernel_C.maxIRQ) + | None \ cirq = ucast irqInvalid" + +lemma finaliseCap_True_cases_ccorres: + "\final. isEndpointCap cap \ isNotificationCap cap + \ isReplyCap cap \ isDomainCap cap \ cap = NullCap \ + ccorres (\rv rv'. ccap_relation (fst rv) (finaliseCap_ret_C.remainder_C rv') + \ ccap_relation (snd rv) (finaliseCap_ret_C.cleanupInfo_C rv')) + ret__struct_finaliseCap_ret_C_' + (invs') (UNIV \ {s. ccap_relation cap (cap_' s)} \ {s. final_' s = from_bool final} + \ {s. exposed_' s = from_bool flag \ \dave has name wrong\}) [] + (finaliseCap cap final flag) (Call finaliseCap_'proc)" + apply (subgoal_tac "\ isArchCap \ cap") + prefer 2 + apply (clarsimp simp: isCap_simps) + apply (cinit lift: cap_' final_' exposed_' cong: call_ignore_cong) + apply csymbr + apply (simp add: cap_get_tag_isCap Collect_False del: Collect_const) + apply (fold case_bool_If) + apply (simp add: false_def) + apply csymbr + apply wpc + apply (simp add: cap_get_tag_isCap ccorres_cond_univ_iff Let_def) + apply (rule ccorres_rhs_assoc)+ + apply (rule ccorres_split_nothrow_novcg) + apply (simp add: when_def) + apply (rule ccorres_cond2) + apply (clarsimp simp: Collect_const_mem from_bool_0) + apply csymbr + apply (rule ccorres_call[where xf'=xfdc], rule cancelAllIPC_ccorres) + apply simp + apply simp + apply simp + apply (rule ccorres_from_vcg[where P=\ and P'=UNIV]) + apply (simp add: return_def, vcg) + apply (rule ceqv_refl) + apply (rule ccorres_rhs_assoc2, rule ccorres_rhs_assoc2, + rule ccorres_rhs_assoc2, rule ccorres_rhs_assoc2, + rule ccorres_split_throws) + apply (rule ccorres_from_vcg_throws[where P=\ and P'=UNIV]) + apply (rule allI, rule conseqPre, vcg) + apply (clarsimp simp add: return_def ccap_relation_NullCap_iff + irq_opt_relation_def) + apply vcg + apply wp + apply (simp add: guard_is_UNIV_def) + apply wpc + apply (simp add: cap_get_tag_isCap Let_def + ccorres_cond_empty_iff ccorres_cond_univ_iff) + apply (rule ccorres_rhs_assoc)+ + apply (rule ccorres_split_nothrow_novcg) + apply (simp add: when_def) + apply (rule ccorres_cond2) + apply (clarsimp simp: Collect_const_mem from_bool_0) + apply (subgoal_tac "cap_get_tag capa = scast cap_notification_cap") prefer 2 + apply (clarsimp simp: ccap_relation_def isNotificationCap_def) + apply (case_tac cap, simp_all)[1] + apply (clarsimp simp: option_map_def split: option.splits) + apply (drule (2) cap_to_H_NTFNCap_tag[OF sym]) + apply (rule ccorres_rhs_assoc) + apply (rule ccorres_rhs_assoc) + apply csymbr + apply csymbr + apply (ctac (no_vcg) add: unbindMaybeNotification_ccorres) + apply (rule ccorres_call[where xf'=xfdc], rule cancelAllSignals_ccorres) + apply simp + apply simp + apply simp + apply (wp | wpc | simp add: guard_is_UNIV_def)+ + apply (rule ccorres_return_Skip') + apply (rule ceqv_refl) + apply (rule ccorres_rhs_assoc2, rule ccorres_rhs_assoc2, + rule ccorres_rhs_assoc2, rule ccorres_rhs_assoc2, + rule ccorres_split_throws) + apply (rule ccorres_from_vcg_throws[where P=\ and P'=UNIV]) + apply (rule allI, rule conseqPre, vcg) + apply (clarsimp simp add: return_def ccap_relation_NullCap_iff + irq_opt_relation_def) + apply vcg + apply wp + apply (simp add: guard_is_UNIV_def) + apply wpc + apply (simp add: cap_get_tag_isCap Let_def + ccorres_cond_empty_iff ccorres_cond_univ_iff) + apply (rule ccorres_rhs_assoc2, rule ccorres_rhs_assoc2, + rule ccorres_split_throws) + apply (rule ccorres_from_vcg_throws[where P=\ and P'=UNIV]) + apply (rule allI, rule conseqPre, vcg) + apply (clarsimp simp add: return_def ccap_relation_NullCap_iff + irq_opt_relation_def) + apply vcg + apply wpc + apply (simp add: cap_get_tag_isCap Let_def + ccorres_cond_empty_iff ccorres_cond_univ_iff) + apply (rule ccorres_rhs_assoc2, rule ccorres_rhs_assoc2, + rule ccorres_split_throws) + apply (rule ccorres_from_vcg_throws[where P=\ and P'=UNIV]) + apply (rule allI, rule conseqPre, vcg) + apply (clarsimp simp add: return_def ccap_relation_NullCap_iff) + apply (clarsimp simp add: irq_opt_relation_def) + apply vcg + \ \NullCap case by exhaustion\ + apply (simp add: cap_get_tag_isCap Let_def + ccorres_cond_empty_iff ccorres_cond_univ_iff) + apply (rule ccorres_rhs_assoc2, rule ccorres_rhs_assoc2, + rule ccorres_split_throws) + apply (rule ccorres_from_vcg_throws[where P=\ and P'=UNIV]) + apply (rule allI, rule conseqPre, vcg) + apply (clarsimp simp add: return_def ccap_relation_NullCap_iff + irq_opt_relation_def) + apply vcg + apply (clarsimp simp: Collect_const_mem cap_get_tag_isCap) + apply (rule TrueI conjI impI TrueI)+ + apply (frule cap_get_tag_to_H, erule(1) cap_get_tag_isCap [THEN iffD2]) + apply (clarsimp simp: invs'_def valid_state'_def valid_pspace'_def isNotificationCap_def + isEndpointCap_def valid_obj'_def projectKOs valid_ntfn'_def + valid_bound_tcb'_def + dest!: obj_at_valid_objs') + apply clarsimp + apply (frule cap_get_tag_to_H, erule(1) cap_get_tag_isCap [THEN iffD2]) + apply clarsimp + done + +lemma finaliseCap_True_standin_ccorres: + "\final. + ccorres (\rv rv'. ccap_relation (fst rv) (finaliseCap_ret_C.remainder_C rv') + \ ccap_relation (snd rv) (finaliseCap_ret_C.cleanupInfo_C rv')) + ret__struct_finaliseCap_ret_C_' + (invs') (UNIV \ {s. ccap_relation cap (cap_' s)} \ {s. final_' s = from_bool final} + \ {s. exposed_' s = from_bool True \ \dave has name wrong\}) [] + (finaliseCapTrue_standin cap final) (Call finaliseCap_'proc)" + unfolding finaliseCapTrue_standin_simple_def + apply (case_tac "P :: bool" for P) + apply (erule finaliseCap_True_cases_ccorres) + apply (simp add: finaliseCap_def ccorres_fail') + done + +lemma offset_xf_for_sequence: + "\s f. offset_' (offset_'_update f s) = f (offset_' s) + \ globals (offset_'_update f s) = globals s" + by simp + +lemma invs'_invs_no_cicd': + "invs' s \ all_invs_but_ct_idle_or_in_cur_domain' s" + by (simp add: invs'_invs_no_cicd) + +lemma ucast_asid_high_bits_is_shift': + "asid \ mask asid_bits \ ucast (asid_high_bits_of (UCAST (machine_word_len \ asid_len) asid)) = (asid >> asid_low_bits)" + apply (simp add: asid_high_bits_of_def) + apply (subst ucast_ucast_mask2; (simp add: is_down)?) + apply (subst mask_eq_ucast_shiftr) + apply (simp add: asid_bits_def) + subgoal sorry + apply (simp add: asid_low_bits_def asid_bits_def) + sorry (* FIXME RISCV: looks ok, but proof is fiddly, and currently unused *) + +lemma deleteASIDPool_ccorres: + "ccorres dc xfdc (invs' and (\_. base < 2 ^ asid_bits \ pool \ 0)) + (UNIV \ {s. asid_base_' s = base} \ {s. pool_' s = Ptr pool}) [] + (deleteASIDPool base pool) (Call deleteASIDPool_'proc)" + apply (rule ccorres_gen_asm) + apply (cinit lift: asid_base_' pool_' simp: whileAnno_def) + apply (rule ccorres_assert) + apply (clarsimp simp: liftM_def dc_def[symmetric] fun_upd_def[symmetric] + when_def + simp del: Collect_const) + apply (rule ccorres_Guard)+ + apply (rule ccorres_pre_gets_riscvKSASIDTable_ksArchState) + apply (rule_tac R="\s. rv = riscvKSASIDTable (ksArchState s)" in ccorres_cond2) + apply clarsimp + apply (subst rf_sr_riscvKSASIDTable, assumption) + apply (simp add: asid_high_bits_word_bits) + apply (rule shiftr_less_t2n) + apply_trace (simp add: asid_low_bits_def asid_high_bits_def) + sorry (* FIXME RISCV + apply (subst ucast_asid_high_bits_is_shift') + apply (simp add: mask_def, simp add: asid_bits_def) + apply (simp add: option_to_ptr_def option_to_0_def split: option.split) + apply (subst ucast_asid_high_bits_is_shift') + apply (simp add: mask_def, simp add: asid_bits_def) + apply (rule ccorres_Guard_Seq ccorres_rhs_assoc)+ + apply (rule ccorres_pre_getObject_asidpool) + apply (rename_tac poolKO) + apply (rule ccorres_move_const_guard)+ + apply (rule ccorres_split_nothrow_novcg_dc) + apply (rule_tac P="\s. rv = riscvKSASIDTable (ksArchState s)" + in ccorres_from_vcg[where P'=UNIV]) + apply (rule allI, rule conseqPre, vcg) + apply (clarsimp simp: simpler_modify_def) + apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def + carch_state_relation_def cmachine_state_relation_def + carch_globals_def h_t_valid_clift_Some_iff) + apply (erule array_relation_update[unfolded fun_upd_def]) + apply (simp add: asid_high_bits_of_def unat_ucast asid_low_bits_def) + apply (rule sym, rule nat_mod_eq') + apply (rule order_less_le_trans, rule iffD1[OF word_less_nat_alt]) + apply (rule shiftr_less_t2n[where m=3]) + subgoal by simp + subgoal by simp + subgoal by (simp add: option_to_ptr_def option_to_0_def) + subgoal by (simp add: asid_high_bits_def) + apply (rule ccorres_pre_getCurThread) + apply (ctac add: setVMRoot_ccorres) + apply wp + apply (simp add: guard_is_UNIV_def) + apply (simp add: pred_conj_def fun_upd_def[symmetric] + cur_tcb'_def[symmetric]) + apply (strengthen invs'_invs_no_cicd', strengthen invs_asid_update_strg') + apply (rule mapM_x_wp') + apply (rule hoare_pre, wp) + apply simp + apply (simp add: guard_is_UNIV_def Kernel_C.asidLowBits_def + word_sle_def word_sless_def Collect_const_mem + mask_def asid_bits_def plus_one_helper + asid_shiftr_low_bits_less) + apply (rule ccorres_return_Skip) + apply (simp add: Kernel_C.asidLowBits_def + word_sle_def word_sless_def) + apply (auto simp: asid_shiftr_low_bits_less Collect_const_mem + mask_def asid_bits_def plus_one_helper) + done + *) + + +lemma deleteASID_ccorres: + "ccorres dc xfdc (invs' and K (asid < 2 ^ asid_bits) and K (vs \ 0)) + ({s. asid___unsigned_long_' s = asid} \ {s. vspace_' s = Ptr vs}) [] + (deleteASID asid vs) (Call deleteASID_'proc)" + apply (cinit lift: asid___unsigned_long_' vspace_' cong: call_ignore_cong) + apply (rule ccorres_Guard_Seq)+ + sorry (* FIXME RISCV + apply (rule_tac r'="\rv rv'. case rv (ucast (asid_high_bits_of asid)) of + None \ rv' = NULL + | Some v \ rv' = Ptr v \ rv' \ NULL" + and xf'="poolPtr_'" in ccorres_split_nothrow) + apply (rule_tac P="invs' and K (asid < 2 ^ 12)" + and P'=UNIV in ccorres_from_vcg) + apply (rule allI, rule conseqPre, vcg) + apply (clarsimp simp: simpler_gets_def Let_def) + apply (erule(1) getKSASIDTable_ccorres_stuff) + apply (simp add: asid_high_bits_of_def + asidLowBits_def Kernel_C.asidLowBits_def + asid_low_bits_def unat_ucast) + apply (rule sym, rule Divides.mod_less, simp) + apply (rule unat_less_power[where sz=3, simplified]) + apply (simp add: word_bits_conv) + apply (rule shiftr_less_t2n[where m=3, simplified]) + apply simp + apply (rule order_less_le_trans, rule ucast_less) + apply simp + apply (simp add: asid_high_bits_def) + apply ceqv + apply wpc + apply (simp add: ccorres_cond_iffs dc_def[symmetric] + Collect_False + del: Collect_const + cong: call_ignore_cong) + apply (rule ccorres_return_Skip) + apply (clarsimp simp: dc_def[symmetric] when_def + Collect_True liftM_def + cong: conj_cong call_ignore_cong + del: Collect_const) + apply ccorres_rewrite + apply (rule ccorres_rhs_assoc)+ + apply (rule ccorres_pre_getObject_asidpool) + apply (rule ccorres_Guard_Seq[where F=ArrayBounds]) + apply (rule ccorres_move_c_guard_ap) + apply (rule ccorres_Guard_Seq)+ + apply (rename_tac pool) + apply (rule ccorres_rhs_assoc2) + apply (rule ccorres_rhs_assoc2) + apply (rule ccorres_rhs_assoc2) + apply (rule_tac xf'=ret__int_' + and val="from_bool (inv ASIDPool pool (ucast (asid_low_bits_of asid)) + = Some vs)" + and R="ko_at' pool x2 and K (vs \ 0)" + in ccorres_symb_exec_r_known_rv_UNIV[where R'=UNIV]) + apply (vcg, clarsimp) + apply (clarsimp dest!: rf_sr_cpspace_asidpool_relation) + apply (erule(1) cmap_relation_ko_atE) + apply (clarsimp simp: typ_heap_simps casid_pool_relation_def + array_relation_def asid_low_bits_of_mask_eq + split: asidpool.split_asm asid_pool_C.split_asm) + apply (drule_tac x="asid && mask asid_low_bits" in spec) + apply (simp add: asid_low_bits_def Kernel_C.asidLowBits_def + mask_def word_and_le1 asid_map_relation_def) + apply (rule conjI, fastforce simp: asid_map_lifts from_bool_def case_bool_If inv_ASIDPool) + apply (fastforce simp: from_bool_def case_bool_If inv_ASIDPool asid_map_lift_def + split: option.split_asm asid_map_CL.split_asm if_split_asm) + apply ceqv + apply (rule ccorres_cond2[where R=\]) + apply (simp add: Collect_const_mem from_bool_0) + apply (rule ccorres_rhs_assoc)+ + apply (ctac (no_vcg) add: hwASIDInvalidate_ccorres) + apply csymbr + apply (rule ccorres_Guard_Seq[where F=ArrayBounds]) + apply (rule ccorres_move_c_guard_ap) + apply (rule ccorres_Guard_Seq)+ + apply (rule ccorres_split_nothrow_novcg_dc) + apply (rule_tac P="ko_at' pool x2" in ccorres_from_vcg[where P'=UNIV]) + apply (rule allI, rule conseqPre, vcg) + apply clarsimp + apply (rule cmap_relationE1[OF rf_sr_cpspace_asidpool_relation], + assumption, erule ko_at_projectKO_opt) + apply (rule bexI [OF _ setObject_eq], + simp_all add: objBits_simps archObjSize_def pageBits_def)[1] + apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def typ_heap_simps) + apply (rule conjI) + apply (clarsimp simp: cpspace_relation_def typ_heap_simps' + update_asidpool_map_tos + update_asidpool_map_to_asidpools) + apply (rule cmap_relation_updI, simp_all)[1] + apply (simp add: casid_pool_relation_def fun_upd_def[symmetric] + inv_ASIDPool + split: asidpool.split_asm asid_pool_C.split_asm) + apply (erule array_relation_update) + subgoal by (simp add: mask_def asid_low_bits_of_mask_eq) + subgoal by (clarsimp dest!: asid_map_lift_asid_map_none simp: asid_map_relation_def) + subgoal by (simp add: asid_low_bits_def) + subgoal by (simp add: carch_state_relation_def cmachine_state_relation_def + fpu_null_state_heap_update_tag_disj_simps + global_ioport_bitmap_heap_update_tag_disj_simps + carch_globals_def update_asidpool_map_tos) + apply (rule ccorres_pre_getCurThread) + apply (ctac add: setVMRoot_ccorres) + apply (simp add: cur_tcb'_def[symmetric]) + apply (strengthen invs'_invs_no_cicd') + apply wp + apply (clarsimp simp: rf_sr_def guard_is_UNIV_def + cstate_relation_def Let_def) + apply wp + apply (rule ccorres_return_Skip) + subgoal by (clarsimp simp: guard_is_UNIV_def Collect_const_mem + word_sle_def word_sless_def + Kernel_C.asidLowBits_def + asid_low_bits_def order_le_less_trans [OF word_and_le1]) + apply wp + apply vcg + apply (clarsimp simp: Collect_const_mem if_1_0_0 + word_sless_def word_sle_def + Kernel_C.asidLowBits_def + typ_at_to_obj_at_arches) + apply (rule conjI) + apply (clarsimp simp: mask_def inv_ASIDPool + split: asidpool.split) + apply (frule obj_at_valid_objs', clarsimp+) + apply (clarsimp simp: asid_bits_def typ_at_to_obj_at_arches + obj_at'_weakenE[OF _ TrueI] + fun_upd_def[symmetric] valid_obj'_def + projectKOs + invs_cur') + apply (rule conjI, blast) + subgoal by (fastforce simp: inv_into_def ran_def split: if_split_asm) + by (clarsimp simp: order_le_less_trans [OF word_and_le1] + asid_shiftr_low_bits_less asid_bits_def mask_def + plus_one_helper arg_cong[where f="\x. 2 ^ x", OF meta_eq_to_obj_eq, OF asid_low_bits_def] + split: option.split_asm) + *) + +lemma setObject_ccorres_lemma: + fixes val :: "'a :: pspace_storable" shows + "\ \s. \ \ (Q s) c {s'. (s \ ksPSpace := ksPSpace s (ptr \ injectKO val) \, s') \ rf_sr},{}; + \s s' val (val' :: 'a). \ ko_at' val' ptr s; (s, s') \ rf_sr \ + \ s' \ Q s; + \val :: 'a. updateObject val = updateObject_default val; + \val :: 'a. (1 :: machine_word) < 2 ^ objBits val; + \(val :: 'a) (val' :: 'a). objBits val = objBits val'; + \ \ Q' c UNIV \ + \ ccorres dc xfdc \ Q' hs + (setObject ptr val) c" + apply (rule ccorres_from_vcg_nofail) + apply (rule allI) + apply (case_tac "obj_at' (\x :: 'a. True) ptr \") + apply (rule_tac P'="Q \" in conseqPre, rule conseqPost, assumption) + apply clarsimp + apply (rule bexI [OF _ setObject_eq], simp+) + apply (drule obj_at_ko_at') + apply clarsimp + apply clarsimp + apply (rule conseqPre, erule conseqPost) + apply clarsimp + apply (subgoal_tac "fst (setObject ptr val \) = {}") + apply simp + apply (erule notE, erule_tac s=\ in empty_failD[rotated]) + apply (simp add: setObject_def split_def) + apply (rule ccontr) + apply (clarsimp elim!: nonemptyE) + apply (frule use_valid [OF _ obj_at_setObject3[where P=\]], simp_all)[1] + apply (simp add: typ_at_to_obj_at'[symmetric]) + apply (frule(1) use_valid [OF _ setObject_typ_at']) + apply simp + apply simp + apply clarsimp + done + +lemma findVSpaceForASID_nonzero: + "\\\ findVSpaceForASID asid \\rv s. rv \ 0\,-" + apply (simp add: findVSpaceForASID_def cong: option.case_cong) + apply (wp | wpc | simp only: o_def simp_thms)+ + done + +lemma unat_shiftr_le_bound: + "2 ^ (len_of TYPE('a :: len) - n) - 1 \ bnd \ 0 < n + \ unat ((x :: 'a word) >> n) \ bnd" + apply (erule order_trans[rotated], simp) + apply (rule nat_le_Suc_less_imp) + apply (rule unat_less_helper, simp) + apply (rule shiftr_less_t2n3) + apply simp + apply simp + done + +lemma unmapPageTable_ccorres: + "ccorres dc xfdc (invs' and page_table_at' ptPtr and (\s. asid \ mask asid_bits \ vaddr < pptrBase)) + ({s. asid___unsigned_long_' s = asid} \ {s. vptr_' s = vaddr} \ {s. target_pt_' s = Ptr ptPtr}) + [] (unmapPageTable asid vaddr ptPtr) (Call unmapPageTable_'proc)" + apply (rule ccorres_gen_asm) + apply (cinit lift: asid___unsigned_long_' vptr_' target_pt_') + sorry (* FIXME RISCV + apply (clarsimp simp add: ignoreFailure_liftM) + apply (ctac add: findVSpaceForASID_ccorres,rename_tac vspace find_ret) + apply clarsimp + apply (ctac add: lookupPDSlot_ccorres, rename_tac pdSlot lu_ret) + apply (clarsimp simp add: pde_pde_pt_def liftE_bindE) + apply (rule ccorres_rhs_assoc2) + apply (rule ccorres_rhs_assoc2) + apply (rule ccorres_rhs_assoc2) + apply (rule ccorres_pre_getObject_pde) + apply (simp only: pde_case_isPageTablePDE) + apply (rule_tac xf'=ret__int_' + and R'=UNIV + and val="from_bool (isPageTablePDE pde \ pdeTable pde = addrFromPPtr ptPtr)" + and R="ko_at' pde pdSlot" + in ccorres_symb_exec_r_known_rv_UNIV) + apply vcg + apply clarsimp + apply (erule cmap_relationE1[OF rf_sr_cpde_relation]) + apply (erule ko_at_projectKO_opt) + apply (rename_tac pde_C) + apply (clarsimp simp: typ_heap_simps) + apply (rule conjI, clarsimp simp: pde_pde_pt_def) + apply (drule pde_lift_pde_pt[simplified pde_pde_pt_def, simplified]) + apply (clarsimp simp: from_bool_def cpde_relation_def Let_def isPageTablePDE_def + pde_pde_pt_lift_def case_bool_If + split: pde.split_asm) + apply clarsimp + apply (simp add: from_bool_def split:bool.splits) + apply (rule strenghten_False_imp) + apply (simp add: cpde_relation_def Let_def) + apply (subgoal_tac "pde_get_tag pde_C = 1") + apply (clarsimp dest!: pde_lift_pde_large[simplified pde_pde_large_def, simplified] + simp: isPageTablePDE_def split: pde.splits) + apply (clarsimp simp: pde_get_tag_def word_and_1) + apply ceqv + apply (rule ccorres_Cond_rhs_Seq) + apply (simp add: from_bool_0) + apply ccorres_rewrite + apply (clarsimp simp: throwError_def) + apply (rule ccorres_return_void_C[simplified dc_def]) + apply (simp add: from_bool_0) + apply (rule ccorres_liftE[simplified dc_def]) + apply (ctac add: flushTable_ccorres) + apply (csymbr, rename_tac invalidPDE) + apply (rule ccorres_split_nothrow_novcg_dc) + apply (rule storePDE_Basic_ccorres) + apply (simp add: cpde_relation_def Let_def) + apply (csymbr, rename_tac root) + apply (ctac add: invalidatePageStructureCacheASID_ccorres[simplified dc_def]) + apply wp + apply (clarsimp simp add: guard_is_UNIV_def) + apply wp + apply clarsimp + apply (vcg exspec=flushTable_modifies) + apply (clarsimp simp: guard_is_UNIV_def) + apply (simp,ccorres_rewrite,simp add:throwError_def) + apply (rule ccorres_return_void_C[simplified dc_def]) + apply (clarsimp,wp) + apply (rule_tac Q'="\_ s. invs' s \ page_table_at' ptPtr s" in hoare_post_imp_R) + apply wp + apply clarsimp + apply (vcg exspec=lookupPDSlot_modifies) + apply (simp,ccorres_rewrite,simp add:throwError_def) + apply (rule ccorres_return_void_C[simplified dc_def]) + apply wp + apply vcg + apply (auto simp add: asid_wf_def mask_def) + done + *) + +lemma return_Null_ccorres: + "ccorres ccap_relation ret__struct_cap_C_' + \ UNIV (SKIP # hs) + (return NullCap) (\ret__struct_cap_C :== CALL cap_null_cap_new() + ;; return_C ret__struct_cap_C_'_update ret__struct_cap_C_')" + apply (rule ccorres_from_vcg_throws) + apply (rule allI, rule conseqPre, vcg) + apply (clarsimp simp add: ccap_relation_NullCap_iff return_def) + done + +lemma no_0_page_table_at'[elim!]: + "\ page_table_at' 0 s; no_0_obj' s \ \ P" + apply (clarsimp simp: page_table_at'_def) + apply (drule spec[where x=0], clarsimp simp: bit_simps) + done + +lemma ccte_relation_ccap_relation: + "ccte_relation cte cte' \ ccap_relation (cteCap cte) (cte_C.cap_C cte')" + by (clarsimp simp: ccte_relation_def ccap_relation_def + cte_to_H_def map_option_Some_eq2 + c_valid_cte_def) + +lemma isFinalCapability_ccorres: + "ccorres ((=) \ from_bool) ret__unsigned_long_' + (cte_wp_at' ((=) cte) slot and invs') + (UNIV \ {s. cte_' s = Ptr slot}) [] + (isFinalCapability cte) (Call isFinalCapability_'proc)" + apply (cinit lift: cte_') + apply (rule ccorres_Guard_Seq) + apply (simp add: Let_def del: Collect_const) + apply (rule ccorres_symb_exec_r) + apply (rule_tac xf'="mdb_'" in ccorres_abstract) + apply ceqv + apply (rule_tac P="mdb_node_to_H (mdb_node_lift rv') = cteMDBNode cte" in ccorres_gen_asm2) + apply csymbr + apply (rule_tac r'="(=) \ from_bool" and xf'="prevIsSameObject_'" + in ccorres_split_nothrow_novcg) + apply (rule ccorres_cond2[where R=\]) + apply (clarsimp simp: Collect_const_mem nullPointer_def) + apply (simp add: mdbPrev_to_H[symmetric]) + apply (rule ccorres_from_vcg[where P=\ and P'=UNIV]) + apply (rule allI, rule conseqPre, vcg) + apply (simp add: return_def from_bool_def false_def) + apply (rule ccorres_rhs_assoc)+ + apply (rule ccorres_symb_exec_l[OF _ getCTE_inv getCTE_wp empty_fail_getCTE]) + apply (rule_tac P="cte_wp_at' ((=) cte) slot + and cte_wp_at' ((=) rv) (mdbPrev (cteMDBNode cte)) + and valid_cap' (cteCap rv) + and K (capAligned (cteCap cte) \ capAligned (cteCap rv))" + and P'=UNIV in ccorres_from_vcg) + apply (rule allI, rule conseqPre, vcg) + apply (clarsimp simp: return_def mdbPrev_to_H[symmetric]) + apply (simp add: rf_sr_cte_at_validD) + apply (clarsimp simp: cte_wp_at_ctes_of) + apply (rule cmap_relationE1 [OF cmap_relation_cte], assumption+, + simp?, simp add: typ_heap_simps)+ + apply (drule ccte_relation_ccap_relation)+ + apply (rule exI, rule conjI, assumption)+ + apply (auto)[1] + apply ceqv + apply (clarsimp simp del: Collect_const) + apply (rule ccorres_cond2[where R=\]) + apply (simp add: from_bool_0 Collect_const_mem) + apply (rule ccorres_return_C, simp+)[1] + apply csymbr + apply (rule ccorres_cond2[where R=\]) + apply (simp add: nullPointer_def Collect_const_mem mdbNext_to_H[symmetric]) + apply (rule ccorres_return_C, simp+)[1] + apply (rule ccorres_symb_exec_l[OF _ getCTE_inv getCTE_wp empty_fail_getCTE]) + apply (rule_tac P="cte_wp_at' ((=) cte) slot + and cte_wp_at' ((=) rva) (mdbNext (cteMDBNode cte)) + and K (capAligned (cteCap rva) \ capAligned (cteCap cte)) + and valid_cap' (cteCap cte)" + and P'=UNIV in ccorres_from_vcg_throws) + apply (rule allI, rule conseqPre, vcg) + apply (clarsimp simp: return_def from_bool_eq_if from_bool_0 + mdbNext_to_H[symmetric] rf_sr_cte_at_validD) + apply (clarsimp simp: cte_wp_at_ctes_of split: if_split) + apply (rule cmap_relationE1 [OF cmap_relation_cte], assumption+, + simp?, simp add: typ_heap_simps)+ + apply (drule ccte_relation_ccap_relation)+ + apply (auto simp: false_def true_def from_bool_def split: bool.splits)[1] + apply (wp getCTE_wp') + apply (clarsimp simp add: guard_is_UNIV_def Collect_const_mem false_def + from_bool_0 true_def from_bool_def) + apply vcg + apply (rule conseqPre, vcg) + apply clarsimp + apply (clarsimp simp: Collect_const_mem) + apply (frule(1) rf_sr_cte_at_validD, simp add: typ_heap_simps) + apply (clarsimp simp: cte_wp_at_ctes_of) + apply (erule(1) cmap_relationE1 [OF cmap_relation_cte]) + apply (simp add: typ_heap_simps) + apply (clarsimp simp add: ccte_relation_def map_option_Some_eq2) + by (auto, + auto dest!: ctes_of_valid' [OF _ invs_valid_objs'] + elim!: valid_capAligned) + +lemmas cleanup_info_wf'_simps[simp] = cleanup_info_wf'_def[split_simps capability.split] + +lemma cteDeleteOne_ccorres: + "ccorres dc xfdc + (invs' and cte_wp_at' (\ct. w = -1 \ cteCap ct = NullCap + \ (\cap'. ccap_relation (cteCap ct) cap' \ cap_get_tag cap' = w)) slot) + ({s. gs_get_assn cteDeleteOne_'proc (ghost'state_' (globals s)) = w} + \ {s. slot_' s = Ptr slot}) [] + (cteDeleteOne slot) (Call cteDeleteOne_'proc)" + unfolding cteDeleteOne_def + apply (rule ccorres_symb_exec_l' + [OF _ getCTE_inv getCTE_sp empty_fail_getCTE]) + apply (cinit' lift: slot_' cong: call_ignore_cong) + apply (rule ccorres_move_c_guard_cte) + apply csymbr + apply (rule ccorres_abstract_cleanup) + apply csymbr + apply (rule ccorres_gen_asm2, + erule_tac t="ret__unsigned_longlong = scast cap_null_cap" + and s="cteCap cte = NullCap" + in ssubst) + apply (clarsimp simp only: when_def unless_def dc_def[symmetric]) + apply (rule ccorres_cond2[where R=\]) + apply (clarsimp simp: Collect_const_mem) + apply (rule ccorres_rhs_assoc)+ + apply csymbr + apply csymbr + apply (rule ccorres_Guard_Seq) + apply (rule ccorres_basic_srnoop) + apply (ctac(no_vcg) add: isFinalCapability_ccorres[where slot=slot]) + apply (rule_tac A="invs' and cte_wp_at' ((=) cte) slot" + in ccorres_guard_imp2[where A'=UNIV]) + apply (simp add: split_def dc_def[symmetric] + del: Collect_const) + apply (rule ccorres_move_c_guard_cte) + apply (ctac(no_vcg) add: finaliseCap_True_standin_ccorres) + apply (rule ccorres_assert) + apply (simp add: dc_def[symmetric]) + apply csymbr + apply (ctac add: emptySlot_ccorres) + apply (simp add: pred_conj_def finaliseCapTrue_standin_simple_def) + apply (strengthen invs_mdb_strengthen' invs_urz) + apply (wp typ_at_lifts isFinalCapability_inv + | strengthen invs_valid_objs')+ + apply (clarsimp simp: from_bool_def true_def irq_opt_relation_def + invs_pspace_aligned' cte_wp_at_ctes_of) + apply (erule(1) cmap_relationE1 [OF cmap_relation_cte]) + apply (clarsimp simp: typ_heap_simps ccte_relation_ccap_relation ccap_relation_NullCap_iff) + apply (wp isFinalCapability_inv) + apply simp + apply (simp del: Collect_const add: false_def) + apply (rule ccorres_return_Skip) + apply (clarsimp simp: Collect_const_mem cte_wp_at_ctes_of) + apply (erule(1) cmap_relationE1 [OF cmap_relation_cte]) + apply (clarsimp simp: typ_heap_simps cap_get_tag_isCap + dest!: ccte_relation_ccap_relation) + apply (auto simp: o_def) + done + +lemma getIRQSlot_ccorres_stuff: + "\ (s, s') \ rf_sr \ \ + CTypesDefs.ptr_add intStateIRQNode_Ptr (uint (irq :: 6 word)) + = Ptr (irq_node' s + 2 ^ cte_level_bits * ucast irq)" + apply (clarsimp simp add: rf_sr_def cstate_relation_def Let_def + cinterrupt_relation_def) + apply (simp add: objBits_simps cte_level_bits_def + size_of_def mult.commute mult.left_commute of_int_uint_ucast ) + done + +lemma deletingIRQHandler_ccorres: + "ccorres dc xfdc (invs' and (\s. weak_sch_act_wf (ksSchedulerAction s) s)) + ({s. irq_opt_relation (Some irq) (irq_' s)}) [] + (deletingIRQHandler irq) (Call deletingIRQHandler_'proc)" + apply (cinit lift: irq_' cong: call_ignore_cong) + apply (clarsimp simp: irq_opt_relation_def ptr_add_assertion_def dc_def[symmetric] + cong: call_ignore_cong ) + apply (rule_tac r'="\rv rv'. rv' = Ptr rv" + and xf'="slot_'" in ccorres_split_nothrow) + apply (rule ccorres_Guard_intStateIRQNode_array_Ptr) + apply (rule ccorres_move_array_assertion_irq) + apply (rule ccorres_from_vcg[where P=\ and P'=UNIV]) + + apply (rule allI, rule conseqPre, vcg) + apply (clarsimp simp: getIRQSlot_def liftM_def getInterruptState_def + locateSlot_conv) + apply (simp add: bind_def simpler_gets_def return_def ucast_nat_def uint_up_ucast + is_up getIRQSlot_ccorres_stuff[simplified] + flip: of_int_uint_ucast) + apply ceqv + apply (rule ccorres_symb_exec_l) + apply (rule ccorres_symb_exec_l) + apply (rule ccorres_symb_exec_r) + apply (ctac add: cteDeleteOne_ccorres[where w="scast cap_notification_cap"]) + apply vcg + apply (rule conseqPre, vcg, clarsimp simp: rf_sr_def + gs_set_assn_Delete_cstate_relation[unfolded o_def]) + apply (wp getCTE_wp' | simp add: getSlotCap_def getIRQSlot_def locateSlot_conv + getInterruptState_def)+ + apply vcg + apply (clarsimp simp: cap_get_tag_isCap ghost_assertion_data_get_def + ghost_assertion_data_set_def) + apply (simp add: cap_tag_defs) + apply (clarsimp simp: cte_wp_at_ctes_of Collect_const_mem + irq_opt_relation_def Kernel_C.maxIRQ_def) + apply (drule word_le_nat_alt[THEN iffD1]) + apply (clarsimp simp: uint_0_iff unat_gt_0 uint_up_ucast is_up unat_def[symmetric]) + done + +(* 6 = wordRadix, + 5 = tcb_cnode_radix + 1, + 7 = wordRadix+1*) +lemma Zombie_new_spec: + "\s. \\ ({s} \ {s. type_' s = 64 \ type_' s < 63}) Call Zombie_new_'proc + {s'. cap_zombie_cap_lift (ret__struct_cap_C_' s') = + \ capZombieID_CL = \<^bsup>s\<^esup>ptr && ~~ mask (if \<^bsup>s\<^esup>type = (1 << 6) then 5 else unat (\<^bsup>s\<^esup>type + 1)) + || \<^bsup>s\<^esup>number___unsigned_long && mask (if \<^bsup>s\<^esup>type = (1 << 6) then 5 else unat (\<^bsup>s\<^esup>type + 1)), + capZombieType_CL = \<^bsup>s\<^esup>type && mask 7 \ + \ cap_get_tag (ret__struct_cap_C_' s') = scast cap_zombie_cap}" + apply vcg + apply (clarsimp simp: word_sle_def) + apply (simp add: mask_def word_log_esimps[where 'a=machine_word_len, simplified]) + apply clarsimp thm Zombie_new_body_def + apply (simp add: word_add_less_mono1[where k=1 and j="0x3F", simplified]) + done + +lemmas upcast_ucast_id = Word_Lemmas.ucast_up_inj + +(* FIXME RISCV not true as stands +lemma irq_opt_relation_Some_ucast: + "\ x && mask 6 = x; + ucast x \ (scast Kernel_C.maxIRQ :: 6 word) \ x \ (scast Kernel_C.maxIRQ :: machine_word) \ + \ irq_opt_relation (Some (ucast x)) (ucast ((ucast x):: 6 word))" + unfolding irq_opt_relation_def + apply simp + + using ucast_ucast_mask[where x=x and 'a=6, symmetric] + apply (simp add: irq_opt_relation_def) + apply (rule conjI, clarsimp simp: irqInvalid_def Kernel_C.maxIRQ_def) + apply (simp only: unat_arith_simps ) + apply (clarsimp simp: word_le_nat_alt Kernel_C.maxIRQ_def) + done + +lemma irq_opt_relation_Some_ucast': + "\ x && mask 6 = x; ucast x \ (scast Kernel_C.maxIRQ :: 6 word) \ x \ (scast Kernel_C.maxIRQ :: machine_word) \ + \ irq_opt_relation (Some (ucast x)) (ucast x)" + apply (rule_tac P = "%y. irq_opt_relation (Some (ucast x)) y" in subst[rotated]) + apply (rule irq_opt_relation_Some_ucast[rotated]) + apply (simp add: ucast_ucast_mask)+ + done +*) + +lemma ccap_relation_IRQHandler_mask: + "\ ccap_relation acap ccap; isIRQHandlerCap acap \ + \ capIRQ_CL (cap_irq_handler_cap_lift ccap) && mask 6 + = capIRQ_CL (cap_irq_handler_cap_lift ccap)" + apply (simp only: cap_get_tag_isCap[symmetric]) + apply (drule ccap_relation_c_valid_cap) + apply (simp add: c_valid_cap_def cap_irq_handler_cap_lift cl_valid_cap_def) + done + +lemma option_to_ctcb_ptr_not_0: + "\ tcb_at' p s; option_to_ctcb_ptr v = tcb_ptr_to_ctcb_ptr p\ \ v = Some p" + apply (clarsimp simp: option_to_ctcb_ptr_def tcb_ptr_to_ctcb_ptr_def + split: option.splits) + apply (frule tcb_aligned') + apply (frule_tac y=ctcb_offset and n=tcbBlockSizeBits in aligned_offset_non_zero) + apply (clarsimp simp: ctcb_offset_defs objBits_defs)+ + done + +lemma update_tcb_map_to_tcb: + "map_to_tcbs (ksPSpace s(p \ KOTCB tcb)) + = (map_to_tcbs (ksPSpace s))(p \ tcb)" + by (rule ext, clarsimp simp: projectKOs map_comp_def split: if_split) + +lemma ep_queue_relation_shift2: + "(option_map2 tcbEPNext_C (f (cslift s)) + = option_map2 tcbEPNext_C (cslift s) + \ option_map2 tcbEPPrev_C (f (cslift s)) + = option_map2 tcbEPPrev_C (cslift s)) + \ ep_queue_relation (f (cslift s)) ts qPrev qHead + = ep_queue_relation (cslift s) ts qPrev qHead" + apply clarsimp + apply (induct ts arbitrary: qPrev qHead) + apply simp + apply simp + apply (simp add: option_map2_def fun_eq_iff + map_option_case) + apply (drule_tac x=qHead in spec)+ + apply (clarsimp split: option.split_asm) + done + +lemma sched_queue_relation_shift: + "(option_map2 tcbSchedNext_C (f (cslift s)) + = option_map2 tcbSchedNext_C (cslift s) + \ option_map2 tcbSchedPrev_C (f (cslift s)) + = option_map2 tcbSchedPrev_C (cslift s)) + \ sched_queue_relation (f (cslift s)) ts qPrev qHead + = sched_queue_relation (cslift s) ts qPrev qHead" + apply clarsimp + apply (induct ts arbitrary: qPrev qHead) + apply simp + apply simp + apply (simp add: option_map2_def fun_eq_iff + map_option_case) + apply (drule_tac x=qHead in spec)+ + apply (clarsimp split: option.split_asm) + done + +lemma cendpoint_relation_udpate_arch: + "\ cslift x p = Some tcb ; cendpoint_relation (cslift x) v v' \ + \ cendpoint_relation (cslift x(p \ tcbArch_C_update f tcb)) v v'" + apply (clarsimp simp: cendpoint_relation_def Let_def tcb_queue_relation'_def + split: endpoint.splits) + apply (subst ep_queue_relation_shift2; simp add: fun_eq_iff) + apply (safe ; case_tac "xa = p" ; clarsimp simp: option_map2_def map_option_case) + apply (subst ep_queue_relation_shift2; simp add: fun_eq_iff) + apply (safe ; case_tac "xa = p" ; clarsimp simp: option_map2_def map_option_case) + done + +lemma cnotification_relation_udpate_arch: + "\ cslift x p = Some tcb ; cnotification_relation (cslift x) v v' \ + \ cnotification_relation (cslift x(p \ tcbArch_C_update f tcb)) v v'" + apply (clarsimp simp: cnotification_relation_def Let_def tcb_queue_relation'_def + split: notification.splits ntfn.splits) + apply (subst ep_queue_relation_shift2; simp add: fun_eq_iff) + apply (safe ; case_tac "xa = p" ; clarsimp simp: option_map2_def map_option_case) + done + +lemma sanitiseSetRegister_ccorres: + "\ val = val'; reg' = register_from_H reg\ \ + ccorres dc xfdc (tcb_at' tptr) + UNIV + hs + (asUser tptr (setRegister reg (local.sanitiseRegister False reg val))) + (\unsigned_long_eret_2 :== CALL sanitiseRegister(reg',val',0);; + CALL setRegister(tcb_ptr_to_ctcb_ptr tptr,reg',\unsigned_long_eret_2))" + apply (rule ccorres_guard_imp2) + apply (rule ccorres_symb_exec_r) + apply (ctac add: setRegister_ccorres) + apply (vcg) + apply (rule conseqPre, vcg) + apply (fastforce simp: sanitiseRegister_def split: register.splits) + by (auto simp: sanitiseRegister_def from_bool_def simp del: Collect_const split: register.splits bool.splits) + +lemma case_option_both[simp]: + "(case f of None \ P | _ \ P) = P" + by (auto split: option.splits) + +lemma if_case_opt_same_branches: + "cond \ Option.is_none opt \ + (if cond then + case opt of + None \ f + | Some x \ g x + else f) = f" + by (cases cond; cases opt; clarsimp) + +method return_NullCap_pair_ccorres = + solves \((rule ccorres_rhs_assoc2)+), (rule ccorres_from_vcg_throws), + (rule allI, rule conseqPre, vcg), (clarsimp simp: return_def ccap_relation_NullCap_iff)\ + +lemma ccap_relation_capFMappedASID_CL_0: + "ccap_relation (ArchObjectCap (FrameCap x0 x1 x2 x3 None)) cap \ + capFMappedASID_CL (cap_frame_cap_lift cap) = 0" + apply (clarsimp simp: ccap_relation_def cap_frame_cap_lift_def) + apply (case_tac "cap_lift cap") + apply (fastforce simp: cap_to_H_def Let_def split: cap_CL.splits if_split_asm)+ + done + +(* FIXME RISCV: left this in as a reference, there are no mode operations on RISCV +lemma Mode_finaliseCap_ccorres_page_cap: + "cp = FrameCap x0 x1 x3 x4 x5 \ + ccorres + (\rv rv'. + ccap_relation (fst rv) (remainder_C rv') \ + ccap_relation (snd rv) (finaliseCap_ret_C.cleanupInfo_C rv')) + ret__struct_finaliseCap_ret_C_' + (invs' and + valid_cap' (ArchObjectCap cp) and + (\s. 2 ^ pageBitsForSize x3 \ gsMaxObjectSize s)) + (UNIV \ \ccap_relation (ArchObjectCap cp) \cap\) + hs + (case x5 of + None \ return (NullCap, NullCap) + | Some (asid, ptr) \ do _ <- unmapPage x3 asid ptr x0; + return (NullCap, NullCap) + od) + (Call Mode_finaliseCap_'proc)" + supply Collect_const[simp del] + apply (cinit' lift: cap_' simp: false_def) + apply csymbr + apply (clarsimp simp: cap_get_tag_isCap_unfolded_H_cap cap_tag_defs) + apply ccorres_rewrite + apply (rule ccorres_rhs_assoc) + apply csymbr + apply wpc + apply (clarsimp simp: ccap_relation_capFMappedASID_CL_0) + apply ccorres_rewrite + apply (rule ccorres_inst[where P=\ and P'=UNIV]) + apply return_NullCap_pair_ccorres + apply clarsimp + apply (rule ccorres_cond_true_seq) + apply (rule ccorres_rhs_assoc) + apply csymbr + apply (rule ccorres_cond_true_seq) + apply (rule ccorres_rhs_assoc)+ + apply csymbr + apply csymbr + apply csymbr + apply csymbr + apply wpfix + apply (ctac add: unmapPage_ccorres) + apply (rule ccorres_inst[where P=\ and P'=UNIV]) + apply return_NullCap_pair_ccorres + apply wp + apply (vcg exspec=unmapPage_modifies) + by (clarsimp elim!: ccap_relationE + simp: cap_to_H_def cap_frame_cap_lift_def cap_get_tag_isCap_unfolded_H_cap + c_valid_cap_def cl_valid_cap_def valid_cap_simps' + maptype_to_H_def vm_page_map_type_defs Let_def + split: cap_CL.splits if_split_asm + dest!: x_less_2_0_1) +*) + +lemma Arch_finaliseCap_ccorres: + notes dc_simp[simp del] Collect_const[simp del] + shows + "ccorres (\rv rv'. ccap_relation (fst rv) (remainder_C rv') \ + ccap_relation (snd rv) (finaliseCap_ret_C.cleanupInfo_C rv')) + ret__struct_finaliseCap_ret_C_' + (invs' and valid_cap' (ArchObjectCap cp) + and (\s. 2 ^ acapBits cp \ gsMaxObjectSize s)) + (UNIV \ {s. ccap_relation (ArchObjectCap cp) (cap_' s)} + \ {s. final_' s = from_bool is_final}) [] + (Arch.finaliseCap cp is_final) (Call Arch_finaliseCap_'proc)" + (is "ccorres _ _ ?abstract_pre ?c_pre _ _ _") + apply (cinit lift: cap_' final_' cong: call_ignore_cong) + apply csymbr + apply (simp add: RISCV64_H.finaliseCap_def cap_get_tag_isCap_ArchObject) + apply (rule ccorres_cases[where P=is_final]; clarsimp cong: arch_capability.case_cong) + prefer 2 + apply (subgoal_tac "isFrameCap cp \ \ isPageTableCap cp \ \ isASIDPoolCap cp \ \ isASIDControlCap cp") + apply (rule ccorres_cases[where P="isFrameCap cp"]; clarsimp) + prefer 2 + apply (rule ccorres_inst[where P="?abstract_pre" and P'=UNIV]) + apply (cases cp; clarsimp simp: isCap_simps; ccorres_rewrite) + apply return_NullCap_pair_ccorres (* ASIDPoolCap *) + apply return_NullCap_pair_ccorres (* ASIDControlCap *) + \ \PageTableCap\ + apply (subst ccorres_cond_seq2_seq[symmetric]) + apply (rule ccorres_guard_imp) + apply (rule ccorres_rhs_assoc) + apply csymbr + apply clarsimp + apply ccorres_rewrite + apply (rule ccorres_inst[where P=\ and P'=UNIV]) + apply (return_NullCap_pair_ccorres, simp+) + \ \FrameCap\ + apply (clarsimp simp: isCap_simps) + apply (rule ccorres_guard_imp[where A="?abstract_pre" and A'=UNIV]) + apply ccorres_rewrite + apply (rule ccorres_add_return2) + sorry (* FIXME RISCV + apply (ctac (no_vcg) add: Mode_finaliseCap_ccorres_page_cap) + apply (rule ccorres_from_vcg_throws[where P=\ and P'=UNIV]) + apply (rule allI, rule conseqPre, vcg) + apply (fastforce simp: return_def) + apply wp + apply fastforce + apply fastforce + apply (fastforce simp: isCap_simps) + apply ccorres_rewrite + apply (rule ccorres_Cond_rhs_Seq) + \ \final \ PageDirectoryCap\ + apply (clarsimp simp: isCap_simps) + apply (rule ccorres_rhs_assoc)+ + apply csymbr + apply ccorres_rewrite + apply (rule ccorres_rhs_assoc)+ + apply csymbr + apply csymbr + apply clarsimp + apply (rule ccorres_Cond_rhs_Seq) + apply (subgoal_tac "capPDMappedAddress cp \ None") + prefer 2 + apply (clarsimp simp add: isCap_simps) + apply (frule cap_get_tag_isCap_unfolded_H_cap) + apply (frule cap_lift_page_directory_cap) + apply (clarsimp simp: ccap_relation_def cap_to_H_def capAligned_def + to_bool_def cap_page_directory_cap_lift_def + asid_bits_def + split: if_split_asm) + apply clarsimp + apply (rule ccorres_rhs_assoc)+ + apply csymbr + apply csymbr + apply csymbr + apply (frule cap_get_tag_isCap_unfolded_H_cap) + apply (subst (asm) ccap_relation_def) + apply (clarsimp simp: cap_page_directory_cap_lift cap_to_H_def split: if_splits) + apply (ctac (no_vcg) add: unmapPageDirectory_ccorres) + apply (rule ccorres_inst[where P=\ and P'=UNIV], return_NullCap_pair_ccorres) + apply (rule wp_post_taut) + apply (subgoal_tac "capPDMappedAddress cp = None") + prefer 2 + apply (clarsimp simp add: isCap_simps) + apply (frule cap_get_tag_isCap_unfolded_H_cap) + apply (frule cap_lift_page_directory_cap) + apply (clarsimp simp: ccap_relation_def cap_to_H_def capAligned_def + to_bool_def cap_page_directory_cap_lift_def + asid_bits_def + split: if_split_asm) + apply simp + apply (rule ccorres_inst[where P=\ and P'=UNIV], return_NullCap_pair_ccorres) + \ \final \ PageTableCap\ + apply (rule ccorres_Cond_rhs_Seq) + apply (clarsimp simp: isCap_simps) + apply (rule ccorres_rhs_assoc)+ + apply csymbr + apply ccorres_rewrite + apply (rule ccorres_rhs_assoc)+ + apply csymbr + apply csymbr + apply clarsimp + apply (rule ccorres_Cond_rhs_Seq) + apply (subgoal_tac "capPTMappedAddress cp \ None") + prefer 2 + apply (clarsimp simp add: isCap_simps) + apply (frule cap_get_tag_isCap_unfolded_H_cap) + apply (frule cap_lift_page_table_cap) + apply (clarsimp simp: ccap_relation_def cap_to_H_def capAligned_def + to_bool_def cap_page_table_cap_lift_def + asid_bits_def + split: if_split_asm) + apply clarsimp + apply (rule ccorres_rhs_assoc)+ + apply csymbr + apply csymbr + apply csymbr + apply (simp add: split_def) + apply (frule cap_get_tag_isCap_unfolded_H_cap) + apply (subst (asm) ccap_relation_def) + apply (clarsimp simp: cap_page_table_cap_lift cap_to_H_def split: if_splits) + apply (ctac (no_vcg) add: unmapPageTable_ccorres) + apply (rule ccorres_inst[where P=\ and P'=UNIV], return_NullCap_pair_ccorres) + apply (rule wp_post_taut) + apply clarsimp + apply (subgoal_tac "capPTMappedAddress cp = None") + prefer 2 + apply (clarsimp simp add: isCap_simps) + apply (frule cap_get_tag_isCap_unfolded_H_cap) + apply (frule cap_lift_page_table_cap) + apply (clarsimp simp: ccap_relation_def cap_to_H_def capAligned_def + to_bool_def cap_page_table_cap_lift_def + asid_bits_def + split: if_split_asm) + apply simp + apply (rule ccorres_inst[where P=\ and P'=UNIV], return_NullCap_pair_ccorres) + \ \final \ ASIDPoolCap\ + apply (rule ccorres_Cond_rhs_Seq) + apply (clarsimp simp: isCap_simps) + apply (rule ccorres_rhs_assoc)+ + apply csymbr + apply csymbr + apply (frule cap_get_tag_isCap_unfolded_H_cap) + apply (subst (asm) ccap_relation_def) + apply (clarsimp simp: cap_asid_pool_cap_lift cap_to_H_def split: if_splits) + apply (ctac (no_vcg) add: deleteASIDPool_ccorres) + apply (rule ccorres_inst[where P=\ and P'=UNIV], return_NullCap_pair_ccorres) + apply (rule wp_post_taut) + \ \final \ (ASIDControlCap \ IOPortControlCap\ + apply (rule ccorres_Cond_rhs_Seq) + apply (clarsimp simp: isCap_simps) + apply (erule disjE; ccorres_rewrite; clarsimp; (rule ccorres_inst[where P=\ and P'=UNIV], return_NullCap_pair_ccorres)) + \ \final \ IOPortCap\ + apply (rule ccorres_Cond_rhs_Seq) + apply (clarsimp simp: isCap_simps) + apply ccorres_rewrite + apply (rule ccorres_from_vcg_throws[where P=\ and P'=UNIV]) + apply (rule allI, rule conseqPre, vcg) + apply (clarsimp simp: return_def ccap_relation_NullCap_iff) + \ \Mode_finaliseCap\ + apply ccorres_rewrite + (* Winnow out the irrelevant cases *) + apply (wpc; (rule ccorres_inst[where P=\ and P'=UNIV], fastforce simp: isCap_simps)?) + \ \PageCap\ + apply clarsimp + apply (rule ccorres_add_return2) + apply (ctac (no_vcg) add: Mode_finaliseCap_ccorres_page_cap) + apply (rule ccorres_from_vcg_throws[where P=\ and P'=UNIV]) + apply (rule allI, rule conseqPre, vcg) + apply (fastforce simp: return_def) + apply wp + \ \PDPointerTableCap\ + apply (rule ccorres_add_return2) + apply (ctac (no_vcg) add: Mode_finaliseCap_ccorres_pdpt[where is_final=True, simplified if_True]) + apply (rule ccorres_from_vcg_throws[where P=\ and P'=UNIV]) + apply (rule allI, rule conseqPre, vcg) + apply (fastforce simp: return_def) + apply wp + \ \PML4Cap\ + apply (rule ccorres_add_return2) + apply (ctac (no_vcg) add: Mode_finaliseCap_ccorres_pml4[where is_final=True, simplified if_True]) + apply (rule ccorres_from_vcg_throws[where P=\ and P'=UNIV]) + apply (rule allI, rule conseqPre, vcg) + apply (fastforce simp: return_def) + apply wp + by (auto elim: ccap_relationE + simp: cap_to_H_def cap_get_tag_isCap_unfolded_H_cap + cap_page_table_cap_lift_def cap_asid_pool_cap_lift_def + cap_page_directory_cap_lift_def cap_frame_cap_lift_def + c_valid_cap_def cl_valid_cap_def valid_cap_simps' + asid_wf_def mask_def to_bool_def asid_bits_def word_le_make_less + Let_def isCap_simps cap_get_tag_isCap_ArchObject + split: cap_CL.splits if_split_asm) + *) + +lemma prepareThreadDelete_ccorres: + "ccorres dc xfdc + (invs' and tcb_at' thread) + (UNIV \ {s. thread_' s = tcb_ptr_to_ctcb_ptr thread}) hs + (prepareThreadDelete thread) (Call Arch_prepareThreadDelete_'proc)" + supply dc_simp[simp del] + apply (cinit lift: thread_', rename_tac cthread) + apply (rule ccorres_return_Skip) + apply fastforce + done + +lemma finaliseCap_ccorres: + "\final. + ccorres (\rv rv'. ccap_relation (fst rv) (finaliseCap_ret_C.remainder_C rv') + \ ccap_relation (snd rv) (finaliseCap_ret_C.cleanupInfo_C rv')) + ret__struct_finaliseCap_ret_C_' + (invs' and sch_act_simple and valid_cap' cap and (\s. ksIdleThread s \ capRange cap) + and (\s. 2 ^ capBits cap \ gsMaxObjectSize s)) + (UNIV \ {s. ccap_relation cap (cap_' s)} \ {s. final_' s = from_bool final} + \ {s. exposed_' s = from_bool flag \ \dave has name wrong\}) [] + (finaliseCap cap final flag) (Call finaliseCap_'proc)" + apply (rule_tac F="capAligned cap" in Corres_UL_C.ccorres_req) + apply (clarsimp simp: valid_capAligned) + apply (case_tac "P :: bool" for P) + apply (rule ccorres_guard_imp2, erule finaliseCap_True_cases_ccorres) + apply simp + apply (subgoal_tac "\acap. (0 <=s (-1 :: word8)) \ acap = capCap cap") + prefer 2 apply simp + apply (erule exE) + apply (cinit lift: cap_' final_' exposed_' cong: call_ignore_cong) + apply csymbr + apply (simp del: Collect_const) + apply (rule ccorres_Cond_rhs_Seq) + apply (clarsimp simp: cap_get_tag_isCap isCap_simps from_bool_neq_0 + cong: if_cong simp del: Collect_const) + apply (clarsimp simp: word_sle_def) + apply (rule ccorres_if_lhs) + apply (rule ccorres_fail) + apply (simp add: liftM_def del: Collect_const) + apply (rule ccorres_rhs_assoc)+ + apply (rule ccorres_add_return2) + apply (ccorres_rewrite) + apply (ctac add: Arch_finaliseCap_ccorres) + apply (rule ccorres_from_vcg_throws[where P=\ and P'=UNIV]) + apply (rule allI, rule conseqPre, vcg) + apply (clarsimp simp: return_def Collect_const_mem) + apply wp + apply (vcg exspec=Arch_finaliseCap_modifies) + apply (simp add: cap_get_tag_isCap Collect_False + del: Collect_const) + apply csymbr + apply (simp add: cap_get_tag_isCap Collect_False Collect_True + del: Collect_const) + apply (rule ccorres_if_lhs) + apply (simp, rule ccorres_fail) + apply (simp add: from_bool_0 Collect_True Collect_False false_def + del: Collect_const) + apply csymbr + apply (simp add: cap_get_tag_isCap Collect_False Collect_True + del: Collect_const) + apply (rule ccorres_if_lhs) + apply (simp add: Let_def) + apply (rule ccorres_from_vcg_throws[where P=\ and P'=UNIV]) + apply (rule allI, rule conseqPre, vcg) + apply (clarsimp simp: cap_get_tag_isCap word_sle_def + return_def word_mod_less_divisor + less_imp_neq [OF word_mod_less_divisor]) + apply (frule cap_get_tag_to_H, erule(1) cap_get_tag_isCap [THEN iffD2]) + apply (clarsimp simp: isCap_simps capAligned_def + objBits_simps word_bits_conv + signed_shift_guard_simpler_64) + apply (rule conjI) + apply (simp add: word_less_nat_alt) + apply (rule conjI) + apply (auto simp: word_less_nat_alt word_le_not_less[symmetric] bit_simps objBits_defs)[1] + apply (simp add: ccap_relation_def cap_zombie_cap_lift) + apply (simp add: cap_to_H_def isZombieTCB_C_def ZombieTCB_C_def) + apply (simp add: less_mask_eq word_less_nat_alt less_imp_neq) + apply (simp add: mod_mask_drop[where n=6] mask_def[where n=6] + less_imp_neq [OF word_mod_less_divisor] + less_imp_neq Let_def objBits_simps') + apply (thin_tac "a = b" for a b)+ + apply (subgoal_tac "P" for P) + apply (subst add.commute, subst unatSuc, assumption)+ + apply clarsimp + apply (rule conjI) + apply (rule word_eqI) + apply (simp add: word_size word_ops_nth_size nth_w2p + less_Suc_eq_le is_aligned_nth) + apply (safe, simp_all)[1] + apply (simp add: shiftL_nat ccap_relation_NullCap_iff[symmetric, simplified ccap_relation_def]) + apply (rule trans, rule unat_power_lower64[symmetric]) + apply (simp add: word_bits_conv) + apply (rule unat_cong, rule word_eqI) + apply (simp add: word_size word_ops_nth_size nth_w2p + is_aligned_nth less_Suc_eq_le) + apply (safe, simp_all)[1] + apply (subst add.commute, subst eq_diff_eq[symmetric]) + apply (clarsimp simp: minus_one_norm) + apply (rule ccorres_if_lhs) + apply (simp add: Let_def getThreadCSpaceRoot_def locateSlot_conv + Collect_True Collect_False + del: Collect_const) + apply (rule ccorres_rhs_assoc)+ + apply csymbr + apply csymbr + apply csymbr + apply csymbr + apply (rule ccorres_Guard_Seq)+ + apply csymbr + apply (ctac(no_vcg) add: unbindNotification_ccorres) + apply (ctac(no_vcg) add: suspend_ccorres[OF cteDeleteOne_ccorres]) + apply (ctac(no_vcg) add: prepareThreadDelete_ccorres) + apply (rule ccorres_from_vcg_throws[where P=\ and P'=UNIV]) + apply (rule allI, rule conseqPre, vcg) + apply (clarsimp simp: word_sle_def return_def) + apply (subgoal_tac "cap_get_tag capa = scast cap_thread_cap") + apply (drule(1) cap_get_tag_to_H) + apply (clarsimp simp: isCap_simps capAligned_def ccap_relation_NullCap_iff) + apply (simp add: ccap_relation_def cap_zombie_cap_lift) + apply (simp add: cap_to_H_def isZombieTCB_C_def ZombieTCB_C_def + mask_def) + apply (simp add: cte_level_bits_def tcbCTableSlot_def + Kernel_C.tcbCTable_def tcbCNodeEntries_def + word_bool_alg.conj_disj_distrib2 + word_bw_assocs) + apply (simp add: objBits_simps ctcb_ptr_to_tcb_ptr_def) + apply (frule is_aligned_add_helper[where p="tcbptr - ctcb_offset" and d=ctcb_offset for tcbptr]) + apply (simp add: ctcb_offset_defs objBits_defs) + apply (simp add: mask_def objBits_defs) + apply (simp add: cap_get_tag_isCap) + apply wp+ + apply (rule ccorres_if_lhs) + apply (simp add: Let_def) + apply (rule ccorres_from_vcg_throws[where P=\ and P'=UNIV]) + apply (rule allI, rule conseqPre, vcg) + apply (clarsimp simp: return_def ccap_relation_NullCap_iff) + apply (simp add: isArchCap_T_isArchObjectCap[symmetric] + del: Collect_const) + apply (rule ccorres_if_lhs) + apply (simp add: Collect_False Collect_True Let_def true_def + del: Collect_const) + apply (rule_tac P="(capIRQ cap) \ RISCV64.maxIRQ" in ccorres_gen_asm) + apply (rule ccorres_rhs_assoc)+ + apply csymbr + apply csymbr + apply (rule_tac xf'=irq_' in ccorres_abstract,ceqv) + apply (rule_tac P="rv' = ucast (capIRQ cap)" in ccorres_gen_asm2) + apply (ctac(no_vcg) add: deletingIRQHandler_ccorres) + apply (rule ccorres_from_vcg_throws[where P=\ ]) + apply (rule allI, rule conseqPre, vcg) + apply (clarsimp simp: return_def) + apply (frule cap_get_tag_to_H, erule(1) cap_get_tag_isCap [THEN iffD2]) + apply (simp add: ccap_relation_NullCap_iff split: if_split) + apply wp + apply (rule ccorres_if_lhs) + apply simp + apply (rule ccorres_fail) + apply (rule ccorres_add_return, rule ccorres_split_nothrow_novcg[where r'=dc and xf'=xfdc]) + apply (rule ccorres_Cond_rhs) + apply (simp add: ccorres_cond_iffs dc_def[symmetric]) + apply (rule ccorres_return_Skip) + apply (rule ccorres_Cond_rhs) + apply (simp add: ccorres_cond_iffs dc_def[symmetric]) + apply (rule ccorres_return_Skip) + apply (rule ccorres_Cond_rhs) + apply (rule ccorres_inst[where P=\ and P'=UNIV]) + apply simp + apply (rule ccorres_Cond_rhs) + apply (simp add: ccorres_cond_iffs dc_def[symmetric]) + apply (rule ccorres_return_Skip) + apply (simp add: ccorres_cond_iffs dc_def[symmetric]) + apply (rule ccorres_return_Skip) + apply (rule ceqv_refl) + apply (rule ccorres_from_vcg_throws[where P=\ and P'=UNIV]) + apply (rule allI, rule conseqPre, vcg) + apply (clarsimp simp: return_def ccap_relation_NullCap_iff + irq_opt_relation_def) + apply wp + apply (simp add: guard_is_UNIV_def) + apply (clarsimp simp: cap_get_tag_isCap word_sle_def Collect_const_mem + false_def from_bool_def) + apply (intro impI conjI) + apply (clarsimp split: bool.splits) + apply (clarsimp split: bool.splits) + apply (clarsimp simp: valid_cap'_def isCap_simps) + apply (clarsimp simp: isCap_simps capRange_def capAligned_def) + apply (clarsimp simp: isCap_simps valid_cap'_def) + apply (clarsimp simp: isCap_simps capRange_def capAligned_def) + apply (clarsimp simp: isCap_simps valid_cap'_def ) + apply clarsimp + apply (clarsimp simp: isCap_simps valid_cap'_def ) + apply (clarsimp simp: tcb_ptr_to_ctcb_ptr_def ccap_relation_def isCap_simps + c_valid_cap_def cap_thread_cap_lift_def cap_to_H_def + ctcb_ptr_to_tcb_ptr_def Let_def + split: option.splits cap_CL.splits if_splits) + apply clarsimp + apply (frule cap_get_tag_to_H, erule(1) cap_get_tag_isCap [THEN iffD2]) + apply (clarsimp simp: isCap_simps from_bool_def false_def) + apply (clarsimp simp: tcb_cnode_index_defs ptr_add_assertion_def) + apply clarsimp + apply (frule cap_get_tag_to_H, erule(1) cap_get_tag_isCap [THEN iffD2]) + apply (frule(1) ccap_relation_IRQHandler_mask) + apply (clarsimp simp: isCap_simps irqInvalid_def + valid_cap'_def RISCV64.maxIRQ_def + Kernel_C.maxIRQ_def) + subgoal sorry + (* FIXME RISCV: we cannot show here that the IRQ is not equal to irqInvalid, which is what + would be required given the definition of irq_opt_relation; on X64 being \ maxIRQ + automatically disqualified irqInvalid as it was greater than maxIRQ; on RISCV irqInvalid + is 0. However, valid_cap' does not prevent the irq from being irqInvalid in an irq handler + cap. + apply (rule irq_opt_relation_Some_ucast'[simplified Kernel_C.maxIRQ_def, simplified]) + apply fastforce + *) + apply simp + apply (clarsimp simp: isCap_simps irqInvalid_def + valid_cap'_def RISCV64.maxIRQ_def + Kernel_C.maxIRQ_def) + apply fastforce + apply clarsimp + apply (frule cap_get_tag_to_H, erule(1) cap_get_tag_isCap [THEN iffD2]) + apply (frule(1) ccap_relation_IRQHandler_mask) + apply (clarsimp simp add:mask_eq_ucast_eq) + done + end + +end