theory Schedule_R

lemma chooseThread_invs_no_cicd'_posts: (* generic version *)
  "\<lbrace> invs_no_cicd' \<rbrace> chooseThread
   \<lbrace>\<lambda>rv s. obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s \<and>
           ct_in_state' activatable' s \<and>
           (ksCurThread s = ksIdleThread s \<or> tcb_in_cur_domain' (ksCurThread s) s) \<rbrace>"
    (is "\<lbrace>_\<rbrace> _ \<lbrace>\<lambda>_. ?POST\<rbrace>") proof - note switchToThread_invs[wp del] note switchToThread_invs_no_cicd'[wp del] note switchToThread_lookupBitmapPriority_wp[wp] note assert_wp[wp del] note if_split[split del] 

  (* if we only have one domain, we are in it *)
   have one_domain_case:
    "\<And>s. \<lbrakk> invs_no_cicd' s; numDomains \<le> 1 \<rbrakk> \<Longrightarrow> ksCurDomain s = 0" by (simp add: all_invs_but_ct_idle_or_in_cur_domain'_def maxDomain_def) show ?thesis unfolding chooseThread_def Let_def curDomain_def apply (simp only: return_bind, simp) apply (rule hoare_seq_ext[where B="\<lambda>rv s. invs_no_cicd' s \<and> rv = ksCurDomain s"]) apply (rule_tac B="\<lambda>rv s. invs_no_cicd' s \<and> curdom = ksCurDomain s \<and>
                               rv = ksReadyQueuesL1Bitmap s curdom" in hoare_seq_ext) apply (rename_tac l1) apply (case_tac "l1 = 0") 
       (* switch to idle thread *)
        apply simp apply (rule hoare_pre) apply (wp (once) switchToIdleThread_ct_not_queued_no_cicd') apply (wp (once)) apply ((wp hoare_disjI1 switchToIdleThread_curr_is_idle)+)[1] apply simp 
      (* we have a thread to switch to *)
       apply (clarsimp simp: bitmap_fun_defs) apply (wp assert_inv switchToThread_ct_not_queued_2 assert_inv hoare_disjI2
                switchToThread_tcb_in_cur_domain') apply clarsimp apply (clarsimp dest!: invs_no_cicd'_queues
                      simp: valid_queues_def lookupBitmapPriority_def[symmetric]) apply (drule (3) lookupBitmapPriority_obj_at') apply normalise_obj_at' apply (fastforce simp: tcb_in_cur_domain'_def inQ_def elim: obj_at'_weaken) apply (wpsimp simp: bitmap_fun_defs curDomain_def one_domain_case)+ done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>all_invs_but_ct_idle_or_in_cur_domain'\<rbrace> chooseThread \<lbrace>\<lambda>rv s. obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s \<and> ct_in_state' activatable' s \<and> (ksCurThread s = ksIdleThread s \<or> tcb_in_cur_domain' (ksCurThread s) s)\<rbrace> proof (state)
goal (1 subgoal):
 1. \<lbrace>all_invs_but_ct_idle_or_in_cur_domain'\<rbrace> chooseThread \<lbrace>\<lambda>rv s. obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s \<and> ct_in_state' activatable' s \<and> (ksCurThread s = ksIdleThread s \<or> tcb_in_cur_domain' (ksCurThread s) s)\<rbrace> proof (state)
this:
\<lbrace>invs' and st_tcb_at' runnable' ?t and tcb_in_cur_domain' ?t\<rbrace> global.switchToThread ?t \<lbrace>\<lambda>rv. invs'\<rbrace>

goal (1 subgoal):
 1. \<lbrace>all_invs_but_ct_idle_or_in_cur_domain'\<rbrace> chooseThread \<lbrace>\<lambda>rv s. obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s \<and> ct_in_state' activatable' s \<and> (ksCurThread s = ksIdleThread s \<or> tcb_in_cur_domain' (ksCurThread s) s)\<rbrace> proof (state)
this:
\<lbrace>all_invs_but_ct_idle_or_in_cur_domain' and st_tcb_at' runnable' ?t and tcb_in_cur_domain' ?t\<rbrace> global.switchToThread ?t \<lbrace>\<lambda>rv. invs'\<rbrace>

goal (1 subgoal):
 1. \<lbrace>all_invs_but_ct_idle_or_in_cur_domain'\<rbrace> chooseThread \<lbrace>\<lambda>rv s. obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s \<and> ct_in_state' activatable' s \<and> (ksCurThread s = ksIdleThread s \<or> tcb_in_cur_domain' (ksCurThread s) s)\<rbrace> proof (state)
