theory TcbAcc_R

lemma tcbSchedEnqueueOrAppend_valid_queues:
  (* f is either (t#ts) or (ts @ [t]), so we define its properties generally *)
  assumes f_set[simp]: "\<And>ts. t \<in> set (f ts)"
  assumes f_set_insert[simp]: "\<And>ts. set (f ts) = insert t (set ts)"
  assumes f_not_empty[simp]: "\<And>ts. f ts \<noteq> []"
  assumes f_distinct: "\<And>ts. \<lbrakk> distinct ts ; t \<notin> set ts \<rbrakk> \<Longrightarrow> distinct (f ts)"
  shows "\<lbrace>Invariants_H.valid_queues and st_tcb_at' runnable' t and valid_objs' \<rbrace>
    do queued \<leftarrow> threadGet tcbQueued t;
       unless queued $
       do tdom \<leftarrow> threadGet tcbDomain t;
          prio \<leftarrow> threadGet tcbPriority t;
          queue \<leftarrow> getQueue tdom prio;
          setQueue tdom prio $ f queue;
          when (null queue) $ addToBitmap tdom prio;
          threadSet (tcbQueued_update (\<lambda>_. True)) t
       od
    od
   \<lbrace>\<lambda>_. Invariants_H.valid_queues\<rbrace>" proof - define could_run where "could_run ==
    \<lambda>d p t. obj_at' (\<lambda>tcb. inQ d p (tcbQueued_update (\<lambda>_. True) tcb) \<and> runnable' (tcbState tcb)) t" have addToBitmap_could_run:
  "\<And>d p. \<lbrace>\<lambda>s. \<forall>d p. t \<in> set (ksReadyQueues s (d, p)) \<longrightarrow> could_run d p t s\<rbrace>
         addToBitmap d p
         \<lbrace>\<lambda>_ s. \<forall>d p. t \<in> set (ksReadyQueues s (d, p)) \<longrightarrow> could_run d p t s\<rbrace>" unfolding bitmap_fun_defs by (wp, clarsimp simp: could_run_def) have setQueue_valid_queues_no_bitmap_except:
    "\<And>d p ts.
     \<lbrace> valid_queues_no_bitmap_except t and
       (\<lambda>s. ksReadyQueues s (d, p) = ts \<and> p \<le> maxPriority \<and> d \<le> maxDomain \<and> t \<notin> set ts) \<rbrace>
         setQueue d p (f ts)
     \<lbrace>\<lambda>rv. valid_queues_no_bitmap_except t\<rbrace>" unfolding setQueue_def valid_queues_no_bitmap_except_def null_def by (wp, auto intro: f_distinct) have threadSet_valid_queues_could_run:
   "\<And>f. \<lbrace> valid_queues_no_bitmap_except t and
          (\<lambda>s. \<forall>d p. t \<in> set (ksReadyQueues s (d,p)) \<longrightarrow> could_run d p t s) and
          valid_bitmapQ and bitmapQ_no_L2_orphans and bitmapQ_no_L1_orphans \<rbrace>
            threadSet (tcbQueued_update (\<lambda>_. True)) t
         \<lbrace>\<lambda>rv. Invariants_H.valid_queues \<rbrace>" unfolding threadSet_def could_run_def apply (rule hoare_seq_ext[OF _ getObject_tcb_sp]) apply (rule hoare_pre) apply (simp add: valid_queues_def valid_queues_no_bitmap_def) apply (wp setObject_queues_unchanged_tcb hoare_Ball_helper hoare_vcg_all_lift
               setObject_tcb_strongest) apply (clarsimp simp: valid_queues_no_bitmap_except_def obj_at'_def) done have setQueue_could_run: "\<And>d p ts.
    \<lbrace> valid_queues and (\<lambda>_. t \<in> set ts) and
      (\<lambda>s. could_run d p t s) \<rbrace>
    setQueue d p ts
    \<lbrace>\<lambda>rv s. (\<forall>d p. t \<in> set (ksReadyQueues s (d, p)) \<longrightarrow> could_run d p t s)\<rbrace>" unfolding setQueue_def valid_queues_def could_run_def by wp (fastforce dest: valid_queues_no_bitmap_objD simp: obj_at'_def inQ_def) note hoare_vcg_if_lift[wp] hoare_vcg_conj_lift[wp] hoare_vcg_const_imp_lift[wp] show ?thesis unfolding tcbSchedEnqueue_def null_def apply (rule hoare_pre) apply (rule hoare_seq_ext) apply (simp add: unless_def) apply (wp threadSet_valid_queues_could_run) apply (wp addToBitmap_could_run addToBitmap_valid_bitmapQ
                  addToBitmap_valid_queues_no_bitmap_except addToBitmap_bitmapQ_no_L2_orphans)+ apply (wp setQueue_valid_queues_no_bitmap_except setQueue_could_run
                 setQueue_valid_bitmapQ_except setQueue_sets_queue setQueue_valid_bitmapQ)+ apply (wp threadGet_const_tcb_at_imp_lift | simp add: if_apply_def2)+ apply clarsimp apply (frule pred_tcb_at') apply (frule (1) valid_objs'_maxDomain) apply (frule (1) valid_objs'_maxPriority) apply (clarsimp simp: valid_queues_def st_tcb_at'_def obj_at'_def valid_queues_no_bitmap_exceptI) apply (fastforce dest!: valid_queues_no_bitmap_objD simp: obj_at'_def inQ_def could_run_def) done qed

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>Invariants_H.valid_queues and st_tcb_at' runnable' t and valid_objs'\<rbrace> do queued <- threadGet tcbQueued t;
unless queued $ do tdom <- threadGet tcbDomain t;
prio <- threadGet tcbPriority t;
queue <- getQueue tdom prio;
setQueue tdom prio $ f queue;
when (null queue) $ addToBitmap tdom prio;
threadSet (tcbQueued_update (\<lambda>_. True)) t
od
od \<lbrace>\<lambda>_. Invariants_H.valid_queues\<rbrace> proof (state)
goal (1 subgoal):
 1. \<lbrace>Invariants_H.valid_queues and st_tcb_at' runnable' t and valid_objs'\<rbrace> do queued <- threadGet tcbQueued t;
unless queued $ do tdom <- threadGet tcbDomain t;
prio <- threadGet tcbPriority t;
queue <- getQueue tdom prio;
setQueue tdom prio $ f queue;
when (null queue) $ addToBitmap tdom prio;
threadSet (tcbQueued_update (\<lambda>_. True)) t
od
od \<lbrace>\<lambda>_. Invariants_H.valid_queues\<rbrace> proof (state)
this:
could_run \<equiv> \<lambda>d p. obj_at' (\<lambda>tcb. inQ d p (tcbQueued_update (\<lambda>_. True) tcb) \<and> runnable' (tcbState tcb))

goal (1 subgoal):
 1. \<lbrace>Invariants_H.valid_queues and st_tcb_at' runnable' t and valid_objs'\<rbrace> do queued <- threadGet tcbQueued t;
