From 916c5d73c183109c70e1a1c32d5a5194098fa34b Mon Sep 17 00:00:00 2001 From: Michael McInerney Date: Wed, 13 Mar 2024 11:51:17 +1030 Subject: [PATCH 1/8] lib+proof: make haskell_assert [wp] and add haskell_assert_inv Signed-off-by: Michael McInerney --- lib/HaskellLemmaBucket.thy | 6 ++++- proof/crefine/AARCH64/Fastpath_C.thy | 2 +- proof/refine/AARCH64/Detype_R.thy | 25 ++++++-------------- proof/refine/AARCH64/Syscall_R.thy | 16 ++++++------- proof/refine/AARCH64/VSpace_R.thy | 3 ++- proof/refine/AARCH64/orphanage/Orphanage.thy | 12 +++++----- proof/refine/ARM/PageTableDuplicates.thy | 3 ++- proof/refine/ARM/Syscall_R.thy | 14 +++++------ proof/refine/ARM/orphanage/Orphanage.thy | 10 ++++---- proof/refine/ARM_HYP/PageTableDuplicates.thy | 3 ++- proof/refine/ARM_HYP/Syscall_R.thy | 17 ++++++------- proof/refine/ARM_HYP/VSpace_R.thy | 1 + proof/refine/RISCV64/Detype_R.thy | 25 ++++++-------------- proof/refine/RISCV64/Ipc_R.thy | 2 -- proof/refine/RISCV64/Syscall_R.thy | 14 +++++------ proof/refine/RISCV64/orphanage/Orphanage.thy | 10 ++++---- proof/refine/X64/Syscall_R.thy | 14 +++++------ 17 files changed, 81 insertions(+), 96 deletions(-) diff --git a/lib/HaskellLemmaBucket.thy b/lib/HaskellLemmaBucket.thy index b1314342d5..092ba8c315 100644 --- a/lib/HaskellLemmaBucket.thy +++ b/lib/HaskellLemmaBucket.thy @@ -127,10 +127,14 @@ lemma empty_fail_stateAssert[intro!, simp]: "empty_fail (stateAssert P l)" unfolding stateAssert_def by simp -lemma haskell_assert_wp: +lemma haskell_assert_wp[wp]: "\\s. Q \ P s\ haskell_assert Q xs \\_. P\" by simp wp +lemma haskell_assert_inv: + "\P\ haskell_assert Q l \\_. P\" + by wpsimp + lemma init_append_last: "xs \ [] \ init xs @ [last xs] = xs" apply (induct xs rule: rev_induct) diff --git a/proof/crefine/AARCH64/Fastpath_C.thy b/proof/crefine/AARCH64/Fastpath_C.thy index e04d077d17..801f974a2e 100644 --- a/proof/crefine/AARCH64/Fastpath_C.thy +++ b/proof/crefine/AARCH64/Fastpath_C.thy @@ -585,7 +585,7 @@ lemma getASIDPoolEntry_wp: getASIDPoolEntry asid \\rv s. P rv s \" unfolding getASIDPoolEntry_def asid_has_entry_def getPoolPtr_def - apply (wpsimp wp: hoare_vcg_imp_lift' hoare_vcg_all_lift getASID_wp simp: comp_def) + apply (wpsimp wp: haskell_assert_inv getASID_wp) apply normalise_obj_at' apply (rename_tac pool) apply (case_tac "pool (asid AND mask asid_low_bits)"; simp) diff --git a/proof/refine/AARCH64/Detype_R.thy b/proof/refine/AARCH64/Detype_R.thy index 052c94a0cd..4a867acf4f 100644 --- a/proof/refine/AARCH64/Detype_R.thy +++ b/proof/refine/AARCH64/Detype_R.thy @@ -3006,25 +3006,14 @@ lemma curDomain_commute: crunch inv[wp]: curDomain P lemma placeNewObject_tcb_at': - notes blah[simp del] = atLeastatMost_subset_iff atLeastLessThan_iff - Int_atLeastAtMost atLeastatMost_empty_iff split_paired_Ex - atLeastAtMost_iff - shows - "\pspace_aligned' and pspace_distinct' - and pspace_no_overlap' ptr (objBits (makeObject::tcb)) - and K(is_aligned ptr (objBits (makeObject::tcb))) - \ placeNewObject ptr (makeObject::tcb) 0 - \\rv s. tcb_at' ptr s \" - apply (simp add:placeNewObject_def placeNewObject'_def split_def alignError_def) + "\pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (objBits (makeObject::tcb)) + and K (is_aligned ptr (objBits (makeObject::tcb)))\ + placeNewObject ptr (makeObject::tcb) 0 + \\_ s. tcb_at' ptr s \" + apply (simp add: placeNewObject_def placeNewObject'_def split_def alignError_def) apply wpsimp - apply (clarsimp simp: obj_at'_def lookupAround2_None1 objBits_simps - lookupAround2_char1 field_simps projectKO_opt_tcb return_def ps_clear_def - simp flip: is_aligned_mask) - apply (drule (1) pspace_no_overlap_disjoint') - apply (clarsimp intro!: set_eqI; - drule_tac m = "ksPSpace s" in domI, - erule in_emptyE, - fastforce elim!: in_emptyE simp:objBits_simps mask_def add_diff_eq) + apply (clarsimp simp: obj_at'_def objBits_simps ps_clear_def) + apply (fastforce intro!: set_eqI dest: pspace_no_overlap_disjoint' simp: add_mask_fold) done lemma monad_commute_if_weak_r: diff --git a/proof/refine/AARCH64/Syscall_R.thy b/proof/refine/AARCH64/Syscall_R.thy index c6601aa9b4..d37f4c493d 100644 --- a/proof/refine/AARCH64/Syscall_R.thy +++ b/proof/refine/AARCH64/Syscall_R.thy @@ -1332,6 +1332,7 @@ lemma hinv_invs'[wp]: done crunch typ_at'[wp]: handleFault "\s. P (typ_at' T p s)" + (wp: crunch_wps) lemmas handleFault_typ_ats[wp] = typ_at_lifts [OF handleFault_typ_at'] @@ -1761,14 +1762,13 @@ lemma hr_ct_active'[wp]: "\invs' and ct_active'\ handleReply \\rv. ct_active'\" apply (simp add: handleReply_def getSlotCap_def getCurThread_def getThreadCallerSlot_def locateSlot_conv) - apply (rule hoare_seq_ext) - apply (rule ct_in_state'_decomp) - apply ((wp hoare_drop_imps | wpc | simp)+)[1] - apply (subst haskell_assert_def) - apply (wp hoare_vcg_all_lift getCTE_wp doReplyTransfer_st_tcb_at_active - | wpc | simp)+ + apply (rule hoare_seq_ext, rename_tac cur_thread) + apply (rule_tac t=cur_thread in ct_in_state'_decomp) + apply (wpsimp wp: getCTE_wp) + apply (fastforce simp: cte_wp_at_ctes_of) + apply (wpsimp wp: getCTE_wp doReplyTransfer_st_tcb_at_active)+ apply (fastforce simp: ct_in_state'_def cte_wp_at_ctes_of valid_cap'_def - dest: ctes_of_valid') + dest: ctes_of_valid') done lemma handleCall_corres: @@ -2086,7 +2086,7 @@ crunches handleVMFault crunches handleHypervisorFault for ksit[wp]: "\s. P (ksIdleThread s)" - (wp: undefined_valid simp: isFpuEnable_def) + (wp: undefined_valid haskell_assert_inv simp: isFpuEnable_def) lemma hh_invs'[wp]: "\invs' and sch_act_not p and (\s. \a b. p \ set (ksReadyQueues s (a, b))) and diff --git a/proof/refine/AARCH64/VSpace_R.thy b/proof/refine/AARCH64/VSpace_R.thy index 8cd50e9df7..32bce50440 100644 --- a/proof/refine/AARCH64/VSpace_R.thy +++ b/proof/refine/AARCH64/VSpace_R.thy @@ -1335,6 +1335,7 @@ lemma vcpuDisable_invs'[wp]: getSCTLR_def get_gic_vcpu_ctrl_hcr_def dsb_def vgicUpdate_def vcpuUpdate_def vcpuSaveReg_def enableFpuEL01_def by (wpsimp wp: dmo'_gets_wp setVCPU_vgic_invs' setVCPU_regs_invs' dmo_maskInterrupt_True + hoare_drop_imps simp: doMachineOp_bind empty_fail_cond) lemma vcpuInvalidateActive_invs'[wp]: @@ -1398,7 +1399,7 @@ crunches loadVMID lemma updateASIDPoolEntry_valid_arch_state'[wp]: "updateASIDPoolEntry f asid \valid_arch_state'\" unfolding updateASIDPoolEntry_def - by (wpsimp wp: getObject_inv simp: loadObject_default_def) + by (wpsimp wp: getObject_inv hoare_drop_imps simp: loadObject_default_def) lemma invalidateVMIDEntry_valid_arch_state'[wp]: "invalidateVMIDEntry vmid \valid_arch_state'\" diff --git a/proof/refine/AARCH64/orphanage/Orphanage.thy b/proof/refine/AARCH64/orphanage/Orphanage.thy index dd647ff45b..2d929cd90a 100644 --- a/proof/refine/AARCH64/orphanage/Orphanage.thy +++ b/proof/refine/AARCH64/orphanage/Orphanage.thy @@ -1275,7 +1275,7 @@ lemma setupCallerCap_no_orphans [wp]: setupCallerCap sender receiver gr \ \rv s. no_orphans s \" unfolding setupCallerCap_def - by (wpsimp wp: setThreadState_not_active_no_orphans + by (wpsimp wp: setThreadState_not_active_no_orphans hoare_drop_imps simp: is_active_thread_state_def isRestart_def isRunning_def) lemma setupCallerCap_almost_no_orphans [wp]: @@ -1283,7 +1283,7 @@ lemma setupCallerCap_almost_no_orphans [wp]: setupCallerCap sender receiver gr \ \rv s. almost_no_orphans tcb_ptr s \" unfolding setupCallerCap_def - by (wpsimp wp: setThreadState_not_active_almost_no_orphans + by (wpsimp wp: setThreadState_not_active_almost_no_orphans hoare_drop_imps simp: is_active_thread_state_def isRestart_def isRunning_def) crunches doIPCTransfer, setMRs @@ -1332,7 +1332,7 @@ lemma sendIPC_valid_queues' [wp]: \ \rv s. valid_queues' s \" unfolding sendIPC_def apply (wpsimp wp: hoare_drop_imps) - apply (wpsimp | wp (once) sts_st_tcb')+ + apply (wpsimp | wp (once) sts_st_tcb' hoare_drop_imps)+ apply (rule_tac Q="\rv. valid_queues' and valid_objs' and ko_at' rv epptr and (\s. sch_act_wf (ksSchedulerAction s) s)" in hoare_post_imp) apply (clarsimp) @@ -1586,7 +1586,7 @@ lemma cteDeleteOne_no_orphans [wp]: cteDeleteOne slot \ \rv s. no_orphans s \" unfolding cteDeleteOne_def - by (wpsimp wp: assert_inv isFinalCapability_inv weak_if_wp) + by (wpsimp wp: assert_inv haskell_assert_inv isFinalCapability_inv weak_if_wp) crunch valid_objs' [wp]: getThreadReplySlot "valid_objs'" @@ -1752,7 +1752,7 @@ lemma deletingIRQHandler_no_orphans [wp]: deletingIRQHandler irq \ \rv s. no_orphans s \" unfolding deletingIRQHandler_def - by wp auto + by (wpsimp wp: hoare_drop_imps) auto lemma finaliseCap_no_orphans [wp]: "\ \s. no_orphans s \ invs' s \ sch_act_simple s \ valid_cap' cap s \ @@ -2184,7 +2184,7 @@ lemma deleteCallerCap_no_orphans [wp]: deleteCallerCap receiver \ \rv s. no_orphans s \" unfolding deleteCallerCap_def - by wpsimp auto + by (wpsimp wp: hoare_drop_imps) auto lemma remove_neg_strg: "(A \ B) \ ((x \ A) \ (\ x \ B))" diff --git a/proof/refine/ARM/PageTableDuplicates.thy b/proof/refine/ARM/PageTableDuplicates.thy index 0af915db38..9ca4c9b4a9 100644 --- a/proof/refine/ARM/PageTableDuplicates.thy +++ b/proof/refine/ARM/PageTableDuplicates.thy @@ -2169,7 +2169,7 @@ crunch valid_duplicates'[wp]: crunch valid_duplicates'[wp]: receiveIPC "\s. vs_valid_duplicates' (ksPSpace s)" -(wp: getNotification_wp gbn_wp') + (wp: getNotification_wp gbn_wp' crunch_wps) crunch valid_duplicates'[wp]: deleteCallerCap "\s. vs_valid_duplicates' (ksPSpace s)" @@ -2177,6 +2177,7 @@ crunch valid_duplicates'[wp]: crunch valid_duplicates'[wp]: handleReply "\s. vs_valid_duplicates' (ksPSpace s)" + (wp: crunch_wps) crunch valid_duplicates'[wp]: handleYield "\s. vs_valid_duplicates' (ksPSpace s)" diff --git a/proof/refine/ARM/Syscall_R.thy b/proof/refine/ARM/Syscall_R.thy index 3f35fa5c05..81515e8b1d 100644 --- a/proof/refine/ARM/Syscall_R.thy +++ b/proof/refine/ARM/Syscall_R.thy @@ -1362,6 +1362,7 @@ lemma hinv_invs'[wp]: done crunch typ_at'[wp]: handleFault "\s. P (typ_at' T p s)" + (wp: crunch_wps) lemmas handleFault_typ_ats[wp] = typ_at_lifts [OF handleFault_typ_at'] @@ -1793,14 +1794,13 @@ lemma hr_ct_active'[wp]: "\invs' and ct_active'\ handleReply \\rv. ct_active'\" apply (simp add: handleReply_def getSlotCap_def getCurThread_def getThreadCallerSlot_def locateSlot_conv) - apply (rule hoare_seq_ext) - apply (rule_tac t=thread in ct_in_state'_decomp) - apply ((wp hoare_drop_imps | wpc | simp)+)[1] - apply (subst haskell_assert_def) - apply (wp hoare_vcg_all_lift getCTE_wp doReplyTransfer_st_tcb_at_active - | wpc | simp)+ + apply (rule hoare_seq_ext, rename_tac cur_thread) + apply (rule_tac t=cur_thread in ct_in_state'_decomp) + apply (wpsimp wp: getCTE_wp) + apply (fastforce simp: cte_wp_at_ctes_of) + apply (wpsimp wp: getCTE_wp doReplyTransfer_st_tcb_at_active)+ apply (fastforce simp: ct_in_state'_def cte_wp_at_ctes_of valid_cap'_def - dest: ctes_of_valid') + dest: ctes_of_valid') done lemma handleCall_corres: diff --git a/proof/refine/ARM/orphanage/Orphanage.thy b/proof/refine/ARM/orphanage/Orphanage.thy index 4c8554f5ec..797ce7e350 100644 --- a/proof/refine/ARM/orphanage/Orphanage.thy +++ b/proof/refine/ARM/orphanage/Orphanage.thy @@ -1255,7 +1255,7 @@ lemma setupCallerCap_no_orphans [wp]: setupCallerCap sender receiver gr \ \rv s. no_orphans s \" unfolding setupCallerCap_def - apply (wp setThreadState_not_active_no_orphans + apply (wp setThreadState_not_active_no_orphans hoare_drop_imps | clarsimp simp: is_active_thread_state_def isRestart_def isRunning_def)+ done @@ -1264,7 +1264,7 @@ lemma setupCallerCap_almost_no_orphans [wp]: setupCallerCap sender receiver gr \ \rv s. almost_no_orphans tcb_ptr s \" unfolding setupCallerCap_def - apply (wp setThreadState_not_active_almost_no_orphans + apply (wp setThreadState_not_active_almost_no_orphans hoare_drop_imps | clarsimp simp: is_active_thread_state_def isRestart_def isRunning_def)+ done @@ -1311,7 +1311,7 @@ lemma sendIPC_valid_queues' [wp]: \ \rv s. valid_queues' s \" unfolding sendIPC_def apply (wpsimp wp: hoare_drop_imps) - apply (wpsimp | wp (once) sts_st_tcb')+ + apply (wpsimp | wp (once) sts_st_tcb' hoare_drop_imps)+ apply (rule_tac Q="\rv. valid_queues' and valid_objs' and ko_at' rv epptr and (\s. sch_act_wf (ksSchedulerAction s) s)" in hoare_post_imp) apply (clarsimp) @@ -1815,7 +1815,7 @@ lemma deletingIRQHandler_no_orphans [wp]: deletingIRQHandler irq \ \rv s. no_orphans s \" unfolding deletingIRQHandler_def - apply (wp, auto) + apply (wp hoare_drop_imps, auto) done lemma finaliseCap_no_orphans [wp]: @@ -2340,7 +2340,7 @@ lemma deleteCallerCap_no_orphans [wp]: deleteCallerCap receiver \ \rv s. no_orphans s \" unfolding deleteCallerCap_def - by wpsimp auto + by (wpsimp wp: hoare_drop_imps) auto lemma remove_neg_strg: "(A \ B) \ ((x \ A) \ (\ x \ B))" diff --git a/proof/refine/ARM_HYP/PageTableDuplicates.thy b/proof/refine/ARM_HYP/PageTableDuplicates.thy index f7511cce06..44902c2764 100644 --- a/proof/refine/ARM_HYP/PageTableDuplicates.thy +++ b/proof/refine/ARM_HYP/PageTableDuplicates.thy @@ -2102,7 +2102,7 @@ crunch valid_duplicates'[wp]: crunch valid_duplicates'[wp]: receiveIPC "\s. vs_valid_duplicates' (ksPSpace s)" -(wp: getNotification_wp gbn_wp') + (wp: getNotification_wp gbn_wp' crunch_wps) crunch valid_duplicates'[wp]: deleteCallerCap "\s. vs_valid_duplicates' (ksPSpace s)" @@ -2110,6 +2110,7 @@ crunch valid_duplicates'[wp]: crunch valid_duplicates'[wp]: handleReply "\s. vs_valid_duplicates' (ksPSpace s)" + (wp: crunch_wps) crunch valid_duplicates'[wp]: handleYield "\s. vs_valid_duplicates' (ksPSpace s)" diff --git a/proof/refine/ARM_HYP/Syscall_R.thy b/proof/refine/ARM_HYP/Syscall_R.thy index 231e0ea580..4d504c9b84 100644 --- a/proof/refine/ARM_HYP/Syscall_R.thy +++ b/proof/refine/ARM_HYP/Syscall_R.thy @@ -1374,6 +1374,7 @@ lemma hinv_invs'[wp]: done crunch typ_at'[wp]: handleFault "\s. P (typ_at' T p s)" + (wp: crunch_wps) lemmas handleFault_typ_ats[wp] = typ_at_lifts [OF handleFault_typ_at'] @@ -1793,14 +1794,13 @@ lemma hr_ct_active'[wp]: "\invs' and ct_active'\ handleReply \\rv. ct_active'\" apply (simp add: handleReply_def getSlotCap_def getCurThread_def getThreadCallerSlot_def locateSlot_conv) - apply (rule hoare_seq_ext) - apply (rule ct_in_state'_decomp) - apply ((wp hoare_drop_imps | wpc | simp)+)[1] - apply (subst haskell_assert_def) - apply (wp hoare_vcg_all_lift getCTE_wp doReplyTransfer_st_tcb_at_active - | wpc | simp)+ + apply (rule hoare_seq_ext, rename_tac cur_thread) + apply (rule_tac t=cur_thread in ct_in_state'_decomp) + apply (wpsimp wp: getCTE_wp) + apply (fastforce simp: cte_wp_at_ctes_of) + apply (wpsimp wp: getCTE_wp doReplyTransfer_st_tcb_at_active)+ apply (fastforce simp: ct_in_state'_def cte_wp_at_ctes_of valid_cap'_def - dest: ctes_of_valid') + dest: ctes_of_valid') done lemma handleCall_corres: @@ -2123,10 +2123,11 @@ crunches handleVMFault for st_tcb_at'[wp]: "st_tcb_at' P t" and norq[wp]: "\s. P (ksReadyQueues s)" (ignore: getFAR getDFSR getIFSR) + crunches handleVMFault, handleHypervisorFault for cap_to'[wp]: "ex_nonz_cap_to' t" and ksit[wp]: "\s. P (ksIdleThread s)" - (ignore: getFAR getDFSR getIFSR) + (ignore: getFAR getDFSR getIFSR wp: crunch_wps) (* FIXME *) lemma hv_stuff'[wp]: diff --git a/proof/refine/ARM_HYP/VSpace_R.thy b/proof/refine/ARM_HYP/VSpace_R.thy index 9c10addd83..bc4dff1fd1 100644 --- a/proof/refine/ARM_HYP/VSpace_R.thy +++ b/proof/refine/ARM_HYP/VSpace_R.thy @@ -4125,6 +4125,7 @@ lemma vcpuDisable_invs'[wp]: getSCTLR_def get_gic_vcpu_ctrl_hcr_def dsb_def vgicUpdate_def vcpuUpdate_def vcpuSaveReg_def by (wpsimp wp: dmo'_gets_wp setVCPU_vgic_invs' setVCPU_regs_invs' dmo_maskInterrupt_True + hoare_drop_imps simp: doMachineOp_bind empty_fail_cond) lemma vcpuInvalidateActive_invs'[wp]: diff --git a/proof/refine/RISCV64/Detype_R.thy b/proof/refine/RISCV64/Detype_R.thy index b0ec6c2aba..8c9ff5c687 100644 --- a/proof/refine/RISCV64/Detype_R.thy +++ b/proof/refine/RISCV64/Detype_R.thy @@ -2849,25 +2849,14 @@ lemma curDomain_commute: crunch inv[wp]: curDomain P lemma placeNewObject_tcb_at': - notes blah[simp del] = atLeastatMost_subset_iff atLeastLessThan_iff - Int_atLeastAtMost atLeastatMost_empty_iff split_paired_Ex - atLeastAtMost_iff - shows - "\pspace_aligned' and pspace_distinct' - and pspace_no_overlap' ptr (objBits (makeObject::tcb)) - and K(is_aligned ptr (objBits (makeObject::tcb))) - \ placeNewObject ptr (makeObject::tcb) 0 - \\rv s. tcb_at' ptr s \" - apply (simp add:placeNewObject_def placeNewObject'_def split_def alignError_def) + "\pspace_aligned' and pspace_distinct' and pspace_no_overlap' ptr (objBits (makeObject::tcb)) + and K (is_aligned ptr (objBits (makeObject::tcb)))\ + placeNewObject ptr (makeObject::tcb) 0 + \\_ s. tcb_at' ptr s \" + apply (simp add: placeNewObject_def placeNewObject'_def split_def alignError_def) apply wpsimp - apply (clarsimp simp: obj_at'_def lookupAround2_None1 objBits_simps - lookupAround2_char1 field_simps projectKO_opt_tcb return_def ps_clear_def - simp flip: is_aligned_mask) - apply (drule (1) pspace_no_overlap_disjoint') - apply (clarsimp intro!: set_eqI; - drule_tac m = "ksPSpace s" in domI, - erule in_emptyE, - fastforce elim!: in_emptyE simp:objBits_simps mask_def add_diff_eq) + apply (clarsimp simp: obj_at'_def objBits_simps ps_clear_def) + apply (fastforce intro!: set_eqI dest: pspace_no_overlap_disjoint' simp: add_mask_fold) done lemma monad_commute_if_weak_r: diff --git a/proof/refine/RISCV64/Ipc_R.thy b/proof/refine/RISCV64/Ipc_R.thy index 8eb0ed05f3..cdfa3f7423 100644 --- a/proof/refine/RISCV64/Ipc_R.thy +++ b/proof/refine/RISCV64/Ipc_R.thy @@ -3540,8 +3540,6 @@ lemma setupCallerCap_vp[wp]: apply (wp | simp add: valid_pspace'_def valid_tcb_state'_def)+ done -declare haskell_assert_inv[wp del] - lemma setupCallerCap_iflive[wp]: "\if_live_then_nonz_cap' and ex_nonz_cap_to' sender\ setupCallerCap sender rcvr grant diff --git a/proof/refine/RISCV64/Syscall_R.thy b/proof/refine/RISCV64/Syscall_R.thy index 21253a4474..b5688aa2f6 100644 --- a/proof/refine/RISCV64/Syscall_R.thy +++ b/proof/refine/RISCV64/Syscall_R.thy @@ -1332,6 +1332,7 @@ lemma hinv_invs'[wp]: done crunch typ_at'[wp]: handleFault "\s. P (typ_at' T p s)" + (wp: crunch_wps) lemmas handleFault_typ_ats[wp] = typ_at_lifts [OF handleFault_typ_at'] @@ -1755,14 +1756,13 @@ lemma hr_ct_active'[wp]: "\invs' and ct_active'\ handleReply \\rv. ct_active'\" apply (simp add: handleReply_def getSlotCap_def getCurThread_def getThreadCallerSlot_def locateSlot_conv) - apply (rule hoare_seq_ext) - apply (rule ct_in_state'_decomp) - apply ((wp hoare_drop_imps | wpc | simp)+)[1] - apply (subst haskell_assert_def) - apply (wp hoare_vcg_all_lift getCTE_wp doReplyTransfer_st_tcb_at_active - | wpc | simp)+ + apply (rule hoare_seq_ext, rename_tac cur_thread) + apply (rule_tac t=cur_thread in ct_in_state'_decomp) + apply (wpsimp wp: getCTE_wp) + apply (fastforce simp: cte_wp_at_ctes_of) + apply (wpsimp wp: getCTE_wp doReplyTransfer_st_tcb_at_active)+ apply (fastforce simp: ct_in_state'_def cte_wp_at_ctes_of valid_cap'_def - dest: ctes_of_valid') + dest: ctes_of_valid') done lemma handleCall_corres: diff --git a/proof/refine/RISCV64/orphanage/Orphanage.thy b/proof/refine/RISCV64/orphanage/Orphanage.thy index 46f6622f12..68f807737b 100644 --- a/proof/refine/RISCV64/orphanage/Orphanage.thy +++ b/proof/refine/RISCV64/orphanage/Orphanage.thy @@ -1287,7 +1287,7 @@ lemma setupCallerCap_no_orphans [wp]: setupCallerCap sender receiver gr \ \rv s. no_orphans s \" unfolding setupCallerCap_def - apply (wp setThreadState_not_active_no_orphans + apply (wp setThreadState_not_active_no_orphans hoare_drop_imps | clarsimp simp: is_active_thread_state_def isRestart_def isRunning_def)+ done @@ -1303,7 +1303,7 @@ lemma setupCallerCap_almost_no_orphans [wp]: setupCallerCap sender receiver gr \ \rv s. almost_no_orphans tcb_ptr s \" unfolding setupCallerCap_def - apply (wp setThreadState_not_active_almost_no_orphans + apply (wp setThreadState_not_active_almost_no_orphans hoare_drop_imps | clarsimp simp: is_active_thread_state_def isRestart_def isRunning_def)+ done @@ -1354,7 +1354,7 @@ lemma sendIPC_valid_queues' [wp]: \ \rv s. valid_queues' s \" unfolding sendIPC_def apply (wpsimp wp: hoare_drop_imps) - apply (wpsimp | wp (once) sts_st_tcb')+ + apply (wpsimp | wp (once) sts_st_tcb' hoare_drop_imps)+ apply (rule_tac Q="\rv. valid_queues' and valid_objs' and ko_at' rv epptr and (\s. sch_act_wf (ksSchedulerAction s) s)" in hoare_post_imp) apply (clarsimp) @@ -1786,7 +1786,7 @@ lemma deletingIRQHandler_no_orphans [wp]: deletingIRQHandler irq \ \rv s. no_orphans s \" unfolding deletingIRQHandler_def - apply (wp, auto) + apply (wp hoare_drop_imps, auto) done lemma finaliseCap_no_orphans [wp]: @@ -2290,7 +2290,7 @@ lemma deleteCallerCap_no_orphans [wp]: deleteCallerCap receiver \ \rv s. no_orphans s \" unfolding deleteCallerCap_def - by wpsimp auto + by (wpsimp wp: hoare_drop_imps) auto lemma remove_neg_strg: "(A \ B) \ ((x \ A) \ (\ x \ B))" diff --git a/proof/refine/X64/Syscall_R.thy b/proof/refine/X64/Syscall_R.thy index 78aaf0ddcc..130d526020 100644 --- a/proof/refine/X64/Syscall_R.thy +++ b/proof/refine/X64/Syscall_R.thy @@ -1341,6 +1341,7 @@ lemma hinv_invs'[wp]: done crunch typ_at'[wp]: handleFault "\s. P (typ_at' T p s)" + (wp: crunch_wps) lemmas handleFault_typ_ats[wp] = typ_at_lifts [OF handleFault_typ_at'] @@ -1763,14 +1764,13 @@ lemma hr_ct_active'[wp]: "\invs' and ct_active'\ handleReply \\rv. ct_active'\" apply (simp add: handleReply_def getSlotCap_def getCurThread_def getThreadCallerSlot_def locateSlot_conv) - apply (rule hoare_seq_ext) - apply (rule ct_in_state'_decomp) - apply ((wp hoare_drop_imps | wpc | simp)+)[1] - apply (subst haskell_assert_def) - apply (wp hoare_vcg_all_lift getCTE_wp doReplyTransfer_st_tcb_at_active - | wpc | simp)+ + apply (rule hoare_seq_ext, rename_tac cur_thread) + apply (rule_tac t=cur_thread in ct_in_state'_decomp) + apply (wpsimp wp: getCTE_wp) + apply (fastforce simp: cte_wp_at_ctes_of) + apply (wpsimp wp: getCTE_wp doReplyTransfer_st_tcb_at_active)+ apply (fastforce simp: ct_in_state'_def cte_wp_at_ctes_of valid_cap'_def - dest: ctes_of_valid') + dest: ctes_of_valid') done lemma handleCall_corres: From 21771305cb349c92d8cdab8e0aedc59e7f3241e1 Mon Sep 17 00:00:00 2001 From: Michael McInerney Date: Wed, 13 Mar 2024 11:55:59 +1030 Subject: [PATCH 2/8] lib: add filter_hd_equals_tl to LemmaBucket Signed-off-by: Michael McInerney --- lib/LemmaBucket.thy | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/lib/LemmaBucket.thy b/lib/LemmaBucket.thy index 7726ec10c7..be6996d83d 100644 --- a/lib/LemmaBucket.thy +++ b/lib/LemmaBucket.thy @@ -510,4 +510,12 @@ lemma cases_conj_strg: "A \ B \ (P \ A) \ (\ lemma and_not_not_or_imp: "(~ A & ~ B | C) = ((A | B) \ C)" by blast +lemma filter_hd_equals_tl: + "\distinct q; q \ []\ \ filter ((\) (hd q)) q = tl q" + apply (induct q rule: length_induct) + apply (rename_tac list) + apply (case_tac list; simp) + apply (fastforce simp: filter_id_conv) + done + end From 1e4de872d2d2953d76b41788c9839a98b5441599 Mon Sep 17 00:00:00 2001 From: Michael McInerney Date: Wed, 13 Mar 2024 12:21:42 +1030 Subject: [PATCH 3/8] lib: add heap_ls_neighbour_in_set Signed-off-by: Michael McInerney --- lib/Heap_List.thy | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/lib/Heap_List.thy b/lib/Heap_List.thy index 9f91b08a9c..1bbaaab1e8 100644 --- a/lib/Heap_List.thy +++ b/lib/Heap_List.thy @@ -383,6 +383,14 @@ lemma not_head_prev_not_None: using sym_heap_prev_None_is_start heap_path_head by fastforce +lemma heap_ls_neighbour_in_set: + "\heap_ls hp st xs; sym_heap hp hp'; st \ None \ hp' (the st) = None; p \ set xs\ + \ \nbr. (hp p = Some nbr \ nbr \ set xs) \ (hp' p = Some nbr \ nbr \ set xs)" + apply (intro conjI impI allI) + apply (erule (2) heap_ls_next_in_list) + apply (fastforce dest: heap_ls_prev_cases[where np=p] sym_heapD2) + done + (* more on heap_path *) lemma heap_ls_next_takeWhile_append: From 3557e358df733edbddb027896b9f2cf8a4f1301e Mon Sep 17 00:00:00 2001 From: Michael McInerney Date: Wed, 13 Mar 2024 12:22:23 +1030 Subject: [PATCH 4/8] lib: add rsubst2, rsubst3, and rsubst4 to Lib Signed-off-by: Michael McInerney --- lib/Lib.thy | 14 ++++++++++++-- 1 file changed, 12 insertions(+), 2 deletions(-) diff --git a/lib/Lib.thy b/lib/Lib.thy index fae597328d..c658531f36 100644 --- a/lib/Lib.thy +++ b/lib/Lib.thy @@ -2533,8 +2533,18 @@ next by (simp only: pv) (erule not_prefix_cases, auto intro: r1 r2 ih) qed -lemma rsubst: - "\ P s; s = t \ \ P t" +lemmas rsubst = back_subst[where a=s and b=t for s t] + +lemma rsubst2: + "\P a b; a = s; b = t\ \ P s t" + by simp + +lemma rsubst3: + "\P a b c ; a = s; b = t; c = u\ \ P s t u" + by simp + +lemma rsubst4: + "\P a b c d; a = s; b = t; c = u; d = v\ \ P s t u v" by simp lemma ex_impE: "((\x. P x) \ Q) \ P x \ Q" From 33c24023a2c71aa9ae677c85cf8d013b890b39d5 Mon Sep 17 00:00:00 2001 From: Michael McInerney Date: Wed, 13 Mar 2024 12:24:31 +1030 Subject: [PATCH 5/8] lib: add some crossing lemmas for corres_underlying Signed-off-by: Michael McInerney reindent corres_cross_add_guard and friend squash Signed-off-by: Michael McInerney --- lib/Corres_UL.thy | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/lib/Corres_UL.thy b/lib/Corres_UL.thy index bead60647e..906c4b4f66 100644 --- a/lib/Corres_UL.thy +++ b/lib/Corres_UL.thy @@ -1176,6 +1176,18 @@ lemma corres_move_asm: lemmas corres_cross_over_guard = corres_move_asm[rotated] +lemma corres_cross_add_guard: + "\\s s'. \(s,s') \ sr; P s; P' s'\ \ Q' s'; + corres_underlying sr nf nf' r P (P' and Q') f g\ + \ corres_underlying sr nf nf' r P P' f g" + by (fastforce simp: corres_underlying_def) + +lemma corres_cross_add_abs_guard: + "\\s s'. \(s,s') \ sr; P s; P' s'\ \ Q s; + corres_underlying sr nf nf' r (P and Q) P' f g\ + \ corres_underlying sr nf nf' r P P' f g" + by (fastforce simp: corres_underlying_def) + lemma corres_either_alternate: "\ corres_underlying sr nf nf' r P Pa' a c; corres_underlying sr nf nf' r P Pb' b c \ \ corres_underlying sr nf nf' r P (Pa' or Pb') (a \ b) c" From 62d4b1f4204de175935072699bdf97228ee3b323 Mon Sep 17 00:00:00 2001 From: Michael McInerney Date: Wed, 13 Mar 2024 12:25:51 +1030 Subject: [PATCH 6/8] lib: add corres_stateAssert_add_assertion Signed-off-by: Michael McInerney --- lib/Corres_UL.thy | 12 ++++++++++++ 1 file changed, 12 insertions(+) diff --git a/lib/Corres_UL.thy b/lib/Corres_UL.thy index 906c4b4f66..395a327b04 100644 --- a/lib/Corres_UL.thy +++ b/lib/Corres_UL.thy @@ -1268,6 +1268,18 @@ lemma corres_stateAssert_implied2: apply simp done +lemma corres_stateAssert_add_assertion: + "\ corres_underlying sr nf nf' r P (Q and Q') f (g ()); + \s s'. \ (s, s') \ sr; P s; Q s' \ \ Q' s' \ + \ corres_underlying sr nf nf' r P Q f (stateAssert Q' [] >>= g)" + apply (clarsimp simp: bind_assoc stateAssert_def) + apply (rule corres_symb_exec_r [OF _ get_sp]) + apply (rule corres_assume_pre) + apply (rule corres_assert_assume) + apply (erule corres_guard_imp, clarsimp+) + apply (wp | rule no_fail_pre)+ + done + lemma corres_add_noop_lhs: "corres_underlying sr nf nf' r P P' (return () >>= (\_. f)) g \ corres_underlying sr nf nf' r P P' f g" From a49ccceb50adfef31e2590cec9ccad35c9870e30 Mon Sep 17 00:00:00 2001 From: Michael McInerney Date: Fri, 15 Mar 2024 21:49:53 +1030 Subject: [PATCH 7/8] lib/monads: rename assert_opt_ovalid to oassert_opt_ovalid and make [wp] Signed-off-by: Michael McInerney --- lib/Monads/reader_option/Reader_Option_VCG.thy | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lib/Monads/reader_option/Reader_Option_VCG.thy b/lib/Monads/reader_option/Reader_Option_VCG.thy index 7fd77e32c2..d7f77bae3f 100644 --- a/lib/Monads/reader_option/Reader_Option_VCG.thy +++ b/lib/Monads/reader_option/Reader_Option_VCG.thy @@ -129,7 +129,7 @@ lemma owhile_ovalid[wp]: apply auto done -lemma assert_opt_ovalid: +lemma oassert_opt_ovalid[wp]: "\\s. \y. x = Some y \ Q y s\ oassert_opt x \Q\" unfolding oassert_opt_def by (case_tac x; wpsimp) From e1da66e0a40771ae11ba004d33326056a565fae2 Mon Sep 17 00:00:00 2001 From: Michael McInerney Date: Fri, 15 Mar 2024 21:53:03 +1030 Subject: [PATCH 8/8] lib/monads: add reader_case_option_wp Signed-off-by: Michael McInerney --- lib/Monads/reader_option/Reader_Option_VCG.thy | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/lib/Monads/reader_option/Reader_Option_VCG.thy b/lib/Monads/reader_option/Reader_Option_VCG.thy index d7f77bae3f..512b271222 100644 --- a/lib/Monads/reader_option/Reader_Option_VCG.thy +++ b/lib/Monads/reader_option/Reader_Option_VCG.thy @@ -114,6 +114,11 @@ lemma ovalid_if_split: "\ P \ \Q\ f \S\; \P \ \R\ g \S\ \ \ \\s. (P \ Q s) \ (\P \ R s)\ if P then f else g \S\" by simp +lemma reader_case_option_wp[wp]: + "\\x. \P x\ m x \Q\; \P'\ m' \Q\\ + \ \\s. (x = None \ P' s) \ (\y. x = Some y \ P y s)\ case_option m' m x \Q\" + by (cases x; simp) + lemma ovalid_case_prod[wp]: assumes "(\x y. ovalid (P x y) (B x y) Q)" shows "ovalid (case v of (x, y) \ P x y) (case v of (x, y) \ B x y) Q"