rename assert squash

Signed-off-by: Michael McInerney <[email protected]>
seL4 · Apr 10, 2024 · 6a8a243 · 6a8a243
1 parent 09833df
commit 6a8a243
Show file tree

Hide file tree

Showing 7 changed files with 55 additions and 55 deletions.
diff --git a/proof/refine/AARCH64/Detype_R.thy b/proof/refine/AARCH64/Detype_R.thy
@@ -100,8 +100,8 @@ defs deletionIsSafe_def:
        t \<notin> mask_range ptr bits) \<and>
        (\<forall>ko. ksPSpace s p = Some (KOArch ko) \<and> p \<in> mask_range ptr bits \<longrightarrow> 6 \<le> bits)"
 
-defs deletionIsSafe2_def:
-  "deletionIsSafe2 \<equiv> \<lambda>ptr bits s. \<forall>p. ko_wp_at' live' p s \<longrightarrow> p \<notin> mask_range ptr bits"
+defs deletionIsSafe_delete_locale_def:
+  "deletionIsSafe_delete_locale \<equiv> \<lambda>ptr bits s. \<forall>p. ko_wp_at' live' p s \<longrightarrow> p \<notin> mask_range ptr bits"
 
 defs ksASIDMapSafe_def:
   "ksASIDMapSafe \<equiv> \<lambda>s. True"
@@ -126,7 +126,7 @@ lemma deleteObjects_def2:
   "is_aligned ptr bits \<Longrightarrow>
    deleteObjects ptr bits = do
      stateAssert (deletionIsSafe ptr bits) [];
-     stateAssert (deletionIsSafe2 ptr bits) [];
+     stateAssert (deletionIsSafe_delete_locale ptr bits) [];
      doMachineOp (freeMemory ptr bits);
      stateAssert (\<lambda>s. \<not> cNodePartialOverlap (gsCNodes s) (\<lambda>x. x \<in> mask_range ptr bits)) [];
      stateAssert (\<lambda>s. \<not> pTablePartialOverlap (gsPTTypes (ksArchState s)) (\<lambda>x. x \<in> mask_range ptr bits)) [];
@@ -172,7 +172,7 @@ lemma deleteObjects_def3:
    do
      assert (is_aligned ptr bits);
      stateAssert (deletionIsSafe ptr bits) [];
-     stateAssert (deletionIsSafe2 ptr bits) [];
+     stateAssert (deletionIsSafe_delete_locale ptr bits) [];
      doMachineOp (freeMemory ptr bits);
      stateAssert (\<lambda>s. \<not> cNodePartialOverlap (gsCNodes s) (\<lambda>x. x \<in> mask_range ptr bits)) [];
      stateAssert (\<lambda>s. \<not> pTablePartialOverlap (gsPTTypes (ksArchState s)) (\<lambda>x. x \<in> mask_range ptr bits)) [];
@@ -813,9 +813,9 @@ lemma live_notRange:
   apply (erule ex_nonz_cap_notRange)
   done
 
-lemma deletionIsSafe2_holds:
-  "deletionIsSafe2 base bits s'"
-  by (fastforce dest: live_notRange simp: deletionIsSafe2_def)
+lemma deletionIsSafe_delete_locale_holds:
+  "deletionIsSafe_delete_locale base bits s'"
+  by (fastforce dest: live_notRange simp: deletionIsSafe_delete_locale_def)
 
 lemma refs_notRange:
   "(x, tp) \<in> state_refs_of' s' y \<Longrightarrow> y \<notin> base_bits"
@@ -957,8 +957,8 @@ lemma corres_return_bind2: (* FIXME AARCH64: move to Corres_UL *)
 
 crunches doMachineOp
   for gsCNodes[wp]: "\<lambda>s. P (gsCNodes s)"
-  and deletionIsSafe2[wp]: "deletionIsSafe2 base magnitude"
-  (simp: deletionIsSafe2_def)
+  and deletionIsSafe_delete_locale[wp]: "deletionIsSafe_delete_locale base magnitude"
+  (simp: deletionIsSafe_delete_locale_def)
 
 lemma deleteObjects_corres:
   "is_aligned base magnitude \<Longrightarrow> magnitude \<ge> 3 \<Longrightarrow>
@@ -985,7 +985,7 @@ lemma deleteObjects_corres:
           simp_all add: detype_locale'_def detype_locale_def p_assoc_help invs_valid_pspace)[1]
    apply (simp add:valid_cap_simps)
   apply (rule corres_stateAssert_add_assertion[rotated])
-   apply (rule_tac ptr=ptr and idx=idx and d=d in delete_locale.deletionIsSafe2_holds)
+   apply (rule_tac ptr=ptr and idx=idx and d=d in delete_locale.deletionIsSafe_delete_locale_holds)
    apply (clarsimp simp: delete_locale_def)
    apply (intro conjI)
     apply (fastforce simp: sch_act_simple_def state_relation_def schact_is_rct_def)

diff --git a/proof/refine/ARM/Detype_R.thy b/proof/refine/ARM/Detype_R.thy
@@ -100,8 +100,8 @@ defs deletionIsSafe_def:
        (\<forall>ko. ksPSpace s p = Some (KOArch ko) \<and> p \<in> {ptr .. ptr + 2 ^ bits - 1}
         \<longrightarrow> 6 \<le> bits)"
 
-defs deletionIsSafe2_def:
-  "deletionIsSafe2 \<equiv> \<lambda>ptr bits s. \<forall>p. ko_wp_at' live' p s \<longrightarrow> p \<notin> {ptr .. ptr + 2 ^ bits - 1}"
+defs deletionIsSafe_delete_locale_def:
+  "deletionIsSafe_delete_locale \<equiv> \<lambda>ptr bits s. \<forall>p. ko_wp_at' live' p s \<longrightarrow> p \<notin> {ptr .. ptr + 2 ^ bits - 1}"
 
 defs ksASIDMapSafe_def:
   "ksASIDMapSafe \<equiv> \<lambda>s. \<forall>asid hw_asid pd.
@@ -119,7 +119,7 @@ lemma deleteObjects_def2:
   "is_aligned ptr bits \<Longrightarrow>
    deleteObjects ptr bits = do
      stateAssert (deletionIsSafe ptr bits) [];
-     stateAssert (deletionIsSafe2 ptr bits) [];
+     stateAssert (deletionIsSafe_delete_locale ptr bits) [];
      doMachineOp (freeMemory ptr bits);
      stateAssert (\<lambda>s. \<not> cNodePartialOverlap (gsCNodes s) (\<lambda>x. x \<in> {ptr .. ptr + 2 ^ bits - 1})) [];
      modify (\<lambda>s. s \<lparr> ksPSpace := \<lambda>x. if x \<in> {ptr .. ptr + 2 ^ bits - 1}
@@ -154,7 +154,7 @@ lemma deleteObjects_def3:
    do
      assert (is_aligned ptr bits);
      stateAssert (deletionIsSafe ptr bits) [];
-     stateAssert (deletionIsSafe2 ptr bits) [];
+     stateAssert (deletionIsSafe_delete_locale ptr bits) [];
      doMachineOp (freeMemory ptr bits);
      stateAssert (\<lambda>s. \<not> cNodePartialOverlap (gsCNodes s) (\<lambda>x. x \<in> {ptr .. ptr + 2 ^ bits - 1})) [];
      modify (\<lambda>s. s \<lparr> ksPSpace := \<lambda>x. if x \<in> {ptr .. ptr + 2 ^ bits - 1}
@@ -781,9 +781,9 @@ lemma live_notRange:
   apply (erule ex_nonz_cap_notRange)
   done
 
-lemma deletionIsSafe2_holds:
-  "deletionIsSafe2 base bits s'"
-  by (fastforce dest: live_notRange simp: deletionIsSafe2_def field_simps)
+lemma deletionIsSafe_delete_locale_holds:
+  "deletionIsSafe_delete_locale base bits s'"
+  by (fastforce dest: live_notRange simp: deletionIsSafe_delete_locale_def field_simps)
 
 lemma refs_notRange:
   "(x, tp) \<in> state_refs_of' s' y \<Longrightarrow> y \<notin> base_bits"
@@ -885,8 +885,8 @@ lemma sym_refs_hyp_refs_triv[simp]: "sym_refs (state_hyp_refs_of s)"
   done
 
 crunches doMachineOp
-  for deletionIsSafe2[wp]: "deletionIsSafe2 base magnitude"
-  (simp: deletionIsSafe2_def)
+  for deletionIsSafe_delete_locale[wp]: "deletionIsSafe_delete_locale base magnitude"
+  (simp: deletionIsSafe_delete_locale_def)
 
 lemma deleteObjects_corres:
   "is_aligned base magnitude \<Longrightarrow> magnitude \<ge> 2 \<Longrightarrow>
@@ -914,7 +914,7 @@ lemma deleteObjects_corres:
      detype_locale_def p_assoc_help invs_valid_pspace)[1]
    apply (simp add:valid_cap_simps)
   apply (rule corres_stateAssert_add_assertion[rotated])
-   apply (rule_tac ptr=ptr and idx=idx and d=d in delete_locale.deletionIsSafe2_holds)
+   apply (rule_tac ptr=ptr and idx=idx and d=d in delete_locale.deletionIsSafe_delete_locale_holds)
    apply (clarsimp simp: delete_locale_def)
    apply (intro conjI)
     apply (fastforce simp: sch_act_simple_def state_relation_def schact_is_rct_def)

diff --git a/proof/refine/ARM_HYP/Detype_R.thy b/proof/refine/ARM_HYP/Detype_R.thy
@@ -100,8 +100,8 @@ defs deletionIsSafe_def:
        (\<forall>ko. ksPSpace s p = Some (KOArch ko) \<and> p \<in> {ptr .. ptr + 2 ^ bits - 1}
         \<longrightarrow> 7 \<le> bits)"
 
-defs deletionIsSafe2_def:
-  "deletionIsSafe2 \<equiv> \<lambda>ptr bits s. \<forall>p. ko_wp_at' live' p s \<longrightarrow> p \<notin> {ptr .. ptr + 2 ^ bits - 1}"
+defs deletionIsSafe_delete_locale_def:
+  "deletionIsSafe_delete_locale \<equiv> \<lambda>ptr bits s. \<forall>p. ko_wp_at' live' p s \<longrightarrow> p \<notin> {ptr .. ptr + 2 ^ bits - 1}"
 
 defs ksASIDMapSafe_def:
   "ksASIDMapSafe \<equiv> \<lambda>s. \<forall>asid hw_asid pd.
@@ -119,7 +119,7 @@ lemma deleteObjects_def2:
   "is_aligned ptr bits \<Longrightarrow>
    deleteObjects ptr bits = do
      stateAssert (deletionIsSafe ptr bits) [];
-     stateAssert (deletionIsSafe2 ptr bits) [];
+     stateAssert (deletionIsSafe_delete_locale ptr bits) [];
      doMachineOp (freeMemory ptr bits);
      stateAssert (\<lambda>s. \<not> cNodePartialOverlap (gsCNodes s) (\<lambda>x. x \<in> {ptr .. ptr + 2 ^ bits - 1})) [];
      modify (\<lambda>s. s \<lparr> ksPSpace := \<lambda>x. if x \<in> {ptr .. ptr + 2 ^ bits - 1}
@@ -154,7 +154,7 @@ lemma deleteObjects_def3:
    do
      assert (is_aligned ptr bits);
      stateAssert (deletionIsSafe ptr bits) [];
-     stateAssert (deletionIsSafe2 ptr bits) [];
+     stateAssert (deletionIsSafe_delete_locale ptr bits) [];
      doMachineOp (freeMemory ptr bits);
      stateAssert (\<lambda>s. \<not> cNodePartialOverlap (gsCNodes s) (\<lambda>x. x \<in> {ptr .. ptr + 2 ^ bits - 1})) [];
      modify (\<lambda>s. s \<lparr> ksPSpace := \<lambda>x. if x \<in> {ptr .. ptr + 2 ^ bits - 1}
@@ -805,9 +805,9 @@ lemma live_notRange:
   apply (erule ex_nonz_cap_notRange)
   done
 
-lemma deletionIsSafe2_holds:
-  "deletionIsSafe2 base bits s'"
-  by (fastforce dest: live_notRange simp: deletionIsSafe2_def field_simps)
+lemma deletionIsSafe_delete_locale_holds:
+  "deletionIsSafe_delete_locale base bits s'"
+  by (fastforce dest: live_notRange simp: deletionIsSafe_delete_locale_def field_simps)
 
 lemma refs_notRange:
   "(x, tp) \<in> state_refs_of' s' y \<Longrightarrow> y \<notin> base_bits"
@@ -930,8 +930,8 @@ lemma cNodeNoPartialOverlap:
 declare wrap_ext_det_ext_ext_def[simp]
 
 crunches doMachineOp
-  for deletionIsSafe2[wp]: "deletionIsSafe2 base magnitude"
-  (simp: deletionIsSafe2_def)
+  for deletionIsSafe_delete_locale[wp]: "deletionIsSafe_delete_locale base magnitude"
+  (simp: deletionIsSafe_delete_locale_def)
 
 lemma deleteObjects_corres:
   "is_aligned base magnitude \<Longrightarrow> magnitude \<ge> 2 \<Longrightarrow>
@@ -959,7 +959,7 @@ lemma deleteObjects_corres:
      detype_locale_def p_assoc_help invs_valid_pspace)[1]
    apply (simp add:valid_cap_simps)
   apply (rule corres_stateAssert_add_assertion[rotated])
-   apply (rule_tac ptr=ptr and idx=idx and d=d in delete_locale.deletionIsSafe2_holds)
+   apply (rule_tac ptr=ptr and idx=idx and d=d in delete_locale.deletionIsSafe_delete_locale_holds)
    apply (clarsimp simp: delete_locale_def)
    apply (intro conjI)
     apply (fastforce simp: sch_act_simple_def state_relation_def schact_is_rct_def)

diff --git a/proof/refine/RISCV64/Detype_R.thy b/proof/refine/RISCV64/Detype_R.thy
@@ -99,8 +99,8 @@ defs deletionIsSafe_def:
        t \<notin> mask_range ptr bits) \<and>
        (\<forall>ko. ksPSpace s p = Some (KOArch ko) \<and> p \<in> mask_range ptr bits \<longrightarrow> 6 \<le> bits)"
 
-defs deletionIsSafe2_def:
-  "deletionIsSafe2 \<equiv> \<lambda>ptr bits s. \<forall>p. ko_wp_at' live' p s \<longrightarrow> p \<notin> mask_range ptr bits"
+defs deletionIsSafe_delete_locale_def:
+  "deletionIsSafe_delete_locale \<equiv> \<lambda>ptr bits s. \<forall>p. ko_wp_at' live' p s \<longrightarrow> p \<notin> mask_range ptr bits"
 
 defs ksASIDMapSafe_def:
   "ksASIDMapSafe \<equiv> \<lambda>s. True"
@@ -118,7 +118,7 @@ lemma deleteObjects_def2:
   "is_aligned ptr bits \<Longrightarrow>
    deleteObjects ptr bits = do
      stateAssert (deletionIsSafe ptr bits) [];
-     stateAssert (deletionIsSafe2 ptr bits) [];
+     stateAssert (deletionIsSafe_delete_locale ptr bits) [];
      doMachineOp (freeMemory ptr bits);
      stateAssert (\<lambda>s. \<not> cNodePartialOverlap (gsCNodes s) (\<lambda>x. x \<in> mask_range ptr bits)) [];
      modify (\<lambda>s. s \<lparr> ksPSpace := \<lambda>x. if x \<in> mask_range ptr bits
@@ -153,7 +153,7 @@ lemma deleteObjects_def3:
    do
      assert (is_aligned ptr bits);
      stateAssert (deletionIsSafe ptr bits) [];
-     stateAssert (deletionIsSafe2 ptr bits) [];
+     stateAssert (deletionIsSafe_delete_locale ptr bits) [];
      doMachineOp (freeMemory ptr bits);
      stateAssert (\<lambda>s. \<not> cNodePartialOverlap (gsCNodes s) (\<lambda>x. x \<in> mask_range ptr bits)) [];
      modify (\<lambda>s. s \<lparr> ksPSpace := \<lambda>x. if x \<in> mask_range ptr bits
@@ -759,9 +759,9 @@ lemma live_notRange:
   apply (erule ex_nonz_cap_notRange)
   done
 
-lemma deletionIsSafe2_holds:
-  "deletionIsSafe2 base bits s'"
-  by (fastforce dest: live_notRange simp: deletionIsSafe2_def)
+lemma deletionIsSafe_delete_locale_holds:
+  "deletionIsSafe_delete_locale base bits s'"
+  by (fastforce dest: live_notRange simp: deletionIsSafe_delete_locale_def)
 
 lemma refs_notRange:
   "(x, tp) \<in> state_refs_of' s' y \<Longrightarrow> y \<notin> base_bits"
@@ -833,8 +833,8 @@ lemma sym_refs_hyp_refs_triv[simp]: "sym_refs (state_hyp_refs_of s')"
   by (case_tac "kheap s' x"; simp)
 
 crunches doMachineOp
-  for deletionIsSafe2[wp]: "deletionIsSafe2 base magnitude"
-  (simp: deletionIsSafe2_def)
+  for deletionIsSafe_delete_locale[wp]: "deletionIsSafe_delete_locale base magnitude"
+  (simp: deletionIsSafe_delete_locale_def)
 
 lemma deleteObjects_corres:
   "is_aligned base magnitude \<Longrightarrow> magnitude \<ge> 3 \<Longrightarrow>
@@ -862,7 +862,7 @@ lemma deleteObjects_corres:
      detype_locale_def p_assoc_help invs_valid_pspace)[1]
    apply (simp add:valid_cap_simps)
   apply (rule corres_stateAssert_add_assertion[rotated])
-   apply (rule_tac ptr=ptr and idx=idx and d=d in delete_locale.deletionIsSafe2_holds)
+   apply (rule_tac ptr=ptr and idx=idx and d=d in delete_locale.deletionIsSafe_delete_locale_holds)
    apply (clarsimp simp: delete_locale_def)
    apply (intro conjI)
     apply (fastforce simp: sch_act_simple_def state_relation_def schact_is_rct_def)
@@ -881,7 +881,7 @@ lemma deleteObjects_corres:
                            untyped_children_in_mdb s \<and> if_unsafe_then_cap s \<and>
                            valid_global_refs s"
               and Q'="\<lambda>_ s. s \<turnstile>' capability.UntypedCap d base magnitude idx \<and>
-                            valid_pspace' s \<and> deletionIsSafe2 base magnitude s"
+                            valid_pspace' s \<and> deletionIsSafe_delete_locale base magnitude s"
                in corres_underlying_split)
      apply (rule corres_bind_return)
      apply (rule corres_guard_imp[where r=dc])

diff --git a/proof/refine/X64/Detype_R.thy b/proof/refine/X64/Detype_R.thy
@@ -100,8 +100,8 @@ defs deletionIsSafe_def:
        (\<forall>ko. ksPSpace s p = Some (KOArch ko) \<and> p \<in> {ptr .. ptr + 2 ^ bits - 1}
         \<longrightarrow> 6 \<le> bits)"
 
-defs deletionIsSafe2_def:
-  "deletionIsSafe2 \<equiv> \<lambda>ptr bits s. \<forall>p. ko_wp_at' live' p s \<longrightarrow> p \<notin> {ptr .. ptr + 2 ^ bits - 1}"
+defs deletionIsSafe_delete_locale_def:
+  "deletionIsSafe_delete_locale \<equiv> \<lambda>ptr bits s. \<forall>p. ko_wp_at' live' p s \<longrightarrow> p \<notin> {ptr .. ptr + 2 ^ bits - 1}"
 
 defs ksASIDMapSafe_def:
   "ksASIDMapSafe \<equiv> \<lambda>s. True"
@@ -118,7 +118,7 @@ lemma deleteObjects_def2:
   "is_aligned ptr bits \<Longrightarrow>
    deleteObjects ptr bits = do
      stateAssert (deletionIsSafe ptr bits) [];
-     stateAssert (deletionIsSafe2 ptr bits) [];
+     stateAssert (deletionIsSafe_delete_locale ptr bits) [];
      doMachineOp (freeMemory ptr bits);
      stateAssert (\<lambda>s. \<not> cNodePartialOverlap (gsCNodes s) (\<lambda>x. x \<in> {ptr .. ptr + 2 ^ bits - 1})) [];
      modify (\<lambda>s. s \<lparr> ksPSpace := \<lambda>x. if x \<in> {ptr .. ptr + 2 ^ bits - 1}
@@ -153,7 +153,7 @@ lemma deleteObjects_def3:
    do
      assert (is_aligned ptr bits);
      stateAssert (deletionIsSafe ptr bits) [];
-     stateAssert (deletionIsSafe2 ptr bits) [];
+     stateAssert (deletionIsSafe_delete_locale ptr bits) [];
      doMachineOp (freeMemory ptr bits);
      stateAssert (\<lambda>s. \<not> cNodePartialOverlap (gsCNodes s) (\<lambda>x. x \<in> {ptr .. ptr + 2 ^ bits - 1})) [];
      modify (\<lambda>s. s \<lparr> ksPSpace := \<lambda>x. if x \<in> {ptr .. ptr + 2 ^ bits - 1}
@@ -827,9 +827,9 @@ lemma live_notRange:
   apply (erule ex_nonz_cap_notRange)
   done
 
-lemma deletionIsSafe2_holds:
-  "deletionIsSafe2 base bits s'"
-  by (fastforce dest: live_notRange simp: deletionIsSafe2_def field_simps)
+lemma deletionIsSafe_delete_locale_holds:
+  "deletionIsSafe_delete_locale base bits s'"
+  by (fastforce dest: live_notRange simp: deletionIsSafe_delete_locale_def field_simps)
 
 lemma refs_notRange:
   "(x, tp) \<in> state_refs_of' s' y \<Longrightarrow> y \<notin> base_bits"
@@ -901,8 +901,8 @@ lemma sym_refs_hyp_refs_triv[simp]: "sym_refs (state_hyp_refs_of s)"
   by (case_tac "kheap s x"; simp)
 
 crunches doMachineOp
-  for deletionIsSafe2[wp]: "deletionIsSafe2 base magnitude"
-  (simp: deletionIsSafe2_def)
+  for deletionIsSafe_delete_locale[wp]: "deletionIsSafe_delete_locale base magnitude"
+  (simp: deletionIsSafe_delete_locale_def)
 
 lemma deleteObjects_corres:
   "is_aligned base magnitude \<Longrightarrow> magnitude \<ge> 3 \<Longrightarrow>
@@ -930,7 +930,7 @@ lemma deleteObjects_corres:
      detype_locale_def p_assoc_help invs_valid_pspace)[1]
    apply (simp add:valid_cap_simps)
   apply (rule corres_stateAssert_add_assertion[rotated])
-   apply (rule_tac ptr=ptr and idx=idx and d=d in delete_locale.deletionIsSafe2_holds)
+   apply (rule_tac ptr=ptr and idx=idx and d=d in delete_locale.deletionIsSafe_delete_locale_holds)
    apply (clarsimp simp: delete_locale_def)
    apply (intro conjI)
     apply (fastforce simp: sch_act_simple_def state_relation_def schact_is_rct_def)

diff --git a/spec/design/skel/PSpaceFuns_H.thy b/spec/design/skel/PSpaceFuns_H.thy
@@ -36,6 +36,6 @@ where "deleteRange m ptr bits \<equiv>
 consts
 lookupAround2 :: "('k :: {linorder,finite}) \<Rightarrow> ( 'k , 'a ) DataMap.map \<Rightarrow> (('k * 'a) option * 'k option)"
 
-#INCLUDE_HASKELL SEL4/Model/PSpace.lhs bodies_only Data.Map=DataMap NOT PSpace ptrBits ptrBitsForSize lookupAround maybeToMonad typeError alignError alignCheck sizeCheck objBits deletionIsSafe deletionIsSafe2 cNodePartialOverlap pointerInUserData ksASIDMapSafe deleteRange
+#INCLUDE_HASKELL SEL4/Model/PSpace.lhs bodies_only Data.Map=DataMap NOT PSpace ptrBits ptrBitsForSize lookupAround maybeToMonad typeError alignError alignCheck sizeCheck objBits deletionIsSafe deletionIsSafe_delete_locale cNodePartialOverlap pointerInUserData ksASIDMapSafe deleteRange
 
 end
diff --git a/spec/haskell/src/SEL4/Model/PSpace.lhs b/spec/haskell/src/SEL4/Model/PSpace.lhs
@@ -244,7 +244,7 @@ No type checks are performed when deleting objects; "deleteObjects" simply delet
 >             alignError bits
 >         stateAssert (deletionIsSafe ptr bits)
 >             "Object deletion would leave dangling pointers"
->         stateAssert (deletionIsSafe2 ptr bits)
+>         stateAssert (deletionIsSafe_delete_locale ptr bits)
 >             "Object deletion would leave dangling pointers"
 >         doMachineOp $ freeMemory (PPtr (fromPPtr ptr)) bits
 >         ps <- gets ksPSpace
@@ -269,8 +269,8 @@ In "deleteObjects" above, we make two assertions, which, when taken together, sa
 > deletionIsSafe :: PPtr a -> Int -> KernelState -> Bool
 > deletionIsSafe _ _ _ = True
 
-> deletionIsSafe2 :: PPtr a -> Int -> KernelState -> Bool
-> deletionIsSafe2 _ _ _ = True
+> deletionIsSafe_delete_locale :: PPtr a -> Int -> KernelState -> Bool
+> deletionIsSafe_delete_locale _ _ _ = True
 
 We also assert that the ghost CNodes are all either completely deleted or unchanged; no CNode should be partially in the range and partially deleted. Again, this assertion requires logical quantifiers, and is inserted in translation.