From 561e031740f95ba2e2dd93a0659f942c558bb1f5 Mon Sep 17 00:00:00 2001 From: Rafal Kolanski Date: Fri, 2 Aug 2024 12:36:34 +1000 Subject: [PATCH] ainvs: remove old arch-split FIXMEs These proofs have been arch-split for some time now so the FIXMEs appear resolved. They are also non-specific, so it is impossible to tell at this point whether they referred to anything. Signed-off-by: Rafal Kolanski --- proof/invariant-abstract/AARCH64/ArchFinalise_AI.thy | 2 +- proof/invariant-abstract/ARM/ArchFinalise_AI.thy | 2 +- proof/invariant-abstract/ARM/ArchKernelInit_AI.thy | 2 +- proof/invariant-abstract/ARM/ArchRetype_AI.thy | 2 +- proof/invariant-abstract/ARM/ArchVSpaceEntries_AI.thy | 2 +- proof/invariant-abstract/ARM_HYP/ArchFinalise_AI.thy | 2 +- proof/invariant-abstract/ARM_HYP/ArchKernelInit_AI.thy | 2 +- proof/invariant-abstract/ARM_HYP/ArchRetype_AI.thy | 2 +- proof/invariant-abstract/ARM_HYP/ArchVCPU_AI.thy | 2 +- proof/invariant-abstract/ARM_HYP/ArchVSpaceEntries_AI.thy | 2 +- proof/invariant-abstract/RISCV64/ArchFinalise_AI.thy | 2 +- proof/invariant-abstract/X64/ArchFinalise_AI.thy | 5 +++-- proof/invariant-abstract/X64/ArchKernelInit_AI.thy | 2 +- proof/invariant-abstract/X64/ArchRetype_AI.thy | 2 +- proof/invariant-abstract/X64/ArchVSpaceEntries_AI.thy | 2 +- 15 files changed, 17 insertions(+), 16 deletions(-) diff --git a/proof/invariant-abstract/AARCH64/ArchFinalise_AI.thy b/proof/invariant-abstract/AARCH64/ArchFinalise_AI.thy index fc03b23bd3..4557bb0ada 100644 --- a/proof/invariant-abstract/AARCH64/ArchFinalise_AI.thy +++ b/proof/invariant-abstract/AARCH64/ArchFinalise_AI.thy @@ -1747,7 +1747,7 @@ lemma invs_valid_arch_capsI: "invs s \ valid_arch_caps s" by (simp add: invs_def valid_state_def) -context Arch begin arch_global_naming (*FIXME: arch-split*) +context Arch begin arch_global_naming lemma do_machine_op_reachable_pg_cap[wp]: "\\s. P (reachable_frame_cap cap s)\ diff --git a/proof/invariant-abstract/ARM/ArchFinalise_AI.thy b/proof/invariant-abstract/ARM/ArchFinalise_AI.thy index 2f214e6f9a..3999d88f53 100644 --- a/proof/invariant-abstract/ARM/ArchFinalise_AI.thy +++ b/proof/invariant-abstract/ARM/ArchFinalise_AI.thy @@ -1130,7 +1130,7 @@ lemma invs_valid_arch_capsI: "invs s \ valid_arch_caps s" by (simp add: invs_def valid_state_def) -context Arch begin arch_global_naming (*FIXME: arch-split*) +context Arch begin arch_global_naming lemma arch_finalise_case_no_lookup: "\pspace_aligned and valid_vspace_objs and valid_objs and diff --git a/proof/invariant-abstract/ARM/ArchKernelInit_AI.thy b/proof/invariant-abstract/ARM/ArchKernelInit_AI.thy index 693b7693a8..801c39620a 100644 --- a/proof/invariant-abstract/ARM/ArchKernelInit_AI.thy +++ b/proof/invariant-abstract/ARM/ArchKernelInit_AI.thy @@ -14,7 +14,7 @@ imports Arch_AI begin -context Arch begin arch_global_naming (*FIXME: arch-split*) +context Arch begin arch_global_naming text \ Showing that there is a state that satisfies the abstract invariants. diff --git a/proof/invariant-abstract/ARM/ArchRetype_AI.thy b/proof/invariant-abstract/ARM/ArchRetype_AI.thy index f18cdb9d22..3ec0e8cc5c 100644 --- a/proof/invariant-abstract/ARM/ArchRetype_AI.thy +++ b/proof/invariant-abstract/ARM/ArchRetype_AI.thy @@ -901,7 +901,7 @@ sublocale retype_region_proofs_gen?: retype_region_proofs_gen end -context Arch begin arch_global_naming (*FIXME: arch-split*) +context Arch begin arch_global_naming definition valid_vs_lookup2 :: "(vs_ref list \ word32) set \ (cslot_ptr \ cap) \ bool" diff --git a/proof/invariant-abstract/ARM/ArchVSpaceEntries_AI.thy b/proof/invariant-abstract/ARM/ArchVSpaceEntries_AI.thy index c96d5762fc..e54d26d89a 100644 --- a/proof/invariant-abstract/ARM/ArchVSpaceEntries_AI.thy +++ b/proof/invariant-abstract/ARM/ArchVSpaceEntries_AI.thy @@ -9,7 +9,7 @@ imports VSpaceEntries_AI begin -context Arch begin arch_global_naming (*FIXME: arch-split*) +context Arch begin arch_global_naming lemma a_type_pdD: "a_type ko = AArch APageDirectory \ \pd. ko = ArchObj (PageDirectory pd)" diff --git a/proof/invariant-abstract/ARM_HYP/ArchFinalise_AI.thy b/proof/invariant-abstract/ARM_HYP/ArchFinalise_AI.thy index 42b3501850..44806f44df 100644 --- a/proof/invariant-abstract/ARM_HYP/ArchFinalise_AI.thy +++ b/proof/invariant-abstract/ARM_HYP/ArchFinalise_AI.thy @@ -1897,7 +1897,7 @@ lemma invs_valid_arch_capsI: "invs s \ valid_arch_caps s" by (simp add: invs_def valid_state_def) -context Arch begin arch_global_naming (*FIXME: arch-split*) +context Arch begin arch_global_naming lemma arch_finalise_case_no_lookup: "\pspace_aligned and valid_vspace_objs and valid_objs and diff --git a/proof/invariant-abstract/ARM_HYP/ArchKernelInit_AI.thy b/proof/invariant-abstract/ARM_HYP/ArchKernelInit_AI.thy index 375d2a832d..b6c45ff9b1 100644 --- a/proof/invariant-abstract/ARM_HYP/ArchKernelInit_AI.thy +++ b/proof/invariant-abstract/ARM_HYP/ArchKernelInit_AI.thy @@ -14,7 +14,7 @@ imports Arch_AI begin -context Arch begin arch_global_naming (*FIXME: arch-split*) +context Arch begin arch_global_naming text \ Showing that there is a state that satisfies the abstract invariants. diff --git a/proof/invariant-abstract/ARM_HYP/ArchRetype_AI.thy b/proof/invariant-abstract/ARM_HYP/ArchRetype_AI.thy index a5667769d8..f9df43d8e2 100644 --- a/proof/invariant-abstract/ARM_HYP/ArchRetype_AI.thy +++ b/proof/invariant-abstract/ARM_HYP/ArchRetype_AI.thy @@ -766,7 +766,7 @@ sublocale retype_region_proofs_gen?: retype_region_proofs_gen end -context Arch begin arch_global_naming (*FIXME: arch-split*) +context Arch begin arch_global_naming definition valid_vs_lookup2 :: "(vs_ref list \ word32) set \ word32 set \ (cslot_ptr \ cap) \ bool" diff --git a/proof/invariant-abstract/ARM_HYP/ArchVCPU_AI.thy b/proof/invariant-abstract/ARM_HYP/ArchVCPU_AI.thy index db3d7df469..023f273197 100644 --- a/proof/invariant-abstract/ARM_HYP/ArchVCPU_AI.thy +++ b/proof/invariant-abstract/ARM_HYP/ArchVCPU_AI.thy @@ -9,7 +9,7 @@ theory ArchVCPU_AI imports AInvs begin -context Arch begin arch_global_naming (*FIXME: arch-split*) +context Arch begin arch_global_naming definition active_cur_vcpu_of :: "'z state \ obj_ref option" where "active_cur_vcpu_of s \ case arm_current_vcpu (arch_state s) of Some (vr, True) \ Some vr diff --git a/proof/invariant-abstract/ARM_HYP/ArchVSpaceEntries_AI.thy b/proof/invariant-abstract/ARM_HYP/ArchVSpaceEntries_AI.thy index f0bb6dbf35..76704a98cc 100644 --- a/proof/invariant-abstract/ARM_HYP/ArchVSpaceEntries_AI.thy +++ b/proof/invariant-abstract/ARM_HYP/ArchVSpaceEntries_AI.thy @@ -8,7 +8,7 @@ theory ArchVSpaceEntries_AI imports VSpaceEntries_AI begin -context Arch begin arch_global_naming (*FIXME: arch-split*) +context Arch begin arch_global_naming lemma a_type_pdD: "a_type ko = AArch APageDirectory \ \pd. ko = ArchObj (PageDirectory pd)" diff --git a/proof/invariant-abstract/RISCV64/ArchFinalise_AI.thy b/proof/invariant-abstract/RISCV64/ArchFinalise_AI.thy index 6db79bd0a2..d9fe10ca35 100644 --- a/proof/invariant-abstract/RISCV64/ArchFinalise_AI.thy +++ b/proof/invariant-abstract/RISCV64/ArchFinalise_AI.thy @@ -1129,7 +1129,7 @@ lemma invs_valid_arch_capsI: "invs s \ valid_arch_caps s" by (simp add: invs_def valid_state_def) -context Arch begin arch_global_naming (*FIXME: arch-split*) +context Arch begin arch_global_naming lemma do_machine_op_reachable_pg_cap[wp]: "\\s. P (reachable_frame_cap cap s)\ diff --git a/proof/invariant-abstract/X64/ArchFinalise_AI.thy b/proof/invariant-abstract/X64/ArchFinalise_AI.thy index efe53a7ae2..dc101958c7 100644 --- a/proof/invariant-abstract/X64/ArchFinalise_AI.thy +++ b/proof/invariant-abstract/X64/ArchFinalise_AI.thy @@ -1172,11 +1172,12 @@ lemma invs_valid_arch_capsI: "invs s \ valid_arch_caps s" by (simp add: invs_def valid_state_def) -context Arch begin arch_global_naming (*FIXME: arch-split*) - +(* FIXME: move *) lemma all_Some_the_strg: "f b = None \ P (the (f b)) \ (\a. f b = Some a \ P a)" by auto +context Arch begin arch_global_naming + lemma vs_cap_ref_PageCap_Some_None[simp]: "(vs_cap_ref (ArchObjectCap (PageCap d p R typ sz (Some v))) = None) = False" by (case_tac sz; simp add: vs_cap_ref_simps split_def) diff --git a/proof/invariant-abstract/X64/ArchKernelInit_AI.thy b/proof/invariant-abstract/X64/ArchKernelInit_AI.thy index 0610edbd20..42bab0aa5b 100644 --- a/proof/invariant-abstract/X64/ArchKernelInit_AI.thy +++ b/proof/invariant-abstract/X64/ArchKernelInit_AI.thy @@ -14,7 +14,7 @@ imports Arch_AI begin -context Arch begin arch_global_naming (*FIXME: arch-split*) +context Arch begin arch_global_naming text \ Showing that there is a state that satisfies the abstract invariants. diff --git a/proof/invariant-abstract/X64/ArchRetype_AI.thy b/proof/invariant-abstract/X64/ArchRetype_AI.thy index 93cd69b827..da95a99243 100644 --- a/proof/invariant-abstract/X64/ArchRetype_AI.thy +++ b/proof/invariant-abstract/X64/ArchRetype_AI.thy @@ -828,7 +828,7 @@ sublocale retype_region_proofs_gen?: retype_region_proofs_gen end -context Arch begin arch_global_naming (*FIXME: arch-split*) +context Arch begin arch_global_naming definition valid_vs_lookup2 :: "(vs_ref list \ machine_word) set \ (cslot_ptr \ cap) \ bool" diff --git a/proof/invariant-abstract/X64/ArchVSpaceEntries_AI.thy b/proof/invariant-abstract/X64/ArchVSpaceEntries_AI.thy index f6b59dbeed..45185e8a02 100644 --- a/proof/invariant-abstract/X64/ArchVSpaceEntries_AI.thy +++ b/proof/invariant-abstract/X64/ArchVSpaceEntries_AI.thy @@ -8,7 +8,7 @@ theory ArchVSpaceEntries_AI imports VSpaceEntries_AI begin -context Arch begin arch_global_naming (*FIXME: arch-split*) +context Arch begin arch_global_naming lemma a_type_pml4D: "a_type ko = AArch APageMapL4 \ \pm. ko = ArchObj (PageMapL4 pm)"