adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

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 <rafal.kolanski@proofcraft.systems>
This commit is contained in:
Rafal Kolanski 2021-06-08 21:33:00 +10:00 committed by Rafal Kolanski
parent 8052df4ac6
commit b8fc709d21
22 changed files with 356 additions and 164 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

24
proof/refine/ARM/Interrupt_R.thy
View File

@ -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 \<top> \<top> 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]:
"\<lbrace>invs'\<rbrace> timerTick \<lbrace>\<lambda>rv. invs'\<rbrace>"
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="\<lambda>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]:

16
proof/refine/ARM/Invariants_H.thy
View File

@ -31,6 +31,21 @@ end
end
section "Relationship of Executable Spec to Kernel Configuration"
text \<open>
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.\<close>
lemma le_maxDomain_eq_less_numDomains:
shows "x \<le> unat maxDomain \<longleftrightarrow> x < Kernel_Config.numDomains"
"y \<le> maxDomain \<longleftrightarrow> 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*)
\<comment> \<open>---------------------------------------------------------------------------\<close>
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

3
proof/refine/ARM/Retype_R.thy
View File

@ -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"

70
proof/refine/ARM/Schedule_R.thy
View File

@ -1415,7 +1415,8 @@ lemma switchToIdleThread_curr_is_idle:
lemma chooseThread_it[wp]:
"\<lbrace>\<lambda>s. P (ksIdleThread s)\<rbrace> chooseThread \<lbrace>\<lambda>_ s. P (ksIdleThread s)\<rbrace>"
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]: "\<lbrace>P\<rbrace> threadGet f t \<lbrace>\<lambda>rv. P\<rbrace>"
apply (simp add: threadGet_def)
@ -1503,6 +1504,16 @@ abbreviation "enumPrio \<equiv> [0.e.maxPriority]"
lemma curDomain_corres: "corres (=) \<top> \<top> (gets cur_domain) (curDomain)"
by (simp add: curDomain_def state_relation_def)
lemma curDomain_corres':
"corres (=) \<top> (\<lambda>s. ksCurDomain s \<le> 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:
"\<lbrakk> valid_bitmapQ s ; bitmapQ_no_L1_orphans s ; ksReadyQueuesL1Bitmap s d \<noteq> 0 \<rbrakk>
\<Longrightarrow> lookupBitmapPriority d s = (Max {prio. ksReadyQueues s (d, prio) \<noteq> []})"
@ -1569,18 +1580,27 @@ lemma ksReadyQueuesL1Bitmap_st_tcb_at':
apply simp
done
lemma curDomain_or_return_0:
"\<lbrakk> \<lbrace>P\<rbrace> curDomain \<lbrace>\<lambda>rv s. Q rv s \<rbrace>; \<And>s. P s \<Longrightarrow> ksCurDomain s \<le> maxDomain \<rbrakk>
\<Longrightarrow> \<lbrace>P\<rbrace> if 1 < numDomains then curDomain else return 0 \<lbrace>\<lambda>rv s. Q rv s \<rbrace>"
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 \<Longrightarrow> ksCurDomain s \<le> 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="_ \<noteq> 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 \<noteq> []}" in allE)
apply (case_tac "ready_queues sa (cur_domain sa) (Max {prio. ready_queues sa (cur_domain sa) prio \<noteq> []})")
apply (erule_tac x="cur_domain s" in allE)
apply (erule_tac x="Max {prio. ready_queues s (cur_domain s) prio \<noteq> []}" in allE)
apply (case_tac "ready_queues s (cur_domain s) (Max {prio. ready_queues s (cur_domain s) prio \<noteq> []})")
apply (clarsimp)
apply (subgoal_tac
"ready_queues sa (cur_domain sa) (Max {prio. ready_queues sa (cur_domain sa) prio \<noteq> []}) \<noteq> []")
"ready_queues s (cur_domain s) (Max {prio. ready_queues s (cur_domain s) prio \<noteq> []}) \<noteq> []")
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:
"\<And>s. \<lbrakk> invs_no_cicd' s; numDomains \<le> 1 \<rbrakk> \<Longrightarrow> 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="\<lambda>rv s. invs_no_cicd' s \<and> rv = ksCurDomain s"])
apply (rule_tac B="\<lambda>rv s. invs_no_cicd' s \<and> curdom = ksCurDomain s \<and>
@ -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:
"\<And>s. \<lbrakk> invs_no_cicd' s; numDomains \<le> 1 \<rbrakk> \<Longrightarrow> 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="\<lambda>rv s. invs_no_cicd' s \<and> rv = ksCurDomain s"])
apply (rule_tac B="\<lambda>rv s. invs_no_cicd' s \<and> curdom = ksCurDomain s \<and>
@ -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:
"\<lbrace>\<lambda>s. P (ksSchedulerAction s)\<rbrace>
chooseThread
\<lbrace>\<lambda>rv s. P (ksSchedulerAction s)\<rbrace>"
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)

2
proof/refine/ARM/Syscall_R.thy
View File

@ -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]:

