theory Schedule_R

lemma chooseThread_corres:
  "corres dc (invs and valid_sched) (invs_no_cicd')
     choose_thread chooseThread" (is "corres _ ?PREI ?PREH _ _") proof - show ?thesis unfolding choose_thread_def chooseThread_def apply (simp only: return_bind Let_def) apply (subst if_swap[where P="_ \<noteq> 0"])  (* put switchToIdleThread on first branch*)
   apply (rule corres_guard_imp) apply (rule corres_split[OF curDomain_corres']) apply clarsimp apply (rule corres_split[OF corres_gets_queues_getReadyQueuesL1Bitmap]) apply (erule corres_if2[OF sym]) apply (rule switchToIdleThread_corres) apply (rule corres_symb_exec_r) apply (rule corres_symb_exec_r) apply (rule_tac
                       P="\<lambda>s. ?PREI s \<and> queues = ready_queues s (cur_domain s) \<and>
                              st_tcb_at runnable (hd (max_non_empty_queue queues)) s" and
                       P'="\<lambda>s. (?PREH s \<and> st_tcb_at' runnable' (hd queue) s) \<and>
                               l1 = ksReadyQueuesL1Bitmap s (ksCurDomain s) \<and>
                               l1 \<noteq> 0 \<and>
                               queue = ksReadyQueues s (ksCurDomain s,
                                         lookupBitmapPriority (ksCurDomain s) s)" and
                       F="hd queue = hd (max_non_empty_queue queues)" in corres_req) apply (fastforce dest!: invs_no_cicd'_queues simp: bitmap_lookup_queue_is_max_non_empty) apply clarsimp apply (rule corres_guard_imp) apply (rule_tac P=\<top> and P'=\<top> in guarded_switch_to_chooseThread_fragment_corres) apply (wp | clarsimp simp: getQueue_def getReadyQueuesL2Bitmap_def)+ apply (clarsimp simp: if_apply_def2) apply (wp hoare_vcg_conj_lift hoare_vcg_imp_lift ksReadyQueuesL1Bitmap_return_wp) apply (wpsimp wp: curDomain_or_return_0 simp: curDomain_def)+ apply (fastforce simp: invs_no_cicd'_def) apply (clarsimp simp: valid_sched_def DetSchedInvs_AI.valid_queues_def max_non_empty_queue_def) apply (erule_tac x="cur_domain s" in allE) apply (erule_tac x="Max {prio. ready_queues s (cur_domain s) prio \<noteq> []}" in allE) apply (case_tac "ready_queues s (cur_domain s) (Max {prio. ready_queues s (cur_domain s) prio \<noteq> []})") apply (clarsimp) apply (subgoal_tac
             "ready_queues s (cur_domain s) (Max {prio. ready_queues s (cur_domain s) prio \<noteq> []}) \<noteq> []") apply (fastforce elim!: setcomp_Max_has_prop)+ apply (simp add: invs_no_cicd_ksCurDomain_maxDomain') apply (clarsimp dest!: invs_no_cicd'_queues) apply (fastforce intro: ksReadyQueuesL1Bitmap_st_tcb_at') done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. corres dc (invs and valid_sched) all_invs_but_ct_idle_or_in_cur_domain' choose_thread chooseThread proof (state)
goal (1 subgoal):
 1. corres dc (invs and valid_sched) all_invs_but_ct_idle_or_in_cur_domain' choose_thread chooseThread proof (prove)
goal (1 subgoal):
 1. corres dc (invs and valid_sched) all_invs_but_ct_idle_or_in_cur_domain' choose_thread chooseThread proof (prove)
goal (1 subgoal):
 1. corres dc (invs and valid_sched) all_invs_but_ct_idle_or_in_cur_domain' (do d <- gets cur_domain;
queues <- gets (\<lambda>s. ready_queues s d);
if \<forall>prio. queues prio = [] then switch_to_idle_thread else guarded_switch_to (hd (max_non_empty_queue queues))
od) (do curdom <- if 1 < numDomains then curDomain else return 0;
l1 <- getReadyQueuesL1Bitmap curdom;
if l1 \<noteq> 0 then do prio <- getHighestPrio curdom;
queue <- getQueue curdom prio;
thread <- return (head queue);
runnable <- isRunnable thread;
haskell_assert runnable [];
global.switchToThread thread
od else global.switchToIdleThread
od) proof (prove)
goal (1 subgoal):
 1. corres dc (invs and valid_sched) all_invs_but_ct_idle_or_in_cur_domain' (do d <- gets cur_domain;
queues <- gets (\<lambda>s. ready_queues s d);
if \<forall>prio. queues prio = [] then switch_to_idle_thread else guarded_switch_to (hd (max_non_empty_queue queues))
od) (do curdom <- if 1 < numDomains then curDomain else return 0;
l1 <- getReadyQueuesL1Bitmap curdom;
if l1 \<noteq> 0 then do prio <- getHighestPrio curdom;
queue <- getQueue curdom prio;
runnable <- isRunnable (head queue);
haskell_assert runnable [];
global.switchToThread (head queue)
od else global.switchToIdleThread
od) proof (prove)
goal (1 subgoal):
 1. corres dc (invs and valid_sched) all_invs_but_ct_idle_or_in_cur_domain' (do d <- gets cur_domain;
queues <- gets (\<lambda>s. ready_queues s d);
if \<forall>prio. queues prio = [] then switch_to_idle_thread else guarded_switch_to (hd (max_non_empty_queue queues))
od) (do curdom <- if 1 < numDomains then curDomain else return 0;
l1 <- getReadyQueuesL1Bitmap curdom;
if \<not> l1 \<noteq> 0 then global.switchToIdleThread else do prio <- getHighestPrio curdom;
queue <- getQueue curdom prio;
runnable <- isRunnable (head queue);
haskell_assert runnable [];
global.switchToThread (head queue)
od
od) proof (prove)
goal (1 subgoal):
 1. corres dc (invs and valid_sched) all_invs_but_ct_idle_or_in_cur_domain' (do d <- gets cur_domain;
queues <- gets (\<lambda>s. ready_queues s d);
if \<forall>prio. queues prio = [] then switch_to_idle_thread else guarded_switch_to (hd (max_non_empty_queue queues))
od) (do curdom <- if 1 < numDomains then curDomain else return 0;
l1 <- getReadyQueuesL1Bitmap curdom;
if \<not> l1 \<noteq> 0 then global.switchToIdleThread else do prio <- getHighestPrio curdom;
queue <- getQueue curdom prio;
runnable <- isRunnable (head queue);
haskell_assert runnable [];
global.switchToThread (head queue)
od
od) proof (prove)
goal (3 subgoals):
 1. corres dc ?Q ?Q' (do d <- gets cur_domain;
queues <- gets (\<lambda>s. ready_queues s d);
if \<forall>prio. queues prio = [] then switch_to_idle_thread else guarded_switch_to (hd (max_non_empty_queue queues))
od) (do curdom <- if 1 < numDomains then curDomain else return 0;
l1 <- getReadyQueuesL1Bitmap curdom;
if \<not> l1 \<noteq> 0 then global.switchToIdleThread else do prio <- getHighestPrio curdom;
queue <- getQueue curdom prio;
runnable <- isRunnable (head queue);
haskell_assert runnable [];
global.switchToThread (head queue)
od
od)
 2. \<And>s. (invs and valid_sched) s \<Longrightarrow> ?Q s
 3. \<And>s. all_invs_but_ct_idle_or_in_cur_domain' s \<Longrightarrow> ?Q' s proof (prove)
