theory IpcCancel_C

lemma scheduleTCB_ccorres':
  "ccorres dc xfdc
           (tcb_at' thread and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and valid_queues
                           and valid_objs')
           (UNIV \<inter> {s. tptr_' s = tcb_ptr_to_ctcb_ptr thread})
           []
  (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_') 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> (\<forall>t. ksSchedulerAction s = SwitchToThread t \<longrightarrow> tcb_at' t s)"
                           and P'=UNIV in ccorres_from_vcg) apply (rule allI, rule conseqPre, vcg) apply (clarsimp simp: return_def 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 (subgoal_tac "ksSchedulerAction \<sigma> = ResumeCurrentThread") apply (clarsimp simp: ctcb_relation_def cthread_state_relation_def) apply (case_tac "tcbState ko", simp_all add: "StrictC'_thread_state_defs")[1] apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def
                                  cscheduler_action_relation_def                                  tcb_at_not_NULL
                           split: scheduler_action.split_asm) apply (clarsimp simp: rf_sr_def cstate_relation_def Let_def
                                 cscheduler_action_relation_def) apply wp+ apply (simp add: isRunnable_def isStopped_def) apply wp apply (simp add: guard_is_UNIV_def) apply clarsimp apply (clarsimp simp: st_tcb_at'_def obj_at'_def weak_sch_act_wf_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. ccorres dc xfdc (tcb_at' thread and (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and Invariants_H.valid_queues 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 (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and Invariants_H.valid_queues 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 (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and Invariants_H.valid_queues 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 (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and Invariants_H.valid_queues 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 (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and Invariants_H.valid_queues 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 (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and Invariants_H.valid_queues 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 (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and Invariants_H.valid_queues 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 (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and Invariants_H.valid_queues 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 (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and Invariants_H.valid_queues 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 (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and Invariants_H.valid_queues 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 (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and Invariants_H.valid_queues 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 (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and Invariants_H.valid_queues 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 (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and Invariants_H.valid_queues 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 (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and Invariants_H.valid_queues 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 (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and Invariants_H.valid_queues 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 (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and Invariants_H.valid_queues 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 (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and Invariants_H.valid_queues 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> (\<forall>t. ksSchedulerAction \<sigma> = SwitchToThread t \<longrightarrow> tcb_at' t \<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> (\<forall>t. ksSchedulerAction s = SwitchToThread t \<longrightarrow> tcb_at' t 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 (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and Invariants_H.valid_queues 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> (\<forall>t. ksSchedulerAction s = SwitchToThread t \<longrightarrow> tcb_at' t 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> (\<forall>t. ksSchedulerAction \<sigma> = SwitchToThread t \<longrightarrow> tcb_at' t \<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> (\<forall>t. ksSchedulerAction s = SwitchToThread t \<longrightarrow> tcb_at' t 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 (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and Invariants_H.valid_queues 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> (\<forall>t. ksSchedulerAction s = SwitchToThread t \<longrightarrow> tcb_at' t 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>; \<forall>t. ksSchedulerAction \<sigma> = SwitchToThread t \<longrightarrow> tcb_at' t \<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> (\<forall>t. ksSchedulerAction s = SwitchToThread t \<longrightarrow> tcb_at' t 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 (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and Invariants_H.valid_queues 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> (\<forall>t. ksSchedulerAction s = SwitchToThread t \<longrightarrow> tcb_at' t 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>; \<forall>t. ksSchedulerAction \<sigma> = SwitchToThread t \<longrightarrow> tcb_at' t \<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> (\<forall>t. ksSchedulerAction s = SwitchToThread t \<longrightarrow> tcb_at' t 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 (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and Invariants_H.valid_queues 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> (\<forall>t. ksSchedulerAction s = SwitchToThread t \<longrightarrow> tcb_at' t 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>; \<forall>t. ksSchedulerAction \<sigma> = SwitchToThread t \<longrightarrow> tcb_at' t \<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>; \<forall>t. ksSchedulerAction \<sigma> = SwitchToThread t \<longrightarrow> tcb_at' t \<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> (\<forall>t. ksSchedulerAction s = SwitchToThread t \<longrightarrow> tcb_at' t 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>; \<forall>t. ksSchedulerAction \<sigma> = SwitchToThread t \<longrightarrow> tcb_at' t \<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>; \<forall>t. ksSchedulerAction \<sigma> = SwitchToThread t \<longrightarrow> tcb_at' t \<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> (\<forall>t. ksSchedulerAction s = SwitchToThread t \<longrightarrow> tcb_at' t 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>\<forall>t. ksSchedulerAction \<sigma> = SwitchToThread t \<longrightarrow> tcb_at' t \<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>; \<forall>t. ksSchedulerAction \<sigma> = SwitchToThread t \<longrightarrow> tcb_at' t \<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> (\<forall>t. ksSchedulerAction s = SwitchToThread t \<longrightarrow> tcb_at' t 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> tcb_at' 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'; 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>; \<forall>t. ksSchedulerAction \<sigma> = SwitchToThread t \<longrightarrow> tcb_at' t \<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> (\<forall>t. ksSchedulerAction s = SwitchToThread t \<longrightarrow> tcb_at' t 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 (12 subgoals):
 1. \<And>\<sigma> x ko ko' t. \<lbrakk>\<forall>t. ksSchedulerAction \<sigma> = SwitchToThread t \<longrightarrow> tcb_at' 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'; 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); ksSchedulerAction \<sigma> = ResumeCurrentThread\<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>\<sigma> x ko ko' t. \<lbrakk>\<forall>t. ksSchedulerAction \<sigma> = SwitchToThread t \<longrightarrow> tcb_at' 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'; 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> ksSchedulerAction \<sigma> = ResumeCurrentThread
 3. \<And>runnable \<sigma> x. \<lbrakk>st_tcb_at' (\<lambda>st. runnable' st = runnable) (ksCurThread \<sigma>) \<sigma>; \<forall>t. ksSchedulerAction \<sigma> = SwitchToThread t \<longrightarrow> tcb_at' t \<sigma>; (\<sigma>, x) \<in> rf_sr; thread = ksCurThread \<sigma>\<rbrakk> \<Longrightarrow> ksSchedulerAction_' (globals x) \<noteq> NULL \<longrightarrow> runnable \<or> ksSchedulerAction \<sigma> \<noteq> ResumeCurrentThread
 4. \<And>tptr runnable curThread s. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<lbrace>(=) s\<rbrace> getSchedulerAction \<lbrace>\<lambda>r. (=) s\<rbrace>
 5. \<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> (\<forall>t. ksSchedulerAction s = SwitchToThread t \<longrightarrow> tcb_at' t s)\<rbrace>
 6. \<And>tptr runnable curThread. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> empty_fail getSchedulerAction
 7. \<And>tptr s. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<lbrace>(=) s\<rbrace> isRunnable thread \<lbrace>\<lambda>r. (=) s\<rbrace>
 8. \<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>
 9. \<And>tptr. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> empty_fail (isRunnable thread)
 10. \<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>
A total of 12 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>\<sigma> x ko ko' t. \<lbrakk>(\<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); ksSchedulerAction \<sigma> = ResumeCurrentThread; 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)) = (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>\<sigma> x ko ko' t. \<lbrakk>\<forall>t. ksSchedulerAction \<sigma> = SwitchToThread t \<longrightarrow> tcb_at' 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'; 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> ksSchedulerAction \<sigma> = ResumeCurrentThread
 3. \<And>runnable \<sigma> x. \<lbrakk>st_tcb_at' (\<lambda>st. runnable' st = runnable) (ksCurThread \<sigma>) \<sigma>; \<forall>t. ksSchedulerAction \<sigma> = SwitchToThread t \<longrightarrow> tcb_at' t \<sigma>; (\<sigma>, x) \<in> rf_sr; thread = ksCurThread \<sigma>\<rbrakk> \<Longrightarrow> ksSchedulerAction_' (globals x) \<noteq> NULL \<longrightarrow> runnable \<or> ksSchedulerAction \<sigma> \<noteq> ResumeCurrentThread
 4. \<And>tptr runnable curThread s. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<lbrace>(=) s\<rbrace> getSchedulerAction \<lbrace>\<lambda>r. (=) s\<rbrace>
 5. \<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> (\<forall>t. ksSchedulerAction s = SwitchToThread t \<longrightarrow> tcb_at' t s)\<rbrace>
 6. \<And>tptr runnable curThread. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> empty_fail getSchedulerAction
 7. \<And>tptr s. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> \<lbrace>(=) s\<rbrace> isRunnable thread \<lbrace>\<lambda>r. (=) s\<rbrace>
 8. \<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>
 9. \<And>tptr. tptr = tcb_ptr_to_ctcb_ptr thread \<Longrightarrow> empty_fail (isRunnable thread)
 10. \<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>
A total of 12 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>\<sigma> x ko ko' t. \<lbrakk>\<forall>t. ksSchedulerAction \<sigma> = SwitchToThread t \<longrightarrow> tcb_at' 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'; 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> ksSchedulerAction \<sigma> = ResumeCurrentThread
 2. \<And>runnable \<sigma> x. \<lbrakk>st_tcb_at' (\<lambda>st. runnable' st = runnable) (ksCurThread \<sigma>) \<sigma>; \<forall>t. ksSchedulerAction \<sigma> = SwitchToThread t \<longrightarrow> tcb_at' t \<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> (\<forall>t. ksSchedulerAction s = SwitchToThread t \<longrightarrow> tcb_at' t 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 (10 subgoals):
 1. \<And>runnable \<sigma> x. \<lbrakk>st_tcb_at' (\<lambda>st. runnable' st = runnable) (ksCurThread \<sigma>) \<sigma>; \<forall>t. ksSchedulerAction \<sigma> = SwitchToThread t \<longrightarrow> tcb_at' t \<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>?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> (\<forall>t. ksSchedulerAction s = SwitchToThread t \<longrightarrow> tcb_at' t 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 (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and Invariants_H.valid_queues 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> (\<forall>t. ksSchedulerAction s = SwitchToThread t \<longrightarrow> tcb_at' t 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>?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> (\<forall>t. ksSchedulerAction s = SwitchToThread t \<longrightarrow> tcb_at' t 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>?P167 tptr\<rbrace> isRunnable thread \<lbrace>\<lambda>runnable s. \<forall>rv. ksCurThread s = rv \<longrightarrow> ?P231 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>?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>
 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 (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and Invariants_H.valid_queues 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> (\<forall>t. ksSchedulerAction s = SwitchToThread t \<longrightarrow> tcb_at' t 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>?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 (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and Invariants_H.valid_queues 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> (\<forall>t. ksSchedulerAction s = SwitchToThread t \<longrightarrow> tcb_at' t s)) and ?R167 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> (\<forall>t. ksSchedulerAction s = SwitchToThread t \<longrightarrow> tcb_at' t 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> (\<forall>t. ksSchedulerAction s = SwitchToThread t \<longrightarrow> tcb_at' t s) \<longrightarrow> s' \<in> UNIV}}} proof (prove)
goal (3 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 (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and Invariants_H.valid_queues 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> (\<forall>t. ksSchedulerAction s = SwitchToThread t \<longrightarrow> tcb_at' t s)) and ?R167 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> (\<forall>t. ksSchedulerAction s = SwitchToThread t \<longrightarrow> tcb_at' t 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> (\<forall>t. ksSchedulerAction s = SwitchToThread t \<longrightarrow> tcb_at' t 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 (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and Invariants_H.valid_queues 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> (\<forall>t. ksSchedulerAction s = SwitchToThread t \<longrightarrow> tcb_at' t 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> (\<forall>t. ksSchedulerAction s = SwitchToThread t \<longrightarrow> tcb_at' t 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> (\<forall>t. ksSchedulerAction s = SwitchToThread t \<longrightarrow> tcb_at' t 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 (\<lambda>s. weak_sch_act_wf (ksSchedulerAction s) s) and Invariants_H.valid_queues 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> (\<forall>t. ksSchedulerAction s = SwitchToThread t \<longrightarrow> tcb_at' t 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> (\<forall>t. ksSchedulerAction s = SwitchToThread t \<longrightarrow> tcb_at' t 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> (\<forall>t. ksSchedulerAction s = SwitchToThread t \<longrightarrow> tcb_at' t s) \<longrightarrow> s' \<in> UNIV}}} proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<lbrakk>(s, s') \<in> rf_sr; tcb_at' thread s; weak_sch_act_wf (ksSchedulerAction s) s; Invariants_H.valid_queues s; valid_objs' s\<rbrakk> \<Longrightarrow> st_tcb_at' (\<lambda>st. runnable' st = st_tcb_at' runnable' thread s) thread s \<and> (\<forall>t. ksSchedulerAction s = SwitchToThread t \<longrightarrow> tcb_at' t s) \<and> (\<not> st_tcb_at' runnable' thread s \<and> ksCurThread s = thread \<and> ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> weak_sch_act_wf ResumeCurrentThread s) proof (prove)
goal:
No subgoals!