33
proof/refine/ARM/orphanage/Orphanage.thy
View File

@ -795,7 +795,8 @@ lemma chooseThread_no_orphans [wp]:
chooseThread
\<lbrace> \<lambda>rv s. no_orphans s \<rbrace>"
(is "\<lbrace>?PRE\<rbrace> _ \<lbrace>_\<rbrace>")
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="\<lambda>rv s. ?PRE s \<and> rv = ksCurDomain s"])
apply (rule_tac B="\<lambda>rv s. ?PRE s \<and> curdom = ksCurDomain s \<and>
@ -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]:
"\<lbrace> \<lambda>s. no_orphans s \<and> invs' s \<rbrace>
timerTick
\<lbrace> \<lambda>_ s. no_orphans s \<rbrace>"
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="\<lambda>rv s. no_orphans s \<and> valid_queues' s \<and> tcb_at' thread s
\<and> 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="\<lambda>rv s. no_orphans s \<and> valid_queues' s \<and> tcb_at' thread s
\<and> 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

24
proof/refine/ARM_HYP/Interrupt_R.thy
View File

@ -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 \<top> \<top> 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]:
"\<lbrace>invs'\<rbrace> timerTick \<lbrace>\<lambda>rv. invs'\<rbrace>"
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="\<lambda>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]:

15
proof/refine/ARM_HYP/Invariants_H.thy
View File

@ -31,6 +31,21 @@ end
end
section "Relationship of Executable Spec to Kernel Configuration"
text \<open>
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.\<close>
lemma le_maxDomain_eq_less_numDomains:
shows "x \<le> unat maxDomain \<longleftrightarrow> x < Kernel_Config.numDomains"
"y \<le> maxDomain \<longleftrightarrow> 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*)
\<comment> \<open>---------------------------------------------------------------------------\<close>
section "Invariants on Executable Spec"

3
proof/refine/ARM_HYP/Retype_R.thy
View File

@ -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"

67
proof/refine/ARM_HYP/Schedule_R.thy
View File

