From a6cd4cb84a448e6d44a557826462935835bc3b89 Mon Sep 17 00:00:00 2001 From: Michael McInerney Date: Tue, 20 Sep 2022 15:34:48 +0930 Subject: [PATCH] rt crefine: ADT_C.thy sorry free Signed-off-by: Michael McInerney --- proof/crefine/RISCV64/ADT_C.thy | 124 ++-- proof/crefine/RISCV64/Detype_C.thy | 42 +- proof/crefine/RISCV64/Invoke_C.thy | 95 +++- proof/crefine/RISCV64/IpcCancel_C.thy | 537 ++++++++++-------- proof/crefine/RISCV64/Ipc_C.thy | 662 ++++++++++++---------- proof/crefine/RISCV64/Recycle_C.thy | 10 - proof/crefine/RISCV64/Refine_C.thy | 18 +- proof/crefine/RISCV64/Retype_C.thy | 6 +- proof/crefine/RISCV64/SR_lemmas_C.thy | 10 +- proof/crefine/RISCV64/Schedule_C.thy | 22 +- proof/crefine/RISCV64/StateRelation_C.thy | 10 +- proof/crefine/RISCV64/TcbQueue_C.thy | 21 +- 12 files changed, 925 insertions(+), 632 deletions(-) diff --git a/proof/crefine/RISCV64/ADT_C.thy b/proof/crefine/RISCV64/ADT_C.thy index 0e96105b5c..47bcd8d7a6 100644 --- a/proof/crefine/RISCV64/ADT_C.thy +++ b/proof/crefine/RISCV64/ADT_C.thy @@ -113,12 +113,14 @@ lemma setTCBContext_C_corres: apply (apply_conjunct \match conclusion in \cready_queues_relation _ _ _\ \ \erule cready_queues_relation_not_queue_ptrs; rule ext; simp split: if_split\\) apply (drule ko_at_projectKO_opt) - apply (erule (2) cmap_relation_upd_relI) - apply (simp add: ctcb_relation_def carch_tcb_relation_def) - apply assumption - apply simp + apply (rule conjI) + apply (erule (2) cmap_relation_upd_relI) + apply (simp add: ctcb_relation_def carch_tcb_relation_def) + apply assumption + apply simp + apply (erule iffD2[OF tcb_queue_relation_only_next_prev, rotated -1]) + apply (rule ext, simp split: if_splits)+ done - end definition @@ -615,6 +617,18 @@ lemma cready_queues_to_H_correct: apply (rule_tac hp="clift s" in tcb_queue_rel'_unique, simp_all add: lift_t_NULL) done +definition crelease_queue_to_H :: "(tcb_C ptr \ tcb_C) \ tcb_C ptr \ machine_word list" where + "crelease_queue_to_H h_tcb qhead \ THE aq. sched_queue_relation h_tcb aq NULL qhead" + +lemma crelease_queue_to_H_correct: + "sched_queue_relation (clift s) ls NULL release_hd \ + crelease_queue_to_H (clift s) release_hd = ls" + apply (clarsimp simp: crelease_queue_to_H_def fun_eq_iff) + apply (rule the_equality) + apply simp + apply (rule_tac hp="clift s" in tcb_queue_rel_unique, simp_all add: lift_t_NULL) + done + (* showing that cpspace_relation is actually unique >>>*) lemma cmap_relation_unique_0: @@ -1256,17 +1270,32 @@ lemma ksPSpace_eq_imp_valid_tcb'_eq: valid_tcb'_def valid_tcb_state'_def valid_bound_ntfn'_def split: thread_state.splits option.splits) +lemma ksPSpace_eq_imp_valid_sc'_eq: + assumes ksPSpace: "ksPSpace s' = ksPSpace s" + shows "valid_sched_context' sc s' = valid_sched_context' sc s" + by (auto simp: ksPSpace_eq_imp_obj_at'_eq[OF ksPSpace] + valid_sched_context'_def valid_bound_ntfn'_def + split: option.splits) + +lemma ksPSpace_eq_imp_valid_reply'_eq: + assumes ksPSpace: "ksPSpace s' = ksPSpace s" + shows "valid_reply' reply s' = valid_reply' reply s" + by (auto simp: ksPSpace_eq_imp_obj_at'_eq[OF ksPSpace] + valid_reply'_def valid_bound_ntfn'_def + split: option.splits) + lemma ksPSpace_eq_imp_valid_objs'_eq: assumes ksPSpace: "ksPSpace s' = ksPSpace s" shows "valid_objs' s' = valid_objs' s" using assms - apply (clarsimp simp: valid_objs'_def valid_obj'_def valid_ep'_def + by (clarsimp simp: valid_objs'_def valid_obj'_def valid_ep'_def ksPSpace_eq_imp_obj_at'_eq[OF ksPSpace] ksPSpace_eq_imp_valid_tcb'_eq[OF ksPSpace] ksPSpace_eq_imp_valid_cap'_eq[OF ksPSpace] + ksPSpace_eq_imp_valid_sc'_eq[OF ksPSpace] + ksPSpace_eq_imp_valid_reply'_eq[OF ksPSpace] valid_ntfn'_def valid_cte'_def valid_bound_tcb'_def split: kernel_object.splits endpoint.splits ntfn.splits option.splits) -sorry (* FIXME RT: ksPSpace_eq_imp_valid_objs'_eq *) lemma ksPSpace_eq_imp_valid_pspace'_eq: assumes ksPSpace: "ksPSpace s' = ksPSpace s" @@ -1309,12 +1338,10 @@ context state_rel begin lemma cDomScheduleIdx_to_H_correct: assumes valid: "invs' as" assumes cstate_rel: "cstate_relation as cs" - assumes ms: "cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as)" shows "unat (ksDomScheduleIdx_' cs) = ksDomScheduleIdx as" using assms - apply (clarsimp simp: cstate_relation_def Let_def observable_memory_def invs'_def - newKernelState_def unat_of_nat_eq cdom_schedule_relation_def) -sorry (* FIXME RT: cDomScheduleIdx_to_H_correct *) + by (clarsimp simp: cstate_relation_def Let_def invs'_def valid_dom_schedule'_def + unat_of_nat_eq cdom_schedule_relation_def) definition cDomSchedule_to_H :: "(dschedule_C['b :: finite]) \ (8 word \ machine_word) list" @@ -1412,12 +1439,12 @@ where ksCurDomain = ucast (ksCurDomain_' s), ksDomainTime = ksDomainTime_' s, ksReadyQueues = cready_queues_to_H (clift (t_hrs_' s)) (ksReadyQueues_' s), - ksReleaseQueue = undefined, \ \FIXME RT: write crelease_queue_to_H\ + ksReleaseQueue = crelease_queue_to_H (clift (t_hrs_' s)) (ksReleaseHead_' s), ksReadyQueuesL1Bitmap = cbitmap_L1_to_H (ksReadyQueuesL1Bitmap_' s), ksReadyQueuesL2Bitmap = cbitmap_L2_to_H (ksReadyQueuesL2Bitmap_' s), ksCurThread = ctcb_ptr_to_tcb_ptr (ksCurThread_' s), ksIdleThread = ctcb_ptr_to_tcb_ptr (ksIdleThread_' s), - ksIdleSC = undefined, \ \FIXME RT: the idle sc in the C is the sc of ksIdleThread\ + ksIdleSC = ptr_val (ksIdleSC_' s), ksConsumedTime = ksConsumed_' s, ksCurTime = ksCurTime_' s, ksCurSc = ptr_val (ksCurSC_' s), @@ -1437,15 +1464,16 @@ lemma trivial_eq_conj: "B = C \ (A \ B) = (A \ C)" by simp lemma cstate_to_H_correct: - assumes valid: "invs' as" + assumes invs': "invs' as" + and schact: "sch_act_wf (ksSchedulerAction as) as" assumes cstate_rel: "cstate_relation as cs" shows "cstate_to_H cs = as \ksMachineState:= observable_memory (ksMachineState as) (user_mem' as)\" apply (subgoal_tac "cstate_to_machine_H cs = observable_memory (ksMachineState as) (user_mem' as)") apply (rule kernel_state.equality, simp_all add: cstate_to_H_def) apply (rule cstate_to_pspace_H_correct) - using valid + using invs' apply (simp add: invs'_def) - using cstate_rel valid + using cstate_rel invs' apply (clarsimp simp: cstate_relation_def cpspace_relation_def Let_def observable_memory_def invs'_def valid_pspace'_def) using cstate_rel @@ -1457,39 +1485,51 @@ lemma cstate_to_H_correct: using cstate_rel apply (clarsimp simp: cstate_relation_def cpspace_relation_def Let_def prod_eq_iff) - using valid cstate_rel + using invs' cstate_rel apply (rule mk_gsUntypedZeroRanges_correct) subgoal using cstate_rel by (fastforce simp: cstate_relation_def cpspace_relation_def Let_def ghost_size_rel_def unat_eq_0 split: if_split) - using valid cstate_rel + using invs' cstate_rel apply (rule cDomScheduleIdx_to_H_correct) using cstate_rel apply (clarsimp simp: cstate_relation_def Let_def) - using valid cstate_rel - apply (rule cDomSchedule_to_H_correct) + using invs' cstate_rel + apply (rule cDomSchedule_to_H_correct) + using cstate_rel + apply (clarsimp simp: cstate_relation_def Let_def) + using cstate_rel + apply (clarsimp simp: cstate_relation_def Let_def ucast_up_ucast_id is_up_8_32) using cstate_rel apply (clarsimp simp: cstate_relation_def Let_def) + apply (rule cready_queues_to_H_correct) using cstate_rel - apply (clarsimp simp: cstate_relation_def Let_def ucast_up_ucast_id is_up_8_32) + apply (clarsimp simp: cstate_relation_def Let_def) + apply (rule crelease_queue_to_H_correct) using cstate_rel apply (clarsimp simp: cstate_relation_def Let_def) - apply (rule cready_queues_to_H_correct) using cstate_rel apply (clarsimp simp: cstate_relation_def Let_def) -sorry (* FIXME RT: cstate_to_H_correct - using cstate_rel - apply (clarsimp simp: cstate_relation_def Let_def) + using cstate_rel + apply (clarsimp simp: cstate_relation_def Let_def) + apply (rule cbitmap_L1_to_H_correct) + apply (clarsimp simp: cstate_relation_def Let_def) + using cstate_rel + apply (clarsimp simp: cstate_relation_def Let_def) + apply (rule cbitmap_L2_to_H_correct) + apply (clarsimp simp: cstate_relation_def Let_def) + using cstate_rel + apply (clarsimp simp: cstate_relation_def Let_def) + using cstate_rel + apply (clarsimp simp: cstate_relation_def Let_def) + using cstate_rel + apply (clarsimp simp: cstate_relation_def Let_def) using cstate_rel apply (clarsimp simp: cstate_relation_def Let_def) - apply (rule cbitmap_L1_to_H_correct) - apply (clarsimp simp: cstate_relation_def Let_def) using cstate_rel apply (clarsimp simp: cstate_relation_def Let_def) - apply (rule cbitmap_L2_to_H_correct) - apply (clarsimp simp: cstate_relation_def Let_def) using cstate_rel apply (clarsimp simp: cstate_relation_def Let_def) using cstate_rel @@ -1498,23 +1538,23 @@ sorry (* FIXME RT: cstate_to_H_correct apply (clarsimp simp: cstate_relation_def Let_def) apply (rule csch_act_rel_to_H[THEN iffD1]) apply (case_tac "ksSchedulerAction as", simp+) - using valid + using schact subgoal - by (clarsimp simp: valid_state'_def st_tcb_at'_def - obj_at'_real_def ko_wp_at'_def objBitsKO_def projectKO_opt_tcb - split: kernel_object.splits) + by (clarsimp simp: st_tcb_at'_def obj_at'_real_def ko_wp_at'_def objBitsKO_def + projectKO_opt_tcb + split: kernel_object.splits) using cstate_rel apply (clarsimp simp: cstate_relation_def Let_def) apply (rule cint_rel_to_H) - using valid - apply (simp add: valid_state'_def) + using invs' + apply (simp add: invs'_def) using cstate_rel apply (clarsimp simp: cstate_relation_def Let_def) using cstate_rel apply (clarsimp simp: cstate_relation_def Let_def) apply (rule carch_state_to_H_correct) - using valid - apply (simp add: valid_state'_def) + using invs' + apply (simp add: invs'_def) using cstate_rel apply (clarsimp simp: cstate_relation_def Let_def) using cstate_rel @@ -1522,17 +1562,17 @@ sorry (* FIXME RT: cstate_to_H_correct using cstate_rel apply (clarsimp simp: cstate_relation_def Let_def carch_state_relation_def carch_globals_def) apply (rule cstate_to_machine_H_correct[simplified]) - using valid - apply (simp add: valid_state'_def) + using invs' + apply (simp add: invs'_def) using cstate_rel apply (simp add: cstate_relation_def Let_def) using cstate_rel apply (simp add: cstate_relation_def Let_def cpspace_relation_def) using cstate_rel apply (simp add: cstate_relation_def Let_def cpspace_relation_def) - using valid - apply (clarsimp simp add: valid_state'_def) - done *) + using invs' + apply (clarsimp simp add: invs'_def) + done end diff --git a/proof/crefine/RISCV64/Detype_C.thy b/proof/crefine/RISCV64/Detype_C.thy index b080bdd1dd..d13294483e 100644 --- a/proof/crefine/RISCV64/Detype_C.thy +++ b/proof/crefine/RISCV64/Detype_C.thy @@ -859,15 +859,14 @@ proof - qed qed - -lemma tcb_queue_relation_live_restrict: +lemma tcb_queue_relation_live_restrict': assumes vuc: "s \' capability.UntypedCap d ptr bits idx" and rel: "\t \ set q. tcb_at' t s" and live: "\t \ set q. ko_wp_at' live' t s" and rl: "\(p :: machine_word) P. ko_wp_at' P p s \ (\ko. P ko \ live' ko) \ p \ {ptr..ptr + 2 ^ bits - 1}" - shows "tcb_queue_relation' getNext getPrev (cm |` (- Ptr ` {ptr..+2 ^ bits})) q cend chead = - tcb_queue_relation' getNext getPrev cm q cend chead" -proof (rule tcb_queue_relation'_cong [OF refl refl refl]) + shows "tcb_queue_relation getNext getPrev (cm |` (- Ptr ` {ptr..+2 ^ bits})) q prev chead = + tcb_queue_relation getNext getPrev cm q prev chead" +proof (rule tcb_queue_relation_cong [OF refl refl refl]) fix p assume "p \ tcb_ptr_to_ctcb_ptr ` set q" @@ -896,6 +895,16 @@ proof (rule tcb_queue_relation'_cong [OF refl refl refl]) thus "(cm |` (- Ptr ` {ptr..+2 ^ bits})) p = cm p" by simp qed +lemma tcb_queue_relation_live_restrict: + assumes vuc: "s \' capability.UntypedCap d ptr bits idx" + and rel: "\t \ set q. tcb_at' t s" + and live: "\t \ set q. ko_wp_at' live' t s" + and rl: "\(p :: machine_word) P. ko_wp_at' P p s \ (\ko. P ko \ live' ko) \ p \ {ptr..ptr + 2 ^ bits - 1}" + shows "tcb_queue_relation' getNext getPrev (cm |` (- Ptr ` {ptr..+2 ^ bits})) q cend chead = + tcb_queue_relation' getNext getPrev cm q cend chead" + using assms + by (fastforce simp: tcb_queue_relation'_def tcb_queue_relation_live_restrict') + fun epQ :: "endpoint \ machine_word list" where @@ -1693,6 +1702,29 @@ proof - [OF D.valid_untyped tat tlive rl]) done + moreover + from rlqrun have "\t \ set (ksReleaseQueue s). tcb_at' t s \ ko_wp_at' live' t s" + apply clarsimp + apply (rule context_conjI) + apply fastforce + apply (drule_tac x=t in spec) + apply (clarsimp simp: ko_wp_at'_def obj_at_simps split: kernel_object.splits) + apply (rule_tac x="KOTCB obj" in exI) + apply (case_tac "tcbState obj"; clarsimp split: thread_state.splits) + done + hence tat: "\t \ set (ksReleaseQueue s). tcb_at' t s" + and tlive: "\t \ set (ksReleaseQueue s). ko_wp_at' live' t s" + by auto + from sr have + "sched_queue_relation (clift ?th_s) (ksReleaseQueue s) NULL (ksReleaseHead_' (globals s'))" + unfolding rf_sr_def cstate_relation_def cpspace_relation_def + apply (simp add: tcb_queue_relation_live_restrict') + apply (clarsimp simp: Let_def all_conj_distrib) + apply ((subst lift_t_typ_region_bytes, rule cm_disj_tcb, assumption+, simp_all)[1])+ + apply (insert rlqrun tat tlive rl) + apply (rule tcb_queue_relation_live_restrict'[THEN iffD2], (fastforce intro!: D.valid_untyped)+) + done + moreover { assume "s' \\<^sub>c riscvKSGlobalPT_Ptr" diff --git a/proof/crefine/RISCV64/Invoke_C.thy b/proof/crefine/RISCV64/Invoke_C.thy index ed9b919cdf..ebff9fe032 100644 --- a/proof/crefine/RISCV64/Invoke_C.thy +++ b/proof/crefine/RISCV64/Invoke_C.thy @@ -40,10 +40,42 @@ lemma cap_case_ThreadCap2: by (simp add: isCap_simps split: capability.split) +lemma threadSet_isSchedulable_bool: + "\\tcb. tcbState tcb = tcbState (f tcb); \tcb. tcbInReleaseQueue tcb = tcbInReleaseQueue (f tcb); + \tcb. tcbSchedContext tcb = tcbSchedContext (f tcb)\ + \ threadSet f t \\s. P (isSchedulable_bool t s)\" + apply (wpsimp wp: threadSet_wp) + apply (erule_tac P=P in back_subst) + apply (fastforce simp: pred_map_simps isSchedulable_bool_def isScActive_def opt_map_def obj_at_simps + split: if_splits option.splits) + done + +lemma tcbSchedDequeue_isSchedulable_bool[wp]: + "tcbSchedDequeue t \\s. P (isSchedulable_bool t s)\" + unfolding tcbSchedDequeue_def setQueue_def + apply (wpsimp wp: threadSet_isSchedulable_bool threadGet_wp simp: bitmap_fun_defs) + apply (fastforce simp: isSchedulable_bool_def isScActive_def obj_at_simps + split: if_splits) + done + +lemma threadSet_ready_or_release'[wp]: + "threadSet f tptr \ready_or_release'\" + unfolding threadSet_def + apply (wpsimp wp: setObject_tcb_wp getTCB_wp') + apply (clarsimp simp: ready_or_release'_def) + done + +lemma tcbSchedDequeue_ready_or_release'_inv: + "tcbSchedDequeue tptr \ready_or_release'\" + unfolding tcbSchedDequeue_def setQueue_def + apply (wpsimp wp: threadGet_wp simp: bitmap_fun_defs) + apply (fastforce simp: ready_or_release'_def obj_at_simps split: if_splits) + done + lemma setDomain_ccorres: "ccorres dc xfdc (invs' and tcb_at' t and sch_act_simple and (\s. \d p. distinct (ksReadyQueues s (d, p))) - and (\s. d \ maxDomain)) + and ready_or_release' and (\s. d \ maxDomain)) (UNIV \ {s. tptr_' s = tcb_ptr_to_ctcb_ptr t} \ {s. dom_' s = ucast d}) [] (setDomain t d) (Call setDomain_'proc)" apply (rule ccorres_gen_asm) @@ -76,22 +108,29 @@ lemma setDomain_ccorres: apply (simp add: guard_is_UNIV_def) apply simp apply wp - apply (rule_tac Q="\_. invs' and tcb_at' t and sch_act_simple - and (\s. curThread = ksCurThread s) - and (\s. \d p. distinct (ksReadyQueues s (d, p)))" + apply (rule_tac Q="\rv'. invs' and tcb_at' t and sch_act_simple + and (\s. curThread = ksCurThread s) + and (\s. \d p. distinct (ksReadyQueues s (d, p))) + and (\s. rv' \ \ t \ set (ksReleaseQueue s)) + and ready_or_release'" in hoare_strengthen_post) - apply wp + apply (wpsimp wp: isSchedulable_wp) apply (fastforce simp: valid_pspace_valid_objs' weak_sch_act_wf_def split: if_splits) apply (rule_tac Q="\_. invs' and tcb_at' t and sch_act_simple and (\s. curThread = ksCurThread s \ (\p. t \ set (ksReadyQueues s p))) - and (\s. \d p. distinct (ksReadyQueues s (d, p)))" + and (\s. \d p. distinct (ksReadyQueues s (d, p))) + and (\s. isSchedulable_bool t s \ \ t \ set (ksReleaseQueue s)) + and ready_or_release'" in hoare_strengthen_post) - apply (wpsimp wp: threadSet_tcbDomain_update_invs') - apply fastforce + apply (wpsimp wp: threadSet_tcbDomain_update_invs' hoare_vcg_imp_lift' + threadSet_isSchedulable_bool)+ apply (simp add: guard_is_UNIV_def) - apply (wp tcbSchedDequeue_not_in_queue hoare_vcg_all_lift) - apply fastforce + apply (wpsimp wp: tcbSchedDequeue_not_in_queue hoare_vcg_all_lift hoare_vcg_imp_lift' + tcbSchedDequeue_ready_or_release'_inv) + apply (fastforce dest: invs_valid_release_queue + simp: isSchedulable_bool_def pred_map_simps opt_map_def obj_at_simps + valid_release_queue_def) done lemma active_runnable': @@ -114,6 +153,37 @@ lemma setThreadState_ksReadyQueues_distinct: apply (wpsimp wp: tcbSchedEnqueue_ksReadyQueues_distinct isSchedulable_wp threadSet_wp) by (fastforce split: if_splits) +lemma tcbSchedEnqueue_ready_or_release'[wp]: + "\\s. ready_or_release' s \ tcbPtr \ set (ksReleaseQueue s)\ + tcbSchedEnqueue tcbPtr + \\_. ready_or_release'\" + unfolding tcbSchedEnqueue_def setQueue_def + apply (wpsimp wp: threadGet_wp simp: bitmap_fun_defs) + apply (fastforce simp: ready_or_release'_def obj_at_simps split: if_splits) + done + +lemma ready_or_release'_ksSchedulerAction_update[simp]: + "ready_or_release' (ksSchedulerAction_update f s) = ready_or_release' s" + by (fastforce simp: ready_or_release'_def) + +lemma rescheduleRequired_ready_or_release'[wp]: + "\valid_release_queue and ready_or_release'\ + rescheduleRequired + \\_. ready_or_release'\" + unfolding rescheduleRequired_def + apply (wpsimp wp: isSchedulable_wp) + apply (fastforce simp: isSchedulable_bool_def opt_map_def pred_map_simps valid_release_queue_def + obj_at_simps + split: if_splits) + done + +lemma setThreadState_ready_or_release'[wp]: + "\ready_or_release' and valid_release_queue\ + setThreadState f tptr + \\_. ready_or_release'\" + unfolding setThreadState_def scheduleTCB_def + by (wpsimp wp: hoare_vcg_if_lift2 hoare_drop_imps threadSet_vrq_inv) + lemma decodeDomainInvocation_ccorres: notes Collect_const[simp del] shows @@ -128,7 +198,8 @@ lemma decodeDomainInvocation_ccorres: s \' fst v) and sysargs_rel args buffer and (\s. \d p. distinct (ksReadyQueues s (d, p)) \ thread \ set (ksReadyQueues s (d,p))) - and (\s. sch_act_wf (ksSchedulerAction s) s)) + and (\s. sch_act_wf (ksSchedulerAction s) s) + and ready_or_release') (UNIV \ {s. unat (length___unsigned_long_' s) = length args} \ {s. current_extra_caps_' (globals s) = extraCaps'} @@ -227,6 +298,8 @@ lemma decodeDomainInvocation_ccorres: apply (clarsimp simp: valid_cap_simps' pred_tcb'_weakenE active_runnable') apply (rule conjI) apply (fastforce simp: tcb_st_refs_of'_def elim:pred_tcb'_weakenE) + apply (rule conjI) + apply fastforce apply (simp add: word_le_nat_alt unat_ucast unat_numDomains_to_H le_maxDomain_eq_less_numDomains) apply (clarsimp simp: ccap_relation_def cap_to_H_simps cap_thread_cap_lift) subgoal (* args ! 0 can be contained in a domain-sized word *) diff --git a/proof/crefine/RISCV64/IpcCancel_C.thy b/proof/crefine/RISCV64/IpcCancel_C.thy index d283b2f17c..188c9024cd 100644 --- a/proof/crefine/RISCV64/IpcCancel_C.thy +++ b/proof/crefine/RISCV64/IpcCancel_C.thy @@ -185,7 +185,6 @@ lemma ntfn_ptr_set_queue_spec: apply (clarsimp simp: packed_heap_update_collapse_hrs typ_heap_simps' canonical_bit_def) done - lemma cancelSignal_ccorres_helper: "ccorres dc xfdc (invs' and (\s. sym_refs (state_refs_of' s)) and st_tcb_at' ((=) (BlockedOnNotification ntfn)) thread and ko_at' ntfn' ntfn) @@ -238,22 +237,27 @@ lemma cancelSignal_ccorres_helper: typ_heap_simps') apply (elim conjE) apply (intro conjI) - \ \tcb relation\ - apply (erule ctcb_relation_null_queue_ptrs) - apply (clarsimp simp: comp_def) - \ \ep relation\ - apply (erule iffD1 [OF cmap_relation_cong, OF refl refl, rotated -1]) - apply simp - apply (rule cendpoint_relation_ntfn_queue, assumption+) + \ \tcb relation\ + apply (erule ctcb_relation_null_queue_ptrs) + apply (clarsimp simp: comp_def) + \ \ep relation\ + apply (erule iffD1 [OF cmap_relation_cong, OF refl refl, rotated -1]) apply simp - apply (erule (1) map_to_ko_atI') - \ \ntfn relation\ - apply (rule cpspace_relation_ntfn_update_ntfn, assumption+) - apply (simp add: cnotification_relation_def Let_def NtfnState_Idle_def) - apply (simp add: carch_state_relation_def carch_globals_def) - subgoal sorry (* FIXME RT: refill_buffer_relation *) - \ \queue relation\ - apply (rule cready_queues_relation_null_queue_ptrs, assumption+) + apply (rule cendpoint_relation_ntfn_queue, assumption+) + apply simp + apply (erule (1) map_to_ko_atI') + \ \ntfn relation\ + apply (rule cpspace_relation_ntfn_update_ntfn, assumption+) + apply (simp add: cnotification_relation_def Let_def NtfnState_Idle_def) + apply (simp add: carch_state_relation_def carch_globals_def) + subgoal sorry (* FIXME RT: refill_buffer_relation *) + \ \queue relations\ + apply (rule cready_queues_relation_null_queue_ptrs, assumption+) + apply (clarsimp simp: comp_def) + apply (erule iffD2[OF tcb_queue_relation_only_next_prev, rotated -1]) + apply (rule null_ep_schedD[THEN conjunct1]) + apply (clarsimp simp: comp_def) + apply (rule null_ep_schedD[THEN conjunct2]) apply (clarsimp simp: comp_def) apply (clarsimp simp: carch_state_relation_def carch_globals_def typ_heap_simps' packed_heap_update_collapse_hrs) @@ -275,34 +279,39 @@ lemma cancelSignal_ccorres_helper: typ_heap_simps') apply (elim conjE) apply (intro conjI) - \ \tcb relation\ - apply (erule ctcb_relation_null_queue_ptrs) - apply (clarsimp simp: comp_def) - \ \ep relation\ - apply (erule iffD1 [OF cmap_relation_cong, OF refl refl, rotated -1]) - apply simp - apply (rule cendpoint_relation_ntfn_queue) - apply fastforce - apply assumption+ - apply simp - apply (erule (1) map_to_ko_atI') - \ \ntfn relation\ - apply (rule cpspace_relation_ntfn_update_ntfn, assumption+) - apply (simp add: cnotification_relation_def Let_def isWaitingNtfn_def - split: ntfn.splits split del: if_split) - apply (erule iffD1 [OF tcb_queue_relation'_cong [OF refl _ _ refl], rotated -1]) - apply (clarsimp simp add: h_t_valid_clift_Some_iff) - apply (subst tcb_queue_relation'_next_sign; assumption?) + \ \tcb relation\ + apply (erule ctcb_relation_null_queue_ptrs) + apply (clarsimp simp: comp_def) + \ \ep relation\ + apply (erule iffD1 [OF cmap_relation_cong, OF refl refl, rotated -1]) + apply simp + apply (rule cendpoint_relation_ntfn_queue) + apply fastforce + apply assumption+ + apply simp + apply (erule (1) map_to_ko_atI') + \ \ntfn relation\ + apply (rule cpspace_relation_ntfn_update_ntfn, assumption+) + apply (simp add: cnotification_relation_def Let_def isWaitingNtfn_def + split: ntfn.splits split del: if_split) + apply (erule iffD1 [OF tcb_queue_relation'_cong [OF refl _ _ refl], rotated -1]) + apply (clarsimp simp add: h_t_valid_clift_Some_iff) + apply (subst tcb_queue_relation'_next_sign; assumption?) + apply fastforce + apply (simp add: notification_lift_def sign_extend_sign_extend_eq canonical_bit_def) + apply (clarsimp simp: h_t_valid_clift_Some_iff notification_lift_def sign_extend_sign_extend_eq) + apply (subst tcb_queue_relation'_prev_sign; assumption?) apply fastforce - apply (simp add: notification_lift_def sign_extend_sign_extend_eq canonical_bit_def) - apply (clarsimp simp: h_t_valid_clift_Some_iff notification_lift_def sign_extend_sign_extend_eq) - apply (subst tcb_queue_relation'_prev_sign; assumption?) - apply fastforce - apply (simp add: canonical_bit_def) - apply simp - \ \queue relation\ - subgoal sorry (* FIXME RT: refill_buffer_relation *) - apply (rule cready_queues_relation_null_queue_ptrs, assumption+) + apply (simp add: canonical_bit_def) + apply simp + \ \queue relations\ + subgoal sorry (* FIXME RT: refill_buffer_relation *) + apply (rule cready_queues_relation_null_queue_ptrs, assumption+) + apply (clarsimp simp: comp_def) + apply (erule iffD2[OF tcb_queue_relation_only_next_prev, rotated -1]) + apply (rule null_ep_schedD[THEN conjunct1]) + apply (clarsimp simp: comp_def) + apply (rule null_ep_schedD[THEN conjunct2]) apply (clarsimp simp: comp_def) subgoal by (clarsimp simp: carch_state_relation_def carch_globals_def) subgoal by (simp add: cmachine_state_relation_def) @@ -710,7 +719,8 @@ lemma state_relation_queue_update_helper': \ obj_at' (\tcb. tcbDomain tcb = qdom) x s) \ (tcb_at' x s \ (\d' p'. (d' \ qdom \ p' \ prio) \ x \ set (ksReadyQueues s (d', p')))); - S \ {}; qdom \ ucast maxDom; prio \ ucast maxPrio \ + S \ {}; qdom \ ucast maxDom; prio \ ucast maxPrio; + set (ksReleaseQueue s) \ S = {} \ \ (s \ksReadyQueues := (ksReadyQueues s)((qdom, prio) := q)\, t) \ rf_sr" apply (subst(asm) disj_imp_rhs) apply (subst obj_at'_and[symmetric]) @@ -727,39 +737,47 @@ lemma state_relation_queue_update_helper': apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def) apply (intro conjI) \ \cpspace_relation\ - apply (erule nonemptyE, drule(1) bspec) - apply (clarsimp simp: cpspace_relation_def) - apply (drule obj_at_ko_at', clarsimp) - apply (rule cmap_relationE1, assumption, - erule ko_at_projectKO_opt) - apply (frule null_sched_queue) - apply (frule null_sched_epD) - apply (intro conjI) - \ \tcb relation\ - apply (drule ctcb_relation_null_queue_ptrs, - simp_all)[1] - \ \endpoint relation\ + apply (erule nonemptyE, drule(1) bspec) + apply (clarsimp simp: cpspace_relation_def) + apply (drule obj_at_ko_at', clarsimp) + apply (rule cmap_relationE1, assumption, + erule ko_at_projectKO_opt) + apply (frule null_sched_queue) + apply (frule null_sched_epD) + apply (intro conjI) + \ \tcb relation\ + apply (drule ctcb_relation_null_queue_ptrs, + simp_all)[1] + \ \endpoint relation\ + apply (erule iffD1 [OF cmap_relation_cong, OF refl refl, rotated -1]) + apply simp + apply (erule cendpoint_relation_upd_tcb_no_queues, simp+) + \ \ntfn relation\ apply (erule iffD1 [OF cmap_relation_cong, OF refl refl, rotated -1]) apply simp - apply (erule cendpoint_relation_upd_tcb_no_queues, simp+) - \ \ntfn relation\ - apply (erule iffD1 [OF cmap_relation_cong, OF refl refl, rotated -1]) - apply simp - apply (erule cnotification_relation_upd_tcb_no_queues, simp+) - \ \refill_buffer_relation\ - apply (clarsimp simp: refill_buffer_relation_def typ_heap_simps) - \ \ready queues\ - apply (simp add: cready_queues_relation_def Let_def cready_queues_index_to_C_in_range - seL4_MinPrio_def minDom_def) - apply clarsimp - apply (frule cready_queues_index_to_C_distinct, assumption+) - apply (clarsimp simp: cready_queues_index_to_C_in_range all_conj_distrib) - apply (rule iffD1 [OF tcb_queue_relation'_cong[OF refl], rotated -1], - drule spec, drule spec, erule mp, simp+) + apply (erule cnotification_relation_upd_tcb_no_queues, simp+) + \ \refill_buffer_relation\ + apply (clarsimp simp: refill_buffer_relation_def typ_heap_simps) + \ \ready queues\ + apply (simp add: cready_queues_relation_def Let_def cready_queues_index_to_C_in_range + seL4_MinPrio_def minDom_def) + apply clarsimp + apply (frule cready_queues_index_to_C_distinct, assumption+) + apply (clarsimp simp: cready_queues_index_to_C_in_range all_conj_distrib) + apply (rule iffD1 [OF tcb_queue_relation'_cong[OF refl], rotated -1], + drule spec, drule spec, erule mp, simp+) + apply clarsimp + apply (drule_tac x="tcb_ptr_to_ctcb_ptr x" in fun_cong)+ + apply (clarsimp simp: restrict_map_def + split: if_split_asm) + \ \release queue\ + apply (rule_tac mp'1="lift_t c_guard (f (t_hrs_' (globals s')))" + and mp1="lift_t c_guard ((t_hrs_' (globals s')))" + in iffD1[OF tcb_queue_relation_cong]; + simp?) apply clarsimp apply (drule_tac x="tcb_ptr_to_ctcb_ptr x" in fun_cong)+ - apply (clarsimp simp: restrict_map_def - split: if_split_asm) + subgoal by (auto simp: restrict_map_def split: if_split_asm) by (auto simp: carch_state_relation_def cmachine_state_relation_def) lemma state_relation_queue_update_helper: @@ -782,7 +800,8 @@ lemma state_relation_queue_update_helper: \ obj_at' (\tcb. tcbDomain tcb = qdom) x s) \ (tcb_at' x s \ (\d' p'. (d' \ qdom \ p' \ prio) \ x \ set (ksReadyQueues s (d', p')))); - S \ {}; qdom \ ucast maxDom; prio \ ucast maxPrio \ + S \ {}; qdom \ ucast maxDom; prio \ ucast maxPrio; + set (ksReleaseQueue s) \ S = {} \ \ (s \ksReadyQueues := (ksReadyQueues s)((qdom, prio) := q)\, t) \ rf_sr" apply (subgoal_tac "\d p. (\t\set (ksReadyQueues s (d, p)). obj_at' (inQ d p) t s) \ distinct (ksReadyQueues s (d, p))") @@ -993,14 +1012,62 @@ lemma c_invert_assist: "3 - (ucast (p :: priority) >> 6 :: machine_word) < 4" using prio_ucast_shiftr_wordRadix_helper'[simplified wordRadix_def] by - (rule word_less_imp_diff_less, simp_all) +lemma tcb_queue_relation_prev_next: + "\ tcb_queue_relation tn tp' mp queue qprev qhead; + tcbp \ set queue; distinct (ctcb_ptr_to_tcb_ptr qprev # queue); + \t \ set queue. tcb_at' t s; qprev \ tcb_Ptr 0 \ mp qprev \ None; + mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb \ + \ (tn tcb \ tcb_Ptr 0 \ tn tcb \ tcb_ptr_to_ctcb_ptr ` set queue + \ mp (tn tcb) \ None \ tn tcb \ tcb_ptr_to_ctcb_ptr tcbp) + \ (tp' tcb \ tcb_Ptr 0 \ (tp' tcb \ tcb_ptr_to_ctcb_ptr ` set queue + \ tp' tcb = qprev) + \ mp (tp' tcb) \ None \ tp' tcb \ tcb_ptr_to_ctcb_ptr tcbp) + \ (tn tcb \ tcb_Ptr 0 \ tn tcb \ tp' tcb)" + apply (induct queue arbitrary: qprev qhead) + apply simp + apply simp + apply (erule disjE) + apply clarsimp + apply (case_tac "queue") + apply clarsimp + apply clarsimp + apply (rule conjI) + apply clarsimp + apply clarsimp + apply (drule_tac f=ctcb_ptr_to_tcb_ptr in arg_cong[where y="tp' tcb"], simp) + apply clarsimp + apply fastforce + done + +lemma tcb_queue_relation_prev_next': + "\ tcb_queue_relation' tn tp' mp queue qhead qend; tcbp \ set queue; distinct queue; + \t \ set queue. tcb_at' t s; mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb \ + \ (tn tcb \ tcb_Ptr 0 \ tn tcb \ tcb_ptr_to_ctcb_ptr ` set queue + \ mp (tn tcb) \ None \ tn tcb \ tcb_ptr_to_ctcb_ptr tcbp) + \ (tp' tcb \ tcb_Ptr 0 \ tp' tcb \ tcb_ptr_to_ctcb_ptr ` set queue + \ mp (tp' tcb) \ None \ tp' tcb \ tcb_ptr_to_ctcb_ptr tcbp) + \ (tn tcb \ tcb_Ptr 0 \ tn tcb \ tp' tcb)" + apply (clarsimp simp: tcb_queue_relation'_def split: if_split_asm) + apply (drule(1) tcb_queue_relation_prev_next, simp_all) + apply (fastforce dest: tcb_at_not_NULL) + apply clarsimp + done + +(* FIXME RT: move to Refine *) +definition ready_or_release' :: "kernel_state \ bool" where + "ready_or_release' s \ \t. \ (\d p. t \ set (ksReadyQueues s (d,p)) \ t \ set (ksReleaseQueue s))" + +(* FIXME RT: move to Refine *) +lemma ready_or_release'_disjoint_queues: + "ready_or_release' s \ \d p. set (ksReadyQueues s (d, p)) \ set (ksReleaseQueue s) = {}" + by (fastforce simp: ready_or_release'_def) + lemma tcbSchedEnqueue_ccorres: "ccorres dc xfdc - (valid_queues and tcb_at' t and valid_objs' - and (\s. \d p. distinct (ksReadyQueues s (d, p)))) - (UNIV \ \\tcb = tcb_ptr_to_ctcb_ptr t\) - hs - (tcbSchedEnqueue t) - (Call tcbSchedEnqueue_'proc)" + (valid_queues and tcb_at' t and valid_objs' and (\s. \d p. distinct (ksReadyQueues s (d, p))) + and (\s. t \ set (ksReleaseQueue s)) and ready_or_release') + \\tcb = tcb_ptr_to_ctcb_ptr t\ hs + (tcbSchedEnqueue t) (Call tcbSchedEnqueue_'proc)" proof - note prio_and_dom_limit_helpers[simp] word_sle_def[simp] maxDom_to_H[simp] maxPrio_to_H[simp] note invert_prioToL1Index_c_simp[simp] @@ -1056,7 +1123,9 @@ proof - apply (rule_tac P="\s. valid_queues s \ (\p. t \ set (ksReadyQueues s p)) \ (\tcb. ko_at' tcb t s \ tcbDomain tcb =rva \ tcbPriority tcb = rvb \ valid_tcb' tcb s) - \ (\d p. distinct (ksReadyQueues s (d, p)))" + \ (\d p. distinct (ksReadyQueues s (d, p))) + \ t \ set (ksReleaseQueue s) + \ ready_or_release' s" and P'=UNIV in ccorres_from_vcg) apply (rule allI, rule conseqPre, vcg) apply (clarsimp simp: getQueue_def gets_def get_def setQueue_def modify_def @@ -1146,24 +1215,31 @@ proof - apply (rule tcb_at_not_NULL, erule obj_at'_weakenE, simp) apply (frule(2) obj_at_cslift_tcb[OF valid_queues_obj_at'D]) apply (clarsimp simp: h_val_field_clift' h_t_valid_clift) - apply (erule_tac S="{t, v}" for v in state_relation_queue_update_helper, + apply (rule_tac S="set (t # ksReadyQueues \ (tcbDomain tcb, tcbPriority tcb))" + in state_relation_queue_update_helper, (simp | rule globals.equality)+, simp_all add: typ_heap_simps if_Some_helper numPriorities_def cready_queues_index_to_C_def2 upd_unless_null_def del: fun_upd_restrict_conv cong: if_cong split del: if_split)[1] - apply simp - apply (rule conjI) - apply clarsimp - apply (drule_tac s="tcb_ptr_to_ctcb_ptr t" in sym, simp) - apply (clarsimp simp add: fun_upd_twist) - prefer 4 - apply (simp add: obj_at'_weakenE[OF _ TrueI]) - apply (rule disjI1, erule (1) valid_queues_obj_at'D) - apply clarsimp - apply (fastforce simp: tcb_null_sched_ptrs_def) - apply (simp add: typ_heap_simps c_guard_clift) + apply simp + apply (rule conjI) + apply clarsimp + apply (drule_tac s="tcb_ptr_to_ctcb_ptr t" in sym, simp) + apply (clarsimp simp add: fun_upd_twist) + prefer 4 + apply (simp add: obj_at'_weakenE[OF _ TrueI]) + apply (fastforce intro!: valid_queues_obj_at'D) + apply (rule ext) + apply (clarsimp split: if_splits simp: typ_heap_simps) + apply (frule rf_sr_sched_queue_relation) + apply fastforce + apply fastforce + apply (meson ctcb_ptr_to_tcb_ptr_imageI) + apply (fastforce simp: tcb_null_sched_ptrs_def) + apply (simp add: typ_heap_simps c_guard_clift) + apply (fastforce simp: ready_or_release'_def) apply (simp add: guard_is_UNIV_def) apply simp apply (wp threadGet_wp) @@ -1175,9 +1251,10 @@ proof - apply simp apply (wp threadGet_wp) apply vcg - apply (fastforce simp: valid_objs'_def obj_at'_def ran_def typ_at'_def valid_obj'_def inQ_def - dest!: valid_queues_obj_at'D) - done + apply clarsimp + apply (frule ready_or_release'_disjoint_queues) + by (fastforce simp: valid_objs'_def obj_at'_def ran_def typ_at'_def valid_obj'_def inQ_def + dest!: valid_queues_obj_at'D) qed lemmas tcbSchedDequeue_update @@ -1185,47 +1262,6 @@ lemmas tcbSchedDequeue_update and tp'=tcbSchedPrev_C and tp_update=tcbSchedPrev_C_update, simplified] -lemma tcb_queue_relation_prev_next: - "\ tcb_queue_relation tn tp' mp queue qprev qhead; - tcbp \ set queue; distinct (ctcb_ptr_to_tcb_ptr qprev # queue); - \t \ set queue. tcb_at' t s; qprev \ tcb_Ptr 0 \ mp qprev \ None; - mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb \ - \ (tn tcb \ tcb_Ptr 0 \ tn tcb \ tcb_ptr_to_ctcb_ptr ` set queue - \ mp (tn tcb) \ None \ tn tcb \ tcb_ptr_to_ctcb_ptr tcbp) - \ (tp' tcb \ tcb_Ptr 0 \ (tp' tcb \ tcb_ptr_to_ctcb_ptr ` set queue - \ tp' tcb = qprev) - \ mp (tp' tcb) \ None \ tp' tcb \ tcb_ptr_to_ctcb_ptr tcbp) - \ (tn tcb \ tcb_Ptr 0 \ tn tcb \ tp' tcb)" - apply (induct queue arbitrary: qprev qhead) - apply simp - apply simp - apply (erule disjE) - apply clarsimp - apply (case_tac "queue") - apply clarsimp - apply clarsimp - apply (rule conjI) - apply clarsimp - apply clarsimp - apply (drule_tac f=ctcb_ptr_to_tcb_ptr in arg_cong[where y="tp' tcb"], simp) - apply clarsimp - apply fastforce - done - -lemma tcb_queue_relation_prev_next': - "\ tcb_queue_relation' tn tp' mp queue qhead qend; tcbp \ set queue; distinct queue; - \t \ set queue. tcb_at' t s; mp (tcb_ptr_to_ctcb_ptr tcbp) = Some tcb \ - \ (tn tcb \ tcb_Ptr 0 \ tn tcb \ tcb_ptr_to_ctcb_ptr ` set queue - \ mp (tn tcb) \ None \ tn tcb \ tcb_ptr_to_ctcb_ptr tcbp) - \ (tp' tcb \ tcb_Ptr 0 \ tp' tcb \ tcb_ptr_to_ctcb_ptr ` set queue - \ mp (tp' tcb) \ None \ tp' tcb \ tcb_ptr_to_ctcb_ptr tcbp) - \ (tn tcb \ tcb_Ptr 0 \ tn tcb \ tp' tcb)" - apply (clarsimp simp: tcb_queue_relation'_def split: if_split_asm) - apply (drule(1) tcb_queue_relation_prev_next, simp_all) - apply (fastforce dest: tcb_at_not_NULL) - apply clarsimp - done - (* L1 bitmap only updated if L2 entry bits end up all zero *) lemma rf_sr_drop_bitmaps_dequeue_helper_L2: "\ (\,\') \ rf_sr ; @@ -1344,7 +1380,7 @@ lemma tcbSchedDequeue_ccorres': "ccorres dc xfdc ((\s. \d p. (\t\set (ksReadyQueues s (d, p)). obj_at' (inQ d p) t s) \ distinct (ksReadyQueues s (d, p))) - and valid_queues' and tcb_at' t and valid_objs') + and valid_queues' and tcb_at' t and valid_objs' and ready_or_release') (UNIV \ \\tcb = tcb_ptr_to_ctcb_ptr t\) [] (tcbSchedDequeue t) @@ -1413,7 +1449,8 @@ proof - apply (rule_tac P="(\s. \d p. (\t\set (ksReadyQueues s (d, p)). obj_at' (inQ d p) t s) \ distinct (ksReadyQueues s (d, p))) and valid_queues' and obj_at' (inQ rva rvb) t - and (\s. rva \ maxDomain \ rvb \ maxPriority)" + and (\s. rva \ maxDomain \ rvb \ maxPriority) + and ready_or_release'" and P'=UNIV in ccorres_from_vcg) apply (rule allI, rule conseqPre, vcg) apply (clarsimp simp: getQueue_def gets_def get_def setQueue_def modify_def @@ -1519,8 +1556,9 @@ proof - maxDom_to_H maxPrio_to_H cong: if_cong split del: if_split)[1] - apply (fastforce simp: tcb_null_sched_ptrs_def typ_heap_simps c_guard_clift - elim: obj_at'_weaken)+ + apply (fastforce simp: tcb_null_sched_ptrs_def typ_heap_simps c_guard_clift + elim: obj_at'_weaken)+ + apply (fastforce simp: ready_or_release'_def) apply (erule_tac S="set (ksReadyQueues \ (tcbDomain ko, tcbPriority ko))" in state_relation_queue_update_helper', (simp | rule globals.equality)+, @@ -1529,8 +1567,9 @@ proof - maxDom_to_H maxPrio_to_H cong: if_cong split del: if_split, simp_all add: typ_heap_simps')[1] - subgoal by (fastforce simp: tcb_null_sched_ptrs_def) - subgoal by fastforce + subgoal by (fastforce simp: tcb_null_sched_ptrs_def) + subgoal by fastforce + apply (fastforce simp: ready_or_release'_def) apply clarsimp apply (rule conjI; clarsimp) apply (rule conjI) @@ -1549,10 +1588,11 @@ proof - cready_queues_index_to_C_def2 maxDom_to_H maxPrio_to_H cong: if_cong split del: if_split)[1] - apply (fold_subgoals (prefix))[4] + apply (fold_subgoals (prefix))[5] subgoal premises prems using prems by - (fastforce simp: typ_heap_simps c_guard_clift tcb_null_sched_ptrs_def - clift_heap_update_same[OF h_t_valid_clift])+ + clift_heap_update_same[OF h_t_valid_clift] + ready_or_release'_def)+ apply (rule conjI; clarsimp simp: queue_in_range[simplified maxDom_to_H maxPrio_to_H]) apply (frule (1) valid_queuesD') apply (drule (1) obj_at_cslift_tcb, clarsimp simp: inQ_def) @@ -1614,8 +1654,7 @@ proof - apply (clarsimp simp: h_val_field_clift' h_t_valid_clift[THEN h_t_valid_field] h_t_valid_clift) apply (simp add: invert_prioToL1Index_c_simp) - apply (frule_tac s=\ in tcb_queue_relation_prev_next') - apply (fastforce simp add: ksQ_tcb_at')+ + apply (frule_tac s=\ in tcb_queue_relation_prev_next'; (fastforce simp: ksQ_tcb_at')?) apply (drule_tac s=\ in tcbSchedDequeue_update, assumption, simp_all add: remove1_filter ksQ_tcb_at')[1] apply (clarsimp simp: filter_noteq_op upd_unless_null_def) @@ -1634,10 +1673,11 @@ proof - cready_queues_index_to_C_def2 maxDom_to_H maxPrio_to_H cong: if_cong split del: if_split)[1] - apply (fastforce simp: tcb_null_sched_ptrs_def) - apply (clarsimp simp: typ_heap_simps') - apply (fastforce simp: typ_heap_simps) - apply (fastforce simp: tcb_null_sched_ptrs_def) + apply (fastforce simp: tcb_null_sched_ptrs_def) + apply (clarsimp simp: typ_heap_simps') + apply (fastforce simp: typ_heap_simps) + apply (fastforce simp: tcb_null_sched_ptrs_def) + apply (fastforce simp: ready_or_release'_def) apply (erule_tac S="set (ksReadyQueues \ (tcbDomain ko, tcbPriority ko))" in state_relation_queue_update_helper', (simp | rule globals.equality)+, @@ -1645,10 +1685,11 @@ proof - cready_queues_index_to_C_def2 maxDom_to_H maxPrio_to_H cong: if_cong split del: if_split)[1] - apply (fold_subgoals (prefix))[4] + apply (fold_subgoals (prefix))[5] subgoal premises prems using prems by - (fastforce simp: typ_heap_simps c_guard_clift tcb_null_sched_ptrs_def - clift_heap_update_same[OF h_t_valid_clift])+ + clift_heap_update_same[OF h_t_valid_clift] + ready_or_release'_def)+ apply (clarsimp) apply (rule conjI; clarsimp simp: typ_heap_simps) apply (rule conjI) @@ -1669,9 +1710,10 @@ proof - cready_queues_index_to_C_def2 typ_heap_simps maxDom_to_H maxPrio_to_H cong: if_cong split del: if_split)[1] - apply (fold_subgoals (prefix))[3] + apply (fold_subgoals (prefix))[4] subgoal premises prems using prems - by (fastforce simp: typ_heap_simps c_guard_clift tcb_null_sched_ptrs_def)+ + by (fastforce simp: typ_heap_simps c_guard_clift tcb_null_sched_ptrs_def + ready_or_release'_def)+ apply (simp add: guard_is_UNIV_def) apply simp apply (wp threadGet_wp) @@ -1683,14 +1725,16 @@ proof - apply simp apply (wp threadGet_wp) apply vcg - by (fastforce simp: valid_objs'_def obj_at'_def ran_def projectKOs typ_at'_def + apply clarsimp + apply (frule ready_or_release'_disjoint_queues) + by (fastforce simp: valid_objs'_def obj_at'_def ran_def typ_at'_def valid_obj'_def valid_tcb'_def inQ_def) qed lemma tcbSchedDequeue_ccorres: "ccorres dc xfdc (valid_queues and valid_queues' and tcb_at' t and valid_objs' - and (\s. \d p. distinct (ksReadyQueues s (d, p)))) + and (\s. \d p. distinct (ksReadyQueues s (d, p))) and ready_or_release') (UNIV \ \\tcb = tcb_ptr_to_ctcb_ptr t\) [] (tcbSchedDequeue t) @@ -1754,7 +1798,8 @@ lemma tcb_queue_relation_qend_mems: lemma tcbSchedAppend_ccorres: "ccorres dc xfdc (valid_queues and tcb_at' t and valid_objs' - and (\s. \d p. distinct (ksReadyQueues s (d, p)))) + and (\s. \d p. distinct (ksReadyQueues s (d, p))) + and (\s. t \ set (ksReleaseQueue s)) and ready_or_release') (UNIV \ \\tcb = tcb_ptr_to_ctcb_ptr t\) [] (tcbSchedAppend t) @@ -1814,7 +1859,10 @@ proof - apply (rule_tac P="\s. valid_queues s \ (\p. t \ set (ksReadyQueues s p)) \ (\tcb. ko_at' tcb t s \ tcbDomain tcb =rva \ tcbPriority tcb = rvb \ valid_tcb' tcb s) - \ (\d p. distinct (ksReadyQueues s (d, p)))" + \ (\d p. distinct (ksReadyQueues s (d, p))) + \ t \ set (ksReleaseQueue s) + \ (\d p. set (ksReadyQueues s (d, p)) \ set (ksReleaseQueue s) = {}) + \ ready_or_release' s" and P'=UNIV in ccorres_from_vcg) apply (rule allI, rule conseqPre, vcg) apply (clarsimp simp: getQueue_def gets_def get_def setQueue_def modify_def @@ -1891,38 +1939,45 @@ proof - apply (clarsimp simp: cready_queues_index_to_C_def2 numPriorities_def) apply (frule(2) obj_at_cslift_tcb[OF valid_queues_obj_at'D]) apply (clarsimp simp: h_val_field_clift' h_t_valid_clift) - apply (erule_tac S="{t, v}" for v in state_relation_queue_update_helper, + apply (rule_tac S="set (t # ksReadyQueues \ (tcbDomain tcb, tcbPriority tcb))" + in state_relation_queue_update_helper, (simp | rule globals.equality)+, simp_all add: typ_heap_simps if_Some_helper numPriorities_def cready_queues_index_to_C_def2 upd_unless_null_def cong: if_cong split del: if_split del: fun_upd_restrict_conv)[1] - apply simp - apply (rule conjI) - apply clarsimp - apply (drule_tac s="tcb_ptr_to_ctcb_ptr t" in sym, simp) - apply (clarsimp simp add: fun_upd_twist) - prefer 4 - apply (simp add: obj_at'_weakenE[OF _ TrueI]) - apply (rule disjI1, erule valid_queues_obj_at'D) - subgoal by simp - subgoal by simp - subgoal by (fastforce simp: tcb_null_sched_ptrs_def) - apply (clarsimp simp: typ_heap_simps') + apply simp + apply (rule conjI) + apply clarsimp + apply (drule_tac s="tcb_ptr_to_ctcb_ptr t" in sym, simp) + apply (clarsimp simp add: fun_upd_twist) + prefer 4 + apply (simp add: obj_at'_weakenE[OF _ TrueI]) + apply (fastforce intro!: valid_queues_obj_at'D) + apply (rule ext) + apply (clarsimp split: if_splits simp: typ_heap_simps) + apply (frule rf_sr_sched_queue_relation) + apply fastforce + apply fastforce + apply (meson ctcb_ptr_to_tcb_ptr_imageI) + subgoal by (fastforce simp: tcb_null_sched_ptrs_def) + apply (clarsimp simp: typ_heap_simps') + apply fast apply (simp add: guard_is_UNIV_def) apply simp apply (wp threadGet_wp) apply vcg apply simp - apply (wp threadGet_wp) - apply vcg - apply (rule ccorres_return_Skip) - apply simp - apply (wp threadGet_wp) - apply vcg - by (fastforce simp: valid_objs'_def obj_at'_def ran_def projectKOs typ_at'_def - valid_obj'_def inQ_def - dest!: valid_queues_obj_at'D) + apply (wp threadGet_wp) + apply vcg + apply (rule ccorres_return_Skip) + apply simp + apply (wp threadGet_wp) + apply vcg + apply clarsimp + apply (frule ready_or_release'_disjoint_queues) + by (fastforce simp: valid_objs'_def obj_at'_def ran_def typ_at'_def valid_obj'_def inQ_def + dest!: valid_queues_obj_at'D) qed lemma isStopped_spec: @@ -2904,23 +2959,28 @@ lemma cancelIPC_ccorres_helper: apply (elim conjE) apply (intro conjI) \ \tcb relation\ - apply (erule ctcb_relation_null_queue_ptrs) - subgoal by (clarsimp simp: comp_def) - \ \ep relation\ - apply (rule cpspace_relation_ep_update_ep, assumption+) - subgoal by (simp add: cendpoint_relation_def Let_def EPState_Idle_def) - subgoal by simp - \ \ntfn relation\ - apply (erule iffD1 [OF cmap_relation_cong, OF refl refl, rotated -1]) - apply simp - apply (rule cnotification_relation_ep_queue, assumption+) - subgoal by simp - apply (erule (1) map_to_ko_atI') - subgoal sorry (* FIXME RT: refill_buffer_relation *) - apply (simp add: heap_to_user_data_def Let_def) - \ \queue relation\ - apply (rule cready_queues_relation_null_queue_ptrs, assumption+) - subgoal by (clarsimp simp: comp_def) + apply (erule ctcb_relation_null_queue_ptrs) + subgoal by (clarsimp simp: comp_def) + \ \ep relation\ + apply (rule cpspace_relation_ep_update_ep, assumption+) + subgoal by (simp add: cendpoint_relation_def Let_def EPState_Idle_def) + subgoal by simp + \ \ntfn relation\ + apply (erule iffD1 [OF cmap_relation_cong, OF refl refl, rotated -1]) + apply simp + apply (rule cnotification_relation_ep_queue, assumption+) + subgoal by simp + apply (erule (1) map_to_ko_atI') + subgoal sorry (* FIXME RT: refill_buffer_relation *) + apply (simp add: heap_to_user_data_def Let_def) + \ \queue relations\ + apply (rule cready_queues_relation_null_queue_ptrs, assumption+) + subgoal by (clarsimp simp: comp_def) + apply (erule iffD2[OF tcb_queue_relation_only_next_prev, rotated -1]) + apply (rule null_ep_schedD[THEN conjunct1]) + apply (clarsimp simp: comp_def) + apply (rule null_ep_schedD[THEN conjunct2]) + apply (clarsimp simp: comp_def) subgoal by (clarsimp simp: carch_state_relation_def carch_globals_def packed_heap_update_collapse_hrs) subgoal by (simp add: cmachine_state_relation_def) @@ -2942,44 +3002,49 @@ lemma cancelIPC_ccorres_helper: apply (elim conjE) apply (intro conjI) \ \tcb relation\ - apply (erule ctcb_relation_null_queue_ptrs) - subgoal by (clarsimp simp: comp_def) - \ \ep relation\ - apply (rule cpspace_relation_ep_update_ep, assumption+) - apply (simp add: cendpoint_relation_def Let_def isSendEP_def isRecvEP_def split: endpoint.splits split del: if_split) - \ \recv case\ - apply (subgoal_tac "pspace_canonical' \") - prefer 2 - apply fastforce - apply (clarsimp - simp: h_t_valid_clift_Some_iff ctcb_offset_defs - tcb_queue_relation'_next_mask tcb_queue_relation'_prev_mask - tcb_queue_relation'_next_sign tcb_queue_relation'_prev_sign - simp flip: canonical_bit_def - cong: tcb_queue_relation'_cong) - subgoal by (intro impI conjI; simp) - \ \send case\ - apply (subgoal_tac "pspace_canonical' \") - prefer 2 - apply fastforce - apply (clarsimp - simp: h_t_valid_clift_Some_iff ctcb_offset_defs - tcb_queue_relation'_next_mask tcb_queue_relation'_prev_mask - tcb_queue_relation'_next_sign tcb_queue_relation'_prev_sign - simp flip: canonical_bit_def - cong: tcb_queue_relation'_cong) - subgoal by (intro impI conjI; simp) - subgoal by simp - \ \ntfn relation\ - apply (erule iffD1 [OF cmap_relation_cong, OF refl refl, rotated -1]) - apply simp - apply (rule cnotification_relation_ep_queue, assumption+) - apply simp - apply (erule (1) map_to_ko_atI') - subgoal sorry (* FIXME RT: refill_buffer_relation *) - \ \queue relation\ - apply (rule cready_queues_relation_null_queue_ptrs, assumption+) - subgoal by (clarsimp simp: comp_def) + apply (erule ctcb_relation_null_queue_ptrs) + subgoal by (clarsimp simp: comp_def) + \ \ep relation\ + apply (rule cpspace_relation_ep_update_ep, assumption+) + apply (simp add: cendpoint_relation_def Let_def isSendEP_def isRecvEP_def split: endpoint.splits split del: if_split) + \ \recv case\ + apply (subgoal_tac "pspace_canonical' \") + prefer 2 + apply fastforce + apply (clarsimp + simp: h_t_valid_clift_Some_iff ctcb_offset_defs + tcb_queue_relation'_next_mask tcb_queue_relation'_prev_mask + tcb_queue_relation'_next_sign tcb_queue_relation'_prev_sign + simp flip: canonical_bit_def + cong: tcb_queue_relation'_cong) + subgoal by (intro impI conjI; simp) + \ \send case\ + apply (subgoal_tac "pspace_canonical' \") + prefer 2 + apply fastforce + apply (clarsimp + simp: h_t_valid_clift_Some_iff ctcb_offset_defs + tcb_queue_relation'_next_mask tcb_queue_relation'_prev_mask + tcb_queue_relation'_next_sign tcb_queue_relation'_prev_sign + simp flip: canonical_bit_def + cong: tcb_queue_relation'_cong) + subgoal by (intro impI conjI; simp) + subgoal by simp + \ \ntfn relation\ + apply (erule iffD1 [OF cmap_relation_cong, OF refl refl, rotated -1]) + apply simp + apply (rule cnotification_relation_ep_queue, assumption+) + apply simp + apply (erule (1) map_to_ko_atI') + subgoal sorry (* FIXME RT: refill_buffer_relation *) + \ \queue relations\ + apply (rule cready_queues_relation_null_queue_ptrs, assumption+) + subgoal by (clarsimp simp: comp_def) + apply (erule iffD2[OF tcb_queue_relation_only_next_prev, rotated -1]) + apply (rule null_ep_schedD[THEN conjunct1]) + apply (clarsimp simp: comp_def) + apply (rule null_ep_schedD[THEN conjunct2]) + apply (clarsimp simp: comp_def) subgoal by (clarsimp simp: carch_state_relation_def carch_globals_def packed_heap_update_collapse_hrs) subgoal by (simp add: cmachine_state_relation_def) diff --git a/proof/crefine/RISCV64/Ipc_C.thy b/proof/crefine/RISCV64/Ipc_C.thy index d16f2eb4bc..cec0322540 100644 --- a/proof/crefine/RISCV64/Ipc_C.thy +++ b/proof/crefine/RISCV64/Ipc_C.thy @@ -4534,23 +4534,28 @@ lemma sendIPC_dequeue_ccorres_helper: typ_heap_simps') apply (elim conjE) apply (intro conjI) - \ \tcb relation\ - apply (erule ctcb_relation_null_queue_ptrs) - apply (clarsimp simp: comp_def) - \ \ep relation\ - apply (rule cpspace_relation_ep_update_ep, assumption+) - apply (simp add: cendpoint_relation_def Let_def EPState_Idle_def - tcb_queue_relation'_def) - apply simp - \ \ntfn relation\ - apply (erule iffD1 [OF cmap_relation_cong, OF refl refl, rotated -1]) - apply simp - apply (rule cnotification_relation_ep_queue, assumption+) - apply simp - apply (erule (1) map_to_ko_atI') - subgoal sorry (* FIXME RT: refill_buffer_relation *) - \ \queue relation\ - apply (rule cready_queues_relation_null_queue_ptrs, assumption+) + \ \tcb relation\ + apply (erule ctcb_relation_null_queue_ptrs) + apply (clarsimp simp: comp_def) + \ \ep relation\ + apply (rule cpspace_relation_ep_update_ep, assumption+) + apply (simp add: cendpoint_relation_def Let_def EPState_Idle_def + tcb_queue_relation'_def) + apply simp + \ \ntfn relation\ + apply (erule iffD1 [OF cmap_relation_cong, OF refl refl, rotated -1]) + apply simp + apply (rule cnotification_relation_ep_queue, assumption+) + apply simp + apply (erule (1) map_to_ko_atI') + subgoal sorry (* FIXME RT: refill_buffer_relation *) + \ \queue relations\ + apply (rule cready_queues_relation_null_queue_ptrs, assumption+) + apply (clarsimp simp: comp_def) + apply (erule iffD2[OF tcb_queue_relation_only_next_prev, rotated -1]) + apply (rule null_ep_schedD[THEN conjunct1]) + apply (clarsimp simp: comp_def) + apply (rule null_ep_schedD[THEN conjunct2]) apply (clarsimp simp: comp_def) apply (clarsimp simp: carch_state_relation_def packed_heap_update_collapse_hrs) apply (simp add: cmachine_state_relation_def) @@ -4575,31 +4580,36 @@ lemma sendIPC_dequeue_ccorres_helper: typ_heap_simps') apply (elim conjE) apply (intro conjI) - \ \tcb relation\ - apply (erule ctcb_relation_null_queue_ptrs) - apply (clarsimp simp: comp_def) - \ \ep relation\ - apply (rule cpspace_relation_ep_update_ep, assumption+) - apply (clarsimp simp: cendpoint_relation_def Let_def - isRecvEP_def isSendEP_def - tcb_queue_relation'_def valid_ep'_def - simp flip: canonical_bit_def - split: endpoint.splits list.splits - split del: if_split) - apply (subgoal_tac "tcb_at' (if x22 = [] then x21 else last x22) \") - apply (erule (1) tcb_and_not_mask_canonical[OF invs_pspace_canonical']) - apply (simp add: objBits_simps') - apply (clarsimp split: if_split) - apply simp - \ \ntfn relation\ - apply (erule iffD1 [OF cmap_relation_cong, OF refl refl, rotated -1]) - apply simp - apply (rule cnotification_relation_ep_queue, assumption+) - apply simp - apply (erule (1) map_to_ko_atI') - subgoal sorry (* FIXME RT: refill_buffer_relation *) - \ \queue relation\ - apply (rule cready_queues_relation_null_queue_ptrs, assumption+) + \ \tcb relation\ + apply (erule ctcb_relation_null_queue_ptrs) + apply (clarsimp simp: comp_def) + \ \ep relation\ + apply (rule cpspace_relation_ep_update_ep, assumption+) + apply (clarsimp simp: cendpoint_relation_def Let_def + isRecvEP_def isSendEP_def + tcb_queue_relation'_def valid_ep'_def + simp flip: canonical_bit_def + split: endpoint.splits list.splits + split del: if_split) + apply (subgoal_tac "tcb_at' (if x22 = [] then x21 else last x22) \") + apply (erule (1) tcb_and_not_mask_canonical[OF invs_pspace_canonical']) + apply (simp add: objBits_simps') + apply (clarsimp split: if_split) + apply simp + \ \ntfn relation\ + apply (erule iffD1 [OF cmap_relation_cong, OF refl refl, rotated -1]) + apply simp + apply (rule cnotification_relation_ep_queue, assumption+) + apply simp + apply (erule (1) map_to_ko_atI') + subgoal sorry (* FIXME RT: refill_buffer_relation *) + \ \queue relations\ + apply (rule cready_queues_relation_null_queue_ptrs, assumption+) + apply (clarsimp simp: comp_def) + apply (erule iffD2[OF tcb_queue_relation_only_next_prev, rotated -1]) + apply (rule null_ep_schedD[THEN conjunct1]) + apply (clarsimp simp: comp_def) + apply (rule null_ep_schedD[THEN conjunct2]) apply (clarsimp simp: comp_def) apply (clarsimp simp: carch_state_relation_def packed_heap_update_collapse_hrs) apply (simp add: cmachine_state_relation_def) @@ -4915,34 +4925,39 @@ lemma sendIPC_enqueue_ccorres_helper: apply (elim conjE) apply (intro conjI) \ \tcb relation\ - apply (erule ctcb_relation_null_queue_ptrs) - apply (clarsimp simp: comp_def) - \ \ep relation\ - apply (rule cpspace_relation_ep_update_ep', assumption+) - apply (clarsimp simp: cendpoint_relation_def Let_def - mask_def [where n=3] EPState_Send_def) - apply (clarsimp simp: tcb_queue_relation'_def is_aligned_neg_mask) - apply (rule conjI, simp add: mask_def) - subgoal - apply (clarsimp simp: valid_pspace'_def objBits_simps' simp flip: canonical_bit_def) - apply (erule (1) tcb_and_not_mask_canonical) - by (simp (no_asm) add: tcbBlockSizeBits_def) - apply (simp add: isSendEP_def isRecvEP_def) - \ \ntfn relation\ - apply (erule iffD1 [OF cmap_relation_cong, OF refl refl, rotated -1]) - apply simp - apply (rule cnotification_relation_ep_queue, assumption+) - apply (simp add: isSendEP_def isRecvEP_def) - apply simp - apply (frule_tac x=p in map_to_ko_atI, clarsimp, clarsimp) - apply fastforce - apply (erule(2) map_to_ko_at_updI') - apply (simp only:projectKOs injectKO_ep objBits_simps) - apply clarsimp - apply (clarsimp simp: obj_at'_def projectKOs) - subgoal sorry (* FIXME RT: refill_buffer_relation *) - \ \queue relation\ - apply (rule cready_queues_relation_null_queue_ptrs, assumption+) + apply (erule ctcb_relation_null_queue_ptrs) + apply (clarsimp simp: comp_def) + \ \ep relation\ + apply (rule cpspace_relation_ep_update_ep', assumption+) + apply (clarsimp simp: cendpoint_relation_def Let_def + mask_def [where n=3] EPState_Send_def) + apply (clarsimp simp: tcb_queue_relation'_def is_aligned_neg_mask) + apply (rule conjI, simp add: mask_def) + subgoal + apply (clarsimp simp: valid_pspace'_def objBits_simps' simp flip: canonical_bit_def) + apply (erule (1) tcb_and_not_mask_canonical) + by (simp (no_asm) add: tcbBlockSizeBits_def) + apply (simp add: isSendEP_def isRecvEP_def) + \ \ntfn relation\ + apply (erule iffD1 [OF cmap_relation_cong, OF refl refl, rotated -1]) + apply simp + apply (rule cnotification_relation_ep_queue, assumption+) + apply (simp add: isSendEP_def isRecvEP_def) + apply simp + apply (frule_tac x=p in map_to_ko_atI, clarsimp, clarsimp) + apply fastforce + apply (erule(2) map_to_ko_at_updI') + apply (simp only:projectKOs injectKO_ep objBits_simps) + apply clarsimp + apply (clarsimp simp: obj_at'_def projectKOs) + subgoal sorry (* FIXME RT: refill_buffer_relation *) + \ \queue relations\ + apply (rule cready_queues_relation_null_queue_ptrs, assumption+) + apply (clarsimp simp: comp_def) + apply (erule iffD2[OF tcb_queue_relation_only_next_prev, rotated -1]) + apply (rule null_ep_schedD[THEN conjunct1]) + apply (clarsimp simp: comp_def) + apply (rule null_ep_schedD[THEN conjunct2]) apply (clarsimp simp: comp_def) apply (clarsimp simp: carch_state_relation_def packed_heap_update_collapse_hrs) apply (simp add: cmachine_state_relation_def) @@ -4960,43 +4975,48 @@ lemma sendIPC_enqueue_ccorres_helper: typ_heap_simps') apply (elim conjE) apply (intro conjI) - \ \tcb relation\ - apply (erule ctcb_relation_null_queue_ptrs) - apply (clarsimp simp: comp_def) - \ \ep relation\ - apply (rule cpspace_relation_ep_update_ep', assumption+) - apply (clarsimp simp: cendpoint_relation_def Let_def - mask_def [where n=3] EPState_Send_def - split: if_split) - subgoal - apply (clarsimp simp: tcb_queue_relation'_def is_aligned_neg_mask - valid_ep'_def - dest: tcb_queue_relation_next_not_NULL) - apply (rule conjI, clarsimp) - apply (rule conjI, fastforce simp: mask_def) - apply (clarsimp simp: valid_pspace'_def objBits_simps' simp flip: canonical_bit_def) - apply (erule (1) tcb_and_not_mask_canonical) - apply (simp (no_asm) add: tcbBlockSizeBits_def) - apply (clarsimp simp: valid_pspace'_def objBits_simps' simp flip: canonical_bit_def) - apply (rule conjI, solves \simp (no_asm) add: mask_def\) - apply (erule (1) tcb_and_not_mask_canonical) - apply (simp (no_asm) add: tcbBlockSizeBits_def) - done - apply (simp add: isSendEP_def isRecvEP_def) - \ \ntfn relation\ - apply (erule iffD1 [OF cmap_relation_cong, OF refl refl, rotated -1]) - apply simp - apply (rule cnotification_relation_ep_queue, assumption+) - apply (simp add: isSendEP_def isRecvEP_def) - apply simp - apply (frule_tac x=p in map_to_ko_atI, clarsimp, clarsimp) - apply fastforce - apply (erule(2) map_to_ko_at_updI') - apply (clarsimp simp: objBitsKO_def) - apply (clarsimp simp: obj_at'_def) - subgoal sorry (* FIXME RT: refill_buffer_relation *) - \ \queue relation\ - apply (rule cready_queues_relation_null_queue_ptrs, assumption+) + \ \tcb relation\ + apply (erule ctcb_relation_null_queue_ptrs) + apply (clarsimp simp: comp_def) + \ \ep relation\ + apply (rule cpspace_relation_ep_update_ep', assumption+) + apply (clarsimp simp: cendpoint_relation_def Let_def + mask_def [where n=3] EPState_Send_def + split: if_split) + subgoal + apply (clarsimp simp: tcb_queue_relation'_def is_aligned_neg_mask + valid_ep'_def + dest: tcb_queue_relation_next_not_NULL) + apply (rule conjI, clarsimp) + apply (rule conjI, fastforce simp: mask_def) + apply (clarsimp simp: valid_pspace'_def objBits_simps' simp flip: canonical_bit_def) + apply (erule (1) tcb_and_not_mask_canonical) + apply (simp (no_asm) add: tcbBlockSizeBits_def) + apply (clarsimp simp: valid_pspace'_def objBits_simps' simp flip: canonical_bit_def) + apply (rule conjI, solves \simp (no_asm) add: mask_def\) + apply (erule (1) tcb_and_not_mask_canonical) + apply (simp (no_asm) add: tcbBlockSizeBits_def) + done + apply (simp add: isSendEP_def isRecvEP_def) + \ \ntfn relation\ + apply (erule iffD1 [OF cmap_relation_cong, OF refl refl, rotated -1]) + apply simp + apply (rule cnotification_relation_ep_queue, assumption+) + apply (simp add: isSendEP_def isRecvEP_def) + apply simp + apply (frule_tac x=p in map_to_ko_atI, clarsimp, clarsimp) + apply fastforce + apply (erule(2) map_to_ko_at_updI') + apply (clarsimp simp: objBitsKO_def) + apply (clarsimp simp: obj_at'_def) + subgoal sorry (* FIXME RT: refill_buffer_relation *) + \ \queue relations\ + apply (rule cready_queues_relation_null_queue_ptrs, assumption+) + apply (clarsimp simp: comp_def) + apply (erule iffD2[OF tcb_queue_relation_only_next_prev, rotated -1]) + apply (rule null_ep_schedD[THEN conjunct1]) + apply (clarsimp simp: comp_def) + apply (rule null_ep_schedD[THEN conjunct2]) apply (clarsimp simp: comp_def) apply (clarsimp simp: carch_state_relation_def packed_heap_update_collapse_hrs) apply (simp add: cmachine_state_relation_def) @@ -5403,8 +5423,13 @@ lemma receiveIPC_enqueue_ccorres_helper: apply (clarsimp simp: objBitsKO_def) apply (clarsimp simp: obj_at'_def) subgoal sorry (* FIXME RT: refill_buffer_relation *) - \ \queue relation\ - apply (rule cready_queues_relation_null_queue_ptrs, assumption+) + \ \queue relations\ + apply (rule cready_queues_relation_null_queue_ptrs, assumption+) + apply (clarsimp simp: comp_def) + apply (erule iffD2[OF tcb_queue_relation_only_next_prev, rotated -1]) + apply (rule null_ep_schedD[THEN conjunct1]) + apply (clarsimp simp: comp_def) + apply (rule null_ep_schedD[THEN conjunct2]) apply (clarsimp simp: comp_def) apply (clarsimp simp: carch_state_relation_def packed_heap_update_collapse_hrs) apply (simp add: cmachine_state_relation_def) @@ -5422,35 +5447,40 @@ lemma receiveIPC_enqueue_ccorres_helper: typ_heap_simps') apply (elim conjE) apply (intro conjI) - \ \tcb relation\ - apply (erule ctcb_relation_null_queue_ptrs) - apply (clarsimp simp: comp_def) - \ \ep relation\ - apply (rule cpspace_relation_ep_update_ep', assumption+) - apply (clarsimp simp: cendpoint_relation_def Let_def - mask_def [where n=3] EPState_Recv_def) - apply (clarsimp simp: tcb_queue_relation'_def is_aligned_neg_mask - simp flip: canonical_bit_def) - subgoal - apply (rule conjI, solves\simp (no_asm) add: mask_def\) - apply (clarsimp simp: valid_pspace'_def) - apply (erule (1) tcb_and_not_mask_canonical, simp (no_asm) add: tcbBlockSizeBits_def) - done - apply (simp add: isSendEP_def isRecvEP_def) - \ \ntfn relation\ - apply (erule iffD1 [OF cmap_relation_cong, OF refl refl, rotated -1]) - apply simp - apply (rule cnotification_relation_ep_queue, assumption+) - apply (simp add: isSendEP_def isRecvEP_def) - apply simp - apply (frule_tac x=p in map_to_ko_atI, clarsimp, clarsimp) - apply fastforce - apply (erule(2) map_to_ko_at_updI') - apply (clarsimp simp: objBitsKO_def) - apply (clarsimp simp: obj_at'_def) - subgoal sorry (* FIXME RT: refill_buffer_relation *) - \ \queue relation\ - apply (rule cready_queues_relation_null_queue_ptrs, assumption+) + \ \tcb relation\ + apply (erule ctcb_relation_null_queue_ptrs) + apply (clarsimp simp: comp_def) + \ \ep relation\ + apply (rule cpspace_relation_ep_update_ep', assumption+) + apply (clarsimp simp: cendpoint_relation_def Let_def + mask_def [where n=3] EPState_Recv_def) + apply (clarsimp simp: tcb_queue_relation'_def is_aligned_neg_mask + simp flip: canonical_bit_def) + subgoal + apply (rule conjI, solves\simp (no_asm) add: mask_def\) + apply (clarsimp simp: valid_pspace'_def) + apply (erule (1) tcb_and_not_mask_canonical, simp (no_asm) add: tcbBlockSizeBits_def) + done + apply (simp add: isSendEP_def isRecvEP_def) + \ \ntfn relation\ + apply (erule iffD1 [OF cmap_relation_cong, OF refl refl, rotated -1]) + apply simp + apply (rule cnotification_relation_ep_queue, assumption+) + apply (simp add: isSendEP_def isRecvEP_def) + apply simp + apply (frule_tac x=p in map_to_ko_atI, clarsimp, clarsimp) + apply fastforce + apply (erule(2) map_to_ko_at_updI') + apply (clarsimp simp: objBitsKO_def) + apply (clarsimp simp: obj_at'_def) + subgoal sorry (* FIXME RT: refill_buffer_relation *) + \ \queue relations\ + apply (rule cready_queues_relation_null_queue_ptrs, assumption+) + apply (clarsimp simp: comp_def) + apply (erule iffD2[OF tcb_queue_relation_only_next_prev, rotated -1]) + apply (rule null_ep_schedD[THEN conjunct1]) + apply (clarsimp simp: comp_def) + apply (rule null_ep_schedD[THEN conjunct2]) apply (clarsimp simp: comp_def) apply (clarsimp simp: carch_state_relation_def packed_heap_update_collapse_hrs) apply (simp add: cmachine_state_relation_def) @@ -5521,23 +5551,28 @@ lemma receiveIPC_dequeue_ccorres_helper: typ_heap_simps') apply (elim conjE) apply (intro conjI) - \ \tcb relation\ - apply (erule ctcb_relation_null_queue_ptrs) - apply (clarsimp simp: comp_def) - \ \ep relation\ - apply (rule cpspace_relation_ep_update_ep, assumption+) - apply (simp add: cendpoint_relation_def Let_def EPState_Idle_def - tcb_queue_relation'_def) - apply simp - \ \ntfn relation\ - apply (erule iffD1 [OF cmap_relation_cong, OF refl refl, rotated -1]) - apply simp - apply (rule cnotification_relation_ep_queue, assumption+) - apply simp - apply (erule (1) map_to_ko_atI') - subgoal sorry (* FIXME RT: refill_buffer_relation *) - \ \queue relation\ - apply (rule cready_queues_relation_null_queue_ptrs, assumption+) + \ \tcb relation\ + apply (erule ctcb_relation_null_queue_ptrs) + apply (clarsimp simp: comp_def) + \ \ep relation\ + apply (rule cpspace_relation_ep_update_ep, assumption+) + apply (simp add: cendpoint_relation_def Let_def EPState_Idle_def + tcb_queue_relation'_def) + apply simp + \ \ntfn relation\ + apply (erule iffD1 [OF cmap_relation_cong, OF refl refl, rotated -1]) + apply simp + apply (rule cnotification_relation_ep_queue, assumption+) + apply simp + apply (erule (1) map_to_ko_atI') + subgoal sorry (* FIXME RT: refill_buffer_relation *) + \ \queue relations\ + apply (rule cready_queues_relation_null_queue_ptrs, assumption+) + apply (clarsimp simp: comp_def) + apply (erule iffD2[OF tcb_queue_relation_only_next_prev, rotated -1]) + apply (rule null_ep_schedD[THEN conjunct1]) + apply (clarsimp simp: comp_def) + apply (rule null_ep_schedD[THEN conjunct2]) apply (clarsimp simp: comp_def) apply (clarsimp simp: carch_state_relation_def packed_heap_update_collapse_hrs) apply (simp add: cmachine_state_relation_def) @@ -5562,31 +5597,36 @@ lemma receiveIPC_dequeue_ccorres_helper: typ_heap_simps') apply (elim conjE) apply (intro conjI) - \ \tcb relation\ - apply (erule ctcb_relation_null_queue_ptrs) - apply (clarsimp simp: comp_def) - \ \ep relation\ - apply (rule cpspace_relation_ep_update_ep, assumption+) - apply (clarsimp simp: cendpoint_relation_def Let_def - isRecvEP_def isSendEP_def - tcb_queue_relation'_def valid_ep'_def - simp flip: canonical_bit_def - split: endpoint.splits list.splits - split del: if_split) - apply (subgoal_tac "tcb_at' (if x22 = [] then x21 else last x22) \") - apply (erule (1) tcb_and_not_mask_canonical[OF invs_pspace_canonical']) - apply (clarsimp simp: objBits_simps') - apply (clarsimp split: if_split) - apply simp - \ \ntfn relation\ - apply (erule iffD1 [OF cmap_relation_cong, OF refl refl, rotated -1]) - apply simp - apply (rule cnotification_relation_ep_queue, assumption+) - apply simp - apply (erule (1) map_to_ko_atI') - subgoal sorry (* FIXME RT: refill_buffer_relation *) - \ \queue relation\ - apply (rule cready_queues_relation_null_queue_ptrs, assumption+) + \ \tcb relation\ + apply (erule ctcb_relation_null_queue_ptrs) + apply (clarsimp simp: comp_def) + \ \ep relation\ + apply (rule cpspace_relation_ep_update_ep, assumption+) + apply (clarsimp simp: cendpoint_relation_def Let_def + isRecvEP_def isSendEP_def + tcb_queue_relation'_def valid_ep'_def + simp flip: canonical_bit_def + split: endpoint.splits list.splits + split del: if_split) + apply (subgoal_tac "tcb_at' (if x22 = [] then x21 else last x22) \") + apply (erule (1) tcb_and_not_mask_canonical[OF invs_pspace_canonical']) + apply (clarsimp simp: objBits_simps') + apply (clarsimp split: if_split) + apply simp + \ \ntfn relation\ + apply (erule iffD1 [OF cmap_relation_cong, OF refl refl, rotated -1]) + apply simp + apply (rule cnotification_relation_ep_queue, assumption+) + apply simp + apply (erule (1) map_to_ko_atI') + subgoal sorry (* FIXME RT: refill_buffer_relation *) + \ \queue relations\ + apply (rule cready_queues_relation_null_queue_ptrs, assumption+) + apply (clarsimp simp: comp_def) + apply (erule iffD2[OF tcb_queue_relation_only_next_prev, rotated -1]) + apply (rule null_ep_schedD[THEN conjunct1]) + apply (clarsimp simp: comp_def) + apply (rule null_ep_schedD[THEN conjunct2]) apply (clarsimp simp: comp_def) apply (clarsimp simp: carch_state_relation_def packed_heap_update_collapse_hrs) apply (simp add: cmachine_state_relation_def) @@ -6095,23 +6135,28 @@ lemma sendSignal_dequeue_ccorres_helper: typ_heap_simps') apply (elim conjE) apply (intro conjI) - \ \tcb relation\ - apply (erule ctcb_relation_null_queue_ptrs) - apply (clarsimp simp: comp_def) - \ \ep relation\ - apply (erule iffD1 [OF cmap_relation_cong, OF refl refl, rotated -1]) - apply simp - apply (rule cendpoint_relation_ntfn_queue, assumption+) - apply simp+ - apply (erule (1) map_to_ko_atI') - \ \ntfn relation\ - apply (rule cpspace_relation_ntfn_update_ntfn, assumption+) - apply (simp add: cnotification_relation_def Let_def NtfnState_Idle_def - tcb_queue_relation'_def) - apply simp - subgoal sorry (* FIXME RT: refill_buffer_relation *) - \ \queue relation\ - apply (rule cready_queues_relation_null_queue_ptrs, assumption+) + \ \tcb relation\ + apply (erule ctcb_relation_null_queue_ptrs) + apply (clarsimp simp: comp_def) + \ \ep relation\ + apply (erule iffD1 [OF cmap_relation_cong, OF refl refl, rotated -1]) + apply simp + apply (rule cendpoint_relation_ntfn_queue, assumption+) + apply simp+ + apply (erule (1) map_to_ko_atI') + \ \ntfn relation\ + apply (rule cpspace_relation_ntfn_update_ntfn, assumption+) + apply (simp add: cnotification_relation_def Let_def NtfnState_Idle_def + tcb_queue_relation'_def) + apply simp + subgoal sorry (* FIXME RT: refill_buffer_relation *) + \ \queue relations\ + apply (rule cready_queues_relation_null_queue_ptrs, assumption+) + apply (clarsimp simp: comp_def) + apply (erule iffD2[OF tcb_queue_relation_only_next_prev, rotated -1]) + apply (rule null_ep_schedD[THEN conjunct1]) + apply (clarsimp simp: comp_def) + apply (rule null_ep_schedD[THEN conjunct2]) apply (clarsimp simp: comp_def) apply (clarsimp simp: carch_state_relation_def packed_heap_update_collapse_hrs) apply (simp add: cmachine_state_relation_def) @@ -6138,33 +6183,38 @@ lemma sendSignal_dequeue_ccorres_helper: typ_heap_simps') apply (elim conjE) apply (intro conjI) - \ \tcb relation\ - apply (erule ctcb_relation_null_queue_ptrs) - apply (clarsimp simp: comp_def) - \ \ep relation\ - apply (erule iffD1 [OF cmap_relation_cong, OF refl refl, rotated -1]) - apply simp - apply (rule cendpoint_relation_ntfn_queue, assumption+) - apply simp+ - apply (erule (1) map_to_ko_atI') - \ \ntfn relation\ - apply (rule cpspace_relation_ntfn_update_ntfn, assumption+) - apply (clarsimp simp: cnotification_relation_def Let_def - isWaitingNtfn_def - tcb_queue_relation'_def valid_ntfn'_def - split: Structures_H.notification.splits list.splits - split del: if_split) - apply (subgoal_tac "tcb_at' (if x22 = [] then x21 else last x22) \") - apply (rule conjI) - subgoal by (erule (1) tcb_ptr_sign_extend_canonical[OF invs_pspace_canonical']) - apply (rule context_conjI) - subgoal by (erule (1) tcb_ptr_sign_extend_canonical[OF invs_pspace_canonical']) - apply clarsimp - apply (clarsimp split: if_split) - apply simp - subgoal sorry (* FIXME RT: refill_buffer_relation *) - \ \queue relation\ - apply (rule cready_queues_relation_null_queue_ptrs, assumption+) + \ \tcb relation\ + apply (erule ctcb_relation_null_queue_ptrs) + apply (clarsimp simp: comp_def) + \ \ep relation\ + apply (erule iffD1 [OF cmap_relation_cong, OF refl refl, rotated -1]) + apply simp + apply (rule cendpoint_relation_ntfn_queue, assumption+) + apply simp+ + apply (erule (1) map_to_ko_atI') + \ \ntfn relation\ + apply (rule cpspace_relation_ntfn_update_ntfn, assumption+) + apply (clarsimp simp: cnotification_relation_def Let_def + isWaitingNtfn_def + tcb_queue_relation'_def valid_ntfn'_def + split: Structures_H.notification.splits list.splits + split del: if_split) + apply (subgoal_tac "tcb_at' (if x22 = [] then x21 else last x22) \") + apply (rule conjI) + subgoal by (erule (1) tcb_ptr_sign_extend_canonical[OF invs_pspace_canonical']) + apply (rule context_conjI) + subgoal by (erule (1) tcb_ptr_sign_extend_canonical[OF invs_pspace_canonical']) + apply clarsimp + apply (clarsimp split: if_split) + apply simp + subgoal sorry (* FIXME RT: refill_buffer_relation *) + \ \queue relations\ + apply (rule cready_queues_relation_null_queue_ptrs, assumption+) + apply (clarsimp simp: comp_def) + apply (erule iffD2[OF tcb_queue_relation_only_next_prev, rotated -1]) + apply (rule null_ep_schedD[THEN conjunct1]) + apply (clarsimp simp: comp_def) + apply (rule null_ep_schedD[THEN conjunct2]) apply (clarsimp simp: comp_def) apply (clarsimp simp: carch_state_relation_def) apply (simp add: cmachine_state_relation_def) @@ -6529,39 +6579,44 @@ lemma receiveSignal_enqueue_ccorres_helper: typ_heap_simps') apply (elim conjE) apply (intro conjI) - \ \tcb relation\ - apply (erule ctcb_relation_null_queue_ptrs) - apply (clarsimp simp: comp_def) - \ \ep relation\ - apply (erule iffD1 [OF cmap_relation_cong, OF refl refl, rotated -1]) - apply simp - apply (rule cendpoint_relation_ntfn_queue, assumption+) - apply (simp add: isWaitingNtfn_def) - apply simp - apply (frule_tac x=p in map_to_ko_atI, clarsimp, clarsimp) - apply fastforce - apply (erule(2) map_to_ko_at_updI') - apply (clarsimp simp: objBitsKO_def) - apply (clarsimp simp: obj_at'_def) - \ \ntfn relation\ - apply (rule cpspace_relation_ntfn_update_ntfn', assumption+) - apply (case_tac "ntfn", simp_all)[1] - apply (clarsimp simp: cnotification_relation_def Let_def - mask_def [where n=3] NtfnState_Waiting_def) - subgoal - apply (clarsimp simp: tcb_queue_relation'_def is_aligned_neg_mask valid_ntfn'_def - dest: tcb_queue_relation_next_not_NULL) - apply (rule conjI, fastforce simp: mask_def) - apply (rule context_conjI) - subgoal by (fastforce simp: valid_pspace'_def objBits_simps' - intro!: tcb_ptr_sign_extend_canonical - dest!: st_tcb_strg'[rule_format]) - by clarsimp - apply (simp add: isWaitingNtfn_def) - subgoal sorry (* FIXME RT: refill_buffer_relation *) - \ \queue relation\ - apply (rule cready_queues_relation_null_queue_ptrs, assumption+) - subgoal by (clarsimp simp: comp_def) + \ \tcb relation\ + apply (erule ctcb_relation_null_queue_ptrs) + apply (clarsimp simp: comp_def) + \ \ep relation\ + apply (erule iffD1 [OF cmap_relation_cong, OF refl refl, rotated -1]) + apply simp + apply (rule cendpoint_relation_ntfn_queue, assumption+) + apply (simp add: isWaitingNtfn_def) + apply simp + apply (frule_tac x=p in map_to_ko_atI, clarsimp, clarsimp) + apply fastforce + apply (erule(2) map_to_ko_at_updI') + apply (clarsimp simp: objBitsKO_def) + apply (clarsimp simp: obj_at'_def) + \ \ntfn relation\ + apply (rule cpspace_relation_ntfn_update_ntfn', assumption+) + apply (case_tac "ntfn", simp_all)[1] + apply (clarsimp simp: cnotification_relation_def Let_def + mask_def [where n=3] NtfnState_Waiting_def) + subgoal + apply (clarsimp simp: tcb_queue_relation'_def is_aligned_neg_mask valid_ntfn'_def + dest: tcb_queue_relation_next_not_NULL) + apply (rule conjI, fastforce simp: mask_def) + apply (rule context_conjI) + subgoal by (fastforce simp: valid_pspace'_def objBits_simps' + intro!: tcb_ptr_sign_extend_canonical + dest!: st_tcb_strg'[rule_format]) + by clarsimp + apply (simp add: isWaitingNtfn_def) + subgoal sorry (* FIXME RT: refill_buffer_relation *) + \ \queue relations\ + apply (rule cready_queues_relation_null_queue_ptrs, assumption+) + subgoal by (clarsimp simp: comp_def) + apply (erule iffD2[OF tcb_queue_relation_only_next_prev, rotated -1]) + apply (rule null_ep_schedD[THEN conjunct1]) + apply (clarsimp simp: comp_def) + apply (rule null_ep_schedD[THEN conjunct2]) + apply (clarsimp simp: comp_def) apply (clarsimp simp: carch_state_relation_def packed_heap_update_collapse_hrs) apply (simp add: cmachine_state_relation_def) apply (simp add: h_t_valid_clift_Some_iff) @@ -6578,50 +6633,55 @@ lemma receiveSignal_enqueue_ccorres_helper: typ_heap_simps') apply (elim conjE) apply (intro conjI) - \ \tcb relation\ - apply (erule ctcb_relation_null_queue_ptrs) - apply (clarsimp simp: comp_def) - \ \ep relation\ - apply (erule iffD1 [OF cmap_relation_cong, OF refl refl, rotated -1]) - apply simp - apply (rule cendpoint_relation_ntfn_queue, assumption+) - apply (simp add: isWaitingNtfn_def) - apply simp - apply (frule_tac x=p in map_to_ko_atI, clarsimp, clarsimp) - apply fastforce - apply (erule(2) map_to_ko_at_updI') - apply (clarsimp simp: objBitsKO_def) - apply (clarsimp simp: obj_at'_def) - \ \ntfn relation\ - apply (rule cpspace_relation_ntfn_update_ntfn', assumption+) - apply (case_tac "ntfn", simp_all)[1] - apply (clarsimp simp: cnotification_relation_def Let_def - mask_def [where n=3] NtfnState_Waiting_def - split: if_split) - subgoal for _ _ ko' - apply (clarsimp simp: tcb_queue_relation'_def is_aligned_neg_mask - dest: tcb_queue_relation_next_not_NULL) - apply (rule conjI, clarsimp) - apply (rule conjI, fastforce simp: mask_def) - apply (rule context_conjI) - subgoal by (fastforce intro!: tcb_ptr_sign_extend_canonical - dest!: st_tcb_strg'[rule_format]) - apply clarsimp - apply clarsimp - apply (rule conjI, fastforce simp: mask_def) - apply (rule conjI) - subgoal by (fastforce intro!: tcb_ptr_sign_extend_canonical - dest!: st_tcb_strg'[rule_format]) - apply (subgoal_tac "canonical_address (ntfnQueue_head_CL (notification_lift ko'))") - apply (clarsimp simp: canonical_address_sign_extended sign_extended_iff_sign_extend) - apply (clarsimp simp: notification_lift_def canonical_address_sign_extended - sign_extended_sign_extend - simp flip: canonical_bit_def) - done - apply (simp add: isWaitingNtfn_def) - subgoal sorry (* FIXME RT: refill_buffer_relation *) - \ \queue relation\ - apply (rule cready_queues_relation_null_queue_ptrs, assumption+) + \ \tcb relation\ + apply (erule ctcb_relation_null_queue_ptrs) + apply (clarsimp simp: comp_def) + \ \ep relation\ + apply (erule iffD1 [OF cmap_relation_cong, OF refl refl, rotated -1]) + apply simp + apply (rule cendpoint_relation_ntfn_queue, assumption+) + apply (simp add: isWaitingNtfn_def) + apply simp + apply (frule_tac x=p in map_to_ko_atI, clarsimp, clarsimp) + apply fastforce + apply (erule(2) map_to_ko_at_updI') + apply (clarsimp simp: objBitsKO_def) + apply (clarsimp simp: obj_at'_def) + \ \ntfn relation\ + apply (rule cpspace_relation_ntfn_update_ntfn', assumption+) + apply (case_tac "ntfn", simp_all)[1] + apply (clarsimp simp: cnotification_relation_def Let_def + mask_def [where n=3] NtfnState_Waiting_def + split: if_split) + subgoal for _ _ ko' + apply (clarsimp simp: tcb_queue_relation'_def is_aligned_neg_mask + dest: tcb_queue_relation_next_not_NULL) + apply (rule conjI, clarsimp) + apply (rule conjI, fastforce simp: mask_def) + apply (rule context_conjI) + subgoal by (fastforce intro!: tcb_ptr_sign_extend_canonical + dest!: st_tcb_strg'[rule_format]) + apply clarsimp + apply clarsimp + apply (rule conjI, fastforce simp: mask_def) + apply (rule conjI) + subgoal by (fastforce intro!: tcb_ptr_sign_extend_canonical + dest!: st_tcb_strg'[rule_format]) + apply (subgoal_tac "canonical_address (ntfnQueue_head_CL (notification_lift ko'))") + apply (clarsimp simp: canonical_address_sign_extended sign_extended_iff_sign_extend) + apply (clarsimp simp: notification_lift_def canonical_address_sign_extended + sign_extended_sign_extend + simp flip: canonical_bit_def) + done + apply (simp add: isWaitingNtfn_def) + subgoal sorry (* FIXME RT: refill_buffer_relation *) + \ \queue relations\ + apply (rule cready_queues_relation_null_queue_ptrs, assumption+) + apply (clarsimp simp: comp_def) + apply (erule iffD2[OF tcb_queue_relation_only_next_prev, rotated -1]) + apply (rule null_ep_schedD[THEN conjunct1]) + apply (clarsimp simp: comp_def) + apply (rule null_ep_schedD[THEN conjunct2]) apply (clarsimp simp: comp_def) apply (clarsimp simp: carch_state_relation_def packed_heap_update_collapse_hrs) apply (simp add: cmachine_state_relation_def) diff --git a/proof/crefine/RISCV64/Recycle_C.thy b/proof/crefine/RISCV64/Recycle_C.thy index 61f33e239c..e8b57db721 100644 --- a/proof/crefine/RISCV64/Recycle_C.thy +++ b/proof/crefine/RISCV64/Recycle_C.thy @@ -773,16 +773,6 @@ lemma cnotification_relation_q_cong: apply (auto intro: iffD1[OF tcb_queue_relation'_cong[OF refl refl refl]]) done -lemma tcbSchedEnqueue_ep_at: - "\obj_at' (P :: endpoint \ bool) ep\ - tcbSchedEnqueue t - \\rv. obj_at' P ep\" - including no_pre - apply (simp add: tcbSchedEnqueue_def unless_def null_def) - apply (wp threadGet_wp, clarsimp, wp+) - apply (clarsimp split: if_split, wp) - done - lemma ccorres_duplicate_guard: "ccorres r xf (P and P) Q hs f f' \ ccorres r xf P Q hs f f'" by (erule ccorres_guard_imp, auto) diff --git a/proof/crefine/RISCV64/Refine_C.thy b/proof/crefine/RISCV64/Refine_C.thy index ab1ef0813b..54b8496987 100644 --- a/proof/crefine/RISCV64/Refine_C.thy +++ b/proof/crefine/RISCV64/Refine_C.thy @@ -892,17 +892,20 @@ lemma dmo_domain_user_mem'[wp]: done lemma do_user_op_corres_C: - "corres_underlying rf_sr False False (=) (invs' and ex_abs einvs) \ - (doUserOp f tc) (doUserOp_C f tc)" + "corres_underlying rf_sr False False (=) + (invs' and (\s. sch_act_wf (ksSchedulerAction s) s) and ex_abs einvs) \ + (doUserOp f tc) (doUserOp_C f tc)" apply (simp only: doUserOp_C_def doUserOp_def split_def) apply (rule corres_guard_imp) apply (rule_tac P=\ and P'=\ and r'="(=)" in corres_split) apply (clarsimp simp: simpler_gets_def getCurThread_def corres_underlying_def rf_sr_def cstate_relation_def Let_def) - apply (rule_tac P=invs' and P'=\ and r'="(=)" in corres_split) + apply (rule_tac P="invs' and (\s. sch_act_wf (ksSchedulerAction s) s)" + and P'=\ and r'="(=)" in corres_split) apply (clarsimp simp: cstate_to_A_def absKState_def rf_sr_def cstate_to_H_correct ptable_lift_def) - apply (rule_tac P=invs' and P'=\ and r'="(=)" in corres_split) + apply (rule_tac P="invs' and (\s. sch_act_wf (ksSchedulerAction s) s)" + and P'=\ and r'="(=)" in corres_split) apply (clarsimp simp: cstate_to_A_def absKState_def rf_sr_def cstate_to_H_correct ptable_rights_def) apply (rule_tac P=pspace_distinct' and P'=\ and r'="(=)" @@ -998,7 +1001,12 @@ lemma refinement2_both: apply (drule lift_state_relationD) apply (clarsimp simp: cstate_to_A_def) apply (subst cstate_to_H_correct) - apply (fastforce simp: full_invs'_def invs'_def) + apply (fastforce simp: full_invs'_def invs'_def) + apply (clarsimp simp: lift_state_relation_def full_invs_def) + apply (rule sch_act_wf_cross) + apply force + subgoal by (clarsimp simp: valid_sched_def) + apply fastforce+ apply (clarsimp simp: rf_sr_def) apply (simp add:absKState_def observable_memory_def absExst_def) apply (rule MachineTypes.machine_state.equality,simp_all)[1] diff --git a/proof/crefine/RISCV64/Retype_C.thy b/proof/crefine/RISCV64/Retype_C.thy index 15f36d1637..c987c30095 100644 --- a/proof/crefine/RISCV64/Retype_C.thy +++ b/proof/crefine/RISCV64/Retype_C.thy @@ -5220,7 +5220,11 @@ lemma threadSet_domain_ccorres [corres]: subgoal by (simp add: ctcb_relation_def) apply assumption apply simp - apply (erule cready_queues_relation_not_queue_ptrs) + apply (rule conjI) + apply (erule cready_queues_relation_not_queue_ptrs) + apply (rule ext, simp split: if_split) + apply (rule ext, simp split: if_split) + apply (erule iffD2[OF tcb_queue_relation_only_next_prev, rotated -1]) apply (rule ext, simp split: if_split) apply (rule ext, simp split: if_split) done diff --git a/proof/crefine/RISCV64/SR_lemmas_C.thy b/proof/crefine/RISCV64/SR_lemmas_C.thy index c690e061c8..a7bf27399e 100644 --- a/proof/crefine/RISCV64/SR_lemmas_C.thy +++ b/proof/crefine/RISCV64/SR_lemmas_C.thy @@ -1077,7 +1077,9 @@ lemma cstate_relation_only_t_hrs: ksDomScheduleIdx_' s = ksDomScheduleIdx_' t; ksCurDomain_' s = ksCurDomain_' t; ksDomainTime_' s = ksDomainTime_' t; - ksConsumed_' s = ksConsumed_' t + ksConsumed_' s = ksConsumed_' t; + ksReleaseHead_' s = ksReleaseHead_' t; + ksReprogram_' s = ksReprogram_' t \ \ cstate_relation a s = cstate_relation a t" unfolding cstate_relation_def @@ -1104,6 +1106,8 @@ lemma rf_sr_upd: "ksCurDomain_' (globals x) = ksCurDomain_' (globals y)" "ksDomainTime_' (globals x) = ksDomainTime_' (globals y)" "ksConsumed_' (globals x) = ksConsumed_' (globals y)" + "ksReleaseHead_' (globals x) = ksReleaseHead_' (globals y)" + "ksReprogram_' (globals x) = ksReprogram_' (globals y)" shows "((a, x) \ rf_sr) = ((a, y) \ rf_sr)" unfolding rf_sr_def using assms by simp (rule cstate_relation_only_t_hrs, auto) @@ -1129,8 +1133,10 @@ lemma rf_sr_upd_safe[simp]: "phantom_machine_state_' (globals (g y)) = phantom_machine_state_' (globals y)" and gs: "ghost'state_' (globals (g y)) = ghost'state_' (globals y)" and wu: "(ksWorkUnitsCompleted_' (globals (g y))) = (ksWorkUnitsCompleted_' (globals y))" + and rlshd: "(ksReleaseHead_' (globals (g y))) = (ksReleaseHead_' (globals y))" + and reprog: "(ksReprogram_' (globals (g y))) = (ksReprogram_' (globals y))" shows "((a, (g y)) \ rf_sr) = ((a, y) \ rf_sr)" - using rl rq rqL1 rqL2 sa ct ctime csc it isc ist arch wu gs dsi cdom dt cons + using rl rq rqL1 rqL2 sa ct ctime csc it isc ist arch wu gs dsi cdom dt cons rlshd reprog by - (rule rf_sr_upd) (* More of a well-formed lemma, but \ *) diff --git a/proof/crefine/RISCV64/Schedule_C.thy b/proof/crefine/RISCV64/Schedule_C.thy index bfe21318ec..b00608a581 100644 --- a/proof/crefine/RISCV64/Schedule_C.thy +++ b/proof/crefine/RISCV64/Schedule_C.thy @@ -77,8 +77,13 @@ lemma ready_qs_runnable_ksMachineState[simp]: "ready_qs_runnable (ksMachineState_update f s) = ready_qs_runnable s" by (clarsimp simp: ready_qs_runnable_def) +lemma ready_or_release'_ksMachineState[simp]: + "ready_or_release' (ksMachineState_update f s) = ready_or_release' s" + by (clarsimp simp: ready_or_release'_def) + crunches setVMRoot for ready_qs_runnable'[wp]: ready_qs_runnable + and ready_or_release'[wp]: ready_or_release' (wp: crunch_wps) lemma switchToThread_ready_qs_runnable[wp]: @@ -86,10 +91,15 @@ lemma switchToThread_ready_qs_runnable[wp]: unfolding RISCV64_H.switchToThread_def by wpsimp +lemma switchToThread_ready_or_release'[wp]: + "RISCV64_H.switchToThread t \ready_or_release'\" + unfolding RISCV64_H.switchToThread_def + by wpsimp + (* FIXME: move *) lemma switchToThread_ccorres: "ccorres dc xfdc - (invs' and tcb_at' t and (\s. \d p. distinct (ksReadyQueues s (d, p)))) + (invs' and tcb_at' t and (\s. \d p. distinct (ksReadyQueues s (d, p))) and ready_or_release') (UNIV \ \\thread = tcb_ptr_to_ctcb_ptr t\) hs (switchToThread t) @@ -211,7 +221,7 @@ lemmas ccorres_remove_tail_Guard_Skip lemma switchToThread_ccorres': "ccorres dc xfdc - (invs' and tcb_at' t and (\s. \d p. distinct (ksReadyQueues s (d, p)))) + (invs' and tcb_at' t and (\s. \d p. distinct (ksReadyQueues s (d, p))) and ready_or_release') (UNIV \ \\thread = tcb_ptr_to_ctcb_ptr t\) hs (switchToThread t) @@ -225,7 +235,8 @@ lemmas word_log2_max_word_word_size = word_log2_max[where 'a=machine_word_len, s lemma chooseThread_ccorres: "ccorres dc xfdc - (invs' and valid_idle' and (\s. \d p. distinct (ksReadyQueues s (d, p)))) UNIV [] + (invs' and valid_idle' and (\s. \d p. distinct (ksReadyQueues s (d, p))) and ready_or_release') + UNIV [] chooseThread (Call chooseThread_'proc)" proof - @@ -381,12 +392,13 @@ sorry (* FIXME RT: nextDomain_ccorres. Involves usToTicks crunches nextDomain for valid_idle'[wp]: valid_idle' and distinct_queues[wp]: "\s. distinct (ksReadyQueues s (d, p))" - (simp: crunch_simps) + and ready_or_release'[wp]: ready_or_release' + (simp: crunch_simps ready_or_release'_def) lemma scheduleChooseNewThread_ccorres: "ccorres dc xfdc (\s. invs' s \ valid_idle' s \ (\d p. distinct (ksReadyQueues s (d, p))) - \ ksSchedulerAction s = ChooseNewThread) UNIV hs + \ ksSchedulerAction s = ChooseNewThread \ ready_or_release' s) UNIV hs (do domainTime \ getDomainTime; y \ when (domainTime = 0) nextDomain; chooseThread diff --git a/proof/crefine/RISCV64/StateRelation_C.thy b/proof/crefine/RISCV64/StateRelation_C.thy index 7aa88348b0..155d3405c5 100644 --- a/proof/crefine/RISCV64/StateRelation_C.thy +++ b/proof/crefine/RISCV64/StateRelation_C.thy @@ -444,7 +444,7 @@ definition refill_buffer_relation :: lemma refill_buffer_relation_gs_dom: "refill_buffer_relation ah ch gs \ let abs_sc_hp = map_to_scs ah; - lens_hp = gs_refill_buffer_lengths gs + lens_hp = gs_sc_size gs in dom abs_sc_hp = dom lens_hp" by (simp add: refill_buffer_relation_def Let_def) @@ -452,7 +452,7 @@ lemma refill_buffer_relation_crefill_hp_dom: "refill_buffer_relation ah ch gs \ let abs_sc_hp = map_to_scs ah; crefill_hp = clift ch; - lens_hp = gs_refill_buffer_lengths gs + lens_hp = gs_sc_size gs in dom crefill_hp = (\p\dom abs_sc_hp. set (map (\i. sc_ptr_to_crefill_ptr p +\<^sub>p int i) [0.. let abs_sc_hp = map_to_scs ah; crefill_hp = clift ch; - lens_hp = gs_refill_buffer_lengths gs + lens_hp = gs_sc_size gs in (\p sc. abs_sc_hp p = Some sc \ dyn_array_list_rel crefill_hp crefill_relation (scRefills sc) (sc_ptr_to_crefill_ptr p) \ lens_hp p = Some (length (scRefills sc)))" @@ -829,6 +829,7 @@ where cready_queues_relation (clift cheap) (ksReadyQueues_' cstate) (ksReadyQueues astate) \ + sched_queue_relation (clift cheap) (ksReleaseQueue astate) NULL (ksReleaseHead_' cstate) \ zero_ranges_are_zero (gsUntypedZeroRanges astate) cheap \ cbitmap_L1_relation (ksReadyQueuesL1Bitmap_' cstate) (ksReadyQueuesL1Bitmap astate) \ cbitmap_L2_relation (ksReadyQueuesL2Bitmap_' cstate) (ksReadyQueuesL2Bitmap astate) \ @@ -859,7 +860,8 @@ where Kernel_C.kernel_all_global_addresses.ksDomSchedule \ ksDomScheduleIdx_' cstate = of_nat (ksDomScheduleIdx astate) \ ksCurDomain_' cstate = ucast (ksCurDomain astate) \ - ksDomainTime_' cstate = ksDomainTime astate" + ksDomainTime_' cstate = ksDomainTime astate \ + to_bool (ksReprogram_' cstate) = ksReprogramTimer astate" end diff --git a/proof/crefine/RISCV64/TcbQueue_C.thy b/proof/crefine/RISCV64/TcbQueue_C.thy index ff0efb30e9..b5349b162e 100644 --- a/proof/crefine/RISCV64/TcbQueue_C.thy +++ b/proof/crefine/RISCV64/TcbQueue_C.thy @@ -1395,23 +1395,24 @@ lemma rf_sr_tcb_update_no_queue: apply (clarsimp simp: map_comp_update projectKO_opt_tcb cvariable_relation_upd_const typ_heap_simps') apply (intro conjI) - subgoal by (clarsimp simp: cmap_relation_def map_comp_update projectKO_opts_defs inj_eq) + subgoal by (clarsimp simp: cmap_relation_def map_comp_update projectKO_opts_defs inj_eq) + apply (erule iffD1 [OF cmap_relation_cong, OF refl refl, rotated -1]) + apply simp + apply (rule cendpoint_relation_upd_tcb_no_queues, assumption+) + subgoal by fastforce + subgoal by fastforce apply (erule iffD1 [OF cmap_relation_cong, OF refl refl, rotated -1]) apply simp - apply (rule cendpoint_relation_upd_tcb_no_queues, assumption+) + apply (rule cnotification_relation_upd_tcb_no_queues, assumption+) subgoal by fastforce subgoal by fastforce - apply (erule iffD1 [OF cmap_relation_cong, OF refl refl, rotated -1]) - apply simp - apply (rule cnotification_relation_upd_tcb_no_queues, assumption+) - subgoal by fastforce - subgoal by fastforce - subgoal by (clarsimp simp: map_comp_update projectKO_opt_sc typ_heap_simps' - refill_buffer_relation_def) + subgoal by (clarsimp simp: map_comp_update projectKO_opt_sc typ_heap_simps' + refill_buffer_relation_def) apply (erule cready_queues_relation_not_queue_ptrs) subgoal by fastforce subgoal by fastforce - subgoal by (clarsimp simp: carch_state_relation_def typ_heap_simps') + subgoal by (fastforce elim!: iffD2[OF tcb_queue_relation_only_next_prev, rotated -1]) + subgoal by (clarsimp simp: carch_state_relation_def typ_heap_simps') by (simp add: cmachine_state_relation_def) lemma rf_sr_tcb_update_no_queue_helper: