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

refine: replace DomainTime_R by assertion 

Signed-off-by: Gerwin Klein <gerwin.klein@data61.csiro.au>
This commit is contained in:
Gerwin Klein 2020-06-29 15:52:43 +08:00
parent 640f5654d5
commit 5ee37bd11e
21 changed files with 259 additions and 6212 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

303
proof/refine/ARM/DomainTime_R.thy
View File

@ -1,303 +0,0 @@
(*
* Copyright 2014, General Dynamics C4 Systems
*
* SPDX-License-Identifier: GPL-2.0-only
*)
theory DomainTime_R
imports
ADT_H
begin
text \<open>Preservation of domain time remaining over kernel invocations;
invariance of domain list validity
\<close>
context begin interpretation Arch . (*FIXME: arch_split*)
(* FIXME move to DetSchedDomainTime_AI *)
crunch domain_list_inv[wp]: do_user_op "\<lambda>s. P (domain_list s)"
(wp: select_wp)
(* abstract and haskell have identical domain list fields *)
abbreviation
valid_domain_list' :: "'a kernel_state_scheme \<Rightarrow> bool"
where
"valid_domain_list' \<equiv> \<lambda>s. valid_domain_list_2 (ksDomSchedule s)"
lemmas valid_domain_list'_def = valid_domain_list_2_def
(* first, crunching valid_domain_list' over the kernel - it is never changed *)
crunches sendFaultIPC, handleFault, replyFromKernel, setDomain, sendSignal,
finaliseCap, finaliseCap, capSwapForDelete
for ksDomSchedule_inv[wp]: "\<lambda>s. P (ksDomSchedule s)"
(wp: getObject_inv loadObject_default_inv crunch_wps
simp: crunch_simps if_apply_def2 unless_def o_def assertE_def)
lemma finaliseSlot_ksDomSchedule_inv[wp]:
"\<lbrace>\<lambda>s. P (ksDomSchedule s) \<rbrace> finaliseSlot param_a param_b \<lbrace>\<lambda>_ s. P (ksDomSchedule s)\<rbrace>"
by (wp finaliseSlot_preservation | clarsimp)+
crunch ksDomSchedule_inv[wp]: invokeTCB "\<lambda>s. P (ksDomSchedule s)"
(wp: crunch_wps checkCap_inv finaliseSlot'_preservation simp: if_apply_def2 crunch_simps)
crunch ksDomSchedule_inv[wp]: doReplyTransfer "\<lambda>s. P (ksDomSchedule s)"
(wp: crunch_wps transferCapsToSlots_pres1 setObject_ep_ct
setObject_ntfn_ct
simp: unless_def crunch_simps
ignore: transferCapsToSlots)
crunch ksDomSchedule_inv[wp]: finaliseCap "\<lambda>s. P (ksDomSchedule s)"
(simp: crunch_simps assertE_def unless_def
wp: getObject_inv loadObject_default_inv crunch_wps)
crunch ksDomSchedule_inv[wp]: cancelBadgedSends "\<lambda>s. P (ksDomSchedule s)"
(simp: filterM_mapM crunch_simps
wp: crunch_wps hoare_unless_wp)
crunch ksDomSchedule_inv[wp]: createNewObjects "\<lambda>s. P (ksDomSchedule s)"
(simp: crunch_simps zipWithM_x_mapM wp: crunch_wps hoare_unless_wp)
crunch ksDomSchedule_inv[wp]: preemptionPoint "\<lambda>s. P (ksDomSchedule s)"
(simp: whenE_def ignore_del: preemptionPoint)
crunch ksDomSchedule_inv[wp]: performARMMMUInvocation "\<lambda>s. P (ksDomSchedule s)"
(wp: crunch_wps getObject_cte_inv getASID_wp
simp: unless_def)
crunch ksDomSchedule_inv[wp]: performInvocation "\<lambda>s. P (ksDomSchedule s)"
(wp: crunch_wps zipWithM_x_inv cteRevoke_preservation mapME_x_inv_wp
simp: unless_def crunch_simps filterM_mapM)
crunch ksDomSchedule_inv[wp]: schedule "\<lambda>s. P (ksDomSchedule s)"
(ignore: setNextPC threadSet simp: crunch_simps bitmap_fun_defs wp:findM_inv hoare_drop_imps)
crunch ksDomSchedule_inv[wp]: activateThread "\<lambda>s. P (ksDomSchedule s)"
crunches receiveSignal, getNotification, receiveIPC, deleteCallerCap
for ksDomSchedule_inv[wp]: "\<lambda>s. P (ksDomSchedule s)"
(wp: hoare_drop_imps simp: crunch_simps)
lemma handleRecv_ksDomSchedule_inv[wp]:
"\<lbrace>\<lambda>s. P (ksDomSchedule s) \<rbrace> handleRecv e \<lbrace>\<lambda>_ s. P (ksDomSchedule s) \<rbrace>"
unfolding handleRecv_def
by (rule hoare_pre)
(wp hoare_drop_imps | simp add: crunch_simps | wpc)+
context
notes if_cong [cong]
begin
crunch ksDomSchedule_inv[wp]: handleEvent "\<lambda>s. P (ksDomSchedule s)"
(wp: syscall_valid' ignore: syscall)
end
lemma callKernel_ksDomSchedule_inv[wp]:
"\<lbrace>\<lambda>s. P (ksDomSchedule s) \<rbrace> callKernel e \<lbrace>\<lambda>_ s. P (ksDomSchedule s) \<rbrace>"
unfolding callKernel_def
by (rule hoare_pre)
(wp | simp add: if_apply_def2)+
(* now we handle preservation of domain time remaining, which most of the kernel does not change *)
crunches setExtraBadge, cteInsert
for ksDomainTime[wp]: "\<lambda>s. P (ksDomainTime s)"
(wp: crunch_wps)
crunch ksDomainTime[wp]: transferCapsToSlots "\<lambda>s. P (ksDomainTime s)"
crunches setupCallerCap, doIPCTransfer, possibleSwitchTo
for ksDomainTime[wp]: "\<lambda>s. P (ksDomainTime s)"
(wp: crunch_wps simp: zipWithM_x_mapM ignore: constOnFailure)
crunches setEndpoint, setNotification, storePTE, storePDE
for ksDomainTime_inv[wp]:
"\<lambda>s. P (ksDomainTime s)"
(wp: crunch_wps setObject_ksPSpace_only updateObject_default_inv)
crunches sendFaultIPC, handleFault, replyFromKernel
for ksDomainTime_inv[wp]: "\<lambda>s. P (ksDomainTime s)"
crunch ksDomainTime_inv[wp]: setDomain "\<lambda>s. P (ksDomainTime s)"
(wp: crunch_wps simp: if_apply_def2)
crunch ksDomainTime_inv[wp]: sendSignal "\<lambda>s. P (ksDomainTime s)"
(wp: crunch_wps simp: crunch_simps simp: unless_def o_def)
crunch ksDomainTime_inv[wp]: deleteASID "\<lambda>s. P (ksDomainTime s)"
(wp: crunch_wps setObject_ksPSpace_only getObject_inv loadObject_default_inv
updateObject_default_inv
simp: crunch_simps)
crunch ksDomainTime_inv[wp]: finaliseCap "\<lambda>s. P (ksDomainTime s)"
(simp: crunch_simps assertE_def
wp: setObject_ksPSpace_only getObject_inv loadObject_default_inv crunch_wps)
crunch ksDomainTime_inv[wp]: cancelBadgedSends "\<lambda>s. P (ksDomainTime s)"
(wp: crunch_wps setObject_ksPSpace_only getObject_inv loadObject_default_inv
updateObject_default_inv hoare_unless_wp
simp: filterM_mapM crunch_simps)
crunch ksDomainTime_inv[wp]: capSwapForDelete "\<lambda>s. P (ksDomainTime s)"
(simp: crunch_simps)
lemma finaliseSlot_ksDomainTime_inv[wp]:
"\<lbrace>\<lambda>s. P (ksDomainTime s) \<rbrace> finaliseSlot param_a param_b \<lbrace>\<lambda>_ s. P (ksDomainTime s)\<rbrace>"
by (wp finaliseSlot_preservation | clarsimp)+
crunch ksDomainTime_inv[wp]: invokeTCB "\<lambda>s. P (ksDomainTime s)"
(wp: crunch_wps checkCap_inv finaliseSlot'_preservation simp: if_apply_def2 crunch_simps)
crunch ksDomainTime_inv[wp]: doReplyTransfer "\<lambda>s. P (ksDomainTime s)"
(wp: crunch_wps transferCapsToSlots_pres1 setObject_ep_ct
setObject_ntfn_ct
simp: crunch_simps
ignore: transferCapsToSlots)
crunch ksDomainTime_inv[wp]: finaliseCap "\<lambda>s. P (ksDomainTime s)"
(simp: crunch_simps assertE_def unless_def
wp: getObject_inv loadObject_default_inv crunch_wps)
crunch ksDomainTime_inv[wp]: cancelBadgedSends "\<lambda>s. P (ksDomainTime s)"
(simp: filterM_mapM crunch_simps
wp: crunch_wps)
crunch ksDomainTime_inv[wp]: createNewObjects "\<lambda>s. P (ksDomainTime s)"
(simp: crunch_simps zipWithM_x_mapM
wp: crunch_wps hoare_unless_wp)
crunch ksDomainTime_inv[wp]: performARMMMUInvocation "\<lambda>s. P (ksDomainTime s)"
(wp: crunch_wps getObject_cte_inv getASID_wp setObject_ksPSpace_only updateObject_default_inv
simp: unless_def)
crunch ksDomainTime_inv[wp]: preemptionPoint "\<lambda>s. P (ksDomainTime s)"
(simp: whenE_def ignore_del: preemptionPoint)
crunch ksDomainTime_inv[wp]: performInvocation "\<lambda>s. P (ksDomainTime s)"
(wp: crunch_wps zipWithM_x_inv cteRevoke_preservation mapME_x_inv_wp
simp: unless_def crunch_simps filterM_mapM)
crunch ksDomainTime_inv[wp]: activateThread "\<lambda>s. P (ksDomainTime s)"
crunches receiveSignal, getNotification, receiveIPC, deleteCallerCap
for ksDomainTime_inv[wp]: "\<lambda>s. P (ksDomainTime s)"
(wp: hoare_drop_imps simp: crunch_simps)
lemma handleRecv_ksDomainTime_inv[wp]:
"\<lbrace>\<lambda>s. P (ksDomainTime s) \<rbrace> handleRecv e \<lbrace>\<lambda>_ s. P (ksDomainTime s) \<rbrace>"
unfolding handleRecv_def
by (rule hoare_pre)
(wp hoare_drop_imps | simp add: crunch_simps | wpc)+
crunches doUserOp, getIRQState, chooseThread, handleYield
for ksDomainTime_inv[wp]: "(\<lambda>s. P (ksDomainTime s))"
(wp: select_wp)
crunches handleSend, handleReply, handleCall, handleHypervisorFault
for ksDomainTime_inv[wp]: "(\<lambda>s. P (ksDomainTime s))"
(wp: syscall_valid' ignore: syscall)
lemma nextDomain_domain_time_left'[wp]:
"\<lbrace> valid_domain_list' \<rbrace>
nextDomain
\<lbrace>\<lambda>_ s. 0 < ksDomainTime s \<rbrace>"
unfolding nextDomain_def Let_def
apply (wpsimp simp: valid_domain_list'_def dschLength_def)
apply (simp only: all_set_conv_all_nth)
apply (erule_tac x="Suc (ksDomScheduleIdx s) mod length (ksDomSchedule s)" in allE)
apply fastforce
done
lemma rescheduleRequired_ksSchedulerAction[wp]:
"\<lbrace>\<top>\<rbrace> rescheduleRequired \<lbrace>\<lambda>_ s. ksSchedulerAction s = ChooseNewThread \<rbrace>"
unfolding rescheduleRequired_def
by (wp setSchedulerAction_direct)
lemma timerTick_valid_domain_time:
"\<lbrace>\<lambda>s. 0 < ksDomainTime s\<rbrace>
timerTick
\<lbrace>\<lambda>_ s. ksDomainTime s = 0 \<longrightarrow> ksSchedulerAction s = ChooseNewThread\<rbrace>"
apply (simp add: timerTick_def numDomains_def)
apply wp
apply (rule_tac Q="\<lambda>_ s. ksSchedulerAction s = ChooseNewThread" in hoare_strengthen_post)
apply (wp | clarsimp simp: if_apply_def2)+
done
lemma handleInterrupt_valid_domain_time:
"\<lbrace>\<lambda>s. 0 < ksDomainTime s \<rbrace>
handleInterrupt i
\<lbrace>\<lambda>rv s. ksDomainTime s = 0 \<longrightarrow> ksSchedulerAction s = ChooseNewThread\<rbrace>"
apply (simp add: handleInterrupt_def)
apply (case_tac "maxIRQ < i"; simp)
subgoal by (wp hoare_false_imp) simp
apply (rule_tac B="\<lambda>_ s. 0 < ksDomainTime s" in hoare_seq_ext[rotated])
apply (rule hoare_pre, wp, simp)
apply (rename_tac st)
apply (case_tac st, simp_all add: maskIrqSignal_def)
(* IRQSignal : no timer tick, trivial preservation of ksDomainTime *)
apply (rule_tac Q="\<lambda>_ s. 0 < ksDomainTime s" in hoare_post_imp, clarsimp)
apply (rule hoare_pre, (wp | wpc)+)
apply (rule_tac Q="\<lambda>_ s. 0 < ksDomainTime s" in hoare_post_imp, clarsimp)
apply wp
(* IRQTimer : tick occurs *) (* IRQReserved : trivial *)
apply (wp timerTick_valid_domain_time
| clarsimp simp: handleReservedIRQ_def
| wp (once) hoare_vcg_imp_lift)+
done
lemma schedule_domain_time_left':
"\<lbrace> valid_domain_list' and
(\<lambda>s. ksDomainTime s = 0 \<longrightarrow> ksSchedulerAction s = ChooseNewThread) \<rbrace>
ThreadDecls_H.schedule
\<lbrace>\<lambda>_ s. 0 < ksDomainTime s \<rbrace>"
unfolding schedule_def scheduleChooseNewThread_def
supply word_neq_0_conv[simp]
apply wpsimp+
apply (rule_tac Q="\<lambda>_. valid_domain_list'" in hoare_post_imp, clarsimp)
apply (wp | clarsimp | wp (once) hoare_drop_imps)+
done
lemma handleEvent_ksDomainTime_inv:
"\<lbrace>\<lambda>s. P (ksDomainTime s) \<and> e \<noteq> Interrupt \<rbrace>
handleEvent e
\<lbrace>\<lambda>_ s. P (ksDomainTime s) \<rbrace>"
apply (cases e, simp_all)
apply (rename_tac syscall)
apply (case_tac syscall, simp_all add: handle_send_def)
apply (wp hv_inv'|simp add: handleEvent_def cong: if_cong|wpc)+
done
lemma callKernel_domain_time_left:
"\<lbrace> (\<lambda>s. 0 < ksDomainTime s) and valid_domain_list' and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_running' s) \<rbrace>
callKernel e
\<lbrace>\<lambda>_ s. 0 < ksDomainTime s \<rbrace>"
including no_pre
unfolding callKernel_def
supply word_neq_0_conv[simp]
apply (case_tac "e = Interrupt")
apply (simp add: handleEvent_def)
apply (rule hoare_pre)
apply ((wp schedule_domain_time_left' handleInterrupt_valid_domain_time
| wpc | simp)+)[1]
apply (rule_tac Q="\<lambda>_ s. 0 < ksDomainTime s \<and> valid_domain_list' s" in hoare_post_imp)
apply fastforce
apply wp
apply simp
(* non-interrupt case; may throw but does not touch ksDomainTime in handleEvent *)
apply simp
apply ((wp schedule_domain_time_left' handleInterrupt_valid_domain_time
| simp add: if_apply_def2)+)[1]
apply (rule_tac Q="\<lambda>_ s. valid_domain_list' s \<and> 0 < ksDomainTime s" in hoare_post_imp)
apply fastforce
apply wp
apply simp
apply (rule hoare_pre)
apply (rule_tac Q="\<lambda>_ s. valid_domain_list' s \<and> 0 < ksDomainTime s"
in NonDetMonadVCG.hoare_post_impErr[rotated 2], assumption)
apply (wp handleEvent_ksDomainTime_inv | clarsimp)+
done
end
end

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

@ -266,7 +266,8 @@ crunch (empty_fail) empty_fail: callKernel
theorem call_kernel_serial:
"\<lbrakk> (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (ct_running or ct_idle) and
(\<lambda>s. scheduler_action s = resume_cur_thread)) s;
(\<lambda>s. scheduler_action s = resume_cur_thread) and
(\<lambda>s. 0 < domain_time s \<and> valid_domain_list s)) s;
\<exists>s'. (s, s') \<in> state_relation \<and>
(invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (ct_running' or ct_idle') and
(\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and

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

@ -2420,7 +2420,7 @@ theorem callKernel_no_orphans [wp]:
callKernel e
\<lbrace> \<lambda>rv s. no_orphans s \<rbrace>"
unfolding callKernel_def
by (wpsimp wp: weak_if_wp schedule_invs')
by (wpsimp wp: weak_if_wp schedule_invs' hoare_drop_imps)
end

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

@ -2267,7 +2267,8 @@ lemma callKernel_valid_duplicates':
apply (rule hoare_pre)
apply (wp activate_invs' activate_sch_act schedule_sch
schedule_sch_act_simple he_invs'
| simp add: no_irq_getActiveIRQ)+
| simp add: no_irq_getActiveIRQ
| wp (once) hoare_drop_imps )+
apply (rule hoare_post_impErr)
apply (rule valid_validE)
prefer 2

72
proof/refine/ARM/Refine.thy
View File

@ -11,7 +11,7 @@
theory Refine
imports
KernelInit_R
DomainTime_R
ADT_H
InitLemmas
PageTableDuplicates
begin
@ -401,15 +401,22 @@ lemma ckernel_invs:
apply (rule hoare_pre)
apply (wp activate_invs' activate_sch_act schedule_sch
schedule_sch_act_simple he_invs' schedule_invs'
hoare_drop_imp[where R="\<lambda>_. kernelExitAssertions"]
| simp add: no_irq_getActiveIRQ)+
done
lemma doMachineOp_ct_running':
"\<lbrace>ct_running'\<rbrace> doMachineOp f \<lbrace>\<lambda>_. ct_running'\<rbrace>"
apply (simp add: ct_in_state'_def doMachineOp_def split_def)
apply wp
apply (simp add: pred_tcb_at'_def o_def)
done
(* abstract and haskell have identical domain list fields *)
abbreviation valid_domain_list' :: "'a kernel_state_scheme \<Rightarrow> bool" where
"valid_domain_list' \<equiv> \<lambda>s. valid_domain_list_2 (ksDomSchedule s)"
lemmas valid_domain_list'_def = valid_domain_list_2_def
defs kernelExitAssertions_def:
"kernelExitAssertions s \<equiv> 0 < ksDomainTime s \<and> valid_domain_list' s"
lemma callKernel_domain_time_left:
"\<lbrace> \<top> \<rbrace> callKernel e \<lbrace>\<lambda>_ s. 0 < ksDomainTime s \<and> valid_domain_list' s \<rbrace>"
unfolding callKernel_def kernelExitAssertions_def by wpsimp
lemma kernelEntry_invs':
"\<lbrace> invs' and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_running' s) and
@ -426,7 +433,6 @@ lemma kernelEntry_invs':
apply (wp ckernel_invs callKernel_valid_duplicates' callKernel_domain_time_left
threadSet_invs_trivial threadSet_ct_running' select_wp
TcbAcc_R.dmo_invs' static_imp_wp
doMachineOp_ct_running'
callKernel_domain_time_left
| clarsimp simp: user_memory_update_def no_irq_def tcb_at_invs'
valid_domain_list'_def)+
@ -491,6 +497,9 @@ lemma device_update_invs':
lemmas ex_abs_def = ex_abs_underlying_def[where sr=state_relation and P=G,abs_def] for G
crunches doMachineOp
for ksDomainTime[wp]: "\<lambda>s. P (ksDomainTime s)"
lemma doUserOp_invs':
"\<lbrace>invs' and ex_abs einvs and
(\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_running' and
@ -500,7 +509,7 @@ lemma doUserOp_invs':
(\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_running' and
(\<lambda>s. 0 < ksDomainTime s) and valid_domain_list'\<rbrace>"
apply (simp add: doUserOp_def split_def ex_abs_def)
apply (wp device_update_invs' doMachineOp_ct_running' select_wp
apply (wp device_update_invs' select_wp
| (wp (once) dmo_invs', wpsimp simp: no_irq_modify device_memory_update_def
user_memory_update_def))+
apply (clarsimp simp: user_memory_update_def simpler_modify_def
@ -520,13 +529,23 @@ lemma doUserOp_valid_duplicates':
text \<open>The top-level correspondence\<close>
lemma kernel_corres:
lemma kernel_corres':
"corres dc (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (ct_running or ct_idle)
and (\<lambda>s. scheduler_action s = resume_cur_thread))
(invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (ct_running' or ct_idle') and
(\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and
(\<lambda>s. vs_valid_duplicates' (ksPSpace s)))
(call_kernel event) (callKernel event)"
(call_kernel event)
(do _ \<leftarrow> runExceptT $
handleEvent event `~catchError~`
(\<lambda>_. withoutPreemption $ do
irq <- doMachineOp (getActiveIRQ True);
when (isJust irq) $ handleInterrupt (fromJust irq)
od);
_ \<leftarrow> ThreadDecls_H.schedule;
activateThread
od)"
unfolding call_kernel_def callKernel_def
apply (simp add: call_kernel_def callKernel_def)
apply (rule corres_guard_imp)
apply (rule corres_split)
@ -561,13 +580,40 @@ lemma kernel_corres:
apply (rule activate_corres)
apply (wp handle_interrupt_valid_sched[unfolded non_kernel_IRQs_def, simplified]
schedule_invs' hoare_vcg_if_lift2 hoare_drop_imps |simp)+
apply (rule_tac Q="\<lambda>_. valid_sched and invs and valid_list" and E="\<lambda>_. valid_sched and invs and valid_list"
apply (rule_tac Q="\<lambda>_. valid_sched and invs and valid_list" and
E="\<lambda>_. valid_sched and invs and valid_list"
in hoare_post_impErr)
apply (wp handle_event_valid_sched |simp)+
apply (wp handle_event_valid_sched hoare_vcg_imp_lift' |simp)+
apply (clarsimp simp: active_from_running)
apply (clarsimp simp: active_from_running')
done
lemma kernel_corres:
"corres dc (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (ct_running or ct_idle) and
(\<lambda>s. scheduler_action s = resume_cur_thread) and
(\<lambda>s. 0 < domain_time s \<and> valid_domain_list s))
(invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (ct_running' or ct_idle') and
(\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and
(\<lambda>s. vs_valid_duplicates' (ksPSpace s)))
(call_kernel event) (callKernel event)"
unfolding callKernel_def K_bind_def
apply (rule corres_guard_imp)
apply (rule corres_add_noop_lhs2)
apply (simp only: bind_assoc[symmetric])
apply (rule corres_split[where r'=dc and
R="\<lambda>_ s. 0 < domain_time s \<and> valid_domain_list s" and
R'="\<lambda>_. \<top>"])
apply (rule corres_bind_return2, rule corres_stateAssert_assume_stronger)
apply simp
apply (simp add: kernelExitAssertions_def state_relation_def)
apply (simp only: bind_assoc)
apply (rule kernel_corres')
apply (wp call_kernel_domain_time_inv_det_ext call_kernel_domain_list_inv_det_ext)
apply wp
apply clarsimp
apply clarsimp
done
lemma user_mem_corres:
"corres (=) invs invs' (gets (\<lambda>x. g (user_mem x))) (gets (\<lambda>x. g (user_mem' x)))"
by (clarsimp simp add: gets_def get_def return_def bind_def

338
proof/refine/ARM_HYP/DomainTime_R.thy
View File

@ -1,338 +0,0 @@
(*
* Copyright 2014, General Dynamics C4 Systems
*
* SPDX-License-Identifier: GPL-2.0-only
*)
theory DomainTime_R
imports
ADT_H
begin
text \<open>Preservation of domain time remaining over kernel invocations;
invariance of domain list validity
\<close>
context begin interpretation Arch . (*FIXME: arch_split*)
(* abstract and haskell have identical domain list fields *)
abbreviation
valid_domain_list' :: "'a kernel_state_scheme \<Rightarrow> bool"
where
"valid_domain_list' \<equiv> \<lambda>s. valid_domain_list_2 (ksDomSchedule s)"
lemmas valid_domain_list'_def = valid_domain_list_2_def
(* first, crunching valid_domain_list' over the kernel - it is never changed *)
crunches sendFaultIPC, handleFault, replyFromKernel
for ksDomSchedule_inv[wp]: "\<lambda>s. P (ksDomSchedule s)"
crunch ksDomSchedule_inv[wp]: setDomain "\<lambda>s. P (ksDomSchedule s)"
(wp: crunch_wps simp: if_apply_def2)
crunch ksDomSchedule_inv[wp]: sendSignal "\<lambda>s. P (ksDomSchedule s)"
(wp: crunch_wps simp: crunch_simps simp: unless_def o_def)
crunches vcpuSwitch, dissociateVCPUTCB
for ksDomSchedule_inv[wp]: "\<lambda>s. P (ksDomSchedule s)"
(wp: crunch_wps setObject_ksDomSchedule_inv FalseI simp: crunch_simps)
crunch ksDomSchedule_inv[wp]: finaliseCap "\<lambda>s. P (ksDomSchedule s)"
(simp: crunch_simps assertE_def unless_def
wp: getObject_inv loadObject_default_inv crunch_wps)
crunches finaliseCap, capSwapForDelete
for ksDomSchedule_inv[wp]: "\<lambda>s. P (ksDomSchedule s)"
(simp: crunch_simps simp: unless_def)
lemma finaliseSlot_ksDomSchedule_inv[wp]:
"\<lbrace>\<lambda>s. P (ksDomSchedule s) \<rbrace> finaliseSlot param_a param_b \<lbrace>\<lambda>_ s. P (ksDomSchedule s)\<rbrace>"
by (wp finaliseSlot_preservation | clarsimp)+
crunch ksDomSchedule_inv[wp]: invokeTCB "\<lambda>s. P (ksDomSchedule s)"
(wp: cteDelete_preservation checkCap_inv crunch_wps simp: crunch_simps unless_def
ignore: checkCapAt cteDelete)
crunch ksDomSchedule_inv[wp]: doReplyTransfer "\<lambda>s. P (ksDomSchedule s)"
(wp: crunch_wps transferCapsToSlots_pres1 setObject_ep_ct
setObject_ntfn_ct
simp: unless_def crunch_simps
ignore: transferCapsToSlots)
crunch ksDomSchedule_inv[wp]: finaliseCap "\<lambda>s. P (ksDomSchedule s)"
(simp: crunch_simps assertE_def unless_def
wp: getObject_inv loadObject_default_inv crunch_wps)
crunch ksDomSchedule_inv[wp]: cancelBadgedSends "\<lambda>s. P (ksDomSchedule s)"
(simp: filterM_mapM crunch_simps
wp: crunch_wps hoare_unless_wp)
crunch ksDomSchedule_inv[wp]: createNewObjects "\<lambda>s. P (ksDomSchedule s)"
(simp: crunch_simps zipWithM_x_mapM wp: crunch_wps hoare_unless_wp)
crunch ksDomSchedule_inv[wp]: preemptionPoint "\<lambda>s. P (ksDomSchedule s)"
(simp: whenE_def ignore_del: preemptionPoint)
crunch ksDomSchedule_inv[wp]: performARMMMUInvocation "\<lambda>s. P (ksDomSchedule s)"
(wp: crunch_wps getObject_cte_inv getASID_wp
simp: unless_def)
crunch ksDomSchedule_inv[wp]: performInvocation "\<lambda>s. P (ksDomSchedule s)"
(wp: crunch_wps zipWithM_x_inv cteRevoke_preservation mapME_x_inv_wp
simp: unless_def crunch_simps filterM_mapM)
crunch ksDomSchedule_inv[wp]: schedule "\<lambda>s. P (ksDomSchedule s)"
(ignore: setNextPC threadSet
simp: crunch_simps bitmap_fun_defs
wp: findM_inv hoare_drop_imps)
crunch ksDomSchedule_inv[wp]: activateThread "\<lambda>s. P (ksDomSchedule s)"
crunches receiveSignal, getNotification, receiveIPC, deleteCallerCap
for ksDomSchedule_inv[wp]: "\<lambda>s. P (ksDomSchedule s)"
(wp: hoare_drop_imps simp: crunch_simps)
lemma handleRecv_ksDomSchedule_inv[wp]:
"\<lbrace>\<lambda>s. P (ksDomSchedule s) \<rbrace> handleRecv e \<lbrace>\<lambda>_ s. P (ksDomSchedule s) \<rbrace>"
unfolding handleRecv_def
by (rule hoare_pre)
(wp hoare_drop_imps | simp add: crunch_simps | wpc)+
crunch ksDomSchedule_inv[wp]: handleEvent "\<lambda>s. P (ksDomSchedule s)"
(wp: hoare_drop_imps syscall_valid' hoare_vcg_if_lift3
ignore: syscall)
lemma callKernel_ksDomSchedule_inv[wp]:
"\<lbrace>\<lambda>s. P (ksDomSchedule s) \<rbrace> callKernel e \<lbrace>\<lambda>_ s. P (ksDomSchedule s) \<rbrace>"
unfolding callKernel_def
by (rule hoare_pre)
(wp | simp add: if_apply_def2)+
(* now we handle preservation of domain time remaining, which most of the kernel does not change *)
crunches setExtraBadge, cteInsert, transferCapsToSlots, setupCallerCap, doIPCTransfer, possibleSwitchTo
for ksDomainTime[wp]: "\<lambda>s. P (ksDomainTime s)"
(wp: crunch_wps simp: zipWithM_x_mapM ignore: constOnFailure)
crunches setEndpoint, setNotification, storePTE, storePDE
for ksDomainTime_inv[wp]: "\<lambda>s. P (ksDomainTime s)"
(wp: crunch_wps setObject_ksPSpace_only updateObject_default_inv)
crunches sendFaultIPC, handleFault, replyFromKernel
for ksDomainTime_inv[wp]: "\<lambda>s. P (ksDomainTime s)"
crunch ksDomainTime_inv[wp]: setDomain "\<lambda>s. P (ksDomainTime s)"
(wp: crunch_wps simp: if_apply_def2)
crunch ksDomainTime_inv[wp]: sendSignal "\<lambda>s. P (ksDomainTime s)"
(wp: crunch_wps simp: crunch_simps simp: unless_def o_def)
crunches deleteASID, dissociateVCPUTCB
for ksDomainTime_inv[wp]: "\<lambda>s. P (ksDomainTime s)"
(wp: crunch_wps setObject_ksPSpace_only getObject_inv loadObject_default_inv
updateObject_default_inv FalseI getVCPU_wp hoare_vcg_all_lift hoare_vcg_if_lift3
simp: crunch_simps)
crunch ksDomainTime_inv[wp]: finaliseCap "\<lambda>s. P (ksDomainTime s)"
(simp: crunch_simps assertE_def
wp: setObject_ksPSpace_only getObject_inv loadObject_default_inv crunch_wps)
crunch ksDomainTime_inv[wp]: cancelBadgedSends "\<lambda>s. P (ksDomainTime s)"
(wp: crunch_wps setObject_ksPSpace_only getObject_inv loadObject_default_inv
updateObject_default_inv hoare_unless_wp
simp: filterM_mapM crunch_simps)
crunch ksDomainTime_inv[wp]: capSwapForDelete "\<lambda>s. P (ksDomainTime s)"
(simp: crunch_simps simp: unless_def)
lemma finaliseSlot_ksDomainTime_inv[wp]:
"\<lbrace>\<lambda>s. P (ksDomainTime s) \<rbrace> finaliseSlot param_a param_b \<lbrace>\<lambda>_ s. P (ksDomainTime s)\<rbrace>"
by (wp finaliseSlot_preservation | clarsimp)+
crunch ksDomainTime_inv[wp]: invokeTCB "\<lambda>s. P (ksDomainTime s)"
(wp: crunch_wps checkCap_inv finaliseSlot'_preservation simp: if_apply_def2 crunch_simps)
crunch ksDomainTime_inv[wp]: doReplyTransfer "\<lambda>s. P (ksDomainTime s)"
(wp: crunch_wps transferCapsToSlots_pres1 setObject_ep_ct
setObject_ntfn_ct
simp: unless_def crunch_simps
ignore: transferCapsToSlots)
crunch ksDomainTime_inv[wp]: finaliseCap "\<lambda>s. P (ksDomainTime s)"
(simp: crunch_simps assertE_def unless_def
wp: getObject_inv loadObject_default_inv crunch_wps)
crunch ksDomainTime_inv[wp]: cancelBadgedSends "\<lambda>s. P (ksDomainTime s)"
(simp: filterM_mapM crunch_simps
wp: crunch_wps)
crunch ksDomainTime_inv[wp]: createNewObjects "\<lambda>s. P (ksDomainTime s)"
(simp: crunch_simps zipWithM_x_mapM
wp: crunch_wps hoare_unless_wp)
crunch ksDomainTime_inv[wp]: performARMMMUInvocation "\<lambda>s. P (ksDomainTime s)"
(wp: crunch_wps getObject_cte_inv getASID_wp setObject_ksPSpace_only updateObject_default_inv
simp: unless_def)
crunch ksDomainTime_inv[wp]: preemptionPoint "\<lambda>s. P (ksDomainTime s)"
(simp: whenE_def ignore_del: preemptionPoint)
lemma setObjectVCPU_ksDomainTime_inv[wp]:
"setObject p (v::vcpu) \<lbrace>\<lambda>s. P (ksDomainTime s)\<rbrace>"
unfolding setObject_def by (wpsimp simp: updateObject_default_def)
crunch ksDomainTime_inv[wp]: performInvocation "\<lambda>s. P (ksDomainTime s)"
(wp: crunch_wps zipWithM_x_inv cteRevoke_preservation mapME_x_inv_wp
simp: unless_def crunch_simps filterM_mapM)
crunch ksDomainTime_inv[wp]: activateThread "\<lambda>s. P (ksDomainTime s)"
crunches receiveSignal, getNotification, receiveIPC, deleteCallerCap
for ksDomainTime_inv[wp]: "\<lambda>s. P (ksDomainTime s)"
(wp: hoare_drop_imps simp: crunch_simps)
lemma handleRecv_ksDomainTime_inv[wp]:
"\<lbrace>\<lambda>s. P (ksDomainTime s) \<rbrace> handleRecv e \<lbrace>\<lambda>_ s. P (ksDomainTime s) \<rbrace>"
unfolding handleRecv_def
by (rule hoare_pre)
(wp hoare_drop_imps | simp add: crunch_simps | wpc)+
crunch ksDomainTime_inv[wp]: doUserOp "(\<lambda>s. P (ksDomainTime s))"
(wp: select_wp)
crunches getIRQState, chooseThread, handleYield
for ksDomainTime_inv[wp]: "(\<lambda>s. P (ksDomainTime s))"
(wp: crunch_wps)
crunches handleSend, handleReply
for ksDomainTime_inv[wp]: "(\<lambda>s. P (ksDomainTime s))"
(wp: hoare_drop_imps syscall_valid'
ignore: syscall)
crunch ksDomainTime_inv[wp]: handleCall "(\<lambda>s. P (ksDomainTime s))"
(wp: crunch_wps setObject_ksPSpace_only updateObject_default_inv cteRevoke_preservation
simp: crunch_simps unless_def
ignore: syscall constOnFailure)
crunches activateThread, handleHypervisorFault
for domain_time'_inv[wp]: "\<lambda>s. P (ksDomainTime s)"
(wp: hoare_drop_imps)
lemma nextDomain_domain_time_left'[wp]:
"\<lbrace> valid_domain_list' \<rbrace>
nextDomain
\<lbrace>\<lambda>_ s. 0 < ksDomainTime s \<rbrace>"
unfolding nextDomain_def Let_def
apply wp
apply (clarsimp simp: valid_domain_list'_def dschLength_def)
apply (simp only: all_set_conv_all_nth)
apply (erule_tac x="Suc (ksDomScheduleIdx s) mod length (ksDomSchedule s)" in allE)
apply fastforce
done
lemma rescheduleRequired_ksSchedulerAction[wp]:
"\<lbrace>\<top>\<rbrace> rescheduleRequired \<lbrace>\<lambda>_ s. ksSchedulerAction s = ChooseNewThread \<rbrace>"
unfolding rescheduleRequired_def
by (wp setSchedulerAction_direct)
lemma timerTick_valid_domain_time:
"\<lbrace>\<lambda>s. 0 < ksDomainTime s\<rbrace>
timerTick
\<lbrace>\<lambda>_ s. ksDomainTime s = 0 \<longrightarrow> ksSchedulerAction s = ChooseNewThread\<rbrace>"
apply (simp add: timerTick_def numDomains_def)
apply wp
apply (rule_tac Q="\<lambda>_ s. ksSchedulerAction s = ChooseNewThread" in hoare_strengthen_post)
apply (wp | clarsimp simp: if_apply_def2)+
done
crunches handleReservedIRQ, handleVMFault
for domain_time'_inv[wp]: "\<lambda>s. P (ksDomainTime s)"
(wp: crunch_wps simp: crunch_simps)
lemma handleReservedIRQ_valid_domain_time[wp]:
"\<lbrace>\<lambda>s. 0 < ksDomainTime s \<rbrace>
handleReservedIRQ i
\<lbrace>\<lambda>rv s. ksDomainTime s = 0 \<longrightarrow> ksSchedulerAction s = ChooseNewThread\<rbrace>"
apply (rule hoare_strengthen_post)
apply (rule handleReservedIRQ_domain_time'_inv)
apply clarsimp
done
lemma handleInterrupt_valid_domain_time:
"\<lbrace>\<lambda>s. 0 < ksDomainTime s \<rbrace>
handleInterrupt i
\<lbrace>\<lambda>rv s. ksDomainTime s = 0 \<longrightarrow> ksSchedulerAction s = ChooseNewThread\<rbrace>"
apply (simp add: handleInterrupt_def)
apply (case_tac "maxIRQ < i"; simp)
subgoal by (wp hoare_false_imp) simp
apply (rule_tac B="\<lambda>_ s. 0 < ksDomainTime s" in hoare_seq_ext[rotated])
apply (rule hoare_pre, wp, simp)
apply (rename_tac st)
apply (case_tac st, simp_all add: maskIrqSignal_def)
(* IRQSignal : no timer tick, trivial preservation of ksDomainTime *)
apply (rule_tac Q="\<lambda>_ s. 0 < ksDomainTime s" in hoare_post_imp, clarsimp)
apply (rule hoare_pre, (wp | wpc)+)
apply (rule_tac Q="\<lambda>_ s. 0 < ksDomainTime s" in hoare_post_imp, clarsimp)
apply wp
(* IRQTimer : tick occurs *) (* IRQReserved : trivial *)
apply (wpsimp wp: timerTick_valid_domain_time
| wp (once) hoare_vcg_imp_lift )+
done
lemma schedule_domain_time_left':
"\<lbrace> valid_domain_list' and
(\<lambda>s. ksDomainTime s = 0 \<longrightarrow> ksSchedulerAction s = ChooseNewThread) \<rbrace>
ThreadDecls_H.schedule
\<lbrace>\<lambda>_ s. 0 < ksDomainTime s \<rbrace>"
unfolding schedule_def scheduleChooseNewThread_def
supply word_neq_0_conv[simp]
apply wpsimp+
apply (rule_tac Q="\<lambda>_. valid_domain_list'" in hoare_post_imp, clarsimp)
apply (wp | clarsimp | wp (once) hoare_drop_imps)+
done
lemma handleEvent_ksDomainTime_inv:
"\<lbrace>\<lambda>s. P (ksDomainTime s) \<and> e \<noteq> Interrupt \<rbrace>
handleEvent e
\<lbrace>\<lambda>_ s. P (ksDomainTime s) \<rbrace>"
apply (cases e, simp_all)
apply (rename_tac syscall)
apply (case_tac syscall, simp_all add: handle_send_def)
apply (wp |simp add: handleEvent_def cong: if_cong|wpc)+
done
lemma callKernel_domain_time_left:
"\<lbrace> (\<lambda>s. 0 < ksDomainTime s) and valid_domain_list' and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_running' s) \<rbrace>
callKernel e
\<lbrace>\<lambda>_ s. 0 < ksDomainTime s \<rbrace>"
including no_pre
unfolding callKernel_def
supply word_neq_0_conv[simp]
apply (case_tac "e = Interrupt")
apply (simp add: handleEvent_def)
apply (rule hoare_pre)
apply ((wp schedule_domain_time_left' handleInterrupt_valid_domain_time
| wpc | simp)+)[1]
apply (rule_tac Q="\<lambda>_ s. 0 < ksDomainTime s \<and> valid_domain_list' s" in hoare_post_imp)
apply fastforce
apply wp
apply simp
(* non-interrupt case; may throw but does not touch ksDomainTime in handleEvent *)
apply simp
apply ((wp schedule_domain_time_left' handleInterrupt_valid_domain_time
| simp add: if_apply_def2)+)[1]
apply (rule_tac Q="\<lambda>_ s. valid_domain_list' s \<and> 0 < ksDomainTime s" in hoare_post_imp)
apply fastforce
apply wp
apply simp
apply (rule hoare_pre)
apply (rule_tac Q="\<lambda>_ s. valid_domain_list' s \<and> 0 < ksDomainTime s"
in NonDetMonadVCG.hoare_post_impErr[rotated 2], assumption)
apply (wp handleEvent_ksDomainTime_inv | clarsimp)+
done
end
end

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

@ -280,7 +280,8 @@ crunch (empty_fail) empty_fail: callKernel
theorem call_kernel_serial:
"\<lbrakk> (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (ct_running or ct_idle) and
(\<lambda>s. scheduler_action s = resume_cur_thread)) s;
(\<lambda>s. scheduler_action s = resume_cur_thread) and
(\<lambda>s. 0 < domain_time s \<and> valid_domain_list s)) s;
\<exists>s'. (s, s') \<in> state_relation \<and>
(invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (ct_running' or ct_idle') and
(\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and

2457
proof/refine/ARM_HYP/Orphanage.thy
View File

File diff suppressed because it is too large Load Diff

1
proof/refine/ARM_HYP/PageTableDuplicates.thy
View File

@ -2198,6 +2198,7 @@ lemma callKernel_valid_duplicates':
apply (simp add: callKernel_def)
apply (rule hoare_pre)
apply (wp activate_invs' activate_sch_act schedule_sch
hoare_drop_imp[where R="\<lambda>_. kernelExitAssertions"]
schedule_sch_act_simple he_invs' hoare_vcg_if_lift3
| simp add: no_irq_getActiveIRQ
| strengthen non_kernel_IRQs_strg, simp cong: conj_cong)+

66
proof/refine/ARM_HYP/Refine.thy
View File

@ -11,7 +11,7 @@
theory Refine
imports
KernelInit_R
DomainTime_R
ADT_H
InitLemmas
PageTableDuplicates
begin
@ -401,16 +401,23 @@ lemma ckernel_invs:
apply (rule hoare_pre)
apply (wp activate_invs' activate_sch_act schedule_sch
schedule_sch_act_simple he_invs' schedule_invs' hoare_vcg_if_lift3
hoare_drop_imp[where R="\<lambda>_. kernelExitAssertions"]
| simp add: no_irq_getActiveIRQ
| strengthen non_kernel_IRQs_strg[where Q=True, simplified], simp cong: conj_cong)+
done
lemma doMachineOp_ct_running':
"\<lbrace>ct_running'\<rbrace> doMachineOp f \<lbrace>\<lambda>_. ct_running'\<rbrace>"
apply (simp add: ct_in_state'_def doMachineOp_def split_def)
apply wp
apply (simp add: pred_tcb_at'_def o_def)
done
(* abstract and haskell have identical domain list fields *)
abbreviation valid_domain_list' :: "'a kernel_state_scheme \<Rightarrow> bool" where
"valid_domain_list' \<equiv> \<lambda>s. valid_domain_list_2 (ksDomSchedule s)"
lemmas valid_domain_list'_def = valid_domain_list_2_def
defs kernelExitAssertions_def:
"kernelExitAssertions s \<equiv> 0 < ksDomainTime s \<and> valid_domain_list' s"
lemma callKernel_domain_time_left:
"\<lbrace> \<top> \<rbrace> callKernel e \<lbrace>\<lambda>_ s. 0 < ksDomainTime s \<and> valid_domain_list' s \<rbrace>"
unfolding callKernel_def kernelExitAssertions_def by wpsimp
lemma kernelEntry_invs':
"\<lbrace> invs' and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_running' s) and
@ -495,6 +502,9 @@ lemma device_update_invs':
gets_def get_def bind_def valid_def return_def)
by (clarsimp simp: invs'_def valid_state'_def valid_irq_states'_def valid_machine_state'_def)
crunches doMachineOp
for ksDomainTime[wp]: "\<lambda>s. P (ksDomainTime s)"
lemma doUserOp_invs':
"\<lbrace>invs' and ex_abs einvs and
(\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_running' and
@ -504,7 +514,7 @@ lemma doUserOp_invs':
(\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_running' and
(\<lambda>s. 0 < ksDomainTime s) and valid_domain_list'\<rbrace>"
apply (simp add: doUserOp_def split_def ex_abs_def)
apply (wp device_update_invs' doMachineOp_ct_running' select_wp
apply (wp device_update_invs' select_wp
| (wp (once) dmo_invs', wpsimp simp: no_irq_modify device_memory_update_def
user_memory_update_def))+
apply (clarsimp simp: user_memory_update_def simpler_modify_def
@ -532,13 +542,23 @@ lemma Ex_Some_conv:
text \<open>The top-level correspondence\<close>
lemma kernel_corres:
lemma kernel_corres':
"corres dc (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (ct_running or ct_idle)
and (\<lambda>s. scheduler_action s = resume_cur_thread))
(invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (ct_running' or ct_idle') and
(\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and
(\<lambda>s. vs_valid_duplicates' (ksPSpace s)))
(call_kernel event) (callKernel event)"
(call_kernel event)
(do _ \<leftarrow> runExceptT $
handleEvent event `~catchError~`
(\<lambda>_. withoutPreemption $ do
irq <- doMachineOp (getActiveIRQ True);
when (isJust irq) $ handleInterrupt (fromJust irq)
od);
_ \<leftarrow> ThreadDecls_H.schedule;
activateThread
od)"
unfolding call_kernel_def callKernel_def
apply (simp add: call_kernel_def callKernel_def)
apply (rule corres_guard_imp)
apply (rule corres_split)
@ -581,6 +601,32 @@ lemma kernel_corres:
apply (clarsimp simp: active_from_running')
done
lemma kernel_corres:
"corres dc (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (ct_running or ct_idle) and
(\<lambda>s. scheduler_action s = resume_cur_thread) and
(\<lambda>s. 0 < domain_time s \<and> valid_domain_list s))
(invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (ct_running' or ct_idle') and
(\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and
(\<lambda>s. vs_valid_duplicates' (ksPSpace s)))
(call_kernel event) (callKernel event)"
unfolding callKernel_def K_bind_def
apply (rule corres_guard_imp)
apply (rule corres_add_noop_lhs2)
apply (simp only: bind_assoc[symmetric])
apply (rule corres_split[where r'=dc and
R="\<lambda>_ s. 0 < domain_time s \<and> valid_domain_list s" and
R'="\<lambda>_. \<top>"])
apply (rule corres_bind_return2, rule corres_stateAssert_assume_stronger)
apply simp
apply (simp add: kernelExitAssertions_def state_relation_def)
apply (simp only: bind_assoc)
apply (rule kernel_corres')
apply (wp call_kernel_domain_time_inv_det_ext call_kernel_domain_list_inv_det_ext)
apply wp
apply clarsimp
apply clarsimp
done
lemma user_mem_corres:
"corres (=) invs invs' (gets (\<lambda>x. g (user_mem x))) (gets (\<lambda>x. g (user_mem' x)))"
by (clarsimp simp add: gets_def get_def return_def bind_def

315
proof/refine/RISCV64/DomainTime_R.thy
View File

@ -1,315 +0,0 @@
(*
* Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
*
* SPDX-License-Identifier: GPL-2.0-only
*)
theory DomainTime_R
imports
ADT_H
begin
text \<open>Preservation of domain time remaining over kernel invocations;
invariance of domain list validity
\<close>
context begin interpretation Arch . (*FIXME: arch_split*)
(* abstract and haskell have identical domain list fields *)
abbreviation
valid_domain_list' :: "'a kernel_state_scheme \<Rightarrow> bool"
where
"valid_domain_list' \<equiv> \<lambda>s. valid_domain_list_2 (ksDomSchedule s)"
lemmas valid_domain_list'_def = valid_domain_list_2_def
(* first, crunching valid_domain_list' over the kernel - it is never changed *)
crunches sendFaultIPC, handleFault, replyFromKernel
for ksDomSchedule_inv[wp]: "\<lambda>s. P (ksDomSchedule s)"
crunch ksDomSchedule_inv[wp]: setDomain "\<lambda>s. P (ksDomSchedule s)"
(wp: crunch_wps simp: if_apply_def2)
crunch ksDomSchedule_inv[wp]: sendSignal "\<lambda>s. P (ksDomSchedule s)"
(wp: crunch_wps simp: crunch_simps simp: unless_def o_def)
crunch ksDomSchedule_inv[wp]: finaliseCap "\<lambda>s. P (ksDomSchedule s)"
(simp: crunch_simps assertE_def unless_def pteAtIndex_def
wp: getObject_inv loadObject_default_inv crunch_wps)
crunches finaliseCap, capSwapForDelete
for ksDomSchedule_inv[wp]: "\<lambda>s. P (ksDomSchedule s)"
(simp: crunch_simps simp: unless_def)
lemma finaliseSlot_ksDomSchedule_inv[wp]:
"\<lbrace>\<lambda>s. P (ksDomSchedule s) \<rbrace> finaliseSlot param_a param_b \<lbrace>\<lambda>_ s. P (ksDomSchedule s)\<rbrace>"
by (wp finaliseSlot_preservation | clarsimp)+
crunch ksDomSchedule_inv[wp]: invokeTCB "\<lambda>s. P (ksDomSchedule s)"
(wp: crunch_wps checkCap_inv finaliseSlot'_preservation simp: if_apply_def2 crunch_simps)
crunch ksDomSchedule_inv[wp]: doReplyTransfer "\<lambda>s. P (ksDomSchedule s)"
(wp: crunch_wps transferCapsToSlots_pres1 setObject_ep_ct
setObject_ntfn_ct
simp: unless_def crunch_simps
ignore: transferCapsToSlots)
crunch ksDomSchedule_inv[wp]: finaliseCap "\<lambda>s. P (ksDomSchedule s)"
(simp: crunch_simps assertE_def unless_def
wp: getObject_inv loadObject_default_inv crunch_wps)
crunch ksDomSchedule_inv[wp]: cancelBadgedSends "\<lambda>s. P (ksDomSchedule s)"
(simp: filterM_mapM crunch_simps
wp: crunch_wps hoare_unless_wp)
crunch ksDomSchedule_inv[wp]: createNewObjects "\<lambda>s. P (ksDomSchedule s)"
(simp: crunch_simps zipWithM_x_mapM wp: crunch_wps hoare_unless_wp)
crunch ksDomSchedule_inv[wp]: preemptionPoint "\<lambda>s. P (ksDomSchedule s)"
(simp: whenE_def ignore_del: preemptionPoint)
crunch ksDomSchedule_inv[wp]: performRISCVMMUInvocation "\<lambda>s. P (ksDomSchedule s)"
(wp: crunch_wps getObject_cte_inv getASID_wp
simp: unless_def crunch_simps)
crunch ksDomSchedule_inv[wp]: performInvocation "\<lambda>s. P (ksDomSchedule s)"
(wp: crunch_wps zipWithM_x_inv cteRevoke_preservation mapME_x_inv_wp
simp: unless_def crunch_simps filterM_mapM)
crunch ksDomSchedule_inv[wp]: schedule "\<lambda>s. P (ksDomSchedule s)"
(ignore: setNextPC threadSet simp: crunch_simps bitmap_fun_defs wp: findM_inv hoare_drop_imps)
crunch ksDomSchedule_inv[wp]: activateThread "\<lambda>s. P (ksDomSchedule s)"
crunches receiveSignal, getNotification, receiveIPC, deleteCallerCap
for ksDomSchedule_inv[wp]:
"\<lambda>s. P (ksDomSchedule s)"
(wp: hoare_drop_imps simp: crunch_simps)
lemma handleRecv_ksDomSchedule_inv[wp]:
"\<lbrace>\<lambda>s. P (ksDomSchedule s) \<rbrace> handleRecv e \<lbrace>\<lambda>_ s. P (ksDomSchedule s) \<rbrace>"
unfolding handleRecv_def
by (rule hoare_pre)
(wp hoare_drop_imps | simp add: crunch_simps | wpc)+
context
notes if_cong [cong]
begin
crunch ksDomSchedule_inv[wp]: handleEvent "\<lambda>s. P (ksDomSchedule s)"
(wp: syscall_valid' ignore: syscall)
end
lemma callKernel_ksDomSchedule_inv[wp]:
"\<lbrace>\<lambda>s. P (ksDomSchedule s) \<rbrace> callKernel e \<lbrace>\<lambda>_ s. P (ksDomSchedule s) \<rbrace>"
unfolding callKernel_def
by (rule hoare_pre)
(wp | simp add: if_apply_def2)+
(* now we handle preservation of domain time remaining, which most of the kernel does not change *)
crunches setExtraBadge, cteInsert, transferCapsToSlots, setupCallerCap, doIPCTransfer, possibleSwitchTo
for ksDomainTime[wp]: "\<lambda>s. P (ksDomainTime s)"
(wp: crunch_wps simp: zipWithM_x_mapM ignore: constOnFailure)
crunches setEndpoint, setNotification, storePTE
for ksDomainTime_inv[wp]: "\<lambda>s. P (ksDomainTime s)"
(wp: crunch_wps setObject_ksPSpace_only updateObject_default_inv)
crunches sendFaultIPC, handleFault, replyFromKernel
for ksDomainTime_inv[wp]: "\<lambda>s. P (ksDomainTime s)"
crunch ksDomainTime_inv[wp]: setDomain "\<lambda>s. P (ksDomainTime s)"
(wp: crunch_wps simp: if_apply_def2)
crunch ksDomainTime_inv[wp]: sendSignal "\<lambda>s. P (ksDomainTime s)"
(wp: crunch_wps simp: crunch_simps simp: unless_def o_def setBoundNotification_def)
crunch ksDomainTime_inv[wp]: deleteASID "\<lambda>s. P (ksDomainTime s)"
(wp: crunch_wps setObject_ksPSpace_only getObject_inv loadObject_default_inv
updateObject_default_inv
simp: crunch_simps)
crunch ksDomainTime_inv[wp]: setBoundNotification "\<lambda>s. P (ksDomainTime s)"
crunch ksDomainTime_inv[wp]: finaliseCap "\<lambda>s. P (ksDomainTime s)"
(simp: crunch_simps assertE_def unless_def pteAtIndex_def
wp: setObject_ksPSpace_only getObject_inv loadObject_default_inv crunch_wps)
crunch ksDomainTime_inv[wp]: cancelBadgedSends "\<lambda>s. P (ksDomainTime s)"
(wp: crunch_wps setObject_ksPSpace_only getObject_inv loadObject_default_inv
updateObject_default_inv hoare_unless_wp
simp: filterM_mapM crunch_simps)
crunch ksDomainTime_inv[wp]: capSwapForDelete "\<lambda>s. P (ksDomainTime s)"
(simp: crunch_simps)
lemma finaliseSlot_ksDomainTime_inv[wp]:
"\<lbrace>\<lambda>s. P (ksDomainTime s) \<rbrace> finaliseSlot param_a param_b \<lbrace>\<lambda>_ s. P (ksDomainTime s)\<rbrace>"
by (wp finaliseSlot_preservation | clarsimp)+
crunch ksDomainTime_inv[wp]: invokeTCB "\<lambda>s. P (ksDomainTime s)"
(wp: crunch_wps checkCap_inv finaliseSlot'_preservation simp: if_apply_def2 crunch_simps)
crunch ksDomainTime_inv[wp]: doReplyTransfer "\<lambda>s. P (ksDomainTime s)"
(wp: crunch_wps transferCapsToSlots_pres1 setObject_ep_ct
setObject_ntfn_ct
simp: unless_def crunch_simps
ignore: transferCapsToSlots)
crunch ksDomainTime_inv[wp]: finaliseCap "\<lambda>s. P (ksDomainTime s)"
(simp: crunch_simps assertE_def unless_def
wp: getObject_inv loadObject_default_inv crunch_wps)
crunch ksDomainTime_inv[wp]: cancelBadgedSends "\<lambda>s. P (ksDomainTime s)"
(simp: filterM_mapM crunch_simps
wp: crunch_wps)
crunch ksDomainTime_inv[wp]: createNewObjects "\<lambda>s. P (ksDomainTime s)"
(simp: crunch_simps zipWithM_x_mapM
wp: crunch_wps hoare_unless_wp)
crunch ksDomainTime_inv[wp]: performRISCVMMUInvocation "\<lambda>s. P (ksDomainTime s)"
(wp: crunch_wps getObject_cte_inv getASID_wp setObject_ksPSpace_only updateObject_default_inv
simp: unless_def crunch_simps)
crunch ksDomainTime_inv[wp]: preemptionPoint "\<lambda>s. P (ksDomainTime s)"
(simp: whenE_def ignore_del: preemptionPoint)
crunch ksDomainTime_inv[wp]: performInvocation "\<lambda>s. P (ksDomainTime s)"
(wp: crunch_wps zipWithM_x_inv cteRevoke_preservation mapME_x_inv_wp
simp: crunch_simps filterM_mapM)
crunch ksDomainTime_inv[wp]: activateThread "\<lambda>s. P (ksDomainTime s)"
crunches receiveSignal, getNotification, receiveIPC, deleteCallerCap
for ksDomainTime_inv[wp]: "\<lambda>s. P (ksDomainTime s)"
(wp: hoare_drop_imps simp: crunch_simps)
lemma handleRecv_ksDomainTime_inv[wp]:
"\<lbrace>\<lambda>s. P (ksDomainTime s) \<rbrace> handleRecv e \<lbrace>\<lambda>_ s. P (ksDomainTime s) \<rbrace>"
unfolding handleRecv_def
by (rule hoare_pre)
(wp hoare_drop_imps | simp add: crunch_simps | wpc)+
crunch ksDomainTime_inv[wp]: doUserOp "(\<lambda>s. P (ksDomainTime s))"
(wp: select_wp)
crunches getIRQState, chooseThread, handleYield
for ksDomainTime_inv[wp]: "(\<lambda>s. P (ksDomainTime s))"
(wp: crunch_wps)
crunches handleCall, handleSend, handleReply
for ksDomainTime_inv[wp]: "(\<lambda>s. P (ksDomainTime s))"
(wp: syscall_valid' crunch_wps simp: crunch_simps ignore: syscall)
crunches activateThread,handleHypervisorFault
for domain_time'_inv[wp]: "\<lambda>s. P (ksDomainTime s)"
lemma nextDomain_domain_time_left'[wp]:
"\<lbrace> valid_domain_list' \<rbrace>
nextDomain
\<lbrace>\<lambda>_ s. 0 < ksDomainTime s \<rbrace>"
unfolding nextDomain_def Let_def
apply (clarsimp simp: valid_domain_list'_def dschLength_def)
apply wp
apply clarsimp
apply (simp only: all_set_conv_all_nth)
apply (erule_tac x="Suc (ksDomScheduleIdx s) mod length (ksDomSchedule s)" in allE)
apply fastforce
done
lemma rescheduleRequired_ksSchedulerAction[wp]:
"\<lbrace>\<top>\<rbrace> rescheduleRequired \<lbrace>\<lambda>_ s. ksSchedulerAction s = ChooseNewThread \<rbrace>"
unfolding rescheduleRequired_def
by (wp setSchedulerAction_direct)
lemma timerTick_valid_domain_time:
"\<lbrace>\<lambda>s. 0 < ksDomainTime s\<rbrace>
timerTick
\<lbrace>\<lambda>_ s. ksDomainTime s = 0 \<longrightarrow> ksSchedulerAction s = ChooseNewThread\<rbrace>"
apply (simp add: timerTick_def numDomains_def)
apply wp
apply (rule_tac Q="\<lambda>_ s. ksSchedulerAction s = ChooseNewThread" in hoare_strengthen_post)
apply (wp | clarsimp simp: if_apply_def2)+
done
lemma handleInterrupt_valid_domain_time:
"\<lbrace>\<lambda>s. 0 < ksDomainTime s \<rbrace>
handleInterrupt i
\<lbrace>\<lambda>rv s. ksDomainTime s = 0 \<longrightarrow> ksSchedulerAction s = ChooseNewThread\<rbrace>"
apply (simp add: handleInterrupt_def)
apply (case_tac "maxIRQ < i"; simp)
subgoal by (wp hoare_false_imp) simp
apply (rule_tac B="\<lambda>_ s. 0 < ksDomainTime s" in hoare_seq_ext[rotated])
apply (rule hoare_pre, wp, simp)
apply (rename_tac st)
apply (case_tac st, simp_all)
(* IRQSignal : no timer tick, trivial preservation of ksDomainTime *)
apply (simp add: maskIrqSignal_def)
apply (rule_tac Q="\<lambda>_ s. 0 < ksDomainTime s" in hoare_post_imp, clarsimp)
apply (rule hoare_pre, (wp | wpc)+)
apply (rule_tac Q="\<lambda>_ s. 0 < ksDomainTime s" in hoare_post_imp, clarsimp)
apply wp
(* IRQTimer : tick occurs *) (* IRQReserved : trivial *)
apply (wp timerTick_valid_domain_time
| clarsimp simp: handleReservedIRQ_def
| wp (once) hoare_vcg_imp_lift)+
done
lemma schedule_domain_time_left':
"\<lbrace> valid_domain_list' and
(\<lambda>s. ksDomainTime s = 0 \<longrightarrow> ksSchedulerAction s = ChooseNewThread) \<rbrace>
ThreadDecls_H.schedule
\<lbrace>\<lambda>_ s. 0 < ksDomainTime s \<rbrace>"
unfolding schedule_def scheduleChooseNewThread_def
supply word_neq_0_conv[simp]
apply wpsimp+
apply (rule_tac Q="\<lambda>_. valid_domain_list'" in hoare_post_imp, clarsimp)
apply (wp | clarsimp | wp (once) hoare_drop_imps)+
done
lemma handleEvent_ksDomainTime_inv:
"\<lbrace>\<lambda>s. P (ksDomainTime s) \<and> e \<noteq> Interrupt \<rbrace>
handleEvent e
\<lbrace>\<lambda>_ s. P (ksDomainTime s) \<rbrace>"
apply (cases e, simp_all)
apply (rename_tac syscall)
apply (case_tac syscall, simp_all add: handle_send_def)
apply (wp hv_inv'|simp add: handleEvent_def cong: if_cong|wpc)+
done
lemma callKernel_domain_time_left:
"\<lbrace> (\<lambda>s. 0 < ksDomainTime s) and valid_domain_list' and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_running' s) \<rbrace>
callKernel e
\<lbrace>\<lambda>_ s. 0 < ksDomainTime s \<rbrace>"
including no_pre
unfolding callKernel_def
supply word_neq_0_conv[simp]
apply (case_tac "e = Interrupt")
apply (simp add: handleEvent_def)
apply (rule hoare_pre)
apply ((wp schedule_domain_time_left' handleInterrupt_valid_domain_time
| wpc | simp)+)[1]
apply (rule_tac Q="\<lambda>_ s. 0 < ksDomainTime s \<and> valid_domain_list' s" in hoare_post_imp)
apply fastforce
apply wp
apply simp
(* non-interrupt case; may throw but does not touch ksDomainTime in handleEvent *)
apply simp
apply ((wp schedule_domain_time_left' handleInterrupt_valid_domain_time
| simp add: if_apply_def2)+)[1]
apply (rule_tac Q="\<lambda>_ s. valid_domain_list' s \<and> 0 < ksDomainTime s" in hoare_post_imp)
apply fastforce
apply wp
apply simp
apply (rule hoare_pre)
apply (rule_tac Q="\<lambda>_ s. valid_domain_list' s \<and> 0 < ksDomainTime s"
in NonDetMonadVCG.hoare_post_impErr[rotated 2], assumption)
apply (wp handleEvent_ksDomainTime_inv | clarsimp)+
done
end
end

3
proof/refine/RISCV64/EmptyFail_H.thy
View File

@ -278,7 +278,8 @@ crunch (empty_fail) empty_fail: callKernel
theorem call_kernel_serial:
"\<lbrakk> (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (ct_running or ct_idle) and
(\<lambda>s. scheduler_action s = resume_cur_thread)) s;
(\<lambda>s. scheduler_action s = resume_cur_thread) and
(\<lambda>s. 0 < domain_time s \<and> valid_domain_list s)) s;
\<exists>s'. (s, s') \<in> state_relation \<and>
(invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (ct_running' or ct_idle') and
(\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) s' \<rbrakk>

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

@ -2371,7 +2371,7 @@ theorem callKernel_no_orphans [wp]:
callKernel e
\<lbrace> \<lambda>rv s. no_orphans s \<rbrace>"
unfolding callKernel_def
by (wpsimp wp: weak_if_wp schedule_invs')
by (wpsimp wp: weak_if_wp schedule_invs' hoare_drop_imps)
end

71
proof/refine/RISCV64/Refine.thy
View File

@ -11,7 +11,7 @@
theory Refine
imports
KernelInit_R
DomainTime_R
ADT_H
InitLemmas
PageTableDuplicates
begin
@ -397,9 +397,23 @@ lemma ckernel_invs:
apply (rule hoare_pre)
apply (wp activate_invs' activate_sch_act schedule_sch
schedule_sch_act_simple he_invs' schedule_invs'
hoare_drop_imps
| simp add: no_irq_getActiveIRQ)+
done
(* abstract and haskell have identical domain list fields *)
abbreviation valid_domain_list' :: "'a kernel_state_scheme \<Rightarrow> bool" where
"valid_domain_list' \<equiv> \<lambda>s. valid_domain_list_2 (ksDomSchedule s)"
lemmas valid_domain_list'_def = valid_domain_list_2_def
defs kernelExitAssertions_def:
"kernelExitAssertions s \<equiv> 0 < ksDomainTime s \<and> valid_domain_list' s"
lemma callKernel_domain_time_left:
"\<lbrace> \<top> \<rbrace> callKernel e \<lbrace>\<lambda>_ s. 0 < ksDomainTime s \<and> valid_domain_list' s \<rbrace>"
unfolding callKernel_def kernelExitAssertions_def by wpsimp
lemma doMachineOp_sch_act_simple:
"doMachineOp f \<lbrace>sch_act_simple\<rbrace>"
by (wp sch_act_simple_lift)
@ -482,6 +496,9 @@ lemma device_update_invs':
gets_def get_def bind_def valid_def return_def)
by (clarsimp simp: invs'_def valid_state'_def valid_irq_states'_def valid_machine_state'_def)
crunches doMachineOp
for ksDomainTime[wp]: "\<lambda>s. P (ksDomainTime s)"
lemma doUserOp_invs':
"\<lbrace>invs' and ex_abs einvs and
(\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_running' and
@ -503,12 +520,22 @@ lemma doUserOp_invs':
text \<open>The top-level correspondence\<close>
lemma kernel_corres:
lemma kernel_corres':
"corres dc (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (ct_running or ct_idle)
and (\<lambda>s. scheduler_action s = resume_cur_thread))
(invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (ct_running' or ct_idle') and
(\<lambda>s. ksSchedulerAction s = ResumeCurrentThread))
(call_kernel event) (callKernel event)"
(call_kernel event)
(do _ \<leftarrow> runExceptT $
handleEvent event `~catchError~`
(\<lambda>_. withoutPreemption $ do
irq <- doMachineOp (getActiveIRQ True);
when (isJust irq) $ handleInterrupt (fromJust irq)
od);
_ \<leftarrow> ThreadDecls_H.schedule;
activateThread
od)"
unfolding call_kernel_def callKernel_def
apply (simp add: call_kernel_def callKernel_def)
apply (rule corres_guard_imp)
apply (rule corres_split)
@ -525,9 +552,9 @@ lemma kernel_corres:
apply (simp add: when_def)
apply (rule corres_when, simp)
apply simp
apply (rule handle_interrupt_corres, simp)
apply (rule handle_interrupt_corres)
apply simp
apply (wp hoare_drop_imps)[1]
apply (wp hoare_drop_imps hoare_vcg_all_lift)[1]
apply simp
apply (rule_tac Q="\<lambda>irq s. invs' s \<and>
(\<forall>irq'. irq = Some irq' \<longrightarrow>
@ -541,15 +568,41 @@ lemma kernel_corres:
apply (simp add: invs'_def valid_state'_def)
apply (rule corres_split [OF _ schedule_corres])
apply (rule activate_corres)
apply (wp schedule_invs' hoare_vcg_if_lift2 hoare_drop_imps
handle_interrupt_valid_sched[unfolded non_kernel_IRQs_def, simplified] |simp)+
apply (rule_tac Q="\<lambda>_. valid_sched and invs and valid_list" and E="\<lambda>_. valid_sched and invs and valid_list"
apply (wp handle_interrupt_valid_sched[unfolded non_kernel_IRQs_def, simplified]
schedule_invs' hoare_vcg_if_lift2 hoare_drop_imps |simp)+
apply (rule_tac Q="\<lambda>_. valid_sched and invs and valid_list" and
E="\<lambda>_. valid_sched and invs and valid_list"
in hoare_post_impErr)
apply (wp handle_event_valid_sched |simp)+
apply (wp handle_event_valid_sched hoare_vcg_imp_lift' |simp)+
apply (clarsimp simp: active_from_running)
apply (clarsimp simp: active_from_running')
done
lemma kernel_corres:
"corres dc (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (ct_running or ct_idle) and
(\<lambda>s. scheduler_action s = resume_cur_thread) and
(\<lambda>s. 0 < domain_time s \<and> valid_domain_list s))
(invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (ct_running' or ct_idle') and
(\<lambda>s. ksSchedulerAction s = ResumeCurrentThread))
(call_kernel event) (callKernel event)"
unfolding callKernel_def K_bind_def
apply (rule corres_guard_imp)
apply (rule corres_add_noop_lhs2)
apply (simp only: bind_assoc[symmetric])
apply (rule corres_split[where r'=dc and
R="\<lambda>_ s. 0 < domain_time s \<and> valid_domain_list s" and
R'="\<lambda>_. \<top>"])
apply (rule corres_bind_return2, rule corres_stateAssert_assume_stronger)
apply simp
apply (simp add: kernelExitAssertions_def state_relation_def)
apply (simp only: bind_assoc)
apply (rule kernel_corres')
apply (wp call_kernel_domain_time_inv_det_ext call_kernel_domain_list_inv_det_ext)
apply wp
apply clarsimp
apply clarsimp
done
lemma user_mem_corres:
"corres (=) invs invs' (gets (\<lambda>x. g (user_mem x))) (gets (\<lambda>x. g (user_mem' x)))"
by (clarsimp simp add: gets_def get_def return_def bind_def

312
proof/refine/X64/DomainTime_R.thy
View File

@ -1,312 +0,0 @@
(*
* Copyright 2014, General Dynamics C4 Systems
*
* SPDX-License-Identifier: GPL-2.0-only
*)
theory DomainTime_R
imports
ADT_H
begin
text \<open>Preservation of domain time remaining over kernel invocations;
invariance of domain list validity
\<close>
context begin interpretation Arch . (*FIXME: arch_split*)
(* abstract and haskell have identical domain list fields *)
abbreviation
valid_domain_list' :: "'a kernel_state_scheme \<Rightarrow> bool"
where
"valid_domain_list' \<equiv> \<lambda>s. valid_domain_list_2 (ksDomSchedule s)"
lemmas valid_domain_list'_def = valid_domain_list_2_def
(* first, crunching valid_domain_list' over the kernel - it is never changed *)
crunches sendFaultIPC, handleFault, replyFromKernel
for ksDomSchedule_inv[wp]: "\<lambda>s. P (ksDomSchedule s)"
crunch ksDomSchedule_inv[wp]: setDomain "\<lambda>s. P (ksDomSchedule s)"
(wp: crunch_wps simp: if_apply_def2)
crunch ksDomSchedule_inv[wp]: sendSignal "\<lambda>s. P (ksDomSchedule s)"
(wp: crunch_wps simp: crunch_simps simp: unless_def o_def)
crunch ksDomSchedule_inv[wp]: finaliseCap "\<lambda>s. P (ksDomSchedule s)"
(simp: crunch_simps assertE_def unless_def
wp: getObject_inv loadObject_default_inv crunch_wps)
crunches finaliseCap, capSwapForDelete
for ksDomSchedule_inv[wp]: "\<lambda>s. P (ksDomSchedule s)"
(simp: crunch_simps simp: unless_def)
lemma finaliseSlot_ksDomSchedule_inv[wp]:
"\<lbrace>\<lambda>s. P (ksDomSchedule s) \<rbrace> finaliseSlot param_a param_b \<lbrace>\<lambda>_ s. P (ksDomSchedule s)\<rbrace>"
by (wp finaliseSlot_preservation | clarsimp)+
crunch ksDomSchedule_inv[wp]: invokeTCB "\<lambda>s. P (ksDomSchedule s)"
(wp: crunch_wps checkCap_inv finaliseSlot'_preservation simp: if_apply_def2 crunch_simps)
crunch ksDomSchedule_inv[wp]: doReplyTransfer "\<lambda>s. P (ksDomSchedule s)"
(wp: crunch_wps transferCapsToSlots_pres1 setObject_ep_ct
setObject_ntfn_ct
simp: unless_def crunch_simps
ignore: transferCapsToSlots)
crunch ksDomSchedule_inv[wp]: finaliseCap "\<lambda>s. P (ksDomSchedule s)"
(simp: crunch_simps assertE_def unless_def
wp: getObject_inv loadObject_default_inv crunch_wps)
crunch ksDomSchedule_inv[wp]: cancelBadgedSends "\<lambda>s. P (ksDomSchedule s)"
(simp: filterM_mapM crunch_simps
wp: crunch_wps hoare_unless_wp)
crunch ksDomSchedule_inv[wp]: createNewObjects "\<lambda>s. P (ksDomSchedule s)"
(simp: crunch_simps zipWithM_x_mapM wp: crunch_wps hoare_unless_wp)
crunch ksDomSchedule_inv[wp]: preemptionPoint "\<lambda>s. P (ksDomSchedule s)"
(simp: whenE_def ignore_del: preemptionPoint)
crunches performX64MMUInvocation, performX64PortInvocation
for ksDomSchedule_inv[wp]: "\<lambda>s. P (ksDomSchedule s)"
(wp: crunch_wps getObject_cte_inv getASID_wp
simp: unless_def crunch_simps)
crunch ksDomSchedule_inv[wp]: performInvocation "\<lambda>s. P (ksDomSchedule s)"
(wp: crunch_wps zipWithM_x_inv cteRevoke_preservation mapME_x_inv_wp
simp: unless_def crunch_simps filterM_mapM)
crunch ksDomSchedule_inv[wp]: schedule "\<lambda>s. P (ksDomSchedule s)"
(ignore: setNextPC threadSet simp: crunch_simps bitmap_fun_defs wp:findM_inv hoare_drop_imps)
crunch ksDomSchedule_inv[wp]: activateThread "\<lambda>s. P (ksDomSchedule s)"
crunches receiveSignal, getNotification, receiveIPC, deleteCallerCap
for ksDomSchedule_inv[wp]: "\<lambda>s. P (ksDomSchedule s)"
(wp: hoare_drop_imps simp: crunch_simps)
lemma handleRecv_ksDomSchedule_inv[wp]:
"\<lbrace>\<lambda>s. P (ksDomSchedule s) \<rbrace> handleRecv e \<lbrace>\<lambda>_ s. P (ksDomSchedule s) \<rbrace>"
unfolding handleRecv_def
by (rule hoare_pre)
(wp hoare_drop_imps | simp add: crunch_simps | wpc)+
context
notes if_cong [cong]
begin
crunch ksDomSchedule_inv[wp]: handleEvent "\<lambda>s. P (ksDomSchedule s)"
(wp: syscall_valid' ignore: syscall)
end
lemma callKernel_ksDomSchedule_inv[wp]:
"\<lbrace>\<lambda>s. P (ksDomSchedule s) \<rbrace> callKernel e \<lbrace>\<lambda>_ s. P (ksDomSchedule s) \<rbrace>"
unfolding callKernel_def
by (rule hoare_pre)
(wp | simp add: if_apply_def2)+
(* now we handle preservation of domain time remaining, which most of the kernel does not change *)
crunches setExtraBadge, cteInsert, transferCapsToSlots, setupCallerCap, doIPCTransfer, possibleSwitchTo
for ksDomainTime[wp]: "\<lambda>s. P (ksDomainTime s)"
(wp: crunch_wps simp: zipWithM_x_mapM ignore: constOnFailure)
crunches setEndpoint, setNotification, storePTE, storePDE, storePDPTE, storePML4E
for ksDomainTime_inv[wp]: "\<lambda>s. P (ksDomainTime s)"
(wp: crunch_wps setObject_ksPSpace_only updateObject_default_inv)
crunches sendFaultIPC, handleFault, replyFromKernel
for ksDomainTime_inv[wp]: "\<lambda>s. P (ksDomainTime s)"
crunch ksDomainTime_inv[wp]: setDomain "\<lambda>s. P (ksDomainTime s)"
(wp: crunch_wps simp: if_apply_def2)
crunch ksDomainTime_inv[wp]: sendSignal "\<lambda>s. P (ksDomainTime s)"
(wp: crunch_wps simp: crunch_simps simp: unless_def o_def)
crunch ksDomainTime_inv[wp]: deleteASID "\<lambda>s. P (ksDomainTime s)"
(wp: crunch_wps setObject_ksPSpace_only getObject_inv loadObject_default_inv
updateObject_default_inv
simp: crunch_simps)
crunch ksDomainTime_inv[wp]: finaliseCap "\<lambda>s. P (ksDomainTime s)"
(simp: crunch_simps assertE_def unless_def
wp: setObject_ksPSpace_only getObject_inv loadObject_default_inv crunch_wps)
crunch ksDomainTime_inv[wp]: cancelBadgedSends "\<lambda>s. P (ksDomainTime s)"
(wp: crunch_wps setObject_ksPSpace_only getObject_inv loadObject_default_inv
updateObject_default_inv hoare_unless_wp
simp: filterM_mapM crunch_simps)
crunch ksDomainTime_inv[wp]: capSwapForDelete "\<lambda>s. P (ksDomainTime s)"
(simp: crunch_simps)
lemma finaliseSlot_ksDomainTime_inv[wp]:
"\<lbrace>\<lambda>s. P (ksDomainTime s) \<rbrace> finaliseSlot param_a param_b \<lbrace>\<lambda>_ s. P (ksDomainTime s)\<rbrace>"
by (wp finaliseSlot_preservation | clarsimp)+
crunch ksDomainTime_inv[wp]: invokeTCB "\<lambda>s. P (ksDomainTime s)"
(wp: crunch_wps checkCap_inv finaliseSlot'_preservation simp: if_apply_def2 crunch_simps)
crunch ksDomainTime_inv[wp]: doReplyTransfer "\<lambda>s. P (ksDomainTime s)"
(wp: crunch_wps transferCapsToSlots_pres1 setObject_ep_ct
setObject_ntfn_ct
simp: unless_def crunch_simps
ignore: transferCapsToSlots)
crunch ksDomainTime_inv[wp]: finaliseCap "\<lambda>s. P (ksDomainTime s)"
(simp: crunch_simps assertE_def unless_def
wp: getObject_inv loadObject_default_inv crunch_wps)
crunch ksDomainTime_inv[wp]: cancelBadgedSends "\<lambda>s. P (ksDomainTime s)"
(simp: filterM_mapM crunch_simps
wp: crunch_wps)
crunch ksDomainTime_inv[wp]: createNewObjects "\<lambda>s. P (ksDomainTime s)"
(simp: crunch_simps zipWithM_x_mapM
wp: crunch_wps hoare_unless_wp)
crunches performX64MMUInvocation, performX64PortInvocation
for ksDomainTime_inv[wp]: "\<lambda>s. P (ksDomainTime s)"
(wp: crunch_wps getObject_cte_inv getASID_wp setObject_ksPSpace_only updateObject_default_inv
simp: unless_def crunch_simps)
crunch ksDomainTime_inv[wp]: preemptionPoint "\<lambda>s. P (ksDomainTime s)"
(simp: whenE_def ignore_del: preemptionPoint)
crunch ksDomainTime_inv[wp]: performInvocation "\<lambda>s. P (ksDomainTime s)"
(wp: crunch_wps zipWithM_x_inv cteRevoke_preservation mapME_x_inv_wp
simp: crunch_simps filterM_mapM)
crunch ksDomainTime_inv[wp]: activateThread "\<lambda>s. P (ksDomainTime s)"
crunches receiveSignal, getNotification, receiveIPC, deleteCallerCap
for ksDomainTime_inv[wp]: "\<lambda>s. P (ksDomainTime s)"
(wp: hoare_drop_imps simp: crunch_simps)
lemma handleRecv_ksDomainTime_inv[wp]:
"\<lbrace>\<lambda>s. P (ksDomainTime s) \<rbrace> handleRecv e \<lbrace>\<lambda>_ s. P (ksDomainTime s) \<rbrace>"
unfolding handleRecv_def
by (rule hoare_pre)
(wp hoare_drop_imps | simp add: crunch_simps | wpc)+
crunch ksDomainTime_inv[wp]: doUserOp "(\<lambda>s. P (ksDomainTime s))"
(wp: select_wp)
crunches getIRQState, chooseThread, handleYield
for ksDomainTime_inv[wp]: "(\<lambda>s. P (ksDomainTime s))"
crunches handleCall, handleSend, handleReply
for ksDomainTime_inv[wp]: "(\<lambda>s. P (ksDomainTime s))"
(wp: syscall_valid' ignore: syscall)
crunches activateThread, handleHypervisorFault
for domain_time'_inv[wp]: "\<lambda>s. P (ksDomainTime s)"
lemma nextDomain_domain_time_left'[wp]:
"\<lbrace> valid_domain_list' \<rbrace>
nextDomain
\<lbrace>\<lambda>_ s. 0 < ksDomainTime s \<rbrace>"
unfolding nextDomain_def Let_def
apply (clarsimp simp: valid_domain_list'_def dschLength_def)
apply wp
apply clarsimp
apply (simp only: all_set_conv_all_nth)
apply (erule_tac x="Suc (ksDomScheduleIdx s) mod length (ksDomSchedule s)" in allE)
apply fastforce
done
lemma rescheduleRequired_ksSchedulerAction[wp]:
"\<lbrace>\<top>\<rbrace> rescheduleRequired \<lbrace>\<lambda>_ s. ksSchedulerAction s = ChooseNewThread \<rbrace>"
unfolding rescheduleRequired_def
by (wp setSchedulerAction_direct)
lemma timerTick_valid_domain_time:
"\<lbrace>\<lambda>s. 0 < ksDomainTime s\<rbrace>
timerTick
\<lbrace>\<lambda>_ s. ksDomainTime s = 0 \<longrightarrow> ksSchedulerAction s = ChooseNewThread\<rbrace>"
apply (simp add: timerTick_def numDomains_def)
apply wp
apply (rule_tac Q="\<lambda>_ s. ksSchedulerAction s = ChooseNewThread" in hoare_strengthen_post)
apply (wp | clarsimp simp: if_apply_def2)+
done
lemma handleInterrupt_valid_domain_time:
"\<lbrace>\<lambda>s. 0 < ksDomainTime s \<rbrace>
handleInterrupt i
\<lbrace>\<lambda>rv s. ksDomainTime s = 0 \<longrightarrow> ksSchedulerAction s = ChooseNewThread\<rbrace>"
apply (simp add: handleInterrupt_def)
apply (case_tac "maxIRQ < i"; simp)
subgoal by (wp hoare_false_imp) simp
apply (rule_tac B="\<lambda>_ s. 0 < ksDomainTime s" in hoare_seq_ext[rotated])
apply (rule hoare_pre, wp, simp)
apply (rename_tac st)
apply (case_tac st, simp_all add: maskIrqSignal_def)
(* IRQSignal : no timer tick, trivial preservation of ksDomainTime *)
apply (rule_tac Q="\<lambda>_ s. 0 < ksDomainTime s" in hoare_post_imp, clarsimp)
apply (rule hoare_pre, (wp | wpc)+)
apply (rule_tac Q="\<lambda>_ s. 0 < ksDomainTime s" in hoare_post_imp, clarsimp)
apply wp
(* IRQTimer : tick occurs *) (* IRQReserved : trivial *)
apply (wp timerTick_valid_domain_time
| clarsimp simp: handleReservedIRQ_def
| wp (once) hoare_vcg_imp_lift)+
done
lemma schedule_domain_time_left':
"\<lbrace> valid_domain_list' and
(\<lambda>s. ksDomainTime s = 0 \<longrightarrow> ksSchedulerAction s = ChooseNewThread) \<rbrace>
ThreadDecls_H.schedule
\<lbrace>\<lambda>_ s. 0 < ksDomainTime s \<rbrace>"
unfolding schedule_def scheduleChooseNewThread_def
supply word_neq_0_conv[simp]
apply wpsimp+
apply (rule_tac Q="\<lambda>_. valid_domain_list'" in hoare_post_imp, clarsimp)
apply (wp | clarsimp | wp (once) hoare_drop_imps)+
done
lemma handleEvent_ksDomainTime_inv:
"\<lbrace>\<lambda>s. P (ksDomainTime s) \<and> e \<noteq> Interrupt \<rbrace>
handleEvent e
\<lbrace>\<lambda>_ s. P (ksDomainTime s) \<rbrace>"
apply (cases e, simp_all)
apply (rename_tac syscall)
apply (case_tac syscall, simp_all add: handle_send_def)
apply (wp hv_inv'|simp add: handleEvent_def cong: if_cong|wpc)+
done
lemma callKernel_domain_time_left:
"\<lbrace> (\<lambda>s. 0 < ksDomainTime s) and valid_domain_list' and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_running' s) \<rbrace>
callKernel e
\<lbrace>\<lambda>_ s. 0 < ksDomainTime s \<rbrace>"
including no_pre
unfolding callKernel_def
supply word_neq_0_conv[simp]
apply (case_tac "e = Interrupt")
apply (simp add: handleEvent_def)
apply (rule hoare_pre)
apply ((wp schedule_domain_time_left' handleInterrupt_valid_domain_time
| wpc | simp)+)[1]
apply (rule_tac Q="\<lambda>_ s. 0 < ksDomainTime s \<and> valid_domain_list' s" in hoare_post_imp)
apply fastforce
apply wp
apply simp
(* non-interrupt case; may throw but does not touch ksDomainTime in handleEvent *)
apply simp
apply ((wp schedule_domain_time_left' handleInterrupt_valid_domain_time
| simp add: if_apply_def2)+)[1]
apply (rule_tac Q="\<lambda>_ s. valid_domain_list' s \<and> 0 < ksDomainTime s" in hoare_post_imp)
apply fastforce
apply wp
apply simp
apply (rule hoare_pre)
apply (rule_tac Q="\<lambda>_ s. valid_domain_list' s \<and> 0 < ksDomainTime s"
in NonDetMonadVCG.hoare_post_impErr[rotated 2], assumption)
apply (wp handleEvent_ksDomainTime_inv | clarsimp)+
done
end
end

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

@ -284,7 +284,8 @@ crunch (empty_fail) empty_fail: callKernel
theorem call_kernel_serial:
"\<lbrakk> (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (ct_running or ct_idle) and
(\<lambda>s. scheduler_action s = resume_cur_thread)) s;
(\<lambda>s. scheduler_action s = resume_cur_thread) and
(\<lambda>s. 0 < domain_time s \<and> valid_domain_list s)) s;
\<exists>s'. (s, s') \<in> state_relation \<and>
(invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (ct_running' or ct_idle') and
(\<lambda>s. ksSchedulerAction s = ResumeCurrentThread)) s' \<rbrakk>

2429
proof/refine/X64/Orphanage.thy
View File

File diff suppressed because it is too large Load Diff

4
proof/refine/X64/PageTableDuplicates.thy
View File

@ -10,10 +10,6 @@ begin
context begin interpretation Arch . (*FIXME: arch_split*)
(* we need the following lemma in Syscall_R *)
crunch inv[wp]: getRegister "P"
lemma doMachineOp_ksPSpace_inv[wp]:
"\<lbrace>\<lambda>s. P (ksPSpace s)\<rbrace> doMachineOp f \<lbrace>\<lambda>ya s. P (ksPSpace s)\<rbrace>"
by (simp add:doMachineOp_def split_def | wp)+

73
proof/refine/X64/Refine.thy
View File

@ -11,7 +11,7 @@
theory Refine
imports
KernelInit_R
DomainTime_R
ADT_H
InitLemmas
PageTableDuplicates
begin
@ -401,15 +401,22 @@ lemma ckernel_invs:
apply (rule hoare_pre)
apply (wp activate_invs' activate_sch_act schedule_sch
schedule_sch_act_simple he_invs' schedule_invs'
hoare_drop_imp[where R="\<lambda>_. kernelExitAssertions"]
| simp add: no_irq_getActiveIRQ)+
done
lemma doMachineOp_ct_running':
"\<lbrace>ct_running'\<rbrace> doMachineOp f \<lbrace>\<lambda>_. ct_running'\<rbrace>"
apply (simp add: ct_in_state'_def doMachineOp_def split_def)
apply wp
apply (simp add: pred_tcb_at'_def o_def)
done
(* abstract and haskell have identical domain list fields *)
abbreviation valid_domain_list' :: "'a kernel_state_scheme \<Rightarrow> bool" where
"valid_domain_list' \<equiv> \<lambda>s. valid_domain_list_2 (ksDomSchedule s)"
lemmas valid_domain_list'_def = valid_domain_list_2_def
defs kernelExitAssertions_def:
"kernelExitAssertions s \<equiv> 0 < ksDomainTime s \<and> valid_domain_list' s"
lemma callKernel_domain_time_left:
"\<lbrace> \<top> \<rbrace> callKernel e \<lbrace>\<lambda>_ s. 0 < ksDomainTime s \<and> valid_domain_list' s \<rbrace>"
unfolding callKernel_def kernelExitAssertions_def by wpsimp
lemma kernelEntry_invs':
"\<lbrace> invs' and (\<lambda>s. e \<noteq> Interrupt \<longrightarrow> ct_running' s) and
@ -424,7 +431,7 @@ lemma kernelEntry_invs':
apply (wp ckernel_invs callKernel_domain_time_left
threadSet_invs_trivial threadSet_ct_running' select_wp
TcbAcc_R.dmo_invs' static_imp_wp
doMachineOp_ct_running' doMachineOp_sch_act_simple
doMachineOp_sch_act_simple
callKernel_domain_time_left
| clarsimp simp: user_memory_update_def no_irq_def tcb_at_invs'
valid_domain_list'_def)+
@ -489,6 +496,9 @@ lemma device_update_invs':
gets_def get_def bind_def valid_def return_def)
by (clarsimp simp: invs'_def valid_state'_def valid_irq_states'_def valid_machine_state'_def)
crunches doMachineOp
for ksDomainTime[wp]: "\<lambda>s. P (ksDomainTime s)"
lemma doUserOp_invs':
"\<lbrace>invs' and ex_abs einvs and
(\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_running' and
@ -498,7 +508,7 @@ lemma doUserOp_invs':
(\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_running' and
(\<lambda>s. 0 < ksDomainTime s) and valid_domain_list'\<rbrace>"
apply (simp add: doUserOp_def split_def ex_abs_def)
apply (wp device_update_invs' doMachineOp_ct_running' select_wp
apply (wp device_update_invs' select_wp
| (wp (once) dmo_invs', wpsimp simp: no_irq_modify device_memory_update_def
user_memory_update_def))+
apply (clarsimp simp: user_memory_update_def simpler_modify_def
@ -510,12 +520,21 @@ lemma doUserOp_invs':
text \<open>The top-level correspondence\<close>
lemma kernel_corres:
lemma kernel_corres':
"corres dc (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (ct_running or ct_idle)
and (\<lambda>s. scheduler_action s = resume_cur_thread))
(invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (ct_running' or ct_idle') and
(\<lambda>s. ksSchedulerAction s = ResumeCurrentThread))
(call_kernel event) (callKernel event)"
(call_kernel event)
(do _ \<leftarrow> runExceptT $
handleEvent event `~catchError~`
(\<lambda>_. withoutPreemption $ do
irq <- doMachineOp (getActiveIRQ True);
when (isJust irq) $ handleInterrupt (fromJust irq)
od);
_ \<leftarrow> ThreadDecls_H.schedule;
activateThread
od)"
apply (simp add: call_kernel_def callKernel_def)
apply (rule corres_guard_imp)
apply (rule corres_split)
@ -569,6 +588,33 @@ lemma device_mem_corres:
invs_def invs'_def
corres_underlying_def device_mem_relation)
lemma kernel_corres:
"corres dc (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and (ct_running or ct_idle) and
(\<lambda>s. scheduler_action s = resume_cur_thread) and
(\<lambda>s. 0 < domain_time s \<and> valid_domain_list s))
(invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and (ct_running' or ct_idle') and
(\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and
(\<lambda>s. vs_valid_duplicates' (ksPSpace s)))
(call_kernel event) (callKernel event)"
unfolding callKernel_def K_bind_def
apply (rule corres_guard_imp)
apply (rule corres_add_noop_lhs2)
apply (simp only: bind_assoc[symmetric])
apply (rule corres_split[where r'=dc and
R="\<lambda>_ s. 0 < domain_time s \<and> valid_domain_list s" and
R'="\<lambda>_. \<top>"])
apply (rule corres_bind_return2, rule corres_stateAssert_assume_stronger)
apply simp
apply (simp add: kernelExitAssertions_def state_relation_def)
apply (simp only: bind_assoc)
apply (rule kernel_corres')
apply (wp call_kernel_domain_time_inv_det_ext call_kernel_domain_list_inv_det_ext)
apply wp
apply clarsimp
apply clarsimp
done
lemma entry_corres:
"corres (=) (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and
(\<lambda>s. 0 < domain_time s) and valid_domain_list and (ct_running or ct_idle) and
@ -818,12 +864,11 @@ lemma ckernel_invariant:
apply (rule valid_corres_combined[OF do_user_op_invs2 corres_guard_imp2[OF do_user_op_corres]])
apply clarsimp
apply (rule doUserOp_invs'[THEN hoare_weaken_pre])
apply (fastforce simp: ex_abs_def domain_time_rel_eq domain_list_rel_eq)
apply (fastforce simp: ex_abs_def)
apply (clarsimp simp: invs_valid_objs' ex_abs_def, rule_tac x=s in exI,
clarsimp simp: ct_running_related sched_act_rct_related)
apply (clarsimp simp: ex_abs_def)
apply (fastforce simp: ex_abs_def ct_running_related sched_act_rct_related
domain_time_rel_eq)
apply (fastforce simp: ex_abs_def ct_running_related sched_act_rct_related)
apply (erule_tac P="a \<and> b \<and> c \<and> (\<exists>x. d x)" for a b c d in disjE)
apply (clarsimp simp add: do_user_op_H_def monad_to_transition_def)

4
spec/design/skel/API_H.thy
View File

@ -12,6 +12,8 @@ begin
text \<open>collects all API modules\<close>
#INCLUDE_HASKELL SEL4.lhs
#INCLUDE_HASKELL SEL4.lhs decls_only NOT callKernel
#INCLUDE_HASKELL SEL4.lhs NOT kernelExitAssertions
end

7
spec/haskell/src/SEL4.lhs
View File

@ -22,7 +22,7 @@ This is the top-level module; it defines the interface between the kernel and th
> import SEL4.API.Types
> import SEL4.Kernel.CSpace(lookupCap)
> import SEL4.Kernel.Thread(schedule, activateThread)
> import SEL4.Model.StateData(KernelState, Kernel, getCurThread, doMachineOp)
> import SEL4.Model.StateData(KernelState, Kernel, getCurThread, doMachineOp, stateAssert)
> import SEL4.Model.Preemption(withoutPreemption)
> import SEL4.Object.Structures
> import SEL4.Object.TCB(asUser)
@ -45,4 +45,9 @@ faults, and system calls; the set of possible events is defined in
> when (isJust irq) $ handleInterrupt (fromJust irq))
> schedule
> activateThread
> stateAssert kernelExitAssertions "Kernel exit conditions must hold"
This will be replaced by actual assertions in the proofs:
> kernelExitAssertions :: KernelState -> Bool
> kernelExitAssertions _ = True