theory Ipc_C

lemma sendIPC_block_ccorres_helper:
  "ccorres dc xfdc (tcb_at' thread and valid_queues and valid_objs' and
                    sch_act_not thread and ep_at' epptr and
                    (\<lambda>s. sch_act_wf (ksSchedulerAction s) s \<and>
                         (\<forall>d p. thread \<notin> set (ksReadyQueues s (d, p)))) and
                    K (bos = ThreadState_BlockedOnSend
                      \<and> epptr' = epptr \<and> badge' = badge
                      \<and> cg = from_bool canGrant \<and> cgr = from_bool canGrantReply
                      \<and> dc' = from_bool do_call) and
                    K (epptr = epptr && ~~ mask 4) and
                    K (badge = badge && mask 28))
                   UNIV hs
           (setThreadState (Structures_H.thread_state.BlockedOnSend
                                epptr badge canGrant canGrantReply do_call) thread)
           (Guard C_Guard
             \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t tcb_ptr_to_ctcb_ptr thread\<rbrace>
             (CALL thread_state_ptr_set_tsType(Ptr
              &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C'']),
              scast bos));;
            Guard C_Guard
             \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t tcb_ptr_to_ctcb_ptr thread\<rbrace>
             (CALL thread_state_ptr_set_blockingObject(Ptr
                           &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C'']), epptr'));;
            Guard C_Guard
             \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t tcb_ptr_to_ctcb_ptr thread\<rbrace>
             (CALL thread_state_ptr_set_blockingIPCBadge(Ptr
                        &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C'']), badge'));;
            Guard C_Guard
             \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t tcb_ptr_to_ctcb_ptr thread\<rbrace>
             (CALL thread_state_ptr_set_blockingIPCCanGrant(Ptr
                           &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C'']), cg));;
            Guard C_Guard
             \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t tcb_ptr_to_ctcb_ptr thread\<rbrace>
             (CALL thread_state_ptr_set_blockingIPCCanGrantReply(Ptr
                           &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C'']), cgr));;
            Guard C_Guard
             \<lbrace>hrs_htd \<acute>t_hrs \<Turnstile>\<^sub>t tcb_ptr_to_ctcb_ptr thread\<rbrace>
             (CALL thread_state_ptr_set_blockingIPCIsCall(Ptr
                         &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C'']), dc'));;
            CALL scheduleTCB(tcb_ptr_to_ctcb_ptr thread))" unfolding K_def setThreadState_def apply (intro ccorres_gen_asm) apply (rule ccorres_guard_imp) apply (rule ccorres_split_nothrow_novcg) apply (rule_tac P=\<top> and P'="tcb_at' thread"
                     in threadSet_ccorres_lemma3) apply vcg apply clarsimp apply (frule(1) tcb_at_h_t_valid) apply (frule h_t_valid_c_guard) apply (clarsimp simp: typ_heap_simps'
                              rf_sr_tcb_update_twice) apply (erule(1) rf_sr_tcb_update_no_queue_gen,
          (simp add: typ_heap_simps')+)[1] apply (simp add: tcb_cte_cases_def) apply (simp add: ctcb_relation_def cthread_state_relation_def
                         ThreadState_BlockedOnSend_def mask_def) apply ceqv apply clarsimp apply ctac apply (wp threadSet_weak_sch_act_wf_runnable' threadSet_valid_queues
               threadSet_valid_objs') apply (clarsimp simp: guard_is_UNIV_def) apply (clarsimp simp: sch_act_wf_weak valid_tcb'_def valid_tcb_state'_def
                         tcb_cte_cases_def) apply clarsimp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres dc xfdc (tcb_at' thread and Invariants_H.valid_queues and valid_objs' and sch_act_not thread and ep_at' epptr and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s \<and> (\<forall>d p. thread \<notin> set (ksReadyQueues s (d, p)))) and K (bos = ThreadState_BlockedOnSend \<and> epptr' = epptr \<and> badge' = badge \<and> cg = from_bool canGrant \<and> cgr = from_bool canGrantReply \<and> dc' = from_bool do_call) and K (epptr = epptr && ~~ mask 4) and K (badge = badge && mask 28)) UNIV hs (setThreadState (Structures_H.thread_state.BlockedOnSend epptr badge canGrant canGrantReply do_call) thread) (Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread} (CALL thread_state_ptr_set_tsType_'proc(PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C'']),SCAST(32 signed \<rightarrow> 32) bos));;
Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread} (CALL thread_state_ptr_set_blockingObject_'proc(PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C'']),epptr'));;
Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread} (CALL thread_state_ptr_set_blockingIPCBadge_'proc(PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C'']),badge'));;
Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread} (CALL thread_state_ptr_set_blockingIPCCanGrant_'proc(PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C'']),cg));;
Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread} (CALL thread_state_ptr_set_blockingIPCCanGrantReply_'proc(PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C'']),cgr));;
Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread} (CALL thread_state_ptr_set_blockingIPCIsCall_'proc(PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C'']),dc'));;
CALL scheduleTCB_'proc(tcb_ptr_to_ctcb_ptr thread)) proof (prove)
goal (1 subgoal):
 1. ccorres dc xfdc (tcb_at' thread and Invariants_H.valid_queues and valid_objs' and sch_act_not thread and ep_at' epptr and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s \<and> (\<forall>d p. thread \<notin> set (ksReadyQueues s (d, p)))) and (\<lambda>y. bos = ThreadState_BlockedOnSend \<and> epptr' = epptr \<and> badge' = badge \<and> cg = from_bool canGrant \<and> cgr = from_bool canGrantReply \<and> dc' = from_bool do_call) and (\<lambda>y. epptr = epptr && ~~ mask 4) and (\<lambda>y. badge = badge && mask 28)) UNIV hs (do threadSet (tcbState_update (\<lambda>_. Structures_H.thread_state.BlockedOnSend epptr badge canGrant canGrantReply do_call)) thread;
runnable <- isRunnable thread;
curThread <- getCurThread;
action <- getSchedulerAction;
when (\<not> runnable \<and> curThread = thread \<and> action = ResumeCurrentThread) $ rescheduleRequired
od) (Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread} (CALL thread_state_ptr_set_tsType_'proc(PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C'']),SCAST(32 signed \<rightarrow> 32) bos));;
Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread} (CALL thread_state_ptr_set_blockingObject_'proc(PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C'']),epptr'));;
Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread} (CALL thread_state_ptr_set_blockingIPCBadge_'proc(PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C'']),badge'));;
Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread} (CALL thread_state_ptr_set_blockingIPCCanGrant_'proc(PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C'']),cg));;
Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread} (CALL thread_state_ptr_set_blockingIPCCanGrantReply_'proc(PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C'']),cgr));;
Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread} (CALL thread_state_ptr_set_blockingIPCIsCall_'proc(PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C'']),dc'));;
CALL scheduleTCB_'proc(tcb_ptr_to_ctcb_ptr thread)) proof (prove)
goal (1 subgoal):
 1. \<lbrakk>badge = badge && mask 28; epptr = epptr && ~~ mask 4; bos = ThreadState_BlockedOnSend \<and> epptr' = epptr \<and> badge' = badge \<and> cg = from_bool canGrant \<and> cgr = from_bool canGrantReply \<and> dc' = from_bool do_call\<rbrakk> \<Longrightarrow> ccorres dc xfdc (tcb_at' thread and Invariants_H.valid_queues and valid_objs' and sch_act_not thread and ep_at' epptr and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s \<and> (\<forall>d p. thread \<notin> set (ksReadyQueues s (d, p))))) UNIV hs (do threadSet (tcbState_update (\<lambda>_. Structures_H.thread_state.BlockedOnSend epptr badge canGrant canGrantReply do_call)) thread;
runnable <- isRunnable thread;
curThread <- getCurThread;
action <- getSchedulerAction;
when (\<not> runnable \<and> curThread = thread \<and> action = ResumeCurrentThread) $ rescheduleRequired
od) (Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread} (CALL thread_state_ptr_set_tsType_'proc(PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C'']),SCAST(32 signed \<rightarrow> 32) bos));;
Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread} (CALL thread_state_ptr_set_blockingObject_'proc(PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C'']),epptr'));;
Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread} (CALL thread_state_ptr_set_blockingIPCBadge_'proc(PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C'']),badge'));;
Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread} (CALL thread_state_ptr_set_blockingIPCCanGrant_'proc(PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C'']),cg));;
Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread} (CALL thread_state_ptr_set_blockingIPCCanGrantReply_'proc(PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C'']),cgr));;
Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread} (CALL thread_state_ptr_set_blockingIPCIsCall_'proc(PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C'']),dc'));;
CALL scheduleTCB_'proc(tcb_ptr_to_ctcb_ptr thread)) proof (prove)
goal (3 subgoals):
 1. \<lbrakk>badge = badge && mask 28; epptr = epptr && ~~ mask 4; bos = ThreadState_BlockedOnSend \<and> epptr' = epptr \<and> badge' = badge \<and> cg = from_bool canGrant \<and> cgr = from_bool canGrantReply \<and> dc' = from_bool do_call\<rbrakk> \<Longrightarrow> ccorres dc xfdc ?Q3 ?Q'3 hs (do threadSet (tcbState_update (\<lambda>_. Structures_H.thread_state.BlockedOnSend epptr badge canGrant canGrantReply do_call)) thread;
runnable <- isRunnable thread;
curThread <- getCurThread;
action <- getSchedulerAction;
when (\<not> runnable \<and> curThread = thread \<and> action = ResumeCurrentThread) $ rescheduleRequired
od) (Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread} (CALL thread_state_ptr_set_tsType_'proc(PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C'']),SCAST(32 signed \<rightarrow> 32) bos));;
Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread} (CALL thread_state_ptr_set_blockingObject_'proc(PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C'']),epptr'));;
Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread} (CALL thread_state_ptr_set_blockingIPCBadge_'proc(PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C'']),badge'));;
Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread} (CALL thread_state_ptr_set_blockingIPCCanGrant_'proc(PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C'']),cg));;
Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread} (CALL thread_state_ptr_set_blockingIPCCanGrantReply_'proc(PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C'']),cgr));;
Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread} (CALL thread_state_ptr_set_blockingIPCIsCall_'proc(PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C'']),dc'));;
CALL scheduleTCB_'proc(tcb_ptr_to_ctcb_ptr thread))
 2. \<And>s. \<lbrakk>badge = badge && mask 28; epptr = epptr && ~~ mask 4; bos = ThreadState_BlockedOnSend \<and> epptr' = epptr \<and> badge' = badge \<and> cg = from_bool canGrant \<and> cgr = from_bool canGrantReply \<and> dc' = from_bool do_call; (tcb_at' thread and Invariants_H.valid_queues and valid_objs' and sch_act_not thread and ep_at' epptr and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s \<and> (\<forall>d p. thread \<notin> set (ksReadyQueues s (d, p))))) s\<rbrakk> \<Longrightarrow> ?Q3 s
 3. \<And>s. \<lbrakk>badge = badge && mask 28; epptr = epptr && ~~ mask 4; bos = ThreadState_BlockedOnSend \<and> epptr' = epptr \<and> badge' = badge \<and> cg = from_bool canGrant \<and> cgr = from_bool canGrantReply \<and> dc' = from_bool do_call; s \<in> UNIV\<rbrakk> \<Longrightarrow> s \<in> ?Q'3 proof (prove)
goal (7 subgoals):
 1. \<lbrakk>badge = badge && mask 28; epptr = epptr && ~~ mask 4; bos = ThreadState_BlockedOnSend \<and> epptr' = epptr \<and> badge' = badge \<and> cg = from_bool canGrant \<and> cgr = from_bool canGrantReply \<and> dc' = from_bool do_call\<rbrakk> \<Longrightarrow> ccorres ?r'7 ?xf'7 ?P7 ?Q'3 [] (threadSet (tcbState_update (\<lambda>_. Structures_H.thread_state.BlockedOnSend epptr badge canGrant canGrantReply do_call)) thread) (Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread} (CALL thread_state_ptr_set_tsType_'proc(PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C'']),SCAST(32 signed \<rightarrow> 32) bos));;
Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread} (CALL thread_state_ptr_set_blockingObject_'proc(PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C'']),epptr'));;
Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread} (CALL thread_state_ptr_set_blockingIPCBadge_'proc(PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C'']),badge'));;
Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread} (CALL thread_state_ptr_set_blockingIPCCanGrant_'proc(PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C'']),cg));;
Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread} (CALL thread_state_ptr_set_blockingIPCCanGrantReply_'proc(PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C'']),cgr));;
Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread} (CALL thread_state_ptr_set_blockingIPCIsCall_'proc(PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C'']),dc')))
 2. \<And>rv' t t'. \<lbrakk>badge = badge && mask 28; epptr = epptr && ~~ mask 4; bos = ThreadState_BlockedOnSend \<and> epptr' = epptr \<and> badge' = badge \<and> cg = from_bool canGrant \<and> cgr = from_bool canGrantReply \<and> dc' = from_bool do_call\<rbrakk> \<Longrightarrow> ceqv \<Gamma> ?xf'7 rv' t t' (CALL scheduleTCB_'proc(tcb_ptr_to_ctcb_ptr thread)) (?d'7 rv')
 3. \<And>rv rv'. \<lbrakk>badge = badge && mask 28; epptr = epptr && ~~ mask 4; bos = ThreadState_BlockedOnSend \<and> epptr' = epptr \<and> badge' = badge \<and> cg = from_bool canGrant \<and> cgr = from_bool canGrantReply \<and> dc' = from_bool do_call; ?r'7 rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q7 rv) (?Q'7 rv rv') hs (K_bind (do runnable <- isRunnable thread;
curThread <- getCurThread;
action <- getSchedulerAction;
when (\<not> runnable \<and> curThread = thread \<and> action = ResumeCurrentThread) $ rescheduleRequired
od) rv) (?d'7 rv')
 4. \<lbrakk>badge = badge && mask 28; epptr = epptr && ~~ mask 4; bos = ThreadState_BlockedOnSend \<and> epptr' = epptr \<and> badge' = badge \<and> cg = from_bool canGrant \<and> cgr = from_bool canGrantReply \<and> dc' = from_bool do_call\<rbrakk> \<Longrightarrow> \<lbrace>?R7\<rbrace> threadSet (tcbState_update (\<lambda>_. Structures_H.thread_state.BlockedOnSend epptr badge canGrant canGrantReply do_call)) thread \<lbrace>?Q7\<rbrace>
 5. \<lbrakk>badge = badge && mask 28; epptr = epptr && ~~ mask 4; bos = ThreadState_BlockedOnSend \<and> epptr' = epptr \<and> badge' = badge \<and> cg = from_bool canGrant \<and> cgr = from_bool canGrantReply \<and> dc' = from_bool do_call\<rbrakk> \<Longrightarrow> guard_is_UNIV ?r'7 ?xf'7 ?Q'7
 6. \<And>s. \<lbrakk>badge = badge && mask 28; epptr = epptr && ~~ mask 4; bos = ThreadState_BlockedOnSend \<and> epptr' = epptr \<and> badge' = badge \<and> cg = from_bool canGrant \<and> cgr = from_bool canGrantReply \<and> dc' = from_bool do_call; (tcb_at' thread and Invariants_H.valid_queues and valid_objs' and sch_act_not thread and ep_at' epptr and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s \<and> (\<forall>d p. thread \<notin> set (ksReadyQueues s (d, p))))) s\<rbrakk> \<Longrightarrow> (?P7 and ?R7) s
 7. \<And>s. \<lbrakk>badge = badge && mask 28; epptr = epptr && ~~ mask 4; bos = ThreadState_BlockedOnSend \<and> epptr' = epptr \<and> badge' = badge \<and> cg = from_bool canGrant \<and> cgr = from_bool canGrantReply \<and> dc' = from_bool do_call; s \<in> UNIV\<rbrakk> \<Longrightarrow> s \<in> ?Q'3 proof (prove)
goal (8 subgoals):
 1. \<And>s tcb. \<lbrakk>badge = badge && mask 28; epptr = epptr && ~~ mask 4; bos = ThreadState_BlockedOnSend \<and> epptr' = epptr \<and> badge' = badge \<and> cg = from_bool canGrant \<and> cgr = from_bool canGrantReply \<and> dc' = from_bool do_call\<rbrakk> \<Longrightarrow> \<Gamma>\<turnstile> (?Q13 s tcb) Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread} (CALL thread_state_ptr_set_tsType_'proc(PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C'']),SCAST(32 signed \<rightarrow> 32) bos));;
Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread} (CALL thread_state_ptr_set_blockingObject_'proc(PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C'']),epptr'));;
Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread} (CALL thread_state_ptr_set_blockingIPCBadge_'proc(PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C'']),badge'));;
Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread} (CALL thread_state_ptr_set_blockingIPCCanGrant_'proc(PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C'']),cg));;
Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread} (CALL thread_state_ptr_set_blockingIPCCanGrantReply_'proc(PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C'']),cgr));;
Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread} (CALL thread_state_ptr_set_blockingIPCIsCall_'proc(PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C'']),dc')) {s'. (s\<lparr>ksPSpace := (ksPSpace s)(thread \<mapsto> injectKOS (tcbState_update (\<lambda>_. Structures_H.thread_state.BlockedOnSend epptr badge canGrant canGrantReply do_call) tcb))\<rparr>, s') \<in> rf_sr}
 2. \<And>s s' tcb tcb'. \<lbrakk>badge = badge && mask 28; epptr = epptr && ~~ mask 4; bos = ThreadState_BlockedOnSend \<and> epptr' = epptr \<and> badge' = badge \<and> cg = from_bool canGrant \<and> cgr = from_bool canGrantReply \<and> dc' = from_bool do_call; (s, s') \<in> rf_sr; True; ko_at' tcb thread s; cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb'; ctcb_relation tcb tcb'; tcb_at' thread s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> s' \<in> ?Q13 s tcb
 3. \<And>rv' t t'. \<lbrakk>badge = badge && mask 28; epptr = epptr && ~~ mask 4; bos = ThreadState_BlockedOnSend \<and> epptr' = epptr \<and> badge' = badge \<and> cg = from_bool canGrant \<and> cgr = from_bool canGrantReply \<and> dc' = from_bool do_call\<rbrakk> \<Longrightarrow> ceqv \<Gamma> xfdc rv' t t' (CALL scheduleTCB_'proc(tcb_ptr_to_ctcb_ptr thread)) (?d'7 rv')
 4. \<And>rv rv'. \<lbrakk>badge = badge && mask 28; epptr = epptr && ~~ mask 4; bos = ThreadState_BlockedOnSend \<and> epptr' = epptr \<and> badge' = badge \<and> cg = from_bool canGrant \<and> cgr = from_bool canGrantReply \<and> dc' = from_bool do_call; dc rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q7 rv) (?Q'7 rv rv') hs (K_bind (do runnable <- isRunnable thread;
curThread <- getCurThread;
action <- getSchedulerAction;
when (\<not> runnable \<and> curThread = thread \<and> action = ResumeCurrentThread) $ rescheduleRequired
od) rv) (?d'7 rv')
 5. \<lbrakk>badge = badge && mask 28; epptr = epptr && ~~ mask 4; bos = ThreadState_BlockedOnSend \<and> epptr' = epptr \<and> badge' = badge \<and> cg = from_bool canGrant \<and> cgr = from_bool canGrantReply \<and> dc' = from_bool do_call\<rbrakk> \<Longrightarrow> \<lbrace>?R7\<rbrace> threadSet (tcbState_update (\<lambda>_. Structures_H.thread_state.BlockedOnSend epptr badge canGrant canGrantReply do_call)) thread \<lbrace>?Q7\<rbrace>
 6. \<lbrakk>badge = badge && mask 28; epptr = epptr && ~~ mask 4; bos = ThreadState_BlockedOnSend \<and> epptr' = epptr \<and> badge' = badge \<and> cg = from_bool canGrant \<and> cgr = from_bool canGrantReply \<and> dc' = from_bool do_call\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc ?Q'7
 7. \<And>s. \<lbrakk>badge = badge && mask 28; epptr = epptr && ~~ mask 4; bos = ThreadState_BlockedOnSend \<and> epptr' = epptr \<and> badge' = badge \<and> cg = from_bool canGrant \<and> cgr = from_bool canGrantReply \<and> dc' = from_bool do_call; (tcb_at' thread and Invariants_H.valid_queues and valid_objs' and sch_act_not thread and ep_at' epptr and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s \<and> (\<forall>d p. thread \<notin> set (ksReadyQueues s (d, p))))) s\<rbrakk> \<Longrightarrow> (tcb_at' thread and tcb_at' thread and ?R7) s
 8. \<And>s. \<lbrakk>badge = badge && mask 28; epptr = epptr && ~~ mask 4; bos = ThreadState_BlockedOnSend \<and> epptr' = epptr \<and> badge' = badge \<and> cg = from_bool canGrant \<and> cgr = from_bool canGrantReply \<and> dc' = from_bool do_call; s \<in> UNIV\<rbrakk> \<Longrightarrow> s \<in> UNIV proof (prove)
