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

clib: improve ccorres_call_getter_setter 

This generalises the rule ccorres_call_getter_setter by allowing the return
relation between the "getter" and the C function called to be arbitrary,
rather than just the identity relation.

A variant of this rule, ccorres_call_getter_setter_dc, is provided for
when we do not care about the return relation.

Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>
This commit is contained in:
Michael McInerney 2023-10-06 19:52:21 +10:30 committed by Achim D. Brucker
parent af3505401b
commit e122ad9d92
2 changed files with 39 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

36
lib/clib/CCorresLemmas.thy
View File

@ -5,7 +5,7 @@
*)
theory CCorresLemmas
imports CCorres_Rewrite
imports CCorres_Rewrite MonadicRewrite_C
begin
lemma ccorres_rel_imp2:
@ -1177,4 +1177,38 @@ lemma ccorres_inr_rrel_Inr[simp]:
= ccorres_underlying srel \<Gamma> r xf ar axf P Q hs m c"
by (simp cong: ccorres_context_cong)+
lemma add_remove_return:
"getter >>= setter = do (do val \<leftarrow> getter; setter val; return val od); return () od"
by (simp add: bind_assoc)
lemma ccorres_call_getter_setter_dc:
assumes cul: "ccorresG sr \<Gamma> r' xf' P (i ` P') [] getter (Call f)"
and gsr: "\<And>x x' s t rv.
\<lbrakk> (x, t) \<in> sr; r' rv (xf' t); ((), x') \<in> fst (setter rv x) \<rbrakk>
\<Longrightarrow> (x', g s t (clean s t)) \<in> sr"
and ist: "\<And>x s. (x, s) \<in> sr \<Longrightarrow> (x, i s) \<in> sr"
and ef: "\<And>val. empty_fail (setter val)"
shows "ccorresG sr \<Gamma> dc xfdc P P' hs
(getter >>= setter)
(call i f clean (\<lambda>s t. Basic (g s t)))"
apply (rule ccorres_guard_imp)
apply (rule monadic_rewrite_ccorres_assemble[rotated])
apply (rule monadic_rewrite_is_refl)
apply (rule add_remove_return)
apply (rule ccorres_seq_skip'[THEN iffD1])
apply (rule ccorres_split_nothrow_novcg)
apply (rule ccorres_call_getter_setter)
apply (fastforce intro: cul)
apply (fastforce intro: gsr)
apply (simp add: gsr)
apply (fastforce intro: ist)
apply (fastforce intro: ef)
apply (rule ceqv_refl)
apply (fastforce intro: ccorres_return_Skip)
apply wpsimp
apply (clarsimp simp: guard_is_UNIV_def)
apply wpsimp
apply fastforce
done
end

8
lib/clib/Corres_UL_C.thy
View File

@ -830,14 +830,14 @@ text \<open>
between the values set on the concrete and abstract side. The @{thm bind_assoc_return_reverse} rule
may assist with rewriting statements to add the extra return needed by this rule\<close>
lemma ccorres_call_getter_setter:
assumes cul: "ccorresG sr \<Gamma> (=) xf' P (i ` P') [] getter (Call f)"
assumes cul: "ccorresG sr \<Gamma> r' xf' P (i ` P') [] getter (Call f)"
and gsr: "\<And>x x' s t rv rv'.
\<lbrakk> (x, t) \<in> sr; rv = xf' t; (rv', x') \<in> fst (setter rv x) \<rbrakk>
\<lbrakk> (x, t) \<in> sr; r' rv (xf' t); (rv', x') \<in> fst (setter rv x) \<rbrakk>
\<Longrightarrow> (x', g s t (clean s t)) \<in> sr"
and res: "\<And>s t rv. rv = xf' t \<Longrightarrow> rv = xf (g s t (clean s t))"
and res: "\<And>s t rv. r' rv (xf' t) \<Longrightarrow> r rv (xf (g s t (clean s t)))"
and ist: "\<And>x s. (x, s) \<in> sr \<Longrightarrow> (x, i s) \<in> sr"
and ef: "\<And>val. empty_fail (setter val)"
shows "ccorresG sr \<Gamma> (=) xf P P' hs
shows "ccorresG sr \<Gamma> r xf P P' hs
(do val \<leftarrow> getter; setter val; return val od)
(call i f clean (\<lambda>s t. Basic (g s t)))"
apply (rule ccorresI')