rt spec+proof: add sorted_ipc_queues invariant

This adds the invariant sorted_ipc_queues, which states that the ipc
queues are sorted by the priority of the TCB. More specifically,
the queues are nonincreasing with respect to the priority of the TCB.

This additionally uses the filter operation in the specification
of tcb_ep_append and tcb_ep_dequeue.

Signed-off-by: Michael McInerney <[email protected]>

proof/crefine/RISCV64/IpcCancel_C.thy

@@ -164,7 +164,8 @@ lemma ntfn_ptr_set_queue_spec:
 
 lemma cancelSignal_ccorres_helper:
   "ccorres dc xfdc (invs' and (\<lambda>s. sym_refs (state_refs_of' s))
-                    and st_tcb_at' ((=) (BlockedOnNotification ntfn)) thread and ko_at' ntfn' ntfn)
+                    and st_tcb_at' ((=) (BlockedOnNotification ntfn)) thread and ko_at' ntfn' ntfn
+                    and K (distinct (ntfnQueue (ntfnObj ntfn'))))
         UNIV
         []
         (setNotification ntfn (ntfnObj_update
@@ -2472,7 +2473,7 @@ lemma cancelSignal_ccorres[corres]:
    apply (simp only: simp_list_case_return return_bind ccorres_seq_skip)
    apply (rule ccorres_stateAssert)+
    apply (rule ccorres_pre_getNotification)
-   apply (rule ccorres_assert)
+   apply (rule ccorres_assert2)+
    apply (rule ccorres_rhs_assoc2)+
    apply (ctac (no_vcg) add: cancelSignal_ccorres_helper)
      apply (ctac add: setThreadState_ccorres)
@@ -2552,11 +2553,11 @@ lemma ep_ptr_set_queue_spec:
   oops
 
 lemma valid_ep_blockedD:
-  "\<lbrakk> valid_ep' ep s; (isSendEP ep \<or> isRecvEP ep) \<rbrakk> \<Longrightarrow> (epQueue ep) \<noteq> [] \<and> (\<forall>t\<in>set (epQueue ep). tcb_at' t s) \<and> distinct (epQueue ep)"
+  "\<lbrakk> valid_ep' ep s; isSendEP ep \<or> isRecvEP ep \<rbrakk>
+   \<Longrightarrow> epQueue ep \<noteq> [] \<and> (\<forall>t\<in>set (epQueue ep). tcb_at' t s)"
   unfolding valid_ep'_def isSendEP_def isRecvEP_def
   by (clarsimp split: endpoint.splits)
 
-
 lemma ep_to_ep_queue:
   assumes ko: "ko_at' ep' ep s"
   and     waiting: "(isSendEP ep' \<or> isRecvEP ep')"
@@ -2742,7 +2743,7 @@ lemma cancelIPC_ccorres_helper:
   "ccorres dc xfdc (invs' and (\<lambda>s. sym_refs (state_refs_of' s)) and
          st_tcb_at' (\<lambda>st. (isBlockedOnSend st \<or> isBlockedOnReceive st)
                             \<and> blockingObject st = ep) thread
-        and ko_at' ep' ep)
+        and ko_at' ep' ep and K (distinct (epQueue ep')))
         {s. epptr_' s = Ptr ep}
         []
         (setEndpoint ep (if remove1 thread (epQueue ep') = [] then Structures_H.endpoint.IdleEP

proof/crefine/RISCV64/Ipc_C.thy

@@ -4467,21 +4467,22 @@ lemma ccorres_getCTE_cte_at:
   done
 
 lemma sendIPC_dequeue_ccorres_helper:
-  "ep_ptr = Ptr ep ==>
-  ccorres (\<lambda>rv rv'. rv' = tcb_ptr_to_ctcb_ptr dest) dest___ptr_to_struct_tcb_C_'
-           (invs' and (\<lambda>s. sym_refs (state_refs_of' s))
-                  and st_tcb_at' (\<lambda>st. isBlockedOnReceive st \<and>
-                                       blockingObject st = ep) dest
-                  and ko_at' (RecvEP (dest#rest)) ep) UNIV hs
-           (setEndpoint ep $ case rest of [] \<Rightarrow> Structures_H.IdleEP
-                                        | (a#list) \<Rightarrow> Structures_H.RecvEP rest)
-        (\<acute>queue :== CALL ep_ptr_get_queue(ep_ptr);;
-         \<acute>dest___ptr_to_struct_tcb_C :== head_C \<acute>queue;;
-         \<acute>queue :== CALL tcbEPDequeue(\<acute>dest___ptr_to_struct_tcb_C,\<acute>queue);;
-         CALL ep_ptr_set_queue(ep_ptr,\<acute>queue);;
-         IF head_C \<acute>queue = Ptr 0 THEN
-             CALL endpoint_ptr_set_state(ep_ptr,scast EPState_Idle)
-         FI)"
+  "ep_ptr = Ptr ep \<Longrightarrow>
+   ccorres (\<lambda>rv rv'. rv' = tcb_ptr_to_ctcb_ptr dest) dest___ptr_to_struct_tcb_C_'
+     (invs' and (\<lambda>s. sym_refs (state_refs_of' s))
+            and st_tcb_at' (\<lambda>st. isBlockedOnReceive st \<and> blockingObject st = ep) dest
+            and ko_at' (RecvEP (dest#rest)) ep
+            and K (distinct (dest # rest)))
+     UNIV hs
+     (setEndpoint ep $ case rest of [] \<Rightarrow> Structures_H.IdleEP
+                                  | (a#list) \<Rightarrow> Structures_H.RecvEP rest)
+     (\<acute>queue :== CALL ep_ptr_get_queue(ep_ptr);;
+      \<acute>dest___ptr_to_struct_tcb_C :== head_C \<acute>queue;;
+      \<acute>queue :== CALL tcbEPDequeue(\<acute>dest___ptr_to_struct_tcb_C,\<acute>queue);;
+      CALL ep_ptr_set_queue(ep_ptr,\<acute>queue);;
+      IF head_C \<acute>queue = Ptr 0 THEN
+          CALL endpoint_ptr_set_state(ep_ptr,scast EPState_Idle)
+      FI)"
   apply (rule ccorres_from_vcg)
   apply (rule allI)
   apply (rule conseqPre, vcg)
@@ -4503,6 +4504,7 @@ lemma sendIPC_dequeue_ccorres_helper:
    apply (rule_tac x=\<sigma> in exI)
    apply (intro conjI)
        apply assumption+
+     apply fastforce
     apply (drule (2) ep_to_ep_queue)
     apply (simp add: tcb_queue_relation'_def)
    apply (clarsimp simp: typ_heap_simps cendpoint_relation_def Let_def
@@ -4852,7 +4854,7 @@ lemma sendIPC_enqueue_ccorres_helper:
                 and ko_at' (ep::Structures_H.endpoint) epptr
                 and K ((ep = IdleEP \<and> queue = [thread]) \<or>
                        (\<exists>q. ep = SendEP q \<and> thread \<notin> set q \<and>
-                            queue = q @ [thread])))
+                            queue = q @ [thread] \<and> distinct q)))
            UNIV hs
            (setEndpoint epptr (Structures_H.endpoint.SendEP queue))
            (\<acute>queue :== CALL ep_ptr_get_queue(ep_Ptr epptr);;
@@ -5379,7 +5381,7 @@ lemma receiveIPC_enqueue_ccorres_helper:
                 and ko_at' (ep::Structures_H.endpoint) epptr
                 and K ((ep = IdleEP \<and> queue = [thread]) \<or>
                        (\<exists>q. ep = RecvEP q \<and> thread \<notin> set q \<and>
-                            queue = q @ [thread])))
+                            queue = q @ [thread] \<and> distinct q)))
            UNIV hs
            (setEndpoint epptr (Structures_H.endpoint.RecvEP queue))
            (\<acute>queue :== CALL ep_ptr_get_queue(ep_Ptr epptr);;
@@ -5522,7 +5524,9 @@ lemma receiveIPC_dequeue_ccorres_helper:
            (invs' and (\<lambda>s. sym_refs (state_refs_of' s))
                   and st_tcb_at' (\<lambda>st. isBlockedOnSend st \<and>
                                        blockingObject st = ep) sender
-                  and ko_at' (SendEP (sender#rest)) ep) UNIV hs
+                  and ko_at' (SendEP (sender # rest)) ep
+                  and K (distinct (sender # rest)))
+           UNIV hs
            (setEndpoint ep (case rest of [] \<Rightarrow> Structures_H.IdleEP
                                        | (a#list) \<Rightarrow> Structures_H.SendEP rest))
         (\<acute>queue :== CALL ep_ptr_get_queue(Ptr ep);;
@@ -5553,6 +5557,7 @@ lemma receiveIPC_dequeue_ccorres_helper:
    apply (rule_tac x=\<sigma> in exI)
    apply (intro conjI)
        apply assumption+
+     apply fastforce
     apply (drule (2) ep_to_ep_queue)
     apply (simp add: tcb_queue_relation'_def)
    apply (clarsimp simp: typ_heap_simps cendpoint_relation_def Let_def
@@ -6085,7 +6090,8 @@ lemma sendSignal_dequeue_ccorres_helper:
            (invs' and (\<lambda>s. sym_refs (state_refs_of' s))
                   and st_tcb_at' ((=) (BlockedOnNotification ntfn)) dest
                   and ko_at' nTFN ntfn
-                  and K (ntfnObj nTFN = WaitingNtfn (dest # rest))) UNIV hs
+                  and K (ntfnObj nTFN = WaitingNtfn (dest # rest)) and K (distinct (dest # rest)))
+           UNIV hs
            (setNotification ntfn $ ntfnObj_update (\<lambda>_. case rest of [] \<Rightarrow> Structures_H.ntfn.IdleNtfn
                                         | (a#list) \<Rightarrow> Structures_H.ntfn.WaitingNtfn rest) nTFN)
         (\<acute>ntfn_queue :== CALL ntfn_ptr_get_queue(Ptr ntfn);;
@@ -6516,7 +6522,7 @@ lemma receiveSignal_enqueue_ccorres_helper:
                 and ko_at' (ntfn::Structures_H.notification) ntfnptr
                 and K ((ntfnObj ntfn = IdleNtfn \<and> queue = [thread]) \<or>
                        (\<exists>q. ntfnObj ntfn = WaitingNtfn q \<and> thread \<notin> set q \<and>
-                            queue = q @ [thread])))
+                            queue = q @ [thread] \<and> distinct q)))
            UNIV hs
            (setNotification ntfnptr $ ntfnObj_update (\<lambda>_. Structures_H.WaitingNtfn queue) ntfn)
            (\<acute>ntfn_queue :== CALL ntfn_ptr_get_queue(ntfn_Ptr ntfnptr);;

proof/crefine/RISCV64/Recycle_C.thy

@@ -934,6 +934,7 @@ lemma cancelBadgedSends_ccorres:
       apply (rule ccorres_return_Skip)
      apply (simp add: ccorres_cond_iffs)
      apply (rule ccorres_return_Skip)
+    apply (rule ccorres_assert2)
     apply (rename_tac list)
     apply (simp add: Collect_True Collect_False endpoint_state_defs
                      ccorres_cond_iffs
@@ -964,6 +965,7 @@ lemma cancelBadgedSends_ccorres:
           subgoal by simp
          apply (simp add: refill_buffer_relation_def image_def dom_def Let_def typ_heap_simps
                           update_ep_map_tos)
+        apply (thin_tac "distinct _")
         apply (rule ccorres_symb_exec_r)
           apply (rule_tac xs=list in filterM_voodoo)
           apply (rule_tac P="\<lambda>xs s. (\<forall>x \<in> set xs \<union> set list.

proof/crefine/RISCV64/SR_lemmas_C.thy

@@ -1212,8 +1212,7 @@ lemma ntfn_blocked_in_queueD:
 (* MOVE *)
 lemma valid_ntfn_isWaitingNtfnD:
   "\<lbrakk> valid_ntfn' ntfn s; isWaitingNtfn (ntfnObj ntfn) \<rbrakk>
-  \<Longrightarrow> (ntfnQueue (ntfnObj ntfn)) \<noteq> [] \<and> (\<forall>t\<in>set (ntfnQueue (ntfnObj ntfn)). tcb_at' t s)
-    \<and> distinct (ntfnQueue (ntfnObj ntfn))"
+  \<Longrightarrow> ntfnQueue (ntfnObj ntfn) \<noteq> [] \<and> (\<forall>t\<in>set (ntfnQueue (ntfnObj ntfn)). tcb_at' t s)"
   unfolding valid_ntfn'_def isWaitingNtfn_def
   by (clarsimp split: Structures_H.notification.splits ntfn.splits)
 

proof/invariant-abstract/ARM/ArchArch_AI.thy

@@ -192,7 +192,7 @@ lemmas perform_asid_pool_invocation_typ_ats [wp] =
 
 
 lemma perform_asid_control_invocation_tcb_at:
-  "\<lbrace>invs and valid_aci aci and st_tcb_at active p and
+  "\<lbrace>invs and valid_aci aci and tcb_at p and ex_nonz_cap_to p and
     K (\<forall>w a b c. aci = asid_control_invocation.MakePool w a b c \<longrightarrow> w \<noteq> p)\<rbrace>
   perform_asid_control_invocation aci
   \<lbrace>\<lambda>rv. tcb_at p\<rbrace>"
@@ -204,10 +204,6 @@ lemma perform_asid_control_invocation_tcb_at:
   apply (intro impI conjI)
     apply (clarsimp simp: retype_addrs_def obj_bits_api_def default_arch_object_def image_def ptr_add_def)
    apply (clarsimp simp: st_tcb_at_tcb_at)+
-  apply (frule st_tcb_ex_cap)
-    apply fastforce
-   apply (clarsimp split: Structures_A.thread_state.splits)
-   apply auto[1]
   apply (clarsimp simp: ex_nonz_cap_to_def valid_aci_def)
   apply (frule invs_untyped_children)
   apply (clarsimp simp:cte_wp_at_caps_of_state)
@@ -250,9 +246,10 @@ lemma invoke_arch_tcb:
     apply fastforce
    apply (clarsimp split: Structures_A.thread_state.splits)
    apply auto[1]
-  apply (clarsimp simp: ex_nonz_cap_to_def)
+  apply (frule st_tcb_at_tcb_at)
+  apply clarsimp
   apply (frule invs_untyped_children)
-  apply (clarsimp simp:cte_wp_at_caps_of_state)
+  apply (clarsimp simp: ex_nonz_cap_to_def cte_wp_at_caps_of_state)
   apply (erule_tac ptr="(aa,ba)" in untyped_children_in_mdbE[where P="\<lambda>c. t \<in> zobj_refs c" for t])
       apply (simp add: cte_wp_at_caps_of_state)+
      apply fastforce

proof/invariant-abstract/ARM/ArchDetSchedAux_AI.thy

@@ -16,27 +16,91 @@ lemmas arch_machine_ops_valid_sched_pred[wp] =
   arch_machine_ops_last_machine_time[THEN dmo_valid_sched_pred]
   arch_machine_ops_last_machine_time[THEN dmo_valid_sched_pred']
 
+lemma set_pt_eps_of[wp]:
+  "set_pt ptr pt \<lbrace>\<lambda>s. P (eps_of s)\<rbrace>"
+  by (set_object_easy_cases def: set_pt_def)
+
+lemma set_pd_eps_of[wp]:
+  "set_pd ptr pd \<lbrace>\<lambda>s. P (eps_of s)\<rbrace>"
+  by (set_object_easy_cases def: set_pd_def)
+
+lemma set_pt_ntfns_of[wp]:
+  "set_pt ptr pt \<lbrace>\<lambda>s. P (ntfns_of s)\<rbrace>"
+  by (set_object_easy_cases def: set_pt_def)
+
+lemma set_pd_ntfns_of[wp]:
+  "set_pd ptr pd \<lbrace>\<lambda>s. P (ntfns_of s)\<rbrace>"
+  by (set_object_easy_cases def: set_pd_def)
+
+lemma set_pt_tcbs_of[wp]:
+  "set_pt ptr pt \<lbrace>\<lambda>s. P (tcbs_of s)\<rbrace>"
+  by (set_object_easy_cases def: set_pt_def)
+
+lemma set_pd_tcbs_of[wp]:
+  "set_pd ptr pd \<lbrace>\<lambda>s. P (tcbs_of s)\<rbrace>"
+  by (set_object_easy_cases def: set_pd_def)
+
 lemma set_pd_valid_sched_pred[wp]:
   "set_pd ptr pd \<lbrace>valid_sched_pred_strong P\<rbrace>"
+  apply (rule hoare_lift_Pf[where f=ntfn_queues_of, rotated], wpsimp)
+  apply (rule hoare_lift_Pf[where f=ep_queues_of, rotated], wpsimp)
+  apply (rule hoare_lift_Pf[where f=prios_of, rotated], wpsimp)
+  apply (rule hoare_lift_Pf[where f=eps_of, rotated], wpsimp)
+  apply (rule hoare_lift_Pf[where f=ntfns_of, rotated], wpsimp)
   apply (wpsimp simp: set_pd_def wp: set_object_wp_strong get_object_wp)
-  by (auto simp: obj_at_kh_kheap_simps vs_all_heap_simps a_type_def fun_upd_def
-           split:  kernel_object.splits if_splits)
+  apply (fastforce simp: obj_at_kh_kheap_simps vs_all_heap_simps a_type_def
+                  split: kernel_object.splits if_splits)
+  done
 
 lemma set_pt_valid_sched_pred[wp]:
   "set_pt ptr pt \<lbrace>valid_sched_pred_strong P\<rbrace>"
+  apply (rule hoare_lift_Pf[where f=ntfn_queues_of, rotated], wpsimp)
+  apply (rule hoare_lift_Pf[where f=ep_queues_of, rotated], wpsimp)
+  apply (rule hoare_lift_Pf[where f=prios_of, rotated], wpsimp)
+  apply (rule hoare_lift_Pf[where f=eps_of, rotated], wpsimp)
+  apply (rule hoare_lift_Pf[where f=ntfns_of, rotated], wpsimp)
   apply (wpsimp simp: set_pt_def wp: set_object_wp_strong get_object_wp)
-  by (auto simp: obj_at_kh_kheap_simps vs_all_heap_simps a_type_def fun_upd_def
-           split:  kernel_object.splits if_splits)
+  apply (fastforce simp: obj_at_kh_kheap_simps vs_all_heap_simps a_type_def
+                  split: kernel_object.splits if_splits)
+  done
+
+lemma set_asid_pool_eps_of[wp]:
+  "set_asid_pool ptr pool \<lbrace>\<lambda>s. P (eps_of s)\<rbrace>"
+  by (set_object_easy_cases def: set_asid_pool_def)
+
+lemma set_asid_pool_ntfns_of[wp]:
+  "set_asid_pool ptr pool \<lbrace>\<lambda>s. P (ntfns_of s)\<rbrace>"
+  by (set_object_easy_cases def: set_asid_pool_def)
+
+lemma set_asid_pool_tcbs_of[wp]:
+  "set_asid_pool ptr pool \<lbrace>\<lambda>s. P (tcbs_of s)\<rbrace>"
+  by (set_object_easy_cases def: set_asid_pool_def)
 
 lemma set_asid_pool_bound_sc_obj_tcb_at[wp]:
   "set_asid_pool ptr pool \<lbrace>valid_sched_pred_strong P\<rbrace>"
+  apply (rule hoare_lift_Pf[where f=ntfn_queues_of, rotated], wpsimp)
+  apply (rule hoare_lift_Pf[where f=ep_queues_of, rotated], wpsimp)
+  apply (rule hoare_lift_Pf[where f=prios_of, rotated], wpsimp)
+  apply (rule hoare_lift_Pf[where f=eps_of, rotated], wpsimp)
+  apply (rule hoare_lift_Pf[where f=ntfns_of, rotated], wpsimp)
   apply (wpsimp simp: set_asid_pool_def wp: set_object_wp_strong get_object_wp)
-  by (auto simp: obj_at_kh_kheap_simps vs_all_heap_simps a_type_def fun_upd_def
-           split:  kernel_object.splits if_splits)
+  apply (fastforce simp: obj_at_kh_kheap_simps vs_all_heap_simps a_type_def
+                  split: kernel_object.splits if_splits)
+  done
+
+crunch copy_global_mappings
+  for eps_of[wp]: "\<lambda>s. P (eps_of s)"
+  and ntfns_of[wp]: "\<lambda>s. P (ntfns_of s)"
+  and prios_of[wp]: "\<lambda>s. P (prios_of s)"
+  (wp: dxo_wp_weak crunch_wps)
 
 lemma copy_global_mappings_valid_sched_pred[wp]:
   "copy_global_mappings pd \<lbrace>valid_sched_pred_strong P\<rbrace>"
-  by (wpsimp simp: copy_global_mappings_def store_pde_def wp: mapM_x_wp_inv)
+  apply (rule hoare_lift_Pf[where f=ntfn_queues_of, rotated], wpsimp)
+  apply (rule hoare_lift_Pf[where f=ep_queues_of, rotated], wpsimp)
+  apply (rule hoare_lift_Pf[where f=prios_of, rotated], wpsimp)
+  apply (wpsimp simp: copy_global_mappings_def store_pte_def store_pde_def wp: mapM_x_wp_inv)
+  done
 
 lemma init_arch_objects_valid_sched_pred[wp, DetSchedAux_AI_assms]:
   "init_arch_objects new_type dev ptr num_objects obj_sz refs \<lbrace>valid_sched_pred_strong P\<rbrace>"
@@ -251,6 +315,32 @@ lemma perform_asid_control_invocation_sc_at_pred_n_live:
   unfolding sc_at_pred_n_def using live
   by (auto intro!: perform_asid_control_invocation_obj_at_live simp: cspace_agnostic_pred_def live_def)
 
+lemma perform_asid_control_invocation_ep_at_pred_live:
+  assumes live: "\<forall>ep. P ep \<longrightarrow> ep \<noteq> IdleEP"
+  shows
+  "\<lbrace>\<lambda>s. Q (ep_at_pred P p s)
+        \<and> invs s
+        \<and> ct_active s
+        \<and> valid_aci aci s
+        \<and> scheduler_action s = resume_cur_thread\<rbrace>
+   perform_asid_control_invocation aci
+   \<lbrace>\<lambda>rv s. Q (ep_at_pred P p s)\<rbrace>"
+  unfolding ep_at_pred_def2 using live
+  by (auto intro!: perform_asid_control_invocation_obj_at_live simp: cspace_agnostic_pred_def live_def)
+
+lemma perform_asid_control_invocation_ntfn_at_pred_live:
+  assumes live: "\<forall>ntfn. P ntfn \<longrightarrow> live_ntfn ntfn"
+  shows
+  "\<lbrace>\<lambda>s. Q (ntfn_at_pred P p s)
+        \<and> invs s
+        \<and> ct_active s
+        \<and> valid_aci aci s
+        \<and> scheduler_action s = resume_cur_thread\<rbrace>
+   perform_asid_control_invocation aci
+   \<lbrace>\<lambda>rv s. Q (ntfn_at_pred P p s)\<rbrace>"
+  unfolding ntfn_at_pred_def2 using live
+  by (auto intro!: perform_asid_control_invocation_obj_at_live simp: cspace_agnostic_pred_def live_def)
+
 lemma perform_asid_control_invocation_valid_idle:
   "\<lbrace>invs and ct_active
          and valid_aci aci
@@ -302,18 +392,22 @@ lemma perform_asid_control_invocation_valid_sched:
    apply (rule_tac I="invs and ct_active and
                       (\<lambda>s. scheduler_action s = resume_cur_thread) and valid_aci aci"
           in valid_sched_tcb_state_preservation_gen)
-                 apply simp
-                 apply (wpsimp wp: perform_asid_control_invocation_st_tcb_at
-                                   perform_asid_control_invocation_pred_tcb_at_live
-                                   perform_asid_control_invocation_sc_at_pred_n_live[where Q="Not"]
-                                   perform_asid_control_etcb_at
-                                   perform_asid_control_invocation_sc_at_pred_n
-                                   perform_asid_control_invocation_valid_idle
-                                   perform_asid_control_invocation_pred_map_sc_refill_cfgs_of
-                                   perform_asid_control_invocation_implies_zero_budget
-                                   perform_asid_control_invocation_sporadic_implies
-                                   hoare_vcg_all_lift
-                             simp: ipc_queued_thread_state_live live_sc_def)+
+                         apply simp
+                          apply (wpsimp wp: perform_asid_control_invocation_st_tcb_at
+                                            perform_asid_control_invocation_pred_tcb_at_live
+                                            perform_asid_control_invocation_sc_at_pred_n_live[where Q="Not"]
+                                            perform_asid_control_etcb_at
+                                            perform_asid_control_invocation_sc_at_pred_n
+                                            perform_asid_control_invocation_valid_idle
+                                            perform_asid_control_invocation_pred_map_sc_refill_cfgs_of
+                                            perform_asid_control_invocation_implies_zero_budget
+                                            perform_asid_control_invocation_sporadic_implies
+                                            perform_asid_control_invocation_ep_at_pred_live
+                                            perform_asid_control_invocation_ntfn_at_pred_live
+                                            hoare_vcg_all_lift
+                                      simp: ipc_queued_thread_state_live live_sc_def
+                                            ntfn_queue_nonempty_live
+                                            tcb_at_st_tcb_at)+
   done
 
 lemma perform_asid_control_invocation_cur_sc_active: