Make hoare_seq_ext and hoare_vcg_seqE wp rules

lib/Monads/nondet/Nondet_VCG.thy

@@ -487,6 +487,24 @@ lemmas hoare_vcg_precond_imp = hoare_weaken_pre (* FIXME lib: eliminate *)
 lemmas hoare_seq_ext = seq_ext[rotated]
 lemmas hoare_vcg_seqE = seqE[rotated]
 
+lemmas hoare_vcg_seqE_R = validE_validE_R[OF hoare_vcg_seqE [OF validE_R_validE validE_R_validE]]
+lemmas hoare_vcg_seqE_E = validE_validE_E[OF hoare_vcg_seqE [OF validE_E_validE]]
+
+lemma hoare_seq_extE_R:
+  "\<lbrakk>\<And>x. \<lbrace>B x\<rbrace> g x \<lbrace>Q\<rbrace>,-; \<lbrace>P\<rbrace> f \<lbrace>B\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f >>= g \<lbrace>Q\<rbrace>,-"
+  apply (clarsimp simp: validE_R_def validE_def)
+  by (wp | assumption)+
+
+lemma hoare_seq_extE_E:
+  "\<lbrakk>\<And>x. \<lbrace>B x\<rbrace> g x -,\<lbrace>E\<rbrace>; \<lbrace>P\<rbrace> f \<lbrace>B\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f >>= g -,\<lbrace>E\<rbrace>"
+  apply (clarsimp simp: validE_E_def validE_def)
+  by (wp | assumption)+
+
+lemma hoare_seq_extE:
+  "\<lbrakk>\<And>x. \<lbrace>B x\<rbrace> g x \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>; \<lbrace>P\<rbrace> f \<lbrace>B\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f >>= g \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>"
+  apply (clarsimp simp: validE_def)
+  by (wp | assumption)+
+
 lemma hoare_seq_ext_nobind:
   "\<lbrakk> \<lbrace>B\<rbrace> g \<lbrace>C\<rbrace>; \<lbrace>A\<rbrace> f \<lbrace>\<lambda>_. B\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>A\<rbrace> do f; g od \<lbrace>C\<rbrace>"
   by (erule seq_ext) (clarsimp simp: valid_def)
@@ -1066,8 +1084,7 @@ lemmas all_classic_wp_combs =
   hoare_classic_wp_combs
 
 lemmas hoare_wp_splits[wp_split] =
