theory Orphanage

lemma tcbSchedAppend_inQueue [wp]:
  "\<lbrace> \<lambda>s. valid_queues' s \<rbrace>
   tcbSchedAppend tcb_ptr
   \<lbrace> \<lambda>rv s. tcb_ptr \<in> all_queued_tcb_ptrs s \<rbrace>" unfolding tcbSchedAppend_def all_queued_tcb_ptrs_def apply (wp | clarsimp simp: unless_def)+ apply (rule_tac Q="\<lambda>rv. \<top>" in hoare_post_imp) apply fastforce apply (wp getObject_tcb_wp | clarsimp simp: threadGet_def)+ apply (fastforce simp: obj_at'_def valid_queues'_def inQ_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_queues'\<rbrace> tcbSchedAppend tcb_ptr \<lbrace>\<lambda>rv s. tcb_ptr \<in> all_queued_tcb_ptrs s\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_queues'\<rbrace> do queued <- threadGet tcbQueued tcb_ptr;
unless queued $ do tdom <- threadGet tcbDomain tcb_ptr;
prio <- threadGet tcbPriority tcb_ptr;
queue <- getQueue tdom prio;
setQueue tdom prio $ queue @ [tcb_ptr];
when (null queue) $ addToBitmap tdom prio;
threadSet (tcbQueued_update (\<lambda>_. True)) tcb_ptr
od
od \<lbrace>\<lambda>rv s. tcb_ptr \<in> {tcb_ptr. \<exists>priority. tcb_ptr \<in> set (ksReadyQueues s priority)}\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>queued tdom. \<not> queued \<Longrightarrow> \<lbrace>?B4 False tdom\<rbrace> threadGet tcbPriority tcb_ptr \<lbrace>\<lambda>prio s. \<exists>a b. (a = tdom \<longrightarrow> b \<noteq> prio) \<longrightarrow> tcb_ptr \<in> set (ksReadyQueues s (a, b))\<rbrace>
 2. \<And>queued. \<not> queued \<Longrightarrow> \<lbrace>?Q3 queued\<rbrace> threadGet tcbDomain tcb_ptr \<lbrace>?B4 queued\<rbrace>
 3. \<lbrace>?Q\<rbrace> threadGet tcbQueued tcb_ptr \<lbrace>\<lambda>queued. if queued then \<lambda>s. tcb_ptr \<in> {tcb_ptr. \<exists>priority. tcb_ptr \<in> set (ksReadyQueues s priority)} else ?Q3 queued\<rbrace>
 4. \<And>s. valid_queues' s \<Longrightarrow> ?Q s proof (prove)
goal (5 subgoals):
 1. \<And>queued tdom rv s. \<lbrakk>\<not> queued; True\<rbrakk> \<Longrightarrow> \<exists>a b. (a = tdom \<longrightarrow> b \<noteq> rv) \<longrightarrow> tcb_ptr \<in> set (ksReadyQueues s (a, b))
 2. \<And>queued tdom. \<not> queued \<Longrightarrow> \<lbrace>?B4 False tdom\<rbrace> threadGet tcbPriority tcb_ptr \<lbrace>\<lambda>rv _. True\<rbrace>
 3. \<And>queued. \<not> queued \<Longrightarrow> \<lbrace>?Q3 queued\<rbrace> threadGet tcbDomain tcb_ptr \<lbrace>?B4 queued\<rbrace>
 4. \<lbrace>?Q\<rbrace> threadGet tcbQueued tcb_ptr \<lbrace>\<lambda>queued. if queued then \<lambda>s. tcb_ptr \<in> {tcb_ptr. \<exists>priority. tcb_ptr \<in> set (ksReadyQueues s priority)} else ?Q3 queued\<rbrace>
 5. \<And>s. valid_queues' s \<Longrightarrow> ?Q s proof (prove)
goal (4 subgoals):
 1. \<And>queued tdom. \<not> queued \<Longrightarrow> \<lbrace>?B4 False tdom\<rbrace> threadGet tcbPriority tcb_ptr \<lbrace>\<lambda>rv _. True\<rbrace>
 2. \<And>queued. \<not> queued \<Longrightarrow> \<lbrace>?Q3 queued\<rbrace> threadGet tcbDomain tcb_ptr \<lbrace>?B4 queued\<rbrace>
 3. \<lbrace>?Q\<rbrace> threadGet tcbQueued tcb_ptr \<lbrace>\<lambda>queued. if queued then \<lambda>s. tcb_ptr \<in> {tcb_ptr. \<exists>priority. tcb_ptr \<in> set (ksReadyQueues s priority)} else ?Q3 queued\<rbrace>
 4. \<And>s. valid_queues' s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>valid_queues' s; tcb_at' tcb_ptr s\<rbrakk> \<Longrightarrow> \<exists>t. (tcbQueued t \<longrightarrow> ko_at' t tcb_ptr s \<and> (\<exists>a b. tcb_ptr \<in> set (ksReadyQueues s (a, b)))) \<and> (\<not> tcbQueued t \<longrightarrow> ko_at' t tcb_ptr s) proof (prove)
goal:
No subgoals!