theory Tcb_R

lemma threadSet_valid_queues'_no_state:
  "(\<And>tcb. tcbQueued tcb = tcbQueued (f tcb))
  \<Longrightarrow> \<lbrace>valid_queues' and (\<lambda>s. \<forall>p. t \<notin> set (ksReadyQueues s p))\<rbrace>
     threadSet f t \<lbrace>\<lambda>_. 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_def
             split del: if_split cong: if_cong) apply (fastforce simp: projectKOs inQ_def split: if_split_asm) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. (\<And>tcb. tcbQueued tcb = tcbQueued (f tcb)) \<Longrightarrow> \<lbrace>valid_queues' and (\<lambda>s. \<forall>p. t \<notin> set (ksReadyQueues s p))\<rbrace> threadSet f t \<lbrace>\<lambda>_. valid_queues'\<rbrace> proof (prove)
goal (1 subgoal):
 1. (\<And>tcb. tcbQueued tcb = tcbQueued (f tcb)) \<Longrightarrow> \<lbrace>(\<lambda>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))) and (\<lambda>s. \<forall>a b. t \<notin> set (ksReadyQueues s (a, b)))\<rbrace> do tcb <- getObject t;
setObject t (f tcb)
od \<lbrace>\<lambda>_ 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. (\<And>tcb. tcbQueued tcb = tcbQueued (f tcb)) \<Longrightarrow> \<lbrace>(\<lambda>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))) and (\<lambda>s. \<forall>a b. t \<notin> set (ksReadyQueues s (a, b)))\<rbrace> do tcb <- getObject t;
setObject t (f tcb)
od \<lbrace>\<lambda>_ 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. (\<And>tcb. tcbQueued tcb = tcbQueued (f tcb)) \<Longrightarrow> \<lbrace>?B8 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. (\<And>tcb. tcbQueued tcb = tcbQueued (f tcb)) \<Longrightarrow> \<lbrace>?P7 d p ta\<rbrace> getObject t \<lbrace>?B8 d p ta\<rbrace>
 3. \<And>d p ta. (\<And>tcb. tcbQueued tcb = tcbQueued (f tcb)) \<Longrightarrow> \<lbrace>?P'7 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. \<lbrakk>\<And>tcb. tcbQueued tcb = tcbQueued (f tcb); ((\<lambda>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))) and (\<lambda>s. \<forall>a b. t \<notin> set (ksReadyQueues s (a, b)))) s\<rbrakk> \<Longrightarrow> \<forall>x xa xb. ?P7 x xa xb s \<or> ?P'7 x xa xb s proof (prove)
goal (3 subgoals):
 1. \<And>d p ta. (\<And>tcb. tcbQueued tcb = tcbQueued (f tcb)) \<Longrightarrow> \<lbrace>?P7 d p ta\<rbrace> getObject t \<lbrace>\<lambda>tcb s. tcb_at' t s \<longrightarrow> \<not> ko_wp_at' (if t = ta then \<lambda>y. \<exists>obj. projectKO_opt (KOTCB (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. (\<And>tcb. tcbQueued tcb = tcbQueued (f tcb)) \<Longrightarrow> \<lbrace>?P'7 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. \<lbrakk>\<And>tcb. tcbQueued tcb = tcbQueued (f tcb); ((\<lambda>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))) and (\<lambda>s. \<forall>a b. t \<notin> set (ksReadyQueues s (a, b)))) s\<rbrakk> \<Longrightarrow> \<forall>x xa xb. ?P7 x xa xb s \<or> ?P'7 x xa xb s proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<And>tcb. tcbQueued tcb = tcbQueued (f tcb); (\<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))) \<and> (\<forall>a b. t \<notin> set (ksReadyQueues s (a, b)))\<rbrakk> \<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 \<lambda>y. \<exists>obj. projectKO_opt (KOTCB (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>\<And>tcb. tcbQueued tcb = tcbQueued (f tcb); \<forall>d p t. (\<exists>ko. ksPSpace s t = Some ko \<and> is_aligned t (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 t (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> t \<in> set (ksReadyQueues s (d, p)); \<forall>a b. t \<notin> set (ksReadyQueues s (a, b)); 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!