diff --git a/proof/crefine/RISCV64/SchedContext_C.thy b/proof/crefine/RISCV64/SchedContext_C.thy
index b53b8efd9d..33281d54d8 100644
--- a/proof/crefine/RISCV64/SchedContext_C.thy
+++ b/proof/crefine/RISCV64/SchedContext_C.thy
@@ -584,11 +584,251 @@ lemma schedContext_updateConsumed_ccorres:
 sorry (* FIXME RT: schedContext_updateConsumed_ccorres *)
 
 lemma invokeSchedControl_ConfigureFlags_ccorres:
-  "ccorres dc xfdc
-     invs' UNIV []
-     (invokeSchedControlConfigureFlags iv)
+  "ccorres (K (K \<bottom>) \<currency> dc) (liftxf errstate id (K ()) ret__unsigned_long_')
+     (invs' and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s)
+      and valid_sc_ctrl_inv'
+            (InvokeSchedControlConfigureFlags scPtr budget period mRefills badge flags))
+     (\<lbrace>\<acute>target___ptr_to_struct_sched_context_C = Ptr scPtr\<rbrace>
+      \<inter> \<lbrace>\<acute>budget = budget\<rbrace> \<inter> \<lbrace>\<acute>period = period\<rbrace> \<inter> \<lbrace>\<acute>max_refills = of_nat mRefills\<rbrace>
+      \<inter> \<lbrace>\<acute>badge___unsigned_long = badge\<rbrace> \<inter> \<lbrace>\<acute>flags = flags\<rbrace>) hs
+     (liftE (invokeSchedControlConfigureFlags
+              (InvokeSchedControlConfigureFlags scPtr budget period mRefills badge flags)))
      (Call invokeSchedControl_ConfigureFlags_'proc)"
-sorry (* FIXME RT: invokeSchedControl_ConfigureFlags_ccorres *)
+  supply Collect_const [simp del]
+  apply (cinit' lift: target___ptr_to_struct_sched_context_C_' budget_' period_' max_refills_'
+                      badge___unsigned_long_' flags_'
+                simp: invokeSchedControlConfigureFlags_def gets_bind_ign liftE_liftM)
+   apply (rule ccorres_pre_getObject_sc, rename_tac sc)
+   apply (rule ccorres_move_c_guard_sc)
+   apply (rule_tac xf'=thread_'
+               and val="option_to_ctcb_ptr (scTCB sc)"
+               and R="obj_at' (\<lambda>sc'. scTCB sc' = scTCB sc) scPtr and valid_objs'"
+                in ccorres_symb_exec_r_known_rv[where R'="UNIV"])
+      apply (rule conseqPre, vcg)
+      apply (fastforce dest: obj_at_cslift_sc simp: csched_context_relation_def typ_heap_simps)
+     apply ceqv
+    apply (rule_tac r'=dc and xf'=xfdc in ccorres_split_nothrow_novcg)
+        apply (clarsimp simp: when_def)
+        apply (rule_tac Q="obj_at' (\<lambda>sc'. scTCB sc' = scTCB sc) scPtr and valid_objs'"
+                     in ccorres_cond_both'[where Q'=\<top>])
+          apply normalise_obj_at'
+          apply (frule (1) sc_ko_at_valid_objs_valid_sc')
+          apply (clarsimp simp: valid_sched_context'_def option_to_ctcb_ptr_def)
+          apply (case_tac "scTCB sc"; clarsimp)
+          apply (fastforce dest: tcb_at_not_NULL)
+         (* target sc is associated with a thread, which we remove from scheduler queues,
+            and then possibly commit the time *)
+         apply clarsimp
+         apply (drule Some_to_the)
+         apply (clarsimp simp: option_to_ctcb_ptr_def split: option.splits)
+         apply (rule ccorres_rhs_assoc)
+         apply (ctac (no_vcg) add: tcbReleaseRemove_ccorres)
+          apply (ctac (no_vcg) add: tcbSchedDequeue_ccorres)
+           apply (rule ccorres_pre_getCurSc)
+           apply (rule_tac Q="\<lambda>s. curSc = ksCurSc s" in ccorres_cond_both'[where Q'=\<top>])
+             apply (fastforce dest: rf_sr_ksCurSC)
+            apply (ctac (no_vcg) add: commitTime_ccorres)
+           apply (rule ccorres_return_Skip)
+          apply (wpsimp wp: hoare_drop_imps)
+         apply (wpsimp wp: tcbReleaseRemove_invs')
+        apply (rule ccorres_return_Skip)
+       apply ceqv
+      apply (rule_tac r'=dc and xf'=xfdc in ccorres_split_nothrow_novcg)
+          apply (rule ccorres_cond_both'[where Q="\<top>" and Q'=\<top>])
+            apply fastforce
+           apply (ctac (no_vcg) add: refill_new_ccorres)
+          apply clarsimp
+          apply (rule ccorres_rhs_assoc)+
+          apply (ctac (no_vcg) add: sc_active_ccorres, rename_tac active)
+           apply csymbr
+           apply clarsimp
+           apply (rule_tac P="to_bool active" in ccorres_cases)
+            apply ccorres_rewrite
+            apply (rule ccorres_cond_seq)
+            apply (rule ccorres_cond_true)
+            apply (rule_tac xf'=ret__int_'
+                        and val="from_bool (scTCB sc \<noteq> None)"
+                        and R="obj_at' (\<lambda>sc'. scTCB sc' = scTCB sc) scPtr and valid_objs'"
+                         in ccorres_symb_exec_r_known_rv[where R'="UNIV"])
+               apply (rule conseqPre, vcg)
+               apply normalise_obj_at'
+               apply (frule (1) sc_ko_at_valid_objs_valid_sc')
+               apply (frule (1) obj_at_cslift_sc)
+               apply (clarsimp simp: option_to_ctcb_ptr_def valid_sched_context'_def)
+               apply (case_tac "scTCB sc"; clarsimp)
+               apply (fastforce dest: tcb_at_not_NULL)
+              apply ceqv
+             apply (rule ccorres_cond_seq)
+             apply (rule ccorres_cond_both'[where Q="\<top>" and Q'=\<top>])
+               apply fastforce
+              apply clarsimp
+              apply (drule Some_to_the)
+              apply (clarsimp simp: option_to_ctcb_ptr_def split: option.splits)
+              apply (rule ccorres_rhs_assoc)+
+              apply (ctac (no_vcg) add: isRunnable_ccorres)
+               apply csymbr
+               apply (rule ccorres_cond_both'[where Q="\<top>" and Q'=\<top>])
+                 apply (clarsimp simp: to_bool_def)
+                apply (ctac (no_vcg) add: refill_update_ccorres)
+               apply (ctac (no_vcg) add: refill_new_ccorres)
+              apply wpsimp
+             (* target sc is not associated with a thread, so we perform refill_new *)
+             apply ccorres_rewrite
+             apply (rule ccorres_cond_false)
+             apply (ctac add: refill_new_ccorres)
+            apply vcg
+           (* target sc is not active, so we perform refill_new *)
+           apply clarsimp
+           apply ccorres_rewrite
+           apply (rule ccorres_cond_seq)
+           apply (rule ccorres_cond_false)
+           apply ccorres_rewrite
+           apply (rule ccorres_cond_seq)
+           apply (rule ccorres_cond_false)
+           apply ccorres_rewrite
+           apply (rule ccorres_cond_false)
+           apply (ctac (no_vcg) add: refill_new_ccorres)
+          apply wpsimp
+         apply ceqv
+        apply (rule_tac r'=dc and xf'=xfdc in ccorres_split_nothrow_novcg)
+            apply (clarsimp simp: when_def)
+            apply (rule_tac Q="obj_at' (\<lambda>sc'. scTCB sc' = scTCB sc) scPtr and valid_objs'"
+                         in ccorres_cond_both'[where Q'=\<top>])
+              apply normalise_obj_at'
+              apply (frule (1) sc_ko_at_valid_objs_valid_sc')
+              apply (frule (1) obj_at_cslift_sc)
+              apply (clarsimp simp: option_to_ctcb_ptr_def valid_sched_context'_def)
+              apply (case_tac "scTCB sc"; clarsimp)
+              apply (fastforce dest: tcb_at_not_NULL)
+             apply (rule ccorres_rhs_assoc)
+             apply (ctac add: schedContext_resume_ccorres)
+               apply (rule ccorres_rhs_assoc)+
+               apply (ctac add: isRunnable_ccorres, rename_tac runnable)
+                 apply (rule ccorres_pre_getCurThread, rename_tac ctPtr)
+                 apply (rule ccorres_cond_seq)
+                 apply ccorres_rewrite
+                 apply clarsimp
+                 apply (drule Some_to_the)
+                 apply (rule_tac P="the (scTCB sc) = ctPtr" in ccorres_cases)
+                  (* the target sc is associated with the current thread,
+                     so we perform rescheduleRequired *)
+                  apply clarsimp
+                  apply (rule ccorres_cond_false)
+                  apply ccorres_rewrite
+                  apply (rule ccorres_cond_true)
+                  apply (ctac add: rescheduleRequired_ccorres)
+                 apply (clarsimp simp: when_def to_bool_def)
+                 apply (rule_tac Q="\<lambda>s. ctPtr = ksCurThread s" in ccorres_cond_both'[where Q'=\<top>])
+                   apply (clarsimp dest!: rf_sr_ksCurThread simp: option_to_ctcb_ptr_def)
+                  (* the target sc is not associated with the current thread, but is associated
+                     with a runnable thread, so we perform possibleSwitchTo *)
+                  apply (rule ccorres_add_return2)
+                  apply (ctac add: possibleSwitchTo_ccorres)
+                    apply (rule ccorres_cond_false)
+                    apply (rule ccorres_return_Skip)
+                   apply wpsimp
+                  apply (vcg exspec=possibleSwitchTo_modifies)
+                 (* the target sc is associated with a thread that is not runnable - do nothing *)
+                 apply (rule ccorres_cond_false)
+                 apply (rule ccorres_return_Skip)
+                apply wpsimp
+               apply (vcg exspec=isRunnable_modifies)
+              apply (rule_tac Q'="\<lambda>_ s. tcb_at' (the (scTCB sc)) s
+                                        \<and> weak_sch_act_wf (ksSchedulerAction s) s
+                                        \<and> ksCurDomain s \<le> maxDomain \<and> valid_objs' s \<and> no_0_obj' s
+                                        \<and> pspace_aligned' s \<and> pspace_distinct' s"
+                           in hoare_post_imp)
+               apply clarsimp
+              apply wpsimp
+             apply (vcg exspec=schedContext_resume_modifies)
+            apply ccorres_rewrite
+            apply (rule ccorres_return_Skip)
+           apply ceqv
+          apply (rule_tac r'=dc and xf'=xfdc in ccorres_split_nothrow_novcg)
+              apply (rule updateSchedContext_ccorres_lemma2[where P=\<top>])
+                apply vcg
+               apply simp
+              apply (fastforce intro: rf_sr_sc_update_no_refill_buffer_update2
+                                      refill_buffer_relation_sc_no_refills_update
+                                simp: typ_heap_simps' csched_context_relation_def)
+             apply ceqv
+            apply (rule ccorres_add_return2)
+            apply (rule ccorres_split_nothrow)
+                apply (rule updateSchedContext_ccorres_lemma2[where P=\<top>])
+                  apply vcg
+                 apply simp
+                apply (fastforce intro: rf_sr_sc_update_no_refill_buffer_update2
+                                        refill_buffer_relation_sc_no_refills_update
+                                  simp: typ_heap_simps' csched_context_relation_def
+                                        seL4_SchedContext_Sporadic_def schedContextSporadicFlag_def
+                                        nth_is_and_neq_0
+                                 split: if_splits)
+               apply ceqv
+              apply (rule ccorres_from_vcg_throws[where P=\<top> and P'=UNIV])
+              apply (rule allI, rule conseqPre, vcg)
+              apply (clarsimp simp: return_def)
+             apply wpsimp
+            apply vcg
+           apply wpsimp
+          apply (clarsimp simp: guard_is_UNIV_def)
+         apply wpsimp
+        apply (clarsimp simp: guard_is_UNIV_def)
+       apply ((wpsimp wp: refillNew_invs' hoare_vcg_imp_lift' hoare_vcg_if_lift2
+               | strengthen invs'_implies)+)[1]
+           apply (drule Some_to_the)
+           apply ((wpsimp wp: refillUpdate_invs' | strengthen invs'_implies)+)[1]
+          apply clarsimp
+          apply (drule Some_to_the)
+          apply ((wpsimp wp: refillNew_invs' | strengthen invs'_implies)+)[1]
+         apply (rule_tac Q'="\<lambda>_ s. invs' s \<and> obj_at' (\<lambda>sc'. scTCB sc' = scTCB sc) scPtr s
+                                   \<and> (\<exists>n. sc_at'_n n scPtr s \<and> valid_refills_number' mRefills n)
+                                   \<and> ex_nonz_cap_to' scPtr s \<and> MIN_REFILLS \<le> mRefills
+                                   \<and> (\<exists>tcbPtr. scTCB sc = Some tcbPtr \<longrightarrow> tcb_at' tcbPtr s)
+                                   \<and> weak_sch_act_wf (ksSchedulerAction s) s"
+                      in hoare_post_imp)
+          apply (clarsimp split: if_splits)
+          apply normalise_obj_at'
+          apply (intro conjI;
+                 fastforce dest!: invs'_ko_at_valid_sched_context' simp: valid_sched_context'_def)
+         apply (wpsimp wp: isRunnable_wp)
+        apply (rule_tac Q'="\<lambda>_ s. invs' s \<and> obj_at' (\<lambda>sc'. scTCB sc' = scTCB sc) scPtr s
+                                  \<and> MIN_REFILLS \<le> mRefills
+                                  \<and> (\<exists>tcbPtr. scTCB sc = Some tcbPtr \<longrightarrow> tcb_at' tcbPtr s)
+                                  \<and> weak_sch_act_wf (ksSchedulerAction s) s"
+                     in hoare_post_imp)
+         apply normalise_obj_at'
+         apply (intro conjI impI allI;
+                fastforce dest!: invs'_ko_at_valid_sched_context' simp: valid_sched_context'_def
+                          split: if_splits)
+        apply ((wpsimp wp: refillNew_invs' hoare_vcg_ex_lift | strengthen invs'_implies)+)[1]
+       apply wpsimp
+      apply (clarsimp simp: guard_is_UNIV_def option_to_ctcb_ptr_def split: option.splits)
+     apply (rule_tac Q'="\<lambda>_ s. invs' s
+                               \<and> obj_at' (\<lambda>sc'. scTCB sc' = scTCB sc) scPtr s
+                               \<and> (\<exists>n. sc_at'_n n scPtr s \<and> valid_refills_number' mRefills n)
+                               \<and> MIN_REFILLS \<le> mRefills \<and> ex_nonz_cap_to' scPtr s
+                               \<and> (\<exists>tcbPtr. scTCB sc = Some tcbPtr \<longrightarrow> tcb_at' tcbPtr s)
+                               \<and> weak_sch_act_wf (ksSchedulerAction s) s"
+                  in hoare_post_imp)
+      apply clarsimp
+      subgoal
+        by (intro conjI impI allI;
+            normalise_obj_at'?,
+            fastforce dest!: invs'_ko_at_valid_sched_context'
+                      intro: obj_at'_weakenE
+                       simp: valid_refills_number'_def valid_sched_context'_def MIN_REFILLS_def
+                             objBits_simps active_sc_at'_def)
+     apply (wpsimp wp: commitTime_invs' hoare_vcg_ex_lift)
+      apply (drule Some_to_the)
+      apply (wpsimp wp: commitTime_invs' hoare_vcg_ex_lift)
+     apply (wpsimp wp: commitTime_invs' tcbReleaseRemove_invs' hoare_vcg_ex_lift)
+    apply (clarsimp simp: guard_is_UNIV_def to_bool_def from_bool_def MIN_REFILLS_def)
+   apply vcg
+  apply (clarsimp split: if_splits)
+  apply (intro conjI impI allI;
+         fastforce dest!: invs'_ko_at_valid_sched_context' intro: obj_at'_weakenE
+                    simp: valid_sched_context'_def)
+  done
 
 end
 
diff --git a/proof/invariant-abstract/AInvs.thy b/proof/invariant-abstract/AInvs.thy
index 93c658b746..6f1e3f1838 100644
--- a/proof/invariant-abstract/AInvs.thy
+++ b/proof/invariant-abstract/AInvs.thy
@@ -215,7 +215,7 @@ lemma invoke_sched_context_cur_sc_tcb_are_bound_imp_cur_sc_active:
   apply (cases iv; clarsimp)
   apply (rule hoare_weaken_pre)
    apply (rule_tac f=cur_sc in hoare_lift_Pf2)
-    apply wpsimp
+    apply ((wpsimp | wp (once) hoare_drop_imps)+)[1]
    apply (wpsimp wp: update_sched_context_wp hoare_vcg_all_lift hoare_drop_imps)
   apply (clarsimp simp: active_sc_def MIN_REFILLS_def vs_all_heap_simps)
   done
@@ -674,18 +674,20 @@ lemma invoke_sched_control_configure_flags_schact_is_rct_imp_ct_not_in_release_q
    apply (fastforce dest: ex_nonz_cap_to_not_idle_sc_ptr)
   apply (rule_tac Q'="?post" in bind_wp_fwd)
    apply (rule hoare_when_cases, simp)
-   apply (rule bind_wp[OF _ assert_opt_sp])
-   apply (rule bind_wp[OF _ gts_sp])
-   apply (rule_tac Q'="\<lambda>_ s. in_release_q (cur_thread s) s \<longrightarrow> tcb_ptr = cur_thread s"
+   apply (rule_tac Q'="\<lambda>_ s. sc_tcb_sc_at (\<lambda>to. to = sc_tcb sc) sc_ptr s
+                             \<and> (in_release_q (cur_thread s) s
+                                \<longrightarrow> heap_ref_eq (cur_thread s) sc_ptr (sc_tcbs_of s))"
                 in bind_wp_fwd)
     apply (wpsimp wp: hoare_vcg_imp_lift' sched_context_resume_ct_not_in_release_q)
-    apply (clarsimp simp: vs_all_heap_simps sc_at_pred_n_def obj_at_def)
+   apply (rule bind_wp[OF _ assert_opt_sp])
+   apply (rule bind_wp[OF _ gts_sp])
    apply (rule bind_wp[OF _ gets_sp])
    apply (rule hoare_if)
     apply (rule_tac Q'="\<lambda>_ s. scheduler_action s = choose_new_thread" in hoare_post_imp)
      apply (clarsimp simp: schact_is_rct_def)
     apply (wpsimp wp: reschedule_cnt)
    apply (wpsimp wp: hoare_drop_imps)
+   apply (clarsimp simp: vs_all_heap_simps obj_at_def sc_at_ppred_def)
   apply wpsimp
   done
 
diff --git a/proof/invariant-abstract/DetSchedSchedule_AI.thy b/proof/invariant-abstract/DetSchedSchedule_AI.thy
index 20f564a1b4..8a044a23cf 100644
--- a/proof/invariant-abstract/DetSchedSchedule_AI.thy
+++ b/proof/invariant-abstract/DetSchedSchedule_AI.thy
@@ -18983,6 +18983,12 @@ lemma sc_sporadic_update_is_active_sc_valid_sched:
   unfolding valid_sched_def
   by (wpsimp wp: sc_sporadic_update_active_scs_valid)
 
+lemma heap_refs_inv_pred_map_sc_tcbs_of_tcb_scps_of:
+  "heap_refs_inv (tcb_scps_of s) (sc_tcbs_of s)
+   \<Longrightarrow> pred_map (\<lambda>tcb. tcb = Some tcb_ptr) (sc_tcbs_of s) sc_ptr
+       \<longleftrightarrow> pred_map (\<lambda>sc. sc = Some sc_ptr) (tcb_scps_of s) tcb_ptr"
+  by (clarsimp simp: heap_refs_inv_def2 pred_map_eq_normalise)
+
 lemma invoke_sched_control_configure_flags_valid_sched:
   "\<lbrace>valid_sched
     and valid_sched_control_inv iv and schact_is_rct and invs
@@ -19009,23 +19015,20 @@ lemma invoke_sched_control_configure_flags_valid_sched:
    apply (clarsimp simp: active_sc_def current_time_bounded_def MIN_REFILLS_def schact_is_rct_simple
                    cong: conj_cong)
    apply (intro conjI impI allI)
-           apply (subgoal_tac "heap_ref_eq t sc_ptr (sc_tcbs_of s)")
-            apply (clarsimp simp: sc_at_kh_simps vs_all_heap_simps sc_at_pred_n_def obj_at_def)
-           apply (clarsimp simp: sc_at_pred_n_def obj_at_def split: if_splits)
-           apply (erule heap_refs_retractD[rotated])
-           apply (erule sym_refs_retract_tcb_scps)
-          apply (clarsimp simp add: sc_at_pred_n_def obj_at_def)
-         apply (clarsimp simp: current_time_bounded_def)
-        apply (clarsimp simp: sc_at_pred_n_def obj_at_def)
-       apply (clarsimp simp: sc_at_pred_n_def obj_at_def)
-       apply (subgoal_tac "heap_ref_eq t sc_ptr (sc_tcbs_of s)")
-        apply (clarsimp simp: sc_at_kh_simps vs_all_heap_simps)
-       apply (erule heap_refs_retractD[rotated])
-       apply (erule sym_refs_retract_tcb_scps)
+        apply (subgoal_tac "heap_ref_eq t sc_ptr (sc_tcbs_of s)")
+         apply (clarsimp simp: sc_at_kh_simps vs_all_heap_simps sc_at_pred_n_def obj_at_def)
+        apply (clarsimp simp: sc_at_pred_n_def obj_at_def split: if_splits)
+        apply (erule heap_refs_retractD[rotated])
+        apply (erule sym_refs_retract_tcb_scps)
+       apply (clarsimp simp add: sc_at_pred_n_def obj_at_def)
       apply (clarsimp simp: sc_at_pred_n_def obj_at_def)
-     apply clarsimp
+     apply (clarsimp simp: sc_at_pred_n_def obj_at_def)
+     apply (subgoal_tac "heap_ref_eq t sc_ptr (sc_tcbs_of s)")
+      apply (clarsimp simp: sc_at_kh_simps vs_all_heap_simps)
+     apply (erule heap_refs_retractD[rotated])
+     apply (erule sym_refs_retract_tcb_scps)
     apply (clarsimp simp: sc_at_pred_n_def obj_at_def)
-   apply (clarsimp simp: sc_at_pred_n_def obj_at_def)
+   apply clarsimp
 
   \<comment> \<open>\<exists>y. sc_tcb sc = Some y\<close>
   apply (clarsimp simp: bind_assoc)
@@ -19112,41 +19115,30 @@ lemma invoke_sched_control_configure_flags_valid_sched:
                             \<and> active_sc_tcb_at tcb_ptr s
                             \<and> sc_ptr \<noteq> idle_sc_ptr
                             \<and> is_active_sc sc_ptr s"
-           in bind_wp)
-   apply (simp add: return_bind)
-   apply (rule bind_wp[OF _ gts_sp])
-   apply (rename_tac thread_state2)
-   apply (simp only: valid_sched_def cong: conj_cong)
+               in bind_wp)
    apply (rule_tac Q'="\<lambda>rv s. valid_sched_except_blocked s
                              \<and> budget \<le> period \<and> period \<le> MAX_PERIOD \<and> current_time_bounded s
                              \<and> valid_blocked_except tcb_ptr s \<and> schact_is_rct s
                              \<and> invs s \<and> consumed_time_bounded s
-                             \<and> (runnable thread_state2
-                                \<longrightarrow> not_in_release_q tcb_ptr s \<longrightarrow> released_sc_tcb_at tcb_ptr s)
-                             \<and> pred_map_eq (thread_state2) (tcb_sts_of s) tcb_ptr
+                             \<and> (pred_map runnable (tcb_sts_of s) tcb_ptr
+                                \<longrightarrow> active_sc_tcb_at tcb_ptr s
+                                     \<longrightarrow> not_in_release_q tcb_ptr s \<longrightarrow> released_sc_tcb_at tcb_ptr s)
                              \<and> sc_tcb_sc_at (\<lambda>tcb. tcb = sc_tcb sc) sc_ptr s
                              \<and> sc_ptr \<noteq> idle_sc_ptr \<and> is_active_sc sc_ptr s"
-           in bind_wp_fwd)
+                in bind_wp_fwd)
     apply (simp only: valid_sched_def cong: conj_cong)
     apply (wpsimp wp: sched_context_resume_valid_ready_qs sched_context_resume_valid_release_q
                       sched_context_resume_valid_sched_action
                       sched_context_resume_valid_blocked_except_set
-                      hoare_vcg_const_imp_lift)
-      apply (rule_tac Q'="\<lambda>_ s. active_sc_tcb_at tcb_ptr s
-                               \<and> (runnable thread_state2 \<longrightarrow> active_sc_tcb_at tcb_ptr s
-                                   \<longrightarrow> not_in_release_q tcb_ptr s \<longrightarrow> released_sc_tcb_at tcb_ptr s)"
-                   in hoare_strengthen_post[rotated])
-       apply clarsimp
-      apply (wpsimp wp: sched_context_resume_cond_released_sc_tcb_at)
-     apply (wpsimp wp: sched_context_resume_sc_tcb_sc_at)
-    apply (clarsimp; intro conjI impI)
-        apply (clarsimp simp: op_equal schact_is_rct_def)
-       apply (clarsimp simp: pred_map_eq_def pred_map_def obj_at_kh_kheap_simps)
-      apply (fastforce simp: sc_at_pred_n_def obj_at_def pred_tcb_at_def)
-     apply (clarsimp simp: vs_all_heap_simps tcb_at_kh_simps)
-    apply (clarsimp simp: vs_all_heap_simps tcb_at_kh_simps)
-   apply (rule bind_wp[OF _ gets_sp])
+                      hoare_vcg_const_imp_lift
+                      sched_context_resume_cond_released_sc_tcb_at
+           | wp (once) hoare_vcg_imp_lift')+
+    apply (clarsimp simp: scheduler_act_not_def schact_is_rct_def pred_map_simps
+                          obj_at_kh_kheap_simps)
    apply (simp add: return_bind)
+   apply (rule bind_wp[OF _ gts_sp])
+   apply (rename_tac thread_state2)
+   apply (rule bind_wp[OF _ gets_sp])
    apply (clarsimp split: if_split)
    apply (intro conjI impI)
     apply (rule_tac Q'="\<lambda>_. valid_sched" in hoare_post_imp)
@@ -19158,10 +19150,16 @@ lemma invoke_sched_control_configure_flags_valid_sched:
    apply (wpsimp wp: possible_switch_to_valid_sched_weak sc_sporadic_update_is_active_sc_valid_sched)
    apply (clarsimp split: if_split)
    apply (intro conjI impI)
-     apply (clarsimp simp: pred_map_simps)
-    apply (frule invs_valid_idle)
-    apply (clarsimp simp: valid_idle_def pred_tcb_at_def obj_at_def vs_all_heap_simps)
-   apply (clarsimp simp: vs_all_heap_simps runnable_eq_active valid_sched_valid_sched_except_blocked
+      apply (clarsimp simp: pred_map_simps vs_all_heap_simps obj_at_kh_kheap_simps)
+     apply (clarsimp simp: obj_at_kh_kheap_simps)
+     apply (elim impE)
+       apply (clarsimp simp: pred_map_simps vs_all_heap_simps obj_at_kh_kheap_simps)
+      apply (fastforce simp: active_sc_tcb_at_def2 tcb_at_kh_simps
+                             heap_refs_inv_pred_map_sc_tcbs_of_tcb_scps_of)
+     apply fastforce
+    apply (clarsimp dest!: invs_valid_idle simp: valid_idle_def pred_tcb_at_def obj_at_def)
+   apply (clarsimp simp: runnable_eq_active valid_sched_valid_sched_except_blocked
+                         obj_at_kh_kheap_simps vs_all_heap_simps
                   elim!: valid_blockedE')
 
   apply (rule hoare_if)
@@ -19176,6 +19174,7 @@ lemma invoke_sched_control_configure_flags_valid_sched:
                          runnable_eq MIN_REFILLS_def active_sc_def)
    apply (clarsimp simp: vs_all_heap_simps current_time_bounded_def)
 
+  apply (rule bind_wp[OF _ get_sc_active_sp])
   apply (rule hoare_if)
    apply (simp add: return_bind)
    apply (rule bind_wp[OF _ gts_sp])
@@ -19183,7 +19182,7 @@ lemma invoke_sched_control_configure_flags_valid_sched:
    apply (clarsimp simp: valid_sched_def)
    apply (rule hoare_if)
 
-     \<comment> \<open>refill_update branch\<close>
+    \<comment> \<open>refill_update branch\<close>
     apply (wpsimp wp: refill_update_valid_ready_qs refill_update_valid_release_q
                       refill_update_valid_sched_action refill_update_released_ipc_queues
                       refill_update_invs refill_update_valid_blocked_except_set
@@ -19855,12 +19854,13 @@ lemma invoke_sched_control_configure_flags_scheduler_act_sane[wp]:
   supply if_split [split del]
   unfolding invoke_sched_control_configure_flags_def
   apply wpsimp
-               apply (wpsimp wp: possible_switch_to_scheduler_act_sane')
-              apply (wpsimp wp:  hoare_vcg_if_lift2 hoare_vcg_imp_lift')
-             apply (wpsimp wp:  hoare_vcg_if_lift2 hoare_vcg_imp_lift')
-            apply (rule_tac Q'="\<lambda>_ s. scheduler_act_sane s" in hoare_strengthen_post[rotated])
-             apply (clarsimp split: if_split)
-  by (wpsimp wp: hoare_vcg_if_lift2 hoare_drop_imp gts_wp hoare_vcg_all_lift)+
+          apply (wpsimp wp: possible_switch_to_scheduler_act_sane')
+         apply wpsimp
+        apply (wpsimp wp:  hoare_vcg_if_lift2 hoare_vcg_imp_lift' gts_wp)
+       apply (wpsimp wp:  hoare_vcg_if_lift2 hoare_vcg_imp_lift')
+      apply (rule_tac Q'="\<lambda>_ s. scheduler_act_sane s" in hoare_strengthen_post[rotated])
+       apply (clarsimp split: if_split)
+      by (wpsimp wp: hoare_vcg_if_lift2 hoare_drop_imp gts_wp hoare_vcg_all_lift)+
 
 crunch invoke_irq_handler
   for scheduler_act_sane[wp]: "scheduler_act_sane::'state_ext state \<Rightarrow> _"
@@ -24087,15 +24087,13 @@ lemma invoke_sched_control_configure_flags_cur_sc_in_release_q_imp_zero_consumed
                            \<and> cur_sc_tcb_are_bound s"
          in bind_wp)
    apply wpsimp
-       apply (wpsimp wp: sched_context_resume_cur_sc_in_release_q_imp_zero_consumed split: if_splits)
-      apply (wpsimp wp: gts_wp)
-     apply wpsimp
+     apply (wpsimp wp: sched_context_resume_cur_sc_in_release_q_imp_zero_consumed split: if_splits)
     apply (rule_tac Q'="\<lambda>_ s. cur_sc_in_release_q_imp_zero_consumed s
-                             \<and> cur_sc_more_than_ready s
-                             \<and> heap_refs_retract (sc_tcbs_of s) (tcb_scps_of s)
-                             \<and> current_time_bounded s \<and> ex_nonz_cap_to sc_ptr s
-                             \<and> ct_active s \<and> invs s \<and> cur_sc_tcb_are_bound s"
-           in hoare_strengthen_post[rotated])
+                              \<and> cur_sc_more_than_ready s
+                              \<and> heap_refs_retract (sc_tcbs_of s) (tcb_scps_of s)
+                              \<and> current_time_bounded s \<and> ex_nonz_cap_to sc_ptr s
+                              \<and> ct_active s \<and> invs s \<and> cur_sc_tcb_are_bound s"
+                 in hoare_strengthen_post[rotated])
      apply (clarsimp simp: cur_sc_more_than_ready_def split: if_splits)
      apply (intro conjI impI allI)
         apply (rule cur_sc_not_idle_sc_ptr; fastforce)
@@ -25025,6 +25023,10 @@ crunch install_tcb_cap, install_tcb_frame_cap, do_reply_transfer, invoke_irq_han
   for cur_sc[wp]: "\<lambda>s :: det_state. P (cur_sc s)"
   (wp: crunch_wps check_cap_inv  preemption_point_inv hoare_vcg_all_lift simp: crunch_simps)
 
+crunch invoke_sched_control_configure_flags
+  for cur_sc[wp]: "\<lambda>s :: det_state. P (cur_sc s)"
+  (wp: crunch_wps hoare_vcg_all_lift)
+
 crunch perform_invocation
   for cur_sc[wp]: "\<lambda>s :: det_state. P (cur_sc s)"
   (wp: crunch_wps preemption_point_inv check_cap_inv filterM_preserved cap_revoke_preservation
@@ -26301,24 +26303,25 @@ lemma invoke_sched_control_configure_flags_ct_ready_if_schedulable[wp]:
   apply (case_tac iv; clarsimp)
   apply (rename_tac sc_ptr budget period mrefills badge flags)
   apply (wpsimp wp: sched_context_resume_ct_ready_if_schedulable)
+        apply (wpsimp wp: gts_wp)
        apply (wpsimp wp: gts_wp)
       apply (wpsimp wp: gts_wp)
-     apply (wpsimp wp: gts_wp)
-     apply (rule_tac Q'="\<lambda>_ s. ct_ready_if_schedulable s
+     apply wpsimp
+    apply (rule_tac Q'="\<lambda>_ s. ct_ready_if_schedulable s
                               \<and> current_time_bounded s
                               \<and> MIN_BUDGET \<le> budget
                               \<and> (sc_active sc \<longrightarrow> is_active_sc sc_ptr s)
                               \<and> (sc_tcb_sc_at ((=) (sc_tcb sc)) sc_ptr s)
                               \<and> invs s \<and> cur_sc s \<noteq> idle_sc_ptr"
             in hoare_post_imp)
-      apply (clarsimp simp: current_time_bounded_def)
-      apply (subgoal_tac "y = cur_thread s")
-       apply (erule ct_ready_if_schedulableE)
-       apply (clarsimp simp: tcb_at_kh_simps vs_all_heap_simps ct_in_state_def sc_at_kh_simps sc_at_pred_n_def obj_at_def
-                             active_sc_def runnable_eq_active pred_map_eq_normalise)
-      apply (clarsimp simp: pred_map_eq_normalise)
-      apply (frule (1) heap_refs_retractD[OF heap_refs_inv_retract_symD[OF sym_refs_inv_sc_tcbs[OF invs_sym_refs]], rotated])
-      apply (clarsimp simp: vs_all_heap_simps sc_at_kh_simps)
+     apply (clarsimp simp: current_time_bounded_def)
+     apply (subgoal_tac "y = cur_thread s")
+      apply (erule ct_ready_if_schedulableE)
+      apply (clarsimp simp: tcb_at_kh_simps vs_all_heap_simps ct_in_state_def sc_at_kh_simps sc_at_pred_n_def obj_at_def
+                            active_sc_def runnable_eq_active pred_map_eq_normalise)
+     apply (clarsimp simp: pred_map_eq_normalise)
+     apply (frule (1) heap_refs_retractD[OF heap_refs_inv_retract_symD[OF sym_refs_inv_sc_tcbs[OF invs_sym_refs]], rotated])
+     apply (clarsimp simp: vs_all_heap_simps sc_at_kh_simps)
     apply (wpsimp wp: commit_time_invs hoare_vcg_if_lift2 hoare_vcg_imp_lift'
                       tcb_sched_action_pred_tcb_at_ct tcb_sched_action_sc_tcb_sc_at)+
   apply (prop_tac "ct_ready_if_schedulable s")
@@ -26401,7 +26404,7 @@ lemma perform_unsafe_invocation_ct_ready_if_schedulable:
 (*FIXME RT: move*)
 crunch perform_invocation
   for cur_thread[wp]: "\<lambda>s :: det_state. P (cur_thread s)"
-  (wp: check_cap_inv crunch_wps cap_revoke_preservation filterM_preserved)
+  (wp: check_cap_inv crunch_wps cap_revoke_preservation filterM_preserved simp: crunch_simps)
 
 lemma perform_invocation_ct_ready_if_schedulable[wp]:
   "\<lbrace>ct_released and invs and valid_sched and valid_machine_time and ct_active and valid_invocation i
diff --git a/proof/invariant-abstract/Deterministic_AI.thy b/proof/invariant-abstract/Deterministic_AI.thy
index 02d0f9339e..594654617a 100644
--- a/proof/invariant-abstract/Deterministic_AI.thy
+++ b/proof/invariant-abstract/Deterministic_AI.thy
@@ -4215,8 +4215,8 @@ end
 context Deterministic_AI_1 begin
 
 crunch invoke_tcb, invoke_sched_control_configure_flags
- for valid_list[wp]: "valid_list"
- (wp: hoare_drop_imp check_cap_inv mapM_x_wp')
+ for valid_list[wp]: valid_list
+ (wp: crunch_wps check_cap_inv mapM_x_wp' simp: crunch_simps)
 
 end
 
diff --git a/proof/invariant-abstract/SchedContextInv_AI.thy b/proof/invariant-abstract/SchedContextInv_AI.thy
index a1313f273b..811a1d458b 100644
--- a/proof/invariant-abstract/SchedContextInv_AI.thy
+++ b/proof/invariant-abstract/SchedContextInv_AI.thy
@@ -1238,7 +1238,7 @@ end
 
 crunch invoke_sched_control_configure_flags
   for typ_at[wp]: "\<lambda>s. P (typ_at T p s)"
-  (simp: crunch_simps)
+  (simp: crunch_simps wp: crunch_wps)
 
 lemma invoke_sched_context_tcb[wp]:
   "\<lbrace>tcb_at tptr\<rbrace> invoke_sched_context i \<lbrace>\<lambda>rv. tcb_at tptr\<rbrace>"
diff --git a/proof/refine/RISCV64/Invariants_H.thy b/proof/refine/RISCV64/Invariants_H.thy
index cda348bc03..53eac38081 100644
--- a/proof/refine/RISCV64/Invariants_H.thy
+++ b/proof/refine/RISCV64/Invariants_H.thy
@@ -3484,6 +3484,10 @@ lemma vms_sch_act_update'[iff]:
    valid_machine_state' s"
   by (simp add: valid_machine_state'_def )
 
+lemma objBits_sched_context_update[simp]:
+  "(\<And>sc. scSize (f sc) = scSize sc) \<Longrightarrow> objBits (f sc) = objBits sc"
+  by (simp add: objBits_simps)
+
 context begin interpretation Arch . (*FIXME: arch-split*)
 
 lemmas bit_simps' = pteBits_def asidHighBits_def asidPoolBits_def asid_low_bits_def
diff --git a/proof/refine/RISCV64/Ipc_R.thy b/proof/refine/RISCV64/Ipc_R.thy
index 857caf31f0..9751d8cacb 100644
--- a/proof/refine/RISCV64/Ipc_R.thy
+++ b/proof/refine/RISCV64/Ipc_R.thy
@@ -4085,16 +4085,6 @@ crunch postpone, schedContextResume, maybeDonateSc
   and valid_objs'[wp]: valid_objs'
   (simp: crunch_simps wp: crunch_wps)
 
-lemma updateSchedContext_sc_obj_at':
-  "\<lbrace>if scPtr = scPtr' then (\<lambda>s. \<forall>ko. ko_at' ko scPtr' s \<longrightarrow> P (f ko)) else obj_at' P scPtr'\<rbrace>
-   updateSchedContext scPtr f
-   \<lbrace>\<lambda>rv. obj_at' P scPtr'\<rbrace>"
-  supply if_split [split del]
-  apply (simp add: updateSchedContext_def)
-  apply (wpsimp wp: set_sc'.obj_at')
-  apply (clarsimp split: if_splits simp: obj_at'_real_def ko_wp_at'_def)
-  done
-
 lemma refillPopHead_bound_tcb_sc_at[wp]:
   "refillPopHead scPtr \<lbrace>obj_at' (\<lambda>a. \<exists>y. scTCB a = Some y) t\<rbrace>"
   supply if_split [split del]
diff --git a/proof/refine/RISCV64/KHeap_R.thy b/proof/refine/RISCV64/KHeap_R.thy
index a70ae33e8f..40e717dd48 100644
--- a/proof/refine/RISCV64/KHeap_R.thy
+++ b/proof/refine/RISCV64/KHeap_R.thy
@@ -4398,6 +4398,22 @@ lemma no_fail_updateSchedContext[wp]:
            (updateSchedContext ptr f)"
   by (wpsimp simp: updateSchedContext_def obj_at'_def projectKOs opt_map_def opt_pred_def)
 
+lemma updateSchedContext_sc_obj_at':
+  "\<lbrace>if scPtr = scPtr' then (\<lambda>s. \<forall>ko. ko_at' ko scPtr' s \<longrightarrow> P (f ko)) else obj_at' P scPtr'\<rbrace>
+   updateSchedContext scPtr f
+   \<lbrace>\<lambda>rv. obj_at' P scPtr'\<rbrace>"
+  supply if_split [split del]
+  apply (simp add: updateSchedContext_def)
+  apply (wpsimp wp: set_sc'.obj_at')
+  apply (clarsimp split: if_splits simp: obj_at'_real_def ko_wp_at'_def)
+  done
+
+lemma updateSchedContext_sc_obj_at'_inv:
+  "(\<And>sc. P (f sc) = P sc) \<Longrightarrow> updateSchedContext scPtr f \<lbrace>\<lambda>s. Q (obj_at' P scPtr' s)\<rbrace>"
+  unfolding updateSchedContext_def
+  apply (wpsimp wp: set_sc'.obj_at')
+  by (clarsimp split: if_splits simp: obj_at'_real_def ko_wp_at'_def)
+
 lemma update_sched_context_rewrite:
   "monadic_rewrite False True (sc_obj_at n scp)
     (update_sched_context scp f)
diff --git a/proof/refine/RISCV64/SchedContextInv_R.thy b/proof/refine/RISCV64/SchedContextInv_R.thy
index 80092fdd10..e7107af142 100644
--- a/proof/refine/RISCV64/SchedContextInv_R.thy
+++ b/proof/refine/RISCV64/SchedContextInv_R.thy
@@ -1420,6 +1420,10 @@ lemma invokeSchedControlConfigureFlags_corres:
        apply fastforce
       apply fastforce
 
+     apply (rule corres_split_forwards'[OF _ get_sc_active_sp scActive_sp])
+      apply (corres corres: scActive_corres)
+       apply fastforce
+      apply fastforce
      apply (rule corres_if_split)
        apply (clarsimp simp: sc_relation_def)
 
@@ -1464,7 +1468,7 @@ lemma invokeSchedControlConfigureFlags_corres:
         apply (clarsimp simp: MIN_REFILLS_def)
        apply (clarsimp simp: valid_refills_number'_def MIN_REFILLS_def)
       apply fastforce
-     apply simp
+     apply fastforce
 
     apply (find_goal \<open>match conclusion in "\<lbrace>P\<rbrace> f \<lbrace>Q\<rbrace>" for P f Q  \<Rightarrow> -\<close>)
     apply (rule hoare_if)
@@ -1475,6 +1479,7 @@ lemma invokeSchedControlConfigureFlags_corres:
       apply (clarsimp simp: current_time_bounded_def active_sc_def MIN_REFILLS_def)
      apply (wpsimp wp: hoare_vcg_imp_lift' hoare_vcg_all_lift)
 
+    apply (rule bind_wp[OF _ get_sc_active_sp])
     apply (rule hoare_if)
      apply (rule bind_wp_fwd_skip, wpsimp)
      apply (rule bind_wp[OF _ gts_sp])
@@ -1509,26 +1514,16 @@ lemma invokeSchedControlConfigureFlags_corres:
     apply wps_conj_solves
      apply (wpsimp wp: refillNew_invs')
     apply (clarsimp simp: ko_wp_at'_def valid_refills_number'_def)
-   apply (rule hoare_if)
-    apply wps_conj_solves
-    apply (rule bind_wp[OF _ isRunnable_sp])
-    apply (rule hoare_if)
-     apply (wpsimp wp: refillUpdate_invs')
-     apply (clarsimp simp: ko_wp_at'_def valid_refills_number'_def)
-    apply (wpsimp wp: refillNew_invs')
-    apply (clarsimp simp: ko_wp_at'_def valid_refills_number'_def)
-   apply wps_conj_solves
-   apply (wpsimp wp: refillNew_invs')
-   apply (clarsimp simp: ko_wp_at'_def valid_refills_number'_def)
+   apply (wpsimp wp: refillNew_invs' refillUpdate_invs' | wps)+
 
   apply (rule stronger_corres_guard_imp)
     apply (rule corres_split[where r'=dc])
        apply (rule corres_when)
         apply (clarsimp simp: sc_relation_def)
-       apply (rule corres_assert_opt_l)
-       apply (rule corres_split[OF isRunnable_corres'])
-          apply (clarsimp simp: sc_relation_def Some_to_the split: if_splits)
-         apply (rule corres_split[OF schedContextResume_corres])
+       apply (rule corres_split[OF schedContextResume_corres])
+         apply (rule corres_assert_opt_l)
+         apply (rule corres_split[OF isRunnable_corres'])
+            apply (clarsimp simp: sc_relation_def Some_to_the split: if_splits)
            apply (rule corres_split[OF getCurThread_corres])
              apply (rule corres_if)
                apply (fastforce dest!: Some_to_the simp: sc_relation_def)
@@ -1538,22 +1533,24 @@ lemma invokeSchedControlConfigureFlags_corres:
              apply (fastforce simp: sc_relation_def Some_to_the)
             apply wpsimp
            apply wpsimp
-          apply ((wpsimp wp: hoare_vcg_imp_lift' sched_context_resume_valid_sched_action
-                 | strengthen valid_objs_valid_tcbs)+)[1]
-         apply (rule_tac Q'="\<lambda>_. invs'" in hoare_post_imp, fastforce)
-         apply (rule schedContextResume_invs')
-        apply (wpsimp wp: gts_wp)
-       apply wpsimp
+          apply (wpsimp wp: gts_wp)
+         apply (wpsimp wp: gts_wp)
+        apply ((wpsimp wp: hoare_vcg_imp_lift' sched_context_resume_valid_sched_action
+                           hoare_vcg_ex_lift hoare_vcg_all_lift
+                | strengthen valid_objs_valid_tcbs)+)[1]
+       apply (rule_tac Q'="\<lambda>_. invs'" in hoare_post_imp, fastforce)
+       apply (rule schedContextResume_invs')
+      apply (wpsimp wp: gts_wp)
       apply (rule corres_split[OF updateSchedContext_no_stack_update_corres])
             apply (clarsimp simp: sc_relation_def)
            apply fastforce
           apply (clarsimp simp: objBits_simps)
          apply (clarsimp simp: objBits_simps)
         apply (rule updateSchedContext_no_stack_update_corres)
-            apply clarsimp
-           apply (clarsimp simp: sc_relation_def)
-          apply fastforce
-         apply (clarsimp simp: objBits_simps)
+           apply clarsimp
+          apply (clarsimp simp: sc_relation_def)
+         apply fastforce
+        apply (clarsimp simp: objBits_simps)
         apply wpsimp+
    apply (fastforce simp: sc_at_pred_n_def obj_at_def schact_is_rct_def pred_tcb_at_def
                    intro: valid_sched_action_weak_valid_sched_action)
diff --git a/proof/refine/RISCV64/Schedule_R.thy b/proof/refine/RISCV64/Schedule_R.thy
index c64742d65a..3c5d251868 100644
--- a/proof/refine/RISCV64/Schedule_R.thy
+++ b/proof/refine/RISCV64/Schedule_R.thy
@@ -1891,22 +1891,59 @@ lemma setRefillHd_active_sc_at'[wp]:
   apply (wpsimp wp: updateSchedContext_active_sc_at')
   done
 
-lemma setReprogramTimer_obj_at'[wp]:
-  "setReprogramTimer b \<lbrace>\<lambda>s. Q (obj_at' P t s)\<rbrace>"
-  unfolding active_sc_at'_def
-  by (wpsimp simp: setReprogramTimer_def)
-
-lemma setReprogramTimer_active_sc_at'[wp]:
-  "setReprogramTimer b \<lbrace>active_sc_at' scPtr\<rbrace>"
-  unfolding active_sc_at'_def
-  by wpsimp
+crunch refillNew, refillUpdate, tcbReleaseRemove, tcbSchedDequeue, commitTime
+  for obj_at'_scTCB[wp]: "\<lambda>s. obj_at' (\<lambda>sc. P (scTCB sc)) scPtr s"
+  and obj_at'_sc_objBits[wp]: "\<lambda>s. Q (obj_at' (\<lambda>sc :: sched_context. P (objBits sc)) scPtr s)"
+  (simp: crunch_simps
+   wp: updateSchedContext_sc_obj_at'_inv crunch_wps hoare_vcg_all_lift ignore: updateSchedContext)
 
-crunch refillBudgetCheck, refillUnblockCheck
-  for typ_at'[wp]: "\<lambda>s. P (typ_at' T p s)"
-  and sc_at'_n[wp]: "\<lambda>s. P (sc_at'_n T p s)"
-  and active_sc_at'[wp]: "active_sc_at' scPtr"
+crunch refillNew, refillUpdate, tcbReleaseRemove, tcbSchedDequeue, commitTime
+  for ksSchedulerAction[wp]: "\<lambda>s. P (ksSchedulerAction s)"
+  (simp: crunch_simps wp: crunch_wps hoare_vcg_all_lift)
+
+crunch refillNew, refillUpdate, tcbReleaseRemove, tcbSchedDequeue, commitTime
+  for weak_sch_act_wf[wp]: "\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s"
+  and ksCurDomain[wp]: "\<lambda>s. P (ksCurDomain s)"
+  (wp: weak_sch_act_wf_lift crunch_wps simp: crunch_simps maybeAddEmptyTail_def)
+
+crunch refillBudgetCheckRoundRobin, refillBudgetCheck
+  for active_sc_at'[wp]: "active_sc_at' scPtr"
   (wp: crunch_wps hoare_vcg_all_lift simp: crunch_simps)
 
+lemma scConsumed_update_active_sc_at'[wp]:
+  "updateSchedContext scPtr (scConsumed_update f) \<lbrace>active_sc_at' scPtr'\<rbrace>"
+  apply (wp updateSchedContext_wp)
+  by (fastforce simp: active_sc_at'_def obj_at'_def objBits_simps' opt_map_def split: if_splits)
+
+lemma active_sc_at'_ksReadyQueues_update[simp]:
+  "active_sc_at' scPtr (ksReadyQueues_update f s) = active_sc_at' scPtr s"
+  by (clarsimp simp: active_sc_at'_def)
+
+lemma active_sc_at'_ksReadyQueuesL1Bitmap_update[simp]:
+  "active_sc_at' scPtr (ksReadyQueuesL1Bitmap_update f s) = active_sc_at' scPtr s"
+  by (clarsimp simp: active_sc_at'_def)
+
+lemma active_sc_at'_ksReadyQueuesL2Bitmap_update[simp]:
+  "active_sc_at' scPtr (ksReadyQueuesL2Bitmap_update f s) = active_sc_at' scPtr s"
+  by (clarsimp simp: active_sc_at'_def)
+
+lemma active_sc_at'_ksReleaseQueue_update[simp]:
+  "active_sc_at' scPtr (ksReleaseQueue_update f s) = active_sc_at' scPtr s"
+  by (clarsimp simp: active_sc_at'_def)
+
+lemma active_sc_at'_ksReprogramTimer[simp]:
+  "active_sc_at' scPtr (ksReprogramTimer_update f s) = active_sc_at' scPtr s"
+  by (clarsimp simp: active_sc_at'_def)
+
+lemma threadSet_active_sc_at'[wp]:
+  "threadSet F tcbPtr \<lbrace>active_sc_at' scPtr\<rbrace>"
+  apply (wpsimp wp: threadSet_wp)
+  by (fastforce simp: active_sc_at'_def obj_at'_def)
+
+crunch tcbSchedDequeue, tcbReleaseRemove, mergeOverlappingRefills, commitTime
+  for active_sc_at'[wp]: "active_sc_at' scPtr"
+  (wp: crunch_wps ignore: threadSet simp: crunch_simps)
+
 lemma updateRefillHd_valid_objs'[wp]:
   "updateRefillHd scPtr f \<lbrace>valid_objs'\<rbrace>"
   unfolding updateRefillHd_def updateSchedContext_def
diff --git a/proof/refine/RISCV64/Tcb_R.thy b/proof/refine/RISCV64/Tcb_R.thy
index a5391fe050..ff8d7d5504 100644
--- a/proof/refine/RISCV64/Tcb_R.thy
+++ b/proof/refine/RISCV64/Tcb_R.thy
@@ -1870,97 +1870,96 @@ lemma schedContextBindTCB_corres:
   apply (simp only: sched_context_bind_tcb_def schedContextBindTCB_def)
   apply (rule stronger_corres_guard_imp)
     apply clarsimp
-       apply (rule corres_split_nor)
-         apply (clarsimp simp: set_tcb_obj_ref_thread_set sc_relation_def)
-          apply (rule threadset_corres; clarsimp simp: tcb_relation_def inQ_def)
-         apply (rule corres_split_nor)
-            apply (rule_tac f'="scTCB_update (\<lambda>_. Some t)"
-                         in updateSchedContext_no_stack_update_corres; clarsimp?)
-             apply (clarsimp simp: sc_relation_def refillSize_def)
-            apply (clarsimp simp: objBits_def objBitsKO_def)
-           apply (rule corres_split[OF ifCondRefillUnblockCheck_corres])
-             apply (rule corres_split_nor)
-                apply (rule schedContextResume_corres)
-               apply (rule corres_split_eqr)
-                  apply (rule getSchedulable_corres)
-                 apply (rule corres_when, simp)
-                 apply (rule corres_split_nor)
-                    apply (rule tcbSchedEnqueue_corres, simp)
-                   apply (rule rescheduleRequired_corres)
-                  apply wp
-                 apply (wpsimp wp: tcbSchedEnqueue_valid_tcbs')
-                apply wpsimp
-               apply (wpsimp wp: threadGet_wp getTCB_wp getSchedulable_wp simp: inReleaseQueue_def)
-              apply (rule_tac Q'="\<lambda>rv. valid_objs and pspace_aligned and pspace_distinct and (\<lambda>s. sym_refs (state_refs_of s)) and
-                                      weak_valid_sched_action and active_scs_valid and
-                                      sc_tcb_sc_at ((=) (Some t)) ptr and current_time_bounded and
-                                      bound_sc_tcb_at (\<lambda>sc. sc = Some ptr) t and
-                                      in_correct_ready_q and ready_or_release and ready_qs_distinct"
-                           in hoare_strengthen_post[rotated])
-               apply (fastforce simp: schedulable_def2)
-              apply (wp sched_context_resume_weak_valid_sched_action sched_context_resume_pred_tcb_at)
-             apply (rule_tac Q'="\<lambda>_. invs'" in hoare_strengthen_post[rotated], fastforce)
-             apply wp
-            apply (rule_tac Q'="\<lambda>_. valid_objs and pspace_aligned and pspace_distinct and
-                                   (\<lambda>s. sym_refs (state_refs_of s)) and current_time_bounded and
-                                   valid_ready_qs and valid_release_q and weak_valid_sched_action and
-                                   active_scs_valid and scheduler_act_not t and
-                                   sc_tcb_sc_at ((=) (Some t)) ptr and
-                                   bound_sc_tcb_at (\<lambda>a. a = Some ptr) t and
-                                   in_correct_ready_q and ready_or_release and ready_qs_distinct"
-                   in hoare_strengthen_post[rotated])
-             apply (clarsimp simp: sc_tcb_sc_at_def obj_at_def valid_sched_action_def dest!: sym[of "Some _"])
-            apply (wpsimp simp: if_cond_refill_unblock_check_def
-                            wp: refill_unblock_check_valid_release_q
-                                refill_unblock_check_valid_sched_action
-                                refill_unblock_check_active_scs_valid)
-           apply (rule_tac Q'="\<lambda>_. invs'" in hoare_strengthen_post[rotated], fastforce)
-           apply wpsimp
-          apply (rule_tac Q'="\<lambda>_. valid_objs and pspace_aligned and pspace_distinct and
-                                 (\<lambda>s. sym_refs (state_refs_of s)) and
-                                 valid_ready_qs and valid_release_q and active_scs_valid and
-                                 ready_or_release and
-                                 sc_tcb_sc_at (\<lambda>sc. sc \<noteq> None) ptr and
-                                 (\<lambda>s. (weak_valid_sched_action s \<and> current_time_bounded s \<and>
-                                       (\<forall>ya. sc_tcb_sc_at ((=) (Some ya)) ptr s \<longrightarrow>
-                                             not_in_release_q ya s \<and> scheduler_act_not ya s)) \<and>
-                                      active_scs_valid s \<and>
-                                      sc_tcb_sc_at ((=) (Some t)) ptr s \<and>
-                                      bound_sc_tcb_at (\<lambda>a. a = Some ptr) t s)"
-                 in hoare_strengthen_post[rotated])
-           apply (clarsimp simp: sc_tcb_sc_at_def obj_at_def is_sc_obj invs_def valid_state_def
-                                 valid_pspace_def option.case_eq_if opt_map_red opt_pred_def)
-           apply (frule valid_ready_qs_in_correct_ready_q)
-           apply (drule valid_ready_qs_ready_qs_distinct)
-           apply (drule (1) valid_sched_context_size_objsI)
-           apply clarsimp
-           apply (clarsimp simp: pred_tcb_at_def obj_at_def vs_all_heap_simps option.case_eq_if
-                                 opt_map_red)
-           apply (rename_tac sc ta tcb tcb')
-           apply (drule_tac tp=ta in sym_ref_tcb_sc)
-             apply (fastforce+)[3]
-          apply ((wpsimp wp: valid_irq_node_typ obj_set_prop_at get_sched_context_wp ssc_refs_of_Some
-                            update_sched_context_valid_objs_same valid_ioports_lift
-                            update_sched_context_iflive_update update_sched_context_refs_of_update
-                            update_sched_context_cur_sc_tcb_None update_sched_context_valid_idle
-                      simp: invs'_def valid_pspace_def updateSchedContext_def
-                 | rule hoare_vcg_conj_lift update_sched_context_wp)+)[2]
-        apply (clarsimp simp: pred_conj_def)
-        apply ((wp set_tcb_sched_context_valid_ready_qs
-                   set_tcb_sched_context_valid_release_q_not_queued
-                   set_tcb_sched_context_simple_weak_valid_sched_action
-               | ((rule hoare_vcg_conj_lift)?, rule set_tcb_obj_ref_wp))+)[1]
-       apply (clarsimp simp: pred_conj_def valid_pspace'_def cong: conj_cong)
-       apply (wp threadSet_valid_objs' threadSet_iflive' threadSet_not_inQ threadSet_ifunsafe'T
-                 threadSet_idle'T threadSet_sch_actT_P[where P=False, simplified] threadSet_ctes_ofT
-                 threadSet_mdb' valid_irq_node_lift
-                 valid_irq_handlers_lift'' untyped_ranges_zero_lift threadSet_valid_dom_schedule'
-                 threadSet_ct_idle_or_in_cur_domain' threadSet_cur threadSet_valid_replies'
-                 sym_heap_sched_pointers_lift threadSet_tcbSchedNexts_of threadSet_tcbSchedPrevs_of
-                 threadSet_valid_sched_pointers threadSet_tcbInReleaseQueue threadSet_tcbQueued
-                 threadSet_cap_to
-              | clarsimp simp: tcb_cte_cases_def cteCaps_of_def cteSizeBits_def
-              | rule hoare_vcg_conj_lift hoare_vcg_all_lift hoare_vcg_imp_lift' refl)+
+    apply (rule corres_split_nor)
+       apply (clarsimp simp: set_tcb_obj_ref_thread_set sc_relation_def)
+       apply (rule threadset_corres; clarsimp simp: tcb_relation_def inQ_def)
+      apply (rule corres_split_nor)
+         apply (rule_tac f'="scTCB_update (\<lambda>_. Some t)"
+                      in updateSchedContext_no_stack_update_corres; clarsimp?)
+         apply (clarsimp simp: sc_relation_def refillSize_def)
+        apply (rule corres_split[OF ifCondRefillUnblockCheck_corres])
+          apply (rule corres_split_nor)
+             apply (rule schedContextResume_corres)
+            apply (rule corres_split_eqr)
+               apply (rule getSchedulable_corres)
+              apply (rule corres_when, simp)
+              apply (rule corres_split_nor)
+                 apply (rule tcbSchedEnqueue_corres, simp)
+                apply (rule rescheduleRequired_corres)
+               apply wp
+              apply (wpsimp wp: tcbSchedEnqueue_valid_tcbs')
+             apply wpsimp
+            apply (wpsimp wp: threadGet_wp getTCB_wp getSchedulable_wp simp: inReleaseQueue_def)
+           apply (rule_tac Q'="\<lambda>rv. valid_objs and pspace_aligned and pspace_distinct and (\<lambda>s. sym_refs (state_refs_of s)) and
+                                    weak_valid_sched_action and active_scs_valid and
+                                    sc_tcb_sc_at ((=) (Some t)) ptr and current_time_bounded and
+                                    bound_sc_tcb_at (\<lambda>sc. sc = Some ptr) t and
+                                    in_correct_ready_q and ready_or_release and ready_qs_distinct"
+                        in hoare_strengthen_post[rotated])
+            apply (fastforce simp: schedulable_def2)
+           apply (wp sched_context_resume_weak_valid_sched_action sched_context_resume_pred_tcb_at)
+          apply (rule_tac Q'="\<lambda>_. invs'" in hoare_strengthen_post[rotated], fastforce)
+          apply wp
+         apply (rule_tac Q'="\<lambda>_. valid_objs and pspace_aligned and pspace_distinct and
+                                 (\<lambda>s. sym_refs (state_refs_of s)) and current_time_bounded and
+                                 valid_ready_qs and valid_release_q and weak_valid_sched_action and
+                                 active_scs_valid and scheduler_act_not t and
+                                 sc_tcb_sc_at ((=) (Some t)) ptr and
+                                 bound_sc_tcb_at (\<lambda>a. a = Some ptr) t and
+                                 in_correct_ready_q and ready_or_release and ready_qs_distinct"
+                      in hoare_strengthen_post[rotated])
+          apply (clarsimp simp: sc_tcb_sc_at_def obj_at_def valid_sched_action_def dest!: sym[of "Some _"])
+         apply (wpsimp simp: if_cond_refill_unblock_check_def
+                         wp: refill_unblock_check_valid_release_q
+                             refill_unblock_check_valid_sched_action
+                             refill_unblock_check_active_scs_valid)
+        apply (rule_tac Q'="\<lambda>_. invs'" in hoare_strengthen_post[rotated], fastforce)
+        apply wpsimp
+       apply (rule_tac Q'="\<lambda>_. valid_objs and pspace_aligned and pspace_distinct and
+                               (\<lambda>s. sym_refs (state_refs_of s)) and
+                               valid_ready_qs and valid_release_q and active_scs_valid and
+                               ready_or_release and
+                               sc_tcb_sc_at (\<lambda>sc. sc \<noteq> None) ptr and
+                               (\<lambda>s. (weak_valid_sched_action s \<and> current_time_bounded s \<and>
+                                    (\<forall>ya. sc_tcb_sc_at ((=) (Some ya)) ptr s \<longrightarrow>
+                                          not_in_release_q ya s \<and> scheduler_act_not ya s)) \<and>
+                                    active_scs_valid s \<and>
+                                    sc_tcb_sc_at ((=) (Some t)) ptr s \<and>
+                                    bound_sc_tcb_at (\<lambda>a. a = Some ptr) t s)"
+                    in hoare_strengthen_post[rotated])
+        apply (clarsimp simp: sc_tcb_sc_at_def obj_at_def is_sc_obj invs_def valid_state_def
+                              valid_pspace_def option.case_eq_if opt_map_red opt_pred_def)
+        apply (frule valid_ready_qs_in_correct_ready_q)
+        apply (drule valid_ready_qs_ready_qs_distinct)
+        apply (drule (1) valid_sched_context_size_objsI)
+        apply clarsimp
+        apply (clarsimp simp: pred_tcb_at_def obj_at_def vs_all_heap_simps option.case_eq_if
+                              opt_map_red)
+        apply (rename_tac sc ta tcb tcb')
+        apply (drule_tac tp=ta in sym_ref_tcb_sc)
+          apply (fastforce+)[3]
+       apply ((wpsimp wp: valid_irq_node_typ obj_set_prop_at get_sched_context_wp ssc_refs_of_Some
+                          update_sched_context_valid_objs_same valid_ioports_lift
+                          update_sched_context_iflive_update update_sched_context_refs_of_update
+                          update_sched_context_cur_sc_tcb_None update_sched_context_valid_idle
+                    simp: invs'_def valid_pspace_def updateSchedContext_def
+               | rule hoare_vcg_conj_lift update_sched_context_wp)+)[2]
+     apply (clarsimp simp: pred_conj_def)
+     apply ((wp set_tcb_sched_context_valid_ready_qs
+                set_tcb_sched_context_valid_release_q_not_queued
+                set_tcb_sched_context_simple_weak_valid_sched_action
+             | ((rule hoare_vcg_conj_lift)?, rule set_tcb_obj_ref_wp))+)[1]
+    apply (clarsimp simp: pred_conj_def valid_pspace'_def cong: conj_cong)
+    apply (wp threadSet_valid_objs' threadSet_iflive' threadSet_not_inQ threadSet_ifunsafe'T
+              threadSet_idle'T threadSet_sch_actT_P[where P=False, simplified] threadSet_ctes_ofT
+              threadSet_mdb' valid_irq_node_lift
+              valid_irq_handlers_lift'' untyped_ranges_zero_lift threadSet_valid_dom_schedule'
+              threadSet_ct_idle_or_in_cur_domain' threadSet_cur threadSet_valid_replies'
+              sym_heap_sched_pointers_lift threadSet_tcbSchedNexts_of threadSet_tcbSchedPrevs_of
+              threadSet_valid_sched_pointers threadSet_tcbInReleaseQueue threadSet_tcbQueued
+              threadSet_cap_to
+           | clarsimp simp: tcb_cte_cases_def cteCaps_of_def cteSizeBits_def
+           | rule hoare_vcg_conj_lift hoare_vcg_all_lift hoare_vcg_imp_lift' refl)+
    apply (clarsimp simp: invs_def valid_state_def valid_pspace_def valid_sched_def)
    apply (intro conjI impI allI; (solves clarsimp)?)
             apply (fastforce simp: valid_obj_def obj_at_def sc_at_ppred_def is_sc_obj_def)
diff --git a/spec/abstract/Ipc_A.thy b/spec/abstract/Ipc_A.thy
index 1e111a6923..c0c7b51e8a 100644
--- a/spec/abstract/Ipc_A.thy
+++ b/spec/abstract/Ipc_A.thy
@@ -753,19 +753,21 @@ where
 
     if period = budget
     then refill_new sc_ptr MIN_REFILLS budget 0
-    else if 0 < sc_refill_max sc \<and> sc_tcb sc \<noteq> None
-         then do tcb_ptr \<leftarrow> assert_opt $ sc_tcb sc;
-                 st \<leftarrow> get_thread_state tcb_ptr;
-                 if runnable st
-                 then refill_update sc_ptr period budget mrefills
-                 else refill_new sc_ptr mrefills budget period
-              od
-         else refill_new sc_ptr mrefills budget period;
+    else do active \<leftarrow> get_sc_active sc_ptr;
+            if active \<and> sc_tcb sc \<noteq> None
+            then do tcb_ptr \<leftarrow> assert_opt $ sc_tcb sc;
+                    st \<leftarrow> get_thread_state tcb_ptr;
+                    if runnable st
+                    then refill_update sc_ptr period budget mrefills
+                    else refill_new sc_ptr mrefills budget period
+                 od
+            else refill_new sc_ptr mrefills budget period
+         od;
 
     when (sc_tcb sc \<noteq> None) $ do
+      sched_context_resume sc_ptr;
       tcb_ptr \<leftarrow> assert_opt $ sc_tcb sc;
       st \<leftarrow> get_thread_state tcb_ptr;
-      sched_context_resume sc_ptr;
       ct \<leftarrow> gets cur_thread;
       if tcb_ptr = ct then reschedule_required
       else when (runnable st) $ possible_switch_to tcb_ptr
diff --git a/spec/abstract/Structures_A.thy b/spec/abstract/Structures_A.thy
index 49a4b87ffa..4014401def 100644
--- a/spec/abstract/Structures_A.thy
+++ b/spec/abstract/Structures_A.thy
@@ -553,7 +553,7 @@ definition "refill_size_bytes = 16"
 definition max_num_refills :: "nat \<Rightarrow> nat" where (* max for extra_refills + MIN_REFILLS; refill_abosolute_max in C *)
   "max_num_refills sz = ((2 ^ sz) - sizeof_sched_context_t) div refill_size_bytes"
 
-definition "sc_sporadic_flag = 1"
+definition "sc_sporadic_flag = 0"
 
 definition
   default_sched_context :: sched_context where
diff --git a/spec/haskell/src/SEL4/API/Types/Universal.lhs b/spec/haskell/src/SEL4/API/Types/Universal.lhs
index 9f8bf346b0..63067431df 100644
--- a/spec/haskell/src/SEL4/API/Types/Universal.lhs
+++ b/spec/haskell/src/SEL4/API/Types/Universal.lhs
@@ -42,4 +42,4 @@ The following is the definition of the seven object types that are always availa
 > minSchedContextBits = 7
 
 > schedContextSporadicFlag :: Int
-> schedContextSporadicFlag = 1
+> schedContextSporadicFlag = 0
diff --git a/spec/haskell/src/SEL4/Object/SchedContext.lhs b/spec/haskell/src/SEL4/Object/SchedContext.lhs
index d9452f2ab9..1674acc18e 100644
--- a/spec/haskell/src/SEL4/Object/SchedContext.lhs
+++ b/spec/haskell/src/SEL4/Object/SchedContext.lhs
@@ -682,7 +682,9 @@ This module uses the C preprocessor to select a target architecture.
 
 >         if period == budget
 >            then refillNew scPtr minRefills budget 0
->            else if (0 < scRefillMax sc && scTCB sc /= Nothing)
+>            else do
+>                active <- scActive scPtr
+>                if (active && scTCB sc /= Nothing)
 >                    then do
 >                      runnable <- isRunnable $ fromJust $ scTCB sc
 >                      if runnable
@@ -691,8 +693,8 @@ This module uses the C preprocessor to select a target architecture.
 >                    else refillNew scPtr mRefills budget period
 
 >         when (scTCB sc /= Nothing) $ do
->             runnable <- isRunnable $ fromJust $ scTCB sc
 >             schedContextResume scPtr
+>             runnable <- isRunnable $ fromJust $ scTCB sc
 >             ctPtr <- getCurThread
 >             if (fromJust $ scTCB sc) == ctPtr
 >                 then rescheduleRequired