rt spec+proof: prove awaken_ccorres

Signed-off-by: Michael McInerney <michael.mcinerney@proofcraft.systems>

proof/crefine/RISCV64/Finalise_C.thy

@@ -637,14 +637,19 @@ lemma merge_overlapping_head_refill_ccorres:
   done
 
 (* FIXME RT: move to Corres_UL_C? *)
-lemma ccorres_to_vcg_Normal:
-  "\<lbrakk>ccorres_underlying srel \<Gamma> rrel xf arrel axf P P' [] a c; no_fail Q a\<rbrakk>
-   \<Longrightarrow> \<Gamma> \<turnstile> {s'. P s \<and> Q s \<and> s' \<in> P' \<and> (s, s') \<in> srel} c UNIV"
-  apply (frule (1) ccorres_to_vcg_with_prop[where R="\<top>\<top>" and s=s])
+lemma ccorres_to_vcg_Normal':
+  "\<lbrakk>ccorres_underlying srel \<Gamma> rrel xf arrel axf P P' [] a c\<rbrakk>
+   \<Longrightarrow> \<Gamma> \<turnstile> {s'. P s \<and> \<not> snd (a s) \<and> s' \<in> P' \<and> (s, s') \<in> srel} c UNIV"
+  apply (frule ccorres_to_vcg_with_prop'[where R="\<top>\<top>" and s=s])
    apply wpsimp
   apply (fastforce elim: conseqPost)
   done
 
+lemma ccorres_to_vcg_Normal:
+  "\<lbrakk>ccorres_underlying srel \<Gamma> rrel xf arrel axf P P' [] a c; no_fail Q a\<rbrakk>
+   \<Longrightarrow> \<Gamma> \<turnstile> {s'. P s \<and> Q s \<and> s' \<in> P' \<and> (s, s') \<in> srel} c UNIV"
+  by (fastforce elim: ccorres_to_vcg_Normal' intro: conseqPre simp: no_fail_def)
+
 crunch scActive
  for (empty_fail) empty_fail[wp]
 

proof/crefine/RISCV64/Ipc_C.thy

@@ -5015,26 +5015,6 @@ lemma schedContext_donate_ccorres:
      (schedContextDonate scPtr tcbPtr) (Call schedContext_donate_'proc)"
 sorry (* FIXME RT: schedContext_donate_ccorres *)
 
-lemma tcbReleaseDequeue_ccorres:
-  "ccorres (\<lambda>ptr ptr'. ptr' = tcb_ptr_to_ctcb_ptr ptr) ret__ptr_to_struct_tcb_C_'
-     (\<lambda>s. \<not> tcbQueueEmpty (ksReleaseQueue s) \<and> valid_objs' s) UNIV []
-     tcbReleaseDequeue (Call tcbReleaseDequeue_'proc)"
-  apply (clarsimp simp: tcbReleaseDequeue_def)
-  apply (rule ccorres_symb_exec_l'[OF _ _ getReleaseQueue_sp]; wpsimp?)
-  apply cinit'
-   apply (rule ccorres_symb_exec_r)
-     apply (ctac add: tcbReleaseRemove_ccorres)
-       apply (fastforce intro: ccorres_return_C)
-      apply wpsimp
-     apply (vcg exspec=tcbReleaseRemove_modifies)
-    apply vcg
-   apply (rule conseqPre, vcg)
-   apply clarsimp
-  apply wpsimp
-  apply (clarsimp simp: rf_sr_def cstate_relation_def ctcb_queue_relation_def option_to_ctcb_ptr_def
-                        Let_def tcbQueueEmpty_def)
-  done
-
 lemma sendIPC_ccorres [corres]:
   "ccorres dc xfdc (invs' and st_tcb_at' simple' thread
                           and sch_act_not thread and ep_at' epptr)

proof/crefine/RISCV64/SR_lemmas_C.thy

@@ -2237,6 +2237,11 @@ lemma rf_sr_ctcb_queue_relation:
   apply (clarsimp simp: Let_def seL4_MinPrio_def minDom_def maxDom_to_H maxPrio_to_H)
   done
 
+lemma rf_sr_ctcb_queue_relation_release_queue:
+  "(s, s') \<in> rf_sr \<Longrightarrow> ctcb_queue_relation (ksReleaseQueue s) (ksReleaseQueue_' (globals s'))"
+  unfolding rf_sr_def cstate_relation_def cready_queues_relation_def
+  by (clarsimp simp: Let_def seL4_MinPrio_def minDom_def maxDom_to_H maxPrio_to_H)
+
 lemma rf_sr_sched_action_relation:
   "(s, s') \<in> rf_sr
    \<Longrightarrow> cscheduler_action_relation (ksSchedulerAction s) (ksSchedulerAction_' (globals s'))"

proof/crefine/RISCV64/Schedule_C.thy

@@ -631,6 +631,200 @@ lemma commitTime_ccorres:
   "ccorres dc xfdc \<top> UNIV [] commitTime (Call commitTime_'proc)"
 sorry (* FIXME RT: commitTime_ccorres *)
 
+lemma ccorres_pre_getReleaseQueue:
+  assumes cc: "\<And>rv. ccorres r xf (P rv) (P' rv) hs (f rv) c"
+  shows
+    "ccorres r xf
+       (\<lambda>s. \<forall>rv. ksReleaseQueue s = rv \<longrightarrow> P rv s)
+       {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> ksReleaseQueue s = rv \<and> P rv s
+                    \<and> ctcb_queue_relation rv (ksReleaseQueue_' (globals s'))
+                   \<longrightarrow> s' \<in> P' rv} hs
+       (getReleaseQueue >>= (\<lambda>rv. f rv)) c"
+  apply (rule ccorres_guard_imp)
+    apply (rule ccorres_symb_exec_l)
+       defer
+       apply wp[1]
+      apply (rule getReleaseQueue_sp)
+     apply wpsimp
+    apply assumption
+   apply clarsimp
+   defer
+   apply (rule ccorres_guard_imp)
+     apply (rule cc)
+    apply clarsimp
+   apply assumption
+  apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def)
+  by fast
+
+lemma scActive_exs_valid[wp]:
+  "sc_at' scPtr s \<Longrightarrow> \<lbrace>(=) s\<rbrace> scActive scPtr \<exists>\<lbrace>\<lambda>r. (=) s\<rbrace>"
+  unfolding scActive_def
+  apply wpsimp
+  by (fastforce dest: no_ofailD[OF no_ofail_readScActive])
+
+lemma release_q_non_empty_and_ready_ccorres:
+  "ccorres (\<lambda>rv rv'. rv = to_bool rv') ret__unsigned_long_'
+     (valid_objs' and no_0_obj' and pspace_aligned' and pspace_distinct'
+      and (\<lambda>s. \<forall>head. tcbQueueHead (ksReleaseQueue s) = Some head \<longrightarrow> active_sc_tcb_at' head s))
+     UNIV []
+     (gets_the releaseQNonEmptyAndReady)
+     (Call release_q_non_empty_and_ready_'proc)"
+  apply cinit'
+   apply (simp add: releaseQNonEmptyAndReady_def gets_the_if_distrib readReleaseQueue_def
+                    gets_the_ogets
+              flip: getReleaseQueue_def)
+   apply (rule ccorres_pre_getReleaseQueue)
+   apply (rename_tac releaseQueue)
+   apply (rule_tac xf'=ret__int_'
+               and val="from_bool (tcbQueueHead releaseQueue \<noteq> None)"
+               and R="\<lambda>s. ksReleaseQueue s = releaseQueue
+                          \<and> (\<forall>head. tcbQueueHead (ksReleaseQueue s) = Some head \<longrightarrow> tcb_at' head s)"
+               and R'=UNIV
+                in ccorres_symb_exec_r_known_rv)
+      apply (rule conseqPre, vcg)
+      apply (fastforce dest: tcb_at_not_NULL rf_sr_ctcb_queue_relation_release_queue
+                       simp: ctcb_queue_relation_def option_to_ctcb_ptr_def
+                      split: option.splits)
+     apply ceqv
+    apply (subst if_swap)
+    apply (rule ccorres_cond_seq)
+    apply ccorres_rewrite
+    apply (rule_tac Q="\<lambda>s. ksReleaseQueue s = releaseQueue" in ccorres_cond_both'[where Q'=\<top>])
+      apply fastforce
+     apply (rule ccorres_rhs_assoc)+
+     apply (clarsimp simp: gets_the_obind)
+     apply (rule ccorres_Guard_Seq)
+     apply (simp flip: threadGet_def refillReady_def)
+     apply (drule Some_to_the)
+     apply clarsimp
+     apply (rule ccorres_pre_threadGet)
+     apply (simp add: gets_the_ohaskell_assert)
+     apply (rule ccorres_assert2)
+     apply (simp flip: scActive_def)
+     apply (rule ccorres_symb_exec_l')
+        apply (rule ccorres_assert2_abs)
+        apply (rule ccorres_add_return2)
+        apply (ctac add: refill_ready_ccorres)
+          apply csymbr
+          apply (fastforce intro: ccorres_return_C')
+         apply wpsimp
+        apply (vcg exspec=refill_ready_modifies)
+       apply wpsimp+
+    apply (fastforce intro: ccorres_return_C)
+   apply vcg
+  apply (rule conjI)
+   apply (fastforce intro!: aligned'_distinct'_obj_at'I
+                      simp: active_sc_tcb_at'_def active_sc_at'_def obj_at'_def
+                            opt_pred_def opt_map_def
+                     split: option.splits)
+  apply clarsimp
+  apply (intro conjI)
+    apply (clarsimp simp: ctcb_relation_def typ_heap_simps' option_to_ctcb_ptr_def
+                          ctcb_queue_relation_def)
+   apply (clarsimp simp: to_bool_def split: if_splits)
+  apply (force dest: obj_at_cslift_tcb
+               simp: typ_heap_simps' ctcb_queue_relation_def option_to_ctcb_ptr_def)
+  done
+
+lemma tcbReleaseDequeue_ccorres:
+  "ccorres dc xfdc
+     (valid_objs' and no_0_obj' and pspace_aligned' and pspace_distinct'
+      and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and (\<lambda>s. ksCurDomain s \<le> maxDomain)
+      and (\<lambda>s. releaseQNonEmptyAndReady s = Some True))
+     UNIV []
+     tcbReleaseDequeue
+     (Call tcbReleaseDequeue_'proc)"
+  apply cinit
+   apply (rule ccorres_stateAssert)+
+   apply (rule ccorres_pre_getReleaseQueue, rename_tac releaseQueue)
+   apply (rule_tac P="tcbQueueHead releaseQueue \<noteq> None" in ccorres_gen_asm)
+   apply (rule ccorres_symb_exec_l')
+     apply (rule ccorres_assert2_abs)
+     apply (rule_tac xf'=awakened_'
+                 and val="option_to_ctcb_ptr (tcbQueueHead releaseQueue)"
+                 and R="\<lambda>s. ksReleaseQueue s = releaseQueue"
+                 and R'=UNIV
+                  in ccorres_symb_exec_r_known_rv)
+        apply (rule conseqPre, vcg)
+        apply clarsimp
+        apply (drule rf_sr_ctcb_queue_relation_release_queue)
+        apply (clarsimp simp: ctcb_queue_relation_def)
+       apply ceqv
+      apply (ctac add: tcbReleaseRemove_ccorres)
+        apply (rule ccorres_add_return2)
+        apply (simp only: bind_assoc)
+        apply (subst ccorres_seq_skip'[symmetric])
+        apply (ctac add: possibleSwitchTo_ccorres)
+          apply (rule ccorres_stateAssert)+
+          apply (rule ccorres_return_Skip')
+         apply wpsimp
+        apply (vcg exspec=possibleSwitchTo_modifies)
+       apply wpsimp
+      apply (vcg exspec=tcbReleaseRemove_modifies)
+     apply vcg
+    apply wpsimp+
+  apply (frule releaseQNonEmptyAndReady_implies_releaseQNonEmpty)
+  by (fastforce dest: obj_at'_tcbQueueHead_ksReleaseQueue simp: option_to_ctcb_ptr_def)
+
+lemma no_ofail_releaseQNonEmptyAndReady:
+  "no_ofail (invs'
+             and (\<lambda>s. \<forall>head. tcbQueueHead (ksReleaseQueue s) = Some head
+                             \<longrightarrow> active_sc_tcb_at' head s))
+            releaseQNonEmptyAndReady"
+  unfolding releaseQNonEmptyAndReady_def readReleaseQueue_def
+  apply (wpsimp wp: ovalid_threadRead)
+  apply (clarsimp split: if_splits)
+  apply (intro conjI)
+   apply (fastforce intro!: aligned'_distinct'_obj_at'I
+                      simp: active_sc_tcb_at'_def opt_pred_def opt_map_def obj_at_simps
+                     split: option.splits)
+  apply normalise_obj_at'
+  apply (fastforce intro!: aligned'_distinct'_obj_at'I
+                     simp: active_sc_tcb_at'_def obj_at'_def opt_pred_def opt_map_def
+                    split: option.splits)
+  done
+
+lemma awaken_ccorres:
+  "ccorres dc xfdc (invs' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)) UNIV []
+     awaken (Call awaken_'proc)"
+  (is "ccorres _ _ ?abs _ _ _ _")
+  apply (cinit simp: runReaderT_def whileAnno_def)
+   apply (rule ccorres_stateAssert)+
+   apply (rule ccorres_handlers_weaken)
+   apply (rule_tac G="\<lambda>_. ?abs
+                          and (\<lambda>s. \<forall>head. tcbQueueHead (ksReleaseQueue s) = Some head
+                                          \<longrightarrow> active_sc_tcb_at' head s)"
+                in ccorres_While'[where G'=UNIV])
+        apply (rule ccorres_guard_imp)
+          apply (ctac add: tcbReleaseDequeue_ccorres)
+         apply fastforce
+        apply fastforce
+       apply (rule ccorres_guard_imp)
+         apply (ctac add: release_q_non_empty_and_ready_ccorres)
+        apply fastforce
+       apply fastforce
+      apply (wpsimp wp: no_ofail_releaseQNonEmptyAndReady)
+     apply (clarsimp simp: pred_conj_def)
+     apply (intro hoare_vcg_conj_lift_pre_fix; (solves wpsimp)?)
+     apply (clarsimp simp: tcbReleaseDequeue_def)
+     apply (wpsimp simp: tcbQueueHead_ksReleaseQueue_active_sc_tcb_at'_asrt_def)
+    apply (rule conseqPre)
+     apply (rule ccorres_to_vcg_Normal'[where xf=xfdc])
+     apply (fastforce intro: ccorres_call[OF tcbReleaseDequeue_ccorres])
+    apply fastforce
+   apply clarsimp
+   apply (rule conseqPre)
+    apply (rule_tac xf=ret__unsigned_long_' in ccorres_to_vcg_Normal)
+     apply (fastforce intro: ccorres_call[OF release_q_non_empty_and_ready_ccorres])
+    apply (fastforce intro: no_ofail_gets_the no_ofail_releaseQNonEmptyAndReady)
+   apply fastforce
+  apply (clarsimp simp: tcbInReleaseQueue_imp_active_sc_tcb_at'_asrt_def ksReleaseQueue_asrt_def
+                        list_queue_relation_def)
+  apply (frule heap_path_head')
+  apply (clarsimp simp: tcbQueueEmpty_def)
+  apply (case_tac "ts = []"; force)
+  done
+
 lemma schedule_ccorres:
   "ccorres dc xfdc invs' UNIV [] schedule (Call schedule_'proc)"
 sorry (* FIXME RT: schedule_ccorres

proof/crefine/RISCV64/Tcb_C.thy

@@ -4952,7 +4952,7 @@ lemma find_time_after_ccorres:
   (is "ccorres _ _ (?abs_inv and _) _ _ _ _")
   supply sched_context_C_size[simp del] refill_C_size[simp del]
   apply (cinit lift: new_time_' tcb_'
-               simp: runReaderT_def whileAnno_def tcbInReleaseQueue_imp_active_sc_tc_at'_asrt_def)
+               simp: runReaderT_def whileAnno_def tcbInReleaseQueue_imp_active_sc_tcb_at'_asrt_def)
    apply (rule ccorres_stateAssert)
    apply (rule ccorres_symb_exec_r)
      apply (rule ccorres_add_return2)

proof/invariant-abstract/DetSchedSchedule_AI.thy

@@ -10816,41 +10816,26 @@ lemma active_sc_tcb_at_budget_sufficient:
   by (fastforce simp: budget_sufficient_def2 active_sc_tcb_at_def2 is_sc_active_kh_simp
                 dest: valid_refills_refill_sufficient active_scs_validE)
 
-lemma awaken_body_valid_ready_qs:
-  "\<lbrace>\<lambda>s. valid_ready_qs s \<and> valid_release_q s \<and> active_scs_valid s
+lemma tcb_release_dequeue_valid_ready_qs:
+  "\<lbrace>\<lambda>s. valid_ready_qs s \<and> valid_release_q s
         \<and> release_queue s \<noteq> [] \<and> budget_ready (hd (release_queue s)) s\<rbrace>
-   awaken_body
+   tcb_release_dequeue
    \<lbrace>\<lambda>_. valid_ready_qs\<rbrace>"
-  apply (clarsimp simp: awaken_body_def tcb_release_dequeue_def bind_assoc)
-  apply (rule bind_wp[OF _ gets_sp], rename_tac rq)
-  apply (rule_tac Q'="\<lambda>_ s. valid_ready_qs s \<and> st_tcb_at runnable (hd rq) s
-                           \<and> released_sc_tcb_at (hd rq) s"
-               in bind_wp_fwd)
-   apply (intro hoare_vcg_conj_lift_pre_fix; (solves wpsimp)?)
-    apply (wpsimp simp: valid_release_q_def obj_at_kh_kheap_simps)
-   apply (wpsimp simp: valid_release_q_def obj_at_kh_kheap_simps released_sc_tcb_at_def)
-   apply (clarsimp intro!: active_sc_tcb_at_budget_sufficient)
-  apply (wpsimp wp: possible_switch_to_valid_ready_qs
-              simp: released_sc_tcb_at_def)
-  apply (clarsimp simp: pred_tcb_at_def obj_at_def)
+  unfolding tcb_release_dequeue_def
+  apply (wpsimp wp: possible_switch_to_valid_ready_qs hoare_disjI2 hoare_vcg_all_lift
+                    hoare_vcg_imp_lift')
+  apply (clarsimp simp: valid_release_q_def)
+  apply (fastforce dest: hd_in_set simp: vs_all_heap_simps obj_at_kh_kheap_simps)
   done
 
-lemma awaken_body_valid_sched_action:
-  "\<lbrace>\<lambda>s. valid_sched_action s \<and> valid_release_q s \<and> active_scs_valid s
+lemma tcb_release_dequeue_valid_sched_action:
+  "\<lbrace>\<lambda>s. valid_sched_action s \<and> valid_release_q s
         \<and> release_queue s \<noteq> [] \<and> budget_ready (hd (release_queue s)) s\<rbrace>
-   awaken_body
+   tcb_release_dequeue
    \<lbrace>\<lambda>_. valid_sched_action\<rbrace>"
-  apply (clarsimp simp: awaken_body_def tcb_release_dequeue_def bind_assoc)
-  apply (rule bind_wp[OF _ gets_sp], rename_tac rq)
-  apply (rule_tac Q'="\<lambda>_ s. valid_sched_action s \<and> st_tcb_at runnable (hd rq) s
-                           \<and> released_sc_tcb_at (hd rq) s"
-               in bind_wp_fwd)
-   apply (intro hoare_vcg_conj_lift_pre_fix; (solves wpsimp)?)
-    apply (wpsimp simp: valid_release_q_def obj_at_kh_kheap_simps)
-   apply wpsimp
-   apply (fastforce intro: active_sc_tcb_at_budget_sufficient
-                     simp: released_sc_tcb_at_def valid_release_q_def)
-  apply (wpsimp simp: obj_at_kh_kheap_simps)
+  unfolding tcb_release_dequeue_def
+  apply (wpsimp wp: hoare_drop_imps)
+  apply (fastforce simp: released_sc_tcb_at_def valid_release_q_def)
   done
 
 lemma read_tcb_refill_ready_SomeD:
@@ -10985,16 +10970,16 @@ lemma awaken_valid_sched:
                           read_tcb_obj_ref_SomeD read_sched_context_SomeD
                           read_release_q_non_empty_and_ready_SomeD
                     simp: vs_all_heap_simps)
-  apply (intro hoare_vcg_conj_lift_pre_fix
-         ; (solves \<open>wpsimp simp: awaken_body_def tcb_release_dequeue_def\<close>)?)
-     apply (wpsimp wp: awaken_body_valid_ready_qs)
-    apply (wpsimp wp: possible_switch_to_not_it_ct_not_in_q simp: awaken_body_def tcb_release_dequeue_def)
+  apply (intro hoare_vcg_conj_lift_pre_fix;
+         (solves \<open>wpsimp simp: tcb_release_dequeue_def\<close>)?)
+     apply (wpsimp wp: tcb_release_dequeue_valid_ready_qs)
+    apply (wpsimp wp: possible_switch_to_not_it_ct_not_in_q simp: tcb_release_dequeue_def)
     apply (clarsimp simp: valid_release_q_def valid_idle_def vs_all_heap_simps pred_tcb_at_def
                           obj_at_def)
     apply (fastforce dest: hd_in_set)
-   apply (wpsimp wp: awaken_body_valid_sched_action)
+   apply (wpsimp wp: tcb_release_dequeue_valid_sched_action)
   apply (wpsimp wp: possible_switch_to_valid_blocked tcb_release_remove_valid_blocked_except
-              simp: awaken_body_def tcb_release_dequeue_def)
+              simp: tcb_release_dequeue_def tcb_release_dequeue_def)
   done
 
 end
@@ -12337,9 +12322,10 @@ lemma not_schedulable_in_release_q_case:
   by (clarsimp simp: schedulable_def2 ct_in_state_def tcb_at_kh_simps runnable_eq_active)
 
 lemma awaken_valid_sched_misc[wp]:
-  "awaken \<lbrace>\<lambda>s. P (consumed_time s) (cur_sc s) (cur_time s) (cur_domain s)
-                 (cur_thread s) (idle_thread s) (kheap s) \<rbrace>"
-  apply (wpsimp simp: awaken_def awaken_body_def tcb_release_dequeue_def)
+  "awaken
+   \<lbrace>\<lambda>s. P (consumed_time s) (cur_sc s) (cur_time s) (cur_domain s) (cur_thread s) (idle_thread s)
+          (kheap s)\<rbrace>"
+  apply (wpsimp simp: awaken_def tcb_release_dequeue_def)
   apply (rule whileLoop_wp)
    apply wpsimp+
   done
@@ -12401,7 +12387,7 @@ lemma possible_switch_to_scheduler_act_sane'':
 
 lemma awaken_cur_sc_in_release_q_imp_zero_consumed[wp]:
   "awaken \<lbrace>cur_sc_in_release_q_imp_zero_consumed ::'state_ext state \<Rightarrow> _\<rbrace>"
-  apply (wpsimp simp: awaken_def awaken_body_def tcb_release_dequeue_def)
+  apply (wpsimp simp: awaken_def tcb_release_dequeue_def)
   apply (clarsimp simp: cur_sc_in_release_q_imp_zero_consumed_def)
   apply (rule whileLoop_wp)
    apply (wpsimp wp: hoare_vcg_all_lift hoare_vcg_imp_lift')+
@@ -12433,8 +12419,8 @@ lemma awaken_in_release_q:
   "\<lbrace>in_release_q t and valid_release_q and (not budget_ready t) and active_scs_valid\<rbrace>
    awaken
    \<lbrace>\<lambda>_ s. in_release_q t s\<rbrace>"
-   (is "valid ?pre _ _")
-  apply (wpsimp simp: awaken_def awaken_body_def tcb_release_dequeue_def)
+  (is "valid ?pre _ _")
+  apply (wpsimp simp: awaken_def tcb_release_dequeue_def)
   apply (rule_tac I="\<lambda>_. ?pre" in valid_whileLoop; (solves simp)?)
   apply (clarsimp simp: pred_conj_def pred_neg_def)
   apply (intro hoare_vcg_conj_lift_pre_fix; (solves \<open>wpsimp wp: hoare_drop_imps\<close>)?)

proof/invariant-abstract/Syscall_AI.thy

@@ -161,7 +161,7 @@ declare sc_and_timer_activatable[wp]
 
 lemma awaken_schact_not_rct[wp]:
   "awaken \<lbrace>\<lambda>s. scheduler_action s \<noteq> resume_cur_thread\<rbrace>"
-  unfolding awaken_def awaken_body_def tcb_release_dequeue_def possible_switch_to_def
+  unfolding awaken_def tcb_release_dequeue_def possible_switch_to_def
   apply (rule whileLoop_wp)
    apply (wpsimp wp: hoare_drop_imps simp: set_scheduler_action_def)+
   done