theory Orphanage

lemma chooseThread_no_orphans [wp]:
  notes hoare_TrueI[simp]
  shows
  "\<lbrace>\<lambda>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)\<rbrace>
   chooseThread
   \<lbrace> \<lambda>rv s. no_orphans s \<rbrace>"
  (is "\<lbrace>?PRE\<rbrace> _ \<lbrace>_\<rbrace>") unfolding chooseThread_def Let_def supply if_split[split del] apply (simp only: return_bind, simp) apply (rule hoare_seq_ext[where B="\<lambda>rv s. ?PRE s \<and> rv = ksCurDomain s"]) apply (rule_tac B="\<lambda>rv s. ?PRE 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, wp (once), simp) 
    (* we have a thread to switch to *)
     apply (clarsimp simp: bitmap_fun_defs) apply (wp assert_inv ThreadDecls_H_switchToThread_no_orphans) apply (clarsimp simp: all_invs_but_ct_idle_or_in_cur_domain'_def valid_state'_def
                          valid_queues_def st_tcb_at'_def) apply (fastforce dest!: lookupBitmapPriority_obj_at' elim: obj_at'_weaken
                     simp: all_active_tcb_ptrs_def) apply (wpsimp simp: bitmap_fun_defs) apply (wp curDomain_or_return_0[simplified]) apply (wpsimp simp: curDomain_def simp: invs_no_cicd_ksCurDomain_maxDomain')+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>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)\<rbrace> chooseThread \<lbrace>\<lambda>rv. no_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>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)\<rbrace> 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 \<lbrace>\<lambda>rv. no_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>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)\<rbrace> 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 \<lbrace>\<lambda>rv. no_orphans\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>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)\<rbrace> do curdom <- if Suc 0 < numDomains then curDomain else return 0;
l1 <- getReadyQueuesL1Bitmap curdom;
if l1 \<noteq> 0 then do prio <- gets (lookupBitmapPriority curdom);
queue <- getQueue curdom prio;
runnable <- isRunnable (hd queue);
y <- assert runnable;
global.switchToThread (hd queue)
od else global.switchToIdleThread
od \<lbrace>\<lambda>rv. no_orphans\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>curdom. \<lbrace>\<lambda>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> curdom = ksCurDomain s\<rbrace> do l1 <- getReadyQueuesL1Bitmap curdom;
if l1 \<noteq> 0 then do prio <- gets (lookupBitmapPriority curdom);
queue <- getQueue curdom prio;
runnable <- isRunnable (hd queue);
y <- assert runnable;
global.switchToThread (hd queue)
od else global.switchToIdleThread
od \<lbrace>\<lambda>rv. no_orphans\<rbrace>
 2. \<lbrace>\<lambda>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)\<rbrace> if Suc 0 < numDomains then curDomain else return 0 \<lbrace>\<lambda>rv 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> rv = ksCurDomain s\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>curdom x. \<lbrace>\<lambda>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> curdom = ksCurDomain s \<and> x = ksReadyQueuesL1Bitmap s curdom\<rbrace> if x \<noteq> 0 then do prio <- gets (lookupBitmapPriority curdom);
queue <- getQueue curdom prio;
runnable <- isRunnable (hd queue);
y <- assert runnable;
global.switchToThread (hd queue)
od else global.switchToIdleThread \<lbrace>\<lambda>rv. no_orphans\<rbrace>
 2. \<And>curdom. \<lbrace>\<lambda>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> curdom = ksCurDomain s\<rbrace> getReadyQueuesL1Bitmap curdom \<lbrace>\<lambda>rv 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> curdom = ksCurDomain s \<and> rv = ksReadyQueuesL1Bitmap s curdom\<rbrace>
 3. \<lbrace>\<lambda>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)\<rbrace> if Suc 0 < numDomains then curDomain else return 0 \<lbrace>\<lambda>rv 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> rv = ksCurDomain s\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>curdom l1. \<lbrace>\<lambda>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> curdom = ksCurDomain s \<and> l1 = ksReadyQueuesL1Bitmap s curdom\<rbrace> if l1 \<noteq> 0 then do prio <- gets (lookupBitmapPriority curdom);
queue <- getQueue curdom prio;
runnable <- isRunnable (hd queue);
y <- assert runnable;
global.switchToThread (hd queue)
od else global.switchToIdleThread \<lbrace>\<lambda>rv. no_orphans\<rbrace>
 2. \<And>curdom. \<lbrace>\<lambda>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> curdom = ksCurDomain s\<rbrace> getReadyQueuesL1Bitmap curdom \<lbrace>\<lambda>rv 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> curdom = ksCurDomain s \<and> rv = ksReadyQueuesL1Bitmap s curdom\<rbrace>
 3. \<lbrace>\<lambda>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)\<rbrace> if Suc 0 < numDomains then curDomain else return 0 \<lbrace>\<lambda>rv 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> rv = ksCurDomain s\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>curdom l1. l1 = 0 \<Longrightarrow> \<lbrace>\<lambda>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> curdom = ksCurDomain s \<and> l1 = ksReadyQueuesL1Bitmap s curdom\<rbrace> if l1 \<noteq> 0 then do prio <- gets (lookupBitmapPriority curdom);