@ -1565,7 +1565,8 @@ lemma switchToIdleThread_curr_is_idle:
lemma chooseThread_it[wp]:
"\<lbrace>\<lambda>s. P (ksIdleThread s)\<rbrace> chooseThread \<lbrace>\<lambda>_ s. P (ksIdleThread s)\<rbrace>"
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]: "\<lbrace>P\<rbrace> threadGet f t \<lbrace>\<lambda>rv. P\<rbrace>"
apply (simp add: threadGet_def)
@ -1679,6 +1680,16 @@ lemma enumPrio_word_div:
lemma curDomain_corres: "corres (=) \<top> \<top> (gets cur_domain) (curDomain)"
by (simp add: curDomain_def state_relation_def)
lemma curDomain_corres':
"corres (=) \<top> (\<lambda>s. ksCurDomain s \<le> 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:
"\<lbrakk> valid_bitmapQ s ; bitmapQ_no_L1_orphans s ; ksReadyQueuesL1Bitmap s d \<noteq> 0 \<rbrakk>
\<Longrightarrow> lookupBitmapPriority d s = (Max {prio. ksReadyQueues s (d, prio) \<noteq> []})"
@ -1745,18 +1756,27 @@ lemma ksReadyQueuesL1Bitmap_st_tcb_at':
apply simp
done
lemma curDomain_or_return_0:
"\<lbrakk> \<lbrace>P\<rbrace> curDomain \<lbrace>\<lambda>rv s. Q rv s \<rbrace>; \<And>s. P s \<Longrightarrow> ksCurDomain s \<le> maxDomain \<rbrakk>
\<Longrightarrow> \<lbrace>P\<rbrace> if 1 < numDomains then curDomain else return 0 \<lbrace>\<lambda>rv s. Q rv s \<rbrace>"
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 \<Longrightarrow> ksCurDomain s \<le> 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="_ \<noteq> 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 \<noteq> []}" in allE)
apply (case_tac "ready_queues sa (cur_domain sa) (Max {prio. ready_queues sa (cur_domain sa) prio \<noteq> []})")
apply (erule_tac x="cur_domain s" in allE)
apply (erule_tac x="Max {prio. ready_queues s (cur_domain s) prio \<noteq> []}" in allE)
apply (case_tac "ready_queues s (cur_domain s) (Max {prio. ready_queues s (cur_domain s) prio \<noteq> []})")
apply (clarsimp)
apply (subgoal_tac
"ready_queues sa (cur_domain sa) (Max {prio. ready_queues sa (cur_domain sa) prio \<noteq> []}) \<noteq> []")
"ready_queues s (cur_domain s) (Max {prio. ready_queues s (cur_domain s) prio \<noteq> []}) \<noteq> []")
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:
"\<And>s. \<lbrakk> invs_no_cicd' s; numDomains \<le> 1 \<rbrakk> \<Longrightarrow> 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="\<lambda>rv s. invs_no_cicd' s \<and> rv = ksCurDomain s"])
apply (rule_tac B="\<lambda>rv s. invs_no_cicd' s \<and> curdom = ksCurDomain s \<and>
@ -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:
"\<And>s. \<lbrakk> invs_no_cicd' s; numDomains \<le> 1 \<rbrakk> \<Longrightarrow> 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="\<lambda>rv s. invs_no_cicd' s \<and> rv = ksCurDomain s"])
apply (rule_tac B="\<lambda>rv s. invs_no_cicd' s \<and> curdom = ksCurDomain s \<and>
@ -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

2
proof/refine/ARM_HYP/Syscall_R.thy
View File

@ -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]:

24
proof/refine/RISCV64/Interrupt_R.thy
View File

@ -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 \<top> \<top> 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]:
"\<lbrace>invs'\<rbrace> timerTick \<lbrace>\<lambda>rv. invs'\<rbrace>"
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="\<lambda>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]:

17
proof/refine/RISCV64/Invariants_H.thy
View File

@ -2674,6 +2674,21 @@ lemma ex_cte_cap_to'_pres:
apply simp
done
section "Relationship of Executable Spec to Kernel Configuration"
text \<open>
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.\<close>
lemma le_maxDomain_eq_less_numDomains:
shows "x \<le> unat maxDomain \<longleftrightarrow> x < Kernel_Config.numDomains"
"y \<le> maxDomain \<longleftrightarrow> 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
end

4
proof/refine/RISCV64/Retype_R.thy
View File

@ -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"

67
proof/refine/RISCV64/Schedule_R.thy
View File

