theory Scheduler_IF

lemma choose_thread_reads_respects_scheduler_other_domain:
  assumes domains_distinct[wp]: "pas_domains_distinct aag"
  shows "reads_respects_scheduler aag l ( invs and pas_refined aag and valid_queues and
                                  (\<lambda>s. \<not> reads_scheduler_cur_domain aag l s)) choose_thread" apply (rule reads_respects_scheduler_unobservable''
                [where P'="\<lambda>s. \<not> reads_scheduler_cur_domain aag l s \<and>
                               invs s \<and> pas_refined aag s \<and> valid_queues s"]) apply (rule hoare_pre) apply (rule scheduler_equiv_lift'[where P="invs"]) apply (simp add: choose_thread_def) apply (wp guarded_switch_to_lift silc_dom_lift | simp)+ apply force apply (simp add: choose_thread_def) apply (wp guarded_switch_to_lift switch_to_idle_thread_unobservable switch_to_thread_unobservable
          | simp)+ apply clarsimp apply (intro impI conjI) apply (simp add: scheduler_equiv_def domain_fields_equiv_def) apply (elim exE) apply (erule any_valid_thread) apply (frule (1) tcb_with_domain_at) apply clarsimp apply (frule (1) tcb_domain_wellformed) apply (force simp: disjoint_iff_not_equal) apply simp done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (invs and pas_refined aag and valid_queues and (\<lambda>s. \<not> reads_scheduler_cur_domain aag l s)) choose_thread proof (prove)
goal (3 subgoals):
 1. \<And>st. \<lbrace>?P and scheduler_equiv aag st and scheduler_affects_equiv aag l st\<rbrace> choose_thread \<lbrace>\<lambda>_. scheduler_equiv aag st\<rbrace>
 2. \<And>st. \<lbrace>(\<lambda>s. \<not> reads_scheduler_cur_domain aag l s \<and> invs s \<and> pas_refined aag s \<and> valid_queues s) and scheduler_equiv aag st and scheduler_affects_equiv aag l st\<rbrace> choose_thread \<lbrace>\<lambda>_. scheduler_affects_equiv aag l st\<rbrace>
 3. \<And>s. (invs and pas_refined aag and valid_queues and (\<lambda>s. \<not> reads_scheduler_cur_domain aag l s)) s \<Longrightarrow> ?P s \<and> \<not> reads_scheduler_cur_domain aag l s \<and> invs s \<and> pas_refined aag s \<and> valid_queues s proof (prove)
goal (4 subgoals):
 1. \<And>st. \<lbrace>?Q4 st\<rbrace> choose_thread \<lbrace>\<lambda>_. scheduler_equiv aag st\<rbrace>
 2. \<And>st s. (?P and scheduler_equiv aag st and scheduler_affects_equiv aag l st) s \<Longrightarrow> ?Q4 st s
 3. \<And>st. \<lbrace>(\<lambda>s. \<not> reads_scheduler_cur_domain aag l s \<and> invs s \<and> pas_refined aag s \<and> valid_queues s) and scheduler_equiv aag st and scheduler_affects_equiv aag l st\<rbrace> choose_thread \<lbrace>\<lambda>_. scheduler_affects_equiv aag l st\<rbrace>
 4. \<And>s. (invs and pas_refined aag and valid_queues and (\<lambda>s. \<not> reads_scheduler_cur_domain aag l s)) s \<Longrightarrow> ?P s \<and> \<not> reads_scheduler_cur_domain aag l s \<and> invs s \<and> pas_refined aag s \<and> valid_queues s proof (prove)
goal (9 subgoals):
 1. \<And>st sta. \<lbrace>invs and globals_equiv_scheduler sta\<rbrace> choose_thread \<lbrace>\<lambda>_. globals_equiv_scheduler sta\<rbrace>
 2. \<And>st Q. \<lbrace>invs and (\<lambda>s. Q (cur_domain s))\<rbrace> choose_thread \<lbrace>\<lambda>r s. Q (cur_domain s)\<rbrace>
 3. \<And>st P. \<lbrace>\<lambda>s. P (idle_thread s)\<rbrace> choose_thread \<lbrace>\<lambda>_ s. P (idle_thread s)\<rbrace>
 4. \<And>st Q. \<lbrace>invs and (\<lambda>s. Q (domain_time s) (domain_index s) (domain_list s))\<rbrace> choose_thread \<lbrace>\<lambda>_ s. Q (domain_time s) (domain_index s) (domain_list s)\<rbrace>
 5. \<And>st P. \<lbrace>\<lambda>s. P (irq_state_of_state s)\<rbrace> choose_thread \<lbrace>\<lambda>_ s. P (irq_state_of_state s)\<rbrace>
 6. \<And>st sta. \<lbrace>invs and silc_dom_equiv aag sta\<rbrace> choose_thread \<lbrace>\<lambda>_. silc_dom_equiv aag sta\<rbrace>
 7. \<And>st s. (?P and scheduler_equiv aag st and scheduler_affects_equiv aag l st) s \<Longrightarrow> (invs and scheduler_equiv aag st) s
 8. \<And>st. \<lbrace>(\<lambda>s. \<not> reads_scheduler_cur_domain aag l s \<and> invs s \<and> pas_refined aag s \<and> valid_queues s) and scheduler_equiv aag st and scheduler_affects_equiv aag l st\<rbrace> choose_thread \<lbrace>\<lambda>_. scheduler_affects_equiv aag l st\<rbrace>
 9. \<And>s. (invs and pas_refined aag and valid_queues and (\<lambda>s. \<not> reads_scheduler_cur_domain aag l s)) s \<Longrightarrow> ?P s \<and> \<not> reads_scheduler_cur_domain aag l s \<and> invs s \<and> pas_refined aag s \<and> valid_queues s proof (prove)
