proof: update for changes to wp attributes

Signed-off-by: Corey Lewis <[email protected]>

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)

proof/infoflow/ARM/ArchRetype_IF.thy

@@ -471,30 +471,31 @@ lemma reset_untyped_cap_reads_respects_g:
         apply (frule(1) caps_of_state_valid)
         apply (clarsimp simp: valid_cap_simps cap_aligned_def field_simps
                               free_index_of_def invs_valid_global_objs)
-        apply (simp add: aligned_add_aligned is_aligned_shiftl)
-        apply (clarsimp simp: Kernel_Config.resetChunkBits_def)
+       apply (simp add: aligned_add_aligned is_aligned_shiftl)
+       apply (clarsimp simp: Kernel_Config.resetChunkBits_def)
        apply (rule hoare_pre)
         apply (wp preemption_point_inv' set_untyped_cap_invs_simple set_cap_cte_wp_at
                   set_cap_no_overlap only_timer_irq_inv_pres[where Q=\<top>, OF _ set_cap_domain_sep_inv]
+                  irq_state_independent_A_conjI
                | simp)+
         apply (strengthen empty_descendants_range_in)
-         apply (wp only_timer_irq_inv_pres[where P=\<top> and Q=\<top>] no_irq_clearMemory
-                | simp | wp (once) dmo_wp)+
-        apply (clarsimp simp: cte_wp_at_caps_of_state is_cap_simps bits_of_def)
-        apply (frule(1) caps_of_state_valid)
-        apply (clarsimp simp: valid_cap_simps cap_aligned_def field_simps free_index_of_def)
-       apply (wp | simp)+
-       apply (wp delete_objects_reads_respects_g)
-      apply (simp add: if_apply_def2)
-      apply (strengthen invs_valid_global_objs)
-      apply (wp add: delete_objects_invs_ex hoare_vcg_const_imp_lift
-                     delete_objects_pspace_no_overlap_again
-                     delete_objects_valid_arch_state
-                     only_timer_irq_inv_pres[where P=\<top> and Q=\<top>]
-                del: Untyped_AI.delete_objects_pspace_no_overlap
-             | simp)+
-     apply (rule get_cap_reads_respects_g)
-    apply (wp get_cap_wp)
+        apply (wp only_timer_irq_inv_pres[where P=\<top> and Q=\<top>] no_irq_clearMemory
+               | simp | wp (once) dmo_wp)+
+       apply (clarsimp simp: cte_wp_at_caps_of_state is_cap_simps bits_of_def)
+       apply (frule(1) caps_of_state_valid)
+       apply (clarsimp simp: valid_cap_simps cap_aligned_def field_simps free_index_of_def)
+      apply (wp | simp)+
+      apply (wp delete_objects_reads_respects_g)
+     apply (simp add: if_apply_def2)
+     apply (strengthen invs_valid_global_objs)
+     apply (wp add: delete_objects_invs_ex hoare_vcg_const_imp_lift
+                    delete_objects_pspace_no_overlap_again
+                    delete_objects_valid_arch_state
+                    only_timer_irq_inv_pres[where P=\<top> and Q=\<top>]
+               del: Untyped_AI.delete_objects_pspace_no_overlap
+            | simp)+
+    apply (rule get_cap_reads_respects_g)
+   apply (wp get_cap_wp)
   apply (clarsimp simp: cte_wp_at_caps_of_state is_cap_simps bits_of_def)
   apply (frule(1) caps_of_state_valid)
   apply (clarsimp simp: valid_cap_simps cap_aligned_def field_simps

proof/infoflow/RISCV64/ArchRetype_IF.thy

@@ -413,30 +413,31 @@ lemma reset_untyped_cap_reads_respects_g:
         apply (frule(1) caps_of_state_valid)
         apply (clarsimp simp: valid_cap_simps cap_aligned_def field_simps
                               free_index_of_def invs_valid_global_objs)
-        apply (simp add: aligned_add_aligned is_aligned_shiftl)
-        apply (clarsimp simp: Kernel_Config.resetChunkBits_def)
+       apply (simp add: aligned_add_aligned is_aligned_shiftl)
+       apply (clarsimp simp: Kernel_Config.resetChunkBits_def)
        apply (rule hoare_pre)
         apply (wp preemption_point_inv' set_untyped_cap_invs_simple set_cap_cte_wp_at
                   set_cap_no_overlap only_timer_irq_inv_pres[where Q=\<top>, OF _ set_cap_domain_sep_inv]
+                  irq_state_independent_A_conjI
                | simp)+
         apply (strengthen empty_descendants_range_in)
-         apply (wp only_timer_irq_inv_pres[where P=\<top> and Q=\<top>] no_irq_clearMemory
-                | simp | wp (once) dmo_wp)+
-        apply (clarsimp simp: cte_wp_at_caps_of_state is_cap_simps bits_of_def)
-        apply (frule(1) caps_of_state_valid)
-        apply (clarsimp simp: valid_cap_simps cap_aligned_def field_simps free_index_of_def)
-       apply (wp | simp)+
-       apply (wp delete_objects_reads_respects_g)
-      apply (simp add: if_apply_def2)
-      apply (strengthen invs_valid_global_objs)
-      apply (wp add: delete_objects_invs_ex hoare_vcg_const_imp_lift
-                     delete_objects_pspace_no_overlap_again
-                     only_timer_irq_inv_pres[where P=\<top> and Q=\<top>]
-                     delete_objects_valid_arch_state
-                del: Untyped_AI.delete_objects_pspace_no_overlap
-             | simp)+
-     apply (rule get_cap_reads_respects_g)
-    apply (wp get_cap_wp)
+        apply (wp only_timer_irq_inv_pres[where P=\<top> and Q=\<top>] no_irq_clearMemory
+               | simp | wp (once) dmo_wp)+
+       apply (clarsimp simp: cte_wp_at_caps_of_state is_cap_simps bits_of_def)
+       apply (frule(1) caps_of_state_valid)
+       apply (clarsimp simp: valid_cap_simps cap_aligned_def field_simps free_index_of_def)
+      apply (wp | simp)+
+      apply (wp delete_objects_reads_respects_g)
+     apply (simp add: if_apply_def2)
+     apply (strengthen invs_valid_global_objs)
+     apply (wp add: delete_objects_invs_ex hoare_vcg_const_imp_lift
+                    delete_objects_pspace_no_overlap_again
+                    only_timer_irq_inv_pres[where P=\<top> and Q=\<top>]
+                    delete_objects_valid_arch_state
+               del: Untyped_AI.delete_objects_pspace_no_overlap
+            | simp)+
+    apply (rule get_cap_reads_respects_g)
+   apply (wp get_cap_wp)
   apply (clarsimp simp: cte_wp_at_caps_of_state is_cap_simps bits_of_def)
   apply (frule(1) caps_of_state_valid)
   apply (clarsimp simp: valid_cap_simps cap_aligned_def field_simps

proof/refine/AARCH64/TcbAcc_R.thy

@@ -1027,20 +1027,18 @@ lemma threadSet_obj_at'_really_strongest:
   "\<lbrace>\<lambda>s. tcb_at' t s \<longrightarrow> obj_at' (\<lambda>obj. if t = t' then P (f obj) else P obj)
     t' s\<rbrace> threadSet f t \<lbrace>\<lambda>rv. obj_at' P t'\<rbrace>"
   apply (simp add: threadSet_def)
-  apply (rule hoare_wp_splits)
-   apply (rule setObject_tcb_strongest)
-  apply (simp only: imp_conv_disj)
-  apply (subst simp_thms(32)[symmetric], rule hoare_vcg_disj_lift)
-   apply (rule hoare_post_imp [where Q="\<lambda>rv s. \<not> tcb_at' t s \<and> tcb_at' t s"])
-    apply simp
-   apply (subst simp_thms(21)[symmetric], rule hoare_vcg_conj_lift)
-    apply (rule getObject_inv_tcb)
-   apply (rule hoare_strengthen_post [OF getObject_ko_at])
+  apply (wp setObject_tcb_strongest)
+   apply (subst simp_thms(32)[symmetric], rule hoare_vcg_disj_lift)
+    apply (rule hoare_post_imp [where Q="\<lambda>rv s. \<not> tcb_at' t s \<and> tcb_at' t s"])
      apply simp
-    apply (simp add: objBits_simps')
-   apply (erule obj_at'_weakenE)
-   apply simp
-  apply (cases "t = t'", simp_all)
+    apply (subst simp_thms(21)[symmetric], rule hoare_vcg_conj_lift)
+     apply (rule getObject_inv_tcb)
+    apply (rule hoare_strengthen_post [OF getObject_ko_at])
+      apply simp
+     apply (simp add: objBits_simps')
+    apply (erule obj_at'_weakenE)
+    apply simp
+   apply (cases "t = t'", simp_all)
    apply (rule OMG_getObject_tcb)
   apply wp
   done

proof/refine/AARCH64/Tcb_R.thy

@@ -1465,6 +1465,10 @@ proof -
     out_no_cap_to_trivial [OF ball_tcb_cap_casesI]
     checked_insert_no_cap_to
   note if_cong [cong] option.case_cong [cong]
+  \<comment> \<open>This proof is quite fragile and was written when hoare_seq_ext was added to the wp set later
+     in the theory dependencies, and so was matched with before alternatives. We re-add it here to
+     create a similar environment and avoid needing to rework the proof.\<close>
+  note hoare_seq_ext[wp]
   show ?thesis
     apply (simp add: invokeTCB_def liftE_bindE)
     apply (simp only: eq_commute[where a= "a"])