-  hoare_seq_ext hoare_vcg_seqE handleE'_wp handleE_wp
-  validE_validE_R [OF hoare_vcg_seqE [OF validE_R_validE]]
+  handleE'_wp handleE_wp
   validE_validE_R [OF handleE'_wp [OF validE_R_validE]]
   validE_validE_R [OF handleE_wp [OF validE_R_validE]]
   catch_wp hoare_vcg_if_split hoare_vcg_if_splitE
@@ -1078,9 +1095,20 @@ lemmas hoare_wp_splits[wp_split] =
 
 lemmas [wp_comb] = hoare_wp_state_combsE hoare_wp_combsE  hoare_wp_combs
 
+(* Add these rules to wp first to control when they are applied. We want them used last, only when
+   no other more specific wp rules apply.
+   hoare_seq_ext, hoare_vcg_seqE and their variants are wp rules instead of wp_split rules because
+   they should be used before other wp_split rules, and in combination with wp_comb rules when
+   necessary.
+   hoare_vcg_prop is unsafe in certain circumstances but still useful to have applied automatically,
+   so we make it the very last rule to be tried. *)
+lemmas [wp] =
+  hoare_vcg_prop hoare_seq_ext
+  hoare_vcg_seqE_R hoare_vcg_seqE_E hoare_vcg_seqE
+  hoare_seq_extE_R hoare_seq_extE_E hoare_seq_extE
+
 (* rules towards the bottom will be matched first *)
-lemmas [wp] = hoare_vcg_prop
-              wp_post_taut
+lemmas [wp] = wp_post_taut
               hoare_fun_app_wp
               returnOk_E
               liftE_validE_E

lib/Monads/trace/Trace_RG.thy

@@ -858,6 +858,11 @@ lemma rg_vcg_split_case_sum:
        \<lbrace>G\<rbrace>, \<lbrace>Q x\<rbrace>"
   by (cases x; simp)
 
+lemma rg_seq_extE:
+  "\<lbrakk>\<And>x. \<lbrace>B x\<rbrace>,\<lbrace>R\<rbrace> g x \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>; \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>B\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace>,\<lbrace>R\<rbrace> f >>= g \<lbrace>G\<rbrace>,\<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>"
+  apply (clarsimp simp: validIE_def)
+  by (wp | assumption)+
+
 lemma bind_twp_nobind:
   "\<lbrakk>\<lbrace>B\<rbrace>,\<lbrace>R\<rbrace> g \<lbrace>G\<rbrace>,\<lbrace>C\<rbrace>; \<lbrace>A\<rbrace>,\<lbrace>R\<rbrace> f \<lbrace>G\<rbrace>,\<lbrace>\<lambda>_. B\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>A\<rbrace>,\<lbrace>R\<rbrace> do f; g od \<lbrace>G\<rbrace>,\<lbrace>C\<rbrace>"
   by (erule bind_twp_fwd) clarsimp
@@ -1409,16 +1414,24 @@ lemmas all_rg_classic_wp_combs =
   rg_classic_wp_combs
 
 lemmas rg_wp_splits[wp_split] =
-  bind_twp bindE_twp handleE'_twp handleE_twp
+  handleE'_twp handleE_twp
   catch_twp rg_vcg_if_split rg_vcg_if_splitE
   liftM_twp liftME_twp whenE_twp unlessE_twp
   validIE_validI
 
 lemmas [wp_comb] = rg_wp_state_combsE rg_wp_combsE rg_wp_combs
 
+(* Add these rules to wp first to control when they are applied. We want them used last, only when
+   no other more specific wp rules apply.
+   bind_twp, bindE_twp and rg_seq_extE are wp rules instead of wp_split rules because
+   they should be used before other wp_split rules, and in combination with wp_comb rules when
+   necessary.
+   rg_vcg_prop is unsafe in certain circumstances but still useful to have applied automatically,
+   so we make it the very last rule to be tried. *)
+lemmas [wp] = rg_vcg_prop bind_twp bindE_twp rg_seq_extE
+
 (* rules towards the bottom will be matched first *)
-lemmas [wp] = rg_vcg_prop
-              twp_post_taut
+lemmas [wp] = twp_post_taut
               twp_post_tautE
               rg_fun_app_twp
               liftE_twp

lib/Monads/trace/Trace_VCG.thy

@@ -520,6 +520,24 @@ lemmas hoare_vcg_precond_imp = hoare_weaken_pre (* FIXME lib: eliminate *)
 lemmas hoare_seq_ext = seq_ext[rotated]
 lemmas hoare_vcg_seqE = seqE[rotated]
 
+lemmas hoare_vcg_seqE_R = validE_validE_R[OF hoare_vcg_seqE [OF validE_R_validE validE_R_validE]]
+lemmas hoare_vcg_seqE_E = validE_validE_E[OF hoare_vcg_seqE [OF validE_E_validE]]
+
+lemma hoare_seq_extE_R:
+  "\<lbrakk>\<And>x. \<lbrace>B x\<rbrace> g x \<lbrace>Q\<rbrace>,-; \<lbrace>P\<rbrace> f \<lbrace>B\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f >>= g \<lbrace>Q\<rbrace>,-"
+  apply (clarsimp simp: validE_R_def validE_def)
+  by (wp | assumption)+
+
+lemma hoare_seq_extE_E:
+  "\<lbrakk>\<And>x. \<lbrace>B x\<rbrace> g x -,\<lbrace>E\<rbrace>; \<lbrace>P\<rbrace> f \<lbrace>B\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f >>= g -,\<lbrace>E\<rbrace>"
+  apply (clarsimp simp: validE_E_def validE_def)
+  by (wp | assumption)+
+
+lemma hoare_seq_extE:
+  "\<lbrakk>\<And>x. \<lbrace>B x\<rbrace> g x \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>; \<lbrace>P\<rbrace> f \<lbrace>B\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>P\<rbrace> f >>= g \<lbrace>Q\<rbrace>,\<lbrace>E\<rbrace>"
+  apply (clarsimp simp: validE_def)
+  by (wp | assumption)+
+
 lemma hoare_seq_ext_nobind:
   "\<lbrakk> \<lbrace>B\<rbrace> g \<lbrace>C\<rbrace>; \<lbrace>A\<rbrace> f \<lbrace>\<lambda>_. B\<rbrace> \<rbrakk> \<Longrightarrow> \<lbrace>A\<rbrace> do f; g od \<lbrace>C\<rbrace>"
   by (erule seq_ext) (clarsimp simp: valid_def)
@@ -1102,7 +1120,7 @@ lemmas all_classic_wp_combs =
   hoare_classic_wp_combs
 
 lemmas hoare_wp_splits[wp_split] =
-  hoare_seq_ext hoare_vcg_seqE handleE'_wp handleE_wp
+  handleE'_wp handleE_wp
   validE_validE_R [OF hoare_vcg_seqE [OF validE_R_validE]]
   validE_validE_R [OF handleE'_wp [OF validE_R_validE]]
   validE_validE_R [OF handleE_wp [OF validE_R_validE]]
@@ -1114,9 +1132,20 @@ lemmas hoare_wp_splits[wp_split] =
 
 lemmas [wp_comb] = hoare_wp_state_combsE hoare_wp_combsE  hoare_wp_combs
 
+(* Add these rules to wp first to control when they are applied. We want them used last, only when
+   no other more specific wp rules apply.
+   hoare_seq_ext, hoare_vcg_seqE and their variants are wp rules instead of wp_split rules because
+   they should be used before other wp_split rules, and in combination with wp_comb rules when
+   necessary.
+   hoare_vcg_prop is unsafe in certain circumstances but still useful to have applied automatically,
+   so we make it the very last rule to be tried. *)
+lemmas [wp] =
+  hoare_vcg_prop hoare_seq_ext
+  hoare_vcg_seqE_R hoare_vcg_seqE_E hoare_vcg_seqE
+  hoare_seq_extE_R hoare_seq_extE_E hoare_seq_extE
+
 (* rules towards the bottom will be matched first *)
-lemmas [wp] = hoare_vcg_prop
-              wp_post_taut
+lemmas [wp] = wp_post_taut
               hoare_fun_app_wp
               returnOk_E
               liftE_validE_E

proof/access-control/ARM/ArchInterrupt_AC.thy

@@ -87,17 +87,12 @@ lemma arch_decode_irq_control_invocation_authorised[Interrupt_AC_assms]:
        (args \<noteq> [] \<longrightarrow> (pasSubject aag, Control, pasIRQAbs aag (ucast (args ! 0))) \<in> pasPolicy aag))\<rbrace>
    arch_decode_irq_control_invocation info_label args slot caps
    \<lbrace>\<lambda>x _. arch_authorised_irq_ctl_inv aag x\<rbrace>, -"
-  unfolding decode_irq_control_invocation_def arch_decode_irq_control_invocation_def
+  unfolding decode_irq_control_invocation_def arch_decode_irq_control_invocation_def Let_def
             authorised_irq_ctl_inv_def arch_authorised_irq_ctl_inv_def arch_check_irq_def
   apply (rule hoare_gen_asmE)
-  apply (rule hoare_pre)
-   apply (simp add: Let_def split del: if_split cong: if_cong)
-   apply (wp whenE_throwError_wp hoare_vcg_imp_lift hoare_drop_imps
-          | strengthen  aag_Control_owns_strg
-          | simp add: o_def del: hoare_True_E_R)+
+  apply (wpsimp wp: weak_if_wp)
   apply (cases args, simp_all)
   apply (cases caps, simp_all)
-  apply (simp add: ucast_mask_drop)
   apply (auto simp: is_cap_simps cap_auth_conferred_def
                     pas_refined_wellformed
                     pas_refined_all_auth_is_owns aag_cap_auth_def)

proof/access-control/Finalise_AC.thy

@@ -958,18 +958,11 @@ lemma rec_del_respects_CTEDelete_transferable':
    apply (wp rec_del_respects'')
    apply (solves \<open>simp\<close>)
   apply (subst rec_del.simps[abs_def])
-  apply (wp add: hoare_K_bind without_preemption_wp hoare_weak_lift_imp wp_transferable
-                 rec_del_Finalise_transferable
-            del: wp_not_transferable
-         | wpc)+
+  apply (wpsimp wp: wp_transferable hoare_weak_lift_imp)
     apply (rule hoare_post_impErr,rule rec_del_Finalise_transferable)
-     apply simp apply (elim conjE) apply simp apply simp
-   apply (wp add: hoare_K_bind without_preemption_wp hoare_weak_lift_imp wp_transferable
-                  rec_del_Finalise_transferable
-             del: wp_not_transferable
-          | wpc)+
+     apply simp apply simp
    apply (rule hoare_post_impErr,rule rec_del_Finalise_transferable)
-    apply simp apply (elim conjE) apply simp apply simp
+    apply simp apply simp
   apply (clarsimp)
   apply (frule(3) cca_to_transferable_or_subject[OF invs_valid_objs invs_mdb])
   by (safe; simp)

proof/access-control/Interrupt_AC.thy

@@ -152,17 +152,11 @@ lemma decode_irq_control_invocation_authorised [wp]:
        (args \<noteq> [] \<longrightarrow> (pasSubject aag, Control, pasIRQAbs aag (ucast (args ! 0))) \<in> pasPolicy aag))\<rbrace>
    decode_irq_control_invocation info_label args slot caps
    \<lbrace>\<lambda>x s. authorised_irq_ctl_inv aag x\<rbrace>, -"
