theory Scheduler_IF

lemma thread_set_reads_respect_scheduler[wp]:
  "reads_respects_scheduler aag l (invs and K(pasObjectAbs aag t \<noteq> SilcLabel)
                                        and (\<lambda>s. t = idle_thread s \<longrightarrow> tc = idle_context s)
                                        and guarded_pas_domain aag)
                            (thread_set (tcb_arch_update (arch_tcb_context_set tc)) t)" apply (rule reads_respects_scheduler_cases[where P'=\<top>]) prefer 3 apply (rule reads_respects_scheduler_unobservable'') apply (wp | simp | elim conjE)+ apply (simp add: thread_set_def) apply wp apply (fastforce simp: scheduler_affects_equiv_def get_tcb_def states_equiv_for_def
                           equiv_for_def scheduler_equiv_def domain_fields_equiv_def equiv_asids_def
                    split: option.splits kernel_object.splits)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (invs and K (pasObjectAbs aag t \<noteq> SilcLabel) and (\<lambda>s. t = idle_thread s \<longrightarrow> tc = idle_context s) and guarded_pas_domain aag) (thread_set (tcb_arch_update (arch_tcb_context_set tc)) t) proof (prove)
goal (4 subgoals):
 1. pasObjectAbs aag t \<in> reads_scheduler aag l \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (\<lambda>_. True) (thread_set (tcb_arch_update (arch_tcb_context_set tc)) t)
 2. \<And>s. \<lbrakk>(invs and K (pasObjectAbs aag t \<noteq> SilcLabel) and (\<lambda>s. t = idle_thread s \<longrightarrow> tc = idle_context s) and guarded_pas_domain aag) s; pasObjectAbs aag t \<in> reads_scheduler aag l\<rbrakk> \<Longrightarrow> True
 3. pasObjectAbs aag t \<notin> reads_scheduler aag l \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) ?P'' (thread_set (tcb_arch_update (arch_tcb_context_set tc)) t)
 4. \<And>s. \<lbrakk>(invs and K (pasObjectAbs aag t \<noteq> SilcLabel) and (\<lambda>s. t = idle_thread s \<longrightarrow> tc = idle_context s) and guarded_pas_domain aag) s; pasObjectAbs aag t \<notin> reads_scheduler aag l\<rbrakk> \<Longrightarrow> ?P'' s proof (prove)
goal (4 subgoals):
 1. pasObjectAbs aag t \<notin> reads_scheduler aag l \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) ?P'' (thread_set (tcb_arch_update (arch_tcb_context_set tc)) t)
 2. pasObjectAbs aag t \<in> reads_scheduler aag l \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (\<lambda>_. True) (thread_set (tcb_arch_update (arch_tcb_context_set tc)) t)
 3. \<And>s. \<lbrakk>(invs and K (pasObjectAbs aag t \<noteq> SilcLabel) and (\<lambda>s. t = idle_thread s \<longrightarrow> tc = idle_context s) and guarded_pas_domain aag) s; pasObjectAbs aag t \<in> reads_scheduler aag l\<rbrakk> \<Longrightarrow> True
 4. \<And>s. \<lbrakk>(invs and K (pasObjectAbs aag t \<noteq> SilcLabel) and (\<lambda>s. t = idle_thread s \<longrightarrow> tc = idle_context s) and guarded_pas_domain aag) s; pasObjectAbs aag t \<notin> reads_scheduler aag l\<rbrakk> \<Longrightarrow> ?P'' s proof (prove)
goal (6 subgoals):
 1. \<And>st. pasObjectAbs aag t \<notin> reads_scheduler aag l \<Longrightarrow> \<lbrace>?P5 and scheduler_equiv aag st and scheduler_affects_equiv aag l st\<rbrace> thread_set (tcb_arch_update (arch_tcb_context_set tc)) t \<lbrace>\<lambda>_. scheduler_equiv aag st\<rbrace>
 2. \<And>st. pasObjectAbs aag t \<notin> reads_scheduler aag l \<Longrightarrow> \<lbrace>?P'5 and scheduler_equiv aag st and scheduler_affects_equiv aag l st\<rbrace> thread_set (tcb_arch_update (arch_tcb_context_set tc)) t \<lbrace>\<lambda>_. scheduler_affects_equiv aag l st\<rbrace>
 3. \<And>s. \<lbrakk>pasObjectAbs aag t \<notin> reads_scheduler aag l; ?P'' s\<rbrakk> \<Longrightarrow> ?P5 s \<and> ?P'5 s
 4. pasObjectAbs aag t \<in> reads_scheduler aag l \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (\<lambda>_. True) (thread_set (tcb_arch_update (arch_tcb_context_set tc)) t)
 5. \<And>s. \<lbrakk>(invs and K (pasObjectAbs aag t \<noteq> SilcLabel) and (\<lambda>s. t = idle_thread s \<longrightarrow> tc = idle_context s) and guarded_pas_domain aag) s; pasObjectAbs aag t \<in> reads_scheduler aag l\<rbrakk> \<Longrightarrow> True
 6. \<And>s. \<lbrakk>(invs and K (pasObjectAbs aag t \<noteq> SilcLabel) and (\<lambda>s. t = idle_thread s \<longrightarrow> tc = idle_context s) and guarded_pas_domain aag) s; pasObjectAbs aag t \<notin> reads_scheduler aag l\<rbrakk> \<Longrightarrow> ?P'' s proof (prove)
