theory Syscall_AI

lemma schedule_ct_activateable[wp]:
  "\<lbrace>invs\<rbrace> (Schedule_A.schedule :: (unit,det_ext) s_monad) \<lbrace>\<lambda>rv. ct_in_state activatable\<rbrace>" apply (simp add: Schedule_A.schedule_def) apply wp apply wpc 
        (* resume current thread *)
         apply wp prefer 2 
       (* choose new thread *)
        apply wp 
      (* switch to thread *)
       apply wpsimp apply (simp add: set_scheduler_action_def) apply (simp | wp gts_wp | wp (once) hoare_drop_imps)+ apply (frule invs_valid_idle) apply (clarsimp simp: ct_in_state_def pred_tcb_at_def obj_at_def valid_idle_def) done

(* Proof state trace *)
proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs\<rbrace> schedule \<lbrace>\<lambda>rv. ct_in_state activatable\<rbrace> proof (prove)
goal (1 subgoal):
 1. \<lbrace>invs\<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 y <- tcb_sched_action tcb_sched_enqueue candidate;
y <- set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else if runnable ct_st \<and> ct_prio = target_prio then do y <- tcb_sched_action tcb_sched_append candidate;
y <- set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else do y <- 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>rv. ct_in_state activatable\<rbrace> proof (prove)
goal (5 subgoals):
 1. \<And>ct ct_st x. \<lbrace>?B9 ct ct_st x\<rbrace> case x of resume_cur_thread \<Rightarrow> do id <- gets idle_thread;
assert (runnable ct_st \<or> ct = id)
od | switch_thread candidate \<Rightarrow> 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 y <- tcb_sched_action tcb_sched_enqueue candidate;
y <- set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else if runnable ct_st \<and> ct_prio = target_prio then do y <- tcb_sched_action tcb_sched_append candidate;
y <- set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else do y <- guarded_switch_to candidate;
set_scheduler_action resume_cur_thread
od
od | choose_new_thread \<Rightarrow> do y <- when (runnable ct_st) (tcb_sched_action tcb_sched_enqueue ct);
schedule_choose_new_thread
od \<lbrace>\<lambda>rv. ct_in_state activatable\<rbrace>
 2. \<And>ct ct_st. \<lbrace>?B8 ct ct_st\<rbrace> gets scheduler_action \<lbrace>?B9 ct ct_st\<rbrace>
 3. \<And>ct. \<lbrace>?B7 ct\<rbrace> get_thread_state ct \<lbrace>?B8 ct\<rbrace>
 4. \<lbrace>?Q6\<rbrace> gets cur_thread \<lbrace>?B7\<rbrace>
 5. \<And>s. invs s \<Longrightarrow> ?Q6 s proof (prove)
goal (7 subgoals):
 1. \<And>ct ct_st x. x = resume_cur_thread \<Longrightarrow> \<lbrace>?R18 ct ct_st x\<rbrace> do id <- gets idle_thread;
assert (runnable ct_st \<or> ct = id)
od \<lbrace>\<lambda>rv. ct_in_state activatable\<rbrace>
 2. \<And>ct ct_st x x2. x = switch_thread x2 \<Longrightarrow> \<lbrace>?R17 ct ct_st x x2\<rbrace> do y <- when (runnable ct_st) (tcb_sched_action tcb_sched_enqueue ct);