-  unfolding decode_irq_control_invocation_def authorised_irq_ctl_inv_def
+  unfolding decode_irq_control_invocation_def authorised_irq_ctl_inv_def Let_def
   apply (rule hoare_gen_asmE)
-  apply (rule hoare_pre)
-   apply (simp add: Let_def split del: if_split cong: if_cong)
-   apply (wp arch_decode_irq_control_invocation_authorised
-             whenE_throwError_wp hoare_vcg_imp_lift hoare_drop_imps
-          | strengthen  aag_Control_owns_strg
-          | simp add: o_def del: hoare_True_E_R)+
+  apply (wpsimp wp: weak_if_wp arch_decode_irq_control_invocation_authorised simp: o_def)
   apply (cases args, simp_all)
   apply (cases caps, simp_all)
-  apply (simp add: ucast_mask_drop)
   apply (auto simp: is_cap_simps cap_auth_conferred_def
                     pas_refined_wellformed
                     pas_refined_all_auth_is_owns aag_cap_auth_def)

proof/access-control/RISCV64/ArchInterrupt_AC.thy

@@ -87,17 +87,12 @@ lemma arch_decode_irq_control_invocation_authorised[Interrupt_AC_assms]:
        (args \<noteq> [] \<longrightarrow> (pasSubject aag, Control, pasIRQAbs aag (ucast (args ! 0))) \<in> pasPolicy aag))\<rbrace>
    arch_decode_irq_control_invocation info_label args slot caps
    \<lbrace>\<lambda>x _. arch_authorised_irq_ctl_inv aag x\<rbrace>, -"
