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 <[email protected]>
seL4 · Aug 2, 2024 · 561e031 · 561e031
1 parent 86c7ce9
commit 561e031
Show file tree

Hide file tree

Showing 15 changed files with 17 additions and 16 deletions.
diff --git 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 \<Longrightarrow> 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]:
   "\<lbrace>\<lambda>s. P (reachable_frame_cap cap s)\<rbrace>

diff --git 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 \<Longrightarrow> 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:
   "\<lbrace>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
@@ -14,7 +14,7 @@ imports
   Arch_AI
 begin
 
-context Arch begin arch_global_naming (*FIXME: arch-split*)
+context Arch begin arch_global_naming
 
 text \<open>
   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
@@ -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 \<times> word32) set \<Rightarrow> (cslot_ptr \<rightharpoonup> cap) \<Rightarrow> bool"

diff --git 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 \<Longrightarrow> \<exists>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
@@ -1897,7 +1897,7 @@ lemma invs_valid_arch_capsI:
   "invs s \<Longrightarrow> 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:
   "\<lbrace>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
@@ -14,7 +14,7 @@ imports
   Arch_AI
 begin
 
-context Arch begin arch_global_naming (*FIXME: arch-split*)
+context Arch begin arch_global_naming
 
 text \<open>
   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
@@ -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 \<times> word32) set \<Rightarrow> word32 set \<Rightarrow> (cslot_ptr \<rightharpoonup> cap) \<Rightarrow> bool"

diff --git 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 \<Rightarrow> obj_ref option" where
   "active_cur_vcpu_of s \<equiv> case arm_current_vcpu (arch_state s) of Some (vr, True) \<Rightarrow> Some vr

diff --git 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 \<Longrightarrow> \<exists>pd. ko = ArchObj (PageDirectory pd)"

diff --git 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 \<Longrightarrow> 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]:
   "\<lbrace>\<lambda>s. P (reachable_frame_cap cap s)\<rbrace>

diff --git 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 \<Longrightarrow> 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 \<or> P (the (f b)) \<longrightarrow> (\<forall>a. f b = Some a \<longrightarrow> 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
@@ -14,7 +14,7 @@ imports
   Arch_AI
 begin
 
-context Arch begin arch_global_naming (*FIXME: arch-split*)
+context Arch begin arch_global_naming
 
 text \<open>
   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
@@ -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 \<times> machine_word) set \<Rightarrow> (cslot_ptr \<rightharpoonup> cap) \<Rightarrow> bool"

diff --git 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 \<Longrightarrow> \<exists>pm. ko = ArchObj (PageMapL4 pm)"