it <- gets idle_thread;
target_prio <- ethread_get tcb_priority x2;
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 y <- tcb_sched_action tcb_sched_enqueue x2;
y <- set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else if runnable ct_st \<and> ct_prio = target_prio then do y <- tcb_sched_action tcb_sched_append x2;
y <- set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else do y <- guarded_switch_to x2;
set_scheduler_action resume_cur_thread
od
od \<lbrace>\<lambda>rv. ct_in_state activatable\<rbrace>
 3. \<And>ct ct_st x. x = choose_new_thread \<Longrightarrow> \<lbrace>?R15 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>rv. ct_in_state activatable\<rbrace>
 4. \<And>ct ct_st. \<lbrace>?B8 ct ct_st\<rbrace> gets scheduler_action \<lbrace>\<lambda>x s. (x = resume_cur_thread \<longrightarrow> ?R18 ct ct_st x s) \<and> (\<forall>xa. x = switch_thread xa \<longrightarrow> ?R17 ct ct_st x xa s) \<and> (x = choose_new_thread \<longrightarrow> ?R15 ct ct_st x s)\<rbrace>
 5. \<And>ct. \<lbrace>?B7 ct\<rbrace> get_thread_state ct \<lbrace>?B8 ct\<rbrace>
 6. \<lbrace>?Q6\<rbrace> gets cur_thread \<lbrace>?B7\<rbrace>
 7. \<And>s. invs s \<Longrightarrow> ?Q6 s proof (prove)
goal (7 subgoals):
 1. \<And>ct ct_st x. x = resume_cur_thread \<Longrightarrow> \<lbrace>?R18 ct ct_st x\<rbrace> do id <- gets idle_thread;
assert (runnable ct_st \<or> ct = id)
od \<lbrace>\<lambda>rv. ct_in_state activatable\<rbrace>
 2. \<And>ct ct_st x x2. x = switch_thread x2 \<Longrightarrow> \<lbrace>?R17 ct ct_st x x2\<rbrace> do y <- when (runnable ct_st) (tcb_sched_action tcb_sched_enqueue ct);
it <- gets idle_thread;
target_prio <- ethread_get tcb_priority x2;
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 y <- tcb_sched_action tcb_sched_enqueue x2;
y <- set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else if runnable ct_st \<and> ct_prio = target_prio then do y <- tcb_sched_action tcb_sched_append x2;
y <- set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else do y <- guarded_switch_to x2;
set_scheduler_action resume_cur_thread
od
od \<lbrace>\<lambda>rv. ct_in_state activatable\<rbrace>
 3. \<And>ct ct_st x. x = choose_new_thread \<Longrightarrow> \<lbrace>?R15 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>rv. ct_in_state activatable\<rbrace>
 4. \<And>ct ct_st. \<lbrace>?B8 ct ct_st\<rbrace> gets scheduler_action \<lbrace>\<lambda>x s. (x = resume_cur_thread \<longrightarrow> ?R18 ct ct_st x s) \<and> (\<forall>xa. x = switch_thread xa \<longrightarrow> ?R17 ct ct_st x xa s) \<and> (x = choose_new_thread \<longrightarrow> ?R15 ct ct_st x s)\<rbrace>
 5. \<And>ct. \<lbrace>?B7 ct\<rbrace> get_thread_state ct \<lbrace>?B8 ct\<rbrace>
 6. \<lbrace>?Q6\<rbrace> gets cur_thread \<lbrace>?B7\<rbrace>
 7. \<And>s. invs s \<Longrightarrow> ?Q6 s proof (prove)
goal (6 subgoals):
 1. \<And>ct ct_st x x2. x = switch_thread x2 \<Longrightarrow> \<lbrace>?R17 ct ct_st x x2\<rbrace> do y <- when (runnable ct_st) (tcb_sched_action tcb_sched_enqueue ct);
it <- gets idle_thread;
target_prio <- ethread_get tcb_priority x2;
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 y <- tcb_sched_action tcb_sched_enqueue x2;
y <- set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else if runnable ct_st \<and> ct_prio = target_prio then do y <- tcb_sched_action tcb_sched_append x2;
y <- set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else do y <- guarded_switch_to x2;
set_scheduler_action resume_cur_thread
od
od \<lbrace>\<lambda>rv. ct_in_state activatable\<rbrace>
 2. \<And>ct ct_st x. x = choose_new_thread \<Longrightarrow> \<lbrace>?R15 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>rv. ct_in_state activatable\<rbrace>
 3. \<And>ct ct_st. \<lbrace>?B8 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> ct_in_state activatable s) \<and> (\<forall>xa. x = switch_thread xa \<longrightarrow> ?R17 ct ct_st x xa s) \<and> (x = choose_new_thread \<longrightarrow> ?R15 ct ct_st x s)\<rbrace>
 4. \<And>ct. \<lbrace>?B7 ct\<rbrace> get_thread_state ct \<lbrace>?B8 ct\<rbrace>
 5. \<lbrace>?Q6\<rbrace> gets cur_thread \<lbrace>?B7\<rbrace>
 6. \<And>s. invs s \<Longrightarrow> ?Q6 s proof (prove)