-  unfolding decode_irq_control_invocation_def arch_decode_irq_control_invocation_def
+  unfolding decode_irq_control_invocation_def arch_decode_irq_control_invocation_def Let_def
             authorised_irq_ctl_inv_def arch_authorised_irq_ctl_inv_def arch_check_irq_def
   apply (rule hoare_gen_asmE)
-  apply (rule hoare_pre)
-   apply (simp add: Let_def split del: if_split cong: if_cong)
-   apply (wp whenE_throwError_wp hoare_vcg_imp_lift hoare_drop_imps
-          | strengthen aag_Control_owns_strg
-          | simp add: o_def del: hoare_True_E_R)+
+  apply (wpsimp wp: weak_if_wp)
   apply (cases args, simp_all)
   apply (cases caps, simp_all)
-  apply (simp add: ucast_mask_drop)
   apply (auto simp: is_cap_simps cap_auth_conferred_def
                     pas_refined_wellformed
                     pas_refined_all_auth_is_owns aag_cap_auth_def)

proof/capDL-api/Invocation_DP.thy

@@ -294,7 +294,7 @@ lemma decode_invocation_nonep:
    decode_invocation cap cap_ref extra_caps intent
    \<lbrace>\<lambda>rv s. nonep_invocation rv\<rbrace>, -"
   apply (simp add: decode_invocation_def)
