theory Scheduler_IF

lemma reads_respects_scheduler_invisible_no_domain_switch:
  assumes domains_distinct[wp]: "pas_domains_distinct aag"
  shows
  "reads_respects_scheduler aag l
     (\<lambda>s. pas_refined aag s \<and> invs s \<and> valid_sched s \<and> guarded_pas_domain aag s
                            \<and> domain_time s \<noteq> 0 \<and> \<not> reads_scheduler_cur_domain aag l s)
     schedule" supply ethread_get_wp[wp del] if_split[split del] apply (rule reads_respects_scheduler_unobservable''[where P=Q and P'=Q and Q=Q for Q]) apply (rule hoare_pre) apply (rule scheduler_equiv_lift'[where P="invs and (\<lambda>s. domain_time s \<noteq> 0)"]) apply (wp schedule_no_domain_switch schedule_no_domain_fields
                    silc_dom_lift | simp)+ apply (simp add: schedule_def) apply (wp guarded_switch_to_lift
             scheduler_equiv_lift
             schedule_choose_new_thread_schedule_affects_no_switch
             set_scheduler_action_unobservable
             tcb_sched_action_unobservable
             switch_to_thread_unobservable silc_dom_lift
             gts_wp
             hoare_vcg_all_lift
             hoare_vcg_disj_lift
          | wpc | simp
          | rule hoare_pre_cont[where f=next_domain]
          | wp (once) hoare_drop_imp[where f="set_scheduler_action choose_new_thread"])+ 
            (* stop on fastfail calculation *)
             apply (clarsimp simp: conj_ac cong: imp_cong conj_cong) apply (wp hoare_drop_imps)[1] apply (wp tcb_sched_action_unobservable gts_wp
                     schedule_choose_new_thread_schedule_affects_no_switch)+ apply (clarsimp simp: if_apply_def2) 
   (* slow 15s *)
    by (safe; (fastforce simp: switch_thread_runnable
              | fastforce dest!: switch_to_cur_domain cur_thread_cur_domain
              | fastforce simp: st_tcb_at_def obj_at_def))+

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (\<lambda>s. pas_refined aag s \<and> invs s \<and> valid_sched s \<and> guarded_pas_domain aag s \<and> domain_time s \<noteq> 0 \<and> \<not> reads_scheduler_cur_domain aag l s) schedule proof (prove)
goal (1 subgoal):
 1. equiv_valid_inv (scheduler_equiv aag) (scheduler_affects_equiv aag l) (\<lambda>s. pas_refined aag s \<and> invs s \<and> valid_sched s \<and> guarded_pas_domain aag s \<and> domain_time s \<noteq> 0 \<and> \<not> reads_scheduler_cur_domain aag l s) schedule proof (prove)
goal (3 subgoals):
 1. \<And>st. \<lbrace>(\<lambda>s. pas_refined aag s \<and> invs s \<and> valid_sched s \<and> guarded_pas_domain aag s \<and> domain_time s \<noteq> 0 \<and> \<not> reads_scheduler_cur_domain aag l s) and scheduler_equiv aag st and scheduler_affects_equiv aag l st\<rbrace> schedule \<lbrace>\<lambda>_. scheduler_equiv aag st\<rbrace>
 2. \<And>st. \<lbrace>(\<lambda>s. pas_refined aag s \<and> invs s \<and> valid_sched s \<and> guarded_pas_domain aag s \<and> domain_time s \<noteq> 0 \<and> \<not> reads_scheduler_cur_domain aag l s) and scheduler_equiv aag st and scheduler_affects_equiv aag l st\<rbrace> schedule \<lbrace>\<lambda>_. scheduler_affects_equiv aag l st\<rbrace>
 3. \<And>s. pas_refined aag s \<and> invs s \<and> valid_sched s \<and> guarded_pas_domain aag s \<and> domain_time s \<noteq> 0 \<and> \<not> reads_scheduler_cur_domain aag l s \<Longrightarrow> (pas_refined aag s \<and> invs s \<and> valid_sched s \<and> guarded_pas_domain aag s \<and> domain_time s \<noteq> 0 \<and> \<not> reads_scheduler_cur_domain aag l s) \<and> pas_refined aag s \<and> invs s \<and> valid_sched s \<and> guarded_pas_domain aag s \<and> domain_time s \<noteq> 0 \<and> \<not> reads_scheduler_cur_domain aag l s proof (prove)
goal (4 subgoals):
 1. \<And>st. \<lbrace>?Q13 st\<rbrace> schedule \<lbrace>\<lambda>_. scheduler_equiv aag st\<rbrace>
 2. \<And>st s. ((\<lambda>s. pas_refined aag s \<and> invs s \<and> valid_sched s \<and> guarded_pas_domain aag s \<and> domain_time s \<noteq> 0 \<and> \<not> reads_scheduler_cur_domain aag l s) and scheduler_equiv aag st and scheduler_affects_equiv aag l st) s \<Longrightarrow> ?Q13 st s
 3. \<And>st. \<lbrace>(\<lambda>s. pas_refined aag s \<and> invs s \<and> valid_sched s \<and> guarded_pas_domain aag s \<and> domain_time s \<noteq> 0 \<and> \<not> reads_scheduler_cur_domain aag l s) and scheduler_equiv aag st and scheduler_affects_equiv aag l st\<rbrace> schedule \<lbrace>\<lambda>_. scheduler_affects_equiv aag l st\<rbrace>
 4. \<And>s. pas_refined aag s \<and> invs s \<and> valid_sched s \<and> guarded_pas_domain aag s \<and> domain_time s \<noteq> 0 \<and> \<not> reads_scheduler_cur_domain aag l s \<Longrightarrow> (pas_refined aag s \<and> invs s \<and> valid_sched s \<and> guarded_pas_domain aag s \<and> domain_time s \<noteq> 0 \<and> \<not> reads_scheduler_cur_domain aag l s) \<and> pas_refined aag s \<and> invs s \<and> valid_sched s \<and> guarded_pas_domain aag s \<and> domain_time s \<noteq> 0 \<and> \<not> reads_scheduler_cur_domain aag l s proof (prove)