goal (6 subgoals):
 1. \<And>ct ct_st x. x = choose_new_thread \<Longrightarrow> \<lbrace>?R15 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>rv. ct_in_state activatable\<rbrace>
 2. \<And>ct ct_st x x2. x = switch_thread x2 \<Longrightarrow> \<lbrace>?R17 ct ct_st x x2\<rbrace> do y <- when (runnable ct_st) (tcb_sched_action tcb_sched_enqueue ct);
it <- gets idle_thread;
target_prio <- ethread_get tcb_priority x2;
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 y <- tcb_sched_action tcb_sched_enqueue x2;
y <- set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else if runnable ct_st \<and> ct_prio = target_prio then do y <- tcb_sched_action tcb_sched_append x2;
y <- set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else do y <- guarded_switch_to x2;
set_scheduler_action resume_cur_thread
od
od \<lbrace>\<lambda>rv. ct_in_state activatable\<rbrace>
 3. \<And>ct ct_st. \<lbrace>?B8 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> ct_in_state activatable s) \<and> (\<forall>xa. x = switch_thread xa \<longrightarrow> ?R17 ct ct_st x xa s) \<and> (x = choose_new_thread \<longrightarrow> ?R15 ct ct_st x s)\<rbrace>
 4. \<And>ct. \<lbrace>?B7 ct\<rbrace> get_thread_state ct \<lbrace>?B8 ct\<rbrace>
 5. \<lbrace>?Q6\<rbrace> gets cur_thread \<lbrace>?B7\<rbrace>
 6. \<And>s. invs s \<Longrightarrow> ?Q6 s proof (prove)
goal (6 subgoals):
 1. \<And>ct ct_st x. x = choose_new_thread \<Longrightarrow> \<lbrace>?R15 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>rv. ct_in_state activatable\<rbrace>
 2. \<And>ct ct_st x x2. x = switch_thread x2 \<Longrightarrow> \<lbrace>?R17 ct ct_st x x2\<rbrace> do y <- when (runnable ct_st) (tcb_sched_action tcb_sched_enqueue ct);
it <- gets idle_thread;
target_prio <- ethread_get tcb_priority x2;
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 y <- tcb_sched_action tcb_sched_enqueue x2;
y <- set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else if runnable ct_st \<and> ct_prio = target_prio then do y <- tcb_sched_action tcb_sched_append x2;
y <- set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else do y <- guarded_switch_to x2;
set_scheduler_action resume_cur_thread
od
od \<lbrace>\<lambda>rv. ct_in_state activatable\<rbrace>
 3. \<And>ct ct_st. \<lbrace>?B8 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> ct_in_state activatable s) \<and> (\<forall>xa. x = switch_thread xa \<longrightarrow> ?R17 ct ct_st x xa s) \<and> (x = choose_new_thread \<longrightarrow> ?R15 ct ct_st x s)\<rbrace>
 4. \<And>ct. \<lbrace>?B7 ct\<rbrace> get_thread_state ct \<lbrace>?B8 ct\<rbrace>
 5. \<lbrace>?Q6\<rbrace> gets cur_thread \<lbrace>?B7\<rbrace>
 6. \<And>s. invs s \<Longrightarrow> ?Q6 s proof (prove)
goal (5 subgoals):
 1. \<And>ct ct_st x x2. x = switch_thread x2 \<Longrightarrow> \<lbrace>?R17 ct ct_st x x2\<rbrace> do y <- when (runnable ct_st) (tcb_sched_action tcb_sched_enqueue ct);
