From 3eee26769cc0f633c044b822c9b58ecf8d032c76 Mon Sep 17 00:00:00 2001 From: Rafal Kolanski Date: Thu, 14 Sep 2023 18:00:22 +1000 Subject: [PATCH] crefine: change misleading proof step in CSpace_RAB_C Trying to figure this out was very educational, since ccorres_abstract was used without intending to abstract a variable, the xf' and lambda name were both red herrings (in fact, this proof only worked if xf' was instantiated with an *irrelevant* C local var name), and the body was not transformed. Signed-off-by: Rafal Kolanski --- proof/crefine/ARM/CSpace_RAB_C.thy | 6 ++---- proof/crefine/ARM_HYP/CSpace_RAB_C.thy | 6 ++---- proof/crefine/RISCV64/CSpace_RAB_C.thy | 6 ++---- proof/crefine/X64/CSpace_RAB_C.thy | 6 ++---- 4 files changed, 8 insertions(+), 16 deletions(-) diff --git a/proof/crefine/ARM/CSpace_RAB_C.thy b/proof/crefine/ARM/CSpace_RAB_C.thy index eda10c9a31..84412cb532 100644 --- a/proof/crefine/ARM/CSpace_RAB_C.thy +++ b/proof/crefine/ARM/CSpace_RAB_C.thy @@ -168,10 +168,8 @@ next apply (simp add: cap_get_tag_isCap split del: if_split) apply (thin_tac "ret__unsigned = X" for X) apply (rule ccorres_split_throws [where P = "?P"]) - apply (rule_tac G' = "\w_rightsMask. ({s. nodeCap_' s = nodeCap} - \ {s. unat (n_bits_' s) = guard'})" - in ccorres_abstract [where xf' = w_rightsMask_']) - apply (rule ceqv_refl) + apply (rule_tac P'="{s. nodeCap_' s = nodeCap} \ {s. unat (n_bits_' s) = guard'}" + in ccorres_inst) apply (rule_tac r' = "?rvr" in ccorres_rel_imp [where xf' = rab_xf]) defer diff --git a/proof/crefine/ARM_HYP/CSpace_RAB_C.thy b/proof/crefine/ARM_HYP/CSpace_RAB_C.thy index 93c935fa86..4659236034 100644 --- a/proof/crefine/ARM_HYP/CSpace_RAB_C.thy +++ b/proof/crefine/ARM_HYP/CSpace_RAB_C.thy @@ -205,10 +205,8 @@ next apply (simp add: cap_get_tag_isCap split del: if_split) apply (thin_tac "ret__unsigned = X" for X) apply (rule ccorres_split_throws [where P = "?P"]) - apply (rule_tac G' = "\w_rightsMask. ({s. nodeCap_' s = nodeCap} - \ {s. unat (n_bits_' s) = guard'})" - in ccorres_abstract [where xf' = w_rightsMask_']) - apply (rule ceqv_refl) + apply (rule_tac P'="{s. nodeCap_' s = nodeCap} \ {s. unat (n_bits_' s) = guard'}" + in ccorres_inst) apply (rule_tac r' = "?rvr" in ccorres_rel_imp [where xf' = rab_xf]) defer diff --git a/proof/crefine/RISCV64/CSpace_RAB_C.thy b/proof/crefine/RISCV64/CSpace_RAB_C.thy index ef2218fd66..c4c5564905 100644 --- a/proof/crefine/RISCV64/CSpace_RAB_C.thy +++ b/proof/crefine/RISCV64/CSpace_RAB_C.thy @@ -208,10 +208,8 @@ next apply (simp add: cap_get_tag_isCap split del: if_split) apply (thin_tac "ret__unsigned_longlong = X" for X) apply (rule ccorres_split_throws [where P = "?P"]) - apply (rule_tac G' = "\w_rightsMask. ({s. nodeCap_' s = nodeCap} - \ {s. unat (n_bits_' s) = guard'})" - in ccorres_abstract [where xf' = w_rightsMask_']) - apply (rule ceqv_refl) + apply (rule_tac P'="{s. nodeCap_' s = nodeCap} \ {s. unat (n_bits_' s) = guard'}" + in ccorres_inst) apply (rule_tac r' = "?rvr" in ccorres_rel_imp [where xf' = rab_xf]) defer diff --git a/proof/crefine/X64/CSpace_RAB_C.thy b/proof/crefine/X64/CSpace_RAB_C.thy index ee0ec07e98..c7838029cd 100644 --- a/proof/crefine/X64/CSpace_RAB_C.thy +++ b/proof/crefine/X64/CSpace_RAB_C.thy @@ -208,10 +208,8 @@ next apply (simp add: cap_get_tag_isCap split del: if_split) apply (thin_tac "ret__unsigned_longlong = X" for X) apply (rule ccorres_split_throws [where P = "?P"]) - apply (rule_tac G' = "\w_rightsMask. ({s. nodeCap_' s = nodeCap} - \ {s. unat (n_bits_' s) = guard'})" - in ccorres_abstract [where xf' = w_rightsMask_']) - apply (rule ceqv_refl) + apply (rule_tac P'="{s. nodeCap_' s = nodeCap} \ {s. unat (n_bits_' s) = guard'}" + in ccorres_inst) apply (rule_tac r' = "?rvr" in ccorres_rel_imp [where xf' = rab_xf]) defer