squash: PR suggestions

Signed-off-by: Corey Lewis <[email protected]>
seL4 · Apr 9, 2024 · 5dbb844 · 5dbb844
1 parent 82b291c
commit 5dbb844
Show file tree

Hide file tree

Showing 4 changed files with 11 additions and 39 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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