theory ArchScheduler_IF

lemma arch_switch_to_thread_midstrength_reads_respects_scheduler[Scheduler_IF_assms, wp]:
  assumes domains_distinct[wp]: "pas_domains_distinct aag"
  shows "midstrength_reads_respects_scheduler aag l
           (invs and pas_refined aag and (\<lambda>s. pasObjectAbs aag t \<in> pasDomainAbs aag (cur_domain s)))
           (do _ <- arch_switch_to_thread t;
               _ <- modify (cur_thread_update (\<lambda>_. t));
               modify (scheduler_action_update (\<lambda>_. resume_cur_thread))
            od)" apply (rule equiv_valid_guard_imp) apply (rule midstrength_reads_respects_scheduler_cases[
                    where Q="(invs and pas_refined aag and
                                  (\<lambda>s. pasObjectAbs aag t \<in> pasDomainAbs aag (cur_domain s)))",
                    OF domains_distinct]) apply (simp add: arch_switch_to_thread_def bind_assoc) apply (rule bind_ev_general) apply (fold set_scheduler_action_def) apply (rule store_cur_thread_fragment_midstrength_reads_respects) apply (rule_tac P="\<top>" and P'="\<top>" in equiv_valid_inv_unobservable) apply (rule hoare_pre) apply (rule scheduler_equiv_lift'[where P=\<top>]) apply (wp globals_equiv_scheduler_inv silc_dom_lift | simp)+ apply (wp midstrength_scheduler_affects_equiv_unobservable set_vm_root_states_equiv_for
                  | simp)+ apply (wp cur_thread_update_not_subject_reads_respects_scheduler | simp | fastforce)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. midstrength_reads_respects_scheduler aag l (invs and pas_refined aag and (\<lambda>s. pasObjectAbs aag t \<in> pasDomainAbs aag (cur_domain s))) (do _ <- arch_switch_to_thread t;
_ <- modify (cur_thread_update (\<lambda>_. t));
modify (scheduler_action_update (\<lambda>_. resume_cur_thread))
od) proof (prove)
goal (2 subgoals):
 1. midstrength_reads_respects_scheduler aag l ?Q (do _ <- arch_switch_to_thread t;
_ <- modify (cur_thread_update (\<lambda>_. t));
modify (scheduler_action_update (\<lambda>_. resume_cur_thread))
od)
 2. \<And>s. (invs and pas_refined aag and (\<lambda>s. pasObjectAbs aag t \<in> pasDomainAbs aag (cur_domain s))) s \<Longrightarrow> ?Q s proof (prove)
goal (6 subgoals):
 1. pasObjectAbs aag t \<in> reads_scheduler aag l \<Longrightarrow> midstrength_reads_respects_scheduler aag l ?P'3 (do _ <- arch_switch_to_thread t;
_ <- modify (cur_thread_update (\<lambda>_. t));
modify (scheduler_action_update (\<lambda>_. resume_cur_thread))
od)
 2. \<And>s. \<lbrakk>(invs and pas_refined aag and (\<lambda>s. pasObjectAbs aag t \<in> pasDomainAbs aag (cur_domain s))) s; pasObjectAbs aag t \<in> reads_scheduler aag l\<rbrakk> \<Longrightarrow> ?P'3 s
 3. pasObjectAbs aag t \<notin> reads_scheduler aag l \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) ?P''3 (do _ <- arch_switch_to_thread t;
_ <- modify (cur_thread_update (\<lambda>_. t));
modify (scheduler_action_update (\<lambda>_. resume_cur_thread))
od)
 4. \<And>s. \<lbrakk>(invs and pas_refined aag and (\<lambda>s. pasObjectAbs aag t \<in> pasDomainAbs aag (cur_domain s))) s; pasObjectAbs aag t \<notin> reads_scheduler aag l\<rbrakk> \<Longrightarrow> ?P''3 s
 5. \<And>s. (invs and pas_refined aag and (\<lambda>s. pasObjectAbs aag t \<in> pasDomainAbs aag (cur_domain s))) s \<Longrightarrow> pasObjectAbs aag t \<in> pasDomainAbs aag (cur_domain s)
 6. \<And>s. (invs and pas_refined aag and (\<lambda>s. pasObjectAbs aag t \<in> pasDomainAbs aag (cur_domain s))) s \<Longrightarrow> (invs and pas_refined aag and (\<lambda>s. pasObjectAbs aag t \<in> pasDomainAbs aag (cur_domain s))) s proof (prove)
