theory Schedule_R

lemma tcbSchedDequeue_valid_queues'[wp]:
  "\<lbrace>valid_queues' and tcb_at' t\<rbrace>
    tcbSchedDequeue t \<lbrace>\<lambda>_. valid_queues'\<rbrace>" unfolding tcbSchedDequeue_def apply (rule_tac B="\<lambda>rv. valid_queues' and obj_at' (\<lambda>obj. tcbQueued obj = rv) t"
                in hoare_seq_ext) prefer 2 apply (wp threadGet_const_tcb_at) apply (fastforce simp: obj_at'_def) apply clarsimp apply (rename_tac queued) apply (case_tac queued, simp_all) apply wp apply (rule_tac d=tdom and p=prio in threadSet_valid_queues'_dequeue) apply (rule hoare_pre_post, assumption) apply (wp | clarsimp simp: bitmap_fun_defs)+ apply (wp hoare_vcg_all_lift setQueue_ksReadyQueues_lift) apply clarsimp apply (wp threadGet_obj_at' threadGet_const_tcb_at)+ apply clarsimp apply (rule context_conjI, clarsimp simp: obj_at'_def) apply (clarsimp simp: valid_queues'_def obj_at'_def projectKOs inQ_def|wp)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_queues' and tcb_at' t\<rbrace> tcbSchedDequeue 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;