it <- gets idle_thread;
target_prio <- ethread_get tcb_priority x2;
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 y <- tcb_sched_action tcb_sched_enqueue x2;
y <- set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else if runnable ct_st \<and> ct_prio = target_prio then do y <- tcb_sched_action tcb_sched_append x2;
y <- set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else do y <- guarded_switch_to x2;
set_scheduler_action resume_cur_thread
od
od \<lbrace>\<lambda>rv. ct_in_state activatable\<rbrace>
 2. \<And>ct ct_st. \<lbrace>?B8 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> ct_in_state activatable s) \<and> (\<forall>xa. x = switch_thread xa \<longrightarrow> ?R17 ct ct_st x xa s) \<and> (x = choose_new_thread \<longrightarrow> (if runnable ct_st then invs else invs) s)\<rbrace>
 3. \<And>ct. \<lbrace>?B7 ct\<rbrace> get_thread_state ct \<lbrace>?B8 ct\<rbrace>
 4. \<lbrace>?Q6\<rbrace> gets cur_thread \<lbrace>?B7\<rbrace>
 5. \<And>s. invs s \<Longrightarrow> ?Q6 s proof (prove)
goal (5 subgoals):
 1. \<And>ct ct_st x x2. x = switch_thread x2 \<Longrightarrow> \<lbrace>?R17 ct ct_st x x2\<rbrace> do y <- when (runnable ct_st) (tcb_sched_action tcb_sched_enqueue ct);
it <- gets idle_thread;
target_prio <- ethread_get tcb_priority x2;
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 y <- tcb_sched_action tcb_sched_enqueue x2;
y <- set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else if runnable ct_st \<and> ct_prio = target_prio then do y <- tcb_sched_action tcb_sched_append x2;
y <- set_scheduler_action choose_new_thread;
schedule_choose_new_thread
od else do y <- guarded_switch_to x2;
set_scheduler_action resume_cur_thread
od
od \<lbrace>\<lambda>rv. ct_in_state activatable\<rbrace>
 2. \<And>ct ct_st. \<lbrace>?B8 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> ct_in_state activatable s) \<and> (\<forall>xa. x = switch_thread xa \<longrightarrow> ?R17 ct ct_st x xa s) \<and> (x = choose_new_thread \<longrightarrow> (if runnable ct_st then invs else invs) s)\<rbrace>
 3. \<And>ct. \<lbrace>?B7 ct\<rbrace> get_thread_state ct \<lbrace>?B8 ct\<rbrace>
 4. \<lbrace>?Q6\<rbrace> gets cur_thread \<lbrace>?B7\<rbrace>
 5. \<And>s. invs s \<Longrightarrow> ?Q6 s proof (prove)
