theory Schedule_R

lemma chooseThread_invs_no_cicd':
  "\<lbrace> invs_no_cicd' \<rbrace> chooseThread \<lbrace>\<lambda>rv. invs' \<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) 

  (* NOTE: do *not* unfold numDomains in the rest of the proof,
           it should work for any number *)

  (* FIXME this is almost identical to the chooseThread_invs_no_cicd'_posts proof, can generalise? *)
   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, wp (once) switchToIdleThread_invs_no_cicd', simp) 
      (* we have a thread to switch to *)
       apply (clarsimp simp: bitmap_fun_defs) apply (wp assert_inv) apply (clarsimp dest!: invs_no_cicd'_queues simp: valid_queues_def) apply (fastforce elim: bitmapQ_from_bitmap_lookup simp: lookupBitmapPriority_def) 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. invs'\<rbrace> proof (state)
goal (1 subgoal):
 1. \<lbrace>all_invs_but_ct_idle_or_in_cur_domain'\<rbrace> chooseThread \<lbrace>\<lambda>rv. invs'\<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. invs'\<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. invs'\<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. invs'\<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. invs'\<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. invs'\<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. invs'\<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. invs'\<rbrace> 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. invs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>all_invs_but_ct_idle_or_in_cur_domain'\<rbrace> chooseThread \<lbrace>\<lambda>rv. invs'\<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. invs'\<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. invs'\<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. invs'\<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. invs'\<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. invs'\<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. invs'\<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. invs'\<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. invs'\<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. invs'\<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. invs'\<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. invs'\<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. invs'\<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' s \<and> bitmapQ (ksCurDomain s) (lookupBitmapPriority (ksCurDomain s) s) s \<and> hd (ksReadyQueues s (curdom, lookupBitmapPriority curdom s)) = hd (ksReadyQueues s (ksCurDomain s, lookupBitmapPriority (ksCurDomain 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> bitmapQ (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. invs'\<rbrace>

goal:
No subgoals!