Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Further improvements to ccorres_While #697

Merged
merged 1 commit into from
Dec 6, 2023
Merged

Further improvements to ccorres_While #697

Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
83 changes: 47 additions & 36 deletions lib/clib/CCorresLemmas.thy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -1070,35 +1070,40 @@ lemma ccorres_While_Normal_helper:
apply (metis (mono_tags, lifting) HoarePartial.SeqSwap empty_iff exec_fault mem_Collect_eq)
done

text \<open>
This rule is intended to be used to show correspondence between a Haskell whileLoop and a C
while loop, where in particular, the C while loop is parsed into a Simpl While loop that
updates the cstate as part of the loop condition. In such a case, the CParser will produce a Simpl
program in the form that is seen in the conclusion of this rule.\<close>
lemma ccorres_While:
assumes body_ccorres:
"\<And>r. ccorresG srel \<Gamma> rrel xf (\<lambda>s. G r s \<and> C r s = Some True) (G' \<inter> C') [] (B r) B'"
assumes setter_ccorres:
"\<And>r. ccorresG srel \<Gamma> (\<lambda>rv rv'. rv = to_bool rv') cond_xf (G r) G' [] (gets_the (C r)) setter"
"\<And>r. ccorresG srel \<Gamma> rrel xf
(\<lambda>s. G r s \<and> C r s = Some True) (G' \<inter> C' \<inter> {s'. rrel r (xf s')}) []
(B r) B'"
assumes cond_ccorres:
"\<And>r. ccorresG srel \<Gamma> (\<lambda>rv rv'. rv = to_bool rv') cond_xf
(G r) (G' \<inter> {s'. rrel r (xf s')}) []
(gets_the (C r)) cond"
assumes nf: "\<And>r. no_fail (\<lambda>s. G r s \<and> C r s = Some True) (B r)"
assumes no_ofail: "\<And>r. no_ofail (G r) (C r)"
assumes body_inv:
"\<And>r. \<lbrace>\<lambda>s. G r s \<and> C r s = Some True\<rbrace> B r \<lbrace>G\<rbrace>"
"\<And>r s. \<Gamma> \<turnstile> {s'. s' \<in> G' \<and> (s, s') \<in> srel \<and> G r s \<and> rrel r (xf s')
\<and> s' \<in> C' \<and> C r s = Some True}
B' G'"
assumes setter_inv_cond:
assumes cond_hoarep:
"\<And>r s. \<Gamma> \<turnstile> {s'. s' \<in> G' \<and> (s, s') \<in> srel \<and> G r s \<and> rrel r (xf s')}
setter
{s'. s' \<in> G' \<and> (cond_xf s' \<noteq> 0 \<longrightarrow> s' \<in> C')}"
assumes setter_rrel:
"\<And>r s. \<Gamma> \<turnstile> {s'. s' \<in> G' \<and> (s, s') \<in> srel \<and> G r s \<and> rrel r (xf s')}
setter
{s'. rrel r (xf s')}"
cond
{s'. s' \<in> G' \<and> (cond_xf s' \<noteq> 0 \<longrightarrow> s' \<in> C') \<and> rrel r (xf s')}"
shows
"ccorresG srel \<Gamma> rrel xf (G r) (G' \<inter> {s'. rrel r (xf s')}) hs
(whileLoop (\<lambda>r s. the (C r s)) B r)
(setter;; (While {s'. cond_xf s' \<noteq> 0} (B';; setter)))"
(cond;; While {s'. cond_xf s' \<noteq> 0} (B';; cond))"
proof -
note unif_rrel_def[simp add] to_bool_def[simp add]
have helper:
"\<And>state xstate'.
\<Gamma> \<turnstile> \<langle>While {s'. cond_xf s' \<noteq> 0} (Seq B' setter), Normal state\<rangle> \<Rightarrow> xstate' \<Longrightarrow>
\<Gamma> \<turnstile> \<langle>While {s'. cond_xf s' \<noteq> 0} (Seq B' cond), Normal state\<rangle> \<Rightarrow> xstate' \<Longrightarrow>
\<forall>st r s. Normal st = xstate' \<and> (s, state) \<in> srel
\<and> (C r s \<noteq> None) \<and> (cond_xf state \<noteq> 0) = the (C r s)
\<and> rrel r (xf state) \<and> G r s \<and> state \<in> G' \<and> (cond_xf state \<noteq> 0 \<longrightarrow> state \<in> C')
Expand Down Expand Up @@ -1133,44 +1138,43 @@ proof -
apply (drule_tac x=rv' in spec)
apply (drule_tac x=s' in spec)
apply (prop_tac "rrel rv' (xf inter_t)")
apply (fastforce dest: hoarep_exec[OF _ _ setter_rrel, rotated])
apply (fastforce dest: hoarep_exec[OF _ _ cond_hoarep, rotated])
apply (elim impE)
apply (frule_tac s'=inter_t and r1=rv' in ccorresE_gets_the[OF setter_ccorres]; assumption?)
apply (frule_tac s'=inter_t and r1=rv' in ccorresE_gets_the[OF cond_ccorres]; assumption?)
apply fastforce
apply (fastforce intro: no_ofail)
apply (fastforce dest: EHOther)
apply (intro conjI)
apply fastforce
using no_ofail apply (fastforce elim!: no_ofailD)
apply fastforce
apply (fastforce dest: hoarep_exec[OF _ _ setter_rrel, rotated])
apply (fastforce dest: hoarep_exec[OF _ _ setter_inv_cond, rotated])
apply (fastforce dest: hoarep_exec[OF _ _ setter_inv_cond, rotated])
apply (fastforce dest: hoarep_exec[OF _ _ setter_inv_cond, rotated])
apply (fastforce dest: hoarep_exec[OF _ _ cond_hoarep, rotated])
apply (fastforce dest: hoarep_exec[OF _ _ cond_hoarep, rotated])
apply (fastforce dest: hoarep_exec[OF _ _ cond_hoarep, rotated])
apply (fastforce dest: hoarep_exec[OF _ _ cond_hoarep, rotated])
apply (fastforce simp: whileLoop_def intro: whileLoop_results.intros(3))
done

have setter_hoarep:
have cond_hoarep':
"\<And>r s s' n xstate.
\<Gamma>\<turnstile>\<^sub>h \<langle>(setter;; While {s'. cond_xf s' \<noteq> 0} (B';; setter)) # hs,s'\<rangle> \<Rightarrow> (n, xstate)
\<Gamma>\<turnstile>\<^sub>h \<langle>(cond;; While {s'. cond_xf s' \<noteq> 0} (B';; cond)) # hs,s'\<rangle> \<Rightarrow> (n, xstate)
\<Longrightarrow> \<Gamma>\<turnstile> {s' \<in> G'. (s, s') \<in> srel \<and> G r s \<and> rrel r (xf s')}
setter
cond
{s'. (s' \<in> G' \<and> (s, s') \<in> srel \<and> G r s \<and> rrel r (xf s'))
\<and> (cond_xf s' \<noteq> 0 \<longrightarrow> (s' \<in> C' \<and> C r s = Some True))}"
apply (insert setter_ccorres)
apply (insert cond_ccorres)
apply (drule_tac x=r in meta_spec)
apply (frule_tac s=s in ccorres_to_vcg_gets_the)
apply (fastforce intro: no_ofail)
apply (insert setter_rrel)
apply (insert cond_hoarep)
apply (drule_tac x=s in meta_spec)
apply (drule_tac x=r in meta_spec)
apply (rule hoarep_conj_lift_pre_fix)
apply (rule hoarep_conj_lift_pre_fix)
apply (insert setter_inv_cond)[1]
apply (drule_tac x=s in meta_spec)
apply (drule_tac x=r in meta_spec)
apply (rule_tac Q'="{s' \<in> G'. cond_xf s' \<noteq> 0 \<longrightarrow> s' \<in> C'}" in conseqPost; fastforce)
apply (insert cond_hoarep)[1]
apply (fastforce simp: conseq_under_new_pre)
apply (fastforce intro!: hoarep_conj_lift_pre_fix simp: Collect_mono conseq_under_new_pre)
apply (insert setter_inv_cond)
apply (insert cond_hoarep)
apply (drule_tac x=s in meta_spec)
apply (drule_tac x=r in meta_spec)
apply (simp add: imp_conjR)
Expand All @@ -1183,6 +1187,12 @@ proof -
apply (simp add: Collect_mono conseq_under_new_pre)
done

have cond_inv_guard:
"\<And>r s. \<Gamma> \<turnstile> {s'. s' \<in> G' \<and> (s, s') \<in> srel \<and> G r s \<and> rrel r (xf s')}
cond
{s'. s' \<in> G' \<and> (cond_xf s' \<noteq> 0 \<longrightarrow> s' \<in> C')}"
by (fastforce intro: conseqPost cond_hoarep)

show ?thesis
apply (clarsimp simp: ccorres_underlying_def)
apply (rename_tac s s' n xstate)
Expand All @@ -1191,12 +1201,12 @@ proof -
in exec_handlers_use_hoare_nothrow_hoarep)
apply fastforce
apply (rule HoarePartial.Seq)
apply (erule setter_hoarep)
apply (erule cond_hoarep')
apply (rule conseqPre)
apply (rule ccorres_While_Normal_helper)
apply (fastforce intro!: setter_hoarep hoarep_ex_lift)
apply (fastforce intro!: cond_hoarep' hoarep_ex_lift)
apply (intro hoarep_ex_pre, rename_tac rv new_s)
apply (insert setter_inv_cond)[1]
apply (insert cond_inv_guard)[1]
apply (drule_tac x=new_s in meta_spec)
apply (drule_tac x=rv in meta_spec)
apply (insert body_ccorres)[1]
Expand All @@ -1216,21 +1226,22 @@ proof -
fastforce simp: Collect_mono conseq_under_new_pre)
apply fastforce
apply (case_tac xstate; clarsimp)
apply (frule intermediate_Normal_state[OF _ _ setter_hoarep]; assumption?)
apply (frule intermediate_Normal_state[OF _ _ cond_hoarep]; assumption?)
apply fastforce
apply clarsimp
apply (rename_tac inter_t)
apply (insert setter_ccorres)
apply (insert cond_ccorres)
apply (drule_tac x=r in meta_spec)
apply (drule (3) ccorresE_gets_the)
apply (drule (2) ccorresE_gets_the)
apply fastforce
apply (fastforce intro: no_ofail)
apply (fastforce dest: EHOther)
apply (prop_tac "rrel r (xf inter_t)")
apply (fastforce dest: hoarep_exec[rotated] intro: setter_rrel)
apply (fastforce dest: hoarep_exec[rotated] intro: cond_hoarep)
apply (case_tac "\<not> the (C r s)")
apply (fastforce elim: exec_Normal_elim_cases simp: whileLoop_cond_fail return_def)
apply (insert no_ofail)
apply (fastforce dest!: helper hoarep_exec[OF _ _ setter_inv_cond, rotated] no_ofailD)
apply (fastforce dest!: helper hoarep_exec[OF _ _ cond_inv_guard, rotated] no_ofailD)
done
qed

Expand Down