goal (5 subgoals):
 1. \<And>d curdom. d = curdom \<Longrightarrow> corres dc (?R4 d) (?R'4 curdom) (do queues <- gets (\<lambda>s. ready_queues s d);
if \<forall>prio. queues prio = [] then switch_to_idle_thread else guarded_switch_to (hd (max_non_empty_queue queues))
od) (do l1 <- getReadyQueuesL1Bitmap curdom;
if \<not> l1 \<noteq> 0 then global.switchToIdleThread else do prio <- getHighestPrio curdom;
queue <- getQueue curdom prio;
runnable <- isRunnable (head queue);
haskell_assert runnable [];
global.switchToThread (head queue)
od
od)
 2. \<lbrace>?Q4\<rbrace> gets cur_domain \<lbrace>?R4\<rbrace>
 3. \<lbrace>?Q'4\<rbrace> if 1 < numDomains then curDomain else return 0 \<lbrace>?R'4\<rbrace>
 4. \<And>s. (invs and valid_sched) s \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 5. \<And>s. all_invs_but_ct_idle_or_in_cur_domain' s \<Longrightarrow> ((\<lambda>s. ksCurDomain s \<le> maxDomain) and ?Q'4) s proof (prove)
goal (5 subgoals):
 1. \<And>d. corres dc (?R4 d) (?R'4 d) (do queues <- gets (\<lambda>s. ready_queues s d);
if \<forall>prio. queues prio = [] then switch_to_idle_thread else guarded_switch_to (hd (max_non_empty_queue queues))
od) (do l1 <- getReadyQueuesL1Bitmap d;
if l1 = 0 then global.switchToIdleThread else do prio <- getHighestPrio d;
queue <- getQueue d prio;
runnable <- isRunnable (head queue);
haskell_assert runnable [];
global.switchToThread (head queue)
od
od)
 2. \<lbrace>?Q4\<rbrace> gets cur_domain \<lbrace>?R4\<rbrace>
 3. \<lbrace>?Q'4\<rbrace> if 1 < numDomains then curDomain else return 0 \<lbrace>?R'4\<rbrace>
 4. \<And>s. (invs and valid_sched) s \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 5. \<And>s. all_invs_but_ct_idle_or_in_cur_domain' s \<Longrightarrow> ((\<lambda>s. ksCurDomain s \<le> maxDomain) and ?Q'4) s proof (prove)
goal (7 subgoals):
 1. \<And>d queues l1. (l1 = 0) = (\<forall>p. queues p = []) \<Longrightarrow> corres dc (?R10 d queues) (?R'10 d l1) (if \<forall>prio. queues prio = [] then switch_to_idle_thread else guarded_switch_to (hd (max_non_empty_queue queues))) (if l1 = 0 then global.switchToIdleThread else do prio <- getHighestPrio d;
queue <- getQueue d prio;
runnable <- isRunnable (head queue);
haskell_assert runnable [];
global.switchToThread (head queue)
od)
 2. \<And>d. \<lbrace>?Q10 d\<rbrace> gets (\<lambda>s. ready_queues s d) \<lbrace>?R10 d\<rbrace>
 3. \<And>d. \<lbrace>?Q'10 d\<rbrace> getReadyQueuesL1Bitmap d \<lbrace>?R'10 d\<rbrace>
 4. \<lbrace>?Q4\<rbrace> gets cur_domain \<lbrace>\<lambda>d. (\<lambda>_. True) and ?Q10 d\<rbrace>
 5. \<lbrace>?Q'4\<rbrace> if 1 < numDomains then curDomain else return 0 \<lbrace>\<lambda>d. Invariants_H.valid_queues and ?Q'10 d\<rbrace>
 6. \<And>s. (invs and valid_sched) s \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 7. \<And>s. all_invs_but_ct_idle_or_in_cur_domain' s \<Longrightarrow> ((\<lambda>s. ksCurDomain s \<le> maxDomain) and ?Q'4) s proof (prove)
goal (8 subgoals):
 1. \<And>d queues l1. \<forall>p. queues p = [] \<Longrightarrow> corres dc (?P17 d queues) (?P'19 d l1) switch_to_idle_thread global.switchToIdleThread
 2. \<And>d queues l1. l1 \<noteq> 0 \<Longrightarrow> corres dc (?Q18 d queues) (?Q'20 d l1) (guarded_switch_to (hd (max_non_empty_queue queues))) (do prio <- getHighestPrio d;
queue <- getQueue d prio;
runnable <- isRunnable (head queue);
haskell_assert runnable [];
global.switchToThread (head queue)
od)
 3. \<And>d. \<lbrace>?Q10 d\<rbrace> gets (\<lambda>s. ready_queues s d) \<lbrace>\<lambda>queues. if \<forall>p. queues p = [] then ?P17 d queues else ?Q18 d queues\<rbrace>
 4. \<And>d. \<lbrace>?Q'10 d\<rbrace> getReadyQueuesL1Bitmap d \<lbrace>\<lambda>l1. if l1 = 0 then ?P'19 d l1 else ?Q'20 d l1\<rbrace>
 5. \<lbrace>?Q4\<rbrace> gets cur_domain \<lbrace>\<lambda>d. (\<lambda>_. True) and ?Q10 d\<rbrace>
 6. \<lbrace>?Q'4\<rbrace> if 1 < numDomains then curDomain else return 0 \<lbrace>\<lambda>d. Invariants_H.valid_queues and ?Q'10 d\<rbrace>
 7. \<And>s. (invs and valid_sched) s \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 8. \<And>s. all_invs_but_ct_idle_or_in_cur_domain' s \<Longrightarrow> ((\<lambda>s. ksCurDomain s \<le> maxDomain) and ?Q'4) s proof (prove)
goal (7 subgoals):
 1. \<And>d queues l1. l1 \<noteq> 0 \<Longrightarrow> corres dc (?Q18 d queues) (?Q'20 d l1) (guarded_switch_to (hd (max_non_empty_queue queues))) (do prio <- getHighestPrio d;
queue <- getQueue d prio;
runnable <- isRunnable (head queue);
haskell_assert runnable [];
global.switchToThread (head queue)
od)
 2. \<And>d. \<lbrace>?Q10 d\<rbrace> gets (\<lambda>s. ready_queues s d) \<lbrace>\<lambda>queues. if \<forall>p. queues p = [] then invs else ?Q18 d queues\<rbrace>
 3. \<And>d. \<lbrace>?Q'10 d\<rbrace> getReadyQueuesL1Bitmap d \<lbrace>\<lambda>l1. if l1 = 0 then all_invs_but_ct_idle_or_in_cur_domain' else ?Q'20 d l1\<rbrace>
 4. \<lbrace>?Q4\<rbrace> gets cur_domain \<lbrace>\<lambda>d. (\<lambda>_. True) and ?Q10 d\<rbrace>
 5. \<lbrace>?Q'4\<rbrace> if 1 < numDomains then curDomain else return 0 \<lbrace>\<lambda>d. Invariants_H.valid_queues and ?Q'10 d\<rbrace>
 6. \<And>s. (invs and valid_sched) s \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 7. \<And>s. all_invs_but_ct_idle_or_in_cur_domain' s \<Longrightarrow> ((\<lambda>s. ksCurDomain s \<le> maxDomain) and ?Q'4) s proof (prove)
goal (10 subgoals):
 1. \<And>d queues l1 prio. l1 \<noteq> 0 \<Longrightarrow> corres dc (?Q18 d queues) (?Q'23 d queues l1 prio) (guarded_switch_to (hd (max_non_empty_queue queues))) (do queue <- getQueue d prio;
runnable <- isRunnable (head queue);
haskell_assert runnable [];
global.switchToThread (head queue)
od)
 2. \<And>d queues l1. l1 \<noteq> 0 \<Longrightarrow> \<lbrace>?Q'20 d l1\<rbrace> getHighestPrio d \<lbrace>?Q'23 d queues l1\<rbrace>
 3. \<And>d queues l1 s. \<lbrakk>l1 \<noteq> 0; ?Q'20 d l1 s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> getHighestPrio d \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<And>d queues l1. \<lbrakk>l1 \<noteq> 0; True\<rbrakk> \<Longrightarrow> no_fail (?Q'20 d l1) (getHighestPrio d)
 5. \<And>d. \<lbrace>?Q10 d\<rbrace> gets (\<lambda>s. ready_queues s d) \<lbrace>\<lambda>queues. if \<forall>p. queues p = [] then invs else ?Q18 d queues\<rbrace>
 6. \<And>d. \<lbrace>?Q'10 d\<rbrace> getReadyQueuesL1Bitmap d \<lbrace>\<lambda>l1. if l1 = 0 then all_invs_but_ct_idle_or_in_cur_domain' else ?Q'20 d l1\<rbrace>
 7. \<lbrace>?Q4\<rbrace> gets cur_domain \<lbrace>\<lambda>d. (\<lambda>_. True) and ?Q10 d\<rbrace>
 8. \<lbrace>?Q'4\<rbrace> if 1 < numDomains then curDomain else return 0 \<lbrace>\<lambda>d. Invariants_H.valid_queues and ?Q'10 d\<rbrace>
 9. \<And>s. (invs and valid_sched) s \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 10. \<And>s. all_invs_but_ct_idle_or_in_cur_domain' s \<Longrightarrow> ((\<lambda>s. ksCurDomain s \<le> maxDomain) and ?Q'4) s proof (prove)
