theory TcbAcc_R

lemma tcbSchedDequeue_valid_objs' [wp]: "\<lbrace> valid_objs' \<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>_. valid_objs' \<rbrace>" unfolding tcbSchedDequeue_def apply (wp threadSet_valid_objs') apply (clarsimp simp add: valid_tcb'_def tcb_cte_cases_def) apply wp apply (simp add: if_apply_def2) apply (wp hoare_drop_imps) apply (wp | simp cong: if_cong add: valid_tcb'_def tcb_cte_cases_def if_apply_def2)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs'\<rbrace> tcbSchedDequeue t \<lbrace>\<lambda>_. valid_objs'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_objs'\<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_objs'\<rbrace> proof (prove)
goal (8 subgoals):
 1. \<And>queued tdom prio queue queue' x. \<lbrakk>queued; null queue'\<rbrakk> \<Longrightarrow> \<lbrace>?P'16 queued tdom prio queue queue' x\<rbrace> removeFromBitmap tdom prio \<lbrace>\<lambda>rv s. \<forall>tcb. valid_tcb' tcb s \<longrightarrow> valid_tcb' (tcbQueued_update (\<lambda>_. False) tcb) s\<rbrace>
 2. \<And>queued tdom prio queue queue'. queued \<Longrightarrow> \<lbrace>?B7 queued tdom prio queue queue'\<rbrace> setQueue tdom prio queue' \<lbrace>\<lambda>x. if null queue' then \<lambda>s. valid_objs' s \<and> ?P'16 queued tdom prio queue queue' x s else (\<lambda>s. valid_objs' s \<and> (\<forall>tcb. valid_tcb' tcb s \<longrightarrow> valid_tcb' (tcbQueued_update (\<lambda>_. False) tcb) s))\<rbrace>
 3. \<And>queued tdom prio queue. queued \<Longrightarrow> \<lbrace>?B6 queued tdom prio queue\<rbrace> return (filter (\<lambda>x. x \<noteq> t) queue) \<lbrace>?B7 queued tdom prio queue\<rbrace>
 4. \<And>queued tdom prio. queued \<Longrightarrow> \<lbrace>?B5 queued tdom prio\<rbrace> getQueue tdom prio \<lbrace>?B6 queued tdom prio\<rbrace>
 5. \<And>queued tdom. queued \<Longrightarrow> \<lbrace>?B4 queued tdom\<rbrace> threadGet tcbPriority t \<lbrace>?B5 queued tdom\<rbrace>
 6. \<And>queued. queued \<Longrightarrow> \<lbrace>?Q3 queued\<rbrace> threadGet tcbDomain t \<lbrace>?B4 queued\<rbrace>
 7. \<lbrace>?Q\<rbrace> threadGet tcbQueued t \<lbrace>\<lambda>queued. if queued then ?Q3 queued else valid_objs'\<rbrace>
 8. \<And>s. valid_objs' s \<Longrightarrow> ?Q s proof (prove)
goal (8 subgoals):
 1. \<And>queued tdom prio queue queue'. \<lbrakk>queued; null queue'\<rbrakk> \<Longrightarrow> \<lbrace>?P'16 True tdom prio queue queue' ()\<rbrace> removeFromBitmap tdom prio \<lbrace>\<lambda>rv s. True\<rbrace>
 2. \<And>queued tdom prio queue queue'. queued \<Longrightarrow> \<lbrace>?B7 queued tdom prio queue queue'\<rbrace> setQueue tdom prio queue' \<lbrace>\<lambda>x. if null queue' then \<lambda>s. valid_objs' s \<and> ?P'16 queued tdom prio queue queue' x s else (\<lambda>s. valid_objs' s \<and> (\<forall>tcb. valid_tcb' tcb s \<longrightarrow> valid_tcb' (tcbQueued_update (\<lambda>_. False) tcb) s))\<rbrace>
 3. \<And>queued tdom prio queue. queued \<Longrightarrow> \<lbrace>?B6 queued tdom prio queue\<rbrace> return (filter (\<lambda>x. x \<noteq> t) queue) \<lbrace>?B7 queued tdom prio queue\<rbrace>
 4. \<And>queued tdom prio. queued \<Longrightarrow> \<lbrace>?B5 queued tdom prio\<rbrace> getQueue tdom prio \<lbrace>?B6 queued tdom prio\<rbrace>
 5. \<And>queued tdom. queued \<Longrightarrow> \<lbrace>?B4 queued tdom\<rbrace> threadGet tcbPriority t \<lbrace>?B5 queued tdom\<rbrace>
 6. \<And>queued. queued \<Longrightarrow> \<lbrace>?Q3 queued\<rbrace> threadGet tcbDomain t \<lbrace>?B4 queued\<rbrace>
 7. \<lbrace>?Q\<rbrace> threadGet tcbQueued t \<lbrace>\<lambda>queued. if queued then ?Q3 queued else valid_objs'\<rbrace>
 8. \<And>s. valid_objs' s \<Longrightarrow> ?Q s proof (prove)
