theory Scheduler_IF

lemma thread_set_scheduler_equiv[wp]:
  "\<lbrace>(invs and K(pasObjectAbs aag t \<noteq> SilcLabel) and
     (\<lambda>s. t = idle_thread s \<longrightarrow> tc = idle_context s)) and scheduler_equiv aag st\<rbrace>
   thread_set (tcb_arch_update (arch_tcb_context_set tc)) t
   \<lbrace>\<lambda>_. scheduler_equiv aag st\<rbrace>" apply (rule scheduler_equiv_lift') apply (rule globals_equiv_scheduler_inv') apply (wpsimp wp: thread_set_context_globals_equiv | simp)+ apply (simp add: silc_dom_equiv_def thread_set_def) apply (wp set_object_wp) apply (clarsimp simp: get_tcb_def equiv_for_def split: kernel_object.splits option.splits) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs and K (pasObjectAbs aag t \<noteq> SilcLabel) and (\<lambda>s. t = idle_thread s \<longrightarrow> tc = idle_context s) and scheduler_equiv aag st\<rbrace> thread_set (tcb_arch_update (arch_tcb_context_set tc)) t \<lbrace>\<lambda>_. scheduler_equiv aag st\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>st. \<lbrace>invs and K (pasObjectAbs aag t \<noteq> SilcLabel) and (\<lambda>s. t = idle_thread s \<longrightarrow> tc = idle_context s) and globals_equiv_scheduler st\<rbrace> thread_set (tcb_arch_update (arch_tcb_context_set tc)) t \<lbrace>\<lambda>_. globals_equiv_scheduler st\<rbrace>
 2. \<And>Q. \<lbrace>invs and K (pasObjectAbs aag t \<noteq> SilcLabel) and (\<lambda>s. t = idle_thread s \<longrightarrow> tc = idle_context s) and (\<lambda>s. Q (cur_domain s))\<rbrace> thread_set (tcb_arch_update (arch_tcb_context_set tc)) t \<lbrace>\<lambda>r s. Q (cur_domain s)\<rbrace>
 3. \<And>P. \<lbrace>\<lambda>s. P (idle_thread s)\<rbrace> thread_set (tcb_arch_update (arch_tcb_context_set tc)) t \<lbrace>\<lambda>_ s. P (idle_thread s)\<rbrace>
 4. \<And>Q. \<lbrace>invs and K (pasObjectAbs aag t \<noteq> SilcLabel) and (\<lambda>s. t = idle_thread s \<longrightarrow> tc = idle_context s) and (\<lambda>s. Q (domain_time s) (domain_index s) (domain_list s))\<rbrace> thread_set (tcb_arch_update (arch_tcb_context_set tc)) t \<lbrace>\<lambda>_ s. Q (domain_time s) (domain_index s) (domain_list s)\<rbrace>
 5. \<And>P. \<lbrace>\<lambda>s. P (irq_state_of_state s)\<rbrace> thread_set (tcb_arch_update (arch_tcb_context_set tc)) t \<lbrace>\<lambda>_ s. P (irq_state_of_state s)\<rbrace>
 6. \<And>st. \<lbrace>invs and K (pasObjectAbs aag t \<noteq> SilcLabel) and (\<lambda>s. t = idle_thread s \<longrightarrow> tc = idle_context s) and silc_dom_equiv aag st\<rbrace> thread_set (tcb_arch_update (arch_tcb_context_set tc)) t \<lbrace>\<lambda>_. silc_dom_equiv aag st\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>st sta. \<lbrace>invs and K (pasObjectAbs aag t \<noteq> SilcLabel) and (\<lambda>s. t = idle_thread s \<longrightarrow> tc = idle_context s) and globals_equiv sta\<rbrace> thread_set (tcb_arch_update (arch_tcb_context_set tc)) t \<lbrace>\<lambda>_. globals_equiv sta\<rbrace>
 2. \<And>Q. \<lbrace>invs and K (pasObjectAbs aag t \<noteq> SilcLabel) and (\<lambda>s. t = idle_thread s \<longrightarrow> tc = idle_context s) and (\<lambda>s. Q (cur_domain s))\<rbrace> thread_set (tcb_arch_update (arch_tcb_context_set tc)) t \<lbrace>\<lambda>r s. Q (cur_domain s)\<rbrace>
 3. \<And>P. \<lbrace>\<lambda>s. P (idle_thread s)\<rbrace> thread_set (tcb_arch_update (arch_tcb_context_set tc)) t \<lbrace>\<lambda>_ s. P (idle_thread s)\<rbrace>
 4. \<And>Q. \<lbrace>invs and K (pasObjectAbs aag t \<noteq> SilcLabel) and (\<lambda>s. t = idle_thread s \<longrightarrow> tc = idle_context s) and (\<lambda>s. Q (domain_time s) (domain_index s) (domain_list s))\<rbrace> thread_set (tcb_arch_update (arch_tcb_context_set tc)) t \<lbrace>\<lambda>_ s. Q (domain_time s) (domain_index s) (domain_list s)\<rbrace>
 5. \<And>P. \<lbrace>\<lambda>s. P (irq_state_of_state s)\<rbrace> thread_set (tcb_arch_update (arch_tcb_context_set tc)) t \<lbrace>\<lambda>_ s. P (irq_state_of_state s)\<rbrace>
 6. \<And>st. \<lbrace>invs and K (pasObjectAbs aag t \<noteq> SilcLabel) and (\<lambda>s. t = idle_thread s \<longrightarrow> tc = idle_context s) and silc_dom_equiv aag st\<rbrace> thread_set (tcb_arch_update (arch_tcb_context_set tc)) t \<lbrace>\<lambda>_. silc_dom_equiv aag st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>st. \<lbrace>invs and (\<lambda>y. pasObjectAbs aag t \<noteq> SilcLabel) and (\<lambda>s. t = idle_thread s \<longrightarrow> tc = idle_context s) and silc_dom_equiv aag st\<rbrace> thread_set (tcb_arch_update (arch_tcb_context_set tc)) t \<lbrace>\<lambda>_. silc_dom_equiv aag st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>st. \<lbrace>invs and (\<lambda>y. pasObjectAbs aag t \<noteq> SilcLabel) and (\<lambda>s. t = idle_thread s \<longrightarrow> tc = idle_context s) and equiv_for (\<lambda>x. pasObjectAbs aag x = SilcLabel) kheap st\<rbrace> do tcb <- gets_the (get_tcb t);
set_object t (TCB (tcb_arch_update (arch_tcb_context_set tc) tcb))
od \<lbrace>\<lambda>_. equiv_for (\<lambda>x. pasObjectAbs aag x = SilcLabel) kheap st\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<And>st s. (invs and (\<lambda>y. pasObjectAbs aag t \<noteq> SilcLabel) and (\<lambda>s. t = idle_thread s \<longrightarrow> tc = idle_context s) and equiv_for (\<lambda>x. pasObjectAbs aag x = SilcLabel) kheap st) s \<Longrightarrow> get_tcb t s \<noteq> None \<longrightarrow> equiv_for (\<lambda>x. pasObjectAbs aag x = SilcLabel) kheap st (s\<lparr>kheap := (kheap s)(t \<mapsto> TCB (tcb_arch_update (arch_tcb_context_set tc) (the (get_tcb t s))))\<rparr>) proof (prove)
goal:
No subgoals!