goal (13 subgoals):
 1. \<And>d queues l1 prio queue. l1 \<noteq> 0 \<Longrightarrow> corres dc (?Q18 d queues) (?Q'28 d queues l1 prio queue) (guarded_switch_to (hd (max_non_empty_queue queues))) (do runnable <- isRunnable (head queue);
haskell_assert runnable [];
global.switchToThread (head queue)
od)
 2. \<And>d queues l1 prio. l1 \<noteq> 0 \<Longrightarrow> \<lbrace>?Q'23 d queues l1 prio\<rbrace> getQueue d prio \<lbrace>?Q'28 d queues l1 prio\<rbrace>
 3. \<And>d queues l1 prio s. \<lbrakk>l1 \<noteq> 0; ?Q'23 d queues l1 prio s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> getQueue d prio \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<And>d queues l1 prio. \<lbrakk>l1 \<noteq> 0; True\<rbrakk> \<Longrightarrow> no_fail (?Q'23 d queues l1 prio) (getQueue d prio)
 5. \<And>d queues l1. l1 \<noteq> 0 \<Longrightarrow> \<lbrace>?Q'20 d l1\<rbrace> getHighestPrio d \<lbrace>?Q'23 d queues l1\<rbrace>
 6. \<And>d queues l1 s. \<lbrakk>l1 \<noteq> 0; ?Q'20 d l1 s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> getHighestPrio d \<lbrace>\<lambda>r. (=) s\<rbrace>
 7. \<And>d queues l1. \<lbrakk>l1 \<noteq> 0; True\<rbrakk> \<Longrightarrow> no_fail (?Q'20 d l1) (getHighestPrio d)
 8. \<And>d. \<lbrace>?Q10 d\<rbrace> gets (\<lambda>s. ready_queues s d) \<lbrace>\<lambda>queues. if \<forall>p. queues p = [] then invs else ?Q18 d queues\<rbrace>
 9. \<And>d. \<lbrace>?Q'10 d\<rbrace> getReadyQueuesL1Bitmap d \<lbrace>\<lambda>l1. if l1 = 0 then all_invs_but_ct_idle_or_in_cur_domain' else ?Q'20 d l1\<rbrace>
 10. \<lbrace>?Q4\<rbrace> gets cur_domain \<lbrace>\<lambda>d. (\<lambda>_. True) and ?Q10 d\<rbrace>
A total of 13 subgoals... proof (prove)
goal (14 subgoals):
 1. \<And>d queues l1 prio queue s s'. \<lbrakk>l1 \<noteq> 0; (s, s') \<in> state_relation; (invs and valid_sched) s \<and> queues = ready_queues s (cur_domain s) \<and> st_tcb_at runnable (hd (max_non_empty_queue queues)) s; (all_invs_but_ct_idle_or_in_cur_domain' s' \<and> st_tcb_at' runnable' (hd queue) s') \<and> l1 = ksReadyQueuesL1Bitmap s' (ksCurDomain s') \<and> l1 \<noteq> 0 \<and> queue = ksReadyQueues s' (ksCurDomain s', lookupBitmapPriority (ksCurDomain s') s')\<rbrakk> \<Longrightarrow> hd queue = hd (max_non_empty_queue queues)
 2. \<And>d queues l1 prio queue. \<lbrakk>l1 \<noteq> 0; hd queue = hd (max_non_empty_queue queues)\<rbrakk> \<Longrightarrow> corres dc (\<lambda>s. (invs and valid_sched) s \<and> queues = ready_queues s (cur_domain s) \<and> st_tcb_at runnable (hd (max_non_empty_queue queues)) s) (\<lambda>s. (all_invs_but_ct_idle_or_in_cur_domain' s \<and> st_tcb_at' runnable' (hd queue) s) \<and> l1 = ksReadyQueuesL1Bitmap s (ksCurDomain s) \<and> l1 \<noteq> 0 \<and> queue = ksReadyQueues s (ksCurDomain s, lookupBitmapPriority (ksCurDomain s) s)) (guarded_switch_to (hd (max_non_empty_queue queues))) (do runnable <- isRunnable (head queue);
haskell_assert runnable [];
global.switchToThread (head queue)
od)
 3. \<And>d queues l1 prio. l1 \<noteq> 0 \<Longrightarrow> \<lbrace>?Q'23 d queues l1 prio\<rbrace> getQueue d prio \<lbrace>\<lambda>queue s. (all_invs_but_ct_idle_or_in_cur_domain' s \<and> st_tcb_at' runnable' (hd queue) s) \<and> l1 = ksReadyQueuesL1Bitmap s (ksCurDomain s) \<and> l1 \<noteq> 0 \<and> queue = ksReadyQueues s (ksCurDomain s, lookupBitmapPriority (ksCurDomain s) s)\<rbrace>
 4. \<And>d queues l1 prio s. \<lbrakk>l1 \<noteq> 0; ?Q'23 d queues l1 prio s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> getQueue d prio \<lbrace>\<lambda>r. (=) s\<rbrace>
 5. \<And>d queues l1 prio. \<lbrakk>l1 \<noteq> 0; True\<rbrakk> \<Longrightarrow> no_fail (?Q'23 d queues l1 prio) (getQueue d prio)
 6. \<And>d queues l1. l1 \<noteq> 0 \<Longrightarrow> \<lbrace>?Q'20 d l1\<rbrace> getHighestPrio d \<lbrace>?Q'23 d queues l1\<rbrace>
 7. \<And>d queues l1 s. \<lbrakk>l1 \<noteq> 0; ?Q'20 d l1 s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> getHighestPrio d \<lbrace>\<lambda>r. (=) s\<rbrace>
 8. \<And>d queues l1. \<lbrakk>l1 \<noteq> 0; True\<rbrakk> \<Longrightarrow> no_fail (?Q'20 d l1) (getHighestPrio d)
 9. \<And>d. \<lbrace>?Q10 d\<rbrace> gets (\<lambda>s. ready_queues s d) \<lbrace>\<lambda>queues. if \<forall>p. queues p = [] then invs else (\<lambda>s. (invs and valid_sched) s \<and> queues = ready_queues s (cur_domain s) \<and> st_tcb_at runnable (hd (max_non_empty_queue queues)) s)\<rbrace>
 10. \<And>d. \<lbrace>?Q'10 d\<rbrace> getReadyQueuesL1Bitmap d \<lbrace>\<lambda>l1. if l1 = 0 then all_invs_but_ct_idle_or_in_cur_domain' else ?Q'20 d l1\<rbrace>
A total of 14 subgoals... proof (prove)
goal (13 subgoals):
 1. \<And>d queues l1 prio queue. \<lbrakk>l1 \<noteq> 0; hd queue = hd (max_non_empty_queue queues)\<rbrakk> \<Longrightarrow> corres dc (\<lambda>s. (invs and valid_sched) s \<and> queues = ready_queues s (cur_domain s) \<and> st_tcb_at runnable (hd (max_non_empty_queue queues)) s) (\<lambda>s. (all_invs_but_ct_idle_or_in_cur_domain' s \<and> st_tcb_at' runnable' (hd queue) s) \<and> l1 = ksReadyQueuesL1Bitmap s (ksCurDomain s) \<and> l1 \<noteq> 0 \<and> queue = ksReadyQueues s (ksCurDomain s, lookupBitmapPriority (ksCurDomain s) s)) (guarded_switch_to (hd (max_non_empty_queue queues))) (do runnable <- isRunnable (head queue);
haskell_assert runnable [];
global.switchToThread (head queue)
od)
 2. \<And>d queues l1 prio. l1 \<noteq> 0 \<Longrightarrow> \<lbrace>?Q'23 d queues l1 prio\<rbrace> getQueue d prio \<lbrace>\<lambda>queue s. (all_invs_but_ct_idle_or_in_cur_domain' s \<and> st_tcb_at' runnable' (hd queue) s) \<and> l1 = ksReadyQueuesL1Bitmap s (ksCurDomain s) \<and> l1 \<noteq> 0 \<and> queue = ksReadyQueues s (ksCurDomain s, lookupBitmapPriority (ksCurDomain s) s)\<rbrace>
 3. \<And>d queues l1 prio s. \<lbrakk>l1 \<noteq> 0; ?Q'23 d queues l1 prio s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> getQueue d prio \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<And>d queues l1 prio. \<lbrakk>l1 \<noteq> 0; True\<rbrakk> \<Longrightarrow> no_fail (?Q'23 d queues l1 prio) (getQueue d prio)
 5. \<And>d queues l1. l1 \<noteq> 0 \<Longrightarrow> \<lbrace>?Q'20 d l1\<rbrace> getHighestPrio d \<lbrace>?Q'23 d queues l1\<rbrace>
 6. \<And>d queues l1 s. \<lbrakk>l1 \<noteq> 0; ?Q'20 d l1 s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> getHighestPrio d \<lbrace>\<lambda>r. (=) s\<rbrace>
 7. \<And>d queues l1. \<lbrakk>l1 \<noteq> 0; True\<rbrakk> \<Longrightarrow> no_fail (?Q'20 d l1) (getHighestPrio d)
 8. \<And>d. \<lbrace>?Q10 d\<rbrace> gets (\<lambda>s. ready_queues s d) \<lbrace>\<lambda>queues. if \<forall>p. queues p = [] then invs else (\<lambda>s. (invs and valid_sched) s \<and> queues = ready_queues s (cur_domain s) \<and> st_tcb_at runnable (hd (max_non_empty_queue queues)) s)\<rbrace>
 9. \<And>d. \<lbrace>?Q'10 d\<rbrace> getReadyQueuesL1Bitmap d \<lbrace>\<lambda>l1. if l1 = 0 then all_invs_but_ct_idle_or_in_cur_domain' else ?Q'20 d l1\<rbrace>
 10. \<lbrace>?Q4\<rbrace> gets cur_domain \<lbrace>\<lambda>d. (\<lambda>_. True) and ?Q10 d\<rbrace>
A total of 13 subgoals... proof (prove)
goal (13 subgoals):
 1. \<And>queues l1 queue. \<lbrakk>l1 \<noteq> 0; hd queue = hd (max_non_empty_queue queues)\<rbrakk> \<Longrightarrow> corres dc (\<lambda>s. invs s \<and> valid_sched s \<and> queues = ready_queues s (cur_domain s) \<and> st_tcb_at runnable (hd (max_non_empty_queue queues)) s) (\<lambda>s. all_invs_but_ct_idle_or_in_cur_domain' s \<and> st_tcb_at' runnable' (hd (max_non_empty_queue queues)) s \<and> l1 = ksReadyQueuesL1Bitmap s (ksCurDomain s) \<and> queue = ksReadyQueues s (ksCurDomain s, lookupBitmapPriority (ksCurDomain s) s)) (guarded_switch_to (hd (max_non_empty_queue queues))) (do runnable <- isRunnable (hd (max_non_empty_queue queues));
y <- assert runnable;
global.switchToThread (hd (max_non_empty_queue queues))
od)
 2. \<And>d queues l1 prio. l1 \<noteq> 0 \<Longrightarrow> \<lbrace>?Q'23 d queues l1 prio\<rbrace> getQueue d prio \<lbrace>\<lambda>queue s. (all_invs_but_ct_idle_or_in_cur_domain' s \<and> st_tcb_at' runnable' (hd queue) s) \<and> l1 = ksReadyQueuesL1Bitmap s (ksCurDomain s) \<and> l1 \<noteq> 0 \<and> queue = ksReadyQueues s (ksCurDomain s, lookupBitmapPriority (ksCurDomain s) s)\<rbrace>
 3. \<And>d queues l1 prio s. \<lbrakk>l1 \<noteq> 0; ?Q'23 d queues l1 prio s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> getQueue d prio \<lbrace>\<lambda>r. (=) s\<rbrace>
 4. \<And>d queues l1 prio. \<lbrakk>l1 \<noteq> 0; True\<rbrakk> \<Longrightarrow> no_fail (?Q'23 d queues l1 prio) (getQueue d prio)
 5. \<And>d queues l1. l1 \<noteq> 0 \<Longrightarrow> \<lbrace>?Q'20 d l1\<rbrace> getHighestPrio d \<lbrace>?Q'23 d queues l1\<rbrace>
 6. \<And>d queues l1 s. \<lbrakk>l1 \<noteq> 0; ?Q'20 d l1 s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> getHighestPrio d \<lbrace>\<lambda>r. (=) s\<rbrace>
 7. \<And>d queues l1. \<lbrakk>l1 \<noteq> 0; True\<rbrakk> \<Longrightarrow> no_fail (?Q'20 d l1) (getHighestPrio d)
 8. \<And>d. \<lbrace>?Q10 d\<rbrace> gets (\<lambda>s. ready_queues s d) \<lbrace>\<lambda>queues. if \<forall>p. queues p = [] then invs else (\<lambda>s. (invs and valid_sched) s \<and> queues = ready_queues s (cur_domain s) \<and> st_tcb_at runnable (hd (max_non_empty_queue queues)) s)\<rbrace>
 9. \<And>d. \<lbrace>?Q'10 d\<rbrace> getReadyQueuesL1Bitmap d \<lbrace>\<lambda>l1. if l1 = 0 then all_invs_but_ct_idle_or_in_cur_domain' else ?Q'20 d l1\<rbrace>
 10. \<lbrace>?Q4\<rbrace> gets cur_domain \<lbrace>\<lambda>d. (\<lambda>_. True) and ?Q10 d\<rbrace>
A total of 13 subgoals... proof (prove)
goal (15 subgoals):
 1. \<And>queues l1 queue. \<lbrakk>l1 \<noteq> 0; hd queue = hd (max_non_empty_queue queues)\<rbrakk> \<Longrightarrow> corres dc (?Q49 queues l1 queue) (?Q'49 queues l1 queue) (guarded_switch_to (hd (max_non_empty_queue queues))) (do runnable <- isRunnable (hd (max_non_empty_queue queues));
y <- assert runnable;
global.switchToThread (hd (max_non_empty_queue queues))
od)
 2. \<And>queues l1 queue s. \<lbrakk>l1 \<noteq> 0; hd queue = hd (max_non_empty_queue queues); invs s \<and> valid_sched s \<and> queues = ready_queues s (cur_domain s) \<and> st_tcb_at runnable (hd (max_non_empty_queue queues)) s\<rbrakk> \<Longrightarrow> ?Q49 queues l1 queue s
 3. \<And>queues l1 queue s. \<lbrakk>l1 \<noteq> 0; hd queue = hd (max_non_empty_queue queues); all_invs_but_ct_idle_or_in_cur_domain' s \<and> st_tcb_at' runnable' (hd (max_non_empty_queue queues)) s \<and> l1 = ksReadyQueuesL1Bitmap s (ksCurDomain s) \<and> queue = ksReadyQueues s (ksCurDomain s, lookupBitmapPriority (ksCurDomain s) s)\<rbrakk> \<Longrightarrow> ?Q'49 queues l1 queue s
 4. \<And>d queues l1 prio. l1 \<noteq> 0 \<Longrightarrow> \<lbrace>?Q'23 d queues l1 prio\<rbrace> getQueue d prio \<lbrace>\<lambda>queue s. (all_invs_but_ct_idle_or_in_cur_domain' s \<and> st_tcb_at' runnable' (hd queue) s) \<and> l1 = ksReadyQueuesL1Bitmap s (ksCurDomain s) \<and> l1 \<noteq> 0 \<and> queue = ksReadyQueues s (ksCurDomain s, lookupBitmapPriority (ksCurDomain s) s)\<rbrace>
 5. \<And>d queues l1 prio s. \<lbrakk>l1 \<noteq> 0; ?Q'23 d queues l1 prio s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> getQueue d prio \<lbrace>\<lambda>r. (=) s\<rbrace>
 6. \<And>d queues l1 prio. \<lbrakk>l1 \<noteq> 0; True\<rbrakk> \<Longrightarrow> no_fail (?Q'23 d queues l1 prio) (getQueue d prio)
 7. \<And>d queues l1. l1 \<noteq> 0 \<Longrightarrow> \<lbrace>?Q'20 d l1\<rbrace> getHighestPrio d \<lbrace>?Q'23 d queues l1\<rbrace>
 8. \<And>d queues l1 s. \<lbrakk>l1 \<noteq> 0; ?Q'20 d l1 s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> getHighestPrio d \<lbrace>\<lambda>r. (=) s\<rbrace>
 9. \<And>d queues l1. \<lbrakk>l1 \<noteq> 0; True\<rbrakk> \<Longrightarrow> no_fail (?Q'20 d l1) (getHighestPrio d)
 10. \<And>d. \<lbrace>?Q10 d\<rbrace> gets (\<lambda>s. ready_queues s d) \<lbrace>\<lambda>queues. if \<forall>p. queues p = [] then invs else (\<lambda>s. (invs and valid_sched) s \<and> queues = ready_queues s (cur_domain s) \<and> st_tcb_at runnable (hd (max_non_empty_queue queues)) s)\<rbrace>
A total of 15 subgoals... proof (prove)
goal (14 subgoals):
 1. \<And>queues l1 queue s. \<lbrakk>l1 \<noteq> 0; hd queue = hd (max_non_empty_queue queues); invs s \<and> valid_sched s \<and> queues = ready_queues s (cur_domain s) \<and> st_tcb_at runnable (hd (max_non_empty_queue queues)) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and st_tcb_at runnable (hd (max_non_empty_queue queues)) and invs and valid_sched) s
 2. \<And>queues l1 queue s. \<lbrakk>l1 \<noteq> 0; hd queue = hd (max_non_empty_queue queues); all_invs_but_ct_idle_or_in_cur_domain' s \<and> st_tcb_at' runnable' (hd (max_non_empty_queue queues)) s \<and> l1 = ksReadyQueuesL1Bitmap s (ksCurDomain s) \<and> queue = ksReadyQueues s (ksCurDomain s, lookupBitmapPriority (ksCurDomain s) s)\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and st_tcb_at' runnable' (hd (max_non_empty_queue queues)) and all_invs_but_ct_idle_or_in_cur_domain') s
 3. \<And>d queues l1 prio. l1 \<noteq> 0 \<Longrightarrow> \<lbrace>?Q'23 d queues l1 prio\<rbrace> getQueue d prio \<lbrace>\<lambda>queue s. (all_invs_but_ct_idle_or_in_cur_domain' s \<and> st_tcb_at' runnable' (hd queue) s) \<and> l1 = ksReadyQueuesL1Bitmap s (ksCurDomain s) \<and> l1 \<noteq> 0 \<and> queue = ksReadyQueues s (ksCurDomain s, lookupBitmapPriority (ksCurDomain s) s)\<rbrace>
 4. \<And>d queues l1 prio s. \<lbrakk>l1 \<noteq> 0; ?Q'23 d queues l1 prio s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> getQueue d prio \<lbrace>\<lambda>r. (=) s\<rbrace>
 5. \<And>d queues l1 prio. \<lbrakk>l1 \<noteq> 0; True\<rbrakk> \<Longrightarrow> no_fail (?Q'23 d queues l1 prio) (getQueue d prio)
 6. \<And>d queues l1. l1 \<noteq> 0 \<Longrightarrow> \<lbrace>?Q'20 d l1\<rbrace> getHighestPrio d \<lbrace>?Q'23 d queues l1\<rbrace>
 7. \<And>d queues l1 s. \<lbrakk>l1 \<noteq> 0; ?Q'20 d l1 s\<rbrakk> \<Longrightarrow> \<lbrace>(=) s\<rbrace> getHighestPrio d \<lbrace>\<lambda>r. (=) s\<rbrace>
 8. \<And>d queues l1. \<lbrakk>l1 \<noteq> 0; True\<rbrakk> \<Longrightarrow> no_fail (?Q'20 d l1) (getHighestPrio d)
 9. \<And>d. \<lbrace>?Q10 d\<rbrace> gets (\<lambda>s. ready_queues s d) \<lbrace>\<lambda>queues. if \<forall>p. queues p = [] then invs else (\<lambda>s. (invs and valid_sched) s \<and> queues = ready_queues s (cur_domain s) \<and> st_tcb_at runnable (hd (max_non_empty_queue queues)) s)\<rbrace>
 10. \<And>d. \<lbrace>?Q'10 d\<rbrace> getReadyQueuesL1Bitmap d \<lbrace>\<lambda>l1. if l1 = 0 then all_invs_but_ct_idle_or_in_cur_domain' else ?Q'20 d l1\<rbrace>
A total of 14 subgoals... proof (prove)
goal (5 subgoals):
 1. \<And>d. \<lbrace>?Q'10 d\<rbrace> getReadyQueuesL1Bitmap d \<lbrace>\<lambda>l1. if l1 = 0 then all_invs_but_ct_idle_or_in_cur_domain' else (\<lambda>s. all_invs_but_ct_idle_or_in_cur_domain' s \<and> st_tcb_at' runnable' (hd (ksReadyQueues s (d, lookupBitmapPriority d s))) s \<and> l1 = ksReadyQueuesL1Bitmap s (ksCurDomain s) \<and> ksReadyQueues s (d, lookupBitmapPriority d s) = ksReadyQueues s (ksCurDomain s, lookupBitmapPriority (ksCurDomain s) s))\<rbrace>
 2. \<lbrace>?Q4\<rbrace> gets cur_domain \<lbrace>\<lambda>d. (\<lambda>_. True) and (\<lambda>s. (if \<forall>p. ready_queues s d p = [] then invs else (\<lambda>sa. (invs and valid_sched) sa \<and> ready_queues s d = ready_queues sa (cur_domain sa) \<and> st_tcb_at runnable (hd (max_non_empty_queue (ready_queues s d))) sa)) s)\<rbrace>
 3. \<lbrace>?Q'4\<rbrace> if 1 < numDomains then curDomain else return 0 \<lbrace>\<lambda>d. Invariants_H.valid_queues and ?Q'10 d\<rbrace>
 4. \<And>s. (invs and valid_sched) s \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 5. \<And>s. all_invs_but_ct_idle_or_in_cur_domain' s \<Longrightarrow> ((\<lambda>s. ksCurDomain s \<le> maxDomain) and ?Q'4) s proof (prove)
goal (5 subgoals):
 1. \<And>d. \<lbrace>?Q'10 d\<rbrace> getReadyQueuesL1Bitmap d \<lbrace>\<lambda>l1 x. (l1 = 0 \<longrightarrow> all_invs_but_ct_idle_or_in_cur_domain' x) \<and> (l1 \<noteq> 0 \<longrightarrow> all_invs_but_ct_idle_or_in_cur_domain' x \<and> st_tcb_at' runnable' (hd (ksReadyQueues x (d, lookupBitmapPriority d x))) x \<and> l1 = ksReadyQueuesL1Bitmap x (ksCurDomain x) \<and> ksReadyQueues x (d, lookupBitmapPriority d x) = ksReadyQueues x (ksCurDomain x, lookupBitmapPriority (ksCurDomain x) x))\<rbrace>
 2. \<lbrace>?Q4\<rbrace> gets cur_domain \<lbrace>\<lambda>d. (\<lambda>_. True) and (\<lambda>s. (if \<forall>p. ready_queues s d p = [] then invs else (\<lambda>sa. (invs and valid_sched) sa \<and> ready_queues s d = ready_queues sa (cur_domain sa) \<and> st_tcb_at runnable (hd (max_non_empty_queue (ready_queues s d))) sa)) s)\<rbrace>
 3. \<lbrace>?Q'4\<rbrace> if 1 < numDomains then curDomain else return 0 \<lbrace>\<lambda>d. Invariants_H.valid_queues and ?Q'10 d\<rbrace>
 4. \<And>s. (invs and valid_sched) s \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 5. \<And>s. all_invs_but_ct_idle_or_in_cur_domain' s \<Longrightarrow> ((\<lambda>s. ksCurDomain s \<le> maxDomain) and ?Q'4) s proof (prove)
goal (4 subgoals):
 1. \<lbrace>?Q4\<rbrace> gets cur_domain \<lbrace>\<lambda>d. (\<lambda>_. True) and (\<lambda>s. (if \<forall>p. ready_queues s d p = [] then invs else (\<lambda>sa. (invs and valid_sched) sa \<and> ready_queues s d = ready_queues sa (cur_domain sa) \<and> st_tcb_at runnable (hd (max_non_empty_queue (ready_queues s d))) sa)) s)\<rbrace>
 2. \<lbrace>?Q'4\<rbrace> if 1 < numDomains then curDomain else return 0 \<lbrace>\<lambda>d. Invariants_H.valid_queues and (\<lambda>s. (ksReadyQueuesL1Bitmap s d \<noteq> 0 \<or> all_invs_but_ct_idle_or_in_cur_domain' s) \<and> (\<not> ksReadyQueuesL1Bitmap s d \<noteq> 0 \<or> all_invs_but_ct_idle_or_in_cur_domain' s \<and> st_tcb_at' runnable' (hd (ksReadyQueues s (d, lookupBitmapPriority d s))) s \<and> ksReadyQueuesL1Bitmap s d = ksReadyQueuesL1Bitmap s (ksCurDomain s) \<and> ksReadyQueues s (d, lookupBitmapPriority d s) = ksReadyQueues s (ksCurDomain s, lookupBitmapPriority (ksCurDomain s) s)))\<rbrace>
 3. \<And>s. (invs and valid_sched) s \<Longrightarrow> ((\<lambda>_. True) and ?Q4) s
 4. \<And>s. all_invs_but_ct_idle_or_in_cur_domain' s \<Longrightarrow> ((\<lambda>s. ksCurDomain s \<le> maxDomain) and ?Q'4) s proof (prove)
goal (3 subgoals):
 1. \<And>x. ?Q118 x \<Longrightarrow> ksCurDomain x \<le> maxDomain
 2. \<And>s. (invs and valid_sched) s \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. ((\<lambda>_. True) and (\<lambda>sa. (if \<forall>p. ready_queues sa (cur_domain s) p = [] then invs else (\<lambda>sb. (invs and valid_sched) sb \<and> ready_queues sa (cur_domain s) = ready_queues sb (cur_domain sb) \<and> st_tcb_at runnable (hd (max_non_empty_queue (ready_queues sa (cur_domain s)))) sb)) sa)) s)) s
 3. \<And>s. all_invs_but_ct_idle_or_in_cur_domain' s \<Longrightarrow> ((\<lambda>s. ksCurDomain s \<le> maxDomain) and (\<lambda>s. (Invariants_H.valid_queues s \<and> (ksReadyQueuesL1Bitmap s (ksCurDomain s) = 0 \<longrightarrow> all_invs_but_ct_idle_or_in_cur_domain' s) \<and> (ksReadyQueuesL1Bitmap s (ksCurDomain s) = 0 \<or> all_invs_but_ct_idle_or_in_cur_domain' s \<and> st_tcb_at' runnable' (hd (ksReadyQueues s (ksCurDomain s, lookupBitmapPriority (ksCurDomain s) s))) s \<and> ksReadyQueuesL1Bitmap s (ksCurDomain s) = ksReadyQueuesL1Bitmap s (ksCurDomain s) \<and> ksReadyQueues s (ksCurDomain s, lookupBitmapPriority (ksCurDomain s) s) = ksReadyQueues s (ksCurDomain s, lookupBitmapPriority (ksCurDomain s) s))) \<and> ?Q118 s)) s proof (prove)
goal (2 subgoals):
 1. \<And>s. (invs and valid_sched) s \<Longrightarrow> ((\<lambda>_. True) and (\<lambda>s. ((\<lambda>_. True) and (\<lambda>sa. (if \<forall>p. ready_queues sa (cur_domain s) p = [] then invs else (\<lambda>sb. (invs and valid_sched) sb \<and> ready_queues sa (cur_domain s) = ready_queues sb (cur_domain sb) \<and> st_tcb_at runnable (hd (max_non_empty_queue (ready_queues sa (cur_domain s)))) sb)) sa)) s)) s
 2. \<And>s. all_invs_but_ct_idle_or_in_cur_domain' s \<Longrightarrow> ((\<lambda>s. ksCurDomain s \<le> maxDomain) and (\<lambda>s. (Invariants_H.valid_queues s \<and> (ksReadyQueuesL1Bitmap s (ksCurDomain s) = 0 \<longrightarrow> all_invs_but_ct_idle_or_in_cur_domain' s) \<and> (ksReadyQueuesL1Bitmap s (ksCurDomain s) = 0 \<or> all_invs_but_ct_idle_or_in_cur_domain' s \<and> st_tcb_at' runnable' (hd (ksReadyQueues s (ksCurDomain s, lookupBitmapPriority (ksCurDomain s) s))) s \<and> ksReadyQueuesL1Bitmap s (ksCurDomain s) = ksReadyQueuesL1Bitmap s (ksCurDomain s) \<and> ksReadyQueues s (ksCurDomain s, lookupBitmapPriority (ksCurDomain s) s) = ksReadyQueues s (ksCurDomain s, lookupBitmapPriority (ksCurDomain s) s))) \<and> ksCurDomain s \<le> maxDomain)) s proof (prove)
goal (2 subgoals):
 1. \<And>s p. \<lbrakk>invs s; valid_etcbs s; \<forall>d p. (\<forall>t\<in>set (ready_queues s d p). is_etcb_at t s \<and> etcb_at (\<lambda>t. tcb_priority t = p \<and> tcb_domain t = d) t s \<and> st_tcb_at runnable t s) \<and> distinct (ready_queues s d p); ct_not_in_q s; valid_sched_action s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; ready_queues s (cur_domain s) p \<noteq> []\<rbrakk> \<Longrightarrow> st_tcb_at runnable (hd (ready_queues s (cur_domain s) (Max {prio. ready_queues s (cur_domain s) prio \<noteq> []}))) s
 2. \<And>s. all_invs_but_ct_idle_or_in_cur_domain' s \<Longrightarrow> ((\<lambda>s. ksCurDomain s \<le> maxDomain) and (\<lambda>s. (Invariants_H.valid_queues s \<and> (ksReadyQueuesL1Bitmap s (ksCurDomain s) = 0 \<longrightarrow> all_invs_but_ct_idle_or_in_cur_domain' s) \<and> (ksReadyQueuesL1Bitmap s (ksCurDomain s) = 0 \<or> all_invs_but_ct_idle_or_in_cur_domain' s \<and> st_tcb_at' runnable' (hd (ksReadyQueues s (ksCurDomain s, lookupBitmapPriority (ksCurDomain s) s))) s \<and> ksReadyQueuesL1Bitmap s (ksCurDomain s) = ksReadyQueuesL1Bitmap s (ksCurDomain s) \<and> ksReadyQueues s (ksCurDomain s, lookupBitmapPriority (ksCurDomain s) s) = ksReadyQueues s (ksCurDomain s, lookupBitmapPriority (ksCurDomain s) s))) \<and> ksCurDomain s \<le> maxDomain)) s proof (prove)
goal (2 subgoals):
 1. \<And>s p. \<lbrakk>invs s; valid_etcbs s; ct_not_in_q s; valid_sched_action s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; ready_queues s (cur_domain s) p \<noteq> []; \<forall>p. (\<forall>t\<in>set (ready_queues s (cur_domain s) p). is_etcb_at t s \<and> etcb_at (\<lambda>t. tcb_priority t = p \<and> tcb_domain t = cur_domain s) t s \<and> st_tcb_at runnable t s) \<and> distinct (ready_queues s (cur_domain s) p)\<rbrakk> \<Longrightarrow> st_tcb_at runnable (hd (ready_queues s (cur_domain s) (Max {prio. ready_queues s (cur_domain s) prio \<noteq> []}))) s
 2. \<And>s. all_invs_but_ct_idle_or_in_cur_domain' s \<Longrightarrow> ((\<lambda>s. ksCurDomain s \<le> maxDomain) and (\<lambda>s. (Invariants_H.valid_queues s \<and> (ksReadyQueuesL1Bitmap s (ksCurDomain s) = 0 \<longrightarrow> all_invs_but_ct_idle_or_in_cur_domain' s) \<and> (ksReadyQueuesL1Bitmap s (ksCurDomain s) = 0 \<or> all_invs_but_ct_idle_or_in_cur_domain' s \<and> st_tcb_at' runnable' (hd (ksReadyQueues s (ksCurDomain s, lookupBitmapPriority (ksCurDomain s) s))) s \<and> ksReadyQueuesL1Bitmap s (ksCurDomain s) = ksReadyQueuesL1Bitmap s (ksCurDomain s) \<and> ksReadyQueues s (ksCurDomain s, lookupBitmapPriority (ksCurDomain s) s) = ksReadyQueues s (ksCurDomain s, lookupBitmapPriority (ksCurDomain s) s))) \<and> ksCurDomain s \<le> maxDomain)) s proof (prove)
goal (2 subgoals):
 1. \<And>s p. \<lbrakk>invs s; valid_etcbs s; ct_not_in_q s; valid_sched_action s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; ready_queues s (cur_domain s) p \<noteq> []; (\<forall>t\<in>set (ready_queues s (cur_domain s) (Max {prio. ready_queues s (cur_domain s) prio \<noteq> []})). is_etcb_at t s \<and> etcb_at (\<lambda>t. tcb_priority t = Max {prio. ready_queues s (cur_domain s) prio \<noteq> []} \<and> tcb_domain t = cur_domain s) t s \<and> st_tcb_at runnable t s) \<and> distinct (ready_queues s (cur_domain s) (Max {prio. ready_queues s (cur_domain s) prio \<noteq> []}))\<rbrakk> \<Longrightarrow> st_tcb_at runnable (hd (ready_queues s (cur_domain s) (Max {prio. ready_queues s (cur_domain s) prio \<noteq> []}))) s
 2. \<And>s. all_invs_but_ct_idle_or_in_cur_domain' s \<Longrightarrow> ((\<lambda>s. ksCurDomain s \<le> maxDomain) and (\<lambda>s. (Invariants_H.valid_queues s \<and> (ksReadyQueuesL1Bitmap s (ksCurDomain s) = 0 \<longrightarrow> all_invs_but_ct_idle_or_in_cur_domain' s) \<and> (ksReadyQueuesL1Bitmap s (ksCurDomain s) = 0 \<or> all_invs_but_ct_idle_or_in_cur_domain' s \<and> st_tcb_at' runnable' (hd (ksReadyQueues s (ksCurDomain s, lookupBitmapPriority (ksCurDomain s) s))) s \<and> ksReadyQueuesL1Bitmap s (ksCurDomain s) = ksReadyQueuesL1Bitmap s (ksCurDomain s) \<and> ksReadyQueues s (ksCurDomain s, lookupBitmapPriority (ksCurDomain s) s) = ksReadyQueues s (ksCurDomain s, lookupBitmapPriority (ksCurDomain s) s))) \<and> ksCurDomain s \<le> maxDomain)) s proof (prove)
goal (3 subgoals):
 1. \<And>s p. \<lbrakk>invs s; valid_etcbs s; ct_not_in_q s; valid_sched_action s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; ready_queues s (cur_domain s) p \<noteq> []; (\<forall>t\<in>set (ready_queues s (cur_domain s) (Max {prio. ready_queues s (cur_domain s) prio \<noteq> []})). is_etcb_at t s \<and> etcb_at (\<lambda>t. tcb_priority t = Max {prio. ready_queues s (cur_domain s) prio \<noteq> []} \<and> tcb_domain t = cur_domain s) t s \<and> st_tcb_at runnable t s) \<and> distinct (ready_queues s (cur_domain s) (Max {prio. ready_queues s (cur_domain s) prio \<noteq> []})); ready_queues s (cur_domain s) (Max {prio. ready_queues s (cur_domain s) prio \<noteq> []}) = []\<rbrakk> \<Longrightarrow> st_tcb_at runnable (hd (ready_queues s (cur_domain s) (Max {prio. ready_queues s (cur_domain s) prio \<noteq> []}))) s
 2. \<And>s p a list. \<lbrakk>invs s; valid_etcbs s; ct_not_in_q s; valid_sched_action s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; ready_queues s (cur_domain s) p \<noteq> []; (\<forall>t\<in>set (ready_queues s (cur_domain s) (Max {prio. ready_queues s (cur_domain s) prio \<noteq> []})). is_etcb_at t s \<and> etcb_at (\<lambda>t. tcb_priority t = Max {prio. ready_queues s (cur_domain s) prio \<noteq> []} \<and> tcb_domain t = cur_domain s) t s \<and> st_tcb_at runnable t s) \<and> distinct (ready_queues s (cur_domain s) (Max {prio. ready_queues s (cur_domain s) prio \<noteq> []})); ready_queues s (cur_domain s) (Max {prio. ready_queues s (cur_domain s) prio \<noteq> []}) = a # list\<rbrakk> \<Longrightarrow> st_tcb_at runnable (hd (ready_queues s (cur_domain s) (Max {prio. ready_queues s (cur_domain s) prio \<noteq> []}))) s
 3. \<And>s. all_invs_but_ct_idle_or_in_cur_domain' s \<Longrightarrow> ((\<lambda>s. ksCurDomain s \<le> maxDomain) and (\<lambda>s. (Invariants_H.valid_queues s \<and> (ksReadyQueuesL1Bitmap s (ksCurDomain s) = 0 \<longrightarrow> all_invs_but_ct_idle_or_in_cur_domain' s) \<and> (ksReadyQueuesL1Bitmap s (ksCurDomain s) = 0 \<or> all_invs_but_ct_idle_or_in_cur_domain' s \<and> st_tcb_at' runnable' (hd (ksReadyQueues s (ksCurDomain s, lookupBitmapPriority (ksCurDomain s) s))) s \<and> ksReadyQueuesL1Bitmap s (ksCurDomain s) = ksReadyQueuesL1Bitmap s (ksCurDomain s) \<and> ksReadyQueues s (ksCurDomain s, lookupBitmapPriority (ksCurDomain s) s) = ksReadyQueues s (ksCurDomain s, lookupBitmapPriority (ksCurDomain s) s))) \<and> ksCurDomain s \<le> maxDomain)) s proof (prove)
goal (3 subgoals):
 1. \<And>s p. \<lbrakk>invs s; valid_etcbs s; ct_not_in_q s; valid_sched_action s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; ready_queues s (cur_domain s) p \<noteq> []; ready_queues s (cur_domain s) (Max {prio. ready_queues s (cur_domain s) prio \<noteq> []}) = []\<rbrakk> \<Longrightarrow> st_tcb_at runnable (hd []) s
 2. \<And>s p a list. \<lbrakk>invs s; valid_etcbs s; ct_not_in_q s; valid_sched_action s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; ready_queues s (cur_domain s) p \<noteq> []; (\<forall>t\<in>set (ready_queues s (cur_domain s) (Max {prio. ready_queues s (cur_domain s) prio \<noteq> []})). is_etcb_at t s \<and> etcb_at (\<lambda>t. tcb_priority t = Max {prio. ready_queues s (cur_domain s) prio \<noteq> []} \<and> tcb_domain t = cur_domain s) t s \<and> st_tcb_at runnable t s) \<and> distinct (ready_queues s (cur_domain s) (Max {prio. ready_queues s (cur_domain s) prio \<noteq> []})); ready_queues s (cur_domain s) (Max {prio. ready_queues s (cur_domain s) prio \<noteq> []}) = a # list\<rbrakk> \<Longrightarrow> st_tcb_at runnable (hd (ready_queues s (cur_domain s) (Max {prio. ready_queues s (cur_domain s) prio \<noteq> []}))) s
 3. \<And>s. all_invs_but_ct_idle_or_in_cur_domain' s \<Longrightarrow> ((\<lambda>s. ksCurDomain s \<le> maxDomain) and (\<lambda>s. (Invariants_H.valid_queues s \<and> (ksReadyQueuesL1Bitmap s (ksCurDomain s) = 0 \<longrightarrow> all_invs_but_ct_idle_or_in_cur_domain' s) \<and> (ksReadyQueuesL1Bitmap s (ksCurDomain s) = 0 \<or> all_invs_but_ct_idle_or_in_cur_domain' s \<and> st_tcb_at' runnable' (hd (ksReadyQueues s (ksCurDomain s, lookupBitmapPriority (ksCurDomain s) s))) s \<and> ksReadyQueuesL1Bitmap s (ksCurDomain s) = ksReadyQueuesL1Bitmap s (ksCurDomain s) \<and> ksReadyQueues s (ksCurDomain s, lookupBitmapPriority (ksCurDomain s) s) = ksReadyQueues s (ksCurDomain s, lookupBitmapPriority (ksCurDomain s) s))) \<and> ksCurDomain s \<le> maxDomain)) s proof (prove)
goal (4 subgoals):
 1. \<And>s p. \<lbrakk>invs s; valid_etcbs s; ct_not_in_q s; valid_sched_action s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; ready_queues s (cur_domain s) p \<noteq> []; ready_queues s (cur_domain s) (Max {prio. ready_queues s (cur_domain s) prio \<noteq> []}) = []; ready_queues s (cur_domain s) (Max {prio. ready_queues s (cur_domain s) prio \<noteq> []}) \<noteq> []\<rbrakk> \<Longrightarrow> st_tcb_at runnable (hd []) s
 2. \<And>s p. \<lbrakk>invs s; valid_etcbs s; ct_not_in_q s; valid_sched_action s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; ready_queues s (cur_domain s) p \<noteq> []; ready_queues s (cur_domain s) (Max {prio. ready_queues s (cur_domain s) prio \<noteq> []}) = []\<rbrakk> \<Longrightarrow> ready_queues s (cur_domain s) (Max {prio. ready_queues s (cur_domain s) prio \<noteq> []}) \<noteq> []
 3. \<And>s p a list. \<lbrakk>invs s; valid_etcbs s; ct_not_in_q s; valid_sched_action s; ct_in_cur_domain s; valid_blocked s; valid_idle_etcb s; ready_queues s (cur_domain s) p \<noteq> []; (\<forall>t\<in>set (ready_queues s (cur_domain s) (Max {prio. ready_queues s (cur_domain s) prio \<noteq> []})). is_etcb_at t s \<and> etcb_at (\<lambda>t. tcb_priority t = Max {prio. ready_queues s (cur_domain s) prio \<noteq> []} \<and> tcb_domain t = cur_domain s) t s \<and> st_tcb_at runnable t s) \<and> distinct (ready_queues s (cur_domain s) (Max {prio. ready_queues s (cur_domain s) prio \<noteq> []})); ready_queues s (cur_domain s) (Max {prio. ready_queues s (cur_domain s) prio \<noteq> []}) = a # list\<rbrakk> \<Longrightarrow> st_tcb_at runnable (hd (ready_queues s (cur_domain s) (Max {prio. ready_queues s (cur_domain s) prio \<noteq> []}))) s
 4. \<And>s. all_invs_but_ct_idle_or_in_cur_domain' s \<Longrightarrow> ((\<lambda>s. ksCurDomain s \<le> maxDomain) and (\<lambda>s. (Invariants_H.valid_queues s \<and> (ksReadyQueuesL1Bitmap s (ksCurDomain s) = 0 \<longrightarrow> all_invs_but_ct_idle_or_in_cur_domain' s) \<and> (ksReadyQueuesL1Bitmap s (ksCurDomain s) = 0 \<or> all_invs_but_ct_idle_or_in_cur_domain' s \<and> st_tcb_at' runnable' (hd (ksReadyQueues s (ksCurDomain s, lookupBitmapPriority (ksCurDomain s) s))) s \<and> ksReadyQueuesL1Bitmap s (ksCurDomain s) = ksReadyQueuesL1Bitmap s (ksCurDomain s) \<and> ksReadyQueues s (ksCurDomain s, lookupBitmapPriority (ksCurDomain s) s) = ksReadyQueues s (ksCurDomain s, lookupBitmapPriority (ksCurDomain s) s))) \<and> ksCurDomain s \<le> maxDomain)) s proof (prove)
goal (1 subgoal):
 1. \<And>s. all_invs_but_ct_idle_or_in_cur_domain' s \<Longrightarrow> ((\<lambda>s. ksCurDomain s \<le> maxDomain) and (\<lambda>s. (Invariants_H.valid_queues s \<and> (ksReadyQueuesL1Bitmap s (ksCurDomain s) = 0 \<longrightarrow> all_invs_but_ct_idle_or_in_cur_domain' s) \<and> (ksReadyQueuesL1Bitmap s (ksCurDomain s) = 0 \<or> all_invs_but_ct_idle_or_in_cur_domain' s \<and> st_tcb_at' runnable' (hd (ksReadyQueues s (ksCurDomain s, lookupBitmapPriority (ksCurDomain s) s))) s \<and> ksReadyQueuesL1Bitmap s (ksCurDomain s) = ksReadyQueuesL1Bitmap s (ksCurDomain s) \<and> ksReadyQueues s (ksCurDomain s, lookupBitmapPriority (ksCurDomain s) s) = ksReadyQueues s (ksCurDomain s, lookupBitmapPriority (ksCurDomain s) s))) \<and> ksCurDomain s \<le> maxDomain)) s proof (prove)
goal (1 subgoal):
 1. \<And>s. all_invs_but_ct_idle_or_in_cur_domain' s \<Longrightarrow> Invariants_H.valid_queues s \<and> (ksReadyQueuesL1Bitmap s (ksCurDomain s) = 0 \<or> st_tcb_at' runnable' (hd (ksReadyQueues s (ksCurDomain s, lookupBitmapPriority (ksCurDomain s) s))) s) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>Invariants_H.valid_queues s; \<not> st_tcb_at' runnable' (hd (ksReadyQueues s (ksCurDomain s, lookupBitmapPriority (ksCurDomain s) s))) s\<rbrakk> \<Longrightarrow> ksReadyQueuesL1Bitmap s (ksCurDomain s) = 0 proof (prove)
goal:
No subgoals! proof (state)
this:
corres dc (invs and valid_sched) all_invs_but_ct_idle_or_in_cur_domain' choose_thread chooseThread

goal:
No subgoals!