proof+autocorres: update for select_wp and alternative_wp

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

proof/access-control/ADT_AC.thy

@@ -95,7 +95,8 @@ lemma do_user_op_respects:
            apply (rule dmo_device_update_respects_Write)
           apply (wpsimp wp: dmo_um_upd_machine_state
                             dmo_user_memory_update_respects_Write
-                            hoare_vcg_all_lift hoare_vcg_imp_lift)+
+                            hoare_vcg_all_lift hoare_vcg_imp_lift
+                    wp_del: select_wp)+
           apply (rule hoare_pre_cont)
          apply (wpsimp wp: select_wp)+
   apply (simp add: restrict_map_def split: if_splits)

proof/access-control/ARM/ArchArch_AC.thy

@@ -826,8 +826,7 @@ lemma decode_arch_invocation_authorised:
   apply (rule hoare_pre)
    apply (simp add: split_def Let_def split del: if_split
               cong: cap.case_cong arch_cap.case_cong if_cong option.case_cong)
-   apply (wp select_wp whenE_throwError_wp check_vp_wpR
-             find_pd_for_asid_authority2
+   apply (wp whenE_throwError_wp check_vp_wpR find_pd_for_asid_authority2
           | wpc
           | simp add: authorised_asid_control_inv_def authorised_page_inv_def
                       authorised_page_directory_inv_def

proof/access-control/ARM/ArchCNode_AC.thy

@@ -75,7 +75,7 @@ crunches set_cdt
 
 crunches prepare_thread_delete, arch_finalise_cap
   for cur_domain[CNode_AC_assms, wp]:"\<lambda>s. P (cur_domain s)"
-  (wp: crunch_wps select_wp hoare_vcg_if_lift2 simp: unless_def)
+  (wp: crunch_wps hoare_vcg_if_lift2 simp: unless_def)
 
 lemma state_vrefs_tcb_upd[CNode_AC_assms]:
   "tcb_at t s \<Longrightarrow> state_vrefs (s\<lparr>kheap := kheap s(t \<mapsto> TCB tcb)\<rparr>) = state_vrefs s"

proof/access-control/CNode_AC.thy

@@ -1522,10 +1522,10 @@ lemma post_cap_deletion_cur_domain[wp]:
   by (wpsimp simp: post_cap_deletion_def)
 
 crunch cur_domain[wp]: cap_swap_for_delete, empty_slot "\<lambda>s. P (cur_domain s)"
-  (wp: crunch_wps select_wp hoare_vcg_if_lift2 simp: unless_def)
+  (wp: crunch_wps hoare_vcg_if_lift2 simp: unless_def)
 
 crunch cur_domain[wp]: finalise_cap "\<lambda>s. P (cur_domain s)"
-  (wp: crunch_wps select_wp hoare_vcg_if_lift2 simp: unless_def)
+  (wp: crunch_wps hoare_vcg_if_lift2 simp: unless_def)
 
 lemma rec_del_cur_domain[wp]:
   "rec_del call \<lbrace>\<lambda>s. P (cur_domain s)\<rbrace>"

proof/access-control/DomainSepInv.thy

@@ -439,7 +439,7 @@ lemma reply_cancel_ipc_domain_sep_inv[wp]:
    reply_cancel_ipc t
    \<lbrace>\<lambda>_ s. domain_sep_inv irqs  (st :: 'state_ext state) (s :: det_ext state)\<rbrace>"
   apply (simp add: reply_cancel_ipc_def)
-  apply (wp select_wp)
+  apply wp
   apply (rule hoare_strengthen_post[OF thread_set_tcb_fault_update_domain_sep_inv])
   apply auto
   done
@@ -553,7 +553,7 @@ lemma cap_revoke_domain_sep_inv':
            apply (wp drop_spec_validE[OF valid_validE[OF preemption_point_domain_sep_inv]]
                     drop_spec_validE[OF valid_validE[OF cap_delete_domain_sep_inv]]
                     drop_spec_validE[OF assertE_wp] drop_spec_validE[OF returnOk_wp]
-                    drop_spec_validE[OF liftE_wp] select_wp
+                    drop_spec_validE[OF liftE_wp]
                 | simp | wp (once) hoare_drop_imps)+
   done
 qed
@@ -1181,7 +1181,7 @@ lemma handle_event_domain_sep_inv:
 lemma schedule_domain_sep_inv:
   "(schedule :: (unit,det_ext) s_monad) \<lbrace>domain_sep_inv irqs (st :: 'state_ext state)\<rbrace>"
   apply (simp add: schedule_def allActiveTCBs_def)
-  apply (wp add: alternative_wp select_wp  guarded_switch_to_lift hoare_drop_imps
+  apply (wp add: guarded_switch_to_lift hoare_drop_imps
             del: ethread_get_wp
          | wpc | clarsimp simp: get_thread_state_def thread_get_def trans_state_update'[symmetric]
                                 schedule_choose_new_thread_def)+

proof/access-control/Finalise_AC.thy

@@ -347,7 +347,7 @@ lemma reply_cancel_ipc_pas_refined[wp]:
    \<lbrace>\<lambda>_. pas_refined aag\<rbrace>"
   apply (rule hoare_gen_asm)
   apply (simp add: reply_cancel_ipc_def)
-  apply (wp add: select_wp wp_transferable del: wp_not_transferable)
+  apply (wp add: wp_transferable del: wp_not_transferable)
    apply (rule hoare_strengthen_post[where Q="\<lambda>_. invs and tcb_at t and pas_refined aag"])
     apply (wpsimp wp: hoare_wp_combs thread_set_tcb_fault_reset_invs thread_set_pas_refined)+
    apply (frule(1) reply_cap_descends_from_master0)
@@ -368,7 +368,7 @@ crunches suspend
   for pspace_aligned[wp]: "\<lambda>s :: det_ext state. pspace_aligned s"
   and valid_vspace_objs[wp]: "\<lambda>s :: det_ext state. valid_vspace_objs s"
   and valid_arch_state[wp]: "\<lambda>s :: det_ext state. valid_arch_state s"
-  (wp: dxo_wp_weak select_wp hoare_drop_imps simp: crunch_simps)
+  (wp: dxo_wp_weak hoare_drop_imps simp: crunch_simps)
 
 crunch pas_refined[wp]: suspend "pas_refined aag"
 
@@ -528,7 +528,7 @@ lemma reply_cancel_ipc_respects[wp]:
    \<lbrace>\<lambda>_. integrity aag X st\<rbrace>"
   apply (simp add: reply_cancel_ipc_def)
   apply (rule hoare_pre)
-   apply (wp add: select_wp wp_transferable del:wp_not_transferable)
+   apply (wp add: wp_transferable del:wp_not_transferable)
    apply simp
    apply (rule hoare_lift_Pf2[where f="cdt"])
     apply (wpsimp wp: hoare_vcg_const_Ball_lift thread_set_integrity_autarch
@@ -1231,7 +1231,7 @@ proof (induct rule: cap_revoke.induct)
     apply (subst cap_revoke.simps)
     apply (unfold P_def)
      apply (wp "1.hyps"[unfolded P_def], simp+)
-           apply (wp preemption_point_inv hoare_drop_imps select_wp
+           apply (wp preemption_point_inv hoare_drop_imps
                      rec_del_preserves_cte_zombie_null_insts[where P=Q]
                   | simp add: Q_Null Q_Zombie)+
     done

proof/access-control/Ipc_AC.thy

@@ -37,7 +37,7 @@ lemma send_signal_caps_of_state[wp]:
   done
 
 crunch mdb[wp]: blocked_cancel_ipc, update_waiting_ntfn "\<lambda>s. P (cdt (s :: det_ext state))"
-  (wp: crunch_wps unless_wp select_wp dxo_wp_weak simp: crunch_simps)
+  (wp: crunch_wps unless_wp dxo_wp_weak simp: crunch_simps)
 
 lemma cancel_ipc_receive_blocked_mdb:
   "\<lbrace>\<lambda>s :: det_ext state. P (cdt s) \<and> st_tcb_at receive_blocked t s\<rbrace>

proof/access-control/RISCV64/ArchCNode_AC.thy

@@ -97,7 +97,7 @@ crunches set_cdt
 
 crunches prepare_thread_delete, arch_finalise_cap
   for cur_domain[CNode_AC_assms, wp]:"\<lambda>s. P (cur_domain s)"
-  (wp: crunch_wps select_wp hoare_vcg_if_lift2 simp: unless_def)
+  (wp: crunch_wps hoare_vcg_if_lift2 simp: unless_def)
 
 lemma state_vrefs_tcb_upd[CNode_AC_assms]:
   "\<lbrakk> pspace_aligned s; valid_vspace_objs s; valid_arch_state s; tcb_at t s \<rbrakk>

proof/access-control/Syscall_AC.thy

@@ -699,7 +699,7 @@ lemma handle_event_integrity:
                   handle_reply_respects handle_fault_integrity_autarch
                   handle_interrupt_integrity handle_vm_fault_integrity
                   handle_reply_pas_refined handle_vm_fault_valid_fault
-                  handle_reply_valid_sched alternative_wp select_wp
+                  handle_reply_valid_sched
                   hoare_vcg_conj_lift hoare_vcg_all_lift hoare_drop_imps
             simp: domain_sep_inv_def
       | rule dmo_wp hoare_vcg_E_elim
@@ -899,7 +899,7 @@ lemma schedule_integrity:
    schedule
    \<lbrace>\<lambda>_. integrity aag X st\<rbrace>"
   apply (simp add: schedule_def)
-  apply (wpsimp wp: alternative_wp switch_to_thread_respects' select_wp guarded_switch_to_lift
+  apply (wpsimp wp: switch_to_thread_respects' guarded_switch_to_lift
                     switch_to_idle_thread_respects choose_thread_respects gts_wp hoare_drop_imps
                     set_scheduler_action_cnt_valid_sched append_thread_queued enqueue_thread_queued
                     tcb_sched_action_enqueue_valid_blocked_except tcb_sched_action_append_integrity'
@@ -949,14 +949,14 @@ crunch pas_refined[wp]: choose_thread "pas_refined aag"
 lemma schedule_pas_refined:
   "schedule \<lbrace>pas_refined aag\<rbrace>"
   apply (simp add: schedule_def allActiveTCBs_def)
-  apply (wp add: alternative_wp guarded_switch_to_lift switch_to_thread_pas_refined select_wp
-                  switch_to_idle_thread_pas_refined gts_wp
-                  guarded_switch_to_lift switch_to_thread_respects_pasMayEditReadyQueues
-                  choose_thread_respects_pasMayEditReadyQueues
-                  next_domain_valid_sched next_domain_valid_queues gts_wp hoare_drop_imps
-                  set_scheduler_action_cnt_valid_sched enqueue_thread_queued
-                  tcb_sched_action_enqueue_valid_blocked_except
-             del: ethread_get_wp
+  apply (wp add: guarded_switch_to_lift switch_to_thread_pas_refined
+                 switch_to_idle_thread_pas_refined gts_wp
+                 guarded_switch_to_lift switch_to_thread_respects_pasMayEditReadyQueues
+                 choose_thread_respects_pasMayEditReadyQueues
+                 next_domain_valid_sched next_domain_valid_queues gts_wp hoare_drop_imps
+                 set_scheduler_action_cnt_valid_sched enqueue_thread_queued
+                 tcb_sched_action_enqueue_valid_blocked_except
+            del: ethread_get_wp
          | wpc | simp add: schedule_choose_new_thread_def)+
   done
 
@@ -983,7 +983,7 @@ lemma ct_active_update[simp]:
 lemma set_cap_ct_active[wp]:
   "set_cap ptr c \<lbrace>ct_active \<rbrace>"
   apply (rule hoare_pre)
-  apply (wps | wpsimp wp: select_wp sts_st_tcb_at_cases thread_set_no_change_tcb_state
+  apply (wps | wpsimp wp: sts_st_tcb_at_cases thread_set_no_change_tcb_state
                     simp: crunch_simps ct_in_state_def)+
   done
 
@@ -1034,7 +1034,7 @@ crunch ct_active[wp]: post_cap_deletion, empty_slot "\<lambda>s :: det_ext state
      wp: crunch_wps filterM_preserved unless_wp)
 
 crunch cur_thread[wp]: cap_swap_for_delete, finalise_cap "\<lambda>s :: det_ext state. P (cur_thread s)"
-  (wp: select_wp dxo_wp_weak crunch_wps simp: crunch_simps)
+  (wp: dxo_wp_weak crunch_wps simp: crunch_simps)
 
 lemma rec_del_cur_thread[wp]:
   "rec_del a \<lbrace>\<lambda>s :: det_ext state. P (cur_thread s)\<rbrace>"
@@ -1139,8 +1139,7 @@ lemma call_kernel_integrity':
   apply (simp add: call_kernel_def)
   apply (simp only: spec_valid_def)
   apply (wpsimp wp: activate_thread_respects schedule_integrity_pasMayEditReadyQueues
-                    handle_interrupt_integrity dmo_wp alternative_wp
-                    select_wp handle_interrupt_pas_refined)
+                    handle_interrupt_integrity dmo_wp handle_interrupt_pas_refined)
     apply (clarsimp simp: if_fun_split)
     apply (rule_tac Q="\<lambda>rv ms. (rv \<noteq> None \<longrightarrow> the rv \<notin> non_kernel_IRQs) \<and>
                                 R True (domain_sep_inv (pasMaySendIrqs aag) st' s) rv ms"
@@ -1182,7 +1181,7 @@ lemma call_kernel_pas_refined:
    \<lbrace>\<lambda>_. pas_refined aag\<rbrace>"
   apply (simp add: call_kernel_def )
   apply (wp activate_thread_pas_refined schedule_pas_refined handle_interrupt_pas_refined
-            do_machine_op_pas_refined dmo_wp alternative_wp select_wp hoare_drop_imps getActiveIRQ_inv
+            do_machine_op_pas_refined dmo_wp hoare_drop_imps getActiveIRQ_inv
          | simp add: if_fun_split
          | strengthen invs_psp_aligned invs_vspace_objs invs_arch_state)+
    apply (wp he_invs handle_event_pas_refined)

proof/bisim/Syscall_S.thy

@@ -699,7 +699,7 @@ lemma schedule_separate_state [wp]:
   "\<lbrace>separate_state\<rbrace> schedule :: (unit,unit) s_monad \<lbrace>\<lambda>_. separate_state\<rbrace>"
   unfolding schedule_def switch_to_thread_def arch_switch_to_thread_def
             switch_to_idle_thread_def arch_switch_to_idle_thread_def allActiveTCBs_def
-  by (wpsimp wp: select_inv separate_state_pres' alternative_wp
+  by (wpsimp wp: select_inv separate_state_pres'
              simp: arch_activate_idle_thread_def |
       strengthen imp_consequent)+
 

proof/capDL-api/Arch_DP.thy

@@ -65,9 +65,9 @@ lemma decode_page_map_intent_rv_20_24:
   \<lbrace>\<lambda>r s. R r\<rbrace>, -"
   apply (simp add: decode_invocation_def get_index_def get_page_intent_def throw_opt_def
                    cap_rights_def decode_page_invocation_def throw_on_none_def get_mapped_asid_def)
-  apply (wp alternativeE_wp select_wp | wpc)+
+  apply (wp | wpc)+
      apply (rule validE_validE_R)
-     apply (wp alternativeE_wp)
+     apply wp
      apply (simp add:cdl_page_mapping_entries_def split del:if_split | wp | wpc)+
   apply auto
   done
@@ -86,9 +86,9 @@ lemma decode_page_map_intent_rv_16_12:
     get_page_intent_def throw_opt_def cap_rights_def
     decode_page_invocation_def throw_on_none_def
     get_mapped_asid_def)
-  apply (wp alternativeE_wp select_wp)
+  apply wp
   apply (rule validE_validE_R)
-   apply (wp alternativeE_wp)
+   apply wp
     apply (simp add:cdl_page_mapping_entries_def)
     apply (wp cdl_lookup_pt_slot_rv | wpc | simp)+
    apply auto
@@ -130,13 +130,13 @@ lemma invoke_page_table_wp:
 done
 
 crunch cdl_cur_thread[wp]: invoke_page "\<lambda>s. P (cdl_current_thread s)"
-(wp: crunch_wps select_wp alternative_wp simp : swp_def )
+  (wp: crunch_wps simp: swp_def)
 
 crunch cdl_cur_thread[wp]: invoke_page_table "\<lambda>s. P (cdl_current_thread s)"
-(wp: crunch_wps select_wp alternative_wp simp : swp_def )
+  (wp: crunch_wps simp: swp_def)
 
 crunch cdl_cur_domain[wp]: invoke_page_table, invoke_page "\<lambda>s. P (cdl_current_domain s)"
-(wp: crunch_wps select_wp alternative_wp simp : swp_def unless_def)
+  (wp: crunch_wps simp: swp_def unless_def)
 
 lemmas cap_asid_simps[simp] = cap_asid_def[split_simps cdl_cap.split]
 lemmas cap_mapped_simps[simp] = cap_mapped_def[split_simps cdl_cap.split]
@@ -153,7 +153,7 @@ lemma decode_page_table_rv:
   apply (simp add:decode_invocation_def get_page_table_intent_def
     throw_opt_def decode_page_table_invocation_def)
   apply (rule hoare_pre)
-   apply (wp alternativeE_wp  throw_on_none_wp | wpc | simp)+
+   apply (wp throw_on_none_wp | wpc | simp)+
   apply (clarsimp split:option.splits simp:get_index_def cap_object_def
     cap_has_object_def get_mapped_asid_def)
   done
@@ -564,7 +564,7 @@ lemma decode_invocation_asid_pool_assign:
      decode_asid_pool_invocation_def get_index_def
      throw_opt_def throw_on_none_def)
    apply (rule validE_validE_R)
-   apply (wp alternativeE_wp select_wp)
+   apply wp
   apply (clarsimp simp:cap_object_def cap_has_object_def)
   done
 

proof/capDL-api/CNode_DP.thy

@@ -60,7 +60,7 @@ lemma invoke_cnode_insert_cdl_current_domain[wp]:
    \<lbrace>\<lambda>_ s. P (cdl_current_domain s) \<rbrace>"
   apply (simp add: invoke_cnode_def)
   apply (rule hoare_pre)
-   apply (wp alternative_wp | wpc | clarsimp)+
+   apply (wp | wpc | clarsimp)+
   done
 
 lemma invoke_cnode_move_cdl_current_domain[wp]:

proof/capDL-api/IRQ_DP.thy

@@ -46,7 +46,6 @@ lemma invoke_irq_handler_set_handler_wp:
         invoke_irq_handler (SetIrqHandler irq cap slot)
        \<lbrace>\<lambda>_. < irq \<mapsto>irq obj \<and>* (obj, 0) \<mapsto>c cap \<and>* R> \<rbrace>"
   apply (clarsimp simp: invoke_irq_handler_def, wp)
-     apply (wp alternative_wp)
       apply (wp sep_wp: insert_cap_child_wp insert_cap_sibling_wp)+
     apply (sep_wp delete_cap_simple_format[where cap=cap'])+
   apply (safe)
@@ -71,7 +70,7 @@ lemma decode_invocation_irq_ack_rv':
 decode_irq_handler_invocation cap cap_ref caps (IrqHandlerAckIntent)
 \<lbrace>P\<rbrace>, -"
   apply (clarsimp simp: decode_irq_handler_invocation_def)
-  apply (wp alternativeE_R_wp)
+  apply wp
   apply (clarsimp)
 done
 
@@ -80,7 +79,7 @@ lemma decode_invocation_irq_clear_rv':
 decode_irq_handler_invocation cap cap_ref caps (IrqHandlerClearIntent)
 \<lbrace>P\<rbrace>, -"
   apply (clarsimp simp: decode_irq_handler_invocation_def)
-  apply (wp alternativeE_R_wp)
+  apply wp
   apply (clarsimp)
 done
 
@@ -105,7 +104,7 @@ decode_irq_handler_invocation cap cap_ref caps (IrqHandlerSetEndpointIntent)
 \<lbrace>P\<rbrace>, -"
   apply (rule validE_R_gen_asm_conj)
   apply (clarsimp simp: decode_irq_handler_invocation_def)
-  apply (wp alternativeE_R_wp | wpc)+
+  apply (wp | wpc)+
     apply (clarsimp split: cdl_cap.splits, safe)
      apply ((wp throw_on_none_rv)+, clarsimp simp: get_index_def)
   apply simp
@@ -117,7 +116,7 @@ lemma decode_irq_control_issue_irq_rv:
          <\<box> (r, (unat depth)) : root_cap index \<mapsto>u cap \<and>* R> s\<rbrace>
            decode_irq_control_invocation target target_ref caps (IrqControlIssueIrqHandlerIntent irq index depth) \<lbrace>P\<rbrace>, -"
   apply (clarsimp simp: decode_irq_control_invocation_def)
-  apply (wp alternativeE_R_wp lookup_slot_for_cnode_op_rvu'[where cap=cap and r=r] throw_on_none_rv)
+  apply (wp lookup_slot_for_cnode_op_rvu'[where cap=cap and r=r] throw_on_none_rv)
   apply (clarsimp simp: get_index_def)
   apply (sep_solve)
 done