goal (9 subgoals):
 1. \<And>st sta. \<lbrace>invs and (\<lambda>s. domain_time s \<noteq> 0) and globals_equiv_scheduler sta\<rbrace> schedule \<lbrace>\<lambda>_. globals_equiv_scheduler sta\<rbrace>
 2. \<And>st Q. \<lbrace>invs and (\<lambda>s. domain_time s \<noteq> 0) and (\<lambda>s. Q (cur_domain s))\<rbrace> schedule \<lbrace>\<lambda>r s. Q (cur_domain s)\<rbrace>
 3. \<And>st P. \<lbrace>\<lambda>s. P (idle_thread s)\<rbrace> schedule \<lbrace>\<lambda>_ s. P (idle_thread s)\<rbrace>
 4. \<And>st Q. \<lbrace>invs and (\<lambda>s. domain_time s \<noteq> 0) and (\<lambda>s. Q (domain_time s) (domain_index s) (domain_list s))\<rbrace> schedule \<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> schedule \<lbrace>\<lambda>_ s. P (irq_state_of_state s)\<rbrace>
 6. \<And>st sta. \<lbrace>invs and (\<lambda>s. domain_time s \<noteq> 0) and silc_dom_equiv aag sta\<rbrace> schedule \<lbrace>\<lambda>_. silc_dom_equiv aag sta\<rbrace>
 7. \<And>st s. ((\<lambda>s. pas_refined aag s \<and> invs s \<and> valid_sched s \<and> guarded_pas_domain aag s \<and> domain_time s \<noteq> 0 \<and> \<not> reads_scheduler_cur_domain aag l s) and scheduler_equiv aag st and scheduler_affects_equiv aag l st) s \<Longrightarrow> (invs and (\<lambda>s. domain_time s \<noteq> 0) and scheduler_equiv aag st) s
 8. \<And>st. \<lbrace>(\<lambda>s. pas_refined aag s \<and> invs s \<and> valid_sched s \<and> guarded_pas_domain aag s \<and> domain_time s \<noteq> 0 \<and> \<not> reads_scheduler_cur_domain aag l s) and scheduler_equiv aag st and scheduler_affects_equiv aag l st\<rbrace> schedule \<lbrace>\<lambda>_. scheduler_affects_equiv aag l st\<rbrace>
 9. \<And>s. pas_refined aag s \<and> invs s \<and> valid_sched s \<and> guarded_pas_domain aag s \<and> domain_time s \<noteq> 0 \<and> \<not> reads_scheduler_cur_domain aag l s \<Longrightarrow> (pas_refined aag s \<and> invs s \<and> valid_sched s \<and> guarded_pas_domain aag s \<and> domain_time s \<noteq> 0 \<and> \<not> reads_scheduler_cur_domain aag l s) \<and> pas_refined aag s \<and> invs s \<and> valid_sched s \<and> guarded_pas_domain aag s \<and> domain_time s \<noteq> 0 \<and> \<not> reads_scheduler_cur_domain aag l s proof (prove)
goal (2 subgoals):
 1. \<And>st. \<lbrace>(\<lambda>s. pas_refined aag s \<and> invs s \<and> valid_sched s \<and> guarded_pas_domain aag s \<and> domain_time s \<noteq> 0 \<and> pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {}) and scheduler_equiv aag st and scheduler_affects_equiv aag l st\<rbrace> schedule \<lbrace>\<lambda>_. scheduler_affects_equiv aag l st\<rbrace>
 2. \<And>s. pas_refined aag s \<and> invs s \<and> valid_sched s \<and> guarded_pas_domain aag s \<and> domain_time s \<noteq> 0 \<and> \<not> reads_scheduler_cur_domain aag l s \<Longrightarrow> (pas_refined aag s \<and> invs s \<and> valid_sched s \<and> guarded_pas_domain aag s \<and> domain_time s \<noteq> 0 \<and> \<not> reads_scheduler_cur_domain aag l s) \<and> pas_refined aag s \<and> invs s \<and> valid_sched s \<and> guarded_pas_domain aag s \<and> domain_time s \<noteq> 0 \<and> \<not> reads_scheduler_cur_domain aag l s proof (prove)
goal (2 subgoals):
 1. \<And>st. \<lbrace>(\<lambda>s. pas_refined aag s \<and> invs s \<and> valid_sched s \<and> guarded_pas_domain aag s \<and> domain_time s \<noteq> 0 \<and> pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {}) and scheduler_equiv aag st and scheduler_affects_equiv aag l st\<rbrace> do ct <- gets cur_thread;
