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

refine+crefine: update refinement proofs 

Co-authored-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
Signed-off-by: Ryan Barry <ryan.barry@proofcraft.systems>
This commit is contained in:
Ryan Barry 2022-05-25 12:46:12 +10:00 committed by Ryan Barry
parent 0d344f0c2e
commit 9bf8cf35bb
5 changed files with 234 additions and 131 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

177
proof/crefine/ARM/Arch_C.thy
View File

@ -1514,7 +1514,7 @@ lemma performPageInvocationMapPTE_ccorres:
apply (cinit lift: pte_entries_' pte_' cap_' ctSlot_' asid_' )
apply (rule_tac P="\<exists>s. valid_pte_slots'2 mapping s" in ccorres_gen_asm)
apply (rule ccorres_gen_asm [where P ="snd (theLeft mapping)\<noteq>[]"])
apply (clarsimp simp: isLeft_def simp del: Collect_const)
apply (clarsimp simp: isLeft_def bind_assoc simp del: Collect_const)
apply (ctac (no_vcg))
apply (ctac (no_vcg) add: pteCheckIfMapped_ccorres)
apply csymbr
@ -1561,7 +1561,6 @@ lemma performPageInvocationMapPTE_ccorres:
apply (simp add: when_def del: Collect_const)
apply (rule ccorres_Cond_rhs_Seq)
apply (simp add: to_bool_def)
apply (rule ccorres_add_return2)
apply (ctac (no_vcg) add: invalidateTLBByASID_ccorres)
apply (rule_tac P=\<top> and P'=UNIV in ccorres_from_vcg_throws)
apply (rule allI, rule conseqPre, vcg)
@ -1775,7 +1774,7 @@ lemma performPageInvocationMapPDE_ccorres:
apply (cinit lift: pde_entries_' pde_' cap_' ctSlot_' asid_' )
apply (rule_tac P="\<exists>s. valid_pde_slots'2 mapping s" in ccorres_gen_asm)
apply (rule ccorres_gen_asm [where P ="snd (theRight mapping)\<noteq>[]"])
apply (clarsimp simp: isRight_def simp del: Collect_const)
apply (clarsimp simp: isRight_def bind_assoc simp del: Collect_const)
apply (ctac (no_vcg))
apply (ctac (no_vcg) add: pdeCheckIfMapped_ccorres)
apply csymbr
@ -1823,7 +1822,6 @@ lemma performPageInvocationMapPDE_ccorres:
apply (simp add: when_def del: Collect_const)
apply (rule ccorres_Cond_rhs_Seq)
apply (simp add: to_bool_def)
apply (rule ccorres_add_return2)
apply (ctac (no_vcg) add: invalidateTLBByASID_ccorres)
apply (rule_tac P=\<top> and P'=UNIV in ccorres_from_vcg_throws)
apply (rule allI, rule conseqPre, vcg)
@ -1885,6 +1883,130 @@ lemma performPageInvocationMapPDE_ccorres:
apply (auto simp: unat_arith_simps unat_word_ariths)
done
lemma setMRs_single:
"setMRs thread buffer [val] = do
_ \<leftarrow> asUser thread (setRegister register.R2 val);
return 1
od"
apply (clarsimp simp: setMRs_def length_msgRegisters n_msgRegisters_def zipWithM_x_def zipWith_def
split: option.splits)
apply (subst zip_commute, subst zip_singleton)
apply (simp add: length_msgRegisters n_msgRegisters_def length_0_conv[symmetric])
apply (clarsimp simp: msgRegisters_unfold sequence_x_def)
done
(* usually when we call setMR directly, we mean to only set a single message register
which will fit in actual registers *)
lemma setMR_as_setRegister_ccorres:
notes dc_simp[simp del]
shows
"ccorres (\<lambda>rv rv'. rv' = of_nat offset + 1) ret__unsigned_'
(tcb_at' thread and K (TCB_H.msgRegisters ! offset = reg \<and> offset < length msgRegisters))
(UNIV \<inter> \<lbrace>\<acute>reg = val\<rbrace>
\<inter> \<lbrace>\<acute>offset = of_nat offset\<rbrace>
\<inter> \<lbrace>\<acute>receiver = tcb_ptr_to_ctcb_ptr thread\<rbrace>) hs
(asUser thread (setRegister reg val))
(Call setMR_'proc)"
apply (rule ccorres_grab_asm)
apply (cinit' lift: reg_' offset_' receiver_')
apply (clarsimp simp: length_msgRegisters)
apply (rule ccorres_cond_false)
apply (rule ccorres_move_const_guards)
apply (rule ccorres_add_return2)
apply (ctac add: setRegister_ccorres)
apply (rule ccorres_from_vcg_throws[where P'=UNIV and P=\<top>])
apply (rule allI, rule conseqPre, vcg)
apply (clarsimp simp: dc_def return_def)
apply (rule hoare_post_taut[of \<top>])
apply (vcg exspec=setRegister_modifies)
apply (clarsimp simp: length_msgRegisters n_msgRegisters_def not_le conj_commute)
apply (subst msgRegisters_ccorres[symmetric])
apply (clarsimp simp: n_msgRegisters_def unat_of_nat_eq)
apply (clarsimp simp: word_less_nat_alt word_le_nat_alt unat_of_nat_eq not_le[symmetric])
done
lemma performPageGetAddress_ccorres:
notes Collect_const[simp del] dc_simp[simp del]
shows
"ccorres ((intr_and_se_rel \<circ> Inr) \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_')
(invs' and (\<lambda>s. ksCurThread s = thread) and ct_in_state' ((=) Restart))
(UNIV \<inter> \<lbrace>\<acute>vbase_ptr = Ptr ptr\<rbrace> \<inter> \<lbrace>\<acute>call = from_bool isCall\<rbrace>) []
(do reply \<leftarrow> performPageInvocation (PageGetAddr ptr);
liftE (replyOnRestart thread reply isCall) od)
(Call performPageGetAddress_'proc)"
apply (cinit' lift: vbase_ptr_' call_' simp: performPageInvocation_def)
apply (clarsimp simp: bind_assoc)
apply csymbr
apply csymbr
apply (rule ccorres_symb_exec_r)
apply (rule_tac xf'=thread_' in ccorres_abstract, ceqv)
apply (rename_tac cthread)
apply (rule_tac P="cthread = tcb_ptr_to_ctcb_ptr thread" in ccorres_gen_asm2)
apply (rule ccorres_Cond_rhs_Seq[rotated]; clarsimp)
apply (simp add: replyOnRestart_def liftE_def bind_assoc)
apply (rule getThreadState_ccorres_foo, rename_tac tstate)
apply (rule_tac P="tstate = Restart" in ccorres_gen_asm)
apply clarsimp
apply (rule_tac P="\<lambda>s. ksCurThread s = thread" in ccorres_cross_over_guard)
apply (ctac (no_vcg) add: setThreadState_ccorres)
apply (rule ccorres_from_vcg_throws[where P=\<top> and P'=UNIV])
apply clarsimp
apply (rule conseqPre, vcg)
apply (clarsimp simp: return_def dc_simp)
apply (rule hoare_post_taut[of \<top>])
apply (rule ccorres_rhs_assoc)+
apply (clarsimp simp: replyOnRestart_def liftE_def bind_assoc)
apply (rule_tac P="\<lambda>s. ksCurThread s = thread" in ccorres_cross_over_guard)
apply (rule getThreadState_ccorres_foo, rename_tac tstate)
apply (rule_tac P="tstate = Restart" in ccorres_gen_asm)
apply (clarsimp simp: bind_assoc)
apply (simp add: replyFromKernel_def bind_assoc)
apply (ctac add: lookupIPCBuffer_ccorres)
apply (ctac add: setRegister_ccorres)
apply (simp add: setMRs_single)
apply (ctac add: setMR_as_setRegister_ccorres[where offset=0])
apply clarsimp
apply csymbr
apply (simp only: setMessageInfo_def bind_assoc)
apply ctac
apply simp
apply (ctac add: setRegister_ccorres)
apply (ctac add: setThreadState_ccorres)
apply (rule ccorres_inst[where P=\<top> and P'=UNIV])
apply (rule ccorres_from_vcg_throws[where P=\<top> and P'=UNIV])
apply (rule allI, rule conseqPre, vcg)
apply (clarsimp simp: return_def dc_def)
apply (rule hoare_post_taut[of \<top>])
apply (vcg exspec=setThreadState_modifies)
apply wpsimp
apply (vcg exspec=setRegister_modifies)
apply wpsimp
apply clarsimp
apply (vcg)
apply wpsimp
apply (clarsimp simp: msgInfoRegister_def ARM.msgInfoRegister_def
Kernel_C.msgInfoRegister_def Kernel_C.R1_def)
apply (vcg exspec=setMR_modifies)
apply wpsimp
apply (clarsimp simp: dc_def)
apply (vcg exspec=setRegister_modifies)
apply wpsimp
apply (clarsimp simp: dc_def ThreadState_Running_def)
apply (vcg exspec=lookupIPCBuffer_modifies)
apply clarsimp
apply vcg
apply clarsimp
apply (rule conseqPre, vcg)
apply clarsimp
apply (clarsimp simp: invs_no_0_obj' tcb_at_invs' invs_queues invs_valid_objs' invs_sch_act_wf'
rf_sr_ksCurThread msgRegisters_unfold
seL4_MessageInfo_lift_def message_info_to_H_def mask_def)
apply (cases isCall)
apply (auto simp: ARM.badgeRegister_def ARM_H.badgeRegister_def Kernel_C.badgeRegister_def
Kernel_C.R0_def fromPAddr_def ThreadState_Running_def
pred_tcb_at'_def obj_at'_def projectKOs ct_in_state'_def)
done
lemma vmsz_aligned_addrFromPPtr':
"vmsz_aligned' (addrFromPPtr p) sz
= vmsz_aligned' p sz"
@ -2208,13 +2330,14 @@ lemma decodeARMFrameInvocation_ccorres:
\<inter> {s. cte_' s = cte_Ptr slot}
\<inter> {s. current_extra_caps_' (globals s) = extraCaps'}
\<inter> {s. ccap_relation (ArchObjectCap cp) (cap_' s)}
\<inter> {s. buffer_' s = option_to_ptr buffer}) []
\<inter> {s. buffer_' s = option_to_ptr buffer}
\<inter> {s. call_' s = from_bool isCall}) []
(decodeARMMMUInvocation label args cptr slot cp extraCaps
>>= invocationCatch thread isBlocking isCall InvokeArchObject)
(Call decodeARMFrameInvocation_'proc)"
supply if_cong[cong] option.case_cong[cong]
apply (clarsimp simp only: isCap_simps)
apply (cinit' lift: invLabel_' length___unsigned_long_' cte_' current_extra_caps_' cap_' buffer_'
apply (cinit' lift: invLabel_' length___unsigned_long_' cte_' current_extra_caps_' cap_' buffer_' call_'
simp: decodeARMMMUInvocation_def decodeARMPageFlush_def)
apply (simp add: Let_def isCap_simps invocation_eq_use_types split_def
del: Collect_const
@ -2233,14 +2356,21 @@ lemma decodeARMFrameInvocation_ccorres:
apply (rule ccorres_rhs_assoc)+
apply (ctac add: setThreadState_ccorres)
apply csymbr
apply (rule ccorres_nondet_refinement)
apply (rule is_nondet_refinement_bindE)
apply (rule is_nondet_refinement_refl)
apply (simp split: if_split, rule conjI[rotated])
apply (rule impI, rule is_nondet_refinement_refl)
apply (rule impI, rule is_nondet_refinement_alternative1)
apply (clarsimp simp: liftE_bindE)
apply (rule ccorres_add_returnOk)
apply (ctac(no_vcg) add: performPageGetAddress_ccorres)
apply (rule ccorres_alternative2)
apply (rule ccorres_return_CE, simp+)[1]
apply (rule ccorres_inst[where P=\<top> and P'=UNIV], simp)
apply wp+
apply (rule ccorres_return_C_errorE, simp+)[1]
apply (wpsimp wp: sts_invs_minor' ct_in_state'_set)+
apply (vcg exspec=setThreadState_modifies)
\<comment> \<open>PageUnify_Instruction | PageCleanInvalidate_Data | Page Invalidate_Data | PageClean_Data\<close>
apply (vcg exspec=setThreadState_modifies)
apply (rule ccorres_rhs_assoc)+
apply csymbr+
apply (simp add: ivc_label_flush_case decodeARMPageFlush_def list_case_If2 if3_fold2
@ -2308,10 +2438,12 @@ lemma decodeARMFrameInvocation_ccorres:
apply (simp add: performARMMMUInvocations bindE_assoc)
apply (ctac add: setThreadState_ccorres)
apply (ctac(no_vcg) add: performPageFlush_ccorres)
apply (rule ccorres_gen_asm)
apply (erule ssubst[OF if_P, where P="\<lambda>x. ccorres _ _ _ _ _ x _"])
apply (rule ccorres_alternative2)
apply (rule ccorres_return_CE, simp+)[1]
apply (rule ccorres_inst[where P=\<top> and P'=UNIV], simp)
apply wp
apply (wpsimp simp: performPageInvocation_def)
apply simp
apply (strengthen unat_sub_le_strg[where v="2 ^ pageBitsForSize (capVPSize cp)"])
apply (simp add: linorder_not_less linorder_not_le order_less_imp_le)
@ -2342,17 +2474,19 @@ lemma decodeARMFrameInvocation_ccorres:
apply (rule ccorres_rhs_assoc)+
apply (ctac add: setThreadState_ccorres)
apply (ctac(no_vcg) add: performPageInvocationUnmap_ccorres)
apply (rule ccorres_gen_asm)
apply (erule ssubst[OF if_P, where P="\<lambda>x. ccorres _ _ _ _ _ x _"])
apply (rule ccorres_alternative2)
apply (rule ccorres_return_CE; simp)
apply (rule ccorres_inst[where P=\<top> and P'=UNIV], simp)
apply wp
apply (wpsimp simp: performPageInvocation_def)
apply (wp sts_invs_minor')
apply simp
apply (vcg exspec=setThreadState_modifies)
\<comment> \<open>PageMap\<close>
supply Collect_const[simp del]
apply (rename_tac word rghts pg_sz mapdata buffera cap excaps cte length___unsigned_long invLabel)
apply (rename_tac word rghts pg_sz mapdata call' buffer' cap excaps cte length___unsigned_long invLabel)
apply simp
apply (rule ccorres_rhs_assoc)+
apply csymbr+
@ -2566,10 +2700,13 @@ lemma decodeARMFrameInvocation_ccorres:
apply ccorres_rewrite
apply (ctac add: setThreadState_ccorres)
apply (ctac(no_vcg) add: performPageInvocationMapPTE_ccorres)
apply (rule ccorres_gen_asm)
apply (erule ssubst[OF if_P, where P="\<lambda>x. ccorres _ _ _ _ _ x _"])
apply (rule ccorres_alternative2)
apply (rule ccorres_return_CE; simp)
apply (rule ccorres_inst[where P=\<top> and P'=UNIV], simp)
apply (wp sts_invs_minor' valid_pte_slots_lift2)+
apply (wpsimp simp: performPageInvocation_def)
apply (wp sts_invs_minor' valid_pte_slots_lift2)
apply (simp, vcg exspec=setThreadState_modifies)
apply (simp, rule ccorres_split_throws)
apply ccorres_rewrite
@ -2588,10 +2725,13 @@ lemma decodeARMFrameInvocation_ccorres:
apply ccorres_rewrite
apply (ctac add: setThreadState_ccorres)
apply (ctac(no_vcg) add: performPageInvocationMapPDE_ccorres)
apply (rule ccorres_gen_asm)
apply (erule ssubst[OF if_P, where P="\<lambda>x. ccorres _ _ _ _ _ x _"])
apply (rule ccorres_alternative2)
apply (rule ccorres_return_CE; simp)
apply (rule ccorres_inst[where P=\<top> and P'=UNIV], simp)
apply wp
apply (wpsimp simp: performPageInvocation_def)
apply (wp sts_invs_minor' valid_pde_slots_lift2)
apply (simp, vcg exspec=setThreadState_modifies)
apply (simp, ccorres_rewrite, rule ccorres_return_C_errorE; simp)
@ -2619,8 +2759,8 @@ lemma decodeARMFrameInvocation_ccorres:
apply (simp, wp (once) hoare_drop_imps, wpsimp)
apply (clarsimp, vcg)
apply (wpsimp, (simp, vcg exspec=getSyscallArg_modifies))+
apply (rename_tac word rghts pg_sz mapdata buffera cap excaps cte length___unsigned_long invLabel
s s')
apply (rename_tac word rghts pg_sz mapdata call' buffer' cap
excaps cte length___unsigned_long invLabel s s')
apply (rule conjI)
apply (clarsimp, frule cte_wp_at_eq_gsMaxObjectSize, clarsimp)
apply (clarsimp simp: cte_wp_at_ctes_of is_aligned_mask[symmetric] vmsz_aligned'_def
@ -3157,7 +3297,8 @@ lemma Arch_decodeInvocation_ccorres:
\<inter> {s. slot_' s = cte_Ptr slot}
\<inter> {s. current_extra_caps_' (globals s) = extraCaps'}
\<inter> {s. ccap_relation (ArchObjectCap cp) (cap_' s)}
\<inter> {s. buffer_' s = option_to_ptr buffer}) []
\<inter> {s. buffer_' s = option_to_ptr buffer}
\<inter> {s. call_' s = from_bool isCall}) []
(Arch.decodeInvocation label args cptr slot cp extraCaps
>>= invocationCatch thread isBlocking isCall InvokeArchObject)
(Call Arch_decodeInvocation_'proc)"
@ -3169,7 +3310,7 @@ lemma Arch_decodeInvocation_ccorres:
defer
apply (simp+)[4]
apply (cinit' lift: invLabel_' length___unsigned_long_' cte_'
current_extra_caps_' cap_' buffer_')
current_extra_caps_' cap_' buffer_' call_')
apply csymbr
apply (simp add: cap_get_tag_isCap_ArchObject
ARM_H.decodeInvocation_def

7
proof/crefine/ARM/Tcb_C.thy
View File

@ -2192,10 +2192,9 @@ lemma decodeReadRegisters_ccorres:
apply (rule ccorres_nondet_refinement)
apply (rule is_nondet_refinement_bindE)
apply (rule is_nondet_refinement_refl)
apply (simp split: if_split)
apply (rule conjI[rotated], rule impI, rule is_nondet_refinement_refl)
apply (rule impI)
apply (rule is_nondet_refinement_alternative1)
apply (simp split: if_split, rule conjI[rotated])
apply (rule impI, rule is_nondet_refinement_refl)
apply (rule impI, rule is_nondet_refinement_alternative1)
apply (simp add: performInvocation_def)
apply (rule ccorres_add_returnOk)
apply (ctac(no_vcg) add: invokeTCB_ReadRegisters_ccorres)

77
proof/crefine/ARM/VSpace_C.thy
View File

@ -1635,32 +1635,27 @@ lemma performPageFlush_ccorres:
apply (simp only: liftE_liftM ccorres_liftM_simp)
apply (cinit lift: pd_' asid_' start_' end_' pstart_' invLabel___int_')
apply (unfold when_def)
apply (rule ccorres_cond_seq)
apply (rule ccorres_cond2[where R=\<top>])
apply (simp split: if_split)
apply (rule ccorres_rhs_assoc)+
apply (ctac (no_vcg) add: setVMRootForFlush_ccorres)
apply (ctac (no_vcg) add: doFlush_ccorres)
apply (rule ccorres_add_return2)
apply (rule ccorres_split_nothrow_novcg_dc)
apply (rule ccorres_split_nothrow_novcg_dc)
apply (rule ccorres_cond2[where R=\<top>])
apply (simp split: if_split)
apply (rule ccorres_rhs_assoc)+
apply (ctac (no_vcg) add: setVMRootForFlush_ccorres)
apply (ctac (no_vcg) add: doFlush_ccorres)
apply (rule ccorres_cond2[where R=\<top>])
apply (simp add: from_bool_def split: if_split bool.splits)
apply (rule ccorres_pre_getCurThread)
apply (ctac add: setVMRoot_ccorres)
apply (rule ccorres_return_Skip)
apply (rule_tac P=\<top> and P'=UNIV in ccorres_from_vcg_throws)
apply (rule allI, rule conseqPre, vcg)
apply (clarsimp simp: return_def)
apply wp
apply (simp add: guard_is_UNIV_def)
apply (simp add: cur_tcb'_def[symmetric])
apply (rule_tac Q="\<lambda>_ s. invs' s \<and> cur_tcb' s" in hoare_post_imp)
apply (simp add: invs'_invs_no_cicd)
apply wp+
apply (simp)
apply (rule_tac P=\<top> and P'=UNIV in ccorres_from_vcg_throws)
apply (rule allI, rule conseqPre, vcg)
apply (clarsimp simp: return_def)
apply (simp add: cur_tcb'_def[symmetric])
apply (rule_tac Q="\<lambda>_ s. invs' s \<and> cur_tcb' s" in hoare_post_imp)
apply (simp add: invs'_invs_no_cicd)
apply wp+
apply (rule ccorres_return_Skip)
apply (rule ccorres_from_vcg_throws[where P=\<top> and P'=UNIV])
apply (rule allI, rule conseqPre, vcg)
apply (clarsimp simp: return_def dc_def)
apply wpsimp
apply (simp add: guard_is_UNIV_def)
apply (clarsimp simp: order_less_imp_le)
done
@ -1758,43 +1753,6 @@ lemma setMessageInfo_ccorres:
Kernel_C.msgInfoRegister_def Kernel_C.R1_def)
done
lemma performPageGetAddress_ccorres:
"ccorres (K (K \<bottom>) \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_')
\<top>
(UNIV \<inter> {s. vbase_ptr_' s = Ptr ptr}) []
(liftE (performPageInvocation (PageGetAddr ptr)))
(Call performPageGetAddress_'proc)"
apply (simp only: liftE_liftM ccorres_liftM_simp)
apply (cinit lift: vbase_ptr_')
apply csymbr
apply (rule ccorres_pre_getCurThread)
apply (clarsimp simp add: setMRs_def zipWithM_x_mapM_x mapM_x_Nil zip_singleton msgRegisters_unfold mapM_x_singleton)
apply (ctac add: setRegister_ccorres)
apply csymbr
apply (rule ccorres_add_return2)
apply (rule ccorres_rhs_assoc2)
apply (rule ccorres_split_nothrow_novcg[where r'=dc and xf'=xfdc])
apply (unfold setMessageInfo_def)
apply ctac
apply (simp only: fun_app_def)
apply (ctac add: setRegister_ccorres)
apply wp
apply vcg
apply ceqv
apply (rule_tac P=\<top> and P'=UNIV in ccorres_from_vcg_throws)
apply (rule allI, rule conseqPre, vcg)
apply (clarsimp simp: return_def)
apply wp
apply (simp add: guard_is_UNIV_def)
apply wp
apply vcg
by (auto simp: ARM_H.fromPAddr_def message_info_to_H_def mask_def ARM_H.msgInfoRegister_def
ARM.msgInfoRegister_def Kernel_C.msgInfoRegister_def Kernel_C.R1_def
word_sle_def word_sless_def Kernel_C.R2_def
kernel_all_global_addresses.msgRegisters_def fupdate_def Arrays.update_def
fcp_beta)
lemma performPageDirectoryInvocationFlush_ccorres:
"ccorres (K (K \<bottom>) \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_')
(invs' and K (asid \<le> mask asid_bits)
@ -2642,7 +2600,6 @@ lemma performPageInvocationUnmap_ccorres:
apply (rule_tac P=" ret__unsigned_long = 0" in ccorres_gen_asm)
apply simp
apply (rule ccorres_symb_exec_l)
apply (subst bind_return [symmetric])
apply (rule ccorres_split_nothrow_novcg)
apply (rule ccorres_Guard)
apply (rule updateCap_frame_mapped_addr_ccorres)
@ -2664,7 +2621,7 @@ lemma performPageInvocationUnmap_ccorres:
apply csymbr
apply wpc
apply (ctac (no_vcg) add: unmapPage_ccorres)
apply (rule ccorres_add_return2)
apply (rule ccorres_lhs_assoc)
apply (rule ccorres_split_nothrow_novcg)
apply (rule ccorres_move_Guard [where P="cte_at' ctSlot" and P'=\<top>])
apply (clarsimp simp: cte_wp_at_ctes_of)

32
proof/refine/ARM/Arch_R.thy
View File

@ -1156,28 +1156,34 @@ lemma arch_performInvocation_corres:
apply (clarsimp simp: arch_perform_invocation_def
ARM_H.performInvocation_def
performARMMMUInvocation_def)
apply (rule corres_split' [where r'=dc])
prefer 2
apply (rule corres_trivial)
apply simp
apply (cases ai)
apply (clarsimp simp: archinv_relation_def)
apply (cases ai)
apply (clarsimp simp: archinv_relation_def)
apply (rule corres_split'[OF _ corres_return_eq_same[OF refl]])
apply (erule corres_guard_imp [OF performPageTableInvocation_corres])
apply (fastforce simp: valid_arch_inv_def)
apply (fastforce simp: valid_arch_inv'_def)
apply (clarsimp simp: archinv_relation_def)
apply wp
apply wp
apply (clarsimp simp: archinv_relation_def)
apply (rule corres_split'[OF _ corres_return_eq_same[OF refl]])
apply (erule corres_guard_imp [OF performPageDirectoryInvocation_corres])
apply (fastforce simp: valid_arch_inv_def)
apply (fastforce simp: valid_arch_inv'_def)
apply (clarsimp simp: archinv_relation_def)
apply (erule corres_guard_imp [OF performPageInvocation_corres])
apply (fastforce simp: valid_arch_inv_def)
apply (fastforce simp: valid_arch_inv'_def)
apply (clarsimp simp: archinv_relation_def)
apply wp
apply wp
apply (clarsimp simp: archinv_relation_def)
apply (erule corres_guard_imp [OF performPageInvocation_corres])
apply (fastforce simp: valid_arch_inv_def)
apply (fastforce simp: valid_arch_inv'_def)
apply (clarsimp simp: archinv_relation_def)
apply (rule corres_split'[OF _ corres_return_eq_same[OF refl]])
apply (rule corres_guard_imp [OF performASIDControlInvocation_corres], rule refl)
apply (fastforce simp: valid_arch_inv_def)
apply (fastforce simp: valid_arch_inv'_def)
apply (clarsimp simp: archinv_relation_def)
apply wp
apply wp
apply (clarsimp simp: archinv_relation_def)
apply (rule corres_split'[OF _ corres_return_eq_same[OF refl]])
apply (rule corres_guard_imp [OF performASIDPoolInvocation_corres], rule refl)
apply (fastforce simp: valid_arch_inv_def)
apply (fastforce simp: valid_arch_inv'_def)

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

@ -2110,7 +2110,7 @@ lemma same_refs_vs_cap_ref_eq:
lemma performPageInvocation_corres:
assumes "page_invocation_map pgi pgi'"
shows "corres dc (invs and valid_etcbs and valid_page_inv pgi)
shows "corres (=) (invs and valid_etcbs and valid_page_inv pgi)
(invs' and valid_page_inv' pgi' and (\<lambda>s. vs_valid_duplicates' (ksPSpace s)))
(perform_page_invocation pgi) (performPageInvocation pgi')"
proof -
@ -2142,8 +2142,11 @@ proof -
apply (rule corres_split_deprecated[OF _ storePTE_corres'])
apply (rule corres_split_deprecated[where r' = dc, OF _ corres_store_pte_with_invalid_tail])
apply (rule corres_split_deprecated[where r'=dc, OF _ corres_machine_op[OF corres_Id]])
apply (clarsimp simp add: when_def)
apply (rule invalidate_tlb_by_asid_corres_ex)
apply (rule corres_split[where r'=dc, OF _ corres_return_eq_same[OF refl]])
apply (clarsimp simp add: when_def)
apply (rule invalidate_tlb_by_asid_corres_ex)
apply wp
apply wp
apply (simp add: last_byte_pte_def objBits_simps archObjSize_def pteBits_def)
apply simp
apply (rule no_fail_cleanCacheRange_PoU)
@ -2190,8 +2193,11 @@ proof -
apply (rule corres_split_deprecated[OF _ storePDE_corres'])
apply (rule corres_split_deprecated[where r'=dc, OF _ corres_store_pde_with_invalid_tail])
apply (rule corres_split_deprecated[where r'=dc,OF _ corres_machine_op[OF corres_Id]])
apply (clarsimp simp: when_def)
apply (rule invalidate_tlb_by_asid_corres_ex)
apply (rule corres_split[where r'=dc, OF _ corres_return_eq_same[OF refl]])
apply (clarsimp simp: when_def)
apply (rule invalidate_tlb_by_asid_corres_ex)
apply wp
apply wp
apply (simp add: last_byte_pde_def objBits_simps archObjSize_def pdeBits_def)
apply simp
apply (rule no_fail_cleanCacheRange_PoU)
@ -2266,10 +2272,11 @@ proof -
apply (rule corres_rel_imp)
apply (rule get_cap_corres_all_rights_P[where P=is_arch_cap], rule refl)
apply (clarsimp simp: is_cap_simps)
apply (rule_tac F="is_page_cap cap" in corres_gen_asm)
apply (rule updateCap_same_master)
apply (clarsimp simp: is_page_cap_def update_map_data_def)
apply (wp get_cap_wp getSlotCap_wp)+
apply (rule corres_split[where r'=dc, OF _ corres_return_eq_same[OF refl]])
apply (rule_tac F="is_page_cap cap" in corres_gen_asm)
apply (rule updateCap_same_master)
apply (clarsimp simp: is_page_cap_def update_map_data_def)
apply (wp get_cap_wp getSlotCap_wp)+
apply (clarsimp simp: cte_wp_at_caps_of_state)
apply (clarsimp simp: cap_rights_update_def acap_rights_update_def update_map_data_def is_cap_simps)
apply auto[1]
@ -2285,10 +2292,11 @@ proof -
apply (rule corres_rel_imp)
apply (rule get_cap_corres_all_rights_P[where P=is_arch_cap], rule refl)
apply (clarsimp simp: is_cap_simps)
apply (rule_tac F="is_page_cap cap" in corres_gen_asm)
apply (rule updateCap_same_master)
apply (clarsimp simp: is_page_cap_def update_map_data_def)
apply (wp get_cap_wp getSlotCap_wp)+
apply (rule corres_split[where r'=dc, OF _ corres_return_eq_same[OF refl]])
apply (rule_tac F="is_page_cap cap" in corres_gen_asm)
apply (rule updateCap_same_master)
apply (clarsimp simp: is_page_cap_def update_map_data_def)
apply (wp get_cap_wp getSlotCap_wp)+
apply (simp add: cte_wp_at_caps_of_state)
apply (strengthen pull_out_P)+
apply wp
@ -2305,32 +2313,24 @@ proof -
apply (clarsimp simp: performPageInvocation_def perform_page_invocation_def
page_invocation_map_def)
apply (rule corres_guard_imp)
apply (rule corres_when, simp)
apply (rule corres_split_deprecated [OF _ setVMRootForFlush_corres])
apply (rule corres_split_deprecated [OF _ corres_machine_op])
prefer 2
apply (rule doFlush_corres)
apply (rule corres_when, simp)
apply (rule corres_split_deprecated [OF _ getCurThread_corres])
apply simp
apply (rule setVMRoot_corres)
apply wp+
apply (simp add: cur_tcb_def [symmetric] cur_tcb'_def [symmetric])
apply (wp hoare_drop_imps)
apply (simp add: cur_tcb_def [symmetric] cur_tcb'_def [symmetric])
apply (wp hoare_drop_imps)+
apply (rule corres_split[where r'=dc, OF _ corres_return_eq_same[OF refl]])
apply (rule corres_when, simp)
apply (rule corres_split_deprecated [OF _ setVMRootForFlush_corres])
apply (rule corres_split_deprecated [OF _ corres_machine_op])
prefer 2
apply (rule doFlush_corres)
apply (rule corres_when, simp)
apply (rule corres_split_deprecated [OF _ getCurThread_corres])
apply simp
apply (rule setVMRoot_corres)
apply wp+
apply (simp add: cur_tcb_def [symmetric] cur_tcb'_def [symmetric])
apply (wp hoare_drop_imps)
apply (simp add: cur_tcb_def [symmetric] cur_tcb'_def [symmetric])
apply (wp hoare_drop_imps)+
apply (auto simp: valid_page_inv_def invs_vspace_objs[simplified])[2]
\<comment> \<open>PageGetAddr\<close>
apply (clarsimp simp: perform_page_invocation_def performPageInvocation_def page_invocation_map_def fromPAddr_def)
apply (rule corres_guard_imp)
apply (rule corres_split_deprecated[OF _ getCurThread_corres])
apply simp
apply (rule corres_split_deprecated[OF setMessageInfo_corres setMRs_corres])
apply (simp add: message_info_map_def)
apply clarsimp
apply (wp)+
apply (clarsimp simp: tcb_at_invs)
apply (clarsimp simp: tcb_at_invs')
done
qed