From ee31cd359316a268ba3c08851ec4f7b0ea34a809 Mon Sep 17 00:00:00 2001 From: Michael McInerney Date: Tue, 9 Jul 2024 11:25:10 +0930 Subject: [PATCH 01/15] clib: remove no_fail assumption from ccorres_While Signed-off-by: Michael McInerney --- lib/clib/CCorresLemmas.thy | 242 ++++++++++++++----------------------- lib/clib/SIMPL_Lemmas.thy | 8 -- 2 files changed, 88 insertions(+), 162 deletions(-) diff --git a/lib/clib/CCorresLemmas.thy b/lib/clib/CCorresLemmas.thy index 74870f7ebf..ad366fda3d 100644 --- a/lib/clib/CCorresLemmas.thy +++ b/lib/clib/CCorresLemmas.thy @@ -1040,41 +1040,22 @@ 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 - text \ - 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.\ + This rule is intended to be used to show correspondence between a @{term whileLoop} and a Simpl + statement involving @{term While} where + + - the @{term whileLoop} condition uses a function in the reader monad, which must not fail, + necessitating the @{term no_ofail} assumption below. Removing this assumption would require a + variant of @{term whileLoop} which uses a reader monad function for the loop condition and + which fails if this reader function fails. + + - the C loop condition updates the cstate, in which case, the CParser will produce a Simpl + statment of the form that is seen in the conclusion of this rule, and + + - the C loop condition and the C loop body always produce, under expected circumstances as + described in the @{term hoarep} assumptions below, @{term Normal} extended states. As such, + the conclusion of this rule, as well as the assumptions below involving @{term ccorresG} + require an empty handler stack.\ lemma ccorres_While: assumes body_ccorres: "\r. ccorresG srel \ rrel xf @@ -1084,84 +1065,28 @@ lemma ccorres_While: "\r. ccorresG srel \ (\rv rv'. rv = to_bool rv') cond_xf (G r) (G' \ {s'. rrel r (xf s')}) [] (gets_the (C r)) cond" - 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} + assumes abs_body_inv: "\r. \\s. G r s \ C r s = Some True\ B r \G\" + assumes conc_body_inv: + "\r s. \ \ {s'. s' \ G' \ (s, s') \ srel \ G r s \ rrel r (xf s') \ \ snd (B r s) \ s' \ C' + \ C r s = Some True} B' G'" assumes cond_hoarep: "\r s. \ \ {s'. s' \ G' \ (s, s') \ srel \ G r s \ rrel r (xf s')} cond {s'. s' \ G' \ (cond_xf s' \ 0 \ s' \ C') \ rrel r (xf s')}" shows - "ccorresG srel \ rrel xf (G r) (G' \ {s'. rrel r (xf s')}) hs + "ccorresG srel \ rrel xf (G r) (G' \ {s'. rrel r (xf s')}) [] (whileLoop (\r s. the (C r s)) B r) (cond;; While {s'. cond_xf s' \ 0} (B';; cond))" proof - - note unif_rrel_def[simp add] to_bool_def[simp add] - have helper: - "\state xstate'. - \ \ \While {s'. cond_xf s' \ 0} (Seq B' cond), Normal state\ \ xstate' \ - \st r s. Normal st = xstate' \ (s, state) \ srel - \ (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 \ 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'' 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 conseqPre) - apply clarsimp - apply (rename_tac inter_t) - 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 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 _ _ cond_hoarep, rotated]) - apply (elim impE) - 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 _ _ 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 cond_hoarep': - "\r s s' n xstate. - \\\<^sub>h \(cond;; While {s'. cond_xf s' \ 0} (B';; cond)) # hs,s'\ \ (n, xstate) - \ \\ {s' \ G'. (s, s') \ srel \ G r s \ rrel r (xf s')} - cond - {s'. (s' \ G' \ (s, s') \ srel \ G r s \ rrel r (xf s')) - \ (cond_xf s' \ 0 \ (s' \ C' \ C r s = Some True))}" + "\r s. + \ \ {s' \ G'. (s, s') \ srel \ G r s \ rrel r (xf s')} + cond + {s'. (s' \ G' \ (s, s') \ srel \ G r s \ rrel r (xf s')) + \ (cond_xf s' \ 0 \ (s' \ C' \ C r s = Some True)) + \ C r s \ None \ the (C r s) = (cond_xf s' \ 0)}" apply (insert cond_ccorres) apply (drule_tac x=r in meta_spec) apply (frule_tac s=s in ccorres_to_vcg_gets_the) @@ -1171,12 +1096,8 @@ proof - apply (drule_tac x=r in meta_spec) apply (rule hoarep_conj_lift_pre_fix) apply (rule hoarep_conj_lift_pre_fix) - apply (insert cond_hoarep)[1] - apply (fastforce simp: conseq_under_new_pre) + apply (fastforce intro: cond_hoarep simp: conseq_under_new_pre) apply (fastforce intro!: hoarep_conj_lift_pre_fix simp: Collect_mono conseq_under_new_pre) - 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) apply (rule hoarep_conj_lift_pre_fix) apply (simp add: Collect_mono conseq_under_new_pre) @@ -1184,65 +1105,78 @@ proof - in conseqPost[rotated]) apply fastforce apply fastforce - apply (simp add: Collect_mono conseq_under_new_pre) + apply (simp add: Collect_mono conseq_under_new_pre to_bool_def) done - have cond_inv_guard: - "\r s. \ \ {s'. s' \ G' \ (s, s') \ srel \ G r s \ rrel r (xf s')} - cond - {s'. s' \ G' \ (cond_xf s' \ 0 \ s' \ C')}" - by (fastforce intro: conseqPost cond_hoarep) + have loop_body_to_Normal: + "\r s s' xstate. + \\ \ \B';; cond, Normal s'\ \ xstate; (s, s') \ srel; rrel r (xf s'); G r s; s' \ G'; + s' \ C'; the (C r s); \ snd (whileLoop (\r s. the (C r s)) B r s)\ + \ isNormal xstate" + apply (frule intermediate_Normal_state) + apply (rule hoarep_conj_lift[where Q'="\s. s \ G'"]) + apply (fastforce intro: ccorres_to_vcg_with_prop' body_ccorres abs_body_inv) + apply (fastforce intro: conc_body_inv) + apply (insert no_ofail) + apply (fastforce dest: snd_whileLoop_first_step simp: no_ofail_def) + apply (fastforce intro: cond_hoarep dest!: hoarep_exec[rotated, where c=cond]) + done - show ?thesis - apply (clarsimp simp: ccorres_underlying_def) - apply (rename_tac s s' n xstate) - 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 cond_hoarep') - apply (rule conseqPre) - apply (rule ccorres_While_Normal_helper) - apply (fastforce intro!: cond_hoarep' hoarep_ex_lift) - apply (intro hoarep_ex_pre, rename_tac rv new_s) - 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] - 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) + have helper: + "\s' xstate'. + \ \ \While {s'. cond_xf s' \ 0} (B';; cond), Normal s'\ \ xstate' \ + \r s. ((s, s') \ srel \ (C r s \ None) \ (cond_xf s' \ 0) = the (C r s) + \ rrel r (xf s') \ G r s \ s' \ G' \ (cond_xf s' \ 0 \ s' \ C') + \ \ snd (whileLoop (\r s. the (C r s)) B r s)) + \ (\t'. Normal t' = xstate' + \ (\rv s'. (rv, s') \ fst (whileLoop (\r s. the (C r s)) B r s) + \ (s', t') \ srel \ rrel rv (xf t')))" + apply (erule exec_While_final_inv''; simp) + apply (fastforce simp: whileLoop_cond_fail return_def) + apply (find_goal \match premises in \\ \ \B';; cond, Normal t\ \ Normal _\ for t \ \-\\) + defer + apply (fastforce dest: loop_body_to_Normal) + apply (fastforce dest: loop_body_to_Normal) + apply (fastforce dest: loop_body_to_Normal) + apply clarsimp + apply (frule loop_body_to_Normal; simp) + apply (rename_tac t t' t'' r s y) + apply (frule snd_whileLoop_first_step) apply fastforce - apply (case_tac xstate; clarsimp) - apply (frule intermediate_Normal_state[OF _ _ cond_hoarep]; assumption?) + apply (frule intermediate_Normal_state[OF _ conc_body_inv]) apply fastforce apply clarsimp apply (rename_tac inter_t) - apply (insert cond_ccorres) + apply (insert body_ccorres) apply (drule_tac x=r in meta_spec) - apply (drule (2) ccorresE_gets_the) + apply (drule_tac s=s in ccorres_to_vcg_with_prop') + apply (fastforce dest: use_valid intro: abs_body_inv) + apply (frule hoarep_exec[rotated, where c=B']) + apply fastforce + apply (fastforce dest: snd_whileLoop_first_step simp: no_fail_def) + apply clarsimp + apply (rename_tac rv' s') + apply (drule_tac x=rv' in spec) + apply (drule_tac x=s' in spec) + apply (elim impE) + apply (frule hoarep_isNormal_exec_handlers[where c=cond]) + apply fastforce + apply (frule_tac s'=inter_t in ccorresE_gets_the[OF cond_ccorres]; assumption?) 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: cond_hoarep) - 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 _ _ cond_inv_guard, rotated] no_ofailD) + apply (frule_tac s=inter_t and t="Normal t'" in hoarep_exec[OF _ _ cond_hoarep, rotated]) + apply fastforce + apply clarsimp + apply (rule conjI) + apply (insert no_ofail) + apply (fastforce simp: no_ofail_def) + apply (simp add: snd_whileLoop_unfold to_bool_def) + apply (fastforce simp: whileLoop_def intro: whileLoop_results.intros(3)) done + + show ?thesis + by (fastforce dest!: helper intermediate_Normal_state spec + intro: ccorresI_empty_handler_stack cond_hoarep') qed lemmas ccorres_While' = ccorres_While[where C'=UNIV, simplified] diff --git a/lib/clib/SIMPL_Lemmas.thy b/lib/clib/SIMPL_Lemmas.thy index 6cc9034016..e5458b886d 100644 --- a/lib/clib/SIMPL_Lemmas.thy +++ b/lib/clib/SIMPL_Lemmas.thy @@ -401,12 +401,4 @@ lemma exec_While_final_inv'': 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 3ec612d33182cbab696fc504656631712c8c962f Mon Sep 17 00:00:00 2001 From: Michael McInerney Date: Tue, 9 Jul 2024 11:26:13 +0930 Subject: [PATCH 02/15] clib: add hoarep_isNormal_exec_handlers to Corres_UL_C Signed-off-by: Michael McInerney --- lib/clib/Corres_UL_C.thy | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/lib/clib/Corres_UL_C.thy b/lib/clib/Corres_UL_C.thy index 7580326cf6..54ed39b3e6 100644 --- a/lib/clib/Corres_UL_C.thy +++ b/lib/clib/Corres_UL_C.thy @@ -64,6 +64,10 @@ lemma exec_handlers_use_hoare_nothrow_hoarep: apply (erule exec_handlers.cases; fastforce simp: isNormal_def isAbr_def) done +lemma hoarep_isNormal_exec_handlers: + "\E \ \c, Normal s'\ \ t; isNormal t\ \ E \\<^sub>h \c # hs, s'\ \ (length hs, t)" + by (fastforce dest: EHOther simp: isNormal_def) + definition unif_rrel :: "bool \ ('a \ 'b \ bool) \ ('t \ 'b) \ ('a \ 'c \ bool) \ ('t \ 'c) From a67b8c29ed6ac147e15fb3556cdd898be9904927 Mon Sep 17 00:00:00 2001 From: Michael McInerney Date: Tue, 9 Jul 2024 11:26:48 +0930 Subject: [PATCH 03/15] clib: add ccorres_empty_handler_stackI to Corres_UL_C Signed-off-by: Michael McInerney --- lib/clib/CCorresLemmas.thy | 2 +- lib/clib/Corres_UL_C.thy | 12 ++++++++++++ 2 files changed, 13 insertions(+), 1 deletion(-) diff --git a/lib/clib/CCorresLemmas.thy b/lib/clib/CCorresLemmas.thy index ad366fda3d..4435f9a3e5 100644 --- a/lib/clib/CCorresLemmas.thy +++ b/lib/clib/CCorresLemmas.thy @@ -1176,7 +1176,7 @@ proof - show ?thesis by (fastforce dest!: helper intermediate_Normal_state spec - intro: ccorresI_empty_handler_stack cond_hoarep') + intro: ccorres_empty_handler_stackI cond_hoarep') qed lemmas ccorres_While' = ccorres_While[where C'=UNIV, simplified] diff --git a/lib/clib/Corres_UL_C.thy b/lib/clib/Corres_UL_C.thy index 54ed39b3e6..f730bdc559 100644 --- a/lib/clib/Corres_UL_C.thy +++ b/lib/clib/Corres_UL_C.thy @@ -141,6 +141,18 @@ lemma ccorresI': apply simp done +text \ For proving low-level @{term ccorresG} statements where the concrete function always + returns a @{term Normal} state, and therefore, the handler stack will not be used, and can + be considered empty.\ +lemma ccorres_empty_handler_stackI: + assumes rl: + "\s s' xstate. + \(s, s') \ srel; G s; s' \ G'; \ \ \c, Normal s'\ \ xstate; \ snd (a s)\ + \ (\t'. xstate = Normal t' \ (\(r, t) \ fst (a s). (t, t') \ srel \ rrel r (xf t')))" + shows "ccorresG srel \ rrel xf G G' [] a c" + by (fastforce dest: rl elim: exec_handlers.cases + simp: ccorres_underlying_def isNormal_def isAbr_def unif_rrel_def) + text \A congruence rule for the program part of correspondence functions (prevents schematic rewriting).\ lemma ccorres_prog_only_cong: From cd2ee532485369d065ae6283d94da0c733c99b4f Mon Sep 17 00:00:00 2001 From: Michael McInerney Date: Tue, 9 Jul 2024 11:29:19 +0930 Subject: [PATCH 04/15] clib: add ccorres_to_vcg_with_prop' to Corres_UL_C Signed-off-by: Michael McInerney --- lib/clib/Corres_UL_C.thy | 14 +++++++++----- 1 file changed, 9 insertions(+), 5 deletions(-) diff --git a/lib/clib/Corres_UL_C.thy b/lib/clib/Corres_UL_C.thy index f730bdc559..15136d8d3b 100644 --- a/lib/clib/Corres_UL_C.thy +++ b/lib/clib/Corres_UL_C.thy @@ -304,18 +304,22 @@ lemma ccorres_from_vcg_nofail: apply (rule hoare_complete, simp add: HoarePartialDef.valid_def) done -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} +lemma ccorres_to_vcg_with_prop': + "\ccorres_underlying srel \ rrel xf arrel axf P P' [] a c; \P\ a \R\\ + \ \ \ {s'. P s \ \ snd (a 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 (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 (fastforce elim!: ccorresE EHOther simp: unif_rrel_simps valid_def) done +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}" + by (fastforce elim: ccorres_to_vcg_with_prop' intro: conseqPre simp: no_fail_def) + 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} From de5c910e5a1625b7d26ec928d017fa6a522b76a7 Mon Sep 17 00:00:00 2001 From: Michael McInerney Date: Tue, 9 Jul 2024 11:29:50 +0930 Subject: [PATCH 05/15] clib: strengthen intermediate_Normal_state Signed-off-by: Michael McInerney --- lib/clib/SIMPL_Lemmas.thy | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/lib/clib/SIMPL_Lemmas.thy b/lib/clib/SIMPL_Lemmas.thy index e5458b886d..3f405324a0 100644 --- a/lib/clib/SIMPL_Lemmas.thy +++ b/lib/clib/SIMPL_Lemmas.thy @@ -352,8 +352,8 @@ lemma hoarep_revert: 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''" + "\\ \ \Seq c\<^sub>1 c\<^sub>2, Normal t\ \ t''; \ \ P c\<^sub>1 Q; t \ P\ + \ \t'. \ \ \c\<^sub>1, Normal t\ \ Normal t' \ t' \ Q \ \ \ \c\<^sub>2, Normal t'\ \ t''" apply (erule exec_Normal_elim_cases(8)) apply (insert hoarep_exec) apply fastforce From 06c389fea56700d776ceba451cdf508fc980043c Mon Sep 17 00:00:00 2001 From: Michael McInerney Date: Tue, 9 Jul 2024 11:30:14 +0930 Subject: [PATCH 06/15] clib: add hoarep_conj_lift Signed-off-by: Michael McInerney --- lib/clib/SIMPL_Lemmas.thy | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/lib/clib/SIMPL_Lemmas.thy b/lib/clib/SIMPL_Lemmas.thy index 3f405324a0..f5660ea441 100644 --- a/lib/clib/SIMPL_Lemmas.thy +++ b/lib/clib/SIMPL_Lemmas.thy @@ -378,9 +378,9 @@ lemma hoarep_ex_lift: 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}" +lemma hoarep_conj_lift: + "\\ \ P c {s. Q s}; \ \ P' c {s. Q' s}\ + \ \ \ (P \ 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"]) @@ -388,6 +388,8 @@ lemma hoarep_conj_lift_pre_fix: apply fastforce done +lemmas hoarep_conj_lift_pre_fix = hoarep_conj_lift[where P=P and P'=P for P, simplified] + lemma exec_While_final_inv'': "\ \ \ \b, x\ \ s'; b = While C B; x = Normal s; \s. s \ C \ I s (Normal s); From b7f616798d1144e1b5791da1e12a5bfbfe39d296 Mon Sep 17 00:00:00 2001 From: Michael McInerney Date: Tue, 9 Jul 2024 16:54:27 +0930 Subject: [PATCH 07/15] clib: add ccorres_assert2_abs Signed-off-by: Michael McInerney --- lib/clib/CCorresLemmas.thy | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/lib/clib/CCorresLemmas.thy b/lib/clib/CCorresLemmas.thy index 4435f9a3e5..5f5c4af6ae 100644 --- a/lib/clib/CCorresLemmas.thy +++ b/lib/clib/CCorresLemmas.thy @@ -586,6 +586,13 @@ lemma ccorres_assert2: (\s. P \ G s) {s. P \ s \ G'} hs (assert P >>= f) c" by (cases P, simp_all add: ccorres_fail') +(* This variant only propagates the assertion into the abstract side, to aid with schematic + matching on the concrete side. *) +lemma ccorres_assert2_abs: + "\ P \ ccorres_underlying sr Gamm r xf arrel axf G G' hs (f ()) c \ + \ ccorres_underlying sr Gamm r xf arrel axf (\s. P \ G s) G' hs (assert P >>= f) c" + by (cases P, simp_all add: ccorres_fail') + (* ccorres_assertE throws away the assert completely; this version provides more info *) (* FIXME: make this ccorres_assertE, and weaker ccorres_assertE into ccorres_assertE_weak, then re-examine situation with ccorres_assert and ccorres_assert2*) From da3ebe5a20fda7ddcefbaf47c675bafa041272d6 Mon Sep 17 00:00:00 2001 From: Michael McInerney Date: Tue, 9 Jul 2024 16:55:07 +0930 Subject: [PATCH 08/15] lib: add more schematics to corres_symb_exec_r_conj_ex_abs This helps to reduce dependence between the schematics used in the assumptions, and allows for easier wp reasoning. Signed-off-by: Michael McInerney --- lib/ExtraCorres.thy | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/lib/ExtraCorres.thy b/lib/ExtraCorres.thy index e110cf5a09..32e4cc8485 100644 --- a/lib/ExtraCorres.thy +++ b/lib/ExtraCorres.thy @@ -356,11 +356,11 @@ lemma corres_noop_ex_abs: lemma corres_symb_exec_r_conj_ex_abs: assumes z: "\rv. corres_underlying sr nf nf' r Q (R' rv) x (y rv)" assumes y: "\Q'\ m \R'\" - assumes x: "\s. Q s \ \\s'. (s, s') \ sr \ P' s'\ m \\rv s'. (s, s') \ sr\" - assumes nf: "nf' \ no_fail (P' and ex_abs_underlying sr Q) m" - shows "corres_underlying sr nf nf' r Q (P' and Q') x (m >>= (\rv. y rv))" + assumes x: "\s. P s \ \\s'. (s, s') \ sr \ P' s'\ m \\rv s'. (s, s') \ sr\" + assumes nf: "nf' \ no_fail (P' and ex_abs_underlying sr P) m" + shows "corres_underlying sr nf nf' r (P and Q) (P' and Q') x (m >>= (\rv. y rv))" proof - - have P: "corres_underlying sr nf nf' dc Q P' (return undefined) m" + have P: "corres_underlying sr nf nf' dc P P' (return undefined) m" apply (rule corres_noop_ex_abs) apply (simp add: x) apply (erule nf) From 5c2cb63f6580a36dc08a254fe82b3c00b2357a1d Mon Sep 17 00:00:00 2001 From: Michael McInerney Date: Tue, 9 Jul 2024 16:59:14 +0930 Subject: [PATCH 09/15] monads/nondet: add gets_the_Some_get Signed-off-by: Michael McInerney --- lib/Monads/nondet/Nondet_Reader_Option.thy | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/lib/Monads/nondet/Nondet_Reader_Option.thy b/lib/Monads/nondet/Nondet_Reader_Option.thy index 918884bcd1..5a2dc85077 100644 --- a/lib/Monads/nondet/Nondet_Reader_Option.thy +++ b/lib/Monads/nondet/Nondet_Reader_Option.thy @@ -70,6 +70,10 @@ lemma gets_the_obind: "gets_the (f |>> g) = gets_the f >>= (\x. gets_the (g x))" by (rule ext) (simp add: monad_simps obind_def split: option.splits) +lemma gets_the_Some_get[simp]: + "gets_the Some = get" + by (clarsimp simp: gets_the_def gets_def assert_opt_Some) + lemma gets_the_return: "gets_the (oreturn x) = return x" by (simp add: monad_simps oreturn_def) From f727f5b4539095b7b79e0d56e8513b78c767b172 Mon Sep 17 00:00:00 2001 From: Michael McInerney Date: Tue, 9 Jul 2024 16:59:38 +0930 Subject: [PATCH 10/15] monads/reader_option: add ask_wp Signed-off-by: Michael McInerney --- lib/Monads/reader_option/Reader_Option_VCG.thy | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/lib/Monads/reader_option/Reader_Option_VCG.thy b/lib/Monads/reader_option/Reader_Option_VCG.thy index 512b271222..9463a53117 100644 --- a/lib/Monads/reader_option/Reader_Option_VCG.thy +++ b/lib/Monads/reader_option/Reader_Option_VCG.thy @@ -83,6 +83,10 @@ lemma ofail_wp[wp]: "ovalid (\_. True) ofail Q" by (simp add: ovalid_def ofail_def) +lemma ask_wp[wp]: + "\\s. P s s\ ask \P\" + by (clarsimp simp: ovalid_def) + lemma asks_wp[wp]: "ovalid (\s. P (f s) s) (asks f) P" by (simp add: split_def asks_def oreturn_def obind_def ovalid_def) From 5d301b25f227f24b6193e8723278b8733dabaf04 Mon Sep 17 00:00:00 2001 From: Michael McInerney Date: Tue, 9 Jul 2024 17:00:07 +0930 Subject: [PATCH 11/15] monads/reader_option: add no_ofail_ask Signed-off-by: Michael McInerney --- lib/Monads/reader_option/Reader_Option_VCG.thy | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/lib/Monads/reader_option/Reader_Option_VCG.thy b/lib/Monads/reader_option/Reader_Option_VCG.thy index 9463a53117..d047236615 100644 --- a/lib/Monads/reader_option/Reader_Option_VCG.thy +++ b/lib/Monads/reader_option/Reader_Option_VCG.thy @@ -250,6 +250,10 @@ lemma no_ofail_ofail[wp]: "no_ofail \ ofail" by (simp add: no_ofail_def) +lemma no_ofail_ask[wp]: + "no_ofail \ ask" + by (simp add: no_ofail_def) + lemma no_ofail_asks_simp[simp]: "no_ofail P (asks f)" unfolding asks_def oreturn_def obind_def no_ofail_def From 98d8daf90d92c323c832840d4391e2c80319d0b3 Mon Sep 17 00:00:00 2001 From: Michael McInerney Date: Tue, 9 Jul 2024 17:01:57 +0930 Subject: [PATCH 12/15] monads/reader_option: add ostate_assert This adds ostate_assert and ohaskell_state_assert, which are versions of state_assert/stateAssert for the reader monad. Also adds several rules for basic reasoning about these functions. Signed-off-by: Michael McInerney --- lib/HaskellLib_H.thy | 5 +- lib/Monads/nondet/Nondet_Reader_Option.thy | 5 ++ .../reader_option/Reader_Option_Monad.thy | 3 ++ .../reader_option/Reader_Option_VCG.thy | 49 ++++++++++++------- 4 files changed, 44 insertions(+), 18 deletions(-) diff --git a/lib/HaskellLib_H.thy b/lib/HaskellLib_H.thy index 1a0111b3bf..2e68307692 100644 --- a/lib/HaskellLib_H.thy +++ b/lib/HaskellLib_H.thy @@ -565,6 +565,9 @@ lemma gets_the_ohaskell_assert: "gets_the (ohaskell_assert P []) = assert P" by (clarsimp simp: ohaskell_assert_def split: if_splits) -lemmas omonad_defs = omonad_defs ohaskell_assert_def ohaskell_fail_def +definition ohaskell_state_assert :: "('s \ bool) \ unit list \ ('s, unit) lookup" where + "ohaskell_state_assert P L \ ostate_assert P" + +lemmas omonad_defs = omonad_defs ohaskell_assert_def ohaskell_state_assert_def ohaskell_fail_def end diff --git a/lib/Monads/nondet/Nondet_Reader_Option.thy b/lib/Monads/nondet/Nondet_Reader_Option.thy index 5a2dc85077..7e5b471f12 100644 --- a/lib/Monads/nondet/Nondet_Reader_Option.thy +++ b/lib/Monads/nondet/Nondet_Reader_Option.thy @@ -98,6 +98,11 @@ lemma gets_the_assert: "gets_the (oassert P) = assert P" by (simp add: oassert_def assert_def gets_the_fail gets_the_return) +lemma gets_the_ostate_assert: + "gets_the (ostate_assert P) = state_assert P" + by (clarsimp simp: ostate_assert_def state_assert_def gets_the_Some_get gets_the_obind + gets_the_assert) + lemma gets_the_assert_opt: "gets_the (oassert_opt P) = assert_opt P" by (simp add: oassert_opt_def assert_opt_def gets_the_return gets_the_fail split: option.splits) diff --git a/lib/Monads/reader_option/Reader_Option_Monad.thy b/lib/Monads/reader_option/Reader_Option_Monad.thy index 686dd1d626..cf03b2c3b2 100644 --- a/lib/Monads/reader_option/Reader_Option_Monad.thy +++ b/lib/Monads/reader_option/Reader_Option_Monad.thy @@ -216,6 +216,9 @@ definition oassert :: "bool \ ('s, unit) lookup" where definition oassert_opt :: "'a option \ ('s, 'a) lookup" where "oassert_opt r \ case r of None \ ofail | Some x \ oreturn x" +definition ostate_assert :: "('s \ bool) \ ('s, unit) lookup" where + "ostate_assert P \ do { s \ Some; oassert (P s)}" + definition oapply :: "'a \ ('a \ 'b option) \ 'b option" where "oapply x \ \s. s x" diff --git a/lib/Monads/reader_option/Reader_Option_VCG.thy b/lib/Monads/reader_option/Reader_Option_VCG.thy index d047236615..770ec119d4 100644 --- a/lib/Monads/reader_option/Reader_Option_VCG.thy +++ b/lib/Monads/reader_option/Reader_Option_VCG.thy @@ -58,6 +58,19 @@ lemmas owhile_add_inv = owhile_inv_def[symmetric] (* WP rules for ovalid. *) + +lemma ovalid_wp_comb1[wp_comb]: + "\ ovalid P' f Q; ovalid P f Q'; \s. P s \ P' s \ \ ovalid P f (\r s. Q r s \ Q' r s)" + by (simp add: ovalid_def) + +lemma ovalid_wp_comb2[wp_comb]: + "\ ovalid P f Q; \s. P' s \ P s \ \ ovalid P' f Q" + by (auto simp: ovalid_def) + +lemma ovalid_wp_comb3[wp_comb]: + "\ ovalid P f Q; ovalid P' f Q' \ \ ovalid (\s. P s \ P' s) f (\r s. Q r s \ Q' r s)" + by (auto simp: ovalid_def) + lemma ovalid_post_taut[wp]: "\P\ f \\\\" by (simp add: ovalid_def) @@ -102,6 +115,15 @@ lemma oassert_wp[wp]: apply (intro conjI; wpsimp) done +lemma ostate_assert_wp: + "\\s. f s \ P () s\ ostate_assert f \P\" + unfolding ostate_assert_def + by (wpsimp wp: ask_wp) + +lemma ostate_assert_sp: + "\P\ ostate_assert Q \\_ s. P s \ Q s\" + by (wpsimp wp: ostate_assert_wp ovalid_wp_comb2) + lemma ogets_wp[wp]: "ovalid (\s. P (f s) s) (ogets f) P" by wp @@ -150,19 +172,6 @@ lemma ovalid_is_triple[wp_trip]: by (auto simp: triple_judgement_def ovalid_def ovalid_property_def) -lemma ovalid_wp_comb1[wp_comb]: - "\ ovalid P' f Q; ovalid P f Q'; \s. P s \ P' s \ \ ovalid P f (\r s. Q r s \ Q' r s)" - by (simp add: ovalid_def) - -lemma ovalid_wp_comb2[wp_comb]: - "\ ovalid P f Q; \s. P' s \ P s \ \ ovalid P' f Q" - by (auto simp: ovalid_def) - -lemma ovalid_wp_comb3[wp_comb]: - "\ ovalid P f Q; ovalid P' f Q' \ \ ovalid (\s. P s \ P' s) f (\r s. Q r s \ Q' r s)" - by (auto simp: ovalid_def) - - (* WP rules for ovalidNF. *) lemma obind_NF_wp[wp]: "\ \r. ovalidNF (R r) (g r) Q; ovalidNF P f R \ \ ovalidNF P (obind f g) Q" @@ -234,6 +243,11 @@ lemma ovalidNF_wp_comb3[wp_comb]: (* FIXME: WP rules for no_ofail, which might not be correct. *) + +lemma no_ofail_pre_imp[wp_pre]: + "\ no_ofail P f; \s. P' s \ P s \ \ no_ofail P' f" + by (simp add: no_ofail_def) + lemma no_ofailD: "\ no_ofail P m; P s \ \ \y. m s = Some y" by (simp add: no_ofail_def) @@ -309,6 +323,11 @@ lemma no_ofail_oassert[simp, wp]: "no_ofail (\_. P) (oassert P)" by (simp add: oassert_def no_ofail_def) +lemma no_ofail_ostate_assert[wp]: + "no_ofail P (ostate_assert P)" + unfolding ostate_assert_def + by wpsimp + lemma no_ofail_is_triple[wp_trip]: "no_ofail P f = triple_judgement P f (\s f. f s \ None)" by (auto simp: triple_judgement_def no_ofail_def) @@ -355,10 +374,6 @@ lemma ovalidNF_pre_imp: "\ \s. P' s \ P s; ovalidNF P f Q \ \ ovalidNF P' f Q" by (simp add: ovalidNF_def) -lemma no_ofail_pre_imp[wp_pre]: - "\ no_ofail P f; \s. P' s \ P s \ \ no_ofail P' f" - by (simp add: no_ofail_def) - lemma ovalid_post_imp: "\ \r s. Q r s \ Q' r s; ovalid P f Q \ \ ovalid P f Q'" by (simp add: ovalid_def) From 23a30df5951aae7bff64ab0c063de8f667ecd006 Mon Sep 17 00:00:00 2001 From: Michael McInerney Date: Tue, 9 Jul 2024 19:37:15 +0930 Subject: [PATCH 13/15] lib+proof: move corres_add_noop_rhs and corres_add_noop_rhs2 to Lib Moved from DRefine and CRefine, respectively Signed-off-by: Michael McInerney --- lib/Corres_UL.thy | 10 ++++++++++ proof/crefine/autocorres-test/AutoCorresTest.thy | 5 ----- proof/drefine/Arch_DR.thy | 5 ----- 3 files changed, 10 insertions(+), 10 deletions(-) diff --git a/lib/Corres_UL.thy b/lib/Corres_UL.thy index a19f6f6e59..faab18b82c 100644 --- a/lib/Corres_UL.thy +++ b/lib/Corres_UL.thy @@ -1504,6 +1504,16 @@ lemmas corres_split_noop_rhs2 lemmas corres_split_dc = corres_split[where r'=dc, simplified] +lemma corres_add_noop_rhs: + "corres_underlying sr nf nf' r P P' f (do _ \ return (); g od) + \ corres_underlying sr nf nf' r P P' f g" + by simp + +lemma corres_add_noop_rhs2: + "corres_underlying sr nf nf' r P P' f (do _ \ g; return () od) + \ corres_underlying sr nf nf' r P P' f g" + by simp + lemma isLeft_case_sum: "isLeft v \ (case v of Inl v' \ f v' | Inr v' \ g v') = f (theLeft v)" by (clarsimp split: sum.splits) diff --git a/proof/crefine/autocorres-test/AutoCorresTest.thy b/proof/crefine/autocorres-test/AutoCorresTest.thy index 01ee243362..bb83ea0a7d 100644 --- a/proof/crefine/autocorres-test/AutoCorresTest.thy +++ b/proof/crefine/autocorres-test/AutoCorresTest.thy @@ -132,11 +132,6 @@ local_setup \AutoCorresModifiesProofs.new_modifies_rules "../c/build/$L4V_ text \Extra corres_underlying rules.\ -lemma corres_add_noop_rhs2: - "corres_underlying sr nf nf' r P P' f (do _ \ g; return () od) - \ corres_underlying sr nf nf' r P P' f g" - by simp - (* Use termination (nf=True) to avoid exs_valid *) lemma corres_noop2_no_exs: assumes x: "\s. P s \ \(=) s\ f \\r. (=) s\ \ empty_fail f" diff --git a/proof/drefine/Arch_DR.thy b/proof/drefine/Arch_DR.thy index cabeb38bf0..18dd07ef2d 100644 --- a/proof/drefine/Arch_DR.thy +++ b/proof/drefine/Arch_DR.thy @@ -1082,11 +1082,6 @@ lemma pde_opt_cap_eq: apply (clarsimp simp: valid_idle_def st_tcb_at_def obj_at_def pred_tcb_at_def) done -lemma corres_add_noop_rhs: - "corres_underlying sr fl fl' r P P' f (do _ \ return (); g od) - \ corres_underlying sr fl fl' r P P' f g" - by simp - lemma gets_the_noop_dcorres: "dcorres dc (\s. f s \ None) \ (gets_the f) (return x)" by (clarsimp simp: gets_the_def corres_underlying_def exec_gets From f3375ad036ceb9a35a3dc4d22d6fa54aee16148a Mon Sep 17 00:00:00 2001 From: Michael McInerney Date: Mon, 15 Jul 2024 13:40:28 +0930 Subject: [PATCH 14/15] lib: adjust corres_symb_exec_r_conj_ex_abs_forwards This was required after a recent update to the schematics of corres_symb_exec_r_conj_ex_abs Signed-off-by: Michael McInerney --- lib/ExtraCorres.thy | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/lib/ExtraCorres.thy b/lib/ExtraCorres.thy index 32e4cc8485..ea6038825a 100644 --- a/lib/ExtraCorres.thy +++ b/lib/ExtraCorres.thy @@ -376,7 +376,7 @@ proof - qed lemmas corres_symb_exec_r_conj_ex_abs_forwards = - corres_symb_exec_r_conj_ex_abs[where P'=P' and Q'=P' for P', simplified] + corres_symb_exec_r_conj_ex_abs[where P=P and Q=P for P, where P'=P' and Q'=P' for P', simplified] lemma gets_the_corres_ex_abs': "\no_ofail P a; no_ofail (P' and ex_abs_underlying sr P) b\ \ From 19cde8ee0c255aa8471943d295afd645aaa2bed9 Mon Sep 17 00:00:00 2001 From: Michael McInerney Date: Mon, 15 Jul 2024 13:41:03 +0930 Subject: [PATCH 15/15] rt crefine: fixup after removing assumption from ccorres_While Signed-off-by: Michael McInerney --- proof/crefine/RISCV64/Finalise_C.thy | 24 +++++++++---------- proof/crefine/RISCV64/Tcb_C.thy | 35 +++++++++++++--------------- 2 files changed, 28 insertions(+), 31 deletions(-) diff --git a/proof/crefine/RISCV64/Finalise_C.thy b/proof/crefine/RISCV64/Finalise_C.thy index 6110bdc7f7..997c819bf4 100644 --- a/proof/crefine/RISCV64/Finalise_C.thy +++ b/proof/crefine/RISCV64/Finalise_C.thy @@ -716,22 +716,22 @@ lemma refill_unblock_check_ccorres: carch_state_relation_def cmachine_state_relation_def) apply ceqv apply (clarsimp simp: whileAnno_def refillHeadOverlappingLoop_def) + apply (rule ccorres_handlers_weaken) apply (rule_tac G="\_. ?abs and active_sc_at' scPtr" and G'=UNIV in ccorres_While') - apply (rule ccorres_guard_imp) - apply (ctac add: merge_overlapping_head_refill_ccorres) - apply (clarsimp simp: active_sc_at'_rewrite runReaderT_def) - apply (fastforce dest: use_ovalid[OF refillHeadOverlapping_refillSize] - intro: valid_objs'_valid_refills') - apply clarsimp - apply (clarsimp simp: runReaderT_def) apply (rule ccorres_guard_imp) - apply (ctac add: refill_head_overlapping_ccorres) - apply clarsimp + apply (ctac add: merge_overlapping_head_refill_ccorres) + apply (clarsimp simp: active_sc_at'_rewrite runReaderT_def) + apply (fastforce dest: use_ovalid[OF refillHeadOverlapping_refillSize] + intro: valid_objs'_valid_refills') apply clarsimp - apply wpsimp - apply (clarsimp simp: active_sc_at'_def) - apply (wpsimp wp: no_ofail_refillHeadOverlapping simp: runReaderT_def) + apply (clarsimp simp: runReaderT_def) + apply (rule ccorres_guard_imp) + apply (ctac add: refill_head_overlapping_ccorres) + apply clarsimp + apply clarsimp + apply wpsimp apply (clarsimp simp: active_sc_at'_def) + apply (wpsimp wp: no_ofail_refillHeadOverlapping simp: runReaderT_def) apply (wpsimp wp: updateRefillHd_valid_objs' mergeOverlappingRefills_valid_objs') apply (clarsimp simp: active_sc_at'_rewrite runReaderT_def) apply (fastforce dest: use_ovalid[OF refillHeadOverlapping_refillSize] diff --git a/proof/crefine/RISCV64/Tcb_C.thy b/proof/crefine/RISCV64/Tcb_C.thy index dd1ff4e115..3d0ab4fd0f 100644 --- a/proof/crefine/RISCV64/Tcb_C.thy +++ b/proof/crefine/RISCV64/Tcb_C.thy @@ -4967,27 +4967,24 @@ lemma find_time_after_ccorres: \ (\ptr. r = Some ptr \ (tcbInReleaseQueue |< tcbs_of' s) ptr)" and G'=UNIV in ccorres_While') - prefer 2 - apply (rule ccorres_guard_imp) - apply (ctac add: time_after_ccorres) - apply fastforce + prefer 2 + apply (rule ccorres_guard_imp) + apply (ctac add: time_after_ccorres) apply fastforce - apply (rule stronger_ccorres_guard_imp) - apply (rule ccorres_pre_getObject_tcb) - apply (rule ccorres_Guard) - apply (rule ccorres_return[where R=\]) - apply vcg - apply clarsimp - apply (erule CollectD) - apply fastforce - apply (clarsimp simp: typ_heap_simps) - apply (frule timeAfter_SomeTrueD) - apply (clarsimp simp: typ_heap_simps option_to_ctcb_ptr_def opt_pred_def opt_map_def - obj_at'_def ctcb_relation_def - split: option.splits) - apply wpsimp + apply fastforce + apply (rule stronger_ccorres_guard_imp) + apply (rule ccorres_pre_getObject_tcb) + apply (rule ccorres_Guard) + apply (rule ccorres_return[where R=\]) + apply vcg + apply clarsimp + apply (erule CollectD) + apply fastforce + apply (clarsimp simp: typ_heap_simps) apply (frule timeAfter_SomeTrueD) - apply clarsimp + apply (clarsimp simp: typ_heap_simps option_to_ctcb_ptr_def opt_pred_def opt_map_def + obj_at'_def ctcb_relation_def + split: option.splits) apply (wpsimp wp: no_ofail_timeAfter) apply (wpsimp wp: getTCB_wp) apply (frule timeAfter_SomeTrueD)