theory ADT_IF

lemma schedule_guarded_pas_domain:
  "\<lbrace>guarded_pas_domain aag and einvs and pas_refined aag\<rbrace>
   schedule
   \<lbrace>\<lambda>_. guarded_pas_domain aag\<rbrace>" supply ethread_get_wp[wp del] apply (simp add: schedule_def) apply (wpsimp wp: guarded_pas_domain_lift[where f="activate_thread"]
                    guarded_pas_domain_lift[where f="set_scheduler_action f" for f]
                    guarded_switch_to_lift switch_to_thread_guarded_pas_domain
                    next_domain_valid_queues activate_thread_cur_thread gts_wp
         | wpc
         | rule choose_thread_guarded_pas_domain
         | simp add: schedule_choose_new_thread_def ethread_get_when_def split del: if_split
         | wp (once) hoare_drop_imp[where f="ethread_get t v" for t v]
         | wp (once) hoare_drop_imp[where f="schedule_switch_thread_fastfail c i cp p" for c i cp p])+ apply (wp hoare_drop_imp) apply (wpsimp wp: guarded_pas_domain_lift[where f="activate_thread"]
                        guarded_pas_domain_lift[where f="set_scheduler_action f" for f]
                        guarded_switch_to_lift switch_to_thread_guarded_pas_domain
                        next_domain_valid_queues activate_thread_cur_thread gts_wp
             | wpc
             | rule choose_thread_guarded_pas_domain
             | simp add: schedule_choose_new_thread_def ethread_get_when_def split del: if_split
             | wp (once) hoare_drop_imp[where f="ethread_get t v" for t v]
             | wp (once) hoare_drop_imp[where f="schedule_switch_thread_fastfail c i cp p" for c i cp p])+ apply (fastforce intro: switch_to_cur_domain switch_thread_runnable
                    simp: valid_sched_def elim!: st_tcb_weakenE)+ done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>guarded_pas_domain aag and einvs and pas_refined aag\<rbrace> schedule \<lbrace>\<lambda>_. guarded_pas_domain aag\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>guarded_pas_domain aag and einvs and pas_refined aag\<rbrace> schedule \<lbrace>\<lambda>_. guarded_pas_domain aag\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>guarded_pas_domain aag and einvs and pas_refined aag\<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>_. guarded_pas_domain aag\<rbrace> proof (prove)