goal (7 subgoals):
 1. \<And>s s' tcb tcb'. \<lbrakk>badge = badge && mask 28; epptr = epptr && ~~ mask 4; bos = ThreadState_BlockedOnSend \<and> epptr' = epptr \<and> badge' = badge \<and> cg = from_bool canGrant \<and> cgr = from_bool canGrantReply \<and> dc' = from_bool do_call; (s, s') \<in> rf_sr; True; ko_at' tcb thread s; cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb'; ctcb_relation tcb tcb'; tcb_at' thread s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> s' \<in> {sa. sa \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread \<and> sa \<Turnstile>\<^sub>c cparent (PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C''])) [''tcbState_C''] \<and> (\<forall>t. (\<exists>thread_state. thread_state_lift thread_state = thread_state_lift (tcbState_C (the (cslift sa (cparent (PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C''])) [''tcbState_C'']))))\<lparr>tsType_CL := SCAST(32 signed \<rightarrow> 32) bos && mask 4\<rparr> \<and> t_hrs_' (globals t) = hrs_mem_update (heap_update (cparent (PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C''])) [''tcbState_C'']) (tcbState_C_update (\<lambda>_. thread_state) (the (cslift sa (cparent (PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C''])) [''tcbState_C'']))))) (t_hrs_' (globals sa))) \<longrightarrow> t \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread \<and> t \<Turnstile>\<^sub>c cparent (PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C''])) [''tcbState_C''] \<and> (\<forall>ta. (\<exists>thread_state. thread_state_lift thread_state = thread_state_lift (tcbState_C (the (cslift t (cparent (PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C''])) [''tcbState_C'']))))\<lparr>blockingObject_CL := epptr' && ~~ mask 4\<rparr> \<and> t_hrs_' (globals ta) = hrs_mem_update (heap_update (cparent (PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C''])) [''tcbState_C'']) (tcbState_C_update (\<lambda>_. thread_state) (the (cslift t (cparent (PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C''])) [''tcbState_C'']))))) (t_hrs_' (globals t))) \<longrightarrow> ta \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread \<and> ta \<Turnstile>\<^sub>c cparent (PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C''])) [''tcbState_C''] \<and> (\<forall>t. (\<exists>thread_state. thread_state_lift thread_state = thread_state_lift (tcbState_C (the (cslift ta (cparent (PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C''])) [''tcbState_C'']))))\<lparr>blockingIPCBadge_CL := badge' && mask 28\<rparr> \<and> t_hrs_' (globals t) = hrs_mem_update (heap_update (cparent (PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C''])) [''tcbState_C'']) (tcbState_C_update (\<lambda>_. thread_state) (the (cslift ta (cparent (PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C''])) [''tcbState_C'']))))) (t_hrs_' (globals ta))) \<longrightarrow> t \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread \<and> t \<Turnstile>\<^sub>c cparent (PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C''])) [''tcbState_C''] \<and> (\<forall>ta. (\<exists>thread_state. thread_state_lift thread_state = thread_state_lift (tcbState_C (the (cslift t (cparent (PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C''])) [''tcbState_C'']))))\<lparr>blockingIPCCanGrant_CL := cg && mask 1\<rparr> \<and> t_hrs_' (globals ta) = hrs_mem_update (heap_update (cparent (PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C''])) [''tcbState_C'']) (tcbState_C_update (\<lambda>_. thread_state) (the (cslift t (cparent (PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C''])) [''tcbState_C'']))))) (t_hrs_' (globals t))) \<longrightarrow> ta \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread \<and> ta \<Turnstile>\<^sub>c cparent (PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C''])) [''tcbState_C''] \<and> (\<forall>t. (\<exists>thread_state. thread_state_lift thread_state = thread_state_lift (tcbState_C (the (cslift ta (cparent (PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C''])) [''tcbState_C'']))))\<lparr>blockingIPCCanGrantReply_CL := cgr && mask 1\<rparr> \<and> t_hrs_' (globals t) = hrs_mem_update (heap_update (cparent (PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C''])) [''tcbState_C'']) (tcbState_C_update (\<lambda>_. thread_state) (the (cslift ta (cparent (PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C''])) [''tcbState_C'']))))) (t_hrs_' (globals ta))) \<longrightarrow> t \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread \<and> t \<Turnstile>\<^sub>c cparent (PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C''])) [''tcbState_C''] \<and> (\<forall>ta. (\<exists>thread_state. thread_state_lift thread_state = thread_state_lift (tcbState_C (the (cslift t (cparent (PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C''])) [''tcbState_C'']))))\<lparr>blockingIPCIsCall_CL := dc' && mask 1\<rparr> \<and> t_hrs_' (globals ta) = hrs_mem_update (heap_update (cparent (PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C''])) [''tcbState_C'']) (tcbState_C_update (\<lambda>_. thread_state) (the (cslift t (cparent (PTR(thread_state_C) &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C''])) [''tcbState_C'']))))) (t_hrs_' (globals t))) \<longrightarrow> (s\<lparr>ksPSpace := (ksPSpace s)(thread \<mapsto> injectKOS (tcbState_update (\<lambda>_. Structures_H.thread_state.BlockedOnSend epptr badge canGrant canGrantReply do_call) tcb))\<rparr>, sa\<lparr>globals := globals sa\<lparr>t_hrs_' := t_hrs_' (globals ta)\<rparr>\<rparr>) \<in> rf_sr))))))}
 2. \<And>rv' t t'. \<lbrakk>badge = badge && mask 28; epptr = epptr && ~~ mask 4; bos = ThreadState_BlockedOnSend \<and> epptr' = epptr \<and> badge' = badge \<and> cg = from_bool canGrant \<and> cgr = from_bool canGrantReply \<and> dc' = from_bool do_call\<rbrakk> \<Longrightarrow> ceqv \<Gamma> xfdc rv' t t' (CALL scheduleTCB_'proc(tcb_ptr_to_ctcb_ptr thread)) (?d'7 rv')
 3. \<And>rv rv'. \<lbrakk>badge = badge && mask 28; epptr = epptr && ~~ mask 4; bos = ThreadState_BlockedOnSend \<and> epptr' = epptr \<and> badge' = badge \<and> cg = from_bool canGrant \<and> cgr = from_bool canGrantReply \<and> dc' = from_bool do_call; dc rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q7 rv) (?Q'7 rv rv') hs (K_bind (do runnable <- isRunnable thread;
curThread <- getCurThread;
action <- getSchedulerAction;
when (\<not> runnable \<and> curThread = thread \<and> action = ResumeCurrentThread) $ rescheduleRequired
od) rv) (?d'7 rv')
 4. \<lbrakk>badge = badge && mask 28; epptr = epptr && ~~ mask 4; bos = ThreadState_BlockedOnSend \<and> epptr' = epptr \<and> badge' = badge \<and> cg = from_bool canGrant \<and> cgr = from_bool canGrantReply \<and> dc' = from_bool do_call\<rbrakk> \<Longrightarrow> \<lbrace>?R7\<rbrace> threadSet (tcbState_update (\<lambda>_. Structures_H.thread_state.BlockedOnSend epptr badge canGrant canGrantReply do_call)) thread \<lbrace>?Q7\<rbrace>
 5. \<lbrakk>badge = badge && mask 28; epptr = epptr && ~~ mask 4; bos = ThreadState_BlockedOnSend \<and> epptr' = epptr \<and> badge' = badge \<and> cg = from_bool canGrant \<and> cgr = from_bool canGrantReply \<and> dc' = from_bool do_call\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc ?Q'7
 6. \<And>s. \<lbrakk>badge = badge && mask 28; epptr = epptr && ~~ mask 4; bos = ThreadState_BlockedOnSend \<and> epptr' = epptr \<and> badge' = badge \<and> cg = from_bool canGrant \<and> cgr = from_bool canGrantReply \<and> dc' = from_bool do_call; (tcb_at' thread and Invariants_H.valid_queues and valid_objs' and sch_act_not thread and ep_at' epptr and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s \<and> (\<forall>d p. thread \<notin> set (ksReadyQueues s (d, p))))) s\<rbrakk> \<Longrightarrow> (tcb_at' thread and tcb_at' thread and ?R7) s
 7. \<And>s. \<lbrakk>badge = badge && mask 28; epptr = epptr && ~~ mask 4; bos = ThreadState_BlockedOnSend \<and> epptr' = epptr \<and> badge' = badge \<and> cg = from_bool canGrant \<and> cgr = from_bool canGrantReply \<and> dc' = from_bool do_call; s \<in> UNIV\<rbrakk> \<Longrightarrow> s \<in> UNIV proof (prove)
goal (7 subgoals):
 1. \<And>s s' tcb tcb'. \<lbrakk>badge = badge && mask 28; epptr = epptr && ~~ mask 4; (s, s') \<in> rf_sr; ko_at' tcb thread s; cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb'; ctcb_relation tcb tcb'; tcb_at' thread s; bos = ThreadState_BlockedOnSend; epptr' = epptr; badge' = badge; cg = from_bool canGrant; cgr = from_bool canGrantReply; dc' = from_bool do_call\<rbrakk> \<Longrightarrow> s' \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread \<and> (\<forall>t. (\<exists>thread_state. thread_state_lift thread_state = thread_state_lift (tcbState_C tcb')\<lparr>tsType_CL := SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnSend && mask 4\<rparr> \<and> t_hrs_' (globals t) = hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_state) tcb')) (t_hrs_' (globals s'))) \<longrightarrow> t \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread \<and> (\<forall>ta. (\<exists>thread_state. thread_state_lift thread_state = thread_state_lift (tcbState_C (the (cslift t (tcb_ptr_to_ctcb_ptr thread))))\<lparr>blockingObject_CL := epptr\<rparr> \<and> t_hrs_' (globals ta) = hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_state) (the (cslift t (tcb_ptr_to_ctcb_ptr thread))))) (t_hrs_' (globals t))) \<longrightarrow> ta \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread \<and> (\<forall>t. (\<exists>thread_state. thread_state_lift thread_state = thread_state_lift (tcbState_C (the (cslift ta (tcb_ptr_to_ctcb_ptr thread))))\<lparr>blockingIPCBadge_CL := badge\<rparr> \<and> t_hrs_' (globals t) = hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_state) (the (cslift ta (tcb_ptr_to_ctcb_ptr thread))))) (t_hrs_' (globals ta))) \<longrightarrow> t \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread \<and> (\<forall>ta. (\<exists>thread_state. thread_state_lift thread_state = thread_state_lift (tcbState_C (the (cslift t (tcb_ptr_to_ctcb_ptr thread))))\<lparr>blockingIPCCanGrant_CL := from_bool canGrant\<rparr> \<and> t_hrs_' (globals ta) = hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_state) (the (cslift t (tcb_ptr_to_ctcb_ptr thread))))) (t_hrs_' (globals t))) \<longrightarrow> ta \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread \<and> (\<forall>t. (\<exists>thread_state. thread_state_lift thread_state = thread_state_lift (tcbState_C (the (cslift ta (tcb_ptr_to_ctcb_ptr thread))))\<lparr>blockingIPCCanGrantReply_CL := from_bool canGrantReply\<rparr> \<and> t_hrs_' (globals t) = hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_state) (the (cslift ta (tcb_ptr_to_ctcb_ptr thread))))) (t_hrs_' (globals ta))) \<longrightarrow> t \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread \<and> (\<forall>ta. (\<exists>thread_state. thread_state_lift thread_state = thread_state_lift (tcbState_C (the (cslift t (tcb_ptr_to_ctcb_ptr thread))))\<lparr>blockingIPCIsCall_CL := from_bool do_call\<rparr> \<and> t_hrs_' (globals ta) = hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_state) (the (cslift t (tcb_ptr_to_ctcb_ptr thread))))) (t_hrs_' (globals t))) \<longrightarrow> (s\<lparr>ksPSpace := (ksPSpace s)(thread \<mapsto> KOTCB (tcbState_update (\<lambda>_. Structures_H.thread_state.BlockedOnSend epptr badge canGrant canGrantReply do_call) tcb))\<rparr>, s'\<lparr>globals := globals s'\<lparr>t_hrs_' := t_hrs_' (globals ta)\<rparr>\<rparr>) \<in> rf_sr))))))
 2. \<And>rv' t t'. \<lbrakk>badge = badge && mask 28; epptr = epptr && ~~ mask 4; bos = ThreadState_BlockedOnSend \<and> epptr' = epptr \<and> badge' = badge \<and> cg = from_bool canGrant \<and> cgr = from_bool canGrantReply \<and> dc' = from_bool do_call\<rbrakk> \<Longrightarrow> ceqv \<Gamma> xfdc rv' t t' (CALL scheduleTCB_'proc(tcb_ptr_to_ctcb_ptr thread)) (?d'7 rv')
 3. \<And>rv rv'. \<lbrakk>badge = badge && mask 28; epptr = epptr && ~~ mask 4; bos = ThreadState_BlockedOnSend \<and> epptr' = epptr \<and> badge' = badge \<and> cg = from_bool canGrant \<and> cgr = from_bool canGrantReply \<and> dc' = from_bool do_call; dc rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q7 rv) (?Q'7 rv rv') hs (K_bind (do runnable <- isRunnable thread;
curThread <- getCurThread;
action <- getSchedulerAction;
when (\<not> runnable \<and> curThread = thread \<and> action = ResumeCurrentThread) $ rescheduleRequired
od) rv) (?d'7 rv')
 4. \<lbrakk>badge = badge && mask 28; epptr = epptr && ~~ mask 4; bos = ThreadState_BlockedOnSend \<and> epptr' = epptr \<and> badge' = badge \<and> cg = from_bool canGrant \<and> cgr = from_bool canGrantReply \<and> dc' = from_bool do_call\<rbrakk> \<Longrightarrow> \<lbrace>?R7\<rbrace> threadSet (tcbState_update (\<lambda>_. Structures_H.thread_state.BlockedOnSend epptr badge canGrant canGrantReply do_call)) thread \<lbrace>?Q7\<rbrace>
 5. \<lbrakk>badge = badge && mask 28; epptr = epptr && ~~ mask 4; bos = ThreadState_BlockedOnSend \<and> epptr' = epptr \<and> badge' = badge \<and> cg = from_bool canGrant \<and> cgr = from_bool canGrantReply \<and> dc' = from_bool do_call\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc ?Q'7
 6. \<And>s. \<lbrakk>badge = badge && mask 28; epptr = epptr && ~~ mask 4; bos = ThreadState_BlockedOnSend \<and> epptr' = epptr \<and> badge' = badge \<and> cg = from_bool canGrant \<and> cgr = from_bool canGrantReply \<and> dc' = from_bool do_call; (tcb_at' thread and Invariants_H.valid_queues and valid_objs' and sch_act_not thread and ep_at' epptr and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s \<and> (\<forall>d p. thread \<notin> set (ksReadyQueues s (d, p))))) s\<rbrakk> \<Longrightarrow> (tcb_at' thread and tcb_at' thread and ?R7) s
 7. \<And>s. \<lbrakk>badge = badge && mask 28; epptr = epptr && ~~ mask 4; bos = ThreadState_BlockedOnSend \<and> epptr' = epptr \<and> badge' = badge \<and> cg = from_bool canGrant \<and> cgr = from_bool canGrantReply \<and> dc' = from_bool do_call; s \<in> UNIV\<rbrakk> \<Longrightarrow> s \<in> UNIV proof (prove)
goal (7 subgoals):
 1. \<And>s s' tcb tcb'. \<lbrakk>badge = badge && mask 28; epptr = epptr && ~~ mask 4; (s, s') \<in> rf_sr; ko_at' tcb thread s; cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb'; ctcb_relation tcb tcb'; tcb_at' thread s; bos = ThreadState_BlockedOnSend; epptr' = epptr; badge' = badge; cg = from_bool canGrant; cgr = from_bool canGrantReply; dc' = from_bool do_call; s' \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread\<rbrakk> \<Longrightarrow> s' \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread \<and> (\<forall>t. (\<exists>thread_state. thread_state_lift thread_state = thread_state_lift (tcbState_C tcb')\<lparr>tsType_CL := SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnSend && mask 4\<rparr> \<and> t_hrs_' (globals t) = hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_state) tcb')) (t_hrs_' (globals s'))) \<longrightarrow> t \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread \<and> (\<forall>ta. (\<exists>thread_state. thread_state_lift thread_state = thread_state_lift (tcbState_C (the (cslift t (tcb_ptr_to_ctcb_ptr thread))))\<lparr>blockingObject_CL := epptr\<rparr> \<and> t_hrs_' (globals ta) = hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_state) (the (cslift t (tcb_ptr_to_ctcb_ptr thread))))) (t_hrs_' (globals t))) \<longrightarrow> ta \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread \<and> (\<forall>t. (\<exists>thread_state. thread_state_lift thread_state = thread_state_lift (tcbState_C (the (cslift ta (tcb_ptr_to_ctcb_ptr thread))))\<lparr>blockingIPCBadge_CL := badge\<rparr> \<and> t_hrs_' (globals t) = hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_state) (the (cslift ta (tcb_ptr_to_ctcb_ptr thread))))) (t_hrs_' (globals ta))) \<longrightarrow> t \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread \<and> (\<forall>ta. (\<exists>thread_state. thread_state_lift thread_state = thread_state_lift (tcbState_C (the (cslift t (tcb_ptr_to_ctcb_ptr thread))))\<lparr>blockingIPCCanGrant_CL := from_bool canGrant\<rparr> \<and> t_hrs_' (globals ta) = hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_state) (the (cslift t (tcb_ptr_to_ctcb_ptr thread))))) (t_hrs_' (globals t))) \<longrightarrow> ta \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread \<and> (\<forall>t. (\<exists>thread_state. thread_state_lift thread_state = thread_state_lift (tcbState_C (the (cslift ta (tcb_ptr_to_ctcb_ptr thread))))\<lparr>blockingIPCCanGrantReply_CL := from_bool canGrantReply\<rparr> \<and> t_hrs_' (globals t) = hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_state) (the (cslift ta (tcb_ptr_to_ctcb_ptr thread))))) (t_hrs_' (globals ta))) \<longrightarrow> t \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread \<and> (\<forall>ta. (\<exists>thread_state. thread_state_lift thread_state = thread_state_lift (tcbState_C (the (cslift t (tcb_ptr_to_ctcb_ptr thread))))\<lparr>blockingIPCIsCall_CL := from_bool do_call\<rparr> \<and> t_hrs_' (globals ta) = hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_state) (the (cslift t (tcb_ptr_to_ctcb_ptr thread))))) (t_hrs_' (globals t))) \<longrightarrow> (s\<lparr>ksPSpace := (ksPSpace s)(thread \<mapsto> KOTCB (tcbState_update (\<lambda>_. Structures_H.thread_state.BlockedOnSend epptr badge canGrant canGrantReply do_call) tcb))\<rparr>, s'\<lparr>globals := globals s'\<lparr>t_hrs_' := t_hrs_' (globals ta)\<rparr>\<rparr>) \<in> rf_sr))))))
 2. \<And>rv' t t'. \<lbrakk>badge = badge && mask 28; epptr = epptr && ~~ mask 4; bos = ThreadState_BlockedOnSend \<and> epptr' = epptr \<and> badge' = badge \<and> cg = from_bool canGrant \<and> cgr = from_bool canGrantReply \<and> dc' = from_bool do_call\<rbrakk> \<Longrightarrow> ceqv \<Gamma> xfdc rv' t t' (CALL scheduleTCB_'proc(tcb_ptr_to_ctcb_ptr thread)) (?d'7 rv')
 3. \<And>rv rv'. \<lbrakk>badge = badge && mask 28; epptr = epptr && ~~ mask 4; bos = ThreadState_BlockedOnSend \<and> epptr' = epptr \<and> badge' = badge \<and> cg = from_bool canGrant \<and> cgr = from_bool canGrantReply \<and> dc' = from_bool do_call; dc rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q7 rv) (?Q'7 rv rv') hs (K_bind (do runnable <- isRunnable thread;
curThread <- getCurThread;
action <- getSchedulerAction;
when (\<not> runnable \<and> curThread = thread \<and> action = ResumeCurrentThread) $ rescheduleRequired
od) rv) (?d'7 rv')
 4. \<lbrakk>badge = badge && mask 28; epptr = epptr && ~~ mask 4; bos = ThreadState_BlockedOnSend \<and> epptr' = epptr \<and> badge' = badge \<and> cg = from_bool canGrant \<and> cgr = from_bool canGrantReply \<and> dc' = from_bool do_call\<rbrakk> \<Longrightarrow> \<lbrace>?R7\<rbrace> threadSet (tcbState_update (\<lambda>_. Structures_H.thread_state.BlockedOnSend epptr badge canGrant canGrantReply do_call)) thread \<lbrace>?Q7\<rbrace>
 5. \<lbrakk>badge = badge && mask 28; epptr = epptr && ~~ mask 4; bos = ThreadState_BlockedOnSend \<and> epptr' = epptr \<and> badge' = badge \<and> cg = from_bool canGrant \<and> cgr = from_bool canGrantReply \<and> dc' = from_bool do_call\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc ?Q'7
 6. \<And>s. \<lbrakk>badge = badge && mask 28; epptr = epptr && ~~ mask 4; bos = ThreadState_BlockedOnSend \<and> epptr' = epptr \<and> badge' = badge \<and> cg = from_bool canGrant \<and> cgr = from_bool canGrantReply \<and> dc' = from_bool do_call; (tcb_at' thread and Invariants_H.valid_queues and valid_objs' and sch_act_not thread and ep_at' epptr and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s \<and> (\<forall>d p. thread \<notin> set (ksReadyQueues s (d, p))))) s\<rbrakk> \<Longrightarrow> (tcb_at' thread and tcb_at' thread and ?R7) s
 7. \<And>s. \<lbrakk>badge = badge && mask 28; epptr = epptr && ~~ mask 4; bos = ThreadState_BlockedOnSend \<and> epptr' = epptr \<and> badge' = badge \<and> cg = from_bool canGrant \<and> cgr = from_bool canGrantReply \<and> dc' = from_bool do_call; s \<in> UNIV\<rbrakk> \<Longrightarrow> s \<in> UNIV proof (prove)
goal (7 subgoals):
 1. \<And>s s' tcb tcb'. \<lbrakk>badge = badge && mask 28; epptr = epptr && ~~ mask 4; (s, s') \<in> rf_sr; ko_at' tcb thread s; cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb'; ctcb_relation tcb tcb'; tcb_at' thread s; bos = ThreadState_BlockedOnSend; epptr' = epptr; badge' = badge; cg = from_bool canGrant; cgr = from_bool canGrantReply; dc' = from_bool do_call; s' \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread; c_guard (tcb_ptr_to_ctcb_ptr thread)\<rbrakk> \<Longrightarrow> s' \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread \<and> (\<forall>t. (\<exists>thread_state. thread_state_lift thread_state = thread_state_lift (tcbState_C tcb')\<lparr>tsType_CL := SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnSend && mask 4\<rparr> \<and> t_hrs_' (globals t) = hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_state) tcb')) (t_hrs_' (globals s'))) \<longrightarrow> t \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread \<and> (\<forall>ta. (\<exists>thread_state. thread_state_lift thread_state = thread_state_lift (tcbState_C (the (cslift t (tcb_ptr_to_ctcb_ptr thread))))\<lparr>blockingObject_CL := epptr\<rparr> \<and> t_hrs_' (globals ta) = hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_state) (the (cslift t (tcb_ptr_to_ctcb_ptr thread))))) (t_hrs_' (globals t))) \<longrightarrow> ta \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread \<and> (\<forall>t. (\<exists>thread_state. thread_state_lift thread_state = thread_state_lift (tcbState_C (the (cslift ta (tcb_ptr_to_ctcb_ptr thread))))\<lparr>blockingIPCBadge_CL := badge\<rparr> \<and> t_hrs_' (globals t) = hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_state) (the (cslift ta (tcb_ptr_to_ctcb_ptr thread))))) (t_hrs_' (globals ta))) \<longrightarrow> t \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread \<and> (\<forall>ta. (\<exists>thread_state. thread_state_lift thread_state = thread_state_lift (tcbState_C (the (cslift t (tcb_ptr_to_ctcb_ptr thread))))\<lparr>blockingIPCCanGrant_CL := from_bool canGrant\<rparr> \<and> t_hrs_' (globals ta) = hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_state) (the (cslift t (tcb_ptr_to_ctcb_ptr thread))))) (t_hrs_' (globals t))) \<longrightarrow> ta \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread \<and> (\<forall>t. (\<exists>thread_state. thread_state_lift thread_state = thread_state_lift (tcbState_C (the (cslift ta (tcb_ptr_to_ctcb_ptr thread))))\<lparr>blockingIPCCanGrantReply_CL := from_bool canGrantReply\<rparr> \<and> t_hrs_' (globals t) = hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_state) (the (cslift ta (tcb_ptr_to_ctcb_ptr thread))))) (t_hrs_' (globals ta))) \<longrightarrow> t \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread \<and> (\<forall>ta. (\<exists>thread_state. thread_state_lift thread_state = thread_state_lift (tcbState_C (the (cslift t (tcb_ptr_to_ctcb_ptr thread))))\<lparr>blockingIPCIsCall_CL := from_bool do_call\<rparr> \<and> t_hrs_' (globals ta) = hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_state) (the (cslift t (tcb_ptr_to_ctcb_ptr thread))))) (t_hrs_' (globals t))) \<longrightarrow> (s\<lparr>ksPSpace := (ksPSpace s)(thread \<mapsto> KOTCB (tcbState_update (\<lambda>_. Structures_H.thread_state.BlockedOnSend epptr badge canGrant canGrantReply do_call) tcb))\<rparr>, s'\<lparr>globals := globals s'\<lparr>t_hrs_' := t_hrs_' (globals ta)\<rparr>\<rparr>) \<in> rf_sr))))))
 2. \<And>rv' t t'. \<lbrakk>badge = badge && mask 28; epptr = epptr && ~~ mask 4; bos = ThreadState_BlockedOnSend \<and> epptr' = epptr \<and> badge' = badge \<and> cg = from_bool canGrant \<and> cgr = from_bool canGrantReply \<and> dc' = from_bool do_call\<rbrakk> \<Longrightarrow> ceqv \<Gamma> xfdc rv' t t' (CALL scheduleTCB_'proc(tcb_ptr_to_ctcb_ptr thread)) (?d'7 rv')
 3. \<And>rv rv'. \<lbrakk>badge = badge && mask 28; epptr = epptr && ~~ mask 4; bos = ThreadState_BlockedOnSend \<and> epptr' = epptr \<and> badge' = badge \<and> cg = from_bool canGrant \<and> cgr = from_bool canGrantReply \<and> dc' = from_bool do_call; dc rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q7 rv) (?Q'7 rv rv') hs (K_bind (do runnable <- isRunnable thread;
curThread <- getCurThread;
action <- getSchedulerAction;
when (\<not> runnable \<and> curThread = thread \<and> action = ResumeCurrentThread) $ rescheduleRequired
od) rv) (?d'7 rv')
 4. \<lbrakk>badge = badge && mask 28; epptr = epptr && ~~ mask 4; bos = ThreadState_BlockedOnSend \<and> epptr' = epptr \<and> badge' = badge \<and> cg = from_bool canGrant \<and> cgr = from_bool canGrantReply \<and> dc' = from_bool do_call\<rbrakk> \<Longrightarrow> \<lbrace>?R7\<rbrace> threadSet (tcbState_update (\<lambda>_. Structures_H.thread_state.BlockedOnSend epptr badge canGrant canGrantReply do_call)) thread \<lbrace>?Q7\<rbrace>
 5. \<lbrakk>badge = badge && mask 28; epptr = epptr && ~~ mask 4; bos = ThreadState_BlockedOnSend \<and> epptr' = epptr \<and> badge' = badge \<and> cg = from_bool canGrant \<and> cgr = from_bool canGrantReply \<and> dc' = from_bool do_call\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc ?Q'7
 6. \<And>s. \<lbrakk>badge = badge && mask 28; epptr = epptr && ~~ mask 4; bos = ThreadState_BlockedOnSend \<and> epptr' = epptr \<and> badge' = badge \<and> cg = from_bool canGrant \<and> cgr = from_bool canGrantReply \<and> dc' = from_bool do_call; (tcb_at' thread and Invariants_H.valid_queues and valid_objs' and sch_act_not thread and ep_at' epptr and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s \<and> (\<forall>d p. thread \<notin> set (ksReadyQueues s (d, p))))) s\<rbrakk> \<Longrightarrow> (tcb_at' thread and tcb_at' thread and ?R7) s
 7. \<And>s. \<lbrakk>badge = badge && mask 28; epptr = epptr && ~~ mask 4; bos = ThreadState_BlockedOnSend \<and> epptr' = epptr \<and> badge' = badge \<and> cg = from_bool canGrant \<and> cgr = from_bool canGrantReply \<and> dc' = from_bool do_call; s \<in> UNIV\<rbrakk> \<Longrightarrow> s \<in> UNIV proof (prove)
goal (7 subgoals):
 1. \<And>s s' tcb tcb' t thread_state ta thread_statea tb thread_stateb tc thread_statec td thread_stated te thread_statee. \<lbrakk>badge = badge && mask 28; epptr = epptr && ~~ mask 4; (s, s') \<in> rf_sr; ko_at' tcb thread s; cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb'; ctcb_relation tcb tcb'; tcb_at' thread s; bos = ThreadState_BlockedOnSend; epptr' = epptr; badge' = badge; cg = from_bool canGrant; cgr = from_bool canGrantReply; dc' = from_bool do_call; thread_state_lift thread_state = thread_state_lift (tcbState_C tcb')\<lparr>tsType_CL := SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnSend && mask 4\<rparr>; t_hrs_' (globals t) = hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_state) tcb')) (t_hrs_' (globals s')); thread_state_lift thread_statea = thread_state_lift (tcbState_C tcb')\<lparr>tsType_CL := SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnSend && mask 4, blockingObject_CL := epptr\<rparr>; t_hrs_' (globals ta) = hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_statea) tcb')) (hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_state) tcb')) (t_hrs_' (globals s'))); thread_state_lift thread_stateb = thread_state_lift (tcbState_C tcb')\<lparr>tsType_CL := SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnSend && mask 4, blockingObject_CL := epptr, blockingIPCBadge_CL := badge\<rparr>; t_hrs_' (globals tb) = hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_stateb) tcb')) (hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_statea) tcb')) (hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_state) tcb')) (t_hrs_' (globals s')))); thread_state_lift thread_statec = thread_state_lift (tcbState_C tcb')\<lparr>tsType_CL := SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnSend && mask 4, blockingObject_CL := epptr, blockingIPCBadge_CL := badge, blockingIPCCanGrant_CL := from_bool canGrant\<rparr>; t_hrs_' (globals tc) = hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_statec) tcb')) (hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_stateb) tcb')) (hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_statea) tcb')) (hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_state) tcb')) (t_hrs_' (globals s'))))); thread_state_lift thread_stated = thread_state_lift (tcbState_C tcb')\<lparr>tsType_CL := SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnSend && mask 4, blockingObject_CL := epptr, blockingIPCBadge_CL := badge, blockingIPCCanGrant_CL := from_bool canGrant, blockingIPCCanGrantReply_CL := from_bool canGrantReply\<rparr>; t_hrs_' (globals td) = hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_stated) tcb')) (hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_statec) tcb')) (hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_stateb) tcb')) (hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_statea) tcb')) (hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_state) tcb')) (t_hrs_' (globals s')))))); thread_state_lift thread_statee = thread_state_lift (tcbState_C tcb')\<lparr>tsType_CL := SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnSend && mask 4, blockingObject_CL := epptr, blockingIPCBadge_CL := badge, blockingIPCCanGrant_CL := from_bool canGrant, blockingIPCCanGrantReply_CL := from_bool canGrantReply, blockingIPCIsCall_CL := from_bool do_call\<rparr>; t_hrs_' (globals te) = hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_statee) tcb')) (hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_stated) tcb')) (hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_statec) tcb')) (hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_stateb) tcb')) (hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_statea) tcb')) (hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_state) tcb')) (t_hrs_' (globals s')))))))\<rbrakk> \<Longrightarrow> (s\<lparr>ksPSpace := (ksPSpace s)(thread \<mapsto> KOTCB (tcbState_update (\<lambda>_. Structures_H.thread_state.BlockedOnSend epptr badge canGrant canGrantReply do_call) tcb))\<rparr>, s'\<lparr>globals := globals s'\<lparr>t_hrs_' := hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_statee) tcb')) (t_hrs_' (globals s'))\<rparr>\<rparr>) \<in> rf_sr
 2. \<And>rv' t t'. \<lbrakk>badge = badge && mask 28; epptr = epptr && ~~ mask 4; bos = ThreadState_BlockedOnSend \<and> epptr' = epptr \<and> badge' = badge \<and> cg = from_bool canGrant \<and> cgr = from_bool canGrantReply \<and> dc' = from_bool do_call\<rbrakk> \<Longrightarrow> ceqv \<Gamma> xfdc rv' t t' (CALL scheduleTCB_'proc(tcb_ptr_to_ctcb_ptr thread)) (?d'7 rv')
 3. \<And>rv rv'. \<lbrakk>badge = badge && mask 28; epptr = epptr && ~~ mask 4; bos = ThreadState_BlockedOnSend \<and> epptr' = epptr \<and> badge' = badge \<and> cg = from_bool canGrant \<and> cgr = from_bool canGrantReply \<and> dc' = from_bool do_call; dc rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q7 rv) (?Q'7 rv rv') hs (K_bind (do runnable <- isRunnable thread;
curThread <- getCurThread;
action <- getSchedulerAction;
when (\<not> runnable \<and> curThread = thread \<and> action = ResumeCurrentThread) $ rescheduleRequired
od) rv) (?d'7 rv')
 4. \<lbrakk>badge = badge && mask 28; epptr = epptr && ~~ mask 4; bos = ThreadState_BlockedOnSend \<and> epptr' = epptr \<and> badge' = badge \<and> cg = from_bool canGrant \<and> cgr = from_bool canGrantReply \<and> dc' = from_bool do_call\<rbrakk> \<Longrightarrow> \<lbrace>?R7\<rbrace> threadSet (tcbState_update (\<lambda>_. Structures_H.thread_state.BlockedOnSend epptr badge canGrant canGrantReply do_call)) thread \<lbrace>?Q7\<rbrace>
 5. \<lbrakk>badge = badge && mask 28; epptr = epptr && ~~ mask 4; bos = ThreadState_BlockedOnSend \<and> epptr' = epptr \<and> badge' = badge \<and> cg = from_bool canGrant \<and> cgr = from_bool canGrantReply \<and> dc' = from_bool do_call\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc ?Q'7
 6. \<And>s. \<lbrakk>badge = badge && mask 28; epptr = epptr && ~~ mask 4; bos = ThreadState_BlockedOnSend \<and> epptr' = epptr \<and> badge' = badge \<and> cg = from_bool canGrant \<and> cgr = from_bool canGrantReply \<and> dc' = from_bool do_call; (tcb_at' thread and Invariants_H.valid_queues and valid_objs' and sch_act_not thread and ep_at' epptr and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s \<and> (\<forall>d p. thread \<notin> set (ksReadyQueues s (d, p))))) s\<rbrakk> \<Longrightarrow> (tcb_at' thread and tcb_at' thread and ?R7) s
 7. \<And>s. \<lbrakk>badge = badge && mask 28; epptr = epptr && ~~ mask 4; bos = ThreadState_BlockedOnSend \<and> epptr' = epptr \<and> badge' = badge \<and> cg = from_bool canGrant \<and> cgr = from_bool canGrantReply \<and> dc' = from_bool do_call; s \<in> UNIV\<rbrakk> \<Longrightarrow> s \<in> UNIV proof (prove)
goal (8 subgoals):
 1. \<And>s s' tcb tcb' t thread_state ta thread_statea tb thread_stateb tc thread_statec td thread_stated te thread_statee. \<lbrakk>badge = badge && mask 28; epptr = epptr && ~~ mask 4; ko_at' tcb thread s; cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb'; ctcb_relation tcb tcb'; tcb_at' thread s; bos = ThreadState_BlockedOnSend; epptr' = epptr; badge' = badge; cg = from_bool canGrant; cgr = from_bool canGrantReply; dc' = from_bool do_call; thread_state_lift thread_state = thread_state_lift (tcbState_C tcb')\<lparr>tsType_CL := SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnSend && mask 4\<rparr>; t_hrs_' (globals t) = hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_state) tcb')) (t_hrs_' (globals s')); thread_state_lift thread_statea = thread_state_lift (tcbState_C tcb')\<lparr>tsType_CL := SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnSend && mask 4, blockingObject_CL := epptr\<rparr>; t_hrs_' (globals ta) = hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_statea) tcb')) (hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_state) tcb')) (t_hrs_' (globals s'))); thread_state_lift thread_stateb = thread_state_lift (tcbState_C tcb')\<lparr>tsType_CL := SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnSend && mask 4, blockingObject_CL := epptr, blockingIPCBadge_CL := badge\<rparr>; t_hrs_' (globals tb) = hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_stateb) tcb')) (hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_statea) tcb')) (hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_state) tcb')) (t_hrs_' (globals s')))); thread_state_lift thread_statec = thread_state_lift (tcbState_C tcb')\<lparr>tsType_CL := SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnSend && mask 4, blockingObject_CL := epptr, blockingIPCBadge_CL := badge, blockingIPCCanGrant_CL := from_bool canGrant\<rparr>; t_hrs_' (globals tc) = hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_statec) tcb')) (hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_stateb) tcb')) (hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_statea) tcb')) (hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_state) tcb')) (t_hrs_' (globals s'))))); thread_state_lift thread_stated = thread_state_lift (tcbState_C tcb')\<lparr>tsType_CL := SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnSend && mask 4, blockingObject_CL := epptr, blockingIPCBadge_CL := badge, blockingIPCCanGrant_CL := from_bool canGrant, blockingIPCCanGrantReply_CL := from_bool canGrantReply\<rparr>; t_hrs_' (globals td) = hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_stated) tcb')) (hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_statec) tcb')) (hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_stateb) tcb')) (hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_statea) tcb')) (hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_state) tcb')) (t_hrs_' (globals s')))))); thread_state_lift thread_statee = thread_state_lift (tcbState_C tcb')\<lparr>tsType_CL := SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnSend && mask 4, blockingObject_CL := epptr, blockingIPCBadge_CL := badge, blockingIPCCanGrant_CL := from_bool canGrant, blockingIPCCanGrantReply_CL := from_bool canGrantReply, blockingIPCIsCall_CL := from_bool do_call\<rparr>; t_hrs_' (globals te) = hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_statee) tcb')) (hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_stated) tcb')) (hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_statec) tcb')) (hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_stateb) tcb')) (hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_statea) tcb')) (hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_state) tcb')) (t_hrs_' (globals s')))))))\<rbrakk> \<Longrightarrow> \<forall>x\<in>ran tcb_cte_cases. case x of (getF, setF) \<Rightarrow> getF (tcbState_update (\<lambda>_. Structures_H.thread_state.BlockedOnSend epptr badge canGrant canGrantReply do_call) tcb) = getF tcb
 2. \<And>s s' tcb tcb' t thread_state ta thread_statea tb thread_stateb tc thread_statec td thread_stated te thread_statee. \<lbrakk>badge = badge && mask 28; epptr = epptr && ~~ mask 4; ko_at' tcb thread s; cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb'; ctcb_relation tcb tcb'; tcb_at' thread s; bos = ThreadState_BlockedOnSend; epptr' = epptr; badge' = badge; cg = from_bool canGrant; cgr = from_bool canGrantReply; dc' = from_bool do_call; thread_state_lift thread_state = thread_state_lift (tcbState_C tcb')\<lparr>tsType_CL := SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnSend && mask 4\<rparr>; t_hrs_' (globals t) = hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_state) tcb')) (t_hrs_' (globals s')); thread_state_lift thread_statea = thread_state_lift (tcbState_C tcb')\<lparr>tsType_CL := SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnSend && mask 4, blockingObject_CL := epptr\<rparr>; t_hrs_' (globals ta) = hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_statea) tcb')) (hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_state) tcb')) (t_hrs_' (globals s'))); thread_state_lift thread_stateb = thread_state_lift (tcbState_C tcb')\<lparr>tsType_CL := SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnSend && mask 4, blockingObject_CL := epptr, blockingIPCBadge_CL := badge\<rparr>; t_hrs_' (globals tb) = hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_stateb) tcb')) (hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_statea) tcb')) (hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_state) tcb')) (t_hrs_' (globals s')))); thread_state_lift thread_statec = thread_state_lift (tcbState_C tcb')\<lparr>tsType_CL := SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnSend && mask 4, blockingObject_CL := epptr, blockingIPCBadge_CL := badge, blockingIPCCanGrant_CL := from_bool canGrant\<rparr>; t_hrs_' (globals tc) = hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_statec) tcb')) (hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_stateb) tcb')) (hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_statea) tcb')) (hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_state) tcb')) (t_hrs_' (globals s'))))); thread_state_lift thread_stated = thread_state_lift (tcbState_C tcb')\<lparr>tsType_CL := SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnSend && mask 4, blockingObject_CL := epptr, blockingIPCBadge_CL := badge, blockingIPCCanGrant_CL := from_bool canGrant, blockingIPCCanGrantReply_CL := from_bool canGrantReply\<rparr>; t_hrs_' (globals td) = hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_stated) tcb')) (hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_statec) tcb')) (hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_stateb) tcb')) (hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_statea) tcb')) (hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_state) tcb')) (t_hrs_' (globals s')))))); thread_state_lift thread_statee = thread_state_lift (tcbState_C tcb')\<lparr>tsType_CL := SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnSend && mask 4, blockingObject_CL := epptr, blockingIPCBadge_CL := badge, blockingIPCCanGrant_CL := from_bool canGrant, blockingIPCCanGrantReply_CL := from_bool canGrantReply, blockingIPCIsCall_CL := from_bool do_call\<rparr>; t_hrs_' (globals te) = hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_statee) tcb')) (hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_stated) tcb')) (hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_statec) tcb')) (hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_stateb) tcb')) (hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_statea) tcb')) (hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_state) tcb')) (t_hrs_' (globals s')))))))\<rbrakk> \<Longrightarrow> ctcb_relation (tcbState_update (\<lambda>_. Structures_H.thread_state.BlockedOnSend epptr badge canGrant canGrantReply do_call) tcb) (tcbState_C_update (\<lambda>_. thread_statee) tcb')
 3. \<And>rv' t t'. \<lbrakk>badge = badge && mask 28; epptr = epptr && ~~ mask 4; bos = ThreadState_BlockedOnSend \<and> epptr' = epptr \<and> badge' = badge \<and> cg = from_bool canGrant \<and> cgr = from_bool canGrantReply \<and> dc' = from_bool do_call\<rbrakk> \<Longrightarrow> ceqv \<Gamma> xfdc rv' t t' (CALL scheduleTCB_'proc(tcb_ptr_to_ctcb_ptr thread)) (?d'7 rv')
 4. \<And>rv rv'. \<lbrakk>badge = badge && mask 28; epptr = epptr && ~~ mask 4; bos = ThreadState_BlockedOnSend \<and> epptr' = epptr \<and> badge' = badge \<and> cg = from_bool canGrant \<and> cgr = from_bool canGrantReply \<and> dc' = from_bool do_call; dc rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q7 rv) (?Q'7 rv rv') hs (K_bind (do runnable <- isRunnable thread;
curThread <- getCurThread;
action <- getSchedulerAction;
when (\<not> runnable \<and> curThread = thread \<and> action = ResumeCurrentThread) $ rescheduleRequired
od) rv) (?d'7 rv')
 5. \<lbrakk>badge = badge && mask 28; epptr = epptr && ~~ mask 4; bos = ThreadState_BlockedOnSend \<and> epptr' = epptr \<and> badge' = badge \<and> cg = from_bool canGrant \<and> cgr = from_bool canGrantReply \<and> dc' = from_bool do_call\<rbrakk> \<Longrightarrow> \<lbrace>?R7\<rbrace> threadSet (tcbState_update (\<lambda>_. Structures_H.thread_state.BlockedOnSend epptr badge canGrant canGrantReply do_call)) thread \<lbrace>?Q7\<rbrace>
 6. \<lbrakk>badge = badge && mask 28; epptr = epptr && ~~ mask 4; bos = ThreadState_BlockedOnSend \<and> epptr' = epptr \<and> badge' = badge \<and> cg = from_bool canGrant \<and> cgr = from_bool canGrantReply \<and> dc' = from_bool do_call\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc ?Q'7
 7. \<And>s. \<lbrakk>badge = badge && mask 28; epptr = epptr && ~~ mask 4; bos = ThreadState_BlockedOnSend \<and> epptr' = epptr \<and> badge' = badge \<and> cg = from_bool canGrant \<and> cgr = from_bool canGrantReply \<and> dc' = from_bool do_call; (tcb_at' thread and Invariants_H.valid_queues and valid_objs' and sch_act_not thread and ep_at' epptr and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s \<and> (\<forall>d p. thread \<notin> set (ksReadyQueues s (d, p))))) s\<rbrakk> \<Longrightarrow> (tcb_at' thread and tcb_at' thread and ?R7) s
 8. \<And>s. \<lbrakk>badge = badge && mask 28; epptr = epptr && ~~ mask 4; bos = ThreadState_BlockedOnSend \<and> epptr' = epptr \<and> badge' = badge \<and> cg = from_bool canGrant \<and> cgr = from_bool canGrantReply \<and> dc' = from_bool do_call; s \<in> UNIV\<rbrakk> \<Longrightarrow> s \<in> UNIV proof (prove)
goal (7 subgoals):
 1. \<And>s s' tcb tcb' t thread_state ta thread_statea tb thread_stateb tc thread_statec td thread_stated te thread_statee. \<lbrakk>badge = badge && mask 28; epptr = epptr && ~~ mask 4; ko_at' tcb thread s; cslift s' (tcb_ptr_to_ctcb_ptr thread) = Some tcb'; ctcb_relation tcb tcb'; tcb_at' thread s; bos = ThreadState_BlockedOnSend; epptr' = epptr; badge' = badge; cg = from_bool canGrant; cgr = from_bool canGrantReply; dc' = from_bool do_call; thread_state_lift thread_state = thread_state_lift (tcbState_C tcb')\<lparr>tsType_CL := SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnSend && mask 4\<rparr>; t_hrs_' (globals t) = hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_state) tcb')) (t_hrs_' (globals s')); thread_state_lift thread_statea = thread_state_lift (tcbState_C tcb')\<lparr>tsType_CL := SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnSend && mask 4, blockingObject_CL := epptr\<rparr>; t_hrs_' (globals ta) = hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_statea) tcb')) (hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_state) tcb')) (t_hrs_' (globals s'))); thread_state_lift thread_stateb = thread_state_lift (tcbState_C tcb')\<lparr>tsType_CL := SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnSend && mask 4, blockingObject_CL := epptr, blockingIPCBadge_CL := badge\<rparr>; t_hrs_' (globals tb) = hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_stateb) tcb')) (hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_statea) tcb')) (hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_state) tcb')) (t_hrs_' (globals s')))); thread_state_lift thread_statec = thread_state_lift (tcbState_C tcb')\<lparr>tsType_CL := SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnSend && mask 4, blockingObject_CL := epptr, blockingIPCBadge_CL := badge, blockingIPCCanGrant_CL := from_bool canGrant\<rparr>; t_hrs_' (globals tc) = hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_statec) tcb')) (hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_stateb) tcb')) (hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_statea) tcb')) (hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_state) tcb')) (t_hrs_' (globals s'))))); thread_state_lift thread_stated = thread_state_lift (tcbState_C tcb')\<lparr>tsType_CL := SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnSend && mask 4, blockingObject_CL := epptr, blockingIPCBadge_CL := badge, blockingIPCCanGrant_CL := from_bool canGrant, blockingIPCCanGrantReply_CL := from_bool canGrantReply\<rparr>; t_hrs_' (globals td) = hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_stated) tcb')) (hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_statec) tcb')) (hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_stateb) tcb')) (hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_statea) tcb')) (hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_state) tcb')) (t_hrs_' (globals s')))))); thread_state_lift thread_statee = thread_state_lift (tcbState_C tcb')\<lparr>tsType_CL := SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnSend && mask 4, blockingObject_CL := epptr, blockingIPCBadge_CL := badge, blockingIPCCanGrant_CL := from_bool canGrant, blockingIPCCanGrantReply_CL := from_bool canGrantReply, blockingIPCIsCall_CL := from_bool do_call\<rparr>; t_hrs_' (globals te) = hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_statee) tcb')) (hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_stated) tcb')) (hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_statec) tcb')) (hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_stateb) tcb')) (hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_statea) tcb')) (hrs_mem_update (heap_update (tcb_ptr_to_ctcb_ptr thread) (tcbState_C_update (\<lambda>_. thread_state) tcb')) (t_hrs_' (globals s')))))))\<rbrakk> \<Longrightarrow> ctcb_relation (tcbState_update (\<lambda>_. Structures_H.thread_state.BlockedOnSend epptr badge canGrant canGrantReply do_call) tcb) (tcbState_C_update (\<lambda>_. thread_statee) tcb')
 2. \<And>rv' t t'. \<lbrakk>badge = badge && mask 28; epptr = epptr && ~~ mask 4; bos = ThreadState_BlockedOnSend \<and> epptr' = epptr \<and> badge' = badge \<and> cg = from_bool canGrant \<and> cgr = from_bool canGrantReply \<and> dc' = from_bool do_call\<rbrakk> \<Longrightarrow> ceqv \<Gamma> xfdc rv' t t' (CALL scheduleTCB_'proc(tcb_ptr_to_ctcb_ptr thread)) (?d'7 rv')
 3. \<And>rv rv'. \<lbrakk>badge = badge && mask 28; epptr = epptr && ~~ mask 4; bos = ThreadState_BlockedOnSend \<and> epptr' = epptr \<and> badge' = badge \<and> cg = from_bool canGrant \<and> cgr = from_bool canGrantReply \<and> dc' = from_bool do_call; dc rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q7 rv) (?Q'7 rv rv') hs (K_bind (do runnable <- isRunnable thread;
curThread <- getCurThread;
action <- getSchedulerAction;
when (\<not> runnable \<and> curThread = thread \<and> action = ResumeCurrentThread) $ rescheduleRequired
od) rv) (?d'7 rv')
 4. \<lbrakk>badge = badge && mask 28; epptr = epptr && ~~ mask 4; bos = ThreadState_BlockedOnSend \<and> epptr' = epptr \<and> badge' = badge \<and> cg = from_bool canGrant \<and> cgr = from_bool canGrantReply \<and> dc' = from_bool do_call\<rbrakk> \<Longrightarrow> \<lbrace>?R7\<rbrace> threadSet (tcbState_update (\<lambda>_. Structures_H.thread_state.BlockedOnSend epptr badge canGrant canGrantReply do_call)) thread \<lbrace>?Q7\<rbrace>
 5. \<lbrakk>badge = badge && mask 28; epptr = epptr && ~~ mask 4; bos = ThreadState_BlockedOnSend \<and> epptr' = epptr \<and> badge' = badge \<and> cg = from_bool canGrant \<and> cgr = from_bool canGrantReply \<and> dc' = from_bool do_call\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc ?Q'7
 6. \<And>s. \<lbrakk>badge = badge && mask 28; epptr = epptr && ~~ mask 4; bos = ThreadState_BlockedOnSend \<and> epptr' = epptr \<and> badge' = badge \<and> cg = from_bool canGrant \<and> cgr = from_bool canGrantReply \<and> dc' = from_bool do_call; (tcb_at' thread and Invariants_H.valid_queues and valid_objs' and sch_act_not thread and ep_at' epptr and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s \<and> (\<forall>d p. thread \<notin> set (ksReadyQueues s (d, p))))) s\<rbrakk> \<Longrightarrow> (tcb_at' thread and tcb_at' thread and ?R7) s
 7. \<And>s. \<lbrakk>badge = badge && mask 28; epptr = epptr && ~~ mask 4; bos = ThreadState_BlockedOnSend \<and> epptr' = epptr \<and> badge' = badge \<and> cg = from_bool canGrant \<and> cgr = from_bool canGrantReply \<and> dc' = from_bool do_call; s \<in> UNIV\<rbrakk> \<Longrightarrow> s \<in> UNIV proof (prove)
goal (6 subgoals):
 1. \<And>rv' t t'. \<lbrakk>badge = badge && mask 28; epptr = epptr && ~~ mask 4; bos = ThreadState_BlockedOnSend \<and> epptr' = epptr \<and> badge' = badge \<and> cg = from_bool canGrant \<and> cgr = from_bool canGrantReply \<and> dc' = from_bool do_call\<rbrakk> \<Longrightarrow> ceqv \<Gamma> xfdc rv' t t' (CALL scheduleTCB_'proc(tcb_ptr_to_ctcb_ptr thread)) (?d'7 rv')
 2. \<And>rv rv'. \<lbrakk>badge = badge && mask 28; epptr = epptr && ~~ mask 4; bos = ThreadState_BlockedOnSend \<and> epptr' = epptr \<and> badge' = badge \<and> cg = from_bool canGrant \<and> cgr = from_bool canGrantReply \<and> dc' = from_bool do_call; dc rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q7 rv) (?Q'7 rv rv') hs (K_bind (do runnable <- isRunnable thread;
curThread <- getCurThread;
action <- getSchedulerAction;
when (\<not> runnable \<and> curThread = thread \<and> action = ResumeCurrentThread) $ rescheduleRequired
od) rv) (?d'7 rv')
 3. \<lbrakk>badge = badge && mask 28; epptr = epptr && ~~ mask 4; bos = ThreadState_BlockedOnSend \<and> epptr' = epptr \<and> badge' = badge \<and> cg = from_bool canGrant \<and> cgr = from_bool canGrantReply \<and> dc' = from_bool do_call\<rbrakk> \<Longrightarrow> \<lbrace>?R7\<rbrace> threadSet (tcbState_update (\<lambda>_. Structures_H.thread_state.BlockedOnSend epptr badge canGrant canGrantReply do_call)) thread \<lbrace>?Q7\<rbrace>
 4. \<lbrakk>badge = badge && mask 28; epptr = epptr && ~~ mask 4; bos = ThreadState_BlockedOnSend \<and> epptr' = epptr \<and> badge' = badge \<and> cg = from_bool canGrant \<and> cgr = from_bool canGrantReply \<and> dc' = from_bool do_call\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc ?Q'7
 5. \<And>s. \<lbrakk>badge = badge && mask 28; epptr = epptr && ~~ mask 4; bos = ThreadState_BlockedOnSend \<and> epptr' = epptr \<and> badge' = badge \<and> cg = from_bool canGrant \<and> cgr = from_bool canGrantReply \<and> dc' = from_bool do_call; (tcb_at' thread and Invariants_H.valid_queues and valid_objs' and sch_act_not thread and ep_at' epptr and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s \<and> (\<forall>d p. thread \<notin> set (ksReadyQueues s (d, p))))) s\<rbrakk> \<Longrightarrow> (tcb_at' thread and tcb_at' thread and ?R7) s
 6. \<And>s. \<lbrakk>badge = badge && mask 28; epptr = epptr && ~~ mask 4; bos = ThreadState_BlockedOnSend \<and> epptr' = epptr \<and> badge' = badge \<and> cg = from_bool canGrant \<and> cgr = from_bool canGrantReply \<and> dc' = from_bool do_call; s \<in> UNIV\<rbrakk> \<Longrightarrow> s \<in> UNIV proof (prove)
goal (5 subgoals):
 1. \<And>rv rv'. \<lbrakk>badge = badge && mask 28; epptr = epptr && ~~ mask 4; bos = ThreadState_BlockedOnSend \<and> epptr' = epptr \<and> badge' = badge \<and> cg = from_bool canGrant \<and> cgr = from_bool canGrantReply \<and> dc' = from_bool do_call; dc rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q7 rv) (?Q'7 rv rv') hs (K_bind (do runnable <- isRunnable thread;
curThread <- getCurThread;
action <- getSchedulerAction;
when (\<not> runnable \<and> curThread = thread \<and> action = ResumeCurrentThread) $ rescheduleRequired
od) rv) (CALL scheduleTCB_'proc(tcb_ptr_to_ctcb_ptr thread))
 2. \<lbrakk>badge = badge && mask 28; epptr = epptr && ~~ mask 4; bos = ThreadState_BlockedOnSend \<and> epptr' = epptr \<and> badge' = badge \<and> cg = from_bool canGrant \<and> cgr = from_bool canGrantReply \<and> dc' = from_bool do_call\<rbrakk> \<Longrightarrow> \<lbrace>?R7\<rbrace> threadSet (tcbState_update (\<lambda>_. Structures_H.thread_state.BlockedOnSend epptr badge canGrant canGrantReply do_call)) thread \<lbrace>?Q7\<rbrace>
 3. \<lbrakk>badge = badge && mask 28; epptr = epptr && ~~ mask 4; bos = ThreadState_BlockedOnSend \<and> epptr' = epptr \<and> badge' = badge \<and> cg = from_bool canGrant \<and> cgr = from_bool canGrantReply \<and> dc' = from_bool do_call\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc ?Q'7
 4. \<And>s. \<lbrakk>badge = badge && mask 28; epptr = epptr && ~~ mask 4; bos = ThreadState_BlockedOnSend \<and> epptr' = epptr \<and> badge' = badge \<and> cg = from_bool canGrant \<and> cgr = from_bool canGrantReply \<and> dc' = from_bool do_call; (tcb_at' thread and Invariants_H.valid_queues and valid_objs' and sch_act_not thread and ep_at' epptr and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s \<and> (\<forall>d p. thread \<notin> set (ksReadyQueues s (d, p))))) s\<rbrakk> \<Longrightarrow> (tcb_at' thread and tcb_at' thread and ?R7) s
 5. \<And>s. \<lbrakk>badge = badge && mask 28; epptr = epptr && ~~ mask 4; bos = ThreadState_BlockedOnSend \<and> epptr' = epptr \<and> badge' = badge \<and> cg = from_bool canGrant \<and> cgr = from_bool canGrantReply \<and> dc' = from_bool do_call; s \<in> UNIV\<rbrakk> \<Longrightarrow> s \<in> UNIV proof (prove)
