theory TcbAcc_R

lemma threadSet_valid_queues_addToQs:
  "\<lbrace>\<lambda>s. (\<forall>ko qdom prio. ko_at' ko t s \<and> inQ qdom prio (F ko) \<and> \<not> inQ qdom prio ko
            \<longrightarrow> t \<in> set (ksReadyQueues s (qdom, prio)))
             \<and> valid_queues' (ksReadyQueues_update (addToQs F t) s)\<rbrace>
     threadSet F t
   \<lbrace>\<lambda>rv. valid_queues'\<rbrace>" apply (simp add: valid_queues'_def threadSet_def obj_at'_real_def
                split del: if_split) apply (simp only: imp_conv_disj) apply (wp hoare_vcg_all_lift hoare_vcg_disj_lift) apply (wp setObject_ko_wp_at | simp add: objBits_simps')+ apply (wp getObject_tcb_wp updateObject_default_inv
               | simp split del: if_split)+ apply (clarsimp simp: obj_at'_def ko_wp_at'_def projectKOs
                        objBits_simps addToQs_set_def
             split del: if_split cong: if_cong) apply (fastforce simp: projectKOs split: if_split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (\<forall>ko qdom prio. ko_at' ko t s \<and> inQ qdom prio (F ko) \<and> \<not> inQ qdom prio ko \<longrightarrow> t \<in> set (ksReadyQueues s (qdom, prio))) \<and> valid_queues' (ksReadyQueues_update (addToQs F t) s)\<rbrace> threadSet F t \<lbrace>\<lambda>rv. valid_queues'\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (\<forall>ko qdom prio. ko_wp_at' (\<lambda>koa. projectKO_opt koa = Some ko) t s \<and> inQ qdom prio (F ko) \<and> \<not> inQ qdom prio ko \<longrightarrow> t \<in> set (ksReadyQueues s (qdom, prio))) \<and> (\<forall>d p ta. ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj \<and> inQ d p obj) ta s \<longrightarrow> ta \<in> set (addToQs F t (ksReadyQueues s) (d, p)))\<rbrace> do tcb <- getObject t;
setObject t (F tcb)
od \<lbrace>\<lambda>rv s. \<forall>d p t. ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj \<and> inQ d p obj) t s \<longrightarrow> t \<in> set (ksReadyQueues s (d, p))\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>\<lambda>s. (\<forall>ko qdom prio. \<not> (ko_wp_at' (\<lambda>koa. projectKO_opt koa = Some ko) t s \<and> inQ qdom prio (F ko) \<and> \<not> inQ qdom prio ko) \<or> t \<in> set (ksReadyQueues s (qdom, prio))) \<and> (\<forall>d p ta. \<not> ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj \<and> inQ d p obj) ta s \<or> ta \<in> set (addToQs F t (ksReadyQueues s) (d, p)))\<rbrace> do tcb <- getObject t;
setObject t (F tcb)
od \<lbrace>\<lambda>rv s. \<forall>d p t. \<not> ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj \<and> inQ d p obj) t s \<or> t \<in> set (ksReadyQueues s (d, p))\<rbrace> proof (prove)
goal (4 subgoals):
 1. \<And>d p ta tcb. \<lbrace>?B10 d p ta tcb\<rbrace> setObject t (F tcb) \<lbrace>\<lambda>rv s. \<not> ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj \<and> inQ d p obj) ta s\<rbrace>
 2. \<And>d p ta. \<lbrace>?P9 d p ta\<rbrace> getObject t \<lbrace>?B10 d p ta\<rbrace>
 3. \<And>d p ta. \<lbrace>?P'9 d p ta\<rbrace> do tcb <- getObject t;
