From c57a69775bc65068cbc9f194d3f12c48f2bd10a5 Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Fri, 23 Jun 2023 10:23:36 +1000 Subject: [PATCH] arm refine: deploy corres_cases in some examples Demonstrates use of corres_cases and corres_cases_both. Main intended benefit is less thinking about safety of schematics, fewer mentions of goal parameter names, and fewer manual guard instantiations. Signed-off-by: Gerwin Klein --- proof/refine/ARM/VSpace_R.thy | 150 +++++++++++++--------------------- 1 file changed, 56 insertions(+), 94 deletions(-) diff --git a/proof/refine/ARM/VSpace_R.thy b/proof/refine/ARM/VSpace_R.thy index aca8f5f015..588807b5ef 100644 --- a/proof/refine/ARM/VSpace_R.thy +++ b/proof/refine/ARM/VSpace_R.thy @@ -458,13 +458,11 @@ lemma getHWASID_corres: apply (simp add: get_hw_asid_def getHWASID_def) apply (rule corres_guard_imp) apply (rule corres_split_eqr[OF loadHWASID_corres[where pd=pd]]) - apply (case_tac maybe_hw_asid, simp_all)[1] + apply (corres_cases; simp) apply (rule corres_split_eqr[OF findFreeHWASID_corres]) apply (rule corres_split[OF storeHWASID_corres[where pd=pd]]) - apply (rule corres_trivial, simp ) - apply (wpsimp wp: load_hw_asid_wp)+ - apply (simp add: pd_at_asid_uniq) - apply simp + apply (rule corres_trivial, simp) + apply (wpsimp wp: load_hw_asid_wp hoare_drop_imp simp: pd_at_asid_uniq)+ done lemma setCurrentPD_to_abs: @@ -498,9 +496,8 @@ lemma handleVMFault_corres: "corres (fr \ dc) (tcb_at thread) (tcb_at' thread) (handle_vm_fault thread fault) (handleVMFault thread fault)" apply (simp add: ARM_H.handleVMFault_def) - apply (cases fault) - apply simp - apply (rule corres_guard_imp) + apply corres_cases + apply simp apply (rule corres_splitEE) apply simp apply (rule corres_machine_op [where r="(=)"]) @@ -512,9 +509,7 @@ lemma handleVMFault_corres: apply (rule corres_Id, rule refl, simp) apply (rule no_fail_getDFSR) apply (rule corres_trivial, simp add: arch_fault_map_def) - apply wp+ - apply simp+ - apply (rule corres_guard_imp) + apply wpsimp+ apply (rule corres_splitEE) apply simp apply (rule asUser_corres') @@ -527,8 +522,7 @@ lemma handleVMFault_corres: apply (rule corres_Id, rule refl, simp) apply (rule no_fail_getIFSR) apply (rule corres_trivial, simp add: arch_fault_map_def) - apply wp+ - apply simp+ + apply wpsimp+ done lemma flushSpace_corres: @@ -545,18 +539,15 @@ lemma flushSpace_corres: apply (rule corres_guard_imp) apply (rule corres_split) apply (rule loadHWASID_corres[where pd=pd]) - apply (rule corres_split[where R="\_. \" and R'="\_. \"]) + apply (rule corres_split) apply (rule corres_machine_op [where r=dc]) apply (rule corres_Id, rule refl, simp) apply (rule no_fail_cleanCaches_PoU) - apply (case_tac maybe_hw_asid) - apply simp - apply clarsimp + apply (corres_cases; clarsimp) apply (rule corres_machine_op) apply (rule corres_Id, rule refl, simp) apply (rule no_fail_invalidateLocalTLB_ASID) - apply wp+ - apply clarsimp + apply wpsimp+ apply (simp add: pd_at_asid_uniq) apply simp done @@ -573,16 +564,13 @@ lemma invalidateTLBByASID_corres: (invalidate_tlb_by_asid asid) (invalidateTLBByASID asid)" apply (simp add: invalidate_tlb_by_asid_def invalidateTLBByASID_def) apply (rule corres_guard_imp) - apply (rule corres_split[where R="\_. \" and R'="\_. \"]) + apply (rule corres_split) apply (rule loadHWASID_corres[where pd=pd]) - apply (case_tac maybe_hw_asid) - apply simp - apply clarsimp + apply (corres_cases; clarsimp) apply (rule corres_machine_op) apply (rule corres_Id, rule refl, simp) apply (rule no_fail_invalidateLocalTLB_ASID) - apply wp+ - apply clarsimp + apply wpsimp+ apply (simp add: pd_at_asid_uniq) apply simp done @@ -842,8 +830,7 @@ lemma deleteASID_corres: apply (simp add: delete_asid_def deleteASID_def) apply (rule corres_guard_imp) apply (rule corres_split[OF corres_gets_asid]) - apply (case_tac "asid_table (asid_high_bits_of asid)", simp) - apply clarsimp + apply (corres_cases; clarsimp) apply (rule_tac P="\s. asid_high_bits_of asid \ dom (asidTable o ucast) \ asid_pool_at (the ((asidTable o ucast) (asid_high_bits_of asid))) s" and P'="pspace_aligned' and pspace_distinct'" and @@ -1078,10 +1065,10 @@ proof - and valid_arch_state and pspace_aligned and pspace_distinct) (pspace_aligned' and pspace_distinct' and no_0_obj') - (do arm_context_switch pd asid; + (do _ \ arm_context_switch pd asid; return True od) - (do armv_contextSwitch pd asid; + (do _ \ armv_contextSwitch pd asid; return True od)" apply (rule corres_guard_imp) @@ -1090,34 +1077,20 @@ proof - apply (wp | simp)+ done show ?thesis - apply (simp add: set_vm_root_for_flush_def setVMRootForFlush_def getThreadVSpaceRoot_def locateSlot_conv) - apply (rule corres_guard_imp) - apply (rule corres_split[OF getCurThread_corres]) - apply (rule corres_split[where R="\_. vspace_at_asid asid pd and K (asid \ 0 \ asid \ mask asid_bits) - and valid_asid_map and valid_vs_lookup - and valid_vspace_objs and valid_global_objs - and unique_table_refs o caps_of_state - and valid_arch_state - and pspace_aligned and pspace_distinct" - and R'="\_. pspace_aligned' and pspace_distinct' and no_0_obj'"]) - apply (rule getSlotCap_corres) - apply (simp add: cte_map_def tcb_cnode_index_def tcbVTableSlot_def to_bl_1) - apply (case_tac "isArchObjectCap rv' \ - isPageDirectoryCap (capCap rv') \ - capPDMappedASID (capCap rv') \ None \ - capPDBasePtr (capCap rv') = pd") - apply (case_tac rv, simp_all add: isCap_simps)[1] - apply (rename_tac arch_cap) - apply (case_tac arch_cap, auto)[1] - apply (case_tac rv, simp_all add: isCap_simps[simplified] X[simplified])[1] - apply (rename_tac arch_cap) - apply (case_tac arch_cap, auto simp: X[simplified] split: option.splits)[1] - apply wp+ - apply (clarsimp simp: cur_tcb_def) - apply (erule tcb_at_cte_at) - apply (simp add: tcb_cap_cases_def) - apply clarsimp - done + apply (simp add: set_vm_root_for_flush_def setVMRootForFlush_def getThreadVSpaceRoot_def locateSlot_conv) + apply (rule corres_guard_imp) + apply (rule corres_split[OF getCurThread_corres]) + apply (rule corres_split) + apply (rule getSlotCap_corres) + apply (simp add: cte_map_def tcb_cnode_index_def tcbVTableSlot_def to_bl_1) + apply (corres_cases; (simp add: isCap_simps, rule X)?)+ + apply (clarsimp simp: isCap_simps, rule X) + apply (wpsimp wp: hoare_drop_imp hoare_vcg_all_lift)+ + apply (clarsimp simp: cur_tcb_def) + apply (erule tcb_at_cte_at) + apply (simp add: tcb_cap_cases_def) + apply clarsimp + done qed crunch typ_at' [wp]: armv_contextSwitch "\s. P (typ_at' T p s)" @@ -1370,13 +1343,11 @@ lemma pageTableMapped_corres: apply simp apply (simp add: liftE_bindE) apply (rule corres_split[OF getObject_PDE_corres']) - apply (rule corres_trivial) - apply (case_tac rv, - simp_all add: returnOk_def pde_relation_aligned_def - split:if_splits ARM_H.pde.splits)[1] - apply (wp | simp add: lookup_pd_slot_def Let_def)+ - apply (simp add: word_neq_0_conv) - apply simp + apply (corres_cases_both simp: pde_relation_aligned_def; + fastforce intro!: corres_returnOkTT + simp: pde_relation_aligned_def + split: if_split_asm) + apply (wpsimp simp: lookup_pd_slot_def word_neq_0_conv)+ done crunch inv[wp]: pageTableMapped "P" @@ -1655,17 +1626,11 @@ lemma doFlush_corres: "corres_underlying Id nf nf' dc \ \ (do_flush typ start end pstart) (doFlush (flush_type_map typ) start end pstart)" apply (simp add: do_flush_def doFlush_def) - apply (cases "typ", simp_all add: flush_type_map_def) - apply (rule corres_Id [where r=dc], rule refl, simp) - apply (wp no_fail_cleanCacheRange_RAM) - apply (rule corres_Id [where r=dc], rule refl, simp) - apply (wp no_fail_invalidateCacheRange_RAM) - apply (rule corres_Id [where r=dc], rule refl, simp) - apply (wp no_fail_cleanInvalidateCacheRange_RAM) - apply (rule corres_Id [where r=dc], rule refl, simp) - apply (rule no_fail_pre, wp add: no_fail_cleanCacheRange_PoU no_fail_invalidateCacheRange_I - no_fail_dsb no_fail_isb del: no_irq) - apply clarsimp + apply corres_pre + apply (corres_cases_both simp: flush_type_map_def; + (rule corres_Id[OF refl], simp, wpsimp wp: no_fail_dsb no_fail_isb)) + apply simp + apply simp done definition @@ -1681,25 +1646,22 @@ lemma performPageDirectoryInvocation_corres: and cur_tcb' and valid_arch_state') (perform_page_directory_invocation pdi) (performPageDirectoryInvocation pdi')" apply (simp add: perform_page_directory_invocation_def performPageDirectoryInvocation_def) - apply (cases pdi) - apply (clarsimp simp: page_directory_invocation_map_def) - apply (rule corres_guard_imp) - apply (rule corres_when, simp) - apply (rule corres_split[OF setVMRootForFlush_corres]) - apply (rule corres_split[OF corres_machine_op]) - apply (rule doFlush_corres) - apply (rule corres_when, simp) - apply (rule corres_split[OF getCurThread_corres]) - apply clarsimp - apply (rule setVMRoot_corres) - apply wp+ - apply (simp add: cur_tcb_def[symmetric]) - apply (wp hoare_drop_imps) - apply (simp add: cur_tcb'_def[symmetric]) - apply (wp hoare_drop_imps)+ - apply clarsimp - apply (auto simp: valid_pdi_def invs_vspace_objs[simplified])[2] - apply (clarsimp simp: page_directory_invocation_map_def) + apply (corres_cases_both simp: page_directory_invocation_map_def) + apply (clarsimp simp: page_directory_invocation_map_def) + apply (rule corres_when, simp) + apply (rule corres_split[OF setVMRootForFlush_corres]) + apply (rule corres_split[OF corres_machine_op]) + apply (rule doFlush_corres) + apply (rule corres_when, simp) + apply (rule corres_split[OF getCurThread_corres]) + apply clarsimp + apply (rule setVMRoot_corres) + apply wp+ + apply (simp flip: cur_tcb_def) + apply (wp hoare_drop_imps) + apply (simp flip: cur_tcb'_def) + apply (wp hoare_drop_imps)+ + apply (auto simp: valid_pdi_def invs_vspace_objs[simplified] page_directory_invocation_map_def) done definition