theory Scheduler_IF

lemma activate_thread_reads_respects_scheduler[wp]:
  assumes domains_distinct[wp]: "pas_domains_distinct aag"
  shows "reads_respects_scheduler aag l (invs and silc_inv aag st and guarded_pas_domain aag)
                                  activate_thread" apply (simp add: activate_thread_def) apply (rule reads_respects_scheduler_cases') apply ((wp sts_reads_respects_scheduler get_thread_state_reads_respects_scheduler
                gts_wp as_user_reads_respects_scheduler
             | wpc
             | simp add: det_setNextPC)+)[1] apply (intro impI conjI allI;
           fastforce simp: det_getRestartPC guarded_pas_domain_def reads_scheduler_def
                           restart_not_idle invs_valid_idle
                     dest: st_tcb_at_not_idle_thread domains_distinct[THEN pas_domains_distinct_inj]) apply (rule reads_respects_scheduler_unobservable''
                 [where P'="\<lambda>s. \<not> reads_scheduler_cur_domain aag l s \<and>
                                guarded_pas_domain aag s \<and> invs s"]) apply ((wp scheduler_equiv_lift'[where P="invs and silc_inv aag st"]
                globals_equiv_scheduler_inv'[where P="valid_arch_state and valid_idle"]
                set_thread_state_globals_equiv gts_wp
             | wpc
             | clarsimp simp: restart_not_idle silc_inv_not_cur_thread
             | force)+)[1] apply (wp gts_wp| wpc | simp)+ apply (clarsimp simp: guarded_pas_domain_def restart_not_idle invs_valid_idle) apply force+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (invs and silc_inv aag st and guarded_pas_domain aag) activate_thread proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (invs and silc_inv aag st and guarded_pas_domain aag) (do thread <- gets cur_thread;
state <- get_thread_state thread;
case state of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user thread getRestartPC;
as_user thread $ setNextPC pc;
set_thread_state thread Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread thread | _ \<Rightarrow> fail
od) proof (prove)
goal (4 subgoals):
 1. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) ?P' (do thread <- gets cur_thread;
state <- get_thread_state thread;
case state of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user thread getRestartPC;
as_user thread $ setNextPC pc;
set_thread_state thread Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread thread | _ \<Rightarrow> fail
od)
 2. \<And>s. \<lbrakk>(invs and silc_inv aag st and guarded_pas_domain aag) s; reads_scheduler_cur_domain aag l s\<rbrakk> \<Longrightarrow> ?P' s
 3. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) ?P'' (do thread <- gets cur_thread;
state <- get_thread_state thread;
case state of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user thread getRestartPC;
as_user thread $ setNextPC pc;
set_thread_state thread Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread thread | _ \<Rightarrow> fail
od)
 4. \<And>s. \<lbrakk>(invs and silc_inv aag st and guarded_pas_domain aag) s; \<not> reads_scheduler_cur_domain aag l s\<rbrakk> \<Longrightarrow> ?P'' s proof (prove)
goal (3 subgoals):
 1. \<And>s. \<lbrakk>(invs and silc_inv aag st and guarded_pas_domain aag) s; reads_scheduler_cur_domain aag l s\<rbrakk> \<Longrightarrow> reads_scheduler_cur_domain aag l s \<and> ((\<lambda>sa. st_tcb_at (\<lambda>_. True) (cur_thread s) sa \<longrightarrow> pasObjectAbs aag (cur_thread s) \<in> reads_scheduler aag l \<or> cur_thread s = idle_thread sa) and valid_idle) s \<and> (\<forall>st. st_tcb_at ((=) st) (cur_thread s) s \<longrightarrow> (st = Running \<longrightarrow> True) \<and> (inactive st \<longrightarrow> True) \<and> (st = Restart \<longrightarrow> (K (pasObjectAbs aag (cur_thread s) \<in> reads_scheduler aag l) and (\<lambda>sa. cur_thread s \<noteq> idle_thread sa) and K (det getRestartPC)) s \<and> K (pasObjectAbs aag (cur_thread s) \<in> reads_scheduler aag l) s \<and> cur_thread s \<noteq> idle_thread s \<and> pasObjectAbs aag (cur_thread s) \<in> reads_scheduler aag l \<and> reads_scheduler_cur_domain aag l s \<and> valid_idle s \<and> cur_thread s \<noteq> idle_thread s) \<and> (\<forall>x xa. st = BlockedOnReceive x xa \<longrightarrow> True) \<and> (\<forall>x xa. st = BlockedOnSend x xa \<longrightarrow> True) \<and> (awaiting_reply st \<longrightarrow> True) \<and> (\<forall>x. st = BlockedOnNotification x \<longrightarrow> True) \<and> (idle st \<longrightarrow> True))
 2. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) ?P'' (do thread <- gets cur_thread;
state <- get_thread_state thread;
case state of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user thread getRestartPC;
as_user thread $ setNextPC pc;
set_thread_state thread Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread thread | _ \<Rightarrow> fail
od)
 3. \<And>s. \<lbrakk>(invs and silc_inv aag st and guarded_pas_domain aag) s; \<not> reads_scheduler_cur_domain aag l s\<rbrakk> \<Longrightarrow> ?P'' s proof (prove)
