refine: update other architectures for ghost state change

Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>

proof/refine/ARM/Detype_R.thy

@@ -126,7 +126,7 @@ lemma deleteObjects_def2:
                                         then None else gsCNodes s x \<rparr>);
      stateAssert ksASIDMapSafe []
    od"
-  apply (simp add: deleteObjects_def is_aligned_mask[symmetric] unless_def)
+  apply (simp add: deleteObjects_def is_aligned_mask[symmetric] unless_def deleteGhost_def)
   apply (rule bind_eqI, rule ext)
   apply (rule bind_eqI, rule ext)
   apply (simp add: bind_assoc[symmetric])

proof/refine/ARM/Untyped_R.thy

@@ -4013,6 +4013,8 @@ lemma idx_le_new_offs:
 
 end
 
+context begin interpretation Arch . (*FIXME: arch_split*)
+
 lemma valid_sched_etcbs[elim!]: "valid_sched_2 queues ekh sa cdom kh ct it \<Longrightarrow> valid_etcbs_2 ekh kh"
   by (simp add: valid_sched_def)
 
@@ -4588,6 +4590,8 @@ lemma whenE_reset_resetUntypedCap_invs_etc:
 
 crunch ksCurDomain[wp]: updateFreeIndex "\<lambda>s. P (ksCurDomain s)"
 
+end
+
 lemma (in range_cover) funky_aligned:
   "is_aligned ((ptr && foo) + v * 2 ^ sbit) sbit"
   apply (rule aligned_add_aligned)

proof/refine/ARM_HYP/Detype_R.thy

@@ -126,7 +126,7 @@ lemma deleteObjects_def2:
                                         then None else gsCNodes s x \<rparr>);
      stateAssert ksASIDMapSafe []
    od"
-  apply (simp add: deleteObjects_def is_aligned_mask[symmetric] unless_def)
+  apply (simp add: deleteObjects_def is_aligned_mask[symmetric] unless_def deleteGhost_def)
   apply (rule bind_eqI, rule ext)
   apply (rule bind_eqI, rule ext)
   apply (simp add: bind_assoc[symmetric])

proof/refine/ARM_HYP/Untyped_R.thy

@@ -4062,6 +4062,8 @@ lemma idx_le_new_offs:
 
 end
 
+context begin interpretation Arch . (*FIXME: arch_split*)
+
 lemma valid_sched_etcbs[elim!]: "valid_sched_2 queues ekh sa cdom kh ct it \<Longrightarrow> valid_etcbs_2 ekh kh"
   by (simp add: valid_sched_def)
 
@@ -4637,6 +4639,8 @@ lemma whenE_reset_resetUntypedCap_invs_etc:
 
 crunch ksCurDomain[wp]: updateFreeIndex "\<lambda>s. P (ksCurDomain s)"
 
+end
+
 lemma (in range_cover) funky_aligned:
   "is_aligned ((ptr && foo) + v * 2 ^ sbit) sbit"
   apply (rule aligned_add_aligned)

proof/refine/RISCV64/Detype_R.thy

@@ -125,7 +125,7 @@ lemma deleteObjects_def2:
                                         then None else gsCNodes s x \<rparr>);
      stateAssert ksASIDMapSafe []
    od"
-  apply (simp add: deleteObjects_def is_aligned_mask[symmetric] unless_def)
+  apply (simp add: deleteObjects_def is_aligned_mask[symmetric] unless_def deleteGhost_def)
   apply (rule bind_eqI, rule ext)
   apply (rule bind_eqI, rule ext)
   apply (simp add: bind_assoc[symmetric])

proof/refine/RISCV64/Untyped_R.thy

@@ -4048,6 +4048,8 @@ lemma idx_le_new_offs:
 
 end
 
+context begin interpretation Arch . (*FIXME: arch_split*)
+
 lemma valid_sched_etcbs[elim!]: "valid_sched_2 queues ekh sa cdom kh ct it \<Longrightarrow> valid_etcbs_2 ekh kh"
   by (simp add: valid_sched_def)
 
@@ -4610,6 +4612,8 @@ lemma whenE_reset_resetUntypedCap_invs_etc:
 
 crunch ksCurDomain[wp]: updateFreeIndex "\<lambda>s. P (ksCurDomain s)"
 
+end
+
 lemma (in range_cover) funky_aligned:
   "is_aligned ((ptr && foo) + v * 2 ^ sbit) sbit"
   apply (rule aligned_add_aligned)

proof/refine/X64/Detype_R.thy

@@ -125,7 +125,7 @@ lemma deleteObjects_def2:
                                         then None else gsCNodes s x \<rparr>);
      stateAssert ksASIDMapSafe []
    od"
-  apply (simp add: deleteObjects_def is_aligned_mask[symmetric] unless_def)
+  apply (simp add: deleteObjects_def is_aligned_mask[symmetric] unless_def deleteGhost_def)
   apply (rule bind_eqI, rule ext)
   apply (rule bind_eqI, rule ext)
   apply (simp add: bind_assoc[symmetric])

proof/refine/X64/Untyped_R.thy

@@ -4145,6 +4145,8 @@ lemma idx_le_new_offs:
 
 end
 
+context begin interpretation Arch . (*FIXME: arch_split*)
+
 lemma valid_sched_etcbs[elim!]: "valid_sched_2 queues ekh sa cdom kh ct it \<Longrightarrow> valid_etcbs_2 ekh kh"
   by (simp add: valid_sched_def)
 
@@ -4718,6 +4720,8 @@ lemma whenE_reset_resetUntypedCap_invs_etc:
 
 crunch ksCurDomain[wp]: updateFreeIndex "\<lambda>s. P (ksCurDomain s)"
 
+end
+
 lemma (in range_cover) funky_aligned:
   "is_aligned ((ptr && foo) + v * 2 ^ sbit) sbit"
   apply (rule aligned_add_aligned)