this:
\<lbrace>\<lambda>s. all_invs_but_ct_idle_or_in_cur_domain' s \<and> bitmapQ (ksCurDomain s) (lookupBitmapPriority (ksCurDomain s) s) s \<and> ?t = hd (ksReadyQueues s (ksCurDomain s, lookupBitmapPriority (ksCurDomain s) s))\<rbrace> global.switchToThread ?t \<lbrace>\<lambda>rv. invs'\<rbrace>

goal (1 subgoal):
 1. \<lbrace>all_invs_but_ct_idle_or_in_cur_domain'\<rbrace> chooseThread \<lbrace>\<lambda>rv s. obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s \<and> ct_in_state' activatable' s \<and> (ksCurThread s = ksIdleThread s \<or> tcb_in_cur_domain' (ksCurThread s) s)\<rbrace> proof (state)
this:
\<lbrace>\<lambda>s. ?P \<longrightarrow> ?Q () s\<rbrace> assert ?P \<lbrace>?Q\<rbrace>

goal (1 subgoal):
 1. \<lbrace>all_invs_but_ct_idle_or_in_cur_domain'\<rbrace> chooseThread \<lbrace>\<lambda>rv s. obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s \<and> ct_in_state' activatable' s \<and> (ksCurThread s = ksIdleThread s \<or> tcb_in_cur_domain' (ksCurThread s) s)\<rbrace> proof (state)
this:
?P (if ?Q then ?x else ?y) = ((?Q \<longrightarrow> ?P ?x) \<and> (\<not> ?Q \<longrightarrow> ?P ?y))

goal (1 subgoal):
 1. \<lbrace>all_invs_but_ct_idle_or_in_cur_domain'\<rbrace> chooseThread \<lbrace>\<lambda>rv s. obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s \<and> ct_in_state' activatable' s \<and> (ksCurThread s = ksIdleThread s \<or> tcb_in_cur_domain' (ksCurThread s) s)\<rbrace> proof (state)
this:
?P (if ?Q then ?x else ?y) = ((?Q \<longrightarrow> ?P ?x) \<and> (\<not> ?Q \<longrightarrow> ?P ?y))

goal (1 subgoal):
 1. \<lbrace>all_invs_but_ct_idle_or_in_cur_domain'\<rbrace> chooseThread \<lbrace>\<lambda>rv s. obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s \<and> ct_in_state' activatable' s \<and> (ksCurThread s = ksIdleThread s \<or> tcb_in_cur_domain' (ksCurThread s) s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>all_invs_but_ct_idle_or_in_cur_domain' s; numDomains \<le> 1\<rbrakk> \<Longrightarrow> ksCurDomain s = 0 proof (state)
this:
\<lbrakk>all_invs_but_ct_idle_or_in_cur_domain' ?s; numDomains \<le> 1\<rbrakk> \<Longrightarrow> ksCurDomain ?s = 0