queue <- getQueue curdom prio;
runnable <- isRunnable (hd queue);
y <- assert runnable;
global.switchToThread (hd queue)
od else global.switchToIdleThread \<lbrace>\<lambda>rv. no_orphans\<rbrace>
 2. \<And>curdom l1. l1 \<noteq> 0 \<Longrightarrow> \<lbrace>\<lambda>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> curdom = ksCurDomain s \<and> l1 = ksReadyQueuesL1Bitmap s curdom\<rbrace> if l1 \<noteq> 0 then do prio <- gets (lookupBitmapPriority curdom);
queue <- getQueue curdom prio;
runnable <- isRunnable (hd queue);
y <- assert runnable;
global.switchToThread (hd queue)
od else global.switchToIdleThread \<lbrace>\<lambda>rv. no_orphans\<rbrace>
 3. \<And>curdom. \<lbrace>\<lambda>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> curdom = ksCurDomain s\<rbrace> getReadyQueuesL1Bitmap curdom \<lbrace>\<lambda>rv 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> curdom = ksCurDomain s \<and> rv = ksReadyQueuesL1Bitmap s curdom\<rbrace>
 4. \<lbrace>\<lambda>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)\<rbrace> if Suc 0 < numDomains then curDomain else return 0 \<lbrace>\<lambda>rv 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> rv = ksCurDomain s\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>curdom l1. l1 = 0 \<Longrightarrow> \<lbrace>\<lambda>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> curdom = ksCurDomain s \<and> l1 = ksReadyQueuesL1Bitmap s curdom\<rbrace> if l1 \<noteq> 0 then do prio <- gets (lookupBitmapPriority curdom);
queue <- getQueue curdom prio;
runnable <- isRunnable (hd queue);
y <- assert runnable;
global.switchToThread (hd queue)
od else global.switchToIdleThread \<lbrace>\<lambda>rv. no_orphans\<rbrace>
 2. \<And>curdom l1. l1 \<noteq> 0 \<Longrightarrow> \<lbrace>\<lambda>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> curdom = ksCurDomain s \<and> l1 = ksReadyQueuesL1Bitmap s curdom\<rbrace> if l1 \<noteq> 0 then do prio <- gets (lookupBitmapPriority curdom);
queue <- getQueue curdom prio;
runnable <- isRunnable (hd queue);
y <- assert runnable;
global.switchToThread (hd queue)
od else global.switchToIdleThread \<lbrace>\<lambda>rv. no_orphans\<rbrace>
 3. \<And>curdom. \<lbrace>\<lambda>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> curdom = ksCurDomain s\<rbrace> getReadyQueuesL1Bitmap curdom \<lbrace>\<lambda>rv 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> curdom = ksCurDomain s \<and> rv = ksReadyQueuesL1Bitmap s curdom\<rbrace>
 4. \<lbrace>\<lambda>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)\<rbrace> if Suc 0 < numDomains then curDomain else return 0 \<lbrace>\<lambda>rv 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> rv = ksCurDomain s\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>curdom l1. l1 \<noteq> 0 \<Longrightarrow> \<lbrace>\<lambda>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> curdom = ksCurDomain s \<and> l1 = ksReadyQueuesL1Bitmap s curdom\<rbrace> if l1 \<noteq> 0 then do prio <- gets (lookupBitmapPriority curdom);
queue <- getQueue curdom prio;
runnable <- isRunnable (hd queue);
y <- assert runnable;
global.switchToThread (hd queue)
od else global.switchToIdleThread \<lbrace>\<lambda>rv. no_orphans\<rbrace>
 2. \<And>curdom. \<lbrace>\<lambda>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> curdom = ksCurDomain s\<rbrace> getReadyQueuesL1Bitmap curdom \<lbrace>\<lambda>rv 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> curdom = ksCurDomain s \<and> rv = ksReadyQueuesL1Bitmap s curdom\<rbrace>
 3. \<lbrace>\<lambda>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)\<rbrace> if Suc 0 < numDomains then curDomain else return 0 \<lbrace>\<lambda>rv 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> rv = ksCurDomain s\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>curdom l1. l1 \<noteq> 0 \<Longrightarrow> \<lbrace>\<lambda>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> curdom = ksCurDomain s \<and> l1 = ksReadyQueuesL1Bitmap s curdom\<rbrace> if l1 \<noteq> 0 then do prio <- gets (lookupBitmapPriority curdom);
