proof: update for changes to nondet monad

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

proof/access-control/ARM/ArchArch_AC.thy

@@ -549,7 +549,7 @@ lemma perform_asid_control_invocation_respects:
   apply (rule hoare_pre)
    apply (wpc, simp)
    apply (wpsimp wp: set_cap_integrity_autarch cap_insert_integrity_autarch
-                     retype_region_integrity[where sz=12] static_imp_wp)
+                     retype_region_integrity[where sz=12] hoare_weak_lift_imp)
   apply (clarsimp simp: authorised_asid_control_inv_def
                         ptr_range_def page_bits_def add.commute
                         range_cover_def obj_bits_api_def default_arch_object_def
@@ -576,12 +576,12 @@ lemma perform_asid_control_invocation_pas_refined [wp]:
    \<lbrace>\<lambda>_. pas_refined aag\<rbrace>"
   apply (simp add: perform_asid_control_invocation_def)
   apply (rule hoare_pre)
-   apply (wp cap_insert_pas_refined' static_imp_wp
+   apply (wp cap_insert_pas_refined' hoare_weak_lift_imp
           | strengthen pas_refined_set_asid_strg
           | wpc
           | simp add: delete_objects_def2 fun_upd_def[symmetric])+
       apply (wp retype_region_pas_refined'[where sz=pageBits]
-                hoare_vcg_ex_lift hoare_vcg_all_lift static_imp_wp hoare_wp_combs hoare_drop_imp
+                hoare_vcg_ex_lift hoare_vcg_all_lift hoare_weak_lift_imp hoare_wp_combs hoare_drop_imp
                 retype_region_invs_extras(1)[where sz = pageBits]
                 retype_region_invs_extras(4)[where sz = pageBits]
                 retype_region_invs_extras(6)[where sz = pageBits]
@@ -591,7 +591,7 @@ lemma perform_asid_control_invocation_pas_refined [wp]:
                 max_index_upd_invs_simple max_index_upd_caps_overlap_reserved
                 hoare_vcg_ex_lift set_cap_cte_wp_at hoare_vcg_disj_lift set_free_index_valid_pspace
                 set_cap_descendants_range_in set_cap_no_overlap get_cap_wp set_cap_caps_no_overlap
-                hoare_vcg_all_lift static_imp_wp retype_region_invs_extras
+                hoare_vcg_all_lift hoare_weak_lift_imp retype_region_invs_extras
                 set_cap_pas_refined_not_transferable
              | simp add: do_machine_op_def split_def cte_wp_at_neg2 region_in_kernel_window_def)+
    apply (rename_tac frame slot parent base cap)

proof/access-control/ARM/ArchDomainSepInv.thy

@@ -49,7 +49,7 @@ lemma perform_page_invocation_domain_sep_inv:
    \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>"
   apply (rule hoare_pre)
    apply (wp mapM_wp[OF _ subset_refl] set_cap_domain_sep_inv mapM_x_wp[OF _ subset_refl]
-             perform_page_invocation_domain_sep_inv_get_cap_helper static_imp_wp
+             perform_page_invocation_domain_sep_inv_get_cap_helper hoare_weak_lift_imp
           | simp add: perform_page_invocation_def o_def | wpc)+
   apply (clarsimp simp: valid_page_inv_def)
   apply (case_tac xa, simp_all add: domain_sep_inv_cap_def is_pg_cap_def)
@@ -79,7 +79,7 @@ lemma perform_asid_control_invocation_domain_sep_inv:
   unfolding perform_asid_control_invocation_def
   apply (rule hoare_pre)
   apply (wp modify_wp cap_insert_domain_sep_inv' set_cap_domain_sep_inv
-            get_cap_domain_sep_inv_cap[where st=st] static_imp_wp
+            get_cap_domain_sep_inv_cap[where st=st] hoare_weak_lift_imp
          | wpc | simp )+
   done
 

proof/access-control/ARM/ArchTcb_AC.thy

@@ -45,7 +45,7 @@ lemma invoke_tcb_tc_respects_aag[Tcb_AC_assms]:
           | wp restart_integrity_autarch set_mcpriority_integrity_autarch
                as_user_integrity_autarch thread_set_integrity_autarch
                option_update_thread_integrity_autarch
-               opt_update_thread_valid_sched static_imp_wp
+               opt_update_thread_valid_sched hoare_weak_lift_imp
                cap_insert_integrity_autarch checked_insert_pas_refined
                cap_delete_respects' cap_delete_pas_refined'
                check_cap_inv2[where Q="\<lambda>_. integrity aag X st"]

proof/access-control/DomainSepInv.thy

@@ -336,7 +336,7 @@ lemma empty_slot_domain_sep_inv:
    \<lbrace>\<lambda>_ s. domain_sep_inv irqs (st :: 'state_ext state) (s :: det_ext state)\<rbrace>"
   unfolding empty_slot_def post_cap_deletion_def
   by (wpsimp wp: get_cap_wp set_cap_domain_sep_inv set_original_wp dxo_wp_weak
-                 static_imp_wp deleted_irq_handler_domain_sep_inv)
+                 hoare_weak_lift_imp deleted_irq_handler_domain_sep_inv)
 
 end
 
@@ -568,7 +568,7 @@ lemma cap_move_cte_wp_at_other:
    cap_move cap src_slot dest_slot
    \<lbrace>\<lambda>_. cte_wp_at P slot\<rbrace>"
   unfolding cap_move_def
-  by (wpsimp wp: set_cdt_cte_wp_at set_cap_cte_wp_at' dxo_wp_weak static_imp_wp set_original_wp)
+  by (wpsimp wp: set_cdt_cte_wp_at set_cap_cte_wp_at' dxo_wp_weak hoare_weak_lift_imp set_original_wp)
 
 lemma cte_wp_at_weak_derived_ReplyCap:
   "cte_wp_at ((=) (ReplyCap x False R)) slot s
@@ -1042,7 +1042,7 @@ lemma invoke_tcb_domain_sep_inv:
     apply (simp add: split_def cong: option.case_cong)
     apply (wp checked_cap_insert_domain_sep_inv hoare_vcg_all_lift_R hoare_vcg_all_lift
               hoare_vcg_const_imp_lift_R cap_delete_domain_sep_inv cap_delete_deletes
-              dxo_wp_weak cap_delete_valid_cap cap_delete_cte_at static_imp_wp
+              dxo_wp_weak cap_delete_valid_cap cap_delete_cte_at hoare_weak_lift_imp
            | wpc | strengthen
            | simp add: option_update_thread_def emptyable_def tcb_cap_cases_def
                        tcb_cap_valid_def tcb_at_st_tcb_at

proof/access-control/Finalise_AC.thy

@@ -533,7 +533,7 @@ lemma reply_cancel_ipc_respects[wp]:
    apply (rule hoare_lift_Pf2[where f="cdt"])
     apply (wpsimp wp: hoare_vcg_const_Ball_lift thread_set_integrity_autarch
                       thread_set_invs_trivial[OF ball_tcb_cap_casesI] thread_set_tcb_state_trivial
-                      thread_set_not_state_valid_sched static_imp_wp thread_set_cte_wp_at_trivial
+                      thread_set_not_state_valid_sched hoare_weak_lift_imp thread_set_cte_wp_at_trivial
                       thread_set_pas_refined
                 simp: ran_tcb_cap_cases)+
   apply (strengthen invs_psp_aligned invs_vspace_objs invs_arch_state, clarsimp)
@@ -799,7 +799,7 @@ proof (induct arbitrary: st rule: rec_del.induct, simp_all only: rec_del_fails)
     apply (simp only: split_def)
     apply (rule hoare_pre_spec_validE)
      apply (rule split_spec_bindE)
-      apply (wp static_imp_wp)
+      apply (wp hoare_weak_lift_imp)
      apply (rule spec_strengthen_postE)
       apply (rule spec_valid_conj_liftE1)
        apply (rule valid_validE_R, rule rec_del_valid_list, rule preemption_point_inv';
@@ -816,7 +816,7 @@ next
     apply (subst rec_del.simps)
     apply (simp only: split_def)
     apply (rule hoare_pre_spec_validE)
-     apply (wp set_cap_integrity_autarch set_cap_pas_refined_not_transferable "2.hyps" static_imp_wp)
+     apply (wp set_cap_integrity_autarch set_cap_pas_refined_not_transferable "2.hyps" hoare_weak_lift_imp)
           apply ((wp preemption_point_inv' | simp add: integrity_subjects_def pas_refined_def)+)[1]
          apply (simp(no_asm))
          apply (rule spec_strengthen_postE)
@@ -833,7 +833,7 @@ next
         apply (simp add: conj_comms)
         apply (wp set_cap_integrity_autarch  set_cap_pas_refined_not_transferable replace_cap_invs
                   final_cap_same_objrefs set_cap_cte_cap_wp_to
-                  set_cap_cte_wp_at hoare_vcg_const_Ball_lift static_imp_wp
+                  set_cap_cte_wp_at hoare_vcg_const_Ball_lift hoare_weak_lift_imp
                        | rule finalise_cap_not_reply_master
                        | simp add: in_monad)+
        apply (rule hoare_strengthen_post)
@@ -848,7 +848,7 @@ next
          apply (wp finalise_cap_invs[where slot=slot]
                    finalise_cap_replaceable[where sl=slot]
                    finalise_cap_makes_halted[where slot=slot]
-                   finalise_cap_auth' static_imp_wp)[1]
+                   finalise_cap_auth' hoare_weak_lift_imp)[1]
         apply (rule finalise_cap_cases[where slot=slot])
        apply (clarsimp simp: cte_wp_at_caps_of_state)
        apply (erule disjE)
@@ -871,7 +871,7 @@ next
   case (3 ptr bits n slot s)
   show ?case
     apply (simp add: spec_validE_def)
-    apply (wp static_imp_wp)
+    apply (wp hoare_weak_lift_imp)
     apply clarsimp
     done
 next
@@ -889,7 +889,7 @@ next
         apply (wpsimp wp: rec_del_invs)
        apply (rule "4.hyps", assumption+)
       apply (wpsimp wp: set_cap_integrity_autarch set_cap_pas_refined_not_transferable
-                        get_cap_wp static_imp_wp)+
+                        get_cap_wp hoare_weak_lift_imp)+
       apply (clarsimp simp: invs_psp_aligned invs_vspace_objs invs_arch_state
                             cte_wp_at_caps_of_state clas_no_asid cli_no_irqs aag_cap_auth_def)
       apply (drule_tac auth=auth in sta_caps, simp+)
@@ -958,13 +958,13 @@ 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 static_imp_wp wp_transferable
+  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 (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 static_imp_wp wp_transferable
+   apply (wp add: hoare_K_bind without_preemption_wp hoare_weak_lift_imp wp_transferable
                   rec_del_Finalise_transferable
              del: wp_not_transferable
           | wpc)+
@@ -1144,7 +1144,7 @@ proof (induct rule: rec_del.induct, simp_all only: rec_del_fails)
     apply (insert P_Null)
     apply (subst rec_del.simps)
     apply (simp only: split_def)
-    apply (wp static_imp_wp | simp)+
+    apply (wp hoare_weak_lift_imp | simp)+
     apply (wp empty_slot_cte_wp_at)[1]
     apply (rule spec_strengthen_postE)
     apply (rule hoare_pre_spec_validE)
@@ -1160,7 +1160,7 @@ next
     apply (subst rec_del.simps)
     apply (simp only: split_def without_preemption_def
                       rec_del_call.simps)
-    apply (wp static_imp_wp)
+    apply (wp hoare_weak_lift_imp)
     apply (wp set_cap_cte_wp_at')[1]
     apply (wp "2.hyps"[simplified without_preemption_def rec_del_call.simps])
          apply ((wp preemption_point_inv | simp)+)[1]
@@ -1172,7 +1172,7 @@ next
       apply (rule_tac Q = "\<lambda>rv' s. (slot \<noteq> p \<or> exposed \<longrightarrow> cte_wp_at P p s) \<and> P (fst rv')
                              \<and> cte_at slot s" in hoare_post_imp)
        apply (clarsimp simp: cte_wp_at_caps_of_state)
-      apply (wp static_imp_wp set_cap_cte_wp_at' finalise_cap_cte_wp_at_nullinv
+      apply (wp hoare_weak_lift_imp set_cap_cte_wp_at' finalise_cap_cte_wp_at_nullinv
                 finalise_cap_fst_ret get_cap_wp
              | simp add: is_final_cap_def)+
     apply (clarsimp simp add: P_Zombie is_cap_simps cte_wp_at_caps_of_state)+

proof/access-control/Ipc_AC.thy

@@ -31,7 +31,7 @@ lemma send_signal_caps_of_state[wp]:
   "send_signal ntfnptr badge \<lbrace>\<lambda>s. P (caps_of_state s)\<rbrace>"
   apply (clarsimp simp: send_signal_def)
   apply (rule hoare_seq_ext[OF _ get_simple_ko_sp])
-   apply (wpsimp wp: dxo_wp_weak cancel_ipc_receive_blocked_caps_of_state gts_wp static_imp_wp
+   apply (wpsimp wp: dxo_wp_weak cancel_ipc_receive_blocked_caps_of_state gts_wp hoare_weak_lift_imp
                simp: update_waiting_ntfn_def)
   apply (clarsimp simp: fun_upd_def[symmetric] st_tcb_def2)
   done
@@ -423,7 +423,7 @@ lemma send_signal_respects:
    apply (rule hoare_pre)
     apply (wp set_notification_respects[where auth=Notify]
                  as_user_set_register_respects_indirect[where ntfnptr=ntfnptr]
-                 set_thread_state_integrity' sts_st_tcb_at' static_imp_wp
+                 set_thread_state_integrity' sts_st_tcb_at' hoare_weak_lift_imp
                  cancel_ipc_receive_blocked_respects[where ntfnptr=ntfnptr]
                  gts_wp
                | wpc | simp)+
@@ -451,7 +451,7 @@ lemma send_signal_respects:
                sts_st_tcb_at' as_user_set_register_respects
                set_thread_state_pas_refined set_simple_ko_pas_refined
                set_thread_state_respects_in_signalling [where ntfnptr = ntfnptr]
-               set_ntfn_valid_objs_at hoare_vcg_disj_lift static_imp_wp
+               set_ntfn_valid_objs_at hoare_vcg_disj_lift hoare_weak_lift_imp
           | wpc
           | simp add: update_waiting_ntfn_def)+
   apply clarsimp
@@ -756,10 +756,10 @@ lemma transfer_caps_loop_presM_extended:
   apply (clarsimp simp add: Let_def split_def whenE_def
                       cong: if_cong list.case_cong split del: if_split)
   apply (rule hoare_pre)
-   apply (wp eb hoare_vcg_const_imp_lift hoare_vcg_const_Ball_lift static_imp_wp
+   apply (wp eb hoare_vcg_const_imp_lift hoare_vcg_const_Ball_lift hoare_weak_lift_imp
           | assumption | simp split del: if_split)+
       apply (rule cap_insert_assume_null)
-      apply (wp x hoare_vcg_const_Ball_lift cap_insert_cte_wp_at static_imp_wp)+
+      apply (wp x hoare_vcg_const_Ball_lift cap_insert_cte_wp_at hoare_weak_lift_imp)+
     apply (rule hoare_vcg_conj_liftE_R)
      apply (rule derive_cap_is_derived_foo')
     apply (rule_tac Q' ="\<lambda>cap' s. (vo \<longrightarrow> cap'\<noteq> NullCap \<longrightarrow>
@@ -1061,7 +1061,7 @@ lemma send_ipc_pas_refined:
                                       (pasObjectAbs aag x21, Reply, pasSubject aag) \<in> pasPolicy aag)"
                     in hoare_strengthen_post[rotated])
         apply simp
-       apply (wp set_thread_state_pas_refined do_ipc_transfer_pas_refined static_imp_wp gts_wp
+       apply (wp set_thread_state_pas_refined do_ipc_transfer_pas_refined hoare_weak_lift_imp gts_wp
               | wpc
               | simp add: hoare_if_r_and)+
    apply (wp hoare_vcg_all_lift hoare_imp_lift_something | simp add: st_tcb_at_tcb_states_of_state_eq)+
@@ -1206,7 +1206,7 @@ lemma receive_ipc_base_pas_refined:
                                   aag_has_auth_to aag Reply (hd list))"
                      in hoare_strengthen_post[rotated])
          apply (fastforce simp: pas_refined_refl)
-        apply (wp static_imp_wp do_ipc_transfer_pas_refined set_simple_ko_pas_refined
+        apply (wp hoare_weak_lift_imp do_ipc_transfer_pas_refined set_simple_ko_pas_refined
                   set_thread_state_pas_refined get_simple_ko_wp hoare_vcg_all_lift
                   hoare_vcg_imp_lift [OF set_simple_ko_get_tcb, unfolded disj_not1]
                | wpc
@@ -1365,7 +1365,7 @@ lemma do_normal_transfer_send_integrity_autarch:
   by (wpsimp wp: as_user_integrity_autarch set_message_info_integrity_autarch
                  copy_mrs_pas_refined copy_mrs_integrity_autarch transfer_caps_integrity_autarch
                  lookup_extra_caps_authorised lookup_extra_caps_length get_mi_length get_mi_valid'
-                 static_imp_wp hoare_vcg_conj_lift hoare_vcg_ball_lift lec_valid_cap')
+                 hoare_weak_lift_imp hoare_vcg_conj_lift hoare_vcg_ball_lift lec_valid_cap')
 
 
 crunch integrity_autarch: setup_caller_cap "integrity aag X st"
@@ -2365,7 +2365,7 @@ lemma send_ipc_integrity_autarch:
     apply (fastforce dest!: integrity_tcb_in_ipc_final elim!: integrity_trans)
    apply (wp setup_caller_cap_respects_in_ipc_reply
              set_thread_state_respects_in_ipc_autarch[where param_b = Inactive]
-             hoare_vcg_if_lift static_imp_wp possible_switch_to_respects_in_ipc_autarch
+             hoare_vcg_if_lift hoare_weak_lift_imp possible_switch_to_respects_in_ipc_autarch
              set_thread_state_running_respects_in_ipc do_ipc_transfer_respects_in_ipc thread_get_inv
              set_endpoint_integrity_in_ipc
           | wpc

proof/access-control/RISCV64/ArchArch_AC.thy

@@ -1237,7 +1237,7 @@ lemma perform_asid_control_invocation_respects:
   apply (wpc, simp)
    apply (wpsimp wp: set_cap_integrity_autarch cap_insert_integrity_autarch
                      asid_table_entry_update_integrity retype_region_integrity[where sz=12]
-                     static_imp_wp delete_objects_valid_vspace_objs delete_objects_valid_arch_state)
+                     hoare_weak_lift_imp delete_objects_valid_vspace_objs delete_objects_valid_arch_state)
   apply (clarsimp simp: authorised_asid_control_inv_def ptr_range_def add.commute range_cover_def
                         obj_bits_api_def default_arch_object_def pageBits_def word_bits_def)
   apply (subst is_aligned_neg_mask_eq[THEN sym], assumption)
@@ -1318,9 +1318,9 @@ lemma perform_asid_control_invocation_pas_refined:
   apply (simp add: perform_asid_control_invocation_def )
   apply wpc
    apply (rule pas_refined_asid_control_helper hoare_seq_ext hoare_K_bind)+
-         apply (wp cap_insert_pas_refined' static_imp_wp | simp)+
+         apply (wp cap_insert_pas_refined' hoare_weak_lift_imp | simp)+
       apply ((wp retype_region_pas_refined'[where sz=pageBits]
-                 hoare_vcg_ex_lift hoare_vcg_all_lift static_imp_wp hoare_wp_combs hoare_drop_imp
+                 hoare_vcg_ex_lift hoare_vcg_all_lift hoare_weak_lift_imp hoare_wp_combs hoare_drop_imp
                  retype_region_invs_extras(1)[where sz = pageBits]
                  retype_region_invs_extras(4)[where sz = pageBits]
                  retype_region_invs_extras(6)[where sz = pageBits]
@@ -1329,7 +1329,7 @@ lemma perform_asid_control_invocation_pas_refined:
                  max_index_upd_invs_simple max_index_upd_caps_overlap_reserved
                  hoare_vcg_ex_lift set_cap_cte_wp_at hoare_vcg_disj_lift set_free_index_valid_pspace
                  set_cap_descendants_range_in set_cap_no_overlap get_cap_wp set_cap_caps_no_overlap
-                 hoare_vcg_all_lift static_imp_wp retype_region_invs_extras
+                 hoare_vcg_all_lift hoare_weak_lift_imp retype_region_invs_extras
                  set_cap_pas_refined_not_transferable arch_update_cap_valid_mdb
              | simp add: do_machine_op_def region_in_kernel_window_def cte_wp_at_neg2)+)[3]
    apply (rename_tac frame slot parent base )

proof/access-control/RISCV64/ArchDomainSepInv.thy

@@ -52,7 +52,7 @@ lemma perform_page_invocation_domain_sep_inv:
    \<lbrace>\<lambda>_. domain_sep_inv irqs st\<rbrace>"
   apply (rule hoare_pre)
    apply (wp mapM_wp[OF _ subset_refl] set_cap_domain_sep_inv mapM_x_wp[OF _ subset_refl]
-             perform_page_invocation_domain_sep_inv_get_cap_helper static_imp_wp
+             perform_page_invocation_domain_sep_inv_get_cap_helper hoare_weak_lift_imp
           | simp add: perform_page_invocation_def o_def | wpc)+
   done
 
@@ -72,7 +72,7 @@ lemma perform_asid_control_invocation_domain_sep_inv:
   unfolding perform_asid_control_invocation_def
   apply (rule hoare_pre)
   apply (wp modify_wp cap_insert_domain_sep_inv' set_cap_domain_sep_inv
-            get_cap_domain_sep_inv_cap[where st=st] static_imp_wp
+            get_cap_domain_sep_inv_cap[where st=st] hoare_weak_lift_imp
          | wpc | simp )+
   done
 

proof/access-control/RISCV64/ArchTcb_AC.thy

@@ -45,7 +45,7 @@ lemma invoke_tcb_tc_respects_aag[Tcb_AC_assms]:
          | wp restart_integrity_autarch set_mcpriority_integrity_autarch
               as_user_integrity_autarch thread_set_integrity_autarch
               option_update_thread_integrity_autarch
-              opt_update_thread_valid_sched static_imp_wp
+              opt_update_thread_valid_sched hoare_weak_lift_imp
               cap_insert_integrity_autarch checked_insert_pas_refined
               cap_delete_respects' cap_delete_pas_refined'
               check_cap_inv2[where Q="\<lambda>_. integrity aag X st"]

proof/access-control/Retype_AC.thy

@@ -970,7 +970,7 @@ lemma reset_untyped_cap_valid_vspace_objs:
    \<lbrace>\<lambda>_. valid_vspace_objs\<rbrace>"
   unfolding reset_untyped_cap_def
   apply (wpsimp wp: mapME_x_inv_wp preemption_point_inv)
-      apply (wp static_imp_wp delete_objects_valid_vspace_objs)
+      apply (wp hoare_weak_lift_imp delete_objects_valid_vspace_objs)
      apply (wpsimp wp: get_cap_wp)+
   apply (cases src_slot)
   apply (auto simp: cte_wp_at_caps_of_state)
@@ -1008,7 +1008,7 @@ lemma reset_untyped_cap_valid_arch_state:
    \<lbrace>\<lambda>_. valid_arch_state\<rbrace>"
   unfolding reset_untyped_cap_def
   apply (wpsimp wp: mapME_x_inv_wp preemption_point_inv)
-      apply (wp static_imp_wp delete_objects_valid_arch_state)
+      apply (wp hoare_weak_lift_imp delete_objects_valid_arch_state)
      apply (wpsimp wp: get_cap_wp)+
   apply (cases src_slot)
   apply (auto simp: cte_wp_at_caps_of_state)