ct_st <- get_thread_state ct;
gets scheduler_action >>= case_scheduler_action (do id <- gets idle_thread;
assert (runnable ct_st \<or> ct = id)
od) (\<lambda>candidate. do y <- when (runnable ct_st) (tcb_sched_action tcb_sched_enqueue ct);
it <- gets idle_thread;
target_prio <- ethread_get tcb_priority candidate;
ct_prio <- ethread_get_when (ct \<noteq> it) tcb_priority ct;
fastfail <- schedule_switch_thread_fastfail ct it ct_prio target_prio;
cur_dom <- gets cur_domain;
highest <- gets (is_highest_prio cur_dom target_prio);
if fastfail \<and> \<not> highest then do tcb_sched_action tcb_sched_enqueue candidate;
set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else if runnable ct_st \<and> ct_prio = target_prio then do tcb_sched_action tcb_sched_append candidate;
set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else do guarded_switch_to candidate;
set_scheduler_action resume_cur_thread
od
od) (do y <- when (runnable ct_st) (tcb_sched_action tcb_sched_enqueue ct);
schedule_choose_new_thread
od)
od \<lbrace>\<lambda>_. scheduler_affects_equiv aag l st\<rbrace>
 2. \<And>s. pas_refined aag s \<and> invs s \<and> valid_sched s \<and> guarded_pas_domain aag s \<and> domain_time s \<noteq> 0 \<and> \<not> reads_scheduler_cur_domain aag l s \<Longrightarrow> (pas_refined aag s \<and> invs s \<and> valid_sched s \<and> guarded_pas_domain aag s \<and> domain_time s \<noteq> 0 \<and> \<not> reads_scheduler_cur_domain aag l s) \<and> pas_refined aag s \<and> invs s \<and> valid_sched s \<and> guarded_pas_domain aag s \<and> domain_time s \<noteq> 0 \<and> \<not> reads_scheduler_cur_domain aag l s proof (prove)
goal (11 subgoals):
 1. \<And>st ct ct_st x x2 it target_prio ct_prio. x = switch_thread x2 \<Longrightarrow> \<lbrace>?B81 st ct ct_st (switch_thread x2) x2 () it target_prio ct_prio\<rbrace> schedule_switch_thread_fastfail ct it ct_prio target_prio \<lbrace>\<lambda>fastfail s. (fastfail \<and> \<not> is_highest_prio (cur_domain s) target_prio s \<longrightarrow> invs s \<and> pas_refined aag s \<and> valid_queues s \<and> st_tcb_at runnable x2 s \<and> domain_time s \<noteq> 0 \<and> pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {} \<and> scheduler_equiv aag st s \<and> pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {} \<and> pas_refined aag s \<and> scheduler_affects_equiv aag l st s \<and> pasObjectAbs aag x2 \<notin> reads_scheduler aag l \<and> cur_domain st = cur_domain s) \<and> ((fastfail \<longrightarrow> is_highest_prio (cur_domain s) target_prio s) \<longrightarrow> (runnable ct_st \<and> ct_prio = target_prio \<longrightarrow> invs s \<and> pas_refined aag s \<and> valid_queues s \<and> st_tcb_at runnable x2 s \<and> domain_time s \<noteq> 0 \<and> pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {} \<and> scheduler_equiv aag st s \<and> pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {} \<and> pas_refined aag s \<and> scheduler_affects_equiv aag l st s \<and> pasObjectAbs aag x2 \<notin> reads_scheduler aag l \<and> cur_domain st = cur_domain s) \<and> ((runnable ct_st \<longrightarrow> ct_prio \<noteq> target_prio) \<longrightarrow> pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {} \<and> pasObjectAbs aag x2 \<notin> reads_scheduler aag l \<and> scheduler_affects_equiv aag l st s \<and> scheduler_equiv aag st s \<and> invs s \<and> pas_refined aag s \<and> cur_domain st = cur_domain s))\<rbrace>
 2. \<And>st ct ct_st x x2 y it target_prio. x = switch_thread x2 \<Longrightarrow> \<lbrace>?B80 st ct ct_st x x2 y it target_prio\<rbrace> ethread_get_when (ct \<noteq> it) tcb_priority ct \<lbrace>?B81 st ct ct_st x x2 y it target_prio\<rbrace>
 3. \<And>st ct ct_st x x2 y it. x = switch_thread x2 \<Longrightarrow> \<lbrace>?B79 st ct ct_st x x2 y it\<rbrace> ethread_get tcb_priority x2 \<lbrace>?B80 st ct ct_st x x2 y it\<rbrace>
 4. \<And>st ct ct_st x x2 y. x = switch_thread x2 \<Longrightarrow> \<lbrace>?B78 st ct ct_st x x2 y\<rbrace> gets idle_thread \<lbrace>?B79 st ct ct_st x x2 y\<rbrace>
 5. \<And>st ct ct_st x x2. x = switch_thread x2 \<Longrightarrow> \<lbrace>?R67 st ct ct_st x x2\<rbrace> when (runnable ct_st) (tcb_sched_action tcb_sched_enqueue ct) \<lbrace>?B78 st ct ct_st x x2\<rbrace>
 6. \<And>st ct ct_st x. x = choose_new_thread \<Longrightarrow> \<lbrace>?R65 st ct ct_st x\<rbrace> do y <- when (runnable ct_st) (tcb_sched_action tcb_sched_enqueue ct);
