theory Ipc_C

lemma receiveSignal_block_ccorres_helper:
  "ccorres dc xfdc (tcb_at' thread and valid_queues and sch_act_not thread and
                    valid_objs' and ntfn_at' ntfnptr and
                    (\<lambda>s. sch_act_wf (ksSchedulerAction s) s \<and>
                        (\<forall>d p. thread \<notin> set (ksReadyQueues s (d, p)))) and
                    K (ntfnptr = ntfnptr && ~~ mask 4))
                   UNIV hs
           (setThreadState (Structures_H.thread_state.BlockedOnNotification
                                ntfnptr) thread)
           (Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread}
             (CALL thread_state_ptr_set_tsType(Ptr
              &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C'']),
              scast ThreadState_BlockedOnNotification));;
            Guard C_Guard {s. s \<Turnstile>\<^sub>c tcb_ptr_to_ctcb_ptr thread}
             (CALL thread_state_ptr_set_blockingObject(Ptr
                           &(tcb_ptr_to_ctcb_ptr thread\<rightarrow>[''tcbState_C'']),
              ucast (ptr_val (ntfn_Ptr ntfnptr))));;
            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')+) apply (simp add: tcb_cte_cases_def) apply (simp add: ctcb_relation_def cthread_state_relation_def
                         ThreadState_BlockedOnNotification_def mask_def) apply ceqv apply clarsimp apply ctac apply (wp threadSet_valid_queues hoare_vcg_all_lift threadSet_valid_objs'
               threadSet_weak_sch_act_wf_runnable') apply (clarsimp simp: guard_is_UNIV_def) apply (auto simp: weak_sch_act_wf_def valid_tcb'_def tcb_cte_cases_def
                     valid_tcb_state'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres dc xfdc (tcb_at' thread and Invariants_H.valid_queues and sch_act_not thread and valid_objs' and ntfn_at' ntfnptr and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s \<and> (\<forall>d p. thread \<notin> set (ksReadyQueues s (d, p)))) and K (ntfnptr = ntfnptr && ~~ mask 4)) UNIV hs (setThreadState (Structures_H.thread_state.BlockedOnNotification ntfnptr) 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) ThreadState_BlockedOnNotification));;
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'']),UCAST(32 \<rightarrow> 32) (ptr_val (ntfn_Ptr ntfnptr))));;
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 sch_act_not thread and valid_objs' and ntfn_at' ntfnptr and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s \<and> (\<forall>d p. thread \<notin> set (ksReadyQueues s (d, p)))) and (\<lambda>y. ntfnptr = ntfnptr && ~~ mask 4)) UNIV hs (do threadSet (tcbState_update (\<lambda>_. Structures_H.thread_state.BlockedOnNotification ntfnptr)) 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) ThreadState_BlockedOnNotification));;
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'']),UCAST(32 \<rightarrow> 32) (ptr_val (ntfn_Ptr ntfnptr))));;
CALL scheduleTCB_'proc(tcb_ptr_to_ctcb_ptr thread)) proof (prove)
goal (1 subgoal):
 1. ntfnptr = ntfnptr && ~~ mask 4 \<Longrightarrow> ccorres dc xfdc (tcb_at' thread and Invariants_H.valid_queues and sch_act_not thread and valid_objs' and ntfn_at' ntfnptr 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.BlockedOnNotification ntfnptr)) 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) ThreadState_BlockedOnNotification));;
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'']),UCAST(32 \<rightarrow> 32) (ptr_val (ntfn_Ptr ntfnptr))));;
CALL scheduleTCB_'proc(tcb_ptr_to_ctcb_ptr thread)) proof (prove)
goal (3 subgoals):
 1. ntfnptr = ntfnptr && ~~ mask 4 \<Longrightarrow> ccorres dc xfdc ?Q1 ?Q'1 hs (do threadSet (tcbState_update (\<lambda>_. Structures_H.thread_state.BlockedOnNotification ntfnptr)) 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) ThreadState_BlockedOnNotification));;
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'']),UCAST(32 \<rightarrow> 32) (ptr_val (ntfn_Ptr ntfnptr))));;
CALL scheduleTCB_'proc(tcb_ptr_to_ctcb_ptr thread))
 2. \<And>s. \<lbrakk>ntfnptr = ntfnptr && ~~ mask 4; (tcb_at' thread and Invariants_H.valid_queues and sch_act_not thread and valid_objs' and ntfn_at' ntfnptr and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s \<and> (\<forall>d p. thread \<notin> set (ksReadyQueues s (d, p))))) s\<rbrakk> \<Longrightarrow> ?Q1 s
 3. \<And>s. \<lbrakk>ntfnptr = ntfnptr && ~~ mask 4; s \<in> UNIV\<rbrakk> \<Longrightarrow> s \<in> ?Q'1 proof (prove)
goal (7 subgoals):
 1. ntfnptr = ntfnptr && ~~ mask 4 \<Longrightarrow> ccorres ?r'5 ?xf'5 ?P5 ?Q'1 [] (threadSet (tcbState_update (\<lambda>_. Structures_H.thread_state.BlockedOnNotification ntfnptr)) 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) ThreadState_BlockedOnNotification));;
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'']),UCAST(32 \<rightarrow> 32) (ptr_val (ntfn_Ptr ntfnptr)))))
 2. \<And>rv' t t'. ntfnptr = ntfnptr && ~~ mask 4 \<Longrightarrow> ceqv \<Gamma> ?xf'5 rv' t t' (CALL scheduleTCB_'proc(tcb_ptr_to_ctcb_ptr thread)) (?d'5 rv')
 3. \<And>rv rv'. \<lbrakk>ntfnptr = ntfnptr && ~~ mask 4; ?r'5 rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q5 rv) (?Q'5 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'5 rv')
 4. ntfnptr = ntfnptr && ~~ mask 4 \<Longrightarrow> \<lbrace>?R5\<rbrace> threadSet (tcbState_update (\<lambda>_. Structures_H.thread_state.BlockedOnNotification ntfnptr)) thread \<lbrace>?Q5\<rbrace>
 5. ntfnptr = ntfnptr && ~~ mask 4 \<Longrightarrow> guard_is_UNIV ?r'5 ?xf'5 ?Q'5
 6. \<And>s. \<lbrakk>ntfnptr = ntfnptr && ~~ mask 4; (tcb_at' thread and Invariants_H.valid_queues and sch_act_not thread and valid_objs' and ntfn_at' ntfnptr and (\<lambda>s. sch_act_wf (ksSchedulerAction s) s \<and> (\<forall>d p. thread \<notin> set (ksReadyQueues s (d, p))))) s\<rbrakk> \<Longrightarrow> (?P5 and ?R5) s
 7. \<And>s. \<lbrakk>ntfnptr = ntfnptr && ~~ mask 4; s \<in> UNIV\<rbrakk> \<Longrightarrow> s \<in> ?Q'1 proof (prove)
goal (8 subgoals):
 1. \<And>s tcb. ntfnptr = ntfnptr && ~~ mask 4 \<Longrightarrow> \<Gamma>\<turnstile> (?Q11 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) ThreadState_BlockedOnNotification));;
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'']),UCAST(32 \<rightarrow> 32) (ptr_val (ntfn_Ptr ntfnptr)))) {s'. (s\<lparr>ksPSpace := (ksPSpace s)(thread \<mapsto> injectKOS (tcbState_update (\<lambda>_. Structures_H.thread_state.BlockedOnNotification ntfnptr) tcb))\<rparr>, s') \<in> rf_sr}
 2. \<And>s s' tcb tcb'. \<lbrakk>ntfnptr = ntfnptr && ~~ mask 4; (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> ?Q11 s tcb
 3. \<And>rv' t t'. ntfnptr = ntfnptr && ~~ mask 4 \<Longrightarrow> ceqv \<Gamma> xfdc rv' t t' (CALL scheduleTCB_'proc(tcb_ptr_to_ctcb_ptr thread)) (?d'5 rv')
 4. \<And>rv rv'. \<lbrakk>ntfnptr = ntfnptr && ~~ mask 4; dc rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q5 rv) (?Q'5 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'5 rv')
 5. ntfnptr = ntfnptr && ~~ mask 4 \<Longrightarrow> \<lbrace>?R5\<rbrace> threadSet (tcbState_update (\<lambda>_. Structures_H.thread_state.BlockedOnNotification ntfnptr)) thread \<lbrace>?Q5\<rbrace>
 6. ntfnptr = ntfnptr && ~~ mask 4 \<Longrightarrow> guard_is_UNIV dc xfdc ?Q'5
 7. \<And>s. \<lbrakk>ntfnptr = ntfnptr && ~~ mask 4; (tcb_at' thread and Invariants_H.valid_queues and sch_act_not thread and valid_objs' and ntfn_at' ntfnptr 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 ?R5) s
 8. \<And>s. \<lbrakk>ntfnptr = ntfnptr && ~~ mask 4; s \<in> UNIV\<rbrakk> \<Longrightarrow> s \<in> UNIV proof (prove)
goal (7 subgoals):
 1. \<And>s s' tcb tcb'. \<lbrakk>ntfnptr = ntfnptr && ~~ mask 4; (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) ThreadState_BlockedOnNotification && 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 := UCAST(32 \<rightarrow> 32) (ptr_val (ntfn_Ptr ntfnptr)) && ~~ 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> (s\<lparr>ksPSpace := (ksPSpace s)(thread \<mapsto> injectKOS (tcbState_update (\<lambda>_. Structures_H.thread_state.BlockedOnNotification ntfnptr) tcb))\<rparr>, sa\<lparr>globals := globals sa\<lparr>t_hrs_' := t_hrs_' (globals ta)\<rparr>\<rparr>) \<in> rf_sr))}
 2. \<And>rv' t t'. ntfnptr = ntfnptr && ~~ mask 4 \<Longrightarrow> ceqv \<Gamma> xfdc rv' t t' (CALL scheduleTCB_'proc(tcb_ptr_to_ctcb_ptr thread)) (?d'5 rv')
 3. \<And>rv rv'. \<lbrakk>ntfnptr = ntfnptr && ~~ mask 4; dc rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q5 rv) (?Q'5 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'5 rv')
 4. ntfnptr = ntfnptr && ~~ mask 4 \<Longrightarrow> \<lbrace>?R5\<rbrace> threadSet (tcbState_update (\<lambda>_. Structures_H.thread_state.BlockedOnNotification ntfnptr)) thread \<lbrace>?Q5\<rbrace>
 5. ntfnptr = ntfnptr && ~~ mask 4 \<Longrightarrow> guard_is_UNIV dc xfdc ?Q'5
 6. \<And>s. \<lbrakk>ntfnptr = ntfnptr && ~~ mask 4; (tcb_at' thread and Invariants_H.valid_queues and sch_act_not thread and valid_objs' and ntfn_at' ntfnptr 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 ?R5) s
 7. \<And>s. \<lbrakk>ntfnptr = ntfnptr && ~~ mask 4; s \<in> UNIV\<rbrakk> \<Longrightarrow> s \<in> UNIV proof (prove)
goal (7 subgoals):
 1. \<And>s s' tcb tcb'. \<lbrakk>ntfnptr = ntfnptr && ~~ 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\<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_BlockedOnNotification && 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 := ntfnptr\<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.BlockedOnNotification ntfnptr) tcb))\<rparr>, s'\<lparr>globals := globals s'\<lparr>t_hrs_' := t_hrs_' (globals ta)\<rparr>\<rparr>) \<in> rf_sr))
 2. \<And>rv' t t'. ntfnptr = ntfnptr && ~~ mask 4 \<Longrightarrow> ceqv \<Gamma> xfdc rv' t t' (CALL scheduleTCB_'proc(tcb_ptr_to_ctcb_ptr thread)) (?d'5 rv')
 3. \<And>rv rv'. \<lbrakk>ntfnptr = ntfnptr && ~~ mask 4; dc rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q5 rv) (?Q'5 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'5 rv')
 4. ntfnptr = ntfnptr && ~~ mask 4 \<Longrightarrow> \<lbrace>?R5\<rbrace> threadSet (tcbState_update (\<lambda>_. Structures_H.thread_state.BlockedOnNotification ntfnptr)) thread \<lbrace>?Q5\<rbrace>
 5. ntfnptr = ntfnptr && ~~ mask 4 \<Longrightarrow> guard_is_UNIV dc xfdc ?Q'5
 6. \<And>s. \<lbrakk>ntfnptr = ntfnptr && ~~ mask 4; (tcb_at' thread and Invariants_H.valid_queues and sch_act_not thread and valid_objs' and ntfn_at' ntfnptr 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 ?R5) s
 7. \<And>s. \<lbrakk>ntfnptr = ntfnptr && ~~ mask 4; s \<in> UNIV\<rbrakk> \<Longrightarrow> s \<in> UNIV proof (prove)
goal (7 subgoals):
 1. \<And>s s' tcb tcb'. \<lbrakk>ntfnptr = ntfnptr && ~~ 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; 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_BlockedOnNotification && 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 := ntfnptr\<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.BlockedOnNotification ntfnptr) tcb))\<rparr>, s'\<lparr>globals := globals s'\<lparr>t_hrs_' := t_hrs_' (globals ta)\<rparr>\<rparr>) \<in> rf_sr))
 2. \<And>rv' t t'. ntfnptr = ntfnptr && ~~ mask 4 \<Longrightarrow> ceqv \<Gamma> xfdc rv' t t' (CALL scheduleTCB_'proc(tcb_ptr_to_ctcb_ptr thread)) (?d'5 rv')
 3. \<And>rv rv'. \<lbrakk>ntfnptr = ntfnptr && ~~ mask 4; dc rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q5 rv) (?Q'5 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'5 rv')
 4. ntfnptr = ntfnptr && ~~ mask 4 \<Longrightarrow> \<lbrace>?R5\<rbrace> threadSet (tcbState_update (\<lambda>_. Structures_H.thread_state.BlockedOnNotification ntfnptr)) thread \<lbrace>?Q5\<rbrace>
 5. ntfnptr = ntfnptr && ~~ mask 4 \<Longrightarrow> guard_is_UNIV dc xfdc ?Q'5
 6. \<And>s. \<lbrakk>ntfnptr = ntfnptr && ~~ mask 4; (tcb_at' thread and Invariants_H.valid_queues and sch_act_not thread and valid_objs' and ntfn_at' ntfnptr 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 ?R5) s
 7. \<And>s. \<lbrakk>ntfnptr = ntfnptr && ~~ mask 4; s \<in> UNIV\<rbrakk> \<Longrightarrow> s \<in> UNIV proof (prove)
goal (7 subgoals):
 1. \<And>s s' tcb tcb'. \<lbrakk>ntfnptr = ntfnptr && ~~ 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; 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_BlockedOnNotification && 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 := ntfnptr\<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.BlockedOnNotification ntfnptr) tcb))\<rparr>, s'\<lparr>globals := globals s'\<lparr>t_hrs_' := t_hrs_' (globals ta)\<rparr>\<rparr>) \<in> rf_sr))
 2. \<And>rv' t t'. ntfnptr = ntfnptr && ~~ mask 4 \<Longrightarrow> ceqv \<Gamma> xfdc rv' t t' (CALL scheduleTCB_'proc(tcb_ptr_to_ctcb_ptr thread)) (?d'5 rv')
 3. \<And>rv rv'. \<lbrakk>ntfnptr = ntfnptr && ~~ mask 4; dc rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q5 rv) (?Q'5 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'5 rv')
 4. ntfnptr = ntfnptr && ~~ mask 4 \<Longrightarrow> \<lbrace>?R5\<rbrace> threadSet (tcbState_update (\<lambda>_. Structures_H.thread_state.BlockedOnNotification ntfnptr)) thread \<lbrace>?Q5\<rbrace>
 5. ntfnptr = ntfnptr && ~~ mask 4 \<Longrightarrow> guard_is_UNIV dc xfdc ?Q'5
 6. \<And>s. \<lbrakk>ntfnptr = ntfnptr && ~~ mask 4; (tcb_at' thread and Invariants_H.valid_queues and sch_act_not thread and valid_objs' and ntfn_at' ntfnptr 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 ?R5) s
 7. \<And>s. \<lbrakk>ntfnptr = ntfnptr && ~~ mask 4; 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. \<lbrakk>ntfnptr = ntfnptr && ~~ 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; thread_state_lift thread_state = thread_state_lift (tcbState_C tcb')\<lparr>tsType_CL := SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnNotification && 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_BlockedOnNotification && mask 4, blockingObject_CL := ntfnptr\<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')))\<rbrakk> \<Longrightarrow> (s\<lparr>ksPSpace := (ksPSpace s)(thread \<mapsto> KOTCB (tcbState_update (\<lambda>_. Structures_H.thread_state.BlockedOnNotification ntfnptr) 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_statea) tcb')) (t_hrs_' (globals s'))\<rparr>\<rparr>) \<in> rf_sr
 2. \<And>rv' t t'. ntfnptr = ntfnptr && ~~ mask 4 \<Longrightarrow> ceqv \<Gamma> xfdc rv' t t' (CALL scheduleTCB_'proc(tcb_ptr_to_ctcb_ptr thread)) (?d'5 rv')
 3. \<And>rv rv'. \<lbrakk>ntfnptr = ntfnptr && ~~ mask 4; dc rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q5 rv) (?Q'5 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'5 rv')
 4. ntfnptr = ntfnptr && ~~ mask 4 \<Longrightarrow> \<lbrace>?R5\<rbrace> threadSet (tcbState_update (\<lambda>_. Structures_H.thread_state.BlockedOnNotification ntfnptr)) thread \<lbrace>?Q5\<rbrace>
 5. ntfnptr = ntfnptr && ~~ mask 4 \<Longrightarrow> guard_is_UNIV dc xfdc ?Q'5
 6. \<And>s. \<lbrakk>ntfnptr = ntfnptr && ~~ mask 4; (tcb_at' thread and Invariants_H.valid_queues and sch_act_not thread and valid_objs' and ntfn_at' ntfnptr 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 ?R5) s
 7. \<And>s. \<lbrakk>ntfnptr = ntfnptr && ~~ mask 4; 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. \<lbrakk>ntfnptr = ntfnptr && ~~ 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; thread_state_lift thread_state = thread_state_lift (tcbState_C tcb')\<lparr>tsType_CL := SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnNotification && 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_BlockedOnNotification && mask 4, blockingObject_CL := ntfnptr\<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')))\<rbrakk> \<Longrightarrow> \<forall>x\<in>ran tcb_cte_cases. case x of (getF, setF) \<Rightarrow> getF (tcbState_update (\<lambda>_. Structures_H.thread_state.BlockedOnNotification ntfnptr) tcb) = getF tcb
 2. \<And>s s' tcb tcb' t thread_state ta thread_statea. \<lbrakk>ntfnptr = ntfnptr && ~~ 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; thread_state_lift thread_state = thread_state_lift (tcbState_C tcb')\<lparr>tsType_CL := SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnNotification && 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_BlockedOnNotification && mask 4, blockingObject_CL := ntfnptr\<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')))\<rbrakk> \<Longrightarrow> ctcb_relation (tcbState_update (\<lambda>_. Structures_H.thread_state.BlockedOnNotification ntfnptr) tcb) (tcbState_C_update (\<lambda>_. thread_statea) tcb')
 3. \<And>rv' t t'. ntfnptr = ntfnptr && ~~ mask 4 \<Longrightarrow> ceqv \<Gamma> xfdc rv' t t' (CALL scheduleTCB_'proc(tcb_ptr_to_ctcb_ptr thread)) (?d'5 rv')
 4. \<And>rv rv'. \<lbrakk>ntfnptr = ntfnptr && ~~ mask 4; dc rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q5 rv) (?Q'5 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'5 rv')
 5. ntfnptr = ntfnptr && ~~ mask 4 \<Longrightarrow> \<lbrace>?R5\<rbrace> threadSet (tcbState_update (\<lambda>_. Structures_H.thread_state.BlockedOnNotification ntfnptr)) thread \<lbrace>?Q5\<rbrace>
 6. ntfnptr = ntfnptr && ~~ mask 4 \<Longrightarrow> guard_is_UNIV dc xfdc ?Q'5
 7. \<And>s. \<lbrakk>ntfnptr = ntfnptr && ~~ mask 4; (tcb_at' thread and Invariants_H.valid_queues and sch_act_not thread and valid_objs' and ntfn_at' ntfnptr 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 ?R5) s
 8. \<And>s. \<lbrakk>ntfnptr = ntfnptr && ~~ mask 4; 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. \<lbrakk>ntfnptr = ntfnptr && ~~ 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; thread_state_lift thread_state = thread_state_lift (tcbState_C tcb')\<lparr>tsType_CL := SCAST(32 signed \<rightarrow> 32) ThreadState_BlockedOnNotification && 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_BlockedOnNotification && mask 4, blockingObject_CL := ntfnptr\<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')))\<rbrakk> \<Longrightarrow> ctcb_relation (tcbState_update (\<lambda>_. Structures_H.thread_state.BlockedOnNotification ntfnptr) tcb) (tcbState_C_update (\<lambda>_. thread_statea) tcb')
 2. \<And>rv' t t'. ntfnptr = ntfnptr && ~~ mask 4 \<Longrightarrow> ceqv \<Gamma> xfdc rv' t t' (CALL scheduleTCB_'proc(tcb_ptr_to_ctcb_ptr thread)) (?d'5 rv')
 3. \<And>rv rv'. \<lbrakk>ntfnptr = ntfnptr && ~~ mask 4; dc rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q5 rv) (?Q'5 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'5 rv')
 4. ntfnptr = ntfnptr && ~~ mask 4 \<Longrightarrow> \<lbrace>?R5\<rbrace> threadSet (tcbState_update (\<lambda>_. Structures_H.thread_state.BlockedOnNotification ntfnptr)) thread \<lbrace>?Q5\<rbrace>
 5. ntfnptr = ntfnptr && ~~ mask 4 \<Longrightarrow> guard_is_UNIV dc xfdc ?Q'5
 6. \<And>s. \<lbrakk>ntfnptr = ntfnptr && ~~ mask 4; (tcb_at' thread and Invariants_H.valid_queues and sch_act_not thread and valid_objs' and ntfn_at' ntfnptr 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 ?R5) s
 7. \<And>s. \<lbrakk>ntfnptr = ntfnptr && ~~ mask 4; s \<in> UNIV\<rbrakk> \<Longrightarrow> s \<in> UNIV proof (prove)
goal (6 subgoals):
 1. \<And>rv' t t'. ntfnptr = ntfnptr && ~~ mask 4 \<Longrightarrow> ceqv \<Gamma> xfdc rv' t t' (CALL scheduleTCB_'proc(tcb_ptr_to_ctcb_ptr thread)) (?d'5 rv')
 2. \<And>rv rv'. \<lbrakk>ntfnptr = ntfnptr && ~~ mask 4; dc rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q5 rv) (?Q'5 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'5 rv')
 3. ntfnptr = ntfnptr && ~~ mask 4 \<Longrightarrow> \<lbrace>?R5\<rbrace> threadSet (tcbState_update (\<lambda>_. Structures_H.thread_state.BlockedOnNotification ntfnptr)) thread \<lbrace>?Q5\<rbrace>
 4. ntfnptr = ntfnptr && ~~ mask 4 \<Longrightarrow> guard_is_UNIV dc xfdc ?Q'5
 5. \<And>s. \<lbrakk>ntfnptr = ntfnptr && ~~ mask 4; (tcb_at' thread and Invariants_H.valid_queues and sch_act_not thread and valid_objs' and ntfn_at' ntfnptr 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 ?R5) s
 6. \<And>s. \<lbrakk>ntfnptr = ntfnptr && ~~ mask 4; s \<in> UNIV\<rbrakk> \<Longrightarrow> s \<in> UNIV proof (prove)
goal (5 subgoals):
 1. \<And>rv rv'. \<lbrakk>ntfnptr = ntfnptr && ~~ mask 4; dc rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q5 rv) (?Q'5 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. ntfnptr = ntfnptr && ~~ mask 4 \<Longrightarrow> \<lbrace>?R5\<rbrace> threadSet (tcbState_update (\<lambda>_. Structures_H.thread_state.BlockedOnNotification ntfnptr)) thread \<lbrace>?Q5\<rbrace>
 3. ntfnptr = ntfnptr && ~~ mask 4 \<Longrightarrow> guard_is_UNIV dc xfdc ?Q'5
 4. \<And>s. \<lbrakk>ntfnptr = ntfnptr && ~~ mask 4; (tcb_at' thread and Invariants_H.valid_queues and sch_act_not thread and valid_objs' and ntfn_at' ntfnptr 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 ?R5) s
 5. \<And>s. \<lbrakk>ntfnptr = ntfnptr && ~~ mask 4; s \<in> UNIV\<rbrakk> \<Longrightarrow> s \<in> UNIV proof (prove)
goal (5 subgoals):
 1. \<And>rv'. ntfnptr = ntfnptr && ~~ mask 4 \<Longrightarrow> ccorres dc xfdc (?Q5 ()) (?Q'5 () 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. ntfnptr = ntfnptr && ~~ mask 4 \<Longrightarrow> \<lbrace>?R5\<rbrace> threadSet (tcbState_update (\<lambda>_. Structures_H.thread_state.BlockedOnNotification ntfnptr)) thread \<lbrace>?Q5\<rbrace>
 3. ntfnptr = ntfnptr && ~~ mask 4 \<Longrightarrow> guard_is_UNIV dc xfdc ?Q'5
 4. \<And>s. \<lbrakk>ntfnptr = ntfnptr && ~~ mask 4; (tcb_at' thread and Invariants_H.valid_queues and sch_act_not thread and valid_objs' and ntfn_at' ntfnptr 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 ?R5) s
 5. \<And>s. \<lbrakk>ntfnptr = ntfnptr && ~~ mask 4; s \<in> UNIV\<rbrakk> \<Longrightarrow> s \<in> UNIV proof (prove)
goal (4 subgoals):
 1. ntfnptr = ntfnptr && ~~ mask 4 \<Longrightarrow> \<lbrace>?R5\<rbrace> threadSet (tcbState_update (\<lambda>_. Structures_H.thread_state.BlockedOnNotification ntfnptr)) 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. ntfnptr = ntfnptr && ~~ mask 4 \<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>ntfnptr = ntfnptr && ~~ mask 4; (tcb_at' thread and Invariants_H.valid_queues and sch_act_not thread and valid_objs' and ntfn_at' ntfnptr 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 ?R5) s
 4. \<And>s. \<lbrakk>ntfnptr = ntfnptr && ~~ mask 4; s \<in> UNIV\<rbrakk> \<Longrightarrow> s \<in> UNIV proof (prove)
goal (3 subgoals):
 1. ntfnptr = ntfnptr && ~~ mask 4 \<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>ntfnptr = ntfnptr && ~~ mask 4; (tcb_at' thread and Invariants_H.valid_queues and sch_act_not thread and valid_objs' and ntfn_at' ntfnptr 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.BlockedOnNotification ntfnptr)) \<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.BlockedOnNotification ntfnptr) tcb) \<and> runnable' (tcbState (tcbState_update (\<lambda>_. Structures_H.thread_state.BlockedOnNotification ntfnptr) 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.BlockedOnNotification ntfnptr) tcb) \<and> runnable' (tcbState (tcbState_update (\<lambda>_. Structures_H.thread_state.BlockedOnNotification ntfnptr) 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.BlockedOnNotification ntfnptr) tcb) s)) s)) s
 3. \<And>s. \<lbrakk>ntfnptr = ntfnptr && ~~ mask 4; s \<in> UNIV\<rbrakk> \<Longrightarrow> s \<in> UNIV proof (prove)
goal (2 subgoals):
 1. \<And>s. \<lbrakk>ntfnptr = ntfnptr && ~~ mask 4; (tcb_at' thread and Invariants_H.valid_queues and sch_act_not thread and valid_objs' and ntfn_at' ntfnptr 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.BlockedOnNotification ntfnptr)) \<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.BlockedOnNotification ntfnptr) tcb) \<and> runnable' (tcbState (tcbState_update (\<lambda>_. Structures_H.thread_state.BlockedOnNotification ntfnptr) 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.BlockedOnNotification ntfnptr) tcb) \<and> runnable' (tcbState (tcbState_update (\<lambda>_. Structures_H.thread_state.BlockedOnNotification ntfnptr) 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.BlockedOnNotification ntfnptr) tcb) s)) s)) s
 2. \<And>s. \<lbrakk>ntfnptr = ntfnptr && ~~ mask 4; s \<in> UNIV\<rbrakk> \<Longrightarrow> s \<in> UNIV proof (prove)
goal:
No subgoals!