goal (9 subgoals):
 1. \<And>sta. \<lbrace>invs and globals_equiv_scheduler sta\<rbrace> do d <- gets cur_domain;
queues <- gets (\<lambda>s. ready_queues s d);
if \<forall>prio. queues prio = [] then switch_to_idle_thread else guarded_switch_to (hd (max_non_empty_queue queues))
od \<lbrace>\<lambda>_. globals_equiv_scheduler sta\<rbrace>
 2. \<And>st Q. \<lbrace>invs and (\<lambda>s. Q (cur_domain s))\<rbrace> choose_thread \<lbrace>\<lambda>r s. Q (cur_domain s)\<rbrace>
 3. \<And>st P. \<lbrace>\<lambda>s. P (idle_thread s)\<rbrace> choose_thread \<lbrace>\<lambda>_ s. P (idle_thread s)\<rbrace>
 4. \<And>st Q. \<lbrace>invs and (\<lambda>s. Q (domain_time s) (domain_index s) (domain_list s))\<rbrace> choose_thread \<lbrace>\<lambda>_ s. Q (domain_time s) (domain_index s) (domain_list s)\<rbrace>
 5. \<And>st P. \<lbrace>\<lambda>s. P (irq_state_of_state s)\<rbrace> choose_thread \<lbrace>\<lambda>_ s. P (irq_state_of_state s)\<rbrace>
 6. \<And>st sta. \<lbrace>invs and silc_dom_equiv aag sta\<rbrace> choose_thread \<lbrace>\<lambda>_. silc_dom_equiv aag sta\<rbrace>
 7. \<And>st s. (?P and scheduler_equiv aag st and scheduler_affects_equiv aag l st) s \<Longrightarrow> (invs and scheduler_equiv aag st) s
 8. \<And>st. \<lbrace>(\<lambda>s. \<not> reads_scheduler_cur_domain aag l s \<and> invs s \<and> pas_refined aag s \<and> valid_queues s) and scheduler_equiv aag st and scheduler_affects_equiv aag l st\<rbrace> choose_thread \<lbrace>\<lambda>_. scheduler_affects_equiv aag l st\<rbrace>
 9. \<And>s. (invs and pas_refined aag and valid_queues and (\<lambda>s. \<not> reads_scheduler_cur_domain aag l s)) s \<Longrightarrow> ?P s \<and> \<not> reads_scheduler_cur_domain aag l s \<and> invs s \<and> pas_refined aag s \<and> valid_queues s proof (prove)
goal (3 subgoals):
 1. \<And>st s. ?P s \<and> scheduler_equiv aag st s \<and> scheduler_affects_equiv aag l st s \<Longrightarrow> invs s \<and> scheduler_equiv aag st s
 2. \<And>st. \<lbrace>(\<lambda>s. \<not> reads_scheduler_cur_domain aag l s \<and> invs s \<and> pas_refined aag s \<and> valid_queues s) and scheduler_equiv aag st and scheduler_affects_equiv aag l st\<rbrace> choose_thread \<lbrace>\<lambda>_. scheduler_affects_equiv aag l st\<rbrace>
 3. \<And>s. (invs and pas_refined aag and valid_queues and (\<lambda>s. \<not> reads_scheduler_cur_domain aag l s)) s \<Longrightarrow> ?P s \<and> \<not> reads_scheduler_cur_domain aag l s \<and> invs s \<and> pas_refined aag s \<and> valid_queues s proof (prove)
goal (2 subgoals):
 1. \<And>st. \<lbrace>(\<lambda>s. \<not> reads_scheduler_cur_domain aag l s \<and> invs s \<and> pas_refined aag s \<and> valid_queues s) and scheduler_equiv aag st and scheduler_affects_equiv aag l st\<rbrace> choose_thread \<lbrace>\<lambda>_. scheduler_affects_equiv aag l st\<rbrace>
 2. \<And>s. (invs and pas_refined aag and valid_queues and (\<lambda>s. \<not> reads_scheduler_cur_domain aag l s)) s \<Longrightarrow> invs s \<and> \<not> reads_scheduler_cur_domain aag l s \<and> invs s \<and> pas_refined aag s \<and> valid_queues s proof (prove)
