MCS: merge master into rt

proof/invariant-abstract/ARM/ArchDetSchedAux_AI.thy

@@ -177,7 +177,7 @@ lemma perform_asid_control_invocation_bound_sc_obj_tcb_at[wp]:
 crunches perform_asid_control_invocation
   for idle_thread[wp]: "\<lambda>s. P (idle_thread s)"
   and valid_blocked[wp]: "valid_blocked"
-  (wp: static_imp_wp)
+  (wp: hoare_weak_lift_imp)
 
 crunches perform_asid_control_invocation
   for rqueues[wp]: "\<lambda>s. P (ready_queues s)"

proof/invariant-abstract/ARM/ArchKHeap_AI.thy

@@ -800,75 +800,79 @@ crunch device_state_inv: storeWord "\<lambda>ms. P (device_state ms)"
 
 (* some hyp_ref invariants *)
 
-lemma state_hyp_refs_of_ep_update: "\<And>s ep val. typ_at AEndpoint ep s \<Longrightarrow>
-       state_hyp_refs_of (s\<lparr>kheap := (kheap s)(ep \<mapsto> Endpoint val)\<rparr>) = state_hyp_refs_of s"
+lemma state_hyp_refs_of_ep_update:
+  "typ_at AEndpoint ep s \<Longrightarrow>
+   state_hyp_refs_of (s\<lparr>kheap := (kheap s)(ep \<mapsto> Endpoint val)\<rparr>) = state_hyp_refs_of s"
   apply (rule all_ext)
   apply (clarsimp simp add: ARM.state_hyp_refs_of_def obj_at_def ARM.hyp_refs_of_def)
   done
 
-lemma state_hyp_refs_of_ntfn_update: "\<And>s ep val. typ_at ANTFN ep s \<Longrightarrow>
-       state_hyp_refs_of (s\<lparr>kheap := (kheap s)(ep \<mapsto> Notification val)\<rparr>) = state_hyp_refs_of s"
+lemma state_hyp_refs_of_ntfn_update:
+  "typ_at ANTFN ep s \<Longrightarrow>
+   state_hyp_refs_of (s\<lparr>kheap := (kheap s)(ep \<mapsto> Notification val)\<rparr>) = state_hyp_refs_of s"
   apply (rule all_ext)
   apply (clarsimp simp add: ARM.state_hyp_refs_of_def obj_at_def ARM.hyp_refs_of_def)
   done
 
-lemma state_hyp_refs_of_sc_update: "\<And>s sc val n. typ_at (ASchedContext n) sc s \<Longrightarrow>
-       state_hyp_refs_of (s\<lparr>kheap := kheap s(sc \<mapsto> SchedContext val n)\<rparr>) = state_hyp_refs_of s"
+lemma state_hyp_refs_of_sc_update:
+  "typ_at (ASchedContext n) sc s \<Longrightarrow>
+   state_hyp_refs_of (s\<lparr>kheap := (kheap s)(sc \<mapsto> SchedContext val n)\<rparr>) = state_hyp_refs_of s"
   apply (rule all_ext)
   apply (clarsimp simp: ARM.state_hyp_refs_of_def obj_at_def ARM.hyp_refs_of_def
                  split: kernel_object.splits)
   done
 
-lemma state_hyp_refs_of_reply_update: "\<And>s r val. typ_at AReply r s \<Longrightarrow>
-       state_hyp_refs_of (s\<lparr>kheap := kheap s(r \<mapsto> Reply val)\<rparr>) = state_hyp_refs_of s"
+lemma state_hyp_refs_of_reply_update:
+  "typ_at AReply r s \<Longrightarrow>
+   state_hyp_refs_of (s\<lparr>kheap := (kheap s)(r \<mapsto> Reply val)\<rparr>) = state_hyp_refs_of s"
   apply (rule all_ext)
   apply (clarsimp simp add: ARM.state_hyp_refs_of_def obj_at_def ARM.hyp_refs_of_def)
   done
 
 lemma state_hyp_refs_of_tcb_bound_ntfn_update:
