From c3c32e719a8581fd93b4aefaaed51494288bb291 Mon Sep 17 00:00:00 2001 From: Michael McInerney Date: Thu, 28 Mar 2024 11:32:02 +1030 Subject: [PATCH] fix AARCH64 squash into haskell_assert_inv commit Signed-off-by: Michael McInerney --- proof/crefine/AARCH64/Fastpath_C.thy | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/proof/crefine/AARCH64/Fastpath_C.thy b/proof/crefine/AARCH64/Fastpath_C.thy index e04d077d17..801f974a2e 100644 --- a/proof/crefine/AARCH64/Fastpath_C.thy +++ b/proof/crefine/AARCH64/Fastpath_C.thy @@ -585,7 +585,7 @@ lemma getASIDPoolEntry_wp: getASIDPoolEntry asid \\rv s. P rv s \" 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)