From 4d19f6616f495825d22f92e5b9f119046c9aa7d4 Mon Sep 17 00:00:00 2001 From: Michael McInerney Date: Mon, 9 Oct 2023 11:50:59 +1030 Subject: [PATCH] clib: improve ccorres_While Signed-off-by: Michael McInerney --- lib/clib/CCorresLemmas.thy | 199 +++++++++++++++++++++++++++++-------- 1 file changed, 160 insertions(+), 39 deletions(-) diff --git a/lib/clib/CCorresLemmas.thy b/lib/clib/CCorresLemmas.thy index 69d8fa267..bb467af53 100644 --- a/lib/clib/CCorresLemmas.thy +++ b/lib/clib/CCorresLemmas.thy @@ -1040,76 +1040,197 @@ lemma ccorres_Guard_True_Seq: \ ccorres_underlying sr \ r xf arrel axf A C hs a (Guard F \True\ c ;; d)" by (simp, ccorres_rewrite, assumption) +lemma ccorres_While_Normal_helper: + assumes setter_inv: + "\ \ {s'. \rv s. G rv s s'} setter {s'. \rv s. G rv s s' \ (cond_xf s' \ 0 \ Cnd rv s s')}" + assumes body_inv: "\ \ {s'. \rv s. G rv s s' \ Cnd rv s s'} B {s'. \rv s. G rv s s'}" + shows "\ \ ({s'. \rv s. G rv s s' \ (cond_xf s' \ 0 \ Cnd rv s s')}) + While {s'. cond_xf s' \ 0} (Seq B setter) + {s'. \rv s. G rv s s'}" + apply (insert assms) + apply (rule hoare_complete) + apply (simp add: cvalid_def HoarePartialDef.valid_def) + apply (intro allI) + apply (rename_tac xstate xstate') + apply (rule impI) + apply (case_tac "\ isNormal xstate") + apply fastforce + apply (simp add: isNormal_def) + apply (elim exE) + apply (simp add: image_def) + apply (erule exec_While_final_inv''[where C="{s'. cond_xf s' \ 0}" and B="B;; setter"]; clarsimp) + apply (frule intermediate_Normal_state[OF _ _ body_inv]) + apply fastforce + apply clarsimp + apply (rename_tac inter_t) + apply (frule hoarep_exec[OF _ _ body_inv, rotated], fastforce) + apply (frule_tac s=inter_t in hoarep_exec[rotated 2], fastforce+)[1] + apply (metis (mono_tags, lifting) HoarePartial.SeqSwap empty_iff exec_abrupt mem_Collect_eq) + apply (metis (mono_tags, lifting) HoarePartial.SeqSwap exec_stuck mem_Collect_eq) + apply (metis (mono_tags, lifting) HoarePartial.SeqSwap empty_iff exec_fault mem_Collect_eq) + done + lemma ccorres_While: assumes body_ccorres: - "\r. ccorresG srel \ (=) xf (G and (\s. the (C r s))) (G' \ C') hs (B r) B'" - and cond_ccorres: - "\r. ccorresG srel \ (\rv rv'. rv = to_bool rv') cond_xf G G' hs (gets_the (C r)) setter" - and nf: "\r. no_fail (G and (\s. the (C r s))) (B r)" - and no_ofail: "\r. no_ofail G (C r)" - and body_inv: "\r. \G and (\s. the (C r s))\ B r \\_. G\" - "\ \ (G' \ C') B' G'" - and setter_inv_cond: "\ \ G' setter (G' \ {s'. cond_xf s' \ 0 \ s' \ C'})" - and setter_xf_inv: "\val. \ \ {s'. xf s' = val} setter {s'. xf s' = val}" - shows "ccorresG srel \ (=) xf G (G' \ {s'. xf s' = r}) hs - (whileLoop (\r s. the (C r s)) B r) - (Seq setter (While {s'. cond_xf s' \ 0} (Seq B' setter)))" + "\r. ccorresG srel \ rrel xf (\s. G r s \ C r s = Some True) (G' \ C') [] (B r) B'" + assumes setter_ccorres: + "\r. ccorresG srel \ (\rv rv'. rv = to_bool rv') cond_xf (G r) G' [] (gets_the (C r)) setter" + assumes nf: "\r. no_fail (\s. G r s \ C r s = Some True) (B r)" + assumes no_ofail: "\r. no_ofail (G r) (C r)" + assumes body_inv: + "\r. \\s. G r s \ C r s = Some True\ B r \G\" + "\r s. \ \ {s'. s' \ G' \ (s, s') \ srel \ G r s \ rrel r (xf s') + \ s' \ C' \ C r s = Some True} + B' G'" + assumes setter_inv_cond: + "\r s. \ \ {s'. s' \ G' \ (s, s') \ srel \ G r s \ rrel r (xf s')} + setter + {s'. s' \ G' \ (cond_xf s' \ 0 \ s' \ C')}" + assumes setter_rrel: + "\r s. \ \ {s'. s' \ G' \ (s, s') \ srel \ G r s \ rrel r (xf s')} + setter + {s'. rrel r (xf s')}" + shows + "ccorresG srel \ rrel xf (G r) (G' \ {s'. rrel r (xf s')}) hs + (whileLoop (\r s. the (C r s)) B r) + (setter;; (While {s'. cond_xf s' \ 0} (B';; setter)))" proof - note unif_rrel_def[simp add] to_bool_def[simp add] have helper: "\state xstate'. \ \ \While {s'. cond_xf s' \ 0} (Seq B' setter), Normal state\ \ xstate' \ \st r s. Normal st = xstate' \ (s, state) \ srel - \ (cond_xf state \ 0) = the (C r s) \ xf state = r \ G s - \ state \ G' \ (cond_xf state \ 0 \ state \ C') + \ (C r s \ None) \ (cond_xf state \ 0) = the (C r s) + \ rrel r (xf state) \ G r s \ state \ G' \ (cond_xf state \ 0 \ state \ C') \ (\rv s'. (rv, s') \ fst (whileLoop (\r s. the (C r s)) B r s) - \ (s', st) \ srel \ rv = xf st)" - apply (erule exec_While_final_inv''; simp) + \ (s', st) \ srel \ rrel rv (xf st))" + apply (erule_tac C="{s'. cond_xf s' \ 0}" in exec_While_final_inv''; simp) apply (fastforce simp: whileLoop_cond_fail return_def) apply clarsimp - apply (rename_tac t t' t'' s) - apply (frule intermediate_Normal_state[where P="G' \ C'"]) + apply (rename_tac t t' t'' r s y) + apply (frule_tac P="{s'. s' \ G' \ (s, s') \ srel \ G r s \ rrel r (xf s') + \ s' \ C' \ (C r s \ None) \ the (C r s)}" + in intermediate_Normal_state) apply fastforce - apply (fastforce intro: body_inv) + apply (fastforce intro: body_inv conseqPre) apply clarsimp apply (rename_tac inter_t) - apply (prop_tac "\s'. (xf inter_t, s') \ fst (B (xf t) s) \ (s', inter_t) \ srel") - subgoal by (erule ccorresE[OF body_ccorres]) - (fastforce simp: no_fail_def nf[simplified no_fail_def] dest: EHOther)+ + apply (prop_tac "\rv' s'. rrel rv' (xf inter_t) \ (rv', s') \ fst (B r s) + \ (s', inter_t) \ srel") + apply (insert body_ccorres)[1] + apply (drule_tac x=r in meta_spec) + apply (erule (1) ccorresE) + apply fastforce + apply fastforce + using nf apply (fastforce simp: no_fail_def) + apply (fastforce dest!: EHOther) + apply fastforce apply clarsimp - apply (prop_tac "G s'") + apply (prop_tac "G rv' s'") apply (fastforce dest: use_valid intro: body_inv) apply (prop_tac "inter_t \ G'") apply (fastforce dest: hoarep_exec[rotated] intro: body_inv) + 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 (elim impE) - apply (drule_tac s'=inter_t and r1="xf t'" in ccorresE_gets_the[OF cond_ccorres]; assumption?) + apply (frule_tac s'=inter_t and r1=rv' in ccorresE_gets_the[OF setter_ccorres]; assumption?) apply (fastforce intro: no_ofail) apply (fastforce dest: EHOther) - subgoal by (fastforce dest: hoarep_exec intro: setter_inv_cond) - apply (prop_tac "xf inter_t = xf t'") - apply (fastforce dest: hoarep_exec[rotated] intro: setter_xf_inv) + 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 simp: whileLoop_def intro: whileLoop_results.intros(3)) done + have setter_hoarep: + "\r s s' n xstate. + \\\<^sub>h \(setter;; While {s'. cond_xf s' \ 0} (B';; setter)) # hs,s'\ \ (n, xstate) + \ \\ {s' \ G'. (s, s') \ srel \ G r s \ rrel r (xf s')} + setter + {s'. (s' \ G' \ (s, s') \ srel \ G r s \ rrel r (xf s')) + \ (cond_xf s' \ 0 \ (s' \ C' \ C r s = Some True))}" + apply (insert setter_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 (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' \ G'. cond_xf s' \ 0 \ s' \ C'}" in conseqPost; fastforce) + apply (fastforce intro!: hoarep_conj_lift_pre_fix simp: Collect_mono conseq_under_new_pre) + apply (insert setter_inv_cond) + apply (drule_tac x=s in meta_spec) + apply (drule_tac x=r in meta_spec) + apply (simp add: imp_conjR) + apply (rule hoarep_conj_lift_pre_fix) + apply (simp add: Collect_mono conseq_under_new_pre) + apply (rule_tac Q'="{s'. C r s \ None \ the (C r s) = (cond_xf s' \ 0)}" + in conseqPost[rotated]) + apply fastforce + apply fastforce + apply (simp add: Collect_mono conseq_under_new_pre) + done + show ?thesis apply (clarsimp simp: ccorres_underlying_def) apply (rename_tac s s' n xstate) - apply (frule (1) exec_handlers_use_hoare_nothrow_hoarep) - apply (rule_tac R="G' \ {s'. s' \ {t. cond_xf t \ 0} \ s' \ C'}" in HoarePartial.Seq) - apply (fastforce intro: setter_inv_cond) - apply (fastforce intro: While_inv_from_body_setter setter_inv_cond body_inv) - apply clarsimp - apply (frule (1) intermediate_Normal_state) - apply (fastforce intro: setter_inv_cond) + apply (frule_tac R'="{s'. s' \ G' \ (s, s') \ srel \ G r s \ rrel r (xf s')}" + and Q'="{s'. \rv s. s' \ G' \ (s, s') \ srel \ G rv s \ rrel rv (xf s')}" + in exec_handlers_use_hoare_nothrow_hoarep) + apply fastforce + apply (rule HoarePartial.Seq) + apply (erule setter_hoarep) + apply (rule conseqPre) + apply (rule ccorres_While_Normal_helper) + apply (fastforce intro!: setter_hoarep hoarep_ex_lift) + apply (intro hoarep_ex_pre, rename_tac rv new_s) + apply (insert setter_inv_cond)[1] + apply (drule_tac x=new_s in meta_spec) + apply (drule_tac x=rv in meta_spec) + apply (insert body_ccorres)[1] + apply (drule_tac x=rv in meta_spec) + apply (insert body_inv(2))[1] + apply (drule_tac x=new_s in meta_spec) + apply (drule_tac x=rv in meta_spec) + apply (frule_tac s=new_s in ccorres_to_vcg_with_prop) + using nf apply fastforce + using body_inv apply fastforce + apply (rule_tac Q'="{s'. s' \ G' + \ (\(rv, s) \fst (B rv new_s). (s, s') \ srel \ rrel rv (xf s') + \ G rv s)}" + in conseqPost; + fastforce?) + apply (rule hoarep_conj_lift_pre_fix; + 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 fastforce apply clarsimp apply (rename_tac inter_t) - apply (drule (2) ccorresE_gets_the[OF cond_ccorres _ _ _ no_ofail]) + apply (insert setter_ccorres) + apply (drule_tac x=r in meta_spec) + apply (drule (3) ccorresE_gets_the) + apply (fastforce intro: no_ofail) apply (fastforce dest: EHOther) - apply (prop_tac "xf inter_t = xf s'") - apply (fastforce dest: hoarep_exec[rotated] intro: setter_xf_inv) - apply (clarsimp simp: isNormal_def) - apply (auto dest: hoarep_exec dest!: helper spec intro: setter_inv_cond) + apply (prop_tac "rrel r (xf inter_t)") + apply (fastforce dest: hoarep_exec[rotated] intro: setter_rrel) + apply (case_tac "\ 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) done qed