when queued $ do tdom <- threadGet tcbDomain t;
prio <- threadGet tcbPriority t;
queue <- getQueue tdom prio;
queue' <- return (filter (\<lambda>x. x \<noteq> t) queue);
setQueue tdom prio queue';
when (null queue') $ removeFromBitmap tdom prio;
threadSet (tcbQueued_update (\<lambda>_. False)) t
od
od \<lbrace>\<lambda>_. valid_queues'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>x. \<lbrace>valid_queues' and obj_at' (\<lambda>obj. tcbQueued obj = x) t\<rbrace> when x $ do tdom <- threadGet tcbDomain t;
prio <- threadGet tcbPriority t;
queue <- getQueue tdom prio;
queue' <- return (filter (\<lambda>x. x \<noteq> t) queue);
setQueue tdom prio queue';
when (null queue') $ removeFromBitmap tdom prio;
threadSet (tcbQueued_update (\<lambda>_. False)) t
od \<lbrace>\<lambda>_. valid_queues'\<rbrace>
 2. \<lbrace>valid_queues' and tcb_at' t\<rbrace> threadGet tcbQueued t \<lbrace>\<lambda>rv. valid_queues' and obj_at' (\<lambda>obj. tcbQueued obj = rv) t\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<lbrace>valid_queues' and tcb_at' t\<rbrace> threadGet tcbQueued t \<lbrace>\<lambda>rv. valid_queues' and obj_at' (\<lambda>obj. tcbQueued obj = rv) t\<rbrace>
 2. \<And>x. \<lbrace>valid_queues' and obj_at' (\<lambda>obj. tcbQueued obj = x) t\<rbrace> when x $ do tdom <- threadGet tcbDomain t;
prio <- threadGet tcbPriority t;
queue <- getQueue tdom prio;
queue' <- return (filter (\<lambda>x. x \<noteq> t) queue);
setQueue tdom prio queue';
when (null queue') $ removeFromBitmap tdom prio;
threadSet (tcbQueued_update (\<lambda>_. False)) t
od \<lbrace>\<lambda>_. valid_queues'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>s. (valid_queues' and tcb_at' t) s \<Longrightarrow> tcb_at' t s \<and> obj_at' ((\<lambda>rv. (valid_queues' and obj_at' (\<lambda>obj. tcbQueued obj = rv) t) s) \<circ> tcbQueued) t s
 2. \<And>x. \<lbrace>valid_queues' and obj_at' (\<lambda>obj. tcbQueued obj = x) t\<rbrace> when x $ do tdom <- threadGet tcbDomain t;
prio <- threadGet tcbPriority t;
queue <- getQueue tdom prio;
queue' <- return (filter (\<lambda>x. x \<noteq> t) queue);
setQueue tdom prio queue';
when (null queue') $ removeFromBitmap tdom prio;
threadSet (tcbQueued_update (\<lambda>_. False)) t
od \<lbrace>\<lambda>_. valid_queues'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrace>valid_queues' and obj_at' (\<lambda>obj. tcbQueued obj = x) t\<rbrace> when x $ do tdom <- threadGet tcbDomain t;
prio <- threadGet tcbPriority t;
queue <- getQueue tdom prio;
queue' <- return (filter (\<lambda>x. x \<noteq> t) queue);
setQueue tdom prio queue';
when (null queue') $ removeFromBitmap tdom prio;
threadSet (tcbQueued_update (\<lambda>_. False)) t
od \<lbrace>\<lambda>_. valid_queues'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>x. \<lbrace>valid_queues' and obj_at' (\<lambda>obj. tcbQueued obj = x) t\<rbrace> when x (do tdom <- threadGet tcbDomain t;
prio <- threadGet tcbPriority t;
queue <- getQueue tdom prio;
y <- setQueue tdom prio (filter (\<lambda>x. x \<noteq> t) queue);
y <- when (null (filter (\<lambda>x. x \<noteq> t) queue)) (removeFromBitmap tdom prio);
threadSet (tcbQueued_update (\<lambda>_. False)) t
od) \<lbrace>\<lambda>_. valid_queues'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>queued. \<lbrace>valid_queues' and obj_at' (\<lambda>obj. tcbQueued obj = queued) t\<rbrace> when queued (do tdom <- threadGet tcbDomain t;
prio <- threadGet tcbPriority t;
queue <- getQueue tdom prio;
y <- setQueue tdom prio (filter (\<lambda>x. x \<noteq> t) queue);
y <- when (null (filter (\<lambda>x. x \<noteq> t) queue)) (removeFromBitmap tdom prio);
threadSet (tcbQueued_update (\<lambda>_. False)) t
od) \<lbrace>\<lambda>_. valid_queues'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>queued. queued \<Longrightarrow> \<lbrace>valid_queues' and obj_at' tcbQueued t\<rbrace> do tdom <- threadGet tcbDomain t;
prio <- threadGet tcbPriority t;
queue <- getQueue tdom prio;
y <- setQueue tdom prio (filter (\<lambda>x. x \<noteq> t) queue);
y <- when (null (filter (\<lambda>x. x \<noteq> t) queue)) (removeFromBitmap tdom prio);
threadSet (tcbQueued_update (\<lambda>_. False)) t
od \<lbrace>\<lambda>_. valid_queues'\<rbrace>
 2. \<And>queued. \<not> queued \<Longrightarrow> \<lbrace>valid_queues' and obj_at' (\<lambda>obj. \<not> tcbQueued obj) t\<rbrace> return () \<lbrace>\<lambda>_. valid_queues'\<rbrace> proof (prove)
goal (8 subgoals):
 1. \<And>queued tdom prio queue y ya. queued \<Longrightarrow> \<lbrace>?B21 queued tdom prio queue y ya\<rbrace> threadSet (tcbQueued_update (\<lambda>_. False)) t \<lbrace>\<lambda>_. valid_queues'\<rbrace>
 2. \<And>queued tdom prio queue y. queued \<Longrightarrow> \<lbrace>?B20 queued tdom prio queue y\<rbrace> when (null (filter (\<lambda>x. x \<noteq> t) queue)) (removeFromBitmap tdom prio) \<lbrace>?B21 queued tdom prio queue y\<rbrace>
 3. \<And>queued tdom prio queue. queued \<Longrightarrow> \<lbrace>?B19 queued tdom prio queue\<rbrace> setQueue tdom prio (filter (\<lambda>x. x \<noteq> t) queue) \<lbrace>?B20 queued tdom prio queue\<rbrace>
 4. \<And>queued tdom prio. queued \<Longrightarrow> \<lbrace>?B18 queued tdom prio\<rbrace> getQueue tdom prio \<lbrace>?B19 queued tdom prio\<rbrace>
 5. \<And>queued tdom. queued \<Longrightarrow> \<lbrace>?B17 queued tdom\<rbrace> threadGet tcbPriority t \<lbrace>?B18 queued tdom\<rbrace>
 6. \<And>queued. queued \<Longrightarrow> \<lbrace>?Q16 queued\<rbrace> threadGet tcbDomain t \<lbrace>?B17 queued\<rbrace>
 7. \<And>queued s. \<lbrakk>queued; (valid_queues' and obj_at' tcbQueued t) s\<rbrakk> \<Longrightarrow> ?Q16 queued s
 8. \<And>queued. \<not> queued \<Longrightarrow> \<lbrace>valid_queues' and obj_at' (\<lambda>obj. \<not> tcbQueued obj) t\<rbrace> return () \<lbrace>\<lambda>_. valid_queues'\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>queued tdom prio queue y. queued \<Longrightarrow> \<lbrace>?B20 queued tdom prio queue y\<rbrace> when (null (filter (\<lambda>x. x \<noteq> t) queue)) (removeFromBitmap tdom prio) \<lbrace>\<lambda>ya s. (\<forall>d p t'. obj_at' (inQ d p) t' s \<and> t' \<noteq> t \<longrightarrow> t' \<in> set (ksReadyQueues s (d, p))) \<and> obj_at' (inQ tdom prio) t s\<rbrace>
 2. \<And>queued tdom prio queue. queued \<Longrightarrow> \<lbrace>?B19 queued tdom prio queue\<rbrace> setQueue tdom prio (filter (\<lambda>x. x \<noteq> t) queue) \<lbrace>?B20 queued tdom prio queue\<rbrace>
 3. \<And>queued tdom prio. queued \<Longrightarrow> \<lbrace>?B18 queued tdom prio\<rbrace> getQueue tdom prio \<lbrace>?B19 queued tdom prio\<rbrace>
 4. \<And>queued tdom. queued \<Longrightarrow> \<lbrace>?B17 queued tdom\<rbrace> threadGet tcbPriority t \<lbrace>?B18 queued tdom\<rbrace>
 5. \<And>queued. queued \<Longrightarrow> \<lbrace>?Q16 queued\<rbrace> threadGet tcbDomain t \<lbrace>?B17 queued\<rbrace>
 6. \<And>queued s. \<lbrakk>queued; (valid_queues' and obj_at' tcbQueued t) s\<rbrakk> \<Longrightarrow> ?Q16 queued s
 7. \<And>queued. \<not> queued \<Longrightarrow> \<lbrace>valid_queues' and obj_at' (\<lambda>obj. \<not> tcbQueued obj) t\<rbrace> return () \<lbrace>\<lambda>_. valid_queues'\<rbrace> proof (prove)
goal (7 subgoals):
 1. \<And>queued tdom prio queue y. queued \<Longrightarrow> \<lbrace>\<lambda>s. (\<forall>d p t'. obj_at' (inQ d p) t' s \<and> t' \<noteq> t \<longrightarrow> t' \<in> set (ksReadyQueues s (d, p))) \<and> obj_at' (inQ tdom prio) t s\<rbrace> when (null (filter (\<lambda>x. x \<noteq> t) queue)) (removeFromBitmap tdom prio) \<lbrace>\<lambda>ya s. (\<forall>d p t'. obj_at' (inQ d p) t' s \<and> t' \<noteq> t \<longrightarrow> t' \<in> set (ksReadyQueues s (d, p))) \<and> obj_at' (inQ tdom prio) t s\<rbrace>
 2. \<And>queued tdom prio queue. queued \<Longrightarrow> \<lbrace>?B19 queued tdom prio queue\<rbrace> setQueue tdom prio (filter (\<lambda>x. x \<noteq> t) queue) \<lbrace>\<lambda>y s. (\<forall>d p t'. obj_at' (inQ d p) t' s \<and> t' \<noteq> t \<longrightarrow> t' \<in> set (ksReadyQueues s (d, p))) \<and> obj_at' (inQ tdom prio) t s\<rbrace>
 3. \<And>queued tdom prio. queued \<Longrightarrow> \<lbrace>?B18 queued tdom prio\<rbrace> getQueue tdom prio \<lbrace>?B19 queued tdom prio\<rbrace>
 4. \<And>queued tdom. queued \<Longrightarrow> \<lbrace>?B17 queued tdom\<rbrace> threadGet tcbPriority t \<lbrace>?B18 queued tdom\<rbrace>
 5. \<And>queued. queued \<Longrightarrow> \<lbrace>?Q16 queued\<rbrace> threadGet tcbDomain t \<lbrace>?B17 queued\<rbrace>
 6. \<And>queued s. \<lbrakk>queued; (valid_queues' and obj_at' tcbQueued t) s\<rbrakk> \<Longrightarrow> ?Q16 queued s
 7. \<And>queued. \<not> queued \<Longrightarrow> \<lbrace>valid_queues' and obj_at' (\<lambda>obj. \<not> tcbQueued obj) t\<rbrace> return () \<lbrace>\<lambda>_. valid_queues'\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>queued tdom prio queue. queued \<Longrightarrow> \<lbrace>?B19 True tdom prio queue\<rbrace> setQueue tdom prio (filter (\<lambda>x. x \<noteq> t) queue) \<lbrace>\<lambda>y s. (\<forall>d p t'. obj_at' (inQ d p) t' s \<and> t' \<noteq> t \<longrightarrow> t' \<in> set (ksReadyQueues s (d, p))) \<and> obj_at' (inQ tdom prio) t s\<rbrace>
 2. \<And>queued tdom prio. queued \<Longrightarrow> \<lbrace>?B18 queued tdom prio\<rbrace> getQueue tdom prio \<lbrace>?B19 queued tdom prio\<rbrace>
 3. \<And>queued tdom. queued \<Longrightarrow> \<lbrace>?B17 queued tdom\<rbrace> threadGet tcbPriority t \<lbrace>?B18 queued tdom\<rbrace>
 4. \<And>queued. queued \<Longrightarrow> \<lbrace>?Q16 queued\<rbrace> threadGet tcbDomain t \<lbrace>?B17 queued\<rbrace>
 5. \<And>queued s. \<lbrakk>queued; (valid_queues' and obj_at' tcbQueued t) s\<rbrakk> \<Longrightarrow> ?Q16 queued s
 6. \<And>queued. \<not> queued \<Longrightarrow> \<lbrace>valid_queues' and obj_at' (\<lambda>obj. \<not> tcbQueued obj) t\<rbrace> return () \<lbrace>\<lambda>_. valid_queues'\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>queued tdom prio. queued \<Longrightarrow> \<lbrace>?B18 queued tdom prio\<rbrace> getQueue tdom prio \<lbrace>\<lambda>a b. (\<forall>x xa xb. obj_at' (inQ x xa) xb (b\<lparr>ksReadyQueues := (ksReadyQueues b)((tdom, prio) := filter (\<lambda>x. x \<noteq> t) a)\<rparr>) \<and> xb \<noteq> t \<longrightarrow> xb \<in> set (ksReadyQueues (b\<lparr>ksReadyQueues := (ksReadyQueues b)((tdom, prio) := filter (\<lambda>x. x \<noteq> t) a)\<rparr>) (x, xa))) \<and> obj_at' (inQ tdom prio) t (b\<lparr>ksReadyQueues := (ksReadyQueues b)((tdom, prio) := filter (\<lambda>x. x \<noteq> t) a)\<rparr>)\<rbrace>
 2. \<And>queued tdom. queued \<Longrightarrow> \<lbrace>?B17 queued tdom\<rbrace> threadGet tcbPriority t \<lbrace>?B18 queued tdom\<rbrace>
 3. \<And>queued. queued \<Longrightarrow> \<lbrace>?Q16 queued\<rbrace> threadGet tcbDomain t \<lbrace>?B17 queued\<rbrace>
 4. \<And>queued s. \<lbrakk>queued; (valid_queues' and obj_at' tcbQueued t) s\<rbrakk> \<Longrightarrow> ?Q16 queued s
 5. \<And>queued. \<not> queued \<Longrightarrow> \<lbrace>valid_queues' and obj_at' (\<lambda>obj. \<not> tcbQueued obj) t\<rbrace> return () \<lbrace>\<lambda>_. valid_queues'\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>queued tdom prio. queued \<Longrightarrow> \<lbrace>?B18 True tdom prio\<rbrace> getQueue tdom prio \<lbrace>\<lambda>x xa. (\<forall>xb xc. (xb = tdom \<and> xc = prio \<longrightarrow> (\<forall>xb. obj_at' (inQ tdom prio) xb xa \<and> xb \<noteq> t \<longrightarrow> xb \<in> set x)) \<and> ((xb = tdom \<longrightarrow> xc \<noteq> prio) \<longrightarrow> (\<forall>x. obj_at' (inQ xb xc) x xa \<and> x \<noteq> t \<longrightarrow> x \<in> set (ksReadyQueues xa (xb, xc))))) \<and> obj_at' (inQ tdom prio) t xa\<rbrace>
 2. \<And>queued tdom. queued \<Longrightarrow> \<lbrace>?B17 queued tdom\<rbrace> threadGet tcbPriority t \<lbrace>?B18 queued tdom\<rbrace>
 3. \<And>queued. queued \<Longrightarrow> \<lbrace>?Q16 queued\<rbrace> threadGet tcbDomain t \<lbrace>?B17 queued\<rbrace>
 4. \<And>queued s. \<lbrakk>queued; (valid_queues' and obj_at' tcbQueued t) s\<rbrakk> \<Longrightarrow> ?Q16 queued s
 5. \<And>queued. \<not> queued \<Longrightarrow> \<lbrace>valid_queues' and obj_at' (\<lambda>obj. \<not> tcbQueued obj) t\<rbrace> return () \<lbrace>\<lambda>_. valid_queues'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>queued s. \<lbrakk>queued; (valid_queues' and obj_at' tcbQueued t) s\<rbrakk> \<Longrightarrow> tcb_at' t s \<and> tcb_at' t s \<and> obj_at' ((\<lambda>rv. obj_at' ((\<lambda>rva. (\<forall>x xa. (x = rv \<and> xa = rva \<longrightarrow> (\<forall>x. obj_at' (inQ rv rva) x s \<and> x \<noteq> t \<longrightarrow> x \<in> set (ksReadyQueues s (rv, rva)))) \<and> ((x = rv \<longrightarrow> xa \<noteq> rva) \<longrightarrow> (\<forall>xb. obj_at' (inQ x xa) xb s \<and> xb \<noteq> t \<longrightarrow> xb \<in> set (ksReadyQueues s (x, xa))))) \<and> obj_at' (inQ rv rva) t s) \<circ> tcbPriority) t s) \<circ> tcbDomain) t s
 2. \<And>queued. \<not> queued \<Longrightarrow> \<lbrace>valid_queues' and obj_at' (\<lambda>obj. \<not> tcbQueued obj) t\<rbrace> return () \<lbrace>\<lambda>_. valid_queues'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>queued s. \<lbrakk>queued; valid_queues' s; obj_at' tcbQueued t s\<rbrakk> \<Longrightarrow> tcb_at' t s \<and> obj_at' ((\<lambda>rv. obj_at' ((\<lambda>rva. (\<forall>x xa. (x = rv \<and> xa = rva \<longrightarrow> (\<forall>x. obj_at' (inQ rv rva) x s \<and> x \<noteq> t \<longrightarrow> x \<in> set (ksReadyQueues s (rv, rva)))) \<and> ((x = rv \<longrightarrow> xa \<noteq> rva) \<longrightarrow> (\<forall>xb. obj_at' (inQ x xa) xb s \<and> xb \<noteq> t \<longrightarrow> xb \<in> set (ksReadyQueues s (x, xa))))) \<and> obj_at' (inQ rv rva) t s) \<circ> tcbPriority) t s) \<circ> tcbDomain) t s
 2. \<And>queued. \<not> queued \<Longrightarrow> \<lbrace>valid_queues' and obj_at' (\<lambda>obj. \<not> tcbQueued obj) t\<rbrace> return () \<lbrace>\<lambda>_. valid_queues'\<rbrace> proof (prove)
goal (2 subgoals):
 1. \<And>queued s. \<lbrakk>queued; valid_queues' s; obj_at' tcbQueued t s; tcb_at' t s\<rbrakk> \<Longrightarrow> obj_at' ((\<lambda>rv. obj_at' ((\<lambda>rva. (\<forall>x xa. (x = rv \<and> xa = rva \<longrightarrow> (\<forall>x. obj_at' (inQ rv rva) x s \<and> x \<noteq> t \<longrightarrow> x \<in> set (ksReadyQueues s (rv, rva)))) \<and> ((x = rv \<longrightarrow> xa \<noteq> rva) \<longrightarrow> (\<forall>xb. obj_at' (inQ x xa) xb s \<and> xb \<noteq> t \<longrightarrow> xb \<in> set (ksReadyQueues s (x, xa))))) \<and> obj_at' (inQ rv rva) t s) \<circ> tcbPriority) t s) \<circ> tcbDomain) t s
 2. \<And>queued. \<not> queued \<Longrightarrow> \<lbrace>valid_queues' and obj_at' (\<lambda>obj. \<not> tcbQueued obj) t\<rbrace> return () \<lbrace>\<lambda>_. valid_queues'\<rbrace> proof (prove)
goal:
No subgoals!