goal (6 subgoals):
 1. pasObjectAbs aag t \<in> reads_scheduler aag l \<Longrightarrow> midstrength_reads_respects_scheduler aag l ?P'3 (do x <- set_vm_root t;
_ <- do_machine_op clearExMonitor;
_ <- modify (cur_thread_update (\<lambda>_. t));
modify (scheduler_action_update (\<lambda>_. resume_cur_thread))
od)
 2. \<And>s. \<lbrakk>(invs and pas_refined aag and (\<lambda>s. pasObjectAbs aag t \<in> pasDomainAbs aag (cur_domain s))) s; pasObjectAbs aag t \<in> reads_scheduler aag l\<rbrakk> \<Longrightarrow> ?P'3 s
 3. pasObjectAbs aag t \<notin> reads_scheduler aag l \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) ?P''3 (do _ <- arch_switch_to_thread t;
_ <- modify (cur_thread_update (\<lambda>_. t));
modify (scheduler_action_update (\<lambda>_. resume_cur_thread))
od)
 4. \<And>s. \<lbrakk>(invs and pas_refined aag and (\<lambda>s. pasObjectAbs aag t \<in> pasDomainAbs aag (cur_domain s))) s; pasObjectAbs aag t \<notin> reads_scheduler aag l\<rbrakk> \<Longrightarrow> ?P''3 s
 5. \<And>s. (invs and pas_refined aag and (\<lambda>s. pasObjectAbs aag t \<in> pasDomainAbs aag (cur_domain s))) s \<Longrightarrow> pasObjectAbs aag t \<in> pasDomainAbs aag (cur_domain s)
 6. \<And>s. (invs and pas_refined aag and (\<lambda>s. pasObjectAbs aag t \<in> pasDomainAbs aag (cur_domain s))) s \<Longrightarrow> (invs and pas_refined aag and (\<lambda>s. pasObjectAbs aag t \<in> pasDomainAbs aag (cur_domain s))) s proof (prove)
goal (8 subgoals):
 1. \<And>rv. pasObjectAbs aag t \<in> reads_scheduler aag l \<Longrightarrow> equiv_valid (scheduler_equiv aag) ?B9 (scheduler_affects_equiv aag l) (?Q9 rv) (do _ <- do_machine_op clearExMonitor;
_ <- modify (cur_thread_update (\<lambda>_. t));
modify (scheduler_action_update (\<lambda>_. resume_cur_thread))
od)
 2. pasObjectAbs aag t \<in> reads_scheduler aag l \<Longrightarrow> equiv_valid (scheduler_equiv aag) (midstrength_scheduler_affects_equiv aag l) ?B9 ?P'9 (set_vm_root t)
 3. pasObjectAbs aag t \<in> reads_scheduler aag l \<Longrightarrow> \<lbrace>?P''9\<rbrace> set_vm_root t \<lbrace>?Q9\<rbrace>
 4. \<And>s. \<lbrakk>(invs and pas_refined aag and (\<lambda>s. pasObjectAbs aag t \<in> pasDomainAbs aag (cur_domain s))) s; pasObjectAbs aag t \<in> reads_scheduler aag l\<rbrakk> \<Longrightarrow> ?P'9 s \<and> ?P''9 s
 5. pasObjectAbs aag t \<notin> reads_scheduler aag l \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) ?P''3 (do _ <- arch_switch_to_thread t;
_ <- modify (cur_thread_update (\<lambda>_. t));
modify (scheduler_action_update (\<lambda>_. resume_cur_thread))
od)
 6. \<And>s. \<lbrakk>(invs and pas_refined aag and (\<lambda>s. pasObjectAbs aag t \<in> pasDomainAbs aag (cur_domain s))) s; pasObjectAbs aag t \<notin> reads_scheduler aag l\<rbrakk> \<Longrightarrow> ?P''3 s
 7. \<And>s. (invs and pas_refined aag and (\<lambda>s. pasObjectAbs aag t \<in> pasDomainAbs aag (cur_domain s))) s \<Longrightarrow> pasObjectAbs aag t \<in> pasDomainAbs aag (cur_domain s)
 8. \<And>s. (invs and pas_refined aag and (\<lambda>s. pasObjectAbs aag t \<in> pasDomainAbs aag (cur_domain s))) s \<Longrightarrow> (invs and pas_refined aag and (\<lambda>s. pasObjectAbs aag t \<in> pasDomainAbs aag (cur_domain s))) s proof (prove)