goal (13 subgoals):
 1. \<And>ct ct_st x2 it target_prio ct_prio fastfail cur_dom highest. \<lbrakk>fastfail \<longrightarrow> highest; runnable ct_st \<longrightarrow> ct_prio \<noteq> target_prio\<rbrakk> \<Longrightarrow> \<lbrace>?B50 ct ct_st (switch_thread x2) x2 () it target_prio ct_prio fastfail cur_dom highest ()\<rbrace> set_scheduler_action resume_cur_thread \<lbrace>\<lambda>rv. ct_in_state activatable\<rbrace>
 2. \<And>ct ct_st x x2 y it target_prio ct_prio fastfail cur_dom highest. \<lbrakk>x = switch_thread x2; \<not> (fastfail \<and> \<not> highest); \<not> (runnable ct_st \<and> ct_prio = target_prio)\<rbrakk> \<Longrightarrow> \<lbrace>?R45 ct ct_st x x2 y it target_prio ct_prio fastfail cur_dom highest\<rbrace> guarded_switch_to x2 \<lbrace>?B50 ct ct_st x x2 y it target_prio ct_prio fastfail cur_dom highest\<rbrace>
 3. \<And>ct ct_st x x2 y it target_prio ct_prio fastfail cur_dom. x = switch_thread x2 \<Longrightarrow> \<lbrace>?B38 ct ct_st x x2 y it target_prio ct_prio fastfail cur_dom\<rbrace> gets (is_highest_prio cur_dom target_prio) \<lbrace>\<lambda>highest s. (fastfail \<and> \<not> highest \<longrightarrow> invs s) \<and> (\<not> (fastfail \<and> \<not> highest) \<longrightarrow> (runnable ct_st \<and> ct_prio = target_prio \<longrightarrow> invs s) \<and> (\<not> (runnable ct_st \<and> ct_prio = target_prio) \<longrightarrow> ?R45 ct ct_st x x2 y it target_prio ct_prio fastfail cur_dom highest s))\<rbrace>
 4. \<And>ct ct_st x x2 y it target_prio ct_prio fastfail. x = switch_thread x2 \<Longrightarrow> \<lbrace>?B37 ct ct_st x x2 y it target_prio ct_prio fastfail\<rbrace> gets cur_domain \<lbrace>?B38 ct ct_st x x2 y it target_prio ct_prio fastfail\<rbrace>
 5. \<And>ct ct_st x x2 y it target_prio ct_prio. x = switch_thread x2 \<Longrightarrow> \<lbrace>?B36 ct ct_st x x2 y it target_prio ct_prio\<rbrace> schedule_switch_thread_fastfail ct it ct_prio target_prio \<lbrace>?B37 ct ct_st x x2 y it target_prio ct_prio\<rbrace>
 6. \<And>ct ct_st x x2 y it target_prio. x = switch_thread x2 \<Longrightarrow> \<lbrace>?B35 ct ct_st x x2 y it target_prio\<rbrace> ethread_get_when (ct \<noteq> it) tcb_priority ct \<lbrace>?B36 ct ct_st x x2 y it target_prio\<rbrace>
 7. \<And>ct ct_st x x2 y it. x = switch_thread x2 \<Longrightarrow> \<lbrace>?B34 ct ct_st x x2 y it\<rbrace> ethread_get tcb_priority x2 \<lbrace>?B35 ct ct_st x x2 y it\<rbrace>
 8. \<And>ct ct_st x x2 y. x = switch_thread x2 \<Longrightarrow> \<lbrace>?B33 ct ct_st x x2 y\<rbrace> gets idle_thread \<lbrace>?B34 ct ct_st x x2 y\<rbrace>
 9. \<And>ct ct_st x x2. x = switch_thread x2 \<Longrightarrow> \<lbrace>?R17 ct ct_st x x2\<rbrace> when (runnable ct_st) (tcb_sched_action tcb_sched_enqueue ct) \<lbrace>?B33 ct ct_st x x2\<rbrace>
 10. \<And>ct ct_st. \<lbrace>?B8 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> ct_in_state activatable s) \<and> (\<forall>xa. x = switch_thread xa \<longrightarrow> ?R17 ct ct_st x xa s) \<and> (x = choose_new_thread \<longrightarrow> (if runnable ct_st then invs else invs) s)\<rbrace>