setObject t (F tcb)
od \<lbrace>\<lambda>rv s. ta \<in> set (ksReadyQueues s (d, p))\<rbrace>
 4. \<And>s. (\<forall>ko qdom prio. \<not> (ko_wp_at' (\<lambda>koa. projectKO_opt koa = Some ko) t s \<and> inQ qdom prio (F ko) \<and> \<not> inQ qdom prio ko) \<or> t \<in> set (ksReadyQueues s (qdom, prio))) \<and> (\<forall>d p ta. \<not> ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj \<and> inQ d p obj) ta s \<or> ta \<in> set (addToQs F t (ksReadyQueues s) (d, p))) \<Longrightarrow> \<forall>x xa xb. ?P9 x xa xb s \<or> ?P'9 x xa xb s proof (prove)
goal (3 subgoals):
 1. \<And>d p ta. \<lbrace>?P9 d p ta\<rbrace> getObject t \<lbrace>\<lambda>tcb s. tcb_at' t s \<longrightarrow> \<not> ko_wp_at' (if t = ta then K (\<exists>obj. projectKO_opt (injectKO (F tcb)) = Some obj \<and> inQ d p obj) else (\<lambda>a. \<exists>obj. projectKO_opt a = Some obj \<and> inQ d p obj)) ta s\<rbrace>
 2. \<And>d p ta. \<lbrace>?P'9 d p ta\<rbrace> do tcb <- getObject t;
setObject t (F tcb)
od \<lbrace>\<lambda>rv s. ta \<in> set (ksReadyQueues s (d, p))\<rbrace>
 3. \<And>s. (\<forall>ko qdom prio. \<not> (ko_wp_at' (\<lambda>koa. projectKO_opt koa = Some ko) t s \<and> inQ qdom prio (F ko) \<and> \<not> inQ qdom prio ko) \<or> t \<in> set (ksReadyQueues s (qdom, prio))) \<and> (\<forall>d p ta. \<not> ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj \<and> inQ d p obj) ta s \<or> ta \<in> set (addToQs F t (ksReadyQueues s) (d, p))) \<Longrightarrow> \<forall>x xa xb. ?P9 x xa xb s \<or> ?P'9 x xa xb s proof (prove)
goal (1 subgoal):
 1. \<And>s. (\<forall>ko qdom prio. inQ qdom prio (F ko) \<longrightarrow> ko_wp_at' (\<lambda>koa. projectKO_opt koa = Some ko) t s \<longrightarrow> inQ qdom prio ko \<or> t \<in> set (ksReadyQueues s (qdom, prio))) \<and> (\<forall>d p ta. ko_wp_at' (\<lambda>ko. \<exists>obj. projectKO_opt ko = Some obj \<and> inQ d p obj) ta s \<longrightarrow> ta \<in> set (addToQs F t (ksReadyQueues s) (d, p))) \<Longrightarrow> tcb_at' t s \<longrightarrow> (\<forall>x xa xb. (\<exists>ta. ko_at' ta t s \<and> \<not> ko_wp_at' (if t = xb then K (\<exists>obj. projectKO_opt (injectKO (F ta)) = Some obj \<and> inQ x xa obj) else (\<lambda>a. \<exists>obj. projectKO_opt a = Some obj \<and> inQ x xa obj)) xb s) \<or> (\<exists>ta. ko_at' ta t s) \<and> xb \<in> set (ksReadyQueues s (x, xa))) proof (prove)
goal (1 subgoal):
 1. \<And>s x xa xb obj ko. \<lbrakk>\<forall>qdom prio. inQ qdom prio (F obj) \<longrightarrow> inQ qdom prio obj \<or> t \<in> set (ksReadyQueues s (qdom, prio)); \<forall>d p ta. (\<exists>ko. ksPSpace s ta = Some ko \<and> is_aligned ta (case ko of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch x \<Rightarrow> archObjSize x | _ \<Rightarrow> pageBits) \<and> (\<exists>obj. ko = KOTCB obj \<and> inQ d p obj) \<and> ps_clear ta (case ko of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch x \<Rightarrow> archObjSize x | _ \<Rightarrow> pageBits) s) \<longrightarrow> ta \<in> set (ksReadyQueues s (d, p)) \<or> ta = t \<and> (\<forall>ko. \<not> inQ d p (F ko)); ksPSpace s t = Some (KOTCB obj); is_aligned t tcbBlockSizeBits; ps_clear t tcbBlockSizeBits s; xb \<notin> set (ksReadyQueues s (x, xa)); (if t = xb then \<lambda>y. inQ x xa (F obj) else (\<lambda>a. \<exists>obj. a = KOTCB obj \<and> inQ x xa obj)) ko; is_aligned xb (case ko of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch x \<Rightarrow> archObjSize x | _ \<Rightarrow> pageBits); ksPSpace s xb = Some ko; ps_clear xb (case ko of KOEndpoint x \<Rightarrow> epSizeBits | KONotification x \<Rightarrow> ntfnSizeBits | KOTCB x \<Rightarrow> tcbBlockSizeBits | KOCTE x \<Rightarrow> cteSizeBits | KOArch x \<Rightarrow> archObjSize x | _ \<Rightarrow> pageBits) s\<rbrakk> \<Longrightarrow> False proof (prove)
goal:
No subgoals!