goal (8 subgoals):
 1. \<And>rv. pasObjectAbs aag t \<in> reads_scheduler aag l \<Longrightarrow> equiv_valid (scheduler_equiv aag) ?B9 (scheduler_affects_equiv aag l) (?Q9 rv) (do _ <- do_machine_op clearExMonitor;
_ <- modify (cur_thread_update (\<lambda>_. t));
set_scheduler_action resume_cur_thread
od)
 2. pasObjectAbs aag t \<in> reads_scheduler aag l \<Longrightarrow> equiv_valid (scheduler_equiv aag) (midstrength_scheduler_affects_equiv aag l) ?B9 ?P'9 (set_vm_root t)
 3. pasObjectAbs aag t \<in> reads_scheduler aag l \<Longrightarrow> \<lbrace>?P''9\<rbrace> set_vm_root t \<lbrace>?Q9\<rbrace>
 4. \<And>s. \<lbrakk>(invs and pas_refined aag and (\<lambda>s. pasObjectAbs aag t \<in> pasDomainAbs aag (cur_domain s))) s; pasObjectAbs aag t \<in> reads_scheduler aag l\<rbrakk> \<Longrightarrow> ?P'9 s \<and> ?P''9 s
 5. pasObjectAbs aag t \<notin> reads_scheduler aag l \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) ?P''3 (do _ <- arch_switch_to_thread t;
_ <- modify (cur_thread_update (\<lambda>_. t));
set_scheduler_action resume_cur_thread
od)
 6. \<And>s. \<lbrakk>(invs and pas_refined aag and (\<lambda>s. pasObjectAbs aag t \<in> pasDomainAbs aag (cur_domain s))) s; pasObjectAbs aag t \<notin> reads_scheduler aag l\<rbrakk> \<Longrightarrow> ?P''3 s
 7. \<And>s. (invs and pas_refined aag and (\<lambda>s. pasObjectAbs aag t \<in> pasDomainAbs aag (cur_domain s))) s \<Longrightarrow> pasObjectAbs aag t \<in> pasDomainAbs aag (cur_domain s)
 8. \<And>s. (invs and pas_refined aag and (\<lambda>s. pasObjectAbs aag t \<in> pasDomainAbs aag (cur_domain s))) s \<Longrightarrow> (invs and pas_refined aag and (\<lambda>s. pasObjectAbs aag t \<in> pasDomainAbs aag (cur_domain s))) s proof (prove)
goal (7 subgoals):
 1. pasObjectAbs aag t \<in> reads_scheduler aag l \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) (midstrength_scheduler_affects_equiv aag l) ?P'9 (set_vm_root t)
 2. pasObjectAbs aag t \<in> reads_scheduler aag l \<Longrightarrow> \<lbrace>?P''9\<rbrace> set_vm_root t \<lbrace>\<lambda>rv. invs\<rbrace>
 3. \<And>s. \<lbrakk>(invs and pas_refined aag and (\<lambda>s. pasObjectAbs aag t \<in> pasDomainAbs aag (cur_domain s))) s; pasObjectAbs aag t \<in> reads_scheduler aag l\<rbrakk> \<Longrightarrow> ?P'9 s \<and> ?P''9 s
 4. pasObjectAbs aag t \<notin> reads_scheduler aag l \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) ?P''3 (do _ <- arch_switch_to_thread t;
_ <- modify (cur_thread_update (\<lambda>_. t));
set_scheduler_action resume_cur_thread
od)
 5. \<And>s. \<lbrakk>(invs and pas_refined aag and (\<lambda>s. pasObjectAbs aag t \<in> pasDomainAbs aag (cur_domain s))) s; pasObjectAbs aag t \<notin> reads_scheduler aag l\<rbrakk> \<Longrightarrow> ?P''3 s
 6. \<And>s. (invs and pas_refined aag and (\<lambda>s. pasObjectAbs aag t \<in> pasDomainAbs aag (cur_domain s))) s \<Longrightarrow> pasObjectAbs aag t \<in> pasDomainAbs aag (cur_domain s)
 7. \<And>s. (invs and pas_refined aag and (\<lambda>s. pasObjectAbs aag t \<in> pasDomainAbs aag (cur_domain s))) s \<Longrightarrow> (invs and pas_refined aag and (\<lambda>s. pasObjectAbs aag t \<in> pasDomainAbs aag (cur_domain s))) s proof (prove)
