From d9411823557dd47151f3454e73f82b24bc855089 Mon Sep 17 00:00:00 2001 From: Corey Lewis Date: Tue, 2 Apr 2024 17:31:59 +1100 Subject: [PATCH] proof: remove hoare_vcg_precond_imp from wp_comb This being a `wp_comb` rule is a leftover from before `wp_pre` was implemented and it is being removed because in some cases it can cause unintended schematics to appear in the assumptions. This commit also updates all of the proofs that accidentally depended on it being a `wp_comb` rule. In many cases this involved `including classic_wp_pre`, which locally returns the wp attributes to a state similar to what it was when the proofs were first written. Other cases required small rewrites, often involving using `wpsimp` instead of `wp`, and removing some uses of `wp (once)`. Signed-off-by: Corey Lewis --- proof/access-control/ARM/ArchFinalise_AC.thy | 2 +- proof/access-control/ARM/ArchRetype_AC.thy | 5 +- proof/access-control/DomainSepInv.thy | 4 +- proof/access-control/Finalise_AC.thy | 2 +- proof/access-control/Ipc_AC.thy | 4 +- .../RISCV64/ArchFinalise_AC.thy | 2 +- .../access-control/RISCV64/ArchRetype_AC.thy | 3 +- proof/access-control/Retype_AC.thy | 2 +- proof/crefine/AARCH64/Fastpath_Equiv.thy | 5 +- proof/crefine/ARM/Fastpath_Equiv.thy | 5 +- proof/crefine/ARM_HYP/Fastpath_Equiv.thy | 5 +- proof/crefine/Move_C.thy | 2 +- proof/drefine/CNode_DR.thy | 3 +- proof/drefine/Finalise_DR.thy | 3 +- proof/drefine/Ipc_DR.thy | 11 ++- proof/drefine/Schedule_DR.thy | 2 +- proof/infoflow/ADT_IF.thy | 5 +- proof/infoflow/ARM/ArchRetype_IF.thy | 2 +- proof/infoflow/ARM/ArchScheduler_IF.thy | 2 +- proof/infoflow/Decode_IF.thy | 20 ++--- proof/infoflow/FinalCaps.thy | 4 +- proof/infoflow/Finalise_IF.thy | 4 +- proof/infoflow/Ipc_IF.thy | 5 +- proof/infoflow/Noninterference.thy | 7 +- proof/infoflow/RISCV64/ArchArch_IF.thy | 2 +- proof/infoflow/RISCV64/ArchRetype_IF.thy | 2 +- proof/infoflow/RISCV64/ArchScheduler_IF.thy | 3 +- proof/infoflow/Scheduler_IF.thy | 4 +- proof/infoflow/Syscall_IF.thy | 4 +- proof/infoflow/Tcb_IF.thy | 21 ++--- .../ARM/ArchVSpaceEntries_AI.thy | 3 +- .../ARM_HYP/ArchVSpaceEntries_AI.thy | 2 +- proof/invariant-abstract/DetSchedAux_AI.thy | 11 +-- .../DetSchedSchedule_AI.thy | 84 +++++++++---------- proof/invariant-abstract/Syscall_AI.thy | 2 +- proof/refine/AARCH64/Finalise_R.thy | 2 +- proof/refine/AARCH64/IpcCancel_R.thy | 6 +- proof/refine/AARCH64/Ipc_R.thy | 11 ++- proof/refine/AARCH64/Retype_R.thy | 13 ++- proof/refine/AARCH64/Schedule_R.thy | 5 +- proof/refine/AARCH64/TcbAcc_R.thy | 8 +- proof/refine/AARCH64/Tcb_R.thy | 4 +- proof/refine/AARCH64/orphanage/Orphanage.thy | 4 +- proof/refine/ARM/Finalise_R.thy | 2 +- proof/refine/ARM/IpcCancel_R.thy | 6 +- proof/refine/ARM/Ipc_R.thy | 13 ++- proof/refine/ARM/Retype_R.thy | 22 ++--- proof/refine/ARM/Schedule_R.thy | 5 +- proof/refine/ARM/TcbAcc_R.thy | 8 +- proof/refine/ARM/Tcb_R.thy | 4 +- proof/refine/ARM/VSpace_R.thy | 10 +-- proof/refine/ARM/orphanage/Orphanage.thy | 8 +- proof/refine/ARM_HYP/Finalise_R.thy | 4 +- proof/refine/ARM_HYP/IpcCancel_R.thy | 6 +- proof/refine/ARM_HYP/Ipc_R.thy | 11 ++- proof/refine/ARM_HYP/Retype_R.thy | 22 ++--- proof/refine/ARM_HYP/Schedule_R.thy | 5 +- proof/refine/ARM_HYP/TcbAcc_R.thy | 8 +- proof/refine/ARM_HYP/Tcb_R.thy | 4 +- proof/refine/ARM_HYP/VSpace_R.thy | 10 +-- proof/refine/RISCV64/Finalise_R.thy | 2 +- proof/refine/RISCV64/IpcCancel_R.thy | 6 +- proof/refine/RISCV64/Ipc_R.thy | 11 ++- proof/refine/RISCV64/Retype_R.thy | 13 ++- proof/refine/RISCV64/Schedule_R.thy | 5 +- proof/refine/RISCV64/TcbAcc_R.thy | 8 +- proof/refine/RISCV64/Tcb_R.thy | 4 +- proof/refine/RISCV64/orphanage/Orphanage.thy | 8 +- proof/refine/X64/Finalise_R.thy | 2 +- proof/refine/X64/IpcCancel_R.thy | 6 +- proof/refine/X64/Ipc_R.thy | 13 ++- proof/refine/X64/Retype_R.thy | 22 ++--- proof/refine/X64/Schedule_R.thy | 5 +- proof/refine/X64/TcbAcc_R.thy | 8 +- proof/refine/X64/Tcb_R.thy | 4 +- proof/refine/X64/VSpace_R.thy | 10 +-- 76 files changed, 267 insertions(+), 308 deletions(-) diff --git a/proof/access-control/ARM/ArchFinalise_AC.thy b/proof/access-control/ARM/ArchFinalise_AC.thy index 37a9bdfdd2..4f7752c65b 100644 --- a/proof/access-control/ARM/ArchFinalise_AC.thy +++ b/proof/access-control/ARM/ArchFinalise_AC.thy @@ -107,7 +107,7 @@ lemma finalise_cap_fst_ret[Finalise_AC_assms]: "\\_. P NullCap \ (\a b c. P (Zombie a b c))\ finalise_cap cap is_final \\rv _. P (fst rv)\" - including no_pre + including classic_wp_pre apply (cases cap, simp_all add: arch_finalise_cap_def split del: if_split) apply (wp | simp add: comp_def split del: if_split | fastforce)+ apply (rule hoare_pre) diff --git a/proof/access-control/ARM/ArchRetype_AC.thy b/proof/access-control/ARM/ArchRetype_AC.thy index 647bf990c3..6d3a9b813c 100644 --- a/proof/access-control/ARM/ArchRetype_AC.thy +++ b/proof/access-control/ARM/ArchRetype_AC.thy @@ -98,7 +98,7 @@ lemma copy_global_mappings_integrity: \\_. integrity aag X st\" apply (rule hoare_gen_asm) apply (simp add: copy_global_mappings_def) - apply (wp mapM_x_wp[OF _ subset_refl] store_pde_respects) + apply (wp mapM_x_wp[OF _ subset_refl] store_pde_respects)+ apply (drule subsetD[OF copy_global_mappings_index_subset]) apply (fastforce simp: pd_shifting') apply wpsimp+ @@ -329,8 +329,7 @@ lemma dmo_freeMemory_respects[Retype_AC_assms]: apply wp apply clarsimp apply (erule use_valid) - apply (wp mol_respects mapM_x_wp' storeWord_integrity_autarch) - apply simp + apply (wpsimp wp: mol_respects mapM_x_wp' storeWord_integrity_autarch) apply (clarsimp simp: word_size_def word_bits_def word_size_bits_def upto_enum_step_shift_red[where us=2, simplified]) apply (erule bspec) diff --git a/proof/access-control/DomainSepInv.thy b/proof/access-control/DomainSepInv.thy index 4ea7c3ce0a..2aa2e02e54 100644 --- a/proof/access-control/DomainSepInv.thy +++ b/proof/access-control/DomainSepInv.thy @@ -452,7 +452,7 @@ lemma finalise_cap_domain_sep_inv_cap: "\\s. domain_sep_inv_cap irqs cap\ finalise_cap cap b \\rv s :: det_ext state. domain_sep_inv_cap irqs (fst rv)\" - including no_pre + including classic_wp_pre apply (case_tac cap) apply (wp | simp add: o_def split del: if_split split: cap.splits | fastforce split: if_splits simp: domain_sep_inv_cap_def)+ @@ -784,7 +784,7 @@ lemma invoke_control_domain_sep_inv: "\domain_sep_inv irqs st and irq_control_inv_valid i\ invoke_irq_control i \\_ s. domain_sep_inv irqs (st :: 'state_ext state) (s :: det_ext state)\" - including no_pre + including classic_wp_pre apply (case_tac i) apply (case_tac irqs) apply (wp cap_insert_domain_sep_inv' | simp )+ diff --git a/proof/access-control/Finalise_AC.thy b/proof/access-control/Finalise_AC.thy index d457a2c991..aa92c68dd3 100644 --- a/proof/access-control/Finalise_AC.thy +++ b/proof/access-control/Finalise_AC.thy @@ -700,7 +700,7 @@ lemma finalise_cap_auth': "\pas_refined aag and K (pas_cap_cur_auth aag cap)\ finalise_cap cap final \\rv _. pas_cap_cur_auth aag (fst rv)\" - including no_pre + including classic_wp_pre apply (rule hoare_gen_asm) apply (cases cap, simp_all split del: if_split) apply (wp | simp add: comp_def hoare_post_taut[where P = \] split del: if_split diff --git a/proof/access-control/Ipc_AC.thy b/proof/access-control/Ipc_AC.thy index 622495d2c9..28b60fd2ee 100644 --- a/proof/access-control/Ipc_AC.thy +++ b/proof/access-control/Ipc_AC.thy @@ -1781,7 +1781,7 @@ lemma cap_insert_ext_integrity_in_ipc_autarch: apply (clarsimp simp: integrity_tcb_in_ipc_def integrity_def tcb_states_of_state_def get_tcb_def split del: if_split cong: if_cong) - including no_pre + including classic_wp_pre apply wp apply (rule hoare_vcg_conj_lift) apply (simp add: list_integ_def del: split_paired_All) @@ -2655,7 +2655,7 @@ lemma empty_slot_respects_in_ipc_autarch: unfolding empty_slot_def post_cap_deletion_def apply simp apply (wp add: set_cap_respects_in_ipc_autarch set_original_respects_in_ipc_autarch) - apply (wp empty_slot_extended_list_integ_lift_in_ipc empty_slot_list_integrity') + apply (wpsimp wp: empty_slot_extended_list_integ_lift_in_ipc empty_slot_list_integrity') apply simp apply wp+ apply (wp set_cdt_empty_slot_respects_in_ipc_autarch) diff --git a/proof/access-control/RISCV64/ArchFinalise_AC.thy b/proof/access-control/RISCV64/ArchFinalise_AC.thy index 6068ca8b1f..ac72ae61b5 100644 --- a/proof/access-control/RISCV64/ArchFinalise_AC.thy +++ b/proof/access-control/RISCV64/ArchFinalise_AC.thy @@ -280,7 +280,7 @@ lemma finalise_cap_fst_ret[Finalise_AC_assms]: "\\_. P NullCap \ (\a b c. P (Zombie a b c))\ finalise_cap cap is_final \\rv _. P (fst rv)\" - including no_pre + including classic_wp_pre apply (cases cap, simp_all add: arch_finalise_cap_def split del: if_split) apply (wp | simp add: comp_def split del: if_split | fastforce)+ apply (rule hoare_pre) diff --git a/proof/access-control/RISCV64/ArchRetype_AC.thy b/proof/access-control/RISCV64/ArchRetype_AC.thy index ddfe34ac64..22abf7683e 100644 --- a/proof/access-control/RISCV64/ArchRetype_AC.thy +++ b/proof/access-control/RISCV64/ArchRetype_AC.thy @@ -292,8 +292,7 @@ lemma dmo_freeMemory_respects[Retype_AC_assms]: apply wp apply clarsimp apply (erule use_valid) - apply (wp mol_respects mapM_x_wp' storeWord_integrity_autarch) - apply simp + apply (wpsimp wp: mol_respects mapM_x_wp' storeWord_integrity_autarch) apply (clarsimp simp: word_size_def word_size_bits_def word_bits_def upto_enum_step_shift_red[where us=3, simplified]) apply (erule bspec) diff --git a/proof/access-control/Retype_AC.thy b/proof/access-control/Retype_AC.thy index de013d7d0c..9aa79123be 100644 --- a/proof/access-control/Retype_AC.thy +++ b/proof/access-control/Retype_AC.thy @@ -497,7 +497,7 @@ lemma retype_region_ext_pas_refined: "\pas_refined aag and pas_cur_domain aag and K (\x\ set xs. is_subject aag x)\ retype_region_ext xs ty \\_. pas_refined aag\" - including no_pre + including classic_wp_pre apply (subst and_assoc[symmetric]) apply (wp retype_region_ext_extended.pas_refined_tcb_domain_map_wellformed') apply (simp add: retype_region_ext_def, wp) diff --git a/proof/crefine/AARCH64/Fastpath_Equiv.thy b/proof/crefine/AARCH64/Fastpath_Equiv.thy index b005190e93..20bbbb6f91 100644 --- a/proof/crefine/AARCH64/Fastpath_Equiv.thy +++ b/proof/crefine/AARCH64/Fastpath_Equiv.thy @@ -755,8 +755,7 @@ lemma fastpath_callKernel_SysCall_corres: apply ((wp assert_inv threadSet_pred_tcb_at_state cteInsert_obj_at'_not_queued | wps)+)[1] apply ((wp assert_inv threadSet_pred_tcb_at_state cteInsert_obj_at'_not_queued | wps)+)[1] apply ((wp assert_inv threadSet_pred_tcb_at_state cteInsert_obj_at'_not_queued | wps)+)[1] - apply (wp fastpathBestSwitchCandidate_lift[where f="threadSet f t" for f t]) - apply simp + apply (wpsimp wp: fastpathBestSwitchCandidate_lift[where f="threadSet f t" for f t]) apply ((wp assert_inv threadSet_pred_tcb_at_state cteInsert_obj_at'_not_queued | wps)+)[1] @@ -1494,7 +1493,7 @@ lemma fastpath_callKernel_SysReplyRecv_corres: (invs' and ct_in_state' ((=) Running) and (\s. ksSchedulerAction s = ResumeCurrentThread) and cnode_caps_gsCNodes') (callKernel (SyscallEvent SysReplyRecv)) (fastpaths SysReplyRecv)" - including no_pre + including classic_wp_pre supply if_cong[cong] option.case_cong[cong] supply if_split[split del] supply user_getreg_inv[wp] (* FIXME *) diff --git a/proof/crefine/ARM/Fastpath_Equiv.thy b/proof/crefine/ARM/Fastpath_Equiv.thy index e4fedded83..036a334477 100644 --- a/proof/crefine/ARM/Fastpath_Equiv.thy +++ b/proof/crefine/ARM/Fastpath_Equiv.thy @@ -661,8 +661,7 @@ lemma fastpath_callKernel_SysCall_corres: apply ((wp assert_inv threadSet_pred_tcb_at_state cteInsert_obj_at'_not_queued | wps)+)[1] apply ((wp assert_inv threadSet_pred_tcb_at_state cteInsert_obj_at'_not_queued | wps)+)[1] apply ((wp assert_inv threadSet_pred_tcb_at_state cteInsert_obj_at'_not_queued | wps)+)[1] - apply (wp fastpathBestSwitchCandidate_lift[where f="threadSet f t" for f t]) - apply simp + apply (wpsimp wp: fastpathBestSwitchCandidate_lift[where f="threadSet f t" for f t]) apply ((wp assert_inv threadSet_pred_tcb_at_state cteInsert_obj_at'_not_queued | wps)+)[1] @@ -1364,7 +1363,7 @@ lemma fastpath_callKernel_SysReplyRecv_corres: (invs' and ct_in_state' ((=) Running) and (\s. ksSchedulerAction s = ResumeCurrentThread) and cnode_caps_gsCNodes') (callKernel (SyscallEvent SysReplyRecv)) (fastpaths SysReplyRecv)" - including no_pre + including classic_wp_pre supply if_cong[cong] option.case_cong[cong] supply if_split[split del] supply user_getreg_inv[wp] (* FIXME *) diff --git a/proof/crefine/ARM_HYP/Fastpath_Equiv.thy b/proof/crefine/ARM_HYP/Fastpath_Equiv.thy index 7bfd4520e8..826695fab6 100644 --- a/proof/crefine/ARM_HYP/Fastpath_Equiv.thy +++ b/proof/crefine/ARM_HYP/Fastpath_Equiv.thy @@ -661,8 +661,7 @@ lemma fastpath_callKernel_SysCall_corres: apply ((wp assert_inv threadSet_pred_tcb_at_state cteInsert_obj_at'_not_queued | wps)+)[1] apply ((wp assert_inv threadSet_pred_tcb_at_state cteInsert_obj_at'_not_queued | wps)+)[1] apply ((wp assert_inv threadSet_pred_tcb_at_state cteInsert_obj_at'_not_queued | wps)+)[1] - apply (wp fastpathBestSwitchCandidate_lift[where f="threadSet f t" for f t]) - apply simp + apply (wpsimp wp: fastpathBestSwitchCandidate_lift[where f="threadSet f t" for f t]) apply ((wp assert_inv threadSet_pred_tcb_at_state cteInsert_obj_at'_not_queued | wps)+)[1] @@ -1367,7 +1366,7 @@ lemma fastpath_callKernel_SysReplyRecv_corres: (invs' and ct_in_state' ((=) Running) and (\s. ksSchedulerAction s = ResumeCurrentThread) and cnode_caps_gsCNodes') (callKernel (SyscallEvent SysReplyRecv)) (fastpaths SysReplyRecv)" - including no_pre + including classic_wp_pre supply if_cong[cong] option.case_cong[cong] supply if_split[split del] supply user_getreg_inv[wp] (* FIXME *) diff --git a/proof/crefine/Move_C.thy b/proof/crefine/Move_C.thy index 997c196e24..e0e8dae8cc 100644 --- a/proof/crefine/Move_C.thy +++ b/proof/crefine/Move_C.thy @@ -988,7 +988,7 @@ lemma empty_fail_getIdleThread [simp,intro!]: lemma setTCB_cur: "\cur_tcb'\ setObject t (v::tcb) \\_. cur_tcb'\" - including no_pre + including classic_wp_pre apply (wp cur_tcb_lift) apply (simp add: setObject_def split_def updateObject_default_def) apply wp diff --git a/proof/drefine/CNode_DR.thy b/proof/drefine/CNode_DR.thy index f8bf527b4f..e92b1742eb 100644 --- a/proof/drefine/CNode_DR.thy +++ b/proof/drefine/CNode_DR.thy @@ -244,8 +244,7 @@ lemma insert_cap_sibling_corres: cte_wp_at_caps_of_state has_parent_cte_at is_physical_def dest!:is_untyped_cap_eqD) apply fastforce - apply (wp get_cap_wp set_cap_idle | simp)+ - apply clarsimp + apply (wpsimp wp: get_cap_wp set_cap_idle)+ apply (clarsimp simp: not_idle_thread_def) apply (clarsimp simp: caps_of_state_transform_opt_cap cte_wp_at_caps_of_state transform_cap_def) diff --git a/proof/drefine/Finalise_DR.thy b/proof/drefine/Finalise_DR.thy index 4ce1997a8b..46aa47278e 100644 --- a/proof/drefine/Finalise_DR.thy +++ b/proof/drefine/Finalise_DR.thy @@ -486,7 +486,7 @@ lemma dcorres_deleting_irq_handler: apply (rule corres_split[OF dcorres_get_irq_slot]) apply (simp, rule delete_cap_simple_corres,simp) apply (rule hoare_vcg_precond_imp [where Q="invs and valid_etcbs"]) - including no_pre + including classic_wp_pre apply (wpsimp simp:get_irq_slot_def)+ apply (rule irq_node_image_not_idle) apply (simp add:invs_def valid_state_def)+ @@ -2503,6 +2503,7 @@ lemma dcorres_delete_asid: apply (wp | clarsimp)+ apply simp apply (wp | clarsimp)+ + apply (rule hoare_pre, wp, clarsimp) apply (rule hoare_pre, wp) apply simp apply (wp | clarsimp)+ diff --git a/proof/drefine/Ipc_DR.thy b/proof/drefine/Ipc_DR.thy index 7e753044d2..e80cd947e2 100644 --- a/proof/drefine/Ipc_DR.thy +++ b/proof/drefine/Ipc_DR.thy @@ -702,7 +702,7 @@ lemma tcb_sched_action_tcb_at_not_idle[wp]: lemma valid_idle_cancel_all_ipc: "\valid_idle and valid_state :: det_state \ bool\ IpcCancel_A.cancel_all_ipc word1 \\a. valid_idle\" - including no_pre + including classic_wp_pre apply (simp add:cancel_all_ipc_def) apply (wp|wpc|simp)+ apply (rename_tac queue list) @@ -757,7 +757,7 @@ lemma valid_idle_cancel_all_ipc: lemma valid_idle_cancel_all_signals: "\valid_idle and valid_state :: det_state \ bool\ IpcCancel_A.cancel_all_signals word1 \\a. valid_idle\" - including no_pre + including classic_wp_pre apply (simp add:cancel_all_signals_def) apply (wp|wpc|simp)+ apply (rename_tac list) @@ -1285,10 +1285,9 @@ next apply (rule dcorres_set_extra_badge,simp) apply (rule Cons.hyps, rule refl, rule refl, simp) apply wp[1] - apply (simp add: store_word_offs_def set_extra_badge_def - not_idle_thread_def ipc_frame_wp_at_def - split_def) - apply (wp evalMonad_lookup_ipc_buffer_wp) + apply (simp add: store_word_offs_def set_extra_badge_def not_idle_thread_def + ipc_frame_wp_at_def split_def) + apply (wpsimp wp: evalMonad_lookup_ipc_buffer_wp) apply (erule cte_wp_at_weakenE) apply (simp add:ipc_buffer_wp_at_def)+ apply wp diff --git a/proof/drefine/Schedule_DR.thy b/proof/drefine/Schedule_DR.thy index 2ef3fefa7d..776ec751a6 100644 --- a/proof/drefine/Schedule_DR.thy +++ b/proof/drefine/Schedule_DR.thy @@ -81,7 +81,7 @@ lemma change_current_domain_and_switch_to_idle_thread_dcorres: Schedule_D.switch_to_thread None od) switch_to_idle_thread" - including no_pre + including classic_wp_pre apply (clarsimp simp: Schedule_D.switch_to_thread_def switch_to_idle_thread_def) apply (rule dcorres_symb_exec_r) apply (rule corres_guard_imp) diff --git a/proof/infoflow/ADT_IF.thy b/proof/infoflow/ADT_IF.thy index bb7d5fd295..4ece642746 100644 --- a/proof/infoflow/ADT_IF.thy +++ b/proof/infoflow/ADT_IF.thy @@ -1665,7 +1665,7 @@ lemma schedule_if_globals_equiv_scheduler[wp]: \\_. globals_equiv_scheduler st\" apply (simp add: schedule_if_def) apply wp - apply (wp globals_equiv_scheduler_inv'[where P="invs"] activate_thread_globals_equiv) + apply (wpsimp wp: globals_equiv_scheduler_inv'[where P="invs"] activate_thread_globals_equiv) apply (simp add: invs_arch_state invs_valid_idle) apply (wp | simp)+ done @@ -2618,8 +2618,7 @@ lemma perform_invocation_irq_state_inv: invoke_tcb_irq_state_inv invoke_cnode_irq_state_inv[simplified validE_R_def] | clarsimp | simp add: invoke_domain_def)+\)?) apply wp - apply (wp irq_state_inv_triv' invoke_irq_control_irq_masks) - apply clarsimp + apply (wpsimp wp: irq_state_inv_triv' invoke_irq_control_irq_masks) apply assumption apply auto[1] apply wp diff --git a/proof/infoflow/ARM/ArchRetype_IF.thy b/proof/infoflow/ARM/ArchRetype_IF.thy index d217f46c4f..d30498d5a1 100644 --- a/proof/infoflow/ARM/ArchRetype_IF.thy +++ b/proof/infoflow/ARM/ArchRetype_IF.thy @@ -278,7 +278,7 @@ lemma copy_global_mappings_globals_equiv: "\globals_equiv s and (\s. x \ arm_global_pd (arch_state s) \ is_aligned x pd_bits)\ copy_global_mappings x \\_. globals_equiv s\" - unfolding copy_global_mappings_def including no_pre + unfolding copy_global_mappings_def including classic_wp_pre apply simp apply wp apply (rule_tac Q="\_. globals_equiv s and (\s. x \ arm_global_pd (arch_state s) \ diff --git a/proof/infoflow/ARM/ArchScheduler_IF.thy b/proof/infoflow/ARM/ArchScheduler_IF.thy index 54cc779509..20465707aa 100644 --- a/proof/infoflow/ARM/ArchScheduler_IF.thy +++ b/proof/infoflow/ARM/ArchScheduler_IF.thy @@ -186,7 +186,7 @@ lemma globals_equiv_scheduler_inv'[Scheduler_IF_assms]: lemma clearExMonitor_globals_equiv_scheduler[wp]: "do_machine_op clearExMonitor \globals_equiv_scheduler sta\" - unfolding clearExMonitor_def including no_pre + unfolding clearExMonitor_def including classic_wp_pre apply (wp dmo_no_mem_globals_equiv_scheduler) apply simp apply (simp add: simpler_modify_def valid_def) diff --git a/proof/infoflow/Decode_IF.thy b/proof/infoflow/Decode_IF.thy index 40a3779db8..92b2ee2ddc 100644 --- a/proof/infoflow/Decode_IF.thy +++ b/proof/infoflow/Decode_IF.thy @@ -110,8 +110,8 @@ lemma slot_cap_long_running_delete_reads_respects_f: apply (fastforce simp: long_running_delete_def is_final_cap_def gets_bind_ign intro: return_ev)+ apply (wp is_final_cap_reads_respects[where st=st])[1] apply (fastforce simp: long_running_delete_def is_final_cap_def gets_bind_ign intro: return_ev)+ - apply (wp reads_respects_f[OF get_cap_rev, where Q="\" and st=st], blast) - apply (wp get_cap_wp | simp)+ + apply (wpsimp wp: reads_respects_f[OF get_cap_rev, where Q="\" and st=st]) + apply (wp get_cap_wp) apply (fastforce intro!: cte_wp_valid_cap aag_has_auth_to_obj_refs_of_owned_cap simp: is_zombie_def dest: silc_inv_not_subject) done @@ -227,14 +227,14 @@ lemma decode_tcb_invocation_reads_respects_f: apply (simp add: unlessE_def[symmetric] unlessE_whenE split del: if_split cong: gen_invocation_labels.case_cong) apply (rule equiv_valid_guard_imp) - apply (wp (once) requiv_cur_thread_eq range_check_ev respects_f[OF derive_cap_rev] - derive_cap_inv slot_cap_long_running_delete_reads_respects_f[where st=st] - respects_f[OF check_valid_ipc_buffer_rev] check_valid_ipc_buffer_inv - respects_f[OF decode_set_priority_rev] respects_f[OF decode_set_mcpriority_rev] - respects_f[OF decode_set_sched_params_rev] - respects_f[OF get_simple_ko_reads_respects] - respects_f[OF get_bound_notification_reads_respects'] - | wp (once) whenE_throwError_wp + apply (wp requiv_cur_thread_eq range_check_ev respects_f[OF derive_cap_rev] + derive_cap_inv slot_cap_long_running_delete_reads_respects_f[where st=st] + respects_f[OF check_valid_ipc_buffer_rev] check_valid_ipc_buffer_inv + respects_f[OF decode_set_priority_rev] respects_f[OF decode_set_mcpriority_rev] + respects_f[OF decode_set_sched_params_rev] + respects_f[OF get_simple_ko_reads_respects] + respects_f[OF get_bound_notification_reads_respects'] + whenE_throwError_wp | wp (once) hoare_drop_imps | wpc | simp add: if_apply_def2 split del: if_split add: o_def split_def)+ diff --git a/proof/infoflow/FinalCaps.thy b/proof/infoflow/FinalCaps.thy index c90d1c1e32..1ec376fff3 100644 --- a/proof/infoflow/FinalCaps.thy +++ b/proof/infoflow/FinalCaps.thy @@ -1441,7 +1441,7 @@ lemma finalise_cap_ret_is_subject: finalise_cap cap is_final \\rv _ :: det_state. case (fst rv) of Zombie ptr bits n \ is_subject aag (obj_ref_of (fst rv)) | _ \ True\" - including no_pre + including classic_wp_pre apply (case_tac cap, simp_all add: is_zombie_def) apply (wp | simp add: comp_def | rule impI | rule conjI)+ apply (fastforce simp: valid_def dest: arch_finalise_cap_ret) @@ -2400,7 +2400,7 @@ lemma transfer_caps_silc_inv: apply (simp add: transfer_caps_def) apply (wpc | wp)+ apply (rule_tac P = "\x \ set dest_slots. is_subject aag (fst x)" in hoare_gen_asm) - apply (wp transfer_caps_loop_pres_dest cap_insert_silc_inv) + apply (wpsimp wp: transfer_caps_loop_pres_dest cap_insert_silc_inv) apply (fastforce simp: silc_inv_def) apply (wp get_receive_slots_authorised hoare_vcg_all_lift hoare_vcg_imp_lift | simp)+ apply (fastforce elim: cte_wp_at_weakenE) diff --git a/proof/infoflow/Finalise_IF.thy b/proof/infoflow/Finalise_IF.thy index 232c643622..87ffc0d644 100644 --- a/proof/infoflow/Finalise_IF.thy +++ b/proof/infoflow/Finalise_IF.thy @@ -570,10 +570,10 @@ lemma tcb_sched_action_reads_respects: apply (force intro: domtcbs simp: get_etcb_def) apply (simp add: equiv_valid_def2 ethread_get_def) apply (rule equiv_valid_rv_bind) - apply (wp equiv_valid_rv_trivial', simp) + apply (wpsimp wp: equiv_valid_rv_trivial') apply (rule equiv_valid_2_bind) prefer 2 - apply (wp equiv_valid_rv_trivial, simp) + apply (wpsimp wp: equiv_valid_rv_trivial) apply (rule equiv_valid_2_bind) apply (rule_tac P=\ and P'=\ and L="{pasObjectAbs aag t}" and L'="{pasObjectAbs aag t}" in ev2_invisible[OF domains_distinct]) diff --git a/proof/infoflow/Ipc_IF.thy b/proof/infoflow/Ipc_IF.thy index 80f3d615df..aa0ca12419 100644 --- a/proof/infoflow/Ipc_IF.thy +++ b/proof/infoflow/Ipc_IF.thy @@ -601,6 +601,9 @@ lemma send_signal_reads_respects: set_thread_state_runnable_equiv_but_for_labels get_simple_ko_wp gts_wp update_waiting_ntfn_equiv_but_for_labels blocked_cancel_ipc_nosts_equiv_but_for_labels + \ \FIXME: The following line is working around the fact that wp (once) doesn't invoke + wp_pre. If that is changed then it could be removed.\ + | wp_pre0 | wpc | wps)+ apply (elim conjE) @@ -1717,7 +1720,7 @@ lemma copy_mrs_globals_equiv: "\globals_equiv s and valid_arch_state and (\s. receiver \ idle_thread s)\ copy_mrs sender sbuf receiver rbuf n \\_. globals_equiv s\" - unfolding copy_mrs_def including no_pre + unfolding copy_mrs_def including classic_wp_pre apply (wp | wpc)+ apply (rule_tac Q="\_. globals_equiv s" in hoare_strengthen_post) apply (wp mapM_wp' | wpc)+ diff --git a/proof/infoflow/Noninterference.thy b/proof/infoflow/Noninterference.thy index 681fa56e8a..713db462fe 100644 --- a/proof/infoflow/Noninterference.thy +++ b/proof/infoflow/Noninterference.thy @@ -381,8 +381,7 @@ lemma kernel_entry_if_globals_equiv_scheduler: and (\s. ct_idle s \ tc = idle_context s)\ kernel_entry_if e tc \\_. globals_equiv_scheduler st\" - apply (wp globals_equiv_scheduler_inv' kernel_entry_if_globals_equiv) - apply (clarsimp) + apply (wpsimp wp: globals_equiv_scheduler_inv' kernel_entry_if_globals_equiv) apply assumption apply clarsimp done @@ -2090,10 +2089,10 @@ lemma tcb_sched_action_reads_respects_g': apply (force intro: domtcbs simp: get_etcb_def) apply (simp add: equiv_valid_def2 ethread_get_def) apply (rule equiv_valid_rv_bind) - apply (wp equiv_valid_rv_trivial', simp) + apply (wpsimp wp: equiv_valid_rv_trivial') apply (rule equiv_valid_2_bind) prefer 2 - apply (wp equiv_valid_rv_trivial, simp) + apply (wpsimp wp: equiv_valid_rv_trivial) apply (rule equiv_valid_2_bind) apply (rule_tac P="\" and P'="\" and L="{pasObjectAbs aag thread}" and L'="{pasObjectAbs aag thread}" in ev2_invisible') diff --git a/proof/infoflow/RISCV64/ArchArch_IF.thy b/proof/infoflow/RISCV64/ArchArch_IF.thy index 46de768008..5ab976337d 100644 --- a/proof/infoflow/RISCV64/ArchArch_IF.thy +++ b/proof/infoflow/RISCV64/ArchArch_IF.thy @@ -464,7 +464,7 @@ lemma copy_global_mappings_valid_arch_state: and (\s. x \ global_refs s \ is_aligned x pt_bits)\ copy_global_mappings x \\_. valid_arch_state\" - unfolding copy_global_mappings_def including no_pre + unfolding copy_global_mappings_def including classic_wp_pre apply simp apply wp apply (rule_tac Q="\_. valid_arch_state and valid_global_vspace_mappings and pspace_aligned diff --git a/proof/infoflow/RISCV64/ArchRetype_IF.thy b/proof/infoflow/RISCV64/ArchRetype_IF.thy index 326f9a25a2..749c1de80d 100644 --- a/proof/infoflow/RISCV64/ArchRetype_IF.thy +++ b/proof/infoflow/RISCV64/ArchRetype_IF.thy @@ -232,7 +232,7 @@ lemma copy_global_mappings_globals_equiv: "\globals_equiv s and (\s. x \ riscv_global_pt (arch_state s) \ is_aligned x pt_bits)\ copy_global_mappings x \\_. globals_equiv s\" - unfolding copy_global_mappings_def including no_pre + unfolding copy_global_mappings_def including classic_wp_pre apply simp apply wp apply (rule_tac Q="\_. globals_equiv s and (\s. x \ riscv_global_pt (arch_state s) \ diff --git a/proof/infoflow/RISCV64/ArchScheduler_IF.thy b/proof/infoflow/RISCV64/ArchScheduler_IF.thy index 28df9083df..8f19866dec 100644 --- a/proof/infoflow/RISCV64/ArchScheduler_IF.thy +++ b/proof/infoflow/RISCV64/ArchScheduler_IF.thy @@ -184,8 +184,7 @@ lemma arch_switch_to_thread_globals_equiv_scheduler[Scheduler_IF_assms]: arch_switch_to_thread thread \\_. globals_equiv_scheduler sta\" unfolding arch_switch_to_thread_def storeWord_def - by (wpsimp wp: dmo_wp modify_wp thread_get_wp' - | wp (once) globals_equiv_scheduler_inv'[where P="\"])+ + by (wpsimp wp: dmo_wp modify_wp thread_get_wp' globals_equiv_scheduler_inv'[where P="\"]) crunches arch_activate_idle_thread for silc_dom_equiv[Scheduler_IF_assms, wp]: "silc_dom_equiv aag st" diff --git a/proof/infoflow/Scheduler_IF.thy b/proof/infoflow/Scheduler_IF.thy index de3d3aeaa4..38cfe61b94 100644 --- a/proof/infoflow/Scheduler_IF.thy +++ b/proof/infoflow/Scheduler_IF.thy @@ -2397,7 +2397,9 @@ lemma context_update_cur_thread_snippit_cur_domain: (\s. reads_scheduler_cur_domain aag l s \ invs s \ silc_inv aag st s \ (ct_idle s \ uc = idle_context s) \ guarded_pas_domain aag s) (gets cur_thread >>= thread_set (tcb_arch_update (arch_tcb_context_set uc)))" - apply wp + \ \FIXME: maybe should make an equiv_valid_pre?\ + apply (rule equiv_valid_guard_imp) + apply wp apply (clarsimp simp: cur_thread_idle silc_inv_not_cur_thread del: notI) done diff --git a/proof/infoflow/Syscall_IF.thy b/proof/infoflow/Syscall_IF.thy index eb4de64723..fa67061a5c 100644 --- a/proof/infoflow/Syscall_IF.thy +++ b/proof/infoflow/Syscall_IF.thy @@ -187,8 +187,8 @@ proof (induct rule: cap_revoke.induct[where ?a1.0=s]) apply (frule aag_can_read_self) apply (simp add: equiv_for_def split del: if_split)+ apply (wp drop_spec_ev2_inv[OF liftE_ev2] gets_evrv | simp)+ - apply (wp drop_spec_ev2_inv[OF liftE_ev2] gets_evrv - reads_respects_f[OF get_cap_rev, where st=st and Q=\,simplified equiv_valid_def2]) + apply (wpsimp wp: drop_spec_ev2_inv[OF liftE_ev2] gets_evrv + reads_respects_f[OF get_cap_rev, where st=st and Q=\,simplified equiv_valid_def2]) apply clarsimp+ apply (frule all_children_subjectReads[simplified comp_def]) apply clarsimp diff --git a/proof/infoflow/Tcb_IF.thy b/proof/infoflow/Tcb_IF.thy index 7fb3dc8dba..7ea3fbef57 100644 --- a/proof/infoflow/Tcb_IF.thy +++ b/proof/infoflow/Tcb_IF.thy @@ -140,8 +140,7 @@ next apply (rule split_spec_bindE) apply (rule split_spec_bindE[rotated]) apply (rule "4.hyps", assumption+) - apply (wp set_cap_P set_cap_Q get_cap_wp | simp) - apply simp + apply (wpsimp wp: set_cap_P set_cap_Q get_cap_wp) apply simp apply wp apply (clarsimp simp add: zombie_is_cap_toE) @@ -203,11 +202,10 @@ lemma rec_del_globals_equiv: "\\s. invs s \ globals_equiv st s \ emptyable (slot_rdcall call) s \ valid_rec_del_call call s\ rec_del call \\_. globals_equiv st\" - apply (wp finalise_cap_globals_equiv - rec_del_preservation2[where Q="valid_arch_state" - and R="\cap s. invs s \ valid_cap cap s - \ (\p. cap = ThreadCap p \ p \ idle_thread s)"]) - apply simp + apply (wpsimp wp: finalise_cap_globals_equiv + rec_del_preservation2[where Q="valid_arch_state" + and R="\cap s. invs s \ valid_cap cap s + \ (\p. cap = ThreadCap p \ p \ idle_thread s)"]) apply (wp set_cap_globals_equiv'') apply simp apply (wp empty_slot_globals_equiv)+ @@ -308,10 +306,9 @@ lemma invoke_tcb_globals_equiv: apply (rule_tac Q="\_. valid_arch_state and globals_equiv st and (\s. word1 \ idle_thread s) and (\s. word2 \ idle_thread s)" in hoare_strengthen_post) - apply ((wp mapM_x_wp' as_user_globals_equiv invoke_tcb_NotificationControl_globals_equiv - | simp - | intro conjI impI - | clarsimp simp: no_cap_to_idle_thread)+)[6] + apply (wpsimp wp: mapM_x_wp' as_user_globals_equiv invoke_tcb_NotificationControl_globals_equiv + weak_if_wp')+ + apply (intro conjI impI; clarsimp simp: no_cap_to_idle_thread)+ apply (simp del: invoke_tcb.simps tcb_inv_wf.simps) apply (wp invoke_tcb_thread_preservation cap_delete_globals_equiv cap_insert_globals_equiv'' thread_set_globals_equiv set_mcpriority_globals_equiv @@ -494,7 +491,7 @@ lemma invoke_tcb_reads_respects_f: and tcb_inv_wf ti and is_subject aag \ cur_thread and K (authorised_tcb_inv aag ti \ authorised_tcb_inv_extra aag ti)) (invoke_tcb ti)" - including no_pre + including classic_wp_pre apply (case_tac ti) \ \WriteRegisters\ apply (strengthen invs_mdb diff --git a/proof/invariant-abstract/ARM/ArchVSpaceEntries_AI.thy b/proof/invariant-abstract/ARM/ArchVSpaceEntries_AI.thy index 6ec2baf64a..6e27ba6a85 100644 --- a/proof/invariant-abstract/ARM/ArchVSpaceEntries_AI.thy +++ b/proof/invariant-abstract/ARM/ArchVSpaceEntries_AI.thy @@ -455,11 +455,10 @@ lemma mapM_x_copy_pde_updates: done lemma copy_global_mappings_valid_pdpt_objs[wp]: - notes hoare_pre [wp_pre del] - shows "\valid_pdpt_objs and valid_arch_state and pspace_aligned and K (is_aligned p pd_bits)\ copy_global_mappings p \\rv. valid_pdpt_objs\" + including classic_wp_pre apply (rule hoare_gen_asm) apply (simp add: copy_global_mappings_def) apply wp diff --git a/proof/invariant-abstract/ARM_HYP/ArchVSpaceEntries_AI.thy b/proof/invariant-abstract/ARM_HYP/ArchVSpaceEntries_AI.thy index 28812e081c..b5636854d2 100644 --- a/proof/invariant-abstract/ARM_HYP/ArchVSpaceEntries_AI.thy +++ b/proof/invariant-abstract/ARM_HYP/ArchVSpaceEntries_AI.thy @@ -439,7 +439,7 @@ lemma mapM_x_copy_pde_updates: ucast (f x && mask pd_bits >> 3)) ` set xs then pd y else pd' y)))) \))\ mapM_x (\x. get_pde (p + f x) >>= store_pde (p' + f x)) xs \\_. Q\" - including no_pre + including classic_wp_pre apply (induct xs) apply (simp add: mapM_x_Nil) apply wp diff --git a/proof/invariant-abstract/DetSchedAux_AI.thy b/proof/invariant-abstract/DetSchedAux_AI.thy index 10ab5dba4c..0f143df8f8 100644 --- a/proof/invariant-abstract/DetSchedAux_AI.thy +++ b/proof/invariant-abstract/DetSchedAux_AI.thy @@ -313,15 +313,12 @@ lemma invoke_untyped_valid_sched: "\invs and valid_untyped_inv ui and ct_active and valid_sched and valid_idle \ invoke_untyped ui \ \_ . valid_sched \" - including no_pre apply (rule hoare_pre) apply (rule_tac I="invs and valid_untyped_inv ui and ct_active" - in valid_sched_tcb_state_preservation) - apply (wp invoke_untyped_st_tcb_at) - apply simp - apply (wp invoke_untyped_etcb_at)+ - apply (rule hoare_post_impErr, rule hoare_pre, rule invoke_untyp_invs, - simp_all add: invs_valid_idle)[1] + in valid_sched_tcb_state_preservation) + apply (wpsimp wp: invoke_untyped_st_tcb_at invoke_untyped_etcb_at)+ + apply (rule hoare_post_impErr, rule invoke_untyp_invs; simp add: invs_valid_idle) + apply simp apply (rule_tac f="\s. P (scheduler_action s)" in hoare_lift_Pf) apply (rule_tac f="\s. x (ready_queues s)" in hoare_lift_Pf) apply wp+ diff --git a/proof/invariant-abstract/DetSchedSchedule_AI.thy b/proof/invariant-abstract/DetSchedSchedule_AI.thy index 77e8c7e7a4..39c628e750 100644 --- a/proof/invariant-abstract/DetSchedSchedule_AI.thy +++ b/proof/invariant-abstract/DetSchedSchedule_AI.thy @@ -917,23 +917,19 @@ lemma as_user_valid_sched[wp]: st_tcb_def2 valid_blocked_def) done -lemma switch_to_thread_ct_not_queued[wp]: - "\valid_queues\ switch_to_thread t \\rv s. not_queued (cur_thread s) s\" - apply (simp add: switch_to_thread_def) - including no_pre - apply wp - prefer 4 - apply (rule get_wp) - prefer 3 - apply (rule assert_inv) - prefer 2 - apply (rule arch_switch_to_thread_valid_queues') - apply (simp add: tcb_sched_action_def - tcb_sched_dequeue_def | wp)+ +lemma tcb_sched_action_dequeue_not_queued[wp]: + "\valid_queues\ tcb_sched_action tcb_sched_dequeue t \\_. not_queued t\" + unfolding tcb_sched_action_def tcb_sched_dequeue_def + apply wpsimp apply (clarsimp simp add: valid_queues_def etcb_at_def not_queued_def split: option.splits) done +lemma switch_to_thread_ct_not_queued[wp]: + "\valid_queues\ switch_to_thread t \\rv s. not_queued (cur_thread s) s\" + unfolding switch_to_thread_def + by wpsimp + end lemma ct_not_in_q_def2: @@ -2728,9 +2724,10 @@ lemma handle_double_fault_valid_sched: \\rv. valid_sched\" apply (simp add: valid_sched_def) including no_pre - apply (wp handle_double_fault_valid_queues handle_double_fault_valid_sched_action - set_thread_state_not_runnable_valid_blocked - | rule hoare_conjI | simp add: handle_double_fault_def | fastforce simp: simple_sched_action_def)+ + apply (wpsimp wp: handle_double_fault_valid_queues handle_double_fault_valid_sched_action + set_thread_state_not_runnable_valid_blocked + comb: hoare_vcg_precond_imp + | rule hoare_conjI | simp add: handle_double_fault_def | fastforce simp: simple_sched_action_def)+ done lemma send_fault_ipc_error_sched_act_not[wp]: @@ -2812,47 +2809,48 @@ lemma receive_ipc_valid_sched: \\rv. valid_sched\" supply option.case_cong_weak[cong] apply (simp add: receive_ipc_def) - including no_pre apply (wp | wpc | simp)+ - apply (wp set_thread_state_sched_act_not_valid_sched | wpc)+ - apply ((wp set_thread_state_sched_act_not_valid_sched - setup_caller_cap_sched_act_not_valid_sched - | simp add: do_nbrecv_failed_transfer_def)+)[2] - apply ((wp possible_switch_to_valid_sched_except sts_st_tcb_at' hoare_drop_imps - set_thread_state_runnable_valid_queues - set_thread_state_runnable_valid_sched_action - set_thread_state_valid_blocked_except | simp | wpc)+)[3] - apply (rule_tac Q="\_. valid_sched and scheduler_act_not (sender) and not_queued (sender) and not_cur_thread (sender) and (\s. sender \ idle_thread s)" in hoare_strengthen_post) - apply wp - apply (simp add: valid_sched_def) - apply ((wp | wpc)+)[1] - apply (simp | wp gts_wp hoare_vcg_all_lift)+ - apply (wp hoare_vcg_imp_lift) - apply ((simp add: set_simple_ko_def set_object_def | - wp hoare_drop_imps | wpc)+)[1] - apply (wp hoare_vcg_imp_lift get_object_wp - set_thread_state_sched_act_not_valid_sched gbn_wp - | simp add: get_simple_ko_def do_nbrecv_failed_transfer_def a_type_def - split: kernel_object.splits - | wpc - | wp (once) hoare_vcg_all_lift hoare_vcg_ex_lift)+ + apply (wp set_thread_state_sched_act_not_valid_sched | wpc)+ + apply ((wp set_thread_state_sched_act_not_valid_sched + setup_caller_cap_sched_act_not_valid_sched + | simp add: do_nbrecv_failed_transfer_def)+)[2] + apply ((wp possible_switch_to_valid_sched_except sts_st_tcb_at' hoare_drop_imps + set_thread_state_runnable_valid_queues + set_thread_state_runnable_valid_sched_action + set_thread_state_valid_blocked_except | simp | wpc)+)[3] + apply (rule_tac Q="\_. valid_sched and scheduler_act_not (sender) and not_queued (sender) + and not_cur_thread (sender) and (\s. sender \ idle_thread s)" + in hoare_strengthen_post) + apply wp + apply (simp add: valid_sched_def) + apply ((wp | wpc)+)[1] + apply (simp | wp gts_wp hoare_vcg_all_lift)+ + apply (wp hoare_vcg_imp_lift) + apply ((simp add: set_simple_ko_def set_object_def + | wp hoare_drop_imps | wpc)+)[1] + apply (wp hoare_vcg_imp_lift get_object_wp + set_thread_state_sched_act_not_valid_sched gbn_wp + | simp add: get_simple_ko_def do_nbrecv_failed_transfer_def a_type_def + split: kernel_object.splits + | wpc + | wp (once) hoare_vcg_all_lift hoare_vcg_ex_lift)+ apply (subst st_tcb_at_kh_simp[symmetric])+ apply (clarsimp simp: st_tcb_at_kh_if_split default_notification_def default_ntfn_def isActive_def) - apply (rename_tac xh xi xj) + apply (rename_tac ref b R ntfn xh xi xj) apply (drule_tac t="hd xh" and P'="\ts. \ active ts" in st_tcb_weakenE) apply clarsimp apply (simp only: st_tcb_at_not) apply (subgoal_tac "hd xh \ idle_thread s") apply (fastforce simp: valid_sched_def valid_sched_action_def weak_valid_sched_action_def valid_queues_def st_tcb_at_not ct_in_state_def not_cur_thread_def runnable_eq_active not_queued_def scheduler_act_not_def split: scheduler_action.splits) -(* clag from send_signal_valid_sched *) + (* clag from send_signal_valid_sched *) apply clarsimp apply (frule invs_valid_idle) - apply (drule_tac ptr=xc in idle_not_queued) + apply (drule_tac ptr=ref in idle_not_queued) apply (clarsimp simp: invs_sym_refs) apply (simp add: state_refs_of_def obj_at_def) apply (frule invs_valid_objs) apply (simp add: valid_objs_def obj_at_def) - apply (drule_tac x = xc in bspec) + apply (drule_tac x = ref in bspec) apply (simp add: dom_def) apply (clarsimp simp: valid_obj_def valid_ntfn_def) apply (drule hd_in_set) diff --git a/proof/invariant-abstract/Syscall_AI.thy b/proof/invariant-abstract/Syscall_AI.thy index aa77e2d0ad..4c66515e52 100644 --- a/proof/invariant-abstract/Syscall_AI.thy +++ b/proof/invariant-abstract/Syscall_AI.thy @@ -1146,7 +1146,7 @@ lemma hy_inv: "(\s f. P (trans_state f s) = P s) \ \ st_tcb_at simple (cur_thread s) s" diff --git a/proof/refine/AARCH64/Finalise_R.thy b/proof/refine/AARCH64/Finalise_R.thy index 13e1f06eac..7c6b922749 100644 --- a/proof/refine/AARCH64/Finalise_R.thy +++ b/proof/refine/AARCH64/Finalise_R.thy @@ -3393,7 +3393,7 @@ lemma cancelAllIPC_mapM_x_valid_objs': tcbSchedEnqueue t od) q \\_. valid_objs'\" - apply (wp mapM_x_wp' sts_valid_objs') + apply (wpsimp wp: mapM_x_wp' sts_valid_objs') apply (clarsimp simp: valid_tcb_state'_def)+ done diff --git a/proof/refine/AARCH64/IpcCancel_R.thy b/proof/refine/AARCH64/IpcCancel_R.thy index 64225e6774..b9330594ed 100644 --- a/proof/refine/AARCH64/IpcCancel_R.thy +++ b/proof/refine/AARCH64/IpcCancel_R.thy @@ -1106,7 +1106,7 @@ lemma sts_weak_sch_act_wf[wp]: \ (ksSchedulerAction s = SwitchToThread t \ runnable' st)\ setThreadState st t \\_ s. weak_sch_act_wf (ksSchedulerAction s) s\" - including no_pre + including classic_wp_pre apply (simp add: setThreadState_def) apply (wp rescheduleRequired_weak_sch_act_wf) apply (rule_tac Q="\_ s. weak_sch_act_wf (ksSchedulerAction s) s" in hoare_post_imp, simp) @@ -1595,7 +1595,7 @@ lemma rescheduleRequired_oa_queued: apply (simp add: rescheduleRequired_def sch_act_simple_def) apply (rule_tac B="\rv s. (rv = ResumeCurrentThread \ rv = ChooseNewThread) \ ?OAQ t' p s" in hoare_seq_ext) - including no_pre + including classic_wp_pre apply (wp | clarsimp)+ apply (case_tac x) apply (wp | clarsimp)+ @@ -1671,7 +1671,7 @@ lemma sts_valid_queues_partial: pred_tcb_at'_def obj_at'_def inQ_def) apply (rule hoare_vcg_all_lift)+ apply (rule hoare_convert_imp) - including no_pre + including classic_wp_pre apply (wp sts_ksQ setThreadState_oa_queued hoare_impI sts_pred_tcb_neq' | clarsimp)+ apply (rule_tac Q="\s. \d p. ?DISTINCT d p s \ sch_act_simple s" in hoare_pre_imp) diff --git a/proof/refine/AARCH64/Ipc_R.thy b/proof/refine/AARCH64/Ipc_R.thy index 5562eda982..b79babae31 100644 --- a/proof/refine/AARCH64/Ipc_R.thy +++ b/proof/refine/AARCH64/Ipc_R.thy @@ -714,8 +714,7 @@ lemma transferCapsToSlots_mdb[wp]: \ transferCaps_srcs caps s\ transferCapsToSlots ep buffer n caps slots mi \\rv. valid_mdb'\" - apply (wp transferCapsToSlots_presM[where drv=True and vo=True and emx=True and pad=True]) - apply clarsimp + apply (wpsimp wp: transferCapsToSlots_presM[where drv=True and vo=True and emx=True and pad=True]) apply (frule valid_capAligned) apply (clarsimp simp: cte_wp_at_ctes_of is_derived'_def badge_derived'_def) apply wp @@ -864,7 +863,7 @@ lemma transferCapsToSlots_irq_handlers[wp]: and transferCaps_srcs caps\ transferCapsToSlots ep buffer n caps slots mi \\rv. valid_irq_handlers'\" - apply (wp transferCapsToSlots_presM[where vo=True and emx=False and drv=True and pad=False]) + apply (wpsimp wp: transferCapsToSlots_presM[where vo=True and emx=False and drv=True and pad=False]) apply (clarsimp simp: is_derived'_def cte_wp_at_ctes_of badge_derived'_def) apply (erule(2) valid_irq_handlers_ctes_ofD) apply wp @@ -961,8 +960,8 @@ lemma tcts_zero_ranges[wp]: \ transferCaps_srcs caps s\ transferCapsToSlots ep buffer n caps slots mi \\rv. untyped_ranges_zero'\" - apply (wp transferCapsToSlots_presM[where emx=True and vo=True - and drv=True and pad=True]) + apply (wpsimp wp: transferCapsToSlots_presM[where emx=True and vo=True + and drv=True and pad=True]) apply (clarsimp simp: cte_wp_at_ctes_of) apply (simp add: cteCaps_of_def) apply (rule hoare_pre, wp untyped_ranges_zero_lift) @@ -1182,7 +1181,7 @@ lemmas copyMRs_typ_at_lifts[wp] = typ_at_lifts [OF copyMRs_typ_at'] lemma copy_mrs_invs'[wp]: "\ invs' and tcb_at' s and tcb_at' r \ copyMRs s sb r rb n \\rv. invs' \" - including no_pre + including classic_wp_pre apply (simp add: copyMRs_def) apply (wp dmo_invs' no_irq_mapM no_irq_storeWord| simp add: split_def) diff --git a/proof/refine/AARCH64/Retype_R.thy b/proof/refine/AARCH64/Retype_R.thy index 93b645cb94..a0e7b99a12 100644 --- a/proof/refine/AARCH64/Retype_R.thy +++ b/proof/refine/AARCH64/Retype_R.thy @@ -3431,11 +3431,11 @@ lemma createObjects_orig_cte_wp_at2': \ (case_option False (P' \ getF) (projectKO_opt val))) \ pspace_no_overlap' ptr sz s\ createObjects' ptr n val gbits \\r s. P (cte_wp_at' P' p s)\" + including classic_wp_pre apply (simp add: cte_wp_at'_obj_at') apply (rule handy_prop_divs) apply (wp createObjects_orig_obj_at2'[where sz = sz], simp) apply (simp add: tcb_cte_cases_def cteSizeBits_def) - including no_pre apply (wp handy_prop_divs createObjects_orig_obj_at2'[where sz = sz] | simp add: o_def cong: option.case_cong)+ done @@ -3456,7 +3456,7 @@ lemma createNewCaps_cte_wp_at2: \ pspace_no_overlap' ptr sz s\ createNewCaps ty ptr n objsz dev \\rv s. P (cte_wp_at' P' p s)\" - including no_pre + including classic_wp_pre apply (simp add: createNewCaps_def createObjects_def AARCH64_H.toAPIType_def split del: if_split) apply (case_tac ty; simp add: createNewCaps_def createObjects_def Arch_createNewCaps_def @@ -4143,7 +4143,7 @@ lemma createNewCaps_idle'[wp]: apply (rename_tac apiobject_type) apply (case_tac apiobject_type, simp_all split del: if_split)[1] apply (wp, simp) - including no_pre + including classic_wp_pre apply (wp mapM_x_wp' createObjects_idle' threadSet_idle' @@ -4263,8 +4263,7 @@ lemma createNewCaps_valid_queues: createNewCaps ty ptr n us d \\rv. valid_queues\" apply (rule hoare_gen_asm) - apply (wp valid_queues_lift_asm createNewCaps_obj_at2[where sz=sz]) - apply (clarsimp simp: projectKO_opts_defs) + apply (wpsimp wp: valid_queues_lift_asm createNewCaps_obj_at2[where sz=sz]) apply (simp add: inQ_def) apply (wp createNewCaps_pred_tcb_at'[where sz=sz] | simp)+ done @@ -4719,8 +4718,8 @@ lemma createObjects_queues: pspace_no_overlap' ptr sz s \ range_cover ptr sz (objBitsKO val + gbits) n \ n \ 0\ createObjects ptr n val gbits \\rv. valid_queues\" - apply (wp valid_queues_lift_asm [unfolded pred_conj_def, OF createObjects_orig_obj_at3] - createObjects_pred_tcb_at' [unfolded pred_conj_def]) + apply (wpsimp wp: valid_queues_lift_asm [unfolded pred_conj_def, OF createObjects_orig_obj_at3] + createObjects_pred_tcb_at' [unfolded pred_conj_def]) apply fastforce apply wp+ apply fastforce diff --git a/proof/refine/AARCH64/Schedule_R.thy b/proof/refine/AARCH64/Schedule_R.thy index bcba0710e2..b8e0b34b28 100644 --- a/proof/refine/AARCH64/Schedule_R.thy +++ b/proof/refine/AARCH64/Schedule_R.thy @@ -1224,8 +1224,7 @@ lemma dmo_cap_to'[wp]: lemma sct_cap_to'[wp]: "\ex_nonz_cap_to' p\ setCurThread t \\rv. ex_nonz_cap_to' p\" apply (simp add: setCurThread_def) - apply (wp ex_nonz_cap_to_pres') - apply (clarsimp elim!: cte_wp_at'_pspaceI)+ + apply (wpsimp wp: ex_nonz_cap_to_pres') done lemma setVCPU_cap_to'[wp]: @@ -2252,7 +2251,7 @@ proof - apply (rename_tac l1) apply (case_tac "l1 = 0") (* switch to idle thread *) - apply (simp, wp (once) switchToIdleThread_invs_no_cicd', simp) + apply (simp, wp switchToIdleThread_invs_no_cicd', simp) (* we have a thread to switch to *) apply (clarsimp simp: bitmap_fun_defs) apply (wp assert_inv) diff --git a/proof/refine/AARCH64/TcbAcc_R.thy b/proof/refine/AARCH64/TcbAcc_R.thy index b9de7dfbe8..d151843ac8 100644 --- a/proof/refine/AARCH64/TcbAcc_R.thy +++ b/proof/refine/AARCH64/TcbAcc_R.thy @@ -2386,7 +2386,7 @@ lemma threadSet_queued_sch_act_wf[wp]: "\\s. sch_act_wf (ksSchedulerAction s) s\ threadSet (tcbQueued_update f) t \\_ s. sch_act_wf (ksSchedulerAction s) s\" - including no_pre + including classic_wp_pre apply (simp add: sch_act_wf_cases split: scheduler_action.split) apply (wp hoare_vcg_conj_lift) @@ -2907,7 +2907,7 @@ lemma rescheduleRequired_valid_bitmapQ_sch_act_simple: "\ valid_bitmapQ and sch_act_simple\ rescheduleRequired \\_. valid_bitmapQ \" - including no_pre + including classic_wp_pre apply (simp add: rescheduleRequired_def sch_act_simple_def) apply (rule_tac B="\rv s. valid_bitmapQ s \ (rv = ResumeCurrentThread \ rv = ChooseNewThread)" in hoare_seq_ext) @@ -2920,7 +2920,7 @@ lemma rescheduleRequired_bitmapQ_no_L1_orphans_sch_act_simple: "\ bitmapQ_no_L1_orphans and sch_act_simple\ rescheduleRequired \\_. bitmapQ_no_L1_orphans \" - including no_pre + including classic_wp_pre apply (simp add: rescheduleRequired_def sch_act_simple_def) apply (rule_tac B="\rv s. bitmapQ_no_L1_orphans s \ (rv = ResumeCurrentThread \ rv = ChooseNewThread)" in hoare_seq_ext) @@ -2933,7 +2933,7 @@ lemma rescheduleRequired_bitmapQ_no_L2_orphans_sch_act_simple: "\ bitmapQ_no_L2_orphans and sch_act_simple\ rescheduleRequired \\_. bitmapQ_no_L2_orphans \" - including no_pre + including classic_wp_pre apply (simp add: rescheduleRequired_def sch_act_simple_def) apply (rule_tac B="\rv s. bitmapQ_no_L2_orphans s \ (rv = ResumeCurrentThread \ rv = ChooseNewThread)" in hoare_seq_ext) diff --git a/proof/refine/AARCH64/Tcb_R.thy b/proof/refine/AARCH64/Tcb_R.thy index 0c2df3888a..9c25603b95 100644 --- a/proof/refine/AARCH64/Tcb_R.thy +++ b/proof/refine/AARCH64/Tcb_R.thy @@ -1565,7 +1565,7 @@ proof - emptyable_def | wpc | strengthen tcb_cap_always_valid_strg use_no_cap_to_obj_asid_strg - | wp (once) add: sch_act_simple_lift hoare_drop_imps del: cteInsert_invs + | wp add: sch_act_simple_lift hoare_drop_imps del: cteInsert_invs | (erule exE, clarsimp simp: word_bits_def))+ apply (clarsimp simp: tcb_at_cte_at_0 tcb_at_cte_at_1[simplified] tcb_at_st_tcb_at[symmetric] tcb_cap_valid_def is_cnode_or_valid_arch_def invs_valid_objs emptyable_def @@ -2700,7 +2700,7 @@ crunches getThreadBufferSlot, setPriority, setMCPriority lemma inv_tcb_IRQInactive: "\valid_irq_states'\ invokeTCB tcb_inv -, \\rv s. intStateIRQTable (ksInterruptState s) rv \ irqstate.IRQInactive\" - including no_pre + including classic_wp_pre apply (simp add: invokeTCB_def) apply (rule hoare_pre) apply (wpc | diff --git a/proof/refine/AARCH64/orphanage/Orphanage.thy b/proof/refine/AARCH64/orphanage/Orphanage.thy index 2d929cd90a..7e56a739c6 100644 --- a/proof/refine/AARCH64/orphanage/Orphanage.thy +++ b/proof/refine/AARCH64/orphanage/Orphanage.thy @@ -789,7 +789,7 @@ lemma chooseThread_no_orphans [wp]: apply (rename_tac l1) apply (case_tac "l1 = 0") (* switch to idle thread *) - apply (simp, wp (once), simp) + apply (simp, wp, simp) (* we have a thread to switch to *) apply (clarsimp simp: bitmap_fun_defs) apply (wp assert_inv ThreadDecls_H_switchToThread_no_orphans) @@ -1814,7 +1814,7 @@ lemma cancelBadgedSends_no_orphans [wp]: \ \rv s. no_orphans s \" unfolding cancelBadgedSends_def by (wpsimp wp: filterM_preserved tcbSchedEnqueue_almost_no_orphans gts_wp' sts_st_tcb' - hoare_drop_imps) + | wp (once) hoare_drop_imps)+ crunch no_orphans [wp]: handleFaultReply "no_orphans" diff --git a/proof/refine/ARM/Finalise_R.thy b/proof/refine/ARM/Finalise_R.thy index 58eb7048a8..1ccfbae968 100644 --- a/proof/refine/ARM/Finalise_R.thy +++ b/proof/refine/ARM/Finalise_R.thy @@ -2992,7 +2992,7 @@ lemma cancelAllIPC_mapM_x_valid_objs': tcbSchedEnqueue t od) q \\_. valid_objs'\" - apply (wp mapM_x_wp' sts_valid_objs') + apply (wpsimp wp: mapM_x_wp' sts_valid_objs') apply (clarsimp simp: valid_tcb_state'_def)+ done diff --git a/proof/refine/ARM/IpcCancel_R.thy b/proof/refine/ARM/IpcCancel_R.thy index b031a5bb31..aaf563b9a8 100644 --- a/proof/refine/ARM/IpcCancel_R.thy +++ b/proof/refine/ARM/IpcCancel_R.thy @@ -1164,7 +1164,7 @@ lemma sts_weak_sch_act_wf[wp]: \ (ksSchedulerAction s = SwitchToThread t \ runnable' st)\ setThreadState st t \\_ s. weak_sch_act_wf (ksSchedulerAction s) s\" - including no_pre + including classic_wp_pre apply (simp add: setThreadState_def) apply (wp rescheduleRequired_weak_sch_act_wf) apply (rule_tac Q="\_ s. weak_sch_act_wf (ksSchedulerAction s) s" in hoare_post_imp, simp) @@ -1483,7 +1483,7 @@ lemma rescheduleRequired_oa_queued: apply (simp add: rescheduleRequired_def sch_act_simple_def) apply (rule_tac B="\rv s. (rv = ResumeCurrentThread \ rv = ChooseNewThread) \ ?OAQ t' p s" in hoare_seq_ext) - including no_pre + including classic_wp_pre apply (wp | clarsimp)+ apply (case_tac x) apply (wp | clarsimp)+ @@ -1546,7 +1546,7 @@ lemma sts_valid_queues_partial: pred_tcb_at'_def obj_at'_def inQ_def) apply (rule hoare_vcg_all_lift)+ apply (rule hoare_convert_imp) - including no_pre + including classic_wp_pre apply (wp sts_ksQ setThreadState_oa_queued hoare_impI sts_pred_tcb_neq' | clarsimp)+ apply (rule_tac Q="\s. \d p. ?DISTINCT d p s \ sch_act_simple s" in hoare_pre_imp) diff --git a/proof/refine/ARM/Ipc_R.thy b/proof/refine/ARM/Ipc_R.thy index bbbdfc219c..e6a261e3d3 100644 --- a/proof/refine/ARM/Ipc_R.thy +++ b/proof/refine/ARM/Ipc_R.thy @@ -706,8 +706,7 @@ lemma transferCapsToSlots_mdb[wp]: \ transferCaps_srcs caps s\ transferCapsToSlots ep buffer n caps slots mi \\rv. valid_mdb'\" - apply (wp transferCapsToSlots_presM[where drv=True and vo=True and emx=True and pad=True]) - apply clarsimp + apply (wpsimp wp: transferCapsToSlots_presM[where drv=True and vo=True and emx=True and pad=True]) apply (frule valid_capAligned) apply (clarsimp simp: cte_wp_at_ctes_of is_derived'_def badge_derived'_def) apply wp @@ -852,7 +851,7 @@ lemma transferCapsToSlots_irq_handlers[wp]: and transferCaps_srcs caps\ transferCapsToSlots ep buffer n caps slots mi \\rv. valid_irq_handlers'\" - apply (wp transferCapsToSlots_presM[where vo=True and emx=False and drv=True and pad=False]) + apply (wpsimp wp: transferCapsToSlots_presM[where vo=True and emx=False and drv=True and pad=False]) apply (clarsimp simp: is_derived'_def cte_wp_at_ctes_of badge_derived'_def) apply (erule(2) valid_irq_handlers_ctes_ofD) apply wp @@ -955,8 +954,8 @@ lemma tcts_zero_ranges[wp]: \ transferCaps_srcs caps s\ transferCapsToSlots ep buffer n caps slots mi \\rv. untyped_ranges_zero'\" - apply (wp transferCapsToSlots_presM[where emx=True and vo=True - and drv=True and pad=True]) + apply (wpsimp wp: transferCapsToSlots_presM[where emx=True and vo=True + and drv=True and pad=True]) apply (clarsimp simp: cte_wp_at_ctes_of) apply (simp add: cteCaps_of_def) apply (rule hoare_pre, wp untyped_ranges_zero_lift) @@ -1138,7 +1137,7 @@ lemmas copyMRs_typ_at_lifts[wp] = typ_at_lifts [OF copyMRs_typ_at'] lemma copy_mrs_invs'[wp]: "\ invs' and tcb_at' s and tcb_at' r \ copyMRs s sb r rb n \\rv. invs' \" - including no_pre + including classic_wp_pre apply (simp add: copyMRs_def) apply (wp dmo_invs' no_irq_mapM no_irq_storeWord| simp add: split_def) @@ -2945,7 +2944,7 @@ lemma sai_invs'[wp]: "\invs' and ex_nonz_cap_to' ntfnptr\ sendSignal ntfnptr badge \\y. invs'\" unfolding sendSignal_def - including no_pre + including classic_wp_pre apply (rule hoare_seq_ext[OF _ get_ntfn_sp']) apply (case_tac "ntfnObj nTFN", simp_all) prefer 3 diff --git a/proof/refine/ARM/Retype_R.thy b/proof/refine/ARM/Retype_R.thy index 8888942ed0..c77ec89d27 100644 --- a/proof/refine/ARM/Retype_R.thy +++ b/proof/refine/ARM/Retype_R.thy @@ -3438,7 +3438,7 @@ lemma createObjects_orig_cte_wp_at2': apply (rule handy_prop_divs) apply (wp createObjects_orig_obj_at2'[where sz = sz], simp) apply (simp add: tcb_cte_cases_def) - including no_pre + including classic_wp_pre apply (wp handy_prop_divs createObjects_orig_obj_at2'[where sz = sz] | simp add: o_def cong: option.case_cong)+ done @@ -3459,7 +3459,7 @@ lemma createNewCaps_cte_wp_at2: \ pspace_no_overlap' ptr sz s\ createNewCaps ty ptr n objsz dev \\rv s. P (cte_wp_at' P' p s)\" - including no_pre + including classic_wp_pre apply (simp add: createNewCaps_def createObjects_def ARM_H.toAPIType_def split del: if_split) apply (case_tac ty; simp add: createNewCaps_def createObjects_def Arch_createNewCaps_def @@ -4111,7 +4111,7 @@ lemma createNewCaps_idle'[wp]: apply (rename_tac apiobject_type) apply (case_tac apiobject_type, simp_all split del: if_split)[1] apply (wp, simp) - including no_pre + including classic_wp_pre apply (wp mapM_x_wp' createObjects_idle' threadSet_idle' @@ -4353,12 +4353,12 @@ lemma createNewCaps_valid_queues: and K (range_cover ptr sz (APIType_capBits ty us) n \ n \ 0)\ createNewCaps ty ptr n us d \\rv. valid_queues\" -apply (rule hoare_gen_asm) -apply (wp valid_queues_lift_asm createNewCaps_obj_at2[where sz=sz]) -apply (clarsimp simp: projectKO_opts_defs) -apply (simp add: inQ_def) -apply (wp createNewCaps_pred_tcb_at'[where sz=sz] | simp)+ -done + apply (rule hoare_gen_asm) + apply (wpsimp wp: valid_queues_lift_asm createNewCaps_obj_at2[where sz=sz]) + apply (clarsimp simp: projectKO_opts_defs) + apply (simp add: inQ_def) + apply (wpsimp wp: createNewCaps_pred_tcb_at'[where sz=sz])+ + done lemma mapM_x_threadSet_valid_pspace: "\valid_pspace' and K (curdom \ maxDomain)\ @@ -4814,8 +4814,8 @@ lemma createObjects_queues: pspace_no_overlap' ptr sz s \ range_cover ptr sz (objBitsKO val + gbits) n \ n \ 0\ createObjects ptr n val gbits \\rv. valid_queues\" - apply (wp valid_queues_lift_asm [unfolded pred_conj_def, OF createObjects_orig_obj_at3] - createObjects_pred_tcb_at' [unfolded pred_conj_def]) + apply (wpsimp wp: valid_queues_lift_asm [unfolded pred_conj_def, OF createObjects_orig_obj_at3] + createObjects_pred_tcb_at' [unfolded pred_conj_def]) apply fastforce apply wp+ apply fastforce diff --git a/proof/refine/ARM/Schedule_R.thy b/proof/refine/ARM/Schedule_R.thy index 8b3d92fa3e..f9d9b29e2e 100644 --- a/proof/refine/ARM/Schedule_R.thy +++ b/proof/refine/ARM/Schedule_R.thy @@ -1101,8 +1101,7 @@ lemma dmo_cap_to'[wp]: lemma sct_cap_to'[wp]: "\ex_nonz_cap_to' p\ setCurThread t \\rv. ex_nonz_cap_to' p\" apply (simp add: setCurThread_def) - apply (wp ex_nonz_cap_to_pres') - apply (clarsimp elim!: cte_wp_at'_pspaceI)+ + apply (wpsimp wp: ex_nonz_cap_to_pres') done @@ -2107,7 +2106,7 @@ proof - apply (rename_tac l1) apply (case_tac "l1 = 0") (* switch to idle thread *) - apply (simp, wp (once) switchToIdleThread_invs_no_cicd', simp) + apply (simp, wp switchToIdleThread_invs_no_cicd', simp) (* we have a thread to switch to *) apply (clarsimp simp: bitmap_fun_defs) apply (wp assert_inv) diff --git a/proof/refine/ARM/TcbAcc_R.thy b/proof/refine/ARM/TcbAcc_R.thy index f040d40a8e..eaa2abc417 100644 --- a/proof/refine/ARM/TcbAcc_R.thy +++ b/proof/refine/ARM/TcbAcc_R.thy @@ -2311,7 +2311,7 @@ lemma threadSet_queued_sch_act_wf[wp]: "\\s. sch_act_wf (ksSchedulerAction s) s\ threadSet (tcbQueued_update f) t \\_ s. sch_act_wf (ksSchedulerAction s) s\" - including no_pre + including classic_wp_pre apply (simp add: sch_act_wf_cases split: scheduler_action.split) apply (wp hoare_vcg_conj_lift) @@ -2827,7 +2827,7 @@ lemma rescheduleRequired_valid_bitmapQ_sch_act_simple: "\ valid_bitmapQ and sch_act_simple\ rescheduleRequired \\_. valid_bitmapQ \" - including no_pre + including classic_wp_pre apply (simp add: rescheduleRequired_def sch_act_simple_def) apply (rule_tac B="\rv s. valid_bitmapQ s \ (rv = ResumeCurrentThread \ rv = ChooseNewThread)" in hoare_seq_ext) @@ -2840,7 +2840,7 @@ lemma rescheduleRequired_bitmapQ_no_L1_orphans_sch_act_simple: "\ bitmapQ_no_L1_orphans and sch_act_simple\ rescheduleRequired \\_. bitmapQ_no_L1_orphans \" - including no_pre + including classic_wp_pre apply (simp add: rescheduleRequired_def sch_act_simple_def) apply (rule_tac B="\rv s. bitmapQ_no_L1_orphans s \ (rv = ResumeCurrentThread \ rv = ChooseNewThread)" in hoare_seq_ext) @@ -2853,7 +2853,7 @@ lemma rescheduleRequired_bitmapQ_no_L2_orphans_sch_act_simple: "\ bitmapQ_no_L2_orphans and sch_act_simple\ rescheduleRequired \\_. bitmapQ_no_L2_orphans \" - including no_pre + including classic_wp_pre apply (simp add: rescheduleRequired_def sch_act_simple_def) apply (rule_tac B="\rv s. bitmapQ_no_L2_orphans s \ (rv = ResumeCurrentThread \ rv = ChooseNewThread)" in hoare_seq_ext) diff --git a/proof/refine/ARM/Tcb_R.thy b/proof/refine/ARM/Tcb_R.thy index 07f0317cbc..bbe4e0ad88 100644 --- a/proof/refine/ARM/Tcb_R.thy +++ b/proof/refine/ARM/Tcb_R.thy @@ -1644,7 +1644,7 @@ proof - emptyable_def | wpc | strengthen tcb_cap_always_valid_strg use_no_cap_to_obj_asid_strg - | wp (once) add: sch_act_simple_lift hoare_drop_imps del: cteInsert_invs + | wp add: sch_act_simple_lift hoare_drop_imps del: cteInsert_invs | (erule exE, clarsimp simp: word_bits_def))+ (* the last two subgoals *) apply (clarsimp simp: tcb_at_cte_at_0 tcb_at_cte_at_1[simplified] tcb_at_st_tcb_at[symmetric] @@ -2750,7 +2750,7 @@ crunches getThreadBufferSlot, setPriority, setMCPriority lemma inv_tcb_IRQInactive: "\valid_irq_states'\ invokeTCB tcb_inv -, \\rv s. intStateIRQTable (ksInterruptState s) rv \ irqstate.IRQInactive\" - including no_pre + including classic_wp_pre apply (simp add: invokeTCB_def) apply (rule hoare_pre) apply (wpc | diff --git a/proof/refine/ARM/VSpace_R.thy b/proof/refine/ARM/VSpace_R.thy index 87707612c3..a89cef829b 100644 --- a/proof/refine/ARM/VSpace_R.thy +++ b/proof/refine/ARM/VSpace_R.thy @@ -881,13 +881,9 @@ lemma deleteASID_corres: apply (simp add: vs_refs_def) apply (rule image_eqI[rotated], erule graph_ofI) apply (simp add: mask_asid_low_bits_ucast_ucast) - apply wp - apply (simp add: o_def) - apply (wp getASID_wp) - apply clarsimp - apply assumption - apply wp+ - apply clarsimp + \ \rewrite assumption so that the goal can refer to the C variable instead of the abstract's.\ + apply (drule Some_to_the) + apply (wpsimp wp: getASID_wp)+ apply (clarsimp simp: valid_arch_state_def valid_asid_table_def dest!: invs_arch_state) apply blast diff --git a/proof/refine/ARM/orphanage/Orphanage.thy b/proof/refine/ARM/orphanage/Orphanage.thy index 797ce7e350..5ca2f8ef52 100644 --- a/proof/refine/ARM/orphanage/Orphanage.thy +++ b/proof/refine/ARM/orphanage/Orphanage.thy @@ -804,7 +804,7 @@ lemma chooseThread_no_orphans [wp]: apply (rename_tac l1) apply (case_tac "l1 = 0") (* switch to idle thread *) - apply (simp, wp (once), simp) + apply (simp, wp, simp) (* we have a thread to switch to *) apply (clarsimp simp: bitmap_fun_defs) apply (wp assert_inv ThreadDecls_H_switchToThread_no_orphans) @@ -1883,10 +1883,8 @@ lemma cancelBadgedSends_no_orphans [wp]: cancelBadgedSends epptr badge \ \rv s. no_orphans s \" unfolding cancelBadgedSends_def - apply (rule hoare_pre) - apply (wp hoare_drop_imps | wpc | clarsimp)+ - apply (wp filterM_preserved tcbSchedEnqueue_almost_no_orphans gts_wp' - sts_st_tcb' hoare_drop_imps | clarsimp)+ + apply (wpsimp wp: filterM_preserved tcbSchedEnqueue_almost_no_orphans gts_wp' sts_st_tcb' + | wp (once) hoare_drop_imps)+ done crunch no_orphans [wp]: invalidateTLBByASID "no_orphans" diff --git a/proof/refine/ARM_HYP/Finalise_R.thy b/proof/refine/ARM_HYP/Finalise_R.thy index 51064db0a5..877efd9b00 100644 --- a/proof/refine/ARM_HYP/Finalise_R.thy +++ b/proof/refine/ARM_HYP/Finalise_R.thy @@ -2745,7 +2745,7 @@ lemma arch_finaliseCap_removeable[wp]: Arch.finaliseCap cap final \\rv s. isNullCap (fst rv) \ removeable' slot s (ArchObjectCap cap) \ isNullCap (snd rv)\" unfolding ARM_HYP_H.finaliseCap_def - including no_pre + including classic_wp_pre apply (case_tac cap; clarsimp) apply ((wpsimp simp: removeable'_def isCap_simps | rule conjI)+)[5] @@ -3419,7 +3419,7 @@ lemma cancelAllIPC_mapM_x_valid_objs': tcbSchedEnqueue t od) q \\_. valid_objs'\" - apply (wp mapM_x_wp' sts_valid_objs') + apply (wpsimp wp: mapM_x_wp' sts_valid_objs') apply (clarsimp simp: valid_tcb_state'_def)+ done diff --git a/proof/refine/ARM_HYP/IpcCancel_R.thy b/proof/refine/ARM_HYP/IpcCancel_R.thy index b1defefcea..cdd9069ccc 100644 --- a/proof/refine/ARM_HYP/IpcCancel_R.thy +++ b/proof/refine/ARM_HYP/IpcCancel_R.thy @@ -1173,7 +1173,7 @@ lemma sts_weak_sch_act_wf[wp]: \ (ksSchedulerAction s = SwitchToThread t \ runnable' st)\ setThreadState st t \\_ s. weak_sch_act_wf (ksSchedulerAction s) s\" - including no_pre + including classic_wp_pre apply (simp add: setThreadState_def) apply (wp rescheduleRequired_weak_sch_act_wf) apply (rule_tac Q="\_ s. weak_sch_act_wf (ksSchedulerAction s) s" in hoare_post_imp, simp) @@ -1637,7 +1637,7 @@ lemma rescheduleRequired_oa_queued: apply (simp add: rescheduleRequired_def sch_act_simple_def) apply (rule_tac B="\rv s. (rv = ResumeCurrentThread \ rv = ChooseNewThread) \ ?OAQ t' p s" in hoare_seq_ext) - including no_pre + including classic_wp_pre apply (wp | clarsimp)+ apply (case_tac x) apply (wp | clarsimp)+ @@ -1713,7 +1713,7 @@ lemma sts_valid_queues_partial: pred_tcb_at'_def obj_at'_def inQ_def) apply (rule hoare_vcg_all_lift)+ apply (rule hoare_convert_imp) - including no_pre + including classic_wp_pre apply (wp sts_ksQ setThreadState_oa_queued hoare_impI sts_pred_tcb_neq' | clarsimp)+ apply (rule_tac Q="\s. \d p. ?DISTINCT d p s \ sch_act_simple s" in hoare_pre_imp) diff --git a/proof/refine/ARM_HYP/Ipc_R.thy b/proof/refine/ARM_HYP/Ipc_R.thy index 48c77e4072..52cdaa3108 100644 --- a/proof/refine/ARM_HYP/Ipc_R.thy +++ b/proof/refine/ARM_HYP/Ipc_R.thy @@ -717,8 +717,7 @@ lemma transferCapsToSlots_mdb[wp]: \ transferCaps_srcs caps s\ transferCapsToSlots ep buffer n caps slots mi \\rv. valid_mdb'\" - apply (wp transferCapsToSlots_presM[where drv=True and vo=True and emx=True and pad=True]) - apply clarsimp + apply (wpsimp wp: transferCapsToSlots_presM[where drv=True and vo=True and emx=True and pad=True]) apply (frule valid_capAligned) apply (clarsimp simp: cte_wp_at_ctes_of is_derived'_def badge_derived'_def) apply wp @@ -871,7 +870,7 @@ lemma transferCapsToSlots_irq_handlers[wp]: and transferCaps_srcs caps\ transferCapsToSlots ep buffer n caps slots mi \\rv. valid_irq_handlers'\" - apply (wp transferCapsToSlots_presM[where vo=True and emx=False and drv=True and pad=False]) + apply (wpsimp wp: transferCapsToSlots_presM[where vo=True and emx=False and drv=True and pad=False]) apply (clarsimp simp: is_derived'_def cte_wp_at_ctes_of badge_derived'_def) apply (erule(2) valid_irq_handlers_ctes_ofD) apply wp @@ -974,8 +973,8 @@ lemma tcts_zero_ranges[wp]: \ transferCaps_srcs caps s\ transferCapsToSlots ep buffer n caps slots mi \\rv. untyped_ranges_zero'\" - apply (wp transferCapsToSlots_presM[where emx=True and vo=True - and drv=True and pad=True]) + apply (wpsimp wp: transferCapsToSlots_presM[where emx=True and vo=True + and drv=True and pad=True]) apply (clarsimp simp: cte_wp_at_ctes_of) apply (simp add: cteCaps_of_def) apply (rule hoare_pre, wp untyped_ranges_zero_lift) @@ -1194,7 +1193,7 @@ lemmas copyMRs_typ_at_lifts[wp] = typ_at_lifts [OF copyMRs_typ_at'] lemma copy_mrs_invs'[wp]: "\ invs' and tcb_at' s and tcb_at' r \ copyMRs s sb r rb n \\rv. invs' \" - including no_pre + including classic_wp_pre apply (simp add: copyMRs_def) apply (wp dmo_invs' no_irq_mapM no_irq_storeWord| simp add: split_def) diff --git a/proof/refine/ARM_HYP/Retype_R.thy b/proof/refine/ARM_HYP/Retype_R.thy index 7be836f8b7..c29f7ab34c 100644 --- a/proof/refine/ARM_HYP/Retype_R.thy +++ b/proof/refine/ARM_HYP/Retype_R.thy @@ -3425,7 +3425,7 @@ lemma createObjects_orig_cte_wp_at2': apply (rule handy_prop_divs) apply (wp createObjects_orig_obj_at2'[where sz = sz], simp) apply (simp add: tcb_cte_cases_def) - including no_pre + including classic_wp_pre apply (wp handy_prop_divs createObjects_orig_obj_at2'[where sz = sz] | simp add: o_def cong: option.case_cong)+ done @@ -3446,7 +3446,7 @@ lemma createNewCaps_cte_wp_at2: \ pspace_no_overlap' ptr sz s\ createNewCaps ty ptr n objsz dev \\rv s. P (cte_wp_at' P' p s)\" - including no_pre + including classic_wp_pre apply (simp add: createNewCaps_def createObjects_def ARM_HYP_H.toAPIType_def split del: if_split) apply (case_tac ty; simp add: createNewCaps_def createObjects_def Arch_createNewCaps_def @@ -4182,7 +4182,7 @@ lemma createNewCaps_idle'[wp]: apply (rename_tac apiobject_type) apply (case_tac apiobject_type, simp_all split del: if_split)[1] apply (wp, simp) - including no_pre + including classic_wp_pre apply (wp mapM_x_wp' createObjects_idle' threadSet_idle' @@ -4378,12 +4378,12 @@ lemma createNewCaps_valid_queues: and K (range_cover ptr sz (APIType_capBits ty us) n \ n \ 0)\ createNewCaps ty ptr n us d \\rv. valid_queues\" -apply (rule hoare_gen_asm) -apply (wp valid_queues_lift_asm createNewCaps_obj_at2[where sz=sz]) -apply (clarsimp simp: projectKO_opts_defs) -apply (simp add: inQ_def) -apply (wp createNewCaps_pred_tcb_at'[where sz=sz] | simp)+ -done + apply (rule hoare_gen_asm) + apply (wpsimp wp: valid_queues_lift_asm createNewCaps_obj_at2[where sz=sz]) + apply (clarsimp simp: projectKO_opts_defs) + apply (simp add: inQ_def) + apply (wpsimp wp: createNewCaps_pred_tcb_at'[where sz=sz])+ + done lemma mapM_x_threadSet_valid_pspace: "\valid_pspace' and K (curdom \ maxDomain)\ @@ -4865,8 +4865,8 @@ lemma createObjects_queues: pspace_no_overlap' ptr sz s \ range_cover ptr sz (objBitsKO val + gbits) n \ n \ 0\ createObjects ptr n val gbits \\rv. valid_queues\" - apply (wp valid_queues_lift_asm [unfolded pred_conj_def, OF createObjects_orig_obj_at3] - createObjects_pred_tcb_at' [unfolded pred_conj_def]) + apply (wpsimp wp: valid_queues_lift_asm [unfolded pred_conj_def, OF createObjects_orig_obj_at3] + createObjects_pred_tcb_at' [unfolded pred_conj_def]) apply fastforce apply wp+ apply fastforce diff --git a/proof/refine/ARM_HYP/Schedule_R.thy b/proof/refine/ARM_HYP/Schedule_R.thy index b4edbdf7f4..709d465cbd 100644 --- a/proof/refine/ARM_HYP/Schedule_R.thy +++ b/proof/refine/ARM_HYP/Schedule_R.thy @@ -1189,8 +1189,7 @@ lemma dmo_cap_to'[wp]: lemma sct_cap_to'[wp]: "\ex_nonz_cap_to' p\ setCurThread t \\rv. ex_nonz_cap_to' p\" apply (simp add: setCurThread_def) - apply (wp ex_nonz_cap_to_pres') - apply (clarsimp elim!: cte_wp_at'_pspaceI)+ + apply (wpsimp wp: ex_nonz_cap_to_pres') done lemma setVCPU_cap_to'[wp]: @@ -2233,7 +2232,7 @@ proof - apply (rename_tac l1) apply (case_tac "l1 = 0") (* switch to idle thread *) - apply (simp, wp (once) switchToIdleThread_invs_no_cicd', simp) + apply (simp, wp switchToIdleThread_invs_no_cicd', simp) (* we have a thread to switch to *) apply (clarsimp simp: bitmap_fun_defs) apply (wp assert_inv) diff --git a/proof/refine/ARM_HYP/TcbAcc_R.thy b/proof/refine/ARM_HYP/TcbAcc_R.thy index cecb49920c..80957947dc 100644 --- a/proof/refine/ARM_HYP/TcbAcc_R.thy +++ b/proof/refine/ARM_HYP/TcbAcc_R.thy @@ -2390,7 +2390,7 @@ lemma threadSet_queued_sch_act_wf[wp]: "\\s. sch_act_wf (ksSchedulerAction s) s\ threadSet (tcbQueued_update f) t \\_ s. sch_act_wf (ksSchedulerAction s) s\" - including no_pre + including classic_wp_pre apply (simp add: sch_act_wf_cases split: scheduler_action.split) apply (wp hoare_vcg_conj_lift) @@ -2911,7 +2911,7 @@ lemma rescheduleRequired_valid_bitmapQ_sch_act_simple: "\ valid_bitmapQ and sch_act_simple\ rescheduleRequired \\_. valid_bitmapQ \" - including no_pre + including classic_wp_pre apply (simp add: rescheduleRequired_def sch_act_simple_def) apply (rule_tac B="\rv s. valid_bitmapQ s \ (rv = ResumeCurrentThread \ rv = ChooseNewThread)" in hoare_seq_ext) @@ -2924,7 +2924,7 @@ lemma rescheduleRequired_bitmapQ_no_L1_orphans_sch_act_simple: "\ bitmapQ_no_L1_orphans and sch_act_simple\ rescheduleRequired \\_. bitmapQ_no_L1_orphans \" - including no_pre + including classic_wp_pre apply (simp add: rescheduleRequired_def sch_act_simple_def) apply (rule_tac B="\rv s. bitmapQ_no_L1_orphans s \ (rv = ResumeCurrentThread \ rv = ChooseNewThread)" in hoare_seq_ext) @@ -2937,7 +2937,7 @@ lemma rescheduleRequired_bitmapQ_no_L2_orphans_sch_act_simple: "\ bitmapQ_no_L2_orphans and sch_act_simple\ rescheduleRequired \\_. bitmapQ_no_L2_orphans \" - including no_pre + including classic_wp_pre apply (simp add: rescheduleRequired_def sch_act_simple_def) apply (rule_tac B="\rv s. bitmapQ_no_L2_orphans s \ (rv = ResumeCurrentThread \ rv = ChooseNewThread)" in hoare_seq_ext) diff --git a/proof/refine/ARM_HYP/Tcb_R.thy b/proof/refine/ARM_HYP/Tcb_R.thy index 92fb4a22f0..5d0255421d 100644 --- a/proof/refine/ARM_HYP/Tcb_R.thy +++ b/proof/refine/ARM_HYP/Tcb_R.thy @@ -1619,7 +1619,7 @@ proof - emptyable_def | wpc | strengthen tcb_cap_always_valid_strg use_no_cap_to_obj_asid_strg - | wp (once) add: sch_act_simple_lift hoare_drop_imps del: cteInsert_invs + | wp add: sch_act_simple_lift hoare_drop_imps del: cteInsert_invs | (erule exE, clarsimp simp: word_bits_def))+ (* the last two subgoals *) apply (clarsimp simp: tcb_at_cte_at_0 tcb_at_cte_at_1[simplified] tcb_at_st_tcb_at[symmetric] @@ -2779,7 +2779,7 @@ crunches getThreadBufferSlot, setPriority, setMCPriority lemma inv_tcb_IRQInactive: "\valid_irq_states'\ invokeTCB tcb_inv -, \\rv s. intStateIRQTable (ksInterruptState s) rv \ irqstate.IRQInactive\" - including no_pre + including classic_wp_pre apply (simp add: invokeTCB_def) apply (rule hoare_pre) apply (wpc | diff --git a/proof/refine/ARM_HYP/VSpace_R.thy b/proof/refine/ARM_HYP/VSpace_R.thy index bc4dff1fd1..b067dc1d6f 100644 --- a/proof/refine/ARM_HYP/VSpace_R.thy +++ b/proof/refine/ARM_HYP/VSpace_R.thy @@ -1424,13 +1424,9 @@ lemma deleteASID_corres: apply (simp add: vs_refs_def) apply (rule image_eqI[rotated], erule graph_ofI) apply (simp add: mask_asid_low_bits_ucast_ucast) - apply wp - apply (simp add: o_def) - apply (wp getASID_wp) - apply clarsimp - apply assumption - apply wp+ - apply clarsimp + \ \rewrite assumption so that the goal can refer to the C variable instead of the abstract's.\ + apply (drule Some_to_the) + apply (wpsimp wp: getASID_wp)+ apply (clarsimp simp: valid_arch_state_def valid_asid_table_def dest!: invs_arch_state) apply blast diff --git a/proof/refine/RISCV64/Finalise_R.thy b/proof/refine/RISCV64/Finalise_R.thy index 2c2b684e63..f658b4d758 100644 --- a/proof/refine/RISCV64/Finalise_R.thy +++ b/proof/refine/RISCV64/Finalise_R.thy @@ -3017,7 +3017,7 @@ lemma cancelAllIPC_mapM_x_valid_objs': tcbSchedEnqueue t od) q \\_. valid_objs'\" - apply (wp mapM_x_wp' sts_valid_objs') + apply (wpsimp wp: mapM_x_wp' sts_valid_objs') apply (clarsimp simp: valid_tcb_state'_def)+ done diff --git a/proof/refine/RISCV64/IpcCancel_R.thy b/proof/refine/RISCV64/IpcCancel_R.thy index 3edc0bb35d..4bc46d5ded 100644 --- a/proof/refine/RISCV64/IpcCancel_R.thy +++ b/proof/refine/RISCV64/IpcCancel_R.thy @@ -1110,7 +1110,7 @@ lemma sts_weak_sch_act_wf[wp]: \ (ksSchedulerAction s = SwitchToThread t \ runnable' st)\ setThreadState st t \\_ s. weak_sch_act_wf (ksSchedulerAction s) s\" - including no_pre + including classic_wp_pre apply (simp add: setThreadState_def) apply (wp rescheduleRequired_weak_sch_act_wf) apply (rule_tac Q="\_ s. weak_sch_act_wf (ksSchedulerAction s) s" in hoare_post_imp, simp) @@ -1447,7 +1447,7 @@ lemma rescheduleRequired_oa_queued: apply (simp add: rescheduleRequired_def sch_act_simple_def) apply (rule_tac B="\rv s. (rv = ResumeCurrentThread \ rv = ChooseNewThread) \ ?OAQ t' p s" in hoare_seq_ext) - including no_pre + including classic_wp_pre apply (wp | clarsimp)+ apply (case_tac x) apply (wp | clarsimp)+ @@ -1523,7 +1523,7 @@ lemma sts_valid_queues_partial: pred_tcb_at'_def obj_at'_def inQ_def) apply (rule hoare_vcg_all_lift)+ apply (rule hoare_convert_imp) - including no_pre + including classic_wp_pre apply (wp sts_ksQ setThreadState_oa_queued hoare_impI sts_pred_tcb_neq' | clarsimp)+ apply (rule_tac Q="\s. \d p. ?DISTINCT d p s \ sch_act_simple s" in hoare_pre_imp) diff --git a/proof/refine/RISCV64/Ipc_R.thy b/proof/refine/RISCV64/Ipc_R.thy index cdfa3f7423..b9aaacf25f 100644 --- a/proof/refine/RISCV64/Ipc_R.thy +++ b/proof/refine/RISCV64/Ipc_R.thy @@ -713,8 +713,7 @@ lemma transferCapsToSlots_mdb[wp]: \ transferCaps_srcs caps s\ transferCapsToSlots ep buffer n caps slots mi \\rv. valid_mdb'\" - apply (wp transferCapsToSlots_presM[where drv=True and vo=True and emx=True and pad=True]) - apply clarsimp + apply (wpsimp wp: transferCapsToSlots_presM[where drv=True and vo=True and emx=True and pad=True]) apply (frule valid_capAligned) apply (clarsimp simp: cte_wp_at_ctes_of is_derived'_def badge_derived'_def) apply wp @@ -861,7 +860,7 @@ lemma transferCapsToSlots_irq_handlers[wp]: and transferCaps_srcs caps\ transferCapsToSlots ep buffer n caps slots mi \\rv. valid_irq_handlers'\" - apply (wp transferCapsToSlots_presM[where vo=True and emx=False and drv=True and pad=False]) + apply (wpsimp wp: transferCapsToSlots_presM[where vo=True and emx=False and drv=True and pad=False]) apply (clarsimp simp: is_derived'_def cte_wp_at_ctes_of badge_derived'_def) apply (erule(2) valid_irq_handlers_ctes_ofD) apply wp @@ -958,8 +957,8 @@ lemma tcts_zero_ranges[wp]: \ transferCaps_srcs caps s\ transferCapsToSlots ep buffer n caps slots mi \\rv. untyped_ranges_zero'\" - apply (wp transferCapsToSlots_presM[where emx=True and vo=True - and drv=True and pad=True]) + apply (wpsimp wp: transferCapsToSlots_presM[where emx=True and vo=True + and drv=True and pad=True]) apply (clarsimp simp: cte_wp_at_ctes_of) apply (simp add: cteCaps_of_def) apply (rule hoare_pre, wp untyped_ranges_zero_lift) @@ -1179,7 +1178,7 @@ lemmas copyMRs_typ_at_lifts[wp] = typ_at_lifts [OF copyMRs_typ_at'] lemma copy_mrs_invs'[wp]: "\ invs' and tcb_at' s and tcb_at' r \ copyMRs s sb r rb n \\rv. invs' \" - including no_pre + including classic_wp_pre apply (simp add: copyMRs_def) apply (wp dmo_invs' no_irq_mapM no_irq_storeWord| simp add: split_def) diff --git a/proof/refine/RISCV64/Retype_R.thy b/proof/refine/RISCV64/Retype_R.thy index cd55719ec1..8ac1ba2fc3 100644 --- a/proof/refine/RISCV64/Retype_R.thy +++ b/proof/refine/RISCV64/Retype_R.thy @@ -3373,11 +3373,11 @@ lemma createObjects_orig_cte_wp_at2': \ (case_option False (P' \ getF) (projectKO_opt val))) \ pspace_no_overlap' ptr sz s\ createObjects' ptr n val gbits \\r s. P (cte_wp_at' P' p s)\" + including classic_wp_pre apply (simp add: cte_wp_at'_obj_at') apply (rule handy_prop_divs) apply (wp createObjects_orig_obj_at2'[where sz = sz], simp) apply (simp add: tcb_cte_cases_def cteSizeBits_def) - including no_pre apply (wp handy_prop_divs createObjects_orig_obj_at2'[where sz = sz] | simp add: o_def cong: option.case_cong)+ done @@ -3398,7 +3398,7 @@ lemma createNewCaps_cte_wp_at2: \ pspace_no_overlap' ptr sz s\ createNewCaps ty ptr n objsz dev \\rv s. P (cte_wp_at' P' p s)\" - including no_pre + including classic_wp_pre apply (simp add: createNewCaps_def createObjects_def RISCV64_H.toAPIType_def split del: if_split) apply (case_tac ty; simp add: createNewCaps_def createObjects_def Arch_createNewCaps_def @@ -4055,7 +4055,7 @@ lemma createNewCaps_idle'[wp]: apply (rename_tac apiobject_type) apply (case_tac apiobject_type, simp_all split del: if_split)[1] apply (wp, simp) - including no_pre + including classic_wp_pre apply (wp mapM_x_wp' createObjects_idle' threadSet_idle' @@ -4191,8 +4191,7 @@ lemma createNewCaps_valid_queues: createNewCaps ty ptr n us d \\rv. valid_queues\" apply (rule hoare_gen_asm) - apply (wp valid_queues_lift_asm createNewCaps_obj_at2[where sz=sz]) - apply (clarsimp simp: projectKO_opts_defs) + apply (wpsimp wp: valid_queues_lift_asm createNewCaps_obj_at2[where sz=sz]) apply (simp add: inQ_def) apply (wp createNewCaps_pred_tcb_at'[where sz=sz] | simp)+ done @@ -4661,8 +4660,8 @@ lemma createObjects_queues: pspace_no_overlap' ptr sz s \ range_cover ptr sz (objBitsKO val + gbits) n \ n \ 0\ createObjects ptr n val gbits \\rv. valid_queues\" - apply (wp valid_queues_lift_asm [unfolded pred_conj_def, OF createObjects_orig_obj_at3] - createObjects_pred_tcb_at' [unfolded pred_conj_def]) + apply (wpsimp wp: valid_queues_lift_asm [unfolded pred_conj_def, OF createObjects_orig_obj_at3] + createObjects_pred_tcb_at' [unfolded pred_conj_def]) apply fastforce apply wp+ apply fastforce diff --git a/proof/refine/RISCV64/Schedule_R.thy b/proof/refine/RISCV64/Schedule_R.thy index 2637f53166..4b28bcfbaf 100644 --- a/proof/refine/RISCV64/Schedule_R.thy +++ b/proof/refine/RISCV64/Schedule_R.thy @@ -1079,8 +1079,7 @@ lemma dmo_cap_to'[wp]: lemma sct_cap_to'[wp]: "\ex_nonz_cap_to' p\ setCurThread t \\rv. ex_nonz_cap_to' p\" apply (simp add: setCurThread_def) - apply (wp ex_nonz_cap_to_pres') - apply (clarsimp elim!: cte_wp_at'_pspaceI)+ + apply (wpsimp wp: ex_nonz_cap_to_pres') done @@ -2095,7 +2094,7 @@ proof - apply (rename_tac l1) apply (case_tac "l1 = 0") (* switch to idle thread *) - apply (simp, wp (once) switchToIdleThread_invs_no_cicd', simp) + apply (simp, wp switchToIdleThread_invs_no_cicd', simp) (* we have a thread to switch to *) apply (clarsimp simp: bitmap_fun_defs) apply (wp assert_inv) diff --git a/proof/refine/RISCV64/TcbAcc_R.thy b/proof/refine/RISCV64/TcbAcc_R.thy index 2cee7bc860..c8aa05c7e3 100644 --- a/proof/refine/RISCV64/TcbAcc_R.thy +++ b/proof/refine/RISCV64/TcbAcc_R.thy @@ -2358,7 +2358,7 @@ lemma threadSet_queued_sch_act_wf[wp]: "\\s. sch_act_wf (ksSchedulerAction s) s\ threadSet (tcbQueued_update f) t \\_ s. sch_act_wf (ksSchedulerAction s) s\" - including no_pre + including classic_wp_pre apply (simp add: sch_act_wf_cases split: scheduler_action.split) apply (wp hoare_vcg_conj_lift) @@ -2879,7 +2879,7 @@ lemma rescheduleRequired_valid_bitmapQ_sch_act_simple: "\ valid_bitmapQ and sch_act_simple\ rescheduleRequired \\_. valid_bitmapQ \" - including no_pre + including classic_wp_pre apply (simp add: rescheduleRequired_def sch_act_simple_def) apply (rule_tac B="\rv s. valid_bitmapQ s \ (rv = ResumeCurrentThread \ rv = ChooseNewThread)" in hoare_seq_ext) @@ -2892,7 +2892,7 @@ lemma rescheduleRequired_bitmapQ_no_L1_orphans_sch_act_simple: "\ bitmapQ_no_L1_orphans and sch_act_simple\ rescheduleRequired \\_. bitmapQ_no_L1_orphans \" - including no_pre + including classic_wp_pre apply (simp add: rescheduleRequired_def sch_act_simple_def) apply (rule_tac B="\rv s. bitmapQ_no_L1_orphans s \ (rv = ResumeCurrentThread \ rv = ChooseNewThread)" in hoare_seq_ext) @@ -2905,7 +2905,7 @@ lemma rescheduleRequired_bitmapQ_no_L2_orphans_sch_act_simple: "\ bitmapQ_no_L2_orphans and sch_act_simple\ rescheduleRequired \\_. bitmapQ_no_L2_orphans \" - including no_pre + including classic_wp_pre apply (simp add: rescheduleRequired_def sch_act_simple_def) apply (rule_tac B="\rv s. bitmapQ_no_L2_orphans s \ (rv = ResumeCurrentThread \ rv = ChooseNewThread)" in hoare_seq_ext) diff --git a/proof/refine/RISCV64/Tcb_R.thy b/proof/refine/RISCV64/Tcb_R.thy index 4c9e2ac531..3854a619f4 100644 --- a/proof/refine/RISCV64/Tcb_R.thy +++ b/proof/refine/RISCV64/Tcb_R.thy @@ -1557,7 +1557,7 @@ proof - emptyable_def | wpc | strengthen tcb_cap_always_valid_strg use_no_cap_to_obj_asid_strg - | wp (once) add: sch_act_simple_lift hoare_drop_imps del: cteInsert_invs + | wp add: sch_act_simple_lift hoare_drop_imps del: cteInsert_invs | (erule exE, clarsimp simp: word_bits_def))+ apply (clarsimp simp: tcb_at_cte_at_0 tcb_at_cte_at_1[simplified] tcb_at_st_tcb_at[symmetric] tcb_cap_valid_def is_cnode_or_valid_arch_def invs_valid_objs emptyable_def @@ -2703,7 +2703,7 @@ crunches getThreadBufferSlot, setPriority, setMCPriority lemma inv_tcb_IRQInactive: "\valid_irq_states'\ invokeTCB tcb_inv -, \\rv s. intStateIRQTable (ksInterruptState s) rv \ irqstate.IRQInactive\" - including no_pre + including classic_wp_pre apply (simp add: invokeTCB_def) apply (rule hoare_pre) apply (wpc | diff --git a/proof/refine/RISCV64/orphanage/Orphanage.thy b/proof/refine/RISCV64/orphanage/Orphanage.thy index 68f807737b..5d7f35c110 100644 --- a/proof/refine/RISCV64/orphanage/Orphanage.thy +++ b/proof/refine/RISCV64/orphanage/Orphanage.thy @@ -792,7 +792,7 @@ lemma chooseThread_no_orphans [wp]: apply (rename_tac l1) apply (case_tac "l1 = 0") (* switch to idle thread *) - apply (simp, wp (once), simp) + apply (simp, wp, simp) (* we have a thread to switch to *) apply (clarsimp simp: bitmap_fun_defs) apply (wp assert_inv ThreadDecls_H_switchToThread_no_orphans) @@ -1855,10 +1855,8 @@ lemma cancelBadgedSends_no_orphans [wp]: cancelBadgedSends epptr badge \ \rv s. no_orphans s \" unfolding cancelBadgedSends_def - apply (rule hoare_pre) - apply (wp hoare_drop_imps | wpc | clarsimp)+ - apply (wp filterM_preserved tcbSchedEnqueue_almost_no_orphans gts_wp' - sts_st_tcb' hoare_drop_imps | clarsimp)+ + apply (wpsimp wp: filterM_preserved tcbSchedEnqueue_almost_no_orphans gts_wp' sts_st_tcb' + | wp (once) hoare_drop_imps)+ done crunch no_orphans [wp]: handleFaultReply "no_orphans" diff --git a/proof/refine/X64/Finalise_R.thy b/proof/refine/X64/Finalise_R.thy index 733a72db45..bcf40bbbe1 100644 --- a/proof/refine/X64/Finalise_R.thy +++ b/proof/refine/X64/Finalise_R.thy @@ -3189,7 +3189,7 @@ lemma cancelAllIPC_mapM_x_valid_objs': tcbSchedEnqueue t od) q \\_. valid_objs'\" - apply (wp mapM_x_wp' sts_valid_objs') + apply (wpsimp wp: mapM_x_wp' sts_valid_objs') apply (clarsimp simp: valid_tcb_state'_def)+ done diff --git a/proof/refine/X64/IpcCancel_R.thy b/proof/refine/X64/IpcCancel_R.thy index d18d63fc87..8894a18267 100644 --- a/proof/refine/X64/IpcCancel_R.thy +++ b/proof/refine/X64/IpcCancel_R.thy @@ -1157,7 +1157,7 @@ lemma sts_weak_sch_act_wf[wp]: \ (ksSchedulerAction s = SwitchToThread t \ runnable' st)\ setThreadState st t \\_ s. weak_sch_act_wf (ksSchedulerAction s) s\" - including no_pre + including classic_wp_pre apply (simp add: setThreadState_def) apply (wp rescheduleRequired_weak_sch_act_wf) apply (rule_tac Q="\_ s. weak_sch_act_wf (ksSchedulerAction s) s" in hoare_post_imp, simp) @@ -1513,7 +1513,7 @@ lemma rescheduleRequired_oa_queued: apply (simp add: rescheduleRequired_def sch_act_simple_def) apply (rule_tac B="\rv s. (rv = ResumeCurrentThread \ rv = ChooseNewThread) \ ?OAQ t' p s" in hoare_seq_ext) - including no_pre + including classic_wp_pre apply (wp | clarsimp)+ apply (case_tac x) apply (wp | clarsimp)+ @@ -1589,7 +1589,7 @@ lemma sts_valid_queues_partial: pred_tcb_at'_def obj_at'_def inQ_def) apply (rule hoare_vcg_all_lift)+ apply (rule hoare_convert_imp) - including no_pre + including classic_wp_pre apply (wp sts_ksQ setThreadState_oa_queued hoare_impI sts_pred_tcb_neq' | clarsimp)+ apply (rule_tac Q="\s. \d p. ?DISTINCT d p s \ sch_act_simple s" in hoare_pre_imp) diff --git a/proof/refine/X64/Ipc_R.thy b/proof/refine/X64/Ipc_R.thy index 4c31d2ec32..ff1801b7bf 100644 --- a/proof/refine/X64/Ipc_R.thy +++ b/proof/refine/X64/Ipc_R.thy @@ -713,8 +713,7 @@ lemma transferCapsToSlots_mdb[wp]: \ transferCaps_srcs caps s\ transferCapsToSlots ep buffer n caps slots mi \\rv. valid_mdb'\" - apply (wp transferCapsToSlots_presM[where drv=True and vo=True and emx=True and pad=True]) - apply clarsimp + apply (wpsimp wp: transferCapsToSlots_presM[where drv=True and vo=True and emx=True and pad=True]) apply (frule valid_capAligned) apply (clarsimp simp: cte_wp_at_ctes_of is_derived'_def badge_derived'_def) apply wp @@ -860,7 +859,7 @@ lemma transferCapsToSlots_irq_handlers[wp]: and transferCaps_srcs caps\ transferCapsToSlots ep buffer n caps slots mi \\rv. valid_irq_handlers'\" - apply (wp transferCapsToSlots_presM[where vo=True and emx=False and drv=True and pad=False]) + apply (wpsimp wp: transferCapsToSlots_presM[where vo=True and emx=False and drv=True and pad=False]) apply (clarsimp simp: is_derived'_def cte_wp_at_ctes_of badge_derived'_def) apply (erule(2) valid_irq_handlers_ctes_ofD) apply wp @@ -893,7 +892,7 @@ lemma transferCapsToSlots_ioports'[wp]: and transferCaps_srcs caps\ transferCapsToSlots ep buffer n caps slots mi \\rv. valid_ioports'\" - apply (wp transferCapsToSlots_presM[where vo=True and emx=False and drv=True and pad=False]) + apply (wpsimp wp: transferCapsToSlots_presM[where vo=True and emx=False and drv=True and pad=False]) apply (clarsimp simp: valid_ioports'_derivedD) apply wp apply (clarsimp simp:cte_wp_at_ctes_of | intro ballI conjI)+ @@ -989,8 +988,8 @@ lemma tcts_zero_ranges[wp]: \ transferCaps_srcs caps s\ transferCapsToSlots ep buffer n caps slots mi \\rv. untyped_ranges_zero'\" - apply (wp transferCapsToSlots_presM[where emx=True and vo=True - and drv=True and pad=True]) + apply (wpsimp wp: transferCapsToSlots_presM[where emx=True and vo=True + and drv=True and pad=True]) apply (clarsimp simp: cte_wp_at_ctes_of) apply (simp add: cteCaps_of_def) apply (rule hoare_pre, wp untyped_ranges_zero_lift) @@ -1228,7 +1227,7 @@ lemmas copyMRs_typ_at_lifts[wp] = typ_at_lifts [OF copyMRs_typ_at'] lemma copy_mrs_invs'[wp]: "\ invs' and tcb_at' s and tcb_at' r \ copyMRs s sb r rb n \\rv. invs' \" - including no_pre + including classic_wp_pre apply (simp add: copyMRs_def) apply (wp dmo_invs' no_irq_mapM no_irq_storeWord| simp add: split_def) diff --git a/proof/refine/X64/Retype_R.thy b/proof/refine/X64/Retype_R.thy index 83f9357b2e..b63669123a 100644 --- a/proof/refine/X64/Retype_R.thy +++ b/proof/refine/X64/Retype_R.thy @@ -3519,7 +3519,7 @@ lemma createObjects_orig_cte_wp_at2': apply (rule handy_prop_divs) apply (wp createObjects_orig_obj_at2'[where sz = sz], simp) apply (simp add: tcb_cte_cases_def) - including no_pre + including classic_wp_pre apply (wp handy_prop_divs createObjects_orig_obj_at2'[where sz = sz] | simp add: o_def cong: option.case_cong)+ done @@ -3540,7 +3540,7 @@ lemma createNewCaps_cte_wp_at2: \ pspace_no_overlap' ptr sz s\ createNewCaps ty ptr n objsz dev \\rv s. P (cte_wp_at' P' p s)\" - including no_pre + including classic_wp_pre apply (simp add: createNewCaps_def createObjects_def X64_H.toAPIType_def split del: if_split) apply (case_tac ty; simp add: createNewCaps_def createObjects_def Arch_createNewCaps_def @@ -4225,7 +4225,7 @@ lemma createNewCaps_idle'[wp]: apply (rename_tac apiobject_type) apply (case_tac apiobject_type, simp_all split del: if_split)[1] apply (wp, simp) - including no_pre + including classic_wp_pre apply (wp mapM_x_wp' createObjects_idle' threadSet_idle' @@ -4390,12 +4390,12 @@ lemma createNewCaps_valid_queues: and K (range_cover ptr sz (APIType_capBits ty us) n \ n \ 0)\ createNewCaps ty ptr n us d \\rv. valid_queues\" -apply (rule hoare_gen_asm) -apply (wp valid_queues_lift_asm createNewCaps_obj_at2[where sz=sz]) -apply (clarsimp simp: projectKO_opts_defs) -apply (simp add: inQ_def) -apply (wp createNewCaps_pred_tcb_at'[where sz=sz] | simp)+ -done + apply (rule hoare_gen_asm) + apply (wpsimp wp: valid_queues_lift_asm createNewCaps_obj_at2[where sz=sz]) + apply (clarsimp simp: projectKO_opts_defs) + apply (simp add: inQ_def) + apply (wpsimp wp: createNewCaps_pred_tcb_at'[where sz=sz])+ + done lemma mapM_x_threadSet_valid_pspace: "\valid_pspace' and K (curdom \ maxDomain)\ @@ -4866,8 +4866,8 @@ lemma createObjects_queues: pspace_no_overlap' ptr sz s \ range_cover ptr sz (objBitsKO val + gbits) n \ n \ 0\ createObjects ptr n val gbits \\rv. valid_queues\" - apply (wp valid_queues_lift_asm [unfolded pred_conj_def, OF createObjects_orig_obj_at3] - createObjects_pred_tcb_at' [unfolded pred_conj_def]) + apply (wpsimp wp: valid_queues_lift_asm [unfolded pred_conj_def, OF createObjects_orig_obj_at3] + createObjects_pred_tcb_at' [unfolded pred_conj_def]) apply fastforce apply wp+ apply fastforce diff --git a/proof/refine/X64/Schedule_R.thy b/proof/refine/X64/Schedule_R.thy index 3aa19c9a3f..4d6bf37acf 100644 --- a/proof/refine/X64/Schedule_R.thy +++ b/proof/refine/X64/Schedule_R.thy @@ -1078,8 +1078,7 @@ lemma dmo_cap_to'[wp]: lemma sct_cap_to'[wp]: "\ex_nonz_cap_to' p\ setCurThread t \\rv. ex_nonz_cap_to' p\" apply (simp add: setCurThread_def) - apply (wp ex_nonz_cap_to_pres') - apply (clarsimp elim!: cte_wp_at'_pspaceI)+ + apply (wpsimp wp: ex_nonz_cap_to_pres') done @@ -2098,7 +2097,7 @@ proof - apply (rename_tac l1) apply (case_tac "l1 = 0") (* switch to idle thread *) - apply (simp, wp (once) switchToIdleThread_invs_no_cicd', simp) + apply (simp, wp switchToIdleThread_invs_no_cicd', simp) (* we have a thread to switch to *) apply (clarsimp simp: bitmap_fun_defs) apply (wp assert_inv) diff --git a/proof/refine/X64/TcbAcc_R.thy b/proof/refine/X64/TcbAcc_R.thy index a93e6af8f7..99e9ebc658 100644 --- a/proof/refine/X64/TcbAcc_R.thy +++ b/proof/refine/X64/TcbAcc_R.thy @@ -2345,7 +2345,7 @@ lemma threadSet_queued_sch_act_wf[wp]: "\\s. sch_act_wf (ksSchedulerAction s) s\ threadSet (tcbQueued_update f) t \\_ s. sch_act_wf (ksSchedulerAction s) s\" - including no_pre + including classic_wp_pre apply (simp add: sch_act_wf_cases split: scheduler_action.split) apply (wp hoare_vcg_conj_lift) @@ -2866,7 +2866,7 @@ lemma rescheduleRequired_valid_bitmapQ_sch_act_simple: "\ valid_bitmapQ and sch_act_simple\ rescheduleRequired \\_. valid_bitmapQ \" - including no_pre + including classic_wp_pre apply (simp add: rescheduleRequired_def sch_act_simple_def) apply (rule_tac B="\rv s. valid_bitmapQ s \ (rv = ResumeCurrentThread \ rv = ChooseNewThread)" in hoare_seq_ext) @@ -2879,7 +2879,7 @@ lemma rescheduleRequired_bitmapQ_no_L1_orphans_sch_act_simple: "\ bitmapQ_no_L1_orphans and sch_act_simple\ rescheduleRequired \\_. bitmapQ_no_L1_orphans \" - including no_pre + including classic_wp_pre apply (simp add: rescheduleRequired_def sch_act_simple_def) apply (rule_tac B="\rv s. bitmapQ_no_L1_orphans s \ (rv = ResumeCurrentThread \ rv = ChooseNewThread)" in hoare_seq_ext) @@ -2892,7 +2892,7 @@ lemma rescheduleRequired_bitmapQ_no_L2_orphans_sch_act_simple: "\ bitmapQ_no_L2_orphans and sch_act_simple\ rescheduleRequired \\_. bitmapQ_no_L2_orphans \" - including no_pre + including classic_wp_pre apply (simp add: rescheduleRequired_def sch_act_simple_def) apply (rule_tac B="\rv s. bitmapQ_no_L2_orphans s \ (rv = ResumeCurrentThread \ rv = ChooseNewThread)" in hoare_seq_ext) diff --git a/proof/refine/X64/Tcb_R.thy b/proof/refine/X64/Tcb_R.thy index f90c895e5b..a5802efd31 100644 --- a/proof/refine/X64/Tcb_R.thy +++ b/proof/refine/X64/Tcb_R.thy @@ -1584,7 +1584,7 @@ proof - emptyable_def | wpc | strengthen tcb_cap_always_valid_strg use_no_cap_to_obj_asid_strg - | wp (once) add: sch_act_simple_lift hoare_drop_imps del: cteInsert_invs + | wp add: sch_act_simple_lift hoare_drop_imps del: cteInsert_invs | (erule exE, clarsimp simp: word_bits_def))+ (* the last two subgoals *) apply (clarsimp simp: tcb_at_cte_at_0 tcb_at_cte_at_1[simplified] tcb_at_st_tcb_at[symmetric] @@ -2735,7 +2735,7 @@ crunches getThreadBufferSlot, setPriority, setMCPriority lemma inv_tcb_IRQInactive: "\valid_irq_states'\ invokeTCB tcb_inv -, \\rv s. intStateIRQTable (ksInterruptState s) rv \ irqstate.IRQInactive\" - including no_pre + including classic_wp_pre apply (simp add: invokeTCB_def) apply (rule hoare_pre) apply (wpc | diff --git a/proof/refine/X64/VSpace_R.thy b/proof/refine/X64/VSpace_R.thy index 2ef1a0379d..51627c6037 100644 --- a/proof/refine/X64/VSpace_R.thy +++ b/proof/refine/X64/VSpace_R.thy @@ -347,13 +347,9 @@ lemma deleteASID_corres [corres]: apply (simp add: vs_refs_def) apply (rule image_eqI[rotated], erule graph_ofI) apply (simp add: mask_asid_low_bits_ucast_ucast) - apply wp - apply (simp add: o_def) - apply (wp getASID_wp) - apply clarsimp - apply assumption - apply wp+ - apply clarsimp + \ \rewrite assumption so that the goal can refer to the C variable instead of the abstract's.\ + apply (drule Some_to_the) + apply (wpsimp wp: getASID_wp)+ apply (clarsimp simp: valid_arch_state_def valid_asid_table_def dest!: invs_arch_state) apply blast