theory Schedule_R

lemma tcbSchedAppend_valid_queues'[wp]:
  (* most of this is identical to tcbSchedEnqueue_valid_queues' in TcbAcc_R *)
  "\<lbrace>valid_queues' and tcb_at' t\<rbrace> tcbSchedAppend t \<lbrace>\<lambda>_. valid_queues'\<rbrace>" apply (simp add: tcbSchedAppend_def) apply (rule hoare_pre) apply (rule_tac B="\<lambda>rv. valid_queues' and obj_at' (\<lambda>obj. tcbQueued obj = rv) t"
           in hoare_seq_ext) apply (rename_tac queued) apply (case_tac queued; simp_all add: unless_def when_def) apply (wp threadSet_valid_queues' setQueue_valid_queues' | simp)+ apply (subst conj_commute, wp) apply (rule hoare_pre_post, assumption) apply (clarsimp simp: addToBitmap_def modifyReadyQueuesL1Bitmap_def modifyReadyQueuesL2Bitmap_def
                               getReadyQueuesL1Bitmap_def getReadyQueuesL2Bitmap_def) apply wp apply fastforce apply wp apply (subst conj_commute) apply clarsimp apply (rule_tac Q="\<lambda>rv. valid_queues'
                   and obj_at' (\<lambda>obj. \<not> tcbQueued obj) t
                   and obj_at' (\<lambda>obj. tcbPriority obj = prio) t
                   and obj_at' (\<lambda>obj. tcbDomain obj = tdom) t
                   and (\<lambda>s. t \<in> set (ksReadyQueues s (tdom, prio)))"
                   in hoare_post_imp) apply (clarsimp simp: valid_queues'_def obj_at'_def projectKOs inQ_def) apply (wp setQueue_valid_queues' | simp | simp add: setQueue_def)+ apply (wp getObject_tcb_wp | simp add: threadGet_def)+ apply (clarsimp simp: obj_at'_def inQ_def projectKOs valid_queues'_def) apply (wp getObject_tcb_wp | simp add: threadGet_def)+ apply (clarsimp simp: obj_at'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_queues' and tcb_at' t\<rbrace> tcbSchedAppend t \<lbrace>\<lambda>_. valid_queues'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_queues' and tcb_at' t\<rbrace> do queued <- threadGet tcbQueued t;
unless queued (do tdom <- threadGet tcbDomain t;
prio <- threadGet tcbPriority t;
queue <- getQueue tdom prio;
y <- setQueue tdom prio (queue @ [t]);
y <- when (null queue) (addToBitmap tdom prio);
threadSet (tcbQueued_update (\<lambda>_. True)) t
od)
od \<lbrace>\<lambda>_. valid_queues'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> do queued <- threadGet tcbQueued t;
unless queued (do tdom <- threadGet tcbDomain t;
prio <- threadGet tcbPriority t;
queue <- getQueue tdom prio;
y <- setQueue tdom prio (queue @ [t]);
y <- when (null queue) (addToBitmap tdom prio);
threadSet (tcbQueued_update (\<lambda>_. True)) t
od)
od \<lbrace>\<lambda>_. valid_queues'\<rbrace>
 2. \<And>s. (valid_queues' and tcb_at' t) s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>x. \<lbrace>valid_queues' and obj_at' (\<lambda>obj. tcbQueued obj = x) t\<rbrace> unless x (do tdom <- threadGet tcbDomain t;
prio <- threadGet tcbPriority t;
queue <- getQueue tdom prio;
y <- setQueue tdom prio (queue @ [t]);
y <- when (null queue) (addToBitmap tdom prio);
threadSet (tcbQueued_update (\<lambda>_. True)) t
od) \<lbrace>\<lambda>_. valid_queues'\<rbrace>
 2. \<lbrace>?Q\<rbrace> threadGet tcbQueued t \<lbrace>\<lambda>rv. valid_queues' and obj_at' (\<lambda>obj. tcbQueued obj = rv) t\<rbrace>
 3. \<And>s. (valid_queues' and tcb_at' t) s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>queued. \<lbrace>valid_queues' and obj_at' (\<lambda>obj. tcbQueued obj = queued) t\<rbrace> unless queued (do tdom <- threadGet tcbDomain t;
prio <- threadGet tcbPriority t;
queue <- getQueue tdom prio;
y <- setQueue tdom prio (queue @ [t]);
y <- when (null queue) (addToBitmap tdom prio);
threadSet (tcbQueued_update (\<lambda>_. True)) t
od) \<lbrace>\<lambda>_. valid_queues'\<rbrace>
 2. \<lbrace>?Q\<rbrace> threadGet tcbQueued t \<lbrace>\<lambda>rv. valid_queues' and obj_at' (\<lambda>obj. tcbQueued obj = rv) t\<rbrace>
 3. \<And>s. (valid_queues' and tcb_at' t) s \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>queued. queued \<Longrightarrow> \<lbrace>valid_queues' and obj_at' tcbQueued t\<rbrace> return () \<lbrace>\<lambda>_. valid_queues'\<rbrace>
 2. \<And>queued. \<not> queued \<Longrightarrow> \<lbrace>valid_queues' and obj_at' (\<lambda>obj. \<not> tcbQueued obj) t\<rbrace> do tdom <- threadGet tcbDomain t;
prio <- threadGet tcbPriority t;
queue <- getQueue tdom prio;
y <- setQueue tdom prio (queue @ [t]);
y <- if null queue then addToBitmap tdom prio else return ();
threadSet (tcbQueued_update (\<lambda>_. True)) t
od \<lbrace>\<lambda>_. valid_queues'\<rbrace>
 3. \<lbrace>?Q\<rbrace> threadGet tcbQueued t \<lbrace>\<lambda>rv. valid_queues' and obj_at' (\<lambda>obj. tcbQueued obj = rv) t\<rbrace>
 4. \<And>s. (valid_queues' and tcb_at' t) s \<Longrightarrow> ?Q s proof (prove)
goal (9 subgoals):
 1. \<And>queued tdom prio queue. \<lbrakk>\<not> queued; null queue\<rbrakk> \<Longrightarrow> \<lbrace>?Q23 False tdom prio queue ()\<rbrace> addToBitmap tdom prio \<lbrace>\<lambda>ya s. (\<forall>ko qdom prio. ko_at' ko t s \<and> inQ qdom prio (tcbQueued_update (\<lambda>_. True) ko) \<and> \<not> inQ qdom prio ko \<longrightarrow> t \<in> set (ksReadyQueues s (qdom, prio))) \<and> valid_queues' s\<rbrace>
 2. \<And>queued tdom prio queue y. \<lbrakk>\<not> queued; \<not> null queue\<rbrakk> \<Longrightarrow> \<lbrace>?R23 queued tdom prio queue y\<rbrace> return () \<lbrace>\<lambda>ya s. (\<forall>ko qdom prio. ko_at' ko t s \<and> inQ qdom prio (tcbQueued_update (\<lambda>_. True) ko) \<and> \<not> inQ qdom prio ko \<longrightarrow> t \<in> set (ksReadyQueues s (qdom, prio))) \<and> valid_queues' s\<rbrace>
 3. \<And>queued tdom prio queue. \<not> queued \<Longrightarrow> \<lbrace>?B19 queued tdom prio queue\<rbrace> setQueue tdom prio (queue @ [t]) \<lbrace>\<lambda>y s. (null queue \<longrightarrow> ?Q23 queued tdom prio queue y s) \<and> (\<not> null queue \<longrightarrow> ?R23 queued tdom prio queue y s)\<rbrace>
 4. \<And>queued tdom prio. \<not> queued \<Longrightarrow> \<lbrace>?B18 queued tdom prio\<rbrace> getQueue tdom prio \<lbrace>?B19 queued tdom prio\<rbrace>
 5. \<And>queued tdom. \<not> queued \<Longrightarrow> \<lbrace>?B17 queued tdom\<rbrace> threadGet tcbPriority t \<lbrace>?B18 queued tdom\<rbrace>
 6. \<And>queued. \<not> queued \<Longrightarrow> \<lbrace>?Q16 queued\<rbrace> threadGet tcbDomain t \<lbrace>?B17 queued\<rbrace>
 7. \<And>queued s. \<lbrakk>\<not> queued; (valid_queues' and obj_at' (\<lambda>obj. \<not> tcbQueued obj) t) s\<rbrakk> \<Longrightarrow> ?Q16 queued s
 8. \<lbrace>?Q\<rbrace> threadGet tcbQueued t \<lbrace>\<lambda>rv. valid_queues' and obj_at' (\<lambda>obj. tcbQueued obj = rv) t\<rbrace>
 9. \<And>s. (valid_queues' and tcb_at' t) s \<Longrightarrow> ?Q s proof (prove)
goal (9 subgoals):
 1. \<And>queued tdom prio queue. \<lbrakk>\<not> queued; null queue\<rbrakk> \<Longrightarrow> \<lbrace>?P'30 queued tdom prio queue (ds_id False) tdom prio (?queue26 queued tdom prio queue) ()\<rbrace> addToBitmap tdom prio \<lbrace>\<lambda>rv s. \<forall>ko qdom prio. ko_at' ko t s \<and> inQ qdom prio (tcbQueued_update (\<lambda>_. True) ko) \<and> \<not> inQ qdom prio ko \<longrightarrow> t \<in> set (ksReadyQueues s (qdom, prio))\<rbrace>
 2. \<And>queued tdom prio queue y. \<lbrakk>\<not> queued; \<not> null queue\<rbrakk> \<Longrightarrow> \<lbrace>?R23 queued tdom prio queue y\<rbrace> return () \<lbrace>\<lambda>ya s. (\<forall>ko qdom prio. ko_at' ko t s \<and> inQ qdom prio (tcbQueued_update (\<lambda>_. True) ko) \<and> \<not> inQ qdom prio ko \<longrightarrow> t \<in> set (ksReadyQueues s (qdom, prio))) \<and> valid_queues' s\<rbrace>
 3. \<And>queued tdom prio queue. \<not> queued \<Longrightarrow> \<lbrace>?B19 queued tdom prio queue\<rbrace> setQueue tdom prio (queue @ [t]) \<lbrace>\<lambda>y s. (null queue \<longrightarrow> valid_queues' s \<and> ?P'32 queued tdom prio queue y s) \<and> (\<not> null queue \<longrightarrow> ?R23 queued tdom prio queue y s)\<rbrace>
 4. \<And>queued tdom prio. \<not> queued \<Longrightarrow> \<lbrace>?B18 queued tdom prio\<rbrace> getQueue tdom prio \<lbrace>?B19 queued tdom prio\<rbrace>
 5. \<And>queued tdom. \<not> queued \<Longrightarrow> \<lbrace>?B17 queued tdom\<rbrace> threadGet tcbPriority t \<lbrace>?B18 queued tdom\<rbrace>
 6. \<And>queued. \<not> queued \<Longrightarrow> \<lbrace>?Q16 queued\<rbrace> threadGet tcbDomain t \<lbrace>?B17 queued\<rbrace>
 7. \<And>queued s. \<lbrakk>\<not> queued; (valid_queues' and obj_at' (\<lambda>obj. \<not> tcbQueued obj) t) s\<rbrakk> \<Longrightarrow> ?Q16 queued s
 8. \<lbrace>?Q\<rbrace> threadGet tcbQueued t \<lbrace>\<lambda>rv. valid_queues' and obj_at' (\<lambda>obj. tcbQueued obj = rv) t\<rbrace>
 9. \<And>s. (valid_queues' and tcb_at' t) s \<Longrightarrow> ?Q s
flex-flex pairs:
\<lambda>queued tdom prio queue. ?P'32 False tdom prio queue () \<equiv>\<^sup>? \<lambda>queued tdom prio queue. ?P'30 queued tdom prio queue False tdom prio (?queue26 queued tdom prio queue) () proof (prove)
goal (9 subgoals):
 1. \<And>queued tdom prio queue. \<lbrakk>\<not> queued; null queue\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>a. \<forall>ko qdom prio. ko_at' ko t a \<and> inQ qdom prio (tcbQueued_update (\<lambda>_. True) ko) \<and> \<not> inQ qdom prio ko \<longrightarrow> t \<in> set (ksReadyQueues a (qdom, prio))\<rbrace> addToBitmap tdom prio \<lbrace>\<lambda>rv a. \<forall>ko qdom prio. ko_at' ko t a \<and> inQ qdom prio (tcbQueued_update (\<lambda>_. True) ko) \<and> \<not> inQ qdom prio ko \<longrightarrow> t \<in> set (ksReadyQueues a (qdom, prio))\<rbrace>
 2. \<And>queued tdom prio queue y. \<lbrakk>\<not> queued; \<not> null queue\<rbrakk> \<Longrightarrow> \<lbrace>?R23 queued tdom prio queue y\<rbrace> return () \<lbrace>\<lambda>ya s. (\<forall>ko qdom prio. ko_at' ko t s \<and> inQ qdom prio (tcbQueued_update (\<lambda>_. True) ko) \<and> \<not> inQ qdom prio ko \<longrightarrow> t \<in> set (ksReadyQueues s (qdom, prio))) \<and> valid_queues' s\<rbrace>
 3. \<And>queued tdom prio queue. \<not> queued \<Longrightarrow> \<lbrace>?B19 queued tdom prio queue\<rbrace> setQueue tdom prio (queue @ [t]) \<lbrace>\<lambda>y s. (null queue \<longrightarrow> valid_queues' s \<and> (\<forall>ko qdom prio. ko_at' ko t s \<and> inQ qdom prio (tcbQueued_update (\<lambda>_. True) ko) \<and> \<not> inQ qdom prio ko \<longrightarrow> t \<in> set (ksReadyQueues s (qdom, prio)))) \<and> (\<not> null queue \<longrightarrow> ?R23 queued tdom prio queue y s)\<rbrace>
 4. \<And>queued tdom prio. \<not> queued \<Longrightarrow> \<lbrace>?B18 queued tdom prio\<rbrace> getQueue tdom prio \<lbrace>?B19 queued tdom prio\<rbrace>
 5. \<And>queued tdom. \<not> queued \<Longrightarrow> \<lbrace>?B17 queued tdom\<rbrace> threadGet tcbPriority t \<lbrace>?B18 queued tdom\<rbrace>
 6. \<And>queued. \<not> queued \<Longrightarrow> \<lbrace>?Q16 queued\<rbrace> threadGet tcbDomain t \<lbrace>?B17 queued\<rbrace>
 7. \<And>queued s. \<lbrakk>\<not> queued; (valid_queues' and obj_at' (\<lambda>obj. \<not> tcbQueued obj) t) s\<rbrakk> \<Longrightarrow> ?Q16 queued s
 8. \<lbrace>?Q\<rbrace> threadGet tcbQueued t \<lbrace>\<lambda>rv. valid_queues' and obj_at' (\<lambda>obj. tcbQueued obj = rv) t\<rbrace>
 9. \<And>s. (valid_queues' and tcb_at' t) s \<Longrightarrow> ?Q s proof (prove)
goal (9 subgoals):
 1. \<And>queued tdom prio queue. \<lbrakk>\<not> queued; null queue\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>a. \<forall>ko qdom prio. ko_at' ko t a \<and> inQ qdom prio (tcbQueued_update (\<lambda>_. True) ko) \<and> \<not> inQ qdom prio ko \<longrightarrow> t \<in> set (ksReadyQueues a (qdom, prio))\<rbrace> do y <- do l1 <- gets (\<lambda>ks. ksReadyQueuesL1Bitmap ks tdom);
modify (\<lambda>ks. ks\<lparr>ksReadyQueuesL1Bitmap := (ksReadyQueuesL1Bitmap ks)(tdom := l1 || 2 ^ prioToL1Index prio)\<rparr>)
od;
l2 <- gets (\<lambda>ks. ksReadyQueuesL2Bitmap ks (tdom, invertL1Index (prioToL1Index prio)));
modify (\<lambda>ks. ks\<lparr>ksReadyQueuesL2Bitmap := (ksReadyQueuesL2Bitmap ks)((tdom, invertL1Index (prioToL1Index prio)) := l2 || 2 ^ unat (prio && mask wordRadix))\<rparr>)
od \<lbrace>\<lambda>rv a. \<forall>ko qdom prio. ko_at' ko t a \<and> inQ qdom prio (tcbQueued_update (\<lambda>_. True) ko) \<and> \<not> inQ qdom prio ko \<longrightarrow> t \<in> set (ksReadyQueues a (qdom, prio))\<rbrace>
 2. \<And>queued tdom prio queue y. \<lbrakk>\<not> queued; \<not> null queue\<rbrakk> \<Longrightarrow> \<lbrace>?R23 queued tdom prio queue y\<rbrace> return () \<lbrace>\<lambda>ya s. (\<forall>ko qdom prio. ko_at' ko t s \<and> inQ qdom prio (tcbQueued_update (\<lambda>_. True) ko) \<and> \<not> inQ qdom prio ko \<longrightarrow> t \<in> set (ksReadyQueues s (qdom, prio))) \<and> valid_queues' s\<rbrace>
 3. \<And>queued tdom prio queue. \<not> queued \<Longrightarrow> \<lbrace>?B19 queued tdom prio queue\<rbrace> setQueue tdom prio (queue @ [t]) \<lbrace>\<lambda>y s. (null queue \<longrightarrow> valid_queues' s \<and> (\<forall>ko qdom prio. ko_at' ko t s \<and> inQ qdom prio (tcbQueued_update (\<lambda>_. True) ko) \<and> \<not> inQ qdom prio ko \<longrightarrow> t \<in> set (ksReadyQueues s (qdom, prio)))) \<and> (\<not> null queue \<longrightarrow> ?R23 queued tdom prio queue y s)\<rbrace>
 4. \<And>queued tdom prio. \<not> queued \<Longrightarrow> \<lbrace>?B18 queued tdom prio\<rbrace> getQueue tdom prio \<lbrace>?B19 queued tdom prio\<rbrace>
 5. \<And>queued tdom. \<not> queued \<Longrightarrow> \<lbrace>?B17 queued tdom\<rbrace> threadGet tcbPriority t \<lbrace>?B18 queued tdom\<rbrace>
 6. \<And>queued. \<not> queued \<Longrightarrow> \<lbrace>?Q16 queued\<rbrace> threadGet tcbDomain t \<lbrace>?B17 queued\<rbrace>
 7. \<And>queued s. \<lbrakk>\<not> queued; (valid_queues' and obj_at' (\<lambda>obj. \<not> tcbQueued obj) t) s\<rbrakk> \<Longrightarrow> ?Q16 queued s
 8. \<lbrace>?Q\<rbrace> threadGet tcbQueued t \<lbrace>\<lambda>rv. valid_queues' and obj_at' (\<lambda>obj. tcbQueued obj = rv) t\<rbrace>
 9. \<And>s. (valid_queues' and tcb_at' t) s \<Longrightarrow> ?Q s proof (prove)
goal (9 subgoals):
 1. \<And>queued tdom prio queue s. \<lbrakk>\<not> queued; null queue; \<forall>ko qdom prio. ko_at' ko t s \<and> inQ qdom prio (tcbQueued_update (\<lambda>_. True) ko) \<and> \<not> inQ qdom prio ko \<longrightarrow> t \<in> set (ksReadyQueues s (qdom, prio))\<rbrakk> \<Longrightarrow> \<forall>ko qdom prioa. ko_at' ko t (s\<lparr>ksReadyQueuesL1Bitmap := (ksReadyQueuesL1Bitmap s)(tdom := ksReadyQueuesL1Bitmap s tdom || 2 ^ prioToL1Index prio), ksReadyQueuesL2Bitmap := (ksReadyQueuesL2Bitmap (s\<lparr>ksReadyQueuesL1Bitmap := (ksReadyQueuesL1Bitmap s)(tdom := ksReadyQueuesL1Bitmap s tdom || 2 ^ prioToL1Index prio)\<rparr>))((tdom, invertL1Index (prioToL1Index prio)) := ksReadyQueuesL2Bitmap (s\<lparr>ksReadyQueuesL1Bitmap := (ksReadyQueuesL1Bitmap s)(tdom := ksReadyQueuesL1Bitmap s tdom || 2 ^ prioToL1Index prio)\<rparr>) (tdom, invertL1Index (prioToL1Index prio)) || 2 ^ unat (prio && mask wordRadix))\<rparr>) \<and> inQ qdom prioa (tcbQueued_update (\<lambda>_. True) ko) \<and> \<not> inQ qdom prioa ko \<longrightarrow> t \<in> set (ksReadyQueues (s\<lparr>ksReadyQueuesL1Bitmap := (ksReadyQueuesL1Bitmap s)(tdom := ksReadyQueuesL1Bitmap s tdom || 2 ^ prioToL1Index prio), ksReadyQueuesL2Bitmap := (ksReadyQueuesL2Bitmap (s\<lparr>ksReadyQueuesL1Bitmap := (ksReadyQueuesL1Bitmap s)(tdom := ksReadyQueuesL1Bitmap s tdom || 2 ^ prioToL1Index prio)\<rparr>))((tdom, invertL1Index (prioToL1Index prio)) := ksReadyQueuesL2Bitmap (s\<lparr>ksReadyQueuesL1Bitmap := (ksReadyQueuesL1Bitmap s)(tdom := ksReadyQueuesL1Bitmap s tdom || 2 ^ prioToL1Index prio)\<rparr>) (tdom, invertL1Index (prioToL1Index prio)) || 2 ^ unat (prio && mask wordRadix))\<rparr>) (qdom, prioa))
 2. \<And>queued tdom prio queue y. \<lbrakk>\<not> queued; \<not> null queue\<rbrakk> \<Longrightarrow> \<lbrace>?R23 queued tdom prio queue y\<rbrace> return () \<lbrace>\<lambda>ya s. (\<forall>ko qdom prio. ko_at' ko t s \<and> inQ qdom prio (tcbQueued_update (\<lambda>_. True) ko) \<and> \<not> inQ qdom prio ko \<longrightarrow> t \<in> set (ksReadyQueues s (qdom, prio))) \<and> valid_queues' s\<rbrace>
 3. \<And>queued tdom prio queue. \<not> queued \<Longrightarrow> \<lbrace>?B19 queued tdom prio queue\<rbrace> setQueue tdom prio (queue @ [t]) \<lbrace>\<lambda>y s. (null queue \<longrightarrow> valid_queues' s \<and> (\<forall>ko qdom prio. ko_at' ko t s \<and> inQ qdom prio (tcbQueued_update (\<lambda>_. True) ko) \<and> \<not> inQ qdom prio ko \<longrightarrow> t \<in> set (ksReadyQueues s (qdom, prio)))) \<and> (\<not> null queue \<longrightarrow> ?R23 queued tdom prio queue y s)\<rbrace>
 4. \<And>queued tdom prio. \<not> queued \<Longrightarrow> \<lbrace>?B18 queued tdom prio\<rbrace> getQueue tdom prio \<lbrace>?B19 queued tdom prio\<rbrace>
 5. \<And>queued tdom. \<not> queued \<Longrightarrow> \<lbrace>?B17 queued tdom\<rbrace> threadGet tcbPriority t \<lbrace>?B18 queued tdom\<rbrace>
 6. \<And>queued. \<not> queued \<Longrightarrow> \<lbrace>?Q16 queued\<rbrace> threadGet tcbDomain t \<lbrace>?B17 queued\<rbrace>
 7. \<And>queued s. \<lbrakk>\<not> queued; (valid_queues' and obj_at' (\<lambda>obj. \<not> tcbQueued obj) t) s\<rbrakk> \<Longrightarrow> ?Q16 queued s
 8. \<lbrace>?Q\<rbrace> threadGet tcbQueued t \<lbrace>\<lambda>rv. valid_queues' and obj_at' (\<lambda>obj. tcbQueued obj = rv) t\<rbrace>
 9. \<And>s. (valid_queues' and tcb_at' t) s \<Longrightarrow> ?Q s proof (prove)
goal (8 subgoals):
 1. \<And>queued tdom prio queue y. \<lbrakk>\<not> queued; \<not> null queue\<rbrakk> \<Longrightarrow> \<lbrace>?R23 queued tdom prio queue y\<rbrace> return () \<lbrace>\<lambda>ya s. (\<forall>ko qdom prio. ko_at' ko t s \<and> inQ qdom prio (tcbQueued_update (\<lambda>_. True) ko) \<and> \<not> inQ qdom prio ko \<longrightarrow> t \<in> set (ksReadyQueues s (qdom, prio))) \<and> valid_queues' s\<rbrace>
 2. \<And>queued tdom prio queue. \<not> queued \<Longrightarrow> \<lbrace>?B19 queued tdom prio queue\<rbrace> setQueue tdom prio (queue @ [t]) \<lbrace>\<lambda>y s. (null queue \<longrightarrow> valid_queues' s \<and> (\<forall>ko qdom prio. ko_at' ko t s \<and> inQ qdom prio (tcbQueued_update (\<lambda>_. True) ko) \<and> \<not> inQ qdom prio ko \<longrightarrow> t \<in> set (ksReadyQueues s (qdom, prio)))) \<and> (\<not> null queue \<longrightarrow> ?R23 queued tdom prio queue y s)\<rbrace>
 3. \<And>queued tdom prio. \<not> queued \<Longrightarrow> \<lbrace>?B18 queued tdom prio\<rbrace> getQueue tdom prio \<lbrace>?B19 queued tdom prio\<rbrace>
 4. \<And>queued tdom. \<not> queued \<Longrightarrow> \<lbrace>?B17 queued tdom\<rbrace> threadGet tcbPriority t \<lbrace>?B18 queued tdom\<rbrace>
 5. \<And>queued. \<not> queued \<Longrightarrow> \<lbrace>?Q16 queued\<rbrace> threadGet tcbDomain t \<lbrace>?B17 queued\<rbrace>
 6. \<And>queued s. \<lbrakk>\<not> queued; (valid_queues' and obj_at' (\<lambda>obj. \<not> tcbQueued obj) t) s\<rbrakk> \<Longrightarrow> ?Q16 queued s
 7. \<lbrace>?Q\<rbrace> threadGet tcbQueued t \<lbrace>\<lambda>rv. valid_queues' and obj_at' (\<lambda>obj. tcbQueued obj = rv) t\<rbrace>
 8. \<And>s. (valid_queues' and tcb_at' t) s \<Longrightarrow> ?Q s proof (prove)
goal (7 subgoals):
 1. \<And>queued tdom prio queue. \<not> queued \<Longrightarrow> \<lbrace>?B19 queued tdom prio queue\<rbrace> setQueue tdom prio (queue @ [t]) \<lbrace>\<lambda>y s. (null queue \<longrightarrow> valid_queues' s \<and> (\<forall>ko qdom prio. ko_at' ko t s \<and> inQ qdom prio (tcbQueued_update (\<lambda>_. True) ko) \<and> \<not> inQ qdom prio ko \<longrightarrow> t \<in> set (ksReadyQueues s (qdom, prio)))) \<and> (\<not> null queue \<longrightarrow> (\<forall>ko qdom prio. ko_at' ko t s \<and> inQ qdom prio (tcbQueued_update (\<lambda>_. True) ko) \<and> \<not> inQ qdom prio ko \<longrightarrow> t \<in> set (ksReadyQueues s (qdom, prio))) \<and> valid_queues' s)\<rbrace>
 2. \<And>queued tdom prio. \<not> queued \<Longrightarrow> \<lbrace>?B18 queued tdom prio\<rbrace> getQueue tdom prio \<lbrace>?B19 queued tdom prio\<rbrace>
 3. \<And>queued tdom. \<not> queued \<Longrightarrow> \<lbrace>?B17 queued tdom\<rbrace> threadGet tcbPriority t \<lbrace>?B18 queued tdom\<rbrace>
 4. \<And>queued. \<not> queued \<Longrightarrow> \<lbrace>?Q16 queued\<rbrace> threadGet tcbDomain t \<lbrace>?B17 queued\<rbrace>
 5. \<And>queued s. \<lbrakk>\<not> queued; (valid_queues' and obj_at' (\<lambda>obj. \<not> tcbQueued obj) t) s\<rbrakk> \<Longrightarrow> ?Q16 queued s
 6. \<lbrace>?Q\<rbrace> threadGet tcbQueued t \<lbrace>\<lambda>rv. valid_queues' and obj_at' (\<lambda>obj. tcbQueued obj = rv) t\<rbrace>
 7. \<And>s. (valid_queues' and tcb_at' t) s \<Longrightarrow> ?Q s proof (prove)
goal (7 subgoals):
 1. \<And>queued tdom prio queue. \<not> queued \<Longrightarrow> \<lbrace>?B65 queued tdom prio queue (?queued65 queued tdom prio queue) tdom prio queue\<rbrace> setQueue tdom prio (queue @ [t]) \<lbrace>\<lambda>y s. (null queue \<longrightarrow> (\<forall>ko qdom prio. ko_at' ko t s \<and> inQ qdom prio (tcbQueued_update (\<lambda>_. True) ko) \<and> \<not> inQ qdom prio ko \<longrightarrow> t \<in> set (ksReadyQueues s (qdom, prio))) \<and> valid_queues' s) \<and> (\<not> null queue \<longrightarrow> (\<forall>ko qdom prio. ko_at' ko t s \<and> inQ qdom prio (tcbQueued_update (\<lambda>_. True) ko) \<and> \<not> inQ qdom prio ko \<longrightarrow> t \<in> set (ksReadyQueues s (qdom, prio))) \<and> valid_queues' s)\<rbrace>
 2. \<And>queued tdom prio. \<not> queued \<Longrightarrow> \<lbrace>?B18 queued tdom prio\<rbrace> getQueue tdom prio \<lbrace>\<lambda>queue. ?B65 queued tdom prio queue (?queued65 queued tdom prio queue) tdom prio queue\<rbrace>
 3. \<And>queued tdom. \<not> queued \<Longrightarrow> \<lbrace>?B17 queued tdom\<rbrace> threadGet tcbPriority t \<lbrace>?B18 queued tdom\<rbrace>
 4. \<And>queued. \<not> queued \<Longrightarrow> \<lbrace>?Q16 queued\<rbrace> threadGet tcbDomain t \<lbrace>?B17 queued\<rbrace>
 5. \<And>queued s. \<lbrakk>\<not> queued; (valid_queues' and obj_at' (\<lambda>obj. \<not> tcbQueued obj) t) s\<rbrakk> \<Longrightarrow> ?Q16 queued s
 6. \<lbrace>?Q\<rbrace> threadGet tcbQueued t \<lbrace>\<lambda>rv. valid_queues' and obj_at' (\<lambda>obj. tcbQueued obj = rv) t\<rbrace>
 7. \<And>s. (valid_queues' and tcb_at' t) s \<Longrightarrow> ?Q s proof (prove)
goal (7 subgoals):
 1. \<And>queued tdom prio queue. \<not> queued \<Longrightarrow> \<lbrace>?B65 False tdom prio queue (?queued65 False tdom prio queue) tdom prio queue\<rbrace> setQueue tdom prio (queue @ [t]) \<lbrace>\<lambda>y s. (\<forall>ko qdom prio. ko_at' ko t s \<and> inQ qdom prio (tcbQueued_update (\<lambda>_. True) ko) \<and> \<not> inQ qdom prio ko \<longrightarrow> t \<in> set (ksReadyQueues s (qdom, prio))) \<and> valid_queues' s\<rbrace>
 2. \<And>queued tdom prio. \<not> queued \<Longrightarrow> \<lbrace>?B18 queued tdom prio\<rbrace> getQueue tdom prio \<lbrace>\<lambda>queue. ?B65 queued tdom prio queue (?queued65 queued tdom prio queue) tdom prio queue\<rbrace>
 3. \<And>queued tdom. \<not> queued \<Longrightarrow> \<lbrace>?B17 queued tdom\<rbrace> threadGet tcbPriority t \<lbrace>?B18 queued tdom\<rbrace>
 4. \<And>queued. \<not> queued \<Longrightarrow> \<lbrace>?Q16 queued\<rbrace> threadGet tcbDomain t \<lbrace>?B17 queued\<rbrace>
 5. \<And>queued s. \<lbrakk>\<not> queued; (valid_queues' and obj_at' (\<lambda>obj. \<not> tcbQueued obj) t) s\<rbrakk> \<Longrightarrow> ?Q16 queued s
 6. \<lbrace>?Q\<rbrace> threadGet tcbQueued t \<lbrace>\<lambda>rv. valid_queues' and obj_at' (\<lambda>obj. tcbQueued obj = rv) t\<rbrace>
 7. \<And>s. (valid_queues' and tcb_at' t) s \<Longrightarrow> ?Q s proof (prove)
goal (8 subgoals):
 1. \<And>queued tdom prio queue rv s. \<lbrakk>\<not> queued; (valid_queues' and obj_at' (\<lambda>obj. \<not> tcbQueued obj) t and obj_at' (\<lambda>obj. tcbPriority obj = prio) t and obj_at' (\<lambda>obj. tcbDomain obj = tdom) t and (\<lambda>s. t \<in> set (ksReadyQueues s (tdom, prio)))) s\<rbrakk> \<Longrightarrow> (\<forall>ko qdom prio. ko_at' ko t s \<and> inQ qdom prio (tcbQueued_update (\<lambda>_. True) ko) \<and> \<not> inQ qdom prio ko \<longrightarrow> t \<in> set (ksReadyQueues s (qdom, prio))) \<and> valid_queues' s
 2. \<And>queued tdom prio queue. \<not> queued \<Longrightarrow> \<lbrace>?B65 False tdom prio queue (?queued65 False tdom prio queue) tdom prio queue\<rbrace> setQueue tdom prio (queue @ [t]) \<lbrace>\<lambda>rv. valid_queues' and obj_at' (\<lambda>obj. \<not> tcbQueued obj) t and obj_at' (\<lambda>obj. tcbPriority obj = prio) t and obj_at' (\<lambda>obj. tcbDomain obj = tdom) t and (\<lambda>s. t \<in> set (ksReadyQueues s (tdom, prio)))\<rbrace>
 3. \<And>queued tdom prio. \<not> queued \<Longrightarrow> \<lbrace>?B18 queued tdom prio\<rbrace> getQueue tdom prio \<lbrace>\<lambda>queue. ?B65 queued tdom prio queue (?queued65 queued tdom prio queue) tdom prio queue\<rbrace>
 4. \<And>queued tdom. \<not> queued \<Longrightarrow> \<lbrace>?B17 queued tdom\<rbrace> threadGet tcbPriority t \<lbrace>?B18 queued tdom\<rbrace>
 5. \<And>queued. \<not> queued \<Longrightarrow> \<lbrace>?Q16 queued\<rbrace> threadGet tcbDomain t \<lbrace>?B17 queued\<rbrace>
 6. \<And>queued s. \<lbrakk>\<not> queued; (valid_queues' and obj_at' (\<lambda>obj. \<not> tcbQueued obj) t) s\<rbrakk> \<Longrightarrow> ?Q16 queued s
 7. \<lbrace>?Q\<rbrace> threadGet tcbQueued t \<lbrace>\<lambda>rv. valid_queues' and obj_at' (\<lambda>obj. tcbQueued obj = rv) t\<rbrace>
 8. \<And>s. (valid_queues' and tcb_at' t) s \<Longrightarrow> ?Q s proof (prove)
goal (7 subgoals):
 1. \<And>queued tdom prio queue. \<not> queued \<Longrightarrow> \<lbrace>?B65 False tdom prio queue (?queued65 False tdom prio queue) tdom prio queue\<rbrace> setQueue tdom prio (queue @ [t]) \<lbrace>\<lambda>rv. valid_queues' and obj_at' (\<lambda>obj. \<not> tcbQueued obj) t and obj_at' (\<lambda>obj. tcbPriority obj = prio) t and obj_at' (\<lambda>obj. tcbDomain obj = tdom) t and (\<lambda>s. t \<in> set (ksReadyQueues s (tdom, prio)))\<rbrace>
 2. \<And>queued tdom prio. \<not> queued \<Longrightarrow> \<lbrace>?B18 queued tdom prio\<rbrace> getQueue tdom prio \<lbrace>\<lambda>queue. ?B65 queued tdom prio queue (?queued65 queued tdom prio queue) tdom prio queue\<rbrace>
 3. \<And>queued tdom. \<not> queued \<Longrightarrow> \<lbrace>?B17 queued tdom\<rbrace> threadGet tcbPriority t \<lbrace>?B18 queued tdom\<rbrace>
 4. \<And>queued. \<not> queued \<Longrightarrow> \<lbrace>?Q16 queued\<rbrace> threadGet tcbDomain t \<lbrace>?B17 queued\<rbrace>
 5. \<And>queued s. \<lbrakk>\<not> queued; (valid_queues' and obj_at' (\<lambda>obj. \<not> tcbQueued obj) t) s\<rbrakk> \<Longrightarrow> ?Q16 queued s
 6. \<lbrace>?Q\<rbrace> threadGet tcbQueued t \<lbrace>\<lambda>rv. valid_queues' and obj_at' (\<lambda>obj. tcbQueued obj = rv) t\<rbrace>
 7. \<And>s. (valid_queues' and tcb_at' t) s \<Longrightarrow> ?Q s proof (prove)
goal (5 subgoals):
 1. \<And>queued tdom. \<not> queued \<Longrightarrow> \<lbrace>?P'151 (ds_id False) tdom\<rbrace> threadGet tcbPriority t \<lbrace>\<lambda>rv s. (\<forall>ta. obj_at' (inQ tdom rv) ta s \<longrightarrow> ta = t \<or> ta \<in> set (ksReadyQueues s (tdom, rv))) \<and> obj_at' (\<lambda>a. \<not> tcbQueued a) t s \<and> obj_at' (\<lambda>a. tcbPriority a = rv) t s \<and> obj_at' (\<lambda>a. tcbDomain a = tdom) t s\<rbrace>
 2. \<And>queued. \<not> queued \<Longrightarrow> \<lbrace>?Q16 queued\<rbrace> threadGet tcbDomain t \<lbrace>\<lambda>a b. valid_queues' b \<and> ?P'151 queued a b\<rbrace>
 3. \<And>queued s. \<lbrakk>\<not> queued; (valid_queues' and obj_at' (\<lambda>obj. \<not> tcbQueued obj) t) s\<rbrakk> \<Longrightarrow> ?Q16 queued s
 4. \<lbrace>?Q\<rbrace> threadGet tcbQueued t \<lbrace>\<lambda>rv. valid_queues' and obj_at' (\<lambda>obj. tcbQueued obj = rv) t\<rbrace>
 5. \<And>s. (valid_queues' and tcb_at' t) s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>queued s. \<lbrakk>\<not> queued; valid_queues' s \<and> obj_at' (\<lambda>obj. \<not> tcbQueued obj) t s\<rbrakk> \<Longrightarrow> tcb_at' t s \<longrightarrow> (\<exists>ta. ko_at' ta t s \<and> (\<exists>tb. ko_at' tb t s \<and> (\<forall>tc. obj_at' (inQ (tcbDomain ta) (tcbPriority tb)) tc s \<longrightarrow> tc = t \<or> tc \<in> set (ksReadyQueues s (tcbDomain ta, tcbPriority tb))) \<and> obj_at' (\<lambda>a. tcbPriority a = tcbPriority tb) t s \<and> obj_at' (\<lambda>a. tcbDomain a = tcbDomain ta) t s))
 2. \<lbrace>?Q\<rbrace> threadGet tcbQueued t \<lbrace>\<lambda>rv. valid_queues' and obj_at' (\<lambda>obj. tcbQueued obj = rv) t\<rbrace>
 3. \<And>s. (valid_queues' and tcb_at' t) s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<rbrace> threadGet tcbQueued t \<lbrace>\<lambda>rv. valid_queues' and obj_at' (\<lambda>obj. tcbQueued obj = rv) t\<rbrace>
 2. \<And>s. (valid_queues' and tcb_at' t) s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. valid_queues' s \<and> tcb_at' t s \<Longrightarrow> \<exists>ta. ko_at' ta t s \<and> obj_at' (\<lambda>obj. tcbQueued obj = tcbQueued ta) t s proof (prove)
goal:
No subgoals!