From b8fc709d210e67433e01143330d3410b71a98a09 Mon Sep 17 00:00:00 2001 From: Rafal Kolanski Date: Tue, 8 Jun 2021 21:33:00 +1000 Subject: [PATCH] refine+orphanage: update proofs to never unfold numDomains Proofs now don't care about numDomains, except for a small interface in Invariants_H. The interface is currently by convention only, and has no enforcement capabilities. Signed-off-by: Rafal Kolanski --- proof/refine/ARM/Interrupt_R.thy | 24 +++---- proof/refine/ARM/Invariants_H.thy | 16 +++++ proof/refine/ARM/Retype_R.thy | 3 +- proof/refine/ARM/Schedule_R.thy | 70 +++++++++++++++----- proof/refine/ARM/Syscall_R.thy | 2 +- proof/refine/ARM/orphanage/Orphanage.thy | 33 +++++---- proof/refine/ARM_HYP/Interrupt_R.thy | 24 +++---- proof/refine/ARM_HYP/Invariants_H.thy | 15 +++++ proof/refine/ARM_HYP/Retype_R.thy | 3 +- proof/refine/ARM_HYP/Schedule_R.thy | 67 ++++++++++++++----- proof/refine/ARM_HYP/Syscall_R.thy | 2 +- proof/refine/RISCV64/Interrupt_R.thy | 24 +++---- proof/refine/RISCV64/Invariants_H.thy | 17 ++++- proof/refine/RISCV64/Retype_R.thy | 4 +- proof/refine/RISCV64/Schedule_R.thy | 67 ++++++++++++++----- proof/refine/RISCV64/Syscall_R.thy | 2 +- proof/refine/RISCV64/orphanage/Orphanage.thy | 36 +++++----- proof/refine/X64/Interrupt_R.thy | 24 +++---- proof/refine/X64/Invariants_H.thy | 15 +++++ proof/refine/X64/Retype_R.thy | 3 +- proof/refine/X64/Schedule_R.thy | 67 ++++++++++++++----- proof/refine/X64/Syscall_R.thy | 2 +- 22 files changed, 356 insertions(+), 164 deletions(-) diff --git a/proof/refine/ARM/Interrupt_R.thy b/proof/refine/ARM/Interrupt_R.thy index 3b61788c9..6ca4d83db 100644 --- a/proof/refine/ARM/Interrupt_R.thy +++ b/proof/refine/ARM/Interrupt_R.thy @@ -607,11 +607,6 @@ lemma getIRQState_prop: apply simp done -lemma num_domains[simp]: - "num_domains = numDomains" - apply(simp add: num_domains_def numDomains_def) - done - lemma decDomainTime_corres: "corres dc \ \ dec_domain_time decDomainTime" apply (simp add:dec_domain_time_def corres_underlying_def @@ -830,17 +825,16 @@ crunch cur_tcb'[wp]: tcbSchedAppend cur_tcb' lemma timerTick_invs'[wp]: "\invs'\ timerTick \\rv. invs'\" - apply (simp add: numDomains_def timerTick_def) - apply (wp threadSet_invs_trivial threadSet_pred_tcb_no_state - rescheduleRequired_all_invs_but_ct_not_inQ - tcbSchedAppend_invs_but_ct_not_inQ' - | simp add: tcb_cte_cases_def numDomains_def - | wpc)+ - apply (simp add:decDomainTime_def) - apply wp - apply simp + apply (simp add: timerTick_def) + apply (wpsimp wp: threadSet_invs_trivial threadSet_pred_tcb_no_state + rescheduleRequired_all_invs_but_ct_not_inQ + tcbSchedAppend_invs_but_ct_not_inQ' + simp: tcb_cte_cases_def) apply (rule_tac Q="\rv. invs'" in hoare_post_imp) apply (clarsimp simp add:invs'_def valid_state'_def) + apply (simp add: decDomainTime_def) + apply wp + apply simp apply wpc apply (wp add: threadGet_wp threadSet_cur threadSet_timeslice_invs rescheduleRequired_all_invs_but_ct_not_inQ @@ -852,7 +846,7 @@ lemma timerTick_invs'[wp]: threadSet_valid_objs' threadSet_timeslice_invs)+ apply (wp threadGet_wp) apply (wp gts_wp')+ - apply (clarsimp simp: invs'_def st_tcb_at'_def obj_at'_def valid_state'_def numDomains_def) + apply (clarsimp simp: invs'_def st_tcb_at'_def obj_at'_def valid_state'_def) done lemma resetTimer_invs'[wp]: diff --git a/proof/refine/ARM/Invariants_H.thy b/proof/refine/ARM/Invariants_H.thy index 6fa58a1f5..1c35897b9 100644 --- a/proof/refine/ARM/Invariants_H.thy +++ b/proof/refine/ARM/Invariants_H.thy @@ -31,6 +31,21 @@ end end +section "Relationship of Executable Spec to Kernel Configuration" + +text \ + Some values are set per kernel configuration (e.g. number of domains), but other related + values (e.g. maximum domain) are derived from storage constraints (e.g. bytes used). + To relate the two, we must look at the values of kernel configuration constants. + To allow the proofs to work for all permitted values of these constants, their definitions + should only be unfolded in this section, and the derived properties kept to a minimum.\ + +lemma le_maxDomain_eq_less_numDomains: + shows "x \ unat maxDomain \ x < Kernel_Config.numDomains" + "y \ maxDomain \ unat y < Kernel_Config.numDomains" + by (auto simp: Kernel_Config.numDomains_def maxDomain_def word_le_nat_alt) + + context begin interpretation Arch . (*FIXME: arch_split*) \ \---------------------------------------------------------------------------\ section "Invariants on Executable Spec" @@ -3377,4 +3392,5 @@ end add_upd_simps "invs' (gsUntypedZeroRanges_update f s)" (obj_at'_real_def) declare upd_simps[simp] + end diff --git a/proof/refine/ARM/Retype_R.thy b/proof/refine/ARM/Retype_R.thy index 33fd97cad..72bc0c12a 100644 --- a/proof/refine/ARM/Retype_R.thy +++ b/proof/refine/ARM/Retype_R.thy @@ -108,8 +108,7 @@ lemma valid_obj_makeObject_cte [simp]: lemma valid_obj_makeObject_tcb [simp]: "valid_obj' (KOTCB makeObject) s" unfolding valid_obj'_def valid_tcb'_def valid_tcb_state'_def - by (clarsimp simp: makeObject_tcb makeObject_cte - tcb_cte_cases_def maxDomain_def numDomains_def maxPriority_def numPriorities_def minBound_word) + by (clarsimp simp: makeObject_tcb makeObject_cte tcb_cte_cases_def minBound_word) lemma valid_obj_makeObject_endpoint [simp]: "valid_obj' (KOEndpoint makeObject) s" diff --git a/proof/refine/ARM/Schedule_R.thy b/proof/refine/ARM/Schedule_R.thy index d748f9689..c7701c5ea 100644 --- a/proof/refine/ARM/Schedule_R.thy +++ b/proof/refine/ARM/Schedule_R.thy @@ -1415,7 +1415,8 @@ lemma switchToIdleThread_curr_is_idle: lemma chooseThread_it[wp]: "\\s. P (ksIdleThread s)\ chooseThread \\_ s. P (ksIdleThread s)\" - by (wp|clarsimp simp: chooseThread_def curDomain_def numDomains_def bitmap_fun_defs|assumption)+ + supply if_split[split del] + by (wpsimp simp: chooseThread_def curDomain_def bitmap_fun_defs) lemma threadGet_inv [wp]: "\P\ threadGet f t \\rv. P\" apply (simp add: threadGet_def) @@ -1503,6 +1504,16 @@ abbreviation "enumPrio \ [0.e.maxPriority]" lemma curDomain_corres: "corres (=) \ \ (gets cur_domain) (curDomain)" by (simp add: curDomain_def state_relation_def) +lemma curDomain_corres': + "corres (=) \ (\s. ksCurDomain s \ maxDomain) + (gets cur_domain) (if 1 < numDomains then curDomain else return 0)" + apply (case_tac "1 < numDomains"; simp) + apply (rule corres_guard_imp[OF curDomain_corres]; solves simp) + (* if we have only one domain, then we are in it *) + apply (clarsimp simp: return_def simpler_gets_def bind_def maxDomain_def + state_relation_def corres_underlying_def) + done + lemma lookupBitmapPriority_Max_eqI: "\ valid_bitmapQ s ; bitmapQ_no_L1_orphans s ; ksReadyQueuesL1Bitmap s d \ 0 \ \ lookupBitmapPriority d s = (Max {prio. ksReadyQueues s (d, prio) \ []})" @@ -1569,18 +1580,27 @@ lemma ksReadyQueuesL1Bitmap_st_tcb_at': apply simp done +lemma curDomain_or_return_0: + "\ \P\ curDomain \\rv s. Q rv s \; \s. P s \ ksCurDomain s \ maxDomain \ + \ \P\ if 1 < numDomains then curDomain else return 0 \\rv s. Q rv s \" + apply (case_tac "1 < numDomains"; simp) + apply (simp add: valid_def curDomain_def simpler_gets_def return_def maxDomain_def) + done + +lemma invs_no_cicd_ksCurDomain_maxDomain': + "invs_no_cicd' s \ ksCurDomain s \ maxDomain" + unfolding invs_no_cicd'_def by simp + lemma chooseThread_corres: "corres dc (invs and valid_sched) (invs_no_cicd') choose_thread chooseThread" (is "corres _ ?PREI ?PREH _ _") proof - show ?thesis - unfolding choose_thread_def chooseThread_def numDomains_def - apply (simp only: numDomains_def return_bind Let_def) - apply (simp cong: if_cong) (* clean up if 1 < numDomains *) + unfolding choose_thread_def chooseThread_def + apply (simp only: return_bind Let_def) apply (subst if_swap[where P="_ \ 0"]) (* put switchToIdleThread on first branch*) - apply (rule corres_name_pre) apply (rule corres_guard_imp) - apply (rule corres_split_deprecated[OF _ curDomain_corres]) + apply (rule corres_split[OF curDomain_corres']) apply clarsimp apply (rule corres_split_deprecated[OF _ corres_gets_queues_getReadyQueuesL1Bitmap]) apply (erule corres_if2[OF sym]) @@ -1603,15 +1623,17 @@ proof - apply (wp | clarsimp simp: getQueue_def getReadyQueuesL2Bitmap_def)+ apply (clarsimp simp: if_apply_def2) apply (wp hoare_vcg_conj_lift hoare_vcg_imp_lift ksReadyQueuesL1Bitmap_return_wp) - apply (simp add: curDomain_def, wp)+ + apply (wpsimp wp: curDomain_or_return_0 simp: curDomain_def)+ + apply (fastforce simp: invs_no_cicd'_def) apply (clarsimp simp: valid_sched_def DetSchedInvs_AI.valid_queues_def max_non_empty_queue_def) - apply (erule_tac x="cur_domain sa" in allE) - apply (erule_tac x="Max {prio. ready_queues sa (cur_domain sa) prio \ []}" in allE) - apply (case_tac "ready_queues sa (cur_domain sa) (Max {prio. ready_queues sa (cur_domain sa) prio \ []})") + apply (erule_tac x="cur_domain s" in allE) + apply (erule_tac x="Max {prio. ready_queues s (cur_domain s) prio \ []}" in allE) + apply (case_tac "ready_queues s (cur_domain s) (Max {prio. ready_queues s (cur_domain s) prio \ []})") apply (clarsimp) apply (subgoal_tac - "ready_queues sa (cur_domain sa) (Max {prio. ready_queues sa (cur_domain sa) prio \ []}) \ []") + "ready_queues s (cur_domain s) (Max {prio. ready_queues s (cur_domain s) prio \ []}) \ []") apply (fastforce elim!: setcomp_Max_has_prop)+ + apply (simp add: invs_no_cicd_ksCurDomain_maxDomain') apply (clarsimp dest!: invs_no_cicd'_queues) apply (fastforce intro: ksReadyQueuesL1Bitmap_st_tcb_at') done @@ -2012,9 +2034,15 @@ proof - note switchToThread_invs_no_cicd'[wp del] note switchToThread_lookupBitmapPriority_wp[wp] note assert_wp[wp del] + note if_split[split del] + + (* if we only have one domain, we are in it *) + have one_domain_case: + "\s. \ invs_no_cicd' s; numDomains \ 1 \ \ ksCurDomain s = 0" + by (simp add: all_invs_but_ct_idle_or_in_cur_domain'_def maxDomain_def) show ?thesis - unfolding chooseThread_def Let_def numDomains_def curDomain_def + unfolding chooseThread_def Let_def curDomain_def apply (simp only: return_bind, simp) apply (rule hoare_seq_ext[where B="\rv s. invs_no_cicd' s \ rv = ksCurDomain s"]) apply (rule_tac B="\rv s. invs_no_cicd' s \ curdom = ksCurDomain s \ @@ -2038,7 +2066,7 @@ proof - apply (drule (3) lookupBitmapPriority_obj_at') apply normalise_obj_at' apply (fastforce simp: tcb_in_cur_domain'_def inQ_def elim: obj_at'_weaken) - apply (wp | simp add: bitmap_fun_defs curDomain_def)+ + apply (wpsimp simp: bitmap_fun_defs curDomain_def one_domain_case)+ done qed @@ -2064,10 +2092,19 @@ proof - note switchToThread_invs_no_cicd'[wp del] note switchToThread_lookupBitmapPriority_wp[wp] note assert_wp[wp del] + note if_split[split del] + + (* if we only have one domain, we are in it *) + have one_domain_case: + "\s. \ invs_no_cicd' s; numDomains \ 1 \ \ ksCurDomain s = 0" + by (simp add: all_invs_but_ct_idle_or_in_cur_domain'_def maxDomain_def) + + (* NOTE: do *not* unfold numDomains in the rest of the proof, + it should work for any number *) (* FIXME this is almost identical to the chooseThread_invs_no_cicd'_posts proof, can generalise? *) show ?thesis - unfolding chooseThread_def Let_def numDomains_def curDomain_def + unfolding chooseThread_def Let_def curDomain_def apply (simp only: return_bind, simp) apply (rule hoare_seq_ext[where B="\rv s. invs_no_cicd' s \ rv = ksCurDomain s"]) apply (rule_tac B="\rv s. invs_no_cicd' s \ curdom = ksCurDomain s \ @@ -2081,7 +2118,7 @@ proof - apply (wp assert_inv) apply (clarsimp dest!: invs_no_cicd'_queues simp: valid_queues_def) apply (fastforce elim: bitmapQ_from_bitmap_lookup simp: lookupBitmapPriority_def) - apply (wp | simp add: bitmap_fun_defs curDomain_def)+ + apply (wpsimp simp: bitmap_fun_defs curDomain_def one_domain_case)+ done qed @@ -2156,7 +2193,8 @@ lemma chooseThread_nosch: "\\s. P (ksSchedulerAction s)\ chooseThread \\rv s. P (ksSchedulerAction s)\" - unfolding chooseThread_def Let_def numDomains_def curDomain_def + unfolding chooseThread_def Let_def curDomain_def + supply if_split[split del] apply (simp only: return_bind, simp) apply (wp findM_inv | simp)+ apply (case_tac queue) diff --git a/proof/refine/ARM/Syscall_R.thy b/proof/refine/ARM/Syscall_R.thy index 8271f545b..d240459d6 100644 --- a/proof/refine/ARM/Syscall_R.thy +++ b/proof/refine/ARM/Syscall_R.thy @@ -606,7 +606,7 @@ lemma dec_dom_inv_wf[wp]: apply (simp add:not_le) apply (simp del: Word.of_nat_unat flip: ucast_nat_def) apply (rule word_of_nat_le) - apply (simp add:numDomains_def maxDomain_def) + apply (simp add: le_maxDomain_eq_less_numDomains) done lemma decode_inv_wf'[wp]: diff --git a/proof/refine/ARM/orphanage/Orphanage.thy b/proof/refine/ARM/orphanage/Orphanage.thy index 50ca02d5c..43b95866e 100644 --- a/proof/refine/ARM/orphanage/Orphanage.thy +++ b/proof/refine/ARM/orphanage/Orphanage.thy @@ -795,7 +795,8 @@ lemma chooseThread_no_orphans [wp]: chooseThread \ \rv s. no_orphans s \" (is "\?PRE\ _ \_\") - unfolding chooseThread_def Let_def numDomains_def curDomain_def + unfolding chooseThread_def Let_def + supply if_split[split del] apply (simp only: return_bind, simp) apply (rule hoare_seq_ext[where B="\rv s. ?PRE s \ rv = ksCurDomain s"]) apply (rule_tac B="\rv s. ?PRE s \ curdom = ksCurDomain s \ @@ -811,7 +812,9 @@ lemma chooseThread_no_orphans [wp]: valid_queues_def st_tcb_at'_def) apply (fastforce dest!: lookupBitmapPriority_obj_at' elim: obj_at'_weaken simp: all_active_tcb_ptrs_def) - apply (simp add: bitmap_fun_defs | wp)+ + apply (wpsimp simp: bitmap_fun_defs) + apply (wp curDomain_or_return_0[simplified]) + apply (wpsimp simp: curDomain_def simp: invs_no_cicd_ksCurDomain_maxDomain')+ done lemma tcbSchedAppend_in_ksQ: @@ -1215,18 +1218,20 @@ lemma timerTick_no_orphans [wp]: "\ \s. no_orphans s \ invs' s \ timerTick \ \_ s. no_orphans s \" - unfolding timerTick_def getDomainTime_def numDomains_def - apply (rule hoare_pre) - apply (wp hoare_drop_imps | clarsimp)+ - apply (wp threadSet_valid_queues' tcbSchedAppend_almost_no_orphans - threadSet_almost_no_orphans threadSet_no_orphans tcbSchedAppend_sch_act_wf - | wpc | clarsimp - | strengthen sch_act_wf_weak)+ - apply (rule_tac Q="\rv s. no_orphans s \ valid_queues' s \ tcb_at' thread s - \ sch_act_wf (ksSchedulerAction s) s" in hoare_post_imp) - apply (clarsimp simp: inQ_def) - apply (wp hoare_drop_imps | clarsimp)+ - apply auto + unfolding timerTick_def getDomainTime_def + supply if_split[split del] + apply (subst threadState_case_if) + apply (wpsimp wp: threadSet_no_orphans threadSet_valid_queues' + threadSet_valid_queues' tcbSchedAppend_almost_no_orphans + threadSet_almost_no_orphans threadSet_no_orphans tcbSchedAppend_sch_act_wf + hoare_drop_imp + simp: if_apply_def2 + | strengthen sch_act_wf_weak)+ + apply (rule_tac Q="\rv s. no_orphans s \ valid_queues' s \ tcb_at' thread s + \ sch_act_wf (ksSchedulerAction s) s" in hoare_post_imp) + apply (clarsimp simp: inQ_def) + apply (wp hoare_drop_imps | clarsimp)+ + apply (auto split: if_split) done diff --git a/proof/refine/ARM_HYP/Interrupt_R.thy b/proof/refine/ARM_HYP/Interrupt_R.thy index b331cfce2..5881fd332 100644 --- a/proof/refine/ARM_HYP/Interrupt_R.thy +++ b/proof/refine/ARM_HYP/Interrupt_R.thy @@ -594,11 +594,6 @@ lemma getIRQState_prop: apply simp done -lemma num_domains[simp]: - "num_domains = numDomains" - apply(simp add: num_domains_def numDomains_def) - done - lemma decDomainTime_corres: "corres dc \ \ dec_domain_time decDomainTime" apply (simp add:dec_domain_time_def corres_underlying_def @@ -1106,17 +1101,16 @@ crunch cur_tcb'[wp]: tcbSchedAppend cur_tcb' lemma timerTick_invs'[wp]: "\invs'\ timerTick \\rv. invs'\" - apply (simp add: numDomains_def timerTick_def) - apply (wp threadSet_invs_trivial threadSet_pred_tcb_no_state - rescheduleRequired_all_invs_but_ct_not_inQ - tcbSchedAppend_invs_but_ct_not_inQ' - | simp add: tcb_cte_cases_def numDomains_def - | wpc)+ - apply (simp add:decDomainTime_def) - apply wp - apply simp + apply (simp add: timerTick_def) + apply (wpsimp wp: threadSet_invs_trivial threadSet_pred_tcb_no_state + rescheduleRequired_all_invs_but_ct_not_inQ + tcbSchedAppend_invs_but_ct_not_inQ' + simp: tcb_cte_cases_def) apply (rule_tac Q="\rv. invs'" in hoare_post_imp) apply (clarsimp simp add:invs'_def valid_state'_def) + apply (simp add: decDomainTime_def) + apply wp + apply simp apply wpc apply (wp add: threadGet_wp threadSet_cur threadSet_timeslice_invs rescheduleRequired_all_invs_but_ct_not_inQ @@ -1128,7 +1122,7 @@ lemma timerTick_invs'[wp]: threadSet_valid_objs' threadSet_timeslice_invs)+ apply (wp threadGet_wp) apply (wp gts_wp')+ - apply (clarsimp simp: invs'_def st_tcb_at'_def obj_at'_def valid_state'_def numDomains_def) + apply (clarsimp simp: invs'_def st_tcb_at'_def obj_at'_def valid_state'_def) done lemma resetTimer_invs'[wp]: diff --git a/proof/refine/ARM_HYP/Invariants_H.thy b/proof/refine/ARM_HYP/Invariants_H.thy index a8d65b7b4..1a7a686f3 100644 --- a/proof/refine/ARM_HYP/Invariants_H.thy +++ b/proof/refine/ARM_HYP/Invariants_H.thy @@ -31,6 +31,21 @@ end end +section "Relationship of Executable Spec to Kernel Configuration" + +text \ + Some values are set per kernel configuration (e.g. number of domains), but other related + values (e.g. maximum domain) are derived from storage constraints (e.g. bytes used). + To relate the two, we must look at the values of kernel configuration constants. + To allow the proofs to work for all permitted values of these constants, their definitions + should only be unfolded in this section, and the derived properties kept to a minimum.\ + +lemma le_maxDomain_eq_less_numDomains: + shows "x \ unat maxDomain \ x < Kernel_Config.numDomains" + "y \ maxDomain \ unat y < Kernel_Config.numDomains" + by (auto simp: Kernel_Config.numDomains_def maxDomain_def word_le_nat_alt) + + context begin interpretation Arch . (*FIXME: arch_split*) \ \---------------------------------------------------------------------------\ section "Invariants on Executable Spec" diff --git a/proof/refine/ARM_HYP/Retype_R.thy b/proof/refine/ARM_HYP/Retype_R.thy index c6c2237eb..b1400ef4b 100644 --- a/proof/refine/ARM_HYP/Retype_R.thy +++ b/proof/refine/ARM_HYP/Retype_R.thy @@ -113,8 +113,7 @@ lemma valid_obj_makeObject_cte [simp]: lemma valid_obj_makeObject_tcb [simp]: "valid_obj' (KOTCB makeObject) s" unfolding valid_obj'_def valid_tcb'_def valid_tcb_state'_def valid_arch_tcb'_def - by (clarsimp simp: makeObject_tcb makeObject_cte newArchTCB_def - tcb_cte_cases_def maxDomain_def numDomains_def maxPriority_def numPriorities_def minBound_word) + by (clarsimp simp: makeObject_tcb makeObject_cte tcb_cte_cases_def minBound_word newArchTCB_def) lemma valid_obj_makeObject_endpoint [simp]: "valid_obj' (KOEndpoint makeObject) s" diff --git a/proof/refine/ARM_HYP/Schedule_R.thy b/proof/refine/ARM_HYP/Schedule_R.thy index 192694565..c40d91fea 100644 --- a/proof/refine/ARM_HYP/Schedule_R.thy +++ b/proof/refine/ARM_HYP/Schedule_R.thy @@ -1565,7 +1565,8 @@ lemma switchToIdleThread_curr_is_idle: lemma chooseThread_it[wp]: "\\s. P (ksIdleThread s)\ chooseThread \\_ s. P (ksIdleThread s)\" - by (wp|clarsimp simp: chooseThread_def curDomain_def numDomains_def bitmap_fun_defs|assumption)+ + supply if_split[split del] + by (wpsimp simp: chooseThread_def curDomain_def bitmap_fun_defs) lemma threadGet_inv [wp]: "\P\ threadGet f t \\rv. P\" apply (simp add: threadGet_def) @@ -1679,6 +1680,16 @@ lemma enumPrio_word_div: lemma curDomain_corres: "corres (=) \ \ (gets cur_domain) (curDomain)" by (simp add: curDomain_def state_relation_def) +lemma curDomain_corres': + "corres (=) \ (\s. ksCurDomain s \ maxDomain) + (gets cur_domain) (if 1 < numDomains then curDomain else return 0)" + apply (case_tac "1 < numDomains"; simp) + apply (rule corres_guard_imp[OF curDomain_corres]; solves simp) + (* if we have only one domain, then we are in it *) + apply (clarsimp simp: return_def simpler_gets_def bind_def maxDomain_def + state_relation_def corres_underlying_def) + done + lemma lookupBitmapPriority_Max_eqI: "\ valid_bitmapQ s ; bitmapQ_no_L1_orphans s ; ksReadyQueuesL1Bitmap s d \ 0 \ \ lookupBitmapPriority d s = (Max {prio. ksReadyQueues s (d, prio) \ []})" @@ -1745,18 +1756,27 @@ lemma ksReadyQueuesL1Bitmap_st_tcb_at': apply simp done +lemma curDomain_or_return_0: + "\ \P\ curDomain \\rv s. Q rv s \; \s. P s \ ksCurDomain s \ maxDomain \ + \ \P\ if 1 < numDomains then curDomain else return 0 \\rv s. Q rv s \" + apply (case_tac "1 < numDomains"; simp) + apply (simp add: valid_def curDomain_def simpler_gets_def return_def maxDomain_def) + done + +lemma invs_no_cicd_ksCurDomain_maxDomain': + "invs_no_cicd' s \ ksCurDomain s \ maxDomain" + unfolding invs_no_cicd'_def by simp + lemma chooseThread_corres: "corres dc (invs and valid_sched) (invs_no_cicd') choose_thread chooseThread" (is "corres _ ?PREI ?PREH _ _") proof - show ?thesis - unfolding choose_thread_def chooseThread_def numDomains_def - apply (simp only: numDomains_def return_bind Let_def) - apply (simp cong: if_cong) (* clean up if 1 < numDomains *) + unfolding choose_thread_def chooseThread_def + apply (simp only: return_bind Let_def) apply (subst if_swap[where P="_ \ 0"]) (* put switchToIdleThread on first branch*) - apply (rule corres_name_pre) apply (rule corres_guard_imp) - apply (rule corres_split_deprecated[OF _ curDomain_corres]) + apply (rule corres_split[OF curDomain_corres']) apply clarsimp apply (rule corres_split_deprecated[OF _ corres_gets_queues_getReadyQueuesL1Bitmap]) apply (erule corres_if2[OF sym]) @@ -1779,15 +1799,17 @@ proof - apply (wpsimp simp: getQueue_def getReadyQueuesL2Bitmap_def)+ apply (clarsimp simp: if_apply_def2) apply (wp hoare_vcg_conj_lift hoare_vcg_imp_lift ksReadyQueuesL1Bitmap_return_wp) - apply (simp add: curDomain_def, wp)+ + apply (wpsimp wp: curDomain_or_return_0 simp: curDomain_def)+ + apply (fastforce simp: invs_no_cicd'_def) apply (clarsimp simp: valid_sched_def DetSchedInvs_AI.valid_queues_def max_non_empty_queue_def) - apply (erule_tac x="cur_domain sa" in allE) - apply (erule_tac x="Max {prio. ready_queues sa (cur_domain sa) prio \ []}" in allE) - apply (case_tac "ready_queues sa (cur_domain sa) (Max {prio. ready_queues sa (cur_domain sa) prio \ []})") + apply (erule_tac x="cur_domain s" in allE) + apply (erule_tac x="Max {prio. ready_queues s (cur_domain s) prio \ []}" in allE) + apply (case_tac "ready_queues s (cur_domain s) (Max {prio. ready_queues s (cur_domain s) prio \ []})") apply (clarsimp) apply (subgoal_tac - "ready_queues sa (cur_domain sa) (Max {prio. ready_queues sa (cur_domain sa) prio \ []}) \ []") + "ready_queues s (cur_domain s) (Max {prio. ready_queues s (cur_domain s) prio \ []}) \ []") apply (fastforce elim!: setcomp_Max_has_prop)+ + apply (simp add: invs_no_cicd_ksCurDomain_maxDomain') apply (clarsimp dest!: invs_no_cicd'_queues) apply (fastforce intro: ksReadyQueuesL1Bitmap_st_tcb_at') done @@ -2192,9 +2214,15 @@ proof - note switchToThread_invs_no_cicd'[wp del] note switchToThread_lookupBitmapPriority_wp[wp] note assert_wp[wp del] + note if_split[split del] + + (* if we only have one domain, we are in it *) + have one_domain_case: + "\s. \ invs_no_cicd' s; numDomains \ 1 \ \ ksCurDomain s = 0" + by (simp add: all_invs_but_ct_idle_or_in_cur_domain'_def maxDomain_def) show ?thesis - unfolding chooseThread_def Let_def numDomains_def curDomain_def + unfolding chooseThread_def Let_def curDomain_def apply (simp only: return_bind, simp) apply (rule hoare_seq_ext[where B="\rv s. invs_no_cicd' s \ rv = ksCurDomain s"]) apply (rule_tac B="\rv s. invs_no_cicd' s \ curdom = ksCurDomain s \ @@ -2218,7 +2246,7 @@ proof - apply (drule (3) lookupBitmapPriority_obj_at') apply normalise_obj_at' apply (fastforce simp: tcb_in_cur_domain'_def inQ_def elim: obj_at'_weaken) - apply (wp | simp add: bitmap_fun_defs curDomain_def)+ + apply (wpsimp simp: bitmap_fun_defs curDomain_def one_domain_case)+ done qed @@ -2244,10 +2272,19 @@ proof - note switchToThread_invs_no_cicd'[wp del] note switchToThread_lookupBitmapPriority_wp[wp] note assert_wp[wp del] + note if_split[split del] + + (* if we only have one domain, we are in it *) + have one_domain_case: + "\s. \ invs_no_cicd' s; numDomains \ 1 \ \ ksCurDomain s = 0" + by (simp add: all_invs_but_ct_idle_or_in_cur_domain'_def maxDomain_def) + + (* NOTE: do *not* unfold numDomains in the rest of the proof, + it should work for any number *) (* FIXME this is almost identical to the chooseThread_invs_no_cicd'_posts proof, can generalise? *) show ?thesis - unfolding chooseThread_def Let_def numDomains_def curDomain_def + unfolding chooseThread_def Let_def curDomain_def apply (simp only: return_bind, simp) apply (rule hoare_seq_ext[where B="\rv s. invs_no_cicd' s \ rv = ksCurDomain s"]) apply (rule_tac B="\rv s. invs_no_cicd' s \ curdom = ksCurDomain s \ @@ -2261,7 +2298,7 @@ proof - apply (wp assert_inv) apply (clarsimp dest!: invs_no_cicd'_queues simp: valid_queues_def) apply (fastforce elim: bitmapQ_from_bitmap_lookup simp: lookupBitmapPriority_def) - apply (wp | simp add: bitmap_fun_defs curDomain_def)+ + apply (wpsimp simp: bitmap_fun_defs curDomain_def one_domain_case)+ done qed diff --git a/proof/refine/ARM_HYP/Syscall_R.thy b/proof/refine/ARM_HYP/Syscall_R.thy index 4101b04bf..543886b44 100644 --- a/proof/refine/ARM_HYP/Syscall_R.thy +++ b/proof/refine/ARM_HYP/Syscall_R.thy @@ -616,7 +616,7 @@ lemma dec_dom_inv_wf[wp]: apply (simp add:not_le) apply (simp del: Word.of_nat_unat flip: ucast_nat_def) apply (rule word_of_nat_le) - apply (simp add:numDomains_def maxDomain_def) + apply (simp add: le_maxDomain_eq_less_numDomains) done lemma decode_inv_wf'[wp]: diff --git a/proof/refine/RISCV64/Interrupt_R.thy b/proof/refine/RISCV64/Interrupt_R.thy index 690c8fd4c..be8367865 100644 --- a/proof/refine/RISCV64/Interrupt_R.thy +++ b/proof/refine/RISCV64/Interrupt_R.thy @@ -602,11 +602,6 @@ lemma getIRQState_prop: apply simp done -lemma num_domains[simp]: - "num_domains = numDomains" - apply(simp add: num_domains_def numDomains_def) - done - lemma decDomainTime_corres: "corres dc \ \ dec_domain_time decDomainTime" apply (simp add:dec_domain_time_def corres_underlying_def decDomainTime_def simpler_modify_def) @@ -795,17 +790,16 @@ crunches tcbSchedAppend lemma timerTick_invs'[wp]: "\invs'\ timerTick \\rv. invs'\" - apply (simp add: numDomains_def timerTick_def) - apply (wp threadSet_invs_trivial threadSet_pred_tcb_no_state - rescheduleRequired_all_invs_but_ct_not_inQ - tcbSchedAppend_invs_but_ct_not_inQ' - | simp add: tcb_cte_cases_def numDomains_def - | wpc)+ - apply (simp add:decDomainTime_def) - apply wp - apply simp + apply (simp add: timerTick_def) + apply (wpsimp wp: threadSet_invs_trivial threadSet_pred_tcb_no_state + rescheduleRequired_all_invs_but_ct_not_inQ + tcbSchedAppend_invs_but_ct_not_inQ' + simp: tcb_cte_cases_def) apply (rule_tac Q="\rv. invs'" in hoare_post_imp) apply (clarsimp simp add:invs'_def valid_state'_def) + apply (simp add: decDomainTime_def) + apply wp + apply simp apply wpc apply (wp add: threadGet_wp threadSet_cur threadSet_timeslice_invs rescheduleRequired_all_invs_but_ct_not_inQ @@ -817,7 +811,7 @@ lemma timerTick_invs'[wp]: threadSet_valid_objs' threadSet_timeslice_invs)+ apply (wp threadGet_wp) apply (wp gts_wp')+ - apply (clarsimp simp: invs'_def st_tcb_at'_def obj_at'_def valid_state'_def numDomains_def) + apply (clarsimp simp: invs'_def st_tcb_at'_def obj_at'_def valid_state'_def) done lemma resetTimer_invs'[wp]: diff --git a/proof/refine/RISCV64/Invariants_H.thy b/proof/refine/RISCV64/Invariants_H.thy index 56c6de163..51df0bb7e 100644 --- a/proof/refine/RISCV64/Invariants_H.thy +++ b/proof/refine/RISCV64/Invariants_H.thy @@ -2674,6 +2674,21 @@ lemma ex_cte_cap_to'_pres: apply simp done +section "Relationship of Executable Spec to Kernel Configuration" + +text \ + Some values are set per kernel configuration (e.g. number of domains), but other related + values (e.g. maximum domain) are derived from storage constraints (e.g. bytes used). + To relate the two, we must look at the values of kernel configuration constants. + To allow the proofs to work for all permitted values of these constants, their definitions + should only be unfolded in this section, and the derived properties kept to a minimum.\ + +lemma le_maxDomain_eq_less_numDomains: + shows "x \ unat maxDomain \ x < Kernel_Config.numDomains" + "y \ maxDomain \ unat y < Kernel_Config.numDomains" + by (auto simp: Kernel_Config.numDomains_def maxDomain_def word_le_nat_alt) + + context begin interpretation Arch . (*FIXME: arch_split*) lemma page_table_pte_atI': @@ -3243,4 +3258,4 @@ add_upd_simps "invs' (gsUntypedZeroRanges_update f s)" (obj_at'_real_def) declare upd_simps[simp] -end \ No newline at end of file +end diff --git a/proof/refine/RISCV64/Retype_R.thy b/proof/refine/RISCV64/Retype_R.thy index 39147ba39..48d155ed7 100644 --- a/proof/refine/RISCV64/Retype_R.thy +++ b/proof/refine/RISCV64/Retype_R.thy @@ -102,9 +102,7 @@ lemma valid_obj_makeObject_cte [simp]: lemma valid_obj_makeObject_tcb [simp]: "valid_obj' (KOTCB makeObject) s" unfolding valid_obj'_def valid_tcb'_def valid_tcb_state'_def - by (clarsimp simp: makeObject_tcb makeObject_cte cteSizeBits_def - tcb_cte_cases_def maxDomain_def numDomains_def maxPriority_def - numPriorities_def minBound_word) + by (clarsimp simp: makeObject_tcb makeObject_cte tcb_cte_cases_def minBound_word cteSizeBits_def) lemma valid_obj_makeObject_endpoint [simp]: "valid_obj' (KOEndpoint makeObject) s" diff --git a/proof/refine/RISCV64/Schedule_R.thy b/proof/refine/RISCV64/Schedule_R.thy index fadbf3b57..20de42668 100644 --- a/proof/refine/RISCV64/Schedule_R.thy +++ b/proof/refine/RISCV64/Schedule_R.thy @@ -1379,7 +1379,8 @@ lemma switchToIdleThread_curr_is_idle: lemma chooseThread_it[wp]: "\\s. P (ksIdleThread s)\ chooseThread \\_ s. P (ksIdleThread s)\" - by (wp|clarsimp simp: chooseThread_def curDomain_def numDomains_def bitmap_fun_defs|assumption)+ + supply if_split[split del] + by (wpsimp simp: chooseThread_def curDomain_def bitmap_fun_defs) lemma threadGet_inv [wp]: "\P\ threadGet f t \\rv. P\" apply (simp add: threadGet_def) @@ -1492,6 +1493,16 @@ lemma enumPrio_word_div: lemma curDomain_corres: "corres (=) \ \ (gets cur_domain) (curDomain)" by (simp add: curDomain_def state_relation_def) +lemma curDomain_corres': + "corres (=) \ (\s. ksCurDomain s \ maxDomain) + (gets cur_domain) (if 1 < numDomains then curDomain else return 0)" + apply (case_tac "1 < numDomains"; simp) + apply (rule corres_guard_imp[OF curDomain_corres]; solves simp) + (* if we have only one domain, then we are in it *) + apply (clarsimp simp: return_def simpler_gets_def bind_def maxDomain_def + state_relation_def corres_underlying_def) + done + lemma lookupBitmapPriority_Max_eqI: "\ valid_bitmapQ s ; bitmapQ_no_L1_orphans s ; ksReadyQueuesL1Bitmap s d \ 0 \ \ lookupBitmapPriority d s = (Max {prio. ksReadyQueues s (d, prio) \ []})" @@ -1558,18 +1569,27 @@ lemma ksReadyQueuesL1Bitmap_st_tcb_at': apply simp done +lemma curDomain_or_return_0: + "\ \P\ curDomain \\rv s. Q rv s \; \s. P s \ ksCurDomain s \ maxDomain \ + \ \P\ if 1 < numDomains then curDomain else return 0 \\rv s. Q rv s \" + apply (case_tac "1 < numDomains"; simp) + apply (simp add: valid_def curDomain_def simpler_gets_def return_def maxDomain_def) + done + +lemma invs_no_cicd_ksCurDomain_maxDomain': + "invs_no_cicd' s \ ksCurDomain s \ maxDomain" + unfolding invs_no_cicd'_def by simp + lemma chooseThread_corres: "corres dc (invs and valid_sched) (invs_no_cicd') choose_thread chooseThread" (is "corres _ ?PREI ?PREH _ _") proof - show ?thesis - unfolding choose_thread_def chooseThread_def numDomains_def - apply (simp only: numDomains_def return_bind Let_def) - apply (simp cong: if_cong) (* clean up if 1 < numDomains *) + unfolding choose_thread_def chooseThread_def + apply (simp only: return_bind Let_def) apply (subst if_swap[where P="_ \ 0"]) (* put switchToIdleThread on first branch*) - apply (rule corres_name_pre) apply (rule corres_guard_imp) - apply (rule corres_split_deprecated[OF _ curDomain_corres]) + apply (rule corres_split[OF curDomain_corres']) apply clarsimp apply (rule corres_split_deprecated[OF _ corres_gets_queues_getReadyQueuesL1Bitmap]) apply (erule corres_if2[OF sym]) @@ -1592,15 +1612,17 @@ proof - apply (wpsimp simp: getQueue_def getReadyQueuesL2Bitmap_def)+ apply (clarsimp simp: if_apply_def2) apply (wp hoare_vcg_conj_lift hoare_vcg_imp_lift ksReadyQueuesL1Bitmap_return_wp) - apply (simp add: curDomain_def, wp)+ + apply (wpsimp wp: curDomain_or_return_0 simp: curDomain_def)+ + apply (fastforce simp: invs_no_cicd'_def) apply (clarsimp simp: valid_sched_def DetSchedInvs_AI.valid_queues_def max_non_empty_queue_def) - apply (erule_tac x="cur_domain sa" in allE) - apply (erule_tac x="Max {prio. ready_queues sa (cur_domain sa) prio \ []}" in allE) - apply (case_tac "ready_queues sa (cur_domain sa) (Max {prio. ready_queues sa (cur_domain sa) prio \ []})") + apply (erule_tac x="cur_domain s" in allE) + apply (erule_tac x="Max {prio. ready_queues s (cur_domain s) prio \ []}" in allE) + apply (case_tac "ready_queues s (cur_domain s) (Max {prio. ready_queues s (cur_domain s) prio \ []})") apply (clarsimp) apply (subgoal_tac - "ready_queues sa (cur_domain sa) (Max {prio. ready_queues sa (cur_domain sa) prio \ []}) \ []") + "ready_queues s (cur_domain s) (Max {prio. ready_queues s (cur_domain s) prio \ []}) \ []") apply (fastforce elim!: setcomp_Max_has_prop)+ + apply (simp add: invs_no_cicd_ksCurDomain_maxDomain') apply (clarsimp dest!: invs_no_cicd'_queues) apply (fastforce intro: ksReadyQueuesL1Bitmap_st_tcb_at') done @@ -1999,9 +2021,15 @@ proof - note switchToThread_invs_no_cicd'[wp del] note switchToThread_lookupBitmapPriority_wp[wp] note assert_wp[wp del] + note if_split[split del] + + (* if we only have one domain, we are in it *) + have one_domain_case: + "\s. \ invs_no_cicd' s; numDomains \ 1 \ \ ksCurDomain s = 0" + by (simp add: all_invs_but_ct_idle_or_in_cur_domain'_def maxDomain_def) show ?thesis - unfolding chooseThread_def Let_def numDomains_def curDomain_def + unfolding chooseThread_def Let_def curDomain_def apply (simp only: return_bind, simp) apply (rule hoare_seq_ext[where B="\rv s. invs_no_cicd' s \ rv = ksCurDomain s"]) apply (rule_tac B="\rv s. invs_no_cicd' s \ curdom = ksCurDomain s \ @@ -2025,7 +2053,7 @@ proof - apply (drule (3) lookupBitmapPriority_obj_at') apply normalise_obj_at' apply (fastforce simp: tcb_in_cur_domain'_def inQ_def elim: obj_at'_weaken) - apply (wp | simp add: bitmap_fun_defs curDomain_def)+ + apply (wpsimp simp: bitmap_fun_defs curDomain_def one_domain_case)+ done qed @@ -2051,10 +2079,19 @@ proof - note switchToThread_invs_no_cicd'[wp del] note switchToThread_lookupBitmapPriority_wp[wp] note assert_wp[wp del] + note if_split[split del] + + (* if we only have one domain, we are in it *) + have one_domain_case: + "\s. \ invs_no_cicd' s; numDomains \ 1 \ \ ksCurDomain s = 0" + by (simp add: all_invs_but_ct_idle_or_in_cur_domain'_def maxDomain_def) + + (* NOTE: do *not* unfold numDomains in the rest of the proof, + it should work for any number *) (* FIXME this is almost identical to the chooseThread_invs_no_cicd'_posts proof, can generalise? *) show ?thesis - unfolding chooseThread_def Let_def numDomains_def curDomain_def + unfolding chooseThread_def Let_def curDomain_def apply (simp only: return_bind, simp) apply (rule hoare_seq_ext[where B="\rv s. invs_no_cicd' s \ rv = ksCurDomain s"]) apply (rule_tac B="\rv s. invs_no_cicd' s \ curdom = ksCurDomain s \ @@ -2068,7 +2105,7 @@ proof - apply (wp assert_inv) apply (clarsimp dest!: invs_no_cicd'_queues simp: valid_queues_def) apply (fastforce elim: bitmapQ_from_bitmap_lookup simp: lookupBitmapPriority_def) - apply (wp | simp add: bitmap_fun_defs curDomain_def)+ + apply (wpsimp simp: bitmap_fun_defs curDomain_def one_domain_case)+ done qed diff --git a/proof/refine/RISCV64/Syscall_R.thy b/proof/refine/RISCV64/Syscall_R.thy index 1c8fc384c..c5fb661ab 100644 --- a/proof/refine/RISCV64/Syscall_R.thy +++ b/proof/refine/RISCV64/Syscall_R.thy @@ -613,7 +613,7 @@ lemma dec_dom_inv_wf[wp]: apply (simp add:not_le) apply (simp del: Word.of_nat_unat flip: ucast_nat_def) apply (rule word_of_nat_le) - apply (simp add:numDomains_def maxDomain_def) + apply (simp add: le_maxDomain_eq_less_numDomains) done lemma decode_inv_wf'[wp]: diff --git a/proof/refine/RISCV64/orphanage/Orphanage.thy b/proof/refine/RISCV64/orphanage/Orphanage.thy index 7a2365b2f..bb0d05317 100644 --- a/proof/refine/RISCV64/orphanage/Orphanage.thy +++ b/proof/refine/RISCV64/orphanage/Orphanage.thy @@ -783,7 +783,8 @@ lemma chooseThread_no_orphans [wp]: chooseThread \ \rv s. no_orphans s \" (is "\?PRE\ _ \_\") - unfolding chooseThread_def Let_def numDomains_def curDomain_def + unfolding chooseThread_def Let_def + supply if_split[split del] apply (simp only: return_bind, simp) apply (rule hoare_seq_ext[where B="\rv s. ?PRE s \ rv = ksCurDomain s"]) apply (rule_tac B="\rv s. ?PRE s \ curdom = ksCurDomain s \ @@ -799,7 +800,9 @@ lemma chooseThread_no_orphans [wp]: valid_queues_def st_tcb_at'_def) apply (fastforce dest!: lookupBitmapPriority_obj_at' elim: obj_at'_weaken simp: all_active_tcb_ptrs_def) - apply (simp add: bitmap_fun_defs | wp)+ + apply (wpsimp simp: bitmap_fun_defs) + apply (wp curDomain_or_return_0[simplified]) + apply (wpsimp simp: curDomain_def simp: invs_no_cicd_ksCurDomain_maxDomain')+ done lemma valid_queues'_ko_atD: @@ -1024,7 +1027,8 @@ lemma chooseThread_nosch: "\\s. P (ksSchedulerAction s)\ chooseThread \\rv s. P (ksSchedulerAction s)\" - unfolding chooseThread_def Let_def numDomains_def curDomain_def + unfolding chooseThread_def Let_def curDomain_def + supply if_split[split del] apply (simp only: return_bind, simp) apply (wp findM_inv | simp)+ apply (case_tac queue) @@ -1243,18 +1247,20 @@ lemma timerTick_no_orphans [wp]: "\ \s. no_orphans s \ invs' s \ timerTick \ \_ s. no_orphans s \" - unfolding timerTick_def getDomainTime_def numDomains_def - apply (rule hoare_pre) - apply (wp hoare_drop_imps | clarsimp)+ - apply (wp threadSet_valid_queues' tcbSchedAppend_almost_no_orphans threadSet_sch_act - threadSet_almost_no_orphans threadSet_no_orphans tcbSchedAppend_sch_act_wf - | wpc | clarsimp - | strengthen sch_act_wf_weak)+ - apply (rule_tac Q="\rv s. no_orphans s \ valid_queues' s \ tcb_at' thread s - \ sch_act_wf (ksSchedulerAction s) s" in hoare_post_imp) - apply (clarsimp simp: inQ_def) - apply (wp hoare_drop_imps | clarsimp)+ - apply auto + unfolding timerTick_def getDomainTime_def + supply if_split[split del] + apply (subst threadState_case_if) + apply (wpsimp wp: threadSet_no_orphans threadSet_valid_queues' + threadSet_valid_queues' tcbSchedAppend_almost_no_orphans threadSet_sch_act + threadSet_almost_no_orphans threadSet_no_orphans tcbSchedAppend_sch_act_wf + hoare_drop_imp + simp: if_apply_def2 + | strengthen sch_act_wf_weak)+ + apply (rule_tac Q="\rv s. no_orphans s \ valid_queues' s \ tcb_at' thread s + \ sch_act_wf (ksSchedulerAction s) s" in hoare_post_imp) + apply (clarsimp simp: inQ_def) + apply (wp hoare_drop_imps | clarsimp)+ + apply (auto split: if_split) done diff --git a/proof/refine/X64/Interrupt_R.thy b/proof/refine/X64/Interrupt_R.thy index d8d6f8d41..42b82a634 100644 --- a/proof/refine/X64/Interrupt_R.thy +++ b/proof/refine/X64/Interrupt_R.thy @@ -651,11 +651,6 @@ lemma getIRQState_prop: apply simp done -lemma num_domains[simp]: - "num_domains = numDomains" - apply(simp add: num_domains_def numDomains_def) - done - lemma decDomainTime_corres: "corres dc \ \ dec_domain_time decDomainTime" apply (simp add:dec_domain_time_def corres_underlying_def @@ -865,17 +860,16 @@ crunch cur_tcb'[wp]: tcbSchedAppend cur_tcb' lemma timerTick_invs'[wp]: "\invs'\ timerTick \\rv. invs'\" - apply (simp add: numDomains_def timerTick_def) - apply (wp threadSet_invs_trivial threadSet_pred_tcb_no_state - rescheduleRequired_all_invs_but_ct_not_inQ - tcbSchedAppend_invs_but_ct_not_inQ' - | simp add: tcb_cte_cases_def numDomains_def - | wpc)+ - apply (simp add:decDomainTime_def) - apply wp - apply simp + apply (simp add: timerTick_def) + apply (wpsimp wp: threadSet_invs_trivial threadSet_pred_tcb_no_state + rescheduleRequired_all_invs_but_ct_not_inQ + tcbSchedAppend_invs_but_ct_not_inQ' + simp: tcb_cte_cases_def) apply (rule_tac Q="\rv. invs'" in hoare_post_imp) apply (clarsimp simp add:invs'_def valid_state'_def) + apply (simp add: decDomainTime_def) + apply wp + apply simp apply wpc apply (wp add: threadGet_wp threadSet_cur threadSet_timeslice_invs rescheduleRequired_all_invs_but_ct_not_inQ @@ -887,7 +881,7 @@ lemma timerTick_invs'[wp]: threadSet_valid_objs' threadSet_timeslice_invs)+ apply (wp threadGet_wp) apply (wp gts_wp')+ - apply (clarsimp simp: invs'_def st_tcb_at'_def obj_at'_def valid_state'_def numDomains_def) + apply (clarsimp simp: invs'_def st_tcb_at'_def obj_at'_def valid_state'_def) done lemma resetTimer_invs'[wp]: diff --git a/proof/refine/X64/Invariants_H.thy b/proof/refine/X64/Invariants_H.thy index 54e56c08f..aef5c0a69 100644 --- a/proof/refine/X64/Invariants_H.thy +++ b/proof/refine/X64/Invariants_H.thy @@ -31,6 +31,21 @@ end end +section "Relationship of Executable Spec to Kernel Configuration" + +text \ + Some values are set per kernel configuration (e.g. number of domains), but other related + values (e.g. maximum domain) are derived from storage constraints (e.g. bytes used). + To relate the two, we must look at the values of kernel configuration constants. + To allow the proofs to work for all permitted values of these constants, their definitions + should only be unfolded in this section, and the derived properties kept to a minimum.\ + +lemma le_maxDomain_eq_less_numDomains: + shows "x \ unat maxDomain \ x < Kernel_Config.numDomains" + "y \ maxDomain \ unat y < Kernel_Config.numDomains" + by (auto simp: Kernel_Config.numDomains_def maxDomain_def word_le_nat_alt) + + context begin interpretation Arch . (*FIXME: arch_split*) \ \---------------------------------------------------------------------------\ section "Invariants on Executable Spec" diff --git a/proof/refine/X64/Retype_R.thy b/proof/refine/X64/Retype_R.thy index d149064e6..b934a932a 100644 --- a/proof/refine/X64/Retype_R.thy +++ b/proof/refine/X64/Retype_R.thy @@ -111,8 +111,7 @@ lemma valid_obj_makeObject_cte [simp]: lemma valid_obj_makeObject_tcb [simp]: "valid_obj' (KOTCB makeObject) s" unfolding valid_obj'_def valid_tcb'_def valid_tcb_state'_def - by (clarsimp simp: makeObject_tcb makeObject_cte - tcb_cte_cases_def maxDomain_def numDomains_def maxPriority_def numPriorities_def minBound_word) + by (clarsimp simp: makeObject_tcb makeObject_cte tcb_cte_cases_def minBound_word) lemma valid_obj_makeObject_endpoint [simp]: "valid_obj' (KOEndpoint makeObject) s" diff --git a/proof/refine/X64/Schedule_R.thy b/proof/refine/X64/Schedule_R.thy index de763e1d3..68b396730 100644 --- a/proof/refine/X64/Schedule_R.thy +++ b/proof/refine/X64/Schedule_R.thy @@ -1399,7 +1399,8 @@ lemma switchToIdleThread_curr_is_idle: lemma chooseThread_it[wp]: "\\s. P (ksIdleThread s)\ chooseThread \\_ s. P (ksIdleThread s)\" - by (wp|clarsimp simp: chooseThread_def curDomain_def numDomains_def bitmap_fun_defs|assumption)+ + supply if_split[split del] + by (wpsimp simp: chooseThread_def curDomain_def bitmap_fun_defs) lemma threadGet_inv [wp]: "\P\ threadGet f t \\rv. P\" apply (simp add: threadGet_def) @@ -1513,6 +1514,16 @@ lemma enumPrio_word_div: lemma curDomain_corres: "corres (=) \ \ (gets cur_domain) (curDomain)" by (simp add: curDomain_def state_relation_def) +lemma curDomain_corres': + "corres (=) \ (\s. ksCurDomain s \ maxDomain) + (gets cur_domain) (if 1 < numDomains then curDomain else return 0)" + apply (case_tac "1 < numDomains"; simp) + apply (rule corres_guard_imp[OF curDomain_corres]; solves simp) + (* if we have only one domain, then we are in it *) + apply (clarsimp simp: return_def simpler_gets_def bind_def maxDomain_def + state_relation_def corres_underlying_def) + done + lemma lookupBitmapPriority_Max_eqI: "\ valid_bitmapQ s ; bitmapQ_no_L1_orphans s ; ksReadyQueuesL1Bitmap s d \ 0 \ \ lookupBitmapPriority d s = (Max {prio. ksReadyQueues s (d, prio) \ []})" @@ -1579,18 +1590,27 @@ lemma ksReadyQueuesL1Bitmap_st_tcb_at': apply simp done +lemma curDomain_or_return_0: + "\ \P\ curDomain \\rv s. Q rv s \; \s. P s \ ksCurDomain s \ maxDomain \ + \ \P\ if 1 < numDomains then curDomain else return 0 \\rv s. Q rv s \" + apply (case_tac "1 < numDomains"; simp) + apply (simp add: valid_def curDomain_def simpler_gets_def return_def maxDomain_def) + done + +lemma invs_no_cicd_ksCurDomain_maxDomain': + "invs_no_cicd' s \ ksCurDomain s \ maxDomain" + unfolding invs_no_cicd'_def by simp + lemma chooseThread_corres: "corres dc (invs and valid_sched) (invs_no_cicd') choose_thread chooseThread" (is "corres _ ?PREI ?PREH _ _") proof - show ?thesis - unfolding choose_thread_def chooseThread_def numDomains_def - apply (simp only: numDomains_def return_bind Let_def) - apply (simp cong: if_cong) (* clean up if 1 < numDomains *) + unfolding choose_thread_def chooseThread_def + apply (simp only: return_bind Let_def) apply (subst if_swap[where P="_ \ 0"]) (* put switchToIdleThread on first branch*) - apply (rule corres_name_pre) apply (rule corres_guard_imp) - apply (rule corres_split_deprecated[OF _ curDomain_corres]) + apply (rule corres_split[OF curDomain_corres']) apply clarsimp apply (rule corres_split_deprecated[OF _ corres_gets_queues_getReadyQueuesL1Bitmap]) apply (erule corres_if2[OF sym]) @@ -1613,15 +1633,17 @@ proof - apply (wpsimp simp: getQueue_def getReadyQueuesL2Bitmap_def)+ apply (clarsimp simp: if_apply_def2) apply (wp hoare_vcg_conj_lift hoare_vcg_imp_lift ksReadyQueuesL1Bitmap_return_wp) - apply (simp add: curDomain_def, wp)+ + apply (wpsimp wp: curDomain_or_return_0 simp: curDomain_def)+ + apply (fastforce simp: invs_no_cicd'_def) apply (clarsimp simp: valid_sched_def DetSchedInvs_AI.valid_queues_def max_non_empty_queue_def) - apply (erule_tac x="cur_domain sa" in allE) - apply (erule_tac x="Max {prio. ready_queues sa (cur_domain sa) prio \ []}" in allE) - apply (case_tac "ready_queues sa (cur_domain sa) (Max {prio. ready_queues sa (cur_domain sa) prio \ []})") + apply (erule_tac x="cur_domain s" in allE) + apply (erule_tac x="Max {prio. ready_queues s (cur_domain s) prio \ []}" in allE) + apply (case_tac "ready_queues s (cur_domain s) (Max {prio. ready_queues s (cur_domain s) prio \ []})") apply (clarsimp) apply (subgoal_tac - "ready_queues sa (cur_domain sa) (Max {prio. ready_queues sa (cur_domain sa) prio \ []}) \ []") + "ready_queues s (cur_domain s) (Max {prio. ready_queues s (cur_domain s) prio \ []}) \ []") apply (fastforce elim!: setcomp_Max_has_prop)+ + apply (simp add: invs_no_cicd_ksCurDomain_maxDomain') apply (clarsimp dest!: invs_no_cicd'_queues) apply (fastforce intro: ksReadyQueuesL1Bitmap_st_tcb_at') done @@ -2023,9 +2045,15 @@ proof - note switchToThread_invs_no_cicd'[wp del] note switchToThread_lookupBitmapPriority_wp[wp] note assert_wp[wp del] + note if_split[split del] + + (* if we only have one domain, we are in it *) + have one_domain_case: + "\s. \ invs_no_cicd' s; numDomains \ 1 \ \ ksCurDomain s = 0" + by (simp add: all_invs_but_ct_idle_or_in_cur_domain'_def maxDomain_def) show ?thesis - unfolding chooseThread_def Let_def numDomains_def curDomain_def + unfolding chooseThread_def Let_def curDomain_def apply (simp only: return_bind, simp) apply (rule hoare_seq_ext[where B="\rv s. invs_no_cicd' s \ rv = ksCurDomain s"]) apply (rule_tac B="\rv s. invs_no_cicd' s \ curdom = ksCurDomain s \ @@ -2049,7 +2077,7 @@ proof - apply (drule (3) lookupBitmapPriority_obj_at') apply normalise_obj_at' apply (fastforce simp: tcb_in_cur_domain'_def inQ_def elim: obj_at'_weaken) - apply (wp | simp add: bitmap_fun_defs curDomain_def)+ + apply (wpsimp simp: bitmap_fun_defs curDomain_def one_domain_case)+ done qed @@ -2075,10 +2103,19 @@ proof - note switchToThread_invs_no_cicd'[wp del] note switchToThread_lookupBitmapPriority_wp[wp] note assert_wp[wp del] + note if_split[split del] + + (* if we only have one domain, we are in it *) + have one_domain_case: + "\s. \ invs_no_cicd' s; numDomains \ 1 \ \ ksCurDomain s = 0" + by (simp add: all_invs_but_ct_idle_or_in_cur_domain'_def maxDomain_def) + + (* NOTE: do *not* unfold numDomains in the rest of the proof, + it should work for any number *) (* FIXME this is almost identical to the chooseThread_invs_no_cicd'_posts proof, can generalise? *) show ?thesis - unfolding chooseThread_def Let_def numDomains_def curDomain_def + unfolding chooseThread_def Let_def curDomain_def apply (simp only: return_bind, simp) apply (rule hoare_seq_ext[where B="\rv s. invs_no_cicd' s \ rv = ksCurDomain s"]) apply (rule_tac B="\rv s. invs_no_cicd' s \ curdom = ksCurDomain s \ @@ -2092,7 +2129,7 @@ proof - apply (wp assert_inv) apply (clarsimp dest!: invs_no_cicd'_queues simp: valid_queues_def) apply (fastforce elim: bitmapQ_from_bitmap_lookup simp: lookupBitmapPriority_def) - apply (wp | simp add: bitmap_fun_defs curDomain_def)+ + apply (wpsimp simp: bitmap_fun_defs curDomain_def one_domain_case)+ done qed diff --git a/proof/refine/X64/Syscall_R.thy b/proof/refine/X64/Syscall_R.thy index d9c29239a..d6873c95e 100644 --- a/proof/refine/X64/Syscall_R.thy +++ b/proof/refine/X64/Syscall_R.thy @@ -616,7 +616,7 @@ lemma dec_dom_inv_wf[wp]: apply (simp add:not_le) apply (simp del: Word.of_nat_unat flip: ucast_nat_def) apply (rule word_of_nat_le) - apply (simp add:numDomains_def maxDomain_def) + apply (simp add: le_maxDomain_eq_less_numDomains) done lemma decode_inv_wf'[wp]: