theory IpcCancel_C

lemma scheduleTCB_ccorres_valid_queues'_pre:
        "ccorresG rf_sr \<Gamma> dc xfdc (tcb_at' thread and st_tcb_at' (not runnable') thread and valid_queues' and valid_queues and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and valid_objs')
         (UNIV \<inter> \<lbrace>\<acute>tptr = tcb_ptr_to_ctcb_ptr thread\<rbrace>) []
         (do (runnable, curThread, action) \<leftarrow> do
             runnable \<leftarrow> isRunnable thread;
             curThread \<leftarrow> getCurThread;
             action \<leftarrow> getSchedulerAction;
             return (runnable, curThread, action) od;
             when (\<not> runnable \<and> curThread = thread \<and> action = ResumeCurrentThread) rescheduleRequired
          od)
         (Call scheduleTCB_'proc)" supply empty_fail_cond[simp] apply (cinit' lift: tptr_' simp del: word_neq_0_conv) apply (rule ccorres_rhs_assoc2)+ apply (rule_tac xf'="ret__int_'" in ccorres_split_nothrow_novcg) defer apply ceqv apply (unfold split_def)[1] apply (rule ccorres_when[where R=\<top>]) apply (intro allI impI) apply (unfold mem_simps)[1] apply assumption apply (ctac add: rescheduleRequired_ccorres) prefer 4 apply (rule ccorres_symb_exec_l) apply (rule ccorres_pre_getCurThread) apply (rule ccorres_symb_exec_l) apply (rule_tac P="\<lambda>s. st_tcb_at' (\<lambda>st. runnable' st = runnable) thread s
                                 \<and> curThread = ksCurThread s
                                 \<and> action = ksSchedulerAction s
                                 \<and> weak_sch_act_wf (ksSchedulerAction s) s"
                           and P'=UNIV in ccorres_from_vcg) apply (rule allI, rule conseqPre, vcg) apply (clarsimp simp: return_def if_1_0_0 split del: if_split) apply (clarsimp simp: from_bool_0 rf_sr_ksCurThread) apply (rule conjI) apply (clarsimp simp: st_tcb_at'_def) apply (drule (1) obj_at_cslift_tcb) apply (clarsimp simp: typ_heap_simps) apply (clarsimp simp: ctcb_relation_def cthread_state_relation_def weak_sch_act_wf_def) apply (case_tac "tcbState ko", simp_all add: "StrictC'_thread_state_defs")[1] apply (fold_subgoals (prefix))[6] subgoal premises prems using prems by (clarsimp simp: rf_sr_def cstate_relation_def Let_def
                                       cscheduler_action_relation_def
                                       tcb_at_not_NULL[OF obj_tcb_at'] st_tcb_at'_def
                                split: scheduler_action.split_asm)+ apply (clarsimp simp: rf_sr_def cstate_relation_def cscheduler_action_relation_def
                           split: scheduler_action.split_asm) apply wp+ apply (simp add: isRunnable_def isStopped_def) apply wp apply (simp add: guard_is_UNIV_def) apply (clarsimp simp: st_tcb_at'_def obj_at'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres dc xfdc (tcb_at' thread and st_tcb_at' (not runnable') thread and valid_queues' and Invariants_H.valid_queues and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and valid_objs') (UNIV \<inter> \<lbrace>\<acute>tptr = tcb_ptr_to_ctcb_ptr thread\<rbrace>) [] (do (runnable, curThread, action) <- do runnable <- isRunnable thread;
curThread <- getCurThread;
action <- getSchedulerAction;
return (runnable, curThread, action)
od;
when (\<not> runnable \<and> curThread = thread \<and> action = ResumeCurrentThread) rescheduleRequired
od) (Call scheduleTCB_'proc) proof (prove)
goal (1 subgoal):
 1. ccorres dc xfdc (tcb_at' thread and st_tcb_at' (not runnable') thread and valid_queues' and Invariants_H.valid_queues and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and valid_objs') (UNIV \<inter> \<lbrace>\<acute>tptr = tcb_ptr_to_ctcb_ptr thread\<rbrace>) [] (do (runnable, curThread, action) <- do runnable <- isRunnable thread;
curThread <- getCurThread;
action <- getSchedulerAction;
return (runnable, curThread, action)
od;
when (\<not> runnable \<and> curThread = thread \<and> action = ResumeCurrentThread) rescheduleRequired
od) (Call scheduleTCB_'proc) proof (prove)
goal (2 subgoals):
 1. \<And>tptr. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> ccorres dc xfdc (?Q157 tptr) (?Q'157 tptr) [SKIP] (do (runnable, curThread, action) <- do runnable <- isRunnable thread;
curThread <- getCurThread;
action <- getSchedulerAction;
return (runnable, curThread, action)
od;
when (\<not> runnable \<and> curThread = thread \<and> action = ResumeCurrentThread) rescheduleRequired
od) (\<acute>ret__int :== (if tptr = \<acute>ksCurThread then 1 else 0);;
(IF \<acute>ret__int \<noteq> 0 THEN
  \<acute>ret__int :== (if \<acute>ksSchedulerAction = NULL then 1 else 0)
FI;;
(IF \<acute>ret__int \<noteq> 0 THEN
  \<acute>ret__unsigned_long :== CALL isRunnable_'proc(tptr);;
\<acute>ret__int :== (if \<acute>ret__unsigned_long = 0 then 1 else 0)
FI;;
IF \<acute>ret__int \<noteq> 0 THEN
  CALL rescheduleRequired_'proc()
FI)))
 2. \<And>tptr s s'. \<lbrakk>tptr = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; (tcb_at' thread and st_tcb_at' (not runnable') thread and valid_queues' and Invariants_H.valid_queues and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and valid_objs') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q157 tptr s \<and> s' \<in> ?Q'157 tptr proof (prove)
goal (2 subgoals):
 1. \<And>tptr. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> ccorres dc xfdc (?Q157 tptr) (?Q'157 tptr) [SKIP] (do (runnable, curThread, action) <- do runnable <- isRunnable thread;
curThread <- getCurThread;
action <- getSchedulerAction;
return (runnable, curThread, action)
od;
when (\<not> runnable \<and> curThread = thread \<and> action = ResumeCurrentThread) rescheduleRequired
od) (\<acute>ret__int :== (if tptr = \<acute>ksCurThread then 1 else 0);;
IF \<acute>ret__int \<noteq> 0 THEN
  \<acute>ret__int :== (if \<acute>ksSchedulerAction = NULL then 1 else 0)
FI;;
IF \<acute>ret__int \<noteq> 0 THEN
  \<acute>ret__unsigned_long :== CALL isRunnable_'proc(tptr);;
\<acute>ret__int :== (if \<acute>ret__unsigned_long = 0 then 1 else 0)
FI;;
IF \<acute>ret__int \<noteq> 0 THEN
  CALL rescheduleRequired_'proc()
FI)
 2. \<And>tptr s s'. \<lbrakk>tptr = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; (tcb_at' thread and st_tcb_at' (not runnable') thread and valid_queues' and Invariants_H.valid_queues and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and valid_objs') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ?Q157 tptr s \<and> s' \<in> ?Q'157 tptr proof (prove)
goal (6 subgoals):
 1. \<And>tptr. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> ccorres (?r'167 tptr) ret__int_' (?P167 tptr) (?Q'157 tptr) [] (do runnable <- isRunnable thread;
curThread <- getCurThread;
action <- getSchedulerAction;
return (runnable, curThread, action)
od) (\<acute>ret__int :== (if tptr = \<acute>ksCurThread then 1 else 0);;
IF \<acute>ret__int \<noteq> 0 THEN
  \<acute>ret__int :== (if \<acute>ksSchedulerAction = NULL then 1 else 0)
FI;;
IF \<acute>ret__int \<noteq> 0 THEN
  \<acute>ret__unsigned_long :== CALL isRunnable_'proc(tptr);;
\<acute>ret__int :== (if \<acute>ret__unsigned_long = 0 then 1 else 0)
FI)
 2. \<And>tptr rv' t t'. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> ceqv \<Gamma> ret__int_' rv' t t' (IF \<acute>ret__int \<noteq> 0 THEN
  CALL rescheduleRequired_'proc()
FI) (?d'167 tptr rv')
 3. \<And>tptr rv rv'. \<lbrakk>tptr = tcb_ptr_to_ctcb_ptr thread; ?r'167 tptr rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q167 tptr rv) (?Q'167 tptr rv rv') [SKIP] (case rv of (runnable, curThread, action) \<Rightarrow> when (\<not> runnable \<and> curThread = thread \<and> action = ResumeCurrentThread) rescheduleRequired) (?d'167 tptr rv')
 4. \<And>tptr. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<lbrace>?R167 tptr\<rbrace> do runnable <- isRunnable thread;
curThread <- getCurThread;
action <- getSchedulerAction;
return (runnable, curThread, action)
od \<lbrace>?Q167 tptr\<rbrace>
 5. \<And>tptr. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> guard_is_UNIV (?r'167 tptr) ret__int_' (?Q'167 tptr)
 6. \<And>tptr s s'. \<lbrakk>tptr = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; (tcb_at' thread and st_tcb_at' (not runnable') thread and valid_queues' and Invariants_H.valid_queues and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and valid_objs') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (?P167 tptr and ?R167 tptr) s \<and> s' \<in> ?Q'157 tptr proof (prove)
goal (6 subgoals):
 1. \<And>tptr rv' t t'. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> ceqv \<Gamma> ret__int_' rv' t t' (IF \<acute>ret__int \<noteq> 0 THEN
  CALL rescheduleRequired_'proc()
FI) (?d'167 tptr rv')
 2. \<And>tptr rv rv'. \<lbrakk>tptr = tcb_ptr_to_ctcb_ptr thread; ?r'167 tptr rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q167 tptr rv) (?Q'167 tptr rv rv') [SKIP] (case rv of (runnable, curThread, action) \<Rightarrow> when (\<not> runnable \<and> curThread = thread \<and> action = ResumeCurrentThread) rescheduleRequired) (?d'167 tptr rv')
 3. \<And>tptr. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<lbrace>?R167 tptr\<rbrace> do runnable <- isRunnable thread;
curThread <- getCurThread;
action <- getSchedulerAction;
return (runnable, curThread, action)
od \<lbrace>?Q167 tptr\<rbrace>
 4. \<And>tptr. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> guard_is_UNIV (?r'167 tptr) ret__int_' (?Q'167 tptr)
 5. \<And>tptr s s'. \<lbrakk>tptr = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; (tcb_at' thread and st_tcb_at' (not runnable') thread and valid_queues' and Invariants_H.valid_queues and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and valid_objs') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (?P167 tptr and ?R167 tptr) s \<and> s' \<in> ?Q'157 tptr
 6. \<And>tptr. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> ccorres (?r'167 tptr) ret__int_' (?P167 tptr) (?Q'157 tptr) [] (do runnable <- isRunnable thread;
curThread <- getCurThread;
action <- getSchedulerAction;
return (runnable, curThread, action)
od) (\<acute>ret__int :== (if tptr = \<acute>ksCurThread then 1 else 0);;
IF \<acute>ret__int \<noteq> 0 THEN
  \<acute>ret__int :== (if \<acute>ksSchedulerAction = NULL then 1 else 0)
FI;;
IF \<acute>ret__int \<noteq> 0 THEN
  \<acute>ret__unsigned_long :== CALL isRunnable_'proc(tptr);;
\<acute>ret__int :== (if \<acute>ret__unsigned_long = 0 then 1 else 0)
FI) proof (prove)
goal (5 subgoals):
 1. \<And>tptr rv rv'. \<lbrakk>tptr = tcb_ptr_to_ctcb_ptr thread; ?r'167 tptr rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q167 tptr rv) (?Q'167 tptr rv rv') [SKIP] (case rv of (runnable, curThread, action) \<Rightarrow> when (\<not> runnable \<and> curThread = thread \<and> action = ResumeCurrentThread) rescheduleRequired) (IF rv' \<noteq> 0 THEN
  CALL rescheduleRequired_'proc()
FI)
 2. \<And>tptr. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<lbrace>?R167 tptr\<rbrace> do runnable <- isRunnable thread;
curThread <- getCurThread;
action <- getSchedulerAction;
return (runnable, curThread, action)
od \<lbrace>?Q167 tptr\<rbrace>
 3. \<And>tptr. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> guard_is_UNIV (?r'167 tptr) ret__int_' (?Q'167 tptr)
 4. \<And>tptr s s'. \<lbrakk>tptr = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; (tcb_at' thread and st_tcb_at' (not runnable') thread and valid_queues' and Invariants_H.valid_queues and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and valid_objs') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (?P167 tptr and ?R167 tptr) s \<and> s' \<in> ?Q'157 tptr
 5. \<And>tptr. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> ccorres (?r'167 tptr) ret__int_' (?P167 tptr) (?Q'157 tptr) [] (do runnable <- isRunnable thread;
curThread <- getCurThread;
action <- getSchedulerAction;
return (runnable, curThread, action)
od) (\<acute>ret__int :== (if tptr = \<acute>ksCurThread then 1 else 0);;
IF \<acute>ret__int \<noteq> 0 THEN
  \<acute>ret__int :== (if \<acute>ksSchedulerAction = NULL then 1 else 0)
FI;;
IF \<acute>ret__int \<noteq> 0 THEN
  \<acute>ret__unsigned_long :== CALL isRunnable_'proc(tptr);;
\<acute>ret__int :== (if \<acute>ret__unsigned_long = 0 then 1 else 0)
FI) proof (prove)
goal (5 subgoals):
 1. \<And>tptr rv rv'. \<lbrakk>tptr = tcb_ptr_to_ctcb_ptr thread; ?r'167 tptr rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Q167 tptr rv) (?Q'167 tptr rv rv') [SKIP] (when (\<not> fst rv \<and> fst (snd rv) = thread \<and> snd (snd rv) = ResumeCurrentThread) rescheduleRequired) (IF rv' \<noteq> 0 THEN
  CALL rescheduleRequired_'proc()
FI)
 2. \<And>tptr. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<lbrace>?R167 tptr\<rbrace> do runnable <- isRunnable thread;
curThread <- getCurThread;
action <- getSchedulerAction;
return (runnable, curThread, action)
od \<lbrace>?Q167 tptr\<rbrace>
 3. \<And>tptr. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> guard_is_UNIV (?r'167 tptr) ret__int_' (?Q'167 tptr)
 4. \<And>tptr s s'. \<lbrakk>tptr = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; (tcb_at' thread and st_tcb_at' (not runnable') thread and valid_queues' and Invariants_H.valid_queues and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and valid_objs') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (?P167 tptr and ?R167 tptr) s \<and> s' \<in> ?Q'157 tptr
 5. \<And>tptr. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> ccorres (?r'167 tptr) ret__int_' (?P167 tptr) (?Q'157 tptr) [] (do runnable <- isRunnable thread;
curThread <- getCurThread;
action <- getSchedulerAction;
return (runnable, curThread, action)
od) (\<acute>ret__int :== (if tptr = \<acute>ksCurThread then 1 else 0);;
IF \<acute>ret__int \<noteq> 0 THEN
  \<acute>ret__int :== (if \<acute>ksSchedulerAction = NULL then 1 else 0)
FI;;
IF \<acute>ret__int \<noteq> 0 THEN
  \<acute>ret__unsigned_long :== CALL isRunnable_'proc(tptr);;
\<acute>ret__int :== (if \<acute>ret__unsigned_long = 0 then 1 else 0)
FI) proof (prove)
goal (6 subgoals):
 1. \<And>tptr rv rv'. \<lbrakk>tptr = tcb_ptr_to_ctcb_ptr thread; ?r'167 tptr rv rv'\<rbrakk> \<Longrightarrow> \<forall>s s'. (s, s') \<in> rf_sr \<and> True \<longrightarrow> (\<not> fst rv \<and> fst (snd rv) = thread \<and> snd (snd rv) = ResumeCurrentThread) = (s' \<in> \<lbrace>rv' \<noteq> 0\<rbrace>)
 2. \<And>tptr rv rv'. \<lbrakk>tptr = tcb_ptr_to_ctcb_ptr thread; ?r'167 tptr rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Pt210 tptr rv) (?Rt208 tptr rv rv') [SKIP] rescheduleRequired (CALL rescheduleRequired_'proc())
 3. \<And>tptr. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<lbrace>?R167 tptr\<rbrace> do runnable <- isRunnable thread;
curThread <- getCurThread;
action <- getSchedulerAction;
return (runnable, curThread, action)
od \<lbrace>\<lambda>rv. (\<lambda>_. True) and (\<lambda>s. \<not> fst rv \<and> fst (snd rv) = thread \<and> snd (snd rv) = ResumeCurrentThread \<longrightarrow> ?Pt210 tptr rv s) and (\<lambda>s. \<not> (\<not> fst rv \<and> fst (snd rv) = thread \<and> snd (snd rv) = ResumeCurrentThread) \<longrightarrow> True)\<rbrace>
 4. \<And>tptr. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> guard_is_UNIV (?r'167 tptr) ret__int_' (\<lambda>rv rv'. {s. (s \<in> \<lbrace>rv' \<noteq> 0\<rbrace> \<longrightarrow> s \<in> ?Rt208 tptr rv rv') \<and> (s \<notin> \<lbrace>rv' \<noteq> 0\<rbrace> \<longrightarrow> s \<in> UNIV)})
 5. \<And>tptr s s'. \<lbrakk>tptr = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; (tcb_at' thread and st_tcb_at' (not runnable') thread and valid_queues' and Invariants_H.valid_queues and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and valid_objs') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (?P167 tptr and ?R167 tptr) s \<and> s' \<in> ?Q'157 tptr
 6. \<And>tptr. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> ccorres (?r'167 tptr) ret__int_' (?P167 tptr) (?Q'157 tptr) [] (do runnable <- isRunnable thread;
curThread <- getCurThread;
action <- getSchedulerAction;
return (runnable, curThread, action)
od) (\<acute>ret__int :== (if tptr = \<acute>ksCurThread then 1 else 0);;
IF \<acute>ret__int \<noteq> 0 THEN
  \<acute>ret__int :== (if \<acute>ksSchedulerAction = NULL then 1 else 0)
FI;;
IF \<acute>ret__int \<noteq> 0 THEN
  \<acute>ret__unsigned_long :== CALL isRunnable_'proc(tptr);;
\<acute>ret__int :== (if \<acute>ret__unsigned_long = 0 then 1 else 0)
FI) proof (prove)
goal (6 subgoals):
 1. \<And>tptr rv rv' s s'. \<lbrakk>tptr = tcb_ptr_to_ctcb_ptr thread; ?r'167 tptr rv rv'; (s, s') \<in> rf_sr \<and> True\<rbrakk> \<Longrightarrow> (\<not> fst rv \<and> fst (snd rv) = thread \<and> snd (snd rv) = ResumeCurrentThread) = (s' \<in> \<lbrace>rv' \<noteq> 0\<rbrace>)
 2. \<And>tptr rv rv'. \<lbrakk>tptr = tcb_ptr_to_ctcb_ptr thread; ?r'167 tptr rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Pt210 tptr rv) (?Rt208 tptr rv rv') [SKIP] rescheduleRequired (CALL rescheduleRequired_'proc())
 3. \<And>tptr. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<lbrace>?R167 tptr\<rbrace> do runnable <- isRunnable thread;
curThread <- getCurThread;
action <- getSchedulerAction;
return (runnable, curThread, action)
od \<lbrace>\<lambda>rv. (\<lambda>_. True) and (\<lambda>s. \<not> fst rv \<and> fst (snd rv) = thread \<and> snd (snd rv) = ResumeCurrentThread \<longrightarrow> ?Pt210 tptr rv s) and (\<lambda>s. \<not> (\<not> fst rv \<and> fst (snd rv) = thread \<and> snd (snd rv) = ResumeCurrentThread) \<longrightarrow> True)\<rbrace>
 4. \<And>tptr. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> guard_is_UNIV (?r'167 tptr) ret__int_' (\<lambda>rv rv'. {s. (s \<in> \<lbrace>rv' \<noteq> 0\<rbrace> \<longrightarrow> s \<in> ?Rt208 tptr rv rv') \<and> (s \<notin> \<lbrace>rv' \<noteq> 0\<rbrace> \<longrightarrow> s \<in> UNIV)})
 5. \<And>tptr s s'. \<lbrakk>tptr = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; (tcb_at' thread and st_tcb_at' (not runnable') thread and valid_queues' and Invariants_H.valid_queues and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and valid_objs') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (?P167 tptr and ?R167 tptr) s \<and> s' \<in> ?Q'157 tptr
 6. \<And>tptr. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> ccorres (?r'167 tptr) ret__int_' (?P167 tptr) (?Q'157 tptr) [] (do runnable <- isRunnable thread;
curThread <- getCurThread;
action <- getSchedulerAction;
return (runnable, curThread, action)
od) (\<acute>ret__int :== (if tptr = \<acute>ksCurThread then 1 else 0);;
IF \<acute>ret__int \<noteq> 0 THEN
  \<acute>ret__int :== (if \<acute>ksSchedulerAction = NULL then 1 else 0)
FI;;
IF \<acute>ret__int \<noteq> 0 THEN
  \<acute>ret__unsigned_long :== CALL isRunnable_'proc(tptr);;
\<acute>ret__int :== (if \<acute>ret__unsigned_long = 0 then 1 else 0)
FI) proof (prove)
goal (6 subgoals):
 1. \<And>tptr rv rv' s s'. \<lbrakk>tptr = tcb_ptr_to_ctcb_ptr thread; ?r'167 tptr rv rv'; (s, s') \<in> rf_sr \<and> True\<rbrakk> \<Longrightarrow> (\<not> fst rv \<and> fst (snd rv) = thread \<and> snd (snd rv) = ResumeCurrentThread) = (rv' \<noteq> 0)
 2. \<And>tptr rv rv'. \<lbrakk>tptr = tcb_ptr_to_ctcb_ptr thread; ?r'167 tptr rv rv'\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Pt210 tptr rv) (?Rt208 tptr rv rv') [SKIP] rescheduleRequired (CALL rescheduleRequired_'proc())
 3. \<And>tptr. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<lbrace>?R167 tptr\<rbrace> do runnable <- isRunnable thread;
curThread <- getCurThread;
action <- getSchedulerAction;
return (runnable, curThread, action)
od \<lbrace>\<lambda>rv. (\<lambda>_. True) and (\<lambda>s. \<not> fst rv \<and> fst (snd rv) = thread \<and> snd (snd rv) = ResumeCurrentThread \<longrightarrow> ?Pt210 tptr rv s) and (\<lambda>s. \<not> (\<not> fst rv \<and> fst (snd rv) = thread \<and> snd (snd rv) = ResumeCurrentThread) \<longrightarrow> True)\<rbrace>
 4. \<And>tptr. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> guard_is_UNIV (?r'167 tptr) ret__int_' (\<lambda>rv rv'. {s. (s \<in> \<lbrace>rv' \<noteq> 0\<rbrace> \<longrightarrow> s \<in> ?Rt208 tptr rv rv') \<and> (s \<notin> \<lbrace>rv' \<noteq> 0\<rbrace> \<longrightarrow> s \<in> UNIV)})
 5. \<And>tptr s s'. \<lbrakk>tptr = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; (tcb_at' thread and st_tcb_at' (not runnable') thread and valid_queues' and Invariants_H.valid_queues and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and valid_objs') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (?P167 tptr and ?R167 tptr) s \<and> s' \<in> ?Q'157 tptr
 6. \<And>tptr. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> ccorres (?r'167 tptr) ret__int_' (?P167 tptr) (?Q'157 tptr) [] (do runnable <- isRunnable thread;
curThread <- getCurThread;
action <- getSchedulerAction;
return (runnable, curThread, action)
od) (\<acute>ret__int :== (if tptr = \<acute>ksCurThread then 1 else 0);;
IF \<acute>ret__int \<noteq> 0 THEN
  \<acute>ret__int :== (if \<acute>ksSchedulerAction = NULL then 1 else 0)
FI;;
IF \<acute>ret__int \<noteq> 0 THEN
  \<acute>ret__unsigned_long :== CALL isRunnable_'proc(tptr);;
\<acute>ret__int :== (if \<acute>ret__unsigned_long = 0 then 1 else 0)
FI) proof (prove)
goal (5 subgoals):
 1. \<And>tptr rv rv'. \<lbrakk>tptr = tcb_ptr_to_ctcb_ptr thread; (\<not> fst rv \<and> fst (snd rv) = thread \<and> snd (snd rv) = ResumeCurrentThread) = (rv' \<noteq> 0)\<rbrakk> \<Longrightarrow> ccorres dc xfdc (?Pt210 tptr rv) (?Rt208 tptr rv rv') [SKIP] rescheduleRequired (CALL rescheduleRequired_'proc())
 2. \<And>tptr. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<lbrace>?R167 tptr\<rbrace> do runnable <- isRunnable thread;
curThread <- getCurThread;
action <- getSchedulerAction;
return (runnable, curThread, action)
od \<lbrace>\<lambda>rv. (\<lambda>_. True) and (\<lambda>s. \<not> fst rv \<and> fst (snd rv) = thread \<and> snd (snd rv) = ResumeCurrentThread \<longrightarrow> ?Pt210 tptr rv s) and (\<lambda>s. \<not> (\<not> fst rv \<and> fst (snd rv) = thread \<and> snd (snd rv) = ResumeCurrentThread) \<longrightarrow> True)\<rbrace>
 3. \<And>tptr. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> guard_is_UNIV (\<lambda>rv rv'. (\<not> fst rv \<and> fst (snd rv) = thread \<and> snd (snd rv) = ResumeCurrentThread) = (rv' \<noteq> 0)) ret__int_' (\<lambda>rv rv'. {s. (s \<in> \<lbrace>rv' \<noteq> 0\<rbrace> \<longrightarrow> s \<in> ?Rt208 tptr rv rv') \<and> (s \<notin> \<lbrace>rv' \<noteq> 0\<rbrace> \<longrightarrow> s \<in> UNIV)})
 4. \<And>tptr s s'. \<lbrakk>tptr = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; (tcb_at' thread and st_tcb_at' (not runnable') thread and valid_queues' and Invariants_H.valid_queues and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and valid_objs') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (?P167 tptr and ?R167 tptr) s \<and> s' \<in> ?Q'157 tptr
 5. \<And>tptr. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> ccorres (\<lambda>rv rv'. (\<not> fst rv \<and> fst (snd rv) = thread \<and> snd (snd rv) = ResumeCurrentThread) = (rv' \<noteq> 0)) ret__int_' (?P167 tptr) (?Q'157 tptr) [] (do runnable <- isRunnable thread;
curThread <- getCurThread;
action <- getSchedulerAction;
return (runnable, curThread, action)
od) (\<acute>ret__int :== (if tptr = \<acute>ksCurThread then 1 else 0);;
IF \<acute>ret__int \<noteq> 0 THEN
  \<acute>ret__int :== (if \<acute>ksSchedulerAction = NULL then 1 else 0)
FI;;
IF \<acute>ret__int \<noteq> 0 THEN
  \<acute>ret__unsigned_long :== CALL isRunnable_'proc(tptr);;
\<acute>ret__int :== (if \<acute>ret__unsigned_long = 0 then 1 else 0)
FI) proof (prove)
goal (4 subgoals):
 1. \<And>tptr. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<lbrace>?R167 tptr\<rbrace> do runnable <- isRunnable thread;
curThread <- getCurThread;
action <- getSchedulerAction;
return (runnable, curThread, action)
od \<lbrace>\<lambda>rv. (\<lambda>_. True) and (\<lambda>s. \<not> fst rv \<and> fst (snd rv) = thread \<and> snd (snd rv) = ResumeCurrentThread \<longrightarrow> (Invariants_H.valid_queues and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and valid_objs') s) and (\<lambda>s. \<not> (\<not> fst rv \<and> fst (snd rv) = thread \<and> snd (snd rv) = ResumeCurrentThread) \<longrightarrow> True)\<rbrace>
 2. \<And>tptr. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> guard_is_UNIV (\<lambda>rv rv'. (\<not> fst rv \<and> fst (snd rv) = thread \<and> snd (snd rv) = ResumeCurrentThread) = (rv' \<noteq> 0)) ret__int_' (\<lambda>rv rv'. {s. (s \<in> \<lbrace>rv' \<noteq> 0\<rbrace> \<longrightarrow> s \<in> {s. s \<in> UNIV}) \<and> (s \<notin> \<lbrace>rv' \<noteq> 0\<rbrace> \<longrightarrow> s \<in> UNIV)})
 3. \<And>tptr s s'. \<lbrakk>tptr = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; (tcb_at' thread and st_tcb_at' (not runnable') thread and valid_queues' and Invariants_H.valid_queues and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and valid_objs') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (?P167 tptr and ?R167 tptr) s \<and> s' \<in> ?Q'157 tptr
 4. \<And>tptr. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> ccorres (\<lambda>rv rv'. (\<not> fst rv \<and> fst (snd rv) = thread \<and> snd (snd rv) = ResumeCurrentThread) = (rv' \<noteq> 0)) ret__int_' (?P167 tptr) (?Q'157 tptr) [] (do runnable <- isRunnable thread;
curThread <- getCurThread;
action <- getSchedulerAction;
return (runnable, curThread, action)
od) (\<acute>ret__int :== (if tptr = \<acute>ksCurThread then 1 else 0);;
IF \<acute>ret__int \<noteq> 0 THEN
  \<acute>ret__int :== (if \<acute>ksSchedulerAction = NULL then 1 else 0)
FI;;
IF \<acute>ret__int \<noteq> 0 THEN
  \<acute>ret__unsigned_long :== CALL isRunnable_'proc(tptr);;
\<acute>ret__int :== (if \<acute>ret__unsigned_long = 0 then 1 else 0)
FI) proof (prove)
goal (4 subgoals):
 1. \<And>tptr. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> ccorres (\<lambda>rv rv'. (\<not> fst rv \<and> fst (snd rv) = thread \<and> snd (snd rv) = ResumeCurrentThread) = (rv' \<noteq> 0)) ret__int_' (?P167 tptr) (?Q'157 tptr) [] (do runnable <- isRunnable thread;
curThread <- getCurThread;
action <- getSchedulerAction;
return (runnable, curThread, action)
od) (\<acute>ret__int :== (if tptr = \<acute>ksCurThread then 1 else 0);;
IF \<acute>ret__int \<noteq> 0 THEN
  \<acute>ret__int :== (if \<acute>ksSchedulerAction = NULL then 1 else 0)
FI;;
IF \<acute>ret__int \<noteq> 0 THEN
  \<acute>ret__unsigned_long :== CALL isRunnable_'proc(tptr);;
\<acute>ret__int :== (if \<acute>ret__unsigned_long = 0 then 1 else 0)
FI)
 2. \<And>tptr. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<lbrace>?R167 tptr\<rbrace> do runnable <- isRunnable thread;
curThread <- getCurThread;
action <- getSchedulerAction;
return (runnable, curThread, action)
od \<lbrace>\<lambda>rv. (\<lambda>_. True) and (\<lambda>s. \<not> fst rv \<and> fst (snd rv) = thread \<and> snd (snd rv) = ResumeCurrentThread \<longrightarrow> (Invariants_H.valid_queues and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and valid_objs') s) and (\<lambda>s. \<not> (\<not> fst rv \<and> fst (snd rv) = thread \<and> snd (snd rv) = ResumeCurrentThread) \<longrightarrow> True)\<rbrace>
 3. \<And>tptr. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> guard_is_UNIV (\<lambda>rv rv'. (\<not> fst rv \<and> fst (snd rv) = thread \<and> snd (snd rv) = ResumeCurrentThread) = (rv' \<noteq> 0)) ret__int_' (\<lambda>rv rv'. {s. (s \<in> \<lbrace>rv' \<noteq> 0\<rbrace> \<longrightarrow> s \<in> {s. s \<in> UNIV}) \<and> (s \<notin> \<lbrace>rv' \<noteq> 0\<rbrace> \<longrightarrow> s \<in> UNIV)})
 4. \<And>tptr s s'. \<lbrakk>tptr = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; (tcb_at' thread and st_tcb_at' (not runnable') thread and valid_queues' and Invariants_H.valid_queues and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and valid_objs') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (?P167 tptr and ?R167 tptr) s \<and> s' \<in> ?Q'157 tptr proof (prove)
goal (7 subgoals):
 1. \<And>tptr runnable. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> ccorres (\<lambda>rv rv'. (\<not> fst rv \<and> fst (snd rv) = thread \<and> snd (snd rv) = ResumeCurrentThread) = (rv' \<noteq> 0)) ret__int_' (?Q226 tptr runnable) (?Q'226 tptr runnable) [] (do curThread <- getCurThread;
action <- getSchedulerAction;
return (runnable, curThread, action)
od) (\<acute>ret__int :== (if tptr = \<acute>ksCurThread then 1 else 0);;
IF \<acute>ret__int \<noteq> 0 THEN
  \<acute>ret__int :== (if \<acute>ksSchedulerAction = NULL then 1 else 0)
FI;;
IF \<acute>ret__int \<noteq> 0 THEN
  \<acute>ret__unsigned_long :== CALL isRunnable_'proc(tptr);;
\<acute>ret__int :== (if \<acute>ret__unsigned_long = 0 then 1 else 0)
FI)
 2. \<And>tptr s. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<lbrace>(=) s\<rbrace> isRunnable thread \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<And>tptr. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<lbrace>?P167 tptr\<rbrace> isRunnable thread \<lbrace>?Q226 tptr\<rbrace>
 4. \<And>tptr. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> empty_fail (isRunnable thread)
 5. \<And>tptr. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<lbrace>?R167 tptr\<rbrace> do runnable <- isRunnable thread;
curThread <- getCurThread;
action <- getSchedulerAction;
return (runnable, curThread, action)
od \<lbrace>\<lambda>rv. (\<lambda>_. True) and (\<lambda>s. \<not> fst rv \<and> fst (snd rv) = thread \<and> snd (snd rv) = ResumeCurrentThread \<longrightarrow> (Invariants_H.valid_queues and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and valid_objs') s) and (\<lambda>s. \<not> (\<not> fst rv \<and> fst (snd rv) = thread \<and> snd (snd rv) = ResumeCurrentThread) \<longrightarrow> True)\<rbrace>
 6. \<And>tptr. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> guard_is_UNIV (\<lambda>rv rv'. (\<not> fst rv \<and> fst (snd rv) = thread \<and> snd (snd rv) = ResumeCurrentThread) = (rv' \<noteq> 0)) ret__int_' (\<lambda>rv rv'. {s. (s \<in> \<lbrace>rv' \<noteq> 0\<rbrace> \<longrightarrow> s \<in> {s. s \<in> UNIV}) \<and> (s \<notin> \<lbrace>rv' \<noteq> 0\<rbrace> \<longrightarrow> s \<in> UNIV)})
 7. \<And>tptr s s'. \<lbrakk>tptr = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; (tcb_at' thread and st_tcb_at' (not runnable') thread and valid_queues' and Invariants_H.valid_queues and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and valid_objs') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (?P167 tptr and ?R167 tptr) s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> ?Q226 tptr rv s \<longrightarrow> s' \<in> ?Q'226 tptr rv} proof (prove)
goal (7 subgoals):
 1. \<And>tptr runnable curThread. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> ccorres (\<lambda>rv rv'. (\<not> fst rv \<and> fst (snd rv) = thread \<and> snd (snd rv) = ResumeCurrentThread) = (rv' \<noteq> 0)) ret__int_' (?P231 tptr runnable curThread) (?P'231 tptr runnable curThread) [] (do action <- getSchedulerAction;
return (runnable, curThread, action)
od) (\<acute>ret__int :== (if tptr = \<acute>ksCurThread then 1 else 0);;
IF \<acute>ret__int \<noteq> 0 THEN
  \<acute>ret__int :== (if \<acute>ksSchedulerAction = NULL then 1 else 0)
FI;;
IF \<acute>ret__int \<noteq> 0 THEN
  \<acute>ret__unsigned_long :== CALL isRunnable_'proc(tptr);;
\<acute>ret__int :== (if \<acute>ret__unsigned_long = 0 then 1 else 0)
FI)
 2. \<And>tptr s. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<lbrace>(=) s\<rbrace> isRunnable thread \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<And>tptr. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<lbrace>?P167 tptr\<rbrace> isRunnable thread \<lbrace>\<lambda>runnable s. \<forall>rv. ksCurThread s = rv \<longrightarrow> ?P231 tptr runnable rv s\<rbrace>
 4. \<And>tptr. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> empty_fail (isRunnable thread)
 5. \<And>tptr. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<lbrace>?R167 tptr\<rbrace> do runnable <- isRunnable thread;
curThread <- getCurThread;
action <- getSchedulerAction;
return (runnable, curThread, action)
od \<lbrace>\<lambda>rv. (\<lambda>_. True) and (\<lambda>s. \<not> fst rv \<and> fst (snd rv) = thread \<and> snd (snd rv) = ResumeCurrentThread \<longrightarrow> (Invariants_H.valid_queues and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and valid_objs') s) and (\<lambda>s. \<not> (\<not> fst rv \<and> fst (snd rv) = thread \<and> snd (snd rv) = ResumeCurrentThread) \<longrightarrow> True)\<rbrace>
 6. \<And>tptr. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> guard_is_UNIV (\<lambda>rv rv'. (\<not> fst rv \<and> fst (snd rv) = thread \<and> snd (snd rv) = ResumeCurrentThread) = (rv' \<noteq> 0)) ret__int_' (\<lambda>rv rv'. {s. (s \<in> \<lbrace>rv' \<noteq> 0\<rbrace> \<longrightarrow> s \<in> {s. s \<in> UNIV}) \<and> (s \<notin> \<lbrace>rv' \<noteq> 0\<rbrace> \<longrightarrow> s \<in> UNIV)})
 7. \<And>tptr s s'. \<lbrakk>tptr = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; (tcb_at' thread and st_tcb_at' (not runnable') thread and valid_queues' and Invariants_H.valid_queues and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and valid_objs') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (?P167 tptr and ?R167 tptr) s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> (\<forall>rva. ksCurThread s = rva \<longrightarrow> ?P231 tptr rv rva s) \<longrightarrow> s' \<in> {s. \<forall>rva. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rva \<longrightarrow> s \<in> ?P'231 tptr rv rva}} proof (prove)
goal (10 subgoals):
 1. \<And>tptr runnable curThread action. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> ccorres (\<lambda>rv rv'. (\<not> fst rv \<and> fst (snd rv) = thread \<and> snd (snd rv) = ResumeCurrentThread) = (rv' \<noteq> 0)) ret__int_' (?Q233 tptr runnable curThread action) (?Q'233 tptr runnable curThread action) [] (return (runnable, curThread, action)) (\<acute>ret__int :== (if tptr = \<acute>ksCurThread then 1 else 0);;
IF \<acute>ret__int \<noteq> 0 THEN
  \<acute>ret__int :== (if \<acute>ksSchedulerAction = NULL then 1 else 0)
FI;;
IF \<acute>ret__int \<noteq> 0 THEN
  \<acute>ret__unsigned_long :== CALL isRunnable_'proc(tptr);;
\<acute>ret__int :== (if \<acute>ret__unsigned_long = 0 then 1 else 0)
FI)
 2. \<And>tptr runnable curThread s. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<lbrace>(=) s\<rbrace> getSchedulerAction \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<And>tptr runnable curThread. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<lbrace>?P231 tptr runnable curThread\<rbrace> getSchedulerAction \<lbrace>?Q233 tptr runnable curThread\<rbrace>
 4. \<And>tptr runnable curThread. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> empty_fail getSchedulerAction
 5. \<And>tptr s. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<lbrace>(=) s\<rbrace> isRunnable thread \<lbrace>\<lambda>r. (=) s\<rbrace>
 6. \<And>tptr. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<lbrace>?P167 tptr\<rbrace> isRunnable thread \<lbrace>\<lambda>runnable s. \<forall>rv. ksCurThread s = rv \<longrightarrow> ?P231 tptr runnable rv s\<rbrace>
 7. \<And>tptr. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> empty_fail (isRunnable thread)
 8. \<And>tptr. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<lbrace>?R167 tptr\<rbrace> do runnable <- isRunnable thread;
curThread <- getCurThread;
action <- getSchedulerAction;
return (runnable, curThread, action)
od \<lbrace>\<lambda>rv. (\<lambda>_. True) and (\<lambda>s. \<not> fst rv \<and> fst (snd rv) = thread \<and> snd (snd rv) = ResumeCurrentThread \<longrightarrow> (Invariants_H.valid_queues and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and valid_objs') s) and (\<lambda>s. \<not> (\<not> fst rv \<and> fst (snd rv) = thread \<and> snd (snd rv) = ResumeCurrentThread) \<longrightarrow> True)\<rbrace>
 9. \<And>tptr. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> guard_is_UNIV (\<lambda>rv rv'. (\<not> fst rv \<and> fst (snd rv) = thread \<and> snd (snd rv) = ResumeCurrentThread) = (rv' \<noteq> 0)) ret__int_' (\<lambda>rv rv'. {s. (s \<in> \<lbrace>rv' \<noteq> 0\<rbrace> \<longrightarrow> s \<in> {s. s \<in> UNIV}) \<and> (s \<notin> \<lbrace>rv' \<noteq> 0\<rbrace> \<longrightarrow> s \<in> UNIV)})
 10. \<And>tptr s s'. \<lbrakk>tptr = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; (tcb_at' thread and st_tcb_at' (not runnable') thread and valid_queues' and Invariants_H.valid_queues and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and valid_objs') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (?P167 tptr and ?R167 tptr) s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> (\<forall>rva. ksCurThread s = rva \<longrightarrow> ?P231 tptr rv rva s) \<longrightarrow> s' \<in> {s. \<forall>rva. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rva \<longrightarrow> s \<in> {s'. \<forall>rvb s. (s, s') \<in> rf_sr \<and> ?Q233 tptr rv rva rvb s \<longrightarrow> s' \<in> ?Q'233 tptr rv rva rvb}}} proof (prove)
goal (10 subgoals):
 1. \<And>tptr runnable curThread action. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<forall>\<sigma>. \<Gamma>\<turnstile> {s. (st_tcb_at' (\<lambda>st. runnable' st = runnable) thread \<sigma> \<and> curThread = ksCurThread \<sigma> \<and> action = ksSchedulerAction \<sigma> \<and> weak_sch_act_wf (ksSchedulerAction \<sigma>) \<sigma>) \<and> s \<in> UNIV \<and> (\<sigma>, s) \<in> rf_sr} \<acute>ret__int :== (if tptr = \<acute>ksCurThread then 1 else 0);;
IF \<acute>ret__int \<noteq> 0 THEN
  \<acute>ret__int :== (if \<acute>ksSchedulerAction = NULL then 1 else 0)
FI;;
IF \<acute>ret__int \<noteq> 0 THEN
  \<acute>ret__unsigned_long :== CALL isRunnable_'proc(tptr);;
\<acute>ret__int :== (if \<acute>ret__unsigned_long = 0 then 1 else 0)
FI {s. \<exists>(rv, \<sigma>')\<in>fst (return (runnable, curThread, action) \<sigma>). (\<sigma>', s) \<in> rf_sr \<and> (\<not> fst rv \<and> fst (snd rv) = thread \<and> snd (snd rv) = ResumeCurrentThread) = (ret__int_' s \<noteq> 0)}
 2. \<And>tptr runnable curThread s. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<lbrace>(=) s\<rbrace> getSchedulerAction \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<And>tptr runnable curThread. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<lbrace>?P231 tptr runnable curThread\<rbrace> getSchedulerAction \<lbrace>\<lambda>action s. st_tcb_at' (\<lambda>st. runnable' st = runnable) thread s \<and> curThread = ksCurThread s \<and> action = ksSchedulerAction s \<and> weak_sch_act_wf (ksSchedulerAction s) s\<rbrace>
 4. \<And>tptr runnable curThread. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> empty_fail getSchedulerAction
 5. \<And>tptr s. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<lbrace>(=) s\<rbrace> isRunnable thread \<lbrace>\<lambda>r. (=) s\<rbrace>
 6. \<And>tptr. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<lbrace>?P167 tptr\<rbrace> isRunnable thread \<lbrace>\<lambda>runnable s. \<forall>rv. ksCurThread s = rv \<longrightarrow> ?P231 tptr runnable rv s\<rbrace>
 7. \<And>tptr. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> empty_fail (isRunnable thread)
 8. \<And>tptr. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<lbrace>?R167 tptr\<rbrace> do runnable <- isRunnable thread;
curThread <- getCurThread;
action <- getSchedulerAction;
return (runnable, curThread, action)
od \<lbrace>\<lambda>rv. (\<lambda>_. True) and (\<lambda>s. \<not> fst rv \<and> fst (snd rv) = thread \<and> snd (snd rv) = ResumeCurrentThread \<longrightarrow> (Invariants_H.valid_queues and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and valid_objs') s) and (\<lambda>s. \<not> (\<not> fst rv \<and> fst (snd rv) = thread \<and> snd (snd rv) = ResumeCurrentThread) \<longrightarrow> True)\<rbrace>
 9. \<And>tptr. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> guard_is_UNIV (\<lambda>rv rv'. (\<not> fst rv \<and> fst (snd rv) = thread \<and> snd (snd rv) = ResumeCurrentThread) = (rv' \<noteq> 0)) ret__int_' (\<lambda>rv rv'. {s. (s \<in> \<lbrace>rv' \<noteq> 0\<rbrace> \<longrightarrow> s \<in> {s. s \<in> UNIV}) \<and> (s \<notin> \<lbrace>rv' \<noteq> 0\<rbrace> \<longrightarrow> s \<in> UNIV)})
 10. \<And>tptr s s'. \<lbrakk>tptr = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; (tcb_at' thread and st_tcb_at' (not runnable') thread and valid_queues' and Invariants_H.valid_queues and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and valid_objs') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (?P167 tptr and ?R167 tptr) s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> (\<forall>rva. ksCurThread s = rva \<longrightarrow> ?P231 tptr rv rva s) \<longrightarrow> s' \<in> {s. \<forall>rva. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rva \<longrightarrow> s \<in> {s'. \<forall>rvb s. (s, s') \<in> rf_sr \<and> st_tcb_at' (\<lambda>st. runnable' st = rv) thread s \<and> rva = ksCurThread s \<and> rvb = ksSchedulerAction s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<longrightarrow> s' \<in> UNIV}}} proof (prove)
goal (10 subgoals):
 1. \<And>tptr runnable curThread action \<sigma>. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> {s. (st_tcb_at' (\<lambda>st. runnable' st = runnable) thread \<sigma> \<and> curThread = ksCurThread \<sigma> \<and> action = ksSchedulerAction \<sigma> \<and> weak_sch_act_wf (ksSchedulerAction \<sigma>) \<sigma>) \<and> s \<in> UNIV \<and> (\<sigma>, s) \<in> rf_sr} \<subseteq> {s. ((if tptr = ksCurThread_' (globals s) then 1 else 0) \<noteq> 0 \<longrightarrow> ((if ksSchedulerAction_' (globals s) = NULL then 1 else 0) \<noteq> 0 \<longrightarrow> cslift s tptr \<noteq> None \<and> (\<forall>t. ret__unsigned_long_' t = from_bool (tsType_CL (thread_state_lift (tcbState_C (the (cslift s tptr)))) \<in> insert (SCAST(32 signed \<rightarrow> 32) ThreadState_Running) (Collect ((=) (SCAST(32 signed \<rightarrow> 32) ThreadState_Restart)))) \<longrightarrow> (\<exists>(rv, \<sigma>')\<in>fst (return (runnable, curThread, action) \<sigma>). (\<sigma>', s\<lparr>ret__unsigned_long_' := from_bool (tsType_CL (thread_state_lift (tcbState_C (the (cslift s tptr)))) \<in> insert (SCAST(32 signed \<rightarrow> 32) ThreadState_Running) (Collect ((=) (SCAST(32 signed \<rightarrow> 32) ThreadState_Restart)))), ret__int_' := if from_bool (tsType_CL (thread_state_lift (tcbState_C (the (cslift s tptr)))) \<in> insert (SCAST(32 signed \<rightarrow> 32) ThreadState_Running) (Collect ((=) (SCAST(32 signed \<rightarrow> 32) ThreadState_Restart)))) = 0 then 1 else 0\<rparr>) \<in> rf_sr \<and> (\<not> fst rv \<and> fst (snd rv) = thread \<and> snd (snd rv) = ResumeCurrentThread) = ((if from_bool (tsType_CL (thread_state_lift (tcbState_C (the (cslift s tptr)))) \<in> insert (SCAST(32 signed \<rightarrow> 32) ThreadState_Running) (Collect ((=) (SCAST(32 signed \<rightarrow> 32) ThreadState_Restart)))) = 0 then 1 else 0) \<noteq> 0)))) \<and> (\<not> (if ksSchedulerAction_' (globals s) = NULL then 1 else 0) \<noteq> 0 \<longrightarrow> (\<exists>(rv, \<sigma>')\<in>fst (return (runnable, curThread, action) \<sigma>). (\<sigma>', s\<lparr>ret__int_' := if ksSchedulerAction_' (globals s) = NULL then 1 else 0\<rparr>) \<in> rf_sr \<and> (\<not> fst rv \<and> fst (snd rv) = thread \<and> snd (snd rv) = ResumeCurrentThread) = ((if ksSchedulerAction_' (globals s) = NULL then 1 else 0) \<noteq> 0)))) \<and> (\<not> (if tptr = ksCurThread_' (globals s) then 1 else 0) \<noteq> 0 \<longrightarrow> ((if tptr = ksCurThread_' (globals s) then 1 else 0) \<noteq> 0 \<longrightarrow> cslift s tptr \<noteq> None \<and> (\<forall>t. ret__unsigned_long_' t = from_bool (tsType_CL (thread_state_lift (tcbState_C (the (cslift s tptr)))) \<in> insert (SCAST(32 signed \<rightarrow> 32) ThreadState_Running) (Collect ((=) (SCAST(32 signed \<rightarrow> 32) ThreadState_Restart)))) \<longrightarrow> (\<exists>(rv, \<sigma>')\<in>fst (return (runnable, curThread, action) \<sigma>). (\<sigma>', s\<lparr>ret__unsigned_long_' := from_bool (tsType_CL (thread_state_lift (tcbState_C (the (cslift s tptr)))) \<in> insert (SCAST(32 signed \<rightarrow> 32) ThreadState_Running) (Collect ((=) (SCAST(32 signed \<rightarrow> 32) ThreadState_Restart)))), ret__int_' := if from_bool (tsType_CL (thread_state_lift (tcbState_C (the (cslift s tptr)))) \<in> insert (SCAST(32 signed \<rightarrow> 32) ThreadState_Running) (Collect ((=) (SCAST(32 signed \<rightarrow> 32) ThreadState_Restart)))) = 0 then 1 else 0\<rparr>) \<in> rf_sr \<and> (\<not> fst rv \<and> fst (snd rv) = thread \<and> snd (snd rv) = ResumeCurrentThread) = ((if from_bool (tsType_CL (thread_state_lift (tcbState_C (the (cslift s tptr)))) \<in> insert (SCAST(32 signed \<rightarrow> 32) ThreadState_Running) (Collect ((=) (SCAST(32 signed \<rightarrow> 32) ThreadState_Restart)))) = 0 then 1 else 0) \<noteq> 0)))) \<and> (\<not> (if tptr = ksCurThread_' (globals s) then 1 else 0) \<noteq> 0 \<longrightarrow> (\<exists>(rv, \<sigma>')\<in>fst (return (runnable, curThread, action) \<sigma>). (\<sigma>', s\<lparr>ret__int_' := if tptr = ksCurThread_' (globals s) then 1 else 0\<rparr>) \<in> rf_sr \<and> (\<not> fst rv \<and> fst (snd rv) = thread \<and> snd (snd rv) = ResumeCurrentThread) = ((if tptr = ksCurThread_' (globals s) then 1 else 0) \<noteq> 0))))}
 2. \<And>tptr runnable curThread s. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<lbrace>(=) s\<rbrace> getSchedulerAction \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<And>tptr runnable curThread. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<lbrace>?P231 tptr runnable curThread\<rbrace> getSchedulerAction \<lbrace>\<lambda>action s. st_tcb_at' (\<lambda>st. runnable' st = runnable) thread s \<and> curThread = ksCurThread s \<and> action = ksSchedulerAction s \<and> weak_sch_act_wf (ksSchedulerAction s) s\<rbrace>
 4. \<And>tptr runnable curThread. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> empty_fail getSchedulerAction
 5. \<And>tptr s. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<lbrace>(=) s\<rbrace> isRunnable thread \<lbrace>\<lambda>r. (=) s\<rbrace>
 6. \<And>tptr. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<lbrace>?P167 tptr\<rbrace> isRunnable thread \<lbrace>\<lambda>runnable s. \<forall>rv. ksCurThread s = rv \<longrightarrow> ?P231 tptr runnable rv s\<rbrace>
 7. \<And>tptr. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> empty_fail (isRunnable thread)
 8. \<And>tptr. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<lbrace>?R167 tptr\<rbrace> do runnable <- isRunnable thread;
curThread <- getCurThread;
action <- getSchedulerAction;
return (runnable, curThread, action)
od \<lbrace>\<lambda>rv. (\<lambda>_. True) and (\<lambda>s. \<not> fst rv \<and> fst (snd rv) = thread \<and> snd (snd rv) = ResumeCurrentThread \<longrightarrow> (Invariants_H.valid_queues and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and valid_objs') s) and (\<lambda>s. \<not> (\<not> fst rv \<and> fst (snd rv) = thread \<and> snd (snd rv) = ResumeCurrentThread) \<longrightarrow> True)\<rbrace>
 9. \<And>tptr. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> guard_is_UNIV (\<lambda>rv rv'. (\<not> fst rv \<and> fst (snd rv) = thread \<and> snd (snd rv) = ResumeCurrentThread) = (rv' \<noteq> 0)) ret__int_' (\<lambda>rv rv'. {s. (s \<in> \<lbrace>rv' \<noteq> 0\<rbrace> \<longrightarrow> s \<in> {s. s \<in> UNIV}) \<and> (s \<notin> \<lbrace>rv' \<noteq> 0\<rbrace> \<longrightarrow> s \<in> UNIV)})
 10. \<And>tptr s s'. \<lbrakk>tptr = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; (tcb_at' thread and st_tcb_at' (not runnable') thread and valid_queues' and Invariants_H.valid_queues and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and valid_objs') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (?P167 tptr and ?R167 tptr) s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> (\<forall>rva. ksCurThread s = rva \<longrightarrow> ?P231 tptr rv rva s) \<longrightarrow> s' \<in> {s. \<forall>rva. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rva \<longrightarrow> s \<in> {s'. \<forall>rvb s. (s, s') \<in> rf_sr \<and> st_tcb_at' (\<lambda>st. runnable' st = rv) thread s \<and> rva = ksCurThread s \<and> rvb = ksSchedulerAction s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<longrightarrow> s' \<in> UNIV}}} proof (prove)
goal (10 subgoals):
 1. \<And>runnable \<sigma> x. \<lbrakk>st_tcb_at' (\<lambda>st. runnable' st = runnable) thread \<sigma>; weak_sch_act_wf (ksSchedulerAction \<sigma>) \<sigma>; (\<sigma>, x) \<in> rf_sr\<rbrakk> \<Longrightarrow> (tcb_ptr_to_ctcb_ptr thread = ksCurThread_' (globals x) \<longrightarrow> (ksSchedulerAction_' (globals x) = NULL \<longrightarrow> (\<exists>y. cslift x (ksCurThread_' (globals x)) = Some y) \<and> ((\<exists>t. ret__unsigned_long_' t = from_bool (tsType_CL (thread_state_lift (tcbState_C (the (cslift x (ksCurThread_' (globals x)))))) = SCAST(32 signed \<rightarrow> 32) ThreadState_Running \<or> tsType_CL (thread_state_lift (tcbState_C (the (cslift x (ksCurThread_' (globals x)))))) = SCAST(32 signed \<rightarrow> 32) ThreadState_Restart)) \<longrightarrow> (\<not> runnable \<and> ksCurThread \<sigma> = thread \<and> ksSchedulerAction \<sigma> = ResumeCurrentThread) = (tsType_CL (thread_state_lift (tcbState_C (the (cslift x (ksCurThread_' (globals x)))))) \<noteq> SCAST(32 signed \<rightarrow> 32) ThreadState_Running \<and> tsType_CL (thread_state_lift (tcbState_C (the (cslift x (ksCurThread_' (globals x)))))) \<noteq> SCAST(32 signed \<rightarrow> 32) ThreadState_Restart))) \<and> (ksSchedulerAction_' (globals x) \<noteq> NULL \<longrightarrow> ksCurThread \<sigma> = thread \<longrightarrow> runnable \<or> ksSchedulerAction \<sigma> \<noteq> ResumeCurrentThread)) \<and> (tcb_ptr_to_ctcb_ptr thread \<noteq> ksCurThread_' (globals x) \<longrightarrow> ksCurThread \<sigma> = thread \<longrightarrow> runnable \<or> ksSchedulerAction \<sigma> \<noteq> ResumeCurrentThread)
 2. \<And>tptr runnable curThread s. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<lbrace>(=) s\<rbrace> getSchedulerAction \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<And>tptr runnable curThread. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<lbrace>?P231 tptr runnable curThread\<rbrace> getSchedulerAction \<lbrace>\<lambda>action s. st_tcb_at' (\<lambda>st. runnable' st = runnable) thread s \<and> curThread = ksCurThread s \<and> action = ksSchedulerAction s \<and> weak_sch_act_wf (ksSchedulerAction s) s\<rbrace>
 4. \<And>tptr runnable curThread. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> empty_fail getSchedulerAction
 5. \<And>tptr s. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<lbrace>(=) s\<rbrace> isRunnable thread \<lbrace>\<lambda>r. (=) s\<rbrace>
 6. \<And>tptr. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<lbrace>?P167 tptr\<rbrace> isRunnable thread \<lbrace>\<lambda>runnable s. \<forall>rv. ksCurThread s = rv \<longrightarrow> ?P231 tptr runnable rv s\<rbrace>
 7. \<And>tptr. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> empty_fail (isRunnable thread)
 8. \<And>tptr. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<lbrace>?R167 tptr\<rbrace> do runnable <- isRunnable thread;
curThread <- getCurThread;
action <- getSchedulerAction;
return (runnable, curThread, action)
od \<lbrace>\<lambda>rv. (\<lambda>_. True) and (\<lambda>s. \<not> fst rv \<and> fst (snd rv) = thread \<and> snd (snd rv) = ResumeCurrentThread \<longrightarrow> (Invariants_H.valid_queues and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and valid_objs') s) and (\<lambda>s. \<not> (\<not> fst rv \<and> fst (snd rv) = thread \<and> snd (snd rv) = ResumeCurrentThread) \<longrightarrow> True)\<rbrace>
 9. \<And>tptr. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> guard_is_UNIV (\<lambda>rv rv'. (\<not> fst rv \<and> fst (snd rv) = thread \<and> snd (snd rv) = ResumeCurrentThread) = (rv' \<noteq> 0)) ret__int_' (\<lambda>rv rv'. {s. (s \<in> \<lbrace>rv' \<noteq> 0\<rbrace> \<longrightarrow> s \<in> {s. s \<in> UNIV}) \<and> (s \<notin> \<lbrace>rv' \<noteq> 0\<rbrace> \<longrightarrow> s \<in> UNIV)})
 10. \<And>tptr s s'. \<lbrakk>tptr = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; (tcb_at' thread and st_tcb_at' (not runnable') thread and valid_queues' and Invariants_H.valid_queues and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and valid_objs') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (?P167 tptr and ?R167 tptr) s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> (\<forall>rva. ksCurThread s = rva \<longrightarrow> ?P231 tptr rv rva s) \<longrightarrow> s' \<in> {s. \<forall>rva. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rva \<longrightarrow> s \<in> {s'. \<forall>rvb s. (s, s') \<in> rf_sr \<and> st_tcb_at' (\<lambda>st. runnable' st = rv) thread s \<and> rva = ksCurThread s \<and> rvb = ksSchedulerAction s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<longrightarrow> s' \<in> UNIV}}} proof (prove)
goal (10 subgoals):
 1. \<And>runnable \<sigma> x. \<lbrakk>st_tcb_at' (\<lambda>st. runnable' st = runnable) (ksCurThread \<sigma>) \<sigma>; weak_sch_act_wf (ksSchedulerAction \<sigma>) \<sigma>; (\<sigma>, x) \<in> rf_sr; thread = ksCurThread \<sigma>\<rbrakk> \<Longrightarrow> (ksSchedulerAction_' (globals x) = NULL \<longrightarrow> (\<exists>y. cslift x (tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>)) = Some y) \<and> ((\<exists>t. ret__unsigned_long_' t = from_bool (tsType_CL (thread_state_lift (tcbState_C (the (cslift x (tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>)))))) = SCAST(32 signed \<rightarrow> 32) ThreadState_Running \<or> tsType_CL (thread_state_lift (tcbState_C (the (cslift x (tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>)))))) = SCAST(32 signed \<rightarrow> 32) ThreadState_Restart)) \<longrightarrow> (\<not> runnable \<and> ksSchedulerAction \<sigma> = ResumeCurrentThread) = (tsType_CL (thread_state_lift (tcbState_C (the (cslift x (tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>)))))) \<noteq> SCAST(32 signed \<rightarrow> 32) ThreadState_Running \<and> tsType_CL (thread_state_lift (tcbState_C (the (cslift x (tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>)))))) \<noteq> SCAST(32 signed \<rightarrow> 32) ThreadState_Restart))) \<and> (ksSchedulerAction_' (globals x) \<noteq> NULL \<longrightarrow> runnable \<or> ksSchedulerAction \<sigma> \<noteq> ResumeCurrentThread)
 2. \<And>tptr runnable curThread s. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<lbrace>(=) s\<rbrace> getSchedulerAction \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<And>tptr runnable curThread. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<lbrace>?P231 tptr runnable curThread\<rbrace> getSchedulerAction \<lbrace>\<lambda>action s. st_tcb_at' (\<lambda>st. runnable' st = runnable) thread s \<and> curThread = ksCurThread s \<and> action = ksSchedulerAction s \<and> weak_sch_act_wf (ksSchedulerAction s) s\<rbrace>
 4. \<And>tptr runnable curThread. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> empty_fail getSchedulerAction
 5. \<And>tptr s. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<lbrace>(=) s\<rbrace> isRunnable thread \<lbrace>\<lambda>r. (=) s\<rbrace>
 6. \<And>tptr. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<lbrace>?P167 tptr\<rbrace> isRunnable thread \<lbrace>\<lambda>runnable s. \<forall>rv. ksCurThread s = rv \<longrightarrow> ?P231 tptr runnable rv s\<rbrace>
 7. \<And>tptr. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> empty_fail (isRunnable thread)
 8. \<And>tptr. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<lbrace>?R167 tptr\<rbrace> do runnable <- isRunnable thread;
curThread <- getCurThread;
action <- getSchedulerAction;
return (runnable, curThread, action)
od \<lbrace>\<lambda>rv. (\<lambda>_. True) and (\<lambda>s. \<not> fst rv \<and> fst (snd rv) = thread \<and> snd (snd rv) = ResumeCurrentThread \<longrightarrow> (Invariants_H.valid_queues and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and valid_objs') s) and (\<lambda>s. \<not> (\<not> fst rv \<and> fst (snd rv) = thread \<and> snd (snd rv) = ResumeCurrentThread) \<longrightarrow> True)\<rbrace>
 9. \<And>tptr. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> guard_is_UNIV (\<lambda>rv rv'. (\<not> fst rv \<and> fst (snd rv) = thread \<and> snd (snd rv) = ResumeCurrentThread) = (rv' \<noteq> 0)) ret__int_' (\<lambda>rv rv'. {s. (s \<in> \<lbrace>rv' \<noteq> 0\<rbrace> \<longrightarrow> s \<in> {s. s \<in> UNIV}) \<and> (s \<notin> \<lbrace>rv' \<noteq> 0\<rbrace> \<longrightarrow> s \<in> UNIV)})
 10. \<And>tptr s s'. \<lbrakk>tptr = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; (tcb_at' thread and st_tcb_at' (not runnable') thread and valid_queues' and Invariants_H.valid_queues and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and valid_objs') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (?P167 tptr and ?R167 tptr) s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> (\<forall>rva. ksCurThread s = rva \<longrightarrow> ?P231 tptr rv rva s) \<longrightarrow> s' \<in> {s. \<forall>rva. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rva \<longrightarrow> s \<in> {s'. \<forall>rvb s. (s, s') \<in> rf_sr \<and> st_tcb_at' (\<lambda>st. runnable' st = rv) thread s \<and> rva = ksCurThread s \<and> rvb = ksSchedulerAction s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<longrightarrow> s' \<in> UNIV}}} proof (prove)
goal (11 subgoals):
 1. \<And>runnable \<sigma> x. \<lbrakk>st_tcb_at' (\<lambda>st. runnable' st = runnable) (ksCurThread \<sigma>) \<sigma>; weak_sch_act_wf (ksSchedulerAction \<sigma>) \<sigma>; (\<sigma>, x) \<in> rf_sr; thread = ksCurThread \<sigma>\<rbrakk> \<Longrightarrow> ksSchedulerAction_' (globals x) = NULL \<longrightarrow> (\<exists>y. cslift x (tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>)) = Some y) \<and> ((\<exists>t. ret__unsigned_long_' t = from_bool (tsType_CL (thread_state_lift (tcbState_C (the (cslift x (tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>)))))) = SCAST(32 signed \<rightarrow> 32) ThreadState_Running \<or> tsType_CL (thread_state_lift (tcbState_C (the (cslift x (tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>)))))) = SCAST(32 signed \<rightarrow> 32) ThreadState_Restart)) \<longrightarrow> (\<not> runnable \<and> ksSchedulerAction \<sigma> = ResumeCurrentThread) = (tsType_CL (thread_state_lift (tcbState_C (the (cslift x (tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>)))))) \<noteq> SCAST(32 signed \<rightarrow> 32) ThreadState_Running \<and> tsType_CL (thread_state_lift (tcbState_C (the (cslift x (tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>)))))) \<noteq> SCAST(32 signed \<rightarrow> 32) ThreadState_Restart))
 2. \<And>runnable \<sigma> x. \<lbrakk>st_tcb_at' (\<lambda>st. runnable' st = runnable) (ksCurThread \<sigma>) \<sigma>; weak_sch_act_wf (ksSchedulerAction \<sigma>) \<sigma>; (\<sigma>, x) \<in> rf_sr; thread = ksCurThread \<sigma>\<rbrakk> \<Longrightarrow> ksSchedulerAction_' (globals x) \<noteq> NULL \<longrightarrow> runnable \<or> ksSchedulerAction \<sigma> \<noteq> ResumeCurrentThread
 3. \<And>tptr runnable curThread s. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<lbrace>(=) s\<rbrace> getSchedulerAction \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<And>tptr runnable curThread. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<lbrace>?P231 tptr runnable curThread\<rbrace> getSchedulerAction \<lbrace>\<lambda>action s. st_tcb_at' (\<lambda>st. runnable' st = runnable) thread s \<and> curThread = ksCurThread s \<and> action = ksSchedulerAction s \<and> weak_sch_act_wf (ksSchedulerAction s) s\<rbrace>
 5. \<And>tptr runnable curThread. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> empty_fail getSchedulerAction
 6. \<And>tptr s. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<lbrace>(=) s\<rbrace> isRunnable thread \<lbrace>\<lambda>r. (=) s\<rbrace>
 7. \<And>tptr. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<lbrace>?P167 tptr\<rbrace> isRunnable thread \<lbrace>\<lambda>runnable s. \<forall>rv. ksCurThread s = rv \<longrightarrow> ?P231 tptr runnable rv s\<rbrace>
 8. \<And>tptr. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> empty_fail (isRunnable thread)
 9. \<And>tptr. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<lbrace>?R167 tptr\<rbrace> do runnable <- isRunnable thread;
curThread <- getCurThread;
action <- getSchedulerAction;
return (runnable, curThread, action)
od \<lbrace>\<lambda>rv. (\<lambda>_. True) and (\<lambda>s. \<not> fst rv \<and> fst (snd rv) = thread \<and> snd (snd rv) = ResumeCurrentThread \<longrightarrow> (Invariants_H.valid_queues and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and valid_objs') s) and (\<lambda>s. \<not> (\<not> fst rv \<and> fst (snd rv) = thread \<and> snd (snd rv) = ResumeCurrentThread) \<longrightarrow> True)\<rbrace>
 10. \<And>tptr. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> guard_is_UNIV (\<lambda>rv rv'. (\<not> fst rv \<and> fst (snd rv) = thread \<and> snd (snd rv) = ResumeCurrentThread) = (rv' \<noteq> 0)) ret__int_' (\<lambda>rv rv'. {s. (s \<in> \<lbrace>rv' \<noteq> 0\<rbrace> \<longrightarrow> s \<in> {s. s \<in> UNIV}) \<and> (s \<notin> \<lbrace>rv' \<noteq> 0\<rbrace> \<longrightarrow> s \<in> UNIV)})
A total of 11 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>runnable \<sigma> x. \<lbrakk>obj_at' ((\<lambda>st. runnable' st = runnable) \<circ> tcbState) (ksCurThread \<sigma>) \<sigma>; weak_sch_act_wf (ksSchedulerAction \<sigma>) \<sigma>; (\<sigma>, x) \<in> rf_sr; thread = ksCurThread \<sigma>; ksSchedulerAction_' (globals x) = NULL\<rbrakk> \<Longrightarrow> (\<exists>y. cslift x (tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>)) = Some y) \<and> ((\<exists>t. ret__unsigned_long_' t = from_bool (tsType_CL (thread_state_lift (tcbState_C (the (cslift x (tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>)))))) = SCAST(32 signed \<rightarrow> 32) ThreadState_Running \<or> tsType_CL (thread_state_lift (tcbState_C (the (cslift x (tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>)))))) = SCAST(32 signed \<rightarrow> 32) ThreadState_Restart)) \<longrightarrow> (\<not> runnable \<and> ksSchedulerAction \<sigma> = ResumeCurrentThread) = (tsType_CL (thread_state_lift (tcbState_C (the (cslift x (tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>)))))) \<noteq> SCAST(32 signed \<rightarrow> 32) ThreadState_Running \<and> tsType_CL (thread_state_lift (tcbState_C (the (cslift x (tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>)))))) \<noteq> SCAST(32 signed \<rightarrow> 32) ThreadState_Restart))
 2. \<And>runnable \<sigma> x. \<lbrakk>st_tcb_at' (\<lambda>st. runnable' st = runnable) (ksCurThread \<sigma>) \<sigma>; weak_sch_act_wf (ksSchedulerAction \<sigma>) \<sigma>; (\<sigma>, x) \<in> rf_sr; thread = ksCurThread \<sigma>\<rbrakk> \<Longrightarrow> ksSchedulerAction_' (globals x) \<noteq> NULL \<longrightarrow> runnable \<or> ksSchedulerAction \<sigma> \<noteq> ResumeCurrentThread
 3. \<And>tptr runnable curThread s. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<lbrace>(=) s\<rbrace> getSchedulerAction \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<And>tptr runnable curThread. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<lbrace>?P231 tptr runnable curThread\<rbrace> getSchedulerAction \<lbrace>\<lambda>action s. st_tcb_at' (\<lambda>st. runnable' st = runnable) thread s \<and> curThread = ksCurThread s \<and> action = ksSchedulerAction s \<and> weak_sch_act_wf (ksSchedulerAction s) s\<rbrace>
 5. \<And>tptr runnable curThread. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> empty_fail getSchedulerAction
 6. \<And>tptr s. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<lbrace>(=) s\<rbrace> isRunnable thread \<lbrace>\<lambda>r. (=) s\<rbrace>
 7. \<And>tptr. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<lbrace>?P167 tptr\<rbrace> isRunnable thread \<lbrace>\<lambda>runnable s. \<forall>rv. ksCurThread s = rv \<longrightarrow> ?P231 tptr runnable rv s\<rbrace>
 8. \<And>tptr. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> empty_fail (isRunnable thread)
 9. \<And>tptr. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<lbrace>?R167 tptr\<rbrace> do runnable <- isRunnable thread;
curThread <- getCurThread;
action <- getSchedulerAction;
return (runnable, curThread, action)
od \<lbrace>\<lambda>rv. (\<lambda>_. True) and (\<lambda>s. \<not> fst rv \<and> fst (snd rv) = thread \<and> snd (snd rv) = ResumeCurrentThread \<longrightarrow> (Invariants_H.valid_queues and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and valid_objs') s) and (\<lambda>s. \<not> (\<not> fst rv \<and> fst (snd rv) = thread \<and> snd (snd rv) = ResumeCurrentThread) \<longrightarrow> True)\<rbrace>
 10. \<And>tptr. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> guard_is_UNIV (\<lambda>rv rv'. (\<not> fst rv \<and> fst (snd rv) = thread \<and> snd (snd rv) = ResumeCurrentThread) = (rv' \<noteq> 0)) ret__int_' (\<lambda>rv rv'. {s. (s \<in> \<lbrace>rv' \<noteq> 0\<rbrace> \<longrightarrow> s \<in> {s. s \<in> UNIV}) \<and> (s \<notin> \<lbrace>rv' \<noteq> 0\<rbrace> \<longrightarrow> s \<in> UNIV)})
A total of 11 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>runnable \<sigma> x. \<lbrakk>weak_sch_act_wf (ksSchedulerAction \<sigma>) \<sigma>; (\<sigma>, x) \<in> rf_sr; thread = ksCurThread \<sigma>; ksSchedulerAction_' (globals x) = NULL; \<exists>ko ko'. ko_at' ko (ksCurThread \<sigma>) \<sigma> \<and> ((\<lambda>st. runnable' st = runnable) \<circ> tcbState) ko \<and> cslift x (tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>)) = Some ko' \<and> ctcb_relation ko ko'\<rbrakk> \<Longrightarrow> (\<exists>y. cslift x (tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>)) = Some y) \<and> ((\<exists>t. ret__unsigned_long_' t = from_bool (tsType_CL (thread_state_lift (tcbState_C (the (cslift x (tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>)))))) = SCAST(32 signed \<rightarrow> 32) ThreadState_Running \<or> tsType_CL (thread_state_lift (tcbState_C (the (cslift x (tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>)))))) = SCAST(32 signed \<rightarrow> 32) ThreadState_Restart)) \<longrightarrow> (\<not> runnable \<and> ksSchedulerAction \<sigma> = ResumeCurrentThread) = (tsType_CL (thread_state_lift (tcbState_C (the (cslift x (tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>)))))) \<noteq> SCAST(32 signed \<rightarrow> 32) ThreadState_Running \<and> tsType_CL (thread_state_lift (tcbState_C (the (cslift x (tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>)))))) \<noteq> SCAST(32 signed \<rightarrow> 32) ThreadState_Restart))
 2. \<And>runnable \<sigma> x. \<lbrakk>st_tcb_at' (\<lambda>st. runnable' st = runnable) (ksCurThread \<sigma>) \<sigma>; weak_sch_act_wf (ksSchedulerAction \<sigma>) \<sigma>; (\<sigma>, x) \<in> rf_sr; thread = ksCurThread \<sigma>\<rbrakk> \<Longrightarrow> ksSchedulerAction_' (globals x) \<noteq> NULL \<longrightarrow> runnable \<or> ksSchedulerAction \<sigma> \<noteq> ResumeCurrentThread
 3. \<And>tptr runnable curThread s. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<lbrace>(=) s\<rbrace> getSchedulerAction \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<And>tptr runnable curThread. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<lbrace>?P231 tptr runnable curThread\<rbrace> getSchedulerAction \<lbrace>\<lambda>action s. st_tcb_at' (\<lambda>st. runnable' st = runnable) thread s \<and> curThread = ksCurThread s \<and> action = ksSchedulerAction s \<and> weak_sch_act_wf (ksSchedulerAction s) s\<rbrace>
 5. \<And>tptr runnable curThread. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> empty_fail getSchedulerAction
 6. \<And>tptr s. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<lbrace>(=) s\<rbrace> isRunnable thread \<lbrace>\<lambda>r. (=) s\<rbrace>
 7. \<And>tptr. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<lbrace>?P167 tptr\<rbrace> isRunnable thread \<lbrace>\<lambda>runnable s. \<forall>rv. ksCurThread s = rv \<longrightarrow> ?P231 tptr runnable rv s\<rbrace>
 8. \<And>tptr. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> empty_fail (isRunnable thread)
 9. \<And>tptr. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<lbrace>?R167 tptr\<rbrace> do runnable <- isRunnable thread;
curThread <- getCurThread;
action <- getSchedulerAction;
return (runnable, curThread, action)
od \<lbrace>\<lambda>rv. (\<lambda>_. True) and (\<lambda>s. \<not> fst rv \<and> fst (snd rv) = thread \<and> snd (snd rv) = ResumeCurrentThread \<longrightarrow> (Invariants_H.valid_queues and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and valid_objs') s) and (\<lambda>s. \<not> (\<not> fst rv \<and> fst (snd rv) = thread \<and> snd (snd rv) = ResumeCurrentThread) \<longrightarrow> True)\<rbrace>
 10. \<And>tptr. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> guard_is_UNIV (\<lambda>rv rv'. (\<not> fst rv \<and> fst (snd rv) = thread \<and> snd (snd rv) = ResumeCurrentThread) = (rv' \<noteq> 0)) ret__int_' (\<lambda>rv rv'. {s. (s \<in> \<lbrace>rv' \<noteq> 0\<rbrace> \<longrightarrow> s \<in> {s. s \<in> UNIV}) \<and> (s \<notin> \<lbrace>rv' \<noteq> 0\<rbrace> \<longrightarrow> s \<in> UNIV)})
A total of 11 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>\<sigma> x ko ko' t. \<lbrakk>weak_sch_act_wf (ksSchedulerAction \<sigma>) \<sigma>; (\<sigma>, x) \<in> rf_sr; thread = ksCurThread \<sigma>; ksSchedulerAction_' (globals x) = NULL; ko_at' ko (ksCurThread \<sigma>) \<sigma>; cslift x (tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>)) = Some ko'; ctcb_relation ko ko'; ret__unsigned_long_' t = from_bool (tsType_CL (thread_state_lift (tcbState_C ko')) = SCAST(32 signed \<rightarrow> 32) ThreadState_Running \<or> tsType_CL (thread_state_lift (tcbState_C ko')) = SCAST(32 signed \<rightarrow> 32) ThreadState_Restart)\<rbrakk> \<Longrightarrow> (\<not> runnable' (tcbState ko) \<and> ksSchedulerAction \<sigma> = ResumeCurrentThread) = (tsType_CL (thread_state_lift (tcbState_C ko')) \<noteq> SCAST(32 signed \<rightarrow> 32) ThreadState_Running \<and> tsType_CL (thread_state_lift (tcbState_C ko')) \<noteq> SCAST(32 signed \<rightarrow> 32) ThreadState_Restart)
 2. \<And>runnable \<sigma> x. \<lbrakk>st_tcb_at' (\<lambda>st. runnable' st = runnable) (ksCurThread \<sigma>) \<sigma>; weak_sch_act_wf (ksSchedulerAction \<sigma>) \<sigma>; (\<sigma>, x) \<in> rf_sr; thread = ksCurThread \<sigma>\<rbrakk> \<Longrightarrow> ksSchedulerAction_' (globals x) \<noteq> NULL \<longrightarrow> runnable \<or> ksSchedulerAction \<sigma> \<noteq> ResumeCurrentThread
 3. \<And>tptr runnable curThread s. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<lbrace>(=) s\<rbrace> getSchedulerAction \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<And>tptr runnable curThread. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<lbrace>?P231 tptr runnable curThread\<rbrace> getSchedulerAction \<lbrace>\<lambda>action s. st_tcb_at' (\<lambda>st. runnable' st = runnable) thread s \<and> curThread = ksCurThread s \<and> action = ksSchedulerAction s \<and> weak_sch_act_wf (ksSchedulerAction s) s\<rbrace>
 5. \<And>tptr runnable curThread. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> empty_fail getSchedulerAction
 6. \<And>tptr s. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<lbrace>(=) s\<rbrace> isRunnable thread \<lbrace>\<lambda>r. (=) s\<rbrace>
 7. \<And>tptr. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<lbrace>?P167 tptr\<rbrace> isRunnable thread \<lbrace>\<lambda>runnable s. \<forall>rv. ksCurThread s = rv \<longrightarrow> ?P231 tptr runnable rv s\<rbrace>
 8. \<And>tptr. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> empty_fail (isRunnable thread)
 9. \<And>tptr. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<lbrace>?R167 tptr\<rbrace> do runnable <- isRunnable thread;
curThread <- getCurThread;
action <- getSchedulerAction;
return (runnable, curThread, action)
od \<lbrace>\<lambda>rv. (\<lambda>_. True) and (\<lambda>s. \<not> fst rv \<and> fst (snd rv) = thread \<and> snd (snd rv) = ResumeCurrentThread \<longrightarrow> (Invariants_H.valid_queues and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and valid_objs') s) and (\<lambda>s. \<not> (\<not> fst rv \<and> fst (snd rv) = thread \<and> snd (snd rv) = ResumeCurrentThread) \<longrightarrow> True)\<rbrace>
 10. \<And>tptr. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> guard_is_UNIV (\<lambda>rv rv'. (\<not> fst rv \<and> fst (snd rv) = thread \<and> snd (snd rv) = ResumeCurrentThread) = (rv' \<noteq> 0)) ret__int_' (\<lambda>rv rv'. {s. (s \<in> \<lbrace>rv' \<noteq> 0\<rbrace> \<longrightarrow> s \<in> {s. s \<in> UNIV}) \<and> (s \<notin> \<lbrace>rv' \<noteq> 0\<rbrace> \<longrightarrow> s \<in> UNIV)})
A total of 11 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>\<sigma> x ko ko' t. \<lbrakk>\<forall>t. ksSchedulerAction \<sigma> = SwitchToThread t \<longrightarrow> st_tcb_at' runnable' t \<sigma> \<and> tcb_in_cur_domain' t \<sigma>; (\<sigma>, x) \<in> rf_sr; thread = ksCurThread \<sigma>; ksSchedulerAction_' (globals x) = NULL; ko_at' ko (ksCurThread \<sigma>) \<sigma>; cslift x (tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>)) = Some ko'; ret__unsigned_long_' t = from_bool (tsType_CL (thread_state_lift (tcbState_C ko')) = SCAST(32 signed \<rightarrow> 32) ThreadState_Running \<or> tsType_CL (thread_state_lift (tcbState_C ko')) = SCAST(32 signed \<rightarrow> 32) ThreadState_Restart); tcbFaultHandler ko = tcbFaultHandler_C ko'; cthread_state_relation_lifted (tcbState ko) (thread_state_lift (tcbState_C ko'), seL4_Fault_lift (tcbFault_C ko')); tcbIPCBuffer ko = tcbIPCBuffer_C ko'; carch_tcb_relation (tcbArch ko) (tcbArch_C ko'); tcbQueued ko = to_bool (tcbQueued_CL (thread_state_lift (tcbState_C ko'))); UCAST(8 \<rightarrow> 32) (tcbDomain ko) = tcbDomain_C ko'; UCAST(8 \<rightarrow> 32) (tcbPriority ko) = tcbPriority_C ko'; UCAST(8 \<rightarrow> 32) (tcbMCP ko) = tcbMCP_C ko'; tcbTimeSlice ko = unat (tcbTimeSlice_C ko'); cfault_rel (tcbFault ko) (seL4_Fault_lift (tcbFault_C ko')) (lookup_fault_lift (tcbLookupFailure_C ko')); option_to_ptr (tcbBoundNotification ko) = tcbBoundNotification_C ko'\<rbrakk> \<Longrightarrow> (\<not> runnable' (tcbState ko) \<and> ksSchedulerAction \<sigma> = ResumeCurrentThread) = (tsType_CL (thread_state_lift (tcbState_C ko')) \<noteq> SCAST(32 signed \<rightarrow> 32) ThreadState_Running \<and> tsType_CL (thread_state_lift (tcbState_C ko')) \<noteq> SCAST(32 signed \<rightarrow> 32) ThreadState_Restart)
 2. \<And>runnable \<sigma> x. \<lbrakk>st_tcb_at' (\<lambda>st. runnable' st = runnable) (ksCurThread \<sigma>) \<sigma>; weak_sch_act_wf (ksSchedulerAction \<sigma>) \<sigma>; (\<sigma>, x) \<in> rf_sr; thread = ksCurThread \<sigma>\<rbrakk> \<Longrightarrow> ksSchedulerAction_' (globals x) \<noteq> NULL \<longrightarrow> runnable \<or> ksSchedulerAction \<sigma> \<noteq> ResumeCurrentThread
 3. \<And>tptr runnable curThread s. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<lbrace>(=) s\<rbrace> getSchedulerAction \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<And>tptr runnable curThread. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<lbrace>?P231 tptr runnable curThread\<rbrace> getSchedulerAction \<lbrace>\<lambda>action s. st_tcb_at' (\<lambda>st. runnable' st = runnable) thread s \<and> curThread = ksCurThread s \<and> action = ksSchedulerAction s \<and> weak_sch_act_wf (ksSchedulerAction s) s\<rbrace>
 5. \<And>tptr runnable curThread. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> empty_fail getSchedulerAction
 6. \<And>tptr s. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<lbrace>(=) s\<rbrace> isRunnable thread \<lbrace>\<lambda>r. (=) s\<rbrace>
 7. \<And>tptr. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<lbrace>?P167 tptr\<rbrace> isRunnable thread \<lbrace>\<lambda>runnable s. \<forall>rv. ksCurThread s = rv \<longrightarrow> ?P231 tptr runnable rv s\<rbrace>
 8. \<And>tptr. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> empty_fail (isRunnable thread)
 9. \<And>tptr. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<lbrace>?R167 tptr\<rbrace> do runnable <- isRunnable thread;
curThread <- getCurThread;
action <- getSchedulerAction;
return (runnable, curThread, action)
od \<lbrace>\<lambda>rv. (\<lambda>_. True) and (\<lambda>s. \<not> fst rv \<and> fst (snd rv) = thread \<and> snd (snd rv) = ResumeCurrentThread \<longrightarrow> (Invariants_H.valid_queues and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and valid_objs') s) and (\<lambda>s. \<not> (\<not> fst rv \<and> fst (snd rv) = thread \<and> snd (snd rv) = ResumeCurrentThread) \<longrightarrow> True)\<rbrace>
 10. \<And>tptr. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> guard_is_UNIV (\<lambda>rv rv'. (\<not> fst rv \<and> fst (snd rv) = thread \<and> snd (snd rv) = ResumeCurrentThread) = (rv' \<noteq> 0)) ret__int_' (\<lambda>rv rv'. {s. (s \<in> \<lbrace>rv' \<noteq> 0\<rbrace> \<longrightarrow> s \<in> {s. s \<in> UNIV}) \<and> (s \<notin> \<lbrace>rv' \<noteq> 0\<rbrace> \<longrightarrow> s \<in> UNIV)})
A total of 11 subgoals... proof (prove)
goal (16 subgoals):
 1. \<And>\<sigma> x ko ko' t. \<lbrakk>\<forall>t. ksSchedulerAction \<sigma> = SwitchToThread t \<longrightarrow> st_tcb_at' runnable' t \<sigma> \<and> tcb_in_cur_domain' t \<sigma>; (\<sigma>, x) \<in> rf_sr; thread = ksCurThread \<sigma>; ksSchedulerAction_' (globals x) = NULL; ko_at' ko (ksCurThread \<sigma>) \<sigma>; cslift x (tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>)) = Some ko'; ret__unsigned_long_' t = SCAST(32 signed \<rightarrow> 32) false; tcbFaultHandler ko = tcbFaultHandler_C ko'; tsType_CL (thread_state_lift (tcbState_C ko')) = 3; tcbIPCBuffer ko = tcbIPCBuffer_C ko'; carch_tcb_relation (tcbArch ko) (tcbArch_C ko'); tcbQueued ko = to_bool (tcbQueued_CL (thread_state_lift (tcbState_C ko'))); UCAST(8 \<rightarrow> 32) (tcbDomain ko) = tcbDomain_C ko'; UCAST(8 \<rightarrow> 32) (tcbPriority ko) = tcbPriority_C ko'; UCAST(8 \<rightarrow> 32) (tcbMCP ko) = tcbMCP_C ko'; tcbTimeSlice ko = unat (tcbTimeSlice_C ko'); cfault_rel (tcbFault ko) (seL4_Fault_lift (tcbFault_C ko')) (lookup_fault_lift (tcbLookupFailure_C ko')); option_to_ptr (tcbBoundNotification ko) = tcbBoundNotification_C ko'; tcbState ko = Structures_H.thread_state.BlockedOnReceive (blockingObject_CL (thread_state_lift (tcbState_C ko'))) (to_bool (blockingIPCCanGrant_CL (thread_state_lift (tcbState_C ko'))))\<rbrakk> \<Longrightarrow> ksSchedulerAction \<sigma> = ResumeCurrentThread
 2. \<And>\<sigma> x ko ko' t. \<lbrakk>\<forall>t. ksSchedulerAction \<sigma> = SwitchToThread t \<longrightarrow> st_tcb_at' runnable' t \<sigma> \<and> tcb_in_cur_domain' t \<sigma>; (\<sigma>, x) \<in> rf_sr; thread = ksCurThread \<sigma>; ksSchedulerAction_' (globals x) = NULL; ko_at' ko (ksCurThread \<sigma>) \<sigma>; cslift x (tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>)) = Some ko'; ret__unsigned_long_' t = SCAST(32 signed \<rightarrow> 32) false; tcbFaultHandler ko = tcbFaultHandler_C ko'; tsType_CL (thread_state_lift (tcbState_C ko')) = 5; tcbIPCBuffer ko = tcbIPCBuffer_C ko'; carch_tcb_relation (tcbArch ko) (tcbArch_C ko'); tcbQueued ko = to_bool (tcbQueued_CL (thread_state_lift (tcbState_C ko'))); UCAST(8 \<rightarrow> 32) (tcbDomain ko) = tcbDomain_C ko'; UCAST(8 \<rightarrow> 32) (tcbPriority ko) = tcbPriority_C ko'; UCAST(8 \<rightarrow> 32) (tcbMCP ko) = tcbMCP_C ko'; tcbTimeSlice ko = unat (tcbTimeSlice_C ko'); cfault_rel (tcbFault ko) (seL4_Fault_lift (tcbFault_C ko')) (lookup_fault_lift (tcbLookupFailure_C ko')); option_to_ptr (tcbBoundNotification ko) = tcbBoundNotification_C ko'; awaiting_reply' (tcbState ko)\<rbrakk> \<Longrightarrow> ksSchedulerAction \<sigma> = ResumeCurrentThread
 3. \<And>\<sigma> x ko ko' t. \<lbrakk>\<forall>t. ksSchedulerAction \<sigma> = SwitchToThread t \<longrightarrow> st_tcb_at' runnable' t \<sigma> \<and> tcb_in_cur_domain' t \<sigma>; (\<sigma>, x) \<in> rf_sr; thread = ksCurThread \<sigma>; ksSchedulerAction_' (globals x) = NULL; ko_at' ko (ksCurThread \<sigma>) \<sigma>; cslift x (tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>)) = Some ko'; ret__unsigned_long_' t = SCAST(32 signed \<rightarrow> 32) false; tcbFaultHandler ko = tcbFaultHandler_C ko'; tsType_CL (thread_state_lift (tcbState_C ko')) = 6; tcbIPCBuffer ko = tcbIPCBuffer_C ko'; carch_tcb_relation (tcbArch ko) (tcbArch_C ko'); tcbQueued ko = to_bool (tcbQueued_CL (thread_state_lift (tcbState_C ko'))); UCAST(8 \<rightarrow> 32) (tcbDomain ko) = tcbDomain_C ko'; UCAST(8 \<rightarrow> 32) (tcbPriority ko) = tcbPriority_C ko'; UCAST(8 \<rightarrow> 32) (tcbMCP ko) = tcbMCP_C ko'; tcbTimeSlice ko = unat (tcbTimeSlice_C ko'); cfault_rel (tcbFault ko) (seL4_Fault_lift (tcbFault_C ko')) (lookup_fault_lift (tcbLookupFailure_C ko')); option_to_ptr (tcbBoundNotification ko) = tcbBoundNotification_C ko'; tcbState ko = Structures_H.thread_state.BlockedOnNotification (blockingObject_CL (thread_state_lift (tcbState_C ko')))\<rbrakk> \<Longrightarrow> ksSchedulerAction \<sigma> = ResumeCurrentThread
 4. \<And>\<sigma> x ko ko' t. \<lbrakk>\<forall>t. ksSchedulerAction \<sigma> = SwitchToThread t \<longrightarrow> st_tcb_at' runnable' t \<sigma> \<and> tcb_in_cur_domain' t \<sigma>; (\<sigma>, x) \<in> rf_sr; thread = ksCurThread \<sigma>; ksSchedulerAction_' (globals x) = NULL; ko_at' ko (ksCurThread \<sigma>) \<sigma>; cslift x (tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>)) = Some ko'; ret__unsigned_long_' t = SCAST(32 signed \<rightarrow> 32) false; tcbFaultHandler ko = tcbFaultHandler_C ko'; tsType_CL (thread_state_lift (tcbState_C ko')) = 0; tcbIPCBuffer ko = tcbIPCBuffer_C ko'; carch_tcb_relation (tcbArch ko) (tcbArch_C ko'); tcbQueued ko = to_bool (tcbQueued_CL (thread_state_lift (tcbState_C ko'))); UCAST(8 \<rightarrow> 32) (tcbDomain ko) = tcbDomain_C ko'; UCAST(8 \<rightarrow> 32) (tcbPriority ko) = tcbPriority_C ko'; UCAST(8 \<rightarrow> 32) (tcbMCP ko) = tcbMCP_C ko'; tcbTimeSlice ko = unat (tcbTimeSlice_C ko'); cfault_rel (tcbFault ko) (seL4_Fault_lift (tcbFault_C ko')) (lookup_fault_lift (tcbLookupFailure_C ko')); option_to_ptr (tcbBoundNotification ko) = tcbBoundNotification_C ko'; tcbState ko = Structures_H.thread_state.Inactive\<rbrakk> \<Longrightarrow> ksSchedulerAction \<sigma> = ResumeCurrentThread
 5. \<And>\<sigma> x ko ko' t. \<lbrakk>\<forall>t. ksSchedulerAction \<sigma> = SwitchToThread t \<longrightarrow> st_tcb_at' runnable' t \<sigma> \<and> tcb_in_cur_domain' t \<sigma>; (\<sigma>, x) \<in> rf_sr; thread = ksCurThread \<sigma>; ksSchedulerAction_' (globals x) = NULL; ko_at' ko (ksCurThread \<sigma>) \<sigma>; cslift x (tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>)) = Some ko'; ret__unsigned_long_' t = SCAST(32 signed \<rightarrow> 32) false; tcbFaultHandler ko = tcbFaultHandler_C ko'; tsType_CL (thread_state_lift (tcbState_C ko')) = 7; tcbIPCBuffer ko = tcbIPCBuffer_C ko'; carch_tcb_relation (tcbArch ko) (tcbArch_C ko'); tcbQueued ko = to_bool (tcbQueued_CL (thread_state_lift (tcbState_C ko'))); UCAST(8 \<rightarrow> 32) (tcbDomain ko) = tcbDomain_C ko'; UCAST(8 \<rightarrow> 32) (tcbPriority ko) = tcbPriority_C ko'; UCAST(8 \<rightarrow> 32) (tcbMCP ko) = tcbMCP_C ko'; tcbTimeSlice ko = unat (tcbTimeSlice_C ko'); cfault_rel (tcbFault ko) (seL4_Fault_lift (tcbFault_C ko')) (lookup_fault_lift (tcbLookupFailure_C ko')); option_to_ptr (tcbBoundNotification ko) = tcbBoundNotification_C ko'; idle' (tcbState ko)\<rbrakk> \<Longrightarrow> ksSchedulerAction \<sigma> = ResumeCurrentThread
 6. \<And>\<sigma> x ko ko' t. \<lbrakk>\<forall>t. ksSchedulerAction \<sigma> = SwitchToThread t \<longrightarrow> st_tcb_at' runnable' t \<sigma> \<and> tcb_in_cur_domain' t \<sigma>; (\<sigma>, x) \<in> rf_sr; thread = ksCurThread \<sigma>; ksSchedulerAction_' (globals x) = NULL; ko_at' ko (ksCurThread \<sigma>) \<sigma>; cslift x (tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>)) = Some ko'; ret__unsigned_long_' t = SCAST(32 signed \<rightarrow> 32) false; tcbFaultHandler ko = tcbFaultHandler_C ko'; tsType_CL (thread_state_lift (tcbState_C ko')) = 4; tcbIPCBuffer ko = tcbIPCBuffer_C ko'; carch_tcb_relation (tcbArch ko) (tcbArch_C ko'); tcbQueued ko = to_bool (tcbQueued_CL (thread_state_lift (tcbState_C ko'))); UCAST(8 \<rightarrow> 32) (tcbDomain ko) = tcbDomain_C ko'; UCAST(8 \<rightarrow> 32) (tcbPriority ko) = tcbPriority_C ko'; UCAST(8 \<rightarrow> 32) (tcbMCP ko) = tcbMCP_C ko'; tcbTimeSlice ko = unat (tcbTimeSlice_C ko'); cfault_rel (tcbFault ko) (seL4_Fault_lift (tcbFault_C ko')) (lookup_fault_lift (tcbLookupFailure_C ko')); option_to_ptr (tcbBoundNotification ko) = tcbBoundNotification_C ko'; tcbState ko = Structures_H.thread_state.BlockedOnSend (blockingObject_CL (thread_state_lift (tcbState_C ko'))) (blockingIPCBadge_CL (thread_state_lift (tcbState_C ko'))) (to_bool (blockingIPCCanGrant_CL (thread_state_lift (tcbState_C ko')))) (to_bool (blockingIPCCanGrantReply_CL (thread_state_lift (tcbState_C ko')))) (to_bool (blockingIPCIsCall_CL (thread_state_lift (tcbState_C ko'))))\<rbrakk> \<Longrightarrow> ksSchedulerAction \<sigma> = ResumeCurrentThread
 7. \<And>runnable \<sigma> x. \<lbrakk>st_tcb_at' (\<lambda>st. runnable' st = runnable) (ksCurThread \<sigma>) \<sigma>; weak_sch_act_wf (ksSchedulerAction \<sigma>) \<sigma>; (\<sigma>, x) \<in> rf_sr; thread = ksCurThread \<sigma>\<rbrakk> \<Longrightarrow> ksSchedulerAction_' (globals x) \<noteq> NULL \<longrightarrow> runnable \<or> ksSchedulerAction \<sigma> \<noteq> ResumeCurrentThread
 8. \<And>tptr runnable curThread s. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<lbrace>(=) s\<rbrace> getSchedulerAction \<lbrace>\<lambda>r. (=) s\<rbrace>
 9. \<And>tptr runnable curThread. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<lbrace>?P231 tptr runnable curThread\<rbrace> getSchedulerAction \<lbrace>\<lambda>action s. st_tcb_at' (\<lambda>st. runnable' st = runnable) thread s \<and> curThread = ksCurThread s \<and> action = ksSchedulerAction s \<and> weak_sch_act_wf (ksSchedulerAction s) s\<rbrace>
 10. \<And>tptr runnable curThread. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> empty_fail getSchedulerAction
A total of 16 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>\<sigma> x ko ko' t. \<lbrakk>\<forall>t. ksSchedulerAction \<sigma> = SwitchToThread t \<longrightarrow> st_tcb_at' runnable' t \<sigma> \<and> tcb_in_cur_domain' t \<sigma>; (\<sigma>, x) \<in> rf_sr; thread = ksCurThread \<sigma>; ksSchedulerAction_' (globals x) = NULL; ko_at' ko (ksCurThread \<sigma>) \<sigma>; cslift x (tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>)) = Some ko'; ret__unsigned_long_' t = SCAST(32 signed \<rightarrow> 32) false; tcbFaultHandler ko = tcbFaultHandler_C ko'\<rbrakk> \<Longrightarrow> (\<lbrakk>tsType_CL (thread_state_lift (tcbState_C ko')) = 3; tcbIPCBuffer ko = tcbIPCBuffer_C ko'; carch_tcb_relation (tcbArch ko) (tcbArch_C ko'); tcbQueued ko = to_bool (tcbQueued_CL (thread_state_lift (tcbState_C ko'))); UCAST(8 \<rightarrow> 32) (tcbDomain ko) = tcbDomain_C ko'; UCAST(8 \<rightarrow> 32) (tcbPriority ko) = tcbPriority_C ko'; UCAST(8 \<rightarrow> 32) (tcbMCP ko) = tcbMCP_C ko'; tcbTimeSlice ko = unat (tcbTimeSlice_C ko'); cfault_rel (tcbFault ko) (seL4_Fault_lift (tcbFault_C ko')) (lookup_fault_lift (tcbLookupFailure_C ko')); option_to_ptr (tcbBoundNotification ko) = tcbBoundNotification_C ko'; tcbState ko = Structures_H.thread_state.BlockedOnReceive (blockingObject_CL (thread_state_lift (tcbState_C ko'))) (to_bool (blockingIPCCanGrant_CL (thread_state_lift (tcbState_C ko'))))\<rbrakk> \<Longrightarrow> ksSchedulerAction \<sigma> = ResumeCurrentThread) &&& (\<lbrakk>tsType_CL (thread_state_lift (tcbState_C ko')) = 5; tcbIPCBuffer ko = tcbIPCBuffer_C ko'; carch_tcb_relation (tcbArch ko) (tcbArch_C ko'); tcbQueued ko = to_bool (tcbQueued_CL (thread_state_lift (tcbState_C ko'))); UCAST(8 \<rightarrow> 32) (tcbDomain ko) = tcbDomain_C ko'; UCAST(8 \<rightarrow> 32) (tcbPriority ko) = tcbPriority_C ko'; UCAST(8 \<rightarrow> 32) (tcbMCP ko) = tcbMCP_C ko'; tcbTimeSlice ko = unat (tcbTimeSlice_C ko'); cfault_rel (tcbFault ko) (seL4_Fault_lift (tcbFault_C ko')) (lookup_fault_lift (tcbLookupFailure_C ko')); option_to_ptr (tcbBoundNotification ko) = tcbBoundNotification_C ko'; awaiting_reply' (tcbState ko)\<rbrakk> \<Longrightarrow> ksSchedulerAction \<sigma> = ResumeCurrentThread) &&& (\<lbrakk>tsType_CL (thread_state_lift (tcbState_C ko')) = 6; tcbIPCBuffer ko = tcbIPCBuffer_C ko'; carch_tcb_relation (tcbArch ko) (tcbArch_C ko'); tcbQueued ko = to_bool (tcbQueued_CL (thread_state_lift (tcbState_C ko'))); UCAST(8 \<rightarrow> 32) (tcbDomain ko) = tcbDomain_C ko'; UCAST(8 \<rightarrow> 32) (tcbPriority ko) = tcbPriority_C ko'; UCAST(8 \<rightarrow> 32) (tcbMCP ko) = tcbMCP_C ko'; tcbTimeSlice ko = unat (tcbTimeSlice_C ko'); cfault_rel (tcbFault ko) (seL4_Fault_lift (tcbFault_C ko')) (lookup_fault_lift (tcbLookupFailure_C ko')); option_to_ptr (tcbBoundNotification ko) = tcbBoundNotification_C ko'; tcbState ko = Structures_H.thread_state.BlockedOnNotification (blockingObject_CL (thread_state_lift (tcbState_C ko')))\<rbrakk> \<Longrightarrow> ksSchedulerAction \<sigma> = ResumeCurrentThread) &&& (\<lbrakk>tsType_CL (thread_state_lift (tcbState_C ko')) = 0; tcbIPCBuffer ko = tcbIPCBuffer_C ko'; carch_tcb_relation (tcbArch ko) (tcbArch_C ko'); tcbQueued ko = to_bool (tcbQueued_CL (thread_state_lift (tcbState_C ko'))); UCAST(8 \<rightarrow> 32) (tcbDomain ko) = tcbDomain_C ko'; UCAST(8 \<rightarrow> 32) (tcbPriority ko) = tcbPriority_C ko'; UCAST(8 \<rightarrow> 32) (tcbMCP ko) = tcbMCP_C ko'; tcbTimeSlice ko = unat (tcbTimeSlice_C ko'); cfault_rel (tcbFault ko) (seL4_Fault_lift (tcbFault_C ko')) (lookup_fault_lift (tcbLookupFailure_C ko')); option_to_ptr (tcbBoundNotification ko) = tcbBoundNotification_C ko'; tcbState ko = Structures_H.thread_state.Inactive\<rbrakk> \<Longrightarrow> ksSchedulerAction \<sigma> = ResumeCurrentThread) &&& (\<lbrakk>tsType_CL (thread_state_lift (tcbState_C ko')) = 7; tcbIPCBuffer ko = tcbIPCBuffer_C ko'; carch_tcb_relation (tcbArch ko) (tcbArch_C ko'); tcbQueued ko = to_bool (tcbQueued_CL (thread_state_lift (tcbState_C ko'))); UCAST(8 \<rightarrow> 32) (tcbDomain ko) = tcbDomain_C ko'; UCAST(8 \<rightarrow> 32) (tcbPriority ko) = tcbPriority_C ko'; UCAST(8 \<rightarrow> 32) (tcbMCP ko) = tcbMCP_C ko'; tcbTimeSlice ko = unat (tcbTimeSlice_C ko'); cfault_rel (tcbFault ko) (seL4_Fault_lift (tcbFault_C ko')) (lookup_fault_lift (tcbLookupFailure_C ko')); option_to_ptr (tcbBoundNotification ko) = tcbBoundNotification_C ko'; idle' (tcbState ko)\<rbrakk> \<Longrightarrow> ksSchedulerAction \<sigma> = ResumeCurrentThread) &&& (\<lbrakk>tsType_CL (thread_state_lift (tcbState_C ko')) = 4; tcbIPCBuffer ko = tcbIPCBuffer_C ko'; carch_tcb_relation (tcbArch ko) (tcbArch_C ko'); tcbQueued ko = to_bool (tcbQueued_CL (thread_state_lift (tcbState_C ko'))); UCAST(8 \<rightarrow> 32) (tcbDomain ko) = tcbDomain_C ko'; UCAST(8 \<rightarrow> 32) (tcbPriority ko) = tcbPriority_C ko'; UCAST(8 \<rightarrow> 32) (tcbMCP ko) = tcbMCP_C ko'; tcbTimeSlice ko = unat (tcbTimeSlice_C ko'); cfault_rel (tcbFault ko) (seL4_Fault_lift (tcbFault_C ko')) (lookup_fault_lift (tcbLookupFailure_C ko')); option_to_ptr (tcbBoundNotification ko) = tcbBoundNotification_C ko'; tcbState ko = Structures_H.thread_state.BlockedOnSend (blockingObject_CL (thread_state_lift (tcbState_C ko'))) (blockingIPCBadge_CL (thread_state_lift (tcbState_C ko'))) (to_bool (blockingIPCCanGrant_CL (thread_state_lift (tcbState_C ko')))) (to_bool (blockingIPCCanGrantReply_CL (thread_state_lift (tcbState_C ko')))) (to_bool (blockingIPCIsCall_CL (thread_state_lift (tcbState_C ko'))))\<rbrakk> \<Longrightarrow> ksSchedulerAction \<sigma> = ResumeCurrentThread)
 2. \<And>runnable \<sigma> x. \<lbrakk>st_tcb_at' (\<lambda>st. runnable' st = runnable) (ksCurThread \<sigma>) \<sigma>; weak_sch_act_wf (ksSchedulerAction \<sigma>) \<sigma>; (\<sigma>, x) \<in> rf_sr; thread = ksCurThread \<sigma>\<rbrakk> \<Longrightarrow> ksSchedulerAction_' (globals x) \<noteq> NULL \<longrightarrow> runnable \<or> ksSchedulerAction \<sigma> \<noteq> ResumeCurrentThread
 3. \<And>tptr runnable curThread s. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<lbrace>(=) s\<rbrace> getSchedulerAction \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<And>tptr runnable curThread. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<lbrace>?P7 tptr runnable curThread\<rbrace> getSchedulerAction \<lbrace>\<lambda>action s. st_tcb_at' (\<lambda>st. runnable' st = runnable) thread s \<and> curThread = ksCurThread s \<and> action = ksSchedulerAction s \<and> weak_sch_act_wf (ksSchedulerAction s) s\<rbrace>
 5. \<And>tptr runnable curThread. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> empty_fail getSchedulerAction
 6. \<And>tptr s. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<lbrace>(=) s\<rbrace> isRunnable thread \<lbrace>\<lambda>r. (=) s\<rbrace>
 7. \<And>tptr. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<lbrace>?Pa7 tptr\<rbrace> isRunnable thread \<lbrace>\<lambda>runnable s. \<forall>rv. ksCurThread s = rv \<longrightarrow> ?P7 tptr runnable rv s\<rbrace>
 8. \<And>tptr. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> empty_fail (isRunnable thread)
 9. \<And>tptr. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<lbrace>?R7 tptr\<rbrace> do runnable <- isRunnable thread;
curThread <- getCurThread;
action <- getSchedulerAction;
return (runnable, curThread, action)
od \<lbrace>\<lambda>rv. (\<lambda>_. True) and (\<lambda>s. \<not> fst rv \<and> fst (snd rv) = thread \<and> snd (snd rv) = ResumeCurrentThread \<longrightarrow> (Invariants_H.valid_queues and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and valid_objs') s) and (\<lambda>s. \<not> (\<not> fst rv \<and> fst (snd rv) = thread \<and> snd (snd rv) = ResumeCurrentThread) \<longrightarrow> True)\<rbrace>
 10. \<And>tptr. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> guard_is_UNIV (\<lambda>rv rv'. (\<not> fst rv \<and> fst (snd rv) = thread \<and> snd (snd rv) = ResumeCurrentThread) = (rv' \<noteq> 0)) ret__int_' (\<lambda>rv rv'. {s. (s \<in> \<lbrace>rv' \<noteq> 0\<rbrace> \<longrightarrow> s \<in> {s. s \<in> UNIV}) \<and> (s \<notin> \<lbrace>rv' \<noteq> 0\<rbrace> \<longrightarrow> s \<in> UNIV)})
A total of 11 subgoals... proof (prove)
goal (1 subgoal):
 1. (\<lbrakk>tsType_CL (thread_state_lift (tcbState_C ko'_)) = 3; tcbIPCBuffer ko_ = tcbIPCBuffer_C ko'_; carch_tcb_relation (tcbArch ko_) (tcbArch_C ko'_); tcbQueued ko_ = to_bool (tcbQueued_CL (thread_state_lift (tcbState_C ko'_))); UCAST(8 \<rightarrow> 32) (tcbDomain ko_) = tcbDomain_C ko'_; UCAST(8 \<rightarrow> 32) (tcbPriority ko_) = tcbPriority_C ko'_; UCAST(8 \<rightarrow> 32) (tcbMCP ko_) = tcbMCP_C ko'_; tcbTimeSlice ko_ = unat (tcbTimeSlice_C ko'_); cfault_rel (tcbFault ko_) (seL4_Fault_lift (tcbFault_C ko'_)) (lookup_fault_lift (tcbLookupFailure_C ko'_)); option_to_ptr (tcbBoundNotification ko_) = tcbBoundNotification_C ko'_; tcbState ko_ = Structures_H.thread_state.BlockedOnReceive (blockingObject_CL (thread_state_lift (tcbState_C ko'_))) (to_bool (blockingIPCCanGrant_CL (thread_state_lift (tcbState_C ko'_))))\<rbrakk> \<Longrightarrow> ksSchedulerAction \<sigma>_ = ResumeCurrentThread) &&& (\<lbrakk>tsType_CL (thread_state_lift (tcbState_C ko'_)) = 5; tcbIPCBuffer ko_ = tcbIPCBuffer_C ko'_; carch_tcb_relation (tcbArch ko_) (tcbArch_C ko'_); tcbQueued ko_ = to_bool (tcbQueued_CL (thread_state_lift (tcbState_C ko'_))); UCAST(8 \<rightarrow> 32) (tcbDomain ko_) = tcbDomain_C ko'_; UCAST(8 \<rightarrow> 32) (tcbPriority ko_) = tcbPriority_C ko'_; UCAST(8 \<rightarrow> 32) (tcbMCP ko_) = tcbMCP_C ko'_; tcbTimeSlice ko_ = unat (tcbTimeSlice_C ko'_); cfault_rel (tcbFault ko_) (seL4_Fault_lift (tcbFault_C ko'_)) (lookup_fault_lift (tcbLookupFailure_C ko'_)); option_to_ptr (tcbBoundNotification ko_) = tcbBoundNotification_C ko'_; awaiting_reply' (tcbState ko_)\<rbrakk> \<Longrightarrow> ksSchedulerAction \<sigma>_ = ResumeCurrentThread) &&& (\<lbrakk>tsType_CL (thread_state_lift (tcbState_C ko'_)) = 6; tcbIPCBuffer ko_ = tcbIPCBuffer_C ko'_; carch_tcb_relation (tcbArch ko_) (tcbArch_C ko'_); tcbQueued ko_ = to_bool (tcbQueued_CL (thread_state_lift (tcbState_C ko'_))); UCAST(8 \<rightarrow> 32) (tcbDomain ko_) = tcbDomain_C ko'_; UCAST(8 \<rightarrow> 32) (tcbPriority ko_) = tcbPriority_C ko'_; UCAST(8 \<rightarrow> 32) (tcbMCP ko_) = tcbMCP_C ko'_; tcbTimeSlice ko_ = unat (tcbTimeSlice_C ko'_); cfault_rel (tcbFault ko_) (seL4_Fault_lift (tcbFault_C ko'_)) (lookup_fault_lift (tcbLookupFailure_C ko'_)); option_to_ptr (tcbBoundNotification ko_) = tcbBoundNotification_C ko'_; tcbState ko_ = Structures_H.thread_state.BlockedOnNotification (blockingObject_CL (thread_state_lift (tcbState_C ko'_)))\<rbrakk> \<Longrightarrow> ksSchedulerAction \<sigma>_ = ResumeCurrentThread) &&& (\<lbrakk>tsType_CL (thread_state_lift (tcbState_C ko'_)) = 0; tcbIPCBuffer ko_ = tcbIPCBuffer_C ko'_; carch_tcb_relation (tcbArch ko_) (tcbArch_C ko'_); tcbQueued ko_ = to_bool (tcbQueued_CL (thread_state_lift (tcbState_C ko'_))); UCAST(8 \<rightarrow> 32) (tcbDomain ko_) = tcbDomain_C ko'_; UCAST(8 \<rightarrow> 32) (tcbPriority ko_) = tcbPriority_C ko'_; UCAST(8 \<rightarrow> 32) (tcbMCP ko_) = tcbMCP_C ko'_; tcbTimeSlice ko_ = unat (tcbTimeSlice_C ko'_); cfault_rel (tcbFault ko_) (seL4_Fault_lift (tcbFault_C ko'_)) (lookup_fault_lift (tcbLookupFailure_C ko'_)); option_to_ptr (tcbBoundNotification ko_) = tcbBoundNotification_C ko'_; tcbState ko_ = Structures_H.thread_state.Inactive\<rbrakk> \<Longrightarrow> ksSchedulerAction \<sigma>_ = ResumeCurrentThread) &&& (\<lbrakk>tsType_CL (thread_state_lift (tcbState_C ko'_)) = 7; tcbIPCBuffer ko_ = tcbIPCBuffer_C ko'_; carch_tcb_relation (tcbArch ko_) (tcbArch_C ko'_); tcbQueued ko_ = to_bool (tcbQueued_CL (thread_state_lift (tcbState_C ko'_))); UCAST(8 \<rightarrow> 32) (tcbDomain ko_) = tcbDomain_C ko'_; UCAST(8 \<rightarrow> 32) (tcbPriority ko_) = tcbPriority_C ko'_; UCAST(8 \<rightarrow> 32) (tcbMCP ko_) = tcbMCP_C ko'_; tcbTimeSlice ko_ = unat (tcbTimeSlice_C ko'_); cfault_rel (tcbFault ko_) (seL4_Fault_lift (tcbFault_C ko'_)) (lookup_fault_lift (tcbLookupFailure_C ko'_)); option_to_ptr (tcbBoundNotification ko_) = tcbBoundNotification_C ko'_; idle' (tcbState ko_)\<rbrakk> \<Longrightarrow> ksSchedulerAction \<sigma>_ = ResumeCurrentThread) &&& (\<lbrakk>tsType_CL (thread_state_lift (tcbState_C ko'_)) = 4; tcbIPCBuffer ko_ = tcbIPCBuffer_C ko'_; carch_tcb_relation (tcbArch ko_) (tcbArch_C ko'_); tcbQueued ko_ = to_bool (tcbQueued_CL (thread_state_lift (tcbState_C ko'_))); UCAST(8 \<rightarrow> 32) (tcbDomain ko_) = tcbDomain_C ko'_; UCAST(8 \<rightarrow> 32) (tcbPriority ko_) = tcbPriority_C ko'_; UCAST(8 \<rightarrow> 32) (tcbMCP ko_) = tcbMCP_C ko'_; tcbTimeSlice ko_ = unat (tcbTimeSlice_C ko'_); cfault_rel (tcbFault ko_) (seL4_Fault_lift (tcbFault_C ko'_)) (lookup_fault_lift (tcbLookupFailure_C ko'_)); option_to_ptr (tcbBoundNotification ko_) = tcbBoundNotification_C ko'_; tcbState ko_ = Structures_H.thread_state.BlockedOnSend (blockingObject_CL (thread_state_lift (tcbState_C ko'_))) (blockingIPCBadge_CL (thread_state_lift (tcbState_C ko'_))) (to_bool (blockingIPCCanGrant_CL (thread_state_lift (tcbState_C ko'_)))) (to_bool (blockingIPCCanGrantReply_CL (thread_state_lift (tcbState_C ko'_)))) (to_bool (blockingIPCIsCall_CL (thread_state_lift (tcbState_C ko'_))))\<rbrakk> \<Longrightarrow> ksSchedulerAction \<sigma>_ = ResumeCurrentThread) proof (prove)
using this:
\<forall>t. ksSchedulerAction \<sigma>_ = SwitchToThread t \<longrightarrow> st_tcb_at' runnable' t \<sigma>_ \<and> tcb_in_cur_domain' t \<sigma>_
(\<sigma>_, x_) \<in> rf_sr
thread = ksCurThread \<sigma>_
ksSchedulerAction_' (globals x_) = NULL
ko_at' ko_ (ksCurThread \<sigma>_) \<sigma>_
cslift x_ (tcb_ptr_to_ctcb_ptr (ksCurThread \<sigma>_)) = Some ko'_
ret__unsigned_long_' t_ = SCAST(32 signed \<rightarrow> 32) false
tcbFaultHandler ko_ = tcbFaultHandler_C ko'_

goal (1 subgoal):
 1. (\<lbrakk>tsType_CL (thread_state_lift (tcbState_C ko'_)) = 3; tcbIPCBuffer ko_ = tcbIPCBuffer_C ko'_; carch_tcb_relation (tcbArch ko_) (tcbArch_C ko'_); tcbQueued ko_ = to_bool (tcbQueued_CL (thread_state_lift (tcbState_C ko'_))); UCAST(8 \<rightarrow> 32) (tcbDomain ko_) = tcbDomain_C ko'_; UCAST(8 \<rightarrow> 32) (tcbPriority ko_) = tcbPriority_C ko'_; UCAST(8 \<rightarrow> 32) (tcbMCP ko_) = tcbMCP_C ko'_; tcbTimeSlice ko_ = unat (tcbTimeSlice_C ko'_); cfault_rel (tcbFault ko_) (seL4_Fault_lift (tcbFault_C ko'_)) (lookup_fault_lift (tcbLookupFailure_C ko'_)); option_to_ptr (tcbBoundNotification ko_) = tcbBoundNotification_C ko'_; tcbState ko_ = Structures_H.thread_state.BlockedOnReceive (blockingObject_CL (thread_state_lift (tcbState_C ko'_))) (to_bool (blockingIPCCanGrant_CL (thread_state_lift (tcbState_C ko'_))))\<rbrakk> \<Longrightarrow> ksSchedulerAction \<sigma>_ = ResumeCurrentThread) &&& (\<lbrakk>tsType_CL (thread_state_lift (tcbState_C ko'_)) = 5; tcbIPCBuffer ko_ = tcbIPCBuffer_C ko'_; carch_tcb_relation (tcbArch ko_) (tcbArch_C ko'_); tcbQueued ko_ = to_bool (tcbQueued_CL (thread_state_lift (tcbState_C ko'_))); UCAST(8 \<rightarrow> 32) (tcbDomain ko_) = tcbDomain_C ko'_; UCAST(8 \<rightarrow> 32) (tcbPriority ko_) = tcbPriority_C ko'_; UCAST(8 \<rightarrow> 32) (tcbMCP ko_) = tcbMCP_C ko'_; tcbTimeSlice ko_ = unat (tcbTimeSlice_C ko'_); cfault_rel (tcbFault ko_) (seL4_Fault_lift (tcbFault_C ko'_)) (lookup_fault_lift (tcbLookupFailure_C ko'_)); option_to_ptr (tcbBoundNotification ko_) = tcbBoundNotification_C ko'_; awaiting_reply' (tcbState ko_)\<rbrakk> \<Longrightarrow> ksSchedulerAction \<sigma>_ = ResumeCurrentThread) &&& (\<lbrakk>tsType_CL (thread_state_lift (tcbState_C ko'_)) = 6; tcbIPCBuffer ko_ = tcbIPCBuffer_C ko'_; carch_tcb_relation (tcbArch ko_) (tcbArch_C ko'_); tcbQueued ko_ = to_bool (tcbQueued_CL (thread_state_lift (tcbState_C ko'_))); UCAST(8 \<rightarrow> 32) (tcbDomain ko_) = tcbDomain_C ko'_; UCAST(8 \<rightarrow> 32) (tcbPriority ko_) = tcbPriority_C ko'_; UCAST(8 \<rightarrow> 32) (tcbMCP ko_) = tcbMCP_C ko'_; tcbTimeSlice ko_ = unat (tcbTimeSlice_C ko'_); cfault_rel (tcbFault ko_) (seL4_Fault_lift (tcbFault_C ko'_)) (lookup_fault_lift (tcbLookupFailure_C ko'_)); option_to_ptr (tcbBoundNotification ko_) = tcbBoundNotification_C ko'_; tcbState ko_ = Structures_H.thread_state.BlockedOnNotification (blockingObject_CL (thread_state_lift (tcbState_C ko'_)))\<rbrakk> \<Longrightarrow> ksSchedulerAction \<sigma>_ = ResumeCurrentThread) &&& (\<lbrakk>tsType_CL (thread_state_lift (tcbState_C ko'_)) = 0; tcbIPCBuffer ko_ = tcbIPCBuffer_C ko'_; carch_tcb_relation (tcbArch ko_) (tcbArch_C ko'_); tcbQueued ko_ = to_bool (tcbQueued_CL (thread_state_lift (tcbState_C ko'_))); UCAST(8 \<rightarrow> 32) (tcbDomain ko_) = tcbDomain_C ko'_; UCAST(8 \<rightarrow> 32) (tcbPriority ko_) = tcbPriority_C ko'_; UCAST(8 \<rightarrow> 32) (tcbMCP ko_) = tcbMCP_C ko'_; tcbTimeSlice ko_ = unat (tcbTimeSlice_C ko'_); cfault_rel (tcbFault ko_) (seL4_Fault_lift (tcbFault_C ko'_)) (lookup_fault_lift (tcbLookupFailure_C ko'_)); option_to_ptr (tcbBoundNotification ko_) = tcbBoundNotification_C ko'_; tcbState ko_ = Structures_H.thread_state.Inactive\<rbrakk> \<Longrightarrow> ksSchedulerAction \<sigma>_ = ResumeCurrentThread) &&& (\<lbrakk>tsType_CL (thread_state_lift (tcbState_C ko'_)) = 7; tcbIPCBuffer ko_ = tcbIPCBuffer_C ko'_; carch_tcb_relation (tcbArch ko_) (tcbArch_C ko'_); tcbQueued ko_ = to_bool (tcbQueued_CL (thread_state_lift (tcbState_C ko'_))); UCAST(8 \<rightarrow> 32) (tcbDomain ko_) = tcbDomain_C ko'_; UCAST(8 \<rightarrow> 32) (tcbPriority ko_) = tcbPriority_C ko'_; UCAST(8 \<rightarrow> 32) (tcbMCP ko_) = tcbMCP_C ko'_; tcbTimeSlice ko_ = unat (tcbTimeSlice_C ko'_); cfault_rel (tcbFault ko_) (seL4_Fault_lift (tcbFault_C ko'_)) (lookup_fault_lift (tcbLookupFailure_C ko'_)); option_to_ptr (tcbBoundNotification ko_) = tcbBoundNotification_C ko'_; idle' (tcbState ko_)\<rbrakk> \<Longrightarrow> ksSchedulerAction \<sigma>_ = ResumeCurrentThread) &&& (\<lbrakk>tsType_CL (thread_state_lift (tcbState_C ko'_)) = 4; tcbIPCBuffer ko_ = tcbIPCBuffer_C ko'_; carch_tcb_relation (tcbArch ko_) (tcbArch_C ko'_); tcbQueued ko_ = to_bool (tcbQueued_CL (thread_state_lift (tcbState_C ko'_))); UCAST(8 \<rightarrow> 32) (tcbDomain ko_) = tcbDomain_C ko'_; UCAST(8 \<rightarrow> 32) (tcbPriority ko_) = tcbPriority_C ko'_; UCAST(8 \<rightarrow> 32) (tcbMCP ko_) = tcbMCP_C ko'_; tcbTimeSlice ko_ = unat (tcbTimeSlice_C ko'_); cfault_rel (tcbFault ko_) (seL4_Fault_lift (tcbFault_C ko'_)) (lookup_fault_lift (tcbLookupFailure_C ko'_)); option_to_ptr (tcbBoundNotification ko_) = tcbBoundNotification_C ko'_; tcbState ko_ = Structures_H.thread_state.BlockedOnSend (blockingObject_CL (thread_state_lift (tcbState_C ko'_))) (blockingIPCBadge_CL (thread_state_lift (tcbState_C ko'_))) (to_bool (blockingIPCCanGrant_CL (thread_state_lift (tcbState_C ko'_)))) (to_bool (blockingIPCCanGrantReply_CL (thread_state_lift (tcbState_C ko'_)))) (to_bool (blockingIPCIsCall_CL (thread_state_lift (tcbState_C ko'_))))\<rbrakk> \<Longrightarrow> ksSchedulerAction \<sigma>_ = ResumeCurrentThread) proof (prove)
goal (10 subgoals):
 1. \<And>runnable \<sigma> x. \<lbrakk>st_tcb_at' (\<lambda>st. runnable' st = runnable) (ksCurThread \<sigma>) \<sigma>; weak_sch_act_wf (ksSchedulerAction \<sigma>) \<sigma>; (\<sigma>, x) \<in> rf_sr; thread = ksCurThread \<sigma>\<rbrakk> \<Longrightarrow> ksSchedulerAction_' (globals x) \<noteq> NULL \<longrightarrow> runnable \<or> ksSchedulerAction \<sigma> \<noteq> ResumeCurrentThread
 2. \<And>tptr runnable curThread s. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<lbrace>(=) s\<rbrace> getSchedulerAction \<lbrace>\<lambda>r. (=) s\<rbrace>
 3. \<And>tptr runnable curThread. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<lbrace>?P7 tptr runnable curThread\<rbrace> getSchedulerAction \<lbrace>\<lambda>action s. st_tcb_at' (\<lambda>st. runnable' st = runnable) thread s \<and> curThread = ksCurThread s \<and> action = ksSchedulerAction s \<and> weak_sch_act_wf (ksSchedulerAction s) s\<rbrace>
 4. \<And>tptr runnable curThread. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> empty_fail getSchedulerAction
 5. \<And>tptr s. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<lbrace>(=) s\<rbrace> isRunnable thread \<lbrace>\<lambda>r. (=) s\<rbrace>
 6. \<And>tptr. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<lbrace>?Pa7 tptr\<rbrace> isRunnable thread \<lbrace>\<lambda>runnable s. \<forall>rv. ksCurThread s = rv \<longrightarrow> ?P7 tptr runnable rv s\<rbrace>
 7. \<And>tptr. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> empty_fail (isRunnable thread)
 8. \<And>tptr. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<lbrace>?R7 tptr\<rbrace> do runnable <- isRunnable thread;
curThread <- getCurThread;
action <- getSchedulerAction;
return (runnable, curThread, action)
od \<lbrace>\<lambda>rv. (\<lambda>_. True) and (\<lambda>s. \<not> fst rv \<and> fst (snd rv) = thread \<and> snd (snd rv) = ResumeCurrentThread \<longrightarrow> (Invariants_H.valid_queues and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and valid_objs') s) and (\<lambda>s. \<not> (\<not> fst rv \<and> fst (snd rv) = thread \<and> snd (snd rv) = ResumeCurrentThread) \<longrightarrow> True)\<rbrace>
 9. \<And>tptr. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> guard_is_UNIV (\<lambda>rv rv'. (\<not> fst rv \<and> fst (snd rv) = thread \<and> snd (snd rv) = ResumeCurrentThread) = (rv' \<noteq> 0)) ret__int_' (\<lambda>rv rv'. {s. (s \<in> \<lbrace>rv' \<noteq> 0\<rbrace> \<longrightarrow> s \<in> {s. s \<in> UNIV}) \<and> (s \<notin> \<lbrace>rv' \<noteq> 0\<rbrace> \<longrightarrow> s \<in> UNIV)})
 10. \<And>tptr s s'. \<lbrakk>tptr = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; (tcb_at' thread and st_tcb_at' (not runnable') thread and valid_queues' and Invariants_H.valid_queues and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and valid_objs') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (?Pa7 tptr and ?R7 tptr) s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> (\<forall>rva. ksCurThread s = rva \<longrightarrow> ?P7 tptr rv rva s) \<longrightarrow> s' \<in> {s. \<forall>rva. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rva \<longrightarrow> s \<in> {s'. \<forall>rvb s. (s, s') \<in> rf_sr \<and> st_tcb_at' (\<lambda>st. runnable' st = rv) thread s \<and> rva = ksCurThread s \<and> rvb = ksSchedulerAction s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<longrightarrow> s' \<in> UNIV}}} proof (prove)
goal (9 subgoals):
 1. \<And>tptr runnable curThread s. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<lbrace>(=) s\<rbrace> getSchedulerAction \<lbrace>\<lambda>r. (=) s\<rbrace>
 2. \<And>tptr runnable curThread. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<lbrace>?P7 tptr runnable curThread\<rbrace> getSchedulerAction \<lbrace>\<lambda>action s. st_tcb_at' (\<lambda>st. runnable' st = runnable) thread s \<and> curThread = ksCurThread s \<and> action = ksSchedulerAction s \<and> weak_sch_act_wf (ksSchedulerAction s) s\<rbrace>
 3. \<And>tptr runnable curThread. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> empty_fail getSchedulerAction
 4. \<And>tptr s. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<lbrace>(=) s\<rbrace> isRunnable thread \<lbrace>\<lambda>r. (=) s\<rbrace>
 5. \<And>tptr. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<lbrace>?Pa7 tptr\<rbrace> isRunnable thread \<lbrace>\<lambda>runnable s. \<forall>rv. ksCurThread s = rv \<longrightarrow> ?P7 tptr runnable rv s\<rbrace>
 6. \<And>tptr. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> empty_fail (isRunnable thread)
 7. \<And>tptr. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<lbrace>?R7 tptr\<rbrace> do runnable <- isRunnable thread;
curThread <- getCurThread;
action <- getSchedulerAction;
return (runnable, curThread, action)
od \<lbrace>\<lambda>rv. (\<lambda>_. True) and (\<lambda>s. \<not> fst rv \<and> fst (snd rv) = thread \<and> snd (snd rv) = ResumeCurrentThread \<longrightarrow> (Invariants_H.valid_queues and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and valid_objs') s) and (\<lambda>s. \<not> (\<not> fst rv \<and> fst (snd rv) = thread \<and> snd (snd rv) = ResumeCurrentThread) \<longrightarrow> True)\<rbrace>
 8. \<And>tptr. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> guard_is_UNIV (\<lambda>rv rv'. (\<not> fst rv \<and> fst (snd rv) = thread \<and> snd (snd rv) = ResumeCurrentThread) = (rv' \<noteq> 0)) ret__int_' (\<lambda>rv rv'. {s. (s \<in> \<lbrace>rv' \<noteq> 0\<rbrace> \<longrightarrow> s \<in> {s. s \<in> UNIV}) \<and> (s \<notin> \<lbrace>rv' \<noteq> 0\<rbrace> \<longrightarrow> s \<in> UNIV)})
 9. \<And>tptr s s'. \<lbrakk>tptr = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; (tcb_at' thread and st_tcb_at' (not runnable') thread and valid_queues' and Invariants_H.valid_queues and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and valid_objs') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> (?Pa7 tptr and ?R7 tptr) s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> (\<forall>rva. ksCurThread s = rva \<longrightarrow> ?P7 tptr rv rva s) \<longrightarrow> s' \<in> {s. \<forall>rva. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rva \<longrightarrow> s \<in> {s'. \<forall>rvb s. (s, s') \<in> rf_sr \<and> st_tcb_at' (\<lambda>st. runnable' st = rv) thread s \<and> rva = ksCurThread s \<and> rvb = ksSchedulerAction s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<longrightarrow> s' \<in> UNIV}}} proof (prove)
goal (4 subgoals):
 1. \<And>tptr. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> empty_fail (isRunnable thread)
 2. \<And>tptr. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<lbrace>?R7 tptr\<rbrace> do runnable <- isRunnable thread;
curThread <- getCurThread;
action <- getSchedulerAction;
return (runnable, curThread, action)
od \<lbrace>\<lambda>rv. (\<lambda>_. True) and (\<lambda>s. \<not> fst rv \<and> fst (snd rv) = thread \<and> snd (snd rv) = ResumeCurrentThread \<longrightarrow> (Invariants_H.valid_queues and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and valid_objs') s) and (\<lambda>s. \<not> (\<not> fst rv \<and> fst (snd rv) = thread \<and> snd (snd rv) = ResumeCurrentThread) \<longrightarrow> True)\<rbrace>
 3. \<And>tptr. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> guard_is_UNIV (\<lambda>rv rv'. (\<not> fst rv \<and> fst (snd rv) = thread \<and> snd (snd rv) = ResumeCurrentThread) = (rv' \<noteq> 0)) ret__int_' (\<lambda>rv rv'. {s. (s \<in> \<lbrace>rv' \<noteq> 0\<rbrace> \<longrightarrow> s \<in> {s. s \<in> UNIV}) \<and> (s \<notin> \<lbrace>rv' \<noteq> 0\<rbrace> \<longrightarrow> s \<in> UNIV)})
 4. \<And>tptr s s'. \<lbrakk>tptr = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; (tcb_at' thread and st_tcb_at' (not runnable') thread and valid_queues' and Invariants_H.valid_queues and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and valid_objs') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>s. \<forall>rv. ksCurThread s = rv \<longrightarrow> st_tcb_at' (\<lambda>st. runnable' st = st_tcb_at' runnable' thread s) thread s \<and> rv = ksCurThread s \<and> ksSchedulerAction s = ksSchedulerAction s \<and> weak_sch_act_wf (ksSchedulerAction s) s) and ?R7 tptr) s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> (\<forall>rva. ksCurThread s = rva \<longrightarrow> st_tcb_at' (\<lambda>st. runnable' st = rv) thread s \<and> rva = ksCurThread s \<and> ksSchedulerAction s = ksSchedulerAction s \<and> weak_sch_act_wf (ksSchedulerAction s) s) \<longrightarrow> s' \<in> {s. \<forall>rva. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rva \<longrightarrow> s \<in> {s'. \<forall>rvb s. (s, s') \<in> rf_sr \<and> st_tcb_at' (\<lambda>st. runnable' st = rv) thread s \<and> rva = ksCurThread s \<and> rvb = ksSchedulerAction s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<longrightarrow> s' \<in> UNIV}}} proof (prove)