-       "kheap s t = Some (TCB tcb) \<Longrightarrow>
-          state_hyp_refs_of (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (tcb\<lparr>tcb_bound_notification := ntfn\<rparr>))\<rparr>)
-            = state_hyp_refs_of s"
+  "kheap s t = Some (TCB tcb) \<Longrightarrow>
+   state_hyp_refs_of (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (tcb\<lparr>tcb_bound_notification := ntfn\<rparr>))\<rparr>)
+     = state_hyp_refs_of s"
   apply (rule all_ext)
   apply (clarsimp simp add: ARM.state_hyp_refs_of_def obj_at_def split: option.splits)
   done
 
 lemma state_hyp_refs_of_tcb_sched_context_update:
-       "kheap s t = Some (TCB tcb) \<Longrightarrow>
-          state_hyp_refs_of (s\<lparr>kheap := kheap s(t \<mapsto> TCB (tcb\<lparr>tcb_sched_context := sc\<rparr>))\<rparr>)
-            = state_hyp_refs_of s"
+  "kheap s t = Some (TCB tcb) \<Longrightarrow>
+   state_hyp_refs_of (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (tcb\<lparr>tcb_sched_context := sc\<rparr>))\<rparr>)
+     = state_hyp_refs_of s"
   apply (rule all_ext)
   apply (clarsimp simp add: ARM.state_hyp_refs_of_def obj_at_def split: option.splits)
   done
 
 lemma state_hyp_refs_of_tcb_yield_to_update:
-       "kheap s t = Some (TCB tcb) \<Longrightarrow>
-          state_hyp_refs_of (s\<lparr>kheap := kheap s(t \<mapsto> TCB (tcb\<lparr>tcb_yield_to := sc\<rparr>))\<rparr>)
-            = state_hyp_refs_of s"
+  "kheap s t = Some (TCB tcb) \<Longrightarrow>
+   state_hyp_refs_of (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (tcb\<lparr>tcb_yield_to := sc\<rparr>))\<rparr>)
+     = state_hyp_refs_of s"
   apply (rule all_ext)
   apply (clarsimp simp add: ARM.state_hyp_refs_of_def obj_at_def split: option.splits)
   done
 
 lemma state_hyp_refs_of_tcb_state_update:
-       "kheap s t = Some (TCB tcb) \<Longrightarrow>
-          state_hyp_refs_of (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (tcb\<lparr>tcb_state := ts\<rparr>))\<rparr>)
-            = state_hyp_refs_of s"
+  "kheap s t = Some (TCB tcb) \<Longrightarrow>
+   state_hyp_refs_of (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (tcb\<lparr>tcb_state := ts\<rparr>))\<rparr>)
+     = state_hyp_refs_of s"
   apply (rule all_ext)
   apply (clarsimp simp add: ARM.state_hyp_refs_of_def obj_at_def split: option.splits)
   done
 
 lemma state_hyp_refs_of_tcb_domain_update:
-       "kheap s t = Some (TCB tcb) \<Longrightarrow>
-          state_hyp_refs_of (s\<lparr>kheap := kheap s(t \<mapsto> TCB (tcb\<lparr>tcb_domain := d\<rparr>))\<rparr>)
-            = state_hyp_refs_of s"
+  "kheap s t = Some (TCB tcb) \<Longrightarrow>
+   state_hyp_refs_of (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (tcb\<lparr>tcb_domain := d\<rparr>))\<rparr>)
+     = state_hyp_refs_of s"
   apply (rule all_ext)
   apply (clarsimp simp add: state_hyp_refs_of_def obj_at_def split: option.splits)
   done
 
 lemma state_hyp_refs_of_tcb_priority_update:
-       "kheap s t = Some (TCB tcb) \<Longrightarrow>
-          state_hyp_refs_of (s\<lparr>kheap := kheap s(t \<mapsto> TCB (tcb\<lparr>tcb_priority := d\<rparr>))\<rparr>)
-            = state_hyp_refs_of s"
+  "kheap s t = Some (TCB tcb) \<Longrightarrow>
+   state_hyp_refs_of (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (tcb\<lparr>tcb_priority := d\<rparr>))\<rparr>)
+     = state_hyp_refs_of s"
   apply (rule all_ext)
   apply (clarsimp simp add: state_hyp_refs_of_def obj_at_def split: option.splits)
   done

proof/invariant-abstract/ARM/ArchTcb_AI.thy

@@ -308,13 +308,13 @@ lemma install_tcb_frame_cap_invs:
    \<comment> \<open>non-exception case\<close>
    apply wpsimp
      apply (wpsimp wp: checked_insert_tcb_invs[where ref="tcb_cnode_index 2"])