unless queued $ do tdom <- threadGet tcbDomain t;
prio <- threadGet tcbPriority t;
queue <- getQueue tdom prio;
setQueue tdom prio $ f queue;
when (null queue) $ addToBitmap tdom prio;
threadSet (tcbQueued_update (\<lambda>_. True)) t
od
od \<lbrace>\<lambda>_. Invariants_H.valid_queues\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>d p. \<lbrace>\<lambda>s. \<forall>d p. t \<in> set (ksReadyQueues s (d, p)) \<longrightarrow> could_run d p t s\<rbrace> addToBitmap d p \<lbrace>\<lambda>_ s. \<forall>d p. t \<in> set (ksReadyQueues s (d, p)) \<longrightarrow> could_run d p t s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>d p. \<lbrace>\<lambda>s. \<forall>d p. t \<in> set (ksReadyQueues s (d, p)) \<longrightarrow> could_run d p t s\<rbrace> do l1index <- return (prioToL1Index p);
l1indexInverted <- return (invertL1Index l1index);
l2bit <- return (fromIntegral (fromIntegral p && mask wordRadix));
do l1 <- gets (\<lambda>ks. ksReadyQueuesL1Bitmap ks d);
modify (\<lambda>ks. ks\<lparr>ksReadyQueuesL1Bitmap := ksReadyQueuesL1Bitmap ks aLU [(d, l1 || HaskellLib_H.bit l1index)]\<rparr>)
od;
l2 <- gets (\<lambda>ks. ksReadyQueuesL2Bitmap ks (d, l1indexInverted));
modify (\<lambda>ks. ks\<lparr>ksReadyQueuesL2Bitmap := ksReadyQueuesL2Bitmap ks aLU [((d, l1indexInverted), l2 || HaskellLib_H.bit l2bit)]\<rparr>)
od \<lbrace>\<lambda>_ s. \<forall>d p. t \<in> set (ksReadyQueues s (d, p)) \<longrightarrow> could_run d p t s\<rbrace> proof (state)
this:
\<lbrace>\<lambda>s. \<forall>d p. t \<in> set (ksReadyQueues s (d, p)) \<longrightarrow> could_run d p t s\<rbrace> addToBitmap ?d ?p \<lbrace>\<lambda>_ s. \<forall>d p. t \<in> set (ksReadyQueues s (d, p)) \<longrightarrow> could_run d p t s\<rbrace>

goal (1 subgoal):
 1. \<lbrace>Invariants_H.valid_queues and st_tcb_at' runnable' t and valid_objs'\<rbrace> do queued <- threadGet tcbQueued t;
unless queued $ do tdom <- threadGet tcbDomain t;
prio <- threadGet tcbPriority t;
queue <- getQueue tdom prio;
setQueue tdom prio $ f queue;
when (null queue) $ addToBitmap tdom prio;
threadSet (tcbQueued_update (\<lambda>_. True)) t
od
od \<lbrace>\<lambda>_. Invariants_H.valid_queues\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>d p ts. \<lbrace>valid_queues_no_bitmap_except t and (\<lambda>s. ksReadyQueues s (d, p) = ts \<and> p \<le> maxPriority \<and> d \<le> maxDomain \<and> t \<notin> set ts)\<rbrace> setQueue d p (f ts) \<lbrace>\<lambda>rv. valid_queues_no_bitmap_except t\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>d p ts. \<lbrace>(\<lambda>s. \<forall>d p. (\<forall>ta\<in>set (ksReadyQueues s (d, p)). ta \<noteq> t \<longrightarrow> obj_at' (inQ d p and runnable' \<circ> tcbState) ta s) \<and> distinct (ksReadyQueues s (d, p)) \<and> (maxDomain < d \<or> maxPriority < p \<longrightarrow> ksReadyQueues s (d, p) = [])) and (\<lambda>s. ksReadyQueues s (d, p) = ts \<and> p \<le> maxPriority \<and> d \<le> maxDomain \<and> t \<notin> set ts)\<rbrace> modify (\<lambda>ks. ks\<lparr>ksReadyQueues := ksReadyQueues ks aLU [((d, p), f ts)]\<rparr>) \<lbrace>\<lambda>rv s. \<forall>d p. (\<forall>ta\<in>set (ksReadyQueues s (d, p)). ta \<noteq> t \<longrightarrow> obj_at' (inQ d p and runnable' \<circ> tcbState) ta s) \<and> distinct (ksReadyQueues s (d, p)) \<and> (maxDomain < d \<or> maxPriority < p \<longrightarrow> ksReadyQueues s (d, p) = [])\<rbrace> proof (state)
this:
\<lbrace>valid_queues_no_bitmap_except t and (\<lambda>s. ksReadyQueues s (?d, ?p) = ?ts \<and> ?p \<le> maxPriority \<and> ?d \<le> maxDomain \<and> t \<notin> set ?ts)\<rbrace> setQueue ?d ?p (f ?ts) \<lbrace>\<lambda>rv. valid_queues_no_bitmap_except t\<rbrace>

goal (1 subgoal):
 1. \<lbrace>Invariants_H.valid_queues and st_tcb_at' runnable' t and valid_objs'\<rbrace> do queued <- threadGet tcbQueued t;
unless queued $ do tdom <- threadGet tcbDomain t;
prio <- threadGet tcbPriority t;
queue <- getQueue tdom prio;
setQueue tdom prio $ f queue;
when (null queue) $ addToBitmap tdom prio;
threadSet (tcbQueued_update (\<lambda>_. True)) t
od
od \<lbrace>\<lambda>_. Invariants_H.valid_queues\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>f. \<lbrace>valid_queues_no_bitmap_except t and (\<lambda>s. \<forall>d p. t \<in> set (ksReadyQueues s (d, p)) \<longrightarrow> could_run d p t s) and valid_bitmapQ and bitmapQ_no_L2_orphans and bitmapQ_no_L1_orphans\<rbrace> threadSet (tcbQueued_update (\<lambda>_. True)) t \<lbrace>\<lambda>rv. Invariants_H.valid_queues\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>f. \<lbrace>valid_queues_no_bitmap_except t and (\<lambda>s. \<forall>d p. t \<in> set (ksReadyQueues s (d, p)) \<longrightarrow> obj_at' (\<lambda>tcb. inQ d p (tcbQueued_update (\<lambda>_. True) tcb) \<and> runnable' (tcbState tcb)) t s) and valid_bitmapQ and bitmapQ_no_L2_orphans and bitmapQ_no_L1_orphans\<rbrace> do tcb <- getObject t;
setObject t $ tcbQueued_update (\<lambda>_. True) tcb
od \<lbrace>\<lambda>rv. Invariants_H.valid_queues\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>f tcb. \<lbrace>valid_queues_no_bitmap_except t and (\<lambda>s. \<forall>d p. t \<in> set (ksReadyQueues s (d, p)) \<longrightarrow> obj_at' (\<lambda>tcb. inQ d p (tcbQueued_update (\<lambda>_. True) tcb) \<and> runnable' (tcbState tcb)) t s) and valid_bitmapQ and bitmapQ_no_L2_orphans and bitmapQ_no_L1_orphans and ko_at' tcb t\<rbrace> setObject t $ tcbQueued_update (\<lambda>_. True) tcb \<lbrace>\<lambda>rv. Invariants_H.valid_queues\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>f tcb. \<lbrace>?Q4 f tcb\<rbrace> setObject t $ tcbQueued_update (\<lambda>_. True) tcb \<lbrace>\<lambda>rv. Invariants_H.valid_queues\<rbrace>
 2. \<And>f tcb s. (valid_queues_no_bitmap_except t and (\<lambda>s. \<forall>d p. t \<in> set (ksReadyQueues s (d, p)) \<longrightarrow> obj_at' (\<lambda>tcb. inQ d p (tcbQueued_update (\<lambda>_. True) tcb) \<and> runnable' (tcbState tcb)) t s) and valid_bitmapQ and bitmapQ_no_L2_orphans and bitmapQ_no_L1_orphans and ko_at' tcb t) s \<Longrightarrow> ?Q4 f tcb s proof (prove)