goal (6 subgoals):
 1. \<And>ct ct_st x2. runnable ct_st \<Longrightarrow> \<lbrace>?P'285 ct ct_st (switch_thread x2) x2\<rbrace> tcb_sched_action tcb_sched_enqueue ct \<lbrace>\<lambda>rv s. (ct \<noteq> idle_thread s \<longrightarrow> pas_refined aag s \<and> valid_queues s \<and> st_tcb_at runnable x2 s \<and> pasObjectAbs aag x2 \<in> pasDomainAbs aag (cur_domain s)) \<and> pas_refined aag s \<and> valid_queues s \<and> st_tcb_at runnable x2 s \<and> pasObjectAbs aag x2 \<in> pasDomainAbs aag (cur_domain s)\<rbrace>
 2. \<And>ct ct_st x. x = choose_new_thread \<Longrightarrow> \<lbrace>?R10 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>_. guarded_pas_domain aag\<rbrace>
 3. \<And>ct ct_st. \<lbrace>?B3 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> guarded_pas_domain aag s) \<and> (\<forall>xa. x = switch_thread xa \<longrightarrow> (if runnable ct_st then \<lambda>s. pas_refined aag s \<and> (valid_queues and st_tcb_at runnable ct) s \<and> st_tcb_at runnable xa s \<and> ?P'285 ct ct_st x xa s else (\<lambda>s. pas_refined aag s \<and> (valid_queues s \<and> st_tcb_at runnable xa s) \<and> (ct \<noteq> idle_thread s \<longrightarrow> (pas_refined aag s \<and> valid_queues s \<and> st_tcb_at runnable xa s) \<and> pasObjectAbs aag xa \<in> pasDomainAbs aag (cur_domain s)) \<and> (pas_refined aag s \<and> valid_queues s \<and> st_tcb_at runnable xa s) \<and> pasObjectAbs aag xa \<in> pasDomainAbs aag (cur_domain s))) s) \<and> (x = choose_new_thread \<longrightarrow> ?R10 ct ct_st x s)\<rbrace>
 4. \<And>ct. \<lbrace>?B2 ct\<rbrace> get_thread_state ct \<lbrace>?B3 ct\<rbrace>
 5. \<lbrace>?Q1\<rbrace> gets cur_thread \<lbrace>?B2\<rbrace>
 6. \<And>s. (guarded_pas_domain aag and einvs and pas_refined aag) s \<Longrightarrow> ?Q1 s proof (prove)
goal (5 subgoals):
 1. \<And>ct ct_st x. x = choose_new_thread \<Longrightarrow> \<lbrace>?R10 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>_. guarded_pas_domain aag\<rbrace>
 2. \<And>ct ct_st. \<lbrace>?B3 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> guarded_pas_domain aag s) \<and> (\<forall>xa. x = switch_thread xa \<longrightarrow> (if runnable ct_st then \<lambda>s. pas_refined aag s \<and> (valid_queues and st_tcb_at runnable ct) s \<and> st_tcb_at runnable xa s \<and> (pas_refined aag s \<and> (valid_queues and st_tcb_at runnable ct) s \<and> st_tcb_at runnable xa s \<and> pasObjectAbs aag xa \<in> pasDomainAbs aag (cur_domain s)) \<and> pas_refined aag s \<and> (valid_queues and st_tcb_at runnable ct) s \<and> st_tcb_at runnable xa s \<and> pasObjectAbs aag xa \<in> pasDomainAbs aag (cur_domain s) else (\<lambda>s. pas_refined aag s \<and> (valid_queues s \<and> st_tcb_at runnable xa s) \<and> (ct \<noteq> idle_thread s \<longrightarrow> (pas_refined aag s \<and> valid_queues s \<and> st_tcb_at runnable xa s) \<and> pasObjectAbs aag xa \<in> pasDomainAbs aag (cur_domain s)) \<and> (pas_refined aag s \<and> valid_queues s \<and> st_tcb_at runnable xa s) \<and> pasObjectAbs aag xa \<in> pasDomainAbs aag (cur_domain s))) s) \<and> (x = choose_new_thread \<longrightarrow> ?R10 ct ct_st x s)\<rbrace>
 3. \<And>ct. \<lbrace>?B2 ct\<rbrace> get_thread_state ct \<lbrace>?B3 ct\<rbrace>
 4. \<lbrace>?Q1\<rbrace> gets cur_thread \<lbrace>?B2\<rbrace>
 5. \<And>s. (guarded_pas_domain aag and einvs and pas_refined aag) s \<Longrightarrow> ?Q1 s proof (prove)
goal (1 subgoal):
 1. \<And>s st. \<lbrakk>guarded_pas_domain aag s; invs s; valid_list s; valid_sched s; pas_refined aag s\<rbrakk> \<Longrightarrow> (runnable st \<longrightarrow> st_tcb_at ((=) st) (cur_thread s) s \<longrightarrow> (\<forall>x. scheduler_action s = switch_thread x \<longrightarrow> valid_queues s \<and> st_tcb_at runnable (cur_thread s) s \<and> st_tcb_at runnable x s \<and> valid_queues s \<and> st_tcb_at runnable (cur_thread s) s \<and> st_tcb_at runnable x s \<and> pasObjectAbs aag x \<in> pasDomainAbs aag (cur_domain s)) \<and> (scheduler_action s = choose_new_thread \<longrightarrow> valid_queues s \<and> st_tcb_at runnable (cur_thread s) s)) \<and> (\<not> runnable st \<longrightarrow> st_tcb_at ((=) st) (cur_thread s) s \<longrightarrow> (\<forall>x. scheduler_action s = switch_thread x \<longrightarrow> valid_queues s \<and> st_tcb_at runnable x s \<and> (cur_thread s \<noteq> idle_thread s \<longrightarrow> valid_queues s \<and> st_tcb_at runnable x s \<and> pasObjectAbs aag x \<in> pasDomainAbs aag (cur_domain s)) \<and> valid_queues s \<and> st_tcb_at runnable x s \<and> pasObjectAbs aag x \<in> pasDomainAbs aag (cur_domain s)) \<and> (scheduler_action s = choose_new_thread \<longrightarrow> valid_queues s)) proof (prove)
goal:
No subgoals!