theory Tcb_R

lemma threadSet_valid_queues_no_state:
  "\<lbrace>Invariants_H.valid_queues and (\<lambda>s. \<forall>p. t \<notin> set (ksReadyQueues s p))\<rbrace>
     threadSet f t \<lbrace>\<lambda>_. Invariants_H.valid_queues\<rbrace>" apply (simp add: threadSet_def) apply wp apply (simp add: valid_queues_def 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_def valid_queues_no_bitmap_def' pred_tcb_at'_def) apply (clarsimp simp: obj_at'_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>Invariants_H.valid_queues and (\<lambda>s. \<forall>p. t \<notin> set (ksReadyQueues s p))\<rbrace> threadSet f t \<lbrace>\<lambda>_. Invariants_H.valid_queues\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>Invariants_H.valid_queues 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>_. Invariants_H.valid_queues\<rbrace> proof (prove)
goal (3 subgoals):
 1. \<And>tcb. \<lbrace>?B1 tcb\<rbrace> setObject t (f tcb) \<lbrace>\<lambda>_. Invariants_H.valid_queues\<rbrace>
 2. \<lbrace>?Q\<rbrace> getObject t \<lbrace>?B1\<rbrace>
 3. \<And>s. (Invariants_H.valid_queues and (\<lambda>s. \<forall>a b. t \<notin> set (ksReadyQueues s (a, b)))) s \<Longrightarrow> ?Q s proof (prove)
goal (3 subgoals):
 1. \<And>tcb. \<lbrace>?B1 tcb\<rbrace> setObject t (f tcb) \<lbrace>\<lambda>_ 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) = [])) \<and> valid_bitmapQ s \<and> bitmapQ_no_L2_orphans s \<and> bitmapQ_no_L1_orphans s\<rbrace>
 2. \<lbrace>?Q\<rbrace> getObject t \<lbrace>?B1\<rbrace>
 3. \<And>s. (Invariants_H.valid_queues and (\<lambda>s. \<forall>a b. t \<notin> set (ksReadyQueues s (a, b)))) s \<Longrightarrow> ?Q s proof (prove)
goal (2 subgoals):
 1. \<lbrace>?Q\<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) = [])) \<and> valid_bitmapQ s \<and> bitmapQ_no_L2_orphans s \<and> bitmapQ_no_L1_orphans s\<rbrace>
 2. \<And>s. (Invariants_H.valid_queues and (\<lambda>s. \<forall>a b. t \<notin> set (ksReadyQueues s (a, b)))) s \<Longrightarrow> ?Q s proof (prove)
goal (1 subgoal):
 1. \<And>s. (Invariants_H.valid_queues and (\<lambda>s. \<forall>a b. t \<notin> set (ksReadyQueues s (a, b)))) 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) = [])) \<and> valid_bitmapQ s \<and> bitmapQ_no_L2_orphans s \<and> bitmapQ_no_L1_orphans s) 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) = []); valid_bitmapQ s; bitmapQ_no_L2_orphans s; bitmapQ_no_L1_orphans s; \<forall>a b. t \<notin> set (ksReadyQueues s (a, b)); tcb_at' t s\<rbrakk> \<Longrightarrow> \<exists>ta. ko_at' ta t s proof (prove)
goal:
No subgoals!