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

armhyp/x64/riscv64 refine: remove interrupt/irq from p_monad 

- fix armhyp/x64/riscv64 Refine for the above change

Signed-off-by: Miki Tanaka <miki.tanaka@data61.csiro.au>
This commit is contained in:
Miki Tanaka 2020-10-24 12:42:34 +11:00 committed by Miki Tanaka
parent b4893afd0b
commit 0b9c186eb0
24 changed files with 86 additions and 86 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -1377,7 +1377,7 @@ lemma perform_vcpu_invocation_corres:
lemma inv_arch_corres:
assumes "archinv_relation ai ai'"
shows "corres (intr \<oplus> (=))
shows "corres (dc \<oplus> (=))
(einvs and ct_active and valid_arch_inv ai)
(invs' and ct_active' and valid_arch_inv' ai' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)))
(arch_perform_invocation ai) (Arch.performInvocation ai')"

10
proof/refine/ARM_HYP/CNodeInv_R.thy
View File

@ -7005,7 +7005,7 @@ lemmas rec_del_valid_list_irq_state_independent[wp] =
lemma rec_del_corres:
"\<forall>C \<in> rec_del_concrete args.
spec_corres s (intr \<oplus> (case args of
spec_corres s (dc \<oplus> (case args of
FinaliseSlotCall _ _ \<Rightarrow> (\<lambda>r r'. fst r = fst r'
\<and> cap_relation (snd r) (snd r') )
| _ \<Rightarrow> dc))
@ -7035,7 +7035,7 @@ proof (induct rule: rec_del.induct,
split_def)
apply (rule spec_corres_guard_imp)
apply (rule spec_corres_splitE)
apply (rule "1.hyps"[simplified rec_del_concrete_unfold])
apply (rule "1.hyps"[simplified rec_del_concrete_unfold dc_def])
apply (rule drop_spec_corres)
apply (simp(no_asm) add: dc_def[symmetric] liftME_def[symmetric]
whenE_liftE)
@ -7406,7 +7406,7 @@ next
qed
lemma cap_delete_corres:
"corres (intr \<oplus> dc)
"corres (dc \<oplus> dc)
(einvs and simple_sched_action and cte_at ptr and emptyable ptr)
(invs' and sch_act_simple and cte_at' (cte_map ptr))
(cap_delete ptr) (cteDelete (cte_map ptr) True)"
@ -7655,7 +7655,7 @@ lemma cap_revoke_mdb_stuff4:
done
lemma cap_revoke_corres':
"spec_corres s (intr \<oplus> dc)
"spec_corres s (dc \<oplus> dc)
(einvs and simple_sched_action and cte_at ptr)
(invs' and sch_act_simple and cte_at' (cte_map ptr))
(cap_revoke ptr) (\<lambda>s. cteRevoke (cte_map ptr) s)"
@ -8744,7 +8744,7 @@ declare corres_False' [simp]
lemma inv_cnode_corres:
"cnodeinv_relation ci ci' \<Longrightarrow>
corres (intr \<oplus> dc)
corres (dc \<oplus> dc)
(einvs and simple_sched_action and valid_cnode_inv ci)
(invs' and sch_act_simple and valid_cnode_inv' ci')
(invoke_cnode ci) (invokeCNode ci')"

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

@ -100,7 +100,7 @@ lemma work_units_and_irq_state_state_relationI [intro!]:
by (simp add: state_relation_def swp_def)
lemma preemption_corres:
"corres (intr \<oplus> dc) \<top> \<top> preemption_point preemptionPoint"
"corres (dc \<oplus> dc) \<top> \<top> preemption_point preemptionPoint"
apply (simp add: preemption_point_def preemptionPoint_def)
by (auto simp: preemption_point_def preemptionPoint_def o_def gets_def liftE_def whenE_def getActiveIRQ_def
corres_underlying_def select_def bind_def get_def bindE_def select_f_def modify_def

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

@ -479,7 +479,7 @@ lemma setIRQTrigger_corres:
done
lemma arch_invoke_irq_control_corres:
"arch_irq_control_inv_relation x2 ivk' \<Longrightarrow> corres (intr \<oplus> dc)
"arch_irq_control_inv_relation x2 ivk' \<Longrightarrow> corres (dc \<oplus> dc)
(einvs and arch_irq_control_inv_valid x2)
(invs' and arch_irq_control_inv_valid' ivk')
(arch_invoke_irq_control x2)
@ -507,7 +507,7 @@ lemma arch_invoke_irq_control_corres:
lemma invoke_irq_control_corres:
"irq_control_inv_relation i i' \<Longrightarrow>
corres (intr \<oplus> dc) (einvs and irq_control_inv_valid i)
corres (dc \<oplus> dc) (einvs and irq_control_inv_valid i)
(invs' and irq_control_inv_valid' i')
(invoke_irq_control i)
(performIRQControl i')"

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

@ -573,9 +573,9 @@ lemma kernel_corres':
apply (rule_tac x=irqa in option_corres)
apply (rule_tac P=\<top> and P'=\<top> in corres_inst)
apply (simp add: when_def)
apply (rule corres_when, simp)
apply (rule corres_when[simplified dc_def], simp)
apply simp
apply (rule handle_interrupt_corres)
apply (rule handle_interrupt_corres[simplified dc_def])
apply simp
apply (wp hoare_drop_imps hoare_vcg_all_lift)[1]
apply simp

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

@ -42,7 +42,7 @@ lemma syscall_corres:
\<Longrightarrow> corres r (P_err rv err)
(P'_err rv' err') (h_err err) (h_err' err')"
"\<And>rvf rvf' rve rve'. \<lbrakk>r_flt_rel rvf rvf'; r_err_rel rvf rvf' rve rve'\<rbrakk>
\<Longrightarrow> corres (intr \<oplus> r)
\<Longrightarrow> corres (dc \<oplus> r)
(P_no_err rvf rve) (P'_no_err rvf' rve')
(m_fin rve) (m_fin' rve')"
@ -52,7 +52,7 @@ lemma syscall_corres:
"\<lbrace>Q\<rbrace> m_flt \<lbrace>\<lambda>rv. P_no_flt rv and Q_no_flt rv\<rbrace>, \<lbrace>P_flt\<rbrace>"
"\<lbrace>Q'\<rbrace> m_flt' \<lbrace>\<lambda>rv. P'_no_flt rv and Q'_no_flt rv\<rbrace>, \<lbrace>P'_flt\<rbrace>"
shows "corres (intr \<oplus> r) (P and Q) (P' and Q')
shows "corres (dc \<oplus> r) (P and Q) (P' and Q')
(Syscall_A.syscall m_flt h_flt m_err h_err m_fin)
(Syscall_H.syscall m_flt' h_flt' m_err' h_err' m_fin')"
apply (simp add: Syscall_A.syscall_def Syscall_H.syscall_def liftE_bindE)
@ -404,7 +404,7 @@ lemma set_domain_setDomain_corres:
lemma pinv_corres:
"\<lbrakk> inv_relation i i'; call \<longrightarrow> block \<rbrakk> \<Longrightarrow>
corres (intr \<oplus> (=))
corres (dc \<oplus> (=))
(einvs and valid_invocation i
and simple_sched_action
and ct_active
@ -1228,7 +1228,7 @@ crunch valid_duplicates'[wp]: setThreadState "\<lambda>s. vs_valid_duplicates' (
(*FIXME: move to NonDetMonadVCG.valid_validE_R *)
lemma hinv_corres:
"c \<longrightarrow> b \<Longrightarrow>
corres (intr \<oplus> dc)
corres (dc \<oplus> dc)
(einvs and (\<lambda>s. scheduler_action s = resume_cur_thread) and ct_active)
(invs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and
(\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_active')
@ -1383,7 +1383,7 @@ crunch typ_at'[wp]: handleFault "\<lambda>s. P (typ_at' T p s)"
lemmas handleFault_typ_ats[wp] = typ_at_lifts [OF handleFault_typ_at']
lemma hs_corres:
"corres (intr \<oplus> dc)
"corres (dc \<oplus> dc)
(einvs and (\<lambda>s. scheduler_action s = resume_cur_thread) and ct_active)
(invs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and
(\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_active')
@ -1810,7 +1810,7 @@ lemma hr_ct_active'[wp]:
done
lemma hc_corres:
"corres (intr \<oplus> dc) (einvs and (\<lambda>s. scheduler_action s = resume_cur_thread) and ct_active)
"corres (dc \<oplus> dc) (einvs and (\<lambda>s. scheduler_action s = resume_cur_thread) and ct_active)
(invs' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and
(\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and
ct_active')
@ -2024,7 +2024,7 @@ lemma hvmf_invs_etc:
done
lemma he_corres:
"corres (intr \<oplus> dc) (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and
"corres (dc \<oplus> dc) (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and
(\<lambda>s. scheduler_action s = resume_cur_thread))
(invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and
(\<lambda>s. vs_valid_duplicates' (ksPSpace s)) and

14
proof/refine/ARM_HYP/Tcb_R.thy
View File

@ -271,7 +271,7 @@ declare det_getRegister[simp]
declare det_setRegister[simp]
lemma readreg_corres:
"corres (intr \<oplus> (=))
"corres (dc \<oplus> (=))
(einvs and tcb_at src and ex_nonz_cap_to src)
(invs' and sch_act_simple and tcb_at' src and ex_nonz_cap_to' src)
(invoke_tcb (tcb_invocation.ReadRegisters src susp n arch))
@ -322,7 +322,7 @@ lemma arch_post_modify_registers_corres:
by simp+
lemma writereg_corres:
"corres (intr \<oplus> (=)) (einvs and tcb_at dest and ex_nonz_cap_to dest)
"corres (dc \<oplus> (=)) (einvs and tcb_at dest and ex_nonz_cap_to dest)
(invs' and sch_act_simple and tcb_at' dest and ex_nonz_cap_to' dest)
(invoke_tcb (tcb_invocation.WriteRegisters dest resume values arch))
(invokeTCB (tcbinvocation.WriteRegisters dest resume values arch'))"
@ -384,7 +384,7 @@ lemma suspend_ResumeCurrentThread_imp_notct[wp]:
by (wpsimp simp: suspend_def)
lemma copyreg_corres:
"corres (intr \<oplus> (=))
"corres (dc \<oplus> (=))
(einvs and simple_sched_action and tcb_at dest and tcb_at src and ex_nonz_cap_to src and
ex_nonz_cap_to dest)
(invs' and sch_act_simple and tcb_at' dest and tcb_at' src
@ -1272,7 +1272,7 @@ lemma tc_corres:
\<and> newroot_rel g'' g''')"
assumes sl: "{e, f, option_map undefined g} \<noteq> {None} \<longrightarrow> sl' = cte_map slot"
shows
"corres (intr \<oplus> (=))
"corres (dc \<oplus> (=))
(einvs and simple_sched_action and tcb_at a and
(\<lambda>s. {e, f, option_map undefined g} \<noteq> {None} \<longrightarrow> cte_at slot s) and
case_option \<top> (valid_cap o fst) e and
@ -1339,7 +1339,7 @@ proof -
have T: "\<And>x x' ref getfn target.
\<lbrakk> newroot_rel x x'; getfn = return (cte_map (target, ref));
x \<noteq> None \<longrightarrow> {e, f, option_map undefined g} \<noteq> {None} \<rbrakk> \<Longrightarrow>
corres (intr \<oplus> dc)
corres (dc \<oplus> dc)
(einvs and simple_sched_action and cte_at (target, ref) and emptyable (target, ref) and
(\<lambda>s. \<forall>(sl, c) \<in> (case x of None \<Rightarrow> {} | Some (c, sl) \<Rightarrow> {(sl, c), (slot, c)}).
@ -1385,7 +1385,7 @@ proof -
by (simp add: getThreadBufferSlot_def locateSlot_conv
cte_map_def tcb_cnode_index_def tcbIPCBufferSlot_def
cte_level_bits_def)
have T2: "corres (intr \<oplus> dc)
have T2: "corres (dc \<oplus> dc)
(einvs and simple_sched_action and tcb_at a and
(\<lambda>s. \<forall>(sl, c) \<in> (case g of None \<Rightarrow> {} | Some (x, v) \<Rightarrow> {(slot, cap.NullCap)} \<union>
(case v of None \<Rightarrow> {} | Some (c, sl) \<Rightarrow> {(sl, c), (slot, c)})).
@ -1814,7 +1814,7 @@ where
lemma tcbinv_corres:
"tcbinv_relation ti ti' \<Longrightarrow>
corres (intr \<oplus> (=))
corres (dc \<oplus> (=))
(einvs and simple_sched_action and Tcb_AI.tcb_inv_wf ti)
(invs' and sch_act_simple and tcb_inv_wf' ti')
(invoke_tcb ti) (invokeTCB ti')"

6
proof/refine/ARM_HYP/Untyped_R.thy
View File

@ -4239,7 +4239,7 @@ context begin interpretation Arch . (*FIXME: arch_split*)
lemma reset_untyped_cap_corres:
"untypinv_relation ui ui'
\<Longrightarrow> corres (intr \<oplus> dc)
\<Longrightarrow> corres (dc \<oplus> dc)
(invs and valid_untyped_inv_wcap ui
(Some (cap.UntypedCap dev ptr sz idx))
and ct_active and einvs
@ -4669,7 +4669,7 @@ context begin interpretation Arch . (*FIXME: arch_split*)
lemma inv_untyped_corres':
"\<lbrakk> untypinv_relation ui ui' \<rbrakk> \<Longrightarrow>
corres (intr \<oplus> (=))
corres (dc \<oplus> (=))
(einvs and valid_untyped_inv ui and ct_active)
(invs' and valid_untyped_inv' ui' and ct_active')
(invoke_untyped ui) (invokeUntyped ui')"
@ -4897,7 +4897,7 @@ lemma inv_untyped_corres':
note msimp[simp add] = neg_mask_add_mask
note if_split[split del]
show " corres (intr \<oplus> (=)) ((=) s) ((=) s')
show " corres (dc \<oplus> (=)) ((=) s) ((=) s')
(invoke_untyped ?ui)
(invokeUntyped ?ui')"
apply (clarsimp simp:invokeUntyped_def invoke_untyped_def getSlotCap_def bind_assoc)

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

@ -943,7 +943,7 @@ shows
lemma inv_arch_corres:
"archinv_relation ai ai' \<Longrightarrow>
corres (intr \<oplus> (=))
corres (dc \<oplus> (=))
(einvs and ct_active and valid_arch_inv ai)
(invs' and ct_active' and valid_arch_inv' ai')
(arch_perform_invocation ai) (Arch.performInvocation ai')"

10
proof/refine/RISCV64/CNodeInv_R.thy
View File

@ -6940,7 +6940,7 @@ lemmas rec_del_valid_list_irq_state_independent[wp] =
lemma rec_del_corres:
"\<forall>C \<in> rec_del_concrete args.
spec_corres s (intr \<oplus> (case args of
spec_corres s (dc \<oplus> (case args of
FinaliseSlotCall _ _ \<Rightarrow> (\<lambda>r r'. fst r = fst r'
\<and> cap_relation (snd r) (snd r') )
| _ \<Rightarrow> dc))
@ -6970,7 +6970,7 @@ proof (induct rule: rec_del.induct,
split_def)
apply (rule spec_corres_guard_imp)
apply (rule spec_corres_splitE)
apply (rule "1.hyps"[simplified rec_del_concrete_unfold])
apply (rule "1.hyps"[simplified rec_del_concrete_unfold dc_def])
apply (rule drop_spec_corres)
apply (simp(no_asm) add: dc_def[symmetric] liftME_def[symmetric]
whenE_liftE)
@ -7341,7 +7341,7 @@ next
qed
lemma cap_delete_corres:
"corres (intr \<oplus> dc)
"corres (dc \<oplus> dc)
(einvs and simple_sched_action and cte_at ptr and emptyable ptr)
(invs' and sch_act_simple and cte_at' (cte_map ptr))
(cap_delete ptr) (cteDelete (cte_map ptr) True)"
@ -7590,7 +7590,7 @@ lemma cap_revoke_mdb_stuff4:
done
lemma cap_revoke_corres':
"spec_corres s (intr \<oplus> dc)
"spec_corres s (dc \<oplus> dc)
(einvs and simple_sched_action and cte_at ptr)
(invs' and sch_act_simple and cte_at' (cte_map ptr))
(cap_revoke ptr) (\<lambda>s. cteRevoke (cte_map ptr) s)"
@ -8686,7 +8686,7 @@ declare corres_False' [simp]
lemma inv_cnode_corres:
"cnodeinv_relation ci ci' \<Longrightarrow>
corres (intr \<oplus> dc)
corres (dc \<oplus> dc)
(einvs and simple_sched_action and valid_cnode_inv ci)
(invs' and sch_act_simple and valid_cnode_inv' ci')
(invoke_cnode ci) (invokeCNode ci')"

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

@ -95,7 +95,7 @@ lemma work_units_and_irq_state_state_relationI [intro!]:
by (simp add: state_relation_def swp_def)
lemma preemption_corres:
"corres (intr \<oplus> dc) \<top> \<top> preemption_point preemptionPoint"
"corres (dc \<oplus> dc) \<top> \<top> preemption_point preemptionPoint"
apply (simp add: preemption_point_def preemptionPoint_def)
by (auto simp: preemption_point_def preemptionPoint_def o_def gets_def liftE_def whenE_def getActiveIRQ_def
corres_underlying_def select_def bind_def get_def bindE_def select_f_def modify_def

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

@ -488,7 +488,7 @@ lemma setIRQTrigger_corres:
done
lemma arch_invoke_irq_control_corres:
"arch_irq_control_inv_relation x2 ivk' \<Longrightarrow> corres (intr \<oplus> dc)
"arch_irq_control_inv_relation x2 ivk' \<Longrightarrow> corres (dc \<oplus> dc)
(einvs and arch_irq_control_inv_valid x2)
(invs' and arch_irq_control_inv_valid' ivk')
(arch_invoke_irq_control x2)
@ -516,7 +516,7 @@ lemma arch_invoke_irq_control_corres:
lemma invoke_irq_control_corres:
"irq_control_inv_relation i i' \<Longrightarrow>
corres (intr \<oplus> dc) (einvs and irq_control_inv_valid i)
corres (dc \<oplus> dc) (einvs and irq_control_inv_valid i)
(invs' and irq_control_inv_valid' i')
(invoke_irq_control i)
(performIRQControl i')"

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

@ -550,9 +550,9 @@ lemma kernel_corres':
apply (rule_tac x=irqa in option_corres)
apply (rule_tac P=\<top> and P'=\<top> in corres_inst)
apply (simp add: when_def)
apply (rule corres_when, simp)
apply (rule corres_when[simplified dc_def], simp)
apply simp
apply (rule handle_interrupt_corres)
apply (rule handle_interrupt_corres[simplified dc_def])
apply simp
apply (wp hoare_drop_imps hoare_vcg_all_lift)[1]
apply simp

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

@ -42,7 +42,7 @@ lemma syscall_corres:
\<Longrightarrow> corres r (P_err rv err)
(P'_err rv' err') (h_err err) (h_err' err')"
"\<And>rvf rvf' rve rve'. \<lbrakk>r_flt_rel rvf rvf'; r_err_rel rvf rvf' rve rve'\<rbrakk>
\<Longrightarrow> corres (intr \<oplus> r)
\<Longrightarrow> corres (dc \<oplus> r)
(P_no_err rvf rve) (P'_no_err rvf' rve')
(m_fin rve) (m_fin' rve')"
@ -52,7 +52,7 @@ lemma syscall_corres:
"\<lbrace>Q\<rbrace> m_flt \<lbrace>\<lambda>rv. P_no_flt rv and Q_no_flt rv\<rbrace>, \<lbrace>P_flt\<rbrace>"
"\<lbrace>Q'\<rbrace> m_flt' \<lbrace>\<lambda>rv. P'_no_flt rv and Q'_no_flt rv\<rbrace>, \<lbrace>P'_flt\<rbrace>"
shows "corres (intr \<oplus> r) (P and Q) (P' and Q')
shows "corres (dc \<oplus> r) (P and Q) (P' and Q')
(Syscall_A.syscall m_flt h_flt m_err h_err m_fin)
(Syscall_H.syscall m_flt' h_flt' m_err' h_err' m_fin')"
apply (simp add: Syscall_A.syscall_def Syscall_H.syscall_def liftE_bindE)
@ -402,7 +402,7 @@ lemma set_domain_setDomain_corres:
lemma pinv_corres:
"\<lbrakk> inv_relation i i'; call \<longrightarrow> block \<rbrakk> \<Longrightarrow>
corres (intr \<oplus> (=))
corres (dc \<oplus> (=))
(einvs and valid_invocation i
and simple_sched_action
and ct_active
@ -1186,7 +1186,7 @@ crunches reply_from_kernel
lemma hinv_corres:
"c \<longrightarrow> b \<Longrightarrow>
corres (intr \<oplus> dc)
corres (dc \<oplus> dc)
(einvs and (\<lambda>s. scheduler_action s = resume_cur_thread) and ct_active)
(invs' and
(\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_active')
@ -1341,7 +1341,7 @@ crunch typ_at'[wp]: handleFault "\<lambda>s. P (typ_at' T p s)"
lemmas handleFault_typ_ats[wp] = typ_at_lifts [OF handleFault_typ_at']
lemma hs_corres:
"corres (intr \<oplus> dc)
"corres (dc \<oplus> dc)
(einvs and (\<lambda>s. scheduler_action s = resume_cur_thread) and ct_active)
(invs' and
(\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_active')
@ -1768,7 +1768,7 @@ lemma hr_ct_active'[wp]:
done
lemma hc_corres:
"corres (intr \<oplus> dc) (einvs and (\<lambda>s. scheduler_action s = resume_cur_thread) and ct_active)
"corres (dc \<oplus> dc) (einvs and (\<lambda>s. scheduler_action s = resume_cur_thread) and ct_active)
(invs' and
(\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and
ct_active')
@ -1950,7 +1950,7 @@ lemma hh_corres:
(* FIXME: move *)
lemma he_corres:
"corres (intr \<oplus> dc) (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and
"corres (dc \<oplus> dc) (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and
(\<lambda>s. scheduler_action s = resume_cur_thread))
(invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and
(\<lambda>s. ksSchedulerAction s = ResumeCurrentThread))

14
proof/refine/RISCV64/Tcb_R.thy
View File

@ -275,7 +275,7 @@ lemma
by (simp add: getRegister_def)
lemma readreg_corres:
"corres (intr \<oplus> (=))
"corres (dc \<oplus> (=))
(einvs and tcb_at src and ex_nonz_cap_to src)
(invs' and sch_act_simple and tcb_at' src and ex_nonz_cap_to' src)
(invoke_tcb (tcb_invocation.ReadRegisters src susp n arch))
@ -314,7 +314,7 @@ lemma arch_post_modify_registers_corres:
by simp+
lemma writereg_corres:
"corres (intr \<oplus> (=)) (einvs and tcb_at dest and ex_nonz_cap_to dest)
"corres (dc \<oplus> (=)) (einvs and tcb_at dest and ex_nonz_cap_to dest)
(invs' and sch_act_simple and tcb_at' dest and ex_nonz_cap_to' dest)
(invoke_tcb (tcb_invocation.WriteRegisters dest resume values arch))
(invokeTCB (tcbinvocation.WriteRegisters dest resume values arch'))"
@ -373,7 +373,7 @@ lemma suspend_ResumeCurrentThread_imp_notct[wp]:
by (wpsimp simp: suspend_def)
lemma copyreg_corres:
"corres (intr \<oplus> (=))
"corres (dc \<oplus> (=))
(einvs and simple_sched_action and tcb_at dest and tcb_at src and ex_nonz_cap_to src and
ex_nonz_cap_to dest)
(invs' and sch_act_simple and tcb_at' dest and tcb_at' src
@ -1190,7 +1190,7 @@ lemma tc_corres:
\<and> newroot_rel g'' g''')"
and u: "{e, f, option_map undefined g} \<noteq> {None} \<longrightarrow> sl' = cte_map slot"
shows
"corres (intr \<oplus> (=))
"corres (dc \<oplus> (=))
(einvs and simple_sched_action and tcb_at a and
(\<lambda>s. {e, f, option_map undefined g} \<noteq> {None} \<longrightarrow> cte_at slot s) and
case_option \<top> (valid_cap o fst) e and
@ -1259,7 +1259,7 @@ proof -
have T: "\<And>x x' ref getfn target.
\<lbrakk> newroot_rel x x'; getfn = return (cte_map (target, ref));
x \<noteq> None \<longrightarrow> {e, f, option_map undefined g} \<noteq> {None} \<rbrakk> \<Longrightarrow>
corres (intr \<oplus> dc)
corres (dc \<oplus> dc)
(einvs and simple_sched_action and cte_at (target, ref) and emptyable (target, ref) and
(\<lambda>s. \<forall>(sl, c) \<in> (case x of None \<Rightarrow> {} | Some (c, sl) \<Rightarrow> {(sl, c), (slot, c)}).
cte_at sl s \<and> no_cap_to_obj_dr_emp c s \<and> valid_cap c s)
@ -1304,7 +1304,7 @@ proof -
by (simp add: getThreadBufferSlot_def locateSlot_conv
cte_map_def tcb_cnode_index_def tcbIPCBufferSlot_def
cte_level_bits_def)
have T2: "corres (intr \<oplus> dc)
have T2: "corres (dc \<oplus> dc)
(einvs and simple_sched_action and tcb_at a and
(\<lambda>s. \<forall>(sl, c) \<in> (case g of None \<Rightarrow> {} | Some (x, v) \<Rightarrow> {(slot, cap.NullCap)} \<union>
(case v of None \<Rightarrow> {} | Some (c, sl) \<Rightarrow> {(sl, c), (slot, c)})).
@ -1735,7 +1735,7 @@ where
lemma tcbinv_corres:
"tcbinv_relation ti ti' \<Longrightarrow>
corres (intr \<oplus> (=))
corres (dc \<oplus> (=))
(einvs and simple_sched_action and Tcb_AI.tcb_inv_wf ti)
(invs' and sch_act_simple and tcb_inv_wf' ti')
(invoke_tcb ti) (invokeTCB ti')"

6
proof/refine/RISCV64/Untyped_R.thy
View File

@ -4206,7 +4206,7 @@ context begin interpretation Arch . (*FIXME: arch_split*)
lemma reset_untyped_cap_corres:
"untypinv_relation ui ui'
\<Longrightarrow> corres (intr \<oplus> dc)
\<Longrightarrow> corres (dc \<oplus> dc)
(invs and valid_untyped_inv_wcap ui
(Some (cap.UntypedCap dev ptr sz idx))
and ct_active and einvs
@ -4632,7 +4632,7 @@ context begin interpretation Arch . (*FIXME: arch_split*)
lemma inv_untyped_corres':
"\<lbrakk> untypinv_relation ui ui' \<rbrakk> \<Longrightarrow>
corres (intr \<oplus> (=))
corres (dc \<oplus> (=))
(einvs and valid_untyped_inv ui and ct_active)
(invs' and valid_untyped_inv' ui' and ct_active')
(invoke_untyped ui) (invokeUntyped ui')"
@ -4877,7 +4877,7 @@ lemma inv_untyped_corres':
note msimp[simp add] = neg_mask_add_mask
note if_split[split del]
show " corres (intr \<oplus> (=)) ((=) s) ((=) s')
show " corres (dc \<oplus> (=)) ((=) s) ((=) s')
(invoke_untyped ?ui)
(invokeUntyped ?ui')"
apply (clarsimp simp:invokeUntyped_def invoke_untyped_def getSlotCap_def bind_assoc)

6
proof/refine/X64/Arch_R.thy
View File

@ -1336,7 +1336,7 @@ lemma port_out_corres[@lift_corres_args, corres]:
lemma perform_port_inv_corres:
"\<lbrakk>archinv_relation ai ai'; ai = arch_invocation.InvokeIOPort x\<rbrakk>
\<Longrightarrow> corres (intr \<oplus> (=))
\<Longrightarrow> corres (dc \<oplus> (=))
(einvs and ct_active and valid_arch_inv ai)
(invs' and ct_active' and valid_arch_inv' ai')
(liftE (perform_io_port_invocation x))
@ -1370,7 +1370,7 @@ lemma valid_ioports_issuedD':
lemma perform_ioport_control_inv_corres:
"\<lbrakk>archinv_relation ai ai'; ai = arch_invocation.InvokeIOPortControl x\<rbrakk> \<Longrightarrow>
corres (intr \<oplus> (=))
corres (dc \<oplus> (=))
(einvs and ct_active and valid_arch_inv ai)
(invs' and ct_active' and valid_arch_inv' ai')
(liftE (do perform_ioport_control_invocation x; return [] od))
@ -1422,7 +1422,7 @@ lemma arch_ioport_inv_case_simp:
lemma inv_arch_corres:
"archinv_relation ai ai' \<Longrightarrow>
corres (intr \<oplus> (=))
corres (dc \<oplus> (=))
(einvs and ct_active and valid_arch_inv ai)
(invs' and ct_active' and valid_arch_inv' ai')
(arch_perform_invocation ai) (Arch.performInvocation ai')"

10
proof/refine/X64/CNodeInv_R.thy
View File

@ -7078,7 +7078,7 @@ lemmas rec_del_valid_list_irq_state_independent[wp] =
lemma rec_del_corres:
"\<forall>C \<in> rec_del_concrete args.
spec_corres s (intr \<oplus> (case args of
spec_corres s (dc \<oplus> (case args of
FinaliseSlotCall _ _ \<Rightarrow> (\<lambda>r r'. fst r = fst r'
\<and> cap_relation (snd r) (snd r') )
| _ \<Rightarrow> dc))
@ -7108,7 +7108,7 @@ proof (induct rule: rec_del.induct,
split_def)
apply (rule spec_corres_guard_imp)
apply (rule spec_corres_splitE)
apply (rule "1.hyps"[simplified rec_del_concrete_unfold])
apply (rule "1.hyps"[simplified rec_del_concrete_unfold dc_def])
apply (rule drop_spec_corres)
apply (simp(no_asm) add: dc_def[symmetric] liftME_def[symmetric]
whenE_liftE)
@ -7479,7 +7479,7 @@ next
qed
lemma cap_delete_corres:
"corres (intr \<oplus> dc)
"corres (dc \<oplus> dc)
(einvs and simple_sched_action and cte_at ptr and emptyable ptr)
(invs' and sch_act_simple and cte_at' (cte_map ptr))
(cap_delete ptr) (cteDelete (cte_map ptr) True)"
@ -7728,7 +7728,7 @@ lemma cap_revoke_mdb_stuff4:
done
lemma cap_revoke_corres':
"spec_corres s (intr \<oplus> dc)
"spec_corres s (dc \<oplus> dc)
(einvs and simple_sched_action and cte_at ptr)
(invs' and sch_act_simple and cte_at' (cte_map ptr))
(cap_revoke ptr) (\<lambda>s. cteRevoke (cte_map ptr) s)"
@ -8871,7 +8871,7 @@ declare corres_False' [simp]
lemma inv_cnode_corres:
"cnodeinv_relation ci ci' \<Longrightarrow>
corres (intr \<oplus> dc)
corres (dc \<oplus> dc)
(einvs and simple_sched_action and valid_cnode_inv ci)
(invs' and sch_act_simple and valid_cnode_inv' ci')
(invoke_cnode ci) (invokeCNode ci')"

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

@ -96,7 +96,7 @@ lemma work_units_and_irq_state_state_relationI [intro!]:
by (simp add: state_relation_def swp_def)
lemma preemption_corres:
"corres (intr \<oplus> dc) \<top> \<top> preemption_point preemptionPoint"
"corres (dc \<oplus> dc) \<top> \<top> preemption_point preemptionPoint"
apply (simp add: preemption_point_def preemptionPoint_def)
by (auto simp: preemption_point_def preemptionPoint_def o_def gets_def liftE_def whenE_def getActiveIRQ_def
corres_underlying_def select_def bind_def get_def bindE_def select_f_def modify_def

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

@ -500,7 +500,7 @@ crunches X64_H.updateIRQState
(simp: ex_cte_cap_wp_to'_def valid_mdb'_def)
lemma arch_invoke_irq_control_corres:
"arch_irq_control_inv_relation x2 ivk' \<Longrightarrow> corres (intr \<oplus> dc)
"arch_irq_control_inv_relation x2 ivk' \<Longrightarrow> corres (dc \<oplus> dc)
(einvs and arch_irq_control_inv_valid x2)
(invs' and arch_irq_control_inv_valid' ivk')
(arch_invoke_irq_control x2)
@ -543,7 +543,7 @@ lemma arch_invoke_irq_control_corres:
lemma invoke_irq_control_corres:
"irq_control_inv_relation i i' \<Longrightarrow>
corres (intr \<oplus> dc) (einvs and irq_control_inv_valid i)
corres (dc \<oplus> dc) (einvs and irq_control_inv_valid i)
(invs' and irq_control_inv_valid' i')
(invoke_irq_control i)
(performIRQControl i')"

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

@ -549,9 +549,9 @@ lemma kernel_corres':
apply (rule_tac x=irqa in option_corres)
apply (rule_tac P=\<top> and P'=\<top> in corres_inst)
apply (simp add: when_def)
apply (rule corres_when, simp)
apply (rule corres_when[simplified dc_def], simp)
apply simp
apply (rule handle_interrupt_corres)
apply (rule handle_interrupt_corres[simplified dc_def])
apply simp
apply (wp hoare_drop_imps hoare_vcg_all_lift)[1]
apply simp

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

@ -42,7 +42,7 @@ lemma syscall_corres:
\<Longrightarrow> corres r (P_err rv err)
(P'_err rv' err') (h_err err) (h_err' err')"
"\<And>rvf rvf' rve rve'. \<lbrakk>r_flt_rel rvf rvf'; r_err_rel rvf rvf' rve rve'\<rbrakk>
\<Longrightarrow> corres (intr \<oplus> r)
\<Longrightarrow> corres (dc \<oplus> r)
(P_no_err rvf rve) (P'_no_err rvf' rve')
(m_fin rve) (m_fin' rve')"
@ -52,7 +52,7 @@ lemma syscall_corres:
"\<lbrace>Q\<rbrace> m_flt \<lbrace>\<lambda>rv. P_no_flt rv and Q_no_flt rv\<rbrace>, \<lbrace>P_flt\<rbrace>"
"\<lbrace>Q'\<rbrace> m_flt' \<lbrace>\<lambda>rv. P'_no_flt rv and Q'_no_flt rv\<rbrace>, \<lbrace>P'_flt\<rbrace>"
shows "corres (intr \<oplus> r) (P and Q) (P' and Q')
shows "corres (dc \<oplus> r) (P and Q) (P' and Q')
(Syscall_A.syscall m_flt h_flt m_err h_err m_fin)
(Syscall_H.syscall m_flt' h_flt' m_err' h_err' m_fin')"
apply (simp add: Syscall_A.syscall_def Syscall_H.syscall_def liftE_bindE)
@ -404,7 +404,7 @@ lemma set_domain_setDomain_corres:
lemma pinv_corres:
"\<lbrakk> inv_relation i i'; call \<longrightarrow> block \<rbrakk> \<Longrightarrow>
corres (intr \<oplus> (=))
corres (dc \<oplus> (=))
(einvs and valid_invocation i
and simple_sched_action
and ct_active
@ -1192,7 +1192,7 @@ lemmas set_thread_state_active_valid_sched =
(*FIXME: move to NonDetMonadVCG.valid_validE_R *)
lemma hinv_corres:
"c \<longrightarrow> b \<Longrightarrow>
corres (intr \<oplus> dc)
corres (dc \<oplus> dc)
(einvs and (\<lambda>s. scheduler_action s = resume_cur_thread) and ct_active)
(invs' and
(\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_active')
@ -1350,7 +1350,7 @@ crunch typ_at'[wp]: handleFault "\<lambda>s. P (typ_at' T p s)"
lemmas handleFault_typ_ats[wp] = typ_at_lifts [OF handleFault_typ_at']
lemma hs_corres:
"corres (intr \<oplus> dc)
"corres (dc \<oplus> dc)
(einvs and (\<lambda>s. scheduler_action s = resume_cur_thread) and ct_active)
(invs' and
(\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and ct_active')
@ -1780,7 +1780,7 @@ lemma hr_ct_active'[wp]:
done
lemma hc_corres:
"corres (intr \<oplus> dc) (einvs and (\<lambda>s. scheduler_action s = resume_cur_thread) and ct_active)
"corres (dc \<oplus> dc) (einvs and (\<lambda>s. scheduler_action s = resume_cur_thread) and ct_active)
(invs' and
(\<lambda>s. ksSchedulerAction s = ResumeCurrentThread) and
ct_active')
@ -1966,7 +1966,7 @@ lemma hh_corres:
(* FIXME: move *)
lemma he_corres:
"corres (intr \<oplus> dc) (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and
"corres (dc \<oplus> dc) (einvs and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running s) and
(\<lambda>s. scheduler_action s = resume_cur_thread))
(invs' and (\<lambda>s. event \<noteq> Interrupt \<longrightarrow> ct_running' s) and
(\<lambda>s. ksSchedulerAction s = ResumeCurrentThread))

14
proof/refine/X64/Tcb_R.thy
View File

@ -273,7 +273,7 @@ lemma
by (simp add: getRegister_def)
lemma readreg_corres:
"corres (intr \<oplus> (=))
"corres (dc \<oplus> (=))
(einvs and tcb_at src and ex_nonz_cap_to src)
(invs' and sch_act_simple and tcb_at' src and ex_nonz_cap_to' src)
(invoke_tcb (tcb_invocation.ReadRegisters src susp n arch))
@ -325,7 +325,7 @@ lemma arch_post_modify_registers_corres:
by simp+
lemma writereg_corres:
"corres (intr \<oplus> (=)) (einvs and tcb_at dest and ex_nonz_cap_to dest)
"corres (dc \<oplus> (=)) (einvs and tcb_at dest and ex_nonz_cap_to dest)
(invs' and sch_act_simple and tcb_at' dest and ex_nonz_cap_to' dest)
(invoke_tcb (tcb_invocation.WriteRegisters dest resume values arch))
(invokeTCB (tcbinvocation.WriteRegisters dest resume values arch'))"
@ -389,7 +389,7 @@ lemma suspend_ResumeCurrentThread_imp_notct[wp]:
by (wpsimp simp: suspend_def)
lemma copyreg_corres:
"corres (intr \<oplus> (=))
"corres (dc \<oplus> (=))
(einvs and simple_sched_action and tcb_at dest and tcb_at src and ex_nonz_cap_to src and
ex_nonz_cap_to dest)
(invs' and sch_act_simple and tcb_at' dest and tcb_at' src
@ -1216,7 +1216,7 @@ lemma tc_corres:
\<and> newroot_rel g'' g''')"
and u: "{e, f, option_map undefined g} \<noteq> {None} \<longrightarrow> sl' = cte_map slot"
shows
"corres (intr \<oplus> (=))
"corres (dc \<oplus> (=))
(einvs and simple_sched_action and tcb_at a and
(\<lambda>s. {e, f, option_map undefined g} \<noteq> {None} \<longrightarrow> cte_at slot s) and
case_option \<top> (valid_cap o fst) e and
@ -1283,7 +1283,7 @@ proof -
have T: "\<And>x x' ref getfn target.
\<lbrakk> newroot_rel x x'; getfn = return (cte_map (target, ref));
x \<noteq> None \<longrightarrow> {e, f, option_map undefined g} \<noteq> {None} \<rbrakk> \<Longrightarrow>
corres (intr \<oplus> dc)
corres (dc \<oplus> dc)
(einvs and simple_sched_action and cte_at (target, ref) and emptyable (target, ref) and
(\<lambda>s. \<forall>(sl, c) \<in> (case x of None \<Rightarrow> {} | Some (c, sl) \<Rightarrow> {(sl, c), (slot, c)}).
@ -1329,7 +1329,7 @@ proof -
by (simp add: getThreadBufferSlot_def locateSlot_conv
cte_map_def tcb_cnode_index_def tcbIPCBufferSlot_def
cte_level_bits_def)
have T2: "corres (intr \<oplus> dc)
have T2: "corres (dc \<oplus> dc)
(einvs and simple_sched_action and tcb_at a and
(\<lambda>s. \<forall>(sl, c) \<in> (case g of None \<Rightarrow> {} | Some (x, v) \<Rightarrow> {(slot, cap.NullCap)} \<union>
(case v of None \<Rightarrow> {} | Some (c, sl) \<Rightarrow> {(sl, c), (slot, c)})).
@ -1760,7 +1760,7 @@ where
lemma tcbinv_corres:
"tcbinv_relation ti ti' \<Longrightarrow>
corres (intr \<oplus> (=))
corres (dc \<oplus> (=))
(einvs and simple_sched_action and Tcb_AI.tcb_inv_wf ti)
(invs' and sch_act_simple and tcb_inv_wf' ti')
(invoke_tcb ti) (invokeTCB ti')"

6
proof/refine/X64/Untyped_R.thy
View File

@ -4323,7 +4323,7 @@ context begin interpretation Arch . (*FIXME: arch_split*)
lemma reset_untyped_cap_corres:
"untypinv_relation ui ui'
\<Longrightarrow> corres (intr \<oplus> dc)
\<Longrightarrow> corres (dc \<oplus> dc)
(invs and valid_untyped_inv_wcap ui
(Some (cap.UntypedCap dev ptr sz idx))
and ct_active and einvs
@ -4753,7 +4753,7 @@ context begin interpretation Arch . (*FIXME: arch_split*)
lemma inv_untyped_corres':
"\<lbrakk> untypinv_relation ui ui' \<rbrakk> \<Longrightarrow>
corres (intr \<oplus> (=))
corres (dc \<oplus> (=))
(einvs and valid_untyped_inv ui and ct_active)
(invs' and valid_untyped_inv' ui' and ct_active')
(invoke_untyped ui) (invokeUntyped ui')"
@ -4991,7 +4991,7 @@ lemma inv_untyped_corres':
note msimp[simp add] = neg_mask_add_mask
note if_split[split del]
show " corres (intr \<oplus> (=)) ((=) s) ((=) s')
show " corres (dc \<oplus> (=)) ((=) s) ((=) s')
(invoke_untyped ?ui)
(invokeUntyped ?ui')"
apply (clarsimp simp:invokeUntyped_def invoke_untyped_def getSlotCap_def bind_assoc)