goal (1 subgoal):
 1. \<lbrace>all_invs_but_ct_idle_or_in_cur_domain'\<rbrace> chooseThread \<lbrace>\<lambda>rv s. obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s \<and> ct_in_state' activatable' s \<and> (ksCurThread s = ksIdleThread s \<or> tcb_in_cur_domain' (ksCurThread s) s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>all_invs_but_ct_idle_or_in_cur_domain'\<rbrace> chooseThread \<lbrace>\<lambda>rv s. obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s \<and> ct_in_state' activatable' s \<and> (ksCurThread s = ksIdleThread s \<or> tcb_in_cur_domain' (ksCurThread s) s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>all_invs_but_ct_idle_or_in_cur_domain'\<rbrace> do curdom <- if 1 < numDomains then gets ksCurDomain 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 \<lbrace>\<lambda>rv s. obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s \<and> ct_in_state' activatable' s \<and> (ksCurThread s = ksIdleThread s \<or> tcb_in_cur_domain' (ksCurThread s) s)\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>all_invs_but_ct_idle_or_in_cur_domain'\<rbrace> do curdom <- if Suc 0 < numDomains then gets ksCurDomain 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 \<lbrace>\<lambda>rv s. obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s \<and> ct_in_state' activatable' s \<and> (ksCurThread s = ksIdleThread s \<or> tcb_in_cur_domain' (ksCurThread s) s)\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>curdom. \<lbrace>\<lambda>s. all_invs_but_ct_idle_or_in_cur_domain' s \<and> curdom = ksCurDomain s\<rbrace> do 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 \<lbrace>\<lambda>rv s. obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s \<and> ct_in_state' activatable' s \<and> (ksCurThread s = ksIdleThread s \<or> tcb_in_cur_domain' (ksCurThread s) s)\<rbrace>
 2. \<lbrace>all_invs_but_ct_idle_or_in_cur_domain'\<rbrace> if Suc 0 < numDomains then gets ksCurDomain else return 0 \<lbrace>\<lambda>rv s. all_invs_but_ct_idle_or_in_cur_domain' s \<and> rv = ksCurDomain s\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>curdom x. \<lbrace>\<lambda>s. all_invs_but_ct_idle_or_in_cur_domain' s \<and> curdom = ksCurDomain s \<and> x = ksReadyQueuesL1Bitmap s curdom\<rbrace> if x \<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 \<lbrace>\<lambda>rv s. obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s \<and> ct_in_state' activatable' s \<and> (ksCurThread s = ksIdleThread s \<or> tcb_in_cur_domain' (ksCurThread s) s)\<rbrace>
 2. \<And>curdom. \<lbrace>\<lambda>s. all_invs_but_ct_idle_or_in_cur_domain' s \<and> curdom = ksCurDomain s\<rbrace> getReadyQueuesL1Bitmap curdom \<lbrace>\<lambda>rv s. all_invs_but_ct_idle_or_in_cur_domain' s \<and> curdom = ksCurDomain s \<and> rv = ksReadyQueuesL1Bitmap s curdom\<rbrace>
 3. \<lbrace>all_invs_but_ct_idle_or_in_cur_domain'\<rbrace> if Suc 0 < numDomains then gets ksCurDomain else return 0 \<lbrace>\<lambda>rv s. all_invs_but_ct_idle_or_in_cur_domain' s \<and> rv = ksCurDomain s\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>curdom l1. \<lbrace>\<lambda>s. all_invs_but_ct_idle_or_in_cur_domain' s \<and> curdom = ksCurDomain s \<and> l1 = ksReadyQueuesL1Bitmap s curdom\<rbrace> 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 \<lbrace>\<lambda>rv s. obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s \<and> ct_in_state' activatable' s \<and> (ksCurThread s = ksIdleThread s \<or> tcb_in_cur_domain' (ksCurThread s) s)\<rbrace>
 2. \<And>curdom. \<lbrace>\<lambda>s. all_invs_but_ct_idle_or_in_cur_domain' s \<and> curdom = ksCurDomain s\<rbrace> getReadyQueuesL1Bitmap curdom \<lbrace>\<lambda>rv s. all_invs_but_ct_idle_or_in_cur_domain' s \<and> curdom = ksCurDomain s \<and> rv = ksReadyQueuesL1Bitmap s curdom\<rbrace>
 3. \<lbrace>all_invs_but_ct_idle_or_in_cur_domain'\<rbrace> if Suc 0 < numDomains then gets ksCurDomain else return 0 \<lbrace>\<lambda>rv s. all_invs_but_ct_idle_or_in_cur_domain' s \<and> rv = ksCurDomain s\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>curdom l1. l1 = 0 \<Longrightarrow> \<lbrace>\<lambda>s. all_invs_but_ct_idle_or_in_cur_domain' s \<and> curdom = ksCurDomain s \<and> l1 = ksReadyQueuesL1Bitmap s curdom\<rbrace> 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 \<lbrace>\<lambda>rv s. obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s \<and> ct_in_state' activatable' s \<and> (ksCurThread s = ksIdleThread s \<or> tcb_in_cur_domain' (ksCurThread s) s)\<rbrace>
 2. \<And>curdom l1. l1 \<noteq> 0 \<Longrightarrow> \<lbrace>\<lambda>s. all_invs_but_ct_idle_or_in_cur_domain' s \<and> curdom = ksCurDomain s \<and> l1 = ksReadyQueuesL1Bitmap s curdom\<rbrace> 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 \<lbrace>\<lambda>rv s. obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s \<and> ct_in_state' activatable' s \<and> (ksCurThread s = ksIdleThread s \<or> tcb_in_cur_domain' (ksCurThread s) s)\<rbrace>
 3. \<And>curdom. \<lbrace>\<lambda>s. all_invs_but_ct_idle_or_in_cur_domain' s \<and> curdom = ksCurDomain s\<rbrace> getReadyQueuesL1Bitmap curdom \<lbrace>\<lambda>rv s. all_invs_but_ct_idle_or_in_cur_domain' s \<and> curdom = ksCurDomain s \<and> rv = ksReadyQueuesL1Bitmap s curdom\<rbrace>
 4. \<lbrace>all_invs_but_ct_idle_or_in_cur_domain'\<rbrace> if Suc 0 < numDomains then gets ksCurDomain else return 0 \<lbrace>\<lambda>rv s. all_invs_but_ct_idle_or_in_cur_domain' s \<and> rv = ksCurDomain s\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>curdom l1. l1 = 0 \<Longrightarrow> \<lbrace>\<lambda>s. all_invs_but_ct_idle_or_in_cur_domain' s \<and> curdom = ksCurDomain s \<and> l1 = ksReadyQueuesL1Bitmap s curdom\<rbrace> 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 \<lbrace>\<lambda>rv s. obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s \<and> ct_in_state' activatable' s \<and> (ksCurThread s = ksIdleThread s \<or> tcb_in_cur_domain' (ksCurThread s) s)\<rbrace>
 2. \<And>curdom l1. l1 \<noteq> 0 \<Longrightarrow> \<lbrace>\<lambda>s. all_invs_but_ct_idle_or_in_cur_domain' s \<and> curdom = ksCurDomain s \<and> l1 = ksReadyQueuesL1Bitmap s curdom\<rbrace> 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 \<lbrace>\<lambda>rv s. obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s \<and> ct_in_state' activatable' s \<and> (ksCurThread s = ksIdleThread s \<or> tcb_in_cur_domain' (ksCurThread s) s)\<rbrace>
 3. \<And>curdom. \<lbrace>\<lambda>s. all_invs_but_ct_idle_or_in_cur_domain' s \<and> curdom = ksCurDomain s\<rbrace> getReadyQueuesL1Bitmap curdom \<lbrace>\<lambda>rv s. all_invs_but_ct_idle_or_in_cur_domain' s \<and> curdom = ksCurDomain s \<and> rv = ksReadyQueuesL1Bitmap s curdom\<rbrace>
 4. \<lbrace>all_invs_but_ct_idle_or_in_cur_domain'\<rbrace> if Suc 0 < numDomains then gets ksCurDomain else return 0 \<lbrace>\<lambda>rv s. all_invs_but_ct_idle_or_in_cur_domain' s \<and> rv = ksCurDomain s\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>curdom. \<lbrace>\<lambda>s. all_invs_but_ct_idle_or_in_cur_domain' s \<and> curdom = ksCurDomain s \<and> ksReadyQueuesL1Bitmap s curdom = 0\<rbrace> global.switchToIdleThread \<lbrace>\<lambda>rv s. obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s \<and> ct_in_state' activatable' s \<and> (ksCurThread s = ksIdleThread s \<or> tcb_in_cur_domain' (ksCurThread s) s)\<rbrace>
 2. \<And>curdom l1. l1 \<noteq> 0 \<Longrightarrow> \<lbrace>\<lambda>s. all_invs_but_ct_idle_or_in_cur_domain' s \<and> curdom = ksCurDomain s \<and> l1 = ksReadyQueuesL1Bitmap s curdom\<rbrace> 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 \<lbrace>\<lambda>rv s. obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s \<and> ct_in_state' activatable' s \<and> (ksCurThread s = ksIdleThread s \<or> tcb_in_cur_domain' (ksCurThread s) s)\<rbrace>
 3. \<And>curdom. \<lbrace>\<lambda>s. all_invs_but_ct_idle_or_in_cur_domain' s \<and> curdom = ksCurDomain s\<rbrace> getReadyQueuesL1Bitmap curdom \<lbrace>\<lambda>rv s. all_invs_but_ct_idle_or_in_cur_domain' s \<and> curdom = ksCurDomain s \<and> rv = ksReadyQueuesL1Bitmap s curdom\<rbrace>
 4. \<lbrace>all_invs_but_ct_idle_or_in_cur_domain'\<rbrace> if Suc 0 < numDomains then gets ksCurDomain else return 0 \<lbrace>\<lambda>rv s. all_invs_but_ct_idle_or_in_cur_domain' s \<and> rv = ksCurDomain s\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>curdom. \<lbrace>?Q7 curdom\<rbrace> global.switchToIdleThread \<lbrace>\<lambda>rv s. obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s \<and> ct_in_state' activatable' s \<and> (ksCurThread s = ksIdleThread s \<or> tcb_in_cur_domain' (ksCurThread s) s)\<rbrace>
 2. \<And>curdom s. all_invs_but_ct_idle_or_in_cur_domain' s \<and> curdom = ksCurDomain s \<and> ksReadyQueuesL1Bitmap s curdom = 0 \<Longrightarrow> ?Q7 curdom s
 3. \<And>curdom l1. l1 \<noteq> 0 \<Longrightarrow> \<lbrace>\<lambda>s. all_invs_but_ct_idle_or_in_cur_domain' s \<and> curdom = ksCurDomain s \<and> l1 = ksReadyQueuesL1Bitmap s curdom\<rbrace> 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 \<lbrace>\<lambda>rv s. obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s \<and> ct_in_state' activatable' s \<and> (ksCurThread s = ksIdleThread s \<or> tcb_in_cur_domain' (ksCurThread s) s)\<rbrace>
 4. \<And>curdom. \<lbrace>\<lambda>s. all_invs_but_ct_idle_or_in_cur_domain' s \<and> curdom = ksCurDomain s\<rbrace> getReadyQueuesL1Bitmap curdom \<lbrace>\<lambda>rv s. all_invs_but_ct_idle_or_in_cur_domain' s \<and> curdom = ksCurDomain s \<and> rv = ksReadyQueuesL1Bitmap s curdom\<rbrace>
 5. \<lbrace>all_invs_but_ct_idle_or_in_cur_domain'\<rbrace> if Suc 0 < numDomains then gets ksCurDomain else return 0 \<lbrace>\<lambda>rv s. all_invs_but_ct_idle_or_in_cur_domain' s \<and> rv = ksCurDomain s\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>curdom. \<lbrace>?P'11 curdom\<rbrace> global.switchToIdleThread \<lbrace>\<lambda>rv s. ct_in_state' activatable' s \<and> (ksCurThread s = ksIdleThread s \<or> tcb_in_cur_domain' (ksCurThread s) s)\<rbrace>
 2. \<And>curdom s. all_invs_but_ct_idle_or_in_cur_domain' s \<and> curdom = ksCurDomain s \<and> ksReadyQueuesL1Bitmap s curdom = 0 \<Longrightarrow> all_invs_but_ct_idle_or_in_cur_domain' s \<and> ?P'11 curdom s
 3. \<And>curdom l1. l1 \<noteq> 0 \<Longrightarrow> \<lbrace>\<lambda>s. all_invs_but_ct_idle_or_in_cur_domain' s \<and> curdom = ksCurDomain s \<and> l1 = ksReadyQueuesL1Bitmap s curdom\<rbrace> 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 \<lbrace>\<lambda>rv s. obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s \<and> ct_in_state' activatable' s \<and> (ksCurThread s = ksIdleThread s \<or> tcb_in_cur_domain' (ksCurThread s) s)\<rbrace>
 4. \<And>curdom. \<lbrace>\<lambda>s. all_invs_but_ct_idle_or_in_cur_domain' s \<and> curdom = ksCurDomain s\<rbrace> getReadyQueuesL1Bitmap curdom \<lbrace>\<lambda>rv s. all_invs_but_ct_idle_or_in_cur_domain' s \<and> curdom = ksCurDomain s \<and> rv = ksReadyQueuesL1Bitmap s curdom\<rbrace>
 5. \<lbrace>all_invs_but_ct_idle_or_in_cur_domain'\<rbrace> if Suc 0 < numDomains then gets ksCurDomain else return 0 \<lbrace>\<lambda>rv s. all_invs_but_ct_idle_or_in_cur_domain' s \<and> rv = ksCurDomain s\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>curdom. \<lbrace>?P'14 curdom\<rbrace> global.switchToIdleThread \<lbrace>\<lambda>rv s. ksCurThread s = ksIdleThread s \<or> tcb_in_cur_domain' (ksCurThread s) s\<rbrace>
 2. \<And>curdom s. all_invs_but_ct_idle_or_in_cur_domain' s \<and> curdom = ksCurDomain s \<and> ksReadyQueuesL1Bitmap s curdom = 0 \<Longrightarrow> all_invs_but_ct_idle_or_in_cur_domain' s \<and> all_invs_but_ct_idle_or_in_cur_domain' s \<and> ?P'14 curdom s
 3. \<And>curdom l1. l1 \<noteq> 0 \<Longrightarrow> \<lbrace>\<lambda>s. all_invs_but_ct_idle_or_in_cur_domain' s \<and> curdom = ksCurDomain s \<and> l1 = ksReadyQueuesL1Bitmap s curdom\<rbrace> 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 \<lbrace>\<lambda>rv s. obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s \<and> ct_in_state' activatable' s \<and> (ksCurThread s = ksIdleThread s \<or> tcb_in_cur_domain' (ksCurThread s) s)\<rbrace>
 4. \<And>curdom. \<lbrace>\<lambda>s. all_invs_but_ct_idle_or_in_cur_domain' s \<and> curdom = ksCurDomain s\<rbrace> getReadyQueuesL1Bitmap curdom \<lbrace>\<lambda>rv s. all_invs_but_ct_idle_or_in_cur_domain' s \<and> curdom = ksCurDomain s \<and> rv = ksReadyQueuesL1Bitmap s curdom\<rbrace>
 5. \<lbrace>all_invs_but_ct_idle_or_in_cur_domain'\<rbrace> if Suc 0 < numDomains then gets ksCurDomain else return 0 \<lbrace>\<lambda>rv s. all_invs_but_ct_idle_or_in_cur_domain' s \<and> rv = ksCurDomain s\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>curdom s. all_invs_but_ct_idle_or_in_cur_domain' s \<and> curdom = ksCurDomain s \<and> ksReadyQueuesL1Bitmap s curdom = 0 \<Longrightarrow> all_invs_but_ct_idle_or_in_cur_domain' s \<and> all_invs_but_ct_idle_or_in_cur_domain' s \<and> True
 2. \<And>curdom l1. l1 \<noteq> 0 \<Longrightarrow> \<lbrace>\<lambda>s. all_invs_but_ct_idle_or_in_cur_domain' s \<and> curdom = ksCurDomain s \<and> l1 = ksReadyQueuesL1Bitmap s curdom\<rbrace> 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 \<lbrace>\<lambda>rv s. obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s \<and> ct_in_state' activatable' s \<and> (ksCurThread s = ksIdleThread s \<or> tcb_in_cur_domain' (ksCurThread s) s)\<rbrace>
 3. \<And>curdom. \<lbrace>\<lambda>s. all_invs_but_ct_idle_or_in_cur_domain' s \<and> curdom = ksCurDomain s\<rbrace> getReadyQueuesL1Bitmap curdom \<lbrace>\<lambda>rv s. all_invs_but_ct_idle_or_in_cur_domain' s \<and> curdom = ksCurDomain s \<and> rv = ksReadyQueuesL1Bitmap s curdom\<rbrace>
 4. \<lbrace>all_invs_but_ct_idle_or_in_cur_domain'\<rbrace> if Suc 0 < numDomains then gets ksCurDomain else return 0 \<lbrace>\<lambda>rv s. all_invs_but_ct_idle_or_in_cur_domain' s \<and> rv = ksCurDomain s\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>curdom l1. l1 \<noteq> 0 \<Longrightarrow> \<lbrace>\<lambda>s. all_invs_but_ct_idle_or_in_cur_domain' s \<and> curdom = ksCurDomain s \<and> l1 = ksReadyQueuesL1Bitmap s curdom\<rbrace> 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 \<lbrace>\<lambda>rv s. obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s \<and> ct_in_state' activatable' s \<and> (ksCurThread s = ksIdleThread s \<or> tcb_in_cur_domain' (ksCurThread s) s)\<rbrace>
 2. \<And>curdom. \<lbrace>\<lambda>s. all_invs_but_ct_idle_or_in_cur_domain' s \<and> curdom = ksCurDomain s\<rbrace> getReadyQueuesL1Bitmap curdom \<lbrace>\<lambda>rv s. all_invs_but_ct_idle_or_in_cur_domain' s \<and> curdom = ksCurDomain s \<and> rv = ksReadyQueuesL1Bitmap s curdom\<rbrace>
 3. \<lbrace>all_invs_but_ct_idle_or_in_cur_domain'\<rbrace> if Suc 0 < numDomains then gets ksCurDomain else return 0 \<lbrace>\<lambda>rv s. all_invs_but_ct_idle_or_in_cur_domain' s \<and> rv = ksCurDomain s\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>curdom l1. l1 \<noteq> 0 \<Longrightarrow> \<lbrace>\<lambda>s. all_invs_but_ct_idle_or_in_cur_domain' s \<and> curdom = ksCurDomain s \<and> l1 = ksReadyQueuesL1Bitmap s curdom\<rbrace> 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 \<lbrace>\<lambda>rv s. obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s \<and> ct_in_state' activatable' s \<and> (ksCurThread s = ksIdleThread s \<or> tcb_in_cur_domain' (ksCurThread s) s)\<rbrace>
 2. \<And>curdom. \<lbrace>\<lambda>s. all_invs_but_ct_idle_or_in_cur_domain' s \<and> curdom = ksCurDomain s\<rbrace> getReadyQueuesL1Bitmap curdom \<lbrace>\<lambda>rv s. all_invs_but_ct_idle_or_in_cur_domain' s \<and> curdom = ksCurDomain s \<and> rv = ksReadyQueuesL1Bitmap s curdom\<rbrace>
 3. \<lbrace>all_invs_but_ct_idle_or_in_cur_domain'\<rbrace> if Suc 0 < numDomains then gets ksCurDomain else return 0 \<lbrace>\<lambda>rv s. all_invs_but_ct_idle_or_in_cur_domain' s \<and> rv = ksCurDomain s\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>curdom l1. l1 \<noteq> 0 \<Longrightarrow> \<lbrace>\<lambda>s. all_invs_but_ct_idle_or_in_cur_domain' s \<and> curdom = ksCurDomain s \<and> l1 = ksReadyQueuesL1Bitmap s curdom\<rbrace> do prio <- gets (lookupBitmapPriority curdom);
