adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

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 <rafal.kolanski@proofcraft.systems>
This commit is contained in:
Rafal Kolanski 2023-09-14 18:00:22 +10:00 committed by Rafal Kolanski
parent c4369f512c
commit deade608ac
4 changed files with 8 additions and 16 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
proof/crefine/ARM/CSpace_RAB_C.thy
View File

@ -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' = "\<lambda>w_rightsMask. ({s. nodeCap_' s = nodeCap}
\<inter> {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} \<inter> {s. unat (n_bits_' s) = guard'}"
in ccorres_inst)
apply (rule_tac r' = "?rvr" in
ccorres_rel_imp [where xf' = rab_xf])
defer

6
proof/crefine/ARM_HYP/CSpace_RAB_C.thy
View File

@ -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' = "\<lambda>w_rightsMask. ({s. nodeCap_' s = nodeCap}
\<inter> {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} \<inter> {s. unat (n_bits_' s) = guard'}"
in ccorres_inst)
apply (rule_tac r' = "?rvr" in
ccorres_rel_imp [where xf' = rab_xf])
defer

6
proof/crefine/RISCV64/CSpace_RAB_C.thy
View File

@ -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' = "\<lambda>w_rightsMask. ({s. nodeCap_' s = nodeCap}
\<inter> {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} \<inter> {s. unat (n_bits_' s) = guard'}"
in ccorres_inst)
apply (rule_tac r' = "?rvr" in
ccorres_rel_imp [where xf' = rab_xf])
defer

6
proof/crefine/X64/CSpace_RAB_C.thy
View File

@ -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' = "\<lambda>w_rightsMask. ({s. nodeCap_' s = nodeCap}
\<inter> {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} \<inter> {s. unat (n_bits_' s) = guard'}"
in ccorres_inst)
apply (rule_tac r' = "?rvr" in
ccorres_rel_imp [where xf' = rab_xf])
defer