From 0de5a12190c4ba789a7eacd760ca0b8e23c4b1c1 Mon Sep 17 00:00:00 2001 From: Corey Lewis Date: Tue, 1 Aug 2023 16:17:24 +1000 Subject: [PATCH] proof+autocorres: update for select_wp Signed-off-by: Corey Lewis --- proof/access-control/ADT_AC.thy | 3 +- proof/access-control/ARM/ArchArch_AC.thy | 3 +- proof/access-control/ARM/ArchCNode_AC.thy | 2 +- proof/access-control/CNode_AC.thy | 4 +- proof/access-control/DomainSepInv.thy | 6 +- proof/access-control/Finalise_AC.thy | 8 +- proof/access-control/Ipc_AC.thy | 2 +- proof/access-control/RISCV64/ArchCNode_AC.thy | 2 +- proof/access-control/Syscall_AC.thy | 29 +++--- proof/bisim/Syscall_S.thy | 2 +- proof/capDL-api/Arch_DP.thy | 18 ++-- proof/capDL-api/CNode_DP.thy | 2 +- proof/capDL-api/IRQ_DP.thy | 9 +- proof/capDL-api/Invocation_DP.thy | 72 ++++++-------- proof/capDL-api/KHeap_DP.thy | 20 ++-- proof/capDL-api/Retype_DP.thy | 97 ++++++++----------- proof/capDL-api/TCB_DP.thy | 49 +++++----- proof/crefine/ARM/Refine_C.thy | 2 +- proof/crefine/ARM/Syscall_C.thy | 3 +- proof/crefine/ARM_HYP/Refine_C.thy | 2 +- proof/crefine/ARM_HYP/Syscall_C.thy | 3 +- proof/crefine/RISCV64/ArchMove_C.thy | 3 +- proof/crefine/RISCV64/Refine_C.thy | 2 +- proof/crefine/RISCV64/Syscall_C.thy | 3 +- proof/crefine/X64/Refine_C.thy | 2 +- proof/crefine/X64/Syscall_C.thy | 3 +- .../crefine/lib/AutoCorresModifiesProofs.thy | 2 +- proof/crefine/lib/AutoCorres_C.thy | 4 +- proof/drefine/Arch_DR.thy | 19 ++-- proof/drefine/CNode_DR.thy | 4 +- proof/drefine/Ipc_DR.thy | 2 +- proof/drefine/KHeap_DR.thy | 9 +- proof/drefine/Schedule_DR.thy | 2 +- proof/infoflow/ADT_IF.thy | 2 +- proof/infoflow/ARM/ArchADT_IF.thy | 28 +++--- proof/infoflow/ARM/ArchArch_IF.thy | 2 +- proof/infoflow/ARM/ArchDecode_IF.thy | 2 +- proof/infoflow/ARM/ArchIRQMasks_IF.thy | 6 +- proof/infoflow/ARM/ArchNoninterference.thy | 11 ++- proof/infoflow/ARM/ArchPasUpdates.thy | 2 +- proof/infoflow/ARM/ArchSyscall_IF.thy | 2 +- proof/infoflow/ARM/ArchUserOp_IF.thy | 2 +- proof/infoflow/Arch_IF.thy | 2 +- proof/infoflow/FinalCaps.thy | 6 +- proof/infoflow/Finalise_IF.thy | 2 +- proof/infoflow/IRQMasks_IF.thy | 4 +- proof/infoflow/PasUpdates.thy | 2 +- proof/infoflow/RISCV64/ArchADT_IF.thy | 26 ++--- proof/infoflow/RISCV64/ArchArch_IF.thy | 2 +- proof/infoflow/RISCV64/ArchDecode_IF.thy | 6 +- proof/infoflow/RISCV64/ArchIRQMasks_IF.thy | 6 +- .../infoflow/RISCV64/ArchNoninterference.thy | 11 ++- proof/infoflow/RISCV64/ArchPasUpdates.thy | 2 +- proof/infoflow/RISCV64/ArchUserOp_IF.thy | 2 +- proof/infoflow/Syscall_IF.thy | 2 +- proof/infoflow/refine/ADT_IF_Refine.thy | 1 - .../infoflow/refine/ARM/ArchADT_IF_Refine.thy | 15 ++- .../refine/ARM/ArchADT_IF_Refine_C.thy | 2 +- .../refine/RISCV64/ArchADT_IF_Refine.thy | 13 ++- .../refine/RISCV64/ArchADT_IF_Refine_C.thy | 2 +- .../AARCH64/ArchArch_AI.thy | 4 +- .../AARCH64/ArchDetSchedSchedule_AI.thy | 2 +- .../AARCH64/ArchFinalise_AI.thy | 4 +- .../AARCH64/ArchVCPU_AI.thy | 8 +- .../AARCH64/ArchVSpaceEntries_AI.thy | 8 +- .../invariant-abstract/AARCH64/Machine_AI.thy | 4 +- proof/invariant-abstract/AInvs.thy | 4 +- proof/invariant-abstract/ARM/ArchArch_AI.thy | 6 +- .../ARM/ArchDetSchedSchedule_AI.thy | 2 +- .../ARM/ArchFinalise_AI.thy | 2 +- .../ARM/ArchVSpaceEntries_AI.thy | 7 +- proof/invariant-abstract/ARM/Machine_AI.thy | 8 +- .../ARM_HYP/ArchArch_AI.thy | 6 +- .../ARM_HYP/ArchDetSchedSchedule_AI.thy | 2 +- .../ARM_HYP/ArchFinalise_AI.thy | 2 +- .../ARM_HYP/ArchVCPU_AI.thy | 8 +- .../ARM_HYP/ArchVSpaceEntries_AI.thy | 7 +- .../invariant-abstract/ARM_HYP/Machine_AI.thy | 9 +- proof/invariant-abstract/CNodeInv_AI.thy | 20 ++-- proof/invariant-abstract/CSpace_AI.thy | 2 +- .../DetSchedDomainTime_AI.thy | 3 +- .../DetSchedSchedule_AI.thy | 10 +- proof/invariant-abstract/Deterministic_AI.thy | 4 +- proof/invariant-abstract/Finalise_AI.thy | 6 +- proof/invariant-abstract/Invariants_AI.thy | 3 +- proof/invariant-abstract/IpcCancel_AI.thy | 18 ++-- proof/invariant-abstract/Ipc_AI.thy | 6 +- proof/invariant-abstract/LevityCatch_AI.thy | 4 +- .../RISCV64/ArchArch_AI.thy | 4 +- .../RISCV64/ArchDetSchedSchedule_AI.thy | 2 +- .../RISCV64/ArchFinalise_AI.thy | 2 +- .../RISCV64/ArchVSpaceEntries_AI.thy | 9 +- .../invariant-abstract/RISCV64/Machine_AI.thy | 6 +- proof/invariant-abstract/Schedule_AI.thy | 9 +- proof/invariant-abstract/Tcb_AI.thy | 3 - proof/invariant-abstract/X64/ArchArch_AI.thy | 6 +- .../X64/ArchDetSchedSchedule_AI.thy | 2 +- .../X64/ArchFinalise_AI.thy | 2 +- .../X64/ArchVSpaceEntries_AI.thy | 9 +- proof/invariant-abstract/X64/Machine_AI.thy | 9 +- proof/refine/AARCH64/InterruptAcc_R.thy | 2 +- proof/refine/AARCH64/IpcCancel_R.thy | 2 +- proof/refine/AARCH64/Ipc_R.thy | 2 +- proof/refine/AARCH64/KHeap_R.thy | 8 +- proof/refine/AARCH64/Refine.thy | 14 +-- proof/refine/AARCH64/Schedule_R.thy | 2 +- proof/refine/AARCH64/Untyped_R.thy | 2 +- proof/refine/ARM/InterruptAcc_R.thy | 2 +- proof/refine/ARM/Ipc_R.thy | 2 +- proof/refine/ARM/KHeap_R.thy | 8 +- proof/refine/ARM/Refine.thy | 14 +-- proof/refine/ARM/Schedule_R.thy | 2 +- proof/refine/ARM/Untyped_R.thy | 2 +- proof/refine/ARM_HYP/InterruptAcc_R.thy | 2 +- proof/refine/ARM_HYP/Ipc_R.thy | 2 +- proof/refine/ARM_HYP/KHeap_R.thy | 8 +- proof/refine/ARM_HYP/Refine.thy | 12 +-- proof/refine/ARM_HYP/Schedule_R.thy | 2 +- proof/refine/ARM_HYP/Untyped_R.thy | 2 +- proof/refine/Move_R.thy | 1 - proof/refine/RISCV64/InterruptAcc_R.thy | 2 +- proof/refine/RISCV64/IpcCancel_R.thy | 2 +- proof/refine/RISCV64/Ipc_R.thy | 2 +- proof/refine/RISCV64/KHeap_R.thy | 8 +- proof/refine/RISCV64/Refine.thy | 14 +-- proof/refine/RISCV64/Schedule_R.thy | 2 +- proof/refine/RISCV64/Untyped_R.thy | 2 +- proof/refine/X64/InterruptAcc_R.thy | 2 +- proof/refine/X64/Ipc_R.thy | 2 +- proof/refine/X64/KHeap_R.thy | 8 +- proof/refine/X64/Refine.thy | 14 +-- proof/refine/X64/Schedule_R.thy | 2 +- proof/refine/X64/Untyped_R.thy | 2 +- proof/sep-capDL/Frame_SD.thy | 2 +- proof/sep-capDL/Helpers_SD.thy | 2 +- tools/autocorres/L1Defs.thy | 4 +- tools/autocorres/L1Valid.thy | 2 +- tools/autocorres/L2Opt.thy | 2 +- 138 files changed, 450 insertions(+), 503 deletions(-) diff --git a/proof/access-control/ADT_AC.thy b/proof/access-control/ADT_AC.thy index eb85735b24..f0c20cbbf2 100644 --- a/proof/access-control/ADT_AC.thy +++ b/proof/access-control/ADT_AC.thy @@ -95,7 +95,8 @@ lemma do_user_op_respects: apply (rule dmo_device_update_respects_Write) apply (wpsimp wp: dmo_um_upd_machine_state dmo_user_memory_update_respects_Write - hoare_vcg_all_lift hoare_vcg_imp_lift)+ + hoare_vcg_all_lift hoare_vcg_imp_lift + wp_del: select_wp)+ apply (rule hoare_pre_cont) apply (wpsimp wp: select_wp)+ apply (simp add: restrict_map_def split: if_splits) diff --git a/proof/access-control/ARM/ArchArch_AC.thy b/proof/access-control/ARM/ArchArch_AC.thy index f1c2b9c0d5..cd183bec17 100644 --- a/proof/access-control/ARM/ArchArch_AC.thy +++ b/proof/access-control/ARM/ArchArch_AC.thy @@ -826,8 +826,7 @@ lemma decode_arch_invocation_authorised: apply (rule hoare_pre) apply (simp add: split_def Let_def split del: if_split cong: cap.case_cong arch_cap.case_cong if_cong option.case_cong) - apply (wp select_wp whenE_throwError_wp check_vp_wpR - find_pd_for_asid_authority2 + apply (wp whenE_throwError_wp check_vp_wpR find_pd_for_asid_authority2 | wpc | simp add: authorised_asid_control_inv_def authorised_page_inv_def authorised_page_directory_inv_def diff --git a/proof/access-control/ARM/ArchCNode_AC.thy b/proof/access-control/ARM/ArchCNode_AC.thy index a385de3008..1e5cc2acb5 100644 --- a/proof/access-control/ARM/ArchCNode_AC.thy +++ b/proof/access-control/ARM/ArchCNode_AC.thy @@ -75,7 +75,7 @@ crunches set_cdt crunches prepare_thread_delete, arch_finalise_cap for cur_domain[CNode_AC_assms, wp]:"\s. P (cur_domain s)" - (wp: crunch_wps select_wp hoare_vcg_if_lift2 simp: unless_def) + (wp: crunch_wps hoare_vcg_if_lift2 simp: unless_def) lemma state_vrefs_tcb_upd[CNode_AC_assms]: "tcb_at t s \ state_vrefs (s\kheap := kheap s(t \ TCB tcb)\) = state_vrefs s" diff --git a/proof/access-control/CNode_AC.thy b/proof/access-control/CNode_AC.thy index 6bc3ac1bca..de40cd12e5 100644 --- a/proof/access-control/CNode_AC.thy +++ b/proof/access-control/CNode_AC.thy @@ -1522,10 +1522,10 @@ lemma post_cap_deletion_cur_domain[wp]: by (wpsimp simp: post_cap_deletion_def) crunch cur_domain[wp]: cap_swap_for_delete, empty_slot "\s. P (cur_domain s)" - (wp: crunch_wps select_wp hoare_vcg_if_lift2 simp: unless_def) + (wp: crunch_wps hoare_vcg_if_lift2 simp: unless_def) crunch cur_domain[wp]: finalise_cap "\s. P (cur_domain s)" - (wp: crunch_wps select_wp hoare_vcg_if_lift2 simp: unless_def) + (wp: crunch_wps hoare_vcg_if_lift2 simp: unless_def) lemma rec_del_cur_domain[wp]: "rec_del call \\s. P (cur_domain s)\" diff --git a/proof/access-control/DomainSepInv.thy b/proof/access-control/DomainSepInv.thy index 691ef30d7a..d9ecb7131e 100644 --- a/proof/access-control/DomainSepInv.thy +++ b/proof/access-control/DomainSepInv.thy @@ -439,7 +439,7 @@ lemma reply_cancel_ipc_domain_sep_inv[wp]: reply_cancel_ipc t \\_ s. domain_sep_inv irqs (st :: 'state_ext state) (s :: det_ext state)\" apply (simp add: reply_cancel_ipc_def) - apply (wp select_wp) + apply wp apply (rule hoare_strengthen_post[OF thread_set_tcb_fault_update_domain_sep_inv]) apply auto done @@ -553,7 +553,7 @@ lemma cap_revoke_domain_sep_inv': apply (wp drop_spec_validE[OF valid_validE[OF preemption_point_domain_sep_inv]] drop_spec_validE[OF valid_validE[OF cap_delete_domain_sep_inv]] drop_spec_validE[OF assertE_wp] drop_spec_validE[OF returnOk_wp] - drop_spec_validE[OF liftE_wp] select_wp + drop_spec_validE[OF liftE_wp] | simp | wp (once) hoare_drop_imps)+ done qed @@ -1181,7 +1181,7 @@ lemma handle_event_domain_sep_inv: lemma schedule_domain_sep_inv: "(schedule :: (unit,det_ext) s_monad) \domain_sep_inv irqs (st :: 'state_ext state)\" apply (simp add: schedule_def allActiveTCBs_def) - apply (wp add: alternative_wp select_wp guarded_switch_to_lift hoare_drop_imps + apply (wp add: guarded_switch_to_lift hoare_drop_imps del: ethread_get_wp | wpc | clarsimp simp: get_thread_state_def thread_get_def trans_state_update'[symmetric] schedule_choose_new_thread_def)+ diff --git a/proof/access-control/Finalise_AC.thy b/proof/access-control/Finalise_AC.thy index b122ad4d15..ca1ccb5d7c 100644 --- a/proof/access-control/Finalise_AC.thy +++ b/proof/access-control/Finalise_AC.thy @@ -347,7 +347,7 @@ lemma reply_cancel_ipc_pas_refined[wp]: \\_. pas_refined aag\" apply (rule hoare_gen_asm) apply (simp add: reply_cancel_ipc_def) - apply (wp add: select_wp wp_transferable del: wp_not_transferable) + apply (wp add: wp_transferable del: wp_not_transferable) apply (rule hoare_strengthen_post[where Q="\_. invs and tcb_at t and pas_refined aag"]) apply (wpsimp wp: hoare_wp_combs thread_set_tcb_fault_reset_invs thread_set_pas_refined)+ apply (frule(1) reply_cap_descends_from_master0) @@ -368,7 +368,7 @@ crunches suspend for pspace_aligned[wp]: "\s :: det_ext state. pspace_aligned s" and valid_vspace_objs[wp]: "\s :: det_ext state. valid_vspace_objs s" and valid_arch_state[wp]: "\s :: det_ext state. valid_arch_state s" - (wp: dxo_wp_weak select_wp hoare_drop_imps simp: crunch_simps) + (wp: dxo_wp_weak hoare_drop_imps simp: crunch_simps) crunch pas_refined[wp]: suspend "pas_refined aag" @@ -528,7 +528,7 @@ lemma reply_cancel_ipc_respects[wp]: \\_. integrity aag X st\" apply (simp add: reply_cancel_ipc_def) apply (rule hoare_pre) - apply (wp add: select_wp wp_transferable del:wp_not_transferable) + apply (wp add: wp_transferable del:wp_not_transferable) apply simp apply (rule hoare_lift_Pf2[where f="cdt"]) apply (wpsimp wp: hoare_vcg_const_Ball_lift thread_set_integrity_autarch @@ -1231,7 +1231,7 @@ proof (induct rule: cap_revoke.induct) apply (subst cap_revoke.simps) apply (unfold P_def) apply (wp "1.hyps"[unfolded P_def], simp+) - apply (wp preemption_point_inv hoare_drop_imps select_wp + apply (wp preemption_point_inv hoare_drop_imps rec_del_preserves_cte_zombie_null_insts[where P=Q] | simp add: Q_Null Q_Zombie)+ done diff --git a/proof/access-control/Ipc_AC.thy b/proof/access-control/Ipc_AC.thy index 512ce60b96..675f430a10 100644 --- a/proof/access-control/Ipc_AC.thy +++ b/proof/access-control/Ipc_AC.thy @@ -37,7 +37,7 @@ lemma send_signal_caps_of_state[wp]: done crunch mdb[wp]: blocked_cancel_ipc, update_waiting_ntfn "\s. P (cdt (s :: det_ext state))" - (wp: crunch_wps unless_wp select_wp dxo_wp_weak simp: crunch_simps) + (wp: crunch_wps unless_wp dxo_wp_weak simp: crunch_simps) lemma cancel_ipc_receive_blocked_mdb: "\\s :: det_ext state. P (cdt s) \ st_tcb_at receive_blocked t s\ diff --git a/proof/access-control/RISCV64/ArchCNode_AC.thy b/proof/access-control/RISCV64/ArchCNode_AC.thy index 245bc1ee9b..ae5a893e22 100644 --- a/proof/access-control/RISCV64/ArchCNode_AC.thy +++ b/proof/access-control/RISCV64/ArchCNode_AC.thy @@ -97,7 +97,7 @@ crunches set_cdt crunches prepare_thread_delete, arch_finalise_cap for cur_domain[CNode_AC_assms, wp]:"\s. P (cur_domain s)" - (wp: crunch_wps select_wp hoare_vcg_if_lift2 simp: unless_def) + (wp: crunch_wps hoare_vcg_if_lift2 simp: unless_def) lemma state_vrefs_tcb_upd[CNode_AC_assms]: "\ pspace_aligned s; valid_vspace_objs s; valid_arch_state s; tcb_at t s \ diff --git a/proof/access-control/Syscall_AC.thy b/proof/access-control/Syscall_AC.thy index b873a14e6c..472347ebbe 100644 --- a/proof/access-control/Syscall_AC.thy +++ b/proof/access-control/Syscall_AC.thy @@ -699,7 +699,7 @@ lemma handle_event_integrity: handle_reply_respects handle_fault_integrity_autarch handle_interrupt_integrity handle_vm_fault_integrity handle_reply_pas_refined handle_vm_fault_valid_fault - handle_reply_valid_sched alternative_wp select_wp + handle_reply_valid_sched hoare_vcg_conj_lift hoare_vcg_all_lift hoare_drop_imps simp: domain_sep_inv_def | rule dmo_wp hoare_vcg_E_elim @@ -899,7 +899,7 @@ lemma schedule_integrity: schedule \\_. integrity aag X st\" apply (simp add: schedule_def) - apply (wpsimp wp: alternative_wp switch_to_thread_respects' select_wp guarded_switch_to_lift + apply (wpsimp wp: switch_to_thread_respects' guarded_switch_to_lift switch_to_idle_thread_respects choose_thread_respects gts_wp hoare_drop_imps set_scheduler_action_cnt_valid_sched append_thread_queued enqueue_thread_queued tcb_sched_action_enqueue_valid_blocked_except tcb_sched_action_append_integrity' @@ -949,14 +949,14 @@ crunch pas_refined[wp]: choose_thread "pas_refined aag" lemma schedule_pas_refined: "schedule \pas_refined aag\" apply (simp add: schedule_def allActiveTCBs_def) - apply (wp add: alternative_wp guarded_switch_to_lift switch_to_thread_pas_refined select_wp - switch_to_idle_thread_pas_refined gts_wp - guarded_switch_to_lift switch_to_thread_respects_pasMayEditReadyQueues - choose_thread_respects_pasMayEditReadyQueues - next_domain_valid_sched next_domain_valid_queues gts_wp hoare_drop_imps - set_scheduler_action_cnt_valid_sched enqueue_thread_queued - tcb_sched_action_enqueue_valid_blocked_except - del: ethread_get_wp + apply (wp add: guarded_switch_to_lift switch_to_thread_pas_refined + switch_to_idle_thread_pas_refined gts_wp + guarded_switch_to_lift switch_to_thread_respects_pasMayEditReadyQueues + choose_thread_respects_pasMayEditReadyQueues + next_domain_valid_sched next_domain_valid_queues gts_wp hoare_drop_imps + set_scheduler_action_cnt_valid_sched enqueue_thread_queued + tcb_sched_action_enqueue_valid_blocked_except + del: ethread_get_wp | wpc | simp add: schedule_choose_new_thread_def)+ done @@ -983,7 +983,7 @@ lemma ct_active_update[simp]: lemma set_cap_ct_active[wp]: "set_cap ptr c \ct_active \" apply (rule hoare_pre) - apply (wps | wpsimp wp: select_wp sts_st_tcb_at_cases thread_set_no_change_tcb_state + apply (wps | wpsimp wp: sts_st_tcb_at_cases thread_set_no_change_tcb_state simp: crunch_simps ct_in_state_def)+ done @@ -1034,7 +1034,7 @@ crunch ct_active[wp]: post_cap_deletion, empty_slot "\s :: det_ext state wp: crunch_wps filterM_preserved unless_wp) crunch cur_thread[wp]: cap_swap_for_delete, finalise_cap "\s :: det_ext state. P (cur_thread s)" - (wp: select_wp dxo_wp_weak crunch_wps simp: crunch_simps) + (wp: dxo_wp_weak crunch_wps simp: crunch_simps) lemma rec_del_cur_thread[wp]: "rec_del a \\s :: det_ext state. P (cur_thread s)\" @@ -1139,8 +1139,7 @@ lemma call_kernel_integrity': apply (simp add: call_kernel_def) apply (simp only: spec_valid_def) apply (wpsimp wp: activate_thread_respects schedule_integrity_pasMayEditReadyQueues - handle_interrupt_integrity dmo_wp alternative_wp - select_wp handle_interrupt_pas_refined) + handle_interrupt_integrity dmo_wp handle_interrupt_pas_refined) apply (clarsimp simp: if_fun_split) apply (rule_tac Q="\rv ms. (rv \ None \ the rv \ non_kernel_IRQs) \ R True (domain_sep_inv (pasMaySendIrqs aag) st' s) rv ms" @@ -1182,7 +1181,7 @@ lemma call_kernel_pas_refined: \\_. pas_refined aag\" apply (simp add: call_kernel_def ) apply (wp activate_thread_pas_refined schedule_pas_refined handle_interrupt_pas_refined - do_machine_op_pas_refined dmo_wp alternative_wp select_wp hoare_drop_imps getActiveIRQ_inv + do_machine_op_pas_refined dmo_wp hoare_drop_imps getActiveIRQ_inv | simp add: if_fun_split | strengthen invs_psp_aligned invs_vspace_objs invs_arch_state)+ apply (wp he_invs handle_event_pas_refined) diff --git a/proof/bisim/Syscall_S.thy b/proof/bisim/Syscall_S.thy index 623a060613..f43a01ef99 100644 --- a/proof/bisim/Syscall_S.thy +++ b/proof/bisim/Syscall_S.thy @@ -699,7 +699,7 @@ lemma schedule_separate_state [wp]: "\separate_state\ schedule :: (unit,unit) s_monad \\_. separate_state\" unfolding schedule_def switch_to_thread_def arch_switch_to_thread_def switch_to_idle_thread_def arch_switch_to_idle_thread_def allActiveTCBs_def - by (wpsimp wp: select_inv separate_state_pres' alternative_wp + by (wpsimp wp: select_inv separate_state_pres' simp: arch_activate_idle_thread_def | strengthen imp_consequent)+ diff --git a/proof/capDL-api/Arch_DP.thy b/proof/capDL-api/Arch_DP.thy index cd5acdcbf4..6543ac019b 100644 --- a/proof/capDL-api/Arch_DP.thy +++ b/proof/capDL-api/Arch_DP.thy @@ -65,9 +65,9 @@ lemma decode_page_map_intent_rv_20_24: \\r s. R r\, -" apply (simp add: decode_invocation_def get_index_def get_page_intent_def throw_opt_def cap_rights_def decode_page_invocation_def throw_on_none_def get_mapped_asid_def) - apply (wp alternativeE_wp select_wp | wpc)+ + apply (wp | wpc)+ apply (rule validE_validE_R) - apply (wp alternativeE_wp) + apply wp apply (simp add:cdl_page_mapping_entries_def split del:if_split | wp | wpc)+ apply auto done @@ -86,9 +86,9 @@ lemma decode_page_map_intent_rv_16_12: get_page_intent_def throw_opt_def cap_rights_def decode_page_invocation_def throw_on_none_def get_mapped_asid_def) - apply (wp alternativeE_wp select_wp) + apply wp apply (rule validE_validE_R) - apply (wp alternativeE_wp) + apply wp apply (simp add:cdl_page_mapping_entries_def) apply (wp cdl_lookup_pt_slot_rv | wpc | simp)+ apply auto @@ -130,13 +130,13 @@ lemma invoke_page_table_wp: done crunch cdl_cur_thread[wp]: invoke_page "\s. P (cdl_current_thread s)" -(wp: crunch_wps select_wp alternative_wp simp : swp_def ) + (wp: crunch_wps simp: swp_def) crunch cdl_cur_thread[wp]: invoke_page_table "\s. P (cdl_current_thread s)" -(wp: crunch_wps select_wp alternative_wp simp : swp_def ) + (wp: crunch_wps simp: swp_def) crunch cdl_cur_domain[wp]: invoke_page_table, invoke_page "\s. P (cdl_current_domain s)" -(wp: crunch_wps select_wp alternative_wp simp : swp_def unless_def) + (wp: crunch_wps simp: swp_def unless_def) lemmas cap_asid_simps[simp] = cap_asid_def[split_simps cdl_cap.split] lemmas cap_mapped_simps[simp] = cap_mapped_def[split_simps cdl_cap.split] @@ -153,7 +153,7 @@ lemma decode_page_table_rv: apply (simp add:decode_invocation_def get_page_table_intent_def throw_opt_def decode_page_table_invocation_def) apply (rule hoare_pre) - apply (wp alternativeE_wp throw_on_none_wp | wpc | simp)+ + apply (wp throw_on_none_wp | wpc | simp)+ apply (clarsimp split:option.splits simp:get_index_def cap_object_def cap_has_object_def get_mapped_asid_def) done @@ -564,7 +564,7 @@ lemma decode_invocation_asid_pool_assign: decode_asid_pool_invocation_def get_index_def throw_opt_def throw_on_none_def) apply (rule validE_validE_R) - apply (wp alternativeE_wp select_wp) + apply wp apply (clarsimp simp:cap_object_def cap_has_object_def) done diff --git a/proof/capDL-api/CNode_DP.thy b/proof/capDL-api/CNode_DP.thy index dbd2c762a6..fd1420c280 100644 --- a/proof/capDL-api/CNode_DP.thy +++ b/proof/capDL-api/CNode_DP.thy @@ -60,7 +60,7 @@ lemma invoke_cnode_insert_cdl_current_domain[wp]: \\_ s. P (cdl_current_domain s) \" apply (simp add: invoke_cnode_def) apply (rule hoare_pre) - apply (wp alternative_wp | wpc | clarsimp)+ + apply (wp | wpc | clarsimp)+ done lemma invoke_cnode_move_cdl_current_domain[wp]: diff --git a/proof/capDL-api/IRQ_DP.thy b/proof/capDL-api/IRQ_DP.thy index 0d0b6659e1..6f4a1ec470 100644 --- a/proof/capDL-api/IRQ_DP.thy +++ b/proof/capDL-api/IRQ_DP.thy @@ -46,7 +46,6 @@ lemma invoke_irq_handler_set_handler_wp: invoke_irq_handler (SetIrqHandler irq cap slot) \\_. < irq \irq obj \* (obj, 0) \c cap \* R> \" apply (clarsimp simp: invoke_irq_handler_def, wp) - apply (wp alternative_wp) apply (wp sep_wp: insert_cap_child_wp insert_cap_sibling_wp)+ apply (sep_wp delete_cap_simple_format[where cap=cap'])+ apply (safe) @@ -71,7 +70,7 @@ lemma decode_invocation_irq_ack_rv': decode_irq_handler_invocation cap cap_ref caps (IrqHandlerAckIntent) \P\, -" apply (clarsimp simp: decode_irq_handler_invocation_def) - apply (wp alternativeE_R_wp) + apply wp apply (clarsimp) done @@ -80,7 +79,7 @@ lemma decode_invocation_irq_clear_rv': decode_irq_handler_invocation cap cap_ref caps (IrqHandlerClearIntent) \P\, -" apply (clarsimp simp: decode_irq_handler_invocation_def) - apply (wp alternativeE_R_wp) + apply wp apply (clarsimp) done @@ -105,7 +104,7 @@ decode_irq_handler_invocation cap cap_ref caps (IrqHandlerSetEndpointIntent) \P\, -" apply (rule validE_R_gen_asm_conj) apply (clarsimp simp: decode_irq_handler_invocation_def) - apply (wp alternativeE_R_wp | wpc)+ + apply (wp | wpc)+ apply (clarsimp split: cdl_cap.splits, safe) apply ((wp throw_on_none_rv)+, clarsimp simp: get_index_def) apply simp @@ -117,7 +116,7 @@ lemma decode_irq_control_issue_irq_rv: <\ (r, (unat depth)) : root_cap index \u cap \* R> s\ decode_irq_control_invocation target target_ref caps (IrqControlIssueIrqHandlerIntent irq index depth) \P\, -" apply (clarsimp simp: decode_irq_control_invocation_def) - apply (wp alternativeE_R_wp lookup_slot_for_cnode_op_rvu'[where cap=cap and r=r] throw_on_none_rv) + apply (wp lookup_slot_for_cnode_op_rvu'[where cap=cap and r=r] throw_on_none_rv) apply (clarsimp simp: get_index_def) apply (sep_solve) done diff --git a/proof/capDL-api/Invocation_DP.thy b/proof/capDL-api/Invocation_DP.thy index 9b16571f1b..56a9ae7c76 100644 --- a/proof/capDL-api/Invocation_DP.thy +++ b/proof/capDL-api/Invocation_DP.thy @@ -12,10 +12,10 @@ crunch cdl_current_domain[wp]: update_available_range, generate_object_ids, upda mark_tcb_intent_error, corrupt_ipc_buffer, insert_cap_sibling, insert_cap_child, move_cap, invoke_irq_control, invoke_irq_handler "\s. P (cdl_current_domain s)" -(wp: crunch_wps select_wp alternative_wp alternativeE_wp unless_wp simp: split_def corrupt_intents_def) +(wp: crunch_wps unless_wp simp: split_def corrupt_intents_def) crunch cdl_irq_node [wp]: corrupt_ipc_buffer "\s. P (cdl_irq_node s)" -(wp: crunch_wps select_wp simp: corrupt_intents_def) +(wp: crunch_wps simp: corrupt_intents_def) crunch cdl_irq_node [wp]: mark_tcb_intent_error "\s. P (cdl_irq_node s)" (wp: crunch_wps) @@ -124,7 +124,7 @@ lemma corrupt_tcb_intent_sep_helper[wp]: \\rv s. A (object_at (\obj. P (object_clean obj)) ptr s)\" apply (simp add:corrupt_tcb_intent_def update_thread_def set_object_def) - apply (wp select_wp | wpc | simp add:set_object_def)+ + apply (wp | wpc | simp add:set_object_def)+ apply (clarsimp simp:object_at_def) apply (simp add:object_clean_def intent_reset_def object_slots_def asid_reset_def update_slots_def) @@ -141,7 +141,7 @@ lemma corrupt_frame_sep_helper[wp]: "\\s. A (object_at (\obj. P (object_clean obj)) ptr s)\ corrupt_frame a \\rv s. A (object_at (\obj. P (object_clean obj)) ptr s)\" apply (simp add:corrupt_frame_def) - apply (wp select_wp) + apply wp apply (clarsimp simp:corrupt_intents_def object_at_def map_add_def split:option.splits cdl_object.splits) apply (simp add:object_clean_def intent_reset_def @@ -157,7 +157,7 @@ lemma corrupt_ipc_buffer_sep_inv[wp]: \\rv s. < P > s\" apply (rule sep_nonimpact_valid_lift) apply (simp add:corrupt_ipc_buffer_def) - apply (wp select_wp hoare_drop_imps | wpc | simp)+ + apply (wp hoare_drop_imps | wpc | simp)+ done lemma update_thread_intent_update: @@ -231,55 +231,48 @@ lemma no_exception_conj': done crunch inv[wp]: decode_untyped_invocation P - (wp:crunch_wps alternativeE_wp mapME_x_inv_wp - unlessE_wp simp:crunch_simps throw_on_none_def) + (wp: crunch_wps mapME_x_inv_wp unlessE_wp simp: crunch_simps throw_on_none_def) crunch inv[wp]: decode_irq_handler_invocation P - (wp:crunch_wps alternativeE_wp - simp:liftE_bindE throw_on_none_def) + (wp: crunch_wps simp: liftE_bindE throw_on_none_def) crunch inv[wp]: decode_tcb_invocation P - (wp:crunch_wps alternativeE_wp - simp:liftE_bindE throw_on_none_def) + (wp: crunch_wps simp: liftE_bindE throw_on_none_def) crunch inv[wp]: decode_domain_invocation P - (wp:crunch_wps alternativeE_wp - simp:liftE_bindE throw_on_none_def) + (wp:crunch_wps simp: liftE_bindE throw_on_none_def) crunch inv[wp]: decode_irq_control_invocation P - (wp:crunch_wps alternativeE_wp select_wp - simp:liftE_bindE throw_on_none_def) + (wp: crunch_wps simp: liftE_bindE throw_on_none_def) crunch inv[wp]: decode_asid_control_invocation P - (wp:crunch_wps alternativeE_wp select_wp ignore:returnOk - simp:liftE_bindE throw_on_none_def) + (wp: crunch_wps ignore: returnOk simp: liftE_bindE throw_on_none_def) crunch inv[wp]: lookup_cap_and_slot P (wp:crunch_wps resolve_address_bits_wp) crunch inv[wp]: decode_page_invocation P - (wp:crunch_wps alternativeE_wp select_wp resolve_address_bits_wp - simp:throw_on_none_def) + (wp: crunch_wps resolve_address_bits_wp simp: throw_on_none_def) lemma decode_page_table_invocation_inv[wp]: "\P\ decode_page_table_invocation a b c d \\_. P\" apply (simp add:decode_page_table_invocation_def) apply (rule hoare_pre) - apply (wpc|wp alternativeE_wp select_wp |simp add:throw_on_none_def)+ + apply (wpc|wp |simp add:throw_on_none_def)+ done lemma decode_page_directory_invocation_inv[wp]: "\P\ decode_page_directory_invocation a b c d \\_. P\" apply (simp add:decode_page_directory_invocation_def) apply (rule hoare_pre) - apply (wpc|wp alternativeE_wp select_wp |simp add:throw_on_none_def)+ + apply (wpc|wp |simp add:throw_on_none_def)+ done lemma decode_asid_pool_invocation_inv[wp]: "\P\ decode_asid_pool_invocation a b c d \\_. P\" apply (simp add:decode_asid_pool_invocation_def) apply (rule hoare_pre) - apply (wpc|wp alternativeE_wp select_wp |simp add:throw_on_none_def)+ + apply (wpc|wp |simp add:throw_on_none_def)+ done lemma decode_invocation_inv[wp]: @@ -427,16 +420,15 @@ lemma handle_event_syscall_no_decode_exception: done crunch cdl_current_thread [wp]: delete_cap_simple "\s. P (cdl_current_thread s)" -(wp:crunch_wps select_wp simp:split_def unless_def) + (wp: crunch_wps simp: split_def unless_def) crunch cdl_current_thread [wp]: mark_tcb_intent_error "\s. P (cdl_current_thread s)" -(wp:crunch_wps select_wp simp:split_def unless_def) + (wp: crunch_wps simp: split_def unless_def) crunch cdl_current_thread [wp]: corrupt_ipc_buffer "\s. P (cdl_current_thread s)" -(wp:crunch_wps select_wp simp:split_def unless_def corrupt_frame_def corrupt_intents_def) + (wp: crunch_wps simp: split_def unless_def corrupt_frame_def corrupt_intents_def) crunch cdl_current_thread [wp]: invoke_irq_control, invoke_irq_handler "\s. P (cdl_current_thread s)" -(wp:alternative_wp) lemma corrupt_tcb_intent_all_active_tcbs[wp]: @@ -478,7 +470,7 @@ lemma send_signal_no_pending: \\r. P\" apply (simp add: send_signal_def send_signal_bound_def) apply (rule hoare_pre) - apply (wp alternative_wp | wpc)+ + apply (wp | wpc)+ apply (rule hoare_pre_cont) apply (rule_tac P = "waiters = {}" in hoare_gen_asm) apply (clarsimp simp: option_select_def) @@ -495,7 +487,7 @@ lemma send_signal_no_pending: done crunch invs[wp]: get_active_irq P - (wp: crunch_wps alternative_wp select_wp) + (wp: crunch_wps) lemma handle_pending_interrupts_no_ntf_cap: "\P and no_pending\ @@ -506,7 +498,7 @@ lemma handle_pending_interrupts_no_ntf_cap: apply (wp send_signal_no_pending | wpc | simp add: option_select_def handle_interrupt_def split del: if_split)+ - apply (wp alternative_wp select_wp hoare_drop_imps hoare_vcg_all_lift) + apply (wp hoare_drop_imps hoare_vcg_all_lift) apply simp done @@ -622,7 +614,7 @@ lemma invoke_cnode_insert_cap: apply (simp add:validE_def) apply (rule hoare_name_pre_state) apply (clarsimp simp:invoke_cnode_def liftE_bindE validE_def[symmetric]) - apply (wpsimp wp: alternative_wp insert_cap_sibling_wp insert_cap_child_wp) + apply (wpsimp wp: insert_cap_sibling_wp insert_cap_child_wp) done lemma invoke_cnode_move_wp: @@ -676,19 +668,17 @@ lemma cdl_cur_thread_detype: by (simp add:detype_def) crunch cdl_current_thread[wp]: reset_untyped_cap "\s. P (cdl_current_thread s)" - (wp: select_wp alternativeE_wp mapME_x_inv_wp whenE_wp - simp: cdl_cur_thread_detype crunch_simps) + (wp: mapME_x_inv_wp whenE_wp simp: cdl_cur_thread_detype crunch_simps) lemmas helper = valid_validE_E[OF reset_untyped_cap_cdl_current_thread] crunch cdl_current_thread[wp]: invoke_untyped "\s. P (cdl_current_thread s)" -(wp:select_wp mapM_x_wp' crunch_wps unless_wp alternativeE_wp - helper - simp:cdl_cur_thread_detype crunch_simps) + (wp: mapM_x_wp' crunch_wps unless_wp helper + simp:cdl_cur_thread_detype crunch_simps) crunch cdl_current_thread[wp]: move_cap "\s. P (cdl_current_thread s)" -(wp:select_wp mapM_x_wp' crunch_wps unless_wp - simp:crunch_simps) + (wp: mapM_x_wp' crunch_wps unless_wp + simp:crunch_simps) lemma cnode_insert_cap_cdl_current_thread: "\\s. P (cdl_current_thread s) \ @@ -698,7 +688,7 @@ lemma cnode_insert_cap_cdl_current_thread: apply (clarsimp simp: invoke_cnode_def liftE_bindE validE_def[symmetric]) apply (rule hoare_pre) - apply (wp alternative_wp | simp | wpc)+ + apply (wp | simp | wpc)+ done lemma cnode_move_cap_cdl_current_thread: @@ -709,7 +699,7 @@ lemma cnode_move_cap_cdl_current_thread: apply (clarsimp simp: invoke_cnode_def liftE_bindE validE_def[symmetric]) apply (rule hoare_pre) - apply (wp alternative_wp | simp | wpc)+ + apply (wp | simp | wpc)+ done lemma sep_any_imp_c'_conj: @@ -865,7 +855,7 @@ lemma tcb_has_error_set_cap: apply (simp add:set_cap_def gets_the_def set_object_def split_def) - apply (wp select_wp|wpc|simp)+ + apply (wp|wpc|simp)+ apply (clarsimp simp:tcb_has_error_def object_at_def,simp split:cdl_object.split_asm) apply (intro conjI impI) @@ -1130,7 +1120,7 @@ lemma invoke_cnode_insert_cap': apply (simp add:validE_def) apply (rule hoare_name_pre_state) apply (clarsimp simp:invoke_cnode_def liftE_bindE validE_def[symmetric]) - apply (wpsimp wp: alternative_wp insert_cap_sibling_wp insert_cap_child_wp + apply (wpsimp wp: insert_cap_sibling_wp insert_cap_child_wp simp: cap_of_insert_call_def) done diff --git a/proof/capDL-api/KHeap_DP.thy b/proof/capDL-api/KHeap_DP.thy index 0e31d16019..f2bdcf33b3 100644 --- a/proof/capDL-api/KHeap_DP.thy +++ b/proof/capDL-api/KHeap_DP.thy @@ -343,7 +343,7 @@ lemma decode_tcb_invocation: "\P\decode_tcb_invocation cap cap_ref caps (TcbWriteRegistersIntent resume flags count regs) \\_. P\" apply (clarsimp simp: decode_tcb_invocation_def) -apply (wp alternative_wp) +apply wp apply (clarsimp) done @@ -373,7 +373,7 @@ lemma invoke_cnode_insert_wp: \\_. c cap \* R>\" apply (rule hoare_gen_asm) apply (clarsimp simp: invoke_cnode_def) - apply (wp insert_cap_sibling_wp insert_cap_child_wp alternative_wp) + apply (wp insert_cap_sibling_wp insert_cap_child_wp) apply (clarsimp) done @@ -580,21 +580,21 @@ lemma derive_cap_rv: derive_cap slot cap \\rv s. P s \ ( rv = cap \ rv = NullCap )\, \\_ _. True\" apply (clarsimp simp: derive_cap_def returnOk_def split: cdl_cap.splits,safe) - apply (wp return_rv whenE_wp alternativeE_wp | clarsimp simp: ensure_no_children_def)+ + apply (wp return_rv whenE_wp | clarsimp simp: ensure_no_children_def)+ done lemma derive_cap_wp [wp]: "\P\ derive_cap slot cap \\_. P\" apply (clarsimp simp: derive_cap_def returnOk_def split: cdl_cap.splits) apply (safe) - apply ((wp alternative_wp whenE_wp)|(clarsimp simp: ensure_no_children_def))+ + apply ((wp whenE_wp)|(clarsimp simp: ensure_no_children_def))+ done lemma derive_cap_wpE: "\P\ derive_cap slot cap \\_.P\,\\_.P\" apply (clarsimp simp: derive_cap_def) - apply (case_tac cap, (wp whenE_wp alternative_wp | + apply (case_tac cap, (wp whenE_wp | simp add: ensure_no_children_def)+) done @@ -710,7 +710,7 @@ lemma derive_cap_invE: "\P (derived_cap cap) and Q\ derive_cap slot cap \P\, \\r. Q\" apply (simp add:derive_cap_def) apply (rule hoare_pre) - apply (wp alternative_wp alternativeE_wp|wpc|simp)+ + apply (wp|wpc|simp)+ apply (auto simp:derived_cap_def) done @@ -759,7 +759,7 @@ lemma decode_cnode_move_rvu: crunch preserve [wp]: decode_cnode_invocation "P" -(wp: derive_cap_wpE unlessE_wp whenE_wp select_wp hoare_drop_imps simp: if_apply_def2 throw_on_none_def) + (wp: derive_cap_wpE unlessE_wp whenE_wp hoare_drop_imps simp: if_apply_def2 throw_on_none_def) lemma decode_invocation_wp: "\P\ decode_invocation (CNodeCap x y z sz) ref caps (CNodeIntent intent) \\_. P\, -" @@ -1151,14 +1151,14 @@ lemma has_restart_cap_sep_wp: lemma lift_do_kernel_op': "\\s'. P s'\ f \\_ s'. Q s'\ \ \\s. P (kernel_state s)\ do_kernel_op f \\_ s. Q (kernel_state s)\" apply (simp add: do_kernel_op_def split_def) - apply (wp select_wp) + apply wp apply (simp add: valid_def split_def) done lemma lift_do_kernel_op: "\\s. s = s'\ f \\_ s. s = s'\ \ \\s. (kernel_state s) = s'\ do_kernel_op f \\_ s. (kernel_state s) = s'\" apply (simp add: do_kernel_op_def split_def) - apply (wp select_wp) + apply wp apply (simp add: valid_def split_def) done @@ -1179,7 +1179,7 @@ lemma schedule_no_choice_wp: schedule \\r s. cdl_current_thread s = Some current_thread \ cdl_current_domain s = current_domain \ P s\" apply (simp add:schedule_def switch_to_thread_def change_current_domain_def) - apply (wp alternative_wp select_wp) + apply wp apply (case_tac s,clarsimp) done diff --git a/proof/capDL-api/Retype_DP.thy b/proof/capDL-api/Retype_DP.thy index 09363f4db8..fc420ae076 100644 --- a/proof/capDL-api/Retype_DP.thy +++ b/proof/capDL-api/Retype_DP.thy @@ -50,7 +50,7 @@ lemma create_objects_mapM_x': qed crunch inv[wp]: generate_object_ids P -(wp:crunch_wps select_wp) + (wp: crunch_wps) lemma pick_rev: assumes "target_object_ids = map (\x. {x}) ids" @@ -111,7 +111,7 @@ lemma generate_object_ids_rv: \\r s. r = map (\x. {x}) (map pick r) \ length r = n \ set (map pick r) \ obj_range \ distinct (map pick r) \" apply (clarsimp simp:generate_object_ids_def) - apply (wp select_wp) + apply wp apply clarsimp apply (simp add: distinct_map) apply (intro conjI) @@ -185,7 +185,7 @@ lemma update_available_range_wp: apply (rule_tac x = new_range in exI) apply (intro conjI,assumption+) apply (sep_select 2,assumption) - apply (wp select_wp) + apply wp apply clarsimp+ done @@ -254,10 +254,10 @@ lemma reset_untyped_cap_wp: apply (rule_tac P = "\fr. cap = UntypedCap dev obj_range fr \ (\fr\ set x. free_range \ fr \ fr \ obj_range)" in hoare_gen_asmE) apply clarsimp - apply (wp whenE_wp mapME_x_wp alternativeE_wp) + apply (wp whenE_wp mapME_x_wp) apply (rule ballI) apply (rule hoare_pre) - apply (wp alternative_wp) + apply wp apply simp apply (rule hoare_post_imp[OF _ set_cap_wp]) apply clarsimp @@ -265,7 +265,7 @@ lemma reset_untyped_cap_wp: apply ((rule conjI, fastforce)+, sep_solve) apply clarsimp apply sep_solve - apply (wp select_wp | clarsimp)+ + apply (wp | clarsimp)+ apply (subst dummy_detype_if_untyped) apply simp apply (sep_select_asm 2) @@ -292,12 +292,12 @@ lemma reset_untyped_cap_wp: done crunch cdl_current_domain[wp]: reset_untyped_cap "\s. P (cdl_current_domain s)" -(wp:select_wp mapM_x_wp' mapME_x_inv_wp alternativeE_wp crunch_wps unless_wp - simp: detype_def crunch_simps) + (wp: mapM_x_wp' mapME_x_inv_wp crunch_wps unless_wp + simp: detype_def crunch_simps) crunch cdl_current_domain[wp]: invoke_untyped "\s. P (cdl_current_domain s)" -(wp: select_wp mapM_x_wp' mapME_x_inv_wp alternativeE_wp crunch_wps unless_wp - simp: detype_def crunch_simps validE_E_def) + (wp: mapM_x_wp' mapME_x_inv_wp crunch_wps unless_wp + simp: detype_def crunch_simps validE_E_def) lemma invoke_untyped_wp: "\ K (default_object nt ts minBound = Some obj \ nt \ UntypedType @@ -416,7 +416,7 @@ lemma decode_untyped_invocation_rvu: get_index_def throw_on_none_def decode_untyped_invocation_def mapME_x_singleton) apply (rule hoare_pre) - apply (wp alternativeE_wp unlessE_wp + apply (wp unlessE_wp lookup_slot_for_cnode_op_rvu' | wpc | clarsimp)+ done @@ -439,17 +439,13 @@ abbreviation (input) "retype_with_kids uinv \ (case uinv of (InvokeUntyped (Retype uref nt ts dest has_kids n)) \ has_kids)" -crunch cdt[wp]: retype_region "\s. P (cdl_cdt s)" -(wp:select_wp simp:crunch_simps corrupt_intents_def) - -crunch has_children[wp]: retype_region "has_children slot" -(wp:select_wp simp:crunch_simps corrupt_intents_def simp:has_children_def is_cdt_parent_def) - -crunch cdt[wp]: update_available_range "\s. P (cdl_cdt s)" -(wp:select_wp simp:crunch_simps corrupt_intents_def) +crunches retype_region, update_available_range + for cdt[wp]: "\s. P (cdl_cdt s)" + (simp: crunch_simps corrupt_intents_def) -crunch has_children[wp]: update_available_range "has_children slot" -(wp:select_wp simp:crunch_simps corrupt_intents_def simp:has_children_def is_cdt_parent_def) +crunches retype_region, update_available_range + for has_children[wp]: "has_children slot" + (simp: crunch_simps corrupt_intents_def has_children_def is_cdt_parent_def) lemma invoke_untyped_one_has_children: "uinv = (Retype uref nt ts [slot] has_kids (Suc 0)) @@ -484,7 +480,7 @@ lemma invoke_untyped_exception: apply (rule hoare_name_pre_stateE) apply (cases uinv) apply clarsimp - apply (wp unlessE_wp alternative_wp + apply (wp unlessE_wp | wpc | simp add: reset_untyped_cap_def)+ apply (rule_tac P = "available_range cap = cap_objects cap" in hoare_gen_asmEx) apply (simp add: whenE_def) @@ -537,14 +533,9 @@ lemma mark_tcb_intent_error_has_children[wp]: by (wpsimp simp: has_children_def is_cdt_parent_def mark_tcb_intent_error_def update_thread_def set_object_def) -crunch cdt[wp]: corrupt_frame "\s. P (cdl_cdt s)" -(wp:select_wp simp:crunch_simps corrupt_intents_def) - -crunch cdt[wp]: corrupt_tcb_intent "\s. P (cdl_cdt s)" -(wp:select_wp simp:crunch_simps corrupt_intents_def) - -crunch cdt[wp]: corrupt_ipc_buffer "\s. P (cdl_cdt s)" -(wp:select_wp simp:crunch_simps corrupt_intents_def) +crunches corrupt_frame, corrupt_tcb_intent, corrupt_ipc_buffer + for cdt[wp]: "\s. P (cdl_cdt s)" + (simp: crunch_simps corrupt_intents_def) lemma corrupt_ipc_buffer_has_children[wp]: "\\s. P (has_children ptr s)\ @@ -703,10 +694,10 @@ lemma seL4_Untyped_Retype_sep: **********************************************************************) crunch cdt_inc[wp]: schedule "\s. cdl_cdt s child = parent" -(wp:select_wp alternative_wp crunch_wps simp:crunch_simps) + (wp: crunch_wps simp: crunch_simps) crunch cdt_inc[wp]: handle_pending_interrupts "\s. cdl_cdt s child = parent" -(wp:select_wp alternative_wp simp:crunch_simps) + (wp: simp: crunch_simps) lemmas gets_the_resolve_cap_sym = gets_the_resolve_cap[symmetric] @@ -795,7 +786,7 @@ lemma invoke_untyped_cdt_inc[wp]: apply (simp add: reset_untyped_cap_def validE_def sum.case_eq_if) apply (rule_tac Q = "\r s. cdl_cdt s child = Some parent" in hoare_post_imp) apply simp - apply (wp whenE_wp alternativeE_wp mapME_x_inv_wp select_wp | simp)+ + apply (wp whenE_wp mapME_x_inv_wp | simp)+ apply (clarsimp simp:detype_def) done @@ -839,10 +830,9 @@ lemma lookup_cap_rvu': done crunch cdl_current_thread [wp]: handle_pending_interrupts "\s. P (cdl_current_thread s)" -(wp: alternative_wp select_wp) crunch cdl_current_thread [wp]: lookup_cap "\s. P (cdl_current_thread s)" -(wp: alternative_wp select_wp hoare_drop_imps) + (wp: hoare_drop_imps) lemma throw_opt_wp_valid: "\P\ throw_opt err x \\r. P\" @@ -891,10 +881,10 @@ lemma corrupt_intents_no_pending: done crunch no_pending[wp]: corrupt_ipc_buffer no_pending - (wp: crunch_wps select_wp update_thread_no_pending corrupt_intents_no_pending) + (wp: crunch_wps update_thread_no_pending corrupt_intents_no_pending) crunch no_pending[wp]: mark_tcb_intent_error no_pending - (wp: crunch_wps select_wp update_thread_no_pending corrupt_intents_no_pending) + (wp: crunch_wps update_thread_no_pending corrupt_intents_no_pending) lemma detype_one_wp: "o - \* R> s @@ -955,11 +945,11 @@ lemma invoke_untyped_preempt: sep_map_set_conj sep_any_map_o obj_range \* Q) s\" apply (simp add: invoke_untyped_def) apply (wp unlessE_wp) - apply (simp add: reset_untyped_cap_def whenE_liftE | wp whenE_wp alternative_wp)+ + apply (simp add: reset_untyped_cap_def whenE_liftE | wp whenE_wp)+ apply (rule_tac P = "\a. cap = UntypedCap dev obj_range a" in hoare_gen_asmEx) apply (rule hoare_post_impErr[where E = E and F = E for E]) apply (rule mapME_x_inv_wp[where P = P and E = "\r. P" for P]) - apply (wp alternative_wp) + apply wp apply simp apply (wp hoare_vcg_ex_lift) apply (rule hoare_post_imp[OF _ set_cap_wp]) @@ -969,7 +959,7 @@ lemma invoke_untyped_preempt: apply sep_solve apply simp apply simp - apply (wp select_wp)+ + apply wp+ apply clarsimp apply (frule opt_cap_sep_imp) apply (clarsimp dest!: reset_cap_asid_untyped_cap_eqD) @@ -1004,14 +994,13 @@ lemma set_parent_cdl_parent: done crunch cdl_parent[wp]: reset_untyped_cap "\s. cdl_cdt s slot = Some parent" - (wp: assert_inv crunch_wps select_wp mapME_x_inv_wp alternative_wp -simp: crunch_simps detype_def) + (wp: assert_inv crunch_wps mapME_x_inv_wp + simp: crunch_simps detype_def) crunch cdl_parent[wp]: insert_cap_child, corrupt_ipc_buffer, corrupt_tcb_intent, update_thread, derive_cap, insert_cap_sibling "\s. cdl_cdt s slot = Some parent" - (wp: crunch_wps select_wp set_parent_cdl_parent simp: crunch_simps -corrupt_intents_def) + (wp: crunch_wps set_parent_cdl_parent simp: crunch_simps corrupt_intents_def) lemma transfer_caps_loop_cdl_parent: "\\s. cdl_cdt s slot = Some parent\ @@ -1019,7 +1008,7 @@ lemma transfer_caps_loop_cdl_parent: \\_ s. cdl_cdt s slot = Some parent\" apply (induct caps arbitrary: dest; clarsimp split del: if_split) apply (rule hoare_pre) - apply (wp alternative_wp crunch_wps | assumption + apply (wp crunch_wps | assumption | simp add: crunch_simps split del: if_split)+ done @@ -1053,7 +1042,7 @@ lemma set_cap_no_pending[wp]: \no_pending\ set_cap slot cap \\rv s. no_pending s\" apply (simp add: set_cap_def) apply (cases slot, simp) - apply (wp set_object_no_pending select_wp | wpc | simp add: no_pending_def)+ + apply (wp set_object_no_pending | wpc | simp add: no_pending_def)+ apply (drule_tac x = a in spec) apply (rule conjI) apply (clarsimp simp: tcb_pending_op_slot_def tcb_ipcbuffer_slot_def) @@ -1103,9 +1092,8 @@ lemma reset_untyped_cap_no_pending[wp]: "\no_pending \ reset_untyped_cap cref \\rv. no_pending\" apply (simp add: reset_untyped_cap_def) apply (wp whenE_wp) - apply (rule_tac P = "snd cref = tcb_pending_op_slot \ \ is_pending_cap cap" in hoare_gen_asmEx) - apply (wp mapME_x_inv_wp alternativeE_wp | simp)+ - apply (wp select_wp)+ + apply (rule_tac P = "snd cref = tcb_pending_op_slot \ \ is_pending_cap cap" in hoare_gen_asmEx) + apply (wp mapME_x_inv_wp | simp)+ apply (clarsimp simp: detype_no_pending) apply (cases cref, clarsimp simp: no_pending_def) done @@ -1158,9 +1146,9 @@ lemma reset_untyped_cap_not_pending_cap[wp]: apply (simp add: reset_untyped_cap_def) apply (wp whenE_wp) apply (rule_tac P = " \ is_pending_cap cap" in hoare_gen_asmEx) - apply (wp mapME_x_inv_wp alternativeE_wp set_cap_opt_cap)+ + apply (wp mapME_x_inv_wp set_cap_opt_cap)+ apply simp - apply (wp select_wp)+ + apply wp+ apply (clarsimp simp: detype_no_pending) apply (cases cref) apply (clarsimp simp: detype_def opt_cap_def slots_of_def object_slots_def @@ -1172,11 +1160,10 @@ lemma invoke_untyped_no_pending[wp]: invoke_untyped (Retype ref a b c d e) \\rv. no_pending\" apply (simp add: invoke_untyped_def create_cap_def) - apply (wpsimp wp: mapM_x_wp' set_cap_no_pending_asm_in_pre get_cap_wp select_wp - simp: update_available_range_def - )+ + apply (wpsimp wp: mapM_x_wp' set_cap_no_pending_asm_in_pre get_cap_wp + simp: update_available_range_def) apply (wp (once) hoare_drop_imps) - apply (wpsimp split_del: if_split)+ + apply (wpsimp split_del: if_split)+ apply (rule_tac Q' = "\r s. no_pending s \ ((\y. opt_cap ref s = Some y) \ \ is_pending_cap (the (opt_cap ref s)))" in hoare_post_imp_R) apply (wp reset_untyped_cap_no_pending) diff --git a/proof/capDL-api/TCB_DP.thy b/proof/capDL-api/TCB_DP.thy index d8f5d39461..23436c7afa 100644 --- a/proof/capDL-api/TCB_DP.thy +++ b/proof/capDL-api/TCB_DP.thy @@ -51,7 +51,7 @@ lemma restart_wp: restart tcb \\_. < (tcb,tcb_pending_op_slot) \c cap \* R > \" apply (clarsimp simp: restart_def) - apply (wp alternative_wp) + apply wp apply (wp set_cap_wp[sep_wand_wp])+ apply (clarsimp) apply (rule hoare_pre_cont) @@ -70,7 +70,7 @@ lemma invoke_tcb_write: invoke_tcb (WriteRegisters tcb x y z) \\_. < (tcb,tcb_pending_op_slot) \c cap \* R >\" apply (clarsimp simp: invoke_tcb_def) - apply (wp alternative_wp restart_wp | simp)+ + apply (wp restart_wp | simp)+ done lemma not_memory_cap_reset_asid: @@ -93,16 +93,15 @@ lemma tcb_update_thread_slot_wp: apply (clarsimp simp: tcb_update_thread_slot_def) apply (rule hoare_name_pre_state) apply (clarsimp) - apply (wp) - apply (wp alternative_wp) - apply (wp insert_cap_child_wp) - apply (wp insert_cap_sibling_wp get_cap_rv)+ + apply wp + apply (wp insert_cap_child_wp) + apply (wp insert_cap_sibling_wp get_cap_rv)+ apply (safe) apply (sep_solve) apply (drule not_memory_cap_reset_asid') apply (clarsimp simp: is_memory_cap_def split:cdl_cap.splits) apply (clarsimp) -done + done lemma tcb_empty_thread_slot_wp: "\<(target_tcb,slot) \c NullCap \* R>\ tcb_empty_thread_slot target_tcb slot \\_. <(target_tcb,slot) \c NullCap \* R>\ " apply (simp add:tcb_empty_thread_slot_def whenE_def | wp)+ @@ -330,7 +329,7 @@ lemma decode_tcb_invocation_wp[wp]: decode_tcb_invocation cap cap_ref caps (TcbConfigureIntent fault_ep cspace_root_data vspace_root_data buffer) \\_. P\, \\_. P\" apply (clarsimp simp: decode_tcb_invocation_def) - apply (wp alternative_wp) + apply wp apply (clarsimp) done @@ -356,7 +355,7 @@ lemma decode_invocation_tcb_rv': decode_tcb_invocation cap cap_ref caps (TcbConfigureIntent fault_ep cspace_root_data vspace_root_data buffer) \P\, -" apply (clarsimp simp: decode_tcb_invocation_def) - apply (wp alternativeE_R_wp) + apply wp apply (wp throw_on_none_rvR)+ apply (safe) apply (clarsimp simp: get_index_def) @@ -474,7 +473,7 @@ lemma tcb_update_vspace_root_inv: tcb_update_vspace_root a b c \\_ s. P (cdl_current_thread s)\" apply (clarsimp simp: tcb_update_vspace_root_def) - apply (wp hoare_drop_imps whenE_wp alternative_wp + apply (wp hoare_drop_imps whenE_wp | simp add: tcb_update_vspace_root_def tcb_update_thread_slot_def)+ apply (wp tcb_empty_thread_slot_wp_inv) apply auto @@ -486,7 +485,7 @@ lemma tcb_update_cspace_root_inv: tcb_update_cspace_root a b c \\_ s. P (cdl_current_thread s)\" apply (clarsimp simp: tcb_update_cspace_root_def) - apply (wp hoare_drop_imps whenE_wp alternative_wp + apply (wp hoare_drop_imps whenE_wp | simp add: tcb_update_vspace_root_def tcb_update_thread_slot_def)+ apply (wp tcb_empty_thread_slot_wp_inv) apply auto @@ -497,7 +496,7 @@ lemma tcb_update_ipc_buffer_inv: tcb_update_ipc_buffer a b c \\_ s. P (cdl_current_thread s)\" apply (clarsimp simp: tcb_update_ipc_buffer_def) - apply (wp hoare_drop_imps whenE_wp alternative_wp + apply (wp hoare_drop_imps whenE_wp | simp add: tcb_update_vspace_root_def tcb_update_thread_slot_def)+ apply (wp tcb_empty_thread_slot_wp_inv) apply auto @@ -516,7 +515,7 @@ lemma invoke_tcb_ThreadControl_cur_thread: \\_ s. P (cdl_current_thread s) \" including no_pre apply (simp add:invoke_tcb_def comp_def) - apply (wp alternative_wp whenE_wp + apply (wp whenE_wp tcb_empty_thread_slot_wp_inv [where R = "(target_tcb, tcb_vspace_slot) \c - \* (target_tcb,tcb_cspace_slot) \c - @@ -527,7 +526,7 @@ lemma invoke_tcb_ThreadControl_cur_thread: apply (clarsimp simp:conj_comms) apply (rule hoare_post_impErr[OF valid_validE,rotated],assumption) apply (fastforce split:option.splits) - apply (wp hoare_drop_imps whenE_wp alternative_wp + apply (wp hoare_drop_imps whenE_wp | simp add: tcb_update_vspace_root_def tcb_update_thread_slot_def)+ apply (rule hoare_post_imp[OF _ insert_cap_child_wp]) apply (sep_erule_concl refl_imp sep_any_imp, assumption) @@ -553,7 +552,7 @@ lemma invoke_tcb_ThreadControl_cur_thread: apply (wp tcb_empty_thread_slot_wp_inv) apply clarsimp apply (sep_solve) - apply (wp hoare_drop_imps whenE_wp alternative_wp + apply (wp hoare_drop_imps whenE_wp | simp add: tcb_update_vspace_root_def tcb_update_thread_slot_def)+ apply (rule hoare_post_imp[OF _ insert_cap_child_wp]) apply (sep_select 2) @@ -591,7 +590,7 @@ lemma invoke_tcb_ThreadControl_cur_thread: " in hoare_post_impErr[rotated -1]) apply assumption apply (wp whenE_wp |wpc|simp add:tcb_update_cspace_root_def)+ - apply (wp hoare_drop_imps whenE_wp alternative_wp + apply (wp hoare_drop_imps whenE_wp | simp add: tcb_update_vspace_root_def tcb_update_thread_slot_def)+ apply (rule hoare_post_imp[OF _ insert_cap_child_wp]) apply (sep_schem) @@ -660,7 +659,7 @@ lemma decode_tcb_invocation_current_thread_inv[wp]: (TcbConfigureIntent fault_ep cspace_root_data vspace_root_data buffer_addr) \\_ s. P (cdl_current_thread s)\" apply (clarsimp simp: decode_tcb_invocation_def) - apply (wp alternative_wp) + apply wp apply (safe) done @@ -782,7 +781,7 @@ lemma invoke_tcb_ThreadControl_cdl_current_domain: \ invoke_tcb (ThreadControl target_tcb tcb_cap_slot faultep croot vroot ipc_buffer) \\_ s. P (cdl_current_domain s) \" apply (simp add:invoke_tcb_def comp_def) - apply (wp alternative_wp whenE_wp + apply (wp whenE_wp tcb_empty_thread_slot_wp_inv [where R = "(target_tcb, tcb_vspace_slot) \c - \* (target_tcb,tcb_cspace_slot) \c - @@ -793,7 +792,7 @@ lemma invoke_tcb_ThreadControl_cdl_current_domain: apply (clarsimp simp:conj_comms) apply (rule hoare_post_impErr[OF valid_validE,rotated],assumption) apply (fastforce split:option.splits) - apply (wp hoare_drop_imps whenE_wp alternative_wp + apply (wp hoare_drop_imps whenE_wp | simp add: tcb_update_vspace_root_def tcb_update_thread_slot_def)+ apply (rule hoare_post_imp[OF _ insert_cap_child_wp]) apply (sep_schem) @@ -818,7 +817,7 @@ lemma invoke_tcb_ThreadControl_cdl_current_domain: apply (wp tcb_empty_thread_slot_wp_inv) apply clarsimp apply (sep_solve) - apply (wp hoare_drop_imps whenE_wp alternative_wp + apply (wp hoare_drop_imps whenE_wp | simp add: tcb_update_vspace_root_def tcb_update_thread_slot_def)+ apply (rule hoare_post_imp[OF _ insert_cap_child_wp]) apply (sep_select 2) @@ -856,7 +855,7 @@ lemma invoke_tcb_ThreadControl_cdl_current_domain: " in hoare_post_impErr[rotated -1]) apply assumption apply (wp whenE_wp |wpc|simp add:tcb_update_cspace_root_def)+ - apply (wp hoare_drop_imps whenE_wp alternative_wp + apply (wp hoare_drop_imps whenE_wp | simp add: tcb_update_vspace_root_def tcb_update_thread_slot_def)+ apply (rule hoare_post_imp[OF _ insert_cap_child_wp]) apply (sep_select 2) @@ -1167,7 +1166,7 @@ lemma restart_cdl_current_domain: "\\s. <(ptr,tcb_pending_op_slot) \c cap \* \ > s \ \ is_pending_cap cap \ P (cdl_current_domain s)\ restart ptr \\r s. P (cdl_current_domain s)\" apply (simp add:restart_def) - apply (wp alternative_wp) + apply wp apply (simp add:cancel_ipc_def) apply (wpsimp wp: hoare_pre_cont[where f="revoke_cap_simple sl" for sl])+ apply (drule opt_cap_sep_imp) @@ -1180,7 +1179,7 @@ lemma restart_cdl_current_thread: "\\s. <(ptr,tcb_pending_op_slot) \c cap \* \ > s \ \ is_pending_cap cap \ P (cdl_current_thread s)\ restart ptr \\r s. P (cdl_current_thread s)\" apply (simp add:restart_def) - apply (wp alternative_wp) + apply wp apply (simp add:cancel_ipc_def) apply (wpsimp wp: hoare_pre_cont[where f="revoke_cap_simple sl" for sl])+ apply (drule opt_cap_sep_imp) @@ -1244,8 +1243,6 @@ lemma seL4_TCB_WriteRegisters_wp: apply (simp add: decode_invocation_def throw_opt_def get_tcb_intent_def decode_tcb_invocation_def) apply wp - apply (rule alternativeE_wp) - apply (wp+)[2] apply (clarsimp simp:conj_comms lookup_extra_caps_def mapME_def sequenceE_def) apply (rule returnOk_wp) @@ -1335,8 +1332,6 @@ lemma seL4_TCB_Resume_wp: apply (simp add: decode_invocation_def throw_opt_def get_tcb_intent_def decode_tcb_invocation_def) apply wp - apply (rule alternativeE_wp) - apply (wp+)[2] apply (clarsimp simp: lookup_extra_caps_def mapME_def sequenceE_def) apply (rule returnOk_wp) apply (rule lookup_cap_and_slot_rvu diff --git a/proof/crefine/ARM/Refine_C.thy b/proof/crefine/ARM/Refine_C.thy index 44ab2394ec..8b51f7be0b 100644 --- a/proof/crefine/ARM/Refine_C.thy +++ b/proof/crefine/ARM/Refine_C.thy @@ -935,7 +935,7 @@ lemma do_user_op_corres_C: apply (rule corres_split[OF user_memory_update_corres_C]) apply (rule corres_split[OF device_update_corres_C, where R="\\" and R'="\\"]) - apply (wp select_wp | simp)+ + apply (wp | simp)+ apply (intro conjI allI ballI impI) apply ((clarsimp simp add: invs'_def valid_state'_def valid_pspace'_def)+)[5] apply (clarsimp simp: ex_abs_def restrict_map_def diff --git a/proof/crefine/ARM/Syscall_C.thy b/proof/crefine/ARM/Syscall_C.thy index 99f8eb0707..cdd7f8c900 100644 --- a/proof/crefine/ARM/Syscall_C.thy +++ b/proof/crefine/ARM/Syscall_C.thy @@ -880,8 +880,7 @@ lemma handleInvocation_ccorres: apply (rule_tac Q="\rv'. invs' and tcb_at' rv" and E="\ft. invs' and tcb_at' rv" in hoare_post_impErr) - apply (wp hoare_split_bind_case_sumE - alternative_wp hoare_drop_imps + apply (wp hoare_split_bind_case_sumE hoare_drop_imps setThreadState_nonqueued_state_update ct_in_state'_set setThreadState_st_tcb hoare_vcg_all_lift sts_ksQ' diff --git a/proof/crefine/ARM_HYP/Refine_C.thy b/proof/crefine/ARM_HYP/Refine_C.thy index cee909bd6e..12797423de 100644 --- a/proof/crefine/ARM_HYP/Refine_C.thy +++ b/proof/crefine/ARM_HYP/Refine_C.thy @@ -951,7 +951,7 @@ lemma do_user_op_corres_C: apply (rule corres_split[OF user_memory_update_corres_C]) apply (rule corres_split[OF device_update_corres_C, where R="\\" and R'="\\"]) - apply (wp select_wp | simp)+ + apply (wp | simp)+ apply (intro conjI allI ballI impI) apply ((clarsimp simp add: invs'_def valid_state'_def valid_pspace'_def)+)[5] apply (clarsimp simp: ex_abs_def restrict_map_def diff --git a/proof/crefine/ARM_HYP/Syscall_C.thy b/proof/crefine/ARM_HYP/Syscall_C.thy index 8096d9e357..142feb4946 100644 --- a/proof/crefine/ARM_HYP/Syscall_C.thy +++ b/proof/crefine/ARM_HYP/Syscall_C.thy @@ -952,8 +952,7 @@ lemma handleInvocation_ccorres: apply (rule_tac Q="\rv'. invs' and tcb_at' rv" and E="\ft. invs' and tcb_at' rv" in hoare_post_impErr) - apply (wp hoare_split_bind_case_sumE - alternative_wp hoare_drop_imps + apply (wp hoare_split_bind_case_sumE hoare_drop_imps setThreadState_nonqueued_state_update ct_in_state'_set setThreadState_st_tcb hoare_vcg_all_lift sts_ksQ' diff --git a/proof/crefine/RISCV64/ArchMove_C.thy b/proof/crefine/RISCV64/ArchMove_C.thy index 87f974705f..a73eae0e85 100644 --- a/proof/crefine/RISCV64/ArchMove_C.thy +++ b/proof/crefine/RISCV64/ArchMove_C.thy @@ -343,8 +343,7 @@ lemma asid_shiftr_low_bits_less[simplified]: lemma getActiveIRQ_neq_Some0x3FF': "\\\ getActiveIRQ in_kernel \\rv s. rv \ Some 0x3FF\" apply (simp add: getActiveIRQ_def) - apply (wp alternative_wp select_wp) - apply simp + apply wpsimp done lemma getActiveIRQ_neq_Some0x3FF: diff --git a/proof/crefine/RISCV64/Refine_C.thy b/proof/crefine/RISCV64/Refine_C.thy index dad7c4e397..5d1f75c3ff 100644 --- a/proof/crefine/RISCV64/Refine_C.thy +++ b/proof/crefine/RISCV64/Refine_C.thy @@ -917,7 +917,7 @@ lemma do_user_op_corres_C: apply (rule corres_split[OF user_memory_update_corres_C]) apply (rule corres_split[OF device_update_corres_C, where R="\\" and R'="\\"]) - apply (wp select_wp | simp)+ + apply (wp | simp)+ apply (intro conjI allI ballI impI) apply ((clarsimp simp add: invs'_def valid_state'_def valid_pspace'_def)+)[5] apply (clarsimp simp: ex_abs_def restrict_map_def diff --git a/proof/crefine/RISCV64/Syscall_C.thy b/proof/crefine/RISCV64/Syscall_C.thy index a3c20082d6..f6235180a6 100644 --- a/proof/crefine/RISCV64/Syscall_C.thy +++ b/proof/crefine/RISCV64/Syscall_C.thy @@ -894,8 +894,7 @@ lemma handleInvocation_ccorres: apply (rule_tac Q="\rv'. invs' and tcb_at' rv" and E="\ft. invs' and tcb_at' rv" in hoare_post_impErr) - apply (wp hoare_split_bind_case_sumE - alternative_wp hoare_drop_imps + apply (wp hoare_split_bind_case_sumE hoare_drop_imps setThreadState_nonqueued_state_update ct_in_state'_set setThreadState_st_tcb hoare_vcg_all_lift sts_ksQ' diff --git a/proof/crefine/X64/Refine_C.thy b/proof/crefine/X64/Refine_C.thy index ad059c8cfa..d258ccf71f 100644 --- a/proof/crefine/X64/Refine_C.thy +++ b/proof/crefine/X64/Refine_C.thy @@ -917,7 +917,7 @@ lemma do_user_op_corres_C: apply (rule corres_split[OF user_memory_update_corres_C]) apply (rule corres_split[OF device_update_corres_C, where R="\\" and R'="\\"]) - apply (wp select_wp | simp)+ + apply (wp | simp)+ apply (intro conjI allI ballI impI) apply ((clarsimp simp add: invs'_def valid_state'_def valid_pspace'_def)+)[5] apply (clarsimp simp: ex_abs_def restrict_map_def diff --git a/proof/crefine/X64/Syscall_C.thy b/proof/crefine/X64/Syscall_C.thy index f3d3004b31..e2ddf59ee8 100644 --- a/proof/crefine/X64/Syscall_C.thy +++ b/proof/crefine/X64/Syscall_C.thy @@ -891,8 +891,7 @@ lemma handleInvocation_ccorres: apply (rule_tac Q="\rv'. invs' and tcb_at' rv" and E="\ft. invs' and tcb_at' rv" in hoare_post_impErr) - apply (wp hoare_split_bind_case_sumE - alternative_wp hoare_drop_imps + apply (wp hoare_split_bind_case_sumE hoare_drop_imps setThreadState_nonqueued_state_update ct_in_state'_set setThreadState_st_tcb hoare_vcg_all_lift sts_ksQ' diff --git a/proof/crefine/lib/AutoCorresModifiesProofs.thy b/proof/crefine/lib/AutoCorresModifiesProofs.thy index 1ae3af10be..1e10f1c320 100644 --- a/proof/crefine/lib/AutoCorresModifiesProofs.thy +++ b/proof/crefine/lib/AutoCorresModifiesProofs.thy @@ -32,7 +32,7 @@ text \ (via L1_call_simpl), so the limitations of ac_corres do not apply. \ lemma autocorres_modifies_transfer: - notes select_wp[wp] hoare_seq_ext[wp] + notes hoare_seq_ext[wp] fixes \ globals f' f_'proc modifies_eqn P xf assumes f'_def: "f' \ AC_call_L1 P globals xf (L1_call_simpl check_termination \ f_'proc)" assumes f_modifies: "\\. \\\<^bsub>/UNIV\<^esub> {\} Call f_'proc {t. modifies_eqn (globals t) (globals \)}" diff --git a/proof/crefine/lib/AutoCorres_C.thy b/proof/crefine/lib/AutoCorres_C.thy index ed98d6e934..6b3f6b7abf 100644 --- a/proof/crefine/lib/AutoCorres_C.thy +++ b/proof/crefine/lib/AutoCorres_C.thy @@ -921,7 +921,7 @@ lemma terminates_spec_no_fail: using spec_result_Normal p_spec by simp have L1_call_simpl_no_fail: "no_fail (\s. P s s) (L1_call_simpl check_termination \ f_'proc)" - apply (wpsimp simp: L1_call_simpl_def wp: no_fail_select select_wp) + apply (wpsimp simp: L1_call_simpl_def wp: no_fail_select) using terminates normal by auto have select_f_L1_call_simpl_no_fail: "\s. no_fail (\_. P s s) (select_f (L1_call_simpl check_termination \ f_'proc s))" @@ -937,7 +937,7 @@ lemma terminates_spec_no_fail: apply (wpsimp wp: select_f_L1_call_simpl_no_fail no_fail_select wp_del: select_f_wp) apply (rule hoare_strengthen_post[OF select_f_L1_call_simpl_rv], fastforce) - apply (wpsimp wp: select_wp nf_pre)+ + apply (wpsimp wp: nf_pre)+ done qed diff --git a/proof/drefine/Arch_DR.thy b/proof/drefine/Arch_DR.thy index 85ddf58a12..49d55c95a9 100644 --- a/proof/drefine/Arch_DR.thy +++ b/proof/drefine/Arch_DR.thy @@ -363,7 +363,7 @@ proof - apply (clarsimp simp add: corres_alternate2 split: ARM_A.pde.split) apply (rule corres_alternate1) apply (rule corres_from_rdonly, simp_all)[1] - apply (wp select_wp | simp)+ + apply (wp | simp)+ apply (simp add: returnOk_def in_monad select_def, wp) apply (clarsimp simp: transform_pt_slot_ref_def all_pd_pt_slots_def opt_object_page_directory @@ -409,7 +409,7 @@ proof - apply (rename_tac word1 set word2) apply (rule corres_alternate1) apply (rule corres_from_rdonly, simp_all)[1] - apply (wp select_wp | simp)+ + apply (wp | simp)+ apply (simp add: returnOk_def in_monad select_def, wp) apply (clarsimp simp: pd_aligned obj_at_def lookup_pd_slot_pd a_type_simps) @@ -458,7 +458,7 @@ proof - lookup_error_injection dc_def[symmetric]) apply (rule corres_alternate1) apply (rule corres_from_rdonly, simp_all)[1] - apply (wp select_wp | simp)+ + apply (wp | simp)+ apply (simp add: returnOk_def in_monad select_def, wp) apply (clarsimp simp: transform_pde_def obj_at_def opt_object_page_directory @@ -477,7 +477,7 @@ proof - lookup_error_injection dc_def[symmetric]) apply (rule corres_alternate1) apply (rule corres_from_rdonly, simp_all)[1] - apply (wp select_wp | simp)+ + apply (wp | simp)+ apply (simp add: returnOk_def in_monad select_def, wp) apply (clarsimp simp: transform_pde_def obj_at_def opt_object_page_directory @@ -557,7 +557,6 @@ lemma select_ret_or_throw_twiceE: done crunch inv[wp]: select_ret_or_throw "P" - (wp: select_wp) lemma corres_initial_bindE_rdonly_select_ret_or_throw: assumes y: "\rv'. corres_underlying sr nf nf' (e \ r) P P' (select_ret_or_throw S X) (d rv')" @@ -659,7 +658,7 @@ proof (induct x) apply (rule ucast_up_inj[where 'b=32]) apply (simp add: ucast_ucast_mask is_aligned_mask asid_low_bits_def) apply simp - apply (wp select_wp | simp add:valid_cap_def split del: if_split)+ + apply (wp | simp add:valid_cap_def split del: if_split)+ done next case ASIDControlCap @@ -737,7 +736,7 @@ next apply (rule less_trans) apply simp apply simp - apply (wp lsfco_not_idle select_inv select_wp | simp)+ + apply (wp lsfco_not_idle select_inv | simp)+ apply (simp add: cte_wp_at_caps_of_state neq_Nil_conv invs_mdb_cte mdb_cte_at_rewrite) apply auto done @@ -948,7 +947,7 @@ next corres_alternate2) apply (rule corres_alternate1) apply (rule corres_from_rdonly,simp_all)[1] - apply (wp select_wp | simp)+ + apply (wp | simp)+ apply (simp add: returnOk_def, wp) apply (clarsimp simp: in_monad select_def arch_invocation_relation_def translate_arch_invocation_def transform_page_table_inv_def @@ -1105,7 +1104,7 @@ lemma set_cap_opt_cap': apply (rule hoare_seq_ext [OF _ dget_object_sp]) apply (case_tac obj; simp add: KHeap_D.set_object_def has_slots_def update_slots_def object_slots_def split del: if_split cong: if_cong bind_cong; - wpsimp wp: select_wp) + wpsimp) by (auto elim!:rsubst[where P=P] simp: opt_cap_def slots_of_def object_slots_def) lemma set_cap_opt_cap: @@ -1206,7 +1205,7 @@ lemma invoke_page_table_corres: apply clarsimp apply (wp store_pte_cte_wp_at) apply fastforce - apply (wp hoare_post_taut)+ + apply wpsimp+ apply (rule_tac Q="\rv s. invs s \ valid_etcbs s \ a \ idle_thread s \ cte_wp_at \ (a,b) s \ caps_of_state s' = caps_of_state s" in hoare_strengthen_post) apply wp diff --git a/proof/drefine/CNode_DR.thy b/proof/drefine/CNode_DR.thy index 0845255a68..fdb277d77f 100644 --- a/proof/drefine/CNode_DR.thy +++ b/proof/drefine/CNode_DR.thy @@ -756,7 +756,7 @@ lemma cap_revoke_corres_helper: apply (erule cte_wp_at_weakenE, simp) apply (simp,blast) apply simp+ - apply (wp select_wp,(clarsimp simp: select_ext_def in_monad)+) + apply (wp, (clarsimp simp: select_ext_def in_monad)+) apply (rule dcorres_expand_pfx) apply (rule_tac r'="\cap cap'. cap = transform_cap cap'" and Q ="\r. \" and Q'="\r s. cte_wp_at (\x. x = r) (aa,ba) s \ s = sfix" in corres_split_forwards') @@ -792,7 +792,7 @@ lemma cap_revoke_corres_helper: in corres_split_forwards') apply (rule corres_guard_imp[OF corres_trivial[OF preemption_corres]]) apply simp+ - apply (wp alternative_wp) + apply wp apply (simp add:valid_def throwError_def return_def) apply (simp add:valid_def returnOk_def return_def) apply fastforce diff --git a/proof/drefine/Ipc_DR.thy b/proof/drefine/Ipc_DR.thy index e9fed4fa54..2023071ac2 100644 --- a/proof/drefine/Ipc_DR.thy +++ b/proof/drefine/Ipc_DR.thy @@ -794,7 +794,7 @@ lemma not_idle_after_reply_cancel_ipc: apply (simp add:cap_delete_one_def unless_def) apply wp+ apply (simp add:IpcCancel_A.empty_slot_def) - apply (wp set_cap_idle select_wp | simp add: if_apply_def2 imp_conjR + apply (wp set_cap_idle | simp add: if_apply_def2 imp_conjR | strengthen imp_consequent[where P="invs s" for s] imp_consequent[where P="valid_idle s" for s])+ apply (strengthen invs_valid_idle) apply (wp thread_set_invs_trivial | simp add: ran_tcb_cap_cases)+ diff --git a/proof/drefine/KHeap_DR.thy b/proof/drefine/KHeap_DR.thy index 408ea41880..e90af545b5 100644 --- a/proof/drefine/KHeap_DR.thy +++ b/proof/drefine/KHeap_DR.thy @@ -82,11 +82,10 @@ termination CSpace_D.resolve_address_bits end -crunch cdl_cdt [wp]: "KHeap_D.set_cap" "\s. P (cdl_cdt s)" - (wp: crunch_wps select_wp simp: crunch_simps) - -crunch cdl_cdt [wp]: "PageTableUnmap_D.cancel_all_ipc", "PageTableUnmap_D.unbind_maybe_notification" "\s. P (cdl_cdt s)" - (wp: crunch_wps select_wp simp: crunch_simps) +crunches + "KHeap_D.set_cap", "PageTableUnmap_D.cancel_all_ipc", "PageTableUnmap_D.unbind_maybe_notification" + for cdl_cdt [wp]: "\s. P (cdl_cdt s)" + (wp: crunch_wps simp: crunch_simps) lemma descendants_cdl_cdt_lift: "(\P. \\s. P (cdl_cdt s)\ f \\_ s. P (cdl_cdt s)\) \ diff --git a/proof/drefine/Schedule_DR.thy b/proof/drefine/Schedule_DR.thy index cbec79861b..2ef3fefa7d 100644 --- a/proof/drefine/Schedule_DR.thy +++ b/proof/drefine/Schedule_DR.thy @@ -139,7 +139,7 @@ lemma corrupt_intents_current_thread: by (simp add: corrupt_intents_def) crunch cdl_cur: corrupt_frame "\s. cdl_current_thread s = x" - (wp: select_wp simp: corrupt_intents_current_thread) + (simp: corrupt_intents_current_thread) (* Switching to the active thread has no effect. *) lemma switch_to_thread_idempotent_corres: diff --git a/proof/infoflow/ADT_IF.thy b/proof/infoflow/ADT_IF.thy index 2bfa4eeedd..63ef7b2f48 100644 --- a/proof/infoflow/ADT_IF.thy +++ b/proof/infoflow/ADT_IF.thy @@ -2505,7 +2505,7 @@ proof(induct rule: cap_revoke.induct[where ?a1.0=s]) apply (wp drop_spec_validE[OF preemption_point_irq_state_inv[simplified validE_R_def]] drop_spec_validE[OF preemption_point_irq_state_inv'[where irq=irq]] drop_spec_validE[OF valid_validE[OF preemption_point_domain_sep_inv]] - cap_delete_domain_sep_inv cap_delete_irq_state_inv select_wp + cap_delete_domain_sep_inv cap_delete_irq_state_inv drop_spec_validE[OF assertE_wp] drop_spec_validE[OF returnOk_wp] drop_spec_validE[OF liftE_wp] drop_spec_validE[OF hoare_vcg_conj_liftE1] | simp | wp (once) hoare_drop_imps)+ diff --git a/proof/infoflow/ARM/ArchADT_IF.thy b/proof/infoflow/ARM/ArchADT_IF.thy index 152d537534..6e0e34eb9a 100644 --- a/proof/infoflow/ARM/ArchADT_IF.thy +++ b/proof/infoflow/ARM/ArchADT_IF.thy @@ -67,7 +67,7 @@ lemma do_user_op_if_invs[ADT_IF_assms]: do_user_op_if f tc \\_. invs and ct_running\" apply (simp add: do_user_op_if_def split_def) - apply (wp do_machine_op_ct_in_state select_wp device_update_invs | wp (once) dmo_invs | simp)+ + apply (wp do_machine_op_ct_in_state device_update_invs | wp (once) dmo_invs | simp)+ apply (clarsimp simp: user_mem_def user_memory_update_def simpler_modify_def restrict_map_def invs_def cur_tcb_def ptable_rights_s_def ptable_lift_s_def) apply (frule ptable_rights_imp_frame) @@ -77,31 +77,31 @@ lemma do_user_op_if_invs[ADT_IF_assms]: done crunch domain_sep_inv[ADT_IF_assms, wp]: do_user_op_if "domain_sep_inv irqs st" - (ignore: user_memory_update wp: select_wp) + (ignore: user_memory_update) crunch valid_sched[ADT_IF_assms, wp]: do_user_op_if "valid_sched" - (ignore: user_memory_update wp: select_wp) + (ignore: user_memory_update) crunch irq_masks[ADT_IF_assms, wp]: do_user_op_if "\s. P (irq_masks_of_state s)" - (ignore: user_memory_update wp: select_wp dmo_wp no_irq) + (ignore: user_memory_update wp: dmo_wp no_irq) crunch valid_list[ADT_IF_assms, wp]: do_user_op_if "valid_list" - (ignore: user_memory_update wp: select_wp) + (ignore: user_memory_update) lemma do_user_op_if_scheduler_action[ADT_IF_assms, wp]: "do_user_op_if f tc \\s. P (scheduler_action s)\" - by (simp add: do_user_op_if_def | wp select_wp | wpc)+ + by (simp add: do_user_op_if_def | wp | wpc)+ lemma do_user_op_silc_inv[ADT_IF_assms, wp]: "do_user_op_if f tc \silc_inv aag st\" apply (simp add: do_user_op_if_def) - apply (wp select_wp | wpc | simp)+ + apply (wp | wpc | simp)+ done lemma do_user_op_pas_refined[ADT_IF_assms, wp]: "do_user_op_if f tc \pas_refined aag\" apply (simp add: do_user_op_if_def) - apply (wp select_wp | wpc | simp)+ + apply (wp | wpc | simp)+ done crunches do_user_op_if @@ -109,7 +109,7 @@ crunches do_user_op_if and cur_domain[ADT_IF_assms, wp]: "\s. P (cur_domain s)" and idle_thread[ADT_IF_assms, wp]: "\s. P (idle_thread s)" and domain_fields[ADT_IF_assms, wp]: "domain_fields P" - (wp: select_wp ignore: user_memory_update) + (ignore: user_memory_update) lemma do_use_op_guarded_pas_domain[ADT_IF_assms, wp]: "do_user_op_if f tc \guarded_pas_domain aag\" @@ -235,7 +235,7 @@ lemma do_user_op_if_idle_equiv[ADT_IF_assms, wp]: do_user_op_if uop tc \\_. idle_equiv st\" unfolding do_user_op_if_def - by (wpsimp wp: dmo_user_memory_update_idle_equiv dmo_device_memory_update_idle_equiv select_wp) + by (wpsimp wp: dmo_user_memory_update_idle_equiv dmo_device_memory_update_idle_equiv) lemma not_in_global_refs_vs_lookup: "\ (\\p) s; valid_vs_lookup s; valid_global_refs s; valid_arch_state s; valid_global_objs s \ @@ -273,7 +273,7 @@ lemma schedule_if_valid_pdpt_objs[ADT_IF_assms, wp]: lemma do_user_op_if_valid_pdpt_objs[ADT_IF_assms, wp]: "\valid_vspace_objs_if\ do_user_op_if a b \\rv s. valid_vspace_objs_if s\" - by (simp add: do_user_op_if_def | wp select_wp | wpc)+ + by (simp add: do_user_op_if_def | wp | wpc)+ lemma valid_vspace_objs_if_ms_update[ADT_IF_assms, simp]: "valid_vspace_objs_if (machine_state_update f s) = valid_vspace_objs_if s" @@ -282,20 +282,20 @@ lemma valid_vspace_objs_if_ms_update[ADT_IF_assms, simp]: lemma do_user_op_if_irq_state_of_state[ADT_IF_assms]: "do_user_op_if utf uc \\s. P (irq_state_of_state s)\" apply (rule hoare_pre) - apply (simp add: do_user_op_if_def user_memory_update_def | wp dmo_wp select_wp | wpc)+ + apply (simp add: do_user_op_if_def user_memory_update_def | wp dmo_wp | wpc)+ done lemma do_user_op_if_irq_masks_of_state[ADT_IF_assms]: "do_user_op_if utf uc \\s. P (irq_masks_of_state s)\" apply (rule hoare_pre) - apply (simp add: do_user_op_if_def user_memory_update_def | wp dmo_wp select_wp | wpc)+ + apply (simp add: do_user_op_if_def user_memory_update_def | wp dmo_wp | wpc)+ done lemma do_user_op_if_irq_measure_if[ADT_IF_assms]: "do_user_op_if utf uc \\s. P (irq_measure_if s)\" apply (rule hoare_pre) apply (simp add: do_user_op_if_def user_memory_update_def irq_measure_if_def - | wps |wp dmo_wp select_wp | wpc)+ + | wps |wp dmo_wp | wpc)+ done lemma invoke_tcb_irq_state_inv[ADT_IF_assms]: diff --git a/proof/infoflow/ARM/ArchArch_IF.thy b/proof/infoflow/ARM/ArchArch_IF.thy index 92215d8e0d..872256754b 100644 --- a/proof/infoflow/ARM/ArchArch_IF.thy +++ b/proof/infoflow/ARM/ArchArch_IF.thy @@ -76,7 +76,7 @@ crunch irq_state_of_state[wp]: arch_perform_invocation "\s. P (irq_state crunch irq_state_of_state[Arch_IF_assms, wp]: arch_finalise_cap, prepare_thread_delete "\s :: det_state. P (irq_state_of_state s)" - (wp: select_wp modify_wp crunch_wps dmo_wp + (wp: modify_wp crunch_wps dmo_wp simp: crunch_simps invalidateLocalTLB_ASID_def dsb_def cleanCaches_PoU_def invalidate_I_PoU_def clean_D_PoU_def) diff --git a/proof/infoflow/ARM/ArchDecode_IF.thy b/proof/infoflow/ARM/ArchDecode_IF.thy index 4905fef5ae..4a257da281 100644 --- a/proof/infoflow/ARM/ArchDecode_IF.thy +++ b/proof/infoflow/ARM/ArchDecode_IF.thy @@ -204,7 +204,7 @@ lemma arch_decode_invocation_reads_respects_f[Decode_IF_assms]: apply (wp check_vp_wpR reads_respects_f_inv'[OF get_asid_pool_rev] reads_respects_f_inv'[OF ensure_empty_rev] reads_respects_f_inv'[OF lookup_slot_for_cnode_op_rev] - reads_respects_f_inv'[OF ensure_no_children_rev] select_wp + reads_respects_f_inv'[OF ensure_no_children_rev] reads_respects_f_inv'[OF ensure_safe_mapping_reads_respects] reads_respects_f_inv'[OF resolve_vaddr_reads_respects] reads_respects_f_inv'[OF create_mapping_entries_rev] diff --git a/proof/infoflow/ARM/ArchIRQMasks_IF.thy b/proof/infoflow/ARM/ArchIRQMasks_IF.thy index d532b90317..0b3761e134 100644 --- a/proof/infoflow/ARM/ArchIRQMasks_IF.thy +++ b/proof/infoflow/ARM/ArchIRQMasks_IF.thy @@ -31,7 +31,7 @@ crunch irq_masks[IRQMasks_IF_assms, wp]: invoke_untyped "\s. P (irq_mask mapM_x_def_bak unless_def) crunch irq_masks[IRQMasks_IF_assms, wp]: finalise_cap "\s. P (irq_masks_of_state s)" - (wp: select_wp crunch_wps dmo_wp no_irq + (wp: crunch_wps dmo_wp no_irq simp: crunch_simps no_irq_setHardwareASID no_irq_invalidateLocalTLB_ASID no_irq_set_current_pd no_irq_invalidateLocalTLB_VAASID no_irq_cleanByVA_PoU) @@ -80,14 +80,14 @@ lemma dmo_getActiveIRQ_return_axiom[IRQMasks_IF_assms, wp]: apply (simp add: getActiveIRQ_def) apply (rule hoare_pre, rule dmo_wp) apply (insert irq_oracle_max_irq) - apply (wp alternative_wp select_wp dmo_getActiveIRQ_irq_masks) + apply (wp dmo_getActiveIRQ_irq_masks) apply clarsimp done crunch irq_masks[IRQMasks_IF_assms, wp]: activate_thread "\s. P (irq_masks_of_state s)" crunch irq_masks[IRQMasks_IF_assms, wp]: schedule "\s. P (irq_masks_of_state s)" - (wp: dmo_wp alternative_wp select_wp crunch_wps simp: crunch_simps clearExMonitor_def) + (wp: dmo_wp crunch_wps simp: crunch_simps clearExMonitor_def) end diff --git a/proof/infoflow/ARM/ArchNoninterference.thy b/proof/infoflow/ARM/ArchNoninterference.thy index e4dfcc2a17..ca5ab33ac2 100644 --- a/proof/infoflow/ARM/ArchNoninterference.thy +++ b/proof/infoflow/ARM/ArchNoninterference.thy @@ -23,9 +23,10 @@ lemma do_user_op_if_integrity[Noninterference_assms]: \\_. integrity aag X st\" apply (simp add: do_user_op_if_def) apply (wpsimp wp: dmo_user_memory_update_respects_Write dmo_device_update_respects_Write - hoare_vcg_all_lift hoare_vcg_imp_lift) + hoare_vcg_all_lift hoare_vcg_imp_lift + wp_del: select_wp) apply (rule hoare_pre_cont) - apply (wp select_wp | wpc | clarsimp)+ + apply (wp | wpc | clarsimp)+ apply (rule conjI) apply clarsimp apply (simp add: restrict_map_def ptable_lift_s_def ptable_rights_s_def split: if_splits) @@ -53,12 +54,12 @@ lemma do_user_op_if_globals_equiv_scheduler[Noninterference_assms]: \\_. globals_equiv_scheduler st\" apply (simp add: do_user_op_if_def) apply (wpsimp wp: dmo_user_memory_update_globals_equiv_scheduler - dmo_device_memory_update_globals_equiv_scheduler select_wp)+ + dmo_device_memory_update_globals_equiv_scheduler)+ apply (auto simp: ptable_lift_s_def ptable_rights_s_def) done crunch silc_dom_equiv[Noninterference_assms, wp]: do_user_op_if "silc_dom_equiv aag st" - (ignore: do_machine_op user_memory_update wp: crunch_wps select_wp) + (ignore: do_machine_op user_memory_update wp: crunch_wps) lemma sameFor_scheduler_affects_equiv[Noninterference_assms]: "\ (s,s') \ same_for aag PSched; (s,s') \ same_for aag (Partition l); @@ -350,7 +351,7 @@ lemma getActiveIRQ_ret_no_dmo[Noninterference_assms, wp]: apply (simp add: getActiveIRQ_def) apply (rule hoare_pre) apply (insert irq_oracle_max_irq) - apply (wp alternative_wp select_wp dmo_getActiveIRQ_irq_masks) + apply (wp dmo_getActiveIRQ_irq_masks) apply clarsimp done diff --git a/proof/infoflow/ARM/ArchPasUpdates.thy b/proof/infoflow/ARM/ArchPasUpdates.thy index 1c81b5482c..8f8aaaa622 100644 --- a/proof/infoflow/ARM/ArchPasUpdates.thy +++ b/proof/infoflow/ARM/ArchPasUpdates.thy @@ -14,7 +14,7 @@ named_theorems PasUpdates_assms crunches arch_post_cap_deletion, arch_finalise_cap, prepare_thread_delete for domain_fields[PasUpdates_assms, wp]: "domain_fields P" - ( wp: syscall_valid select_wp crunch_wps rec_del_preservation cap_revoke_preservation modify_wp + ( wp: syscall_valid crunch_wps rec_del_preservation cap_revoke_preservation modify_wp simp: crunch_simps check_cap_at_def filterM_mapM unless_def ignore: without_preemption filterM rec_del check_cap_at cap_revoke ignore_del: retype_region_ext create_cap_ext cap_insert_ext ethread_set cap_move_ext diff --git a/proof/infoflow/ARM/ArchSyscall_IF.thy b/proof/infoflow/ARM/ArchSyscall_IF.thy index bfaa82c626..709535dc31 100644 --- a/proof/infoflow/ARM/ArchSyscall_IF.thy +++ b/proof/infoflow/ARM/ArchSyscall_IF.thy @@ -120,7 +120,7 @@ lemma decode_arch_invocation_authorised_for_globals[Syscall_IF_assms]: apply (simp add: split_def Let_def cong: cap.case_cong arch_cap.case_cong if_cong option.case_cong split del: if_split) - apply (wp select_wp select_ext_weak_wp whenE_throwError_wp check_vp_wpR unlessE_wp get_pde_wp + apply (wp select_ext_weak_wp whenE_throwError_wp check_vp_wpR unlessE_wp get_pde_wp get_master_pde_wp find_pd_for_asid_authority3 create_mapping_entries_parent_for_refs | wpc | simp add: authorised_for_globals_page_inv_def diff --git a/proof/infoflow/ARM/ArchUserOp_IF.thy b/proof/infoflow/ARM/ArchUserOp_IF.thy index 02bf34edc7..394b5ac167 100644 --- a/proof/infoflow/ARM/ArchUserOp_IF.thy +++ b/proof/infoflow/ARM/ArchUserOp_IF.thy @@ -982,7 +982,7 @@ lemma do_user_op_reads_respects_g: apply (rule spec_equiv_valid_guard_imp) apply (wpsimp wp: dmo_user_memory_update_reads_respects_g dmo_device_state_update_reads_respects_g dmo_setExMonitor_reads_respects_g dmo_device_state_update_reads_respects_g - select_ev select_wp dmo_getExMonitor_reads_respects_g dmo_wp) + select_ev dmo_getExMonitor_reads_respects_g dmo_wp) apply clarsimp apply (rule conjI) apply clarsimp diff --git a/proof/infoflow/Arch_IF.thy b/proof/infoflow/Arch_IF.thy index 41907814de..20b15e6bf0 100644 --- a/proof/infoflow/Arch_IF.thy +++ b/proof/infoflow/Arch_IF.thy @@ -437,7 +437,7 @@ crunch irq_state_of_state[wp]: schedule "\s. P (irq_state_of_state s)" simp: machine_op_lift_def machine_rest_lift_def crunch_simps) crunch irq_state_of_state[wp]: finalise_cap "\s. P (irq_state_of_state s)" - (wp: select_wp modify_wp crunch_wps dmo_wp simp: crunch_simps) + (wp: modify_wp crunch_wps dmo_wp simp: crunch_simps) crunch irq_state_of_state[wp]: send_signal, restart "\s. P (irq_state_of_state s)" diff --git a/proof/infoflow/FinalCaps.thy b/proof/infoflow/FinalCaps.thy index 60706a9b88..5e954e5f8f 100644 --- a/proof/infoflow/FinalCaps.thy +++ b/proof/infoflow/FinalCaps.thy @@ -1208,7 +1208,7 @@ lemma reply_cancel_ipc_silc_inv: reply_cancel_ipc t \\_. silc_inv aag st\" unfolding reply_cancel_ipc_def - apply (wp cap_delete_one_silc_inv select_wp hoare_vcg_if_lift | simp)+ + apply (wp cap_delete_one_silc_inv hoare_vcg_if_lift | simp)+ apply wps apply (wp static_imp_wp hoare_vcg_all_lift hoare_vcg_ball_lift) apply clarsimp @@ -1773,7 +1773,7 @@ lemma cap_revoke_silc_inv': apply (rule spec_valid_conj_liftE1, (wp | simp)+) apply (rule drop_spec_validE[OF valid_validE[OF cap_delete_silc_inv]]) apply (wp drop_spec_validE[OF assertE_wp] drop_spec_validE[OF without_preemption_wp] - get_cap_wp select_wp drop_spec_validE[OF returnOk_wp])+ + get_cap_wp drop_spec_validE[OF returnOk_wp])+ apply clarsimp apply (clarsimp cong: conj_cong simp: conj_comms) apply (rule conjI) @@ -2856,7 +2856,7 @@ lemma handle_event_silc_inv: crunch silc_inv[wp]: activate_thread "silc_inv aag st" crunch silc_inv[wp]: schedule "silc_inv aag st" - ( wp: alternative_wp OR_choice_weak_wp select_wp crunch_wps + ( wp: OR_choice_weak_wp crunch_wps ignore: set_scheduler_action simp: crunch_simps) diff --git a/proof/infoflow/Finalise_IF.thy b/proof/infoflow/Finalise_IF.thy index 1b39733a63..de0818eeee 100644 --- a/proof/infoflow/Finalise_IF.thy +++ b/proof/infoflow/Finalise_IF.thy @@ -994,7 +994,7 @@ lemma reply_cancel_ipc_reads_respects_f: unfolding reply_cancel_ipc_def apply (rule gen_asm_ev) apply (wp cap_delete_one_reads_respects_f_transferable[where st=st] - select_singleton_ev select_inv select_wp assert_wp + select_singleton_ev select_inv assert_wp reads_respects_f[OF get_cap_rev, where st=st] reads_respects_f[OF thread_set_reads_respects, where st=st] reads_respects_f[OF gets_descendants_of_revrv[folded equiv_valid_def2]] diff --git a/proof/infoflow/IRQMasks_IF.thy b/proof/infoflow/IRQMasks_IF.thy index 897f34c316..b4eb9daa34 100644 --- a/proof/infoflow/IRQMasks_IF.thy +++ b/proof/infoflow/IRQMasks_IF.thy @@ -169,7 +169,7 @@ end crunch irq_masks[wp]: cancel_ipc "\s. P (irq_masks_of_state s)" - (wp: select_wp crunch_wps simp: crunch_simps) + (wp: crunch_wps simp: crunch_simps) crunch irq_masks[wp]: restart, set_mcpriority "\s. P (irq_masks_of_state s)" @@ -212,7 +212,7 @@ proof (induct rule: cap_revoke.induct[where ?a1.0=s]) drop_spec_validE[OF valid_validE[OF preemption_point_domain_sep_inv]] cap_delete_domain_sep_inv cap_delete_irq_masks drop_spec_validE[OF assertE_wp] drop_spec_validE[OF returnOk_wp] - drop_spec_validE[OF liftE_wp] select_wp + drop_spec_validE[OF liftE_wp] drop_spec_validE[OF hoare_vcg_conj_liftE1] | simp | wp (once) hoare_drop_imps)+ apply fastforce diff --git a/proof/infoflow/PasUpdates.thy b/proof/infoflow/PasUpdates.thy index 14b5ae3469..1d6ceed8db 100644 --- a/proof/infoflow/PasUpdates.thy +++ b/proof/infoflow/PasUpdates.thy @@ -45,7 +45,7 @@ crunch domain_fields[wp]: cap_swap_ext, set_thread_state_ext, tcb_sched_action, reschedule_required, cap_swap_for_delete, finalise_cap, cap_move, cap_swap, cap_delete, cancel_badged_sends, cap_insert "domain_fields P" - ( wp: syscall_valid select_wp crunch_wps rec_del_preservation cap_revoke_preservation modify_wp + ( wp: syscall_valid crunch_wps rec_del_preservation cap_revoke_preservation modify_wp simp: crunch_simps check_cap_at_def filterM_mapM unless_def ignore: without_preemption filterM rec_del check_cap_at cap_revoke ignore_del: retype_region_ext create_cap_ext cap_insert_ext ethread_set cap_move_ext diff --git a/proof/infoflow/RISCV64/ArchADT_IF.thy b/proof/infoflow/RISCV64/ArchADT_IF.thy index a70fe81d27..82a752388a 100644 --- a/proof/infoflow/RISCV64/ArchADT_IF.thy +++ b/proof/infoflow/RISCV64/ArchADT_IF.thy @@ -25,7 +25,7 @@ lemma do_user_op_if_invs[ADT_IF_assms]: do_user_op_if f tc \\_. invs and ct_running\" apply (simp add: do_user_op_if_def split_def) - apply (wp do_machine_op_ct_in_state select_wp device_update_invs | wp (once) dmo_invs | simp)+ + apply (wp do_machine_op_ct_in_state device_update_invs | wp (once) dmo_invs | simp)+ apply (clarsimp simp: user_mem_def user_memory_update_def simpler_modify_def restrict_map_def invs_def cur_tcb_def ptable_rights_s_def ptable_lift_s_def) apply (frule ptable_rights_imp_frame) @@ -35,31 +35,31 @@ lemma do_user_op_if_invs[ADT_IF_assms]: done crunch domain_sep_inv[ADT_IF_assms, wp]: do_user_op_if "domain_sep_inv irqs st" - (ignore: user_memory_update wp: select_wp) + (ignore: user_memory_update) crunch valid_sched[ADT_IF_assms, wp]: do_user_op_if "valid_sched" - (ignore: user_memory_update wp: select_wp) + (ignore: user_memory_update) crunch irq_masks[ADT_IF_assms, wp]: do_user_op_if "\s. P (irq_masks_of_state s)" - (ignore: user_memory_update wp: select_wp dmo_wp no_irq) + (ignore: user_memory_update wp: dmo_wp no_irq) crunch valid_list[ADT_IF_assms, wp]: do_user_op_if "valid_list" - (ignore: user_memory_update wp: select_wp) + (ignore: user_memory_update) lemma do_user_op_if_scheduler_action[ADT_IF_assms, wp]: "do_user_op_if f tc \\s. P (scheduler_action s)\" - by (simp add: do_user_op_if_def | wp select_wp | wpc)+ + by (simp add: do_user_op_if_def | wp | wpc)+ lemma do_user_op_silc_inv[ADT_IF_assms, wp]: "do_user_op_if f tc \silc_inv aag st\" apply (simp add: do_user_op_if_def) - apply (wp select_wp | wpc | simp)+ + apply (wp | wpc | simp)+ done lemma do_user_op_pas_refined[ADT_IF_assms, wp]: "do_user_op_if f tc \pas_refined aag\" apply (simp add: do_user_op_if_def) - apply (wp select_wp | wpc | simp)+ + apply (wp | wpc | simp)+ done crunches do_user_op_if @@ -67,7 +67,7 @@ crunches do_user_op_if and cur_domain[ADT_IF_assms, wp]: "\s. P (cur_domain s)" and idle_thread[ADT_IF_assms, wp]: "\s. P (idle_thread s)" and domain_fields[ADT_IF_assms, wp]: "domain_fields P" - (wp: select_wp ignore: user_memory_update) + (ignore: user_memory_update) lemma do_use_op_guarded_pas_domain[ADT_IF_assms, wp]: "do_user_op_if f tc \guarded_pas_domain aag\" @@ -187,7 +187,7 @@ lemma do_user_op_if_idle_equiv[ADT_IF_assms, wp]: do_user_op_if uop tc \\_. idle_equiv st\" unfolding do_user_op_if_def - by (wpsimp wp: dmo_user_memory_update_idle_equiv dmo_device_memory_update_idle_equiv select_wp) + by (wpsimp wp: dmo_user_memory_update_idle_equiv dmo_device_memory_update_idle_equiv) lemma kernel_entry_if_valid_vspace_objs_if[ADT_IF_assms, wp]: "\valid_vspace_objs_if and invs and (\s. e \ Interrupt \ ct_active s)\ @@ -214,20 +214,20 @@ lemma valid_vspace_objs_if_ms_update[ADT_IF_assms, simp]: lemma do_user_op_if_irq_state_of_state[ADT_IF_assms]: "do_user_op_if utf uc \\s. P (irq_state_of_state s)\" apply (rule hoare_pre) - apply (simp add: do_user_op_if_def user_memory_update_def | wp dmo_wp select_wp | wpc)+ + apply (simp add: do_user_op_if_def user_memory_update_def | wp dmo_wp | wpc)+ done lemma do_user_op_if_irq_masks_of_state[ADT_IF_assms]: "do_user_op_if utf uc \\s. P (irq_masks_of_state s)\" apply (rule hoare_pre) - apply (simp add: do_user_op_if_def user_memory_update_def | wp dmo_wp select_wp | wpc)+ + apply (simp add: do_user_op_if_def user_memory_update_def | wp dmo_wp | wpc)+ done lemma do_user_op_if_irq_measure_if[ADT_IF_assms]: "do_user_op_if utf uc \\s. P (irq_measure_if s)\" apply (rule hoare_pre) apply (simp add: do_user_op_if_def user_memory_update_def irq_measure_if_def - | wps |wp dmo_wp select_wp | wpc)+ + | wps |wp dmo_wp | wpc)+ done lemma invoke_tcb_irq_state_inv[ADT_IF_assms]: diff --git a/proof/infoflow/RISCV64/ArchArch_IF.thy b/proof/infoflow/RISCV64/ArchArch_IF.thy index 3901077868..5f2f165870 100644 --- a/proof/infoflow/RISCV64/ArchArch_IF.thy +++ b/proof/infoflow/RISCV64/ArchArch_IF.thy @@ -74,7 +74,7 @@ crunch irq_state_of_state[wp]: arch_perform_invocation "\s. P (irq_state crunch irq_state_of_state[Arch_IF_assms, wp]: arch_finalise_cap, prepare_thread_delete "\s :: det_state. P (irq_state_of_state s)" - (wp: select_wp modify_wp crunch_wps dmo_wp + (wp: modify_wp crunch_wps dmo_wp simp: crunch_simps hwASIDFlush_def) lemma equiv_asid_machine_state_update[Arch_IF_assms, simp]: diff --git a/proof/infoflow/RISCV64/ArchDecode_IF.thy b/proof/infoflow/RISCV64/ArchDecode_IF.thy index 657072fdb5..5be04e10b1 100644 --- a/proof/infoflow/RISCV64/ArchDecode_IF.thy +++ b/proof/infoflow/RISCV64/ArchDecode_IF.thy @@ -144,7 +144,7 @@ lemma decode_asid_control_invocation_reads_respects_f: apply (wp check_vp_wpR reads_respects_f_inv'[OF get_asid_pool_rev] reads_respects_f_inv'[OF ensure_empty_rev] reads_respects_f_inv'[OF lookup_slot_for_cnode_op_rev] - reads_respects_f_inv'[OF ensure_no_children_rev] select_wp + reads_respects_f_inv'[OF ensure_no_children_rev] reads_respects_f_inv'[OF lookup_error_on_failure_rev] gets_apply_ev is_final_cap_reads_respects @@ -193,7 +193,7 @@ lemma decode_frame_invocation_reads_respects_f: reads_respects_f_inv'[OF ensure_empty_rev] reads_respects_f_inv'[OF get_pte_rev] reads_respects_f_inv'[OF lookup_slot_for_cnode_op_rev] - reads_respects_f_inv'[OF ensure_no_children_rev] select_wp + reads_respects_f_inv'[OF ensure_no_children_rev] reads_respects_f_inv'[OF lookup_error_on_failure_rev] find_vspace_for_asid_reads_respects is_final_cap_reads_respects @@ -254,7 +254,7 @@ lemma decode_page_table_invocation_reads_respects_f: reads_respects_f_inv'[OF ensure_empty_rev] reads_respects_f_inv'[OF get_pte_rev] reads_respects_f_inv'[OF lookup_slot_for_cnode_op_rev] - reads_respects_f_inv'[OF ensure_no_children_rev] select_wp + reads_respects_f_inv'[OF ensure_no_children_rev] reads_respects_f_inv'[OF lookup_error_on_failure_rev] find_vspace_for_asid_reads_respects is_final_cap_reads_respects diff --git a/proof/infoflow/RISCV64/ArchIRQMasks_IF.thy b/proof/infoflow/RISCV64/ArchIRQMasks_IF.thy index 6e3ae7cd4f..e0c3ed7a98 100644 --- a/proof/infoflow/RISCV64/ArchIRQMasks_IF.thy +++ b/proof/infoflow/RISCV64/ArchIRQMasks_IF.thy @@ -30,7 +30,7 @@ crunch irq_masks[IRQMasks_IF_assms, wp]: invoke_untyped "\s. P (irq_mask simp: crunch_simps no_irq_clearMemory mapM_x_def_bak unless_def) crunch irq_masks[IRQMasks_IF_assms, wp]: finalise_cap "\s. P (irq_masks_of_state s)" - ( wp: select_wp crunch_wps dmo_wp no_irq + ( wp: crunch_wps dmo_wp no_irq simp: crunch_simps no_irq_setVSpaceRoot no_irq_hwASIDFlush) crunch irq_masks[IRQMasks_IF_assms, wp]: send_signal "\s. P (irq_masks_of_state s)" @@ -77,14 +77,14 @@ lemma dmo_getActiveIRQ_return_axiom[IRQMasks_IF_assms, wp]: apply (simp add: getActiveIRQ_def) apply (rule hoare_pre, rule dmo_wp) apply (insert irq_oracle_max_irq) - apply (wp alternative_wp select_wp dmo_getActiveIRQ_irq_masks) + apply (wp dmo_getActiveIRQ_irq_masks) apply clarsimp done crunch irq_masks[IRQMasks_IF_assms, wp]: activate_thread "\s. P (irq_masks_of_state s)" crunch irq_masks[IRQMasks_IF_assms, wp]: schedule "\s. P (irq_masks_of_state s)" - (wp: dmo_wp alternative_wp select_wp crunch_wps simp: crunch_simps) + (wp: dmo_wp crunch_wps simp: crunch_simps) end diff --git a/proof/infoflow/RISCV64/ArchNoninterference.thy b/proof/infoflow/RISCV64/ArchNoninterference.thy index dcf4c00cfc..1ccab6450b 100644 --- a/proof/infoflow/RISCV64/ArchNoninterference.thy +++ b/proof/infoflow/RISCV64/ArchNoninterference.thy @@ -19,9 +19,10 @@ lemma do_user_op_if_integrity[Noninterference_assms]: \\_. integrity aag X st\" apply (simp add: do_user_op_if_def) apply (wpsimp wp: dmo_user_memory_update_respects_Write dmo_device_update_respects_Write - hoare_vcg_all_lift hoare_vcg_imp_lift) + hoare_vcg_all_lift hoare_vcg_imp_lift + wp_del: select_wp) apply (rule hoare_pre_cont) - apply (wp select_wp | wpc | clarsimp)+ + apply (wp | wpc | clarsimp)+ apply (rule conjI) apply clarsimp apply (simp add: restrict_map_def ptable_lift_s_def ptable_rights_s_def split: if_splits) @@ -39,12 +40,12 @@ lemma do_user_op_if_globals_equiv_scheduler[Noninterference_assms]: \\_. globals_equiv_scheduler st\" apply (simp add: do_user_op_if_def) apply (wpsimp wp: dmo_user_memory_update_globals_equiv_scheduler - dmo_device_memory_update_globals_equiv_scheduler select_wp)+ + dmo_device_memory_update_globals_equiv_scheduler)+ apply (auto simp: ptable_lift_s_def ptable_rights_s_def) done crunch silc_dom_equiv[Noninterference_assms, wp]: do_user_op_if "silc_dom_equiv aag st" - (ignore: do_machine_op user_memory_update wp: crunch_wps select_wp) + (ignore: do_machine_op user_memory_update wp: crunch_wps) lemma sameFor_scheduler_affects_equiv[Noninterference_assms]: "\ (s,s') \ same_for aag PSched; (s,s') \ same_for aag (Partition l); @@ -352,7 +353,7 @@ lemma getActiveIRQ_ret_no_dmo[Noninterference_assms, wp]: apply (simp add: getActiveIRQ_def) apply (rule hoare_pre) apply (insert irq_oracle_max_irq) - apply (wp alternative_wp select_wp dmo_getActiveIRQ_irq_masks) + apply (wp dmo_getActiveIRQ_irq_masks) apply clarsimp done diff --git a/proof/infoflow/RISCV64/ArchPasUpdates.thy b/proof/infoflow/RISCV64/ArchPasUpdates.thy index a7392bebfd..f785571dc1 100644 --- a/proof/infoflow/RISCV64/ArchPasUpdates.thy +++ b/proof/infoflow/RISCV64/ArchPasUpdates.thy @@ -14,7 +14,7 @@ named_theorems PasUpdates_assms crunches arch_post_cap_deletion, arch_finalise_cap, prepare_thread_delete for domain_fields[PasUpdates_assms, wp]: "domain_fields P" - ( wp: syscall_valid select_wp crunch_wps rec_del_preservation cap_revoke_preservation modify_wp + ( wp: syscall_valid crunch_wps rec_del_preservation cap_revoke_preservation modify_wp simp: crunch_simps check_cap_at_def filterM_mapM unless_def ignore: without_preemption filterM rec_del check_cap_at cap_revoke ignore_del: retype_region_ext create_cap_ext cap_insert_ext ethread_set cap_move_ext diff --git a/proof/infoflow/RISCV64/ArchUserOp_IF.thy b/proof/infoflow/RISCV64/ArchUserOp_IF.thy index 33680e99cb..7e0168d38f 100644 --- a/proof/infoflow/RISCV64/ArchUserOp_IF.thy +++ b/proof/infoflow/RISCV64/ArchUserOp_IF.thy @@ -820,7 +820,7 @@ lemma do_user_op_reads_respects_g: apply (clarsimp simp: globals_equiv_def reads_equiv_g_def) apply (rule spec_equiv_valid_guard_imp) apply (wpsimp wp: dmo_user_memory_update_reads_respects_g dmo_device_state_update_reads_respects_g - dmo_device_state_update_reads_respects_g select_ev select_wp dmo_wp) + dmo_device_state_update_reads_respects_g select_ev dmo_wp) apply clarsimp apply (rule conjI) apply clarsimp diff --git a/proof/infoflow/Syscall_IF.thy b/proof/infoflow/Syscall_IF.thy index b162edd9a5..e14c659c29 100644 --- a/proof/infoflow/Syscall_IF.thy +++ b/proof/infoflow/Syscall_IF.thy @@ -174,7 +174,7 @@ proof (induct rule: cap_revoke.induct[where ?a1.0=s]) cap_delete_pas_refined cap_delete_silc_inv[where st=st] cap_delete_only_timer_irq_inv[where st=st' and irq=irq] drop_spec_ev[OF assertE_ev] drop_spec_ev[OF liftE_ev] - get_cap_wp select_wp select_ev drop_spec_ev2_inv[OF liftE_ev2] + get_cap_wp select_ev drop_spec_ev2_inv[OF liftE_ev2] reads_respects_f[OF get_cap_rev, where st=st and aag=aag] | simp (no_asm) add: returnOk_def | rule next_revoke_eq' | (simp add: pred_conj_def, erule conjE, assumption) diff --git a/proof/infoflow/refine/ADT_IF_Refine.thy b/proof/infoflow/refine/ADT_IF_Refine.thy index 5750ae76e7..cfeaaa4cb6 100644 --- a/proof/infoflow/refine/ADT_IF_Refine.thy +++ b/proof/infoflow/refine/ADT_IF_Refine.thy @@ -813,7 +813,6 @@ lemma abstract_invs: crunches checkActiveIRQ_if for ksDomainTime_inv[wp]: "\s. P (ksDomainTime s)" and ksDomSchedule_inv[wp]: "\s. P (ksDomSchedule s)" - (wp: select_wp) lemma kernelEntry_if_valid_domain_time: "e \ Interrupt \ \\\ kernelEntry_if e tc \\_ s. 0 < ksDomainTime s \ valid_domain_list' s\" diff --git a/proof/infoflow/refine/ARM/ArchADT_IF_Refine.thy b/proof/infoflow/refine/ARM/ArchADT_IF_Refine.thy index 2d6be286d0..14f0275927 100644 --- a/proof/infoflow/refine/ARM/ArchADT_IF_Refine.thy +++ b/proof/infoflow/refine/ARM/ArchADT_IF_Refine.thy @@ -246,7 +246,7 @@ lemma doUserOp_if_invs'[ADT_IF_Refine_assms, wp]: apply (wp device_update_invs' dmo_setExMonitor_wp' dmo_invs' | simp)+ apply (clarsimp simp add: no_irq_modify user_memory_update_def) apply wpsimp - apply (wp select_wp)+ + apply wp+ apply (clarsimp simp: user_memory_update_def simpler_modify_def restrict_map_def split: option.splits) @@ -257,25 +257,25 @@ lemma doUserOp_if_invs'[ADT_IF_Refine_assms, wp]: lemma doUserOp_valid_duplicates[ADT_IF_Refine_assms, wp]: "doUserOp_if f tc \arch_extras\" apply (simp add: doUserOp_if_def split_def) - apply (wp dmo_setExMonitor_wp' dmo_invs' select_wp | simp)+ + apply (wp dmo_setExMonitor_wp' dmo_invs' | simp)+ done lemma doUserOp_if_schedact[ADT_IF_Refine_assms, wp]: "doUserOp_if f tc \\s. P (ksSchedulerAction s)\" apply (simp add: doUserOp_if_def) - apply (wp select_wp | wpc | simp)+ + apply (wp | wpc | simp)+ done lemma doUserOp_if_st_tcb_at[ADT_IF_Refine_assms, wp]: "doUserOp_if f tc \st_tcb_at' st t\" apply (simp add: doUserOp_if_def) - apply (wp select_wp | wpc | simp)+ + apply (wp | wpc | simp)+ done lemma doUserOp_if_cur_thread[ADT_IF_Refine_assms, wp]: "doUserOp_if f tc \\s. P (ksCurThread s)\" apply (simp add: doUserOp_if_def) - apply (wp select_wp | wpc | simp)+ + apply (wp | wpc | simp)+ done lemma do_user_op_if_corres'[ADT_IF_Refine_assms]: @@ -334,7 +334,7 @@ lemma do_user_op_if_corres'[ADT_IF_Refine_assms]: apply (rule corres_split[OF corres_machine_op', where r'="(=)"]) apply (rule corres_underlying_trivial, simp) apply (rule corres_return_same_trivial) - by (wp hoare_TrueI[where P = \] | simp)+ + by wpsimp+ lemma dmo_getActiveIRQ_corres[ADT_IF_Refine_assms]: "corres (=) \ \ (do_machine_op (getActiveIRQ in_kernel)) (doMachineOp (getActiveIRQ in_kernel'))" @@ -401,7 +401,6 @@ lemma handle_preemption_if_corres[ADT_IF_Refine_assms]: crunches doUserOp_if for ksDomainTime_inv[ADT_IF_Refine_assms, wp]: "\s. P (ksDomainTime s)" and ksDomSchedule_inv[ADT_IF_Refine_assms, wp]: "\s. P (ksDomSchedule s)" - (wp: select_wp) crunches checkActiveIRQ_if for arch_extras[ADT_IF_Refine_assms, wp]: arch_extras @@ -422,7 +421,7 @@ lemma doUserOp_if_no_interrupt[ADT_IF_Refine_assms]: doUserOp_if uop tc \\r s. (fst r) \ Some Interrupt\" apply (simp add: doUserOp_if_def del: split_paired_All) - apply (wp select_wp | wpc)+ + apply (wp | wpc)+ apply (clarsimp simp: uop_sane_def simp del: split_paired_All) done diff --git a/proof/infoflow/refine/ARM/ArchADT_IF_Refine_C.thy b/proof/infoflow/refine/ARM/ArchADT_IF_Refine_C.thy index 60b2f1ce65..18518c2964 100644 --- a/proof/infoflow/refine/ARM/ArchADT_IF_Refine_C.thy +++ b/proof/infoflow/refine/ARM/ArchADT_IF_Refine_C.thy @@ -247,7 +247,7 @@ lemma do_user_op_if_C_corres[ADT_IF_Refine_assms]: apply (rule corres_split[OF device_update_corres_C]) apply (rule corres_split[OF corres_dmo_setExMonitor_C, where R="\\" and R'="\\"]) - apply (wp select_wp | simp)+ + apply (wp | simp)+ apply (clarsimp simp: ex_abs_def restrict_map_def invs_pspace_aligned' invs_pspace_distinct' ptable_lift_s'_def ptable_rights_s'_def split: if_splits) diff --git a/proof/infoflow/refine/RISCV64/ArchADT_IF_Refine.thy b/proof/infoflow/refine/RISCV64/ArchADT_IF_Refine.thy index fd13f3ae1f..23e74cf71a 100644 --- a/proof/infoflow/refine/RISCV64/ArchADT_IF_Refine.thy +++ b/proof/infoflow/refine/RISCV64/ArchADT_IF_Refine.thy @@ -186,7 +186,7 @@ lemma doUserOp_if_invs'[ADT_IF_Refine_assms, wp]: apply (wp device_update_invs' dmo_invs' | simp)+ apply (clarsimp simp add: no_irq_modify user_memory_update_def) apply wpsimp - apply (wp select_wp)+ + apply wp+ apply (clarsimp simp: user_memory_update_def simpler_modify_def restrict_map_def split: option.splits) @@ -197,25 +197,25 @@ lemma doUserOp_if_invs'[ADT_IF_Refine_assms, wp]: lemma doUserOp_valid_duplicates[ADT_IF_Refine_assms, wp]: "doUserOp_if f tc \arch_extras\" apply (simp add: doUserOp_if_def split_def) - apply (wp dmo_invs' select_wp | simp)+ + apply (wp dmo_invs' | simp)+ done lemma doUserOp_if_schedact[ADT_IF_Refine_assms, wp]: "doUserOp_if f tc \\s. P (ksSchedulerAction s)\" apply (simp add: doUserOp_if_def) - apply (wp select_wp | wpc | simp)+ + apply (wp | wpc | simp)+ done lemma doUserOp_if_st_tcb_at[ADT_IF_Refine_assms, wp]: "doUserOp_if f tc \st_tcb_at' st t\" apply (simp add: doUserOp_if_def) - apply (wp select_wp | wpc | simp)+ + apply (wp | wpc | simp)+ done lemma doUserOp_if_cur_thread[ADT_IF_Refine_assms, wp]: "doUserOp_if f tc \\s. P (ksCurThread s)\" apply (simp add: doUserOp_if_def) - apply (wp select_wp | wpc | simp)+ + apply (wp | wpc | simp)+ done lemma do_user_op_if_corres'[ADT_IF_Refine_assms]: @@ -348,7 +348,6 @@ lemma handle_preemption_if_corres[ADT_IF_Refine_assms]: crunches doUserOp_if for ksDomainTime_inv[ADT_IF_Refine_assms, wp]: "\s. P (ksDomainTime s)" and ksDomSchedule_inv[ADT_IF_Refine_assms, wp]: "\s. P (ksDomSchedule s)" - (wp: select_wp) crunches checkActiveIRQ_if for arch_extras[ADT_IF_Refine_assms, wp]: arch_extras @@ -369,7 +368,7 @@ lemma doUserOp_if_no_interrupt[ADT_IF_Refine_assms]: doUserOp_if uop tc \\r s. (fst r) \ Some Interrupt\" apply (simp add: doUserOp_if_def del: split_paired_All) - apply (wp select_wp | wpc)+ + apply (wp | wpc)+ apply (clarsimp simp: uop_sane_def simp del: split_paired_All) done diff --git a/proof/infoflow/refine/RISCV64/ArchADT_IF_Refine_C.thy b/proof/infoflow/refine/RISCV64/ArchADT_IF_Refine_C.thy index 077a9129e1..7982e61afb 100644 --- a/proof/infoflow/refine/RISCV64/ArchADT_IF_Refine_C.thy +++ b/proof/infoflow/refine/RISCV64/ArchADT_IF_Refine_C.thy @@ -169,7 +169,7 @@ lemma do_user_op_if_C_corres[ADT_IF_Refine_assms]: apply (rule corres_underlying_split4) apply (rule corres_split[OF user_memory_update_corres_C]) apply (rule corres_split[OF device_update_corres_C]) - apply (wp select_wp | simp)+ + apply (wp | simp)+ apply (clarsimp simp: ex_abs_def restrict_map_def invs_pspace_aligned' invs_pspace_distinct' ptable_lift_s'_def ptable_rights_s'_def split: if_splits) diff --git a/proof/invariant-abstract/AARCH64/ArchArch_AI.thy b/proof/invariant-abstract/AARCH64/ArchArch_AI.thy index 23d6aa1694..2c15e67eb2 100644 --- a/proof/invariant-abstract/AARCH64/ArchArch_AI.thy +++ b/proof/invariant-abstract/AARCH64/ArchArch_AI.thy @@ -1336,7 +1336,7 @@ crunch_ignore (add: select_ext find_vspace_for_asid) crunch inv [wp]: arch_decode_invocation "P" - (wp: crunch_wps select_wp select_ext_weak_wp hoare_vcg_all_lift + (wp: crunch_wps select_ext_weak_wp hoare_vcg_all_lift hoare_vcg_all_lift_R hoare_drop_imps simp: crunch_simps) @@ -1641,7 +1641,7 @@ lemma decode_asid_control_invocation_wf[wp]: apply (simp add: lookup_target_slot_def) apply wp apply (clarsimp simp: cte_wp_at_def) - apply (wpsimp wp: ensure_no_children_sp select_ext_weak_wp select_wp whenE_throwError_wp)+ + apply (wpsimp wp: ensure_no_children_sp select_ext_weak_wp whenE_throwError_wp)+ apply (rule conjI, fastforce) apply (cases excaps, simp) apply (case_tac list, simp) diff --git a/proof/invariant-abstract/AARCH64/ArchDetSchedSchedule_AI.thy b/proof/invariant-abstract/AARCH64/ArchDetSchedSchedule_AI.thy index 59c232c9b7..e45b48e3ba 100644 --- a/proof/invariant-abstract/AARCH64/ArchDetSchedSchedule_AI.thy +++ b/proof/invariant-abstract/AARCH64/ArchDetSchedSchedule_AI.thy @@ -345,7 +345,7 @@ crunch valid_etcbs [wp, DetSchedSchedule_AI_assms]: crunch simple_sched_action [wp, DetSchedSchedule_AI_assms]: arch_finalise_cap, prepare_thread_delete simple_sched_action - (wp: hoare_drop_imps mapM_x_wp mapM_wp select_wp subset_refl + (wp: hoare_drop_imps mapM_x_wp mapM_wp subset_refl simp: unless_def if_fun_split) crunch valid_sched [wp, DetSchedSchedule_AI_assms]: diff --git a/proof/invariant-abstract/AARCH64/ArchFinalise_AI.thy b/proof/invariant-abstract/AARCH64/ArchFinalise_AI.thy index 636df09577..4206c6c8fd 100644 --- a/proof/invariant-abstract/AARCH64/ArchFinalise_AI.thy +++ b/proof/invariant-abstract/AARCH64/ArchFinalise_AI.thy @@ -1598,7 +1598,7 @@ crunches (wp: crunch_wps subset_refl) crunch irq_node[Finalise_AI_asms,wp]: prepare_thread_delete "\s. P (interrupt_irq_node s)" - (wp: crunch_wps select_wp simp: crunch_simps) + (wp: crunch_wps simp: crunch_simps) crunch irq_node[wp]: arch_finalise_cap "\s. P (interrupt_irq_node s)" (simp: crunch_simps wp: crunch_wps) @@ -1830,7 +1830,7 @@ lemma (* replace_cap_invs_arch_update *)[Finalise_AI_asms]: lemma dmo_pred_tcb_at[wp]: "do_machine_op mop \\s. P (pred_tcb_at f Q t s)\" apply (simp add: do_machine_op_def split_def) - apply (wp select_wp) + apply wp apply (clarsimp simp: pred_tcb_at_def obj_at_def) done diff --git a/proof/invariant-abstract/AARCH64/ArchVCPU_AI.thy b/proof/invariant-abstract/AARCH64/ArchVCPU_AI.thy index 343c4165c3..91d376d8ff 100644 --- a/proof/invariant-abstract/AARCH64/ArchVCPU_AI.thy +++ b/proof/invariant-abstract/AARCH64/ArchVCPU_AI.thy @@ -252,7 +252,7 @@ lemma schedule_valid_cur_vcpu[wp]: (schedule :: (unit, unit) s_monad) \\_. valid_cur_vcpu\" unfolding schedule_def allActiveTCBs_def - by (wpsimp wp: alternative_wp select_wp) + by wpsimp crunches cancel_all_ipc, blocked_cancel_ipc, unbind_maybe_notification, cancel_all_signals, bind_notification, fast_finalise, deleted_irq_handler, post_cap_deletion, cap_delete_one, @@ -262,7 +262,7 @@ crunches cancel_all_ipc, blocked_cancel_ipc, unbind_maybe_notification, cancel_a restart, reschedule_required, possible_switch_to, thread_set_priority, reply_from_kernel for arch_state[wp]: "\s. P (arch_state s)" and cur_thread[wp]: "\s. P (cur_thread s)" - (wp: mapM_x_wp_inv thread_set.arch_state select_wp crunch_wps + (wp: mapM_x_wp_inv thread_set.arch_state crunch_wps simp: crunch_simps possible_switch_to_def reschedule_required_def) lemma do_unbind_notification_arch_tcb_at[wp]: @@ -294,7 +294,7 @@ crunches blocked_cancel_ipc, cap_delete_one, cancel_signal lemma reply_cancel_ipc_arch_tcb_at[wp]: "reply_cancel_ipc ntfnptr \arch_tcb_at P t\" unfolding reply_cancel_ipc_def thread_set_def - apply (wpsimp wp: set_object_wp select_wp) + apply (wpsimp wp: set_object_wp) by (clarsimp simp: pred_tcb_at_def obj_at_def get_tcb_def) crunches cancel_ipc, send_ipc, receive_ipc @@ -373,7 +373,7 @@ crunches cap_insert, cap_move crunches suspend, unbind_notification, cap_swap_for_delete for state_hyp_refs_of[wp]: "\s. P (state_hyp_refs_of s)" - (wp: crunch_wps thread_set_hyp_refs_trivial select_wp simp: crunch_simps) + (wp: crunch_wps thread_set_hyp_refs_trivial simp: crunch_simps) lemma prepare_thread_delete_valid_cur_vcpu[wp]: "\\s. valid_cur_vcpu s \ sym_refs (state_hyp_refs_of s)\ diff --git a/proof/invariant-abstract/AARCH64/ArchVSpaceEntries_AI.thy b/proof/invariant-abstract/AARCH64/ArchVSpaceEntries_AI.thy index 9fdb9ab43e..491f59906e 100644 --- a/proof/invariant-abstract/AARCH64/ArchVSpaceEntries_AI.thy +++ b/proof/invariant-abstract/AARCH64/ArchVSpaceEntries_AI.thy @@ -99,7 +99,7 @@ crunch valid_vspace_objs'[wp]: set_simple_ko "valid_vspace_objs'" (wp: crunch_wps) crunch valid_vspace_objs'[wp]: finalise_cap, cap_swap_for_delete, empty_slot "valid_vspace_objs'" - (wp: crunch_wps select_wp preemption_point_inv simp: crunch_simps unless_def ignore:set_object) + (wp: crunch_wps preemption_point_inv simp: crunch_simps unless_def ignore:set_object) lemma preemption_point_valid_vspace_objs'[wp]: "\valid_vspace_objs'\ preemption_point \\rv. valid_vspace_objs'\" @@ -213,7 +213,7 @@ lemma perform_asid_pool_invocation_valid_vspace_objs'[wp]: crunch valid_vspace_objs'[wp]: perform_asid_pool_invocation, perform_asid_control_invocation "valid_vspace_objs'" (ignore: delete_objects set_object - wp: static_imp_wp select_wp crunch_wps + wp: static_imp_wp crunch_wps simp: crunch_simps unless_def) lemma perform_page_valid_vspace_objs'[wp]: @@ -277,7 +277,7 @@ lemma handle_invocation_valid_vspace_objs'[wp]: crunch valid_vspace_objs'[wp]: activate_thread,switch_to_thread, handle_hypervisor_fault, switch_to_idle_thread, handle_call, handle_recv, handle_reply, handle_send, handle_yield, handle_interrupt "valid_vspace_objs'" - (simp: crunch_simps wp: crunch_wps alternative_wp select_wp OR_choice_weak_wp select_ext_weak_wp + (simp: crunch_simps wp: crunch_wps OR_choice_weak_wp select_ext_weak_wp ignore: without_preemption getActiveIRQ resetTimer ackInterrupt OR_choice set_scheduler_action) @@ -288,7 +288,7 @@ lemma handle_event_valid_vspace_objs'[wp]: lemma schedule_valid_vspace_objs'[wp]: "\valid_vspace_objs'\ schedule :: (unit,unit) s_monad \\_. valid_vspace_objs'\" apply (simp add: schedule_def allActiveTCBs_def) - apply (wp alternative_wp select_wp) + apply wp apply simp done diff --git a/proof/invariant-abstract/AARCH64/Machine_AI.thy b/proof/invariant-abstract/AARCH64/Machine_AI.thy index a5d3146ac5..e6c2328ff7 100644 --- a/proof/invariant-abstract/AARCH64/Machine_AI.thy +++ b/proof/invariant-abstract/AARCH64/Machine_AI.thy @@ -100,7 +100,7 @@ definition "irq_state_independent P \ \f s. P s \ lemma getActiveIRQ_inv[wp]: "\irq_state_independent P\ \ getActiveIRQ in_kernel \P\" apply (simp add: getActiveIRQ_def) - apply (wp alternative_wp select_wp) + apply wp apply (simp add: irq_state_independent_def) done @@ -392,7 +392,7 @@ lemma getActiveIRQ_le_maxIRQ': getActiveIRQ in_kernel \\rv s. \x. rv = Some x \ x \ maxIRQ\" apply (simp add: getActiveIRQ_def) - apply (wpsimp wp: alternative_wp select_wp) + apply wpsimp apply (rule ccontr) apply (simp add: linorder_not_le) done diff --git a/proof/invariant-abstract/AInvs.thy b/proof/invariant-abstract/AInvs.thy index cf0cf83db3..1310a21a9f 100644 --- a/proof/invariant-abstract/AInvs.thy +++ b/proof/invariant-abstract/AInvs.thy @@ -44,7 +44,7 @@ lemma kernel_entry_invs: (kernel_entry e us) :: (user_context,unit) s_monad \\rv. invs and (\s. ct_running s \ ct_idle s)\" apply (simp add: kernel_entry_def) - apply (wp akernel_invs thread_set_invs_trivial thread_set_ct_in_state select_wp + apply (wp akernel_invs thread_set_invs_trivial thread_set_ct_in_state do_machine_op_ct_in_state static_imp_wp hoare_vcg_disj_lift | clarsimp simp add: tcb_cap_cases_def)+ done @@ -89,7 +89,7 @@ lemma do_user_op_invs: \\_. invs and ct_running\" apply (simp add: do_user_op_def split_def) apply (wp device_update_invs) - apply (wp do_machine_op_ct_in_state select_wp dmo_invs | simp add:dom_restrict_plus_eq)+ + apply (wp do_machine_op_ct_in_state dmo_invs | simp add:dom_restrict_plus_eq)+ apply (clarsimp simp: user_memory_update_def simpler_modify_def restrict_map_def invs_def cur_tcb_def split: option.splits if_split_asm) diff --git a/proof/invariant-abstract/ARM/ArchArch_AI.thy b/proof/invariant-abstract/ARM/ArchArch_AI.thy index 4f0ef1f420..72950eb1e9 100644 --- a/proof/invariant-abstract/ARM/ArchArch_AI.thy +++ b/proof/invariant-abstract/ARM/ArchArch_AI.thy @@ -946,7 +946,7 @@ lemma create_mapping_entries_inv [wp]: crunch_ignore (add: select_ext) crunch inv [wp]: arch_decode_invocation "P" - (wp: crunch_wps select_wp select_ext_weak_wp simp: crunch_simps) + (wp: crunch_wps select_ext_weak_wp simp: crunch_simps) lemma create_mappings_empty [wp]: @@ -1266,7 +1266,7 @@ lemma arch_decode_inv_wf[wp]: apply (rename_tac word1 word2) apply (simp add: arch_decode_invocation_def Let_def split_def cong: if_cong split del: if_split) apply (rule hoare_pre) - apply ((wp whenE_throwError_wp check_vp_wpR ensure_empty_stronger select_wp select_ext_weak_wp| + apply ((wp whenE_throwError_wp check_vp_wpR ensure_empty_stronger select_ext_weak_wp| wpc| simp add: valid_arch_inv_def valid_apinv_def)+)[1] apply (simp add: valid_arch_inv_def valid_apinv_def) @@ -1328,7 +1328,7 @@ lemma arch_decode_inv_wf[wp]: apply (simp add: asid_bits_def asid_low_bits_def) apply (simp add: asid_bits_def) apply (simp split del: if_split) - apply (wp ensure_no_children_sp select_ext_weak_wp select_wp whenE_throwError_wp | wpc | simp)+ + apply (wp ensure_no_children_sp select_ext_weak_wp whenE_throwError_wp | wpc | simp)+ apply clarsimp apply (rule conjI, fastforce) apply (cases excaps, simp) diff --git a/proof/invariant-abstract/ARM/ArchDetSchedSchedule_AI.thy b/proof/invariant-abstract/ARM/ArchDetSchedSchedule_AI.thy index 49c9a827ba..295ee1c6de 100644 --- a/proof/invariant-abstract/ARM/ArchDetSchedSchedule_AI.thy +++ b/proof/invariant-abstract/ARM/ArchDetSchedSchedule_AI.thy @@ -204,7 +204,7 @@ crunch valid_etcbs [wp, DetSchedSchedule_AI_assms]: crunch simple_sched_action [wp, DetSchedSchedule_AI_assms]: arch_finalise_cap, prepare_thread_delete simple_sched_action - (wp: hoare_drop_imps mapM_x_wp mapM_wp select_wp subset_refl + (wp: hoare_drop_imps mapM_x_wp mapM_wp subset_refl simp: unless_def if_fun_split) crunches arch_finalise_cap, prepare_thread_delete, arch_invoke_irq_handler diff --git a/proof/invariant-abstract/ARM/ArchFinalise_AI.thy b/proof/invariant-abstract/ARM/ArchFinalise_AI.thy index d3be9ff89a..a0dd0c82af 100644 --- a/proof/invariant-abstract/ARM/ArchFinalise_AI.thy +++ b/proof/invariant-abstract/ARM/ArchFinalise_AI.thy @@ -639,7 +639,7 @@ interpretation Finalise_AI_2?: Finalise_AI_2 context Arch begin global_naming ARM crunch irq_node[wp]: arch_finalise_cap "\s. P (interrupt_irq_node s)" - (wp: crunch_wps select_wp simp: crunch_simps) + (wp: crunch_wps simp: crunch_simps) crunch irq_node[wp,Finalise_AI_asms]: prepare_thread_delete "\s. P (interrupt_irq_node s)" diff --git a/proof/invariant-abstract/ARM/ArchVSpaceEntries_AI.thy b/proof/invariant-abstract/ARM/ArchVSpaceEntries_AI.thy index 559a0ce300..3ed467cc85 100644 --- a/proof/invariant-abstract/ARM/ArchVSpaceEntries_AI.thy +++ b/proof/invariant-abstract/ARM/ArchVSpaceEntries_AI.thy @@ -402,7 +402,7 @@ lemma set_simple_ko_valid_pdpt_objs[wp]: split: kernel_object.splits) crunch valid_pdpt_objs[wp]: finalise_cap, cap_swap_for_delete, empty_slot "valid_pdpt_objs" - (wp: crunch_wps select_wp preemption_point_inv simp: crunch_simps unless_def ignore:set_object) + (wp: crunch_wps preemption_point_inv simp: crunch_simps unless_def ignore:set_object) lemma preemption_point_valid_pdpt_objs[wp]: "\valid_pdpt_objs\ preemption_point \\rv. valid_pdpt_objs\" @@ -1513,15 +1513,14 @@ lemma handle_invocation_valid_pdpt[wp]: crunch valid_pdpt[wp]: handle_event, activate_thread,switch_to_thread, switch_to_idle_thread "valid_pdpt_objs" - (simp: crunch_simps wp: crunch_wps alternative_wp select_wp OR_choice_weak_wp select_ext_weak_wp + (simp: crunch_simps wp: crunch_wps OR_choice_weak_wp select_ext_weak_wp ignore: without_preemption getActiveIRQ resetTimer ackInterrupt getFAR getDFSR getIFSR OR_choice set_scheduler_action clearExMonitor) lemma schedule_valid_pdpt[wp]: "\valid_pdpt_objs\ schedule :: (unit,unit) s_monad \\_. valid_pdpt_objs\" apply (simp add: schedule_def allActiveTCBs_def) - apply (wp alternative_wp select_wp) - apply simp + apply wpsimp done lemma call_kernel_valid_pdpt[wp]: diff --git a/proof/invariant-abstract/ARM/Machine_AI.thy b/proof/invariant-abstract/ARM/Machine_AI.thy index 66069e8061..ab2f402f20 100644 --- a/proof/invariant-abstract/ARM/Machine_AI.thy +++ b/proof/invariant-abstract/ARM/Machine_AI.thy @@ -327,7 +327,7 @@ definition "irq_state_independent P \ \f s. P s \ lemma getActiveIRQ_inv [wp]: "\irq_state_independent P\ \ \P\ getActiveIRQ in_kernel \\rv. P\" apply (simp add: getActiveIRQ_def) - apply (wp alternative_wp select_wp) + apply wp apply (simp add: irq_state_independent_def) done @@ -613,7 +613,7 @@ lemma no_irq_clearMemory: "no_irq (clearMemory a b)" lemma getActiveIRQ_le_maxIRQ': "\\s. \irq > maxIRQ. irq_masks s irq\ getActiveIRQ in_kernel \\rv s. \x. rv = Some x \ x \ maxIRQ\" apply (simp add: getActiveIRQ_def) - apply (wp alternative_wp select_wp) + apply wp apply clarsimp apply (rule ccontr) apply (simp add: linorder_not_le) @@ -623,14 +623,14 @@ lemma getActiveIRQ_le_maxIRQ': lemma getActiveIRQ_neq_Some0xFF': "\\\ getActiveIRQ in_kernel \\rv s. rv \ Some 0x3FF\" apply (simp add: getActiveIRQ_def) - apply (wp alternative_wp select_wp) + apply wp apply simp done lemma getActiveIRQ_neq_non_kernel: "\\\ getActiveIRQ True \\rv s. rv \ Some ` non_kernel_IRQs \" apply (simp add: getActiveIRQ_def) - apply (wp alternative_wp select_wp) + apply wp apply auto done diff --git a/proof/invariant-abstract/ARM_HYP/ArchArch_AI.thy b/proof/invariant-abstract/ARM_HYP/ArchArch_AI.thy index e94651cdc5..bff5414bd4 100644 --- a/proof/invariant-abstract/ARM_HYP/ArchArch_AI.thy +++ b/proof/invariant-abstract/ARM_HYP/ArchArch_AI.thy @@ -1281,7 +1281,7 @@ crunch inv[wp]: ensure_safe_mapping, create_mapping_entries "P" crunch_ignore (add: select_ext) crunch inv [wp]: arch_decode_invocation "P" - (wp: crunch_wps select_wp select_ext_weak_wp simp: crunch_simps) + (wp: crunch_wps select_ext_weak_wp simp: crunch_simps) lemma create_mappings_empty [wp]: @@ -1596,7 +1596,7 @@ lemma arch_decode_inv_wf[wp]: apply (rename_tac word1 word2) apply (simp add: arch_decode_invocation_def Let_def decode_mmu_invocation_def split_def cong: if_cong) apply (rule hoare_pre) - apply ((wp whenE_throwError_wp check_vp_wpR ensure_empty_stronger select_wp select_ext_weak_wp| + apply ((wp whenE_throwError_wp check_vp_wpR ensure_empty_stronger select_ext_weak_wp| wpc| simp add: valid_arch_inv_def valid_apinv_def)+)[1] apply (simp add: if_apply_def2 valid_apinv_def) @@ -1657,7 +1657,7 @@ lemma arch_decode_inv_wf[wp]: apply (simp add: asid_bits_def asid_low_bits_def) apply (simp add: asid_bits_def) apply simp - apply (wp ensure_no_children_sp select_ext_weak_wp select_wp whenE_throwError_wp|wpc | simp)+ + apply (wp ensure_no_children_sp select_ext_weak_wp whenE_throwError_wp|wpc | simp)+ apply clarsimp apply (rule conjI, fastforce) apply (cases excaps, simp) diff --git a/proof/invariant-abstract/ARM_HYP/ArchDetSchedSchedule_AI.thy b/proof/invariant-abstract/ARM_HYP/ArchDetSchedSchedule_AI.thy index 2362067046..84867f0f8d 100644 --- a/proof/invariant-abstract/ARM_HYP/ArchDetSchedSchedule_AI.thy +++ b/proof/invariant-abstract/ARM_HYP/ArchDetSchedSchedule_AI.thy @@ -299,7 +299,7 @@ crunch valid_etcbs [wp, DetSchedSchedule_AI_assms]: crunch simple_sched_action [wp, DetSchedSchedule_AI_assms]: arch_finalise_cap, prepare_thread_delete simple_sched_action - (wp: hoare_drop_imps mapM_x_wp mapM_wp select_wp subset_refl + (wp: hoare_drop_imps mapM_x_wp mapM_wp subset_refl simp: unless_def if_fun_split) crunches arch_finalise_cap, prepare_thread_delete, arch_invoke_irq_handler diff --git a/proof/invariant-abstract/ARM_HYP/ArchFinalise_AI.thy b/proof/invariant-abstract/ARM_HYP/ArchFinalise_AI.thy index 4793ea4d63..2d14aaba13 100644 --- a/proof/invariant-abstract/ARM_HYP/ArchFinalise_AI.thy +++ b/proof/invariant-abstract/ARM_HYP/ArchFinalise_AI.thy @@ -1398,7 +1398,7 @@ crunches (wp: crunch_wps subset_refl) crunch irq_node[Finalise_AI_asms,wp]: prepare_thread_delete "\s. P (interrupt_irq_node s)" - (wp: crunch_wps select_wp simp: crunch_simps) + (wp: crunch_wps simp: crunch_simps) crunch irq_node[wp]: arch_finalise_cap "\s. P (interrupt_irq_node s)" (simp: crunch_simps wp: crunch_wps) diff --git a/proof/invariant-abstract/ARM_HYP/ArchVCPU_AI.thy b/proof/invariant-abstract/ARM_HYP/ArchVCPU_AI.thy index 1076fd9885..1273ab1fbf 100644 --- a/proof/invariant-abstract/ARM_HYP/ArchVCPU_AI.thy +++ b/proof/invariant-abstract/ARM_HYP/ArchVCPU_AI.thy @@ -255,7 +255,7 @@ lemma schedule_valid_cur_vcpu[wp]: (schedule :: (unit, unit) s_monad) \\_. valid_cur_vcpu\" unfolding schedule_def allActiveTCBs_def - by (wpsimp wp: alternative_wp select_wp) + by wpsimp crunches cancel_all_ipc, blocked_cancel_ipc, unbind_maybe_notification, cancel_all_signals, bind_notification, fast_finalise, deleted_irq_handler, post_cap_deletion, cap_delete_one, @@ -265,7 +265,7 @@ crunches cancel_all_ipc, blocked_cancel_ipc, unbind_maybe_notification, cancel_a restart, reschedule_required, possible_switch_to, thread_set_priority, reply_from_kernel for arch_state[wp]: "\s. P (arch_state s)" and cur_thread[wp]: "\s. P (cur_thread s)" - (wp: mapM_x_wp_inv thread_set.arch_state select_wp crunch_wps + (wp: mapM_x_wp_inv thread_set.arch_state crunch_wps simp: crunch_simps possible_switch_to_def reschedule_required_def) lemma do_unbind_notification_arch_tcb_at[wp]: @@ -297,7 +297,7 @@ crunches blocked_cancel_ipc, cap_delete_one, cancel_signal lemma reply_cancel_ipc_arch_tcb_at[wp]: "reply_cancel_ipc ntfnptr \arch_tcb_at P t\" unfolding reply_cancel_ipc_def thread_set_def - apply (wpsimp wp: set_object_wp select_wp) + apply (wpsimp wp: set_object_wp) by (clarsimp simp: pred_tcb_at_def obj_at_def get_tcb_def) crunches cancel_ipc, send_ipc, receive_ipc @@ -376,7 +376,7 @@ crunches cap_insert, cap_move crunches suspend, unbind_notification, cap_swap_for_delete for state_hyp_refs_of[wp]: "\s. P (state_hyp_refs_of s)" - (wp: crunch_wps thread_set_hyp_refs_trivial select_wp simp: crunch_simps) + (wp: crunch_wps thread_set_hyp_refs_trivial simp: crunch_simps) lemma prepare_thread_delete_valid_cur_vcpu[wp]: "\\s. valid_cur_vcpu s \ sym_refs (state_hyp_refs_of s)\ diff --git a/proof/invariant-abstract/ARM_HYP/ArchVSpaceEntries_AI.thy b/proof/invariant-abstract/ARM_HYP/ArchVSpaceEntries_AI.thy index d4896e1949..6de970f90f 100644 --- a/proof/invariant-abstract/ARM_HYP/ArchVSpaceEntries_AI.thy +++ b/proof/invariant-abstract/ARM_HYP/ArchVSpaceEntries_AI.thy @@ -410,7 +410,7 @@ lemma set_simple_ko_valid_pdpt_objs[wp]: done crunch valid_pdpt_objs[wp]: finalise_cap, cap_swap_for_delete, empty_slot "valid_pdpt_objs" - (wp: crunch_wps select_wp preemption_point_inv simp: crunch_simps unless_def ignore:set_object) + (wp: crunch_wps preemption_point_inv simp: crunch_simps unless_def ignore:set_object) lemma preemption_point_valid_pdpt_objs[wp]: "\valid_pdpt_objs\ preemption_point \\rv. valid_pdpt_objs\" @@ -1511,15 +1511,14 @@ lemma handle_invocation_valid_pdpt[wp]: crunch valid_pdpt[wp]: handle_event, activate_thread,switch_to_thread, switch_to_idle_thread "valid_pdpt_objs" - (simp: crunch_simps wp: crunch_wps alternative_wp select_wp OR_choice_weak_wp select_ext_weak_wp + (simp: crunch_simps wp: crunch_wps OR_choice_weak_wp select_ext_weak_wp ignore: without_preemption getActiveIRQ resetTimer ackInterrupt getFAR getDFSR getIFSR OR_choice set_scheduler_action clearExMonitor) lemma schedule_valid_pdpt[wp]: "\valid_pdpt_objs\ schedule :: (unit,unit) s_monad \\_. valid_pdpt_objs\" apply (simp add: schedule_def allActiveTCBs_def) - apply (wp alternative_wp select_wp) - apply simp + apply wpsimp done lemma call_kernel_valid_pdpt[wp]: diff --git a/proof/invariant-abstract/ARM_HYP/Machine_AI.thy b/proof/invariant-abstract/ARM_HYP/Machine_AI.thy index 9bab71c277..5a172f2603 100644 --- a/proof/invariant-abstract/ARM_HYP/Machine_AI.thy +++ b/proof/invariant-abstract/ARM_HYP/Machine_AI.thy @@ -336,7 +336,7 @@ definition "irq_state_independent P \ \f s. P s \ lemma getActiveIRQ_inv [wp]: "\irq_state_independent P\ \ \P\ getActiveIRQ in_kernel \\rv. P\" apply (simp add: getActiveIRQ_def) - apply (wp alternative_wp select_wp) + apply wp apply (simp add: irq_state_independent_def) done @@ -670,7 +670,7 @@ lemma no_irq_clearMemory: "no_irq (clearMemory a b)" lemma getActiveIRQ_le_maxIRQ': "\\s. \irq > maxIRQ. irq_masks s irq\ getActiveIRQ in_kernel \\rv s. \x. rv = Some x \ x \ maxIRQ\" apply (simp add: getActiveIRQ_def) - apply (wp alternative_wp select_wp) + apply wp apply clarsimp apply (rule ccontr) apply (simp add: linorder_not_le) @@ -680,14 +680,13 @@ lemma getActiveIRQ_le_maxIRQ': lemma getActiveIRQ_neq_Some0xFF': "\\\ getActiveIRQ in_kernel \\rv s. rv \ Some 0x3FF\" apply (simp add: getActiveIRQ_def) - apply (wp alternative_wp select_wp) - apply simp + apply wpsimp done lemma getActiveIRQ_neq_non_kernel: "\\\ getActiveIRQ True \\rv s. rv \ Some ` non_kernel_IRQs \" apply (simp add: getActiveIRQ_def) - apply (wp alternative_wp select_wp) + apply wp apply auto done diff --git a/proof/invariant-abstract/CNodeInv_AI.thy b/proof/invariant-abstract/CNodeInv_AI.thy index 643f760cb4..ae2857d1a5 100644 --- a/proof/invariant-abstract/CNodeInv_AI.thy +++ b/proof/invariant-abstract/CNodeInv_AI.thy @@ -897,12 +897,12 @@ context CNodeInv_AI begin lemma preemption_point_not_recursive_cspaces[wp]: "preemption_point \\s. P (not_recursive_cspaces s)\" unfolding preemption_point_def - by (wpsimp wp: OR_choiceE_weak_wp alternative_wp hoare_drop_imp) + by (wpsimp wp: OR_choiceE_weak_wp hoare_drop_imp) lemma preemption_point_caps_of_state[wp]: "preemption_point \\s. P (caps_of_state s)\" unfolding preemption_point_def - by (wpsimp wp: OR_choiceE_weak_wp alternative_wp hoare_drop_imp) + by (wpsimp wp: OR_choiceE_weak_wp hoare_drop_imp) lemma rec_del_termination: "All (rec_del_dom :: rec_del_call \ 'state_ext state \ bool)" @@ -1089,7 +1089,7 @@ end lemma dom_valid_cap[wp]: "\valid_cap c\ do_machine_op f \\_. valid_cap c\" apply (simp add: do_machine_op_def split_def) - apply (wp select_wp) + apply wp apply simp done @@ -1097,7 +1097,7 @@ lemma dom_valid_cap[wp]: lemma dom_cte_at: "\cte_at c\ do_machine_op f \\_. cte_at c\" apply (simp add: do_machine_op_def split_def) - apply (wp select_wp) + apply wp apply (simp add: cte_at_cases) done @@ -2394,7 +2394,7 @@ declare thread_set_Pmdb [wp] lemma reply_cancel_ipc_emptyable[wp]: "\invs and emptyable sl and valid_mdb\ reply_cancel_ipc ptr \\_. emptyable sl\" apply (simp add: reply_cancel_ipc_def) - apply (wp select_wp select_inv hoare_drop_imps | simp add: Ball_def)+ + apply (wp select_inv hoare_drop_imps | simp add: Ball_def)+ apply (wp hoare_vcg_all_lift hoare_convert_imp thread_set_Pmdb thread_set_invs_trivial thread_set_emptyable thread_set_cte_at | simp add: tcb_cap_cases_def descendants_of_cte_at)+ @@ -2712,16 +2712,16 @@ lemmas empty_slot_rvk_prog' = empty_slot_rvk_prog[unfolded o_def] crunch rvk_prog: cancel_ipc "\s. revoke_progress_ord m (\x. option_map cap_to_rpo (caps_of_state s x))" (simp: crunch_simps o_def unless_def is_final_cap_def tcb_cap_cases_def - wp: hoare_drop_imps empty_slot_rvk_prog' select_wp + wp: hoare_drop_imps empty_slot_rvk_prog' thread_set_caps_of_state_trivial) crunch rvk_prog: suspend "\s. revoke_progress_ord m (\x. option_map cap_to_rpo (caps_of_state s x))" (simp: crunch_simps o_def unless_def is_final_cap_def - wp: crunch_wps empty_slot_rvk_prog' select_wp) + wp: crunch_wps empty_slot_rvk_prog') crunch rvk_prog: deleting_irq_handler "\s. revoke_progress_ord m (\x. option_map cap_to_rpo (caps_of_state s x))" (simp: crunch_simps o_def unless_def is_final_cap_def - wp: crunch_wps empty_slot_rvk_prog' select_wp) + wp: crunch_wps empty_slot_rvk_prog') locale CNodeInv_AI_3 = CNodeInv_AI_2 state_ext_t for state_ext_t :: "'state_ext::state_ext itself" + @@ -2998,7 +2998,7 @@ proof (induct rule: cap_revoke_induct) show ?case apply (subst cap_revoke_simps) apply (wp "1.hyps") - apply (wp x p hoare_drop_imps select_wp)+ + apply (wp x p hoare_drop_imps)+ apply simp_all done qed @@ -3022,7 +3022,7 @@ proof (induct rule: cap_revoke_induct) show ?case apply (subst cap_revoke_simps) apply (wp "1.hyps") - apply (wp x p hoare_drop_imps select_wp)+ + apply (wp x p hoare_drop_imps)+ apply (simp_all add: y) done qed diff --git a/proof/invariant-abstract/CSpace_AI.thy b/proof/invariant-abstract/CSpace_AI.thy index 4ffd7d2877..a064743d16 100644 --- a/proof/invariant-abstract/CSpace_AI.thy +++ b/proof/invariant-abstract/CSpace_AI.thy @@ -115,7 +115,7 @@ lemma preemption_point_inv: shows "\irq_state_independent_A P; \f s. P (trans_state f s) = P s\ \ \P\ preemption_point \\_. P\" apply (intro impI conjI | simp add: preemption_point_def o_def - | wp hoare_post_imp[OF _ getActiveIRQ_wp] OR_choiceE_weak_wp alternative_wp[where P=P] + | wp hoare_post_imp[OF _ getActiveIRQ_wp] OR_choiceE_weak_wp | wpc)+ done diff --git a/proof/invariant-abstract/DetSchedDomainTime_AI.thy b/proof/invariant-abstract/DetSchedDomainTime_AI.thy index 753e697921..e11b910d86 100644 --- a/proof/invariant-abstract/DetSchedDomainTime_AI.thy +++ b/proof/invariant-abstract/DetSchedDomainTime_AI.thy @@ -247,7 +247,6 @@ end section \Preservation of domain time remaining\ crunch domain_time_inv[wp]: do_user_op "(\s. P (domain_time s))" - (wp: select_wp) context DetSchedDomainTime_AI begin @@ -262,7 +261,7 @@ crunch domain_time_inv[wp]: choose_thread "\s. P (domain_time s)" crunch domain_time_inv[wp]: send_signal "\s. P (domain_time s)" - (wp: hoare_drop_imps mapM_x_wp_inv select_wp simp: crunch_simps unless_def) + (wp: hoare_drop_imps mapM_x_wp_inv simp: crunch_simps unless_def) crunch domain_time_inv[wp]: cap_swap_for_delete, empty_slot, get_object, get_cap, tcb_sched_action diff --git a/proof/invariant-abstract/DetSchedSchedule_AI.thy b/proof/invariant-abstract/DetSchedSchedule_AI.thy index 2385914a0b..ebb5e8681a 100644 --- a/proof/invariant-abstract/DetSchedSchedule_AI.thy +++ b/proof/invariant-abstract/DetSchedSchedule_AI.thy @@ -1525,7 +1525,7 @@ crunch valid_sched[wp]: cap_swap_for_delete, empty_slot, cap_delete_one valid_sc lemma reply_cancel_ipc_valid_sched[wp]: "\valid_sched\ reply_cancel_ipc tptr \\rv. valid_sched\" apply (simp add: reply_cancel_ipc_def) - apply (wp select_wp hoare_drop_imps thread_set_not_state_valid_sched | simp)+ + apply (wp hoare_drop_imps thread_set_not_state_valid_sched | simp)+ done end @@ -1659,7 +1659,7 @@ crunches update_restart_pc (simp: crunch_simps ignore: set_object) crunch simple_sched_action[wp]: finalise_cap simple_sched_action - (wp: hoare_drop_imps mapM_x_wp mapM_wp select_wp subset_refl + (wp: hoare_drop_imps mapM_x_wp mapM_wp subset_refl simp: unless_def if_fun_split) lemma suspend_valid_sched[wp]: @@ -1998,7 +1998,7 @@ crunch not_cur_thread[wp]: empty_slot "not_cur_thread thread" (wp: crunch_wps) crunch not_cur_thread[wp]: setup_reply_master, cancel_ipc "not_cur_thread thread" - (wp: hoare_drop_imps select_wp mapM_x_wp simp: unless_def if_fun_split) + (wp: hoare_drop_imps mapM_x_wp simp: unless_def if_fun_split) crunch etcb_at[wp]: setup_reply_master "etcb_at P t" @@ -3461,8 +3461,8 @@ crunch valid_list[wp]: schedule_choose_new_thread valid_list lemma schedule_valid_list[wp]: "\valid_list\ Schedule_A.schedule \\_. valid_list\" apply (simp add: Schedule_A.schedule_def) - apply (wp add: tcb_sched_action_valid_list alternative_wp select_wp gts_wp hoare_drop_imps - del: ethread_get_wp + apply (wp add: tcb_sched_action_valid_list gts_wp hoare_drop_imps + del: ethread_get_wp | wpc | simp)+ done diff --git a/proof/invariant-abstract/Deterministic_AI.thy b/proof/invariant-abstract/Deterministic_AI.thy index 9661387dc1..c46775a01b 100644 --- a/proof/invariant-abstract/Deterministic_AI.thy +++ b/proof/invariant-abstract/Deterministic_AI.thy @@ -3839,7 +3839,7 @@ crunch valid_list[wp]: thread_set valid_list lemma reply_cancel_ipc_valid_list[wp]: "\valid_list\ reply_cancel_ipc a \\_. valid_list\" unfolding reply_cancel_ipc_def - by (wp select_wp hoare_drop_imps thread_set_mdb | simp)+ + by (wp hoare_drop_imps thread_set_mdb | simp)+ crunch all_but_exst[wp]: update_work_units "all_but_exst P" @@ -3854,7 +3854,7 @@ global_interpretation reset_work_units_ext_extended: is_extended "reset_work_uni lemma preemption_point_inv': "\irq_state_independent_A P; \f s. P (work_units_completed_update f s) = P s\ \ \P\ preemption_point \\_. P\" apply (intro impI conjI | simp add: preemption_point_def o_def - | wp hoare_post_imp[OF _ getActiveIRQ_wp] OR_choiceE_weak_wp alternative_wp[where P=P] + | wp hoare_post_imp[OF _ getActiveIRQ_wp] OR_choiceE_weak_wp | wpc | simp add: update_work_units_def reset_work_units_def)+ done diff --git a/proof/invariant-abstract/Finalise_AI.thy b/proof/invariant-abstract/Finalise_AI.thy index bef35e5619..d542fd4ae1 100644 --- a/proof/invariant-abstract/Finalise_AI.thy +++ b/proof/invariant-abstract/Finalise_AI.thy @@ -487,7 +487,7 @@ lemma cancel_ipc_caps_of_state: \\rv s. P (caps_of_state s)\" apply (simp add: cancel_ipc_def reply_cancel_ipc_def cong: Structures_A.thread_state.case_cong) - apply (wpsimp wp: cap_delete_one_caps_of_state select_wp) + apply (wpsimp wp: cap_delete_one_caps_of_state) apply (rule_tac Q="\_ s. (\p. cte_wp_at can_fast_finalise p s \ P ((caps_of_state s) (p \ cap.NullCap))) \ P (caps_of_state s)" @@ -1019,10 +1019,10 @@ locale Finalise_AI_3 = Finalise_AI_2 a b crunches suspend, unbind_maybe_notification, unbind_notification for irq_node[wp]: "\s. P (interrupt_irq_node s)" - (wp: crunch_wps select_wp simp: crunch_simps) + (wp: crunch_wps simp: crunch_simps) crunch irq_node[wp]: deleting_irq_handler "\s. P (interrupt_irq_node s)" - (wp: crunch_wps select_wp simp: crunch_simps) + (wp: crunch_wps simp: crunch_simps) lemmas cancel_all_ipc_cte_irq_node[wp] = hoare_use_eq_irq_node [OF cancel_all_ipc_irq_node cancel_all_ipc_cte_wp_at] diff --git a/proof/invariant-abstract/Invariants_AI.thy b/proof/invariant-abstract/Invariants_AI.thy index 2edeb99a23..10dd21d71f 100644 --- a/proof/invariant-abstract/Invariants_AI.thy +++ b/proof/invariant-abstract/Invariants_AI.thy @@ -3092,8 +3092,7 @@ lemma real_cte_at_typ_valid: lemma dmo_aligned[wp]: "do_machine_op f \pspace_aligned\" apply (simp add: do_machine_op_def split_def) - apply (wp select_wp) - apply (clarsimp simp: pspace_aligned_def) + apply wpsimp done lemma cte_wp_at_eqD2: diff --git a/proof/invariant-abstract/IpcCancel_AI.thy b/proof/invariant-abstract/IpcCancel_AI.thy index 9261e1ab21..05e86eb7ff 100644 --- a/proof/invariant-abstract/IpcCancel_AI.thy +++ b/proof/invariant-abstract/IpcCancel_AI.thy @@ -196,7 +196,7 @@ lemma update_restart_pc_has_reply_cap[wp]: done crunch st_tcb_at_simple[wp]: reply_cancel_ipc "st_tcb_at simple t" - (wp: crunch_wps select_wp sts_st_tcb_at_cases thread_set_no_change_tcb_state + (wp: crunch_wps sts_st_tcb_at_cases thread_set_no_change_tcb_state simp: crunch_simps unless_def) lemma cancel_ipc_simple [wp]: @@ -230,7 +230,7 @@ context IpcCancel_AI begin crunch typ_at[wp]: cancel_ipc, reply_cancel_ipc, unbind_maybe_notification "\(s :: 'a state). P (typ_at T p s)" - (wp: crunch_wps hoare_vcg_if_splitE select_wp + (wp: crunch_wps hoare_vcg_if_splitE simp: crunch_simps unless_def) lemma cancel_ipc_tcb [wp]: @@ -437,7 +437,7 @@ lemma reply_cancel_ipc_invs: (cap_delete_one p :: (unit,'z::state_ext) s_monad) \\rv. invs\" shows "\invs\ (reply_cancel_ipc t :: (unit,'z::state_ext) s_monad) \\rv. invs\" apply (simp add: reply_cancel_ipc_def) - apply (wp delete select_wp) + apply (wp delete) apply (rule_tac Q="\rv. invs" in hoare_post_imp) apply (fastforce simp: emptyable_def dest: reply_slot_not_descendant) apply (wp thread_set_invs_trivial) @@ -527,15 +527,15 @@ lemma no_refs_simple_strg: crunch it[wp]: cancel_all_ipc "\s. P (idle_thread s)" - (wp: crunch_wps select_wp simp: unless_def crunch_simps) + (wp: crunch_wps simp: unless_def crunch_simps) crunch it[wp]: cancel_all_signals, fast_finalise, unbind_notification "\s. P (idle_thread s)" - (wp: crunch_wps select_wp simp: unless_def crunch_simps) + (wp: crunch_wps simp: unless_def crunch_simps) context IpcCancel_AI begin crunch it[wp]: reply_cancel_ipc "\(s::'a state). P (idle_thread s)" - (wp: crunch_wps select_wp simp: unless_def crunch_simps) + (wp: crunch_wps simp: unless_def crunch_simps) crunch it[wp]: cancel_ipc "\(s :: 'a state). P (idle_thread s)" @@ -575,7 +575,7 @@ lemma (in delete_one_abs) reply_cancel_ipc_no_reply_cap[wp]: delete_one_deletes delete_one_caps_of_state) apply (clarsimp simp: has_reply_cap_def cte_wp_at_caps_of_state is_reply_cap_to_def) apply (case_tac "(aa, ba) = (a, b)",simp_all)[1] - apply (wp hoare_vcg_all_lift select_wp | simp del: split_paired_All)+ + apply (wp hoare_vcg_all_lift | simp del: split_paired_All)+ apply (rule_tac Q="\_ s. invs s \ tcb_at t s" in hoare_post_imp) apply (erule conjE) apply (frule(1) reply_cap_descends_from_master) @@ -641,7 +641,7 @@ lemma (in delete_one_pre) reply_cancel_ipc_cte_wp_at_preserved: "(\cap. P cap \ \ can_fast_finalise cap) \ \cte_wp_at P p\ (reply_cancel_ipc t :: (unit,'a) s_monad) \\rv. cte_wp_at P p\" unfolding reply_cancel_ipc_def - apply (wpsimp wp: select_wp delete_one_cte_wp_at_preserved) + apply (wpsimp wp: delete_one_cte_wp_at_preserved) apply (rule_tac Q="\_. cte_wp_at P p" in hoare_post_imp, clarsimp) apply (wpsimp wp: thread_set_cte_wp_at_trivial simp: ran_tcb_cap_cases) apply assumption @@ -735,7 +735,7 @@ lemma reply_cancel_ipc_bound_tcb_at[wp]: reply_cancel_ipc p \\_. bound_tcb_at P t\" unfolding reply_cancel_ipc_def - apply (wpsimp wp: cap_delete_one_bound_tcb_at select_inv select_wp) + apply (wpsimp wp: cap_delete_one_bound_tcb_at select_inv) apply (rule_tac Q="\_. bound_tcb_at P t and valid_mdb and valid_objs and tcb_at p" in hoare_strengthen_post) apply (wpsimp wp: thread_set_no_change_tcb_pred thread_set_mdb) apply (fastforce simp:tcb_cap_cases_def) diff --git a/proof/invariant-abstract/Ipc_AI.thy b/proof/invariant-abstract/Ipc_AI.thy index 3fcd5f30dc..d78d399685 100644 --- a/proof/invariant-abstract/Ipc_AI.thy +++ b/proof/invariant-abstract/Ipc_AI.thy @@ -1439,9 +1439,7 @@ lemmas get_tcb_ko_atI = get_tcb_ko_at [THEN iffD1] crunch "distinct" [wp]: set_mrs pspace_distinct - (wp: select_wp hoare_vcg_split_case_option mapM_wp - hoare_drop_imps refl - simp: zipWithM_x_mapM) + (wp: mapM_wp simp: zipWithM_x_mapM) crunch "distinct" [wp]: copy_mrs pspace_distinct @@ -2957,7 +2955,7 @@ crunch cap_to[wp]: receive_signal "ex_nonz_cap_to p" (wp: crunch_wps) crunch mdb[wp]: set_message_info valid_mdb - (wp: select_wp crunch_wps mapM_wp') + (wp: crunch_wps mapM_wp') lemma ep_queue_cap_to: "\ ko_at (Endpoint ep) p s; invs s; diff --git a/proof/invariant-abstract/LevityCatch_AI.thy b/proof/invariant-abstract/LevityCatch_AI.thy index fc826a6490..10b229f813 100644 --- a/proof/invariant-abstract/LevityCatch_AI.thy +++ b/proof/invariant-abstract/LevityCatch_AI.thy @@ -67,12 +67,12 @@ lemma const_on_failure_wp: happen in goals that are stated by crunch. *) lemma select_ext_weak_wp[wp]: "\\s. \x\S. Q x s\ select_ext a S \Q\" - by (wpsimp simp: select_ext_def wp: select_wp) + by (wpsimp simp: select_ext_def) (* The "real" wp rule for select_ext, requires det_ext state: *) lemma select_ext_wp[wp]: "\\s. a s \ S \ Q (a s) s\ select_ext a S \Q\" unfolding select_ext_def unwrap_ext_det_ext_ext_def - by (wpsimp simp: select_switch_det_ext_ext_def wp: select_wp) + by (wpsimp simp: select_switch_det_ext_ext_def) end diff --git a/proof/invariant-abstract/RISCV64/ArchArch_AI.thy b/proof/invariant-abstract/RISCV64/ArchArch_AI.thy index 07893616b1..a9f5859b29 100644 --- a/proof/invariant-abstract/RISCV64/ArchArch_AI.thy +++ b/proof/invariant-abstract/RISCV64/ArchArch_AI.thy @@ -998,7 +998,7 @@ crunch_ignore (add: select_ext find_vspace_for_asid) crunch inv [wp]: arch_decode_invocation "P" - (wp: crunch_wps select_wp select_ext_weak_wp simp: crunch_simps) + (wp: crunch_wps select_ext_weak_wp simp: crunch_simps) declare lookup_slot_for_cnode_op_cap_to [wp] @@ -1271,7 +1271,7 @@ lemma decode_asid_control_invocation_wf[wp]: apply (simp add: lookup_target_slot_def) apply wp apply (clarsimp simp: cte_wp_at_def) - apply (wpsimp wp: ensure_no_children_sp select_ext_weak_wp select_wp whenE_throwError_wp)+ + apply (wpsimp wp: ensure_no_children_sp select_ext_weak_wp whenE_throwError_wp)+ apply (rule conjI, fastforce) apply (cases excaps, simp) apply (case_tac list, simp) diff --git a/proof/invariant-abstract/RISCV64/ArchDetSchedSchedule_AI.thy b/proof/invariant-abstract/RISCV64/ArchDetSchedSchedule_AI.thy index ebd006b100..6e43b06c0e 100644 --- a/proof/invariant-abstract/RISCV64/ArchDetSchedSchedule_AI.thy +++ b/proof/invariant-abstract/RISCV64/ArchDetSchedSchedule_AI.thy @@ -193,7 +193,7 @@ crunch valid_etcbs [wp, DetSchedSchedule_AI_assms]: crunch simple_sched_action [wp, DetSchedSchedule_AI_assms]: arch_finalise_cap, prepare_thread_delete simple_sched_action - (wp: hoare_drop_imps mapM_x_wp mapM_wp select_wp subset_refl + (wp: hoare_drop_imps mapM_x_wp mapM_wp subset_refl simp: unless_def if_fun_split) crunch valid_sched [wp, DetSchedSchedule_AI_assms]: diff --git a/proof/invariant-abstract/RISCV64/ArchFinalise_AI.thy b/proof/invariant-abstract/RISCV64/ArchFinalise_AI.thy index d92fa381ea..c8b3ec5785 100644 --- a/proof/invariant-abstract/RISCV64/ArchFinalise_AI.thy +++ b/proof/invariant-abstract/RISCV64/ArchFinalise_AI.thy @@ -1227,7 +1227,7 @@ lemma (* replace_cap_invs_arch_update *)[Finalise_AI_asms]: lemma dmo_pred_tcb_at[wp]: "do_machine_op mop \\s. P (pred_tcb_at f Q t s)\" apply (simp add: do_machine_op_def split_def) - apply (wp select_wp) + apply wp apply (clarsimp simp: pred_tcb_at_def obj_at_def) done diff --git a/proof/invariant-abstract/RISCV64/ArchVSpaceEntries_AI.thy b/proof/invariant-abstract/RISCV64/ArchVSpaceEntries_AI.thy index 95ab70f3e7..ec72a6be23 100644 --- a/proof/invariant-abstract/RISCV64/ArchVSpaceEntries_AI.thy +++ b/proof/invariant-abstract/RISCV64/ArchVSpaceEntries_AI.thy @@ -106,7 +106,7 @@ crunch valid_vspace_objs'[wp]: set_simple_ko "valid_vspace_objs'" (wp: crunch_wps) crunch valid_vspace_objs'[wp]: finalise_cap, cap_swap_for_delete, empty_slot "valid_vspace_objs'" - (wp: crunch_wps select_wp preemption_point_inv simp: crunch_simps unless_def ignore:set_object) + (wp: crunch_wps preemption_point_inv simp: crunch_simps unless_def ignore:set_object) lemma preemption_point_valid_vspace_objs'[wp]: "\valid_vspace_objs'\ preemption_point \\rv. valid_vspace_objs'\" @@ -233,7 +233,7 @@ lemma perform_asid_pool_invocation_valid_vspace_objs'[wp]: crunch valid_vspace_objs'[wp]: perform_asid_pool_invocation, perform_asid_control_invocation "valid_vspace_objs'" (ignore: delete_objects set_object - wp: static_imp_wp select_wp crunch_wps + wp: static_imp_wp crunch_wps simp: crunch_simps unless_def) lemma pte_range_interD: @@ -309,7 +309,7 @@ lemma handle_invocation_valid_vspace_objs'[wp]: crunch valid_vspace_objs'[wp]: activate_thread,switch_to_thread, handle_hypervisor_fault, switch_to_idle_thread, handle_call, handle_recv, handle_reply, handle_send, handle_yield, handle_interrupt "valid_vspace_objs'" - (simp: crunch_simps wp: crunch_wps alternative_wp select_wp OR_choice_weak_wp select_ext_weak_wp + (simp: crunch_simps wp: crunch_wps OR_choice_weak_wp select_ext_weak_wp ignore: without_preemption getActiveIRQ resetTimer ackInterrupt OR_choice set_scheduler_action) @@ -320,8 +320,7 @@ lemma handle_event_valid_vspace_objs'[wp]: lemma schedule_valid_vspace_objs'[wp]: "\valid_vspace_objs'\ schedule :: (unit,unit) s_monad \\_. valid_vspace_objs'\" apply (simp add: schedule_def allActiveTCBs_def) - apply (wp alternative_wp select_wp) - apply simp + apply wpsimp done lemma call_kernel_valid_vspace_objs'[wp]: diff --git a/proof/invariant-abstract/RISCV64/Machine_AI.thy b/proof/invariant-abstract/RISCV64/Machine_AI.thy index 443e646067..f24f14c5a8 100644 --- a/proof/invariant-abstract/RISCV64/Machine_AI.thy +++ b/proof/invariant-abstract/RISCV64/Machine_AI.thy @@ -184,7 +184,7 @@ definition "irq_state_independent P \ \f s. P s \ lemma getActiveIRQ_inv [wp]: "\irq_state_independent P\ \ \P\ getActiveIRQ in_kernel \\rv. P\" apply (simp add: getActiveIRQ_def) - apply (wp alternative_wp select_wp) + apply wp apply (simp add: irq_state_independent_def) done @@ -329,7 +329,7 @@ lemma getActiveIRQ_le_maxIRQ': getActiveIRQ in_kernel \\rv s. \x. rv = Some x \ x \ maxIRQ\" apply (simp add: getActiveIRQ_def) - apply (wp alternative_wp select_wp) + apply wp apply clarsimp apply (rule ccontr) apply (simp add: linorder_not_le) @@ -338,7 +338,7 @@ lemma getActiveIRQ_le_maxIRQ': lemma getActiveIRQ_neq_non_kernel: "\\\ getActiveIRQ True \\rv s. rv \ Some ` non_kernel_IRQs \" apply (simp add: getActiveIRQ_def) - apply (wp alternative_wp select_wp) + apply wp apply auto done diff --git a/proof/invariant-abstract/Schedule_AI.thy b/proof/invariant-abstract/Schedule_AI.thy index 059dd5be19..26d95425fc 100644 --- a/proof/invariant-abstract/Schedule_AI.thy +++ b/proof/invariant-abstract/Schedule_AI.thy @@ -177,8 +177,8 @@ locale Schedule_AI_U = Schedule_AI "TYPE(unit)" lemma (in Schedule_AI_U) schedule_invs[wp]: "\invs\ (Schedule_A.schedule :: (unit,unit) s_monad) \\rv. invs\" apply (simp add: Schedule_A.schedule_def allActiveTCBs_def) - apply (wp OR_choice_weak_wp alternative_wp dmo_invs thread_get_inv - do_machine_op_tcb select_ext_weak_wp select_wp when_def + apply (wp OR_choice_weak_wp dmo_invs thread_get_inv + do_machine_op_tcb select_ext_weak_wp when_def | clarsimp simp: getActiveTCB_def get_tcb_def)+ done @@ -202,9 +202,8 @@ lemma (in Schedule_AI_U) schedule_ct_activateable[wp]: done show ?thesis apply (simp add: Schedule_A.schedule_def allActiveTCBs_def) - apply (wp alternative_wp - select_ext_weak_wp select_wp stt_activatable stit_activatable - | simp add: P Q)+ + apply (wp select_ext_weak_wp stt_activatable stit_activatable + | simp add: P Q)+ apply (clarsimp simp: getActiveTCB_def ct_in_state_def) apply (rule conjI) apply clarsimp diff --git a/proof/invariant-abstract/Tcb_AI.thy b/proof/invariant-abstract/Tcb_AI.thy index f518e4d30d..d20c73f832 100644 --- a/proof/invariant-abstract/Tcb_AI.thy +++ b/proof/invariant-abstract/Tcb_AI.thy @@ -920,9 +920,6 @@ lemma (in Tcb_AI) decode_set_tls_base_wf: apply wpsimp done -declare alternativeE_wp[wp] -declare alternativeE_R_wp[wp] - (*FIXME Move up*) lemma OR_choice_E_weak_wp: "\P\ f \ g \Q\,- \ \P\ OR_choice b f g \Q\,-" apply (simp add: validE_R_def validE_def OR_choice_weak_wp) diff --git a/proof/invariant-abstract/X64/ArchArch_AI.thy b/proof/invariant-abstract/X64/ArchArch_AI.thy index 92c9e31146..a5020d6de0 100644 --- a/proof/invariant-abstract/X64/ArchArch_AI.thy +++ b/proof/invariant-abstract/X64/ArchArch_AI.thy @@ -1011,7 +1011,7 @@ lemma create_mapping_entries_inv [wp]: crunch_ignore (add: select_ext) crunch inv [wp]: arch_decode_invocation "P" - (wp: crunch_wps select_wp select_ext_weak_wp simp: crunch_simps) + (wp: crunch_wps select_ext_weak_wp simp: crunch_simps) lemma create_mappings_empty [wp]: @@ -1576,7 +1576,7 @@ lemma arch_decode_inv_wf[wp]: apply (simp add: arch_decode_invocation_def Let_def split_def cong: if_cong split del: if_split) apply (rule hoare_pre) - apply ((wp whenE_throwError_wp check_vp_wpR ensure_empty_stronger select_wp select_ext_weak_wp + apply ((wp whenE_throwError_wp check_vp_wpR ensure_empty_stronger select_ext_weak_wp | wpc | simp add: valid_arch_inv_def valid_apinv_def)+)[1] apply (simp add: valid_arch_inv_def valid_apinv_def) apply (intro allI impI ballI) @@ -1620,7 +1620,7 @@ lemma arch_decode_inv_wf[wp]: apply (simp add: lookup_target_slot_def) apply wp apply (clarsimp simp: cte_wp_at_def asid_wf_high) - apply (wp ensure_no_children_sp select_ext_weak_wp select_wp whenE_throwError_wp | wpc | simp)+ + apply (wp ensure_no_children_sp select_ext_weak_wp whenE_throwError_wp | wpc | simp)+ apply clarsimp apply (rule conjI, fastforce) apply (cases excaps, simp) diff --git a/proof/invariant-abstract/X64/ArchDetSchedSchedule_AI.thy b/proof/invariant-abstract/X64/ArchDetSchedSchedule_AI.thy index 5f8793a5b8..579035e2a1 100644 --- a/proof/invariant-abstract/X64/ArchDetSchedSchedule_AI.thy +++ b/proof/invariant-abstract/X64/ArchDetSchedSchedule_AI.thy @@ -243,7 +243,7 @@ lemma flush_table_simple_sched_action[wp]: "\simple_sched_action\valid_sched\ flush_table a b c d \\rv. valid_sched\" diff --git a/proof/invariant-abstract/X64/ArchFinalise_AI.thy b/proof/invariant-abstract/X64/ArchFinalise_AI.thy index 2052939a4a..5d612a2ed2 100644 --- a/proof/invariant-abstract/X64/ArchFinalise_AI.thy +++ b/proof/invariant-abstract/X64/ArchFinalise_AI.thy @@ -666,7 +666,7 @@ lemma flush_table_pred_tcb_at: "\\s. pred_tcb_at proj P t s\s. P (interrupt_irq_node s)" - (wp: crunch_wps select_wp simp: crunch_simps) + (wp: crunch_wps simp: crunch_simps) crunch pred_tcb_at[wp]: arch_finalise_cap "pred_tcb_at proj P t" (simp: crunch_simps set_arch_obj_simps wp: crunch_wps set_aobject_pred_tcb_at diff --git a/proof/invariant-abstract/X64/ArchVSpaceEntries_AI.thy b/proof/invariant-abstract/X64/ArchVSpaceEntries_AI.thy index e71b9742e9..6aebdc7877 100644 --- a/proof/invariant-abstract/X64/ArchVSpaceEntries_AI.thy +++ b/proof/invariant-abstract/X64/ArchVSpaceEntries_AI.thy @@ -318,7 +318,7 @@ crunch valid_vspace_objs'[wp]: set_simple_ko "valid_vspace_objs'" (wp: crunch_wps) crunch valid_vspace_objs'[wp]: finalise_cap, cap_swap_for_delete, empty_slot "valid_vspace_objs'" - (wp: crunch_wps select_wp preemption_point_inv simp: crunch_simps unless_def ignore:set_object) + (wp: crunch_wps preemption_point_inv simp: crunch_simps unless_def ignore:set_object) lemma preemption_point_valid_vspace_objs'[wp]: "\valid_vspace_objs'\ preemption_point \\rv. valid_vspace_objs'\" @@ -556,7 +556,7 @@ lemma invoke_untyped_valid_vspace_objs'[wp]: crunch valid_vspace_objs'[wp]: perform_asid_pool_invocation, perform_asid_control_invocation "valid_vspace_objs'" (ignore: delete_objects set_object - wp: static_imp_wp select_wp crunch_wps + wp: static_imp_wp crunch_wps simp: crunch_simps unless_def) lemma pte_range_interD: @@ -703,7 +703,7 @@ lemma handle_invocation_valid_vspace_objs'[wp]: crunch valid_vspace_objs'[wp]: activate_thread,switch_to_thread, handle_hypervisor_fault, switch_to_idle_thread, handle_call, handle_recv, handle_reply, handle_send, handle_yield, handle_interrupt "valid_vspace_objs'" - (simp: crunch_simps wp: crunch_wps alternative_wp select_wp OR_choice_weak_wp select_ext_weak_wp + (simp: crunch_simps wp: crunch_wps OR_choice_weak_wp select_ext_weak_wp ignore: without_preemption getActiveIRQ resetTimer ackInterrupt getFaultAddress OR_choice set_scheduler_action) @@ -714,8 +714,7 @@ lemma handle_event_valid_vspace_objs'[wp]: lemma schedule_valid_vspace_objs'[wp]: "\valid_vspace_objs'\ schedule :: (unit,unit) s_monad \\_. valid_vspace_objs'\" apply (simp add: schedule_def allActiveTCBs_def) - apply (wp alternative_wp select_wp) - apply simp + apply wpsimp done lemma call_kernel_valid_vspace_objs'[wp]: diff --git a/proof/invariant-abstract/X64/Machine_AI.thy b/proof/invariant-abstract/X64/Machine_AI.thy index 9ff693faeb..efd31cf7d0 100644 --- a/proof/invariant-abstract/X64/Machine_AI.thy +++ b/proof/invariant-abstract/X64/Machine_AI.thy @@ -184,7 +184,7 @@ definition "irq_state_independent P \ \f s. P s \ lemma getActiveIRQ_inv [wp]: "\irq_state_independent P\ \ \P\ getActiveIRQ in_kernel \\rv. P\" apply (simp add: getActiveIRQ_def) - apply (wp alternative_wp select_wp) + apply wp apply (simp add: irq_state_independent_def) done @@ -369,7 +369,7 @@ lemma getActiveIRQ_le_maxIRQ': getActiveIRQ in_kernel \\rv s. \x. rv = Some x \ x \ maxIRQ\" apply (simp add: getActiveIRQ_def) - apply (wp alternative_wp select_wp) + apply wp apply clarsimp apply (rule ccontr) apply (simp add: linorder_not_le) @@ -379,14 +379,13 @@ lemma getActiveIRQ_le_maxIRQ': lemma getActiveIRQ_neq_Some0xFF': "\\\ getActiveIRQ in_kernel \\rv s. rv \ Some 0x3FF\" apply (simp add: getActiveIRQ_def) - apply (wp alternative_wp select_wp) - apply simp + apply wpsimp done lemma getActiveIRQ_neq_non_kernel: "\\\ getActiveIRQ True \\rv s. rv \ Some ` non_kernel_IRQs \" apply (simp add: getActiveIRQ_def) - apply (wp alternative_wp select_wp) + apply wp apply auto done diff --git a/proof/refine/AARCH64/InterruptAcc_R.thy b/proof/refine/AARCH64/InterruptAcc_R.thy index 538ba8d28f..3f046d309e 100644 --- a/proof/refine/AARCH64/InterruptAcc_R.thy +++ b/proof/refine/AARCH64/InterruptAcc_R.thy @@ -115,7 +115,7 @@ lemma preemptionPoint_inv: shows "\P\ preemptionPoint \\_. P\" using assms apply (simp add: preemptionPoint_def setWorkUnits_def getWorkUnits_def modifyWorkUnits_def) apply (wpc - | wp whenE_wp hoare_seq_ext [OF _ select_inv] alternative_wp hoare_drop_imps + | wp whenE_wp hoare_seq_ext [OF _ select_inv] hoare_drop_imps | simp)+ done diff --git a/proof/refine/AARCH64/IpcCancel_R.thy b/proof/refine/AARCH64/IpcCancel_R.thy index 8b9b07b2a3..66f5a1432e 100644 --- a/proof/refine/AARCH64/IpcCancel_R.thy +++ b/proof/refine/AARCH64/IpcCancel_R.thy @@ -1365,7 +1365,7 @@ interpretation Arch . crunches cancel_ipc for pspace_aligned[wp]: "pspace_aligned :: det_state \ _" and pspace_distinct[wp]: "pspace_distinct :: det_state \ _" - (simp: crunch_simps wp: crunch_wps select_wp) + (simp: crunch_simps wp: crunch_wps) end diff --git a/proof/refine/AARCH64/Ipc_R.thy b/proof/refine/AARCH64/Ipc_R.thy index e77593c652..db8c4450bd 100644 --- a/proof/refine/AARCH64/Ipc_R.thy +++ b/proof/refine/AARCH64/Ipc_R.thy @@ -2571,7 +2571,7 @@ lemmas setMessageInfo_typ_ats[wp] = typ_at_lifts [OF setMessageInfo_typ_at'] declare tl_drop_1[simp] crunch cur[wp]: cancel_ipc "cur_tcb" - (wp: select_wp crunch_wps simp: crunch_simps) + (wp: crunch_wps simp: crunch_simps) lemma valid_sched_weak_strg: "valid_sched s \ weak_valid_sched_action s" diff --git a/proof/refine/AARCH64/KHeap_R.thy b/proof/refine/AARCH64/KHeap_R.thy index 6faa3d6a59..4121ed32c4 100644 --- a/proof/refine/AARCH64/KHeap_R.thy +++ b/proof/refine/AARCH64/KHeap_R.thy @@ -2184,21 +2184,21 @@ lemma valid_globals_cte_wpD': lemma dmo_aligned'[wp]: "\pspace_aligned'\ doMachineOp f \\_. pspace_aligned'\" apply (simp add: doMachineOp_def split_def) - apply (wp select_wp) + apply wp apply clarsimp done lemma dmo_distinct'[wp]: "\pspace_distinct'\ doMachineOp f \\_. pspace_distinct'\" apply (simp add: doMachineOp_def split_def) - apply (wp select_wp) + apply wp apply clarsimp done lemma dmo_valid_objs'[wp]: "\valid_objs'\ doMachineOp f \\_. valid_objs'\" apply (simp add: doMachineOp_def split_def) - apply (wp select_wp) + apply wp apply clarsimp done @@ -2206,7 +2206,7 @@ lemma dmo_inv': assumes R: "\P. \P\ f \\_. P\" shows "\P\ doMachineOp f \\_. P\" apply (simp add: doMachineOp_def split_def) - apply (wp select_wp) + apply wp apply clarsimp apply (drule in_inv_by_hoareD [OF R]) apply simp diff --git a/proof/refine/AARCH64/Refine.thy b/proof/refine/AARCH64/Refine.thy index 5a33212dc2..1eb545922c 100644 --- a/proof/refine/AARCH64/Refine.thy +++ b/proof/refine/AARCH64/Refine.thy @@ -291,18 +291,18 @@ definition lemma do_user_op_valid_list:"\valid_list\ do_user_op f tc \\_. valid_list\" unfolding do_user_op_def - apply (wp select_wp | simp add: split_def)+ + apply (wp | simp add: split_def)+ done lemma do_user_op_valid_sched:"\valid_sched\ do_user_op f tc \\_. valid_sched\" unfolding do_user_op_def - apply (wp select_wp | simp add: split_def)+ + apply (wp | simp add: split_def)+ done lemma do_user_op_sched_act: "\\s. P (scheduler_action s)\ do_user_op f tc \\_ s. P (scheduler_action s)\" unfolding do_user_op_def - apply (wp select_wp | simp add: split_def)+ + apply (wp | simp add: split_def)+ done lemma do_user_op_invs2: @@ -433,7 +433,7 @@ lemma kernelEntry_invs': (\s. 0 < ksDomainTime s) and valid_domain_list' \" apply (simp add: kernelEntry_def) apply (wp ckernel_invs callKernel_domain_time_left - threadSet_invs_trivial threadSet_ct_running' select_wp + threadSet_invs_trivial threadSet_ct_running' TcbAcc_R.dmo_invs' static_imp_wp doMachineOp_ct_in_state' doMachineOp_sch_act_simple callKernel_domain_time_left @@ -512,7 +512,7 @@ lemma doUserOp_invs': (\s. ksSchedulerAction s = ResumeCurrentThread) and ct_running' and (\s. 0 < ksDomainTime s) and valid_domain_list'\" apply (simp add: doUserOp_def split_def ex_abs_def) - apply (wp device_update_invs' doMachineOp_ct_in_state' select_wp + apply (wp device_update_invs' doMachineOp_ct_in_state' | (wp (once) dmo_invs', wpsimp simp: no_irq_modify device_memory_update_def user_memory_update_def))+ apply (clarsimp simp: user_memory_update_def simpler_modify_def @@ -659,7 +659,7 @@ lemma entry_corres: apply (rule hoare_strengthen_post, rule ckernel_invs, simp add: invs'_def cur_tcb'_def) apply (wp thread_set_invs_trivial thread_set_ct_running threadSet_invs_trivial threadSet_ct_running' - select_wp thread_set_not_state_valid_sched static_imp_wp + thread_set_not_state_valid_sched static_imp_wp hoare_vcg_disj_lift ct_in_state_thread_state_lift | simp add: tcb_cap_cases_def ct_in_state'_def thread_set_no_change_tcb_state | (wps, wp threadSet_st_tcb_at2) )+ @@ -827,7 +827,7 @@ lemma domain_list_rel_eq: by (clarsimp simp: state_relation_def) crunch valid_objs': doUserOp, checkActiveIRQ valid_objs' - (wp: crunch_wps select_wp) + (wp: crunch_wps) lemma ckernel_invariant: "ADT_H uop \ full_invs'" diff --git a/proof/refine/AARCH64/Schedule_R.thy b/proof/refine/AARCH64/Schedule_R.thy index f210ca2fa0..0ade5d66ca 100644 --- a/proof/refine/AARCH64/Schedule_R.thy +++ b/proof/refine/AARCH64/Schedule_R.thy @@ -42,7 +42,7 @@ proof - apply (auto simp add: bind_def alternative_def return_def split_def prod_eq_iff) done have Q: "\P\ (do x \ f; return (Some x) od) \ return None \\rv. if rv \ None then \ else P\" - by (wp alternative_wp | simp)+ + by (wp | simp)+ show ?thesis using p apply (induct xs) apply (simp add: y del: dc_simp) diff --git a/proof/refine/AARCH64/Untyped_R.thy b/proof/refine/AARCH64/Untyped_R.thy index 224f61bfc1..02cefb891d 100644 --- a/proof/refine/AARCH64/Untyped_R.thy +++ b/proof/refine/AARCH64/Untyped_R.thy @@ -3202,7 +3202,7 @@ lemma createNewCaps_valid_cap': lemma dmo_ctes_of[wp]: "\\s. P (ctes_of s)\ doMachineOp mop \\rv s. P (ctes_of s)\" - by (simp add: doMachineOp_def split_def | wp select_wp)+ + by (simp add: doMachineOp_def split_def | wp)+ lemma createNewCaps_ranges: "\\s. range_cover ptr sz (APIType_capBits ty us) n \ 0 diff --git a/proof/refine/ARM/InterruptAcc_R.thy b/proof/refine/ARM/InterruptAcc_R.thy index 123ac7f82d..5d5bd979c7 100644 --- a/proof/refine/ARM/InterruptAcc_R.thy +++ b/proof/refine/ARM/InterruptAcc_R.thy @@ -114,7 +114,7 @@ lemma preemptionPoint_inv: shows "\P\ preemptionPoint \\_. P\" using assms apply (simp add: preemptionPoint_def setWorkUnits_def getWorkUnits_def modifyWorkUnits_def) apply (wpc - | wp whenE_wp hoare_seq_ext [OF _ select_inv] alternative_wp hoare_drop_imps + | wp whenE_wp hoare_seq_ext [OF _ select_inv] hoare_drop_imps | simp)+ done diff --git a/proof/refine/ARM/Ipc_R.thy b/proof/refine/ARM/Ipc_R.thy index 49ff66feec..7b973a8134 100644 --- a/proof/refine/ARM/Ipc_R.thy +++ b/proof/refine/ARM/Ipc_R.thy @@ -2514,7 +2514,7 @@ lemmas setMessageInfo_typ_ats[wp] = typ_at_lifts [OF setMessageInfo_typ_at'] declare tl_drop_1[simp] crunch cur[wp]: cancel_ipc "cur_tcb" - (wp: select_wp crunch_wps simp: crunch_simps) + (wp: crunch_wps simp: crunch_simps) crunch valid_objs'[wp]: asUser "valid_objs'" diff --git a/proof/refine/ARM/KHeap_R.thy b/proof/refine/ARM/KHeap_R.thy index d5235057c1..2708b28ab0 100644 --- a/proof/refine/ARM/KHeap_R.thy +++ b/proof/refine/ARM/KHeap_R.thy @@ -2076,21 +2076,21 @@ lemma valid_globals_cte_wpD': lemma dmo_aligned'[wp]: "\pspace_aligned'\ doMachineOp f \\_. pspace_aligned'\" apply (simp add: doMachineOp_def split_def) - apply (wp select_wp) + apply wp apply clarsimp done lemma dmo_distinct'[wp]: "\pspace_distinct'\ doMachineOp f \\_. pspace_distinct'\" apply (simp add: doMachineOp_def split_def) - apply (wp select_wp) + apply wp apply clarsimp done lemma dmo_valid_objs'[wp]: "\valid_objs'\ doMachineOp f \\_. valid_objs'\" apply (simp add: doMachineOp_def split_def) - apply (wp select_wp) + apply wp apply clarsimp done @@ -2098,7 +2098,7 @@ lemma dmo_inv': assumes R: "\P. \P\ f \\_. P\" shows "\P\ doMachineOp f \\_. P\" apply (simp add: doMachineOp_def split_def) - apply (wp select_wp) + apply wp apply clarsimp apply (drule in_inv_by_hoareD [OF R]) apply simp diff --git a/proof/refine/ARM/Refine.thy b/proof/refine/ARM/Refine.thy index 6fadade1cf..c94879f165 100644 --- a/proof/refine/ARM/Refine.thy +++ b/proof/refine/ARM/Refine.thy @@ -296,18 +296,18 @@ definition lemma do_user_op_valid_list:"\valid_list\ do_user_op f tc \\_. valid_list\" unfolding do_user_op_def - apply (wp select_wp | simp add: split_def)+ + apply (wp | simp add: split_def)+ done lemma do_user_op_valid_sched:"\valid_sched\ do_user_op f tc \\_. valid_sched\" unfolding do_user_op_def - apply (wp select_wp | simp add: split_def)+ + apply (wp | simp add: split_def)+ done lemma do_user_op_sched_act: "\\s. P (scheduler_action s)\ do_user_op f tc \\_ s. P (scheduler_action s)\" unfolding do_user_op_def - apply (wp select_wp | simp add: split_def)+ + apply (wp | simp add: split_def)+ done lemma do_user_op_invs2: @@ -421,7 +421,7 @@ lemma kernelEntry_invs': (\s. 0 < ksDomainTime s) and valid_domain_list' \" apply (simp add: kernelEntry_def) apply (wp ckernel_invs callKernel_valid_duplicates' callKernel_domain_time_left - threadSet_invs_trivial threadSet_ct_running' select_wp + threadSet_invs_trivial threadSet_ct_running' TcbAcc_R.dmo_invs' static_imp_wp callKernel_domain_time_left | clarsimp simp: user_memory_update_def no_irq_def tcb_at_invs' @@ -499,7 +499,7 @@ lemma doUserOp_invs': (\s. ksSchedulerAction s = ResumeCurrentThread) and ct_running' and (\s. 0 < ksDomainTime s) and valid_domain_list'\" apply (simp add: doUserOp_def split_def ex_abs_def) - apply (wp device_update_invs' select_wp + apply (wp device_update_invs' | (wp (once) dmo_invs', wpsimp simp: no_irq_modify device_memory_update_def user_memory_update_def))+ apply (clarsimp simp: user_memory_update_def simpler_modify_def @@ -513,7 +513,7 @@ lemma doUserOp_valid_duplicates': doUserOp f tc \\_ s. vs_valid_duplicates' (ksPSpace s)\" apply (simp add: doUserOp_def split_def) - apply (wp dmo_invs' select_wp) + apply (wp dmo_invs') apply clarsimp done @@ -644,7 +644,7 @@ lemma entry_corres: apply (rule hoare_strengthen_post, rule ckernel_invs, simp add: invs'_def cur_tcb'_def) apply (wp thread_set_invs_trivial thread_set_ct_running threadSet_invs_trivial threadSet_ct_running' - select_wp thread_set_not_state_valid_sched static_imp_wp + thread_set_not_state_valid_sched static_imp_wp hoare_vcg_disj_lift ct_in_state_thread_state_lift | simp add: tcb_cap_cases_def ct_in_state'_def thread_set_no_change_tcb_state | (wps, wp threadSet_st_tcb_at2) )+ diff --git a/proof/refine/ARM/Schedule_R.thy b/proof/refine/ARM/Schedule_R.thy index ec634bc82c..02921fc419 100644 --- a/proof/refine/ARM/Schedule_R.thy +++ b/proof/refine/ARM/Schedule_R.thy @@ -41,7 +41,7 @@ proof - apply (auto simp add: bind_def alternative_def return_def split_def prod_eq_iff) done have Q: "\P\ (do x \ f; return (Some x) od) \ return None \\rv. if rv \ None then \ else P\" - by (wp alternative_wp | simp)+ + by (wp | simp)+ show ?thesis using p apply (induct xs) apply (simp add: y del: dc_simp) diff --git a/proof/refine/ARM/Untyped_R.thy b/proof/refine/ARM/Untyped_R.thy index eac92fa4f1..09e2b5e352 100644 --- a/proof/refine/ARM/Untyped_R.thy +++ b/proof/refine/ARM/Untyped_R.thy @@ -3181,7 +3181,7 @@ lemma createNewCaps_valid_cap': lemma dmo_ctes_of[wp]: "\\s. P (ctes_of s)\ doMachineOp mop \\rv s. P (ctes_of s)\" - by (simp add: doMachineOp_def split_def | wp select_wp)+ + by (simp add: doMachineOp_def split_def | wp)+ lemma createNewCaps_ranges: "\\s. range_cover ptr sz (APIType_capBits ty us) n \ 0 diff --git a/proof/refine/ARM_HYP/InterruptAcc_R.thy b/proof/refine/ARM_HYP/InterruptAcc_R.thy index a0708471c1..174dad753f 100644 --- a/proof/refine/ARM_HYP/InterruptAcc_R.thy +++ b/proof/refine/ARM_HYP/InterruptAcc_R.thy @@ -119,7 +119,7 @@ lemma preemptionPoint_inv: shows "\P\ preemptionPoint \\_. P\" using assms apply (simp add: preemptionPoint_def setWorkUnits_def getWorkUnits_def modifyWorkUnits_def) apply (wpc - | wp whenE_wp hoare_seq_ext [OF _ select_inv] alternative_wp hoare_drop_imps + | wp whenE_wp hoare_seq_ext [OF _ select_inv] hoare_drop_imps | simp)+ done diff --git a/proof/refine/ARM_HYP/Ipc_R.thy b/proof/refine/ARM_HYP/Ipc_R.thy index 1a27a0c08c..ce53168398 100644 --- a/proof/refine/ARM_HYP/Ipc_R.thy +++ b/proof/refine/ARM_HYP/Ipc_R.thy @@ -2641,7 +2641,7 @@ lemmas setMessageInfo_typ_ats[wp] = typ_at_lifts [OF setMessageInfo_typ_at'] declare tl_drop_1[simp] crunch cur[wp]: cancel_ipc "cur_tcb" - (wp: select_wp crunch_wps simp: crunch_simps) + (wp: crunch_wps simp: crunch_simps) crunch valid_objs'[wp]: asUser "valid_objs'" diff --git a/proof/refine/ARM_HYP/KHeap_R.thy b/proof/refine/ARM_HYP/KHeap_R.thy index 64daf32395..6eec9c3cba 100644 --- a/proof/refine/ARM_HYP/KHeap_R.thy +++ b/proof/refine/ARM_HYP/KHeap_R.thy @@ -2262,21 +2262,21 @@ lemma valid_globals_cte_wpD': lemma dmo_aligned'[wp]: "\pspace_aligned'\ doMachineOp f \\_. pspace_aligned'\" apply (simp add: doMachineOp_def split_def) - apply (wp select_wp) + apply wp apply clarsimp done lemma dmo_distinct'[wp]: "\pspace_distinct'\ doMachineOp f \\_. pspace_distinct'\" apply (simp add: doMachineOp_def split_def) - apply (wp select_wp) + apply wp apply clarsimp done lemma dmo_valid_objs'[wp]: "\valid_objs'\ doMachineOp f \\_. valid_objs'\" apply (simp add: doMachineOp_def split_def) - apply (wp select_wp) + apply wp apply clarsimp done @@ -2284,7 +2284,7 @@ lemma dmo_inv': assumes R: "\P. \P\ f \\_. P\" shows "\P\ doMachineOp f \\_. P\" apply (simp add: doMachineOp_def split_def) - apply (wp select_wp) + apply wp apply clarsimp apply (drule in_inv_by_hoareD [OF R]) apply simp diff --git a/proof/refine/ARM_HYP/Refine.thy b/proof/refine/ARM_HYP/Refine.thy index 2ec62aecd3..92a68a54c8 100644 --- a/proof/refine/ARM_HYP/Refine.thy +++ b/proof/refine/ARM_HYP/Refine.thy @@ -296,18 +296,18 @@ definition lemma do_user_op_valid_list:"\valid_list\ do_user_op f tc \\_. valid_list\" unfolding do_user_op_def - apply (wp select_wp | simp add: split_def)+ + apply (wp | simp add: split_def)+ done lemma do_user_op_valid_sched:"\valid_sched\ do_user_op f tc \\_. valid_sched\" unfolding do_user_op_def - apply (wp select_wp | simp add: split_def)+ + apply (wp | simp add: split_def)+ done lemma do_user_op_sched_act: "\\s. P (scheduler_action s)\ do_user_op f tc \\_ s. P (scheduler_action s)\" unfolding do_user_op_def - apply (wp select_wp | simp add: split_def)+ + apply (wp | simp add: split_def)+ done lemma do_user_op_invs2: @@ -422,7 +422,7 @@ lemma kernelEntry_invs': (\s. 0 < ksDomainTime s) and valid_domain_list' \" apply (simp add: kernelEntry_def) apply (wp ckernel_invs callKernel_valid_duplicates' callKernel_domain_time_left - threadSet_invs_trivial threadSet_ct_running' select_wp + threadSet_invs_trivial threadSet_ct_running' TcbAcc_R.dmo_invs' callKernel_domain_time_left static_imp_wp | clarsimp simp: user_memory_update_def no_irq_def tcb_at_invs' atcbContextSet_def @@ -504,7 +504,7 @@ lemma doUserOp_invs': (\s. ksSchedulerAction s = ResumeCurrentThread) and ct_running' and (\s. 0 < ksDomainTime s) and valid_domain_list'\" apply (simp add: doUserOp_def split_def ex_abs_def) - apply (wp device_update_invs' select_wp + apply (wp device_update_invs' | (wp (once) dmo_invs', wpsimp simp: no_irq_modify device_memory_update_def user_memory_update_def))+ apply (clarsimp simp: user_memory_update_def simpler_modify_def @@ -518,7 +518,7 @@ lemma doUserOp_valid_duplicates': doUserOp f tc \\_ s. vs_valid_duplicates' (ksPSpace s)\" apply (simp add: doUserOp_def split_def) - apply (wp dmo_invs' select_wp) + apply (wp dmo_invs') apply clarsimp done diff --git a/proof/refine/ARM_HYP/Schedule_R.thy b/proof/refine/ARM_HYP/Schedule_R.thy index bb88c5d52e..9076942689 100644 --- a/proof/refine/ARM_HYP/Schedule_R.thy +++ b/proof/refine/ARM_HYP/Schedule_R.thy @@ -41,7 +41,7 @@ proof - apply (auto simp add: bind_def alternative_def return_def split_def prod_eq_iff) done have Q: "\P\ (do x \ f; return (Some x) od) \ return None \\rv. if rv \ None then \ else P\" - by (wp alternative_wp | simp)+ + by (wp | simp)+ show ?thesis using p apply (induct xs) apply (simp add: y del: dc_simp) diff --git a/proof/refine/ARM_HYP/Untyped_R.thy b/proof/refine/ARM_HYP/Untyped_R.thy index efba360df2..721aaea69f 100644 --- a/proof/refine/ARM_HYP/Untyped_R.thy +++ b/proof/refine/ARM_HYP/Untyped_R.thy @@ -3232,7 +3232,7 @@ lemma createNewCaps_valid_cap': lemma dmo_ctes_of[wp]: "\\s. P (ctes_of s)\ doMachineOp mop \\rv s. P (ctes_of s)\" - by (simp add: doMachineOp_def split_def | wp select_wp)+ + by (simp add: doMachineOp_def split_def | wp)+ lemma createNewCaps_ranges: "\\s. range_cover ptr sz (APIType_capBits ty us) n \ 0 diff --git a/proof/refine/Move_R.thy b/proof/refine/Move_R.thy index 20a78364c6..513b51bdfc 100644 --- a/proof/refine/Move_R.thy +++ b/proof/refine/Move_R.thy @@ -207,7 +207,6 @@ lemma get_mapM_x_lower: (* Move to DetSchedDomainTime_AI *) crunch domain_list_inv[wp]: do_user_op "\s. P (domain_list s)" - (wp: select_wp) lemma next_child_child_set: "\next_child slot (cdt_list s) = Some child; valid_list s\ diff --git a/proof/refine/RISCV64/InterruptAcc_R.thy b/proof/refine/RISCV64/InterruptAcc_R.thy index 3bf412ae4e..02a1048ede 100644 --- a/proof/refine/RISCV64/InterruptAcc_R.thy +++ b/proof/refine/RISCV64/InterruptAcc_R.thy @@ -113,7 +113,7 @@ lemma preemptionPoint_inv: shows "\P\ preemptionPoint \\_. P\" using assms apply (simp add: preemptionPoint_def setWorkUnits_def getWorkUnits_def modifyWorkUnits_def) apply (wpc - | wp whenE_wp hoare_seq_ext [OF _ select_inv] alternative_wp hoare_drop_imps + | wp whenE_wp hoare_seq_ext [OF _ select_inv] hoare_drop_imps | simp)+ done diff --git a/proof/refine/RISCV64/IpcCancel_R.thy b/proof/refine/RISCV64/IpcCancel_R.thy index a39155cad7..3edc0bb35d 100644 --- a/proof/refine/RISCV64/IpcCancel_R.thy +++ b/proof/refine/RISCV64/IpcCancel_R.thy @@ -1367,7 +1367,7 @@ interpretation Arch . crunches cancel_ipc for pspace_aligned[wp]: "pspace_aligned :: det_state \ _" and pspace_distinct[wp]: "pspace_distinct :: det_state \ _" - (simp: crunch_simps wp: crunch_wps select_wp) + (simp: crunch_simps wp: crunch_wps) end diff --git a/proof/refine/RISCV64/Ipc_R.thy b/proof/refine/RISCV64/Ipc_R.thy index 16bc96cafc..5147b576c8 100644 --- a/proof/refine/RISCV64/Ipc_R.thy +++ b/proof/refine/RISCV64/Ipc_R.thy @@ -2581,7 +2581,7 @@ lemmas setMessageInfo_typ_ats[wp] = typ_at_lifts [OF setMessageInfo_typ_at'] declare tl_drop_1[simp] crunch cur[wp]: cancel_ipc "cur_tcb" - (wp: select_wp crunch_wps simp: crunch_simps) + (wp: crunch_wps simp: crunch_simps) lemma valid_sched_weak_strg: "valid_sched s \ weak_valid_sched_action s" diff --git a/proof/refine/RISCV64/KHeap_R.thy b/proof/refine/RISCV64/KHeap_R.thy index bb7b5b88ea..194f9a1b90 100644 --- a/proof/refine/RISCV64/KHeap_R.thy +++ b/proof/refine/RISCV64/KHeap_R.thy @@ -2054,21 +2054,21 @@ lemma valid_globals_cte_wpD': lemma dmo_aligned'[wp]: "\pspace_aligned'\ doMachineOp f \\_. pspace_aligned'\" apply (simp add: doMachineOp_def split_def) - apply (wp select_wp) + apply wp apply clarsimp done lemma dmo_distinct'[wp]: "\pspace_distinct'\ doMachineOp f \\_. pspace_distinct'\" apply (simp add: doMachineOp_def split_def) - apply (wp select_wp) + apply wp apply clarsimp done lemma dmo_valid_objs'[wp]: "\valid_objs'\ doMachineOp f \\_. valid_objs'\" apply (simp add: doMachineOp_def split_def) - apply (wp select_wp) + apply wp apply clarsimp done @@ -2076,7 +2076,7 @@ lemma dmo_inv': assumes R: "\P. \P\ f \\_. P\" shows "\P\ doMachineOp f \\_. P\" apply (simp add: doMachineOp_def split_def) - apply (wp select_wp) + apply wp apply clarsimp apply (drule in_inv_by_hoareD [OF R]) apply simp diff --git a/proof/refine/RISCV64/Refine.thy b/proof/refine/RISCV64/Refine.thy index b641b3331e..9f54720fce 100644 --- a/proof/refine/RISCV64/Refine.thy +++ b/proof/refine/RISCV64/Refine.thy @@ -290,18 +290,18 @@ definition lemma do_user_op_valid_list:"\valid_list\ do_user_op f tc \\_. valid_list\" unfolding do_user_op_def - apply (wp select_wp | simp add: split_def)+ + apply (wp | simp add: split_def)+ done lemma do_user_op_valid_sched:"\valid_sched\ do_user_op f tc \\_. valid_sched\" unfolding do_user_op_def - apply (wp select_wp | simp add: split_def)+ + apply (wp | simp add: split_def)+ done lemma do_user_op_sched_act: "\\s. P (scheduler_action s)\ do_user_op f tc \\_ s. P (scheduler_action s)\" unfolding do_user_op_def - apply (wp select_wp | simp add: split_def)+ + apply (wp | simp add: split_def)+ done lemma do_user_op_invs2: @@ -419,7 +419,7 @@ lemma kernelEntry_invs': (\s. 0 < ksDomainTime s) and valid_domain_list' \" apply (simp add: kernelEntry_def) apply (wp ckernel_invs callKernel_domain_time_left - threadSet_invs_trivial threadSet_ct_running' select_wp + threadSet_invs_trivial threadSet_ct_running' TcbAcc_R.dmo_invs' static_imp_wp doMachineOp_ct_in_state' doMachineOp_sch_act_simple callKernel_domain_time_left @@ -498,7 +498,7 @@ lemma doUserOp_invs': (\s. ksSchedulerAction s = ResumeCurrentThread) and ct_running' and (\s. 0 < ksDomainTime s) and valid_domain_list'\" apply (simp add: doUserOp_def split_def ex_abs_def) - apply (wp device_update_invs' doMachineOp_ct_in_state' select_wp + apply (wp device_update_invs' doMachineOp_ct_in_state' | (wp (once) dmo_invs', wpsimp simp: no_irq_modify device_memory_update_def user_memory_update_def))+ apply (clarsimp simp: user_memory_update_def simpler_modify_def @@ -633,7 +633,7 @@ lemma entry_corres: apply (rule hoare_strengthen_post, rule ckernel_invs, simp add: invs'_def cur_tcb'_def) apply (wp thread_set_invs_trivial thread_set_ct_running threadSet_invs_trivial threadSet_ct_running' - select_wp thread_set_not_state_valid_sched static_imp_wp + thread_set_not_state_valid_sched static_imp_wp hoare_vcg_disj_lift ct_in_state_thread_state_lift | simp add: tcb_cap_cases_def ct_in_state'_def thread_set_no_change_tcb_state | (wps, wp threadSet_st_tcb_at2) )+ @@ -801,7 +801,7 @@ lemma domain_list_rel_eq: by (clarsimp simp: state_relation_def) crunch valid_objs': doUserOp, checkActiveIRQ valid_objs' - (wp: crunch_wps select_wp) + (wp: crunch_wps) lemma ckernel_invariant: "ADT_H uop \ full_invs'" diff --git a/proof/refine/RISCV64/Schedule_R.thy b/proof/refine/RISCV64/Schedule_R.thy index d43d083f9e..4bc496808b 100644 --- a/proof/refine/RISCV64/Schedule_R.thy +++ b/proof/refine/RISCV64/Schedule_R.thy @@ -41,7 +41,7 @@ proof - apply (auto simp add: bind_def alternative_def return_def split_def prod_eq_iff) done have Q: "\P\ (do x \ f; return (Some x) od) \ return None \\rv. if rv \ None then \ else P\" - by (wp alternative_wp | simp)+ + by (wp | simp)+ show ?thesis using p apply (induct xs) apply (simp add: y del: dc_simp) diff --git a/proof/refine/RISCV64/Untyped_R.thy b/proof/refine/RISCV64/Untyped_R.thy index d2fb109ffc..0cba959861 100644 --- a/proof/refine/RISCV64/Untyped_R.thy +++ b/proof/refine/RISCV64/Untyped_R.thy @@ -3200,7 +3200,7 @@ lemma createNewCaps_valid_cap': lemma dmo_ctes_of[wp]: "\\s. P (ctes_of s)\ doMachineOp mop \\rv s. P (ctes_of s)\" - by (simp add: doMachineOp_def split_def | wp select_wp)+ + by (simp add: doMachineOp_def split_def | wp)+ lemma createNewCaps_ranges: "\\s. range_cover ptr sz (APIType_capBits ty us) n \ 0 diff --git a/proof/refine/X64/InterruptAcc_R.thy b/proof/refine/X64/InterruptAcc_R.thy index df0c445ba4..47d19ccf96 100644 --- a/proof/refine/X64/InterruptAcc_R.thy +++ b/proof/refine/X64/InterruptAcc_R.thy @@ -112,7 +112,7 @@ lemma preemptionPoint_inv: shows "\P\ preemptionPoint \\_. P\" using assms apply (simp add: preemptionPoint_def setWorkUnits_def getWorkUnits_def modifyWorkUnits_def) apply (wpc - | wp whenE_wp hoare_seq_ext [OF _ select_inv] alternative_wp hoare_drop_imps + | wp whenE_wp hoare_seq_ext [OF _ select_inv] hoare_drop_imps | simp)+ done diff --git a/proof/refine/X64/Ipc_R.thy b/proof/refine/X64/Ipc_R.thy index b8bd0758fb..a2eac7b8cd 100644 --- a/proof/refine/X64/Ipc_R.thy +++ b/proof/refine/X64/Ipc_R.thy @@ -2628,7 +2628,7 @@ lemmas setMessageInfo_typ_ats[wp] = typ_at_lifts [OF setMessageInfo_typ_at'] declare tl_drop_1[simp] crunch cur[wp]: cancel_ipc "cur_tcb" - (wp: select_wp crunch_wps simp: crunch_simps) + (wp: crunch_wps simp: crunch_simps) crunch valid_objs'[wp]: asUser "valid_objs'" diff --git a/proof/refine/X64/KHeap_R.thy b/proof/refine/X64/KHeap_R.thy index 78c97b39bb..199dd740ef 100644 --- a/proof/refine/X64/KHeap_R.thy +++ b/proof/refine/X64/KHeap_R.thy @@ -2114,21 +2114,21 @@ lemma valid_globals_cte_wpD': lemma dmo_aligned'[wp]: "\pspace_aligned'\ doMachineOp f \\_. pspace_aligned'\" apply (simp add: doMachineOp_def split_def) - apply (wp select_wp) + apply wp apply clarsimp done lemma dmo_distinct'[wp]: "\pspace_distinct'\ doMachineOp f \\_. pspace_distinct'\" apply (simp add: doMachineOp_def split_def) - apply (wp select_wp) + apply wp apply clarsimp done lemma dmo_valid_objs'[wp]: "\valid_objs'\ doMachineOp f \\_. valid_objs'\" apply (simp add: doMachineOp_def split_def) - apply (wp select_wp) + apply wp apply clarsimp done @@ -2136,7 +2136,7 @@ lemma dmo_inv': assumes R: "\P. \P\ f \\_. P\" shows "\P\ doMachineOp f \\_. P\" apply (simp add: doMachineOp_def split_def) - apply (wp select_wp) + apply wp apply clarsimp apply (drule in_inv_by_hoareD [OF R]) apply simp diff --git a/proof/refine/X64/Refine.thy b/proof/refine/X64/Refine.thy index 3d7ab23cb8..b80b9b6ea8 100644 --- a/proof/refine/X64/Refine.thy +++ b/proof/refine/X64/Refine.thy @@ -296,18 +296,18 @@ definition lemma do_user_op_valid_list:"\valid_list\ do_user_op f tc \\_. valid_list\" unfolding do_user_op_def - apply (wp select_wp | simp add: split_def)+ + apply (wp | simp add: split_def)+ done lemma do_user_op_valid_sched:"\valid_sched\ do_user_op f tc \\_. valid_sched\" unfolding do_user_op_def - apply (wp select_wp | simp add: split_def)+ + apply (wp | simp add: split_def)+ done lemma do_user_op_sched_act: "\\s. P (scheduler_action s)\ do_user_op f tc \\_ s. P (scheduler_action s)\" unfolding do_user_op_def - apply (wp select_wp | simp add: split_def)+ + apply (wp | simp add: split_def)+ done lemma do_user_op_invs2: @@ -419,7 +419,7 @@ lemma kernelEntry_invs': (\s. 0 < ksDomainTime s) and valid_domain_list' \" apply (simp add: kernelEntry_def) apply (wp ckernel_invs callKernel_domain_time_left - threadSet_invs_trivial threadSet_ct_running' select_wp + threadSet_invs_trivial threadSet_ct_running' TcbAcc_R.dmo_invs' static_imp_wp doMachineOp_sch_act_simple callKernel_domain_time_left @@ -498,7 +498,7 @@ lemma doUserOp_invs': (\s. ksSchedulerAction s = ResumeCurrentThread) and ct_running' and (\s. 0 < ksDomainTime s) and valid_domain_list'\" apply (simp add: doUserOp_def split_def ex_abs_def) - apply (wp device_update_invs' select_wp + apply (wp device_update_invs' | (wp (once) dmo_invs', wpsimp simp: no_irq_modify device_memory_update_def user_memory_update_def))+ apply (clarsimp simp: user_memory_update_def simpler_modify_def @@ -632,7 +632,7 @@ lemma entry_corres: apply (rule hoare_strengthen_post, rule ckernel_invs, simp add: invs'_def cur_tcb'_def) apply (wp thread_set_invs_trivial thread_set_ct_running threadSet_invs_trivial threadSet_ct_running' - select_wp thread_set_not_state_valid_sched static_imp_wp + thread_set_not_state_valid_sched static_imp_wp hoare_vcg_disj_lift ct_in_state_thread_state_lift | simp add: tcb_cap_cases_def ct_in_state'_def thread_set_no_change_tcb_state | (wps, wp threadSet_st_tcb_at2) )+ @@ -800,7 +800,7 @@ lemma domain_list_rel_eq: by (clarsimp simp: state_relation_def) crunch valid_objs': doUserOp, checkActiveIRQ valid_objs' - (wp: crunch_wps select_wp) + (wp: crunch_wps) lemma ckernel_invariant: "ADT_H uop \ full_invs'" diff --git a/proof/refine/X64/Schedule_R.thy b/proof/refine/X64/Schedule_R.thy index 316d11cf87..a248f01710 100644 --- a/proof/refine/X64/Schedule_R.thy +++ b/proof/refine/X64/Schedule_R.thy @@ -41,7 +41,7 @@ proof - apply (auto simp add: bind_def alternative_def return_def split_def prod_eq_iff) done have Q: "\P\ (do x \ f; return (Some x) od) \ return None \\rv. if rv \ None then \ else P\" - by (wp alternative_wp | simp)+ + by (wp | simp)+ show ?thesis using p apply (induct xs) apply (simp add: y del: dc_simp) diff --git a/proof/refine/X64/Untyped_R.thy b/proof/refine/X64/Untyped_R.thy index d1230a5aee..01734b8b21 100644 --- a/proof/refine/X64/Untyped_R.thy +++ b/proof/refine/X64/Untyped_R.thy @@ -3292,7 +3292,7 @@ lemma createNewCaps_valid_cap': lemma dmo_ctes_of[wp]: "\\s. P (ctes_of s)\ doMachineOp mop \\rv s. P (ctes_of s)\" - by (simp add: doMachineOp_def split_def | wp select_wp)+ + by (simp add: doMachineOp_def split_def | wp)+ lemma createNewCaps_ranges: "\\s. range_cover ptr sz (APIType_capBits ty us) n \ 0 diff --git a/proof/sep-capDL/Frame_SD.thy b/proof/sep-capDL/Frame_SD.thy index 861d47b6ab..30ab6b796f 100644 --- a/proof/sep-capDL/Frame_SD.thy +++ b/proof/sep-capDL/Frame_SD.thy @@ -316,7 +316,7 @@ lemma set_cap_wp: apply (case_tac ptr, rename_tac obj_id slot, clarsimp) apply (wp|wpc)+ apply (rule_tac obj = obj in set_object_slot_wp) - apply (wp select_wp |wpc)+ + apply (wp |wpc)+ apply clarsimp apply (clarsimp simp: update_slots_def has_slots_def split: cdl_object.splits) diff --git a/proof/sep-capDL/Helpers_SD.thy b/proof/sep-capDL/Helpers_SD.thy index 79d3127f2b..8d2a1a4634 100644 --- a/proof/sep-capDL/Helpers_SD.thy +++ b/proof/sep-capDL/Helpers_SD.thy @@ -1034,7 +1034,7 @@ lemma derive_cap_wp: "\ P (derived_cap cap) \ derive_cap slot cap \P\, -" apply (clarsimp simp: derive_cap_def derived_cap_def) apply (clarsimp simp: validE_R_def derive_cap_def split:cdl_cap.splits) - apply (safe, (wp alternative_wp alternativeE_wp whenE_wp | + apply (safe, (wp whenE_wp | clarsimp simp: ensure_no_children_def)+ ) done diff --git a/tools/autocorres/L1Defs.thy b/tools/autocorres/L1Defs.thy index 76c24ebf5f..346223fa4f 100644 --- a/tools/autocorres/L1Defs.thy +++ b/tools/autocorres/L1Defs.thy @@ -320,7 +320,7 @@ lemma L1corres_prepend_unknown_var': apply (monad_eq simp: Bex_def) apply metis apply (subst L1_init_def) - apply (wp del: hoare_vcg_prop) + apply (wpsimp wp_del: hoare_vcg_prop) done lemma L1_catch_seq_join: "no_throw \ A \ L1_seq A (L1_catch B C) = (L1_catch (L1_seq A B) C)" @@ -334,7 +334,7 @@ lemma no_throw_L1_init [simp]: "no_throw P (L1_init f)" apply (rule no_throw_bindE [where B=\]) apply simp apply simp - apply wp + apply wpsimp done lemma L1corres_prepend_unknown_var: diff --git a/tools/autocorres/L1Valid.thy b/tools/autocorres/L1Valid.thy index fdd0b33451..1ac15209a6 100644 --- a/tools/autocorres/L1Valid.thy +++ b/tools/autocorres/L1Valid.thy @@ -29,7 +29,7 @@ lemma L1_spec_wp [wp]: "\ \s. \t. (s, t) \ f \ \s. \x. P () (f (\_. x) s) \ L1_init f \ P \, \ Q \" apply (unfold L1_init_def) - apply (wp select_wp) + apply wp apply fastforce done diff --git a/tools/autocorres/L2Opt.thy b/tools/autocorres/L2Opt.thy index 93f2d01f24..eb4ea9cc52 100644 --- a/tools/autocorres/L2Opt.thy +++ b/tools/autocorres/L2Opt.thy @@ -152,7 +152,7 @@ lemma monad_equiv_guard_conj [L2flow]: lemma monad_equiv_unknown [L2flow]: "monad_equiv P (L2_unknown name) (L2_unknown name) (\r s. P s) (\_ _. False)" apply (clarsimp simp: monad_equiv_def L2_defs) - apply (wp select_wp) + apply wp apply force done