queue <- getQueue curdom prio;
runnable <- isRunnable (hd queue);
y <- assert runnable;
global.switchToThread (hd queue)
od else global.switchToIdleThread \<lbrace>\<lambda>rv. no_orphans\<rbrace>
 2. \<And>curdom. \<lbrace>\<lambda>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> curdom = ksCurDomain s\<rbrace> getReadyQueuesL1Bitmap curdom \<lbrace>\<lambda>rv 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> curdom = ksCurDomain s \<and> rv = ksReadyQueuesL1Bitmap s curdom\<rbrace>
 3. \<lbrace>\<lambda>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)\<rbrace> if Suc 0 < numDomains then curDomain else return 0 \<lbrace>\<lambda>rv 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> rv = ksCurDomain s\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>curdom l1. l1 \<noteq> 0 \<Longrightarrow> \<lbrace>\<lambda>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> 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. no_orphans\<rbrace>
 2. \<And>curdom. \<lbrace>\<lambda>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> curdom = ksCurDomain s\<rbrace> getReadyQueuesL1Bitmap curdom \<lbrace>\<lambda>rv 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> curdom = ksCurDomain s \<and> rv = ksReadyQueuesL1Bitmap s curdom\<rbrace>
 3. \<lbrace>\<lambda>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)\<rbrace> if Suc 0 < numDomains then curDomain else return 0 \<lbrace>\<lambda>rv 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> rv = ksCurDomain s\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>curdom l1 s. \<lbrakk>l1 \<noteq> 0; 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> curdom = ksCurDomain s \<and> l1 = ksReadyQueuesL1Bitmap s curdom\<rbrakk> \<Longrightarrow> no_orphans s \<and> st_tcb_at' runnable' (hd (ksReadyQueues s (curdom, lookupBitmapPriority curdom s))) s \<and> (ksCurThread s \<in> all_active_tcb_ptrs s \<longrightarrow> ksCurThread s \<in> all_queued_tcb_ptrs s)
 2. \<And>curdom. \<lbrace>\<lambda>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> curdom = ksCurDomain s\<rbrace> getReadyQueuesL1Bitmap curdom \<lbrace>\<lambda>rv 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> curdom = ksCurDomain s \<and> rv = ksReadyQueuesL1Bitmap s curdom\<rbrace>
 3. \<lbrace>\<lambda>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)\<rbrace> if Suc 0 < numDomains then curDomain else return 0 \<lbrace>\<lambda>rv 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> rv = ksCurDomain s\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>ksReadyQueuesL1Bitmap s (ksCurDomain s) \<noteq> 0; no_orphans s; valid_pspace' s; sch_act_wf (ksSchedulerAction s) s; valid_queues_no_bitmap s; valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; sym_refs (state_refs_of' s); if_live_then_nonz_cap' s; if_unsafe_then_cap' s; valid_idle' s; valid_global_refs' s; valid_arch_state' s; valid_irq_node' (irq_node' s) s; valid_irq_handlers' s; valid_irq_states' s; irqs_masked' s; valid_machine_state' s; cur_tcb' s; valid_queues' s; ct_not_inQ s; valid_pde_mappings' s; pspace_domain_valid s; ksCurDomain s \<le> maxDomain; ksDomSchedule (KernelInit_H.newKernelState undefined) \<noteq> []; \<forall>x\<in>set (ksDomSchedule (KernelInit_H.newKernelState undefined)). dschDomain x \<le> maxDomain \<and> 0 < dschLength x; ksDomSchedule s = ksDomSchedule (KernelInit_H.newKernelState undefined); ksDomScheduleIdx s < length (ksDomSchedule (KernelInit_H.newKernelState undefined)); untyped_ranges_zero' s; is_active_tcb_ptr (ksCurThread s) s \<longrightarrow> ksCurThread s \<in> all_queued_tcb_ptrs s\<rbrakk> \<Longrightarrow> obj_at' (runnable' \<circ> tcbState) (hd (ksReadyQueues s (ksCurDomain s, lookupBitmapPriority (ksCurDomain s) s))) s \<and> (ksCurThread s \<in> all_active_tcb_ptrs s \<longrightarrow> ksCurThread s \<in> all_queued_tcb_ptrs s)
 2. \<And>curdom. \<lbrace>\<lambda>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> curdom = ksCurDomain s\<rbrace> getReadyQueuesL1Bitmap curdom \<lbrace>\<lambda>rv 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> curdom = ksCurDomain s \<and> rv = ksReadyQueuesL1Bitmap s curdom\<rbrace>
 3. \<lbrace>\<lambda>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)\<rbrace> if Suc 0 < numDomains then curDomain else return 0 \<lbrace>\<lambda>rv 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> rv = ksCurDomain s\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>curdom. \<lbrace>\<lambda>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> curdom = ksCurDomain s\<rbrace> getReadyQueuesL1Bitmap curdom \<lbrace>\<lambda>rv 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> curdom = ksCurDomain s \<and> rv = ksReadyQueuesL1Bitmap s curdom\<rbrace>
 2. \<lbrace>\<lambda>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)\<rbrace> if Suc 0 < numDomains then curDomain else return 0 \<lbrace>\<lambda>rv 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> rv = ksCurDomain s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>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)\<rbrace> if Suc 0 < numDomains then curDomain else return 0 \<lbrace>\<lambda>rv 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> rv = ksCurDomain s\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<lbrace>?P'97\<rbrace> curDomain \<lbrace>\<lambda>rv s. rv = ksCurDomain s\<rbrace>
 2. \<And>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> ?P'97 s \<Longrightarrow> ksCurDomain s \<le> maxDomain
 3. \<And>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) \<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> ?P'97 s proof (prove)
goal:
No subgoals!