diff --git a/proof/crefine/RISCV64/Finalise_C.thy b/proof/crefine/RISCV64/Finalise_C.thy
index 4526800986..99474d3382 100644
--- a/proof/crefine/RISCV64/Finalise_C.thy
+++ b/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]
 
diff --git a/proof/crefine/RISCV64/Ipc_C.thy b/proof/crefine/RISCV64/Ipc_C.thy
index 31584cccaf..1f80932177 100644
--- a/proof/crefine/RISCV64/Ipc_C.thy
+++ b/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)
diff --git a/proof/crefine/RISCV64/SR_lemmas_C.thy b/proof/crefine/RISCV64/SR_lemmas_C.thy
index 8db22e5f90..f004d6ca24 100644
--- a/proof/crefine/RISCV64/SR_lemmas_C.thy
+++ b/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'))"
diff --git a/proof/crefine/RISCV64/Schedule_C.thy b/proof/crefine/RISCV64/Schedule_C.thy
index f6f679b3c1..a312834f69 100644
--- a/proof/crefine/RISCV64/Schedule_C.thy
+++ b/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
diff --git a/proof/crefine/RISCV64/Tcb_C.thy b/proof/crefine/RISCV64/Tcb_C.thy
index 00df4d7c4d..ac68d104a2 100644
--- a/proof/crefine/RISCV64/Tcb_C.thy
+++ b/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)
diff --git a/proof/invariant-abstract/DetSchedSchedule_AI.thy b/proof/invariant-abstract/DetSchedSchedule_AI.thy
index e30840929c..79f069d9ae 100644
--- a/proof/invariant-abstract/DetSchedSchedule_AI.thy
+++ b/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>)?)
diff --git a/proof/invariant-abstract/Syscall_AI.thy b/proof/invariant-abstract/Syscall_AI.thy
index ec04f2b2cb..182e4c001f 100644
--- a/proof/invariant-abstract/Syscall_AI.thy
+++ b/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
diff --git a/proof/refine/RISCV64/EmptyFail_H.thy b/proof/refine/RISCV64/EmptyFail_H.thy
index 6d9f340a15..30d9db8bed 100644
--- a/proof/refine/RISCV64/EmptyFail_H.thy
+++ b/proof/refine/RISCV64/EmptyFail_H.thy
@@ -291,7 +291,7 @@ crunch tcbReleaseDequeue
 
 lemma awaken_empty_fail[intro!, wp, simp]:
   "empty_fail awaken"
-  apply (clarsimp simp: awaken_def awakenBody_def)
+  apply (clarsimp simp: awaken_def tcbReleaseDequeue_def)
   apply (wpsimp wp: empty_fail_whileLoop)
   done
 