goal (2 subgoals):
 1. \<And>st. \<lbrace>(\<lambda>s. pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {} \<and> invs s \<and> pas_refined aag s \<and> valid_queues s) and scheduler_equiv aag st and scheduler_affects_equiv aag l st\<rbrace> do d <- gets cur_domain;
queues <- gets (\<lambda>s. ready_queues s d);
if \<forall>prio. queues prio = [] then switch_to_idle_thread else guarded_switch_to (hd (max_non_empty_queue queues))
od \<lbrace>\<lambda>_. scheduler_affects_equiv aag l st\<rbrace>
 2. \<And>s. (invs and pas_refined aag and valid_queues and (\<lambda>s. \<not> reads_scheduler_cur_domain aag l s)) s \<Longrightarrow> invs s \<and> \<not> reads_scheduler_cur_domain aag l s \<and> invs s \<and> pas_refined aag s \<and> valid_queues s proof (prove)
goal (2 subgoals):
 1. \<And>st s. pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {} \<and> invs s \<and> pas_refined aag s \<and> valid_queues s \<and> scheduler_equiv aag st s \<and> scheduler_affects_equiv aag l st s \<Longrightarrow> ((\<forall>prio. ready_queues s (cur_domain s) prio = []) \<longrightarrow> cur_domain s = cur_domain st) \<and> ((\<exists>prio. ready_queues s (cur_domain s) prio \<noteq> []) \<longrightarrow> pasObjectAbs aag (hd (max_non_empty_queue (ready_queues s (cur_domain s)))) \<notin> reads_scheduler aag l)
 2. \<And>s. (invs and pas_refined aag and valid_queues and (\<lambda>s. \<not> reads_scheduler_cur_domain aag l s)) s \<Longrightarrow> invs s \<and> \<not> reads_scheduler_cur_domain aag l s \<and> invs s \<and> pas_refined aag s \<and> valid_queues s proof (prove)
goal (2 subgoals):
 1. \<And>st s. \<lbrakk>pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {}; invs s; pas_refined aag s; valid_queues s; scheduler_equiv aag st s; scheduler_affects_equiv aag l st s\<rbrakk> \<Longrightarrow> ((\<forall>prio. ready_queues s (cur_domain s) prio = []) \<longrightarrow> cur_domain s = cur_domain st) \<and> ((\<exists>prio. ready_queues s (cur_domain s) prio \<noteq> []) \<longrightarrow> pasObjectAbs aag (hd (max_non_empty_queue (ready_queues s (cur_domain s)))) \<notin> reads_scheduler aag l)
 2. \<And>s. (invs and pas_refined aag and valid_queues and (\<lambda>s. \<not> reads_scheduler_cur_domain aag l s)) s \<Longrightarrow> invs s \<and> \<not> reads_scheduler_cur_domain aag l s \<and> invs s \<and> pas_refined aag s \<and> valid_queues s proof (prove)
goal (3 subgoals):
 1. \<And>st s. \<lbrakk>pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {}; invs s; pas_refined aag s; valid_queues s; scheduler_equiv aag st s; scheduler_affects_equiv aag l st s; \<forall>prio. ready_queues s (cur_domain s) prio = []\<rbrakk> \<Longrightarrow> cur_domain s = cur_domain st
 2. \<And>st s. \<lbrakk>pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {}; invs s; pas_refined aag s; valid_queues s; scheduler_equiv aag st s; scheduler_affects_equiv aag l st s; \<exists>prio. ready_queues s (cur_domain s) prio \<noteq> []\<rbrakk> \<Longrightarrow> pasObjectAbs aag (hd (max_non_empty_queue (ready_queues s (cur_domain s)))) \<notin> reads_scheduler aag l
 3. \<And>s. (invs and pas_refined aag and valid_queues and (\<lambda>s. \<not> reads_scheduler_cur_domain aag l s)) s \<Longrightarrow> invs s \<and> \<not> reads_scheduler_cur_domain aag l s \<and> invs s \<and> pas_refined aag s \<and> valid_queues s proof (prove)
goal (2 subgoals):
 1. \<And>st s. \<lbrakk>pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {}; invs s; pas_refined aag s; valid_queues s; scheduler_equiv aag st s; scheduler_affects_equiv aag l st s; \<exists>prio. ready_queues s (cur_domain s) prio \<noteq> []\<rbrakk> \<Longrightarrow> pasObjectAbs aag (hd (max_non_empty_queue (ready_queues s (cur_domain s)))) \<notin> reads_scheduler aag l
 2. \<And>s. (invs and pas_refined aag and valid_queues and (\<lambda>s. \<not> reads_scheduler_cur_domain aag l s)) s \<Longrightarrow> invs s \<and> \<not> reads_scheduler_cur_domain aag l s \<and> invs s \<and> pas_refined aag s \<and> valid_queues s proof (prove)
