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