fix AARCH64 squash into haskell_assert_inv commit

Signed-off-by: Michael McInerney <[email protected]>
seL4 · Apr 8, 2024 · c3c32e7 · c3c32e7
1 parent 8d21051
commit c3c32e7
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/proof/crefine/AARCH64/Fastpath_C.thy b/proof/crefine/AARCH64/Fastpath_C.thy
@@ -585,7 +585,7 @@ lemma getASIDPoolEntry_wp:
    getASIDPoolEntry asid
    \<lbrace>\<lambda>rv s. P rv s \<rbrace>"
   unfolding getASIDPoolEntry_def asid_has_entry_def getPoolPtr_def
-  apply (wpsimp wp: hoare_vcg_imp_lift' hoare_vcg_all_lift getASID_wp simp: comp_def)
+  apply (wpsimp wp: haskell_assert_inv getASID_wp)
   apply normalise_obj_at'
   apply (rename_tac pool)
   apply (case_tac "pool (asid AND mask asid_low_bits)"; simp)