goal (3 subgoals):
 1. \<And>tptr. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<lbrace>?R7 tptr\<rbrace> do runnable <- isRunnable thread;
curThread <- getCurThread;
action <- getSchedulerAction;
return (runnable, curThread, action)
od \<lbrace>\<lambda>rv. (\<lambda>_. True) and (\<lambda>s. \<not> fst rv \<and> fst (snd rv) = thread \<and> snd (snd rv) = ResumeCurrentThread \<longrightarrow> (Invariants_H.valid_queues and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and valid_objs') s) and (\<lambda>s. \<not> (\<not> fst rv \<and> fst (snd rv) = thread \<and> snd (snd rv) = ResumeCurrentThread) \<longrightarrow> True)\<rbrace>
 2. \<And>tptr. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> guard_is_UNIV (\<lambda>rv rv'. (\<not> fst rv \<and> fst (snd rv) = thread \<and> snd (snd rv) = ResumeCurrentThread) = (rv' \<noteq> 0)) ret__int_' (\<lambda>rv rv'. {s. (s \<in> \<lbrace>rv' \<noteq> 0\<rbrace> \<longrightarrow> s \<in> {s. s \<in> UNIV}) \<and> (s \<notin> \<lbrace>rv' \<noteq> 0\<rbrace> \<longrightarrow> s \<in> UNIV)})
 3. \<And>tptr s s'. \<lbrakk>tptr = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; (tcb_at' thread and st_tcb_at' (not runnable') thread and valid_queues' and Invariants_H.valid_queues and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and valid_objs') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>s. \<forall>rv. ksCurThread s = rv \<longrightarrow> st_tcb_at' (\<lambda>st. runnable' st = st_tcb_at' runnable' thread s) thread s \<and> rv = ksCurThread s \<and> ksSchedulerAction s = ksSchedulerAction s \<and> weak_sch_act_wf (ksSchedulerAction s) s) and ?R7 tptr) s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> (\<forall>rva. ksCurThread s = rva \<longrightarrow> st_tcb_at' (\<lambda>st. runnable' st = rv) thread s \<and> rva = ksCurThread s \<and> ksSchedulerAction s = ksSchedulerAction s \<and> weak_sch_act_wf (ksSchedulerAction s) s) \<longrightarrow> s' \<in> {s. \<forall>rva. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rva \<longrightarrow> s \<in> {s'. \<forall>rvb s. (s, s') \<in> rf_sr \<and> st_tcb_at' (\<lambda>st. runnable' st = rv) thread s \<and> rva = ksCurThread s \<and> rvb = ksSchedulerAction s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<longrightarrow> s' \<in> UNIV}}} proof (prove)
goal (2 subgoals):
 1. \<And>tptr. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> guard_is_UNIV (\<lambda>rv rv'. (\<not> fst rv \<and> fst (snd rv) = thread \<and> snd (snd rv) = ResumeCurrentThread) = (rv' \<noteq> 0)) ret__int_' (\<lambda>rv rv'. {s. (s \<in> \<lbrace>rv' \<noteq> 0\<rbrace> \<longrightarrow> s \<in> {s. s \<in> UNIV}) \<and> (s \<notin> \<lbrace>rv' \<noteq> 0\<rbrace> \<longrightarrow> s \<in> UNIV)})
 2. \<And>tptr s s'. \<lbrakk>tptr = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; (tcb_at' thread and st_tcb_at' (not runnable') thread and valid_queues' and Invariants_H.valid_queues and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and valid_objs') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>s. \<forall>rv. ksCurThread s = rv \<longrightarrow> st_tcb_at' (\<lambda>st. runnable' st = st_tcb_at' runnable' thread s) thread s \<and> rv = ksCurThread s \<and> ksSchedulerAction s = ksSchedulerAction s \<and> weak_sch_act_wf (ksSchedulerAction s) s) and (\<lambda>s. ((\<lambda>_. True) and (\<lambda>sa. \<not> fst (st_tcb_at' runnable' thread s, ksCurThread s, ksSchedulerAction s) \<and> fst (snd (st_tcb_at' runnable' thread s, ksCurThread s, ksSchedulerAction s)) = thread \<and> snd (snd (st_tcb_at' runnable' thread s, ksCurThread s, ksSchedulerAction s)) = ResumeCurrentThread \<longrightarrow> (Invariants_H.valid_queues and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and valid_objs') sa) and (\<lambda>sa. \<not> (\<not> fst (st_tcb_at' runnable' thread s, ksCurThread s, ksSchedulerAction s) \<and> fst (snd (st_tcb_at' runnable' thread s, ksCurThread s, ksSchedulerAction s)) = thread \<and> snd (snd (st_tcb_at' runnable' thread s, ksCurThread s, ksSchedulerAction s)) = ResumeCurrentThread) \<longrightarrow> True)) s)) s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> (\<forall>rva. ksCurThread s = rva \<longrightarrow> st_tcb_at' (\<lambda>st. runnable' st = rv) thread s \<and> rva = ksCurThread s \<and> ksSchedulerAction s = ksSchedulerAction s \<and> weak_sch_act_wf (ksSchedulerAction s) s) \<longrightarrow> s' \<in> {s. \<forall>rva. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rva \<longrightarrow> s \<in> {s'. \<forall>rvb s. (s, s') \<in> rf_sr \<and> st_tcb_at' (\<lambda>st. runnable' st = rv) thread s \<and> rva = ksCurThread s \<and> rvb = ksSchedulerAction s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<longrightarrow> s' \<in> UNIV}}} proof (prove)
goal (1 subgoal):
 1. \<And>tptr s s'. \<lbrakk>tptr = tcb_ptr_to_ctcb_ptr thread; (s, s') \<in> rf_sr; (tcb_at' thread and st_tcb_at' (not runnable') thread and valid_queues' and Invariants_H.valid_queues and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and valid_objs') s; s' \<in> UNIV\<rbrakk> \<Longrightarrow> ((\<lambda>s. \<forall>rv. ksCurThread s = rv \<longrightarrow> st_tcb_at' (\<lambda>st. runnable' st = st_tcb_at' runnable' thread s) thread s \<and> rv = ksCurThread s \<and> ksSchedulerAction s = ksSchedulerAction s \<and> weak_sch_act_wf (ksSchedulerAction s) s) and (\<lambda>s. ((\<lambda>_. True) and (\<lambda>sa. \<not> fst (st_tcb_at' runnable' thread s, ksCurThread s, ksSchedulerAction s) \<and> fst (snd (st_tcb_at' runnable' thread s, ksCurThread s, ksSchedulerAction s)) = thread \<and> snd (snd (st_tcb_at' runnable' thread s, ksCurThread s, ksSchedulerAction s)) = ResumeCurrentThread \<longrightarrow> (Invariants_H.valid_queues and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and valid_objs') sa) and (\<lambda>sa. \<not> (\<not> fst (st_tcb_at' runnable' thread s, ksCurThread s, ksSchedulerAction s) \<and> fst (snd (st_tcb_at' runnable' thread s, ksCurThread s, ksSchedulerAction s)) = thread \<and> snd (snd (st_tcb_at' runnable' thread s, ksCurThread s, ksSchedulerAction s)) = ResumeCurrentThread) \<longrightarrow> True)) s)) s \<and> s' \<in> {s'. \<forall>rv s. (s, s') \<in> rf_sr \<and> (\<forall>rva. ksCurThread s = rva \<longrightarrow> st_tcb_at' (\<lambda>st. runnable' st = rv) thread s \<and> rva = ksCurThread s \<and> ksSchedulerAction s = ksSchedulerAction s \<and> weak_sch_act_wf (ksSchedulerAction s) s) \<longrightarrow> s' \<in> {s. \<forall>rva. ksCurThread_' (globals s) = tcb_ptr_to_ctcb_ptr rva \<longrightarrow> s \<in> {s'. \<forall>rvb s. (s, s') \<in> rf_sr \<and> st_tcb_at' (\<lambda>st. runnable' st = rv) thread s \<and> rva = ksCurThread s \<and> rvb = ksSchedulerAction s \<and> weak_sch_act_wf (ksSchedulerAction s) s \<longrightarrow> s' \<in> UNIV}}} proof (prove)
goal:
No subgoals!