Prove schedContext_donate_ccorres

proof/crefine/RISCV64/ADT_C.thy

@@ -1143,21 +1143,21 @@ lemma map_to_cnes_eq:
   apply (clarsimp simp: projectKO_opt_cte split: kernel_object.splits)
   done
 
-lemma ksPSpace_valid_pspace_scRefs_nonzero:
-  "\<lbrakk>\<exists>s. ksPSpace s = ah \<and> valid_pspace' s; map_to_scs ah p = Some sc\<rbrakk> \<Longrightarrow>
+lemma map_to_scs_Some_scRefs_nonzero:
+  "\<lbrakk>map_to_scs (ksPSpace s) p = Some sc; valid_objs' s; no_0_obj' s\<rbrakk> \<Longrightarrow>
    scTCB sc \<noteq> Some 0 \<and> scReply sc \<noteq> Some 0 \<and> scNtfn sc \<noteq> Some 0 \<and> scYieldFrom sc \<noteq> Some 0"
-  apply (clarsimp simp: map_comp_def valid_pspace'_def split: option.splits)
+  apply (clarsimp simp: map_comp_def split: option.splits)
   by (fastforce simp: valid_obj'_def valid_sched_context'_def)
 
 lemma scRefills_unique:
-  assumes "refill_buffer_relation ah ch gs" "refill_buffer_relation ah' ch gs"
-      and "ksPSpace s = ah \<and> ksPSpace s p = Some (KOSchedContext sc) \<and> valid_sched_context' sc s"
-      and "ksPSpace s' = ah' \<and> ksPSpace s' p = Some (KOSchedContext sc') \<and> valid_sched_context' sc' s'"
+  assumes "refill_buffer_relation (ksPSpace as) ch gs" "refill_buffer_relation (ksPSpace as') ch gs"
+      and "ksPSpace as p = Some (KOSchedContext sc)" "valid_sched_context' sc as"
+      and "ksPSpace as' p = Some (KOSchedContext sc')" "valid_sched_context' sc' s'"
   shows   "scRefills sc = scRefills sc'"
   apply (insert assms)
   apply (clarsimp simp: valid_sched_context'_def)
-  apply (frule refill_buffer_relation_crefill_relation[where ah="ksPSpace s"])
-  apply (frule refill_buffer_relation_crefill_relation[where ah="ksPSpace s'"])
+  apply (frule refill_buffer_relation_crefill_relation[where ah="ksPSpace as"])
+  apply (frule refill_buffer_relation_crefill_relation[where ah="ksPSpace as'"])
   apply (clarsimp simp: Let_def)
   apply (drule_tac x=p in spec)+
   apply (rule list_eq_iff_nth_eq[THEN iffD2])
@@ -1177,61 +1177,102 @@ lemma scRefills_unique:
 
 lemma scSize_unique:
   assumes "refill_buffer_relation ah ch gs" "refill_buffer_relation ah' ch gs"
-      and "ksPSpace s = ah \<and> ksPSpace s p = Some (KOSchedContext sc)"
-      and "ksPSpace s' = ah' \<and> ksPSpace s' p = Some (KOSchedContext sc')"
+      and "ah p = Some (KOSchedContext sc)"
+      and "ah' p = Some (KOSchedContext sc')"
   shows   "scSize sc = scSize sc'"
   apply (insert assms)
-  apply (clarsimp simp: valid_sched_context'_def)
-  apply (frule refill_buffer_relation_size_eq[where ah="ksPSpace s"])
-  apply (frule refill_buffer_relation_size_eq[where ah="ksPSpace s'"])
+  apply (frule refill_buffer_relation_size_eq[where ah=ah])
+  apply (frule refill_buffer_relation_size_eq[where ah=ah'])
   apply (clarsimp simp: Let_def)
   apply (drule_tac x=p in spec)+
   by fastforce
 
+lemma
+  assumes "pspace_aligned' as" "pspace_distinct' as" "valid_sched_context' asc as"
+  shows tcb_at'_scTCB:
+    "\<forall>tcbPtr. scTCB asc = Some tcbPtr \<longrightarrow> tcb_at' tcbPtr as"
+  and reply_at'_scReply:
+    "\<forall>replyPtr. scReply asc = Some replyPtr \<longrightarrow> reply_at' replyPtr as"
+  and ntfn_at'_scNtfn:
+    "\<forall>ntfnPtr. scNtfn asc = Some ntfnPtr \<longrightarrow> ntfn_at' ntfnPtr as"
+  and tcb_at'_scYieldFrom:
+    "\<forall>tcbPtr. scYieldFrom asc = Some tcbPtr \<longrightarrow> tcb_at' tcbPtr as"
+  using assms
+  by (clarsimp simp: valid_sched_context'_def obj_at'_def)+
+
 lemma cpspace_sched_context_relation_unique:
-  assumes rels: "cpspace_sched_context_relation ah ch" "cpspace_sched_context_relation ah' ch"
-                "refill_buffer_relation ah ch gs" "refill_buffer_relation ah' ch gs"
-      and   vs: "\<exists>s. ksPSpace s = ah \<and> valid_pspace' s"
-      and  vs': "\<exists>s. ksPSpace s = ah' \<and> valid_pspace' s"
-  shows   "map_to_scs ah' = map_to_scs ah"
+  assumes rels: "cpspace_sched_context_relation (ksPSpace as) ch"
+                "cpspace_sched_context_relation (ksPSpace as') ch"
+                "refill_buffer_relation (ksPSpace as) ch gs"
+                "refill_buffer_relation (ksPSpace as') ch gs"
+  assumes   vs: "valid_objs' as" "no_0_obj' as"
+  assumes  vs': "valid_objs' as'" "no_0_obj' as'"
+  assumes  adb: "pspace_aligned' as" "pspace_distinct' as" "pspace_bounded' as"
+  assumes adb': "pspace_aligned' as'" "pspace_distinct' as'" "pspace_bounded' as'"
+  shows   "map_to_scs (ksPSpace as') = map_to_scs (ksPSpace as)"
   using rels
   apply (clarsimp simp: cmap_relation_def)
   apply (drule inj_image_inv[OF inj_Ptr])+
   apply simp
   apply (rule ext)
-  apply (rename_tac x)
-  apply (case_tac "x:dom (map_to_scs ah)")
+  apply (rename_tac p)
+  apply (case_tac "p \<in> dom (map_to_scs (ksPSpace as))")
    prefer 2
    apply (fastforce simp: dom_def)
   apply (drule bspec, assumption)+
-  apply (simp add: dom_def Collect_eq, drule_tac x=x in spec)
+  apply (simp add: dom_def Collect_eq, drule_tac x=p in spec)
   apply clarsimp
   apply (rename_tac sc sc')
-  apply (frule ksPSpace_valid_pspace_scRefs_nonzero[OF vs])
-  apply (frule ksPSpace_valid_pspace_scRefs_nonzero[OF vs'])
-  apply (cut_tac vs vs')
+  apply (prop_tac "valid_sched_context' sc as")
+   apply (fastforce dest: ksPSpace_valid_sched_context' map_to_ko_atI intro: vs adb map_to_ko_atI
+                    simp: obj_at'_def)
+  apply (prop_tac "valid_sched_context' sc' as'")
+   apply (fastforce dest: ksPSpace_valid_sched_context' map_to_ko_atI intro: vs' adb' map_to_ko_atI
+                    simp: obj_at'_def)
+  apply (frule map_to_scs_Some_scRefs_nonzero[OF _ vs])
+  apply (frule map_to_scs_Some_scRefs_nonzero[OF _ vs'])
+  apply (frule tcb_at'_scTCB[OF adb(1) adb(2)])
+  apply (frule tcb_at'_scTCB[OF adb'(1) adb'(2)])
+  apply (frule reply_at'_scReply[OF adb(1) adb(2)])
+  apply (frule reply_at'_scReply[OF adb'(1) adb'(2)])
+  apply (frule ntfn_at'_scNtfn[OF adb(1) adb(2)])
+  apply (frule ntfn_at'_scNtfn[OF adb'(1) adb'(2)])
+  apply (frule tcb_at'_scYieldFrom[OF adb(1) adb(2)])
+  apply (frule tcb_at'_scYieldFrom[OF adb'(1) adb'(2)])
+  apply (insert vs vs' adb adb')
   apply (clarsimp simp: valid_pspace'_def)
-  apply (rename_tac s s')
-  apply (frule (3) map_to_ko_atI)
-  apply (frule_tac v=sc in map_to_ko_atI, simp+)
-  apply (frule_tac v=sc' in map_to_ko_atI, simp+)
-  apply (clarsimp dest!: obj_at_valid_objs' split: option.splits)
-  apply (prop_tac "ksPSpace s x = Some (KOSchedContext sc)")
-   apply (clarsimp simp: map_comp_def split: option.splits)
-  apply (prop_tac "ksPSpace s' x = Some (KOSchedContext sc')")
-   apply (clarsimp simp: map_comp_def split: option.splits)
+  apply (frule (3) map_to_ko_atI[where s=as])
+  apply (frule (3) map_to_ko_atI[where s=as'])
+  apply (frule_tac p=p in scRefills_unique[where as=as and as'=as'])
+       apply force
+      apply (force simp: obj_at'_def)
+     apply force
+    apply (force simp: obj_at'_def)
+   apply force
+  apply (frule_tac p=p in scSize_unique[where ah="ksPSpace as" and ah'="ksPSpace as'"])
+     apply fastforce
+    apply (force simp: obj_at'_def)
+   apply (force simp: obj_at'_def)
   apply (thin_tac "map_to_scs x y = Some z" for x y z)+
-  apply (frule_tac s=s and s'=s' and p=x and sc=sc and sc'=sc'
-               and ah="ksPSpace s" and ah'="ksPSpace s'"
-                in scRefills_unique,
-         (fastforce simp: valid_obj'_def)+)
-  apply (frule_tac s=s and s'=s' and p=x and sc=sc and sc'=sc'
-               and ah="ksPSpace s" and ah'="ksPSpace s'"
-                in scSize_unique,
-         fastforce+)
-  apply (case_tac sc, case_tac sc', case_tac "the (clift ch (sched_context_Ptr x))")
-  by (auto simp: csched_context_relation_def option_to_ptr_def option_to_0_def
-          split: if_splits option.splits) \<comment> \<open>takes ~ a minute\<close>
+  apply (case_tac "the (clift ch (sched_context_Ptr p))")
+  apply (clarsimp simp: csched_context_relation_def)
+  apply (clarsimp simp: option_to_ctcb_ptr_def option_to_ptr_def option_to_0_def)
+  apply (rule sched_context.expand)
+  apply clarsimp
+  apply (intro conjI)
+     apply (case_tac "scTCB sc"; case_tac "scTCB sc'"; clarsimp)
+       apply (force dest!: kernel.tcb_at_not_NULL)
+      apply (force dest!: kernel.tcb_at_not_NULL)
+     apply (force simp: tcb_ptr_to_ctcb_ptr_inj)
+    apply (case_tac "scReply sc", case_tac "scReply sc'"; clarsimp)
+    apply (clarsimp split: option.splits)
+   apply (case_tac "scNtfn sc", case_tac "scNtfn sc'"; clarsimp)
+   apply (clarsimp split: option.splits)
+  apply (case_tac "scYieldFrom sc"; case_tac "scYieldFrom sc'"; clarsimp)
+    apply (force dest!: kernel.tcb_at_not_NULL)
+   apply (force dest!: kernel.tcb_at_not_NULL)
+  apply (force simp: tcb_ptr_to_ctcb_ptr_inj)
+  done
 
 lemma ksPSpace_valid_pspace_replyRefs_nonzero:
   "\<lbrakk>\<exists>s. ksPSpace s = ah \<and> valid_pspace' s; map_to_replies ah p = Some reply\<rbrakk> \<Longrightarrow>
@@ -1308,7 +1349,8 @@ proof -
     apply (drule (1) cpspace_user_data_relation_unique)
     apply (drule (1) cpspace_device_data_relation_unique)
     apply (drule (3) cpspace_sched_context_relation_unique)
-      apply (fastforce intro: valid_pspaces)+
+               apply (fastforce intro: no_0_objs no_0_objs' valid_objs valid_objs')+
+           apply (fastforce intro: aligned distinct bounded aligned' distinct' bounded')+
     apply (drule (1) cpspace_reply_relation_unique)
       apply (fastforce intro: valid_pspaces)+
     apply (thin_tac "cmap_relation a c f r" for a c f r)+

proof/crefine/RISCV64/Finalise_C.thy

@@ -1362,7 +1362,7 @@ lemma schedContext_cancelYieldTo_ccorres:
          apply clarsimp
          apply (rule rf_sr_sc_update_no_refill_buffer_update2; fastforce?)
            apply (simp add: typ_heap_simps')
-          apply (clarsimp simp: csched_context_relation_def Let_def
+          apply (clarsimp simp: csched_context_relation_def Let_def option_to_ctcb_ptr_def
                          split: if_splits)
          apply (fastforce intro: refill_buffer_relation_sc_no_refills_update)
         apply ceqv

proof/crefine/RISCV64/IpcCancel_C.thy

@@ -1877,7 +1877,7 @@ lemma rescheduleRequired_ccorres:
   "ccorres dc xfdc
      ((\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and valid_objs' and no_0_obj'
       and pspace_aligned' and pspace_distinct')
-     UNIV []
+     UNIV hs
      rescheduleRequired (Call rescheduleRequired_'proc)"
   supply if_split[split del]
   apply cinit

proof/crefine/RISCV64/Ipc_C.thy

@@ -5009,11 +5009,101 @@ lemma reply_push_ccorres:
      (replyPush callerPtr calleePtr replyPtr canDonate) (Call reply_push_'proc)"
 sorry (* FIXME RT: reply_push_ccorres *)
 
+(* Note that valid_objs' can be removed from the Haskell guard by asserting valid_objs' within
+   schedContextDonate *)
 lemma schedContext_donate_ccorres:
   "ccorres dc xfdc
-     \<top> (\<lbrace>\<acute>sc = Ptr callerPtr\<rbrace> \<inter> \<lbrace>\<acute>to = tcb_ptr_to_ctcb_ptr tcbPtr\<rbrace>) []
+     (sc_at' scPtr and tcb_at' tcbPtr and valid_objs' and no_0_obj'
+      and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and pspace_aligned' and pspace_distinct')
+     (\<lbrace>\<acute>sc = Ptr scPtr\<rbrace> \<inter> \<lbrace>\<acute>to = tcb_ptr_to_ctcb_ptr tcbPtr\<rbrace>) []
      (schedContextDonate scPtr tcbPtr) (Call schedContext_donate_'proc)"
-sorry (* FIXME RT: schedContext_donate_ccorres *)
+  (is "ccorres _ _ ?abs _ _ _ _")
+  apply (cinit lift: sc_' to_')
+   apply (rule ccorres_pre_getObject_sc, rename_tac sc)
+   apply (rule ccorres_move_c_guard_sc)
+   apply (rule_tac xf'=from_'
+               and val="option_to_ctcb_ptr (scTCB sc)"
+               and R="ko_at' sc scPtr"
+               and R'=UNIV
+                in ccorres_symb_exec_r_known_rv)
+      apply (rule conseqPre, vcg)
+      apply clarsimp
+      apply (frule (1) obj_at_cslift_sc)
+      apply (clarsimp simp: csched_context_relation_def typ_heap_simps)
+     apply ceqv
+    apply (clarsimp simp: when_def)
+    apply (rule_tac r'=dc and xf'=xfdc in ccorres_split_nothrow)
+        apply (rule_tac Q="no_0_obj' and ko_at' sc scPtr and valid_objs'"
+                    and Q'="\<lambda>s'. from_' s' = option_to_ctcb_ptr (scTCB sc)"
+                     in ccorres_cond_both')
+          apply (fastforce dest: tcb_at_not_NULL sc_ko_at_valid_objs_valid_sc'
+                           simp: option_to_ctcb_ptr_def valid_sched_context'_def
+                          split: option.splits)
+         apply (rule ccorres_rhs_assoc)+
+         apply (ctac add: tcbSchedDequeue_ccorres)
+           apply (ctac add: tcbReleaseRemove_ccorres)
+             apply (rule ccorres_move_c_guard_tcb)
+             apply (rule_tac r'=dc and xf'=xfdc in ccorres_split_nothrow)
+                 apply (rule_tac R="{s'. from_' s' = option_to_ctcb_ptr (scTCB sc)}"
+                             and P'="valid_objs' and no_0_obj' and ko_at' sc scPtr"
+                              in threadSet_ccorres_lemma4[where P=\<top>])
+                  apply vcg
+                 subgoal
+                   by (fastforce intro!: rf_sr_tcb_update_no_queue_gen2
+                                   simp: typ_heap_simps' option_to_ctcb_ptr_def tcb_cte_cases_def
+                                         cteSizeBits_def ctcb_relation_def)
+                apply ceqv
+               apply (rule ccorres_pre_getCurThread)
+               apply (rule ccorres_pre_getSchedulerAction)
+               apply (rule_tac Q="\<lambda>s. action = ksSchedulerAction s \<and> cur = ksCurThread s
+                                      \<and> valid_objs' s \<and> no_0_obj' s \<and> ko_at' sc scPtr s"
+                           and Q'="\<lambda>s'. from_' s' = option_to_ctcb_ptr (scTCB sc)"
+                            in ccorres_cond_both')
+                 apply clarsimp
+                 apply (prop_tac "tcb_at' (the (scTCB sc)) s")
+                  apply (fastforce dest!: sc_ko_at_valid_objs_valid_sc'
+                                    simp: valid_sched_context'_def)
+                 subgoal
+                   by (force dest: tcb_at_not_NULL tcb_at_1
+                             simp: rf_sr_def cstate_relation_def Let_def option_to_ctcb_ptr_def
+                                   cscheduler_action_relation_def
+                            split: scheduler_action.splits)
+                apply (ctac add: rescheduleRequired_ccorres)
+               apply (rule ccorres_return_Skip)
+              apply (rule_tac Q'="\<lambda>_. ?abs and ko_at' sc scPtr" in hoare_post_imp)
+               apply clarsimp
+              apply wpsimp
+             apply vcg
+            apply wpsimp
+           apply (vcg exspec=tcbReleaseRemove_modifies)
+          apply wpsimp
+         apply (vcg exspec=tcbSchedDequeue_modifies)
+        apply (rule ccorres_return_Skip)
+       apply ceqv
+      apply (rule_tac r'=dc and xf'=xfdc in 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 option_to_ctcb_ptr_def)
+         apply ceqv
+        apply (rule threadSet_ccorres_lemma2[where P=\<top>])
+         apply vcg
+        subgoal
+          by (fastforce intro!: rf_sr_tcb_update_no_queue_gen2
+                          simp: typ_heap_simps' tcb_cte_cases_def cteSizeBits_def ctcb_relation_def)
+       apply wpsimp
+      apply vcg
+     apply (wpsimp wp: hoare_drop_imps)
+    apply (vcg exspec=tcbSchedDequeue_modifies
+               exspec=tcbReleaseRemove_modifies
+               exspec=rescheduleRequired_modifies)
+   apply vcg
+  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 split: option.splits)
+  done
 
 lemma sendIPC_ccorres [corres]:
   "ccorres dc xfdc (invs' and st_tcb_at' simple' thread

proof/crefine/RISCV64/IsolatedThreadAction.thy

@@ -920,7 +920,7 @@ lemma tcbReleaseRemove_tcbPriority[wp]:
 
 lemma schedContextDonate_tcbPriority[wp]:
   "schedContextDonate scPtr tcbPtr \<lbrace>obj_at' (\<lambda>tcb. P (tcbPriority tcb)) t\<rbrace>"
-  apply (simp add: schedContextDonate_def)
+  apply (simp add: schedContextDonate_def updateSchedContext_def)
   by (wpsimp wp: hoare_drop_imps)
 
 lemma asUser_obj_at_unchangedT:

proof/crefine/RISCV64/Retype_C.thy

@@ -4770,7 +4770,7 @@ proof (intro impI allI)
        (the (sc_of' ko))
        (from_bytes (replicate (size_of TYPE(sched_context_C)) 0))"
     unfolding csched_context_relation_def sched_context_C_size
-    apply (simp add: makeObject_sc size_of_def projectKO_opt_sc ko_def)
+    apply (simp add: makeObject_sc size_of_def projectKO_opt_sc ko_def option_to_ctcb_ptr_def)
     apply (simp add: from_bytes_def)
     apply (simp add: typ_info_simps sched_context_C_tag_def)
     apply (simp add: ti_typ_pad_combine_empty_ti ti_typ_pad_combine_td align_of_def padup_def

proof/crefine/RISCV64/StateRelation_C.thy

@@ -386,12 +386,12 @@ definition csched_context_relation :: "Structures_H.sched_context \<Rightarrow>
   "csched_context_relation asc csc \<equiv>
        scPeriod asc = scPeriod_C csc
      \<and> scConsumed asc = scConsumed_C csc
-     \<and> option_to_ptr (scTCB asc) = scTcb_C csc
+     \<and> option_to_ctcb_ptr (scTCB asc) = scTcb_C csc
      \<and> option_to_ptr (scReply asc) = scReply_C csc
      \<and> option_to_ptr (scNtfn asc) = scNotification_C csc
      \<and> scBadge asc = scBadge_C csc
      \<and> scSporadic asc = to_bool (scSporadic_C csc)
-     \<and> option_to_ptr (scYieldFrom asc) = scYieldFrom_C csc
+     \<and> option_to_ctcb_ptr (scYieldFrom asc) = scYieldFrom_C csc
      \<and> scRefillMax asc = unat (scRefillMax_C csc)
      \<and> scRefillHead asc = unat (scRefillHead_C csc)
      \<and> scRefillTail asc = unat (scRefillTail_C csc)"

proof/refine/RISCV64/Ipc_R.thy

@@ -6178,35 +6178,6 @@ lemma bindScReply_valid_idle':
   unfolding bindScReply_def
   by (wpsimp wp: hoare_vcg_imp_lift' hoare_vcg_all_lift set_reply'.obj_at')
 
-lemma replyPush_valid_idle':
-  "\<lbrace>valid_idle'
-    and valid_pspace'
-    and (\<lambda>s. callerPtr \<noteq> ksIdleThread s)
-    and sym_heap_tcbSCs\<rbrace>
-   replyPush callerPtr calleePtr replyPtr canDonate
-   \<lbrace>\<lambda>_. valid_idle'\<rbrace>"
-  apply (simp only: replyPush_def)
-  supply if_split [split del]
-  apply wpsimp
-         apply (wpsimp wp: schedContextDonate_valid_idle' bindScReply_valid_idle')+
-       apply (wpsimp wp: hoare_vcg_if_lift2 hoare_vcg_imp_lift')
-      apply (wpsimp wp: hoare_vcg_if_lift2 hoare_vcg_imp_lift')
-     apply (wpsimp wp: threadGet_wp)+
-  apply (clarsimp simp: tcb_at'_ex_eq_all valid_pspace'_def)
-  apply (subgoal_tac "\<forall>kob. valid_reply' kob s \<longrightarrow> valid_reply' (replyTCB_update (\<lambda>_. Some callerPtr) kob) s")
-   apply (subgoal_tac "calleePtr \<noteq> idle_thread_ptr", simp)
-    apply (subgoal_tac "y \<noteq> idle_sc_ptr", simp)
-     apply (erule (3) not_idle_scTCB)
-     apply (frule (1) tcb_ko_at_valid_objs_valid_tcb')
-     apply (clarsimp simp: valid_tcb'_def)
-    apply (frule (2) not_idle_tcbSC[where p=callerPtr])
-      apply (clarsimp simp: valid_idle'_def)
-     apply (clarsimp simp: obj_at'_real_def ko_wp_at'_def)
-    apply (clarsimp simp: obj_at'_real_def ko_wp_at'_def)
-   apply (clarsimp simp: valid_idle'_def idle_tcb'_def obj_at'_real_def ko_wp_at'_def)
-  apply (clarsimp simp: valid_reply'_def)
-  done
-
 lemma replyPush_untyped_ranges_zero'[wp]:
   "replyPush callerPtr calleePtr replyPtr canDonate \<lbrace>untyped_ranges_zero'\<rbrace>"
   apply (clarsimp simp: untyped_ranges_zero_inv_null_filter_cteCaps_of)
@@ -6724,8 +6695,7 @@ lemma si_invs'_helper2:
         od)
   \<lbrace>\<lambda>b s. invs' s \<and> tcb_at' d s \<and> ex_nonz_cap_to' d s
          \<and> st_tcb_at' (Not \<circ> is_BlockedOnReply) d s\<rbrace>"
-  apply (wpsimp wp: ex_nonz_cap_to_pres' schedContextDonate_invs' replyPush_invs'
-                    replyPush_valid_idle' sts_invs_minor' schedContextDonate_valid_idle'
+  apply (wpsimp wp: ex_nonz_cap_to_pres' schedContextDonate_invs' replyPush_invs' sts_invs_minor'
                     replyPush_st_tcb_at'_not_caller sts_st_tcb' threadGet_wp)
   apply (frule_tac P'="(\<lambda>st'. \<forall>rptr. st' \<noteq> BlockedOnReply rptr)" in pred_tcb'_weakenE)
    apply (clarsimp simp: is_BlockedOnReply_def)