goal (11 subgoals):
 1. \<And>st. pasObjectAbs aag t \<in> reads_scheduler aag l \<Longrightarrow> \<lbrace>(\<lambda>_. True) and scheduler_equiv aag st and midstrength_scheduler_affects_equiv aag l st\<rbrace> set_vm_root t \<lbrace>\<lambda>_. scheduler_equiv aag st\<rbrace>
 2. \<And>st. pasObjectAbs aag t \<in> reads_scheduler aag l \<Longrightarrow> \<lbrace>(\<lambda>_. True) and scheduler_equiv aag st and midstrength_scheduler_affects_equiv aag l st\<rbrace> set_vm_root t \<lbrace>\<lambda>_. midstrength_scheduler_affects_equiv aag l st\<rbrace>
 3. pasObjectAbs aag t \<in> reads_scheduler aag l \<Longrightarrow> \<forall>s s'. scheduler_equiv aag s s' \<and> midstrength_scheduler_affects_equiv aag l s s' \<longrightarrow> scheduler_equiv aag s' s \<and> midstrength_scheduler_affects_equiv aag l s' s
 4. pasObjectAbs aag t \<in> reads_scheduler aag l \<Longrightarrow> \<forall>s s' s''. scheduler_equiv aag s s' \<and> midstrength_scheduler_affects_equiv aag l s s' \<longrightarrow> scheduler_equiv aag s' s'' \<and> midstrength_scheduler_affects_equiv aag l s' s'' \<longrightarrow> scheduler_equiv aag s s'' \<and> midstrength_scheduler_affects_equiv aag l s s''
 5. \<And>s. \<lbrakk>pasObjectAbs aag t \<in> reads_scheduler aag l; ?P'9 s\<rbrakk> \<Longrightarrow> True \<and> True
 6. pasObjectAbs aag t \<in> reads_scheduler aag l \<Longrightarrow> \<lbrace>?P''9\<rbrace> set_vm_root t \<lbrace>\<lambda>rv. invs\<rbrace>
 7. \<And>s. \<lbrakk>(invs and pas_refined aag and (\<lambda>s. pasObjectAbs aag t \<in> pasDomainAbs aag (cur_domain s))) s; pasObjectAbs aag t \<in> reads_scheduler aag l\<rbrakk> \<Longrightarrow> ?P'9 s \<and> ?P''9 s
 8. pasObjectAbs aag t \<notin> reads_scheduler aag l \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) ?P''3 (do _ <- arch_switch_to_thread t;
_ <- modify (cur_thread_update (\<lambda>_. t));
set_scheduler_action resume_cur_thread
od)
 9. \<And>s. \<lbrakk>(invs and pas_refined aag and (\<lambda>s. pasObjectAbs aag t \<in> pasDomainAbs aag (cur_domain s))) s; pasObjectAbs aag t \<notin> reads_scheduler aag l\<rbrakk> \<Longrightarrow> ?P''3 s
 10. \<And>s. (invs and pas_refined aag and (\<lambda>s. pasObjectAbs aag t \<in> pasDomainAbs aag (cur_domain s))) s \<Longrightarrow> pasObjectAbs aag t \<in> pasDomainAbs aag (cur_domain s)
