theory TcbAcc_R

lemma threadSet_valid_queues_no_bitmap:
  "\<lbrace> valid_queues_no_bitmap and
    (\<lambda>s. \<forall>d p. (\<exists>tcb. (inQ d p tcb \<and> runnable' (tcbState tcb)) \<and>
                     \<not>(inQ d p (f tcb) \<and> runnable' (tcbState (f tcb))))
                \<longrightarrow> obj_at' (\<lambda>tcb. (inQ d p tcb \<and> runnable' (tcbState tcb)) \<and>
                                 \<not>(inQ d p (f tcb) \<and> runnable' (tcbState (f tcb)))) t s
                \<longrightarrow> t \<notin> set (ksReadyQueues s (d, p))
    )\<rbrace>
     threadSet f t
   \<lbrace>\<lambda>rv. valid_queues_no_bitmap \<rbrace>" apply (simp add: threadSet_def) apply wp apply (simp add: Invariants_H.valid_queues_no_bitmap_def' pred_tcb_at'_def) apply (wp setObject_queues_unchanged_tcb
             hoare_Ball_helper
             hoare_vcg_all_lift
             setObject_tcb_strongest)[1] apply (wp getObject_tcb_wp) apply (clarsimp simp: valid_queues_no_bitmap_def' pred_tcb_at'_def) apply (clarsimp simp: obj_at'_def projectKOs) apply (fastforce) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_queues_no_bitmap and (\<lambda>s. \<forall>d p. (\<exists>tcb. (inQ d p tcb \<and> runnable' (tcbState tcb)) \<and> \<not> (inQ d p (f tcb) \<and> runnable' (tcbState (f tcb)))) \<longrightarrow> obj_at' (\<lambda>tcb. (inQ d p tcb \<and> runnable' (tcbState tcb)) \<and> \<not> (inQ d p (f tcb) \<and> runnable' (tcbState (f tcb)))) t s \<longrightarrow> t \<notin> set (ksReadyQueues s (d, p)))\<rbrace> threadSet f t \<lbrace>\<lambda>rv. valid_queues_no_bitmap\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>valid_queues_no_bitmap and (\<lambda>s. \<forall>d p. (\<exists>tcb. inQ d p tcb \<and> runnable' (tcbState tcb) \<and> (inQ d p (f tcb) \<longrightarrow> \<not> runnable' (tcbState (f tcb)))) \<longrightarrow> obj_at' (\<lambda>tcb. inQ d p tcb \<and> runnable' (tcbState tcb) \<and> (inQ d p (f tcb) \<longrightarrow> \<not> runnable' (tcbState (f tcb)))) t s \<longrightarrow> t \<notin> set (ksReadyQueues s (d, p)))\<rbrace> do tcb <- getObject t;
setObject t (f tcb)
od \<lbrace>\<lambda>rv. valid_queues_no_bitmap\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>tcb. \<lbrace>?B6 tcb\<rbrace> setObject t (f tcb) \<lbrace>\<lambda>rv. valid_queues_no_bitmap\<rbrace>
 2. \<lbrace>?Q5\<rbrace> getObject t \<lbrace>?B6\<rbrace>
 3. \<And>s. (valid_queues_no_bitmap and (\<lambda>s. \<forall>d p. (\<exists>tcb. inQ d p tcb \<and> runnable' (tcbState tcb) \<and> (inQ d p (f tcb) \<longrightarrow> \<not> runnable' (tcbState (f tcb)))) \<longrightarrow> obj_at' (\<lambda>tcb. inQ d p tcb \<and> runnable' (tcbState tcb) \<and> (inQ d p (f tcb) \<longrightarrow> \<not> runnable' (tcbState (f tcb)))) t s \<longrightarrow> t \<notin> set (ksReadyQueues s (d, p)))) s \<Longrightarrow> ?Q5 s proof (prove)
goal (3 subgoals):
 1. \<And>tcb. \<lbrace>?B6 tcb\<rbrace> setObject t (f tcb) \<lbrace>\<lambda>rv s. \<forall>d p. (\<forall>t\<in>set (ksReadyQueues s (d, p)). obj_at' (inQ d p) t s \<and> obj_at' (\<lambda>ko. runnable' (tcbState ko)) t s) \<and> distinct (ksReadyQueues s (d, p)) \<and> (maxDomain < d \<longrightarrow> ksReadyQueues s (d, p) = []) \<and> (maxPriority < p \<longrightarrow> ksReadyQueues s (d, p) = [])\<rbrace>
 2. \<lbrace>?Q5\<rbrace> getObject t \<lbrace>?B6\<rbrace>
 3. \<And>s. (valid_queues_no_bitmap and (\<lambda>s. \<forall>d p. (\<exists>tcb. inQ d p tcb \<and> runnable' (tcbState tcb) \<and> (inQ d p (f tcb) \<longrightarrow> \<not> runnable' (tcbState (f tcb)))) \<longrightarrow> obj_at' (\<lambda>tcb. inQ d p tcb \<and> runnable' (tcbState tcb) \<and> (inQ d p (f tcb) \<longrightarrow> \<not> runnable' (tcbState (f tcb)))) t s \<longrightarrow> t \<notin> set (ksReadyQueues s (d, p)))) s \<Longrightarrow> ?Q5 s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q5\<rbrace> getObject t \<lbrace>\<lambda>tcb s. \<forall>x xa. (\<forall>xb\<in>set (ksReadyQueues s (x, xa)). (if t = xb then inQ x xa (f tcb) else obj_at' (inQ x xa) xb s) \<and> (if t = xb then runnable' (tcbState (f tcb)) else obj_at' (\<lambda>ko. runnable' (tcbState ko)) xb s)) \<and> distinct (ksReadyQueues s (x, xa)) \<and> (maxDomain < x \<longrightarrow> ksReadyQueues s (x, xa) = []) \<and> (maxPriority < xa \<longrightarrow> ksReadyQueues s (x, xa) = [])\<rbrace>
 2. \<And>s. (valid_queues_no_bitmap and (\<lambda>s. \<forall>d p. (\<exists>tcb. inQ d p tcb \<and> runnable' (tcbState tcb) \<and> (inQ d p (f tcb) \<longrightarrow> \<not> runnable' (tcbState (f tcb)))) \<longrightarrow> obj_at' (\<lambda>tcb. inQ d p tcb \<and> runnable' (tcbState tcb) \<and> (inQ d p (f tcb) \<longrightarrow> \<not> runnable' (tcbState (f tcb)))) t s \<longrightarrow> t \<notin> set (ksReadyQueues s (d, p)))) s \<Longrightarrow> ?Q5 s proof (prove)
goal (1 subgoal):
 1. \<And>s. (valid_queues_no_bitmap and (\<lambda>s. \<forall>d p. (\<exists>tcb. inQ d p tcb \<and> runnable' (tcbState tcb) \<and> (inQ d p (f tcb) \<longrightarrow> \<not> runnable' (tcbState (f tcb)))) \<longrightarrow> obj_at' (\<lambda>tcb. inQ d p tcb \<and> runnable' (tcbState tcb) \<and> (inQ d p (f tcb) \<longrightarrow> \<not> runnable' (tcbState (f tcb)))) t s \<longrightarrow> t \<notin> set (ksReadyQueues s (d, p)))) s \<Longrightarrow> tcb_at' t s \<longrightarrow> (\<exists>ta. ko_at' ta t s \<and> (\<forall>x xa. (\<forall>xb\<in>set (ksReadyQueues s (x, xa)). (if t = xb then inQ x xa (f ta) else obj_at' (inQ x xa) xb s) \<and> (if t = xb then runnable' (tcbState (f ta)) else obj_at' (\<lambda>ko. runnable' (tcbState ko)) xb s)) \<and> distinct (ksReadyQueues s (x, xa)) \<and> (maxDomain < x \<longrightarrow> ksReadyQueues s (x, xa) = []) \<and> (maxPriority < xa \<longrightarrow> ksReadyQueues s (x, xa) = []))) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>\<forall>d p. (\<forall>t\<in>set (ksReadyQueues s (d, p)). obj_at' (inQ d p) t s \<and> obj_at' (\<lambda>ko. runnable' (tcbState ko)) t s) \<and> distinct (ksReadyQueues s (d, p)) \<and> (maxDomain < d \<longrightarrow> ksReadyQueues s (d, p) = []) \<and> (maxPriority < p \<longrightarrow> ksReadyQueues s (d, p) = []); \<forall>d p. (\<exists>tcb. inQ d p tcb \<and> runnable' (tcbState tcb) \<and> (inQ d p (f tcb) \<longrightarrow> \<not> runnable' (tcbState (f tcb)))) \<longrightarrow> obj_at' (\<lambda>tcb. inQ d p tcb \<and> runnable' (tcbState tcb) \<and> (inQ d p (f tcb) \<longrightarrow> \<not> runnable' (tcbState (f tcb)))) t s \<longrightarrow> t \<notin> set (ksReadyQueues s (d, p)); tcb_at' t s\<rbrakk> \<Longrightarrow> \<exists>ta. ko_at' ta t s \<and> (\<forall>x xa. t \<in> set (ksReadyQueues s (x, xa)) \<longrightarrow> inQ x xa (f ta) \<and> runnable' (tcbState (f ta))) proof (prove)
goal (1 subgoal):
 1. \<And>s obj x xa. \<lbrakk>\<forall>d p. (\<forall>t\<in>set (ksReadyQueues s (d, p)). (\<exists>ko. ksPSpace s t = Some ko \<and> is_aligned t (objBitsKO ko) \<and> (\<exists>obj. ko = KOTCB obj \<and> inQ d p obj \<and> ps_clear t (objBitsKO ko) s)) \<and> (\<exists>ko. ksPSpace s t = Some ko \<and> is_aligned t (objBitsKO ko) \<and> (\<exists>obj. ko = KOTCB obj \<and> runnable' (tcbState obj) \<and> ps_clear t (objBitsKO ko) s))) \<and> distinct (ksReadyQueues s (d, p)) \<and> (maxDomain < d \<longrightarrow> ksReadyQueues s (d, p) = []) \<and> (maxPriority < p \<longrightarrow> ksReadyQueues s (d, p) = []); \<forall>d p. (\<exists>tcb. inQ d p tcb \<and> runnable' (tcbState tcb) \<and> (inQ d p (f tcb) \<longrightarrow> \<not> runnable' (tcbState (f tcb)))) \<longrightarrow> inQ d p obj \<and> runnable' (tcbState obj) \<and> (inQ d p (f obj) \<longrightarrow> \<not> runnable' (tcbState (f obj))) \<longrightarrow> t \<notin> set (ksReadyQueues s (d, p)); ksPSpace s t = Some (KOTCB obj); is_aligned t (objBitsKO (KOTCB obj)); ps_clear t (objBitsKO (KOTCB obj)) s; t \<in> set (ksReadyQueues s (x, xa))\<rbrakk> \<Longrightarrow> inQ x xa (f obj) \<and> runnable' (tcbState (f obj)) proof (prove)
goal:
No subgoals!