schedule_choose_new_thread
od \<lbrace>\<lambda>_. scheduler_affects_equiv aag l st\<rbrace>
 7. \<And>st ct ct_st. \<lbrace>?B57 st ct ct_st\<rbrace> gets scheduler_action \<lbrace>\<lambda>x s. (x = resume_cur_thread \<longrightarrow> runnable ct_st \<or> ct = idle_thread s \<longrightarrow> scheduler_affects_equiv aag l st s) \<and> (\<forall>xa. x = switch_thread xa \<longrightarrow> ?R67 st ct ct_st x xa s) \<and> (x = choose_new_thread \<longrightarrow> ?R65 st ct ct_st x s)\<rbrace>
 8. \<And>st ct. \<lbrace>?B56 st ct\<rbrace> get_thread_state ct \<lbrace>?B57 st ct\<rbrace>
 9. \<And>st. \<lbrace>?Q55 st\<rbrace> gets cur_thread \<lbrace>?B56 st\<rbrace>
 10. \<And>st s. ((\<lambda>s. pas_refined aag s \<and> invs s \<and> valid_sched s \<and> guarded_pas_domain aag s \<and> domain_time s \<noteq> 0 \<and> pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {}) and scheduler_equiv aag st and scheduler_affects_equiv aag l st) s \<Longrightarrow> ?Q55 st s
A total of 11 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>st ct ct_st x x2 it target_prio ct_prio. x = switch_thread x2 \<Longrightarrow> \<lbrace>?B81 st ct ct_st (switch_thread x2) x2 () it target_prio ct_prio\<rbrace> schedule_switch_thread_fastfail ct it ct_prio target_prio \<lbrace>\<lambda>fastfail s. (fastfail \<and> \<not> is_highest_prio (cur_domain s) target_prio s \<longrightarrow> invs s \<and> pas_refined aag s \<and> valid_queues s \<and> st_tcb_at runnable x2 s \<and> domain_time s \<noteq> 0 \<and> pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {} \<and> scheduler_equiv aag st s \<and> pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {} \<and> pas_refined aag s \<and> scheduler_affects_equiv aag l st s \<and> pasObjectAbs aag x2 \<notin> reads_scheduler aag l \<and> cur_domain st = cur_domain s) \<and> ((fastfail \<longrightarrow> is_highest_prio (cur_domain s) target_prio s) \<longrightarrow> (runnable ct_st \<and> ct_prio = target_prio \<longrightarrow> invs s \<and> pas_refined aag s \<and> valid_queues s \<and> st_tcb_at runnable x2 s \<and> domain_time s \<noteq> 0 \<and> pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {} \<and> scheduler_equiv aag st s \<and> pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {} \<and> pas_refined aag s \<and> scheduler_affects_equiv aag l st s \<and> pasObjectAbs aag x2 \<notin> reads_scheduler aag l \<and> cur_domain st = cur_domain s) \<and> ((runnable ct_st \<longrightarrow> ct_prio \<noteq> target_prio) \<longrightarrow> pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {} \<and> pasObjectAbs aag x2 \<notin> reads_scheduler aag l \<and> scheduler_affects_equiv aag l st s \<and> scheduler_equiv aag st s \<and> invs s \<and> pas_refined aag s \<and> cur_domain st = cur_domain s))\<rbrace>
 2. \<And>st ct ct_st x x2 y it target_prio. x = switch_thread x2 \<Longrightarrow> \<lbrace>?B80 st ct ct_st x x2 y it target_prio\<rbrace> ethread_get_when (ct \<noteq> it) tcb_priority ct \<lbrace>?B81 st ct ct_st x x2 y it target_prio\<rbrace>
 3. \<And>st ct ct_st x x2 y it. x = switch_thread x2 \<Longrightarrow> \<lbrace>?B79 st ct ct_st x x2 y it\<rbrace> ethread_get tcb_priority x2 \<lbrace>?B80 st ct ct_st x x2 y it\<rbrace>
 4. \<And>st ct ct_st x x2 y. x = switch_thread x2 \<Longrightarrow> \<lbrace>?B78 st ct ct_st x x2 y\<rbrace> gets idle_thread \<lbrace>?B79 st ct ct_st x x2 y\<rbrace>
 5. \<And>st ct ct_st x x2. x = switch_thread x2 \<Longrightarrow> \<lbrace>?R67 st ct ct_st x x2\<rbrace> when (runnable ct_st) (tcb_sched_action tcb_sched_enqueue ct) \<lbrace>?B78 st ct ct_st x x2\<rbrace>
 6. \<And>st ct ct_st x. x = choose_new_thread \<Longrightarrow> \<lbrace>?R65 st ct ct_st x\<rbrace> do y <- when (runnable ct_st) (tcb_sched_action tcb_sched_enqueue ct);
schedule_choose_new_thread
od \<lbrace>\<lambda>_. scheduler_affects_equiv aag l st\<rbrace>
 7. \<And>st ct ct_st. \<lbrace>?B57 st ct ct_st\<rbrace> gets scheduler_action \<lbrace>\<lambda>x s. (x = resume_cur_thread \<longrightarrow> runnable ct_st \<or> ct = idle_thread s \<longrightarrow> scheduler_affects_equiv aag l st s) \<and> (\<forall>xa. x = switch_thread xa \<longrightarrow> ?R67 st ct ct_st x xa s) \<and> (x = choose_new_thread \<longrightarrow> ?R65 st ct ct_st x s)\<rbrace>
 8. \<And>st ct. \<lbrace>?B56 st ct\<rbrace> get_thread_state ct \<lbrace>?B57 st ct\<rbrace>
 9. \<And>st. \<lbrace>?Q55 st\<rbrace> gets cur_thread \<lbrace>?B56 st\<rbrace>
 10. \<And>st s. ((\<lambda>s. pas_refined aag s \<and> invs s \<and> valid_sched s \<and> guarded_pas_domain aag s \<and> domain_time s \<noteq> 0 \<and> pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {}) and scheduler_equiv aag st and scheduler_affects_equiv aag l st) s \<Longrightarrow> ?Q55 st s