A total of 11 subgoals... proof (prove)
goal (12 subgoals):
 1. \<And>st. pasObjectAbs aag t \<in> reads_scheduler aag l \<Longrightarrow> \<lbrace>?Q17 st\<rbrace> set_vm_root t \<lbrace>\<lambda>_. scheduler_equiv aag st\<rbrace>
 2. \<And>st s. \<lbrakk>pasObjectAbs aag t \<in> reads_scheduler aag l; ((\<lambda>_. True) and scheduler_equiv aag st and midstrength_scheduler_affects_equiv aag l st) s\<rbrakk> \<Longrightarrow> ?Q17 st s
 3. \<And>st. pasObjectAbs aag t \<in> reads_scheduler aag l \<Longrightarrow> \<lbrace>(\<lambda>_. True) and scheduler_equiv aag st and midstrength_scheduler_affects_equiv aag l st\<rbrace> set_vm_root t \<lbrace>\<lambda>_. midstrength_scheduler_affects_equiv aag l st\<rbrace>
 4. pasObjectAbs aag t \<in> reads_scheduler aag l \<Longrightarrow> \<forall>s s'. scheduler_equiv aag s s' \<and> midstrength_scheduler_affects_equiv aag l s s' \<longrightarrow> scheduler_equiv aag s' s \<and> midstrength_scheduler_affects_equiv aag l s' s
 5. pasObjectAbs aag t \<in> reads_scheduler aag l \<Longrightarrow> \<forall>s s' s''. scheduler_equiv aag s s' \<and> midstrength_scheduler_affects_equiv aag l s s' \<longrightarrow> scheduler_equiv aag s' s'' \<and> midstrength_scheduler_affects_equiv aag l s' s'' \<longrightarrow> scheduler_equiv aag s s'' \<and> midstrength_scheduler_affects_equiv aag l s s''
 6. \<And>s. \<lbrakk>pasObjectAbs aag t \<in> reads_scheduler aag l; ?P'9 s\<rbrakk> \<Longrightarrow> True \<and> True
 7. pasObjectAbs aag t \<in> reads_scheduler aag l \<Longrightarrow> \<lbrace>?P''9\<rbrace> set_vm_root t \<lbrace>\<lambda>rv. invs\<rbrace>
 8. \<And>s. \<lbrakk>(invs and pas_refined aag and (\<lambda>s. pasObjectAbs aag t \<in> pasDomainAbs aag (cur_domain s))) s; pasObjectAbs aag t \<in> reads_scheduler aag l\<rbrakk> \<Longrightarrow> ?P'9 s \<and> ?P''9 s
 9. pasObjectAbs aag t \<notin> reads_scheduler aag l \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) ?P''3 (do _ <- arch_switch_to_thread t;
_ <- modify (cur_thread_update (\<lambda>_. t));
set_scheduler_action resume_cur_thread
od)
 10. \<And>s. \<lbrakk>(invs and pas_refined aag and (\<lambda>s. pasObjectAbs aag t \<in> pasDomainAbs aag (cur_domain s))) s; pasObjectAbs aag t \<notin> reads_scheduler aag l\<rbrakk> \<Longrightarrow> ?P''3 s