-    apply (wpsimp wp: hoare_vcg_all_lift static_imp_wp
+    apply (wpsimp wp: hoare_vcg_all_lift hoare_weak_lift_imp
                       thread_set_tcb_ipc_buffer_cap_cleared_invs
                       thread_set_cte_wp_at_trivial[where Q="\<lambda>x. x", OF ball_tcb_cap_casesI]
                       thread_set_ipc_tcb_cap_valid)
    apply((wpsimp wp: cap_delete_deletes
              hoare_vcg_const_imp_lift_R hoare_vcg_all_lift_R hoare_vcg_all_lift
-             static_imp_wp static_imp_conj_wp
+             hoare_weak_lift_imp hoare_weak_lift_imp_conj
            | strengthen use_no_cap_to_obj_asid_strg
            | wp cap_delete_ep)+)[1]
   by (clarsimp simp: is_cap_simps' valid_fault_handler_def)

proof/invariant-abstract/ARM/ArchVSpaceEntries_AI.thy

@@ -1623,7 +1623,7 @@ crunch valid_pdpt[wp]: schedule_choose_new_thread "valid_pdpt_objs"
 crunch valid_pdpt[wp]: activate_thread, switch_to_thread, switch_to_idle_thread,
                        awaken "valid_pdpt_objs"
   (simp: crunch_simps
-   wp: crunch_wps alternative_valid select_wp OR_choice_weak_wp select_ext_weak_wp)
+   wp: crunch_wps OR_choice_weak_wp select_ext_weak_wp)
 
 crunch valid_pdpt[wp]: handle_call, handle_recv, handle_send, handle_yield,
  handle_interrupt, handle_vm_fault, handle_hypervisor_fault
@@ -1634,7 +1634,7 @@ crunch valid_pdpt[wp]: handle_call, handle_recv, handle_send, handle_yield,
 
 lemma schedule_valid_pdpt[wp]: "\<lbrace>valid_pdpt_objs\<rbrace> schedule :: (unit,det_ext) s_monad \<lbrace>\<lambda>_. valid_pdpt_objs\<rbrace>"
   apply (simp add: schedule_def)
-  apply (wpsimp wp: alternative_wp select_wp hoare_drop_imps)
+  apply (wpsimp wp: hoare_drop_imps)
   done
 
 crunches check_domain_time

proof/invariant-abstract/CSpace_AI.thy

@@ -233,7 +233,7 @@ lemma preemption_point_inv:
   apply (rule hoare_seq_ext_skipE, wpsimp)
   apply (rule valid_validE)
   apply (rule OR_choiceE_weak_wp)
-  apply (rule alternative_valid; (solves wpsimp)?)
+  apply (rule alternative_wp[where P=P and P'=P for P, simplified]; (solves wpsimp)?)
   apply (rule validE_valid)
   apply (rule hoare_seq_ext_skipE, solves \<open>wpsimp wp: update_time_stamp_wp\<close>)+
   apply wpsimp

proof/invariant-abstract/DetSchedDomainTime_AI.thy

@@ -253,7 +253,7 @@ crunch domain_list[wp]: maybe_donate_sc "\<lambda>s :: det_state. P (domain_list
   (wp: crunch_wps)
 
 crunch domain_list_inv[wp]: send_signal "\<lambda>s::det_state. P (domain_list s)"
-  (wp: hoare_drop_imps mapM_x_wp_inv select_wp maybeM_inv simp: crunch_simps unless_def)
+  (wp: hoare_drop_imps mapM_x_wp_inv maybeM_inv simp: crunch_simps unless_def)
 
 crunch domain_list_inv[wp]: lookup_reply,lookup_cap "\<lambda>s::det_state. P (domain_list s)"
 

proof/invariant-abstract/DetSchedInvs_AI.thy

@@ -3292,17 +3292,17 @@ lemmas tcb_ready_times_of_kh_update_indep'[simp]
 
 lemma tcb_ready_time_ep_update:
   "\<lbrakk> ep_at ref s; a_type new = AEndpoint\<rbrakk> \<Longrightarrow>
-   tcb_ready_times_of_kh (kheap s(ref \<mapsto> new)) = tcb_ready_times_of s"
+   tcb_ready_times_of_kh ((kheap s)(ref \<mapsto> new)) = tcb_ready_times_of s"
   by (clarsimp simp: obj_at_def is_ep)
 
 lemma tcb_ready_time_reply_update:
   "\<lbrakk> reply_at ref s; a_type new = AReply\<rbrakk> \<Longrightarrow>
-   tcb_ready_times_of_kh (kheap s(ref \<mapsto> new)) = tcb_ready_times_of s"
+   tcb_ready_times_of_kh ((kheap s)(ref \<mapsto> new)) = tcb_ready_times_of s"
   by (clarsimp simp: obj_at_def is_reply)
 
 lemma tcb_ready_time_ntfn_update:
   "\<lbrakk> ntfn_at ref s; a_type new = ANTFN\<rbrakk> \<Longrightarrow>
-   tcb_ready_times_of_kh (kheap s(ref \<mapsto> new)) = tcb_ready_times_of s"
+   tcb_ready_times_of_kh ((kheap s)(ref \<mapsto> new)) = tcb_ready_times_of s"
   by (clarsimp simp: obj_at_def is_ntfn)
 
 lemmas tcb_ready_time_update_indeps[simp]
@@ -3314,7 +3314,7 @@ lemmas tcb_ready_time_update_indeps'[simp]
 lemma tcb_ready_time_thread_state_update[simp]:
   assumes "kheap s tp = Some (TCB tcb)"
   assumes "tcb_sched_context tcb' = tcb_sched_context tcb"
-  shows "tcb_ready_times_of_kh (kheap s(tp \<mapsto> TCB tcb')) = tcb_ready_times_of s"
+  shows "tcb_ready_times_of_kh ((kheap s)(tp \<mapsto> TCB tcb')) = tcb_ready_times_of s"
   using assms by (simp add: fun_upd_def vs_all_heap_simps)
 
 lemmas tcb_ready_time_thread_state_update'[simp]
@@ -3326,7 +3326,7 @@ lemma tcb_ready_time_kh_tcb_sc_update:
     scopt = Some scp'; kheap s scp' = Some (SchedContext sc' n');
     r_time (refill_hd sc) = r_time (refill_hd sc') \<rbrakk> \<Longrightarrow>
    tcb_ready_times_of_kh
-            (kheap s(tp \<mapsto> TCB (tcb\<lparr>tcb_sched_context := scopt\<rparr>)))
+            ((kheap s)(tp \<mapsto> TCB (tcb\<lparr>tcb_sched_context := scopt\<rparr>)))
         = tcb_ready_times_of s"
   by (auto intro!: map_eqI
              simp: fun_upd_def vs_all_heap_simps tcb_ready_times_defs
@@ -3335,12 +3335,12 @@ lemma tcb_ready_time_kh_tcb_sc_update:
 
 lemma tcb_at_simple_type_update[iff]:
   "\<lbrakk>obj_at is_simple_type epptr s; is_simple_type ko\<rbrakk> \<Longrightarrow>
-      tcbs_of_kh (kheap s(epptr \<mapsto> ko)) = tcbs_of s"
+      tcbs_of_kh ((kheap s)(epptr \<mapsto> ko)) = tcbs_of s"
   by (rule map_eqI, auto simp add: vs_heap_simps obj_at_def)
 
 lemma sc_at_simple_type_update[iff]:
   "\<lbrakk>obj_at is_simple_type epptr s; is_simple_type ko\<rbrakk> \<Longrightarrow>
-      scs_of_kh (kheap s(epptr \<mapsto> ko)) = scs_of s"
+      scs_of_kh ((kheap s)(epptr \<mapsto> ko)) = scs_of s"
   by (rule map_eqI, auto simp add: vs_heap_simps obj_at_def)
 
 (* lifting lemmas *)
@@ -3507,7 +3507,7 @@ lemma switch_in_cur_domain_lift_pre_conj:
   apply wp_pre
    apply (rule hoare_lift_Pf_pre_conj[where f=scheduler_action, OF _ b])
    apply (rule hoare_lift_Pf_pre_conj[where f=cur_domain, OF _ c])
-   by (wpsimp simp: switch_in_cur_domain_def in_cur_domain_def wp: hoare_vcg_all_lift static_imp_wp a)+
+   by (wpsimp simp: switch_in_cur_domain_def in_cur_domain_def wp: hoare_vcg_all_lift hoare_weak_lift_imp a)+
 
 lemmas switch_in_cur_domain_lift = switch_in_cur_domain_lift_pre_conj[where R = \<top>, simplified]