theory Orphanage

lemma schedule_no_orphans[wp]:
  notes ssa_wp[wp del]
  shows
  "\<lbrace> \<lambda>s. no_orphans s \<and> invs' s \<rbrace>
   schedule
   \<lbrace> \<lambda>rv s. no_orphans s \<rbrace>" proof - have do_switch_to:
    "\<And>candidate.
     \<lbrace>\<lambda>s. no_orphans s \<and> ksSchedulerAction s = SwitchToThread candidate
          \<and> st_tcb_at' runnable' candidate s
          \<and> (st_tcb_at' runnable' (ksCurThread s) s
             \<longrightarrow> (\<exists>d p. ksCurThread s \<in> set (ksReadyQueues s (d, p)))) \<rbrace>
      do ThreadDecls_H.switchToThread candidate;
         setSchedulerAction ResumeCurrentThread
      od
    \<lbrace>\<lambda>rv. no_orphans\<rbrace>" apply (wpsimp wp: scheduleChooseNewThread_no_orphans ssa_no_orphans
                      hoare_vcg_all_lift ThreadDecls_H_switchToThread_no_orphans)+ apply (rule_tac Q="\<lambda>_ s. (t = candidate \<longrightarrow> ksCurThread s = candidate) \<and>
                               (t \<noteq> candidate \<longrightarrow> sch_act_not t s)"
              in hoare_post_imp) apply (wpsimp wp: stt_nosch hoare_weak_lift_imp)+ apply (fastforce dest!: in_all_active_tcb_ptrsD simp: all_queued_tcb_ptrs_def comp_def) done have abort_switch_to_enq:
    "\<And>candidate.
     \<lbrace>\<lambda>s. no_orphans s \<and> invs' s \<and> valid_queues' s
          \<and> ksSchedulerAction s = SwitchToThread candidate
          \<and> (st_tcb_at' runnable' (ksCurThread s) s
               \<longrightarrow> (\<exists>d p. ksCurThread s \<in> set (ksReadyQueues s (d, p)))) \<rbrace>
       do tcbSchedEnqueue candidate;
          setSchedulerAction ChooseNewThread;
          scheduleChooseNewThread
       od
     \<lbrace>\<lambda>rv. no_orphans\<rbrace>" apply (rule hoare_pre) apply (wp scheduleChooseNewThread_no_orphans ssa_no_orphans setSchedulerAction_direct) apply (wpsimp wp: hoare_vcg_imp_lift' hoare_vcg_ex_lift
                    simp: is_active_tcb_ptr_runnable' all_queued_tcb_ptrs_def
             | rule hoare_lift_Pf2[where f=ksCurThread, OF setSchedulerAction_ksQ])+ apply (wp tcbSchedEnqueue_in_ksQ' tcbSchedEnqueue_no_orphans hoare_vcg_all_lift hoare_vcg_imp_lift' hoare_vcg_disj_lift) apply (wp hoare_lift_Pf2[where f=ksCurThread, OF tcbSchedEnqueue_pred_tcb_at']
                hoare_lift_Pf2[where f=ksCurThread, OF tcbSchedEnqueue_in_ksQ_already_queued]
                tcbSchedEnqueue_no_orphans
             | strengthen not_pred_tcb_at'_strengthen
             | wp (once) hoare_vcg_imp_lift')+ apply (clarsimp) apply (frule invs_sch_act_wf', clarsimp simp: pred_tcb_at') apply (simp add: st_tcb_at_neg' tcb_at_invs') done have abort_switch_to_app:
    "\<And>candidate.
     \<lbrace>\<lambda>s. no_orphans s \<and> invs' s \<and> valid_queues' s
          \<and> ksSchedulerAction s = SwitchToThread candidate
          \<and> (st_tcb_at' runnable' (ksCurThread s) s
             \<longrightarrow> (\<exists>d p. ksCurThread s \<in> set (ksReadyQueues s (d, p))) ) \<rbrace>
       do tcbSchedAppend candidate;
          setSchedulerAction ChooseNewThread;
          scheduleChooseNewThread
       od
     \<lbrace>\<lambda>rv. no_orphans\<rbrace>" apply (rule hoare_pre) apply (wp scheduleChooseNewThread_no_orphans ssa_no_orphans setSchedulerAction_direct) apply (wpsimp wp: hoare_vcg_imp_lift' hoare_vcg_ex_lift
                    simp: is_active_tcb_ptr_runnable' all_queued_tcb_ptrs_def
             | rule hoare_lift_Pf2[where f=ksCurThread, OF setSchedulerAction_ksQ])+ apply (wp tcbSchedAppend_in_ksQ'' tcbSchedAppend_no_orphans hoare_vcg_all_lift hoare_vcg_imp_lift' hoare_vcg_disj_lift) apply (wp hoare_lift_Pf2[where f=ksCurThread, OF tcbSchedAppend_pred_tcb_at']
                hoare_lift_Pf2[where f=ksCurThread, OF tcbSchedAppend_in_ksQ_already_queued]
                tcbSchedAppend_no_orphans
             | strengthen not_pred_tcb_at'_strengthen
             | wp (once) hoare_vcg_imp_lift')+ apply (clarsimp) apply (frule invs_sch_act_wf', clarsimp simp: pred_tcb_at') apply (simp add: st_tcb_at_neg' tcb_at_invs') done show ?thesis unfolding schedule_def supply if_weak_cong[cong] apply (wp, wpc)
       \<comment> \<open>action = ResumeCurrentThread\<close> apply (wp)[1]
     \<comment> \<open>action = ChooseNewThread\<close> apply (clarsimp simp: when_def scheduleChooseNewThread_def) apply (wp ssa_no_orphans hoare_vcg_all_lift) apply (wp hoare_disjI1 chooseThread_nosch) apply (wp nextDomain_invs_no_cicd' hoare_vcg_imp_lift
                   hoare_lift_Pf2 [OF ksQ_all_queued_tcb_ptrs_lift
                                      [OF nextDomain_ksQ]
                                      nextDomain_ct']
                   hoare_lift_Pf2 [OF st_tcb_at'_is_active_tcb_ptr_lift
                                    [OF nextDomain_st_tcb_at']
                                    nextDomain_ct']
                   hoare_vcg_all_lift getDomainTime_wp)[2] apply ((wp tcbSchedEnqueue_no_orphans tcbSchedEnqueue_in_ksQ'
                  hoare_drop_imp
             | clarsimp simp: all_queued_tcb_ptrs_def
             | strengthen all_invs_but_ct_idle_or_in_cur_domain'_strg
             | wps tcbSchedEnqueue_ct')+)[1] apply ((wp tcbSchedEnqueue_no_orphans tcbSchedEnqueue_in_ksQ'
                  hoare_drop_imp
             | clarsimp simp: all_queued_tcb_ptrs_def
             | strengthen all_invs_but_ct_idle_or_in_cur_domain'_strg
             | wps tcbSchedEnqueue_ct')+)[1] apply wp[1]
    \<comment> \<open>action = SwitchToThread candidate\<close> apply (clarsimp) apply (rename_tac candidate) apply (wpsimp wp: do_switch_to abort_switch_to_enq abort_switch_to_app) 
          (* isHighestPrio *)
           apply (wp hoare_drop_imps) apply (wp add: tcbSchedEnqueue_no_orphans)+ apply (clarsimp simp: conj_comms cong: conj_cong imp_cong split del: if_split) apply (wp hoare_lift_Pf2[where f=ksCurThread, OF tcbSchedEnqueue_pred_tcb_at']
              hoare_lift_Pf2[where f=ksCurThread, OF tcbSchedEnqueue_in_ksQ']
              hoare_vcg_imp_lift'
           | strengthen not_pred_tcb_at'_strengthen)+ apply (clarsimp simp: comp_def) apply (frule invs_queues) apply (clarsimp simp: invs_valid_queues' tcb_at_invs' st_tcb_at_neg' is_active_tcb_ptr_runnable') apply (fastforce simp: all_invs_but_ct_idle_or_in_cur_domain'_strg invs_switchToThread_runnable') done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. no_orphans s \<and> invs' s\<rbrace> ThreadDecls_H.schedule \<lbrace>\<lambda>rv. no_orphans\<rbrace> proof (state)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. no_orphans s \<and> invs' s\<rbrace> ThreadDecls_H.schedule \<lbrace>\<lambda>rv. no_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>candidate. \<lbrace>\<lambda>s. no_orphans s \<and> ksSchedulerAction s = SwitchToThread candidate \<and> st_tcb_at' runnable' candidate s \<and> (st_tcb_at' runnable' (ksCurThread s) s \<longrightarrow> (\<exists>d p. ksCurThread s \<in> set (ksReadyQueues s (d, p))))\<rbrace> do global.switchToThread candidate;
setSchedulerAction ResumeCurrentThread
od \<lbrace>\<lambda>rv. no_orphans\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>candidate t. \<lbrace>?P7 candidate t\<rbrace> global.switchToThread candidate \<lbrace>\<lambda>rv s. ksSchedulerAction s = SwitchToThread t \<longrightarrow> t \<in> all_queued_tcb_ptrs s \<or> ksCurThread s = t\<rbrace>
 2. \<And>candidate s. no_orphans s \<and> ksSchedulerAction s = SwitchToThread candidate \<and> st_tcb_at' runnable' candidate s \<and> (st_tcb_at' runnable' (ksCurThread s) s \<longrightarrow> (\<exists>d p. ksCurThread s \<in> set (ksReadyQueues s (d, p)))) \<Longrightarrow> (no_orphans s \<and> st_tcb_at' runnable' candidate s \<and> (ksCurThread s \<in> all_active_tcb_ptrs s \<longrightarrow> ksCurThread s \<in> all_queued_tcb_ptrs s)) \<and> (\<forall>x. ?P7 candidate x s) proof (prove)
goal (3 subgoals):
 1. \<And>candidate t rv s. (t = candidate \<longrightarrow> ksCurThread s = candidate) \<and> (t \<noteq> candidate \<longrightarrow> sch_act_not t s) \<Longrightarrow> ksSchedulerAction s = SwitchToThread t \<longrightarrow> t \<in> all_queued_tcb_ptrs s \<or> ksCurThread s = t
 2. \<And>candidate t. \<lbrace>?P7 candidate t\<rbrace> global.switchToThread candidate \<lbrace>\<lambda>_ s. (t = candidate \<longrightarrow> ksCurThread s = candidate) \<and> (t \<noteq> candidate \<longrightarrow> sch_act_not t s)\<rbrace>
 3. \<And>candidate s. no_orphans s \<and> ksSchedulerAction s = SwitchToThread candidate \<and> st_tcb_at' runnable' candidate s \<and> (st_tcb_at' runnable' (ksCurThread s) s \<longrightarrow> (\<exists>d p. ksCurThread s \<in> set (ksReadyQueues s (d, p)))) \<Longrightarrow> (no_orphans s \<and> st_tcb_at' runnable' candidate s \<and> (ksCurThread s \<in> all_active_tcb_ptrs s \<longrightarrow> ksCurThread s \<in> all_queued_tcb_ptrs s)) \<and> (\<forall>x. ?P7 candidate x s) proof (prove)
goal (1 subgoal):
 1. \<And>candidate s. \<lbrakk>no_orphans s; ksSchedulerAction s = SwitchToThread candidate; st_tcb_at' runnable' candidate s; st_tcb_at' runnable' (ksCurThread s) s \<longrightarrow> (\<exists>d p. ksCurThread s \<in> set (ksReadyQueues s (d, p))); ksCurThread s \<in> all_active_tcb_ptrs s\<rbrakk> \<Longrightarrow> ksCurThread s \<in> all_queued_tcb_ptrs s proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrace>\<lambda>s. no_orphans s \<and> ksSchedulerAction s = SwitchToThread ?candidate \<and> st_tcb_at' runnable' ?candidate s \<and> (st_tcb_at' runnable' (ksCurThread s) s \<longrightarrow> (\<exists>d p. ksCurThread s \<in> set (ksReadyQueues s (d, p))))\<rbrace> do global.switchToThread ?candidate;
setSchedulerAction ResumeCurrentThread
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>

goal (1 subgoal):
 1. \<lbrace>\<lambda>s. no_orphans s \<and> invs' s\<rbrace> ThreadDecls_H.schedule \<lbrace>\<lambda>rv. no_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>candidate. \<lbrace>\<lambda>s. no_orphans s \<and> invs' s \<and> valid_queues' s \<and> ksSchedulerAction s = SwitchToThread candidate \<and> (st_tcb_at' runnable' (ksCurThread s) s \<longrightarrow> (\<exists>d p. ksCurThread s \<in> set (ksReadyQueues s (d, p))))\<rbrace> do tcbSchedEnqueue candidate;
setSchedulerAction ChooseNewThread;
scheduleChooseNewThread
od \<lbrace>\<lambda>rv. no_orphans\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>candidate. \<lbrace>?Q candidate\<rbrace> do tcbSchedEnqueue candidate;
setSchedulerAction ChooseNewThread;
scheduleChooseNewThread
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>
 2. \<And>candidate s. no_orphans s \<and> invs' s \<and> valid_queues' s \<and> ksSchedulerAction s = SwitchToThread candidate \<and> (st_tcb_at' runnable' (ksCurThread s) s \<longrightarrow> (\<exists>d p. ksCurThread s \<in> set (ksReadyQueues s (d, p)))) \<Longrightarrow> ?Q candidate s proof (prove)
goal (3 subgoals):
 1. \<And>candidate x. \<lbrace>?P'14 candidate x\<rbrace> setSchedulerAction ChooseNewThread \<lbrace>\<lambda>rv s. st_tcb_at' runnable' (ksCurThread s) s \<longrightarrow> (\<exists>d p. ksCurThread s \<in> set (ksReadyQueues s (d, p)))\<rbrace>
 2. \<And>candidate. \<lbrace>?Q candidate\<rbrace> tcbSchedEnqueue candidate \<lbrace>\<lambda>x s. (invs' and sch_act_wf ChooseNewThread and (\<lambda>s. ChooseNewThread = ResumeCurrentThread \<longrightarrow> obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s) and (\<lambda>s. ChooseNewThread = ResumeCurrentThread \<longrightarrow> ksCurThread s = ksIdleThread s \<or> tcb_in_cur_domain' (ksCurThread s) s)) s \<and> (no_orphans s \<and> (\<forall>t. sch_act_not t s \<or> t \<in> all_queued_tcb_ptrs s \<or> ksCurThread s = t)) \<and> True \<and> ?P'14 candidate x s\<rbrace>
 3. \<And>candidate s. no_orphans s \<and> invs' s \<and> valid_queues' s \<and> ksSchedulerAction s = SwitchToThread candidate \<and> (st_tcb_at' runnable' (ksCurThread s) s \<longrightarrow> (\<exists>d p. ksCurThread s \<in> set (ksReadyQueues s (d, p)))) \<Longrightarrow> ?Q candidate s proof (prove)
goal (2 subgoals):
 1. \<And>candidate. \<lbrace>?P'45 candidate\<rbrace> tcbSchedEnqueue candidate \<lbrace>\<lambda>rv s. (\<forall>t. ksSchedulerAction s = SwitchToThread t \<longrightarrow> (\<exists>a b. t \<in> set (ksReadyQueues s (a, b))) \<or> ksCurThread s = t) \<and> (st_tcb_at' runnable' (ksCurThread s) s \<longrightarrow> (\<exists>x xa. ksCurThread s \<in> set (ksReadyQueues s (x, xa))))\<rbrace>
 2. \<And>candidate s. no_orphans s \<and> invs' s \<and> valid_queues' s \<and> ksSchedulerAction s = SwitchToThread candidate \<and> (st_tcb_at' runnable' (ksCurThread s) s \<longrightarrow> (\<exists>d p. ksCurThread s \<in> set (ksReadyQueues s (d, p)))) \<Longrightarrow> (invs' and st_tcb_at' runnable' candidate and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> candidate)) s \<and> no_orphans s \<and> ?P'45 candidate s proof (prove)
goal (3 subgoals):
 1. \<And>candidate. \<lbrace>?P'56 candidate\<rbrace> tcbSchedEnqueue candidate \<lbrace>\<lambda>rv s. \<not> st_tcb_at' runnable' (ksCurThread s) s\<rbrace>
 2. \<And>candidate. \<lbrace>?Q'56 candidate\<rbrace> tcbSchedEnqueue candidate \<lbrace>\<lambda>rv s. \<exists>x xa. ksCurThread s \<in> set (ksReadyQueues s (x, xa))\<rbrace>
 3. \<And>candidate s. no_orphans s \<and> invs' s \<and> valid_queues' s \<and> ksSchedulerAction s = SwitchToThread candidate \<and> (st_tcb_at' runnable' (ksCurThread s) s \<longrightarrow> (\<exists>d p. ksCurThread s \<in> set (ksReadyQueues s (d, p)))) \<Longrightarrow> (invs' and st_tcb_at' runnable' candidate and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> candidate)) s \<and> no_orphans s \<and> (\<forall>x. \<not> sch_act_not x s \<longrightarrow> (valid_queues' and tcb_at' x and K (x = candidate)) s \<or> ksCurThread s = x) \<and> (\<not> ?P'56 candidate s \<longrightarrow> ?Q'56 candidate s) proof (prove)
goal (1 subgoal):
 1. \<And>candidate s. no_orphans s \<and> invs' s \<and> valid_queues' s \<and> ksSchedulerAction s = SwitchToThread candidate \<and> (st_tcb_at' runnable' (ksCurThread s) s \<longrightarrow> (\<exists>d p. ksCurThread s \<in> set (ksReadyQueues s (d, p)))) \<Longrightarrow> (invs' and st_tcb_at' runnable' candidate and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> candidate)) s \<and> no_orphans s \<and> (\<forall>x. \<not> sch_act_not x s \<longrightarrow> (valid_queues' and tcb_at' x and K (x = candidate)) s \<or> ksCurThread s = x) \<and> (\<not> st_tcb_at' (Not \<circ> runnable') (ksCurThread s) s \<longrightarrow> valid_queues' s \<and> tcb_at' candidate s \<and> (\<exists>domain priority. ksCurThread s \<in> set (ksReadyQueues s (domain, priority)))) proof (prove)
goal (1 subgoal):
 1. \<And>candidate s. \<lbrakk>no_orphans s; invs' s; valid_queues' s; ksSchedulerAction s = SwitchToThread candidate; st_tcb_at' runnable' (ksCurThread s) s \<longrightarrow> (\<exists>d p. ksCurThread s \<in> set (ksReadyQueues s (d, p)))\<rbrakk> \<Longrightarrow> st_tcb_at' runnable' candidate s \<and> (tcb_at' candidate s \<or> ksCurThread s = candidate) \<and> (\<not> st_tcb_at' (\<lambda>a. \<not> runnable' a) (ksCurThread s) s \<longrightarrow> tcb_at' candidate s \<and> (\<exists>domain priority. ksCurThread s \<in> set (ksReadyQueues s (domain, priority)))) proof (prove)
goal (1 subgoal):
 1. \<And>candidate s. \<lbrakk>no_orphans s; invs' s; valid_queues' s; ksSchedulerAction s = SwitchToThread candidate; st_tcb_at' runnable' candidate s; tcb_in_cur_domain' candidate s; \<not> st_tcb_at' (\<lambda>a. \<not> runnable' a) (ksCurThread s) s; \<not> st_tcb_at' runnable' (ksCurThread s) s\<rbrakk> \<Longrightarrow> \<exists>domain priority. ksCurThread s \<in> set (ksReadyQueues s (domain, priority)) proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrace>\<lambda>s. no_orphans s \<and> invs' s \<and> valid_queues' s \<and> ksSchedulerAction s = SwitchToThread ?candidate \<and> (st_tcb_at' runnable' (ksCurThread s) s \<longrightarrow> (\<exists>d p. ksCurThread s \<in> set (ksReadyQueues s (d, p))))\<rbrace> do tcbSchedEnqueue ?candidate;
setSchedulerAction ChooseNewThread;
scheduleChooseNewThread
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>

goal (1 subgoal):
 1. \<lbrace>\<lambda>s. no_orphans s \<and> invs' s\<rbrace> ThreadDecls_H.schedule \<lbrace>\<lambda>rv. no_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>candidate. \<lbrace>\<lambda>s. no_orphans s \<and> invs' s \<and> valid_queues' s \<and> ksSchedulerAction s = SwitchToThread candidate \<and> (st_tcb_at' runnable' (ksCurThread s) s \<longrightarrow> (\<exists>d p. ksCurThread s \<in> set (ksReadyQueues s (d, p))))\<rbrace> do tcbSchedAppend candidate;
setSchedulerAction ChooseNewThread;
scheduleChooseNewThread
od \<lbrace>\<lambda>rv. no_orphans\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>candidate. \<lbrace>?Q candidate\<rbrace> do tcbSchedAppend candidate;
setSchedulerAction ChooseNewThread;
scheduleChooseNewThread
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>
 2. \<And>candidate s. no_orphans s \<and> invs' s \<and> valid_queues' s \<and> ksSchedulerAction s = SwitchToThread candidate \<and> (st_tcb_at' runnable' (ksCurThread s) s \<longrightarrow> (\<exists>d p. ksCurThread s \<in> set (ksReadyQueues s (d, p)))) \<Longrightarrow> ?Q candidate s proof (prove)
goal (3 subgoals):
 1. \<And>candidate x. \<lbrace>?P'14 candidate x\<rbrace> setSchedulerAction ChooseNewThread \<lbrace>\<lambda>rv s. st_tcb_at' runnable' (ksCurThread s) s \<longrightarrow> (\<exists>d p. ksCurThread s \<in> set (ksReadyQueues s (d, p)))\<rbrace>
 2. \<And>candidate. \<lbrace>?Q candidate\<rbrace> tcbSchedAppend candidate \<lbrace>\<lambda>x s. (invs' and sch_act_wf ChooseNewThread and (\<lambda>s. ChooseNewThread = ResumeCurrentThread \<longrightarrow> obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s) and (\<lambda>s. ChooseNewThread = ResumeCurrentThread \<longrightarrow> ksCurThread s = ksIdleThread s \<or> tcb_in_cur_domain' (ksCurThread s) s)) s \<and> (no_orphans s \<and> (\<forall>t. sch_act_not t s \<or> t \<in> all_queued_tcb_ptrs s \<or> ksCurThread s = t)) \<and> True \<and> ?P'14 candidate x s\<rbrace>
 3. \<And>candidate s. no_orphans s \<and> invs' s \<and> valid_queues' s \<and> ksSchedulerAction s = SwitchToThread candidate \<and> (st_tcb_at' runnable' (ksCurThread s) s \<longrightarrow> (\<exists>d p. ksCurThread s \<in> set (ksReadyQueues s (d, p)))) \<Longrightarrow> ?Q candidate s proof (prove)
goal (2 subgoals):
 1. \<And>candidate. \<lbrace>?P'45 candidate\<rbrace> tcbSchedAppend candidate \<lbrace>\<lambda>rv s. (\<forall>t. ksSchedulerAction s = SwitchToThread t \<longrightarrow> (\<exists>a b. t \<in> set (ksReadyQueues s (a, b))) \<or> ksCurThread s = t) \<and> (st_tcb_at' runnable' (ksCurThread s) s \<longrightarrow> (\<exists>x xa. ksCurThread s \<in> set (ksReadyQueues s (x, xa))))\<rbrace>
 2. \<And>candidate s. no_orphans s \<and> invs' s \<and> valid_queues' s \<and> ksSchedulerAction s = SwitchToThread candidate \<and> (st_tcb_at' runnable' (ksCurThread s) s \<longrightarrow> (\<exists>d p. ksCurThread s \<in> set (ksReadyQueues s (d, p)))) \<Longrightarrow> (invs' and st_tcb_at' runnable' candidate and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> candidate)) s \<and> no_orphans s \<and> ?P'45 candidate s proof (prove)
goal (3 subgoals):
 1. \<And>candidate. \<lbrace>?P'56 candidate\<rbrace> tcbSchedAppend candidate \<lbrace>\<lambda>rv s. \<not> st_tcb_at' runnable' (ksCurThread s) s\<rbrace>
 2. \<And>candidate. \<lbrace>?Q'56 candidate\<rbrace> tcbSchedAppend candidate \<lbrace>\<lambda>rv s. \<exists>x xa. ksCurThread s \<in> set (ksReadyQueues s (x, xa))\<rbrace>
 3. \<And>candidate s. no_orphans s \<and> invs' s \<and> valid_queues' s \<and> ksSchedulerAction s = SwitchToThread candidate \<and> (st_tcb_at' runnable' (ksCurThread s) s \<longrightarrow> (\<exists>d p. ksCurThread s \<in> set (ksReadyQueues s (d, p)))) \<Longrightarrow> (invs' and st_tcb_at' runnable' candidate and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> candidate)) s \<and> no_orphans s \<and> (\<forall>x. \<not> sch_act_not x s \<longrightarrow> valid_queues' s \<and> tcb_at' candidate s \<and> (x \<noteq> candidate \<longrightarrow> (\<exists>domain priority. x \<in> set (ksReadyQueues s (domain, priority)))) \<or> ksCurThread s = x) \<and> (\<not> ?P'56 candidate s \<longrightarrow> ?Q'56 candidate s) proof (prove)
goal (1 subgoal):
 1. \<And>candidate s. no_orphans s \<and> invs' s \<and> valid_queues' s \<and> ksSchedulerAction s = SwitchToThread candidate \<and> (st_tcb_at' runnable' (ksCurThread s) s \<longrightarrow> (\<exists>d p. ksCurThread s \<in> set (ksReadyQueues s (d, p)))) \<Longrightarrow> (invs' and st_tcb_at' runnable' candidate and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> candidate)) s \<and> no_orphans s \<and> (\<forall>x. \<not> sch_act_not x s \<longrightarrow> valid_queues' s \<and> tcb_at' candidate s \<and> (x \<noteq> candidate \<longrightarrow> (\<exists>domain priority. x \<in> set (ksReadyQueues s (domain, priority)))) \<or> ksCurThread s = x) \<and> (\<not> st_tcb_at' (Not \<circ> runnable') (ksCurThread s) s \<longrightarrow> valid_queues' s \<and> tcb_at' candidate s \<and> (\<exists>domain priority. ksCurThread s \<in> set (ksReadyQueues s (domain, priority)))) proof (prove)
goal (1 subgoal):
 1. \<And>candidate s. \<lbrakk>no_orphans s; invs' s; valid_queues' s; ksSchedulerAction s = SwitchToThread candidate; st_tcb_at' runnable' (ksCurThread s) s \<longrightarrow> (\<exists>d p. ksCurThread s \<in> set (ksReadyQueues s (d, p)))\<rbrakk> \<Longrightarrow> st_tcb_at' runnable' candidate s \<and> (tcb_at' candidate s \<or> ksCurThread s = candidate) \<and> (\<not> st_tcb_at' (\<lambda>a. \<not> runnable' a) (ksCurThread s) s \<longrightarrow> tcb_at' candidate s \<and> (\<exists>domain priority. ksCurThread s \<in> set (ksReadyQueues s (domain, priority)))) proof (prove)
goal (1 subgoal):
 1. \<And>candidate s. \<lbrakk>no_orphans s; invs' s; valid_queues' s; ksSchedulerAction s = SwitchToThread candidate; st_tcb_at' runnable' candidate s; tcb_in_cur_domain' candidate s; \<not> st_tcb_at' (\<lambda>a. \<not> runnable' a) (ksCurThread s) s; \<not> st_tcb_at' runnable' (ksCurThread s) s\<rbrakk> \<Longrightarrow> \<exists>domain priority. ksCurThread s \<in> set (ksReadyQueues s (domain, priority)) proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrace>\<lambda>s. no_orphans s \<and> invs' s \<and> valid_queues' s \<and> ksSchedulerAction s = SwitchToThread ?candidate \<and> (st_tcb_at' runnable' (ksCurThread s) s \<longrightarrow> (\<exists>d p. ksCurThread s \<in> set (ksReadyQueues s (d, p))))\<rbrace> do tcbSchedAppend ?candidate;
setSchedulerAction ChooseNewThread;
scheduleChooseNewThread
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>

goal (1 subgoal):
 1. \<lbrace>\<lambda>s. no_orphans s \<and> invs' s\<rbrace> ThreadDecls_H.schedule \<lbrace>\<lambda>rv. no_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. no_orphans s \<and> invs' s\<rbrace> ThreadDecls_H.schedule \<lbrace>\<lambda>rv. no_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. no_orphans s \<and> invs' s\<rbrace> do curThread <- getCurThread;
action <- getSchedulerAction;
case action of ResumeCurrentThread \<Rightarrow> return () | ChooseNewThread \<Rightarrow> do curRunnable <- isRunnable curThread;
when curRunnable $ tcbSchedEnqueue curThread;
scheduleChooseNewThread
od | SwitchToThread candidate \<Rightarrow> do wasRunnable <- isRunnable curThread;
when wasRunnable (tcbSchedEnqueue curThread);
idleThread <- getIdleThread;
targetPrio <- threadGet tcbPriority candidate;
curPrio <- threadGet tcbPriority curThread;
fastfail <- scheduleSwitchThreadFastfail curThread idleThread curPrio targetPrio;
curDom <- curDomain;
highest <- isHighestPrio curDom targetPrio;
if fastfail \<and> \<not> highest then do tcbSchedEnqueue candidate;
setSchedulerAction ChooseNewThread;
scheduleChooseNewThread
od else if wasRunnable \<and> curPrio = targetPrio then do tcbSchedAppend candidate;
setSchedulerAction ChooseNewThread;
scheduleChooseNewThread
od else do global.switchToThread candidate;
setSchedulerAction ResumeCurrentThread
od
od
od \<lbrace>\<lambda>rv. no_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. no_orphans s \<and> invs' s\<rbrace> do curThread <- getCurThread;
action <- getSchedulerAction;
case action of ResumeCurrentThread \<Rightarrow> return () | ChooseNewThread \<Rightarrow> do curRunnable <- isRunnable curThread;
when curRunnable $ tcbSchedEnqueue curThread;
scheduleChooseNewThread
od | SwitchToThread candidate \<Rightarrow> do wasRunnable <- isRunnable curThread;
when wasRunnable (tcbSchedEnqueue curThread);
idleThread <- getIdleThread;
targetPrio <- threadGet tcbPriority candidate;
curPrio <- threadGet tcbPriority curThread;
fastfail <- scheduleSwitchThreadFastfail curThread idleThread curPrio targetPrio;
curDom <- curDomain;
highest <- isHighestPrio curDom targetPrio;
if fastfail \<and> \<not> highest then do tcbSchedEnqueue candidate;
setSchedulerAction ChooseNewThread;
scheduleChooseNewThread
od else if wasRunnable \<and> curPrio = targetPrio then do tcbSchedAppend candidate;
setSchedulerAction ChooseNewThread;
scheduleChooseNewThread
od else do global.switchToThread candidate;
setSchedulerAction ResumeCurrentThread
od
od
od \<lbrace>\<lambda>rv. no_orphans\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>curThread action. action = ResumeCurrentThread \<Longrightarrow> \<lbrace>?R13 curThread action\<rbrace> return () \<lbrace>\<lambda>rv. no_orphans\<rbrace>
 2. \<And>curThread action. action = ChooseNewThread \<Longrightarrow> \<lbrace>?R14 curThread action\<rbrace> do curRunnable <- isRunnable curThread;
when curRunnable $ tcbSchedEnqueue curThread;
scheduleChooseNewThread
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>
 3. \<And>curThread action x3. action = SwitchToThread x3 \<Longrightarrow> \<lbrace>?R15 curThread action x3\<rbrace> do wasRunnable <- isRunnable curThread;
when wasRunnable (tcbSchedEnqueue curThread);
idleThread <- getIdleThread;
targetPrio <- threadGet tcbPriority x3;
curPrio <- threadGet tcbPriority curThread;
fastfail <- scheduleSwitchThreadFastfail curThread idleThread curPrio targetPrio;
curDom <- curDomain;
highest <- isHighestPrio curDom targetPrio;
if fastfail \<and> \<not> highest then do tcbSchedEnqueue x3;
setSchedulerAction ChooseNewThread;
scheduleChooseNewThread
od else if wasRunnable \<and> curPrio = targetPrio then do tcbSchedAppend x3;
setSchedulerAction ChooseNewThread;
scheduleChooseNewThread
od else do global.switchToThread x3;
setSchedulerAction ResumeCurrentThread
od
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>
 4. \<And>curThread. \<lbrace>?B1 curThread\<rbrace> getSchedulerAction \<lbrace>\<lambda>action s. (action = ResumeCurrentThread \<longrightarrow> ?R13 curThread action s) \<and> (action = ChooseNewThread \<longrightarrow> ?R14 curThread action s) \<and> (\<forall>x. action = SwitchToThread x \<longrightarrow> ?R15 curThread action x s)\<rbrace>
 5. \<lbrace>?Q\<rbrace> getCurThread \<lbrace>?B1\<rbrace>
 6. \<And>s. no_orphans s \<and> invs' s \<Longrightarrow> ?Q s proof (prove)
goal (5 subgoals):
 1. \<And>curThread action. action = ChooseNewThread \<Longrightarrow> \<lbrace>?R14 curThread action\<rbrace> do curRunnable <- isRunnable curThread;
when curRunnable $ tcbSchedEnqueue curThread;
scheduleChooseNewThread
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>
 2. \<And>curThread action x3. action = SwitchToThread x3 \<Longrightarrow> \<lbrace>?R15 curThread action x3\<rbrace> do wasRunnable <- isRunnable curThread;
when wasRunnable (tcbSchedEnqueue curThread);
idleThread <- getIdleThread;
targetPrio <- threadGet tcbPriority x3;
curPrio <- threadGet tcbPriority curThread;
fastfail <- scheduleSwitchThreadFastfail curThread idleThread curPrio targetPrio;
curDom <- curDomain;
highest <- isHighestPrio curDom targetPrio;
if fastfail \<and> \<not> highest then do tcbSchedEnqueue x3;
setSchedulerAction ChooseNewThread;
scheduleChooseNewThread
od else if wasRunnable \<and> curPrio = targetPrio then do tcbSchedAppend x3;
setSchedulerAction ChooseNewThread;
scheduleChooseNewThread
od else do global.switchToThread x3;
setSchedulerAction ResumeCurrentThread
od
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>
 3. \<And>curThread. \<lbrace>?B1 curThread\<rbrace> getSchedulerAction \<lbrace>\<lambda>action s. (action = ResumeCurrentThread \<longrightarrow> no_orphans s) \<and> (action = ChooseNewThread \<longrightarrow> ?R14 curThread action s) \<and> (\<forall>x. action = SwitchToThread x \<longrightarrow> ?R15 curThread action x s)\<rbrace>
 4. \<lbrace>?Q\<rbrace> getCurThread \<lbrace>?B1\<rbrace>
 5. \<And>s. no_orphans s \<and> invs' s \<Longrightarrow> ?Q s proof (prove)
goal (5 subgoals):
 1. \<And>curThread. \<lbrace>?R14 curThread ChooseNewThread\<rbrace> do curRunnable <- isRunnable curThread;
y <- if curRunnable then tcbSchedEnqueue curThread else return ();
domainTime <- getDomainTime;
y <- if domainTime = 0 then nextDomain else return ();
y <- chooseThread;
setSchedulerAction ResumeCurrentThread
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>
 2. \<And>curThread action x3. action = SwitchToThread x3 \<Longrightarrow> \<lbrace>?R15 curThread action x3\<rbrace> do wasRunnable <- isRunnable curThread;
when wasRunnable (tcbSchedEnqueue curThread);
idleThread <- getIdleThread;
targetPrio <- threadGet tcbPriority x3;
curPrio <- threadGet tcbPriority curThread;
fastfail <- scheduleSwitchThreadFastfail curThread idleThread curPrio targetPrio;
curDom <- curDomain;
highest <- isHighestPrio curDom targetPrio;
if fastfail \<and> \<not> highest then do tcbSchedEnqueue x3;
setSchedulerAction ChooseNewThread;
scheduleChooseNewThread
od else if wasRunnable \<and> curPrio = targetPrio then do tcbSchedAppend x3;
setSchedulerAction ChooseNewThread;
scheduleChooseNewThread
od else do global.switchToThread x3;
setSchedulerAction ResumeCurrentThread
od
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>
 3. \<And>curThread. \<lbrace>?B1 curThread\<rbrace> getSchedulerAction \<lbrace>\<lambda>action s. (action = ResumeCurrentThread \<longrightarrow> no_orphans s) \<and> (action = ChooseNewThread \<longrightarrow> ?R14 curThread action s) \<and> (\<forall>x. action = SwitchToThread x \<longrightarrow> ?R15 curThread action x s)\<rbrace>
 4. \<lbrace>?Q\<rbrace> getCurThread \<lbrace>?B1\<rbrace>
 5. \<And>s. no_orphans s \<and> invs' s \<Longrightarrow> ?Q s proof (prove)
goal (9 subgoals):
 1. \<And>curThread curRunnable x xa xb t. \<lbrace>?P31 curThread curRunnable x xa xb t\<rbrace> chooseThread \<lbrace>\<lambda>rv s. sch_act_not t s \<or> t \<in> all_queued_tcb_ptrs s \<or> ksCurThread s = t\<rbrace>
 2. \<And>curThread curRunnable x xa. \<lbrace>?B26 curThread curRunnable x xa\<rbrace> if xa = 0 then nextDomain else return () \<lbrace>\<lambda>xb s. (no_orphans s \<and> all_invs_but_ct_idle_or_in_cur_domain' s \<and> (is_active_tcb_ptr (ksCurThread s) s \<longrightarrow> ksCurThread s \<in> all_queued_tcb_ptrs s)) \<and> (\<forall>xc. ?P31 curThread curRunnable x xa xb xc s)\<rbrace>
 3. \<And>curThread curRunnable x. \<lbrace>?B25 curThread curRunnable x\<rbrace> getDomainTime \<lbrace>?B26 curThread curRunnable x\<rbrace>
 4. \<And>curThread curRunnable. \<lbrace>?B24 curThread curRunnable\<rbrace> if curRunnable then tcbSchedEnqueue curThread else return () \<lbrace>?B25 curThread curRunnable\<rbrace>
 5. \<And>curThread. \<lbrace>?R14 curThread (ds_id ChooseNewThread)\<rbrace> isRunnable curThread \<lbrace>?B24 curThread\<rbrace>
 6. \<And>curThread action x3. action = SwitchToThread x3 \<Longrightarrow> \<lbrace>?R15 curThread action x3\<rbrace> do wasRunnable <- isRunnable curThread;
when wasRunnable (tcbSchedEnqueue curThread);
idleThread <- getIdleThread;
targetPrio <- threadGet tcbPriority x3;
curPrio <- threadGet tcbPriority curThread;
fastfail <- scheduleSwitchThreadFastfail curThread idleThread curPrio targetPrio;
curDom <- curDomain;
highest <- isHighestPrio curDom targetPrio;
if fastfail \<and> \<not> highest then do tcbSchedEnqueue x3;
setSchedulerAction ChooseNewThread;
scheduleChooseNewThread
od else if wasRunnable \<and> curPrio = targetPrio then do tcbSchedAppend x3;
setSchedulerAction ChooseNewThread;
scheduleChooseNewThread
od else do global.switchToThread x3;
setSchedulerAction ResumeCurrentThread
od
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>
 7. \<And>curThread. \<lbrace>?B1 curThread\<rbrace> getSchedulerAction \<lbrace>\<lambda>action s. (action = ResumeCurrentThread \<longrightarrow> no_orphans s) \<and> (action = ChooseNewThread \<longrightarrow> ?R14 curThread action s) \<and> (\<forall>x. action = SwitchToThread x \<longrightarrow> ?R15 curThread action x s)\<rbrace>
 8. \<lbrace>?Q\<rbrace> getCurThread \<lbrace>?B1\<rbrace>
 9. \<And>s. no_orphans s \<and> invs' s \<Longrightarrow> ?Q s proof (prove)
goal (8 subgoals):
 1. \<And>curThread curRunnable x xa. \<lbrace>?B26 curThread curRunnable x xa\<rbrace> if xa = 0 then nextDomain else return () \<lbrace>\<lambda>xb s. (no_orphans s \<and> all_invs_but_ct_idle_or_in_cur_domain' s \<and> (is_active_tcb_ptr (ksCurThread s) s \<longrightarrow> ksCurThread s \<in> all_queued_tcb_ptrs s)) \<and> (\<forall>x. sch_act_not x s)\<rbrace>
 2. \<And>curThread curRunnable x. \<lbrace>?B25 curThread curRunnable x\<rbrace> getDomainTime \<lbrace>?B26 curThread curRunnable x\<rbrace>
 3. \<And>curThread curRunnable. \<lbrace>?B24 curThread curRunnable\<rbrace> if curRunnable then tcbSchedEnqueue curThread else return () \<lbrace>?B25 curThread curRunnable\<rbrace>
 4. \<And>curThread. \<lbrace>?R14 curThread (ds_id ChooseNewThread)\<rbrace> isRunnable curThread \<lbrace>?B24 curThread\<rbrace>
 5. \<And>curThread action x3. action = SwitchToThread x3 \<Longrightarrow> \<lbrace>?R15 curThread action x3\<rbrace> do wasRunnable <- isRunnable curThread;
when wasRunnable (tcbSchedEnqueue curThread);
idleThread <- getIdleThread;
targetPrio <- threadGet tcbPriority x3;
curPrio <- threadGet tcbPriority curThread;
fastfail <- scheduleSwitchThreadFastfail curThread idleThread curPrio targetPrio;
curDom <- curDomain;
highest <- isHighestPrio curDom targetPrio;
if fastfail \<and> \<not> highest then do tcbSchedEnqueue x3;
setSchedulerAction ChooseNewThread;
scheduleChooseNewThread
od else if wasRunnable \<and> curPrio = targetPrio then do tcbSchedAppend x3;
setSchedulerAction ChooseNewThread;
scheduleChooseNewThread
od else do global.switchToThread x3;
setSchedulerAction ResumeCurrentThread
od
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>
 6. \<And>curThread. \<lbrace>?B1 curThread\<rbrace> getSchedulerAction \<lbrace>\<lambda>action s. (action = ResumeCurrentThread \<longrightarrow> no_orphans s) \<and> (action = ChooseNewThread \<longrightarrow> ?R14 curThread action s) \<and> (\<forall>x. action = SwitchToThread x \<longrightarrow> ?R15 curThread action x s)\<rbrace>
 7. \<lbrace>?Q\<rbrace> getCurThread \<lbrace>?B1\<rbrace>
 8. \<And>s. no_orphans s \<and> invs' s \<Longrightarrow> ?Q s proof (prove)
goal (7 subgoals):
 1. \<And>curThread curRunnable x. \<lbrace>?B25 curThread curRunnable x\<rbrace> getDomainTime \<lbrace>\<lambda>xa s. (xa = 0 \<longrightarrow> no_orphans s \<and> (invs' and (\<lambda>s. ksSchedulerAction s = ChooseNewThread)) s \<and> (\<not> is_active_tcb_ptr (ksCurThread s) s \<or> ksCurThread s \<in> all_queued_tcb_ptrs s) \<and> (\<forall>x. sch_act_not x s)) \<and> (xa \<noteq> 0 \<longrightarrow> no_orphans s \<and> (all_invs_but_ct_idle_or_in_cur_domain' s \<and> (is_active_tcb_ptr (ksCurThread s) s \<longrightarrow> ksCurThread s \<in> all_queued_tcb_ptrs s)) \<and> (\<forall>x. sch_act_not x s))\<rbrace>
 2. \<And>curThread curRunnable. \<lbrace>?B24 curThread curRunnable\<rbrace> if curRunnable then tcbSchedEnqueue curThread else return () \<lbrace>?B25 curThread curRunnable\<rbrace>
 3. \<And>curThread. \<lbrace>?R14 curThread (ds_id ChooseNewThread)\<rbrace> isRunnable curThread \<lbrace>?B24 curThread\<rbrace>
 4. \<And>curThread action x3. action = SwitchToThread x3 \<Longrightarrow> \<lbrace>?R15 curThread action x3\<rbrace> do wasRunnable <- isRunnable curThread;
when wasRunnable (tcbSchedEnqueue curThread);
idleThread <- getIdleThread;
targetPrio <- threadGet tcbPriority x3;
curPrio <- threadGet tcbPriority curThread;
fastfail <- scheduleSwitchThreadFastfail curThread idleThread curPrio targetPrio;
curDom <- curDomain;
highest <- isHighestPrio curDom targetPrio;
if fastfail \<and> \<not> highest then do tcbSchedEnqueue x3;
setSchedulerAction ChooseNewThread;
scheduleChooseNewThread
od else if wasRunnable \<and> curPrio = targetPrio then do tcbSchedAppend x3;
setSchedulerAction ChooseNewThread;
scheduleChooseNewThread
od else do global.switchToThread x3;
setSchedulerAction ResumeCurrentThread
od
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>
 5. \<And>curThread. \<lbrace>?B1 curThread\<rbrace> getSchedulerAction \<lbrace>\<lambda>action s. (action = ResumeCurrentThread \<longrightarrow> no_orphans s) \<and> (action = ChooseNewThread \<longrightarrow> ?R14 curThread action s) \<and> (\<forall>x. action = SwitchToThread x \<longrightarrow> ?R15 curThread action x s)\<rbrace>
 6. \<lbrace>?Q\<rbrace> getCurThread \<lbrace>?B1\<rbrace>
 7. \<And>s. no_orphans s \<and> invs' s \<Longrightarrow> ?Q s proof (prove)
goal (6 subgoals):
 1. \<And>curThread curRunnable. \<lbrace>?B24 curThread curRunnable\<rbrace> if curRunnable then tcbSchedEnqueue curThread else return () \<lbrace>\<lambda>x s. (no_orphans s \<and> (invs' and (\<lambda>s. ksSchedulerAction s = ChooseNewThread)) s \<and> (\<not> is_active_tcb_ptr (ksCurThread s) s \<or> ksCurThread s \<in> all_queued_tcb_ptrs s) \<and> (\<forall>x. sch_act_not x s)) \<and> no_orphans s \<and> (all_invs_but_ct_idle_or_in_cur_domain' s \<and> (is_active_tcb_ptr (ksCurThread s) s \<longrightarrow> ksCurThread s \<in> all_queued_tcb_ptrs s)) \<and> (\<forall>x. sch_act_not x s)\<rbrace>
 2. \<And>curThread. \<lbrace>?R14 curThread (ds_id ChooseNewThread)\<rbrace> isRunnable curThread \<lbrace>?B24 curThread\<rbrace>
 3. \<And>curThread action x3. action = SwitchToThread x3 \<Longrightarrow> \<lbrace>?R15 curThread action x3\<rbrace> do wasRunnable <- isRunnable curThread;
when wasRunnable (tcbSchedEnqueue curThread);
idleThread <- getIdleThread;
targetPrio <- threadGet tcbPriority x3;
curPrio <- threadGet tcbPriority curThread;
fastfail <- scheduleSwitchThreadFastfail curThread idleThread curPrio targetPrio;
curDom <- curDomain;
highest <- isHighestPrio curDom targetPrio;
if fastfail \<and> \<not> highest then do tcbSchedEnqueue x3;
setSchedulerAction ChooseNewThread;
scheduleChooseNewThread
od else if wasRunnable \<and> curPrio = targetPrio then do tcbSchedAppend x3;
setSchedulerAction ChooseNewThread;
scheduleChooseNewThread
od else do global.switchToThread x3;
setSchedulerAction ResumeCurrentThread
od
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>
 4. \<And>curThread. \<lbrace>?B1 curThread\<rbrace> getSchedulerAction \<lbrace>\<lambda>action s. (action = ResumeCurrentThread \<longrightarrow> no_orphans s) \<and> (action = ChooseNewThread \<longrightarrow> ?R14 curThread action s) \<and> (\<forall>x. action = SwitchToThread x \<longrightarrow> ?R15 curThread action x s)\<rbrace>
 5. \<lbrace>?Q\<rbrace> getCurThread \<lbrace>?B1\<rbrace>
 6. \<And>s. no_orphans s \<and> invs' s \<Longrightarrow> ?Q s proof (prove)
goal (5 subgoals):
 1. \<And>curThread. \<lbrace>?R14 curThread (ds_id ChooseNewThread)\<rbrace> isRunnable curThread \<lbrace>\<lambda>curRunnable s. (curRunnable \<longrightarrow> no_orphans s \<and> (invs' and st_tcb_at' runnable' curThread and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> curThread)) s \<and> ksSchedulerAction s = ChooseNewThread \<and> (valid_queues' and tcb_at' (ksCurThread s) and K (ksCurThread s = curThread)) s \<and> (\<forall>x. sch_act_not x s) \<and> no_orphans s \<and> (invs' and st_tcb_at' runnable' curThread and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> curThread)) s \<and> (valid_queues' and tcb_at' (ksCurThread s) and K (ksCurThread s = curThread)) s \<and> (\<forall>x. sch_act_not x s)) \<and> (\<not> curRunnable \<longrightarrow> no_orphans s \<and> ((invs' and (\<lambda>s. ksSchedulerAction s = ChooseNewThread)) s \<and> (\<not> is_active_tcb_ptr (ksCurThread s) s \<or> ksCurThread s \<in> all_queued_tcb_ptrs s) \<and> (\<forall>x. sch_act_not x s)) \<and> no_orphans s \<and> (all_invs_but_ct_idle_or_in_cur_domain' s \<and> (is_active_tcb_ptr (ksCurThread s) s \<longrightarrow> ksCurThread s \<in> all_queued_tcb_ptrs s)) \<and> (\<forall>x. sch_act_not x s))\<rbrace>
 2. \<And>curThread action x3. action = SwitchToThread x3 \<Longrightarrow> \<lbrace>?R15 curThread action x3\<rbrace> do wasRunnable <- isRunnable curThread;
when wasRunnable (tcbSchedEnqueue curThread);
idleThread <- getIdleThread;
targetPrio <- threadGet tcbPriority x3;
curPrio <- threadGet tcbPriority curThread;
fastfail <- scheduleSwitchThreadFastfail curThread idleThread curPrio targetPrio;
curDom <- curDomain;
highest <- isHighestPrio curDom targetPrio;
if fastfail \<and> \<not> highest then do tcbSchedEnqueue x3;
setSchedulerAction ChooseNewThread;
scheduleChooseNewThread
od else if wasRunnable \<and> curPrio = targetPrio then do tcbSchedAppend x3;
setSchedulerAction ChooseNewThread;
scheduleChooseNewThread
od else do global.switchToThread x3;
setSchedulerAction ResumeCurrentThread
od
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>
 3. \<And>curThread. \<lbrace>?B1 curThread\<rbrace> getSchedulerAction \<lbrace>\<lambda>action s. (action = ResumeCurrentThread \<longrightarrow> no_orphans s) \<and> (action = ChooseNewThread \<longrightarrow> ?R14 curThread action s) \<and> (\<forall>x. action = SwitchToThread x \<longrightarrow> ?R15 curThread action x s)\<rbrace>
 4. \<lbrace>?Q\<rbrace> getCurThread \<lbrace>?B1\<rbrace>
 5. \<And>s. no_orphans s \<and> invs' s \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>curThread action x3. action = SwitchToThread x3 \<Longrightarrow> \<lbrace>?R15 curThread action x3\<rbrace> do wasRunnable <- isRunnable curThread;
when wasRunnable (tcbSchedEnqueue curThread);
idleThread <- getIdleThread;
targetPrio <- threadGet tcbPriority x3;
curPrio <- threadGet tcbPriority curThread;
fastfail <- scheduleSwitchThreadFastfail curThread idleThread curPrio targetPrio;
curDom <- curDomain;
highest <- isHighestPrio curDom targetPrio;
if fastfail \<and> \<not> highest then do tcbSchedEnqueue x3;
setSchedulerAction ChooseNewThread;
scheduleChooseNewThread
od else if wasRunnable \<and> curPrio = targetPrio then do tcbSchedAppend x3;
setSchedulerAction ChooseNewThread;
scheduleChooseNewThread
od else do global.switchToThread x3;
setSchedulerAction ResumeCurrentThread
od
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>
 2. \<And>curThread. \<lbrace>?B1 curThread\<rbrace> getSchedulerAction \<lbrace>\<lambda>action s. (action = ResumeCurrentThread \<longrightarrow> no_orphans s) \<and> (action = ChooseNewThread \<longrightarrow> (st_tcb_at' runnable' curThread s \<longrightarrow> no_orphans s \<and> (invs' and st_tcb_at' runnable' curThread and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> curThread)) s \<and> ksSchedulerAction s = ChooseNewThread \<and> (valid_queues' and tcb_at' (ksCurThread s) and K (ksCurThread s = curThread)) s \<and> (\<forall>x. sch_act_not x s) \<and> no_orphans s \<and> (invs' and st_tcb_at' runnable' curThread and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> curThread)) s \<and> (valid_queues' and tcb_at' (ksCurThread s) and K (ksCurThread s = curThread)) s \<and> (\<forall>x. sch_act_not x s)) \<and> (\<not> st_tcb_at' runnable' curThread s \<longrightarrow> no_orphans s \<and> ((invs' and (\<lambda>s. ksSchedulerAction s = ChooseNewThread)) s \<and> (\<not> is_active_tcb_ptr (ksCurThread s) s \<or> ksCurThread s \<in> all_queued_tcb_ptrs s) \<and> (\<forall>x. sch_act_not x s)) \<and> no_orphans s \<and> (all_invs_but_ct_idle_or_in_cur_domain' s \<and> (is_active_tcb_ptr (ksCurThread s) s \<longrightarrow> ksCurThread s \<in> all_queued_tcb_ptrs s)) \<and> (\<forall>x. sch_act_not x s))) \<and> (\<forall>x. action = SwitchToThread x \<longrightarrow> ?R15 curThread action x s)\<rbrace>
 3. \<lbrace>?Q\<rbrace> getCurThread \<lbrace>?B1\<rbrace>
 4. \<And>s. no_orphans s \<and> invs' s \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>curThread x3. \<lbrace>?R15 curThread (SwitchToThread x3) x3\<rbrace> do wasRunnable <- isRunnable curThread;
y <- when wasRunnable (tcbSchedEnqueue curThread);
idleThread <- getIdleThread;
targetPrio <- threadGet tcbPriority x3;
curPrio <- threadGet tcbPriority curThread;
fastfail <- scheduleSwitchThreadFastfail curThread idleThread curPrio targetPrio;
curDom <- curDomain;
highest <- isHighestPrio curDom targetPrio;
if fastfail \<and> \<not> highest then do tcbSchedEnqueue x3;
setSchedulerAction ChooseNewThread;
scheduleChooseNewThread
od else if wasRunnable \<and> curPrio = targetPrio then do tcbSchedAppend x3;
setSchedulerAction ChooseNewThread;
scheduleChooseNewThread
od else do global.switchToThread x3;
setSchedulerAction ResumeCurrentThread
od
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>
 2. \<And>curThread. \<lbrace>?B1 curThread\<rbrace> getSchedulerAction \<lbrace>\<lambda>action s. (action = ResumeCurrentThread \<longrightarrow> no_orphans s) \<and> (action = ChooseNewThread \<longrightarrow> (st_tcb_at' runnable' curThread s \<longrightarrow> no_orphans s \<and> (invs' and st_tcb_at' runnable' curThread and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> curThread)) s \<and> ksSchedulerAction s = ChooseNewThread \<and> (valid_queues' and tcb_at' (ksCurThread s) and K (ksCurThread s = curThread)) s \<and> (\<forall>x. sch_act_not x s) \<and> no_orphans s \<and> (invs' and st_tcb_at' runnable' curThread and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> curThread)) s \<and> (valid_queues' and tcb_at' (ksCurThread s) and K (ksCurThread s = curThread)) s \<and> (\<forall>x. sch_act_not x s)) \<and> (\<not> st_tcb_at' runnable' curThread s \<longrightarrow> no_orphans s \<and> ((invs' and (\<lambda>s. ksSchedulerAction s = ChooseNewThread)) s \<and> (\<not> is_active_tcb_ptr (ksCurThread s) s \<or> ksCurThread s \<in> all_queued_tcb_ptrs s) \<and> (\<forall>x. sch_act_not x s)) \<and> no_orphans s \<and> (all_invs_but_ct_idle_or_in_cur_domain' s \<and> (is_active_tcb_ptr (ksCurThread s) s \<longrightarrow> ksCurThread s \<in> all_queued_tcb_ptrs s)) \<and> (\<forall>x. sch_act_not x s))) \<and> (\<forall>x. action = SwitchToThread x \<longrightarrow> ?R15 curThread action x s)\<rbrace>
 3. \<lbrace>?Q\<rbrace> getCurThread \<lbrace>?B1\<rbrace>
 4. \<And>s. no_orphans s \<and> invs' s \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>curThread candidate. \<lbrace>?R15 curThread (SwitchToThread candidate) candidate\<rbrace> do wasRunnable <- isRunnable curThread;
y <- when wasRunnable (tcbSchedEnqueue curThread);
idleThread <- getIdleThread;
targetPrio <- threadGet tcbPriority candidate;
curPrio <- threadGet tcbPriority curThread;
fastfail <- scheduleSwitchThreadFastfail curThread idleThread curPrio targetPrio;
curDom <- curDomain;
highest <- isHighestPrio curDom targetPrio;
if fastfail \<and> \<not> highest then do tcbSchedEnqueue candidate;
setSchedulerAction ChooseNewThread;
scheduleChooseNewThread
od else if wasRunnable \<and> curPrio = targetPrio then do tcbSchedAppend candidate;
setSchedulerAction ChooseNewThread;
scheduleChooseNewThread
od else do global.switchToThread candidate;
setSchedulerAction ResumeCurrentThread
od
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>
 2. \<And>curThread. \<lbrace>?B1 curThread\<rbrace> getSchedulerAction \<lbrace>\<lambda>action s. (action = ResumeCurrentThread \<longrightarrow> no_orphans s) \<and> (action = ChooseNewThread \<longrightarrow> (st_tcb_at' runnable' curThread s \<longrightarrow> no_orphans s \<and> (invs' and st_tcb_at' runnable' curThread and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> curThread)) s \<and> ksSchedulerAction s = ChooseNewThread \<and> (valid_queues' and tcb_at' (ksCurThread s) and K (ksCurThread s = curThread)) s \<and> (\<forall>x. sch_act_not x s) \<and> no_orphans s \<and> (invs' and st_tcb_at' runnable' curThread and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> curThread)) s \<and> (valid_queues' and tcb_at' (ksCurThread s) and K (ksCurThread s = curThread)) s \<and> (\<forall>x. sch_act_not x s)) \<and> (\<not> st_tcb_at' runnable' curThread s \<longrightarrow> no_orphans s \<and> ((invs' and (\<lambda>s. ksSchedulerAction s = ChooseNewThread)) s \<and> (\<not> is_active_tcb_ptr (ksCurThread s) s \<or> ksCurThread s \<in> all_queued_tcb_ptrs s) \<and> (\<forall>x. sch_act_not x s)) \<and> no_orphans s \<and> (all_invs_but_ct_idle_or_in_cur_domain' s \<and> (is_active_tcb_ptr (ksCurThread s) s \<longrightarrow> ksCurThread s \<in> all_queued_tcb_ptrs s)) \<and> (\<forall>x. sch_act_not x s))) \<and> (\<forall>x. action = SwitchToThread x \<longrightarrow> ?R15 curThread action x s)\<rbrace>
 3. \<lbrace>?Q\<rbrace> getCurThread \<lbrace>?B1\<rbrace>
 4. \<And>s. no_orphans s \<and> invs' s \<Longrightarrow> ?Q s proof (prove)
goal (11 subgoals):
 1. \<And>curThread candidate wasRunnable xa xb xc xd xe. \<lbrace>?B171 curThread candidate wasRunnable () xa xb xc xd xe\<rbrace> isHighestPrio xe xb \<lbrace>\<lambda>xf s. (xd \<and> \<not> xf \<longrightarrow> no_orphans s \<and> invs' s \<and> valid_queues' s \<and> ksSchedulerAction s = SwitchToThread candidate \<and> (st_tcb_at' runnable' (ksCurThread s) s \<longrightarrow> (\<exists>d p. ksCurThread s \<in> set (ksReadyQueues s (d, p))))) \<and> ((xd \<longrightarrow> xf) \<longrightarrow> (wasRunnable \<and> xc = xb \<longrightarrow> no_orphans s \<and> invs' s \<and> valid_queues' s \<and> ksSchedulerAction s = SwitchToThread candidate \<and> (st_tcb_at' runnable' (ksCurThread s) s \<longrightarrow> (\<exists>d p. ksCurThread s \<in> set (ksReadyQueues s (d, p))))) \<and> ((wasRunnable \<longrightarrow> xc \<noteq> xb) \<longrightarrow> no_orphans s \<and> ksSchedulerAction s = SwitchToThread candidate \<and> st_tcb_at' runnable' candidate s \<and> (st_tcb_at' runnable' (ksCurThread s) s \<longrightarrow> (\<exists>d p. ksCurThread s \<in> set (ksReadyQueues s (d, p))))))\<rbrace>
 2. \<And>curThread candidate wasRunnable x xa xb xc xd. \<lbrace>?B170 curThread candidate wasRunnable x xa xb xc xd\<rbrace> curDomain \<lbrace>?B171 curThread candidate wasRunnable x xa xb xc xd\<rbrace>
 3. \<And>curThread candidate wasRunnable x xa xb xc. \<lbrace>?B169 curThread candidate wasRunnable x xa xb xc\<rbrace> scheduleSwitchThreadFastfail curThread xa xc xb \<lbrace>?B170 curThread candidate wasRunnable x xa xb xc\<rbrace>
 4. \<And>curThread candidate wasRunnable x xa xb. \<lbrace>?B168 curThread candidate wasRunnable x xa xb\<rbrace> threadGet tcbPriority curThread \<lbrace>?B169 curThread candidate wasRunnable x xa xb\<rbrace>
 5. \<And>curThread candidate wasRunnable x xa. \<lbrace>?B167 curThread candidate wasRunnable x xa\<rbrace> threadGet tcbPriority candidate \<lbrace>?B168 curThread candidate wasRunnable x xa\<rbrace>
 6. \<And>curThread candidate wasRunnable x. \<lbrace>?B166 curThread candidate wasRunnable x\<rbrace> getIdleThread \<lbrace>?B167 curThread candidate wasRunnable x\<rbrace>
 7. \<And>curThread candidate wasRunnable. \<lbrace>?B165 curThread candidate wasRunnable\<rbrace> when wasRunnable (tcbSchedEnqueue curThread) \<lbrace>?B166 curThread candidate wasRunnable\<rbrace>
 8. \<And>curThread candidate. \<lbrace>?R15 curThread (SwitchToThread candidate) candidate\<rbrace> isRunnable curThread \<lbrace>?B165 curThread candidate\<rbrace>
 9. \<And>curThread. \<lbrace>?B1 curThread\<rbrace> getSchedulerAction \<lbrace>\<lambda>action s. (action = ResumeCurrentThread \<longrightarrow> no_orphans s) \<and> (action = ChooseNewThread \<longrightarrow> (st_tcb_at' runnable' curThread s \<longrightarrow> no_orphans s \<and> (invs' and st_tcb_at' runnable' curThread and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> curThread)) s \<and> ksSchedulerAction s = ChooseNewThread \<and> (valid_queues' and tcb_at' (ksCurThread s) and K (ksCurThread s = curThread)) s \<and> (\<forall>x. sch_act_not x s) \<and> no_orphans s \<and> (invs' and st_tcb_at' runnable' curThread and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> curThread)) s \<and> (valid_queues' and tcb_at' (ksCurThread s) and K (ksCurThread s = curThread)) s \<and> (\<forall>x. sch_act_not x s)) \<and> (\<not> st_tcb_at' runnable' curThread s \<longrightarrow> no_orphans s \<and> ((invs' and (\<lambda>s. ksSchedulerAction s = ChooseNewThread)) s \<and> (\<not> is_active_tcb_ptr (ksCurThread s) s \<or> ksCurThread s \<in> all_queued_tcb_ptrs s) \<and> (\<forall>x. sch_act_not x s)) \<and> no_orphans s \<and> (all_invs_but_ct_idle_or_in_cur_domain' s \<and> (is_active_tcb_ptr (ksCurThread s) s \<longrightarrow> ksCurThread s \<in> all_queued_tcb_ptrs s)) \<and> (\<forall>x. sch_act_not x s))) \<and> (\<forall>x. action = SwitchToThread x \<longrightarrow> ?R15 curThread action x s)\<rbrace>
 10. \<lbrace>?Q\<rbrace> getCurThread \<lbrace>?B1\<rbrace>
A total of 11 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>curThread candidate wasRunnable xa xb xc xd xe. \<lbrace>?B171 curThread candidate wasRunnable () xa xb xc xd xe\<rbrace> isHighestPrio xe xb \<lbrace>\<lambda>xf s. (xd \<and> \<not> xf \<longrightarrow> no_orphans s \<and> invs' s \<and> valid_queues' s \<and> ksSchedulerAction s = SwitchToThread candidate \<and> (st_tcb_at' runnable' (ksCurThread s) s \<longrightarrow> (\<exists>d p. ksCurThread s \<in> set (ksReadyQueues s (d, p))))) \<and> ((xd \<longrightarrow> xf) \<longrightarrow> (wasRunnable \<and> xc = xb \<longrightarrow> no_orphans s \<and> invs' s \<and> valid_queues' s \<and> ksSchedulerAction s = SwitchToThread candidate \<and> (st_tcb_at' runnable' (ksCurThread s) s \<longrightarrow> (\<exists>d p. ksCurThread s \<in> set (ksReadyQueues s (d, p))))) \<and> ((wasRunnable \<longrightarrow> xc \<noteq> xb) \<longrightarrow> no_orphans s \<and> ksSchedulerAction s = SwitchToThread candidate \<and> st_tcb_at' runnable' candidate s \<and> (st_tcb_at' runnable' (ksCurThread s) s \<longrightarrow> (\<exists>d p. ksCurThread s \<in> set (ksReadyQueues s (d, p))))))\<rbrace>
 2. \<And>curThread candidate wasRunnable x xa xb xc xd. \<lbrace>?B170 curThread candidate wasRunnable x xa xb xc xd\<rbrace> curDomain \<lbrace>?B171 curThread candidate wasRunnable x xa xb xc xd\<rbrace>
 3. \<And>curThread candidate wasRunnable x xa xb xc. \<lbrace>?B169 curThread candidate wasRunnable x xa xb xc\<rbrace> scheduleSwitchThreadFastfail curThread xa xc xb \<lbrace>?B170 curThread candidate wasRunnable x xa xb xc\<rbrace>
 4. \<And>curThread candidate wasRunnable x xa xb. \<lbrace>?B168 curThread candidate wasRunnable x xa xb\<rbrace> threadGet tcbPriority curThread \<lbrace>?B169 curThread candidate wasRunnable x xa xb\<rbrace>
 5. \<And>curThread candidate wasRunnable x xa. \<lbrace>?B167 curThread candidate wasRunnable x xa\<rbrace> threadGet tcbPriority candidate \<lbrace>?B168 curThread candidate wasRunnable x xa\<rbrace>
 6. \<And>curThread candidate wasRunnable x. \<lbrace>?B166 curThread candidate wasRunnable x\<rbrace> getIdleThread \<lbrace>?B167 curThread candidate wasRunnable x\<rbrace>
 7. \<And>curThread candidate wasRunnable. \<lbrace>?B165 curThread candidate wasRunnable\<rbrace> when wasRunnable (tcbSchedEnqueue curThread) \<lbrace>?B166 curThread candidate wasRunnable\<rbrace>
 8. \<And>curThread candidate. \<lbrace>?R15 curThread (SwitchToThread candidate) candidate\<rbrace> isRunnable curThread \<lbrace>?B165 curThread candidate\<rbrace>
 9. \<And>curThread. \<lbrace>?B1 curThread\<rbrace> getSchedulerAction \<lbrace>\<lambda>action s. (action = ResumeCurrentThread \<longrightarrow> no_orphans s) \<and> (action = ChooseNewThread \<longrightarrow> (st_tcb_at' runnable' curThread s \<longrightarrow> no_orphans s \<and> (invs' and st_tcb_at' runnable' curThread and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> curThread)) s \<and> ksSchedulerAction s = ChooseNewThread \<and> (valid_queues' and tcb_at' (ksCurThread s) and K (ksCurThread s = curThread)) s \<and> (\<forall>x. sch_act_not x s) \<and> no_orphans s \<and> (invs' and st_tcb_at' runnable' curThread and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> curThread)) s \<and> (valid_queues' and tcb_at' (ksCurThread s) and K (ksCurThread s = curThread)) s \<and> (\<forall>x. sch_act_not x s)) \<and> (\<not> st_tcb_at' runnable' curThread s \<longrightarrow> no_orphans s \<and> ((invs' and (\<lambda>s. ksSchedulerAction s = ChooseNewThread)) s \<and> (\<not> is_active_tcb_ptr (ksCurThread s) s \<or> ksCurThread s \<in> all_queued_tcb_ptrs s) \<and> (\<forall>x. sch_act_not x s)) \<and> no_orphans s \<and> (all_invs_but_ct_idle_or_in_cur_domain' s \<and> (is_active_tcb_ptr (ksCurThread s) s \<longrightarrow> ksCurThread s \<in> all_queued_tcb_ptrs s)) \<and> (\<forall>x. sch_act_not x s))) \<and> (\<forall>x. action = SwitchToThread x \<longrightarrow> ?R15 curThread action x s)\<rbrace>
 10. \<lbrace>?Q\<rbrace> getCurThread \<lbrace>?B1\<rbrace>
A total of 11 subgoals... proof (prove)
goal (10 subgoals):
 1. \<And>curThread candidate wasRunnable x xa xb xc xd. \<lbrace>?B170 curThread candidate wasRunnable x xa xb xc xd\<rbrace> curDomain \<lbrace>\<lambda>a b. (no_orphans b \<and> invs' b \<and> valid_queues' b \<and> ksSchedulerAction b = SwitchToThread candidate \<and> (st_tcb_at' runnable' (ksCurThread b) b \<longrightarrow> (\<exists>d p. ksCurThread b \<in> set (ksReadyQueues b (d, p))))) \<and> (no_orphans b \<and> invs' b \<and> valid_queues' b \<and> ksSchedulerAction b = SwitchToThread candidate \<and> (st_tcb_at' runnable' (ksCurThread b) b \<longrightarrow> (\<exists>d p. ksCurThread b \<in> set (ksReadyQueues b (d, p))))) \<and> no_orphans b \<and> ksSchedulerAction b = SwitchToThread candidate \<and> st_tcb_at' runnable' candidate b \<and> (st_tcb_at' runnable' (ksCurThread b) b \<longrightarrow> (\<exists>d p. ksCurThread b \<in> set (ksReadyQueues b (d, p))))\<rbrace>
 2. \<And>curThread candidate wasRunnable x xa xb xc. \<lbrace>?B169 curThread candidate wasRunnable x xa xb xc\<rbrace> scheduleSwitchThreadFastfail curThread xa xc xb \<lbrace>?B170 curThread candidate wasRunnable x xa xb xc\<rbrace>
 3. \<And>curThread candidate wasRunnable x xa xb. \<lbrace>?B168 curThread candidate wasRunnable x xa xb\<rbrace> threadGet tcbPriority curThread \<lbrace>?B169 curThread candidate wasRunnable x xa xb\<rbrace>
 4. \<And>curThread candidate wasRunnable x xa. \<lbrace>?B167 curThread candidate wasRunnable x xa\<rbrace> threadGet tcbPriority candidate \<lbrace>?B168 curThread candidate wasRunnable x xa\<rbrace>
 5. \<And>curThread candidate wasRunnable x. \<lbrace>?B166 curThread candidate wasRunnable x\<rbrace> getIdleThread \<lbrace>?B167 curThread candidate wasRunnable x\<rbrace>
 6. \<And>curThread candidate wasRunnable. \<lbrace>?B165 curThread candidate wasRunnable\<rbrace> when wasRunnable (tcbSchedEnqueue curThread) \<lbrace>?B166 curThread candidate wasRunnable\<rbrace>
 7. \<And>curThread candidate. \<lbrace>?R15 curThread (SwitchToThread candidate) candidate\<rbrace> isRunnable curThread \<lbrace>?B165 curThread candidate\<rbrace>
 8. \<And>curThread. \<lbrace>?B1 curThread\<rbrace> getSchedulerAction \<lbrace>\<lambda>action s. (action = ResumeCurrentThread \<longrightarrow> no_orphans s) \<and> (action = ChooseNewThread \<longrightarrow> (st_tcb_at' runnable' curThread s \<longrightarrow> no_orphans s \<and> (invs' and st_tcb_at' runnable' curThread and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> curThread)) s \<and> ksSchedulerAction s = ChooseNewThread \<and> (valid_queues' and tcb_at' (ksCurThread s) and K (ksCurThread s = curThread)) s \<and> (\<forall>x. sch_act_not x s) \<and> no_orphans s \<and> (invs' and st_tcb_at' runnable' curThread and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> curThread)) s \<and> (valid_queues' and tcb_at' (ksCurThread s) and K (ksCurThread s = curThread)) s \<and> (\<forall>x. sch_act_not x s)) \<and> (\<not> st_tcb_at' runnable' curThread s \<longrightarrow> no_orphans s \<and> ((invs' and (\<lambda>s. ksSchedulerAction s = ChooseNewThread)) s \<and> (\<not> is_active_tcb_ptr (ksCurThread s) s \<or> ksCurThread s \<in> all_queued_tcb_ptrs s) \<and> (\<forall>x. sch_act_not x s)) \<and> no_orphans s \<and> (all_invs_but_ct_idle_or_in_cur_domain' s \<and> (is_active_tcb_ptr (ksCurThread s) s \<longrightarrow> ksCurThread s \<in> all_queued_tcb_ptrs s)) \<and> (\<forall>x. sch_act_not x s))) \<and> (\<forall>x. action = SwitchToThread x \<longrightarrow> ?R15 curThread action x s)\<rbrace>
 9. \<lbrace>?Q\<rbrace> getCurThread \<lbrace>?B1\<rbrace>
 10. \<And>s. no_orphans s \<and> invs' s \<Longrightarrow> ?Q s proof (prove)
goal (5 subgoals):
 1. \<And>curThread candidate wasRunnable. wasRunnable \<Longrightarrow> \<lbrace>?P'223 curThread candidate wasRunnable\<rbrace> tcbSchedEnqueue curThread \<lbrace>\<lambda>rv s. (st_tcb_at' runnable' (ksCurThread s) s \<longrightarrow> (\<exists>d p. ksCurThread s \<in> set (ksReadyQueues s (d, p)))) \<and> (no_orphans s \<and> invs' s \<and> valid_queues' s \<and> ksSchedulerAction s = SwitchToThread candidate \<and> (st_tcb_at' runnable' (ksCurThread s) s \<longrightarrow> (\<exists>d p. ksCurThread s \<in> set (ksReadyQueues s (d, p))))) \<and> no_orphans s \<and> ksSchedulerAction s = SwitchToThread candidate \<and> st_tcb_at' runnable' candidate s \<and> (st_tcb_at' runnable' (ksCurThread s) s \<longrightarrow> (\<exists>d p. ksCurThread s \<in> set (ksReadyQueues s (d, p))))\<rbrace>
 2. \<And>curThread candidate. \<lbrace>?R15 curThread (SwitchToThread candidate) candidate\<rbrace> isRunnable curThread \<lbrace>\<lambda>wasRunnable. if wasRunnable then \<lambda>s. no_orphans s \<and> (invs' and st_tcb_at' runnable' curThread and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> curThread)) s \<and> (valid_queues' and st_tcb_at' runnable' curThread) s \<and> ksSchedulerAction s = SwitchToThread candidate \<and> ?P'223 curThread candidate wasRunnable s else (\<lambda>s. no_orphans s \<and> (invs' s \<and> valid_queues' s \<and> ksSchedulerAction s = SwitchToThread candidate \<and> (st_tcb_at' runnable' (ksCurThread s) s \<longrightarrow> (\<exists>d p. ksCurThread s \<in> set (ksReadyQueues s (d, p))))) \<and> (no_orphans s \<and> invs' s \<and> valid_queues' s \<and> ksSchedulerAction s = SwitchToThread candidate \<and> (st_tcb_at' runnable' (ksCurThread s) s \<longrightarrow> (\<exists>d p. ksCurThread s \<in> set (ksReadyQueues s (d, p))))) \<and> no_orphans s \<and> ksSchedulerAction s = SwitchToThread candidate \<and> st_tcb_at' runnable' candidate s \<and> (st_tcb_at' runnable' (ksCurThread s) s \<longrightarrow> (\<exists>d p. ksCurThread s \<in> set (ksReadyQueues s (d, p)))))\<rbrace>
 3. \<And>curThread. \<lbrace>?B1 curThread\<rbrace> getSchedulerAction \<lbrace>\<lambda>action s. (action = ResumeCurrentThread \<longrightarrow> no_orphans s) \<and> (action = ChooseNewThread \<longrightarrow> (st_tcb_at' runnable' curThread s \<longrightarrow> no_orphans s \<and> (invs' and st_tcb_at' runnable' curThread and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> curThread)) s \<and> ksSchedulerAction s = ChooseNewThread \<and> (valid_queues' and tcb_at' (ksCurThread s) and K (ksCurThread s = curThread)) s \<and> (\<forall>x. sch_act_not x s) \<and> no_orphans s \<and> (invs' and st_tcb_at' runnable' curThread and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> curThread)) s \<and> (valid_queues' and tcb_at' (ksCurThread s) and K (ksCurThread s = curThread)) s \<and> (\<forall>x. sch_act_not x s)) \<and> (\<not> st_tcb_at' runnable' curThread s \<longrightarrow> no_orphans s \<and> ((invs' and (\<lambda>s. ksSchedulerAction s = ChooseNewThread)) s \<and> (\<not> is_active_tcb_ptr (ksCurThread s) s \<or> ksCurThread s \<in> all_queued_tcb_ptrs s) \<and> (\<forall>x. sch_act_not x s)) \<and> no_orphans s \<and> (all_invs_but_ct_idle_or_in_cur_domain' s \<and> (is_active_tcb_ptr (ksCurThread s) s \<longrightarrow> ksCurThread s \<in> all_queued_tcb_ptrs s)) \<and> (\<forall>x. sch_act_not x s))) \<and> (\<forall>x. action = SwitchToThread x \<longrightarrow> ?R15 curThread action x s)\<rbrace>
 4. \<lbrace>?Q\<rbrace> getCurThread \<lbrace>?B1\<rbrace>
 5. \<And>s. no_orphans s \<and> invs' s \<Longrightarrow> ?Q s proof (prove)
goal (5 subgoals):
 1. \<And>curThread candidate wasRunnable. wasRunnable \<Longrightarrow> \<lbrace>?P'223 curThread candidate True\<rbrace> tcbSchedEnqueue curThread \<lbrace>\<lambda>rv s. invs' s \<and> valid_queues' s \<and> no_orphans s \<and> ksSchedulerAction s = SwitchToThread candidate \<and> st_tcb_at' runnable' candidate s \<and> (st_tcb_at' runnable' (ksCurThread s) s \<longrightarrow> (\<exists>d p. ksCurThread s \<in> set (ksReadyQueues s (d, p))))\<rbrace>
 2. \<And>curThread candidate. \<lbrace>?R15 curThread (SwitchToThread candidate) candidate\<rbrace> isRunnable curThread \<lbrace>\<lambda>wasRunnable. if wasRunnable then \<lambda>s. no_orphans s \<and> (invs' and st_tcb_at' runnable' curThread and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> curThread)) s \<and> (valid_queues' and st_tcb_at' runnable' curThread) s \<and> ksSchedulerAction s = SwitchToThread candidate \<and> ?P'223 curThread candidate wasRunnable s else (\<lambda>s. no_orphans s \<and> (invs' s \<and> valid_queues' s \<and> ksSchedulerAction s = SwitchToThread candidate \<and> (st_tcb_at' runnable' (ksCurThread s) s \<longrightarrow> (\<exists>d p. ksCurThread s \<in> set (ksReadyQueues s (d, p))))) \<and> (no_orphans s \<and> invs' s \<and> valid_queues' s \<and> ksSchedulerAction s = SwitchToThread candidate \<and> (st_tcb_at' runnable' (ksCurThread s) s \<longrightarrow> (\<exists>d p. ksCurThread s \<in> set (ksReadyQueues s (d, p))))) \<and> no_orphans s \<and> ksSchedulerAction s = SwitchToThread candidate \<and> st_tcb_at' runnable' candidate s \<and> (st_tcb_at' runnable' (ksCurThread s) s \<longrightarrow> (\<exists>d p. ksCurThread s \<in> set (ksReadyQueues s (d, p)))))\<rbrace>
 3. \<And>curThread. \<lbrace>?B1 curThread\<rbrace> getSchedulerAction \<lbrace>\<lambda>action s. (action = ResumeCurrentThread \<longrightarrow> no_orphans s) \<and> (action = ChooseNewThread \<longrightarrow> (st_tcb_at' runnable' curThread s \<longrightarrow> no_orphans s \<and> (invs' and st_tcb_at' runnable' curThread and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> curThread)) s \<and> ksSchedulerAction s = ChooseNewThread \<and> (valid_queues' and tcb_at' (ksCurThread s) and K (ksCurThread s = curThread)) s \<and> (\<forall>x. sch_act_not x s) \<and> no_orphans s \<and> (invs' and st_tcb_at' runnable' curThread and (\<lambda>s. ksSchedulerAction s = ResumeCurrentThread \<longrightarrow> ksCurThread s \<noteq> curThread)) s \<and> (valid_queues' and tcb_at' (ksCurThread s) and K (ksCurThread s = curThread)) s \<and> (\<forall>x. sch_act_not x s)) \<and> (\<not> st_tcb_at' runnable' curThread s \<longrightarrow> no_orphans s \<and> ((invs' and (\<lambda>s. ksSchedulerAction s = ChooseNewThread)) s \<and> (\<not> is_active_tcb_ptr (ksCurThread s) s \<or> ksCurThread s \<in> all_queued_tcb_ptrs s) \<and> (\<forall>x. sch_act_not x s)) \<and> no_orphans s \<and> (all_invs_but_ct_idle_or_in_cur_domain' s \<and> (is_active_tcb_ptr (ksCurThread s) s \<longrightarrow> ksCurThread s \<in> all_queued_tcb_ptrs s)) \<and> (\<forall>x. sch_act_not x s))) \<and> (\<forall>x. action = SwitchToThread x \<longrightarrow> ?R15 curThread action x s)\<rbrace>
 4. \<lbrace>?Q\<rbrace> getCurThread \<lbrace>?B1\<rbrace>
 5. \<And>s. no_orphans s \<and> invs' s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. no_orphans s \<and> invs' s \<Longrightarrow> (\<not> \<not> \<not> ksSchedulerAction s \<noteq> ResumeCurrentThread \<longrightarrow> no_orphans s) \<and> (\<not> \<not> \<not> ksSchedulerAction s \<noteq> ChooseNewThread \<longrightarrow> (\<not> \<not> \<not> st_tcb_at' (Not \<circ> runnable') (ksCurThread s) s \<longrightarrow> no_orphans s \<and> (invs' and st_tcb_at' runnable' (ksCurThread s) and (\<lambda>sa. ksSchedulerAction sa = ResumeCurrentThread \<longrightarrow> ksCurThread sa \<noteq> ksCurThread s)) s \<and> ksSchedulerAction s = ChooseNewThread \<and> (valid_queues' and tcb_at' (ksCurThread s) and K (ksCurThread s = ksCurThread s)) s \<and> (\<forall>x. sch_act_not x s) \<and> no_orphans s \<and> (invs' and st_tcb_at' runnable' (ksCurThread s) and (\<lambda>sa. ksSchedulerAction sa = ResumeCurrentThread \<longrightarrow> ksCurThread sa \<noteq> ksCurThread s)) s \<and> (valid_queues' and tcb_at' (ksCurThread s) and K (ksCurThread s = ksCurThread s)) s \<and> (\<forall>x. sch_act_not x s)) \<and> (\<not> \<not> \<not> \<not> \<not> st_tcb_at' runnable' (ksCurThread s) s \<longrightarrow> no_orphans s \<and> ((invs' and (\<lambda>s. ksSchedulerAction s = ChooseNewThread)) s \<and> (\<not> is_active_tcb_ptr (ksCurThread s) s \<or> ksCurThread s \<in> all_queued_tcb_ptrs s) \<and> (\<forall>x. sch_act_not x s)) \<and> no_orphans s \<and> (all_invs_but_ct_idle_or_in_cur_domain' s \<and> (is_active_tcb_ptr (ksCurThread s) s \<longrightarrow> ksCurThread s \<in> all_queued_tcb_ptrs s)) \<and> (\<forall>x. sch_act_not x s))) \<and> (\<forall>x. ksSchedulerAction s = SwitchToThread x \<longrightarrow> (if st_tcb_at' runnable' (ksCurThread s) s then \<lambda>sa. no_orphans sa \<and> (invs' and st_tcb_at' runnable' (ksCurThread s) and (\<lambda>sa. ksSchedulerAction sa = ResumeCurrentThread \<longrightarrow> ksCurThread sa \<noteq> ksCurThread s)) sa \<and> (valid_queues' and st_tcb_at' runnable' (ksCurThread s)) sa \<and> ksSchedulerAction sa = ksSchedulerAction s \<and> (invs' and st_tcb_at' runnable' (ksCurThread s) and (\<lambda>sa. ksSchedulerAction sa = ResumeCurrentThread \<longrightarrow> ksCurThread sa \<noteq> ksCurThread s)) sa \<and> (valid_queues' and st_tcb_at' runnable' (ksCurThread s)) sa \<and> no_orphans sa \<and> ksSchedulerAction sa = ksSchedulerAction s \<and> st_tcb_at' runnable' x sa \<and> (\<not> st_tcb_at' (Not \<circ> runnable') (ksCurThread sa) sa \<longrightarrow> (valid_queues' and tcb_at' (ksCurThread sa) and K (ksCurThread sa = ksCurThread s)) sa) else (\<lambda>sa. no_orphans sa \<and> (invs' sa \<and> valid_queues' sa \<and> ksSchedulerAction sa = ksSchedulerAction s \<and> (st_tcb_at' runnable' (ksCurThread sa) sa \<longrightarrow> (\<exists>d p. ksCurThread sa \<in> set (ksReadyQueues sa (d, p))))) \<and> (no_orphans sa \<and> invs' sa \<and> valid_queues' sa \<and> ksSchedulerAction sa = ksSchedulerAction s \<and> (st_tcb_at' runnable' (ksCurThread sa) sa \<longrightarrow> (\<exists>d p. ksCurThread sa \<in> set (ksReadyQueues sa (d, p))))) \<and> no_orphans sa \<and> ksSchedulerAction sa = ksSchedulerAction s \<and> st_tcb_at' runnable' x sa \<and> (st_tcb_at' runnable' (ksCurThread sa) sa \<longrightarrow> (\<exists>d p. ksCurThread sa \<in> set (ksReadyQueues sa (d, p)))))) s) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>no_orphans s; invs' s\<rbrakk> \<Longrightarrow> (ksSchedulerAction s = ChooseNewThread \<longrightarrow> (\<not> st_tcb_at' (\<lambda>x. \<not> runnable' x) (ksCurThread s) s \<longrightarrow> st_tcb_at' runnable' (ksCurThread s) s \<and> valid_queues' s \<and> tcb_at' (ksCurThread s) s \<and> st_tcb_at' runnable' (ksCurThread s) s \<and> valid_queues' s \<and> tcb_at' (ksCurThread s) s) \<and> (\<not> st_tcb_at' runnable' (ksCurThread s) s \<longrightarrow> (is_active_tcb_ptr (ksCurThread s) s \<longrightarrow> ksCurThread s \<in> all_queued_tcb_ptrs s) \<and> all_invs_but_ct_idle_or_in_cur_domain' s \<and> (is_active_tcb_ptr (ksCurThread s) s \<longrightarrow> ksCurThread s \<in> all_queued_tcb_ptrs s))) \<and> (\<forall>x. (st_tcb_at' runnable' (ksCurThread s) s \<longrightarrow> ksSchedulerAction s = SwitchToThread x \<longrightarrow> valid_queues' s \<and> st_tcb_at' runnable' x s \<and> (\<not> st_tcb_at' (\<lambda>x. \<not> runnable' x) (ksCurThread s) s \<longrightarrow> valid_queues' s \<and> tcb_at' (ksCurThread s) s)) \<and> (\<not> st_tcb_at' runnable' (ksCurThread s) s \<longrightarrow> ksSchedulerAction s = SwitchToThread x \<longrightarrow> valid_queues' s \<and> st_tcb_at' runnable' x s)) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>no_orphans s; invs' s; Invariants_H.valid_queues s\<rbrakk> \<Longrightarrow> (ksSchedulerAction s = ChooseNewThread \<longrightarrow> (\<not> st_tcb_at' (\<lambda>x. \<not> runnable' x) (ksCurThread s) s \<longrightarrow> st_tcb_at' runnable' (ksCurThread s) s \<and> valid_queues' s \<and> tcb_at' (ksCurThread s) s \<and> st_tcb_at' runnable' (ksCurThread s) s \<and> valid_queues' s \<and> tcb_at' (ksCurThread s) s) \<and> (\<not> st_tcb_at' runnable' (ksCurThread s) s \<longrightarrow> (is_active_tcb_ptr (ksCurThread s) s \<longrightarrow> ksCurThread s \<in> all_queued_tcb_ptrs s) \<and> all_invs_but_ct_idle_or_in_cur_domain' s \<and> (is_active_tcb_ptr (ksCurThread s) s \<longrightarrow> ksCurThread s \<in> all_queued_tcb_ptrs s))) \<and> (\<forall>x. (st_tcb_at' runnable' (ksCurThread s) s \<longrightarrow> ksSchedulerAction s = SwitchToThread x \<longrightarrow> valid_queues' s \<and> st_tcb_at' runnable' x s \<and> (\<not> st_tcb_at' (\<lambda>x. \<not> runnable' x) (ksCurThread s) s \<longrightarrow> valid_queues' s \<and> tcb_at' (ksCurThread s) s)) \<and> (\<not> st_tcb_at' runnable' (ksCurThread s) s \<longrightarrow> ksSchedulerAction s = SwitchToThread x \<longrightarrow> valid_queues' s \<and> st_tcb_at' runnable' x s)) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>no_orphans s; invs' s; Invariants_H.valid_queues s\<rbrakk> \<Longrightarrow> (ksSchedulerAction s = ChooseNewThread \<longrightarrow> \<not> st_tcb_at' runnable' (ksCurThread s) s \<longrightarrow> all_invs_but_ct_idle_or_in_cur_domain' s) \<and> (\<forall>x. ksSchedulerAction s = SwitchToThread x \<longrightarrow> st_tcb_at' runnable' x s) proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrace>\<lambda>s. no_orphans s \<and> invs' s\<rbrace> ThreadDecls_H.schedule \<lbrace>\<lambda>rv. no_orphans\<rbrace>

goal:
No subgoals!