goal (2 subgoals):
 1. \<And>f tcb. \<lbrace>?Q4 f tcb\<rbrace> setObject t (tcbQueued_update (\<lambda>_. True) tcb) \<lbrace>\<lambda>rv s. (\<forall>d p. (\<forall>t\<in>set (ksReadyQueues s (d, p)). obj_at' (inQ d p and runnable' \<circ> tcbState) t s) \<and> distinct (ksReadyQueues s (d, p)) \<and> (maxDomain < d \<longrightarrow> ksReadyQueues s (d, p) = []) \<and> (maxPriority < p \<longrightarrow> ksReadyQueues s (d, p) = [])) \<and> valid_bitmapQ s \<and> bitmapQ_no_L2_orphans s \<and> bitmapQ_no_L1_orphans s\<rbrace>
 2. \<And>f tcb s. (valid_queues_no_bitmap_except t and (\<lambda>s. \<forall>d p. t \<in> set (ksReadyQueues s (d, p)) \<longrightarrow> obj_at' (\<lambda>tcb. inQ d p (tcbQueued_update (\<lambda>_. True) tcb) \<and> runnable' (tcbState tcb)) t s) and valid_bitmapQ and bitmapQ_no_L2_orphans and bitmapQ_no_L1_orphans and ko_at' tcb t) s \<Longrightarrow> ?Q4 f tcb s proof (prove)
goal (1 subgoal):
 1. \<And>f tcb s. (valid_queues_no_bitmap_except t and (\<lambda>s. \<forall>d p. t \<in> set (ksReadyQueues s (d, p)) \<longrightarrow> obj_at' (\<lambda>tcb. inQ d p (tcbQueued_update (\<lambda>_. True) tcb) \<and> runnable' (tcbState tcb)) t s) and valid_bitmapQ and bitmapQ_no_L2_orphans and bitmapQ_no_L1_orphans and ko_at' tcb t) s \<Longrightarrow> (\<forall>x xa. (\<forall>xb\<in>set (ksReadyQueues s (x, xa)). if t = xb then (inQ x xa and runnable' \<circ> tcbState) (tcbQueued_update (\<lambda>_. True) tcb) else obj_at' (inQ x xa and runnable' \<circ> tcbState) xb s) \<and> distinct (ksReadyQueues s (x, xa)) \<and> (maxDomain < x \<longrightarrow> ksReadyQueues s (x, xa) = []) \<and> (maxPriority < xa \<longrightarrow> ksReadyQueues s (x, xa) = [])) \<and> valid_bitmapQ s \<and> bitmapQ_no_L2_orphans s \<and> bitmapQ_no_L1_orphans s proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrace>valid_queues_no_bitmap_except t and (\<lambda>s. \<forall>d p. t \<in> set (ksReadyQueues s (d, p)) \<longrightarrow> could_run d p t s) and valid_bitmapQ and bitmapQ_no_L2_orphans and bitmapQ_no_L1_orphans\<rbrace> threadSet (tcbQueued_update (\<lambda>_. True)) t \<lbrace>\<lambda>rv. Invariants_H.valid_queues\<rbrace>

goal (1 subgoal):
 1. \<lbrace>Invariants_H.valid_queues and st_tcb_at' runnable' t and valid_objs'\<rbrace> do queued <- threadGet tcbQueued t;
unless queued $ do tdom <- threadGet tcbDomain t;
prio <- threadGet tcbPriority t;
queue <- getQueue tdom prio;
setQueue tdom prio $ f queue;
when (null queue) $ addToBitmap tdom prio;
threadSet (tcbQueued_update (\<lambda>_. True)) t
od
od \<lbrace>\<lambda>_. Invariants_H.valid_queues\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>d p ts. \<lbrace>Invariants_H.valid_queues and (\<lambda>_. t \<in> set ts) and could_run d p t\<rbrace> setQueue d p ts \<lbrace>\<lambda>rv s. \<forall>d p. t \<in> set (ksReadyQueues s (d, p)) \<longrightarrow> could_run d p t s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>d p ts. \<lbrace>(\<lambda>s. valid_queues_no_bitmap s \<and> valid_bitmapQ s \<and> bitmapQ_no_L2_orphans s \<and> bitmapQ_no_L1_orphans s) and (\<lambda>_. t \<in> set ts) and obj_at' (\<lambda>tcb. inQ d p (tcbQueued_update (\<lambda>_. True) tcb) \<and> runnable' (tcbState tcb)) t\<rbrace> modify (\<lambda>ks. ks\<lparr>ksReadyQueues := ksReadyQueues ks aLU [((d, p), ts)]\<rparr>) \<lbrace>\<lambda>rv s. \<forall>d p. t \<in> set (ksReadyQueues s (d, p)) \<longrightarrow> obj_at' (\<lambda>tcb. inQ d p (tcbQueued_update (\<lambda>_. True) tcb) \<and> runnable' (tcbState tcb)) t s\<rbrace> proof (state)
this:
\<lbrace>Invariants_H.valid_queues and (\<lambda>_. t \<in> set ?ts1) and could_run ?d1 ?p1 t\<rbrace> setQueue ?d1 ?p1 ?ts1 \<lbrace>\<lambda>rv s. \<forall>d p. t \<in> set (ksReadyQueues s (d, p)) \<longrightarrow> could_run d p t s\<rbrace>

goal (1 subgoal):
 1. \<lbrace>Invariants_H.valid_queues and st_tcb_at' runnable' t and valid_objs'\<rbrace> do queued <- threadGet tcbQueued t;
unless queued $ do tdom <- threadGet tcbDomain t;
prio <- threadGet tcbPriority t;
queue <- getQueue tdom prio;
setQueue tdom prio $ f queue;
when (null queue) $ addToBitmap tdom prio;
threadSet (tcbQueued_update (\<lambda>_. True)) t
od
od \<lbrace>\<lambda>_. Invariants_H.valid_queues\<rbrace> proof (state)
this:
\<lbrace>?R\<rbrace> ?f \<lbrace>\<lambda>rv s. (?P \<longrightarrow> ?X rv s) \<and> (\<not> ?P \<longrightarrow> ?Y rv s)\<rbrace> \<Longrightarrow> \<lbrace>?R\<rbrace> ?f \<lbrace>\<lambda>rv s. if ?P then ?X rv s else ?Y rv s\<rbrace>
\<lbrace>?R\<rbrace> ?f \<lbrace>\<lambda>rv s. (?P \<longrightarrow> ?X rv s) \<and> (\<not> ?P \<longrightarrow> ?Y rv s)\<rbrace> \<Longrightarrow> \<lbrace>?R\<rbrace> ?f \<lbrace>\<lambda>rv. if ?P then ?X rv else ?Y rv\<rbrace>
\<lbrakk>\<lbrace>?P\<rbrace> ?f \<lbrace>?Q\<rbrace>; \<lbrace>?P'\<rbrace> ?f \<lbrace>?Q'\<rbrace>\<rbrakk> \<Longrightarrow> \<lbrace>\<lambda>s. ?P s \<and> ?P' s\<rbrace> ?f \<lbrace>\<lambda>rv s. ?Q rv s \<and> ?Q' rv s\<rbrace>
(?P \<Longrightarrow> \<lbrace>?Q\<rbrace> ?m \<lbrace>?R\<rbrace>) \<Longrightarrow> \<lbrace>\<lambda>s. ?P \<longrightarrow> ?Q s\<rbrace> ?m \<lbrace>\<lambda>rv s. ?P \<longrightarrow> ?R rv s\<rbrace>

goal (1 subgoal):
 1. \<lbrace>Invariants_H.valid_queues and st_tcb_at' runnable' t and valid_objs'\<rbrace> do queued <- threadGet tcbQueued t;