A total of 11 subgoals... proof (prove)
goal (11 subgoals):
 1. \<And>st ct ct_st x2 it target_prio ct_prio. \<lbrace>?B81 st ct ct_st (switch_thread x2) x2 () it target_prio ct_prio\<rbrace> schedule_switch_thread_fastfail ct it ct_prio target_prio \<lbrace>\<lambda>fastfail s. (fastfail \<and> \<not> is_highest_prio (cur_domain s) target_prio s \<longrightarrow> invs s \<and> pas_refined aag s \<and> st_tcb_at runnable x2 s \<and> scheduler_equiv aag st s \<and> domain_time s \<noteq> 0 \<and> scheduler_affects_equiv aag l st s \<and> cur_domain st = cur_domain s \<and> pasObjectAbs aag x2 \<notin> reads_scheduler aag l \<and> valid_queues s \<and> pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {}) \<and> ((fastfail \<longrightarrow> is_highest_prio (cur_domain s) target_prio s) \<longrightarrow> ((runnable ct_st \<longrightarrow> ct_prio \<noteq> target_prio) \<longrightarrow> invs s \<and> pas_refined aag s \<and> scheduler_equiv aag st s \<and> scheduler_affects_equiv aag l st s \<and> cur_domain st = cur_domain s \<and> pasObjectAbs aag x2 \<notin> reads_scheduler aag l \<and> pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {}) \<and> (runnable ct_st \<and> ct_prio = target_prio \<longrightarrow> invs s \<and> pas_refined aag s \<and> st_tcb_at runnable x2 s \<and> scheduler_equiv aag st s \<and> domain_time s \<noteq> 0 \<and> scheduler_affects_equiv aag l st s \<and> cur_domain st = cur_domain s \<and> pasObjectAbs aag x2 \<notin> reads_scheduler aag l \<and> valid_queues s \<and> pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {}))\<rbrace>
 2. \<And>st ct ct_st x x2 y it target_prio. x = switch_thread x2 \<Longrightarrow> \<lbrace>?B80 st ct ct_st x x2 y it target_prio\<rbrace> ethread_get_when (ct \<noteq> it) tcb_priority ct \<lbrace>?B81 st ct ct_st x x2 y it target_prio\<rbrace>
 3. \<And>st ct ct_st x x2 y it. x = switch_thread x2 \<Longrightarrow> \<lbrace>?B79 st ct ct_st x x2 y it\<rbrace> ethread_get tcb_priority x2 \<lbrace>?B80 st ct ct_st x x2 y it\<rbrace>
 4. \<And>st ct ct_st x x2 y. x = switch_thread x2 \<Longrightarrow> \<lbrace>?B78 st ct ct_st x x2 y\<rbrace> gets idle_thread \<lbrace>?B79 st ct ct_st x x2 y\<rbrace>
 5. \<And>st ct ct_st x x2. x = switch_thread x2 \<Longrightarrow> \<lbrace>?R67 st ct ct_st x x2\<rbrace> when (runnable ct_st) (tcb_sched_action tcb_sched_enqueue ct) \<lbrace>?B78 st ct ct_st x x2\<rbrace>
 6. \<And>st ct ct_st x. x = choose_new_thread \<Longrightarrow> \<lbrace>?R65 st ct ct_st x\<rbrace> do y <- when (runnable ct_st) (tcb_sched_action tcb_sched_enqueue ct);
schedule_choose_new_thread
od \<lbrace>\<lambda>_. scheduler_affects_equiv aag l st\<rbrace>
 7. \<And>st ct ct_st. \<lbrace>?B57 st ct ct_st\<rbrace> gets scheduler_action \<lbrace>\<lambda>x s. (x = resume_cur_thread \<longrightarrow> runnable ct_st \<or> ct = idle_thread s \<longrightarrow> scheduler_affects_equiv aag l st s) \<and> (\<forall>xa. x = switch_thread xa \<longrightarrow> ?R67 st ct ct_st x xa s) \<and> (x = choose_new_thread \<longrightarrow> ?R65 st ct ct_st x s)\<rbrace>
 8. \<And>st ct. \<lbrace>?B56 st ct\<rbrace> get_thread_state ct \<lbrace>?B57 st ct\<rbrace>
 9. \<And>st. \<lbrace>?Q55 st\<rbrace> gets cur_thread \<lbrace>?B56 st\<rbrace>
 10. \<And>st s. ((\<lambda>s. pas_refined aag s \<and> invs s \<and> valid_sched s \<and> guarded_pas_domain aag s \<and> domain_time s \<noteq> 0 \<and> pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {}) and scheduler_equiv aag st and scheduler_affects_equiv aag l st) s \<Longrightarrow> ?Q55 st s