diff --git a/proof/refine/RISCV64/Ipc_R.thy b/proof/refine/RISCV64/Ipc_R.thy
index 6f8671e771..9b321d418f 100644
--- a/proof/refine/RISCV64/Ipc_R.thy
+++ b/proof/refine/RISCV64/Ipc_R.thy
@@ -3445,7 +3445,7 @@ lemma findTimeAfter_corres:
   apply (rule corres_gen_asm')
   apply (clarsimp simp: find_time_after_def findTimeAfter_def runReaderT_def)
   apply (rule corres_stateAssert_implied[where P=P and P'=P for P, simplified, rotated])
-   apply (fastforce simp: tcbInReleaseQueue_imp_active_sc_tc_at'_asrt_def
+   apply (fastforce simp: tcbInReleaseQueue_imp_active_sc_tcb_at'_asrt_def
                    dest!: release_queue_active_sc_tcb_at_cross)
   apply (rule stronger_corres_guard_imp)
     apply (rule_tac P="\<lambda>r s. ?abs s \<and> suffix r ls"
diff --git a/proof/refine/RISCV64/KHeap_R.thy b/proof/refine/RISCV64/KHeap_R.thy
index f66f847a3b..e1efe240eb 100644
--- a/proof/refine/RISCV64/KHeap_R.thy
+++ b/proof/refine/RISCV64/KHeap_R.thy
@@ -5086,8 +5086,8 @@ lemma active_sc_tcb_at_cross:
   apply (clarsimp simp: active_sc_tcb_at'_def in_omonad obj_at'_def active_sc_at'_def)
   done
 
-defs tcbInReleaseQueue_imp_active_sc_tc_at'_asrt_def:
-  "tcbInReleaseQueue_imp_active_sc_tc_at'_asrt \<equiv>
+defs tcbInReleaseQueue_imp_active_sc_tcb_at'_asrt_def:
+  "tcbInReleaseQueue_imp_active_sc_tcb_at'_asrt \<equiv>
      \<lambda>s'. \<forall>tcbPtr.
            (tcbInReleaseQueue |< tcbs_of' s') tcbPtr
            \<longrightarrow> (tcb_at' tcbPtr s' \<and> active_sc_tcb_at' tcbPtr s')"
diff --git a/proof/refine/RISCV64/Schedule_R.thy b/proof/refine/RISCV64/Schedule_R.thy
index d9986b314b..f634ef8b9c 100644
--- a/proof/refine/RISCV64/Schedule_R.thy
+++ b/proof/refine/RISCV64/Schedule_R.thy
@@ -64,9 +64,6 @@ crunch commitTime, refillNew, refillUpdate
 
 end
 
-global_interpretation tcbReleaseDequeue: typ_at_all_props' tcbReleaseDequeue
-  by typ_at_props'
-
 global_interpretation refillPopHead: typ_at_all_props' "refillPopHead scPtr"
   by typ_at_props'
 
@@ -2507,13 +2504,8 @@ lemma possibleSwitchTo_utr[wp]:
   "possibleSwitchTo t \<lbrace>untyped_ranges_zero'\<rbrace>"
   by (wpsimp simp: cteCaps_of_def o_def wp: untyped_ranges_zero_lift)
 
-lemma possibleSwitchTo_invs'[wp]:
-  "\<lbrace>invs' and st_tcb_at' runnable' tptr\<rbrace>
-   possibleSwitchTo tptr
-   \<lbrace>\<lambda>_. invs'\<rbrace>"
-  apply (simp add: possibleSwitchTo_def)
-  apply (wpsimp wp: hoare_vcg_imp_lift threadGet_wp inReleaseQueue_wp ssa_invs')
-  done
+crunch possibleSwitchTo
+  for invs'[wp]: invs'
 
 lemma possibleSwitchTo_sch_act_not_other:
   "\<lbrace>\<lambda>s. sch_act_not t' s \<and> t' \<noteq> t\<rbrace>
@@ -2533,22 +2525,16 @@ lemma getReleaseQueue_sp:
   by wpsimp
 
 lemma releaseQNonEmptyAndReady_implies_releaseQNonEmpty:
-  "the (releaseQNonEmptyAndReady s) \<Longrightarrow> tcbQueueHead (ksReleaseQueue s) \<noteq> None"
+  "releaseQNonEmptyAndReady s = Some True \<Longrightarrow> tcbQueueHead (ksReleaseQueue s) \<noteq> None"
   by (clarsimp simp: releaseQNonEmptyAndReady_def readReleaseQueue_def obind_def omonad_defs
               split: if_splits)
 
-lemma awaken_invs':
-  "awaken \<lbrace>invs'\<rbrace>"
-  apply (clarsimp simp: awaken_def awakenBody_def)
-  apply (rule_tac I="\<lambda>_. invs'" in valid_whileLoop; simp add: runReaderT_def)
-  apply wpsimp
-   apply (wpsimp wp: tcbReleaseDequeue_invs' hoare_drop_imps)
-  apply (fastforce intro!: releaseQNonEmptyAndReady_implies_releaseQNonEmpty)
-  done
+crunch awaken
+  for invs'[wp]: invs'
+  (wp: crunch_wps)
 
-crunch tcbReleaseDequeue
-  for st_tcb_at'[wp]: "\<lambda>s. Q (st_tcb_at' P p s)"
-  and valid_replies' [wp]: valid_replies'
+crunch tcbReleaseRemove
+  for valid_replies' [wp]: valid_replies'
   (wp: crunch_wps threadSet_pred_tcb_no_state valid_replies'_lift)
 
 crunch awaken
@@ -2813,54 +2799,6 @@ lemma setReprogramTimer_corres[corres]:
   apply (simp add: state_relation_def swp_def)
   done
 
-lemma readTCBRefillReady_no_ofail:
-  "no_ofail (\<lambda>s'. obj_at' (\<lambda>tcb. \<exists>sc. tcbSchedContext tcb = Some sc \<and> sc_at' sc s') t s')
-            (readTCBRefillReady t)"
-  unfolding readTCBRefillReady_def
-  apply (wpsimp wp: ovalid_threadRead)
-  apply (clarsimp simp: obj_at'_def)
-  done
-
-lemma gets_the_readTCBRefillReady_corres:
-  "t = t' \<Longrightarrow>
-   corres (=)
-     (active_sc_tcb_at t and active_scs_valid and valid_objs and pspace_aligned and pspace_distinct)
-     (valid_objs' and pspace_bounded')
-     (gets_the (read_tcb_refill_ready t )) (gets_the (readTCBRefillReady t'))"
-  apply (clarsimp simp: read_tcb_refill_ready_def readTCBRefillReady_def read_tcb_obj_ref_def
-                        gets_the_thread_read gets_the_assert_opt
-             simp flip: threadGet_def get_sc_refill_ready_def[simplified fun_app_def]
-                        refillReady_def)
-  apply (rule stronger_corres_guard_imp)
-    apply (rule_tac r'="(=)" in corres_split[OF threadGet_corres])
-       apply (clarsimp simp: tcb_relation_def)
-      apply (rule corres_assert_opt_l)
-      apply (rule refillReady_corres)
-      apply fastforce
-     apply (wpsimp wp: thread_get_wp)
-    apply (wpsimp wp: threadGet_wp)
-   apply (clarsimp simp: vs_all_heap_simps obj_at_def is_tcb_def is_sc_obj_def)
-   apply (intro conjI)
-    apply (fastforce elim: valid_objs_valid_sched_context_size)
-   apply (fastforce elim!: active_scs_validE[rotated]
-                   intro!: valid_refills_nonempty_refills
-                     simp: vs_all_heap_simps obj_at_def is_tcb_def is_sc_obj_def)
-  apply (normalise_obj_at', rename_tac ko)
-  apply (frule cross_relF[OF _ isScActive_cross_rel])
-   apply fastforce
-  apply (prop_tac "bound (tcbSchedContext ko)")
-   apply (clarsimp simp: obj_at'_def opt_map_def pred_map_simps)
-  apply (erule valid_objs'_valid_refills')
-   apply (rule aligned'_distinct'_obj_at'I)
-      apply (clarsimp simp: obj_at'_def opt_map_def isScActive_def pred_map_simps
-                     split: option.splits)
-     apply (fastforce intro: pspace_aligned_cross)
-    apply (fastforce intro!: pspace_distinct_cross)
-   apply fastforce
-  apply (fastforce simp: is_active_sc'_def opt_pred_def opt_map_def obj_at'_def isScActive_def
-                         pred_map_simps)
-  done
-
 lemma getReleaseQueue_corres:
   "corres (\<lambda>ls q. (ls = [] \<longleftrightarrow> tcbQueueEmpty q) \<and> (ls \<noteq> [] \<longrightarrow> tcbQueueHead q = Some (hd ls))
                   \<and> queue_end_valid ls q)
@@ -2871,24 +2809,73 @@ lemma getReleaseQueue_corres:
                     simp: release_queue_relation_def list_queue_relation_def tcbQueueEmpty_def)
   done
 
+lemma scActive_inv:
+  "scActive scPtr \<lbrace>P\<rbrace>"
+  by wpsimp
+
 lemma gets_the_releaseQNonEmptyAndReady_corres:
   "corres (=)
      (valid_release_q and active_scs_valid and valid_objs and pspace_aligned and pspace_distinct)
      (valid_objs' and pspace_bounded')
      (gets_the (read_release_q_non_empty_and_ready)) (gets_the (releaseQNonEmptyAndReady))"
-  apply (clarsimp simp: read_release_q_non_empty_and_ready_def releaseQNonEmptyAndReady_def
-                        gets_the_ogets getReleaseQueue_def[symmetric] readReleaseQueue_def
-                        gets_the_if_distrib)
+  apply (rule_tac Q'=pspace_aligned' in corres_cross_add_guard)
+   apply (fastforce dest: pspace_aligned_cross)
+  apply (rule_tac Q'=pspace_distinct' in corres_cross_add_guard)
+   apply (fastforce dest: pspace_distinct_cross)
+  apply (simp add: read_release_q_non_empty_and_ready_def releaseQNonEmptyAndReady_def
+                   gets_the_ogets readReleaseQueue_def gets_the_if_distrib
+             flip: getReleaseQueue_def)
   apply (rule stronger_corres_guard_imp)
     apply (rule corres_split[OF getReleaseQueue_corres])
-      apply (rule corres_if_strong[where R=\<top> and R'=\<top> and P=\<top>])
+      apply (rule corres_if_strong[where R=\<top> and R'=\<top> and P=\<top> and P'=\<top>])
         apply (fastforce simp: tcbQueueEmpty_def)
        apply clarsimp
-      apply (rule gets_the_readTCBRefillReady_corres)
-      apply wpsimp+
-   apply (fastforce elim: valid_release_q_active_sc)
-  apply fastforce
-  done
+      apply (simp add: read_tcb_refill_ready_def read_tcb_obj_ref_def gets_the_thread_read
+                       gets_the_assert_opt gets_the_ohaskell_assert
+                 flip: threadGet_def get_sc_refill_ready_def refillReady_def)
+      apply (rule_tac r'="(=)" in corres_split[OF threadGet_corres])
+         apply (clarsimp simp: tcb_relation_def)
+        apply (rule corres_assert_opt_l)
+        apply (rule corres_assert_gen_asm2)
+        apply (simp flip: scActive_def)
+        apply (rule corres_symb_exec_r'[where Q'=\<top>])
+           apply (rule corres_assert_gen_asm2)
+           apply (rule refillReady_corres)
+           apply fastforce
+          apply wpsimp
+         apply (rule scActive_inv)
+         apply clarsimp
+        apply wpsimp
+       apply (wpsimp wp: thread_get_wp)
+      apply (rule_tac Q'="\<lambda>rv s. \<exists>scPtr. rv = Some scPtr \<and> active_sc_at' scPtr s \<and> valid_objs' s"
+                   in hoare_post_imp)
+       apply (fastforce intro: valid_objs'_valid_refills'
+                         simp: active_sc_at'_def is_active_sc'_def obj_at'_def
+                               opt_pred_def opt_map_def)
+      apply clarsimp
+      apply (drule Some_to_the)
+      apply (wpsimp wp: hoare_vcg_ex_lift threadGet_wp)
+     apply wpsimp
+    apply wpsimp
+   apply (clarsimp simp: valid_release_q_def)
+   apply (drule_tac x="hd (release_queue s)" in bspec)
+    apply fastforce
+   apply (fastforce elim!: valid_objs_valid_sched_context_size active_scs_validE[rotated]
+                   intro!: valid_refills_nonempty_refills
+                     simp: vs_all_heap_simps obj_at_def is_tcb_def is_sc_obj_def)
+  apply (clarsimp split: if_splits)
+  apply (rename_tac head)
+  apply (frule (4) release_queue_active_sc_tcb_at_cross)
+  apply (frule state_relation_release_queue_relation)
+  apply (drule_tac x=head in spec)
+  apply (clarsimp simp: release_queue_relation_def)
+  apply (frule (3) obj_at'_tcbQueueHead_ksReleaseQueue)
+  apply (clarsimp simp: tcbQueueEmpty_def)
+  apply normalise_obj_at'
+  apply (frule (1) tcb_ko_at_valid_objs_valid_tcb')
+  by (fastforce simp: active_sc_tcb_at'_def opt_pred_def opt_map_def
+                      obj_at'_def active_sc_at'_def  valid_bound_obj'_def valid_tcb'_def
+               split: option.splits)
 
 lemma release_queue_length_well_founded:
   "wf {((r :: unit, s :: 'a state), (r', s')). length (release_queue s) < length (release_queue s')}"
@@ -2914,21 +2901,14 @@ lemma tcb_release_dequeue_release_queue_length:
   apply (clarsimp simp: read_release_q_non_empty_and_ready_simp)
   done
 
-lemma awaken_body_release_queue_length:
-  "\<lbrace>\<lambda>s'. the (read_release_q_non_empty_and_ready s') \<and> s' = s\<rbrace>
-   awaken_body
-   \<lbrace>\<lambda>_ s'. length (release_queue s') < length (release_queue s)\<rbrace>"
-  apply (clarsimp simp: awaken_body_def)
-  apply (wpsimp wp: tcb_release_dequeue_release_queue_length hoare_drop_imps)
-  done
-
 lemma awaken_terminates:
-  "whileLoop_terminates (\<lambda>_ s. (the (read_release_q_non_empty_and_ready s))) (\<lambda>_. awaken_body) r' s"
+  "whileLoop_terminates (\<lambda>_ s. (the (read_release_q_non_empty_and_ready s)))
+                        (\<lambda>_. tcb_release_dequeue) r' s"
   apply (rule_tac R="{((r', s'), (r, s)). length (release_queue s') < length (release_queue s)}"
                in whileLoop_terminates_inv)
     apply simp
    apply clarsimp
-   apply (rule awaken_body_release_queue_length)
+   apply (rule tcb_release_dequeue_release_queue_length)
   apply (rule release_queue_length_well_founded)
   done
 
@@ -3146,28 +3126,6 @@ lemma tcbReleaseRemove_corres:
      by (auto dest!: hd_in_set simp: opt_pred_def opt_map_def fun_upd_apply split: option.splits)
   by (auto simp: in_opt_pred opt_map_red fun_upd_apply split: option.splits)
 
-lemma tcbReleaseDequeue_corres:
-  "corres (=)
-     (pspace_aligned and pspace_distinct and valid_release_q and (\<lambda>s. release_queue s \<noteq> [])
-      and ready_or_release)
-     (sym_heap_sched_pointers and valid_objs')
-     tcb_release_dequeue tcbReleaseDequeue"
-  apply (clarsimp simp: tcb_release_dequeue_def tcbReleaseDequeue_def)
-  apply (rule corres_symb_exec_l[rotated, OF _ gets_sp]; wpsimp?)
-  apply (rename_tac rlq)
-  apply (rule corres_symb_exec_r[rotated, OF getReleaseQueue_sp]; wpsimp?)
-  apply (rename_tac queue)
-  apply (rule_tac F="rlq \<noteq> [] \<and> hd rlq = the (tcbQueueHead queue)" in corres_req)
-   apply (drule state_relation_release_queue_relation)
-   apply (clarsimp simp: list_queue_relation_def release_queue_relation_def)
-   apply (fastforce dest: heap_path_head heap_ls_unique)
-  apply (corresKsimp corres: tcbReleaseRemove_corres)
-  apply (drule state_relation_release_queue_relation)
-  apply (clarsimp simp: release_queue_relation_def list_queue_relation_def)
-  apply (fastforce dest: heap_path_head
-                   simp: valid_release_q_def  vs_all_heap_simps obj_at_def is_tcb_def)
-  done
-
 lemma tcbInReleaseQueue_update_valid_tcbs'[wp]:
   "threadSet (tcbInReleaseQueue_update f) tcbPtr \<lbrace>valid_tcbs'\<rbrace>"
   by (wpsimp wp: threadSet_valid_tcbs')
@@ -3181,107 +3139,91 @@ lemma tcbQueueRemove_valid_tcbs'[wp]:
 
 crunch tcbReleaseDequeue
   for valid_tcbs'[wp]: valid_tcbs'
+  and valid_sched_pointers[wp]: valid_sched_pointers
+  (wp: crunch_wps)
 
-crunch tcbReleaseDequeue
-  for valid_sched_pointers[wp]: valid_sched_pointers
-
-lemma tcb_release_dequeue_runnable_tcb_at_rv:
-  "\<lbrace>\<lambda>s. release_queue s \<noteq> [] \<and> valid_release_q s\<rbrace>
-   tcb_release_dequeue
-   \<lbrace>\<lambda>rv s. st_tcb_at runnable rv s\<rbrace>"
-  apply (clarsimp simp: tcb_release_dequeue_def)
-  apply wpsimp
-  apply (fastforce simp: valid_release_q_def vs_all_heap_simps obj_at_kh_kheap_simps is_tcb_def)
-  done
-
-crunch tcb_release_dequeue
-  for valid_sched_action[wp]: valid_sched_action
-  and pspace_aligned[wp]: pspace_aligned
-  and pspace_distinct[wp]: pspace_distinct
-  and valid_tcbs[wp]: valid_tcbs
-  and active_sc_valid_refills[wp]: active_scs_valid
-  and ready_or_release[wp]: ready_or_release
-  and valid_ready_qs[wp]: valid_ready_qs
+crunch tcb_release_remove
+  for ready_qs_distinct[wp]: ready_qs_distinct
   and in_correct_ready_q[wp]: in_correct_ready_q
-  and ready_qs_distinct[wp]: ready_qs_distinct
-  and valid_objs[wp]: valid_objs
   (rule: in_correct_ready_q_lift simp: crunch_simps ready_qs_distinct_def)
 
-lemma tcb_release_dequeue_not_in_release_q[wp]:
-  "\<lbrace>\<top>\<rbrace> tcb_release_dequeue \<lbrace>not_in_release_q\<rbrace>"
-  unfolding tcb_release_dequeue_def
-  by wpsimp
+defs tcbQueueHead_ksReleaseQueue_active_sc_tcb_at'_asrt_def:
+  "tcbQueueHead_ksReleaseQueue_active_sc_tcb_at'_asrt s \<equiv>
+     \<forall>head. tcbQueueHead (ksReleaseQueue s) = Some head \<longrightarrow> active_sc_tcb_at' head s"
 
-lemma awakenBody_corres:
+lemma tcbReleaseDequeue_corres:
   "corres dc
-     (pspace_aligned and pspace_distinct and valid_objs and valid_sched_action
-      and valid_tcbs and in_correct_ready_q and ready_qs_distinct
+     (pspace_aligned and pspace_distinct and valid_sched_action
+      and valid_objs and in_correct_ready_q and ready_qs_distinct
       and active_scs_valid and ready_or_release
-      and (\<lambda>s. valid_release_q s \<and> release_queue s \<noteq> []))
-     (valid_objs' and valid_sched_pointers and sym_heap_sched_pointers
-      and pspace_aligned' and pspace_distinct' and pspace_bounded')
-     awaken_body awakenBody"
-  (is "corres _ (?abs_inv and _) ?conc _ _")
-  apply (clarsimp simp: awaken_body_def awakenBody_def)
-  apply (rule_tac P="\<lambda>rv. ?abs_inv and not_in_release_q rv and st_tcb_at runnable rv"
-              and P'="\<lambda>_. ?conc"
-               in corres_underlying_split_ex_abs)
-     apply (corres corres: tcbReleaseDequeue_corres)
-    apply clarsimp
-    apply (rule corres_symb_exec_r_conj_ex_abs_forwards[OF _ isRunnable_sp, rotated];
-           (solves wpsimp)?)
-     apply wpsimp
-     apply (fastforce elim!: tcb_at_cross dest: state_relation_pspace_relation simp: ex_abs_def)
-    apply (rule corres_symb_exec_r_conj_ex_abs_forwards[OF _ assert_sp, rotated]; (solves wpsimp)?)
-     apply wpsimp
-     apply (fastforce dest: st_tcb_at_runnable_cross
-                      simp: ex_abs_def pred_tcb_at'_def obj_at'_def runnable_eq_active')
-    apply (corres corres: possibleSwitchTo_corres)
-   apply (wpsimp wp: tcb_release_dequeue_runnable_tcb_at_rv)
-  apply wpsimp
+      and valid_release_q and (\<lambda>s. release_queue s \<noteq> []))
+     (valid_objs' and valid_sched_pointers and sym_heap_sched_pointers and pspace_bounded')
+     tcb_release_dequeue tcbReleaseDequeue"
+  apply (rule_tac Q'=pspace_aligned' in corres_cross_add_guard)
+   apply (fastforce dest: pspace_aligned_cross)
+  apply (rule_tac Q'=pspace_distinct' in corres_cross_add_guard)
+   apply (fastforce dest: pspace_distinct_cross)
+  apply (clarsimp simp: tcb_release_dequeue_def tcbReleaseDequeue_def)
+  apply (rule corres_stateAssert_add_assertion[rotated])
+   apply (fastforce intro: ksReleaseQueue_asrt_cross)
+  apply (rule corres_stateAssert_add_assertion[rotated])
+   apply (fastforce simp: tcbInReleaseQueue_imp_active_sc_tcb_at'_asrt_def
+                   dest!: release_queue_active_sc_tcb_at_cross)
+  apply (rule stronger_corres_guard_imp)
+    apply (rule corres_split[OF getReleaseQueue_corres])
+      apply clarsimp
+      apply (rename_tac rlq queue)
+      apply (rule corres_symb_exec_r_conj_ex_abs_forwards)
+         apply (rule corres_assert_assume_r)
+         apply (rule_tac F="rlq \<noteq> []" in corres_gen_asm)
+         apply simp
+         apply (rule corres_split[OF tcbReleaseRemove_corres])
+            apply fastforce
+           apply (rule corres_add_noop_lhs2)
+           apply (rule corres_add_noop_rhs2)
+           apply (simp only: bind_assoc)
+           apply (rule corres_split[OF possibleSwitchTo_corres])
+              apply fastforce
+             apply (rule corres_symb_exec_r_conj_ex_abs[where P'=\<top> and P=\<top>])
+                apply (rule corres_symb_exec_r_conj_ex_abs
+                             [where P'=\<top>
+                                and P="valid_release_q and pspace_aligned and pspace_distinct
+                                       and valid_objs"])
+                   apply (rule corres_return_trivial)
+                  apply wpsimp
+                 apply wpsimp
+                apply (wpsimp wp: no_fail_stateAssert)
+                apply (clarsimp simp: ex_abs_def)
+                apply (frule (4) release_queue_active_sc_tcb_at_cross)
+                apply (fastforce dest!: state_relation_release_queue_relation
+                                        tcbQueueHead_ksReleaseQueue
+                                  simp: tcbQueueHead_ksReleaseQueue_active_sc_tcb_at'_asrt_def
+                                        release_queue_relation_def tcbQueueEmpty_def)
+               apply wpsimp+
+             apply (wpsimp wp: no_fail_stateAssert)
+             apply (fastforce intro: ksReleaseQueue_asrt_cross simp: ex_abs_def)
+            apply wpsimp+
+   apply (fastforce dest!: hd_in_set
+                     simp: valid_release_q_def vs_all_heap_simps pred_tcb_at_def obj_at_def is_tcb_def)
+  apply (fastforce dest: state_relation_release_queue_relation heap_path_head
+                 intro!: st_tcb_at_runnable_cross
+                   simp: valid_release_q_def vs_all_heap_simps pred_tcb_at_def obj_at_def
+                         release_queue_relation_def list_queue_relation_def)
   done
 
-crunch tcb_release_dequeue
-  for weak_valid_sched_action[wp]: weak_valid_sched_action
-
-crunch awakenBody
-  for sym_heap_sched_pointers[wp]: sym_heap_sched_pointers
-  (wp: crunch_wps)
-
 crunch tcbReleaseDequeue
   for weak_sch_act_wf[wp]: "\<lambda>s'. weak_sch_act_wf (ksSchedulerAction s') s'"
+  (wp: crunch_wps)
 
 crunch tcb_release_dequeue
   for pred_tcb_at[wp]: "\<lambda>s. Q (pred_tcb_at proj P tptr s)"
   and released_sc_tcb_at[wp]: "released_sc_tcb_at t"
 
-lemma read_tcb_refill_ready_released_sc_tcb_at:
-  "\<lbrakk>active_sc_tcb_at tcb_ptr s; read_tcb_refill_ready tcb_ptr s = Some True\<rbrakk>
-   \<Longrightarrow> released_sc_tcb_at tcb_ptr s"
-  by (fastforce dest: read_refill_head_SomeD
-                simp: read_tcb_refill_ready_def vs_all_heap_simps read_tcb_obj_ref_def
-                      thread_read_def omonad_defs oliftM_def  get_tcb_def read_sc_refill_ready_def
-                      read_sched_context_def)
-
-lemma awaken_body_valid_ready_qs:
-  "\<lbrace>\<lambda>s. valid_release_q s \<and> valid_ready_qs s \<and> read_release_q_non_empty_and_ready s = Some True\<rbrace>
-   awaken_body
-   \<lbrace>\<lambda>_. valid_ready_qs\<rbrace>"
-  apply (clarsimp simp: awaken_body_def)
-  apply (wpsimp wp: possible_switch_to_valid_ready_qs hoare_disjI2 hoare_vcg_all_lift
-                    hoare_vcg_imp_lift'
-              simp: tcb_release_dequeue_def)
-  apply (simp add: read_release_q_non_empty_and_ready_simp split: if_splits)
-  apply (rule conjI)
-   apply (fastforce dest: hd_in_set simp: valid_release_q_def vs_all_heap_simps obj_at_def)
-  apply (fastforce intro: valid_release_q_active_sc read_tcb_refill_ready_released_sc_tcb_at)
-  done
-
-crunch awaken_body
+crunch tcb_release_dequeue
   for in_correct_ready_q[wp]: in_correct_ready_q
   (rule: in_correct_ready_q_lift ignore: tcb_sched_action)
 
-crunch awaken_body
+crunch tcb_release_dequeue
   for ready_qs_distinct[wp]: ready_qs_distinct
   (rule: ready_qs_distinct_lift ignore: tcb_sched_action wp: crunch_wps)
 
@@ -3294,6 +3236,11 @@ lemma awaken_corres:
       and pspace_aligned' and pspace_distinct' and pspace_bounded')
      Schedule_A.awaken awaken"
   apply (clarsimp simp: awaken_def Schedule_A.awaken_def runReaderT_def)
+  apply (rule corres_stateAssert_ignore)
+   apply (fastforce intro: ksReleaseQueue_asrt_cross)
+  apply (rule corres_stateAssert_ignore)
+   apply (fastforce simp: tcbInReleaseQueue_imp_active_sc_tcb_at'_asrt_def
+                   dest!: release_queue_active_sc_tcb_at_cross)
   apply (rule corres_whileLoop_abs; simp)
       apply (rule_tac f=read_release_q_non_empty_and_ready
                   and f'=releaseQNonEmptyAndReady
@@ -3304,16 +3251,17 @@ lemma awaken_corres:
        apply fastforce
       apply (clarsimp simp: no_ofail_def)
       apply (erule (1) valid_release_q_read_release_q_non_empty_and_ready_bound)
-     apply (corresKsimp corres: awakenBody_corres)
-     apply (fastforce simp: read_release_q_non_empty_and_ready_simp)
+     apply (corres corres: tcbReleaseDequeue_corres)
+      apply (fastforce simp: read_release_q_non_empty_and_ready_simp)
+     apply fastforce
     apply (clarsimp simp: pred_conj_def)
     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_sched_action)
+           (solves \<open>wpsimp simp: tcb_release_dequeue_def\<close>)?)
+    apply (wpsimp wp: tcb_release_dequeue_valid_sched_action)
     apply (frule valid_release_q_read_release_q_non_empty_and_ready_bound)
      apply fastforce
     apply (fastforce dest: read_release_q_non_empty_and_ready_True_simp)
-   apply ((wpsimp simp: awakenBody_def | wpsimp wp: hoare_drop_imps)+)[1]
+   apply ((wpsimp simp: tcbReleaseDequeue_def | wpsimp wp: hoare_drop_imps)+)[1]
   apply (fastforce intro!: awaken_terminates)
   done
 
diff --git a/proof/refine/RISCV64/TcbAcc_R.thy b/proof/refine/RISCV64/TcbAcc_R.thy
index 204f79e9d0..9bd166d61d 100644
--- a/proof/refine/RISCV64/TcbAcc_R.thy
+++ b/proof/refine/RISCV64/TcbAcc_R.thy
@@ -2116,8 +2116,8 @@ crunch setReprogramTimer, setReleaseQueue, setQueue, removeFromBitmap
    simp: crunch_simps tcb_cte_cases_def tcb_bound_refs'_def cur_tcb'_def threadSet_cur
          bitmap_fun_defs valid_machine_state'_def)
 
-crunch tcbReleaseDequeue, tcbReleaseEnqueue,
-         tcbSchedEnqueue, tcbSchedAppend, tcbSchedDequeue, setQueue
+crunch tcbReleaseRemove, tcbReleaseEnqueue,
+       tcbSchedEnqueue, tcbSchedAppend, tcbSchedDequeue, setQueue
   for pspace_aligned'[wp]: pspace_aligned'
   and state_refs_of'[wp]: "\<lambda>s. P (state_refs_of' s)"
   and pspace_distinct'[wp]: pspace_distinct'
@@ -2147,7 +2147,7 @@ crunch tcbReleaseDequeue, tcbReleaseEnqueue,
   (wp: crunch_wps threadSet_state_refs_of'[where f'=id and g'=id]
    simp: crunch_simps tcb_cte_cases_def tcb_bound_refs'_def bitmap_fun_defs)
 
-crunch tcbReleaseDequeue, tcbReleaseEnqueue
+crunch tcbReleaseRemove, tcbReleaseEnqueue
   for valid_machine_state'[wp]: valid_machine_state'
   (wp: crunch_wps)
 
@@ -6087,19 +6087,19 @@ lemma setReleaseQueue_pred_tcb_at'[wp]:
 global_interpretation tcbReleaseRemove: typ_at_all_props' "tcbReleaseRemove tptr"
   by typ_at_props'
 
-crunch tcbReleaseDequeue, tcbQueueRemove, tcbReleaseEnqueue
+crunch tcbReleaseRemove, tcbQueueRemove, tcbReleaseEnqueue
   for valid_irq_handlers'[wp]: valid_irq_handlers'
   (wp: valid_irq_handlers_lift'')
 
-crunch tcbReleaseDequeue, tcbQueueRemove, tcbReleaseEnqueue
+crunch tcbReleaseRemove, tcbQueueRemove, tcbReleaseEnqueue
   for ct_idle_or_in_cur_domain'[wp]: ct_idle_or_in_cur_domain'
   (wp: crunch_wps threadSet_ct_idle_or_in_cur_domain')
 
-crunch tcbReleaseDequeue, tcbQueueRemove, tcbReleaseEnqueue
+crunch tcbReleaseRemove, tcbQueueRemove, tcbReleaseEnqueue
   for if_unsafe_then_cap'[wp]: if_unsafe_then_cap'
   (wp: crunch_wps threadSet_ifunsafe'T simp: tcb_cte_cases_def cteSizeBits_def)
 
-crunch tcbReleaseDequeue, tcbQueueRemove, tcbReleaseEnqueue
+crunch tcbReleaseRemove, tcbQueueRemove, tcbReleaseEnqueue
   for ctes_of[wp]: "\<lambda>s. P (ctes_of s)"
   and valid_idle'[wp]: valid_idle'
   (simp: crunch_simps wp: crunch_wps threadSet_idle')
@@ -6108,14 +6108,14 @@ crunch setReleaseQueue, tcbQueueRemove, setReprogramTimer
   for valid_objs'[wp]: valid_objs'
   (wp: crunch_wps hoare_vcg_all_lift simp: crunch_simps)
 
-crunch tcbReleaseDequeue
+crunch tcbReleaseRemove
   for valid_objs'[wp]: valid_objs'
 
-crunch tcbReleaseDequeue, tcbQueueRemove, tcbReleaseEnqueue
+crunch tcbReleaseRemove, tcbQueueRemove, tcbReleaseEnqueue
   for pred_tcb_at'[wp]: "\<lambda>s. P' (pred_tcb_at' P obj t s)"
   (wp: crunch_wps threadSet_pred_tcb_no_state simp: tcb_to_itcb'_def)
 
-crunch tcbReleaseDequeue, tcbQueueRemove, tcbReleaseEnqueue
+crunch tcbReleaseRemove, tcbQueueRemove, tcbReleaseEnqueue
   for tcbDomain[wp]: "obj_at' (\<lambda>tcb. P (tcbDomain tcb)) t"
   and tcb_in_cur_domain'[wp]: "tcb_in_cur_domain' t"
   and sch_act_wf[wp]: "\<lambda>s. sch_act_wf (ksSchedulerAction s) s"
@@ -6478,7 +6478,7 @@ lemma tcbReleaseRemove_sym_heap_sched_pointers[wp]:
   apply (fastforce simp: ksReleaseQueue_asrt_def opt_pred_def obj_at'_def opt_map_red)
   done
 
-crunch tcbReleaseDequeue
+crunch tcbReleaseRemove
   for sym_heap_sched_pointers[wp]: sym_heap_sched_pointers
 
 crunch setReprogramTimer
@@ -6574,11 +6574,6 @@ lemma tcbReleaseRemove_invs':
               simp: cteCaps_of_def o_def)
   done
 
-lemma tcbReleaseDequeue_invs'[wp]:
-  "tcbReleaseDequeue \<lbrace>invs'\<rbrace>"
-  unfolding tcbReleaseDequeue_def
-  by (wpsimp wp: tcbReleaseRemove_invs')
-
 crunch setReleaseQueue, setReprogramTimer
   for valid_bitmapQ[wp]: valid_bitmapQ
   and bitmapQ_no_L2_orphans[wp]: bitmapQ_no_L2_orphans
diff --git a/spec/abstract/Schedule_A.thy b/spec/abstract/Schedule_A.thy
index f8237edfcf..6e1c3d50a6 100644
--- a/spec/abstract/Schedule_A.thy
+++ b/spec/abstract/Schedule_A.thy
@@ -146,24 +146,17 @@ where
      else read_tcb_refill_ready (hd rq)
    }"
 
-definition tcb_release_dequeue :: "(obj_ref, 'z::state_ext) s_monad"
-where
-  "tcb_release_dequeue = do
+definition tcb_release_dequeue :: "(unit, 'z::state_ext) s_monad" where
+  "tcb_release_dequeue \<equiv> do
      rq \<leftarrow> gets release_queue;
+     assert (rq \<noteq> []);
      tcb_release_remove (hd rq);
-     return (hd rq)
+     possible_switch_to (hd rq)
    od"
 
-definition awaken_body :: "(unit, 'z::state_ext) s_monad"
-where
-  "awaken_body = do
-     awakened \<leftarrow> tcb_release_dequeue;
-     possible_switch_to awakened
-   od"
-
-definition awaken :: "(unit, 'z::state_ext) s_monad"
-where
-  "awaken \<equiv> whileLoop (\<lambda>r s. the (read_release_q_non_empty_and_ready s)) (\<lambda>_. awaken_body) ()"
+definition awaken :: "(unit, 'z::state_ext) s_monad" where
+  "awaken \<equiv> whileLoop (\<lambda>r s. the (read_release_q_non_empty_and_ready s))
+                       (\<lambda>_. tcb_release_dequeue) ()"
 
 definition max_non_empty_queue :: "(priority \<Rightarrow> ready_queue) \<Rightarrow> ready_queue" where
   "max_non_empty_queue queues \<equiv> queues (Max {prio. queues prio \<noteq> []})"
diff --git a/spec/design/skel/KernelStateData_H.thy b/spec/design/skel/KernelStateData_H.thy
index b67579130b..40179a2dce 100644
--- a/spec/design/skel/KernelStateData_H.thy
+++ b/spec/design/skel/KernelStateData_H.thy
@@ -100,7 +100,7 @@ where
     return r
   od"
 
-#INCLUDE_HASKELL SEL4/Model/StateData.lhs decls_only ONLY capHasProperty sym_refs_asrt valid_replies'_sc_asrt ready_qs_runnable tcs_cross_asrt1 tcs_cross_asrt2 ct_not_inQ_asrt sch_act_wf_asrt valid_idle'_asrt cur_tcb'_asrt sch_act_sane_asrt ct_not_ksQ_asrt ct_active'_asrt rct_imp_activatable'_asrt ct_activatable'_asrt ready_or_release'_asrt findTimeAfter_asrt not_tcbInReleaseQueue_asrt tcbInReleaseQueue_imp_active_sc_tc_at'_asrt not_tcbQueued_asrt ksReadyQueues_asrt ksReleaseQueue_asrt idleThreadNotQueued sc_at'_asrt valid_tcbs'_asrt
-#INCLUDE_HASKELL SEL4/Model/StateData.lhs NOT doMachineOp KernelState ReadyQueue ReleaseQueue ReaderM Kernel KernelR getsJust assert stateAssert funOfM condition whileLoop findM funArray newKernelState capHasProperty ifM whenM whileM andM orM sym_refs_asrt valid_replies'_sc_asrt ready_qs_runnable tcs_cross_asrt1 tcs_cross_asrt2 ct_not_inQ_asrt sch_act_wf_asrt valid_idle'_asrt cur_tcb'_asrt sch_act_sane_asrt ct_not_ksQ_asrt ct_active'_asrt rct_imp_activatable'_asrt ct_activatable'_asrt ready_or_release'_asrt findTimeAfter_asrt not_tcbInReleaseQueue_asrt tcbInReleaseQueue_imp_active_sc_tc_at'_asrt not_tcbQueued_asrt ksReadyQueues_asrt ksReleaseQueue_asrt idleThreadNotQueued sc_at'_asrt valid_tcbs'_asrt
+#INCLUDE_HASKELL SEL4/Model/StateData.lhs decls_only ONLY capHasProperty sym_refs_asrt valid_replies'_sc_asrt ready_qs_runnable tcs_cross_asrt1 tcs_cross_asrt2 ct_not_inQ_asrt sch_act_wf_asrt valid_idle'_asrt cur_tcb'_asrt sch_act_sane_asrt ct_not_ksQ_asrt ct_active'_asrt rct_imp_activatable'_asrt ct_activatable'_asrt ready_or_release'_asrt findTimeAfter_asrt not_tcbInReleaseQueue_asrt tcbInReleaseQueue_imp_active_sc_tcb_at'_asrt tcbQueueHead_ksReleaseQueue_active_sc_tcb_at'_asrt not_tcbQueued_asrt ksReadyQueues_asrt ksReleaseQueue_asrt idleThreadNotQueued sc_at'_asrt valid_tcbs'_asrt
+#INCLUDE_HASKELL SEL4/Model/StateData.lhs NOT doMachineOp KernelState ReadyQueue ReleaseQueue ReaderM Kernel KernelR getsJust assert stateAssert funOfM condition whileLoop findM funArray newKernelState capHasProperty ifM whenM whileM andM orM sym_refs_asrt valid_replies'_sc_asrt ready_qs_runnable tcs_cross_asrt1 tcs_cross_asrt2 ct_not_inQ_asrt sch_act_wf_asrt valid_idle'_asrt cur_tcb'_asrt sch_act_sane_asrt ct_not_ksQ_asrt ct_active'_asrt rct_imp_activatable'_asrt ct_activatable'_asrt ready_or_release'_asrt findTimeAfter_asrt not_tcbInReleaseQueue_asrt tcbInReleaseQueue_imp_active_sc_tcb_at'_asrt tcbQueueHead_ksReleaseQueue_active_sc_tcb_at'_asrt not_tcbQueued_asrt ksReadyQueues_asrt ksReleaseQueue_asrt idleThreadNotQueued sc_at'_asrt valid_tcbs'_asrt
 
 end
diff --git a/spec/haskell/src/SEL4/Model/StateData.lhs b/spec/haskell/src/SEL4/Model/StateData.lhs
index 589bcd7972..adc2e392c5 100644
--- a/spec/haskell/src/SEL4/Model/StateData.lhs
+++ b/spec/haskell/src/SEL4/Model/StateData.lhs
@@ -494,8 +494,14 @@ An assert that will say that the tcbInReleaseQueue flag is not set.
 An assert that will say that every thread in the release queue is associated
 with an active scheduling context.
 
-> tcbInReleaseQueue_imp_active_sc_tc_at'_asrt :: KernelState -> Bool
-> tcbInReleaseQueue_imp_active_sc_tc_at'_asrt _ = True
+> tcbInReleaseQueue_imp_active_sc_tcb_at'_asrt :: KernelState -> Bool
+> tcbInReleaseQueue_imp_active_sc_tcb_at'_asrt _ = True
+
+An assert that will say that if the release queue is not empty, then the head
+of the release queue is associated with an active scheduling context.
+
+> tcbQueueHead_ksReleaseQueue_active_sc_tcb_at'_asrt :: KernelState -> Bool
+> tcbQueueHead_ksReleaseQueue_active_sc_tcb_at'_asrt _ = True
 
 An assert that will say that the tcbQueued flag of the thread is not set.
 
diff --git a/spec/haskell/src/SEL4/Object/SchedContext.lhs b/spec/haskell/src/SEL4/Object/SchedContext.lhs
index d36482fe7e..ea3711294f 100644
--- a/spec/haskell/src/SEL4/Object/SchedContext.lhs
+++ b/spec/haskell/src/SEL4/Object/SchedContext.lhs
@@ -24,7 +24,7 @@ This module uses the C preprocessor to select a target architecture.
 >         refillCapacity, readRefillCapacity, getRefillCapacity, refillBudgetCheck,
 >         refillBudgetCheckRoundRobin, updateSchedContext, emptyRefill,
 >         isCurDomainExpired, refillUnblockCheck,ifCondRefillUnblockCheck,
->         readRefillReady, refillReady, tcbReleaseEnqueue, tcbQueueRemove, tcbReleaseDequeue,
+>         readRefillReady, refillReady, tcbReleaseEnqueue, tcbQueueRemove,
 >         refillSufficient, readRefillSufficient, getRefillSufficient, postpone,
 >         schedContextDonate, maybeDonateSc, maybeReturnSc, schedContextUnbindNtfn,
 >         schedContextMaybeUnbindNtfn, isRoundRobin, getRefills, setRefills, getRefillFull,
@@ -32,7 +32,7 @@ This module uses the C preprocessor to select a target architecture.
 >         schedContextUnbindReply, schedContextSetInactive, unbindFromSC,
 >         schedContextCancelYieldTo, refillAbsoluteMax, schedContextUpdateConsumed,
 >         scReleased, setConsumed, refillResetRR, preemptionPoint, refillHdInsufficient,
->         nonOverlappingMergeRefills, headInsufficientLoop, maxReleaseTime, scActive
+>         nonOverlappingMergeRefills, headInsufficientLoop, maxReleaseTime, readScActive, scActive
 >     ) where
 
 \begin{impdetails}
@@ -803,8 +803,8 @@ This module uses the C preprocessor to select a target architecture.
 
 > findTimeAfter :: Maybe (PPtr TCB) -> Time -> Kernel (Maybe (PPtr TCB))
 > findTimeAfter tcbPtrOpt newTime = do
->     stateAssert tcbInReleaseQueue_imp_active_sc_tc_at'_asrt
->         "Every thread in the release queue is associated with an active scheduling context"
+>     stateAssert tcbInReleaseQueue_imp_active_sc_tcb_at'_asrt
+>         "every thread in the release queue is associated with an active scheduling context"
 >     whileLoop (\afterPtrOpt -> fromJust . runReaderT (timeAfter afterPtrOpt newTime))
 >               (\afterPtrOpt -> do
 >                   tcb <- getObject (fromJust afterPtrOpt)
@@ -848,13 +848,6 @@ This module uses the C preprocessor to select a target architecture.
 >                   tcbQueueInsert tcbPtr afterPtr)
 >     threadSet (\t -> t { tcbInReleaseQueue = True }) tcbPtr
 
-> tcbReleaseDequeue :: Kernel (PPtr TCB)
-> tcbReleaseDequeue = do
->     queue <- getReleaseQueue
->     tcbPtr <- return $ fromJust $ tcbQueueHead queue
->     tcbReleaseRemove tcbPtr
->     return tcbPtr
-
 In preemptible code, the kernel may explicitly mark a preemption point with the "preemptionPoint" function. The preemption will only be taken if an interrupt has occurred and the preemption point has been called "workUnitsLimit" times.
 
 > workUnitsLimit = error "see Kernel_Config"
diff --git a/spec/haskell/src/SEL4/Object/TCB.lhs b/spec/haskell/src/SEL4/Object/TCB.lhs
index 7e30165bed..8a357d8385 100644
--- a/spec/haskell/src/SEL4/Object/TCB.lhs
+++ b/spec/haskell/src/SEL4/Object/TCB.lhs
@@ -1077,27 +1077,41 @@ On some architectures, the thread context may include registers that may be modi
 >         commitTime
 >     setCurSc ctScPtr
 
-> readTCBRefillReady :: PPtr TCB -> KernelR Bool
-> readTCBRefillReady tcbPtr = do
->      scOpt <- threadRead tcbSchedContext tcbPtr
->      readRefillReady $ fromJust scOpt
-
 > releaseQNonEmptyAndReady :: KernelR Bool
 > releaseQNonEmptyAndReady = do
 >     rq <- readReleaseQueue
 >     if (tcbQueueHead rq == Nothing)
 >       then return False
->       else readTCBRefillReady (fromJust $ tcbQueueHead rq)
-
-> awakenBody :: Kernel ()
-> awakenBody = do
->     awakened <- tcbReleaseDequeue
+>       else do
+>           let head = fromJust (tcbQueueHead rq)
+>           scOpt <- threadRead tcbSchedContext head
+>           assert (scOpt /= Nothing) "the head of the release queue must have an associated scheduling context"
+>           let scPtr = fromJust scOpt
+>           active <- readScActive scPtr
+>           assert active "the scheduling context associated with the head of the release queue must be active"
+>           readRefillReady scPtr
+
+> tcbReleaseDequeue :: Kernel ()
+> tcbReleaseDequeue = do
+>     stateAssert ksReleaseQueue_asrt ""
+>     stateAssert tcbInReleaseQueue_imp_active_sc_tcb_at'_asrt
+>         "every thread in the release queue is associated with an active scheduling context"
+>     queue <- getReleaseQueue
+>     awakened <- return $ fromJust $ tcbQueueHead queue
 >     runnable <- isRunnable awakened
 >     assert runnable "the awakened thread must be runnable"
+>     tcbReleaseRemove awakened
 >     possibleSwitchTo awakened
+>     stateAssert ksReleaseQueue_asrt ""
+>     stateAssert tcbQueueHead_ksReleaseQueue_active_sc_tcb_at'_asrt
+>         "if the release queue is not empty, then the head of the release queue is associated with an active scheduling context"
 
 > awaken :: Kernel ()
-> awaken = whileLoop (const (fromJust . runReaderT releaseQNonEmptyAndReady)) (const awakenBody) ()
+> awaken = do
+>     stateAssert ksReleaseQueue_asrt ""
+>     stateAssert tcbInReleaseQueue_imp_active_sc_tcb_at'_asrt
+>         "every thread in the release queue is associated with an active scheduling context"
+>     whileLoop (const (fromJust . runReaderT releaseQNonEmptyAndReady)) (const tcbReleaseDequeue) ()
 
 > tcbEPFindIndex :: PPtr TCB -> [PPtr TCB] -> Int -> Kernel Int
 > tcbEPFindIndex tptr queue curIndex = do