@ -1379,7 +1379,8 @@ lemma switchToIdleThread_curr_is_idle:
lemma chooseThread_it[wp]:
"\<lbrace>\<lambda>s. P (ksIdleThread s)\<rbrace> chooseThread \<lbrace>\<lambda>_ s. P (ksIdleThread s)\<rbrace>"
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]: "\<lbrace>P\<rbrace> threadGet f t \<lbrace>\<lambda>rv. P\<rbrace>"
apply (simp add: threadGet_def)
@ -1492,6 +1493,16 @@ lemma enumPrio_word_div:
lemma curDomain_corres: "corres (=) \<top> \<top> (gets cur_domain) (curDomain)"
by (simp add: curDomain_def state_relation_def)
lemma curDomain_corres':
"corres (=) \<top> (\<lambda>s. ksCurDomain s \<le> 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:
"\<lbrakk> valid_bitmapQ s ; bitmapQ_no_L1_orphans s ; ksReadyQueuesL1Bitmap s d \<noteq> 0 \<rbrakk>
\<Longrightarrow> lookupBitmapPriority d s = (Max {prio. ksReadyQueues s (d, prio) \<noteq> []})"
@ -1558,18 +1569,27 @@ lemma ksReadyQueuesL1Bitmap_st_tcb_at':
apply simp
done
lemma curDomain_or_return_0:
"\<lbrakk> \<lbrace>P\<rbrace> curDomain \<lbrace>\<lambda>rv s. Q rv s \<rbrace>; \<And>s. P s \<Longrightarrow> ksCurDomain s \<le> maxDomain \<rbrakk>
\<Longrightarrow> \<lbrace>P\<rbrace> if 1 < numDomains then curDomain else return 0 \<lbrace>\<lambda>rv s. Q rv s \<rbrace>"
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 \<Longrightarrow> ksCurDomain s \<le> 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="_ \<noteq> 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 \<noteq> []}" in allE)
apply (case_tac "ready_queues sa (cur_domain sa) (Max {prio. ready_queues sa (cur_domain sa) prio \<noteq> []})")
apply (erule_tac x="cur_domain s" in allE)
apply (erule_tac x="Max {prio. ready_queues s (cur_domain s) prio \<noteq> []}" in allE)
apply (case_tac "ready_queues s (cur_domain s) (Max {prio. ready_queues s (cur_domain s) prio \<noteq> []})")
apply (clarsimp)
apply (subgoal_tac
"ready_queues sa (cur_domain sa) (Max {prio. ready_queues sa (cur_domain sa) prio \<noteq> []}) \<noteq> []")
"ready_queues s (cur_domain s) (Max {prio. ready_queues s (cur_domain s) prio \<noteq> []}) \<noteq> []")
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:
"\<And>s. \<lbrakk> invs_no_cicd' s; numDomains \<le> 1 \<rbrakk> \<Longrightarrow> 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="\<lambda>rv s. invs_no_cicd' s \<and> rv = ksCurDomain s"])
apply (rule_tac B="\<lambda>rv s. invs_no_cicd' s \<and> curdom = ksCurDomain s \<and>
@ -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:
"\<And>s. \<lbrakk> invs_no_cicd' s; numDomains \<le> 1 \<rbrakk> \<Longrightarrow> 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="\<lambda>rv s. invs_no_cicd' s \<and> rv = ksCurDomain s"])
apply (rule_tac B="\<lambda>rv s. invs_no_cicd' s \<and> curdom = ksCurDomain s \<and>
@ -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

2
proof/refine/RISCV64/Syscall_R.thy
View File

@ -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]:

36
proof/refine/RISCV64/orphanage/Orphanage.thy
View File

@ -783,7 +783,8 @@ lemma chooseThread_no_orphans [wp]:
chooseThread
\<lbrace> \<lambda>rv s. no_orphans s \<rbrace>"
(is "\<lbrace>?PRE\<rbrace> _ \<lbrace>_\<rbrace>")
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="\<lambda>rv s. ?PRE s \<and> rv = ksCurDomain s"])
apply (rule_tac B="\<lambda>rv s. ?PRE s \<and> curdom = ksCurDomain s \<and>
@ -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:
"\<lbrace>\<lambda>s. P (ksSchedulerAction s)\<rbrace>
chooseThread
\<lbrace>\<lambda>rv s. P (ksSchedulerAction s)\<rbrace>"
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]:
"\<lbrace> \<lambda>s. no_orphans s \<and> invs' s \<rbrace>
timerTick
\<lbrace> \<lambda>_ s. no_orphans s \<rbrace>"
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="\<lambda>rv s. no_orphans s \<and> valid_queues' s \<and> tcb_at' thread s
\<and> 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="\<lambda>rv s. no_orphans s \<and> valid_queues' s \<and> tcb_at' thread s
\<and> 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

24
proof/refine/X64/Interrupt_R.thy
View File

@ -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 \<top> \<top> 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]:
"\<lbrace>invs'\<rbrace> timerTick \<lbrace>\<lambda>rv. invs'\<rbrace>"
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="\<lambda>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]:

15
proof/refine/X64/Invariants_H.thy
View File

@ -31,6 +31,21 @@ end
end
section "Relationship of Executable Spec to Kernel Configuration"
text \<open>
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.\<close>
lemma le_maxDomain_eq_less_numDomains:
shows "x \<le> unat maxDomain \<longleftrightarrow> x < Kernel_Config.numDomains"
"y \<le> maxDomain \<longleftrightarrow> 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*)
\<comment> \<open>---------------------------------------------------------------------------\<close>
section "Invariants on Executable Spec"

3
proof/refine/X64/Retype_R.thy
View File

@ -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"

67
proof/refine/X64/Schedule_R.thy
View File

@ -1399,7 +1399,8 @@ lemma switchToIdleThread_curr_is_idle:
lemma chooseThread_it[wp]:
"\<lbrace>\<lambda>s. P (ksIdleThread s)\<rbrace> chooseThread \<lbrace>\<lambda>_ s. P (ksIdleThread s)\<rbrace>"
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]: "\<lbrace>P\<rbrace> threadGet f t \<lbrace>\<lambda>rv. P\<rbrace>"
apply (simp add: threadGet_def)
@ -1513,6 +1514,16 @@ lemma enumPrio_word_div:
lemma curDomain_corres: "corres (=) \<top> \<top> (gets cur_domain) (curDomain)"
by (simp add: curDomain_def state_relation_def)
lemma curDomain_corres':
"corres (=) \<top> (\<lambda>s. ksCurDomain s \<le> 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:
"\<lbrakk> valid_bitmapQ s ; bitmapQ_no_L1_orphans s ; ksReadyQueuesL1Bitmap s d \<noteq> 0 \<rbrakk>
\<Longrightarrow> lookupBitmapPriority d s = (Max {prio. ksReadyQueues s (d, prio) \<noteq> []})"
@ -1579,18 +1590,27 @@ lemma ksReadyQueuesL1Bitmap_st_tcb_at':
apply simp
done
lemma curDomain_or_return_0:
"\<lbrakk> \<lbrace>P\<rbrace> curDomain \<lbrace>\<lambda>rv s. Q rv s \<rbrace>; \<And>s. P s \<Longrightarrow> ksCurDomain s \<le> maxDomain \<rbrakk>
\<Longrightarrow> \<lbrace>P\<rbrace> if 1 < numDomains then curDomain else return 0 \<lbrace>\<lambda>rv s. Q rv s \<rbrace>"
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 \<Longrightarrow> ksCurDomain s \<le> 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="_ \<noteq> 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 \<noteq> []}" in allE)
apply (case_tac "ready_queues sa (cur_domain sa) (Max {prio. ready_queues sa (cur_domain sa) prio \<noteq> []})")
apply (erule_tac x="cur_domain s" in allE)
apply (erule_tac x="Max {prio. ready_queues s (cur_domain s) prio \<noteq> []}" in allE)
apply (case_tac "ready_queues s (cur_domain s) (Max {prio. ready_queues s (cur_domain s) prio \<noteq> []})")
apply (clarsimp)
apply (subgoal_tac
"ready_queues sa (cur_domain sa) (Max {prio. ready_queues sa (cur_domain sa) prio \<noteq> []}) \<noteq> []")
"ready_queues s (cur_domain s) (Max {prio. ready_queues s (cur_domain s) prio \<noteq> []}) \<noteq> []")
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:
"\<And>s. \<lbrakk> invs_no_cicd' s; numDomains \<le> 1 \<rbrakk> \<Longrightarrow> 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="\<lambda>rv s. invs_no_cicd' s \<and> rv = ksCurDomain s"])
apply (rule_tac B="\<lambda>rv s. invs_no_cicd' s \<and> curdom = ksCurDomain s \<and>
@ -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:
"\<And>s. \<lbrakk> invs_no_cicd' s; numDomains \<le> 1 \<rbrakk> \<Longrightarrow> 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="\<lambda>rv s. invs_no_cicd' s \<and> rv = ksCurDomain s"])
apply (rule_tac B="\<lambda>rv s. invs_no_cicd' s \<and> curdom = ksCurDomain s \<and>
@ -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

2
proof/refine/X64/Syscall_R.thy
View File

@ -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]: