From 5dbb844007e7f5a1f36e48820cc70eb9ba687187 Mon Sep 17 00:00:00 2001
From: Corey Lewis <corey.lewis@proofcraft.systems>
Date: Tue, 9 Apr 2024 17:20:41 +1000
Subject: [PATCH] squash: PR suggestions

Signed-off-by: Corey Lewis <corey.lewis@proofcraft.systems>
---
 proof/infoflow/Ipc_IF.thy         |  2 ++
 proof/refine/ARM/VSpace_R.thy     | 16 +++-------------
 proof/refine/ARM_HYP/VSpace_R.thy | 16 +++-------------
 proof/refine/X64/VSpace_R.thy     | 16 +++-------------
 4 files changed, 11 insertions(+), 39 deletions(-)

diff --git a/proof/infoflow/Ipc_IF.thy b/proof/infoflow/Ipc_IF.thy
index 096991da36..aa0ca12419 100644
--- a/proof/infoflow/Ipc_IF.thy
+++ b/proof/infoflow/Ipc_IF.thy
@@ -601,6 +601,8 @@ lemma send_signal_reads_respects:
                         set_thread_state_runnable_equiv_but_for_labels get_simple_ko_wp
                         gts_wp update_waiting_ntfn_equiv_but_for_labels
                         blocked_cancel_ipc_nosts_equiv_but_for_labels
+            \<comment> \<open>FIXME: The following line is working around the fact that wp (once) doesn't invoke
+                      wp_pre. If that is changed then it could be removed.\<close>
             | wp_pre0
             | wpc
             | wps)+
diff --git a/proof/refine/ARM/VSpace_R.thy b/proof/refine/ARM/VSpace_R.thy
index 585321f238..a89cef829b 100644
--- a/proof/refine/ARM/VSpace_R.thy
+++ b/proof/refine/ARM/VSpace_R.thy
@@ -881,19 +881,9 @@ lemma deleteASID_corres:
        apply (simp add: vs_refs_def)
        apply (rule image_eqI[rotated], erule graph_ofI)
        apply (simp add: mask_asid_low_bits_ucast_ucast)
-      apply wp
-      apply (simp add: o_def)
-      \<comment> \<open>FIXME: This proof weakens the schematic precondition so that an extra variable can be used,
-                and then uses `(clarsimp, assumption)` to resolve the schematic.
-                An alternative would be to use @{thm Some_to_the} to rewrite the conclusion, so that
-                the precondition does not need to depend on that variable.
-                Both approaches feel fragile.\<close>
-      apply (rule hoare_pre)
-       apply (wp getASID_wp)
-      apply clarsimp
-      apply assumption
-     apply wp+
-   apply clarsimp
+      \<comment> \<open>rewrite assumption so that the goal can refer to the C variable instead of the abstract's.\<close>
+      apply (drule Some_to_the)
+      apply (wpsimp wp: getASID_wp)+
    apply (clarsimp simp: valid_arch_state_def valid_asid_table_def
                   dest!: invs_arch_state)
    apply blast
diff --git a/proof/refine/ARM_HYP/VSpace_R.thy b/proof/refine/ARM_HYP/VSpace_R.thy
index 37aa69a6dd..b067dc1d6f 100644
--- a/proof/refine/ARM_HYP/VSpace_R.thy
+++ b/proof/refine/ARM_HYP/VSpace_R.thy
@@ -1424,19 +1424,9 @@ lemma deleteASID_corres:
        apply (simp add: vs_refs_def)
        apply (rule image_eqI[rotated], erule graph_ofI)
        apply (simp add: mask_asid_low_bits_ucast_ucast)
-      apply wp
-      apply (simp add: o_def)
-      \<comment> \<open>FIXME: This proof weakens the schematic precondition so that an extra variable can be used,
-                and then uses `(clarsimp, assumption)` to resolve the schematic.
-                An alternative would be to use @{thm Some_to_the} to rewrite the conclusion, so that
-                the precondition does not need to depend on that variable.
-                Both approaches feel fragile.\<close>
-      apply (rule hoare_pre)
-       apply (wp getASID_wp)
-      apply clarsimp
-      apply assumption
-     apply wp+
-   apply clarsimp
+      \<comment> \<open>rewrite assumption so that the goal can refer to the C variable instead of the abstract's.\<close>
+      apply (drule Some_to_the)
+      apply (wpsimp wp: getASID_wp)+
    apply (clarsimp simp: valid_arch_state_def valid_asid_table_def
                   dest!: invs_arch_state)
    apply blast
diff --git a/proof/refine/X64/VSpace_R.thy b/proof/refine/X64/VSpace_R.thy
index 6109c0a9e7..51627c6037 100644
--- a/proof/refine/X64/VSpace_R.thy
+++ b/proof/refine/X64/VSpace_R.thy
@@ -347,19 +347,9 @@ lemma deleteASID_corres [corres]:
        apply (simp add: vs_refs_def)
        apply (rule image_eqI[rotated], erule graph_ofI)
        apply (simp add: mask_asid_low_bits_ucast_ucast)
-      apply wp
-      apply (simp add: o_def)
-      \<comment> \<open>FIXME: This proof weakens the schematic precondition so that an extra variable can be used,
-                and then uses `(clarsimp, assumption)` to resolve the schematic.
-                An alternative would be to use @{thm Some_to_the} to rewrite the conclusion, so that
-                the precondition does not need to depend on that variable.
-                Both approaches feel fragile.\<close>
-      apply (rule hoare_pre)
-       apply (wp getASID_wp)
-      apply clarsimp
-      apply assumption
-     apply wp+
-   apply clarsimp
+      \<comment> \<open>rewrite assumption so that the goal can refer to the C variable instead of the abstract's.\<close>
+      apply (drule Some_to_the)
+      apply (wpsimp wp: getASID_wp)+
    apply (clarsimp simp: valid_arch_state_def valid_asid_table_def
                   dest!: invs_arch_state)
    apply blast