A total of 12 subgoals... proof (prove)
goal (17 subgoals):
 1. \<And>st sta. pasObjectAbs aag t \<in> reads_scheduler aag l \<Longrightarrow> \<lbrace>(\<lambda>_. True) and globals_equiv_scheduler sta\<rbrace> set_vm_root t \<lbrace>\<lambda>_. globals_equiv_scheduler sta\<rbrace>
 2. \<And>st Q. pasObjectAbs aag t \<in> reads_scheduler aag l \<Longrightarrow> \<lbrace>(\<lambda>_. True) and (\<lambda>s. Q (cur_domain s))\<rbrace> set_vm_root t \<lbrace>\<lambda>r s. Q (cur_domain s)\<rbrace>
 3. \<And>st P. pasObjectAbs aag t \<in> reads_scheduler aag l \<Longrightarrow> \<lbrace>\<lambda>s. P (idle_thread s)\<rbrace> set_vm_root t \<lbrace>\<lambda>_ s. P (idle_thread s)\<rbrace>
 4. \<And>st Q. pasObjectAbs aag t \<in> reads_scheduler aag l \<Longrightarrow> \<lbrace>(\<lambda>_. True) and (\<lambda>s. Q (domain_time s) (domain_index s) (domain_list s))\<rbrace> set_vm_root t \<lbrace>\<lambda>_ s. Q (domain_time s) (domain_index s) (domain_list s)\<rbrace>
 5. \<And>st P. pasObjectAbs aag t \<in> reads_scheduler aag l \<Longrightarrow> \<lbrace>\<lambda>s. P (irq_state_of_state s)\<rbrace> set_vm_root t \<lbrace>\<lambda>_ s. P (irq_state_of_state s)\<rbrace>
 6. \<And>st sta. pasObjectAbs aag t \<in> reads_scheduler aag l \<Longrightarrow> \<lbrace>(\<lambda>_. True) and silc_dom_equiv aag sta\<rbrace> set_vm_root t \<lbrace>\<lambda>_. silc_dom_equiv aag sta\<rbrace>
 7. \<And>st s. \<lbrakk>pasObjectAbs aag t \<in> reads_scheduler aag l; ((\<lambda>_. True) and scheduler_equiv aag st and midstrength_scheduler_affects_equiv aag l st) s\<rbrakk> \<Longrightarrow> ((\<lambda>_. True) and scheduler_equiv aag st) s
 8. \<And>st. pasObjectAbs aag t \<in> reads_scheduler aag l \<Longrightarrow> \<lbrace>(\<lambda>_. True) and scheduler_equiv aag st and midstrength_scheduler_affects_equiv aag l st\<rbrace> set_vm_root t \<lbrace>\<lambda>_. midstrength_scheduler_affects_equiv aag l st\<rbrace>
 9. pasObjectAbs aag t \<in> reads_scheduler aag l \<Longrightarrow> \<forall>s s'. scheduler_equiv aag s s' \<and> midstrength_scheduler_affects_equiv aag l s s' \<longrightarrow> scheduler_equiv aag s' s \<and> midstrength_scheduler_affects_equiv aag l s' s
 10. pasObjectAbs aag t \<in> reads_scheduler aag l \<Longrightarrow> \<forall>s s' s''. scheduler_equiv aag s s' \<and> midstrength_scheduler_affects_equiv aag l s s' \<longrightarrow> scheduler_equiv aag s' s'' \<and> midstrength_scheduler_affects_equiv aag l s' s'' \<longrightarrow> scheduler_equiv aag s s'' \<and> midstrength_scheduler_affects_equiv aag l s s''
A total of 17 subgoals... proof (prove)
goal (10 subgoals):
 1. \<And>st. pasObjectAbs aag t \<in> reads_scheduler aag l \<Longrightarrow> \<lbrace>scheduler_equiv aag st and midstrength_scheduler_affects_equiv aag l st\<rbrace> set_vm_root t \<lbrace>\<lambda>_. midstrength_scheduler_affects_equiv aag l st\<rbrace>
 2. pasObjectAbs aag t \<in> reads_scheduler aag l \<Longrightarrow> \<forall>s s'. scheduler_equiv aag s s' \<and> midstrength_scheduler_affects_equiv aag l s s' \<longrightarrow> scheduler_equiv aag s' s \<and> midstrength_scheduler_affects_equiv aag l s' s
 3. pasObjectAbs aag t \<in> reads_scheduler aag l \<Longrightarrow> \<forall>s s' s''. scheduler_equiv aag s s' \<and> midstrength_scheduler_affects_equiv aag l s s' \<longrightarrow> scheduler_equiv aag s' s'' \<and> midstrength_scheduler_affects_equiv aag l s' s'' \<longrightarrow> scheduler_equiv aag s s'' \<and> midstrength_scheduler_affects_equiv aag l s s''
 4. \<And>s. \<lbrakk>pasObjectAbs aag t \<in> reads_scheduler aag l; ?P'9 s\<rbrakk> \<Longrightarrow> True \<and> True
 5. pasObjectAbs aag t \<in> reads_scheduler aag l \<Longrightarrow> \<lbrace>?P''9\<rbrace> set_vm_root t \<lbrace>\<lambda>rv. invs\<rbrace>
 6. \<And>s. \<lbrakk>(invs and pas_refined aag and (\<lambda>s. pasObjectAbs aag t \<in> pasDomainAbs aag (cur_domain s))) s; pasObjectAbs aag t \<in> reads_scheduler aag l\<rbrakk> \<Longrightarrow> ?P'9 s \<and> ?P''9 s
 7. pasObjectAbs aag t \<notin> reads_scheduler aag l \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) ?P''3 (do _ <- arch_switch_to_thread t;
_ <- modify (cur_thread_update (\<lambda>_. t));
set_scheduler_action resume_cur_thread
od)
 8. \<And>s. \<lbrakk>(invs and pas_refined aag and (\<lambda>s. pasObjectAbs aag t \<in> pasDomainAbs aag (cur_domain s))) s; pasObjectAbs aag t \<notin> reads_scheduler aag l\<rbrakk> \<Longrightarrow> ?P''3 s
 9. \<And>s. (invs and pas_refined aag and (\<lambda>s. pasObjectAbs aag t \<in> pasDomainAbs aag (cur_domain s))) s \<Longrightarrow> pasObjectAbs aag t \<in> pasDomainAbs aag (cur_domain s)
 10. \<And>s. (invs and pas_refined aag and (\<lambda>s. pasObjectAbs aag t \<in> pasDomainAbs aag (cur_domain s))) s \<Longrightarrow> (invs and pas_refined aag and (\<lambda>s. pasObjectAbs aag t \<in> pasDomainAbs aag (cur_domain s))) s proof (prove)