-  apply (wpsimp simp: o_def nonep_invocation_def simp_del: hoare_True_E_R)
+  apply (wpsimp simp: o_def nonep_invocation_def)
   apply (auto simp: ep_related_cap_def)
   done
 
@@ -578,9 +578,7 @@ lemma call_kernel_with_intent_no_fault_helper:
                 | Inr rv \<Rightarrow> Q (Inr rv) s" and Q=Q for Q, rotated])
          apply (case_tac r, simp_all)[1]
         apply (simp add: validE_def[symmetric])
-        apply (rule hoare_pre, wp)
-          apply (simp add: validE_def, (wp | simp add: validE_def[symmetric])+)
-          apply (wp handle_pending_interrupts_no_ntf_cap)
+        apply (wp handle_pending_interrupts_no_ntf_cap)
          apply (rule handle_event_syscall_no_decode_exception
                    [where cur_thread = root_tcb_id
                       and intent_op = intent_op
@@ -1071,10 +1069,7 @@ lemma call_kernel_with_intent_allow_error_helper:
                 | Inr rv \<Rightarrow> Q (Inr rv) s" and Q=Q for Q, rotated])
          apply (case_tac r, simp_all)[1]
         apply (simp add: validE_def[symmetric])
-        apply (rule hoare_pre, wp)
-          apply (simp add: validE_def, (wp | simp add: validE_def[symmetric])+)
-          apply (wp handle_pending_interrupts_no_ntf_cap)
-
+        apply (wp handle_pending_interrupts_no_ntf_cap)
          apply (rule handle_event_syscall_allow_error
                        [where cur_thread = root_tcb_id
                           and intent_op = intent_op

proof/drefine/Arch_DR.thy

@@ -963,7 +963,7 @@ next
         apply (simp add: pd_shifting_dual ucast_nat_def shiftr_20_less triple_shift_fun
                          le_shiftr linorder_not_le)
        apply (rule hoare_pre, wp, auto)[1]
-      apply (wp | simp)+
+      apply (wp weak_if_wp | simp)+
     apply (clarsimp simp: is_final_cap'_def
       is_final_cap_def split:list.splits)
     apply (simp add: liftE_bindE is_final_cap_def corres_symb_exec_in_gets

proof/drefine/Corres_D.thy

@@ -633,6 +633,7 @@ lemma dcorres_rhs_noop_above: "\<lbrakk> dcorres anyrel P P' (return ()) m; dcor
 lemmas dcorres_rhs_noop_below_True = dcorres_rhs_noop_below[OF _ _ hoare_TrueI hoare_TrueI]
 lemmas dcorres_rhs_noop_above_True = dcorres_rhs_noop_above[OF _ _ hoare_TrueI hoare_TrueI]
 
+\<comment> \<open>FIXME: remove\<close>
 declare hoare_TrueI[simp]
 
 lemma dcorres_dc_rhs_noop_below_gen:

proof/drefine/Syscall_DR.thy

@@ -1325,21 +1325,12 @@ lemma handle_invocation_corres:
           apply (simp add: not_idle_thread_def)
           apply (strengthen invs_valid_idle)
           apply wp+
-        apply (simp add:conj_comms not_idle_thread_def split_def)
+        \<comment> \<open>The following proof is quite fragile. If clarsimp is used, either on its own or as part
+            of wpsimp, then it rewrites pairs and necessary rules no longer match.\<close>
+        apply (simp add: not_idle_thread_def split_def)
         apply (wp sts_Restart_invs set_thread_state_ct_active)+
-       apply (simp add:conj_comms split_def msg_from_syscall_error_simp)
-       apply (wp | simp add:split_def)+
-      apply (rule_tac Q'="\<lambda>r s. s = s'a \<and> ex_nonz_cap_to (cur_thread s) s \<and> valid_invocation r s \<and>
-                                invocation_duplicates_valid r s"
-                      in hoare_post_imp_R)
-       apply (simp add:split_def liftE_bindE[symmetric])
-       apply (wp decode_inv_wf)
-      apply (clarsimp simp:ct_in_state_def st_tcb_at_def obj_at_def not_idle_thread_def)+
-     apply (rule wp_post_tautE)
-    apply clarsimp
-    apply wp
-       apply (simp add:split_def liftE_bindE[symmetric])
-       apply (wp | simp add: split_def liftE_bindE[symmetric])+
+       apply (simp add: split_def msg_from_syscall_error_simp)
+       apply (wp | simp add: split_def)+
       apply (rule_tac Q="\<lambda>r s. s = s'a \<and>
                                evalMonad (lookup_ipc_buffer False (cur_thread s'a)) s'a = Some r \<and>
                                cte_wp_at (Not \<circ> is_master_reply_cap) (snd x) s \<and>
@@ -1351,12 +1342,12 @@ lemma handle_invocation_corres:
                                (\<forall>r\<in>cte_refs (fst x) (interrupt_irq_node s). ex_cte_cap_wp_to \<top> r s)"
                       in hoare_strengthen_post)
        apply (wp evalMonad_wp)
-         apply (simp add: empty_when_fail_lookup_ipc_buffer  weak_det_spec_lookup_ipc_buffer)+
+         apply (simp add: empty_when_fail_lookup_ipc_buffer weak_det_spec_lookup_ipc_buffer)+
        apply wp
       apply (clarsimp simp: invs_def valid_state_def valid_pspace_def valid_idle_def st_tcb_ex_cap
                             ct_in_state_def pred_tcb_at_def not_idle_thread_def obj_at_def
                      dest!: get_tcb_SomeD)
-     apply (wp)+
+     apply wp+
     apply (clarsimp simp:invs_def valid_state_def not_idle_thread_def pred_tcb_at_def obj_at_def)
    apply simp_all
   done

proof/drefine/Tcb_DR.thy

@@ -1117,8 +1117,7 @@ lemma dcorres_tcb_update_ipc_buffer:
              apply wp
             apply wpsimp
            apply (wp when_wp)+
-          apply (rule hoare_strengthen_post[OF hoare_TrueI[where P = \<top>]],clarsimp+)
-        apply (wp wp_post_taut hoare_drop_imp get_cap_weak_wp)+
+        apply (wpsimp wp: wp_post_taut hoare_drop_imp get_cap_weak_wp simp_del: hoare_TrueI)+
       apply (clarsimp simp:conj_comms)
       apply (wp thread_set_global_refs_triv thread_set_valid_idle)
        apply (clarsimp simp:tcb_cap_cases_def)