From e721428d3414c242a16284a7ccd1952fd7c05489 Mon Sep 17 00:00:00 2001 From: Gerwin Klein Date: Tue, 21 Jan 2025 17:23:00 +1100 Subject: [PATCH] refine+crefine: remove valid_arch_mdb_ctes - replace the ioport_control invariant with archMDBAssertions - remove lemmas needed only for the invariant - add corresponding crossing lemmas for caps_of_state based on existing older cte_wp_at lemmas Signed-off-by: Gerwin Klein --- proof/crefine/AARCH64/CSpace_C.thy | 5 +- proof/crefine/AARCH64/Fastpath_C.thy | 2 + .../crefine/AARCH64/IsolatedThreadAction.thy | 17 +- proof/crefine/ARM/CSpace_C.thy | 3 +- proof/crefine/ARM/Fastpath_C.thy | 2 + proof/crefine/ARM/IsolatedThreadAction.thy | 17 +- proof/crefine/ARM_HYP/CSpace_C.thy | 3 +- proof/crefine/ARM_HYP/Fastpath_C.thy | 2 + .../crefine/ARM_HYP/IsolatedThreadAction.thy | 17 +- proof/crefine/RISCV64/ADT_C.thy | 2 +- proof/crefine/RISCV64/ArchMove_C.thy | 18 +- proof/crefine/RISCV64/CSpace_C.thy | 5 +- .../crefine/RISCV64/IsolatedThreadAction.thy | 16 +- proof/crefine/X64/CSpace_C.thy | 5 +- proof/crefine/X64/IsolatedThreadAction.thy | 17 +- proof/refine/AARCH64/ArchInvsDefs_H.thy | 3 - proof/refine/AARCH64/Arch_R.thy | 9 +- proof/refine/AARCH64/CNodeInv_R.thy | 3 - proof/refine/AARCH64/CSpace1_R.thy | 94 +++++--- proof/refine/AARCH64/CSpace_R.thy | 36 +-- proof/refine/AARCH64/Interrupt_R.thy | 3 + proof/refine/AARCH64/InvariantUpdates_H.thy | 6 - proof/refine/AARCH64/Ipc_R.thy | 50 +++-- proof/refine/AARCH64/Tcb_R.thy | 2 +- proof/refine/ARM/ArchInvsDefs_H.thy | 3 - proof/refine/ARM/Arch_R.thy | 9 +- proof/refine/ARM/CNodeInv_R.thy | 3 - proof/refine/ARM/CSpace1_R.thy | 94 +++++--- proof/refine/ARM/CSpace_R.thy | 37 +-- proof/refine/ARM/Interrupt_R.thy | 3 + proof/refine/ARM/InvariantUpdates_H.thy | 6 - proof/refine/ARM/Ipc_R.thy | 50 +++-- proof/refine/ARM/Tcb_R.thy | 2 +- proof/refine/ARM_HYP/ArchInvsDefs_H.thy | 3 - proof/refine/ARM_HYP/Arch_R.thy | 9 +- proof/refine/ARM_HYP/CNodeInv_R.thy | 3 - proof/refine/ARM_HYP/CSpace1_R.thy | 94 +++++--- proof/refine/ARM_HYP/CSpace_R.thy | 37 +-- proof/refine/ARM_HYP/Interrupt_R.thy | 3 + proof/refine/ARM_HYP/InvariantUpdates_H.thy | 6 - proof/refine/ARM_HYP/Ipc_R.thy | 50 +++-- proof/refine/ARM_HYP/Tcb_R.thy | 2 +- proof/refine/Invariants_H.thy | 8 +- proof/refine/RISCV64/ArchInvsDefs_H.thy | 3 - proof/refine/RISCV64/Arch_R.thy | 9 +- proof/refine/RISCV64/CNodeInv_R.thy | 3 - proof/refine/RISCV64/CSpace1_R.thy | 94 +++++--- proof/refine/RISCV64/CSpace_R.thy | 36 +-- proof/refine/RISCV64/Interrupt_R.thy | 3 + proof/refine/RISCV64/InvariantUpdates_H.thy | 6 - proof/refine/RISCV64/Ipc_R.thy | 50 +++-- proof/refine/RISCV64/Tcb_R.thy | 2 +- proof/refine/X64/ArchInvsDefs_H.thy | 12 - proof/refine/X64/ArchInvsLemmas_H.thy | 9 - proof/refine/X64/Arch_R.thy | 17 +- proof/refine/X64/CNodeInv_R.thy | 80 +------ proof/refine/X64/CSpace1_R.thy | 211 +++++++++--------- proof/refine/X64/CSpace_I.thy | 38 +--- proof/refine/X64/CSpace_R.thy | 164 +++----------- proof/refine/X64/Detype_R.thy | 5 - proof/refine/X64/Finalise_R.thy | 13 -- proof/refine/X64/Interrupt_R.thy | 19 +- proof/refine/X64/Ipc_R.thy | 50 +++-- proof/refine/X64/Retype_R.thy | 11 +- proof/refine/X64/Tcb_R.thy | 2 +- proof/refine/X64/Untyped_R.thy | 8 - 66 files changed, 823 insertions(+), 781 deletions(-) diff --git a/proof/crefine/AARCH64/CSpace_C.thy b/proof/crefine/AARCH64/CSpace_C.thy index f3cc296f8e..2d4ecb29b8 100644 --- a/proof/crefine/AARCH64/CSpace_C.thy +++ b/proof/crefine/AARCH64/CSpace_C.thy @@ -985,8 +985,9 @@ lemma cteInsert_ccorres: (Call cteInsert_'proc)" supply ctes_of_aligned_bits[simp] apply (cinit (no_ignore_call) lift: destSlot_' srcSlot_' newCap_' - simp del: return_bind simp add: Collect_const) + simp del: return_bind simp add: Collect_const) apply (rule ccorres_move_c_guard_cte) + apply (rule ccorres_stateAssert) apply (ctac pre: ccorres_pre_getCTE) apply (rule ccorres_move_c_guard_cte) apply (ctac pre: ccorres_pre_getCTE) @@ -1040,7 +1041,7 @@ lemma cteInsert_ccorres: apply (frule valid_cap_untyped_inv) apply clarsimp apply (rule conjI) - apply (case_tac ctea) + apply (case_tac cte) apply (clarsimp simp: isUntypedCap_def split: capability.splits) apply (frule valid_cap_untyped_inv[OF ctes_of_valid_cap']) apply fastforce diff --git a/proof/crefine/AARCH64/Fastpath_C.thy b/proof/crefine/AARCH64/Fastpath_C.thy index 18fe506b69..a8dacac7fa 100644 --- a/proof/crefine/AARCH64/Fastpath_C.thy +++ b/proof/crefine/AARCH64/Fastpath_C.thy @@ -2279,6 +2279,7 @@ proof - apply (rule ccorres_assert2) apply (rule ccorres_pre_threadGet, rename_tac destState) apply (rule_tac P="isReceive destState" in ccorres_gen_asm) + apply (rule ccorres_stateAssert) apply (rule ccorres_pre_getCTE2, rename_tac curThreadReplyCTE2) apply (rule ccorres_pre_getCTE2, rename_tac destCallerCTE) apply (rule ccorres_assert2)+ @@ -2449,6 +2450,7 @@ proof - apply (rule conseqPre, vcg, clarsimp) apply (simp add: cte_level_bits_def field_simps shiftl_t2n ctes_of_Some_cte_wp_at + archMDBAssertions_def del: all_imp_to_ex cong: imp_cong conj_cong) apply (wp hoare_vcg_all_lift threadSet_ctes_of hoare_vcg_imp_lift' threadSet_valid_objs' diff --git a/proof/crefine/AARCH64/IsolatedThreadAction.thy b/proof/crefine/AARCH64/IsolatedThreadAction.thy index ea26491a83..82b47cc01f 100644 --- a/proof/crefine/AARCH64/IsolatedThreadAction.thy +++ b/proof/crefine/AARCH64/IsolatedThreadAction.thy @@ -1528,6 +1528,20 @@ lemma setCTE_isolatable: apply (clarsimp simp: obj_at'_def projectKOs) done +lemma archMDBAssertions_isolatable: + "thread_actions_isolatable idx (stateAssert archMDBAssertions [])" + unfolding stateAssert_def archMDBAssertions_def + apply (clarsimp simp: thread_actions_isolatable_def) + apply (simp add: isolate_thread_actions_def bind_assoc split_def) + apply (simp add: bind_select_f_bind[symmetric] select_f_returns) + apply (clarsimp simp: monadic_rewrite_def exec_gets getSchedulerAction_def + map_to_ctes_partial_overwrite) + apply (simp add: select_f_asserts) + apply (clarsimp simp: exec_modify o_def return_def) + apply (simp add: ksPSpace_update_partial_id) + apply (simp add: return_def fail_def modify_def get_def put_def assert_def bind_def) + done + lemma cteInsert_isolatable: "thread_actions_isolatable idx (cteInsert cap src dest)" supply if_split[split del] if_cong[cong] @@ -1536,7 +1550,8 @@ lemma cteInsert_isolatable: apply (intro thread_actions_isolatable_bind[OF _ _ hoare_weaken_pre] thread_actions_isolatable_if thread_actions_isolatable_returns - getCTE_isolatable setCTE_isolatable) + getCTE_isolatable setCTE_isolatable + archMDBAssertions_isolatable) apply (wp | simp)+ done diff --git a/proof/crefine/ARM/CSpace_C.thy b/proof/crefine/ARM/CSpace_C.thy index 84d0b1f044..792d3a2e0c 100644 --- a/proof/crefine/ARM/CSpace_C.thy +++ b/proof/crefine/ARM/CSpace_C.thy @@ -1010,6 +1010,7 @@ lemma cteInsert_ccorres: simp del: return_bind simp add: Collect_const) apply (rule ccorres_move_c_guard_cte) + apply (rule ccorres_stateAssert) apply (ctac pre: ccorres_pre_getCTE) apply (rule ccorres_move_c_guard_cte) apply (ctac pre: ccorres_pre_getCTE) @@ -1063,7 +1064,7 @@ lemma cteInsert_ccorres: apply (frule valid_cap_untyped_inv) apply clarsimp apply (rule conjI) - apply (case_tac ctea) + apply (case_tac cte) apply (clarsimp simp: isUntypedCap_def split: capability.splits) apply (frule valid_cap_untyped_inv[OF ctes_of_valid_cap']) apply fastforce diff --git a/proof/crefine/ARM/Fastpath_C.thy b/proof/crefine/ARM/Fastpath_C.thy index 6e14968108..48ecb62ebc 100644 --- a/proof/crefine/ARM/Fastpath_C.thy +++ b/proof/crefine/ARM/Fastpath_C.thy @@ -2083,6 +2083,7 @@ proof - apply (rule ccorres_assert2) apply (rule ccorres_pre_threadGet, rename_tac destState) apply (rule_tac P="isReceive destState" in ccorres_gen_asm) + apply (rule ccorres_stateAssert) apply (rule ccorres_pre_getCTE2, rename_tac curThreadReplyCTE2) apply (rule ccorres_pre_getCTE2, rename_tac destCallerCTE) apply (rule ccorres_assert2)+ @@ -2246,6 +2247,7 @@ proof - apply (rule conseqPre, vcg, clarsimp) apply (simp add: cte_level_bits_def field_simps shiftl_t2n ctes_of_Some_cte_wp_at + archMDBAssertions_def del: all_imp_to_ex cong: imp_cong conj_cong) apply (wp hoare_vcg_all_lift threadSet_ctes_of hoare_vcg_imp_lift' threadSet_valid_objs' diff --git a/proof/crefine/ARM/IsolatedThreadAction.thy b/proof/crefine/ARM/IsolatedThreadAction.thy index 4f54066de2..61b7d713fb 100644 --- a/proof/crefine/ARM/IsolatedThreadAction.thy +++ b/proof/crefine/ARM/IsolatedThreadAction.thy @@ -1141,6 +1141,20 @@ lemma assert_isolatable: thread_actions_isolatable_returns thread_actions_isolatable_fail) +lemma archMDBAssertions_isolatable: + "thread_actions_isolatable idx (stateAssert archMDBAssertions [])" + unfolding stateAssert_def archMDBAssertions_def + apply (clarsimp simp: thread_actions_isolatable_def) + apply (simp add: isolate_thread_actions_def bind_assoc split_def) + apply (simp add: bind_select_f_bind[symmetric] select_f_returns) + apply (clarsimp simp: monadic_rewrite_def exec_gets getSchedulerAction_def + map_to_ctes_partial_overwrite) + apply (simp add: select_f_asserts) + apply (clarsimp simp: exec_modify o_def return_def) + apply (simp add: ksPSpace_update_partial_id) + apply (simp add: return_def fail_def modify_def get_def put_def assert_def bind_def) + done + lemma cteInsert_isolatable: "thread_actions_isolatable idx (cteInsert cap src dest)" supply if_split[split del] if_cong[cong] @@ -1149,7 +1163,8 @@ lemma cteInsert_isolatable: apply (intro thread_actions_isolatable_bind[OF _ _ hoare_weaken_pre] thread_actions_isolatable_if thread_actions_isolatable_returns assert_isolatable - getCTE_isolatable setCTE_isolatable) + getCTE_isolatable setCTE_isolatable + archMDBAssertions_isolatable) apply (wp | simp)+ done diff --git a/proof/crefine/ARM_HYP/CSpace_C.thy b/proof/crefine/ARM_HYP/CSpace_C.thy index b7029f9449..e7abb000ef 100644 --- a/proof/crefine/ARM_HYP/CSpace_C.thy +++ b/proof/crefine/ARM_HYP/CSpace_C.thy @@ -1050,6 +1050,7 @@ lemma cteInsert_ccorres: simp del: return_bind simp add: Collect_const) apply (rule ccorres_move_c_guard_cte) + apply (rule ccorres_stateAssert) apply (ctac pre: ccorres_pre_getCTE) apply (rule ccorres_move_c_guard_cte) apply (ctac pre: ccorres_pre_getCTE) @@ -1103,7 +1104,7 @@ lemma cteInsert_ccorres: apply (frule valid_cap_untyped_inv) apply clarsimp apply (rule conjI) - apply (case_tac ctea) + apply (case_tac cte) apply (clarsimp simp: isUntypedCap_def split: capability.splits) apply (frule valid_cap_untyped_inv[OF ctes_of_valid_cap']) apply fastforce diff --git a/proof/crefine/ARM_HYP/Fastpath_C.thy b/proof/crefine/ARM_HYP/Fastpath_C.thy index 5ba460dc59..e7c9912ba5 100644 --- a/proof/crefine/ARM_HYP/Fastpath_C.thy +++ b/proof/crefine/ARM_HYP/Fastpath_C.thy @@ -2129,6 +2129,7 @@ proof - apply (rule ccorres_assert2) apply (rule ccorres_pre_threadGet, rename_tac destState) apply (rule_tac P="isReceive destState" in ccorres_gen_asm) + apply (rule ccorres_stateAssert) apply (rule ccorres_pre_getCTE2, rename_tac curThreadReplyCTE2) apply (rule ccorres_pre_getCTE2, rename_tac destCallerCTE) apply (rule ccorres_assert2)+ @@ -2290,6 +2291,7 @@ proof - apply (rule conseqPre, vcg, clarsimp) apply (simp add: cte_level_bits_def field_simps shiftl_t2n ctes_of_Some_cte_wp_at + archMDBAssertions_def del: all_imp_to_ex cong: imp_cong conj_cong) apply (wp hoare_vcg_all_lift threadSet_ctes_of hoare_vcg_imp_lift' threadSet_valid_objs' diff --git a/proof/crefine/ARM_HYP/IsolatedThreadAction.thy b/proof/crefine/ARM_HYP/IsolatedThreadAction.thy index 9b2c5fd10e..e71ebcaebf 100644 --- a/proof/crefine/ARM_HYP/IsolatedThreadAction.thy +++ b/proof/crefine/ARM_HYP/IsolatedThreadAction.thy @@ -1416,6 +1416,20 @@ lemma assert_isolatable: thread_actions_isolatable_returns thread_actions_isolatable_fail) +lemma archMDBAssertions_isolatable: + "thread_actions_isolatable idx (stateAssert archMDBAssertions [])" + unfolding stateAssert_def archMDBAssertions_def + apply (clarsimp simp: thread_actions_isolatable_def) + apply (simp add: isolate_thread_actions_def bind_assoc split_def) + apply (simp add: bind_select_f_bind[symmetric] select_f_returns) + apply (clarsimp simp: monadic_rewrite_def exec_gets getSchedulerAction_def + map_to_ctes_partial_overwrite) + apply (simp add: select_f_asserts) + apply (clarsimp simp: exec_modify o_def return_def) + apply (simp add: ksPSpace_update_partial_id) + apply (simp add: return_def fail_def modify_def get_def put_def assert_def bind_def) + done + lemma cteInsert_isolatable: "thread_actions_isolatable idx (cteInsert cap src dest)" supply if_split[split del] if_cong[cong] @@ -1424,7 +1438,8 @@ lemma cteInsert_isolatable: apply (intro thread_actions_isolatable_bind[OF _ _ hoare_weaken_pre] thread_actions_isolatable_if thread_actions_isolatable_returns assert_isolatable - getCTE_isolatable setCTE_isolatable) + getCTE_isolatable setCTE_isolatable + archMDBAssertions_isolatable) apply (wp | simp)+ done diff --git a/proof/crefine/RISCV64/ADT_C.thy b/proof/crefine/RISCV64/ADT_C.thy index b1ab7d123b..faeca60f76 100644 --- a/proof/crefine/RISCV64/ADT_C.thy +++ b/proof/crefine/RISCV64/ADT_C.thy @@ -1215,7 +1215,7 @@ lemma ksPSpace_eq_imp_valid_pspace'_eq: assumes ksPSpace: "ksPSpace s' = ksPSpace s" shows "valid_pspace' s = valid_pspace' s'" using assms - by (clarsimp simp: valid_pspace'_def pspace_aligned'_def + by (clarsimp simp: valid_pspace'_def pspace_aligned'_def pspace_in_kernel_mappings'_def pspace_distinct'_def ps_clear_def no_0_obj'_def valid_mdb'_def pspace_canonical'_def pspace_in_kernel_mappings'_def ksPSpace_eq_imp_valid_objs'_eq[OF ksPSpace]) diff --git a/proof/crefine/RISCV64/ArchMove_C.thy b/proof/crefine/RISCV64/ArchMove_C.thy index d8af0372e4..c990bef195 100644 --- a/proof/crefine/RISCV64/ArchMove_C.thy +++ b/proof/crefine/RISCV64/ArchMove_C.thy @@ -33,15 +33,6 @@ lemma ps_clear_is_aligned_ksPSpace_None: context Arch begin arch_global_naming -lemma ps_clear_is_aligned_ctes_None: - assumes "ps_clear p tcbBlockSizeBits s" - and "is_aligned p tcbBlockSizeBits" - shows "ksPSpace s (p + 2*2^cteSizeBits) = None" - and "ksPSpace s (p + 3*2^cteSizeBits) = None" - and "ksPSpace s (p + 4*2^cteSizeBits) = None" - by (auto intro: assms ps_clear_is_aligned_ksPSpace_None - simp: objBits_defs mask_def)+ - lemma word_shift_by_3: "x * 8 = (x::'a::len word) << 3" by (simp add: shiftl_t2n) @@ -75,6 +66,15 @@ where (* FIXME: move to GenericLib *) lemmas unat64_eq_of_nat = unat_eq_of_nat[where 'a=64, folded word_bits_def] +lemma ps_clear_is_aligned_ctes_None: + assumes "ps_clear p tcbBlockSizeBits s" + and "is_aligned p tcbBlockSizeBits" + shows "ksPSpace s (p + 2*2^cteSizeBits) = None" + and "ksPSpace s (p + 3*2^cteSizeBits) = None" + and "ksPSpace s (p + 4*2^cteSizeBits) = None" + by (auto intro: assms ps_clear_is_aligned_ksPSpace_None + simp: objBits_defs mask_def)+ + crunch archThreadGet for inv'[wp]: P diff --git a/proof/crefine/RISCV64/CSpace_C.thy b/proof/crefine/RISCV64/CSpace_C.thy index aca185a59c..2972c840b3 100644 --- a/proof/crefine/RISCV64/CSpace_C.thy +++ b/proof/crefine/RISCV64/CSpace_C.thy @@ -994,8 +994,9 @@ lemma cteInsert_ccorres: (Call cteInsert_'proc)" supply ctes_of_aligned_bits[simp] apply (cinit (no_ignore_call) lift: destSlot_' srcSlot_' newCap_' - simp del: return_bind simp add: Collect_const) + simp del: return_bind simp add: Collect_const) apply (rule ccorres_move_c_guard_cte) + apply (rule ccorres_stateAssert) apply (ctac pre: ccorres_pre_getCTE) apply (rule ccorres_move_c_guard_cte) apply (ctac pre: ccorres_pre_getCTE) @@ -1049,7 +1050,7 @@ lemma cteInsert_ccorres: apply (frule valid_cap_untyped_inv) apply clarsimp apply (rule conjI) - apply (case_tac ctea) + apply (case_tac cte) apply (clarsimp simp: isUntypedCap_def split: capability.splits) apply (frule valid_cap_untyped_inv[OF ctes_of_valid_cap']) apply fastforce diff --git a/proof/crefine/RISCV64/IsolatedThreadAction.thy b/proof/crefine/RISCV64/IsolatedThreadAction.thy index 5d39d64dc0..de9fe4cc6f 100644 --- a/proof/crefine/RISCV64/IsolatedThreadAction.thy +++ b/proof/crefine/RISCV64/IsolatedThreadAction.thy @@ -1177,13 +1177,27 @@ lemma assert_isolatable: thread_actions_isolatable_returns thread_actions_isolatable_fail) +lemma archMDBAssertions_isolatable: + "thread_actions_isolatable idx (stateAssert archMDBAssertions [])" + unfolding stateAssert_def archMDBAssertions_def + apply (clarsimp simp: thread_actions_isolatable_def) + apply (simp add: isolate_thread_actions_def bind_assoc split_def) + apply (simp add: bind_select_f_bind[symmetric] select_f_returns) + apply (clarsimp simp: monadic_rewrite_def exec_gets getSchedulerAction_def + map_to_ctes_partial_overwrite) + apply (simp add: select_f_asserts) + apply (clarsimp simp: exec_modify o_def return_def) + apply (simp add: ksPSpace_update_partial_id) + apply (simp add: return_def fail_def modify_def get_def put_def assert_def bind_def) + done + lemma cteInsert_isolatable: "thread_actions_isolatable idx (cteInsert cap src dest)" supply if_split[split del] if_cong[cong] apply (simp add: cteInsert_def updateCap_def updateMDB_def Let_def setUntypedCapAsFull_def) apply (intro thread_actions_isolatable_bind[OF _ _ hoare_weaken_pre] - thread_actions_isolatable_if + thread_actions_isolatable_if archMDBAssertions_isolatable thread_actions_isolatable_returns assert_isolatable getCTE_isolatable setCTE_isolatable) apply (wp | simp)+ diff --git a/proof/crefine/X64/CSpace_C.thy b/proof/crefine/X64/CSpace_C.thy index e8b39a5233..f7b50972dc 100644 --- a/proof/crefine/X64/CSpace_C.thy +++ b/proof/crefine/X64/CSpace_C.thy @@ -1020,8 +1020,9 @@ lemma cteInsert_ccorres: (Call cteInsert_'proc)" supply ctes_of_aligned_bits[simp] apply (cinit (no_ignore_call) lift: destSlot_' srcSlot_' newCap_' - simp del: return_bind simp add: Collect_const) + simp del: return_bind simp add: Collect_const) apply (rule ccorres_move_c_guard_cte) + apply (rule ccorres_stateAssert) apply (ctac pre: ccorres_pre_getCTE) apply (rule ccorres_move_c_guard_cte) apply (ctac pre: ccorres_pre_getCTE) @@ -1075,7 +1076,7 @@ lemma cteInsert_ccorres: apply (frule valid_cap_untyped_inv) apply clarsimp apply (rule conjI) - apply (case_tac ctea) + apply (case_tac cte) apply (clarsimp simp: isUntypedCap_def split: capability.splits) apply (frule valid_cap_untyped_inv[OF ctes_of_valid_cap']) apply fastforce diff --git a/proof/crefine/X64/IsolatedThreadAction.thy b/proof/crefine/X64/IsolatedThreadAction.thy index 53b98565d6..f2a11252e8 100644 --- a/proof/crefine/X64/IsolatedThreadAction.thy +++ b/proof/crefine/X64/IsolatedThreadAction.thy @@ -1167,6 +1167,20 @@ lemma assert_isolatable: thread_actions_isolatable_returns thread_actions_isolatable_fail) +lemma archMDBAssertions_isolatable: + "thread_actions_isolatable idx (stateAssert archMDBAssertions [])" + unfolding stateAssert_def archMDBAssertions_def + apply (clarsimp simp: thread_actions_isolatable_def) + apply (simp add: isolate_thread_actions_def bind_assoc split_def) + apply (simp add: bind_select_f_bind[symmetric] select_f_returns) + apply (clarsimp simp: monadic_rewrite_def exec_gets getSchedulerAction_def + map_to_ctes_partial_overwrite) + apply (simp add: select_f_asserts) + apply (clarsimp simp: exec_modify o_def return_def) + apply (simp add: ksPSpace_update_partial_id) + apply (simp add: return_def fail_def modify_def get_def put_def assert_def bind_def) + done + lemma cteInsert_isolatable: "thread_actions_isolatable idx (cteInsert cap src dest)" supply if_split[split del] if_cong[cong] @@ -1175,7 +1189,8 @@ lemma cteInsert_isolatable: apply (intro thread_actions_isolatable_bind[OF _ _ hoare_weaken_pre] thread_actions_isolatable_if thread_actions_isolatable_returns assert_isolatable - getCTE_isolatable setCTE_isolatable) + getCTE_isolatable setCTE_isolatable + archMDBAssertions_isolatable) apply (wp | simp)+ done diff --git a/proof/refine/AARCH64/ArchInvsDefs_H.thy b/proof/refine/AARCH64/ArchInvsDefs_H.thy index 50072fabbb..8af60d4e36 100644 --- a/proof/refine/AARCH64/ArchInvsDefs_H.thy +++ b/proof/refine/AARCH64/ArchInvsDefs_H.thy @@ -200,9 +200,6 @@ definition where "isArchFrameCap cap \ case cap of ArchObjectCap (FrameCap _ _ _ _ _) \ True | _ \ False" -definition valid_arch_mdb_ctes :: "cte_heap \ bool" where - "valid_arch_mdb_ctes \ \" - (* Addresses of all PTEs in a VSRoot table at p *) definition table_refs' :: "machine_word \ machine_word set" where "table_refs' p \ (\i. p + (i << pte_bits)) ` mask_range 0 (ptTranslationBits VSRootPT_T)" diff --git a/proof/refine/AARCH64/Arch_R.thy b/proof/refine/AARCH64/Arch_R.thy index ff4072cd66..30cb21d78e 100644 --- a/proof/refine/AARCH64/Arch_R.thy +++ b/proof/refine/AARCH64/Arch_R.thy @@ -143,6 +143,7 @@ lemma performASIDControlInvocation_corres: apply (cases i) apply (rename_tac word1 prod1 prod2 word2) apply (clarsimp simp: asid_ci_map_def) + apply (rename_tac p slot p' slot' word2) apply (simp add: perform_asid_control_invocation_def placeNewObject_def2 performASIDControlInvocation_def) apply (rule corres_name_pre) @@ -195,7 +196,7 @@ lemma performASIDControlInvocation_corres: apply wp+ apply (strengthen safe_parent_strg[where idx = "2^pageBits"]) apply (strengthen invs_valid_objs invs_distinct - invs_psp_aligned invs_mdb + invs_psp_aligned invs_mdb invs_arch_state | simp cong:conj_cong)+ apply (wp retype_region_plain_invs[where sz = pageBits] retype_cte_wp_at[where sz = pageBits])+ @@ -279,7 +280,7 @@ lemma performASIDControlInvocation_corres: apply (drule detype_locale.non_null_present) apply (fastforce simp: cte_wp_at_caps_of_state) apply simp - apply (frule_tac ptr = "(aa,ba)" in detype_invariants [rotated 3]) + apply (frule_tac ptr = "(p', slot')" in detype_invariants [rotated 3]) apply fastforce apply simp apply (simp add: cte_wp_at_caps_of_state) @@ -304,7 +305,7 @@ lemma performASIDControlInvocation_corres: apply (simp add:detype_clear_um_independent) apply (rule conjI) apply clarsimp - apply (drule_tac p = "(aa,ba)" in cap_refs_in_kernel_windowD2[OF caps_of_state_cteD]) + apply (drule_tac p = "(p', slot')" in cap_refs_in_kernel_windowD2[OF caps_of_state_cteD]) apply fastforce apply (clarsimp simp: region_in_kernel_window_def valid_cap_def cap_aligned_def is_aligned_neg_mask_eq detype_def clear_um_def) @@ -319,7 +320,7 @@ lemma performASIDControlInvocation_corres: st_tcb_at_kh_def obj_at_kh_def st_tcb_at_def obj_at_def is_etcb_at_def wrap_ext_det_ext_ext_def) apply (simp add: detype_def clear_um_def) - apply (drule_tac x = "cte_map (aa,ba)" in pspace_relation_cte_wp_atI[OF state_relation_pspace_relation]) + apply (drule_tac x = "cte_map (p', slot')" in pspace_relation_cte_wp_atI[OF state_relation_pspace_relation]) apply (simp add:invs_valid_objs)+ apply clarsimp apply (drule cte_map_inj_eq) diff --git a/proof/refine/AARCH64/CNodeInv_R.thy b/proof/refine/AARCH64/CNodeInv_R.thy index 7be1e991d8..aead729009 100644 --- a/proof/refine/AARCH64/CNodeInv_R.thy +++ b/proof/refine/AARCH64/CNodeInv_R.thy @@ -8398,9 +8398,6 @@ proof apply (erule (1) irq_controlD, rule irq_control) done - show "valid_arch_mdb_ctes m'" - by simp - have distz: "distinct_zombies m" using valid by (simp add: valid_mdb_ctes_def) diff --git a/proof/refine/AARCH64/CSpace1_R.thy b/proof/refine/AARCH64/CSpace1_R.thy index 322e8b604c..0305fcbacf 100644 --- a/proof/refine/AARCH64/CSpace1_R.thy +++ b/proof/refine/AARCH64/CSpace1_R.thy @@ -14,6 +14,20 @@ imports CSpace_I begin +context Arch begin arch_global_naming + +(* No assertion necessary for this architecture. *) +definition arch_mdb_assert :: "cte_heap \ bool" where + "arch_mdb_assert m \ True" + +end + +arch_requalify_consts + arch_mdb_assert + +defs archMDBAssertions_def: + "archMDBAssertions s \ arch_mdb_assert (ctes_of s)" + context Arch begin global_naming AARCH64_A (*FIXME: arch-split*) lemmas final_matters_def = final_matters_def[simplified final_matters_arch_def] @@ -248,7 +262,7 @@ lemma pspace_relation_cte_wp_at: lemma pspace_relation_ctes_ofI: "\ pspace_relation (kheap s) (ksPSpace s'); - cte_wp_at ((=) c) slot s; pspace_aligned' s'; + cte_wp_at ((=) c) slot s; pspace_aligned' s'; pspace_distinct' s' \ \ \cte. ctes_of s' (cte_map slot) = Some cte \ cap_relation c (cteCap cte)" apply (cases slot, clarsimp) @@ -256,6 +270,22 @@ lemma pspace_relation_ctes_ofI: apply (simp add: cte_wp_at_ctes_of) done +lemma pspace_relation_caps_of_state_cross: + "\ pspace_relation (kheap s) (ksPSpace s'); + caps_of_state s slot = Some c; pspace_aligned s; pspace_distinct s \ + \ \cte. ctes_of s' (cte_map slot) = Some cte \ cap_relation c (cteCap cte)" + for s' :: kernel_state + by (auto simp: cte_wp_at_caps_of_state + intro!: pspace_relation_ctes_ofI pspace_aligned_cross pspace_distinct_cross) + +lemma caps_of_state_cross: + "\ caps_of_state s slot = Some cap; pspace_aligned s; pspace_distinct s; (s,s') \ state_relation \ + \ \cap'. cteCaps_of s' (cte_map slot) = Some cap' \ cap_relation cap cap'" + apply (erule state_relationE) + apply (drule (3) pspace_relation_caps_of_state_cross) + apply (fastforce simp: cteCaps_of_def) + done + lemma get_cap_corres_P: "corres (\x y. cap_relation x (cteCap y) \ P x) (cte_wp_at P cslot_ptr) @@ -912,21 +942,13 @@ lemma ctes_of_valid_cap'': done lemma cap_insert_objs' [wp]: - "\valid_objs' - and valid_cap' cap\ - cteInsert cap src dest \\rv. valid_objs'\" - including no_pre - apply (simp add: cteInsert_def updateCap_def setUntypedCapAsFull_def bind_assoc split del: if_split) - apply (wp setCTE_valid_objs) - apply simp - apply wp+ - apply (clarsimp simp: updateCap_def) - apply (wp|simp)+ - apply (rule hoare_drop_imp)+ - apply wp+ - apply (rule hoare_strengthen_post[OF getCTE_sp]) + "\valid_objs' and valid_cap' cap\ + cteInsert cap src dest + \\_. valid_objs'\" + apply (simp add: cteInsert_def updateCap_def setUntypedCapAsFull_def) + apply (wpsimp wp: setCTE_valid_objs | wp getCTE_wp')+ apply (clarsimp simp: cte_wp_at_ctes_of isCap_simps - dest!: ctes_of_valid_cap'') + dest!: ctes_of_valid_cap'') done lemma cteInsert_weak_cte_wp_at: @@ -1964,6 +1986,14 @@ lemma pspace_relation_cte_wp_atI: apply assumption done +lemma caps_of_state_rev_cross: + "\ ctes_of s' p = Some cte; valid_objs s; (s,s') \ state_relation \ + \ \cap slot. caps_of_state s slot = Some cap \ p = cte_map slot \ cap_relation cap (cteCap cte)" + apply (erule state_relationE) + apply (drule (2) pspace_relation_cte_wp_atI) + apply (fastforce simp: cte_wp_at_caps_of_state) + done + lemma sameRegion_corres: "\ sameRegionAs c' d'; cap_relation c c'; cap_relation d d' \ \ same_region_as c d" @@ -5195,6 +5225,15 @@ lemma cte_map_inj_eq': done context begin interpretation Arch . (*FIXME: arch-split*) + +(* interface lemma: generic statement, arch-specific proof *) +lemma archMDBAssertions_cross: + "\ valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_arch_state s; valid_objs s; + (s, s') \ state_relation \ + \ archMDBAssertions s'" + unfolding archMDBAssertions_def + by (simp add: arch_mdb_assert_def) + lemma cteInsert_corres: notes split_paired_All[simp del] split_paired_Ex[simp del] trans_state_update'[symmetric,simp] @@ -5203,30 +5242,33 @@ lemma cteInsert_corres: (valid_objs and pspace_distinct and pspace_aligned and valid_mdb and valid_list and K (src\dest) and cte_wp_at (\c. c=Structures_A.NullCap) dest and - (\s. cte_wp_at (is_derived (cdt s) src c) src s)) + (\s. cte_wp_at (is_derived (cdt s) src c) src s) and valid_arch_state) (pspace_distinct' and pspace_aligned' and valid_mdb' and valid_cap' c' and cte_wp_at' (\c. cteCap c=NullCap) dest') (cap_insert c src dest) (cteInsert c' src' dest')" - (is "corres _ (?P and (\s. cte_wp_at _ _ s)) (?P' and cte_wp_at' _ _) _ _") + (is "corres _ (?P and (\s. cte_wp_at _ _ s) and valid_arch_state) (?P' and cte_wp_at' _ _) _ _") using assms unfolding cap_insert_def cteInsert_def apply simp + (* this lemma doesn't use the assertion, but does need to establish it *) + apply (rule corres_stateAssert_add_assertion[rotated]) + apply (rule archMDBAssertions_cross; simp add: valid_mdb_def) apply (rule corres_guard_imp) apply (rule corres_split[OF get_cap_corres]) apply (rule corres_split[OF get_cap_corres]) - apply (rule_tac F="cteCap rv' = NullCap" in corres_gen_asm2) + apply (rule_tac F="cteCap oldCTE = NullCap" in corres_gen_asm2) apply simp apply (rule_tac P="?P and cte_at dest and (\s. cte_wp_at (is_derived (cdt s) src c) src s) and cte_wp_at ((=) src_cap) src" and Q="?P' and - cte_wp_at' ((=) rv') (cte_map dest) and + cte_wp_at' ((=) oldCTE) (cte_map dest) and cte_wp_at' ((=) srcCTE) (cte_map src)" in corres_assert_assume) prefer 2 apply (clarsimp simp: cte_wp_at_ctes_of valid_mdb'_def valid_mdb_ctes_def valid_nullcaps_def) - apply (case_tac rv') + apply (case_tac oldCTE) apply (simp add: initMDBNode_def) apply (erule allE)+ apply (erule (1) impE) @@ -5235,7 +5277,7 @@ lemma cteInsert_corres: apply (rule_tac R="\r. ?P and cte_at dest and (\s. (is_derived (cdt s) src c) src_cap) and cte_wp_at ((=) (masked_as_full src_cap c)) src" and - R'="\r. ?P' and cte_wp_at' ((=) rv') (cte_map dest) and + R'="\r. ?P' and cte_wp_at' ((=) oldCTE) (cte_map dest) and cte_wp_at' ((=) (CTE (maskedAsFull (cteCap srcCTE) c') (cteMDBNode srcCTE))) (cte_map src)" in corres_split[where r'=dc]) @@ -5299,7 +5341,7 @@ lemma cteInsert_corres: apply (thin_tac "machine_state t = s" for s t)+ apply (case_tac "srcCTE") apply (rename_tac src_cap' src_node) - apply (case_tac "rv'") + apply (case_tac "oldCTE") apply (rename_tac dest_node) apply (clarsimp simp: in_set_cap_cte_at_swp) apply (subgoal_tac "cte_at src a \ is_derived (cdt a) src c src_cap") @@ -5587,7 +5629,7 @@ lemma cteInsert_corres: apply clarsimp apply (subgoal_tac "mdbRevocable node = isCapRevocable c' (cteCap srcCTE)") prefer 2 - apply (case_tac rv') + apply (case_tac oldCTE) subgoal by (clarsimp simp add: const_def modify_map_def split: if_split_asm) apply simp apply (rule is_cap_revocable_eq, assumption, assumption) @@ -5600,7 +5642,7 @@ lemma cteInsert_corres: split:if_splits dest!:cap_master_cap_eqDs) apply clarsimp apply (case_tac srcCTE) - apply (case_tac rv') + apply (case_tac oldCTE) apply clarsimp apply (subgoal_tac "\cap' node'. ctes_of b (cte_map (aa,bb)) = Some (CTE cap' node')") prefer 2 @@ -5626,7 +5668,7 @@ lemma cteInsert_corres: apply (wp set_untyped_cap_full_valid_objs set_untyped_cap_as_full_valid_mdb set_untyped_cap_as_full_cte_wp_at setUntypedCapAsFull_valid_cap setUntypedCapAsFull_cte_wp_at | clarsimp simp: cte_wp_at_caps_of_state| wps)+ - apply (case_tac rv',clarsimp simp:cte_wp_at_ctes_of maskedAsFull_def) + apply (case_tac oldCTE,clarsimp simp:cte_wp_at_ctes_of maskedAsFull_def) apply (wp getCTE_wp' get_cap_wp)+ apply clarsimp subgoal by (fastforce elim: cte_wp_at_weakenE) @@ -5636,7 +5678,7 @@ lemma cteInsert_corres: apply (thin_tac "machine_state t = s" for s t)+ apply (case_tac "srcCTE") apply (rename_tac src_cap' src_node) - apply (case_tac "rv'") + apply (case_tac "oldCTE") apply (rename_tac dest_node) apply (clarsimp simp: in_set_cap_cte_at_swp) apply (subgoal_tac "cte_at src a \ is_derived (cdt a) src c src_cap") diff --git a/proof/refine/AARCH64/CSpace_R.thy b/proof/refine/AARCH64/CSpace_R.thy index 6778d2349e..498fb85bd5 100644 --- a/proof/refine/AARCH64/CSpace_R.thy +++ b/proof/refine/AARCH64/CSpace_R.thy @@ -4519,6 +4519,7 @@ end locale mdb_insert_simple = mdb_insert + assumes safe_parent: "safe_parent_for' m src c'" assumes simple: "is_simple_cap' c'" + assumes arch_mdb_assert: "arch_mdb_assert m" begin interpretation Arch . (*FIXME: arch-split*) @@ -4717,6 +4718,12 @@ lemma maskedAsFull_revokable_safe_parent: context begin interpretation Arch . (*FIXME: arch-split*) +(* FIXME arch-split: generic statement, arch specific proof *) +lemma setUntypedCapAsFull_archMDBAssertions[wp]: + "setUntypedCapAsFull src_cap cap p \archMDBAssertions\" + unfolding archMDBAssertions_def arch_mdb_assert_def + by wp + lemma cteInsert_simple_corres: assumes "cap_relation c c'" "src' = cte_map src" "dest' = cte_map dest" notes trans_state_update'[symmetric,simp] @@ -4725,34 +4732,36 @@ lemma cteInsert_simple_corres: valid_mdb and valid_list and K (src\dest) and cte_wp_at (\c. c=cap.NullCap) dest and K (is_simple_cap c) and - (\s. cte_wp_at (safe_parent_for (cdt s) src c) src s)) + (\s. cte_wp_at (safe_parent_for (cdt s) src c) src s) and valid_arch_state) (pspace_distinct' and pspace_aligned' and valid_mdb' and valid_cap' c' and K (is_simple_cap' c') and cte_wp_at' (\c. cteCap c=NullCap) dest' and (\s. safe_parent_for' (ctes_of s) src' c')) (cap_insert c src dest) (cteInsert c' src' dest')" - (is "corres _ (?P and (\s. cte_wp_at _ _ s)) (?P' and cte_wp_at' _ _ and _) _ _") + (is "corres _ (?P and (\s. cte_wp_at _ _ s) and valid_arch_state) (?P' and cte_wp_at' _ _ and _) _ _") using assms unfolding cap_insert_def cteInsert_def supply subst_all [simp del] apply simp + apply (rule corres_stateAssert_add_assertion[rotated]) + apply (rule archMDBAssertions_cross; simp add: valid_mdb_def) apply (rule corres_guard_imp) apply (rule corres_split[OF get_cap_corres]) apply (rule corres_split[OF get_cap_corres]) - apply (rule_tac F="cteCap rv' = NullCap" in corres_gen_asm2) + apply (rule_tac F="cteCap oldCTE = NullCap" in corres_gen_asm2) apply simp apply (rule_tac P="?P and cte_at dest and (\s. cte_wp_at (safe_parent_for (cdt s) src c) src s) and cte_wp_at ((=) src_cap) src" and - Q="?P' and - cte_wp_at' ((=) rv') (cte_map dest) and + Q="?P' and archMDBAssertions and + cte_wp_at' ((=) oldCTE) (cte_map dest) and cte_wp_at' ((=) srcCTE) (cte_map src) and (\s. safe_parent_for' (ctes_of s) src' c')" in corres_assert_assume) prefer 2 apply (clarsimp simp: cte_wp_at_ctes_of valid_mdb'_def valid_mdb_ctes_def valid_nullcaps_def) - apply (case_tac rv') + apply (case_tac oldCTE) apply (simp add: initMDBNode_def) apply (erule allE)+ apply (erule (1) impE) @@ -4761,7 +4770,7 @@ lemma cteInsert_simple_corres: apply (rule_tac R="\r. ?P and cte_at dest and (\s. cte_wp_at (safe_parent_for (cdt s) src c) src s) and cte_wp_at ((=) (masked_as_full src_cap c)) src" and - R'="\r. ?P' and cte_wp_at' ((=) rv') (cte_map dest) + R'="\r. ?P' and archMDBAssertions and cte_wp_at' ((=) oldCTE) (cte_map dest) and cte_wp_at' ((=) (CTE (maskedAsFull (cteCap srcCTE) c') (cteMDBNode srcCTE))) (cte_map src) and (\s. safe_parent_for' (ctes_of s) src' c')" in corres_split[where r'=dc]) @@ -4856,7 +4865,7 @@ lemma cteInsert_simple_corres: apply clarsimp apply (subgoal_tac "mdbRevocable node = isCapRevocable c' (cteCap srcCTE)") prefer 2 - apply (case_tac rv') + apply (case_tac oldCTE) apply (clarsimp simp add: const_def modify_map_def split: if_split_asm) apply clarsimp apply (rule is_cap_revocable_eq, assumption, assumption) @@ -4869,7 +4878,7 @@ lemma cteInsert_simple_corres: apply (clarsimp simp: cte_wp_at_def is_simple_cap_def) apply clarsimp apply (case_tac srcCTE) - apply (case_tac rv') + apply (case_tac oldCTE) apply clarsimp apply (subgoal_tac "\cap' node'. ctes_of b (cte_map (aa,bb)) = Some (CTE cap' node')") prefer 2 @@ -4893,14 +4902,14 @@ lemma cteInsert_simple_corres: set_untyped_cap_as_full_cte_wp_at setUntypedCapAsFull_valid_cap setUntypedCapAsFull_cte_wp_at setUntypedCapAsFull_safe_parent_for' | clarsimp | wps)+ apply (clarsimp simp:cte_wp_at_caps_of_state ) - apply (case_tac rv',clarsimp simp:cte_wp_at_ctes_of maskedAsFull_def) + apply (case_tac oldCTE,clarsimp simp:cte_wp_at_ctes_of maskedAsFull_def) apply (wp getCTE_wp' get_cap_wp)+ apply clarsimp subgoal by (fastforce elim: cte_wp_at_weakenE) subgoal by (clarsimp simp: cte_wp_at'_def) apply (case_tac "srcCTE") apply (rename_tac src_cap' src_node) - apply (case_tac "rv'") + apply (case_tac "oldCTE") apply (rename_tac dest_node) apply (clarsimp simp: in_set_cap_cte_at_swp) apply (subgoal_tac "cte_at src a \ safe_parent_for (cdt a) src c src_cap") @@ -4924,7 +4933,8 @@ lemma cteInsert_simple_corres: apply (simp (no_asm_simp) add: cdt_relation_def split: if_split) apply (intro impI allI) apply (frule mdb_insert_simple_axioms.intro) - apply(clarsimp simp:cte_wp_at_ctes_of) + apply(clarsimp simp:cte_wp_at_ctes_of) + apply (simp add: archMDBAssertions_def) apply (drule (1) mdb_insert_simple.intro) apply (drule_tac src_cap' = src_cap' in maskedAsFull_revokable_safe_parent[symmetric]) apply simp+ @@ -5820,7 +5830,7 @@ lemma cteInsert_simple_mdb': mdb_ptr_axioms.intro mdb_insert_axioms.intro) apply (simp add:modify_map_def valid_mdb_ctes_maskedAsFull)+ apply (clarsimp simp:nullPointer_def)+ - apply ((clarsimp simp:valid_mdb_ctes_def)+) + apply (clarsimp simp:valid_mdb_ctes_def archMDBAssertions_def)+ apply (drule mdb_insert_simple'.mdb) apply (clarsimp simp:valid_mdb_ctes_def) done diff --git a/proof/refine/AARCH64/Interrupt_R.thy b/proof/refine/AARCH64/Interrupt_R.thy index b6985106fa..47d0f51a8d 100644 --- a/proof/refine/AARCH64/Interrupt_R.thy +++ b/proof/refine/AARCH64/Interrupt_R.thy @@ -477,6 +477,9 @@ lemma setIRQTrigger_corres: | simp add: dc_def)+ done +crunch set_irq_state + for valid_arch_state[wp]: valid_arch_state + lemma arch_performIRQControl_corres: "arch_irq_control_inv_relation x2 ivk' \ corres (dc \ dc) (einvs and arch_irq_control_inv_valid x2) diff --git a/proof/refine/AARCH64/InvariantUpdates_H.thy b/proof/refine/AARCH64/InvariantUpdates_H.thy index 9ba90373c8..4a2d623f5c 100644 --- a/proof/refine/AARCH64/InvariantUpdates_H.thy +++ b/proof/refine/AARCH64/InvariantUpdates_H.thy @@ -516,10 +516,4 @@ lemma invs'_gsTypes_update: end -(* FIXME arch-split: valid_arch_mdb_ctes only exists to contain ioport_control on x64, and it is not - yet clear what the best way to arch-split it is, or whether it can be crossed from AInvs. - Therefore, for now, export the truth that it doesn't do anything on this arch beyond this point *) -arch_requalify_facts valid_arch_mdb_ctes_def -lemmas [simp] = valid_arch_mdb_ctes_def - end diff --git a/proof/refine/AARCH64/Ipc_R.thy b/proof/refine/AARCH64/Ipc_R.thy index ef18b656ec..56c206ddb7 100644 --- a/proof/refine/AARCH64/Ipc_R.thy +++ b/proof/refine/AARCH64/Ipc_R.thy @@ -392,6 +392,10 @@ lemma cte_refs'_maskedAsFull[simp]: apply (clarsimp simp:maskedAsFull_def isCap_simps)+ done +lemma set_extra_badge_valid_arch_state[wp]: + "set_extra_badge buffer badge n \ valid_arch_state \" + unfolding set_extra_badge_def + by wp lemma transferCapsToSlots_corres: "\ list_all2 (\(cap, slot) (cap', slot'). cap_relation cap cap' @@ -399,7 +403,7 @@ lemma transferCapsToSlots_corres: mi' = message_info_map mi \ \ corres ((=) \ message_info_map) (\s. valid_objs s \ pspace_aligned s \ pspace_distinct s \ valid_mdb s - \ valid_list s + \ valid_list s \ valid_arch_state s \ (case ep of Some x \ ep_at x s | _ \ True) \ (\x \ set slots. cte_wp_at (\cap. cap = cap.NullCap) x s \ real_cte_at x s) @@ -473,7 +477,8 @@ next apply (simp add: tl_map) apply (rule corres_rel_imp, rule Cons.hyps, simp_all)[1] apply (wp valid_case_option_post_wp hoare_vcg_const_Ball_lift - hoare_vcg_const_Ball_lift cap_insert_weak_cte_wp_at) + hoare_vcg_const_Ball_lift cap_insert_derived_valid_arch_state + cap_insert_weak_cte_wp_at) apply (wp hoare_vcg_const_Ball_lift | simp add:split_def del: imp_disj1)+ apply (wp cap_insert_cte_wp_at) apply (wp valid_case_option_post_wp hoare_vcg_const_Ball_lift @@ -614,6 +619,7 @@ lemma cteInsert_assume_Null: apply (rule hoare_name_pre_state) apply (erule impCE) apply (simp add: cteInsert_def) + apply (rule bind_wp[OF _ stateAssert_sp]) apply (rule bind_wp[OF _ getCTE_sp])+ apply (rule hoare_name_pre_state) apply (clarsimp simp: cte_wp_at_ctes_of) @@ -1041,7 +1047,7 @@ lemma transferCaps_corres: corres ((=) \ message_info_map) (tcb_at receiver and valid_objs and pspace_aligned and pspace_distinct and valid_mdb - and valid_list + and valid_list and valid_arch_state and (\s. case ep of Some x \ ep_at x s | _ \ True) and case_option \ in_user_frame recv_buf and (\s. valid_message_info info) @@ -1414,10 +1420,14 @@ lemma copyMRs_valid_mdb[wp]: "\valid_mdb'\ copyMRs t buf t' buf' n \\rv. valid_mdb'\" by (simp add: valid_mdb'_def copyMRs_ctes_of) +crunch copy_mrs + for valid_arch_state[wp]: valid_arch_state + (wp: crunch_wps) + lemma doNormalTransfer_corres: "corres dc (tcb_at sender and tcb_at receiver and (pspace_aligned:: det_state \ bool) - and valid_objs and cur_tcb and valid_mdb and valid_list and pspace_distinct + and valid_objs and cur_tcb and valid_mdb and valid_list and valid_arch_state and pspace_distinct and (\s. case ep of Some x \ ep_at x s | _ \ True) and case_option \ in_user_frame send_buf and case_option \ in_user_frame recv_buf) @@ -1696,7 +1706,7 @@ lemma lookupIPCBuffer_valid_ipc_buffer [wp]: lemma doIPCTransfer_corres: "corres dc (tcb_at s and tcb_at r and valid_objs and pspace_aligned - and valid_list + and valid_list and valid_arch_state and pspace_distinct and valid_mdb and cur_tcb and (\s. case ep of Some x \ ep_at x s | _ \ True)) (tcb_at' s and tcb_at' r and valid_pspace' and cur_tcb' @@ -1704,9 +1714,9 @@ lemma doIPCTransfer_corres: (do_ipc_transfer s ep bg grt r) (doIPCTransfer s ep bg grt r)" apply (simp add: do_ipc_transfer_def doIPCTransfer_def) - apply (rule_tac Q="%receiveBuffer sa. tcb_at s sa \ valid_objs sa \ - pspace_aligned sa \ tcb_at r sa \ - cur_tcb sa \ valid_mdb sa \ valid_list sa \ pspace_distinct sa \ + apply (rule_tac Q="\receiveBuffer sa. tcb_at s sa \ valid_objs sa \ + pspace_aligned sa \ pspace_distinct sa \ tcb_at r sa \ + cur_tcb sa \ valid_mdb sa \ valid_list sa \ valid_arch_state sa \ (case ep of None \ True | Some x \ ep_at x sa) \ case_option (\_. True) in_user_frame receiveBuffer sa \ obj_at (\ko. \tcb. ko = TCB tcb @@ -2282,7 +2292,7 @@ lemma setupCallerCap_corres: (st_tcb_at (Not \ halted) sender and tcb_at receiver and st_tcb_at (Not \ awaiting_reply) sender and valid_reply_caps and valid_objs and pspace_distinct and pspace_aligned and valid_mdb - and valid_list and + and valid_list and valid_arch_state and valid_reply_masters and cte_wp_at (\c. c = cap.NullCap) (receiver, tcb_cnode_index 3)) (tcb_at' sender and tcb_at' receiver and valid_pspace' and (\s. weak_sch_act_wf (ksSchedulerAction s) s)) @@ -2501,6 +2511,7 @@ proof - valid_queues_in_correct_ready_q valid_queues_ready_qs_distinct valid_sched_valid_queues)+ apply ((wp hoare_drop_imps do_ipc_transfer_tcb_caps weak_valid_sched_action_lift + do_ipc_transfer_valid_arch | clarsimp simp: is_cap_simps)+)[1] apply (simp add: pred_conj_def) apply (strengthen sch_act_wf_weak) @@ -3216,7 +3227,7 @@ lemma receiveIPC_corres: apply (rule corres_split[OF doIPCTransfer_corres]) apply (simp split del: if_split cong: if_cong) apply (fold dc_def)[1] - apply (rule_tac P="valid_objs and valid_mdb and valid_list + apply (rule_tac P="valid_objs and valid_mdb and valid_list and valid_arch_state and valid_sched and cur_tcb and valid_reply_caps @@ -3246,7 +3257,7 @@ lemma receiveIPC_corres: apply (fastforce simp: st_tcb_at_tcb_at st_tcb_def2 valid_sched_def valid_sched_action_def) apply (clarsimp split: if_split_asm) - apply (clarsimp | wp do_ipc_transfer_tcb_caps)+ + apply (clarsimp | wp do_ipc_transfer_tcb_caps do_ipc_transfer_valid_arch)+ apply (rule_tac Q'="\_ s. sch_act_wf (ksSchedulerAction s) s \ sym_heap_sched_pointers s \ valid_sched_pointers s \ pspace_aligned' s \ pspace_distinct' s" @@ -3584,19 +3595,12 @@ lemma cteInsert_cap_to': "\ex_nonz_cap_to' p and cte_wp_at' (\c. cteCap c = NullCap) dest\ cteInsert cap src dest \\rv. ex_nonz_cap_to' p\" - apply (simp add: cteInsert_def ex_nonz_cap_to'_def - updateCap_def setUntypedCapAsFull_def - split del: if_split) - apply (rule hoare_pre, rule hoare_vcg_ex_lift) - apply (wp updateMDB_weak_cte_wp_at - setCTE_weak_cte_wp_at - | simp - | rule hoare_drop_imps)+ - apply (wp getCTE_wp) - apply clarsimp + apply (simp add: cteInsert_def ex_nonz_cap_to'_def updateCap_def setUntypedCapAsFull_def) + apply (wpsimp wp: updateMDB_weak_cte_wp_at setCTE_weak_cte_wp_at hoare_vcg_ex_lift + | rule hoare_drop_imps + | wp getCTE_wp)+ (* getCTE_wp is separate to apply it only to the last one *) apply (rule_tac x=cref in exI) - apply (rule conjI) - apply (clarsimp simp: cte_wp_at_ctes_of)+ + apply (fastforce simp: cte_wp_at_ctes_of) done crunch setExtraBadge diff --git a/proof/refine/AARCH64/Tcb_R.thy b/proof/refine/AARCH64/Tcb_R.thy index 9e7b2892ad..6dc628c412 100644 --- a/proof/refine/AARCH64/Tcb_R.thy +++ b/proof/refine/AARCH64/Tcb_R.thy @@ -851,7 +851,7 @@ lemma checkCapAt_cteInsert_corres: apply clarsimp apply (rule conjI, fastforce)+ apply (cases src_slot) - apply (clarsimp simp: cte_wp_at_caps_of_state) + apply (clarsimp simp: cte_wp_at_caps_of_state invs_arch_state) apply (rule conjI) apply (frule same_object_as_cap_master) apply (clarsimp simp: cap_master_cap_simps is_cnode_or_valid_arch_def diff --git a/proof/refine/ARM/ArchInvsDefs_H.thy b/proof/refine/ARM/ArchInvsDefs_H.thy index 5c9372dbf3..45fc969c5a 100644 --- a/proof/refine/ARM/ArchInvsDefs_H.thy +++ b/proof/refine/ARM/ArchInvsDefs_H.thy @@ -174,9 +174,6 @@ abbreviation (input) lemmas isArchPageCap_def = isArchFrameCap_def -definition valid_arch_mdb_ctes :: "cte_heap \ bool" where - "valid_arch_mdb_ctes \ \" - definition page_directory_refs' :: "word32 \ word32 set" where "page_directory_refs' x \ (\y. x + (y << 2)) ` {y. y < 2 ^ 12}" diff --git a/proof/refine/ARM/Arch_R.thy b/proof/refine/ARM/Arch_R.thy index 825a297896..4939f7cc10 100644 --- a/proof/refine/ARM/Arch_R.thy +++ b/proof/refine/ARM/Arch_R.thy @@ -137,6 +137,7 @@ lemma performASIDControlInvocation_corres: apply (cases i) apply (rename_tac word1 prod1 prod2 word2) apply (clarsimp simp: asid_ci_map_def) + apply (rename_tac p slot p' slot' word2) apply (simp add: perform_asid_control_invocation_def placeNewObject_def2 performASIDControlInvocation_def) apply (rule corres_name_pre) @@ -194,7 +195,7 @@ lemma performASIDControlInvocation_corres: apply wp+ apply (strengthen safe_parent_strg[where idx = "2^pageBits"]) apply (strengthen invs_valid_objs invs_distinct - invs_psp_aligned invs_mdb + invs_psp_aligned invs_mdb invs_arch_state | simp cong:conj_cong)+ apply (wp retype_region_plain_invs[where sz = pageBits] retype_cte_wp_at[where sz = pageBits])+ @@ -277,7 +278,7 @@ lemma performASIDControlInvocation_corres: apply (drule detype_locale.non_null_present) apply (fastforce simp:cte_wp_at_caps_of_state) apply simp - apply (frule_tac ptr = "(aa,ba)" in detype_invariants [rotated 3]) + apply (frule_tac ptr = "(p', slot')" in detype_invariants [rotated 3]) apply fastforce apply simp apply (simp add: cte_wp_at_caps_of_state) @@ -304,7 +305,7 @@ lemma performASIDControlInvocation_corres: apply (simp add:empty_descendants_range_in)+ apply (rule conjI) apply clarsimp - apply (drule_tac p = "(aa,ba)" in cap_refs_in_kernel_windowD2[OF caps_of_state_cteD]) + apply (drule_tac p = "(p', slot')" in cap_refs_in_kernel_windowD2[OF caps_of_state_cteD]) apply fastforce apply (clarsimp simp: region_in_kernel_window_def valid_cap_def cap_aligned_def is_aligned_neg_mask_eq detype_def clear_um_def) @@ -314,7 +315,7 @@ lemma performASIDControlInvocation_corres: apply (clarsimp simp: detype_def clear_um_def detype_ext_def valid_sched_def valid_etcbs_def st_tcb_at_kh_def obj_at_kh_def st_tcb_at_def obj_at_def is_etcb_at_def) apply (simp add: detype_def clear_um_def) - apply (drule_tac x = "cte_map (aa,ba)" in pspace_relation_cte_wp_atI[OF state_relation_pspace_relation]) + apply (drule_tac x = "cte_map (p', slot')" in pspace_relation_cte_wp_atI[OF state_relation_pspace_relation]) apply (simp add:invs_valid_objs)+ apply clarsimp apply (drule cte_map_inj_eq) diff --git a/proof/refine/ARM/CNodeInv_R.thy b/proof/refine/ARM/CNodeInv_R.thy index b4456a969b..a891af069e 100644 --- a/proof/refine/ARM/CNodeInv_R.thy +++ b/proof/refine/ARM/CNodeInv_R.thy @@ -8371,9 +8371,6 @@ proof apply (erule (1) irq_controlD, rule irq_control) done - show "valid_arch_mdb_ctes m'" - by simp - have distz: "distinct_zombies m" using valid by (simp add: valid_mdb_ctes_def) diff --git a/proof/refine/ARM/CSpace1_R.thy b/proof/refine/ARM/CSpace1_R.thy index ca93a5334e..7b50f6cf0f 100644 --- a/proof/refine/ARM/CSpace1_R.thy +++ b/proof/refine/ARM/CSpace1_R.thy @@ -14,6 +14,20 @@ imports "AInvs.ArchDetSchedSchedule_AI" begin +context Arch begin arch_global_naming + +(* No assertion necessary for this architecture. *) +definition arch_mdb_assert :: "cte_heap \ bool" where + "arch_mdb_assert m \ True" + +end + +arch_requalify_consts + arch_mdb_assert + +defs archMDBAssertions_def: + "archMDBAssertions s \ arch_mdb_assert (ctes_of s)" + context Arch begin global_naming ARM_A (*FIXME: arch-split*) lemmas final_matters_def = final_matters_def[simplified final_matters_arch_def] @@ -250,7 +264,7 @@ lemma pspace_relation_cte_wp_at: lemma pspace_relation_ctes_ofI: "\ pspace_relation (kheap s) (ksPSpace s'); - cte_wp_at ((=) c) slot s; pspace_aligned' s'; + cte_wp_at ((=) c) slot s; pspace_aligned' s'; pspace_distinct' s' \ \ \cte. ctes_of s' (cte_map slot) = Some cte \ cap_relation c (cteCap cte)" apply (cases slot, clarsimp) @@ -258,6 +272,22 @@ lemma pspace_relation_ctes_ofI: apply (simp add: cte_wp_at_ctes_of) done +lemma pspace_relation_caps_of_state_cross: + "\ pspace_relation (kheap s) (ksPSpace s'); + caps_of_state s slot = Some c; pspace_aligned s; pspace_distinct s \ + \ \cte. ctes_of s' (cte_map slot) = Some cte \ cap_relation c (cteCap cte)" + for s' :: kernel_state + by (auto simp: cte_wp_at_caps_of_state + intro!: pspace_relation_ctes_ofI pspace_aligned_cross pspace_distinct_cross) + +lemma caps_of_state_cross: + "\ caps_of_state s slot = Some cap; pspace_aligned s; pspace_distinct s; (s,s') \ state_relation \ + \ \cap'. cteCaps_of s' (cte_map slot) = Some cap' \ cap_relation cap cap'" + apply (erule state_relationE) + apply (drule (3) pspace_relation_caps_of_state_cross) + apply (fastforce simp: cteCaps_of_def) + done + lemma get_cap_corres_P: "corres (\x y. cap_relation x (cteCap y) \ P x) (cte_wp_at P cslot_ptr) @@ -890,21 +920,13 @@ lemma ctes_of_valid_cap'': done lemma cap_insert_objs' [wp]: - "\valid_objs' - and valid_cap' cap\ - cteInsert cap src dest \\rv. valid_objs'\" - including no_pre - apply (simp add: cteInsert_def updateCap_def setUntypedCapAsFull_def bind_assoc split del: if_split) - apply (wp setCTE_valid_objs) - apply simp - apply wp+ - apply (clarsimp simp: updateCap_def) - apply (wp|simp)+ - apply (rule hoare_drop_imp)+ - apply wp+ - apply (rule hoare_strengthen_post[OF getCTE_sp]) + "\valid_objs' and valid_cap' cap\ + cteInsert cap src dest + \\_. valid_objs'\" + apply (simp add: cteInsert_def updateCap_def setUntypedCapAsFull_def) + apply (wpsimp wp: setCTE_valid_objs | wp getCTE_wp')+ apply (clarsimp simp: cte_wp_at_ctes_of isCap_simps - dest!: ctes_of_valid_cap'') + dest!: ctes_of_valid_cap'') done lemma cteInsert_weak_cte_wp_at: @@ -1930,6 +1952,14 @@ lemma pspace_relation_cte_wp_atI: apply assumption done +lemma caps_of_state_rev_cross: + "\ ctes_of s' p = Some cte; valid_objs s; (s,s') \ state_relation \ + \ \cap slot. caps_of_state s slot = Some cap \ p = cte_map slot \ cap_relation cap (cteCap cte)" + apply (erule state_relationE) + apply (drule (2) pspace_relation_cte_wp_atI) + apply (fastforce simp: cte_wp_at_caps_of_state) + done + lemma sameRegion_corres: "\ sameRegionAs c' d'; cap_relation c c'; cap_relation d d' \ \ same_region_as c d" @@ -5064,6 +5094,15 @@ lemma cte_map_inj_eq': done context begin interpretation Arch . (*FIXME: arch-split*) + +(* interface lemma: generic statement, arch-specific proof *) +lemma archMDBAssertions_cross: + "\ valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_arch_state s; valid_objs s; + (s, s') \ state_relation \ + \ archMDBAssertions s'" + unfolding archMDBAssertions_def + by (simp add: arch_mdb_assert_def) + lemma cteInsert_corres: notes split_paired_All[simp del] split_paired_Ex[simp del] trans_state_update'[symmetric,simp] @@ -5072,30 +5111,33 @@ lemma cteInsert_corres: (valid_objs and pspace_distinct and pspace_aligned and valid_mdb and valid_list and K (src\dest) and cte_wp_at (\c. c=Structures_A.NullCap) dest and - (\s. cte_wp_at (is_derived (cdt s) src c) src s)) + (\s. cte_wp_at (is_derived (cdt s) src c) src s) and valid_arch_state) (pspace_distinct' and pspace_aligned' and valid_mdb' and valid_cap' c' and cte_wp_at' (\c. cteCap c=NullCap) dest') (cap_insert c src dest) (cteInsert c' src' dest')" - (is "corres _ (?P and (\s. cte_wp_at _ _ s)) (?P' and cte_wp_at' _ _) _ _") + (is "corres _ (?P and (\s. cte_wp_at _ _ s) and valid_arch_state) (?P' and cte_wp_at' _ _) _ _") using assms unfolding cap_insert_def cteInsert_def apply simp + (* this lemma doesn't use the assertion, but does need to establish it *) + apply (rule corres_stateAssert_add_assertion[rotated]) + apply (rule archMDBAssertions_cross; simp add: valid_mdb_def) apply (rule corres_guard_imp) apply (rule corres_split[OF get_cap_corres]) apply (rule corres_split[OF get_cap_corres]) - apply (rule_tac F="cteCap rv' = NullCap" in corres_gen_asm2) + apply (rule_tac F="cteCap oldCTE = NullCap" in corres_gen_asm2) apply simp apply (rule_tac P="?P and cte_at dest and (\s. cte_wp_at (is_derived (cdt s) src c) src s) and cte_wp_at ((=) src_cap) src" and Q="?P' and - cte_wp_at' ((=) rv') (cte_map dest) and + cte_wp_at' ((=) oldCTE) (cte_map dest) and cte_wp_at' ((=) srcCTE) (cte_map src)" in corres_assert_assume) prefer 2 apply (clarsimp simp: cte_wp_at_ctes_of valid_mdb'_def valid_mdb_ctes_def valid_nullcaps_def) - apply (case_tac rv') + apply (case_tac oldCTE) apply (simp add: initMDBNode_def) apply (erule allE)+ apply (erule (1) impE) @@ -5104,7 +5146,7 @@ lemma cteInsert_corres: apply (rule_tac R="\r. ?P and cte_at dest and (\s. (is_derived (cdt s) src c) src_cap) and cte_wp_at ((=) (masked_as_full src_cap c)) src" and - R'="\r. ?P' and cte_wp_at' ((=) rv') (cte_map dest) and + R'="\r. ?P' and cte_wp_at' ((=) oldCTE) (cte_map dest) and cte_wp_at' ((=) (CTE (maskedAsFull (cteCap srcCTE) c') (cteMDBNode srcCTE))) (cte_map src)" in corres_split[where r'=dc]) @@ -5168,7 +5210,7 @@ lemma cteInsert_corres: apply (thin_tac "machine_state t = s" for s t)+ apply (case_tac "srcCTE") apply (rename_tac src_cap' src_node) - apply (case_tac "rv'") + apply (case_tac "oldCTE") apply (rename_tac dest_node) apply (clarsimp simp: in_set_cap_cte_at_swp) apply (subgoal_tac "cte_at src a \ is_derived (cdt a) src c src_cap") @@ -5455,7 +5497,7 @@ lemma cteInsert_corres: apply clarsimp apply (subgoal_tac "mdbRevocable node = revokable' (cteCap srcCTE) c'") prefer 2 - apply (case_tac rv') + apply (case_tac oldCTE) subgoal by (clarsimp simp add: const_def modify_map_def split: if_split_asm) apply simp apply (rule revokable_eq, assumption, assumption) @@ -5468,7 +5510,7 @@ lemma cteInsert_corres: split:if_splits dest!:cap_master_cap_eqDs) apply clarsimp apply (case_tac srcCTE) - apply (case_tac rv') + apply (case_tac oldCTE) apply clarsimp apply (subgoal_tac "\cap' node'. ctes_of b (cte_map (aa,bb)) = Some (CTE cap' node')") prefer 2 @@ -5494,7 +5536,7 @@ lemma cteInsert_corres: apply (wp set_untyped_cap_full_valid_objs set_untyped_cap_as_full_valid_mdb set_untyped_cap_as_full_cte_wp_at setUntypedCapAsFull_valid_cap setUntypedCapAsFull_cte_wp_at | clarsimp simp: cte_wp_at_caps_of_state| wps)+ - apply (case_tac rv',clarsimp simp:cte_wp_at_ctes_of maskedAsFull_def) + apply (case_tac oldCTE,clarsimp simp:cte_wp_at_ctes_of maskedAsFull_def) apply (wp getCTE_wp' get_cap_wp)+ apply clarsimp subgoal by (fastforce elim: cte_wp_at_weakenE) @@ -5504,7 +5546,7 @@ lemma cteInsert_corres: apply (thin_tac "machine_state t = s" for s t)+ apply (case_tac "srcCTE") apply (rename_tac src_cap' src_node) - apply (case_tac "rv'") + apply (case_tac "oldCTE") apply (rename_tac dest_node) apply (clarsimp simp: in_set_cap_cte_at_swp) apply (subgoal_tac "cte_at src a \ is_derived (cdt a) src c src_cap") diff --git a/proof/refine/ARM/CSpace_R.thy b/proof/refine/ARM/CSpace_R.thy index 98c013ef22..f89505913a 100644 --- a/proof/refine/ARM/CSpace_R.thy +++ b/proof/refine/ARM/CSpace_R.thy @@ -4530,6 +4530,7 @@ end locale mdb_insert_simple = mdb_insert + assumes safe_parent: "safe_parent_for' m src c'" assumes simple: "is_simple_cap' c'" + assumes arch_mdb_assert: "arch_mdb_assert m" begin interpretation Arch . (*FIXME: arch-split*) lemma dest_no_parent_n: @@ -4722,6 +4723,13 @@ lemma maskedAsFull_revokable_safe_parent: done context begin interpretation Arch . (*FIXME: arch-split*) + +(* FIXME arch-split: generic statement, arch specific proof *) +lemma setUntypedCapAsFull_archMDBAssertions[wp]: + "setUntypedCapAsFull src_cap cap p \archMDBAssertions\" + unfolding archMDBAssertions_def arch_mdb_assert_def + by wp + lemma cteInsert_simple_corres: assumes "cap_relation c c'" "src' = cte_map src" "dest' = cte_map dest" notes trans_state_update'[symmetric,simp] @@ -4730,34 +4738,36 @@ lemma cteInsert_simple_corres: valid_mdb and valid_list and K (src\dest) and cte_wp_at (\c. c=cap.NullCap) dest and K (is_simple_cap c) and - (\s. cte_wp_at (safe_parent_for (cdt s) src c) src s)) + (\s. cte_wp_at (safe_parent_for (cdt s) src c) src s) and valid_arch_state) (pspace_distinct' and pspace_aligned' and valid_mdb' and valid_cap' c' and K (is_simple_cap' c') and cte_wp_at' (\c. cteCap c=NullCap) dest' and (\s. safe_parent_for' (ctes_of s) src' c')) (cap_insert c src dest) (cteInsert c' src' dest')" - (is "corres _ (?P and (\s. cte_wp_at _ _ s)) (?P' and cte_wp_at' _ _ and _) _ _") + (is "corres _ (?P and (\s. cte_wp_at _ _ s) and valid_arch_state) (?P' and cte_wp_at' _ _ and _) _ _") using assms unfolding cap_insert_def cteInsert_def supply subst_all [simp del] apply simp + apply (rule corres_stateAssert_add_assertion[rotated]) + apply (rule archMDBAssertions_cross; simp add: valid_mdb_def) apply (rule corres_guard_imp) apply (rule corres_split[OF get_cap_corres]) apply (rule corres_split[OF get_cap_corres]) - apply (rule_tac F="cteCap rv' = NullCap" in corres_gen_asm2) + apply (rule_tac F="cteCap oldCTE = NullCap" in corres_gen_asm2) apply simp apply (rule_tac P="?P and cte_at dest and (\s. cte_wp_at (safe_parent_for (cdt s) src c) src s) and cte_wp_at ((=) src_cap) src" and - Q="?P' and - cte_wp_at' ((=) rv') (cte_map dest) and + Q="?P' and archMDBAssertions and + cte_wp_at' ((=) oldCTE) (cte_map dest) and cte_wp_at' ((=) srcCTE) (cte_map src) and (\s. safe_parent_for' (ctes_of s) src' c')" in corres_assert_assume) prefer 2 apply (clarsimp simp: cte_wp_at_ctes_of valid_mdb'_def valid_mdb_ctes_def valid_nullcaps_def) - apply (case_tac rv') + apply (case_tac oldCTE) apply (simp add: initMDBNode_def) apply (erule allE)+ apply (erule (1) impE) @@ -4766,7 +4776,7 @@ lemma cteInsert_simple_corres: apply (rule_tac R="\r. ?P and cte_at dest and (\s. cte_wp_at (safe_parent_for (cdt s) src c) src s) and cte_wp_at ((=) (masked_as_full src_cap c)) src" and - R'="\r. ?P' and cte_wp_at' ((=) rv') (cte_map dest) + R'="\r. ?P' and archMDBAssertions and cte_wp_at' ((=) oldCTE) (cte_map dest) and cte_wp_at' ((=) (CTE (maskedAsFull (cteCap srcCTE) c') (cteMDBNode srcCTE))) (cte_map src) and (\s. safe_parent_for' (ctes_of s) src' c')" in corres_split[where r'=dc]) @@ -4859,7 +4869,7 @@ lemma cteInsert_simple_corres: apply clarsimp apply (subgoal_tac "mdbRevocable node = revokable' (cteCap srcCTE) c'") prefer 2 - apply (case_tac rv') + apply (case_tac oldCTE) apply (clarsimp simp add: const_def modify_map_def split: if_split_asm) apply clarsimp apply (rule revokable_eq, assumption, assumption) @@ -4872,7 +4882,7 @@ lemma cteInsert_simple_corres: apply (clarsimp simp: cte_wp_at_def is_simple_cap_def) apply clarsimp apply (case_tac srcCTE) - apply (case_tac rv') + apply (case_tac oldCTE) apply clarsimp apply (subgoal_tac "\cap' node'. ctes_of b (cte_map (aa,bb)) = Some (CTE cap' node')") prefer 2 @@ -4897,14 +4907,14 @@ lemma cteInsert_simple_corres: setUntypedCapAsFull_valid_cap setUntypedCapAsFull_cte_wp_at setUntypedCapAsFull_safe_parent_for' | clarsimp | wps)+ apply (clarsimp simp:cte_wp_at_caps_of_state ) - apply (case_tac rv',clarsimp simp:cte_wp_at_ctes_of maskedAsFull_def) + apply (case_tac oldCTE,clarsimp simp:cte_wp_at_ctes_of maskedAsFull_def) apply (wp getCTE_wp' get_cap_wp)+ apply clarsimp subgoal by (fastforce elim: cte_wp_at_weakenE) subgoal by (clarsimp simp: cte_wp_at'_def) apply (case_tac "srcCTE") apply (rename_tac src_cap' src_node) - apply (case_tac "rv'") + apply (case_tac "oldCTE") apply (rename_tac dest_node) apply (clarsimp simp: in_set_cap_cte_at_swp) apply (subgoal_tac "cte_at src a \ safe_parent_for (cdt a) src c src_cap") @@ -4928,7 +4938,8 @@ lemma cteInsert_simple_corres: apply (simp (no_asm_simp) add: cdt_relation_def split: if_split) apply (intro impI allI) apply (frule mdb_insert_simple_axioms.intro) - apply(clarsimp simp:cte_wp_at_ctes_of) + apply(clarsimp simp:cte_wp_at_ctes_of) + apply (simp add: archMDBAssertions_def) apply (drule (1) mdb_insert_simple.intro) apply (drule_tac src_cap' = src_cap' in maskedAsFull_revokable_safe_parent[symmetric]) apply simp+ @@ -5812,7 +5823,7 @@ lemma cteInsert_simple_mdb': mdb_ptr_axioms.intro mdb_insert_axioms.intro) apply (simp add:modify_map_def valid_mdb_ctes_maskedAsFull)+ apply (clarsimp simp:nullPointer_def)+ - apply ((clarsimp simp:valid_mdb_ctes_def)+) + apply (clarsimp simp:valid_mdb_ctes_def archMDBAssertions_def)+ apply (drule mdb_insert_simple'.mdb) apply (clarsimp simp:valid_mdb_ctes_def) done diff --git a/proof/refine/ARM/Interrupt_R.thy b/proof/refine/ARM/Interrupt_R.thy index c4ab7d5eae..5f6460f598 100644 --- a/proof/refine/ARM/Interrupt_R.thy +++ b/proof/refine/ARM/Interrupt_R.thy @@ -489,6 +489,9 @@ lemma setIRQTrigger_corres: | simp add: dc_def)+ done +crunch set_irq_state + for valid_arch_state[wp]: valid_arch_state + lemma arch_performIRQControl_corres: "arch_irq_control_inv_relation x2 ivk' \ corres (dc \ dc) (einvs and arch_irq_control_inv_valid x2) diff --git a/proof/refine/ARM/InvariantUpdates_H.thy b/proof/refine/ARM/InvariantUpdates_H.thy index 6d2b2cd552..7bede75489 100644 --- a/proof/refine/ARM/InvariantUpdates_H.thy +++ b/proof/refine/ARM/InvariantUpdates_H.thy @@ -483,10 +483,4 @@ lemma invs'_update_cnt[elim!]: by (clarsimp simp: invs'_def valid_state'_def valid_irq_node'_def cur_tcb'_def ct_idle_or_in_cur_domain'_def tcb_in_cur_domain'_def bitmapQ_defs) -(* FIXME arch-split: valid_arch_mdb_ctes only exists to contain ioport_control on x64, and it is not - yet clear what the best way to arch-split it is, or whether it can be crossed from AInvs. - Therefore, for now, export the truth that it doesn't do anything on this arch beyond this point *) -arch_requalify_facts valid_arch_mdb_ctes_def -lemmas [simp] = valid_arch_mdb_ctes_def - end diff --git a/proof/refine/ARM/Ipc_R.thy b/proof/refine/ARM/Ipc_R.thy index 329096a33b..cc188baeaa 100644 --- a/proof/refine/ARM/Ipc_R.thy +++ b/proof/refine/ARM/Ipc_R.thy @@ -377,6 +377,10 @@ lemma cte_refs'_maskedAsFull[simp]: apply (clarsimp simp:maskedAsFull_def isCap_simps)+ done +lemma set_extra_badge_valid_arch_state[wp]: + "set_extra_badge buffer badge n \ valid_arch_state \" + unfolding set_extra_badge_def + by wp lemma transferCapsToSlots_corres: "\ list_all2 (\(cap, slot) (cap', slot'). cap_relation cap cap' @@ -384,7 +388,7 @@ lemma transferCapsToSlots_corres: mi' = message_info_map mi \ \ corres ((=) \ message_info_map) (\s. valid_objs s \ pspace_aligned s \ pspace_distinct s \ valid_mdb s - \ valid_list s + \ valid_list s \ valid_arch_state s \ (case ep of Some x \ ep_at x s | _ \ True) \ (\x \ set slots. cte_wp_at (\cap. cap = cap.NullCap) x s \ real_cte_at x s) @@ -458,7 +462,8 @@ next apply (simp add: tl_map) apply (rule corres_rel_imp, rule Cons.hyps, simp_all)[1] apply (wp valid_case_option_post_wp hoare_vcg_const_Ball_lift - hoare_vcg_const_Ball_lift cap_insert_weak_cte_wp_at) + hoare_vcg_const_Ball_lift cap_insert_derived_valid_arch_state + cap_insert_weak_cte_wp_at) apply (wp hoare_vcg_const_Ball_lift | simp add:split_def del: imp_disj1)+ apply (wp cap_insert_cte_wp_at) apply (wp valid_case_option_post_wp hoare_vcg_const_Ball_lift @@ -599,6 +604,7 @@ lemma cteInsert_assume_Null: apply (rule hoare_name_pre_state) apply (erule impCE) apply (simp add: cteInsert_def) + apply (rule bind_wp[OF _ stateAssert_sp]) apply (rule bind_wp[OF _ getCTE_sp])+ apply (rule hoare_name_pre_state) apply (clarsimp simp: cte_wp_at_ctes_of) @@ -1034,7 +1040,7 @@ lemma transferCaps_corres: corres ((=) \ message_info_map) (tcb_at receiver and valid_objs and pspace_aligned and pspace_distinct and valid_mdb - and valid_list + and valid_list and valid_arch_state and (\s. case ep of Some x \ ep_at x s | _ \ True) and case_option \ in_user_frame recv_buf and (\s. valid_message_info info) @@ -1395,10 +1401,14 @@ lemma copyMRs_valid_mdb[wp]: "\valid_mdb'\ copyMRs t buf t' buf' n \\rv. valid_mdb'\" by (simp add: valid_mdb'_def copyMRs_ctes_of) +crunch copy_mrs + for valid_arch_state[wp]: valid_arch_state + (wp: crunch_wps) + lemma doNormalTransfer_corres: "corres dc (tcb_at sender and tcb_at receiver and (pspace_aligned:: det_state \ bool) - and valid_objs and cur_tcb and valid_mdb and valid_list and pspace_distinct + and valid_objs and cur_tcb and valid_mdb and valid_list and valid_arch_state and pspace_distinct and (\s. case ep of Some x \ ep_at x s | _ \ True) and case_option \ in_user_frame send_buf and case_option \ in_user_frame recv_buf) @@ -1670,7 +1680,7 @@ lemma lookupIPCBuffer_valid_ipc_buffer [wp]: lemma doIPCTransfer_corres: "corres dc (tcb_at s and tcb_at r and valid_objs and pspace_aligned - and valid_list + and valid_list and valid_arch_state and pspace_distinct and valid_mdb and cur_tcb and (\s. case ep of Some x \ ep_at x s | _ \ True)) (tcb_at' s and tcb_at' r and valid_pspace' and cur_tcb' @@ -1678,9 +1688,9 @@ lemma doIPCTransfer_corres: (do_ipc_transfer s ep bg grt r) (doIPCTransfer s ep bg grt r)" apply (simp add: do_ipc_transfer_def doIPCTransfer_def) - apply (rule_tac Q="%receiveBuffer sa. tcb_at s sa \ valid_objs sa \ - pspace_aligned sa \ tcb_at r sa \ - cur_tcb sa \ valid_mdb sa \ valid_list sa \ pspace_distinct sa \ + apply (rule_tac Q="\receiveBuffer sa. tcb_at s sa \ valid_objs sa \ + pspace_aligned sa \ pspace_distinct sa \ tcb_at r sa \ + cur_tcb sa \ valid_mdb sa \ valid_list sa \ valid_arch_state sa \ (case ep of None \ True | Some x \ ep_at x sa) \ case_option (\_. True) in_user_frame receiveBuffer sa \ obj_at (\ko. \tcb. ko = TCB tcb @@ -2255,7 +2265,7 @@ lemma setupCallerCap_corres: (st_tcb_at (Not \ halted) sender and tcb_at receiver and st_tcb_at (Not \ awaiting_reply) sender and valid_reply_caps and valid_objs and pspace_distinct and pspace_aligned and valid_mdb - and valid_list and + and valid_list and valid_arch_state and valid_reply_masters and cte_wp_at (\c. c = cap.NullCap) (receiver, tcb_cnode_index 3)) (tcb_at' sender and tcb_at' receiver and valid_pspace' and (\s. weak_sch_act_wf (ksSchedulerAction s) s)) @@ -2469,6 +2479,7 @@ proof - valid_queues_in_correct_ready_q valid_queues_ready_qs_distinct valid_sched_valid_queues)+ apply ((wp hoare_drop_imps do_ipc_transfer_tcb_caps weak_valid_sched_action_lift + do_ipc_transfer_valid_arch | clarsimp simp: is_cap_simps)+)[1] apply (simp add: pred_conj_def) apply (strengthen sch_act_wf_weak) @@ -3191,7 +3202,7 @@ lemma receiveIPC_corres: apply (rule corres_split[OF doIPCTransfer_corres]) apply (simp split del: if_split cong: if_cong) apply (fold dc_def)[1] - apply (rule_tac P="valid_objs and valid_mdb and valid_list + apply (rule_tac P="valid_objs and valid_mdb and valid_list and valid_arch_state and valid_sched and cur_tcb and valid_reply_caps @@ -3221,7 +3232,7 @@ lemma receiveIPC_corres: apply (fastforce simp: st_tcb_at_tcb_at st_tcb_def2 valid_sched_def valid_sched_action_def) apply (clarsimp split: if_split_asm) - apply (clarsimp | wp do_ipc_transfer_tcb_caps)+ + apply (clarsimp | wp do_ipc_transfer_tcb_caps do_ipc_transfer_valid_arch)+ apply (rule_tac Q'="\_ s. sch_act_wf (ksSchedulerAction s) s \ sym_heap_sched_pointers s \ valid_sched_pointers s \ pspace_aligned' s \ pspace_distinct' s" @@ -3563,19 +3574,12 @@ lemma cteInsert_cap_to': "\ex_nonz_cap_to' p and cte_wp_at' (\c. cteCap c = NullCap) dest\ cteInsert cap src dest \\rv. ex_nonz_cap_to' p\" - apply (simp add: cteInsert_def ex_nonz_cap_to'_def - updateCap_def setUntypedCapAsFull_def - split del: if_split) - apply (rule hoare_pre, rule hoare_vcg_ex_lift) - apply (wp updateMDB_weak_cte_wp_at - setCTE_weak_cte_wp_at - | simp - | rule hoare_drop_imps)+ - apply (wp getCTE_wp) - apply clarsimp + apply (simp add: cteInsert_def ex_nonz_cap_to'_def updateCap_def setUntypedCapAsFull_def) + apply (wpsimp wp: updateMDB_weak_cte_wp_at setCTE_weak_cte_wp_at hoare_vcg_ex_lift + | rule hoare_drop_imps + | wp getCTE_wp)+ (* getCTE_wp is separate to apply it only to the last one *) apply (rule_tac x=cref in exI) - apply (rule conjI) - apply (clarsimp simp: cte_wp_at_ctes_of)+ + apply (fastforce simp: cte_wp_at_ctes_of) done crunch setExtraBadge diff --git a/proof/refine/ARM/Tcb_R.thy b/proof/refine/ARM/Tcb_R.thy index d43abb7fad..3aa6eed474 100644 --- a/proof/refine/ARM/Tcb_R.thy +++ b/proof/refine/ARM/Tcb_R.thy @@ -869,7 +869,7 @@ lemma checkCapAt_cteInsert_corres: apply clarsimp apply (rule conjI, fastforce)+ apply (cases src_slot) - apply (clarsimp simp: cte_wp_at_caps_of_state) + apply (clarsimp simp: cte_wp_at_caps_of_state invs_arch_state) apply (rule conjI) apply (frule same_object_as_cap_master) apply (clarsimp simp: cap_master_cap_simps is_cnode_or_valid_arch_def diff --git a/proof/refine/ARM_HYP/ArchInvsDefs_H.thy b/proof/refine/ARM_HYP/ArchInvsDefs_H.thy index f826e64123..1eb8f02d8c 100644 --- a/proof/refine/ARM_HYP/ArchInvsDefs_H.thy +++ b/proof/refine/ARM_HYP/ArchInvsDefs_H.thy @@ -212,9 +212,6 @@ abbreviation (input) lemmas isArchPageCap_def = isArchFrameCap_def -definition valid_arch_mdb_ctes :: "cte_heap \ bool" where - "valid_arch_mdb_ctes \ \" - definition page_directory_refs' :: "word32 \ word32 set" where "page_directory_refs' x \ (\y. x + (y << 3)) ` {y. y < 2 ^ 11}" diff --git a/proof/refine/ARM_HYP/Arch_R.thy b/proof/refine/ARM_HYP/Arch_R.thy index 57e588ebc8..77304f6673 100644 --- a/proof/refine/ARM_HYP/Arch_R.thy +++ b/proof/refine/ARM_HYP/Arch_R.thy @@ -137,6 +137,7 @@ lemma performASIDControlInvocation_corres: apply (cases i) apply (rename_tac word1 prod1 prod2 word2) apply (clarsimp simp: asid_ci_map_def) + apply (rename_tac p slot p' slot' word2) apply (simp add: perform_asid_control_invocation_def placeNewObject_def2 performASIDControlInvocation_def) apply (rule corres_name_pre) @@ -194,7 +195,7 @@ lemma performASIDControlInvocation_corres: apply wp+ apply (strengthen safe_parent_strg[where idx = "2^pageBits"]) apply (strengthen invs_valid_objs invs_distinct - invs_psp_aligned invs_mdb + invs_psp_aligned invs_mdb invs_arch_state | simp cong:conj_cong)+ apply (wp retype_region_plain_invs[where sz = pageBits] retype_cte_wp_at[where sz = pageBits])+ @@ -278,7 +279,7 @@ lemma performASIDControlInvocation_corres: apply (drule detype_locale.non_null_present) apply (fastforce simp:cte_wp_at_caps_of_state) apply simp - apply (frule_tac ptr = "(aa,ba)" in detype_invariants [rotated 3]) + apply (frule_tac ptr = "(p', slot')" in detype_invariants [rotated 3]) apply fastforce apply simp apply (simp add: cte_wp_at_caps_of_state) @@ -305,7 +306,7 @@ lemma performASIDControlInvocation_corres: apply (simp add:empty_descendants_range_in)+ apply (rule conjI) apply clarsimp - apply (drule_tac p = "(aa,ba)" in cap_refs_in_kernel_windowD2[OF caps_of_state_cteD]) + apply (drule_tac p = "(p', slot')" in cap_refs_in_kernel_windowD2[OF caps_of_state_cteD]) apply fastforce apply (clarsimp simp: region_in_kernel_window_def valid_cap_def cap_aligned_def is_aligned_neg_mask_eq detype_def clear_um_def) @@ -315,7 +316,7 @@ lemma performASIDControlInvocation_corres: apply (clarsimp simp: detype_def clear_um_def detype_ext_def valid_sched_def valid_etcbs_def st_tcb_at_kh_def obj_at_kh_def st_tcb_at_def obj_at_def is_etcb_at_def) apply (simp add: detype_def clear_um_def) - apply (drule_tac x = "cte_map (aa,ba)" in pspace_relation_cte_wp_atI[OF state_relation_pspace_relation]) + apply (drule_tac x = "cte_map (p', slot')" in pspace_relation_cte_wp_atI[OF state_relation_pspace_relation]) apply (simp add:invs_valid_objs)+ apply clarsimp apply (drule cte_map_inj_eq) diff --git a/proof/refine/ARM_HYP/CNodeInv_R.thy b/proof/refine/ARM_HYP/CNodeInv_R.thy index 43e571cf7a..5c4221469b 100644 --- a/proof/refine/ARM_HYP/CNodeInv_R.thy +++ b/proof/refine/ARM_HYP/CNodeInv_R.thy @@ -8466,9 +8466,6 @@ proof apply (erule (1) irq_controlD, rule irq_control) done - show "valid_arch_mdb_ctes m'" - by simp - have distz: "distinct_zombies m" using valid by (simp add: valid_mdb_ctes_def) diff --git a/proof/refine/ARM_HYP/CSpace1_R.thy b/proof/refine/ARM_HYP/CSpace1_R.thy index fefddf70c1..7add6866a8 100644 --- a/proof/refine/ARM_HYP/CSpace1_R.thy +++ b/proof/refine/ARM_HYP/CSpace1_R.thy @@ -14,6 +14,20 @@ imports "AInvs.ArchDetSchedSchedule_AI" begin +context Arch begin arch_global_naming + +(* No assertion necessary for this architecture. *) +definition arch_mdb_assert :: "cte_heap \ bool" where + "arch_mdb_assert m \ True" + +end + +arch_requalify_consts + arch_mdb_assert + +defs archMDBAssertions_def: + "archMDBAssertions s \ arch_mdb_assert (ctes_of s)" + context Arch begin global_naming ARM_HYP_A (*FIXME: arch-split*) lemmas final_matters_def = final_matters_def[simplified final_matters_arch_def] @@ -250,7 +264,7 @@ lemma pspace_relation_cte_wp_at: lemma pspace_relation_ctes_ofI: "\ pspace_relation (kheap s) (ksPSpace s'); - cte_wp_at ((=) c) slot s; pspace_aligned' s'; + cte_wp_at ((=) c) slot s; pspace_aligned' s'; pspace_distinct' s' \ \ \cte. ctes_of s' (cte_map slot) = Some cte \ cap_relation c (cteCap cte)" apply (cases slot, clarsimp) @@ -258,6 +272,22 @@ lemma pspace_relation_ctes_ofI: apply (simp add: cte_wp_at_ctes_of) done +lemma pspace_relation_caps_of_state_cross: + "\ pspace_relation (kheap s) (ksPSpace s'); + caps_of_state s slot = Some c; pspace_aligned s; pspace_distinct s \ + \ \cte. ctes_of s' (cte_map slot) = Some cte \ cap_relation c (cteCap cte)" + for s' :: kernel_state + by (auto simp: cte_wp_at_caps_of_state + intro!: pspace_relation_ctes_ofI pspace_aligned_cross pspace_distinct_cross) + +lemma caps_of_state_cross: + "\ caps_of_state s slot = Some cap; pspace_aligned s; pspace_distinct s; (s,s') \ state_relation \ + \ \cap'. cteCaps_of s' (cte_map slot) = Some cap' \ cap_relation cap cap'" + apply (erule state_relationE) + apply (drule (3) pspace_relation_caps_of_state_cross) + apply (fastforce simp: cteCaps_of_def) + done + lemma get_cap_corres_P: "corres (\x y. cap_relation x (cteCap y) \ P x) (cte_wp_at P cslot_ptr) @@ -907,21 +937,13 @@ lemma ctes_of_valid_cap'': done lemma cap_insert_objs' [wp]: - "\valid_objs' - and valid_cap' cap\ - cteInsert cap src dest \\rv. valid_objs'\" - including no_pre - apply (simp add: cteInsert_def updateCap_def setUntypedCapAsFull_def bind_assoc split del: if_split) - apply (wp setCTE_valid_objs) - apply simp - apply wp+ - apply (clarsimp simp: updateCap_def) - apply (wp|simp)+ - apply (rule hoare_drop_imp)+ - apply wp+ - apply (rule hoare_strengthen_post[OF getCTE_sp]) + "\valid_objs' and valid_cap' cap\ + cteInsert cap src dest + \\_. valid_objs'\" + apply (simp add: cteInsert_def updateCap_def setUntypedCapAsFull_def) + apply (wpsimp wp: setCTE_valid_objs | wp getCTE_wp')+ apply (clarsimp simp: cte_wp_at_ctes_of isCap_simps - dest!: ctes_of_valid_cap'') + dest!: ctes_of_valid_cap'') done lemma cteInsert_weak_cte_wp_at: @@ -1970,6 +1992,14 @@ lemma pspace_relation_cte_wp_atI: apply assumption done +lemma caps_of_state_rev_cross: + "\ ctes_of s' p = Some cte; valid_objs s; (s,s') \ state_relation \ + \ \cap slot. caps_of_state s slot = Some cap \ p = cte_map slot \ cap_relation cap (cteCap cte)" + apply (erule state_relationE) + apply (drule (2) pspace_relation_cte_wp_atI) + apply (fastforce simp: cte_wp_at_caps_of_state) + done + lemma sameRegion_corres: "\ sameRegionAs c' d'; cap_relation c c'; cap_relation d d' \ \ same_region_as c d" @@ -5229,6 +5259,15 @@ lemma cte_map_inj_eq': done context begin interpretation Arch . (*FIXME: arch-split*) + +(* interface lemma: generic statement, arch-specific proof *) +lemma archMDBAssertions_cross: + "\ valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_arch_state s; valid_objs s; + (s, s') \ state_relation \ + \ archMDBAssertions s'" + unfolding archMDBAssertions_def + by (simp add: arch_mdb_assert_def) + lemma cteInsert_corres: notes split_paired_All[simp del] split_paired_Ex[simp del] trans_state_update'[symmetric,simp] @@ -5237,30 +5276,33 @@ lemma cteInsert_corres: (valid_objs and pspace_distinct and pspace_aligned and valid_mdb and valid_list and K (src\dest) and cte_wp_at (\c. c=Structures_A.NullCap) dest and - (\s. cte_wp_at (is_derived (cdt s) src c) src s)) + (\s. cte_wp_at (is_derived (cdt s) src c) src s) and valid_arch_state) (pspace_distinct' and pspace_aligned' and valid_mdb' and valid_cap' c' and cte_wp_at' (\c. cteCap c=NullCap) dest') (cap_insert c src dest) (cteInsert c' src' dest')" - (is "corres _ (?P and (\s. cte_wp_at _ _ s)) (?P' and cte_wp_at' _ _) _ _") + (is "corres _ (?P and (\s. cte_wp_at _ _ s) and valid_arch_state) (?P' and cte_wp_at' _ _) _ _") using assms unfolding cap_insert_def cteInsert_def apply simp + (* this lemma doesn't use the assertion, but does need to establish it *) + apply (rule corres_stateAssert_add_assertion[rotated]) + apply (rule archMDBAssertions_cross; simp add: valid_mdb_def) apply (rule corres_guard_imp) apply (rule corres_split[OF get_cap_corres]) apply (rule corres_split[OF get_cap_corres]) - apply (rule_tac F="cteCap rv' = NullCap" in corres_gen_asm2) + apply (rule_tac F="cteCap oldCTE = NullCap" in corres_gen_asm2) apply simp apply (rule_tac P="?P and cte_at dest and (\s. cte_wp_at (is_derived (cdt s) src c) src s) and cte_wp_at ((=) src_cap) src" and Q="?P' and - cte_wp_at' ((=) rv') (cte_map dest) and + cte_wp_at' ((=) oldCTE) (cte_map dest) and cte_wp_at' ((=) srcCTE) (cte_map src)" in corres_assert_assume) prefer 2 apply (clarsimp simp: cte_wp_at_ctes_of valid_mdb'_def valid_mdb_ctes_def valid_nullcaps_def) - apply (case_tac rv') + apply (case_tac oldCTE) apply (simp add: initMDBNode_def) apply (erule allE)+ apply (erule (1) impE) @@ -5269,7 +5311,7 @@ lemma cteInsert_corres: apply (rule_tac R="\r. ?P and cte_at dest and (\s. (is_derived (cdt s) src c) src_cap) and cte_wp_at ((=) (masked_as_full src_cap c)) src" and - R'="\r. ?P' and cte_wp_at' ((=) rv') (cte_map dest) and + R'="\r. ?P' and cte_wp_at' ((=) oldCTE) (cte_map dest) and cte_wp_at' ((=) (CTE (maskedAsFull (cteCap srcCTE) c') (cteMDBNode srcCTE))) (cte_map src)" in corres_split[where r'=dc]) @@ -5353,7 +5395,7 @@ lemma cteInsert_corres: apply(rule conjI) apply (case_tac "srcCTE") apply (rename_tac src_cap' src_node) - apply (case_tac "rv'") + apply (case_tac "oldCTE") apply (rename_tac dest_node) apply (clarsimp simp: in_set_cap_cte_at_swp) apply (subgoal_tac "cte_at src a \ is_derived (cdt a) src c src_cap") @@ -5640,7 +5682,7 @@ lemma cteInsert_corres: apply clarsimp apply (subgoal_tac "mdbRevocable node = revokable' (cteCap srcCTE) c'") prefer 2 - apply (case_tac rv') + apply (case_tac oldCTE) subgoal by (clarsimp simp add: const_def modify_map_def split: if_split_asm) apply simp apply (rule revokable_eq, assumption, assumption) @@ -5653,7 +5695,7 @@ lemma cteInsert_corres: split:if_splits dest!:cap_master_cap_eqDs) apply clarsimp apply (case_tac srcCTE) - apply (case_tac rv') + apply (case_tac oldCTE) apply clarsimp apply (subgoal_tac "\cap' node'. ctes_of b (cte_map (aa,bb)) = Some (CTE cap' node')") prefer 2 @@ -5680,14 +5722,14 @@ lemma cteInsert_corres: apply (wp set_untyped_cap_full_valid_objs set_untyped_cap_as_full_valid_mdb set_untyped_cap_as_full_cte_wp_at setUntypedCapAsFull_valid_cap setUntypedCapAsFull_cte_wp_at | clarsimp simp: cte_wp_at_caps_of_state| wps)+ - apply (case_tac rv',clarsimp simp:cte_wp_at_ctes_of maskedAsFull_def) + apply (case_tac oldCTE,clarsimp simp:cte_wp_at_ctes_of maskedAsFull_def) apply (wp getCTE_wp' get_cap_wp)+ apply clarsimp subgoal by (fastforce elim: cte_wp_at_weakenE) apply (clarsimp simp: cte_wp_at'_def) apply (case_tac "srcCTE") apply (rename_tac src_cap' src_node) - apply (case_tac "rv'") + apply (case_tac "oldCTE") apply (rename_tac dest_node) apply (clarsimp simp: in_set_cap_cte_at_swp) apply (subgoal_tac "cte_at src a \ is_derived (cdt a) src c src_cap") diff --git a/proof/refine/ARM_HYP/CSpace_R.thy b/proof/refine/ARM_HYP/CSpace_R.thy index b1af243a36..9854d4cfef 100644 --- a/proof/refine/ARM_HYP/CSpace_R.thy +++ b/proof/refine/ARM_HYP/CSpace_R.thy @@ -4582,6 +4582,7 @@ end locale mdb_insert_simple = mdb_insert + assumes safe_parent: "safe_parent_for' m src c'" assumes simple: "is_simple_cap' c'" + assumes arch_mdb_assert: "arch_mdb_assert m" begin interpretation Arch . (*FIXME: arch-split*) lemma dest_no_parent_n: @@ -4774,6 +4775,13 @@ lemma maskedAsFull_revokable_safe_parent: done context begin interpretation Arch . (*FIXME: arch-split*) + +(* FIXME arch-split: generic statement, arch specific proof *) +lemma setUntypedCapAsFull_archMDBAssertions[wp]: + "setUntypedCapAsFull src_cap cap p \archMDBAssertions\" + unfolding archMDBAssertions_def arch_mdb_assert_def + by wp + lemma cteInsert_simple_corres: assumes "cap_relation c c'" "src' = cte_map src" "dest' = cte_map dest" notes trans_state_update'[symmetric,simp] @@ -4782,34 +4790,36 @@ lemma cteInsert_simple_corres: valid_mdb and valid_list and K (src\dest) and cte_wp_at (\c. c=cap.NullCap) dest and K (is_simple_cap c) and - (\s. cte_wp_at (safe_parent_for (cdt s) src c) src s)) + (\s. cte_wp_at (safe_parent_for (cdt s) src c) src s) and valid_arch_state) (pspace_distinct' and pspace_aligned' and valid_mdb' and valid_cap' c' and K (is_simple_cap' c') and cte_wp_at' (\c. cteCap c=NullCap) dest' and (\s. safe_parent_for' (ctes_of s) src' c')) (cap_insert c src dest) (cteInsert c' src' dest')" - (is "corres _ (?P and (\s. cte_wp_at _ _ s)) (?P' and cte_wp_at' _ _ and _) _ _") + (is "corres _ (?P and (\s. cte_wp_at _ _ s) and valid_arch_state) (?P' and cte_wp_at' _ _ and _) _ _") using assms unfolding cap_insert_def cteInsert_def supply subst_all [simp del] apply simp + apply (rule corres_stateAssert_add_assertion[rotated]) + apply (rule archMDBAssertions_cross; simp add: valid_mdb_def) apply (rule corres_guard_imp) apply (rule corres_split[OF get_cap_corres]) apply (rule corres_split[OF get_cap_corres]) - apply (rule_tac F="cteCap rv' = NullCap" in corres_gen_asm2) + apply (rule_tac F="cteCap oldCTE = NullCap" in corres_gen_asm2) apply simp apply (rule_tac P="?P and cte_at dest and (\s. cte_wp_at (safe_parent_for (cdt s) src c) src s) and cte_wp_at ((=) src_cap) src" and - Q="?P' and - cte_wp_at' ((=) rv') (cte_map dest) and + Q="?P' and archMDBAssertions and + cte_wp_at' ((=) oldCTE) (cte_map dest) and cte_wp_at' ((=) srcCTE) (cte_map src) and (\s. safe_parent_for' (ctes_of s) src' c')" in corres_assert_assume) prefer 2 apply (clarsimp simp: cte_wp_at_ctes_of valid_mdb'_def valid_mdb_ctes_def valid_nullcaps_def) - apply (case_tac rv') + apply (case_tac oldCTE) apply (simp add: initMDBNode_def) apply (erule allE)+ apply (erule (1) impE) @@ -4818,7 +4828,7 @@ lemma cteInsert_simple_corres: apply (rule_tac R="\r. ?P and cte_at dest and (\s. cte_wp_at (safe_parent_for (cdt s) src c) src s) and cte_wp_at ((=) (masked_as_full src_cap c)) src" and - R'="\r. ?P' and cte_wp_at' ((=) rv') (cte_map dest) + R'="\r. ?P' and archMDBAssertions and cte_wp_at' ((=) oldCTE) (cte_map dest) and cte_wp_at' ((=) (CTE (maskedAsFull (cteCap srcCTE) c') (cteMDBNode srcCTE))) (cte_map src) and (\s. safe_parent_for' (ctes_of s) src' c')" in corres_split[where r'=dc]) @@ -4911,7 +4921,7 @@ lemma cteInsert_simple_corres: apply clarsimp apply (subgoal_tac "mdbRevocable node = revokable' (cteCap srcCTE) c'") prefer 2 - apply (case_tac rv') + apply (case_tac oldCTE) apply (clarsimp simp add: const_def modify_map_def split: if_split_asm) apply clarsimp apply (rule revokable_eq, assumption, assumption) @@ -4924,7 +4934,7 @@ lemma cteInsert_simple_corres: apply (clarsimp simp: cte_wp_at_def is_simple_cap_def) apply clarsimp apply (case_tac srcCTE) - apply (case_tac rv') + apply (case_tac oldCTE) apply clarsimp apply (subgoal_tac "\cap' node'. ctes_of b (cte_map (aa,bb)) = Some (CTE cap' node')") prefer 2 @@ -4949,14 +4959,14 @@ lemma cteInsert_simple_corres: setUntypedCapAsFull_valid_cap setUntypedCapAsFull_cte_wp_at setUntypedCapAsFull_safe_parent_for' | clarsimp | wps)+ apply (clarsimp simp:cte_wp_at_caps_of_state ) - apply (case_tac rv',clarsimp simp:cte_wp_at_ctes_of maskedAsFull_def) + apply (case_tac oldCTE,clarsimp simp:cte_wp_at_ctes_of maskedAsFull_def) apply (wp getCTE_wp' get_cap_wp)+ apply clarsimp subgoal by (fastforce elim: cte_wp_at_weakenE) subgoal by (clarsimp simp: cte_wp_at'_def) apply (case_tac "srcCTE") apply (rename_tac src_cap' src_node) - apply (case_tac "rv'") + apply (case_tac "oldCTE") apply (rename_tac dest_node) apply (clarsimp simp: in_set_cap_cte_at_swp) apply (subgoal_tac "cte_at src a \ safe_parent_for (cdt a) src c src_cap") @@ -4980,7 +4990,8 @@ lemma cteInsert_simple_corres: apply (simp (no_asm_simp) add: cdt_relation_def split: if_split) apply (intro impI allI) apply (frule mdb_insert_simple_axioms.intro) - apply(clarsimp simp:cte_wp_at_ctes_of) + apply(clarsimp simp:cte_wp_at_ctes_of) + apply (simp add: archMDBAssertions_def) apply (drule (1) mdb_insert_simple.intro) apply (drule_tac src_cap' = src_cap' in maskedAsFull_revokable_safe_parent[symmetric]) apply simp+ @@ -5879,7 +5890,7 @@ lemma cteInsert_simple_mdb': mdb_ptr_axioms.intro mdb_insert_axioms.intro) apply (simp add:modify_map_def valid_mdb_ctes_maskedAsFull)+ apply (clarsimp simp:nullPointer_def)+ - apply ((clarsimp simp:valid_mdb_ctes_def)+) + apply (clarsimp simp:valid_mdb_ctes_def archMDBAssertions_def)+ apply (drule mdb_insert_simple'.mdb) apply (clarsimp simp:valid_mdb_ctes_def) done diff --git a/proof/refine/ARM_HYP/Interrupt_R.thy b/proof/refine/ARM_HYP/Interrupt_R.thy index 2c7c17c4a4..b4c25ad1d6 100644 --- a/proof/refine/ARM_HYP/Interrupt_R.thy +++ b/proof/refine/ARM_HYP/Interrupt_R.thy @@ -475,6 +475,9 @@ lemma setIRQTrigger_corres: | simp add: dc_def)+ done +crunch set_irq_state + for valid_arch_state[wp]: valid_arch_state + lemma arch_performIRQControl_corres: "arch_irq_control_inv_relation x2 ivk' \ corres (dc \ dc) (einvs and arch_irq_control_inv_valid x2) diff --git a/proof/refine/ARM_HYP/InvariantUpdates_H.thy b/proof/refine/ARM_HYP/InvariantUpdates_H.thy index f845fba319..d0fe35e942 100644 --- a/proof/refine/ARM_HYP/InvariantUpdates_H.thy +++ b/proof/refine/ARM_HYP/InvariantUpdates_H.thy @@ -483,10 +483,4 @@ lemma invs'_update_cnt[elim!]: by (clarsimp simp: invs'_def valid_state'_def valid_irq_node'_def cur_tcb'_def ct_idle_or_in_cur_domain'_def tcb_in_cur_domain'_def bitmapQ_defs) -(* FIXME arch-split: valid_arch_mdb_ctes only exists to contain ioport_control on x64, and it is not - yet clear what the best way to arch-split it is, or whether it can be crossed from AInvs. - Therefore, for now, export the truth that it doesn't do anything on this arch beyond this point *) -arch_requalify_facts valid_arch_mdb_ctes_def -lemmas [simp] = valid_arch_mdb_ctes_def - end diff --git a/proof/refine/ARM_HYP/Ipc_R.thy b/proof/refine/ARM_HYP/Ipc_R.thy index 13d9da30da..c8914e1314 100644 --- a/proof/refine/ARM_HYP/Ipc_R.thy +++ b/proof/refine/ARM_HYP/Ipc_R.thy @@ -388,6 +388,10 @@ lemma cte_refs'_maskedAsFull[simp]: apply (clarsimp simp:maskedAsFull_def isCap_simps)+ done +lemma set_extra_badge_valid_arch_state[wp]: + "set_extra_badge buffer badge n \ valid_arch_state \" + unfolding set_extra_badge_def + by wp lemma transferCapsToSlots_corres: "\ list_all2 (\(cap, slot) (cap', slot'). cap_relation cap cap' @@ -395,7 +399,7 @@ lemma transferCapsToSlots_corres: mi' = message_info_map mi \ \ corres ((=) \ message_info_map) (\s. valid_objs s \ pspace_aligned s \ pspace_distinct s \ valid_mdb s - \ valid_list s + \ valid_list s \ valid_arch_state s \ (case ep of Some x \ ep_at x s | _ \ True) \ (\x \ set slots. cte_wp_at (\cap. cap = cap.NullCap) x s \ real_cte_at x s) @@ -469,7 +473,8 @@ next apply (simp add: tl_map) apply (rule corres_rel_imp, rule Cons.hyps, simp_all)[1] apply (wp valid_case_option_post_wp hoare_vcg_const_Ball_lift - hoare_vcg_const_Ball_lift cap_insert_weak_cte_wp_at) + hoare_vcg_const_Ball_lift cap_insert_derived_valid_arch_state + cap_insert_weak_cte_wp_at) apply (wp hoare_vcg_const_Ball_lift | simp add:split_def del: imp_disj1)+ apply (wp cap_insert_cte_wp_at) apply (wp valid_case_option_post_wp hoare_vcg_const_Ball_lift @@ -610,6 +615,7 @@ lemma cteInsert_assume_Null: apply (rule hoare_name_pre_state) apply (erule impCE) apply (simp add: cteInsert_def) + apply (rule bind_wp[OF _ stateAssert_sp]) apply (rule bind_wp[OF _ getCTE_sp])+ apply (rule hoare_name_pre_state) apply (clarsimp simp: cte_wp_at_ctes_of) @@ -1052,7 +1058,7 @@ lemma transferCaps_corres: corres ((=) \ message_info_map) (tcb_at receiver and valid_objs and pspace_aligned and pspace_distinct and valid_mdb - and valid_list + and valid_list and valid_arch_state and (\s. case ep of Some x \ ep_at x s | _ \ True) and case_option \ in_user_frame recv_buf and (\s. valid_message_info info) @@ -1458,10 +1464,14 @@ lemma copyMRs_valid_mdb[wp]: "\valid_mdb'\ copyMRs t buf t' buf' n \\rv. valid_mdb'\" by (simp add: valid_mdb'_def copyMRs_ctes_of) +crunch copy_mrs + for valid_arch_state[wp]: valid_arch_state + (wp: crunch_wps) + lemma doNormalTransfer_corres: "corres dc (tcb_at sender and tcb_at receiver and (pspace_aligned:: det_state \ bool) - and valid_objs and cur_tcb and valid_mdb and valid_list and pspace_distinct + and valid_objs and cur_tcb and valid_mdb and valid_list and valid_arch_state and pspace_distinct and (\s. case ep of Some x \ ep_at x s | _ \ True) and case_option \ in_user_frame send_buf and case_option \ in_user_frame recv_buf) @@ -1768,7 +1778,7 @@ lemma lookupIPCBuffer_valid_ipc_buffer [wp]: lemma doIPCTransfer_corres: "corres dc (tcb_at s and tcb_at r and valid_objs and pspace_aligned - and valid_list + and valid_list and valid_arch_state and pspace_distinct and valid_mdb and cur_tcb and (\s. case ep of Some x \ ep_at x s | _ \ True)) (tcb_at' s and tcb_at' r and valid_pspace' and cur_tcb' @@ -1776,9 +1786,9 @@ lemma doIPCTransfer_corres: (do_ipc_transfer s ep bg grt r) (doIPCTransfer s ep bg grt r)" apply (simp add: do_ipc_transfer_def doIPCTransfer_def) - apply (rule_tac Q="%receiveBuffer sa. tcb_at s sa \ valid_objs sa \ - pspace_aligned sa \ tcb_at r sa \ - cur_tcb sa \ valid_mdb sa \ valid_list sa \ pspace_distinct sa \ + apply (rule_tac Q="\receiveBuffer sa. tcb_at s sa \ valid_objs sa \ + pspace_aligned sa \ pspace_distinct sa \ tcb_at r sa \ + cur_tcb sa \ valid_mdb sa \ valid_list sa \ valid_arch_state sa \ (case ep of None \ True | Some x \ ep_at x sa) \ case_option (\_. True) in_user_frame receiveBuffer sa \ obj_at (\ko. \tcb. ko = TCB tcb @@ -2386,7 +2396,7 @@ lemma setupCallerCap_corres: (st_tcb_at (Not \ halted) sender and tcb_at receiver and st_tcb_at (Not \ awaiting_reply) sender and valid_reply_caps and valid_objs and pspace_distinct and pspace_aligned and valid_mdb - and valid_list and + and valid_list and valid_arch_state and valid_reply_masters and cte_wp_at (\c. c = cap.NullCap) (receiver, tcb_cnode_index 3)) (tcb_at' sender and tcb_at' receiver and valid_pspace' and (\s. weak_sch_act_wf (ksSchedulerAction s) s)) @@ -2603,6 +2613,7 @@ proof - valid_queues_in_correct_ready_q valid_queues_ready_qs_distinct valid_sched_valid_queues)+ apply ((wp hoare_drop_imps do_ipc_transfer_tcb_caps weak_valid_sched_action_lift + do_ipc_transfer_valid_arch | clarsimp simp: is_cap_simps)+)[1] apply (simp add: pred_conj_def) apply (strengthen sch_act_wf_weak) @@ -3328,7 +3339,7 @@ lemma receiveIPC_corres: apply (rule corres_split[OF doIPCTransfer_corres]) apply (simp split del: if_split cong: if_cong) apply (fold dc_def)[1] - apply (rule_tac P="valid_objs and valid_mdb and valid_list + apply (rule_tac P="valid_objs and valid_mdb and valid_list and valid_arch_state and valid_sched and cur_tcb and valid_reply_caps @@ -3358,7 +3369,7 @@ lemma receiveIPC_corres: apply (fastforce simp: st_tcb_at_tcb_at st_tcb_def2 valid_sched_def valid_sched_action_def) apply (clarsimp split: if_split_asm) - apply (clarsimp | wp do_ipc_transfer_tcb_caps)+ + apply (clarsimp | wp do_ipc_transfer_tcb_caps do_ipc_transfer_valid_arch)+ apply (rule_tac Q'="\_ s. sch_act_wf (ksSchedulerAction s) s \ sym_heap_sched_pointers s \ valid_sched_pointers s \ pspace_aligned' s \ pspace_distinct' s" @@ -3713,19 +3724,12 @@ lemma cteInsert_cap_to': "\ex_nonz_cap_to' p and cte_wp_at' (\c. cteCap c = NullCap) dest\ cteInsert cap src dest \\rv. ex_nonz_cap_to' p\" - apply (simp add: cteInsert_def ex_nonz_cap_to'_def - updateCap_def setUntypedCapAsFull_def - split del: if_split) - apply (rule hoare_pre, rule hoare_vcg_ex_lift) - apply (wp updateMDB_weak_cte_wp_at - setCTE_weak_cte_wp_at - | simp - | rule hoare_drop_imps)+ - apply (wp getCTE_wp) - apply clarsimp + apply (simp add: cteInsert_def ex_nonz_cap_to'_def updateCap_def setUntypedCapAsFull_def) + apply (wpsimp wp: updateMDB_weak_cte_wp_at setCTE_weak_cte_wp_at hoare_vcg_ex_lift + | rule hoare_drop_imps + | wp getCTE_wp)+ (* getCTE_wp is separate to apply it only to the last one *) apply (rule_tac x=cref in exI) - apply (rule conjI) - apply (clarsimp simp: cte_wp_at_ctes_of)+ + apply (fastforce simp: cte_wp_at_ctes_of) done crunch setExtraBadge diff --git a/proof/refine/ARM_HYP/Tcb_R.thy b/proof/refine/ARM_HYP/Tcb_R.thy index 849d926639..1fc409c811 100644 --- a/proof/refine/ARM_HYP/Tcb_R.thy +++ b/proof/refine/ARM_HYP/Tcb_R.thy @@ -875,7 +875,7 @@ lemma checkCapAt_cteInsert_corres: apply clarsimp apply (rule conjI, fastforce)+ apply (cases src_slot) - apply (clarsimp simp: cte_wp_at_caps_of_state) + apply (clarsimp simp: cte_wp_at_caps_of_state invs_arch_state) apply (rule conjI) apply (frule same_object_as_cap_master) apply (clarsimp simp: cap_master_cap_simps is_cnode_or_valid_arch_def diff --git a/proof/refine/Invariants_H.thy b/proof/refine/Invariants_H.thy index ac27d25067..6e39984a86 100644 --- a/proof/refine/Invariants_H.thy +++ b/proof/refine/Invariants_H.thy @@ -26,7 +26,6 @@ arch_requalify_consts global_refs' valid_arch_state' archMakeObjectT - valid_arch_mdb_ctes pspace_in_kernel_mappings' kernel_data_refs kernel_mappings @@ -413,8 +412,6 @@ where "valid_objs' s \ \obj \ ran (ksPSpace s). valid_obj' obj s" -type_synonym cte_heap = "machine_word \ cte option" - definition map_to_ctes :: "(machine_word \ kernel_object) \ cte_heap" where @@ -640,8 +637,7 @@ where mdb_chunked m \ untyped_mdb' m \ untyped_inc' m \ valid_nullcaps m \ ut_revocable' m \ class_links m \ distinct_zombies m - \ irq_control m \ reply_masters_rvk_fb m - \ valid_arch_mdb_ctes m" + \ irq_control m \ reply_masters_rvk_fb m" definition valid_mdb' :: "kernel_state \ bool" @@ -2215,7 +2211,7 @@ lemma valid_mdb_ctesI [intro]: caps_contained' m; mdb_chunked m; untyped_mdb' m; untyped_inc' m; valid_nullcaps m; ut_revocable' m; class_links m; distinct_zombies m; irq_control m; - reply_masters_rvk_fb m; valid_arch_mdb_ctes m \ + reply_masters_rvk_fb m \ \ valid_mdb_ctes m" unfolding valid_mdb_ctes_def by auto diff --git a/proof/refine/RISCV64/ArchInvsDefs_H.thy b/proof/refine/RISCV64/ArchInvsDefs_H.thy index cd57e941e5..21af5588b2 100644 --- a/proof/refine/RISCV64/ArchInvsDefs_H.thy +++ b/proof/refine/RISCV64/ArchInvsDefs_H.thy @@ -159,9 +159,6 @@ definition where "isArchFrameCap cap \ case cap of ArchObjectCap (FrameCap _ _ _ _ _) \ True | _ \ False" -definition valid_arch_mdb_ctes :: "cte_heap \ bool" where - "valid_arch_mdb_ctes \ \" - (* Addresses of all PTEs in a VSRoot table at p *) definition table_refs' :: "machine_word \ machine_word set" where "table_refs' x \ (\y. x + (y << pte_bits)) ` mask_range 0 ptTranslationBits" diff --git a/proof/refine/RISCV64/Arch_R.thy b/proof/refine/RISCV64/Arch_R.thy index 6b741ce77d..eed3ceaa1b 100644 --- a/proof/refine/RISCV64/Arch_R.thy +++ b/proof/refine/RISCV64/Arch_R.thy @@ -142,6 +142,7 @@ lemma performASIDControlInvocation_corres: apply (cases i) apply (rename_tac word1 prod1 prod2 word2) apply (clarsimp simp: asid_ci_map_def) + apply (rename_tac p slot p' slot' word2) apply (simp add: perform_asid_control_invocation_def placeNewObject_def2 performASIDControlInvocation_def) apply (rule corres_name_pre) @@ -193,7 +194,7 @@ lemma performASIDControlInvocation_corres: apply wp+ apply (strengthen safe_parent_strg[where idx = "2^pageBits"]) apply (strengthen invs_valid_objs invs_distinct - invs_psp_aligned invs_mdb + invs_psp_aligned invs_mdb invs_arch_state | simp cong:conj_cong)+ apply (wp retype_region_plain_invs[where sz = pageBits] retype_cte_wp_at[where sz = pageBits])+ @@ -277,7 +278,7 @@ lemma performASIDControlInvocation_corres: apply (drule detype_locale.non_null_present) apply (fastforce simp: cte_wp_at_caps_of_state) apply simp - apply (frule_tac ptr = "(aa,ba)" in detype_invariants [rotated 3]) + apply (frule_tac ptr = "(p', slot')" in detype_invariants [rotated 3]) apply fastforce apply simp apply (simp add: cte_wp_at_caps_of_state) @@ -302,7 +303,7 @@ lemma performASIDControlInvocation_corres: apply (simp add:detype_clear_um_independent) apply (rule conjI) apply clarsimp - apply (drule_tac p = "(aa,ba)" in cap_refs_in_kernel_windowD2[OF caps_of_state_cteD]) + apply (drule_tac p = "(p', slot')" in cap_refs_in_kernel_windowD2[OF caps_of_state_cteD]) apply fastforce apply (clarsimp simp: region_in_kernel_window_def valid_cap_def cap_aligned_def is_aligned_neg_mask_eq detype_def clear_um_def) @@ -316,7 +317,7 @@ lemma performASIDControlInvocation_corres: apply (clarsimp simp: detype_def clear_um_def detype_ext_def valid_sched_def valid_etcbs_def st_tcb_at_kh_def obj_at_kh_def st_tcb_at_def obj_at_def is_etcb_at_def) apply (simp add: detype_def clear_um_def) - apply (drule_tac x = "cte_map (aa,ba)" in pspace_relation_cte_wp_atI[OF state_relation_pspace_relation]) + apply (drule_tac x = "cte_map (p', slot')" in pspace_relation_cte_wp_atI[OF state_relation_pspace_relation]) apply (simp add:invs_valid_objs)+ apply clarsimp apply (drule cte_map_inj_eq) diff --git a/proof/refine/RISCV64/CNodeInv_R.thy b/proof/refine/RISCV64/CNodeInv_R.thy index 8c635d667a..6962fbd4f3 100644 --- a/proof/refine/RISCV64/CNodeInv_R.thy +++ b/proof/refine/RISCV64/CNodeInv_R.thy @@ -8376,9 +8376,6 @@ proof apply (erule (1) irq_controlD, rule irq_control) done - show "valid_arch_mdb_ctes m'" - by simp - have distz: "distinct_zombies m" using valid by (simp add: valid_mdb_ctes_def) diff --git a/proof/refine/RISCV64/CSpace1_R.thy b/proof/refine/RISCV64/CSpace1_R.thy index 48de02a89a..559504641f 100644 --- a/proof/refine/RISCV64/CSpace1_R.thy +++ b/proof/refine/RISCV64/CSpace1_R.thy @@ -13,6 +13,20 @@ imports CSpace_I begin +context Arch begin arch_global_naming + +(* No assertion necessary for this architecture. *) +definition arch_mdb_assert :: "cte_heap \ bool" where + "arch_mdb_assert m \ True" + +end + +arch_requalify_consts + arch_mdb_assert + +defs archMDBAssertions_def: + "archMDBAssertions s \ arch_mdb_assert (ctes_of s)" + context Arch begin global_naming RISCV64_A (*FIXME: arch-split*) lemmas final_matters_def = final_matters_def[simplified final_matters_arch_def] @@ -247,7 +261,7 @@ lemma pspace_relation_cte_wp_at: lemma pspace_relation_ctes_ofI: "\ pspace_relation (kheap s) (ksPSpace s'); - cte_wp_at ((=) c) slot s; pspace_aligned' s'; + cte_wp_at ((=) c) slot s; pspace_aligned' s'; pspace_distinct' s' \ \ \cte. ctes_of s' (cte_map slot) = Some cte \ cap_relation c (cteCap cte)" apply (cases slot, clarsimp) @@ -255,6 +269,22 @@ lemma pspace_relation_ctes_ofI: apply (simp add: cte_wp_at_ctes_of) done +lemma pspace_relation_caps_of_state_cross: + "\ pspace_relation (kheap s) (ksPSpace s'); + caps_of_state s slot = Some c; pspace_aligned s; pspace_distinct s \ + \ \cte. ctes_of s' (cte_map slot) = Some cte \ cap_relation c (cteCap cte)" + for s' :: kernel_state + by (auto simp: cte_wp_at_caps_of_state + intro!: pspace_relation_ctes_ofI pspace_aligned_cross pspace_distinct_cross) + +lemma caps_of_state_cross: + "\ caps_of_state s slot = Some cap; pspace_aligned s; pspace_distinct s; (s,s') \ state_relation \ + \ \cap'. cteCaps_of s' (cte_map slot) = Some cap' \ cap_relation cap cap'" + apply (erule state_relationE) + apply (drule (3) pspace_relation_caps_of_state_cross) + apply (fastforce simp: cteCaps_of_def) + done + lemma get_cap_corres_P: "corres (\x y. cap_relation x (cteCap y) \ P x) (cte_wp_at P cslot_ptr) @@ -911,21 +941,13 @@ lemma ctes_of_valid_cap'': done lemma cap_insert_objs' [wp]: - "\valid_objs' - and valid_cap' cap\ - cteInsert cap src dest \\rv. valid_objs'\" - including no_pre - apply (simp add: cteInsert_def updateCap_def setUntypedCapAsFull_def bind_assoc split del: if_split) - apply (wp setCTE_valid_objs) - apply simp - apply wp+ - apply (clarsimp simp: updateCap_def) - apply (wp|simp)+ - apply (rule hoare_drop_imp)+ - apply wp+ - apply (rule hoare_strengthen_post[OF getCTE_sp]) + "\valid_objs' and valid_cap' cap\ + cteInsert cap src dest + \\_. valid_objs'\" + apply (simp add: cteInsert_def updateCap_def setUntypedCapAsFull_def) + apply (wpsimp wp: setCTE_valid_objs | wp getCTE_wp')+ apply (clarsimp simp: cte_wp_at_ctes_of isCap_simps - dest!: ctes_of_valid_cap'') + dest!: ctes_of_valid_cap'') done lemma cteInsert_weak_cte_wp_at: @@ -1963,6 +1985,14 @@ lemma pspace_relation_cte_wp_atI: apply assumption done +lemma caps_of_state_rev_cross: + "\ ctes_of s' p = Some cte; valid_objs s; (s,s') \ state_relation \ + \ \cap slot. caps_of_state s slot = Some cap \ p = cte_map slot \ cap_relation cap (cteCap cte)" + apply (erule state_relationE) + apply (drule (2) pspace_relation_cte_wp_atI) + apply (fastforce simp: cte_wp_at_caps_of_state) + done + lemma sameRegion_corres: "\ sameRegionAs c' d'; cap_relation c c'; cap_relation d d' \ \ same_region_as c d" @@ -5194,6 +5224,15 @@ lemma cte_map_inj_eq': done context begin interpretation Arch . (*FIXME: arch-split*) + +(* interface lemma: generic statement, arch-specific proof *) +lemma archMDBAssertions_cross: + "\ valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_arch_state s; valid_objs s; + (s, s') \ state_relation \ + \ archMDBAssertions s'" + unfolding archMDBAssertions_def + by (simp add: arch_mdb_assert_def) + lemma cteInsert_corres: notes split_paired_All[simp del] split_paired_Ex[simp del] trans_state_update'[symmetric,simp] @@ -5202,30 +5241,33 @@ lemma cteInsert_corres: (valid_objs and pspace_distinct and pspace_aligned and valid_mdb and valid_list and K (src\dest) and cte_wp_at (\c. c=Structures_A.NullCap) dest and - (\s. cte_wp_at (is_derived (cdt s) src c) src s)) + (\s. cte_wp_at (is_derived (cdt s) src c) src s) and valid_arch_state) (pspace_distinct' and pspace_aligned' and valid_mdb' and valid_cap' c' and cte_wp_at' (\c. cteCap c=NullCap) dest') (cap_insert c src dest) (cteInsert c' src' dest')" - (is "corres _ (?P and (\s. cte_wp_at _ _ s)) (?P' and cte_wp_at' _ _) _ _") + (is "corres _ (?P and (\s. cte_wp_at _ _ s) and valid_arch_state) (?P' and cte_wp_at' _ _) _ _") using assms unfolding cap_insert_def cteInsert_def apply simp + (* this lemma doesn't use the assertion, but does need to establish it *) + apply (rule corres_stateAssert_add_assertion[rotated]) + apply (rule archMDBAssertions_cross; simp add: valid_mdb_def) apply (rule corres_guard_imp) apply (rule corres_split[OF get_cap_corres]) apply (rule corres_split[OF get_cap_corres]) - apply (rule_tac F="cteCap rv' = NullCap" in corres_gen_asm2) + apply (rule_tac F="cteCap oldCTE = NullCap" in corres_gen_asm2) apply simp apply (rule_tac P="?P and cte_at dest and (\s. cte_wp_at (is_derived (cdt s) src c) src s) and cte_wp_at ((=) src_cap) src" and Q="?P' and - cte_wp_at' ((=) rv') (cte_map dest) and + cte_wp_at' ((=) oldCTE) (cte_map dest) and cte_wp_at' ((=) srcCTE) (cte_map src)" in corres_assert_assume) prefer 2 apply (clarsimp simp: cte_wp_at_ctes_of valid_mdb'_def valid_mdb_ctes_def valid_nullcaps_def) - apply (case_tac rv') + apply (case_tac oldCTE) apply (simp add: initMDBNode_def) apply (erule allE)+ apply (erule (1) impE) @@ -5234,7 +5276,7 @@ lemma cteInsert_corres: apply (rule_tac R="\r. ?P and cte_at dest and (\s. (is_derived (cdt s) src c) src_cap) and cte_wp_at ((=) (masked_as_full src_cap c)) src" and - R'="\r. ?P' and cte_wp_at' ((=) rv') (cte_map dest) and + R'="\r. ?P' and cte_wp_at' ((=) oldCTE) (cte_map dest) and cte_wp_at' ((=) (CTE (maskedAsFull (cteCap srcCTE) c') (cteMDBNode srcCTE))) (cte_map src)" in corres_split[where r'=dc]) @@ -5298,7 +5340,7 @@ lemma cteInsert_corres: apply (thin_tac "machine_state t = s" for s t)+ apply (case_tac "srcCTE") apply (rename_tac src_cap' src_node) - apply (case_tac "rv'") + apply (case_tac "oldCTE") apply (rename_tac dest_node) apply (clarsimp simp: in_set_cap_cte_at_swp) apply (subgoal_tac "cte_at src a \ is_derived (cdt a) src c src_cap") @@ -5586,7 +5628,7 @@ lemma cteInsert_corres: apply clarsimp apply (subgoal_tac "mdbRevocable node = isCapRevocable c' (cteCap srcCTE)") prefer 2 - apply (case_tac rv') + apply (case_tac oldCTE) subgoal by (clarsimp simp add: const_def modify_map_def split: if_split_asm) apply simp apply (rule is_cap_revocable_eq, assumption, assumption) @@ -5599,7 +5641,7 @@ lemma cteInsert_corres: split:if_splits dest!:cap_master_cap_eqDs) apply clarsimp apply (case_tac srcCTE) - apply (case_tac rv') + apply (case_tac oldCTE) apply clarsimp apply (subgoal_tac "\cap' node'. ctes_of b (cte_map (aa,bb)) = Some (CTE cap' node')") prefer 2 @@ -5627,7 +5669,7 @@ lemma cteInsert_corres: apply (wp set_untyped_cap_full_valid_objs set_untyped_cap_as_full_valid_mdb set_untyped_cap_as_full_cte_wp_at setUntypedCapAsFull_valid_cap setUntypedCapAsFull_cte_wp_at | clarsimp simp: cte_wp_at_caps_of_state| wps)+ - apply (case_tac rv',clarsimp simp:cte_wp_at_ctes_of maskedAsFull_def) + apply (case_tac oldCTE,clarsimp simp:cte_wp_at_ctes_of maskedAsFull_def) apply (wp getCTE_wp' get_cap_wp)+ apply clarsimp subgoal by (fastforce elim: cte_wp_at_weakenE) @@ -5637,7 +5679,7 @@ lemma cteInsert_corres: apply (thin_tac "machine_state t = s" for s t)+ apply (case_tac "srcCTE") apply (rename_tac src_cap' src_node) - apply (case_tac "rv'") + apply (case_tac "oldCTE") apply (rename_tac dest_node) apply (clarsimp simp: in_set_cap_cte_at_swp) apply (subgoal_tac "cte_at src a \ is_derived (cdt a) src c src_cap") diff --git a/proof/refine/RISCV64/CSpace_R.thy b/proof/refine/RISCV64/CSpace_R.thy index 98e56c3cfc..f4b248a4be 100644 --- a/proof/refine/RISCV64/CSpace_R.thy +++ b/proof/refine/RISCV64/CSpace_R.thy @@ -4519,6 +4519,7 @@ end locale mdb_insert_simple = mdb_insert + assumes safe_parent: "safe_parent_for' m src c'" assumes simple: "is_simple_cap' c'" + assumes arch_mdb_assert: "arch_mdb_assert m" begin interpretation Arch . (*FIXME: arch-split*) @@ -4717,6 +4718,12 @@ lemma maskedAsFull_revokable_safe_parent: context begin interpretation Arch . (*FIXME: arch-split*) +(* FIXME arch-split: generic statement, arch specific proof *) +lemma setUntypedCapAsFull_archMDBAssertions[wp]: + "setUntypedCapAsFull src_cap cap p \archMDBAssertions\" + unfolding archMDBAssertions_def arch_mdb_assert_def + by wp + lemma cteInsert_simple_corres: assumes "cap_relation c c'" "src' = cte_map src" "dest' = cte_map dest" notes trans_state_update'[symmetric,simp] @@ -4725,34 +4732,36 @@ lemma cteInsert_simple_corres: valid_mdb and valid_list and K (src\dest) and cte_wp_at (\c. c=cap.NullCap) dest and K (is_simple_cap c) and - (\s. cte_wp_at (safe_parent_for (cdt s) src c) src s)) + (\s. cte_wp_at (safe_parent_for (cdt s) src c) src s) and valid_arch_state) (pspace_distinct' and pspace_aligned' and valid_mdb' and valid_cap' c' and K (is_simple_cap' c') and cte_wp_at' (\c. cteCap c=NullCap) dest' and (\s. safe_parent_for' (ctes_of s) src' c')) (cap_insert c src dest) (cteInsert c' src' dest')" - (is "corres _ (?P and (\s. cte_wp_at _ _ s)) (?P' and cte_wp_at' _ _ and _) _ _") + (is "corres _ (?P and (\s. cte_wp_at _ _ s) and valid_arch_state) (?P' and cte_wp_at' _ _ and _) _ _") using assms unfolding cap_insert_def cteInsert_def supply subst_all [simp del] apply simp + apply (rule corres_stateAssert_add_assertion[rotated]) + apply (rule archMDBAssertions_cross; simp add: valid_mdb_def) apply (rule corres_guard_imp) apply (rule corres_split[OF get_cap_corres]) apply (rule corres_split[OF get_cap_corres]) - apply (rule_tac F="cteCap rv' = NullCap" in corres_gen_asm2) + apply (rule_tac F="cteCap oldCTE = NullCap" in corres_gen_asm2) apply simp apply (rule_tac P="?P and cte_at dest and (\s. cte_wp_at (safe_parent_for (cdt s) src c) src s) and cte_wp_at ((=) src_cap) src" and - Q="?P' and - cte_wp_at' ((=) rv') (cte_map dest) and + Q="?P' and archMDBAssertions and + cte_wp_at' ((=) oldCTE) (cte_map dest) and cte_wp_at' ((=) srcCTE) (cte_map src) and (\s. safe_parent_for' (ctes_of s) src' c')" in corres_assert_assume) prefer 2 apply (clarsimp simp: cte_wp_at_ctes_of valid_mdb'_def valid_mdb_ctes_def valid_nullcaps_def) - apply (case_tac rv') + apply (case_tac oldCTE) apply (simp add: initMDBNode_def) apply (erule allE)+ apply (erule (1) impE) @@ -4761,7 +4770,7 @@ lemma cteInsert_simple_corres: apply (rule_tac R="\r. ?P and cte_at dest and (\s. cte_wp_at (safe_parent_for (cdt s) src c) src s) and cte_wp_at ((=) (masked_as_full src_cap c)) src" and - R'="\r. ?P' and cte_wp_at' ((=) rv') (cte_map dest) + R'="\r. ?P' and archMDBAssertions and cte_wp_at' ((=) oldCTE) (cte_map dest) and cte_wp_at' ((=) (CTE (maskedAsFull (cteCap srcCTE) c') (cteMDBNode srcCTE))) (cte_map src) and (\s. safe_parent_for' (ctes_of s) src' c')" in corres_split[where r'=dc]) @@ -4856,7 +4865,7 @@ lemma cteInsert_simple_corres: apply clarsimp apply (subgoal_tac "mdbRevocable node = isCapRevocable c' (cteCap srcCTE)") prefer 2 - apply (case_tac rv') + apply (case_tac oldCTE) apply (clarsimp simp add: const_def modify_map_def split: if_split_asm) apply clarsimp apply (rule is_cap_revocable_eq, assumption, assumption) @@ -4869,7 +4878,7 @@ lemma cteInsert_simple_corres: apply (clarsimp simp: cte_wp_at_def is_simple_cap_def) apply clarsimp apply (case_tac srcCTE) - apply (case_tac rv') + apply (case_tac oldCTE) apply clarsimp apply (subgoal_tac "\cap' node'. ctes_of b (cte_map (aa,bb)) = Some (CTE cap' node')") prefer 2 @@ -4893,14 +4902,14 @@ lemma cteInsert_simple_corres: set_untyped_cap_as_full_cte_wp_at setUntypedCapAsFull_valid_cap setUntypedCapAsFull_cte_wp_at setUntypedCapAsFull_safe_parent_for' | clarsimp | wps)+ apply (clarsimp simp:cte_wp_at_caps_of_state ) - apply (case_tac rv',clarsimp simp:cte_wp_at_ctes_of maskedAsFull_def) + apply (case_tac oldCTE,clarsimp simp:cte_wp_at_ctes_of maskedAsFull_def) apply (wp getCTE_wp' get_cap_wp)+ apply clarsimp subgoal by (fastforce elim: cte_wp_at_weakenE) subgoal by (clarsimp simp: cte_wp_at'_def) apply (case_tac "srcCTE") apply (rename_tac src_cap' src_node) - apply (case_tac "rv'") + apply (case_tac "oldCTE") apply (rename_tac dest_node) apply (clarsimp simp: in_set_cap_cte_at_swp) apply (subgoal_tac "cte_at src a \ safe_parent_for (cdt a) src c src_cap") @@ -4924,7 +4933,8 @@ lemma cteInsert_simple_corres: apply (simp (no_asm_simp) add: cdt_relation_def split: if_split) apply (intro impI allI) apply (frule mdb_insert_simple_axioms.intro) - apply(clarsimp simp:cte_wp_at_ctes_of) + apply(clarsimp simp:cte_wp_at_ctes_of) + apply (simp add: archMDBAssertions_def) apply (drule (1) mdb_insert_simple.intro) apply (drule_tac src_cap' = src_cap' in maskedAsFull_revokable_safe_parent[symmetric]) apply simp+ @@ -5820,7 +5830,7 @@ lemma cteInsert_simple_mdb': mdb_ptr_axioms.intro mdb_insert_axioms.intro) apply (simp add:modify_map_def valid_mdb_ctes_maskedAsFull)+ apply (clarsimp simp:nullPointer_def)+ - apply ((clarsimp simp:valid_mdb_ctes_def)+) + apply (clarsimp simp:valid_mdb_ctes_def archMDBAssertions_def)+ apply (drule mdb_insert_simple'.mdb) apply (clarsimp simp:valid_mdb_ctes_def) done diff --git a/proof/refine/RISCV64/Interrupt_R.thy b/proof/refine/RISCV64/Interrupt_R.thy index 9a562e17d1..d4196d88eb 100644 --- a/proof/refine/RISCV64/Interrupt_R.thy +++ b/proof/refine/RISCV64/Interrupt_R.thy @@ -488,6 +488,9 @@ lemma setIRQTrigger_corres: | simp add: dc_def)+ done +crunch set_irq_state + for valid_arch_state[wp]: valid_arch_state + lemma arch_performIRQControl_corres: "arch_irq_control_inv_relation x2 ivk' \ corres (dc \ dc) (einvs and arch_irq_control_inv_valid x2) diff --git a/proof/refine/RISCV64/InvariantUpdates_H.thy b/proof/refine/RISCV64/InvariantUpdates_H.thy index a094f36565..4df6c8b8c9 100644 --- a/proof/refine/RISCV64/InvariantUpdates_H.thy +++ b/proof/refine/RISCV64/InvariantUpdates_H.thy @@ -483,10 +483,4 @@ lemma invs'_update_cnt[elim!]: by (clarsimp simp: invs'_def valid_state'_def valid_queues_def valid_irq_node'_def cur_tcb'_def ct_idle_or_in_cur_domain'_def tcb_in_cur_domain'_def bitmapQ_defs) -(* FIXME arch-split: valid_arch_mdb_ctes only exists to contain ioport_control on x64, and it is not - yet clear what the best way to arch-split it is, or whether it can be crossed from AInvs. - Therefore, for now, export the truth that it doesn't do anything on this arch beyond this point *) -arch_requalify_facts valid_arch_mdb_ctes_def -lemmas [simp] = valid_arch_mdb_ctes_def - end diff --git a/proof/refine/RISCV64/Ipc_R.thy b/proof/refine/RISCV64/Ipc_R.thy index 346bf01bdf..e44097df93 100644 --- a/proof/refine/RISCV64/Ipc_R.thy +++ b/proof/refine/RISCV64/Ipc_R.thy @@ -391,6 +391,10 @@ lemma cte_refs'_maskedAsFull[simp]: apply (clarsimp simp:maskedAsFull_def isCap_simps)+ done +lemma set_extra_badge_valid_arch_state[wp]: + "set_extra_badge buffer badge n \ valid_arch_state \" + unfolding set_extra_badge_def + by wp lemma transferCapsToSlots_corres: "\ list_all2 (\(cap, slot) (cap', slot'). cap_relation cap cap' @@ -398,7 +402,7 @@ lemma transferCapsToSlots_corres: mi' = message_info_map mi \ \ corres ((=) \ message_info_map) (\s. valid_objs s \ pspace_aligned s \ pspace_distinct s \ valid_mdb s - \ valid_list s + \ valid_list s \ valid_arch_state s \ (case ep of Some x \ ep_at x s | _ \ True) \ (\x \ set slots. cte_wp_at (\cap. cap = cap.NullCap) x s \ real_cte_at x s) @@ -472,7 +476,8 @@ next apply (simp add: tl_map) apply (rule corres_rel_imp, rule Cons.hyps, simp_all)[1] apply (wp valid_case_option_post_wp hoare_vcg_const_Ball_lift - hoare_vcg_const_Ball_lift cap_insert_weak_cte_wp_at) + hoare_vcg_const_Ball_lift cap_insert_derived_valid_arch_state + cap_insert_weak_cte_wp_at) apply (wp hoare_vcg_const_Ball_lift | simp add:split_def del: imp_disj1)+ apply (wp cap_insert_cte_wp_at) apply (wp valid_case_option_post_wp hoare_vcg_const_Ball_lift @@ -613,6 +618,7 @@ lemma cteInsert_assume_Null: apply (rule hoare_name_pre_state) apply (erule impCE) apply (simp add: cteInsert_def) + apply (rule bind_wp[OF _ stateAssert_sp]) apply (rule bind_wp[OF _ getCTE_sp])+ apply (rule hoare_name_pre_state) apply (clarsimp simp: cte_wp_at_ctes_of) @@ -1040,7 +1046,7 @@ lemma transferCaps_corres: corres ((=) \ message_info_map) (tcb_at receiver and valid_objs and pspace_aligned and pspace_distinct and valid_mdb - and valid_list + and valid_list and valid_arch_state and (\s. case ep of Some x \ ep_at x s | _ \ True) and case_option \ in_user_frame recv_buf and (\s. valid_message_info info) @@ -1446,10 +1452,14 @@ lemma copyMRs_valid_mdb[wp]: "\valid_mdb'\ copyMRs t buf t' buf' n \\rv. valid_mdb'\" by (simp add: valid_mdb'_def copyMRs_ctes_of) +crunch copy_mrs + for valid_arch_state[wp]: valid_arch_state + (wp: crunch_wps) + lemma doNormalTransfer_corres: "corres dc (tcb_at sender and tcb_at receiver and (pspace_aligned:: det_state \ bool) - and valid_objs and cur_tcb and valid_mdb and valid_list and pspace_distinct + and valid_objs and cur_tcb and valid_mdb and valid_list and valid_arch_state and pspace_distinct and (\s. case ep of Some x \ ep_at x s | _ \ True) and case_option \ in_user_frame send_buf and case_option \ in_user_frame recv_buf) @@ -1728,7 +1738,7 @@ lemma lookupIPCBuffer_valid_ipc_buffer [wp]: lemma doIPCTransfer_corres: "corres dc (tcb_at s and tcb_at r and valid_objs and pspace_aligned - and valid_list + and valid_list and valid_arch_state and pspace_distinct and valid_mdb and cur_tcb and (\s. case ep of Some x \ ep_at x s | _ \ True)) (tcb_at' s and tcb_at' r and valid_pspace' and cur_tcb' @@ -1736,9 +1746,9 @@ lemma doIPCTransfer_corres: (do_ipc_transfer s ep bg grt r) (doIPCTransfer s ep bg grt r)" apply (simp add: do_ipc_transfer_def doIPCTransfer_def) - apply (rule_tac Q="%receiveBuffer sa. tcb_at s sa \ valid_objs sa \ - pspace_aligned sa \ tcb_at r sa \ - cur_tcb sa \ valid_mdb sa \ valid_list sa \ pspace_distinct sa \ + apply (rule_tac Q="\receiveBuffer sa. tcb_at s sa \ valid_objs sa \ + pspace_aligned sa \ pspace_distinct sa \ tcb_at r sa \ + cur_tcb sa \ valid_mdb sa \ valid_list sa \ valid_arch_state sa \ (case ep of None \ True | Some x \ ep_at x sa) \ case_option (\_. True) in_user_frame receiveBuffer sa \ obj_at (\ko. \tcb. ko = TCB tcb @@ -2315,7 +2325,7 @@ lemma setupCallerCap_corres: (st_tcb_at (Not \ halted) sender and tcb_at receiver and st_tcb_at (Not \ awaiting_reply) sender and valid_reply_caps and valid_objs and pspace_distinct and pspace_aligned and valid_mdb - and valid_list and + and valid_list and valid_arch_state and valid_reply_masters and cte_wp_at (\c. c = cap.NullCap) (receiver, tcb_cnode_index 3)) (tcb_at' sender and tcb_at' receiver and valid_pspace' and (\s. weak_sch_act_wf (ksSchedulerAction s) s)) @@ -2534,6 +2544,7 @@ proof - valid_queues_in_correct_ready_q valid_queues_ready_qs_distinct valid_sched_valid_queues)+ apply ((wp hoare_drop_imps do_ipc_transfer_tcb_caps weak_valid_sched_action_lift + do_ipc_transfer_valid_arch | clarsimp simp: is_cap_simps)+)[1] apply (simp add: pred_conj_def) apply (strengthen sch_act_wf_weak) @@ -3254,7 +3265,7 @@ lemma receiveIPC_corres: apply (rule corres_split[OF doIPCTransfer_corres]) apply (simp split del: if_split cong: if_cong) apply (fold dc_def)[1] - apply (rule_tac P="valid_objs and valid_mdb and valid_list + apply (rule_tac P="valid_objs and valid_mdb and valid_list and valid_arch_state and valid_sched and cur_tcb and valid_reply_caps @@ -3284,7 +3295,7 @@ lemma receiveIPC_corres: apply (fastforce simp: st_tcb_at_tcb_at st_tcb_def2 valid_sched_def valid_sched_action_def) apply (clarsimp split: if_split_asm) - apply (clarsimp | wp do_ipc_transfer_tcb_caps)+ + apply (clarsimp | wp do_ipc_transfer_tcb_caps do_ipc_transfer_valid_arch)+ apply (rule_tac Q'="\_ s. sch_act_wf (ksSchedulerAction s) s \ sym_heap_sched_pointers s \ valid_sched_pointers s \ pspace_aligned' s \ pspace_distinct' s" @@ -3617,19 +3628,12 @@ lemma cteInsert_cap_to': "\ex_nonz_cap_to' p and cte_wp_at' (\c. cteCap c = NullCap) dest\ cteInsert cap src dest \\rv. ex_nonz_cap_to' p\" - apply (simp add: cteInsert_def ex_nonz_cap_to'_def - updateCap_def setUntypedCapAsFull_def - split del: if_split) - apply (rule hoare_pre, rule hoare_vcg_ex_lift) - apply (wp updateMDB_weak_cte_wp_at - setCTE_weak_cte_wp_at - | simp - | rule hoare_drop_imps)+ - apply (wp getCTE_wp) - apply clarsimp + apply (simp add: cteInsert_def ex_nonz_cap_to'_def updateCap_def setUntypedCapAsFull_def) + apply (wpsimp wp: updateMDB_weak_cte_wp_at setCTE_weak_cte_wp_at hoare_vcg_ex_lift + | rule hoare_drop_imps + | wp getCTE_wp)+ (* getCTE_wp is separate to apply it only to the last one *) apply (rule_tac x=cref in exI) - apply (rule conjI) - apply (clarsimp simp: cte_wp_at_ctes_of)+ + apply (fastforce simp: cte_wp_at_ctes_of) done crunch setExtraBadge diff --git a/proof/refine/RISCV64/Tcb_R.thy b/proof/refine/RISCV64/Tcb_R.thy index 6a8265c608..2f852ebbfb 100644 --- a/proof/refine/RISCV64/Tcb_R.thy +++ b/proof/refine/RISCV64/Tcb_R.thy @@ -845,7 +845,7 @@ lemma checkCapAt_cteInsert_corres: apply clarsimp apply (rule conjI, fastforce)+ apply (cases src_slot) - apply (clarsimp simp: cte_wp_at_caps_of_state) + apply (clarsimp simp: cte_wp_at_caps_of_state invs_arch_state) apply (rule conjI) apply (frule same_object_as_cap_master) apply (clarsimp simp: cap_master_cap_simps is_cnode_or_valid_arch_def diff --git a/proof/refine/X64/ArchInvsDefs_H.thy b/proof/refine/X64/ArchInvsDefs_H.thy index 454f8953db..010c2f2b2a 100644 --- a/proof/refine/X64/ArchInvsDefs_H.thy +++ b/proof/refine/X64/ArchInvsDefs_H.thy @@ -198,13 +198,6 @@ primrec acapClass :: "arch_capability \ capclass" where | "acapClass (IOPortCap x y) = IOPortClass" | "acapClass IOPortControlCap = IOPortClass" -(* IOPortControl caps are unique and always revocable *) -definition - "ioport_control m \ - \p n. m p = Some (CTE (ArchObjectCap IOPortControlCap) n) \ - mdbRevocable n \ - (\p' n'. m p' = Some (CTE (ArchObjectCap IOPortControlCap) n') \ p' = p)" - definition isArchFrameCap :: "capability \ bool" where @@ -221,11 +214,6 @@ definition where "isArchIOPortCap cap \ case cap of ArchObjectCap (IOPortCap f l) \ True | _ \ False" -definition valid_arch_mdb_ctes :: "cte_heap \ bool" where - "valid_arch_mdb_ctes \ ioport_control" - -lemmas [simp] = valid_arch_mdb_ctes_def - definition table_refs' :: "machine_word \ machine_word set" where "table_refs' x \ (\y. x + (y << word_size_bits)) ` {y. y < 2^ptTranslationBits}" diff --git a/proof/refine/X64/ArchInvsLemmas_H.thy b/proof/refine/X64/ArchInvsLemmas_H.thy index 11a32aab90..38ead17306 100644 --- a/proof/refine/X64/ArchInvsLemmas_H.thy +++ b/proof/refine/X64/ArchInvsLemmas_H.thy @@ -373,15 +373,6 @@ lemma page_map_l4_pml4e_atI': "\ page_map_l4_at' p s; x < 2^ptTranslationBits \ \ pml4e_at' (p + (x << word_size_bits)) s" by (simp add: page_map_l4_at'_def pageBits_def) -lemma ioport_controlD: - "\ m p = Some (CTE (ArchObjectCap IOPortControlCap) n); m p' = Some (CTE (ArchObjectCap IOPortControlCap) n'); - ioport_control m \ \ p' = p" - unfolding ioport_control_def by blast - -lemma ioport_revocable: - "\ m p = Some (CTE (ArchObjectCap IOPortControlCap) n); ioport_control m \ \ mdbRevocable n" - unfolding ioport_control_def by blast - lemma tcb_hyp_refs_of'_simps[simp]: "tcb_hyp_refs' atcb = {}" by (auto simp: tcb_hyp_refs'_def) diff --git a/proof/refine/X64/Arch_R.thy b/proof/refine/X64/Arch_R.thy index 7531980d00..a376268451 100644 --- a/proof/refine/X64/Arch_R.thy +++ b/proof/refine/X64/Arch_R.thy @@ -139,6 +139,7 @@ lemma performASIDControlInvocation_corres: apply (cases i) apply (rename_tac word1 prod1 prod2 word2) apply (clarsimp simp: asid_ci_map_def) + apply (rename_tac p slot p' slot' word2) apply (simp add: perform_asid_control_invocation_def placeNewObject_def2 performASIDControlInvocation_def) apply (rule corres_name_pre) @@ -197,7 +198,7 @@ lemma performASIDControlInvocation_corres: apply wp+ apply (strengthen safe_parent_strg[where idx = "2^pageBits"]) apply (strengthen invs_valid_objs invs_distinct - invs_psp_aligned invs_mdb + invs_psp_aligned invs_mdb invs_arch_state | simp cong:conj_cong)+ apply (wp retype_region_plain_invs[where sz = pageBits] retype_cte_wp_at[where sz = pageBits])+ @@ -269,9 +270,9 @@ lemma performASIDControlInvocation_corres: deleteObjects_null_filter[where p="makePoolParent i'"]) apply (clarsimp simp:invs_mdb max_free_index_def invs_untyped_children) apply (prop_tac "detype_locale x y sa" for x y) - apply (simp add: detype_locale_def) - apply (fastforce simp: cte_wp_at_caps_of_state descendants_range_def2 - empty_descendants_range_in invs_untyped_children) + apply (clarsimp simp: detype_locale_def cte_wp_at_caps_of_state) + apply (rule conjI, assumption, rule conjI, solves simp) (* force instantiation to Untyped cap *) + apply (fastforce simp: descendants_range_def2 empty_descendants_range_in invs_untyped_children) apply (intro conjI) apply (clarsimp) apply (erule(1) caps_of_state_valid) @@ -283,7 +284,7 @@ lemma performASIDControlInvocation_corres: apply (drule detype_locale.non_null_present) apply (fastforce simp:cte_wp_at_caps_of_state) apply simp - apply (frule_tac ptr = "(aa,ba)" in detype_invariants [rotated 3]) + apply (frule_tac ptr = "(p', slot')" in detype_invariants [rotated 3]) apply fastforce apply simp apply (simp add: cte_wp_at_caps_of_state) @@ -311,7 +312,7 @@ lemma performASIDControlInvocation_corres: apply (simp add:empty_descendants_range_in)+ apply (rule conjI) apply clarsimp - apply (drule_tac p = "(aa,ba)" in cap_refs_in_kernel_windowD2[OF caps_of_state_cteD]) + apply (drule_tac p = "(p', slot')" in cap_refs_in_kernel_windowD2[OF caps_of_state_cteD]) apply fastforce apply (clarsimp simp: region_in_kernel_window_def valid_cap_def cap_aligned_def is_aligned_neg_mask_eq detype_def clear_um_def) @@ -321,7 +322,7 @@ lemma performASIDControlInvocation_corres: apply (clarsimp simp: detype_def clear_um_def detype_ext_def valid_sched_def valid_etcbs_def st_tcb_at_kh_def obj_at_kh_def st_tcb_at_def obj_at_def is_etcb_at_def) apply (simp add: detype_def clear_um_def) - apply (drule_tac x = "cte_map (aa,ba)" in pspace_relation_cte_wp_atI[OF state_relation_pspace_relation]) + apply (drule_tac x = "cte_map (p', slot')" in pspace_relation_cte_wp_atI[OF state_relation_pspace_relation]) apply (simp add:invs_valid_objs)+ apply clarsimp apply (drule cte_map_inj_eq) @@ -1392,7 +1393,7 @@ lemma performX64PortInvocation_corres: apply wpsimp apply (clarsimp simp: is_simple_cap_def is_cap_simps) apply wpsimp - apply (strengthen invs_distinct[mk_strg] invs_psp_aligned_strg invs_strgs) + apply (strengthen invs_distinct[mk_strg] invs_psp_aligned_strg invs_strgs invs_arch_state) apply (wpsimp wp: set_ioport_mask_invs set_ioport_mask_safe_parent_for) apply (clarsimp simp: is_simple_cap'_def isCap_simps) apply wpsimp diff --git a/proof/refine/X64/CNodeInv_R.thy b/proof/refine/X64/CNodeInv_R.thy index 9a886cd6d9..4b8074e011 100644 --- a/proof/refine/X64/CNodeInv_R.thy +++ b/proof/refine/X64/CNodeInv_R.thy @@ -4781,55 +4781,6 @@ lemma irq_control_n: "irq_control n" apply clarsimp done -context begin interpretation Arch . (* FIXME arch-split *) - -lemma ioport_control_n: "ioport_control n" - using src dest dest_derived src_derived - apply (clarsimp simp: ioport_control_def) - apply (frule revokable) - apply (drule n_cap) - apply (clarsimp split: if_split_asm) - apply (clarsimp simp: weak_derived'_def) - apply (frule ioport_revocable, rule arch_mdb_ctes[simplified]) - apply clarsimp - apply (drule n_cap) - apply (split if_split_asm) - apply (thin_tac "capability.ArchObjectCap X64_H.IOPortControlCap = dcap") - apply clarsimp - apply (clarsimp split: if_split_asm) - apply (drule (1) ioport_controlD, rule arch_mdb_ctes[simplified]) - apply simp - apply (drule (1) ioport_controlD, rule arch_mdb_ctes[simplified]) - apply simp - apply (clarsimp simp: weak_derived'_def) - apply (frule ioport_revocable, rule arch_mdb_ctes[simplified]) - apply clarsimp - apply (drule n_cap) - apply (split if_split_asm) - apply clarsimp - apply (drule (1) ioport_controlD, rule arch_mdb_ctes[simplified]) - apply simp - apply (split if_split_asm) - apply (thin_tac "capability.ArchObjectCap X64_H.IOPortControlCap = scap") - apply clarsimp - apply (clarsimp split: if_split_asm) - apply (drule (1) ioport_controlD, rule arch_mdb_ctes[simplified]) - apply simp - apply (clarsimp simp: weak_derived'_def) - apply (frule ioport_revocable, rule arch_mdb_ctes[simplified]) - apply clarsimp - apply (drule n_cap) - apply (clarsimp split: if_split_asm) - apply (drule (1) ioport_controlD, rule arch_mdb_ctes[simplified]) - apply simp - apply (drule (1) ioport_controlD, rule arch_mdb_ctes[simplified]) - apply clarsimp - apply (drule (1) ioport_controlD, rule arch_mdb_ctes[simplified]) - apply clarsimp - done - -end - lemma distinct_zombies_m: "distinct_zombies m" using valid by auto @@ -4874,9 +4825,9 @@ lemma cteSwap_valid_mdb_helper: shows "valid_mdb_ctes n" using cteSwap_chain cteSwap_dlist_helper cteSwap_valid_badges cteSwap_chunked caps_contained untyped_mdb_n untyped_inc_n - nullcaps_n ut_rev_n class_links_n irq_control_n ioport_control_n + nullcaps_n ut_rev_n class_links_n irq_control_n distinct_zombies_n reply_masters_rvk_fb_n - by (auto simp: untyped_eq X64.valid_arch_mdb_ctes_def) + by (auto simp: untyped_eq) end @@ -5732,10 +5683,7 @@ lemma make_zombie_invs': apply (subgoal_tac "cap \ IRQControlCap") apply (clarsimp simp: irq_control_def) apply (clarsimp simp: isCap_simps) - apply (rule conjI[rotated]) - apply (subgoal_tac "cap \ ArchObjectCap IOPortControlCap") - apply (clarsimp simp: ioport_control_def) - apply (clarsimp simp: isCap_simps) + apply (clarsimp simp: isCap_simps) apply (simp add: reply_masters_rvk_fb_def, erule ball_ran_fun_updI) apply (clarsimp simp: isCap_simps) apply (clarsimp simp: modify_map_apply) @@ -8493,28 +8441,6 @@ proof apply (erule (1) irq_controlD, rule irq_control) done - show "valid_arch_mdb_ctes m'" using src dest parency - apply (clarsimp simp: ioport_control_def) - apply (frule m'_revocable) - apply (drule m'_cap) - apply (clarsimp split: if_split_asm) - apply (clarsimp simp add: weak_derived'_def) - apply (frule ioport_revocable, rule arch_mdb_ctes[simplified]) - apply clarsimp - apply (drule m'_cap) - apply (clarsimp split: if_split_asm) - apply (drule (1) ioport_controlD, rule arch_mdb_ctes[simplified]) - apply simp - apply (frule ioport_revocable, rule arch_mdb_ctes[simplified]) - apply clarsimp - apply (drule m'_cap) - apply (clarsimp split: if_split_asm) - apply (clarsimp simp: weak_derived'_def) - apply (drule (1) ioport_controlD, rule arch_mdb_ctes[simplified]) - apply simp - apply (erule (1) ioport_controlD, rule arch_mdb_ctes[simplified]) - done - have distz: "distinct_zombies m" using valid by (simp add: valid_mdb_ctes_def) diff --git a/proof/refine/X64/CSpace1_R.thy b/proof/refine/X64/CSpace1_R.thy index 116366ac8a..4151dd801d 100644 --- a/proof/refine/X64/CSpace1_R.thy +++ b/proof/refine/X64/CSpace1_R.thy @@ -14,6 +14,24 @@ imports "AInvs.ArchDetSchedSchedule_AI" begin +context Arch begin arch_global_naming + +(* IOPortControl caps are unique and always revocable. Defined separately from archMDBAssertions, + because locale mdb_insert_simple needs a form that only takes a cte_heap. *) +definition arch_mdb_assert :: "cte_heap \ bool" where + "arch_mdb_assert m \ + \p n. m p = Some (CTE (ArchObjectCap IOPortControlCap) n) \ + mdbRevocable n \ + (\p' n'. m p' = Some (CTE (ArchObjectCap IOPortControlCap) n') \ p' = p)" + +end + +arch_requalify_consts + arch_mdb_assert + +defs archMDBAssertions_def: + "archMDBAssertions s \ arch_mdb_assert (ctes_of s)" + context Arch begin global_naming X64_A (*FIXME: arch-split*) lemmas final_matters_def = final_matters_def[simplified final_matters_arch_def] @@ -248,7 +266,7 @@ lemma pspace_relation_cte_wp_at: lemma pspace_relation_ctes_ofI: "\ pspace_relation (kheap s) (ksPSpace s'); - cte_wp_at ((=) c) slot s; pspace_aligned' s'; + cte_wp_at ((=) c) slot s; pspace_aligned' s'; pspace_distinct' s' \ \ \cte. ctes_of s' (cte_map slot) = Some cte \ cap_relation c (cteCap cte)" apply (cases slot, clarsimp) @@ -256,6 +274,22 @@ lemma pspace_relation_ctes_ofI: apply (simp add: cte_wp_at_ctes_of) done +lemma pspace_relation_caps_of_state_cross: + "\ pspace_relation (kheap s) (ksPSpace s'); + caps_of_state s slot = Some c; pspace_aligned s; pspace_distinct s \ + \ \cte. ctes_of s' (cte_map slot) = Some cte \ cap_relation c (cteCap cte)" + for s' :: kernel_state + by (auto simp: cte_wp_at_caps_of_state + intro!: pspace_relation_ctes_ofI pspace_aligned_cross pspace_distinct_cross) + +lemma caps_of_state_cross: + "\ caps_of_state s slot = Some cap; pspace_aligned s; pspace_distinct s; (s,s') \ state_relation \ + \ \cap'. cteCaps_of s' (cte_map slot) = Some cap' \ cap_relation cap cap'" + apply (erule state_relationE) + apply (drule (3) pspace_relation_caps_of_state_cross) + apply (fastforce simp: cteCaps_of_def) + done + lemma get_cap_corres_P: "corres (\x y. cap_relation x (cteCap y) \ P x) (cte_wp_at P cslot_ptr) @@ -917,21 +951,13 @@ lemma ctes_of_valid_cap'': done lemma cap_insert_objs' [wp]: - "\valid_objs' - and valid_cap' cap\ - cteInsert cap src dest \\rv. valid_objs'\" - including no_pre - apply (simp add: cteInsert_def updateCap_def setUntypedCapAsFull_def bind_assoc split del: if_split) - apply (wp setCTE_valid_objs) - apply simp - apply wp+ - apply (clarsimp simp: updateCap_def) - apply (wp|simp)+ - apply (rule hoare_drop_imp)+ - apply wp+ - apply (rule hoare_strengthen_post[OF getCTE_sp]) + "\valid_objs' and valid_cap' cap\ + cteInsert cap src dest + \\_. valid_objs'\" + apply (simp add: cteInsert_def updateCap_def setUntypedCapAsFull_def) + apply (wpsimp wp: setCTE_valid_objs | wp getCTE_wp')+ apply (clarsimp simp: cte_wp_at_ctes_of isCap_simps - dest!: ctes_of_valid_cap'') + dest!: ctes_of_valid_cap'') done lemma cteInsert_weak_cte_wp_at: @@ -1972,6 +1998,21 @@ lemma pspace_relation_cte_wp_atI: apply assumption done +lemma caps_of_state_rev_cross: + "\ ctes_of s' p = Some cte; valid_objs s; (s,s') \ state_relation \ + \ \cap slot. caps_of_state s slot = Some cap \ p = cte_map slot \ cap_relation cap (cteCap cte)" + apply (erule state_relationE) + apply (drule (2) pspace_relation_cte_wp_atI) + apply (fastforce simp: cte_wp_at_caps_of_state) + done + +lemma cap_relation_IOPortControlCap[simp]: + "cap_relation cap (ArchObjectCap IOPortControlCap) = + (cap = Structures_A.ArchObjectCap X64_A.IOPortControlCap)" + apply (cases cap; simp) + apply (rename_tac acap, case_tac acap; simp) + done + lemma sameRegion_corres: "\ sameRegionAs c' d'; cap_relation c c'; cap_relation d d' \ \ same_region_as c d" @@ -4550,43 +4591,6 @@ lemma irq_control_preserve: apply (simp add:dom misc)+ done -lemma ioport_control_preserve_oneway: - assumes dom: "\x. (x \ dom m) = (x \ dom m')" - assumes misc: - "\x cte cte'. \m x =Some cte;m' x = Some cte'\ \ - isIOPortControlCap' (cteCap cte) = isIOPortControlCap' (cteCap cte') \ - cteMDBNode cte = cteMDBNode cte'" - shows "ioport_control m \ ioport_control m'" - apply (clarsimp simp:ioport_control_def) - apply (frule iffD2[OF dom,OF domI]) - apply clarsimp - apply (frule(1) misc) - apply (clarsimp simp:isCap_simps) - apply (case_tac y) - apply (elim allE impE) - apply fastforce - apply clarsimp - apply (drule_tac x = p' in spec) - apply (erule impE) - apply (frule_tac x1 = p' in iffD2[OF dom,OF domI]) - apply clarsimp - apply (drule(1) misc)+ - apply (case_tac y) - apply (simp add:isCap_simps)+ - done - -lemma ioport_control_preserve: - assumes dom: "\x. (x \ dom m) = (x \ dom m')" - assumes misc: - "\x cte cte'. \m x =Some cte;m' x = Some cte'\ \ - isIOPortControlCap' (cteCap cte) = isIOPortControlCap' (cteCap cte') \ - cteMDBNode cte = cteMDBNode cte'" - shows "ioport_control m = ioport_control m'" - apply (rule iffI[OF ioport_control_preserve_oneway[OF dom misc]]) - apply (assumption)+ - apply (rule ioport_control_preserve_oneway) - apply (simp add:dom misc)+ - done end locale mdb_inv_preserve = fixes m m' @@ -4625,8 +4629,7 @@ lemma preserve_stuff: \ mdb_chunked m = mdb_chunked m' \ valid_badges m = valid_badges m' \ untyped_mdb' m = untyped_mdb' m' - \ irq_control m = irq_control m' - \ ioport_control m = ioport_control m'" + \ irq_control m = irq_control m'" apply (intro conjI) apply (rule valid_dlist_preserve) apply (simp add:mdb_inv_preserve_def dom misc sameRegion mdb_next)+ @@ -4646,8 +4649,6 @@ lemma preserve_stuff: apply (simp add:mdb_inv_preserve_def dom misc sameRegion mdb_next)+ apply (rule irq_control_preserve) apply (simp add:mdb_inv_preserve_def dom misc sameRegion mdb_next)+ - apply (rule ioport_control_preserve) - apply (simp add:mdb_inv_preserve_def dom misc sameRegion mdb_next)+ done lemma untyped_inc': @@ -4983,39 +4984,6 @@ lemma updateCapFreeIndex_irq_control: apply (clarsimp simp:cte_wp_at_ctes_of)+ done -context begin interpretation Arch . (* FIXME arch-split *) - -lemma updateCapFreeIndex_ioport_control: - assumes preserve:"\m m'. mdb_inv_preserve m m' \ mdb_inv_preserve (Q m) (Q m')" - shows - "\\s. P (ioport_control (Q (ctes_of s))) \ cte_wp_at' (\c. c = srcCTE \ isUntypedCap (cteCap c)) src s\ - updateCap src (capFreeIndex_update (\_. index) (cteCap srcCTE)) - \\r s. P (ioport_control (Q (ctes_of s)))\" - apply (wp updateCap_ctes_of_wp) - apply (subgoal_tac "mdb_inv_preserve (Q (ctes_of s)) (Q (modify_map (ctes_of s) src - (cteCap_update (\_. capFreeIndex_update (\_. index) (cteCap srcCTE)))))") - apply (drule mdb_inv_preserve.preserve_stuff) - apply simp - apply (rule preserve) - apply (rule mdb_inv_preserve_updateCap) - apply (clarsimp simp:cte_wp_at_ctes_of)+ - done - -lemma setUntypedCapAsFull_ioport_control: - assumes preserve:"\m m'. mdb_inv_preserve m m' \ mdb_inv_preserve (Q m) (Q m')" - shows - "\\s. P (ioport_control (Q (ctes_of s))) \ cte_wp_at' (\c. c = srcCTE) src s\ - setUntypedCapAsFull (cteCap srcCTE) cap src - \\r s. P (ioport_control (Q (ctes_of s)))\" - apply (clarsimp simp:setUntypedCapAsFull_def split:if_splits,intro conjI impI) - apply (wp updateCapFreeIndex_ioport_control) - apply (clarsimp simp:cte_wp_at_ctes_of preserve)+ - apply wp - apply clarsimp - done - -end - lemma setUntypedCapAsFull_mdb_chunked: assumes preserve:"\m m'. mdb_inv_preserve m m' \ mdb_inv_preserve (Q m) (Q m')" shows @@ -5315,6 +5283,46 @@ lemma cte_map_inj_eq': done context begin interpretation Arch . (*FIXME: arch-split*) + +lemma arch_mdb_assertD: + "\ m p = Some (CTE (ArchObjectCap IOPortControlCap) n); m p' = Some (CTE (ArchObjectCap IOPortControlCap) n'); + arch_mdb_assert m \ \ p' = p" + unfolding arch_mdb_assert_def by blast + +lemma ioport_revocable: + "\ m p = Some (CTE (ArchObjectCap IOPortControlCap) n); arch_mdb_assert m \ \ mdbRevocable n" + unfolding arch_mdb_assert_def by blast + +lemma arch_mdb_assert_cross: + "\ valid_arch_mdb (is_original_cap s) (caps_of_state s); ioport_control_unique s; valid_objs s; + (s,s') \ state_relation \ + \ arch_mdb_assert (ctes_of s')" + unfolding arch_mdb_assert_def valid_arch_mdb_def + apply clarsimp + apply (frule (2) caps_of_state_rev_cross) + apply clarsimp + apply (rule conjI) + (* revocable *) + apply (simp add: ioport_revocable_def) + apply (erule allE, erule allE, erule (1) impE) + apply (erule state_relationE) + apply (clarsimp simp: revokable_relation_def) + apply (force simp: null_filter_def) + (* ioport_control_unique *) + apply (thin_tac "ctes_of s' _ = _") + apply (clarsimp simp: ioport_control_unique_def) + apply (drule (2) caps_of_state_rev_cross) + apply fastforce + done + +(* interface lemma: generic statement, arch-specific proof *) +lemma archMDBAssertions_cross: + "\ valid_arch_mdb (is_original_cap s) (caps_of_state s); valid_arch_state s; valid_objs s; + (s, s') \ state_relation \ + \ archMDBAssertions s'" + unfolding archMDBAssertions_def + by (drule arch_mdb_assert_cross; simp add: valid_arch_state_def) + lemma cteInsert_corres: notes split_paired_All[simp del] split_paired_Ex[simp del] trans_state_update'[symmetric,simp] @@ -5323,30 +5331,33 @@ lemma cteInsert_corres: (valid_objs and pspace_distinct and pspace_aligned and valid_mdb and valid_list and K (src\dest) and cte_wp_at (\c. c=Structures_A.NullCap) dest and - (\s. cte_wp_at (is_derived (cdt s) src c) src s)) + (\s. cte_wp_at (is_derived (cdt s) src c) src s) and valid_arch_state) (pspace_distinct' and pspace_aligned' and valid_mdb' and valid_cap' c' and cte_wp_at' (\c. cteCap c=NullCap) dest') (cap_insert c src dest) (cteInsert c' src' dest')" - (is "corres _ (?P and (\s. cte_wp_at _ _ s)) (?P' and cte_wp_at' _ _) _ _") + (is "corres _ (?P and (\s. cte_wp_at _ _ s) and valid_arch_state) (?P' and cte_wp_at' _ _) _ _") using assms unfolding cap_insert_def cteInsert_def apply simp + (* this lemma doesn't use the assertion, but does need to establish it *) + apply (rule corres_stateAssert_add_assertion[rotated]) + apply (rule archMDBAssertions_cross; simp add: valid_mdb_def) apply (rule corres_guard_imp) apply (rule corres_split[OF get_cap_corres]) apply (rule corres_split[OF get_cap_corres]) - apply (rule_tac F="cteCap rv' = NullCap" in corres_gen_asm2) + apply (rule_tac F="cteCap oldCTE = NullCap" in corres_gen_asm2) apply simp apply (rule_tac P="?P and cte_at dest and (\s. cte_wp_at (is_derived (cdt s) src c) src s) and cte_wp_at ((=) src_cap) src" and Q="?P' and - cte_wp_at' ((=) rv') (cte_map dest) and + cte_wp_at' ((=) oldCTE) (cte_map dest) and cte_wp_at' ((=) srcCTE) (cte_map src)" in corres_assert_assume) prefer 2 apply (clarsimp simp: cte_wp_at_ctes_of valid_mdb'_def valid_mdb_ctes_def valid_nullcaps_def) - apply (case_tac rv') + apply (case_tac oldCTE) apply (simp add: initMDBNode_def) apply (erule allE)+ apply (erule (1) impE) @@ -5355,7 +5366,7 @@ lemma cteInsert_corres: apply (rule_tac R="\r. ?P and cte_at dest and (\s. (is_derived (cdt s) src c) src_cap) and cte_wp_at ((=) (masked_as_full src_cap c)) src" and - R'="\r. ?P' and cte_wp_at' ((=) rv') (cte_map dest) and + R'="\r. ?P' and cte_wp_at' ((=) oldCTE) (cte_map dest) and cte_wp_at' ((=) (CTE (maskedAsFull (cteCap srcCTE) c') (cteMDBNode srcCTE))) (cte_map src)" in corres_split[where r'=dc]) @@ -5442,7 +5453,7 @@ lemma cteInsert_corres: apply(rule conjI) apply (case_tac "srcCTE") apply (rename_tac src_cap' src_node) - apply (case_tac "rv'") + apply (case_tac "oldCTE") apply (rename_tac dest_node) apply (clarsimp simp: in_set_cap_cte_at_swp) apply (subgoal_tac "cte_at src a \ is_derived (cdt a) src c src_cap") @@ -5712,7 +5723,7 @@ lemma cteInsert_corres: apply clarsimp apply (subgoal_tac "mdbRevocable node = isCapRevocable c' (cteCap srcCTE)") prefer 2 - apply (case_tac rv') + apply (case_tac oldCTE) subgoal by (clarsimp simp add: const_def modify_map_def split: if_split_asm) apply simp apply (rule is_cap_revocable_eq, assumption, assumption) @@ -5725,7 +5736,7 @@ lemma cteInsert_corres: split:if_splits dest!:cap_master_cap_eqDs) apply clarsimp apply (case_tac srcCTE) - apply (case_tac rv') + apply (case_tac oldCTE) apply clarsimp apply (subgoal_tac "\cap' node'. ctes_of b (cte_map (aa,bb)) = Some (CTE cap' node')") prefer 2 @@ -5752,14 +5763,14 @@ lemma cteInsert_corres: apply (wp set_untyped_cap_full_valid_objs set_untyped_cap_as_full_valid_mdb set_untyped_cap_as_full_cte_wp_at setUntypedCapAsFull_valid_cap setUntypedCapAsFull_cte_wp_at | clarsimp simp: cte_wp_at_caps_of_state| wps)+ - apply (case_tac rv',clarsimp simp:cte_wp_at_ctes_of maskedAsFull_def) + apply (case_tac oldCTE, clarsimp simp:cte_wp_at_ctes_of maskedAsFull_def) apply (wp getCTE_wp' get_cap_wp)+ apply clarsimp subgoal by (fastforce elim: cte_wp_at_weakenE) apply (clarsimp simp: cte_wp_at'_def) apply (case_tac "srcCTE") apply (rename_tac src_cap' src_node) - apply (case_tac "rv'") + apply (case_tac "oldCTE") apply (rename_tac dest_node) apply (clarsimp simp: in_set_cap_cte_at_swp) apply (subgoal_tac "cte_at src a \ is_derived (cdt a) src c src_cap") diff --git a/proof/refine/X64/CSpace_I.thy b/proof/refine/X64/CSpace_I.thy index da26dd48aa..7905f2df9f 100644 --- a/proof/refine/X64/CSpace_I.thy +++ b/proof/refine/X64/CSpace_I.thy @@ -1418,8 +1418,7 @@ lemma untyped_mdb: "untyped_mdb' m" and untyped_inc: "untyped_inc' m" and class_links: "class_links m" and - irq_control: "irq_control m" and - arch_mdb_ctes: "valid_arch_mdb_ctes m" (* FIXME arch-split: this should be valid_arch_mdb_ctes *) + irq_control: "irq_control m" using valid by (simp_all add: valid_mdb_ctes_def) @@ -1956,35 +1955,6 @@ lemma irq_control_init: apply (erule (1) irq_controlD, rule ctrl) done -definition - "no_ioport' m \ \p cte. m p = Some cte \ cteCap cte \ (ArchObjectCap IOPortControlCap)" - -lemma no_ioportD': - "\ m p = Some (CTE (ArchObjectCap IOPortControlCap) n); no_ioport' m \ \ False" - unfolding no_ioport'_def - apply (erule allE, erule allE, erule (1) impE) - apply auto - done - -lemma ioport_control_init: - assumes no_ioport: "cap = (ArchObjectCap IOPortControlCap) \ no_ioport' m" - assumes ctrl: "ioport_control m" - shows "ioport_control (m(p \ CTE cap initMDBNode))" - using no_ioport - apply (clarsimp simp: ioport_control_def) - apply (rule conjI) - apply (clarsimp simp: initMDBNode_def) - apply (erule (1) no_ioportD') - apply clarsimp - apply (frule ioport_revocable, rule ctrl) - apply clarsimp - apply (rule conjI) - apply clarsimp - apply (erule (1) no_ioportD') - apply clarsimp - apply (erule (1) ioport_controlD, rule ctrl) - done - lemma valid_mdb_ctes_init: "\ valid_mdb_ctes m; m p = Some cte; no_mdb cte; caps_no_overlap' m (capRange cap); s \' cap; @@ -2019,10 +1989,8 @@ lemma valid_mdb_ctes_init: apply (rule valid_capAligned, erule(1) ctes_of_valid_cap') apply (rule conjI) apply (erule (1) irq_control_init) - apply (rule conjI) - apply (simp add: ran_def reply_masters_rvk_fb_def) - apply (auto simp: initMDBNode_def)[1] - apply (erule (1) ioport_control_init) + apply (simp add: ran_def reply_masters_rvk_fb_def) + apply (auto simp: initMDBNode_def)[1] done lemma setCTE_state_refs_of'[wp]: diff --git a/proof/refine/X64/CSpace_R.thy b/proof/refine/X64/CSpace_R.thy index a61db81a45..e97fda36d3 100644 --- a/proof/refine/X64/CSpace_R.thy +++ b/proof/refine/X64/CSpace_R.thy @@ -1405,24 +1405,6 @@ lemma (in mdb_insert_der) irq_control_n: apply (erule (1) irq_controlD, rule irq_control) done -(* FIXME arch-split: locale issues here, can't place in Arch, need to re-work hierarchy *) -lemma (in mdb_insert_der) ioport_control_n: - "X64.ioport_control n" - using src dest partial_is_derived' - apply (clarsimp simp: X64.ioport_control_def) - apply (frule n_cap) - apply (drule n_revocable) - apply (clarsimp split: if_split_asm) - apply (simp add: is_derived'_def isCap_simps) - apply (frule X64.ioport_revocable, rule arch_mdb_ctes[simplified X64.valid_arch_mdb_ctes_def]) - apply clarsimp - apply (drule n_cap) - apply (clarsimp split: if_split_asm) - apply (erule disjE) - apply (clarsimp simp: is_derived'_def isCap_simps) - apply (erule (1) X64.ioport_controlD, rule arch_mdb_ctes[simplified X64.valid_arch_mdb_ctes_def]) - done - context mdb_insert_child begin @@ -1998,73 +1980,6 @@ lemma cteInsert_irq_control: apply (clarsimp simp: modify_map_apply irq_control_prev_update fun_upd_def) done -lemma ioport_control_prev_update: - "ioport_control (modify_map m x (cteMDBNode_update (mdbPrev_update f))) = ioport_control m" - apply (simp add: ioport_control_def) - apply (rule iffI) - apply clarsimp - apply (simp only: modify_map_if) - apply (erule_tac x=p in allE) - apply (simp (no_asm_use) split: if_split_asm) - apply (case_tac "x=p") - apply fastforce - apply clarsimp - apply (erule_tac x=p' in allE) - apply simp - apply (case_tac "x=p'") - apply simp - apply fastforce - apply clarsimp - apply (erule_tac x=p in allE) - apply (simp add: modify_map_if split: if_split_asm) - apply clarsimp - apply (case_tac "x=p'") - apply clarsimp - apply clarsimp - apply clarsimp - apply (case_tac "x=p'") - apply clarsimp - apply clarsimp - done - -lemma cteInsert_ioport_control: - "\valid_mdb' and pspace_distinct' and pspace_aligned' and (\s. src \ dest) and - (\s. cte_wp_at' (is_derived' (ctes_of s) src cap \ cteCap) src s)\ - cteInsert cap src dest - \\_ s. ioport_control (ctes_of s)\" - apply (unfold cteInsert_def updateCap_def) - apply (simp add: valid_mdb'_def split del: if_split) - apply (wp updateMDB_ctes_of_no_0 getCTE_wp') - apply (clarsimp simp: cte_wp_at_ctes_of simp del: fun_upd_apply) - apply (wp hoare_vcg_imp_lift hoare_vcg_all_lift setUntypedCapAsFull_ctes_of - setUntypedCapAsFull_ctes_of_no_0 setUntypedCapAsFull_ioport_control mdb_inv_preserve_fun_upd - mdb_inv_preserve_modify_map,simp) - apply (wp getCTE_wp)+ - apply (clarsimp simp:cte_wp_at_ctes_of simp del:fun_upd_apply) - apply (subgoal_tac "src \ 0") - prefer 2 - apply (fastforce simp: valid_mdb_ctes_def no_0_def) - apply (subgoal_tac "dest \ 0") - prefer 2 - apply (fastforce simp: valid_mdb_ctes_def no_0_def) - apply (rule conjI) - apply (fastforce simp: valid_mdb_ctes_def no_0_def) - apply (case_tac cte) - apply (rename_tac s_cap s_node) - apply (case_tac cteb) - apply (rename_tac d_cap d_node) - apply (simp add: nullPointer_def) - apply (subgoal_tac "mdb_insert_der (ctes_of s) src s_cap s_node dest NullCap d_node cap") - prefer 2 - apply unfold_locales[1] - apply (assumption|rule refl)+ - apply (simp add: valid_mdb_ctes_def) - apply (simp add: valid_mdb_ctes_def) - apply assumption+ - apply (drule mdb_insert_der.ioport_control_n) - apply (clarsimp simp: modify_map_apply ioport_control_prev_update fun_upd_def) - done - lemma capMaster_isUntyped: "capMasterCap c = capMasterCap c' \ isUntypedCap c = isUntypedCap c'" by (simp add: capMasterCap_def isCap_simps split: capability.splits) @@ -2241,7 +2156,7 @@ lemma cteInsert_mdb' [wp]: \\_. valid_mdb'\" apply (simp add:valid_mdb'_def valid_mdb_ctes_def) apply (rule_tac Q'="\r s. valid_dlist (ctes_of s) \ irq_control (ctes_of s) \ - no_0 (ctes_of s) \ mdb_chain_0 (ctes_of s) \ ioport_control (ctes_of s) \ + no_0 (ctes_of s) \ mdb_chain_0 (ctes_of s) \ mdb_chunked (ctes_of s) \ untyped_mdb' (ctes_of s) \ untyped_inc' (ctes_of s) \ Q s" for Q in hoare_strengthen_post) @@ -2250,7 +2165,7 @@ lemma cteInsert_mdb' [wp]: apply assumption apply (rule hoare_name_pre_state) apply (wp cteInsert_no_0 cteInsert_valid_dlist cteInsert_mdb_chain_0 cteInsert_untyped_inc' - cteInsert_mdb_chunked cteInsert_untyped_mdb cteInsert_irq_control cteInsert_ioport_control) + cteInsert_mdb_chunked cteInsert_untyped_mdb cteInsert_irq_control) apply (unfold cteInsert_def) apply (unfold cteInsert_def updateCap_def) apply (simp add: valid_mdb'_def split del: if_split) @@ -2308,7 +2223,6 @@ proof - and class_links: "class_links ?m" and distinct_zombies: "distinct_zombies ?m" and irq: "irq_control ?m" - and ioport: "ioport_control ?m" and reply_masters_rvk_fb: "reply_masters_rvk_fb ?m" and vn: "valid_nullcaps ?m" and ut_rev:"ut_revocable' ?m" @@ -4541,14 +4455,9 @@ lemma arch_update_setCTE_mdb: apply (clarsimp simp: is_arch_update'_def isCap_simps) apply (rule conjI) apply clarsimp - apply (rule conjI) - apply (simp add: reply_masters_rvk_fb_def) - apply (erule ball_ran_fun_updI) - apply (clarsimp simp add: is_arch_update'_def isCap_simps) - apply (clarsimp simp: is_arch_update'_def) - apply (case_tac cap; clarsimp simp: isCap_simps) - apply (case_tac x8; clarsimp simp: isCap_simps ioport_control_def) - apply auto + apply (simp add: reply_masters_rvk_fb_def) + apply (erule ball_ran_fun_updI) + apply (clarsimp simp add: is_arch_update'_def isCap_simps) done lemma capMaster_zobj_refs: @@ -4673,6 +4582,7 @@ end locale mdb_insert_simple = mdb_insert + assumes safe_parent: "safe_parent_for' m src c'" assumes simple: "is_simple_cap' c'" + assumes arch_mdb_assert: "arch_mdb_assert m" begin interpretation Arch . (*FIXME: arch-split*) lemma dest_no_parent_n: @@ -4711,7 +4621,7 @@ lemma src_node_revokable [simp]: apply (erule disjE) apply (clarsimp simp: ut_revocable'_def) apply (clarsimp simp: isCap_simps) - apply (erule ioport_revocable, rule arch_mdb_ctes[simplified]) + apply (erule ioport_revocable, rule arch_mdb_assert) done lemma new_child [simp]: @@ -4876,6 +4786,15 @@ lemma maskedAsFull_revokable_safe_parent: context begin interpretation Arch . (*FIXME: arch-split*) +(* FIXME arch-split: generic statement, arch specific proof *) +lemma setUntypedCapAsFull_archMDBAssertions[wp]: + "setUntypedCapAsFull src_cap cap p \archMDBAssertions\" + unfolding setUntypedCapAsFull_def archMDBAssertions_def updateCap_def + apply (wpsimp wp: getCTE_wp') + apply (rename_tac cte, case_tac cte, rename_tac cte_cap node) + apply (clarsimp simp: arch_mdb_assert_def cte_wp_at_ctes_of isCap_simps split: if_split_asm) + done + lemma cteInsert_simple_corres: assumes "cap_relation c c'" "src' = cte_map src" "dest' = cte_map dest" notes trans_state_update'[symmetric,simp] @@ -4884,34 +4803,36 @@ lemma cteInsert_simple_corres: valid_mdb and valid_list and K (src\dest) and cte_wp_at (\c. c=cap.NullCap) dest and K (is_simple_cap c) and - (\s. cte_wp_at (safe_parent_for (cdt s) src c) src s)) + (\s. cte_wp_at (safe_parent_for (cdt s) src c) src s) and valid_arch_state) (pspace_distinct' and pspace_aligned' and valid_mdb' and valid_cap' c' and K (is_simple_cap' c') and cte_wp_at' (\c. cteCap c=NullCap) dest' and (\s. safe_parent_for' (ctes_of s) src' c')) (cap_insert c src dest) (cteInsert c' src' dest')" - (is "corres _ (?P and (\s. cte_wp_at _ _ s)) (?P' and cte_wp_at' _ _ and _) _ _") + (is "corres _ (?P and (\s. cte_wp_at _ _ s) and valid_arch_state) (?P' and cte_wp_at' _ _ and _) _ _") using assms unfolding cap_insert_def cteInsert_def supply subst_all [simp del] apply simp + apply (rule corres_stateAssert_add_assertion[rotated]) + apply (rule archMDBAssertions_cross; simp add: valid_mdb_def) apply (rule corres_guard_imp) apply (rule corres_split[OF get_cap_corres]) apply (rule corres_split[OF get_cap_corres]) - apply (rule_tac F="cteCap rv' = NullCap" in corres_gen_asm2) + apply (rule_tac F="cteCap oldCTE = NullCap" in corres_gen_asm2) apply simp apply (rule_tac P="?P and cte_at dest and (\s. cte_wp_at (safe_parent_for (cdt s) src c) src s) and cte_wp_at ((=) src_cap) src" and - Q="?P' and - cte_wp_at' ((=) rv') (cte_map dest) and + Q="?P' and archMDBAssertions and + cte_wp_at' ((=) oldCTE) (cte_map dest) and cte_wp_at' ((=) srcCTE) (cte_map src) and (\s. safe_parent_for' (ctes_of s) src' c')" in corres_assert_assume) prefer 2 apply (clarsimp simp: cte_wp_at_ctes_of valid_mdb'_def valid_mdb_ctes_def valid_nullcaps_def) - apply (case_tac rv') + apply (case_tac oldCTE) apply (simp add: initMDBNode_def) apply (erule allE)+ apply (erule (1) impE) @@ -4920,7 +4841,7 @@ lemma cteInsert_simple_corres: apply (rule_tac R="\r. ?P and cte_at dest and (\s. cte_wp_at (safe_parent_for (cdt s) src c) src s) and cte_wp_at ((=) (masked_as_full src_cap c)) src" and - R'="\r. ?P' and cte_wp_at' ((=) rv') (cte_map dest) + R'="\r. ?P' and archMDBAssertions and cte_wp_at' ((=) oldCTE) (cte_map dest) and cte_wp_at' ((=) (CTE (maskedAsFull (cteCap srcCTE) c') (cteMDBNode srcCTE))) (cte_map src) and (\s. safe_parent_for' (ctes_of s) src' c')" in corres_split[where r'=dc]) @@ -5015,7 +4936,7 @@ lemma cteInsert_simple_corres: apply clarsimp apply (subgoal_tac "mdbRevocable node = isCapRevocable c' (cteCap srcCTE)") prefer 2 - apply (case_tac rv') + apply (case_tac oldCTE) apply (clarsimp simp add: const_def modify_map_def split: if_split_asm) apply clarsimp apply (rule is_cap_revocable_eq, assumption, assumption) @@ -5028,7 +4949,7 @@ lemma cteInsert_simple_corres: apply (clarsimp simp: cte_wp_at_def is_simple_cap_def) apply clarsimp apply (case_tac srcCTE) - apply (case_tac rv') + apply (case_tac oldCTE) apply clarsimp apply (subgoal_tac "\cap' node'. ctes_of b (cte_map (aa,bb)) = Some (CTE cap' node')") prefer 2 @@ -5052,14 +4973,14 @@ lemma cteInsert_simple_corres: set_untyped_cap_as_full_cte_wp_at setUntypedCapAsFull_valid_cap setUntypedCapAsFull_cte_wp_at setUntypedCapAsFull_safe_parent_for' | clarsimp | wps)+ apply (clarsimp simp:cte_wp_at_caps_of_state ) - apply (case_tac rv',clarsimp simp:cte_wp_at_ctes_of maskedAsFull_def) + apply (case_tac oldCTE,clarsimp simp:cte_wp_at_ctes_of maskedAsFull_def) apply (wp getCTE_wp' get_cap_wp)+ apply clarsimp subgoal by (fastforce elim: cte_wp_at_weakenE) subgoal by (clarsimp simp: cte_wp_at'_def) apply (case_tac "srcCTE") apply (rename_tac src_cap' src_node) - apply (case_tac "rv'") + apply (case_tac "oldCTE") apply (rename_tac dest_node) apply (clarsimp simp: in_set_cap_cte_at_swp) apply (subgoal_tac "cte_at src a \ safe_parent_for (cdt a) src c src_cap") @@ -5083,7 +5004,8 @@ lemma cteInsert_simple_corres: apply (simp (no_asm_simp) add: cdt_relation_def split: if_split) apply (intro impI allI) apply (frule mdb_insert_simple_axioms.intro) - apply(clarsimp simp:cte_wp_at_ctes_of) + apply(clarsimp simp:cte_wp_at_ctes_of) + apply (simp add: archMDBAssertions_def) apply (drule (1) mdb_insert_simple.intro) apply (drule_tac src_cap' = src_cap' in maskedAsFull_revokable_safe_parent[symmetric]) apply simp+ @@ -5740,7 +5662,7 @@ lemma ioport_control_src: apply (erule disjE, clarsimp simp: isCap_simps) apply (erule disjE, clarsimp simp: isCap_simps capRange_def) apply (clarsimp simp: isCap_simps split: if_split_asm) - apply (drule (1) ioport_controlD, rule arch_mdb_ctes[simplified]) + apply (drule (1) arch_mdb_assertD, rule arch_mdb_assert) apply simp done @@ -5955,26 +5877,6 @@ lemma irq' [simp]: apply (erule (1) irq_controlD, rule irq_control) done -context begin interpretation Arch . (* FIXME arch-split *) - -lemma ioport' [simp]: - "ioport_control n'" using simple - apply (clarsimp simp: ioport_control_def) - apply (frule n'_cap) - apply (drule n'_rev) - apply (clarsimp split: if_split_asm) - apply (simp add: is_simple_cap'_def isCap_simps) - apply (frule ioport_revocable, rule arch_mdb_ctes[simplified]) - apply clarsimp - apply (drule n'_cap) - apply (clarsimp split: if_split_asm) - apply (erule disjE) - apply (clarsimp simp: is_simple_cap'_def isCap_simps) - apply (erule (1) ioport_controlD, rule arch_mdb_ctes[simplified]) - done - -end - lemma reply_masters_rvk_fb: "reply_masters_rvk_fb m" using valid by (simp add: valid_mdb_ctes_def) @@ -6047,7 +5949,7 @@ lemma cteInsert_simple_mdb': mdb_ptr_axioms.intro mdb_insert_axioms.intro) apply (simp add:modify_map_def valid_mdb_ctes_maskedAsFull)+ apply (clarsimp simp:nullPointer_def)+ - apply ((clarsimp simp:valid_mdb_ctes_def)+) + apply (clarsimp simp:valid_mdb_ctes_def archMDBAssertions_def)+ apply (drule mdb_insert_simple'.mdb) apply (clarsimp simp:valid_mdb_ctes_def) done diff --git a/proof/refine/X64/Detype_R.thy b/proof/refine/X64/Detype_R.thy index 62401110d4..64ba5bb398 100644 --- a/proof/refine/X64/Detype_R.thy +++ b/proof/refine/X64/Detype_R.thy @@ -628,7 +628,6 @@ lemma valid_objs: "valid_objs' s'" and ut_rev: "ut_revocable' (ctes_of s')" and dist_z: "distinct_zombies (ctes_of s')" and irq_ctrl: "irq_control (ctes_of s')" - and ioport_ctrl: "ioport_control (ctes_of s')" and clinks: "class_links (ctes_of s')" and rep_r_fb: "reply_masters_rvk_fb (ctes_of s')" and idle: "valid_idle' s'" @@ -1586,10 +1585,6 @@ proof (simp add: invs'_def valid_state'_def valid_pspace'_def show "irq_control ?ctes'" by (clarsimp simp: irq_control_def) - from ioport_ctrl - show "valid_arch_mdb_ctes ?ctes'" - by (clarsimp simp: ioport_control_def) - from dist_z show "distinct_zombies ?ctes'" apply (simp add: tree_to_ctes distinct_zombies_def diff --git a/proof/refine/X64/Finalise_R.thy b/proof/refine/X64/Finalise_R.thy index 8774905fa1..1c1a83cc29 100644 --- a/proof/refine/X64/Finalise_R.thy +++ b/proof/refine/X64/Finalise_R.thy @@ -1060,19 +1060,6 @@ lemma irq_control_n [simp]: "irq_control n" apply (erule (1) irq_controlD, rule irq_control) done -lemma ioport_control_n [simp]: "ioport_control n" - using slot - apply (clarsimp simp: ioport_control_def) - apply (frule n_revokable) - apply (drule n_cap) - apply (clarsimp split: if_split_asm) - apply (frule ioport_revocable, rule arch_mdb_ctes[simplified]) - apply clarsimp - apply (drule n_cap) - apply (clarsimp simp: if_split_asm) - apply (erule (1) ioport_controlD, rule arch_mdb_ctes[simplified]) - done - lemma reply_masters_rvk_fb_m: "reply_masters_rvk_fb m" using valid by auto diff --git a/proof/refine/X64/Interrupt_R.thy b/proof/refine/X64/Interrupt_R.thy index 755fdc12ee..6f234a3bde 100644 --- a/proof/refine/X64/Interrupt_R.thy +++ b/proof/refine/X64/Interrupt_R.thy @@ -500,6 +500,13 @@ crunch X64_H.updateIRQState and ex_cte_cap_wp_to'[wp]: "ex_cte_cap_wp_to' a b" (simp: ex_cte_cap_wp_to'_def valid_mdb'_def) +crunch set_irq_state + for valid_arch_state[wp]: valid_arch_state + +lemma maxUserIRQ_le_maxIRQ: + "X64.maxUserIRQ \ maxIRQ" + by (simp add: X64.maxUserIRQ_def maxIRQ_def) + lemma arch_performIRQControl_corres: "arch_irq_control_inv_relation x2 ivk' \ corres (dc \ dc) (einvs and arch_irq_control_inv_valid x2) @@ -516,10 +523,12 @@ lemma arch_performIRQControl_corres: apply (rule setIRQState_corres) apply (simp add: irq_state_relation_def) apply (rule cteInsert_simple_corres) - apply (wpsimp simp: IRQHandler_valid IRQHandler_valid' | wps)+ + apply (wpsimp simp: IRQHandler_valid IRQHandler_valid' + | strengthen invs_arch_state + | wps)+ apply (clarsimp simp: invs_def valid_state_def valid_pspace_def cte_wp_at_caps_of_state is_simple_cap_def is_cap_simps arch_irq_control_inv_valid_def - safe_parent_for_def) + safe_parent_for_def order_trans[OF _ maxUserIRQ_le_maxIRQ]) apply (clarsimp simp: invs'_def valid_state'_def valid_pspace'_def IRQHandler_valid IRQHandler_valid' is_simple_cap'_def isCap_simps IRQ_def) apply (clarsimp simp: safe_parent_for'_def cte_wp_at_ctes_of) @@ -533,10 +542,12 @@ lemma arch_performIRQControl_corres: apply (rule setIRQState_corres) apply (simp add: irq_state_relation_def) apply (rule cteInsert_simple_corres) - apply (wpsimp simp: IRQHandler_valid IRQHandler_valid' | wps)+ + apply (wpsimp simp: IRQHandler_valid IRQHandler_valid' + | strengthen invs_arch_state + | wps)+ apply (clarsimp simp: invs_def valid_state_def valid_pspace_def cte_wp_at_caps_of_state is_simple_cap_def is_cap_simps arch_irq_control_inv_valid_def - safe_parent_for_def) + safe_parent_for_def order_trans[OF _ maxUserIRQ_le_maxIRQ]) apply (clarsimp simp: invs'_def valid_state'_def valid_pspace'_def IRQHandler_valid IRQHandler_valid' is_simple_cap'_def isCap_simps IRQ_def) apply (clarsimp simp: safe_parent_for'_def cte_wp_at_ctes_of) diff --git a/proof/refine/X64/Ipc_R.thy b/proof/refine/X64/Ipc_R.thy index b598d115d6..d5e2c5e684 100644 --- a/proof/refine/X64/Ipc_R.thy +++ b/proof/refine/X64/Ipc_R.thy @@ -392,6 +392,10 @@ lemma cte_refs'_maskedAsFull[simp]: apply (clarsimp simp:maskedAsFull_def isCap_simps)+ done +lemma set_extra_badge_valid_arch_state[wp]: + "set_extra_badge buffer badge n \ valid_arch_state \" + unfolding set_extra_badge_def + by wp lemma transferCapsToSlots_corres: "\ list_all2 (\(cap, slot) (cap', slot'). cap_relation cap cap' @@ -399,7 +403,7 @@ lemma transferCapsToSlots_corres: mi' = message_info_map mi \ \ corres ((=) \ message_info_map) (\s. valid_objs s \ pspace_aligned s \ pspace_distinct s \ valid_mdb s - \ valid_list s + \ valid_list s \ valid_arch_state s \ (case ep of Some x \ ep_at x s | _ \ True) \ (\x \ set slots. cte_wp_at (\cap. cap = cap.NullCap) x s \ real_cte_at x s) @@ -473,7 +477,8 @@ next apply (simp add: tl_map) apply (rule corres_rel_imp, rule Cons.hyps, simp_all)[1] apply (wp valid_case_option_post_wp hoare_vcg_const_Ball_lift - hoare_vcg_const_Ball_lift cap_insert_weak_cte_wp_at) + hoare_vcg_const_Ball_lift cap_insert_derived_valid_arch_state + cap_insert_weak_cte_wp_at) apply (wp hoare_vcg_const_Ball_lift | simp add:split_def del: imp_disj1)+ apply (wp cap_insert_cte_wp_at) apply (wp valid_case_option_post_wp hoare_vcg_const_Ball_lift @@ -614,6 +619,7 @@ lemma cteInsert_assume_Null: apply (rule hoare_name_pre_state) apply (erule impCE) apply (simp add: cteInsert_def) + apply (rule bind_wp[OF _ stateAssert_sp]) apply (rule bind_wp[OF _ getCTE_sp])+ apply (rule hoare_name_pre_state) apply (clarsimp simp: cte_wp_at_ctes_of) @@ -1040,7 +1046,7 @@ lemma transferCaps_corres: corres ((=) \ message_info_map) (tcb_at receiver and valid_objs and pspace_aligned and pspace_distinct and valid_mdb - and valid_list + and valid_list and valid_arch_state and (\s. case ep of Some x \ ep_at x s | _ \ True) and case_option \ in_user_frame recv_buf and (\s. valid_message_info info) @@ -1459,10 +1465,14 @@ lemma copyMRs_valid_mdb[wp]: "\valid_mdb'\ copyMRs t buf t' buf' n \\rv. valid_mdb'\" by (simp add: valid_mdb'_def copyMRs_ctes_of) +crunch copy_mrs + for valid_arch_state[wp]: valid_arch_state + (wp: crunch_wps) + lemma doNormalTransfer_corres: "corres dc (tcb_at sender and tcb_at receiver and (pspace_aligned:: det_state \ bool) - and valid_objs and cur_tcb and valid_mdb and valid_list and pspace_distinct + and valid_objs and cur_tcb and valid_mdb and valid_list and valid_arch_state and pspace_distinct and (\s. case ep of Some x \ ep_at x s | _ \ True) and case_option \ in_user_frame send_buf and case_option \ in_user_frame recv_buf) @@ -1733,7 +1743,7 @@ lemma lookupIPCBuffer_valid_ipc_buffer [wp]: lemma doIPCTransfer_corres: "corres dc (tcb_at s and tcb_at r and valid_objs and pspace_aligned - and valid_list + and valid_list and valid_arch_state and pspace_distinct and valid_mdb and cur_tcb and (\s. case ep of Some x \ ep_at x s | _ \ True)) (tcb_at' s and tcb_at' r and valid_pspace' and cur_tcb' @@ -1741,9 +1751,9 @@ lemma doIPCTransfer_corres: (do_ipc_transfer s ep bg grt r) (doIPCTransfer s ep bg grt r)" apply (simp add: do_ipc_transfer_def doIPCTransfer_def) - apply (rule_tac Q="%receiveBuffer sa. tcb_at s sa \ valid_objs sa \ - pspace_aligned sa \ tcb_at r sa \ - cur_tcb sa \ valid_mdb sa \ valid_list sa \ pspace_distinct sa \ + apply (rule_tac Q="\receiveBuffer sa. tcb_at s sa \ valid_objs sa \ + pspace_aligned sa \ pspace_distinct sa \ tcb_at r sa \ + cur_tcb sa \ valid_mdb sa \ valid_list sa \ valid_arch_state sa \ (case ep of None \ True | Some x \ ep_at x sa) \ case_option (\_. True) in_user_frame receiveBuffer sa \ obj_at (\ko. \tcb. ko = TCB tcb @@ -2329,7 +2339,7 @@ lemma setupCallerCap_corres: (st_tcb_at (Not \ halted) sender and tcb_at receiver and st_tcb_at (Not \ awaiting_reply) sender and valid_reply_caps and valid_objs and pspace_distinct and pspace_aligned and valid_mdb - and valid_list and + and valid_list and valid_arch_state and valid_reply_masters and cte_wp_at (\c. c = cap.NullCap) (receiver, tcb_cnode_index 3)) (tcb_at' sender and tcb_at' receiver and valid_pspace' and (\s. weak_sch_act_wf (ksSchedulerAction s) s)) @@ -2546,6 +2556,7 @@ proof - valid_queues_in_correct_ready_q valid_queues_ready_qs_distinct valid_sched_valid_queues)+ apply ((wp hoare_drop_imps do_ipc_transfer_tcb_caps weak_valid_sched_action_lift + do_ipc_transfer_valid_arch | clarsimp simp: is_cap_simps)+)[1] apply (simp add: pred_conj_def) apply (strengthen sch_act_wf_weak) @@ -3245,7 +3256,7 @@ lemma receiveIPC_corres: apply (rule corres_split[OF doIPCTransfer_corres]) apply (simp split del: if_split cong: if_cong) apply (fold dc_def)[1] - apply (rule_tac P="valid_objs and valid_mdb and valid_list + apply (rule_tac P="valid_objs and valid_mdb and valid_list and valid_arch_state and valid_sched and cur_tcb and valid_reply_caps @@ -3275,7 +3286,7 @@ lemma receiveIPC_corres: apply (fastforce simp: st_tcb_at_tcb_at st_tcb_def2 valid_sched_def valid_sched_action_def) apply (clarsimp split: if_split_asm) - apply (clarsimp | wp do_ipc_transfer_tcb_caps)+ + apply (clarsimp | wp do_ipc_transfer_tcb_caps do_ipc_transfer_valid_arch)+ apply (rule_tac Q'="\_ s. sch_act_wf (ksSchedulerAction s) s \ sym_heap_sched_pointers s \ valid_sched_pointers s \ pspace_aligned' s \ pspace_distinct' s" @@ -3607,19 +3618,12 @@ lemma cteInsert_cap_to': "\ex_nonz_cap_to' p and cte_wp_at' (\c. cteCap c = NullCap) dest\ cteInsert cap src dest \\rv. ex_nonz_cap_to' p\" - apply (simp add: cteInsert_def ex_nonz_cap_to'_def - updateCap_def setUntypedCapAsFull_def - split del: if_split) - apply (rule hoare_pre, rule hoare_vcg_ex_lift) - apply (wp updateMDB_weak_cte_wp_at - setCTE_weak_cte_wp_at - | simp - | rule hoare_drop_imps)+ - apply (wp getCTE_wp) - apply clarsimp + apply (simp add: cteInsert_def ex_nonz_cap_to'_def updateCap_def setUntypedCapAsFull_def) + apply (wpsimp wp: updateMDB_weak_cte_wp_at setCTE_weak_cte_wp_at hoare_vcg_ex_lift + | rule hoare_drop_imps + | wp getCTE_wp)+ (* getCTE_wp is separate to apply it only to the last one *) apply (rule_tac x=cref in exI) - apply (rule conjI) - apply (clarsimp simp: cte_wp_at_ctes_of)+ + apply (fastforce simp: cte_wp_at_ctes_of) done crunch setExtraBadge diff --git a/proof/refine/X64/Retype_R.thy b/proof/refine/X64/Retype_R.thy index 24fd400795..e5e6bca43b 100644 --- a/proof/refine/X64/Retype_R.thy +++ b/proof/refine/X64/Retype_R.thy @@ -3029,15 +3029,6 @@ lemma irq_control_n: apply (erule (1) irq_controlD, rule irq_control) done -lemma ioport_control_n: - "ioport_control n" - apply (clarsimp simp add: ioport_control_def) - apply (simp add: n_Some_eq split: if_split_asm) - apply (frule ioport_revocable, rule arch_mdb_ctes[simplified]) - apply clarsimp - apply (erule (1) ioport_controlD, rule arch_mdb_ctes[simplified]) - done - lemma dist_z_m: "distinct_zombies m" using valid by auto @@ -3065,7 +3056,7 @@ lemma valid_n: by (simp add: valid_mdb_ctes_def dlist_n no_0_n mdb_chain_0_n valid_badges_n caps_contained_n untyped_mdb_n untyped_inc_n mdb_chunked_n valid_nullcaps_n ut_rev_n - class_links_n irq_control_n dist_z_n ioport_control_n + class_links_n irq_control_n dist_z_n reply_masters_rvk_fb_n) end diff --git a/proof/refine/X64/Tcb_R.thy b/proof/refine/X64/Tcb_R.thy index 218b5d059b..1891e4e47f 100644 --- a/proof/refine/X64/Tcb_R.thy +++ b/proof/refine/X64/Tcb_R.thy @@ -867,7 +867,7 @@ lemma checkCapAt_cteInsert_corres: apply clarsimp apply (rule conjI, fastforce)+ apply (cases src_slot) - apply (clarsimp simp: cte_wp_at_caps_of_state) + apply (clarsimp simp: cte_wp_at_caps_of_state invs_arch_state) apply (rule conjI) apply (frule same_object_as_cap_master) apply (clarsimp simp: cap_master_cap_simps is_cnode_or_valid_arch_def diff --git a/proof/refine/X64/Untyped_R.thy b/proof/refine/X64/Untyped_R.thy index 90cad18eef..74903212f0 100644 --- a/proof/refine/X64/Untyped_R.thy +++ b/proof/refine/X64/Untyped_R.thy @@ -2692,14 +2692,6 @@ lemma irq_control_n' [simp]: apply (clarsimp simp: modify_map_if split: if_split_asm) done -lemma ioport_control_n' [simp]: - "ioport_control n'" - using arch_mdb_ctes[simplified] phys - apply (clarsimp simp: ioport_control_def) - apply (clarsimp simp: n'_def n_def) - apply (clarsimp simp: modify_map_if split: if_split_asm) - done - lemma dist_z_m: "distinct_zombies m" using valid by auto