rt proof: rename whileLoop_wp'

Signed-off-by: Corey Lewis <corey.lewis@proofcraft.systems>

proof/invariant-abstract/ARM/ArchVSpaceEntries_AI.thy

@@ -430,14 +430,14 @@ lemma as_user_valid_pdpt_objs[wp]:
 
 crunch valid_pdpt_objs[wp]: send_signal, send_ipc "valid_pdpt_objs"
   (wp: get_sched_context_wp mapM_wp' maybeM_inv hoare_vcg_if_lift2 hoare_drop_imps
-       transfer_caps_loop_pres whileLoop_wp'
+       transfer_caps_loop_pres whileLoop_valid_inv
   simp: zipWithM_x_mapM
   ignore: set_thread_state_act set_object test_reschedule)
 
 crunch valid_pdpt_objs[wp]: cancel_all_ipc, cancel_all_signals, unbind_maybe_notification,
   sched_context_maybe_unbind_ntfn, reply_unlink_tcb,
   sched_context_unbind_all_tcbs, sched_context_unbind_ntfn "valid_pdpt_objs"
-  (wp: maybeM_inv hoare_drop_imp mapM_x_wp' whileLoop_wp' ignore: tcb_release_remove
+  (wp: maybeM_inv hoare_drop_imp mapM_x_wp' whileLoop_valid_inv ignore: tcb_release_remove
    simp: crunch_simps is_round_robin_def)
 
 crunch valid_pdpt_objs[wp]:
@@ -1150,7 +1150,7 @@ crunch valid_pdpt_objs[wp]: end_timeslice "valid_pdpt_objs::det_state \<Rightarr
 
 crunches check_budget_restart, invoke_sched_control_configure_flags
   for valid_pdpt_objs[wp]: "valid_pdpt_objs::det_state \<Rightarrow> _"
-  (wp: hoare_drop_imps hoare_vcg_if_lift2 whileLoop_wp' hoare_vcg_all_lift
+  (wp: hoare_drop_imps hoare_vcg_if_lift2 whileLoop_valid_inv hoare_vcg_all_lift
   simp: Let_def ignore: tcb_release_remove)
 
 lemma perform_invocation_valid_pdpt[wp]:

proof/invariant-abstract/Bits_AI.thy

@@ -8,7 +8,7 @@ theory Bits_AI
 imports ArchBits_AI
 begin
 
-lemmas crunch_wps = hoare_drop_imps mapM_wp' mapM_x_wp' whileLoop_wp'
+lemmas crunch_wps = hoare_drop_imps mapM_wp' mapM_x_wp' whileLoop_valid_inv
 
 lemmas crunch_simps = split_def whenE_def unlessE_def Let_def if_fun_split
                       assertE_def zipWithM_mapM zipWithM_x_mapM

proof/invariant-abstract/DetSchedDomainTime_AI.thy

@@ -106,7 +106,7 @@ crunches reply_remove, sched_context_unbind_tcb, sched_context_zero_refill_max
   (wp: hoare_drop_imps get_simple_ko_wp)
 
 crunch domain_list_inv[wp]: cancel_all_ipc, cancel_all_signals "\<lambda>s. P (domain_list s)"
-  (wp: hoare_drop_imps mapM_x_wp' whileLoop_wp')
+  (wp: hoare_drop_imps mapM_x_wp' whileLoop_valid_inv)
 
 crunch domain_list_inv[wp]: finalise_cap "\<lambda>s::det_state. P (domain_list s)"
   (wp: crunch_wps maybeM_inv dxo_wp_weak select_inv simp: crunch_simps)
@@ -204,7 +204,7 @@ crunches
   set_priority, restart, sched_context_bind_tcb,sched_context_bind_ntfn,
   sched_context_unbind_reply, sched_context_yield_to
   for domain_list_inv[wp]: "\<lambda>s. P (domain_list s)"
-  (wp: hoare_drop_imps mapM_wp' maybeM_inv whileLoop_wp' simp: crunch_simps)
+  (wp: hoare_drop_imps mapM_wp' maybeM_inv whileLoop_valid_inv simp: crunch_simps)
 
 context DetSchedDomainTime_AI begin
 

proof/invariant-abstract/Deterministic_AI.thy

@@ -3956,7 +3956,7 @@ crunches
   sched_context_unbind_ntfn, sched_context_maybe_unbind_ntfn,
   sched_context_unbind_yield_from, cancel_all_ipc, thread_set, reply_remove_tcb
   for valid_list[wp]: valid_list
-  (wp: mapM_x_wp' hoare_drop_imp whileLoop_wp' simp: is_round_robin_def crunch_simps)
+  (wp: mapM_x_wp' hoare_drop_imp whileLoop_valid_inv simp: is_round_robin_def crunch_simps)
 
 crunch all_but_exst[wp]: update_work_units "all_but_exst P"
 
@@ -4063,7 +4063,7 @@ crunch valid_list[wp]: do_fault_transfer valid_list
   (wp: mapM_wp hoare_drop_imp ignore: make_fault_msg)
 
 crunch valid_list[wp]: transfer_caps,do_normal_transfer,do_ipc_transfer,refill_unblock_check valid_list
-  (wp: mapM_wp hoare_drop_imp whileLoop_wp')
+  (wp: mapM_wp hoare_drop_imp whileLoop_valid_inv)
 
 lemma send_ipc_valid_list[wp]:
   "send_ipc block call badge can_grant can_reply_grant can_donate thread epptr \<lbrace>valid_list\<rbrace>"
@@ -4089,7 +4089,7 @@ crunches set_refills,refill_size, schedule_used
 lemma refill_budget_check_valid_list[wp]:
   "refill_budget_check usage \<lbrace>valid_list\<rbrace>"
   unfolding refill_budget_check_defs
-  apply (wpsimp wp: whileLoop_wp' hoare_drop_imps)
+  apply (wpsimp wp: whileLoop_valid_inv hoare_drop_imps)
   done
 
 lemma refill_budget_check_round_robin_valid_list[wp]:

proof/invariant-abstract/IpcCancel_AI.thy

@@ -2400,7 +2400,7 @@ lemma refill_unblock_check_obj_at_impossible':
    refill_unblock_check sc_opt
    \<lbrace>\<lambda>s. P (obj_at P' p s)\<rbrace>"
   unfolding refill_unblock_check_def
-  by (wpsimp wp: whileLoop_wp' update_sched_context_wp get_refills_wp
+  by (wpsimp wp: whileLoop_valid_inv update_sched_context_wp get_refills_wp
            simp: refill_head_overlapping_loop_def merge_refills_def update_refill_hd_def
                  refill_pop_head_def is_round_robin_def
     | clarsimp elim!: rsubst[where P=P] simp: obj_at_def)+

proof/invariant-abstract/SchedContextInv_AI.thy

@@ -1486,7 +1486,7 @@ lemma set_refills_active_sc_at[wp]:
 lemma refill_unblock_check_active_sc_at[wp]:
   "refill_unblock_check sc_ptr \<lbrace>\<lambda>s. Q (active_sc_at sc_ptr s)\<rbrace>"
   apply (clarsimp simp: refill_unblock_check_defs simp del: update_refill_hd_def)
-  apply (wpsimp wp: set_refills_wp get_refills_wp whileLoop_wp'
+  apply (wpsimp wp: set_refills_wp get_refills_wp whileLoop_valid_inv
               simp: update_refill_hd_rewrite update_sched_context_set_refills_rewrite active_sc_at_def)
   done
 
@@ -1580,7 +1580,7 @@ lemma set_sc_obj_ref_active:
 
 crunches commit_time
   for sc_active: "active_sc_at sc_ptr"
-  (wp: set_sc_obj_ref_active whileLoop_wp' crunch_wps simp: crunch_simps)
+  (wp: set_sc_obj_ref_active whileLoop_valid_inv crunch_wps simp: crunch_simps)
 
 lemma sc_badge_update_active[wp]:
   "set_sc_obj_ref sc_badge_update sc_ptr x \<lbrace>active_sc_at p'\<rbrace>"

proof/invariant-abstract/SchedContext_AI.thy

@@ -177,7 +177,7 @@ lemma update_refill_tl_valid_objs[wp]:
 
 lemma refill_unblock_check_valid_objs[wp]:
   "refill_unblock_check sc_ptr \<lbrace>valid_objs\<rbrace>"
-  by (wpsimp wp: set_refills_valid_objs whileLoop_wp' get_refills_wp
+  by (wpsimp wp: set_refills_valid_objs whileLoop_valid_inv get_refills_wp
                  hoare_drop_imps
            simp: refill_unblock_check_defs)
 
@@ -208,7 +208,7 @@ lemma refill_pop_head_valid_objs[wp]:
 lemma head_insufficient_loop_valid_objs[wp]:
   "head_insufficient_loop usage \<lbrace>valid_objs\<rbrace>"
   unfolding head_insufficient_loop_def
-  by (wpsimp wp: whileLoop_wp' simp: non_overlapping_merge_refills_def update_refill_hd_def)
+  by (wpsimp wp: whileLoop_valid_inv simp: non_overlapping_merge_refills_def update_refill_hd_def)
 
 lemma schedule_used_valid_objs[wp]:
   "schedule_used sc_ptr new \<lbrace>valid_objs\<rbrace>"
@@ -221,7 +221,7 @@ lemma handle_overrun_loop_valid_objs[wp]:
   "handle_overrun_loop usage \<lbrace>valid_objs\<rbrace>"
   unfolding handle_overrun_loop_def handle_overrun_loop_body_def refill_single_def refill_size_def
             update_refill_hd_def
-  apply (wpsimp wp: whileLoop_wp'
+  apply (wpsimp wp: whileLoop_valid_inv
               simp: valid_sched_context_def)
   done
 
@@ -527,15 +527,15 @@ crunches head_insufficient_loop, handle_overrun_loop
 
 lemma refill_budget_check_if_live_then_nonz_cap[wp]:
   "refill_budget_check usage \<lbrace>if_live_then_nonz_cap\<rbrace>"
-  apply (wpsimp wp: whileLoop_wp' get_refills_wp hoare_drop_imps
+  apply (wpsimp wp: whileLoop_valid_inv get_refills_wp hoare_drop_imps
                     hoare_vcg_all_lift hoare_vcg_if_lift2
               simp: refill_budget_check_def update_refill_hd_def)
   done
 
 lemma refill_unblock_check_refs_of[wp]:
   "refill_unblock_check sc_ptr \<lbrace>\<lambda>s. P (state_refs_of s)\<rbrace>"
   apply (wpsimp simp: refill_unblock_check_defs
-                  wp: hoare_drop_imp whileLoop_wp')
+                  wp: hoare_drop_imp whileLoop_valid_inv)
   apply (clarsimp simp: state_refs_of_def)
   done
 
@@ -613,7 +613,7 @@ lemma refill_budget_check_invs[wp]:
   "refill_budget_check usage \<lbrace>invs\<rbrace>"
   unfolding refill_budget_check_def
   apply (wpsimp simp: refill_budget_check_defs
-                  wp: hoare_drop_imp whileLoop_wp' hoare_vcg_if_lift2)
+                  wp: hoare_drop_imp whileLoop_valid_inv hoare_vcg_if_lift2)
   done
 
 lemma update_sched_context_valid_irq_node [wp]:
@@ -776,7 +776,7 @@ crunches head_insufficient_loop, handle_overrun_loop
 lemma refill_budget_check_valid_replies_pred[wp]:
   "refill_budget_check usage \<lbrace> valid_replies_pred P \<rbrace>"
   apply (wpsimp simp: refill_budget_check_def
-                  wp: get_refills_wp whileLoop_wp' hoare_drop_imps
+                  wp: get_refills_wp whileLoop_valid_inv hoare_drop_imps
                       hoare_vcg_all_lift hoare_vcg_if_lift2)
   done
 
@@ -882,7 +882,7 @@ crunches handle_overrun_loop, head_insufficient_loop
 lemma refill_budget_check_bound_sc_tcb_at_ct[wp]:
   "refill_budget_check usage \<lbrace>\<lambda>s. bound_sc_tcb_at P (cur_thread s) s\<rbrace>"
   unfolding refill_budget_check_def
-  apply (wpsimp wp: whileLoop_wp' get_refills_wp hoare_drop_imps hoare_vcg_all_lift
+  apply (wpsimp wp: whileLoop_valid_inv get_refills_wp hoare_drop_imps hoare_vcg_all_lift
                     hoare_vcg_if_lift2)
   done
 
@@ -897,7 +897,7 @@ lemma commit_time_bound_sc_tcb_at [wp]:
 lemma refill_unblock_check_bound_sc_tcb_at [wp]:
   "refill_unblock_check sc_ptr \<lbrace>\<lambda>s. bound_sc_tcb_at ((=) (Some sc)) (cur_thread s) s\<rbrace>"
   unfolding refill_unblock_check_defs
-  apply (wpsimp wp: whileLoop_wp' get_refills_wp hoare_drop_imps)
+  apply (wpsimp wp: whileLoop_valid_inv get_refills_wp hoare_drop_imps)
   done
 
 crunches if_cond_refill_unblock_check
@@ -996,7 +996,7 @@ crunches head_insufficient_loop, handle_overrun_loop
 lemma refill_budget_check_ct_in_state[wp]:
   "refill_budget_check usage \<lbrace> ct_in_state t \<rbrace>"
   unfolding refill_budget_check_def
-  apply (wpsimp wp: whileLoop_wp' get_refills_wp hoare_drop_imps hoare_vcg_all_lift
+  apply (wpsimp wp: whileLoop_valid_inv get_refills_wp hoare_drop_imps hoare_vcg_all_lift
                     hoare_vcg_if_lift2)
   done
 
@@ -1011,7 +1011,7 @@ crunch ct_in_state[wp]: commit_time "ct_in_state t"
 lemma refill_unblock_check_ct_in_state[wp]:
   "refill_unblock_check csc \<lbrace> ct_in_state t \<rbrace>"
   unfolding refill_unblock_check_defs
-  apply (wpsimp wp: whileLoop_wp' get_refills_wp hoare_drop_imps)
+  apply (wpsimp wp: whileLoop_valid_inv get_refills_wp hoare_drop_imps)
   done
 
 lemma switch_sched_context_ct_in_state[wp]:
@@ -1714,7 +1714,7 @@ lemma refill_unblock_check_state_refs_of_ct[wp]:
    apply (clarsimp simp: state_refs_of_def obj_at_def
                  intro!: ext elim!: rsubst[where P="\<lambda>x. P x (cur_thread s)" for s])+
   apply (wpsimp simp: set_refills_def
-                  wp: update_sched_context_wp get_refills_wp whileLoop_wp')
+                  wp: update_sched_context_wp get_refills_wp whileLoop_valid_inv)
    apply (clarsimp simp: state_refs_of_def obj_at_def
                  intro!: ext elim!: rsubst[where P="\<lambda>x. P x (cur_thread s)" for s])+
   done
@@ -1723,7 +1723,7 @@ lemma refill_unblock_check_it_ct[wp]:
   "refill_unblock_check scp \<lbrace>\<lambda>s. P (idle_thread s) (cur_thread s)\<rbrace>"
   apply (wpsimp simp: refill_unblock_check_defs set_refills_def update_sched_context_def
                       set_object_def
-                  wp: get_refills_wp get_object_wp whileLoop_wp')
+                  wp: get_refills_wp get_object_wp whileLoop_valid_inv)
   done
 
 lemma get_sc_refill_capacity_sp:

proof/refine/ARM/IpcCancel_R.thy

@@ -3185,7 +3185,7 @@ lemma refillPopHead_valid_pspace'[wp]:
    refillPopHead scp
    \<lbrace>\<lambda>_. valid_pspace'\<rbrace>"
   unfolding refillPopHead_def updateSchedContext_def
-  apply (wpsimp wp: whileLoop_wp')
+  apply (wpsimp wp: whileLoop_valid_inv)
   by (fastforce simp: obj_at'_def projectKOs valid_obj'_def refillNextIndex_def MIN_REFILLS_def
                       valid_sched_context'_def valid_sched_context_size'_def scBits_simps objBits_simps
                dest!: opt_predD
@@ -3194,7 +3194,7 @@ lemma refillPopHead_valid_pspace'[wp]:
 lemma refillUnblockCheck_ko_wp_at_not_live[wp]:
   "refillUnblockCheck scp \<lbrace>\<lambda>s. P (ko_wp_at' (Not \<circ> live') p' s)\<rbrace>"
   unfolding refillUnblockCheck_def refillHeadOverlappingLoop_def mergeRefills_def
-  apply (wpsimp wp: whileLoop_wp' updateSchedContext_wp hoare_drop_imps
+  apply (wpsimp wp: whileLoop_valid_inv updateSchedContext_wp hoare_drop_imps
               simp: updateRefillHd_def refillPopHead_def)
         apply (clarsimp simp: ko_wp_at'_def obj_at'_def projectKOs runReaderT_def
                               opt_map_red refillNextIndex_def
@@ -3220,7 +3220,7 @@ lemma refillUnblockCheck_refs_of'[wp]:
   "refillUnblockCheck sc_ptr \<lbrace>\<lambda>s. P (state_refs_of' s)\<rbrace>"
   unfolding refillUnblockCheck_def refillHeadOverlappingLoop_def mergeRefills_def
   apply (wpsimp simp: updateRefillHd_def refillPopHead_def
-                  wp: hoare_drop_imp whileLoop_wp' isRoundRobin_wp updateSchedContext_wp)
+                  wp: hoare_drop_imp whileLoop_valid_inv isRoundRobin_wp updateSchedContext_wp)
         apply (clarsimp simp: runReaderT_def elim!: rsubst[where P=P])
         apply (clarsimp simp: obj_at'_def projectKOs opt_map_red refillNextIndex_def)
         apply (fastforce simp: state_refs_of'_def get_refs_def2 ps_clear_upd objBits_simps option.case_eq_if

proof/refine/ARM/Ipc_R.thy

@@ -5722,7 +5722,7 @@ lemma refillUnblockCheck_sym_heap_tcbSCs[wp]:
    \<lbrace>\<lambda>_. sym_heap_tcbSCs\<rbrace>"
   supply opt_mapE [rule del]
   unfolding refillUnblockCheck_def refillHeadOverlappingLoop_def mergeRefills_def updateRefillHd_def
-  apply (wpsimp wp: whileLoop_wp' updateSchedContext_wp wp_del: use_corresK
+  apply (wpsimp wp: whileLoop_valid_inv updateSchedContext_wp wp_del: use_corresK
               simp: refillPopHead_def)
         apply (clarsimp simp: sym_heap_def obj_at'_def projectKOs ps_clear_upd opt_map_red projectKO_opt_tcb)
        apply (wpsimp wp: updateSchedContext_wp getCurTime_wp refillReady_wp isRoundRobin_wp
@@ -5746,7 +5746,7 @@ lemma refillUnblockCheck_sym_heap_scReplies[wp]:
    \<lbrace>\<lambda>_. sym_heap_scReplies\<rbrace>"
   supply opt_mapE [rule del]
   unfolding refillUnblockCheck_def refillHeadOverlappingLoop_def mergeRefills_def updateRefillHd_def
-  apply (wpsimp wp: whileLoop_wp' updateSchedContext_wp wp_del: use_corresK
+  apply (wpsimp wp: whileLoop_valid_inv updateSchedContext_wp wp_del: use_corresK
               simp: refillPopHead_def)
         apply (clarsimp simp: sym_heap_def obj_at'_def projectKOs ps_clear_upd opt_map_red projectKO_opt_reply)
         apply (drule_tac x=scp and y=p' in spec2)

proof/refine/ARM/Schedule_R.thy

@@ -2402,7 +2402,7 @@ lemma refillUnblockCheck_valid_machine_state'[wp]:
                         refillHeadOverlappingLoop_def mergeRefills_def updateRefillHd_def
                         refillPopHead_def updateSchedContext_def setReprogramTimer_def
                         valid_machine_state'_def pointerInUserData_def pointerInDeviceData_def)
-  apply (wpsimp wp: whileLoop_wp' hoare_vcg_all_lift hoare_vcg_disj_lift scActive_wp
+  apply (wpsimp wp: whileLoop_valid_inv hoare_vcg_all_lift hoare_vcg_disj_lift scActive_wp
                     hoare_drop_imps getRefillNext_wp)
   apply fastforce
   done
@@ -2412,7 +2412,7 @@ lemma refillUnblockCheck_list_refs_of_replies'[wp]:
   apply (clarsimp simp: refillUnblockCheck_def valid_mdb'_def refillHeadOverlappingLoop_def
                         mergeRefills_def updateRefillHd_def refillPopHead_def updateSchedContext_def
                         setReprogramTimer_def refillReady_def isRoundRobin_def)
-  apply (wpsimp wp: whileLoop_wp' hoare_drop_imps scActive_wp getRefillNext_wp
+  apply (wpsimp wp: whileLoop_valid_inv hoare_drop_imps scActive_wp getRefillNext_wp
               simp: o_def)
   done
 
@@ -2596,7 +2596,7 @@ lemma refillBudgetCheck_valid_mdb'[wp]:
 lemma handleOverrunLoop_list_refs_of_replies'[wp]:
   "handleOverrunLoop usage \<lbrace>\<lambda>s. sym_refs (list_refs_of_replies' s)\<rbrace>"
   apply (clarsimp simp: handleOverrunLoop_def)
-  apply (wpsimp wp: whileLoop_wp' hoare_drop_imps getRefillNext_wp
+  apply (wpsimp wp: whileLoop_valid_inv hoare_drop_imps getRefillNext_wp
                     getRefillSize_wp refillFull_wp refillEmpty_wp
               simp: o_def handleOverrunLoopBody_def refillPopHead_def updateSchedContext_def
                     scheduleUsed_def refillAddTail_def  updateRefillHd_def setRefillTl_def
@@ -2609,7 +2609,7 @@ lemma refillBudgetCheck_list_refs_of_replies'[wp]:
                         setReprogramTimer_def refillReady_def isRoundRobin_def
                         headInsufficientLoop_def nonOverlappingMergeRefills_def)
   apply (rule hoare_seq_ext_skip, solves wpsimp)+
-  apply (wpsimp wp: whileLoop_wp' hoare_drop_imps refillFull_wp refillEmpty_wp getRefillNext_wp
+  apply (wpsimp wp: whileLoop_valid_inv hoare_drop_imps refillFull_wp refillEmpty_wp getRefillNext_wp
                      getRefillSize_wp hoare_vcg_all_lift hoare_vcg_if_lift2
               simp: o_def scheduleUsed_def refillAddTail_def setRefillHd_def updateRefillHd_def
                     setRefillTl_def updateRefillTl_def updateSchedContext_def)
@@ -2633,7 +2633,7 @@ lemma refillBudgetCheck_valid_idle'[wp]:
 lemma handleOverrunLoop_valid_machine_state'[wp]:
   "handleOverrunLoop usage \<lbrace>valid_machine_state'\<rbrace>"
   apply (clarsimp simp: handleOverrunLoop_def)
-  apply (wpsimp wp: whileLoop_wp' hoare_drop_imps getRefillNext_wp
+  apply (wpsimp wp: whileLoop_valid_inv hoare_drop_imps getRefillNext_wp
                     getRefillSize_wp refillFull_wp refillEmpty_wp
               simp: handleOverrunLoopBody_def refillPopHead_def updateSchedContext_def
                     scheduleUsed_def refillAddTail_def  updateRefillHd_def setRefillTl_def
@@ -2646,7 +2646,7 @@ lemma refillBudgetCheck_valid_machine_state'[wp]:
                         setReprogramTimer_def refillReady_def isRoundRobin_def
                         headInsufficientLoop_def nonOverlappingMergeRefills_def)
   apply (rule hoare_seq_ext_skip, solves wpsimp)+
-  apply (wpsimp wp: whileLoop_wp' hoare_vcg_all_lift hoare_vcg_disj_lift scActive_wp hoare_drop_imps
+  apply (wpsimp wp: whileLoop_valid_inv hoare_vcg_all_lift hoare_vcg_disj_lift scActive_wp hoare_drop_imps
                     refillFull_wp refillEmpty_wp getRefillNext_wp  getRefillSize_wp
               simp: scheduleUsed_def refillAddTail_def setRefillTl_def updateRefillTl_def
                     setRefillHd_def updateRefillHd_def updateSchedContext_def)

proof/refine/RISCV64/IpcCancel_R.thy

@@ -3146,7 +3146,7 @@ lemma refillPopHead_valid_pspace'[wp]:
    refillPopHead scp
    \<lbrace>\<lambda>_. valid_pspace'\<rbrace>"
   unfolding refillPopHead_def updateSchedContext_def
-  apply (wpsimp wp: whileLoop_wp')
+  apply (wpsimp wp: whileLoop_valid_inv)
   by (fastforce simp: obj_at'_def  valid_obj'_def refillNextIndex_def MIN_REFILLS_def
                       valid_sched_context'_def valid_sched_context_size'_def scBits_simps objBits_simps
                dest!: opt_predD
@@ -3155,7 +3155,7 @@ lemma refillPopHead_valid_pspace'[wp]:
 lemma refillUnblockCheck_ko_wp_at_not_live[wp]:
   "refillUnblockCheck scp \<lbrace>\<lambda>s. P (ko_wp_at' (Not \<circ> live') p' s)\<rbrace>"
   unfolding refillUnblockCheck_def refillHeadOverlappingLoop_def mergeRefills_def
-  apply (wpsimp wp: whileLoop_wp' updateSchedContext_wp hoare_drop_imps
+  apply (wpsimp wp: whileLoop_valid_inv updateSchedContext_wp hoare_drop_imps
               simp: updateRefillHd_def refillPopHead_def)
         apply (clarsimp simp: ko_wp_at'_def obj_at'_def runReaderT_def
                               opt_map_red refillNextIndex_def
@@ -3181,7 +3181,7 @@ lemma refillUnblockCheck_refs_of'[wp]:
   "refillUnblockCheck sc_ptr \<lbrace>\<lambda>s. P (state_refs_of' s)\<rbrace>"
   unfolding refillUnblockCheck_def refillHeadOverlappingLoop_def mergeRefills_def
   apply (wpsimp simp: updateRefillHd_def refillPopHead_def
-                  wp: hoare_drop_imp whileLoop_wp' isRoundRobin_wp updateSchedContext_wp)
+                  wp: hoare_drop_imp whileLoop_valid_inv isRoundRobin_wp updateSchedContext_wp)
         apply (clarsimp simp: runReaderT_def elim!: rsubst[where P=P])
         apply (clarsimp simp: obj_at'_def  opt_map_red refillNextIndex_def)
         apply (fastforce simp: state_refs_of'_def get_refs_def2 ps_clear_upd objBits_simps option.case_eq_if