From e89813ecf2b32f3c27fd0efaf09a8c45bf8abf1c Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Mon, 30 Jan 2023 17:31:34 +1100 Subject: [PATCH] proofs: updates for monad refactor Signed-off-by: Gerwin Klein --- lib/Hoare_Sep_Tactics/Hoare_Sep_Tactics.thy | 16 +++--- proof/access-control/ARM/ArchArch_AC.thy | 5 +- proof/capDL-api/IRQ_DP.thy | 2 +- proof/capDL-api/Invocation_DP.thy | 17 ++----- proof/capDL-api/KHeap_DP.thy | 20 +++----- proof/capDL-api/Retype_DP.thy | 23 ++++----- proof/capDL-api/TCB_DP.thy | 3 +- proof/crefine/ARM/ArchMove_C.thy | 44 +++++----------- proof/crefine/ARM/CLevityCatch.thy | 2 +- proof/crefine/ARM/Fastpath_Equiv.thy | 2 +- proof/crefine/ARM/IpcCancel_C.thy | 3 ++ proof/crefine/ARM/Ipc_C.thy | 4 ++ proof/crefine/ARM/IsolatedThreadAction.thy | 5 +- proof/crefine/ARM/Machine_C.thy | 13 ++--- proof/crefine/ARM/Retype_C.thy | 13 +++-- proof/crefine/ARM/SyscallArgs_C.thy | 4 +- proof/crefine/ARM/Tcb_C.thy | 12 ++--- proof/crefine/ARM/VSpace_C.thy | 4 +- proof/crefine/ARM_HYP/ArchMove_C.thy | 46 +++++------------ proof/crefine/ARM_HYP/CLevityCatch.thy | 6 +-- proof/crefine/ARM_HYP/Fastpath_Equiv.thy | 2 +- proof/crefine/ARM_HYP/Finalise_C.thy | 2 +- proof/crefine/ARM_HYP/IpcCancel_C.thy | 3 ++ proof/crefine/ARM_HYP/Ipc_C.thy | 5 +- .../crefine/ARM_HYP/IsolatedThreadAction.thy | 2 +- proof/crefine/ARM_HYP/Machine_C.thy | 15 +++--- proof/crefine/ARM_HYP/Retype_C.thy | 13 +++-- proof/crefine/ARM_HYP/SyscallArgs_C.thy | 4 +- proof/crefine/ARM_HYP/Tcb_C.thy | 11 ++-- proof/crefine/ARM_HYP/VSpace_C.thy | 6 ++- proof/crefine/Move_C.thy | 15 +++--- proof/crefine/RISCV64/ArchMove_C.thy | 30 ++++------- proof/crefine/RISCV64/CLevityCatch.thy | 6 +-- proof/crefine/RISCV64/Finalise_C.thy | 2 +- proof/crefine/RISCV64/IpcCancel_C.thy | 7 ++- proof/crefine/RISCV64/Ipc_C.thy | 11 ++-- .../crefine/RISCV64/IsolatedThreadAction.thy | 4 +- proof/crefine/RISCV64/Retype_C.thy | 13 +++-- proof/crefine/RISCV64/SyscallArgs_C.thy | 4 +- proof/crefine/RISCV64/Tcb_C.thy | 11 ++-- proof/crefine/X64/ArchMove_C.thy | 51 +++++-------------- proof/crefine/X64/CLevityCatch.thy | 4 +- proof/crefine/X64/Finalise_C.thy | 2 +- proof/crefine/X64/IpcCancel_C.thy | 9 ++-- proof/crefine/X64/Ipc_C.thy | 6 ++- proof/crefine/X64/IsolatedThreadAction.thy | 4 +- proof/crefine/X64/Retype_C.thy | 13 +++-- proof/crefine/X64/SyscallArgs_C.thy | 4 +- proof/crefine/X64/Tcb_C.thy | 11 ++-- proof/drefine/Arch_DR.thy | 9 ++-- proof/drefine/CNode_DR.thy | 9 ++-- proof/drefine/Intent_DR.thy | 2 +- proof/drefine/Ipc_DR.thy | 3 +- proof/drefine/KHeap_DR.thy | 7 +-- proof/drefine/Untyped_DR.thy | 9 +++- proof/infoflow/ARM/ArchArch_IF.thy | 12 +++-- proof/infoflow/ARM/ArchIRQMasks_IF.thy | 5 +- proof/infoflow/CNode_IF.thy | 2 +- proof/infoflow/Finalise_IF.thy | 2 +- proof/infoflow/Noninterference.thy | 3 +- proof/infoflow/RISCV64/ArchIRQMasks_IF.thy | 2 +- proof/infoflow/Syscall_IF.thy | 7 +-- proof/infoflow/Tcb_IF.thy | 3 +- .../AARCH64/ArchDetype_AI.thy | 2 +- .../AARCH64/ArchEmptyFail_AI.thy | 19 ++++--- .../invariant-abstract/AARCH64/ArchTcb_AI.thy | 3 +- .../AARCH64/ArchVSpace_AI.thy | 2 +- .../invariant-abstract/AARCH64/Machine_AI.thy | 2 +- .../invariant-abstract/ARM/ArchDetype_AI.thy | 2 +- .../ARM/ArchEmptyFail_AI.thy | 16 +++--- proof/invariant-abstract/ARM/ArchTcb_AI.thy | 6 +-- .../ARM/ArchVSpaceEntries_AI.thy | 2 - proof/invariant-abstract/ARM/Machine_AI.thy | 23 +++++---- .../ARM_HYP/ArchArch_AI.thy | 2 +- .../ARM_HYP/ArchDetype_AI.thy | 2 +- .../ARM_HYP/ArchEmptyFail_AI.thy | 17 ++++--- .../ARM_HYP/ArchSchedule_AI.thy | 16 ------ .../invariant-abstract/ARM_HYP/ArchTcb_AI.thy | 6 +-- .../ARM_HYP/ArchVSpaceEntries_AI.thy | 2 - .../ARM_HYP/ArchVSpace_AI.thy | 4 +- .../invariant-abstract/ARM_HYP/Machine_AI.thy | 27 +++++----- proof/invariant-abstract/CNodeInv_AI.thy | 3 +- proof/invariant-abstract/EmptyFail_AI.thy | 2 +- proof/invariant-abstract/Include_AI.thy | 15 +++--- .../RISCV64/ArchDetype_AI.thy | 2 +- .../RISCV64/ArchEmptyFail_AI.thy | 19 ++++--- .../invariant-abstract/RISCV64/ArchTcb_AI.thy | 3 +- .../RISCV64/ArchVSpaceEntries_AI.thy | 2 - .../invariant-abstract/RISCV64/Machine_AI.thy | 8 +-- proof/invariant-abstract/SubMonad_AI.thy | 2 +- proof/invariant-abstract/VSpaceEntries_AI.thy | 1 - .../invariant-abstract/X64/ArchDetype_AI.thy | 2 +- .../X64/ArchEmptyFail_AI.thy | 21 ++++---- proof/invariant-abstract/X64/ArchTcb_AI.thy | 4 +- .../X64/ArchVSpaceEntries_AI.thy | 2 - proof/invariant-abstract/X64/Machine_AI.thy | 16 +++--- proof/refine/ARM/Arch_R.thy | 3 +- proof/refine/ARM/CSpace_R.thy | 3 +- proof/refine/ARM/Detype_R.thy | 2 +- proof/refine/ARM/EmptyFail.thy | 31 ++++++----- proof/refine/ARM/EmptyFail_H.thy | 23 +++------ proof/refine/ARM/Finalise_R.thy | 7 +-- proof/refine/ARM/Interrupt_R.thy | 1 + proof/refine/ARM/IpcCancel_R.thy | 10 ++-- proof/refine/ARM/PageTableDuplicates.thy | 1 - proof/refine/ARM/Schedule_R.thy | 2 +- proof/refine/ARM/TcbAcc_R.thy | 1 - proof/refine/ARM/Tcb_R.thy | 1 + proof/refine/ARM/Untyped_R.thy | 3 +- proof/refine/ARM_HYP/ArchAcc_R.thy | 6 ++- proof/refine/ARM_HYP/Arch_R.thy | 3 +- proof/refine/ARM_HYP/CSpace_R.thy | 3 +- proof/refine/ARM_HYP/Detype_R.thy | 2 +- proof/refine/ARM_HYP/EmptyFail.thy | 31 ++++++----- proof/refine/ARM_HYP/EmptyFail_H.thy | 25 ++++----- proof/refine/ARM_HYP/Finalise_R.thy | 7 +-- proof/refine/ARM_HYP/Interrupt_R.thy | 17 +++---- proof/refine/ARM_HYP/IpcCancel_R.thy | 7 +-- proof/refine/ARM_HYP/PageTableDuplicates.thy | 1 - proof/refine/ARM_HYP/Schedule_R.thy | 2 +- proof/refine/ARM_HYP/Syscall_R.thy | 1 - proof/refine/ARM_HYP/TcbAcc_R.thy | 1 - proof/refine/ARM_HYP/Tcb_R.thy | 1 + proof/refine/ARM_HYP/Untyped_R.thy | 3 +- proof/refine/ARM_HYP/VSpace_R.thy | 6 +-- proof/refine/RISCV64/CSpace_R.thy | 3 +- proof/refine/RISCV64/Detype_R.thy | 2 +- proof/refine/RISCV64/EmptyFail.thy | 31 ++++++----- proof/refine/RISCV64/EmptyFail_H.thy | 17 ++----- proof/refine/RISCV64/IpcCancel_R.thy | 10 ++-- proof/refine/RISCV64/Schedule_R.thy | 2 +- proof/refine/RISCV64/Syscall_R.thy | 1 - proof/refine/RISCV64/TcbAcc_R.thy | 1 - proof/refine/RISCV64/Tcb_R.thy | 1 + proof/refine/X64/CSpace_R.thy | 3 +- proof/refine/X64/Detype_R.thy | 2 +- proof/refine/X64/EmptyFail.thy | 31 ++++++----- proof/refine/X64/EmptyFail_H.thy | 27 ++++------ proof/refine/X64/Finalise_R.thy | 7 +-- proof/refine/X64/IpcCancel_R.thy | 10 ++-- proof/refine/X64/Schedule_R.thy | 2 +- proof/refine/X64/Syscall_R.thy | 1 - proof/refine/X64/TcbAcc_R.thy | 1 - proof/refine/X64/Tcb_R.thy | 1 + proof/refine/X64/Untyped_R.thy | 3 +- spec/capDL/Monads_D.thy | 3 +- spec/design/m-skel/AARCH64/MachineTypes.thy | 8 +-- spec/design/m-skel/ARM/MachineTypes.thy | 6 ++- spec/design/m-skel/ARM_HYP/MachineTypes.thy | 6 ++- spec/design/m-skel/RISCV64/MachineTypes.thy | 8 +-- spec/design/m-skel/X64/MachineTypes.thy | 8 +-- sys-init/CreateObjects_SI.thy | 5 +- tools/autocorres/CorresXF.thy | 4 +- tools/autocorres/ExceptionRewrite.thy | 19 ++----- .../tests/proof-tests/word_abs_options.thy | 8 +-- 155 files changed, 597 insertions(+), 682 deletions(-) diff --git a/lib/Hoare_Sep_Tactics/Hoare_Sep_Tactics.thy b/lib/Hoare_Sep_Tactics/Hoare_Sep_Tactics.thy index 63cba92be..34cb78aec 100644 --- a/lib/Hoare_Sep_Tactics/Hoare_Sep_Tactics.thy +++ b/lib/Hoare_Sep_Tactics/Hoare_Sep_Tactics.thy @@ -81,14 +81,14 @@ schematic_goal strong_sep_impl_sep_wp': "\sep_lift. (\R. \(\s. (P \* R) (sep_lift s) )\ f \\rv. (\s. (Q rv \* R) (sep_lift s))\) \ \(\s. ( P \* (?f Q R)) (sep_lift s))\ f \\rv s . R rv (sep_lift s)\" - apply (atomize) - apply (erule_tac x="(\s. \x. (Q x \* R x) s)" in allE) - apply (rule hoare_strengthen_post) - apply (assumption) - apply (sep_drule (direct) extract_all) - apply (erule_tac x=r in allE) - apply (sep_solve) -done + apply (atomize) + apply (erule_tac x="(\s. \x. (Q x \* R x) s)" in allE) + apply (erule hoare_strengthen_post) + apply (rename_tac rv s) + apply (sep_drule (direct) extract_all) + apply (erule_tac x=rv in allE) + apply (sep_solve) + done lemma strong_sep_impl_sep_wp'': "\sep_lift. diff --git a/proof/access-control/ARM/ArchArch_AC.thy b/proof/access-control/ARM/ArchArch_AC.thy index 06a62a5fe..f1c2b9c0d 100644 --- a/proof/access-control/ARM/ArchArch_AC.thy +++ b/proof/access-control/ARM/ArchArch_AC.thy @@ -959,8 +959,9 @@ lemma delete_asid_pool_pas_refined [wp]: crunch respects[wp]: invalidate_asid_entry "integrity aag X st" crunch respects[wp]: flush_space "integrity aag X st" - (ignore: do_machine_op simp: invalidateLocalTLB_ASID_def cleanCaches_PoU_def - dsb_def clean_D_PoU_def invalidate_I_PoU_def do_machine_op_bind) + (ignore: do_machine_op + simp: invalidateLocalTLB_ASID_def cleanCaches_PoU_def dsb_def clean_D_PoU_def invalidate_I_PoU_def + do_machine_op_bind empty_fail_cond) lemma delete_asid_pool_respects[wp]: "\integrity aag X st and diff --git a/proof/capDL-api/IRQ_DP.thy b/proof/capDL-api/IRQ_DP.thy index 2a4caa2bb..0d0b6659e 100644 --- a/proof/capDL-api/IRQ_DP.thy +++ b/proof/capDL-api/IRQ_DP.thy @@ -123,7 +123,7 @@ lemma decode_irq_control_issue_irq_rv: done schematic_goal lookup_extra_caps_once_wp: "\?P\ lookup_extra_caps root_tcb_id [endpoint_cptr] \Q\, \Q'\" -apply (clarsimp simp: lookup_extra_caps_def mapME_def sequenceE_def, wp, clarsimp) +apply (clarsimp simp: lookup_extra_caps_def mapME_def sequenceE_def, wp) apply (rule lookup_cap_and_slot_rvu) done diff --git a/proof/capDL-api/Invocation_DP.thy b/proof/capDL-api/Invocation_DP.thy index 448d41639..9b16571f1 100644 --- a/proof/capDL-api/Invocation_DP.thy +++ b/proof/capDL-api/Invocation_DP.thy @@ -622,13 +622,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 (rule alternative_wp) - apply (rule hoare_pre) - apply (rule insert_cap_sibling_wp) - apply simp - apply (rule hoare_pre) - apply (rule insert_cap_child_wp) - apply simp + apply (wpsimp wp: alternative_wp insert_cap_sibling_wp insert_cap_child_wp) done lemma invoke_cnode_move_wp: @@ -1136,13 +1130,8 @@ 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 (rule alternative_wp) - apply (rule hoare_pre) - apply (rule insert_cap_sibling_wp) - apply (simp add:cap_of_insert_call_def) - apply (rule hoare_pre) - apply (rule insert_cap_child_wp) - apply (simp add:cap_of_insert_call_def) + apply (wpsimp wp: alternative_wp insert_cap_sibling_wp insert_cap_child_wp + simp: cap_of_insert_call_def) done lemma object_to_sep_state_slot: diff --git a/proof/capDL-api/KHeap_DP.thy b/proof/capDL-api/KHeap_DP.thy index 28883e7d3..0e31d1601 100644 --- a/proof/capDL-api/KHeap_DP.thy +++ b/proof/capDL-api/KHeap_DP.thy @@ -862,14 +862,9 @@ lemma lookup_cap_rvu : done lemma lookup_cap_wp: - "\P\ - lookup_cap thread cap_ptr - \\_. P\, \\_ .P \ " - apply (clarsimp simp: lookup_cap_def) - apply (wp lookup_slot_wp get_cap_wp) - apply (clarsimp) - apply (wp lookup_slot_wp) - apply assumption + "\P\ lookup_cap thread cap_ptr \\_. P\, \\_ .P \ " + apply (clarsimp simp: lookup_cap_def) + apply (wp lookup_slot_wp get_cap_wp) done @@ -1119,9 +1114,9 @@ lemma get_thread_sep_wp: done lemma get_thread_inv: -"\ Q \ - get_thread thread \\t s. Q s\" - by (simp add:get_thread_def | wp | wpc)+ + "\ Q \ get_thread thread \\t s. Q s\" + unfolding get_thread_def + by wpsimp lemma get_thread_sep_wp_precise: "\\s. tcb_at' (\tcb. Q tcb s) thread s \ @@ -1145,8 +1140,7 @@ lemma has_restart_cap_sep_wp: \\rv. Q rv\" apply (rule hoare_name_pre_state) apply (clarsimp simp: object_at_def) - apply (simp add: object_at_def get_thread_def has_restart_cap_def - | wp+ | wpc | intro conjI)+ + apply (wpsimp simp: object_at_def get_thread_def has_restart_cap_def | intro conjI)+ apply (clarsimp dest!: opt_cap_sep_imp simp: opt_cap_def slots_of_def) apply (clarsimp simp: object_slots_def) diff --git a/proof/capDL-api/Retype_DP.thy b/proof/capDL-api/Retype_DP.thy index 8f1956b5a..09363f4db 100644 --- a/proof/capDL-api/Retype_DP.thy +++ b/proof/capDL-api/Retype_DP.thy @@ -432,8 +432,7 @@ lemma set_parent_has_children[wp]: lemma create_cap_has_children[wp]: "\\\ create_cap new_type sz uref slot dev \\r. has_children uref\" apply (clarsimp simp :create_cap_def split_def) - apply wp - apply simp + apply wpsimp done abbreviation (input) "retype_with_kids uinv @@ -533,12 +532,10 @@ lemma invoke_untyped_one_wp: lemma mark_tcb_intent_error_has_children[wp]: "\\s. P (has_children ptr s)\ - mark_tcb_intent_error cur_thread b - \\rv s. P (has_children ptr s)\" - apply (simp add:has_children_def is_cdt_parent_def - mark_tcb_intent_error_def update_thread_def - set_object_def | wp | wpc)+ - done + mark_tcb_intent_error cur_thread b + \\rv s. P (has_children ptr s)\" + 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) @@ -871,12 +868,10 @@ lemma update_thread_no_pending: K(\x. (case cdl_tcb_caps x tcb_pending_op_slot of Some cap \ \ is_pending_cap cap | _ \ True)\ (case cdl_tcb_caps (t x) tcb_pending_op_slot of Some cap \ \ is_pending_cap cap | _ \ True))\ update_thread thread_ptr t \\rv. no_pending\" - apply (simp add: update_thread_def set_object_def | (wp modify_wp)+ | wpc)+ - apply (clarsimp simp: no_pending_def) - apply (drule_tac x = oid in spec) - apply (clarsimp simp: opt_cap_def slots_of_def - object_slots_def - split: if_splits option.splits) + unfolding update_thread_def set_object_def + apply wpsimp + apply (fastforce simp: opt_cap_def slots_of_def object_slots_def no_pending_def + split: if_splits option.splits) done lemma update_thread_tcb_at: diff --git a/proof/capDL-api/TCB_DP.thy b/proof/capDL-api/TCB_DP.thy index bf198b47f..d8f5d3946 100644 --- a/proof/capDL-api/TCB_DP.thy +++ b/proof/capDL-api/TCB_DP.thy @@ -1222,8 +1222,9 @@ lemma seL4_TCB_WriteRegisters_wp: apply (wp do_kernel_op_pull_back) apply (rule hoare_post_imp[OF _ call_kernel_with_intent_allow_error_helper [where check = False,simplified]]) + apply (rename_tac rv s) apply clarsimp - apply (case_tac r,(clarsimp,assumption)+)[1] + apply (case_tac rv, (clarsimp,assumption)+)[1] apply fastforce apply (rule hoare_strengthen_post[OF set_cap_wp]) apply (sep_select 3,sep_cancel) diff --git a/proof/crefine/ARM/ArchMove_C.thy b/proof/crefine/ARM/ArchMove_C.thy index dccb362a3..dc3ee0892 100644 --- a/proof/crefine/ARM/ArchMove_C.thy +++ b/proof/crefine/ARM/ArchMove_C.thy @@ -82,21 +82,13 @@ lemma setCTE_asidpool': lemma empty_fail_findPDForASID[iff]: "empty_fail (findPDForASID asid)" - apply (simp add: findPDForASID_def liftME_def) - apply (intro empty_fail_bindE, simp_all split: option.split) - apply (simp add: assertE_def split: if_split) - apply (simp add: assertE_def split: if_split) - apply (simp add: empty_fail_getObject) - apply (simp add: assertE_def liftE_bindE checkPDAt_def split: if_split) - done + unfolding findPDForASID_def checkPDAt_def + by (wpsimp wp: empty_fail_getObject) lemma empty_fail_findPDForASIDAssert[iff]: "empty_fail (findPDForASIDAssert asid)" - apply (simp add: findPDForASIDAssert_def catch_def - checkPDAt_def checkPDUniqueToASID_def - checkPDASIDMapMembership_def) - apply (intro empty_fail_bind, simp_all split: sum.split) - done + unfolding findPDForASIDAssert_def checkPDAt_def checkPDUniqueToASID_def checkPDASIDMapMembership_def + by (wpsimp wp: empty_fail_getObject) crunches Arch.switchToThread for valid_queues'[wp]: valid_queues' @@ -209,7 +201,7 @@ lemma cap_case_isPageDirectoryCap: lemma empty_fail_loadWordUser[intro!, simp]: "empty_fail (loadWordUser x)" - by (simp add: loadWordUser_def ef_loadWord ef_dmo') + by (fastforce simp: loadWordUser_def ef_loadWord ef_dmo') lemma empty_fail_getMRs[iff]: "empty_fail (getMRs t buf mi)" @@ -219,26 +211,14 @@ lemma empty_fail_getReceiveSlots: "empty_fail (getReceiveSlots r rbuf)" proof - note - empty_fail_assertE[iff] - empty_fail_resolveAddressBits[iff] + empty_fail_resolveAddressBits[wp] + empty_fail_rethrowFailure[wp] + empty_fail_rethrowFailure[wp] show ?thesis - apply (clarsimp simp: getReceiveSlots_def loadCapTransfer_def split_def - split: option.split) - apply (rule empty_fail_bind) - apply (simp add: capTransferFromWords_def) - apply (simp add: emptyOnFailure_def unifyFailure_def) - apply (intro empty_fail_catch empty_fail_bindE empty_fail_rethrowFailure, - simp_all add: empty_fail_whenEs) - apply (simp_all add: lookupCap_def split_def lookupCapAndSlot_def - lookupSlotForThread_def liftME_def - getThreadCSpaceRoot_def locateSlot_conv bindE_assoc - lookupSlotForCNodeOp_def lookupErrorOnFailure_def - cong: if_cong) - apply (intro empty_fail_bindE, - simp_all add: getSlotCap_def) - apply (intro empty_fail_If empty_fail_bindE empty_fail_rethrowFailure impI, - simp_all add: empty_fail_whenEs rangeCheck_def) - done + unfolding getReceiveSlots_def loadCapTransfer_def lookupCap_def lookupCapAndSlot_def + by (wpsimp simp: emptyOnFailure_def unifyFailure_def lookupSlotForThread_def + capTransferFromWords_def getThreadCSpaceRoot_def locateSlot_conv bindE_assoc + lookupSlotForCNodeOp_def lookupErrorOnFailure_def rangeCheck_def) qed lemma user_getreg_rv: diff --git a/proof/crefine/ARM/CLevityCatch.thy b/proof/crefine/ARM/CLevityCatch.thy index 91d258017..235b14e48 100644 --- a/proof/crefine/ARM/CLevityCatch.thy +++ b/proof/crefine/ARM/CLevityCatch.thy @@ -66,7 +66,7 @@ lemma asUser_get_registers: apply (simp add: mapM_empty asUser_return) apply wp apply simp - apply (simp add: mapM_Cons asUser_bind_distrib asUser_return) + apply (simp add: mapM_Cons asUser_bind_distrib asUser_return empty_fail_cond) apply wp apply simp apply (rule hoare_strengthen_post) diff --git a/proof/crefine/ARM/Fastpath_Equiv.thy b/proof/crefine/ARM/Fastpath_Equiv.thy index 5fd357a80..9de7239e4 100644 --- a/proof/crefine/ARM/Fastpath_Equiv.thy +++ b/proof/crefine/ARM/Fastpath_Equiv.thy @@ -864,7 +864,7 @@ lemma receiveIPC_simple_rewrite: lemma empty_fail_isFinalCapability: "empty_fail (isFinalCapability cte)" - by (simp add: isFinalCapability_def Let_def split: if_split) + by (simp add: isFinalCapability_def Let_def empty_fail_cond split: if_split) lemma cteDeleteOne_replycap_rewrite: "monadic_rewrite True False diff --git a/proof/crefine/ARM/IpcCancel_C.thy b/proof/crefine/ARM/IpcCancel_C.thy index aed779b54..2f7523ee0 100644 --- a/proof/crefine/ARM/IpcCancel_C.thy +++ b/proof/crefine/ARM/IpcCancel_C.thy @@ -2216,6 +2216,7 @@ lemma scheduleTCB_ccorres': rescheduleRequired od) (Call scheduleTCB_'proc)" + supply empty_fail_cond[simp] apply (cinit' lift: tptr_') apply (rule ccorres_rhs_assoc2)+ apply (rule_tac xf'="ret__int_'" in ccorres_split_nothrow_novcg) @@ -2270,6 +2271,7 @@ lemma scheduleTCB_ccorres_valid_queues'_pre: when (\ runnable \ curThread = thread \ action = ResumeCurrentThread) rescheduleRequired od) (Call scheduleTCB_'proc)" + supply empty_fail_cond[simp] apply (cinit' lift: tptr_' simp del: word_neq_0_conv) apply (rule ccorres_rhs_assoc2)+ apply (rule_tac xf'="ret__int_'" in ccorres_split_nothrow_novcg) @@ -2362,6 +2364,7 @@ lemma scheduleTCB_ccorres_valid_queues'_pre_simple: when (\ runnable \ curThread = thread \ action = ResumeCurrentThread) rescheduleRequired od) (Call scheduleTCB_'proc)" + supply empty_fail_cond[simp] apply (cinit' lift: tptr_' simp del: word_neq_0_conv) apply (rule ccorres_rhs_assoc2)+ apply (rule_tac xf'="ret__int_'" in ccorres_split_nothrow_novcg) diff --git a/proof/crefine/ARM/Ipc_C.thy b/proof/crefine/ARM/Ipc_C.thy index 92f03c306..f7bbcde84 100644 --- a/proof/crefine/ARM/Ipc_C.thy +++ b/proof/crefine/ARM/Ipc_C.thy @@ -377,6 +377,7 @@ lemma handleArchFaultReply': msg \ getMRs s sb tag; handleArchFaultReply f r (msgLabel tag) msg od) x' = handleArchFaultReply' f s r tag x'" + supply empty_fail_cond[simp] apply (unfold handleArchFaultReply'_def getMRs_def msgMaxLength_def bit_def msgLengthBits_def msgRegisters_unfold fromIntegral_simp1 fromIntegral_simp2 @@ -461,6 +462,7 @@ lemma handleFaultReply': msg \ getMRs s sb tag; handleFaultReply f r (msgLabel tag) msg od) (handleFaultReply' f s r)" + supply empty_fail_cond[simp] apply (unfold handleFaultReply'_def getMRs_def msgMaxLength_def bit_def msgLengthBits_def msgRegisters_unfold fromIntegral_simp1 fromIntegral_simp2 @@ -1607,6 +1609,7 @@ proof - let ?obj_at_ft = "obj_at' (\tcb. tcbFault tcb = Some ft) sender" note symb_exec_r_fault = ccorres_symb_exec_r_known_rv_UNIV [where xf'=ret__unsigned_' and R="?obj_at_ft" and R'=UNIV] + note empty_fail_cond[simp] show ?thesis apply (unfold K_def) apply (intro ccorres_gen_asm) @@ -2919,6 +2922,7 @@ proof - let ?curr = "\s. current_extra_caps_' (globals s)" let ?EXCNONE = "{s. ret__unsigned_long_' s = scast EXCEPTION_NONE}" let ?interpret = "\v n. take n (array_to_list (excaprefs_C v))" + note empty_fail_cond[simp] show ?thesis apply (rule ccorres_gen_asm)+ apply (cinit(no_subst_asm) lift: thread_' bufferPtr_' info_' simp: whileAnno_def) diff --git a/proof/crefine/ARM/IsolatedThreadAction.thy b/proof/crefine/ARM/IsolatedThreadAction.thy index aecaf976a..1ee5ead20 100644 --- a/proof/crefine/ARM/IsolatedThreadAction.thy +++ b/proof/crefine/ARM/IsolatedThreadAction.thy @@ -345,6 +345,9 @@ lemma getObject_get_assert: apply (simp add: lookupAround2_known1 assert_opt_def obj_at'_def projectKO_def2 split: option.split) + apply (rule conjI) + apply (clarsimp simp: fail_def fst_return conj_comms project_inject + objBits_def bind_def simpler_gets_def) apply (clarsimp simp: fail_def fst_return conj_comms project_inject objBits_def) apply (simp only: assert2[symmetric], @@ -757,7 +760,7 @@ lemma doIPCTransfer_simple_rewrite: (* FIXME move *) lemma empty_fail_isRunnable[intro!, wp, simp]: "empty_fail (isRunnable t)" - by (simp add: isRunnable_def isStopped_def) + by (simp add: isRunnable_def isStopped_def empty_fail_cond) lemma setupCallerCap_rewrite: "monadic_rewrite True True (\s. reply_masters_rvk_fb (ctes_of s)) diff --git a/proof/crefine/ARM/Machine_C.thy b/proof/crefine/ARM/Machine_C.thy index 10bd73d19..c6ea7f984 100644 --- a/proof/crefine/ARM/Machine_C.thy +++ b/proof/crefine/ARM/Machine_C.thy @@ -442,7 +442,7 @@ lemma cleanInvalidateCacheRange_RAM_ccorres: apply (rule ccorres_basic_srnoop) apply (simp add: cleanInvalidateCacheRange_RAM_def doMachineOp_bind empty_fail_dsb empty_fail_cleanInvalidateL2Range - empty_fail_cleanInvalByVA) + empty_fail_cleanInvalByVA empty_fail_cond) apply (ctac (no_vcg) add: cleanCacheRange_PoC_ccorres) apply (ctac (no_vcg) add: dsb_ccorres) apply (ctac (no_vcg) add: cleanInvalidateL2Range_ccorres) @@ -474,7 +474,8 @@ lemma cleanCacheRange_RAM_ccorres: (doMachineOp (cleanCacheRange_RAM w1 w2 w3)) (Call cleanCacheRange_RAM_'proc)" apply (cinit' lift: start_' end_' pstart_') - apply (simp add: cleanCacheRange_RAM_def doMachineOp_bind empty_fail_dsb empty_fail_cleanL2Range) + apply (simp add: cleanCacheRange_RAM_def doMachineOp_bind empty_fail_dsb empty_fail_cleanL2Range + empty_fail_cond) apply (rule ccorres_Guard_Seq) apply (rule ccorres_basic_srnoop2, simp) apply (ctac (no_vcg) add: cleanCacheRange_PoC_ccorres) @@ -536,8 +537,8 @@ lemma invalidateCacheRange_RAM_ccorres: apply (clarsimp simp: word_sle_def whileAnno_def split del: if_split) apply (ccorres_remove_UNIV_guard) apply (simp add: invalidateCacheRange_RAM_def doMachineOp_bind when_def - if_split_empty_fail empty_fail_invalidateL2Range empty_fail_invalidateByVA - empty_fail_dsb dmo_if + empty_fail_invalidateL2Range empty_fail_invalidateByVA + empty_fail_dsb dmo_if empty_fail_cond split del: if_split) apply (rule ccorres_split_nothrow_novcg) apply (rule ccorres_cond[where R=\]) @@ -646,7 +647,7 @@ lemma cleanCaches_PoU_ccorres: (doMachineOp cleanCaches_PoU) (Call cleanCaches_PoU_'proc)" apply cinit' - apply (simp add: cleanCaches_PoU_def doMachineOp_bind + apply (simp add: cleanCaches_PoU_def doMachineOp_bind empty_fail_cond empty_fail_dsb empty_fail_clean_D_PoU empty_fail_invalidate_I_PoU) apply (ctac (no_vcg) add: dsb_ccorres) apply (ctac (no_vcg) add: clean_D_PoU_ccorres) @@ -672,7 +673,7 @@ lemma setCurrentPD_ccorres: (Call setCurrentPD_'proc)" apply cinit' apply (clarsimp simp: setCurrentPD_def doMachineOp_bind empty_fail_dsb empty_fail_isb - writeTTBR0_empty_fail + writeTTBR0_empty_fail empty_fail_cond intro!: ccorres_cond_empty) apply (rule ccorres_rhs_assoc)+ apply (ctac (no_vcg) add: dsb_ccorres) diff --git a/proof/crefine/ARM/Retype_C.thy b/proof/crefine/ARM/Retype_C.thy index 3e1d369f5..92e223e05 100644 --- a/proof/crefine/ARM/Retype_C.thy +++ b/proof/crefine/ARM/Retype_C.thy @@ -2103,8 +2103,8 @@ lemma getCTE_pre_cte_at: apply clarsimp done -lemmas ccorres_guard_from_wp_liftM = ccorres_guard_from_wp [OF liftM_pre iffD2 [OF empty_fail_liftM]] -lemmas ccorres_guard_from_wp_bind_liftM = ccorres_guard_from_wp_bind [OF liftM_pre iffD2 [OF empty_fail_liftM]] +lemmas ccorres_guard_from_wp_liftM = ccorres_guard_from_wp [OF liftM_pre empty_fail_liftM] +lemmas ccorres_guard_from_wp_bind_liftM = ccorres_guard_from_wp_bind [OF liftM_pre empty_fail_liftM] lemmas ccorres_liftM_getCTE_cte_at = ccorres_guard_from_wp_liftM [OF getCTE_pre_cte_at empty_fail_getCTE] ccorres_guard_from_wp_bind_liftM [OF getCTE_pre_cte_at empty_fail_getCTE] @@ -5998,7 +5998,8 @@ lemma createObject_caps_overlap_reserved_ret': apply clarsimp apply (rule hoare_strengthen_post[OF createNewCaps_caps_overlap_reserved_ret'[where sz = "APIType_capBits ty us"]]) apply assumption - apply (case_tac r,simp) + apply (rename_tac rv s) + apply (case_tac rv,simp) apply clarsimp apply (erule caps_overlap_reserved'_subseteq) apply (rule untypedRange_in_capRange) @@ -6067,7 +6068,8 @@ lemma createObject_IRQHandler: apply clarsimp apply (rule hoare_strengthen_post[OF createNewCaps_IRQHandler[where irq = x and P = "\_ _. False"]]) apply assumption - apply (case_tac r,clarsimp+) + apply (rename_tac rv s) + apply (case_tac rv; clarsimp) apply (clarsimp simp:word_bits_conv) done @@ -6084,7 +6086,8 @@ lemma createObject_capClass[wp]: apply clarsimp apply (rule hoare_strengthen_post[OF createNewCaps_range_helper]) apply assumption - apply (case_tac r,clarsimp+) + apply (rename_tac rv s) + apply (case_tac rv; clarsimp) apply (clarsimp simp:word_bits_conv ) apply (rule range_cover_full) apply (simp add:word_bits_conv)+ diff --git a/proof/crefine/ARM/SyscallArgs_C.thy b/proof/crefine/ARM/SyscallArgs_C.thy index 1e79117b7..903b61c23 100644 --- a/proof/crefine/ARM/SyscallArgs_C.thy +++ b/proof/crefine/ARM/SyscallArgs_C.thy @@ -1194,7 +1194,7 @@ lemma getSyscallArg_ccorres_foo: apply (simp add: index_msgRegisters_less unat_less_helper) apply wp[1] apply (wp getMRs_tcbContext) - apply simp + apply fastforce apply (rule ccorres_seq_skip [THEN iffD2]) apply (rule ccorres_add_return2) apply (rule ccorres_symb_exec_l) @@ -1218,7 +1218,7 @@ lemma getSyscallArg_ccorres_foo: in hoare_pre(1)) apply (wp getMRs_user_word) apply (clarsimp simp: msgMaxLength_def unat_less_helper) - apply simp + apply fastforce apply (clarsimp simp: sysargs_rel_def sysargs_rel_n_def) apply (rule conjI, clarsimp simp: unat_of_nat32 word_bits_def) apply (drule equalityD2) diff --git a/proof/crefine/ARM/Tcb_C.thy b/proof/crefine/ARM/Tcb_C.thy index d2383932a..9bc8943d6 100644 --- a/proof/crefine/ARM/Tcb_C.thy +++ b/proof/crefine/ARM/Tcb_C.thy @@ -1469,6 +1469,7 @@ lemma invokeTCB_WriteRegisters_ccorres[where S=UNIV]: \ {s. buffer_' s = option_to_ptr buffer}) [] (invokeTCB (WriteRegisters dst resume values arch)) (Call invokeTCB_WriteRegisters_'proc)" + supply empty_fail_cond[simp] apply (rule ccorres_gen_asm) apply (erule conjE) apply (cinit lift: n_' dest_' resumeTarget_' buffer_' @@ -1707,7 +1708,7 @@ shows (doE reply \ invokeTCB (ReadRegisters target susp n archCp); liftE (replyOnRestart thread reply isCall) odE) (Call invokeTCB_ReadRegisters_'proc)" - supply option.case_cong_weak[cong] + supply option.case_cong_weak[cong] empty_fail_cond[simp] apply (rule ccorres_gen_asm) apply (cinit' lift: tcb_src_' suspendSource_' n_' call_' simp: invokeTCB_def liftE_bindE bind_assoc) @@ -3566,11 +3567,10 @@ lemma decodeSetSchedParams_ccorres: apply (simp only: cap_get_tag_isCap[symmetric], drule(1) cap_get_tag_to_H) apply (clarsimp simp: valid_cap'_def capAligned_def interpret_excaps_eq excaps_map_def) apply (intro conjI impI allI) - apply (clarsimp simp: unat_eq_0 le_max_word_ucast_id - thread_control_update_mcp_def thread_control_update_priority_def - cap_get_tag_isCap_unfolded_H_cap isCap_simps - interpret_excaps_eq excaps_map_def)+ - done + by (clarsimp simp: unat_eq_0 le_max_word_ucast_id + thread_control_update_mcp_def thread_control_update_priority_def + cap_get_tag_isCap_unfolded_H_cap isCap_simps + interpret_excaps_eq excaps_map_def)+ lemma decodeSetIPCBuffer_ccorres: "interpret_excaps extraCaps' = excaps_map extraCaps \ diff --git a/proof/crefine/ARM/VSpace_C.thy b/proof/crefine/ARM/VSpace_C.thy index 4f8e72df6..670430c4d 100644 --- a/proof/crefine/ARM/VSpace_C.thy +++ b/proof/crefine/ARM/VSpace_C.thy @@ -1594,7 +1594,9 @@ lemma doFlush_ccorres: apply (rule ccorres_cond_false) apply (rule ccorres_cond_false) apply (rule ccorres_cond_true) - apply (simp add: empty_fail_cleanCacheRange_PoU empty_fail_dsb empty_fail_invalidateCacheRange_I empty_fail_branchFlushRange empty_fail_isb doMachineOp_bind) + apply (simp add: empty_fail_cond empty_fail_cleanCacheRange_PoU empty_fail_dsb + empty_fail_invalidateCacheRange_I empty_fail_branchFlushRange empty_fail_isb + doMachineOp_bind) apply (rule ccorres_rhs_assoc)+ apply (fold dc_def) apply (ctac (no_vcg) add: cleanCacheRange_PoU_ccorres) diff --git a/proof/crefine/ARM_HYP/ArchMove_C.thy b/proof/crefine/ARM_HYP/ArchMove_C.thy index 047455718..ccd1b36fd 100644 --- a/proof/crefine/ARM_HYP/ArchMove_C.thy +++ b/proof/crefine/ARM_HYP/ArchMove_C.thy @@ -187,21 +187,13 @@ lemma dmo_invalidateCacheRange_RAM_invs'[wp]: lemma empty_fail_findPDForASID[iff]: "empty_fail (findPDForASID asid)" - apply (simp add: findPDForASID_def liftME_def) - apply (intro empty_fail_bindE, simp_all split: option.split) - apply (simp add: assertE_def split: if_split) - apply (simp add: assertE_def split: if_split) - apply (simp add: empty_fail_getObject) - apply (simp add: assertE_def liftE_bindE checkPDAt_def split: if_split) - done + unfolding findPDForASID_def checkPDAt_def + by (wpsimp wp: empty_fail_getObject) lemma empty_fail_findPDForASIDAssert[iff]: "empty_fail (findPDForASIDAssert asid)" - apply (simp add: findPDForASIDAssert_def catch_def - checkPDAt_def checkPDUniqueToASID_def - checkPDASIDMapMembership_def) - apply (intro empty_fail_bind, simp_all split: sum.split) - done + unfolding findPDForASIDAssert_def checkPDAt_def checkPDUniqueToASID_def checkPDASIDMapMembership_def + by (wpsimp wp: empty_fail_getObject) lemma vcpu_at_ko: "vcpu_at' p s \ \vcpu. ko_at' (vcpu::vcpu) p s" @@ -229,7 +221,7 @@ lemma atg_sp': (* FIXME: MOVE to EmptyFail *) lemma empty_fail_archThreadGet [intro!, wp, simp]: "empty_fail (archThreadGet f p)" - by (simp add: archThreadGet_def getObject_def split_def) + by (fastforce simp: archThreadGet_def getObject_def split_def) lemma mab_gt_2 [simp]: "2 \ msg_align_bits" by (simp add: msg_align_bits) @@ -608,7 +600,7 @@ lemma cap_case_isPageDirectoryCap: lemma empty_fail_loadWordUser[intro!, simp]: "empty_fail (loadWordUser x)" - by (simp add: loadWordUser_def ef_loadWord ef_dmo') + by (fastforce simp: loadWordUser_def ef_loadWord ef_dmo') lemma empty_fail_getMRs[iff]: "empty_fail (getMRs t buf mi)" @@ -618,26 +610,14 @@ lemma empty_fail_getReceiveSlots: "empty_fail (getReceiveSlots r rbuf)" proof - note - empty_fail_assertE[iff] - empty_fail_resolveAddressBits[iff] + empty_fail_resolveAddressBits[wp] + empty_fail_rethrowFailure[wp] + empty_fail_rethrowFailure[wp] show ?thesis - apply (clarsimp simp: getReceiveSlots_def loadCapTransfer_def split_def - split: option.split) - apply (rule empty_fail_bind) - apply (simp add: capTransferFromWords_def) - apply (simp add: emptyOnFailure_def unifyFailure_def) - apply (intro empty_fail_catch empty_fail_bindE empty_fail_rethrowFailure, - simp_all add: empty_fail_whenEs) - apply (simp_all add: lookupCap_def split_def lookupCapAndSlot_def - lookupSlotForThread_def liftME_def - getThreadCSpaceRoot_def locateSlot_conv bindE_assoc - lookupSlotForCNodeOp_def lookupErrorOnFailure_def - cong: if_cong) - apply (intro empty_fail_bindE, - simp_all add: getSlotCap_def) - apply (intro empty_fail_If empty_fail_bindE empty_fail_rethrowFailure impI, - simp_all add: empty_fail_whenEs rangeCheck_def) - done + unfolding getReceiveSlots_def loadCapTransfer_def lookupCap_def lookupCapAndSlot_def + by (wpsimp simp: emptyOnFailure_def unifyFailure_def lookupSlotForThread_def + capTransferFromWords_def getThreadCSpaceRoot_def locateSlot_conv bindE_assoc + lookupSlotForCNodeOp_def lookupErrorOnFailure_def rangeCheck_def) qed lemma user_getreg_rv: diff --git a/proof/crefine/ARM_HYP/CLevityCatch.thy b/proof/crefine/ARM_HYP/CLevityCatch.thy index 734f15bc4..9646e184f 100644 --- a/proof/crefine/ARM_HYP/CLevityCatch.thy +++ b/proof/crefine/ARM_HYP/CLevityCatch.thy @@ -64,12 +64,12 @@ lemma empty_fail_getExtraCPtrs [intro!, simp]: "empty_fail (getExtraCPtrs sendBuffer info)" apply (simp add: getExtraCPtrs_def) apply (cases info, simp) - apply (cases sendBuffer, simp_all) + apply (cases sendBuffer; fastforce) done lemma empty_fail_loadCapTransfer [intro!, simp]: "empty_fail (loadCapTransfer a)" - by (simp add: loadCapTransfer_def capTransferFromWords_def) + by (fastforce simp: loadCapTransfer_def capTransferFromWords_def) lemma empty_fail_emptyOnFailure [intro!, simp]: "empty_fail m \ empty_fail (emptyOnFailure m)" @@ -89,7 +89,7 @@ lemma asUser_get_registers: apply (simp add: mapM_empty asUser_return) apply wp apply simp - apply (simp add: mapM_Cons asUser_bind_distrib asUser_return) + apply (simp add: mapM_Cons asUser_bind_distrib asUser_return empty_fail_cond) apply wp apply simp apply (rule hoare_strengthen_post) diff --git a/proof/crefine/ARM_HYP/Fastpath_Equiv.thy b/proof/crefine/ARM_HYP/Fastpath_Equiv.thy index eb1def7b9..1aacccb1a 100644 --- a/proof/crefine/ARM_HYP/Fastpath_Equiv.thy +++ b/proof/crefine/ARM_HYP/Fastpath_Equiv.thy @@ -867,7 +867,7 @@ lemma receiveIPC_simple_rewrite: lemma empty_fail_isFinalCapability: "empty_fail (isFinalCapability cte)" - by (simp add: isFinalCapability_def Let_def split: if_split) + by (simp add: isFinalCapability_def Let_def empty_fail_cond split: if_split) lemma cteDeleteOne_replycap_rewrite: "monadic_rewrite True False diff --git a/proof/crefine/ARM_HYP/Finalise_C.thy b/proof/crefine/ARM_HYP/Finalise_C.thy index 3b290744c..0c7eef48d 100644 --- a/proof/crefine/ARM_HYP/Finalise_C.thy +++ b/proof/crefine/ARM_HYP/Finalise_C.thy @@ -1334,7 +1334,7 @@ lemma setObject_ccorres_lemma: apply (subgoal_tac "fst (setObject ptr val \) = {}") apply simp apply (erule notE, erule_tac s=\ in empty_failD[rotated]) - apply (simp add: setObject_def split_def) + apply (simp add: setObject_def split_def empty_fail_cond) apply (rule ccontr) apply (clarsimp elim!: nonemptyE) apply (frule use_valid [OF _ obj_at_setObject3[where P=\]], simp_all)[1] diff --git a/proof/crefine/ARM_HYP/IpcCancel_C.thy b/proof/crefine/ARM_HYP/IpcCancel_C.thy index 5623d522e..bc7925a94 100644 --- a/proof/crefine/ARM_HYP/IpcCancel_C.thy +++ b/proof/crefine/ARM_HYP/IpcCancel_C.thy @@ -2396,6 +2396,7 @@ lemma scheduleTCB_ccorres': rescheduleRequired od) (Call scheduleTCB_'proc)" + supply empty_fail_cond[simp] apply (cinit' lift: tptr_' simp del: word_neq_0_conv) apply (rule ccorres_rhs_assoc2)+ apply (rule_tac xf'="ret__int_'" in ccorres_split_nothrow_novcg) @@ -2450,6 +2451,7 @@ lemma scheduleTCB_ccorres_valid_queues'_pre: when (\ runnable \ curThread = thread \ action = ResumeCurrentThread) rescheduleRequired od) (Call scheduleTCB_'proc)" + supply empty_fail_cond[simp] apply (cinit' lift: tptr_' simp del: word_neq_0_conv) apply (rule ccorres_rhs_assoc2)+ apply (rule_tac xf'="ret__int_'" in ccorres_split_nothrow_novcg) @@ -2542,6 +2544,7 @@ lemma scheduleTCB_ccorres_valid_queues'_pre_simple: when (\ runnable \ curThread = thread \ action = ResumeCurrentThread) rescheduleRequired od) (Call scheduleTCB_'proc)" + supply empty_fail_cond[simp] apply (cinit' lift: tptr_' simp del: word_neq_0_conv) apply (rule ccorres_rhs_assoc2)+ apply (rule_tac xf'="ret__int_'" in ccorres_split_nothrow_novcg) diff --git a/proof/crefine/ARM_HYP/Ipc_C.thy b/proof/crefine/ARM_HYP/Ipc_C.thy index 7b7aa1bf7..407375c18 100644 --- a/proof/crefine/ARM_HYP/Ipc_C.thy +++ b/proof/crefine/ARM_HYP/Ipc_C.thy @@ -466,6 +466,7 @@ lemma handleArchFaultReply': msg \ getMRs s sb tag; handleArchFaultReply f r (msgLabel tag) msg od) x' = handleArchFaultReply' f s r tag x'" + supply empty_fail_cond[simp] apply (unfold handleArchFaultReply'_def getMRs_def msgMaxLength_def bit_def msgLengthBits_def msgRegisters_unfold fromIntegral_simp1 fromIntegral_simp2 @@ -628,7 +629,7 @@ lemma handleFaultReply': msg \ getMRs s sb tag; handleFaultReply f r (msgLabel tag) msg od) (handleFaultReply' f s r)" - supply if_cong[cong] + supply if_cong[cong] empty_fail_cond[simp] supply empty_fail_asUser[wp] empty_fail_getRegister[wp] apply (unfold handleFaultReply'_def getMRs_def msgMaxLength_def bit_def msgLengthBits_def msgRegisters_unfold @@ -2013,6 +2014,7 @@ proof - let ?obj_at_ft = "obj_at' (\tcb. tcbFault tcb = Some ft) sender" note symb_exec_r_fault = ccorres_symb_exec_r_known_rv_UNIV [where xf'=ret__unsigned_' and R="?obj_at_ft" and R'=UNIV] + note empty_fail_cond[simp] show ?thesis apply (unfold K_def) apply (intro ccorres_gen_asm) @@ -3388,6 +3390,7 @@ proof - let ?EXCNONE = "{s. ret__unsigned_long_' s = scast EXCEPTION_NONE}" let ?interpret = "\v n. take n (array_to_list (excaprefs_C v))" note if_split[split del] + note empty_fail_cond[simp] show ?thesis apply (rule ccorres_gen_asm)+ apply (cinit(no_subst_asm) lift: thread_' bufferPtr_' info_' simp: whileAnno_def) diff --git a/proof/crefine/ARM_HYP/IsolatedThreadAction.thy b/proof/crefine/ARM_HYP/IsolatedThreadAction.thy index bd013597b..e9438a8c4 100644 --- a/proof/crefine/ARM_HYP/IsolatedThreadAction.thy +++ b/proof/crefine/ARM_HYP/IsolatedThreadAction.thy @@ -1016,7 +1016,7 @@ lemma rescheduleRequired_simple_rewrite: (* FIXME move *) lemma empty_fail_isRunnable[intro!, wp, simp]: "empty_fail (isRunnable t)" - by (simp add: isRunnable_def isStopped_def) + by (simp add: isRunnable_def isStopped_def empty_fail_cond) lemma setupCallerCap_rewrite: "monadic_rewrite True True (\s. reply_masters_rvk_fb (ctes_of s)) diff --git a/proof/crefine/ARM_HYP/Machine_C.thy b/proof/crefine/ARM_HYP/Machine_C.thy index 66e8fa7c4..191ca7271 100644 --- a/proof/crefine/ARM_HYP/Machine_C.thy +++ b/proof/crefine/ARM_HYP/Machine_C.thy @@ -588,7 +588,7 @@ lemma cleanInvalidateCacheRange_RAM_ccorres: apply (rule ccorres_basic_srnoop) apply (simp add: cleanInvalidateCacheRange_RAM_def doMachineOp_bind empty_fail_dsb empty_fail_cleanInvalidateL2Range - empty_fail_cleanInvalByVA) + empty_fail_cleanInvalByVA empty_fail_cond) apply (ctac (no_vcg) add: cleanCacheRange_PoC_ccorres) apply (ctac (no_vcg) add: dsb_ccorres) apply (ctac (no_vcg) add: plat_cleanInvalidateL2Range_ccorres) @@ -620,7 +620,8 @@ lemma cleanCacheRange_RAM_ccorres: (doMachineOp (cleanCacheRange_RAM w1 w2 w3)) (Call cleanCacheRange_RAM_'proc)" apply (cinit' lift: start_' end_' pstart_') - apply (simp add: cleanCacheRange_RAM_def doMachineOp_bind empty_fail_dsb empty_fail_cleanL2Range) + apply (simp add: cleanCacheRange_RAM_def doMachineOp_bind empty_fail_dsb empty_fail_cleanL2Range + empty_fail_cond) apply (rule ccorres_Guard_Seq) apply (rule ccorres_basic_srnoop2, simp) apply (ctac (no_vcg) add: cleanCacheRange_PoC_ccorres) @@ -680,9 +681,9 @@ lemma invalidateCacheRange_RAM_ccorres: apply (cinit' lift: start_' end_' pstart_') apply (clarsimp simp: word_sle_def whileAnno_def split del: if_split) apply (simp add: invalidateCacheRange_RAM_def doMachineOp_bind when_def - if_split_empty_fail empty_fail_invalidateL2Range empty_fail_invalidateByVA - empty_fail_dsb dmo_if - split del: if_split) + empty_fail_invalidateL2Range empty_fail_invalidateByVA + empty_fail_dsb dmo_if empty_fail_cond + split del: if_split) apply (rule ccorres_split_nothrow_novcg) apply (rule ccorres_cond[where R=\]) apply (clarsimp simp: lineStart_def cacheLineBits_def) @@ -776,7 +777,7 @@ lemma cleanCaches_PoU_ccorres: (doMachineOp cleanCaches_PoU) (Call cleanCaches_PoU_'proc)" apply cinit' - apply (simp add: cleanCaches_PoU_def doMachineOp_bind + apply (simp add: cleanCaches_PoU_def doMachineOp_bind empty_fail_cond empty_fail_dsb empty_fail_clean_D_PoU empty_fail_invalidate_I_PoU) apply (ctac (no_vcg) add: dsb_ccorres) apply (ctac (no_vcg) add: clean_D_PoU_ccorres) @@ -793,7 +794,7 @@ lemma setCurrentPD_ccorres: (Call setCurrentPD_'proc)" apply cinit' apply (clarsimp simp: setCurrentPD_def doMachineOp_bind empty_fail_dsb empty_fail_isb - setCurrentPDPL2_empty_fail + setCurrentPDPL2_empty_fail empty_fail_cond intro!: ccorres_cond_empty) apply (ctac (no_vcg) add: setCurrentPDPL2_ccorres) apply wpsimp diff --git a/proof/crefine/ARM_HYP/Retype_C.thy b/proof/crefine/ARM_HYP/Retype_C.thy index f5234902f..d8ae56970 100644 --- a/proof/crefine/ARM_HYP/Retype_C.thy +++ b/proof/crefine/ARM_HYP/Retype_C.thy @@ -2470,8 +2470,8 @@ lemma getCTE_pre_cte_at: lemmas ccorres_getCTE_cte_at = ccorres_guard_from_wp [OF getCTE_pre_cte_at empty_fail_getCTE] ccorres_guard_from_wp_bind [OF getCTE_pre_cte_at empty_fail_getCTE] -lemmas ccorres_guard_from_wp_liftM = ccorres_guard_from_wp [OF liftM_pre iffD2 [OF empty_fail_liftM]] -lemmas ccorres_guard_from_wp_bind_liftM = ccorres_guard_from_wp_bind [OF liftM_pre iffD2 [OF empty_fail_liftM]] +lemmas ccorres_guard_from_wp_liftM = ccorres_guard_from_wp [OF liftM_pre empty_fail_liftM] +lemmas ccorres_guard_from_wp_bind_liftM = ccorres_guard_from_wp_bind [OF liftM_pre empty_fail_liftM] lemmas ccorres_liftM_getCTE_cte_at = ccorres_guard_from_wp_liftM [OF getCTE_pre_cte_at empty_fail_getCTE] ccorres_guard_from_wp_bind_liftM [OF getCTE_pre_cte_at empty_fail_getCTE] @@ -7331,7 +7331,8 @@ lemma createObject_caps_overlap_reserved_ret': apply clarsimp apply (rule hoare_strengthen_post[OF createNewCaps_caps_overlap_reserved_ret'[where sz = "APIType_capBits ty us"]]) apply assumption - apply (case_tac r,simp) + apply (rename_tac rv s) + apply (case_tac rv,simp) apply clarsimp apply (erule caps_overlap_reserved'_subseteq) apply (rule untypedRange_in_capRange) @@ -7404,7 +7405,8 @@ lemma createObject_IRQHandler: apply clarsimp apply (rule hoare_strengthen_post[OF createNewCaps_IRQHandler[where irq = x and P = "\_ _. False"]]) apply assumption - apply (case_tac r,clarsimp+) + apply (rename_tac rv s) + apply (case_tac rv; clarsimp) apply (clarsimp simp:word_bits_conv) done @@ -7421,7 +7423,8 @@ lemma createObject_capClass[wp]: apply clarsimp apply (rule hoare_strengthen_post[OF createNewCaps_range_helper]) apply assumption - apply (case_tac r,clarsimp+) + apply (rename_tac rv s) + apply (case_tac rv; clarsimp) apply (clarsimp simp:word_bits_conv ) apply (rule range_cover_full) apply (simp add:word_bits_conv)+ diff --git a/proof/crefine/ARM_HYP/SyscallArgs_C.thy b/proof/crefine/ARM_HYP/SyscallArgs_C.thy index b4795ea32..e17b14a61 100644 --- a/proof/crefine/ARM_HYP/SyscallArgs_C.thy +++ b/proof/crefine/ARM_HYP/SyscallArgs_C.thy @@ -1228,7 +1228,7 @@ lemma getSyscallArg_ccorres_foo: apply (simp add: index_msgRegisters_less unat_less_helper) apply wp[1] apply (wp getMRs_tcbContext) - apply simp + apply fastforce apply (rule ccorres_seq_skip [THEN iffD2]) apply (rule ccorres_add_return2) apply (rule ccorres_symb_exec_l) @@ -1252,7 +1252,7 @@ lemma getSyscallArg_ccorres_foo: in hoare_pre(1)) apply (wp getMRs_user_word) apply (clarsimp simp: msgMaxLength_def unat_less_helper) - apply simp + apply fastforce apply (clarsimp simp: sysargs_rel_def sysargs_rel_n_def) apply (rule conjI, clarsimp simp: unat_of_nat32 word_bits_def) apply (drule equalityD2) diff --git a/proof/crefine/ARM_HYP/Tcb_C.thy b/proof/crefine/ARM_HYP/Tcb_C.thy index af1553c0a..ed4388afc 100644 --- a/proof/crefine/ARM_HYP/Tcb_C.thy +++ b/proof/crefine/ARM_HYP/Tcb_C.thy @@ -1540,6 +1540,7 @@ lemma invokeTCB_WriteRegisters_ccorres[where S=UNIV]: \ {s. buffer_' s = option_to_ptr buffer}) [] (invokeTCB (WriteRegisters dst resume values arch)) (Call invokeTCB_WriteRegisters_'proc)" + supply empty_fail_cond[simp] apply (rule ccorres_gen_asm) apply (erule conjE) apply (cinit lift: n_' dest_' resumeTarget_' buffer_' @@ -1788,6 +1789,7 @@ shows (doE reply \ invokeTCB (ReadRegisters target susp n archCp); liftE (replyOnRestart thread reply isCall) odE) (Call invokeTCB_ReadRegisters_'proc)" + supply empty_fail_cond[simp] apply (rule ccorres_gen_asm) using [[goals_limit=1]] apply (cinit' lift: tcb_src_' suspendSource_' n_' call_' simp: invokeTCB_def liftE_bindE bind_assoc) @@ -3652,11 +3654,10 @@ lemma decodeSetSchedParams_ccorres: apply (simp only: cap_get_tag_isCap[symmetric], drule(1) cap_get_tag_to_H) apply (clarsimp simp: valid_cap'_def capAligned_def interpret_excaps_eq excaps_map_def) apply (intro conjI impI allI) - apply (clarsimp simp: unat_eq_0 le_max_word_ucast_id - thread_control_update_mcp_def thread_control_update_priority_def - cap_get_tag_isCap_unfolded_H_cap isCap_simps - interpret_excaps_eq excaps_map_def)+ - done + by (clarsimp simp: unat_eq_0 le_max_word_ucast_id + thread_control_update_mcp_def thread_control_update_priority_def + cap_get_tag_isCap_unfolded_H_cap isCap_simps + interpret_excaps_eq excaps_map_def)+ lemma decodeSetIPCBuffer_ccorres: "interpret_excaps extraCaps' = excaps_map extraCaps \ diff --git a/proof/crefine/ARM_HYP/VSpace_C.thy b/proof/crefine/ARM_HYP/VSpace_C.thy index 6b47927fa..5b3c0365e 100644 --- a/proof/crefine/ARM_HYP/VSpace_C.thy +++ b/proof/crefine/ARM_HYP/VSpace_C.thy @@ -2022,7 +2022,7 @@ lemma vcpu_disable_ccorres: and (case v of None \ \ | Some new \ vcpu_at' new)) (UNIV \ {s. vcpu_' s = option_to_ptr v}) hs (vcpuDisable v) (Call vcpu_disable_'proc)" - supply if_cong[cong] option.case_cong[cong] + supply if_cong[cong] option.case_cong[cong] empty_fail_cond[simp] apply (cinit lift: vcpu_') apply (ctac (no_vcg) add: dsb_ccorres) apply (rule ccorres_split_nothrow_novcg) @@ -2072,6 +2072,7 @@ lemma vcpu_enable_ccorres: and valid_arch_state' and vcpu_at' v) (UNIV \ {s. vcpu_' s = vcpu_Ptr v}) hs (vcpuEnable v) (Call vcpu_enable_'proc)" + supply empty_fail_cond[simp] apply (cinit lift: vcpu_') apply (ctac (no_vcg) add: vcpu_restore_reg_ccorres)+ apply (rule ccorres_pre_getObject_vcpu, rename_tac vcpu) @@ -2132,6 +2133,7 @@ lemma vcpu_restore_ccorres: and vcpu_at' vcpuPtr) (UNIV \ {s. vcpu_' s = vcpu_Ptr vcpuPtr}) hs (vcpuRestore vcpuPtr) (Call vcpu_restore_'proc)" + supply empty_fail_cond[simp] apply (cinit lift: vcpu_' simp: whileAnno_def) apply (simp add: doMachineOp_bind uncurry_def split_def doMachineOp_mapM_x)+ apply (clarsimp simp: bind_assoc) @@ -2724,7 +2726,7 @@ lemma doFlush_ccorres: apply (rule ccorres_cond_true) apply (simp add: empty_fail_cleanCacheRange_PoU empty_fail_dsb empty_fail_invalidateCacheRange_I empty_fail_branchFlushRange empty_fail_isb - doMachineOp_bind) + doMachineOp_bind empty_fail_cond) apply (rule ccorres_rhs_assoc)+ apply (fold dc_def) apply (ctac (no_vcg) add: cleanCacheRange_PoU_ccorres) diff --git a/proof/crefine/Move_C.thy b/proof/crefine/Move_C.thy index a0b3c0f45..38b60bfe1 100644 --- a/proof/crefine/Move_C.thy +++ b/proof/crefine/Move_C.thy @@ -670,6 +670,7 @@ lemma empty_fail_asUser[iff]: lemma asUser_mapM_x: "(\x. empty_fail (f x)) \ asUser t (mapM_x f xs) = do stateAssert (tcb_at' t) []; mapM_x (\x. asUser t (f x)) xs od" + supply empty_fail_cond[simp] apply (simp add: mapM_x_mapM asUser_bind_distrib) apply (subst submonad_mapM [OF submonad_asUser submonad_asUser]) apply simp @@ -785,7 +786,7 @@ lemma empty_fail_rethrowFailure: lemma empty_fail_resolveAddressBits: "empty_fail (resolveAddressBits cap cptr bits)" proof - - note empty_fail_assertE[iff] + note empty_fail_cond[simp] show ?thesis apply (rule empty_fail_use_cutMon) apply (induct rule: resolveAddressBits.induct) @@ -793,8 +794,7 @@ proof - apply (unfold Let_def cnode_cap_case_if fun_app_def K_bind_def haskell_assertE_def split_def) apply (intro empty_fail_cutMon_intros) - apply (clarsimp simp: empty_fail_drop_cutMon empty_fail_whenEs - locateSlot_conv returnOk_liftE[symmetric] + apply (clarsimp simp: empty_fail_drop_cutMon locateSlot_conv returnOk_liftE[symmetric] isCap_simps)+ done qed @@ -828,8 +828,9 @@ lemma getMessageInfo_le3: apply wp apply (rule_tac Q="\_. \" in hoare_strengthen_post) apply wp + apply (rename_tac rv s) apply (simp add: messageInfoFromWord_def Let_def msgExtraCapBits_def) - apply (cut_tac y="r >> Types_H.msgLengthBits" in word_and_le1 [where a=3]) + apply (cut_tac y="rv >> Types_H.msgLengthBits" in word_and_le1 [where a=3]) apply (simp add: word_le_nat_alt) done @@ -998,8 +999,7 @@ lemma empty_fail_slotCapLongRunningDelete: "empty_fail (slotCapLongRunningDelete slot)" by (auto simp: slotCapLongRunningDelete_def Let_def case_Null_If isFinalCapability_def - split: if_split - intro!: empty_fail_bind) + split: if_split) lemmas mapM_x_append = mapM_x_append2 @@ -1020,9 +1020,6 @@ lemma getSlotCap_wp': apply (clarsimp simp: cte_wp_at_ctes_of) done -lemma fromIntegral_simp_nat[simp]: "(fromIntegral :: nat \ nat) = id" - by (simp add: fromIntegral_def fromInteger_nat toInteger_nat) - lemma invs_cicd_valid_objs' [elim!]: "all_invs_but_ct_idle_or_in_cur_domain' s \ valid_objs' s" by (simp add: all_invs_but_ct_idle_or_in_cur_domain'_def valid_pspace'_def) diff --git a/proof/crefine/RISCV64/ArchMove_C.thy b/proof/crefine/RISCV64/ArchMove_C.thy index f400e9ea3..a5b9dea12 100644 --- a/proof/crefine/RISCV64/ArchMove_C.thy +++ b/proof/crefine/RISCV64/ArchMove_C.thy @@ -93,7 +93,7 @@ lemma atg_sp': (* FIXME: MOVE to EmptyFail *) lemma empty_fail_archThreadGet [intro!, wp, simp]: "empty_fail (archThreadGet f p)" - by (simp add: archThreadGet_def getObject_def split_def) + by (fastforce simp: archThreadGet_def getObject_def split_def) (* FIXME: move to ainvs? *) lemma sign_extend_canonical_address: @@ -377,7 +377,7 @@ lemma length_msgRegisters[simplified size_msgRegisters_def]: lemma empty_fail_loadWordUser[intro!, simp]: "empty_fail (loadWordUser x)" - by (simp add: loadWordUser_def ef_loadWord ef_dmo') + by (fastforce simp: loadWordUser_def ef_loadWord ef_dmo') lemma empty_fail_getMRs[iff]: "empty_fail (getMRs t buf mi)" @@ -387,26 +387,14 @@ lemma empty_fail_getReceiveSlots: "empty_fail (getReceiveSlots r rbuf)" proof - note - empty_fail_assertE[iff] - empty_fail_resolveAddressBits[iff] + empty_fail_resolveAddressBits[wp] + empty_fail_rethrowFailure[wp] + empty_fail_rethrowFailure[wp] show ?thesis - apply (clarsimp simp: getReceiveSlots_def loadCapTransfer_def split_def - split: option.split) - apply (rule empty_fail_bind) - apply (simp add: capTransferFromWords_def) - apply (simp add: emptyOnFailure_def unifyFailure_def) - apply (intro empty_fail_catch empty_fail_bindE empty_fail_rethrowFailure, - simp_all add: empty_fail_whenEs) - apply (simp_all add: lookupCap_def split_def lookupCapAndSlot_def - lookupSlotForThread_def liftME_def - getThreadCSpaceRoot_def locateSlot_conv bindE_assoc - lookupSlotForCNodeOp_def lookupErrorOnFailure_def - cong: if_cong) - apply (intro empty_fail_bindE, - simp_all add: getSlotCap_def) - apply (intro empty_fail_If empty_fail_bindE empty_fail_rethrowFailure impI, - simp_all add: empty_fail_whenEs rangeCheck_def) - done + unfolding getReceiveSlots_def loadCapTransfer_def lookupCap_def lookupCapAndSlot_def + by (wpsimp simp: emptyOnFailure_def unifyFailure_def lookupSlotForThread_def + capTransferFromWords_def getThreadCSpaceRoot_def locateSlot_conv bindE_assoc + lookupSlotForCNodeOp_def lookupErrorOnFailure_def rangeCheck_def) qed lemma user_getreg_rv: diff --git a/proof/crefine/RISCV64/CLevityCatch.thy b/proof/crefine/RISCV64/CLevityCatch.thy index 6692c171a..691ea86ee 100644 --- a/proof/crefine/RISCV64/CLevityCatch.thy +++ b/proof/crefine/RISCV64/CLevityCatch.thy @@ -65,12 +65,12 @@ lemma empty_fail_getExtraCPtrs [intro!, simp]: "empty_fail (getExtraCPtrs sendBuffer info)" apply (simp add: getExtraCPtrs_def) apply (cases info, simp) - apply (cases sendBuffer, simp_all) + apply (cases sendBuffer; fastforce) done lemma empty_fail_loadCapTransfer [intro!, simp]: "empty_fail (loadCapTransfer a)" - by (simp add: loadCapTransfer_def capTransferFromWords_def) + by (fastforce simp: loadCapTransfer_def capTransferFromWords_def) lemma empty_fail_emptyOnFailure [intro!, simp]: "empty_fail m \ empty_fail (emptyOnFailure m)" @@ -90,7 +90,7 @@ lemma asUser_get_registers: apply (simp add: mapM_empty asUser_return) apply wp apply simp - apply (simp add: mapM_Cons asUser_bind_distrib asUser_return) + apply (simp add: mapM_Cons asUser_bind_distrib asUser_return empty_fail_cond) apply wp apply simp apply (rule hoare_strengthen_post) diff --git a/proof/crefine/RISCV64/Finalise_C.thy b/proof/crefine/RISCV64/Finalise_C.thy index 8e5e17251..e19d5ae15 100644 --- a/proof/crefine/RISCV64/Finalise_C.thy +++ b/proof/crefine/RISCV64/Finalise_C.thy @@ -1185,7 +1185,7 @@ lemma setObject_ccorres_lemma: apply (subgoal_tac "fst (setObject ptr val \) = {}") apply simp apply (erule notE, erule_tac s=\ in empty_failD[rotated]) - apply (simp add: setObject_def split_def) + apply (simp add: setObject_def split_def empty_fail_cond) apply (rule ccontr) apply (clarsimp elim!: nonemptyE) apply (frule use_valid [OF _ obj_at_setObject3[where P=\]], simp_all)[1] diff --git a/proof/crefine/RISCV64/IpcCancel_C.thy b/proof/crefine/RISCV64/IpcCancel_C.thy index 4e5d904bd..f1b88a60a 100644 --- a/proof/crefine/RISCV64/IpcCancel_C.thy +++ b/proof/crefine/RISCV64/IpcCancel_C.thy @@ -2353,6 +2353,7 @@ lemma scheduleTCB_ccorres': rescheduleRequired od) (Call scheduleTCB_'proc)" + supply empty_fail_cond[simp] apply (cinit' lift: tptr_') apply (rule ccorres_rhs_assoc2)+ apply (rule_tac xf'="ret__int_'" in ccorres_split_nothrow_novcg) @@ -2407,7 +2408,8 @@ lemma scheduleTCB_ccorres_valid_queues'_pre: when (\ runnable \ curThread = thread \ action = ResumeCurrentThread) rescheduleRequired od) (Call scheduleTCB_'proc)" - apply (cinit' lift: tptr_' simp del: word_neq_0_conv) + supply empty_fail_cond[simp] + apply (cinit' lift: tptr_') apply (rule ccorres_rhs_assoc2)+ apply (rule_tac xf'="ret__int_'" in ccorres_split_nothrow_novcg) defer @@ -2428,7 +2430,7 @@ lemma scheduleTCB_ccorres_valid_queues'_pre: \ weak_sch_act_wf (ksSchedulerAction s) s" and P'=UNIV in ccorres_from_vcg) apply (rule allI, rule conseqPre, vcg) - apply (clarsimp simp: return_def if_1_0_0 split del: if_split) + apply (clarsimp simp: return_def) apply (clarsimp simp: from_bool_0 rf_sr_ksCurThread) apply (rule conjI) apply (clarsimp simp: st_tcb_at'_def) @@ -2499,6 +2501,7 @@ lemma scheduleTCB_ccorres_valid_queues'_pre_simple: when (\ runnable \ curThread = thread \ action = ResumeCurrentThread) rescheduleRequired od) (Call scheduleTCB_'proc)" + supply empty_fail_cond[simp] apply (cinit' lift: tptr_' simp del: word_neq_0_conv) apply (rule ccorres_rhs_assoc2)+ apply (rule_tac xf'="ret__int_'" in ccorres_split_nothrow_novcg) diff --git a/proof/crefine/RISCV64/Ipc_C.thy b/proof/crefine/RISCV64/Ipc_C.thy index 82f27762e..3606f864b 100644 --- a/proof/crefine/RISCV64/Ipc_C.thy +++ b/proof/crefine/RISCV64/Ipc_C.thy @@ -405,6 +405,7 @@ lemma handleArchFaultReply': msg \ getMRs s sb tag; handleArchFaultReply f r (msgLabel tag) msg od) x' = handleArchFaultReply' f s r tag x'" + supply empty_fail_cond[simp] apply (unfold handleArchFaultReply'_def getMRs_def msgMaxLength_def bit_def msgLengthBits_def msgRegisters_unfold fromIntegral_simp1 fromIntegral_simp2 @@ -549,6 +550,7 @@ lemma handleFaultReply': msg \ getMRs s sb tag; handleFaultReply f r (msgLabel tag) msg od) (handleFaultReply' f s r)" + supply empty_fail_cond[simp] apply (unfold handleFaultReply'_def getMRs_def msgMaxLength_def bit_def msgLengthBits_def msgRegisters_unfold fromIntegral_simp1 fromIntegral_simp2 @@ -1771,12 +1773,12 @@ proof - let ?obj_at_ft = "obj_at' (\tcb. tcbFault tcb = Some ft) sender" note symb_exec_r_fault = ccorres_symb_exec_r_known_rv_UNIV [where xf'=ret__unsigned_longlong_' and R="?obj_at_ft" and R'=UNIV] + note empty_fail_cond[simp] show ?thesis apply (unfold K_def) apply (intro ccorres_gen_asm) apply (cinit' lift: sender_' receiver_' receiveIPCBuffer_' simp: whileAnno_def) - apply (simp add: makeFaultMessage_def setMRs_to_setMR - del: Collect_const split del: if_split) + apply (simp add: makeFaultMessage_def setMRs_to_setMR) apply (rule_tac val="fault_to_fault_tag ft" in symb_exec_r_fault) apply (vcg, clarsimp) apply (drule(1) obj_at_cslift_tcb) @@ -1789,8 +1791,7 @@ proof - apply wpc apply (simp add: bind_assoc seL4_Fault_tag_defs ccorres_cond_iffs Collect_True Collect_False - zipWithM_mapM zip_append2 mapM_append - del: Collect_const split del: if_split) + zipWithM_mapM zip_append2 mapM_append) apply (rule ccorres_symb_exec_l) apply (rule ccorres_stateAssert) apply (rule_tac P="length msg = unat n_exceptionMessage" @@ -3144,6 +3145,7 @@ proof - let ?curr = "\s. current_extra_caps_' (globals s)" let ?EXCNONE = "{s. ret__unsigned_long_' s = scast EXCEPTION_NONE}" let ?interpret = "\v n. take n (array_to_list (excaprefs_C v))" + note empty_fail_cond[simp] show ?thesis apply (rule ccorres_gen_asm)+ apply (cinit(no_subst_asm) lift: thread_' bufferPtr_' info_' simp: whileAnno_def) @@ -3697,6 +3699,7 @@ lemma copyMRsFaultReply_ccorres_syscall: let ?obj_at_ft = "obj_at' (\tcb. tcbFault tcb = Some f) s" note symb_exec_r_fault = ccorres_symb_exec_r_known_rv_UNIV [where xf'=ret__unsigned_' and R="?obj_at_ft" and R'=UNIV] + note empty_fail_cond[simp] show ?thesis apply (unfold K_def, rule ccorres_gen_asm) using [[goals_limit=1]] apply (cinit' lift: sender_' receiver_' diff --git a/proof/crefine/RISCV64/IsolatedThreadAction.thy b/proof/crefine/RISCV64/IsolatedThreadAction.thy index f50005c7b..9e2c04e2d 100644 --- a/proof/crefine/RISCV64/IsolatedThreadAction.thy +++ b/proof/crefine/RISCV64/IsolatedThreadAction.thy @@ -400,7 +400,7 @@ lemma getObject_get_assert: apply (simp add: lookupAround2_known1 assert_opt_def obj_at'_def projectKO_def2 split: option.split) - apply (clarsimp simp: fail_def fst_return conj_comms project_inject + apply (clarsimp simp: fail_set fst_return conj_comms project_inject objBits_def) apply (simp only: assert2[symmetric], rule bind_apply_cong[OF refl]) @@ -816,7 +816,7 @@ lemma rescheduleRequired_simple_rewrite: (* FIXME move *) lemma empty_fail_isRunnable[intro!, wp, simp]: "empty_fail (isRunnable t)" - by (simp add: isRunnable_def isStopped_def) + by (simp add: isRunnable_def isStopped_def empty_fail_cond) lemma setupCallerCap_rewrite: "monadic_rewrite True True (\s. reply_masters_rvk_fb (ctes_of s)) diff --git a/proof/crefine/RISCV64/Retype_C.thy b/proof/crefine/RISCV64/Retype_C.thy index 41734578d..a9b7f5431 100644 --- a/proof/crefine/RISCV64/Retype_C.thy +++ b/proof/crefine/RISCV64/Retype_C.thy @@ -2275,8 +2275,8 @@ lemma getCTE_pre_cte_at: lemmas ccorres_getCTE_cte_at = ccorres_guard_from_wp [OF getCTE_pre_cte_at empty_fail_getCTE] ccorres_guard_from_wp_bind [OF getCTE_pre_cte_at empty_fail_getCTE] -lemmas ccorres_guard_from_wp_liftM = ccorres_guard_from_wp [OF liftM_pre iffD2 [OF empty_fail_liftM]] -lemmas ccorres_guard_from_wp_bind_liftM = ccorres_guard_from_wp_bind [OF liftM_pre iffD2 [OF empty_fail_liftM]] +lemmas ccorres_guard_from_wp_liftM = ccorres_guard_from_wp [OF liftM_pre empty_fail_liftM] +lemmas ccorres_guard_from_wp_bind_liftM = ccorres_guard_from_wp_bind [OF liftM_pre empty_fail_liftM] lemmas ccorres_liftM_getCTE_cte_at = ccorres_guard_from_wp_liftM [OF getCTE_pre_cte_at empty_fail_getCTE] ccorres_guard_from_wp_bind_liftM [OF getCTE_pre_cte_at empty_fail_getCTE] @@ -6439,7 +6439,8 @@ lemma createObject_caps_overlap_reserved_ret': apply clarsimp apply (rule hoare_strengthen_post[OF createNewCaps_caps_overlap_reserved_ret'[where sz = "APIType_capBits ty us"]]) apply assumption - apply (case_tac r,simp) + apply (rename_tac rv s) + apply (case_tac rv,simp) apply clarsimp apply (erule caps_overlap_reserved'_subseteq) apply (rule untypedRange_in_capRange) @@ -6512,7 +6513,8 @@ lemma createObject_IRQHandler: apply clarsimp apply (rule hoare_strengthen_post[OF createNewCaps_IRQHandler[where irq = x and P = "\_ _. False"]]) apply assumption - apply (case_tac r,clarsimp+) + apply (rename_tac rv s) + apply (case_tac rv; clarsimp) apply (clarsimp simp:word_bits_conv) done @@ -6529,7 +6531,8 @@ lemma createObject_capClass[wp]: apply clarsimp apply (rule hoare_strengthen_post[OF createNewCaps_range_helper]) apply assumption - apply (case_tac r,clarsimp+) + apply (rename_tac rv s) + apply (case_tac rv; clarsimp) apply (clarsimp simp:word_bits_conv ) apply (rule range_cover_full) apply (simp add:word_bits_conv)+ diff --git a/proof/crefine/RISCV64/SyscallArgs_C.thy b/proof/crefine/RISCV64/SyscallArgs_C.thy index 6f919d09e..f29bf7aa6 100644 --- a/proof/crefine/RISCV64/SyscallArgs_C.thy +++ b/proof/crefine/RISCV64/SyscallArgs_C.thy @@ -1135,7 +1135,7 @@ lemma getSyscallArg_ccorres_foo: apply (clarsimp simp: index_msgRegisters_less' ucast_up_less_bounded_iff_less_ucast_down') apply wp[1] apply (wp getMRs_tcbContext) - apply simp + apply fastforce apply (rule ccorres_seq_skip [THEN iffD2]) apply (rule ccorres_add_return2) apply (rule ccorres_symb_exec_l) @@ -1159,7 +1159,7 @@ lemma getSyscallArg_ccorres_foo: in hoare_pre(1)) apply (wp getMRs_user_word) apply (clarsimp simp: msgMaxLength_def unat_less_helper) - apply simp + apply fastforce apply (clarsimp simp: sysargs_rel_def sysargs_rel_n_def) apply (rule conjI, clarsimp simp: unat_of_nat64 word_bits_def) apply (drule equalityD2) diff --git a/proof/crefine/RISCV64/Tcb_C.thy b/proof/crefine/RISCV64/Tcb_C.thy index efd21d933..3663ff9f5 100644 --- a/proof/crefine/RISCV64/Tcb_C.thy +++ b/proof/crefine/RISCV64/Tcb_C.thy @@ -1563,6 +1563,7 @@ lemma invokeTCB_WriteRegisters_ccorres[where S=UNIV]: \ {s. buffer_' s = option_to_ptr buffer}) [] (invokeTCB (WriteRegisters dst resume values arch)) (Call invokeTCB_WriteRegisters_'proc)" + supply empty_fail_cond[simp] apply (rule ccorres_gen_asm) apply (erule conjE) apply (cinit lift: n_' dest___ptr_to_struct_tcb_C_' resumeTarget_' buffer_' @@ -1811,6 +1812,7 @@ shows (doE reply \ invokeTCB (ReadRegisters target susp n archCp); liftE (replyOnRestart thread reply isCall) odE) (Call invokeTCB_ReadRegisters_'proc)" + supply empty_fail_cond[simp] apply (rule ccorres_gen_asm) apply (cinit' lift: tcb_src_' suspendSource_' n_' call_' simp: invokeTCB_def liftE_bindE bind_assoc) @@ -3642,11 +3644,10 @@ lemma decodeSetSchedParams_ccorres: apply (simp only: cap_get_tag_isCap[symmetric], drule(1) cap_get_tag_to_H) apply (clarsimp simp: valid_cap'_def capAligned_def interpret_excaps_eq excaps_map_def) apply (intro conjI impI allI) - apply (clarsimp simp: unat_eq_0 le_max_word_ucast_id - thread_control_update_mcp_def thread_control_update_priority_def - cap_get_tag_isCap_unfolded_H_cap isCap_simps - interpret_excaps_eq excaps_map_def)+ - done + by (clarsimp simp: unat_eq_0 le_max_word_ucast_id + thread_control_update_mcp_def thread_control_update_priority_def + cap_get_tag_isCap_unfolded_H_cap isCap_simps + interpret_excaps_eq excaps_map_def)+ lemma decodeSetIPCBuffer_ccorres: "interpret_excaps extraCaps' = excaps_map extraCaps \ diff --git a/proof/crefine/X64/ArchMove_C.thy b/proof/crefine/X64/ArchMove_C.thy index 779a31a10..26bc611b5 100644 --- a/proof/crefine/X64/ArchMove_C.thy +++ b/proof/crefine/X64/ArchMove_C.thy @@ -16,7 +16,7 @@ lemma ps_clear_is_aligned_ksPSpace_None: \ ksPSpace s (p + d) = None" apply (simp add: ps_clear_def add_diff_eq[symmetric] mask_2pm1[symmetric]) apply (drule equals0D[where a="p + d"]) - apply (simp add: dom_def word_gt_0 del: word_neq_0_conv) + apply (simp add: dom_def word_gt_0) apply (drule mp) apply (rule word_plus_mono_right) apply simp @@ -47,8 +47,6 @@ where "port_mask start end = mask (unat (end && mask wordRadix)) && ~~ mask (unat (start && mask wordRadix))" -declare word_neq_0_conv [simp del] - lemma unat_ucast_prio_L1_cmask_simp: "unat (ucast (p::priority) && 0x3F :: machine_word) = unat (p && 0x3F)" using unat_ucast_prio_mask_simp[where m=6] @@ -183,13 +181,8 @@ lemma vmsz_aligned_aligned_pageBits: lemma empty_fail_findVSpaceForASID[iff]: "empty_fail (findVSpaceForASID asid)" - apply (simp add: findVSpaceForASID_def liftME_def) - apply (intro empty_fail_bindE, simp_all split: option.split) - apply (simp add: assertE_def split: if_split) - apply (simp add: assertE_def split: if_split) - apply (simp add: empty_fail_getObject) - apply (simp add: assertE_def liftE_bindE checkPML4At_def split: if_split) - done + unfolding findVSpaceForASID_def checkPML4At_def + by (wpsimp wp: empty_fail_getObject) crunch inv'[wp]: archThreadGet P @@ -209,7 +202,7 @@ lemma atg_sp': (* FIXME: MOVE to EmptyFail *) lemma empty_fail_archThreadGet [intro!, wp, simp]: "empty_fail (archThreadGet f p)" - by (simp add: archThreadGet_def getObject_def split_def) + by (fastforce simp: archThreadGet_def getObject_def split_def) lemma more_pageBits_inner_beauty: fixes x :: "9 word" @@ -354,7 +347,7 @@ lemma asUser_get_registers: apply (simp add: mapM_empty asUser_return) apply wp apply simp - apply (simp add: mapM_Cons asUser_bind_distrib asUser_return) + apply (simp add: mapM_Cons asUser_bind_distrib asUser_return empty_fail_cond) apply wp apply simp apply (rule hoare_strengthen_post) @@ -374,7 +367,7 @@ lemma asUser_get_registers: (* FIXME: move to where is_aligned_ptrFromPAddr is *) lemma is_aligned_ptrFromPAddr_pageBitsForSize: "is_aligned p (pageBitsForSize sz) \ is_aligned (ptrFromPAddr p) (pageBitsForSize sz)" - by (cases sz ; simp add: is_aligned_ptrFromPAddr_n pageBits_def bit_simps) + by (cases sz ; simp add: is_aligned_ptrFromPAddr_n bit_simps) lemma is_aligned_pageBitsForSize_minimum: "\ is_aligned p (pageBitsForSize sz) ; n \ pageBits \ \ is_aligned p n" @@ -405,10 +398,6 @@ lemma valid_eq_wf_asid_pool'[simp]: declare valid_asid_pool'.simps[simp del] (*<<<*) -(* FIXME: change the original to be predicated! *) -crunch ko_at'2[wp]: doMachineOp "\s. P (ko_at' p t s)" - (simp: crunch_simps) - (* FIXME: change the original to be predicated! *) crunch pred_tcb_at'2[wp]: doMachineOp "\s. P (pred_tcb_at' a b p s)" (simp: crunch_simps) @@ -473,7 +462,7 @@ lemma length_msgRegisters[simplified size_msgRegisters_def]: lemma empty_fail_loadWordUser[intro!, simp]: "empty_fail (loadWordUser x)" - by (simp add: loadWordUser_def ef_loadWord ef_dmo') + by (fastforce simp: loadWordUser_def ef_loadWord ef_dmo') lemma empty_fail_getMRs[iff]: "empty_fail (getMRs t buf mi)" @@ -483,26 +472,14 @@ lemma empty_fail_getReceiveSlots: "empty_fail (getReceiveSlots r rbuf)" proof - note - empty_fail_assertE[iff] - empty_fail_resolveAddressBits[iff] + empty_fail_resolveAddressBits[wp] + empty_fail_rethrowFailure[wp] + empty_fail_rethrowFailure[wp] show ?thesis - apply (clarsimp simp: getReceiveSlots_def loadCapTransfer_def split_def - split: option.split) - apply (rule empty_fail_bind) - apply (simp add: capTransferFromWords_def) - apply (simp add: emptyOnFailure_def unifyFailure_def) - apply (intro empty_fail_catch empty_fail_bindE empty_fail_rethrowFailure, - simp_all add: empty_fail_whenEs) - apply (simp_all add: lookupCap_def split_def lookupCapAndSlot_def - lookupSlotForThread_def liftME_def - getThreadCSpaceRoot_def locateSlot_conv bindE_assoc - lookupSlotForCNodeOp_def lookupErrorOnFailure_def - cong: if_cong) - apply (intro empty_fail_bindE, - simp_all add: getSlotCap_def) - apply (intro empty_fail_If empty_fail_bindE empty_fail_rethrowFailure impI, - simp_all add: empty_fail_whenEs rangeCheck_def) - done + unfolding getReceiveSlots_def loadCapTransfer_def lookupCap_def lookupCapAndSlot_def + by (wpsimp simp: emptyOnFailure_def unifyFailure_def lookupSlotForThread_def + capTransferFromWords_def getThreadCSpaceRoot_def locateSlot_conv bindE_assoc + lookupSlotForCNodeOp_def lookupErrorOnFailure_def rangeCheck_def) qed lemma user_getreg_rv: diff --git a/proof/crefine/X64/CLevityCatch.thy b/proof/crefine/X64/CLevityCatch.thy index 878c3126e..419c1adc9 100644 --- a/proof/crefine/X64/CLevityCatch.thy +++ b/proof/crefine/X64/CLevityCatch.thy @@ -55,12 +55,12 @@ lemma empty_fail_getExtraCPtrs [intro!, simp]: "empty_fail (getExtraCPtrs sendBuffer info)" apply (simp add: getExtraCPtrs_def) apply (cases info, simp) - apply (cases sendBuffer, simp_all) + apply (cases sendBuffer; fastforce) done lemma empty_fail_loadCapTransfer [intro!, simp]: "empty_fail (loadCapTransfer a)" - by (simp add: loadCapTransfer_def capTransferFromWords_def) + by (fastforce simp: loadCapTransfer_def capTransferFromWords_def) lemma empty_fail_emptyOnFailure [intro!, simp]: "empty_fail m \ empty_fail (emptyOnFailure m)" diff --git a/proof/crefine/X64/Finalise_C.thy b/proof/crefine/X64/Finalise_C.thy index f858a4f40..d62777b4c 100644 --- a/proof/crefine/X64/Finalise_C.thy +++ b/proof/crefine/X64/Finalise_C.thy @@ -1319,7 +1319,7 @@ lemma setObject_ccorres_lemma: apply (subgoal_tac "fst (setObject ptr val \) = {}") apply simp apply (erule notE, erule_tac s=\ in empty_failD[rotated]) - apply (simp add: setObject_def split_def) + apply (simp add: setObject_def split_def empty_fail_cond) apply (rule ccontr) apply (clarsimp elim!: nonemptyE) apply (frule use_valid [OF _ obj_at_setObject3[where P=\]], simp_all)[1] diff --git a/proof/crefine/X64/IpcCancel_C.thy b/proof/crefine/X64/IpcCancel_C.thy index a32787fcf..9d55bf402 100644 --- a/proof/crefine/X64/IpcCancel_C.thy +++ b/proof/crefine/X64/IpcCancel_C.thy @@ -2407,7 +2407,8 @@ lemma scheduleTCB_ccorres': rescheduleRequired od) (Call scheduleTCB_'proc)" - apply (cinit' lift: tptr_' simp del: word_neq_0_conv) + supply empty_fail_cond[simp] + apply (cinit' lift: tptr_') apply (rule ccorres_rhs_assoc2)+ apply (rule_tac xf'="ret__int_'" in ccorres_split_nothrow_novcg) defer @@ -2428,7 +2429,7 @@ lemma scheduleTCB_ccorres': \ (\t. ksSchedulerAction s = SwitchToThread t \ tcb_at' t s)" and P'=UNIV in ccorres_from_vcg) apply (rule allI, rule conseqPre, vcg) - apply (clarsimp simp: return_def if_1_0_0 split del: if_split) + apply (clarsimp simp: return_def) apply (clarsimp simp: from_bool_0 rf_sr_ksCurThread) apply (rule conjI) apply (clarsimp simp: st_tcb_at'_def) @@ -2461,7 +2462,8 @@ lemma scheduleTCB_ccorres_valid_queues'_pre: when (\ runnable \ curThread = thread \ action = ResumeCurrentThread) rescheduleRequired od) (Call scheduleTCB_'proc)" - apply (cinit' lift: tptr_' simp del: word_neq_0_conv) + supply empty_fail_cond[simp] + apply (cinit' lift: tptr_') apply (rule ccorres_rhs_assoc2)+ apply (rule_tac xf'="ret__int_'" in ccorres_split_nothrow_novcg) defer @@ -2553,6 +2555,7 @@ lemma scheduleTCB_ccorres_valid_queues'_pre_simple: when (\ runnable \ curThread = thread \ action = ResumeCurrentThread) rescheduleRequired od) (Call scheduleTCB_'proc)" + supply empty_fail_cond[simp] apply (cinit' lift: tptr_' simp del: word_neq_0_conv) apply (rule ccorres_rhs_assoc2)+ apply (rule_tac xf'="ret__int_'" in ccorres_split_nothrow_novcg) diff --git a/proof/crefine/X64/Ipc_C.thy b/proof/crefine/X64/Ipc_C.thy index c9eb39011..8206d66ed 100644 --- a/proof/crefine/X64/Ipc_C.thy +++ b/proof/crefine/X64/Ipc_C.thy @@ -408,6 +408,7 @@ lemma handleArchFaultReply': msg \ getMRs s sb tag; handleArchFaultReply f r (msgLabel tag) msg od) x' = handleArchFaultReply' f s r tag x'" + supply empty_fail_cond[simp] apply (unfold handleArchFaultReply'_def getMRs_def msgMaxLength_def bit_def msgLengthBits_def msgRegisters_unfold fromIntegral_simp1 fromIntegral_simp2 @@ -552,7 +553,7 @@ lemma handleFaultReply': msg \ getMRs s sb tag; handleFaultReply f r (msgLabel tag) msg od) (handleFaultReply' f s r)" - supply if_cong[cong] + supply if_cong[cong] empty_fail_cond[simp] supply empty_fail_asUser[wp] empty_fail_getRegister[wp] apply (unfold handleFaultReply'_def getMRs_def msgMaxLength_def bit_def msgLengthBits_def msgRegisters_unfold @@ -1780,6 +1781,7 @@ proof - let ?obj_at_ft = "obj_at' (\tcb. tcbFault tcb = Some ft) sender" note symb_exec_r_fault = ccorres_symb_exec_r_known_rv_UNIV [where xf'=ret__unsigned_longlong_' and R="?obj_at_ft" and R'=UNIV] + note empty_fail_cond[simp] show ?thesis apply (unfold K_def) apply (intro ccorres_gen_asm) @@ -3153,6 +3155,7 @@ proof - let ?curr = "\s. current_extra_caps_' (globals s)" let ?EXCNONE = "{s. ret__unsigned_long_' s = scast EXCEPTION_NONE}" let ?interpret = "\v n. take n (array_to_list (excaprefs_C v))" + note empty_fail_cond[simp] show ?thesis apply (rule ccorres_gen_asm)+ apply (cinit(no_subst_asm) lift: thread_' bufferPtr_' info_' simp: whileAnno_def) @@ -3707,6 +3710,7 @@ lemma copyMRsFaultReply_ccorres_syscall: let ?obj_at_ft = "obj_at' (\tcb. tcbFault tcb = Some f) s" note symb_exec_r_fault = ccorres_symb_exec_r_known_rv_UNIV [where xf'=ret__unsigned_' and R="?obj_at_ft" and R'=UNIV] + note empty_fail_cond[simp] show ?thesis apply (unfold K_def, rule ccorres_gen_asm) using [[goals_limit=1]] apply (cinit' lift: sender_' receiver_' diff --git a/proof/crefine/X64/IsolatedThreadAction.thy b/proof/crefine/X64/IsolatedThreadAction.thy index c2419ea7c..62ce61e6b 100644 --- a/proof/crefine/X64/IsolatedThreadAction.thy +++ b/proof/crefine/X64/IsolatedThreadAction.thy @@ -401,7 +401,7 @@ lemma getObject_get_assert: apply (simp add: lookupAround2_known1 assert_opt_def obj_at'_def projectKO_def2 split: option.split) - apply (clarsimp simp: fail_def fst_return conj_comms project_inject + apply (clarsimp simp: fail_set fst_return conj_comms project_inject objBits_def) apply (simp only: assert2[symmetric], rule bind_apply_cong[OF refl]) @@ -823,7 +823,7 @@ lemma rescheduleRequired_simple_rewrite: (* FIXME move *) lemma empty_fail_isRunnable[intro!, wp, simp]: "empty_fail (isRunnable t)" - by (simp add: isRunnable_def isStopped_def) + by (simp add: isRunnable_def isStopped_def empty_fail_cond) lemma setupCallerCap_rewrite: "monadic_rewrite True True (\s. reply_masters_rvk_fb (ctes_of s)) diff --git a/proof/crefine/X64/Retype_C.thy b/proof/crefine/X64/Retype_C.thy index 145e7c21c..0dbee4ade 100644 --- a/proof/crefine/X64/Retype_C.thy +++ b/proof/crefine/X64/Retype_C.thy @@ -2821,8 +2821,8 @@ lemma getCTE_pre_cte_at: lemmas ccorres_getCTE_cte_at = ccorres_guard_from_wp [OF getCTE_pre_cte_at empty_fail_getCTE] ccorres_guard_from_wp_bind [OF getCTE_pre_cte_at empty_fail_getCTE] -lemmas ccorres_guard_from_wp_liftM = ccorres_guard_from_wp [OF liftM_pre iffD2 [OF empty_fail_liftM]] -lemmas ccorres_guard_from_wp_bind_liftM = ccorres_guard_from_wp_bind [OF liftM_pre iffD2 [OF empty_fail_liftM]] +lemmas ccorres_guard_from_wp_liftM = ccorres_guard_from_wp [OF liftM_pre empty_fail_liftM] +lemmas ccorres_guard_from_wp_bind_liftM = ccorres_guard_from_wp_bind [OF liftM_pre empty_fail_liftM] lemmas ccorres_liftM_getCTE_cte_at = ccorres_guard_from_wp_liftM [OF getCTE_pre_cte_at empty_fail_getCTE] ccorres_guard_from_wp_bind_liftM [OF getCTE_pre_cte_at empty_fail_getCTE] @@ -7553,7 +7553,8 @@ lemma createObject_caps_overlap_reserved_ret': apply clarsimp apply (rule hoare_strengthen_post[OF createNewCaps_caps_overlap_reserved_ret'[where sz = "APIType_capBits ty us"]]) apply assumption - apply (case_tac r,simp) + apply (rename_tac rv s) + apply (case_tac rv,simp) apply clarsimp apply (erule caps_overlap_reserved'_subseteq) apply (rule untypedRange_in_capRange) @@ -7626,7 +7627,8 @@ lemma createObject_IRQHandler: apply clarsimp apply (rule hoare_strengthen_post[OF createNewCaps_IRQHandler[where irq = x and P = "\_ _. False"]]) apply assumption - apply (case_tac r,clarsimp+) + apply (rename_tac rv s) + apply (case_tac rv; clarsimp) apply (clarsimp simp:word_bits_conv) done @@ -7643,7 +7645,8 @@ lemma createObject_capClass[wp]: apply clarsimp apply (rule hoare_strengthen_post[OF createNewCaps_range_helper]) apply assumption - apply (case_tac r,clarsimp+) + apply (rename_tac rv s) + apply (case_tac rv; clarsimp) apply (clarsimp simp:word_bits_conv ) apply (rule range_cover_full) apply (simp add:word_bits_conv)+ diff --git a/proof/crefine/X64/SyscallArgs_C.thy b/proof/crefine/X64/SyscallArgs_C.thy index b2323eeb5..1c398a16e 100644 --- a/proof/crefine/X64/SyscallArgs_C.thy +++ b/proof/crefine/X64/SyscallArgs_C.thy @@ -1141,7 +1141,7 @@ lemma getSyscallArg_ccorres_foo: apply (simp add: index_msgRegisters_less unat_less_helper) apply wp[1] apply (wp getMRs_tcbContext) - apply simp + apply fastforce apply (rule ccorres_seq_skip [THEN iffD2]) apply (rule ccorres_add_return2) apply (rule ccorres_symb_exec_l) @@ -1165,7 +1165,7 @@ lemma getSyscallArg_ccorres_foo: in hoare_pre(1)) apply (wp getMRs_user_word) apply (clarsimp simp: msgMaxLength_def unat_less_helper) - apply simp + apply fastforce apply (clarsimp simp: sysargs_rel_def sysargs_rel_n_def) apply (rule conjI, clarsimp simp: unat_of_nat64 word_bits_def) apply (drule equalityD2) diff --git a/proof/crefine/X64/Tcb_C.thy b/proof/crefine/X64/Tcb_C.thy index 417f4c3f9..6e85b3763 100644 --- a/proof/crefine/X64/Tcb_C.thy +++ b/proof/crefine/X64/Tcb_C.thy @@ -1557,6 +1557,7 @@ lemma invokeTCB_WriteRegisters_ccorres[where S=UNIV]: \ {s. buffer_' s = option_to_ptr buffer}) [] (invokeTCB (WriteRegisters dst resume values arch)) (Call invokeTCB_WriteRegisters_'proc)" + supply empty_fail_cond[simp] apply (rule ccorres_gen_asm) apply (erule conjE) apply (cinit lift: n_' dest___ptr_to_struct_tcb_C_' resumeTarget_' buffer_' @@ -1805,6 +1806,7 @@ shows (doE reply \ invokeTCB (ReadRegisters target susp n archCp); liftE (replyOnRestart thread reply isCall) odE) (Call invokeTCB_ReadRegisters_'proc)" + supply empty_fail_cond[simp] apply (rule ccorres_gen_asm) apply (cinit' lift: tcb_src_' suspendSource_' n_' call_' simp: invokeTCB_def liftE_bindE bind_assoc) @@ -3635,11 +3637,10 @@ lemma decodeSetSchedParams_ccorres: apply (simp only: cap_get_tag_isCap[symmetric], drule(1) cap_get_tag_to_H) apply (clarsimp simp: valid_cap'_def capAligned_def interpret_excaps_eq excaps_map_def) apply (intro conjI impI allI) - apply (clarsimp simp: unat_eq_0 le_max_word_ucast_id - thread_control_update_mcp_def thread_control_update_priority_def - cap_get_tag_isCap_unfolded_H_cap isCap_simps - interpret_excaps_eq excaps_map_def)+ - done + by (clarsimp simp: unat_eq_0 le_max_word_ucast_id + thread_control_update_mcp_def thread_control_update_priority_def + cap_get_tag_isCap_unfolded_H_cap isCap_simps + interpret_excaps_eq excaps_map_def)+ lemma decodeSetIPCBuffer_ccorres: "interpret_excaps extraCaps' = excaps_map extraCaps \ diff --git a/proof/drefine/Arch_DR.thy b/proof/drefine/Arch_DR.thy index 3972822eb..85ddf58a1 100644 --- a/proof/drefine/Arch_DR.thy +++ b/proof/drefine/Arch_DR.thy @@ -783,7 +783,8 @@ next apply (rule corres_from_rdonly, simp_all)[1] apply (wp+ | simp)+ apply (rule hoare_strengthen_post, rule hoare_post_taut) - apply (case_tac r, auto simp add: in_monad)[1] + apply (rename_tac rv s) + apply (case_tac rv, auto simp add: in_monad)[1] apply (simp add: corres_whenE_throwError_split_rhs corres_alternate2 check_vp_alignment_def unlessE_whenE) apply (clarsimp simp add: liftE_bindE[symmetric]) @@ -822,7 +823,8 @@ next apply (rule corres_from_rdonly, simp_all)[1] apply (wp+ | simp)+ apply (rule hoare_strengthen_post, rule hoare_post_taut) - apply (case_tac r, auto simp add: in_monad)[1] + apply (rename_tac rv s) + apply (case_tac rv, auto simp add: in_monad)[1] apply (simp add: corres_whenE_throwError_split_rhs corres_alternate2 check_vp_alignment_def unlessE_whenE) apply (clarsimp simp add: liftE_bindE[symmetric]) @@ -935,7 +937,8 @@ next apply (rule corres_from_rdonly, simp_all)[1] apply (wp | simp)+ apply (rule hoare_strengthen_post, rule hoare_post_taut) - apply (case_tac r, auto simp add: in_monad)[1] + apply (rename_tac rv s) + apply (case_tac rv, auto simp add: in_monad)[1] apply (simp add: corres_whenE_throwError_split_rhs corres_alternate2 check_vp_alignment_def unlessE_whenE) apply clarsimp diff --git a/proof/drefine/CNode_DR.thy b/proof/drefine/CNode_DR.thy index 11905758b..0845255a6 100644 --- a/proof/drefine/CNode_DR.thy +++ b/proof/drefine/CNode_DR.thy @@ -792,9 +792,10 @@ lemma cap_revoke_corres_helper: in corres_split_forwards') apply (rule corres_guard_imp[OF corres_trivial[OF preemption_corres]]) apply simp+ - apply (rule alternative_wp) - apply (simp add:valid_def throwError_def return_def) - apply (simp add:valid_def returnOk_def return_def) + apply (wp alternative_wp) + apply (simp add:valid_def throwError_def return_def) + apply (simp add:valid_def returnOk_def return_def) + apply fastforce apply (clarsimp simp: valid_def) apply clarsimp apply (case_tac rva) @@ -1346,7 +1347,7 @@ next show ?case apply (clarsimp simp:mapM_Cons) apply (subst do_machine_op_bind) - apply (clarsimp simp:ef_storeWord)+ + apply (clarsimp simp:ef_storeWord empty_fail_cond)+ apply (subst corrupt_frame_duplicate[symmetric]) apply (rule corres_guard_imp) apply (rule corres_split) diff --git a/proof/drefine/Intent_DR.thy b/proof/drefine/Intent_DR.thy index 40ffab6ea..55ef038c6 100644 --- a/proof/drefine/Intent_DR.thy +++ b/proof/drefine/Intent_DR.thy @@ -551,7 +551,7 @@ lemma mapM_load_word_offs_do_machine_op: "mapM (load_word_offs ptr) list = do_machine_op (mapM loadWord (map (\offs. ptr + of_nat (offs * word_size)) list))" apply (subst submonad_mapM[OF submonad_do_machine_op submonad_do_machine_op]) - apply (simp add: loadWord_def) + apply (simp add: loadWord_def empty_fail_cond) apply (simp add: load_word_offs_def[abs_def] mapM_map_simp o_def) done diff --git a/proof/drefine/Ipc_DR.thy b/proof/drefine/Ipc_DR.thy index 3da5739a7..e9fed4fa5 100644 --- a/proof/drefine/Ipc_DR.thy +++ b/proof/drefine/Ipc_DR.thy @@ -1345,7 +1345,8 @@ next \ valid_mdb s \ QM s cap'))" for QM in hoare_post_imp_R) prefer 2 - apply (subgoal_tac "r\ cap.NullCap \ cte_wp_at ((\) cap.NullCap) (slot_ptr, slot_idx) s") + apply (rename_tac rv s) + apply (subgoal_tac "rv \ cap.NullCap \ cte_wp_at ((\) cap.NullCap) (slot_ptr, slot_idx) s") apply (intro impI) apply simp apply (elim conjE) diff --git a/proof/drefine/KHeap_DR.thy b/proof/drefine/KHeap_DR.thy index 7ce4474d9..408ea4188 100644 --- a/proof/drefine/KHeap_DR.thy +++ b/proof/drefine/KHeap_DR.thy @@ -2776,15 +2776,16 @@ lemma get_tcb_reply_cap_wp_original_cap: apply (rule hoare_post_imp [where Q="\r. cte_wp_at (\c. r \ cap.NullCap) (sid,tcb_cnode_index 2) and valid_mdb and tcb_at sid and valid_objs and cte_wp_at ((=) r) (sid,tcb_cnode_index 2)"]) + apply (rename_tac rv s) apply clarsimp - apply (subgoal_tac "is_master_reply_cap r \ obj_ref_of r = sid") + apply (subgoal_tac "is_master_reply_cap rv \ obj_ref_of rv = sid") apply clarsimp apply (frule cte_wp_tcb_cap_valid) apply simp+ apply (clarsimp simp:valid_mdb_def reply_master_revocable_def) - apply (drule_tac x = "obj_ref_of r" in spec) + apply (drule_tac x = "obj_ref_of rv" in spec) apply (drule_tac x = "tcb_cnode_index 2" in spec) - apply (drule_tac x = r in spec) + apply (drule_tac x = rv in spec) apply (drule iffD1[OF cte_wp_at_caps_of_state])+ apply clarsimp apply (frule cte_wp_tcb_cap_valid) diff --git a/proof/drefine/Untyped_DR.thy b/proof/drefine/Untyped_DR.thy index cca827f65..b9e65d608 100644 --- a/proof/drefine/Untyped_DR.thy +++ b/proof/drefine/Untyped_DR.thy @@ -65,12 +65,16 @@ next apply (rule someI2_ex, fastforce+)+ done + (* FIXME: For some reason In_Monad.in_fail doesn't fire below. This version would probably + have been better in the first place. *) + have [simp]: "\s. fst (fail s) = {}" by (simp add: fail_def) + have loadWord_const: "\a s. \x\fst (loadWord a s). snd x = s" apply (case_tac "is_aligned a 2") apply (simp add: loadWord_def is_aligned_mask exec_gets) apply (simp add: return_def) - apply (simp add: loadWord_def exec_gets fail_def is_aligned_mask) + apply (simp add: loadWord_def exec_gets is_aligned_mask) done have loadWord_atMostOneResult: @@ -78,7 +82,7 @@ next apply (case_tac "is_aligned a 2") apply (simp add: loadWord_def is_aligned_mask exec_gets) apply (simp add: return_def) - apply (simp add: loadWord_def exec_gets fail_def is_aligned_mask) + apply (simp add: loadWord_def exec_gets is_aligned_mask) done have mapM_loadWord_atMostOneResult[rule_format]: @@ -648,6 +652,7 @@ lemma clearMemory_unused_corres_noop: (return ()) (do_machine_op (clearMemory p (2 ^ (obj_bits_api ty us))))" (is "\ ?def; ?szv; ?in \ \ dcorres dc \ ?P ?f ?g") + supply empty_fail_cond[simp] apply (drule page_objects_default_object[where us=us and dev = dev], clarsimp) apply (rename_tac pgsz) apply (simp add: clearMemory_def do_machine_op_bind cleanCacheRange_PoC_def diff --git a/proof/infoflow/ARM/ArchArch_IF.thy b/proof/infoflow/ARM/ArchArch_IF.thy index 5b282cc84..92215d8e0 100644 --- a/proof/infoflow/ARM/ArchArch_IF.thy +++ b/proof/infoflow/ARM/ArchArch_IF.thy @@ -399,8 +399,9 @@ lemma find_pd_for_asid_assert_reads_respects: apply (wpsimp wp: get_pde_rev find_pd_for_asid_reads_respects hoare_vcg_all_lift) apply (rule_tac Q'="\rv s. is_subject aag (lookup_pd_slot rv 0 && ~~ mask pd_bits)" in hoare_post_imp_R) - apply (rule find_pd_for_asid_pd_slot_authorised) - apply (subgoal_tac "lookup_pd_slot r 0 = r") + apply (rule find_pd_for_asid_pd_slot_authorised) + apply (rename_tac rv s) + apply (subgoal_tac "lookup_pd_slot rv 0 = rv") apply fastforce apply (simp add: lookup_pd_slot_def) apply fastforce @@ -410,7 +411,7 @@ lemma modify_arm_hwasid_table_reads_respects: "reads_respects aag l \ (modify (\s. s\arch_state := arch_state s\arm_hwasid_table := param\\))" apply (simp add: equiv_valid_def2) apply (rule modify_ev2) - (* FIXME: slow 5s *) + (* slow 5s *) by (auto simp: reads_equiv_def affects_equiv_def states_equiv_for_def equiv_for_def intro: equiv_asids_triv' split: if_splits) @@ -419,7 +420,7 @@ lemma modify_arm_asid_map_reads_respects: "reads_respects aag l \ (modify (\s. s\arch_state := arch_state s\arm_asid_map := param\\))" apply (simp add: equiv_valid_def2) apply (rule modify_ev2) - (* FIXME: slow 5s *) + (* slow 5s *) by (auto simp: reads_equiv_def affects_equiv_def states_equiv_for_def equiv_for_def intro: equiv_asids_triv' split: if_splits) @@ -427,7 +428,7 @@ lemma modify_arm_next_asid_reads_respects: "reads_respects aag l \ (modify (\s. s\arch_state := arch_state s\arm_next_asid := param\\))" apply (simp add: equiv_valid_def2) apply (rule modify_ev2) - (* FIXME: slow 5s *) + (* slow 5s *) by (auto simp: reads_equiv_def affects_equiv_def states_equiv_for_def equiv_for_def intro: equiv_asids_triv' split: if_splits) @@ -1277,6 +1278,7 @@ lemma do_flush_globals_equiv: apply (cases "typ") by (wp dmo_cacheRangeOp_lift | simp add: do_flush_def cache_machine_op_defs do_flush_defs do_machine_op_bind when_def + empty_fail_cond | clarsimp | rule conjI)+ lemma perform_page_directory_invocation_globals_equiv: diff --git a/proof/infoflow/ARM/ArchIRQMasks_IF.thy b/proof/infoflow/ARM/ArchIRQMasks_IF.thy index d63a5b739..d532b9031 100644 --- a/proof/infoflow/ARM/ArchIRQMasks_IF.thy +++ b/proof/infoflow/ARM/ArchIRQMasks_IF.thy @@ -24,9 +24,6 @@ lemma delete_objects_irq_masks[IRQMasks_IF_assms, wp]: apply (wp dmo_wp no_irq_mapM_x no_irq | simp add: freeMemory_def no_irq_storeWord)+ done -crunch irq_masks[wp]: cleanCacheRange_PoU "\s. P (irq_masks s)" - (ignore_del: cleanCacheRange_PoU) - crunch irq_masks[IRQMasks_IF_assms, wp]: invoke_untyped "\s. P (irq_masks_of_state s)" (ignore: delete_objects wp: crunch_wps dmo_wp wp: mapME_x_inv_wp preemption_point_inv @@ -135,7 +132,7 @@ lemma invoke_tcb_irq_masks[IRQMasks_IF_assms]: apply (rule hoare_post_impErr[OF cap_delete_irq_masks[where P=P]]) apply blast apply blast - apply (wpsimp wp: hoare_vcg_all_lift_R hoare_vcg_const_imp_lift_R + apply (wpsimp wp: hoare_vcg_all_lift_R hoare_vcg_const_imp_lift_R hoare_vcg_all_lift hoare_drop_imps checked_cap_insert_domain_sep_inv)+ apply (rule_tac Q="\ r s. domain_sep_inv False st s \ P (irq_masks_of_state s)" and E="\_ s. P (irq_masks_of_state s)" in hoare_post_impErr) diff --git a/proof/infoflow/CNode_IF.thy b/proof/infoflow/CNode_IF.thy index e73c9fbd4..606e60c13 100644 --- a/proof/infoflow/CNode_IF.thy +++ b/proof/infoflow/CNode_IF.thy @@ -576,7 +576,7 @@ lemma preemption_point_def2: odE" apply (rule ext) apply (simp add: preemption_point_def OR_choiceE_def wrap_ext_bool_det_ext_ext_def - ef_mk_ef work_units_limit_reached_def select_f_def) + ef_mk_ef work_units_limit_reached_def select_f_def empty_fail_cond) apply (clarsimp simp: work_units_limit_reached_def gets_def liftE_def select_f_def get_def lift_def return_def bind_def bindE_def split_def image_def split: option.splits sum.splits) diff --git a/proof/infoflow/Finalise_IF.thy b/proof/infoflow/Finalise_IF.thy index 4ebce3968..1b39733a6 100644 --- a/proof/infoflow/Finalise_IF.thy +++ b/proof/infoflow/Finalise_IF.thy @@ -583,7 +583,7 @@ lemma tcb_sched_action_reads_respects: apply (simp | wp)+ apply (clarsimp simp: equiv_valid_2_def gets_apply_def get_def bind_def return_def labels_are_invisible_def) - apply wp+ + apply wpsimp+ apply (force intro: domtcbs simp: get_etcb_def pas_refined_def tcb_domain_map_wellformed_aux_def) done diff --git a/proof/infoflow/Noninterference.thy b/proof/infoflow/Noninterference.thy index 4c43bad10..b4435fc1a 100644 --- a/proof/infoflow/Noninterference.thy +++ b/proof/infoflow/Noninterference.thy @@ -2103,8 +2103,7 @@ lemma tcb_sched_action_reads_respects_g': apply (rule doesnt_touch_globalsI | simp | wp)+ apply (clarsimp simp: equiv_valid_2_def gets_apply_def get_def bind_def return_def labels_are_invisible_def) - apply wp+ - apply clarsimp + apply wpsimp+ apply (clarsimp simp: pas_refined_def tcb_domain_map_wellformed_aux_def) apply (erule_tac x="(thread, tcb_domain y)" in ballE) apply force diff --git a/proof/infoflow/RISCV64/ArchIRQMasks_IF.thy b/proof/infoflow/RISCV64/ArchIRQMasks_IF.thy index f192b8de6..6e3ae7cd4 100644 --- a/proof/infoflow/RISCV64/ArchIRQMasks_IF.thy +++ b/proof/infoflow/RISCV64/ArchIRQMasks_IF.thy @@ -128,7 +128,7 @@ lemma invoke_tcb_irq_masks[IRQMasks_IF_assms]: apply (rule hoare_post_impErr[OF cap_delete_irq_masks[where P=P]]) apply blast apply blast - apply (wpsimp wp: hoare_vcg_all_lift_R hoare_vcg_const_imp_lift_R + apply (wpsimp wp: hoare_vcg_all_lift_R hoare_vcg_const_imp_lift_R hoare_vcg_all_lift hoare_drop_imps checked_cap_insert_domain_sep_inv)+ apply (rule_tac Q="\ r s. domain_sep_inv False st s \ P (irq_masks_of_state s)" and E="\_ s. P (irq_masks_of_state s)" in hoare_post_impErr) diff --git a/proof/infoflow/Syscall_IF.thy b/proof/infoflow/Syscall_IF.thy index 1de1f707c..b162edd9a 100644 --- a/proof/infoflow/Syscall_IF.thy +++ b/proof/infoflow/Syscall_IF.thy @@ -446,14 +446,11 @@ lemma syscall_requiv_f_g: apply assumption+ apply (rule hoare_strengthen_post) apply assumption - apply (case_tac r) - apply simp - apply simp + apply (simp split: sum.splits) apply (rule hoare_strengthen_post, rule hoare_pre) apply assumption apply simp - apply (case_tac r) - apply simp+ + apply (simp split: sum.splits) done (*FIXME: Move to base*) diff --git a/proof/infoflow/Tcb_IF.thy b/proof/infoflow/Tcb_IF.thy index ca6872103..ad90ae59c 100644 --- a/proof/infoflow/Tcb_IF.thy +++ b/proof/infoflow/Tcb_IF.thy @@ -501,7 +501,8 @@ lemma invoke_tcb_reads_respects_f: | wpsimp wp: when_ev restart_reads_respects_f reschedule_required_reads_respects_f as_user_reads_respects_f restart_silc_inv restart_pas_refined hoare_vcg_if_lift)+ apply (rule hoare_strengthen_post[where Q="\_ s. \rv. R rv s" and R=R for R, rotated]) - apply (erule_tac x=r in allE, assumption) + apply (rename_tac rv s) + apply (erule_tac x=rv in allE, assumption) apply wpsimp+ apply (solves \auto intro!: det_zipWithM simp: det_setRegister det_getRestartPC det_setNextPC diff --git a/proof/invariant-abstract/AARCH64/ArchDetype_AI.thy b/proof/invariant-abstract/AARCH64/ArchDetype_AI.thy index 1db400bf2..570eeb085 100644 --- a/proof/invariant-abstract/AARCH64/ArchDetype_AI.thy +++ b/proof/invariant-abstract/AARCH64/ArchDetype_AI.thy @@ -83,7 +83,7 @@ next qed lemma empty_fail_freeMemory [Detype_AI_asms]: "empty_fail (freeMemory ptr bits)" - by (simp add: freeMemory_def mapM_x_mapM) + by (fastforce simp: freeMemory_def mapM_x_mapM) lemma region_in_kernel_window_detype[simp]: diff --git a/proof/invariant-abstract/AARCH64/ArchEmptyFail_AI.thy b/proof/invariant-abstract/AARCH64/ArchEmptyFail_AI.thy index 36ff7280a..a4ff0dfb1 100644 --- a/proof/invariant-abstract/AARCH64/ArchEmptyFail_AI.thy +++ b/proof/invariant-abstract/AARCH64/ArchEmptyFail_AI.thy @@ -34,7 +34,7 @@ context Arch begin global_naming AARCH64 crunch (empty_fail) empty_fail[wp, EmptyFail_AI_assms]: handle_fault (simp: kernel_object.splits option.splits arch_cap.splits cap.splits endpoint.splits bool.splits list.splits thread_state.splits split_def catch_def sum.splits - Let_def wp: zipWithM_x_empty_fail) + Let_def) crunch (empty_fail) empty_fail[wp]: decode_tcb_configure, decode_bind_notification, decode_unbind_notification, @@ -60,14 +60,13 @@ lemma arch_decode_ARMASIDControlMakePool_empty_fail: apply (simp add: decode_asid_control_invocation_def) apply (intro impI conjI allI) apply (simp add: split_def) - apply wp - apply simp + apply (wp (once), simp) apply (subst bindE_assoc[symmetric]) apply (rule empty_fail_bindE) - subgoal by (fastforce simp: empty_fail_def whenE_def throwError_def select_ext_def bindE_def - bind_def return_def returnOk_def lift_def liftE_def fail_def - gets_def get_def assert_def select_def - split: if_split_asm) + subgoal by (force simp: empty_fail_def whenE_def throwError_def select_ext_def bindE_def + bind_def return_def returnOk_def lift_def liftE_def fail_def + gets_def get_def assert_def select_def + split: if_split_asm) apply wpsimp apply (wpsimp simp: decode_frame_invocation_def decode_fr_inv_flush_def Let_def) apply (wpsimp simp: decode_vspace_invocation_def decode_vs_inv_flush_def @@ -93,9 +92,9 @@ lemma arch_decode_ARMASIDPoolAssign_empty_fail: apply (rule empty_fail_bindE, wpsimp) apply (subst bindE_assoc[symmetric]) apply (rule empty_fail_bindE) - subgoal by (fastforce simp: empty_fail_def whenE_def throwError_def select_def bindE_def - bind_def return_def returnOk_def lift_def liftE_def select_ext_def - gets_def get_def assert_def fail_def) + subgoal by (force simp: empty_fail_def whenE_def throwError_def select_def bindE_def + bind_def return_def returnOk_def lift_def liftE_def select_ext_def + gets_def get_def assert_def fail_def) apply wpsimp done diff --git a/proof/invariant-abstract/AARCH64/ArchTcb_AI.thy b/proof/invariant-abstract/AARCH64/ArchTcb_AI.thy index bc3bb5bdb..98b24a3ef 100644 --- a/proof/invariant-abstract/AARCH64/ArchTcb_AI.thy +++ b/proof/invariant-abstract/AARCH64/ArchTcb_AI.thy @@ -179,7 +179,6 @@ lemma cap_delete_no_cap_to_obj_asid[wp, Tcb_AI_asms]: apply (simp add: cap_delete_def no_cap_to_obj_with_diff_ref_ran_caps_form) apply wp - apply simp apply (rule use_spec) apply (rule rec_del_all_caps_in_range) apply (simp | rule obj_ref_none_no_asid)+ @@ -235,7 +234,7 @@ lemma tc_invs[Tcb_AI_asms]: apply (simp add: split_def set_mcpriority_def cong: option.case_cong) apply (rule hoare_vcg_precond_imp) apply wp - apply ((simp only: simp_thms + apply ((simp only: simp_thms cong: conj_cong | (simp add: conj_comms del: hoare_True_E_R, strengthen imp_consequent[where Q="x = None" for x], simp cong: conj_cong) | rule wp_split_const_if wp_split_const_if_R diff --git a/proof/invariant-abstract/AARCH64/ArchVSpace_AI.thy b/proof/invariant-abstract/AARCH64/ArchVSpace_AI.thy index 45760e3eb..edb27a74b 100644 --- a/proof/invariant-abstract/AARCH64/ArchVSpace_AI.thy +++ b/proof/invariant-abstract/AARCH64/ArchVSpace_AI.thy @@ -2864,7 +2864,7 @@ lemma vcpu_enable_invs[wp]: lemma vcpu_restore_invs[wp]: "vcpu_restore v \invs\" - apply (simp add: vcpu_restore_def do_machine_op_bind dom_mapM) + apply (simp add: vcpu_restore_def do_machine_op_bind dom_mapM empty_fail_cond) apply (wpsimp wp: mapM_wp_inv) done diff --git a/proof/invariant-abstract/AARCH64/Machine_AI.thy b/proof/invariant-abstract/AARCH64/Machine_AI.thy index ef27a6f9c..b34a001a7 100644 --- a/proof/invariant-abstract/AARCH64/Machine_AI.thy +++ b/proof/invariant-abstract/AARCH64/Machine_AI.thy @@ -89,7 +89,7 @@ text \Failure on empty result\ crunches loadWord, storeWord, machine_op_lift, clearMemory for (empty_fail) empty_fail[intro!, wp, simp] - (ignore: NonDetMonad.bind mapM_x simp: machine_op_lift_def) + (ignore: NonDetMonad.bind mapM_x simp: machine_op_lift_def empty_fail_cond) lemmas ef_machine_op_lift = machine_op_lift_empty_fail \ \required for generic interface\ diff --git a/proof/invariant-abstract/ARM/ArchDetype_AI.thy b/proof/invariant-abstract/ARM/ArchDetype_AI.thy index 58062ba37..7224372b9 100644 --- a/proof/invariant-abstract/ARM/ArchDetype_AI.thy +++ b/proof/invariant-abstract/ARM/ArchDetype_AI.thy @@ -89,7 +89,7 @@ next qed lemma empty_fail_freeMemory [Detype_AI_asms]: "empty_fail (freeMemory ptr bits)" - by (simp add: freeMemory_def mapM_x_mapM ef_storeWord) + by (fastforce simp: freeMemory_def mapM_x_mapM ef_storeWord) lemma region_in_kernel_window_detype[simp]: diff --git a/proof/invariant-abstract/ARM/ArchEmptyFail_AI.thy b/proof/invariant-abstract/ARM/ArchEmptyFail_AI.thy index c00e5b048..f33092611 100644 --- a/proof/invariant-abstract/ARM/ArchEmptyFail_AI.thy +++ b/proof/invariant-abstract/ARM/ArchEmptyFail_AI.thy @@ -37,7 +37,7 @@ context Arch begin global_naming ARM crunch (empty_fail) empty_fail[wp, EmptyFail_AI_assms]: handle_fault (simp: kernel_object.splits option.splits arch_cap.splits cap.splits endpoint.splits bool.splits list.splits thread_state.splits split_def catch_def sum.splits - Let_def wp: zipWithM_x_empty_fail) + Let_def) crunch (empty_fail) empty_fail[wp]: decode_tcb_configure, decode_bind_notification, decode_unbind_notification, @@ -61,11 +61,13 @@ lemma arch_decode_ARMASIDControlMakePool_empty_fail: apply (simp add: isPageFlushLabel_def isPDFlushLabel_def split: arch_cap.splits)+ apply (rule impI) apply (simp add: split_def) - apply wp - apply simp + apply (wp (once), simp) apply (subst bindE_assoc[symmetric]) apply (rule empty_fail_bindE) - subgoal by (fastforce simp: empty_fail_def whenE_def throwError_def select_ext_def bindE_def bind_def return_def returnOk_def lift_def liftE_def fail_def gets_def get_def assert_def select_def split: if_split_asm) + subgoal by (force simp: empty_fail_def whenE_def throwError_def select_ext_def bindE_def + bind_def return_def returnOk_def lift_def liftE_def fail_def gets_def + get_def assert_def select_def + split: if_split_asm) by (simp add: Let_def split: cap.splits arch_cap.splits option.splits bool.splits | wp | intro conjI impI allI)+ lemma arch_decode_ARMASIDPoolAssign_empty_fail: @@ -83,9 +85,9 @@ lemma arch_decode_ARMASIDPoolAssign_empty_fail: apply ((simp | wp)+)[1] apply (subst bindE_assoc[symmetric]) apply (rule empty_fail_bindE) - subgoal by (fastforce simp: empty_fail_def whenE_def throwError_def select_def bindE_def - bind_def return_def returnOk_def lift_def liftE_def select_ext_def - gets_def get_def assert_def fail_def) + subgoal by (force simp: empty_fail_def whenE_def throwError_def select_def bindE_def + bind_def return_def returnOk_def lift_def liftE_def select_ext_def + gets_def get_def assert_def fail_def) apply wp done diff --git a/proof/invariant-abstract/ARM/ArchTcb_AI.thy b/proof/invariant-abstract/ARM/ArchTcb_AI.thy index 77e2c0c6f..e1f7dcaf9 100644 --- a/proof/invariant-abstract/ARM/ArchTcb_AI.thy +++ b/proof/invariant-abstract/ARM/ArchTcb_AI.thy @@ -187,7 +187,6 @@ lemma cap_delete_no_cap_to_obj_asid[wp, Tcb_AI_asms]: apply (simp add: cap_delete_def no_cap_to_obj_with_diff_ref_ran_caps_form) apply wp - apply simp apply (rule use_spec) apply (rule rec_del_all_caps_in_range) apply (simp add: table_cap_ref_def[simplified, split_simps cap.split] @@ -238,8 +237,9 @@ lemma tc_invs[Tcb_AI_asms]: apply (simp add: split_def set_mcpriority_def cong: option.case_cong) apply (rule hoare_vcg_precond_imp) apply wp - (* takes long: *) - apply ((simp only: simp_thms + (* takes long: (30 sec) *) + apply ((simp only: simp_thms cong: conj_cong + | (strengthen invs_strengthen)+ | rule wp_split_const_if wp_split_const_if_R hoare_vcg_all_lift_R hoare_vcg_E_elim hoare_vcg_const_imp_lift_R diff --git a/proof/invariant-abstract/ARM/ArchVSpaceEntries_AI.thy b/proof/invariant-abstract/ARM/ArchVSpaceEntries_AI.thy index 77c06b148..559a0ce30 100644 --- a/proof/invariant-abstract/ARM/ArchVSpaceEntries_AI.thy +++ b/proof/invariant-abstract/ARM/ArchVSpaceEntries_AI.thy @@ -1074,8 +1074,6 @@ lemma perform_invocation_valid_pdpt[wp]: \\rv. valid_pdpt_objs\" apply (cases i, simp_all) apply (wp send_signal_interrupt_states | simp)+ - apply (clarsimp simp: invocation_duplicates_valid_def) - apply (wp | wpc | simp)+ apply (simp add: arch_perform_invocation_def) apply (rule hoare_pre) apply (wp | wpc | simp)+ diff --git a/proof/invariant-abstract/ARM/Machine_AI.thy b/proof/invariant-abstract/ARM/Machine_AI.thy index 947310012..ab23862c3 100644 --- a/proof/invariant-abstract/ARM/Machine_AI.thy +++ b/proof/invariant-abstract/ARM/Machine_AI.thy @@ -83,13 +83,13 @@ lemma det_getRestartPC: "det getRestartPC" lemma det_setNextPC: "det (setNextPC p)" by (simp add: setNextPC_def det_setRegister) - +(* FIXME empty_fail: make all empty_fail [intro!, wp], and non-conditional ones [simp] *) lemma ef_loadWord: "empty_fail (loadWord x)" - by (simp add: loadWord_def) + by (fastforce simp: loadWord_def) lemma ef_storeWord: "empty_fail (storeWord x y)" - by (simp add: storeWord_def) + by (fastforce simp: storeWord_def) lemma no_fail_getRestartPC: "no_fail \ getRestartPC" @@ -731,11 +731,12 @@ lemma empty_fail_cleanCacheRange_PoC[simp, intro!]: lemma empty_fail_cleanInvalidateCacheRange_RAM[simp, intro!]: "empty_fail (cleanInvalidateCacheRange_RAM s e p)" - by (simp add: cleanInvalidateCacheRange_RAM_def empty_fail_dsb empty_fail_cleanInvalidateL2Range empty_fail_cleanInvalByVA) + by (fastforce simp: cleanInvalidateCacheRange_RAM_def empty_fail_dsb + empty_fail_cleanInvalidateL2Range empty_fail_cleanInvalByVA) lemma empty_fail_cleanCacheRange_RAM[simp, intro!]: "empty_fail (cleanCacheRange_RAM s e p)" - by (simp add: cleanCacheRange_RAM_def empty_fail_dsb empty_fail_cleanL2Range) + by (fastforce simp: cleanCacheRange_RAM_def empty_fail_dsb empty_fail_cleanL2Range) lemma empty_fail_invalidateCacheRange_I[simp, intro!]: "empty_fail (invalidateCacheRange_I s e p)" @@ -743,8 +744,8 @@ lemma empty_fail_invalidateCacheRange_I[simp, intro!]: lemma empty_fail_invalidateCacheRange_RAM[simp, intro!]: "empty_fail (invalidateCacheRange_RAM s e p)" - by (simp add: invalidateCacheRange_RAM_def lineStart_def cacheLineBits_def - empty_fail_invalidateL2Range empty_fail_invalidateByVA empty_fail_dsb) + by (fastforce simp: invalidateCacheRange_RAM_def lineStart_def cacheLineBits_def + empty_fail_invalidateL2Range empty_fail_invalidateByVA empty_fail_dsb) lemma empty_fail_branchFlushRange[simp, intro!]: "empty_fail (branchFlushRange s e p)" @@ -752,16 +753,16 @@ lemma empty_fail_branchFlushRange[simp, intro!]: lemma empty_fail_cleanCaches_PoU[simp, intro!]: "empty_fail cleanCaches_PoU" - by (simp add: cleanCaches_PoU_def empty_fail_dsb empty_fail_clean_D_PoU empty_fail_invalidate_I_PoU) + by (fastforce simp: cleanCaches_PoU_def empty_fail_dsb empty_fail_clean_D_PoU empty_fail_invalidate_I_PoU) lemma empty_fail_cleanInvalidateL1Caches[simp, intro!]: "empty_fail cleanInvalidateL1Caches" - by (simp add: cleanInvalidateL1Caches_def empty_fail_dsb empty_fail_cleanInvalidate_D_PoC - empty_fail_invalidate_I_PoU) + by (fastforce simp: cleanInvalidateL1Caches_def empty_fail_dsb empty_fail_cleanInvalidate_D_PoC + empty_fail_invalidate_I_PoU) lemma empty_fail_clearMemory [simp, intro!]: "\a b. empty_fail (clearMemory a b)" - by (simp add: clearMemory_def mapM_x_mapM ef_storeWord) + by (fastforce simp: clearMemory_def mapM_x_mapM ef_storeWord) end diff --git a/proof/invariant-abstract/ARM_HYP/ArchArch_AI.thy b/proof/invariant-abstract/ARM_HYP/ArchArch_AI.thy index 922b53008..e94651cdc 100644 --- a/proof/invariant-abstract/ARM_HYP/ArchArch_AI.thy +++ b/proof/invariant-abstract/ARM_HYP/ArchArch_AI.thy @@ -1145,7 +1145,7 @@ lemma vcpu_enable_valid_machine_state[wp]: crunches vcpu_restore, vcpu_save for valid_machine_state[wp]: valid_machine_state - (wp: mapM_wp_inv simp: do_machine_op_bind dom_mapM ignore: do_machine_op) + (wp: mapM_wp_inv simp: do_machine_op_bind dom_mapM empty_fail_cond ignore: do_machine_op) crunches associate_vcpu_tcb for valid_machine_state[wp]: valid_machine_state diff --git a/proof/invariant-abstract/ARM_HYP/ArchDetype_AI.thy b/proof/invariant-abstract/ARM_HYP/ArchDetype_AI.thy index d3230cce0..e1bd9515b 100644 --- a/proof/invariant-abstract/ARM_HYP/ArchDetype_AI.thy +++ b/proof/invariant-abstract/ARM_HYP/ArchDetype_AI.thy @@ -93,7 +93,7 @@ next qed lemma empty_fail_freeMemory [Detype_AI_asms]: "empty_fail (freeMemory ptr bits)" - by (simp add: freeMemory_def mapM_x_mapM ef_storeWord) + by (fastforce simp: freeMemory_def mapM_x_mapM ef_storeWord) lemma region_in_kernel_window_detype[simp]: diff --git a/proof/invariant-abstract/ARM_HYP/ArchEmptyFail_AI.thy b/proof/invariant-abstract/ARM_HYP/ArchEmptyFail_AI.thy index cb3b1c871..512664ff7 100644 --- a/proof/invariant-abstract/ARM_HYP/ArchEmptyFail_AI.thy +++ b/proof/invariant-abstract/ARM_HYP/ArchEmptyFail_AI.thy @@ -37,7 +37,8 @@ context Arch begin global_naming ARM_HYP crunch (empty_fail) empty_fail[wp, EmptyFail_AI_assms]: handle_fault (simp: kernel_object.splits option.splits arch_cap.splits cap.splits endpoint.splits bool.splits list.splits thread_state.splits split_def catch_def sum.splits - Let_def wp: zipWithM_x_empty_fail empty_fail_addressTranslateS1) + Let_def + wp: empty_fail_addressTranslateS1) crunch (empty_fail) empty_fail[wp]: decode_tcb_configure, decode_bind_notification, decode_unbind_notification, @@ -65,11 +66,13 @@ lemma arch_decode_ARMASIDControlMakePool_empty_fail: prefer 2 apply (simp add: isPageFlushLabel_def isPDFlushLabel_def split: arch_cap.splits)+ apply (simp add: split_def) - apply wp - apply simp + apply (wp (once), simp) apply (subst bindE_assoc[symmetric]) apply (rule empty_fail_bindE) - subgoal by (fastforce simp: empty_fail_def whenE_def throwError_def select_ext_def bindE_def bind_def return_def returnOk_def lift_def liftE_def fail_def gets_def get_def assert_def select_def split: if_split_asm) + subgoal by (force simp: empty_fail_def whenE_def throwError_def select_ext_def bindE_def bind_def + return_def returnOk_def lift_def liftE_def fail_def gets_def get_def + assert_def select_def + split: if_split_asm) apply (simp add: Let_def split: cap.splits arch_cap.splits option.splits bool.splits | wp | intro conjI impI allI)+ done (* needs tidying up *) @@ -89,9 +92,9 @@ lemma arch_decode_ARMASIDPoolAssign_empty_fail: apply ((simp | wp)+)[1] apply (subst bindE_assoc[symmetric]) apply (rule empty_fail_bindE) - subgoal by (fastforce simp: empty_fail_def whenE_def throwError_def select_def bindE_def - bind_def return_def returnOk_def lift_def liftE_def select_ext_def - gets_def get_def assert_def fail_def) + subgoal by (force simp: empty_fail_def whenE_def throwError_def select_def bindE_def + bind_def return_def returnOk_def lift_def liftE_def select_ext_def + gets_def get_def assert_def fail_def) apply wp+ done diff --git a/proof/invariant-abstract/ARM_HYP/ArchSchedule_AI.thy b/proof/invariant-abstract/ARM_HYP/ArchSchedule_AI.thy index 89cdc626a..d8cc9e511 100644 --- a/proof/invariant-abstract/ARM_HYP/ArchSchedule_AI.thy +++ b/proof/invariant-abstract/ARM_HYP/ArchSchedule_AI.thy @@ -27,22 +27,6 @@ lemma dmo_mapM_storeWord_0_invs[wp,Schedule_AI_asms]: apply wp apply (clarsimp simp: word_bits_conv) done -(* -global_naming ARM_HYP (*FIXME: arch_split*) -lemma set_vm_root_kheap_arch_state[wp]: - "\\s. P (kheap s) (arm_globals_frame (arch_state s))\ set_vm_root a - \\_ s. P (kheap s) (arm_globals_frame (arch_state s))\" (is "valid ?P _ _") - apply (simp add: set_vm_root_def arm_context_switch_def) - apply (wp | wpcw | simp add: arm_context_switch_def get_hw_asid_def - store_hw_asid_def find_pd_for_asid_assert_def find_free_hw_asid_def - invalidate_hw_asid_entry_def invalidate_asid_def load_hw_asid_def)+ - apply (simp add: whenE_def, intro conjI impI) - apply (wp, simp add: returnOk_def validE_E_def validE_def)+ - apply (simp add: whenE_def, intro conjI[rotated] impI) - apply (wp | simp add: returnOk_def validE_E_def validE_def)+ - apply (wp | simp add: throwError_def validE_R_def validE_def)+ -done -*) crunch device_state_inv[wp]: clearExMonitor "\ms. P (device_state ms)" diff --git a/proof/invariant-abstract/ARM_HYP/ArchTcb_AI.thy b/proof/invariant-abstract/ARM_HYP/ArchTcb_AI.thy index 1a3f9dcd4..c5a940f2b 100644 --- a/proof/invariant-abstract/ARM_HYP/ArchTcb_AI.thy +++ b/proof/invariant-abstract/ARM_HYP/ArchTcb_AI.thy @@ -189,7 +189,6 @@ lemma cap_delete_no_cap_to_obj_asid[wp, Tcb_AI_asms]: apply (simp add: cap_delete_def no_cap_to_obj_with_diff_ref_ran_caps_form) apply wp - apply simp apply (rule use_spec) apply (rule rec_del_all_caps_in_range) apply (rule mp[OF _ obj_ref_none_no_asid(1)[of cap]], simp) @@ -240,8 +239,9 @@ lemma tc_invs[Tcb_AI_asms]: apply (simp add: split_def set_mcpriority_def cong: option.case_cong) apply (rule hoare_vcg_precond_imp) apply wp - (* takes long: *) - apply ((simp only: simp_thms + (* takes long: (30 sec) *) + apply ((simp only: simp_thms cong: conj_cong + | (strengthen invs_strengthen)+ | rule wp_split_const_if wp_split_const_if_R hoare_vcg_all_lift_R hoare_vcg_E_elim hoare_vcg_const_imp_lift_R diff --git a/proof/invariant-abstract/ARM_HYP/ArchVSpaceEntries_AI.thy b/proof/invariant-abstract/ARM_HYP/ArchVSpaceEntries_AI.thy index 0ba4baa59..d4896e194 100644 --- a/proof/invariant-abstract/ARM_HYP/ArchVSpaceEntries_AI.thy +++ b/proof/invariant-abstract/ARM_HYP/ArchVSpaceEntries_AI.thy @@ -1033,8 +1033,6 @@ lemma perform_invocation_valid_pdpt[wp]: \\rv. valid_pdpt_objs\" apply (cases i, simp_all) apply (wp send_signal_interrupt_states | simp)+ - apply (clarsimp simp: invocation_duplicates_valid_def) - apply (wp | wpc | simp)+ apply (simp add: arch_perform_invocation_def) apply (rule hoare_pre) apply (wp | wpc | simp)+ diff --git a/proof/invariant-abstract/ARM_HYP/ArchVSpace_AI.thy b/proof/invariant-abstract/ARM_HYP/ArchVSpace_AI.thy index 9a48452a6..38ecc5c29 100644 --- a/proof/invariant-abstract/ARM_HYP/ArchVSpace_AI.thy +++ b/proof/invariant-abstract/ARM_HYP/ArchVSpace_AI.thy @@ -2538,7 +2538,7 @@ lemma vcpu_enable_invs[wp]: lemma vcpu_restore_invs[wp]: "\\s. invs s\ vcpu_restore v \\_. invs\" - apply (simp add: vcpu_restore_def do_machine_op_bind dom_mapM) + apply (simp add: vcpu_restore_def do_machine_op_bind dom_mapM empty_fail_cond) apply (wpsimp wp: mapM_wp_inv) done @@ -2571,7 +2571,7 @@ lemma vcpu_save_invs[wp]: lemma vcpu_disable_invs[wp]: "\\ s. invs s\ vcpu_disable v \\_ s . invs s\" apply (simp add: vcpu_disable_def) - apply (wpsimp simp: do_machine_op_bind empty_fail_isb + apply (wpsimp simp: do_machine_op_bind empty_fail_isb empty_fail_cond wp: set_vcpu_invs_eq_hyp get_vcpu_wp maskInterrupt_invs | wp hoare_vcg_all_lift hoare_vcg_imp_lift')+ done diff --git a/proof/invariant-abstract/ARM_HYP/Machine_AI.thy b/proof/invariant-abstract/ARM_HYP/Machine_AI.thy index 6f4376ed7..13a1f6873 100644 --- a/proof/invariant-abstract/ARM_HYP/Machine_AI.thy +++ b/proof/invariant-abstract/ARM_HYP/Machine_AI.thy @@ -83,13 +83,13 @@ lemma det_getRestartPC: "det getRestartPC" lemma det_setNextPC: "det (setNextPC p)" by (simp add: setNextPC_def det_setRegister) - +(* FIXME empty_fail: make all empty_fail [intro!, wp], and non-conditional ones [simp] *) lemma ef_loadWord: "empty_fail (loadWord x)" - by (simp add: loadWord_def) + by (fastforce simp: loadWord_def) lemma ef_storeWord: "empty_fail (storeWord x y)" - by (simp add: storeWord_def) + by (fastforce simp: storeWord_def) lemma no_fail_getRestartPC: "no_fail \ getRestartPC" @@ -772,7 +772,7 @@ lemma empty_fail_setHCR[simp, intro!]: lemma empty_fail_addressTranslateS1[simp, intro!]: "empty_fail (addressTranslateS1 w)" - by (simp add: addressTranslateS1_def) + by (fastforce simp: addressTranslateS1_def) lemma empty_fail_writeContextIDAndPD[simp, intro!]: "empty_fail (writeContextIDAndPD asid w)" @@ -804,7 +804,7 @@ lemma empty_fail_set_gic_vcpu_ctrl_apr[simp, intro!]: lemma empty_fail_get_gic_vcpu_ctrl_lr[simp, intro!]: "empty_fail (get_gic_vcpu_ctrl_lr n)" - by (simp add: get_gic_vcpu_ctrl_lr_def) + by (fastforce simp: get_gic_vcpu_ctrl_lr_def) lemma empty_fail_set_gic_vcpu_ctrl_lr[simp, intro!]: "empty_fail (set_gic_vcpu_ctrl_lr n w)" @@ -846,11 +846,12 @@ lemma empty_fail_cleanCacheRange_PoC[simp, intro!]: lemma empty_fail_cleanInvalidateCacheRange_RAM[simp, intro!]: "empty_fail (cleanInvalidateCacheRange_RAM s e p)" - by (simp add: cleanInvalidateCacheRange_RAM_def empty_fail_dsb empty_fail_cleanInvalidateL2Range empty_fail_cleanInvalByVA) + by (fastforce simp: cleanInvalidateCacheRange_RAM_def empty_fail_dsb + empty_fail_cleanInvalidateL2Range empty_fail_cleanInvalByVA) lemma empty_fail_cleanCacheRange_RAM[simp, intro!]: "empty_fail (cleanCacheRange_RAM s e p)" - by (simp add: cleanCacheRange_RAM_def empty_fail_dsb empty_fail_cleanL2Range) + by (fastforce simp: cleanCacheRange_RAM_def empty_fail_dsb empty_fail_cleanL2Range) lemma empty_fail_invalidateCacheRange_I[simp, intro!]: "empty_fail (invalidateCacheRange_I s e p)" @@ -858,8 +859,8 @@ lemma empty_fail_invalidateCacheRange_I[simp, intro!]: lemma empty_fail_invalidateCacheRange_RAM[simp, intro!]: "empty_fail (invalidateCacheRange_RAM s e p)" - by (simp add: invalidateCacheRange_RAM_def lineStart_def cacheLineBits_def - empty_fail_invalidateL2Range empty_fail_invalidateByVA empty_fail_dsb) + by (fastforce simp: invalidateCacheRange_RAM_def lineStart_def cacheLineBits_def + empty_fail_invalidateL2Range empty_fail_invalidateByVA empty_fail_dsb) lemma empty_fail_branchFlushRange[simp, intro!]: "empty_fail (branchFlushRange s e p)" @@ -867,16 +868,16 @@ lemma empty_fail_branchFlushRange[simp, intro!]: lemma empty_fail_cleanCaches_PoU[simp, intro!]: "empty_fail cleanCaches_PoU" - by (simp add: cleanCaches_PoU_def empty_fail_dsb empty_fail_clean_D_PoU empty_fail_invalidate_I_PoU) + by (fastforce simp: cleanCaches_PoU_def empty_fail_dsb empty_fail_clean_D_PoU empty_fail_invalidate_I_PoU) lemma empty_fail_cleanInvalidateL1Caches[simp, intro!]: "empty_fail cleanInvalidateL1Caches" - by (simp add: cleanInvalidateL1Caches_def empty_fail_dsb empty_fail_cleanInvalidate_D_PoC - empty_fail_invalidate_I_PoU) + by (fastforce simp: cleanInvalidateL1Caches_def empty_fail_dsb empty_fail_cleanInvalidate_D_PoC + empty_fail_invalidate_I_PoU) lemma empty_fail_clearMemory [simp, intro!]: "\a b. empty_fail (clearMemory a b)" - by (simp add: clearMemory_def mapM_x_mapM ef_storeWord) + by (fastforce simp: clearMemory_def mapM_x_mapM ef_storeWord) end diff --git a/proof/invariant-abstract/CNodeInv_AI.thy b/proof/invariant-abstract/CNodeInv_AI.thy index 3b300d518..643f760cb 100644 --- a/proof/invariant-abstract/CNodeInv_AI.thy +++ b/proof/invariant-abstract/CNodeInv_AI.thy @@ -448,6 +448,7 @@ lemma decode_cnode_inv_wf[wp]: and cte_wp_at (\c. c = src_cap) src_slot and cte_wp_at ((=) cap.NullCap) x" in hoare_post_imp) + apply (rename_tac rv s) apply (clarsimp simp: cte_wp_at_caps_of_state all_rights_def) apply (simp add: cap_master_update_cap_data weak_derived_update_cap_data cap_asid_update_cap_data @@ -455,7 +456,7 @@ lemma decode_cnode_inv_wf[wp]: apply (strengthen cap_badge_update_cap_data) apply simp apply (frule (1) caps_of_state_valid_cap) - apply (case_tac "is_zombie r") + apply (case_tac "is_zombie rv") apply (clarsimp simp add: valid_cap_def2 update_cap_data_def is_cap_simps split: if_split_asm) diff --git a/proof/invariant-abstract/EmptyFail_AI.thy b/proof/invariant-abstract/EmptyFail_AI.thy index 681b0410e..28115a54f 100644 --- a/proof/invariant-abstract/EmptyFail_AI.thy +++ b/proof/invariant-abstract/EmptyFail_AI.thy @@ -45,7 +45,7 @@ lemma do_machine_op_empty_fail[wp]: "empty_fail f \ empty_fail (do_machine_op f)" apply (simp add: do_machine_op_def | wp)+ apply (simp add: empty_fail_def) - apply (simp add: split_def) + apply (simp add: split_def empty_fail_cond) done lemma throw_on_false_empty_fail[wp]: diff --git a/proof/invariant-abstract/Include_AI.thy b/proof/invariant-abstract/Include_AI.thy index 10cb2301f..ed57697d3 100644 --- a/proof/invariant-abstract/Include_AI.thy +++ b/proof/invariant-abstract/Include_AI.thy @@ -8,13 +8,14 @@ theory Include_AI imports Lib.Lib ArchCrunchSetup_AI - "Monads.Eisbach_WP" - "ASpec.Syscall_A" - "Lib.LemmaBucket" - "Lib.ListLibLemmas" - "Lib.LemmaBucket" - "Lib.SplitRule" - "Rights_AI" + Monads.Eisbach_WP + Monads.Strengthen_Setup + ASpec.Syscall_A + Lib.LemmaBucket + Lib.ListLibLemmas + Lib.LemmaBucket + Lib.SplitRule + Rights_AI begin no_notation bind_drop (infixl ">>" 60) diff --git a/proof/invariant-abstract/RISCV64/ArchDetype_AI.thy b/proof/invariant-abstract/RISCV64/ArchDetype_AI.thy index 5bb6fd74b..ff5c24d72 100644 --- a/proof/invariant-abstract/RISCV64/ArchDetype_AI.thy +++ b/proof/invariant-abstract/RISCV64/ArchDetype_AI.thy @@ -82,7 +82,7 @@ next qed lemma empty_fail_freeMemory [Detype_AI_asms]: "empty_fail (freeMemory ptr bits)" - by (simp add: freeMemory_def mapM_x_mapM ef_storeWord) + by (fastforce simp: freeMemory_def mapM_x_mapM ef_storeWord) lemma region_in_kernel_window_detype[simp]: diff --git a/proof/invariant-abstract/RISCV64/ArchEmptyFail_AI.thy b/proof/invariant-abstract/RISCV64/ArchEmptyFail_AI.thy index d07be6796..69d218d8d 100644 --- a/proof/invariant-abstract/RISCV64/ArchEmptyFail_AI.thy +++ b/proof/invariant-abstract/RISCV64/ArchEmptyFail_AI.thy @@ -32,7 +32,7 @@ context Arch begin global_naming RISCV64 crunch (empty_fail) empty_fail[wp, EmptyFail_AI_assms]: handle_fault (simp: kernel_object.splits option.splits arch_cap.splits cap.splits endpoint.splits bool.splits list.splits thread_state.splits split_def catch_def sum.splits - Let_def wp: zipWithM_x_empty_fail) + Let_def) crunch (empty_fail) empty_fail[wp]: decode_tcb_configure, decode_bind_notification, decode_unbind_notification, @@ -54,14 +54,13 @@ lemma arch_decode_RISCVASIDControlMakePool_empty_fail: apply (simp add: decode_asid_control_invocation_def) apply (intro impI conjI allI) apply (simp add: split_def) - apply wp - apply simp + apply (wp (once), simp) apply (subst bindE_assoc[symmetric]) apply (rule empty_fail_bindE) - subgoal by (fastforce simp: empty_fail_def whenE_def throwError_def select_ext_def bindE_def - bind_def return_def returnOk_def lift_def liftE_def fail_def - gets_def get_def assert_def select_def - split: if_split_asm) + subgoal by (force simp: empty_fail_def whenE_def throwError_def select_ext_def bindE_def + bind_def return_def returnOk_def lift_def liftE_def fail_def + gets_def get_def assert_def select_def + split: if_split_asm) apply wpsimp apply (wpsimp simp: decode_frame_invocation_def) apply (wpsimp simp: decode_page_table_invocation_def) @@ -84,9 +83,9 @@ lemma arch_decode_RISCVASIDPoolAssign_empty_fail: apply (rule empty_fail_bindE, wpsimp) apply (subst bindE_assoc[symmetric]) apply (rule empty_fail_bindE) - subgoal by (fastforce simp: empty_fail_def whenE_def throwError_def select_def bindE_def - bind_def return_def returnOk_def lift_def liftE_def select_ext_def - gets_def get_def assert_def fail_def) + subgoal by (force simp: empty_fail_def whenE_def throwError_def select_def bindE_def + bind_def return_def returnOk_def lift_def liftE_def select_ext_def + gets_def get_def assert_def fail_def) apply wpsimp done diff --git a/proof/invariant-abstract/RISCV64/ArchTcb_AI.thy b/proof/invariant-abstract/RISCV64/ArchTcb_AI.thy index f2f28a178..2256385a7 100644 --- a/proof/invariant-abstract/RISCV64/ArchTcb_AI.thy +++ b/proof/invariant-abstract/RISCV64/ArchTcb_AI.thy @@ -181,7 +181,6 @@ lemma cap_delete_no_cap_to_obj_asid[wp, Tcb_AI_asms]: apply (simp add: cap_delete_def no_cap_to_obj_with_diff_ref_ran_caps_form) apply wp - apply simp apply (rule use_spec) apply (rule rec_del_all_caps_in_range) apply (simp | rule obj_ref_none_no_asid)+ @@ -237,7 +236,7 @@ lemma tc_invs[Tcb_AI_asms]: apply (simp add: split_def set_mcpriority_def cong: option.case_cong) apply (rule hoare_vcg_precond_imp) apply wp - apply ((simp only: simp_thms + apply ((simp only: simp_thms cong: conj_cong | (simp add: conj_comms del: hoare_True_E_R, strengthen imp_consequent[where Q="x = None" for x], simp cong: conj_cong) | rule wp_split_const_if wp_split_const_if_R diff --git a/proof/invariant-abstract/RISCV64/ArchVSpaceEntries_AI.thy b/proof/invariant-abstract/RISCV64/ArchVSpaceEntries_AI.thy index 6d1fe116d..95ab70f3e 100644 --- a/proof/invariant-abstract/RISCV64/ArchVSpaceEntries_AI.thy +++ b/proof/invariant-abstract/RISCV64/ArchVSpaceEntries_AI.thy @@ -287,8 +287,6 @@ lemma perform_invocation_valid_vspace_objs'[wp]: \\rv. valid_vspace_objs'\" apply (cases i, simp_all) apply (wp send_signal_interrupt_states | simp)+ - apply (clarsimp simp:) - apply (wp | wpc | simp)+ apply (simp add: arch_perform_invocation_def) apply (wp | wpc | simp)+ apply (auto simp: valid_arch_inv_def intro: valid_objs_caps) diff --git a/proof/invariant-abstract/RISCV64/Machine_AI.thy b/proof/invariant-abstract/RISCV64/Machine_AI.thy index db1d26fcc..1aef2e7d5 100644 --- a/proof/invariant-abstract/RISCV64/Machine_AI.thy +++ b/proof/invariant-abstract/RISCV64/Machine_AI.thy @@ -83,13 +83,13 @@ lemma det_getRestartPC: "det getRestartPC" lemma det_setNextPC: "det (setNextPC p)" by (simp add: setNextPC_def det_setRegister) - +(* FIXME empty_fail: make all empty_fail [intro!, wp], and non-conditional ones [simp] *) lemma ef_loadWord: "empty_fail (loadWord x)" - by (simp add: loadWord_def) + by (fastforce simp: loadWord_def) lemma ef_storeWord: "empty_fail (storeWord x y)" - by (simp add: storeWord_def) + by (fastforce simp: storeWord_def) lemma no_fail_getRestartPC: "no_fail \ getRestartPC" @@ -356,7 +356,7 @@ lemma empty_fail_initL2Cache: "empty_fail initL2Cache" lemma empty_fail_clearMemory [simp, intro!]: "\a b. empty_fail (clearMemory a b)" - by (simp add: clearMemory_def mapM_x_mapM ef_storeWord) + by (fastforce simp: clearMemory_def mapM_x_mapM ef_storeWord) lemma no_irq_setVSpaceRoot: "no_irq (setVSpaceRoot r a)" diff --git a/proof/invariant-abstract/SubMonad_AI.thy b/proof/invariant-abstract/SubMonad_AI.thy index 13e23d3ad..99b09dcd5 100644 --- a/proof/invariant-abstract/SubMonad_AI.thy +++ b/proof/invariant-abstract/SubMonad_AI.thy @@ -42,7 +42,7 @@ lemma assert_get_thread_do_machine_op_comm: apply (rule submonad_comm2 [OF _ _ submonad_do_machine_op]) apply (rule submonad_args_pspace) apply (rule assert_get_tcb_pspace) - apply simp+ + apply (simp add: empty_fail_cond)+ done end diff --git a/proof/invariant-abstract/VSpaceEntries_AI.thy b/proof/invariant-abstract/VSpaceEntries_AI.thy index b3f5479d7..84036ab1e 100644 --- a/proof/invariant-abstract/VSpaceEntries_AI.thy +++ b/proof/invariant-abstract/VSpaceEntries_AI.thy @@ -148,7 +148,6 @@ lemma mapME_x_wp: shows "set xs \ S \ \P\ mapME_x f xs \\rv. P\, \E\" apply (subst mapME_x_mapME) apply wp - apply simp apply (rule mapME_wp) apply (rule x) apply assumption+ diff --git a/proof/invariant-abstract/X64/ArchDetype_AI.thy b/proof/invariant-abstract/X64/ArchDetype_AI.thy index 9eaf867fe..f1b28872b 100644 --- a/proof/invariant-abstract/X64/ArchDetype_AI.thy +++ b/proof/invariant-abstract/X64/ArchDetype_AI.thy @@ -82,7 +82,7 @@ next qed lemma empty_fail_freeMemory [Detype_AI_asms]: "empty_fail (freeMemory ptr bits)" - by (simp add: freeMemory_def mapM_x_mapM ef_storeWord) + by (fastforce simp: freeMemory_def mapM_x_mapM ef_storeWord) lemma region_in_kernel_window_detype[simp]: diff --git a/proof/invariant-abstract/X64/ArchEmptyFail_AI.thy b/proof/invariant-abstract/X64/ArchEmptyFail_AI.thy index c806a6fa4..dab6b318d 100644 --- a/proof/invariant-abstract/X64/ArchEmptyFail_AI.thy +++ b/proof/invariant-abstract/X64/ArchEmptyFail_AI.thy @@ -37,7 +37,7 @@ context Arch begin global_naming X64 crunch (empty_fail) empty_fail[wp, EmptyFail_AI_assms]: handle_fault (simp: kernel_object.splits option.splits arch_cap.splits cap.splits endpoint.splits bool.splits list.splits thread_state.splits split_def catch_def sum.splits - Let_def wp: zipWithM_x_empty_fail) + Let_def) lemma port_out_empty_fail[simp, intro!]: assumes ef: "\a. empty_fail (oper a)" @@ -80,12 +80,11 @@ lemma arch_decode_X64ASIDControlMakePool_empty_fail: apply (simp split: arch_cap.splits) apply (intro conjI impI) apply (simp add: split_def) - apply wp - apply simp + apply (wp (once), simp) apply (subst bindE_assoc[symmetric]) apply (rule empty_fail_bindE) - subgoal by (fastforce simp: empty_fail_def whenE_def throwError_def select_ext_def bindE_def bind_def return_def - returnOk_def lift_def liftE_def fail_def gets_def get_def assert_def select_def split: if_split_asm) + subgoal by (force simp: empty_fail_def whenE_def throwError_def select_ext_def bindE_def bind_def return_def + returnOk_def lift_def liftE_def fail_def gets_def get_def assert_def select_def split: if_split_asm) apply (simp add: Let_def split: cap.splits arch_cap.splits option.splits bool.splits | wp | intro conjI impI allI)+ by (clarsimp simp add: decode_page_invocation_def decode_page_table_invocation_def decode_page_directory_invocation_def decode_pdpt_invocation_def @@ -110,9 +109,9 @@ lemma arch_decode_X64ASIDPoolAssign_empty_fail: apply ((simp | wp)+)[1] apply (subst bindE_assoc[symmetric]) apply (rule empty_fail_bindE) - subgoal by (fastforce simp: empty_fail_def whenE_def throwError_def select_def bindE_def - bind_def return_def returnOk_def lift_def liftE_def select_ext_def - gets_def get_def assert_def fail_def) + subgoal by (force simp: empty_fail_def whenE_def throwError_def select_def bindE_def + bind_def return_def returnOk_def lift_def liftE_def select_ext_def + gets_def get_def assert_def fail_def) apply (clarsimp simp: decode_page_invocation_def decode_page_table_invocation_def decode_page_directory_invocation_def decode_pdpt_invocation_def | wp | intro conjI)+ done @@ -142,9 +141,7 @@ context Arch begin global_naming X64 lemma flush_table_empty_fail[simp, wp]: "empty_fail (flush_table a b c d)" unfolding flush_table_def - apply simp - apply (wp | wpc | simp)+ - done + by wpsimp crunch (empty_fail) empty_fail[wp, EmptyFail_AI_assms]: maskInterrupt, empty_slot, finalise_cap, preemption_point, @@ -152,7 +149,7 @@ crunch (empty_fail) empty_fail[wp, EmptyFail_AI_assms]: maskInterrupt, empty_slo (simp: Let_def catch_def split_def OR_choiceE_def mk_ef_def option.splits endpoint.splits notification.splits thread_state.splits sum.splits cap.splits arch_cap.splits kernel_object.splits vmpage_size.splits pde.splits bool.splits list.splits - forM_x_def empty_fail_mapM_x set_object_def + set_object_def ignore: nativeThreadUsingFPU_impl switchFpuOwner_impl) crunch (empty_fail) empty_fail[wp, EmptyFail_AI_assms]: setRegister, setNextPC diff --git a/proof/invariant-abstract/X64/ArchTcb_AI.thy b/proof/invariant-abstract/X64/ArchTcb_AI.thy index 089ef5585..9320999df 100644 --- a/proof/invariant-abstract/X64/ArchTcb_AI.thy +++ b/proof/invariant-abstract/X64/ArchTcb_AI.thy @@ -198,7 +198,6 @@ lemma cap_delete_no_cap_to_obj_asid[wp, Tcb_AI_asms]: apply (simp add: cap_delete_def no_cap_to_obj_with_diff_ref_ran_caps_form) apply wp - apply simp apply (rule use_spec) apply (rule rec_del_all_caps_in_range) apply (simp add: table_cap_ref_def[simplified, split_simps cap.split] @@ -233,7 +232,8 @@ lemma tc_invs[Tcb_AI_asms]: apply (simp add: split_def set_mcpriority_def cong: option.case_cong) apply (rule hoare_vcg_precond_imp) apply wp - apply ((simp only: simp_thms + apply ((simp only: simp_thms cong: conj_cong + | (strengthen invs_strengthen)+ | (simp add: conj_comms del: hoare_True_E_R, strengthen imp_consequent[where Q="x = None" for x], simp cong: conj_cong) | rule wp_split_const_if wp_split_const_if_R diff --git a/proof/invariant-abstract/X64/ArchVSpaceEntries_AI.thy b/proof/invariant-abstract/X64/ArchVSpaceEntries_AI.thy index 7f4ca6d4e..e71b9742e 100644 --- a/proof/invariant-abstract/X64/ArchVSpaceEntries_AI.thy +++ b/proof/invariant-abstract/X64/ArchVSpaceEntries_AI.thy @@ -681,8 +681,6 @@ lemma perform_invocation_valid_vspace_objs'[wp]: \\rv. valid_vspace_objs'\" apply (cases i, simp_all) apply (wp send_signal_interrupt_states | simp)+ - apply (clarsimp simp:) - apply (wp | wpc | simp)+ apply (simp add: arch_perform_invocation_def) apply (wp | wpc | simp)+ apply (auto simp: valid_arch_inv_def ) diff --git a/proof/invariant-abstract/X64/Machine_AI.thy b/proof/invariant-abstract/X64/Machine_AI.thy index e41fbe1cf..4e37700a4 100644 --- a/proof/invariant-abstract/X64/Machine_AI.thy +++ b/proof/invariant-abstract/X64/Machine_AI.thy @@ -83,13 +83,13 @@ lemma det_getRestartPC: "det getRestartPC" lemma det_setNextPC: "det (setNextPC p)" by (simp add: setNextPC_def det_setRegister) - +(* FIXME empty_fail: make all empty_fail [intro!, wp], and non-conditional ones [simp] *) lemma ef_loadWord: "empty_fail (loadWord x)" - by (simp add: loadWord_def) + by (fastforce simp: loadWord_def) lemma ef_storeWord: "empty_fail (storeWord x y)" - by (simp add: storeWord_def) + by (fastforce simp: storeWord_def) lemma no_fail_getRestartPC: "no_fail \ getRestartPC" @@ -407,7 +407,7 @@ lemma empty_fail_initL2Cache: "empty_fail initL2Cache" lemma empty_fail_clearMemory [simp, intro!]: "\a b. empty_fail (clearMemory a b)" - by (simp add: clearMemory_def mapM_x_mapM ef_storeWord) + by (fastforce simp: clearMemory_def mapM_x_mapM ef_storeWord) lemma getFaultAddress_ef[simp,wp]: "empty_fail getFaultAddress" by (simp add: getFaultAddress_def) @@ -428,19 +428,19 @@ lemma hwASIDInvalidate_ef[simp,wp]: "empty_fail (hwASIDInvalidate b a)" by (simp add: hwASIDInvalidate_def) lemma updateIRQState_ef[simp,wp]: "empty_fail (updateIRQState b c)" - by (simp add: updateIRQState_def) + by (fastforce simp: updateIRQState_def) lemma writeCR3_ef[simp,wp]: "empty_fail (writeCR3 a b)" by (simp add: writeCR3_def) lemma in8_ef[simp,wp]: "empty_fail (in8 port)" - by (simp add: in8_def) + by (fastforce simp: in8_def) lemma in16_ef[simp,wp]: "empty_fail (in16 port)" - by (simp add: in16_def) + by (fastforce simp: in16_def) lemma in32_ef[simp,wp]: "empty_fail (in32 port)" - by (simp add: in32_def) + by (fastforce simp: in32_def) lemma out8_ef[simp,wp]: "empty_fail (out8 port dat)" by (simp add: out8_def) diff --git a/proof/refine/ARM/Arch_R.thy b/proof/refine/ARM/Arch_R.thy index 601513967..4ee951cb6 100644 --- a/proof/refine/ARM/Arch_R.thy +++ b/proof/refine/ARM/Arch_R.thy @@ -1536,7 +1536,8 @@ lemma createMappingEntires_valid_slots_duplicated'[wp]: apply (rule_tac Q' = "\p s. is_aligned p 6 \ page_table_at' (p && ~~ mask ptBits) s" in hoare_post_imp_R) apply (wp lookupPTSlot_aligned lookupPTSlot_page_table_at') - apply (rule_tac x = r in exI) + apply (rename_tac rv s) + apply (rule_tac x = rv in exI) apply (clarsimp simp: largePagePTEOffsets_def pteBits_def) apply (frule is_aligned_no_wrap'[where off = "0x3c"]) apply simp diff --git a/proof/refine/ARM/CSpace_R.thy b/proof/refine/ARM/CSpace_R.thy index af50e55aa..ba40e62b1 100644 --- a/proof/refine/ARM/CSpace_R.thy +++ b/proof/refine/ARM/CSpace_R.thy @@ -3968,8 +3968,9 @@ lemma setupReplyMaster_corres: cte_wp_at' ((=) rv) (cte_map (t, tcb_cnode_index 2))" in hoare_strengthen_post) apply (wp hoare_drop_imps getCTE_wp') + apply (rename_tac rv s) apply (clarsimp simp: cte_wp_at_ctes_of valid_mdb'_def valid_mdb_ctes_def) - apply (case_tac r, fastforce elim: valid_nullcapsE) + apply (case_tac rv, fastforce elim: valid_nullcapsE) apply (fastforce elim: tcb_at_cte_at) apply (clarsimp simp: cte_at'_obj_at' tcb_cte_cases_def cte_map_def) apply (clarsimp simp: invs'_def valid_state'_def valid_pspace'_def) diff --git a/proof/refine/ARM/Detype_R.thy b/proof/refine/ARM/Detype_R.thy index b279e5c58..2e6481b76 100644 --- a/proof/refine/ARM/Detype_R.thy +++ b/proof/refine/ARM/Detype_R.thy @@ -2101,7 +2101,7 @@ qed lemma empty_fail_locateCTE: "empty_fail (locateCTE src)" - by (simp add:locateCTE_def bind_assoc split_def) + by (fastforce simp: locateCTE_def bind_assoc split_def) lemma fail_empty_locateCTE: "snd (locateCTE src s) \ fst (locateCTE src s) = {}" diff --git a/proof/refine/ARM/EmptyFail.thy b/proof/refine/ARM/EmptyFail.thy index d3b7d68de..741a9ba83 100644 --- a/proof/refine/ARM/EmptyFail.thy +++ b/proof/refine/ARM/EmptyFail.thy @@ -19,12 +19,12 @@ lemma empty_fail_projectKO [simp, intro!]: lemma empty_fail_alignCheck [intro!, wp, simp]: "empty_fail (alignCheck a b)" unfolding alignCheck_def - by (simp add: alignError_def) + by (fastforce simp: alignError_def) lemma empty_fail_magnitudeCheck [intro!, wp, simp]: "empty_fail (magnitudeCheck a b c)" unfolding magnitudeCheck_def - by (simp split: option.splits) + by (fastforce split: option.splits) lemma empty_fail_loadObject_default [intro!, wp, simp]: shows "empty_fail (loadObject_default x b c d)" @@ -33,7 +33,7 @@ lemma empty_fail_loadObject_default [intro!, wp, simp]: lemma empty_fail_threadGet [intro!, wp, simp]: "empty_fail (threadGet f p)" - by (simp add: threadGet_def getObject_def split_def) + by (fastforce simp: threadGet_def getObject_def split_def) lemma empty_fail_getCTE [intro!, wp, simp]: "empty_fail (getCTE slot)" @@ -47,12 +47,12 @@ lemma empty_fail_getCTE [intro!, wp, simp]: lemma empty_fail_updateObject_cte [intro!, wp, simp]: "empty_fail (updateObject (v :: cte) ko a b c)" - by (simp add: updateObject_cte typeError_def unless_def split: kernel_object.splits ) + by (fastforce simp: updateObject_cte typeError_def unless_def split: kernel_object.splits ) lemma empty_fail_setCTE [intro!, wp, simp]: "empty_fail (setCTE p cte)" unfolding setCTE_def - by (simp add: setObject_def split_def) + by (fastforce simp: setObject_def split_def) lemma empty_fail_updateMDB [intro!, wp, simp]: "empty_fail (updateMDB a b)" @@ -60,16 +60,15 @@ lemma empty_fail_updateMDB [intro!, wp, simp]: lemma empty_fail_getSlotCap [intro!, wp, simp]: "empty_fail (getSlotCap a)" - unfolding getSlotCap_def by simp + unfolding getSlotCap_def by fastforce context begin interpretation Arch . (*FIXME: arch_split*) lemma empty_fail_getObject: - assumes x: "(\b c d. empty_fail (loadObject x b c d::'a :: pspace_storable kernel))" + assumes "\b c d. empty_fail (loadObject x b c d::'a :: pspace_storable kernel)" shows "empty_fail (getObject x :: 'a :: pspace_storable kernel)" apply (simp add: getObject_def split_def) - apply (safe intro!: empty_fail_bind empty_fail_gets empty_fail_assert_opt) - apply (rule x) + apply (safe intro!: assms) done lemma empty_fail_getObject_tcb [intro!, wp, simp]: @@ -78,22 +77,22 @@ lemma empty_fail_getObject_tcb [intro!, wp, simp]: lemma empty_fail_updateTrackedFreeIndex [intro!, wp, simp]: shows "empty_fail (updateTrackedFreeIndex p idx)" - by (simp add: updateTrackedFreeIndex_def) + by (fastforce simp add: updateTrackedFreeIndex_def) lemma empty_fail_updateNewFreeIndex [intro!, wp, simp]: shows "empty_fail (updateNewFreeIndex p)" apply (simp add: updateNewFreeIndex_def) - apply (safe intro!: empty_fail_bind) + apply safe apply (simp split: capability.split) done lemma empty_fail_insertNewCap [intro!, wp, simp]: "empty_fail (insertNewCap p p' cap)" - unfolding insertNewCap_def by simp + unfolding insertNewCap_def by fastforce lemma empty_fail_getIRQSlot [intro!, wp, simp]: "empty_fail (getIRQSlot irq)" - by (simp add: getIRQSlot_def getInterruptState_def locateSlot_conv) + by (fastforce simp: getIRQSlot_def getInterruptState_def locateSlot_conv) lemma empty_fail_getObject_ntfn [intro!, wp, simp]: "empty_fail (getObject p :: Structures_H.notification kernel)" @@ -107,15 +106,15 @@ lemma empty_fail_lookupIPCBuffer [intro!, wp, simp]: "empty_fail (lookupIPCBuffer a b)" by (clarsimp simp: lookupIPCBuffer_def Let_def getThreadBufferSlot_def locateSlot_conv - split: capability.splits arch_capability.splits | wp | wpc)+ + split: capability.splits arch_capability.splits | wp | wpc | safe)+ lemma empty_fail_updateObject_default [intro!, wp, simp]: "empty_fail (updateObject_default v ko a b c)" - by (simp add: updateObject_default_def typeError_def unless_def split: kernel_object.splits ) + by (fastforce simp: updateObject_default_def typeError_def unless_def split: kernel_object.splits) lemma empty_fail_threadSet [intro!, wp, simp]: "empty_fail (threadSet f p)" - by (simp add: threadSet_def getObject_def setObject_def split_def) + by (fastforce simp: threadSet_def getObject_def setObject_def split_def) lemma empty_fail_getThreadState[iff]: "empty_fail (getThreadState t)" diff --git a/proof/refine/ARM/EmptyFail_H.thy b/proof/refine/ARM/EmptyFail_H.thy index 7ae323a3a..19a71ee07 100644 --- a/proof/refine/ARM/EmptyFail_H.thy +++ b/proof/refine/ARM/EmptyFail_H.thy @@ -17,19 +17,19 @@ context begin interpretation Arch . (*FIXME: arch_split*) lemmas forM_empty_fail[intro!, wp, simp] = empty_fail_mapM[simplified forM_def[symmetric]] lemmas forM_x_empty_fail[intro!, wp, simp] = empty_fail_mapM_x[simplified forM_x_def[symmetric]] -lemmas forME_x_empty_fail[intro!, wp, simp] = mapME_x_empty_fail[simplified forME_x_def[symmetric]] +lemmas forME_x_empty_fail[intro!, wp, simp] = empty_fail_mapME_x[simplified forME_x_def[symmetric]] lemma withoutPreemption_empty_fail[intro!, wp, simp]: "empty_fail m \ empty_fail (withoutPreemption m)" - by (simp add: withoutPreemption_def) + by simp lemma withoutFailure_empty_fail[intro!, wp, simp]: "empty_fail m \ empty_fail (withoutFailure m)" - by (simp add: withoutFailure_def) + by simp lemma catchFailure_empty_fail[intro!, wp, simp]: "\ empty_fail f; \x. empty_fail (g x) \ \ empty_fail (catchFailure f g)" - by (simp add: catchFailure_def empty_fail_catch) + by (simp add: empty_fail_catch) lemma emptyOnFailure_empty_fail[intro!, wp, simp]: "empty_fail m \ empty_fail (emptyOnFailure m)" @@ -86,9 +86,6 @@ proof (induct arbitrary: s rule: resolveAddressBits.induct) lemmas resolveAddressBits_empty_fail[intro!, wp, simp] = resolveAddressBits_spec_empty_fail[THEN use_spec_empty_fail] -crunch (empty_fail) empty_fail[intro!, wp, simp]: lookupIPCBuffer -(simp:Let_def) - declare ef_dmo'[intro!, wp, simp] lemma empty_fail_getObject_ep [intro!, wp, simp]: @@ -175,7 +172,7 @@ crunch (empty_fail) "_H_empty_fail"[intro!, wp, simp]: "ThreadDecls_H.suspend" lemma ThreadDecls_H_restart_empty_fail[intro!, wp, simp]: "empty_fail (ThreadDecls_H.restart target)" - by (simp add:restart_def) + by (fastforce simp: restart_def) crunch (empty_fail) empty_fail[intro!, wp, simp]: finaliseCap, preemptionPoint, capSwapForDelete (wp: empty_fail_catch simp: Let_def) @@ -213,18 +210,14 @@ lemmas finaliseSlot_empty_fail[intro!, wp, simp] = lemma checkCapAt_empty_fail[intro!, wp, simp]: "empty_fail action \ empty_fail (checkCapAt cap ptr action)" - by (simp add: checkCapAt_def) + by (fastforce simp: checkCapAt_def) lemma assertDerived_empty_fail[intro!, wp, simp]: "empty_fail f \ empty_fail (assertDerived src cap f)" - by (simp add: assertDerived_def) + by (fastforce simp: assertDerived_def) crunch (empty_fail) empty_fail[intro!, wp, simp]: cteDelete -lemma liftE_empty_fail[intro!, wp, simp]: - "empty_fail f \ empty_fail (liftE f)" - by simp - lemma spec_empty_fail_unlessE': "\ \ P \ spec_empty_fail f s \ \ spec_empty_fail (unlessE P f) s" by (simp add:unlessE_def spec_empty_returnOk) @@ -254,7 +247,7 @@ lemma Syscall_H_syscall_empty_fail[intro!, wp, simp]: lemma catchError_empty_fail[intro!, wp, simp]: "\ empty_fail f; \x. empty_fail (g x) \ \ empty_fail (catchError f g)" - by (simp add: catchError_def handle_empty_fail) + by fastforce crunch (empty_fail) empty_fail[intro!, wp, simp]: chooseThread, getDomainTime, nextDomain, isHighestPrio diff --git a/proof/refine/ARM/Finalise_R.thy b/proof/refine/ARM/Finalise_R.thy index 9b28b8da1..2c60fe565 100644 --- a/proof/refine/ARM/Finalise_R.thy +++ b/proof/refine/ARM/Finalise_R.thy @@ -2396,11 +2396,12 @@ lemma deleteASID_invs'[wp]: apply (simp add: deleteASID_def cong: option.case_cong) apply (rule hoare_pre) apply (wp | wpc)+ - apply (rule_tac Q="\rv. valid_obj' (injectKO rv) and invs'" - in hoare_post_imp) + apply (rule_tac Q="\rv. valid_obj' (injectKO rv) and invs'" + in hoare_post_imp) + apply (rename_tac rv s) apply (clarsimp split: if_split_asm del: subsetI) apply (simp add: fun_upd_def[symmetric] valid_obj'_def) - apply (case_tac r, simp) + apply (case_tac rv, simp) apply (subst inv_f_f, rule inj_onI, simp)+ apply (rule conjI) apply clarsimp diff --git a/proof/refine/ARM/Interrupt_R.thy b/proof/refine/ARM/Interrupt_R.thy index d6041bbc0..202bf7636 100644 --- a/proof/refine/ARM/Interrupt_R.thy +++ b/proof/refine/ARM/Interrupt_R.thy @@ -187,6 +187,7 @@ crunches arch_check_irq, checkIRQ lemma arch_check_irq_maxIRQ_valid: "\\\ arch_check_irq y \\_. (\s. unat y \ unat maxIRQ)\, -" unfolding arch_check_irq_def + supply hoare_vcg_prop[wp del] (* FIXME lib: check rule order *) apply (wpsimp simp: validE_R_def wp: whenE_throwError_wp) by (metis unat_ucast_10_32 word_le_nat_alt word_le_not_less) diff --git a/proof/refine/ARM/IpcCancel_R.thy b/proof/refine/ARM/IpcCancel_R.thy index 1c962b461..b031a5bb3 100644 --- a/proof/refine/ARM/IpcCancel_R.thy +++ b/proof/refine/ARM/IpcCancel_R.thy @@ -699,12 +699,13 @@ lemma cancelSignal_invs': apply assumption apply (rule hoare_strengthen_post) apply (rule get_ntfn_sp') + apply (rename_tac rv s) apply (clarsimp simp: pred_tcb_at') apply (frule NIQ) apply (clarsimp simp: pred_tcb_at'_def obj_at'_def) apply (rule conjI) apply (clarsimp simp: valid_ntfn'_def) - apply (case_tac "ntfnObj r", simp_all add: isWaitingNtfn_def) + apply (case_tac "ntfnObj rv", simp_all add: isWaitingNtfn_def) apply (frule ko_at_valid_objs') apply (simp add: valid_pspace_valid_objs') apply (clarsimp simp: projectKO_opt_ntfn split: kernel_object.splits) @@ -727,7 +728,7 @@ lemma cancelSignal_invs': split: ntfn.splits) apply (rule conjI, clarsimp elim!: if_live_state_refsE) apply (fastforce simp: sym_refs_def dest!: idle'_no_refs) - apply (case_tac "ntfnObj r", simp_all) + apply (case_tac "ntfnObj rv", simp_all) apply (frule obj_at_valid_objs', clarsimp) apply (clarsimp simp: projectKOs valid_obj'_def valid_ntfn'_def) apply (rule conjI, clarsimp split: option.splits) @@ -2251,14 +2252,15 @@ lemma cancelAllIPC_invs'[wp]: prefer 2 apply assumption apply (rule hoare_strengthen_post [OF get_ep_sp']) + apply (rename_tac rv s) apply (clarsimp simp: invs'_def valid_state'_def valid_ep'_def) apply (frule obj_at_valid_objs', fastforce) apply (clarsimp simp: projectKOs valid_obj'_def) apply (rule conjI) - apply (case_tac r, simp_all add: valid_ep'_def)[1] + apply (case_tac rv, simp_all add: valid_ep'_def)[1] apply (rule conjI[rotated]) apply (drule(1) sym_refs_ko_atD') - apply (case_tac r, simp_all add: st_tcb_at_refs_of_rev')[1] + apply (case_tac rv, simp_all add: st_tcb_at_refs_of_rev')[1] apply (clarsimp elim!: if_live_state_refsE | drule(1) bspec | drule st_tcb_at_state_refs_ofD')+ apply (drule(2) ep_q_refs_max) diff --git a/proof/refine/ARM/PageTableDuplicates.thy b/proof/refine/ARM/PageTableDuplicates.thy index 34e8d44f5..c9301f170 100644 --- a/proof/refine/ARM/PageTableDuplicates.thy +++ b/proof/refine/ARM/PageTableDuplicates.thy @@ -1727,7 +1727,6 @@ lemma cteDelete_valid_duplicates': apply (rule hoare_gen_asm) apply (simp add: cteDelete_def whenE_def split_def) apply (rule hoare_pre, wp finaliseSlot_invs) - apply simp apply (rule valid_validE) apply (rule hoare_post_imp[OF _ finaliseSlot_valid_duplicates']) apply simp diff --git a/proof/refine/ARM/Schedule_R.thy b/proof/refine/ARM/Schedule_R.thy index 20c24c654..199cd2e7c 100644 --- a/proof/refine/ARM/Schedule_R.thy +++ b/proof/refine/ARM/Schedule_R.thy @@ -238,7 +238,7 @@ proof - simp add: valid_queues_def) apply (wp hoare_vcg_if_lift hoare_vcg_conj_lift hoare_vcg_imp_lift)+ apply (wp hoare_vcg_imp_lift setQueue_valid_queues_no_bitmap_except_dequeue_wp - setQueue_valid_bitmapQ threadGet_const_tcb_at)+ + setQueue_valid_bitmapQ threadGet_const_tcb_at hoare_vcg_if_lift)+ (* wp done *) apply (normalise_obj_at') apply (clarsimp simp: correct_queue_def) diff --git a/proof/refine/ARM/TcbAcc_R.thy b/proof/refine/ARM/TcbAcc_R.thy index a078637c8..9122d635a 100644 --- a/proof/refine/ARM/TcbAcc_R.thy +++ b/proof/refine/ARM/TcbAcc_R.thy @@ -14,7 +14,6 @@ declare if_weak_cong [cong] declare result_in_set_wp[wp] declare hoare_in_monad_post[wp] declare trans_state_update'[symmetric,simp] -declare empty_fail_sequence_x[simp] declare storeWordUser_typ_at' [wp] (* Auxiliaries and basic properties of priority bitmap functions *) diff --git a/proof/refine/ARM/Tcb_R.thy b/proof/refine/ARM/Tcb_R.thy index 4842f42ba..a7b87e2cb 100644 --- a/proof/refine/ARM/Tcb_R.thy +++ b/proof/refine/ARM/Tcb_R.thy @@ -2752,6 +2752,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 apply (simp add: invokeTCB_def) apply (rule hoare_pre) apply (wpc | diff --git a/proof/refine/ARM/Untyped_R.thy b/proof/refine/ARM/Untyped_R.thy index de2445412..06e9511fb 100644 --- a/proof/refine/ARM/Untyped_R.thy +++ b/proof/refine/ARM/Untyped_R.thy @@ -5662,8 +5662,7 @@ lemma inv_untyped_IRQInactive: "\valid_irq_states'\ invokeUntyped ui -, \\rv s. intStateIRQTable (ksInterruptState s) rv \ irqstate.IRQInactive\" apply (simp add: invokeUntyped_def) - apply (rule hoare_pre) - apply (wp whenE_wp resetUntypedCap_IRQInactive | wpc | simp)+ + apply (wpsimp wp: resetUntypedCap_IRQInactive) done end diff --git a/proof/refine/ARM_HYP/ArchAcc_R.thy b/proof/refine/ARM_HYP/ArchAcc_R.thy index d2d3cb8ff..196e03386 100644 --- a/proof/refine/ARM_HYP/ArchAcc_R.thy +++ b/proof/refine/ARM_HYP/ArchAcc_R.thy @@ -342,6 +342,10 @@ lemma magnitudeCheck_assert2: using in_magnitude_check[where x=x and n=n and s=s and s'=s and v="()"] by (simp add: magnitudeCheck_assert in_monad) +lemma fst_fail: (* FIXME lib: move up *) + "fst (fail s) = {}" + by (simp add: fail_def) + lemma getObject_get_assert: assumes deflt: "\a b c d. (loadObject a b c d :: ('a :: pspace_storable) kernel) = loadObject_default a b c d" @@ -361,7 +365,7 @@ lemma getObject_get_assert: apply (simp add: lookupAround2_known1 assert_opt_def obj_at'_def projectKO_def2 split: option.split) - apply (clarsimp simp: fail_def fst_return conj_comms project_inject + apply (clarsimp simp: fst_fail fst_return conj_comms project_inject objBits_def) apply (simp only: assert2[symmetric], rule bind_apply_cong[OF refl]) diff --git a/proof/refine/ARM_HYP/Arch_R.thy b/proof/refine/ARM_HYP/Arch_R.thy index 1814816e2..5f0925b0d 100644 --- a/proof/refine/ARM_HYP/Arch_R.thy +++ b/proof/refine/ARM_HYP/Arch_R.thy @@ -1769,7 +1769,8 @@ lemma createMappingEntires_valid_slots_duplicated'[wp]: in hoare_post_imp_R) apply (wp lookupPTSlot_aligned lookupPTSlot_page_table_at' | simp add: vspace_bits_defs largePagePTEOffsets_def superSectionPDEOffsets_def)+ - apply (rule_tac x = r in exI) + apply (rename_tac rv s) + apply (rule_tac x = rv in exI) apply clarsimp apply (frule is_aligned_no_wrap'[where off = "0x78"]) apply simp diff --git a/proof/refine/ARM_HYP/CSpace_R.thy b/proof/refine/ARM_HYP/CSpace_R.thy index 941c3d6fd..356b58ea2 100644 --- a/proof/refine/ARM_HYP/CSpace_R.thy +++ b/proof/refine/ARM_HYP/CSpace_R.thy @@ -4020,8 +4020,9 @@ lemma setupReplyMaster_corres: cte_wp_at' ((=) rv) (cte_map (t, tcb_cnode_index 2))" in hoare_strengthen_post) apply (wp hoare_drop_imps getCTE_wp') + apply (rename_tac rv s) apply (clarsimp simp: cte_wp_at_ctes_of valid_mdb'_def valid_mdb_ctes_def) - apply (case_tac r, fastforce elim: valid_nullcapsE) + apply (case_tac rv, fastforce elim: valid_nullcapsE) apply (fastforce elim: tcb_at_cte_at) apply (clarsimp simp: cte_at'_obj_at' tcb_cte_cases_def cte_map_def) apply (clarsimp simp: invs'_def valid_state'_def valid_pspace'_def) diff --git a/proof/refine/ARM_HYP/Detype_R.thy b/proof/refine/ARM_HYP/Detype_R.thy index 5e8937cd7..f576b07b9 100644 --- a/proof/refine/ARM_HYP/Detype_R.thy +++ b/proof/refine/ARM_HYP/Detype_R.thy @@ -2164,7 +2164,7 @@ qed lemma empty_fail_locateCTE: "empty_fail (locateCTE src)" - by (simp add:locateCTE_def bind_assoc split_def) + by (fastforce simp: locateCTE_def bind_assoc split_def) lemma fail_empty_locateCTE: "snd (locateCTE src s) \ fst (locateCTE src s) = {}" diff --git a/proof/refine/ARM_HYP/EmptyFail.thy b/proof/refine/ARM_HYP/EmptyFail.thy index d3b7d68de..741a9ba83 100644 --- a/proof/refine/ARM_HYP/EmptyFail.thy +++ b/proof/refine/ARM_HYP/EmptyFail.thy @@ -19,12 +19,12 @@ lemma empty_fail_projectKO [simp, intro!]: lemma empty_fail_alignCheck [intro!, wp, simp]: "empty_fail (alignCheck a b)" unfolding alignCheck_def - by (simp add: alignError_def) + by (fastforce simp: alignError_def) lemma empty_fail_magnitudeCheck [intro!, wp, simp]: "empty_fail (magnitudeCheck a b c)" unfolding magnitudeCheck_def - by (simp split: option.splits) + by (fastforce split: option.splits) lemma empty_fail_loadObject_default [intro!, wp, simp]: shows "empty_fail (loadObject_default x b c d)" @@ -33,7 +33,7 @@ lemma empty_fail_loadObject_default [intro!, wp, simp]: lemma empty_fail_threadGet [intro!, wp, simp]: "empty_fail (threadGet f p)" - by (simp add: threadGet_def getObject_def split_def) + by (fastforce simp: threadGet_def getObject_def split_def) lemma empty_fail_getCTE [intro!, wp, simp]: "empty_fail (getCTE slot)" @@ -47,12 +47,12 @@ lemma empty_fail_getCTE [intro!, wp, simp]: lemma empty_fail_updateObject_cte [intro!, wp, simp]: "empty_fail (updateObject (v :: cte) ko a b c)" - by (simp add: updateObject_cte typeError_def unless_def split: kernel_object.splits ) + by (fastforce simp: updateObject_cte typeError_def unless_def split: kernel_object.splits ) lemma empty_fail_setCTE [intro!, wp, simp]: "empty_fail (setCTE p cte)" unfolding setCTE_def - by (simp add: setObject_def split_def) + by (fastforce simp: setObject_def split_def) lemma empty_fail_updateMDB [intro!, wp, simp]: "empty_fail (updateMDB a b)" @@ -60,16 +60,15 @@ lemma empty_fail_updateMDB [intro!, wp, simp]: lemma empty_fail_getSlotCap [intro!, wp, simp]: "empty_fail (getSlotCap a)" - unfolding getSlotCap_def by simp + unfolding getSlotCap_def by fastforce context begin interpretation Arch . (*FIXME: arch_split*) lemma empty_fail_getObject: - assumes x: "(\b c d. empty_fail (loadObject x b c d::'a :: pspace_storable kernel))" + assumes "\b c d. empty_fail (loadObject x b c d::'a :: pspace_storable kernel)" shows "empty_fail (getObject x :: 'a :: pspace_storable kernel)" apply (simp add: getObject_def split_def) - apply (safe intro!: empty_fail_bind empty_fail_gets empty_fail_assert_opt) - apply (rule x) + apply (safe intro!: assms) done lemma empty_fail_getObject_tcb [intro!, wp, simp]: @@ -78,22 +77,22 @@ lemma empty_fail_getObject_tcb [intro!, wp, simp]: lemma empty_fail_updateTrackedFreeIndex [intro!, wp, simp]: shows "empty_fail (updateTrackedFreeIndex p idx)" - by (simp add: updateTrackedFreeIndex_def) + by (fastforce simp add: updateTrackedFreeIndex_def) lemma empty_fail_updateNewFreeIndex [intro!, wp, simp]: shows "empty_fail (updateNewFreeIndex p)" apply (simp add: updateNewFreeIndex_def) - apply (safe intro!: empty_fail_bind) + apply safe apply (simp split: capability.split) done lemma empty_fail_insertNewCap [intro!, wp, simp]: "empty_fail (insertNewCap p p' cap)" - unfolding insertNewCap_def by simp + unfolding insertNewCap_def by fastforce lemma empty_fail_getIRQSlot [intro!, wp, simp]: "empty_fail (getIRQSlot irq)" - by (simp add: getIRQSlot_def getInterruptState_def locateSlot_conv) + by (fastforce simp: getIRQSlot_def getInterruptState_def locateSlot_conv) lemma empty_fail_getObject_ntfn [intro!, wp, simp]: "empty_fail (getObject p :: Structures_H.notification kernel)" @@ -107,15 +106,15 @@ lemma empty_fail_lookupIPCBuffer [intro!, wp, simp]: "empty_fail (lookupIPCBuffer a b)" by (clarsimp simp: lookupIPCBuffer_def Let_def getThreadBufferSlot_def locateSlot_conv - split: capability.splits arch_capability.splits | wp | wpc)+ + split: capability.splits arch_capability.splits | wp | wpc | safe)+ lemma empty_fail_updateObject_default [intro!, wp, simp]: "empty_fail (updateObject_default v ko a b c)" - by (simp add: updateObject_default_def typeError_def unless_def split: kernel_object.splits ) + by (fastforce simp: updateObject_default_def typeError_def unless_def split: kernel_object.splits) lemma empty_fail_threadSet [intro!, wp, simp]: "empty_fail (threadSet f p)" - by (simp add: threadSet_def getObject_def setObject_def split_def) + by (fastforce simp: threadSet_def getObject_def setObject_def split_def) lemma empty_fail_getThreadState[iff]: "empty_fail (getThreadState t)" diff --git a/proof/refine/ARM_HYP/EmptyFail_H.thy b/proof/refine/ARM_HYP/EmptyFail_H.thy index b20a5662f..129f720fd 100644 --- a/proof/refine/ARM_HYP/EmptyFail_H.thy +++ b/proof/refine/ARM_HYP/EmptyFail_H.thy @@ -17,19 +17,19 @@ context begin interpretation Arch . (*FIXME: arch_split*) lemmas forM_empty_fail[intro!, wp, simp] = empty_fail_mapM[simplified forM_def[symmetric]] lemmas forM_x_empty_fail[intro!, wp, simp] = empty_fail_mapM_x[simplified forM_x_def[symmetric]] -lemmas forME_x_empty_fail[intro!, wp, simp] = mapME_x_empty_fail[simplified forME_x_def[symmetric]] +lemmas forME_x_empty_fail[intro!, wp, simp] = empty_fail_mapME_x[simplified forME_x_def[symmetric]] lemma withoutPreemption_empty_fail[intro!, wp, simp]: "empty_fail m \ empty_fail (withoutPreemption m)" - by (simp add: withoutPreemption_def) + by simp lemma withoutFailure_empty_fail[intro!, wp, simp]: "empty_fail m \ empty_fail (withoutFailure m)" - by (simp add: withoutFailure_def) + by simp lemma catchFailure_empty_fail[intro!, wp, simp]: "\ empty_fail f; \x. empty_fail (g x) \ \ empty_fail (catchFailure f g)" - by (simp add: catchFailure_def empty_fail_catch) + by (simp add: empty_fail_catch) lemma emptyOnFailure_empty_fail[intro!, wp, simp]: "empty_fail m \ empty_fail (emptyOnFailure m)" @@ -86,9 +86,6 @@ proof (induct arbitrary: s rule: resolveAddressBits.induct) lemmas resolveAddressBits_empty_fail[intro!, wp, simp] = resolveAddressBits_spec_empty_fail[THEN use_spec_empty_fail] -crunch (empty_fail) empty_fail[intro!, wp, simp]: lookupIPCBuffer -(simp:Let_def) - declare ef_dmo'[intro!, wp, simp] lemma empty_fail_getObject_ep [intro!, wp, simp]: @@ -178,11 +175,11 @@ crunch (empty_fail) "_H_empty_fail"[intro!, wp, simp]: "ThreadDecls_H.suspend" lemma ThreadDecls_H_restart_empty_fail[intro!, wp, simp]: "empty_fail (ThreadDecls_H.restart target)" - by (simp add:restart_def) + by (fastforce simp: restart_def) lemma vcpuUpdate_empty_fail[intro!, wp, simp]: "empty_fail (vcpuUpdate p f)" - by (simp add: vcpuUpdate_def) + by (fastforce simp: vcpuUpdate_def) crunch (empty_fail) empty_fail[intro!, wp, simp]: vcpuEnable, vcpuRestore (simp: uncurry_def) @@ -223,18 +220,14 @@ lemmas finaliseSlot_empty_fail[intro!, wp, simp] = lemma checkCapAt_empty_fail[intro!, wp, simp]: "empty_fail action \ empty_fail (checkCapAt cap ptr action)" - by (simp add: checkCapAt_def) + by (fastforce simp: checkCapAt_def) lemma assertDerived_empty_fail[intro!, wp, simp]: "empty_fail f \ empty_fail (assertDerived src cap f)" - by (simp add: assertDerived_def) + by (fastforce simp: assertDerived_def) crunch (empty_fail) empty_fail[intro!, wp, simp]: cteDelete -lemma liftE_empty_fail[intro!, wp, simp]: - "empty_fail f \ empty_fail (liftE f)" - by simp - lemma spec_empty_fail_unlessE': "\ \ P \ spec_empty_fail f s \ \ spec_empty_fail (unlessE P f) s" by (simp add:unlessE_def spec_empty_returnOk) @@ -264,7 +257,7 @@ lemma Syscall_H_syscall_empty_fail[intro!, wp, simp]: lemma catchError_empty_fail[intro!, wp, simp]: "\ empty_fail f; \x. empty_fail (g x) \ \ empty_fail (catchError f g)" - by (simp add: catchError_def handle_empty_fail) + by fastforce crunch (empty_fail) empty_fail[intro!, wp, simp]: chooseThread, getDomainTime, nextDomain, isHighestPrio diff --git a/proof/refine/ARM_HYP/Finalise_R.thy b/proof/refine/ARM_HYP/Finalise_R.thy index 8229aa571..15b0add5c 100644 --- a/proof/refine/ARM_HYP/Finalise_R.thy +++ b/proof/refine/ARM_HYP/Finalise_R.thy @@ -2400,11 +2400,12 @@ lemma deleteASID_invs'[wp]: apply (simp add: deleteASID_def cong: option.case_cong) apply (rule hoare_pre) apply (wp | wpc)+ - apply (rule_tac Q="\rv. valid_obj' (injectKO rv) and invs'" - in hoare_post_imp) + apply (rule_tac Q="\rv. valid_obj' (injectKO rv) and invs'" + in hoare_post_imp) + apply (rename_tac rv s) apply (clarsimp split: if_split_asm del: subsetI) apply (simp add: fun_upd_def[symmetric] valid_obj'_def) - apply (case_tac r, simp) + apply (case_tac rv, simp) apply (subst inv_f_f, rule inj_onI, simp)+ apply (rule conjI) apply clarsimp diff --git a/proof/refine/ARM_HYP/Interrupt_R.thy b/proof/refine/ARM_HYP/Interrupt_R.thy index 432ea3c6d..7a93ec1cc 100644 --- a/proof/refine/ARM_HYP/Interrupt_R.thy +++ b/proof/refine/ARM_HYP/Interrupt_R.thy @@ -186,6 +186,7 @@ crunches arch_check_irq, checkIRQ lemma arch_check_irq_maxIRQ_valid: "\\\ arch_check_irq y \\_. (\s. unat y \ unat maxIRQ)\, -" unfolding arch_check_irq_def + supply hoare_vcg_prop[wp del] (* FIXME lib: check rule order *) apply (wpsimp simp: validE_R_def wp: whenE_throwError_wp) by (metis unat_ucast_10_32 word_le_nat_alt word_le_not_less) @@ -874,14 +875,15 @@ proof - \ sch_act_not rv x \ (\d p. rv \ set (ksReadyQueues x (d, p)))" in hoare_post_imp) + apply (rename_tac rv s) apply clarsimp apply (strengthen st_tcb_ex_cap''[where P=active']) apply (strengthen invs_iflive') apply (clarsimp cong: imp_cong conj_cong simp: not_pred_tcb') apply (clarsimp simp: pred_tcb_at'_def) - apply (rule conjI, erule_tac p=r in obj_at'_weakenE - , fastforce split: thread_state.splits) - apply (erule_tac p=r in obj_at'_weakenE, fastforce split: thread_state.splits) + apply (rule conjI, erule_tac p=rv in obj_at'_weakenE, + fastforce split: thread_state.splits) + apply (erule_tac p=rv in obj_at'_weakenE, fastforce split: thread_state.splits) apply wp apply (wpsimp wp: wplr wplr' hoare_vcg_all_lift hoare_vcg_imp_lift' dmo_gets_wp dmo'_gets_wp @@ -946,12 +948,13 @@ lemma vppiEvent_corres: \ invs' x \ sch_act_not rv x \ (\d p. rv \ set (ksReadyQueues x (d, p)))" in hoare_post_imp) + apply (rename_tac rv s) apply (strengthen st_tcb_ex_cap''[where P=active']) apply (strengthen invs_iflive') apply (clarsimp cong: imp_cong conj_cong simp: not_pred_tcb') apply (clarsimp simp: pred_tcb_at'_def) - apply (rule conjI, erule_tac p=r in obj_at'_weakenE, fastforce split: thread_state.splits) - apply (erule_tac p=r in obj_at'_weakenE, fastforce split: thread_state.splits) + apply (rule conjI, erule_tac p=rv in obj_at'_weakenE, fastforce split: thread_state.splits) + apply (erule_tac p=rv in obj_at'_weakenE, fastforce split: thread_state.splits) apply wp apply (wpsimp wp: vcpu_update_tcb_at hoare_vcg_all_lift hoare_vcg_imp_lift' cong: vcpu.fold_congs)+ @@ -1026,10 +1029,6 @@ lemma handleInterrupt_corres: apply (rule corres_machine_op, rule corres_eq_trivial ; (simp add: no_fail_maskInterrupt no_fail_bind no_fail_ackInterrupt)+)+ apply wp+ - apply clarsimp - apply clarsimp - apply (rule hoare_post_taut) (* FIXME: wp (once) does not terminate? *) - apply wp+ apply clarsimp apply fastforce apply (rule corres_guard_imp) diff --git a/proof/refine/ARM_HYP/IpcCancel_R.thy b/proof/refine/ARM_HYP/IpcCancel_R.thy index 7ef00de13..49a70b700 100644 --- a/proof/refine/ARM_HYP/IpcCancel_R.thy +++ b/proof/refine/ARM_HYP/IpcCancel_R.thy @@ -699,12 +699,13 @@ lemma cancelSignal_invs': apply assumption apply (rule hoare_strengthen_post) apply (rule get_ntfn_sp') + apply (rename_tac rv s) apply (clarsimp simp: pred_tcb_at') apply (frule NIQ) apply (clarsimp simp: pred_tcb_at'_def obj_at'_def) apply (rule conjI) apply (clarsimp simp: valid_ntfn'_def) - apply (case_tac "ntfnObj r", simp_all add: isWaitingNtfn_def) + apply (case_tac "ntfnObj rv", simp_all add: isWaitingNtfn_def) apply (frule ko_at_valid_objs') apply (simp add: valid_pspace_valid_objs') apply (clarsimp simp: projectKO_opt_ntfn split: kernel_object.splits) @@ -729,7 +730,7 @@ lemma cancelSignal_invs': split: ntfn.splits) apply (rule conjI, clarsimp elim!: if_live_state_refsE) apply (fastforce simp: sym_refs_def dest!: idle'_no_refs) - apply (case_tac "ntfnObj r", simp_all) + apply (case_tac "ntfnObj rv", simp_all) apply (frule obj_at_valid_objs', clarsimp) apply (clarsimp simp: projectKOs valid_obj'_def valid_ntfn'_def) apply (rule conjI, clarsimp split: option.splits) @@ -745,7 +746,7 @@ lemma cancelSignal_invs': set_eq_subset) apply (rule conjI, clarsimp elim!: if_live_state_refsE) apply (rule conjI) - apply (case_tac "ntfnBoundTCB r") + apply (case_tac "ntfnBoundTCB rv") apply (clarsimp elim!: if_live_state_refsE)+ apply (clarsimp dest!: idle'_no_refs) done diff --git a/proof/refine/ARM_HYP/PageTableDuplicates.thy b/proof/refine/ARM_HYP/PageTableDuplicates.thy index d50e09f61..6dd347159 100644 --- a/proof/refine/ARM_HYP/PageTableDuplicates.thy +++ b/proof/refine/ARM_HYP/PageTableDuplicates.thy @@ -1335,7 +1335,6 @@ lemma cteDelete_valid_duplicates': apply (rule hoare_gen_asm) apply (simp add: cteDelete_def whenE_def split_def) apply (rule hoare_pre, wp finaliseSlot_invs) - apply simp apply (rule valid_validE) apply (rule hoare_post_imp[OF _ finaliseSlot_valid_duplicates']) apply simp diff --git a/proof/refine/ARM_HYP/Schedule_R.thy b/proof/refine/ARM_HYP/Schedule_R.thy index 43ce7f78a..d9467203f 100644 --- a/proof/refine/ARM_HYP/Schedule_R.thy +++ b/proof/refine/ARM_HYP/Schedule_R.thy @@ -318,7 +318,7 @@ proof - simp add: valid_queues_def) apply (wp hoare_vcg_if_lift hoare_vcg_conj_lift hoare_vcg_imp_lift)+ apply (wp hoare_vcg_imp_lift setQueue_valid_queues_no_bitmap_except_dequeue_wp - setQueue_valid_bitmapQ threadGet_const_tcb_at)+ + setQueue_valid_bitmapQ threadGet_const_tcb_at hoare_vcg_if_lift)+ (* wp done *) apply (normalise_obj_at') apply (clarsimp simp: correct_queue_def) diff --git a/proof/refine/ARM_HYP/Syscall_R.thy b/proof/refine/ARM_HYP/Syscall_R.thy index 59d420c3f..c1bc9f1d2 100644 --- a/proof/refine/ARM_HYP/Syscall_R.thy +++ b/proof/refine/ARM_HYP/Syscall_R.thy @@ -2255,7 +2255,6 @@ lemma hi_IRQInactive: -, \\rv s. intStateIRQTable (ksInterruptState s) rv \ irqstate.IRQInactive\" apply (simp add: handleInvocation_def split_def) apply (wp syscall_valid' retype_pi_IRQInactive) - apply simp_all done lemma handleSend_IRQInactive: diff --git a/proof/refine/ARM_HYP/TcbAcc_R.thy b/proof/refine/ARM_HYP/TcbAcc_R.thy index 5a043d2f6..1a4ab8ae0 100644 --- a/proof/refine/ARM_HYP/TcbAcc_R.thy +++ b/proof/refine/ARM_HYP/TcbAcc_R.thy @@ -14,7 +14,6 @@ declare if_weak_cong [cong] declare result_in_set_wp[wp] declare hoare_in_monad_post[wp] declare trans_state_update'[symmetric,simp] -declare empty_fail_sequence_x[simp] declare storeWordUser_typ_at' [wp] (* Auxiliaries and basic properties of priority bitmap functions *) diff --git a/proof/refine/ARM_HYP/Tcb_R.thy b/proof/refine/ARM_HYP/Tcb_R.thy index 8e8813038..8259c4e21 100644 --- a/proof/refine/ARM_HYP/Tcb_R.thy +++ b/proof/refine/ARM_HYP/Tcb_R.thy @@ -2779,6 +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 apply (simp add: invokeTCB_def) apply (rule hoare_pre) apply (wpc | diff --git a/proof/refine/ARM_HYP/Untyped_R.thy b/proof/refine/ARM_HYP/Untyped_R.thy index 8e786c767..ea0e241e7 100644 --- a/proof/refine/ARM_HYP/Untyped_R.thy +++ b/proof/refine/ARM_HYP/Untyped_R.thy @@ -5719,8 +5719,7 @@ lemma inv_untyped_IRQInactive: "\valid_irq_states'\ invokeUntyped ui -, \\rv s. intStateIRQTable (ksInterruptState s) rv \ irqstate.IRQInactive\" apply (simp add: invokeUntyped_def) - apply (rule hoare_pre) - apply (wp whenE_wp resetUntypedCap_IRQInactive | wpc | simp)+ + apply (wpsimp wp: resetUntypedCap_IRQInactive) done end diff --git a/proof/refine/ARM_HYP/VSpace_R.thy b/proof/refine/ARM_HYP/VSpace_R.thy index c677628bc..29af49516 100644 --- a/proof/refine/ARM_HYP/VSpace_R.thy +++ b/proof/refine/ARM_HYP/VSpace_R.thy @@ -982,7 +982,7 @@ lemma vcpuDisable_corres: apply (cases vcpuopt; clarsimp simp: vcpu_disable_def vcpuDisable_def) (* no current VCPU *) subgoal - apply (clarsimp simp: doMachineOp_bind do_machine_op_bind) + apply (clarsimp simp: doMachineOp_bind do_machine_op_bind empty_fail_cond) apply (rule corres_guard_imp) apply (rule corres_split_dc[OF corres_machine_op] | rule corres_machine_op corres_Id @@ -1036,7 +1036,7 @@ lemma vcpuRestore_corres: apply (case_tac vcpu' , clarsimp simp: comp_def vcpu_relation_def vgic_map_def mapM_x_mapM uncurry_def split_def mapM_map_simp) - apply (simp add: doMachineOp_bind do_machine_op_bind bind_assoc) + apply (simp add: doMachineOp_bind do_machine_op_bind bind_assoc empty_fail_cond) apply (rule corres_split_dc[OF corres_machine_op]) apply (rule corres_Id; wpsimp) apply (rule corres_split_dc[OF corres_machine_op]) @@ -4125,7 +4125,7 @@ lemma vcpuDisable_invs'[wp]: getSCTLR_def get_gic_vcpu_ctrl_hcr_def dsb_def vgicUpdate_def vcpuUpdate_def vcpuSaveReg_def by (wpsimp wp: dmo'_gets_wp setVCPU_vgic_invs' setVCPU_regs_invs' dmo_maskInterrupt_True - simp: doMachineOp_bind) + simp: doMachineOp_bind empty_fail_cond) lemma vcpuInvalidateActive_invs'[wp]: "vcpuInvalidateActive \invs'\" diff --git a/proof/refine/RISCV64/CSpace_R.thy b/proof/refine/RISCV64/CSpace_R.thy index d7ee32c48..96aace713 100644 --- a/proof/refine/RISCV64/CSpace_R.thy +++ b/proof/refine/RISCV64/CSpace_R.thy @@ -3969,8 +3969,9 @@ lemma setupReplyMaster_corres: cte_wp_at' ((=) rv) (cte_map (t, tcb_cnode_index 2))" in hoare_strengthen_post) apply (wp hoare_drop_imps getCTE_wp') + apply (rename_tac rv s) apply (clarsimp simp: cte_wp_at_ctes_of valid_mdb'_def valid_mdb_ctes_def) - apply (case_tac r, fastforce elim: valid_nullcapsE) + apply (case_tac rv, fastforce elim: valid_nullcapsE) apply (fastforce elim: tcb_at_cte_at) apply (clarsimp simp: cte_at'_obj_at' tcb_cte_cases_def cte_map_def) apply (clarsimp simp: invs'_def valid_state'_def valid_pspace'_def) diff --git a/proof/refine/RISCV64/Detype_R.thy b/proof/refine/RISCV64/Detype_R.thy index efd2c62f2..b6b3cbbf8 100644 --- a/proof/refine/RISCV64/Detype_R.thy +++ b/proof/refine/RISCV64/Detype_R.thy @@ -2010,7 +2010,7 @@ qed lemma empty_fail_locateCTE: "empty_fail (locateCTE src)" - by (simp add:locateCTE_def bind_assoc split_def) + by (fastforce simp: locateCTE_def bind_assoc split_def) lemma fail_empty_locateCTE: "snd (locateCTE src s) \ fst (locateCTE src s) = {}" diff --git a/proof/refine/RISCV64/EmptyFail.thy b/proof/refine/RISCV64/EmptyFail.thy index 42bd0962e..87316f621 100644 --- a/proof/refine/RISCV64/EmptyFail.thy +++ b/proof/refine/RISCV64/EmptyFail.thy @@ -19,12 +19,12 @@ lemma empty_fail_projectKO [simp, intro!]: lemma empty_fail_alignCheck [intro!, wp, simp]: "empty_fail (alignCheck a b)" unfolding alignCheck_def - by (simp add: alignError_def) + by (fastforce simp: alignError_def) lemma empty_fail_magnitudeCheck [intro!, wp, simp]: "empty_fail (magnitudeCheck a b c)" unfolding magnitudeCheck_def - by (simp split: option.splits) + by (fastforce split: option.splits) lemma empty_fail_loadObject_default [intro!, wp, simp]: shows "empty_fail (loadObject_default x b c d)" @@ -33,7 +33,7 @@ lemma empty_fail_loadObject_default [intro!, wp, simp]: lemma empty_fail_threadGet [intro!, wp, simp]: "empty_fail (threadGet f p)" - by (simp add: threadGet_def getObject_def split_def) + by (fastforce simp: threadGet_def getObject_def split_def) lemma empty_fail_getCTE [intro!, wp, simp]: "empty_fail (getCTE slot)" @@ -47,12 +47,12 @@ lemma empty_fail_getCTE [intro!, wp, simp]: lemma empty_fail_updateObject_cte [intro!, wp, simp]: "empty_fail (updateObject (v :: cte) ko a b c)" - by (simp add: updateObject_cte typeError_def unless_def split: kernel_object.splits ) + by (fastforce simp: updateObject_cte typeError_def unless_def split: kernel_object.splits ) lemma empty_fail_setCTE [intro!, wp, simp]: "empty_fail (setCTE p cte)" unfolding setCTE_def - by (simp add: setObject_def split_def) + by (fastforce simp: setObject_def split_def) lemma empty_fail_updateCap [intro!, wp, simp]: "empty_fail (updateCap p f)" @@ -64,36 +64,35 @@ lemma empty_fail_updateMDB [intro!, wp, simp]: lemma empty_fail_getSlotCap [intro!, wp, simp]: "empty_fail (getSlotCap a)" - unfolding getSlotCap_def by simp + unfolding getSlotCap_def by fastforce context begin interpretation Arch . (*FIXME: arch_split*) lemma empty_fail_getObject: - assumes x: "(\b c d. empty_fail (loadObject x b c d::'a :: pspace_storable kernel))" + assumes "\b c d. empty_fail (loadObject x b c d::'a :: pspace_storable kernel)" shows "empty_fail (getObject x :: 'a :: pspace_storable kernel)" apply (simp add: getObject_def split_def) - apply (safe intro!: empty_fail_bind empty_fail_gets empty_fail_assert_opt) - apply (rule x) + apply (safe intro!: assms) done lemma empty_fail_updateTrackedFreeIndex [intro!, wp, simp]: shows "empty_fail (updateTrackedFreeIndex p idx)" - by (simp add: updateTrackedFreeIndex_def) + by (fastforce simp add: updateTrackedFreeIndex_def) lemma empty_fail_updateNewFreeIndex [intro!, wp, simp]: shows "empty_fail (updateNewFreeIndex p)" apply (simp add: updateNewFreeIndex_def) - apply (safe intro!: empty_fail_bind) + apply safe apply (simp split: capability.split) done lemma empty_fail_insertNewCap [intro!, wp, simp]: "empty_fail (insertNewCap p p' cap)" - unfolding insertNewCap_def by simp + unfolding insertNewCap_def by fastforce lemma empty_fail_getIRQSlot [intro!, wp, simp]: "empty_fail (getIRQSlot irq)" - by (simp add: getIRQSlot_def getInterruptState_def locateSlot_conv) + by (fastforce simp: getIRQSlot_def getInterruptState_def locateSlot_conv) lemma empty_fail_getObject_ntfn [intro!, wp, simp]: "empty_fail (getObject p :: Structures_H.notification kernel)" @@ -106,15 +105,15 @@ lemma empty_fail_getNotification [intro!, wp, simp]: lemma empty_fail_lookupIPCBuffer [intro!, wp, simp]: "empty_fail (lookupIPCBuffer a b)" by (clarsimp simp: lookupIPCBuffer_def Let_def getThreadBufferSlot_def locateSlot_conv - split: capability.splits arch_capability.splits | wp | wpc)+ + split: capability.splits arch_capability.splits | wp | wpc | safe)+ lemma empty_fail_updateObject_default [intro!, wp, simp]: "empty_fail (updateObject_default v ko a b c)" - by (simp add: updateObject_default_def typeError_def unless_def split: kernel_object.splits ) + by (fastforce simp: updateObject_default_def typeError_def unless_def split: kernel_object.splits ) lemma empty_fail_threadSet [intro!, wp, simp]: "empty_fail (threadSet f p)" - by (simp add: threadSet_def getObject_def setObject_def split_def) + by (fastforce simp: threadSet_def getObject_def setObject_def split_def) lemma empty_fail_getThreadState[iff]: "empty_fail (getThreadState t)" diff --git a/proof/refine/RISCV64/EmptyFail_H.thy b/proof/refine/RISCV64/EmptyFail_H.thy index edd562214..50293f474 100644 --- a/proof/refine/RISCV64/EmptyFail_H.thy +++ b/proof/refine/RISCV64/EmptyFail_H.thy @@ -17,7 +17,7 @@ context begin interpretation Arch . (*FIXME: arch_split*) lemmas forM_empty_fail[intro!, wp, simp] = empty_fail_mapM[simplified forM_def[symmetric]] lemmas forM_x_empty_fail[intro!, wp, simp] = empty_fail_mapM_x[simplified forM_x_def[symmetric]] -lemmas forME_x_empty_fail[intro!, wp, simp] = mapME_x_empty_fail[simplified forME_x_def[symmetric]] +lemmas forME_x_empty_fail[intro!, wp, simp] = empty_fail_mapME_x[simplified forME_x_def[symmetric]] lemma withoutPreemption_empty_fail[intro!, wp, simp]: "empty_fail m \ empty_fail (withoutPreemption m)" @@ -80,9 +80,6 @@ proof (induct arbitrary: s rule: resolveAddressBits.induct) lemmas resolveAddressBits_empty_fail[intro!, wp, simp] = resolveAddressBits_spec_empty_fail[THEN use_spec_empty_fail] -crunch (empty_fail) empty_fail[intro!, wp, simp]: lookupIPCBuffer -(simp:Let_def) - declare ef_dmo'[intro!, wp, simp] lemma empty_fail_getObject_ep [intro!, wp, simp]: @@ -173,7 +170,7 @@ crunch (empty_fail) "_H_empty_fail"[intro!, wp, simp]: "ThreadDecls_H.suspend" lemma ThreadDecls_H_restart_empty_fail[intro!, wp, simp]: "empty_fail (ThreadDecls_H.restart target)" - by (simp add:restart_def) + by (fastforce simp: restart_def) lemma empty_fail_lookupPTFromLevel[intro!, wp, simp]: "empty_fail (lookupPTFromLevel level ptPtr vPtr target)" @@ -217,18 +214,14 @@ lemmas finaliseSlot_empty_fail[intro!, wp, simp] = lemma checkCapAt_empty_fail[intro!, wp, simp]: "empty_fail action \ empty_fail (checkCapAt cap ptr action)" - by (simp add: checkCapAt_def) + by (fastforce simp: checkCapAt_def) lemma assertDerived_empty_fail[intro!, wp, simp]: "empty_fail f \ empty_fail (assertDerived src cap f)" - by (simp add: assertDerived_def) + by (fastforce simp: assertDerived_def) crunch (empty_fail) empty_fail[intro!, wp, simp]: cteDelete -lemma liftE_empty_fail[intro!, wp, simp]: - "empty_fail f \ empty_fail (liftE f)" - by simp - lemma spec_empty_fail_unlessE': "\ \ P \ spec_empty_fail f s \ \ spec_empty_fail (unlessE P f) s" by (simp add:unlessE_def spec_empty_returnOk) @@ -258,7 +251,7 @@ lemma Syscall_H_syscall_empty_fail[intro!, wp, simp]: lemma catchError_empty_fail[intro!, wp, simp]: "\ empty_fail f; \x. empty_fail (g x) \ \ empty_fail (catchError f g)" - by (simp add: catchError_def handle_empty_fail) + by fastforce crunch (empty_fail) empty_fail[intro!, wp, simp]: chooseThread, getDomainTime, nextDomain, isHighestPrio diff --git a/proof/refine/RISCV64/IpcCancel_R.thy b/proof/refine/RISCV64/IpcCancel_R.thy index d351a96e8..a39155cad 100644 --- a/proof/refine/RISCV64/IpcCancel_R.thy +++ b/proof/refine/RISCV64/IpcCancel_R.thy @@ -689,12 +689,13 @@ lemma cancelSignal_invs': apply assumption apply (rule hoare_strengthen_post) apply (rule get_ntfn_sp') + apply (rename_tac rv s) apply (clarsimp simp: pred_tcb_at') apply (frule NIQ) apply (clarsimp simp: pred_tcb_at'_def obj_at'_def) apply (rule conjI) apply (clarsimp simp: valid_ntfn'_def) - apply (case_tac "ntfnObj r", simp_all add: isWaitingNtfn_def) + apply (case_tac "ntfnObj rv", simp_all add: isWaitingNtfn_def) apply (frule ko_at_valid_objs') apply (simp add: valid_pspace_valid_objs') apply (clarsimp simp: projectKO_opt_ntfn split: kernel_object.splits) @@ -717,7 +718,7 @@ lemma cancelSignal_invs': split: ntfn.splits) apply (rule conjI, clarsimp elim!: if_live_state_refsE) apply (fastforce simp: sym_refs_def dest!: idle'_no_refs) - apply (case_tac "ntfnObj r", simp_all) + apply (case_tac "ntfnObj rv", simp_all) apply (frule obj_at_valid_objs', clarsimp) apply (clarsimp simp: valid_obj'_def valid_ntfn'_def) apply (rule conjI, clarsimp split: option.splits) @@ -2224,14 +2225,15 @@ lemma cancelAllIPC_invs'[wp]: prefer 2 apply assumption apply (rule hoare_strengthen_post [OF get_ep_sp']) + apply (rename_tac rv s) apply (clarsimp simp: invs'_def valid_state'_def valid_ep'_def) apply (frule obj_at_valid_objs', fastforce) apply (clarsimp simp: valid_obj'_def) apply (rule conjI) - apply (case_tac r, simp_all add: valid_ep'_def)[1] + apply (case_tac rv, simp_all add: valid_ep'_def)[1] apply (rule conjI[rotated]) apply (drule(1) sym_refs_ko_atD') - apply (case_tac r, simp_all add: st_tcb_at_refs_of_rev')[1] + apply (case_tac rv, simp_all add: st_tcb_at_refs_of_rev')[1] apply (clarsimp elim!: if_live_state_refsE | drule(1) bspec | drule st_tcb_at_state_refs_ofD')+ apply (drule(2) ep_q_refs_max) diff --git a/proof/refine/RISCV64/Schedule_R.thy b/proof/refine/RISCV64/Schedule_R.thy index 07703557b..3c7f31c1d 100644 --- a/proof/refine/RISCV64/Schedule_R.thy +++ b/proof/refine/RISCV64/Schedule_R.thy @@ -244,7 +244,7 @@ proof - simp add: valid_queues_def) apply (wp hoare_vcg_if_lift hoare_vcg_conj_lift hoare_vcg_imp_lift)+ apply (wp hoare_vcg_imp_lift setQueue_valid_queues_no_bitmap_except_dequeue_wp - setQueue_valid_bitmapQ threadGet_const_tcb_at)+ + setQueue_valid_bitmapQ threadGet_const_tcb_at hoare_vcg_if_lift)+ (* wp done *) apply (normalise_obj_at') apply (clarsimp simp: correct_queue_def) diff --git a/proof/refine/RISCV64/Syscall_R.thy b/proof/refine/RISCV64/Syscall_R.thy index 504d1e7e9..eed665862 100644 --- a/proof/refine/RISCV64/Syscall_R.thy +++ b/proof/refine/RISCV64/Syscall_R.thy @@ -2181,7 +2181,6 @@ lemma hi_IRQInactive: -, \\rv s. intStateIRQTable (ksInterruptState s) rv \ irqstate.IRQInactive\" apply (simp add: handleInvocation_def split_def) apply (wp syscall_valid' retype_pi_IRQInactive) - apply simp_all done lemma handleSend_IRQInactive: diff --git a/proof/refine/RISCV64/TcbAcc_R.thy b/proof/refine/RISCV64/TcbAcc_R.thy index 4f8b9d42b..22465675f 100644 --- a/proof/refine/RISCV64/TcbAcc_R.thy +++ b/proof/refine/RISCV64/TcbAcc_R.thy @@ -14,7 +14,6 @@ declare if_weak_cong [cong] declare result_in_set_wp[wp] declare hoare_in_monad_post[wp] declare trans_state_update'[symmetric,simp] -declare empty_fail_sequence_x[simp] declare storeWordUser_typ_at' [wp] (* Auxiliaries and basic properties of priority bitmap functions *) diff --git a/proof/refine/RISCV64/Tcb_R.thy b/proof/refine/RISCV64/Tcb_R.thy index 86fc1999f..f5d625eba 100644 --- a/proof/refine/RISCV64/Tcb_R.thy +++ b/proof/refine/RISCV64/Tcb_R.thy @@ -2703,6 +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 apply (simp add: invokeTCB_def) apply (rule hoare_pre) apply (wpc | diff --git a/proof/refine/X64/CSpace_R.thy b/proof/refine/X64/CSpace_R.thy index 8025ab2bb..eb02e8ac8 100644 --- a/proof/refine/X64/CSpace_R.thy +++ b/proof/refine/X64/CSpace_R.thy @@ -4165,8 +4165,9 @@ lemma setupReplyMaster_corres: cte_wp_at' ((=) rv) (cte_map (t, tcb_cnode_index 2))" in hoare_strengthen_post) apply (wp hoare_drop_imps getCTE_wp') + apply (rename_tac rv s) apply (clarsimp simp: cte_wp_at_ctes_of valid_mdb'_def valid_mdb_ctes_def) - apply (case_tac r, fastforce elim: valid_nullcapsE) + apply (case_tac rv, fastforce elim: valid_nullcapsE) apply (fastforce elim: tcb_at_cte_at) apply (clarsimp simp: cte_at'_obj_at' tcb_cte_cases_def cte_map_def) apply (clarsimp simp: invs'_def valid_state'_def valid_pspace'_def) diff --git a/proof/refine/X64/Detype_R.thy b/proof/refine/X64/Detype_R.thy index 280fbc199..cfdc950da 100644 --- a/proof/refine/X64/Detype_R.thy +++ b/proof/refine/X64/Detype_R.thy @@ -2122,7 +2122,7 @@ qed lemma empty_fail_locateCTE: "empty_fail (locateCTE src)" - by (simp add:locateCTE_def bind_assoc split_def) + by (fastforce simp: locateCTE_def bind_assoc split_def) lemma fail_empty_locateCTE: "snd (locateCTE src s) \ fst (locateCTE src s) = {}" diff --git a/proof/refine/X64/EmptyFail.thy b/proof/refine/X64/EmptyFail.thy index 6a0f0f136..7c62a3f9c 100644 --- a/proof/refine/X64/EmptyFail.thy +++ b/proof/refine/X64/EmptyFail.thy @@ -19,12 +19,12 @@ lemma empty_fail_projectKO [simp, intro!]: lemma empty_fail_alignCheck [intro!, wp, simp]: "empty_fail (alignCheck a b)" unfolding alignCheck_def - by (simp add: alignError_def) + by (fastforce simp: alignError_def) lemma empty_fail_magnitudeCheck [intro!, wp, simp]: "empty_fail (magnitudeCheck a b c)" unfolding magnitudeCheck_def - by (simp split: option.splits) + by (fastforce split: option.splits) lemma empty_fail_loadObject_default [intro!, wp, simp]: shows "empty_fail (loadObject_default x b c d)" @@ -33,7 +33,7 @@ lemma empty_fail_loadObject_default [intro!, wp, simp]: lemma empty_fail_threadGet [intro!, wp, simp]: "empty_fail (threadGet f p)" - by (simp add: threadGet_def getObject_def split_def) + by (fastforce simp: threadGet_def getObject_def split_def) lemma empty_fail_getCTE [intro!, wp, simp]: "empty_fail (getCTE slot)" @@ -47,12 +47,12 @@ lemma empty_fail_getCTE [intro!, wp, simp]: lemma empty_fail_updateObject_cte [intro!, wp, simp]: "empty_fail (updateObject (v :: cte) ko a b c)" - by (simp add: updateObject_cte typeError_def unless_def split: kernel_object.splits ) + by (fastforce simp: updateObject_cte typeError_def unless_def split: kernel_object.splits ) lemma empty_fail_setCTE [intro!, wp, simp]: "empty_fail (setCTE p cte)" unfolding setCTE_def - by (simp add: setObject_def split_def) + by (fastforce simp: setObject_def split_def) lemma empty_fail_updateCap [intro!, wp, simp]: "empty_fail (updateCap p f)" @@ -64,36 +64,35 @@ lemma empty_fail_updateMDB [intro!, wp, simp]: lemma empty_fail_getSlotCap [intro!, wp, simp]: "empty_fail (getSlotCap a)" - unfolding getSlotCap_def by simp + unfolding getSlotCap_def by fastforce context begin interpretation Arch . (*FIXME: arch_split*) lemma empty_fail_getObject: - assumes x: "(\b c d. empty_fail (loadObject x b c d::'a :: pspace_storable kernel))" + assumes "\b c d. empty_fail (loadObject x b c d::'a :: pspace_storable kernel)" shows "empty_fail (getObject x :: 'a :: pspace_storable kernel)" apply (simp add: getObject_def split_def) - apply (safe intro!: empty_fail_bind empty_fail_gets empty_fail_assert_opt) - apply (rule x) + apply (safe intro!: assms) done lemma empty_fail_updateTrackedFreeIndex [intro!, wp, simp]: shows "empty_fail (updateTrackedFreeIndex p idx)" - by (simp add: updateTrackedFreeIndex_def) + by (fastforce simp add: updateTrackedFreeIndex_def) lemma empty_fail_updateNewFreeIndex [intro!, wp, simp]: shows "empty_fail (updateNewFreeIndex p)" apply (simp add: updateNewFreeIndex_def) - apply (safe intro!: empty_fail_bind) + apply safe apply (simp split: capability.split) done lemma empty_fail_insertNewCap [intro!, wp, simp]: "empty_fail (insertNewCap p p' cap)" - unfolding insertNewCap_def by simp + unfolding insertNewCap_def by fastforce lemma empty_fail_getIRQSlot [intro!, wp, simp]: "empty_fail (getIRQSlot irq)" - by (simp add: getIRQSlot_def getInterruptState_def locateSlot_conv) + by (fastforce simp: getIRQSlot_def getInterruptState_def locateSlot_conv) lemma empty_fail_getObject_ntfn [intro!, wp, simp]: "empty_fail (getObject p :: Structures_H.notification kernel)" @@ -107,15 +106,15 @@ lemma empty_fail_lookupIPCBuffer [intro!, wp, simp]: "empty_fail (lookupIPCBuffer a b)" by (clarsimp simp: lookupIPCBuffer_def Let_def getThreadBufferSlot_def locateSlot_conv - split: capability.splits arch_capability.splits | wp | wpc)+ + split: capability.splits arch_capability.splits | wp | wpc | safe)+ lemma empty_fail_updateObject_default [intro!, wp, simp]: "empty_fail (updateObject_default v ko a b c)" - by (simp add: updateObject_default_def typeError_def unless_def split: kernel_object.splits ) + by (fastforce simp: updateObject_default_def typeError_def unless_def split: kernel_object.splits) lemma empty_fail_threadSet [intro!, wp, simp]: "empty_fail (threadSet f p)" - by (simp add: threadSet_def getObject_def setObject_def split_def) + by (fastforce simp: threadSet_def getObject_def setObject_def split_def) lemma empty_fail_getThreadState[iff]: "empty_fail (getThreadState t)" diff --git a/proof/refine/X64/EmptyFail_H.thy b/proof/refine/X64/EmptyFail_H.thy index f8aa4a890..274d1cc81 100644 --- a/proof/refine/X64/EmptyFail_H.thy +++ b/proof/refine/X64/EmptyFail_H.thy @@ -17,19 +17,19 @@ context begin interpretation Arch . (*FIXME: arch_split*) lemmas forM_empty_fail[intro!, wp, simp] = empty_fail_mapM[simplified forM_def[symmetric]] lemmas forM_x_empty_fail[intro!, wp, simp] = empty_fail_mapM_x[simplified forM_x_def[symmetric]] -lemmas forME_x_empty_fail[intro!, wp, simp] = mapME_x_empty_fail[simplified forME_x_def[symmetric]] +lemmas forME_x_empty_fail[intro!, wp, simp] = empty_fail_mapME_x[simplified forME_x_def[symmetric]] lemma withoutPreemption_empty_fail[intro!, wp, simp]: "empty_fail m \ empty_fail (withoutPreemption m)" - by (simp add: withoutPreemption_def) + by simp lemma withoutFailure_empty_fail[intro!, wp, simp]: "empty_fail m \ empty_fail (withoutFailure m)" - by (simp add: withoutFailure_def) + by simp lemma catchFailure_empty_fail[intro!, wp, simp]: "\ empty_fail f; \x. empty_fail (g x) \ \ empty_fail (catchFailure f g)" - by (simp add: catchFailure_def empty_fail_catch) + by (simp add: empty_fail_catch) lemma emptyOnFailure_empty_fail[intro!, wp, simp]: "empty_fail m \ empty_fail (emptyOnFailure m)" @@ -86,9 +86,6 @@ proof (induct arbitrary: s rule: resolveAddressBits.induct) lemmas resolveAddressBits_empty_fail[intro!, wp, simp] = resolveAddressBits_spec_empty_fail[THEN use_spec_empty_fail] -crunch (empty_fail) empty_fail[intro!, wp, simp]: lookupIPCBuffer -(simp:Let_def) - declare ef_dmo'[intro!, wp, simp] lemma empty_fail_getObject_ep [intro!, wp, simp]: @@ -179,7 +176,7 @@ crunch (empty_fail) "_H_empty_fail"[intro!, wp, simp]: "ThreadDecls_H.suspend" lemma ThreadDecls_H_restart_empty_fail[intro!, wp, simp]: "empty_fail (ThreadDecls_H.restart target)" - by (simp add:restart_def) + by (fastforce simp: restart_def) crunch (empty_fail) empty_fail[intro!, wp, simp]: finaliseCap, preemptionPoint, capSwapForDelete (wp: empty_fail_catch simp: Let_def) @@ -217,18 +214,14 @@ lemmas finaliseSlot_empty_fail[intro!, wp, simp] = lemma checkCapAt_empty_fail[intro!, wp, simp]: "empty_fail action \ empty_fail (checkCapAt cap ptr action)" - by (simp add: checkCapAt_def) + by (fastforce simp: checkCapAt_def) lemma assertDerived_empty_fail[intro!, wp, simp]: "empty_fail f \ empty_fail (assertDerived src cap f)" - by (simp add: assertDerived_def) + by (fastforce simp: assertDerived_def) crunch (empty_fail) empty_fail[intro!, wp, simp]: cteDelete -lemma liftE_empty_fail[intro!, wp, simp]: - "empty_fail f \ empty_fail (liftE f)" - by simp - lemma spec_empty_fail_unlessE': "\ \ P \ spec_empty_fail f s \ \ spec_empty_fail (unlessE P f) s" by (simp add:unlessE_def spec_empty_returnOk) @@ -258,7 +251,7 @@ lemma Syscall_H_syscall_empty_fail[intro!, wp, simp]: lemma catchError_empty_fail[intro!, wp, simp]: "\ empty_fail f; \x. empty_fail (g x) \ \ empty_fail (catchError f g)" - by (simp add: catchError_def handle_empty_fail) + by fastforce crunch (empty_fail) empty_fail[intro!, wp, simp]: chooseThread, getDomainTime, nextDomain, isHighestPrio @@ -275,11 +268,11 @@ crunch (empty_fail) empty_fail[wp, simp]: setMRs, setMessageInfo lemma empty_fail_portIn[intro!, wp, simp]: "empty_fail a \ empty_fail (portIn a)" - by (simp add: portIn_def) + by (fastforce simp: portIn_def) lemma empty_fail_portOut[intro!, wp, simp]: "empty_fail (w a) \ empty_fail (portOut w a)" - by (simp add: portOut_def) + by (fastforce simp: portOut_def) crunch (empty_fail) empty_fail: callKernel (wp: empty_fail_catch) diff --git a/proof/refine/X64/Finalise_R.thy b/proof/refine/X64/Finalise_R.thy index f109200b9..6e34b0f22 100644 --- a/proof/refine/X64/Finalise_R.thy +++ b/proof/refine/X64/Finalise_R.thy @@ -2545,11 +2545,12 @@ lemma deleteASID_invs'[wp]: apply (simp add: deleteASID_def cong: option.case_cong) apply (rule hoare_pre) apply (wp | wpc)+ - apply (rule_tac Q="\rv. valid_obj' (injectKO rv) and invs'" - in hoare_post_imp) + apply (rule_tac Q="\rv. valid_obj' (injectKO rv) and invs'" + in hoare_post_imp) + apply (rename_tac rv s) apply (clarsimp split: if_split_asm del: subsetI) apply (simp add: fun_upd_def[symmetric] valid_obj'_def) - apply (case_tac r, simp) + apply (case_tac rv, simp) apply (subst inv_f_f, rule inj_onI, simp)+ apply (rule conjI) apply clarsimp diff --git a/proof/refine/X64/IpcCancel_R.thy b/proof/refine/X64/IpcCancel_R.thy index 07211de1d..1c0bde487 100644 --- a/proof/refine/X64/IpcCancel_R.thy +++ b/proof/refine/X64/IpcCancel_R.thy @@ -699,12 +699,13 @@ lemma cancelSignal_invs': apply assumption apply (rule hoare_strengthen_post) apply (rule get_ntfn_sp') + apply (rename_tac rv s) apply (clarsimp simp: pred_tcb_at') apply (frule NIQ) apply (clarsimp simp: pred_tcb_at'_def obj_at'_def) apply (rule conjI) apply (clarsimp simp: valid_ntfn'_def) - apply (case_tac "ntfnObj r", simp_all add: isWaitingNtfn_def) + apply (case_tac "ntfnObj rv", simp_all add: isWaitingNtfn_def) apply (frule ko_at_valid_objs') apply (simp add: valid_pspace_valid_objs') apply (clarsimp simp: projectKO_opt_ntfn split: kernel_object.splits) @@ -727,7 +728,7 @@ lemma cancelSignal_invs': split: ntfn.splits) apply (rule conjI, clarsimp elim!: if_live_state_refsE) apply (fastforce simp: sym_refs_def dest!: idle'_no_refs) - apply (case_tac "ntfnObj r", simp_all) + apply (case_tac "ntfnObj rv", simp_all) apply (frule obj_at_valid_objs', clarsimp) apply (clarsimp simp: projectKOs valid_obj'_def valid_ntfn'_def) apply (rule conjI, clarsimp split: option.splits) @@ -2305,14 +2306,15 @@ lemma cancelAllIPC_invs'[wp]: prefer 2 apply assumption apply (rule hoare_strengthen_post [OF get_ep_sp']) + apply (rename_tac rv s) apply (clarsimp simp: invs'_def valid_state'_def valid_ep'_def) apply (frule obj_at_valid_objs', fastforce) apply (clarsimp simp: projectKOs valid_obj'_def) apply (rule conjI) - apply (case_tac r, simp_all add: valid_ep'_def)[1] + apply (case_tac rv, simp_all add: valid_ep'_def)[1] apply (rule conjI[rotated]) apply (drule(1) sym_refs_ko_atD') - apply (case_tac r, simp_all add: st_tcb_at_refs_of_rev')[1] + apply (case_tac rv, simp_all add: st_tcb_at_refs_of_rev')[1] apply (clarsimp elim!: if_live_state_refsE | drule(1) bspec | drule st_tcb_at_state_refs_ofD')+ apply (drule(2) ep_q_refs_max) diff --git a/proof/refine/X64/Schedule_R.thy b/proof/refine/X64/Schedule_R.thy index be2b80fa3..946b5f040 100644 --- a/proof/refine/X64/Schedule_R.thy +++ b/proof/refine/X64/Schedule_R.thy @@ -239,7 +239,7 @@ proof - simp add: valid_queues_def) apply (wp hoare_vcg_if_lift hoare_vcg_conj_lift hoare_vcg_imp_lift)+ apply (wp hoare_vcg_imp_lift setQueue_valid_queues_no_bitmap_except_dequeue_wp - setQueue_valid_bitmapQ threadGet_const_tcb_at)+ + setQueue_valid_bitmapQ threadGet_const_tcb_at hoare_vcg_if_lift)+ (* wp done *) apply (normalise_obj_at') apply (clarsimp simp: correct_queue_def) diff --git a/proof/refine/X64/Syscall_R.thy b/proof/refine/X64/Syscall_R.thy index 4a369719e..9d24c6ef8 100644 --- a/proof/refine/X64/Syscall_R.thy +++ b/proof/refine/X64/Syscall_R.thy @@ -2192,7 +2192,6 @@ lemma hi_IRQInactive: -, \\rv s. intStateIRQTable (ksInterruptState s) rv \ irqstate.IRQInactive\" apply (simp add: handleInvocation_def split_def) apply (wp syscall_valid' retype_pi_IRQInactive) - apply simp_all done lemma handleSend_IRQInactive: diff --git a/proof/refine/X64/TcbAcc_R.thy b/proof/refine/X64/TcbAcc_R.thy index fd80cc97e..f5903bd0b 100644 --- a/proof/refine/X64/TcbAcc_R.thy +++ b/proof/refine/X64/TcbAcc_R.thy @@ -14,7 +14,6 @@ declare if_weak_cong [cong] declare result_in_set_wp[wp] declare hoare_in_monad_post[wp] declare trans_state_update'[symmetric,simp] -declare empty_fail_sequence_x[simp] declare storeWordUser_typ_at' [wp] (* Auxiliaries and basic properties of priority bitmap functions *) diff --git a/proof/refine/X64/Tcb_R.thy b/proof/refine/X64/Tcb_R.thy index 6b456767a..51364be0a 100644 --- a/proof/refine/X64/Tcb_R.thy +++ b/proof/refine/X64/Tcb_R.thy @@ -2735,6 +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 apply (simp add: invokeTCB_def) apply (rule hoare_pre) apply (wpc | diff --git a/proof/refine/X64/Untyped_R.thy b/proof/refine/X64/Untyped_R.thy index 37af61887..f15c42d16 100644 --- a/proof/refine/X64/Untyped_R.thy +++ b/proof/refine/X64/Untyped_R.thy @@ -5823,8 +5823,7 @@ lemma inv_untyped_IRQInactive: "\valid_irq_states'\ invokeUntyped ui -, \\rv s. intStateIRQTable (ksInterruptState s) rv \ irqstate.IRQInactive\" apply (simp add: invokeUntyped_def) - apply (rule hoare_pre) - apply (wp whenE_wp resetUntypedCap_IRQInactive | wpc | simp)+ + apply (wpsimp wp: resetUntypedCap_IRQInactive) done end diff --git a/spec/capDL/Monads_D.thy b/spec/capDL/Monads_D.thy index 40e851457..48fe35b82 100644 --- a/spec/capDL/Monads_D.thy +++ b/spec/capDL/Monads_D.thy @@ -11,7 +11,8 @@ theory Monads_D imports Types_D - "Monads.NonDetMonadVCG" + Monads.In_Monad + Monads.NonDetMonadVCG begin (* Kernel state monad *) diff --git a/spec/design/m-skel/AARCH64/MachineTypes.thy b/spec/design/m-skel/AARCH64/MachineTypes.thy index 02fb89b8d..ed9ce4793 100644 --- a/spec/design/m-skel/AARCH64/MachineTypes.thy +++ b/spec/design/m-skel/AARCH64/MachineTypes.thy @@ -7,9 +7,11 @@ chapter "AARCH64 Machine Types" theory MachineTypes imports - "Word_Lib.WordSetup" - "Monads.OptionMonadND" - "Lib.HaskellLib_H" + Word_Lib.WordSetup + Monads.Empty_Fail + Monads.No_Fail + Monads.OptionMonadND + Lib.HaskellLib_H Platform begin diff --git a/spec/design/m-skel/ARM/MachineTypes.thy b/spec/design/m-skel/ARM/MachineTypes.thy index 7d3764c20..18b819ede 100644 --- a/spec/design/m-skel/ARM/MachineTypes.thy +++ b/spec/design/m-skel/ARM/MachineTypes.thy @@ -8,8 +8,10 @@ chapter "ARM Machine Types" theory MachineTypes imports - "Word_Lib.WordSetup" - "Monads.OptionMonadND" + Word_Lib.WordSetup + Monads.Empty_Fail + Monads.No_Fail + Monads.OptionMonadND Setup_Locale Platform begin diff --git a/spec/design/m-skel/ARM_HYP/MachineTypes.thy b/spec/design/m-skel/ARM_HYP/MachineTypes.thy index 09726ff9a..77e6f4fc8 100644 --- a/spec/design/m-skel/ARM_HYP/MachineTypes.thy +++ b/spec/design/m-skel/ARM_HYP/MachineTypes.thy @@ -8,8 +8,10 @@ chapter \ARM\_HYP Machine Types\ theory MachineTypes imports - "Word_Lib.WordSetup" - "Monads.OptionMonadND" + Word_Lib.WordSetup + Monads.Empty_Fail + Monads.No_Fail + Monads.OptionMonadND Setup_Locale Platform begin diff --git a/spec/design/m-skel/RISCV64/MachineTypes.thy b/spec/design/m-skel/RISCV64/MachineTypes.thy index 2375c2dbc..e4533a75a 100644 --- a/spec/design/m-skel/RISCV64/MachineTypes.thy +++ b/spec/design/m-skel/RISCV64/MachineTypes.thy @@ -8,9 +8,11 @@ chapter "RISCV 64bit Machine Types" theory MachineTypes imports - "Word_Lib.WordSetup" - "Monads.OptionMonadND" - "Lib.HaskellLib_H" + Word_Lib.WordSetup + Monads.Empty_Fail + Monads.No_Fail + Monads.OptionMonadND + Lib.HaskellLib_H Platform begin diff --git a/spec/design/m-skel/X64/MachineTypes.thy b/spec/design/m-skel/X64/MachineTypes.thy index c0fa7ac53..ea19e28b9 100644 --- a/spec/design/m-skel/X64/MachineTypes.thy +++ b/spec/design/m-skel/X64/MachineTypes.thy @@ -8,9 +8,11 @@ chapter "x86-64bit Machine Types" theory MachineTypes imports - "Word_Lib.WordSetup" - "Monads.OptionMonadND" - "Lib.HaskellLib_H" + Word_Lib.WordSetup + Monads.Empty_Fail + Monads.No_Fail + Monads.OptionMonadND + Lib.HaskellLib_H Platform begin diff --git a/sys-init/CreateObjects_SI.thy b/sys-init/CreateObjects_SI.thy index 4aa88a359..94ebae8fc 100644 --- a/sys-init/CreateObjects_SI.thy +++ b/sys-init/CreateObjects_SI.thy @@ -218,7 +218,8 @@ lemma retype_untyped_wp: (assumption|simp add: unat_of_nat32 |rule offset_slot' [symmetric] guard_equal_si_cnode_cap)+) apply clarsimp apply sep_solve - apply (case_tac r) + apply (rename_tac rv s) + apply (case_tac rv) apply clarsimp apply sep_solve apply clarsimp @@ -1109,7 +1110,7 @@ lemma retype_untyped_loop_inv_helper: apply (rule valid_rv_split) apply (fact retype_untyped_loop_inv_fail) apply (fact retype_untyped_loop_inv_success) - apply (case_tac r, simp_all) + apply (simp split: if_split_asm) done lemma nth_mem_sub: diff --git a/tools/autocorres/CorresXF.thy b/tools/autocorres/CorresXF.thy index c203cf080..8b052e8c3 100644 --- a/tools/autocorres/CorresXF.thy +++ b/tools/autocorres/CorresXF.thy @@ -249,7 +249,7 @@ lemma corresXF_join: apply (simp add: corresXF_simple_def split: sum.splits unit.splits) apply (clarsimp simp: NonDetMonad.lift_def throwError_def return_def) apply fastforce - apply (fastforce simp: NonDetMonad.validE_def split: sum.splits cong del: unit.case_cong) + apply (fastforce simp: NonDetMonadVCG.validE_def split: sum.splits cong del: unit.case_cong) apply simp done @@ -263,7 +263,7 @@ lemma corresXF_except: apply (simp add: corresXF_simple_def split: sum.splits unit.splits) apply (clarsimp simp: NonDetMonad.lift_def throwError_def return_def) apply fastforce - apply (clarsimp simp: NonDetMonad.validE_def split: sum.splits cong del: unit.case_cong) + apply (clarsimp simp: NonDetMonadVCG.validE_def split: sum.splits cong del: unit.case_cong) apply simp done diff --git a/tools/autocorres/ExceptionRewrite.thy b/tools/autocorres/ExceptionRewrite.thy index b40ae9952..556baae7c 100644 --- a/tools/autocorres/ExceptionRewrite.thy +++ b/tools/autocorres/ExceptionRewrite.thy @@ -58,12 +58,6 @@ lemma alwaysfail_noreturn: "always_fail P A \ no_return P A" lemma alwaysfail_nothrow: "always_fail P A \ no_throw P A" by (clarsimp simp: always_fail_def no_throw_def validE_def valid_def split: sum.splits) -lemma empty_fail_handleE: "\ empty_fail L; \r. empty_fail (R r) \ \ empty_fail (L R)" - apply (clarsimp simp: handleE_def handleE'_def) - apply (erule empty_fail_bind) - apply (clarsimp simp: empty_fail_error_bits split: sum.splits) - done - lemma no_return_bindE: "no_return (\_. True) A \ (A >>=E B) = A" apply (rule ext)+ @@ -120,20 +114,13 @@ lemma L1_condition_empty_fail: "\ empty_fail L; empty_fail R \ \ by (clarsimp simp: empty_fail_def L1_defs returnOk_def return_def split: condition_splits) lemma L1_seq_empty_fail: "\ empty_fail L; empty_fail R \ \ empty_fail (L1_seq L R)" - apply (clarsimp simp: L1_defs) - apply (erule (1) empty_fail_bindE) - done + by (clarsimp simp: L1_defs) lemma L1_catch_empty_fail: "\ empty_fail L; empty_fail R \ \ empty_fail (L1_catch L R)" - apply (clarsimp simp: L1_defs) - apply (erule (1) empty_fail_handleE) - done + by (clarsimp simp: L1_defs) lemma L1_while_empty_fail: "empty_fail B \ empty_fail (L1_while C B)" - apply (clarsimp simp: L1_while_def) - apply (rule empty_fail_whileLoopE) - apply simp - done + by (clarsimp simp: L1_while_def) (* * no_throw lemmas. diff --git a/tools/autocorres/tests/proof-tests/word_abs_options.thy b/tools/autocorres/tests/proof-tests/word_abs_options.thy index cc02f7b90..e6c326608 100644 --- a/tools/autocorres/tests/proof-tests/word_abs_options.thy +++ b/tools/autocorres/tests/proof-tests/word_abs_options.thy @@ -18,22 +18,22 @@ context word_abs_options begin lemma "\ \ \ isum1' (a :: sword32) (b :: sword32) \ \r _. r = a + b \" unfolding isum1'_def - apply (wp refl) + apply (wp refl impI) done lemma "\ \ \ isum2' (a :: int) (b :: int) \ \r _. r = a + b \" unfolding isum2'_def - apply (wp refl) + apply (wp refl impI) done lemma "\ \ \ usum1' (a :: word32) (b :: word32) \ \r _. r = a + b \" unfolding usum1'_def - apply (wp refl) + apply (wp refl impI) done lemma "\ \ \ usum2' (a :: nat) (b :: nat) \ \r _. r = a + b \" unfolding usum2'_def - apply (wp refl) + apply (wp refl impI) done end