A total of 11 subgoals... proof (prove)
goal (10 subgoals):
 1. \<And>st ct ct_st x x2 y it target_prio. x = switch_thread x2 \<Longrightarrow> \<lbrace>?B80 st ct ct_st x x2 y it target_prio\<rbrace> ethread_get_when (ct \<noteq> it) tcb_priority ct \<lbrace>\<lambda>a b. (invs b \<and> pas_refined aag b \<and> st_tcb_at runnable x2 b \<and> scheduler_equiv aag st b \<and> domain_time b \<noteq> 0 \<and> scheduler_affects_equiv aag l st b \<and> cur_domain st = cur_domain b \<and> pasObjectAbs aag x2 \<notin> reads_scheduler aag l \<and> valid_queues b \<and> pasDomainAbs aag (cur_domain b) \<inter> reads_scheduler aag l = {}) \<and> (invs b \<and> pas_refined aag b \<and> scheduler_equiv aag st b \<and> scheduler_affects_equiv aag l st b \<and> cur_domain st = cur_domain b \<and> pasObjectAbs aag x2 \<notin> reads_scheduler aag l \<and> pasDomainAbs aag (cur_domain b) \<inter> reads_scheduler aag l = {}) \<and> invs b \<and> pas_refined aag b \<and> st_tcb_at runnable x2 b \<and> scheduler_equiv aag st b \<and> domain_time b \<noteq> 0 \<and> scheduler_affects_equiv aag l st b \<and> cur_domain st = cur_domain b \<and> pasObjectAbs aag x2 \<notin> reads_scheduler aag l \<and> valid_queues b \<and> pasDomainAbs aag (cur_domain b) \<inter> reads_scheduler aag l = {}\<rbrace>
 2. \<And>st ct ct_st x x2 y it. x = switch_thread x2 \<Longrightarrow> \<lbrace>?B79 st ct ct_st x x2 y it\<rbrace> ethread_get tcb_priority x2 \<lbrace>?B80 st ct ct_st x x2 y it\<rbrace>
 3. \<And>st ct ct_st x x2 y. x = switch_thread x2 \<Longrightarrow> \<lbrace>?B78 st ct ct_st x x2 y\<rbrace> gets idle_thread \<lbrace>?B79 st ct ct_st x x2 y\<rbrace>
 4. \<And>st ct ct_st x x2. x = switch_thread x2 \<Longrightarrow> \<lbrace>?R67 st ct ct_st x x2\<rbrace> when (runnable ct_st) (tcb_sched_action tcb_sched_enqueue ct) \<lbrace>?B78 st ct ct_st x x2\<rbrace>
 5. \<And>st ct ct_st x. x = choose_new_thread \<Longrightarrow> \<lbrace>?R65 st ct ct_st x\<rbrace> do y <- when (runnable ct_st) (tcb_sched_action tcb_sched_enqueue ct);
schedule_choose_new_thread
od \<lbrace>\<lambda>_. scheduler_affects_equiv aag l st\<rbrace>
 6. \<And>st ct ct_st. \<lbrace>?B57 st ct ct_st\<rbrace> gets scheduler_action \<lbrace>\<lambda>x s. (x = resume_cur_thread \<longrightarrow> runnable ct_st \<or> ct = idle_thread s \<longrightarrow> scheduler_affects_equiv aag l st s) \<and> (\<forall>xa. x = switch_thread xa \<longrightarrow> ?R67 st ct ct_st x xa s) \<and> (x = choose_new_thread \<longrightarrow> ?R65 st ct ct_st x s)\<rbrace>
 7. \<And>st ct. \<lbrace>?B56 st ct\<rbrace> get_thread_state ct \<lbrace>?B57 st ct\<rbrace>
 8. \<And>st. \<lbrace>?Q55 st\<rbrace> gets cur_thread \<lbrace>?B56 st\<rbrace>
 9. \<And>st s. ((\<lambda>s. pas_refined aag s \<and> invs s \<and> valid_sched s \<and> guarded_pas_domain aag s \<and> domain_time s \<noteq> 0 \<and> pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {}) and scheduler_equiv aag st and scheduler_affects_equiv aag l st) s \<Longrightarrow> ?Q55 st s
 10. \<And>s. pas_refined aag s \<and> invs s \<and> valid_sched s \<and> guarded_pas_domain aag s \<and> domain_time s \<noteq> 0 \<and> \<not> reads_scheduler_cur_domain aag l s \<Longrightarrow> (pas_refined aag s \<and> invs s \<and> valid_sched s \<and> guarded_pas_domain aag s \<and> domain_time s \<noteq> 0 \<and> \<not> reads_scheduler_cur_domain aag l s) \<and> pas_refined aag s \<and> invs s \<and> valid_sched s \<and> guarded_pas_domain aag s \<and> domain_time s \<noteq> 0 \<and> \<not> reads_scheduler_cur_domain aag l s proof (prove)
