diff --git a/proof/crefine/RISCV64/Finalise_C.thy b/proof/crefine/RISCV64/Finalise_C.thy index 5db0345fcc..2c25fdab35 100644 --- a/proof/crefine/RISCV64/Finalise_C.thy +++ b/proof/crefine/RISCV64/Finalise_C.thy @@ -35,102 +35,226 @@ declare if_split [split del] definition "option_map2 f m = option_map f \ m" -lemma head_end_ksReadyQueues_': - "\ (s, s') \ rf_sr; ksReadyQueues_asrt s; pspace_aligned' s; pspace_distinct' s; - d \ maxDomain; p \ maxPriority \ - \ head_C (index (ksReadyQueues_' (globals s')) (cready_queues_index_to_C d p)) = NULL - \ end_C (index (ksReadyQueues_' (globals s')) (cready_queues_index_to_C d p)) = NULL" - apply (frule (2) rf_sr_ctcb_queue_relation[where d=d and p=p]) - apply (clarsimp simp: ready_queue_relation_def ksReadyQueues_asrt_def) - apply (drule_tac x=d in spec) - apply (drule_tac x=p in spec) +lemma thread_state_ptr_set_tcbQueued_tcb_fields: + "\s. \ \\<^bsub>/UNIV\<^esub> \s. s \\<^sub>c (cparent \<^bsup>s\<^esup>thread_state_ptr [''tcbState_C''] :: tcb_C ptr)\ + Call thread_state_ptr_set_tcbQueued_'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 \ \for speed\ + apply (clarsimp simp: typ_heap_simps h_t_valid_clift_Some_iff) + apply (frule h_t_valid_clift) + apply (clarsimp simp: packed_heap_update_collapse_hrs) + apply (intro conjI; + fwd_all_new \subst parent_update_child\ + \fastforce intro!: h_t_valid_c_guard + simp: option_map2_def fun_eq_iff typ_heap_simps + split: if_splits\) + done + +lemma thread_state_ptr_set_tsType_tcb_fields: + "\s. \ \\<^bsub>/UNIV\<^esub> \s. s \\<^sub>c (cparent \<^bsup>s\<^esup>thread_state_ptr [''tcbState_C''] :: tcb_C ptr)\ + Call thread_state_ptr_set_tsType_'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 \ \for speed\ + apply (clarsimp simp: typ_heap_simps h_t_valid_clift_Some_iff) + apply (frule h_t_valid_clift) + apply (clarsimp simp: packed_heap_update_collapse_hrs) + apply (intro conjI; + fwd_all_new \subst parent_update_child\ + \fastforce intro!: h_t_valid_c_guard + simp: option_map2_def fun_eq_iff typ_heap_simps + split: if_splits\) + done + +lemma tcb_queue_prepend_tcb_fields: + "\s. \ \\<^bsub>/UNIV\<^esub> {s} + Call tcb_queue_prepend_'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 (rule allI, rule conseqPre) + apply vcg + apply (clarsimp simp: option_map2_def fun_eq_iff typ_heap_simps h_t_valid_clift_Some_iff + split: if_splits) + done + +lemma addToBitmap_tcb_fields: + "\s. \ \\<^bsub>/UNIV\<^esub> {s} + Call addToBitmap_'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 (rule allI, rule conseqPre) + apply vcg + apply clarsimp + done + +lemma ready_queues_index_tcb_fields: + "\s. \ \\<^bsub>/UNIV\<^esub> {s} + Call ready_queues_index_'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) + apply vcg apply clarsimp - apply (frule tcbQueueHead_iff_tcbQueueEnd) - apply (clarsimp simp: ctcb_queue_relation_def option_to_ctcb_ptr_def split: option.splits) - apply (frule (3) obj_at'_tcbQueueHead_ksReadyQueues) - apply (frule (3) obj_at'_tcbQueueEnd_ksReadyQueues) - apply (rename_tac head "end") - apply (prop_tac "tcb_at' head s") - apply (fastforce simp: tcbQueueEmpty_def) - apply (prop_tac "tcb_at' end s") - apply (fastforce simp: tcbQueueEmpty_def) - apply (fastforce dest: tcb_at_not_NULL) - done - -lemma tcbSchedEnqueue_cslift_spec: - "\s. \\\<^bsub>/UNIV\<^esub> \s. \d v. option_map2 tcbPriority_C (cslift s) \tcb = Some v - \ unat v \ numPriorities - \ option_map2 tcbDomain_C (cslift s) \tcb = Some d - \ unat d < Kernel_Config.numDomains - \ (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) - \ (head_C (index \ksReadyQueues (unat (d * 0x100 + v))) \ NULL - \ end_C (index \ksReadyQueues (unat (d * 0x100 + v))) \ NULL)\ + done + +lemma tcbSchedEnqueue_tcb_fields: + "\s. \ \\<^bsub>/UNIV\<^esub> \s. True\ 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 le_maxDomain_eq_less_numDomains) - apply unat_arith + apply (rule allI, rule conseqPre) + apply (vcg exspec=thread_state_ptr_set_tcbQueued_tcb_fields + exspec=tcb_queue_prepend_tcb_fields + exspec=addToBitmap_tcb_fields + exspec=ready_queues_index_tcb_fields) + apply simp + done + +lemma isSchedulable_tcb_fields: + "\s. \ \\<^bsub>/UNIV\<^esub> {s} + Call isSchedulable_'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 (rule allI, rule conseqPre) + apply (vcg exspec=isRunnable_modifies) apply clarsimp - apply (rule conjI) - apply (clarsimp simp: typ_heap_simps cong: if_cong) - apply (simp split: if_split) - by (auto simp: typ_heap_simps' if_Some_helper numPriorities_def - cong: if_cong split: if_splits) - -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 - \ unat v \ numPriorities - \ option_map2 tcbDomain_C (cslift s) (tcb_Ptr x) = Some d - \ unat d < Kernel_Config.numDomains - \ (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)}" + done + +lemma rescheduleRequired_tcb_fields: + "\s. \ \\<^bsub>/UNIV\<^esub> {s} + Call rescheduleRequired_'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 (rule allI, rule conseqPre) + apply (vcg exspec=tcbSchedEnqueue_tcb_fields exspec=isSchedulable_tcb_fields) + apply clarsimp + done + +lemma possibleSwitchTo_tcb_fields: + "\s. \ \\<^bsub>/UNIV\<^esub> {s} + Call possibleSwitchTo_'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 (rule allI, rule conseqPre) + apply (vcg exspec=rescheduleRequired_tcb_fields exspec=tcbSchedEnqueue_tcb_fields) + apply clarsimp + done + +lemma setThreadState_tcb_fields: + "\s. \ \\<^bsub>/UNIV\<^esub> {s} + 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)}" + apply (rule allI, rule conseqPre) + apply (vcg exspec=rescheduleRequired_tcb_fields + exspec=thread_state_ptr_set_tsType_tcb_fields + exspec=isSchedulable_tcb_fields) + apply clarsimp + done + +lemma refill_head_overlapping_tcb_fields: + "\s. \ \\<^bsub>/UNIV\<^esub> {s} + Call refill_head_overlapping_'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 (rule allI, rule conseqPre) + apply vcg + apply clarsimp + done + +lemma refill_pop_head_tcb_fields: + "\s. \ \\<^bsub>/UNIV\<^esub> {s} + Call refill_pop_head_'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 (rule allI, rule conseqPre) + apply (vcg exspec=refill_head_modifies exspec=refill_next_modifies exspec=refill_size_modifies) + apply (clarsimp simp: typ_heap_simps) + done + +lemma merge_overlapping_head_refill_tcb_fields: + "\s. \ \\<^bsub>/UNIV\<^esub> {s} + Call merge_overlapping_head_refill_'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 (rule allI, rule conseqPre) + apply (vcg exspec=refill_pop_head_tcb_fields exspec=refill_head_modifies + exspec=refill_index_modifies) + apply (clarsimp simp: typ_heap_simps) + done + +lemma refill_unblock_check_tcb_fields: + "\s. \ \\<^bsub>/UNIV\<^esub> {s} + Call refill_unblock_check_'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)}" + (is "\s. \ \\<^bsub>/UNIV\<^esub> {s} ?f ({s'. ?post s 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=isSchedulable_modifies) + apply vcg_step + apply (rule HoarePartial.SeqSwap) + apply (rule_tac I="{t. ?post t s}" in HoarePartial.reannotateWhileNoGuard) + apply (vcg exspec=merge_overlapping_head_refill_tcb_fields + exspec=refill_head_overlapping_tcb_fields) + apply fastforce + apply fastforce + apply (vcg exspec=refill_head_overlapping_tcb_fields) 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) + apply (rule order_refl) + apply vcg + by (clarsimp simp: typ_heap_simps) + +lemma restart_thread_if_no_fault_tcb_fields: + "\s. \\\<^bsub>/UNIV\<^esub> {s} + Call restart_thread_if_no_fault_'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 (rule allI, rule conseqPre) + apply (vcg exspec=possibleSwitchTo_tcb_fields exspec=setThreadState_tcb_fields + exspec=refill_unblock_check_tcb_fields) + apply clarsimp + done lemma ep_queue_relation_shift: "(option_map2 tcbEPNext_C (cslift s') @@ -178,55 +302,6 @@ lemma ctcb_relation_tcbPriority_maxPriority_numPriorities: apply (simp add: maxPriority_def numPriorities_def word_le_nat_alt) done -lemma tcbSchedEnqueue_cslift_precond_discharge: - "\ (s, s') \ rf_sr; obj_at' (P :: tcb \ bool) x s; - ksReadyQueues_asrt s; pspace_aligned' s; pspace_distinct' s; pspace_bounded' s; - valid_objs' s \ \ - (\d v. option_map2 tcbPriority_C (cslift s') (tcb_ptr_to_ctcb_ptr x) = Some v - \ unat v < numPriorities - \ option_map2 tcbDomain_C (cslift s') (tcb_ptr_to_ctcb_ptr x) = Some d - \ unat d < Kernel_Config.numDomains - \ (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) - \ (head_C (index (ksReadyQueues_' (globals s')) (unat (d * 0x100 + v))) \ NULL - \ end_C (index (ksReadyQueues_' (globals s')) (unat (d * 0x100 + v))) \ NULL))" - apply (drule(1) obj_at_cslift_tcb) - apply (clarsimp simp: typ_heap_simps' option_map2_def) - apply (rename_tac tcb tcb') - 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_maxDomain_numDomains - ctcb_relation_tcbPriority_maxPriority_numPriorities) - apply (frule_tac d="tcbDomain tcb" and p="tcbPriority tcb" - in rf_sr_ctcb_queue_relation) - apply (simp add: maxDom_to_H maxPrio_to_H)+ - apply (frule_tac d="tcbDomain tcb" and p="tcbPriority tcb" in head_end_ksReadyQueues_', fastforce+) - apply (simp add: cready_queues_index_to_C_def2 numPriorities_def le_maxDomain_eq_less_numDomains) - apply (clarsimp simp: ctcb_relation_def) - apply (frule arg_cong[where f=unat], subst(asm) unat_ucast_up_simp, simp) - apply (clarsimp simp: ready_queue_relation_def ksReadyQueues_asrt_def) - apply (drule_tac x="tcbDomain tcb" in spec) - apply (drule_tac x="tcbPriority tcb" in spec) - apply clarsimp - apply (prop_tac "tcbQueueHead ((ksReadyQueues s (tcbDomain tcb, tcbPriority tcb))) \ None") - apply (frule tcbQueueHead_iff_tcbQueueEnd) - apply (clarsimp simp: ctcb_queue_relation_def option_to_ctcb_ptr_def) - apply (clarsimp simp: ksReadyQueues_asrt_def) - apply (frule (3) obj_at'_tcbQueueHead_ksReadyQueues) - apply (clarsimp simp: tcbQueueEmpty_def) - apply (rename_tac queue_head) - apply (frule_tac thread=queue_head in obj_at_cslift_tcb) - apply fastforce - apply (clarsimp dest: obj_at_cslift_tcb simp: ctcb_queue_relation_def option_to_ctcb_ptr_def) - done - lemma isRoundRobin_ccorres: "ccorres (\rv rv'. rv = to_bool rv') ret__unsigned_long_' \ \\sc = Ptr scPtr\ [] (isRoundRobin scPtr) (Call isRoundRobin_'proc)" diff --git a/proof/crefine/RISCV64/Recycle_C.thy b/proof/crefine/RISCV64/Recycle_C.thy index 21aa3e8e74..f3d47e982d 100644 --- a/proof/crefine/RISCV64/Recycle_C.thy +++ b/proof/crefine/RISCV64/Recycle_C.thy @@ -805,16 +805,123 @@ lemma ntfn_q_refs'_no_NTFNBound[simp]: "(x, NTFNBound) \ ntfn_q_refs_of' ntfn" by (auto simp: ntfn_q_refs_of'_def split: ntfn.splits) +lemma restart_thread_if_no_fault_ccorres: + "ccorres dc xfdc + (valid_objs' and no_0_obj' and pspace_aligned' and pspace_distinct' and pspace_bounded' + and (\s. ksCurDomain s \ maxDomain) and (\s. weak_sch_act_wf (ksSchedulerAction s) s) + and tcb_at' t) + \\thread = tcb_ptr_to_ctcb_ptr t\ hs + (restartThreadIfNoFault t) + (Call restart_thread_if_no_fault_'proc)" + apply (cinit lift: thread_') + apply (rule ccorres_pre_threadGet, rename_tac fault_opt) + apply (rule ccorres_move_c_guard_tcb) + apply (rule_tac val="case_option (scast seL4_Fault_NullFault) fault_to_fault_tag fault_opt" + and xf'=ret__unsigned_longlong_' + and R="\s. \tcb. ko_at' tcb t s \ tcbFault tcb = fault_opt" + in ccorres_symb_exec_r_known_rv_UNIV[where R'=UNIV]) + apply (vcg, clarsimp) + apply (erule (1) cmap_relation_ko_atE[OF cmap_relation_tcb]) + subgoal + by (fastforce simp: ctcb_relation_def typ_heap_simps cfault_rel_def seL4_Fault_lift_def + Let_def + split: if_split_asm option.split) + apply ceqv + apply (rule ccorres_cond[where R=\]) + apply (clarsimp split: option.splits fault.splits) + apply (rename_tac fault s s', case_tac fault; clarsimp simp: seL4_Faults) + apply (rename_tac arch_fault, case_tac arch_fault, clarsimp simp: seL4_Arch_Faults) + apply (rule ccorres_rhs_assoc)+ + apply (ctac add: setThreadState_ccorres) + apply (clarsimp simp: ifCondRefillUnblockCheck_def) + apply (rule ccorres_pre_threadGet) + apply (rule ccorres_move_c_guard_tcb) + apply (clarsimp simp: when_def) + apply (simp add: if_to_top_of_bind) + apply (rule ccorres_if_lhs) + apply (clarsimp simp: bind_assoc, rename_tac scPtr) + apply (wpfix add: option.sel) + apply (rule ccorres_pre_getObject_sc, rename_tac sc) + apply (rule ccorres_pre_getCurSc, rename_tac cur_sc) + apply (rule_tac xf'="ret__unsigned_long_'" + and val="from_bool (scSporadic sc)" + and R="obj_at' (\tcb. tcbSchedContext tcb = Some scPtr) t and ko_at' sc scPtr + and no_0_obj'" + and R'=UNIV + in ccorres_symb_exec_r_known_rv) + apply (rule conseqPre, vcg) + apply normalise_obj_at' + apply (frule (1) obj_at_cslift_tcb) + apply (frule (1) obj_at_cslift_sc) + apply (clarsimp simp: typ_heap_simps ctcb_relation_def csched_context_relation_def + to_bool_def + split: if_splits) + apply ceqv + apply (rule ccorres_split_nothrow[where r'=dc and xf'=xfdc]) + apply (rule ccorres_cond[where R=\]) + apply fastforce + apply (rule ccorres_move_c_guard_tcb) + apply (rule_tac Q="\s. cur_sc = ksCurSc s + \ obj_at' (\tcb. tcbSchedContext tcb = Some scPtr) t s" + in ccorres_cond_both'[where Q'=\]) + apply clarsimp + apply (frule (1) obj_at_cslift_tcb) + apply (fastforce dest!: rf_sr_ksCurSC simp: typ_heap_simps' ctcb_relation_def) + apply (rule ccorres_move_c_guard_tcb) + apply (ctac add: refill_unblock_check_ccorres) + apply (rule ccorres_return_Skip) + apply (rule ccorres_return_Skip) + apply ceqv + apply (ctac add: possibleSwitchTo_ccorres) + apply wpsimp + apply (vcg exspec=refill_unblock_check_modifies) + apply (vcg exspec=sc_sporadic_modifies) + apply (rule_tac xf'="ret__unsigned_long_'" + and val="from_bool False" + and R="obj_at' (\tcb. tcbSchedContext tcb = None) t" + and R'=UNIV + in ccorres_symb_exec_r_known_rv) + apply (rule conseqPre, vcg) + apply clarsimp + apply (frule (1) obj_at_cslift_tcb) + apply (clarsimp simp: typ_heap_simps ctcb_relation_def) + apply ceqv + apply clarsimp + apply (ctac add: possibleSwitchTo_ccorres) + apply (vcg exspec=sc_sporadic_modifies) + apply (rule_tac Q'="\_. tcb_at' t and valid_objs' and no_0_obj' + and pspace_aligned' and pspace_distinct' and pspace_bounded' + and (\s. ksCurDomain s \ maxDomain) + and (\s. weak_sch_act_wf (ksSchedulerAction s) s)" + in hoare_post_imp) + apply (fastforce simp: obj_at'_def) + apply wpsimp + apply (vcg exspec=setThreadState_modifies) + apply (ctac add: setThreadState_ccorres) + apply (fastforce simp: mask_def[where n=4] ThreadState_defs typ_heap_simps ctcb_relation_def + guard_is_UNIV_def from_bool_def) + apply fastforce + done + +crunch restartThreadIfNoFault + for tcb_at'[wp]: "tcb_at' tcbPtr" + +crunch possibleSwitchTo, ifCondRefillUnblockCheck + for ko_at'_endpoint[wp]: "ko_at' (ep :: endpoint) ptr" + (simp: crunch_simps wp: crunch_wps) + lemma cancelBadgedSends_ccorres: - "ccorres dc xfdc (invs' and ep_at' ptr) - (UNIV \ {s. epptr_' s = Ptr ptr} \ {s. badge___unsigned_long_' s = bdg}) [] - (cancelBadgedSends ptr bdg) (Call cancelBadgedSends_'proc)" + "ccorres dc xfdc + (invs' and ep_at' ptr) + (\\epptr = ep_Ptr ptr\ \ \\badge___unsigned_long = bdg\) [] + (cancelBadgedSends ptr bdg) (Call cancelBadgedSends_'proc)" apply (cinit lift: epptr_' badge___unsigned_long_' simp: whileAnno_def) + apply (rule ccorres_stateAssert)+ apply (simp add: list_case_return cong: list.case_cong Structures_H.endpoint.case_cong call_ignore_cong del: Collect_const) -sorry (* FIXME RT: cancelBadgedSends_ccorres *) (* apply (rule ccorres_pre_getEndpoint) + apply (clarsimp, rename_tac ep) apply (rule_tac R="ko_at' ep ptr" and xf'="ret__unsigned_longlong_'" and val="case ep of RecvEP q \ scast EPState_Recv | IdleEP \ scast EPState_Idle | SendEP q \ scast EPState_Send" @@ -854,22 +961,31 @@ sorry (* FIXME RT: cancelBadgedSends_ccorres *) (* carch_state_relation_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(1) cpspace_relation_ep_update_ep2) - apply (simp add: cendpoint_relation_def endpoint_state_defs) - subgoal by simp + apply (rule conjI) + apply (erule(1) cpspace_relation_ep_update_ep2) + apply (simp add: cendpoint_relation_def endpoint_state_defs) + subgoal by simp + apply (simp add: refill_buffer_relation_def image_def dom_def Let_def typ_heap_simps + update_ep_map_tos) apply (rule ccorres_symb_exec_r) apply (rule_tac xs=list in filterM_voodoo) apply (rule_tac P="\xs s. (\x \ set xs \ set list. - st_tcb_at' (\st. isBlockedOnSend st \ blockingObject st = ptr) x s) - \ distinct (xs @ list) \ ko_at' IdleEP ptr s - \ (\p. \x \ set (xs @ list). \rf. (x, rf) \ {r \ state_refs_of' s p. snd r \ NTFNBound}) - \ pspace_aligned' s \ pspace_distinct' s \ pspace_canonical' s - \ sch_act_wf (ksSchedulerAction s) s \ valid_objs' s - \ ksReadyQueues_head_end s \ ksReadyQueues_head_end_tcb_at' s" - and P'="\xs. {s. ep_queue_relation' (cslift s) (xs @ list) + st_tcb_at' (\st. isBlockedOnSend st + \ blockingObject st = ptr) x s) + \ distinct (xs @ list) \ ko_at' IdleEP ptr s + \ (\p. \x \ set (xs @ list). + \rf. (x, rf) \ {r \ state_refs_of' s p. + snd r \ NTFNBound + \ snd r \ SCTcb + \ snd r \ SCYieldFrom}) + \ pspace_aligned' s \ pspace_distinct' s \ pspace_bounded' s + \ pspace_canonical' s + \ weak_sch_act_wf (ksSchedulerAction s) s + \ valid_objs' s \ no_0_obj' s \ ksCurDomain s \ maxDomain" + and P'="\xs. {s. ep_queue_relation' (cslift s) (xs @ list) (head_C (queue_' s)) (end_C (queue_' s))} - \ {s. thread_' s = (case list of [] \ tcb_Ptr 0 - | x # xs \ tcb_ptr_to_ctcb_ptr x)}" + \ {s. thread_' s = (case list of [] \ tcb_Ptr 0 + | x # xs \ tcb_ptr_to_ctcb_ptr x)}" in ccorres_inst_voodoo) apply (induct_tac list) apply (rule allI) @@ -893,11 +1009,14 @@ sorry (* FIXME RT: cancelBadgedSends_ccorres *) (* packed_heap_update_collapse_hrs carch_state_relation_def cmachine_state_relation_def) - apply (clarsimp simp: cpspace_relation_def typ_heap_simps' - update_ep_map_tos) - apply (erule(1) cpspace_relation_ep_update_ep2) - subgoal by (simp add: cendpoint_relation_def Let_def) - subgoal by simp + apply (clarsimp simp: cpspace_relation_def typ_heap_simps' update_ep_map_tos) + apply (rule conjI) + apply (erule(1) cpspace_relation_ep_update_ep2) + subgoal by (simp add: cendpoint_relation_def Let_def) + subgoal by simp + subgoal + by (simp add: refill_buffer_relation_def image_def dom_def Let_def typ_heap_simps + update_ep_map_tos) apply (clarsimp simp: tcb_at_not_NULL[OF pred_tcb_at'] setEndpoint_def) apply (rule rev_bexI, rule setObject_eq, @@ -908,16 +1027,20 @@ sorry (* FIXME RT: cancelBadgedSends_ccorres *) (* cmachine_state_relation_def) apply (clarsimp simp: cpspace_relation_def typ_heap_simps' update_ep_map_tos) - apply (erule(1) cpspace_relation_ep_update_ep2) - apply (simp add: cendpoint_relation_def Let_def) - apply (subgoal_tac "tcb_at' (last (a # list)) \ \ tcb_at' a \") - apply (clarsimp simp: is_aligned_neg_mask_eq[OF is_aligned_tcb_ptr_to_ctcb_ptr[where P=\]]) - apply (simp add: tcb_queue_relation'_def EPState_Send_def mask_def) - apply (drule (1) tcb_and_not_mask_canonical[where n=2]) - apply (simp (no_asm) add: tcbBlockSizeBits_def) - subgoal by (simp add: mask_def canonical_bit_def) - subgoal by (auto split: if_split) - subgoal by simp + apply (rule conjI) + apply (erule(1) cpspace_relation_ep_update_ep2) + apply (simp add: cendpoint_relation_def Let_def) + apply (subgoal_tac "tcb_at' (last (a # list)) \ \ tcb_at' a \") + apply (clarsimp simp: is_aligned_neg_mask_eq[OF is_aligned_tcb_ptr_to_ctcb_ptr[where P=\]]) + apply (simp add: tcb_queue_relation'_def EPState_Send_def mask_def) + apply (drule (1) tcb_and_not_mask_canonical[where n=2]) + apply (simp (no_asm) add: tcbBlockSizeBits_def) + subgoal by (simp add: mask_def canonical_bit_def) + subgoal by (auto split: if_split) + subgoal by simp + subgoal + by (simp add: refill_buffer_relation_def image_def dom_def Let_def typ_heap_simps + update_ep_map_tos) apply (ctac add: rescheduleRequired_ccorres) apply (rule hoare_pre, wp weak_sch_act_wf_lift_linear set_ep_valid_objs') apply (clarsimp simp: weak_sch_act_wf_def sch_act_wf_def) @@ -957,69 +1080,75 @@ sorry (* FIXME RT: cancelBadgedSends_ccorres *) (* apply (rule ccorres_if_bind, rule ccorres_if_lhs) apply (simp add: bind_assoc) apply (rule ccorres_rhs_assoc)+ - apply (ctac add: setThreadState_ccorres) - apply (ctac add: tcbSchedEnqueue_ccorres) - apply (rule_tac P="\s. \t \ set (x @ a # lista). tcb_at' t s" - in ccorres_cross_over_guard) - apply (rule ccorres_add_return, rule ccorres_split_nothrow[OF _ ceqv_refl]) - apply (rule_tac rrel=dc and xf=xfdc - and P="\s. (\t \ set (x @ a # lista). tcb_at' t s) - \ (\p. \t \ set (x @ a # lista). \rf. (t, rf) \ {r \ state_refs_of' s p. snd r \ NTFNBound}) - \ distinct (x @ a # lista) - \ pspace_aligned' s \ pspace_distinct' s - \ ksReadyQueues_head_end s \ ksReadyQueues_head_end_tcb_at' s" - and P'="{s. ep_queue_relation' (cslift s) (x @ a # lista) - (head_C (queue_' s)) (end_C (queue_' s))}" - in ccorres_from_vcg) - apply (thin_tac "\x. P x" for P) - apply (rule allI, rule conseqPre, vcg) - apply (clarsimp simp: ball_Un) - apply (rule exI, rule conjI) - apply (rule exI, erule conjI) - apply (intro conjI[rotated]) - apply (assumption) + apply (ctac add: restart_thread_if_no_fault_ccorres) + apply (rule_tac P="\s. \t \ set (x @ a # lista). tcb_at' t s" + in ccorres_cross_over_guard) + apply (rule ccorres_add_return, rule ccorres_split_nothrow[OF _ ceqv_refl]) + apply (rule_tac rrel=dc and xf=xfdc + and P="\s. (\t \ set (x @ a # lista). tcb_at' t s) + \ (\p. \t \ set (x @ a # lista). + \rf. (t, rf) \ {r \ state_refs_of' s p. + snd r \ NTFNBound + \ snd r \ SCTcb + \ snd r \ SCYieldFrom}) + \ distinct (x @ a # lista) + \ pspace_aligned' s \ pspace_distinct' s \ pspace_bounded' s + \ ksCurDomain s \ maxDomain" + and P'="{s. ep_queue_relation' (cslift s) (x @ a # lista) + (head_C (queue_' s)) (end_C (queue_' s))}" + in ccorres_from_vcg) + apply (thin_tac "\x. P x" for P) + apply (rule allI, rule conseqPre, vcg) + apply (clarsimp simp: ball_Un) + apply (rule exI, rule conjI) + apply (rule exI, erule conjI) + apply (intro conjI[rotated]) + apply (assumption) apply (fold_subgoals (prefix))[3] - subgoal premises prems using prems by (fastforce intro: pred_tcb_at')+ - apply (clarsimp simp: return_def rf_sr_def cstate_relation_def Let_def) - apply (rule conjI) - apply (clarsimp simp: cpspace_relation_def) - apply (rule conjI, erule ctcb_relation_null_ep_ptrs) - subgoal by (simp add: o_def) - apply (rule conjI) - apply (erule iffD1 [OF cmap_relation_cong, OF refl refl, rotated -1]) - apply clarsimp - apply (rule cendpoint_relation_q_cong) - apply (rule sym, erule restrict_map_eqI) - apply (clarsimp simp: image_iff) - apply (drule(2) map_to_ko_atI) - apply (drule ko_at_state_refs_ofD') - apply clarsimp - apply (drule_tac x=p in spec) - subgoal by fastforce - - apply (erule iffD1 [OF cmap_relation_cong, OF refl refl, rotated -1]) - apply clarsimp - apply (drule(2) map_to_ko_atI, drule ko_at_state_refs_ofD') - - apply (rule cnotification_relation_q_cong) - apply (rule sym, erule restrict_map_eqI) - apply (clarsimp simp: image_iff) - apply (drule_tac x=p in spec) - subgoal by fastforce - apply (clarsimp simp: carch_state_relation_def cmachine_state_relation_def) - apply (rule ccorres_symb_exec_r2) - apply (erule spec) - apply vcg - apply (vcg spec=modifies) - apply wp - apply simp - apply vcg - apply (wp hoare_vcg_const_Ball_lift sch_act_wf_lift) + subgoal premises prems using prems by (fastforce intro: pred_tcb_at')+ + apply (clarsimp simp: return_def rf_sr_def cstate_relation_def Let_def) + apply (rule conjI) + apply (clarsimp simp: cpspace_relation_def) + apply (rule conjI, erule ctcb_relation_null_ep_ptrs) + subgoal by (simp add: o_def) + apply (rule conjI) + apply (erule iffD1 [OF cmap_relation_cong, OF refl refl, rotated -1]) + apply clarsimp + apply (rule cendpoint_relation_q_cong) + apply (rule sym, erule restrict_map_eqI) + apply (clarsimp simp: image_iff) + apply (drule(2) map_to_ko_atI) + apply simp + apply (drule ko_at_state_refs_ofD') + apply clarsimp + apply (drule_tac x=p in spec) + subgoal for \ ep ep' ref rf + by (intro conjI; clarsimp, case_tac ep; clarsimp) + apply (erule iffD1 [OF cmap_relation_cong, OF refl refl, rotated -1]) + apply clarsimp + apply (drule (3) map_to_ko_atI, drule ko_at_state_refs_ofD') + apply (rule cnotification_relation_q_cong) + apply (rule sym, erule restrict_map_eqI) + apply (clarsimp simp: image_iff) + apply (drule_tac x=p in spec) + subgoal for \ ntfn ntfn' ref rf + by (intro conjI; clarsimp, case_tac "ntfnObj ntfn"; clarsimp) + subgoal + by (clarsimp simp: carch_state_relation_def cmachine_state_relation_def + refill_buffer_relation_def) + apply (rule ccorres_symb_exec_r2) + apply (erule spec) + apply vcg + apply (vcg spec=modifies) + apply wp apply simp - apply (vcg exspec=tcbSchedEnqueue_cslift_spec) + apply vcg + apply (clarsimp simp: restartThreadIfNoFault_def) apply (wp hoare_vcg_const_Ball_lift sts_st_tcb_at'_cases - sts_sch_act sts_valid_objs') - apply (vcg exspec=setThreadState_cslift_spec) + sts_sch_act sts_valid_objs' + setThreadState_state_refs_of' threadGet_wp hoare_vcg_all_lift + | wp (once) hoare_drop_imps)+ + apply (vcg exspec=restart_thread_if_no_fault_tcb_fields) apply (simp add: ccorres_cond_iffs) apply (rule ccorres_symb_exec_r2) apply (drule_tac x="x @ [a]" in spec, simp) @@ -1035,20 +1164,7 @@ sorry (* FIXME RT: cancelBadgedSends_ccorres *) (* apply (clarsimp simp: typ_heap_simps st_tcb_at'_def) apply (drule(1) obj_at_cslift_tcb) apply (clarsimp simp: ctcb_relation_blocking_ipc_badge) - apply (rule conjI, simp add: ThreadState_defs mask_def) - 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; simp?) - subgoal by clarsimp - apply clarsimp - apply (rule conjI) - apply (frule tcbSchedEnqueue_cslift_precond_discharge; simp?) - subgoal by clarsimp - apply clarsimp + apply (rule context_conjI) apply (clarsimp simp: tcb_queue_relation'_def) apply (erule iffD2[OF ep_queue_relation_shift[rule_format], rotated -1]) @@ -1077,7 +1193,7 @@ sorry (* FIXME RT: cancelBadgedSends_ccorres *) (* apply clarsimp apply (frule ko_at_valid_objs', clarsimp) apply (simp add: projectKOs) - apply (clarsimp simp: valid_obj'_def valid_ep'_def) + apply (clarsimp simp: valid_obj'_def valid_ep'_def sym_refs_asrt_def sch_act_wf_asrt_def) apply (frule sym_refs_ko_atD', clarsimp) apply (clarsimp simp: st_tcb_at_refs_of_rev') apply (rule conjI) @@ -1085,10 +1201,11 @@ sorry (* FIXME RT: cancelBadgedSends_ccorres *) (* apply (rule conjI) apply (clarsimp split: if_split) apply (drule sym_refsD, clarsimp) - apply (drule(1) bspec)+ - by (auto simp: obj_at'_def projectKOs state_refs_of'_def pred_tcb_at'_def tcb_bound_refs'_def - dest!: symreftype_inverse') *) - + apply (fastforce simp: obj_at'_def projectKOs state_refs_of'_def pred_tcb_at'_def + tcb_bound_refs'_def get_refs_def2 + dest!: symreftype_inverse') + apply fastforce + done lemma tcb_ptr_to_ctcb_ptr_force_fold: "x + 2 ^ ctcb_size_bits = ptr_val (tcb_ptr_to_ctcb_ptr x)" diff --git a/proof/crefine/RISCV64/StateRelation_C.thy b/proof/crefine/RISCV64/StateRelation_C.thy index 022e79ff33..707a2122b0 100644 --- a/proof/crefine/RISCV64/StateRelation_C.thy +++ b/proof/crefine/RISCV64/StateRelation_C.thy @@ -923,6 +923,7 @@ lemmas seL4_Faults = seL4_Fault_UserException_def seL4_Fault_UnknownSyscall_def seL4_Fault_CapFault_def seL4_Fault_Timeout_def + seL4_Fault_NullFault_def lemmas seL4_Arch_Faults = seL4_Fault_VMFault_def