A total of 13 subgoals... proof (prove)
goal (13 subgoals):
 1. \<And>ct ct_st x2 it target_prio ct_prio fastfail cur_dom highest. \<lbrakk>fastfail \<longrightarrow> highest; runnable ct_st \<longrightarrow> ct_prio \<noteq> target_prio\<rbrakk> \<Longrightarrow> \<lbrace>?B50 ct ct_st (switch_thread x2) x2 () it target_prio ct_prio fastfail cur_dom highest ()\<rbrace> modify (scheduler_action_update (\<lambda>_. resume_cur_thread)) \<lbrace>\<lambda>rv. ct_in_state activatable\<rbrace>
 2. \<And>ct ct_st x x2 y it target_prio ct_prio fastfail cur_dom highest. \<lbrakk>x = switch_thread x2; \<not> (fastfail \<and> \<not> highest); \<not> (runnable ct_st \<and> ct_prio = target_prio)\<rbrakk> \<Longrightarrow> \<lbrace>?R45 ct ct_st x x2 y it target_prio ct_prio fastfail cur_dom highest\<rbrace> guarded_switch_to x2 \<lbrace>?B50 ct ct_st x x2 y it target_prio ct_prio fastfail cur_dom highest\<rbrace>
 3. \<And>ct ct_st x x2 y it target_prio ct_prio fastfail cur_dom. x = switch_thread x2 \<Longrightarrow> \<lbrace>?B38 ct ct_st x x2 y it target_prio ct_prio fastfail cur_dom\<rbrace> gets (is_highest_prio cur_dom target_prio) \<lbrace>\<lambda>highest s. (fastfail \<and> \<not> highest \<longrightarrow> invs s) \<and> (\<not> (fastfail \<and> \<not> highest) \<longrightarrow> (runnable ct_st \<and> ct_prio = target_prio \<longrightarrow> invs s) \<and> (\<not> (runnable ct_st \<and> ct_prio = target_prio) \<longrightarrow> ?R45 ct ct_st x x2 y it target_prio ct_prio fastfail cur_dom highest s))\<rbrace>
 4. \<And>ct ct_st x x2 y it target_prio ct_prio fastfail. x = switch_thread x2 \<Longrightarrow> \<lbrace>?B37 ct ct_st x x2 y it target_prio ct_prio fastfail\<rbrace> gets cur_domain \<lbrace>?B38 ct ct_st x x2 y it target_prio ct_prio fastfail\<rbrace>
 5. \<And>ct ct_st x x2 y it target_prio ct_prio. x = switch_thread x2 \<Longrightarrow> \<lbrace>?B36 ct ct_st x x2 y it target_prio ct_prio\<rbrace> schedule_switch_thread_fastfail ct it ct_prio target_prio \<lbrace>?B37 ct ct_st x x2 y it target_prio ct_prio\<rbrace>
 6. \<And>ct ct_st x x2 y it target_prio. x = switch_thread x2 \<Longrightarrow> \<lbrace>?B35 ct ct_st x x2 y it target_prio\<rbrace> ethread_get_when (ct \<noteq> it) tcb_priority ct \<lbrace>?B36 ct ct_st x x2 y it target_prio\<rbrace>
 7. \<And>ct ct_st x x2 y it. x = switch_thread x2 \<Longrightarrow> \<lbrace>?B34 ct ct_st x x2 y it\<rbrace> ethread_get tcb_priority x2 \<lbrace>?B35 ct ct_st x x2 y it\<rbrace>
 8. \<And>ct ct_st x x2 y. x = switch_thread x2 \<Longrightarrow> \<lbrace>?B33 ct ct_st x x2 y\<rbrace> gets idle_thread \<lbrace>?B34 ct ct_st x x2 y\<rbrace>
 9. \<And>ct ct_st x x2. x = switch_thread x2 \<Longrightarrow> \<lbrace>?R17 ct ct_st x x2\<rbrace> when (runnable ct_st) (tcb_sched_action tcb_sched_enqueue ct) \<lbrace>?B33 ct ct_st x x2\<rbrace>
 10. \<And>ct ct_st. \<lbrace>?B8 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> ct_in_state activatable s) \<and> (\<forall>xa. x = switch_thread xa \<longrightarrow> ?R17 ct ct_st x xa s) \<and> (x = choose_new_thread \<longrightarrow> (if runnable ct_st then invs else invs) s)\<rbrace>
A total of 13 subgoals... proof (prove)
goal (1 subgoal):
 1. \<And>s. invs s \<Longrightarrow> \<forall>st. st_tcb_at ((=) st) (cur_thread s) s \<longrightarrow> scheduler_action s = resume_cur_thread \<longrightarrow> (runnable st \<longrightarrow> ct_in_state activatable s) \<and> (cur_thread s = idle_thread s \<longrightarrow> ct_in_state activatable s) proof (prove)
goal (1 subgoal):
 1. \<And>s. \<lbrakk>invs s; valid_idle s\<rbrakk> \<Longrightarrow> \<forall>st. st_tcb_at ((=) st) (cur_thread s) s \<longrightarrow> scheduler_action s = resume_cur_thread \<longrightarrow> (runnable st \<longrightarrow> ct_in_state activatable s) \<and> (cur_thread s = idle_thread s \<longrightarrow> ct_in_state activatable s) proof (prove)
goal:
No subgoals!