goal (9 subgoals):
 1. pasObjectAbs aag t \<in> reads_scheduler aag l \<Longrightarrow> \<forall>s s'. scheduler_equiv aag s s' \<and> midstrength_scheduler_affects_equiv aag l s s' \<longrightarrow> scheduler_equiv aag s' s \<and> midstrength_scheduler_affects_equiv aag l s' s
 2. pasObjectAbs aag t \<in> reads_scheduler aag l \<Longrightarrow> \<forall>s s' s''. scheduler_equiv aag s s' \<and> midstrength_scheduler_affects_equiv aag l s s' \<longrightarrow> scheduler_equiv aag s' s'' \<and> midstrength_scheduler_affects_equiv aag l s' s'' \<longrightarrow> scheduler_equiv aag s s'' \<and> midstrength_scheduler_affects_equiv aag l s s''
 3. \<And>s. \<lbrakk>pasObjectAbs aag t \<in> reads_scheduler aag l; ?P'9 s\<rbrakk> \<Longrightarrow> True \<and> True
 4. pasObjectAbs aag t \<in> reads_scheduler aag l \<Longrightarrow> \<lbrace>?P''9\<rbrace> set_vm_root t \<lbrace>\<lambda>rv. invs\<rbrace>
 5. \<And>s. \<lbrakk>(invs and pas_refined aag and (\<lambda>s. pasObjectAbs aag t \<in> pasDomainAbs aag (cur_domain s))) s; pasObjectAbs aag t \<in> reads_scheduler aag l\<rbrakk> \<Longrightarrow> ?P'9 s \<and> ?P''9 s
 6. pasObjectAbs aag t \<notin> reads_scheduler aag l \<Longrightarrow> equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) ?P''3 (do _ <- arch_switch_to_thread t;
_ <- modify (cur_thread_update (\<lambda>_. t));
set_scheduler_action resume_cur_thread
od)
 7. \<And>s. \<lbrakk>(invs and pas_refined aag and (\<lambda>s. pasObjectAbs aag t \<in> pasDomainAbs aag (cur_domain s))) s; pasObjectAbs aag t \<notin> reads_scheduler aag l\<rbrakk> \<Longrightarrow> ?P''3 s
 8. \<And>s. (invs and pas_refined aag and (\<lambda>s. pasObjectAbs aag t \<in> pasDomainAbs aag (cur_domain s))) s \<Longrightarrow> pasObjectAbs aag t \<in> pasDomainAbs aag (cur_domain s)
 9. \<And>s. (invs and pas_refined aag and (\<lambda>s. pasObjectAbs aag t \<in> pasDomainAbs aag (cur_domain s))) s \<Longrightarrow> (invs and pas_refined aag and (\<lambda>s. pasObjectAbs aag t \<in> pasDomainAbs aag (cur_domain s))) s proof (prove)
goal:
No subgoals!