goal (2 subgoals):
 1. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) ?P'' (do thread <- gets cur_thread;
state <- get_thread_state thread;
case state of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user thread getRestartPC;
as_user thread $ setNextPC pc;
set_thread_state thread Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread thread | _ \<Rightarrow> fail
od)
 2. \<And>s. \<lbrakk>(invs and silc_inv aag st and guarded_pas_domain aag) s; \<not> reads_scheduler_cur_domain aag l s\<rbrakk> \<Longrightarrow> ?P'' s proof (prove)
goal (4 subgoals):
 1. \<And>st. \<lbrace>?P312 and scheduler_equiv aag st and scheduler_affects_equiv aag l st\<rbrace> do thread <- gets cur_thread;
state <- get_thread_state thread;
case state of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user thread getRestartPC;
as_user thread $ setNextPC pc;
set_thread_state thread Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread thread | _ \<Rightarrow> fail
od \<lbrace>\<lambda>_. scheduler_equiv aag st\<rbrace>
 2. \<And>st. \<lbrace>(\<lambda>s. \<not> reads_scheduler_cur_domain aag l s \<and> guarded_pas_domain aag s \<and> invs s) and scheduler_equiv aag st and scheduler_affects_equiv aag l st\<rbrace> do thread <- gets cur_thread;
state <- get_thread_state thread;
case state of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user thread getRestartPC;
as_user thread $ setNextPC pc;
set_thread_state thread Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread thread | _ \<Rightarrow> fail
od \<lbrace>\<lambda>_. scheduler_affects_equiv aag l st\<rbrace>
 3. \<And>s. ?P'' s \<Longrightarrow> ?P312 s \<and> \<not> reads_scheduler_cur_domain aag l s \<and> guarded_pas_domain aag s \<and> invs s
 4. \<And>s. \<lbrakk>(invs and silc_inv aag st and guarded_pas_domain aag) s; \<not> reads_scheduler_cur_domain aag l s\<rbrakk> \<Longrightarrow> ?P'' s proof (prove)
goal (3 subgoals):
 1. \<And>st. \<lbrace>(\<lambda>s. \<not> reads_scheduler_cur_domain aag l s \<and> guarded_pas_domain aag s \<and> invs s) and scheduler_equiv aag st and scheduler_affects_equiv aag l st\<rbrace> do thread <- gets cur_thread;
state <- get_thread_state thread;
case state of Running \<Rightarrow> return () | Restart \<Rightarrow> do pc <- as_user thread getRestartPC;
as_user thread $ setNextPC pc;
set_thread_state thread Running
od | IdleThreadState \<Rightarrow> arch_activate_idle_thread thread | _ \<Rightarrow> fail
od \<lbrace>\<lambda>_. scheduler_affects_equiv aag l st\<rbrace>
 2. \<And>s. ?P'' s \<Longrightarrow> (invs s \<and> silc_inv aag st s) \<and> \<not> reads_scheduler_cur_domain aag l s \<and> guarded_pas_domain aag s \<and> invs s
 3. \<And>s. \<lbrakk>(invs and silc_inv aag st and guarded_pas_domain aag) s; \<not> reads_scheduler_cur_domain aag l s\<rbrakk> \<Longrightarrow> ?P'' s proof (prove)
goal (3 subgoals):
 1. \<And>st s. pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {} \<and> guarded_pas_domain aag s \<and> invs s \<and> scheduler_equiv aag st s \<and> scheduler_affects_equiv aag l st s \<Longrightarrow> st_tcb_at ((=) Restart) (cur_thread s) s \<longrightarrow> pasObjectAbs aag (cur_thread s) \<notin> reads_scheduler aag l
 2. \<And>s. ?P'' s \<Longrightarrow> (invs s \<and> silc_inv aag st s) \<and> \<not> reads_scheduler_cur_domain aag l s \<and> guarded_pas_domain aag s \<and> invs s
 3. \<And>s. \<lbrakk>(invs and silc_inv aag st and guarded_pas_domain aag) s; \<not> reads_scheduler_cur_domain aag l s\<rbrakk> \<Longrightarrow> ?P'' s proof (prove)
goal (3 subgoals):
 1. \<And>st s. \<lbrakk>pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {}; pasObjectAbs aag (cur_thread s) \<in> pasDomainAbs aag (cur_domain s); invs s; scheduler_equiv aag st s; scheduler_affects_equiv aag l st s; st_tcb_at ((=) Restart) (cur_thread s) s; pasObjectAbs aag (cur_thread s) \<in> reads_scheduler aag l\<rbrakk> \<Longrightarrow> False
 2. \<And>s. ?P'' s \<Longrightarrow> (invs s \<and> silc_inv aag st s) \<and> \<not> reads_scheduler_cur_domain aag l s \<and> guarded_pas_domain aag s \<and> invs s
 3. \<And>s. \<lbrakk>(invs and silc_inv aag st and guarded_pas_domain aag) s; \<not> reads_scheduler_cur_domain aag l s\<rbrakk> \<Longrightarrow> ?P'' s proof (prove)
goal:
No subgoals!