goal (2 subgoals):
 1. \<And>st s. ((\<lambda>s. pas_refined aag s \<and> invs s \<and> valid_sched s \<and> guarded_pas_domain aag s \<and> domain_time s \<noteq> 0 \<and> pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {}) and scheduler_equiv aag st and scheduler_affects_equiv aag l st) s \<Longrightarrow> \<forall>sta. st_tcb_at ((=) sta) (cur_thread s) s \<longrightarrow> (scheduler_action s = resume_cur_thread \<longrightarrow> runnable sta \<or> cur_thread s = idle_thread s \<longrightarrow> scheduler_affects_equiv aag l st s) \<and> (\<forall>x. scheduler_action s = switch_thread x \<longrightarrow> (if runnable sta then \<lambda>sa. invs sa \<and> pas_refined aag sa \<and> st_tcb_at runnable x sa \<and> scheduler_equiv aag st sa \<and> domain_time sa \<noteq> 0 \<and> (pas_refined aag and scheduler_affects_equiv aag l st and (\<lambda>sa. pasObjectAbs aag (cur_thread s) \<notin> reads_scheduler aag l)) sa \<and> cur_domain st = cur_domain sa \<and> pasObjectAbs aag x \<notin> reads_scheduler aag l \<and> (valid_queues and st_tcb_at runnable (cur_thread s)) sa \<and> pasDomainAbs aag (cur_domain sa) \<inter> reads_scheduler aag l = {} \<and> invs sa \<and> pas_refined aag sa \<and> scheduler_equiv aag st sa \<and> (pas_refined aag and scheduler_affects_equiv aag l st and (\<lambda>sa. pasObjectAbs aag (cur_thread s) \<notin> reads_scheduler aag l)) sa \<and> (cur_domain st = cur_domain sa \<and> pasObjectAbs aag x \<notin> reads_scheduler aag l \<and> pasDomainAbs aag (cur_domain sa) \<inter> reads_scheduler aag l = {}) \<and> invs sa \<and> pas_refined aag sa \<and> st_tcb_at runnable x sa \<and> scheduler_equiv aag st sa \<and> domain_time sa \<noteq> 0 \<and> (pas_refined aag and scheduler_affects_equiv aag l st and (\<lambda>sa. pasObjectAbs aag (cur_thread s) \<notin> reads_scheduler aag l)) sa \<and> cur_domain st = cur_domain sa \<and> pasObjectAbs aag x \<notin> reads_scheduler aag l \<and> (valid_queues and st_tcb_at runnable (cur_thread s)) sa \<and> pasDomainAbs aag (cur_domain sa) \<inter> reads_scheduler aag l = {} else (\<lambda>s. invs s \<and> (pas_refined aag s \<and> st_tcb_at runnable x s \<and> scheduler_equiv aag st s \<and> domain_time s \<noteq> 0 \<and> scheduler_affects_equiv aag l st s \<and> cur_domain st = cur_domain s \<and> pasObjectAbs aag x \<notin> reads_scheduler aag l \<and> valid_queues s \<and> pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {}) \<and> (invs s \<and> pas_refined aag s \<and> scheduler_equiv aag st s \<and> scheduler_affects_equiv aag l st s \<and> cur_domain st = cur_domain s \<and> pasObjectAbs aag x \<notin> reads_scheduler aag l \<and> pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {}) \<and> invs s \<and> pas_refined aag s \<and> st_tcb_at runnable x s \<and> scheduler_equiv aag st s \<and> domain_time s \<noteq> 0 \<and> scheduler_affects_equiv aag l st s \<and> cur_domain st = cur_domain s \<and> pasObjectAbs aag x \<notin> reads_scheduler aag l \<and> valid_queues s \<and> pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {})) s) \<and> (scheduler_action s = choose_new_thread \<longrightarrow> (if runnable sta then \<lambda>sa. invs sa \<and> pas_refined aag sa \<and> (valid_queues and st_tcb_at runnable (cur_thread s)) sa \<and> domain_time sa \<noteq> 0 \<and> \<not> reads_scheduler_cur_domain aag l sa \<and> scheduler_equiv aag st sa \<and> (pas_refined aag and scheduler_affects_equiv aag l st and (\<lambda>sa. pasObjectAbs aag (cur_thread s) \<notin> reads_scheduler aag l)) sa \<and> cur_domain st = cur_domain sa else (\<lambda>s. invs s \<and> pas_refined aag s \<and> valid_queues s \<and> domain_time s \<noteq> 0 \<and> \<not> reads_scheduler_cur_domain aag l s \<and> scheduler_equiv aag st s \<and> scheduler_affects_equiv aag l st s \<and> cur_domain st = cur_domain s)) s)
 2. \<And>s. pas_refined aag s \<and> invs s \<and> valid_sched s \<and> guarded_pas_domain aag s \<and> domain_time s \<noteq> 0 \<and> \<not> reads_scheduler_cur_domain aag l s \<Longrightarrow> (pas_refined aag s \<and> invs s \<and> valid_sched s \<and> guarded_pas_domain aag s \<and> domain_time s \<noteq> 0 \<and> \<not> reads_scheduler_cur_domain aag l s) \<and> pas_refined aag s \<and> invs s \<and> valid_sched s \<and> guarded_pas_domain aag s \<and> domain_time s \<noteq> 0 \<and> \<not> reads_scheduler_cur_domain aag l s proof (prove)