queue <- getQueue curdom prio;
runnable <- isRunnable (hd queue);
y <- assert runnable;
global.switchToThread (hd queue)
od \<lbrace>\<lambda>rv s. obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s \<and> ct_in_state' activatable' s \<and> (ksCurThread s = ksIdleThread s \<or> tcb_in_cur_domain' (ksCurThread s) s)\<rbrace>
 2. \<And>curdom. \<lbrace>\<lambda>s. all_invs_but_ct_idle_or_in_cur_domain' s \<and> curdom = ksCurDomain s\<rbrace> getReadyQueuesL1Bitmap curdom \<lbrace>\<lambda>rv s. all_invs_but_ct_idle_or_in_cur_domain' s \<and> curdom = ksCurDomain s \<and> rv = ksReadyQueuesL1Bitmap s curdom\<rbrace>
 3. \<lbrace>all_invs_but_ct_idle_or_in_cur_domain'\<rbrace> if Suc 0 < numDomains then gets ksCurDomain else return 0 \<lbrace>\<lambda>rv s. all_invs_but_ct_idle_or_in_cur_domain' s \<and> rv = ksCurDomain s\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>curdom l1 s. \<lbrakk>l1 \<noteq> 0; all_invs_but_ct_idle_or_in_cur_domain' s \<and> curdom = ksCurDomain s \<and> l1 = ksReadyQueuesL1Bitmap s curdom\<rbrakk> \<Longrightarrow> (all_invs_but_ct_idle_or_in_cur_domain' and tcb_at' (hd (ksReadyQueues s (curdom, lookupBitmapPriority curdom s)))) s \<and> obj_at' (activatable' \<circ> tcbState) (hd (ksReadyQueues s (curdom, lookupBitmapPriority curdom s))) s \<and> tcb_in_cur_domain' (hd (ksReadyQueues s (curdom, lookupBitmapPriority curdom s))) s
 2. \<And>curdom. \<lbrace>\<lambda>s. all_invs_but_ct_idle_or_in_cur_domain' s \<and> curdom = ksCurDomain s\<rbrace> getReadyQueuesL1Bitmap curdom \<lbrace>\<lambda>rv s. all_invs_but_ct_idle_or_in_cur_domain' s \<and> curdom = ksCurDomain s \<and> rv = ksReadyQueuesL1Bitmap s curdom\<rbrace>
 3. \<lbrace>all_invs_but_ct_idle_or_in_cur_domain'\<rbrace> if Suc 0 < numDomains then gets ksCurDomain else return 0 \<lbrace>\<lambda>rv s. all_invs_but_ct_idle_or_in_cur_domain' s \<and> rv = ksCurDomain s\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>ksReadyQueuesL1Bitmap s (ksCurDomain s) \<noteq> 0; all_invs_but_ct_idle_or_in_cur_domain' s\<rbrakk> \<Longrightarrow> tcb_at' (hd (ksReadyQueues s (ksCurDomain s, lookupBitmapPriority (ksCurDomain s) s))) s \<and> obj_at' (activatable' \<circ> tcbState) (hd (ksReadyQueues s (ksCurDomain s, lookupBitmapPriority (ksCurDomain s) s))) s \<and> tcb_in_cur_domain' (hd (ksReadyQueues s (ksCurDomain s, lookupBitmapPriority (ksCurDomain s) s))) s
 2. \<And>curdom. \<lbrace>\<lambda>s. all_invs_but_ct_idle_or_in_cur_domain' s \<and> curdom = ksCurDomain s\<rbrace> getReadyQueuesL1Bitmap curdom \<lbrace>\<lambda>rv s. all_invs_but_ct_idle_or_in_cur_domain' s \<and> curdom = ksCurDomain s \<and> rv = ksReadyQueuesL1Bitmap s curdom\<rbrace>
 3. \<lbrace>all_invs_but_ct_idle_or_in_cur_domain'\<rbrace> if Suc 0 < numDomains then gets ksCurDomain else return 0 \<lbrace>\<lambda>rv s. all_invs_but_ct_idle_or_in_cur_domain' s \<and> rv = ksCurDomain s\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>ksReadyQueuesL1Bitmap s (ksCurDomain s) \<noteq> 0; valid_queues_no_bitmap s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s\<rbrakk> \<Longrightarrow> tcb_at' (hd (ksReadyQueues s (ksCurDomain s, lookupBitmapPriority (ksCurDomain s) s))) s \<and> obj_at' (activatable' \<circ> tcbState) (hd (ksReadyQueues s (ksCurDomain s, lookupBitmapPriority (ksCurDomain s) s))) s \<and> tcb_in_cur_domain' (hd (ksReadyQueues s (ksCurDomain s, lookupBitmapPriority (ksCurDomain s) s))) s
 2. \<And>curdom. \<lbrace>\<lambda>s. all_invs_but_ct_idle_or_in_cur_domain' s \<and> curdom = ksCurDomain s\<rbrace> getReadyQueuesL1Bitmap curdom \<lbrace>\<lambda>rv s. all_invs_but_ct_idle_or_in_cur_domain' s \<and> curdom = ksCurDomain s \<and> rv = ksReadyQueuesL1Bitmap s curdom\<rbrace>
 3. \<lbrace>all_invs_but_ct_idle_or_in_cur_domain'\<rbrace> if Suc 0 < numDomains then gets ksCurDomain else return 0 \<lbrace>\<lambda>rv s. all_invs_but_ct_idle_or_in_cur_domain' s \<and> rv = ksCurDomain s\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>valid_queues_no_bitmap s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; obj_at' (inQ (ksCurDomain s) (lookupBitmapPriority (ksCurDomain s) s) and runnable' \<circ> tcbState) (hd (ksReadyQueues s (ksCurDomain s, lookupBitmapPriority (ksCurDomain s) s))) s\<rbrakk> \<Longrightarrow> tcb_at' (hd (ksReadyQueues s (ksCurDomain s, lookupBitmapPriority (ksCurDomain s) s))) s \<and> obj_at' (activatable' \<circ> tcbState) (hd (ksReadyQueues s (ksCurDomain s, lookupBitmapPriority (ksCurDomain s) s))) s \<and> tcb_in_cur_domain' (hd (ksReadyQueues s (ksCurDomain s, lookupBitmapPriority (ksCurDomain s) s))) s
 2. \<And>curdom. \<lbrace>\<lambda>s. all_invs_but_ct_idle_or_in_cur_domain' s \<and> curdom = ksCurDomain s\<rbrace> getReadyQueuesL1Bitmap curdom \<lbrace>\<lambda>rv s. all_invs_but_ct_idle_or_in_cur_domain' s \<and> curdom = ksCurDomain s \<and> rv = ksReadyQueuesL1Bitmap s curdom\<rbrace>
 3. \<lbrace>all_invs_but_ct_idle_or_in_cur_domain'\<rbrace> if Suc 0 < numDomains then gets ksCurDomain else return 0 \<lbrace>\<lambda>rv s. all_invs_but_ct_idle_or_in_cur_domain' s \<and> rv = ksCurDomain s\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>s ko. \<lbrakk>valid_queues_no_bitmap s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; ko_at' ko (hd (ksReadyQueues s (ksCurDomain s, lookupBitmapPriority (ksCurDomain s) s))) s; inQ (ksCurDomain s) (lookupBitmapPriority (ksCurDomain s) s) ko; runnable' (tcbState ko)\<rbrakk> \<Longrightarrow> tcb_in_cur_domain' (hd (ksReadyQueues s (ksCurDomain s, lookupBitmapPriority (ksCurDomain s) s))) s
 2. \<And>curdom. \<lbrace>\<lambda>s. all_invs_but_ct_idle_or_in_cur_domain' s \<and> curdom = ksCurDomain s\<rbrace> getReadyQueuesL1Bitmap curdom \<lbrace>\<lambda>rv s. all_invs_but_ct_idle_or_in_cur_domain' s \<and> curdom = ksCurDomain s \<and> rv = ksReadyQueuesL1Bitmap s curdom\<rbrace>
 3. \<lbrace>all_invs_but_ct_idle_or_in_cur_domain'\<rbrace> if Suc 0 < numDomains then gets ksCurDomain else return 0 \<lbrace>\<lambda>rv s. all_invs_but_ct_idle_or_in_cur_domain' s \<and> rv = ksCurDomain s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>curdom. \<lbrace>\<lambda>s. all_invs_but_ct_idle_or_in_cur_domain' s \<and> curdom = ksCurDomain s\<rbrace> getReadyQueuesL1Bitmap curdom \<lbrace>\<lambda>rv s. all_invs_but_ct_idle_or_in_cur_domain' s \<and> curdom = ksCurDomain s \<and> rv = ksReadyQueuesL1Bitmap s curdom\<rbrace>
 2. \<lbrace>all_invs_but_ct_idle_or_in_cur_domain'\<rbrace> if Suc 0 < numDomains then gets ksCurDomain else return 0 \<lbrace>\<lambda>rv s. all_invs_but_ct_idle_or_in_cur_domain' s \<and> rv = ksCurDomain s\<rbrace> proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrace>all_invs_but_ct_idle_or_in_cur_domain'\<rbrace> chooseThread \<lbrace>\<lambda>rv s. obj_at' (Not \<circ> tcbQueued) (ksCurThread s) s \<and> ct_in_state' activatable' s \<and> (ksCurThread s = ksIdleThread s \<or> tcb_in_cur_domain' (ksCurThread s) s)\<rbrace>

goal:
No subgoals!