unless queued $ do tdom <- threadGet tcbDomain t;
prio <- threadGet tcbPriority t;
queue <- getQueue tdom prio;
setQueue tdom prio $ f queue;
when (null queue) $ addToBitmap tdom prio;
threadSet (tcbQueued_update (\<lambda>_. True)) t
od
od \<lbrace>\<lambda>_. Invariants_H.valid_queues\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>Invariants_H.valid_queues and st_tcb_at' runnable' t and valid_objs'\<rbrace> do queued <- threadGet tcbQueued t;
unless queued $ do tdom <- threadGet tcbDomain t;
prio <- threadGet tcbPriority t;
queue <- getQueue tdom prio;
setQueue tdom prio $ f queue;
when (null queue) $ addToBitmap tdom prio;
threadSet (tcbQueued_update (\<lambda>_. True)) t
od
od \<lbrace>\<lambda>_. Invariants_H.valid_queues\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>Invariants_H.valid_queues and st_tcb_at' runnable' t and valid_objs'\<rbrace> do queued <- threadGet tcbQueued t;
unless queued $ do tdom <- threadGet tcbDomain t;
prio <- threadGet tcbPriority t;
queue <- getQueue tdom prio;
setQueue tdom prio $ f queue;
when (queue = []) $ addToBitmap tdom prio;
threadSet (tcbQueued_update (\<lambda>_. True)) t
od
od \<lbrace>\<lambda>_. Invariants_H.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;
setQueue tdom prio $ f queue;
when (queue = []) $ addToBitmap tdom prio;
threadSet (tcbQueued_update (\<lambda>_. True)) t
od
od \<lbrace>\<lambda>_. Invariants_H.valid_queues\<rbrace>
 2. \<And>s. (Invariants_H.valid_queues and st_tcb_at' runnable' t and valid_objs') s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>queued. \<lbrace>?B3 queued\<rbrace> unless queued $ do tdom <- threadGet tcbDomain t;
prio <- threadGet tcbPriority t;
queue <- getQueue tdom prio;
setQueue tdom prio $ f queue;
when (queue = []) $ addToBitmap tdom prio;
threadSet (tcbQueued_update (\<lambda>_. True)) t
od \<lbrace>\<lambda>_. Invariants_H.valid_queues\<rbrace>
 2. \<lbrace>?Q\<rbrace> threadGet tcbQueued t \<lbrace>?B3\<rbrace>
 3. \<And>s. (Invariants_H.valid_queues and st_tcb_at' runnable' t and valid_objs') s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>queued. \<lbrace>?B3 queued\<rbrace> when (\<not> queued) (do tdom <- threadGet tcbDomain t;
prio <- threadGet tcbPriority t;
queue <- getQueue tdom prio;
y <- setQueue tdom prio (f queue);
y <- when (queue = []) (addToBitmap tdom prio);
threadSet (tcbQueued_update (\<lambda>_. True)) t
od) \<lbrace>\<lambda>_. Invariants_H.valid_queues\<rbrace>
 2. \<lbrace>?Q\<rbrace> threadGet tcbQueued t \<lbrace>?B3\<rbrace>
 3. \<And>s. (Invariants_H.valid_queues and st_tcb_at' runnable' t and valid_objs') s \<Longrightarrow> ?Q s proof (prove)
goal (11 subgoals):
 1. \<And>queued tdom prio queue y. \<lbrakk>\<not> queued; queue = []\<rbrakk> \<Longrightarrow> \<lbrace>?Q21 queued tdom prio queue y\<rbrace> addToBitmap tdom prio \<lbrace>\<lambda>rv. valid_queues_no_bitmap_except t\<rbrace>
 2. \<And>queued tdom prio queue y. \<not> queued \<Longrightarrow> \<lbrace>?P'20 queued tdom prio queue y\<rbrace> when (queue = []) (addToBitmap tdom prio) \<lbrace>\<lambda>rv s. \<forall>d p. t \<in> set (ksReadyQueues s (d, p)) \<longrightarrow> could_run d p t s\<rbrace>
 3. \<And>queued tdom prio queue y. \<not> queued \<Longrightarrow> \<lbrace>?P'18 queued tdom prio queue y\<rbrace> when (queue = []) (addToBitmap tdom prio) \<lbrace>\<lambda>rv. valid_bitmapQ\<rbrace>
 4. \<And>queued tdom prio queue y. \<not> queued \<Longrightarrow> \<lbrace>?P'16 queued tdom prio queue y\<rbrace> when (queue = []) (addToBitmap tdom prio) \<lbrace>\<lambda>rv. bitmapQ_no_L2_orphans\<rbrace>
 5. \<And>queued tdom prio queue y. \<not> queued \<Longrightarrow> \<lbrace>?P'14 queued tdom prio queue y\<rbrace> when (queue = []) (addToBitmap tdom prio) \<lbrace>\<lambda>rv. bitmapQ_no_L1_orphans\<rbrace>
 6. \<And>queued tdom prio queue. \<not> queued \<Longrightarrow> \<lbrace>?B10 queued tdom prio queue\<rbrace> setQueue tdom prio (f queue) \<lbrace>\<lambda>y s. ((((if queue = [] then ?Q21 queued tdom prio queue y else valid_queues_no_bitmap_except t) s \<and> ?P'20 queued tdom prio queue y s) \<and> ?P'18 queued tdom prio queue y s) \<and> ?P'16 queued tdom prio queue y s) \<and> ?P'14 queued tdom prio queue y s\<rbrace>
 7. \<And>queued tdom prio. \<not> queued \<Longrightarrow> \<lbrace>?B9 queued tdom prio\<rbrace> getQueue tdom prio \<lbrace>?B10 queued tdom prio\<rbrace>
 8. \<And>queued tdom. \<not> queued \<Longrightarrow> \<lbrace>?B8 queued tdom\<rbrace> threadGet tcbPriority t \<lbrace>?B9 queued tdom\<rbrace>
 9. \<And>queued. \<not> queued \<Longrightarrow> \<lbrace>?Q7 queued\<rbrace> threadGet tcbDomain t \<lbrace>?B8 queued\<rbrace>
 10. \<lbrace>?Q\<rbrace> threadGet tcbQueued t \<lbrace>\<lambda>queued. if \<not> queued then ?Q7 queued else Invariants_H.valid_queues\<rbrace>
A total of 11 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>queued tdom prio queue. \<lbrakk>\<not> queued; queue = []\<rbrakk> \<Longrightarrow> \<lbrace>?Q49 queued tdom prio queue\<rbrace> setQueue tdom prio (f queue) \<lbrace>\<lambda>rv. valid_queues_no_bitmap_except t\<rbrace>
 2. \<And>queued tdom prio queue. \<not> queued \<Longrightarrow> \<lbrace>?P'48 queued tdom prio queue\<rbrace> setQueue tdom prio (f queue) \<lbrace>\<lambda>rv s. queue \<noteq> [] \<longrightarrow> valid_queues_no_bitmap_except t s\<rbrace>
 3. \<And>queued tdom prio queue. \<not> queued \<Longrightarrow> \<lbrace>?P'46 queued tdom prio queue\<rbrace> setQueue tdom prio (f queue) \<lbrace>\<lambda>rv. if queue = [] then \<lambda>s. \<forall>d p. t \<in> set (ksReadyQueues s (d, p)) \<longrightarrow> could_run d p t s else (\<lambda>s. \<forall>d p. t \<in> set (ksReadyQueues s (d, p)) \<longrightarrow> could_run d p t s)\<rbrace>
 4. \<And>queued tdom prio queue. \<not> queued \<Longrightarrow> \<lbrace>?P'45 queued tdom prio queue\<rbrace> setQueue tdom prio (f queue) \<lbrace>\<lambda>rv. if queue = [] then valid_bitmapQ_except tdom prio and bitmapQ_no_L2_orphans and (\<lambda>s. ksReadyQueues s (tdom, prio) \<noteq> []) else valid_bitmapQ\<rbrace>
 5. \<And>queued tdom prio queue. \<not> queued \<Longrightarrow> \<lbrace>?P'44 queued tdom prio queue\<rbrace> setQueue tdom prio (f queue) \<lbrace>\<lambda>rv. if queue = [] then bitmapQ_no_L2_orphans else bitmapQ_no_L2_orphans\<rbrace>
 6. \<And>queued tdom prio queue. \<not> queued \<Longrightarrow> \<lbrace>?P'43 queued tdom prio queue\<rbrace> setQueue tdom prio (f queue) \<lbrace>\<lambda>rv. if queue = [] then bitmapQ_no_L1_orphans else bitmapQ_no_L1_orphans\<rbrace>
 7. \<And>queued tdom prio. \<not> queued \<Longrightarrow> \<lbrace>?B9 queued tdom prio\<rbrace> getQueue tdom prio \<lbrace>\<lambda>queue s. (((((queue = [] \<longrightarrow> ?Q49 queued tdom prio queue s) \<and> ?P'48 queued tdom prio queue s) \<and> ?P'46 queued tdom prio queue s) \<and> ?P'45 queued tdom prio queue s) \<and> ?P'44 queued tdom prio queue s) \<and> ?P'43 queued tdom prio queue s\<rbrace>
 8. \<And>queued tdom. \<not> queued \<Longrightarrow> \<lbrace>?B8 queued tdom\<rbrace> threadGet tcbPriority t \<lbrace>?B9 queued tdom\<rbrace>
 9. \<And>queued. \<not> queued \<Longrightarrow> \<lbrace>?Q7 queued\<rbrace> threadGet tcbDomain t \<lbrace>?B8 queued\<rbrace>
 10. \<lbrace>?Q\<rbrace> threadGet tcbQueued t \<lbrace>\<lambda>queued. if \<not> queued then ?Q7 queued else Invariants_H.valid_queues\<rbrace>
A total of 11 subgoals... proof (prove)
goal (9 subgoals):
 1. \<And>queued tdom. \<not> queued \<Longrightarrow> \<lbrace>?P124 queued tdom\<rbrace> threadGet tcbPriority t \<lbrace>\<lambda>rv s. ksReadyQueues s (tdom, rv) = [] \<longrightarrow> (valid_queues_no_bitmap_except t and (\<lambda>sa. ksReadyQueues sa (tdom, rv) = ksReadyQueues s (tdom, rv) \<and> rv \<le> maxPriority \<and> tdom \<le> maxDomain \<and> t \<notin> set (ksReadyQueues s (tdom, rv)))) s\<rbrace>
 2. \<And>queued tdom. \<not> queued \<Longrightarrow> \<lbrace>?P'124 queued tdom\<rbrace> threadGet tcbPriority t \<lbrace>\<lambda>rv s. ksReadyQueues s (tdom, rv) \<noteq> [] \<longrightarrow> (valid_queues_no_bitmap_except t and (\<lambda>sa. ksReadyQueues sa (tdom, rv) = ksReadyQueues s (tdom, rv) \<and> rv \<le> maxPriority \<and> tdom \<le> maxDomain \<and> t \<notin> set (ksReadyQueues s (tdom, rv)))) s\<rbrace>
 3. \<And>queued tdom. \<not> queued \<Longrightarrow> \<lbrace>?P'123 queued tdom\<rbrace> threadGet tcbPriority t \<lbrace>\<lambda>rv s. (ksReadyQueues s (tdom, rv) = [] \<longrightarrow> (Invariants_H.valid_queues and (\<lambda>_. t \<in> set (f (ksReadyQueues s (tdom, rv)))) and could_run tdom rv t) s) \<and> (ksReadyQueues s (tdom, rv) \<noteq> [] \<longrightarrow> (Invariants_H.valid_queues and (\<lambda>_. t \<in> set (f (ksReadyQueues s (tdom, rv)))) and could_run tdom rv t) s)\<rbrace>
 4. \<And>queued tdom. \<not> queued \<Longrightarrow> \<lbrace>?P'122 queued tdom\<rbrace> threadGet tcbPriority t \<lbrace>\<lambda>rv s. (ksReadyQueues s (tdom, rv) = [] \<longrightarrow> (valid_bitmapQ_except tdom rv s \<and> bitmapQ_no_L2_orphans s) \<and> f (ksReadyQueues s (tdom, rv)) \<noteq> []) \<and> (ksReadyQueues s (tdom, rv) \<noteq> [] \<longrightarrow> (valid_bitmapQ and (\<lambda>sa. (ksReadyQueues sa (tdom, rv) = []) = (f (ksReadyQueues s (tdom, rv)) = []))) s)\<rbrace>
 5. \<And>queued tdom. \<not> queued \<Longrightarrow> \<lbrace>?P'121 queued tdom\<rbrace> threadGet tcbPriority t \<lbrace>\<lambda>rv s. (ksReadyQueues s (tdom, rv) = [] \<longrightarrow> bitmapQ_no_L2_orphans s) \<and> (ksReadyQueues s (tdom, rv) \<noteq> [] \<longrightarrow> bitmapQ_no_L2_orphans s)\<rbrace>
 6. \<And>queued tdom. \<not> queued \<Longrightarrow> \<lbrace>?P'120 queued tdom\<rbrace> threadGet tcbPriority t \<lbrace>\<lambda>rv s. (ksReadyQueues s (tdom, rv) = [] \<longrightarrow> bitmapQ_no_L1_orphans s) \<and> (ksReadyQueues s (tdom, rv) \<noteq> [] \<longrightarrow> bitmapQ_no_L1_orphans s)\<rbrace>
 7. \<And>queued. \<not> queued \<Longrightarrow> \<lbrace>?Q7 queued\<rbrace> threadGet tcbDomain t \<lbrace>\<lambda>tdom s. ((((?P124 queued tdom s \<and> ?P'124 queued tdom s) \<and> ?P'123 queued tdom s) \<and> ?P'122 queued tdom s) \<and> ?P'121 queued tdom s) \<and> ?P'120 queued tdom s\<rbrace>
 8. \<lbrace>?Q\<rbrace> threadGet tcbQueued t \<lbrace>\<lambda>queued. if \<not> queued then ?Q7 queued else Invariants_H.valid_queues\<rbrace>
 9. \<And>s. (Invariants_H.valid_queues and st_tcb_at' runnable' t and valid_objs') s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. Invariants_H.valid_queues s \<and> st_tcb_at' runnable' t s \<and> valid_objs' s \<Longrightarrow> tcb_at' t s \<and> obj_at' (Not \<circ> tcbQueued) t s \<longrightarrow> obj_at' (\<lambda>rv. (obj_at' ((\<lambda>rv. obj_at' ((\<lambda>rva. ksReadyQueues s (rv, rva) = []) \<circ> tcbPriority) t s) \<circ> tcbDomain) t s \<longrightarrow> obj_at' ((\<lambda>rv. obj_at' ((\<lambda>rva. valid_queues_no_bitmap_except t s \<and> rva \<le> maxPriority \<and> rv \<le> maxDomain \<and> t \<notin> set (ksReadyQueues s (rv, rva))) \<circ> tcbPriority) t s) \<circ> tcbDomain) t s) \<and> (obj_at' ((\<lambda>rv. obj_at' ((\<lambda>rva. ksReadyQueues s (rv, rva) \<noteq> []) \<circ> tcbPriority) t s) \<circ> tcbDomain) t s \<longrightarrow> obj_at' ((\<lambda>rv. obj_at' ((\<lambda>rva. valid_queues_no_bitmap_except t s \<and> rva \<le> maxPriority \<and> rv \<le> maxDomain \<and> t \<notin> set (ksReadyQueues s (rv, rva))) \<circ> tcbPriority) t s) \<circ> tcbDomain) t s) \<and> (obj_at' ((\<lambda>rv. obj_at' ((\<lambda>rva. ksReadyQueues s (rv, rva) = []) \<circ> tcbPriority) t s) \<circ> tcbDomain) t s \<longrightarrow> obj_at' ((\<lambda>rv. obj_at' ((\<lambda>rva. could_run rv rva t s) \<circ> tcbPriority) t s) \<circ> tcbDomain) t s) \<and> (obj_at' ((\<lambda>rv. obj_at' ((\<lambda>rva. ksReadyQueues s (rv, rva) \<noteq> []) \<circ> tcbPriority) t s) \<circ> tcbDomain) t s \<longrightarrow> obj_at' ((\<lambda>rv. obj_at' ((\<lambda>rva. could_run rv rva t s) \<circ> tcbPriority) t s) \<circ> tcbDomain) t s) \<and> (obj_at' ((\<lambda>rv. obj_at' ((\<lambda>rva. ksReadyQueues s (rv, rva) = []) \<circ> tcbPriority) t s) \<circ> tcbDomain) t s \<longrightarrow> obj_at' ((\<lambda>rv. obj_at' ((\<lambda>rva. valid_bitmapQ_except rv rva s \<and> bitmapQ_no_L2_orphans s) \<circ> tcbPriority) t s) \<circ> tcbDomain) t s) \<and> (obj_at' ((\<lambda>rv. obj_at' ((\<lambda>rva. ksReadyQueues s (rv, rva) \<noteq> []) \<circ> tcbPriority) t s) \<circ> tcbDomain) t s \<longrightarrow> obj_at' ((\<lambda>rv. obj_at' ((\<lambda>rva. valid_bitmapQ s \<and> ksReadyQueues s (rv, rva) \<noteq> []) \<circ> tcbPriority) t s) \<circ> tcbDomain) t s) \<and> (obj_at' ((\<lambda>rv. obj_at' ((\<lambda>rva. ksReadyQueues s (rv, rva) = []) \<circ> tcbPriority) t s) \<circ> tcbDomain) t s \<longrightarrow> obj_at' (\<lambda>rv. obj_at' (\<lambda>rv. bitmapQ_no_L2_orphans s) t s) t s) \<and> (obj_at' ((\<lambda>rv. obj_at' ((\<lambda>rva. ksReadyQueues s (rv, rva) \<noteq> []) \<circ> tcbPriority) t s) \<circ> tcbDomain) t s \<longrightarrow> obj_at' (\<lambda>rv. obj_at' (\<lambda>rv. bitmapQ_no_L2_orphans s) t s) t s) \<and> (obj_at' ((\<lambda>rv. obj_at' ((\<lambda>rva. ksReadyQueues s (rv, rva) = []) \<circ> tcbPriority) t s) \<circ> tcbDomain) t s \<longrightarrow> obj_at' (\<lambda>rv. obj_at' (\<lambda>rv. bitmapQ_no_L1_orphans s) t s) t s) \<and> (obj_at' ((\<lambda>rv. obj_at' ((\<lambda>rva. ksReadyQueues s (rv, rva) \<noteq> []) \<circ> tcbPriority) t s) \<circ> tcbDomain) t s \<longrightarrow> obj_at' (\<lambda>rv. obj_at' (\<lambda>rv. bitmapQ_no_L1_orphans s) t s) t s)) t s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>Invariants_H.valid_queues s; st_tcb_at' runnable' t s; valid_objs' s; tcb_at' t s; obj_at' (Not \<circ> tcbQueued) t s\<rbrakk> \<Longrightarrow> obj_at' (\<lambda>rv. (obj_at' ((\<lambda>rv. obj_at' ((\<lambda>rva. ksReadyQueues s (rv, rva) = []) \<circ> tcbPriority) t s) \<circ> tcbDomain) t s \<longrightarrow> obj_at' ((\<lambda>rv. obj_at' ((\<lambda>rva. valid_queues_no_bitmap_except t s \<and> rva \<le> maxPriority \<and> rv \<le> maxDomain \<and> t \<notin> set (ksReadyQueues s (rv, rva))) \<circ> tcbPriority) t s) \<circ> tcbDomain) t s) \<and> (obj_at' ((\<lambda>rv. obj_at' ((\<lambda>rva. ksReadyQueues s (rv, rva) \<noteq> []) \<circ> tcbPriority) t s) \<circ> tcbDomain) t s \<longrightarrow> obj_at' ((\<lambda>rv. obj_at' ((\<lambda>rva. valid_queues_no_bitmap_except t s \<and> rva \<le> maxPriority \<and> rv \<le> maxDomain \<and> t \<notin> set (ksReadyQueues s (rv, rva))) \<circ> tcbPriority) t s) \<circ> tcbDomain) t s) \<and> (obj_at' ((\<lambda>rv. obj_at' ((\<lambda>rva. ksReadyQueues s (rv, rva) = []) \<circ> tcbPriority) t s) \<circ> tcbDomain) t s \<longrightarrow> obj_at' ((\<lambda>rv. obj_at' ((\<lambda>rva. could_run rv rva t s) \<circ> tcbPriority) t s) \<circ> tcbDomain) t s) \<and> (obj_at' ((\<lambda>rv. obj_at' ((\<lambda>rva. ksReadyQueues s (rv, rva) \<noteq> []) \<circ> tcbPriority) t s) \<circ> tcbDomain) t s \<longrightarrow> obj_at' ((\<lambda>rv. obj_at' ((\<lambda>rva. could_run rv rva t s) \<circ> tcbPriority) t s) \<circ> tcbDomain) t s) \<and> (obj_at' ((\<lambda>rv. obj_at' ((\<lambda>rva. ksReadyQueues s (rv, rva) = []) \<circ> tcbPriority) t s) \<circ> tcbDomain) t s \<longrightarrow> obj_at' ((\<lambda>rv. obj_at' ((\<lambda>rva. valid_bitmapQ_except rv rva s \<and> bitmapQ_no_L2_orphans s) \<circ> tcbPriority) t s) \<circ> tcbDomain) t s) \<and> (obj_at' ((\<lambda>rv. obj_at' ((\<lambda>rva. ksReadyQueues s (rv, rva) \<noteq> []) \<circ> tcbPriority) t s) \<circ> tcbDomain) t s \<longrightarrow> obj_at' ((\<lambda>rv. obj_at' ((\<lambda>rva. valid_bitmapQ s \<and> ksReadyQueues s (rv, rva) \<noteq> []) \<circ> tcbPriority) t s) \<circ> tcbDomain) t s) \<and> (obj_at' ((\<lambda>rv. obj_at' ((\<lambda>rva. ksReadyQueues s (rv, rva) = []) \<circ> tcbPriority) t s) \<circ> tcbDomain) t s \<longrightarrow> obj_at' (\<lambda>rv. obj_at' (\<lambda>rv. bitmapQ_no_L2_orphans s) t s) t s) \<and> (obj_at' ((\<lambda>rv. obj_at' ((\<lambda>rva. ksReadyQueues s (rv, rva) \<noteq> []) \<circ> tcbPriority) t s) \<circ> tcbDomain) t s \<longrightarrow> obj_at' (\<lambda>rv. obj_at' (\<lambda>rv. bitmapQ_no_L2_orphans s) t s) t s) \<and> (obj_at' ((\<lambda>rv. obj_at' ((\<lambda>rva. ksReadyQueues s (rv, rva) = []) \<circ> tcbPriority) t s) \<circ> tcbDomain) t s \<longrightarrow> obj_at' (\<lambda>rv. obj_at' (\<lambda>rv. bitmapQ_no_L1_orphans s) t s) t s) \<and> (obj_at' ((\<lambda>rv. obj_at' ((\<lambda>rva. ksReadyQueues s (rv, rva) \<noteq> []) \<circ> tcbPriority) t s) \<circ> tcbDomain) t s \<longrightarrow> obj_at' (\<lambda>rv. obj_at' (\<lambda>rv. bitmapQ_no_L1_orphans s) t s) t s)) t s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>Invariants_H.valid_queues s; st_tcb_at' runnable' t s; valid_objs' s; tcb_at' t s; obj_at' (Not \<circ> tcbQueued) t s; tcb_at' t s\<rbrakk> \<Longrightarrow> obj_at' (\<lambda>rv. (obj_at' ((\<lambda>rv. obj_at' ((\<lambda>rva. ksReadyQueues s (rv, rva) = []) \<circ> tcbPriority) t s) \<circ> tcbDomain) t s \<longrightarrow> obj_at' ((\<lambda>rv. obj_at' ((\<lambda>rva. valid_queues_no_bitmap_except t s \<and> rva \<le> maxPriority \<and> rv \<le> maxDomain \<and> t \<notin> set (ksReadyQueues s (rv, rva))) \<circ> tcbPriority) t s) \<circ> tcbDomain) t s) \<and> (obj_at' ((\<lambda>rv. obj_at' ((\<lambda>rva. ksReadyQueues s (rv, rva) \<noteq> []) \<circ> tcbPriority) t s) \<circ> tcbDomain) t s \<longrightarrow> obj_at' ((\<lambda>rv. obj_at' ((\<lambda>rva. valid_queues_no_bitmap_except t s \<and> rva \<le> maxPriority \<and> rv \<le> maxDomain \<and> t \<notin> set (ksReadyQueues s (rv, rva))) \<circ> tcbPriority) t s) \<circ> tcbDomain) t s) \<and> (obj_at' ((\<lambda>rv. obj_at' ((\<lambda>rva. ksReadyQueues s (rv, rva) = []) \<circ> tcbPriority) t s) \<circ> tcbDomain) t s \<longrightarrow> obj_at' ((\<lambda>rv. obj_at' ((\<lambda>rva. could_run rv rva t s) \<circ> tcbPriority) t s) \<circ> tcbDomain) t s) \<and> (obj_at' ((\<lambda>rv. obj_at' ((\<lambda>rva. ksReadyQueues s (rv, rva) \<noteq> []) \<circ> tcbPriority) t s) \<circ> tcbDomain) t s \<longrightarrow> obj_at' ((\<lambda>rv. obj_at' ((\<lambda>rva. could_run rv rva t s) \<circ> tcbPriority) t s) \<circ> tcbDomain) t s) \<and> (obj_at' ((\<lambda>rv. obj_at' ((\<lambda>rva. ksReadyQueues s (rv, rva) = []) \<circ> tcbPriority) t s) \<circ> tcbDomain) t s \<longrightarrow> obj_at' ((\<lambda>rv. obj_at' ((\<lambda>rva. valid_bitmapQ_except rv rva s \<and> bitmapQ_no_L2_orphans s) \<circ> tcbPriority) t s) \<circ> tcbDomain) t s) \<and> (obj_at' ((\<lambda>rv. obj_at' ((\<lambda>rva. ksReadyQueues s (rv, rva) \<noteq> []) \<circ> tcbPriority) t s) \<circ> tcbDomain) t s \<longrightarrow> obj_at' ((\<lambda>rv. obj_at' ((\<lambda>rva. valid_bitmapQ s \<and> ksReadyQueues s (rv, rva) \<noteq> []) \<circ> tcbPriority) t s) \<circ> tcbDomain) t s) \<and> (obj_at' ((\<lambda>rv. obj_at' ((\<lambda>rva. ksReadyQueues s (rv, rva) = []) \<circ> tcbPriority) t s) \<circ> tcbDomain) t s \<longrightarrow> obj_at' (\<lambda>rv. obj_at' (\<lambda>rv. bitmapQ_no_L2_orphans s) t s) t s) \<and> (obj_at' ((\<lambda>rv. obj_at' ((\<lambda>rva. ksReadyQueues s (rv, rva) \<noteq> []) \<circ> tcbPriority) t s) \<circ> tcbDomain) t s \<longrightarrow> obj_at' (\<lambda>rv. obj_at' (\<lambda>rv. bitmapQ_no_L2_orphans s) t s) t s) \<and> (obj_at' ((\<lambda>rv. obj_at' ((\<lambda>rva. ksReadyQueues s (rv, rva) = []) \<circ> tcbPriority) t s) \<circ> tcbDomain) t s \<longrightarrow> obj_at' (\<lambda>rv. obj_at' (\<lambda>rv. bitmapQ_no_L1_orphans s) t s) t s) \<and> (obj_at' ((\<lambda>rv. obj_at' ((\<lambda>rva. ksReadyQueues s (rv, rva) \<noteq> []) \<circ> tcbPriority) t s) \<circ> tcbDomain) t s \<longrightarrow> obj_at' (\<lambda>rv. obj_at' (\<lambda>rv. bitmapQ_no_L1_orphans s) t s) t s)) t s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>Invariants_H.valid_queues s; st_tcb_at' runnable' t s; valid_objs' s; tcb_at' t s; obj_at' (Not \<circ> tcbQueued) t s; tcb_at' t s; obj_at' (\<lambda>tcb. tcbDomain tcb \<le> maxDomain) t s\<rbrakk> \<Longrightarrow> obj_at' (\<lambda>rv. (obj_at' ((\<lambda>rv. obj_at' ((\<lambda>rva. ksReadyQueues s (rv, rva) = []) \<circ> tcbPriority) t s) \<circ> tcbDomain) t s \<longrightarrow> obj_at' ((\<lambda>rv. obj_at' ((\<lambda>rva. valid_queues_no_bitmap_except t s \<and> rva \<le> maxPriority \<and> rv \<le> maxDomain \<and> t \<notin> set (ksReadyQueues s (rv, rva))) \<circ> tcbPriority) t s) \<circ> tcbDomain) t s) \<and> (obj_at' ((\<lambda>rv. obj_at' ((\<lambda>rva. ksReadyQueues s (rv, rva) \<noteq> []) \<circ> tcbPriority) t s) \<circ> tcbDomain) t s \<longrightarrow> obj_at' ((\<lambda>rv. obj_at' ((\<lambda>rva. valid_queues_no_bitmap_except t s \<and> rva \<le> maxPriority \<and> rv \<le> maxDomain \<and> t \<notin> set (ksReadyQueues s (rv, rva))) \<circ> tcbPriority) t s) \<circ> tcbDomain) t s) \<and> (obj_at' ((\<lambda>rv. obj_at' ((\<lambda>rva. ksReadyQueues s (rv, rva) = []) \<circ> tcbPriority) t s) \<circ> tcbDomain) t s \<longrightarrow> obj_at' ((\<lambda>rv. obj_at' ((\<lambda>rva. could_run rv rva t s) \<circ> tcbPriority) t s) \<circ> tcbDomain) t s) \<and> (obj_at' ((\<lambda>rv. obj_at' ((\<lambda>rva. ksReadyQueues s (rv, rva) \<noteq> []) \<circ> tcbPriority) t s) \<circ> tcbDomain) t s \<longrightarrow> obj_at' ((\<lambda>rv. obj_at' ((\<lambda>rva. could_run rv rva t s) \<circ> tcbPriority) t s) \<circ> tcbDomain) t s) \<and> (obj_at' ((\<lambda>rv. obj_at' ((\<lambda>rva. ksReadyQueues s (rv, rva) = []) \<circ> tcbPriority) t s) \<circ> tcbDomain) t s \<longrightarrow> obj_at' ((\<lambda>rv. obj_at' ((\<lambda>rva. valid_bitmapQ_except rv rva s \<and> bitmapQ_no_L2_orphans s) \<circ> tcbPriority) t s) \<circ> tcbDomain) t s) \<and> (obj_at' ((\<lambda>rv. obj_at' ((\<lambda>rva. ksReadyQueues s (rv, rva) \<noteq> []) \<circ> tcbPriority) t s) \<circ> tcbDomain) t s \<longrightarrow> obj_at' ((\<lambda>rv. obj_at' ((\<lambda>rva. valid_bitmapQ s \<and> ksReadyQueues s (rv, rva) \<noteq> []) \<circ> tcbPriority) t s) \<circ> tcbDomain) t s) \<and> (obj_at' ((\<lambda>rv. obj_at' ((\<lambda>rva. ksReadyQueues s (rv, rva) = []) \<circ> tcbPriority) t s) \<circ> tcbDomain) t s \<longrightarrow> obj_at' (\<lambda>rv. obj_at' (\<lambda>rv. bitmapQ_no_L2_orphans s) t s) t s) \<and> (obj_at' ((\<lambda>rv. obj_at' ((\<lambda>rva. ksReadyQueues s (rv, rva) \<noteq> []) \<circ> tcbPriority) t s) \<circ> tcbDomain) t s \<longrightarrow> obj_at' (\<lambda>rv. obj_at' (\<lambda>rv. bitmapQ_no_L2_orphans s) t s) t s) \<and> (obj_at' ((\<lambda>rv. obj_at' ((\<lambda>rva. ksReadyQueues s (rv, rva) = []) \<circ> tcbPriority) t s) \<circ> tcbDomain) t s \<longrightarrow> obj_at' (\<lambda>rv. obj_at' (\<lambda>rv. bitmapQ_no_L1_orphans s) t s) t s) \<and> (obj_at' ((\<lambda>rv. obj_at' ((\<lambda>rva. ksReadyQueues s (rv, rva) \<noteq> []) \<circ> tcbPriority) t s) \<circ> tcbDomain) t s \<longrightarrow> obj_at' (\<lambda>rv. obj_at' (\<lambda>rv. bitmapQ_no_L1_orphans s) t s) t s)) t s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>Invariants_H.valid_queues s; st_tcb_at' runnable' t s; valid_objs' s; tcb_at' t s; obj_at' (Not \<circ> tcbQueued) t s; tcb_at' t s; obj_at' (\<lambda>tcb. tcbDomain tcb \<le> maxDomain) t s; obj_at' (\<lambda>tcb. tcbPriority tcb \<le> maxPriority) t s\<rbrakk> \<Longrightarrow> obj_at' (\<lambda>rv. (obj_at' ((\<lambda>rv. obj_at' ((\<lambda>rva. ksReadyQueues s (rv, rva) = []) \<circ> tcbPriority) t s) \<circ> tcbDomain) t s \<longrightarrow> obj_at' ((\<lambda>rv. obj_at' ((\<lambda>rva. valid_queues_no_bitmap_except t s \<and> rva \<le> maxPriority \<and> rv \<le> maxDomain \<and> t \<notin> set (ksReadyQueues s (rv, rva))) \<circ> tcbPriority) t s) \<circ> tcbDomain) t s) \<and> (obj_at' ((\<lambda>rv. obj_at' ((\<lambda>rva. ksReadyQueues s (rv, rva) \<noteq> []) \<circ> tcbPriority) t s) \<circ> tcbDomain) t s \<longrightarrow> obj_at' ((\<lambda>rv. obj_at' ((\<lambda>rva. valid_queues_no_bitmap_except t s \<and> rva \<le> maxPriority \<and> rv \<le> maxDomain \<and> t \<notin> set (ksReadyQueues s (rv, rva))) \<circ> tcbPriority) t s) \<circ> tcbDomain) t s) \<and> (obj_at' ((\<lambda>rv. obj_at' ((\<lambda>rva. ksReadyQueues s (rv, rva) = []) \<circ> tcbPriority) t s) \<circ> tcbDomain) t s \<longrightarrow> obj_at' ((\<lambda>rv. obj_at' ((\<lambda>rva. could_run rv rva t s) \<circ> tcbPriority) t s) \<circ> tcbDomain) t s) \<and> (obj_at' ((\<lambda>rv. obj_at' ((\<lambda>rva. ksReadyQueues s (rv, rva) \<noteq> []) \<circ> tcbPriority) t s) \<circ> tcbDomain) t s \<longrightarrow> obj_at' ((\<lambda>rv. obj_at' ((\<lambda>rva. could_run rv rva t s) \<circ> tcbPriority) t s) \<circ> tcbDomain) t s) \<and> (obj_at' ((\<lambda>rv. obj_at' ((\<lambda>rva. ksReadyQueues s (rv, rva) = []) \<circ> tcbPriority) t s) \<circ> tcbDomain) t s \<longrightarrow> obj_at' ((\<lambda>rv. obj_at' ((\<lambda>rva. valid_bitmapQ_except rv rva s \<and> bitmapQ_no_L2_orphans s) \<circ> tcbPriority) t s) \<circ> tcbDomain) t s) \<and> (obj_at' ((\<lambda>rv. obj_at' ((\<lambda>rva. ksReadyQueues s (rv, rva) \<noteq> []) \<circ> tcbPriority) t s) \<circ> tcbDomain) t s \<longrightarrow> obj_at' ((\<lambda>rv. obj_at' ((\<lambda>rva. valid_bitmapQ s \<and> ksReadyQueues s (rv, rva) \<noteq> []) \<circ> tcbPriority) t s) \<circ> tcbDomain) t s) \<and> (obj_at' ((\<lambda>rv. obj_at' ((\<lambda>rva. ksReadyQueues s (rv, rva) = []) \<circ> tcbPriority) t s) \<circ> tcbDomain) t s \<longrightarrow> obj_at' (\<lambda>rv. obj_at' (\<lambda>rv. bitmapQ_no_L2_orphans s) t s) t s) \<and> (obj_at' ((\<lambda>rv. obj_at' ((\<lambda>rva. ksReadyQueues s (rv, rva) \<noteq> []) \<circ> tcbPriority) t s) \<circ> tcbDomain) t s \<longrightarrow> obj_at' (\<lambda>rv. obj_at' (\<lambda>rv. bitmapQ_no_L2_orphans s) t s) t s) \<and> (obj_at' ((\<lambda>rv. obj_at' ((\<lambda>rva. ksReadyQueues s (rv, rva) = []) \<circ> tcbPriority) t s) \<circ> tcbDomain) t s \<longrightarrow> obj_at' (\<lambda>rv. obj_at' (\<lambda>rv. bitmapQ_no_L1_orphans s) t s) t s) \<and> (obj_at' ((\<lambda>rv. obj_at' ((\<lambda>rva. ksReadyQueues s (rv, rva) \<noteq> []) \<circ> tcbPriority) t s) \<circ> tcbDomain) t s \<longrightarrow> obj_at' (\<lambda>rv. obj_at' (\<lambda>rv. bitmapQ_no_L1_orphans s) t s) t s)) t s proof (prove)
goal (1 subgoal):
 1. \<And>s ko objc. \<lbrakk>valid_objs' s; valid_queues_no_bitmap s; ksPSpace s t = Some ko; valid_bitmapQ s; is_aligned t (objBitsKO ko); bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; fst (projectKO ko s) = {(objc, s)}; runnable' (tcbState objc); ps_clear t (objBitsKO ko) s; \<not> tcbQueued objc; tcbDomain objc \<le> maxDomain; tcbPriority objc \<le> maxPriority\<rbrakk> \<Longrightarrow> (ksReadyQueues s (tcbDomain objc, tcbPriority objc) \<noteq> [] \<longrightarrow> t \<notin> set (ksReadyQueues s (tcbDomain objc, tcbPriority objc))) \<and> (ksReadyQueues s (tcbDomain objc, tcbPriority objc) = [] \<longrightarrow> could_run (tcbDomain objc) (tcbPriority objc) t s) \<and> (ksReadyQueues s (tcbDomain objc, tcbPriority objc) \<noteq> [] \<longrightarrow> could_run (tcbDomain objc) (tcbPriority objc) t s) \<and> (ksReadyQueues s (tcbDomain objc, tcbPriority objc) = [] \<longrightarrow> valid_bitmapQ_except (tcbDomain objc) (tcbPriority objc) s) proof (prove)
goal:
No subgoals! proof (state)
this:
\<lbrace>Invariants_H.valid_queues and st_tcb_at' runnable' t and valid_objs'\<rbrace> do queued <- threadGet tcbQueued t;
unless queued $ do tdom <- threadGet tcbDomain t;
prio <- threadGet tcbPriority t;
queue <- getQueue tdom prio;
setQueue tdom prio $ f queue;
when (null queue) $ addToBitmap tdom prio;
threadSet (tcbQueued_update (\<lambda>_. True)) t
od
od \<lbrace>\<lambda>_. Invariants_H.valid_queues\<rbrace>

goal:
No subgoals!