From e0c58e96f758c63115eb9036333f3f7260c4335a Mon Sep 17 00:00:00 2001 From: Michael McInerney Date: Fri, 6 Oct 2023 19:52:21 +1030 Subject: [PATCH 1/4] 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 --- lib/clib/CCorresLemmas.thy | 36 +++++++++++++++++++++++++++++++++++- lib/clib/Corres_UL_C.thy | 8 ++++---- 2 files changed, 39 insertions(+), 5 deletions(-) diff --git a/lib/clib/CCorresLemmas.thy b/lib/clib/CCorresLemmas.thy index 8f712fb50a..fe2425677c 100644 --- a/lib/clib/CCorresLemmas.thy +++ b/lib/clib/CCorresLemmas.thy @@ -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 \ r xf ar axf P Q hs m c" by (simp cong: ccorres_context_cong)+ +lemma add_remove_return: + "getter >>= setter = do (do val \ getter; setter val; return val od); return () od" + by (simp add: bind_assoc) + +lemma ccorres_call_getter_setter_dc: + assumes cul: "ccorresG sr \ r' xf' P (i ` P') [] getter (Call f)" + and gsr: "\x x' s t rv. + \ (x, t) \ sr; r' rv (xf' t); ((), x') \ fst (setter rv x) \ + \ (x', g s t (clean s t)) \ sr" + and ist: "\x s. (x, s) \ sr \ (x, i s) \ sr" + and ef: "\val. empty_fail (setter val)" + shows "ccorresG sr \ dc xfdc P P' hs + (getter >>= setter) + (call i f clean (\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 diff --git a/lib/clib/Corres_UL_C.thy b/lib/clib/Corres_UL_C.thy index 2a5c678be8..9ba8fb9ab5 100644 --- a/lib/clib/Corres_UL_C.thy +++ b/lib/clib/Corres_UL_C.thy @@ -830,14 +830,14 @@ text \ 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\ lemma ccorres_call_getter_setter: - assumes cul: "ccorresG sr \ (=) xf' P (i ` P') [] getter (Call f)" + assumes cul: "ccorresG sr \ r' xf' P (i ` P') [] getter (Call f)" and gsr: "\x x' s t rv rv'. - \ (x, t) \ sr; rv = xf' t; (rv', x') \ fst (setter rv x) \ + \ (x, t) \ sr; r' rv (xf' t); (rv', x') \ fst (setter rv x) \ \ (x', g s t (clean s t)) \ sr" - and res: "\s t rv. rv = xf' t \ rv = xf (g s t (clean s t))" + and res: "\s t rv. r' rv (xf' t) \ r rv (xf (g s t (clean s t)))" and ist: "\x s. (x, s) \ sr \ (x, i s) \ sr" and ef: "\val. empty_fail (setter val)" - shows "ccorresG sr \ (=) xf P P' hs + shows "ccorresG sr \ r xf P P' hs (do val \ getter; setter val; return val od) (call i f clean (\s t. Basic (g s t)))" apply (rule ccorresI') From 27687bf717a0316d89560a526bcc72859d495d0a Mon Sep 17 00:00:00 2001 From: Michael McInerney Date: Mon, 9 Oct 2023 11:37:13 +1030 Subject: [PATCH 2/4] clib: add some rules for hoarep Signed-off-by: Michael McInerney --- lib/clib/CCorresLemmas.thy | 43 ---------------------------- lib/clib/SIMPL_Lemmas.thy | 58 ++++++++++++++++++++++++++++++++++++++ 2 files changed, 58 insertions(+), 43 deletions(-) diff --git a/lib/clib/CCorresLemmas.thy b/lib/clib/CCorresLemmas.thy index fe2425677c..69d8fa2674 100644 --- a/lib/clib/CCorresLemmas.thy +++ b/lib/clib/CCorresLemmas.thy @@ -1040,49 +1040,6 @@ 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 exec_While_final_inv'': - "\ \ \ \b, x\ \ s'; b = While C B; x = Normal s; - \s. s \ C \ I s (Normal s); - \t t' t''. \ t \ C; \\ \B, Normal t\ \ Normal t'; \\ \While C B, Normal t'\ \ t''; - I t' t'' \ \ I t t''; - \t t'. \ t \ C; \\ \B, Normal t\ \ Abrupt t' \ \ I t (Abrupt t'); - \t. \ t \ C; \ \ \B, Normal t\ \ Stuck \ \ I t Stuck; - \t f. \ t \ C; \\ \B, Normal t\ \ Fault f \ \ I t (Fault f) \ - \ I s s'" - apply (induct arbitrary: s rule: exec.induct; simp) - apply (erule exec_elim_cases; fastforce simp: exec.WhileTrue exec.WhileFalse) - done - -lemma intermediate_Normal_state: - "\\ \ \Seq c\<^sub>1 c\<^sub>2, Normal t\ \ t''; t \ P; \ \ P c\<^sub>1 Q\ - \ \t'. \ \ \c\<^sub>1, Normal t\ \ Normal t' \ \ \ \c\<^sub>2, Normal t'\ \ t''" - apply (erule exec_Normal_elim_cases(8)) - apply (insert hoarep_exec) - apply fastforce - done - -lemma While_inv_from_body: - "\ \ (G \ C) B G \ \ \ G While C B G" - apply (drule hoare_sound)+ - apply (rule hoare_complete) - apply (clarsimp simp: cvalid_def HoarePartialDef.valid_def) - by (erule exec_While_final_inv''[where I="\s s'. s \ G \ s' \ Normal ` G", THEN impE], - fastforce+) - -lemma While_inv_from_body_setter: - "\\ \ G setter (G \ {s. s \ C \ s \ Cnd}); \ \ (G \ Cnd) B G\ - \ \ \ (G \ {s. s \ C \ s \ Cnd}) While C (Seq B setter) G" - apply (drule hoare_sound)+ - apply (rule hoare_complete) - apply (clarsimp simp: cvalid_def HoarePartialDef.valid_def) - by (rule exec_While_final_inv'' - [where I="\s s'. s \ G \ (s \ C \ s \ Cnd) \ s' \ Normal ` G", THEN impE], - (fastforce dest!: intermediate_Normal_state[where c\<^sub>1=B and P="G \ Cnd" and Q=G] - intro: hoare_complete - simp: cvalid_def HoarePartialDef.valid_def)+) - -lemmas hoarep_Int_pre_fix = hoarep_Int[where P=P and P'=P for P, simplified] - lemma ccorres_While: assumes body_ccorres: "\r. ccorresG srel \ (=) xf (G and (\s. the (C r s))) (G' \ C') hs (B r) B'" diff --git a/lib/clib/SIMPL_Lemmas.thy b/lib/clib/SIMPL_Lemmas.thy index 6f4d592886..6cc9034016 100644 --- a/lib/clib/SIMPL_Lemmas.thy +++ b/lib/clib/SIMPL_Lemmas.thy @@ -72,6 +72,7 @@ lemma hoarep_Int: apply fastforce done +lemmas hoarep_Int_pre_fix = hoarep_Int[where P=P and P'=P for P, simplified] lemma Normal_result: "\ \ \c, s\ \ Normal t' \ \t. s = Normal t" @@ -350,5 +351,62 @@ lemma hoarep_revert: apply simp done +lemma intermediate_Normal_state: + "\\ \ \Seq c\<^sub>1 c\<^sub>2, Normal t\ \ t''; t \ P; \ \ P c\<^sub>1 Q\ + \ \t'. \ \ \c\<^sub>1, Normal t\ \ Normal t' \ \ \ \c\<^sub>2, Normal t'\ \ t''" + apply (erule exec_Normal_elim_cases(8)) + apply (insert hoarep_exec) + apply fastforce + done + +lemma hoarep_ex_pre: + "(\x. \ \ {s. P x s} c Q) \ \ \ {s. \x. P x s} c Q" + apply (rule hoare_complete) + apply (clarsimp simp: cvalid_def HoarePartialDef.valid_def) + apply (fastforce dest: hoarep_exec'[rotated]) + done + +lemma hoarep_ex_lift: + "(\x. \ \ {s. P x s} c {s. Q x s}) \ \ \ {s. \x. P x s} c {s. \x. Q x s}" + apply (rule hoare_complete) + apply (clarsimp simp: cvalid_def HoarePartialDef.valid_def) + apply (rename_tac s x) + apply (drule_tac x=x in meta_spec) + apply (prop_tac "s \ Collect (P x)") + apply fastforce + apply (frule (2) hoarep_exec) + apply fastforce + done + +lemma hoarep_conj_lift_pre_fix: + "\\ \ P c {s. Q s}; \ \ P c {s. Q' s}\ + \ \ \ P c {s. Q s \ Q' s}" + apply (rule hoare_complete) + apply (clarsimp simp: cvalid_def HoarePartialDef.valid_def) + apply (frule (2) hoarep_exec[where Q="Collect Q"]) + apply (frule (2) hoarep_exec[where Q="Collect Q'"]) + apply fastforce + done + +lemma exec_While_final_inv'': + "\ \ \ \b, x\ \ s'; b = While C B; x = Normal s; + \s. s \ C \ I s (Normal s); + \t t' t''. \ t \ C; \\ \B, Normal t\ \ Normal t'; \\ \While C B, Normal t'\ \ t''; + I t' t'' \ \ I t t''; + \t t'. \ t \ C; \\ \B, Normal t\ \ Abrupt t' \ \ I t (Abrupt t'); + \t. \ t \ C; \ \ \B, Normal t\ \ Stuck \ \ I t Stuck; + \t f. \ t \ C; \\ \B, Normal t\ \ Fault f \ \ I t (Fault f) \ + \ I s s'" + apply (induct arbitrary: s rule: exec.induct; simp) + apply (erule exec_elim_cases; fastforce simp: exec.WhileTrue exec.WhileFalse) + done + +lemma While_inv_from_body: + "\ \ (G \ C) B G \ \ \ G While C B G" + apply (drule hoare_sound)+ + apply (rule hoare_complete) + apply (clarsimp simp: cvalid_def HoarePartialDef.valid_def) + by (erule exec_While_final_inv''[where I="\s s'. s \ G \ s' \ Normal ` G", THEN impE], + fastforce+) end From cb22921154b80fb1d1b1e4ca0b80dca0b605fdff Mon Sep 17 00:00:00 2001 From: Michael McInerney Date: Fri, 6 Oct 2023 20:09:31 +1030 Subject: [PATCH 3/4] clib+crefine: improve and consolidate variants of ccorres_to_vcg Signed-off-by: Michael McInerney --- lib/clib/Corres_UL_C.thy | 53 ++++++++++++++++-------------- proof/crefine/ARM_HYP/Retype_C.thy | 15 --------- proof/crefine/RISCV64/Retype_C.thy | 15 --------- proof/crefine/X64/Retype_C.thy | 15 --------- 4 files changed, 28 insertions(+), 70 deletions(-) diff --git a/lib/clib/Corres_UL_C.thy b/lib/clib/Corres_UL_C.thy index 9ba8fb9ab5..2ec5b2c808 100644 --- a/lib/clib/Corres_UL_C.thy +++ b/lib/clib/Corres_UL_C.thy @@ -288,26 +288,37 @@ lemma ccorres_from_vcg_nofail: apply (rule hoare_complete, simp add: HoarePartialDef.valid_def) done - -lemma ccorres_to_vcg: - "ccorres_underlying srel \ rrel xf arrel axf P P' [] a c \ - (\\. \ snd (a \) \ \ \ {s. P \ \ s \ P' \ (\, s) \ srel} - c - {s. (\(rv, \') \ fst (a \). (\', s) \ srel \ rrel rv (xf s))})" - apply - - apply rule - apply (rule impI) +lemma ccorres_to_vcg_with_prop: + "\ccorres_underlying srel \ rrel xf arrel axf P P' [] a c; no_fail Q a; \P\ a \R\\ + \ \ \ {s'. P s \ Q s \ s' \ P' \ (s, s') \ srel} + c {t'. \(rv, t) \ fst (a s). (t, t') \ srel \ rrel rv (xf t') \ R rv t}" apply (rule hoare_complete) - apply (simp add: HoarePartialDef.valid_def cvalid_def) - apply (intro impI allI) + apply (clarsimp simp: HoarePartialDef.valid_def cvalid_def no_fail_def) + apply (drule_tac x=s in spec) apply clarsimp apply (frule (5) ccorres_empty_handler_abrupt) - apply (erule (4) ccorresE) - apply (erule (1) EHOther) - apply clarsimp - apply rule - apply simp - apply (fastforce simp: unif_rrel_simps) + apply (fastforce elim!: ccorresE EHOther simp: unif_rrel_simps valid_def) + done + +lemma ccorres_to_vcg: + "\ccorres_underlying srel \ rrel xf arrel axf P P' [] a c; no_fail Q a\ + \ \ \ {s'. P s \ Q s \ s' \ P' \ (s, s') \ srel} + c {t'. \(rv, t) \ fst (a s). (t, t') \ srel \ rrel rv (xf t')}" + apply (frule (1) ccorres_to_vcg_with_prop[where R="\\"]) + apply wpsimp + apply fastforce + done + +lemma ccorres_to_vcg_gets_the: + "\ccorres_underlying srel \ rrel xf arrel axf P P' [] (gets_the r) c; no_ofail P r\ + \ \ \ (P' \ {s'. (s, s') \ srel \ P s}) + c {t'. (s, t') \ srel \ P s \ (r s \ None) \ rrel (the (r s)) (xf t')}" + apply (frule ccorres_to_vcg_with_prop[where R="\_. P" and s=s]) + apply (erule no_ofail_gets_the) + apply wpsimp + apply (clarsimp simp: gets_the_def simpler_gets_def bind_def return_def get_def assert_opt_def + fail_def conseq_under_new_pre + split: option.splits) done lemma exec_handlers_Seq_cases0': @@ -1402,14 +1413,6 @@ lemma ccorres_move_Guard: section "novcg" -lemma ccorres_to_vcg': - "\ ccorres_underlying srel \ rrel xf arrel axf P P' [] a c; \ snd (a \) \ \ - \\ {s. P \ \ s \ P' \ (\, s) \ srel} c - {s. \(rv, \')\fst (a \). (\', s) \ srel \ rrel rv (xf s)}" - apply (drule ccorres_to_vcg) - apply clarsimp - done - lemma exec_handlers_Hoare_UNIV: "guard_is_UNIV r xf Q \ exec_handlers_Hoare \ UNIV cs (ccHoarePost r xf Q) UNIV" diff --git a/proof/crefine/ARM_HYP/Retype_C.thy b/proof/crefine/ARM_HYP/Retype_C.thy index 767dcac4dc..23030fcc21 100644 --- a/proof/crefine/ARM_HYP/Retype_C.thy +++ b/proof/crefine/ARM_HYP/Retype_C.thy @@ -2422,21 +2422,6 @@ next done qed -(* FIXME: move *) -lemma ccorres_to_vcg_nf: - "\ccorres rrel xf P P' [] a c; no_fail Q a; \s. P s \ Q s\ - \ \\ {s. P \ \ s \ P' \ (\, s) \ rf_sr} c - {s. \(rv, \')\fst (a \). (\', s) \ rf_sr \ rrel rv (xf s)}" - apply (rule HoarePartial.conseq_exploit_pre) - apply clarsimp - apply (rule conseqPre) - apply (drule ccorres_to_vcg') - prefer 2 - apply simp - apply (simp add: no_fail_def) - apply clarsimp - done - lemma mdb_node_get_mdbNext_heap_ccorres: "ccorres (=) ret__unsigned_' \ UNIV hs (liftM (mdbNext \ cteMDBNode) (getCTE parent)) diff --git a/proof/crefine/RISCV64/Retype_C.thy b/proof/crefine/RISCV64/Retype_C.thy index 1e09815965..a1b8e76ab6 100644 --- a/proof/crefine/RISCV64/Retype_C.thy +++ b/proof/crefine/RISCV64/Retype_C.thy @@ -2244,21 +2244,6 @@ next done qed -(* FIXME: move *) -lemma ccorres_to_vcg_nf: - "\ccorres rrel xf P P' [] a c; no_fail Q a; \s. P s \ Q s\ - \ \\ {s. P \ \ s \ P' \ (\, s) \ rf_sr} c - {s. \(rv, \')\fst (a \). (\', s) \ rf_sr \ rrel rv (xf s)}" - apply (rule HoarePartial.conseq_exploit_pre) - apply clarsimp - apply (rule conseqPre) - apply (drule ccorres_to_vcg') - prefer 2 - apply simp - apply (simp add: no_fail_def) - apply clarsimp - done - lemma mdb_node_get_mdbNext_heap_ccorres: "ccorres (=) ret__unsigned_longlong_' \ UNIV hs (liftM (mdbNext \ cteMDBNode) (getCTE parent)) diff --git a/proof/crefine/X64/Retype_C.thy b/proof/crefine/X64/Retype_C.thy index 4f37ce630d..ba09bf95e1 100644 --- a/proof/crefine/X64/Retype_C.thy +++ b/proof/crefine/X64/Retype_C.thy @@ -2771,21 +2771,6 @@ next done qed -(* FIXME: move *) -lemma ccorres_to_vcg_nf: - "\ccorres rrel xf P P' [] a c; no_fail Q a; \s. P s \ Q s\ - \ \\ {s. P \ \ s \ P' \ (\, s) \ rf_sr} c - {s. \(rv, \')\fst (a \). (\', s) \ rf_sr \ rrel rv (xf s)}" - apply (rule HoarePartial.conseq_exploit_pre) - apply clarsimp - apply (rule conseqPre) - apply (drule ccorres_to_vcg') - prefer 2 - apply simp - apply (simp add: no_fail_def) - apply clarsimp - done - lemma mdb_node_get_mdbNext_heap_ccorres: "ccorres (=) ret__unsigned_longlong_' \ UNIV hs (liftM (mdbNext \ cteMDBNode) (getCTE parent)) From b3917f1185f6a99e3ca629cc620b01c0d01567ea Mon Sep 17 00:00:00 2001 From: Michael McInerney Date: Mon, 9 Oct 2023 11:50:59 +1030 Subject: [PATCH 4/4] 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 69d8fa2674..bb467af531 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