goal (7 subgoals):
 1. \<And>queued tdom prio queue queue'. queued \<Longrightarrow> \<lbrace>?B7 queued tdom prio queue queue'\<rbrace> setQueue tdom prio queue' \<lbrace>\<lambda>x. if null queue' then \<lambda>s. valid_objs' s \<and> True else (\<lambda>s. valid_objs' s \<and> (\<forall>tcb. valid_tcb' tcb s \<longrightarrow> valid_tcb' (tcbQueued_update (\<lambda>_. False) tcb) s))\<rbrace>
 2. \<And>queued tdom prio queue. queued \<Longrightarrow> \<lbrace>?B6 queued tdom prio queue\<rbrace> return (filter (\<lambda>x. x \<noteq> t) queue) \<lbrace>?B7 queued tdom prio queue\<rbrace>
 3. \<And>queued tdom prio. queued \<Longrightarrow> \<lbrace>?B5 queued tdom prio\<rbrace> getQueue tdom prio \<lbrace>?B6 queued tdom prio\<rbrace>
 4. \<And>queued tdom. queued \<Longrightarrow> \<lbrace>?B4 queued tdom\<rbrace> threadGet tcbPriority t \<lbrace>?B5 queued tdom\<rbrace>
 5. \<And>queued. queued \<Longrightarrow> \<lbrace>?Q3 queued\<rbrace> threadGet tcbDomain t \<lbrace>?B4 queued\<rbrace>
 6. \<lbrace>?Q\<rbrace> threadGet tcbQueued t \<lbrace>\<lambda>queued. if queued then ?Q3 queued else valid_objs'\<rbrace>
 7. \<And>s. valid_objs' s \<Longrightarrow> ?Q s proof (prove)
goal (7 subgoals):
 1. \<And>queued tdom prio queue queue'. queued \<Longrightarrow> \<lbrace>?B7 True tdom prio queue queue'\<rbrace> setQueue tdom prio queue' \<lbrace>\<lambda>x. valid_objs'\<rbrace>
 2. \<And>queued tdom prio queue. queued \<Longrightarrow> \<lbrace>?B6 queued tdom prio queue\<rbrace> return (filter (\<lambda>x. x \<noteq> t) queue) \<lbrace>?B7 queued tdom prio queue\<rbrace>
 3. \<And>queued tdom prio. queued \<Longrightarrow> \<lbrace>?B5 queued tdom prio\<rbrace> getQueue tdom prio \<lbrace>?B6 queued tdom prio\<rbrace>
 4. \<And>queued tdom. queued \<Longrightarrow> \<lbrace>?B4 queued tdom\<rbrace> threadGet tcbPriority t \<lbrace>?B5 queued tdom\<rbrace>
 5. \<And>queued. queued \<Longrightarrow> \<lbrace>?Q3 queued\<rbrace> threadGet tcbDomain t \<lbrace>?B4 queued\<rbrace>
 6. \<lbrace>?Q\<rbrace> threadGet tcbQueued t \<lbrace>\<lambda>queued. if queued then ?Q3 queued else valid_objs'\<rbrace>
 7. \<And>s. valid_objs' s \<Longrightarrow> ?Q s proof (prove)
goal (6 subgoals):
 1. \<And>queued tdom prio queue. queued \<Longrightarrow> \<lbrace>?B6 queued tdom prio queue\<rbrace> return (filter (\<lambda>x. x \<noteq> t) queue) \<lbrace>\<lambda>a. valid_objs'\<rbrace>
 2. \<And>queued tdom prio. queued \<Longrightarrow> \<lbrace>?B5 queued tdom prio\<rbrace> getQueue tdom prio \<lbrace>?B6 queued tdom prio\<rbrace>
 3. \<And>queued tdom. queued \<Longrightarrow> \<lbrace>?B4 queued tdom\<rbrace> threadGet tcbPriority t \<lbrace>?B5 queued tdom\<rbrace>
 4. \<And>queued. queued \<Longrightarrow> \<lbrace>?Q3 queued\<rbrace> threadGet tcbDomain t \<lbrace>?B4 queued\<rbrace>
 5. \<lbrace>?Q\<rbrace> threadGet tcbQueued t \<lbrace>\<lambda>queued. if queued then ?Q3 queued else valid_objs'\<rbrace>
 6. \<And>s. valid_objs' s \<Longrightarrow> ?Q s proof (prove)
goal:
No subgoals!