goal (2 subgoals):
 1. \<And>st s prio. \<lbrakk>pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {}; invs s; pas_refined aag s; valid_queues s; scheduler_equiv aag st s; scheduler_affects_equiv aag l st s; ready_queues s (cur_domain s) prio \<noteq> []\<rbrakk> \<Longrightarrow> pasObjectAbs aag (hd (max_non_empty_queue (ready_queues s (cur_domain s)))) \<notin> reads_scheduler aag l
 2. \<And>s. (invs and pas_refined aag and valid_queues and (\<lambda>s. \<not> reads_scheduler_cur_domain aag l s)) s \<Longrightarrow> invs s \<and> \<not> reads_scheduler_cur_domain aag l s \<and> invs s \<and> pas_refined aag s \<and> valid_queues s proof (prove)
goal (2 subgoals):
 1. \<And>st s prio x prioa. \<lbrakk>pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {}; invs s; pas_refined aag s; valid_queues s; scheduler_equiv aag st s; scheduler_affects_equiv aag l st s; x \<in> set (ready_queues s (cur_domain s) prioa)\<rbrakk> \<Longrightarrow> pasObjectAbs aag x \<notin> reads_scheduler aag l
 2. \<And>s. (invs and pas_refined aag and valid_queues and (\<lambda>s. \<not> reads_scheduler_cur_domain aag l s)) s \<Longrightarrow> invs s \<and> \<not> reads_scheduler_cur_domain aag l s \<and> invs s \<and> pas_refined aag s \<and> valid_queues s proof (prove)
goal (2 subgoals):
 1. \<And>st s prio x prioa. \<lbrakk>pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {}; invs s; pas_refined aag s; valid_queues s; scheduler_equiv aag st s; scheduler_affects_equiv aag l st s; x \<in> set (ready_queues s (cur_domain s) prioa); \<exists>t. ekheap s x = Some t \<and> tcb_domain t = cur_domain s\<rbrakk> \<Longrightarrow> pasObjectAbs aag x \<notin> reads_scheduler aag l
 2. \<And>s. (invs and pas_refined aag and valid_queues and (\<lambda>s. \<not> reads_scheduler_cur_domain aag l s)) s \<Longrightarrow> invs s \<and> \<not> reads_scheduler_cur_domain aag l s \<and> invs s \<and> pas_refined aag s \<and> valid_queues s proof (prove)
goal (2 subgoals):
 1. \<And>st s x prioa t. \<lbrakk>pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {}; invs s; pas_refined aag s; valid_queues s; scheduler_equiv aag st s; scheduler_affects_equiv aag l st s; x \<in> set (ready_queues s (cur_domain s) prioa); ekheap s x = Some t; tcb_domain t = cur_domain s; pasObjectAbs aag x \<in> reads_scheduler aag l\<rbrakk> \<Longrightarrow> False
 2. \<And>s. (invs and pas_refined aag and valid_queues and (\<lambda>s. \<not> reads_scheduler_cur_domain aag l s)) s \<Longrightarrow> invs s \<and> \<not> reads_scheduler_cur_domain aag l s \<and> invs s \<and> pas_refined aag s \<and> valid_queues s proof (prove)
goal (2 subgoals):
 1. \<And>st s x prioa t. \<lbrakk>pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {}; invs s; pas_refined aag s; valid_queues s; scheduler_equiv aag st s; scheduler_affects_equiv aag l st s; x \<in> set (ready_queues s (cur_domain s) prioa); ekheap s x = Some t; tcb_domain t = cur_domain s; pasObjectAbs aag x \<in> reads_scheduler aag l; pasObjectAbs aag x \<in> pasDomainAbs aag (tcb_domain t)\<rbrakk> \<Longrightarrow> False
 2. \<And>s. (invs and pas_refined aag and valid_queues and (\<lambda>s. \<not> reads_scheduler_cur_domain aag l s)) s \<Longrightarrow> invs s \<and> \<not> reads_scheduler_cur_domain aag l s \<and> invs s \<and> pas_refined aag s \<and> valid_queues s proof (prove)
goal (1 subgoal):
 1. \<And>s. (invs and pas_refined aag and valid_queues and (\<lambda>s. \<not> reads_scheduler_cur_domain aag l s)) s \<Longrightarrow> invs s \<and> \<not> reads_scheduler_cur_domain aag l s \<and> invs s \<and> pas_refined aag s \<and> valid_queues s proof (prove)
goal:
No subgoals!