goal (2 subgoals):
 1. \<And>st s sta. \<lbrakk>pas_refined aag s; invs s; valid_sched s; guarded_pas_domain aag s; domain_time s \<noteq> 0; pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {}; scheduler_equiv aag st s; scheduler_affects_equiv aag l st s; st_tcb_at ((=) sta) (cur_thread s) s\<rbrakk> \<Longrightarrow> (\<forall>x. scheduler_action s = switch_thread x \<longrightarrow> (runnable sta \<longrightarrow> st_tcb_at runnable x s \<and> pasObjectAbs aag (cur_thread s) \<notin> reads_scheduler aag l \<and> cur_domain st = cur_domain s \<and> pasObjectAbs aag x \<notin> reads_scheduler aag l \<and> valid_queues s \<and> st_tcb_at runnable (cur_thread s) s \<and> pasObjectAbs aag (cur_thread s) \<notin> reads_scheduler aag l \<and> cur_domain st = cur_domain s \<and> pasObjectAbs aag x \<notin> reads_scheduler aag l \<and> st_tcb_at runnable x s \<and> pasObjectAbs aag (cur_thread s) \<notin> reads_scheduler aag l \<and> cur_domain st = cur_domain s \<and> pasObjectAbs aag x \<notin> reads_scheduler aag l \<and> valid_queues s \<and> st_tcb_at runnable (cur_thread s) s) \<and> (\<not> runnable sta \<longrightarrow> st_tcb_at runnable x s \<and> cur_domain st = cur_domain s \<and> pasObjectAbs aag x \<notin> reads_scheduler aag l \<and> valid_queues s \<and> cur_domain st = cur_domain s \<and> pasObjectAbs aag x \<notin> reads_scheduler aag l \<and> st_tcb_at runnable x s \<and> cur_domain st = cur_domain s \<and> pasObjectAbs aag x \<notin> reads_scheduler aag l \<and> valid_queues s)) \<and> (scheduler_action s = choose_new_thread \<longrightarrow> (runnable sta \<longrightarrow> valid_queues s \<and> st_tcb_at runnable (cur_thread s) s \<and> pasObjectAbs aag (cur_thread s) \<notin> reads_scheduler aag l \<and> cur_domain st = cur_domain s) \<and> (\<not> runnable sta \<longrightarrow> valid_queues s \<and> cur_domain st = cur_domain s))
 2. \<And>s. pas_refined aag s \<and> invs s \<and> valid_sched s \<and> guarded_pas_domain aag s \<and> domain_time s \<noteq> 0 \<and> \<not> reads_scheduler_cur_domain aag l s \<Longrightarrow> (pas_refined aag s \<and> invs s \<and> valid_sched s \<and> guarded_pas_domain aag s \<and> domain_time s \<noteq> 0 \<and> \<not> reads_scheduler_cur_domain aag l s) \<and> pas_refined aag s \<and> invs s \<and> valid_sched s \<and> guarded_pas_domain aag s \<and> domain_time s \<noteq> 0 \<and> \<not> reads_scheduler_cur_domain aag l s proof (prove)
goal (2 subgoals):
 1. \<And>st s sta. \<lbrakk>pas_refined aag s; invs s; valid_sched s; guarded_pas_domain aag s; domain_time s \<noteq> 0; pasDomainAbs aag (cur_domain s) \<inter> reads_scheduler aag l = {}; scheduler_equiv aag st s; scheduler_affects_equiv aag l st s; st_tcb_at ((=) sta) (cur_thread s) s\<rbrakk> \<Longrightarrow> (\<forall>x. scheduler_action s = switch_thread x \<longrightarrow> (runnable sta \<longrightarrow> st_tcb_at runnable x s \<and> pasObjectAbs aag (cur_thread s) \<notin> reads_scheduler aag l \<and> cur_domain st = cur_domain s \<and> pasObjectAbs aag x \<notin> reads_scheduler aag l \<and> valid_queues s \<and> st_tcb_at runnable (cur_thread s) s \<and> pasObjectAbs aag (cur_thread s) \<notin> reads_scheduler aag l \<and> cur_domain st = cur_domain s \<and> pasObjectAbs aag x \<notin> reads_scheduler aag l \<and> st_tcb_at runnable x s \<and> pasObjectAbs aag (cur_thread s) \<notin> reads_scheduler aag l \<and> cur_domain st = cur_domain s \<and> pasObjectAbs aag x \<notin> reads_scheduler aag l \<and> valid_queues s \<and> st_tcb_at runnable (cur_thread s) s) \<and> (\<not> runnable sta \<longrightarrow> st_tcb_at runnable x s \<and> cur_domain st = cur_domain s \<and> pasObjectAbs aag x \<notin> reads_scheduler aag l \<and> valid_queues s \<and> cur_domain st = cur_domain s \<and> pasObjectAbs aag x \<notin> reads_scheduler aag l \<and> st_tcb_at runnable x s \<and> cur_domain st = cur_domain s \<and> pasObjectAbs aag x \<notin> reads_scheduler aag l \<and> valid_queues s)) \<and> (scheduler_action s = choose_new_thread \<longrightarrow> (runnable sta \<longrightarrow> valid_queues s \<and> st_tcb_at runnable (cur_thread s) s \<and> pasObjectAbs aag (cur_thread s) \<notin> reads_scheduler aag l \<and> cur_domain st = cur_domain s) \<and> (\<not> runnable sta \<longrightarrow> valid_queues s \<and> cur_domain st = cur_domain s))
 2. \<And>s. pas_refined aag s \<and> invs s \<and> valid_sched s \<and> guarded_pas_domain aag s \<and> domain_time s \<noteq> 0 \<and> \<not> reads_scheduler_cur_domain aag l s \<Longrightarrow> (pas_refined aag s \<and> invs s \<and> valid_sched s \<and> guarded_pas_domain aag s \<and> domain_time s \<noteq> 0 \<and> \<not> reads_scheduler_cur_domain aag l s) \<and> pas_refined aag s \<and> invs s \<and> valid_sched s \<and> guarded_pas_domain aag s \<and> domain_time s \<noteq> 0 \<and> \<not> reads_scheduler_cur_domain aag l s