goal (3 subgoals):
 1. pasObjectAbs aag t \<in> reads_scheduler aag l \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (\<lambda>_. True) (thread_set (tcb_arch_update (arch_tcb_context_set tc)) t)
 2. \<And>s. \<lbrakk>(invs and K (pasObjectAbs aag t \<noteq> SilcLabel) and (\<lambda>s. t = idle_thread s \<longrightarrow> tc = idle_context s) and guarded_pas_domain aag) s; pasObjectAbs aag t \<in> reads_scheduler aag l\<rbrakk> \<Longrightarrow> True
 3. \<And>s. \<lbrakk>(invs and K (pasObjectAbs aag t \<noteq> SilcLabel) and (\<lambda>s. t = idle_thread s \<longrightarrow> tc = idle_context s) and guarded_pas_domain aag) s; pasObjectAbs aag t \<notin> reads_scheduler aag l\<rbrakk> \<Longrightarrow> invs s \<and> pasObjectAbs aag t \<noteq> SilcLabel \<and> (t = idle_thread s \<longrightarrow> tc = idle_context s) proof (prove)
goal (3 subgoals):
 1. pasObjectAbs aag t \<in> reads_scheduler aag l \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (\<lambda>_. True) (do tcb <- gets_the (get_tcb t);
set_object t (TCB (tcb_arch_update (arch_tcb_context_set tc) tcb))
od)
 2. \<And>s. \<lbrakk>(invs and K (pasObjectAbs aag t \<noteq> SilcLabel) and (\<lambda>s. t = idle_thread s \<longrightarrow> tc = idle_context s) and guarded_pas_domain aag) s; pasObjectAbs aag t \<in> reads_scheduler aag l\<rbrakk> \<Longrightarrow> True
 3. \<And>s. \<lbrakk>(invs and K (pasObjectAbs aag t \<noteq> SilcLabel) and (\<lambda>s. t = idle_thread s \<longrightarrow> tc = idle_context s) and guarded_pas_domain aag) s; pasObjectAbs aag t \<notin> reads_scheduler aag l\<rbrakk> \<Longrightarrow> invs s \<and> pasObjectAbs aag t \<noteq> SilcLabel \<and> (t = idle_thread s \<longrightarrow> tc = idle_context s) proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>pasObjectAbs aag t \<in> reads_scheduler aag l; True\<rbrakk> \<Longrightarrow> K (\<forall>s ta. scheduler_equiv aag s ta \<and> scheduler_affects_equiv aag l s ta \<longrightarrow> get_tcb t s = get_tcb t ta) s \<and> (get_tcb t s \<noteq> None \<longrightarrow> True)
 2. \<And>s. \<lbrakk>(invs and K (pasObjectAbs aag t \<noteq> SilcLabel) and (\<lambda>s. t = idle_thread s \<longrightarrow> tc = idle_context s) and guarded_pas_domain aag) s; pasObjectAbs aag t \<in> reads_scheduler aag l\<rbrakk> \<Longrightarrow> True
 3. \<And>s. \<lbrakk>(invs and K (pasObjectAbs aag t \<noteq> SilcLabel) and (\<lambda>s. t = idle_thread s \<longrightarrow> tc = idle_context s) and guarded_pas_domain aag) s; pasObjectAbs aag t \<notin> reads_scheduler aag l\<rbrakk> \<Longrightarrow> invs s \<and> pasObjectAbs aag t \<noteq> SilcLabel \<and> (t = idle_thread s \<longrightarrow> tc = idle_context s) proof (prove)
goal:
No subgoals!