goal (5 subgoals):
 1. \<And>rv'. \<lbrakk>badge = badge && mask 28; epptr = epptr && ~~ mask 4; bos = ThreadState_BlockedOnSend; epptr' = epptr; badge' = badge; cg = from_bool canGrant; cgr = from_bool canGrantReply; dc' = from_bool do_call\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q7 ()) (?Q'7 () rv') hs (do runnable <- isRunnable thread;
curThread <- getCurThread;
action <- getSchedulerAction;
when (\<not> runnable \<and> curThread = thread \<and> action = ResumeCurrentThread) rescheduleRequired
od) (CALL scheduleTCB_'proc(tcb_ptr_to_ctcb_ptr thread))
 2. \<lbrakk>badge = badge && mask 28; epptr = epptr && ~~ mask 4; bos = ThreadState_BlockedOnSend \<and> epptr' = epptr \<and> badge' = badge \<and> cg = from_bool canGrant \<and> cgr = from_bool canGrantReply \<and> dc' = from_bool do_call\<rbrakk> \<Longrightarrow> \<lbrace>?R7\<rbrace> threadSet (tcbState_update (\<lambda>_. Structures_H.thread_state.BlockedOnSend epptr badge canGrant canGrantReply do_call)) thread \<lbrace>?Q7\<rbrace>
 3. \<lbrakk>badge = badge && mask 28; epptr = epptr && ~~ mask 4; bos = ThreadState_BlockedOnSend \<and> epptr' = epptr \<and> badge' = badge \<and> cg = from_bool canGrant \<and> cgr = from_bool canGrantReply \<and> dc' = from_bool do_call\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc ?Q'7
 4. \<And>s. \<lbrakk>badge = badge && mask 28; epptr = epptr && ~~ mask 4; bos = ThreadState_BlockedOnSend \<and> epptr' = epptr \<and> badge' = badge \<and> cg = from_bool canGrant \<and> cgr = from_bool canGrantReply \<and> dc' = from_bool do_call; (tcb_at' thread and Invariants_H.valid_queues and valid_objs' and sch_act_not thread and ep_at' epptr and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s \<and> (\<forall>d p. thread \<notin> set (ksReadyQueues s (d, p))))) s\<rbrakk> \<Longrightarrow> (tcb_at' thread and tcb_at' thread and ?R7) s
 5. \<And>s. \<lbrakk>badge = badge && mask 28; epptr = epptr && ~~ mask 4; bos = ThreadState_BlockedOnSend \<and> epptr' = epptr \<and> badge' = badge \<and> cg = from_bool canGrant \<and> cgr = from_bool canGrantReply \<and> dc' = from_bool do_call; s \<in> UNIV\<rbrakk> \<Longrightarrow> s \<in> UNIV proof (prove)
goal (4 subgoals):
 1. \<lbrakk>badge = badge && mask 28; epptr = epptr && ~~ mask 4; bos = ThreadState_BlockedOnSend \<and> epptr' = epptr \<and> badge' = badge \<and> cg = from_bool canGrant \<and> cgr = from_bool canGrantReply \<and> dc' = from_bool do_call\<rbrakk> \<Longrightarrow> \<lbrace>?R7\<rbrace> threadSet (tcbState_update (\<lambda>_. Structures_H.thread_state.BlockedOnSend epptr badge canGrant canGrantReply do_call)) thread \<lbrace>\<lambda>a. tcb_at' thread and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and Invariants_H.valid_queues and valid_objs'\<rbrace>
 2. \<lbrakk>badge = badge && mask 28; epptr = epptr && ~~ mask 4; bos = ThreadState_BlockedOnSend \<and> epptr' = epptr \<and> badge' = badge \<and> cg = from_bool canGrant \<and> cgr = from_bool canGrantReply \<and> dc' = from_bool do_call\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (\<lambda>a b. {s. tptr_'_update (\<lambda>_. tcb_ptr_to_ctcb_ptr thread) s \<in> UNIV \<inter> \<lbrace>\<acute>tptr = tcb_ptr_to_ctcb_ptr thread\<rbrace>})
 3. \<And>s. \<lbrakk>badge = badge && mask 28; epptr = epptr && ~~ mask 4; bos = ThreadState_BlockedOnSend \<and> epptr' = epptr \<and> badge' = badge \<and> cg = from_bool canGrant \<and> cgr = from_bool canGrantReply \<and> dc' = from_bool do_call; (tcb_at' thread and Invariants_H.valid_queues and valid_objs' and sch_act_not thread and ep_at' epptr and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s \<and> (\<forall>d p. thread \<notin> set (ksReadyQueues s (d, p))))) s\<rbrakk> \<Longrightarrow> (tcb_at' thread and tcb_at' thread and ?R7) s
 4. \<And>s. \<lbrakk>badge = badge && mask 28; epptr = epptr && ~~ mask 4; bos = ThreadState_BlockedOnSend \<and> epptr' = epptr \<and> badge' = badge \<and> cg = from_bool canGrant \<and> cgr = from_bool canGrantReply \<and> dc' = from_bool do_call; s \<in> UNIV\<rbrakk> \<Longrightarrow> s \<in> UNIV proof (prove)
goal (3 subgoals):
 1. \<lbrakk>badge = badge && mask 28; epptr = epptr && ~~ mask 4; bos = ThreadState_BlockedOnSend \<and> epptr' = epptr \<and> badge' = badge \<and> cg = from_bool canGrant \<and> cgr = from_bool canGrantReply \<and> dc' = from_bool do_call\<rbrakk> \<Longrightarrow> guard_is_UNIV dc xfdc (\<lambda>a b. {s. tptr_'_update (\<lambda>_. tcb_ptr_to_ctcb_ptr thread) s \<in> UNIV \<inter> \<lbrace>\<acute>tptr = tcb_ptr_to_ctcb_ptr thread\<rbrace>})
 2. \<And>s. \<lbrakk>badge = badge && mask 28; epptr = epptr && ~~ mask 4; bos = ThreadState_BlockedOnSend \<and> epptr' = epptr \<and> badge' = badge \<and> cg = from_bool canGrant \<and> cgr = from_bool canGrantReply \<and> dc' = from_bool do_call; (tcb_at' thread and Invariants_H.valid_queues and valid_objs' and sch_act_not thread and ep_at' epptr and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s \<and> (\<forall>d p. thread \<notin> set (ksReadyQueues s (d, p))))) s\<rbrakk> \<Longrightarrow> (tcb_at' thread and tcb_at' thread and (\<lambda>s. obj_at' (\<lambda>obj. if thread = thread then True else True) thread s \<and> ((ksSchedulerAction s = SwitchToThread thread \<longrightarrow> runnable' (Structures_H.thread_state.BlockedOnSend epptr badge canGrant canGrantReply do_call)) \<and> weak_sch_act_wf (ksSchedulerAction s) s) \<and> (Invariants_H.valid_queues and (\<lambda>s. \<forall>d p. (\<exists>tcb. (inQ d p tcb \<and> runnable' (tcbState tcb)) \<and> \<not> (inQ d p (tcbState_update (\<lambda>_. Structures_H.thread_state.BlockedOnSend epptr badge canGrant canGrantReply do_call) tcb) \<and> runnable' (tcbState (tcbState_update (\<lambda>_. Structures_H.thread_state.BlockedOnSend epptr badge canGrant canGrantReply do_call) tcb)))) \<longrightarrow> obj_at' (\<lambda>tcb. (inQ d p tcb \<and> runnable' (tcbState tcb)) \<and> \<not> (inQ d p (tcbState_update (\<lambda>_. Structures_H.thread_state.BlockedOnSend epptr badge canGrant canGrantReply do_call) tcb) \<and> runnable' (tcbState (tcbState_update (\<lambda>_. Structures_H.thread_state.BlockedOnSend epptr badge canGrant canGrantReply do_call) tcb)))) thread s \<longrightarrow> thread \<notin> set (ksReadyQueues s (d, p)))) s \<and> (valid_objs' and (\<lambda>s. \<forall>tcb. valid_tcb' tcb s \<longrightarrow> valid_tcb' (tcbState_update (\<lambda>_. Structures_H.thread_state.BlockedOnSend epptr badge canGrant canGrantReply do_call) tcb) s)) s)) s
 3. \<And>s. \<lbrakk>badge = badge && mask 28; epptr = epptr && ~~ mask 4; bos = ThreadState_BlockedOnSend \<and> epptr' = epptr \<and> badge' = badge \<and> cg = from_bool canGrant \<and> cgr = from_bool canGrantReply \<and> dc' = from_bool do_call; s \<in> UNIV\<rbrakk> \<Longrightarrow> s \<in> UNIV proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>badge = badge && mask 28; epptr = epptr && ~~ mask 4; bos = ThreadState_BlockedOnSend \<and> epptr' = epptr \<and> badge' = badge \<and> cg = from_bool canGrant \<and> cgr = from_bool canGrantReply \<and> dc' = from_bool do_call; (tcb_at' thread and Invariants_H.valid_queues and valid_objs' and sch_act_not thread and ep_at' epptr and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s \<and> (\<forall>d p. thread \<notin> set (ksReadyQueues s (d, p))))) s\<rbrakk> \<Longrightarrow> (tcb_at' thread and tcb_at' thread and (\<lambda>s. obj_at' (\<lambda>obj. if thread = thread then True else True) thread s \<and> ((ksSchedulerAction s = SwitchToThread thread \<longrightarrow> runnable' (Structures_H.thread_state.BlockedOnSend epptr badge canGrant canGrantReply do_call)) \<and> weak_sch_act_wf (ksSchedulerAction s) s) \<and> (Invariants_H.valid_queues and (\<lambda>s. \<forall>d p. (\<exists>tcb. (inQ d p tcb \<and> runnable' (tcbState tcb)) \<and> \<not> (inQ d p (tcbState_update (\<lambda>_. Structures_H.thread_state.BlockedOnSend epptr badge canGrant canGrantReply do_call) tcb) \<and> runnable' (tcbState (tcbState_update (\<lambda>_. Structures_H.thread_state.BlockedOnSend epptr badge canGrant canGrantReply do_call) tcb)))) \<longrightarrow> obj_at' (\<lambda>tcb. (inQ d p tcb \<and> runnable' (tcbState tcb)) \<and> \<not> (inQ d p (tcbState_update (\<lambda>_. Structures_H.thread_state.BlockedOnSend epptr badge canGrant canGrantReply do_call) tcb) \<and> runnable' (tcbState (tcbState_update (\<lambda>_. Structures_H.thread_state.BlockedOnSend epptr badge canGrant canGrantReply do_call) tcb)))) thread s \<longrightarrow> thread \<notin> set (ksReadyQueues s (d, p)))) s \<and> (valid_objs' and (\<lambda>s. \<forall>tcb. valid_tcb' tcb s \<longrightarrow> valid_tcb' (tcbState_update (\<lambda>_. Structures_H.thread_state.BlockedOnSend epptr badge canGrant canGrantReply do_call) tcb) s)) s)) s
 2. \<And>s. \<lbrakk>badge = badge && mask 28; epptr = epptr && ~~ mask 4; bos = ThreadState_BlockedOnSend \<and> epptr' = epptr \<and> badge' = badge \<and> cg = from_bool canGrant \<and> cgr = from_bool canGrantReply \<and> dc' = from_bool do_call; s \<in> UNIV\<rbrakk> \<Longrightarrow> s \<in> UNIV proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>badge = badge && mask 28; epptr = epptr && ~~ mask 4; bos = ThreadState_BlockedOnSend \<and> epptr' = epptr \<and> badge' = badge \<and> cg = from_bool canGrant \<and> cgr = from_bool canGrantReply \<and> dc' = from_bool do_call; s \<in> UNIV\<rbrakk> \<Longrightarrow> s \<in> UNIV proof (prove)
goal:
No subgoals!