From 9bf8cf35bb308bc2cdcb727d969bbb19ba5a68fe Mon Sep 17 00:00:00 2001 From: Ryan Barry Date: Wed, 25 May 2022 12:46:12 +1000 Subject: [PATCH] refine+crefine: update refinement proofs Co-authored-by: Gerwin Klein Signed-off-by: Ryan Barry --- proof/crefine/ARM/Arch_C.thy | 177 +++++++++++++++++++++++++++++---- proof/crefine/ARM/Tcb_C.thy | 7 +- proof/crefine/ARM/VSpace_C.thy | 77 ++++---------- proof/refine/ARM/Arch_R.thy | 32 +++--- proof/refine/ARM/VSpace_R.thy | 72 +++++++------- 5 files changed, 234 insertions(+), 131 deletions(-) diff --git a/proof/crefine/ARM/Arch_C.thy b/proof/crefine/ARM/Arch_C.thy index 824e7fc61..b925d72fb 100644 --- a/proof/crefine/ARM/Arch_C.thy +++ b/proof/crefine/ARM/Arch_C.thy @@ -1514,7 +1514,7 @@ lemma performPageInvocationMapPTE_ccorres: apply (cinit lift: pte_entries_' pte_' cap_' ctSlot_' asid_' ) apply (rule_tac P="\s. valid_pte_slots'2 mapping s" in ccorres_gen_asm) apply (rule ccorres_gen_asm [where P ="snd (theLeft mapping)\[]"]) - 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=\ 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="\s. valid_pde_slots'2 mapping s" in ccorres_gen_asm) apply (rule ccorres_gen_asm [where P ="snd (theRight mapping)\[]"]) - 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=\ 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 + _ \ 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 (\rv rv'. rv' = of_nat offset + 1) ret__unsigned_' + (tcb_at' thread and K (TCB_H.msgRegisters ! offset = reg \ offset < length msgRegisters)) + (UNIV \ \\reg = val\ + \ \\offset = of_nat offset\ + \ \\receiver = tcb_ptr_to_ctcb_ptr thread\) 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=\]) + apply (rule allI, rule conseqPre, vcg) + apply (clarsimp simp: dc_def return_def) + apply (rule hoare_post_taut[of \]) + 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 \ Inr) \ dc) (liftxf errstate id (K ()) ret__unsigned_long_') + (invs' and (\s. ksCurThread s = thread) and ct_in_state' ((=) Restart)) + (UNIV \ \\vbase_ptr = Ptr ptr\ \ \\call = from_bool isCall\) [] + (do reply \ 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="\s. ksCurThread s = thread" in ccorres_cross_over_guard) + apply (ctac (no_vcg) add: setThreadState_ccorres) + apply (rule ccorres_from_vcg_throws[where P=\ and P'=UNIV]) + apply clarsimp + apply (rule conseqPre, vcg) + apply (clarsimp simp: return_def dc_simp) + apply (rule hoare_post_taut[of \]) + apply (rule ccorres_rhs_assoc)+ + apply (clarsimp simp: replyOnRestart_def liftE_def bind_assoc) + apply (rule_tac P="\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=\ and P'=UNIV]) + apply (rule ccorres_from_vcg_throws[where P=\ and P'=UNIV]) + apply (rule allI, rule conseqPre, vcg) + apply (clarsimp simp: return_def dc_def) + apply (rule hoare_post_taut[of \]) + 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: \ {s. cte_' s = cte_Ptr slot} \ {s. current_extra_caps_' (globals s) = extraCaps'} \ {s. ccap_relation (ArchObjectCap cp) (cap_' s)} - \ {s. buffer_' s = option_to_ptr buffer}) [] + \ {s. buffer_' s = option_to_ptr buffer} + \ {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=\ 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) \ \PageUnify_Instruction | PageCleanInvalidate_Data | Page Invalidate_Data | PageClean_Data\ - 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="\x. ccorres _ _ _ _ _ x _"]) apply (rule ccorres_alternative2) apply (rule ccorres_return_CE, simp+)[1] apply (rule ccorres_inst[where P=\ 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="\x. ccorres _ _ _ _ _ x _"]) apply (rule ccorres_alternative2) apply (rule ccorres_return_CE; simp) apply (rule ccorres_inst[where P=\ and P'=UNIV], simp) - apply wp + apply (wpsimp simp: performPageInvocation_def) apply (wp sts_invs_minor') apply simp apply (vcg exspec=setThreadState_modifies) \ \PageMap\ 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="\x. ccorres _ _ _ _ _ x _"]) apply (rule ccorres_alternative2) apply (rule ccorres_return_CE; simp) apply (rule ccorres_inst[where P=\ 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="\x. ccorres _ _ _ _ _ x _"]) apply (rule ccorres_alternative2) apply (rule ccorres_return_CE; simp) apply (rule ccorres_inst[where P=\ 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: \ {s. slot_' s = cte_Ptr slot} \ {s. current_extra_caps_' (globals s) = extraCaps'} \ {s. ccap_relation (ArchObjectCap cp) (cap_' s)} - \ {s. buffer_' s = option_to_ptr buffer}) [] + \ {s. buffer_' s = option_to_ptr buffer} + \ {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 diff --git a/proof/crefine/ARM/Tcb_C.thy b/proof/crefine/ARM/Tcb_C.thy index 0653a4d08..d2383932a 100644 --- a/proof/crefine/ARM/Tcb_C.thy +++ b/proof/crefine/ARM/Tcb_C.thy @@ -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) diff --git a/proof/crefine/ARM/VSpace_C.thy b/proof/crefine/ARM/VSpace_C.thy index 6059a527a..54068f338 100644 --- a/proof/crefine/ARM/VSpace_C.thy +++ b/proof/crefine/ARM/VSpace_C.thy @@ -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=\]) - 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=\]) + 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=\]) 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=\ 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="\_ s. invs' s \ cur_tcb' s" in hoare_post_imp) - apply (simp add: invs'_invs_no_cicd) - apply wp+ - apply (simp) - apply (rule_tac P=\ 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="\_ s. invs' s \ 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=\ 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 \) \ dc) (liftxf errstate id (K ()) ret__unsigned_long_') - \ - (UNIV \ {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=\ 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 \) \ dc) (liftxf errstate id (K ()) ret__unsigned_long_') (invs' and K (asid \ 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'=\]) apply (clarsimp simp: cte_wp_at_ctes_of) diff --git a/proof/refine/ARM/Arch_R.thy b/proof/refine/ARM/Arch_R.thy index b5fef3e60..883e8e09a 100644 --- a/proof/refine/ARM/Arch_R.thy +++ b/proof/refine/ARM/Arch_R.thy @@ -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) diff --git a/proof/refine/ARM/VSpace_R.thy b/proof/refine/ARM/VSpace_R.thy index 9e64ccb06..cfc28aea8 100644 --- a/proof/refine/ARM/VSpace_R.thy +++ b/proof/refine/ARM/VSpace_R.thy @@ -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 (\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] \ \PageGetAddr\ 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